nx_subsumption.nx

nx_subsumption.nx -- forward subsumption for clause sets. Per Vampire-displacement roadmap Phase 1 step 2: clause C subsumes clause D iff there exists a substitution sigma such that for every literal Lc in C, there is a literal Ld in D with the same polarity AND Lc[sigma] = Ld. When C subsumes D, D is redundant and can be dropped from the passive set -- this is the single biggest pruner in saturation provers. Algorithm: backtracking match. For each literal of C in order, try every same-polarity literal of D as a match candidate. Snapshot substitution length before each attempt; on failure, roll back by resetting s.n. Subst bindings are append-only (see nx_unify), so truncating restores the prior state exactly. One-way matching (nx_match) is required, not full unification -- only C's variables get bound; D is treated as fixed. Bits-up nx_int, Result-typed errors via underlying primitives, scale-agnostic via nx_tier.