style: reformat codebase with consistent indentation

49 files changed, 294 insertions, 354 deletions

diff --git a/include/atp/core/clause.h b/include/atp/core/clause.h
index b4d3e68..7e0cbff 100644
--- a/include/atp/core/clause.h
+++ b/include/atp/core/clause.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file clause.h
@@ -25,11 +24,11 @@
 /// NOTE: V1 uses std::vector<Literal> for simplicity.
 /// Future optimization: migrate to a Clause Arena with contiguous storage.
 
-#include <vector>
-
 #include "atp/core/literal.h"
 #include "atp/core/types.h"
 
+#include <vector>
+
 namespace atp {
 
 /// A clause: a disjunction of literals plus provenance for proof reconstruction.
diff --git a/include/atp/core/clause_store.h b/include/atp/core/clause_store.h
index 23db996..5d6562a 100644
--- a/include/atp/core/clause_store.h
+++ b/include/atp/core/clause_store.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file clause_store.h
diff --git a/include/atp/core/literal.h b/include/atp/core/literal.h
index a3192a9..212c281 100644
--- a/include/atp/core/literal.h
+++ b/include/atp/core/literal.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file literal.h
@@ -28,8 +27,8 @@ 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}; }
diff --git a/include/atp/core/symbol_table.h b/include/atp/core/symbol_table.h
index 856c395..30453fc 100644
--- a/include/atp/core/symbol_table.h
+++ b/include/atp/core/symbol_table.h
@@ -16,20 +16,19 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file symbol_table.h
 /// @brief Bidirectional mapping between symbol names and SymbolIds,
 ///        with kind and sort metadata.
 
+#include "atp/core/types.h"
+
 #include <deque>
 #include <string>
 #include <string_view>
 #include <unordered_map>
 
-#include "atp/core/types.h"
-
 namespace atp {
 
 /// Metadata associated with an interned symbol.
diff --git a/include/atp/core/term.h b/include/atp/core/term.h
index 017882a..2be01e7 100644
--- a/include/atp/core/term.h
+++ b/include/atp/core/term.h
@@ -24,22 +24,20 @@
 /// V1 uses vector<TermId> for args.
 /// Future: flat arena with contiguous arg storage for cache locality.
 
-#include <vector>
-
 #include "atp/core/types.h"
 
+#include <vector>
+
 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/types.h b/include/atp/core/types.h
index c68e716..23f2322 100644
--- a/include/atp/core/types.h
+++ b/include/atp/core/types.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file types.h
@@ -57,24 +56,24 @@ enum class SymbolKind : uint8_t {
 /// Deliberately uses uint16_t for extensibility toward algebra/analysis rules.
 enum class InferenceRule : uint16_t {
     // ── Core resolution rules ──
-    kInput            = 0,    ///< Original input clause (axiom / negated conjecture)
-    kResolution       = 1,    ///< Binary resolution
-    kFactoring        = 2,    ///< Factoring
+    kInput = 0,       ///< Original input clause (axiom / negated conjecture)
+    kResolution = 1,  ///< Binary resolution
+    kFactoring = 2,   ///< Factoring
 
     // ── Equality rules (algebra) ──
-    kParamodulation   = 100,  ///< Paramodulation (equality resolution)
-    kDemodulation     = 101,  ///< Demodulation (simplification by rewriting)
-    kEqualityResolution = 102, ///< s != t resolved with unifier
-    kEqualityFactoring  = 103, ///< Factoring with equality
+    kParamodulation = 100,      ///< Paramodulation (equality resolution)
+    kDemodulation = 101,        ///< Demodulation (simplification by rewriting)
+    kEqualityResolution = 102,  ///< s != t resolved with unifier
+    kEqualityFactoring = 103,   ///< Factoring with equality
 
     // ── Simplification rules ──
-    kSubsumption      = 200,  ///< Removed by subsumption
-    kTautologyElim    = 201,  ///< Removed as tautology
-    kPureLiteralElim  = 202,  ///< Pure literal elimination
+    kSubsumption = 200,      ///< Removed by subsumption
+    kTautologyElim = 201,    ///< Removed as tautology
+    kPureLiteralElim = 202,  ///< Pure literal elimination
 
     // ── Theory rules (analysis, arithmetic) ──
     kTheoryResolution = 300,  ///< Theory-specific resolution
-    kTheoryRewrite    = 301,  ///< Theory-driven rewriting
+    kTheoryRewrite = 301,     ///< Theory-driven rewriting
 };
 
 }  // namespace atp
diff --git a/include/atp/frontend/tptp_parser.h b/include/atp/frontend/tptp_parser.h
index 075b45e..738d34b 100644
--- a/include/atp/frontend/tptp_parser.h
+++ b/include/atp/frontend/tptp_parser.h
@@ -42,15 +42,15 @@ namespace atp {
 /// Role of a TPTP formula.
 /// See TPTP spec: https://www.tptp.org/TPTP/SyntaxBNF.html
 enum class FormulaRole : uint8_t {
-    kAxiom,                ///< Background truth
-    kHypothesis,           ///< Problem-specific assumption
-    kDefinition,           ///< Symbol definition (can be unfolded)
-    kAssumption,           ///< Assumed for this proof attempt
-    kLemma,                ///< Derived intermediate result
-    kTheorem,              ///< Previously proved statement (used as axiom)
-    kConjecture,           ///< The statement to prove
-    kNegatedConjecture,    ///< Already negated conjecture (input was cnf)
-    kPlain,                ///< No semantic role specified
+    kAxiom,              ///< Background truth
+    kHypothesis,         ///< Problem-specific assumption
+    kDefinition,         ///< Symbol definition (can be unfolded)
+    kAssumption,         ///< Assumed for this proof attempt
+    kLemma,              ///< Derived intermediate result
+    kTheorem,            ///< Previously proved statement (used as axiom)
+    kConjecture,         ///< The statement to prove
+    kNegatedConjecture,  ///< Already negated conjecture (input was cnf)
+    kPlain,              ///< No semantic role specified
 };
 
 /// Map a TPTP role string to enum. Returns kPlain for unknown roles.
@@ -82,12 +82,10 @@ 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& filepath, TermBank& bank, SymbolTable& symbols);
 
 /// Parse a TPTP string (for testing).
-ParsedProblem parseTptpString(const std::string& input,
-                              TermBank& bank, SymbolTable& symbols);
+ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols);
 
 /// Prepare a parsed problem for proving:
 ///   1. Negate conjecture formulas.
