c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 7.17291 s
c decisions             : 271707         (37880 /sec)