Theorem CS-13. Nilpotent CS satisfy the quotient condition. Let a, b, c, d, a_{0}, b_{0}, c_{0}, d_{0} be constants.

\{ \begin{matrix}CS \\ xyzyx = yxzxy \\ aa_{0} = bb_{0} \\ ca_{0} = db_{0} \\ ac_{0} = bd_{0} \end{matrix} \} ⇒ \{cc_{0} = dd_{0}\}.

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

1 d · d_{0} = c · c_{0} → □ 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 8 b · b_{0} = a · a_{0} 11,10 d · b_{0} = c · a_{0} 12 b · d_{0} = a · c_{0}

15,14  b · b_{0} · x = a · a_{0} · x  [8 → 5 :6, flip]
17,16  d · b_{0} · x = c · a_{0} · x  [10 → 5 :6, flip]
18  b_{0} · d · x · c · a_{0} = c · a_{0} · x · b_{0} · d  [10 → 7 :17]
20  b_{0} · b · x · a · a_{0} = a · a_{0} · x · b_{0} · b  [8 → 7 :15]
22  x · y · z · u · y · x = y · x · z · u · x · y  [5 → 7 :6]
27  x · y · z · y · x · u = y · x · z · x · y · u  [7 → 5 :6,6,6,6,6,6,6]
28  d_{0} · b · x · a · c_{0} = b · d_{0} · x · d_{0} · b  [12 → 7]
30,29  b · d_{0} · x = a · c_{0} · x  [12 → 5 :6, flip]
31  a · c_{0} · x · d_{0} · b = d_{0} · b · x · a · c_{0}  [flip 28 :30]
33  b · x · b_{0} · y · b_{0} · x = a · a_{0} · x · y · x · b_{0}  [7 → 14]
53  x · d_{0} · a · c_{0} · x = d_{0} · x · b · x · d_{0}  [29 → 7]
66  c · a_{0} · x · b_{0} · d · y = b_{0} · d · x · c · a_{0} · y  [18 → 5 :6,6,6,6,6,6,6]
81  a · a_{0} · x · b_{0} · b · y = b_{0} · b · x · a · a_{0} · y  [20 → 5 :6,6,6,6,6,6,6]
95  d_{0} · b · x · a · c_{0} · y = a · c_{0} · x · d_{0} · b · y  [31 → 5 :6,6,6,6,6,6,6]
96  a · c_{0} · x · d_{0} · b · y = d_{0} · b · x · a · c_{0} · y  [flip 95]
137  x · b_{0} · y · a · a_{0} · x = b_{0} · x · y · b · x · b_{0}  [14 → 22]
138  x · y · z · u · v · y · x = y · x · z · u · v · x · y  [5 → 22 :6]
235  d_{0} · x · b · x · d_{0} · y = x · d_{0} · a · c_{0} · x · y  [53 → 5 :6,6,6,6,6,6,6]
236  x · d_{0} · a · c_{0} · x · y = d_{0} · x · b · x · d_{0} · y  [flip 235]
309  a · a_{0} · d_{0} · x · d_{0} · b_{0} = a · c_{0} · b_{0} · x · b_{0} · d_{0}  [29 → 33, flip]
430,429  b_{0} · d · b · c · a_{0} · x = c · a_{0} · a · a_{0} · d · x  [14 → 66, flip]
488  a · a_{0} · x · b_{0} · a · c_{0} = b_{0} · b · x · a · a_{0} · d_{0}  [12 → 81]
550  a · c_{0} · x · d_{0} · a · a_{0} = d_{0} · b · x · a · c_{0} · b_{0}  [8 → 96]
645  x · b_{0} · y · z · a · a_{0} · x = b_{0} · x · y · z · b · x · b_{0}  [5 → 137 :6]
648  b_{0} · x · y · z · b · x · b_{0} = x · b_{0} · y · z · a · a_{0} · x  [flip 645]
944  x · y · z · u · z · y · x = z · x · y · u · y · x · z  [27 → 138]

