The article is organized as follows. We start with a brief overview of superposition and model elimination (Section 2). Moreover, we discuss strengths and weaknesses of the calculi in more detail and introduce our approach for combining the strengths of both calculi.  In Section 3 we address effects of the integration of ME subgoal clauses into the search state of a superposition-based prover. Furthermore, we describe two variants of a relevancy-based filtering of subgoal clauses. Section 4 deals with the use of bottom-up generated lemmas. We discuss in detail the ability of the produced clauses in order to help decrease proof lengths for refuting a given set of clauses as well as to reorder the search space in an appropriate manner. Based on this discussion, we introduce several relevancy measures. In Section 5, an experimental study conducted with the high-performance theorem provers SETHEO and SPASS reveals the potential of our techniques. We have chosen these systems in order to show that our concept can easily be integrated into existing systems and is even able to improve on the performance of very powerful provers. Finally, in Section 6 an overview of related approaches for top-down/bottom-up integration concludes the article.

## 2. A Framework For Coupling Top-Down And Bottom-Up Provers

In the following, we introduce typical representatives of top-down and bottom-up calculi and discuss their strengths and weaknesses in detail. After that, we sketch the basics of our methodology in order to combine these calculi,

## 2.1  Automated Theorem Proving With Superposition And Model Elimination

The general problem in first-order theorem proving is to show the inconsistency of a set C
of clauses. A clause is a set of literals. As already discussed, theorem provers usually utilize either top-down or bottom-up calculi for accomplishing this task.

Typically, a bottom-up calculus contains several inference rules which can be applied to a set of clauses that constitute the search state. Generally, the inference rules can be divided into two classes: Expansion inference rules permit the generation of new clauses and contraction inference rules delete clauses or replace them by others. The most popular bottom-upcalculus is the resolution calculus (Robinson, 1965). There, the expansion rules are resolution and factoring. The resolution calculus can be extended with contraction rules, e.g. the deletion of tautologies.  If equality is involved in a problem it is sensible to employ the superposition calculus (Bachmair & Ganzinger, 1994), which extends resolution with specific rules suitable for handling equations. The expansion rules of the superposition calculus are superposition, equality resolution, and equality factoring. Again, additional contraction rules such as tautology deletion, subsumption, condensing, and rewriting can be employed. It is to be emphasized that for our study we employ the version of the ssssee to the content of entails that factoring is only applied to positive literals.

A bottom-up theorem prover usually maintains a set FP of so-called potential or passive clauses from which it selects and removes one clause C at a time. This clause is put into the set FA of activated clauses. Activated clauses are, unlike potential clauses, allowed to produce new clauses via the application of some inference rules. The inferred new clauses are put into FP. Initially, FA = 0 and FP = C. The indeterministic selection or aclivation