c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 21.9477 s
c decisions             : 767819         (34984 /sec)