(VAR X Y Z V V1 V2 I P)
(STRATEGY CONTEXTSENSITIVE 
  (__ 1 2)
  (nil)
  (U11 1)
  (tt)
  (U12 1)
  (isNeList)
  (U21 1)
  (U22 1)
  (isList)
  (U23 1)
  (U31 1)
  (U32 1)
  (isQid)
  (U41 1)
  (U42 1)
  (U43 1)
  (U51 1)
  (U52 1)
  (U53 1)
  (U61 1)
  (U62 1)
  (U71 1)
  (U72 1)
  (isNePal)
  (and 1)
  (isPalListKind)
  (isPal)
  (a)
  (e)
  (i)
  (o)
  (u)
)
(RULES 
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U11(tt,V) -> U12(isNeList(V))
U12(tt) -> tt
U21(tt,V1,V2) -> U22(isList(V1),V2)
U22(tt,V2) -> U23(isList(V2))
U23(tt) -> tt
U31(tt,V) -> U32(isQid(V))
U32(tt) -> tt
U41(tt,V1,V2) -> U42(isList(V1),V2)
U42(tt,V2) -> U43(isNeList(V2))
U43(tt) -> tt
U51(tt,V1,V2) -> U52(isNeList(V1),V2)
U52(tt,V2) -> U53(isList(V2))
U53(tt) -> tt
U61(tt,V) -> U62(isQid(V))
U62(tt) -> tt
U71(tt,V) -> U72(isNePal(V))
U72(tt) -> tt
and(tt,X) -> X
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(__(V1,V2)) -> U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNePal(V) -> U61(isPalListKind(V),V)
isNePal(__(I,__(P,I))) -> and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))
isPal(V) -> U71(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)) -> and(isPalListKind(V1),isPalListKind(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:

-> Dependency pairs:
nF___(__(X,Y),Z) -> nF___(X,__(Y,Z))
nF___(__(X,Y),Z) -> nF___(Y,Z)
nF_U11(tt,V) -> nF_U12(isNeList(V))
nF_U11(tt,V) -> nF_isNeList(V)
nF_U21(tt,V1,V2) -> nF_U22(isList(V1),V2)
nF_U21(tt,V1,V2) -> nF_isList(V1)
nF_U22(tt,V2) -> nF_U23(isList(V2))
nF_U22(tt,V2) -> nF_isList(V2)
nF_U31(tt,V) -> nF_U32(isQid(V))
nF_U31(tt,V) -> nF_isQid(V)
nF_U41(tt,V1,V2) -> nF_U42(isList(V1),V2)
nF_U41(tt,V1,V2) -> nF_isList(V1)
nF_U42(tt,V2) -> nF_U43(isNeList(V2))
nF_U42(tt,V2) -> nF_isNeList(V2)
nF_U51(tt,V1,V2) -> nF_U52(isNeList(V1),V2)
nF_U51(tt,V1,V2) -> nF_isNeList(V1)
nF_U52(tt,V2) -> nF_U53(isList(V2))
nF_U52(tt,V2) -> nF_isList(V2)
nF_U61(tt,V) -> nF_U62(isQid(V))
nF_U61(tt,V) -> nF_isQid(V)
nF_U71(tt,V) -> nF_U72(isNePal(V))
nF_U71(tt,V) -> nF_isNePal(V)
nF_and(tt,X) -> X
nF_isList(V) -> nF_U11(isPalListKind(V),V)
nF_isList(V) -> nF_isPalListKind(V)
nF_isList(__(V1,V2)) -> nF_U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_isList(__(V1,V2)) -> nF_and(isPalListKind(V1),isPalListKind(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(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_isNeList(__(V1,V2)) -> nF_and(isPalListKind(V1),isPalListKind(V2))
nF_isNeList(__(V1,V2)) -> nF_isPalListKind(V1)
nF_isNeList(__(V1,V2)) -> nF_U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_isNePal(V) -> nF_U61(isPalListKind(V),V)
nF_isNePal(V) -> nF_isPalListKind(V)
nF_isNePal(__(I,__(P,I))) -> nF_and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))
nF_isNePal(__(I,__(P,I))) -> nF_and(isQid(I),isPalListKind(I))
nF_isNePal(__(I,__(P,I))) -> nF_isQid(I)
nF_isPal(V) -> nF_U71(isPalListKind(V),V)
nF_isPal(V) -> nF_isPalListKind(V)
nF_isPalListKind(__(V1,V2)) -> nF_and(isPalListKind(V1),isPalListKind(V2))
nF_isPalListKind(__(V1,V2)) -> nF_isPalListKind(V1)

-> Proof of termination for PALINDROME_complete_1_1:
-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_isNeList(V)
nF_isList(V) -> nF_U11(isPalListKind(V),V)
nF_U52(tt,V2) -> nF_isList(V2)
nF_U51(tt,V1,V2) -> nF_U52(isNeList(V1),V2)
nF_isNeList(__(V1,V2)) -> nF_U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U51(tt,V1,V2) -> nF_isNeList(V1)
nF_U42(tt,V2) -> nF_isNeList(V2)
nF_U41(tt,V1,V2) -> nF_U42(isList(V1),V2)
nF_isNeList(__(V1,V2)) -> nF_U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U41(tt,V1,V2) -> nF_isList(V1)
nF_U22(tt,V2) -> nF_isList(V2)
nF_U21(tt,V1,V2) -> nF_U22(isList(V1),V2)
nF_isList(__(V1,V2)) -> nF_U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U21(tt,V1,V2) -> nF_isList(V1)

Usable Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U11(tt,V) -> U12(isNeList(V))
U12(tt) -> tt
U21(tt,V1,V2) -> U22(isList(V1),V2)
U22(tt,V2) -> U23(isList(V2))
U23(tt) -> tt
U31(tt,V) -> U32(isQid(V))
U32(tt) -> tt
U41(tt,V1,V2) -> U42(isList(V1),V2)
U42(tt,V2) -> U43(isNeList(V2))
U43(tt) -> tt
U51(tt,V1,V2) -> U52(isNeList(V1),V2)
U52(tt,V2) -> U53(isList(V2))
U53(tt) -> tt
U61(tt,V) -> U62(isQid(V))
U62(tt) -> tt
U71(tt,V) -> U72(isNePal(V))
U72(tt) -> tt
and(tt,X) -> X
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(__(V1,V2)) -> U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNePal(V) -> U61(isPalListKind(V),V)
isNePal(__(I,__(P,I))) -> and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))
isPal(V) -> U71(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)) -> and(isPalListKind(V1),isPalListKind(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) = X1 + X2
[tt] = 1
[U12](X) = X
[isNeList](X) = X + 1
[U21](X1,X2,X3) = X2 + 1
[U22](X1,X2) = X1
[isList](X) = X + 1
[U23](X) = 1
[U31](X1,X2) = X1 + X2
[U32](X) = X
[isQid](X) = X
[U41](X1,X2,X3) = X3 + 1
[U42](X1,X2) = X2 + 1
[U43](X) = X
[U51](X1,X2,X3) = X2 + 1
[U52](X1,X2) = X1
[U53](X) = 1
[U61](X1,X2) = X1
[U62](X) = 1
[U71](X1,X2) = X1
[U72](X) = 1
[isNePal](X) = X + 1
[and](X1,X2) = X2
[isPalListKind](X) = 1
[isPal](X) = 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U52](X1,X2) = X1 + X2
[nF_U51](X1,X2,X3) = X1 + X2 + X3
[nF_isNeList](X) = X
[nF_U42](X1,X2) = X1 + X2
[nF_U41](X1,X2,X3) = X1 + X2 + X3
[nF_U22](X1,X2) = X1 + X2
[nF_U21](X1,X2,X3) = X1 + X2 + X3

