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
 eq(#(),#()) -> true()
 eq(#(),1(y)) -> false()
 eq(1(x),#()) -> false()
 eq(#(),0(y)) -> eq(#(),y)
 eq(0(x),#()) -> eq(x,#())
 eq(1(x),1(y)) -> eq(x,y)
 eq(0(x),1(y)) -> false()
 eq(1(x),0(y)) -> false()
 eq(0(x),0(y)) -> eq(x,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(#())),#())
 *(#(),x) -> #()
 *(0(x),y) -> 0(*(x,y))
 *(1(x),y) -> +(0(*(x,y)),y)
 *(*(x,y),z) -> *(x,*(y,z))
 *(x,+(y,z)) -> +(*(x,y),*(x,z))
 app(nil(),l) -> l
 app(cons(x,l1),l2) -> cons(x,app(l1,l2))
 sum(nil()) -> 0(#())
 sum(cons(x,l)) -> +(x,sum(l))
 sum(app(l1,l2)) -> +(sum(l1),sum(l2))
 prod(nil()) -> 1(#())
 prod(cons(x,l)) -> *(x,prod(l))
 prod(app(l1,l2)) -> *(prod(l1),prod(l2))
 mem(x,nil()) -> false()
 mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
 inter(x,nil()) -> nil()
 inter(nil(),x) -> nil()
 inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
 inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
 inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
 inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
 ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
 ifinter(false(),x,l1,l2) -> inter(l1,l2)

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))
   eq#(#(),0(y)) -> eq#(#(),y)
   eq#(0(x),#()) -> eq#(x,#())
   eq#(1(x),1(y)) -> eq#(x,y)
   eq#(0(x),0(y)) -> eq#(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(#())),#())
   *#(0(x),y) -> *#(x,y)
   *#(0(x),y) -> 0#(*(x,y))
   *#(1(x),y) -> *#(x,y)
   *#(1(x),y) -> 0#(*(x,y))
   *#(1(x),y) -> +#(0(*(x,y)),y)
   *#(*(x,y),z) -> *#(y,z)
   *#(*(x,y),z) -> *#(x,*(y,z))
   *#(x,+(y,z)) -> *#(x,z)
   *#(x,+(y,z)) -> *#(x,y)
   *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
   app#(cons(x,l1),l2) -> app#(l1,l2)
   sum#(nil()) -> 0#(#())
   sum#(cons(x,l)) -> sum#(l)
   sum#(cons(x,l)) -> +#(x,sum(l))
   sum#(app(l1,l2)) -> sum#(l2)
   sum#(app(l1,l2)) -> sum#(l1)
   sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
   prod#(cons(x,l)) -> prod#(l)
   prod#(cons(x,l)) -> *#(x,prod(l))
   prod#(app(l1,l2)) -> prod#(l2)
   prod#(app(l1,l2)) -> prod#(l1)
   prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
   mem#(x,cons(y,l)) -> mem#(x,l)
   mem#(x,cons(y,l)) -> eq#(x,y)
   mem#(x,cons(y,l)) -> if#(eq(x,y),true(),mem(x,l))
   inter#(app(l1,l2),l3) -> inter#(l2,l3)
   inter#(app(l1,l2),l3) -> inter#(l1,l3)
   inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
   inter#(l1,app(l2,l3)) -> inter#(l1,l3)
   inter#(l1,app(l2,l3)) -> inter#(l1,l2)
   inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
   inter#(cons(x,l1),l2) -> mem#(x,l2)
   inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
   inter#(l1,cons(x,l2)) -> mem#(x,l1)
   inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
   ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
   ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
  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
   eq(#(),#()) -> true()
   eq(#(),1(y)) -> false()
   eq(1(x),#()) -> false()
   eq(#(),0(y)) -> eq(#(),y)
   eq(0(x),#()) -> eq(x,#())
   eq(1(x),1(y)) -> eq(x,y)
   eq(0(x),1(y)) -> false()
   eq(1(x),0(y)) -> false()
   eq(0(x),0(y)) -> eq(x,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(#())),#())
   *(#(),x) -> #()
   *(0(x),y) -> 0(*(x,y))
   *(1(x),y) -> +(0(*(x,y)),y)
   *(*(x,y),z) -> *(x,*(y,z))
   *(x,+(y,z)) -> +(*(x,y),*(x,z))
   app(nil(),l) -> l
   app(cons(x,l1),l2) -> cons(x,app(l1,l2))
   sum(nil()) -> 0(#())
   sum(cons(x,l)) -> +(x,sum(l))
   sum(app(l1,l2)) -> +(sum(l1),sum(l2))
   prod(nil()) -> 1(#())
   prod(cons(x,l)) -> *(x,prod(l))
   prod(app(l1,l2)) -> *(prod(l1),prod(l2))
   mem(x,nil()) -> false()
   mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
   inter(x,nil()) -> nil()
   inter(nil(),x) -> nil()
   inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
   inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
   inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
   inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
   ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
   ifinter(false(),x,l1,l2) -> inter(l1,l2)
  Usable Rule 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))
    eq#(#(),0(y)) -> eq#(#(),y)
    eq#(0(x),#()) -> eq#(x,#())
    eq#(1(x),1(y)) -> eq#(x,y)
    eq#(0(x),0(y)) -> eq#(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(#())),#())
    *#(0(x),y) -> *#(x,y)
    *#(0(x),y) -> 0#(*(x,y))
    *#(1(x),y) -> *#(x,y)
    *#(1(x),y) -> 0#(*(x,y))
    *#(1(x),y) -> +#(0(*(x,y)),y)
    *#(*(x,y),z) -> *#(y,z)
    *#(*(x,y),z) -> *#(x,*(y,z))
    *#(x,+(y,z)) -> *#(x,z)
    *#(x,+(y,z)) -> *#(x,y)
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    app#(cons(x,l1),l2) -> app#(l1,l2)
    sum#(nil()) -> 0#(#())
    sum#(cons(x,l)) -> sum#(l)
    sum#(cons(x,l)) -> +#(x,sum(l))
    sum#(app(l1,l2)) -> sum#(l2)
    sum#(app(l1,l2)) -> sum#(l1)
    sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
    prod#(cons(x,l)) -> prod#(l)
    prod#(cons(x,l)) -> *#(x,prod(l))
    prod#(app(l1,l2)) -> prod#(l2)
    prod#(app(l1,l2)) -> prod#(l1)
    prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
    mem#(x,cons(y,l)) -> mem#(x,l)
    mem#(x,cons(y,l)) -> eq#(x,y)
    mem#(x,cons(y,l)) -> if#(eq(x,y),true(),mem(x,l))
    inter#(app(l1,l2),l3) -> inter#(l2,l3)
    inter#(app(l1,l2),l3) -> inter#(l1,l3)
    inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
    inter#(l1,app(l2,l3)) -> inter#(l1,l3)
    inter#(l1,app(l2,l3)) -> inter#(l1,l2)
    inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
    inter#(cons(x,l1),l2) -> mem#(x,l2)
    inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
    inter#(l1,cons(x,l2)) -> mem#(x,l1)
    inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
    ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
    ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
   TRS:
    f38(x,y) -> x
    f38(x,y) -> y
    +(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))
    0(#()) -> #()
    -(#(),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))
    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()
    not(true()) -> false()
    not(false()) -> true()
    log'(#()) -> #()
    log'(1(x)) -> +(log'(x),1(#()))
    log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    *(#(),x) -> #()
    *(0(x),y) -> 0(*(x,y))
    *(1(x),y) -> +(0(*(x,y)),y)
    *(*(x,y),z) -> *(x,*(y,z))
    *(x,+(y,z)) -> +(*(x,y),*(x,z))
    sum(nil()) -> 0(#())
    sum(cons(x,l)) -> +(x,sum(l))
    sum(app(l1,l2)) -> +(sum(l1),sum(l2))
    prod(nil()) -> 1(#())
    prod(cons(x,l)) -> *(x,prod(l))
    prod(app(l1,l2)) -> *(prod(l1),prod(l2))
    mem(x,nil()) -> false()
    mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
    eq(#(),#()) -> true()
    eq(#(),1(y)) -> false()
    eq(1(x),#()) -> false()
    eq(#(),0(y)) -> eq(#(),y)
    eq(0(x),#()) -> eq(x,#())
    eq(1(x),1(y)) -> eq(x,y)
    eq(0(x),1(y)) -> false()
    eq(1(x),0(y)) -> false()
    eq(0(x),0(y)) -> eq(x,y)
    inter(x,nil()) -> nil()
    inter(nil(),x) -> nil()
    inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
    inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
    inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
    inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
    app(nil(),l) -> l
    app(cons(x,l1),l2) -> cons(x,app(l1,l2))
    ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
    ifinter(false(),x,l1,l2) -> inter(l1,l2)
   CDG 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))
     eq#(#(),0(y)) -> eq#(#(),y)
     eq#(0(x),#()) -> eq#(x,#())
     eq#(1(x),1(y)) -> eq#(x,y)
     eq#(0(x),0(y)) -> eq#(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(#())),#())
     *#(0(x),y) -> *#(x,y)
     *#(0(x),y) -> 0#(*(x,y))
     *#(1(x),y) -> *#(x,y)
     *#(1(x),y) -> 0#(*(x,y))
     *#(1(x),y) -> +#(0(*(x,y)),y)
     *#(*(x,y),z) -> *#(y,z)
     *#(*(x,y),z) -> *#(x,*(y,z))
     *#(x,+(y,z)) -> *#(x,z)
     *#(x,+(y,z)) -> *#(x,y)
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     app#(cons(x,l1),l2) -> app#(l1,l2)
     sum#(nil()) -> 0#(#())
     sum#(cons(x,l)) -> sum#(l)
     sum#(cons(x,l)) -> +#(x,sum(l))
     sum#(app(l1,l2)) -> sum#(l2)
     sum#(app(l1,l2)) -> sum#(l1)
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
     prod#(cons(x,l)) -> prod#(l)
     prod#(cons(x,l)) -> *#(x,prod(l))
     prod#(app(l1,l2)) -> prod#(l2)
     prod#(app(l1,l2)) -> prod#(l1)
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
     mem#(x,cons(y,l)) -> mem#(x,l)
     mem#(x,cons(y,l)) -> eq#(x,y)
     mem#(x,cons(y,l)) -> if#(eq(x,y),true(),mem(x,l))
     inter#(app(l1,l2),l3) -> inter#(l2,l3)
     inter#(app(l1,l2),l3) -> inter#(l1,l3)
     inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
     inter#(l1,app(l2,l3)) -> inter#(l1,l3)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2)
     inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
     inter#(cons(x,l1),l2) -> mem#(x,l2)
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
     inter#(l1,cons(x,l2)) -> mem#(x,l1)
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
    TRS:
     f38(x,y) -> x
     f38(x,y) -> y
     +(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))
     0(#()) -> #()
     -(#(),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))
     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()
     not(true()) -> false()
     not(false()) -> true()
     log'(#()) -> #()
     log'(1(x)) -> +(log'(x),1(#()))
     log'(0(x)) -> if(ge(x,1(#())),+(log'(x),1(#())),#())
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     *(#(),x) -> #()
     *(0(x),y) -> 0(*(x,y))
     *(1(x),y) -> +(0(*(x,y)),y)
     *(*(x,y),z) -> *(x,*(y,z))
     *(x,+(y,z)) -> +(*(x,y),*(x,z))
     sum(nil()) -> 0(#())
     sum(cons(x,l)) -> +(x,sum(l))
     sum(app(l1,l2)) -> +(sum(l1),sum(l2))
     prod(nil()) -> 1(#())
     prod(cons(x,l)) -> *(x,prod(l))
     prod(app(l1,l2)) -> *(prod(l1),prod(l2))
     mem(x,nil()) -> false()
     mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
     eq(#(),#()) -> true()
     eq(#(),1(y)) -> false()
     eq(1(x),#()) -> false()
     eq(#(),0(y)) -> eq(#(),y)
     eq(0(x),#()) -> eq(x,#())
     eq(1(x),1(y)) -> eq(x,y)
     eq(0(x),1(y)) -> false()
     eq(1(x),0(y)) -> false()
     eq(0(x),0(y)) -> eq(x,y)
     inter(x,nil()) -> nil()
     inter(nil(),x) -> nil()
     inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
     inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
     inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
     inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
     app(nil(),l) -> l
     app(cons(x,l1),l2) -> cons(x,app(l1,l2))
     ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
     ifinter(false(),x,l1,l2) -> inter(l1,l2)
    graph:
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> inter#(l2,l3)
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> inter#(l1,l3)
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l3)
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l2)
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(cons(x,l1),l2) -> mem#(x,l2)
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,cons(x,l2)) -> mem#(x,l1)
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> inter#(l2,l3)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> inter#(l1,l3)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l3)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l2)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(cons(x,l1),l2) -> mem#(x,l2)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,cons(x,l2)) -> mem#(x,l1)
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2) ->
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2) ->
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2) ->
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
     inter#(cons(x,l1),l2) -> mem#(x,l2) ->
     mem#(x,cons(y,l)) -> mem#(x,l)
     inter#(cons(x,l1),l2) -> mem#(x,l2) ->
     mem#(x,cons(y,l)) -> eq#(x,y)
     inter#(cons(x,l1),l2) -> mem#(x,l2) ->
     mem#(x,cons(y,l)) -> if#(eq(x,y),true(),mem(x,l))
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(app(l1,l2),l3) -> inter#(l2,l3)
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(app(l1,l2),l3) -> inter#(l1,l3)
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l3)
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l2)
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(cons(x,l1),l2) -> mem#(x,l2)
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(l1,cons(x,l2)) -> mem#(x,l1)
     inter#(app(l1,l2),l3) -> inter#(l2,l3) ->
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(app(l1,l2),l3) -> inter#(l2,l3)
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(app(l1,l2),l3) -> inter#(l1,l3)
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l3)
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l2)
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(cons(x,l1),l2) -> mem#(x,l2)
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(l1,cons(x,l2)) -> mem#(x,l1)
     inter#(app(l1,l2),l3) -> inter#(l1,l3) ->
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
     inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3)) ->
     app#(cons(x,l1),l2) -> app#(l1,l2)
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1) ->
     ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1) ->
     ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
     inter#(l1,cons(x,l2)) -> mem#(x,l1) ->
     mem#(x,cons(y,l)) -> mem#(x,l)
     inter#(l1,cons(x,l2)) -> mem#(x,l1) ->
     mem#(x,cons(y,l)) -> eq#(x,y)
     inter#(l1,cons(x,l2)) -> mem#(x,l1) ->
     mem#(x,cons(y,l)) -> if#(eq(x,y),true(),mem(x,l))
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(app(l1,l2),l3) -> inter#(l2,l3)
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(app(l1,l2),l3) -> inter#(l1,l3)
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l3)
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l2)
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(cons(x,l1),l2) -> mem#(x,l2)
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(l1,cons(x,l2)) -> mem#(x,l1)
     inter#(l1,app(l2,l3)) -> inter#(l1,l3) ->
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> inter#(l2,l3)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> inter#(l1,l3)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l3)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> inter#(l1,l2)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(cons(x,l1),l2) -> mem#(x,l2)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(l1,cons(x,l2)) -> mem#(x,l1)
     inter#(l1,app(l2,l3)) -> inter#(l1,l2) ->
     inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
     inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3)) ->
     app#(cons(x,l1),l2) -> app#(l1,l2)
     mem#(x,cons(y,l)) -> mem#(x,l) -> mem#(x,cons(y,l)) -> mem#(x,l)
     mem#(x,cons(y,l)) -> mem#(x,l) -> mem#(x,cons(y,l)) -> eq#(x,y)
     mem#(x,cons(y,l)) -> mem#(x,l) ->
     mem#(x,cons(y,l)) -> if#(eq(x,y),true(),mem(x,l))
     mem#(x,cons(y,l)) -> eq#(x,y) -> eq#(#(),0(y)) -> eq#(#(),y)
     mem#(x,cons(y,l)) -> eq#(x,y) -> eq#(0(x),#()) -> eq#(x,#())
     mem#(x,cons(y,l)) -> eq#(x,y) -> eq#(1(x),1(y)) -> eq#(x,y)
     mem#(x,cons(y,l)) -> eq#(x,y) -> eq#(0(x),0(y)) -> eq#(x,y)
     prod#(cons(x,l)) -> prod#(l) -> prod#(cons(x,l)) -> prod#(l)
     prod#(cons(x,l)) -> prod#(l) -> prod#(cons(x,l)) -> *#(x,prod(l))
     prod#(cons(x,l)) -> prod#(l) -> prod#(app(l1,l2)) -> prod#(l2)
     prod#(cons(x,l)) -> prod#(l) -> prod#(app(l1,l2)) -> prod#(l1)
     prod#(cons(x,l)) -> prod#(l) ->
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(0(x),y) -> *#(x,y)
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(0(x),y) -> 0#(*(x,y))
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(1(x),y) -> *#(x,y)
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(1(x),y) -> 0#(*(x,y))
     prod#(cons(x,l)) -> *#(x,prod(l)) ->
     *#(1(x),y) -> +#(0(*(x,y)),y)
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(*(x,y),z) -> *#(y,z)
     prod#(cons(x,l)) -> *#(x,prod(l)) ->
     *#(*(x,y),z) -> *#(x,*(y,z))
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(x,+(y,z)) -> *#(x,z)
     prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(x,+(y,z)) -> *#(x,y)
     prod#(cons(x,l)) -> *#(x,prod(l)) ->
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     prod#(app(l1,l2)) -> prod#(l2) -> prod#(cons(x,l)) -> prod#(l)
     prod#(app(l1,l2)) -> prod#(l2) ->
     prod#(cons(x,l)) -> *#(x,prod(l))
     prod#(app(l1,l2)) -> prod#(l2) -> prod#(app(l1,l2)) -> prod#(l2)
     prod#(app(l1,l2)) -> prod#(l2) -> prod#(app(l1,l2)) -> prod#(l1)
     prod#(app(l1,l2)) -> prod#(l2) ->
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
     prod#(app(l1,l2)) -> prod#(l1) -> prod#(cons(x,l)) -> prod#(l)
     prod#(app(l1,l2)) -> prod#(l1) ->
     prod#(cons(x,l)) -> *#(x,prod(l))
     prod#(app(l1,l2)) -> prod#(l1) -> prod#(app(l1,l2)) -> prod#(l2)
     prod#(app(l1,l2)) -> prod#(l1) -> prod#(app(l1,l2)) -> prod#(l1)
     prod#(app(l1,l2)) -> prod#(l1) ->
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(0(x),y) -> *#(x,y)
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(0(x),y) -> 0#(*(x,y))
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(1(x),y) -> *#(x,y)
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(1(x),y) -> 0#(*(x,y))
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(1(x),y) -> +#(0(*(x,y)),y)
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(*(x,y),z) -> *#(y,z)
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(*(x,y),z) -> *#(x,*(y,z))
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(x,+(y,z)) -> *#(x,z)
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(x,+(y,z)) -> *#(x,y)
     prod#(app(l1,l2)) -> *#(prod(l1),prod(l2)) ->
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     sum#(cons(x,l)) -> sum#(l) -> sum#(nil()) -> 0#(#())
     sum#(cons(x,l)) -> sum#(l) -> sum#(cons(x,l)) -> sum#(l)
     sum#(cons(x,l)) -> sum#(l) -> sum#(cons(x,l)) -> +#(x,sum(l))
     sum#(cons(x,l)) -> sum#(l) -> sum#(app(l1,l2)) -> sum#(l2)
     sum#(cons(x,l)) -> sum#(l) -> sum#(app(l1,l2)) -> sum#(l1)
     sum#(cons(x,l)) -> sum#(l) ->
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(0(x),0(y)) -> +#(x,y)
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(0(x),0(y)) -> 0#(+(x,y))
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(0(x),1(y)) -> +#(x,y)
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(1(x),0(y)) -> +#(x,y)
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(1(x),1(y)) -> +#(x,y)
     sum#(cons(x,l)) -> +#(x,sum(l)) ->
     +#(1(x),1(y)) -> +#(+(x,y),1(#()))
     sum#(cons(x,l)) -> +#(x,sum(l)) ->
     +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(+(x,y),z) -> +#(y,z)
     sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(+(x,y),z) -> +#(x,+(y,z))
     sum#(app(l1,l2)) -> sum#(l2) -> sum#(nil()) -> 0#(#())
     sum#(app(l1,l2)) -> sum#(l2) -> sum#(cons(x,l)) -> sum#(l)
     sum#(app(l1,l2)) -> sum#(l2) -> sum#(cons(x,l)) -> +#(x,sum(l))
     sum#(app(l1,l2)) -> sum#(l2) -> sum#(app(l1,l2)) -> sum#(l2)
     sum#(app(l1,l2)) -> sum#(l2) -> sum#(app(l1,l2)) -> sum#(l1)
     sum#(app(l1,l2)) -> sum#(l2) ->
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
     sum#(app(l1,l2)) -> sum#(l1) -> sum#(nil()) -> 0#(#())
     sum#(app(l1,l2)) -> sum#(l1) -> sum#(cons(x,l)) -> sum#(l)
     sum#(app(l1,l2)) -> sum#(l1) -> sum#(cons(x,l)) -> +#(x,sum(l))
     sum#(app(l1,l2)) -> sum#(l1) -> sum#(app(l1,l2)) -> sum#(l2)
     sum#(app(l1,l2)) -> sum#(l1) -> sum#(app(l1,l2)) -> sum#(l1)
     sum#(app(l1,l2)) -> sum#(l1) ->
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(0(x),0(y)) -> +#(x,y)
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(0(x),0(y)) -> 0#(+(x,y))
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(0(x),1(y)) -> +#(x,y)
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(1(x),0(y)) -> +#(x,y)
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(1(x),1(y)) -> +#(x,y)
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(1(x),1(y)) -> +#(+(x,y),1(#()))
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(+(x,y),z) -> +#(y,z)
     sum#(app(l1,l2)) -> +#(sum(l1),sum(l2)) ->
     +#(+(x,y),z) -> +#(x,+(y,z))
     app#(cons(x,l1),l2) -> app#(l1,l2) ->
     app#(cons(x,l1),l2) -> app#(l1,l2)
     *#(*(x,y),z) -> *#(y,z) -> *#(0(x),y) -> *#(x,y)
     *#(*(x,y),z) -> *#(y,z) -> *#(0(x),y) -> 0#(*(x,y))
     *#(*(x,y),z) -> *#(y,z) -> *#(1(x),y) -> *#(x,y)
     *#(*(x,y),z) -> *#(y,z) -> *#(1(x),y) -> 0#(*(x,y))
     *#(*(x,y),z) -> *#(y,z) -> *#(1(x),y) -> +#(0(*(x,y)),y)
     *#(*(x,y),z) -> *#(y,z) -> *#(*(x,y),z) -> *#(y,z)
     *#(*(x,y),z) -> *#(y,z) -> *#(*(x,y),z) -> *#(x,*(y,z))
     *#(*(x,y),z) -> *#(y,z) -> *#(x,+(y,z)) -> *#(x,z)
     *#(*(x,y),z) -> *#(y,z) -> *#(x,+(y,z)) -> *#(x,y)
     *#(*(x,y),z) -> *#(y,z) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(0(x),y) -> *#(x,y)
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(0(x),y) -> 0#(*(x,y))
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(1(x),y) -> *#(x,y)
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(1(x),y) -> 0#(*(x,y))
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(1(x),y) -> +#(0(*(x,y)),y)
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(y,z)
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z))
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(x,+(y,z)) -> *#(x,z)
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(x,+(y,z)) -> *#(x,y)
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     *#(1(x),y) -> *#(x,y) -> *#(0(x),y) -> *#(x,y)
     *#(1(x),y) -> *#(x,y) -> *#(0(x),y) -> 0#(*(x,y))
     *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> *#(x,y)
     *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> 0#(*(x,y))
     *#(1(x),y) -> *#(x,y) -> *#(1(x),y) -> +#(0(*(x,y)),y)
     *#(1(x),y) -> *#(x,y) -> *#(*(x,y),z) -> *#(y,z)
     *#(1(x),y) -> *#(x,y) -> *#(*(x,y),z) -> *#(x,*(y,z))
     *#(1(x),y) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,z)
     *#(1(x),y) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,y)
     *#(1(x),y) -> *#(x,y) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(0(x),0(y)) -> +#(x,y)
     *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(0(x),0(y)) -> 0#(+(x,y))
     *#(1(x),y) -> +#(0(*(x,y)),y) -> +#(0(x),1(y)) -> +#(x,y)
     *#(0(x),y) -> *#(x,y) -> *#(0(x),y) -> *#(x,y)
     *#(0(x),y) -> *#(x,y) -> *#(0(x),y) -> 0#(*(x,y))
     *#(0(x),y) -> *#(x,y) -> *#(1(x),y) -> *#(x,y)
     *#(0(x),y) -> *#(x,y) -> *#(1(x),y) -> 0#(*(x,y))
     *#(0(x),y) -> *#(x,y) -> *#(1(x),y) -> +#(0(*(x,y)),y)
     *#(0(x),y) -> *#(x,y) -> *#(*(x,y),z) -> *#(y,z)
     *#(0(x),y) -> *#(x,y) -> *#(*(x,y),z) -> *#(x,*(y,z))
     *#(0(x),y) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,z)
     *#(0(x),y) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,y)
     *#(0(x),y) -> *#(x,y) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     *#(x,+(y,z)) -> *#(x,z) -> *#(0(x),y) -> *#(x,y)
     *#(x,+(y,z)) -> *#(x,z) -> *#(0(x),y) -> 0#(*(x,y))
     *#(x,+(y,z)) -> *#(x,z) -> *#(1(x),y) -> *#(x,y)
     *#(x,+(y,z)) -> *#(x,z) -> *#(1(x),y) -> 0#(*(x,y))
     *#(x,+(y,z)) -> *#(x,z) -> *#(1(x),y) -> +#(0(*(x,y)),y)
     *#(x,+(y,z)) -> *#(x,z) -> *#(*(x,y),z) -> *#(y,z)
     *#(x,+(y,z)) -> *#(x,z) -> *#(*(x,y),z) -> *#(x,*(y,z))
     *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,z)
     *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,y)
     *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     *#(x,+(y,z)) -> *#(x,y) -> *#(0(x),y) -> *#(x,y)
     *#(x,+(y,z)) -> *#(x,y) -> *#(0(x),y) -> 0#(*(x,y))
     *#(x,+(y,z)) -> *#(x,y) -> *#(1(x),y) -> *#(x,y)
     *#(x,+(y,z)) -> *#(x,y) -> *#(1(x),y) -> 0#(*(x,y))
     *#(x,+(y,z)) -> *#(x,y) -> *#(1(x),y) -> +#(0(*(x,y)),y)
     *#(x,+(y,z)) -> *#(x,y) -> *#(*(x,y),z) -> *#(y,z)
     *#(x,+(y,z)) -> *#(x,y) -> *#(*(x,y),z) -> *#(x,*(y,z))
     *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,z)
     *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,y)
     *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(0(x),0(y)) -> +#(x,y)
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
     +#(0(x),0(y)) -> 0#(+(x,y))
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(0(x),1(y)) -> +#(x,y)
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(1(x),0(y)) -> +#(x,y)
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(1(x),1(y)) -> +#(x,y)
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
     +#(1(x),1(y)) -> +#(+(x,y),1(#()))
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
     +#(1(x),1(y)) -> 0#(+(+(x,y),1(#())))
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(+(x,y),z) -> +#(y,z)
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(+(x,y),z) -> +#(x,+(y,z))
     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)
     eq#(1(x),1(y)) -> eq#(x,y) -> eq#(#(),0(y)) -> eq#(#(),y)
     eq#(1(x),1(y)) -> eq#(x,y) -> eq#(0(x),#()) -> eq#(x,#())
     eq#(1(x),1(y)) -> eq#(x,y) -> eq#(1(x),1(y)) -> eq#(x,y)
     eq#(1(x),1(y)) -> eq#(x,y) -> eq#(0(x),0(y)) -> eq#(x,y)
     eq#(0(x),0(y)) -> eq#(x,y) -> eq#(#(),0(y)) -> eq#(#(),y)
     eq#(0(x),0(y)) -> eq#(x,y) -> eq#(0(x),#()) -> eq#(x,#())
     eq#(0(x),0(y)) -> eq#(x,y) -> eq#(1(x),1(y)) -> eq#(x,y)
     eq#(0(x),0(y)) -> eq#(x,y) -> eq#(0(x),0(y)) -> eq#(x,y)
     eq#(0(x),#()) -> eq#(x,#()) -> eq#(0(x),#()) -> eq#(x,#())
     eq#(#(),0(y)) -> eq#(#(),y) -> eq#(#(),0(y)) -> eq#(#(),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) -> -#(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))
    Restore Modifier:
     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))
      eq#(#(),0(y)) -> eq#(#(),y)
      eq#(0(x),#()) -> eq#(x,#())
      eq#(1(x),1(y)) -> eq#(x,y)
      eq#(0(x),0(y)) -> eq#(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(#())),#())
      *#(0(x),y) -> *#(x,y)
      *#(0(x),y) -> 0#(*(x,y))
      *#(1(x),y) -> *#(x,y)
      *#(1(x),y) -> 0#(*(x,y))
      *#(1(x),y) -> +#(0(*(x,y)),y)
      *#(*(x,y),z) -> *#(y,z)
      *#(*(x,y),z) -> *#(x,*(y,z))
      *#(x,+(y,z)) -> *#(x,z)
      *#(x,+(y,z)) -> *#(x,y)
      *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
      app#(cons(x,l1),l2) -> app#(l1,l2)
      sum#(nil()) -> 0#(#())
      sum#(cons(x,l)) -> sum#(l)
      sum#(cons(x,l)) -> +#(x,sum(l))
      sum#(app(l1,l2)) -> sum#(l2)
      sum#(app(l1,l2)) -> sum#(l1)
      sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
      prod#(cons(x,l)) -> prod#(l)
      prod#(cons(x,l)) -> *#(x,prod(l))
      prod#(app(l1,l2)) -> prod#(l2)
      prod#(app(l1,l2)) -> prod#(l1)
      prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
      mem#(x,cons(y,l)) -> mem#(x,l)
      mem#(x,cons(y,l)) -> eq#(x,y)
      mem#(x,cons(y,l)) -> if#(eq(x,y),true(),mem(x,l))
      inter#(app(l1,l2),l3) -> inter#(l2,l3)
      inter#(app(l1,l2),l3) -> inter#(l1,l3)
      inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
      inter#(l1,app(l2,l3)) -> inter#(l1,l3)
      inter#(l1,app(l2,l3)) -> inter#(l1,l2)
      inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
      inter#(cons(x,l1),l2) -> mem#(x,l2)
      inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
      inter#(l1,cons(x,l2)) -> mem#(x,l1)
      inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
      ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
      ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
     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
      eq(#(),#()) -> true()
      eq(#(),1(y)) -> false()
      eq(1(x),#()) -> false()
      eq(#(),0(y)) -> eq(#(),y)
      eq(0(x),#()) -> eq(x,#())
      eq(1(x),1(y)) -> eq(x,y)
      eq(0(x),1(y)) -> false()
      eq(1(x),0(y)) -> false()
      eq(0(x),0(y)) -> eq(x,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(#())),#())
      *(#(),x) -> #()
      *(0(x),y) -> 0(*(x,y))
      *(1(x),y) -> +(0(*(x,y)),y)
      *(*(x,y),z) -> *(x,*(y,z))
      *(x,+(y,z)) -> +(*(x,y),*(x,z))
      app(nil(),l) -> l
      app(cons(x,l1),l2) -> cons(x,app(l1,l2))
      sum(nil()) -> 0(#())
      sum(cons(x,l)) -> +(x,sum(l))
      sum(app(l1,l2)) -> +(sum(l1),sum(l2))
      prod(nil()) -> 1(#())
      prod(cons(x,l)) -> *(x,prod(l))
      prod(app(l1,l2)) -> *(prod(l1),prod(l2))
      mem(x,nil()) -> false()
      mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
      inter(x,nil()) -> nil()
      inter(nil(),x) -> nil()
      inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
      inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
      inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
      inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
      ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
      ifinter(false(),x,l1,l2) -> inter(l1,l2)
     SCC Processor:
      #sccs: 14
      #rules: 45
      #arcs: 387/5041
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       sum#(cons(x,l)) -> sum#(l)
       sum#(app(l1,l2)) -> sum#(l1)
       sum#(app(l1,l2)) -> sum#(l2)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       prod#(cons(x,l)) -> prod#(l)
       prod#(app(l1,l2)) -> prod#(l1)
       prod#(app(l1,l2)) -> prod#(l2)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       *#(x,+(y,z)) -> *#(x,y)
       *#(x,+(y,z)) -> *#(x,z)
       *#(*(x,y),z) -> *#(x,*(y,z))
       *#(*(x,y),z) -> *#(y,z)
       *#(1(x),y) -> *#(x,y)
       *#(0(x),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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
       inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
       ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
       inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
       inter#(l1,app(l2,l3)) -> inter#(l1,l2)
       inter#(l1,app(l2,l3)) -> inter#(l1,l3)
       inter#(app(l1,l2),l3) -> inter#(l1,l3)
       inter#(app(l1,l2),l3) -> inter#(l2,l3)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       app#(cons(x,l1),l2) -> app#(l1,l2)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       mem#(x,cons(y,l)) -> mem#(x,l)
      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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       eq#(0(x),0(y)) -> eq#(x,y)
       eq#(1(x),1(y)) -> eq#(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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       eq#(#(),0(y)) -> eq#(#(),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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open
      
      DPs:
       eq#(0(x),#()) -> eq#(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
       eq(#(),#()) -> true()
       eq(#(),1(y)) -> false()
       eq(1(x),#()) -> false()
       eq(#(),0(y)) -> eq(#(),y)
       eq(0(x),#()) -> eq(x,#())
       eq(1(x),1(y)) -> eq(x,y)
       eq(0(x),1(y)) -> false()
       eq(1(x),0(y)) -> false()
       eq(0(x),0(y)) -> eq(x,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(#())),#())
       *(#(),x) -> #()
       *(0(x),y) -> 0(*(x,y))
       *(1(x),y) -> +(0(*(x,y)),y)
       *(*(x,y),z) -> *(x,*(y,z))
       *(x,+(y,z)) -> +(*(x,y),*(x,z))
       app(nil(),l) -> l
       app(cons(x,l1),l2) -> cons(x,app(l1,l2))
       sum(nil()) -> 0(#())
       sum(cons(x,l)) -> +(x,sum(l))
       sum(app(l1,l2)) -> +(sum(l1),sum(l2))
       prod(nil()) -> 1(#())
       prod(cons(x,l)) -> *(x,prod(l))
       prod(app(l1,l2)) -> *(prod(l1),prod(l2))
       mem(x,nil()) -> false()
       mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
       inter(x,nil()) -> nil()
       inter(nil(),x) -> nil()
       inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
       inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
       inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
       inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
       ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
       ifinter(false(),x,l1,l2) -> inter(l1,l2)
      Open