ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.3: error below the reduction pair processor
  1.1.3.1: error below the reduction pair processor
   1.1.3.1.1: error below the reduction pair processor
    1.1.3.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
     pairs:
     
     proper#(isNeList(X)) -> proper#(X)
     proper#(isNePal(X)) -> proper#(X)
     proper#(isPal(X)) -> proper#(X)
     rules:
     
     __(mark(X1), X2) -> mark(__(X1, X2))
     __(X1, mark(X2)) -> mark(__(X1, X2))
     __(ok(X1), ok(X2)) -> ok(__(X1, X2))
     active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z)))
     active(__(X, nil)) -> mark(X)
     active(__(nil, X)) -> mark(X)
     active(and(tt, X)) -> mark(X)
     active(isList(V)) -> mark(isNeList(V))
     active(isList(nil)) -> mark(tt)
     active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2)))
     active(isNeList(V)) -> mark(isQid(V))
     active(isNeList(__(V1, V2))) -> mark(and(isList(V1), isNeList(V2)))
     active(isNeList(__(V1, V2))) -> mark(and(isNeList(V1), isList(V2)))
     active(isNePal(V)) -> mark(isQid(V))
     active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P)))
     active(isPal(V)) -> mark(isNePal(V))
     active(isPal(nil)) -> mark(tt)
     active(isQid(a)) -> mark(tt)
     active(isQid(e)) -> mark(tt)
     active(isQid(i)) -> mark(tt)
     active(isQid(o)) -> mark(tt)
     active(isQid(u)) -> mark(tt)
     active(__(X1, X2)) -> __(active(X1), X2)
     active(__(X1, X2)) -> __(X1, active(X2))
     active(and(X1, X2)) -> and(active(X1), X2)
     and(mark(X1), X2) -> mark(and(X1, X2))
     and(ok(X1), ok(X2)) -> ok(and(X1, X2))
     isList(ok(X)) -> ok(isList(X))
     isNeList(ok(X)) -> ok(isNeList(X))
     isNePal(ok(X)) -> ok(isNePal(X))
     isPal(ok(X)) -> ok(isPal(X))
     isQid(ok(X)) -> ok(isQid(X))
     proper(__(X1, X2)) -> __(proper(X1), proper(X2))
     proper(nil) -> ok(nil)
     proper(and(X1, X2)) -> and(proper(X1), proper(X2))
     proper(tt) -> ok(tt)
     proper(isList(X)) -> isList(proper(X))
     proper(isNeList(X)) -> isNeList(proper(X))
     proper(isQid(X)) -> isQid(proper(X))
     proper(isNePal(X)) -> isNePal(proper(X))
     proper(isPal(X)) -> isPal(proper(X))
     proper(a) -> ok(a)
     proper(e) -> ok(e)
     proper(i) -> ok(i)
     proper(o) -> ok(o)
     proper(u) -> ok(u)
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     
      the pairs 
     proper#(isNePal(X)) -> proper#(X)
     
     could not apply the generic root reduction pair processor with the following
     SCNP-version with mu = MS and the level mapping defined by 
     pi(proper#) = [(epsilon,0),(1,0)]
     Argument Filter: 
     pi(proper#/1) = []
     pi(isNeList/1) = 1
     pi(isNePal/1) = [1]
     pi(isPal/1) = 1
     
     RPO with the following precedence
     precedence(proper#[1]) = 0
     precedence(isNePal[1]) = 1
     
     precedence(_) = 0
     and the following status
     status(proper#[1]) = lex
     status(isNePal[1]) = lex
     
     status(_) = lex
     
     problem when orienting DPs
     cannot orient pair proper#(isNeList(X)) -> proper#(X) weakly:
     [(proper#(isNeList(X)),0),(isNeList(X),0)] >=mu [(proper#(X),0),(X,0)] could not be ensured