c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.279957 s c decisions : 37836 (135149 /sec)