c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 14.2918 s
c decisions             : 500773         (35039 /sec)