Merge remote-tracking branch 'proofsearch-import/master'

10 files changed, 1781 insertions, 0 deletions

diff --git a/proofsearch/tests/CMakeLists.txt b/proofsearch/tests/CMakeLists.txt
new file mode 100644
index 0000000..184357b
--- /dev/null
+++ b/proofsearch/tests/CMakeLists.txt
@@ -0,0 +1,31 @@
+# ─── GoogleTest ───────────────────────────────────────────────────────────────
+include(FetchContent)
+FetchContent_Declare(
+    googletest
+    GIT_REPOSITORY https://github.com/google/googletest.git
+    GIT_TAG        v1.14.0
+)
+# Prevent GoogleTest from overriding our compiler/linker options
+set(gtest_force_shared_crt ON CACHE BOOL "" FORCE)
+FetchContent_MakeAvailable(googletest)
+
+include(GoogleTest)
+
+# ─── Helper: define a test target ────────────────────────────────────────────
+function(atp_add_test TEST_NAME TEST_SOURCE)
+    add_executable(${TEST_NAME} ${TEST_SOURCE})
+    target_link_libraries(${TEST_NAME} PRIVATE atp_core GTest::gtest_main)
+    target_compile_options(${TEST_NAME} PRIVATE ${ATP_PROJECT_WARNING_FLAGS})
+    gtest_discover_tests(${TEST_NAME})
+endfunction()
+
+# ─── Test Targets ────────────────────────────────────────────────────────────
+atp_add_test(test_term_bank       test_term_bank.cc)
+atp_add_test(test_unification     test_unification.cc)
+atp_add_test(test_clausifier      test_clausifier.cc)
+atp_add_test(test_resolution      test_resolution.cc)
+atp_add_test(test_discrim_tree    test_discrim_tree.cc)
+atp_add_test(test_prover          test_prover.cc)
+atp_add_test(test_simplify        test_simplify.cc)
+atp_add_test(test_proof_trace     test_proof_trace.cc)
+atp_add_test(test_end_to_end      test_end_to_end.cc)
diff --git a/proofsearch/tests/test_clausifier.cc b/proofsearch/tests/test_clausifier.cc
new file mode 100644
index 0000000..17c63f8
--- /dev/null
+++ b/proofsearch/tests/test_clausifier.cc
@@ -0,0 +1,17 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
diff --git a/proofsearch/tests/test_discrim_tree.cc b/proofsearch/tests/test_discrim_tree.cc
new file mode 100644
index 0000000..17c63f8
--- /dev/null
+++ b/proofsearch/tests/test_discrim_tree.cc
@@ -0,0 +1,17 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
diff --git a/proofsearch/tests/test_end_to_end.cc b/proofsearch/tests/test_end_to_end.cc
new file mode 100644
index 0000000..ceb9991
--- /dev/null
+++ b/proofsearch/tests/test_end_to_end.cc
@@ -0,0 +1,184 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+/// @file test_end_to_end.cc
+/// @brief End-to-end tests: TPTP string → parse → prove → verify result.
+
+#include "atp/core/clause_store.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/frontend/tptp_parser.h"
+#include "atp/proof/proof_trace.h"
+#include "atp/search/prover.h"
+
+#include <gtest/gtest.h>
+#include <string>
+#include <utility>
+
+namespace atp {
+namespace {
+
+/// Helper: parse a TPTP string and run the prover, return the result.
+struct E2EResult {
+    ProverResult result_;
+    std::string proof_output_;
+};
+
+E2EResult runProver(const std::string& tptp_input) {
+    SymbolTable symbols;
+    TermBank bank(symbols);
+    ClauseStore store;
+
+    auto problem = parseTptpString(tptp_input, bank, symbols);
+    auto clauses = prepareForProving(problem, bank, symbols);
+
+    Prover prover(bank, store);
+    prover.addClauses(std::move(clauses));
+    ProverResult const result = prover.prove();
+
+    std::string proof_output;
+    if (result == ProverResult::kTheorem) {
+        auto eid = prover.getEmptyClauseId();
+        if (eid.has_value()) {
+            auto proof = extractProof(store, *eid);
+            proof_output = formatProof(proof, store, bank);
+        }
+    }
+
+    return {result, proof_output};
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Simple Propositional
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, SimplePropositional) {
+    auto [result, proof] = runProver(R"(
+        cnf(fact, axiom, p(a)).
+        cnf(rule, axiom, ~p(X) | q(X)).
+        cnf(goal, negated_conjecture, ~q(a)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kTheorem);
+    EXPECT_FALSE(proof.empty());
+    // Proof should contain the key elements
+    EXPECT_NE(proof.find("p(a)"), std::string::npos) << proof;
+    EXPECT_NE(proof.find("q(a)"), std::string::npos) << proof;
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Trivial: direct contradiction
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, DirectContradiction) {
+    auto [result, proof] = runProver(R"(
+        cnf(pos, axiom, p(a)).
+        cnf(neg, negated_conjecture, ~p(a)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kTheorem);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Satisfiable: no contradiction possible
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, Satisfiable) {
+    auto [result, proof] = runProver(R"(
+        cnf(a1, axiom, p(a)).
+        cnf(a2, axiom, q(b)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kSaturation);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Three-step chain
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, ThreeStepChain) {
+    auto [result, proof] = runProver(R"(
+        cnf(a1, axiom, p(a)).
+        cnf(a2, axiom, ~p(X) | q(X)).
+        cnf(a3, axiom, ~q(X) | r(X)).
+        cnf(goal, negated_conjecture, ~r(a)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kTheorem);
+    EXPECT_NE(proof.find("r(a)"), std::string::npos) << proof;
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Proof output format
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, ProofOutputContainsAllSteps) {
+    auto [result, proof] = runProver(R"(
+        cnf(fact, axiom, p(a)).
+        cnf(rule, axiom, ~p(X) | q(X)).
+        cnf(goal, negated_conjecture, ~q(a)).
+    )");
+
+    ASSERT_EQ(result, ProverResult::kTheorem);
+
+    // Must contain [input] lines for axioms
+    EXPECT_NE(proof.find("[input]"), std::string::npos) << proof;
+    // Must contain [resolution] for derived clauses
+    EXPECT_NE(proof.find("[resolution]"), std::string::npos) << proof;
+    // Must contain empty clause marker
+    std::string const empty_marker = "□";
+    EXPECT_NE(proof.find(empty_marker), std::string::npos) << proof;
+    // Must contain [X, Y] provenance (sequential numbers)
+    EXPECT_NE(proof.find('['), std::string::npos) << proof;
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Monkey and Banana Problem (the flagship test!)
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, MonkeyBanana) {
+    auto [result, proof] = runProver(R"(
+        % Initial state
+        cnf(init_state, axiom, state(a, b, c, h0, s0)).
+
+        % Action: Go(X)
+        cnf(action_go, axiom, ~state(M, B, G, h0, S) | state(X, B, G, h0, do(go(X), S))).
+
+        % Action: Push(X)
+        cnf(action_push, axiom, ~state(M, M, G, h0, S) | state(X, X, G, h0, do(push(X), S))).
+
+        % Action: Climb
+        cnf(action_climb, axiom, ~state(M, M, G, h0, S) | state(M, M, G, h1, do(climb, S))).
+
+        % Action: Down
+        cnf(action_down, axiom, ~state(M, B, G, h1, S) | state(M, B, G, h0, do(down, S))).
+
+        % Action: Reach
+        cnf(action_reach, axiom, ~state(G, G, G, h1, S) | goal_reached(do(reach, S))).
+
+        % Negated goal
+        cnf(negated_goal, negated_conjecture, ~goal_reached(S)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kTheorem) << "ATP should prove the monkey can get the banana!\n"
+                                              << "Proof output:\n"
+                                              << proof;
+}
+
+}  // namespace
+}  // namespace atp
diff --git a/proofsearch/tests/test_proof_trace.cc b/proofsearch/tests/test_proof_trace.cc
new file mode 100644
index 0000000..f2c3c96
--- /dev/null
+++ b/proofsearch/tests/test_proof_trace.cc
@@ -0,0 +1,207 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/proof/proof_trace.h"
+#include "atp/search/prover.h"
+
+#include <gtest/gtest.h>
+#include <string>
+#include <utility>
+#include <vector>
+
+namespace atp {
+namespace {
+
+class ProofTraceTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
+    ClauseStore store_;
+
+    SymbolId sym_a_{}, sym_b_{};
+    SymbolId sym_p_{}, sym_q_{};
+    SymbolId sym_x_{};
+
+    TermId a_term_{}, b_term_{}, x_term_{};
+
+    void SetUp() override {
+        sym_a_ = symbols_.intern("a", SymbolKind::kConstant);
+        sym_b_ = symbols_.intern("b", SymbolKind::kConstant);
+        sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1);
+        sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1);
+        sym_x_ = symbols_.intern("X", SymbolKind::kVariable);
+
+        a_term_ = bank_.makeTerm(sym_a_, {});
+        b_term_ = bank_.makeTerm(sym_b_, {});
+        x_term_ = bank_.makeVar(sym_x_);
+    }
+
+    TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); }
+    TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); }
+
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
+
+    static Clause makeClause(std::vector<Literal> lits) {
+        Clause cl;
+        cl.literals_ = std::move(lits);
+        return cl;
+    }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// termToString Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProofTraceTest, TermToStringConstant) {
+    EXPECT_EQ(termToString(a_term_, bank_), "a");
+}
+
+TEST_F(ProofTraceTest, TermToStringVariable) {
+    EXPECT_EQ(termToString(x_term_, bank_), "X");
+}
+
+TEST_F(ProofTraceTest, TermToStringCompound) {
+    TermId const pa = p(a_term_);
+    EXPECT_EQ(termToString(pa, bank_), "P(a)");
+}
+
+TEST_F(ProofTraceTest, TermToStringNested) {
+    SymbolId const sym_f = symbols_.intern("f", SymbolKind::kFunction, 1);
+    TermId const fa = bank_.makeTerm(sym_f, {{a_term_}});
+    TermId const pfa = p(fa);
+    EXPECT_EQ(termToString(pfa, bank_), "P(f(a))");
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// clauseToString Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProofTraceTest, ClauseToStringEmpty) {
+    Clause const empty = makeClause({});
+    EXPECT_EQ(clauseToString(empty, bank_), "□");
+}
+
+TEST_F(ProofTraceTest, ClauseToStringSinglePositive) {
+    Clause const c = makeClause({pos(p(a_term_))});
+    EXPECT_EQ(clauseToString(c, bank_), "P(a)");
+}
+
+TEST_F(ProofTraceTest, ClauseToStringSingleNegative) {
+    Clause const c = makeClause({neg(p(a_term_))});
+    EXPECT_EQ(clauseToString(c, bank_), "¬P(a)");
+}
+
+TEST_F(ProofTraceTest, ClauseToStringMultipleLiterals) {
+    Clause const c = makeClause({neg(p(x_term_)), pos(q(x_term_))});
+    std::string const s = clauseToString(c, bank_);
+    EXPECT_EQ(s, "¬P(X) ∨ Q(X)");
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// extractProof Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProofTraceTest, ExtractProofTrivial) {
+    // Run a trivial proof: {P(a)} + {¬P(a)} → □
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_term_))}), makeClause({neg(p(a_term_))})});
+    ProverResult const result = prover.prove();
+    ASSERT_EQ(result, ProverResult::kTheorem);
+
+    auto eid = prover.getEmptyClauseId();
+    ASSERT_TRUE(eid.has_value());
+
+    auto proof = extractProof(store_, *eid);
+    ASSERT_GE(proof.size(), 3U);  // At least: 2 axioms + 1 empty clause
+
+    // First steps should be axioms (kInput)
+    EXPECT_EQ(proof.front().rule_, InferenceRule::kInput);
+    // Last step should be the empty clause
+    EXPECT_EQ(proof.back().clause_id_, *eid);
+    // Last step should be resolution
+    EXPECT_EQ(proof.back().rule_, InferenceRule::kResolution);
+}
+
+TEST_F(ProofTraceTest, ExtractProofTwoStep) {
+    // {P(a)}, {¬P(X), Q(X)}, {¬Q(a)} → □ in 2 resolution steps
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_term_))}), makeClause({neg(p(x_term_)), pos(q(x_term_))}),
+                       makeClause({neg(q(a_term_))})});
+    ProverResult const result = prover.prove();
+    ASSERT_EQ(result, ProverResult::kTheorem);
+
+    auto eid = prover.getEmptyClauseId();
+    ASSERT_TRUE(eid.has_value());
+
+    auto proof = extractProof(store_, *eid);
+    // Should have axioms + intermediate + empty clause
+    ASSERT_GE(proof.size(), 4U);  // 3 axioms + at least 1 intermediate + empty
+
+    // Last step is the empty clause
+    EXPECT_EQ(proof.back().clause_id_, *eid);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// formatProof Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProofTraceTest, FormatProofContainsExpectedElements) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_term_))}), makeClause({neg(p(a_term_))})});
+    prover.prove();
+
+    auto eid = prover.getEmptyClauseId();
+    ASSERT_TRUE(eid.has_value());
+
+    auto proof = extractProof(store_, *eid);
+    std::string const output = formatProof(proof, store_, bank_);
+
+    // Should contain key elements
+    EXPECT_NE(output.find("input"), std::string::npos) << output;
+    EXPECT_NE(output.find("resolution"), std::string::npos) << output;
+    EXPECT_NE(output.find("P(a)"), std::string::npos) << output;
+    // Empty clause should appear
+    std::string const empty_marker = "□";
+    EXPECT_NE(output.find(empty_marker), std::string::npos) << output;
+}
+
+TEST_F(ProofTraceTest, FormatProofNoParentsForAxioms) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_term_))}), makeClause({neg(p(a_term_))})});
+    prover.prove();
+
+    auto eid = prover.getEmptyClauseId();
+    auto proof = extractProof(store_, *eid);
+    std::string const output = formatProof(proof, store_, bank_);
+
+    // The first line (an axiom) should NOT have "[from ...]"
+    // Find the first newline
+    auto first_line = output.substr(0, output.find('\n'));
+    EXPECT_EQ(first_line.find("[from"), std::string::npos)
+        << "Axiom should not have parent info: " << first_line;
+}
+
+}  // namespace
+}  // namespace atp
diff --git a/proofsearch/tests/test_prover.cc b/proofsearch/tests/test_prover.cc
new file mode 100644
index 0000000..74d02ad
--- /dev/null
+++ b/proofsearch/tests/test_prover.cc
@@ -0,0 +1,183 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/search/prover.h"
+
+#include <gtest/gtest.h>
+#include <utility>
+#include <vector>
+
+namespace atp {
+namespace {
+
+class ProverTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
+    ClauseStore store_;
+
+    SymbolId sym_a_{}, sym_b_{};
+    SymbolId sym_f_{};
+    SymbolId sym_p_{}, sym_q_{}, sym_r_{};
+    SymbolId sym_x_{}, sym_y_{};
+
+    TermId a_{}, b_{}, x_{}, y_{};
+
+
+    void SetUp() override {
+        sym_a_ = symbols_.intern("a", SymbolKind::kConstant);
+        sym_b_ = symbols_.intern("b", SymbolKind::kConstant);
+        sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1);
+        sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1);
+        sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1);
+        sym_r_ = symbols_.intern("R", SymbolKind::kPredicate, 2);
+        sym_x_ = symbols_.intern("X", SymbolKind::kVariable);
+        sym_y_ = symbols_.intern("Y", SymbolKind::kVariable);
+
+        a_ = bank_.makeTerm(sym_a_, {});
+        b_ = bank_.makeTerm(sym_b_, {});
+        x_ = bank_.makeVar(sym_x_);
+        y_ = bank_.makeVar(sym_y_);
+    }
+
+    TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); }
+    TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); }
+    TermId r(TermId a1, TermId a2) { return bank_.makeTerm(sym_r_, {{a1, a2}}); }
+    TermId f(TermId arg) { return bank_.makeTerm(sym_f_, {{arg}}); }
+
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
+
+    static Clause makeClause(std::vector<Literal> lits) {
+        Clause cl;
+        cl.literals_ = std::move(lits);
+        return cl;
+    }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Trivial refutation: {P(a)} and {¬P(a)} → empty clause
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, TrivialRefutation) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_))}), makeClause({neg(p(a_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+    EXPECT_TRUE(prover.getEmptyClauseId().has_value());
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Unification required: {P(X)} and {¬P(a)} → empty clause
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, RefutationWithUnification) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(x_))}), makeClause({neg(p(a_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Multi-step: {P(a)}, {¬P(X), Q(X)}, {¬Q(a)}
+// Step 1: resolve P(a) with ¬P(X)∨Q(X) → Q(a)
+// Step 2: resolve Q(a) with ¬Q(a) → empty
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, TwoStepRefutation) {
+    Prover prover(bank_, store_);
+    prover.addClauses(
+        {makeClause({pos(p(a_))}), makeClause({neg(p(x_)), pos(q(x_))}), makeClause({neg(q(a_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Saturation: {P(a)}, {Q(b)} — no complementary literals
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, Saturation) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_))}), makeClause({pos(q(b_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kSaturation);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Timeout: set very low limits
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, Timeout) {
+    ProverConfig config;
+    config.max_iterations_ = 1;
+
+    // Need enough clauses to not saturate in 1 iteration
+    Prover prover(bank_, store_, config);
+    prover.addClauses({makeClause({pos(p(x_)), pos(q(x_))}), makeClause({neg(p(a_)), pos(q(a_))}),
+                       makeClause({neg(q(x_)), pos(p(f(x_)))}), makeClause({neg(p(x_)), neg(q(x_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTimeout);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Chain reasoning: P(a), ¬P(X)∨Q(X), ¬Q(X)∨R(X), ¬R(a)
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, ThreeStepChain) {
+    const SymbolId kSymS = symbols_.intern("S", SymbolKind::kPredicate, 1);
+    auto s = [&](TermId arg) { return bank_.makeTerm(kSymS, {{arg}}); };
+
+    Prover prover(bank_, store_);
+    prover.addClauses({
+        makeClause({pos(p(a_))}),             // P(a)
+        makeClause({neg(p(x_)), pos(q(x_))}),  // ¬P(X) ∨ Q(X)
+        makeClause({neg(q(x_)), pos(s(x_))}),  // ¬Q(X) ∨ S(X)
+        makeClause({neg(s(a_))})              // ¬S(a)
+    });
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Empty clause in input directly
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, EmptyClauseInInput) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({}),  // empty clause directly
+                       makeClause({pos(p(a_))})});
+
+    // Empty clause should be detected immediately when selected from queue
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+}
+
+}  // namespace
+}  // namespace atp
diff --git a/proofsearch/tests/test_resolution.cc b/proofsearch/tests/test_resolution.cc
new file mode 100644
index 0000000..02250d9
--- /dev/null
+++ b/proofsearch/tests/test_resolution.cc
@@ -0,0 +1,257 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/clause.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/infer/resolution.h"
+
+#include <gtest/gtest.h>
+#include <utility>
+#include <vector>
+
+namespace atp {
+namespace {
+
+class ResolutionTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
+
+    SymbolId sym_a_{}, sym_b_{}, sym_c_{};
+    SymbolId sym_f_{};
+    SymbolId sym_p_{}, sym_q_{}, sym_r_{};
+    SymbolId sym_x_{}, sym_y_{}, sym_z_{};
+
+    TermId a_{}, b_{}, c_{};
+    TermId x_{}, y_{}, z_{};
+
+    void SetUp() override {
+        sym_a_ = symbols_.intern("a", SymbolKind::kConstant);
+        sym_b_ = symbols_.intern("b", SymbolKind::kConstant);
+        sym_c_ = symbols_.intern("c", SymbolKind::kConstant);
+        sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1);
+        sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1);
+        sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1);
+        sym_r_ = symbols_.intern("R", SymbolKind::kPredicate, 2);
+        sym_x_ = symbols_.intern("X", SymbolKind::kVariable);
+        sym_y_ = symbols_.intern("Y", SymbolKind::kVariable);
+        sym_z_ = symbols_.intern("Z", SymbolKind::kVariable);
+
+        a_ = bank_.makeTerm(sym_a_, {});
+        b_ = bank_.makeTerm(sym_b_, {});
+        c_ = bank_.makeTerm(sym_c_, {});
+        x_ = bank_.makeVar(sym_x_);
+        y_ = bank_.makeVar(sym_y_);
+        z_ = bank_.makeVar(sym_z_);
+    }
+
+    TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); }
+    TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); }
+    TermId r(TermId a1, TermId a2) { return bank_.makeTerm(sym_r_, {{a1, a2}}); }
+    TermId f(TermId arg) { return bank_.makeTerm(sym_f_, {{arg}}); }
+
+    // Helper: make a clause from literals
+    static Clause makeClause(std::vector<Literal> lits, ClauseId id = kInvalidId) {
+        Clause c;
+        c.id_ = id;
+        c.literals_ = std::move(lits);
+        return c;
+    }
+
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Basic Resolution Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ResolutionTest, SimpleGroundResolution) {
+    // {P(a)} and {¬P(a), Q(b)}  → {Q(b)}
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_)), pos(q(b_))}, 1);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->literals_.size(), 1);
+    EXPECT_EQ(result->literals_[0].atom_, q(b_));
+    EXPECT_TRUE(result->literals_[0].is_positive_);
+}
+
+TEST_F(ResolutionTest, ResolutionWithUnification) {
+    // {P(X)} and {¬P(a)} → {} (empty clause!)
+    Clause const c1 = makeClause({pos(p(x_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_))}, 1);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_TRUE(result->isEmpty()) << "Should derive empty clause (contradiction)";
+}
+
+TEST_F(ResolutionTest, ResolutionFailsSamePolarity) {
+    // {P(a)} and {P(b)} → no resolution (both positive)
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({pos(p(b_))}, 1);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    EXPECT_FALSE(result.has_value());
+}
+
+TEST_F(ResolutionTest, ResolutionFailsNoUnifier) {
+    // {P(a)} and {¬P(b)} → can't unify a with b
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(b_))}, 1);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    EXPECT_FALSE(result.has_value());
+}
+
+TEST_F(ResolutionTest, ResolutionAppliesSubstToRemainingLiterals) {
+    // {P(X), Q(X)} and {¬P(a)} → {Q(a)}
+    Clause const c1 = makeClause({pos(p(x_)), pos(q(x_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_))}, 1);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->literals_.size(), 1);
+    EXPECT_EQ(result->literals_[0].atom_, q(a_));
+}
+
+TEST_F(ResolutionTest, ResolutionMultipleLiterals) {
+    // {P(X), Q(b)} and {¬P(a), R(a, c)} → {Q(b), R(a, c)}
+    Clause const c1 = makeClause({pos(p(x_)), pos(q(b_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_)), pos(r(a_, c_))}, 1);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->literals_.size(), 2);
+}
+
+TEST_F(ResolutionTest, VariableRenamingWorks) {
+    // Both clauses use variable X
+    // {P(X)} and {¬P(X), Q(X)} → {Q(a)} only if X is renamed in c2
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(x_)), pos(q(x_))}, 1);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->literals_.size(), 1);
+    // Q(X) should become Q(a) after substitution {X→a}
+    EXPECT_EQ(result->literals_[0].atom_, q(a_));
+}
+
+TEST_F(ResolutionTest, VariableRenamingPreventsClash) {
+    // {R(X, a)} and {¬R(b, X)}
+    // Without renaming: X would clash between c1 and c2
+    // With renaming: c2's X → _R0, then unify R(X,a) with R(b,_R0) → {X→b, _R0→a}
+    Clause const c1 = makeClause({pos(r(x_, a_))}, 0);
+    Clause const c2 = makeClause({neg(r(b_, x_))}, 1);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_TRUE(result->isEmpty());
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// AllResolvents Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ResolutionTest, AllResolventsFindsAll) {
+    // {P(a), Q(a)} and {¬P(a), ¬Q(a)}
+    // Can resolve on P or Q → 2 resolvents
+    Clause const c1 = makeClause({pos(p(a_)), pos(q(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_)), neg(q(a_))}, 1);
+
+    auto results = allResolvents(bank_, c1, c2);
+    EXPECT_EQ(results.size(), 2);
+}
+
+TEST_F(ResolutionTest, AllResolventsEmpty) {
+    // {P(a)} and {Q(b)} → no complementary pairs
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({pos(q(b_))}, 1);
+
+    auto results = allResolvents(bank_, c1, c2);
+    EXPECT_TRUE(results.empty());
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Factoring Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ResolutionTest, SimpleFactoring) {
+    // {P(X), P(a), Q(X)} → factor P(X) with P(a): {P(a), Q(a)}
+    Clause const c = makeClause({pos(p(x_)), pos(p(a_)), pos(q(x_))}, 0);
+
+    auto results = factor(bank_, c);
+    ASSERT_EQ(results.size(), 1);
+    EXPECT_EQ(results[0].literals_.size(), 2);
+    // After factoring: {P(a), Q(a)}
+    EXPECT_EQ(results[0].literals_[0].atom_, p(a_));
+    EXPECT_EQ(results[0].literals_[1].atom_, q(a_));
+}
+
+TEST_F(ResolutionTest, NoFactoring) {
+    // {P(a), Q(b)} → different predicates, can't factor
+    Clause const c = makeClause({pos(p(a_)), pos(q(b_))}, 0);
+    auto results = factor(bank_, c);
+    EXPECT_TRUE(results.empty());
+}
+
+TEST_F(ResolutionTest, FactoringDifferentPolarity) {
+    // {P(a), ¬P(a)} → different polarity, can't factor
+    Clause const c = makeClause({pos(p(a_)), neg(p(a_))}, 0);
+    auto results = factor(bank_, c);
+    EXPECT_TRUE(results.empty());
+}
+
+TEST_F(ResolutionTest, FactoringNonUnifiable) {
+    // {P(a), P(b)} → can't unify a with b
+    Clause const c = makeClause({pos(p(a_)), pos(p(b_))}, 0);
+    auto results = factor(bank_, c);
+    EXPECT_TRUE(results.empty());
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Provenance Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ResolutionTest, ResolventHasProvenance) {
+    Clause const c1 = makeClause({pos(p(x_))}, 5);
+    Clause const c2 = makeClause({neg(p(a_))}, 7);
+
+    auto result = resolve(bank_, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->rule_, InferenceRule::kResolution);
+    EXPECT_EQ(result->parent1_, 5);
+    EXPECT_EQ(result->parent2_, 7);
+}
+
+TEST_F(ResolutionTest, FactoredHasProvenance) {
+    Clause const c = makeClause({pos(p(x_)), pos(p(a_))}, 3);
+    auto results = factor(bank_, c);
+    ASSERT_FALSE(results.empty());
+    EXPECT_EQ(results[0].rule_, InferenceRule::kFactoring);
+    EXPECT_EQ(results[0].parent1_, 3);
+}
+
+}  // namespace
+}  // namespace atp
diff --git a/proofsearch/tests/test_simplify.cc b/proofsearch/tests/test_simplify.cc
new file mode 100644
index 0000000..968ab3b
--- /dev/null
+++ b/proofsearch/tests/test_simplify.cc
@@ -0,0 +1,191 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/clause.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/simplify/subsumption.h"
+#include "atp/simplify/tautology.h"
+
+#include <gtest/gtest.h>
+#include <utility>
+#include <vector>
+
+namespace atp {
+namespace {
+
+class SimplifyTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
+
+    SymbolId sym_a_{}, sym_b_{}, sym_c_{};
+    SymbolId sym_p_{}, sym_q_{}, sym_r_{};
+    SymbolId sym_x_{};
+
+    TermId a_{}, b_{}, c_{}, x_{};
+
+    void SetUp() override {
+        sym_a_ = symbols_.intern("a", SymbolKind::kConstant);
+        sym_b_ = symbols_.intern("b", SymbolKind::kConstant);
+        sym_c_ = symbols_.intern("c", SymbolKind::kConstant);
+        sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1);
+        sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1);
+        sym_r_ = symbols_.intern("R", SymbolKind::kPredicate, 2);
+        sym_x_ = symbols_.intern("X", SymbolKind::kVariable);
+
+        a_ = bank_.makeTerm(sym_a_, {});
+        b_ = bank_.makeTerm(sym_b_, {});
+        c_ = bank_.makeTerm(sym_c_, {});
+        x_ = bank_.makeVar(sym_x_);
+    }
+
+    TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); }
+    TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); }
+    TermId r(TermId a1, TermId a2) { return bank_.makeTerm(sym_r_, {{a1, a2}}); }
+
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
+
+    static Clause makeClause(std::vector<Literal> lits) {
+        Clause cl;
+        cl.literals_ = std::move(lits);
+        return cl;
+    }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Tautology Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(SimplifyTest, TautologyComplementaryLiterals) {
+    // {P(a), ¬P(a)} → tautology
+    Clause const cl = makeClause({pos(p(a_)), neg(p(a_))});
+    EXPECT_TRUE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, TautologyWithExtraLiterals) {
+    // {Q(b), P(a), ¬P(a)} → tautology
+    Clause const cl = makeClause({pos(q(b_)), pos(p(a_)), neg(p(a_))});
+    EXPECT_TRUE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologySamePolarity) {
+    // {P(a), P(a)} → NOT tautology (same polarity)
+    Clause const cl = makeClause({pos(p(a_)), pos(p(a_))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologyDifferentAtoms) {
+    // {P(a), ¬P(b)} → NOT tautology (different atoms)
+    Clause const cl = makeClause({pos(p(a_)), neg(p(b_))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologyDifferentPredicates) {
+    // {P(a), ¬Q(a)} → NOT tautology (different predicates)
+    Clause const cl = makeClause({pos(p(a_)), neg(q(a_))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologyEmptyClause) {
+    Clause const cl = makeClause({});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologySingleLiteral) {
+    Clause const cl = makeClause({pos(p(a_))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, TautologyVariableAtom) {
+    // {P(X), ¬P(X)} → tautology (same variable term)
+    Clause const cl = makeClause({pos(p(x_)), neg(p(x_))});
+    EXPECT_TRUE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologyVarVsConst) {
+    // {P(X), ¬P(a)} → NOT tautology (syntactically different)
+    Clause const cl = makeClause({pos(p(x_)), neg(p(a_))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Subsumption Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(SimplifyTest, SubsumesSubset) {
+    // {P(a)} subsumes {P(a), Q(b)}
+    Clause const gen = makeClause({pos(p(a_))});
+    Clause const spec = makeClause({pos(p(a_)), pos(q(b_))});
+    EXPECT_TRUE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesIdentical) {
+    // {P(a), Q(b)} subsumes {P(a), Q(b)}
+    Clause const c1 = makeClause({pos(p(a_)), pos(q(b_))});
+    Clause const c2 = makeClause({pos(p(a_)), pos(q(b_))});
+    EXPECT_TRUE(subsumes(c1, c2));
+}
+
+TEST_F(SimplifyTest, SubsumesEmptyClause) {
+    // {} subsumes everything
+    Clause const empty = makeClause({});
+    Clause const cl = makeClause({pos(p(a_)), neg(q(b_))});
+    EXPECT_TRUE(subsumes(empty, cl));
+}
+
+TEST_F(SimplifyTest, SubsumesNotLarger) {
+    // {P(a), Q(b)} does NOT subsume {P(a)}
+    Clause const gen = makeClause({pos(p(a_)), pos(q(b_))});
+    Clause const spec = makeClause({pos(p(a_))});
+    EXPECT_FALSE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesRequiresSamePolarity) {
+    // {P(a)} does NOT subsume {¬P(a)}
+    Clause const gen = makeClause({pos(p(a_))});
+    Clause const spec = makeClause({neg(p(a_))});
+    EXPECT_FALSE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesRequiresSameAtom) {
+    // {P(a)} does NOT subsume {P(b)}
+    Clause const gen = makeClause({pos(p(a_))});
+    Clause const spec = makeClause({pos(p(b_))});
+    EXPECT_FALSE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesNegativeLiterals) {
+    // {¬P(a)} subsumes {¬P(a), Q(b)}
+    Clause const gen = makeClause({neg(p(a_))});
+    Clause const spec = makeClause({neg(p(a_)), pos(q(b_))});
+    EXPECT_TRUE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesOrderIndependent) {
+    // {Q(b), P(a)} subsumes {P(a), Q(b), R(a,b)} regardless of order
+    Clause const gen = makeClause({pos(q(b_)), pos(p(a_))});
+    Clause const spec = makeClause({pos(p(a_)), pos(q(b_)), pos(r(a_, b_))});
+    EXPECT_TRUE(subsumes(gen, spec));
+}
+
+}  // namespace
+}  // namespace atp
diff --git a/proofsearch/tests/test_term_bank.cc b/proofsearch/tests/test_term_bank.cc
new file mode 100644
index 0000000..0d4fcc7
--- /dev/null
+++ b/proofsearch/tests/test_term_bank.cc
@@ -0,0 +1,339 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+
+#include <cstddef>
+#include <gtest/gtest.h>
+#include <span>
+#include <stdexcept>
+#include <utility>
+
+namespace atp {
+namespace {
+
+// ═══════════════════════════════════════════════════════════════════════════
+// SymbolTable Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(SymbolTableTest, InternReturnsConsistentId) {
+    SymbolTable st;
+    SymbolId const id1 = st.intern("foo", SymbolKind::kFunction, 2);
+    SymbolId const id2 = st.intern("foo", SymbolKind::kFunction, 2);
+    EXPECT_EQ(id1, id2);
+}
+
+TEST(SymbolTableTest, DifferentNamesGetDifferentIds) {
+    SymbolTable st;
+    SymbolId const a = st.intern("a", SymbolKind::kConstant);
+    SymbolId const b = st.intern("b", SymbolKind::kConstant);
+    EXPECT_NE(a, b);
+}
+
+TEST(SymbolTableTest, GetNameRoundTrips) {
+    SymbolTable st;
+    SymbolId const id = st.intern("hello", SymbolKind::kFunction, 1);
+    EXPECT_EQ(st.getName(id), "hello");
+}
+
+TEST(SymbolTableTest, GetInfoPreservesMetadata) {
+    SymbolTable st;
+    SymbolId const id = st.intern("P", SymbolKind::kPredicate, 3, 42);
+    const SymbolInfo& info = st.getInfo(id);
+    EXPECT_EQ(info.name_, "P");
+    EXPECT_EQ(info.kind_, SymbolKind::kPredicate);
+    EXPECT_EQ(info.arity_, 3);
+    EXPECT_EQ(info.sort_, 42);
+}
+
+TEST(SymbolTableTest, IsVariableDetectsKind) {
+    SymbolTable st;
+    SymbolId const var = st.intern("X", SymbolKind::kVariable);
+    SymbolId const con = st.intern("a", SymbolKind::kConstant);
+    SymbolId const fun = st.intern("f", SymbolKind::kFunction, 1);
+    EXPECT_TRUE(st.isVariable(var));
+    EXPECT_FALSE(st.isVariable(con));
+    EXPECT_FALSE(st.isVariable(fun));
+}
+
+TEST(SymbolTableTest, MismatchKindThrows) {
+    SymbolTable st;
+    st.intern("x", SymbolKind::kConstant);
+    EXPECT_THROW(st.intern("x", SymbolKind::kVariable), std::runtime_error);
+}
+
+TEST(SymbolTableTest, MismatchArityThrows) {
+    SymbolTable st;
+    st.intern("f", SymbolKind::kFunction, 1);
+    EXPECT_THROW(st.intern("f", SymbolKind::kFunction, 2), std::runtime_error);
+}
+
+TEST(SymbolTableTest, SizeTracksInternedSymbols) {
+    SymbolTable st;
+    EXPECT_EQ(st.size(), 0);
+    st.intern("a", SymbolKind::kConstant);
+    EXPECT_EQ(st.size(), 1);
+    st.intern("b", SymbolKind::kConstant);
+    EXPECT_EQ(st.size(), 2);
+    st.intern("a", SymbolKind::kConstant);  // duplicate
+    EXPECT_EQ(st.size(), 2);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// TermBank Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+class TermBankTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
+
+    SymbolId sym_a_{}, sym_b_{}, sym_f_{}, sym_g_{}, sym_x_id_{}, sym_y_id_{};
+
+    void SetUp() override {
+        sym_a_ = symbols_.intern("a", SymbolKind::kConstant);
+        sym_b_ = symbols_.intern("b", SymbolKind::kConstant);
+        sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1);
+        sym_g_ = symbols_.intern("g", SymbolKind::kFunction, 2);
+        sym_x_id_ = symbols_.intern("X", SymbolKind::kVariable);
+        sym_y_id_ = symbols_.intern("Y", SymbolKind::kVariable);
+    }
+};
+
+TEST_F(TermBankTest, HashConsingReturnsSameId) {
+    const TermId kA1 = bank_.makeTerm(sym_a_, {});
+    const TermId kA2 = bank_.makeTerm(sym_a_, {});
+    EXPECT_EQ(kA1, kA2) << "Hash consing failed: same term got different IDs";
+}
+
+TEST_F(TermBankTest, DifferentTermsGetDifferentIds) {
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    const TermId kB = bank_.makeTerm(sym_b_, {});
+    EXPECT_NE(kA, kB);
+}
+
+TEST_F(TermBankTest, CompoundTermHashConsing) {
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    const TermId kB = bank_.makeTerm(sym_b_, {});
+    // f(a)
+    const TermId kFA1 = bank_.makeTerm(sym_f_, {{kA}});
+    const TermId kFA2 = bank_.makeTerm(sym_f_, {{kA}});
+    EXPECT_EQ(kFA1, kFA2);
+    // f(b) != f(a)
+    const TermId kFB = bank_.makeTerm(sym_f_, {{kB}});
+    EXPECT_NE(kFA1, kFB);
+}
+
+TEST_F(TermBankTest, NestedTermHashConsing) {
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    const TermId kFA = bank_.makeTerm(sym_f_, {{kA}});
+    // g(f(a), a)
+    const TermId kGFAA1 = bank_.makeTerm(sym_g_, {{kFA, kA}});
+    const TermId kGFAA2 = bank_.makeTerm(sym_g_, {{kFA, kA}});
+    EXPECT_EQ(kGFAA1, kGFAA2);
+}
+
+TEST_F(TermBankTest, GetTermReturnsCorrectSymbol) {
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    const Term& t = bank_.getTerm(kA);
+    EXPECT_EQ(t.symbol_id_, sym_a_);
+    EXPECT_EQ(t.arity(), 0);
+}
+
+TEST_F(TermBankTest, GetTermReturnsCorrectArgs) {
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    const TermId kB = bank_.makeTerm(sym_b_, {});
+    const TermId kGAB = bank_.makeTerm(sym_g_, {{kA, kB}});
+
+    const Term& t = bank_.getTerm(kGAB);
+    EXPECT_EQ(t.symbol_id_, sym_g_);
+    EXPECT_EQ(t.arity(), 2);
+    ASSERT_EQ(t.args_.size(), 2);
+    EXPECT_EQ(t.args_[0], kA);
+    EXPECT_EQ(t.args_[1], kB);
+}
+
+TEST_F(TermBankTest, MakeVarCreatesZeroArityTerm) {
+    const TermId kX = bank_.makeVar(sym_x_id_);
+    const Term& t = bank_.getTerm(kX);
+    EXPECT_EQ(t.symbol_id_, sym_x_id_);
+    EXPECT_EQ(t.arity(), 0);
+    EXPECT_TRUE(t.args_.empty());
+}
+
+TEST_F(TermBankTest, IsVariableDistinguishesFromConstants) {
+    const TermId kX = bank_.makeVar(sym_x_id_);
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+
+    EXPECT_TRUE(bank_.isVariable(kX)) << "Variable should be detected as variable";
+    EXPECT_FALSE(bank_.isVariable(kA)) << "Constant should NOT be detected as variable";
+}
+
+TEST_F(TermBankTest, VariableHashConsing) {
+    const TermId kX1 = bank_.makeVar(sym_x_id_);
+    const TermId kX2 = bank_.makeVar(sym_x_id_);
+    EXPECT_EQ(kX1, kX2);
+
+    const TermId kY = bank_.makeVar(sym_y_id_);
+    EXPECT_NE(kX1, kY);
+}
+
+TEST_F(TermBankTest, SizeTracksUniqueTerms) {
+    EXPECT_EQ(bank_.size(), 0);
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    EXPECT_EQ(bank_.size(), 1);
+    bank_.makeTerm(sym_a_, {});  // duplicate
+    EXPECT_EQ(bank_.size(), 1);
+    bank_.makeTerm(sym_b_, {});
+    EXPECT_EQ(bank_.size(), 2);
+    bank_.makeTerm(sym_f_, {{kA}});
+    EXPECT_EQ(bank_.size(), 3);
+}
+
+TEST_F(TermBankTest, CompoundTermWithVariableArgs) {
+    // f(X) — a function applied to a variable
+    const TermId kX = bank_.makeVar(sym_x_id_);
+    const TermId kFX = bank_.makeTerm(sym_f_, {{kX}});
+
+    const Term& t = bank_.getTerm(kFX);
+    EXPECT_EQ(t.symbol_id_, sym_f_);
+    EXPECT_EQ(t.arity(), 1);
+    EXPECT_EQ(t.args_[0], kX);
+
+    EXPECT_FALSE(bank_.isVariable(kFX));
+    EXPECT_TRUE(bank_.isVariable(kX));
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// ClauseStore Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(ClauseStoreTest, AddAndRetrieve) {
+    ClauseStore store;
+    Clause c;
+    c.literals_.push_back(Literal{.atom_ = 0, .is_positive_ = true});
+    c.literals_.push_back(Literal{.atom_ = 1, .is_positive_ = false});
+
+    const ClauseId kId = store.addClause(std::move(c));
+    EXPECT_EQ(kId, 0);
+
+    const Clause& retrieved = store.getClause(kId);
+    EXPECT_EQ(retrieved.id_, kId);
+    EXPECT_EQ(retrieved.literals_.size(), 2);
+    EXPECT_EQ(retrieved.literals_[0].atom_, 0);
+    EXPECT_TRUE(retrieved.literals_[0].is_positive_);
+    EXPECT_EQ(retrieved.literals_[1].atom_, 1);
+    EXPECT_FALSE(retrieved.literals_[1].is_positive_);
+}
+
+TEST(ClauseStoreTest, AssignsSequentialIds) {
+    ClauseStore store;
+    const ClauseId kId0 = store.addClause(Clause{});
+    const ClauseId kId1 = store.addClause(Clause{});
+    const ClauseId kId2 = store.addClause(Clause{});
+    EXPECT_EQ(kId0, 0);
+    EXPECT_EQ(kId1, 1);
+    EXPECT_EQ(kId2, 2);
+    EXPECT_EQ(store.size(), 3);
+}
+
+TEST(ClauseStoreTest, StampsClauseWithId) {
+    ClauseStore store;
+    Clause c;
+    c.id_ = kInvalidId;  // unset
+    const ClauseId kId = store.addClause(std::move(c));
+    EXPECT_EQ(store.getClause(kId).id_, kId);
+}
+
+TEST(ClauseStoreTest, MutableAccess) {
+    ClauseStore store;
+    Clause c;
+    c.depth_ = 0;
+    const ClauseId kId = store.addClause(std::move(c));
+
+    store.getMutableClause(kId).depth_ = 42;
+    EXPECT_EQ(store.getClause(kId).depth_, 42);
+}
+
+TEST(ClauseStoreTest, ForEachVisitsAll) {
+    ClauseStore store;
+    store.addClause(Clause{});
+    store.addClause(Clause{});
+    store.addClause(Clause{});
+
+    size_t count = 0;
+    store.forEach([&count](const Clause&) { count++; });
+    EXPECT_EQ(count, 3);
+}
+
+TEST(ClauseStoreTest, EmptyClauseDetection) {
+    Clause c;
+    EXPECT_TRUE(c.isEmpty());
+    c.literals_.push_back(Literal{.atom_ = 0, .is_positive_ = true});
+    EXPECT_FALSE(c.isEmpty());
+    EXPECT_EQ(c.size(), 1);
+}
+
+TEST(ClauseStoreTest, ProvenancePreserved) {
+    ClauseStore store;
+    Clause c;
+    c.rule_ = InferenceRule::kResolution;
+    c.parent1_ = 3;
+    c.parent2_ = 7;
+    c.depth_ = 5;
+
+    ClauseId const id = store.addClause(std::move(c));
+    const Clause& retrieved = store.getClause(id);
+    EXPECT_EQ(retrieved.rule_, InferenceRule::kResolution);
+    EXPECT_EQ(retrieved.parent1_, 3);
+    EXPECT_EQ(retrieved.parent2_, 7);
+    EXPECT_EQ(retrieved.depth_, 5);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Literal Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(LiteralTest, Complement) {
+    const Literal kPos{.atom_ = 42, .is_positive_ = true};
+    const Literal kNeg = kPos.complement();
+    EXPECT_EQ(kNeg.atom_, 42);
+    EXPECT_FALSE(kNeg.is_positive_);
+
+    const Literal kBack = kNeg.complement();
+    EXPECT_EQ(kBack, kPos);
+}
+
+TEST(LiteralTest, Equality) {
+    const Literal kA{.atom_ = 1, .is_positive_ = true};
+    const Literal kB{.atom_ = 1, .is_positive_ = true};
+    const Literal kC{.atom_ = 1, .is_positive_ = false};
+    const Literal kD{.atom_ = 2, .is_positive_ = true};
+    EXPECT_EQ(kA, kB);
+    EXPECT_NE(kA, kC);
+    EXPECT_NE(kA, kD);
+}
+
+}  // namespace
+}  // namespace atp
diff --git a/proofsearch/tests/test_unification.cc b/proofsearch/tests/test_unification.cc
new file mode 100644
index 0000000..63ac9f0
--- /dev/null
+++ b/proofsearch/tests/test_unification.cc
@@ -0,0 +1,355 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/infer/substitution.h"
+#include "atp/infer/unification.h"
+
+#include <gtest/gtest.h>
+
+namespace atp {
+namespace {
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Test Fixture
+// ═══════════════════════════════════════════════════════════════════════════
+
+class UnificationTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
+
+    // Symbols
+    SymbolId sym_a_{}, sym_b_{}, sym_c_{};
+    SymbolId sym_f_{}, sym_g_{}, sym_h_{};
+    SymbolId sym_p_{};
+    SymbolId sym_x_{}, sym_y_{}, sym_z_{};
+
+    // Terms (created in SetUp)
+    TermId a_{}, b_{}, c_{};
+    TermId x_{}, y_{}, z_{};
+
+    void SetUp() override {
+        sym_a_ = symbols_.intern("a", SymbolKind::kConstant);
+        sym_b_ = symbols_.intern("b", SymbolKind::kConstant);
+        sym_c_ = symbols_.intern("c", SymbolKind::kConstant);
+        sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1);
+        sym_g_ = symbols_.intern("g", SymbolKind::kFunction, 2);
+        sym_h_ = symbols_.intern("h", SymbolKind::kFunction, 1);
+        sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 2);
+        sym_x_ = symbols_.intern("X", SymbolKind::kVariable);
+        sym_y_ = symbols_.intern("Y", SymbolKind::kVariable);
+        sym_z_ = symbols_.intern("Z", SymbolKind::kVariable);
+
+        a_ = bank_.makeTerm(sym_a_, {});
+        b_ = bank_.makeTerm(sym_b_, {});
+        c_ = bank_.makeTerm(sym_c_, {});
+        x_ = bank_.makeVar(sym_x_);
+        y_ = bank_.makeVar(sym_y_);
+        z_ = bank_.makeVar(sym_z_);
+    }
+
+    // Helper: make f(arg)
+    TermId f(TermId arg) { return bank_.makeTerm(sym_f_, {{arg}}); }
+    // Helper: make g(arg1, arg2)
+    TermId g(TermId a1, TermId a2) { return bank_.makeTerm(sym_g_, {{a1, a2}}); }
+    // Helper: make h(arg)
+    TermId h(TermId arg) { return bank_.makeTerm(sym_h_, {{arg}}); }
+    // Helper: make P(arg1, arg2)
+    TermId p(TermId a1, TermId a2) { return bank_.makeTerm(sym_p_, {{a1, a2}}); }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Substitution Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(UnificationTest, SubstBindAndLookup) {
+    Substitution subst;
+    EXPECT_TRUE(subst.bind(x_, a_));
+    EXPECT_EQ(subst.lookup(x_), a_);
+    EXPECT_EQ(subst.lookup(y_), kInvalidId);  // unbound
+}
+
+TEST_F(UnificationTest, SubstBindSameTermSucceeds) {
+    Substitution subst;
+    EXPECT_TRUE(subst.bind(x_, a_));
+    EXPECT_TRUE(subst.bind(x_, a_));  // same binding → OK
+}
+
+TEST_F(UnificationTest, SubstBindDifferentTermFails) {
+    Substitution subst;
+    EXPECT_TRUE(subst.bind(x_, a_));
+    EXPECT_FALSE(subst.bind(x_, b_));  // different binding → fail
+}
+
+TEST_F(UnificationTest, SubstResolveChain) {
+    // X → Y → a
+    Substitution subst;
+    subst.bind(x_, y_);
+    subst.bind(y_, a_);
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
+}
+
+TEST_F(UnificationTest, SubstResolveUnbound) {
+    Substitution const subst;
+    EXPECT_EQ(subst.resolve(x_, bank_), x_);  // unbound → returns itself
+}
+
+TEST_F(UnificationTest, SubstResolveNonVariable) {
+    Substitution const subst;
+    EXPECT_EQ(subst.resolve(a_, bank_), a_);  // constant → returns itself
+}
+
+TEST_F(UnificationTest, SubstApplySimple) {
+    // σ = {X → a}    apply to f(X) → f(a)
+    Substitution subst;
+    subst.bind(x_, a_);
+    TermId const fx = f(x_);
+    TermId const result = subst.apply(fx, bank_);
+    TermId const expected = f(a_);
+    EXPECT_EQ(result, expected);
+}
+
+TEST_F(UnificationTest, SubstApplyLeavesUnbound) {
+    // σ = {X → a}    apply to g(X, Y) → g(a, Y)
+    Substitution subst;
+    subst.bind(x_, a_);
+    TermId const gxy = g(x_, y_);
+    TermId const result = subst.apply(gxy, bank_);
+    TermId const expected = g(a_, y_);
+    EXPECT_EQ(result, expected);
+}
+
+TEST_F(UnificationTest, SubstApplyNested) {
+    // σ = {X → f(a)}    apply to g(X, b) → g(f(a), b)
+    Substitution subst;
+    subst.bind(x_, f(a_));
+    TermId const result = subst.apply(g(x_, b_), bank_);
+    EXPECT_EQ(result, g(f(a_), b_));
+}
+
+TEST_F(UnificationTest, SubstOccursIn) {
+    Substitution const subst;
+    // X occurs in f(X)
+    EXPECT_TRUE(subst.occursIn(x_, f(x_), bank_));
+    // X occurs in g(a, f(X))
+    EXPECT_TRUE(subst.occursIn(x_, g(a_, f(x_)), bank_));
+    // X does NOT occur in f(a)
+    EXPECT_FALSE(subst.occursIn(x_, f(a_), bank_));
+    // X does NOT occur in Y (different variable)
+    EXPECT_FALSE(subst.occursIn(x_, y_, bank_));
+}
+
+TEST_F(UnificationTest, SubstClearAndSize) {
+    Substitution subst;
+    EXPECT_TRUE(subst.empty());
+    subst.bind(x_, a_);
+    subst.bind(y_, b_);
+    EXPECT_EQ(subst.size(), 2);
+    subst.clear();
+    EXPECT_TRUE(subst.empty());
+    EXPECT_EQ(subst.lookup(x_), kInvalidId);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Unification Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(UnificationTest, UnifyIdenticalConstants) {
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, a_, a_, subst));
+    EXPECT_TRUE(subst.empty());
+}
+
+TEST_F(UnificationTest, UnifyDifferentConstants) {
+    Substitution subst;
+    EXPECT_FALSE(unify(bank_, a_, b_, subst));
+}
+
+TEST_F(UnificationTest, UnifyVarWithConstant) {
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, x_, a_, subst));
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
+}
+
+TEST_F(UnificationTest, UnifyConstantWithVar) {
+    // Symmetric: unify(a, X) should also work
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, a_, x_, subst));
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
+}
+
+TEST_F(UnificationTest, UnifyTwoVariables) {
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, x_, y_, subst));
+    // One should be bound to the other
+    TermId const rx = subst.resolve(x_, bank_);
+    TermId const ry = subst.resolve(y_, bank_);
+    EXPECT_EQ(rx, ry);
+}
+
+TEST_F(UnificationTest, UnifyCompoundTerms) {
+    // f(X) =? f(a)  → {X → a}
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, f(x_), f(a_), subst));
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
+}
+
+TEST_F(UnificationTest, UnifyMultipleArgs) {
+    // g(X, Y) =? g(a, b)  → {X → a, Y → b}
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, g(x_, y_), g(a_, b_), subst));
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
+    EXPECT_EQ(subst.resolve(y_, bank_), b_);
+}
+
+TEST_F(UnificationTest, UnifyConflictingBindings) {
+    // g(X, X) =? g(a, b)  → fails (X can't be both a and b)
+    Substitution subst;
+    EXPECT_FALSE(unify(bank_, g(x_, x_), g(a_, b_), subst));
+}
+
+TEST_F(UnificationTest, UnifyConsistentRepeatedVar) {
+    // g(X, X) =? g(a, a)  → {X → a}
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, g(x_, x_), g(a_, a_), subst));
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
+}
+
+TEST_F(UnificationTest, UnifyDifferentHeadSymbols) {
+    // f(X) =? h(X) → fails
+    Substitution subst;
+    EXPECT_FALSE(unify(bank_, f(x_), h(x_), subst));
+}
+
+TEST_F(UnificationTest, UnifyDifferentArity) {
+    // f(X) =? g(X, Y) → fails (arity 1 vs 2)
+    Substitution subst;
+    EXPECT_FALSE(unify(bank_, f(x_), g(x_, y_), subst));
+}
+
+TEST_F(UnificationTest, UnifyNestedTerms) {
+    // f(g(X, a)) =? f(Y)  → {Y → g(X, a)}
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, f(g(x_, a_)), f(y_), subst));
+    EXPECT_EQ(subst.resolve(y_, bank_), g(x_, a_));
+}
+
+TEST_F(UnificationTest, UnifyVarWithCompound) {
+    // X =? f(a) → {X → f(a)}
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, x_, f(a_), subst));
+    EXPECT_EQ(subst.resolve(x_, bank_), f(a_));
+}
+
+TEST_F(UnificationTest, UnifyDeepNesting) {
+    // f(f(f(X))) =? f(f(f(a))) → {X → a}
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, f(f(f(x_))), f(f(f(a_))), subst));
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
+}
+
+TEST_F(UnificationTest, UnifyChainedVariables) {
+    // g(X, Y) =? g(Y, a) → {X → Y, Y → a} effectively X → a
+    Substitution subst;
+    EXPECT_TRUE(unify(bank_, g(x_, y_), g(y_, a_), subst));
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
+    EXPECT_EQ(subst.resolve(y_, bank_), a_);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Occurs Check Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(UnificationTest, OccursCheckBlocks) {
+    // X =? f(X) with occurs check → fails
+    Substitution subst;
+    UnificationConfig const config{.enable_occurs_check_ = true};
+    EXPECT_FALSE(unify(bank_, x_, f(x_), subst, config));
+}
+
+TEST_F(UnificationTest, OccursCheckDisabledAllows) {
+    // X =? f(X) without occurs check → succeeds (unsound but fast)
+    Substitution subst;
+    UnificationConfig const config{.enable_occurs_check_ = false};
+    EXPECT_TRUE(unify(bank_, x_, f(x_), subst, config));
+}
+
+TEST_F(UnificationTest, OccursCheckDeep) {
+    // X =? f(g(X, a)) with occurs check → fails
+    Substitution subst;
+    UnificationConfig const config{.enable_occurs_check_ = true};
+    EXPECT_FALSE(unify(bank_, x_, f(g(x_, a_)), subst, config));
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// applySubstitution Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(UnificationTest, ApplySubstitutionSimple) {
+    Substitution subst;
+    subst.bind(x_, a_);
+    EXPECT_EQ(applySubstitution(subst, f(x_), bank_), f(a_));
+}
+
+TEST_F(UnificationTest, ApplySubstitutionNested) {
+    Substitution subst;
+    subst.bind(x_, a_);
+    subst.bind(y_, b_);
+    EXPECT_EQ(applySubstitution(subst, g(f(x_), y_), bank_), g(f(a_), b_));
+}
+
+TEST_F(UnificationTest, ApplySubstitutionPreservesUnbound) {
+    Substitution subst;
+    subst.bind(x_, a_);
+    // Y is unbound → stays as Y
+    EXPECT_EQ(applySubstitution(subst, g(x_, y_), bank_), g(a_, y_));
+}
+
+TEST_F(UnificationTest, ApplySubstitutionToConstant) {
+    Substitution subst;
+    subst.bind(x_, a_);
+    // Constant is unchanged
+    EXPECT_EQ(applySubstitution(subst, b_, bank_), b_);
+}
+
+TEST_F(UnificationTest, ApplySubstitutionChain) {
+    // σ = {X → Y, Y → a}   apply to f(X) → f(a)
+    Substitution subst;
+    subst.bind(x_, y_);
+    subst.bind(y_, a_);
+    EXPECT_EQ(applySubstitution(subst, f(x_), bank_), f(a_));
+}
+
+TEST_F(UnificationTest, UnifyThenApply) {
+    // Full round-trip: unify P(X, f(Y)) with P(a, f(b)), then apply
+    Substitution subst;
+    TermId const lhs = p(x_, f(y_));
+    TermId const rhs = p(a_, f(b_));
+    ASSERT_TRUE(unify(bank_, lhs, rhs, subst));
+
+    EXPECT_EQ(applySubstitution(subst, lhs, bank_), p(a_, f(b_)));
+    EXPECT_EQ(applySubstitution(subst, rhs, bank_), p(a_, f(b_)));
+    // Both sides should produce the same term after applying the MGU
+    EXPECT_EQ(applySubstitution(subst, lhs, bank_), applySubstitution(subst, rhs, bank_));
+}
+
+}  // namespace
+}  // namespace atp