Theorem TC-6. Inconsistency of TC with semilattices.

\{ \begin{matrix}TC \\ x · x = x \\ x · y = y · x \\ (x · y) · z = x · (y · z) \end{matrix} \} ⇒ \{x = y\}.

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

1 x = x 2 x · y = z, u · v = z, x · w = v_{6}, v_{7} · v = v_{6} → u · w = v_{7} · y 4,3 x · x = x 5 x · y = y · x 7,6 (x · y) · z = x · (y · z) 8 B = A → □

24  x · (x · y) = x · y  [2,6,3,6,1 :7,4]
27,26  x · (y · x) = y · x  [2,5,3,6,1 :7,4]
43,42  x · y = y  [2,5,3,5,24 :7,27,4]
44  x = y  [2,5,1,3,24 :43,43,43]
45  □  [44,8]