nx_avatar_split.nx

nx_avatar_split.nx -- AVATAR-style clause splitting. Per Vampire-displacement roadmap Phase 2. AVATAR (Voronkov 2014) splits multi-component clauses into independent sub-clauses; full AVATAR uses a SAT solver to coordinate which split combinations to explore. This commit ships the SPLIT-ONLY primitive (trivial AVATAR). For each multi-component input clause, emit one output clause per component containing only that component's literals. Single- component clauses pass through unchanged. Sound when split components are ground or when each split's variables don't escape into the SAT-side coordination -- which is always the case here because we're splitting variable-disjoint components. The components don't share variables by construction (that's what "component" means), so each can be saturated independently and any UNSAT in any sub-clause is UNSAT for the whole clause set. API: nx_avatar_split_clause(c, out, cap) -> n_emitted nx_avatar_split_all(in, n_in, out, cap) -> n_emitted