Theorem DUAL-GT-2. An independent self-dual 2-basis for Abelian GT.

\{ \begin{matrix}(z · (x · y)) · (y · z)′ = x \\ (z · y)′ · ((y · x) · z) = x \end{matrix} \} ⇔ \{ \begin{matrix}x · x′ = y · y′ \\ x · (y · y′) = x \\ (x · y) · z = x · (y · z) \\ x · y = y · x \end{matrix} \} .

(⇐) is trivial, because the right-hand side is a well-known basis for Abelian group theory. The proof of (⇒) is below. MACE shows the 2-basis to be independent with a 3-element nongroup model of the first equation.

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

1 x = x 2 B · B′ = A · A′, A · (B · B′) = A, (A · B) · C = A · (B · C),

B · A = A · B → □

3 (x · (y · z)) · (z · x)′ = y 5 (x · y)′ · ((y · z) · x) = z

7  (x · y) · ((z · u)′ · x)′ = u · (y · z)  [3 → 3]
17  ((x · y)′ · y)′ · z = z · x  [3 → 5]
20  x · y = ((y · z)′ · z)′ · x  [flip 17]
23  x · (y · (y · z)′)′ = z · x  [5 → 3]
26  x · y = y · (z · (z · x)′)′  [flip 23]
31  ((x · y) · (z · x)′) · z = y  [5 → 17, flip]
62,61  ((x · (y · z))′ · y)′ = z · x  [31 → 31, flip]
95  (((x · y)′ · y)′ · z)′ · ((x · u) · z) = u  [20 → 5]
126  x · ((y · (z · x)′) · z) = y  [31 → 7 :62, flip]
171  x · (((((y · x)′ · z)′ · z)′ · u) · y) = u  [20 → 126]
173  x · (((y · x)′ · z) · y) = ((z · u)′ · u)′  [17 → 126]
183,182 (x · (x · y)′)′ = y  [5 → 126]
184  ((x · y)′ · y)′ = z · (((u · z)′ · x) · u)  [flip 173]
185  x · y = y · x  [26 :183]
198  (((x · (y · z)′) · y) · (u · z)) · x′ = u  [126 → 3]
212,211 ((x · y)′ · y)′ · z = x · z  [20 → 185]
223,222 x · (((y · x)′ · z) · y) = z  [171 :212]
245  (x · y)′ · ((x · z) · y) = z  [95 :212]
255  ((x · y)′ · y)′ = x  [184 :223]
257  (x · (y · x)′)′ = y  [185 → 182]
294,293 (x · y) · z = x · (y · z)  [255 → 7]
330,329 (x · y)′ · (x · (z · y)) = z  [245 :294]
353  x · (y · x′) = y  [198 :294,294,294,330,294]
423  B · B′ = A · A′, A · (B · B′) = A → □  [2 :294 :1,185]
458  x · (x′ · y) = y  [185 → 353]
465,464 (x · y′)′ = y · x′  [353 → 182]
482,481 x · (y · y′) = x  [257 :465,294]
492  B · B′ = A · A′ → □  [423 :482 :1]
526  x · x′ = y · y′  [481 → 458]
527  □  [526,492]