17 files changed, 1579 insertions, 0 deletions
diff --git a/proofsearch/src/core/clause_store.cc b/proofsearch/src/core/clause_store.cc
new file mode 100644
index 0000000..f8ee73d
--- /dev/null
+++ b/proofsearch/src/core/clause_store.cc
@@ -0,0 +1,59 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/clause_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;
+    clauses_.push_back(std::move(clause));
+    return new_id;
+}
+
+const Clause& ClauseStore::getClause(ClauseId id) const {
+    assert(id < clauses_.size() && "ClauseId out of bounds!");
+    return clauses_[id];
+}
+
+Clause& ClauseStore::getMutableClause(ClauseId id) {
+    assert(id < clauses_.size() && "ClauseId out of bounds!");
+    return clauses_[id];
+}
+
+size_t ClauseStore::size() const {
+    return clauses_.size();
+}
+
+void ClauseStore::forEach(const std::function<void(const Clause&)>& visitor) const {
+    for (const auto& clause : clauses_) {
+        // TODO: Tombstone mechanism
+        visitor(clause);
+    }
+}
+
+}  // namespace atp
diff --git a/proofsearch/src/core/symbol_table.cc b/proofsearch/src/core/symbol_table.cc
new file mode 100644
index 0000000..b707132
--- /dev/null
+++ b/proofsearch/src/core/symbol_table.cc
@@ -0,0 +1,65 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/symbol_table.h"
+
+#include "atp/core/types.h"
+
+#include <cstddef>
+#include <cstdint>
+#include <stdexcept>
+#include <string>
+#include <string_view>
+
+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 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(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_;
+}
+
+const SymbolInfo& SymbolTable::getInfo(SymbolId id) const {
+    return infos_[id];
+}
+
+bool SymbolTable::isVariable(SymbolId id) const {
+    return infos_[id].kind_ == SymbolKind::kVariable;
+}
+
+size_t SymbolTable::size() const {
+    return infos_.size();
+}
+
+}  // namespace atp
diff --git a/proofsearch/src/core/term_bank.cc b/proofsearch/src/core/term_bank.cc
new file mode 100644
index 0000000..0dc166f
--- /dev/null
+++ b/proofsearch/src/core/term_bank.cc
@@ -0,0 +1,63 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/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()}};
+    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_ = key.args_};
+    terms_.push_back(std::move(new_term));
+    term_to_id_.emplace(std::move(key), new_id);
+    return new_id;
+}
+
+TermId TermBank::makeVar(SymbolId var_symbol) {
+    return makeTerm(var_symbol, {});
+}
+
+const Term& TermBank::getTerm(TermId id) const {
+    assert(id < terms_.size() && "TermId out of bounds!");
+    return terms_[id];
+}
+
+bool TermBank::isVariable(TermId id) const {
+    assert(id < terms_.size() && "TermId out of bounds!");
+    return symbols_->isVariable(terms_[id].symbol_id_);
+}
+
+size_t TermBank::size() const {
+    return terms_.size();
+}
+
+}  // namespace atp
diff --git a/proofsearch/src/frontend/tptp_parser.cc b/proofsearch/src/frontend/tptp_parser.cc
new file mode 100644
index 0000000..10190b8
--- /dev/null
+++ b/proofsearch/src/frontend/tptp_parser.cc
@@ -0,0 +1,325 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/frontend/tptp_parser.h"
+
+#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") {
+        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 : 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_{};
+};
+
+class TptpLexer {
+  public:
+    explicit TptpLexer(std::string_view input) : source_(input) {}
+
+    Token nextToken() {
+        skipWhitespaceAndComments();
+
+        if (pos_ >= source_.length()) {
+            return {.type_ = TokenType::kEOF, .value_ = "", .line_ = line_, .column_ = column_};
+        }
+
+        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)) != 0) || c == '_') {
+            while (
+                pos_ < source_.size() &&
+                ((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_};
+        }
+
+        advanceChar();
+        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_};
+        }
+    }
+
+  private:
+    std::string_view source_;
+    size_t pos_ = 0;
+    size_t line_ = 1;
+    size_t column_ = 1;
+
+    void advanceChar() {
+        if (pos_ < source_.size()) {
+            if (source_[pos_] == '\n') {
+                line_++;
+                column_ = 1;
+            } else {
+                column_++;
+            }
+            pos_++;
+        }
+    }
+
+    void skipWhitespaceAndComments() {
+        while (pos_ < source_.size()) {
+            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') {
+                    advanceChar();
+                }
+            } else {
+                break;
+            }
+        }
+    }
+};
+
+class TptpParser {
+  public:
+    explicit TptpParser(std::string_view input, TermBank& bank, SymbolTable& symbols)
+        : lexer_(input), bank_(bank), symbols_(symbols) {
+        advance();
+    }
+
+    void parseProblem(ParsedProblem& problem) {
+        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.name_ = std::string(current_token_.value_);
+                expect(TokenType::kWord);
+                expect(TokenType::kComma);
+
+                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) {
+                    advance();
+                    clause.literals_.push_back(parseLiteral());
+                }
+                af.clauses_.push_back(std::move(clause));
+
+                expect(TokenType::kRParen);
+                expect(TokenType::kDot);
+                problem.formulas_.push_back(std::move(af));
+
+                variable_cache_.clear();
+            } else if (current_token_.value_ == "fof") {
+                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_) + "'");
+            }
+        }
+    }
+
+  private:
+    TptpLexer lexer_;
+    TermBank& bank_;
+    SymbolTable& symbols_;
+    Token current_token_{};
+    std::vector<Token> tokens_;
+    std::unordered_map<std::string_view, SymbolId> variable_cache_;
+
+    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_) +
+                                     "'");
+        }
+        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_) +
+                                     "'");
+        }
+
+        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) {
+            // Check cache first — same variable name in one clause → same TermId
+            auto it = variable_cache_.find(name);
+            if (it != variable_cache_.end()) {
+                return it->second;
+            }
+            SymbolId const sym = symbols_.intern(name, SymbolKind::kVariable);
+            TermId const var_id = bank_.makeVar(sym);
+            variable_cache_[name] = var_id;
+            return var_id;
+        }
+
+        // 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) {
+                args.push_back(parseTerm());
+                while (current_token_.type_ == TokenType::kComma) {
+                    advance();
+                    args.push_back(parseTerm());
+                }
+            }
+            expect(TokenType::kRParen);
+            const SymbolId sym = symbols_.intern(name, SymbolKind::kFunction,
+                                                 static_cast<uint16_t>(args.size()));
+            return bank_.makeTerm(sym, args);
+        }
+
+        // Constant: no parentheses (e.g., a, b, h0, s0)
+        const SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0);
+        return bank_.makeTerm(sym, {});
+    }
+
+    Literal parseLiteral() {
+        bool is_positive = true;
+        if (current_token_.type_ == TokenType::kNot) {
+            is_positive = false;
+            advance();
+        }
+        TermId const term = parseTerm();
+        return Literal{.atom_ = term, .is_positive_ = is_positive};
+    }
+};
+
+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) {
+    std::ifstream file(filename, std::ios::binary);
+    if (!file.is_open()) {
+        throw std::runtime_error("Failed to open file: " + filename);
+    }
+    std::string const content((std::istreambuf_iterator<char>(file)), std::istreambuf_iterator<char>());
+    ParsedProblem problem = parseTptpString(content, bank, symbols);
+    problem.source_file_ = filename;
+    return problem;
+}
+
+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;
+                final_clauses.push_back(std::move(clause));
+            }
+        }
+    }
+    return final_clauses;
+}
+
+}  // namespace atp
diff --git a/proofsearch/src/index/discrim_tree.cc b/proofsearch/src/index/discrim_tree.cc
new file mode 100644
index 0000000..17c63f8
--- /dev/null
+++ b/proofsearch/src/index/discrim_tree.cc
@@ -0,0 +1,17 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
diff --git a/proofsearch/src/infer/resolution.cc b/proofsearch/src/infer/resolution.cc
new file mode 100644
index 0000000..5fb0d4a
--- /dev/null
+++ b/proofsearch/src/infer/resolution.cc
@@ -0,0 +1,176 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/infer/resolution.h"
+
+#include "atp/core/clause.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#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 {
+
+namespace {
+
+/// Recursively collect all variable TermIds appearing in a term.
+void collectVariables(TermId term, const TermBank& bank, std::unordered_map<TermId, bool>& seen) {
+    if (bank.isVariable(term)) {
+        seen[term] = true;
+        return;
+    }
+    // Copy args to avoid dangling ref (bank is const here, but be safe)
+    const Term& t = bank.getTerm(term);
+    for (TermId const arg : t.args_) {
+        collectVariables(arg, bank, seen);
+    }
+}
+
+}  // namespace
+
+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);
+    }
+
+    if (var_set.empty()) {
+        return c;  // Ground clause — nothing to rename
+    }
+
+    // 2. Create fresh variables and build a substitution
+    Substitution rename_subst;
+    for (auto& [old_var_id, _] : var_set) {
+        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 const new_atom = applySubstitution(rename_subst, lit.atom_, bank);
+        renamed.literals_.push_back({.atom_ = new_atom, .is_positive_ = lit.is_positive_});
+    }
+    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) {
+    // Must have opposite polarity
+    if (c1.literals_[lit_idx1].is_positive_ == c2.literals_[lit_idx2].is_positive_) {
+        return std::nullopt;
+    }
+
+    // Rename c2's variables to avoid clashes with c1
+    // Use a static counter — safe for single-threaded prover
+    static uint32_t var_counter = 0;
+    auto& symbols = bank.mutableSymbols();
+    Clause c2r = renameVariables(c2, bank, symbols, var_counter);
+
+    // Unify the complementary atoms
+    Substitution subst;
+    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_;
+
+    for (size_t i = 0; i < c1.literals_.size(); ++i) {
+        if (i != lit_idx1) {
+            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) {
+        if (i != lit_idx2) {
+            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;
+}
+
+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_) {
+                if (auto r = resolve(bank, c1, i, c2, j, uconfig)) {
+                    results.push_back(std::move(*r));
+                }
+            }
+        }
+    }
+    return results;
+}
+
+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_) {
+                continue;  // Must have same polarity
+            }
+            Substitution subst;
+            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) {
+                if (k != j) {
+                    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));
+        }
+    }
+    return results;
+}
+
+}  // namespace atp
diff --git a/proofsearch/src/infer/substitution.cc b/proofsearch/src/infer/substitution.cc
new file mode 100644
index 0000000..584008b
--- /dev/null
+++ b/proofsearch/src/infer/substitution.cc
@@ -0,0 +1,119 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/infer/substitution.h"
+
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+
+#include <algorithm>
+#include <vector>
+
+namespace atp {
+
+bool Substitution::bind(TermId var, TermId term) {
+    auto [it, inserted] = bindings_.emplace(var, term);
+    if (!inserted) {
+        // Already bound — succeed only if bound to the same term
+        return it->second == term;
+    }
+    return true;
+}
+
+TermId Substitution::lookup(TermId var) const {
+    auto it = bindings_.find(var);
+    if (it != bindings_.end()) {
+        return it->second;
+    }
+    return kInvalidId;
+}
+
+TermId Substitution::resolve(TermId id, const TermBank& bank) const {
+    // Walk the chain: X → Y → Z → f(a)
+    // Stop when we hit a non-variable or an unbound variable.
+    while (bank.isVariable(id)) {
+        auto it = bindings_.find(id);
+        if (it == bindings_.end()) {
+            break;  // Unbound variable — stop here
+        }
+        id = it->second;
+    }
+    return id;
+}
+
+TermId Substitution::apply(TermId term, TermBank& bank) const {
+    // First, resolve through variable chain
+    term = resolve(term, bank);
+
+    if (bank.isVariable(term)) {
+        // Free variable (unbound) — leave as-is
+        return term;
+    }
+
+    // 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 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
+        return term;
+    }
+
+    // Recursively apply to all arguments
+    std::vector<TermId> new_args;
+    new_args.reserve(old_args.size());
+    bool changed = false;
+    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;
+        }
+    }
+
+    if (!changed) {
+        return term;
+    }
+
+    return bank.makeTerm(sym, new_args);
+}
+
+bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const {
+    term = resolve(term, bank);
+
+    if (var == term) {
+        return true;
+    }
+
+    if (bank.isVariable(term)) {
+        return false;  // Different unbound variable
+    }
+
+    const Term& t = bank.getTerm(term);
+    return std::any_of(t.args_.begin(), t.args_.end(),
+                       [&](TermId arg) { return occursIn(var, arg, bank); });
+}
+
+void Substitution::clear() {
+    bindings_.clear();
+}
+
+}  // namespace atp
+\ No newline at end of file
diff --git a/proofsearch/src/infer/unification.cc b/proofsearch/src/infer/unification.cc
new file mode 100644
index 0000000..c42bf67
--- /dev/null
+++ b/proofsearch/src/infer/unification.cc
@@ -0,0 +1,92 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/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,
+           const UnificationConfig& config) {
+    t1 = subst.resolve(t1, bank);
+    t2 = subst.resolve(t2, bank);
+
+    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(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);
+
+    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)) {
+            return false;
+        }
+    }
+
+    return true;
+}
+
+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 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 const 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/proofsearch/src/main.cc b/proofsearch/src/main.cc
new file mode 100644
index 0000000..c683d39
--- /dev/null
+++ b/proofsearch/src/main.cc
@@ -0,0 +1,99 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+/// @file main.cc
+/// @brief ATP Engine command-line entry point.
+
+#include "atp/core/clause_store.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/frontend/tptp_parser.h"
+#include "atp/proof/proof_trace.h"
+#include "atp/search/prover.h"
+
+#include <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"
+              << "This program comes with ABSOLUTELY NO WARRANTY.\n"
+              << "This is free software, and you are welcome to redistribute it\n"
+              << "under certain conditions; see LICENSE for details.\n\n";
+
+    if (argc < 2) {
+        std::cerr << "Usage: atp <file.p>\n";
+        return EXIT_FAILURE;
+    }
+
+    const std::string filepath = argv[1];
+
+    try {
+        // 1. Initialize core modules
+        atp::SymbolTable symbols;
+        atp::TermBank bank(symbols);
+        atp::ClauseStore store;
+
+        // 2. Parse TPTP input
+        auto problem = atp::parseTptpFile(filepath, bank, symbols);
+
+        std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << filepath
+                  << "\n";
+
+        // 3. Prepare clauses for proving
+        auto clauses = atp::prepareForProving(problem, bank, symbols);
+
+        std::cerr << "% " << clauses.size() << " clauses prepared for proving\n";
+
+        // 4. Run the prover
+        atp::Prover prover(bank, store);
+        prover.addClauses(std::move(clauses));
+        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";
+
+                // 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 << atp::formatProof(proof, store, bank);
+                    std::cout << "% SZS output end Proof for " << filepath << "\n";
+                }
+                break;
+            }
+            case atp::ProverResult::kSaturation:
+                std::cout << "% SZS status Satisfiable for " << filepath << "\n";
+                break;
+            case atp::ProverResult::kTimeout:
+                std::cout << "% SZS status Timeout for " << filepath << "\n";
+                break;
+        }
+
+    } catch (const std::exception& e) {
+        std::cerr << "% Error: " << e.what() << "\n";
+        return EXIT_FAILURE;
+    }
+
+    return EXIT_SUCCESS;
+}
diff --git a/proofsearch/src/normalize/clausifier.cc b/proofsearch/src/normalize/clausifier.cc
new file mode 100644
index 0000000..17c63f8
--- /dev/null
+++ b/proofsearch/src/normalize/clausifier.cc
@@ -0,0 +1,17 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
diff --git a/proofsearch/src/proof/proof_trace.cc b/proofsearch/src/proof/proof_trace.cc
new file mode 100644
index 0000000..5fa4b04
--- /dev/null
+++ b/proofsearch/src/proof/proof_trace.cc
@@ -0,0 +1,249 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/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 <cstddef>
+#include <stack>
+#include <string>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+namespace atp {
+
+// extractProof
+// DFS from empty clause back to axioms, collect all participating clauses,
+// then reverse for topological order (axioms first).
+
+std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_clause_id) {
+    std::vector<ProofStep> steps;
+    std::unordered_set<ClauseId> visited;
+    std::stack<ClauseId> worklist;
+    worklist.push(empty_clause_id);
+
+    while (!worklist.empty()) {
+        const ClauseId cid = worklist.top();
+        worklist.pop();
+
+        if (cid == kInvalidId) {
+            continue;
+        }
+        if (visited.contains(cid)) {
+            continue;
+        }
+        visited.insert(cid);
+
+        const Clause& c = store.getClause(cid);
+        steps.push_back({
+            .clause_id_ = cid,
+            .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_);
+    }
+
+    // Reverse: axioms (leaves) first → empty clause (root) last
+    std::ranges::reverse(steps);
+    return steps;
+}
+
+// termToString
+
+std::string termToString(TermId id, const TermBank& bank) {
+    const Term& t = bank.getTerm(id);
+    std::string name(bank.symbols().getName(t.symbol_id_));
+
+    if (t.args_.empty()) {
+        return name;
+    }
+
+    std::string result = name + "(";
+    for (size_t i = 0; i < t.args_.size(); ++i) {
+        if (i > 0) {
+            result += ",";
+        }
+        result += termToString(t.args_[i], bank);
+    }
+    result += ")";
+    return result;
+}
+
+// Pretty variable names
+
+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) {
+    constexpr size_t kBaseCount = 6;
+    const size_t base_index = index % kBaseCount;
+    const char base = [&]() {
+        switch (base_index) {
+            case 0:
+                return 'X';
+            case 1:
+                return 'Y';
+            case 2:
+                return 'Z';
+            case 3:
+                return 'W';
+            case 4:
+                return 'V';
+            case 5:
+                return 'U';
+            default:
+                return 'X';
+        }
+    }();
+
+    const size_t suffix = index / kBaseCount;
+    if (suffix == 0) {
+        return std::string{base};
+    }
+    return std::string{base} + std::to_string(suffix);
+}
+
+/// Pretty-print a term, renaming variables to readable names.
+/// `var_map` is built incrementally: each new variable gets the next name.
+std::string termToPretty(TermId id, const TermBank& bank,
+                         std::unordered_map<TermId, std::string>& var_map) {
+    if (bank.isVariable(id)) {
+        auto it = var_map.find(id);
+        if (it != var_map.end()) {
+            return it->second;
+        }
+        const std::string name = prettyVarName(var_map.size());
+        var_map[id] = name;
+        return name;
+    }
+
+    const Term& t = bank.getTerm(id);
+    std::string name(bank.symbols().getName(t.symbol_id_));
+
+    if (t.args_.empty()) {
+        return name;
+    }
+
+    std::string result = name + "(";
+    for (size_t i = 0; i < t.args_.size(); ++i) {
+        if (i > 0) {
+            result += ",";
+        }
+        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
+
+std::string clauseToString(const Clause& clause, const TermBank& bank) {
+    if (clause.isEmpty()) {
+        return "□";
+    }
+
+    // Per-clause variable renaming: _R109 → X, _R286 → Y, etc.
+    std::unordered_map<TermId, std::string> var_map;
+
+    std::string result;
+    for (size_t i = 0; i < clause.literals_.size(); ++i) {
+        if (i > 0) {
+            result += " ∨ ";
+        }
+        if (!clause.literals_[i].is_positive_) {
+            result += "¬";
+        }
+        result += termToPretty(clause.literals_[i].atom_, bank, var_map);
+    }
+    return result;
+}
+
+// formatProof
+
+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) {
+        id_to_step[proof[i].clause_id_] = i + 1;  // 1-based
+    }
+
+    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);
+        }
+        // Fallback: shouldn't happen in a valid proof
+        return "?" + std::to_string(cid);
+    };
+
+    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_);
+
+        result += std::to_string(i + 1) + ". ";
+        result += "[" + ruleToString(step.rule_) + "] ";
+        result += clauseToString(c, bank);
+
+        // Show parents for derived clauses
+        if (step.parent1_ != kInvalidId) {
+            result += "  [" + local_name(step.parent1_);
+            if (step.parent2_ != kInvalidId) {
+                result += ", " + local_name(step.parent2_);
+            }
+            result += "]";
+        }
+
+        result += "\n";
+    }
+    return result;
+}
+
+}  // namespace atp
diff --git a/proofsearch/src/rewrite/ordering.cc b/proofsearch/src/rewrite/ordering.cc
new file mode 100644
index 0000000..17c63f8
--- /dev/null
+++ b/proofsearch/src/rewrite/ordering.cc
@@ -0,0 +1,17 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
diff --git a/proofsearch/src/rewrite/paramodulation.cc b/proofsearch/src/rewrite/paramodulation.cc
new file mode 100644
index 0000000..17c63f8
--- /dev/null
+++ b/proofsearch/src/rewrite/paramodulation.cc
@@ -0,0 +1,17 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
diff --git a/proofsearch/src/search/prover.cc b/proofsearch/src/search/prover.cc
new file mode 100644
index 0000000..f3f8bb0
--- /dev/null
+++ b/proofsearch/src/search/prover.cc
@@ -0,0 +1,167 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/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"
+#include "atp/simplify/subsumption.h"
+#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_) {}
+
+void Prover::addClauses(std::vector<Clause> clauses) {
+    for (auto& clause : clauses) {
+        clause.depth_ = 0;
+        ClauseId const id = store_.addClause(clause);
+        unprocessed_.push(store_.getClause(id));
+    }
+}
+
+bool Prover::hitResourceLimit(size_t iterations) const {
+    return iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_;
+}
+
+Clause Prover::popGivenClause() {
+    Clause given = unprocessed_.top();
+    unprocessed_.pop();
+    return given;
+}
+
+bool Prover::isForwardSubsumedByProcessed(const Clause& clause) const {
+    return std::ranges::any_of(processed_,
+                               [&](ClauseId pid) { return subsumes(store_.getClause(pid), clause); });
+}
+
+bool Prover::shouldSkipGiven(const Clause& given) const {
+    return isTautology(given) || isForwardSubsumedByProcessed(given);
+}
+
+void Prover::applyBackwardSubsumption(const Clause& given) {
+    std::erase_if(processed_, [&](ClauseId pid) { return subsumes(given, store_.getClause(pid)); });
+}
+
+std::vector<Clause> Prover::generateNewClauses(const Clause& given) const {
+    std::vector<Clause> new_clauses;
+    const UnificationConfig uconfig{.enable_occurs_check_ = config_.enable_occurs_check_};
+
+    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);
+
+        for (auto& r : resolvents1) {
+            new_clauses.push_back(std::move(r));
+        }
+        for (auto& r : resolvents2) {
+            new_clauses.push_back(std::move(r));
+        }
+    }
+
+    auto factors = factor(bank_, given, uconfig);
+    for (auto& f : factors) {
+        new_clauses.push_back(std::move(f));
+    }
+
+    return new_clauses;
+}
+
+uint16_t Prover::computeDepth(const Clause& clause) const {
+    uint32_t const d1 = (clause.parent1_ != kInvalidId) ? store_.getClause(clause.parent1_).depth_ : 0;
+    uint32_t const d2 = (clause.parent2_ != kInvalidId) ? store_.getClause(clause.parent2_).depth_ : 0;
+    return static_cast<uint16_t>(std::max(d1, d2) + 1);
+}
+
+std::optional<ClauseId> Prover::processNewClauses(std::vector<Clause> new_clauses) {
+    for (auto& nc : new_clauses) {
+        if (nc.isEmpty()) {
+            return store_.addClause(std::move(nc));
+        }
+
+        if (isTautology(nc)) {
+            continue;
+        }
+
+        nc.depth_ = computeDepth(nc);
+
+        ClauseId const nid = store_.addClause(nc);
+        const Clause& stored_nc = store_.getClause(nid);
+        if (isForwardSubsumedByProcessed(stored_nc)) {
+            continue;
+        }
+
+        unprocessed_.push(stored_nc);
+    }
+
+    return std::nullopt;
+}
+
+ProverResult Prover::prove() {
+    size_t iterations = 0;
+
+    while (!unprocessed_.empty()) {
+        if (hitResourceLimit(iterations)) {
+            return ProverResult::kTimeout;
+        }
+        ++iterations;
+
+        Clause given = popGivenClause();
+
+        if (given.isEmpty()) {
+            empty_clause_id_ = given.id_;
+            return ProverResult::kTheorem;
+        }
+
+        if (shouldSkipGiven(given)) {
+            continue;
+        }
+
+        applyBackwardSubsumption(given);
+        std::vector<Clause> new_clauses = generateNewClauses(given);
+        processed_.push_back(given.id_);
+
+        const std::optional<ClauseId> derived_empty = processNewClauses(std::move(new_clauses));
+        if (derived_empty.has_value()) {
+            empty_clause_id_ = derived_empty;
+            return ProverResult::kTheorem;
+        }
+    }
+
+    return ProverResult::kSaturation;
+}
+
+std::optional<ClauseId> Prover::getEmptyClauseId() const {
+    return empty_clause_id_;
+}
+
+}  // namespace atp
+\ No newline at end of file
diff --git a/proofsearch/src/simplify/subsumption.cc b/proofsearch/src/simplify/subsumption.cc
new file mode 100644
index 0000000..0038ad1
--- /dev/null
+++ b/proofsearch/src/simplify/subsumption.cc
@@ -0,0 +1,43 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/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_) {
+        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;
+        }
+    }
+    return true;
+}
+}  // namespace atp
diff --git a/proofsearch/src/simplify/tautology.cc b/proofsearch/src/simplify/tautology.cc
new file mode 100644
index 0000000..e35d874
--- /dev/null
+++ b/proofsearch/src/simplify/tautology.cc
@@ -0,0 +1,37 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/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_) {
+                return true;
+            }
+        }
+    }
+    return false;
+}
+}  // namespace atp
+\ No newline at end of file
diff --git a/proofsearch/src/strategy/problem_analyzer.cc b/proofsearch/src/strategy/problem_analyzer.cc
new file mode 100644
index 0000000..17c63f8
--- /dev/null
+++ b/proofsearch/src/strategy/problem_analyzer.cc
@@ -0,0 +1,17 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */