c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 379.028 s
c decisions             : 7802556        (20586 /sec)