unsat
(a0 a1 a2 a3 a4 a5 a6)
(b0 b1 b2 b3 b4 b5 b6 b7 b8 b9)