c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 2.71359 s
c decisions             : 129525         (47732 /sec)