Anita Jindal's dissertation[3] included a parallel implementation of OTTER based on the distributed memory computational model. Ralph Butler and Ross Overbeek also did a version based on FDB. The idea is to specialize the work to be done by separate processes that communicate via messages. Thus some processes derive new clauses and send them to subsumption processes, who filter the derived clauses and send the survivors on to a master process which then distributes new work back to the generating processes. Each process maintains a copy of the database of clauses that has been used as given clauses. The separate copies of the database can become slightly different from one another, but by by having the master process perform a final subsumption test prior to updating his copy of the database, consistency and redundancy control are maintained. The system has obtained good speedups on large problems.