Theorem CS-5. Support (5) for the CS conjecture.

\{ \begin{matrix}(xy)z = x(yz) \\ xyzu = yzux \end{matrix} \} ⇒ \{ \begin{matrix}(xy)^{3} = x^{3}y^{3} \\ x^{3}y^{3} = y^{3}x^{3} \end{matrix} \} .

Proof (found by Otter 3.0.4 on gyro at 4.89 seconds). 4 A · B · A · B · A · B = A · A · A · B · B · B,

B · B · B · A · A · A = A · A · A · B · B · B → □

6,5 (x · y) · z = x · y · z 7 x · y · z · u = y · z · u · x

8  x · y · z · u = u · x · y · z  [flip 7]
9  x · y · z · u · v · w = y · w · z · u · v · x  [7 → 7 :6,6]
22  x · y · z · u = z · u · x · y  [7 → 8]
111  x · y · z · u · v · w = v · u · w · y · z · x  [22 → 9 :6]
134  x · y · z · u · v · w = w · u · v · y · x · z  [flip 111]
373  x · y · z · u · v · w = z · w · y · u · x · v  [8 → 134 :6]
412  x · y · z · u · v · w = v · z · x · u · w · y  [flip 373]
462  □  [4,412,134]