c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 2.82657 s
c decisions             : 128299         (45390 /sec)