YES

Problem:
 and(false(),false()) -> false()
 and(true(),false()) -> false()
 and(false(),true()) -> false()
 and(true(),true()) -> true()
 eq(nil(),nil()) -> true()
 eq(cons(T,L),nil()) -> false()
 eq(nil(),cons(T,L)) -> false()
 eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
 eq(var(L),var(Lp)) -> eq(L,Lp)
 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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
 eq(apply(T,S),lambda(X,Tp)) -> false()
 eq(lambda(X,T),var(L)) -> false()
 eq(lambda(X,T),apply(Tp,Sp)) -> false()
 eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
 if(true(),var(K),var(L)) -> var(K)
 if(false(),var(K),var(L)) -> var(L)
 ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
 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(Tp,Lp)) -> eq#(L,Lp)
   eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
   eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
   eq#(var(L),var(Lp)) -> eq#(L,Lp)
   eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
   eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
   eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
   eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
   eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
   eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
   ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp)
   ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp))
   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(false(),false()) -> false()
   and(true(),false()) -> false()
   and(false(),true()) -> false()
   and(true(),true()) -> true()
   eq(nil(),nil()) -> true()
   eq(cons(T,L),nil()) -> false()
   eq(nil(),cons(T,L)) -> false()
   eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
   eq(var(L),var(Lp)) -> eq(L,Lp)
   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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
   eq(apply(T,S),lambda(X,Tp)) -> false()
   eq(lambda(X,T),var(L)) -> false()
   eq(lambda(X,T),apply(Tp,Sp)) -> false()
   eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
   if(true(),var(K),var(L)) -> var(K)
   if(false(),var(K),var(L)) -> var(L)
   ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
   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)))
  TDG Processor:
   DPs:
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp)
    ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp))
    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(false(),false()) -> false()
    and(true(),false()) -> false()
    and(false(),true()) -> false()
    and(true(),true()) -> true()
    eq(nil(),nil()) -> true()
    eq(cons(T,L),nil()) -> false()
    eq(nil(),cons(T,L)) -> false()
    eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
    eq(var(L),var(Lp)) -> eq(L,Lp)
    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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
    eq(apply(T,S),lambda(X,Tp)) -> false()
    eq(lambda(X,T),var(L)) -> false()
    eq(lambda(X,T),apply(Tp,Sp)) -> false()
    eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
    if(true(),var(K),var(L)) -> var(K)
    if(false(),var(K),var(L)) -> var(L)
    ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
    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(Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
    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#(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,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,S)
    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(Lp)) -> if#(eq(L,Lp),var(K),var(Lp))
    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(Lp)) -> eq#(L,Lp)
    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,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,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,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#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp))
    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(Lp)) -> eq#(L,Lp)
    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,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,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,S)
    ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ->
    ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp))
    ren#(X,Y,apply(T,S)) -> ren#(X,Y,T) ->
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp)
    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,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,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,S)
    ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ->
    ren#(var(L),var(K),var(Lp)) -> if#(eq(L,Lp),var(K),var(Lp))
    ren#(X,Y,apply(T,S)) -> ren#(X,Y,S) ->
    ren#(var(L),var(K),var(Lp)) -> eq#(L,Lp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    eq#(var(L),var(Lp)) -> eq#(L,Lp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> and#(eq(T,Tp),eq(X,Xp))
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> and#(eq(T,Tp),eq(S,Sp))
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(var(L),var(Lp)) -> eq#(L,Lp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> and#(eq(T,Tp),eq(L,Lp))
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) ->
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
    eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp) -> eq#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
   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,apply(T,S)) -> ren#(X,Y,S)
     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))
    TRS:
     and(false(),false()) -> false()
     and(true(),false()) -> false()
     and(false(),true()) -> false()
     and(true(),true()) -> true()
     eq(nil(),nil()) -> true()
     eq(cons(T,L),nil()) -> false()
     eq(nil(),cons(T,L)) -> false()
     eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
     eq(var(L),var(Lp)) -> eq(L,Lp)
     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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
     eq(apply(T,S),lambda(X,Tp)) -> false()
     eq(lambda(X,T),var(L)) -> false()
     eq(lambda(X,T),apply(Tp,Sp)) -> false()
     eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
     if(true(),var(K),var(L)) -> var(K)
     if(false(),var(K),var(L)) -> var(L)
     ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
     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)))
    Arctic Interpretation Processor:
     dimension: 1
     usable rules:
      and(false(),false()) -> false()
      and(true(),false()) -> false()
      and(false(),true()) -> false()
      and(true(),true()) -> true()
      eq(nil(),nil()) -> true()
      eq(cons(T,L),nil()) -> false()
      eq(nil(),cons(T,L)) -> false()
      eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
      eq(var(L),var(Lp)) -> eq(L,Lp)
      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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
      eq(apply(T,S),lambda(X,Tp)) -> false()
      eq(lambda(X,T),var(L)) -> false()
      eq(lambda(X,T),apply(Tp,Sp)) -> false()
      eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
      if(true(),var(K),var(L)) -> var(K)
      if(false(),var(K),var(L)) -> var(L)
      ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
      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)))
     interpretation:
      [ren#](x0, x1, x2) = 1x1 + x2 + 0,
      
      [ren](x0, x1, x2) = x2 + 0,
      
      [if](x0, x1, x2) = x0 + x1 + 0,
      
      [lambda](x0, x1) = 1x1 + 4,
      
      [apply](x0, x1) = 4x0 + 2x1 + 4,
      
      [var](x0) = 0,
      
      [cons](x0, x1) = x0 + x1 + 2,
      
      [eq](x0, x1) = 0,
      
      [nil] = 4,
      
      [true] = 0,
      
      [and](x0, x1) = x1 + 0,
      
      [false] = 0
     orientation:
      ren#(X,Y,lambda(Z,T)) = 1T + 1Y + 4 >= T + 1 = ren#(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T)
      
      ren#(X,Y,apply(T,S)) = 2S + 4T + 1Y + 4 >= S + 1Y + 0 = ren#(X,Y,S)
      
      ren#(X,Y,apply(T,S)) = 2S + 4T + 1Y + 4 >= T + 1Y + 0 = ren#(X,Y,T)
      
      ren#(X,Y,lambda(Z,T)) = 1T + 1Y + 4 >= T + 1Y + 0 = ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T))
      
      and(false(),false()) = 0 >= 0 = false()
      
      and(true(),false()) = 0 >= 0 = false()
      
      and(false(),true()) = 0 >= 0 = false()
      
      and(true(),true()) = 0 >= 0 = true()
      
      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(Tp,Lp)) = 0 >= 0 = and(eq(T,Tp),eq(L,Lp))
      
      eq(var(L),var(Lp)) = 0 >= 0 = eq(L,Lp)
      
      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(Tp,Sp)) = 0 >= 0 = and(eq(T,Tp),eq(S,Sp))
      
      eq(apply(T,S),lambda(X,Tp)) = 0 >= 0 = false()
      
      eq(lambda(X,T),var(L)) = 0 >= 0 = false()
      
      eq(lambda(X,T),apply(Tp,Sp)) = 0 >= 0 = false()
      
      eq(lambda(X,T),lambda(Xp,Tp)) = 0 >= 0 = and(eq(T,Tp),eq(X,Xp))
      
      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(Lp)) = 0 >= 0 = if(eq(L,Lp),var(K),var(Lp))
      
      ren(X,Y,apply(T,S)) = 2S + 4T + 4 >= 2S + 4T + 4 = apply(ren(X,Y,T),ren(X,Y,S))
      
      ren(X,Y,lambda(Z,T)) = 1T + 4 >= 1T + 4 = 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,apply(T,S)) -> ren#(X,Y,S)
       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))
      TRS:
       and(false(),false()) -> false()
       and(true(),false()) -> false()
       and(false(),true()) -> false()
       and(true(),true()) -> true()
       eq(nil(),nil()) -> true()
       eq(cons(T,L),nil()) -> false()
       eq(nil(),cons(T,L)) -> false()
       eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
       eq(var(L),var(Lp)) -> eq(L,Lp)
       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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
       eq(apply(T,S),lambda(X,Tp)) -> false()
       eq(lambda(X,T),var(L)) -> false()
       eq(lambda(X,T),apply(Tp,Sp)) -> false()
       eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
       if(true(),var(K),var(L)) -> var(K)
       if(false(),var(K),var(L)) -> var(L)
       ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
       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)))
     Restore Modifier:
      DPs:
       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#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T))
      TRS:
       and(false(),false()) -> false()
       and(true(),false()) -> false()
       and(false(),true()) -> false()
       and(true(),true()) -> true()
       eq(nil(),nil()) -> true()
       eq(cons(T,L),nil()) -> false()
       eq(nil(),cons(T,L)) -> false()
       eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
       eq(var(L),var(Lp)) -> eq(L,Lp)
       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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
       eq(apply(T,S),lambda(X,Tp)) -> false()
       eq(lambda(X,T),var(L)) -> false()
       eq(lambda(X,T),apply(Tp,Sp)) -> false()
       eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
       if(true(),var(K),var(L)) -> var(K)
       if(false(),var(K),var(L)) -> var(L)
       ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
       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)))
      Arctic Interpretation Processor:
       dimension: 1
       usable rules:
        if(true(),var(K),var(L)) -> var(K)
        if(false(),var(K),var(L)) -> var(L)
        ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
        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)))
       interpretation:
        [ren#](x0, x1, x2) = x2 + 0,
        
        [ren](x0, x1, x2) = x2 + 0,
        
        [if](x0, x1, x2) = x1 + x2 + 0,
        
        [lambda](x0, x1) = 1x0 + 1x1 + 1,
        
        [apply](x0, x1) = 2x0 + x1 + 4,
        
        [var](x0) = 0,
        
        [cons](x0, x1) = 5x0 + x1 + 0,
        
        [eq](x0, x1) = 1x0 + 4,
        
        [nil] = 6,
        
        [true] = 1,
        
        [and](x0, x1) = 0,
        
        [false] = 4
       orientation:
        ren#(X,Y,apply(T,S)) = S + 2T + 4 >= S + 0 = ren#(X,Y,S)
        
        ren#(X,Y,apply(T,S)) = S + 2T + 4 >= T + 0 = ren#(X,Y,T)
        
        ren#(X,Y,lambda(Z,T)) = 1T + 1Z + 1 >= T + 0 = ren#(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil())))),T))
        
        and(false(),false()) = 0 >= 4 = false()
        
        and(true(),false()) = 0 >= 4 = false()
        
        and(false(),true()) = 0 >= 4 = false()
        
        and(true(),true()) = 0 >= 1 = true()
        
        eq(nil(),nil()) = 7 >= 1 = true()
        
        eq(cons(T,L),nil()) = 1L + 6T + 4 >= 4 = false()
        
        eq(nil(),cons(T,L)) = 7 >= 4 = false()
        
        eq(cons(T,L),cons(Tp,Lp)) = 1L + 6T + 4 >= 0 = and(eq(T,Tp),eq(L,Lp))
        
        eq(var(L),var(Lp)) = 4 >= 1L + 4 = eq(L,Lp)
        
        eq(var(L),apply(T,S)) = 4 >= 4 = false()
        
        eq(var(L),lambda(X,T)) = 4 >= 4 = false()
        
        eq(apply(T,S),var(L)) = 1S + 3T + 5 >= 4 = false()
        
        eq(apply(T,S),apply(Tp,Sp)) = 1S + 3T + 5 >= 0 = and(eq(T,Tp),eq(S,Sp))
        
        eq(apply(T,S),lambda(X,Tp)) = 1S + 3T + 5 >= 4 = false()
        
        eq(lambda(X,T),var(L)) = 2T + 2X + 4 >= 4 = false()
        
        eq(lambda(X,T),apply(Tp,Sp)) = 2T + 2X + 4 >= 4 = false()
        
        eq(lambda(X,T),lambda(Xp,Tp)) = 2T + 2X + 4 >= 0 = and(eq(T,Tp),eq(X,Xp))
        
        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(Lp)) = 0 >= 0 = if(eq(L,Lp),var(K),var(Lp))
        
        ren(X,Y,apply(T,S)) = S + 2T + 4 >= S + 2T + 4 = apply(ren(X,Y,T),ren(X,Y,S))
        
        ren(X,Y,lambda(Z,T)) = 1T + 1Z + 1 >= 1T + 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,apply(T,S)) -> ren#(X,Y,S)
         ren#(X,Y,apply(T,S)) -> ren#(X,Y,T)
        TRS:
         and(false(),false()) -> false()
         and(true(),false()) -> false()
         and(false(),true()) -> false()
         and(true(),true()) -> true()
         eq(nil(),nil()) -> true()
         eq(cons(T,L),nil()) -> false()
         eq(nil(),cons(T,L)) -> false()
         eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
         eq(var(L),var(Lp)) -> eq(L,Lp)
         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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
         eq(apply(T,S),lambda(X,Tp)) -> false()
         eq(lambda(X,T),var(L)) -> false()
         eq(lambda(X,T),apply(Tp,Sp)) -> false()
         eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
         if(true(),var(K),var(L)) -> var(K)
         if(false(),var(K),var(L)) -> var(L)
         ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
         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)))
       Restore Modifier:
        DPs:
         ren#(X,Y,apply(T,S)) -> ren#(X,Y,S)
         ren#(X,Y,apply(T,S)) -> ren#(X,Y,T)
        TRS:
         and(false(),false()) -> false()
         and(true(),false()) -> false()
         and(false(),true()) -> false()
         and(true(),true()) -> true()
         eq(nil(),nil()) -> true()
         eq(cons(T,L),nil()) -> false()
         eq(nil(),cons(T,L)) -> false()
         eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
         eq(var(L),var(Lp)) -> eq(L,Lp)
         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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
         eq(apply(T,S),lambda(X,Tp)) -> false()
         eq(lambda(X,T),var(L)) -> false()
         eq(lambda(X,T),apply(Tp,Sp)) -> false()
         eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
         if(true(),var(K),var(L)) -> var(K)
         if(false(),var(K),var(L)) -> var(L)
         ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
         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)))
        Subterm Criterion Processor:
         simple projection:
          pi(ren#) = 2
         problem:
          DPs:
           
          TRS:
           and(false(),false()) -> false()
           and(true(),false()) -> false()
           and(false(),true()) -> false()
           and(true(),true()) -> true()
           eq(nil(),nil()) -> true()
           eq(cons(T,L),nil()) -> false()
           eq(nil(),cons(T,L)) -> false()
           eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
           eq(var(L),var(Lp)) -> eq(L,Lp)
           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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
           eq(apply(T,S),lambda(X,Tp)) -> false()
           eq(lambda(X,T),var(L)) -> false()
           eq(lambda(X,T),apply(Tp,Sp)) -> false()
           eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
           if(true(),var(K),var(L)) -> var(K)
           if(false(),var(K),var(L)) -> var(L)
           ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
           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#(cons(T,L),cons(Tp,Lp)) -> eq#(L,Lp)
     eq#(cons(T,L),cons(Tp,Lp)) -> eq#(T,Tp)
     eq#(var(L),var(Lp)) -> eq#(L,Lp)
     eq#(apply(T,S),apply(Tp,Sp)) -> eq#(S,Sp)
     eq#(apply(T,S),apply(Tp,Sp)) -> eq#(T,Tp)
     eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(X,Xp)
     eq#(lambda(X,T),lambda(Xp,Tp)) -> eq#(T,Tp)
    TRS:
     and(false(),false()) -> false()
     and(true(),false()) -> false()
     and(false(),true()) -> false()
     and(true(),true()) -> true()
     eq(nil(),nil()) -> true()
     eq(cons(T,L),nil()) -> false()
     eq(nil(),cons(T,L)) -> false()
     eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
     eq(var(L),var(Lp)) -> eq(L,Lp)
     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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
     eq(apply(T,S),lambda(X,Tp)) -> false()
     eq(lambda(X,T),var(L)) -> false()
     eq(lambda(X,T),apply(Tp,Sp)) -> false()
     eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
     if(true(),var(K),var(L)) -> var(K)
     if(false(),var(K),var(L)) -> var(L)
     ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
     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)))
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     problem:
      DPs:
       
      TRS:
       and(false(),false()) -> false()
       and(true(),false()) -> false()
       and(false(),true()) -> false()
       and(true(),true()) -> true()
       eq(nil(),nil()) -> true()
       eq(cons(T,L),nil()) -> false()
       eq(nil(),cons(T,L)) -> false()
       eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp))
       eq(var(L),var(Lp)) -> eq(L,Lp)
       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(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp))
       eq(apply(T,S),lambda(X,Tp)) -> false()
       eq(lambda(X,T),var(L)) -> false()
       eq(lambda(X,T),apply(Tp,Sp)) -> false()
       eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp))
       if(true(),var(K),var(L)) -> var(K)
       if(false(),var(K),var(L)) -> var(L)
       ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp))
       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