c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE c CPU time : 0.146977 s c decisions : 13976 (95090 /sec)