c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 1634.61 s
c decisions             : 23563580       (14415 /sec)