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

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

(⇐) is trivial, because the right-hand side is a well-known basis for group theory. The proof of (⇒) is below. The 2-basis is independent because each equation by itself has a projection (nongroup) model. (Also, it is known that no single axiom for groups can be as small as either of these [?].)

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

1 x = x 2 B · B′ = A · A′, A · (B · B′) = A, (A · B) · C = A · (B · C) → □ 3 ((x · y) · z) · (y · z)′ = x 6,5 (x · y)′ · (x · (y · z)) = z

7  (x · y) · ((z · u)′ · y)′ = (x · z) · u  [3 → 3]
8  x · (y · (z · y)′)′ = x · z  [3 → 3]
12  (x · y) · z = (x · u) · ((y · z)′ · u)′  [flip 7]
35  ((x · y) · (z · y)′) · z = x  [3 → 8, flip]
37  (x · (y · x)′)′ = y  [8 → 5 :6, flip]
43  ((x · y)′ · x)′ = y  [37 → 37]
45  x · (y · ((x · y)′ · z)) = z  [37 → 5]
48,47  (x′ · (y · z)′)′ = y · (z · x)  [5 → 43]
52,51  x · ((y · x)′ · (y · z)) = z  [43 → 5]
63  (x · y) · (z · y)′ = (x · (u · z)′) · u  [43 → 7]
75,74  (x · y) · (z · ((y · z)′ · u)) = x · u  [7 → 37 :48]
98  ((x · ((y · z) · (u · z)′)) · u) · y′ = x  [35 → 3]
119,118 (x · y) · (z′ · y)′ = x · z  [45 → 7 :75]
137,136 (x · y) · z = x · (y · z)  [12 :119]
143,142 x · (y · y′) = x  [98 :137,137,137,137,137,137,137,137,52]
182  x · (y · (z · y)′) = x · ((u · z)′ · u)  [63 :137,137]
193  B · B′ = A · A′ → □  [2 :143,137 :1,1]
196  x · (y · (x · y)′) = z · z′  [142 → 45]
200,199 (x · y)′ · x = y′  [142 → 5]
203 x · x′ = y · (z · (y · z)′) [flip 196]
205,204 x · (y · (z · y)′) = x · z′  [182 :200]
210  x · x′ = y · y′  [flip 203 :205]
211  □  [210,193]