
| domain | Spass | Setheo | adaptive | lemma | competitive | cooperative   |    |     |     |     |      |    |
|--------------------------------------------------------------------------|----|-----|-----|-----|------|----|
| A NA                                                                     | 0  | 2.  | 2.  | 2   | 4    |    |
| BO                                                                       | 4  | u   | 5   | 4   | 5    | 6  |
| CAT                                                                      | 11 | 14  |     |     |      |    |
| 6                                                                        | 4  | 8   |     |     |      |    |
| CIV                                                                      | 0  | 0   |     |     |      |    |
| l                                                                        | l  | 1   |     |     |      |    |
| COL                                                                      | 2  | 10  | 2   | 14  | 12   | 16 |
| G EO                                                                     | 10 | 11  | 14  | 15  |      |    |
| 8                                                                        |    |     |     |     |      |    |
| GRP                                                                      | 30 | 36  | 30  | 38  |      |    |
| l                                                                        | 3  |     |     |     |      |    |
| HEN                                                                      | 5  | g   | 10  | 1 2 |      |    |
| LCL                                                                      | 25 | 8   | 26  | 9   | 30   | 31 |
| LDA                                                                      | c  | 9   |     |     |      |    |
| 1                                                                        | 1  | 6   | 9   |     |      |    |
| NUM                                                                      | 0  | 0   |     |     |      |    |
| l                                                                        | 1  | l   | l   |     |      |    |
| PLA                                                                      |    | 2   | 3   | 2   |      | w  |
| RNG                                                                      | 9  |     |     |     |      |    |
| 4                                                                        | 6  | 4   | 6   | 9   |      |    |
| ROB                                                                      | 2  | l   | 3   | l   |      | 3  |
| SET                                                                      | 21 | 24  | 24  | 35  | 39   | 48 |
| SY N                                                                     | 0  | 0   | l   | 0   | 0    | l  |
| 18                                                                       | 7  | 145 | 103 | 172 | 21 1 |    |

Table 1: Integration of top-down/bottom-up approaches by cooperative provers: solved
The results reveal the high potential of our approach to significantly improve on single provers. Spass is only able to solve 55.9% of the problems which can be solved by cooperation, SETHEO can only solve 36.5%. Competition of provers is very successful because of the very different behavior of the provers. But even a competitive prover consisting of SPASS and SETHEO can only solve 81.5% of the problems solvable by cooperation. Hence, cooperation is really important in order to increase the success rate. When integrating subgoal clauses into Spass its solvability rate is increased by 22.9%. In the most cases subgoal clauses take part in the search process and can help to reorder the search in a favorable manner. The use of lemmas increases SETHEO's performance by 33.8%. The increase of the solvability rate of SETHEO is really due to occurring resource reductions. In almost all cases where a substantial speed-up is obtained we could find a proof with a smaller resource. Then, the lemmas are used as expected, i.e. they are able to close subgoals that occur after few inferences and whose ME proof would require many inferences.

When taking a closer look at the results we can recognize the following. A prover which already shows a rather satisfactory behavior in a specific domain can often profit from others. Cooperation can entail that other hard problems can additionally be solved. However, if a prover is not suitable for a certain domain then cooperation will normally not result in a significant increase of its performance. Because of the fact that SETHEO and SPASS show a very different behavior in the most cases at least one prover can be improved in a certain domain.