Function grid_tseitin 

pub fn grid_tseitin(
    w: usize,
    n: usize,
) -> (Vec<XorEquation>, DimacsCnf, ExpectedVerdict)

The Tseitin formula on a w × n grid with odd total charge — UNSATISFIABLE, and the sharpest indictment of resolution search there is. A grid has treewidth exactly w (a fixed constant, independent of the length n), so a POLYNOMIAL-size, bounded-width resolution refutation provably EXISTS. Yet CDCL solvers without Gaussian reasoning blow up on the parity regardless — they cannot find the short proof that is known to exist — while Gaussian elimination over GF(2) decides it in near-linear time. One Boolean per grid edge; per vertex, the XOR of its incident edges equals its charge (vertex 0 charged, the rest not — an odd sum, hence inconsistent). Returns the XOR system (for crate::xorsat) and the equisatisfiable CNF.