Problem STN-1. (gL)-basis for ternary Steiner law. The type is ⟨3, 0⟩.

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

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

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

9,8  f(e, x, f(e, y, x)) = y  [3 → 6]
12  f(x, e, e) = f(x, y, f(e, y, e))  [6 → 4 :(gL)]
20  f(e, x, f(y, f(z, e, e), x)) = f(z, u, f(y, u, e))  [8 → 12 :(gL)]
282  f(e, e, x) = f(y, f(y, e, e), x)  [(gL) 20]
347  f(x, y, f(x, y, e)) = e  [282 → 20 :9, flip]
422  f(x, y, f(x, y, z)) = z  [6 → 347 :(gL) :7]
424  □  [422,1]