diff --git a/README.md b/README.md
index 7e1d036bd727a7a3b27b9e52f114d53fc348338a..bde5a1437b088005c16558866d64825004e415ab 100644
--- a/README.md
+++ b/README.md
@@ -61,7 +61,7 @@ For more theoretical background see the papers linked below.
   [format/cpp/syntax.h](src/lela/format/cpp/syntax.h) overloads some C++
   operators.
 
-## Plan for the future
+## Future work
 
 * Add sitcalc-style actions: regression, progression, or simulate ESL [3] with
   preprocessing, or all of them?
diff --git a/examples/minesweeper/kb.h b/examples/minesweeper/kb.h
index aeaaa1216377946d07159d05c7fe95d962abdf8a..e6ad7804e884cce3881265edf6f8abdb4d39da78 100644
--- a/examples/minesweeper/kb.h
+++ b/examples/minesweeper/kb.h
@@ -61,27 +61,27 @@ class KnowledgeBase {
         F(ctx_.CreateName(Bool)),
 #endif
         MineF(ctx_.CreateFunction(Bool, 2)) {
-    lela::format::output::RegisterSort(Bool, "");
-    lela::format::output::RegisterSort(XPos, "");
-    lela::format::output::RegisterSort(YPos, "");
-    lela::format::output::RegisterSymbol(T.symbol(), "T");
+    lela::format::RegisterSort(Bool, "");
+    lela::format::RegisterSort(XPos, "");
+    lela::format::RegisterSort(YPos, "");
+    lela::format::RegisterSymbol(T.symbol(), "T");
 #ifdef USE_DETERMINES
-    lela::format::output::RegisterSymbol(F.symbol(), "F");
+    lela::format::RegisterSymbol(F.symbol(), "F");
 #endif
-    lela::format::output::RegisterSymbol(MineF, "Mine");
+    lela::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::output::RegisterSymbol(X[i].symbol(), ss.str());
+      lela::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::output::RegisterSymbol(Y[i].symbol(), ss.str());
+      lela::format::RegisterSymbol(Y[i].symbol(), ss.str());
     }
     processed_.resize(g_->n_fields(), false);
   }
