c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.462929 s c decisions : 31668 (68408 /sec)