c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 53.0779 s
c decisions             : 1495097        (28168 /sec)