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

31 files changed, 877 insertions, 809 deletions

diff --git a/include/atp/core/clause.h b/include/atp/core/clause.h
index 7e0cbff..6387adf 100644
--- a/include/atp/core/clause.h
+++ b/include/atp/core/clause.h
@@ -33,20 +33,20 @@ namespace atp {
 
 /// A clause: a disjunction of literals plus provenance for proof reconstruction.
 struct Clause {
-    ClauseId id = kInvalidId;
-    std::vector<Literal> literals;
+    ClauseId id_ = kInvalidId;
+    std::vector<Literal> literals_;
 
     // Provenance (for proof trace)
-    InferenceRule rule = InferenceRule::kInput;
-    ClauseId parent1 = kInvalidId;
-    ClauseId parent2 = kInvalidId;
-    uint16_t depth = 0;  ///< Derivation depth (for BFS scheduling)
+    InferenceRule rule_ = InferenceRule::kInput;
+    ClauseId parent1_ = kInvalidId;
+    ClauseId parent2_ = kInvalidId;
+    uint16_t depth_ = 0;  ///< Derivation depth (for BFS scheduling)
 
     /// True if the clause has no literals (contradiction).
-    [[nodiscard]] bool isEmpty() const { return literals.empty(); }
+    [[nodiscard]] bool isEmpty() const { return literals_.empty(); }
 
     /// Number of literals.
-    [[nodiscard]] size_t size() const { return literals.size(); }
+    [[nodiscard]] size_t size() const { return literals_.size(); }
 };
 
 }  // namespace atp
