c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.595909 s c decisions : 113414 (190321 /sec)