The main 112-vertex counterexample

Statement

There is a simple connected bridgeless cubic graph G on 112 vertices and 168 edges, of girth five and edge- and vertex-connectivity three, with no Petersen coloring and no normal five-edge-coloring.

Assumptions

G is the exact labeled graph in Appendix A; its normalized sorted-edge-list digest identifies the SAT input. No minimum-order claim is made.

Explanation

Proof outlines · 1

Two independent coloring encodings

SAT encodings and externally checked DRAT certificates

Each possible coloring would satisfy its corresponding CNF. The reported UNSAT certificates exclude all satisfying assignments. Graph reconstruction, encoding semantics and certificate checking are distinct steps.

A solver’s UNSAT message alone is insufficient. OpenMath inspected the small archive and graph data, but has not rerun the four DRAT checks.

Proved: Explicit main graph and noncolorability reported ↗ · source dated Aug 8, 2026 · observed Oct 14, 2026. Exact main labeled graph in Theorem 1.1.

Proved: External SAT and DRAT checks reported ↗ · source dated Aug 8, 2026 · observed Oct 14, 2026. Four graph/formulation pairs; not an OpenMath execution.

Independent mathematical assessment of this argument remains separate from the statement’s attributed status.

The main 112-vertex counterexample →

Petersen and normal-five colorings are equivalent →

Constructions · 1

Inspect the main graph

Inspect the exact adjacency

112 numbered vertices and 168 undirected edges.

Vertex

Vertex 0 has neighbors 1, 5, 31.

Complete adjacency table

Every numbered vertex and its neighbors
Vertex	Neighbors
0	1, 5, 31
1	0, 2, 6
2	1, 7, 100
3	5, 6, 11
4	6, 7, 9
5	0, 3, 7
6	1, 3, 4
7	2, 4, 5
8	9, 10, 11
9	4, 8, 14
10	8, 12, 20
11	3, 8, 28
12	10, 13, 17
13	12, 14, 18
14	9, 13, 19
15	17, 18, 22
16	18, 19, 56
17	12, 15, 19
18	13, 15, 16
19	14, 16, 17
20	10, 21, 25
21	20, 22, 26
22	15, 21, 27
23	25, 26, 30
24	26, 27, 39
25	20, 23, 27
26	21, 23, 24
27	22, 24, 25
28	11, 29, 33
29	28, 30, 34
30	23, 29, 35
31	0, 33, 34
32	34, 35, 37
33	28, 31, 35
34	29, 31, 32
35	30, 32, 33
36	37, 38, 39
37	32, 36, 42
38	36, 64, 92
39	24, 36, 78
40	41, 45, 71
41	40, 42, 46
42	37, 41, 47
43	45, 46, 51
44	46, 47, 49
45	40, 43, 47
46	41, 43, 44
47	42, 44, 45
48	49, 50, 51
49	44, 48, 54
50	48, 52, 60
51	43, 48, 68
52	50, 53, 57
53	52, 54, 58
54	49, 53, 59
55	57, 58, 62
56	16, 58, 59
57	52, 55, 59
58	53, 55, 56
59	54, 56, 57
60	50, 61, 65
61	60, 62, 66
62	55, 61, 67
63	65, 66, 70
64	38, 66, 67
65	60, 63, 67
66	61, 63, 64
67	62, 64, 65
68	51, 69, 73
69	68, 70, 74
70	63, 69, 75
71	40, 73, 74
72	74, 75, 108
73	68, 71, 75
74	69, 71, 72
75	70, 72, 73
76	77, 81, 107
77	76, 78, 82
78	39, 77, 83
79	81, 82, 87
80	82, 83, 85
81	76, 79, 83
82	77, 79, 80
83	78, 80, 81
84	85, 86, 87
85	80, 84, 90
86	84, 88, 96
87	79, 84, 104
88	86, 89, 93
89	88, 90, 94
90	85, 89, 95
91	93, 94, 98
92	38, 94, 95
93	88, 91, 95
94	89, 91, 92
95	90, 92, 93
96	86, 97, 101
97	96, 98, 102
98	91, 97, 103
99	101, 102, 106
100	2, 102, 103
101	96, 99, 103
102	97, 99, 100
103	98, 100, 101
104	87, 105, 109
105	104, 106, 110
106	99, 105, 111
107	76, 109, 110
108	72, 110, 111
109	104, 107, 111
110	105, 107, 108
111	106, 108, 109

