pub fn certified_unsat_lex( num_vars: usize, formula: &[Vec<Lit>], generators: &[Perm], ) -> CertifiedRefutation