@@ -96,7 +94,6 @@ ParsedProblem parseTptpString(const std::string& input,
 ///   4. Assign ClauseIds and set provenance to kInput.
 ///
 /// Returns the final clause set ready for the Prover.
-std::vector<Clause> prepareForProving(ParsedProblem& problem,
-                                      TermBank& bank, SymbolTable& symbols);
+std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank& bank, SymbolTable& symbols);
 
 }  // namespace atp
diff --git a/include/atp/index/discrim_tree.h b/include/atp/index/discrim_tree.h
index 8cadaa6..c5954d7 100644
--- a/include/atp/index/discrim_tree.h
+++ b/include/atp/index/discrim_tree.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file discrim_tree.h
diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h
index df9cab3..6e2954d 100644
--- a/include/atp/infer/resolution.h
+++ b/include/atp/infer/resolution.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file resolution.h
@@ -24,32 +23,28 @@
 
 #include "atp/core/clause.h"
 #include "atp/core/term_bank.h"
+#include "atp/infer/unification.h"
 
 #include <optional>
 #include <vector>
 
-#include "atp/infer/unification.h"
-
 namespace atp {
 
 /// Attempt binary resolution between two clauses on the specified literal indices.
 /// @return The resolvent clause if resolution succeeds, std::nullopt otherwise.
-std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
-                              const Clause& c2, size_t lit_idx2,
-                              const UnificationConfig& uconfig = {});
+std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2,
+                              size_t lit_idx2, const UnificationConfig& uconfig = {});
 
 /// Generate all possible resolvents between two clauses.
 std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
                                   const UnificationConfig& uconfig = {});
 
 /// Attempt factoring on a single clause (merge two unifiable literals).
-std::vector<Clause> factor(TermBank& bank, const Clause& c,
-                           const UnificationConfig& uconfig = {});
+std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig = {});
 
 /// Rename all variables in a clause to fresh ones, avoiding conflicts
 /// with variables already in the bank.
 Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
                        uint32_t& next_var_id);
 
-
 }  // namespace atp
diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h
index f2ea180..9a4b6cc 100644
--- a/include/atp/infer/unification.h
+++ b/include/atp/infer/unification.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file unification.h
diff --git a/include/atp/normalize/formula.h b/include/atp/normalize/formula.h
index 2cd7900..1bcc021 100644
--- a/include/atp/normalize/formula.h
+++ b/include/atp/normalize/formula.h
@@ -35,15 +35,15 @@ namespace atp {
 
 /// AST node types for first-order logic formulas.
 enum class FormulaKind : uint8_t {
-    kAtom,       ///< Predicate application: P(t1, ..., tn)
-    kEquality,   ///< Equality atom: t1 = t2 (distinguished for equality reasoning)
-    kNot,        ///< Negation: ¬F
-    kAnd,        ///< Conjunction: F ∧ G
-    kOr,         ///< Disjunction: F ∨ G
-    kImplies,    ///< Implication: F → G
-    kIff,        ///< Biconditional: F ↔ G
-    kForall,     ///< Universal: ∀x. F
-    kExists,     ///< Existential: ∃x. F
+    kAtom,      ///< Predicate application: P(t1, ..., tn)
+    kEquality,  ///< Equality atom: t1 = t2 (distinguished for equality reasoning)
+    kNot,       ///< Negation: ¬F
+    kAnd,       ///< Conjunction: F ∧ G
+    kOr,        ///< Disjunction: F ∨ G
+    kImplies,   ///< Implication: F → G
+    kIff,       ///< Biconditional: F ↔ G
+    kForall,    ///< Universal: ∀x. F
+    kExists,    ///< Existential: ∃x. F
 };
 
 /// A first-order logic formula node.
@@ -77,10 +77,8 @@ struct Formula {
                                                 std::unique_ptr<Formula> rhs);
     static std::unique_ptr<Formula> makeIff(std::unique_ptr<Formula> lhs,
                                             std::unique_ptr<Formula> rhs);
-    static std::unique_ptr<Formula> makeForall(SymbolId var,
-                                               std::unique_ptr<Formula> body);
-    static std::unique_ptr<Formula> makeExists(SymbolId var,
-                                               std::unique_ptr<Formula> body);
+    static std::unique_ptr<Formula> makeForall(SymbolId var, std::unique_ptr<Formula> body);
+    static std::unique_ptr<Formula> makeExists(SymbolId var, std::unique_ptr<Formula> body);
 };
 
 }  // namespace atp
diff --git a/include/atp/proof/proof_trace.h b/include/atp/proof/proof_trace.h
index a80a327..28099fe 100644
--- a/include/atp/proof/proof_trace.h
+++ b/include/atp/proof/proof_trace.h
@@ -49,7 +49,7 @@ std::string termToString(TermId id, const TermBank& bank);
 std::string clauseToString(const Clause& clause, const TermBank& bank);
 
 /// Format a proof as a human-readable string.
-std::string formatProof(const std::vector<ProofStep>& proof,
-                        const ClauseStore& store, const TermBank& bank);
+std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore& store,
+                        const TermBank& bank);
 
 }  // namespace atp
diff --git a/include/atp/rewrite/ordering.h b/include/atp/rewrite/ordering.h
index 5696766..195c3c6 100644
--- a/include/atp/rewrite/ordering.h
+++ b/include/atp/rewrite/ordering.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file ordering.h
@@ -34,10 +33,10 @@ namespace atp {
 
 /// Ordering comparison result.
 enum class OrderResult : uint8_t {
-    kLessThan,       ///< t1 < t2
-    kEqual,          ///< t1 = t2
-    kGreaterThan,    ///< t1 > t2
-    kIncomparable,   ///< t1 and t2 are incomparable
+    kLessThan,      ///< t1 < t2
+    kEqual,         ///< t1 = t2
+    kGreaterThan,   ///< t1 > t2
+    kIncomparable,  ///< t1 and t2 are incomparable
 };
 
 /// Abstract base for term orderings.
@@ -47,8 +46,7 @@ class TermOrdering {
     virtual ~TermOrdering() = default;
 
     /// Compare two terms under the ordering.
-    [[nodiscard]] virtual OrderResult compare(const TermBank& bank, TermId t1,
-                                              TermId t2) const = 0;
+    [[nodiscard]] virtual OrderResult compare(const TermBank& bank, TermId t1, TermId t2) const = 0;
 };
 
 }  // namespace atp
