c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE c CPU time : 0.319951 s c decisions : 55394 (173133 /sec)