c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE c CPU time : 0.185971 s c decisions : 23344 (125525 /sec)