c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 13.9599 s
c decisions             : 523177         (37477 /sec)