diff --git a/include/atp/core/literal.h b/include/atp/core/literal.h
index 212c281..e58b185 100644
--- a/include/atp/core/literal.h
+++ b/include/atp/core/literal.h
@@ -27,11 +27,11 @@ namespace atp {
 
 /// A literal: a polarity flag plus the TermId of the atom.
 struct Literal {
-    TermId atom;       ///< TermId of the predicate application
-    bool is_positive;  ///< true = positive, false = negated
+    TermId atom_;       ///< TermId of the predicate application
+    bool is_positive_;  ///< true = positive, false = negated
 
     /// Complement: flip polarity, same atom.
-    [[nodiscard]] Literal complement() const { return {.atom = atom, .is_positive = !is_positive}; }
+    [[nodiscard]] Literal complement() const { return {.atom_ = atom_, .is_positive_ = !is_positive_}; }
 
     bool operator==(const Literal& other) const = default;
 };
diff --git a/include/atp/core/symbol_table.h b/include/atp/core/symbol_table.h
index 30453fc..a646f78 100644
--- a/include/atp/core/symbol_table.h
+++ b/include/atp/core/symbol_table.h
@@ -33,10 +33,10 @@ namespace atp {
 
 /// Metadata associated with an interned symbol.
 struct SymbolInfo {
-    std::string name;
-    SymbolKind kind = SymbolKind::kFunction;
-    uint16_t arity = 0;
-    SortId sort = kUnsorted;  ///< Result sort (for sorted logic)
+    std::string name_;
+    SymbolKind kind_ = SymbolKind::kFunction;
+    uint16_t arity_ = 0;
+    SortId sort_ = kUnsorted;  ///< Result sort (for sorted logic)
 };
 
 /// Interns symbol names so that each unique string is stored exactly once.
diff --git a/include/atp/core/term.h b/include/atp/core/term.h
index 2be01e7..d35c753 100644
--- a/include/atp/core/term.h
+++ b/include/atp/core/term.h
@@ -33,11 +33,11 @@ namespace atp {
 /// A term is a function/predicate application: f(t1, t2, ..., tn).
 /// Variables are 0-arity terms whose symbol has SymbolKind::kVariable.
 struct Term {
-    SymbolId symbol_id;        ///< Index into the SymbolTable
-    std::vector<TermId> args;  ///< Argument sub-term IDs
+    SymbolId symbol_id_;        ///< Index into the SymbolTable
+    std::vector<TermId> args_;  ///< Argument sub-term IDs
 
     /// Number of arguments.
-    [[nodiscard]] uint16_t arity() const { return static_cast<uint16_t>(args.size()); }
+    [[nodiscard]] uint16_t arity() const { return static_cast<uint16_t>(args_.size()); }
 };
 
 }  // namespace atp
diff --git a/include/atp/core/term_bank.h b/include/atp/core/term_bank.h
index f909e2f..3339ceb 100644
--- a/include/atp/core/term_bank.h
+++ b/include/atp/core/term_bank.h
@@ -61,17 +61,17 @@ class TermBank {
 
   private:
     struct TermKey {
-        SymbolId symbol;
-        std::vector<TermId> args;
+        SymbolId symbol_;
+        std::vector<TermId> args_;
 
         bool operator==(const TermKey& other) const = default;
     };
 
     struct TermKeyHash {
         size_t operator()(const TermKey& key) const {
-            size_t seed = std::hash<uint32_t>{}(key.symbol);
-            for (TermId arg : key.args) {
-                seed ^= std::hash<uint32_t>{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+            size_t seed = std::hash<uint32_t>{}(key.symbol_);
+            for (const TermId kArg : key.args_) {
+                seed ^= std::hash<TermId>{}(kArg) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
             }
             return seed;
         }
diff --git a/include/atp/frontend/tptp_parser.h b/include/atp/frontend/tptp_parser.h
index 738d34b..89eab6b 100644
--- a/include/atp/frontend/tptp_parser.h
+++ b/include/atp/frontend/tptp_parser.h
@@ -58,22 +58,22 @@ FormulaRole parseRole(std::string_view role_str);
 
 /// A parsed TPTP formula with its name and role.
 struct AnnotatedFormula {
-    std::string name;                  ///< Formula name (e.g., "axiom1")
-    FormulaRole role;                  ///< Semantic role
-    std::unique_ptr<Formula> formula;  ///< The FOL formula (for fof(...))
-    std::vector<Clause> clauses;       ///< Direct clauses (for cnf(...))
-    bool is_cnf = false;               ///< true if input was cnf(), false if fof()
+    std::string name_;                  ///< Formula name (e.g., "axiom1")
+    FormulaRole role_;                  ///< Semantic role
+    std::unique_ptr<Formula> formula_;  ///< The FOL formula (for fof(...))
+    std::vector<Clause> clauses_;       ///< Direct clauses (for cnf(...))
+    bool is_cnf_ = false;               ///< true if input was cnf(), false if fof()
 };
 
 /// A complete parsed TPTP problem.
 struct ParsedProblem {
-    std::vector<AnnotatedFormula> formulas;
+    std::vector<AnnotatedFormula> formulas_;
 
     /// Does any formula contain an equality predicate?
-    bool has_equality = false;
+    bool has_equality_ = false;
 
     /// Original file path (for error messages).
-    std::string source_file;
+    std::string source_file_;
 };
 
 /// Parse a TPTP file.
@@ -82,7 +82,7 @@ struct ParsedProblem {
 /// For `fof(...)` entries: Formula AST is built (clausification happens later).
 ///
 /// All symbols are interned into `symbols` and terms into `bank` during parsing.
-ParsedProblem parseTptpFile(const std::string& filepath, TermBank& bank, SymbolTable& symbols);
+ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolTable& symbols);
 
 /// Parse a TPTP string (for testing).
 ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols);
diff --git a/include/atp/index/discrim_tree.h b/include/atp/index/discrim_tree.h
index c5954d7..5f8a206 100644
--- a/include/atp/index/discrim_tree.h
+++ b/include/atp/index/discrim_tree.h
@@ -37,8 +37,8 @@ namespace atp {
 
 /// A match result from the discrimination tree.
 struct IndexMatch {
-    ClauseId clause_id;
-    size_t lit_index;
+    ClauseId clause_id_;
+    size_t lit_index_;
 };
 
 /// A discrimination tree index over terms.
diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h
index 9a4b6cc..870be66 100644
--- a/include/atp/infer/unification.h
+++ b/include/atp/infer/unification.h
@@ -28,7 +28,7 @@ namespace atp {
 
 /// Configuration for the unification algorithm.
 struct UnificationConfig {
-    bool enable_occurs_check = false;  ///< Set true for sound but slower unification
+    bool enable_occurs_check_ = false;  ///< Set true for sound but slower unification
 };
 
 /// Attempt to unify two terms, producing a most general unifier.
diff --git a/include/atp/normalize/formula.h b/include/atp/normalize/formula.h
index 1bcc021..5ee9b94 100644
--- a/include/atp/normalize/formula.h
+++ b/include/atp/normalize/formula.h
@@ -51,18 +51,18 @@ enum class FormulaKind : uint8_t {
 /// All identifiers are interned: atoms as TermIds, quantifier variables as
 /// SymbolIds. No raw strings survive past the parser.
 struct Formula {
-    FormulaKind kind;
+    FormulaKind kind_;
 
     /// For kAtom / kEquality: the predicate/equality term, already interned.
-    TermId atom = kInvalidId;
+    TermId atom_ = kInvalidId;
 
     /// For kForall / kExists: the bound variable, as an interned SymbolId.
     /// Using SymbolId (not string) so the clausifier can map bound variables
     /// back to term-bank variables without string lookups.
-    SymbolId bound_var = kInvalidId;
+    SymbolId bound_var_ = kInvalidId;
 
     /// Sub-formulas (1 for Not/Quantifiers, 2 for binary connectives).
-    std::vector<std::unique_ptr<Formula>> children;
+    std::vector<std::unique_ptr<Formula>> children_;
 
     // ── Factory methods ──
 
diff --git a/include/atp/proof/proof_trace.h b/include/atp/proof/proof_trace.h
index 28099fe..4ea7aa1 100644
--- a/include/atp/proof/proof_trace.h
+++ b/include/atp/proof/proof_trace.h
@@ -32,10 +32,10 @@ namespace atp {
 
 /// A single step in a reconstructed proof.
 struct ProofStep {
-    ClauseId clause_id;
-    InferenceRule rule;
-    ClauseId parent1;
-    ClauseId parent2;
+    ClauseId clause_id_;
+    InferenceRule rule_;
+    ClauseId parent1_;
+    ClauseId parent2_;
 };
 
 /// Reconstruct the proof trace from the empty clause.
diff --git a/include/atp/search/clause_queue.h b/include/atp/search/clause_queue.h
index 6a8f9fc..dfb575c 100644
--- a/include/atp/search/clause_queue.h
+++ b/include/atp/search/clause_queue.h
@@ -32,12 +32,12 @@ using ClauseComparator = std::function<bool(const Clause& a, const Clause& b)>;
 
 /// BFS comparator: prioritize shallower derivation depth.
 inline bool bfsCompare(const Clause& a, const Clause& b) {
-    return a.depth > b.depth;  // min-heap by depth
+    return a.depth_ > b.depth_;  // min-heap by depth
 }
 
 /// Weight comparator: prioritize shorter (fewer literals) clauses.
 inline bool weightCompare(const Clause& a, const Clause& b) {
-    return a.literals.size() > b.literals.size();  // min-heap by literal count
+    return a.literals_.size() > b.literals_.size();  // min-heap by literal count
 }
 
 }  // namespace atp
diff --git a/include/atp/search/prover.h b/include/atp/search/prover.h
index 6ee22f0..c1246ae 100644
--- a/include/atp/search/prover.h
+++ b/include/atp/search/prover.h
@@ -46,10 +46,10 @@ enum class ProverResult : uint8_t {
 /// V1 configuration — simple and direct.
 /// Future: replaced by strategy::Calculus for dynamic rule loading.
 struct ProverConfig {
-    ClauseComparator comparator = bfsCompare;
-    size_t max_clauses = 100000;     ///< Safety limit
-    size_t max_iterations = 500000;  ///< Safety limit
-    bool enable_occurs_check = false;
+    ClauseComparator comparator_ = bfsCompare;
+    size_t max_clauses_ = 100000;     ///< Safety limit
+    size_t max_iterations_ = 500000;  ///< Safety limit
+    bool enable_occurs_check_ = false;
 };
 
 /// Main prover class implementing the Given Clause Loop.
diff --git a/src/core/clause_store.cc b/src/core/clause_store.cc
index 75959c3..f8ee73d 100644
--- a/src/core/clause_store.cc
+++ b/src/core/clause_store.cc
@@ -18,14 +18,19 @@
 
 #include "atp/core/clause_store.h"
 
+#include "atp/core/clause.h"
+#include "atp/core/types.h"
+
 #include <cassert>
+#include <cstddef>
+#include <functional>
 #include <utility>
 
 namespace atp {
 
 ClauseId ClauseStore::addClause(Clause clause) {
     auto new_id = static_cast<ClauseId>(clauses_.size());
-    clause.id = new_id;
+    clause.id_ = new_id;
     clauses_.push_back(std::move(clause));
     return new_id;
 }
diff --git a/src/core/symbol_table.cc b/src/core/symbol_table.cc
index 42c7dd8..b707132 100644
--- a/src/core/symbol_table.cc
+++ b/src/core/symbol_table.cc
@@ -21,7 +21,9 @@
 #include "atp/core/types.h"
 
 #include <cstddef>
+#include <cstdint>
 #include <stdexcept>
+#include <string>
 #include <string_view>
 
 namespace atp {
@@ -29,22 +31,23 @@ namespace atp {
 SymbolId SymbolTable::intern(std::string_view name, SymbolKind kind, uint16_t arity, SortId sort) {
     auto it = name_to_id_.find(name);
     if (it != name_to_id_.end()) {
-        SymbolId id = it->second;
-        SymbolInfo& info = infos_[id];
-        if (info.kind != kind || info.arity != arity) {
+        SymbolId const id = it->second;
+        SymbolInfo const& info = infos_[id];
+        if (info.kind_ != kind || info.arity_ != arity) {
             throw std::runtime_error("Symbol kind or arity mismatch for: " + std::string(name));
         }
         return id;
     }
     auto new_id = static_cast<SymbolId>(infos_.size());
-    infos_.push_back({.name = std::string(name), .kind = kind, .arity = arity, .sort = sort});
-    std::string_view stable_name_view = infos_.back().name;
+    infos_.push_back(SymbolInfo{
+        .name_ = std::string(name), .kind_ = kind, .arity_ = arity, .sort_ = sort});
+    std::string_view const stable_name_view = infos_.back().name_;
     name_to_id_.emplace(stable_name_view, new_id);
     return new_id;
 }
 
 std::string_view SymbolTable::getName(SymbolId id) const {
-    return infos_[id].name;
+    return infos_[id].name_;
 }
 
 const SymbolInfo& SymbolTable::getInfo(SymbolId id) const {
@@ -52,7 +55,7 @@ const SymbolInfo& SymbolTable::getInfo(SymbolId id) const {
 }
 
 bool SymbolTable::isVariable(SymbolId id) const {
-    return infos_[id].kind == SymbolKind::kVariable;
+    return infos_[id].kind_ == SymbolKind::kVariable;
 }
 
 size_t SymbolTable::size() const {
diff --git a/src/core/term_bank.cc b/src/core/term_bank.cc
index 8c8ef29..2e117b3 100644
--- a/src/core/term_bank.cc
+++ b/src/core/term_bank.cc
@@ -18,20 +18,25 @@
 
 #include "atp/core/term_bank.h"
 
+#include "atp/core/term.h"
 #include "atp/core/types.h"
 
 #include <cassert>
+#include <cstddef>
+#include <span>
+#include <utility>
+#include <vector>
 
 namespace atp {
 
 TermId TermBank::makeTerm(SymbolId symbol, std::span<const TermId> args) {
-    TermKey key{.symbol = symbol, .args = {args.begin(), args.end()}};
+    TermKey key{.symbol_ = symbol, .args_ = {args.begin(), args.end()}};
     auto it = term_to_id_.find(key);
     if (it != term_to_id_.end()) {
         return it->second;
     }
     auto new_id = static_cast<TermId>(terms_.size());
-    Term new_term{.symbol_id = symbol, .args = {args.begin(), args.end()}};
+    Term new_term{.symbol_id_ = symbol, .args_ = key.args_};
     terms_.push_back(std::move(new_term));
     term_to_id_.emplace(std::move(key), new_id);
     return new_id;
@@ -48,7 +53,7 @@ const Term& TermBank::getTerm(TermId id) const {
 
 bool TermBank::isVariable(TermId id) const {
     assert(id < terms_.size() && "TermId out of bounds!");
-    return symbols_.isVariable(terms_[id].symbol_id);
+    return symbols_.isVariable(terms_[id].symbol_id_);
 }
 
 size_t TermBank::size() const {
diff --git a/src/frontend/tptp_parser.cc b/src/frontend/tptp_parser.cc
index 2f32522..ddf8aad 100644
--- a/src/frontend/tptp_parser.cc
+++ b/src/frontend/tptp_parser.cc
@@ -20,96 +20,111 @@
 
 #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 <cctype>
+#include <cstddef>
+#include <cstdint>
 #include <fstream>
+#include <ios>
+#include <iterator>
 #include <stdexcept>
 #include <string>
 #include <string_view>
 #include <unordered_map>
+#include <utility>
 #include <vector>
 
 namespace atp {
 
 FormulaRole parseRole(std::string_view role_str) {
-    if (role_str == "axiom")
+    if (role_str == "axiom") {
         return FormulaRole::kAxiom;
-    if (role_str == "hypothesis")
+}
+    if (role_str == "hypothesis") {
         return FormulaRole::kHypothesis;
-    if (role_str == "definition")
+}
+    if (role_str == "definition") {
         return FormulaRole::kDefinition;
-    if (role_str == "assumption")
+}
+    if (role_str == "assumption") {
         return FormulaRole::kAssumption;
-    if (role_str == "lemma")
+}
+    if (role_str == "lemma") {
         return FormulaRole::kLemma;
-    if (role_str == "theorem")
+}
+    if (role_str == "theorem") {
         return FormulaRole::kTheorem;
-    if (role_str == "conjecture")
+}
+    if (role_str == "conjecture") {
         return FormulaRole::kConjecture;
-    if (role_str == "negated_conjecture")
+}
+    if (role_str == "negated_conjecture") {
         return FormulaRole::kNegatedConjecture;
-    if (role_str == "plain")
+}
+    if (role_str == "plain") {
         return FormulaRole::kPlain;
+}
     return FormulaRole::kPlain;
 }
 
-enum class TokenType { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown };
+enum class TokenType : std::uint8_t { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown };
 
 struct Token {
-    TokenType type;
-    std::string_view value;
-    size_t line;
-    size_t column;
+    TokenType type_{};
+    std::string_view value_;
+    size_t line_{};
+    size_t column_{};
 };
 
 class TptpLexer {
   public:
     explicit TptpLexer(std::string_view input) : source_(input) {}
 
-    Token next_token() {
-        skip_whitespace_and_comments();
+    Token nextToken() {
+        skipWhitespaceAndComments();
 
         if (pos_ >= source_.length()) {
-            return {.type = TokenType::kEOF, .value = "", .line = line_, .column = column_};
+            return {.type_ = TokenType::kEOF, .value_ = "", .line_ = line_, .column_ = column_};
         }
 
-        size_t start_pos = pos_;
-        [[maybe_unused]] size_t start_col = column_;
-        char c = source_[pos_];
+        size_t const start_pos = pos_;
+        [[maybe_unused]] size_t const start_col = column_;
+        char const c = source_[pos_];
 
-        if (std::isalpha(static_cast<unsigned char>(c)) || c == '_') {
+        if ((std::isalpha(static_cast<unsigned char>(c)) != 0) || c == '_') {
             while (
                 pos_ < source_.size() &&
-                (std::isalnum(static_cast<unsigned char>(source_[pos_])) || source_[pos_] == '_')) {
-                advance_char();
+                ((std::isalnum(static_cast<unsigned char>(source_[pos_])) != 0) || source_[pos_] == '_')) {
+                advanceChar();
             }
-            return {.type = TokenType::kWord,
-                    .value = source_.substr(start_pos, pos_ - start_pos),
-                    .line = line_,
-                    .column = column_};
+            return {.type_ = TokenType::kWord,
+                    .value_ = source_.substr(start_pos, pos_ - start_pos),
+                    .line_ = line_,
+                    .column_ = column_};
         }
 
-        advance_char();
+        advanceChar();
         switch (c) {
             case '(':
-                return {.type = TokenType::kLParen, .value = "(", .line = line_, .column = column_};
+                return {.type_ = TokenType::kLParen, .value_ = "(", .line_ = line_, .column_ = column_};
             case ')':
-                return {.type = TokenType::kRParen, .value = ")", .line = line_, .column = column_};
+                return {.type_ = TokenType::kRParen, .value_ = ")", .line_ = line_, .column_ = column_};
             case ',':
-                return {.type = TokenType::kComma, .value = ",", .line = line_, .column = column_};
+                return {.type_ = TokenType::kComma, .value_ = ",", .line_ = line_, .column_ = column_};
             case '.':
-                return {.type = TokenType::kDot, .value = ".", .line = line_, .column = column_};
+                return {.type_ = TokenType::kDot, .value_ = ".", .line_ = line_, .column_ = column_};
             case '~':
-                return {.type = TokenType::kNot, .value = "~", .line = line_, .column = column_};
+                return {.type_ = TokenType::kNot, .value_ = "~", .line_ = line_, .column_ = column_};
             case '|':
-                return {.type = TokenType::kOr, .value = "|", .line = line_, .column = column_};
+                return {.type_ = TokenType::kOr, .value_ = "|", .line_ = line_, .column_ = column_};
             default:
-                return {.type = TokenType::kUnkown,
-                        .value = source_.substr(start_pos, 1),
-                        .line = line_,
-                        .column = column_};
+                return {.type_ = TokenType::kUnkown,
+                        .value_ = source_.substr(start_pos, 1),
+                        .line_ = line_,
+                        .column_ = column_};
         }
     }
 
@@ -119,7 +134,7 @@ class TptpLexer {
     size_t line_ = 1;
     size_t column_ = 1;
 
-    void advance_char() {
+    void advanceChar() {
         if (pos_ < source_.size()) {
             if (source_[pos_] == '\n') {
                 line_++;
@@ -131,14 +146,14 @@ class TptpLexer {
         }
     }
 
-    void skip_whitespace_and_comments() {
+    void skipWhitespaceAndComments() {
         while (pos_ < source_.size()) {
-            char c = source_[pos_];
-            if (std::isspace(static_cast<unsigned char>(c))) {
-                advance_char();
+            char const c = source_[pos_];
+            if (std::isspace(static_cast<unsigned char>(c)) != 0) {
+                advanceChar();
             } else if (c == '%') {
                 while (pos_ < source_.size() && source_[pos_] != '\n') {
-                    advance_char();
+                    advanceChar();
                 }
             } else {
                 break;
@@ -155,41 +170,41 @@ class TptpParser {
     }
 
     void parseProblem(ParsedProblem& problem) {
-        while (current_token_.type != TokenType::kEOF) {
-            if (current_token_.type == TokenType::kWord && current_token_.value == "cnf") {
+        while (current_token_.type_ != TokenType::kEOF) {
+            if (current_token_.type_ == TokenType::kWord && current_token_.value_ == "cnf") {
                 advance();
                 expect(TokenType::kLParen);
 
                 AnnotatedFormula af;
-                af.is_cnf = true;
+                af.is_cnf_ = true;
 
-                af.name = std::string(current_token_.value);
+                af.name_ = std::string(current_token_.value_);
                 expect(TokenType::kWord);
                 expect(TokenType::kComma);
 
-                af.role = parseRole(current_token_.value);
+                af.role_ = parseRole(current_token_.value_);
                 expect(TokenType::kWord);
                 expect(TokenType::kComma);
 
                 Clause clause;
-                clause.literals.push_back(parseLiteral());
-                while (current_token_.type == TokenType::kOr) {
+                clause.literals_.push_back(parseLiteral());
+                while (current_token_.type_ == TokenType::kOr) {
                     advance();
-                    clause.literals.push_back(parseLiteral());
+                    clause.literals_.push_back(parseLiteral());
                 }
-                af.clauses.push_back(std::move(clause));
+                af.clauses_.push_back(std::move(clause));
 
                 expect(TokenType::kRParen);
                 expect(TokenType::kDot);
-                problem.formulas.push_back(std::move(af));
+                problem.formulas_.push_back(std::move(af));
 
                 variable_cache_.clear();
-            } else if (current_token_.value == "fof") {
+            } else if (current_token_.value_ == "fof") {
                 throw std::runtime_error("FOF parsing not implemented. Line " +
-                                         std::to_string(current_token_.line));
+                                         std::to_string(current_token_.line_));
             } else {
                 throw std::runtime_error("Unknown declaration: '" +
-                                         std::string(current_token_.value) + "'");
+                                         std::string(current_token_.value_) + "'");
             }
         }
     }
@@ -198,33 +213,33 @@ class TptpParser {
     TptpLexer lexer_;
     TermBank& bank_;
     SymbolTable& symbols_;
-    Token current_token_;
+    Token current_token_{};
+    std::vector<Token> tokens_;
+    std::unordered_map<std::string_view, SymbolId> variable_cache_{};
 
-    std::unordered_map<std::string_view, TermId> variable_cache_;
-
-    void advance() { current_token_ = lexer_.next_token(); }
+    void advance() { current_token_ = lexer_.nextToken(); }
 
     void expect(TokenType type) {
-        if (current_token_.type != type) {
-            throw std::runtime_error("Parse error at line " + std::to_string(current_token_.line) +
-                                     ", col " + std::to_string(current_token_.column) +
-                                     ": unexpected token '" + std::string(current_token_.value) +
+        if (current_token_.type_ != type) {
+            throw std::runtime_error("Parse error at line " + std::to_string(current_token_.line_) +
+                                     ", col " + std::to_string(current_token_.column_) +
+                                     ": unexpected token '" + std::string(current_token_.value_) +
                                      "'");
         }
         advance();
     }
 
     TermId parseTerm() {
-        if (current_token_.type != TokenType::kWord) {
+        if (current_token_.type_ != TokenType::kWord) {
             throw std::runtime_error("Expected variable or function name at line " +
-                                     std::to_string(current_token_.line) + ", col " +
-                                     std::to_string(current_token_.column) +
-                                     ": unexpected token '" + std::string(current_token_.value) +
+                                     std::to_string(current_token_.line_) + ", col " +
+                                     std::to_string(current_token_.column_) +
+                                     ": unexpected token '" + std::string(current_token_.value_) +
                                      "'");
         }
 
-        std::string_view name = current_token_.value;
-        bool is_variable = std::isupper(static_cast<unsigned char>(name[0]));
+        std::string_view const name = current_token_.value_;
+        bool const is_variable = std::isupper(static_cast<unsigned char>(name[0])) != 0;
         advance();
 
         if (is_variable) {
@@ -233,18 +248,17 @@ class TptpParser {
             if (it != variable_cache_.end()) {
                 return it->second;
             }
-            SymbolId sym = symbols_.intern(name, SymbolKind::kVariable);
-            TermId var_id = bank_.makeVar(sym);
+            SymbolId const sym = symbols_.intern(name, SymbolKind::kVariable);
+            TermId const var_id = bank_.makeVar(sym);
             variable_cache_[name] = var_id;
             return var_id;
-        } else {
-            // Check if this is a function/predicate (has args) or a constant (no parens)
-            if (current_token_.type == TokenType::kLParen) {
+        }             // Check if this is a function/predicate (has args) or a constant (no parens)
+            if (current_token_.type_ == TokenType::kLParen) {
                 advance();  // consume '('
                 std::vector<TermId> args;
-                if (current_token_.type != TokenType::kRParen) {
+                if (current_token_.type_ != TokenType::kRParen) {
                     args.push_back(parseTerm());
-                    while (current_token_.type == TokenType::kComma) {
+                    while (current_token_.type_ == TokenType::kComma) {
                         advance();
                         args.push_back(parseTerm());
                     }
@@ -258,17 +272,17 @@ class TptpParser {
                 SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0);
                 return bank_.makeTerm(sym, {});
             }
-        }
+       
     }
 
     Literal parseLiteral() {
         bool is_positive = true;
-        if (current_token_.type == TokenType::kNot) {
+        if (current_token_.type_ == TokenType::kNot) {
             is_positive = false;
             advance();
         }
-        TermId term = parseTerm();
-        return Literal{.atom = term, .is_positive = is_positive};
+        TermId const term = parseTerm();
+        return Literal{.atom_ = term, .is_positive_ = is_positive};
     }
 };
 
@@ -284,22 +298,22 @@ ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolT
     if (!file.is_open()) {
         throw std::runtime_error("Failed to open file: " + filename);
     }
-    std::string content((std::istreambuf_iterator<char>(file)), std::istreambuf_iterator<char>());
+    std::string const content((std::istreambuf_iterator<char>(file)), std::istreambuf_iterator<char>());
     ParsedProblem problem = parseTptpString(content, bank, symbols);
-    problem.source_file = filename;
+    problem.source_file_ = filename;
     return problem;
 }
 
-std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank& bank,
-                                      SymbolTable& symbols) {
+std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank&  /*bank*/,
+                                      SymbolTable&  /*symbols*/) {
     std::vector<Clause> final_clauses;
 
-    for (auto& af : problem.formulas) {
-        if (af.is_cnf) {
-            for (auto& clause : af.clauses) {
-                clause.rule = InferenceRule::kInput;
-                clause.parent1 = kInvalidId;
-                clause.parent2 = kInvalidId;
+    for (auto& af : problem.formulas_) {
+        if (af.is_cnf_) {
+            for (auto& clause : af.clauses_) {
+                clause.rule_ = InferenceRule::kInput;
+                clause.parent1_ = kInvalidId;
+                clause.parent2_ = kInvalidId;
                 final_clauses.push_back(std::move(clause));
             }
         }
diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc
index f072b8e..82e59b7 100644
--- a/src/infer/resolution.cc
+++ b/src/infer/resolution.cc
@@ -26,8 +26,12 @@
 #include "atp/infer/substitution.h"
 #include "atp/infer/unification.h"
 
+#include <cstddef>
+#include <cstdint>
+#include <optional>
 #include <string>
 #include <unordered_map>
+#include <utility>
 #include <vector>
 
 namespace atp {
@@ -42,7 +46,7 @@ void collectVariables(TermId term, const TermBank& bank, std::unordered_map<Term
     }
     // Copy args to avoid dangling ref (bank is const here, but be safe)
     const Term& t = bank.getTerm(term);
-    for (TermId arg : t.args) {
+    for (TermId const arg : t.args_) {
         collectVariables(arg, bank, seen);
     }
 }
@@ -53,8 +57,8 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
                        uint32_t& next_var_id) {
     // 1. Collect all variables in the clause
     std::unordered_map<TermId, bool> var_set;
-    for (const auto& lit : c.literals) {
-        collectVariables(lit.atom, bank, var_set);
+    for (const auto& lit : c.literals_) {
+        collectVariables(lit.atom_, bank, var_set);
     }
 
     if (var_set.empty()) {
@@ -64,22 +68,22 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
     // 2. Create fresh variables and build a substitution
     Substitution rename_subst;
     for (auto& [old_var_id, _] : var_set) {
-        std::string fresh_name = "_R" + std::to_string(next_var_id++);
-        SymbolId fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable);
-        TermId fresh_var = bank.makeVar(fresh_sym);
+        std::string const fresh_name = "_R" + std::to_string(next_var_id++);
+        SymbolId const fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable);
+        TermId const fresh_var = bank.makeVar(fresh_sym);
         rename_subst.bind(old_var_id, fresh_var);
     }
 
     // 3. Apply the renaming substitution to all literals
     Clause renamed;
-    renamed.id = c.id;
-    renamed.rule = c.rule;
-    renamed.parent1 = c.parent1;
-    renamed.parent2 = c.parent2;
-    renamed.depth = c.depth;
-    for (const auto& lit : c.literals) {
-        TermId new_atom = applySubstitution(rename_subst, lit.atom, bank);
-        renamed.literals.push_back({.atom = new_atom, .is_positive = lit.is_positive});
+    renamed.id_ = c.id_;
+    renamed.rule_ = c.rule_;
+    renamed.parent1_ = c.parent1_;
+    renamed.parent2_ = c.parent2_;
+    renamed.depth_ = c.depth_;
+    for (const auto& lit : c.literals_) {
+        TermId const new_atom = applySubstitution(rename_subst, lit.atom_, bank);
+        renamed.literals_.push_back({.atom_ = new_atom, .is_positive_ = lit.is_positive_});
     }
     return renamed;
 }
@@ -87,7 +91,7 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
 std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2,
                               size_t lit_idx2, const UnificationConfig& uconfig) {
     // Must have opposite polarity
-    if (c1.literals[lit_idx1].is_positive == c2.literals[lit_idx2].is_positive) {
+    if (c1.literals_[lit_idx1].is_positive_ == c2.literals_[lit_idx2].is_positive_) {
         return std::nullopt;
     }
 
@@ -99,28 +103,28 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
 
     // Unify the complementary atoms
     Substitution subst;
-    if (!unify(bank, c1.literals[lit_idx1].atom, c2r.literals[lit_idx2].atom, subst, uconfig)) {
+    if (!unify(bank, c1.literals_[lit_idx1].atom_, c2r.literals_[lit_idx2].atom_, subst, uconfig)) {
         return std::nullopt;
     }
 
     // Build the resolvent: all literals except the resolved pair, with subst applied
     Clause resolvent;
-    resolvent.rule = InferenceRule::kResolution;
-    resolvent.parent1 = c1.id;
-    resolvent.parent2 = c2.id;
+    resolvent.rule_ = InferenceRule::kResolution;
+    resolvent.parent1_ = c1.id_;
+    resolvent.parent2_ = c2.id_;
 
-    for (size_t i = 0; i < c1.literals.size(); ++i) {
+    for (size_t i = 0; i < c1.literals_.size(); ++i) {
         if (i != lit_idx1) {
-            TermId new_atom = applySubstitution(subst, c1.literals[i].atom, bank);
-            resolvent.literals.push_back(
-                {.atom = new_atom, .is_positive = c1.literals[i].is_positive});
+            TermId const new_atom = applySubstitution(subst, c1.literals_[i].atom_, bank);
+            resolvent.literals_.push_back(
+                {.atom_ = new_atom, .is_positive_ = c1.literals_[i].is_positive_});
         }
     }
-    for (size_t i = 0; i < c2r.literals.size(); ++i) {
+    for (size_t i = 0; i < c2r.literals_.size(); ++i) {
         if (i != lit_idx2) {
-            TermId new_atom = applySubstitution(subst, c2r.literals[i].atom, bank);
-            resolvent.literals.push_back(
-                {.atom = new_atom, .is_positive = c2r.literals[i].is_positive});
+            TermId const new_atom = applySubstitution(subst, c2r.literals_[i].atom_, bank);
+            resolvent.literals_.push_back(
+                {.atom_ = new_atom, .is_positive_ = c2r.literals_[i].is_positive_});
         }
     }
     return resolvent;
@@ -129,9 +133,9 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
 std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
                                   const UnificationConfig& uconfig) {
     std::vector<Clause> results;
-    for (size_t i = 0; i < c1.literals.size(); ++i) {
-        for (size_t j = 0; j < c2.literals.size(); ++j) {
-            if (c1.literals[i].is_positive != c2.literals[j].is_positive) {
+    for (size_t i = 0; i < c1.literals_.size(); ++i) {
+        for (size_t j = 0; j < c2.literals_.size(); ++j) {
+            if (c1.literals_[i].is_positive_ != c2.literals_[j].is_positive_) {
                 if (auto r = resolve(bank, c1, i, c2, j, uconfig)) {
                     results.push_back(std::move(*r));
                 }
@@ -143,24 +147,24 @@ std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause
 
 std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig) {
     std::vector<Clause> results;
-    for (size_t i = 0; i < c.literals.size(); ++i) {
-        for (size_t j = i + 1; j < c.literals.size(); ++j) {
-            if (c.literals[i].is_positive != c.literals[j].is_positive) {
+    for (size_t i = 0; i < c.literals_.size(); ++i) {
+        for (size_t j = i + 1; j < c.literals_.size(); ++j) {
+            if (c.literals_[i].is_positive_ != c.literals_[j].is_positive_) {
                 continue;  // Must have same polarity
             }
             Substitution subst;
-            if (!unify(bank, c.literals[i].atom, c.literals[j].atom, subst, uconfig)) {
+            if (!unify(bank, c.literals_[i].atom_, c.literals_[j].atom_, subst, uconfig)) {
                 continue;
             }
             // Build factored clause: drop literal j, apply subst to all
             Clause factored;
-            factored.rule = InferenceRule::kFactoring;
-            factored.parent1 = c.id;
-            for (size_t k = 0; k < c.literals.size(); ++k) {
+            factored.rule_ = InferenceRule::kFactoring;
+            factored.parent1_ = c.id_;
+            for (size_t k = 0; k < c.literals_.size(); ++k) {
                 if (k != j) {
-                    TermId new_atom = applySubstitution(subst, c.literals[k].atom, bank);
-                    factored.literals.push_back(
-                        {.atom = new_atom, .is_positive = c.literals[k].is_positive});
+                    TermId const new_atom = applySubstitution(subst, c.literals_[k].atom_, bank);
+                    factored.literals_.push_back(
+                        {.atom_ = new_atom, .is_positive_ = c.literals_[k].is_positive_});
                 }
             }
             results.push_back(std::move(factored));
diff --git a/src/infer/substitution.cc b/src/infer/substitution.cc
index a7ce617..8710fb0 100644
--- a/src/infer/substitution.cc
+++ b/src/infer/substitution.cc
@@ -22,6 +22,8 @@
 #include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 
+#include <vector>
+
 namespace atp {
 
 bool Substitution::bind(TermId var, TermId term) {
@@ -66,8 +68,8 @@ TermId Substitution::apply(TermId term, TermBank& bank) const {
     // IMPORTANT: Copy symbol_id and args BEFORE recursing.
     // Recursive apply() calls may trigger bank.makeTerm() → realloc → dangling ref.
     const Term& t = bank.getTerm(term);
-    SymbolId sym = t.symbol_id;
-    std::vector<TermId> old_args(t.args);  // copy!
+    SymbolId const sym = t.symbol_id_;
+    std::vector<TermId> const old_args(t.args_);  // copy!
 
     if (old_args.empty()) {
         // Constant or 0-arity — no substitution needed
@@ -78,8 +80,8 @@ TermId Substitution::apply(TermId term, TermBank& bank) const {
     std::vector<TermId> new_args;
     new_args.reserve(old_args.size());
     bool changed = false;
-    for (TermId arg : old_args) {
-        TermId new_arg = apply(arg, bank);
+    for (TermId const arg : old_args) {
+        TermId const new_arg = apply(arg, bank);
         new_args.push_back(new_arg);
         if (new_arg != arg) {
             changed = true;
@@ -105,7 +107,7 @@ bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const
     }
 
     const Term& t = bank.getTerm(term);
-    for (TermId arg : t.args) {
+    for (TermId const arg : t.args_) {
         if (occursIn(var, arg, bank)) {
             return true;
         }
diff --git a/src/infer/unification.cc b/src/infer/unification.cc
index 66e1af6..c42bf67 100644
--- a/src/infer/unification.cc
+++ b/src/infer/unification.cc
@@ -18,9 +18,14 @@
 
 #include "atp/infer/unification.h"
 
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 #include "atp/infer/substitution.h"
 
+#include <cstddef>
+#include <vector>
+
 namespace atp {
 
 bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
@@ -33,7 +38,7 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
     }
 
     if (bank.isVariable(t1)) {
-        if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) {
+        if (config.enable_occurs_check_ && subst.occursIn(t1, t2, bank)) {
             return false;
         }
         subst.bind(t1, t2);
@@ -41,7 +46,7 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
     }
 
     if (bank.isVariable(t2)) {
-        if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) {
+        if (config.enable_occurs_check_ && subst.occursIn(t2, t1, bank)) {
             return false;
         }
         subst.bind(t2, t1);
@@ -51,12 +56,12 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
     const Term& term1 = bank.getTerm(t1);
     const Term& term2 = bank.getTerm(t2);
 
-    if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) {
+    if (term1.symbol_id_ != term2.symbol_id_ || term1.arity() != term2.arity()) {
         return false;
     }
 
     for (size_t i = 0; i < term1.arity(); ++i) {
-        if (!unify(bank, term1.args[i], term2.args[i], subst, config)) {
+        if (!unify(bank, term1.args_[i], term2.args_[i], subst, config)) {
             return false;
         }
     }
@@ -73,12 +78,12 @@ TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank)
     // IMPORTANT: Copy args and symbol_id BEFORE recursing.
     // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs.
     const Term& t = bank.getTerm(term);
-    SymbolId sym = t.symbol_id;
-    std::vector<TermId> old_args(t.args);  // copy!
+    SymbolId const sym = t.symbol_id_;
+    std::vector<TermId> const old_args(t.args_);  // copy!
 
     std::vector<TermId> new_args;
     new_args.reserve(old_args.size());
-    for (TermId arg : old_args) {
+    for (TermId const arg : old_args) {
         new_args.push_back(applySubstitution(subst, arg, bank));
     }
     return bank.makeTerm(sym, new_args);
diff --git a/src/main.cc b/src/main.cc
index bd385d8..81dbc91 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -27,8 +27,10 @@
 #include "atp/search/prover.h"
 
 #include <cstdlib>
+#include <exception>
 #include <iostream>
 #include <string>
+#include <utility>
 
 int main(int argc, char* argv[]) {
     std::cerr << "richard-atp-engine  Copyright (C) 2026  Richard Qin\n"
@@ -41,7 +43,7 @@ int main(int argc, char* argv[]) {
         return EXIT_FAILURE;
     }
 
-    const std::string filepath = argv[1];
+    const std::string kFilepath = argv[1];
 
     try {
         // 1. Initialize core modules
@@ -50,9 +52,9 @@ int main(int argc, char* argv[]) {
         atp::ClauseStore store;
 
         // 2. Parse TPTP input
-        auto problem = atp::parseTptpFile(filepath, bank, symbols);
+        auto problem = atp::parseTptpFile(kFilepath, bank, symbols);
 
-        std::cerr << "% Parsed " << problem.formulas.size() << " formulas from " << filepath
+        std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << kFilepath
                   << "\n";
 
         // 3. Prepare clauses for proving
@@ -63,28 +65,28 @@ int main(int argc, char* argv[]) {
         // 4. Run the prover
         atp::Prover prover(bank, store);
         prover.addClauses(std::move(clauses));
-        atp::ProverResult result = prover.prove();
+        atp::ProverResult const result = prover.prove();
 
         // 5. Output result (SZS format)
         switch (result) {
             case atp::ProverResult::kTheorem: {
-                std::cout << "% SZS status Theorem for " << filepath << "\n\n";
+                std::cout << "% SZS status Theorem for " << kFilepath << "\n\n";
 
                 // Extract and print proof
                 auto eid = prover.getEmptyClauseId();
                 if (eid.has_value()) {
                     auto proof = atp::extractProof(store, *eid);
-                    std::cout << "% SZS output start Proof for " << filepath << "\n";
+                    std::cout << "% SZS output start Proof for " << kFilepath << "\n";
                     std::cout << atp::formatProof(proof, store, bank);
-                    std::cout << "% SZS output end Proof for " << filepath << "\n";
+                    std::cout << "% SZS output end Proof for " << kFilepath << "\n";
                 }
                 break;
             }
             case atp::ProverResult::kSaturation:
-                std::cout << "% SZS status Satisfiable for " << filepath << "\n";
+                std::cout << "% SZS status Satisfiable for " << kFilepath << "\n";
                 break;
             case atp::ProverResult::kTimeout:
-                std::cout << "% SZS status Timeout for " << filepath << "\n";
+                std::cout << "% SZS status Timeout for " << kFilepath << "\n";
                 break;
         }
 
diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc
index 183ab2e..a0d5a11 100644
--- a/src/proof/proof_trace.cc
+++ b/src/proof/proof_trace.cc
@@ -19,11 +19,15 @@
 #include "atp/proof/proof_trace.h"
 
 #include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
 #include "atp/core/symbol_table.h"
 #include "atp/core/term.h"
+#include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 
 #include <algorithm>
+#include <array>
+#include <cstddef>
 #include <stack>
 #include <string>
 #include <unordered_map>
@@ -43,29 +47,29 @@ std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_cla
     worklist.push(empty_clause_id);
 
     while (!worklist.empty()) {
-        ClauseId cid = worklist.top();
+        const ClauseId kCid = worklist.top();
         worklist.pop();
 
-        if (cid == kInvalidId) {
+        if (kCid == kInvalidId) {
             continue;
         }
-        if (visited.count(cid) > 0) {
+        if (visited.contains(kCid)) {
             continue;
         }
-        visited.insert(cid);
+        visited.insert(kCid);
 
-        const Clause& c = store.getClause(cid);
+        const Clause& c = store.getClause(kCid);
         steps.push_back({
-            .clause_id = cid,
-            .rule = c.rule,
-            .parent1 = c.parent1,
-            .parent2 = c.parent2,
+            .clause_id_ = kCid,
+            .rule_ = c.rule_,
+            .parent1_ = c.parent1_,
+            .parent2_ = c.parent2_,
         });
 
         // Recurse into parents (axioms have kInvalidId parents, which are
         // filtered by the check at the top of the loop)
-        worklist.push(c.parent1);
-        worklist.push(c.parent2);
+        worklist.push(c.parent1_);
+        worklist.push(c.parent2_);
     }
 
     // Reverse: axioms (leaves) first → empty clause (root) last
@@ -77,18 +81,18 @@ std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_cla
 
 std::string termToString(TermId id, const TermBank& bank) {
     const Term& t = bank.getTerm(id);
-    std::string name(bank.symbols().getName(t.symbol_id));
+    std::string name(bank.symbols().getName(t.symbol_id_));
 
-    if (t.args.empty()) {
+    if (t.args_.empty()) {
         return name;
     }
 
     std::string result = name + "(";
-    for (size_t i = 0; i < t.args.size(); ++i) {
+    for (size_t i = 0; i < t.args_.size(); ++i) {
         if (i > 0) {
             result += ",";
         }
-        result += termToString(t.args[i], bank);
+        result += termToString(t.args_[i], bank);
     }
     result += ")";
     return result;
@@ -101,15 +105,15 @@ namespace {
 /// Generate a human-readable variable name from an index.
 /// 0→X, 1→Y, 2→Z, 3→W, 4→V, 5→U, 6→X1, 7→Y1, ...
 std::string prettyVarName(size_t index) {
-    static const char kBaseNames[] = {'X', 'Y', 'Z', 'W', 'V', 'U'};
-    static constexpr size_t kBaseCount = sizeof(kBaseNames);
+    static constexpr std::array<char, 6> kBaseNames = {'X', 'Y', 'Z', 'W', 'V', 'U'};
+    static constexpr size_t kBaseCount = kBaseNames.size();
 
-    char base = kBaseNames[index % kBaseCount];
-    size_t suffix = index / kBaseCount;
-    if (suffix == 0) {
-        return std::string(1, base);
+    const char kBase = kBaseNames[index % kBaseCount];
+    const size_t kSuffix = index / kBaseCount;
+    if (kSuffix == 0) {
+        return std::string{kBase};
     }
-    return std::string(1, base) + std::to_string(suffix);
+    return std::string{kBase} + std::to_string(kSuffix);
 }
 
 /// Pretty-print a term, renaming variables to readable names.
@@ -121,29 +125,44 @@ std::string termToPretty(TermId id, const TermBank& bank,
         if (it != var_map.end()) {
             return it->second;
         }
-        std::string name = prettyVarName(var_map.size());
-        var_map[id] = name;
-        return name;
+        const std::string kName = prettyVarName(var_map.size());
+        var_map[id] = kName;
+        return kName;
     }
 
     const Term& t = bank.getTerm(id);
-    std::string name(bank.symbols().getName(t.symbol_id));
+    std::string name(bank.symbols().getName(t.symbol_id_));
 
-    if (t.args.empty()) {
+    if (t.args_.empty()) {
         return name;
     }
 
     std::string result = name + "(";
-    for (size_t i = 0; i < t.args.size(); ++i) {
+    for (size_t i = 0; i < t.args_.size(); ++i) {
         if (i > 0) {
             result += ",";
         }
-        result += termToPretty(t.args[i], bank, var_map);
+        result += termToPretty(t.args_[i], bank, var_map);
     }
     result += ")";
     return result;
 }
 
+// ruleToString
+
+std::string ruleToString(InferenceRule rule) {
+    switch (rule) {
+        case InferenceRule::kInput:
+            return "input";
+        case InferenceRule::kResolution:
+            return "resolution";
+        case InferenceRule::kFactoring:
+            return "factoring";
+        default:
+            return "unknown";
+    }
+}
+
 }  // namespace
 
 // clauseToString
@@ -157,33 +176,18 @@ std::string clauseToString(const Clause& clause, const TermBank& bank) {
     std::unordered_map<TermId, std::string> var_map;
 
     std::string result;
-    for (size_t i = 0; i < clause.literals.size(); ++i) {
+    for (size_t i = 0; i < clause.literals_.size(); ++i) {
         if (i > 0) {
             result += " ∨ ";
         }
-        if (!clause.literals[i].is_positive) {
+        if (!clause.literals_[i].is_positive_) {
             result += "¬";
         }
-        result += termToPretty(clause.literals[i].atom, bank, var_map);
+        result += termToPretty(clause.literals_[i].atom_, bank, var_map);
     }
     return result;
 }
 
-// ruleToString
-
-static std::string ruleToString(InferenceRule rule) {
-    switch (rule) {
-        case InferenceRule::kInput:
-            return "input";
-        case InferenceRule::kResolution:
-            return "resolution";
-        case InferenceRule::kFactoring:
-            return "factoring";
-        default:
-            return "unknown";
-    }
-}
-
 // formatProof
 
 std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore& store,
@@ -191,10 +195,10 @@ std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore&
     // Build a local renumbering: internal ClauseId → sequential proof step number
     std::unordered_map<ClauseId, size_t> id_to_step;
     for (size_t i = 0; i < proof.size(); ++i) {
-        id_to_step[proof[i].clause_id] = i + 1;  // 1-based
+        id_to_step[proof[i].clause_id_] = i + 1;  // 1-based
     }
 
-    auto localName = [&](ClauseId cid) -> std::string {
+    auto local_name = [&](ClauseId cid) -> std::string {
         auto it = id_to_step.find(cid);
         if (it != id_to_step.end()) {
             return std::to_string(it->second);
@@ -206,17 +210,17 @@ std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore&
     std::string result;
     for (size_t i = 0; i < proof.size(); ++i) {
         const auto& step = proof[i];
-        const Clause& c = store.getClause(step.clause_id);
+        const Clause& c = store.getClause(step.clause_id_);
 
         result += std::to_string(i + 1) + ". ";
-        result += "[" + ruleToString(step.rule) + "] ";
+        result += "[" + ruleToString(step.rule_) + "] ";
         result += clauseToString(c, bank);
 
         // Show parents for derived clauses
-        if (step.parent1 != kInvalidId) {
-            result += "  [" + localName(step.parent1);
-            if (step.parent2 != kInvalidId) {
-                result += ", " + localName(step.parent2);
+        if (step.parent1_ != kInvalidId) {
+            result += "  [" + local_name(step.parent1_);
+            if (step.parent2_ != kInvalidId) {
+                result += ", " + local_name(step.parent2_);
             }
             result += "]";
         }
diff --git a/src/search/prover.cc b/src/search/prover.cc
index 5b68e9d..2c2de40 100644
--- a/src/search/prover.cc
+++ b/src/search/prover.cc
@@ -18,6 +18,9 @@
 
 #include "atp/search/prover.h"
 
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 #include "atp/infer/resolution.h"
 #include "atp/infer/unification.h"
@@ -25,16 +28,21 @@
 #include "atp/simplify/tautology.h"
 
 #include <algorithm>
+#include <cstddef>
+#include <cstdint>
+#include <optional>
+#include <utility>
+#include <vector>
 
 namespace atp {
 
 Prover::Prover(TermBank& bank, ClauseStore& store, ProverConfig config)
-    : bank_(bank), store_(store), config_(std::move(config)), unprocessed_(config_.comparator) {}
+    : bank_(bank), store_(store), config_(std::move(config)), unprocessed_(config_.comparator_) {}
 
 void Prover::addClauses(std::vector<Clause> clauses) {
     for (auto& clause : clauses) {
-        clause.depth = 0;
-        ClauseId id = store_.addClause(clause);
+        clause.depth_ = 0;
+        ClauseId const id = store_.addClause(clause);
         unprocessed_.push(store_.getClause(id));
     }
 }
@@ -44,7 +52,7 @@ ProverResult Prover::prove() {
 
     while (!unprocessed_.empty()) {
         // Resource limits
-        if (iterations >= config_.max_iterations || store_.size() >= config_.max_clauses) {
+        if (iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_) {
             return ProverResult::kTimeout;
         }
         ++iterations;
@@ -55,7 +63,7 @@ ProverResult Prover::prove() {
 
         // 2. Check if given is itself the empty clause
         if (given.isEmpty()) {
-            empty_clause_id_ = given.id;
+            empty_clause_id_ = given.id_;
             return ProverResult::kTheorem;
         }
 
@@ -65,7 +73,7 @@ ProverResult Prover::prove() {
         }
 
         bool forward_subsumed = false;
-        for (ClauseId pid : processed_) {
+        for (ClauseId const pid : processed_) {
             if (subsumes(store_.getClause(pid), given)) {
                 forward_subsumed = true;
                 break;
@@ -84,14 +92,14 @@ ProverResult Prover::prove() {
         // 5. Generate new clauses
         // Inference BEFORE adding given to processed — matches doc §4.6.
         std::vector<Clause> new_clauses;
-        const UnificationConfig uconfig{.enable_occurs_check = config_.enable_occurs_check};
+        const UnificationConfig kUconfig{.enable_occurs_check_ = config_.enable_occurs_check_};
 
         // 5a. Resolve given with every processed clause (both directions)
-        for (ClauseId pid : processed_) {
+        for (ClauseId const pid : processed_) {
             const Clause& pc = store_.getClause(pid);
 
-            auto resolvents1 = allResolvents(bank_, given, pc, uconfig);
-            auto resolvents2 = allResolvents(bank_, pc, given, uconfig);
+            auto resolvents1 = allResolvents(bank_, given, pc, kUconfig);
+            auto resolvents2 = allResolvents(bank_, pc, given, kUconfig);
 
             for (auto& r : resolvents1) {
                 new_clauses.push_back(std::move(r));
@@ -102,13 +110,13 @@ ProverResult Prover::prove() {
         }
 
         // 5b. Factor given (only once)
-        auto factors = factor(bank_, given, uconfig);
+        auto factors = factor(bank_, given, kUconfig);
         for (auto& f : factors) {
             new_clauses.push_back(std::move(f));
         }
 
         // 6. Add given to processed AFTER inference
-        processed_.push_back(given.id);
+        processed_.push_back(given.id_);
 
         // 7. Process new clauses
         for (auto& nc : new_clauses) {
@@ -125,17 +133,17 @@ ProverResult Prover::prove() {
             }
 
             // 7c. Set depth
-            uint32_t d1 = (nc.parent1 != kInvalidId) ? store_.getClause(nc.parent1).depth : 0;
-            uint32_t d2 = (nc.parent2 != kInvalidId) ? store_.getClause(nc.parent2).depth : 0;
-            nc.depth = static_cast<uint16_t>(std::max(d1, d2) + 1);
+            uint32_t const d1 = (nc.parent1_ != kInvalidId) ? store_.getClause(nc.parent1_).depth_ : 0;
+            uint32_t const d2 = (nc.parent2_ != kInvalidId) ? store_.getClause(nc.parent2_).depth_ : 0;
+            nc.depth_ = static_cast<uint16_t>(std::max(d1, d2) + 1);
 
             // 7d. Store the clause (needed for forward subsumption check)
-            ClauseId nid = store_.addClause(nc);
+            ClauseId const nid = store_.addClause(nc);
             const Clause& stored_nc = store_.getClause(nid);
 
             // 7e. Forward subsumption on new clause
             bool new_subsumed = false;
-            for (ClauseId pid : processed_) {
+            for (ClauseId const pid : processed_) {
                 if (subsumes(store_.getClause(pid), stored_nc)) {
                     new_subsumed = true;
                     break;
diff --git a/src/simplify/subsumption.cc b/src/simplify/subsumption.cc
index 3756d82..0038ad1 100644
--- a/src/simplify/subsumption.cc
+++ b/src/simplify/subsumption.cc
@@ -18,16 +18,18 @@
 
 #include "atp/simplify/subsumption.h"
 
+#include "atp/core/clause.h"
+
 namespace atp {
 
 bool subsumes(const Clause& general, const Clause& specific) {
     if (general.size() > specific.size()) {
         return false;
     }
-    for (const auto& lit_g : general.literals) {
+    for (const auto& lit_g : general.literals_) {
         bool found = false;
-        for (const auto& lit_s : specific.literals) {
-            if (lit_g.atom == lit_s.atom && lit_g.is_positive == lit_s.is_positive) {
+        for (const auto& lit_s : specific.literals_) {
+            if (lit_g.atom_ == lit_s.atom_ && lit_g.is_positive_ == lit_s.is_positive_) {
                 found = true;
                 break;
             }
diff --git a/src/simplify/tautology.cc b/src/simplify/tautology.cc
index 70bdced..e35d874 100644
--- a/src/simplify/tautology.cc
+++ b/src/simplify/tautology.cc
@@ -18,14 +18,16 @@
 
 #include "atp/simplify/tautology.h"
 
+#include "atp/core/clause.h"
+
 #include <cstddef>
 
 namespace atp {
 bool isTautology(const Clause& clause) {
     for (size_t i = 0; i < clause.size(); ++i) {
         for (size_t j = i + 1; j < clause.size(); ++j) {
-            if (clause.literals[i].atom == clause.literals[j].atom &&
-                clause.literals[i].is_positive != clause.literals[j].is_positive) {
+            if (clause.literals_[i].atom_ == clause.literals_[j].atom_ &&
+                clause.literals_[i].is_positive_ != clause.literals_[j].is_positive_) {
                 return true;
             }
         }
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