MAYBE
MAYBE
TRS:
 {
                O(0()) -> 0(),
             +(x, 0()) -> x,
         +(x, +(y, z)) -> +(+(x, y), z),
             +(0(), x) -> x,
         +(O(x), O(y)) -> O(+(x, y)),
         +(O(x), I(y)) -> I(+(x, y)),
         +(I(x), O(y)) -> I(+(x, y)),
         +(I(x), I(y)) -> O(+(+(x, y), I(0()))),
             -(x, 0()) -> x,
             -(0(), x) -> 0(),
         -(O(x), O(y)) -> O(-(x, y)),
         -(O(x), I(y)) -> I(-(-(x, y), I(1()))),
         -(I(x), O(y)) -> I(-(x, y)),
         -(I(x), I(y)) -> O(-(x, y)),
          not(false()) -> true(),
           not(true()) -> false(),
       and(x, false()) -> false(),
        and(x, true()) -> x,
     if(false(), x, y) -> y,
      if(true(), x, y) -> x,
            ge(x, 0()) -> true(),
         ge(0(), O(x)) -> ge(0(), x),
         ge(0(), I(x)) -> false(),
        ge(O(x), O(y)) -> ge(x, y),
        ge(O(x), I(y)) -> not(ge(y, x)),
        ge(I(x), O(y)) -> ge(x, y),
        ge(I(x), I(y)) -> ge(x, y),
             Log'(0()) -> 0(),
            Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0()),
            Log'(I(x)) -> +(Log'(x), I(0())),
                Log(x) -> -(Log'(x), I(0())),
             Val(L(x)) -> x,
   Val(N(x, l(), r())) -> x,
             Min(L(x)) -> x,
   Min(N(x, l(), r())) -> Min(l()),
             Max(L(x)) -> x,
   Max(N(x, l(), r())) -> Max(r()),
              BS(L(x)) -> true(),
    BS(N(x, l(), r())) ->
  and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r()))),
            Size(L(x)) -> I(0()),
  Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1())),
              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()))
  )
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                  O(0()) -> 0(),
               +(x, 0()) -> x,
           +(x, +(y, z)) -> +(+(x, y), z),
               +(0(), x) -> x,
           +(O(x), O(y)) -> O(+(x, y)),
           +(O(x), I(y)) -> I(+(x, y)),
           +(I(x), O(y)) -> I(+(x, y)),
           +(I(x), I(y)) -> O(+(+(x, y), I(0()))),
               -(x, 0()) -> x,
               -(0(), x) -> 0(),
           -(O(x), O(y)) -> O(-(x, y)),
           -(O(x), I(y)) -> I(-(-(x, y), I(1()))),
           -(I(x), O(y)) -> I(-(x, y)),
           -(I(x), I(y)) -> O(-(x, y)),
            not(false()) -> true(),
             not(true()) -> false(),
         and(x, false()) -> false(),
          and(x, true()) -> x,
       if(false(), x, y) -> y,
        if(true(), x, y) -> x,
              ge(x, 0()) -> true(),
           ge(0(), O(x)) -> ge(0(), x),
           ge(0(), I(x)) -> false(),
          ge(O(x), O(y)) -> ge(x, y),
          ge(O(x), I(y)) -> not(ge(y, x)),
          ge(I(x), O(y)) -> ge(x, y),
          ge(I(x), I(y)) -> ge(x, y),
               Log'(0()) -> 0(),
              Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0()),
              Log'(I(x)) -> +(Log'(x), I(0())),
                  Log(x) -> -(Log'(x), I(0())),
               Val(L(x)) -> x,
     Val(N(x, l(), r())) -> x,
               Min(L(x)) -> x,
     Min(N(x, l(), r())) -> Min(l()),
               Max(L(x)) -> x,
     Max(N(x, l(), r())) -> Max(r()),
                BS(L(x)) -> true(),
      BS(N(x, l(), r())) ->
    and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r()))),
              Size(L(x)) -> I(0()),
    Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1())),
                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()))
    )
   }
  Fail