c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 89.2074 s
c decisions             : 2883193        (32320 /sec)