MAYBE
Trs:
 {        not(false()) -> true(),
           not(true()) -> false(),
                O(0()) -> 0(),
                Log(x) -> -(Log'(x), I(0())),
            Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0()),
             Log'(0()) -> 0(),
            Log'(I(x)) -> +(Log'(x), I(0())),
             Val(L(x)) -> x,
   Val(N(x, l(), r())) -> x,
              BS(L(x)) -> true(),
    BS(N(x, l(), r())) -> and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r()))),
             Min(L(x)) -> x,
   Min(N(x, l(), r())) -> Min(l()),
             Max(L(x)) -> x,
   Max(N(x, l(), r())) -> Max(r()),
         +(O(x), O(y)) -> O(+(x, y)),
         +(O(x), I(y)) -> I(+(x, y)),
             +(0(), x) -> x,
         +(I(x), O(y)) -> I(+(x, y)),
         +(I(x), I(y)) -> O(+(+(x, y), I(0()))),
         +(x, +(y, z)) -> +(+(x, y), z),
             +(x, 0()) -> x,
              WB(L(x)) -> true(),
    WB(N(x, l(), r())) -> and(if(ge(Size(l()), Size(r())), ge(I(0()), -(Size(l()), Size(r()))), ge(I(0()), -(Size(r()), Size(l())))), and(WB(l()), WB(r()))),
         -(O(x), O(y)) -> O(-(x, y)),
         -(O(x), I(y)) -> I(-(-(x, y), I(1()))),
             -(0(), x) -> 0(),
         -(I(x), O(y)) -> I(-(x, y)),
         -(I(x), I(y)) -> O(-(x, y)),
             -(x, 0()) -> x,
            Size(L(x)) -> I(0()),
  Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1())),
        ge(O(x), O(y)) -> ge(x, y),
        ge(O(x), I(y)) -> not(ge(y, x)),
         ge(0(), O(x)) -> ge(0(), x),
         ge(0(), I(x)) -> false(),
        ge(I(x), O(y)) -> ge(x, y),
        ge(I(x), I(y)) -> ge(x, y),
            ge(x, 0()) -> true(),
     if(false(), x, y) -> y,
      if(true(), x, y) -> x,
       and(x, false()) -> false(),
        and(x, true()) -> x}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open