diff --git a/src/duality/duality.h b/src/duality/duality.h
index 4539b4711..82d729104 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -91,13 +91,23 @@ namespace Duality {
 
       expr SimplifyAndOr(const std::vector<expr> &args, bool is_and);
 
+      expr ReallySimplifyAndOr(const std::vector<expr> &args, bool is_and);
+
+      int MaxIndex(hash_map<ast,int> &memo, const Term &t);
+
+      bool IsClosedFormula(const Term &t);
+
   private:
 
       void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
       int CountOperatorsRec(hash_set<ast> &memo, const Term &t);
       void RemoveRedundancyOp(bool pol, std::vector<expr> &args, hash_map<ast, Term> &smemo);
       Term RemoveRedundancyRec(hash_map<ast, Term> &memo, hash_map<ast, Term> &smemo, const Term &t);
-    Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val);
+      Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val);
+      expr ReduceAndOr(const std::vector<expr> &args, bool is_and, std::vector<expr> &res);
+      expr FinishAndOr(const std::vector<expr> &args, bool is_and);
+      expr PullCommonFactors(std::vector<expr> &args, bool is_and);
+
 
 };
 
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 5260dc7e9..3fd74993c 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -25,6 +25,7 @@ Revision History:
 #include "duality_profiling.h"
 #include <algorithm>
 #include <fstream>
+#include <set>
 
 #ifndef WIN32
 // #define Z3OPS
