This web page is associated with a paper (with the same name)
that will appear in the
*Journal of Automated Reasoning*.
Here is the
preprint.

The EQP proofs use associative-commutative unification, and the Otter proofs use associativity and commutativity as axioms.

**Lemma 0**.
Robbins algebras satisfying *exists C (C+C=C)* are Boolean.

The EQP proof is the same as the one in the paper.

**Lemma 1**.
Robbins algebras satisfying *exists C exists D (C+D=C)* are Boolean.

The EQP proof is the same as the one in the paper.

**Lemma 2**.
Robbins algebras satisfying *exists C exists D (n(C+D)=n(C))* are Boolean.

(Lemma 2 is not used in the overall proof in the paper.)

**Lemma 3**.
All Robbins algebras satisfy *exists C exists D (C+D=C)*.

The EQP proof is the same as the one in the paper (search m5-50).

This proof is from the same search (m5-50) as the proof of Lemma 3 above.