c [1mUNSATISFIABLE[0m
s UNSATISFIABLE
c CPU time              : 95.9434 s
c decisions             : 2525117        (26319 /sec)