c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 19.0051 s
c decisions             : 639594         (33654 /sec)