Change default option to --inst-when=full-last-call (interleave instantiation and theory combination).  Fix inefficiency in NNF, enable by default.  Set best defaults for --mbqi=abs.