nx_tptp_formula.nx

nx_tptp_formula.nx -- TPTP CNF formula body parser. Per Vampire-displacement roadmap Phase 1.6: closes the BLOCKED axis from the CASC bench harness. Reads a TPTP CNF formula body and emits a *Clause ready for the saturation loop. Grammar handled (TPTP CNF subset): clause ::= [ "(" ] literal { "|" literal } [ ")" ] literal ::= [ "~" ] atom atom ::= predicate-application | term "=" term (equality) | term "!=" term (inequality) term ::= delegated to nx_tptp_term Equality is mapped to a caller-supplied eq_sym (a normal binary predicate sym_id reserved for "="). Inequality literal flips the sign of the surrounding literal. Bits-up parsing. Returns null on parse failure (the smoke test covers both the success and failure paths). FOF (quantifiers, &, =>, <=>, etc.) is Phase 2 -- CNF alone is what the CASC FOF division accepts after a TPTP-tooled CNF transformation, and is what TPTP-Easy provides directly.