c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 16.7754 s
c decisions             : 710292         (42341 /sec)