YES
(VAR X Y Z V V1 V2 I P X1 X2)
(RULES 
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
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
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
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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
)

Proving termination of rewriting for PALINDROME_complete_noand_FR:

-> Dependency pairs:
nF___(__(X,Y),Z) -> nF___(X,__(Y,Z))
nF___(__(X,Y),Z) -> nF___(Y,Z)
nF_U11(tt,V) -> nF_U12(isPalListKind(activate(V)),activate(V))
nF_U11(tt,V) -> nF_isPalListKind(activate(V))
nF_U11(tt,V) -> nF_activate(V)
nF_U12(tt,V) -> nF_U13(isNeList(activate(V)))
nF_U12(tt,V) -> nF_isNeList(activate(V))
nF_U12(tt,V) -> nF_activate(V)
nF_U21(tt,V1,V2) -> nF_U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U21(tt,V1,V2) -> nF_isPalListKind(activate(V1))
nF_U21(tt,V1,V2) -> nF_activate(V1)
nF_U21(tt,V1,V2) -> nF_activate(V2)
nF_U22(tt,V1,V2) -> nF_U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U22(tt,V1,V2) -> nF_isPalListKind(activate(V2))
nF_U22(tt,V1,V2) -> nF_activate(V2)
nF_U22(tt,V1,V2) -> nF_activate(V1)
nF_U23(tt,V1,V2) -> nF_U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U23(tt,V1,V2) -> nF_isPalListKind(activate(V2))
nF_U23(tt,V1,V2) -> nF_activate(V2)
nF_U23(tt,V1,V2) -> nF_activate(V1)
nF_U24(tt,V1,V2) -> nF_U25(isList(activate(V1)),activate(V2))
nF_U24(tt,V1,V2) -> nF_isList(activate(V1))
nF_U24(tt,V1,V2) -> nF_activate(V1)
nF_U24(tt,V1,V2) -> nF_activate(V2)
nF_U25(tt,V2) -> nF_U26(isList(activate(V2)))
nF_U25(tt,V2) -> nF_isList(activate(V2))
nF_U25(tt,V2) -> nF_activate(V2)
nF_U31(tt,V) -> nF_U32(isPalListKind(activate(V)),activate(V))
nF_U31(tt,V) -> nF_isPalListKind(activate(V))
nF_U31(tt,V) -> nF_activate(V)
nF_U32(tt,V) -> nF_U33(isQid(activate(V)))
nF_U32(tt,V) -> nF_isQid(activate(V))
nF_U32(tt,V) -> nF_activate(V)
nF_U41(tt,V1,V2) -> nF_U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U41(tt,V1,V2) -> nF_isPalListKind(activate(V1))
nF_U41(tt,V1,V2) -> nF_activate(V1)
nF_U41(tt,V1,V2) -> nF_activate(V2)
nF_U42(tt,V1,V2) -> nF_U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U42(tt,V1,V2) -> nF_isPalListKind(activate(V2))
nF_U42(tt,V1,V2) -> nF_activate(V2)
nF_U42(tt,V1,V2) -> nF_activate(V1)
nF_U43(tt,V1,V2) -> nF_U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U43(tt,V1,V2) -> nF_isPalListKind(activate(V2))
nF_U43(tt,V1,V2) -> nF_activate(V2)
nF_U43(tt,V1,V2) -> nF_activate(V1)
nF_U44(tt,V1,V2) -> nF_U45(isList(activate(V1)),activate(V2))
nF_U44(tt,V1,V2) -> nF_isList(activate(V1))
nF_U44(tt,V1,V2) -> nF_activate(V1)
nF_U44(tt,V1,V2) -> nF_activate(V2)
nF_U45(tt,V2) -> nF_U46(isNeList(activate(V2)))
nF_U45(tt,V2) -> nF_isNeList(activate(V2))
nF_U45(tt,V2) -> nF_activate(V2)
nF_U51(tt,V1,V2) -> nF_U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U51(tt,V1,V2) -> nF_isPalListKind(activate(V1))
nF_U51(tt,V1,V2) -> nF_activate(V1)
nF_U51(tt,V1,V2) -> nF_activate(V2)
nF_U52(tt,V1,V2) -> nF_U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U52(tt,V1,V2) -> nF_isPalListKind(activate(V2))
nF_U52(tt,V1,V2) -> nF_activate(V2)
nF_U52(tt,V1,V2) -> nF_activate(V1)
nF_U53(tt,V1,V2) -> nF_U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U53(tt,V1,V2) -> nF_isPalListKind(activate(V2))
nF_U53(tt,V1,V2) -> nF_activate(V2)
nF_U53(tt,V1,V2) -> nF_activate(V1)
nF_U54(tt,V1,V2) -> nF_U55(isNeList(activate(V1)),activate(V2))
nF_U54(tt,V1,V2) -> nF_isNeList(activate(V1))
nF_U54(tt,V1,V2) -> nF_activate(V1)
nF_U54(tt,V1,V2) -> nF_activate(V2)
nF_U55(tt,V2) -> nF_U56(isList(activate(V2)))
nF_U55(tt,V2) -> nF_isList(activate(V2))
nF_U55(tt,V2) -> nF_activate(V2)
nF_U61(tt,V) -> nF_U62(isPalListKind(activate(V)),activate(V))
nF_U61(tt,V) -> nF_isPalListKind(activate(V))
nF_U61(tt,V) -> nF_activate(V)
nF_U62(tt,V) -> nF_U63(isQid(activate(V)))
nF_U62(tt,V) -> nF_isQid(activate(V))
nF_U62(tt,V) -> nF_activate(V)
nF_U71(tt,I,P) -> nF_U72(isPalListKind(activate(I)),activate(P))
nF_U71(tt,I,P) -> nF_isPalListKind(activate(I))
nF_U71(tt,I,P) -> nF_activate(I)
nF_U71(tt,I,P) -> nF_activate(P)
nF_U72(tt,P) -> nF_U73(isPal(activate(P)),activate(P))
nF_U72(tt,P) -> nF_isPal(activate(P))
nF_U72(tt,P) -> nF_activate(P)
nF_U73(tt,P) -> nF_U74(isPalListKind(activate(P)))
nF_U73(tt,P) -> nF_isPalListKind(activate(P))
nF_U73(tt,P) -> nF_activate(P)
nF_U81(tt,V) -> nF_U82(isPalListKind(activate(V)),activate(V))
nF_U81(tt,V) -> nF_isPalListKind(activate(V))
nF_U81(tt,V) -> nF_activate(V)
nF_U82(tt,V) -> nF_U83(isNePal(activate(V)))
nF_U82(tt,V) -> nF_isNePal(activate(V))
nF_U82(tt,V) -> nF_activate(V)
nF_U91(tt,V2) -> nF_U92(isPalListKind(activate(V2)))
nF_U91(tt,V2) -> nF_isPalListKind(activate(V2))
nF_U91(tt,V2) -> nF_activate(V2)
nF_isList(V) -> nF_U11(isPalListKind(activate(V)),activate(V))
nF_isList(V) -> nF_isPalListKind(activate(V))
nF_isList(V) -> nF_activate(V)
nF_isList(n____(V1,V2)) -> nF_U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isList(n____(V1,V2)) -> nF_isPalListKind(activate(V1))
nF_isList(n____(V1,V2)) -> nF_activate(V1)
nF_isList(n____(V1,V2)) -> nF_activate(V2)
nF_isNeList(V) -> nF_U31(isPalListKind(activate(V)),activate(V))
nF_isNeList(V) -> nF_isPalListKind(activate(V))
nF_isNeList(V) -> nF_activate(V)
nF_isNeList(n____(V1,V2)) -> nF_U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_isPalListKind(activate(V1))
nF_isNeList(n____(V1,V2)) -> nF_activate(V1)
nF_isNeList(n____(V1,V2)) -> nF_activate(V2)
nF_isNeList(n____(V1,V2)) -> nF_U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNePal(V) -> nF_U61(isPalListKind(activate(V)),activate(V))
nF_isNePal(V) -> nF_isPalListKind(activate(V))
nF_isNePal(V) -> nF_activate(V)
nF_isNePal(n____(I,n____(P,I))) -> nF_U71(isQid(activate(I)),activate(I),activate(P))
nF_isNePal(n____(I,n____(P,I))) -> nF_isQid(activate(I))
nF_isNePal(n____(I,n____(P,I))) -> nF_activate(I)
nF_isNePal(n____(I,n____(P,I))) -> nF_activate(P)
nF_isPal(V) -> nF_U81(isPalListKind(activate(V)),activate(V))
nF_isPal(V) -> nF_isPalListKind(activate(V))
nF_isPal(V) -> nF_activate(V)
nF_isPalListKind(n____(V1,V2)) -> nF_U91(isPalListKind(activate(V1)),activate(V2))
nF_isPalListKind(n____(V1,V2)) -> nF_isPalListKind(activate(V1))
nF_isPalListKind(n____(V1,V2)) -> nF_activate(V1)
nF_isPalListKind(n____(V1,V2)) -> nF_activate(V2)
nF_activate(n__nil) -> nF_nil
nF_activate(n____(X1,X2)) -> nF___(activate(X1),activate(X2))
nF_activate(n____(X1,X2)) -> nF_activate(X1)
nF_activate(n____(X1,X2)) -> nF_activate(X2)
nF_activate(n__a) -> nF_a
nF_activate(n__e) -> nF_e
nF_activate(n__i) -> nF_i
nF_activate(n__o) -> nF_o
nF_activate(n__u) -> nF_u

