Function tseitin_expander 

pub fn tseitin_expander(
    n: usize,
    seed: u64,
) -> (Vec<XorEquation>, DimacsCnf, ExpectedVerdict)

The Tseitin formula on a random 3-regular expander with odd total charge — UNSATISFIABLE, exponentially hard for resolution (so every CDCL solver blows up), yet solved in polynomial time by Gaussian elimination over GF(2). A non-pigeonhole hard family: the hardness is parity / graph expansion, not covering symmetry. One Boolean per edge; per vertex, the XOR of its incident edges equals that vertex’s charge (vertex 0 charged, the rest not — an odd sum, hence inconsistent). Returns the XOR system (for crate::xorsat) and the equisatisfiable CNF.