refactor: rename struct members to follow trailing underscore naming convention across core, search, and frontend components

7 files changed, 531 insertions, 519 deletions

diff --git a/tests/test_end_to_end.cc b/tests/test_end_to_end.cc
index d45a101..ceb9991 100644
--- a/tests/test_end_to_end.cc
+++ b/tests/test_end_to_end.cc
@@ -28,14 +28,15 @@
 
 #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;
+    ProverResult result_;
+    std::string proof_output_;
 };
 
 E2EResult runProver(const std::string& tptp_input) {
@@ -48,7 +49,7 @@ E2EResult runProver(const std::string& tptp_input) {
 
     Prover prover(bank, store);
     prover.addClauses(std::move(clauses));
-    ProverResult result = prover.prove();
+    ProverResult const result = prover.prove();
 
     std::string proof_output;
     if (result == ProverResult::kTheorem) {
@@ -140,10 +141,10 @@ TEST(EndToEnd, ProofOutputContainsAllSteps) {
     // Must contain [resolution] for derived clauses
     EXPECT_NE(proof.find("[resolution]"), std::string::npos) << proof;
     // Must contain empty clause marker
-    std::string empty_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;
+    EXPECT_NE(proof.find('['), std::string::npos) << proof;
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
diff --git a/tests/test_proof_trace.cc b/tests/test_proof_trace.cc
index 5e12060..f2c3c96 100644
--- a/tests/test_proof_trace.cc
+++ b/tests/test_proof_trace.cc
@@ -27,43 +27,45 @@
 
 #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;
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
+    ClauseStore store_;
 
-    SymbolId sym_a{}, sym_b{};
-    SymbolId sym_P{}, sym_Q{};
-    SymbolId sym_X{};
+    SymbolId sym_a_{}, sym_b_{};
+    SymbolId sym_p_{}, sym_q_{};
+    SymbolId sym_x_{};
 
-    TermId a_term{}, b_term{}, X_term{};
+    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);
+        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}}); }
+    TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); }
+    TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); }
 
-    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
-    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
 
-    Clause makeClause(std::vector<Literal> lits) {
+    static Clause makeClause(std::vector<Literal> lits) {
         Clause cl;
-        cl.literals = std::move(lits);
+        cl.literals_ = std::move(lits);
         return cl;
     }
 };
@@ -73,23 +75,23 @@ class ProofTraceTest : public ::testing::Test {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProofTraceTest, TermToStringConstant) {
-    EXPECT_EQ(termToString(a_term, bank), "a");
+    EXPECT_EQ(termToString(a_term_, bank_), "a");
 }
 
 TEST_F(ProofTraceTest, TermToStringVariable) {
-    EXPECT_EQ(termToString(X_term, bank), "X");
+    EXPECT_EQ(termToString(x_term_, bank_), "X");
 }
 
 TEST_F(ProofTraceTest, TermToStringCompound) {
-    TermId pa = P(a_term);
-    EXPECT_EQ(termToString(pa, bank), "P(a)");
+    TermId const pa = p(a_term_);
+    EXPECT_EQ(termToString(pa, bank_), "P(a)");
 }
 
 TEST_F(ProofTraceTest, TermToStringNested) {
-    SymbolId sym_f = symbols.intern("f", SymbolKind::kFunction, 1);
-    TermId fa = bank.makeTerm(sym_f, {{a_term}});
-    TermId pfa = P(fa);
-    EXPECT_EQ(termToString(pfa, bank), "P(f(a))");
+    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))");
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -97,23 +99,23 @@ TEST_F(ProofTraceTest, TermToStringNested) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProofTraceTest, ClauseToStringEmpty) {
-    Clause empty = makeClause({});
-    EXPECT_EQ(clauseToString(empty, bank), "□");
+    Clause const empty = makeClause({});
+    EXPECT_EQ(clauseToString(empty, bank_), "□");
 }
 
 TEST_F(ProofTraceTest, ClauseToStringSinglePositive) {
-    Clause c = makeClause({pos(P(a_term))});
-    EXPECT_EQ(clauseToString(c, bank), "P(a)");
+    Clause const c = makeClause({pos(p(a_term_))});
+    EXPECT_EQ(clauseToString(c, bank_), "P(a)");
 }
 
 TEST_F(ProofTraceTest, ClauseToStringSingleNegative) {
-    Clause c = makeClause({neg(P(a_term))});
-    EXPECT_EQ(clauseToString(c, bank), "¬P(a)");
+    Clause const c = makeClause({neg(p(a_term_))});
+    EXPECT_EQ(clauseToString(c, bank_), "¬P(a)");
 }
 
 TEST_F(ProofTraceTest, ClauseToStringMultipleLiterals) {
-    Clause c = makeClause({neg(P(X_term)), pos(Q(X_term))});
-    std::string s = clauseToString(c, bank);
+    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)");
 }
 
