Function break_all_symmetry 

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

Iterated symmetry breaking to a fixpoint — the automated breaker. Repeatedly detect the formula’s variable symmetry and break each generator with one sound lex constraint — x_v ≤ x_{g[v]} at g’s least moved point v (v < g[v], and the lex-minimum of g’s orbit satisfies it, so it keeps ≥ 1 model per orbit, no auxiliary variables) — then re-detect on the strengthened formula, so symmetry that earlier breaks expose is broken in its turn. It runs until a round adds no new constraint: the symmetry “broken to conclusion.” Sound: every clause breaks a genuine symmetry of the current formula, so each round is equisatisfiability-preserving and the whole is equisatisfiable with the input. Returns the original clauses plus the accumulated breaks; the residual variable-symmetry group has shrunk (to trivial when single-bit breaks suffice). Solve the result with solve_comprehensive.