Boolean meet and the constants 0 and 1 are easily defined from the Robbins algebra primitives.
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.
For a complete proof of the Robbins conjecture in one consistent notation and following McCune closely, see Mann (2003).