c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 9.59954 s
c decisions             : 404339         (42121 /sec)