MAYBE

Problem:
 O(0()) -> 0()
 +(0(),x) -> x
 +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z)
 -(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(true()) -> false()
 not(false()) -> true()
 and(x,true()) -> x
 and(x,false()) -> false()
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 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)
 ge(x,0()) -> true()
 ge(0(),O(x)) -> ge(0(),x)
 ge(0(),I(x)) -> false()
 Log'(0()) -> 0()
 Log'(I(x)) -> +(Log'(x),I(0()))
 Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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())))

Proof:
 DP Processor:
  DPs:
   +#(O(x),O(y)) -> +#(x,y)
   +#(O(x),O(y)) -> O#(+(x,y))
   +#(O(x),I(y)) -> +#(x,y)
   +#(I(x),O(y)) -> +#(x,y)
   +#(I(x),I(y)) -> +#(x,y)
   +#(I(x),I(y)) -> +#(+(x,y),I(0()))
   +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
   +#(x,+(y,z)) -> +#(x,y)
   +#(x,+(y,z)) -> +#(+(x,y),z)
   -#(O(x),O(y)) -> -#(x,y)
   -#(O(x),O(y)) -> O#(-(x,y))
   -#(O(x),I(y)) -> -#(x,y)
   -#(O(x),I(y)) -> -#(-(x,y),I(1()))
   -#(I(x),O(y)) -> -#(x,y)
   -#(I(x),I(y)) -> -#(x,y)
   -#(I(x),I(y)) -> O#(-(x,y))
   ge#(O(x),O(y)) -> ge#(x,y)
   ge#(O(x),I(y)) -> ge#(y,x)
   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)
   ge#(0(),O(x)) -> ge#(0(),x)
   Log'#(I(x)) -> Log'#(x)
   Log'#(I(x)) -> +#(Log'(x),I(0()))
   Log'#(O(x)) -> Log'#(x)
   Log'#(O(x)) -> +#(Log'(x),I(0()))
   Log'#(O(x)) -> ge#(x,I(0()))
   Log'#(O(x)) -> if#(ge(x,I(0())),+(Log'(x),I(0())),0())
   Log#(x) -> Log'#(x)
   Log#(x) -> -#(Log'(x),I(0()))
   Min#(N(x,l(),r())) -> Min#(l())
   Max#(N(x,l(),r())) -> Max#(r())
   BS#(N(x,l(),r())) -> BS#(r())
   BS#(N(x,l(),r())) -> BS#(l())
   BS#(N(x,l(),r())) -> and#(BS(l()),BS(r()))
   BS#(N(x,l(),r())) -> Min#(r())
   BS#(N(x,l(),r())) -> ge#(Min(r()),x)
   BS#(N(x,l(),r())) -> Max#(l())
   BS#(N(x,l(),r())) -> ge#(x,Max(l()))
   BS#(N(x,l(),r())) -> and#(ge(x,Max(l())),ge(Min(r()),x))
   BS#(N(x,l(),r())) -> and#(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
   Size#(N(x,l(),r())) -> Size#(r())
   Size#(N(x,l(),r())) -> Size#(l())
   Size#(N(x,l(),r())) -> +#(Size(l()),Size(r()))
   Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1()))
   WB#(N(x,l(),r())) -> WB#(r())
   WB#(N(x,l(),r())) -> WB#(l())
   WB#(N(x,l(),r())) -> and#(WB(l()),WB(r()))
   WB#(N(x,l(),r())) -> -#(Size(r()),Size(l()))
   WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l())))
   WB#(N(x,l(),r())) -> -#(Size(l()),Size(r()))
   WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r())))
   WB#(N(x,l(),r())) -> Size#(r())
   WB#(N(x,l(),r())) -> Size#(l())
   WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r()))
   WB#(N(x,l(),r())) ->
   if#(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))),ge(I(0()),-(Size(r()),Size(l()))))
   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())))
  TRS:
   O(0()) -> 0()
   +(0(),x) -> x
   +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z)
   -(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(true()) -> false()
   not(false()) -> true()
   and(x,true()) -> x
   and(x,false()) -> false()
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   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)
   ge(x,0()) -> true()
   ge(0(),O(x)) -> ge(0(),x)
   ge(0(),I(x)) -> false()
   Log'(0()) -> 0()
   Log'(I(x)) -> +(Log'(x),I(0()))
   Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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())))
  CDG Processor:
   DPs:
    +#(O(x),O(y)) -> +#(x,y)
    +#(O(x),O(y)) -> O#(+(x,y))
    +#(O(x),I(y)) -> +#(x,y)
    +#(I(x),O(y)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    +#(x,+(y,z)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z)
    -#(O(x),O(y)) -> -#(x,y)
    -#(O(x),O(y)) -> O#(-(x,y))
    -#(O(x),I(y)) -> -#(x,y)
    -#(O(x),I(y)) -> -#(-(x,y),I(1()))
    -#(I(x),O(y)) -> -#(x,y)
    -#(I(x),I(y)) -> -#(x,y)
    -#(I(x),I(y)) -> O#(-(x,y))
    ge#(O(x),O(y)) -> ge#(x,y)
    ge#(O(x),I(y)) -> ge#(y,x)
    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)
    ge#(0(),O(x)) -> ge#(0(),x)
    Log'#(I(x)) -> Log'#(x)
    Log'#(I(x)) -> +#(Log'(x),I(0()))
    Log'#(O(x)) -> Log'#(x)
    Log'#(O(x)) -> +#(Log'(x),I(0()))
    Log'#(O(x)) -> ge#(x,I(0()))
    Log'#(O(x)) -> if#(ge(x,I(0())),+(Log'(x),I(0())),0())
    Log#(x) -> Log'#(x)
    Log#(x) -> -#(Log'(x),I(0()))
    Min#(N(x,l(),r())) -> Min#(l())
    Max#(N(x,l(),r())) -> Max#(r())
    BS#(N(x,l(),r())) -> BS#(r())
    BS#(N(x,l(),r())) -> BS#(l())
    BS#(N(x,l(),r())) -> and#(BS(l()),BS(r()))
    BS#(N(x,l(),r())) -> Min#(r())
    BS#(N(x,l(),r())) -> ge#(Min(r()),x)
    BS#(N(x,l(),r())) -> Max#(l())
    BS#(N(x,l(),r())) -> ge#(x,Max(l()))
    BS#(N(x,l(),r())) -> and#(ge(x,Max(l())),ge(Min(r()),x))
    BS#(N(x,l(),r())) -> and#(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
    Size#(N(x,l(),r())) -> Size#(r())
    Size#(N(x,l(),r())) -> Size#(l())
    Size#(N(x,l(),r())) -> +#(Size(l()),Size(r()))
    Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1()))
    WB#(N(x,l(),r())) -> WB#(r())
    WB#(N(x,l(),r())) -> WB#(l())
    WB#(N(x,l(),r())) -> and#(WB(l()),WB(r()))
    WB#(N(x,l(),r())) -> -#(Size(r()),Size(l()))
    WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l())))
    WB#(N(x,l(),r())) -> -#(Size(l()),Size(r()))
    WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r())))
    WB#(N(x,l(),r())) -> Size#(r())
    WB#(N(x,l(),r())) -> Size#(l())
    WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r()))
    WB#(N(x,l(),r())) ->
    if#(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))),ge(I(0()),-(Size(r()),Size(l()))))
    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())))
   TRS:
    O(0()) -> 0()
    +(0(),x) -> x
    +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z)
    -(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(true()) -> false()
    not(false()) -> true()
    and(x,true()) -> x
    and(x,false()) -> false()
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    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)
    ge(x,0()) -> true()
    ge(0(),O(x)) -> ge(0(),x)
    ge(0(),I(x)) -> false()
    Log'(0()) -> 0()
    Log'(I(x)) -> +(Log'(x),I(0()))
    Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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())))
   graph:
    Log#(x) -> Log'#(x) -> Log'#(I(x)) -> Log'#(x)
    Log#(x) -> Log'#(x) -> Log'#(I(x)) -> +#(Log'(x),I(0()))
    Log#(x) -> Log'#(x) -> Log'#(O(x)) -> Log'#(x)
    Log#(x) -> Log'#(x) -> Log'#(O(x)) -> +#(Log'(x),I(0()))
    Log#(x) -> Log'#(x) -> Log'#(O(x)) -> ge#(x,I(0()))
    Log#(x) -> Log'#(x) ->
    Log'#(O(x)) -> if#(ge(x,I(0())),+(Log'(x),I(0())),0())
    Log#(x) -> -#(Log'(x),I(0())) -> -#(O(x),I(y)) -> -#(x,y)
    Log#(x) -> -#(Log'(x),I(0())) ->
    -#(O(x),I(y)) -> -#(-(x,y),I(1()))
    Log#(x) -> -#(Log'(x),I(0())) -> -#(I(x),I(y)) -> -#(x,y)
    Log#(x) -> -#(Log'(x),I(0())) -> -#(I(x),I(y)) -> O#(-(x,y))
    Log'#(I(x)) -> Log'#(x) -> Log'#(I(x)) -> Log'#(x)
    Log'#(I(x)) -> Log'#(x) -> Log'#(I(x)) -> +#(Log'(x),I(0()))
    Log'#(I(x)) -> Log'#(x) -> Log'#(O(x)) -> Log'#(x)
    Log'#(I(x)) -> Log'#(x) -> Log'#(O(x)) -> +#(Log'(x),I(0()))
    Log'#(I(x)) -> Log'#(x) -> Log'#(O(x)) -> ge#(x,I(0()))
    Log'#(I(x)) -> Log'#(x) ->
    Log'#(O(x)) -> if#(ge(x,I(0())),+(Log'(x),I(0())),0())
    Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(O(x),I(y)) -> +#(x,y)
    Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(I(x),I(y)) -> +#(x,y)
    Log'#(I(x)) -> +#(Log'(x),I(0())) ->
    +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    Log'#(I(x)) -> +#(Log'(x),I(0())) ->
    +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    Log'#(O(x)) -> Log'#(x) -> Log'#(I(x)) -> Log'#(x)
    Log'#(O(x)) -> Log'#(x) -> Log'#(I(x)) -> +#(Log'(x),I(0()))
    Log'#(O(x)) -> Log'#(x) -> Log'#(O(x)) -> Log'#(x)
    Log'#(O(x)) -> Log'#(x) -> Log'#(O(x)) -> +#(Log'(x),I(0()))
    Log'#(O(x)) -> Log'#(x) -> Log'#(O(x)) -> ge#(x,I(0()))
    Log'#(O(x)) -> Log'#(x) ->
    Log'#(O(x)) -> if#(ge(x,I(0())),+(Log'(x),I(0())),0())
    Log'#(O(x)) -> ge#(x,I(0())) -> ge#(O(x),I(y)) -> ge#(y,x)
    Log'#(O(x)) -> ge#(x,I(0())) -> ge#(O(x),I(y)) -> not#(ge(y,x))
    Log'#(O(x)) -> ge#(x,I(0())) -> ge#(I(x),I(y)) -> ge#(x,y)
    Log'#(O(x)) -> +#(Log'(x),I(0())) -> +#(O(x),I(y)) -> +#(x,y)
    Log'#(O(x)) -> +#(Log'(x),I(0())) -> +#(I(x),I(y)) -> +#(x,y)
    Log'#(O(x)) -> +#(Log'(x),I(0())) ->
    +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    Log'#(O(x)) -> +#(Log'(x),I(0())) ->
    +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    ge#(I(x),I(y)) -> ge#(x,y) -> ge#(O(x),O(y)) -> ge#(x,y)
    ge#(I(x),I(y)) -> ge#(x,y) -> ge#(O(x),I(y)) -> ge#(y,x)
    ge#(I(x),I(y)) -> ge#(x,y) -> ge#(O(x),I(y)) -> not#(ge(y,x))
    ge#(I(x),I(y)) -> ge#(x,y) -> ge#(I(x),O(y)) -> ge#(x,y)
    ge#(I(x),I(y)) -> ge#(x,y) -> ge#(I(x),I(y)) -> ge#(x,y)
    ge#(I(x),I(y)) -> ge#(x,y) -> ge#(0(),O(x)) -> ge#(0(),x)
    ge#(I(x),O(y)) -> ge#(x,y) -> ge#(O(x),O(y)) -> ge#(x,y)
    ge#(I(x),O(y)) -> ge#(x,y) -> ge#(O(x),I(y)) -> ge#(y,x)
    ge#(I(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),O(y)) -> ge#(x,y)
    ge#(I(x),O(y)) -> ge#(x,y) -> ge#(I(x),I(y)) -> ge#(x,y)
    ge#(I(x),O(y)) -> ge#(x,y) -> ge#(0(),O(x)) -> ge#(0(),x)
    ge#(O(x),I(y)) -> ge#(y,x) -> ge#(O(x),O(y)) -> ge#(x,y)
    ge#(O(x),I(y)) -> ge#(y,x) -> ge#(O(x),I(y)) -> ge#(y,x)
    ge#(O(x),I(y)) -> ge#(y,x) -> ge#(O(x),I(y)) -> not#(ge(y,x))
    ge#(O(x),I(y)) -> ge#(y,x) -> ge#(I(x),O(y)) -> ge#(x,y)
    ge#(O(x),I(y)) -> ge#(y,x) -> ge#(I(x),I(y)) -> ge#(x,y)
    ge#(O(x),I(y)) -> ge#(y,x) -> ge#(0(),O(x)) -> ge#(0(),x)
    ge#(O(x),O(y)) -> ge#(x,y) -> ge#(O(x),O(y)) -> ge#(x,y)
    ge#(O(x),O(y)) -> ge#(x,y) -> ge#(O(x),I(y)) -> ge#(y,x)
    ge#(O(x),O(y)) -> ge#(x,y) -> ge#(O(x),I(y)) -> not#(ge(y,x))
    ge#(O(x),O(y)) -> ge#(x,y) -> ge#(I(x),O(y)) -> ge#(x,y)
    ge#(O(x),O(y)) -> ge#(x,y) -> ge#(I(x),I(y)) -> ge#(x,y)
    ge#(O(x),O(y)) -> ge#(x,y) -> ge#(0(),O(x)) -> ge#(0(),x)
    ge#(0(),O(x)) -> ge#(0(),x) -> ge#(0(),O(x)) -> ge#(0(),x)
    -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y)
    -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),O(y)) -> O#(-(x,y))
    -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(x,y)
    -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(-(x,y),I(1()))
    -#(I(x),I(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y)
    -#(I(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y)
    -#(I(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y))
    -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y)
    -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> O#(-(x,y))
    -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(x,y)
    -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(-(x,y),I(1()))
    -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y)
    -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y)
    -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y))
    -#(O(x),I(y)) -> -#(-(x,y),I(1())) ->
    -#(O(x),I(y)) -> -#(x,y)
    -#(O(x),I(y)) -> -#(-(x,y),I(1())) ->
    -#(O(x),I(y)) -> -#(-(x,y),I(1()))
    -#(O(x),I(y)) -> -#(-(x,y),I(1())) ->
    -#(I(x),I(y)) -> -#(x,y)
    -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(I(x),I(y)) -> O#(-(x,y))
    -#(O(x),I(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y)
    -#(O(x),I(y)) -> -#(x,y) -> -#(O(x),O(y)) -> O#(-(x,y))
    -#(O(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(x,y)
    -#(O(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(-(x,y),I(1()))
    -#(O(x),I(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y)
    -#(O(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y)
    -#(O(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y))
    -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y)
    -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> O#(-(x,y))
    -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(x,y)
    -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(-(x,y),I(1()))
    -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y)
    -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y)
    -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y))
    +#(I(x),I(y)) -> +#(+(x,y),I(0())) ->
    +#(O(x),I(y)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(+(x,y),I(0())) ->
    +#(I(x),I(y)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(+(x,y),I(0())) ->
    +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    +#(I(x),I(y)) -> +#(+(x,y),I(0())) ->
    +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    +#(I(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y))
    +#(I(x),I(y)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    +#(I(x),I(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y)
    +#(I(x),I(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(I(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y)
    +#(I(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y))
    +#(I(x),O(y)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y)
    +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y)
    +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y)
    +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    +#(I(x),O(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y)
    +#(I(x),O(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(O(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y)
    +#(O(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y))
    +#(O(x),I(y)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y)
    +#(O(x),I(y)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y)
    +#(O(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y)
    +#(O(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    +#(O(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    +#(O(x),I(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y)
    +#(O(x),I(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(O(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y)
    +#(O(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y))
    +#(O(x),O(y)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y)
    +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y)
    +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y)
    +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    +#(O(x),O(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y)
    +#(O(x),O(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(O(x),O(y)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(O(x),O(y)) -> O#(+(x,y))
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(O(x),I(y)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(I(x),O(y)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(I(x),I(y)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    +#(x,+(y,z)) -> +#(+(x,y),z) ->
    +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(x,+(y,z)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y))
    +#(x,+(y,z)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0()))
    +#(x,+(y,z)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
    +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z)
   SCC Processor:
    #sccs: 5
    #rules: 19
    #arcs: 148/3249
    DPs:
     -#(I(x),I(y)) -> -#(x,y)
     -#(I(x),O(y)) -> -#(x,y)
     -#(O(x),I(y)) -> -#(-(x,y),I(1()))
     -#(O(x),I(y)) -> -#(x,y)
     -#(O(x),O(y)) -> -#(x,y)
    TRS:
     O(0()) -> 0()
     +(0(),x) -> x
     +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z)
     -(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(true()) -> false()
     not(false()) -> true()
     and(x,true()) -> x
     and(x,false()) -> false()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,0()) -> true()
     ge(0(),O(x)) -> ge(0(),x)
     ge(0(),I(x)) -> false()
     Log'(0()) -> 0()
     Log'(I(x)) -> +(Log'(x),I(0()))
     Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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())))
    Open
    
    DPs:
     Log'#(O(x)) -> Log'#(x)
     Log'#(I(x)) -> Log'#(x)
    TRS:
     O(0()) -> 0()
     +(0(),x) -> x
     +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z)
     -(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(true()) -> false()
     not(false()) -> true()
     and(x,true()) -> x
     and(x,false()) -> false()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,0()) -> true()
     ge(0(),O(x)) -> ge(0(),x)
     ge(0(),I(x)) -> false()
     Log'(0()) -> 0()
     Log'(I(x)) -> +(Log'(x),I(0()))
     Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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())))
    Open
    
    DPs:
     +#(I(x),I(y)) -> +#(+(x,y),I(0()))
     +#(I(x),I(y)) -> +#(x,y)
     +#(x,+(y,z)) -> +#(+(x,y),z)
     +#(x,+(y,z)) -> +#(x,y)
     +#(I(x),O(y)) -> +#(x,y)
     +#(O(x),I(y)) -> +#(x,y)
     +#(O(x),O(y)) -> +#(x,y)
    TRS:
     O(0()) -> 0()
     +(0(),x) -> x
     +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z)
     -(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(true()) -> false()
     not(false()) -> true()
     and(x,true()) -> x
     and(x,false()) -> false()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,0()) -> true()
     ge(0(),O(x)) -> ge(0(),x)
     ge(0(),I(x)) -> false()
     Log'(0()) -> 0()
     Log'(I(x)) -> +(Log'(x),I(0()))
     Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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())))
    Open
    
    DPs:
     ge#(I(x),I(y)) -> ge#(x,y)
     ge#(I(x),O(y)) -> ge#(x,y)
     ge#(O(x),I(y)) -> ge#(y,x)
     ge#(O(x),O(y)) -> ge#(x,y)
    TRS:
     O(0()) -> 0()
     +(0(),x) -> x
     +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z)
     -(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(true()) -> false()
     not(false()) -> true()
     and(x,true()) -> x
     and(x,false()) -> false()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,0()) -> true()
     ge(0(),O(x)) -> ge(0(),x)
     ge(0(),I(x)) -> false()
     Log'(0()) -> 0()
     Log'(I(x)) -> +(Log'(x),I(0()))
     Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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())))
    Open
    
    DPs:
     ge#(0(),O(x)) -> ge#(0(),x)
    TRS:
     O(0()) -> 0()
     +(0(),x) -> x
     +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z)
     -(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(true()) -> false()
     not(false()) -> true()
     and(x,true()) -> x
     and(x,false()) -> false()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,0()) -> true()
     ge(0(),O(x)) -> ge(0(),x)
     ge(0(),I(x)) -> false()
     Log'(0()) -> 0()
     Log'(I(x)) -> +(Log'(x),I(0()))
     Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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())))
    Open