c [1mUNSATISFIABLE[0m s UNSATISFIABLE c CPU time : 0.419936 s c decisions : 26287 (62598 /sec)