@@ -123,42 +125,42 @@ TEST_F(ProofTraceTest, ClauseToStringMultipleLiterals) {
 
 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 result = prover.prove();
+    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
+    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);
+    EXPECT_EQ(proof.front().rule_, InferenceRule::kInput);
     // Last step should be the empty clause
-    EXPECT_EQ(proof.back().clause_id, *eid);
+    EXPECT_EQ(proof.back().clause_id_, *eid);
     // Last step should be resolution
-    EXPECT_EQ(proof.back().rule, InferenceRule::kResolution);
+    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 result = prover.prove();
+    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);
+    auto proof = extractProof(store_, *eid);
     // Should have axioms + intermediate + empty clause
-    ASSERT_GE(proof.size(), 4u);  // 3 axioms + at least 1 intermediate + empty
+    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);
+    EXPECT_EQ(proof.back().clause_id_, *eid);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -166,33 +168,33 @@ TEST_F(ProofTraceTest, ExtractProofTwoStep) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProofTraceTest, FormatProofContainsExpectedElements) {
-    Prover prover(bank, store);
-    prover.addClauses({makeClause({pos(P(a_term))}), makeClause({neg(P(a_term))})});
+    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 output = formatProof(proof, store, bank);
+    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 empty_marker = "□";
+    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 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 output = formatProof(proof, store, bank);
+    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
diff --git a/tests/test_prover.cc b/tests/test_prover.cc
index ada1af2..74d02ad 100644
--- a/tests/test_prover.cc
+++ b/tests/test_prover.cc
@@ -25,50 +25,53 @@
 #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;
+    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{};
+    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_{};
 
-    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);
+        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}}); }
+    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}}); }
 
-    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
-    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
 
-    Clause makeClause(std::vector<Literal> lits) {
+    static Clause makeClause(std::vector<Literal> lits) {
         Clause cl;
-        cl.literals = std::move(lits);
+        cl.literals_ = std::move(lits);
         return cl;
     }
 };
@@ -78,11 +81,11 @@ class ProverTest : public ::testing::Test {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProverTest, TrivialRefutation) {
-    Prover prover(bank, store);
-    prover.addClauses({makeClause({pos(P(a))}), makeClause({neg(P(a))})});
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_))}), makeClause({neg(p(a_))})});
 
-    ProverResult result = prover.prove();
-    EXPECT_EQ(result, ProverResult::kTheorem);
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
     EXPECT_TRUE(prover.getEmptyClauseId().has_value());
 }
 
@@ -91,11 +94,11 @@ TEST_F(ProverTest, TrivialRefutation) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProverTest, RefutationWithUnification) {
-    Prover prover(bank, store);
-    prover.addClauses({makeClause({pos(P(X))}), makeClause({neg(P(a))})});
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(x_))}), makeClause({neg(p(a_))})});
 
-    ProverResult result = prover.prove();
-    EXPECT_EQ(result, ProverResult::kTheorem);
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -105,12 +108,12 @@ TEST_F(ProverTest, RefutationWithUnification) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProverTest, TwoStepRefutation) {
-    Prover prover(bank, store);
+    Prover prover(bank_, store_);
     prover.addClauses(
-        {makeClause({pos(P(a))}), makeClause({neg(P(X)), pos(Q(X))}), makeClause({neg(Q(a))})});
+        {makeClause({pos(p(a_))}), makeClause({neg(p(x_)), pos(q(x_))}), makeClause({neg(q(a_))})});
 
-    ProverResult result = prover.prove();
-    EXPECT_EQ(result, ProverResult::kTheorem);
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -118,11 +121,11 @@ TEST_F(ProverTest, TwoStepRefutation) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProverTest, Saturation) {
-    Prover prover(bank, store);
-    prover.addClauses({makeClause({pos(P(a))}), makeClause({pos(Q(b))})});
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_))}), makeClause({pos(q(b_))})});
 
-    ProverResult result = prover.prove();
-    EXPECT_EQ(result, ProverResult::kSaturation);
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kSaturation);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -131,15 +134,15 @@ TEST_F(ProverTest, Saturation) {
 
 TEST_F(ProverTest, Timeout) {
     ProverConfig config;
-    config.max_iterations = 1;
+    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))})});
+    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_))})});
 
