c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 0.610907 s
c decisions             : 39217          (64195 /sec)