c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 8.71068 s
c decisions             : 299027         (34329 /sec)