c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 25.6371 s
c decisions             : 742520         (28963 /sec)