K_3, b=2, N=5: vars=60 clauses=80 -> SAT (0.0s); decoded model re-checked: 2-iatlon, no constrained K_3
K_3, b=2, N=6: vars=120 clauses=220 -> UNSAT (0.0s)
   => p(K_3,2) = 6: CONFIRMED
