Function emit_modp_drat 

pub fn emit_modp_drat(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> Option<Vec<Vec<Lit>>>

The CNF→GF(p) bridge: compile a modular (mod-p / counting) UNSAT verdict into a strict DRAT proof. We recover the one-hot modular system from clauses, solve it over the prime field, and — on UNSAT — resolution-refute the sub-CNF confined to the one-hot bits of the involved groups. That sub-CNF (the forbidden-tuple gadgets of the combination’s equations together with their groups’ at-least-one/at-most-one clauses) is unsatisfiable, so DP elimination over those Boolean variables yields the empty clause, every line RUP against the original CNF. None if the formula is not a recoverable mod-p encoding or its modular system is satisfiable.