c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 319.73 s
c decisions             : 7321185        (22898 /sec)