-> Dependency pairs narrowed: 
nF_U24(tt,V1,V2) -> nF_U25(isList(activate(V1)),activate(V2))
nF_U44(tt,V1,V2) -> nF_U45(isList(activate(V1)),activate(V2))
nF_U54(tt,V1,V2) -> nF_U55(isNeList(activate(V1)),activate(V2))

-> New dependency pairs: 
nF_U24(tt,V1,V2) -> nF_U25(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U44(tt,V1,V2) -> nF_U45(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U54(tt,V1,V2) -> nF_U55(U31(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))

-> Proof of termination for PALINDROME_complete_noand_FR_1_1:
-> -> Dependency pairs in cycle:
nF_U71(tt,I,P) -> nF_U72(isPalListKind(activate(I)),activate(P))
nF_isNePal(n____(I,n____(P,I))) -> nF_U71(isQid(activate(I)),activate(I),activate(P))
nF_U82(tt,V) -> nF_isNePal(activate(V))
nF_U81(tt,V) -> nF_U82(isPalListKind(activate(V)),activate(V))
nF_isPal(V) -> nF_U81(isPalListKind(activate(V)),activate(V))
nF_U72(tt,P) -> nF_isPal(activate(P))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U91(tt,V2) -> U92(isPalListKind(activate(V2)))
U92(tt) -> 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
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 0
[U11](X1,X2) = 0
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = 0
[activate](X) = X
[U13](X) = 0
[isNeList](X) = 0
[U21](X1,X2,X3) = 0
[U22](X1,X2,X3) = 0
[U23](X1,X2,X3) = 0
[U24](X1,X2,X3) = 0
[U25](X1,X2) = 0
[isList](X) = 0
[U26](X) = 0
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[isQid](X) = X
[U41](X1,X2,X3) = 0
[U42](X1,X2,X3) = 0
[U43](X1,X2,X3) = 0
[U44](X1,X2,X3) = 0
[U45](X1,X2) = 0
[U46](X) = 0
[U51](X1,X2,X3) = 0
[U52](X1,X2,X3) = 0
[U53](X1,X2,X3) = 0
[U54](X1,X2,X3) = 0
[U55](X1,X2) = 0
[U56](X) = 0
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = 0
[U92](X) = 0
[n__nil] = 0
[n____](X1,X2) = X1 + X2 + 1
[n__a] = 1
[n__e] = 1
[n__i] = 1
[n__o] = 1
[n__u] = 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U71](X1,X2,X3) = X3 + 1
[nF_isNePal](X) = X
[nF_U82](X1,X2) = X2
[nF_U81](X1,X2) = X2
[nF_isPal](X) = X
[nF_U72](X1,X2) = X2 + 1

TIME: 7.3086e-2


-> Proof of termination for PALINDROME_complete_noand_FR_1_2:
-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_U12(isPalListKind(activate(V)),activate(V))
nF_isList(V) -> nF_U11(isPalListKind(activate(V)),activate(V))
nF_U55(tt,V2) -> nF_isList(activate(V2))
nF_U54(tt,V1,V2) -> nF_U55(U31(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U53(tt,V1,V2) -> nF_U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U52(tt,V1,V2) -> nF_U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U51(tt,V1,V2) -> nF_U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U54(tt,V1,V2) -> nF_isNeList(activate(V1))
nF_U45(tt,V2) -> nF_isNeList(activate(V2))
nF_U44(tt,V1,V2) -> nF_U45(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U43(tt,V1,V2) -> nF_U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U42(tt,V1,V2) -> nF_U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U41(tt,V1,V2) -> nF_U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U12(tt,V) -> nF_isNeList(activate(V))
nF_U44(tt,V1,V2) -> nF_isList(activate(V1))
nF_U25(tt,V2) -> nF_isList(activate(V2))
nF_U24(tt,V1,V2) -> nF_U25(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U23(tt,V1,V2) -> nF_U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U22(tt,V1,V2) -> nF_U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U21(tt,V1,V2) -> nF_U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isList(n____(V1,V2)) -> nF_U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U24(tt,V1,V2) -> nF_isList(activate(V1))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
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
U91(tt,V2) -> U92(isPalListKind(activate(V2)))
U92(tt) -> tt
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))
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
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 0
[U11](X1,X2) = X1
[tt] = 1
[U12](X1,X2) = X1
[isPalListKind](X) = 1
[activate](X) = X
[U13](X) = 1
[isNeList](X) = X + 1
[U21](X1,X2,X3) = X1
[U22](X1,X2,X3) = 1
[U23](X1,X2,X3) = 1
[U24](X1,X2,X3) = X1
[U25](X1,X2) = X1
[isList](X) = 1
[U26](X) = 1
[U31](X1,X2) = 1
[U32](X1,X2) = X1
[U33](X) = 1
[isQid](X) = 1
[U41](X1,X2,X3) = 1
[U42](X1,X2,X3) = X1
[U43](X1,X2,X3) = X1
[U44](X1,X2,X3) = X1
[U45](X1,X2) = X1
[U46](X) = 1
[U51](X1,X2,X3) = X2 + 1
[U52](X1,X2,X3) = X1 + X2
[U53](X1,X2,X3) = X1 + X2
[U54](X1,X2,X3) = X1 + X2
[U55](X1,X2) = X1
[U56](X) = 1
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = X1
[U92](X) = 1
[n__nil] = 0
[n____](X1,X2) = X1 + X2 + 1
[n__a] = 0
[n__e] = 1
[n__i] = 0
[n__o] = 1
[n__u] = 0
[a] = 0
[e] = 1
[i] = 0
[o] = 1
[u] = 0
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U55](X1,X2) = X1 + X2
[nF_U54](X1,X2,X3) = X2 + X3 + 1
[nF_U53](X1,X2,X3) = X1 + X2 + X3
[nF_U52](X1,X2,X3) = X2 + X3 + 1
[nF_U51](X1,X2,X3) = X1 + X2 + X3
[nF_isNeList](X) = X
[nF_U45](X1,X2) = X1 + X2
[nF_U44](X1,X2,X3) = X2 + X3 + 1
[nF_U43](X1,X2,X3) = X1 + X2 + X3
[nF_U42](X1,X2,X3) = X2 + X3 + 1
[nF_U41](X1,X2,X3) = X1 + X2 + X3
[nF_U12](X1,X2) = X2
[nF_U25](X1,X2) = X1 + X2
[nF_U24](X1,X2,X3) = X2 + X3 + 1
[nF_U23](X1,X2,X3) = X2 + X3 + 1
[nF_U22](X1,X2,X3) = X1 + X2 + X3
[nF_U21](X1,X2,X3) = X1 + X2 + X3

TIME: 0.35685

-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_U12(isPalListKind(activate(V)),activate(V))
nF_isList(V) -> nF_U11(isPalListKind(activate(V)),activate(V))
nF_U25(tt,V2) -> nF_isList(activate(V2))
nF_U24(tt,V1,V2) -> nF_U25(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U23(tt,V1,V2) -> nF_U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U22(tt,V1,V2) -> nF_U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U21(tt,V1,V2) -> nF_U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isList(n____(V1,V2)) -> nF_U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U44(tt,V1,V2) -> nF_isList(activate(V1))
nF_U43(tt,V1,V2) -> nF_U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U42(tt,V1,V2) -> nF_U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U41(tt,V1,V2) -> nF_U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U12(tt,V) -> nF_isNeList(activate(V))
nF_U45(tt,V2) -> nF_isNeList(activate(V2))
nF_U44(tt,V1,V2) -> nF_U45(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U54(tt,V1,V2) -> nF_isNeList(activate(V1))
nF_U53(tt,V1,V2) -> nF_U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U52(tt,V1,V2) -> nF_U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U51(tt,V1,V2) -> nF_U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U55(tt,V2) -> nF_isList(activate(V2))
nF_U54(tt,V1,V2) -> nF_U55(U31(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
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
U91(tt,V2) -> U92(isPalListKind(activate(V2)))
U92(tt) -> tt
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))
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
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 0
[U11](X1,X2) = 1
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = 0
[activate](X) = X
[U13](X) = 0
[isNeList](X) = X + 1
[U21](X1,X2,X3) = 0
[U22](X1,X2,X3) = 0
[U23](X1,X2,X3) = 0
[U24](X1,X2,X3) = 0
[U25](X1,X2) = 0
[isList](X) = X + 1
[U26](X) = 0
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[isQid](X) = 0
[U41](X1,X2,X3) = X2 + 1
[U42](X1,X2,X3) = X2 + 1
[U43](X1,X2,X3) = X2 + 1
[U44](X1,X2,X3) = X2 + 1
[U45](X1,X2) = X1
[U46](X) = 0
[U51](X1,X2,X3) = X2 + 1
[U52](X1,X2,X3) = X2 + 1
[U53](X1,X2,X3) = X2 + 1
[U54](X1,X2,X3) = X2 + 1
[U55](X1,X2) = X1
[U56](X) = 0
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = 0
[U92](X) = 0
[n__nil] = 0
[n____](X1,X2) = X1 + X2 + 1
[n__a] = 1
[n__e] = 1
[n__i] = 0
[n__o] = 1
[n__u] = 1
[a] = 1
[e] = 1
[i] = 0
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U25](X1,X2) = X1 + X2
[nF_U24](X1,X2,X3) = X3 + 1
[nF_U23](X1,X2,X3) = X3 + 1
[nF_U22](X1,X2,X3) = X3 + 1
[nF_U21](X1,X2,X3) = X3 + 1
[nF_U44](X1,X2,X3) = X2 + X3
[nF_U43](X1,X2,X3) = X2 + X3
[nF_U42](X1,X2,X3) = X2 + X3
[nF_U41](X1,X2,X3) = X2 + X3
[nF_isNeList](X) = X
[nF_U12](X1,X2) = X2
[nF_U45](X1,X2) = X2
[nF_U54](X1,X2,X3) = X2 + X3 + 1
[nF_U53](X1,X2,X3) = X2 + X3 + 1
[nF_U52](X1,X2,X3) = X2 + X3 + 1
[nF_U51](X1,X2,X3) = X2 + X3 + 1
[nF_U55](X1,X2) = X2

TIME: 0.478238

-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_U12(isPalListKind(activate(V)),activate(V))
nF_isList(V) -> nF_U11(isPalListKind(activate(V)),activate(V))
nF_U44(tt,V1,V2) -> nF_isList(activate(V1))
nF_U43(tt,V1,V2) -> nF_U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U42(tt,V1,V2) -> nF_U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U41(tt,V1,V2) -> nF_U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U54(tt,V1,V2) -> nF_isNeList(activate(V1))
nF_U53(tt,V1,V2) -> nF_U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U52(tt,V1,V2) -> nF_U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U51(tt,V1,V2) -> nF_U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U45(tt,V2) -> nF_isNeList(activate(V2))
nF_U44(tt,V1,V2) -> nF_U45(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U12(tt,V) -> nF_isNeList(activate(V))
nF_U25(tt,V2) -> nF_isList(activate(V2))
nF_U24(tt,V1,V2) -> nF_U25(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U23(tt,V1,V2) -> nF_U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U22(tt,V1,V2) -> nF_U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U21(tt,V1,V2) -> nF_U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isList(n____(V1,V2)) -> nF_U21(isPalListKind(activate(V1)),activate(V1),activate(V2))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
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
U91(tt,V2) -> U92(isPalListKind(activate(V2)))
U92(tt) -> tt
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))
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
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = 0
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = 0
[activate](X) = X
[U13](X) = 0
[isNeList](X) = 0
[U21](X1,X2,X3) = 0
[U22](X1,X2,X3) = 0
[U23](X1,X2,X3) = 0
[U24](X1,X2,X3) = 0
[U25](X1,X2) = 0
[isList](X) = X
[U26](X) = 0
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[isQid](X) = X
[U41](X1,X2,X3) = 0
[U42](X1,X2,X3) = 0
[U43](X1,X2,X3) = 0
[U44](X1,X2,X3) = 0
[U45](X1,X2) = 0
[U46](X) = 0
[U51](X1,X2,X3) = 0
[U52](X1,X2,X3) = 0
[U53](X1,X2,X3) = 0
[U54](X1,X2,X3) = 0
[U55](X1,X2) = 0
[U56](X) = 0
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = 0
[U92](X) = 0
[n__nil] = 1
[n____](X1,X2) = X1 + X2 + 1
[n__a] = 1
[n__e] = 1
[n__i] = 1
[n__o] = 1
[n__u] = 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U44](X1,X2,X3) = X2 + X3
[nF_U43](X1,X2,X3) = X2 + X3
[nF_U42](X1,X2,X3) = X2 + X3
[nF_U41](X1,X2,X3) = X2 + X3
[nF_isNeList](X) = X
[nF_U54](X1,X2,X3) = X2
[nF_U53](X1,X2,X3) = X2
[nF_U52](X1,X2,X3) = X2
[nF_U51](X1,X2,X3) = X2
[nF_U45](X1,X2) = X2
[nF_U12](X1,X2) = X2
[nF_U25](X1,X2) = X2
[nF_U24](X1,X2,X3) = X3
[nF_U23](X1,X2,X3) = X3
[nF_U22](X1,X2,X3) = X3
[nF_U21](X1,X2,X3) = X3

TIME: 0.256486

-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_U12(isPalListKind(activate(V)),activate(V))
nF_isList(V) -> nF_U11(isPalListKind(activate(V)),activate(V))
nF_U44(tt,V1,V2) -> nF_isList(activate(V1))
nF_U43(tt,V1,V2) -> nF_U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U42(tt,V1,V2) -> nF_U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U41(tt,V1,V2) -> nF_U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U12(tt,V) -> nF_isNeList(activate(V))
nF_U45(tt,V2) -> nF_isNeList(activate(V2))
nF_U44(tt,V1,V2) -> nF_U45(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U54(tt,V1,V2) -> nF_isNeList(activate(V1))
nF_U53(tt,V1,V2) -> nF_U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U52(tt,V1,V2) -> nF_U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U51(tt,V1,V2) -> nF_U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U51(isPalListKind(activate(V1)),activate(V1),activate(V2))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
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
U91(tt,V2) -> U92(isPalListKind(activate(V2)))
U92(tt) -> tt
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))
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
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = X1 + 1
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = X
[activate](X) = X
[U13](X) = 0
[isNeList](X) = 0
[U21](X1,X2,X3) = 0
[U22](X1,X2,X3) = 0
[U23](X1,X2,X3) = 0
[U24](X1,X2,X3) = 0
[U25](X1,X2) = 0
[isList](X) = X + 1
[U26](X) = 0
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[isQid](X) = X
[U41](X1,X2,X3) = 0
[U42](X1,X2,X3) = 0
[U43](X1,X2,X3) = 0
[U44](X1,X2,X3) = 0
[U45](X1,X2) = 0
[U46](X) = 0
[U51](X1,X2,X3) = 0
[U52](X1,X2,X3) = 0
[U53](X1,X2,X3) = 0
[U54](X1,X2,X3) = 0
[U55](X1,X2) = 0
[U56](X) = 0
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = 0
[U92](X) = 0
[n__nil] = 1
[n____](X1,X2) = X1 + X2 + 1
[n__a] = 1
[n__e] = 1
[n__i] = 1
[n__o] = 1
[n__u] = 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U44](X1,X2,X3) = X2 + X3 + 1
[nF_U43](X1,X2,X3) = X2 + X3 + 1
[nF_U42](X1,X2,X3) = X2 + X3 + 1
[nF_U41](X1,X2,X3) = X2 + X3 + 1
[nF_isNeList](X) = X
[nF_U12](X1,X2) = X2
[nF_U45](X1,X2) = X1 + X2
[nF_U54](X1,X2,X3) = X2
[nF_U53](X1,X2,X3) = X2
[nF_U52](X1,X2,X3) = X2
[nF_U51](X1,X2,X3) = X2

