c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 36.6284 s
c decisions             : 1257516        (34332 /sec)