c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 2.76558 s
c decisions             : 130025         (47015 /sec)