c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 7.45887 s
c decisions             : 326453         (43767 /sec)