-    ProverResult result = prover.prove();
-    EXPECT_EQ(result, ProverResult::kTimeout);
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTimeout);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -147,19 +150,19 @@ TEST_F(ProverTest, Timeout) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProverTest, ThreeStepChain) {
-    SymbolId sym_S = symbols.intern("S", SymbolKind::kPredicate, 1);
-    auto S = [&](TermId arg) { return bank.makeTerm(sym_S, {{arg}}); };
+    const SymbolId kSymS = symbols_.intern("S", SymbolKind::kPredicate, 1);
+    auto s = [&](TermId arg) { return bank_.makeTerm(kSymS, {{arg}}); };
 
-    Prover prover(bank, store);
+    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)
+        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)
     });
 
-    ProverResult result = prover.prove();
-    EXPECT_EQ(result, ProverResult::kTheorem);
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -167,13 +170,13 @@ TEST_F(ProverTest, ThreeStepChain) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ProverTest, EmptyClauseInInput) {
-    Prover prover(bank, store);
+    Prover prover(bank_, store_);
     prover.addClauses({makeClause({}),  // empty clause directly
-                       makeClause({pos(P(a))})});
+                       makeClause({pos(p(a_))})});
 
     // Empty clause should be detected immediately when selected from queue
-    ProverResult result = prover.prove();
-    EXPECT_EQ(result, ProverResult::kTheorem);
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
 }
 
 }  // namespace
diff --git a/tests/test_resolution.cc b/tests/test_resolution.cc
index 931635d..02250d9 100644
--- a/tests/test_resolution.cc
+++ b/tests/test_resolution.cc
@@ -22,62 +22,62 @@
 #include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 #include "atp/infer/resolution.h"
-#include "atp/infer/substitution.h"
-#include "atp/infer/unification.h"
 
 #include <gtest/gtest.h>
+#include <utility>
+#include <vector>
 
 namespace atp {
 namespace {
 
 class ResolutionTest : public ::testing::Test {
   protected:
-    SymbolTable symbols;
-    TermBank bank{symbols};
+    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{};
+    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{};
+    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);
+        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}}); }
+    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
-    Clause makeClause(std::vector<Literal> lits, ClauseId id = kInvalidId) {
+    static Clause makeClause(std::vector<Literal> lits, ClauseId id = kInvalidId) {
         Clause c;
-        c.id = id;
-        c.literals = std::move(lits);
+        c.id_ = id;
+        c.literals_ = std::move(lits);
         return c;
     }
 
-    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
-    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
 };
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -86,86 +86,86 @@ class ResolutionTest : public ::testing::Test {
 
 TEST_F(ResolutionTest, SimpleGroundResolution) {
     // {P(a)} and {¬P(a), Q(b)}  → {Q(b)}
-    Clause c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({neg(P(a)), pos(Q(b))}, 1);
+    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);
+    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);
+    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 c1 = makeClause({pos(P(X))}, 0);
-    Clause c2 = makeClause({neg(P(a))}, 1);
+    Clause const c1 = makeClause({pos(p(x_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    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 c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({pos(P(b))}, 1);
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({pos(p(b_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    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 c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({neg(P(b))}, 1);
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(b_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    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 c1 = makeClause({pos(P(X)), pos(Q(X))}, 0);
-    Clause c2 = makeClause({neg(P(a))}, 1);
+    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);
+    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));
+    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 c1 = makeClause({pos(P(X)), pos(Q(b))}, 0);
-    Clause c2 = makeClause({neg(P(a)), pos(R(a, c))}, 1);
+    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);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
-    EXPECT_EQ(result->literals.size(), 2);
+    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 c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({neg(P(X)), pos(Q(X))}, 1);
+    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);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
-    EXPECT_EQ(result->literals.size(), 1);
+    EXPECT_EQ(result->literals_.size(), 1);
     // Q(X) should become Q(a) after substitution {X→a}
-    EXPECT_EQ(result->literals[0].atom, Q(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 c1 = makeClause({pos(R(X, a))}, 0);
-    Clause c2 = makeClause({neg(R(b, X))}, 1);
+    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);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
     EXPECT_TRUE(result->isEmpty());
 }
@@ -177,19 +177,19 @@ TEST_F(ResolutionTest, VariableRenamingPreventsClash) {
 TEST_F(ResolutionTest, AllResolventsFindsAll) {
     // {P(a), Q(a)} and {¬P(a), ¬Q(a)}
     // Can resolve on P or Q → 2 resolvents
-    Clause c1 = makeClause({pos(P(a)), pos(Q(a))}, 0);
-    Clause c2 = makeClause({neg(P(a)), neg(Q(a))}, 1);
+    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);
+    auto results = allResolvents(bank_, c1, c2);
     EXPECT_EQ(results.size(), 2);
 }
 
 TEST_F(ResolutionTest, AllResolventsEmpty) {
     // {P(a)} and {Q(b)} → no complementary pairs
-    Clause c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({pos(Q(b))}, 1);
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({pos(q(b_))}, 1);
 
-    auto results = allResolvents(bank, c1, c2);
+    auto results = allResolvents(bank_, c1, c2);
     EXPECT_TRUE(results.empty());
 }
 
@@ -199,34 +199,34 @@ TEST_F(ResolutionTest, AllResolventsEmpty) {
 
 TEST_F(ResolutionTest, SimpleFactoring) {
     // {P(X), P(a), Q(X)} → factor P(X) with P(a): {P(a), Q(a)}
-    Clause c = makeClause({pos(P(X)), pos(P(a)), pos(Q(X))}, 0);
+    Clause const c = makeClause({pos(p(x_)), pos(p(a_)), pos(q(x_))}, 0);
 
-    auto results = factor(bank, c);
+    auto results = factor(bank_, c);
     ASSERT_EQ(results.size(), 1);
-    EXPECT_EQ(results[0].literals.size(), 2);
+    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));
+    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 c = makeClause({pos(P(a)), pos(Q(b))}, 0);
-    auto results = factor(bank, c);
+    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 c = makeClause({pos(P(a)), neg(P(a))}, 0);
-    auto results = factor(bank, c);
+    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 c = makeClause({pos(P(a)), pos(P(b))}, 0);
-    auto results = factor(bank, c);
+    Clause const c = makeClause({pos(p(a_)), pos(p(b_))}, 0);
+    auto results = factor(bank_, c);
     EXPECT_TRUE(results.empty());
 }
 
@@ -235,22 +235,22 @@ TEST_F(ResolutionTest, FactoringNonUnifiable) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ResolutionTest, ResolventHasProvenance) {
-    Clause c1 = makeClause({pos(P(X))}, 5);
-    Clause c2 = makeClause({neg(P(a))}, 7);
+    Clause const c1 = makeClause({pos(p(x_))}, 5);
+    Clause const c2 = makeClause({neg(p(a_))}, 7);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    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);
+    EXPECT_EQ(result->rule_, InferenceRule::kResolution);
+    EXPECT_EQ(result->parent1_, 5);
+    EXPECT_EQ(result->parent2_, 7);
 }
 
 TEST_F(ResolutionTest, FactoredHasProvenance) {
-    Clause c = makeClause({pos(P(X)), pos(P(a))}, 3);
-    auto results = factor(bank, c);
+    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);
+    EXPECT_EQ(results[0].rule_, InferenceRule::kFactoring);
+    EXPECT_EQ(results[0].parent1_, 3);
 }
 
 }  // namespace
