c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.526919 s c decisions : 73702 (139873 /sec)