c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 3.36549 s
c decisions             : 165372         (49138 /sec)