diff --git a/tests/test_simplify.cc b/tests/test_simplify.cc
index 98b0db9..968ab3b 100644
--- a/tests/test_simplify.cc
+++ b/tests/test_simplify.cc
@@ -25,46 +25,48 @@
 #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};
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
 
-    SymbolId sym_a{}, sym_b{}, sym_c{};
-    SymbolId sym_P{}, sym_Q{}, sym_R{};
-    SymbolId sym_X{};
+    SymbolId sym_a_{}, sym_b_{}, sym_c_{};
+    SymbolId sym_p_{}, sym_q_{}, sym_r_{};
+    SymbolId sym_x_{};
 
-    TermId a{}, b{}, c{}, 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);
+        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}}); }
+    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}}); }
 
-    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
-    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
 
-    Clause makeClause(std::vector<Literal> lits) {
+    static Clause makeClause(std::vector<Literal> lits) {
         Clause cl;
-        cl.literals = std::move(lits);
+        cl.literals_ = std::move(lits);
         return cl;
     }
 };
@@ -75,53 +77,53 @@ class SimplifyTest : public ::testing::Test {
 
 TEST_F(SimplifyTest, TautologyComplementaryLiterals) {
     // {P(a), ¬P(a)} → tautology
-    Clause cl = makeClause({pos(P(a)), neg(P(a))});
+    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 cl = makeClause({pos(Q(b)), pos(P(a)), neg(P(a))});
+    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 cl = makeClause({pos(P(a)), pos(P(a))});
+    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 cl = makeClause({pos(P(a)), neg(P(b))});
+    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 cl = makeClause({pos(P(a)), neg(Q(a))});
+    Clause const cl = makeClause({pos(p(a_)), neg(q(a_))});
     EXPECT_FALSE(isTautology(cl));
 }
 
 TEST_F(SimplifyTest, NotTautologyEmptyClause) {
-    Clause cl = makeClause({});
+    Clause const cl = makeClause({});
     EXPECT_FALSE(isTautology(cl));
 }
 
 TEST_F(SimplifyTest, NotTautologySingleLiteral) {
-    Clause cl = makeClause({pos(P(a))});
+    Clause const cl = makeClause({pos(p(a_))});
     EXPECT_FALSE(isTautology(cl));
 }
 
 TEST_F(SimplifyTest, TautologyVariableAtom) {
     // {P(X), ¬P(X)} → tautology (same variable term)
-    Clause cl = makeClause({pos(P(X)), neg(P(X))});
+    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 cl = makeClause({pos(P(X)), neg(P(a))});
+    Clause const cl = makeClause({pos(p(x_)), neg(p(a_))});
     EXPECT_FALSE(isTautology(cl));
 }
 
@@ -131,57 +133,57 @@ TEST_F(SimplifyTest, NotTautologyVarVsConst) {
 
 TEST_F(SimplifyTest, SubsumesSubset) {
     // {P(a)} subsumes {P(a), Q(b)}
-    Clause gen = makeClause({pos(P(a))});
-    Clause spec = makeClause({pos(P(a)), pos(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 c1 = makeClause({pos(P(a)), pos(Q(b))});
-    Clause c2 = makeClause({pos(P(a)), pos(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 empty = makeClause({});
-    Clause cl = makeClause({pos(P(a)), neg(Q(b))});
+    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 gen = makeClause({pos(P(a)), pos(Q(b))});
-    Clause spec = makeClause({pos(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 gen = makeClause({pos(P(a))});
-    Clause spec = makeClause({neg(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 gen = makeClause({pos(P(a))});
-    Clause spec = makeClause({pos(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 gen = makeClause({neg(P(a))});
-    Clause spec = makeClause({neg(P(a)), pos(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 gen = makeClause({pos(Q(b)), pos(P(a))});
-    Clause spec = makeClause({pos(P(a)), pos(Q(b)), pos(R(a, b))});
+    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));
 }
 
diff --git a/tests/test_term_bank.cc b/tests/test_term_bank.cc
index 3ea15ac..0d4fcc7 100644
--- a/tests/test_term_bank.cc
+++ b/tests/test_term_bank.cc
@@ -24,7 +24,11 @@
 #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 {
@@ -35,39 +39,39 @@ namespace {
 
 TEST(SymbolTableTest, InternReturnsConsistentId) {
     SymbolTable st;
-    SymbolId id1 = st.intern("foo", SymbolKind::kFunction, 2);
-    SymbolId id2 = st.intern("foo", SymbolKind::kFunction, 2);
+    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 a = st.intern("a", SymbolKind::kConstant);
-    SymbolId b = st.intern("b", SymbolKind::kConstant);
+    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 id = st.intern("hello", SymbolKind::kFunction, 1);
+    SymbolId const id = st.intern("hello", SymbolKind::kFunction, 1);
     EXPECT_EQ(st.getName(id), "hello");
 }
 
 TEST(SymbolTableTest, GetInfoPreservesMetadata) {
     SymbolTable st;
-    SymbolId id = st.intern("P", SymbolKind::kPredicate, 3, 42);
+    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);
+    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 var = st.intern("X", SymbolKind::kVariable);
-    SymbolId con = st.intern("a", SymbolKind::kConstant);
-    SymbolId fun = st.intern("f", SymbolKind::kFunction, 1);
+    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));
@@ -102,123 +106,123 @@ TEST(SymbolTableTest, SizeTracksInternedSymbols) {
 
 class TermBankTest : public ::testing::Test {
   protected:
-    SymbolTable symbols;
-    TermBank bank{symbols};
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
 
-    SymbolId sym_a, sym_b, sym_f, sym_g, sym_X, sym_Y;
+    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 = symbols.intern("X", SymbolKind::kVariable);
-        sym_Y = symbols.intern("Y", SymbolKind::kVariable);
+        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) {
-    TermId a1 = bank.makeTerm(sym_a, {});
-    TermId a2 = bank.makeTerm(sym_a, {});
-    EXPECT_EQ(a1, a2) << "Hash consing failed: same term got different IDs";
+    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) {
-    TermId a = bank.makeTerm(sym_a, {});
-    TermId b = bank.makeTerm(sym_b, {});
-    EXPECT_NE(a, b);
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    const TermId kB = bank_.makeTerm(sym_b_, {});
+    EXPECT_NE(kA, kB);
 }
 
 TEST_F(TermBankTest, CompoundTermHashConsing) {
-    TermId a = bank.makeTerm(sym_a, {});
-    TermId b = bank.makeTerm(sym_b, {});
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    const TermId kB = bank_.makeTerm(sym_b_, {});
     // f(a)
-    TermId fa1 = bank.makeTerm(sym_f, {{a}});
-    TermId fa2 = bank.makeTerm(sym_f, {{a}});
-    EXPECT_EQ(fa1, fa2);
+    const TermId kFA1 = bank_.makeTerm(sym_f_, {{kA}});
+    const TermId kFA2 = bank_.makeTerm(sym_f_, {{kA}});
+    EXPECT_EQ(kFA1, kFA2);
     // f(b) != f(a)
-    TermId fb = bank.makeTerm(sym_f, {{b}});
-    EXPECT_NE(fa1, fb);
+    const TermId kFB = bank_.makeTerm(sym_f_, {{kB}});
+    EXPECT_NE(kFA1, kFB);
 }
 
 TEST_F(TermBankTest, NestedTermHashConsing) {
-    TermId a = bank.makeTerm(sym_a, {});
-    TermId fa = bank.makeTerm(sym_f, {{a}});
+    const TermId kA = bank_.makeTerm(sym_a_, {});
+    const TermId kFA = bank_.makeTerm(sym_f_, {{kA}});
     // g(f(a), a)
-    TermId gfa_a_1 = bank.makeTerm(sym_g, {{fa, a}});
-    TermId gfa_a_2 = bank.makeTerm(sym_g, {{fa, a}});
-    EXPECT_EQ(gfa_a_1, gfa_a_2);
+    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) {
-    TermId a = bank.makeTerm(sym_a, {});
-    const Term& t = bank.getTerm(a);
-    EXPECT_EQ(t.symbol_id, sym_a);
+    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) {
-    TermId a = bank.makeTerm(sym_a, {});
-    TermId b = bank.makeTerm(sym_b, {});
-    TermId gab = bank.makeTerm(sym_g, {{a, b}});
+    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(gab);
-    EXPECT_EQ(t.symbol_id, sym_g);
+    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], a);
-    EXPECT_EQ(t.args[1], b);
+    ASSERT_EQ(t.args_.size(), 2);
+    EXPECT_EQ(t.args_[0], kA);
+    EXPECT_EQ(t.args_[1], kB);
 }
 
 TEST_F(TermBankTest, MakeVarCreatesZeroArityTerm) {
-    TermId x = bank.makeVar(sym_X);
-    const Term& t = bank.getTerm(x);
-    EXPECT_EQ(t.symbol_id, sym_X);
+    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());
+    EXPECT_TRUE(t.args_.empty());
 }
 
 TEST_F(TermBankTest, IsVariableDistinguishesFromConstants) {
-    TermId x = bank.makeVar(sym_X);
-    TermId a = bank.makeTerm(sym_a, {});
+    const TermId kX = bank_.makeVar(sym_x_id_);
+    const TermId kA = bank_.makeTerm(sym_a_, {});
 
-    EXPECT_TRUE(bank.isVariable(x)) << "Variable should be detected as variable";
-    EXPECT_FALSE(bank.isVariable(a)) << "Constant should NOT be detected as variable";
+    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) {
-    TermId x1 = bank.makeVar(sym_X);
-    TermId x2 = bank.makeVar(sym_X);
-    EXPECT_EQ(x1, x2);
+    const TermId kX1 = bank_.makeVar(sym_x_id_);
+    const TermId kX2 = bank_.makeVar(sym_x_id_);
+    EXPECT_EQ(kX1, kX2);
 
-    TermId y = bank.makeVar(sym_Y);
-    EXPECT_NE(x1, y);
+    const TermId kY = bank_.makeVar(sym_y_id_);
+    EXPECT_NE(kX1, kY);
 }
 
 TEST_F(TermBankTest, SizeTracksUniqueTerms) {
-    EXPECT_EQ(bank.size(), 0);
-    TermId a = 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, {{a}});
-    EXPECT_EQ(bank.size(), 3);
+    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
-    TermId x = bank.makeVar(sym_X);
-    TermId fx = bank.makeTerm(sym_f, {{x}});
+    const TermId kX = bank_.makeVar(sym_x_id_);
+    const TermId kFX = bank_.makeTerm(sym_f_, {{kX}});
 
-    const Term& t = bank.getTerm(fx);
-    EXPECT_EQ(t.symbol_id, sym_f);
+    const Term& t = bank_.getTerm(kFX);
+    EXPECT_EQ(t.symbol_id_, sym_f_);
     EXPECT_EQ(t.arity(), 1);
-    EXPECT_EQ(t.args[0], x);
+    EXPECT_EQ(t.args_[0], kX);
 
-    EXPECT_FALSE(bank.isVariable(fx));
-    EXPECT_TRUE(bank.isVariable(x));
+    EXPECT_FALSE(bank_.isVariable(kFX));
+    EXPECT_TRUE(bank_.isVariable(kX));
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -228,48 +232,48 @@ TEST_F(TermBankTest, CompoundTermWithVariableArgs) {
 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});
-
-    ClauseId id = store.addClause(std::move(c));
-    EXPECT_EQ(id, 0);
-
-    const Clause& retrieved = store.getClause(id);
-    EXPECT_EQ(retrieved.id, id);
-    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);
+    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;
-    ClauseId id0 = store.addClause(Clause{});
-    ClauseId id1 = store.addClause(Clause{});
-    ClauseId id2 = store.addClause(Clause{});
-    EXPECT_EQ(id0, 0);
-    EXPECT_EQ(id1, 1);
-    EXPECT_EQ(id2, 2);
+    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
-    ClauseId id = store.addClause(std::move(c));
-    EXPECT_EQ(store.getClause(id).id, id);
+    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;
-    ClauseId id = store.addClause(std::move(c));
+    c.depth_ = 0;
+    const ClauseId kId = store.addClause(std::move(c));
 
-    store.getMutableClause(id).depth = 42;
-    EXPECT_EQ(store.getClause(id).depth, 42);
+    store.getMutableClause(kId).depth_ = 42;
+    EXPECT_EQ(store.getClause(kId).depth_, 42);
 }
 
 TEST(ClauseStoreTest, ForEachVisitsAll) {
@@ -286,7 +290,7 @@ TEST(ClauseStoreTest, ForEachVisitsAll) {
 TEST(ClauseStoreTest, EmptyClauseDetection) {
     Clause c;
     EXPECT_TRUE(c.isEmpty());
-    c.literals.push_back(Literal{.atom = 0, .is_positive = true});
+    c.literals_.push_back(Literal{.atom_ = 0, .is_positive_ = true});
     EXPECT_FALSE(c.isEmpty());
     EXPECT_EQ(c.size(), 1);
 }
@@ -294,17 +298,17 @@ TEST(ClauseStoreTest, EmptyClauseDetection) {
 TEST(ClauseStoreTest, ProvenancePreserved) {
     ClauseStore store;
     Clause c;
-    c.rule = InferenceRule::kResolution;
-    c.parent1 = 3;
-    c.parent2 = 7;
-    c.depth = 5;
+    c.rule_ = InferenceRule::kResolution;
+    c.parent1_ = 3;
+    c.parent2_ = 7;
+    c.depth_ = 5;
 
-    ClauseId id = store.addClause(std::move(c));
+    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);
+    EXPECT_EQ(retrieved.rule_, InferenceRule::kResolution);
+    EXPECT_EQ(retrieved.parent1_, 3);
+    EXPECT_EQ(retrieved.parent2_, 7);
+    EXPECT_EQ(retrieved.depth_, 5);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -312,23 +316,23 @@ TEST(ClauseStoreTest, ProvenancePreserved) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST(LiteralTest, Complement) {
-    Literal pos{.atom = 42, .is_positive = true};
-    Literal neg = pos.complement();
-    EXPECT_EQ(neg.atom, 42);
-    EXPECT_FALSE(neg.is_positive);
+    const Literal kPos{.atom_ = 42, .is_positive_ = true};
+    const Literal kNeg = kPos.complement();
+    EXPECT_EQ(kNeg.atom_, 42);
+    EXPECT_FALSE(kNeg.is_positive_);
 
-    Literal back = neg.complement();
-    EXPECT_EQ(back, pos);
+    const Literal kBack = kNeg.complement();
+    EXPECT_EQ(kBack, kPos);
 }
 
 TEST(LiteralTest, Equality) {
-    Literal a{.atom = 1, .is_positive = true};
-    Literal b{.atom = 1, .is_positive = true};
-    Literal c{.atom = 1, .is_positive = false};
-    Literal d{.atom = 2, .is_positive = true};
-    EXPECT_EQ(a, b);
-    EXPECT_NE(a, c);
-    EXPECT_NE(a, d);
+    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
diff --git a/tests/test_unification.cc b/tests/test_unification.cc
index 516058a..63ac9f0 100644
--- a/tests/test_unification.cc
+++ b/tests/test_unification.cc
@@ -33,47 +33,47 @@ namespace {
 
 class UnificationTest : public ::testing::Test {
   protected:
-    SymbolTable symbols;
-    TermBank bank{symbols};
+    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{};
+    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{};
+    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);
+        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}}); }
+    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}}); }
+    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}}); }
+    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}}); }
+    TermId p(TermId a1, TermId a2) { return bank_.makeTerm(sym_p_, {{a1, a2}}); }
 };
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -82,90 +82,90 @@ class UnificationTest : public ::testing::Test {
 
 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
+    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
+    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
+    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);
+    subst.bind(x_, y_);
+    subst.bind(y_, a_);
+    EXPECT_EQ(subst.resolve(x_, bank_), a_);
 }
 
 TEST_F(UnificationTest, SubstResolveUnbound) {
-    Substitution subst;
-    EXPECT_EQ(subst.resolve(X, bank), X);  // unbound → returns itself
+    Substitution const subst;
+    EXPECT_EQ(subst.resolve(x_, bank_), x_);  // unbound → returns itself
 }
 
 TEST_F(UnificationTest, SubstResolveNonVariable) {
-    Substitution subst;
-    EXPECT_EQ(subst.resolve(a, bank), a);  // constant → returns itself
+    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 fx = f(X);
-    TermId result = subst.apply(fx, bank);
-    TermId expected = f(a);
+    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 gxy = g(X, Y);
-    TermId result = subst.apply(gxy, bank);
-    TermId expected = g(a, Y);
+    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 result = subst.apply(g(X, b), bank);
-    EXPECT_EQ(result, g(f(a), b));
+    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 subst;
+    Substitution const subst;
     // X occurs in f(X)
-    EXPECT_TRUE(subst.occursIn(X, f(X), bank));
+    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));
+    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));
+    EXPECT_FALSE(subst.occursIn(x_, f(a_), bank_));
     // X does NOT occur in Y (different variable)
