c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 2.19867 s
c decisions             : 98706          (44894 /sec)