c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 1.69774 s
c decisions             : 83375          (49109 /sec)