nx_inst_gen.nx

nx_inst_gen.nx -- instance generation (Inst-Gen). Per Vampire-displacement roadmap Phase 2. Korovin + Voronkov 2003 alternative to resolution: instead of resolving complementary literals away (producing a single resolvent), INSTANTIATE both clauses with the unifier (producing two more-specific clauses). The downstream SAT-coupled prover (iProver, Vampire+SAT) then works on ground instances to prove UNSAT. Inst-Gen excels at problems with large finite Herbrand universes where resolution blows up but ground reasoning succeeds. Standard formulation: C ∨ L D ∨ ¬L' σ = mgu(L, L') ---------------------- (C ∨ L)σ (D ∨ ¬L')σ Both resulting clauses keep their full literal sets -- σ just makes them more specific. No literals are removed. This is the crucial difference from resolution. API: nx_inst_gen(c1, i, c2, j, c1_out, c2_out) -> *NxResult Caller allocates c1_out + c2_out; primitive populates both with the σ-applied versions.