c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 953.152 s
c decisions             : 17127077       (17969 /sec)