c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 28.3757 s
c decisions             : 817314         (28803 /sec)