c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 22.2246 s
c decisions             : 588353         (26473 /sec)