c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 2510.2 s
c decisions             : 37625112       (14989 /sec)