c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 477.585 s
c decisions             : 11450859       (23977 /sec)