Function affine_p_refutation_drat 

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

The clausal DRAT certificate for a GF(p) affine refutation, or None if the formula’s mod-p core is not inconsistent (or the resolution expansion overruns its budget). Recovers the one-hot GF(p) system, finds the Σ multiplierᵢ·equationᵢ dependency whose left side cancels while the right does not (crate::modp::solve), and compiles it to RUP resolvent lemmas over the Boolean one-hot encoding through the crate::xor_drat bridge — drat-trim-checkable against the original CNF, the mod-p generalization of crate::affine::affine_refutation_drat.