c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE c CPU time : 0.45693 s c decisions : 50352 (110196 /sec)