nx_pre_sat.nx

nx_pre_sat.nx -- pre-saturation simplification of input clause set. Per Vampire-displacement roadmap Phase 2. Before the saturation loop starts, run a pass that drops tautologies + forward-subsumed clauses from the input. Reduces the initial working set, which compounds with the discount loop's per-step pruning. Pure composition over existing primitives: - nx_is_tautology (nx_tautology.nx) - nx_subsumes (nx_subsumption.nx) Algorithm (linear-quadratic in n_input): For each input clause C in order: 1. If C is a tautology -> drop. 2. If any already-kept clause subsumes C -> drop. 3. Otherwise: backward-subsume the kept set against C (drop any older C' that the new C subsumes), then add C. This is a one-shot variant of the discount loop's per-pick filter, applied to the input batch only -- it doesn't re-saturate.