V1 n=4 k=2 b=2 vars=24 clauses=40 encode=0.0s solve=0.0s -> SAT (star-free exists)
V2 n=4 k=2 b=2 vars=36 clauses=40 encode=0.0s solve=0.0s -> SAT (star-free exists)
V1 n=5 k=2 b=2 vars=60 clauses=160 encode=0.0s solve=0.0s -> UNSAT (star forced)
V2 n=5 k=2 b=2 vars=90 clauses=160 encode=0.0s solve=0.0s -> UNSAT (star forced)
V1 n=6 k=3 b=2 vars=150 clauses=440 encode=0.0s solve=0.0s -> SAT (star-free exists)
V2 n=6 k=3 b=2 vars=240 clauses=440 encode=0.0s solve=0.0s -> SAT (star-free exists)
V1 n=7 k=3 b=2 vars=315 clauses=1435 encode=0.0s solve=0.0s -> UNSAT (star forced)
V2 n=7 k=3 b=2 vars=525 clauses=1435 encode=0.0s solve=0.0s -> UNSAT (star forced)
V1 n=6 k=2 b=3 vars=150 clauses=435 encode=0.0s solve=0.0s -> SAT (star-free exists)
V2 n=6 k=2 b=3 vars=210 clauses=435 encode=0.0s solve=0.0s -> SAT (star-free exists)
V1 n=7 k=2 b=3 vars=315 clauses=1190 encode=0.0s solve=0.0s -> UNSAT (star forced)
V2 n=7 k=2 b=3 vars=420 clauses=1400 encode=0.0s solve=0.0s -> UNSAT (star forced)
V1 n=8 k=4 b=2 vars=728 clauses=3696 encode=0.0s solve=0.0s -> SAT (star-free exists)
V2 n=8 k=4 b=2 vars=1288 clauses=3696 encode=0.0s solve=0.0s -> SAT (star-free exists)
V1 n=9 k=4 b=2 vars=1512 clauses=10794 encode=0.0s solve=0.0s -> UNSAT (star forced)
V2 n=9 k=4 b=2 vars=2772 clauses=10794 encode=0.0s solve=0.1s -> UNSAT (star forced)
V1 n=8 k=2 b=4 vars=728 clauses=2744 encode=0.0s solve=0.0s -> SAT (star-free exists)
V2 n=8 k=2 b=4 vars=896 clauses=3584 encode=0.0s solve=0.0s -> SAT (star-free exists)
V1 n=9 k=2 b=4 vars=1512 clauses=6930 encode=0.0s solve=1.7s -> UNSAT (star forced)
V2 n=9 k=2 b=4 vars=1764 clauses=10458 encode=0.0s solve=2.6s -> UNSAT (star forced)
V1 n=9 k=3 b=3 vars=1512 clauses=11970 encode=0.0s solve=0.0s -> SAT (star-free exists)
V2 n=9 k=3 b=3 vars=2268 clauses=15750 encode=0.0s solve=0.0s -> SAT (star-free exists)
V1 n=10 k=3 b=3 vars=2520 clauses=27510 encode=0.0s solve=9.8s -> UNSAT (star forced)
V2 n=10 k=3 b=3 vars=3780 clauses=38850 encode=0.0s solve=173.4s -> UNSAT (star forced)
V1 n=10 k=2 b=5 vars=3510 clauses=15690 encode=0.0s solve=0.0s -> SAT (star-free exists)
V2 n=10 k=2 b=5 vars=3870 clauses=25770 encode=0.0s solve=0.0s -> SAT (star-free exists)
V1 n=11 k=2 b=5 vars=7425 clauses=39567 encode=0.0s solve=1350.7s -> UNSAT (star forced)
# run stopped here by hand (V2 n=11 k=2 b=5 and the (10,5,2),(11,5,2) cases not run in this encoding): superseded by the proof of Theorem 1