TIME: 0.24506700000000003

-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_U12(isPalListKind(activate(V)),activate(V))
nF_isList(V) -> nF_U11(isPalListKind(activate(V)),activate(V))
nF_U44(tt,V1,V2) -> nF_isList(activate(V1))
nF_U43(tt,V1,V2) -> nF_U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U42(tt,V1,V2) -> nF_U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U41(tt,V1,V2) -> nF_U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U45(tt,V2) -> nF_isNeList(activate(V2))
nF_U44(tt,V1,V2) -> nF_U45(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))
nF_U12(tt,V) -> nF_isNeList(activate(V))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
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
U91(tt,V2) -> U92(isPalListKind(activate(V2)))
U92(tt) -> tt
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))
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
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = X1 + 1
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = X
[activate](X) = X
[U13](X) = 0
[isNeList](X) = X + 1
[U21](X1,X2,X3) = X2 + 1
[U22](X1,X2,X3) = X2 + 1
[U23](X1,X2,X3) = X2 + 1
[U24](X1,X2,X3) = X2 + 1
[U25](X1,X2) = X1
[isList](X) = X + 1
[U26](X) = 0
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[isQid](X) = 0
[U41](X1,X2,X3) = X2 + 1
[U42](X1,X2,X3) = X2 + 1
[U43](X1,X2,X3) = X2 + 1
[U44](X1,X2,X3) = X2 + 1
[U45](X1,X2) = X1
[U46](X) = 0
[U51](X1,X2,X3) = X2 + 1
[U52](X1,X2,X3) = X2 + 1
[U53](X1,X2,X3) = X2 + 1
[U54](X1,X2,X3) = X2 + 1
[U55](X1,X2) = X1
[U56](X) = 0
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = 0
[U92](X) = 0
[n__nil] = 1
[n____](X1,X2) = X1 + X2 + 1
[n__a] = 1
[n__e] = 1
[n__i] = 1
[n__o] = 1
[n__u] = 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X2 + 1
[nF_isList](X) = X + 1
[nF_U44](X1,X2,X3) = X2 + X3 + 1
[nF_U43](X1,X2,X3) = X2 + X3 + 1
[nF_U42](X1,X2,X3) = X2 + X3 + 1
[nF_U41](X1,X2,X3) = X2 + X3 + 1
[nF_isNeList](X) = X
[nF_U45](X1,X2) = X1 + X2
[nF_U12](X1,X2) = X2 + 1

