c [1mUNSATISFIABLE[0m s UNSATISFIABLE c CPU time : 0.148977 s c decisions : 11746 (78844 /sec)