c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 19.73 s
c decisions             : 599355         (30378 /sec)