c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 114.873 s
c decisions             : 3016247        (26257 /sec)