c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.52492 s c decisions : 104013 (198150 /sec)