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 when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  U11#(tt, V) -> isNeList#(activate(V))
  U21#(tt, V1, V2) -> U22#(isList(activate(V1)), activate(V2))
  U21#(tt, V1, V2) -> isList#(activate(V1))
  U22#(tt, V2) -> isList#(activate(V2))
  U41#(tt, V1, V2) -> U42#(isList(activate(V1)), activate(V2))
  U41#(tt, V1, V2) -> isList#(activate(V1))
  U42#(tt, V2) -> isNeList#(activate(V2))
  U51#(tt, V1, V2) -> U52#(isNeList(activate(V1)), activate(V2))
  U51#(tt, V1, V2) -> isNeList#(activate(V1))
  U52#(tt, V2) -> isList#(activate(V2))
  isList#(V) -> U11#(isPalListKind(activate(V)), activate(V))
  isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  rules:
  
  U11(tt, V) -> U12(isNeList(activate(V)))
  U12(tt) -> tt
  U21(tt, V1, V2) -> U22(isList(activate(V1)), activate(V2))
  U22(tt, V2) -> U23(isList(activate(V2)))
  U23(tt) -> tt
  U31(tt, V) -> U32(isQid(activate(V)))
  U32(tt) -> tt
  U41(tt, V1, V2) -> U42(isList(activate(V1)), activate(V2))
  U42(tt, V2) -> U43(isNeList(activate(V2)))
  U43(tt) -> tt
  U51(tt, V1, V2) -> U52(isNeList(activate(V1)), activate(V2))
  U52(tt, V2) -> U53(isList(activate(V2)))
  U53(tt) -> tt
  U61(tt, V) -> U62(isQid(activate(V)))
  U62(tt) -> tt
  U71(tt, V) -> U72(isNePal(activate(V)))
  U72(tt) -> tt
  __(__(X, Y), Z) -> __(X, __(Y, Z))
  __(X, nil) -> X
  __(nil, X) -> X
  __(X1, X2) -> n____(X1, X2)
  a -> n__a
  activate(n__nil) -> nil
  activate(n____(X1, X2)) -> __(activate(X1), activate(X2))
  activate(n__isPalListKind(X)) -> isPalListKind(X)
  activate(n__and(X1, X2)) -> and(activate(X1), X2)
  activate(n__isPal(X)) -> isPal(X)
  activate(n__a) -> a
  activate(n__e) -> e
  activate(n__i) -> i
  activate(n__o) -> o
  activate(n__u) -> u
  activate(X) -> X
  and(tt, X) -> activate(X)
  and(X1, X2) -> n__and(X1, X2)
  e -> n__e
  i -> n__i
  isList(V) -> U11(isPalListKind(activate(V)), activate(V))
  isList(n__nil) -> tt
  isList(n____(V1, V2)) -> U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  isNeList(V) -> U31(isPalListKind(activate(V)), activate(V))
  isNeList(n____(V1, V2)) -> U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  isNeList(n____(V1, V2)) -> U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  isNePal(V) -> U61(isPalListKind(activate(V)), activate(V))
  isNePal(n____(I, n____(P, I))) -> and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))
  isPal(V) -> U71(isPalListKind(activate(V)), activate(V))
  isPal(n__nil) -> tt
  isPal(X) -> n__isPal(X)
  isPalListKind(n__a) -> tt
  isPalListKind(n__e) -> tt
  isPalListKind(n__i) -> tt
  isPalListKind(n__nil) -> tt
  isPalListKind(n__o) -> tt
  isPalListKind(n__u) -> tt
  isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))
  isPalListKind(X) -> n__isPalListKind(X)
  isQid(n__a) -> tt
  isQid(n__e) -> tt
  isQid(n__i) -> tt
  isQid(n__o) -> tt
  isQid(n__u) -> tt
  nil -> n__nil
  o -> n__o
  u -> n__u
  
   the pairs 
  U42#(tt, V2) -> isNeList#(activate(V2))
  U51#(tt, V1, V2) -> U52#(isNeList(activate(V1)), activate(V2))
  U52#(tt, V2) -> isList#(activate(V2))
  isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(U11#) = [(2,0)]
  pi(isNeList#) = [(epsilon,0)]
  pi(U41#) = [(epsilon,0),(2,0)]
  pi(U42#) = [(epsilon,0)]
  pi(U51#) = [(epsilon,0),(2,0)]
  pi(U52#) = [(epsilon,0)]
  pi(isList#) = [(epsilon,0),(1,0)]
  pi(U21#) = [(epsilon,0),(2,0),(3,0)]
  pi(U22#) = [(epsilon,0),(1,0)]
  Argument Filter: 
  pi(U11#/2) = []
  pi(tt/0) = []
  pi(isNeList#/1) = 1
  pi(activate/1) = 1
  pi(n____/2) = [1,2]
  pi(U41#/3) = [1,3]
  pi(and/2) = 2
  pi(isPalListKind/1) = []
  pi(n__isPalListKind/1) = []
  pi(U42#/2) = [1,2]
  pi(isList/1) = []
  pi(U51#/3) = [1,3]
  pi(U52#/2) = [2,1]
  pi(isNeList/1) = []
  pi(isList#/1) = []
  pi(U21#/3) = []
  pi(U22#/2) = 2
  pi(n__nil/0) = []
  pi(nil/0) = []
  pi(__/2) = [1,2]
  pi(n__and/2) = 2
  pi(n__isPal/1) = [1]
  pi(isPal/1) = [1]
  pi(n__a/0) = []
  pi(a/0) = []
  pi(n__e/0) = []
  pi(e/0) = []
  pi(n__i/0) = []
  pi(i/0) = []
  pi(n__o/0) = []
  pi(o/0) = []
  pi(n__u/0) = []
  pi(u/0) = []
  pi(U11/2) = []
  pi(U21/3) = []
  pi(U31/2) = []
  pi(U41/3) = 1
  pi(U51/3) = []
  pi(U42/2) = []
  pi(U12/1) = []
  pi(U52/2) = 1
  pi(U22/2) = []
  pi(U43/1) = []
  pi(U53/1) = []
  pi(U23/1) = []
  pi(U32/1) = []
  pi(isQid/1) = []
  pi(U71/2) = []
  pi(U72/1) = []
  pi(isNePal/1) = []
  pi(U61/2) = [1,2]
  pi(U62/1) = []
  
  RPO with the following precedence
  precedence(U11#[2]) = 1
  precedence(tt[0]) = 1
  precedence(n____[2]) = 8
  precedence(U41#[3]) = 1
  precedence(isPalListKind[1]) = 2
  precedence(n__isPalListKind[1]) = 2
  precedence(U42#[2]) = 1
  precedence(isList[1]) = 1
  precedence(U51#[3]) = 4
  precedence(U52#[2]) = 3
  precedence(isNeList[1]) = 2
  precedence(isList#[1]) = 1
  precedence(U21#[3]) = 5
  precedence(n__nil[0]) = 9
  precedence(nil[0]) = 9
  precedence(__[2]) = 8
  precedence(n__isPal[1]) = 7
  precedence(isPal[1]) = 7
  precedence(n__a[0]) = 10
  precedence(a[0]) = 10
  precedence(n__e[0]) = 11
  precedence(e[0]) = 11
  precedence(n__i[0]) = 12
  precedence(i[0]) = 12
  precedence(n__o[0]) = 13
  precedence(o[0]) = 13
  precedence(n__u[0]) = 14
  precedence(u[0]) = 14
  precedence(U11[2]) = 1
  precedence(U21[3]) = 1
  precedence(U31[2]) = 2
  precedence(U51[3]) = 2
  precedence(U42[2]) = 1
  precedence(U12[1]) = 1
  precedence(U22[2]) = 1
  precedence(U43[1]) = 1
  precedence(U53[1]) = 1
  precedence(U23[1]) = 1
  precedence(U32[1]) = 1
  precedence(isQid[1]) = 2
  precedence(U71[2]) = 7
  precedence(U72[1]) = 6
  precedence(isNePal[1]) = 16
  precedence(U61[2]) = 15
  precedence(U62[1]) = 0
  
  precedence(_) = 0
  and the following status
  status(U11#[2]) = mul
  status(tt[0]) = mul
  status(n____[2]) = lex
  status(U41#[3]) = mul
  status(isPalListKind[1]) = mul
  status(n__isPalListKind[1]) = mul
  status(U42#[2]) = mul
  status(isList[1]) = lex
  status(U51#[3]) = mul
  status(U52#[2]) = lex
  status(isNeList[1]) = mul
  status(isList#[1]) = lex
  status(U21#[3]) = mul
  status(n__nil[0]) = mul
  status(nil[0]) = mul
  status(__[2]) = lex
  status(n__isPal[1]) = lex
  status(isPal[1]) = lex
  status(n__a[0]) = mul
  status(a[0]) = mul
  status(n__e[0]) = mul
  status(e[0]) = mul
  status(n__i[0]) = mul
  status(i[0]) = mul
  status(n__o[0]) = mul
  status(o[0]) = mul
  status(n__u[0]) = mul
  status(u[0]) = mul
  status(U11[2]) = lex
  status(U21[3]) = lex
  status(U31[2]) = mul
  status(U51[3]) = mul
  status(U42[2]) = lex
  status(U12[1]) = lex
  status(U22[2]) = lex
  status(U43[1]) = lex
  status(U53[1]) = lex
  status(U23[1]) = lex
  status(U32[1]) = lex
  status(isQid[1]) = mul
  status(U71[2]) = lex
  status(U72[1]) = mul
  status(isNePal[1]) = mul
  status(U61[2]) = mul
  status(U62[1]) = mul
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair U41#(tt, V1, V2) -> U42#(isList(activate(V1)), activate(V2)) weakly:
  [(U41#(tt, V1, V2),0),(V1,0)] >=mu [(U42#(isList(activate(V1)), activate(V2)),0)] could not be ensured