[1] class test (F1)-(F2) and reality (F3) against conjugation orbits of A_n
   n=4: 12 elements, 4 A_n-classes; labels = orbits: True; sizes and (F3): True
   n=5: 60 elements, 5 A_n-classes; labels = orbits: True; sizes and (F3): True
   n=6: 360 elements, 7 A_n-classes; labels = orbits: True; sizes and (F3): True
   n=7: 2520 elements, 9 A_n-classes; labels = orbits: True; sizes and (F3): True
   n=8: 20160 elements, 14 A_n-classes; labels = orbits: True; sizes and (F3): True
   (0.2 s)
[2] brute force over A_n, 4 <= n <= 8: Hall matchings (Lemma 2.2) and tight sets
   n=4: no Hall matching exactly for C = 3+, 3- (A_4 not expansive); S = V_4 (2 classes), C = 3+ or 3-: SC is 1 class
   n=5: 5 classes, a Hall matching for every class C: True; max |T(C)| = 3
   n=6: 7 classes, a Hall matching for every class C: True; max |T(C)| = 3
   n=7: 9 classes, a Hall matching for every class C: True; max |T(C)| = 3
   n=8: 14 classes, a Hall matching for every class C: True; max |T(C)| = 5
   (0.7 s)
[3] S_n is not conjugacy-expansive: S = A_n, C = transpositions
   n=3: SC = S_n minus A_n: True; k(S) = 2 > k(SC) = 1
   n=4: SC = S_n minus A_n: True; k(S) = 3 > k(SC) = 2
   n=5: SC = S_n minus A_n: True; k(S) = 4 > k(SC) = 3
   n=6: SC = S_n minus A_n: True; k(S) = 6 > k(SC) = 5
   n=7: SC = S_n minus A_n: True; k(S) = 8 > k(SC) = 7
   3 <= n <= 60: #even - #odd partitions = #partitions into distinct odd parts >= 1: True
   (11.2 s)
[4] character-free certificates (Theorem A; Theorem B for n <= 23)
   cert_all_n12_14.jsonl: 9888 witness pairs, all valid: True, label mismatches: 0 (0.1 s)
      n=12: 42 classes C certified (every non-identity class C; 42 non-identity classes)
      n=13: 54 classes C certified (every non-identity class C; 54 non-identity classes)
      n=14: 71 classes C certified (every non-identity class C; 71 non-identity classes)
   cert_all_n15_18.jsonl: 87728 witness pairs, all valid: True, label mismatches: 0 (0.9 s)
      n=15: 93 classes C certified (every non-identity class C; 93 non-identity classes)
      n=16: 122 classes C certified (every non-identity class C; 122 non-identity classes)
      n=17: 155 classes C certified (every non-identity class C; 155 non-identity classes)
      n=18: 199 classes C certified (every non-identity class C; 199 non-identity classes)
   cert_all_n5_11.jsonl: 2104 witness pairs, all valid: True, label mismatches: 0 (0.0 s)
      n=5: 4 classes C certified (every non-identity class C; 4 non-identity classes)
      n=6: 6 classes C certified (every non-identity class C; 6 non-identity classes)
      n=7: 8 classes C certified (every non-identity class C; 8 non-identity classes)
      n=8: 13 classes C certified (every non-identity class C; 13 non-identity classes)
      n=9: 17 classes C certified (every non-identity class C; 17 non-identity classes)
      n=10: 23 classes C certified (every non-identity class C; 23 non-identity classes)
      n=11: 30 classes C certified (every non-identity class C; 30 non-identity classes)
   cert_small_n5_23.jsonl: 14957 witness pairs, all valid: True, label mismatches: 0 (0.2 s)
      n=5: 4 classes C certified (every non-identity class C; 4 non-identity classes)
      n=6: 6 classes C certified (every non-identity class C; 6 non-identity classes)
      n=7: 5 classes C certified (exactly the classes of support <= 6; 8 non-identity classes)
      n=8: 5 classes C certified (exactly the classes of support <= 6; 13 non-identity classes)
      n=9: 5 classes C certified (exactly the classes of support <= 6; 17 non-identity classes)
      n=10: 5 classes C certified (exactly the classes of support <= 6; 23 non-identity classes)
      n=11: 5 classes C certified (exactly the classes of support <= 6; 30 non-identity classes)
      n=12: 5 classes C certified (exactly the classes of support <= 6; 42 non-identity classes)
      n=13: 5 classes C certified (exactly the classes of support <= 6; 54 non-identity classes)
      n=14: 5 classes C certified (exactly the classes of support <= 6; 71 non-identity classes)
      n=15: 5 classes C certified (exactly the classes of support <= 6; 93 non-identity classes)
      n=16: 5 classes C certified (exactly the classes of support <= 6; 122 non-identity classes)
      n=17: 5 classes C certified (exactly the classes of support <= 6; 155 non-identity classes)
      n=18: 5 classes C certified (exactly the classes of support <= 6; 199 non-identity classes)
      n=19: 5 classes C certified (exactly the classes of support <= 6; 253 non-identity classes)
      n=20: 5 classes C certified (exactly the classes of support <= 6; 323 non-identity classes)
      n=21: 5 classes C certified (exactly the classes of support <= 6; 407 non-identity classes)
      n=22: 5 classes C certified (exactly the classes of support <= 6; 512 non-identity classes)
      n=23: 5 classes C certified (exactly the classes of support <= 6; 640 non-identity classes)
   (1.2 s)