TIME: 0.220847

-> -> Dependency pairs in cycle:
nF_U43(tt,V1,V2) -> nF_U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U42(tt,V1,V2) -> nF_U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
nF_U41(tt,V1,V2) -> nF_U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_isNeList(n____(V1,V2)) -> nF_U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
nF_U45(tt,V2) -> nF_isNeList(activate(V2))
nF_U44(tt,V1,V2) -> nF_U45(U11(isPalListKind(activate(activate(V1))),activate(activate(V1))),activate(V2))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
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
U91(tt,V2) -> U92(isPalListKind(activate(V2)))
U92(tt) -> tt
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))
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
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2
[nil] = 1
[U11](X1,X2) = X2
[tt] = 1
[U12](X1,X2) = X2
[isPalListKind](X) = X
[activate](X) = X
[U13](X) = X
[isNeList](X) = X
[U21](X1,X2,X3) = X3
[U22](X1,X2,X3) = X3
[U23](X1,X2,X3) = X1
[U24](X1,X2,X3) = 1
[U25](X1,X2) = 1
[isList](X) = X
[U26](X) = 1
[U31](X1,X2) = X2
[U32](X1,X2) = X1
[U33](X) = X
[isQid](X) = 1
[U41](X1,X2,X3) = X1 + X3
[U42](X1,X2,X3) = X3
[U43](X1,X2,X3) = X3
[U44](X1,X2,X3) = X3
[U45](X1,X2) = X2
[U46](X) = X
[U51](X1,X2,X3) = X1 + X3
[U52](X1,X2,X3) = X3
[U53](X1,X2,X3) = X3
[U54](X1,X2,X3) = X3
[U55](X1,X2) = X2
[U56](X) = X
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = X1 + X2
[U92](X) = X
[n__nil] = 1
[n____](X1,X2) = X1 + X2
[n__a] = 1
[n__e] = 1
[n__i] = 1
[n__o] = 1
[n__u] = 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U43](X1,X2,X3) = X3 + 1
[nF_U42](X1,X2,X3) = X1 + X3
[nF_U41](X1,X2,X3) = X2 + X3
[nF_isNeList](X) = X
[nF_U45](X1,X2) = X2
[nF_U44](X1,X2,X3) = X3 + 1

