diff --git a/CMakeLists.txt b/CMakeLists.txt
index 76c16ae8c7273ce1a11fd686af331f07bad3cb27..2e034fb85ef087c1bac88b42f75a87109282284c 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,8 +1,8 @@
 # CMakeLists files in this project can
-# refer to the root source directory of the project as ${lela_SOURCE_DIR} and
-# to the root binary directory of the project as ${lela_BINARY_DIR}.
+# refer to the root source directory of the project as ${limbo_SOURCE_DIR} and
+# to the root binary directory of the project as ${limbo_BINARY_DIR}.
 cmake_minimum_required (VERSION 2.8.11)
-project (lela)
+project (limbo)
 
 include (CTest)
 
@@ -45,9 +45,6 @@ endif ()
 
 add_subdirectory (src)
 
-#add_subdirectory (eclipse-clp)
-#add_subdirectory (bats)
-
 add_subdirectory (tests)
 add_subdirectory (examples)
 
diff --git a/README.md b/README.md
index bde5a1437b088005c16558866d64825004e415ab..c54a2d413d440dbf9ebb8b6655b96dc469f93af8 100644
--- a/README.md
+++ b/README.md
@@ -1,26 +1,28 @@
-# Limited Epistemic Logic in Action
+# A Reasoning System for First-Order Limited Belief
 
