c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 23.3544 s
c decisions             : 827878         (35448 /sec)