diff --git a/include/atp/rewrite/paramodulation.h b/include/atp/rewrite/paramodulation.h
index f43cd7b..9dfbd66 100644
--- a/include/atp/rewrite/paramodulation.h
+++ b/include/atp/rewrite/paramodulation.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file paramodulation.h
diff --git a/include/atp/search/clause_queue.h b/include/atp/search/clause_queue.h
index 828a725..6a8f9fc 100644
--- a/include/atp/search/clause_queue.h
+++ b/include/atp/search/clause_queue.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file clause_queue.h
diff --git a/include/atp/search/prover.h b/include/atp/search/prover.h
index d84a647..6ee22f0 100644
--- a/include/atp/search/prover.h
+++ b/include/atp/search/prover.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file prover.h
@@ -39,9 +38,9 @@ namespace atp {
 
 /// Result of a proof attempt.
 enum class ProverResult : uint8_t {
-    kTheorem,       ///< Empty clause derived — conjecture is a theorem
-    kSaturation,    ///< Search space saturated — cannot prove
-    kTimeout,       ///< Resource limit exceeded
+    kTheorem,     ///< Empty clause derived — conjecture is a theorem
+    kSaturation,  ///< Search space saturated — cannot prove
+    kTimeout,     ///< Resource limit exceeded
 };
 
 /// V1 configuration — simple and direct.
diff --git a/include/atp/simplify/subsumption.h b/include/atp/simplify/subsumption.h
index c39b586..970b6d8 100644
--- a/include/atp/simplify/subsumption.h
+++ b/include/atp/simplify/subsumption.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file subsumption.h
diff --git a/include/atp/simplify/tautology.h b/include/atp/simplify/tautology.h
index 80aa1f9..f17f0c7 100644
--- a/include/atp/simplify/tautology.h
+++ b/include/atp/simplify/tautology.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file tautology.h
diff --git a/include/atp/strategy/calculus.h b/include/atp/strategy/calculus.h
index ee8ee09..e06988e 100644
--- a/include/atp/strategy/calculus.h
+++ b/include/atp/strategy/calculus.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file calculus.h
diff --git a/include/atp/strategy/inference_rule.h b/include/atp/strategy/inference_rule.h
index 1c7dbba..88b6fe0 100644
--- a/include/atp/strategy/inference_rule.h
+++ b/include/atp/strategy/inference_rule.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file inference_rule.h
@@ -62,9 +61,10 @@ class GeneratingRule : public InferenceRuleBase {
     /// @param processed All previously processed clauses (accessed via store).
     /// @param bank      The global term bank.
     /// @return Newly generated clauses (not yet added to the store).
-    [[nodiscard]] virtual std::vector<Clause> generate(
-        const Clause& given, const std::vector<ClauseId>& processed,
-        const ClauseStore& store, TermBank& bank) const = 0;
+    [[nodiscard]] virtual std::vector<Clause> generate(const Clause& given,
+                                                       const std::vector<ClauseId>& processed,
+                                                       const ClauseStore& store,
+                                                       TermBank& bank) const = 0;
 };
 
 /// Simplifying inference rule: rewrite or delete a clause in-place.
@@ -74,8 +74,7 @@ class SimplifyingRule : public InferenceRuleBase {
 
     /// Attempt to simplify a clause. Returns true if the clause was modified.
     /// If the clause should be deleted entirely, clear its literals.
-    virtual bool simplify(Clause& clause, const ClauseStore& store,
-                          TermBank& bank) const = 0;
+    virtual bool simplify(Clause& clause, const ClauseStore& store, TermBank& bank) const = 0;
 };
 
 }  // namespace atp
