Theorem TBA-1. A short single axiom for TBA.

\{ \begin{matrix}f(f(v, w, x), y, f(v, w, z)) = f(v, w, f(x, y, z)) \\ f(y, x, x) = x \\ f(x, y, g(y)) = x \\ f(x, x, y) = x \\ f(g(y), y, x) = x \end{matrix} \} ⇔

{f(f(x, g(x), y), g(f(f(z, u, v), w, f(z, u, v6))), f(u, f(v6, w, v), z)) = y}.

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

1 x = x 3,2 f(f(x, y, z), u, f(x, y, v)) = f(x, y, f(z, u, v)) 4 f(x, y, y) = y 7,6 f(x, y, g(y)) = x 9,8 f(x, x, y) = x 10 f(g(x), x, y) = y 12 f(f(A, g(A), B), g(f(f(C, D, E), F, f(C, D, G))),

f(D, f(G, F, E), C)) ≠ B

13 f(f(A, g(A), B), g(f(C, D, f(E, F, G))), f(D, f(G, F, E), C)) ≠ B

[copy,12 :3]

14 f(x, y, f(z, f(x, y, u), u)) = f(x, y, u) [2 → 4]
17,16 f(f(x, y, z), u, y) = f(x, y, f(z, u, y))  [4 → 2]
18  f(x, y, f(z, x, u)) = f(z, x, f(x, y, u))  [4 → 2]
19  f(x, y, f(y, z, u)) = f(y, z, f(x, y, u))  [flip 18]
20  f(x, y, f(z, f(x, y, z), u)) = f(x, y, z)  [2 → 8]
22  f(x, y, x) = x  [8 → 2 :9,9]
25,24 f(f(x, y, z), u, x) = f(x, y, f(z, u, x))  [22 → 2]
33 f(x, y, f(z, x, g(y))) = x [6 → 14 :7]
46,45 f(x, y, f(z, u, f(v, x, g(y)))) = f(x, y, f(z, u, x))  [33 → 2 :25, flip]
57  f(x, y, z) = f(x, z, f(g(z), y, z))  [6 → 16]
60  f(x, y, f(g(y), z, y)) = f(x, z, y)  [flip 57]
61  f(x, y, f(z, g(y), x)) = x  [16 → 33 :46]
71  f(g(g(x)), x, y) = g(g(x))  [6 → 61]
80,79 g(g(x)) = x  [4 → 71, flip]
84,83 f(x, g(x), y) = y  [79 → 10]
85 f(x, g(y), f(z, y, x)) = x [79 → 61]
90,89 f(x, g(y), y) = x  [79 → 6]
91 f(B, g(f(C, D, f(E, F, G))), f(D, f(G, F, E), C)) ≠ B [13 :84]
163,162 f(x, y, f(z, x, y)) = f(z, x, y)  [4 → 19, flip]
286  f(x, g(y), f(y, x, z)) = x  [89 → 20 :90]
374  f(x, y, z) = f(y, z, x)  [286 → 85 :80,17,163]
403,402 f(g(x), y, x) = y  [83 → 374, flip]
420  f(x, y, z) = f(x, z, y)  [60 :403]
444  f(B, g(f(D, f(E, F, G), C)), f(D, f(G, F, E), C)) ≠ B  [374 → 91]

612  f(x, y, z) = f(z, y, x)  [374 → 420]
1085  B ≠ B  [612 → 444 :90]
1086  □  [1085,1]

Proof (⇐) found by Otter 3.0.4 on gyro at 1.73 seconds. 1 x = x 2 f(f(D, E, A), B, f(D, E, C)) = f(D, E, f(A, B, C)),

f(B, A, A) = A, f(A, B, g(B)) = A,

f(A, A, B) = A, f(g(B), B, A) = A → □

4,3 f(f(x, g(x), y), g(f(f(z, u, v), w, f(z, u, v_{6}))),

f(u, f(v_{6}, w, v), z)) = y

5 f(f(x, y, z), g(f(f(u, v, w), v_{6}, f(u, v, v_{7}))), f(v, f(v_{7}, v_{6}, w), u)) =

f(y, f(z, g(f(x, y, v_{8})), v_{8}), x)  [3 → 3]

