c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE c CPU time : 0.142978 s c decisions : 18330 (128202 /sec)