c SATISFIABLE: No goal function specified. s SATISFIABLE c CPU time : 0.344947 s c decisions : 45883 (133015 /sec)