c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 2.10668 s
c decisions             : 95446          (45306 /sec)