Function check_pr_refutation 

pub fn check_pr_refutation(
    num_vars: usize,
    original: &[Vec<Lit>],
    steps: &[ProofStep],
) -> bool

Verify a refutation made of ProofSteps over original. Each step’s added clause must check (RUP or PR) against the database built so far; then the empty clause must be RUP. Returns false if any step fails to check — a bogus or unsound proof is rejected.