diff --git a/include/atp/strategy/problem_analyzer.h b/include/atp/strategy/problem_analyzer.h
index b5fdef4..5e6c5cf 100644
--- a/include/atp/strategy/problem_analyzer.h
+++ b/include/atp/strategy/problem_analyzer.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file problem_analyzer.h
@@ -41,10 +40,10 @@ namespace atp {
 
 /// Features detected in the input problem.
 struct ProblemFeatures {
-    bool has_equality = false;        ///< Contains '=' predicate
+    bool has_equality = false;             ///< Contains '=' predicate
     bool is_purely_propositional = false;  ///< No function symbols, no variables
-    bool is_horn = false;             ///< All clauses are Horn clauses
-    bool has_existential = false;     ///< Had existential quantifiers (Skolemized)
+    bool is_horn = false;                  ///< All clauses are Horn clauses
+    bool has_existential = false;          ///< Had existential quantifiers (Skolemized)
     size_t num_clauses = 0;
     size_t num_predicates = 0;
     size_t num_functions = 0;
diff --git a/include/atp/utils/hash_utils.h b/include/atp/utils/hash_utils.h
index 4531fa6..ae31f43 100644
--- a/include/atp/utils/hash_utils.h
+++ b/include/atp/utils/hash_utils.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file hash_utils.h
diff --git a/include/atp/utils/logger.h b/include/atp/utils/logger.h
index 95d3dd2..de77c54 100644
--- a/include/atp/utils/logger.h
+++ b/include/atp/utils/logger.h
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file logger.h
@@ -28,16 +27,15 @@
 #define ATP_LOG_LEVEL 2  // 0=TRACE, 1=DEBUG, 2=INFO, 3=WARN, 4=ERROR
 #endif
 
-#define ATP_LOG(level, level_str, fmt, ...)                        \
-    do {                                                           \
-        if constexpr (level >= ATP_LOG_LEVEL) {                    \
-            std::fprintf(stderr, "[%s] " fmt "\n", level_str,     \
-                         ##__VA_ARGS__);                           \
-        }                                                          \
+#define ATP_LOG(level, level_str, fmt, ...)                                   \
+    do {                                                                      \
+        if constexpr (level >= ATP_LOG_LEVEL) {                               \
+            std::fprintf(stderr, "[%s] " fmt "\n", level_str, ##__VA_ARGS__); \
+        }                                                                     \
     } while (0)
 
 #define ATP_TRACE(fmt, ...) ATP_LOG(0, "TRACE", fmt, ##__VA_ARGS__)
 #define ATP_DEBUG(fmt, ...) ATP_LOG(1, "DEBUG", fmt, ##__VA_ARGS__)
-#define ATP_INFO(fmt, ...)  ATP_LOG(2, "INFO",  fmt, ##__VA_ARGS__)
-#define ATP_WARN(fmt, ...)  ATP_LOG(3, "WARN",  fmt, ##__VA_ARGS__)
+#define ATP_INFO(fmt, ...) ATP_LOG(2, "INFO", fmt, ##__VA_ARGS__)
+#define ATP_WARN(fmt, ...) ATP_LOG(3, "WARN", fmt, ##__VA_ARGS__)
 #define ATP_ERROR(fmt, ...) ATP_LOG(4, "ERROR", fmt, ##__VA_ARGS__)
diff --git a/src/core/clause_store.cc b/src/core/clause_store.cc
index a0adbe6..75959c3 100644
--- a/src/core/clause_store.cc
+++ b/src/core/clause_store.cc
@@ -17,6 +17,7 @@
  */
 
 #include "atp/core/clause_store.h"
+
 #include <cassert>
 #include <utility>
 
diff --git a/src/core/symbol_table.cc b/src/core/symbol_table.cc
index 261805a..42c7dd8 100644
--- a/src/core/symbol_table.cc
+++ b/src/core/symbol_table.cc
@@ -17,15 +17,16 @@
  */
 
 #include "atp/core/symbol_table.h"
+
 #include "atp/core/types.h"
+
 #include <cstddef>
 #include <stdexcept>
 #include <string_view>
 
 namespace atp {
 
-SymbolId SymbolTable::intern(std::string_view name, SymbolKind kind, uint16_t arity,
-                    SortId sort) {
+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;
@@ -58,5 +59,4 @@ size_t SymbolTable::size() const {
     return infos_.size();
 }
 
-} // namespace atp
-
+}  // namespace atp
diff --git a/src/core/term_bank.cc b/src/core/term_bank.cc
index 53b4f0c..8c8ef29 100644
--- a/src/core/term_bank.cc
+++ b/src/core/term_bank.cc
@@ -17,7 +17,9 @@
  */
 
 #include "atp/core/term_bank.h"
+
 #include "atp/core/types.h"
+
 #include <cassert>
 
 namespace atp {
diff --git a/src/frontend/tptp_parser.cc b/src/frontend/tptp_parser.cc
index df8baeb..2f32522 100644
--- a/src/frontend/tptp_parser.cc
+++ b/src/frontend/tptp_parser.cc
@@ -17,10 +17,12 @@
  */
 
 #include "atp/frontend/tptp_parser.h"
+
 #include "atp/core/clause.h"
 #include "atp/core/literal.h"
 #include "atp/core/term_bank.h"
 #include "atp/core/types.h"
+
 #include <cctype>
 #include <fstream>
 #include <stdexcept>
@@ -31,31 +33,29 @@
 
 namespace atp {
 
-FormulaRole parseRole(std::string_view role_str){
-    if (role_str == "axiom") return FormulaRole::kAxiom;
-    if (role_str == "hypothesis") return FormulaRole::kHypothesis;
-    if (role_str == "definition") return FormulaRole::kDefinition;
-    if (role_str == "assumption") return FormulaRole::kAssumption;
-    if (role_str == "lemma") return FormulaRole::kLemma;
-    if (role_str == "theorem") return FormulaRole::kTheorem;
-    if (role_str == "conjecture") return FormulaRole::kConjecture;
-    if (role_str == "negated_conjecture") return FormulaRole::kNegatedConjecture;
-    if (role_str == "plain") return FormulaRole::kPlain;
+FormulaRole parseRole(std::string_view role_str) {
+    if (role_str == "axiom")
+        return FormulaRole::kAxiom;
+    if (role_str == "hypothesis")
+        return FormulaRole::kHypothesis;
+    if (role_str == "definition")
+        return FormulaRole::kDefinition;
+    if (role_str == "assumption")
+        return FormulaRole::kAssumption;
+    if (role_str == "lemma")
+        return FormulaRole::kLemma;
+    if (role_str == "theorem")
+        return FormulaRole::kTheorem;
+    if (role_str == "conjecture")
+        return FormulaRole::kConjecture;
+    if (role_str == "negated_conjecture")
+        return FormulaRole::kNegatedConjecture;
+    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 { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown };
 
 struct Token {
     TokenType type;
@@ -65,7 +65,7 @@ struct Token {
 };
 
 class TptpLexer {
-public:
+  public:
     explicit TptpLexer(std::string_view input) : source_(input) {}
 
     Token next_token() {
@@ -80,25 +80,40 @@ public:
         char c = source_[pos_];
 
         if (std::isalpha(static_cast<unsigned char>(c)) || c == '_') {
-            while (pos_ < source_.size() && (std::isalnum(static_cast<unsigned char>(source_[pos_])) || source_[pos_] == '_')) {
+            while (
+                pos_ < source_.size() &&
+                (std::isalnum(static_cast<unsigned char>(source_[pos_])) || source_[pos_] == '_')) {
                 advance_char();
             }
-            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();
         switch (c) {
-            case '(': return {.type = TokenType::kLParen, .value = "(", .line = line_, .column = column_};
-            case ')': return {.type = TokenType::kRParen, .value = ")", .line = line_, .column = column_};
-            case ',': return {.type = TokenType::kComma, .value = ",", .line = line_, .column = column_};
-            case '.': return {.type = TokenType::kDot, .value = ".", .line = line_, .column = column_};
-            case '~': return {.type = TokenType::kNot, .value = "~", .line = line_, .column = column_};
-            case '|': return {.type = TokenType::kOr, .value = "|", .line = line_, .column = column_};
-            default: return {.type = TokenType::kUnkown, .value = source_.substr(start_pos, 1), .line = line_, .column = column_};
+            case '(':
+                return {.type = TokenType::kLParen, .value = "(", .line = line_, .column = column_};
+            case ')':
+                return {.type = TokenType::kRParen, .value = ")", .line = line_, .column = column_};
+            case ',':
+                return {.type = TokenType::kComma, .value = ",", .line = line_, .column = column_};
+            case '.':
+                return {.type = TokenType::kDot, .value = ".", .line = line_, .column = column_};
+            case '~':
+                return {.type = TokenType::kNot, .value = "~", .line = line_, .column = column_};
+            case '|':
+                return {.type = TokenType::kOr, .value = "|", .line = line_, .column = column_};
+            default:
+                return {.type = TokenType::kUnkown,
+                        .value = source_.substr(start_pos, 1),
+                        .line = line_,
+                        .column = column_};
         }
     }
 
-private:
+  private:
     std::string_view source_;
     size_t pos_ = 0;
     size_t line_ = 1;
@@ -133,8 +148,9 @@ private:
 };
 
 class TptpParser {
-public:
-    explicit TptpParser(std::string_view input, TermBank& bank, SymbolTable& symbols) : lexer_(input), bank_(bank), symbols_(symbols) {
+  public:
+    explicit TptpParser(std::string_view input, TermBank& bank, SymbolTable& symbols)
+        : lexer_(input), bank_(bank), symbols_(symbols) {
         advance();
     }
 
@@ -146,11 +162,11 @@ public:
 
                 AnnotatedFormula af;
                 af.is_cnf = true;
-                
+
                 af.name = std::string(current_token_.value);
                 expect(TokenType::kWord);
                 expect(TokenType::kComma);
-                
+
                 af.role = parseRole(current_token_.value);
                 expect(TokenType::kWord);
                 expect(TokenType::kComma);
@@ -169,14 +185,16 @@ public:
 
                 variable_cache_.clear();
             } else if (current_token_.value == "fof") {
-                throw std::runtime_error("FOF parsing not implemented. Line " + std::to_string(current_token_.line));
+                throw std::runtime_error("FOF parsing not implemented. Line " +
+                                         std::to_string(current_token_.line));
             } else {
-                throw std::runtime_error("Unknown declaration: '" + std::string(current_token_.value) + "'");
+                throw std::runtime_error("Unknown declaration: '" +
+                                         std::string(current_token_.value) + "'");
             }
         }
     }
 
-private:
+  private:
     TptpLexer lexer_;
     TermBank& bank_;
     SymbolTable& symbols_;
@@ -184,24 +202,25 @@ private:
 
     std::unordered_map<std::string_view, TermId> variable_cache_;
 
-    void advance() {
-        current_token_ = lexer_.next_token();
-    }
+    void advance() { current_token_ = lexer_.next_token(); }
 
     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) + "'");
+            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) {
-            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) + "'");
+            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::string_view name = current_token_.value;
@@ -253,14 +272,14 @@ private:
     }
 };
 
-ParsedProblem parseTptpString(const std::string &input, TermBank &bank, SymbolTable &symbols){
+ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols) {
     ParsedProblem problem;
     TptpParser parser(input, bank, symbols);
     parser.parseProblem(problem);
     return problem;
 }
 
-ParsedProblem parseTptpFile(const std::string &filename, TermBank &bank, SymbolTable &symbols){
+ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolTable& symbols) {
     std::ifstream file(filename, std::ios::binary);
     if (!file.is_open()) {
         throw std::runtime_error("Failed to open file: " + filename);
@@ -271,12 +290,13 @@ ParsedProblem parseTptpFile(const std::string &filename, TermBank &bank, SymbolT
     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){
+    for (auto& af : problem.formulas) {
+        if (af.is_cnf) {
+            for (auto& clause : af.clauses) {
                 clause.rule = InferenceRule::kInput;
                 clause.parent1 = kInvalidId;
                 clause.parent2 = kInvalidId;
@@ -287,4 +307,4 @@ std::vector<Clause> prepareForProving(ParsedProblem &problem, TermBank &bank, Sy
     return final_clauses;
 }
 
-} // namespace atp
+}  // namespace atp
diff --git a/src/index/discrim_tree.cc b/src/index/discrim_tree.cc
index b62ffd0..17c63f8 100644
--- a/src/index/discrim_tree.cc
+++ b/src/index/discrim_tree.cc
@@ -15,5 +15,3 @@
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
-
-
diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc
index 3c82460..f072b8e 100644
--- a/src/infer/resolution.cc
+++ b/src/infer/resolution.cc
@@ -17,6 +17,7 @@
  */
 
 #include "atp/infer/resolution.h"
+
 #include "atp/core/clause.h"
 #include "atp/core/symbol_table.h"
 #include "atp/core/term.h"
@@ -34,8 +35,7 @@ namespace atp {
 namespace {
 
 /// Recursively collect all variable TermIds appearing in a term.
-void collectVariables(TermId term, const TermBank& bank,
-                      std::unordered_map<TermId, bool>& seen) {
+void collectVariables(TermId term, const TermBank& bank, std::unordered_map<TermId, bool>& seen) {
     if (bank.isVariable(term)) {
         seen[term] = true;
         return;
@@ -84,9 +84,8 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
     return renamed;
 }
 
-std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
-                              const Clause& c2, size_t lit_idx2,
-                              const UnificationConfig& uconfig) {
+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) {
         return std::nullopt;
@@ -142,8 +141,7 @@ std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause
     return results;
 }
 
-std::vector<Clause> factor(TermBank& bank, const Clause& c,
-                           const UnificationConfig& uconfig) {
+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) {
diff --git a/src/infer/substitution.cc b/src/infer/substitution.cc
index c570676..a7ce617 100644
--- a/src/infer/substitution.cc
+++ b/src/infer/substitution.cc
@@ -17,6 +17,7 @@
  */
 
 #include "atp/infer/substitution.h"
+
 #include "atp/core/term.h"
 #include "atp/core/term_bank.h"
 #include "atp/core/types.h"
diff --git a/src/infer/unification.cc b/src/infer/unification.cc
index be8a025..66e1af6 100644
--- a/src/infer/unification.cc
+++ b/src/infer/unification.cc
@@ -16,72 +16,72 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #include "atp/infer/unification.h"
+
 #include "atp/core/types.h"
 #include "atp/infer/substitution.h"
 
 namespace atp {
 
-    bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
+bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
            const UnificationConfig& config) {
-        t1 = subst.resolve(t1, bank);
-        t2 = subst.resolve(t2, bank);
+    t1 = subst.resolve(t1, bank);
+    t2 = subst.resolve(t2, bank);
 
-        if (t1 == t2) {
-            return true;
-        }
+    if (t1 == t2) {
+        return true;
+    }
 
-        if (bank.isVariable(t1)) {
-            if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) {
-                return false;
-            }
-            subst.bind(t1, t2);
-            return true;
+    if (bank.isVariable(t1)) {
+        if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) {
+            return false;
         }
+        subst.bind(t1, t2);
+        return true;
+    }
 
-        if (bank.isVariable(t2)) {
-            if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) {
-                return false;
-            }
-            subst.bind(t2, t1);
-            return true;
+    if (bank.isVariable(t2)) {
+        if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) {
+            return false;
         }
+        subst.bind(t2, t1);
+        return true;
+    }
+
+    const Term& term1 = bank.getTerm(t1);
+    const Term& term2 = bank.getTerm(t2);
 
-        const Term& term1 = bank.getTerm(t1);
-        const Term& term2 = bank.getTerm(t2);
+    if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) {
+        return false;
+    }
 
-        if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) {
+    for (size_t i = 0; i < term1.arity(); ++i) {
+        if (!unify(bank, term1.args[i], term2.args[i], subst, config)) {
             return false;
         }
+    }
 
-        for (size_t i = 0; i < term1.arity(); ++i) {
-            if (!unify(bank, term1.args[i], term2.args[i], subst, config)) {
-                return false;
-            }
-        }
+    return true;
+}
 
-        return true;
+TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) {
+    term = subst.resolve(term, bank);
+    if (bank.isVariable(term)) {
+        return term;
     }
 
-    TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) {
-        term = subst.resolve(term, bank);
-        if (bank.isVariable(term)) {
-            return term;
-        }
-
-        // 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!
+    // 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!
 
-        std::vector<TermId> new_args;
-        new_args.reserve(old_args.size());
-        for (TermId arg : old_args) {
-            new_args.push_back(applySubstitution(subst, arg, bank));
-        }
-        return bank.makeTerm(sym, new_args);
+    std::vector<TermId> new_args;
+    new_args.reserve(old_args.size());
+    for (TermId arg : old_args) {
+        new_args.push_back(applySubstitution(subst, arg, bank));
     }
+    return bank.makeTerm(sym, new_args);
+}
 
 }  // namespace atp
\ No newline at end of file
diff --git a/src/main.cc b/src/main.cc
index bf49c02..bd385d8 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -52,8 +52,8 @@ int main(int argc, char* argv[]) {
         // 2. Parse TPTP input
         auto problem = atp::parseTptpFile(filepath, bank, symbols);
 
-        std::cerr << "% Parsed " << problem.formulas.size()
-                  << " formulas from " << filepath << "\n";
+        std::cerr << "% Parsed " << problem.formulas.size() << " formulas from " << filepath
+                  << "\n";
 
         // 3. Prepare clauses for proving
         auto clauses = atp::prepareForProving(problem, bank, symbols);
diff --git a/src/normalize/clausifier.cc b/src/normalize/clausifier.cc
index b62ffd0..17c63f8 100644
--- a/src/normalize/clausifier.cc
+++ b/src/normalize/clausifier.cc
@@ -15,5 +15,3 @@
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
-
-
diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc
index 66038ba..183ab2e 100644
--- a/src/proof/proof_trace.cc
+++ b/src/proof/proof_trace.cc
@@ -17,6 +17,7 @@
  */
 
 #include "atp/proof/proof_trace.h"
+
 #include "atp/core/clause.h"
 #include "atp/core/symbol_table.h"
 #include "atp/core/term.h"
@@ -31,7 +32,7 @@
 
 namespace atp {
 
-// ─── extractProof 
+// extractProof
 // DFS from empty clause back to axioms, collect all participating clauses,
 // then reverse for topological order (axioms first).
 
@@ -72,7 +73,7 @@ std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_cla
     return steps;
 }
 
-// ─── termToString (public — raw names) ──────────────────────────────────
+// termToString
 
 std::string termToString(TermId id, const TermBank& bank) {
     const Term& t = bank.getTerm(id);
@@ -93,7 +94,7 @@ std::string termToString(TermId id, const TermBank& bank) {
     return result;
 }
 
-// ─── Pretty variable names ──────────────────────────────────────────────
+// Pretty variable names
 
 namespace {
 
@@ -145,7 +146,7 @@ std::string termToPretty(TermId id, const TermBank& bank,
 
 }  // namespace
 
-// ─── clauseToString ─────────────────────────────────────────────────────
+// clauseToString
 
 std::string clauseToString(const Clause& clause, const TermBank& bank) {
     if (clause.isEmpty()) {
@@ -168,21 +169,25 @@ std::string clauseToString(const Clause& clause, const TermBank& bank) {
     return result;
 }
 
-// ─── ruleToString 
+// 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";
+        case InferenceRule::kInput:
+            return "input";
+        case InferenceRule::kResolution:
+            return "resolution";
+        case InferenceRule::kFactoring:
+            return "factoring";
+        default:
+            return "unknown";
     }
 }
 
-// ─── formatProof 
+// formatProof
 
-std::string formatProof(const std::vector<ProofStep>& proof,
-                        const ClauseStore& store, const TermBank& bank) {
+std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore& store,
+                        const TermBank& bank) {
     // 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) {
diff --git a/src/rewrite/ordering.cc b/src/rewrite/ordering.cc
index b62ffd0..17c63f8 100644
--- a/src/rewrite/ordering.cc
+++ b/src/rewrite/ordering.cc
@@ -15,5 +15,3 @@
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
-
-
diff --git a/src/rewrite/paramodulation.cc b/src/rewrite/paramodulation.cc
index b62ffd0..17c63f8 100644
--- a/src/rewrite/paramodulation.cc
+++ b/src/rewrite/paramodulation.cc
@@ -15,5 +15,3 @@
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
-
-
diff --git a/src/search/prover.cc b/src/search/prover.cc
index e1b117b..5b68e9d 100644
--- a/src/search/prover.cc
+++ b/src/search/prover.cc
@@ -17,6 +17,7 @@
  */
 
 #include "atp/search/prover.h"
+
 #include "atp/core/types.h"
 #include "atp/infer/resolution.h"
 #include "atp/infer/unification.h"
@@ -28,10 +29,7 @@
 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) {
@@ -46,8 +44,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;
@@ -81,9 +78,8 @@ ProverResult Prover::prove() {
         // 4. Backward subsumption
         // Remove from processed all clauses that are subsumed by given.
         // Use erase-remove idiom for O(n) scan instead of repeated erase.
-        std::erase_if(processed_, [&](ClauseId pid) {
-            return subsumes(given, store_.getClause(pid));
-        });
+        std::erase_if(processed_,
+                      [&](ClauseId pid) { return subsumes(given, store_.getClause(pid)); });
 
         // 5. Generate new clauses
         // Inference BEFORE adding given to processed — matches doc §4.6.
@@ -129,12 +125,8 @@ 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;
+            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);
 
             // 7d. Store the clause (needed for forward subsumption check)
diff --git a/src/simplify/subsumption.cc b/src/simplify/subsumption.cc
index cf243c9..3756d82 100644
--- a/src/simplify/subsumption.cc
+++ b/src/simplify/subsumption.cc
@@ -18,25 +18,24 @@
 
 #include "atp/simplify/subsumption.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) {
-            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) {
-                    found = true;
-                    break;
-                }
-            }
-            if (!found) {
-                return false;
+bool subsumes(const Clause& general, const Clause& specific) {
+    if (general.size() > specific.size()) {
+        return false;
+    }
+    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) {
+                found = true;
+                break;
             }
         }
-        return true;
+        if (!found) {
+            return false;
+        }
     }
+    return true;
 }
+}  // namespace atp
diff --git a/src/simplify/tautology.cc b/src/simplify/tautology.cc
index d41ecd7..70bdced 100644
--- a/src/simplify/tautology.cc
+++ b/src/simplify/tautology.cc
@@ -17,18 +17,19 @@
  */
 
 #include "atp/simplify/tautology.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) {
-                    return true;
-                }
+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) {
+                return true;
             }
         }
-        return false;
     }
-}
\ No newline at end of file
+    return false;
+}
+}  // namespace atp
\ No newline at end of file
diff --git a/src/strategy/problem_analyzer.cc b/src/strategy/problem_analyzer.cc
index b62ffd0..17c63f8 100644
--- a/src/strategy/problem_analyzer.cc
+++ b/src/strategy/problem_analyzer.cc
@@ -15,5 +15,3 @@
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
-
-
diff --git a/tests/test_clausifier.cc b/tests/test_clausifier.cc
index b62ffd0..17c63f8 100644
--- a/tests/test_clausifier.cc
+++ b/tests/test_clausifier.cc
@@ -15,5 +15,3 @@
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
-
-
diff --git a/tests/test_discrim_tree.cc b/tests/test_discrim_tree.cc
index b62ffd0..17c63f8 100644
--- a/tests/test_discrim_tree.cc
+++ b/tests/test_discrim_tree.cc
@@ -15,5 +15,3 @@
  * You should have received a copy of the GNU General Public License
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
-
-
diff --git a/tests/test_end_to_end.cc b/tests/test_end_to_end.cc
index 44a44c2..d45a101 100644
--- a/tests/test_end_to_end.cc
+++ b/tests/test_end_to_end.cc
@@ -19,8 +19,6 @@
 /// @file test_end_to_end.cc
 /// @brief End-to-end tests: TPTP string → parse → prove → verify result.
 
