c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 188.784 s
c decisions             : 2725805        (14439 /sec)