Theorem STN-3. (gL)-basis for 5-ary Steiner law.

\{ \begin{matrix}f(u, v, w, x, y) = f(u, v, w, y, x) \\ f(e, e, e, e, e) = e \\ f(e, e, e, x, f(e, e, e, x, y)) = y \end{matrix} \} =(gL)⇒

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

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

1 f(E, D, A, B, f(E, D, A, B, C)) ≠ C 3 f(x, y, z, u, v) = f(x, y, z, v, u) 4 f(e, e, e, e, e) = e 7,6 f(e, e, e, x, f(e, e, e, x, y)) = y

9,8 f(e, e, e, x, f(e, e, e, y, x)) = y  [3 → 6]
12 f(x, y, z, e, e) = f(x, y, z, u, f(e, e, e, u, e))  [6 → 4 :(gL) :(gL) :(gL)]

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

[8 → 12 :(gL) :(gL) :(gL)]

223 f(e, e, e, e, x) = f(y, z, u, f(y, z, u, e, e), x)  [(gL) 20]
277 f(x, y, z, u, f(x, y, z, u, e)) = e  [223 → 20 :9, flip]
340 f(x, y, z, u, f(x, y, z, u, v)) = v  [6 → 277 :(gL) :7]
342 □  [340,1]