c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 117.473 s
c decisions             : 3151761        (26830 /sec)