c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.043993 s c decisions : 4599 (104539 /sec)