c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 4287.9 s
c decisions             : 72485844       (16905 /sec)