From 7408740374f46b24edd53d421dbc270d2fca1293 Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Sat, 4 Apr 2026 04:56:51 +0800
Subject: feat: implement command-line interface and add end-to-end
 propositional logic test suite

---
 src/proof/proof_trace.cc | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/proof/proof_trace.cc')

diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc
index b1b4343..fff54a3 100644
--- a/src/proof/proof_trace.cc
+++ b/src/proof/proof_trace.cc
@@ -30,7 +30,7 @@
 
 namespace atp {
 
-// ─── extractProof ────────────────────────────────────────────────────────────
+// ─── extractProof 
 // DFS from empty clause back to axioms, collect all participating clauses,
 // then reverse for topological order (axioms first).
 
@@ -71,7 +71,7 @@ std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_cla
     return steps;
 }
 
-// ─── termToString ────────────────────────────────────────────────────────────
+// ─── termToString 
 
 std::string termToString(TermId id, const TermBank& bank) {
     const Term& t = bank.getTerm(id);
@@ -92,7 +92,7 @@ std::string termToString(TermId id, const TermBank& bank) {
     return result;
 }
 
-// ─── clauseToString ──────────────────────────────────────────────────────────
+// ─── clauseToString 
 
 std::string clauseToString(const Clause& clause, const TermBank& bank) {
     if (clause.isEmpty()) {
@@ -112,7 +112,7 @@ std::string clauseToString(const Clause& clause, const TermBank& bank) {
     return result;
 }
 
-// ─── ruleToString ────────────────────────────────────────────────────────────
+// ─── ruleToString 
 
 static std::string ruleToString(InferenceRule rule) {
     switch (rule) {
@@ -123,7 +123,7 @@ static std::string ruleToString(InferenceRule rule) {
     }
 }
 
-// ─── formatProof ─────────────────────────────────────────────────────────────
+// ─── formatProof 
 
 std::string formatProof(const std::vector<ProofStep>& proof,
                         const ClauseStore& store, const TermBank& bank) {
-- 
cgit v1.2.3