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'))
   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