c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 5787.24 s
c decisions             : 42075060       (7270 /sec)