Function plain_cdcl_refutation 

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

A plain CDCL refutation of clauses as RUP proof steps — always re-checkable. The certified fallback that guarantees solve_certified and sdcl_refute never emit an unchecked proof, and the universal source of a cake_lpr-checkable LRAT certificate for any UNSAT instance.