A 112-Vertex Counterexample to the Petersen Coloring Conjecture
We give an explicit simple bridgeless cubic graph on 112 vertices with no Petersen coloring, and hence no normal 5-edge-coloring. The graph is identified by the SHA-256 digest in Theorem 1.1. It is assembled from three copies of a four-pole L and a claw six-pole C; in turn, L is assembled from four copies of a four-pole F and one copy of C, where F is obtained from the Petersen graph by deleting the endpoints of one edge. We give direct SAT formulations for Petersen colorings and normal 5-edge-colorings. CaDiCaL 3.0.1 returned UNSAT for both formulas, and drat-trim verified the resulting DRAT proofs. The ancillary archive contains the construction, an explicit relabeling, the encoders, certificates, hashes, and verification programs. Combined with a theorem of Ma, Mattiolo, Steffen, and Wolf, the counterexample also implies that infinitely many connected simple bridgeless cubic graphs have no Petersen coloring. We also give a separately verified, nonisomorphic $D_3$-symmetric 112-vertex counterexample. We do not address whether 112 is minimum.