c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 35972.7 s
c decisions             : 206761052      (5748 /sec)