c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 1.84872 s
c decisions             : 121283         (65604 /sec)