c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 17.4453 s
c decisions             : 641743         (36786 /sec)