diff --git a/examples/minesweeper/minesweeper.cc b/examples/minesweeper/minesweeper.cc
index 18def03be9121f7a10527eddadd18cec6475e489..74c47483bec35d8cb4d5e05b963a5c98bab024eb 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::output::operator<<;
+      using lela::format::operator<<;
       std::cout << ", which is just a guess.";
     } else {
       std::cout << ", found at split level " << k << ".";
diff --git a/examples/minesweeper/test.sh b/examples/minesweeper/test.sh
index 64d5014601731fe7dc5ffc1152d1a4fff41d501a..121da8aac7aa4c2009a3b15a77ff66fade5decf5 100755
--- a/examples/minesweeper/test.sh
+++ b/examples/minesweeper/test.sh
@@ -7,6 +7,6 @@ F=test-${W}x${H}-${M}-${K}-${max}.log
 
 inxi -Fx -c 0 >$F
 
-for seed in $(seq 1 $max); do ./minesweeper $W $H $M $seed $K; done | grep You >>$F
+for seed in $(seq 1 $max); do ./minesweeper $W $H $M $seed $K | grep You >>$F; done
 echo $F
 
diff --git a/examples/sudoku/kb.h b/examples/sudoku/kb.h
index 4829ab781ac544f300074e78b3f2631f9d9f8e68..7aabbf417378538c10d832f4bee905b52bf896e0 100644
--- a/examples/sudoku/kb.h
+++ b/examples/sudoku/kb.h
@@ -22,14 +22,14 @@ class KnowledgeBase {
       : max_k_(max_k),
         VAL_(ctx_.CreateSort()),
         val_(ctx_.CreateFunction(VAL_, 2)) {
-    lela::format::output::RegisterSort(VAL_, "");
-    lela::format::output::RegisterSymbol(val_, "val");
+    lela::format::RegisterSort(VAL_, "");
+    lela::format::RegisterSymbol(val_, "val");
     using namespace lela::format::cpp;
     for (std::size_t i = 1; i <= 9; ++i) {
       vals_.push_back(ctx_.CreateName(VAL_));
       std::stringstream ss;
       ss << i;
-      lela::format::output::RegisterSymbol(vals_.back().symbol(), ss.str());
+      lela::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) {
diff --git a/examples/tui/sudoku.h b/examples/tui/sudoku.h
index 6e7c9acccb01f351b81bee747433ca9b8ed5fb2a..33a66c3cacab3a758524d581825fc92f1d68fb0b 100644
--- a/examples/tui/sudoku.h
+++ b/examples/tui/sudoku.h
@@ -35,7 +35,7 @@ struct SudokuCallbacks {
             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)));
             if (b) {
-              using lela::format::output::operator<<;
+              using lela::format::operator<<;
               std::stringstream ss;
               ss << ns_[n];
               std::cout << ss.str().substr(1);
diff --git a/examples/tui/tui-js.cc b/examples/tui/tui-js.cc
index 581561492fb69fe72c61a1fb3726f94b804d1264..bfacb2b7ab44dad0bcc999c30b4705954d3df3f0 100644
--- a/examples/tui/tui-js.cc
+++ b/examples/tui/tui-js.cc
@@ -20,7 +20,7 @@
 #include "battleship.h"
 #include "sudoku.h"
 
-using lela::format::output::operator<<;
+using lela::format::operator<<;
 
 template<typename T>
 inline std::string to_string(const T& x) {
diff --git a/examples/tui/tui.cc b/examples/tui/tui.cc
index 877ed00d935134ab3edd750d4f5b999ed13a9111..1d25f0046c16458b98690e8098a3c35151709a4d 100644
--- a/examples/tui/tui.cc
+++ b/examples/tui/tui.cc
@@ -20,7 +20,7 @@
 #include "battleship.h"
 #include "sudoku.h"
 
-using lela::format::output::operator<<;
+using lela::format::operator<<;
 
 template<typename ForwardIt, typename Context>
 static bool parse(ForwardIt begin, ForwardIt end, Context* ctx) {
@@ -128,7 +128,7 @@ struct Callback : public lela::format::pdl::DefaultCallback {
         std::cerr << "Setup[" << p << "] = " << std::endl << ctx->kb()->sphere(p)->setup() << std::endl;
       }
     } else if (proc == "print") {
-      lela::format::output::print_range(std::cout, args, "", "", " ");
+      lela::format::print_range(std::cout, args, "", "", " ");
       std::cout << std::endl;
     } else if (proc == "enable_query_logging") {
       ctx->logger()->print_queries = true;
@@ -140,7 +140,7 @@ struct Callback : public lela::format::pdl::DefaultCallback {
       // it's a call for Sudoku
     } else {
       std::cerr << "Calling " << proc;
-      lela::format::output::print_range(std::cerr, args, "(", ")", ",");
+      lela::format::print_range(std::cerr, args, "(", ")", ",");
       std::cerr << " failed" << std::endl;
     }
   }
diff --git a/src/lela/clause.h b/src/lela/clause.h
index a15700f663570be441f10db7a14acaa8617b51c4..80b84c61903c460f2a360db1e0141db449d53ffc 100644
--- a/src/lela/clause.h
+++ b/src/lela/clause.h
@@ -32,6 +32,7 @@
 #include <vector>
 
 #include <lela/literal.h>
+
 #include <lela/internal/bloom.h>
 #include <lela/internal/ints.h>
 #include <lela/internal/iter.h>
@@ -49,7 +50,7 @@ class Clause {
 
   explicit Clause(const Literal a) : size_(!a.invalid() ? 1 : 0) {
     lits1_[0] = a;
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -69,7 +70,7 @@ class Clause {
       lits2_[i++] = *it++;
     }
     Minimize();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -79,7 +80,7 @@ class Clause {
     if (size2() > 0) {
       std::memcpy(lits2_.get(), c.lits2_.get(), size2() * sizeof(Literal));
     }
-#if defined(BLOOM)
+#ifdef BLOOM
     lhs_bloom_ = c.lhs_bloom_;
 #endif
     assert(!any([](Literal a) { return a.invalid(); }));
@@ -96,7 +97,7 @@ class Clause {
       }
       std::memcpy(lits2_.get(), c.lits2_.get(), size2() * sizeof(Literal));
     }
-#if defined(BLOOM)
+#ifdef BLOOM
     lhs_bloom_ = c.lhs_bloom_;
 #endif
     assert(!any([](Literal a) { return a.invalid(); }));
@@ -108,7 +109,7 @@ class Clause {
 
   bool operator==(const Clause& c) const {
     return size() == c.size() &&
-#if defined(BLOOM)
+#ifdef BLOOM
            lhs_bloom_ == c.lhs_bloom_ &&
 #endif
            std::memcmp(lits1_, c.lits1_, size1() * sizeof(Literal)) == 0 &&
@@ -159,14 +160,14 @@ class Clause {
   }
   bool invalid() const { return empty(); }
 
-#if defined(BLOOM)
+#ifdef BLOOM
   internal::BloomSet<Term> lhs_bloom() const { return lhs_bloom_; }
 #endif
 
   static bool Subsumes(const Literal a, const Clause c) {
     assert(a.primitive());
     assert(c.primitive());
-#if defined(BLOOM)
+#ifdef BLOOM
     if (!c.lhs_bloom_.PossiblyContains(a.lhs())) {
       return false;
     }
@@ -185,7 +186,7 @@ class Clause {
   static bool Subsumes(const Literal a, const Literal b, const Clause c) {
     assert(a < b);
     assert(c.primitive());
-#if defined(BLOOM)
+#ifdef BLOOM
     if (!c.lhs_bloom_.PossiblyContains(a.lhs()) || !c.lhs_bloom_.PossiblyContains(b.lhs())) {
       return false;
     }
@@ -213,7 +214,7 @@ next:
   static bool Subsumes(const Clause& c, const Clause& d) {
     assert(c.primitive());
     assert(d.primitive());
-#if defined(BLOOM)
+#ifdef BLOOM
     if (!c.lhs_bloom_.PossiblySubsetOf(d.lhs_bloom_)) {
       return false;
     }
@@ -244,7 +245,7 @@ next:
     assert(b.primitive());
     assert(!valid());
     assert(!b.valid() && !b.invalid());
-#if defined(BLOOM)
+#ifdef BLOOM
     if (!lhs_bloom_.PossiblyContains(b.lhs())) {
       return;
     }
@@ -256,7 +257,7 @@ next:
       }
     }
     RemoveNulls();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -279,7 +280,7 @@ next:
       }
     }
     RemoveNulls();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -302,7 +303,7 @@ next:
       }
     }
     RemoveNulls();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -313,7 +314,7 @@ next:
     assert(std::all_of(units.begin(), units.end(), [](Literal a) { return a.primitive(); }));
     assert(std::all_of(units.begin(), units.end(), [](Literal a) { return !a.valid() && !a.invalid(); }));
     for (Literal b : units) {
-#if defined(BLOOM)
+#ifdef BLOOM
       if (!lhs_bloom_.PossiblyContains(b.lhs())) {
         continue;
       }
@@ -326,7 +327,7 @@ next:
       }
     }
     RemoveNulls();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -337,7 +338,7 @@ next:
 
   bool Mentions(Literal a) const {
     return
-#if defined(BLOOM)
+#ifdef BLOOM
         lhs_bloom_.PossiblyContains(a.lhs()) &&
 #endif
         any([a](Literal b) { return a == b; });
@@ -345,7 +346,7 @@ next:
 
   bool MentionsLhs(Term t) const {
     return
-#if defined(BLOOM)
+#ifdef BLOOM
         lhs_bloom_.PossiblyContains(t) &&
 #endif
         any([t](Literal a) { return a.lhs() == t; });
@@ -431,7 +432,7 @@ next:
     assert(!any([](Literal a) { return a.invalid(); }));
   }
 
-#if defined(BLOOM)
+#ifdef BLOOM
   void InitBloom() {
     lhs_bloom_.Clear();
     for (size_t i = 0; i < size(); ++i) {
@@ -441,7 +442,7 @@ next:
 #endif
 
   size_t size_ = 0;
-#if defined(BLOOM)
+#ifdef BLOOM
   internal::BloomSet<Term> lhs_bloom_;
 #endif
   Literal lits1_[kArraySize];
diff --git a/src/lela/format/output.h b/src/lela/format/output.h
index db5c9a5939348fce10ead3e9d9c951a6f9f22cbe..5d803b91609e093a421c0712726dbb931b12a449 100644
--- a/src/lela/format/output.h
+++ b/src/lela/format/output.h
@@ -2,11 +2,9 @@
 // Copyright 2014-2017 Christoph Schwering
 // Licensed under the MIT license. See LICENSE file in the project root.
 //
-// Overloads the stream operator (<<) for Literal, Clause, and so on. For
-// Sort and Symbol objects, a human-readable name can be registered.
-
-#ifndef LELA_FORMAT_OUTPUT_H_
-#define LELA_FORMAT_OUTPUT_H_
+// Overloads the stream operator (<<) for Literal, Clause, and so on. These
+// operators are only activated when the corresponding header is included.
+// For Sort and Symbol objects, a human-readable name can be registered.
 
 #include <algorithm>
 #include <list>
@@ -19,27 +17,20 @@
 #include <utility>
 #include <vector>
 
-#include <lela/formula.h>
-#include <lela/literal.h>
-#if 0
-#include <lela/modal.h>
-#endif
-#include <lela/setup.h>
-#if 0
-#include <lela/solver.h>
-#endif
 #include <lela/term.h>
+
 #include <lela/internal/compar.h>
-#include <lela/internal/hashset.h>
 #include <lela/internal/iter.h>
 #include <lela/internal/maybe.h>
 
+#ifndef MARK
 #define MARK (std::cout << __FILE__ << ":" << __LINE__ << std::endl)
+#endif
 
 namespace lela {
 namespace format {
-namespace output {
 
+#ifndef LELA_FORMAT_OUTPUT_H_
 typedef std::unordered_map<Symbol::Sort, std::string> SortMap;
 typedef std::unordered_map<Symbol, std::string> SymbolMap;
 
@@ -124,13 +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_
 
+#ifdef LELA_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_
 
+#ifdef LELA_INTERNAL_MAYBE_H_
 template<typename K, typename T>
 std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m);
+#endif  // LELA_INTERNAL_MAYBE_H_
 
+#ifdef LELA_TERM_H_
+#ifndef LELA_TERM_OUTPUT
+#define LELA_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);
@@ -166,79 +165,81 @@ std::ostream& operator<<(std::ostream& os, const Term t) {
   }
   return os;
 }
+#endif  // LELA_TERM_OUTPUT
+#endif  // LELA_TERM_H_
 
-struct PrintSymbolComparator {
-  typedef Symbol value_type;
-
-  bool operator()(Symbol s1, Symbol s2) const {
-    internal::Maybe<std::string> n1 = LookupSymbol(s1);
-    internal::Maybe<std::string> n2 = LookupSymbol(s2);
-    return n1 && n2  ? n1.val < n2.val :
-           n1 && !n2 ? true :
-           !n1 && n2 ? false :
-                       s1.hash() < s2.hash();
-  }
-};
-
-struct PrintTermComparator {
-  typedef Term value_type;
-
-  inline bool operator()(Term t1, Term t2) const;
-};
-
-inline bool PrintTermComparator::operator()(Term t1, Term t2) const {
-  internal::LexicographicComparator<
-      PrintSymbolComparator,
-      internal::LessComparator<Symbol::Arity>,
-      internal::LexicographicContainerComparator<Term::Vector, PrintTermComparator>> comp;
-  return comp(t1.symbol(), t1.arity(), t1.args(),
-              t2.symbol(), t2.arity(), t2.args());
-}
-
-struct PrintLiteralComparator {
-  typedef Literal value_type;
-
-  bool operator()(Literal l1, Literal l2) const {
-    return comp(l1.lhs(), l1.rhs(), l1.pos(),
-                l2.lhs(), l2.rhs(), l2.pos());
-  }
-
-  internal::LexicographicComparator<
-      PrintTermComparator,
-      PrintTermComparator,
-      internal::LessComparator<bool>> comp;
-};
-
+#ifdef LELA_LITERAL_H_
+#ifndef LELA_LITERAL_OUTPUT
+#define LELA_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_
 
+#ifdef LELA_CLAUSE_H_
+#ifndef LELA_CLAUSE_OUTPUT
+#define LELA_CLAUSE_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Clause& c) {
+  struct PrintLiteralComparator {
+    struct PrintTermComparator {
+      struct PrintSymbolComparator {
+        typedef Symbol value_type;
+
+        bool operator()(Symbol s1, Symbol s2) const {
+          internal::Maybe<std::string> n1 = LookupSymbol(s1);
+          internal::Maybe<std::string> n2 = LookupSymbol(s2);
+          return n1 && n2  ? n1.val < n2.val :
+                 n1 && !n2 ? true :
+                 !n1 && n2 ? false :
+                             s1.hash() < s2.hash();
+        }
+      };
+
+      typedef Term value_type;
+
+      inline bool operator()(Term t1, Term t2) const {
+        internal::LexicographicComparator<
+            PrintSymbolComparator,
+            internal::LessComparator<Symbol::Arity>,
+            internal::LexicographicContainerComparator<Term::Vector, PrintTermComparator>> comp;
+        return comp(t1.symbol(), t1.arity(), t1.args(),
+                    t2.symbol(), t2.arity(), t2.args());
+      }
+    };
+
+    bool operator()(Literal l1, Literal l2) const {
+      return comp(l1.lhs(), l1.rhs(), l1.pos(),
+                  l2.lhs(), l2.rhs(), l2.pos());
+    }
+
+    internal::LexicographicComparator<
+        PrintTermComparator,
+        PrintTermComparator,
+        internal::LessComparator<bool>> comp;
+  };
   std::vector<Literal> vec(c.begin(), c.end());
   std::sort(vec.begin(), vec.end(), PrintLiteralComparator());
   return print_range(os, vec, "[", "]", " \u2228 ");
 }
+#endif  // LELA_OUTPUT_CLAUSE
+#endif  // LELA_CLAUSE_H_
 
+#ifdef LELA_SETUP_H_
+#ifndef LELA_SETUP_OUTPUT
+#define LELA_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_
 
-#if 0
-std::ostream& operator<<(std::ostream& os, const Solver& s) {
-  return os << s.setup();
-}
-
-std::ostream& operator<<(std::ostream& os, const KnowledgeBase& kb) {
-  for (const Solver& s : kb.spheres()) {
-    os << s << std::endl;
-  }
-  return os;
-}
-#endif
-
+#ifdef LELA_FORMULA_H_
+#ifndef LELA_FORMULA_OUTPUT
+#define LELA_FORMULA_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Formula& alpha) {
   switch (alpha.type()) {
     case Formula::kAtomic:
@@ -293,7 +294,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_
 
+#ifndef LELA_FORMAT_OUTPUT_H_
 template<typename InputIt>
 std::ostream& print_sequence(std::ostream& os,
                              InputIt begin,
@@ -389,13 +393,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_
 
+#ifdef LELA_INTERNAL_HASHSET_H_
+#ifndef LELA_INTERNAL_HASHSET_OUTPUT
+#define LELA_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_
 
+#ifdef LELA_INTERNAL_MAYBE_H_
+#ifndef LELA_INTERNAL_MAYBE_OUTPUT
+#define LELA_INTERNAL_MAYBE_OUTPUT
 template<typename T>
 std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m) {
   if (m) {
@@ -405,10 +418,13 @@ std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m) {
   }
   return os;
 }
+#endif  // LELA_INTERNAL_MAYBE_OUTPUT
+#endif  // LELA_INTERNAL_MAYBE_H_
 
-}  // namespace output
 }  // namespace format
 }  // namespace lela
 
+#ifndef LELA_FORMAT_OUTPUT_H_
+#define LELA_FORMAT_OUTPUT_H_
 #endif  // LELA_FORMAT_OUTPUT_H_
 
diff --git a/src/lela/format/pdl/context.h b/src/lela/format/pdl/context.h
index 4605c02eaf96f9871ed2c4ad4606ccd81b5c9332..e7ca79befaad0a841dfaee27eafd50b464145e98 100644
--- a/src/lela/format/pdl/context.h
+++ b/src/lela/format/pdl/context.h
@@ -12,8 +12,8 @@
 #ifndef LELA_FORMAT_PDL_CONTEXT_H_
 #define LELA_FORMAT_PDL_CONTEXT_H_
 
-#include <map>
 #include <iostream>
+#include <map>
 #include <string>
 #include <stdexcept>
 #include <utility>
@@ -22,6 +22,7 @@
 #include <lela/term.h>
 #include <lela/formula.h>
 #include <lela/kb.h>
+
 #include <lela/format/output.h>
 
 namespace lela {
@@ -132,7 +133,7 @@ class Context {
 
   void RegisterSort(const std::string& id) {
     const Symbol::Sort sort = CreateSort();
-    lela::format::output::RegisterSort(sort, "");
+    lela::format::RegisterSort(sort, "");
     sorts_.Register(id, sort);
     logger_(DefaultLogger::RegisterSortData(id));
   }
@@ -143,7 +144,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Term var = CreateVariable(sort);
     vars_.Register(id, var);
-    lela::format::output::RegisterSymbol(var.symbol(), id);
+    lela::format::RegisterSymbol(var.symbol(), id);
     logger_(DefaultLogger::RegisterVariableData(id, sort_id));
   }
 
@@ -153,7 +154,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Term name = CreateName(sort);
     names_.Register(id, name);
-    lela::format::output::RegisterSymbol(name.symbol(), id);
+    lela::format::RegisterSymbol(name.symbol(), id);
     logger_(DefaultLogger::RegisterNameData(id, sort_id));
   }
 
@@ -163,7 +164,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Symbol fun = CreateFunction(sort, arity);
     funs_.Register(id, fun);
-    lela::format::output::RegisterSymbol(fun, id);
+    lela::format::RegisterSymbol(fun, id);
     logger_(DefaultLogger::RegisterFunctionData(id, arity, sort_id));
   }
 
diff --git a/src/lela/format/pdl/parser.h b/src/lela/format/pdl/parser.h
index 32e372fa6fcdffdd5815246ffdf6f7af298f6e34..0f7777a34e4eb5433183cec4d97063f2a236388b 100644
--- a/src/lela/format/pdl/parser.h
+++ b/src/lela/format/pdl/parser.h
@@ -24,7 +24,9 @@
 #include <lela/formula.h>
 #include <lela/grounder.h>
 #include <lela/setup.h>
+
 #include <lela/format/output.h>
+
 #include <lela/format/pdl/lexer.h>
 
 namespace lela {
@@ -771,7 +773,7 @@ class Parser {
         return Success<>();
       } else {
         std::stringstream ss;
-        using lela::format::output::operator<<;
+        using lela::format::operator<<;
         ss << (is_assert ? "Assertion" : "Refutation") << " of " << *alpha.val << " failed";
         return Error<>(LELA_MSG(ss.str()));
       }
@@ -1173,7 +1175,7 @@ class Parser {
       const Result<Action<>> r = branch();
       if (!r) {
         std::stringstream ss;
-        using lela::format::output::operator<<;
+        using lela::format::operator<<;
         ss << Tok(0) << " " << Tok(1) << " " << Tok(2) << "...";
         return Error<Action<>>(LELA_MSG("Error in start with unparsed input "+ ss.str()), r);
       }
diff --git a/src/lela/formula.h b/src/lela/formula.h
index 1fff3c9028f08c8c899ad080932366c42a1dbf43..5af5e82703d901574a4a831ff1a41749dd686cb4 100644
--- a/src/lela/formula.h
+++ b/src/lela/formula.h
@@ -22,6 +22,7 @@
 #include <vector>
 
 #include <lela/clause.h>
+
 #include <lela/internal/iter.h>
 #include <lela/internal/ints.h>
 #include <lela/internal/maybe.h>
diff --git a/src/lela/grounder.h b/src/lela/grounder.h
index 5cae13189f7c677105372ea22a29981abed5bccc..457651da2dcbd2ba399e635b44a44c0ce4d78be7 100644
--- a/src/lela/grounder.h
+++ b/src/lela/grounder.h
@@ -38,6 +38,7 @@
 #include <lela/clause.h>
 #include <lela/formula.h>
 #include <lela/setup.h>
+
 #include <lela/internal/hash.h>
 #include <lela/internal/ints.h>
 #include <lela/internal/iter.h>
diff --git a/src/lela/kb.h b/src/lela/kb.h
index 14e69b075049a036b1056d4e9a72260e2aeafc9f..188ed4361ef48bce8f23e19a08772f58894b4cf1 100644
--- a/src/lela/kb.h
+++ b/src/lela/kb.h
@@ -31,9 +31,15 @@
 #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 <lela/internal/ints.h>
+#include <lela/internal/iter.h>
 #include <lela/internal/maybe.h>
 
 namespace lela {
diff --git a/src/lela/literal.h b/src/lela/literal.h
index 498918706658c356e90f12fe6864374493f6d3e6..76162357b250b74438bca56230701a21d5adf8ba 100644
--- a/src/lela/literal.h
+++ b/src/lela/literal.h
@@ -25,7 +25,9 @@
 #include <utility>
 
 #include <lela/term.h>
+
 #include <lela/internal/ints.h>
+#include <lela/internal/maybe.h>
 
 namespace lela {
 
diff --git a/src/lela/setup.h b/src/lela/setup.h
index 7f2894270718b42961fa716d09f7a2fd5bea956f..f269aa96e6240fde5fc41b3351cd8452909497b5 100644
--- a/src/lela/setup.h
+++ b/src/lela/setup.h
@@ -66,9 +66,12 @@
 #include <vector>
 
 #include <lela/clause.h>
-#include <lela/internal/intmap.h>
+#include <lela/literal.h>
+#include <lela/term.h>
+
 #include <lela/internal/ints.h>
 #include <lela/internal/iter.h>
+#include <lela/internal/maybe.h>
 
 namespace lela {
 
@@ -243,7 +246,7 @@ class Setup {
 
   bool LocallyConsistent(const std::unordered_set<Term>& ts) const {
     assert(std::all_of(ts.begin(), ts.end(), [](Term t) { return t.primitive(); }));
-#if defined(BLOOM)
+#ifdef BLOOM
     internal::BloomSet<Term> bs;
     for (Term t : ts) {
       bs.Add(t);
@@ -253,7 +256,7 @@ class Setup {
     for (size_t i : clauses()) {
       const Clause c = clause(i);
       if (
-#if defined(BLOOM)
+#ifdef BLOOM
           bs.PossiblyOverlaps(c.lhs_bloom()) &&
 #endif
           std::any_of(c.begin(), c.end(), [&ts](Literal a) { return ts.find(a.lhs()) != ts.end(); })) {
diff --git a/src/lela/solver.h b/src/lela/solver.h
index 3a9a97c06801aab259f85265228982c4c6f5e708..e5f287b6db7066e314e7978e0a0ad917534a793c 100644
--- a/src/lela/solver.h
+++ b/src/lela/solver.h
@@ -51,10 +51,15 @@
 #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 <lela/internal/ints.h>
+#include <lela/internal/maybe.h>
+
 namespace lela {
 
 class Solver {
diff --git a/tests/clause.cc b/tests/clause.cc
index ffc3ab70535132e287c6159669463be1156b97e9..c15ac652c4ac596b7b9330f1cd9bb87ff131ba4a 100644
--- a/tests/clause.cc
+++ b/tests/clause.cc
@@ -9,7 +9,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 struct EqSubstitute {
   EqSubstitute(Term pre, Term post) : pre_(pre), post_(post) {}
diff --git a/tests/formula.cc b/tests/formula.cc
index 4a8db21415297456297e6ca5b4b8f25b229601e2..ca35c35d21487d6fe83431a0edf50ebadcd486bb 100644
--- a/tests/formula.cc
+++ b/tests/formula.cc
@@ -9,8 +9,8 @@
 
 namespace lela {
 
+using namespace lela::format;
 using namespace lela::format::cpp;
-using namespace lela::format::output;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
diff --git a/tests/grounder.cc b/tests/grounder.cc
index 28f972333bf9a7f5cb5314f15d9bdf59897f7f5c..e0e5d007e785c599c7ea17c3820601e528acab71 100644
--- a/tests/grounder.cc
+++ b/tests/grounder.cc
@@ -11,7 +11,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 std::unordered_set<Clause> unique(const Setup& s) {
   std::unordered_set<Clause> set;
diff --git a/tests/hashset.cc b/tests/hashset.cc
index d747998d9462ff405165e677f8111d629afa11f8..6f2adeea218e9a0af768d228fcd276ef77f3e1a8 100644
--- a/tests/hashset.cc
+++ b/tests/hashset.cc
@@ -19,7 +19,7 @@ struct Value {
 
 std::ostream& operator<<(std::ostream& os, Value i) { return std::cout << i.x; }
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 namespace lela {
 namespace internal {
diff --git a/tests/kb.cc b/tests/kb.cc
index 31005b9a79ddf951eed0bae86ceb7f7deaa40b0b..bd27e651975547ac9dcafff26d4eaf42a220d5af 100644
--- a/tests/kb.cc
+++ b/tests/kb.cc
@@ -9,8 +9,8 @@
 
 namespace lela {
 
+using namespace lela::format;
 using namespace lela::format::cpp;
-using namespace lela::format::output;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
diff --git a/tests/literal.cc b/tests/literal.cc
index e50622456c1790c6f773c828709442b40b03e15e..503b8b58f9ccfd5b086bad6daf6c749b8636e1f0 100644
--- a/tests/literal.cc
+++ b/tests/literal.cc
@@ -8,7 +8,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 TEST(LiteralTest, general) {
   Symbol::Factory& sf = *Symbol::Factory::Instance();
diff --git a/tests/setup.cc b/tests/setup.cc
index 6146cc00009822f465e1a03f0f9fd4fa702a60d1..93a0e0d2713dd35d7e9bd7b3010096ac78ecc5a1 100644
--- a/tests/setup.cc
+++ b/tests/setup.cc
@@ -11,7 +11,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 template<typename T>
 size_t dist(T r) { return std::distance(r.begin(), r.end()); }
diff --git a/tests/solver.cc b/tests/solver.cc
index eedd3cdca362261c8458e9ee86c5b11e1b9121b7..7465db645ac9abf044821c222cefa2722d88defd 100644
--- a/tests/solver.cc
+++ b/tests/solver.cc
@@ -9,8 +9,8 @@
 
 namespace lela {
 
+using namespace lela::format;
 using namespace lela::format::cpp;
-using namespace lela::format::output;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
diff --git a/tests/syntax.cc b/tests/syntax.cc
index ceb8310cd1a7bc34194037995cb2909d28b8054e..d4c3de5a349b38d606a4e2908a7aedf484bf4830 100644
--- a/tests/syntax.cc
+++ b/tests/syntax.cc
@@ -9,8 +9,8 @@
 
 namespace lela {
 
+using namespace lela::format;
 using namespace lela::format::cpp;
-using namespace lela::format::output;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
diff --git a/tests/term.cc b/tests/term.cc
index b84856cbf7119ce20dd9c45dfc8e87e489ab2751..ebd24a7886a5172c37a035a8a01acc07ac326b62 100644
--- a/tests/term.cc
+++ b/tests/term.cc
@@ -8,7 +8,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 struct EqSubstitute {
   EqSubstitute(Term pre, Term post) : pre_(pre), post_(post) {}