c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 143.797 s
c decisions             : 3881022        (26990 /sec)