c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 9215.62 s
c decisions             : 84120732       (9128 /sec)