6 f(f(x, g(x), y), g(f(f(z, u, f(v, f(w, v_{6}, v_{7}), v_{8})), g(f(f(v_{8}, v, v_{7}), v_{6},

f(v_{8}, v, w))), f(z, u, f(v_{9}, g(v_{9}), v_{10})))), f(u, v_{10}, z)) = y  [3 → 3]

8 f(x, f(y, g(f(z, x, u)), u), z) = f(f(z, x, y), g(f(f(v, w, v_{6}), v_{7},

f(v, w, v_{8}))), f(w, f(v_{8}, v_{7}, v_{6}), v))  [flip 5]
9  f(x, f(y, g(f(z, x, u)), u), z) = f(x, f(y, g(f(z, x, v)), v), z)  [5 → 5]
10  f(g(x), f(y, g(f(x, g(x), z)), z), x) = y  [3 → 5, flip]

13,12 f(f(x, g(x), y), g(f(z, g(z), f(u, g(u), v))), f(g(z), v, z)) = y

[6 → 6 :4]
15,14 f(g(x), y, x) = y  [12 → 12 :13, flip]
18  f(f(x, g(x), y), g(f(z, g(z), g(g(u)))), u) = y  [12 → 12 :15]
20  f(x, g(f(y, g(y), z)), z) = x  [10 :15]
27,26 f(x, g(g(g(y))), y) = x  [14 → 20]
31,30 g(f(x, g(x), y)) = g(y)  [14 → 20]
33,32 f(x, g(y), y) = x  [20 :31]
35,34 f(x, g(x), y) = y  [18 :31,27]
37,36 f(x, g(f(f(y, z, u), v, f(y, z, w))), f(z, f(w, v, u), y)) = x  [3 :35]
38  f(x, f(y, g(f(z, x, u)), u), z) = f(z, x, y)  [8 :37]
39  f(x, y, z) = f(y, f(z, g(f(x, y, u)), u), x)  [5 :37]
43,42 g(g(x)) = x  [14 → 34]
47,46 f(x, y, g(y)) = x  [42 → 32]
49,48 f(g(x), x, y) = y  [42 → 34]
51,50 f(x, y, g(x)) = y  [42 → 14]

52 f(f(D, E, A), B, f(D, E, C)) = f(D, E, f(A, B, C)),

f(B, A, A) = A, f(A, A, B) = A → □  [2 :47,49 :1,1]
56,55 f(x, f(y, g(f(z, x, u)), u), z) = f(x, f(y, g(z), g(x)), z) [46 → 9, flip]
59  f(x, y, z) = f(y, f(z, g(x), g(y)), x)  [39 :56]
60  f(x, f(y, g(z), g(x)), z) = f(z, x, y)  [38 :56]
67  f(x, g(f(y, z, u)), f(u, z, y)) = x  [48 → 36 :49,51]
107  f(x, y, z) = f(z, y, x)  [48 → 67 :43]
111  f(f(x, y, z), g(f(z, y, x)), u) = u  [67 → 107, flip]
132,131 f(f(x, y, z), u, f(x, y, v)) = f(y, f(z, u, v), x)  [36 → 111]

139 f(E, f(A, B, C), D) = f(D, E, f(A, B, C)), f(B, A, A) = A,

f(A, A, B) = A → □  [52 :132]
144  f(x, f(y, g(x), g(z)), z) = f(x, f(y, g(z), g(x)), z)  [50 → 55]
149  f(x, f(y, g(z), g(x)), z) = f(x, f(y, g(x), g(z)), z)  [flip 144]
160  f(x, y, z) = f(y, f(x, g(z), g(y)), z)  [107 → 59]
171  f(x, f(y, g(z), g(x)), z) = f(y, x, z)  [flip 160]
290,289 f(x, y, y) = y  [50 → 60 :33, flip]
294,293 f(x, f(y, g(x), g(z)), z) = f(x, z, y)  [107 → 60]

301 f(E, f(A, B, C), D) = f(D, E, f(A, B, C)),

f(A, A, B) = A → □  [139 :290 :1]
310,309 f(x, f(y, g(z), g(x)), z) = f(x, z, y)  [149 :294]
340 f(x, y, z) = f(z, x, y) [171 :310]
363,362 f(x, x, y) = x  [107 → 289]
364  □  [301 :363 :340,1]