c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 0.605907 s
c decisions             : 39057          (64460 /sec)