c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.536918 s c decisions : 71523 (133210 /sec)