TIME: 7.8797e-2

-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_isNeList(V)
nF_isList(V) -> nF_U11(isPalListKind(V),V)
nF_U22(tt,V2) -> nF_isList(V2)
nF_U21(tt,V1,V2) -> nF_U22(isList(V1),V2)
nF_isList(__(V1,V2)) -> nF_U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U41(tt,V1,V2) -> nF_isList(V1)
nF_isNeList(__(V1,V2)) -> nF_U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U42(tt,V2) -> nF_isNeList(V2)
nF_U41(tt,V1,V2) -> nF_U42(isList(V1),V2)
nF_U51(tt,V1,V2) -> nF_isNeList(V1)
nF_isNeList(__(V1,V2)) -> nF_U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U52(tt,V2) -> nF_isList(V2)
nF_U51(tt,V1,V2) -> nF_U52(isNeList(V1),V2)

Usable Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U11(tt,V) -> U12(isNeList(V))
U12(tt) -> tt
U21(tt,V1,V2) -> U22(isList(V1),V2)
U22(tt,V2) -> U23(isList(V2))
U23(tt) -> tt
U31(tt,V) -> U32(isQid(V))
U32(tt) -> tt
U41(tt,V1,V2) -> U42(isList(V1),V2)
U42(tt,V2) -> U43(isNeList(V2))
U43(tt) -> tt
U51(tt,V1,V2) -> U52(isNeList(V1),V2)
U52(tt,V2) -> U53(isList(V2))
U53(tt) -> tt
U61(tt,V) -> U62(isQid(V))
U62(tt) -> tt
U71(tt,V) -> U72(isNePal(V))
U72(tt) -> tt
and(tt,X) -> X
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(__(V1,V2)) -> U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNePal(V) -> U61(isPalListKind(V),V)
isNePal(__(I,__(P,I))) -> and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))
isPal(V) -> U71(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)) -> and(isPalListKind(V1),isPalListKind(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](X) = 0
[isNeList](X) = 0
[U21](X1,X2,X3) = X2 + 1
[U22](X1,X2) = X1
[isList](X) = X + 1
[U23](X) = 0
[U31](X1,X2) = 0
[U32](X) = 0
[isQid](X) = 0
[U41](X1,X2,X3) = 0
[U42](X1,X2) = 0
[U43](X) = 0
[U51](X1,X2,X3) = 0
[U52](X1,X2) = 0
[U53](X) = 0
[U61](X1,X2) = 0
[U62](X) = 0
[U71](X1,X2) = 0
[U72](X) = 0
[isNePal](X) = X
[and](X1,X2) = X2
[isPalListKind](X) = X
[isPal](X) = 0
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U22](X1,X2) = X2
[nF_U21](X1,X2,X3) = X3
[nF_U41](X1,X2,X3) = X2 + X3
[nF_isNeList](X) = X
[nF_U42](X1,X2) = X2
[nF_U51](X1,X2,X3) = X2 + X3 + 1
[nF_U52](X1,X2) = X2

