c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 5.75712 s
c decisions             : 270621         (47006 /sec)