Theorem DUAL-GT-3. An independent self-dual 3-basis for GT.

\{ \begin{matrix}x · (x′ · y) = y & (1) \\ (x · y′) · y = x & (2) \\ (x · y) · ((z · z′) · u) = (x · (v′ · v)) · (y · u) & (3) \end{matrix} \} .

The Otter proof below derives a well-known basis for GT. The basis is easily shown to be independent: the first two equations are not a basis because 3 variables are required, and MACE finds 3-element nongroup models of {(1),(3)} and (dually) of {(2),(3)}.

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

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

8  (x · (y′ · y)) · (z · u) = (x · z) · ((v · v′) · u)  [flip 7]
9  x′′ · y = x · y  [3 → 3, flip]
14,13  x′′ = x  [9 → 5 :6, flip]
15  x′ · (x · y) = y  [9 → 3]
17  (x · y) · y′ = x  [13 → 5]
27  (x · y) · z = (x · (u′ · u)) · (y · z)  [5 → 7]
38  (x · (y′ · y)) · (z · u) = (x · z) · u  [flip 27]
42  x · (y · x)′ = y′  [15 → 17]
50  (x · y)′ = y′ · x′  [17 → 42, flip]
65  (x · (y · z)) · (z′ · y′) = x  [50 → 17]
80  (x · ((y · z) · u)) · (u′ · (z′ · y′)) = x  [50 → 65]
91,90  (x · y) · ((z · z′) · u) = x · (y · u)  [15 → 8 :14, flip]
99,98  x · (y′ · y) = x  [65 → 8 :14,91, flip]
118,117 (x · y) · z = x · (y · z)  [38 :99, flip]
120,119 x · (y · y′) = x  [80 :118,118,118,118,4,4]
121  B · B′ = A · A′ → □  [2 :120,118 :1,1]
125  x · x′ = y · y′  [119 → 3]
126  □  [125,121]