c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 0.972852 s
c decisions             : 129946         (133572 /sec)