c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.156976 s c decisions : 24162 (153922 /sec)