c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.52592 s c decisions : 61710 (117337 /sec)