c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 8672.33 s
c decisions             : 119557049      (13786 /sec)