Function check 

pub fn check(
    aig: &Aig,
    certificate: &Certificate,
    claims: &[(AigLit, AigLit)],
) -> bool

Whether certificate proves every claim: each lemma’s proof refutes its query in order, and each claimed pair is one literal, or two literals the lemmas join with matching phase.