c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 1.39579 s
c decisions             : 73662          (52775 /sec)