TIME: 7.5187e-2

-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_isNeList(V)
nF_isList(V) -> nF_U11(isPalListKind(V),V)
nF_U41(tt,V1,V2) -> nF_isList(V1)
nF_isNeList(__(V1,V2)) -> nF_U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U51(tt,V1,V2) -> nF_isNeList(V1)
nF_isNeList(__(V1,V2)) -> nF_U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U42(tt,V2) -> nF_isNeList(V2)
nF_U41(tt,V1,V2) -> nF_U42(isList(V1),V2)
nF_U22(tt,V2) -> nF_isList(V2)
nF_U21(tt,V1,V2) -> nF_U22(isList(V1),V2)
nF_isList(__(V1,V2)) -> nF_U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)

Usable Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U11(tt,V) -> U12(isNeList(V))
U12(tt) -> tt
U21(tt,V1,V2) -> U22(isList(V1),V2)
U22(tt,V2) -> U23(isList(V2))
U23(tt) -> tt
U31(tt,V) -> U32(isQid(V))
U32(tt) -> tt
U41(tt,V1,V2) -> U42(isList(V1),V2)
U42(tt,V2) -> U43(isNeList(V2))
U43(tt) -> tt
U51(tt,V1,V2) -> U52(isNeList(V1),V2)
U52(tt,V2) -> U53(isList(V2))
U53(tt) -> tt
U61(tt,V) -> U62(isQid(V))
U62(tt) -> tt
U71(tt,V) -> U72(isNePal(V))
U72(tt) -> tt
and(tt,X) -> X
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(__(V1,V2)) -> U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNePal(V) -> U61(isPalListKind(V),V)
isNePal(__(I,__(P,I))) -> and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))
isPal(V) -> U71(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)) -> and(isPalListKind(V1),isPalListKind(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](X) = 0
[isNeList](X) = X
[U21](X1,X2,X3) = 0
[U22](X1,X2) = 0
[isList](X) = X
[U23](X) = 0
[U31](X1,X2) = 0
[U32](X) = 0
[isQid](X) = 0
[U41](X1,X2,X3) = 0
[U42](X1,X2) = 0
[U43](X) = 0
[U51](X1,X2,X3) = 0
[U52](X1,X2) = 0
[U53](X) = 0
[U61](X1,X2) = 0
[U62](X) = 0
[U71](X1,X2) = 0
[U72](X) = 0
[isNePal](X) = X
[and](X1,X2) = X2
[isPalListKind](X) = 0
[isPal](X) = 0
[a] = 0
[e] = 0
[i] = 0
[o] = 0
[u] = 0
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U41](X1,X2,X3) = X2 + X3
[nF_isNeList](X) = X
[nF_U51](X1,X2,X3) = X2
[nF_U42](X1,X2) = X2
[nF_U22](X1,X2) = X2
[nF_U21](X1,X2,X3) = X3

