c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 2.05369 s
c decisions             : 225195         (109654 /sec)