style: reformat codebase with consistent indentation

1 files changed, 45 insertions, 45 deletions

diff --git a/proofsearch/src/infer/unification.cc b/proofsearch/src/infer/unification.cc
index be8a025..66e1af6 100644
--- a/proofsearch/src/infer/unification.cc
+++ b/proofsearch/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