c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 44602 s
c decisions             : 308207353      (6910 /sec)