c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 2.51162 s
c decisions             : 115424         (45956 /sec)