c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 8.5627 s
c decisions             : 310024         (36206 /sec)