Theorem OC-3. Validity of ternary overlay for quasigroups.

\{ \begin{matrix}· is a quasigroup \\ g(x, e, e) = f(x, e, e) \\ g(e, x, e) = f(e, x, e) \\ g(e, e, x) = f(e, e, x) \end{matrix} \} =(gL)⇒ \{g(x, y, z) = f(x, y, z)\}.

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

1 g(A, B, C) ≠ f(A, B, C) 6,5 x\(x · y) = y 7 (x/y) · y = x 9 (x · y)/y = x 11 g(x, e, e) = f(x, e, e) 12 g(e, x, e) = f(e, x, e) 13 g(e, e, x) = f(e, e, x)

14  (x/y)\x = y  [7 → 5]
18  (x · g(y, e, e))/f(y, e, e) = x  [11 → 9]
42  (x · g(e, y, e))/f(e, y, e) = x  [12 → 9]
66  (x · g(e, e, y))/f(e, e, y) = x  [13 → 9]

90 (x · g(y, z, u))/f(y, v, w) = (x · g(v_{6}, z, u))/f(v_{6}, v, w)

[18 → 18 :(gL) :(gL) :(gL) :(gL)]

107  ((x · g(y, z, u))/f(y, v, w))\(x · g(v_{6}, z, u)) = f(v_{6}, v, w) [90 → 14]
224 (x · g(y, z, e))/f(y, z, e) = x [90 → 42]

406 (x · g(y, z, u))/f(v, w, u) = (x · g(y, z, v_{6}))/f(v, w, v_{6})

[66 → 66 :(gL) :(gL) :(gL) :(gL)]

1602  (x · g(y, z, u))/f(y, z, u) = x  [224 → 406, flip]
2470  g(x, y, z) = f(x, y, z)  [1602 → 107 :6]
2471  □  [2470,1]