YES

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(#())),#())
  EDG 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(#())),#())
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [-#](x0, x1) = x1,
      
      [log'](x0) = x0,
      
      [log](x0) = x0,
      
      [ge](x0, x1) = x0,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [false] = 0,
      
      [not](x0) = 1,
      
      [true] = 0,
      
      [-](x0, x1) = x0,
      
      [1](x0) = x0 + 1,
      
      [+](x0, x1) = x0 + x1,
      
      [0](x0) = x0 + 1,
      
      [#] = 0
     orientation:
      -#(1(x),1(y)) = y + 1 >= y = -#(x,y)
      
      -#(1(x),0(y)) = y + 1 >= y = -#(x,y)
      
      -#(0(x),1(y)) = y + 1 >= 1 = -#(-(x,y),1(#()))
      
      -#(0(x),1(y)) = y + 1 >= y = -#(x,y)
      
      -#(0(x),0(y)) = y + 1 >= y = -#(x,y)
      
      0(#()) = 1 >= 0 = #()
      
      +(#(),x) = x >= x = x
      
      +(x,#()) = x >= x = x
      
      +(0(x),0(y)) = x + y + 2 >= x + y + 1 = 0(+(x,y))
      
      +(0(x),1(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
      
      +(1(x),0(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
      
      +(1(x),1(y)) = x + y + 2 >= x + y + 2 = 0(+(+(x,y),1(#())))
      
      +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
      
      -(#(),x) = 0 >= 0 = #()
      
      -(x,#()) = x >= x = x
      
      -(0(x),0(y)) = x + 1 >= x + 1 = 0(-(x,y))
      
      -(0(x),1(y)) = x + 1 >= x + 1 = 1(-(-(x,y),1(#())))
      
      -(1(x),0(y)) = x + 1 >= x + 1 = 1(-(x,y))
      
      -(1(x),1(y)) = x + 1 >= x + 1 = 0(-(x,y))
      
      not(true()) = 1 >= 0 = false()
      
      not(false()) = 1 >= 0 = true()
      
      if(true(),x,y) = x + y >= x = x
      
      if(false(),x,y) = x + y >= y = y
      
      ge(0(x),0(y)) = x + 1 >= x = ge(x,y)
      
      ge(0(x),1(y)) = x + 1 >= 1 = not(ge(y,x))
      
      ge(1(x),0(y)) = x + 1 >= x = ge(x,y)
      
      ge(1(x),1(y)) = x + 1 >= x = ge(x,y)
      
      ge(x,#()) = x >= 0 = true()
      
      ge(#(),0(x)) = 0 >= 0 = ge(#(),x)
      
      ge(#(),1(x)) = 0 >= 0 = false()
      
      log(x) = x >= x = -(log'(x),1(#()))
      
      log'(#()) = 0 >= 0 = #()
      
      log'(1(x)) = x + 1 >= x + 1 = +(log'(x),1(#()))
      
      log'(0(x)) = x + 1 >= x + 1 = if(ge(x,1(#())),+(log'(x),1(#())),#())
     problem:
      DPs:
       -#(0(x),1(y)) -> -#(-(x,y),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(#())),#())
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [-#](x0, x1) = x0,
       
       [log'](x0) = x0,
       
       [log](x0) = x0,
       
       [ge](x0, x1) = 0,
       
       [if](x0, x1, x2) = x1 + x2,
       
       [false] = 0,
       
       [not](x0) = 0,
       
       [true] = 0,
       
       [-](x0, x1) = x0,
       
       [1](x0) = x0 + 1,
       
       [+](x0, x1) = x0 + x1,
       
       [0](x0) = x0 + 1,
       
       [#] = 0
      orientation:
       -#(0(x),1(y)) = x + 1 >= x = -#(-(x,y),1(#()))
       
       0(#()) = 1 >= 0 = #()
       
       +(#(),x) = x >= x = x
       
       +(x,#()) = x >= x = x
       
       +(0(x),0(y)) = x + y + 2 >= x + y + 1 = 0(+(x,y))
       
       +(0(x),1(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
       
       +(1(x),0(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
       
       +(1(x),1(y)) = x + y + 2 >= x + y + 2 = 0(+(+(x,y),1(#())))
       
       +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
       
       -(#(),x) = 0 >= 0 = #()
       
       -(x,#()) = x >= x = x
       
       -(0(x),0(y)) = x + 1 >= x + 1 = 0(-(x,y))
       
       -(0(x),1(y)) = x + 1 >= x + 1 = 1(-(-(x,y),1(#())))
       
       -(1(x),0(y)) = x + 1 >= x + 1 = 1(-(x,y))
       
       -(1(x),1(y)) = x + 1 >= x + 1 = 0(-(x,y))
       
       not(true()) = 0 >= 0 = false()
       
       not(false()) = 0 >= 0 = true()
       
       if(true(),x,y) = x + y >= x = x
       
       if(false(),x,y) = x + y >= y = y
       
       ge(0(x),0(y)) = 0 >= 0 = ge(x,y)
       
       ge(0(x),1(y)) = 0 >= 0 = not(ge(y,x))
       
       ge(1(x),0(y)) = 0 >= 0 = ge(x,y)
       
       ge(1(x),1(y)) = 0 >= 0 = ge(x,y)
       
       ge(x,#()) = 0 >= 0 = true()
       
       ge(#(),0(x)) = 0 >= 0 = ge(#(),x)
       
       ge(#(),1(x)) = 0 >= 0 = false()
       
       log(x) = x >= x = -(log'(x),1(#()))
       
       log'(#()) = 0 >= 0 = #()
       
       log'(1(x)) = x + 1 >= x + 1 = +(log'(x),1(#()))
       
       log'(0(x)) = x + 1 >= x + 1 = if(ge(x,1(#())),+(log'(x),1(#())),#())
      problem:
       DPs:
        
       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(#())),#())
      Qed
    
    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(#())),#())
    Subterm Criterion Processor:
     simple projection:
      pi(log'#) = 0
     problem:
      DPs:
       
      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(#())),#())
     Qed
    
    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(#())),#())
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [+#](x0, x1) = x0 + x1,
      
      [log'](x0) = x0,
      
      [log](x0) = x0,
      
      [ge](x0, x1) = x0 + 1,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [false] = 1,
      
      [not](x0) = 1,
      
      [true] = 0,
      
      [-](x0, x1) = x0,
      
      [1](x0) = x0 + 1,
      
      [+](x0, x1) = x0 + x1,
      
      [0](x0) = x0 + 1,
      
      [#] = 0
     orientation:
      +#(+(x,y),z) = x + y + z >= x + y + z = +#(x,+(y,z))
      
      +#(+(x,y),z) = x + y + z >= y + z = +#(y,z)
      
      +#(1(x),1(y)) = x + y + 2 >= x + y + 1 = +#(+(x,y),1(#()))
      
      +#(1(x),1(y)) = x + y + 2 >= x + y = +#(x,y)
      
      +#(1(x),0(y)) = x + y + 2 >= x + y = +#(x,y)
      
      +#(0(x),1(y)) = x + y + 2 >= x + y = +#(x,y)
      
      +#(0(x),0(y)) = x + y + 2 >= x + y = +#(x,y)
      
      0(#()) = 1 >= 0 = #()
      
      +(#(),x) = x >= x = x
      
      +(x,#()) = x >= x = x
      
      +(0(x),0(y)) = x + y + 2 >= x + y + 1 = 0(+(x,y))
      
      +(0(x),1(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
      
      +(1(x),0(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
      
      +(1(x),1(y)) = x + y + 2 >= x + y + 2 = 0(+(+(x,y),1(#())))
      
      +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
      
      -(#(),x) = 0 >= 0 = #()
      
      -(x,#()) = x >= x = x
      
      -(0(x),0(y)) = x + 1 >= x + 1 = 0(-(x,y))
      
      -(0(x),1(y)) = x + 1 >= x + 1 = 1(-(-(x,y),1(#())))
      
      -(1(x),0(y)) = x + 1 >= x + 1 = 1(-(x,y))
      
      -(1(x),1(y)) = x + 1 >= x + 1 = 0(-(x,y))
      
      not(true()) = 1 >= 1 = false()
      
      not(false()) = 1 >= 0 = true()
      
      if(true(),x,y) = x + y >= x = x
      
      if(false(),x,y) = x + y >= y = y
      
      ge(0(x),0(y)) = x + 2 >= x + 1 = ge(x,y)
      
      ge(0(x),1(y)) = x + 2 >= 1 = not(ge(y,x))
      
      ge(1(x),0(y)) = x + 2 >= x + 1 = ge(x,y)
      
      ge(1(x),1(y)) = x + 2 >= x + 1 = ge(x,y)
      
      ge(x,#()) = x + 1 >= 0 = true()
      
      ge(#(),0(x)) = 1 >= 1 = ge(#(),x)
      
      ge(#(),1(x)) = 1 >= 1 = false()
      
      log(x) = x >= x = -(log'(x),1(#()))
      
      log'(#()) = 0 >= 0 = #()
      
      log'(1(x)) = x + 1 >= x + 1 = +(log'(x),1(#()))
      
      log'(0(x)) = x + 1 >= x + 1 = if(ge(x,1(#())),+(log'(x),1(#())),#())
     problem:
      DPs:
       +#(+(x,y),z) -> +#(x,+(y,z))
       +#(+(x,y),z) -> +#(y,z)
      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(#())),#())
     Subterm Criterion Processor:
      simple projection:
       pi(+#) = 0
      problem:
       DPs:
        
       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(#())),#())
      Qed
    
    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(#())),#())
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [ge#](x0, x1) = x0 + x1,
      
      [log'](x0) = x0,
      
      [log](x0) = x0,
      
      [ge](x0, x1) = x0,
      
      [if](x0, x1, x2) = x1 + x2,
      
      [false] = 0,
      
      [not](x0) = 0,
      
      [true] = 0,
      
      [-](x0, x1) = x0,
      
      [1](x0) = x0 + 1,
      
      [+](x0, x1) = x0 + x1,
      
      [0](x0) = x0 + 1,
      
      [#] = 0
     orientation:
      ge#(1(x),1(y)) = x + y + 2 >= x + y = ge#(x,y)
      
      ge#(1(x),0(y)) = x + y + 2 >= x + y = ge#(x,y)
      
      ge#(0(x),1(y)) = x + y + 2 >= x + y = ge#(y,x)
      
      ge#(0(x),0(y)) = x + y + 2 >= x + y = ge#(x,y)
      
      0(#()) = 1 >= 0 = #()
      
      +(#(),x) = x >= x = x
      
      +(x,#()) = x >= x = x
      
      +(0(x),0(y)) = x + y + 2 >= x + y + 1 = 0(+(x,y))
      
      +(0(x),1(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
      
      +(1(x),0(y)) = x + y + 2 >= x + y + 1 = 1(+(x,y))
      
      +(1(x),1(y)) = x + y + 2 >= x + y + 2 = 0(+(+(x,y),1(#())))
      
      +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
      
      -(#(),x) = 0 >= 0 = #()
      
      -(x,#()) = x >= x = x
      
      -(0(x),0(y)) = x + 1 >= x + 1 = 0(-(x,y))
      
      -(0(x),1(y)) = x + 1 >= x + 1 = 1(-(-(x,y),1(#())))
      
      -(1(x),0(y)) = x + 1 >= x + 1 = 1(-(x,y))
      
      -(1(x),1(y)) = x + 1 >= x + 1 = 0(-(x,y))
      
      not(true()) = 0 >= 0 = false()
      
      not(false()) = 0 >= 0 = true()
      
      if(true(),x,y) = x + y >= x = x
      
      if(false(),x,y) = x + y >= y = y
      
      ge(0(x),0(y)) = x + 1 >= x = ge(x,y)
      
      ge(0(x),1(y)) = x + 1 >= 0 = not(ge(y,x))
      
      ge(1(x),0(y)) = x + 1 >= x = ge(x,y)
      
      ge(1(x),1(y)) = x + 1 >= x = ge(x,y)
      
      ge(x,#()) = x >= 0 = true()
      
      ge(#(),0(x)) = 0 >= 0 = ge(#(),x)
      
      ge(#(),1(x)) = 0 >= 0 = false()
      
      log(x) = x >= x = -(log'(x),1(#()))
      
      log'(#()) = 0 >= 0 = #()
      
      log'(1(x)) = x + 1 >= x + 1 = +(log'(x),1(#()))
      
      log'(0(x)) = x + 1 >= x + 1 = if(ge(x,1(#())),+(log'(x),1(#())),#())
     problem:
      DPs:
       
      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(#())),#())
     Qed
    
    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(#())),#())
    Subterm Criterion Processor:
     simple projection:
      pi(ge#) = 1
     problem:
      DPs:
       
      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(#())),#())
     Qed