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 below the reduction pair processor
   1.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))
    rules:
    
    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)))
    
     the pairs 
    ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t))
    
    could not apply the generic root reduction pair processor with the following
    SCNP-version with mu = MAX and the level mapping defined by 
    pi(ren#) = [(3,1)]
    Argument Filter: 
    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) = [2]
    pi(apply/2) = []
    pi(true/0) = []
    pi(false/0) = []
    pi(and/2) = [1,2]
    
    RPO with the following precedence
    precedence(lambda[2]) = 2
    precedence(var[1]) = 0
    precedence(cons[2]) = 2
    precedence(nil[0]) = 2
    precedence(eq[2]) = 1
    precedence(apply[2]) = 3
    precedence(true[0]) = 0
    precedence(false[0]) = 2
    precedence(and[2]) = 4
    
    precedence(_) = 0
    and the following status
    status(lambda[2]) = mul
    status(var[1]) = mul
    status(cons[2]) = lex
    status(nil[0]) = mul
    status(eq[2]) = mul
    status(apply[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)