 Verifying the Robbins conjecture required proving Huntington's equation, or some other axiomatization of a Boolean algebra, as theorems of a Robbins algebra.Huntington, Robbins, Alfred Tarski, and others worked on the problem, but failed to find a proof or counterexample.William McCune proved the conjecture in 1996, using the automated theorem prover EQP.