In [24] Slaney and Lusk focused on parallelizing the closure algorithm in a completely general setting. The application of this parallel algorithm to OTTER yielded ROO[9], a shared-memory parallel theorem prover completely compatible with OTTER, including back subsumption and back demodulation. In ROO, there is only one copy of the formula database, and the parallelism comes from parallelizing the outer loop of the closure algorithm. The complicated part is ensuring that separate processes do not add the same newly derived clause to the database. That is, once more the basic issue is redundancy control. For details of how this problem is solved, see [9].
An extensive set of experiments, together with clauses for all the problems, appears in [6]. ROO, running on a Sequent symmetry, is currently the fastest system in use at Argonne. A planned port to the Alliant FX/2800 will make it substantially faster.