c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 97.3452 s
c decisions             : 2512753        (25813 /sec)