c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.132979 s c decisions : 16725 (125772 /sec)