Example TC-3. TC with a right identity does not necessarily satisfy RC.

\{ \begin{matrix}TC \\ x · e = x \end{matrix} \} ⇏ RC.

Model. The clauses

z_{1} · x = u, z_{2} · y = u, z_{1} · z = w, z_{3} · y = w → z_{2} · z = z_{3} · x x · e = x C_{4} · A = C_{3} · B C_{2} · A = C_{1} · B C_{4} · F = C_{3} · E C_{2} · F ≠ C_{1} · E

have the following model (found by MACE 1.2.0 on gyro at 0.89 seconds).

 e: 0          C3: 0         . | 0 1 2
 A: 0          C4: 0         --+------
 B: 0          F: 0          0 | 0 0 0
 C1: 1         E: 2          1 | 1 1 2
 C2: 1                       2 | 2 2 1