TIME: 0.33785


-> Proof of termination for PALINDROME_complete_noand_FR_1_3:
-> -> Dependency pairs in cycle:
nF_isPalListKind(n____(V1,V2)) -> nF_isPalListKind(activate(V1))
nF_U91(tt,V2) -> nF_isPalListKind(activate(V2))
nF_isPalListKind(n____(V1,V2)) -> nF_U91(isPalListKind(activate(V1)),activate(V2))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U91(tt,V2) -> U92(isPalListKind(activate(V2)))
U92(tt) -> 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))
nil -> n__nil
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = 0
[tt] = 1
[U12](X1,X2) = 0
[isPalListKind](X) = X
[activate](X) = X
[U13](X) = 0
[isNeList](X) = 0
[U21](X1,X2,X3) = 0
[U22](X1,X2,X3) = 0
[U23](X1,X2,X3) = 0
[U24](X1,X2,X3) = 0
[U25](X1,X2) = 0
[isList](X) = 0
[U26](X) = 0
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[isQid](X) = 0
[U41](X1,X2,X3) = 0
[U42](X1,X2,X3) = 0
[U43](X1,X2,X3) = 0
[U44](X1,X2,X3) = 0
[U45](X1,X2) = 0
[U46](X) = 0
[U51](X1,X2,X3) = 0
[U52](X1,X2,X3) = 0
[U53](X1,X2,X3) = 0
[U54](X1,X2,X3) = 0
[U55](X1,X2) = 0
[U56](X) = 0
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = X1 + X2
[U92](X) = X
[n__nil] = 1
[n____](X1,X2) = X1 + X2 + 1
[n__a] = 1
[n__e] = 1
[n__i] = 1
[n__o] = 1
[n__u] = 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_isPalListKind](X) = X
[nF_U91](X1,X2) = X2

