c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 453.31 s
c decisions             : 9851203        (21732 /sec)