c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 6.18506 s
c decisions             : 281097         (45448 /sec)