c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 0.726889 s
c decisions             : 44377          (61051 /sec)