c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 682.051 s
c decisions             : 11735660       (17206 /sec)