c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 12.2171 s
c decisions             : 484737         (39677 /sec)