c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 0.6529 s
c decisions             : 42681          (65371 /sec)