nx_hyperres.nx

nx_hyperres.nx -- N-electron hyperresolution. Per Vampire-displacement roadmap Phase 2. Generalization of binary resolution: combine one nucleus clause with N "electron" clauses in a single inference step. Each electron contributes one positive literal that resolves with one chosen negative literal of the nucleus, all under a composed unifier. Robinson + Wos 1965 standard formulation: Nucleus: C ∨ ~a_1 ∨ ~a_2 ∨ ... ∨ ~a_n Electrons: E_i ∨ b_i (one per i, b_i positive) Unifier: σ = compose(unify(a_1,b_1), unify(a_2,b_2), ...) Derive: (C ∨ E_1 ∨ E_2 ∨ ... ∨ E_n)σ where C is the residual non-consumed part of the nucleus and each E_i is the residual non-consumed part of electron i. API: caller picks the consumed literals by index. Each negative literal in nucleus targeted at neg_indices[i] is paired with the positive literal in electrons[i] at pos_indices[i]. Variable renaming across input clauses is the caller's responsibility (matches nx_resolve's contract). Bits-up nx_int. Result-typed for fallible API.