as resources. As start clauses for an adaptive refinement we selected N rf = 5 subgoal clauses. These parameters allowed the efficient generation of all subgoal clauses within the initial segments of the search tree. Usually with this method at most 500 subgoal clauses were generated, i.e. about the same number as when employing variant 1. For the selection of subgoal clauses that are to be transmitted to SPASS we used domain-dependent parameters. For CAT, COL, and LDA we used 100 clauses. In the other domains in preliminary experiments the use of 30 clauses achieved the best results.

The bottom-up lem mas were selected via the functions ϕ δυ , ϕ δυ , and ϕ δυ . We selected with each of the functions a maximum of 10 clauses.

The setting of Setheo was automatically chosen as described by Moser et al. (1997).

The Spass standard heuristic essentially selects clauses of the smallest size. Periodically, clauses are selected with breadth-first search.

## 5.2 Experimental Results

In the following we compare the results of our cooperative prover with the single provers. This comparison is performed regarding the whole TPTP library. After that, we analyze runtimes in few selected domains of TPTP.

## 5.2.1 Comparison Of Different Variants In The Tptp

Table 1 presents results of our experiments. It shows the number of solved hard problems in certain domains of TPTP. Solved means that a proof could be found within 300 seconds. We consider a problem to be hard if neither SPASS nor SETHEO are able to solve it within 10 seconds. The table only presents the results of such domains where hard problems exist and where at least one hard problem could be solved by any of the considered variants.

Note that the table cannot give hints on the power of the single provers. This is because it does not give the complete number of problems which can be solved by each single prover in the whole domain. Since many non-hard problems are in the TPTP this number is usually much higher than the number of solved hard problems. Nevertheless, the table is sufficient for analyzing the performance of our cooperative system since only the hard problems are interesting for studying the potential of cooperation.

Column 1 of the table displays the name of the domain. Columns 2 and 3 present the nmber of solved problems of SPASS and SETHEO (on a SPARCstation-20/712) when working alone.  Column 4 shows the number of solved problems of SPASS when it obtains subgoal clauses from SETHEO which are generated regarding variant 2. This variant performs better than variant 1 (see also the following subsection). Column 5 displays the number of solved problems of SETHEO when it obtains bottom-up generated lemmas from SPASS. In that case we always employed vanant 2 for generating subgoal clauses (recall that the selection of lemmas depends on the way how subgoal clauses are generated). Column 6 gives the nmber of solved problems of a competitive version of SPASS and SETHEO in order to show that our cooperative proveris indeed much more powerful than a simple competitive parallel prover. Finally, in column 7 we can find the number of solved problems of our cooperative system.