c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 7.06693 s
c decisions             : 281230         (39795 /sec)