-LELA (**L**imited **E**pistemic **L**ogic in **A**ction) is a C++ library for
-*decidable reasoning in first-order knowledge bases* based on the theory of
-*limited belief* from [1,2,3,4]. [Here are some web
-demos](http://www.cse.unsw.edu.au/~cschwering/demo/).
+Limbo is a *reasoning system for a first-order logic of **lim**ited
+**b**elief*. Limited belief allows for decidable reasoning in first-order
+knowledge bases, and in the propositional case it is even tractable. See
+[\[1,2,3,4\]](#references) for details on the theory, or click
+[here](http://www.cse.unsw.edu.au/~cschwering/limbo/) to see some web demos.
 
 ## Features
 
-The library provides a logical language to encode and reason about knowledge
-and belief.
+Limbo provides a logical language to represent and reason about (possibly
+incomplete) knowledge and belief.
 
-The logical language features functions of different sorts, standard names that
-designate distinct objects, first-order variables and quantification, equality,
-and modal operators for knowledge and conditional belief. (Predicates are not
-built-in but can be simulated without overhead using boolean functions.)
+This logical language is a first-order modal dialect: it features functions and
+equality, standard names to designate distinct objects, first-order variables
+and quantification, sorts, and modal operators for knowledge and conditional
+belief. (Predicates are not built-in but can be simulated without overhead
+using boolean functions.)
 
 An agent's knowledge and beliefs are encoded in this language. This knowledge
 base is subject to a syntactic restriction: it must be in clausal form, and all
-variables must be universally quantified. (Existentially quantified variables
-in the knowledge base can be simulated through Skolemization.) For instance,
-assuming a birthday scenario and a gift box, we could say that we know the box
-contains a gift.
+variables must be universally quantified; however, as existentially quantified
+variables can be simulated through Skolemization, this is no effective
+restriction. An example knowledge base might assume a birthday scenario and
+stipulate that that a certain gift box is known to contain an (unknown) gift.
 
 Reasoning in such knowledge bases is done with queries expressed in this
 language. For example, we can say that we believe that something is in the box
@@ -44,22 +46,21 @@ For more theoretical background see the papers linked below.
 
 ## Examples
 
-* This [web demo](http://www.cse.unsw.edu.au/~cschwering/demo/tui/) allows to
+* This [web demo](http://www.cse.unsw.edu.au/~cschwering/limbo/tui/) allows to
   define and query a knowledge base through a simple text interface.
   You can also use it from the command line; the the code is
   [here](examples/tui/).
 * There's are
-  [Minesweeper](http://www.cse.unsw.edu.au/~cschwering/demo/minesweeper/) and
-  [Sudoku](http://www.cse.unsw.edu.au/~cschwering/demo/sudoku/) web demos. You
+  [Minesweeper](http://www.cse.unsw.edu.au/~cschwering/limbo/minesweeper/) and
+  [Sudoku](http://www.cse.unsw.edu.au/~cschwering/limbo/sudoku/) web demos. You
   can use them it from the command line as well; the the code is
   [here](examples/minesweeper/) and [here](examples/sudoku/).
-* The main part of the C++ API is [kb.h](src/lela/kb.h),
-  [formula.h](src/lela/formula.h), [clause.h](src/lela/clause.h),
-  [literal.h](src/lela/literal.h), [term.h](src/lela/term.h), in this
-  order.
-  To make creating formulas a little more convenient,
-  [format/cpp/syntax.h](src/lela/format/cpp/syntax.h) overloads some C++
-  operators.
+* The main part of the C++ API is [kb.h](src/limbo/kb.h),
+  [formula.h](src/limbo/formula.h), [clause.h](src/limbo/clause.h),
+  [literal.h](src/limbo/literal.h), [term.h](src/limbo/term.h), in this
+  order. Optional C++ operator overloadings are provided by
+  [format/cpp/syntax.h](src/limbo/format/cpp/syntax.h) to make creating
+  formulas a little more convenient.
 
 ## Future work
 
diff --git a/examples/minesweeper/CMakeLists.txt b/examples/minesweeper/CMakeLists.txt
index 72456fa1201153cdb3a93e54f67e84c8ac69b01b..e62b5962c79331dda1bbb5666a502eae66304bdd 100644
--- a/examples/minesweeper/CMakeLists.txt
+++ b/examples/minesweeper/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_executable (minesweeper minesweeper.cc)
-target_link_libraries (minesweeper LINK_PUBLIC lela)
+target_link_libraries (minesweeper LINK_PUBLIC limbo)
 
 set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DUSE_DETERMINES")
 #set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DEND_GAME_CLAUSES")
@@ -10,7 +10,7 @@ if (EMCC)
                 separate_arguments(FLAGS UNIX_COMMAND "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_RELEASE}")
                 add_custom_command (OUTPUT minesweeper-js.js minesweeper-js.js.mem
                         COMMAND ${EMCC} ${FLAGS} -I../../src minesweeper-js.cc -o minesweeper-js.js
-                                -s EXPORTED_FUNCTIONS=['_lela_init','_lela_play_turn']
+                                -s EXPORTED_FUNCTIONS=['_limbo_init','_limbo_play_turn']
                                 -s TOTAL_MEMORY=67108864
                         DEPENDS minesweeper-js.cc "*.h"
                         VERBATIM)
diff --git a/examples/minesweeper/agent.h b/examples/minesweeper/agent.h
index 6fd17ed062d7ac303bfc92a4d87a3d6331125778..dbea1d8155cd258ff233baed75af43d5adf671b8 100644
--- a/examples/minesweeper/agent.h
+++ b/examples/minesweeper/agent.h
@@ -45,7 +45,7 @@ class Agent {
           if (g_->opened(p) || g_->flagged(p)) {
             continue;
           }
-          const lela::internal::Maybe<bool> r = kb_->IsMine(p, k);
+          const limbo::internal::Maybe<bool> r = kb_->IsMine(p, k);
           if (r.yes) {
             if (r.val) {
               logger_.flagged(p, k);
diff --git a/examples/minesweeper/kb.h b/examples/minesweeper/kb.h
index e6ad7804e884cce3881265edf6f8abdb4d39da78..caa520f09d852cc97b43987e8aee1fcb30f05720 100644
--- a/examples/minesweeper/kb.h
+++ b/examples/minesweeper/kb.h
@@ -7,11 +7,11 @@
 #include <sstream>
 #include <vector>
 
-#include <lela/solver.h>
-#include <lela/internal/maybe.h>
-#include <lela/internal/iter.h>
-#include <lela/format/output.h>
-#include <lela/format/cpp/syntax.h>
+#include <limbo/solver.h>
+#include <limbo/internal/maybe.h>
+#include <limbo/internal/iter.h>
+#include <limbo/format/output.h>
+#include <limbo/format/cpp/syntax.h>
 
 #include "game.h"
 #include "timer.h"
@@ -61,75 +61,75 @@ class KnowledgeBase {
         F(ctx_.CreateName(Bool)),
 #endif
         MineF(ctx_.CreateFunction(Bool, 2)) {
-    lela::format::RegisterSort(Bool, "");
-    lela::format::RegisterSort(XPos, "");
-    lela::format::RegisterSort(YPos, "");
-    lela::format::RegisterSymbol(T.symbol(), "T");
+    limbo::format::RegisterSort(Bool, "");
+    limbo::format::RegisterSort(XPos, "");
+    limbo::format::RegisterSort(YPos, "");
+    limbo::format::RegisterSymbol(T.symbol(), "T");
 #ifdef USE_DETERMINES
-    lela::format::RegisterSymbol(F.symbol(), "F");
+    limbo::format::RegisterSymbol(F.symbol(), "F");
 #endif
-    lela::format::RegisterSymbol(MineF, "Mine");
+    limbo::format::RegisterSymbol(MineF, "Mine");
     X.resize(g_->width());
     for (size_t i = 0; i < g_->width(); ++i) {
       X[i] = ctx_.CreateName(XPos);
       std::stringstream ss;
       ss << "#X" << i;
-      lela::format::RegisterSymbol(X[i].symbol(), ss.str());
+      limbo::format::RegisterSymbol(X[i].symbol(), ss.str());
     }
     Y.resize(g_->height());
     for (size_t i = 0; i < g_->height(); ++i) {
       Y[i] = ctx_.CreateName(YPos);
       std::stringstream ss;
       ss << "#Y" << i;
-      lela::format::RegisterSymbol(Y[i].symbol(), ss.str());
+      limbo::format::RegisterSymbol(Y[i].symbol(), ss.str());
     }
     processed_.resize(g_->n_fields(), false);
   }
 
   size_t max_k() const { return max_k_; }
 
-  const lela::Solver& solver() const { return ctx_.solver(); }
-  const lela::Setup& setup() const { return solver().setup(); }
+  const limbo::Solver& solver() const { return ctx_.solver(); }
+  const limbo::Setup& setup() const { return solver().setup(); }
 
-  lela::internal::Maybe<bool> IsMine(Point p, int k) {
+  limbo::internal::Maybe<bool> IsMine(Point p, int k) {
     t_.start();
-    lela::internal::Maybe<bool> r = lela::internal::Nothing;
+    limbo::internal::Maybe<bool> r = limbo::internal::Nothing;
 #ifdef USE_DETERMINES
     // In this case we need a second name to represent falsity. The reason is
     // that without such a name, falsity is represented by "/= T", which is for
     // Determines() just means the term's value is not determined, whereas we'd
     // want it to be determined as false.
-    lela::internal::Maybe<lela::Term> is_mine = solver()->Determines(k, Mine(p), lela::Solver::kConsistencyGuarantee);
+    limbo::internal::Maybe<limbo::Term> is_mine = solver()->Determines(k, Mine(p), limbo::Solver::kConsistencyGuarantee);
     assert(!is_mine || is_mine.val == T || is_mine.val == F);
-    assert(solver()->Determines(k, Mine(p), lela::Solver::kNoConsistencyGuarantee) == is_mine);
-    assert(solver()->Entails(k, *lela::Formula::Factory::Atomic(lela::Clause{MineLit(true, p)}),
-                             lela::Solver::kConsistencyGuarantee) ==
+    assert(solver()->Determines(k, Mine(p), limbo::Solver::kNoConsistencyGuarantee) == is_mine);
+    assert(solver()->Entails(k, *limbo::Formula::Factory::Atomic(limbo::Clause{MineLit(true, p)}),
+                             limbo::Solver::kConsistencyGuarantee) ==
            (is_mine && is_mine.val == T));
-    assert(solver()->Entails(k, *lela::Formula::Factory::Atomic(lela::Clause{MineLit(true, p)}),
-                             lela::Solver::kConsistencyGuarantee) ==
-           solver()->Entails(k, *lela::Formula::Factory::Atomic(lela::Clause{MineLit(true, p)}),
-                             lela::Solver::kNoConsistencyGuarantee));
-    assert(solver()->Entails(k, *lela::Formula::Factory::Atomic(lela::Clause{MineLit(false, p)}),
-                             lela::Solver::kConsistencyGuarantee) ==
-           solver()->Entails(k, *lela::Formula::Factory::Atomic(lela::Clause{MineLit(false, p)}),
-                             lela::Solver::kNoConsistencyGuarantee));
-    assert(solver()->Entails(k, *lela::Formula::Factory::Atomic(lela::Clause{MineLit(false, p)}),
-                             lela::Solver::kConsistencyGuarantee) ==
+    assert(solver()->Entails(k, *limbo::Formula::Factory::Atomic(limbo::Clause{MineLit(true, p)}),
+                             limbo::Solver::kConsistencyGuarantee) ==
+           solver()->Entails(k, *limbo::Formula::Factory::Atomic(limbo::Clause{MineLit(true, p)}),
+                             limbo::Solver::kNoConsistencyGuarantee));
+    assert(solver()->Entails(k, *limbo::Formula::Factory::Atomic(limbo::Clause{MineLit(false, p)}),
+                             limbo::Solver::kConsistencyGuarantee) ==
+           solver()->Entails(k, *limbo::Formula::Factory::Atomic(limbo::Clause{MineLit(false, p)}),
+                             limbo::Solver::kNoConsistencyGuarantee));
+    assert(solver()->Entails(k, *limbo::Formula::Factory::Atomic(limbo::Clause{MineLit(false, p)}),
+                             limbo::Solver::kConsistencyGuarantee) ==
            (is_mine && is_mine.val == F));
     if (is_mine) {
       assert(!is_mine.val.null());
-      r = lela::internal::Just(is_mine.val == T);
+      r = limbo::internal::Just(is_mine.val == T);
       assert(g_->mine(p) == r.val);
     }
 #else
-    lela::Formula::Ref yes_mine = lela::Formula::Factory::Atomic(lela::Clause{MineLit(true, p)});
-    lela::Formula::Ref no_mine = lela::Formula::Factory::Atomic(lela::Clause{MineLit(false, p)});
-    if (solver()->Entails(k, *yes_mine, lela::Solver::kConsistencyGuarantee)) {
+    limbo::Formula::Ref yes_mine = limbo::Formula::Factory::Atomic(limbo::Clause{MineLit(true, p)});
+    limbo::Formula::Ref no_mine = limbo::Formula::Factory::Atomic(limbo::Clause{MineLit(false, p)});
+    if (solver()->Entails(k, *yes_mine, limbo::Solver::kConsistencyGuarantee)) {
       assert(g_->mine(p));
-      r = lela::internal::Just(true);
-    } else if (solver()->Entails(k, *no_mine, lela::Solver::kConsistencyGuarantee)) {
+      r = limbo::internal::Just(true);
+    } else if (solver()->Entails(k, *no_mine, limbo::Solver::kConsistencyGuarantee)) {
       assert(!g_->mine(p));
-      r = lela::internal::Just(false);
+      r = limbo::internal::Just(false);
     }
 #endif
     t_.stop();
@@ -157,22 +157,22 @@ class KnowledgeBase {
   void ResetTimer() { t_.reset(); }
 
  private:
-  lela::Term Mine(Point p) const {
+  limbo::Term Mine(Point p) const {
     return MineF(X[p.x], Y[p.y]);
   }
 
-  lela::Literal MineLit(bool is, Point p) const {
-    lela::Term t = Mine(p);
+  limbo::Literal MineLit(bool is, Point p) const {
+    limbo::Term t = Mine(p);
 #ifdef USE_DETERMINES
-    return lela::Literal::Eq(t, is ? T : F);
+    return limbo::Literal::Eq(t, is ? T : F);
 #else
-    return is ? lela::Literal::Eq(t, T) : lela::Literal::Neq(t, T);
+    return is ? limbo::Literal::Eq(t, T) : limbo::Literal::Neq(t, T);
 #endif
   }
 
-  lela::Clause MineClause(bool sign, const std::vector<Point> ns) const {
-    auto r = lela::internal::transform_range(ns.begin(), ns.end(), [this, sign](Point p) { return MineLit(sign, p); });
-    return lela::Clause(r.begin(), r.end());
+  limbo::Clause MineClause(bool sign, const std::vector<Point> ns) const {
+    auto r = limbo::internal::transform_range(ns.begin(), ns.end(), [this, sign](Point p) { return MineLit(sign, p); });
+    return limbo::Clause(r.begin(), r.end());
   }
 
   bool Update(Point p) {
@@ -183,11 +183,11 @@ class KnowledgeBase {
         return false;
       }
       case Game::FLAGGED: {
-        AddClause(lela::Clause{MineLit(true, p)});
+        AddClause(limbo::Clause{MineLit(true, p)});
         return true;
       }
       case Game::HIT_MINE: {
-        AddClause(lela::Clause{MineLit(true, p)});
+        AddClause(limbo::Clause{MineLit(true, p)});
         return true;
       }
       default: {
@@ -199,7 +199,7 @@ class KnowledgeBase {
         for (const std::vector<Point>& ps : util::Subsets(ns, m + 1)) {
           AddClause(MineClause(false, ps));
         }
-        AddClause(lela::Clause{MineLit(false, p)});
+        AddClause(limbo::Clause{MineLit(false, p)});
         return true;
       }
     }
@@ -221,12 +221,12 @@ class KnowledgeBase {
     }
   }
 
-  void AddClause(const lela::Clause& c) {
+  void AddClause(const limbo::Clause& c) {
 #ifdef USE_DETERMINES
-    for (lela::Literal a : c) {
-      lela::Term t = a.lhs();
+    for (limbo::Literal a : c) {
+      limbo::Term t = a.lhs();
       if (closure_added_.find(t) == closure_added_.end()) {
-        solver()->AddClause(lela::Clause{lela::Literal::Eq(t, T), lela::Literal::Eq(t, F)});
+        solver()->AddClause(limbo::Clause{limbo::Literal::Eq(t, T), limbo::Literal::Eq(t, F)});
         closure_added_.insert(t);
       }
     }
@@ -234,26 +234,26 @@ class KnowledgeBase {
     solver()->AddClause(c);
   }
 
-  lela::Solver* solver() { return ctx_.solver(); }
+  limbo::Solver* solver() { return ctx_.solver(); }
 
   const Game* g_;
   size_t max_k_;
 
-  lela::format::cpp::Context ctx_;
+  limbo::format::cpp::Context ctx_;
 
-  lela::Symbol::Sort Bool;
-  lela::Symbol::Sort XPos;
-  lela::Symbol::Sort YPos;
-  lela::format::cpp::HiTerm T;               // name for positive truth value
+  limbo::Symbol::Sort Bool;
+  limbo::Symbol::Sort XPos;
+  limbo::Symbol::Sort YPos;
+  limbo::format::cpp::HiTerm T;               // name for positive truth value
 #ifdef USE_DETERMINES
-  lela::format::cpp::HiTerm F;               // name for negative truth value
+  limbo::format::cpp::HiTerm F;               // name for negative truth value
 #endif
-  std::vector<lela::format::cpp::HiTerm> X;  // names for X positions
-  std::vector<lela::format::cpp::HiTerm> Y;  // names for Y positions
-  lela::format::cpp::HiSymbol MineF;
+  std::vector<limbo::format::cpp::HiTerm> X;  // names for X positions
+  std::vector<limbo::format::cpp::HiTerm> Y;  // names for Y positions
+  limbo::format::cpp::HiSymbol MineF;
 
 #ifdef USE_DETERMINES
-  std::unordered_set<lela::Term> closure_added_;
+  std::unordered_set<limbo::Term> closure_added_;
 #endif
 
   std::vector<bool> processed_;
diff --git a/examples/minesweeper/minesweeper-js.cc b/examples/minesweeper/minesweeper-js.cc
index 5b207b5bc7a80378b873583e8cfd0651561c755e..ba4f1a349582780c0fbecea194f84a6f7a11a91b 100644
--- a/examples/minesweeper/minesweeper-js.cc
+++ b/examples/minesweeper/minesweeper-js.cc
@@ -35,8 +35,8 @@ static Timer* timer_overall = nullptr;
 static std::vector<int>* split_counts = nullptr;
 
 void Finalize() {
-  lela::Symbol::Factory::Reset();
-  lela::Term::Factory::Reset();
+  limbo::Symbol::Factory::Reset();
+  limbo::Term::Factory::Reset();
   if (game)
     delete game;
   if (kb)
@@ -91,11 +91,11 @@ bool PlayTurn() {
 
 }  // namespace game
 
-extern "C" void lela_init(size_t width, size_t height, size_t n_mines, size_t seed, int max_k) {
+extern "C" void limbo_init(size_t width, size_t height, size_t n_mines, size_t seed, int max_k) {
   game::Init(width, height, n_mines, seed, max_k);
 }
 
-extern "C" int lela_play_turn() {
+extern "C" int limbo_play_turn() {
   return game::PlayTurn() ? 1 : 0;
 }
 
diff --git a/examples/minesweeper/minesweeper-js.html b/examples/minesweeper/minesweeper-js.html
index 8567eec77f6a9903778150bbec9fb270c5874af4..85672c96e757559785de2b5d347c7ad63c3939dc 100644
--- a/examples/minesweeper/minesweeper-js.html
+++ b/examples/minesweeper/minesweeper-js.html
@@ -85,6 +85,11 @@ For further demos and details on the reasoner, <a href="../">click here</a>.
 </form>
 
 <script>
+function preloadImg(image) {
+    var img = new Image();
+    img.src = image;
+}
+
 $(document).ready(function() {
     $('#config-small').click(function() { setConfig(8, 8, 10); return false; }).click();
     $('#config-medium').click(function() { setConfig(16, 16, 40); return false; });
@@ -97,6 +102,8 @@ $(document).ready(function() {
     $('#different-seed').click(function() { $('#seed').val(parseInt($('#seed').val()) + 1); scrollToShow('#play-button'); return false; });
     $('#different-field-size').click(function() { scrollToShow('#config-small'); return false; });
     $('#play-again-msg').hide();
+    preloadImg('flag.svg');
+    preloadImg('mine.svg');
     initDisplay();
 });
 
@@ -125,7 +132,7 @@ function play() {
     resetGameVariables();
     timerOverall = 0;
     scrollToShow('#output');
-    Module.ccall('lela_init', 'void', ['number', 'number', 'number', 'number', 'number'], [width, height, n_mines, seed, max_k]);
+    Module.ccall('limbo_init', 'void', ['number', 'number', 'number', 'number', 'number'], [width, height, n_mines, seed, max_k]);
     playTurn();
 }
 
@@ -133,7 +140,7 @@ function playTurn() {
     setTimeout(function() {
         var t0 = performance.now();
         timerTurn = t0;
-        var gameOver = Module.ccall('lela_play_turn', 'number', [], []);
+        var gameOver = Module.ccall('limbo_play_turn', 'number', [], []);
         var t1 = performance.now();
         timerOverall += t1 - t0;
         if (!gameOver) {
diff --git a/examples/minesweeper/minesweeper.cc b/examples/minesweeper/minesweeper.cc
index 74c47483bec35d8cb4d5e05b963a5c98bab024eb..67d12153dceb99a4cf60fddc066cbc6007301249 100644
--- a/examples/minesweeper/minesweeper.cc
+++ b/examples/minesweeper/minesweeper.cc
@@ -31,7 +31,7 @@ struct Logger {
     if (first_ && k == -1) {
       std::cout << ", chosen at random.";
     } else if (k == -1) {
-      using lela::format::operator<<;
+      using limbo::format::operator<<;
       std::cout << ", which is just a guess.";
     } else {
       std::cout << ", found at split level " << k << ".";
diff --git a/examples/minesweeper/printer.h b/examples/minesweeper/printer.h
index d6f47a8788423ac881bda3ec4e17265239e4ab73..5bf8415439bb375b830fdb558e0bb325ae5df544 100644
--- a/examples/minesweeper/printer.h
+++ b/examples/minesweeper/printer.h
@@ -8,7 +8,7 @@
 #include <iomanip>
 #include <string>
 
-#include <lela/format/output.h>
+#include <limbo/format/output.h>
 
 #include "game.h"
 #include "kb.h"
@@ -183,7 +183,7 @@ class KnowledgeBasePrinter : public Printer {
     switch (g.state(p)) {
       case Game::UNEXPLORED: {
         if (g.frontier(p)) {
-          const lela::internal::Maybe<bool> r = kb_->IsMine(p, kb_->max_k());
+          const limbo::internal::Maybe<bool> r = kb_->IsMine(p, kb_->max_k());
           if (r.yes) {
             assert(g.mine(p) == r.val);
             if (r.val) {
diff --git a/examples/sudoku/CMakeLists.txt b/examples/sudoku/CMakeLists.txt
index 60f8d6655f8007d98c4199de79571d6a80207bc1..7500099b75091d6636c7d9cb70f4b459230b33df 100644
--- a/examples/sudoku/CMakeLists.txt
+++ b/examples/sudoku/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_executable (sudoku sudoku.cc)
-target_link_libraries (sudoku LINK_PUBLIC lela)
+target_link_libraries (sudoku LINK_PUBLIC limbo)
 
 
 # add_test (NAME sudokus COMMAND ./test-sudokus.sh)
@@ -11,7 +11,7 @@ if (EMCC)
                 separate_arguments(FLAGS UNIX_COMMAND "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_RELEASE}")
                 add_custom_command (OUTPUT sudoku-js.js sudoku-js.js.mem
                     COMMAND ${EMCC} ${FLAGS} -I../../src sudoku-js.cc -o sudoku-js.js
-                                -s EXPORTED_FUNCTIONS=['_lela_init','_lela_play_turn']
+                                -s EXPORTED_FUNCTIONS=['_limbo_init','_limbo_play_turn']
                                 -s TOTAL_MEMORY=67108864
                         DEPENDS sudoku-js.cc "*.h"
                         VERBATIM)
diff --git a/examples/sudoku/agent.h b/examples/sudoku/agent.h
index 7beb4075b6303c30acce60d48b15f46ccdfbcc41..66c63e654d6e20aeda397cd862d7d54781fc6eb2 100644
--- a/examples/sudoku/agent.h
+++ b/examples/sudoku/agent.h
@@ -6,7 +6,7 @@
 
 #include <iostream>
 
-#include <lela/internal/maybe.h>
+#include <limbo/internal/maybe.h>
 
 #include "game.h"
 #include "kb.h"
@@ -22,31 +22,31 @@ class Agent {
   };
 
   virtual ~Agent() {}
-  virtual lela::internal::Maybe<Result> Explore() = 0;
+  virtual limbo::internal::Maybe<Result> Explore() = 0;
 };
 
 class KnowledgeBaseAgent : public Agent {
  public:
   KnowledgeBaseAgent(Game* g, KnowledgeBase* kb) : g_(g), kb_(kb) {}
 
-  lela::internal::Maybe<Result> Explore() override {
+  limbo::internal::Maybe<Result> Explore() override {
     for (int k = 0; k <= kb_->max_k(); ++k) {
       for (std::size_t x = 1; x <= 9; ++x) {
         for (std::size_t y = 1; y <= 9; ++y) {
           Point p(x, y);
           if (g_->get(p) == 0) {
-            const lela::internal::Maybe<int> r = kb_->Val(p, k);
+            const limbo::internal::Maybe<int> r = kb_->Val(p, k);
             if (r) {
               const int n = r.val;
               kb_->Add(p, n);
               g_->set(p, n);
-              return lela::internal::Just(Result(p, n, k));
+              return limbo::internal::Just(Result(p, n, k));
             }
           }
         }
       }
     }
-    return lela::internal::Nothing;
+    return limbo::internal::Nothing;
   }
 
  private:
diff --git a/examples/sudoku/kb.h b/examples/sudoku/kb.h
index 7aabbf417378538c10d832f4bee905b52bf896e0..211dfc51fe9968ca3bb12a10a635b5c9c9aa6c47 100644
--- a/examples/sudoku/kb.h
+++ b/examples/sudoku/kb.h
@@ -7,11 +7,11 @@
 #include <sstream>
 #include <vector>
 
-#include <lela/solver.h>
-#include <lela/internal/maybe.h>
-#include <lela/internal/iter.h>
-#include <lela/format/output.h>
-#include <lela/format/cpp/syntax.h>
+#include <limbo/solver.h>
+#include <limbo/internal/maybe.h>
+#include <limbo/internal/iter.h>
+#include <limbo/format/output.h>
+#include <limbo/format/cpp/syntax.h>
 
 #include "game.h"
 #include "timer.h"
@@ -22,14 +22,14 @@ class KnowledgeBase {
       : max_k_(max_k),
         VAL_(ctx_.CreateSort()),
         val_(ctx_.CreateFunction(VAL_, 2)) {
-    lela::format::RegisterSort(VAL_, "");
-    lela::format::RegisterSymbol(val_, "val");
-    using namespace lela::format::cpp;
+    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_));
       std::stringstream ss;
       ss << i;
-      lela::format::RegisterSymbol(vals_.back().symbol(), ss.str());
+      limbo::format::RegisterSymbol(vals_.back().symbol(), ss.str());
     }
     for (std::size_t x = 1; x <= 9; ++x) {
       for (std::size_t y = 1; y <= 9; ++y) {
@@ -66,11 +66,11 @@ class KnowledgeBase {
     }
     for (std::size_t x = 1; x <= 9; ++x) {
       for (std::size_t y = 1; y <= 9; ++y) {
-        std::vector<lela::Literal> lits;
+        std::vector<limbo::Literal> lits;
         for (std::size_t i = 1; i <= 9; ++i) {
-          lits.push_back(lela::Literal::Eq(val(x, y), n(i)));
+          lits.push_back(limbo::Literal::Eq(val(x, y), n(i)));
         }
-        ctx_.AddClause(lela::Clause(lits.begin(), lits.end()));
+        ctx_.AddClause(limbo::Clause(lits.begin(), lits.end()));
       }
     }
     for (std::size_t x = 1; x <= 9; ++x) {
@@ -85,55 +85,55 @@ class KnowledgeBase {
 
   int max_k() const { return max_k_; }
 
-  lela::Solver* solver() { return ctx_.solver(); }
-  const lela::Solver& solver() const { return ctx_.solver(); }
-  const lela::Setup& setup() const { return solver().setup(); }
+  limbo::Solver* solver() { return ctx_.solver(); }
+  const limbo::Solver& solver() const { return ctx_.solver(); }
+  const limbo::Setup& setup() const { return solver().setup(); }
 
   void Add(Point p, int i) {
     ctx_.AddClause(val(p) == n(i));
   }
 
-  lela::internal::Maybe<int> Val(Point p, int k) {
+  limbo::internal::Maybe<int> Val(Point p, int k) {
     t_.start();
-    const lela::internal::Maybe<lela::Term> r = solver()->Determines(k, val(p), lela::Solver::kConsistencyGuarantee);
-    assert(std::all_of(lela::internal::int_iterator<size_t>(1), lela::internal::int_iterator<size_t>(9),
-           [&](size_t i) { return solver()->Entails(k, val(p) == n(i), lela::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)); }));
     if (r) {
       assert(!r.val.null());
       for (std::size_t i = 1; i <= 9; ++i) {
         if (r.val.null() || r.val == n(i)) {
-          return lela::internal::Just(i);
+          return limbo::internal::Just(i);
         }
       }
     }
     t_.stop();
-    return lela::internal::Nothing;
+    return limbo::internal::Nothing;
   }
 
   const Timer& timer() const { return t_; }
   void ResetTimer() { t_.reset(); }
 
  private:
-  lela::format::cpp::HiTerm n(std::size_t n) const {
+  limbo::format::cpp::HiTerm n(std::size_t n) const {
     return vals_[n-1];
   }
 
-  lela::format::cpp::HiTerm val(Point p) const {
+  limbo::format::cpp::HiTerm val(Point p) const {
     return val(p.x, p.y);
   }
 
-  lela::format::cpp::HiTerm val(std::size_t x, std::size_t y) const {
+  limbo::format::cpp::HiTerm val(std::size_t x, std::size_t y) const {
     return val_(vals_[x-1], vals_[y-1]);
   }
 
   int max_k_;
 
-  lela::format::cpp::Context ctx_;
+  limbo::format::cpp::Context ctx_;
 
-  lela::Symbol::Sort VAL_;
-  lela::format::cpp::HiSymbol val_;
-  std::vector<lela::format::cpp::HiTerm> vals_;
+  limbo::Symbol::Sort VAL_;
+  limbo::format::cpp::HiSymbol val_;
+  std::vector<limbo::format::cpp::HiTerm> vals_;
 
   Timer t_;
 };
diff --git a/examples/sudoku/printer.h b/examples/sudoku/printer.h
index ac92387a43e9d2c629c434f15c048b7f1782f2b9..e20ff5a9ac9e96a16b7e0457b0f953107b2fe1aa 100644
--- a/examples/sudoku/printer.h
+++ b/examples/sudoku/printer.h
@@ -9,7 +9,7 @@
 #include <string>
 #include <sstream>
 
-#include <lela/format/output.h>
+#include <limbo/format/output.h>
 
 #include "game.h"
 #include "kb.h"
diff --git a/examples/sudoku/sudoku-js.cc b/examples/sudoku/sudoku-js.cc
index 25ac4392ea7a6d8319b7de9a0c34759edd83e68d..33c2c1eec5e281c9b63cc69483279cc768924fdc 100644
--- a/examples/sudoku/sudoku-js.cc
+++ b/examples/sudoku/sudoku-js.cc
@@ -84,8 +84,8 @@ static SimplePrinter* printer = nullptr;
 static std::vector<int>* split_counts = nullptr;
 
 void Finalize() {
-  lela::Symbol::Factory::Reset();
-  lela::Term::Factory::Reset();
+  limbo::Symbol::Factory::Reset();
+  limbo::Term::Factory::Reset();
   if (agent)
     delete agent;
   if (kb)
@@ -120,7 +120,7 @@ bool PlayTurn() {
   Timer timer_turn;
   timer_turn.start();
   timer_overall->start();
-  const lela::internal::Maybe<Agent::Result> r = agent->Explore();
+  const limbo::internal::Maybe<Agent::Result> r = agent->Explore();
   timer_overall->stop();
   timer_turn.stop();
   if (r) {
@@ -159,14 +159,14 @@ bool PlayTurn() {
 
 }  // namespace game
 
-extern "C" void lela_init(const char* cfg, int max_k) {
+extern "C" void limbo_init(const char* cfg, int max_k) {
   if (!logging::redirector_) {
     logging::redirector_ = new logging::StreamRedirector<logging::JsLogger>(&std::cout);
   }
   game::Init(cfg, max_k);
 }
 
-extern "C" int lela_play_turn() {
+extern "C" int limbo_play_turn() {
   return game::PlayTurn() ? 1 : 0;
 }
 
diff --git a/examples/sudoku/sudoku-js.html b/examples/sudoku/sudoku-js.html
index 1ae852f8106c26c687ca87e5e0b361b6f598309c..244755c3f0ae0f199bf8b17c1d32550f51da5798 100644
--- a/examples/sudoku/sudoku-js.html
+++ b/examples/sudoku/sudoku-js.html
@@ -141,7 +141,7 @@ function initGame() {
     if (max_k == null) {
         max_k = 2;
     }
-    Module.ccall('lela_init', 'void', ['string', 'number'], [config, max_k]);
+    Module.ccall('limbo_init', 'void', ['string', 'number'], [config, max_k]);
 }
 
 function play() {
@@ -153,7 +153,7 @@ function play() {
 
 function playTurn() {
     setTimeout(function() {
-        var game_over = Module.ccall('lela_play_turn', 'number', [], []);
+        var game_over = Module.ccall('limbo_play_turn', 'number', [], []);
         if (!game_over) {
             playTurn();
         } else {
diff --git a/examples/sudoku/sudoku.cc b/examples/sudoku/sudoku.cc
index 8e2724b9a5c16e588167e18bd3d0f972bedb0091..8a5a43c18803878b2eed43e0726bbce728e456a1 100644
--- a/examples/sudoku/sudoku.cc
+++ b/examples/sudoku/sudoku.cc
@@ -9,7 +9,7 @@
 #include <iostream>
 #include <string>
 
-#include <lela/internal/maybe.h>
+#include <limbo/internal/maybe.h>
 
 #include "agent.h"
 #include "game.h"
@@ -25,7 +25,7 @@ inline bool Play(const std::string& cfg, int max_k, const Colors& colors, std::o
   SimplePrinter printer(&colors, os);
   std::vector<int> split_counts;
   split_counts.resize(max_k + 1);
-  lela::internal::Maybe<Agent::Result> r;
+  limbo::internal::Maybe<Agent::Result> r;
   *os << "Initial Sudoku:" << std::endl;
   *os << std::endl;
   printer.Print(g);
diff --git a/examples/sudoku/test-and-eval-sudokus.sh b/examples/sudoku/test-and-eval-sudokus.sh
new file mode 100755
index 0000000000000000000000000000000000000000..8a2e8f922d3a9ed2b5116f393217ab529a7ce9d2
--- /dev/null
+++ b/examples/sudoku/test-and-eval-sudokus.sh
@@ -0,0 +1,9 @@
+F=$1
+
+for sudoku in $(cat $F)
+do
+    echo -n "Preset cells: "
+    echo -n $sudoku | sed 's/\.//g' | wc -c
+    ./sudoku $sudoku 2 | grep Solution
+done
+
diff --git a/examples/tui/CMakeLists.txt b/examples/tui/CMakeLists.txt
index b8e3346c2fcfb94b190561be7d1927ed7803ee2f..6d136c18c2cb4077c492f8fbc2025ee0ddb16523 100644
--- a/examples/tui/CMakeLists.txt
+++ b/examples/tui/CMakeLists.txt
@@ -1,8 +1,8 @@
 add_executable (tui tui.cc linenoise/linenoise.c) 
-target_link_libraries (tui LINK_PUBLIC lela)
+target_link_libraries (tui LINK_PUBLIC limbo)
 
 
-file (GLOB tests RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}" "*.lela")
+file (GLOB tests RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}" "*.limbo")
 foreach (test ${tests})
     add_test (NAME ${test} COMMAND ./tui ${test})
 endforeach ()
@@ -14,7 +14,7 @@ if (EMCC)
                 separate_arguments(FLAGS UNIX_COMMAND "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_RELEASE}")
                 add_custom_command (OUTPUT tui-js.js tui-js.js.mem
                         COMMAND ${EMCC} ${FLAGS} -I../../src tui-js.cc -o tui-js.js
-				-s EXPORTED_FUNCTIONS=['_lela_init','_lela_parse','_lela_free']
+				-s EXPORTED_FUNCTIONS=['_limbo_init','_limbo_parse','_limbo_free']
                                 -s TOTAL_MEMORY=16777216
                         DEPENDS tui-js.cc "*.h"
                         VERBATIM)
diff --git a/examples/tui/battleship.h b/examples/tui/battleship.h
index 2a0c19783709639b6ed23197596c7b0f11e6163f..070d4612ce2a2ba7cfb0a26baf1d793bbcd151e7 100644
--- a/examples/tui/battleship.h
+++ b/examples/tui/battleship.h
@@ -15,9 +15,9 @@
 #include <set>
 #include <vector>
 
-#include <lela/term.h>
-#include <lela/clause.h>
-#include <lela/literal.h>
+#include <limbo/term.h>
+#include <limbo/clause.h>
+#include <limbo/literal.h>
 
 struct Point {
   Point() {}
@@ -225,7 +225,7 @@ std::ostream& operator<<(std::ostream& os, const BattleshipGame& g) {
 
 struct BattleshipCallbacks {
   template<typename T>
-  bool operator()(T* ctx, const std::string& proc, const std::vector<lela::Term>& args) {
+  bool operator()(T* ctx, const std::string& proc, const std::vector<limbo::Term>& args) {
     if (proc == "bs_init" && !bs_) {
       if (args.size() == 4) {
         bs_ = std::make_shared<BattleshipGame>(1, 4, std::vector<size_t>{0, 0, 1});
@@ -254,16 +254,16 @@ struct BattleshipCallbacks {
  private:
   template<typename T>
   void Fire(T* ctx, Point p) {
-    const lela::Term t = Lookup(p);
+    const limbo::Term t = Lookup(p);
     const bool is_water = !bs_->Fire(p);
-    const lela::Term Water = ctx->CreateTerm(ctx->LookupFunction("water"), {t});
-    const lela::Term Fired = ctx->CreateTerm(ctx->LookupFunction("fired"), {t});
-    const lela::Term True = ctx->LookupName("T");
-    ctx->kb()->Add(lela::Clause{is_water ? lela::Literal::Eq(Water, True) : lela::Literal::Neq(Water, True)});
-    ctx->kb()->Add(lela::Clause{lela::Literal::Eq(Fired, True)});
+    const limbo::Term Water = ctx->CreateTerm(ctx->LookupFunction("water"), {t});
+    const limbo::Term Fired = ctx->CreateTerm(ctx->LookupFunction("fired"), {t});
+    const limbo::Term True = ctx->LookupName("T");
+    ctx->kb()->Add(limbo::Clause{is_water ? limbo::Literal::Eq(Water, True) : limbo::Literal::Neq(Water, True)});
+    ctx->kb()->Add(limbo::Clause{limbo::Literal::Eq(Fired, True)});
   }
 
-  Point Lookup(lela::Term t) {
+  Point Lookup(limbo::Term t) {
     for (size_t i = 0; i < ps_.size(); ++i) {
       if (ps_[i] == t) {
         return bs_->to_point(i);
@@ -272,12 +272,12 @@ struct BattleshipCallbacks {
     throw;
   }
 
-  lela::Term Lookup(Point p) {
+  limbo::Term Lookup(Point p) {
     return ps_[bs_->to_index(p)];
   }
 
   std::shared_ptr<BattleshipGame> bs_;
-  std::vector<lela::Term> ps_;
+  std::vector<limbo::Term> ps_;
 };
 
 #endif  // EXAMPLES_TEXTINTERFACE_BATTLESHIP_H_
diff --git a/examples/tui/example-battleship-1x4.lela b/examples/tui/example-battleship-1x4.limbo
similarity index 100%
rename from examples/tui/example-battleship-1x4.lela
rename to examples/tui/example-battleship-1x4.limbo
diff --git a/examples/tui/example-battleship-4x4.lela b/examples/tui/example-battleship-4x4.limbo
similarity index 100%
rename from examples/tui/example-battleship-4x4.lela
rename to examples/tui/example-battleship-4x4.limbo
diff --git a/examples/tui/example-rich-father.lela b/examples/tui/example-rich-father.limbo
similarity index 100%
rename from examples/tui/example-rich-father.lela
rename to examples/tui/example-rich-father.limbo
diff --git a/examples/tui/example-siblings.lela b/examples/tui/example-siblings.limbo
similarity index 100%
rename from examples/tui/example-siblings.lela
rename to examples/tui/example-siblings.limbo
diff --git a/examples/tui/example-unknown-father.lela b/examples/tui/example-unknown-father.limbo
similarity index 100%
rename from examples/tui/example-unknown-father.lela
rename to examples/tui/example-unknown-father.limbo
diff --git a/examples/tui/example-veggie.lela b/examples/tui/example-veggie.limbo
similarity index 100%
rename from examples/tui/example-veggie.lela
rename to examples/tui/example-veggie.limbo
diff --git a/examples/tui/sudoku.h b/examples/tui/sudoku.h
index 33a66c3cacab3a758524d581825fc92f1d68fb0b..be74e4889a270acc0d104cb1c1d4e8fca59d85e2 100644
--- a/examples/tui/sudoku.h
+++ b/examples/tui/sudoku.h
@@ -8,17 +8,17 @@
 #include <sstream>
 #include <vector>
 
-#include <lela/term.h>
-#include <lela/clause.h>
-#include <lela/literal.h>
-#include <lela/formula.h>
-#include <lela/format/output.h>
+#include <limbo/term.h>
+#include <limbo/clause.h>
+#include <limbo/literal.h>
+#include <limbo/formula.h>
+#include <limbo/format/output.h>
 
 #include "timer.h"
 
 struct SudokuCallbacks {
   template<typename T>
-  bool operator()(T* ctx, const std::string& proc, const std::vector<lela::Term>& args) {
+  bool operator()(T* ctx, const std::string& proc, const std::vector<limbo::Term>& args) {
     if (proc == "su_init") {
       ns_ = args;
     } else if (proc == "su_print") {
@@ -31,11 +31,11 @@ struct SudokuCallbacks {
         for (size_t x = 0; x < ns_.size(); ++x) {
           bool known = false;
           for (size_t n = 0; n < ns_.size(); ++n) {
-            const lela::Term Val = ctx->CreateTerm(ctx->LookupFunction("val"), {ns_[x], ns_[y]});
-            const lela::Clause c{lela::Literal::Eq(Val, ns_[n])};
-            bool b = ctx->kb()->Entails(*lela::Formula::Factory::Know(0, lela::Formula::Factory::Atomic(c)));
+            const limbo::Term Val = ctx->CreateTerm(ctx->LookupFunction("val"), {ns_[x], ns_[y]});
+            const limbo::Clause c{limbo::Literal::Eq(Val, ns_[n])};
+            bool b = ctx->kb()->Entails(*limbo::Formula::Factory::Know(0, limbo::Formula::Factory::Atomic(c)));
             if (b) {
-              using lela::format::operator<<;
+              using limbo::format::operator<<;
               std::stringstream ss;
               ss << ns_[n];
               std::cout << ss.str().substr(1);
@@ -66,7 +66,7 @@ struct SudokuCallbacks {
   }
 
  private:
-  std::vector<lela::Term> ns_;
+  std::vector<limbo::Term> ns_;
   Timer timer_;
 };
 
diff --git a/examples/tui/test-battleship-1x4.lela b/examples/tui/test-battleship-1x4.limbo
similarity index 100%
rename from examples/tui/test-battleship-1x4.lela
rename to examples/tui/test-battleship-1x4.limbo
diff --git a/examples/tui/test-control.lela b/examples/tui/test-control.limbo
similarity index 100%
rename from examples/tui/test-control.lela
rename to examples/tui/test-control.limbo
diff --git a/examples/tui/test-functions.lela b/examples/tui/test-functions.limbo
similarity index 100%
rename from examples/tui/test-functions.lela
rename to examples/tui/test-functions.limbo
diff --git a/examples/tui/test-guarantee.lela b/examples/tui/test-guarantee.limbo
similarity index 100%
rename from examples/tui/test-guarantee.lela
rename to examples/tui/test-guarantee.limbo
diff --git a/examples/tui/test-introspection-constant.lela b/examples/tui/test-introspection-constant.limbo
similarity index 100%
rename from examples/tui/test-introspection-constant.lela
rename to examples/tui/test-introspection-constant.limbo
diff --git a/examples/tui/test-introspection-disjunction.lela b/examples/tui/test-introspection-disjunction.limbo
similarity index 100%
rename from examples/tui/test-introspection-disjunction.lela
rename to examples/tui/test-introspection-disjunction.limbo
diff --git a/examples/tui/test-introspection-existential.lela b/examples/tui/test-introspection-existential.limbo
similarity index 100%
rename from examples/tui/test-introspection-existential.lela
rename to examples/tui/test-introspection-existential.limbo
diff --git a/examples/tui/test-propositions.lela b/examples/tui/test-propositions.limbo
similarity index 100%
rename from examples/tui/test-propositions.lela
rename to examples/tui/test-propositions.limbo
diff --git a/examples/tui/test-rich-father.lela b/examples/tui/test-rich-father.limbo
similarity index 100%
rename from examples/tui/test-rich-father.lela
rename to examples/tui/test-rich-father.limbo
diff --git a/examples/tui/test-siblings.lela b/examples/tui/test-siblings.limbo
similarity index 100%
rename from examples/tui/test-siblings.lela
rename to examples/tui/test-siblings.limbo
diff --git a/examples/tui/test-unknown-father.lela b/examples/tui/test-unknown-father.limbo
similarity index 100%
rename from examples/tui/test-unknown-father.lela
rename to examples/tui/test-unknown-father.limbo
diff --git a/examples/tui/test-veggie-with-guarantee.lela b/examples/tui/test-veggie-with-guarantee.limbo
similarity index 100%
rename from examples/tui/test-veggie-with-guarantee.lela
rename to examples/tui/test-veggie-with-guarantee.limbo
diff --git a/examples/tui/test-veggie.lela b/examples/tui/test-veggie.limbo
similarity index 100%
rename from examples/tui/test-veggie.lela
rename to examples/tui/test-veggie.limbo
diff --git a/examples/tui/test-ws-zoomed-by.lela b/examples/tui/test-ws-zoomed-by.limbo
similarity index 100%
rename from examples/tui/test-ws-zoomed-by.lela
rename to examples/tui/test-ws-zoomed-by.limbo
diff --git a/examples/tui/tui-js.cc b/examples/tui/tui-js.cc
index 6009d52b2e77cc71cea05f744aa398f00ea4a966..b6e1a9de0a18d5d974daaefabdd52792a97b14a6 100644
--- a/examples/tui/tui-js.cc
+++ b/examples/tui/tui-js.cc
@@ -11,16 +11,16 @@
 
 #include <emscripten.h>
 
-#include <lela/setup.h>
-#include <lela/formula.h>
-#include <lela/format/output.h>
-#include <lela/format/pdl/context.h>
-#include <lela/format/pdl/parser.h>
+#include <limbo/setup.h>
+#include <limbo/formula.h>
+#include <limbo/format/output.h>
+#include <limbo/format/pdl/context.h>
+#include <limbo/format/pdl/parser.h>
 
 #include "battleship.h"
 #include "sudoku.h"
 
-using lela::format::operator<<;
+using limbo::format::operator<<;
 
 template<typename T>
 inline std::string to_string(const T& x) {
@@ -41,7 +41,7 @@ static std::string in_color(const std::string& text, const std::string& color) {
   return ss.str();
 }
 
-struct Logger : public lela::format::pdl::DefaultLogger {
+struct Logger : public limbo::format::pdl::DefaultLogger {
   void operator()(const LogData&)                      const { std::cerr << "Unknown log data" << std::endl; }
   void operator()(const RegisterData& d)               const { std::cerr << "Registered " << d.id << std::endl; }
   void operator()(const RegisterSortData& d)           const { std::cerr << "Registered sort " << d.id << std::endl; }
@@ -54,7 +54,7 @@ struct Logger : public lela::format::pdl::DefaultLogger {
   void operator()(const UnregisterMetaVariableData& d) const { std::cerr << "Unregistered meta variable " << d.id << std::endl; }
   void operator()(const AddToKbData& d)                const { std::cerr << "Added " << d.alpha << " " << (d.ok ? "" : "un") << "successfully" << std::endl; }
   void operator()(const QueryData& d)                  const {
-    //for (lela::KnowledgeBase::sphere_index p = 0; p < d.kb.n_spheres(); ++p) {
+    //for (limbo::KnowledgeBase::sphere_index p = 0; p < d.kb.n_spheres(); ++p) {
     //  std::cerr << "Setup[" << p << "] = " << std::endl << d.kb.sphere(p).setup() << std::endl;
     //}
     const std::string r = in_color(d.yes ? "Yes" : "No", d.yes ? "#0c0" : "#c00");
@@ -69,15 +69,15 @@ struct Logger : public lela::format::pdl::DefaultLogger {
   bool print_queries = true;
 };
 
-struct Callback : public lela::format::pdl::DefaultCallback {
+struct Callback : public limbo::format::pdl::DefaultCallback {
   template<typename T>
-  void operator()(T* ctx, const std::string& proc, const std::vector<lela::Term>& args) {
+  void operator()(T* ctx, const std::string& proc, const std::vector<limbo::Term>& args) {
     if (proc == "print_kb") {
-      for (lela::KnowledgeBase::sphere_index p = 0; p < ctx->kb()->n_spheres(); ++p) {
+      for (limbo::KnowledgeBase::sphere_index p = 0; p < ctx->kb()->n_spheres(); ++p) {
         std::cout << "Setup[" << p << "] = " << std::endl << ctx->kb()->sphere(p)->setup() << std::endl;
       }
     } else if (proc == "print") {
-      lela::format::print_range(std::cout, args, "", "", " ");
+      limbo::format::print_range(std::cout, args, "", "", " ");
       std::cout << std::endl;
     } else if (proc == "enable_query_logging") {
       ctx->logger()->print_queries = true;
@@ -89,7 +89,7 @@ struct Callback : public lela::format::pdl::DefaultCallback {
       // it's a call for Sudoku
     } else {
       std::cout << "Calling " << proc;
-      lela::format::print_range(std::cerr, args, "(", ")", ",");
+      limbo::format::print_range(std::cerr, args, "(", ")", ",");
       std::cout << " failed" << std::endl;
     }
   }
@@ -99,25 +99,25 @@ struct Callback : public lela::format::pdl::DefaultCallback {
   SudokuCallbacks su_;
 };
 
-typedef lela::format::pdl::Context<Logger, Callback> Context;
-typedef lela::format::pdl::Parser<std::string::const_iterator, Context> Parser;
+typedef limbo::format::pdl::Context<Logger, Callback> Context;
+typedef limbo::format::pdl::Parser<std::string::const_iterator, Context> Parser;
 
 static Context* ctx = nullptr;
 
-extern "C" void lela_init() {
+extern "C" void limbo_init() {
   if (ctx) {
     delete ctx;
   }
   ctx = new Context();
 }
 
-extern "C" void lela_free() {
+extern "C" void limbo_free() {
   if (ctx) {
     delete ctx;
   }
 }
 
-extern "C" void lela_parse(const char* c_str) {
+extern "C" void limbo_parse(const char* c_str) {
   const std::string str = c_str;
 
   Parser parser(str.begin(), str.end());
diff --git a/examples/tui/tui-js.html b/examples/tui/tui-js.html
index f4f33238df828c9dc6911e0914edacd7d0594a1d..964a5e8b131b5efa3754110d08eb22bd9a88a108 100644
--- a/examples/tui/tui-js.html
+++ b/examples/tui/tui-js.html
@@ -185,11 +185,11 @@ function resetTerminal() {
 }
 
 function loadExample(file) {
-    Module.ccall('lela_init', 'void', [], []);
+    Module.ccall('limbo_init', 'void', [], []);
     $('#examples').val('');
     if (file) {
         $.ajax({
-            url : file + '.lela',
+            url : file + '.limbo',
             dataType: 'text',
             success: function(data) {
                 $('#examples').val(file);
@@ -227,7 +227,7 @@ function loadExample(file) {
     }
 }
 
-function lela_exec(command) {
+function limbo_exec(command) {
     var t = $('#terminal').terminal();
     if (command == 'help') {
         var maxlen = 0;
@@ -261,14 +261,14 @@ function lela_exec(command) {
     } else if (command == 'hide-debug') {
         $('#show-debug').prop('checked', false).change();
     } else {
-        Module.ccall('lela_parse', 'void', ['string'], [command]);
+        Module.ccall('limbo_parse', 'void', ['string'], [command]);
     }
 }
 
 $(document).ready(function() {
     $('#debug-toggle').click(function() { $('#debug-div').toggle(); return false; });
 
-    Module.ccall('lela_init', 'void', [], []);
+    Module.ccall('limbo_init', 'void', [], []);
 
     var select_ex = getParameterByName('ex');
     if (select_ex) {
@@ -278,16 +278,16 @@ $(document).ready(function() {
     }
 
     jQuery(function($, undefined) {
-	$('#terminal').terminal(lela_exec, {
+	$('#terminal').terminal(limbo_exec, {
 	    greetings:
-                inColor('LELA Terminal\n'+
+                inColor('Limbo Terminal\n'+
 		        '\n'+
 		        'Select one of the pre-defined examples from the dropdown list above, or type "help" and press enter.\n'+
                         '\n', 'purple'),
 	    name: 'tui',
 	    height: 0.75 * $(window).height(),
 	    width: 0.95 * $(window).width(),
-            prompt: inColor('lela> ', '#888'),
+            prompt: inColor('limbo> ', '#888'),
 	});
     });
 
diff --git a/examples/tui/tui.cc b/examples/tui/tui.cc
index 066c2ec80ea8b798b4ef0b4d97b237fff474ffc9..854a0c0f226254f5de620520971779fcdfb44ee6 100644
--- a/examples/tui/tui.cc
+++ b/examples/tui/tui.cc
@@ -14,19 +14,19 @@
 #include <memory>
 #include <vector>
 
-#include <lela/setup.h>
-#include <lela/formula.h>
-#include <lela/internal/iter.h>
-#include <lela/format/output.h>
-#include <lela/format/pdl/context.h>
-#include <lela/format/pdl/parser.h>
+#include <limbo/setup.h>
+#include <limbo/formula.h>
+#include <limbo/internal/iter.h>
+#include <limbo/format/output.h>
+#include <limbo/format/pdl/context.h>
+#include <limbo/format/pdl/parser.h>
 
 #include "linenoise/linenoise.h"
 
 #include "battleship.h"
 #include "sudoku.h"
 
-using lela::format::operator<<;
+using limbo::format::operator<<;
 
 static constexpr int RED = 31;
 static constexpr int GREEN = 32;
@@ -39,7 +39,7 @@ static std::string in_color(const std::string& text, int color) {
 
 template<typename ForwardIt, typename Context>
 static bool parse(ForwardIt begin, ForwardIt end, Context* ctx) {
-  typedef lela::format::pdl::Parser<ForwardIt, Context> Parser;
+  typedef limbo::format::pdl::Parser<ForwardIt, Context> Parser;
   Parser parser(begin, end);
   auto parse_result = parser.Parse();
   if (!parse_result) {
@@ -63,7 +63,7 @@ class multi_pass_iterator {
   typedef value_type reference;
   typedef value_type* pointer;
   typedef std::forward_iterator_tag iterator_category;
-  typedef lela::internal::iterator_proxy<multi_pass_iterator> proxy;
+  typedef limbo::internal::iterator_proxy<multi_pass_iterator> proxy;
 
   multi_pass_iterator() = default;
   multi_pass_iterator(InputIt it) : data_(new Data(it)) {}
@@ -110,15 +110,15 @@ class multi_pass_iterator {
   size_t index_ = 0;
 };
 
-struct Callback : public lela::format::pdl::DefaultCallback {
+struct Callback : public limbo::format::pdl::DefaultCallback {
   template<typename T>
-  void operator()(T* ctx, const std::string& proc, const std::vector<lela::Term>& args) {
+  void operator()(T* ctx, const std::string& proc, const std::vector<limbo::Term>& args) {
     if (proc == "print_kb") {
-      for (lela::KnowledgeBase::sphere_index p = 0; p < ctx->kb()->n_spheres(); ++p) {
+      for (limbo::KnowledgeBase::sphere_index p = 0; p < ctx->kb()->n_spheres(); ++p) {
         std::cerr << "Setup[" << p << "] = " << std::endl << ctx->kb()->sphere(p)->setup() << std::endl;
       }
     } else if (proc == "print") {
-      lela::format::print_range(std::cout, args, "", "", " ");
+      limbo::format::print_range(std::cout, args, "", "", " ");
       std::cout << std::endl;
     } else if (proc == "enable_query_logging") {
       ctx->logger()->print_queries = true;
@@ -130,7 +130,7 @@ struct Callback : public lela::format::pdl::DefaultCallback {
       // it's a call for Sudoku
     } else {
       std::cerr << "Calling " << proc;
-      lela::format::print_range(std::cerr, args, "(", ")", ",");
+      limbo::format::print_range(std::cerr, args, "(", ")", ",");
       std::cerr << " failed" << std::endl;
     }
   }
@@ -140,7 +140,7 @@ struct Callback : public lela::format::pdl::DefaultCallback {
   SudokuCallbacks su_;
 };
 
-struct Logger : public lela::format::pdl::DefaultLogger {
+struct Logger : public limbo::format::pdl::DefaultLogger {
   void operator()(const LogData&)                      const { std::cerr << "Unknown log data" << std::endl; }
   void operator()(const RegisterData& d)               const { std::cerr << "Registered " << d.id << std::endl; }
   void operator()(const RegisterSortData& d)           const { std::cerr << "Registered sort " << d.id << std::endl; }
@@ -153,7 +153,7 @@ struct Logger : public lela::format::pdl::DefaultLogger {
   void operator()(const UnregisterMetaVariableData& d) const { std::cerr << "Unregistered meta variable " << d.id << std::endl; }
   void operator()(const AddToKbData& d)                const { std::cerr << "Added " << d.alpha << " " << (d.ok ? "" : "un") << "successfully" << std::endl; }
   void operator()(const QueryData& d)                  const {
-    //for (lela::KnowledgeBase::sphere_index p = 0; p < d.kb.n_spheres(); ++p) {
+    //for (limbo::KnowledgeBase::sphere_index p = 0; p < d.kb.n_spheres(); ++p) {
     //  std::cout << "Setup[" << p << "] = " << std::endl << d.kb.sphere(p).setup() << std::endl;
     //}
     std::ostream* os;
@@ -167,7 +167,7 @@ struct Logger : public lela::format::pdl::DefaultLogger {
     //std::cout << std::endl;
   }
   bool print_queries = true;
-  lela::format::pdl::Context<Logger, Callback>* ctx;
+  limbo::format::pdl::Context<Logger, Callback>* ctx;
 };
 
 int main(int argc, char** argv) {
@@ -210,7 +210,7 @@ int main(int argc, char** argv) {
   }
 
   std::ios_base::sync_with_stdio(true);
-  lela::format::pdl::Context<Logger, Callback> ctx;
+  limbo::format::pdl::Context<Logger, Callback> ctx;
   ctx.logger()->ctx = &ctx;
 
   for (const std::string& arg : args) {
@@ -269,7 +269,7 @@ int main(int argc, char** argv) {
 	if ((dir = opendir(directory.c_str())) != NULL) {
 	  while ((ent = readdir(dir)) != NULL) {
             const std::string file = ent->d_name;
-	    if (is_postfix(".lela", file)) {
+	    if (is_postfix(".limbo", file)) {
               std::cout << file << std::endl;
             }
 	  }
diff --git a/examples/upload.sh b/examples/upload.sh
index 31a74d428d81ab4aa59e455dcf12c38bd8e80b10..a784b0012abcf012d59d00e2a5c3bbcd2ab1728e 100755
--- a/examples/upload.sh
+++ b/examples/upload.sh
@@ -1,2 +1,2 @@
-./zip.sh - | ssh unsw "tar zxvf - -C public_html/demo/"
+./zip.sh - | ssh unsw "tar zxvf - -C public_html/limbo/"
 
diff --git a/examples/zip.sh b/examples/zip.sh
index 78b1569391cfb924bec01bca05caf6220623afc8..402ab3a94b43a8dedc1b6bccc6cb5ee6ff04b4ac 100755
--- a/examples/zip.sh
+++ b/examples/zip.sh
@@ -18,5 +18,5 @@ $CMD \
     index.html jquery*.js \
     minesweeper/minesweeper-js.{html,js,js.mem} minesweeper/*.svg \
     sudoku/sudoku-js.{html,js,js.mem} sudoku/sudokus.txt \
-    tui/tui-js.{html,js,js.mem} tui/jquery.terminal*.{js,css} tui/unix_formatting.js tui/*.lela
+    tui/tui-js.{html,js,js.mem} tui/jquery.terminal*.{js,css} tui/unix_formatting.js tui/*.limbo
 
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0c870a0ac3494ad67af3fed8a748bac317d6ff92..44edc9dd5ba0edbce60b8c18603c245e0bb43aac 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1,7 +1,7 @@
-add_library (lela INTERFACE)
+add_library (limbo INTERFACE)
 
-target_include_directories (lela INTERFACE
+target_include_directories (limbo INTERFACE
 	$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
-	$<INSTALL_INTERFACE:include/lela>
+	$<INSTALL_INTERFACE:include/limbo>
 )
 
diff --git a/src/lela/clause.h b/src/limbo/clause.h
similarity index 95%
rename from src/lela/clause.h
rename to src/limbo/clause.h
index 02e4dc792318816a69046ca7a105ad4df6f0a5e1..926448cfcbca740117b2c4fd594301997d41b34d 100644
--- a/src/lela/clause.h
+++ b/src/limbo/clause.h
@@ -17,8 +17,8 @@
 // that unit propagation or subsumption won't work early (in a sound but
 // incomplete way).
 
-#ifndef LELA_CLAUSE_H_
-#define LELA_CLAUSE_H_
+#ifndef LIMBO_CLAUSE_H_
+#define LIMBO_CLAUSE_H_
 
 #include <cassert>
 #include <cstring>
@@ -31,15 +31,15 @@
 #include <utility>
 #include <vector>
 
-#include <lela/literal.h>
+#include <limbo/literal.h>
 
-#include <lela/internal/bloom.h>
-#include <lela/internal/ints.h>
-#include <lela/internal/iter.h>
-#include <lela/internal/maybe.h>
-#include <lela/internal/traits.h>
+#include <limbo/internal/bloom.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/iter.h>
+#include <limbo/internal/maybe.h>
+#include <limbo/internal/traits.h>
 
-namespace lela {
+namespace limbo {
 
 class Clause {
  public:
@@ -449,22 +449,22 @@ next:
   std::unique_ptr<Literal[]> lits2_;
 };
 
-}  // namespace lela
+}  // namespace limbo
 
 
 namespace std {
 
 template<>
-struct hash<lela::Clause> {
-  lela::internal::hash32_t operator()(const lela::Clause& a) const { return a.hash(); }
+struct hash<limbo::Clause> {
+  limbo::internal::hash32_t operator()(const limbo::Clause& a) const { return a.hash(); }
 };
 
 template<>
-struct equal_to<lela::Clause> {
-  bool operator()(const lela::Clause& a, const lela::Clause& b) const { return a == b; }
+struct equal_to<limbo::Clause> {
+  bool operator()(const limbo::Clause& a, const limbo::Clause& b) const { return a == b; }
 };
 
 }  // namespace std
 
-#endif  // LELA_CLAUSE_H_
+#endif  // LIMBO_CLAUSE_H_
 
diff --git a/src/lela/format/cpp/syntax.h b/src/limbo/format/cpp/syntax.h
similarity index 91%
rename from src/lela/format/cpp/syntax.h
rename to src/limbo/format/cpp/syntax.h
index 725dd9583d44ce5b99ce52a7f34d8533b4e017b9..d3cef4caf2e016a0e8ec2ead942d40fe4f2c72f2 100644
--- a/src/lela/format/cpp/syntax.h
+++ b/src/limbo/format/cpp/syntax.h
@@ -4,20 +4,20 @@
 //
 // Overloads some operators to provide a higher-level syntax for formulas.
 
-#ifndef LELA_FORMAT_CPP_SYNTAX_H_
-#define LELA_FORMAT_CPP_SYNTAX_H_
+#ifndef LIMBO_FORMAT_CPP_SYNTAX_H_
+#define LIMBO_FORMAT_CPP_SYNTAX_H_
 
 #include <utility>
 
-#include <lela/formula.h>
-#include <lela/clause.h>
-#include <lela/literal.h>
-#include <lela/solver.h>
-#include <lela/term.h>
+#include <limbo/formula.h>
+#include <limbo/clause.h>
+#include <limbo/literal.h>
+#include <limbo/solver.h>
+#include <limbo/term.h>
 
 #define MARK (std::cout << __FILE__ << ":" << __LINE__ << std::endl)
 
-namespace lela {
+namespace limbo {
 namespace format {
 namespace cpp {
 
@@ -43,7 +43,7 @@ class HiFormula;
 class HiFormula {
  public:
   HiFormula(const Literal& a) : HiFormula(Clause({a})) {}  // NOLINT
-  HiFormula(const lela::Clause& c) : HiFormula(Formula::Factory::Atomic(c)) {}  // NOLINT
+  HiFormula(const limbo::Clause& c) : HiFormula(Formula::Factory::Atomic(c)) {}  // NOLINT
   HiFormula(const Formula::Ref& phi) : HiFormula(*phi) {}  // NOLINT
   HiFormula(const Formula& phi) : phi_(phi.Clone()) {}  // NOLINT
 
@@ -128,7 +128,7 @@ inline HiFormula Fa(HiTerm x, const HiFormula& phi) { return ~Ex(x, ~phi); }
 
 }  // namespace cpp
 }  // namespace format
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_FORMAT_CPP_SYNTAX_H_
+#endif  // LIMBO_FORMAT_CPP_SYNTAX_H_
 
diff --git a/src/lela/format/output.h b/src/limbo/format/output.h
similarity index 88%
rename from src/lela/format/output.h
rename to src/limbo/format/output.h
index 09dedca0316b99a606c20133b8487e7d9e7201f8..34e11ee92e90a81bcc845fb839e975387443b87b 100644
--- a/src/lela/format/output.h
+++ b/src/limbo/format/output.h
@@ -17,20 +17,20 @@
 #include <utility>
 #include <vector>
 
-#include <lela/term.h>
+#include <limbo/term.h>
 
-#include <lela/internal/compar.h>
-#include <lela/internal/iter.h>
-#include <lela/internal/maybe.h>
+#include <limbo/internal/compar.h>
+#include <limbo/internal/iter.h>
+#include <limbo/internal/maybe.h>
 
-#ifndef MARK
+#ifndef MARK  // NOLINT
 #define MARK (std::cout << __FILE__ << ":" << __LINE__ << std::endl)
 #endif
 
-namespace lela {
+namespace limbo {
 namespace format {
 
-#ifndef LELA_FORMAT_OUTPUT_H_
+#ifndef LIMBO_FORMAT_OUTPUT_H_
 typedef std::unordered_map<Symbol::Sort, std::string> SortMap;
 typedef std::unordered_map<Symbol, std::string> SymbolMap;
 
@@ -115,21 +115,21 @@ std::ostream& operator<<(std::ostream& os, const std::unordered_map<K, T, H, E>&
 
 template<typename K, typename T, typename H, typename E>
 std::ostream& operator<<(std::ostream& os, const std::unordered_multimap<K, T, H, E>& map);
-#endif  // LELA_FORMAT_OUTPUT_H_
+#endif  // LIMBO_FORMAT_OUTPUT_H_
 
-#ifdef LELA_INTERNAL_HASHSET_H_
+#ifdef LIMBO_INTERNAL_HASHSET_H_
 template<typename T, typename H, typename E>
 std::ostream& operator<<(std::ostream& os, const internal::HashSet<T, H, E>& set);
-#endif  // LELA_INTERNAL_HASHSET_H_
+#endif  // LIMBO_INTERNAL_HASHSET_H_
 
-#ifdef LELA_INTERNAL_MAYBE_H_
+#ifdef LIMBO_INTERNAL_MAYBE_H_
 template<typename K, typename T>
 std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m);
-#endif  // LELA_INTERNAL_MAYBE_H_
+#endif  // LIMBO_INTERNAL_MAYBE_H_
 
-#ifdef LELA_TERM_H_
-#ifndef LELA_TERM_OUTPUT
-#define LELA_TERM_OUTPUT
+#ifdef LIMBO_TERM_H_
+#ifndef LIMBO_TERM_OUTPUT
+#define LIMBO_TERM_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Symbol s) {
   internal::Maybe<std::string> sort_name = LookupSort(s.sort());
   internal::Maybe<std::string> symbol_name = LookupSymbol(s);
@@ -165,22 +165,22 @@ std::ostream& operator<<(std::ostream& os, const Term t) {
   }
   return os;
 }
-#endif  // LELA_TERM_OUTPUT
-#endif  // LELA_TERM_H_
+#endif  // LIMBO_TERM_OUTPUT
+#endif  // LIMBO_TERM_H_
 
-#ifdef LELA_LITERAL_H_
-#ifndef LELA_LITERAL_OUTPUT
-#define LELA_LITERAL_OUTPUT
+#ifdef LIMBO_LITERAL_H_
+#ifndef LIMBO_LITERAL_OUTPUT
+#define LIMBO_LITERAL_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Literal a) {
   os << a.lhs() << ' ' << (a.pos() ? "\u003D" : "\u2260") << ' ' << a.rhs();
   return os;
 }
-#endif  // LELA_LITERAL_OUTPUT_
-#endif  // LELA_LITERAL_H_
+#endif  // LIMBO_LITERAL_OUTPUT_
+#endif  // LIMBO_LITERAL_H_
 
-#ifdef LELA_CLAUSE_H_
-#ifndef LELA_CLAUSE_OUTPUT
-#define LELA_CLAUSE_OUTPUT
+#ifdef LIMBO_CLAUSE_H_
+#ifndef LIMBO_CLAUSE_OUTPUT
+#define LIMBO_CLAUSE_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Clause& c) {
   struct PrintLiteralComparator {
     struct PrintTermComparator {
@@ -223,23 +223,23 @@ std::ostream& operator<<(std::ostream& os, const Clause& c) {
   std::sort(vec.begin(), vec.end(), PrintLiteralComparator());
   return print_range(os, vec, "[", "]", " \u2228 ");
 }
-#endif  // LELA_OUTPUT_CLAUSE
-#endif  // LELA_CLAUSE_H_
+#endif  // LIMBO_OUTPUT_CLAUSE
+#endif  // LIMBO_CLAUSE_H_
 
-#ifdef LELA_SETUP_H_
-#ifndef LELA_SETUP_OUTPUT
-#define LELA_SETUP_OUTPUT
+#ifdef LIMBO_SETUP_H_
+#ifndef LIMBO_SETUP_OUTPUT
+#define LIMBO_SETUP_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Setup& s) {
   auto is = s.clauses();
   auto cs = internal::transform_range(is.begin(), is.end(), [&s](size_t i) { return s.clause(i); });
   return print_range(os, cs, "{ ", "\n}", "\n, ");
 }
-#endif  // LELA_SETUP_OUTPUT
-#endif  // LELA_SETUP_H_
+#endif  // LIMBO_SETUP_OUTPUT
+#endif  // LIMBO_SETUP_H_
 
-#ifdef LELA_FORMULA_H_
-#ifndef LELA_FORMULA_OUTPUT
-#define LELA_FORMULA_OUTPUT
+#ifdef LIMBO_FORMULA_H_
+#ifndef LIMBO_FORMULA_OUTPUT
+#define LIMBO_FORMULA_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Formula& alpha) {
   switch (alpha.type()) {
     case Formula::kAtomic: {
@@ -316,10 +316,10 @@ std::ostream& operator<<(std::ostream& os, const Formula& alpha) {
 std::ostream& operator<<(std::ostream& os, const Formula::Ref& alpha) {
   return os << *alpha;
 }
-#endif  // LELA_FORMULA_OUTPUT
-#endif  // LELA_FORMULA_H_
+#endif  // LIMBO_FORMULA_OUTPUT
+#endif  // LIMBO_FORMULA_H_
 
-#ifndef LELA_FORMAT_OUTPUT_H_
+#ifndef LIMBO_FORMAT_OUTPUT_H_
 template<typename InputIt>
 std::ostream& print_sequence(std::ostream& os,
                              InputIt begin,
@@ -415,22 +415,22 @@ std::ostream& operator<<(std::ostream& os, const std::unordered_multimap<K, T, H
   print_sequence(os, map.begin(), map.end(), "m{", "}m", ", ");
   return os;
 }
-#endif  // LELA_FORMAT_OUTPUT_H_
+#endif  // LIMBO_FORMAT_OUTPUT_H_
 
-#ifdef LELA_INTERNAL_HASHSET_H_
-#ifndef LELA_INTERNAL_HASHSET_OUTPUT
-#define LELA_INTERNAL_HASHSET_OUTPUT
+#ifdef LIMBO_INTERNAL_HASHSET_H_
+#ifndef LIMBO_INTERNAL_HASHSET_OUTPUT
+#define LIMBO_INTERNAL_HASHSET_OUTPUT
 template<typename T, typename H, typename E>
 std::ostream& operator<<(std::ostream& os, const internal::HashSet<T, H, E>& set) {
   print_sequence(os, set.begin(), set.end(), "{", "}", ", ");
   return os;
 }
-#endif  // LELA_INTERNAL_HASHSET_OUTPUT
-#endif  // LELA_INTERNAL_HASHSET_H_
+#endif  // LIMBO_INTERNAL_HASHSET_OUTPUT
+#endif  // LIMBO_INTERNAL_HASHSET_H_
 
-#ifdef LELA_INTERNAL_MAYBE_H_
-#ifndef LELA_INTERNAL_MAYBE_OUTPUT
-#define LELA_INTERNAL_MAYBE_OUTPUT
+#ifdef LIMBO_INTERNAL_MAYBE_H_
+#ifndef LIMBO_INTERNAL_MAYBE_OUTPUT
+#define LIMBO_INTERNAL_MAYBE_OUTPUT
 template<typename T>
 std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m) {
   if (m) {
@@ -440,13 +440,13 @@ std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m) {
   }
   return os;
 }
-#endif  // LELA_INTERNAL_MAYBE_OUTPUT
-#endif  // LELA_INTERNAL_MAYBE_H_
+#endif  // LIMBO_INTERNAL_MAYBE_OUTPUT
+#endif  // LIMBO_INTERNAL_MAYBE_H_
 
 }  // namespace format
-}  // namespace lela
+}  // namespace limbo
 
-#ifndef LELA_FORMAT_OUTPUT_H_
-#define LELA_FORMAT_OUTPUT_H_
-#endif  // LELA_FORMAT_OUTPUT_H_
+#ifndef LIMBO_FORMAT_OUTPUT_H_
+#define LIMBO_FORMAT_OUTPUT_H_
+#endif  // LIMBO_FORMAT_OUTPUT_H_
 
diff --git a/src/lela/format/pdl/context.h b/src/limbo/format/pdl/context.h
similarity index 94%
rename from src/lela/format/pdl/context.h
rename to src/limbo/format/pdl/context.h
index e7ca79befaad0a841dfaee27eafd50b464145e98..e5d4a5aef282718fb71245e7ba9a6f7c55a5e91b 100644
--- a/src/lela/format/pdl/context.h
+++ b/src/limbo/format/pdl/context.h
@@ -9,8 +9,8 @@
 // operator() for the structs defined in Logger. Logger itself is a minimal
 // implementation of a Logger, which ignores all log data.
 
-#ifndef LELA_FORMAT_PDL_CONTEXT_H_
-#define LELA_FORMAT_PDL_CONTEXT_H_
+#ifndef LIMBO_FORMAT_PDL_CONTEXT_H_
+#define LIMBO_FORMAT_PDL_CONTEXT_H_
 
 #include <iostream>
 #include <map>
@@ -19,13 +19,13 @@
 #include <utility>
 #include <vector>
 
-#include <lela/term.h>
-#include <lela/formula.h>
-#include <lela/kb.h>
+#include <limbo/term.h>
+#include <limbo/formula.h>
+#include <limbo/kb.h>
 
-#include <lela/format/output.h>
+#include <limbo/format/output.h>
 
-namespace lela {
+namespace limbo {
 namespace format {
 namespace pdl {
 
@@ -133,7 +133,7 @@ class Context {
 
   void RegisterSort(const std::string& id) {
     const Symbol::Sort sort = CreateSort();
-    lela::format::RegisterSort(sort, "");
+    limbo::format::RegisterSort(sort, "");
     sorts_.Register(id, sort);
     logger_(DefaultLogger::RegisterSortData(id));
   }
@@ -144,7 +144,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Term var = CreateVariable(sort);
     vars_.Register(id, var);
-    lela::format::RegisterSymbol(var.symbol(), id);
+    limbo::format::RegisterSymbol(var.symbol(), id);
     logger_(DefaultLogger::RegisterVariableData(id, sort_id));
   }
 
@@ -154,7 +154,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Term name = CreateName(sort);
     names_.Register(id, name);
-    lela::format::RegisterSymbol(name.symbol(), id);
+    limbo::format::RegisterSymbol(name.symbol(), id);
     logger_(DefaultLogger::RegisterNameData(id, sort_id));
   }
 
@@ -164,7 +164,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Symbol fun = CreateFunction(sort, arity);
     funs_.Register(id, fun);
-    lela::format::RegisterSymbol(fun, id);
+    limbo::format::RegisterSymbol(fun, id);
     logger_(DefaultLogger::RegisterFunctionData(id, arity, sort_id));
   }
 
@@ -237,7 +237,7 @@ class Context {
 
 }  // namespace pdl
 }  // namespace format
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_FORMAT_PDL_CONTEXT_H_
+#endif  // LIMBO_FORMAT_PDL_CONTEXT_H_
 
diff --git a/src/lela/format/pdl/lexer.h b/src/limbo/format/pdl/lexer.h
similarity index 97%
rename from src/lela/format/pdl/lexer.h
rename to src/limbo/format/pdl/lexer.h
index 311d2c9e849cdb4aba1b1b951189e25a143799c3..53cb082e8ffe7a92bbbb725cb84470b22f3583a6 100644
--- a/src/lela/format/pdl/lexer.h
+++ b/src/limbo/format/pdl/lexer.h
@@ -7,8 +7,8 @@
 // The compuational complexity is pretty bad (O(n^2)), but we don't expect very
 // long tokens, so parsing shouldn't be the bottleneck.
 
-#ifndef LELA_FORMAT_PDL_LEXER_H_
-#define LELA_FORMAT_PDL_LEXER_H_
+#ifndef LIMBO_FORMAT_PDL_LEXER_H_
+#define LIMBO_FORMAT_PDL_LEXER_H_
 
 #include <cassert>
 
@@ -18,9 +18,9 @@
 #include <string>
 #include <utility>
 
-#include <lela/internal/iter.h>
+#include <limbo/internal/iter.h>
 
-namespace lela {
+namespace limbo {
 namespace format {
 namespace pdl {
 
@@ -69,7 +69,7 @@ class Lexer {
     typedef value_type reference;
     typedef value_type* pointer;
     typedef std::forward_iterator_tag iterator_category;
-    typedef lela::internal::iterator_proxy<iterator> proxy;
+    typedef limbo::internal::iterator_proxy<iterator> proxy;
 
     iterator() = default;
     iterator(const LexemeVector* lexemes, ForwardIt it, ForwardIt end) : lexemes_(lexemes), it_(it), end_(end) {
@@ -147,9 +147,9 @@ class Lexer {
 
   Lexer(ForwardIt begin, ForwardIt end) : begin_(begin), end_(end) {
     lexemes_.emplace_back(Token::kSort,         [](Word w) { return IsPrefix(w, {"Sort", "sort"}); });
-    lexemes_.emplace_back(Token::kVar,          [](Word w) { return IsPrefix(w, {"Var", "Variable", "var", "variable"}); });
+    lexemes_.emplace_back(Token::kVar,          [](Word w) { return IsPrefix(w, {"Var", "Variable", "var", "variable"}); });  // NOLINT
     lexemes_.emplace_back(Token::kName,         [](Word w) { return IsPrefix(w, {"Name", "name"}); });
-    lexemes_.emplace_back(Token::kFun,          [](Word w) { return IsPrefix(w, {"Fun", "fun", "Function", "function"}); });
+    lexemes_.emplace_back(Token::kFun,          [](Word w) { return IsPrefix(w, {"Fun", "fun", "Function", "function"}); });  // NOLINT
     lexemes_.emplace_back(Token::kSlash,        [](Word w) { return IsPrefix(w, "/"); });
     lexemes_.emplace_back(Token::kKB,           [](Word w) { return IsPrefix(w, {"KB", "Kb", "kb"}); });
     lexemes_.emplace_back(Token::kLet,          [](Word w) { return IsPrefix(w, {"Let", "let"}); });
@@ -299,7 +299,7 @@ std::ostream& operator<<(std::ostream& os, const Token& t) {
 
 }  // namespace pdl
 }  // namespace format
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_FORMAT_PDL_LEXER_H_
+#endif  // LIMBO_FORMAT_PDL_LEXER_H_
 
diff --git a/src/lela/format/pdl/parser.h b/src/limbo/format/pdl/parser.h
similarity index 73%
rename from src/lela/format/pdl/parser.h
rename to src/limbo/format/pdl/parser.h
index 9357561ab50d00a280d20296cdca81a56c89b411..3e6dce705d446cf9610c6e7e3ca8ebdfd427ef70 100644
--- a/src/lela/format/pdl/parser.h
+++ b/src/limbo/format/pdl/parser.h
@@ -8,8 +8,8 @@
 // definition. The Context template parameter is merely passed around to be
 // the argument of Parser::Action functors, as returned by Parser::Parse().
 
-#ifndef LELA_FORMAT_PDL_PARSER_H_
-#define LELA_FORMAT_PDL_PARSER_H_
+#ifndef LIMBO_FORMAT_PDL_PARSER_H_
+#define LIMBO_FORMAT_PDL_PARSER_H_
 
 #include <cassert>
 
@@ -21,22 +21,22 @@
 #include <utility>
 #include <vector>
 
-#include <lela/formula.h>
-#include <lela/grounder.h>
-#include <lela/setup.h>
+#include <limbo/formula.h>
+#include <limbo/grounder.h>
+#include <limbo/setup.h>
 
-#include <lela/format/output.h>
+#include <limbo/format/output.h>
 
-#include <lela/format/pdl/lexer.h>
+#include <limbo/format/pdl/lexer.h>
 
-namespace lela {
+namespace limbo {
 namespace format {
 namespace pdl {
 
-#define LELA_S(x)          #x
-#define LELA_S_(x)         LELA_S(x)
-#define LELA_STR__LINE__   LELA_S_(__LINE__)
-#define LELA_MSG(msg)      (std::string(msg) +" (in rule "+ __FUNCTION__ +":"+ LELA_STR__LINE__ +")")
+#define LIMBO_S(x)          #x
+#define LIMBO_S_(x)         LIMBO_S(x)
+#define LIMBO_STR__LINE__   LIMBO_S_(__LINE__)
+#define LIMBO_MSG(msg)      (std::string(msg) +" (in rule "+ __FUNCTION__ +":"+ LIMBO_STR__LINE__ +")")
 
 template<typename ForwardIt, typename Context>
 class Parser {
@@ -111,7 +111,7 @@ class Parser {
       if (f) {
         return (*f)(ctx);
       } else {
-        return Result<T>(Result<T>::kError, LELA_MSG("Action is null"));
+        return Result<T>(Result<T>::kError, LIMBO_MSG("Action is null"));
       }
     }
 
@@ -186,11 +186,11 @@ class Parser {
               ctx->RegisterSort(id);
               return Success<>();
             } else {
-              return Error<>(LELA_MSG("Sort "+ id +" is already registered"));
+              return Error<>(LIMBO_MSG("Sort "+ id +" is already registered"));
             }
           };
         } else {
-          return Error<Action<>>(LELA_MSG("Expected sort identifier"));
+          return Error<Action<>>(LIMBO_MSG("Expected sort identifier"));
         }
       } while (Is(Tok(), Token::kComma));
       return Success<Action<>>(std::move(a));
@@ -204,7 +204,7 @@ class Parser {
           ids.push_back(Tok().val.str());
           Advance();
         } else {
-          return Error<Action<>>(LELA_MSG(var ? "Expected variable identifier" : "Expected name identifier"));
+          return Error<Action<>>(LIMBO_MSG(var ? "Expected variable identifier" : "Expected name identifier"));
         }
       } while (Is(Tok(0), Token::kComma));
       if (Is(Tok(0), Token::kRArrow) &&
@@ -219,16 +219,16 @@ class Parser {
                 var ? ctx->RegisterVariable(id, sort) : ctx->RegisterName(id, sort);
                 return Success<>();
               } else {
-                return Error<>(LELA_MSG("Term "+ id +" is already registered"));
+                return Error<>(LIMBO_MSG("Term "+ id +" is already registered"));
               }
             } else {
-              return Error<>(LELA_MSG("Sort "+ sort +" is not registered"));
+              return Error<>(LIMBO_MSG("Sort "+ sort +" is not registered"));
             }
           };
         }
         return Success<Action<>>(std::move(a));
       } else {
-        return Error<Action<>>(LELA_MSG("Expected arrow and sort identifier"));
+        return Error<Action<>>(LIMBO_MSG("Expected arrow and sort identifier"));
       }
     }
     if (Is(Tok(), Token::kFun)) {
@@ -241,7 +241,7 @@ class Parser {
           ids.push_back(std::make_pair(Tok(0).val.str(), std::stoi(Tok(2).val.str())));
           Advance(3);
         } else {
-          return Error<Action<>>(LELA_MSG("Expected function identifier"));
+          return Error<Action<>>(LIMBO_MSG("Expected function identifier"));
         }
       } while (Is(Tok(0), Token::kComma));
       if (Is(Tok(0), Token::kRArrow) &&
@@ -258,19 +258,19 @@ class Parser {
                 ctx->RegisterFunction(id, arity, sort);
                 return Success<>();
               } else {
-                return Error<>(LELA_MSG("Term "+ id +" is already registered"));
+                return Error<>(LIMBO_MSG("Term "+ id +" is already registered"));
               }
             } else {
-              return Error<>(LELA_MSG("Sort "+ sort +" is not registered"));
+              return Error<>(LIMBO_MSG("Sort "+ sort +" is not registered"));
             }
           };
         }
         return Success<Action<>>(std::move(a));
       } else {
-        return Error<Action<>>(LELA_MSG("Expected arrow and sort identifier"));
+        return Error<Action<>>(LIMBO_MSG("Expected arrow and sort identifier"));
       }
     }
-    return Unapplicable<Action<>>(LELA_MSG("Expected 'Sort', 'Var', 'Name' or 'Fun'"));
+    return Unapplicable<Action<>>(LIMBO_MSG("Expected 'Sort', 'Var', 'Name' or 'Fun'"));
   }
 
   // atomic_term --> x
@@ -288,17 +288,17 @@ class Parser {
         } else if (ctx->IsRegisteredFunction(id)) {
           Symbol f = ctx->LookupFunction(id);
           if (f.arity() != 0) {
-            return Error<Term>(LELA_MSG("Wrong number of arguments for "+ id));
+            return Error<Term>(LIMBO_MSG("Wrong number of arguments for "+ id));
           }
           return Success(ctx->CreateTerm(f, {}));
         } else if (ctx->IsRegisteredMetaVariable(id)) {
           return Success(ctx->LookupMetaVariable(id));
         } else {
-          return Error<Term>(LELA_MSG("Error in atomic_term"));
+          return Error<Term>(LIMBO_MSG("Error in atomic_term"));
         }
       });
     }
-    return Error<Action<Term>>(LELA_MSG("Expected a declared variable/name/function identifier"));
+    return Error<Action<Term>>(LIMBO_MSG("Expected a declared variable/name/function identifier"));
   }
 
   // term --> x
@@ -315,7 +315,7 @@ class Parser {
         for (;;) {
           Result<Action<Term>> t = term();
           if (!t) {
-            return Error<Action<Term>>(LELA_MSG("Expected argument term"), t);
+            return Error<Action<Term>>(LIMBO_MSG("Expected argument term"), t);
           }
           args.push_back(t.val);
           if (Is(Tok(), Token::kComma)) {
@@ -325,7 +325,7 @@ class Parser {
             Advance();
             break;
           } else {
-            return Error<Action<Term>>(LELA_MSG("Expected comma ',' or closing parenthesis ')'"));
+            return Error<Action<Term>>(LIMBO_MSG("Expected comma ',' or closing parenthesis ')'"));
           }
         }
       }
@@ -337,7 +337,7 @@ class Parser {
         } else if (ctx->IsRegisteredFunction(id)) {
           Symbol f = ctx->LookupFunction(id);
           if (static_cast<size_t>(f.arity()) != args_a.size()) {
-            return Error<Term>(LELA_MSG("Wrong number of arguments for "+ id));
+            return Error<Term>(LIMBO_MSG("Wrong number of arguments for "+ id));
           }
           Term::Vector args;
           for (const Action<Term>& a : args_a) {
@@ -345,45 +345,45 @@ class Parser {
             if (t) {
               args.push_back(t.val);
             } else {
-              return Error<Term>(LELA_MSG("Expected argument term"), t);
+              return Error<Term>(LIMBO_MSG("Expected argument term"), t);
             }
           }
           return Success(ctx->CreateTerm(f, args));
         } else if (ctx->IsRegisteredMetaVariable(id)) {
           return Success(ctx->LookupMetaVariable(id));
         } else {
-          return Error<Term>(LELA_MSG("Error in term"));
+          return Error<Term>(LIMBO_MSG("Error in term"));
         }
       });
     }
-    return Error<Action<Term>>(LELA_MSG("Expected a declared variable/name/function identifier"));
+    return Error<Action<Term>>(LIMBO_MSG("Expected a declared variable/name/function identifier"));
   }
 
   // literal --> term [ '==' | '!=' ] term
   Result<Action<std::unique_ptr<Literal>>> literal() {
     Result<Action<Term>> lhs = term();
     if (!lhs) {
-      return Error<Action<std::unique_ptr<Literal>>>(LELA_MSG("Expected a lhs term"), lhs);
+      return Error<Action<std::unique_ptr<Literal>>>(LIMBO_MSG("Expected a lhs term"), lhs);
     }
     bool pos;
     if (Is(Tok(), Token::kEquality) || Is(Tok(), Token::kInequality)) {
       pos = Is(Tok(), Token::kEquality);
       Advance();
     } else {
-      return Error<Action<std::unique_ptr<Literal>>>(LELA_MSG("Expected equality or inequality '=='/'!='"));
+      return Error<Action<std::unique_ptr<Literal>>>(LIMBO_MSG("Expected equality or inequality '=='/'!='"));
     }
     Result<Action<Term>> rhs = term();
     if (!rhs) {
-      return Error<Action<std::unique_ptr<Literal>>>(LELA_MSG("Expected rhs term"), rhs);
+      return Error<Action<std::unique_ptr<Literal>>>(LIMBO_MSG("Expected rhs term"), rhs);
     }
     return Success<Action<std::unique_ptr<Literal>>>([lhs_a = lhs.val, pos, rhs_a = rhs.val](Context* ctx) {
       Result<Term> lhs = lhs_a.Run(ctx);
       if (!lhs) {
-        return Error<std::unique_ptr<Literal>>(LELA_MSG("Expected a lhs term"), lhs);
+        return Error<std::unique_ptr<Literal>>(LIMBO_MSG("Expected a lhs term"), lhs);
       }
       Result<Term> rhs = rhs_a.Run(ctx);
       if (!rhs) {
-        return Error<std::unique_ptr<Literal>>(LELA_MSG("Expected a rhs term"), rhs);
+        return Error<std::unique_ptr<Literal>>(LIMBO_MSG("Expected a rhs term"), rhs);
       }
       Literal a = pos ? Literal::Eq(lhs.val, rhs.val) : Literal::Neq(lhs.val, rhs.val);
       return Success(std::unique_ptr<Literal>(new Literal(a)));
@@ -405,12 +405,12 @@ class Parser {
       Advance();
       Result<Action<Formula::Ref>> alpha = primary_formula();
       if (!alpha) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected a primary formula within negation"), alpha);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected a primary formula within negation"), alpha);
       }
       return Success<Action<Formula::Ref>>([this, alpha_a = alpha.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected a primary formula within negation"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected a primary formula within negation"), alpha);
         }
         return Success<Formula::Ref>(Formula::Factory::Not(std::move(alpha.val)));
       });
@@ -420,20 +420,20 @@ class Parser {
       Advance();
       Result<Action<Term>> x = atomic_term();
       if (!x) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected variable in quantifier"), x);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected variable in quantifier"), x);
       }
       Result<Action<Formula::Ref>> alpha = primary_formula();
       if (!alpha) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected primary formula within quantifier"), alpha);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected primary formula within quantifier"), alpha);
       }
       return Success<Action<Formula::Ref>>([this, ex, x_a = x.val, alpha_a = alpha.val](Context* ctx) {
         Result<Term> x = x_a.Run(ctx);
         if (!x || !x.val.variable()) {
-          return Error<Formula::Ref>(LELA_MSG("Expected variable in quantifier"), x);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected variable in quantifier"), x);
         }
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected primary formula within quantifier"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected primary formula within quantifier"), alpha);
         }
         return Success(ex ? Formula::Factory::Exists(x.val, std::move(alpha.val))
                           : Formula::Factory::Not(
@@ -444,26 +444,26 @@ class Parser {
       bool know = Is(Tok(), Token::kKnow);
       Advance();
       if (!Is(Tok(), Token::kLess)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected '<'"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected '<'"));
       }
       Advance();
       if (!Is(Tok(), Token::kUint)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected split level integer"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected split level integer"));
       }
       const Formula::split_level k = std::stoi(Tok().val.str());
       Advance();
       if (!Is(Tok(), Token::kGreater)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected '>'"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected '>'"));
       }
       Advance();
       Result<Action<Formula::Ref>> alpha = primary_formula();
       if (!alpha) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected primary formula within modality"), alpha);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected primary formula within modality"), alpha);
       }
       return Success<Action<Formula::Ref>>([this, know, k, alpha_a = alpha.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected primary formula within modality"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected primary formula within modality"), alpha);
         }
         if (know) {
           return Success(Formula::Factory::Know(k, std::move(alpha.val)));
@@ -475,47 +475,47 @@ class Parser {
     if (Is(Tok(), Token::kBel)) {
       Advance();
       if (!Is(Tok(), Token::kLess)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected '<'"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected '<'"));
       }
       Advance();
       if (!Is(Tok(), Token::kUint)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected first split level integer"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected first split level integer"));
       }
       const Formula::split_level k = std::stoi(Tok().val.str());
       Advance();
       if (!Is(Tok(), Token::kComma)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected ','"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected ','"));
       }
       Advance();
       if (!Is(Tok(), Token::kUint)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected second split level integer"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected second split level integer"));
       }
       const Formula::split_level l = std::stoi(Tok().val.str());
       Advance();
       if (!Is(Tok(), Token::kGreater)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected '>'"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected '>'"));
       }
       Advance();
       Result<Action<Formula::Ref>> alpha = primary_formula();
       if (!alpha) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected primary formula within modality"), alpha);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected primary formula within modality"), alpha);
       }
       if (!Is(Tok(), Token::kDoubleRArrow)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected conditional belief arrow"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected conditional belief arrow"));
       }
       Advance();
       Result<Action<Formula::Ref>> beta = primary_formula();
       if (!beta) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected primary formula within modality"), beta);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected primary formula within modality"), beta);
       }
       return Success<Action<Formula::Ref>>([this, k, l, alpha_a = alpha.val, beta_a = beta.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected primary formula within modality"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected primary formula within modality"), alpha);
         }
         Result<Formula::Ref> beta = beta_a.Run(ctx);
         if (!beta) {
-          return Error<Formula::Ref>(LELA_MSG("Expected primary formula within modality"), beta);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected primary formula within modality"), beta);
         }
         return Success(Formula::Factory::Bel(k, l, std::move(alpha.val), std::move(beta.val)));
       });
@@ -524,12 +524,12 @@ class Parser {
       Advance();
       Result<Action<Formula::Ref>> alpha = primary_formula();
       if (!alpha) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected primary formula within modality"), alpha);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected primary formula within modality"), alpha);
       }
       return Success<Action<Formula::Ref>>([this, alpha_a = alpha.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected primary formula within modality"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected primary formula within modality"), alpha);
         }
         return Success(Formula::Factory::Guarantee(std::move(alpha.val)));
       });
@@ -538,16 +538,16 @@ class Parser {
       Advance();
       Result<Action<Formula::Ref>> alpha = formula();
       if (!alpha) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected formula within brackets"), alpha);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected formula within brackets"), alpha);
       }
       if (!Is(Tok(), Token::kRightParen)) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected closing right parenthesis ')'"));
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected closing right parenthesis ')'"));
       }
       Advance();
       return Success<Action<Formula::Ref>>([this, alpha_a = alpha.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected formula within brackets"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected formula within brackets"), alpha);
         }
         return Success(std::move(alpha.val));
       });
@@ -558,19 +558,19 @@ class Parser {
       Advance();
       return Success<Action<Formula::Ref>>([this, id](Context* ctx) {
         if (!ctx->IsRegisteredFormula(id)) {
-          return Error<Formula::Ref>(LELA_MSG("Undefined formula abbreviation "+ id));
+          return Error<Formula::Ref>(LIMBO_MSG("Undefined formula abbreviation "+ id));
         }
         return Success(ctx->LookupFormula(id).Clone());
       });
     }
     Result<Action<std::unique_ptr<Literal>>> a = literal();
     if (!a) {
-      return Error<Action<Formula::Ref>>(LELA_MSG("Expected literal"), a);
+      return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected literal"), a);
     }
     return Success<Action<Formula::Ref>>([this, a_a = a.val](Context* ctx) {
       Result<std::unique_ptr<Literal>> a = a_a.Run(ctx);
       if (!a) {
-        return Error<Formula::Ref>(LELA_MSG("Expected literal"), a);
+        return Error<Formula::Ref>(LIMBO_MSG("Expected literal"), a);
       }
       return Success(Formula::Factory::Atomic(Clause{*a.val}));
     });
@@ -580,22 +580,22 @@ class Parser {
   Result<Action<Formula::Ref>> conjunctive_formula() {
     Result<Action<Formula::Ref>> alpha = primary_formula();
     if (!alpha) {
-      return Error<Action<Formula::Ref>>(LELA_MSG("Expected left conjunctive formula"), alpha);
+      return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected left conjunctive formula"), alpha);
     }
     while (Is(Tok(), Token::kAnd)) {
       Advance();
       Result<Action<Formula::Ref>> beta = primary_formula();
       if (!beta) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected left conjunctive formula"), beta);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected left conjunctive formula"), beta);
       }
       alpha = Success<Action<Formula::Ref>>([alpha_a = alpha.val, beta_a = beta.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected left conjunctive formula"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected left conjunctive formula"), alpha);
         }
         Result<Formula::Ref> beta = beta_a.Run(ctx);
         if (!beta) {
-          return Error<Formula::Ref>(LELA_MSG("Expected right conjunctive formula"), beta);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected right conjunctive formula"), beta);
         }
         return Success(Formula::Factory::Not(Formula::Factory::Or(Formula::Factory::Not(std::move(alpha.val)),
                                                                   Formula::Factory::Not(std::move(beta.val)))));
@@ -608,22 +608,22 @@ class Parser {
   Result<Action<Formula::Ref>> disjunctive_formula() {
     Result<Action<Formula::Ref>> alpha = conjunctive_formula();
     if (!alpha) {
-      return Error<Action<Formula::Ref>>(LELA_MSG("Expected left argument conjunctive formula"), alpha);
+      return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected left argument conjunctive formula"), alpha);
     }
     while (Is(Tok(), Token::kOr)) {
       Advance();
       Result<Action<Formula::Ref>> beta = conjunctive_formula();
       if (!beta) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected right argument conjunctive formula"), beta);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected right argument conjunctive formula"), beta);
       }
       alpha = Success<Action<Formula::Ref>>([alpha_a = alpha.val, beta_a = beta.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected left argument conjunctive formula"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected left argument conjunctive formula"), alpha);
         }
         Result<Formula::Ref> beta = beta_a.Run(ctx);
         if (!beta) {
-          return Error<Formula::Ref>(LELA_MSG("Expected right argument conjunctive formula"), beta);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected right argument conjunctive formula"), beta);
         }
         return Success(Formula::Factory::Or(std::move(alpha.val), std::move(beta.val)));
       });
@@ -636,22 +636,22 @@ class Parser {
   Result<Action<Formula::Ref>> implication_formula() {
     Result<Action<Formula::Ref>> alpha = disjunctive_formula();
     if (!alpha) {
-      return Error<Action<Formula::Ref>>(LELA_MSG("Expected left argument disjunctive formula"), alpha);
+      return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected left argument disjunctive formula"), alpha);
     }
     if (Is(Tok(), Token::kRArrow)) {
       Advance();
       Result<Action<Formula::Ref>> beta = disjunctive_formula();
       if (!beta) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected right argument disjunctive formula"), beta);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected right argument disjunctive formula"), beta);
       }
       alpha = Success<Action<Formula::Ref>>([this, alpha_a = alpha.val, beta_a = beta.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected left argument disjunctive formula"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected left argument disjunctive formula"), alpha);
         }
         Result<Formula::Ref> beta = beta_a.Run(ctx);
         if (!beta) {
-          return Error<Formula::Ref>(LELA_MSG("Expected right argument disjunctive formula"), beta);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected right argument disjunctive formula"), beta);
         }
         return Success(Formula::Factory::Or(Formula::Factory::Not(std::move(alpha.val)), std::move(beta.val)));
       });
@@ -664,22 +664,22 @@ class Parser {
   Result<Action<Formula::Ref>> equivalence_formula() {
     Result<Action<Formula::Ref>> alpha = implication_formula();
     if (!alpha) {
-      return Error<Action<Formula::Ref>>(LELA_MSG("Expected left argument implication formula"), alpha);
+      return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected left argument implication formula"), alpha);
     }
     if (Is(Tok(), Token::kLRArrow)) {
       Advance();
       Result<Action<Formula::Ref>> beta = implication_formula();
       if (!beta) {
-        return Error<Action<Formula::Ref>>(LELA_MSG("Expected right argument implication formula"), beta);
+        return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected right argument implication formula"), beta);
       }
       alpha = Success<Action<Formula::Ref>>([alpha_a = alpha.val, beta_a = beta.val](Context* ctx) {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<Formula::Ref>(LELA_MSG("Expected left argument implication formula"), alpha);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected left argument implication formula"), alpha);
         }
         Result<Formula::Ref> beta = beta_a.Run(ctx);
         if (!beta) {
-          return Error<Formula::Ref>(LELA_MSG("Expected right argument implication formula"), beta);
+          return Error<Formula::Ref>(LIMBO_MSG("Expected right argument implication formula"), beta);
         }
         Formula::Ref lr = Formula::Factory::Or(Formula::Factory::Not(alpha.val->Clone()), beta.val->Clone());
         Formula::Ref rl = Formula::Factory::Or(Formula::Factory::Not(std::move(alpha.val)), std::move(beta.val));
@@ -698,26 +698,26 @@ class Parser {
   // kb_formula --> KB : formula
   Result<Action<>> kb_formula() {
     if (!Is(Tok(), Token::kKB)) {
-      return Unapplicable<Action<>>(LELA_MSG("Expected 'KB'"));
+      return Unapplicable<Action<>>(LIMBO_MSG("Expected 'KB'"));
     }
     Advance();
     if (!Is(Tok(), Token::kColon)) {
-      return Error<Action<>>(LELA_MSG("Expected ':'"));
+      return Error<Action<>>(LIMBO_MSG("Expected ':'"));
     }
     Advance();
     Result<Action<Formula::Ref>> alpha = formula();
     if (!alpha) {
-      return Error<Action<>>(LELA_MSG("Expected KB formula"), alpha);
+      return Error<Action<>>(LIMBO_MSG("Expected KB formula"), alpha);
     }
     return Success<Action<>>([this, alpha_a = alpha.val](Context* ctx) {
       Result<Formula::Ref> alpha = alpha_a.Run(ctx);
       if (!alpha) {
-        return Error<>(LELA_MSG("Expected KB formula"), alpha);
+        return Error<>(LIMBO_MSG("Expected KB formula"), alpha);
       }
       if (ctx->AddToKb(*alpha.val)) {
         return Success<>();
       } else {
-        return Error<>(LELA_MSG("Couldn't add formula to KB; is it proper+ "
+        return Error<>(LIMBO_MSG("Couldn't add formula to KB; is it proper+ "
                                 "(i.e., its NF must be a universally quantified clause)?"));
       }
     });
@@ -727,15 +727,15 @@ class Parser {
   Result<Action<Formula::Ref>> subjective_formula() {
     Result<Action<Formula::Ref>> alpha = formula();
     if (!alpha) {
-      return Error<Action<Formula::Ref>>(LELA_MSG("Expected subjective formula"), alpha);
+      return Error<Action<Formula::Ref>>(LIMBO_MSG("Expected subjective formula"), alpha);
     }
     return Success<Action<Formula::Ref>>([this, alpha_a = alpha.val](Context* ctx) {
       Result<Formula::Ref> alpha = alpha_a.Run(ctx);
       if (!alpha) {
-        return Error<Formula::Ref>(LELA_MSG("Expected subjective formula"), alpha);
+        return Error<Formula::Ref>(LIMBO_MSG("Expected subjective formula"), alpha);
       }
       if (!alpha.val->subjective()) {
-        return Error<Formula::Ref>(LELA_MSG("Expected subjective formula "
+        return Error<Formula::Ref>(LIMBO_MSG("Expected subjective formula "
                                               "(i.e., no functions outside of modal operators; "
                                               "probably caused by missing brackets)"));
       }
@@ -751,25 +751,25 @@ class Parser {
           Is(Tok(), Token::kIdentifier)) &&
         !Is(Tok(), Token::kAssert) &&
         !Is(Tok(), Token::kRefute)) {
-      return Unapplicable<Action<>>(LELA_MSG("Expected 'Query', 'Assert', or 'Refute'"));
+      return Unapplicable<Action<>>(LIMBO_MSG("Expected 'Query', 'Assert', or 'Refute'"));
     }
     const bool is_query = !Is(Tok(), Token::kAssert) && !Is(Tok(), Token::kRefute);
     const bool is_assert = Is(Tok(), Token::kAssert);
     if (Is(Tok(), Token::kQuery) || Is(Tok(), Token::kAssert) || Is(Tok(), Token::kRefute)) {
       Advance();
       if (!Is(Tok(), Token::kColon)) {
-        return Error<Action<>>(LELA_MSG("Expected ':'"));
+        return Error<Action<>>(LIMBO_MSG("Expected ':'"));
       }
       Advance();
       }
     Result<Action<Formula::Ref>> alpha = subjective_formula();
     if (!alpha) {
-      return Error<Action<>>(LELA_MSG("Expected query/assertion/refutation subjective_formula"), alpha);
+      return Error<Action<>>(LIMBO_MSG("Expected query/assertion/refutation subjective_formula"), alpha);
     }
     return Success<Action<>>([this, alpha_a = alpha.val, is_query, is_assert](Context* ctx) {
       Result<Formula::Ref> alpha = alpha_a.Run(ctx);
       if (!alpha) {
-        return Error<>(LELA_MSG("Expected query/assertion/refutation subjective_formula"), alpha);
+        return Error<>(LIMBO_MSG("Expected query/assertion/refutation subjective_formula"), alpha);
       }
       const bool r = ctx->Query(*alpha.val);
       if (is_query) {
@@ -778,9 +778,9 @@ class Parser {
         return Success<>();
       } else {
         std::stringstream ss;
-        using lela::format::operator<<;
+        using limbo::format::operator<<;
         ss << (is_assert ? "Assertion" : "Refutation") << " of " << *alpha.val << " failed";
-        return Error<>(LELA_MSG(ss.str()));
+        return Error<>(LIMBO_MSG(ss.str()));
       }
     });
   }
@@ -803,23 +803,23 @@ class Parser {
         Advance();
         Result<Action<Term>> t = term();
         if (!t) {
-          return Error<Action<IdTerms>>(LELA_MSG("Expected argument term"), t);
+          return Error<Action<IdTerms>>(LIMBO_MSG("Expected argument term"), t);
         }
         ts.push_back(std::move(t.val));
       } while (Is(Tok(), Token::kComma));
     }
     if (!Is(Tok(), Token::kRArrow)) {
-      return Error<Action<IdTerms>>(LELA_MSG("Expected right arrow '->'"));
+      return Error<Action<IdTerms>>(LIMBO_MSG("Expected right arrow '->'"));
     }
     Advance();
     if (!Is(Tok(), Token::kIdentifier)) {
-      return Error<Action<IdTerms>>(LELA_MSG("Expected sort identifier"));
+      return Error<Action<IdTerms>>(LIMBO_MSG("Expected sort identifier"));
     }
     const std::string sort = Tok().val.str();
     Advance();
     return Success<Action<IdTerms>>([this, id, sort_id = sort, ts_a = ts](Context* ctx) {
       if (!ctx->IsRegisteredSort(sort_id)) {
-        return Error<IdTerms>(LELA_MSG("Sort "+ sort_id +" is not registered"));
+        return Error<IdTerms>(LIMBO_MSG("Sort "+ sort_id +" is not registered"));
       }
       Symbol::Sort sort = ctx->LookupSort(sort_id);
       std::vector<Term> ts;
@@ -830,10 +830,10 @@ class Parser {
         for (const Action<Term>& t_a : ts_a) {
           Result<Term> t = t_a.Run(ctx);
           if (!t) {
-            return Error<IdTerms>(LELA_MSG("Expected term in range"), t);
+            return Error<IdTerms>(LIMBO_MSG("Expected term in range"), t);
           }
           if (t.val.sort() != sort) {
-            return Error<IdTerms>(LELA_MSG("Term in range is not of sort "+ sort_id));
+            return Error<IdTerms>(LIMBO_MSG("Term in range is not of sort "+ sort_id));
           }
           ts.push_back(t.val);
         }
@@ -845,27 +845,27 @@ class Parser {
   // if_else --> If formula block [ Else block ]
   Result<Action<>> if_else() {
     if (!Is(Tok(), Token::kIf)) {
-      return Unapplicable<Action<>>(LELA_MSG("Expected 'If'"));
+      return Unapplicable<Action<>>(LIMBO_MSG("Expected 'If'"));
     }
     Advance();
     Result<Action<IdTerms>> bind = bind_meta_variables();
     if (!bind) {
-      return Error<Action<>>(LELA_MSG("Expected bind_meta_variables"), bind);
+      return Error<Action<>>(LIMBO_MSG("Expected bind_meta_variables"), bind);
     }
     Result<Action<Formula::Ref>> alpha = formula();
     if (!alpha) {
-      return Error<Action<>>(LELA_MSG("Expected formula in if_else"), alpha);
+      return Error<Action<>>(LIMBO_MSG("Expected formula in if_else"), alpha);
     }
     Result<Action<>> if_block = block();
     if (!if_block) {
-      return Error<Action<>>(LELA_MSG("Expected if block in if_else"), if_block);
+      return Error<Action<>>(LIMBO_MSG("Expected if block in if_else"), if_block);
     }
     Result<Action<>> else_block;
     if (Is(Tok(), Token::kElse)) {
       Advance();
       else_block = block();
       if (!else_block) {
-        return Error<Action<>>(LELA_MSG("Expected else block in if_else"), else_block);
+        return Error<Action<>>(LIMBO_MSG("Expected else block in if_else"), else_block);
       }
     } else {
       else_block = Success<Action<>>([](Context* ctx) { return Success<>(); });
@@ -881,7 +881,7 @@ class Parser {
           ctx->RegisterMetaVariable(id, t);
           Result<Formula::Ref> alpha = alpha_a.Run(ctx);
           if (!alpha) {
-            return Error<>(LELA_MSG("Expected condition subjective_formula"), alpha);
+            return Error<>(LIMBO_MSG("Expected condition subjective_formula"), alpha);
           }
           if (ctx->Query(*alpha.val)) {
             cond = true;
@@ -892,7 +892,7 @@ class Parser {
       } else {
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<>(LELA_MSG("Expected condition subjective_formula"), alpha);
+          return Error<>(LIMBO_MSG("Expected condition subjective_formula"), alpha);
         }
         cond = ctx->Query(*alpha.val);
       }
@@ -906,7 +906,7 @@ class Parser {
         r = else_block_a.Run(ctx);
       }
       if (!r) {
-        return Error<>(LELA_MSG("Expected block in if_else"), r);
+        return Error<>(LIMBO_MSG("Expected block in if_else"), r);
       }
       return r;
     });
@@ -915,27 +915,27 @@ class Parser {
   // while_loop --> While formula block [ Else block ]
   Result<Action<>> while_loop() {
     if (!Is(Tok(), Token::kWhile)) {
-      return Unapplicable<Action<>>(LELA_MSG("Expected 'While'"));
+      return Unapplicable<Action<>>(LIMBO_MSG("Expected 'While'"));
     }
     Advance();
     Result<Action<IdTerms>> bind = bind_meta_variables();
     if (!bind) {
-      return Error<Action<>>(LELA_MSG("Expected bind_meta_variables"), bind);
+      return Error<Action<>>(LIMBO_MSG("Expected bind_meta_variables"), bind);
     }
     Result<Action<Formula::Ref>> alpha = formula();
     if (!alpha) {
-      return Error<Action<>>(LELA_MSG("Expected formula in while_loop"), alpha);
+      return Error<Action<>>(LIMBO_MSG("Expected formula in while_loop"), alpha);
     }
     Result<Action<>> while_block = block();
     if (!while_block) {
-      return Error<Action<>>(LELA_MSG("Expected if block in while_else"), while_block);
+      return Error<Action<>>(LIMBO_MSG("Expected if block in while_else"), while_block);
     }
     Result<Action<>> else_block;
     if (Is(Tok(), Token::kElse)) {
       Advance();
       else_block = block();
       if (!else_block) {
-        return Error<Action<>>(LELA_MSG("Expected else block in while_loop"), else_block);
+        return Error<Action<>>(LIMBO_MSG("Expected else block in while_loop"), else_block);
       }
     } else {
       else_block = Success<Action<>>([](Context* ctx) { return Success<>(); });
@@ -953,7 +953,7 @@ class Parser {
             ctx->RegisterMetaVariable(id, t);
             Result<Formula::Ref> alpha = alpha_a.Run(ctx);
             if (!alpha) {
-              return Error<>(LELA_MSG("Expected condition subjective_formula"), alpha);
+              return Error<>(LIMBO_MSG("Expected condition subjective_formula"), alpha);
             }
             if (ctx->Query(*alpha.val)) {
               cond = true;
@@ -964,7 +964,7 @@ class Parser {
         } else {
           Result<Formula::Ref> alpha = alpha_a.Run(ctx);
           if (!alpha) {
-            return Error<>(LELA_MSG("Expected condition subjective_formula"), alpha);
+            return Error<>(LIMBO_MSG("Expected condition subjective_formula"), alpha);
           }
           cond = ctx->Query(*alpha.val);
         }
@@ -975,7 +975,7 @@ class Parser {
             ctx->UnregisterMetaVariable(id);
           }
           if (!r) {
-            return Error<>(LELA_MSG("Expected block in while_loop"), r);
+            return Error<>(LIMBO_MSG("Expected block in while_loop"), r);
           }
         } else {
           break;
@@ -984,7 +984,7 @@ class Parser {
       if (!once) {
         Result<> r = else_block_a.Run(ctx);
         if (!r) {
-          return Error<>(LELA_MSG("Expected block in while_loop"), r);
+          return Error<>(LIMBO_MSG("Expected block in while_loop"), r);
         }
       }
       return Success<>();
@@ -994,27 +994,27 @@ class Parser {
   // for_loop --> For formula block [ Else block ]
   Result<Action<>> for_loop() {
     if (!Is(Tok(), Token::kFor)) {
-      return Unapplicable<Action<>>(LELA_MSG("Expected 'For'"));
+      return Unapplicable<Action<>>(LIMBO_MSG("Expected 'For'"));
     }
     Advance();
     Result<Action<IdTerms>> bind = bind_meta_variables();
     if (!bind) {
-      return Error<Action<>>(LELA_MSG("Expected bind_meta_variables"), bind);
+      return Error<Action<>>(LIMBO_MSG("Expected bind_meta_variables"), bind);
     }
     Result<Action<Formula::Ref>> alpha = formula();
     if (!alpha) {
-      return Error<Action<>>(LELA_MSG("Expected formula in for_loop"), alpha);
+      return Error<Action<>>(LIMBO_MSG("Expected formula in for_loop"), alpha);
     }
     Result<Action<>> for_block = block();
     if (!for_block) {
-      return Error<Action<>>(LELA_MSG("Expected if block in for_else"), for_block);
+      return Error<Action<>>(LIMBO_MSG("Expected if block in for_else"), for_block);
     }
     Result<Action<>> else_block;
     if (Is(Tok(), Token::kElse)) {
       Advance();
       else_block = block();
       if (!else_block) {
-        return Error<Action<>>(LELA_MSG("Expected else block in for_loop"), else_block);
+        return Error<Action<>>(LIMBO_MSG("Expected else block in for_loop"), else_block);
       }
     } else {
       else_block = Success<Action<>>([](Context* ctx) { return Success<>(); });
@@ -1024,21 +1024,21 @@ class Parser {
       Result<IdTerms> bind = bind_a.Run(ctx);
       const std::string id = bind.val.first;
       if (id.empty()) {
-        return Error<>(LELA_MSG("Expected meta variable id"));
+        return Error<>(LIMBO_MSG("Expected meta variable id"));
       }
       bool once = false;
       for (Term t : bind.val.second) {
         ctx->RegisterMetaVariable(id, t);
         Result<Formula::Ref> alpha = alpha_a.Run(ctx);
         if (!alpha) {
-          return Error<>(LELA_MSG("Expected condition subjective_formula"), alpha);
+          return Error<>(LIMBO_MSG("Expected condition subjective_formula"), alpha);
         }
         if (ctx->Query(*alpha.val)) {
           once = true;
           Result<> r = for_block_a.Run(ctx);
           if (!r) {
             ctx->UnregisterMetaVariable(id);
-            return Error<>(LELA_MSG("Expected block in for_loop"), r);
+            return Error<>(LIMBO_MSG("Expected block in for_loop"), r);
           }
         }
         ctx->UnregisterMetaVariable(id);
@@ -1046,7 +1046,7 @@ class Parser {
       if (!once) {
         Result<> r = else_block_a.Run(ctx);
         if (!r) {
-          return Error<>(LELA_MSG("Expected block in for_loop"), r);
+          return Error<>(LIMBO_MSG("Expected block in for_loop"), r);
         }
       }
       return Success<>();
@@ -1056,26 +1056,26 @@ class Parser {
   // abbreviation --> let identifier := formula
   Result<Action<>> abbreviation() {
     if (!Is(Tok(), Token::kLet)) {
-      return Unapplicable<Action<>>(LELA_MSG("Expected abbreviation operator 'let'"));
+      return Unapplicable<Action<>>(LIMBO_MSG("Expected abbreviation operator 'let'"));
     }
     Advance();
     if (!Is(Tok(), Token::kIdentifier)) {
-      return Error<Action<>>(LELA_MSG("Expected fresh identifier"));
+      return Error<Action<>>(LIMBO_MSG("Expected fresh identifier"));
     }
     const std::string id = Tok().val.str();
     Advance();
     if (!Is(Tok(), Token::kAssign)) {
-      return Error<Action<>>(LELA_MSG("Expected assignment operator ':='"));
+      return Error<Action<>>(LIMBO_MSG("Expected assignment operator ':='"));
     }
     Advance();
     Result<Action<Formula::Ref>> alpha = formula();
     if (!alpha) {
-      return Error<Action<>>(LELA_MSG("Expected formula"), alpha);
+      return Error<Action<>>(LIMBO_MSG("Expected formula"), alpha);
     }
     return Success<Action<>>([this, id, alpha_a = alpha.val](Context* ctx) {
       Result<Formula::Ref> alpha = alpha_a.Run(ctx);
       if (!alpha) {
-        return Error<>(LELA_MSG("Expected formula"), alpha);
+        return Error<>(LIMBO_MSG("Expected formula"), alpha);
       }
       ctx->RegisterFormula(id, *alpha.val);
       return Success<>();
@@ -1085,20 +1085,20 @@ class Parser {
   // call --> Call id
   Result<Action<>> call() {
     if (!Is(Tok(), Token::kCall)) {
-      return Unapplicable<Action<>>(LELA_MSG("Expected 'Call'"));
+      return Unapplicable<Action<>>(LIMBO_MSG("Expected 'Call'"));
     }
     Advance();
     if (!Is(Tok(), Token::kColon)) {
-      return Error<Action<>>(LELA_MSG("Expected ':'"));
+      return Error<Action<>>(LIMBO_MSG("Expected ':'"));
     }
     Advance();
     if (!Is(Tok(), Token::kIdentifier)) {
-      return Error<Action<>>(LELA_MSG("Expected meta variable in for_loop"));
+      return Error<Action<>>(LIMBO_MSG("Expected meta variable in for_loop"));
     }
     const std::string id = Tok().val.str();
     Advance();
     if (!Is(Tok(), Token::kLeftParen)) {
-      return Error<Action<>>(LELA_MSG("Expected opening parentheses '('"));
+      return Error<Action<>>(LIMBO_MSG("Expected opening parentheses '('"));
     }
     std::vector<Action<Term>> ts;
     do {
@@ -1108,12 +1108,12 @@ class Parser {
       }
       Result<Action<Term>> t = term();
       if (!t) {
-        return Error<Action<>>(LELA_MSG("Expected argument"), t);
+        return Error<Action<>>(LIMBO_MSG("Expected argument"), t);
       }
       ts.push_back(std::move(t.val));
     } while (Is(Tok(), Token::kComma));
     if (!Is(Tok(), Token::kRightParen)) {
-      return Error<Action<>>(LELA_MSG("Expected closing parentheses '('"));
+      return Error<Action<>>(LIMBO_MSG("Expected closing parentheses '('"));
     }
     Advance();
     return Success<Action<>>([this, id, ts_as = ts](Context* ctx) {
@@ -1132,7 +1132,7 @@ class Parser {
     if (!Is(Tok(), Token::kBegin)) {
       Result<Action<>> r = branch();
       if (!r) {
-        return Error<Action<>>(LELA_MSG("Expected branch in block"), r);
+        return Error<Action<>>(LIMBO_MSG("Expected branch in block"), r);
       }
       return r;
     } else {
@@ -1147,7 +1147,7 @@ class Parser {
         } else {
           Result<Action<>> r = branch();
           if (!r) {
-            return Error<Action<>>(LELA_MSG("Expected branch in block"), r);
+            return Error<Action<>>(LIMBO_MSG("Expected branch in block"), r);
           }
           a += r.val;
         }
@@ -1166,10 +1166,10 @@ class Parser {
       if (r) {
         return r;
       } else if (r.applied()) {
-        return Error<Action<>>(LELA_MSG("Error in branch"), r);
+        return Error<Action<>>(LIMBO_MSG("Error in branch"), r);
       }
     }
-    return Unapplicable<Action<>>(LELA_MSG("No rule applicable in branch"));
+    return Unapplicable<Action<>>(LIMBO_MSG("No rule applicable in branch"));
   }
 
   // start --> branch
@@ -1180,31 +1180,31 @@ class Parser {
       const Result<Action<>> r = branch();
       if (!r) {
         std::stringstream ss;
-        using lela::format::operator<<;
+        using limbo::format::operator<<;
         ss << Tok(0) << " " << Tok(1) << " " << Tok(2) << "...";
-        return Error<Action<>>(LELA_MSG("Error in start with unparsed input "+ ss.str()), r);
+        return Error<Action<>>(LIMBO_MSG("Error in start with unparsed input "+ ss.str()), r);
       }
       a += r.val;
     }
     return Success<Action<>>(std::move(a));
   }
 
-  bool Is(const lela::internal::Maybe<Token>& symbol, Token::Id id) const {
+  bool Is(const limbo::internal::Maybe<Token>& symbol, Token::Id id) const {
     return symbol && symbol.val.id() == id;
   }
 
   template<typename UnaryPredicate>
-  bool Is(const lela::internal::Maybe<Token>& symbol, Token::Id id, UnaryPredicate p) const {
+  bool Is(const limbo::internal::Maybe<Token>& symbol, Token::Id id, UnaryPredicate p) const {
     return symbol && symbol.val.id() == id && p(symbol.val.str());
   }
 
-  lela::internal::Maybe<Token> Tok(size_t n = 0) const {
+  limbo::internal::Maybe<Token> Tok(size_t n = 0) const {
     auto it = begin();
     for (size_t i = 0; i < n && it != end_; ++i) {
       assert(begin() != end());
       ++it;
     }
-    return it != end_ ? lela::internal::Just(*it) : lela::internal::Nothing;
+    return it != end_ ? limbo::internal::Just(*it) : limbo::internal::Nothing;
   }
 
   void Advance(size_t n = 1) {
@@ -1247,7 +1247,7 @@ const char* Parser<ForwardIt, Context>::kCausesLabel       = " causes: ";
 
 }  // namespace pdl
 }  // namespace format
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_FORMAT_PDL_PARSER_H_
+#endif  // LIMBO_FORMAT_PDL_PARSER_H_
 
diff --git a/src/lela/formula.h b/src/limbo/formula.h
similarity index 99%
rename from src/lela/formula.h
rename to src/limbo/formula.h
index 5af5e82703d901574a4a831ff1a41749dd686cb4..02b7b8e4cf0c0d1d5c962b9c114d5b9001f6af6e 100644
--- a/src/lela/formula.h
+++ b/src/limbo/formula.h
@@ -9,8 +9,8 @@
 // NF() rectifies a formula (that is, renames variables to make sure no variable
 // occurs freely and bound or bound by two different quantifiers).
 
-#ifndef LELA_FORMULA_H_
-#define LELA_FORMULA_H_
+#ifndef LIMBO_FORMULA_H_
+#define LIMBO_FORMULA_H_
 
 #include <cassert>
 
@@ -21,13 +21,13 @@
 #include <unordered_map>
 #include <vector>
 
-#include <lela/clause.h>
+#include <limbo/clause.h>
 
-#include <lela/internal/iter.h>
-#include <lela/internal/ints.h>
-#include <lela/internal/maybe.h>
+#include <limbo/internal/iter.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/maybe.h>
 
-namespace lela {
+namespace limbo {
 
 class Formula {
  public:
@@ -885,7 +885,7 @@ inline const class Formula::Guarantee& Formula::as_guarantee() const {
   return *dynamic_cast<const class Guarantee*>(this);
 }
 
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_FORMULA_H_
+#endif  // LIMBO_FORMULA_H_
 
diff --git a/src/lela/grounder.h b/src/limbo/grounder.h
similarity index 98%
rename from src/lela/grounder.h
rename to src/limbo/grounder.h
index 432cae4815533bb004511e8606125a9149aa6b4d..94582de8044619328ee55b87de50c4becc2c1628 100644
--- a/src/lela/grounder.h
+++ b/src/limbo/grounder.h
@@ -22,8 +22,8 @@
 // Symbol::Factory. Returning such temporary names for later re-use may avoid
 // bloating up the setups.
 
-#ifndef LELA_GROUNDER_H_
-#define LELA_GROUNDER_H_
+#ifndef LIMBO_GROUNDER_H_
+#define LIMBO_GROUNDER_H_
 
 #include <cassert>
 
@@ -35,16 +35,16 @@
 #include <unordered_set>
 #include <utility>
 
-#include <lela/clause.h>
-#include <lela/formula.h>
-#include <lela/setup.h>
+#include <limbo/clause.h>
+#include <limbo/formula.h>
+#include <limbo/setup.h>
 
-#include <lela/internal/hash.h>
-#include <lela/internal/ints.h>
-#include <lela/internal/iter.h>
-#include <lela/internal/maybe.h>
+#include <limbo/internal/hash.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/iter.h>
+#include <limbo/internal/maybe.h>
 
-namespace lela {
+namespace limbo {
 
 class Grounder {
  public:
@@ -663,7 +663,7 @@ class Grounder {
   internal::Maybe<Setup> setup_;
 };
 
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_GROUNDER_H_
+#endif  // LIMBO_GROUNDER_H_
 
diff --git a/src/lela/internal/bloom.h b/src/limbo/internal/bloom.h
similarity index 89%
rename from src/lela/internal/bloom.h
rename to src/limbo/internal/bloom.h
index 9b0ee5ec7725b73e3f8c260aa43834a54b9d277a..07063ffc46b9e912cb515c65300cbb4786e83a1b 100644
--- a/src/lela/internal/bloom.h
+++ b/src/limbo/internal/bloom.h
@@ -21,15 +21,15 @@
 // We take the byte pairs 1,2 and 3,4 and 5,6 and 7,8 and consider the 16bit
 // number formed by each of them as a single hash.
 
-#ifndef LELA_INTERNAL_BLOOM_H_
-#define LELA_INTERNAL_BLOOM_H_
+#ifndef LIMBO_INTERNAL_BLOOM_H_
+#define LIMBO_INTERNAL_BLOOM_H_
 
 #include <functional>
 
-#include <lela/internal/hash.h>
-#include <lela/internal/ints.h>
+#include <limbo/internal/hash.h>
+#include <limbo/internal/ints.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 class BloomFilter {
@@ -133,22 +133,22 @@ class BloomSet {
 };
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
 
 namespace std {
 
 template<>
-struct equal_to<lela::internal::BloomFilter> {
-  bool operator()(const lela::internal::BloomFilter& a, const lela::internal::BloomFilter& b) const { return a == b; }
+struct equal_to<limbo::internal::BloomFilter> {
+  bool operator()(const limbo::internal::BloomFilter& a, const limbo::internal::BloomFilter& b) const { return a == b; }
 };
 
 template<typename T>
-struct equal_to<lela::internal::BloomSet<T>> {
-  bool operator()(const lela::internal::BloomSet<T>& a, const lela::internal::BloomSet<T>& b) const { return a == b; }
+struct equal_to<limbo::internal::BloomSet<T>> {
+  bool operator()(const limbo::internal::BloomSet<T>& a, const limbo::internal::BloomSet<T>& b) const { return a == b; }
 };
 
 }  // namespace std
 
-#endif  // LELA_INTERNAL_BLOOM_H_
+#endif  // LIMBO_INTERNAL_BLOOM_H_
 
diff --git a/src/lela/internal/compar.h b/src/limbo/internal/compar.h
similarity index 93%
rename from src/lela/internal/compar.h
rename to src/limbo/internal/compar.h
index 495909cb922e941252f5e454a8194f803f8bb640..03b985438ee9398c2c0b7fcc18bb9d7a4d4fa318 100644
--- a/src/lela/internal/compar.h
+++ b/src/limbo/internal/compar.h
@@ -6,12 +6,12 @@
 // containers. Currently only few are in use, the previous prototypes made
 // much heavier use of specific sorting.
 
-#ifndef LELA_INTERNAL_COMPAR_H_
-#define LELA_INTERNAL_COMPAR_H_
+#ifndef LIMBO_INTERNAL_COMPAR_H_
+#define LIMBO_INTERNAL_COMPAR_H_
 
 #include <algorithm>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 template<class T>
@@ -75,7 +75,7 @@ struct LexicographicComparator<Compar> {
 };
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_INTERNAL_COMPAR_H_
+#endif  // LIMBO_INTERNAL_COMPAR_H_
 
diff --git a/src/lela/internal/hash.h b/src/limbo/internal/hash.h
similarity index 93%
rename from src/lela/internal/hash.h
rename to src/limbo/internal/hash.h
index 066573d001d21affa99d0361999b176180a2064e..1c0019545ac4fa3cbfc6ca32902dc20009b91795 100644
--- a/src/lela/internal/hash.h
+++ b/src/limbo/internal/hash.h
@@ -4,12 +4,12 @@
 //
 // Some fast hash functions.
 
-#ifndef LELA_INTERNAL_HASH_H_
-#define LELA_INTERNAL_HASH_H_
+#ifndef LIMBO_INTERNAL_HASH_H_
+#define LIMBO_INTERNAL_HASH_H_
 
-#include <lela/internal/ints.h>
+#include <limbo/internal/ints.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 typedef u32 hash32_t;
@@ -116,7 +116,7 @@ hash64_t murmur64a_hash(const T& x, hash64_t seed = 0) {
 }
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_INTERNAL_HASH_H_
+#endif  // LIMBO_INTERNAL_HASH_H_
 
diff --git a/src/lela/internal/hashset.h b/src/limbo/internal/hashset.h
similarity index 97%
rename from src/lela/internal/hashset.h
rename to src/limbo/internal/hashset.h
index 70a842608b5a58603a6c33b14707fd6c01968a11..5deaafbd834cf2ff20fd462273711a480307b3c9 100644
--- a/src/lela/internal/hashset.h
+++ b/src/limbo/internal/hashset.h
@@ -4,8 +4,8 @@
 //
 // A closed hash set.
 
-#ifndef LELA_INTERNAL_HASHSET_H_
-#define LELA_INTERNAL_HASHSET_H_
+#ifndef LIMBO_INTERNAL_HASHSET_H_
+#define LIMBO_INTERNAL_HASHSET_H_
 
 #include <cstdlib>
 #include <cstring>
@@ -16,11 +16,11 @@
 #include <utility>
 #include <vector>
 
-#include <lela/internal/hash.h>
-#include <lela/internal/ints.h>
-#include <lela/internal/iter.h>
+#include <limbo/internal/hash.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/iter.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 template<typename T, typename Hash = std::hash<T>, typename Equal = std::equal_to<T>>
@@ -357,7 +357,7 @@ class HashSet {
 };
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_INTERNAL_HASHSET_H_
+#endif  // LIMBO_INTERNAL_HASHSET_H_
 
diff --git a/src/lela/internal/intmap.h b/src/limbo/internal/intmap.h
similarity index 93%
rename from src/lela/internal/intmap.h
rename to src/limbo/internal/intmap.h
index 19fc3a4825b318e27ecc0779126dd37719b1ca10..be088dbc336ad472953093a4eee2652e0e0d0acc 100644
--- a/src/lela/internal/intmap.h
+++ b/src/limbo/internal/intmap.h
@@ -8,18 +8,18 @@
 // default is T(), which amounts to 0 for integers and false for bools; the
 // value can be changed by set_null_value().
 
-#ifndef LELA_INTERNAL_INTMAP_H_
-#define LELA_INTERNAL_INTMAP_H_
+#ifndef LIMBO_INTERNAL_INTMAP_H_
+#define LIMBO_INTERNAL_INTMAP_H_
 
 #include <algorithm>
 #include <iterator>
 #include <utility>
 #include <vector>
 
-#include <lela/internal/iter.h>
-#include <lela/internal/ints.h>
+#include <limbo/internal/iter.h>
+#include <limbo/internal/ints.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 template<typename Key, typename T>
@@ -106,7 +106,7 @@ class IntMap : public std::vector<T> {
 };
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_INTERNAL_INTMAP_H_
+#endif  // LIMBO_INTERNAL_INTMAP_H_
 
diff --git a/src/lela/internal/ints.h b/src/limbo/internal/ints.h
similarity index 79%
rename from src/lela/internal/ints.h
rename to src/limbo/internal/ints.h
index 90951a26c65cf11e356a6ad9d2cf3d62bc44b1bd..6a0908a192f7c95ada3a45355b471a3a9da52327 100644
--- a/src/lela/internal/ints.h
+++ b/src/limbo/internal/ints.h
@@ -4,12 +4,12 @@
 //
 // Integer typedefs.
 
-#ifndef LELA_INTERNAL_INTS_H_
-#define LELA_INTERNAL_INTS_H_
+#ifndef LIMBO_INTERNAL_INTS_H_
+#define LIMBO_INTERNAL_INTS_H_
 
 #include <cstdint>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 typedef std::int8_t i8;
@@ -23,7 +23,7 @@ typedef std::uintptr_t uptr_t;
 typedef std::intptr_t iptr_t;
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_INTERNAL_INTS_H_
+#endif  // LIMBO_INTERNAL_INTS_H_
 
diff --git a/src/lela/internal/iter.h b/src/limbo/internal/iter.h
similarity index 98%
rename from src/lela/internal/iter.h
rename to src/limbo/internal/iter.h
index b4b003ed86eefeaa88dc8f8c719e01d645eb8b93..277071414faaa08cf50559da0e5d9581790f3409 100644
--- a/src/lela/internal/iter.h
+++ b/src/limbo/internal/iter.h
@@ -7,17 +7,17 @@
 // Maybe boost provides the same iterators and we should move to boost (this set
 // of iterators evolved somewhat).
 
-#ifndef LELA_INTERNAL_ITER_H_
-#define LELA_INTERNAL_ITER_H_
+#ifndef LIMBO_INTERNAL_ITER_H_
+#define LIMBO_INTERNAL_ITER_H_
 
 #include <iterator>
 #include <type_traits>
 #include <utility>
 
-#include <lela/internal/ints.h>
-#include <lela/internal/traits.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/traits.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 // Wrapper for operator*() and operator++(int).
@@ -437,7 +437,7 @@ inline joined_iterators<InputIt1, InputIt2> join_ranges(Range1 r1, Range2 r2) {
 }
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_INTERNAL_ITER_H_
+#endif  // LIMBO_INTERNAL_ITER_H_
 
diff --git a/src/lela/internal/maybe.h b/src/limbo/internal/maybe.h
similarity index 93%
rename from src/lela/internal/maybe.h
rename to src/limbo/internal/maybe.h
index 68d4aa7764483a86c08bf1b1ada0d36612f2f34f..fec639334a6d564480366255c24bbfefa45c6f0e 100644
--- a/src/lela/internal/maybe.h
+++ b/src/limbo/internal/maybe.h
@@ -8,15 +8,15 @@
 //
 // To handle Maybe<std::unique_ptr<T>> we use std::forward(). Is that correct?
 
-#ifndef LELA_INTERNAL_MAYBE_H_
-#define LELA_INTERNAL_MAYBE_H_
+#ifndef LIMBO_INTERNAL_MAYBE_H_
+#define LIMBO_INTERNAL_MAYBE_H_
 
 #include <cassert>
 
 #include <memory>
 #include <utility>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 template<typename T>
@@ -62,7 +62,7 @@ Maybe<typename std::remove_cv<typename std::remove_reference<T>::type>::type> Ju
 }
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_INTERNAL_MAYBE_H_
+#endif  // LIMBO_INTERNAL_MAYBE_H_
 
diff --git a/src/lela/internal/traits.h b/src/limbo/internal/traits.h
similarity index 93%
rename from src/lela/internal/traits.h
rename to src/limbo/internal/traits.h
index db971bc5576f57b6cdfd6e613c6482f743d8bfac..dc012c3be11ef0e3d6869b887a8140422bf40ba8 100644
--- a/src/lela/internal/traits.h
+++ b/src/limbo/internal/traits.h
@@ -4,13 +4,13 @@
 //
 // Traits, mostly to extract and identify the arguments of functors.
 
-#ifndef LELA_INTERNAL_TRAITS_H_
-#define LELA_INTERNAL_TRAITS_H_
+#ifndef LIMBO_INTERNAL_TRAITS_H_
+#define LIMBO_INTERNAL_TRAITS_H_
 
 #include <tuple>
 #include <type_traits>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 // first_type<T, U>::type is T::type if it exists, and U::type else.
@@ -64,8 +64,8 @@ struct remove_const_ref {
 };
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_INTERNAL_TRAITS_H_
+#endif  // LIMBO_INTERNAL_TRAITS_H_
 
 
diff --git a/src/lela/kb.h b/src/limbo/kb.h
similarity index 97%
rename from src/lela/kb.h
rename to src/limbo/kb.h
index 778d178183e9373172109072e8aba2fe177f7ce5..bbd9a8542c094759303e0600f10dc1c14ae3d2d4 100644
--- a/src/lela/kb.h
+++ b/src/limbo/kb.h
@@ -23,26 +23,26 @@
 // Queries are not subject to any syntactic restrictions. Technically, they are
 // evaluated using variants of Levesque's representation theorem.
 
-#ifndef LELA_KB_H_
-#define LELA_KB_H_
+#ifndef LIMBO_KB_H_
+#define LIMBO_KB_H_
 
 #include <cassert>
 
 #include <utility>
 #include <vector>
 
-#include <lela/clause.h>
-#include <lela/formula.h>
-#include <lela/grounder.h>
-#include <lela/literal.h>
-#include <lela/solver.h>
-#include <lela/term.h>
+#include <limbo/clause.h>
+#include <limbo/formula.h>
+#include <limbo/grounder.h>
+#include <limbo/literal.h>
+#include <limbo/solver.h>
+#include <limbo/term.h>
 
-#include <lela/internal/ints.h>
-#include <lela/internal/iter.h>
-#include <lela/internal/maybe.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/iter.h>
+#include <limbo/internal/maybe.h>
 
-namespace lela {
+namespace limbo {
 
 class KnowledgeBase {
  public:
@@ -350,7 +350,7 @@ class KnowledgeBase {
   bool spheres_changed_ = false;
 };
 
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_KB_H_
+#endif  // LIMBO_KB_H_
 
diff --git a/src/lela/literal.h b/src/limbo/literal.h
similarity index 93%
rename from src/lela/literal.h
rename to src/limbo/literal.h
index 76162357b250b74438bca56230701a21d5adf8ba..b9d1961fd4ec9d9705e85d8c8678b220c0de2dd4 100644
--- a/src/lela/literal.h
+++ b/src/limbo/literal.h
@@ -15,8 +15,8 @@
 // Due to the memory-wise lightweight representation of terms, copying or
 // comparing literals is very fast.
 
-#ifndef LELA_LITERAL_H_
-#define LELA_LITERAL_H_
+#ifndef LIMBO_LITERAL_H_
+#define LIMBO_LITERAL_H_
 
 #include <cassert>
 
@@ -24,12 +24,12 @@
 #include <functional>
 #include <utility>
 
-#include <lela/term.h>
+#include <limbo/term.h>
 
-#include <lela/internal/ints.h>
-#include <lela/internal/maybe.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/maybe.h>
 
-namespace lela {
+namespace limbo {
 
 class Literal {
  public:
@@ -176,22 +176,22 @@ struct Literal::LhsHash {
   internal::hash32_t operator()(const Literal a) const { return a.lhs().hash(); }
 };
 
-}  // namespace lela
+}  // namespace limbo
 
 
 namespace std {
 
 template<>
-struct hash<lela::Literal> {
-  lela::internal::hash32_t operator()(const lela::Literal a) const { return a.hash(); }
+struct hash<limbo::Literal> {
+  limbo::internal::hash32_t operator()(const limbo::Literal a) const { return a.hash(); }
 };
 
 template<>
-struct equal_to<lela::Literal> {
-  bool operator()(const lela::Literal a, const lela::Literal b) const { return a == b; }
+struct equal_to<limbo::Literal> {
+  bool operator()(const limbo::Literal a, const limbo::Literal b) const { return a == b; }
 };
 
 }  // namespace std
 
-#endif  // LELA_LITERAL_H_
+#endif  // LIMBO_LITERAL_H_
 
diff --git a/src/lela/setup.h b/src/limbo/setup.h
similarity index 98%
rename from src/lela/setup.h
rename to src/limbo/setup.h
index f269aa96e6240fde5fc41b3351cd8452909497b5..cf610e3dce6d19aea69465f4076ea2bf39c2d80a 100644
--- a/src/lela/setup.h
+++ b/src/limbo/setup.h
@@ -55,8 +55,8 @@
 // reasons, but because it may likely lead to complications with the linked
 // structure of setups and therefore hints at a programming error.
 
-#ifndef LELA_SETUP_H_
-#define LELA_SETUP_H_
+#ifndef LIMBO_SETUP_H_
+#define LIMBO_SETUP_H_
 
 #include <cassert>
 
@@ -65,15 +65,15 @@
 #include <utility>
 #include <vector>
 
-#include <lela/clause.h>
-#include <lela/literal.h>
-#include <lela/term.h>
+#include <limbo/clause.h>
+#include <limbo/literal.h>
+#include <limbo/term.h>
 
-#include <lela/internal/ints.h>
-#include <lela/internal/iter.h>
-#include <lela/internal/maybe.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/iter.h>
+#include <limbo/internal/maybe.h>
 
-namespace lela {
+namespace limbo {
 
 class Setup {
  public:
@@ -491,7 +491,7 @@ class Setup {
 #endif
 };
 
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_SETUP_H_
+#endif  // LIMBO_SETUP_H_
 
diff --git a/src/lela/solver.h b/src/limbo/solver.h
similarity index 98%
rename from src/lela/solver.h
rename to src/limbo/solver.h
index 076ff6a301a83bb382e40c5e61b0862800fc8e06..2a96770027024de91e69bbbb8ddbe9d301e1538f 100644
--- a/src/lela/solver.h
+++ b/src/limbo/solver.h
@@ -43,24 +43,24 @@
 // the Consistent() method is that it is perhaps less confusing and less prone
 // to typos and shares some code with the sound Entails().
 
-#ifndef LELA_SOLVER_H_
-#define LELA_SOLVER_H_
+#ifndef LIMBO_SOLVER_H_
+#define LIMBO_SOLVER_H_
 
 #include <cassert>
 
 #include <iterator>
 #include <list>
 
-#include <lela/formula.h>
-#include <lela/grounder.h>
-#include <lela/literal.h>
-#include <lela/setup.h>
-#include <lela/term.h>
+#include <limbo/formula.h>
+#include <limbo/grounder.h>
+#include <limbo/literal.h>
+#include <limbo/setup.h>
+#include <limbo/term.h>
 
-#include <lela/internal/ints.h>
-#include <lela/internal/maybe.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/maybe.h>
 
-namespace lela {
+namespace limbo {
 
 class Solver {
  public:
@@ -474,7 +474,7 @@ next_split:
   Grounder grounder_;
 };
 
-}  // namespace lela
+}  // namespace limbo
 
-#endif  // LELA_SOLVER_H_
+#endif  // LIMBO_SOLVER_H_
 
diff --git a/src/lela/term.h b/src/limbo/term.h
similarity index 94%
rename from src/lela/term.h
rename to src/limbo/term.h
index eea4a6a481e511daeab7b651d124c2a74e4451e6..a307cec52cfb71ca8c2fff8a8478132e035c44f5 100644
--- a/src/lela/term.h
+++ b/src/limbo/term.h
@@ -26,8 +26,8 @@
 // certain operations on Terms and Literals can be expressed as bitwise
 // operations on their integer representations.
 
-#ifndef LELA_TERM_H_
-#define LELA_TERM_H_
+#ifndef LIMBO_TERM_H_
+#define LIMBO_TERM_H_
 
 #include <cassert>
 
@@ -38,12 +38,12 @@
 #include <utility>
 #include <vector>
 
-#include <lela/internal/hash.h>
-#include <lela/internal/intmap.h>
-#include <lela/internal/ints.h>
-#include <lela/internal/maybe.h>
+#include <limbo/internal/hash.h>
+#include <limbo/internal/intmap.h>
+#include <limbo/internal/ints.h>
+#include <limbo/internal/maybe.h>
 
-namespace lela {
+namespace limbo {
 
 template<typename T>
 struct Singleton {
@@ -217,7 +217,7 @@ struct Term::Data {
 
   internal::hash32_t hash() const {
     internal::hash32_t h = symbol.hash();
-    for (const lela::Term t : args) {
+    for (const limbo::Term t : args) {
       h ^= t.hash();
     }
     return h;
@@ -416,32 +416,32 @@ void Term::Traverse(UnaryFunction f) const {
   }
 }
 
-}  // namespace lela
+}  // namespace limbo
 
 
 namespace std {
 
 template<>
-struct hash<lela::Symbol> {
-  lela::internal::hash32_t operator()(const lela::Symbol s) const { return s.hash(); }
+struct hash<limbo::Symbol> {
+  limbo::internal::hash32_t operator()(const limbo::Symbol s) const { return s.hash(); }
 };
 
 template<>
-struct equal_to<lela::Symbol> {
-  bool operator()(const lela::Symbol a, const lela::Symbol b) const { return a == b; }
+struct equal_to<limbo::Symbol> {
+  bool operator()(const limbo::Symbol a, const limbo::Symbol b) const { return a == b; }
 };
 
 template<>
-struct hash<lela::Term> {
-  lela::internal::hash32_t operator()(const lela::Term t) const { return t.hash(); }
+struct hash<limbo::Term> {
+  limbo::internal::hash32_t operator()(const limbo::Term t) const { return t.hash(); }
 };
 
 template<>
-struct equal_to<lela::Term> {
-  bool operator()(const lela::Term a, const lela::Term b) const { return a == b; }
+struct equal_to<limbo::Term> {
+  bool operator()(const limbo::Term a, const limbo::Term b) const { return a == b; }
 };
 
 }  // namespace std
 
-#endif  // LELA_TERM_H_
+#endif  // LIMBO_TERM_H_
 
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index b5948b9631a9c4e32f78fab37088d3f19c8eea2a..aa7db4f4166892ebf48f9c2a3c4a999395c2bdb8 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -5,7 +5,7 @@ include_directories (${GTEST_INCLUDE_DIRS})
 if (GTest_FOUND)
     foreach (test hash iter hashset intmap term bloom literal clause setup formula syntax grounder solver kb)
             add_executable (${test} ${test}.cc)
-            target_link_libraries (${test} LINK_PUBLIC lela ${GTEST_BOTH_LIBRARIES} pthread)
+            target_link_libraries (${test} LINK_PUBLIC limbo ${GTEST_BOTH_LIBRARIES} pthread)
             add_test (NAME ${test} COMMAND ${test})
     endforeach ()
 endif ()
diff --git a/tests/bloom.cc b/tests/bloom.cc
index 588dfb2e75ac81f37f8d07db403c4c2ee1d9bec7..62d10d4c7335a2dac56a1d409dda4d396d3a4d59 100644
--- a/tests/bloom.cc
+++ b/tests/bloom.cc
@@ -3,14 +3,14 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/term.h>
-#include <lela/internal/bloom.h>
-#include <lela/format/output.h>
+#include <limbo/term.h>
+#include <limbo/internal/bloom.h>
+#include <limbo/format/output.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
-using namespace lela::format;
+using namespace limbo::format;
 
 TEST(BloomFilterTest, Subset_Contains) {
   Symbol::Factory& sf = *Symbol::Factory::Instance();
@@ -97,5 +97,5 @@ TEST(BloomFilterTest, hash) {
 }
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/clause.cc b/tests/clause.cc
index c15ac652c4ac596b7b9330f1cd9bb87ff131ba4a..f72abaa70ba577d7ac4408f9a523ed42beb716f8 100644
--- a/tests/clause.cc
+++ b/tests/clause.cc
@@ -3,13 +3,13 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/clause.h>
-#include <lela/internal/maybe.h>
-#include <lela/format/output.h>
+#include <limbo/clause.h>
+#include <limbo/internal/maybe.h>
+#include <limbo/format/output.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
+using namespace limbo::format;
 
 struct EqSubstitute {
   EqSubstitute(Term pre, Term post) : pre_(pre), post_(post) {}
@@ -356,5 +356,5 @@ TEST(ClauseTest, Subsumes3) {
   EXPECT_TRUE(Clause{Literal::Neq(P,T)}.Subsumes(Clause{Literal::Neq(P,T)}));
 }
 
-}  // namespace lela
+}  // namespace limbo
  
diff --git a/tests/formula.cc b/tests/formula.cc
index ca35c35d21487d6fe83431a0edf50ebadcd486bb..21c111a6b2d8d69feaaa8e56a90d862055cff284 100644
--- a/tests/formula.cc
+++ b/tests/formula.cc
@@ -3,14 +3,14 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/formula.h>
-#include <lela/format/output.h>
-#include <lela/format/cpp/syntax.h>
+#include <limbo/formula.h>
+#include <limbo/format/output.h>
+#include <limbo/format/cpp/syntax.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
-using namespace lela::format::cpp;
+using namespace limbo::format;
+using namespace limbo::format::cpp;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
@@ -120,5 +120,5 @@ TEST(Formula, NF) {
   }
 }
 
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/grounder.cc b/tests/grounder.cc
index 108d3f35539cfc154e99ee05d444592e3765ecca..9c445b9e5251161483b9788aaeed22b7f235eee5 100644
--- a/tests/grounder.cc
+++ b/tests/grounder.cc
@@ -5,13 +5,13 @@
 
 #include <unordered_set>
 
-#include <lela/formula.h>
-#include <lela/grounder.h>
-#include <lela/format/output.h>
+#include <limbo/formula.h>
+#include <limbo/grounder.h>
+#include <limbo/format/output.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
+using namespace limbo::format;
 
 std::unordered_set<Clause> unique(const Setup& s) {
   std::unordered_set<Clause> set;
@@ -63,7 +63,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Eq(n1,n1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [n1=n1]. The clause is valid and hence skipped.
     EXPECT_EQ(unique_length(s), 0);
     EXPECT_TRUE(s.Consistent());
@@ -72,7 +72,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Neq(n1,n1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [n1/=n1]. The clause is invalid and hence boiled
     // down to [].
     EXPECT_EQ(unique_length(s), 1);
@@ -82,7 +82,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Eq(x1, x1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [n1=n1]. The clause is valid and hence skipped.
     EXPECT_EQ(unique_length(s), 0);
     EXPECT_TRUE(s.Consistent());
@@ -91,7 +91,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Neq(x1, x1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [n1/=n1]. The clause is invalid and hence boiled
     // down to [].
     EXPECT_EQ(unique_length(s), 1);
@@ -101,7 +101,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Eq(n1, x1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [n1=n1], [n3=n1]. The first clause is valid and
     // hence skipped. The second is invalid and hence boiled down to [].
     EXPECT_EQ(unique_length(s), 1);
@@ -111,7 +111,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Neq(n1, x1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [n1/=n1], [n3/=n1]. The second clause is valid and
     // hence skipped. The first is invalid and hence boiled down to [].
     EXPECT_EQ(unique_length(s), 1);
@@ -121,7 +121,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Eq(x1, x2)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [n1=n1], [n3=2], [n1=n3], [n3=n1]. The former two
     // clauses are valid and hence skipped. The latter ones are invalid and
     // hence boiled down to [].
@@ -132,7 +132,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Neq(x1, x1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [n1/=n1]. The clause is invalid and hence boiled
     // down to [].
     EXPECT_EQ(unique_length(s), 1);
@@ -143,10 +143,10 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Eq(tf.CreateTerm(a, {}), x1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [a=n1], [a=n2], which yields [].
     //EXPECT_EQ(unique_length(s), 2);  // the second clause is replaced with []
-    //const_cast<lela::Setup&>(s).Minimize();
+    //const_cast<limbo::Setup&>(s).Minimize();
     EXPECT_EQ(unique_length(s), 1);
     EXPECT_FALSE(s.Consistent());
   }
@@ -154,7 +154,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Eq(tf.CreateTerm(a, {}), n1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [a=n1].
     EXPECT_EQ(unique_length(s), 1);
     EXPECT_TRUE(s.Consistent());
@@ -163,11 +163,11 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Eq(tf.CreateTerm(f, {n1}), x1)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [f(n1)=n1)], [f(n1)=n3]. The clauses unify and
     // yield [].
     //EXPECT_EQ(unique_length(s), 2);
-    //const_cast<lela::Setup&>(s).Minimize();
+    //const_cast<limbo::Setup&>(s).Minimize();
     EXPECT_EQ(unique_length(s), 1);
     EXPECT_FALSE(s.Consistent());
   }
@@ -175,10 +175,10 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Neq(tf.CreateTerm(f, {n1}), x2)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [f(n1)/=n1)], [f(n1)/=n3], [f(n1)/=n4].
     //EXPECT_EQ(unique_length(s), 3);
-    //const_cast<lela::Setup&>(s).Minimize();
+    //const_cast<limbo::Setup&>(s).Minimize();
     EXPECT_EQ(unique_length(s), 3);
     EXPECT_TRUE(s.Consistent());
   }
@@ -186,11 +186,11 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Eq(tf.CreateTerm(h, {n1,x2}), x3)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [h(n1,nX)=nY] for X=1,2,3 and Y=4,5. The clauses
     // unify and yield [].
     //EXPECT_EQ(unique_length(s), 3+1);  // after [h(n1,nX)=n4] for all nX have been added, adding any [h(n1,nX)=n5] yields []
-    //const_cast<lela::Setup&>(s).Minimize();
+    //const_cast<limbo::Setup&>(s).Minimize();
     EXPECT_EQ(unique_length(s), 1);
     EXPECT_FALSE(s.Consistent());
   }
@@ -198,10 +198,10 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
   {
     Grounder g(&sf, &tf);
     g.AddClause(Clause({Literal::Neq(tf.CreateTerm(h, {n1,x2}), x3)}));
-    const lela::Setup& s = g.Ground();
+    const limbo::Setup& s = g.Ground();
     // Grounding should be [h(n1,nX)=nY] for X=1,2,3 and Y=4,5.
     //EXPECT_EQ(unique_length(s), 3*2);
-    //const_cast<lela::Setup&>(s).Minimize();
+    //const_cast<limbo::Setup&>(s).Minimize();
     EXPECT_EQ(unique_length(s), 3*2);
     EXPECT_TRUE(s.Consistent());
   }
@@ -213,7 +213,7 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
 //    g.PrepareForQuery(Formula::Factory::Exists(x2, *Formula::Factory::Atomic({Literal::Eq(x2, x2)}))->NF(&sf, &tf));
 //    g.PrepareForQuery(Formula::Factory::Exists(x3, *Formula::Factory::Atomic({Literal::Eq(x3, x3)}))->NF(&sf, &tf));
 //    g.PrepareForQuery(Formula::Factory::Exists(x4, *Formula::Factory::Atomic({Literal::Eq(x4, x4)}))->NF(&sf, &tf));
-//    const lela::Setup& s = g.Ground();
+//    const limbo::Setup& s = g.Ground();
 //    EXPECT_EQ(unique_length(s), 2);
 //  }
 
@@ -530,5 +530,5 @@ TEST(GrounderTest, Ground_SplitNames_iterated) {
   }
 }
 
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/hash.cc b/tests/hash.cc
index c6b346d3384ff6f921ca6b7aacb9b2275668de96..24161d0f6291c742e927d4fa1c7f8ab0b26fff79 100644
--- a/tests/hash.cc
+++ b/tests/hash.cc
@@ -5,9 +5,9 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/internal/hash.h>
+#include <limbo/internal/hash.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 TEST(HashTest, hash) {
@@ -31,5 +31,5 @@ TEST(HashTest, hash) {
 }
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/hashset.cc b/tests/hashset.cc
index 6f2adeea218e9a0af768d228fcd276ef77f3e1a8..cc5b82848c06cac053a08103cad40408745dd2ae 100644
--- a/tests/hashset.cc
+++ b/tests/hashset.cc
@@ -5,9 +5,9 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/internal/hashset.h>
+#include <limbo/internal/hashset.h>
 
-#include <lela/format/output.h>
+#include <limbo/format/output.h>
 
 struct Value {
   Value() = default;
@@ -19,9 +19,9 @@ struct Value {
 
 std::ostream& operator<<(std::ostream& os, Value i) { return std::cout << i.x; }
 
-using namespace lela::format;
+using namespace limbo::format;
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 TEST(HashSetTest, main) {
@@ -67,5 +67,5 @@ TEST(HashSetTest, main) {
 }
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/intmap.cc b/tests/intmap.cc
index 9aae6ac574a3d1608db5406f975e91d27067500b..9b0e44802bc4133ba0f57f915a64ecf716df46d9 100644
--- a/tests/intmap.cc
+++ b/tests/intmap.cc
@@ -3,9 +3,9 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/internal/intmap.h>
+#include <limbo/internal/intmap.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 template<typename T>
@@ -51,5 +51,5 @@ TEST(IntMapTest, general) {
 }
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/iter.cc b/tests/iter.cc
index f2c902da7742e09413bb2aacb51ede7f060195fb..81263bff5e5877624b143241acb4bcca42717238 100644
--- a/tests/iter.cc
+++ b/tests/iter.cc
@@ -3,9 +3,9 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/internal/iter.h>
+#include <limbo/internal/iter.h>
 
-namespace lela {
+namespace limbo {
 namespace internal {
 
 struct Int {
@@ -161,5 +161,5 @@ TEST(IterTest, join_ranges) {
 }
 
 }  // namespace internal
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/kb.cc b/tests/kb.cc
index bd27e651975547ac9dcafff26d4eaf42a220d5af..fe44cc3e867af92f4aac335580a459c65e2c8226 100644
--- a/tests/kb.cc
+++ b/tests/kb.cc
@@ -3,14 +3,14 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/kb.h>
-#include <lela/format/output.h>
-#include <lela/format/cpp/syntax.h>
+#include <limbo/kb.h>
+#include <limbo/format/output.h>
+#include <limbo/format/cpp/syntax.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
-using namespace lela::format::cpp;
+using namespace limbo::format;
+using namespace limbo::format::cpp;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
@@ -74,5 +74,5 @@ TEST(KnowledgeBaseTest, ECAI2016Sound_NoGuarantee) {
   EXPECT_TRUE(kb.Entails(*Formula::Factory::Bel(1, 1, *(Italian != T), *(Veggie != T))));
 }
 
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/literal.cc b/tests/literal.cc
index 503b8b58f9ccfd5b086bad6daf6c749b8636e1f0..e23157c26aaf4ccfc047895d1a6451b1646de935 100644
--- a/tests/literal.cc
+++ b/tests/literal.cc
@@ -3,12 +3,12 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/literal.h>
-#include <lela/format/output.h>
+#include <limbo/literal.h>
+#include <limbo/format/output.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
+using namespace limbo::format;
 
 TEST(LiteralTest, general) {
   Symbol::Factory& sf = *Symbol::Factory::Instance();
@@ -93,5 +93,5 @@ TEST(LiteralTest, general) {
   EXPECT_TRUE(Literal::Valid(Literal::Neq(f1, n1), Literal::Neq(f1, n2)));
 }
 
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/setup.cc b/tests/setup.cc
index 93a0e0d2713dd35d7e9bd7b3010096ac78ecc5a1..514999e9136d42d4c141f5acff2c2aa12dcb45af 100644
--- a/tests/setup.cc
+++ b/tests/setup.cc
@@ -6,12 +6,12 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/setup.h>
-#include <lela/format/output.h>
+#include <limbo/setup.h>
+#include <limbo/format/output.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
+using namespace limbo::format;
 
 template<typename T>
 size_t dist(T r) { return std::distance(r.begin(), r.end()); }
@@ -29,9 +29,9 @@ TEST(SetupTest, Subsumes_Consistent_clauses) {
   const Term gm = tf.CreateTerm(Symbol::Factory::CreateFunction(4, s1, 1), {m});
 
   {
-    lela::Setup s0;
-    EXPECT_EQ(s0.AddClause(Clause({Literal::Neq(fn,n), Literal::Eq(fm,m)})), lela::Setup::kOk);
-    EXPECT_EQ(s0.AddClause(Clause({Literal::Neq(gn,n), Literal::Eq(gm,m)})), lela::Setup::kOk);
+    limbo::Setup s0;
+    EXPECT_EQ(s0.AddClause(Clause({Literal::Neq(fn,n), Literal::Eq(fm,m)})), limbo::Setup::kOk);
+    EXPECT_EQ(s0.AddClause(Clause({Literal::Neq(gn,n), Literal::Eq(gm,m)})), limbo::Setup::kOk);
     EXPECT_TRUE(s0.Consistent());
     EXPECT_TRUE(s0.LocallyConsistent({fm,fn}));
     for (size_t i : s0.clauses()) {
@@ -40,11 +40,11 @@ TEST(SetupTest, Subsumes_Consistent_clauses) {
     EXPECT_FALSE(s0.Subsumes(Clause({Literal::Eq(a,m), Literal::Eq(a,n)})));
 
     {
-      lela::Setup& s1 = s0;
-      EXPECT_EQ(s1.AddClause(Clause({Literal::Neq(fn,n), Literal::Eq(fm,m)})), lela::Setup::kOk);
-      EXPECT_EQ(s1.AddClause(Clause({Literal::Neq(gn,n), Literal::Eq(gm,m)})), lela::Setup::kOk);
-      EXPECT_EQ(s1.AddClause(Clause({Literal::Neq(a,n), Literal::Eq(fn,n)})), lela::Setup::kOk);
-      EXPECT_EQ(s1.AddClause(Clause({Literal::Neq(a,n), Literal::Eq(gn,n)})), lela::Setup::kOk);
+      limbo::Setup& s1 = s0;
+      EXPECT_EQ(s1.AddClause(Clause({Literal::Neq(fn,n), Literal::Eq(fm,m)})), limbo::Setup::kOk);
+      EXPECT_EQ(s1.AddClause(Clause({Literal::Neq(gn,n), Literal::Eq(gm,m)})), limbo::Setup::kOk);
+      EXPECT_EQ(s1.AddClause(Clause({Literal::Neq(a,n), Literal::Eq(fn,n)})), limbo::Setup::kOk);
+      EXPECT_EQ(s1.AddClause(Clause({Literal::Neq(a,n), Literal::Eq(gn,n)})), limbo::Setup::kOk);
       EXPECT_EQ(dist(s1.clauses()), 6);
       s1.Minimize();
       EXPECT_EQ(dist(s1.clauses()), 4);
@@ -55,8 +55,8 @@ TEST(SetupTest, Subsumes_Consistent_clauses) {
       EXPECT_FALSE(s1.Subsumes(Clause({Literal::Eq(a,m), Literal::Eq(a,n)})));
 
       {
-        lela::Setup& s2 = s1;
-        EXPECT_EQ(s2.AddClause(Clause({Literal::Eq(a,m), Literal::Eq(a,n)})), lela::Setup::kOk);
+        limbo::Setup& s2 = s1;
+        EXPECT_EQ(s2.AddClause(Clause({Literal::Eq(a,m), Literal::Eq(a,n)})), limbo::Setup::kOk);
         EXPECT_EQ(dist(s2.clauses()), 5);
         EXPECT_TRUE(!s2.Consistent());
         for (const size_t i : s2.clauses()) {
@@ -64,8 +64,8 @@ TEST(SetupTest, Subsumes_Consistent_clauses) {
         }
 
         {
-          lela::Setup& s3 = s2;
-          EXPECT_EQ(s3.AddClause(Clause({Literal::Neq(a,m)})), lela::Setup::kOk);
+          limbo::Setup& s3 = s2;
+          EXPECT_EQ(s3.AddClause(Clause({Literal::Neq(a,m)})), limbo::Setup::kOk);
           EXPECT_EQ(dist(s3.clauses()), 5+1+1+2+2);
           s3.Minimize();
           EXPECT_EQ(dist(s3.clauses()), 5);
@@ -76,5 +76,5 @@ TEST(SetupTest, Subsumes_Consistent_clauses) {
   }
 }
 
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/solver.cc b/tests/solver.cc
index 7465db645ac9abf044821c222cefa2722d88defd..d1f932b3dd5fb0f91151b6782898ab8e2309ee94 100644
--- a/tests/solver.cc
+++ b/tests/solver.cc
@@ -3,14 +3,14 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/solver.h>
-#include <lela/format/output.h>
-#include <lela/format/cpp/syntax.h>
+#include <limbo/solver.h>
+#include <limbo/format/output.h>
+#include <limbo/format/cpp/syntax.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
-using namespace lela::format::cpp;
+using namespace limbo::format;
+using namespace limbo::format::cpp;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
@@ -240,5 +240,5 @@ TEST(SolverTest, Constants) {
   }
 }
 
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/syntax.cc b/tests/syntax.cc
index d4c3de5a349b38d606a4e2908a7aedf484bf4830..9611b7e243aac02acbd92347abe99d2f75f08ffb 100644
--- a/tests/syntax.cc
+++ b/tests/syntax.cc
@@ -3,14 +3,14 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/formula.h>
-#include <lela/format/output.h>
-#include <lela/format/cpp/syntax.h>
+#include <limbo/formula.h>
+#include <limbo/format/output.h>
+#include <limbo/format/cpp/syntax.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
-using namespace lela::format::cpp;
+using namespace limbo::format;
+using namespace limbo::format::cpp;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
@@ -62,5 +62,5 @@ TEST(Syntax, general) {
   }
 }
 
-}  // namespace lela
+}  // namespace limbo
 
diff --git a/tests/term.cc b/tests/term.cc
index ebd24a7886a5172c37a035a8a01acc07ac326b62..b0071fc7c1d5b79a20a3b11db9958fb01e5a7e40 100644
--- a/tests/term.cc
+++ b/tests/term.cc
@@ -3,12 +3,12 @@
 
 #include <gtest/gtest.h>
 
-#include <lela/term.h>
-#include <lela/format/output.h>
+#include <limbo/term.h>
+#include <limbo/format/output.h>
 
-namespace lela {
+namespace limbo {
 
-using namespace lela::format;
+using namespace limbo::format;
 
 struct EqSubstitute {
   EqSubstitute(Term pre, Term post) : pre_(pre), post_(post) {}
@@ -151,5 +151,5 @@ TEST(TermTest, Isomorphic) {
   { auto u = Term::Isomorphic(fn2n1, fn1n1); EXPECT_FALSE(bool(u)); }
 }
 
-}  // namespace lela
+}  // namespace limbo