c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 8.33073 s
c decisions             : 344873         (41398 /sec)