MAYBE

Problem:
 0(#()) -> #()
 +(#(),x) -> x
 +(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,y),z) -> +(x,+(y,z))
 -(#(),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()
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 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)
 ge(x,#()) -> true()
 ge(#(),0(x)) -> ge(#(),x)
 ge(#(),1(x)) -> false()
 log(x) -> -(log'(x),1(#()))
 log'(#()) -> #()
 log'(1(x)) -> +(log'(x),1(#()))
 log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())

Proof:
 DP Processor:
  DPs:
   +#(0(x),0(y)) -> +#(x,y)
   +#(0(x),0(y)) -> 0#(+(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(#()))
   +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   -#(0(x),0(y)) -> -#(x,y)
   -#(0(x),0(y)) -> 0#(-(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)
   -#(1(x),1(y)) -> 0#(-(x,y))
   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#(1(x),0(y)) -> ge#(x,y)
   ge#(1(x),1(y)) -> ge#(x,y)
   ge#(#(),0(x)) -> ge#(#(),x)
   log#(x) -> log'#(x)
   log#(x) -> -#(log'(x),1(#()))
   log'#(1(x)) -> log'#(x)
   log'#(1(x)) -> +#(log'(x),1(#()))
   log'#(0(x)) -> log'#(x)
   log'#(0(x)) -> +#(log'(x),1(#()))
   log'#(0(x)) -> ge#(x,1(#()))
   log'#(0(x)) -> if#(ge(x,1(#())),+(log'(x),1(#())),#())
  TRS:
   0(#()) -> #()
   +(#(),x) -> x
   +(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,y),z) -> +(x,+(y,z))
   -(#(),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()
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   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)
   ge(x,#()) -> true()
   ge(#(),0(x)) -> ge(#(),x)
   ge(#(),1(x)) -> false()
   log(x) -> -(log'(x),1(#()))
   log'(#()) -> #()
   log'(1(x)) -> +(log'(x),1(#()))
   log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
  ADG Processor:
   DPs:
    +#(0(x),0(y)) -> +#(x,y)
    +#(0(x),0(y)) -> 0#(+(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(#()))
    +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z))
    -#(0(x),0(y)) -> -#(x,y)
    -#(0(x),0(y)) -> 0#(-(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)
    -#(1(x),1(y)) -> 0#(-(x,y))
    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#(1(x),0(y)) -> ge#(x,y)
    ge#(1(x),1(y)) -> ge#(x,y)
    ge#(#(),0(x)) -> ge#(#(),x)
    log#(x) -> log'#(x)
    log#(x) -> -#(log'(x),1(#()))
    log'#(1(x)) -> log'#(x)
    log'#(1(x)) -> +#(log'(x),1(#()))
    log'#(0(x)) -> log'#(x)
    log'#(0(x)) -> +#(log'(x),1(#()))
    log'#(0(x)) -> ge#(x,1(#()))
    log'#(0(x)) -> if#(ge(x,1(#())),+(log'(x),1(#())),#())
   TRS:
    0(#()) -> #()
    +(#(),x) -> x
    +(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,y),z) -> +(x,+(y,z))
    -(#(),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()
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    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)
    ge(x,#()) -> true()
    ge(#(),0(x)) -> ge(#(),x)
    ge(#(),1(x)) -> false()
    log(x) -> -(log'(x),1(#()))
    log'(#()) -> #()
    log'(1(x)) -> +(log'(x),1(#()))
    log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
   graph:
    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)) -> +#(log'(x),1(#()))
    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),1(#())) -> +#(0(x),1(y)) -> +#(x,y)
    log'#(1(x)) -> +#(log'(x),1(#())) -> +#(1(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)) -> 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'#(0(x)) -> log'#(x) -> log'#(1(x)) -> log'#(x)
    log'#(0(x)) -> log'#(x) -> log'#(1(x)) -> +#(log'(x),1(#()))
    log'#(0(x)) -> log'#(x) -> log'#(0(x)) -> log'#(x)
    log'#(0(x)) -> log'#(x) -> log'#(0(x)) -> +#(log'(x),1(#()))
    log'#(0(x)) -> log'#(x) -> log'#(0(x)) -> ge#(x,1(#()))
    log'#(0(x)) -> log'#(x) ->
    log'#(0(x)) -> if#(ge(x,1(#())),+(log'(x),1(#())),#())
    log'#(0(x)) -> ge#(x,1(#())) -> ge#(0(x),1(y)) -> ge#(y,x)
    log'#(0(x)) -> ge#(x,1(#())) -> ge#(0(x),1(y)) -> not#(ge(y,x))
    log'#(0(x)) -> ge#(x,1(#())) -> ge#(1(x),1(y)) -> ge#(x,y)
    log'#(0(x)) -> +#(log'(x),1(#())) -> +#(0(x),1(y)) -> +#(x,y)
    log'#(0(x)) -> +#(log'(x),1(#())) -> +#(1(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)) -> 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#(x) -> log'#(x) -> log'#(1(x)) -> log'#(x)
    log#(x) -> log'#(x) -> log'#(1(x)) -> +#(log'(x),1(#()))
    log#(x) -> log'#(x) -> log'#(0(x)) -> log'#(x)
    log#(x) -> log'#(x) -> log'#(0(x)) -> +#(log'(x),1(#()))
    log#(x) -> log'#(x) -> log'#(0(x)) -> ge#(x,1(#()))
    log#(x) -> log'#(x) ->
    log'#(0(x)) -> if#(ge(x,1(#())),+(log'(x),1(#())),#())
    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)) -> -#(x,y)
    log#(x) -> -#(log'(x),1(#())) -> -#(1(x),1(y)) -> 0#(-(x,y))
    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)) -> 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#(1(x),0(y)) -> ge#(x,y)
    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#(#(),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)) -> 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#(1(x),0(y)) -> ge#(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#(#(),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)) -> ge#(y,x)
    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#(1(x),0(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)) -> ge#(y,x) -> 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)) -> 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#(1(x),0(y)) -> ge#(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#(#(),0(x)) -> ge#(#(),x)
    ge#(#(),0(x)) -> ge#(#(),x) -> ge#(#(),0(x)) -> ge#(#(),x)
    -#(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) -> -#(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)) -> -#(x,y)
    -#(1(x),1(y)) -> -#(x,y) -> -#(1(x),1(y)) -> 0#(-(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))
    -#(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)) -> -#(x,y)
    -#(1(x),0(y)) -> -#(x,y) -> -#(1(x),1(y)) -> 0#(-(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),1(#())) -> -#(1(x),1(y)) -> 0#(-(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) -> -#(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)) -> -#(x,y)
    -#(0(x),1(y)) -> -#(x,y) -> -#(1(x),1(y)) -> 0#(-(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))
    -#(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)) -> -#(x,y)
    -#(0(x),0(y)) -> -#(x,y) -> -#(1(x),1(y)) -> 0#(-(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),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) -> +#(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) -> +#(0(x),1(y)) -> +#(x,y)
    +#(1(x),1(y)) -> +#(x,y) -> +#(1(x),0(y)) -> +#(x,y)
    +#(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(#()))
    +#(1(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(1(x),1(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z)
    +#(1(x),1(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(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))
    +#(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(#()))
    +#(1(x),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(1(x),0(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z)
    +#(1(x),0(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(y,z) -> +#(0(x),0(y)) -> +#(x,y)
    +#(+(x,y),z) -> +#(y,z) -> +#(0(x),0(y)) -> 0#(+(x,y))
    +#(+(x,y),z) -> +#(y,z) -> +#(0(x),1(y)) -> +#(x,y)
    +#(+(x,y),z) -> +#(y,z) -> +#(1(x),0(y)) -> +#(x,y)
    +#(+(x,y),z) -> +#(y,z) -> +#(1(x),1(y)) -> +#(x,y)
    +#(+(x,y),z) -> +#(y,z) -> +#(1(x),1(y)) -> +#(+(x,y),1(#()))
    +#(+(x,y),z) -> +#(y,z) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(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)) -> +#(0(x),1(y)) -> +#(x,y)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(1(x),0(y)) -> +#(x,y)
    +#(+(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(#()))
    +#(+(x,y),z) -> +#(x,+(y,z)) ->
    +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(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) -> +#(0(x),1(y)) -> +#(x,y)
    +#(0(x),1(y)) -> +#(x,y) -> +#(1(x),0(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(#()))
    +#(0(x),1(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(0(x),1(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z)
    +#(0(x),1(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(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))
    +#(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(#()))
    +#(0(x),0(y)) -> +#(x,y) -> +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
    +#(0(x),0(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z)
    +#(0(x),0(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z))
   SCC Processor:
    #sccs: 5
    #rules: 19
    #arcs: 154/900
    DPs:
     -#(1(x),1(y)) -> -#(x,y)
     -#(1(x),0(y)) -> -#(x,y)
     -#(0(x),1(y)) -> -#(-(x,y),1(#()))
     -#(0(x),1(y)) -> -#(x,y)
     -#(0(x),0(y)) -> -#(x,y)
    TRS:
     0(#()) -> #()
     +(#(),x) -> x
     +(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,y),z) -> +(x,+(y,z))
     -(#(),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()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,#()) -> true()
     ge(#(),0(x)) -> ge(#(),x)
     ge(#(),1(x)) -> false()
     log(x) -> -(log'(x),1(#()))
     log'(#()) -> #()
     log'(1(x)) -> +(log'(x),1(#()))
     log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
    Open
    
    DPs:
     log'#(1(x)) -> log'#(x)
     log'#(0(x)) -> log'#(x)
    TRS:
     0(#()) -> #()
     +(#(),x) -> x
     +(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,y),z) -> +(x,+(y,z))
     -(#(),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()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,#()) -> true()
     ge(#(),0(x)) -> ge(#(),x)
     ge(#(),1(x)) -> false()
     log(x) -> -(log'(x),1(#()))
     log'(#()) -> #()
     log'(1(x)) -> +(log'(x),1(#()))
     log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
    Open
    
    DPs:
     +#(+(x,y),z) -> +#(x,+(y,z))
     +#(+(x,y),z) -> +#(y,z)
     +#(1(x),1(y)) -> +#(+(x,y),1(#()))
     +#(1(x),1(y)) -> +#(x,y)
     +#(1(x),0(y)) -> +#(x,y)
     +#(0(x),1(y)) -> +#(x,y)
     +#(0(x),0(y)) -> +#(x,y)
    TRS:
     0(#()) -> #()
     +(#(),x) -> x
     +(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,y),z) -> +(x,+(y,z))
     -(#(),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()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,#()) -> true()
     ge(#(),0(x)) -> ge(#(),x)
     ge(#(),1(x)) -> false()
     log(x) -> -(log'(x),1(#()))
     log'(#()) -> #()
     log'(1(x)) -> +(log'(x),1(#()))
     log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
    Open
    
    DPs:
     ge#(1(x),1(y)) -> ge#(x,y)
     ge#(1(x),0(y)) -> ge#(x,y)
     ge#(0(x),1(y)) -> ge#(y,x)
     ge#(0(x),0(y)) -> ge#(x,y)
    TRS:
     0(#()) -> #()
     +(#(),x) -> x
     +(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,y),z) -> +(x,+(y,z))
     -(#(),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()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,#()) -> true()
     ge(#(),0(x)) -> ge(#(),x)
     ge(#(),1(x)) -> false()
     log(x) -> -(log'(x),1(#()))
     log'(#()) -> #()
     log'(1(x)) -> +(log'(x),1(#()))
     log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
    Open
    
    DPs:
     ge#(#(),0(x)) -> ge#(#(),x)
    TRS:
     0(#()) -> #()
     +(#(),x) -> x
     +(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,y),z) -> +(x,+(y,z))
     -(#(),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()
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     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)
     ge(x,#()) -> true()
     ge(#(),0(x)) -> ge(#(),x)
     ge(#(),1(x)) -> false()
     log(x) -> -(log'(x),1(#()))
     log'(#()) -> #()
     log'(1(x)) -> +(log'(x),1(#()))
     log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
    Open