Theorem TBG-1. A (gL)-basis for ternary Boolean groups. The pair of equations {p(x, x, x) = x, p(x, y, p(z, u, v)) = p(y, z, p(u, v, x))} is a (gL)-basis for the variety of Boolean groups, where p(x, y, z) is x + (y + z). It is sufficient to derive a basis for Boolean groups as follows.

\{ \begin{matrix}p(x, x, x) = x \\ p(x, y, p(z, u, v)) = p(y, z, p(u, v, x)) \\ p(x, y, z) = x + (y + z) \end{matrix} \} =(gL)⇒

\{ \begin{matrix}(x + y) + z = x + (y + z) \\ x + x = y + y \\ x + (y + y) = x \end{matrix} \} .

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

1 x = x 2 (A + B) + C = A + (B + C), B + B = A + A,

A + (B + B) = A → □

3 p(x, x, x) = x 4 p(x, y, p(z, u, v)) = p(y, z, p(u, v, x)) 5 p(x, y, z) = x + (y + z)

7,6  (x + (x + x)) + (x + x) = x  [3 → 3 :5,5]
13,12  x + (x + x) = x  [3 → 6 :5,7]
14  x + (y + z) = y + (z + (z + (z + x)))  [3 → 4 :5,5,5]
16,15  x + (y + (z + (x + x))) = y + (z + x)  [3 → 4 :5,5,5]
17  x + (y + z) = y + (x + z)  [(gL) 4 :5,5]
20,19  x + (y + (x + x)) = y + x  [12 → 17, flip]
26,25  (x + x) + (y + x) = y + x  [12 → 14 :13]
32  x + (y + (y + (y + z))) = z + (x + y)  [14 → 12 :13]
35,34  (x + x) + ((x + x) + y) = x + (x + y)  [19 → 19 :(gL)]
36  x + (x + (y + x)) = y + x  [17 → 19]
38  x + (x + (x + (x + (x + y)))) = y + x  [14 → 19]
43,42  (x + x) + x = x  [12 → 19 :26,13]
56  ((x + x) + y) + (x + x) = (x + y) + x  [42 → 12 :(gL) :43]
61,60  ((x + y) + (x + y)) + z = (y + y) + z  [25 → 25 :(gL)]
65,64  (x + x) + (y + (z + x)) = y + (z + x)  [19 → 25 :(gL) :61,20]

68,67 (x + y) + ((x + y) + z) = y + (y + z)

[25 → 34 :26,26,26,26,61,61,35,26, flip]

76,75  x + ((y + x) + x) = y + x  [14 → 36 :68,13]
80  (x + (y + y)) + (y + y) = (x + y) + y  [36 → 56 :65,20]
84  (x + (y + y)) + y = (x + y) + (y + y)  [12 → 56 :(gL) :26, flip]
96,95  (x + y) + (z + y) = x + (y + (z + y))  [12 → 75 :(gL) :13,16]
99  ((x + y) + y) + (x + (x + y)) = x + y  [75 → 75 :76,96,76]
110  (x + (y + y)) + y = x + y  [84 :96,13]
125,124 (x + (y + y)) + z = x + z  [42 → 110 :(gL) :43]
143,142 (x + y) + y = x + (y + y)  [80 :125, flip]
145,144 x + (x + (x + y)) = x + y  [99 :143,125]

148  x + y = y + x  [38 :145,145]
149  x + (y + z) = z + (x + y)  [32 :145]
167  x + (y + (z + y)) = x + z  [36 → 148 :(gL)]
170,169 x + (y + (z + z)) = x + y  [19 → 148 :(gL)]
176,175 (x + y) + z = x + (y + z)  [15 → 148 :170, flip]
194 x + (y + (x + z)) = y + z [36 → 148 :(gL) :176,176]
197,196 x + (y + (y + z)) = x + z  [19 → 148 :(gL) :176,176]
209 B + B = A + A, A + (B + B) = A → □ [2 :176 :1]
222,221 x + (y + y) = x  [12 → 167 :176,197]
224 B + B = A + A → □ [209 :222 :1]
231,230 x + (y + x) = y  [149 → 221]
236  x + x = A + A → □  [194 → 224 :231]
237  □  [236,221]