Theorem LT-1. Inconsistency of a semilattice operation with (gL).

\{ \begin{matrix}xx = x \\ x(yz) = y(zx) \end{matrix} \} =(gL)⇒ \{x = y\}.

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

1 B ≠ A 4,3 x · x = x 5 x · (y · z) = y · (z · x)

10  x · (y · (z · y)) = x · y  [3 → 5 :(gL), flip]
12  (x · y) · (z · u) = z · (y · (u · x))  [5 → 5]
15,14  x · (y · x) = y · x  [3 → 5]
21,20  x · (y · z) = x · z  [10 :15]
25,24  x · y = y  [14 :21,4, flip]
26  x = y  [12 :25,25,25,25,25,25]
27  □  [26,1]