6 files changed, 22 insertions, 29 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