We give a method for extending efficient SMT theorem provers
to handle quantifiers, using Superposition inference rules.
In our method, the input formula is converted into CNF as in
traditional first order logic theorem provers.  The ground
clauses are given to the SMT theorem prover, which runs a
DPLL method to build partial models.  The partial model is
passed to a congruence closure procedure, as is normally
done in SMT.  The congruence closure calculates all reduced
(dis)equalities in the partial model and passes them to a
Superposition procedure, along with a justification.  The
Superposition procedure then performs an inference rule, which
we call Justified Superposition, between the (dis)equalities
and the nonground clauses, plus usual Superposition rules
with the nonground clauses.  Any resulting ground clauses
are provided to the DPLL engine.  We prove the completeness
of this method, using a nontrivial modification of the
Bachmair Ganzinger model generation technique.  We believe
this combination uses the best of both worlds, an SMT process
to handle ground clauses efficiently, and a Superposition
procedure which uses orderings to handle the nonground clauses.
We also present some ideas for making the Superposition part
more efficient, where we compile the inferences using ideas
from Schematic Paramodulation and techniques from databases
and expert systems.  An implementation based on these ideas
is planned.