We give a saturation procedure that takes
a theory as input, and returns a decision
procedure for that theory when it halts.
In addition, it returns a bound on
the complexity of that theory: O(n lg(n))
for some theories (such as the theory of lists),
polynomial for other theories (including all
equational theories that halt), and simply
exponential for other theories (such as the
theory of arrays).
