c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 100295 s
c decisions             : 456359478      (4550 /sec)