pub fn refutation(
num_vars: usize,
original: &[Vec<Lit>],
learned: &[Vec<Lit>],
) -> Option<Lrat>Expand description
The trimmed LRAT refutation of original that learned (each clause RUP from the formula and the clauses before
it) carries to the empty clause, or None when the empty clause is not RUP from them all or a learned clause the
refutation needs is not RUP in its place: the derivation of the empty clause, after the learned clauses.