c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 0.832873 s
c decisions             : 48824          (58621 /sec)