Wormald conjectured that every cubic graph of order divisible by four has an edge partition into two isomorphic spanning linear forests. The question is whether this holds for all such cubic graphs, including disconnected ones.

The witness graph is the disjoint union of K_{3,3} with a 10-vertex bridged cubic graph built from two subdivided copies of K_4. Degree counting and the complement structure on K_{3,3} force every monochromatic component to have even order. A parity argument on a five-vertex side of the bridge then gives a contradiction. In Lean, the component inventories of all 512 edge subsets of K_{3,3} are checked with a kernel-checked certificate checker, and the inventory and parity lemmas are proved formally.

The 16-vertex graph is a counterexample, and adjoining copies of K_4 gives counterexamples of every order 16+4t. The connected case remains open. Both the concrete theorem and the family theorem are machine-checked in Lean and depend only on the standard axioms (propext, Classical.choice, Quot.sound).