Function is_pr 

pub fn is_pr(
    num_vars: usize,
    db: &[Vec<Lit>],
    clause: &[Lit],
    witness: &Witness,
) -> bool

Is clause propagation-redundant w.r.t. db under witness?