Function symmetric_resolution_closure 

pub fn symmetric_resolution_closure(
    cover: &Cover,
    generators: &[CubeSym],
    max_rounds: usize,
    max_reps: usize,
) -> (usize, bool)

Symmetric resolution closure on orbit representatives: resolve each representative against every image in another representative’s orbit. Since resolution commutes with symmetry — σ(resolve(c,d)) = resolve(σc,σd) — this captures every derivable rule up to symmetry without building the raw exponential closure. Returns the saturated count of orbit-types and whether the empty clause (a refutation) was derived, bounded by max_rounds and a max_reps size guard.

Measured limit (honest): this refutes PHP(3) at 12 orbit-types but does not scale — at PHP(4) the symmetric closure already explodes past tens of thousands of types. Even quotiented by symmetry, the full resolution closure is the wrong abstraction; the max_reps guard makes it fail safe rather than run away. The scalable path is pigeonhole_abstract_refutation — lift to the rule-type level and apply the counting invariant, not the closure.