c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 1.77673 s
c decisions             : 81492          (45866 /sec)