[T2] long gadgets (Table 2)
   mu=(3,) c=(1 2 3) r=3 L>=3: L-cycle True; = printed True; g = printed True, same for all L > r True; parity 'odd' True; Lemma 4.4 (formula, g fixes r+1..L, criterion) True
   mu=(3,) c=(1 3 5) r=5 L>=5: L-cycle True; = printed True; g = printed True, same for all L > r True; parity 'even' True; Lemma 4.4 (formula, g fixes r+1..L, criterion) True
   mu=(2, 2) c=(1 3)(2 4) r=4 L>=4: L-cycle True; = printed True; g = printed True, same for all L > r True; parity 'odd' True; Lemma 4.4 (formula, g fixes r+1..L, criterion) True
   mu=(2, 2) c=(1 4)(2 6) r=6 L>=6: L-cycle True; = printed True; g = printed True, same for all L > r True; parity 'even' True; Lemma 4.4 (formula, g fixes r+1..L, criterion) True
   mu=(5,) c=(1 2 3 4 5) r=5 L>=5: L-cycle True; = printed True; g = printed True, same for all L > r True; parity 'odd' True; Lemma 4.4 (formula, g fixes r+1..L, criterion) True
   mu=(5,) c=(1 2 3 5 6) r=6 L>=6: L-cycle True; = printed True; g = printed True, same for all L > r True; parity 'even' True; Lemma 4.4 (formula, g fixes r+1..L, criterion) True
   mu=(3, 3) c=(1 2 3)(4 5 6) r=6 L>=6: L-cycle True; = printed True; g = printed True, same for all L > r True; parity 'even' True; Lemma 4.4 (formula, g fixes r+1..L, criterion) True
   mu=(4, 2) c=(1 2 3 5)(4 6) r=6 L>=6: L-cycle True; = printed True; g = printed True, same for all L > r True; parity 'even' True; Lemma 4.4 (formula, g fixes r+1..L, criterion) True
[T3] small gadgets (Table 3)
   mu=(3,) tau=(2, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(2, 2) tau=(3, 1): c of type mu, x_tau c = printed, of type tau: True (split tau; conjugator even)
   mu=(2, 2) tau=(3, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(2, 2) tau=(3, 3): c of type mu, x_tau c = printed, of type tau: True
   mu=(2, 2) tau=(2, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(5,) tau=(4, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(5,) tau=(4, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(5,) tau=(4, 3): c of type mu, x_tau c = printed, of type tau: True
   mu=(5,) tau=(4, 4): c of type mu, x_tau c = printed, of type tau: True
   mu=(5,) tau=(3, 3): c of type mu, x_tau c = printed, of type tau: True
   mu=(5,) tau=(3, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(5,) tau=(3, 1, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(5,) tau=(2, 2, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(5, 1): c of type mu, x_tau c = printed, of type tau: True (split tau; conjugator even)
   mu=(3, 3) tau=(5, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(5, 3): c of type mu, x_tau c = printed, of type tau: True (split tau; conjugator even)
   mu=(3, 3) tau=(5, 4): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(5, 5): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(4, 1, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(4, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(4, 3): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(4, 4): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(3, 3): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(3, 2, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(3, 2, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(3, 1, 1, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(2, 2, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(3, 3) tau=(2, 2, 1, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(5, 1): c of type mu, x_tau c = printed, of type tau: True (split tau; conjugator even)
   mu=(4, 2) tau=(5, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(5, 3): c of type mu, x_tau c = printed, of type tau: True (split tau; conjugator ODD)
   mu=(4, 2) tau=(5, 4): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(5, 5): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(4, 1, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(4, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(4, 3): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(4, 4): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(3, 2, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(3, 2, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(3, 3, 1): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(3, 3, 2): c of type mu, x_tau c = printed, of type tau: True
   mu=(4, 2) tau=(2, 2, 1, 1): c of type mu, x_tau c = printed, of type tau: True
   42 small gadgets
[T4] partners (Table 4), witnesses on n points, 24 <= n <= 90
   mu=(3,) K=(2^{n/2}) -> P(K)=(3,1,2^{(n-4)/2}): witness valid for all 17 values of n: True
   mu=(5,) K=(2^{n/2}) -> P(K)=(3,1,2^{(n-4)/2}): witness valid for all 17 values of n: True
   mu=(4, 2) K=(3,1^{n-3}) -> P(K)=(4,3,2,1^{n-9}): witness valid for all 67 values of n: True
   mu=(4, 2) K=(2^{n/2}) -> P(K)=(3,1,2^{(n-4)/2}): witness valid for all 17 values of n: True
   mu=(4, 2) K=(2^{(n-1)/2},1) -> P(K)=(3,1,1,2^{(n-5)/2}): witness valid for all 17 values of n: True
   mu=(4, 2) K=(3^{n/3}) -> P(K)=(5,1,3^{n/3-2}): witness valid for all 23 values of n: True
[S1] Step 1 of the proof of Theorem B, literally, every even type of 24 <= n <= 52
   4532740 (type, mu) pairs: every even type outside E(mu,n) is covered as the text says, every member of E is left over, and no member of E contains a gadget: True
   (ii) distinct odd parts <= 7 sum to 16 < 24, (iii) 1+3+5 = 9 < 24: True; C has >= 18 fixed points for n >= 24 (non-split, real): True
[S2] Step 2: partners
   24 <= n <= 52: one partner per member of E, even, non-split, pairwise distinct, outside E: True
[C] Lemma 5.5 (odd 7 <= n <= 79) and Lemma 5.6 (odd 5 <= n <= 41)
   Lemma 5.5: 396877 types; P injective, even, 3 <= l(P) <= (n-1)/2, l + l(P) <= n+1: True
   Lemma 5.6 on random n-cycles: zt = (a1 a3 a2 a4 ... an), zt and tz in the other half: True
TOTAL FAILS: 0
