c [1mUNSATISFIABLE[0m s UNSATISFIABLE c CPU time : 0.281957 s c decisions : 19492 (69131 /sec)