c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 8.38373 s
c decisions             : 305997         (36499 /sec)