MAYBE

Problem:
 and(true(),y) -> y
 and(false(),y) -> false()
 eq(nil(),nil()) -> true()
 eq(cons(t,l),nil()) -> false()
 eq(nil(),cons(t,l)) -> false()
 eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
 eq(var(l),var(l')) -> eq(l,l')
 eq(var(l),apply(t,s)) -> false()
 eq(var(l),lambda(x,t)) -> false()
 eq(apply(t,s),var(l)) -> false()
 eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
 eq(apply(t,s),lambda(x,t)) -> false()
 eq(lambda(x,t),var(l)) -> false()
 eq(lambda(x,t),apply(t,s)) -> false()
 eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
 if(true(),var(k),var(l')) -> var(k)
 if(false(),var(k),var(l')) -> var(l')
 ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
 ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
 ren(x,y,lambda(z,t)) ->
 lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var
                                                                   (cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                 t)))

Proof:
 DP Processor:
  DPs:
   eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
   eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
   eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
   eq#(var(l),var(l')) -> eq#(l,l')
   eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
   eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
   eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
   eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
   eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
   eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
   ren#(var(l),var(k),var(l')) -> eq#(l,l')
   ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
   ren#(x,y,apply(t,s)) -> ren#(x,y,s)
   ren#(x,y,apply(t,s)) -> ren#(x,y,t)
   ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
   ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
  TRS:
   and(true(),y) -> y
   and(false(),y) -> false()
   eq(nil(),nil()) -> true()
   eq(cons(t,l),nil()) -> false()
   eq(nil(),cons(t,l)) -> false()
   eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
   eq(var(l),var(l')) -> eq(l,l')
   eq(var(l),apply(t,s)) -> false()
   eq(var(l),lambda(x,t)) -> false()
   eq(apply(t,s),var(l)) -> false()
   eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
   eq(apply(t,s),lambda(x,t)) -> false()
   eq(lambda(x,t),var(l)) -> false()
   eq(lambda(x,t),apply(t,s)) -> false()
   eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
   if(true(),var(k),var(l')) -> var(k)
   if(false(),var(k),var(l')) -> var(l')
   ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
   ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
   ren(x,y,lambda(z,t)) ->
   lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,
                                                                   var
                                                                   (cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                   t)))
  EDG Processor:
   DPs:
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    ren#(var(l),var(k),var(l')) -> eq#(l,l')
    ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
    ren#(x,y,apply(t,s)) -> ren#(x,y,s)
    ren#(x,y,apply(t,s)) -> ren#(x,y,t)
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
   TRS:
    and(true(),y) -> y
    and(false(),y) -> false()
    eq(nil(),nil()) -> true()
    eq(cons(t,l),nil()) -> false()
    eq(nil(),cons(t,l)) -> false()
    eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
    eq(var(l),var(l')) -> eq(l,l')
    eq(var(l),apply(t,s)) -> false()
    eq(var(l),lambda(x,t)) -> false()
    eq(apply(t,s),var(l)) -> false()
    eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
    eq(apply(t,s),lambda(x,t)) -> false()
    eq(lambda(x,t),var(l)) -> false()
    eq(lambda(x,t),apply(t,s)) -> false()
    eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
    if(true(),var(k),var(l')) -> var(k)
    if(false(),var(k),var(l')) -> var(l')
    ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
    ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
    ren(x,y,lambda(z,t)) ->
    lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,
                                                                    var
                                                                    (
                                                                    cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                    t)))
   graph:
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    ren#(var(l),var(k),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t) ->
    ren#(var(l),var(k),var(l')) -> eq#(l,l')
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t) ->
    ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t) ->
    ren#(x,y,apply(t,s)) -> ren#(x,y,s)
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t) ->
    ren#(x,y,apply(t,s)) -> ren#(x,y,t)
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t) ->
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t) ->
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)) ->
    ren#(var(l),var(k),var(l')) -> eq#(l,l')
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)) ->
    ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)) ->
    ren#(x,y,apply(t,s)) -> ren#(x,y,s)
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)) ->
    ren#(x,y,apply(t,s)) -> ren#(x,y,t)
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)) ->
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)) ->
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
    ren#(x,y,apply(t,s)) -> ren#(x,y,s) ->
    ren#(var(l),var(k),var(l')) -> eq#(l,l')
    ren#(x,y,apply(t,s)) -> ren#(x,y,s) ->
    ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
    ren#(x,y,apply(t,s)) -> ren#(x,y,s) ->
    ren#(x,y,apply(t,s)) -> ren#(x,y,s)
    ren#(x,y,apply(t,s)) -> ren#(x,y,s) ->
    ren#(x,y,apply(t,s)) -> ren#(x,y,t)
    ren#(x,y,apply(t,s)) -> ren#(x,y,s) ->
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
    ren#(x,y,apply(t,s)) -> ren#(x,y,s) ->
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
    ren#(x,y,apply(t,s)) -> ren#(x,y,t) ->
    ren#(var(l),var(k),var(l')) -> eq#(l,l')
    ren#(x,y,apply(t,s)) -> ren#(x,y,t) ->
    ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
    ren#(x,y,apply(t,s)) -> ren#(x,y,t) ->
    ren#(x,y,apply(t,s)) -> ren#(x,y,s)
    ren#(x,y,apply(t,s)) -> ren#(x,y,t) ->
    ren#(x,y,apply(t,s)) -> ren#(x,y,t)
    ren#(x,y,apply(t,s)) -> ren#(x,y,t) ->
    ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
    ren#(x,y,apply(t,s)) -> ren#(x,y,t) ->
    ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(var(l),var(l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(var(l),var(l')) -> eq#(l,l')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
    eq#(cons(t,l),cons(t',l')) -> eq#(t,t') ->
    eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
   Restore Modifier:
    DPs:
     eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
     eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
     eq#(cons(t,l),cons(t',l')) -> and#(eq(t,t'),eq(l,l'))
     eq#(var(l),var(l')) -> eq#(l,l')
     eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
     eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
     eq#(apply(t,s),apply(t',s')) -> and#(eq(t,t'),eq(s,s'))
     eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
     eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
     eq#(lambda(x,t),lambda(x',t')) -> and#(eq(x,x'),eq(t,t'))
     ren#(var(l),var(k),var(l')) -> eq#(l,l')
     ren#(var(l),var(k),var(l')) -> if#(eq(l,l'),var(k),var(l'))
     ren#(x,y,apply(t,s)) -> ren#(x,y,s)
     ren#(x,y,apply(t,s)) -> ren#(x,y,t)
     ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
     ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
    TRS:
     and(true(),y) -> y
     and(false(),y) -> false()
     eq(nil(),nil()) -> true()
     eq(cons(t,l),nil()) -> false()
     eq(nil(),cons(t,l)) -> false()
     eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
     eq(var(l),var(l')) -> eq(l,l')
     eq(var(l),apply(t,s)) -> false()
     eq(var(l),lambda(x,t)) -> false()
     eq(apply(t,s),var(l)) -> false()
     eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
     eq(apply(t,s),lambda(x,t)) -> false()
     eq(lambda(x,t),var(l)) -> false()
     eq(lambda(x,t),apply(t,s)) -> false()
     eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
     if(true(),var(k),var(l')) -> var(k)
     if(false(),var(k),var(l')) -> var(l')
     ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
     ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
     ren(x,y,lambda(z,t)) ->
     lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(
                                                                    z,
                                                                    var
                                                                    (
                                                                    cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                    t)))
    SCC Processor:
     #sccs: 2
     #rules: 11
     #arcs: 104/256
     DPs:
      ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
      ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
      ren#(x,y,apply(t,s)) -> ren#(x,y,t)
      ren#(x,y,apply(t,s)) -> ren#(x,y,s)
     TRS:
      and(true(),y) -> y
      and(false(),y) -> false()
      eq(nil(),nil()) -> true()
      eq(cons(t,l),nil()) -> false()
      eq(nil(),cons(t,l)) -> false()
      eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
      eq(var(l),var(l')) -> eq(l,l')
      eq(var(l),apply(t,s)) -> false()
      eq(var(l),lambda(x,t)) -> false()
      eq(apply(t,s),var(l)) -> false()
      eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
      eq(apply(t,s),lambda(x,t)) -> false()
      eq(lambda(x,t),var(l)) -> false()
      eq(lambda(x,t),apply(t,s)) -> false()
      eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
      if(true(),var(k),var(l')) -> var(k)
      if(false(),var(k),var(l')) -> var(l')
      ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
      ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
      ren(x,y,lambda(z,t)) ->
      lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren
                                                                  (z,
                                                                   var
                                                                   (cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                   t)))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [ren#](x0, x1, x2) = x2 + 1,
       
       [ren](x0, x1, x2) = x2,
       
       [if](x0, x1, x2) = 0,
       
       [lambda](x0, x1) = x0 + x1,
       
       [apply](x0, x1) = x0 + x1 + 1,
       
       [var](x0) = 0,
       
       [cons](x0, x1) = x1,
       
       [eq](x0, x1) = 0,
       
       [nil] = 1,
       
       [false] = 0,
       
       [and](x0, x1) = x1,
       
       [true] = 0
      orientation:
       ren#(x,y,lambda(z,t)) = t + z + 1 >= t + 1 = ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
       
       ren#(x,y,lambda(z,t)) = t + z + 1 >= t + 1 = ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
       
       ren#(x,y,apply(t,s)) = s + t + 2 >= t + 1 = ren#(x,y,t)
       
       ren#(x,y,apply(t,s)) = s + t + 2 >= s + 1 = ren#(x,y,s)
       
       and(true(),y) = y >= y = y
       
       and(false(),y) = y >= 0 = false()
       
       eq(nil(),nil()) = 0 >= 0 = true()
       
       eq(cons(t,l),nil()) = 0 >= 0 = false()
       
       eq(nil(),cons(t,l)) = 0 >= 0 = false()
       
       eq(cons(t,l),cons(t',l')) = 0 >= 0 = and(eq(t,t'),eq(l,l'))
       
       eq(var(l),var(l')) = 0 >= 0 = eq(l,l')
       
       eq(var(l),apply(t,s)) = 0 >= 0 = false()
       
       eq(var(l),lambda(x,t)) = 0 >= 0 = false()
       
       eq(apply(t,s),var(l)) = 0 >= 0 = false()
       
       eq(apply(t,s),apply(t',s')) = 0 >= 0 = and(eq(t,t'),eq(s,s'))
       
       eq(apply(t,s),lambda(x,t)) = 0 >= 0 = false()
       
       eq(lambda(x,t),var(l)) = 0 >= 0 = false()
       
       eq(lambda(x,t),apply(t,s)) = 0 >= 0 = false()
       
       eq(lambda(x,t),lambda(x',t')) = 0 >= 0 = and(eq(x,x'),eq(t,t'))
       
       if(true(),var(k),var(l')) = 0 >= 0 = var(k)
       
       if(false(),var(k),var(l')) = 0 >= 0 = var(l')
       
       ren(var(l),var(k),var(l')) = 0 >= 0 = if(eq(l,l'),var(k),var(l'))
       
       ren(x,y,apply(t,s)) = s + t + 1 >= s + t + 1 = apply(ren(x,y,t),ren(x,y,s))
       
       ren(x,y,lambda(z,t)) = t + z >= t = lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var
                                                                  (cons
                                                                   (x,
                                                                    cons
                                                                    (
                                                                    y,
                                                                    cons
                                                                    (
                                                                    lambda
                                                                    (
                                                                    z,t),
                                                                    nil
                                                                    ())))),
                                                                t)))
      problem:
       DPs:
        ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
        ren#(x,y,lambda(z,t)) -> ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
       TRS:
        and(true(),y) -> y
        and(false(),y) -> false()
        eq(nil(),nil()) -> true()
        eq(cons(t,l),nil()) -> false()
        eq(nil(),cons(t,l)) -> false()
        eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
        eq(var(l),var(l')) -> eq(l,l')
        eq(var(l),apply(t,s)) -> false()
        eq(var(l),lambda(x,t)) -> false()
        eq(apply(t,s),var(l)) -> false()
        eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
        eq(apply(t,s),lambda(x,t)) -> false()
        eq(lambda(x,t),var(l)) -> false()
        eq(lambda(x,t),apply(t,s)) -> false()
        eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
        if(true(),var(k),var(l')) -> var(k)
        if(false(),var(k),var(l')) -> var(l')
        ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
        ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
        ren(x,y,lambda(z,t)) ->
        lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren
                                                                    (
                                                                    z,
                                                                    var
                                                                    (
                                                                    cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                    t)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [ren#](x0, x1, x2) = x1 + x2,
        
        [ren](x0, x1, x2) = x2,
        
        [if](x0, x1, x2) = 1,
        
        [lambda](x0, x1) = x1 + 1,
        
        [apply](x0, x1) = 0,
        
        [var](x0) = 1,
        
        [cons](x0, x1) = x0 + 1,
        
        [eq](x0, x1) = 0,
        
        [nil] = 0,
        
        [false] = 0,
        
        [and](x0, x1) = x1,
        
        [true] = 0
       orientation:
        ren#(x,y,lambda(z,t)) = t + y + 1 >= t + 1 = ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
        
        ren#(x,y,lambda(z,t)) = t + y + 1 >= t + y = ren#(x,y,ren(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t))
        
        and(true(),y) = y >= y = y
        
        and(false(),y) = y >= 0 = false()
        
        eq(nil(),nil()) = 0 >= 0 = true()
        
        eq(cons(t,l),nil()) = 0 >= 0 = false()
        
        eq(nil(),cons(t,l)) = 0 >= 0 = false()
        
        eq(cons(t,l),cons(t',l')) = 0 >= 0 = and(eq(t,t'),eq(l,l'))
        
        eq(var(l),var(l')) = 0 >= 0 = eq(l,l')
        
        eq(var(l),apply(t,s)) = 0 >= 0 = false()
        
        eq(var(l),lambda(x,t)) = 0 >= 0 = false()
        
        eq(apply(t,s),var(l)) = 0 >= 0 = false()
        
        eq(apply(t,s),apply(t',s')) = 0 >= 0 = and(eq(t,t'),eq(s,s'))
        
        eq(apply(t,s),lambda(x,t)) = 0 >= 0 = false()
        
        eq(lambda(x,t),var(l)) = 0 >= 0 = false()
        
        eq(lambda(x,t),apply(t,s)) = 0 >= 0 = false()
        
        eq(lambda(x,t),lambda(x',t')) = 0 >= 0 = and(eq(x,x'),eq(t,t'))
        
        if(true(),var(k),var(l')) = 1 >= 1 = var(k)
        
        if(false(),var(k),var(l')) = 1 >= 1 = var(l')
        
        ren(var(l),var(k),var(l')) = 1 >= 1 = if(eq(l,l'),var(k),var(l'))
        
        ren(x,y,apply(t,s)) = 0 >= 0 = apply(ren(x,y,t),ren(x,y,s))
        
        ren(x,y,lambda(z,t)) = t + 1 >= t + 1 = lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var
                                                                  (cons
                                                                   (x,
                                                                    cons
                                                                    (
                                                                    y,
                                                                    cons
                                                                    (
                                                                    lambda
                                                                    (
                                                                    z,t),
                                                                    nil
                                                                    ())))),
                                                                t)))
       problem:
        DPs:
         ren#(x,y,lambda(z,t)) -> ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
        TRS:
         and(true(),y) -> y
         and(false(),y) -> false()
         eq(nil(),nil()) -> true()
         eq(cons(t,l),nil()) -> false()
         eq(nil(),cons(t,l)) -> false()
         eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
         eq(var(l),var(l')) -> eq(l,l')
         eq(var(l),apply(t,s)) -> false()
         eq(var(l),lambda(x,t)) -> false()
         eq(apply(t,s),var(l)) -> false()
         eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
         eq(apply(t,s),lambda(x,t)) -> false()
         eq(lambda(x,t),var(l)) -> false()
         eq(lambda(x,t),apply(t,s)) -> false()
         eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
         if(true(),var(k),var(l')) -> var(k)
         if(false(),var(k),var(l')) -> var(l')
         ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
         ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
         ren(x,y,lambda(z,t)) ->
         lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,
                                                                 ren(
                                                                    z,
                                                                    var
                                                                    (
                                                                    cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                    t)))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [ren#](x0, x1, x2) = x2,
         
         [ren](x0, x1, x2) = x2,
         
         [if](x0, x1, x2) = 0,
         
         [lambda](x0, x1) = x1 + 1,
         
         [apply](x0, x1) = 0,
         
         [var](x0) = 0,
         
         [cons](x0, x1) = x1 + 1,
         
         [eq](x0, x1) = 0,
         
         [nil] = 0,
         
         [false] = 0,
         
         [and](x0, x1) = x1,
         
         [true] = 0
        orientation:
         ren#(x,y,lambda(z,t)) = t + 1 >= t = ren#(z,var(cons(x,cons(y,cons(lambda(z,t),nil())))),t)
         
         and(true(),y) = y >= y = y
         
         and(false(),y) = y >= 0 = false()
         
         eq(nil(),nil()) = 0 >= 0 = true()
         
         eq(cons(t,l),nil()) = 0 >= 0 = false()
         
         eq(nil(),cons(t,l)) = 0 >= 0 = false()
         
         eq(cons(t,l),cons(t',l')) = 0 >= 0 = and(eq(t,t'),eq(l,l'))
         
         eq(var(l),var(l')) = 0 >= 0 = eq(l,l')
         
         eq(var(l),apply(t,s)) = 0 >= 0 = false()
         
         eq(var(l),lambda(x,t)) = 0 >= 0 = false()
         
         eq(apply(t,s),var(l)) = 0 >= 0 = false()
         
         eq(apply(t,s),apply(t',s')) = 0 >= 0 = and(eq(t,t'),eq(s,s'))
         
         eq(apply(t,s),lambda(x,t)) = 0 >= 0 = false()
         
         eq(lambda(x,t),var(l)) = 0 >= 0 = false()
         
         eq(lambda(x,t),apply(t,s)) = 0 >= 0 = false()
         
         eq(lambda(x,t),lambda(x',t')) = 0 >= 0 = and(eq(x,x'),eq(t,t'))
         
         if(true(),var(k),var(l')) = 0 >= 0 = var(k)
         
         if(false(),var(k),var(l')) = 0 >= 0 = var(l')
         
         ren(var(l),var(k),var(l')) = 0 >= 0 = if(eq(l,l'),var(k),var(l'))
         
         ren(x,y,apply(t,s)) = 0 >= 0 = apply(ren(x,y,t),ren(x,y,s))
         
         ren(x,y,lambda(z,t)) = t + 1 >= t + 1 = lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren(z,var
                                                                  (cons
                                                                   (x,
                                                                    cons
                                                                    (
                                                                    y,
                                                                    cons
                                                                    (
                                                                    lambda
                                                                    (
                                                                    z,t),
                                                                    nil
                                                                    ())))),
                                                                t)))
        problem:
         DPs:
          
         TRS:
          and(true(),y) -> y
          and(false(),y) -> false()
          eq(nil(),nil()) -> true()
          eq(cons(t,l),nil()) -> false()
          eq(nil(),cons(t,l)) -> false()
          eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
          eq(var(l),var(l')) -> eq(l,l')
          eq(var(l),apply(t,s)) -> false()
          eq(var(l),lambda(x,t)) -> false()
          eq(apply(t,s),var(l)) -> false()
          eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
          eq(apply(t,s),lambda(x,t)) -> false()
          eq(lambda(x,t),var(l)) -> false()
          eq(lambda(x,t),apply(t,s)) -> false()
          eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
          if(true(),var(k),var(l')) -> var(k)
          if(false(),var(k),var(l')) -> var(l')
          ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
          ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
          ren(x,y,lambda(z,t)) ->
          lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,
                                                                  ren
                                                                  (z,
                                                                   var
                                                                   (cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                   t)))
        Qed
     
     DPs:
      eq#(lambda(x,t),lambda(x',t')) -> eq#(x,x')
      eq#(lambda(x,t),lambda(x',t')) -> eq#(t,t')
      eq#(apply(t,s),apply(t',s')) -> eq#(t,t')
      eq#(apply(t,s),apply(t',s')) -> eq#(s,s')
      eq#(var(l),var(l')) -> eq#(l,l')
      eq#(cons(t,l),cons(t',l')) -> eq#(t,t')
      eq#(cons(t,l),cons(t',l')) -> eq#(l,l')
     TRS:
      and(true(),y) -> y
      and(false(),y) -> false()
      eq(nil(),nil()) -> true()
      eq(cons(t,l),nil()) -> false()
      eq(nil(),cons(t,l)) -> false()
      eq(cons(t,l),cons(t',l')) -> and(eq(t,t'),eq(l,l'))
      eq(var(l),var(l')) -> eq(l,l')
      eq(var(l),apply(t,s)) -> false()
      eq(var(l),lambda(x,t)) -> false()
      eq(apply(t,s),var(l)) -> false()
      eq(apply(t,s),apply(t',s')) -> and(eq(t,t'),eq(s,s'))
      eq(apply(t,s),lambda(x,t)) -> false()
      eq(lambda(x,t),var(l)) -> false()
      eq(lambda(x,t),apply(t,s)) -> false()
      eq(lambda(x,t),lambda(x',t')) -> and(eq(x,x'),eq(t,t'))
      if(true(),var(k),var(l')) -> var(k)
      if(false(),var(k),var(l')) -> var(l')
      ren(var(l),var(k),var(l')) -> if(eq(l,l'),var(k),var(l'))
      ren(x,y,apply(t,s)) -> apply(ren(x,y,t),ren(x,y,s))
      ren(x,y,lambda(z,t)) ->
      lambda(var(cons(x,cons(y,cons(lambda(z,t),nil())))),ren(x,y,ren
                                                                  (z,
                                                                   var
                                                                   (cons
                                                                    (
                                                                    x,
                                                                    cons
                                                                    (y,cons(lambda(z,t),nil())))),
                                                                   t)))
     Open