c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 1795.42 s
c decisions             : 28775466       (16027 /sec)