c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.45393 s c decisions : 63203 (139235 /sec)