style: reformat codebase with consistent indentation

17 files changed, 186 insertions, 177 deletions

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/>.
  */
-
-