c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 6.14706 s
c decisions             : 250161         (40696 /sec)