Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers.  Minor fixes to ambqi.  Preparation for CASC proof output.  Add NNF option.