Theorem RBA-3. A Robbins algebra with c + d = c is Boolean.

\{ \begin{matrix}x + y = y + x \\ (x + y) + z = x + (y + z) \\ n(n(x + y) + n(x + n(y))) = x \\ ∃c∃d (c + d = c) \end{matrix} \} ⇒ \{n(x + n(y)) + n(n(x) + n(y)) = y\}.

By Thm. RBA-2, it is sufficient to show ∃e, e + e = e.

Proof (found by Otter 3.0.4 on gyro at 1506.42 seconds).

1 x + x ≠ x 4,3 x + y = y + x 6,5 (x + y) + z = x + (y + z) 8,7 x + (y + z) = y + (x + z) 9 n(n(x + y) + n(x + n(y))) = x 12,11 c + d = c

14  n(n(x + (y + z)) + n(y + n(x + z))) = y  [7 → 9]
18  n(n(x + y) + n(y + n(x))) = y  [3 → 9]
20  n(n(x + y) + n(x + (n(y + z) + n(y + n(z))))) = x  [9 → 9 :4]
22  n(n(x + y) + n(n(y) + x)) = x  [3 → 9]
26  c + (x + d) = x + c  [11 → 7, flip]
31,30  c + (d + x) = c + x  [11 → 5, flip]
32  n(n(x + c) + n(c + n(x + d))) = c  [26 → 9]
40  n(n(c + x) + n(d + (n(c) + x))) = d + x  [30 → 18 :4,8]
44  n(n(c) + n(d + n(c))) = d  [11 → 18]
58  n(n(x + y) + n(n(x) + y)) = y  [3 → 18]
62  n(n(x + n(y)) + n(y + x)) = x  [3 → 18]
67,66  n(d + n(d + (n(c) + n(c)))) = n(c)  [44 → 18 :4,8,4]
77,76  n(n(c + x) + n(d + n(c + x))) = d  [30 → 14]
80  n(n(x + (y + z)) + n(y + n(z + x))) = y  [3 → 14]
102  n(n(x + (n(y + z) + n(z + n(y)))) + n(z + x)) = x  [18 → 22]
108  n(d + n(c + n(d + n(c)))) = n(d + n(c))  [44 → 22 :4,4]
112  n(x + n(x + (y + n(n(y) + x)))) = n(n(y) + x)  [22 → 22 :8,4,4]
130  n(n(x + (y + z)) + n(n(x + y) + z)) = z  [5 → 58]
146  n(x + n(y + (x + n(n(y) + x)))) = n(n(y) + x)  [58 → 58 :6,4]
176  n(n(x + n(y + z)) + n(y + (z + x))) = x  [5 → 62]
242  n(n(x + c) + n(c + n(d + x))) = c  [3 → 32]

294 n(n(x + n(y + n(z))) + n(x + (y + n(z + (y + n(y+

n(z))))))) = x  [62 → 20 :8,4,4]
434 n(n(c + n(d + x)) + n(x + c)) = c [3 → 242]
529,528 n(n(c) + n(d + (d + n(c)))) = d + d  [11 → 40 :4]

636 n(n(n(d + (n(c) + x)) + (y + n(c + x))) + n(y + (d + x))) = y

[40 → 80]

814  n(n(x + (y + z)) + n(n(y + x) + z)) = z  [7 → 130]
866  n(n(x + n(y + z)) + n(z + (y + x))) = x  [3 → 176]
1140  n(n(d + (x + n(c + y))) + n(y + (c + x))) = d + x  [30 → 866 :6]

1933,1932 n(n(c) + n(d + (n(x + c) + n(c + n(x))))) = d  [11 → 102 :4]

2194 n(n(c + n(d + n(c))) + n(c + n(c + n(d + n(c))))) = c

[108 → 434 :4]

2356 n(n(d + n(c + x)) + n(c + (x + n(d + n(c + x))))) = d

[76 → 112 :4,8,31,4,6,77]

5429,5428 n(d + n(d + (n(c + x) + n(c + (x + n(d + n(c + x))))))) =

n(c + x)  [76 → 294 :8,6,8,31,8]

6608 n(c + (x + n(d + n(c + x)))) = n(c + x)

[2356 → 814 :8,4,5429, flip]

6611,6610 n(c + n(d + n(c))) = n(c)  [11 → 6608 :31,12]
6653,6652 n(n(c) + n(c + n(c))) = c  [2194 :6611,6611]

6721,6720 n(c + n(c + (n(c) + n(c + (c + n(c + n(c))))))) = n(c)

[6652 → 294 :8]

6798 n(n(c + n(c)) + n(c + (c + n(c + n(c))))) = c

[6652 → 146 :4,6653]
7832  n(c + (c + n(c + n(c)))) = n(c)  [6798 → 814 :8,4,6721, flip]
7834  d + n(c + n(c)) = d  [7832 → 1140 :4,4,1933, flip]
8090  d + d = d  [7834 → 636 :4,67,529]
8092  □  [8090,1]