c UNSATISFIABLE
s UNSATISFIABLE
c CPU time              : 4.08538 s
c decisions             : 137292         (33606 /sec)