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

{CS, xy^{2} = y^{2}x} ⇒ {(xy)^{4} = x^{4}y^{4}}.

This was previously proved by Padmanabhan (unpublished). In fact, Otter proves a stronger theorem, xyxyzyxu = zxxxyyyu, without using the cancellation laws. Proof (found by Otter 3.0.4 on gyro at 187.41 seconds).

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

8  x · y · z · y · z = y · z · y · z · x  [3 → 5 :4,4]
13  x · x · y · z = y · x · x · z  [5 → 3 :4,4,4]
14  x · y · y · z = y · y · x · z  [flip 13]
48  x · y · x · y · z · u = z · x · y · x · y · u  [8 → 3 :4,4,4,4,4,4,4]
50  x · y · z · y · z · u = y · z · y · z · x · u  [flip 48]
78  x · y · z · z · y · u = y · y · x · z · z · u  [14 → 14]
3988  x · y · y · y · z · z · z · u = y · z · y · z · x · z · y · u  [78 → 50]
4008  x · y · x · y · z · y · x · u = z · x · x · x · y · y · y · u  [flip 3988]
4009  □  [4008,1]