c [1mUNSATISFIABLE[0m s UNSATISFIABLE c CPU time : 0.009998 s c decisions : 437 (43709 /sec)