c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 1.14183 s
c decisions             : 61340          (53721 /sec)