c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 11.2083 s
c decisions             : 291825         (26037 /sec)