diff --git a/examples/sudoku/kb.h b/examples/sudoku/kb.h
index 211dfc51fe9968ca3bb12a10a635b5c9c9aa6c47..313262b351bff0c7417ac20f8e034381c3fb19ab 100644
--- a/examples/sudoku/kb.h
+++ b/examples/sudoku/kb.h
@@ -16,17 +16,19 @@
 #include "game.h"
 #include "timer.h"
 
+using namespace limbo;
+
 class KnowledgeBase {
  public:
   KnowledgeBase(const Game* g, int max_k)
       : max_k_(max_k),
-        VAL_(ctx_.CreateSort()),
-        val_(ctx_.CreateFunction(VAL_, 2)) {
+        VAL_(CreateSort()),
+        val_(CreateFunctionSymbol(VAL_, 2)) {
     limbo::format::RegisterSort(VAL_, "");
     limbo::format::RegisterSymbol(val_, "val");
     using namespace limbo::format::cpp;
     for (std::size_t i = 1; i <= 9; ++i) {
-      vals_.push_back(ctx_.CreateName(VAL_));
+      vals_.push_back(CreateName(VAL_));
       std::stringstream ss;
       ss << i;
       limbo::format::RegisterSymbol(vals_.back().symbol(), ss.str());
@@ -35,7 +37,7 @@ class KnowledgeBase {
       for (std::size_t y = 1; y <= 9; ++y) {
         for (std::size_t yy = 1; yy <= 9; ++yy) {
           if (y != yy) {
-            ctx_.AddClause(val(x, y) != val(x, yy));
+            kb_.Add(val(x, y) != val(x, yy));
           }
         }
       }
@@ -44,7 +46,7 @@ class KnowledgeBase {
       for (std::size_t xx = 1; xx <= 9; ++xx) {
         for (std::size_t y = 1; y <= 9; ++y) {
           if (x != xx) {
-            ctx_.AddClause(val(x, y) != val(xx, y));
+            kb_.Add(val(x, y) != val(xx, y));
           }
         }
       }
@@ -56,7 +58,7 @@ class KnowledgeBase {
             for (std::size_t y = 3*j-2; y <= 3*j; ++y) {
               for (std::size_t yy = 3*j-2; yy <= 3*j; ++yy) {
                 if (x != xx || y != yy) {
-                  ctx_.AddClause(val(x, y) != val(xx, yy));
+                  kb_.Add(val(x, y) != val(xx, yy));
                 }
               }
             }
@@ -70,14 +72,14 @@ class KnowledgeBase {
         for (std::size_t i = 1; i <= 9; ++i) {
           lits.push_back(limbo::Literal::Eq(val(x, y), n(i)));
         }
-        ctx_.AddClause(limbo::Clause(lits.begin(), lits.end()));
+        kb_.Add(limbo::Clause(lits.begin(), lits.end()));
       }
     }
     for (std::size_t x = 1; x <= 9; ++x) {
       for (std::size_t y = 1; y <= 9; ++y) {
         int i = g->get(Point(x, y));
         if (i != 0) {
-          ctx_.AddClause(val(x, y) == n(i));
+          kb_.Add(val(x, y) == n(i));
         }
       }
     }
@@ -85,17 +87,15 @@ class KnowledgeBase {
 
   int max_k() const { return max_k_; }
 
-  limbo::Solver* solver() { return ctx_.solver(); }
-  const limbo::Solver& solver() const { return ctx_.solver(); }
+  limbo::Solver& solver() { return kb_.sphere(0); }
+  const limbo::Solver& solver() const { return kb_.sphere(0); }
   const limbo::Setup& setup() const { return solver().setup(); }
 
-  void Add(Point p, int i) {
-    ctx_.AddClause(val(p) == n(i));
-  }
+  void Add(Point p, int i) { kb_.Add(Clause{Literal::Eq(val(p), n(i))}); }
 
   limbo::internal::Maybe<int> Val(Point p, int k) {
     t_.start();
-    const limbo::internal::Maybe<limbo::Term> r = solver()->Determines(k, val(p), limbo::Solver::kConsistencyGuarantee);
+    const limbo::internal::Maybe<limbo::Term> r = solver().Determines(k, val(p), limbo::Solver::kConsistencyGuarantee);
     assert(std::all_of(limbo::internal::int_iterator<size_t>(1), limbo::internal::int_iterator<size_t>(9),
            [&](size_t i) { return solver()->Entails(k, val(p) == n(i), limbo::Solver::kConsistencyGuarantee) ==
                                   (r && r.val == n(i)); }));
@@ -115,25 +115,46 @@ class KnowledgeBase {
   void ResetTimer() { t_.reset(); }
 
  private:
-  limbo::format::cpp::HiTerm n(std::size_t n) const {
+  limbo::Term n(std::size_t n) const {
     return vals_[n-1];
   }
 
-  limbo::format::cpp::HiTerm val(Point p) const {
+  limbo::Term val(Point p) const {
     return val(p.x, p.y);
   }
 
-  limbo::format::cpp::HiTerm val(std::size_t x, std::size_t y) const {
-    return val_(vals_[x-1], vals_[y-1]);
+  limbo::Term val(std::size_t x, std::size_t y) const {
+    return CreateFunction(val_, limbo::Term::Vector{vals_[x-1], vals_[y-1]});
+  }
+
+  limbo::Symbol::Sort CreateSort() const {
+    return limbo::Symbol::Factory::Instance()->CreateSort();
   }
 
+  limbo::Symbol CreateFunctionSymbol(limbo::Symbol::Sort sort, limbo::Symbol::Arity arity) const {
+    return limbo::Symbol::Factory::Instance()->CreateFunction(sort, arity);
+  }
+
+  limbo::Term CreateName(limbo::Symbol::Sort sort) const {
+    return limbo::Term::Factory::Instance()->CreateTerm(limbo::Symbol::Factory::Instance()->CreateName(sort));
+  }
+
+  limbo::Term CreateVariable(limbo::Symbol::Sort sort) const {
+    return limbo::Term::Factory::Instance()->CreateTerm(limbo::Symbol::Factory::Instance()->CreateVariable(sort));
+  }
+
+  limbo::Term CreateFunction(limbo::Symbol symbol, const limbo::Term::Vector& args) const {
+    return limbo::Term::Factory::Instance()->CreateTerm(symbol, args);
+  }
+
+
   int max_k_;
 
-  limbo::format::cpp::Context ctx_;
+  limbo::KnowledgeBase kb_;
 
   limbo::Symbol::Sort VAL_;
-  limbo::format::cpp::HiSymbol val_;
-  std::vector<limbo::format::cpp::HiTerm> vals_;
+  limbo::Symbol val_;
+  limbo::Term::Vector vals_;
 
   Timer t_;
 };
diff --git a/examples/tui/example-battleship-1x4.limbo b/examples/tui/example-battleship-1x4.limbo
index 82127ee18d0198c82ba81aa580992a8e4587fa60..ca1479e93d73cceef121d06fbb5dec1c732371d7 100644
--- a/examples/tui/example-battleship-1x4.limbo
+++ b/examples/tui/example-battleship-1x4.limbo
@@ -73,4 +73,3 @@ while Ex p G (~K<0> fired(p)=T ^ ~K<2> water(p)=T) {
     Call: bs_print()
 }
 
-
diff --git a/src/limbo/format/cpp/syntax.h b/src/limbo/format/cpp/syntax.h
index d3cef4caf2e016a0e8ec2ead942d40fe4f2c72f2..89ac9ec86bf133385214d641d6d5d2c47fd7b2a0 100644
--- a/src/limbo/format/cpp/syntax.h
+++ b/src/limbo/format/cpp/syntax.h
@@ -92,11 +92,11 @@ class Context {
     Formula::Ref psi = phi.NF(sf(), tf());
     internal::Maybe<Clause> c = psi->AsUnivClause();
     assert(c);
-    solver_.AddClause(c.val);
+    solver_.grounder().AddClause(c.val);
   }
 
   void AddClause(const Clause& c) {
-    solver_.AddClause(c);
+    solver_.grounder().AddClause(c);
   }
 
   Solver* solver() { return &solver_; }
diff --git a/src/limbo/grounder.h b/src/limbo/grounder.h
index 83d8c478f26af760877b61c722af821fc824cb03..aa5feb02d05d12783b1e6061c06271ab4485012b 100644
--- a/src/limbo/grounder.h
+++ b/src/limbo/grounder.h
@@ -427,18 +427,22 @@ class Grounder {
   // inconsistent.
 
   Setup::Result AddClause(const Clause& c, Undo* undo = nullptr, bool do_not_add_if_inconsistent = false) {
-    return AddClauses(internal::singleton_range(c), undo, do_not_add_if_inconsistent);
+    auto r = internal::singleton_range(c);
+    return AddClauses(r.begin(), r.end(), undo, do_not_add_if_inconsistent);
   }
 
-  template<typename T>
-  Setup::Result AddClauses(const T& clauses, Undo* undo = nullptr, const bool do_not_add_if_inconsistent = false) {
+  template<typename InputIt>
+  Setup::Result AddClauses(InputIt first,
+                           InputIt last,
+                           Undo* undo = nullptr,
+                           const bool do_not_add_if_inconsistent = false) {
     // Add c to ungrounded_clauses.
     // Add new names in c to names.
     // Add variables to vars, generate plus-names.
     // Re-ground.
     Ply& p = new_ply();
-    for (const Clause& c : clauses) {
-      Ungrounded<Clause> uc(c);
+    for (; first != last; ++first) {
+      Ungrounded<Clause> uc(*first);
       uc.val.Traverse([this, &p, &uc](Term t) {
         if (t.variable()) {
           uc.vars.insert(t);
@@ -552,6 +556,8 @@ class Grounder {
 
   void UndoLast() { pop_ply(); }
 
+  void Consolidate() { MergePlies(true); }
+
   Literal Variablify(Literal a) {
     assert(a.ground());
     Term::Vector ns;
@@ -567,7 +573,6 @@ class Grounder {
     }, tf_);
   }
 
-  Plies plies(Plies::Policy p = Plies::kAll) const { return Plies(this, p); }
   LhsTerms lhs_terms(Plies::Policy p = Plies::kAll) const { return LhsTerms(this, p); }
   // The additional name must not be used after RhsName's death.
   RhsNames rhs_names(Term t, Plies::Policy p = Plies::kSinceSetup) { return RhsNames(this, t, p); }
@@ -678,6 +683,8 @@ class Grounder {
     }
   }
 
+  Plies plies(Plies::Policy p = Plies::kAll) const { return Plies(this, p); }
+
   Ply& last_ply() { assert(!plies_.empty()); return plies_.back(); }
   const Ply& last_ply() const { assert(!plies_.empty()); return plies_.back(); }
 
@@ -1010,6 +1017,54 @@ rescan:
     p.clauses.shallow_setup = p.clauses.full_setup->shallow_copy();
   }
 
+  void MergePlies(bool minimize) {
+    assert(!plies_.empty());
+    auto p = plies_.end();
+    for (auto it = plies_.begin(); it != plies_.end(); ++it) {
+      if (it->clauses.full_setup) {
+        p = it;
+      }
+    }
+    if (p == plies_.end()) {
+      return;
+    }
+    bool after = false;
+    for (auto it = plies_.begin(); it != plies_.end(); ++it) {
+      assert(!it->do_not_add_if_inconsistent);
+      if (it == p) {
+        after = true;
+        continue;
+      }
+      p->clauses.ungrounded.insert(p->clauses.ungrounded.end(),
+                                   it->clauses.ungrounded.begin(), it->clauses.ungrounded.end());
+      p->names.mentioned.insert(it->names.mentioned);
+      p->names.plus_max.insert(it->names.plus_max);
+      p->names.plus_new.insert(it->names.plus_new);
+      p->names.plus_mentioned.insert(it->names.plus_mentioned);
+      if (after) {
+        assert(!it->clauses.full_setup);
+        p->clauses.shallow_setup.Immortalize();
+        p->relevant.ungrounded.insert(it->relevant.ungrounded.begin(), it->relevant.ungrounded.end());
+        p->relevant.terms.insert(it->relevant.terms);
+        p->lhs_rhs.ungrounded.insert(it->lhs_rhs.ungrounded.begin(), it->lhs_rhs.ungrounded.end());
+        for (auto& lhs_rhs : it->lhs_rhs.map) {
+          auto lhs = p->lhs_rhs.map.find(lhs_rhs.first);
+          if (lhs == p->lhs_rhs.map.end()) {
+            p->lhs_rhs.map.insert(lhs_rhs);
+          } else {
+            lhs->second.insert(lhs_rhs.second.begin(), lhs_rhs.second.end());
+          }
+        }
+      }
+    }
+    if (minimize) {
+      p->clauses.full_setup->Minimize();
+    }
+    plies_.erase(plies_.begin(), p);
+    plies_.erase(std::next(p), plies_.end());
+    assert(plies_.size() == 1);
+  }
+
   Term::Factory* const tf_;
   NamePool name_pool_;
   VariablePool var_pool_;
diff --git a/src/limbo/internal/intmap.h b/src/limbo/internal/intmap.h
index ea51e8b9346a160cf4bb9d116e61b1dd62ad9169..58c44f44e8ebf3a434f8bf280fefcd4cca4ecb4c 100644
--- a/src/limbo/internal/intmap.h
+++ b/src/limbo/internal/intmap.h
@@ -122,6 +122,12 @@ class IntMultiMap {
     return n;
   }
 
+  void insert(const IntMultiMap& m) {
+    for (Key key : m.keys()) {
+      (*this)[key].insert(map_[key].begin(), map_[key].end());
+    }
+  }
+
   size_t erase(Key key, const T& val) {
     size_t n = map_[key].erase(val);
     size_ -= n;
@@ -197,20 +203,12 @@ class IntMultiSet {
 
   size_t insert(const T& val) { return map_.insert(key_(val), val); }
 
-  void erase(const T& val) { map_.erase(key_(val), val); }
+  void insert(const IntMultiSet& m) { map_.insert(m.map_); }
 
   template<typename Collection>
   size_t insert(const Collection& vals) { map_.insert(vals); }
 
-  size_t insert(const IntMultiSet& set) {
-    size_t n = 0;
-    for (Key key : set.keys()) {
-      for (const T& val : set.values(key)) {
-        n += insert(val);
-      }
-    }
-    return n;
-  }
+  void erase(const T& val) { map_.erase(key_(val), val); }
 
   bool contains(const T& val) const { return map_.contains(key_(val), val); }
 
diff --git a/src/limbo/internal/iter.h b/src/limbo/internal/iter.h
index c3e1e1887379336354be227b00f506838cc708f3..c773c26540a404da92a045af85595caea2c4cc84 100644
--- a/src/limbo/internal/iter.h
+++ b/src/limbo/internal/iter.h
@@ -454,19 +454,17 @@ class filter_iterator {
   static_assert(std::is_convertible<typename InputIt::iterator_category, std::input_iterator_tag>::value,
                 "InputIt has wrong iterator category");
 
-  template<typename It = InputIt>
-  typename internal::if_arg<UnaryPredicate, It>::type Skip() {
-    while (iter_ != end_ && !pred_(*iter_)) {
+  void Skip() {
+    while (iter_ != end_ && !call()) {
       ++iter_;
     }
   }
 
   template<typename It = InputIt>
-  typename internal::if_arg<UnaryPredicate, value_type>::type Skip() {
-    while (iter_ != end_ && !pred_(*iter_)) {
-      ++iter_;
-    }
-  }
+  typename internal::if_arg<UnaryPredicate, value_type, bool>::type call() { return pred_(*iter_); }
+
+  template<typename It = InputIt>
+  typename internal::if_arg<UnaryPredicate, It, bool>::type call() { return pred_(iter_); }
 
   InputIt iter_;
   InputIt end_;
diff --git a/src/limbo/kb.h b/src/limbo/kb.h
index 070b2f48311bc343aaa45f96eef09e0268a9ae27..9e99e70e9f39f218c51b95e94706c3f9429a8569 100644
--- a/src/limbo/kb.h
+++ b/src/limbo/kb.h
@@ -136,9 +136,7 @@ class KnowledgeBase {
       assert(spheres_.size() == 1);
       assert(n_processed_beliefs_ == 0);
       for (Solver& sphere : spheres_) {
-        for (const Clause& c : knowledge_) {
-          sphere.AddClause(c);
-        }
+        sphere.grounder().AddClauses(knowledge_.begin() + n_processed_knowledge_, knowledge_.end());
       }
     } else {
       spheres_.clear();
@@ -149,15 +147,13 @@ class KnowledgeBase {
       do {
         last_n_done = n_done;
         Solver sphere(sf_, tf_);
-        for (const Clause& c : knowledge_) {
-          sphere.AddClause(c);
-        }
-        for (size_t i = 0; i < beliefs_.size(); ++i) {
-          const Conditional& c = beliefs_[i];
-          if (!done[i]) {
-            sphere.AddClause(c.not_ante_or_conse);
-          }
-        }
+        auto is = internal::filter_range(internal::int_iterator<size_t>(0),
+                                         internal::int_iterator<size_t>(beliefs_.size()),
+                                         [this, &done](size_t i) { return !done[i]; });
+        auto bs = internal::transform_range(is.begin(), is.end(),
+                                            [this](size_t i) -> const Clause& { return beliefs_[i].not_ante_or_conse; });
+        auto cs = internal::join_ranges(knowledge_.cbegin(), knowledge_.cend(), bs.begin(), bs.end());
+        sphere.grounder().AddClauses(cs.begin(), cs.end());
         bool next_is_plausibility_consistent = true;
         for (size_t i = 0; i < beliefs_.size(); ++i) {
           const Conditional& c = beliefs_[i];
@@ -256,12 +252,17 @@ class KnowledgeBase {
   }
 
   Formula::Ref ResEntails(sphere_index p, belief_level k, const Formula& phi) {
-    // If phi is just a literal (t = n) or (t = x) for primitive t, we can use Solver::Determines to speed things up.
+    // If phi is just a literal (t = n) or (t = x) for primitive t, we can
+    // use Solver::Determines to speed things up.
     if (phi.type() == Formula::kAtomic) {
       const Clause& c = phi.as_atomic().arg();
       if (c.unit()) {
         Literal a = c.first();
-        if (a.lhs().primitive() && a.pos()) {
+        // Currently we enable this only for (t = x) and not for (t = n), for
+        // the latter introduces a new temporary variable which in turn leads
+        // to additional names for grounding.
+        // TODO Make Grounder::PrepareForQuery() more efficient for (t = n).
+        if (a.lhs().primitive() && a.pos() && a.rhs().variable()) {
           internal::Maybe<Term> r = spheres_[p].Determines(k, a.lhs());
           if (a.rhs().name()) {
             return bool_to_formula(r && (r.val.null() || r.val == a.rhs()));
diff --git a/src/limbo/setup.h b/src/limbo/setup.h
index e1a9ef278b597f0f801a893743f1d5b8b38e3325..fa722e3fd0bb5471af8ce7a29808d34bc5ee3900 100644
--- a/src/limbo/setup.h
+++ b/src/limbo/setup.h
@@ -139,6 +139,8 @@ class Setup {
       }
     }
 
+    void Immortalize() { setup_ = nullptr; }
+
     Setup& setup() { return *setup_; }
     const Setup& setup() const { return *setup_; }
 
@@ -164,6 +166,8 @@ class Setup {
     friend Setup;
 
     struct Data {
+      Data() = default;
+      Data(bool ec, size_t nc, size_t nu) : empty_clause(ec), n_clauses(nc), n_units(nu) {}
       bool empty_clause = false;
       size_t n_clauses = 0;
       size_t n_units = 0;
@@ -172,7 +176,7 @@ class Setup {
 #endif
     };
 
-    explicit ShallowCopy(Setup* s) : setup_(s), data_({s->empty_clause_, s->clauses_.size(), s->units_.size()}) {
+    explicit ShallowCopy(Setup* s) : setup_(s), data_(Data(s->empty_clause_, s->clauses_.size(), s->units_.size())) {
       assert(data_.empty_clause + data_.n_clauses + data_.n_units == 0 || ++setup_->saved_ > 0);
 #ifndef NDEBUG
       data_.saved = s->saved_;
diff --git a/src/limbo/solver.h b/src/limbo/solver.h
index 30d5f5a630eee046f6627448210669ac98ee9b91..f20a453e16e6f35b1be9613e548ce8bb8a33737b 100644
--- a/src/limbo/solver.h
+++ b/src/limbo/solver.h
@@ -52,8 +52,6 @@ class Solver {
   Solver(Solver&&) = default;
   Solver& operator=(Solver&&) = default;
 
-  Setup::Result AddClause(const Clause& c) { return grounder_.AddClause(c); }
-
   Grounder& grounder() { return grounder_; }
   const Grounder& grounder() const { return grounder_; }