Function resolution_width_closure 

pub fn resolution_width_closure(
    clauses: &[Vec<Lit>],
    w: usize,
    convention: WidthConvention,
) -> BTreeSet<MaskClause>

The width-w resolution closure — the least fixpoint of pairwise resolution over the admissible axioms, keeping every resolvent of width ≤ w. This set contains every clause any width-w resolution derivation (under the convention) can produce, so it decides width-w refutability ((0,0) present ⟺ refutable) and, when the empty clause is absent, the set itself is the re-checkable lower-bound certificate (check_res_width_lower_bound).