nx_fmb.nx

nx_fmb.nx -- Finite Model Building. Per Vampire Trophy Cabinet (https://github.com/vprover/vampire/wiki/Trophy-Cabinet): "Our success [in the FNT division] is supported heavily by our implementation of finite model building." FMB is the explicitly-named technique Vampire credits with its Find-Non-Theorems wins. Shipping it closes the BLOCKED_ON_FMB axis from the substrate's honest CASC verdict. Algorithm (MACE-style, simplified): For each domain size N = 1, 2, 3, ...: 1. Ground every clause over a domain of N constants {d_1, d_2, ..., d_N}. Every variable in every clause is instantiated as each domain element in turn (one variable -> N copies of the clause; two variables -> N^2 copies; etc.). 2. Convert the ground clause set into a propositional SAT problem. 3. Run the SAT solver. If SAT, the original problem has a finite model of size N -- emit MODEL_FOUND verdict. If UNSAT, try N+1. 4. If no model found within max_size, return UNKNOWN. Verdicts: NX_FMB_MODEL_FOUND -- problem has a finite model (so the negated conjecture is satisfiable; original was NOT a theorem) -- CounterModel found NX_FMB_NO_MODEL -- search ran up to max_size without finding NX_FMB_ERROR -- bad input / capacity exceeded This is the basic CounterSatisfiable detector. Real Vampire FMB uses CSP-style constraints + sort inference + sym break; this MVP uses naive grounding + DPLL on the SAT side. Sufficient for FNT-easy problems. Bits-up nx_int; uses existing nx_sat_solver DPLL backend.