c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 50.0934 s
c decisions             : 1563916        (31220 /sec)