

![0_image_0.png](0_image_0.png)

Our criterion aims mainly at excluding lemmas that are applicable in too many cases and hence introduce too many solutions of subgoals that do not lead to a refutation of the input clauses. In contrast to expanding inferences we rate contraction inferences positively. Indeed, ME provers do not have contracting inferences. But as shown by Letz et al. (1992), subsumption can partly be simulated by subsumption constraints. Hence, clauses that are able to contract many other clauses can support search pruning techniques.

## 4.3.3 D Erivation -B Ased S Election

The second filter function QBU tries to select facts that are able to close subgoals that are very hard to solve with a connection-tableau-based prover. In order to estimate this, we consider the derivation history of a fact. We employ this filter function only if equality is involved in a problem.

Example 4.1 Let {f(f(x)) = g(x)} and {h(b) = f(b)} be axioms.  Then, the clause
{b) = f(h(b))} can be derived by one superposition step. However, if -g(b) = f(h(b)) is a subgoal of an ME proof, its proof is more complicated (see Figure 4).

In general, if the superposition step is performed at a position p and [p] denotes the depth of the position (above [p] = 1), then at most [p] + 5 inferences are needed in order to prove the result of such a superposition step. The proof necessitates at most a depth of II I + 3.

This example shows that the simulation of the specific equational operations of a superposition prover necessitates a high depth as well as inference resource in an ME prover. That is, lemmas derived by many superposition steps are able to close subgoals that cannot be solved by an ME prover within small resources. Hence, if such lemmas are applicable large resource reductions possibly occur for depth or inference oriented bounds. The judgment function φ B U employs this criterion. Again, the filter function φ B U selects facts with the highest value regarding this judgment function.