c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 1238.25 s
c decisions             : 15265782       (12328 /sec)