c [1mUNSATISFIABLE[0m s UNSATISFIABLE c CPU time : 0.007998 s c decisions : 416 (52013 /sec)