c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 0.777881 s
c decisions             : 43166          (55492 /sec)