ceta_eq: 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(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))
   ren#(x, y, lambda(z, t)) -> 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 = MS and the level mapping defined by 
   pi(ren#) = [(epsilon,0),(2,0),(3,0)]
   polynomial interpretration over naturals with negative constants
   Pol(ren#(x_1, x_2, x_3)) = 1
   Pol(lambda(x_1, x_2)) = 1 + x_2
   Pol(ren(x_1, x_2, x_3)) = x_3
   Pol(var(x_1)) = 0
   Pol(cons(x_1, x_2)) = 0
   Pol(nil) = 0
   Pol(if(x_1, x_2, x_3)) = 0
   Pol(eq(x_1, x_2)) = 0
   Pol(apply(x_1, x_2)) = 0
   Pol(true) = 0
   Pol(false) = 0
   Pol(and(x_1, x_2)) = 1
   problem when orienting DPs
   cannot orient pair ren#(x, y, lambda(z, t)) -> ren#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)) strictly:
   [(ren#(x, y, lambda(z, t)),0),(y,0),(lambda(z, t),0)] >mu [(ren#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)),0),(y,0),(ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t),0)] could not be ensured