K_(1,1), b=1, N=1: vars=0 clauses=0 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,1) present=False
K_(1,1), b=1, N=2: vars=3 clauses=5 -> UNSAT (0.0s)
   => p(K_(1,1),1) = 2: CONFIRMED
K_(1,2), b=1, N=2: vars=1 clauses=1 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,2) present=False
K_(1,2), b=1, N=3: vars=9 clauses=12 -> UNSAT (0.0s)
   => p(K_(1,2),1) = 3: CONFIRMED
K_(1,3), b=1, N=3: vars=3 clauses=3 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,3) present=False
K_(1,3), b=1, N=4: vars=18 clauses=22 -> UNSAT (0.0s)
   => p(K_(1,3),1) = 4: CONFIRMED
K_(1,1), b=2, N=2: vars=2 clauses=2 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,1) present=False
K_(1,1), b=2, N=3: vars=9 clauses=13 -> UNSAT (0.0s)
   => p(K_(1,1),2) = 3: CONFIRMED
K_(1,1), b=3, N=3: vars=6 clauses=6 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,1) present=False
K_(1,1), b=3, N=4: vars=18 clauses=25 -> UNSAT (0.0s)
   => p(K_(1,1),3) = 4: CONFIRMED
K_(1,2), b=2, N=4: vars=36 clauses=40 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,2) present=False
K_(1,2), b=2, N=5: vars=90 clauses=160 -> UNSAT (0.0s)
   => p(K_(1,2),2) = 5: CONFIRMED
K_(1,3), b=2, N=6: vars=240 clauses=440 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,3) present=False
K_(1,3), b=2, N=7: vars=525 clauses=1435 -> UNSAT (0.0s)
   => p(K_(1,3),2) = 7: CONFIRMED
K_(1,2), b=3, N=6: vars=210 clauses=435 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,2) present=False
K_(1,2), b=3, N=7: vars=420 clauses=1400 -> UNSAT (0.0s)
   => p(K_(1,2),3) = 7: CONFIRMED
K_(1,4), b=2, N=8: vars=1288 clauses=3696 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,4) present=False
K_(1,4), b=2, N=9: vars=2772 clauses=10794 -> UNSAT (0.1s)
   => p(K_(1,4),2) = 9: CONFIRMED
K_(1,2), b=4, N=8: vars=896 clauses=3584 -> SAT (0.0s); decoded model re-checked: b-iatlon=True, constrained K_(1,2) present=False
K_(1,2), b=4, N=9: vars=1764 clauses=10458 -> UNSAT (9.0s)
   => p(K_(1,2),4) = 9: CONFIRMED
K_(1,3), b=3, N=9: vars=2268 clauses=15750 -> SAT (0.1s); decoded model re-checked: b-iatlon=True, constrained K_(1,3) present=False
K_(1,3), b=3, N=10: vars=3780 clauses=38850 -> UNSAT (697.5s)
   => p(K_(1,3),3) = 10: CONFIRMED
K_(1,5), b=2, N=10: vars=6660 clauses=26580 -> SAT (0.1s); decoded model re-checked: b-iatlon=True, constrained K_(1,5) present=False
K_(1,5), b=2, N=11: vars=14355 clauses=72237 -> UNSAT (30.8s)
   => p(K_(1,5),2) = 11: CONFIRMED
K_(1,2), b=5, N=10: vars=3870 clauses=25770 -> SAT (0.1s); decoded model re-checked: b-iatlon=True, constrained K_(1,2) present=False
python3 run2_iatlon_sat.py  1117.29s user 10.33s system 57% cpu 32:58.05 total
[note added by hand 2026-09-30T10:05:03Z] run stopped by hand during (k,b)=(2,5), N=11 (unbroken encoding, >20 min); that case and the N=13 cases (6,2),(2,6),(4,3),(3,4) were run separately with a valid symmetry break: see run2_iatlon_sat_single_*_out.txt
