c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 14.0229 s
c decisions             : 531982         (37937 /sec)