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) -> U12#(isPalListKind(activate(V)), activate(V)) U12#(tt, V) -> isNeList#(activate(V)) U21#(tt, V1, V2) -> U22#(isPalListKind(activate(V1)), activate(V1), activate(V2)) U22#(tt, V1, V2) -> U23#(isPalListKind(activate(V2)), activate(V1), activate(V2)) U23#(tt, V1, V2) -> U24#(isPalListKind(activate(V2)), activate(V1), activate(V2)) U24#(tt, V1, V2) -> U25#(isList(activate(V1)), activate(V2)) U24#(tt, V1, V2) -> isList#(activate(V1)) U25#(tt, V2) -> isList#(activate(V2)) U41#(tt, V1, V2) -> U42#(isPalListKind(activate(V1)), activate(V1), activate(V2)) U42#(tt, V1, V2) -> U43#(isPalListKind(activate(V2)), activate(V1), activate(V2)) U43#(tt, V1, V2) -> U44#(isPalListKind(activate(V2)), activate(V1), activate(V2)) U44#(tt, V1, V2) -> U45#(isList(activate(V1)), activate(V2)) U44#(tt, V1, V2) -> isList#(activate(V1)) U45#(tt, V2) -> isNeList#(activate(V2)) U51#(tt, V1, V2) -> U52#(isPalListKind(activate(V1)), activate(V1), activate(V2)) U52#(tt, V1, V2) -> U53#(isPalListKind(activate(V2)), activate(V1), activate(V2)) U53#(tt, V1, V2) -> U54#(isPalListKind(activate(V2)), activate(V1), activate(V2)) U54#(tt, V1, V2) -> U55#(isNeList(activate(V1)), activate(V2)) U54#(tt, V1, V2) -> isNeList#(activate(V1)) U55#(tt, V2) -> isList#(activate(V2)) isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)) isList#(n____(V1, V2)) -> U21#(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList#(n____(V1, V2)) -> U41#(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList#(n____(V1, V2)) -> U51#(isPalListKind(activate(V1)), activate(V1), activate(V2)) rules: U11(tt, V) -> U12(isPalListKind(activate(V)), activate(V)) U12(tt, V) -> U13(isNeList(activate(V))) U13(tt) -> tt U21(tt, V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) U22(tt, V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) U23(tt, V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) U24(tt, V1, V2) -> U25(isList(activate(V1)), activate(V2)) U25(tt, V2) -> U26(isList(activate(V2))) U26(tt) -> tt U31(tt, V) -> U32(isPalListKind(activate(V)), activate(V)) U32(tt, V) -> U33(isQid(activate(V))) U33(tt) -> tt U41(tt, V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) U42(tt, V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) U43(tt, V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) U44(tt, V1, V2) -> U45(isList(activate(V1)), activate(V2)) U45(tt, V2) -> U46(isNeList(activate(V2))) U46(tt) -> tt U51(tt, V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) U52(tt, V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) U53(tt, V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) U54(tt, V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) U55(tt, V2) -> U56(isList(activate(V2))) U56(tt) -> tt U61(tt, V) -> U62(isPalListKind(activate(V)), activate(V)) U62(tt, V) -> U63(isQid(activate(V))) U63(tt) -> tt U71(tt, I, P) -> U72(isPalListKind(activate(I)), activate(P)) U72(tt, P) -> U73(isPal(activate(P)), activate(P)) U73(tt, P) -> U74(isPalListKind(activate(P))) U74(tt) -> tt U81(tt, V) -> U82(isPalListKind(activate(V)), activate(V)) U82(tt, V) -> U83(isNePal(activate(V))) U83(tt) -> tt U91(tt, V2) -> U92(isPalListKind(activate(V2))) U92(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__a) -> a activate(n__e) -> e activate(n__i) -> i activate(n__o) -> o activate(n__u) -> u activate(X) -> X e -> n__e i -> n__i isList(V) -> U11(isPalListKind(activate(V)), activate(V)) isList(n__nil) -> tt isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) isNePal(n____(I, n____(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) isPal(n__nil) -> tt 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)) -> U91(isPalListKind(activate(V1)), activate(V2)) 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 U24#(tt, V1, V2) -> U25#(isList(activate(V1)), activate(V2)) U24#(tt, V1, V2) -> isList#(activate(V1)) U44#(tt, V1, V2) -> U45#(isList(activate(V1)), activate(V2)) U44#(tt, V1, V2) -> isList#(activate(V1)) U54#(tt, V1, V2) -> isNeList#(activate(V1)) U55#(tt, V2) -> isList#(activate(V2)) isList#(n____(V1, V2)) -> U21#(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList#(n____(V1, V2)) -> U41#(isPalListKind(activate(V1)), activate(V1), activate(V2)) isNeList#(n____(V1, V2)) -> U51#(isPalListKind(activate(V1)), activate(V1), activate(V2)) could not apply the generic reduction pair processor with the following Argument Filter: pi(U11#/2) = [2] pi(tt/0) = [] pi(U12#/2) = [2] pi(isPalListKind/1) = [1] pi(activate/1) = 1 pi(isNeList#/1) = [1] pi(n____/2) = [1,2] pi(U41#/3) = [2,3] pi(U42#/3) = [2,3] pi(U43#/3) = [2,3] pi(U44#/3) = [2,3] pi(U45#/2) = [2] pi(isList/1) = [] pi(U51#/3) = [2,3] pi(U52#/3) = [2,3] pi(U53#/3) = [2,3] pi(U54#/3) = [2,3] pi(U55#/2) = [1,2] pi(isNeList/1) = 1 pi(isList#/1) = [1] pi(U21#/3) = [2,3] pi(U22#/3) = [2,3] pi(U23#/3) = [2,3] pi(U24#/3) = [2,3] pi(U25#/2) = [2] pi(n__nil/0) = [] pi(nil/0) = [] pi(__/2) = [1,2] 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(U91/2) = [] pi(U11/2) = [] pi(U21/3) = [] pi(U31/2) = 2 pi(U41/3) = [2,3] pi(U51/3) = [2,3] pi(U42/3) = [2,3] pi(U12/2) = [] pi(U22/3) = [] pi(U52/3) = [2] pi(U43/3) = [3] pi(U13/1) = [] pi(U23/3) = [] pi(U53/3) = [2] pi(U44/3) = [3] pi(U24/3) = [] pi(U54/3) = [2] pi(U45/2) = [2] pi(U25/2) = [] pi(U55/2) = [1] pi(U46/1) = [1] pi(U26/1) = [] pi(U56/1) = [1] pi(U32/2) = 2 pi(U33/1) = 1 pi(isQid/1) = 1 pi(U92/1) = [1] RPO with the following precedence precedence(U11#[2]) = 7 precedence(tt[0]) = 6 precedence(U12#[2]) = 7 precedence(isPalListKind[1]) = 1 precedence(isNeList#[1]) = 7 precedence(n____[2]) = 9 precedence(U41#[3]) = 7 precedence(U42#[3]) = 7 precedence(U43#[3]) = 7 precedence(U44#[3]) = 7 precedence(U45#[2]) = 7 precedence(isList[1]) = 6 precedence(U51#[3]) = 7 precedence(U52#[3]) = 7 precedence(U53#[3]) = 7 precedence(U54#[3]) = 7 precedence(U55#[2]) = 7 precedence(isList#[1]) = 7 precedence(U21#[3]) = 7 precedence(U22#[3]) = 7 precedence(U23#[3]) = 7 precedence(U24#[3]) = 7 precedence(U25#[2]) = 7 precedence(n__nil[0]) = 10 precedence(nil[0]) = 10 precedence(__[2]) = 9 precedence(n__a[0]) = 11 precedence(a[0]) = 11 precedence(n__e[0]) = 12 precedence(e[0]) = 12 precedence(n__i[0]) = 13 precedence(i[0]) = 13 precedence(n__o[0]) = 14 precedence(o[0]) = 14 precedence(n__u[0]) = 15 precedence(u[0]) = 15 precedence(U91[2]) = 16 precedence(U11[2]) = 6 precedence(U21[3]) = 6 precedence(U41[3]) = 3 precedence(U51[3]) = 8 precedence(U42[3]) = 3 precedence(U12[2]) = 6 precedence(U22[3]) = 6 precedence(U52[3]) = 4 precedence(U43[3]) = 2 precedence(U13[1]) = 6 precedence(U23[3]) = 6 precedence(U53[3]) = 0 precedence(U44[3]) = 2 precedence(U24[3]) = 6 precedence(U54[3]) = 0 precedence(U45[2]) = 0 precedence(U25[2]) = 6 precedence(U55[2]) = 0 precedence(U46[1]) = 0 precedence(U26[1]) = 6 precedence(U56[1]) = 0 precedence(U92[1]) = 5 precedence(_) = 0 and the following status status(U11#[2]) = mul status(tt[0]) = mul status(U12#[2]) = mul status(isPalListKind[1]) = mul status(isNeList#[1]) = mul status(n____[2]) = lex status(U41#[3]) = mul status(U42#[3]) = mul status(U43#[3]) = mul status(U44#[3]) = mul status(U45#[2]) = mul status(isList[1]) = lex status(U51#[3]) = mul status(U52#[3]) = mul status(U53#[3]) = mul status(U54#[3]) = mul status(U55#[2]) = mul status(isList#[1]) = mul status(U21#[3]) = mul status(U22#[3]) = mul status(U23#[3]) = mul status(U24#[3]) = mul status(U25#[2]) = mul status(n__nil[0]) = mul status(nil[0]) = mul status(__[2]) = 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(U91[2]) = mul status(U11[2]) = lex status(U21[3]) = lex status(U41[3]) = mul status(U51[3]) = mul status(U42[3]) = mul status(U12[2]) = lex status(U22[3]) = lex status(U52[3]) = mul status(U43[3]) = mul status(U13[1]) = lex status(U23[3]) = lex status(U53[3]) = mul status(U44[3]) = mul status(U24[3]) = lex status(U54[3]) = mul status(U45[2]) = mul status(U25[2]) = lex status(U55[2]) = mul status(U46[1]) = mul status(U26[1]) = lex status(U56[1]) = mul status(U92[1]) = mul status(_) = lex problem when orienting (usable) rules could not orient U55(tt, V2) >= U56(isList(activate(V2))) pi( U55(tt, V2) ) = U55(tt) pi( U56(isList(activate(V2))) ) = U56(isList) could not orient U55(tt) >=RPO U56(isList)