MAYBE
Time: 0.056473
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()))}
 DP:
  DP:
   {      +#(x, +(y, z)) -> +#(x, y),
          +#(x, +(y, z)) -> +#(+(x, y), z),
            +#(O x, O y) -> O# +(x, y),
            +#(O x, O y) -> +#(x, y),
            +#(O x, I y) -> +#(x, y),
            +#(I x, O y) -> +#(x, y),
            +#(I x, I y) -> O# +(+(x, y), I 0()),
            +#(I x, I y) -> +#(x, y),
            +#(I x, I y) -> +#(+(x, y), I 0()),
            -#(O x, O y) -> O# -(x, y),
            -#(O x, O y) -> -#(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) -> O# -(x, y),
            -#(I x, I y) -> -#(x, y),
           ge#(0(), O x) -> ge#(0(), x),
           ge#(O x, O y) -> ge#(x, y),
           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#(I x, I y) -> ge#(x, y),
               Log'# O x -> +#(Log' x, I 0()),
               Log'# O x -> if#(ge(x, I 0()), +(Log' x, I 0()), 0()),
               Log'# O x -> ge#(x, I 0()),
               Log'# O x -> Log'# x,
               Log'# I x -> +#(Log' x, I 0()),
               Log'# I x -> Log'# x,
                  Log# x -> -#(Log' x, I 0()),
                  Log# x -> Log'# x,
     Min# N(x, l(), r()) -> Min# l(),
     Max# N(x, l(), r()) -> Max# r(),
      BS# N(x, l(), r()) -> and#(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())),
      BS# N(x, l(), r()) -> and#(ge(x, Max l()), ge(Min r(), x)),
      BS# N(x, l(), r()) -> and#(BS l(), BS r()),
      BS# N(x, l(), r()) -> ge#(x, Max l()),
      BS# N(x, l(), r()) -> ge#(Min r(), x),
      BS# N(x, l(), r()) -> Min# r(),
      BS# N(x, l(), r()) -> Max# l(),
      BS# N(x, l(), r()) -> BS# l(),
      BS# N(x, l(), r()) -> BS# r(),
    Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()),
    Size# N(x, l(), r()) -> +#(Size l(), Size r()),
    Size# N(x, l(), r()) -> Size# l(),
    Size# N(x, l(), r()) -> Size# r(),
      WB# N(x, l(), r()) -> -#(Size l(), Size r()),
      WB# N(x, l(), r()) -> -#(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())),
      WB# N(x, l(), r()) -> and#(WB l(), WB 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()) -> ge#(I 0(), -(Size l(), Size r())),
      WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l())),
      WB# N(x, l(), r()) -> ge#(Size l(), Size r()),
      WB# N(x, l(), r()) -> Size# l(),
      WB# N(x, l(), r()) -> Size# r(),
      WB# N(x, l(), r()) -> WB# l(),
      WB# N(x, l(), r()) -> WB# r()}
  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()))}
  EDG:
   {(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 -> 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 -> Log'# x, Log'# O x -> +#(Log' x, I 0()))
    (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 -> 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, Log'# O x -> +#(Log' x, I 0()))
    (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
    (+#(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 0()))
    (+#(O x, O y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
    (+#(O x, O y) -> +#(x, y), +#(O x, I y) -> +#(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), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(O x, O y) -> +#(x, y), +#(x, +(y, z)) -> +#(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) -> +#(x, y))
    (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (+#(I x, O y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
    (+#(I x, O y) -> +#(x, y), +#(O x, I y) -> +#(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), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(I x, O y) -> +#(x, y), +#(x, +(y, z)) -> +#(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))
    (-#(O x, O y) -> -#(x, y), -#(I x, O y) -> -#(x, y))
    (-#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()))
    (-#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(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))
    (-#(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))
    (-#(I x, O y) -> -#(x, y), -#(I x, O y) -> -#(x, y))
    (-#(I x, O y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()))
    (-#(I x, O y) -> -#(x, y), -#(O x, I y) -> -#(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))
    (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#(I 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#(O x, O y) -> ge#(x, y))
    (ge#(O x, O y) -> ge#(x, y), ge#(0(), O x) -> ge#(0(), x))
    (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#(I 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#(O x, O y) -> ge#(x, y))
    (ge#(I x, I y) -> ge#(x, y), ge#(0(), O x) -> ge#(0(), x))
    (+#(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) -> +#(x, y))
    (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O 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) -> +#(x, y))
    (Log'# O x -> +#(Log' x, I 0()), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (Log'# O x -> +#(Log' x, I 0()), +#(O 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) -> +#(x, y))
    (Log'# I x -> +#(Log' x, I 0()), +#(I x, I y) -> O# +(+(x, y), I 0()))
    (Log'# I x -> +#(Log' x, I 0()), +#(O x, I y) -> +#(x, y))
    (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) -> O# -(x, y))
    (Log# x -> -#(Log' x, I 0()), -#(I x, I y) -> -#(x, y))
    (Log'# O x -> ge#(x, I 0()), ge#(O x, I y) -> not# ge(y, x))
    (Log'# O x -> ge#(x, I 0()), ge#(O x, I y) -> ge#(y, x))
    (Log'# O x -> ge#(x, I 0()), ge#(I x, I y) -> ge#(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) -> O# -(x, y))
    (-#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, I y) -> -#(x, y))
    (ge#(I x, O 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) -> not# ge(y, x))
    (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#(I x, O y) -> ge#(x, y))
    (ge#(I x, O y) -> ge#(x, y), ge#(I x, I y) -> ge#(x, y))
    (-#(I x, I y) -> -#(x, y), -#(O x, O y) -> O# -(x, y))
    (-#(I x, I y) -> -#(x, y), -#(O x, O y) -> -#(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) -> O# -(x, y))
    (-#(I x, I y) -> -#(x, y), -#(I x, I y) -> -#(x, y))
    (-#(O x, I y) -> -#(x, y), -#(O x, O y) -> O# -(x, y))
    (-#(O x, I y) -> -#(x, y), -#(O x, O y) -> -#(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) -> O# -(x, y))
    (-#(O x, I y) -> -#(x, y), -#(I x, I y) -> -#(x, y))
    (+#(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, I y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
    (+#(I x, I y) -> +#(x, y), +#(O x, O y) -> +#(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) -> O# +(+(x, y), I 0()))
    (+#(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()))
    (+#(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, I y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
    (+#(O x, I y) -> +#(x, y), +#(O x, O y) -> +#(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) -> O# +(+(x, y), I 0()))
    (+#(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()))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(x, +(y, z)) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(O x, O y) -> +#(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) -> O# +(+(x, y), I 0()))
    (+#(x, +(y, z)) -> +#(x, y), +#(I x, I y) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
    (ge#(0(), O x) -> ge#(0(), x), ge#(0(), O x) -> ge#(0(), x))
    (+#(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), z), +#(O x, O y) -> O# +(x, y))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, O y) -> +#(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) -> O# +(+(x, y), I 0()))
    (+#(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()))
    (Log'# I x -> Log'# x, Log'# O x -> +#(Log' 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, Log'# O x -> ge#(x, I 0()))
    (Log'# I x -> Log'# x, Log'# O x -> Log'# x)
    (Log'# I x -> Log'# x, Log'# I x -> +#(Log' x, I 0()))
    (Log'# I x -> Log'# x, Log'# I x -> Log'# x)
    (ge#(O x, I y) -> ge#(y, x), 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) -> not# ge(y, x))
    (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#(I x, O y) -> ge#(x, y))
    (ge#(O x, I y) -> ge#(y, x), ge#(I x, I y) -> ge#(x, y))}
   STATUS:
    arrows: 0.954448
    SCCS (5):
     Scc:
      {-#(O x, O y) -> -#(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)}
     Scc:
      {Log'# O x -> Log'# x,
       Log'# I x -> Log'# x}
     Scc:
      {+#(x, +(y, z)) -> +#(x, y),
       +#(x, +(y, z)) -> +#(+(x, y), z),
         +#(O x, O y) -> +#(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())}
     Scc:
      {ge#(O x, O y) -> ge#(x, y),
       ge#(O x, I y) -> ge#(y, x),
       ge#(I x, O y) -> ge#(x, y),
       ge#(I x, I y) -> ge#(x, y)}
     Scc:
      {ge#(0(), O x) -> ge#(0(), x)}
     
     
     
     
     
     
     
     
     
     
     
     SCC (5):
      Strict:
       {-#(O x, O y) -> -#(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)}
      Weak:
      {              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()))}
      Open
     
     
     
     
     
     
     
     
     
     
     
     
     
     
     
     
     
     
     
     
     
     SCC (2):
      Strict:
       {Log'# O x -> Log'# x,
        Log'# I x -> Log'# x}
      Weak:
      {              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()))}
      Open
     
     
     
     
     SCC (7):
      Strict:
       {+#(x, +(y, z)) -> +#(x, y),
        +#(x, +(y, z)) -> +#(+(x, y), z),
          +#(O x, O y) -> +#(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())}
      Weak:
      {              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()))}
      Open
     
     
     SCC (4):
      Strict:
       {ge#(O x, O y) -> ge#(x, y),
        ge#(O x, I y) -> ge#(y, x),
        ge#(I x, O y) -> ge#(x, y),
        ge#(I x, I y) -> ge#(x, y)}
      Weak:
      {              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()))}
      Open
     
     SCC (1):
      Strict:
       {ge#(0(), O x) -> ge#(0(), x)}
      Weak:
      {              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()))}
      Open