-#include <gtest/gtest.h>
-
 #include "atp/core/clause_store.h"
 #include "atp/core/symbol_table.h"
 #include "atp/core/term_bank.h"
@@ -28,6 +26,7 @@
 #include "atp/proof/proof_trace.h"
 #include "atp/search/prover.h"
 
+#include <gtest/gtest.h>
 #include <string>
 
 namespace atp {
@@ -175,9 +174,9 @@ TEST(EndToEnd, MonkeyBanana) {
         cnf(negated_goal, negated_conjecture, ~goal_reached(S)).
     )");
 
-    EXPECT_EQ(result, ProverResult::kTheorem)
-        << "ATP should prove the monkey can get the banana!\n"
-        << "Proof output:\n" << proof;
+    EXPECT_EQ(result, ProverResult::kTheorem) << "ATP should prove the monkey can get the banana!\n"
+                                              << "Proof output:\n"
+                                              << proof;
 }
 
 }  // namespace
diff --git a/tests/test_proof_trace.cc b/tests/test_proof_trace.cc
index d7ff246..5e12060 100644
--- a/tests/test_proof_trace.cc
+++ b/tests/test_proof_trace.cc
@@ -16,8 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-#include <gtest/gtest.h>
-
 #include "atp/core/clause.h"
 #include "atp/core/clause_store.h"
 #include "atp/core/literal.h"
