Model building into quantifiers engine.  Simplify axiom-inst mode.