c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 3998.98 s
c decisions             : 36948947       (9240 /sec)