Function check 

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

Whether proof refutes 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 (each unit under the step’s negation, the last a conflict), and a step derives the empty clause. Every literal must lie below num_vars.