c SATISFIABLE: No goal function specified.
s SATISFIABLE
c CPU time              : 1.19882 s
c decisions             : 154685         (129031 /sec)