(VAR X Y Z V V1 V2 I P)
(STRATEGY CONTEXTSENSITIVE 
  (__ 1 2)
  (nil)
  (U11 1)
  (tt)
  (U12 1)
  (isPalListKind)
  (U13 1)
  (isNeList)
  (U21 1)
  (U22 1)
  (U23 1)
  (U24 1)
  (U25 1)
  (isList)
  (U26 1)
  (U31 1)
  (U32 1)
  (U33 1)
  (isQid)
  (U41 1)
  (U42 1)
  (U43 1)
  (U44 1)
  (U45 1)
  (U46 1)
  (U51 1)
  (U52 1)
  (U53 1)
  (U54 1)
  (U55 1)
  (U56 1)
  (U61 1)
  (U62 1)
  (U63 1)
  (U71 1)
  (U72 1)
  (U73 1)
  (isPal)
  (U74 1)
  (U81 1)
  (U82 1)
  (U83 1)
  (isNePal)
  (U91 1)
  (U92 1)
  (a)
  (e)
  (i)
  (o)
  (u)
)
(RULES 
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U11(tt,V) -> U12(isPalListKind(V),V)
U12(tt,V) -> U13(isNeList(V))
U13(tt) -> tt
U21(tt,V1,V2) -> U22(isPalListKind(V1),V1,V2)
U22(tt,V1,V2) -> U23(isPalListKind(V2),V1,V2)
U23(tt,V1,V2) -> U24(isPalListKind(V2),V1,V2)
U24(tt,V1,V2) -> U25(isList(V1),V2)
U25(tt,V2) -> U26(isList(V2))
U26(tt) -> tt
U31(tt,V) -> U32(isPalListKind(V),V)
U32(tt,V) -> U33(isQid(V))
U33(tt) -> tt
U41(tt,V1,V2) -> U42(isPalListKind(V1),V1,V2)
U42(tt,V1,V2) -> U43(isPalListKind(V2),V1,V2)
U43(tt,V1,V2) -> U44(isPalListKind(V2),V1,V2)
U44(tt,V1,V2) -> U45(isList(V1),V2)
U45(tt,V2) -> U46(isNeList(V2))
U46(tt) -> tt
U51(tt,V1,V2) -> U52(isPalListKind(V1),V1,V2)
U52(tt,V1,V2) -> U53(isPalListKind(V2),V1,V2)
U53(tt,V1,V2) -> U54(isPalListKind(V2),V1,V2)
U54(tt,V1,V2) -> U55(isNeList(V1),V2)
U55(tt,V2) -> U56(isList(V2))
U56(tt) -> tt
U61(tt,V) -> U62(isPalListKind(V),V)
U62(tt,V) -> U63(isQid(V))
U63(tt) -> tt
U71(tt,I,P) -> U72(isPalListKind(I),P)
U72(tt,P) -> U73(isPal(P),P)
U73(tt,P) -> U74(isPalListKind(P))
U74(tt) -> tt
U81(tt,V) -> U82(isPalListKind(V),V)
U82(tt,V) -> U83(isNePal(V))
U83(tt) -> tt
U91(tt,V2) -> U92(isPalListKind(V2))
U92(tt) -> tt
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(isPalListKind(V1),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(isPalListKind(V1),V1,V2)
isNeList(__(V1,V2)) -> U51(isPalListKind(V1),V1,V2)
isNePal(V) -> U61(isPalListKind(V),V)
isNePal(__(I,__(P,I))) -> U71(isQid(I),I,P)
isPal(V) -> U81(isPalListKind(V),V)
isPal(nil) -> tt
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind(__(V1,V2)) -> U91(isPalListKind(V1),V2)
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt
)

Proving termination of context-sensitive rewriting for PALINDROME_complete_noand:

-> Dependency pairs:
nF___(__(X,Y),Z) -> nF___(X,__(Y,Z))
nF___(__(X,Y),Z) -> nF___(Y,Z)
nF_U11(tt,V) -> nF_U12(isPalListKind(V),V)
nF_U11(tt,V) -> nF_isPalListKind(V)
nF_U12(tt,V) -> nF_U13(isNeList(V))
nF_U12(tt,V) -> nF_isNeList(V)
nF_U21(tt,V1,V2) -> nF_U22(isPalListKind(V1),V1,V2)
nF_U21(tt,V1,V2) -> nF_isPalListKind(V1)
nF_U22(tt,V1,V2) -> nF_U23(isPalListKind(V2),V1,V2)
nF_U22(tt,V1,V2) -> nF_isPalListKind(V2)
nF_U23(tt,V1,V2) -> nF_U24(isPalListKind(V2),V1,V2)
nF_U23(tt,V1,V2) -> nF_isPalListKind(V2)
nF_U24(tt,V1,V2) -> nF_U25(isList(V1),V2)
nF_U24(tt,V1,V2) -> nF_isList(V1)
nF_U25(tt,V2) -> nF_U26(isList(V2))
nF_U25(tt,V2) -> nF_isList(V2)
nF_U31(tt,V) -> nF_U32(isPalListKind(V),V)
nF_U31(tt,V) -> nF_isPalListKind(V)
nF_U32(tt,V) -> nF_U33(isQid(V))
nF_U32(tt,V) -> nF_isQid(V)
nF_U41(tt,V1,V2) -> nF_U42(isPalListKind(V1),V1,V2)
nF_U41(tt,V1,V2) -> nF_isPalListKind(V1)
nF_U42(tt,V1,V2) -> nF_U43(isPalListKind(V2),V1,V2)
nF_U42(tt,V1,V2) -> nF_isPalListKind(V2)
nF_U43(tt,V1,V2) -> nF_U44(isPalListKind(V2),V1,V2)
nF_U43(tt,V1,V2) -> nF_isPalListKind(V2)
nF_U44(tt,V1,V2) -> nF_U45(isList(V1),V2)
nF_U44(tt,V1,V2) -> nF_isList(V1)
nF_U45(tt,V2) -> nF_U46(isNeList(V2))
nF_U45(tt,V2) -> nF_isNeList(V2)
nF_U51(tt,V1,V2) -> nF_U52(isPalListKind(V1),V1,V2)
nF_U51(tt,V1,V2) -> nF_isPalListKind(V1)
nF_U52(tt,V1,V2) -> nF_U53(isPalListKind(V2),V1,V2)
nF_U52(tt,V1,V2) -> nF_isPalListKind(V2)
nF_U53(tt,V1,V2) -> nF_U54(isPalListKind(V2),V1,V2)
nF_U53(tt,V1,V2) -> nF_isPalListKind(V2)
nF_U54(tt,V1,V2) -> nF_U55(isNeList(V1),V2)
nF_U54(tt,V1,V2) -> nF_isNeList(V1)
nF_U55(tt,V2) -> nF_U56(isList(V2))
nF_U55(tt,V2) -> nF_isList(V2)
nF_U61(tt,V) -> nF_U62(isPalListKind(V),V)
nF_U61(tt,V) -> nF_isPalListKind(V)
nF_U62(tt,V) -> nF_U63(isQid(V))
nF_U62(tt,V) -> nF_isQid(V)
nF_U71(tt,I,P) -> nF_U72(isPalListKind(I),P)
nF_U71(tt,I,P) -> nF_isPalListKind(I)
nF_U72(tt,P) -> nF_U73(isPal(P),P)
nF_U72(tt,P) -> nF_isPal(P)
nF_U73(tt,P) -> nF_U74(isPalListKind(P))
nF_U73(tt,P) -> nF_isPalListKind(P)
nF_U81(tt,V) -> nF_U82(isPalListKind(V),V)
nF_U81(tt,V) -> nF_isPalListKind(V)
nF_U82(tt,V) -> nF_U83(isNePal(V))
nF_U82(tt,V) -> nF_isNePal(V)
nF_U91(tt,V2) -> nF_U92(isPalListKind(V2))
nF_U91(tt,V2) -> nF_isPalListKind(V2)
nF_isList(V) -> nF_U11(isPalListKind(V),V)
nF_isList(V) -> nF_isPalListKind(V)
nF_isList(__(V1,V2)) -> nF_U21(isPalListKind(V1),V1,V2)
nF_isList(__(V1,V2)) -> nF_isPalListKind(V1)
nF_isNeList(V) -> nF_U31(isPalListKind(V),V)
nF_isNeList(V) -> nF_isPalListKind(V)
nF_isNeList(__(V1,V2)) -> nF_U41(isPalListKind(V1),V1,V2)
nF_isNeList(__(V1,V2)) -> nF_isPalListKind(V1)
nF_isNeList(__(V1,V2)) -> nF_U51(isPalListKind(V1),V1,V2)
nF_isNePal(V) -> nF_U61(isPalListKind(V),V)
nF_isNePal(V) -> nF_isPalListKind(V)
nF_isNePal(__(I,__(P,I))) -> nF_U71(isQid(I),I,P)
nF_isNePal(__(I,__(P,I))) -> nF_isQid(I)
nF_isPal(V) -> nF_U81(isPalListKind(V),V)
nF_isPal(V) -> nF_isPalListKind(V)
nF_isPalListKind(__(V1,V2)) -> nF_U91(isPalListKind(V1),V2)
nF_isPalListKind(__(V1,V2)) -> nF_isPalListKind(V1)

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

Termination proved: Cycles verify subterm criterion.

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

Usable Rules:
U11(tt,V) -> U12(isPalListKind(V),V)
U12(tt,V) -> U13(isNeList(V))
U13(tt) -> tt
U21(tt,V1,V2) -> U22(isPalListKind(V1),V1,V2)
U22(tt,V1,V2) -> U23(isPalListKind(V2),V1,V2)
U23(tt,V1,V2) -> U24(isPalListKind(V2),V1,V2)
U24(tt,V1,V2) -> U25(isList(V1),V2)
U25(tt,V2) -> U26(isList(V2))
U26(tt) -> tt
U31(tt,V) -> U32(isPalListKind(V),V)
U32(tt,V) -> U33(isQid(V))
U33(tt) -> tt
U41(tt,V1,V2) -> U42(isPalListKind(V1),V1,V2)
U42(tt,V1,V2) -> U43(isPalListKind(V2),V1,V2)
U43(tt,V1,V2) -> U44(isPalListKind(V2),V1,V2)
U44(tt,V1,V2) -> U45(isList(V1),V2)
U45(tt,V2) -> U46(isNeList(V2))
U46(tt) -> tt
U51(tt,V1,V2) -> U52(isPalListKind(V1),V1,V2)
U52(tt,V1,V2) -> U53(isPalListKind(V2),V1,V2)
U53(tt,V1,V2) -> U54(isPalListKind(V2),V1,V2)
U54(tt,V1,V2) -> U55(isNeList(V1),V2)
U55(tt,V2) -> U56(isList(V2))
U56(tt) -> tt
U91(tt,V2) -> U92(isPalListKind(V2))
U92(tt) -> tt
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(isPalListKind(V1),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(isPalListKind(V1),V1,V2)
isNeList(__(V1,V2)) -> U51(isPalListKind(V1),V1,V2)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind(__(V1,V2)) -> U91(isPalListKind(V1),V2)
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = 0
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = X
[U13](X) = 0
[isNeList](X) = X
[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) = 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
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U55](X1,X2) = X2
[nF_U54](X1,X2,X3) = X2 + X3
[nF_U53](X1,X2,X3) = X2 + X3
[nF_U52](X1,X2,X3) = X2 + X3
[nF_U51](X1,X2,X3) = X2 + X3
[nF_isNeList](X) = X
[nF_U45](X1,X2) = X2
[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_U12](X1,X2) = X2
[nF_U25](X1,X2) = X2
[nF_U24](X1,X2,X3) = X2 + X3 + 1
[nF_U23](X1,X2,X3) = X2 + X3 + 1
[nF_U22](X1,X2,X3) = X2 + X3 + 1
[nF_U21](X1,X2,X3) = X2 + X3 + 1

TIME: 0.187672

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

Usable Rules:
U11(tt,V) -> U12(isPalListKind(V),V)
U12(tt,V) -> U13(isNeList(V))
U13(tt) -> tt
U21(tt,V1,V2) -> U22(isPalListKind(V1),V1,V2)
U22(tt,V1,V2) -> U23(isPalListKind(V2),V1,V2)
U23(tt,V1,V2) -> U24(isPalListKind(V2),V1,V2)
U24(tt,V1,V2) -> U25(isList(V1),V2)
U25(tt,V2) -> U26(isList(V2))
U26(tt) -> tt
U31(tt,V) -> U32(isPalListKind(V),V)
U32(tt,V) -> U33(isQid(V))
U33(tt) -> tt
U41(tt,V1,V2) -> U42(isPalListKind(V1),V1,V2)
U42(tt,V1,V2) -> U43(isPalListKind(V2),V1,V2)
U43(tt,V1,V2) -> U44(isPalListKind(V2),V1,V2)
U44(tt,V1,V2) -> U45(isList(V1),V2)
U45(tt,V2) -> U46(isNeList(V2))
U46(tt) -> tt
U51(tt,V1,V2) -> U52(isPalListKind(V1),V1,V2)
U52(tt,V1,V2) -> U53(isPalListKind(V2),V1,V2)
U53(tt,V1,V2) -> U54(isPalListKind(V2),V1,V2)
U54(tt,V1,V2) -> U55(isNeList(V1),V2)
U55(tt,V2) -> U56(isList(V2))
U56(tt) -> tt
U91(tt,V2) -> U92(isPalListKind(V2))
U92(tt) -> tt
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(isPalListKind(V1),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(isPalListKind(V1),V1,V2)
isNeList(__(V1,V2)) -> U51(isPalListKind(V1),V1,V2)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind(__(V1,V2)) -> U91(isPalListKind(V1),V2)
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 0
[U11](X1,X2) = 1
[tt] = 0
[U12](X1,X2) = 1
[isPalListKind](X) = 0
[U13](X) = X
[isNeList](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) = 1
[U32](X1,X2) = 1
[U33](X) = X
[isQid](X) = 1
[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) = 1
[U52](X1,X2,X3) = 1
[U53](X1,X2,X3) = 1
[U54](X1,X2,X3) = 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
[a] = 0
[e] = 0
[i] = 0
[o] = 0
[u] = 0
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[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
[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.16486

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

Usable Rules:
U11(tt,V) -> U12(isPalListKind(V),V)
U12(tt,V) -> U13(isNeList(V))
U13(tt) -> tt
U21(tt,V1,V2) -> U22(isPalListKind(V1),V1,V2)
U22(tt,V1,V2) -> U23(isPalListKind(V2),V1,V2)
U23(tt,V1,V2) -> U24(isPalListKind(V2),V1,V2)
U24(tt,V1,V2) -> U25(isList(V1),V2)
U25(tt,V2) -> U26(isList(V2))
U26(tt) -> tt
U31(tt,V) -> U32(isPalListKind(V),V)
U32(tt,V) -> U33(isQid(V))
U33(tt) -> tt
U41(tt,V1,V2) -> U42(isPalListKind(V1),V1,V2)
U42(tt,V1,V2) -> U43(isPalListKind(V2),V1,V2)
U43(tt,V1,V2) -> U44(isPalListKind(V2),V1,V2)
U44(tt,V1,V2) -> U45(isList(V1),V2)
U45(tt,V2) -> U46(isNeList(V2))
U46(tt) -> tt
U51(tt,V1,V2) -> U52(isPalListKind(V1),V1,V2)
U52(tt,V1,V2) -> U53(isPalListKind(V2),V1,V2)
U53(tt,V1,V2) -> U54(isPalListKind(V2),V1,V2)
U54(tt,V1,V2) -> U55(isNeList(V1),V2)
U55(tt,V2) -> U56(isList(V2))
U56(tt) -> tt
U91(tt,V2) -> U92(isPalListKind(V2))
U92(tt) -> tt
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(isPalListKind(V1),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(isPalListKind(V1),V1,V2)
isNeList(__(V1,V2)) -> U51(isPalListKind(V1),V1,V2)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind(__(V1,V2)) -> U91(isPalListKind(V1),V2)
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = 0
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = X
[U13](X) = 0
[isNeList](X) = X
[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) = 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
[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: 8.1341e-2

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

Usable Rules:
U11(tt,V) -> U12(isPalListKind(V),V)
U12(tt,V) -> U13(isNeList(V))
U13(tt) -> tt
U21(tt,V1,V2) -> U22(isPalListKind(V1),V1,V2)
U22(tt,V1,V2) -> U23(isPalListKind(V2),V1,V2)
U23(tt,V1,V2) -> U24(isPalListKind(V2),V1,V2)
U24(tt,V1,V2) -> U25(isList(V1),V2)
U25(tt,V2) -> U26(isList(V2))
U26(tt) -> tt
U31(tt,V) -> U32(isPalListKind(V),V)
U32(tt,V) -> U33(isQid(V))
U33(tt) -> tt
U41(tt,V1,V2) -> U42(isPalListKind(V1),V1,V2)
U42(tt,V1,V2) -> U43(isPalListKind(V2),V1,V2)
U43(tt,V1,V2) -> U44(isPalListKind(V2),V1,V2)
U44(tt,V1,V2) -> U45(isList(V1),V2)
U45(tt,V2) -> U46(isNeList(V2))
U46(tt) -> tt
U51(tt,V1,V2) -> U52(isPalListKind(V1),V1,V2)
U52(tt,V1,V2) -> U53(isPalListKind(V2),V1,V2)
U53(tt,V1,V2) -> U54(isPalListKind(V2),V1,V2)
U54(tt,V1,V2) -> U55(isNeList(V1),V2)
U55(tt,V2) -> U56(isList(V2))
U56(tt) -> tt
U91(tt,V2) -> U92(isPalListKind(V2))
U92(tt) -> tt
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(isPalListKind(V1),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(isPalListKind(V1),V1,V2)
isNeList(__(V1,V2)) -> U51(isPalListKind(V1),V1,V2)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind(__(V1,V2)) -> U91(isPalListKind(V1),V2)
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = 0
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = X
[U13](X) = 0
[isNeList](X) = X
[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) = 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
[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_U12](X1,X2) = X2
[nF_U45](X1,X2) = 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: 7.6225e-2

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

Usable Rules:
U11(tt,V) -> U12(isPalListKind(V),V)
U12(tt,V) -> U13(isNeList(V))
U13(tt) -> tt
U21(tt,V1,V2) -> U22(isPalListKind(V1),V1,V2)
U22(tt,V1,V2) -> U23(isPalListKind(V2),V1,V2)
U23(tt,V1,V2) -> U24(isPalListKind(V2),V1,V2)
U24(tt,V1,V2) -> U25(isList(V1),V2)
U25(tt,V2) -> U26(isList(V2))
U26(tt) -> tt
U31(tt,V) -> U32(isPalListKind(V),V)
U32(tt,V) -> U33(isQid(V))
U33(tt) -> tt
U41(tt,V1,V2) -> U42(isPalListKind(V1),V1,V2)
U42(tt,V1,V2) -> U43(isPalListKind(V2),V1,V2)
U43(tt,V1,V2) -> U44(isPalListKind(V2),V1,V2)
U44(tt,V1,V2) -> U45(isList(V1),V2)
U45(tt,V2) -> U46(isNeList(V2))
U46(tt) -> tt
U51(tt,V1,V2) -> U52(isPalListKind(V1),V1,V2)
U52(tt,V1,V2) -> U53(isPalListKind(V2),V1,V2)
U53(tt,V1,V2) -> U54(isPalListKind(V2),V1,V2)
U54(tt,V1,V2) -> U55(isNeList(V1),V2)
U55(tt,V2) -> U56(isList(V2))
U56(tt) -> tt
U91(tt,V2) -> U92(isPalListKind(V2))
U92(tt) -> tt
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(isPalListKind(V1),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(isPalListKind(V1),V1,V2)
isNeList(__(V1,V2)) -> U51(isPalListKind(V1),V1,V2)
isPalListKind(a) -> tt
isPalListKind(e) -> tt
isPalListKind(i) -> tt
isPalListKind(nil) -> tt
isPalListKind(o) -> tt
isPalListKind(u) -> tt
isPalListKind(__(V1,V2)) -> U91(isPalListKind(V1),V2)
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt

Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[nil] = 1
[U11](X1,X2) = 0
[tt] = 0
[U12](X1,X2) = 0
[isPalListKind](X) = X
[U13](X) = 0
[isNeList](X) = X
[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) = 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
[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) = X2
[nF_U12](X1,X2) = X2 + 1

TIME: 6.9185e-2

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

Termination proved: Cycles verify subterm criterion.

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

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_complete_noand_1_4:
-> -> 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 CSDG + 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.