c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 1.57276 s
c decisions             : 82959          (52747 /sec)