c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.510922 s c decisions : 48799 (95512 /sec)