sanity colour n=3 no good 3-star, not 2-colourable: SAT (as expected)
sanity colour n=4 no good 4-star, not 3-colourable: SAT (as expected)
sanity colour n=5 no good 3-star, not 2-colourable: SAT (as expected)
sanity colour n=6 no good 3-star, not 2-colourable: SAT (as expected)
sanity alpha n=4=k*a (k=2, a=2): SAT (as expected)
sanity alpha n=6=k*a (k=3, a=2): SAT (as expected)
sanity alpha n=6=k*a (k=2, a=3): SAT (as expected)
sanity alpha n=9=k*a (k=3, a=3): SAT (as expected)
mode colour: counterexample to Theorem 2.2 on n points for k (k < n)
colour n=2 k=1: vars=1 clauses=3 partitions=1 -> UNSAT (0.0s)
colour n=3 k=1: vars=6 clauses=10 partitions=1 -> UNSAT (0.0s)
colour n=3 k=2: vars=6 clauses=10 partitions=4 -> UNSAT (0.0s)
colour n=4 k=1: vars=24 clauses=37 partitions=1 -> UNSAT (0.0s)
colour n=4 k=2: vars=24 clauses=44 partitions=8 -> UNSAT (0.0s)
colour n=4 k=3: vars=24 clauses=42 partitions=14 -> UNSAT (0.0s)
colour n=5 k=1: vars=80 clauses=141 partitions=1 -> UNSAT (0.0s)
colour n=5 k=2: vars=80 clauses=166 partitions=16 -> UNSAT (0.0s)
colour n=5 k=3: vars=80 clauses=181 partitions=41 -> UNSAT (0.0s)
colour n=5 k=4: vars=80 clauses=176 partitions=51 -> UNSAT (0.0s)
colour n=6 k=1: vars=240 clauses=511 partitions=1 -> UNSAT (0.0s)
colour n=6 k=2: vars=240 clauses=572 partitions=32 -> UNSAT (0.0s)
colour n=6 k=3: vars=240 clauses=662 partitions=122 -> UNSAT (0.0s)
colour n=6 k=4: vars=240 clauses=697 partitions=187 -> UNSAT (0.0s)
colour n=6 k=5: vars=240 clauses=688 partitions=202 -> UNSAT (0.0s)
colour n=7 k=1: vars=672 clauses=1723 partitions=1 -> UNSAT (0.0s)
colour n=7 k=2: vars=672 clauses=1849 partitions=64 -> UNSAT (0.0s)
colour n=7 k=3: vars=672 clauses=2185 partitions=365 -> UNSAT (0.0s)
colour n=7 k=4: vars=672 clauses=2500 partitions=715 -> UNSAT (0.0s)
colour n=7 k=5: vars=672 clauses=2577 partitions=855 -> UNSAT (0.0s)
colour n=7 k=6: vars=672 clauses=2563 partitions=876 -> UNSAT (0.0s)
colour n=8 k=1: vars=1792 clauses=5433 partitions=1 -> UNSAT (0.0s)
colour n=8 k=2: vars=1792 clauses=5672 partitions=128 -> UNSAT (0.7s)
colour n=8 k=3: vars=1792 clauses=6750 partitions=1094 -> UNSAT (1.0s)
colour n=8 k=4: vars=1792 clauses=8451 partitions=2795 -> UNSAT (0.1s)
colour n=8 k=5: vars=1792 clauses=9389 partitions=3845 -> UNSAT (0.1s)
colour n=8 k=6: vars=1792 clauses=9543 partitions=4111 -> UNSAT (0.1s)
colour n=8 k=7: vars=1792 clauses=9523 partitions=4139 -> UNSAT (0.1s)
colour n=9 k=1: vars=4608 clauses=16201 partitions=1 -> UNSAT (0.0s)
colour n=9 k=2: vars=4608 clauses=16636 partitions=256 -> UNSAT (48.1s)
colour n=9 k=3: vars=4608 clauses=19913 partitions=3281 -> UNSAT (145.3s)
colour n=9 k=4: vars=4608 clauses=27809 partitions=11051 -> UNSAT (8.7s)
colour n=9 k=5: vars=4608 clauses=34634 partitions=18002 -> UNSAT (0.4s)
mode alpha: n = k*a+1 points, no good k-star, alpha <= a
alpha k=2 a=2 n=5: vars=80 clauses=160 -> UNSAT (0.0s)
alpha k=3 a=2 n=7: vars=672 clauses=1855 -> UNSAT (0.0s)
alpha k=2 a=3 n=7: vars=672 clauses=1820 -> UNSAT (0.0s)
alpha k=4 a=2 n=9: vars=4608 clauses=16842 -> UNSAT (0.2s)
alpha k=2 a=4 n=9: vars=4608 clauses=16506 -> UNSAT (9.4s)
alpha k=3 a=3 n=10: vars=11520 clauses=47130 -> UNSAT (667.7s)
alpha k=5 a=2 n=11: vars=28160 clauses=129657 -> UNSAT (35.7s)
[note added by hand 2026-09-30T10:36:58Z] run stopped by hand during alpha k=2 a=5 n=11 (~50 min without result); the remaining alpha case (4,3) n=13 was not run. All claims of the paper are covered by the completed cases above and by run2_colouring_sat_n9_k678_out.txt.
