Function check_derivation 

pub fn check_derivation(
    num_vars: usize,
    original: &[Vec<Lit>],
    proof: &Lrat,
    claims: &[Vec<Lit>],
) -> bool

Whether proof derives every clause of claims from original: every step’s id exceeds the one before it (and the formula’s), every hint names a clause already present, every step’s hints replay, and each claim, its literals in any order, is the clause of a step or of the formula. Every literal must lie below num_vars.