diff --git a/src/lela/format/output.h b/src/lela/format/output.h
index 0141b93920b3c3d03c03f241b30b2ca45391aef6..d344e81b07ba787c9ec1c0676111bf38fcef48a8 100644
--- a/src/lela/format/output.h
+++ b/src/lela/format/output.h
@@ -41,6 +41,11 @@ inline SymbolMap* symbol_map() {
   return ↦
 }
 
+inline void UnregisterAll() {
+  sort_map()->clear();
+  symbol_map()->clear();
+}
+
 inline void RegisterSort(Symbol::Sort s, const std::string& n) {
   (*sort_map())[s] = n;
 }
diff --git a/src/lela/grounder.h b/src/lela/grounder.h
index fb1708a3523a883011725cd1991f6b73b500f022..ef3253f08ca4d240346bc820f0fa3eec0735c043 100644
--- a/src/lela/grounder.h
+++ b/src/lela/grounder.h
@@ -128,6 +128,7 @@ class Grounder {
   void PrepareForQuery(size_t k, const Formula::Reader<T>& phi) {
     names_changed_ |= AddMentionedNames(Mentioned<Term, SortedTermSet>([](Term t) { return t.name(); }, phi));
     names_changed_ |= AddPlusNames(PlusNames(phi));
+    names_changed_ |= AddPlusNames(PlusSplitNames(k, phi));
     AddSplitTerms(SplitTerms(k, phi));
     AddAssignLiterals(AssignLiterals(k, phi));
   }
@@ -367,9 +368,6 @@ class Grounder {
     // variables in any clause.
     // PlusNames() computes p for a given clause; it is hence p+1 where p
     // is the number of variables in that clause.
-    // This fix also takes care of the right-hand side split name: splitting
-    // always needs to consider at least one name that does not occur in the KB
-    // or query, i.e., for every split term there must be at least plus name.
     PlusMap plus_one;
     c.Traverse([&plus_one](Term t) { plus_one[t.sort()] = 1; return true; });
     return PlusMap::Zip(plus, plus_one, [](size_t lp, size_t rp) { return lp + rp; });
@@ -418,6 +416,39 @@ class Grounder {
     }
   }
 
+  template<typename T>
+  static PlusMap PlusSplitNames(size_t k, const Formula::Reader<T>& phi) {
+    // When a term t only occurs in the form of literals (t = n), (t = x), or
+    // their duals and negations, then splitting does not necessitate an
+    // additional name. However, when t is an argument of another term or when
+    // it occurs in literals of the form (t = t') or its dual or negation, then
+    // we might need a name for every split.
+    // Note that in general we really need k plus names. For instance,
+    // (c = d) is not valid. To see that for k >= 2, splitting needs to consider
+    // at least 2 <= k names, not just one.
+    PlusMap plus;
+    phi.Traverse([&plus, k](Literal a) {
+      auto f = [&plus, k](Term t) {
+        if (t.function()) {
+          plus[t.sort()] = k;
+        }
+        return true;
+      };
+      if (a.lhs().function() && a.rhs().function()) {
+        f(a.lhs());
+        f(a.rhs());
+      }
+      for (Term t : a.lhs().args()) {
+        t.Traverse(f);
+      }
+      for (Term t : a.rhs().args()) {
+        t.Traverse(f);
+      }
+      return true;
+    });
+    return plus;
+  }
+
   template<typename T>
   TermSet SplitTerms(size_t k, const Formula::Reader<T>& phi) {
     if (k == 0) {
diff --git a/src/lela/solver.h b/src/lela/solver.h
index e698cf1e1814dcb71d7ec58943c266f97da2a69e..784cff76969d3cba2ac64cd3912a09cf6bc6cd59 100644
--- a/src/lela/solver.h
+++ b/src/lela/solver.h
@@ -94,6 +94,10 @@ class Solver {
   }
 
  private:
+#ifdef FRIEND_TEST
+  FRIEND_TEST(SolverTest, Constants);
+#endif
+
   typedef Grounder::TermSet TermSet;
   typedef Grounder::LiteralSet LiteralSet;
   typedef Grounder::SortedTermSet SortedTermSet;
diff --git a/tests/grounder.cc b/tests/grounder.cc
index 92338b20c8023e632d7f4424a67b8505376c6c51..86bc98981a31759c38193c439729bd2d1178532f 100644
--- a/tests/grounder.cc
+++ b/tests/grounder.cc
@@ -194,17 +194,20 @@ TEST(GrounderTest, Ground_SplitTerms_Names) {
     EXPECT_NE(x3.sort(), a.sort());
     EXPECT_EQ(names.size(), 2);
     EXPECT_EQ(names[n1.symbol().sort()].size(), 2);
-    EXPECT_EQ(names[x3.symbol().sort()].size(), 1);
+    EXPECT_EQ(names[x3.symbol().sort()].size(), 2);
     EXPECT_EQ(names[a.sort()].size(), 2);
-    EXPECT_EQ(names[g.sort()].size(), 1);
-    EXPECT_EQ(names[h.sort()].size(), 1);
-    Term nx3 = names[x3.sort()][0];
-    Term nSplit = names[a.sort()][ names[a.sort()][0] == n1 ? 1 : 0 ];
-    EXPECT_NE(nx3, n1);
-    EXPECT_NE(nSplit, n1);
-    EXPECT_NE(nSplit, nx3);
+    EXPECT_EQ(names[g.sort()].size(), 2);
+    EXPECT_EQ(names[h.sort()].size(), 2);
+    Term nx3_1 = names[x3.sort()][0];
+    Term nx3_2 = names[x3.sort()][1];
+    Term n_Split = names[a.sort()][ names[a.sort()][0] == n1 ? 1 : 0 ];
+    EXPECT_NE(nx3_1, n1);
+    EXPECT_NE(nx3_2, n1);
+    EXPECT_NE(n_Split, n1);
+    EXPECT_NE(n_Split, nx3_1);
+    EXPECT_NE(n_Split, nx3_2);
     EXPECT_EQ(std::set<Term>(terms.begin(), terms.end()),
-              std::set<Term>({tf.CreateTerm(a, {}), tf.CreateTerm(g, {n1}), tf.CreateTerm(g, {nSplit}), tf.CreateTerm(h, {n1, nx3})}));
+              std::set<Term>({tf.CreateTerm(a, {}), tf.CreateTerm(g, {n1}), tf.CreateTerm(g, {n_Split}), tf.CreateTerm(h, {n1, nx3_1}), tf.CreateTerm(h, {n1, nx3_2})}));
   }
 
   {
@@ -398,8 +401,8 @@ TEST(GrounderTest, Ground_SplitNames) {
     g.PrepareForQuery(0, phi.reader());
     Grounder::SortedTermSet names = g.Names();
     EXPECT_EQ(names[Bool].size(), 1+1);// 2+0);
-    EXPECT_EQ(names[Human].size(), 1+0);
-    EXPECT_EQ(names[Animal].size(), 0+0);
+    EXPECT_EQ(names[Human].size(), 1+1);
+    EXPECT_EQ(names[Animal].size(), 0+1);
     Grounder::TermSet terms = g.SplitTerms();
     EXPECT_EQ(terms.size(), 0);
   }
@@ -408,7 +411,7 @@ TEST(GrounderTest, Ground_SplitNames) {
     g.PrepareForQuery(1, phi.reader());
     Grounder::SortedTermSet names = g.Names();
     EXPECT_EQ(names[Bool].size(), 1+1);// 2+0);
-    EXPECT_EQ(names[Human].size(), 1+0);
+    EXPECT_EQ(names[Human].size(), 1+1);
     EXPECT_EQ(names[Animal].size(), 0+1);
     Grounder::TermSet terms = g.SplitTerms();
     EXPECT_NE(terms.size(), 0);
@@ -418,7 +421,7 @@ TEST(GrounderTest, Ground_SplitNames) {
     g.PrepareForQuery(2, phi.reader());
     Grounder::SortedTermSet names = g.Names();
     EXPECT_EQ(names[Bool].size(), 1+1);// 2+0);
-    EXPECT_EQ(names[Human].size(), 1+0);
+    EXPECT_EQ(names[Human].size(), 1+1);
     EXPECT_EQ(names[Animal].size(), 0+2);
     Grounder::TermSet terms = g.SplitTerms();
     EXPECT_NE(terms.size(), 0);
@@ -428,7 +431,7 @@ TEST(GrounderTest, Ground_SplitNames) {
     g.PrepareForQuery(3, phi.reader());
     Grounder::SortedTermSet names = g.Names();
     EXPECT_EQ(names[Bool].size(), 1+1);// 2+0);
-    EXPECT_EQ(names[Human].size(), 1+0);
+    EXPECT_EQ(names[Human].size(), 1+1);
     EXPECT_EQ(names[Animal].size(), 0+3);
     Grounder::TermSet terms = g.SplitTerms();
     EXPECT_NE(terms.size(), 0);
@@ -460,8 +463,8 @@ TEST(GrounderTest, Ground_SplitNames_iterated) {
     g.PrepareForQuery(0, phi.reader());
     Grounder::SortedTermSet names = g.Names();
     EXPECT_EQ(names[Bool].size(), 1+1);// 2+0);
-    EXPECT_EQ(names[Human].size(), 1+0);
-    EXPECT_EQ(names[Animal].size(), 0+0);
+    EXPECT_EQ(names[Human].size(), 1+1);
+    EXPECT_EQ(names[Animal].size(), 0+1);
     Grounder::TermSet terms = g.SplitTerms();
     EXPECT_EQ(terms.size(), 0);
   }
@@ -469,7 +472,7 @@ TEST(GrounderTest, Ground_SplitNames_iterated) {
     g.PrepareForQuery(1, phi.reader());
     Grounder::SortedTermSet names = g.Names();
     EXPECT_EQ(names[Bool].size(), 1+1);// 2+0);
-    EXPECT_EQ(names[Human].size(), 1+0);
+    EXPECT_EQ(names[Human].size(), 1+1);
     EXPECT_EQ(names[Animal].size(), 0+1);
     Grounder::TermSet terms = g.SplitTerms();
     EXPECT_NE(terms.size(), 0);
@@ -478,7 +481,7 @@ TEST(GrounderTest, Ground_SplitNames_iterated) {
     g.PrepareForQuery(2, phi.reader());
     Grounder::SortedTermSet names = g.Names();
     EXPECT_EQ(names[Bool].size(), 1+1);// 2+0);
-    EXPECT_EQ(names[Human].size(), 1+0);
+    EXPECT_EQ(names[Human].size(), 1+1);
     EXPECT_EQ(names[Animal].size(), 0+2);
     Grounder::TermSet terms = g.SplitTerms();
     EXPECT_NE(terms.size(), 0);
@@ -487,7 +490,7 @@ TEST(GrounderTest, Ground_SplitNames_iterated) {
     g.PrepareForQuery(3, phi.reader());
     Grounder::SortedTermSet names = g.Names();
     EXPECT_EQ(names[Bool].size(), 1+1);// 2+0);
-    EXPECT_EQ(names[Human].size(), 1+0);
+    EXPECT_EQ(names[Human].size(), 1+1);
     EXPECT_EQ(names[Animal].size(), 0+3);
     Grounder::TermSet terms = g.SplitTerms();
     EXPECT_NE(terms.size(), 0);
diff --git a/tests/solver.cc b/tests/solver.cc
index 41f1ad7dbf1090ed0aba0444121af5f4b78da03c..729892b751b647bc2fcc4662556bb3f5a455d21a 100644
--- a/tests/solver.cc
+++ b/tests/solver.cc
@@ -192,7 +192,7 @@ TEST(SolverTest, ECAI2016Complete) {
   EXPECT_TRUE(solver.Consistent(1, Formula::Clause(Clause{Italian == T}).reader()));
 }
 
-TEST(SetupTest, Bool) {
+TEST(SolverTest, Bool) {
   Solver solver;
   Context ctx(solver.sf(), solver.tf());
   Symbol::Factory sf;
@@ -212,5 +212,24 @@ TEST(SetupTest, Bool) {
   }
 }
 
+TEST(SolverTest, Constants) {
+  Solver solver;
+  UnregisterAll();
+  Context ctx(solver.sf(), solver.tf());
+  Symbol::Factory sf;
+  Term::Factory tf;
+  auto SomeSort = sf.CreateSort();    RegisterSort(SomeSort, "");
+  auto a = ctx.NewFun(SomeSort, 0)(); REGISTER_SYMBOL(a);
+  auto b = ctx.NewFun(SomeSort, 0)(); REGISTER_SYMBOL(b);
+  {
+    for (int i = 0; i < 2; ++i) {
+      for (int k = 0; k <= 3; ++k) {
+        EXPECT_FALSE(solver.Entails(k, Formula::Clause(Clause{a == b}).reader()));
+        EXPECT_FALSE(solver.Entails(k, Formula::Clause(Clause{a != b}).reader()));
+      }
+    }
+  }
+}
+
 }  // namespace lela