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 below the reduction pair processor
   1.1.1.1.1: error below the reduction pair processor
    1.1.1.1.1.1: error when applying the reduction pair processor to remove from the DP problem
     pairs:
     
     active#(U61(tt, V)) -> mark#(U62(isQid(V)))
     active#(isNePal(V)) -> mark#(U61(isPalListKind(V), V))
     mark#(__(X1, X2)) -> active#(__(mark(X1), mark(X2)))
     mark#(U11(X1, X2)) -> active#(U11(mark(X1), X2))
     mark#(U12(X)) -> active#(U12(mark(X)))
     mark#(U12(X)) -> mark#(X)
     mark#(isNeList(X)) -> active#(isNeList(X))
     mark#(U21(X1, X2, X3)) -> active#(U21(mark(X1), X2, X3))
     mark#(U22(X1, X2)) -> active#(U22(mark(X1), X2))
     mark#(isList(X)) -> active#(isList(X))
     mark#(U23(X)) -> active#(U23(mark(X)))
     mark#(U31(X1, X2)) -> active#(U31(mark(X1), X2))
     mark#(U32(X)) -> active#(U32(mark(X)))
     mark#(isQid(X)) -> active#(isQid(X))
     mark#(U41(X1, X2, X3)) -> active#(U41(mark(X1), X2, X3))
     mark#(U42(X1, X2)) -> active#(U42(mark(X1), X2))
     mark#(U43(X)) -> active#(U43(mark(X)))
     mark#(U51(X1, X2, X3)) -> active#(U51(mark(X1), X2, X3))
     mark#(U52(X1, X2)) -> active#(U52(mark(X1), X2))
     mark#(U53(X)) -> active#(U53(mark(X)))
     mark#(U53(X)) -> mark#(X)
     mark#(U61(X1, X2)) -> active#(U61(mark(X1), X2))
     mark#(U61(X1, X2)) -> mark#(X1)
     mark#(U62(X)) -> active#(U62(mark(X)))
     mark#(U62(X)) -> mark#(X)
     mark#(U71(X1, X2)) -> active#(U71(mark(X1), X2))
     mark#(U72(X)) -> active#(U72(mark(X)))
     mark#(isNePal(X)) -> active#(isNePal(X))
     mark#(isPalListKind(X)) -> active#(isPalListKind(X))
     mark#(isPal(X)) -> active#(isPal(X))
     rules:
     
     U11(mark(X1), X2) -> U11(X1, X2)
     U11(X1, mark(X2)) -> U11(X1, X2)
     U11(active(X1), X2) -> U11(X1, X2)
     U11(X1, active(X2)) -> U11(X1, X2)
     U12(mark(X)) -> U12(X)
     U12(active(X)) -> U12(X)
     U21(mark(X1), X2, X3) -> U21(X1, X2, X3)
     U21(X1, mark(X2), X3) -> U21(X1, X2, X3)
     U21(X1, X2, mark(X3)) -> U21(X1, X2, X3)
     U21(active(X1), X2, X3) -> U21(X1, X2, X3)
     U21(X1, active(X2), X3) -> U21(X1, X2, X3)
     U21(X1, X2, active(X3)) -> U21(X1, X2, X3)
     U22(mark(X1), X2) -> U22(X1, X2)
     U22(X1, mark(X2)) -> U22(X1, X2)
     U22(active(X1), X2) -> U22(X1, X2)
     U22(X1, active(X2)) -> U22(X1, X2)
     U23(mark(X)) -> U23(X)
     U23(active(X)) -> U23(X)
     U31(mark(X1), X2) -> U31(X1, X2)
     U31(X1, mark(X2)) -> U31(X1, X2)
     U31(active(X1), X2) -> U31(X1, X2)
     U31(X1, active(X2)) -> U31(X1, X2)
     U32(mark(X)) -> U32(X)
     U32(active(X)) -> U32(X)
     U41(mark(X1), X2, X3) -> U41(X1, X2, X3)
     U41(X1, mark(X2), X3) -> U41(X1, X2, X3)
     U41(X1, X2, mark(X3)) -> U41(X1, X2, X3)
     U41(active(X1), X2, X3) -> U41(X1, X2, X3)
     U41(X1, active(X2), X3) -> U41(X1, X2, X3)
     U41(X1, X2, active(X3)) -> U41(X1, X2, X3)
     U42(mark(X1), X2) -> U42(X1, X2)
     U42(X1, mark(X2)) -> U42(X1, X2)
     U42(active(X1), X2) -> U42(X1, X2)
     U42(X1, active(X2)) -> U42(X1, X2)
     U43(mark(X)) -> U43(X)
     U43(active(X)) -> U43(X)
     U51(mark(X1), X2, X3) -> U51(X1, X2, X3)
     U51(X1, mark(X2), X3) -> U51(X1, X2, X3)
     U51(X1, X2, mark(X3)) -> U51(X1, X2, X3)
     U51(active(X1), X2, X3) -> U51(X1, X2, X3)
     U51(X1, active(X2), X3) -> U51(X1, X2, X3)
     U51(X1, X2, active(X3)) -> U51(X1, X2, X3)
     U52(mark(X1), X2) -> U52(X1, X2)
     U52(X1, mark(X2)) -> U52(X1, X2)
     U52(active(X1), X2) -> U52(X1, X2)
     U52(X1, active(X2)) -> U52(X1, X2)
     U53(mark(X)) -> U53(X)
     U53(active(X)) -> U53(X)
     U61(mark(X1), X2) -> U61(X1, X2)
     U61(X1, mark(X2)) -> U61(X1, X2)
     U61(active(X1), X2) -> U61(X1, X2)
     U61(X1, active(X2)) -> U61(X1, X2)
     U62(mark(X)) -> U62(X)
     U62(active(X)) -> U62(X)
     U71(mark(X1), X2) -> U71(X1, X2)
     U71(X1, mark(X2)) -> U71(X1, X2)
     U71(active(X1), X2) -> U71(X1, X2)
     U71(X1, active(X2)) -> U71(X1, X2)
     U72(mark(X)) -> U72(X)
     U72(active(X)) -> U72(X)
     __(mark(X1), X2) -> __(X1, X2)
     __(X1, mark(X2)) -> __(X1, X2)
     __(active(X1), X2) -> __(X1, X2)
     __(X1, active(X2)) -> __(X1, X2)
     active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z)))
     active(__(X, nil)) -> mark(X)
     active(__(nil, X)) -> mark(X)
     active(U11(tt, V)) -> mark(U12(isNeList(V)))
     active(U12(tt)) -> mark(tt)
     active(U21(tt, V1, V2)) -> mark(U22(isList(V1), V2))
     active(U22(tt, V2)) -> mark(U23(isList(V2)))
     active(U23(tt)) -> mark(tt)
     active(U31(tt, V)) -> mark(U32(isQid(V)))
     active(U32(tt)) -> mark(tt)
     active(U41(tt, V1, V2)) -> mark(U42(isList(V1), V2))
     active(U42(tt, V2)) -> mark(U43(isNeList(V2)))
     active(U43(tt)) -> mark(tt)
     active(U51(tt, V1, V2)) -> mark(U52(isNeList(V1), V2))
     active(U52(tt, V2)) -> mark(U53(isList(V2)))
     active(U53(tt)) -> mark(tt)
     active(U61(tt, V)) -> mark(U62(isQid(V)))
     active(U62(tt)) -> mark(tt)
     active(U71(tt, V)) -> mark(U72(isNePal(V)))
     active(U72(tt)) -> mark(tt)
     active(and(tt, X)) -> mark(X)
     active(isList(V)) -> mark(U11(isPalListKind(V), V))
     active(isList(nil)) -> mark(tt)
     active(isList(__(V1, V2))) -> mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
     active(isNeList(V)) -> mark(U31(isPalListKind(V), V))
     active(isNeList(__(V1, V2))) -> mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
     active(isNeList(__(V1, V2))) -> mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2))
     active(isNePal(V)) -> mark(U61(isPalListKind(V), V))
     active(isNePal(__(I, __(P, I)))) -> mark(and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))))
     active(isPal(V)) -> mark(U71(isPalListKind(V), V))
     active(isPal(nil)) -> mark(tt)
     active(isPalListKind(a)) -> mark(tt)
     active(isPalListKind(e)) -> mark(tt)
     active(isPalListKind(i)) -> mark(tt)
     active(isPalListKind(nil)) -> mark(tt)
     active(isPalListKind(o)) -> mark(tt)
     active(isPalListKind(u)) -> mark(tt)
     active(isPalListKind(__(V1, V2))) -> mark(and(isPalListKind(V1), isPalListKind(V2)))
     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)
     and(mark(X1), X2) -> and(X1, X2)
     and(X1, mark(X2)) -> and(X1, X2)
     and(active(X1), X2) -> and(X1, X2)
     and(X1, active(X2)) -> and(X1, X2)
     isList(mark(X)) -> isList(X)
     isList(active(X)) -> isList(X)
     isNeList(mark(X)) -> isNeList(X)
     isNeList(active(X)) -> isNeList(X)
     isNePal(mark(X)) -> isNePal(X)
     isNePal(active(X)) -> isNePal(X)
     isPal(mark(X)) -> isPal(X)
     isPal(active(X)) -> isPal(X)
     isPalListKind(mark(X)) -> isPalListKind(X)
     isPalListKind(active(X)) -> isPalListKind(X)
     isQid(mark(X)) -> isQid(X)
     isQid(active(X)) -> isQid(X)
     mark(__(X1, X2)) -> active(__(mark(X1), mark(X2)))
     mark(nil) -> active(nil)
     mark(U11(X1, X2)) -> active(U11(mark(X1), X2))
     mark(tt) -> active(tt)
     mark(U12(X)) -> active(U12(mark(X)))
     mark(isNeList(X)) -> active(isNeList(X))
     mark(U21(X1, X2, X3)) -> active(U21(mark(X1), X2, X3))
     mark(U22(X1, X2)) -> active(U22(mark(X1), X2))
     mark(isList(X)) -> active(isList(X))
     mark(U23(X)) -> active(U23(mark(X)))
     mark(U31(X1, X2)) -> active(U31(mark(X1), X2))
     mark(U32(X)) -> active(U32(mark(X)))
     mark(isQid(X)) -> active(isQid(X))
     mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3))
     mark(U42(X1, X2)) -> active(U42(mark(X1), X2))
     mark(U43(X)) -> active(U43(mark(X)))
     mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3))
     mark(U52(X1, X2)) -> active(U52(mark(X1), X2))
     mark(U53(X)) -> active(U53(mark(X)))
     mark(U61(X1, X2)) -> active(U61(mark(X1), X2))
     mark(U62(X)) -> active(U62(mark(X)))
     mark(U71(X1, X2)) -> active(U71(mark(X1), X2))
     mark(U72(X)) -> active(U72(mark(X)))
     mark(isNePal(X)) -> active(isNePal(X))
     mark(and(X1, X2)) -> active(and(mark(X1), X2))
     mark(isPalListKind(X)) -> active(isPalListKind(X))
     mark(isPal(X)) -> active(isPal(X))
     mark(a) -> active(a)
     mark(e) -> active(e)
     mark(i) -> active(i)
     mark(o) -> active(o)
     mark(u) -> active(u)
     
      the pairs 
     active#(isNePal(V)) -> mark#(U61(isPalListKind(V), V))
     
     could not apply the generic reduction pair processor with the following
     Argument Filter: 
     pi(mark#/1) = [1]
     pi(__/2) = [1,2]
     pi(active#/1) = [1]
     pi(mark/1) = 1
     pi(U11/2) = [2]
     pi(U12/1) = 1
     pi(isNeList/1) = [1]
     pi(U21/3) = [1,2,3]
     pi(U22/2) = [2]
     pi(isList/1) = [1]
     pi(U23/1) = []
     pi(U31/2) = [2]
     pi(U32/1) = []
     pi(isQid/1) = []
     pi(U41/3) = [2]
     pi(U61/2) = 1
     pi(tt/0) = []
     pi(U62/1) = 1
     pi(U42/2) = 1
     pi(U43/1) = []
     pi(U51/3) = [3]
     pi(U52/2) = [2]
     pi(U53/1) = 1
     pi(U71/2) = []
     pi(isNePal/1) = []
     pi(isPalListKind/1) = []
     pi(U72/1) = 1
     pi(isPal/1) = []
     pi(active/1) = 1
     pi(nil/0) = []
     pi(and/2) = 2
     pi(a/0) = []
     pi(e/0) = []
     pi(i/0) = []
     pi(o/0) = []
     pi(u/0) = []
     
     RPO with the following precedence
     precedence(mark#[1]) = 2
     precedence(__[2]) = 0
     precedence(active#[1]) = 2
     precedence(U11[2]) = 6
     precedence(isNeList[1]) = 6
     precedence(U21[3]) = 4
     precedence(U22[2]) = 4
     precedence(isList[1]) = 6
     precedence(U23[1]) = 3
     precedence(U31[2]) = 5
     precedence(U32[1]) = 5
     precedence(isQid[1]) = 1
     precedence(U41[3]) = 6
     precedence(tt[0]) = 1
     precedence(U43[1]) = 1
     precedence(U51[3]) = 6
     precedence(U52[2]) = 6
     precedence(U71[2]) = 7
     precedence(isNePal[1]) = 7
     precedence(isPalListKind[1]) = 1
     precedence(isPal[1]) = 7
     precedence(nil[0]) = 8
     precedence(a[0]) = 9
     precedence(e[0]) = 10
     precedence(i[0]) = 11
     precedence(o[0]) = 1
     precedence(u[0]) = 12
     
     precedence(_) = 0
     and the following status
     status(mark#[1]) = mul
     status(__[2]) = lex
     status(active#[1]) = mul
     status(U11[2]) = mul
     status(isNeList[1]) = mul
     status(U21[3]) = mul
     status(U22[2]) = mul
     status(isList[1]) = mul
     status(U23[1]) = lex
     status(U31[2]) = lex
     status(U32[1]) = lex
     status(isQid[1]) = mul
     status(U41[3]) = mul
     status(tt[0]) = mul
     status(U43[1]) = mul
     status(U51[3]) = mul
     status(U52[2]) = mul
     status(U71[2]) = lex
     status(isNePal[1]) = lex
     status(isPalListKind[1]) = mul
     status(isPal[1]) = lex
     status(nil[0]) = mul
     status(a[0]) = mul
     status(e[0]) = mul
     status(i[0]) = mul
     status(o[0]) = mul
     status(u[0]) = mul
     
     status(_) = lex
     
     problem when orienting DPs
     could not orient active#(U61(tt, V)) >= mark#(U62(isQid(V)))
     pi( active#(U61(tt, V)) ) = active#(tt)
     pi( mark#(U62(isQid(V))) ) = mark#(isQid)
     could not orient active#(tt) >=RPO mark#(isQid)