K_(1,2), b=5, N=11 (symmetry-broken, cadical195): vars=7920 clauses=70272 -> UNSAT (161.5s)
