Function structural_profile 

pub fn structural_profile(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> StructuralProfile

Profile an instance: collapse its rules to orbit-types, probe which cut decides it, and carve it to its irreducible core. The reading that emerges — quotient size tracks cut-decidability tracks core reducibility — is the single axis underneath every lever: difficulty is quotient size.