c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 3.9334 s
c decisions             : 165069         (41966 /sec)