c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 271.195 s
c decisions             : 5567422        (20529 /sec)