c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.19497 s c decisions : 25858 (132626 /sec)