Theorem RC-1. Inconsistency of RC with semilattices.

\{ \begin{matrix}RC \\ 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.55 seconds).

1 x = x 2 x · y = z, u · v = z, w · y = v_{6}, v_{7} · v = v_{6}, x · v_{8} = v_{9},

u · v_{10} = v_{9} → w · v_{8} = v_{7} · v_{10}

4,3 x · x = x 5 x · y = y · x 7,6 (x · y) · z = x · (y · z) 8 B = A → □

9  x · (y · x) = y · x  [2,5,3,5,3,1,5 :7,4]
16,15  x · y = y  [2,9,9,9,3,1,9 :4,4,7,4, flip]
17  x = y  [2,9,9,5,5,5,9 :16,16,16]
18  □  [17,8]