A machine transcript, made inspectable
Eight Days for Fifteen Lines
EQP searched for about eight days, then printed fifteen derived equations that force a contradiction. Replay every substitution, break one step, and see why a short checkable proof can remain hidden for decades.
The two inputs are simple. One is the Robbins equation. The other denies that any terms C, D can satisfy n(C + D) = n(C). Every later line is generated from earlier lines by paramodulation, with + treated as associative and commutative. If the last positive equality is an instance of the denial, the pair cannot both be true.
The substitution desk
Choose a line. The result is generated again, not copied into the verdict.
Line 5
acceptedPublished equation
Parents
Computed substitution
Selected redex
Generated result
Generated result matches the published line after AC normalization.
The load-bearing bridge
Fifteen lines do not contain every Boolean law.
They establish the second Winker condition. The published sufficiency route continues through three certificate stages. Choose a stage to inspect the handoff. This page recomputes the handoffs between their published endpoints; it does not claim to replay every internal line of those separate certificates.
The check
What is recomputed. The page parses all equations, standardizes parent variables apart, finds associative-commutative matches, performs the cited paramodulation, applies the listed demodulation on lines 16379 and 17666, and compares the generated result with each published conclusion. The final equality is then matched against denial line 2. The offline verifier also requires two negative controls to fail.
Published constants, not derived measurements. The transcript prints 678232.20 seconds. McCune separately described the search as about 8 days on an RS/6000 using about 30 MB. Only the conversion to 7.84991 days and the count of fifteen generated lines are computed here. The historical runtime is not a modern benchmark.
Uncertainty and free choices.
- Associative-commutative normalization may reorder and reassociate +. It never moves a term across n, and it does not assume idempotence, a zero, or double negation.
- The displayed ordering of equal AC sums, variable names, and the chosen witness terms C, D are free presentation choices. Other AC orderings and renamed variables express the same inference.
- This is an independent reconstruction of the EQP transcript. EQP itself did not emit a proof object. McCune used the EQP result to guide Otter, and a separate checker checked Otter's object.
- The browser checks the fifteen-line transcript and the endpoint handoffs in the Winker chain. The internal Winker certificate lines are linked below but are not replayed here, so the Boolean conclusion still relies on Winker's published sufficiency theorem and McCune's certificate archive.
- The successful search was guided by a target Winker condition and chosen search restrictions. It was not an unguided push of a button.
The vacuous setting. Testing the Robbins equation only in the two-element Boolean algebra cannot settle the hard direction, because Boolean algebras already satisfy it. Comparing an equation with itself, or merely sorting an AC sum, checks syntax rather than the proof. The green verdict requires every nontrivial inference and the final conflict.
Run the independent audit with node research/robbins-eqp/verify-robbins-eqp.mjs.
Sources and exact scope
- McCune and the Argonne Automated Deduction Group, EQP proof transcript. This is the frozen primary artifact for the two inputs, fifteen generated lines, dependencies, EQP version, start stamp, and printed runtime.
- William McCune, Robbins Algebras Are Boolean. This primary project account supplies the finding date, hardware class, rounded elapsed time and memory, search guidance, and the distinction between EQP's transcript and Otter's checked proof object.
- William McCune, Solution of the Robbins Problem, Journal of Automated Reasoning, 1997. This is the peer-reviewed theorem and search account.
- William McCune, Robbins Algebra Lemmas. This primary index states the three Winker lemmas, their dependency order, and links the EQP, Otter, and Otter proof-object files.
- Steve Winker, Absorption and idempotency criteria for a problem in near-Boolean algebras, Journal of Algebra, 1992. This is the peer-reviewed sufficiency result.
- Branden Fitelson, Using Mathematica to Understand the Computer Proof of the Robbins Conjecture, 1997. Its line-by-line reconstruction cross-checks the otherwise implicit substitutions, especially the simplification at line 16379.