Light-Weight Integration of SAT Solving into First-Order
               Reasoners -- First Experiments

                  Stephan Schulz

We describe a light-weight integration of the propositional SAT solver
PicoSAT and the saturation-based superposition prover E. The proof
search is driven by the saturation prover. Periodically, the
saturation is interrupted, and all first-order clauses are
grounded. The resulting ground problem is converted to a propositional
format and handed to the SAT solver. If the SAT solver reports
unsatisfiability, the proof is extracted and reported on the
first-order level. First experiments demonstrate the viability of the
approach and suggest future extensions. They also yield interesting
information about the structure of the search space.