YES
TRS:
 {           0(#()) -> #(),
          +(x, #()) -> x,
      +(x, +(y, z)) -> +(+(x, y), z),
          +(#(), x) -> x,
      +(0(x), 0(y)) -> 0(+(x, y)),
      +(0(x), 1(y)) -> 1(+(x, y)),
      +(1(x), 0(y)) -> 1(+(x, y)),
      +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
          -(x, #()) -> x,
          -(#(), x) -> #(),
      -(0(x), 0(y)) -> 0(-(x, y)),
      -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
      -(1(x), 0(y)) -> 1(-(x, y)),
      -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
      ge(#(), 0(x)) -> ge(#(), x),
      ge(#(), 1(x)) -> false(),
     ge(0(x), 0(y)) -> ge(x, y),
     ge(0(x), 1(y)) -> not(ge(y, x)),
     ge(1(x), 0(y)) -> ge(x, y),
     ge(1(x), 1(y)) -> ge(x, y),
          val(l(x)) -> x,
    val(n(x, y, z)) -> x,
          min(l(x)) -> x,
    min(n(x, y, z)) -> min(y),
          max(l(x)) -> x,
    max(n(x, y, z)) -> max(z),
           bs(l(x)) -> true(),
     bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
         size(l(x)) -> 1(#()),
   size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
           wb(l(x)) -> true(),
     wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
 DP:
  Strict:
   {   +#(x, +(y, z)) -> +#(x, y),
       +#(x, +(y, z)) -> +#(+(x, y), z),
       +#(0(x), 0(y)) -> 0#(+(x, y)),
       +#(0(x), 0(y)) -> +#(x, y),
       +#(0(x), 1(y)) -> +#(x, y),
       +#(1(x), 0(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))),
       +#(1(x), 1(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(+(x, y), 1(#())),
       -#(0(x), 0(y)) -> 0#(-(x, y)),
       -#(0(x), 0(y)) -> -#(x, y),
       -#(0(x), 1(y)) -> -#(x, y),
       -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
       -#(1(x), 0(y)) -> -#(x, y),
       -#(1(x), 1(y)) -> 0#(-(x, y)),
       -#(1(x), 1(y)) -> -#(x, y),
       ge#(#(), 0(x)) -> ge#(#(), x),
      ge#(0(x), 0(y)) -> ge#(x, y),
      ge#(0(x), 1(y)) -> not#(ge(y, x)),
      ge#(0(x), 1(y)) -> ge#(y, x),
      ge#(1(x), 0(y)) -> ge#(x, y),
      ge#(1(x), 1(y)) -> ge#(x, y),
     min#(n(x, y, z)) -> min#(y),
     max#(n(x, y, z)) -> max#(z),
      bs#(n(x, y, z)) -> and#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
      bs#(n(x, y, z)) -> and#(ge(x, max(y)), ge(min(z), x)),
      bs#(n(x, y, z)) -> and#(bs(y), bs(z)),
      bs#(n(x, y, z)) -> ge#(x, max(y)),
      bs#(n(x, y, z)) -> ge#(min(z), x),
      bs#(n(x, y, z)) -> min#(z),
      bs#(n(x, y, z)) -> max#(y),
      bs#(n(x, y, z)) -> bs#(y),
      bs#(n(x, y, z)) -> bs#(z),
    size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())),
    size#(n(x, y, z)) -> +#(size(x), size(y)),
    size#(n(x, y, z)) -> size#(x),
    size#(n(x, y, z)) -> size#(y),
      wb#(n(x, y, z)) -> -#(size(y), size(z)),
      wb#(n(x, y, z)) -> -#(size(z), size(y)),
      wb#(n(x, y, z)) -> and#(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z))),
      wb#(n(x, y, z)) -> and#(wb(y), wb(z)),
      wb#(n(x, y, z)) -> if#(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))),
      wb#(n(x, y, z)) -> ge#(1(#()), -(size(y), size(z))),
      wb#(n(x, y, z)) -> ge#(1(#()), -(size(z), size(y))),
      wb#(n(x, y, z)) -> ge#(size(y), size(z)),
      wb#(n(x, y, z)) -> size#(y),
      wb#(n(x, y, z)) -> size#(z),
      wb#(n(x, y, z)) -> wb#(y),
      wb#(n(x, y, z)) -> wb#(z)}
  Weak:
  {           0(#()) -> #(),
           +(x, #()) -> x,
       +(x, +(y, z)) -> +(+(x, y), z),
           +(#(), x) -> x,
       +(0(x), 0(y)) -> 0(+(x, y)),
       +(0(x), 1(y)) -> 1(+(x, y)),
       +(1(x), 0(y)) -> 1(+(x, y)),
       +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
           -(x, #()) -> x,
           -(#(), x) -> #(),
       -(0(x), 0(y)) -> 0(-(x, y)),
       -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
       -(1(x), 0(y)) -> 1(-(x, y)),
       -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
       ge(#(), 0(x)) -> ge(#(), x),
       ge(#(), 1(x)) -> false(),
      ge(0(x), 0(y)) -> ge(x, y),
      ge(0(x), 1(y)) -> not(ge(y, x)),
      ge(1(x), 0(y)) -> ge(x, y),
      ge(1(x), 1(y)) -> ge(x, y),
           val(l(x)) -> x,
     val(n(x, y, z)) -> x,
           min(l(x)) -> x,
     min(n(x, y, z)) -> min(y),
           max(l(x)) -> x,
     max(n(x, y, z)) -> max(z),
            bs(l(x)) -> true(),
      bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
          size(l(x)) -> 1(#()),
    size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
            wb(l(x)) -> true(),
      wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
  EDG:
   {
    (size#(n(x, y, z)) -> size#(x), size#(n(x, y, z)) -> size#(y))
    (size#(n(x, y, z)) -> size#(x), size#(n(x, y, z)) -> size#(x))
    (size#(n(x, y, z)) -> size#(x), size#(n(x, y, z)) -> +#(size(x), size(y)))
    (size#(n(x, y, z)) -> size#(x), size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())))
    (+#(x, +(y, z)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(x, +(y, z)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(x, +(y, z)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(0(x), 1(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(1(x), 1(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
    (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
    (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
    (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
    (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(1(x), 1(y)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(1(x), 0(y)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(0(x), 1(y)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(0(x), 0(y)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y))
    (bs#(n(x, y, z)) -> min#(z), min#(n(x, y, z)) -> min#(y))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> wb#(z))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> wb#(y))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> size#(z))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> size#(y))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> ge#(size(y), size(z)))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> ge#(1(#()), -(size(z), size(y))))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> ge#(1(#()), -(size(y), size(z))))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> if#(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> and#(wb(y), wb(z)))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> and#(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z))))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> -#(size(z), size(y)))
    (wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> -#(size(y), size(z)))
    (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 1(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(x, y))
    (wb#(n(x, y, z)) -> ge#(1(#()), -(size(y), size(z))), ge#(1(x), 1(y)) -> ge#(x, y))
    (wb#(n(x, y, z)) -> ge#(1(#()), -(size(y), size(z))), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(#(), 0(x)) -> ge#(#(), x), ge#(#(), 0(x)) -> ge#(#(), x))
    (bs#(n(x, y, z)) -> ge#(x, max(y)), ge#(1(x), 1(y)) -> ge#(x, y))
    (bs#(n(x, y, z)) -> ge#(x, max(y)), ge#(1(x), 0(y)) -> ge#(x, y))
    (bs#(n(x, y, z)) -> ge#(x, max(y)), ge#(0(x), 1(y)) -> ge#(y, x))
    (bs#(n(x, y, z)) -> ge#(x, max(y)), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (bs#(n(x, y, z)) -> ge#(x, max(y)), ge#(0(x), 0(y)) -> ge#(x, y))
    (bs#(n(x, y, z)) -> ge#(x, max(y)), ge#(#(), 0(x)) -> ge#(#(), x))
    (wb#(n(x, y, z)) -> -#(size(y), size(z)), -#(1(x), 1(y)) -> -#(x, y))
    (wb#(n(x, y, z)) -> -#(size(y), size(z)), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (wb#(n(x, y, z)) -> -#(size(y), size(z)), -#(1(x), 0(y)) -> -#(x, y))
    (wb#(n(x, y, z)) -> -#(size(y), size(z)), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (wb#(n(x, y, z)) -> -#(size(y), size(z)), -#(0(x), 1(y)) -> -#(x, y))
    (wb#(n(x, y, z)) -> -#(size(y), size(z)), -#(0(x), 0(y)) -> -#(x, y))
    (wb#(n(x, y, z)) -> -#(size(y), size(z)), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (min#(n(x, y, z)) -> min#(y), min#(n(x, y, z)) -> min#(y))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> bs#(z))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> bs#(y))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> max#(y))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> min#(z))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> ge#(min(z), x))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> ge#(x, max(y)))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> and#(bs(y), bs(z)))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> and#(ge(x, max(y)), ge(min(z), x)))
    (bs#(n(x, y, z)) -> bs#(y), bs#(n(x, y, z)) -> and#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))))
    (wb#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> size#(y))
    (wb#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> size#(x))
    (wb#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> +#(size(x), size(y)))
    (wb#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())))
    (bs#(n(x, y, z)) -> ge#(min(z), x), ge#(1(x), 1(y)) -> ge#(x, y))
    (bs#(n(x, y, z)) -> ge#(min(z), x), ge#(1(x), 0(y)) -> ge#(x, y))
    (bs#(n(x, y, z)) -> ge#(min(z), x), ge#(0(x), 1(y)) -> ge#(y, x))
    (bs#(n(x, y, z)) -> ge#(min(z), x), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (bs#(n(x, y, z)) -> ge#(min(z), x), ge#(0(x), 0(y)) -> ge#(x, y))
    (bs#(n(x, y, z)) -> ge#(min(z), x), ge#(#(), 0(x)) -> ge#(#(), x))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> -#(size(y), size(z)))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> -#(size(z), size(y)))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> and#(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z))))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> and#(wb(y), wb(z)))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> if#(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> ge#(1(#()), -(size(y), size(z))))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> ge#(1(#()), -(size(z), size(y))))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> ge#(size(y), size(z)))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> size#(y))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> size#(z))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> wb#(y))
    (wb#(n(x, y, z)) -> wb#(y), wb#(n(x, y, z)) -> wb#(z))
    (size#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())))
    (size#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> +#(size(x), size(y)))
    (size#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> size#(x))
    (size#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> size#(y))
    (bs#(n(x, y, z)) -> max#(y), max#(n(x, y, z)) -> max#(z))
    (wb#(n(x, y, z)) -> ge#(size(y), size(z)), ge#(#(), 0(x)) -> ge#(#(), x))
    (wb#(n(x, y, z)) -> ge#(size(y), size(z)), ge#(0(x), 0(y)) -> ge#(x, y))
    (wb#(n(x, y, z)) -> ge#(size(y), size(z)), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (wb#(n(x, y, z)) -> ge#(size(y), size(z)), ge#(0(x), 1(y)) -> ge#(y, x))
    (wb#(n(x, y, z)) -> ge#(size(y), size(z)), ge#(1(x), 0(y)) -> ge#(x, y))
    (wb#(n(x, y, z)) -> ge#(size(y), size(z)), ge#(1(x), 1(y)) -> ge#(x, y))
    (wb#(n(x, y, z)) -> -#(size(z), size(y)), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (wb#(n(x, y, z)) -> -#(size(z), size(y)), -#(0(x), 0(y)) -> -#(x, y))
    (wb#(n(x, y, z)) -> -#(size(z), size(y)), -#(0(x), 1(y)) -> -#(x, y))
    (wb#(n(x, y, z)) -> -#(size(z), size(y)), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (wb#(n(x, y, z)) -> -#(size(z), size(y)), -#(1(x), 0(y)) -> -#(x, y))
    (wb#(n(x, y, z)) -> -#(size(z), size(y)), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (wb#(n(x, y, z)) -> -#(size(z), size(y)), -#(1(x), 1(y)) -> -#(x, y))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(x, +(y, z)) -> +#(x, y))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(x, +(y, z)) -> +#(+(x, y), z))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(0(x), 0(y)) -> +#(x, y))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(0(x), 1(y)) -> +#(x, y))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(1(x), 0(y)) -> +#(x, y))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(1(x), 1(y)) -> +#(x, y))
    (size#(n(x, y, z)) -> +#(size(x), size(y)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (wb#(n(x, y, z)) -> ge#(1(#()), -(size(z), size(y))), ge#(1(x), 0(y)) -> ge#(x, y))
    (wb#(n(x, y, z)) -> ge#(1(#()), -(size(z), size(y))), ge#(1(x), 1(y)) -> ge#(x, y))
    (size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
    (size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
    (size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (wb#(n(x, y, z)) -> size#(z), size#(n(x, y, z)) -> +#(+(size(x), size(y)), 1(#())))
    (wb#(n(x, y, z)) -> size#(z), size#(n(x, y, z)) -> +#(size(x), size(y)))
    (wb#(n(x, y, z)) -> size#(z), size#(n(x, y, z)) -> size#(x))
    (wb#(n(x, y, z)) -> size#(z), size#(n(x, y, z)) -> size#(y))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> and#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> and#(ge(x, max(y)), ge(min(z), x)))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> and#(bs(y), bs(z)))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> ge#(x, max(y)))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> ge#(min(z), x))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> min#(z))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> max#(y))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> bs#(y))
    (bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> bs#(z))
    (max#(n(x, y, z)) -> max#(z), max#(n(x, y, z)) -> max#(z))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y))
    (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
    (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
    (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
    (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
    (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
    (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
    (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
    (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), 0(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(#(), 0(x)) -> ge#(#(), x))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 0(y)) -> ge#(x, y))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 1(y)) -> ge#(y, x))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 1(y)) -> ge#(x, y))
   }
   SCCS:
    Scc:
     {wb#(n(x, y, z)) -> wb#(y),
      wb#(n(x, y, z)) -> wb#(z)}
    Scc:
     {size#(n(x, y, z)) -> size#(x),
      size#(n(x, y, z)) -> size#(y)}
    Scc:
     {bs#(n(x, y, z)) -> bs#(y),
      bs#(n(x, y, z)) -> bs#(z)}
    Scc:
     {max#(n(x, y, z)) -> max#(z)}
    Scc:
     {min#(n(x, y, z)) -> min#(y)}
    Scc:
     {ge#(0(x), 0(y)) -> ge#(x, y),
      ge#(0(x), 1(y)) -> ge#(y, x),
      ge#(1(x), 0(y)) -> ge#(x, y),
      ge#(1(x), 1(y)) -> ge#(x, y)}
    Scc:
     {ge#(#(), 0(x)) -> ge#(#(), x)}
    Scc:
     {-#(0(x), 0(y)) -> -#(x, y),
      -#(0(x), 1(y)) -> -#(x, y),
      -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
      -#(1(x), 0(y)) -> -#(x, y),
      -#(1(x), 1(y)) -> -#(x, y)}
    Scc:
     {+#(x, +(y, z)) -> +#(x, y),
      +#(x, +(y, z)) -> +#(+(x, y), z),
      +#(0(x), 0(y)) -> +#(x, y),
      +#(0(x), 1(y)) -> +#(x, y),
      +#(1(x), 0(y)) -> +#(x, y),
      +#(1(x), 1(y)) -> +#(x, y),
      +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
    SCC:
     Strict:
      {wb#(n(x, y, z)) -> wb#(y),
       wb#(n(x, y, z)) -> wb#(z)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     SPSC:
      Simple Projection:
       pi(wb#) = 0
      Strict:
       {wb#(n(x, y, z)) -> wb#(z)}
      EDG:
       {(wb#(n(x, y, z)) -> wb#(z), wb#(n(x, y, z)) -> wb#(z))}
       SCCS:
        Scc:
         {wb#(n(x, y, z)) -> wb#(z)}
        SCC:
         Strict:
          {wb#(n(x, y, z)) -> wb#(z)}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
              +(x, +(y, z)) -> +(+(x, y), z),
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  val(l(x)) -> x,
            val(n(x, y, z)) -> x,
                  min(l(x)) -> x,
            min(n(x, y, z)) -> min(y),
                  max(l(x)) -> x,
            max(n(x, y, z)) -> max(z),
                   bs(l(x)) -> true(),
             bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                 size(l(x)) -> 1(#()),
           size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                   wb(l(x)) -> true(),
             wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
         SPSC:
          Simple Projection:
           pi(wb#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {size#(n(x, y, z)) -> size#(x),
       size#(n(x, y, z)) -> size#(y)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     SPSC:
      Simple Projection:
       pi(size#) = 0
      Strict:
       {size#(n(x, y, z)) -> size#(y)}
      EDG:
       {(size#(n(x, y, z)) -> size#(y), size#(n(x, y, z)) -> size#(y))}
       SCCS:
        Scc:
         {size#(n(x, y, z)) -> size#(y)}
        SCC:
         Strict:
          {size#(n(x, y, z)) -> size#(y)}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
              +(x, +(y, z)) -> +(+(x, y), z),
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  val(l(x)) -> x,
            val(n(x, y, z)) -> x,
                  min(l(x)) -> x,
            min(n(x, y, z)) -> min(y),
                  max(l(x)) -> x,
            max(n(x, y, z)) -> max(z),
                   bs(l(x)) -> true(),
             bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                 size(l(x)) -> 1(#()),
           size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                   wb(l(x)) -> true(),
             wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
         SPSC:
          Simple Projection:
           pi(size#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {bs#(n(x, y, z)) -> bs#(y),
       bs#(n(x, y, z)) -> bs#(z)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     SPSC:
      Simple Projection:
       pi(bs#) = 0
      Strict:
       {bs#(n(x, y, z)) -> bs#(z)}
      EDG:
       {(bs#(n(x, y, z)) -> bs#(z), bs#(n(x, y, z)) -> bs#(z))}
       SCCS:
        Scc:
         {bs#(n(x, y, z)) -> bs#(z)}
        SCC:
         Strict:
          {bs#(n(x, y, z)) -> bs#(z)}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
              +(x, +(y, z)) -> +(+(x, y), z),
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  val(l(x)) -> x,
            val(n(x, y, z)) -> x,
                  min(l(x)) -> x,
            min(n(x, y, z)) -> min(y),
                  max(l(x)) -> x,
            max(n(x, y, z)) -> max(z),
                   bs(l(x)) -> true(),
             bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                 size(l(x)) -> 1(#()),
           size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                   wb(l(x)) -> true(),
             wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
         SPSC:
          Simple Projection:
           pi(bs#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {max#(n(x, y, z)) -> max#(z)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     SPSC:
      Simple Projection:
       pi(max#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {min#(n(x, y, z)) -> min#(y)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     SPSC:
      Simple Projection:
       pi(min#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {ge#(0(x), 0(y)) -> ge#(x, y),
       ge#(0(x), 1(y)) -> ge#(y, x),
       ge#(1(x), 0(y)) -> ge#(x, y),
       ge#(1(x), 1(y)) -> ge#(x, y)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     POLY:
      Argument Filtering:
       pi(wb) = [], pi(size) = [], pi(bs) = [], pi(max) = [], pi(min) = [], pi(n) = [], pi(l) = [], pi(val) = [], pi(ge#) = [0,1], pi(ge) = [], pi(if) = [], pi(and) = [], pi(false) = [], pi(not) = [], pi(true) = [], pi(-) = [], pi(1) = [0], pi(+) = [], pi(0) = 0, pi(#) = []
      Usable Rules:
       {}
      Interpretation:
       [ge#](x0, x1) = x0 + x1,
       [1](x0) = x0 + 1
      Strict:
       {ge#(0(x), 0(y)) -> ge#(x, y)}
      Weak:
       {           0(#()) -> #(),
                +(x, #()) -> x,
            +(x, +(y, z)) -> +(+(x, y), z),
                +(#(), x) -> x,
            +(0(x), 0(y)) -> 0(+(x, y)),
            +(0(x), 1(y)) -> 1(+(x, y)),
            +(1(x), 0(y)) -> 1(+(x, y)),
            +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                -(x, #()) -> x,
                -(#(), x) -> #(),
            -(0(x), 0(y)) -> 0(-(x, y)),
            -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
            -(1(x), 0(y)) -> 1(-(x, y)),
            -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
            ge(#(), 0(x)) -> ge(#(), x),
            ge(#(), 1(x)) -> false(),
           ge(0(x), 0(y)) -> ge(x, y),
           ge(0(x), 1(y)) -> not(ge(y, x)),
           ge(1(x), 0(y)) -> ge(x, y),
           ge(1(x), 1(y)) -> ge(x, y),
                val(l(x)) -> x,
          val(n(x, y, z)) -> x,
                min(l(x)) -> x,
          min(n(x, y, z)) -> min(y),
                max(l(x)) -> x,
          max(n(x, y, z)) -> max(z),
                 bs(l(x)) -> true(),
           bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
               size(l(x)) -> 1(#()),
         size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                 wb(l(x)) -> true(),
           wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
      EDG:
       {(ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y))}
       SCCS:
        Scc:
         {ge#(0(x), 0(y)) -> ge#(x, y)}
        SCC:
         Strict:
          {ge#(0(x), 0(y)) -> ge#(x, y)}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
              +(x, +(y, z)) -> +(+(x, y), z),
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  val(l(x)) -> x,
            val(n(x, y, z)) -> x,
                  min(l(x)) -> x,
            min(n(x, y, z)) -> min(y),
                  max(l(x)) -> x,
            max(n(x, y, z)) -> max(z),
                   bs(l(x)) -> true(),
             bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                 size(l(x)) -> 1(#()),
           size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                   wb(l(x)) -> true(),
             wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
         SPSC:
          Simple Projection:
           pi(ge#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {ge#(#(), 0(x)) -> ge#(#(), x)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     SPSC:
      Simple Projection:
       pi(ge#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {-#(0(x), 0(y)) -> -#(x, y),
       -#(0(x), 1(y)) -> -#(x, y),
       -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
       -#(1(x), 0(y)) -> -#(x, y),
       -#(1(x), 1(y)) -> -#(x, y)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     POLY:
      Argument Filtering:
       pi(wb) = [], pi(size) = [], pi(bs) = [], pi(max) = [], pi(min) = [], pi(n) = [], pi(l) = [], pi(val) = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(false) = [], pi(not) = [], pi(true) = [], pi(-#) = 1, pi(-) = [], pi(1) = 0, pi(+) = [], pi(0) = [0], pi(#) = []
      Usable Rules:
       {}
      Interpretation:
       [0](x0) = x0 + 1,
       [#] = 0
      Strict:
       {-#(0(x), 1(y)) -> -#(x, y),
        -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
        -#(1(x), 1(y)) -> -#(x, y)}
      Weak:
       {           0(#()) -> #(),
                +(x, #()) -> x,
            +(x, +(y, z)) -> +(+(x, y), z),
                +(#(), x) -> x,
            +(0(x), 0(y)) -> 0(+(x, y)),
            +(0(x), 1(y)) -> 1(+(x, y)),
            +(1(x), 0(y)) -> 1(+(x, y)),
            +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                -(x, #()) -> x,
                -(#(), x) -> #(),
            -(0(x), 0(y)) -> 0(-(x, y)),
            -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
            -(1(x), 0(y)) -> 1(-(x, y)),
            -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
            ge(#(), 0(x)) -> ge(#(), x),
            ge(#(), 1(x)) -> false(),
           ge(0(x), 0(y)) -> ge(x, y),
           ge(0(x), 1(y)) -> not(ge(y, x)),
           ge(1(x), 0(y)) -> ge(x, y),
           ge(1(x), 1(y)) -> ge(x, y),
                val(l(x)) -> x,
          val(n(x, y, z)) -> x,
                min(l(x)) -> x,
          min(n(x, y, z)) -> min(y),
                max(l(x)) -> x,
          max(n(x, y, z)) -> max(z),
                 bs(l(x)) -> true(),
           bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
               size(l(x)) -> 1(#()),
         size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                 wb(l(x)) -> true(),
           wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
      EDG:
       {(-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
        (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
        (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
        (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(x, y))
        (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
        (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 1(y)) -> -#(x, y))
        (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
        (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
        (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))}
       SCCS:
        Scc:
         {-#(0(x), 1(y)) -> -#(x, y),
          -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
          -#(1(x), 1(y)) -> -#(x, y)}
        SCC:
         Strict:
          {-#(0(x), 1(y)) -> -#(x, y),
           -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
           -#(1(x), 1(y)) -> -#(x, y)}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
              +(x, +(y, z)) -> +(+(x, y), z),
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  val(l(x)) -> x,
            val(n(x, y, z)) -> x,
                  min(l(x)) -> x,
            min(n(x, y, z)) -> min(y),
                  max(l(x)) -> x,
            max(n(x, y, z)) -> max(z),
                   bs(l(x)) -> true(),
             bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                 size(l(x)) -> 1(#()),
           size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                   wb(l(x)) -> true(),
             wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
         POLY:
          Argument Filtering:
           pi(wb) = [], pi(size) = [], pi(bs) = [], pi(max) = [], pi(min) = [], pi(n) = [], pi(l) = [], pi(val) = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(false) = [], pi(not) = [], pi(true) = [], pi(-#) = 1, pi(-) = [], pi(1) = [0], pi(+) = [], pi(0) = [], pi(#) = []
          Usable Rules:
           {}
          Interpretation:
           [1](x0) = x0 + 1,
           [#] = 0
          Strict:
           {-#(0(x), 1(y)) -> -#(-(x, y), 1(#()))}
          Weak:
           {           0(#()) -> #(),
                    +(x, #()) -> x,
                +(x, +(y, z)) -> +(+(x, y), z),
                    +(#(), x) -> x,
                +(0(x), 0(y)) -> 0(+(x, y)),
                +(0(x), 1(y)) -> 1(+(x, y)),
                +(1(x), 0(y)) -> 1(+(x, y)),
                +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                    -(x, #()) -> x,
                    -(#(), x) -> #(),
                -(0(x), 0(y)) -> 0(-(x, y)),
                -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                -(1(x), 0(y)) -> 1(-(x, y)),
                -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
                ge(#(), 0(x)) -> ge(#(), x),
                ge(#(), 1(x)) -> false(),
               ge(0(x), 0(y)) -> ge(x, y),
               ge(0(x), 1(y)) -> not(ge(y, x)),
               ge(1(x), 0(y)) -> ge(x, y),
               ge(1(x), 1(y)) -> ge(x, y),
                    val(l(x)) -> x,
              val(n(x, y, z)) -> x,
                    min(l(x)) -> x,
              min(n(x, y, z)) -> min(y),
                    max(l(x)) -> x,
              max(n(x, y, z)) -> max(z),
                     bs(l(x)) -> true(),
               bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                   size(l(x)) -> 1(#()),
             size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                     wb(l(x)) -> true(),
               wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
          EDG:
           {(-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))}
           SCCS:
            Scc:
             {-#(0(x), 1(y)) -> -#(-(x, y), 1(#()))}
            SCC:
             Strict:
              {-#(0(x), 1(y)) -> -#(-(x, y), 1(#()))}
             Weak:
             {           0(#()) -> #(),
                      +(x, #()) -> x,
                  +(x, +(y, z)) -> +(+(x, y), z),
                      +(#(), x) -> x,
                  +(0(x), 0(y)) -> 0(+(x, y)),
                  +(0(x), 1(y)) -> 1(+(x, y)),
                  +(1(x), 0(y)) -> 1(+(x, y)),
                  +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                      -(x, #()) -> x,
                      -(#(), x) -> #(),
                  -(0(x), 0(y)) -> 0(-(x, y)),
                  -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                  -(1(x), 0(y)) -> 1(-(x, y)),
                  -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
                  ge(#(), 0(x)) -> ge(#(), x),
                  ge(#(), 1(x)) -> false(),
                 ge(0(x), 0(y)) -> ge(x, y),
                 ge(0(x), 1(y)) -> not(ge(y, x)),
                 ge(1(x), 0(y)) -> ge(x, y),
                 ge(1(x), 1(y)) -> ge(x, y),
                      val(l(x)) -> x,
                val(n(x, y, z)) -> x,
                      min(l(x)) -> x,
                min(n(x, y, z)) -> min(y),
                      max(l(x)) -> x,
                max(n(x, y, z)) -> max(z),
                       bs(l(x)) -> true(),
                 bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                     size(l(x)) -> 1(#()),
               size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                       wb(l(x)) -> true(),
                 wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
             POLY:
              Argument Filtering:
               pi(wb) = [], pi(size) = [], pi(bs) = [], pi(max) = [], pi(min) = [], pi(n) = [], pi(l) = [], pi(val) = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(false) = [], pi(not) = [], pi(true) = [], pi(-#) = 0, pi(-) = 0, pi(1) = [0], pi(+) = [], pi(0) = [0], pi(#) = []
              Usable Rules:
               {}
              Interpretation:
               [0](x0) = x0 + 1
              Strict:
               {}
              Weak:
               {           0(#()) -> #(),
                        +(x, #()) -> x,
                    +(x, +(y, z)) -> +(+(x, y), z),
                        +(#(), x) -> x,
                    +(0(x), 0(y)) -> 0(+(x, y)),
                    +(0(x), 1(y)) -> 1(+(x, y)),
                    +(1(x), 0(y)) -> 1(+(x, y)),
                    +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                        -(x, #()) -> x,
                        -(#(), x) -> #(),
                    -(0(x), 0(y)) -> 0(-(x, y)),
                    -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                    -(1(x), 0(y)) -> 1(-(x, y)),
                    -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
                    ge(#(), 0(x)) -> ge(#(), x),
                    ge(#(), 1(x)) -> false(),
                   ge(0(x), 0(y)) -> ge(x, y),
                   ge(0(x), 1(y)) -> not(ge(y, x)),
                   ge(1(x), 0(y)) -> ge(x, y),
                   ge(1(x), 1(y)) -> ge(x, y),
                        val(l(x)) -> x,
                  val(n(x, y, z)) -> x,
                        min(l(x)) -> x,
                  min(n(x, y, z)) -> min(y),
                        max(l(x)) -> x,
                  max(n(x, y, z)) -> max(z),
                         bs(l(x)) -> true(),
                   bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                       size(l(x)) -> 1(#()),
                 size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                         wb(l(x)) -> true(),
                   wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
              Qed
    SCC:
     Strict:
      {+#(x, +(y, z)) -> +#(x, y),
       +#(x, +(y, z)) -> +#(+(x, y), z),
       +#(0(x), 0(y)) -> +#(x, y),
       +#(0(x), 1(y)) -> +#(x, y),
       +#(1(x), 0(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
          +(x, +(y, z)) -> +(+(x, y), z),
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              val(l(x)) -> x,
        val(n(x, y, z)) -> x,
              min(l(x)) -> x,
        min(n(x, y, z)) -> min(y),
              max(l(x)) -> x,
        max(n(x, y, z)) -> max(z),
               bs(l(x)) -> true(),
         bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
             size(l(x)) -> 1(#()),
       size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
               wb(l(x)) -> true(),
         wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
     POLY:
      Argument Filtering:
       pi(wb) = [], pi(size) = [], pi(bs) = [], pi(max) = [], pi(min) = [], pi(n) = [], pi(l) = [], pi(val) = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(false) = [], pi(not) = [], pi(true) = [], pi(-) = [], pi(1) = 0, pi(+#) = 1, pi(+) = [0,1], pi(0) = 0, pi(#) = []
      Usable Rules:
       {}
      Interpretation:
       [+](x0, x1) = x0 + x1 + 1,
       [#] = 0
      Strict:
       {+#(0(x), 0(y)) -> +#(x, y),
        +#(0(x), 1(y)) -> +#(x, y),
        +#(1(x), 0(y)) -> +#(x, y),
        +#(1(x), 1(y)) -> +#(x, y),
        +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
      Weak:
       {           0(#()) -> #(),
                +(x, #()) -> x,
            +(x, +(y, z)) -> +(+(x, y), z),
                +(#(), x) -> x,
            +(0(x), 0(y)) -> 0(+(x, y)),
            +(0(x), 1(y)) -> 1(+(x, y)),
            +(1(x), 0(y)) -> 1(+(x, y)),
            +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                -(x, #()) -> x,
                -(#(), x) -> #(),
            -(0(x), 0(y)) -> 0(-(x, y)),
            -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
            -(1(x), 0(y)) -> 1(-(x, y)),
            -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
            ge(#(), 0(x)) -> ge(#(), x),
            ge(#(), 1(x)) -> false(),
           ge(0(x), 0(y)) -> ge(x, y),
           ge(0(x), 1(y)) -> not(ge(y, x)),
           ge(1(x), 0(y)) -> ge(x, y),
           ge(1(x), 1(y)) -> ge(x, y),
                val(l(x)) -> x,
          val(n(x, y, z)) -> x,
                min(l(x)) -> x,
          min(n(x, y, z)) -> min(y),
                max(l(x)) -> x,
          max(n(x, y, z)) -> max(z),
                 bs(l(x)) -> true(),
           bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
               size(l(x)) -> 1(#()),
         size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                 wb(l(x)) -> true(),
           wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
      EDG:
       {(+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
        (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
        (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
        (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
        (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
        (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
        (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
        (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
        (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
        (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
        (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
        (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
        (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
        (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
        (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
        (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
        (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
        (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
        (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
        (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
        (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
        (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
        (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))}
       SCCS:
        Scc:
         {+#(0(x), 0(y)) -> +#(x, y),
          +#(0(x), 1(y)) -> +#(x, y),
          +#(1(x), 0(y)) -> +#(x, y),
          +#(1(x), 1(y)) -> +#(x, y),
          +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
        SCC:
         Strict:
          {+#(0(x), 0(y)) -> +#(x, y),
           +#(0(x), 1(y)) -> +#(x, y),
           +#(1(x), 0(y)) -> +#(x, y),
           +#(1(x), 1(y)) -> +#(x, y),
           +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
              +(x, +(y, z)) -> +(+(x, y), z),
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  val(l(x)) -> x,
            val(n(x, y, z)) -> x,
                  min(l(x)) -> x,
            min(n(x, y, z)) -> min(y),
                  max(l(x)) -> x,
            max(n(x, y, z)) -> max(z),
                   bs(l(x)) -> true(),
             bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                 size(l(x)) -> 1(#()),
           size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                   wb(l(x)) -> true(),
             wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
         POLY:
          Argument Filtering:
           pi(wb) = [], pi(size) = [], pi(bs) = [], pi(max) = [], pi(min) = [], pi(n) = [], pi(l) = [], pi(val) = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(false) = [], pi(not) = [], pi(true) = [], pi(-) = [], pi(1) = 0, pi(+#) = 1, pi(+) = [], pi(0) = [0], pi(#) = []
          Usable Rules:
           {}
          Interpretation:
           [0](x0) = x0 + 1,
           [#] = 0
          Strict:
           {+#(0(x), 1(y)) -> +#(x, y),
            +#(1(x), 1(y)) -> +#(x, y),
            +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
          Weak:
           {           0(#()) -> #(),
                    +(x, #()) -> x,
                +(x, +(y, z)) -> +(+(x, y), z),
                    +(#(), x) -> x,
                +(0(x), 0(y)) -> 0(+(x, y)),
                +(0(x), 1(y)) -> 1(+(x, y)),
                +(1(x), 0(y)) -> 1(+(x, y)),
                +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                    -(x, #()) -> x,
                    -(#(), x) -> #(),
                -(0(x), 0(y)) -> 0(-(x, y)),
                -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                -(1(x), 0(y)) -> 1(-(x, y)),
                -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
                ge(#(), 0(x)) -> ge(#(), x),
                ge(#(), 1(x)) -> false(),
               ge(0(x), 0(y)) -> ge(x, y),
               ge(0(x), 1(y)) -> not(ge(y, x)),
               ge(1(x), 0(y)) -> ge(x, y),
               ge(1(x), 1(y)) -> ge(x, y),
                    val(l(x)) -> x,
              val(n(x, y, z)) -> x,
                    min(l(x)) -> x,
              min(n(x, y, z)) -> min(y),
                    max(l(x)) -> x,
              max(n(x, y, z)) -> max(z),
                     bs(l(x)) -> true(),
               bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                   size(l(x)) -> 1(#()),
             size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                     wb(l(x)) -> true(),
               wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
          EDG:
           {(+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
            (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
            (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
            (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
            (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
            (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
            (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
            (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
            (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))}
           SCCS:
            Scc:
             {+#(0(x), 1(y)) -> +#(x, y),
              +#(1(x), 1(y)) -> +#(x, y),
              +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
            SCC:
             Strict:
              {+#(0(x), 1(y)) -> +#(x, y),
               +#(1(x), 1(y)) -> +#(x, y),
               +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
             Weak:
             {           0(#()) -> #(),
                      +(x, #()) -> x,
                  +(x, +(y, z)) -> +(+(x, y), z),
                      +(#(), x) -> x,
                  +(0(x), 0(y)) -> 0(+(x, y)),
                  +(0(x), 1(y)) -> 1(+(x, y)),
                  +(1(x), 0(y)) -> 1(+(x, y)),
                  +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                      -(x, #()) -> x,
                      -(#(), x) -> #(),
                  -(0(x), 0(y)) -> 0(-(x, y)),
                  -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                  -(1(x), 0(y)) -> 1(-(x, y)),
                  -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
                  ge(#(), 0(x)) -> ge(#(), x),
                  ge(#(), 1(x)) -> false(),
                 ge(0(x), 0(y)) -> ge(x, y),
                 ge(0(x), 1(y)) -> not(ge(y, x)),
                 ge(1(x), 0(y)) -> ge(x, y),
                 ge(1(x), 1(y)) -> ge(x, y),
                      val(l(x)) -> x,
                val(n(x, y, z)) -> x,
                      min(l(x)) -> x,
                min(n(x, y, z)) -> min(y),
                      max(l(x)) -> x,
                max(n(x, y, z)) -> max(z),
                       bs(l(x)) -> true(),
                 bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                     size(l(x)) -> 1(#()),
               size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                       wb(l(x)) -> true(),
                 wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
             POLY:
              Argument Filtering:
               pi(wb) = [], pi(size) = [], pi(bs) = [], pi(max) = [], pi(min) = [], pi(n) = [], pi(l) = [], pi(val) = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(false) = [], pi(not) = [], pi(true) = [], pi(-) = [], pi(1) = [0], pi(+#) = 1, pi(+) = [], pi(0) = [], pi(#) = []
              Usable Rules:
               {}
              Interpretation:
               [1](x0) = x0 + 1,
               [#] = 0
              Strict:
               {+#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
              Weak:
               {           0(#()) -> #(),
                        +(x, #()) -> x,
                    +(x, +(y, z)) -> +(+(x, y), z),
                        +(#(), x) -> x,
                    +(0(x), 0(y)) -> 0(+(x, y)),
                    +(0(x), 1(y)) -> 1(+(x, y)),
                    +(1(x), 0(y)) -> 1(+(x, y)),
                    +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                        -(x, #()) -> x,
                        -(#(), x) -> #(),
                    -(0(x), 0(y)) -> 0(-(x, y)),
                    -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                    -(1(x), 0(y)) -> 1(-(x, y)),
                    -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
                    ge(#(), 0(x)) -> ge(#(), x),
                    ge(#(), 1(x)) -> false(),
                   ge(0(x), 0(y)) -> ge(x, y),
                   ge(0(x), 1(y)) -> not(ge(y, x)),
                   ge(1(x), 0(y)) -> ge(x, y),
                   ge(1(x), 1(y)) -> ge(x, y),
                        val(l(x)) -> x,
                  val(n(x, y, z)) -> x,
                        min(l(x)) -> x,
                  min(n(x, y, z)) -> min(y),
                        max(l(x)) -> x,
                  max(n(x, y, z)) -> max(z),
                         bs(l(x)) -> true(),
                   bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                       size(l(x)) -> 1(#()),
                 size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                         wb(l(x)) -> true(),
                   wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
              EDG:
               {(+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))}
               SCCS:
                Scc:
                 {+#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
                SCC:
                 Strict:
                  {+#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
                 Weak:
                 {           0(#()) -> #(),
                          +(x, #()) -> x,
                      +(x, +(y, z)) -> +(+(x, y), z),
                          +(#(), x) -> x,
                      +(0(x), 0(y)) -> 0(+(x, y)),
                      +(0(x), 1(y)) -> 1(+(x, y)),
                      +(1(x), 0(y)) -> 1(+(x, y)),
                      +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                          -(x, #()) -> x,
                          -(#(), x) -> #(),
                      -(0(x), 0(y)) -> 0(-(x, y)),
                      -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                      -(1(x), 0(y)) -> 1(-(x, y)),
                      -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
                      ge(#(), 0(x)) -> ge(#(), x),
                      ge(#(), 1(x)) -> false(),
                     ge(0(x), 0(y)) -> ge(x, y),
                     ge(0(x), 1(y)) -> not(ge(y, x)),
                     ge(1(x), 0(y)) -> ge(x, y),
                     ge(1(x), 1(y)) -> ge(x, y),
                          val(l(x)) -> x,
                    val(n(x, y, z)) -> x,
                          min(l(x)) -> x,
                    min(n(x, y, z)) -> min(y),
                          max(l(x)) -> x,
                    max(n(x, y, z)) -> max(z),
                           bs(l(x)) -> true(),
                     bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                         size(l(x)) -> 1(#()),
                   size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                           wb(l(x)) -> true(),
                     wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
                 POLY:
                  Argument Filtering:
                   pi(wb) = [], pi(size) = [], pi(bs) = [], pi(max) = [], pi(min) = [], pi(n) = [], pi(l) = [], pi(val) = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(false) = [], pi(not) = [], pi(true) = [], pi(-) = [], pi(1) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(0) = 0, pi(#) = []
                  Usable Rules:
                   {}
                  Interpretation:
                   [+#](x0, x1) = x0 + x1,
                   [+](x0, x1) = x0 + x1,
                   [1](x0) = x0 + 1,
                   [#] = 0
                  Strict:
                   {}
                  Weak:
                   {           0(#()) -> #(),
                            +(x, #()) -> x,
                        +(x, +(y, z)) -> +(+(x, y), z),
                            +(#(), x) -> x,
                        +(0(x), 0(y)) -> 0(+(x, y)),
                        +(0(x), 1(y)) -> 1(+(x, y)),
                        +(1(x), 0(y)) -> 1(+(x, y)),
                        +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                            -(x, #()) -> x,
                            -(#(), x) -> #(),
                        -(0(x), 0(y)) -> 0(-(x, y)),
                        -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                        -(1(x), 0(y)) -> 1(-(x, y)),
                        -(1(x), 1(y)) -> 0(-(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(x, #()) -> true(),
                        ge(#(), 0(x)) -> ge(#(), x),
                        ge(#(), 1(x)) -> false(),
                       ge(0(x), 0(y)) -> ge(x, y),
                       ge(0(x), 1(y)) -> not(ge(y, x)),
                       ge(1(x), 0(y)) -> ge(x, y),
                       ge(1(x), 1(y)) -> ge(x, y),
                            val(l(x)) -> x,
                      val(n(x, y, z)) -> x,
                            min(l(x)) -> x,
                      min(n(x, y, z)) -> min(y),
                            max(l(x)) -> x,
                      max(n(x, y, z)) -> max(z),
                             bs(l(x)) -> true(),
                       bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z))),
                           size(l(x)) -> 1(#()),
                     size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#())),
                             wb(l(x)) -> true(),
                       wb(n(x, y, z)) -> and(if(ge(size(y), size(z)), ge(1(#()), -(size(y), size(z))), ge(1(#()), -(size(z), size(y)))), and(wb(y), wb(z)))}
                  Qed