1006,1005 d_{0} · d · b · d · d_{0} · b_{0} = d · d_{0} · a · c_{0} · c · a_{0}  [10 → 236, flip]
1263  a_{0} · d_{0} · x · d_{0} · b_{0} = c_{0} · b_{0} · x · b_{0} · d_{0}  [3,2,309, flip]
1265  a_{0} · d_{0} · x · y · d_{0} · b_{0} = c_{0} · b_{0} · x · y · b_{0} · d_{0}  [5 → 1263 :6]
1483  c_{0} · b_{0} · b · x · a · a_{0} · d_{0} = a · c_{0} · a_{0} · x · b_{0} · c_{0} · a  [488 → 138]
1484  a · c_{0} · a_{0} · x · b_{0} · c_{0} · a = c_{0} · b_{0} · b · x · a · a_{0} · d_{0}  [flip 1483]
1541  a_{0} · d_{0} · b · x · a · c_{0} · b_{0} = a · a_{0} · c_{0} · x · d_{0} · a_{0} · a  [550 → 138]
1542  a · a_{0} · c_{0} · x · d_{0} · a_{0} · a = a_{0} · d_{0} · b · x · a · c_{0} · b_{0}  [flip 1541]
3341  a_{0} · d_{0} · x · a · c_{0} · b_{0} = c_{0} · b_{0} · x · a · a_{0} · d_{0}  [29 → 1265 :15]
3343  a_{0} · d_{0} · x · y · z · d_{0} · b_{0} = c_{0} · b_{0} · x · y · z · b_{0} · d_{0}  [5 → 1265 :6]
5263,5262 a_{0} · d_{0} · x · y · a · c_{0} · b_{0} = c_{0} · b_{0} · x · y · a · a_{0} · d_{0}  [5 → 3341 :6]
5268  a · a_{0} · c_{0} · x · d_{0} · a_{0} · a = c_{0} · b_{0} · b · x · a · a_{0} · d_{0}  [1542 :5263]
7031  x · y · z · u · z · y · x = z · y · x · u · x · y · z  [138 → 944]

9084 a_{0} · d · d_{0} · a · c_{0} · c · a_{0} = c_{0} · c · a_{0} · a · a_{0} · d · d_{0}

[1005 → 3343 :17,430]

10077  c_{0} · a_{0} · x · b_{0} · c_{0} · a = a_{0} · c_{0} · x · d_{0} · a_{0} · a  [3,1484,5268]
10079  a_{0} · c_{0} · d · d_{0} · a_{0} · a = c_{0} · a_{0} · c · a_{0} · c_{0} · a  [16 → 10077, flip]
10101  c_{0} · d · d_{0} · a_{0} · a = c_{0} · c · c_{0} · a_{0} · a  [3,27,10079, flip]
10103  d · d_{0} · a_{0} · a = c · c_{0} · a_{0} · a  [3,2,10101, flip]
10151  a_{0} · a · d · d_{0} · a · a_{0} = a · a_{0} · c · c_{0} · a_{0} · a  [10103 → 22, flip]
10421  a · d · d_{0} · a · a_{0} = a · c · c_{0} · a · a_{0}  [3,22,10151, flip]
10423  d · d_{0} · a · a_{0} = c · c_{0} · a · a_{0}  [3,2,10421, flip]
10477  d · d_{0} · a · a_{0} · x = c · c_{0} · a · a_{0} · x  [10423 → 5 :6,6,6,6,6, flip]

10555 b_{0} · x · d · d_{0} · b · x · b_{0} = x · b_{0} · c · c_{0} · a · a_{0} · x

[10477 → 645, flip]
13651  x · d · d_{0} · b · x · b_{0} = x · c · c_{0} · b · x · b_{0}  [3,648,10555, flip]
13665  d · d_{0} · b · x · b_{0} = c · c_{0} · b · x · b_{0}  [3,2,13651, flip]
13671  d · d_{0} · b · x · y · b_{0} = c · c_{0} · b · x · y · b_{0}  [5 → 13665 :6]

13744,13743 d · d_{0} · a · c_{0} · c · a_{0} = c · c_{0} · a · c_{0} · c · a_{0}

[27 → 13671 :1006,11,30]

13747 c_{0} · c · a_{0} · a · a_{0} · d · d_{0} = a_{0} · c · c_{0} · a · c_{0} · c · a_{0}

[9084 :13744, flip]

18197  c · a_{0} · a · a_{0} · d · d_{0} = c · a_{0} · a · a_{0} · c · c_{0}  [3,7031,13747, flip]
18201  a_{0} · a · a_{0} · d · d_{0} = a_{0} · a · a_{0} · c · c_{0}  [3,2,18197, flip]
18205  a · a_{0} · d · d_{0} = a · a_{0} · c · c_{0}  [3,2,18201, flip]
18225  a_{0} · d · d_{0} = a_{0} · c · c_{0}  [3,2,18205, flip]
18263  d · d_{0} = c · c_{0}  [3,2,18225, flip]
18265  □  [18263,1]