The components of SSCPA do not cooperate, with no communication of control information or intermediate results. Therefore SSCPA can solve at most the union of the problems that the individual components can solve within the same total CPU time limit, i.e., there is no gain in depth of coverage. CSSCPA is a cooperative competition parallel ATP system, which extends SSCPA by a mechanism for transferring intermediate results between the components. The result is a compositional competition-cooperation parallel ATP system, which has high breadth of coverage and also increased depth of coverage.
CSSCPA employs a formula librarian (the FLi) that can do subsumption and also detect unit contradictions in the clauses it holds. When given an ATP problem, CSSCPA first sends a copy of the problem to the FLi, where it is stored. CSSCPA then selects and starts components to use, and parses their standard outputs for logical consequences. Each logical consequence is forwarded to the FLi. If at any time a component finds a solution, then CSSCPA is stopped and success is reported. The FLi keeps an incoming clause only if keeping it improves the overall quality of its clause set, in the sense that a better clause set is one that is easier to refute. For example, the FLi's clause set is improved if an incoming logical consequence subsumes a clause in the set. Whenever the quality of clause set in the FLi improves, the FLi reports the improvement to CSSCPA. When the clause set in the FLi has improved significantly relative to the original input problem, CSSCPA stops the components. CSSCPA then collects the improved clause set from the FLi, and restarts with the improved clause set as the input problem. CSCCPA thus creates a sequence of successively easier problems to solve. The arrangement is clearly sound. The synergistic effects allow the system to solve problems that none of the component systems are able to solve independently, thus increasing the depth of coverage.