TIME: 7.5212e-2

-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_isNeList(V)
nF_isList(V) -> nF_U11(isPalListKind(V),V)
nF_U41(tt,V1,V2) -> nF_isList(V1)
nF_isNeList(__(V1,V2)) -> nF_U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
nF_U42(tt,V2) -> nF_isNeList(V2)
nF_U41(tt,V1,V2) -> nF_U42(isList(V1),V2)
nF_U51(tt,V1,V2) -> nF_isNeList(V1)
nF_isNeList(__(V1,V2)) -> nF_U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)

Usable Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U11(tt,V) -> U12(isNeList(V))
U12(tt) -> tt
U21(tt,V1,V2) -> U22(isList(V1),V2)
U22(tt,V2) -> U23(isList(V2))
U23(tt) -> tt
U31(tt,V) -> U32(isQid(V))
U32(tt) -> tt
U41(tt,V1,V2) -> U42(isList(V1),V2)
U42(tt,V2) -> U43(isNeList(V2))
U43(tt) -> tt
U51(tt,V1,V2) -> U52(isNeList(V1),V2)
U52(tt,V2) -> U53(isList(V2))
U53(tt) -> tt
U61(tt,V) -> U62(isQid(V))
U62(tt) -> tt
U71(tt,V) -> U72(isNePal(V))
U72(tt) -> tt
and(tt,X) -> X
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(__(V1,V2)) -> U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNePal(V) -> U61(isPalListKind(V),V)
isNePal(__(I,__(P,I))) -> and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))
isPal(V) -> U71(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)) -> and(isPalListKind(V1),isPalListKind(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) = 1
[tt] = 1
[U12](X) = 1
[isNeList](X) = X
[U21](X1,X2,X3) = 1
[U22](X1,X2) = 1
[isList](X) = 1
[U23](X) = X
[U31](X1,X2) = X2
[U32](X) = X
[isQid](X) = X
[U41](X1,X2,X3) = X3
[U42](X1,X2) = X2
[U43](X) = X
[U51](X1,X2,X3) = X1 + X2
[U52](X1,X2) = X1
[U53](X) = 1
[U61](X1,X2) = X1
[U62](X) = 1
[U71](X1,X2) = X1
[U72](X) = 1
[isNePal](X) = X
[and](X1,X2) = X2
[isPalListKind](X) = X
[isPal](X) = X
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X2
[nF_isList](X) = X
[nF_U41](X1,X2,X3) = X2 + X3 + 1
[nF_isNeList](X) = X
[nF_U42](X1,X2) = X1 + X2
[nF_U51](X1,X2,X3) = X2

TIME: 0.176655

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

Usable Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U11(tt,V) -> U12(isNeList(V))
U12(tt) -> tt
U21(tt,V1,V2) -> U22(isList(V1),V2)
U22(tt,V2) -> U23(isList(V2))
U23(tt) -> tt
U31(tt,V) -> U32(isQid(V))
U32(tt) -> tt
U41(tt,V1,V2) -> U42(isList(V1),V2)
U42(tt,V2) -> U43(isNeList(V2))
U43(tt) -> tt
U51(tt,V1,V2) -> U52(isNeList(V1),V2)
U52(tt,V2) -> U53(isList(V2))
U53(tt) -> tt
U61(tt,V) -> U62(isQid(V))
U62(tt) -> tt
U71(tt,V) -> U72(isNePal(V))
U72(tt) -> tt
and(tt,X) -> X
isList(V) -> U11(isPalListKind(V),V)
isList(nil) -> tt
isList(__(V1,V2)) -> U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(V) -> U31(isPalListKind(V),V)
isNeList(__(V1,V2)) -> U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNeList(__(V1,V2)) -> U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)
isNePal(V) -> U61(isPalListKind(V),V)
isNePal(__(I,__(P,I))) -> and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))
isPal(V) -> U71(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)) -> and(isPalListKind(V1),isPalListKind(V2))
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt

