c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 56.5134 s
c decisions             : 1678445        (29700 /sec)