nx_answer.nx

nx_answer.nx -- AnswerLiteral support for "find a witness" queries. Per Vampire-displacement roadmap Phase 2. When a conjecture has the shape ∃X. p(X) and we want to know WHICH X works (not just that some X exists), we attach a special $answer(X) literal to the negated conjecture clause. Saturation tracks the answer literal through every inference; when the proof closes (empty-clause-modulo- answer), the surviving $answer(witness) literal carries the X instantiation that closed the proof. Convention: the answer predicate symbol id is caller-supplied (no magic constant, same shape as eq_sym in nx_tautology / nx_tptp_load). Recommended: NX_ANS_BASE (700_000) -- distinct from user (1_000+), Tseitin (800_000+), Skolem (900_000+). API: nx_answer_attach(c, ans_sym, witness_var_id) -- adds $answer(X) literal nx_clause_is_answer_only(c, ans_sym) -- 1 iff c only has $answer(...) nx_clause_extract_answer(c, ans_sym) -- returns the witness term, null if none