Polynomial Interpretation:

[__](X1,X2) = X1 + X2
[nil] = 1
[U11](X1,X2) = X2
[tt] = 1
[U12](X) = X
[isNeList](X) = X
[U21](X1,X2,X3) = X3
[U22](X1,X2) = X2
[isList](X) = X
[U23](X) = X
[U31](X1,X2) = X2
[U32](X) = X
[isQid](X) = X
[U41](X1,X2,X3) = X2
[U42](X1,X2) = X1
[U43](X) = 1
[U51](X1,X2,X3) = X2
[U52](X1,X2) = X1
[U53](X) = 1
[U61](X1,X2) = X1 + X2
[U62](X) = X
[U71](X1,X2) = X1
[U72](X) = 1
[isNePal](X) = X + 1
[and](X1,X2) = X2
[isPalListKind](X) = 1
[isPal](X) = X + 1
[a] = 1
[e] = 1
[i] = 1
[o] = 1
[u] = 1
[nF_U11](X1,X2) = X1 + X2
[nF_isList](X) = X + 1
[nF_U41](X1,X2,X3) = X1 + X2 + X3
[nF_isNeList](X) = X + 1
[nF_U42](X1,X2) = X1 + X2

TIME: 0.173188

-> -> Dependency pairs in cycle:
nF_U11(tt,V) -> nF_isNeList(V)
nF_isList(V) -> nF_U11(isPalListKind(V),V)
nF_U41(tt,V1,V2) -> nF_isList(V1)
nF_isNeList(__(V1,V2)) -> nF_U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_complete_1_2:
-> -> Dependency pairs in cycle:
nF_isPalListKind(__(V1,V2)) -> nF_isPalListKind(V1)
nF_isPal(V) -> nF_isPalListKind(V)
nF_and(tt,X) -> X
nF_isPalListKind(__(V1,V2)) -> nF_and(isPalListKind(V1),isPalListKind(V2))
nF_isNePal(V) -> nF_isPalListKind(V)
nF_U71(tt,V) -> nF_isNePal(V)
nF_isPal(V) -> nF_U71(isPalListKind(V),V)
nF_isNePal(__(I,__(P,I))) -> nF_and(isQid(I),isPalListKind(I))
nF_isNePal(__(I,__(P,I))) -> nF_and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))

