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

{CS, xxxyy = yxxyx} ⇒ {zzwww = wzwwz}.

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. Note also that in the proof below, Otter proves that squares commute.

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

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

8  x · y · y · x · y = y · y · y · x · x  [flip 6]
9  x · x · x · y · z · y · z = y · z · x · x · y · z · x  [4 → 6 :5,5]
11  x · y · z · z · x · y · z = z · z · z · x · y · x · y  [flip 9]
13  x · y · y · x · y · z = y · y · y · x · x · z  [6 → 4 :5,5,5,5,5,5,5]
14  x · x · x · y · y · z = y · x · x · y · x · z  [flip 13]
31  x · y · y · y · x · y = y · y · y · x · y · x  [2,1,9]
45  x · x · y · y · y · x · x = y · x · x · y · x · x · y  [8 → 14]
53  x · y · y · x · y · y · x = y · y · x · x · x · y · y  [flip 45]
55  x · y · z · z · z · x · y · z = z · z · z · x · y · z · x · y  [4 → 31 :5,5]
57  x · x · y · y · y · x · y · x = y · x · x · y · x · y · x · y  [31 → 14]
59  x · x · x · y · x · y · z = y · x · x · x · y · x · z  [31 → 4 :5,5,5,5,5,5,5,5,5]
60  x · y · y · x · y · x · y · x = y · y · x · x · x · y · x · y  [flip 57]
62  x · y · y · y · x · y · z = y · y · y · x · y · x · z  [flip 59]
65  x · x · y · x · y · y = y · x · x · y · y · x  [2,13,11]
82  x · y · y · x · x · y · z = y · y · x · y · x · x · z  [65 → 4 :5,5,5,5,5,5,5,5,5]
135  x · x · y · y · y · x · y · z = y · y · y · x · y · x · x · z  [59 → 62]
140  x · x · x · y · x · y · y · z = y · y · x · x · x · y · x · z  [flip 135]
171  x · y · x · x · x · y · y = y · y · x · y · x · x · x  [8 → 82]
487  x · x · y · x · x · y · y = y · x · x · x · y · y · x  [2,13,55]
598  x · x · y · x · y · x · y = y · y · x · y · x · x · x  [2,60,140]
612  x · y · y · y · x · x = y · x · y · x · y · x  [2,171,598]
613  x · x · y · y · x · y = y · x · y · x · y · x  [2,82,598]
643  x · y · x · y · x · y · z = y · x · x · x · y · y · z  [612 → 4 :5,5,5,5,5,5,5,5,5]
714  x · y · x · x · y · y = y · x · y · x · y · x  [2,487,643]
777  x · y · y · x · y = y · x · x · y · y  [2,613,714]
778  x · x · x · y · y = x · y · y · x · x  [2,612,714]
841  x · y · y · x · x · z = y · x · x · y · x · z  [777 → 4 :5,5,5,5,5,5,5]
869  x · x · y · y = y · y · x · x  [2,1,778]
920  x · x · y · y · z = y · y · x · x · z  [869 → 4 :5,5,5,5,5]
997  x · x · y · x · x · y = y · x · x · y · x · x  [2,53,920]
1949 x · x · y · y · y = y · x · y · y · x  [2,841,997]
1950 □  [1949,7]