Construction details

Order and size: 112 vertices; 168 edges
Coloring encodings: Petersen: 3,640 variables and 68,324 clauses; normal five: 1,960 variables and 25,484 clauses
Certificate tools: CaDiCaL 3.0.1 at c60730422e758ef1cebe7aeddf2dda31c996bf04; drat-trim at 2e3b2dc0ecf938addbd779d42877b6ed69d9a985
Normalized edge-list SHA-256: dc16cc18600cf77c8661b7baf89c7019f265299308541961ff884ea7187b4e8b

The exact adjacency data identifies this witness. Inspecting neighbors does not verify noncolorability, and 112 is not asserted to be minimal.

The main 112-vertex counterexample →

Evidence

Source reports

Proved

Explicit main graph and noncolorability reported ↗

Exact main labeled graph in Theorem 1.1.

A 112-Vertex Counterexample to the Petersen Coloring Conjecture · Theorem 1.1; Section 3; Appendix A →

Source dated Aug 8, 2026 · Observed Oct 14, 2026

Proved

External SAT and DRAT checks reported ↗

Four graph/formulation pairs; not an OpenMath execution.

Petersen counterexample: frozen construction and certificates · 03_CERTIFICATION, 04_OPTIONAL_D3 and 05_DOCUMENTATION →

Source dated Aug 8, 2026 · Observed Oct 14, 2026

Connections

In this problem · publication v7 · Selected context

Petersen coloring conjecture →

Counterexample · Proved

Relationship not independently reviewed. This concerns its use in this problem.

Sources

A 112-Vertex Counterexample to the Petersen Coloring Conjecture →

Theorem 1.1; Section 3; Appendix A → · Original passage ↗
Recorded wording
The main graph has 112 vertices, 168 edges, girth five and edge- and vertex-connectivity three. Section 3 specifies its recursive construction.
paraphrase · Linked proof prose is not republished. Any copied graph data is CC0, as specified by its archive.
Introduction; Proposition 2.1; references to Jaeger (1985, 1988) → · Original passage ↗
Recorded wording
The edge-star formulation is equivalent to the existence of a normal five-edge-coloring. The original conjecture concerns every bridgeless cubic graph.
paraphrase · Linked proof prose is not republished. Any copied graph data is CC0, as specified by its archive.

Bryce Putman · Preprint · Publication date Aug 8, 2026

Source-reported results and external checks are separate from independent OpenMath assessment.

Revision & attribution

Source revision: v1. Observed Oct 14, 2026.

Putman reports extensive OpenAI-model assistance in discovery, search, verification and preparation; he reviewed the final claims and artifacts and accepts responsibility.

Petersen counterexample: frozen construction and certificates →

03_CERTIFICATION, 04_OPTIONAL_D3 and 05_DOCUMENTATION → · Original passage ↗
Recorded wording
CaDiCaL 3.0.1 reports UNSAT; drat-trim reports VERIFIED for four DRAT proofs. Separate encoders, satisfiable controls and status-parsing negative controls support the reported checks.
paraphrase · Linked proof prose is not republished. Any copied graph data is CC0, as specified by its archive.

Bryce Putman · Project documentation · Publication date Aug 8, 2026

Source-reported results and external checks are separate from independent OpenMath assessment.

Revision & attribution

Source revision: 1.1.0. Observed Oct 14, 2026.

The author attributes discovery and verification assistance to OpenAI systems; source logs are external computational reports.

History

Statement versions

Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.

Assessment history · 2

Assessments retained in these publication records. Earlier statement versions retain their own source histories.

Proved

External SAT and DRAT checks reported ↗

Four graph/formulation pairs; not an OpenMath execution.

Source dated Aug 8, 2026 · Observed Oct 14, 2026 · Source passage →

Proved

Explicit main graph and noncolorability reported ↗

Exact main labeled graph in Theorem 1.1.

Source dated Aug 8, 2026 · Observed Oct 14, 2026 · Source passage →

Record details

Claim ID: claim-petersen-112-main-witness
Statement version: 1
SHA-256: a85cdc53d405efc54b0fefb6f9010a099069ec6f0c4f6423a6574c451a6130cb

Publication records

Petersen coloring conjecture · publication v7 · JSON →