Part S1: counterexamples to Theorem 2.2 among all monotone graph systems
  sanity n=4 k=2 without the no-star clauses: SAT (as expected)
  sanity n=6 k=3 without the no-star clauses: SAT (as expected)
  sanity n=8 k=4 without the no-star clauses: SAT (as expected)
  n=2 k=1: UNSAT  (4 clauses, 1 partitions, 0.0s)
  n=3 k=1: UNSAT  (14 clauses, 1 partitions, 0.0s)
  n=3 k=2: UNSAT  (14 clauses, 4 partitions, 0.0s)
  n=4 k=1: UNSAT  (48 clauses, 1 partitions, 0.0s)
  n=4 k=2: UNSAT  (55 clauses, 8 partitions, 0.0s)
  n=4 k=3: UNSAT  (53 clauses, 14 partitions, 0.0s)
  n=5 k=1: UNSAT  (167 clauses, 1 partitions, 0.0s)
  n=5 k=2: UNSAT  (192 clauses, 16 partitions, 0.0s)
  n=5 k=3: UNSAT  (207 clauses, 41 partitions, 0.0s)
  n=5 k=4: UNSAT  (202 clauses, 51 partitions, 0.0s)
  n=6 k=1: UNSAT  (568 clauses, 1 partitions, 0.0s)
  n=6 k=2: UNSAT  (629 clauses, 32 partitions, 0.0s)
  n=6 k=3: UNSAT  (719 clauses, 122 partitions, 0.0s)
  n=6 k=4: UNSAT  (754 clauses, 187 partitions, 0.0s)
  n=6 k=5: UNSAT  (745 clauses, 202 partitions, 0.0s)
  n=7 k=1: UNSAT  (1843 clauses, 1 partitions, 0.0s)
  n=7 k=2: UNSAT  (1969 clauses, 64 partitions, 0.0s)
  n=7 k=3: UNSAT  (2305 clauses, 365 partitions, 0.0s)
  n=7 k=4: UNSAT  (2620 clauses, 715 partitions, 0.0s)
  n=7 k=5: UNSAT  (2697 clauses, 855 partitions, 0.0s)
  n=7 k=6: UNSAT  (2683 clauses, 876 partitions, 0.0s)
  n=8 k=1: UNSAT  (5680 clauses, 1 partitions, 0.0s)
  n=8 k=2: UNSAT  (5919 clauses, 128 partitions, 0.3s)
  n=8 k=3: UNSAT  (6997 clauses, 1094 partitions, 1.1s)
  n=8 k=4: UNSAT  (8698 clauses, 2795 partitions, 0.1s)
  n=8 k=5: UNSAT  (9636 clauses, 3845 partitions, 0.0s)
  n=8 k=6: UNSAT  (9790 clauses, 4111 partitions, 0.0s)
  n=8 k=7: UNSAT  (9770 clauses, 4139 partitions, 0.0s)
Part S2: Patak's b-iatlon graphs, constrained K_{1,k}
  k=1 b=3 n=3: SAT (star-free b-iatlon graph exists)  (6 clauses, 0.0s)
  k=1 b=3 n=4: UNSAT (constrained K_1,k forced)  (25 clauses, 0.0s)
  k=2 b=2 n=4: SAT (star-free b-iatlon graph exists)  (40 clauses, 0.0s)
  k=2 b=2 n=5: UNSAT (constrained K_1,k forced)  (160 clauses, 0.0s)
  k=3 b=2 n=6: SAT (star-free b-iatlon graph exists)  (440 clauses, 0.0s)
  k=3 b=2 n=7: UNSAT (constrained K_1,k forced)  (1435 clauses, 0.0s)
  k=2 b=3 n=6: SAT (star-free b-iatlon graph exists)  (435 clauses, 0.0s)
  k=2 b=3 n=7: UNSAT (constrained K_1,k forced)  (1400 clauses, 0.0s)
  k=4 b=2 n=8: SAT (star-free b-iatlon graph exists)  (3696 clauses, 0.0s)
  k=4 b=2 n=9: UNSAT (constrained K_1,k forced)  (10794 clauses, 0.3s)
  k=2 b=4 n=8: SAT (star-free b-iatlon graph exists)  (3584 clauses, 0.0s)
  k=2 b=4 n=9: UNSAT (constrained K_1,k forced)  (10458 clauses, 5.8s)
  k=3 b=3 n=9: SAT (star-free b-iatlon graph exists)  (15750 clauses, 0.1s)
  k=3 b=3 n=10: UNSAT (constrained K_1,k forced)  (38850 clauses, 463.3s)
Part S3: constrained K_3 in 2-iatlon graphs
  n=5: SAT (no constrained K_3 possible)  (80 clauses)
  n=6: UNSAT (constrained K_3 forced)  (220 clauses)
all SAT checks as expected
exit 0
