c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 40.0979 s
c decisions             : 1192015        (29728 /sec)