c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 2.67259 s
c decisions             : 114362         (42791 /sec)