c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 13.428 s
c decisions             : 493715         (36768 /sec)