Usable Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil) -> X
__(nil,X) -> X
U61(tt,V) -> U62(isQid(V))
U62(tt) -> tt
U71(tt,V) -> U72(isNePal(V))
U72(tt) -> tt
and(tt,X) -> X
isNePal(V) -> U61(isPalListKind(V),V)
isNePal(__(I,__(P,I))) -> and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))
isPal(V) -> U71(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)) -> and(isPalListKind(V1),isPalListKind(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) = X1
[tt] = 0
[U12](X) = X
[isNeList](X) = 0
[U21](X1,X2,X3) = X1
[U22](X1,X2) = X1
[isList](X) = 0
[U23](X) = X
[U31](X1,X2) = X1
[U32](X) = X
[isQid](X) = 0
[U41](X1,X2,X3) = X1
[U42](X1,X2) = X1
[U43](X) = X
[U51](X1,X2,X3) = X1
[U52](X1,X2) = X1
[U53](X) = X
[U61](X1,X2) = X1
[U62](X) = X
[U71](X1,X2) = X1 + X2
[U72](X) = X
[isNePal](X) = X
[and](X1,X2) = X1 + X2
[isPalListKind](X) = 0
[isPal](X) = X + 1
[a] = 0
[e] = 0
[i] = 0
[o] = 0
[u] = 0
[nF_isPalListKind](X) = 0
[nF_isPal](X) = X
[nF_and](X1,X2) = X2
[nF_isNePal](X) = X
[nF_U71](X1,X2) = X2

TIME: 5.2157e-2

-> -> Dependency pairs in cycle:
nF_isPalListKind(__(V1,V2)) -> nF_isPalListKind(V1)
nF_isNePal(V) -> nF_isPalListKind(V)
nF_U71(tt,V) -> nF_isNePal(V)
nF_isPal(V) -> nF_U71(isPalListKind(V),V)
nF_and(tt,X) -> X
nF_isNePal(__(I,__(P,I))) -> nF_and(isQid(I),isPalListKind(I))
nF_isPalListKind(__(V1,V2)) -> nF_and(isPalListKind(V1),isPalListKind(V2))
nF_isPal(V) -> nF_isPalListKind(V)


Polynomial Interpretation:

[__](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[__](X1,X2) = X1 + X2 + 1
[isPalListKind](X) = X + 1
[__](X1,X2) = X1 + X2 + 1
[isPalListKind](X) = X + 1
[isNePal](X) = X + 1
[U71](X1,X2) = X1 + X2 + 1
[isPal](X) = X + 1
[and](X1,X2) = X1 + X2 + 1
[U11](X1,X2) = X1
[U12](X) = X
[U21](X1,X2,X3) = X1
[U22](X1,X2) = X1
[U23](X) = X
[U31](X1,X2) = X1
[U32](X) = X
[U41](X1,X2,X3) = X1
[U42](X1,X2) = X1
[U43](X) = X
[U51](X1,X2,X3) = X1
[U52](X1,X2) = X1
[U53](X) = X
[U61](X1,X2) = X1
[U62](X) = X
[U72](X) = X

TIME: 1.5749e-2

Termination proved: There exists a projection such that there are no minimal mu-rewrite sequences in cycle.
-> -> Dependency pairs in cycle:
nF_isPalListKind(__(V1,V2)) -> nF_isPalListKind(V1)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for PALINDROME_complete_1_3:
-> -> 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.