c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 1.2898 s
c decisions             : 69786          (54106 /sec)