unsat
(a0 a1 a2 a3 a4)
(b0 b1 b2 b3)