MAYBE
Time: 0.018181
TRS:
 {            0 #() -> #(),
          +(x, #()) -> x,
          +(#(), x) -> x,
        +(0 x, 0 y) -> 0 +(x, y),
        +(0 x, 1 y) -> 1 +(x, y),
      +(+(x, y), z) -> +(x, +(y, z)),
        +(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 false() -> true(),
         not true() -> false(),
  if(false(), x, y) -> y,
   if(true(), x, y) -> x,
         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),
           log' #() -> #(),
           log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()),
           log' 1 x -> +(log' x, 1 #()),
              log x -> -(log' x, 1 #())}
 DP:
  DP:
   {  +#(0 x, 0 y) -> 0# +(x, y),
      +#(0 x, 0 y) -> +#(x, y),
      +#(0 x, 1 y) -> +#(x, y),
    +#(+(x, y), z) -> +#(x, +(y, z)),
    +#(+(x, y), z) -> +#(y, z),
      +#(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),
         log'# 0 x -> +#(log' x, 1 #()),
         log'# 0 x -> if#(ge(x, 1 #()), +(log' x, 1 #()), #()),
         log'# 0 x -> ge#(x, 1 #()),
         log'# 0 x -> log'# x,
         log'# 1 x -> +#(log' x, 1 #()),
         log'# 1 x -> log'# x,
            log# x -> -#(log' x, 1 #()),
            log# x -> log'# x}
  TRS:
  {            0 #() -> #(),
           +(x, #()) -> x,
           +(#(), x) -> x,
         +(0 x, 0 y) -> 0 +(x, y),
         +(0 x, 1 y) -> 1 +(x, y),
       +(+(x, y), z) -> +(x, +(y, z)),
         +(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 false() -> true(),
          not true() -> false(),
   if(false(), x, y) -> y,
    if(true(), x, y) -> x,
          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),
            log' #() -> #(),
            log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()),
            log' 1 x -> +(log' x, 1 #()),
               log x -> -(log' x, 1 #())}
  UR:
   {            0 #() -> #(),
            +(x, #()) -> x,
            +(#(), x) -> x,
          +(0 x, 0 y) -> 0 +(x, y),
          +(0 x, 1 y) -> 1 +(x, y),
        +(+(x, y), z) -> +(x, +(y, z)),
          +(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 false() -> true(),
           not true() -> false(),
    if(false(), x, y) -> y,
     if(true(), x, y) -> x,
           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),
             log' #() -> #(),
             log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()),
             log' 1 x -> +(log' x, 1 #()),
              a(w, v) -> w,
              a(w, v) -> v}
   EDG:
    {(+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(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) -> 0# +(+(x, y), 1 #()))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(y, z))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(x, y))
     (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(x, y))
     (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (log'# 0 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(y, z))
     (log'# 0 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(x, +(y, z)))
     (log'# 0 x -> +#(log' x, 1 #()), +#(0 x, 1 y) -> +#(x, y))
     (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(x, y))
     (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (log'# 1 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(y, z))
     (log'# 1 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(x, +(y, z)))
     (log'# 1 x -> +#(log' x, 1 #()), +#(0 x, 1 y) -> +#(x, y))
     (log'# 1 x -> log'# x, log'# 1 x -> log'# x)
     (log'# 1 x -> log'# x, log'# 1 x -> +#(log' x, 1 #()))
     (log'# 1 x -> log'# x, log'# 0 x -> log'# x)
     (log'# 1 x -> log'# x, log'# 0 x -> ge#(x, 1 #()))
     (log'# 1 x -> log'# x, log'# 0 x -> if#(ge(x, 1 #()), +(log' x, 1 #()), #()))
     (log'# 1 x -> log'# x, log'# 0 x -> +#(log' x, 1 #()))
     (ge#(#(), 0 x) -> ge#(#(), x), ge#(#(), 0 x) -> ge#(#(), x))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(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) -> 0# +(+(x, y), 1 #()))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(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) -> 0# +(+(x, y), 1 #()))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (-#(0 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y))
     (-#(0 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y))
     (-#(0 x, 0 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y))
     (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #()))
     (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y))
     (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y))
     (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y))
     (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y))
     (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y))
     (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y))
     (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #()))
     (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y))
     (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y))
     (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y))
     (ge#(0 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y))
     (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#(0 x, 1 y) -> ge#(y, x))
     (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, 0 y) -> ge#(x, y))
     (ge#(0 x, 0 y) -> ge#(x, y), ge#(#(), 0 x) -> ge#(#(), x))
     (ge#(1 x, 1 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y))
     (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#(0 x, 1 y) -> ge#(y, x))
     (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, 0 y) -> ge#(x, y))
     (ge#(1 x, 1 y) -> ge#(x, y), ge#(#(), 0 x) -> ge#(#(), x))
     (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))
     (ge#(1 x, 0 y) -> ge#(x, y), ge#(#(), 0 x) -> ge#(#(), 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, 1 y) -> not# ge(y, x))
     (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#(1 x, 0 y) -> ge#(x, y))
     (ge#(1 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y))
     (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y))
     (-#(1 x, 1 y) -> -#(x, y), -#(0 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, 1 y) -> -#(-(x, y), 1 #()))
     (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y))
     (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y))
     (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y))
     (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y))
     (-#(0 x, 1 y) -> -#(x, y), -#(0 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, 1 y) -> -#(-(x, y), 1 #()))
     (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y))
     (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y))
     (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 0 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, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 0 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, 1 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(+(x, y), z) -> +#(y, z), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(0 x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(0 x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #()))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (log# x -> log'# x, log'# 0 x -> +#(log' x, 1 #()))
     (log# x -> log'# x, log'# 0 x -> if#(ge(x, 1 #()), +(log' x, 1 #()), #()))
     (log# x -> log'# x, log'# 0 x -> ge#(x, 1 #()))
     (log# x -> log'# x, log'# 0 x -> log'# x)
     (log# x -> log'# x, log'# 1 x -> +#(log' x, 1 #()))
     (log# x -> log'# x, log'# 1 x -> log'# x)
     (log'# 0 x -> log'# x, log'# 0 x -> +#(log' x, 1 #()))
     (log'# 0 x -> log'# x, log'# 0 x -> if#(ge(x, 1 #()), +(log' x, 1 #()), #()))
     (log'# 0 x -> log'# x, log'# 0 x -> ge#(x, 1 #()))
     (log'# 0 x -> log'# x, log'# 0 x -> log'# x)
     (log'# 0 x -> log'# x, log'# 1 x -> +#(log' x, 1 #()))
     (log'# 0 x -> log'# x, log'# 1 x -> log'# x)
     (log# x -> -#(log' x, 1 #()), -#(0 x, 1 y) -> -#(x, y))
     (log# x -> -#(log' x, 1 #()), -#(0 x, 1 y) -> -#(-(x, y), 1 #()))
     (log# x -> -#(log' x, 1 #()), -#(1 x, 1 y) -> 0# -(x, y))
     (log# x -> -#(log' x, 1 #()), -#(1 x, 1 y) -> -#(x, y))
     (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 1 y) -> not# ge(y, x))
     (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 1 y) -> ge#(y, x))
     (log'# 0 x -> ge#(x, 1 #()), ge#(1 x, 1 y) -> ge#(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) -> 0# -(x, y))
     (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 1 y) -> -#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 0 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, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))}
    STATUS:
     arrows: 0.828889
     SCCS (5):
      Scc:
       {log'# 0 x -> log'# x,
        log'# 1 x -> log'# x}
      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:
       {  +#(0 x, 0 y) -> +#(x, y),
          +#(0 x, 1 y) -> +#(x, y),
        +#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z),
          +#(1 x, 0 y) -> +#(x, y),
          +#(1 x, 1 y) -> +#(x, y),
          +#(1 x, 1 y) -> +#(+(x, y), 1 #())}
      
      
      SCC (2):
       Strict:
        {log'# 0 x -> log'# x,
         log'# 1 x -> log'# x}
       Weak:
       {            0 #() -> #(),
                +(x, #()) -> x,
                +(#(), x) -> x,
              +(0 x, 0 y) -> 0 +(x, y),
              +(0 x, 1 y) -> 1 +(x, y),
            +(+(x, y), z) -> +(x, +(y, z)),
              +(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 false() -> true(),
               not true() -> false(),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
               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),
                 log' #() -> #(),
                 log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()),
                 log' 1 x -> +(log' x, 1 #()),
                    log x -> -(log' x, 1 #())}
       Open
      
      
      
      
      SCC (4):
       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) -> x,
              +(0 x, 0 y) -> 0 +(x, y),
              +(0 x, 1 y) -> 1 +(x, y),
            +(+(x, y), z) -> +(x, +(y, z)),
              +(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 false() -> true(),
               not true() -> false(),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
               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),
                 log' #() -> #(),
                 log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()),
                 log' 1 x -> +(log' x, 1 #()),
                    log x -> -(log' x, 1 #())}
       Open
      SCC (1):
       Strict:
        {ge#(#(), 0 x) -> ge#(#(), x)}
       Weak:
       {            0 #() -> #(),
                +(x, #()) -> x,
                +(#(), x) -> x,
              +(0 x, 0 y) -> 0 +(x, y),
              +(0 x, 1 y) -> 1 +(x, y),
            +(+(x, y), z) -> +(x, +(y, z)),
              +(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 false() -> true(),
               not true() -> false(),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
               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),
                 log' #() -> #(),
                 log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()),
                 log' 1 x -> +(log' x, 1 #()),
                    log x -> -(log' x, 1 #())}
       Open
      
      
      SCC (5):
       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) -> x,
              +(0 x, 0 y) -> 0 +(x, y),
              +(0 x, 1 y) -> 1 +(x, y),
            +(+(x, y), z) -> +(x, +(y, z)),
              +(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 false() -> true(),
               not true() -> false(),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
               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),
                 log' #() -> #(),
                 log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()),
                 log' 1 x -> +(log' x, 1 #()),
                    log x -> -(log' x, 1 #())}
       Open
      
      
      SCC (7):
       Strict:
        {  +#(0 x, 0 y) -> +#(x, y),
           +#(0 x, 1 y) -> +#(x, y),
         +#(+(x, y), z) -> +#(x, +(y, z)),
         +#(+(x, y), z) -> +#(y, z),
           +#(1 x, 0 y) -> +#(x, y),
           +#(1 x, 1 y) -> +#(x, y),
           +#(1 x, 1 y) -> +#(+(x, y), 1 #())}
       Weak:
       {            0 #() -> #(),
                +(x, #()) -> x,
                +(#(), x) -> x,
              +(0 x, 0 y) -> 0 +(x, y),
              +(0 x, 1 y) -> 1 +(x, y),
            +(+(x, y), z) -> +(x, +(y, z)),
              +(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 false() -> true(),
               not true() -> false(),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
               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),
                 log' #() -> #(),
                 log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()),
                 log' 1 x -> +(log' x, 1 #()),
                    log x -> -(log' x, 1 #())}
       Open