c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 878.587 s
c decisions             : 16222558       (18464 /sec)