c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 86.5498 s
c decisions             : 2582856        (29842 /sec)