TIME: 0.205083

-> -> Dependency pairs in cycle:
nF_isPalListKind(n____(V1,V2)) -> nF_isPalListKind(activate(V1))

UsableRules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
nil -> n__nil
__(X1,X2) -> n____(X1,X2)
a -> n__a
e -> n__e
i -> n__i
o -> n__o
u -> n__u
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

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = 0
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = 0
[activate](X) = X
[U13](X) = 0
[isNeList](X) = 0
[U21](X1,X2,X3) = 0
[U22](X1,X2,X3) = 0
[U23](X1,X2,X3) = 0
[U24](X1,X2,X3) = 0
[U25](X1,X2) = 0
[isList](X) = 0
[U26](X) = 0
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[isQid](X) = 0
[U41](X1,X2,X3) = 0
[U42](X1,X2,X3) = 0
[U43](X1,X2,X3) = 0
[U44](X1,X2,X3) = 0
[U45](X1,X2) = 0
[U46](X) = 0
[U51](X1,X2,X3) = 0
[U52](X1,X2,X3) = 0
[U53](X1,X2,X3) = 0
[U54](X1,X2,X3) = 0
[U55](X1,X2) = 0
[U56](X) = 0
[U61](X1,X2) = 0
[U62](X1,X2) = 0
[U63](X) = 0
[U71](X1,X2,X3) = 0
[U72](X1,X2) = 0
[U73](X1,X2) = 0
[isPal](X) = 0
[U74](X) = 0
[U81](X1,X2) = 0
[U82](X1,X2) = 0
[U83](X) = 0
[isNePal](X) = 0
[U91](X1,X2) = 0
[U92](X) = 0
[n__nil] = 1
[n____](X1,X2) = X1 + X2 + 1
[n__a] = 1
[n__e] = 1
[n__i] = 1
[n__o] = 1
[n__u] = 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_isPalListKind](X) = X

TIME: 0.19748900000000003


-> Proof of termination for PALINDROME_complete_noand_FR_1_4:
-> -> Dependency pairs in cycle:
nF_activate(n____(X1,X2)) -> nF_activate(X2)
nF_activate(n____(X1,X2)) -> nF_activate(X1)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_complete_noand_FR_1_5:
-> -> Dependency pairs in cycle:
nF___(__(X,Y),Z) -> nF___(X,__(Y,Z))
nF___(__(X,Y),Z) -> nF___(Y,Z)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.