c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 69.3375 s
c decisions             : 1634570        (23574 /sec)