c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 4.06738 s
c decisions             : 180984         (44496 /sec)