c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE c CPU time : 0.313952 s c decisions : 47992 (152864 /sec)