c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 15.4397 s
c decisions             : 536265         (34733 /sec)