c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 747.287 s
c decisions             : 13847264       (18530 /sec)