Part A: Theorem 2.2 by brute force
  n=4: all 46656 monotone graph systems (6 up-sets per pair), every k: no good k-star => covered by k independent sets  [5.8s]
        (systems/k with a good k-star and no k-colouring: 47879; with a good k-star and a k-colouring: 41855)
  n=5: 20000 random monotone graph systems, every k: implication holds  [9.4s]
  n=6: 3000 random monotone graph systems, every k: implication holds  [3.3s]
  n=7: 300 random monotone graph systems, every k: implication holds  [0.8s]
Part B: p(K_3,2) = 6
  certificate C_5: 2-iatlon = True, triangle-free = True
  n=5: 59049 choice functions, 2124 without a constrained K_3 (brute force)
  n=5: backtracking search: 2124 choice functions without a constrained K_3 (8678 nodes, 0.1s)
  n=6: backtracking search: 0 choice functions without a constrained K_3 (815671 nodes, 18.7s)
  => every 2-iatlon graph on 6 vertices contains a constrained K_3 (reduction to choice functions: Lemma 3.2(c)), and the certificate shows 5 vertices do not suffice.
Part C: Theorem 3.3 on random b-iatlon choice functions with kb+1 vertices
  (k,b)=(2,2), n=kb+1=5: 300 random 2-iatlon choice functions, a verified constrained K_1,2 every time
  (k,b)=(3,2), n=kb+1=7: 300 random 2-iatlon choice functions, a verified constrained K_1,3 every time
  (k,b)=(2,3), n=kb+1=7: 300 random 3-iatlon choice functions, a verified constrained K_1,2 every time
  (k,b)=(4,2), n=kb+1=9: 200 random 2-iatlon choice functions, a verified constrained K_1,4 every time
  (k,b)=(3,3), n=kb+1=10: 100 random 3-iatlon choice functions, a verified constrained K_1,3 every time
  (k,b)=(2,5), n=kb+1=11: 100 random 5-iatlon choice functions, a verified constrained K_1,2 every time
  (k,b)=(5,2), n=kb+1=11: 100 random 2-iatlon choice functions, a verified constrained K_1,5 every time
Part D: arithmetic of the bounds
  K_2: ours vs Patak  b=1: 2 vs 2; b=2: 3 vs 3; b=3: 4 vs 4; b=4: 5 vs 5; b=10: 11 vs 11
  K_3: ours vs Patak  b=1: 3 vs 3; b=2: 7 vs 9; b=3: 13 vs 22; b=4: 21 vs 45; b=10: 111 vs 561
  K_4: ours vs Patak  b=1: 4 vs 4; b=2: 15 vs 27; b=3: 40 vs 130; b=4: 85 vs 445; b=10: 1111 vs 30811
  K_5: ours vs Patak  b=1: 5 vs 5; b=2: 31 vs 81; b=3: 121 vs 778; b=4: 341 vs 4445; b=10: 11111 vs 1694561
  recursions: p(K_n,b) <= sum_{j<n} b^j, p(K_{3,3},b) <= 3b^3+b^2+b+1, p((g+1)K_{3,3},b) <= 3b^3+b^2+b+1+g(9b-3): arithmetic checked for b<=7, g<=4
  R^d (d=2): ours sum_(j<=4) b^j at b=2: 31; Patak b*S_3+1 at b=2: 81
all checks passed  [41s]
python3 check_theorem.py  14.84s user 0.15s system 36% cpu 40.743 total
