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

{CS, xyzyx = yxzxy} ⇒ {xyyx = yxxy}.

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

1 A · B · B · A = B · A · A · B → □ 2 x = x 3 x · y = z, x · u = z → y = u 6,5 (x · y) · z = x · y · z 7 x · y · z · y · x = y · x · z · x · y

11  x · y · z · u · y · x = y · x · z · u · x · y  [5 → 7 :6]
17  x · y · z · y · x · u = y · x · z · x · y · u  [7 → 5 :6,6,6,6,6,6,6]
22  x · y · z · u · v · y · x = y · x · z · u · v · x · y  [5 → 11 :6]
262  x · y · x · z · z · x = x · y · z · x · x · z  [3,17,22]
329  x · y · z · z · y = x · z · y · y · z  [3,2,262]
376  x · y · y · x = y · x · x · y  [3,2,329]
377  □  [376,1]