@@ -369,18 +370,20 @@ namespace Duality {
   }
 
   bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){
-    if(!lit.is_app())
-      return false;
-    decl_kind k = lit.decl().get_decl_kind();
-    if(k == Not){
-      if(IsLiteral(lit.arg(0),atom,val)){
-	val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); 
-	return true;
+    if(!(lit.is_quantifier() && IsClosedFormula(lit))){
+      if(!lit.is_app())
+	return false;
+      decl_kind k = lit.decl().get_decl_kind();
+      if(k == Not){
+	if(IsLiteral(lit.arg(0),atom,val)){
+	  val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); 
+	  return true;
+	}
+	return false;
       }
-      return false;
+      if(k == And || k == Or || k == Iff || k == Implies)
+	return false;
     }
-    if(k == And || k == Or || k == Iff || k == Implies)
-      return false;
     atom = lit;
     val = ctx.bool_val(true);
     return true;
@@ -396,19 +399,78 @@ namespace Duality {
     return !f;
   }
 
-  expr Z3User::SimplifyAndOr(const std::vector<expr> &args, bool is_and){
-    std::vector<expr> sargs;
+  expr Z3User::ReduceAndOr(const std::vector<expr> &args, bool is_and, std::vector<expr> &res){
     for(unsigned i = 0; i < args.size(); i++)
       if(!eq(args[i],ctx.bool_val(is_and))){
 	if(eq(args[i],ctx.bool_val(!is_and)))
 	  return ctx.bool_val(!is_and);
-	sargs.push_back(args[i]);
+	res.push_back(args[i]);
       }
-    if(sargs.size() == 0)
+    return expr();
+  }
+
+  expr Z3User::FinishAndOr(const std::vector<expr> &args, bool is_and){
+    if(args.size() == 0)
       return ctx.bool_val(is_and);
-    if(sargs.size() == 1)
-      return sargs[0];
-    return ctx.make(is_and ? And : Or,sargs);
+    if(args.size() == 1)
+      return args[0];
+    return ctx.make(is_and ? And : Or,args);
+  }
+
+  expr Z3User::SimplifyAndOr(const std::vector<expr> &args, bool is_and){
+    std::vector<expr> sargs;
+    expr res = ReduceAndOr(args,is_and,sargs);
+    if(!res.null()) return res;
+    return FinishAndOr(sargs,is_and);
+  }
+
+  expr Z3User::PullCommonFactors(std::vector<expr> &args, bool is_and){
+    
+    // first check if there's anything to do...
+    if(args.size() < 2)
+      return FinishAndOr(args,is_and);
+    for(unsigned i = 0; i < args.size(); i++){
+      const expr &a = args[i];
+      if(!(a.is_app() && a.decl().get_decl_kind() == (is_and ? Or : And)))
+	return FinishAndOr(args,is_and);
+    }
+    std::vector<expr> common;
+    for(unsigned i = 0; i < args.size(); i++){
+      unsigned n = args[i].num_args();
+      std::vector<expr> v(n),w;
+      for(unsigned j = 0; j < n; j++)
+	v[j] = args[i].arg(j);
+      std::less<ast> comp;
+      std::sort(v.begin(),v.end(),comp);
+      if(i == 0)
+	common.swap(v);
+      else {
+	std::set_intersection(common.begin(),common.end(),v.begin(),v.end(),std::back_inserter(w),comp);
+	common.swap(w);
+      }
+    }  
+    if(common.empty())
+      return FinishAndOr(args,is_and);
+    std::set<ast> common_set(common.begin(),common.end());
+    for(unsigned i = 0; i < args.size(); i++){
+      unsigned n = args[i].num_args();
+      std::vector<expr> lits;
+      for(unsigned j = 0; j < n; j++){
+	const expr b = args[i].arg(j);
+	if(common_set.find(b) == common_set.end())
+	  lits.push_back(b);
+      }
+      args[i] = SimplifyAndOr(lits,!is_and);
+    }  
+    common.push_back(SimplifyAndOr(args,is_and));
+    return SimplifyAndOr(common,!is_and);
+  }
+
+  expr Z3User::ReallySimplifyAndOr(const std::vector<expr> &args, bool is_and){
+    std::vector<expr> sargs;
+    expr res = ReduceAndOr(args,is_and,sargs);
+    if(!res.null()) return res;
+    return PullCommonFactors(sargs,is_and);
   }
 
   Z3User::Term Z3User::SubstAtomTriv(const expr &foo, const expr &atom, const expr &val){
@@ -436,10 +498,17 @@ namespace Duality {
 	std::vector<Term> args(nargs);
 	for(int i = 0; i < nargs; i++)
 	  args[i] = SubstAtom(memo,t.arg(i),atom,val);
-	res = SimplifyAndOr(args,k == And);
+	res = ReallySimplifyAndOr(args, k==And);
 	return res;
       }
     }
+    else if(t.is_quantifier() && atom.is_quantifier()){
+      if(eq(t,atom))
+	res = val;
+      else
+	res = clone_quantifier(t,SubstAtom(memo,t.body(),atom,val));
+      return res;
+    }
     res = SubstAtomTriv(t,atom,val);
     return res;
   }
@@ -474,14 +543,19 @@ namespace Duality {
 	  args.push_back(RemoveRedundancyRec(memo, smemo, t.arg(i)));
 
 	decl_kind k = f.get_decl_kind();
-	if(k == And)
+	if(k == And){
 	  RemoveRedundancyOp(true,args,smemo);
-	else if(k == Or)
+	  res = ReallySimplifyAndOr(args, true);
+	}
+	else if(k == Or){
 	  RemoveRedundancyOp(false,args,smemo);
-	if(k == Equal && args[0].get_id() > args[1].get_id())
-	  std::swap(args[0],args[1]);
-	
-	res = f(args.size(),&args[0]);
+	  res = ReallySimplifyAndOr(args, false);
+	}
+	else {
+	  if(k == Equal && args[0].get_id() > args[1].get_id())
+	    std::swap(args[0],args[1]);
+	  res = f(args.size(),&args[0]);
+	}
       }
     else if (t.is_quantifier())
       {
@@ -1991,7 +2065,13 @@ namespace Duality {
       }
     }
     else if (f.is_quantifier()){
-      GetGroundLitsUnderQuants(memo,f.body(),res,1);
+#if 0
+      // treat closed quantified formula as a literal 'cause we hate nested quantifiers
+      if(under && IsClosedFormula(f)) 
+	res.push_back(f);
+      else
+#endif
+	GetGroundLitsUnderQuants(memo,f.body(),res,1);
       return;
     }
     if(under && f.is_ground())
@@ -2019,14 +2099,18 @@ namespace Duality {
 	  atom = lit.arg(0);
 	}
 	expr etval = ctx.bool_val(tval);
-	int b = SubtermTruth(stt_memo,atom);
-	if(b == (tval ? 1 : 0))
-	  subst[atom] = etval;
+	if(atom.is_quantifier())
+	  subst[atom] = etval; // this is a bit desperate, since we can't eval quants
 	else {
-	  if(b == 0 || b == 1){
-	    etval = ctx.bool_val(b ? true : false);
+	  int b = SubtermTruth(stt_memo,atom);
+	  if(b == (tval ? 1 : 0))
 	    subst[atom] = etval;
-	    conjuncts.push_back(b ? atom : !atom);
+	  else {
+	    if(b == 0 || b == 1){
+	      etval = ctx.bool_val(b ? true : false);
+	      subst[atom] = etval;
+	      conjuncts.push_back(b ? atom : !atom);
+	    }
 	  }
 	}
       }
@@ -2038,7 +2122,7 @@ namespace Duality {
 	g = g && ctx.make(And,conjuncts);
       g = g.simplify();
     }
-#if 0
+#if 1
     expr g_old = g;
     g = RemoveRedundancy(g);
     bool changed = !eq(g,g_old);
@@ -2441,6 +2525,37 @@ namespace Duality {
     return SubstBoundRec(memo, subst, 0, t);
   }
 
+  int Z3User::MaxIndex(hash_map<ast,int> &memo, const Term &t)
+  {
+    std::pair<ast,int> foo(t,-1);
+    std::pair<hash_map<ast,int>::iterator, bool> bar = memo.insert(foo);
+    int &res = bar.first->second;
+    if(!bar.second) return res;
+    if (t.is_app()){
+      func_decl f = t.decl();
+      int nargs = t.num_args();
+      for(int i = 0; i < nargs; i++){
+	int m = MaxIndex(memo, t.arg(i));
+	if(m > res)
+	  res = m;
+      }
+    }
+    else if (t.is_quantifier()){
+      int bound = t.get_quantifier_num_bound();
+      res = MaxIndex(memo,t.body()) - bound;
+    }
+    else if (t.is_var()) {
+      res = t.get_index_value();
+    }
+    return res;
+  }
+
+  bool Z3User::IsClosedFormula(const Term &t){
+    hash_map<ast,int> memo;
+    return MaxIndex(memo,t) < 0;
+  }
+  
+
   /** Convert a collection of clauses to Nodes and Edges in the RPFP.
 
       Predicate unknowns are uninterpreted predicates not
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 63f3dd251..fae914292 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -109,36 +109,49 @@ public:
      symbols and assign each to a frame. THe assignment is heuristic.
   */
 
-  void scan_skolems_rec(hash_set<ast> &memo, const ast &proof){
-    std::pair<hash_set<ast>::iterator,bool> bar = memo.insert(proof);
-    if(!bar.second)
-      return;
+  int scan_skolems_rec(hash_map<ast,int> &memo, const ast &proof, int frame){
+    std::pair<ast,int> foo(proof,INT_MAX);
+    std::pair<AstToInt::iterator, bool> bar = memo.insert(foo);
+    int &res = bar.first->second;
+    if(!bar.second) return res;
     pfrule dk = pr(proof);
-    if(dk == PR_SKOLEMIZE){
+    if(dk == PR_ASSERTED){
+      ast ass = conc(proof);
+      res = frame_of_assertion(ass);
+    }
+    else if(dk == PR_SKOLEMIZE){
       ast quanted = arg(conc(proof),0);
       if(op(quanted) == Not)
 	quanted = arg(quanted,0);
-      range r = ast_range(quanted);
-      if(range_is_empty(r))
-	r = ast_scope(quanted);
+      // range r = ast_range(quanted);
+      // if(range_is_empty(r))
+      range r = ast_scope(quanted);
       if(range_is_empty(r))
 	throw "can't skolemize";
-      int frame = range_max(r);
+      if(frame == INT_MAX || !in_range(frame,r))
+	frame = range_max(r); // this is desperation -- may fail
       if(frame >= frames) frame = frames - 1;
       add_frame_range(frame,arg(conc(proof),1));
       r = ast_scope(arg(conc(proof),1));
     }
+    else if(dk==PR_MODUS_PONENS_OEQ){
+      frame = scan_skolems_rec(memo,prem(proof,0),frame);
+      scan_skolems_rec(memo,prem(proof,1),frame);
+    }
     else {
       unsigned nprems = num_prems(proof);
       for(unsigned i = 0; i < nprems; i++){
-	scan_skolems_rec(memo,prem(proof,i));
+	int bar = scan_skolems_rec(memo,prem(proof,i),frame);
+	if(res == INT_MAX || res == bar) res = bar;
+	else if(bar != INT_MAX) res = -1;
       }
     }
+    return res;
   }
 
   void scan_skolems(const ast &proof){
-    hash_set<ast> memo;
-    scan_skolems_rec(memo,proof);
+    hash_map<ast,int> memo;
+    scan_skolems_rec(memo,proof, INT_MAX);
   }
 
   // determine locality of a proof term