c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.45693 s c decisions : 57036 (124824 /sec)