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

{CS, xyyyxy = yyyyxx} ⇒ {zwzzzw = wwzzzz}.

Note that the conclusion is the dual (i.e., reverse) of the hypothesis. In group theory, substitute for each variable its inverse, take the inverse of both sides, then simplify.

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

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

8  x · x · x · x · y · y = y · x · x · x · y · x  [flip 6]
9  x · y · z · z · z · x · y · z = z · z · z · z · x · y · x · y  [4 → 6 :5,5]
13  x · x · x · x · y · y · z = y · x · x · x · y · x · z  [6 → 4 :5,5,5,5,5,5,5,5,5]
19  x · x · x · x · y · z · z · z · y · z = z · x · x · x · z · x · z · z · y · y  [8 → 13]
38  x · x · x · x · y · x · y = y · x · x · x · x · y · x  [2,1,9]

41 x · y · z · u · u · u · x · y · z · u = u · u · u · u · x · y · z · x · y · z

[4 → 9 :5,5]

66 x · y · y · y · y · x · y · z = y · y · y · y · x · y · x · z

[38 → 4 :5,5,5,5,5,5,5,5,5,5,5]

277  x · x · x · y · y · y · y · z · z = x · x · x · z · y · y · y · z · y  [2,13,19]
566  x · x · x · x · y · x · y · x · y = x · y · x · x · x · y · x · y · x  [2,66,41]
695  x · x · y · z · z · z · y · z = x · x · z · z · z · z · y · y  [2,1,277]
699  x · y · y · y · y · z · z = x · z · y · y · y · z · y  [2,1,695]

717 x · y · z · z · z · y · z · u = x · z · z · z · z · y · y · u

[699 → 4 :5,5,5,5,5,5,5,5,5,5,5]

718  x · y · y · y · y · z · z · u = x · z · y · y · y · z · y · u  [flip 717]
905  x · x · x · x · y · y · y · x = x · x · x · y · x · y · x · y  [2,718,566]
925  x · x · y · x · y · x · y = x · x · x · y · y · y · x  [2,1,905]
939  x · x · y · y · y · x = x · y · x · y · x · y  [2,1,925]
977  x · y · x · y · x = y · x · x · x · y  [2,1,939]
978  x · y · y · y · x = y · x · y · x · y  [2,939,1]
1017 x · y · z · x · y · z · x = y · z · x · x · x · y · z  [4 → 977 :5,5]
1054 x · y · y · y · x · z = y · x · y · x · y · z  [977 → 4 :5,5,5,5,5,5,5]
1088 x · y · x · y · x · z = y · x · x · x · y · z  [flip 1054]
1132 B · B · A · B · A · B = A · A · B · B · B · B → □  [978 → 7]
1505 x · x · y · y · y · x · z = y · x · x · x · y · y · z  [1088 → 1088]
1566 x · y · y · y · x · x · z = y · y · x · x · x · y · z  [flip 1505]
3129 x · x · x · y · x · y = y · x · x · y · x · x  [2,38,1017]
4718 x · x · y · x · x · y = x · x · x · y · y · x  [2,1017,1566]
4942 x · x · y · y · x = x · y · x · x · y  [2,1,4718]
5054 x · y · y · x = y · x · x · y  [2,1,4942]
5272 x · y · y · x · z = y · x · x · y · z  [5054 → 4 :5,5,5,5,5]

5383 x · x · y · x · y = y · y · x · x · x  [2,3129,5272]^{5972 x · x · y · y · y · z = y · y · x · y · x · z  [5383 → 4 :5,5,5,5,5,5,5]}^{6049 x · x · y · x · y · z = y · y · x · x · x · z  [flip 5972]}^{6050 □  [6049,1132]}

2