[5] Theorem B: gadgets, Step 1, Step 2
   long  mu=3      c=(1 2 3)            r=3: L-cycle for r <= L <= 60: True; locality: True; conjugator even for odd L: False
   long  mu=3      c=(1 3 5)            r=5: L-cycle for r <= L <= 60: True; locality: True; conjugator even for odd L: True
   long  mu=2.2    c=(1 3)(2 4)         r=4: L-cycle for r <= L <= 60: True; locality: True; conjugator even for odd L: False
   long  mu=2.2    c=(1 4)(2 6)         r=6: L-cycle for r <= L <= 60: True; locality: True; conjugator even for odd L: True
   long  mu=5      c=(1 2 3 4 5)        r=5: L-cycle for r <= L <= 60: True; locality: True; conjugator even for odd L: False
   long  mu=5      c=(1 2 3 5 6)        r=6: L-cycle for r <= L <= 60: True; locality: True; conjugator even for odd L: True
   long  mu=3.3    c=(1 2 3)(4 5 6)     r=6: L-cycle for r <= L <= 60: True; locality: True; conjugator even for odd L: True
   long  mu=4.2    c=(1 2 3 5)(4 6)     r=6: L-cycle for r <= L <= 60: True; locality: True; conjugator even for odd L: True
   small gadgets verified: 42 of 42; split tau with an odd conjugator: [('4.2', '5.3')] (not used: split types are covered by even long gadgets)
   partner witness mu=3, K=2^(n/2): local type of x c = 3.1: True
   partner witness mu=5, K=2^(n/2): local type of x c = 3.2.1: True
   partner witness mu=4.2, K=2^(n/2): local type of x c = 3.2.1: True
   partner witness mu=4.2, K=2^((n-1)/2).1: local type of x c = 3.2.1.1: True
   partner witness mu=4.2, K=3^(n/3): local type of x c = 5.1: True
   partner witness mu=4.2, K=3.1^(n-3): local type of x c = 4.3.2: True
   (ii),(iii): distinct odd parts <= 7 sum to at most 16 < 24; parts <= 5: at most 9
   Step 1 (24 <= n <= 40, five mu, 524900 even types): every type outside E(mu,n) has a gadget, no member of E has one; Step 2: partners even, non-split, distinct, outside E, with witnesses
   (2.0 s)
[6] Theorem C
   Lemma 5.5 (injection P; 3 <= l(P) <= (n-1)/2; l + l(P) <= n+1), odd 7 <= n <= 61: True
   Lemma 5.6 (z t and t z lie in the other class of n-cycles), odd 5 <= n <= 31: True
   n=7 (brute force over A_n): integral: True; Lemma 5.3: True (49 type pairs); Corollary 5.4: True; rule L in KC <=> l(K)+l(L) <= n+1 for K, L != 1: True; permutation of the proof valid: True
   n=9 (brute force over A_n): integral: True; Lemma 5.3: True (225 type pairs); Corollary 5.4: True; rule L in KC <=> l(K)+l(L) <= n+1 for K, L != 1: True; permutation of the proof valid: True
   Corollary 5.2, n=3: (lambda, nu) realised by x c0 (c0 an n-cycle) <=> l(lambda)+l(nu) <= n+1, same parity as n+1: True
   Corollary 5.2, n=4: (lambda, nu) realised by x c0 (c0 an n-cycle) <=> l(lambda)+l(nu) <= n+1, same parity as n+1: True
   Corollary 5.2, n=5: (lambda, nu) realised by x c0 (c0 an n-cycle) <=> l(lambda)+l(nu) <= n+1, same parity as n+1: True
   Corollary 5.2, n=6: (lambda, nu) realised by x c0 (c0 an n-cycle) <=> l(lambda)+l(nu) <= n+1, same parity as n+1: True
   Corollary 5.2, n=7: (lambda, nu) realised by x c0 (c0 an n-cycle) <=> l(lambda)+l(nu) <= n+1, same parity as n+1: True
   Corollary 5.2, n=8: (lambda, nu) realised by x c0 (c0 an n-cycle) <=> l(lambda)+l(nu) <= n+1, same parity as n+1: True
   Corollary 5.2, n=9: (lambda, nu) realised by x c0 (c0 an n-cycle) <=> l(lambda)+l(nu) <= n+1, same parity as n+1: True
   (8.5 s)
[7] numbers printed in the note
   k(A_n), 5 <= n <= 27: True [5, 7, 9, 14, 18, 24, 31, 43, 55, 72, 94, 123, 156, 200, 254, 324, 408, 513, 641, 804, 997, 1236, 1526]
   |class of n-cycles| = n!/(2n) < n!/(2(n-2)) = |class of type (n-2,1,1)|, odd 5 <= n <= 39: True
   (0.0 s)
TOTAL FAILS: 0   (total time 23.8 s)
