c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 67.5297 s
c decisions             : 1886420        (27935 /sec)