It is interesting to find out whether certain characteristics of problems lead to a high or low performance of the cooperative system. We examine whether the characteristics
"a domain contains equality" and "a domain contains non-Horn problems" influence the performance. First, we should note that these characteristics do not completely determine the performance of the cooperative system. There are gains of efficiency for all kinds of problem, regardless of the type of clauses occurring in the problems. But we can at least observe some tendencies.

Firstly, we can observe that the cooperation approach is especially well-suited for problems containing equality. The best results are obtained in the domains CAT, GRP, and SET which contain many problems with equality. When analyzing proof runs we can find two reasons for this. In such domains SPASS is able to support SETHEO because it has much stronger inferences for handling equality than SETHEO. SPASS can often derive "difficult" lemmas with few inferences, i.e. lemmas whose derivation would require many inferences by SETHEO. SETHEO can support SPASS because it is able to make transformations of the proof goal that Spass cannot perform because of its fixed ordering used for superposition.

This can increase the flexibility of the proof search performed by Spass.

Secondly, we consider whether the fact that a domain contains mostly Horn or non-Horn problems influences the performance of the cooperation approach. Considering the domains where the cooperation approach could successfully be applied we can notice that successes could be obtained for Horn (e.g., COL) as well as non-Horn domains (e.g., SET). In the domains where no hard problems could be solved (neither sequentially nor with cooperation) often the percentage of non-Horn clauses is rather high (note that these domains do not appear in the table). The main reason for this, however, appears to be that the single provers show a weak performance in these domains. A strong relationship between the performance of the cooperative prover and the fact whether a problem is Horn or non-Horn could not really be found in the experiments.

## 5.2.2 Analysis Of Runtimes In Selected Domains

Up to now we only considered the number of solved problems. In addition, it is interesting to analyze whether the use of subgoal clauses or lemmas can speed-up the proof search in general, i.e. also for problems that can be solved by single provers. Short run times are especially important if theorem provers are used within interactive proverenvironments. We restrict ourselves to the three domains CAT, COL, and LDA and are going to analyze the runtimes in more detail Table 2 presents the runtimes when tackling hard problems of the three test domains. We omitted all problems that could neither be solved by a single prover when working alone, nor by any of the cooperation variants. Column 1 of the table displays the name of the problem. Columns 2 and 3 present the runtimes of Spass and Setheo (on a SPARCstation-20/712) when working alone, columns 4 and 5 the runtimes of SPASS when it obtains subgoal clauses from SETHEO which are generated regarding variants 1 and 2, respectively. Note that the runtimes include the generation and selection time of subgoal clauses, and the transmission to Spass. Column 6 displays the runtime of Setheo if it obtains bottom-up generated lemmas from Spass. In that case we always employed variant 2 for generating subgoal clauses. Also these runtimes include the preprocessing of SPASS and the transmission and