c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 12.5901 s
c decisions             : 481998         (38284 /sec)