-    EXPECT_FALSE(subst.occursIn(X, Y, bank));
+    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);
+    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);
+    EXPECT_EQ(subst.lookup(x_), kInvalidId);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -174,104 +174,104 @@ TEST_F(UnificationTest, SubstClearAndSize) {
 
 TEST_F(UnificationTest, UnifyIdenticalConstants) {
     Substitution subst;
-    EXPECT_TRUE(unify(bank, a, a, 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));
+    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);
+    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);
+    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));
+    EXPECT_TRUE(unify(bank_, x_, y_, subst));
     // One should be bound to the other
-    TermId rx = subst.resolve(X, bank);
-    TermId ry = subst.resolve(Y, bank);
+    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);
+    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);
+    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));
+    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);
+    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));
+    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));
+    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));
+    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));
+    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);
+    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);
+    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_);
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -281,22 +281,22 @@ TEST_F(UnificationTest, UnifyChainedVariables) {
 TEST_F(UnificationTest, OccursCheckBlocks) {
     // X =? f(X) with occurs check → fails
     Substitution subst;
-    UnificationConfig config{.enable_occurs_check = true};
-    EXPECT_FALSE(unify(bank, X, f(X), subst, config));
+    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 config{.enable_occurs_check = false};
-    EXPECT_TRUE(unify(bank, X, f(X), subst, config));
+    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 config{.enable_occurs_check = true};
-    EXPECT_FALSE(unify(bank, X, f(g(X, a)), subst, config));
+    UnificationConfig const config{.enable_occurs_check_ = true};
+    EXPECT_FALSE(unify(bank_, x_, f(g(x_, a_)), subst, config));
 }
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -305,50 +305,50 @@ TEST_F(UnificationTest, OccursCheckDeep) {
 
 TEST_F(UnificationTest, ApplySubstitutionSimple) {
     Substitution subst;
-    subst.bind(X, a);
-    EXPECT_EQ(applySubstitution(subst, f(X), bank), f(a));
+    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));
+    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);
+    subst.bind(x_, a_);
     // Y is unbound → stays as Y
-    EXPECT_EQ(applySubstitution(subst, g(X, Y), bank), g(a, Y));
+    EXPECT_EQ(applySubstitution(subst, g(x_, y_), bank_), g(a_, y_));
 }
 
 TEST_F(UnificationTest, ApplySubstitutionToConstant) {
     Substitution subst;
-    subst.bind(X, a);
+    subst.bind(x_, a_);
     // Constant is unchanged
-    EXPECT_EQ(applySubstitution(subst, b, bank), b);
+    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));
+    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 lhs = P(X, f(Y));
-    TermId rhs = P(a, f(b));
-    ASSERT_TRUE(unify(bank, lhs, rhs, 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)));
+    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));
+    EXPECT_EQ(applySubstitution(subst, lhs, bank_), applySubstitution(subst, rhs, bank_));
 }
 
 }  // namespace