@@ -27,6 +25,7 @@
 #include "atp/proof/proof_trace.h"
 #include "atp/search/prover.h"
 
+#include <gtest/gtest.h>
 #include <string>
 
 namespace atp {
@@ -125,10 +124,7 @@ 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))})
-    });
+    prover.addClauses({makeClause({pos(P(a_term))}), makeClause({neg(P(a_term))})});
     ProverResult result = prover.prove();
     ASSERT_EQ(result, ProverResult::kTheorem);
 
@@ -149,11 +145,8 @@ TEST_F(ProofTraceTest, ExtractProofTrivial) {
 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))})
-    });
+    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();
     ASSERT_EQ(result, ProverResult::kTheorem);
 
@@ -174,10 +167,7 @@ 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.addClauses({makeClause({pos(P(a_term))}), makeClause({neg(P(a_term))})});
     prover.prove();
 
     auto eid = prover.getEmptyClauseId();
@@ -197,10 +187,7 @@ TEST_F(ProofTraceTest, FormatProofContainsExpectedElements) {
 
 TEST_F(ProofTraceTest, FormatProofNoParentsForAxioms) {
     Prover prover(bank, store);
-    prover.addClauses({
-        makeClause({pos(P(a_term))}),
-        makeClause({neg(P(a_term))})
-    });
+    prover.addClauses({makeClause({pos(P(a_term))}), makeClause({neg(P(a_term))})});
     prover.prove();
 
     auto eid = prover.getEmptyClauseId();
diff --git a/tests/test_prover.cc b/tests/test_prover.cc
index cec1c35..ada1af2 100644
--- a/tests/test_prover.cc
+++ b/tests/test_prover.cc
@@ -16,8 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-#include <gtest/gtest.h>
-
 #include "atp/core/clause.h"
 #include "atp/core/clause_store.h"
 #include "atp/core/literal.h"
@@ -26,6 +24,8 @@
 #include "atp/core/types.h"
 #include "atp/search/prover.h"
 
+#include <gtest/gtest.h>
+
 namespace atp {
 namespace {
 
@@ -79,10 +79,7 @@ class ProverTest : public ::testing::Test {
 
 TEST_F(ProverTest, TrivialRefutation) {
     Prover prover(bank, store);
-    prover.addClauses({
-        makeClause({pos(P(a))}),
-        makeClause({neg(P(a))})
-    });
+    prover.addClauses({makeClause({pos(P(a))}), makeClause({neg(P(a))})});
 
     ProverResult result = prover.prove();
     EXPECT_EQ(result, ProverResult::kTheorem);
@@ -95,10 +92,7 @@ TEST_F(ProverTest, TrivialRefutation) {
 
 TEST_F(ProverTest, RefutationWithUnification) {
     Prover prover(bank, store);
-    prover.addClauses({
-        makeClause({pos(P(X))}),
-        makeClause({neg(P(a))})
-    });
+    prover.addClauses({makeClause({pos(P(X))}), makeClause({neg(P(a))})});
 
     ProverResult result = prover.prove();
     EXPECT_EQ(result, ProverResult::kTheorem);
@@ -112,11 +106,8 @@ TEST_F(ProverTest, RefutationWithUnification) {
 
 TEST_F(ProverTest, TwoStepRefutation) {
     Prover prover(bank, store);
-    prover.addClauses({
-        makeClause({pos(P(a))}),
-        makeClause({neg(P(X)), pos(Q(X))}),
-        makeClause({neg(Q(a))})
-    });
+    prover.addClauses(
+        {makeClause({pos(P(a))}), makeClause({neg(P(X)), pos(Q(X))}), makeClause({neg(Q(a))})});
 
     ProverResult result = prover.prove();
     EXPECT_EQ(result, ProverResult::kTheorem);
@@ -128,10 +119,7 @@ TEST_F(ProverTest, TwoStepRefutation) {
 
 TEST_F(ProverTest, Saturation) {
     Prover prover(bank, store);
-    prover.addClauses({
-        makeClause({pos(P(a))}),
-        makeClause({pos(Q(b))})
-    });
+    prover.addClauses({makeClause({pos(P(a))}), makeClause({pos(Q(b))})});
 
     ProverResult result = prover.prove();
     EXPECT_EQ(result, ProverResult::kSaturation);
@@ -147,12 +135,8 @@ TEST_F(ProverTest, Timeout) {
 
     // 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.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);
@@ -168,10 +152,10 @@ TEST_F(ProverTest, ThreeStepChain) {
 
     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();
@@ -184,10 +168,8 @@ TEST_F(ProverTest, ThreeStepChain) {
 
 TEST_F(ProverTest, EmptyClauseInInput) {
     Prover prover(bank, store);
-    prover.addClauses({
-        makeClause({}),  // empty clause directly
-        makeClause({pos(P(a))})
-    });
+    prover.addClauses({makeClause({}),  // empty clause directly
+                       makeClause({pos(P(a))})});
 
     // Empty clause should be detected immediately when selected from queue
     ProverResult result = prover.prove();
diff --git a/tests/test_resolution.cc b/tests/test_resolution.cc
index 767e865..931635d 100644
--- a/tests/test_resolution.cc
+++ b/tests/test_resolution.cc
@@ -16,8 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-#include <gtest/gtest.h>
-
 #include "atp/core/clause.h"
 #include "atp/core/literal.h"
 #include "atp/core/symbol_table.h"
@@ -27,6 +25,8 @@
 #include "atp/infer/substitution.h"
 #include "atp/infer/unification.h"
 
+#include <gtest/gtest.h>
+
 namespace atp {
 namespace {
 
diff --git a/tests/test_simplify.cc b/tests/test_simplify.cc
index 07875de..98b0db9 100644
--- a/tests/test_simplify.cc
+++ b/tests/test_simplify.cc
@@ -16,8 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-#include <gtest/gtest.h>
-
 #include "atp/core/clause.h"
 #include "atp/core/literal.h"
 #include "atp/core/symbol_table.h"
@@ -26,6 +24,8 @@
 #include "atp/simplify/subsumption.h"
 #include "atp/simplify/tautology.h"
 
+#include <gtest/gtest.h>
+
 namespace atp {
 namespace {
 
diff --git a/tests/test_term_bank.cc b/tests/test_term_bank.cc
index 63acc34..3ea15ac 100644
--- a/tests/test_term_bank.cc
+++ b/tests/test_term_bank.cc
@@ -16,8 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-#include <gtest/gtest.h>
-
 #include "atp/core/clause.h"
 #include "atp/core/clause_store.h"
 #include "atp/core/literal.h"
@@ -26,6 +24,8 @@
 #include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 
+#include <gtest/gtest.h>
+
 namespace atp {
 namespace {
 
diff --git a/tests/test_unification.cc b/tests/test_unification.cc
index 3ee6f00..516058a 100644
--- a/tests/test_unification.cc
+++ b/tests/test_unification.cc
@@ -16,14 +16,14 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-#include <gtest/gtest.h>
-
 #include "atp/core/symbol_table.h"
 #include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 #include "atp/infer/substitution.h"
 #include "atp/infer/unification.h"
 
+#include <gtest/gtest.h>
+
 namespace atp {
 namespace {
 
@@ -348,8 +348,7 @@ TEST_F(UnificationTest, UnifyThenApply) {
     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