c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 1.41678 s
c decisions             : 121639         (85856 /sec)