Function is_refutation 

pub fn is_refutation(
    clauses: &[HornClause],
    num_vars: usize,
    refutation: &[usize],
) -> bool

Re-check a refutation: replaying only the listed clauses by forward chaining forces some goal clause’s body fully true (a contradiction). A solver-free certificate of unsatisfiability.