Proof: Consider the following set C of clauses (again we employ >= 0):

$${\mathcal{C}}=\left\{\begin{array}{l}{{}}\\ {{}}\\ {{}}\end{array}\right.$$
$$\left.\begin{array}{l l l}{{\{l_{4},\,l_{6},\,l_{7}\},}}&{{\{l_{4},\,l_{6},\,\neg l_{7}\},}}&{{\{l_{3},\,\neg l_{4}\},}}\\ {{\{l_{3},\,\neg l_{6}\},}}&{{\{\neg l_{2},\,\neg l_{4}\},}}&{{\{l_{4},\,\neg l_{5},\,\neg l_{6}\},}}\\ {{\{\neg l_{2},\,l_{5}\},}}&{{\{l_{1},\,l_{2},\,\neg l_{3}\},}}&{{\{\neg l_{1},\,l_{2},\,\neg l_{3}\}}}\end{array}\right\}$$

Each minimal refutation proof for this set requires 9 resolution steps, e.g.:
Now, it holds:

$${\mathcal{S}}_{n e\,g}^{\mathit{I n f}\,,2,{\mathcal{C}}}=\left\{\begin{array}{l}{{}}\\ {{}}\end{array}\right.$$
$$\begin{array}{r l}{{\{\neg l_{2},l_{6},l_{7}\},}}&{{}}\\ {{\{\neg l_{1},\neg l_{3},\neg l_{4}\},}}&{{}}\end{array}\begin{array}{r l}{{\{\neg l_{2},l_{6},\neg l_{7}\},}}&{{}}\\ {{\{\neg l_{2},\neg l_{5},\neg l_{6}\}}}\end{array}\begin{array}{r l}{{}}\\ {{}}\end{array}$$

When enumerating all proofs for C ∪ S Inf. 2.c one can recognize that the minimal proof length cannot be reduced.

| 14, 16, 171           |
|-----------------------|
| { l 4 , l 6 , - l 7 } |
| { 13, -14 }           |
| { 13, ---- 1          |
| {-l2, -l4 }           |
| {l4, -l5, -l6}        |
| {-l2, 15}             |
| {li, l2, -l3}         |
| {-li, l2, -l3}        |

| [10, res(1, 2)]        | {l              |
|------------------------|-----------------|
| [11, res(6, 10)]       | { 14, -15}      |
| [ 1 2, res(3, 10)]     | { I3, I6 }      |
| [ 1 3 , res( 7 , 11 )] | {-l 2, 14 }     |
| [14, res(5, 13)]       | {-{-}           |
| [15, res(4, 12)]       | { }             |
| [16, res(8, 9)]        | { l 2 , ¬ l 3 } |
| [17, res(14, 16)]      | {-}             |
| [18, res(15, 17)]      | □               |

□
In the case where equality is involved in our proof problems, we obtain a theorem analogous to the previous one:
Theorem 3.4 For each resource k > 1 there is a set of unit equationsC where the minimal sssssee and the state of the Proof: In analogy to Theorem 3.2.

□
We can recognize that for CTC neg the results are essentially the same as for CTC . In general the reduction of the heuristic search for a proof cannot be guaranteed and proof

| 1, ax   |
|---------|
| 2, ax   |
| [3, ax  |
| [4, ax  |
| 5, ax   |
| [6, ax] |
| [7, ax] |
| 8, ax   |
| [9, ax] |

lengths may not always be reduced. In practice, however, we could again observe that a restructuring of the search caused by subgoal clauses often allows proofs to be found faster.

In the following we simply assume that inferences with subgoal clauses are not omitted by a superposition prover, i.e. that they are involved in the proof search. We want to deal in more detail with the problem of identifying subgoal clauses which can lead to a large reduction of the search effort and how we can efficiently select such subgoal clauses.

This problem has to be tackled with heuristics since there is —as we have examined—no theoretical guarantee and also no method to decide whethersubgoal clauses are useful.

## 3.2  Relevancy-Based  Generation Of Subgoal  Clauses

Even when using small resources k the sets S lnf,k,c and S lnf,k,c can become quite large.

Thus, it is not sensible to integrate all subgoal clauses from S Inf,k,c or S Inf,k,c into the