ceta_equiv: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.1: error below the reduction pair processor
  1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
   pairs:
   
   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)
   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)))
   
    the pairs 
   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)
   
   could not apply the generic reduction pair processor with the following
   Argument Filter: 
   pi(ren#/3) = [1,2,3]
   pi(lambda/2) = [1,2]
   pi(ren/3) = 3
   pi(var/1) = []
   pi(cons/2) = []
   pi(nil/0) = []
   pi(if/3) = 2
   pi(eq/2) = [1]
   pi(apply/2) = 2
   pi(true/0) = []
   pi(false/0) = []
   pi(and/2) = [2,1]
   
   RPO with the following precedence
   precedence(ren#[3]) = 4
   precedence(lambda[2]) = 3
   precedence(var[1]) = 0
   precedence(cons[2]) = 2
   precedence(nil[0]) = 0
   precedence(eq[2]) = 1
   precedence(true[0]) = 0
   precedence(false[0]) = 5
   precedence(and[2]) = 6
   
   precedence(_) = 0
   and the following status
   status(ren#[3]) = mul
   status(lambda[2]) = mul
   status(var[1]) = mul
   status(cons[2]) = lex
   status(nil[0]) = mul
   status(eq[2]) = lex
   status(true[0]) = mul
   status(false[0]) = mul
   status(and[2]) = lex
   
   status(_) = lex
   
   problem when orienting (usable) rules
   could not orient 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)))
   pi( ren(X, Y, lambda(Z, T)) ) = lambda(Z, T)
   pi( 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))) ) = lambda(var, T)
   could not orient lambda(Z, T) >=RPO lambda(var, T)