MAYBE
MAYBE
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(#()))
 }
 DUP: We consider a duplicating system.
  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(#()))
   }
  Fail