nx_tautology.nx

nx_tautology.nx -- syntactic tautology detection on clauses. Per Vampire-displacement roadmap Phase 1 step 4. A clause is a tautology when its truth is forced regardless of interpretation; such clauses add nothing to the search space and are dropped before they enter the passive set. Two patterns recognised here: (a) Reflexive equality: + eq(t, t) for any term t. (b) Propositional pair: contains both +L and -L over identical atoms. Equality predicate symbol id is a parameter -- the caller (TPTP parser, kernel API) names whichever sym_id "=" was registered under. Avoids a magic constant baked into substrate. Sealed verdict {NX_TAUTOLOGY, NX_NOT_TAUTOLOGY}. This is the purely syntactic check; semantic tautology detection (E-resolution across equivalent atoms) is a Phase 2 extension.