Function find_pr_clause_unified 

pub fn find_pr_clause_unified(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    alpha: &[Lit],
    generators: &[Perm],
) -> Option<(Vec<Lit>, Witness)>

The unified PR-clause finder: the universal SDCL discovery (positive-reduct assignment witness) PLUS the scalable symmetry path (substitution witnesses from the supplied generators). The assignment witness is general but can fail to certify at scale (it needs F|α UP-refutable); a substitution witness from a live automorphism certifies the lead clauses at any size via an immediate conflict. Trying both gives SDCL that discovers AND scales.