Runtime Complexity (innermost) proof of /tmp/tmpvzFIqh/PALINDROME_complete_noand

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(1)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 788 ms)

↳2 CdtProblem

↳3 CdtUnreachableProof (⇔, 10 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 SIsEmptyProof (⇔, 0 ms)

↳8 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

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

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(U11(tt, z0)) → mark(U12(isPalListKind(z0), z0))
active(U12(tt, z0)) → mark(U13(isNeList(z0)))
active(U13(tt)) → mark(tt)
active(U21(tt, z0, z1)) → mark(U22(isPalListKind(z0), z0, z1))
active(U22(tt, z0, z1)) → mark(U23(isPalListKind(z1), z0, z1))
active(U23(tt, z0, z1)) → mark(U24(isPalListKind(z1), z0, z1))
active(U24(tt, z0, z1)) → mark(U25(isList(z0), z1))
active(U25(tt, z0)) → mark(U26(isList(z0)))
active(U26(tt)) → mark(tt)
active(U31(tt, z0)) → mark(U32(isPalListKind(z0), z0))
active(U32(tt, z0)) → mark(U33(isQid(z0)))
active(U33(tt)) → mark(tt)
active(U41(tt, z0, z1)) → mark(U42(isPalListKind(z0), z0, z1))
active(U42(tt, z0, z1)) → mark(U43(isPalListKind(z1), z0, z1))
active(U43(tt, z0, z1)) → mark(U44(isPalListKind(z1), z0, z1))
active(U44(tt, z0, z1)) → mark(U45(isList(z0), z1))
active(U45(tt, z0)) → mark(U46(isNeList(z0)))
active(U46(tt)) → mark(tt)
active(U51(tt, z0, z1)) → mark(U52(isPalListKind(z0), z0, z1))
active(U52(tt, z0, z1)) → mark(U53(isPalListKind(z1), z0, z1))
active(U53(tt, z0, z1)) → mark(U54(isPalListKind(z1), z0, z1))
active(U54(tt, z0, z1)) → mark(U55(isNeList(z0), z1))
active(U55(tt, z0)) → mark(U56(isList(z0)))
active(U56(tt)) → mark(tt)
active(U61(tt, z0)) → mark(U62(isPalListKind(z0), z0))
active(U62(tt, z0)) → mark(U63(isQid(z0)))
active(U63(tt)) → mark(tt)
active(U71(tt, z0, z1)) → mark(U72(isPalListKind(z0), z1))
active(U72(tt, z0)) → mark(U73(isPal(z0), z0))
active(U73(tt, z0)) → mark(U74(isPalListKind(z0)))
active(U74(tt)) → mark(tt)
active(U81(tt, z0)) → mark(U82(isPalListKind(z0), z0))
active(U82(tt, z0)) → mark(U83(isNePal(z0)))
active(U83(tt)) → mark(tt)
active(U91(tt, z0)) → mark(U92(isPalListKind(z0)))
active(U92(tt)) → mark(tt)
active(isList(z0)) → mark(U11(isPalListKind(z0), z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(U21(isPalListKind(z0), z0, z1))
active(isNeList(z0)) → mark(U31(isPalListKind(z0), z0))
active(isNeList(__(z0, z1))) → mark(U41(isPalListKind(z0), z0, z1))
active(isNeList(__(z0, z1))) → mark(U51(isPalListKind(z0), z0, z1))
active(isNePal(z0)) → mark(U61(isPalListKind(z0), z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(U71(isQid(z0), z0, z1))
active(isPal(z0)) → mark(U81(isPalListKind(z0), z0))
active(isPal(nil)) → mark(tt)
active(isPalListKind(a)) → mark(tt)
active(isPalListKind(e)) → mark(tt)
active(isPalListKind(i)) → mark(tt)
active(isPalListKind(nil)) → mark(tt)
active(isPalListKind(o)) → mark(tt)
active(isPalListKind(u)) → mark(tt)
active(isPalListKind(__(z0, z1))) → mark(U91(isPalListKind(z0), z1))
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(U11(z0, z1)) → active(U11(mark(z0), z1))
mark(tt) → active(tt)
mark(U12(z0, z1)) → active(U12(mark(z0), z1))
mark(isPalListKind(z0)) → active(isPalListKind(z0))
mark(U13(z0)) → active(U13(mark(z0)))
mark(isNeList(z0)) → active(isNeList(z0))
mark(U21(z0, z1, z2)) → active(U21(mark(z0), z1, z2))
mark(U22(z0, z1, z2)) → active(U22(mark(z0), z1, z2))
mark(U23(z0, z1, z2)) → active(U23(mark(z0), z1, z2))
mark(U24(z0, z1, z2)) → active(U24(mark(z0), z1, z2))
mark(U25(z0, z1)) → active(U25(mark(z0), z1))
mark(isList(z0)) → active(isList(z0))
mark(U26(z0)) → active(U26(mark(z0)))
mark(U31(z0, z1)) → active(U31(mark(z0), z1))
mark(U32(z0, z1)) → active(U32(mark(z0), z1))
mark(U33(z0)) → active(U33(mark(z0)))
mark(isQid(z0)) → active(isQid(z0))
mark(U41(z0, z1, z2)) → active(U41(mark(z0), z1, z2))
mark(U42(z0, z1, z2)) → active(U42(mark(z0), z1, z2))
mark(U43(z0, z1, z2)) → active(U43(mark(z0), z1, z2))
mark(U44(z0, z1, z2)) → active(U44(mark(z0), z1, z2))
mark(U45(z0, z1)) → active(U45(mark(z0), z1))
mark(U46(z0)) → active(U46(mark(z0)))
mark(U51(z0, z1, z2)) → active(U51(mark(z0), z1, z2))
mark(U52(z0, z1, z2)) → active(U52(mark(z0), z1, z2))
mark(U53(z0, z1, z2)) → active(U53(mark(z0), z1, z2))
mark(U54(z0, z1, z2)) → active(U54(mark(z0), z1, z2))
mark(U55(z0, z1)) → active(U55(mark(z0), z1))
mark(U56(z0)) → active(U56(mark(z0)))
mark(U61(z0, z1)) → active(U61(mark(z0), z1))
mark(U62(z0, z1)) → active(U62(mark(z0), z1))
mark(U63(z0)) → active(U63(mark(z0)))
mark(U71(z0, z1, z2)) → active(U71(mark(z0), z1, z2))
mark(U72(z0, z1)) → active(U72(mark(z0), z1))
mark(U73(z0, z1)) → active(U73(mark(z0), z1))
mark(isPal(z0)) → active(isPal(z0))
mark(U74(z0)) → active(U74(mark(z0)))
mark(U81(z0, z1)) → active(U81(mark(z0), z1))
mark(U82(z0, z1)) → active(U82(mark(z0), z1))
mark(U83(z0)) → active(U83(mark(z0)))
mark(isNePal(z0)) → active(isNePal(z0))
mark(U91(z0, z1)) → active(U91(mark(z0), z1))
mark(U92(z0)) → active(U92(mark(z0)))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
U11(mark(z0), z1) → U11(z0, z1)
U11(z0, mark(z1)) → U11(z0, z1)
U11(active(z0), z1) → U11(z0, z1)
U11(z0, active(z1)) → U11(z0, z1)
U12(mark(z0), z1) → U12(z0, z1)
U12(z0, mark(z1)) → U12(z0, z1)
U12(active(z0), z1) → U12(z0, z1)
U12(z0, active(z1)) → U12(z0, z1)
isPalListKind(mark(z0)) → isPalListKind(z0)
isPalListKind(active(z0)) → isPalListKind(z0)
U13(mark(z0)) → U13(z0)
U13(active(z0)) → U13(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
U21(mark(z0), z1, z2) → U21(z0, z1, z2)
U21(z0, mark(z1), z2) → U21(z0, z1, z2)
U21(z0, z1, mark(z2)) → U21(z0, z1, z2)
U21(active(z0), z1, z2) → U21(z0, z1, z2)
U21(z0, active(z1), z2) → U21(z0, z1, z2)
U21(z0, z1, active(z2)) → U21(z0, z1, z2)
U22(mark(z0), z1, z2) → U22(z0, z1, z2)
U22(z0, mark(z1), z2) → U22(z0, z1, z2)
U22(z0, z1, mark(z2)) → U22(z0, z1, z2)
U22(active(z0), z1, z2) → U22(z0, z1, z2)
U22(z0, active(z1), z2) → U22(z0, z1, z2)
U22(z0, z1, active(z2)) → U22(z0, z1, z2)
U23(mark(z0), z1, z2) → U23(z0, z1, z2)
U23(z0, mark(z1), z2) → U23(z0, z1, z2)
U23(z0, z1, mark(z2)) → U23(z0, z1, z2)
U23(active(z0), z1, z2) → U23(z0, z1, z2)
U23(z0, active(z1), z2) → U23(z0, z1, z2)
U23(z0, z1, active(z2)) → U23(z0, z1, z2)
U24(mark(z0), z1, z2) → U24(z0, z1, z2)
U24(z0, mark(z1), z2) → U24(z0, z1, z2)
U24(z0, z1, mark(z2)) → U24(z0, z1, z2)
U24(active(z0), z1, z2) → U24(z0, z1, z2)
U24(z0, active(z1), z2) → U24(z0, z1, z2)
U24(z0, z1, active(z2)) → U24(z0, z1, z2)
U25(mark(z0), z1) → U25(z0, z1)
U25(z0, mark(z1)) → U25(z0, z1)
U25(active(z0), z1) → U25(z0, z1)
U25(z0, active(z1)) → U25(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
U26(mark(z0)) → U26(z0)
U26(active(z0)) → U26(z0)
U31(mark(z0), z1) → U31(z0, z1)
U31(z0, mark(z1)) → U31(z0, z1)
U31(active(z0), z1) → U31(z0, z1)
U31(z0, active(z1)) → U31(z0, z1)
U32(mark(z0), z1) → U32(z0, z1)
U32(z0, mark(z1)) → U32(z0, z1)
U32(active(z0), z1) → U32(z0, z1)
U32(z0, active(z1)) → U32(z0, z1)
U33(mark(z0)) → U33(z0)
U33(active(z0)) → U33(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
U41(mark(z0), z1, z2) → U41(z0, z1, z2)
U41(z0, mark(z1), z2) → U41(z0, z1, z2)
U41(z0, z1, mark(z2)) → U41(z0, z1, z2)
U41(active(z0), z1, z2) → U41(z0, z1, z2)
U41(z0, active(z1), z2) → U41(z0, z1, z2)
U41(z0, z1, active(z2)) → U41(z0, z1, z2)
U42(mark(z0), z1, z2) → U42(z0, z1, z2)
U42(z0, mark(z1), z2) → U42(z0, z1, z2)
U42(z0, z1, mark(z2)) → U42(z0, z1, z2)
U42(active(z0), z1, z2) → U42(z0, z1, z2)
U42(z0, active(z1), z2) → U42(z0, z1, z2)
U42(z0, z1, active(z2)) → U42(z0, z1, z2)
U43(mark(z0), z1, z2) → U43(z0, z1, z2)
U43(z0, mark(z1), z2) → U43(z0, z1, z2)
U43(z0, z1, mark(z2)) → U43(z0, z1, z2)
U43(active(z0), z1, z2) → U43(z0, z1, z2)
U43(z0, active(z1), z2) → U43(z0, z1, z2)
U43(z0, z1, active(z2)) → U43(z0, z1, z2)
U44(mark(z0), z1, z2) → U44(z0, z1, z2)
U44(z0, mark(z1), z2) → U44(z0, z1, z2)
U44(z0, z1, mark(z2)) → U44(z0, z1, z2)
U44(active(z0), z1, z2) → U44(z0, z1, z2)
U44(z0, active(z1), z2) → U44(z0, z1, z2)
U44(z0, z1, active(z2)) → U44(z0, z1, z2)
U45(mark(z0), z1) → U45(z0, z1)
U45(z0, mark(z1)) → U45(z0, z1)
U45(active(z0), z1) → U45(z0, z1)
U45(z0, active(z1)) → U45(z0, z1)
U46(mark(z0)) → U46(z0)
U46(active(z0)) → U46(z0)
U51(mark(z0), z1, z2) → U51(z0, z1, z2)
U51(z0, mark(z1), z2) → U51(z0, z1, z2)
U51(z0, z1, mark(z2)) → U51(z0, z1, z2)
U51(active(z0), z1, z2) → U51(z0, z1, z2)
U51(z0, active(z1), z2) → U51(z0, z1, z2)
U51(z0, z1, active(z2)) → U51(z0, z1, z2)
U52(mark(z0), z1, z2) → U52(z0, z1, z2)
U52(z0, mark(z1), z2) → U52(z0, z1, z2)
U52(z0, z1, mark(z2)) → U52(z0, z1, z2)
U52(active(z0), z1, z2) → U52(z0, z1, z2)
U52(z0, active(z1), z2) → U52(z0, z1, z2)
U52(z0, z1, active(z2)) → U52(z0, z1, z2)
U53(mark(z0), z1, z2) → U53(z0, z1, z2)
U53(z0, mark(z1), z2) → U53(z0, z1, z2)
U53(z0, z1, mark(z2)) → U53(z0, z1, z2)
U53(active(z0), z1, z2) → U53(z0, z1, z2)
U53(z0, active(z1), z2) → U53(z0, z1, z2)
U53(z0, z1, active(z2)) → U53(z0, z1, z2)
U54(mark(z0), z1, z2) → U54(z0, z1, z2)
U54(z0, mark(z1), z2) → U54(z0, z1, z2)
U54(z0, z1, mark(z2)) → U54(z0, z1, z2)
U54(active(z0), z1, z2) → U54(z0, z1, z2)
U54(z0, active(z1), z2) → U54(z0, z1, z2)
U54(z0, z1, active(z2)) → U54(z0, z1, z2)
U55(mark(z0), z1) → U55(z0, z1)
U55(z0, mark(z1)) → U55(z0, z1)
U55(active(z0), z1) → U55(z0, z1)
U55(z0, active(z1)) → U55(z0, z1)
U56(mark(z0)) → U56(z0)
U56(active(z0)) → U56(z0)
U61(mark(z0), z1) → U61(z0, z1)
U61(z0, mark(z1)) → U61(z0, z1)
U61(active(z0), z1) → U61(z0, z1)
U61(z0, active(z1)) → U61(z0, z1)
U62(mark(z0), z1) → U62(z0, z1)
U62(z0, mark(z1)) → U62(z0, z1)
U62(active(z0), z1) → U62(z0, z1)
U62(z0, active(z1)) → U62(z0, z1)
U63(mark(z0)) → U63(z0)
U63(active(z0)) → U63(z0)
U71(mark(z0), z1, z2) → U71(z0, z1, z2)
U71(z0, mark(z1), z2) → U71(z0, z1, z2)
U71(z0, z1, mark(z2)) → U71(z0, z1, z2)
U71(active(z0), z1, z2) → U71(z0, z1, z2)
U71(z0, active(z1), z2) → U71(z0, z1, z2)
U71(z0, z1, active(z2)) → U71(z0, z1, z2)
U72(mark(z0), z1) → U72(z0, z1)
U72(z0, mark(z1)) → U72(z0, z1)
U72(active(z0), z1) → U72(z0, z1)
U72(z0, active(z1)) → U72(z0, z1)
U73(mark(z0), z1) → U73(z0, z1)
U73(z0, mark(z1)) → U73(z0, z1)
U73(active(z0), z1) → U73(z0, z1)
U73(z0, active(z1)) → U73(z0, z1)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)
U74(mark(z0)) → U74(z0)
U74(active(z0)) → U74(z0)
U81(mark(z0), z1) → U81(z0, z1)
U81(z0, mark(z1)) → U81(z0, z1)
U81(active(z0), z1) → U81(z0, z1)
U81(z0, active(z1)) → U81(z0, z1)
U82(mark(z0), z1) → U82(z0, z1)
U82(z0, mark(z1)) → U82(z0, z1)
U82(active(z0), z1) → U82(z0, z1)
U82(z0, active(z1)) → U82(z0, z1)
U83(mark(z0)) → U83(z0)
U83(active(z0)) → U83(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
U91(mark(z0), z1) → U91(z0, z1)
U91(z0, mark(z1)) → U91(z0, z1)
U91(active(z0), z1) → U91(z0, z1)
U91(z0, active(z1)) → U91(z0, z1)
U92(mark(z0)) → U92(z0)
U92(active(z0)) → U92(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(U11(tt, z0)) → c3(MARK(U12(isPalListKind(z0), z0)), U12'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U12(tt, z0)) → c4(MARK(U13(isNeList(z0))), U13'(isNeList(z0)), ISNELIST(z0))
ACTIVE(U13(tt)) → c5(MARK(tt))
ACTIVE(U21(tt, z0, z1)) → c6(MARK(U22(isPalListKind(z0), z0, z1)), U22'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U22(tt, z0, z1)) → c7(MARK(U23(isPalListKind(z1), z0, z1)), U23'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U23(tt, z0, z1)) → c8(MARK(U24(isPalListKind(z1), z0, z1)), U24'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U24(tt, z0, z1)) → c9(MARK(U25(isList(z0), z1)), U25'(isList(z0), z1), ISLIST(z0))
ACTIVE(U25(tt, z0)) → c10(MARK(U26(isList(z0))), U26'(isList(z0)), ISLIST(z0))
ACTIVE(U26(tt)) → c11(MARK(tt))
ACTIVE(U31(tt, z0)) → c12(MARK(U32(isPalListKind(z0), z0)), U32'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U32(tt, z0)) → c13(MARK(U33(isQid(z0))), U33'(isQid(z0)), ISQID(z0))
ACTIVE(U33(tt)) → c14(MARK(tt))
ACTIVE(U41(tt, z0, z1)) → c15(MARK(U42(isPalListKind(z0), z0, z1)), U42'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U42(tt, z0, z1)) → c16(MARK(U43(isPalListKind(z1), z0, z1)), U43'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U43(tt, z0, z1)) → c17(MARK(U44(isPalListKind(z1), z0, z1)), U44'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U44(tt, z0, z1)) → c18(MARK(U45(isList(z0), z1)), U45'(isList(z0), z1), ISLIST(z0))
ACTIVE(U45(tt, z0)) → c19(MARK(U46(isNeList(z0))), U46'(isNeList(z0)), ISNELIST(z0))
ACTIVE(U46(tt)) → c20(MARK(tt))
ACTIVE(U51(tt, z0, z1)) → c21(MARK(U52(isPalListKind(z0), z0, z1)), U52'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U52(tt, z0, z1)) → c22(MARK(U53(isPalListKind(z1), z0, z1)), U53'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U53(tt, z0, z1)) → c23(MARK(U54(isPalListKind(z1), z0, z1)), U54'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U54(tt, z0, z1)) → c24(MARK(U55(isNeList(z0), z1)), U55'(isNeList(z0), z1), ISNELIST(z0))
ACTIVE(U55(tt, z0)) → c25(MARK(U56(isList(z0))), U56'(isList(z0)), ISLIST(z0))
ACTIVE(U56(tt)) → c26(MARK(tt))
ACTIVE(U61(tt, z0)) → c27(MARK(U62(isPalListKind(z0), z0)), U62'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U62(tt, z0)) → c28(MARK(U63(isQid(z0))), U63'(isQid(z0)), ISQID(z0))
ACTIVE(U63(tt)) → c29(MARK(tt))
ACTIVE(U71(tt, z0, z1)) → c30(MARK(U72(isPalListKind(z0), z1)), U72'(isPalListKind(z0), z1), ISPALLISTKIND(z0))
ACTIVE(U72(tt, z0)) → c31(MARK(U73(isPal(z0), z0)), U73'(isPal(z0), z0), ISPAL(z0))
ACTIVE(U73(tt, z0)) → c32(MARK(U74(isPalListKind(z0))), U74'(isPalListKind(z0)), ISPALLISTKIND(z0))
ACTIVE(U74(tt)) → c33(MARK(tt))
ACTIVE(U81(tt, z0)) → c34(MARK(U82(isPalListKind(z0), z0)), U82'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U82(tt, z0)) → c35(MARK(U83(isNePal(z0))), U83'(isNePal(z0)), ISNEPAL(z0))
ACTIVE(U83(tt)) → c36(MARK(tt))
ACTIVE(U91(tt, z0)) → c37(MARK(U92(isPalListKind(z0))), U92'(isPalListKind(z0)), ISPALLISTKIND(z0))
ACTIVE(U92(tt)) → c38(MARK(tt))
ACTIVE(isList(z0)) → c39(MARK(U11(isPalListKind(z0), z0)), U11'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isList(nil)) → c40(MARK(tt))
ACTIVE(isList(__(z0, z1))) → c41(MARK(U21(isPalListKind(z0), z0, z1)), U21'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNeList(z0)) → c42(MARK(U31(isPalListKind(z0), z0)), U31'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isNeList(__(z0, z1))) → c43(MARK(U41(isPalListKind(z0), z0, z1)), U41'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNeList(__(z0, z1))) → c44(MARK(U51(isPalListKind(z0), z0, z1)), U51'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNePal(z0)) → c45(MARK(U61(isPalListKind(z0), z0)), U61'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c46(MARK(U71(isQid(z0), z0, z1)), U71'(isQid(z0), z0, z1), ISQID(z0))
ACTIVE(isPal(z0)) → c47(MARK(U81(isPalListKind(z0), z0)), U81'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isPal(nil)) → c48(MARK(tt))
ACTIVE(isPalListKind(a)) → c49(MARK(tt))
ACTIVE(isPalListKind(e)) → c50(MARK(tt))
ACTIVE(isPalListKind(i)) → c51(MARK(tt))
ACTIVE(isPalListKind(nil)) → c52(MARK(tt))
ACTIVE(isPalListKind(o)) → c53(MARK(tt))
ACTIVE(isPalListKind(u)) → c54(MARK(tt))
ACTIVE(isPalListKind(__(z0, z1))) → c55(MARK(U91(isPalListKind(z0), z1)), U91'(isPalListKind(z0), z1), ISPALLISTKIND(z0))
ACTIVE(isQid(a)) → c56(MARK(tt))
ACTIVE(isQid(e)) → c57(MARK(tt))
ACTIVE(isQid(i)) → c58(MARK(tt))
ACTIVE(isQid(o)) → c59(MARK(tt))
ACTIVE(isQid(u)) → c60(MARK(tt))
MARK(__(z0, z1)) → c61(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(nil) → c62(ACTIVE(nil))
MARK(U11(z0, z1)) → c63(ACTIVE(U11(mark(z0), z1)), U11'(mark(z0), z1), MARK(z0))
MARK(tt) → c64(ACTIVE(tt))
MARK(U12(z0, z1)) → c65(ACTIVE(U12(mark(z0), z1)), U12'(mark(z0), z1), MARK(z0))
MARK(isPalListKind(z0)) → c66(ACTIVE(isPalListKind(z0)), ISPALLISTKIND(z0))
MARK(U13(z0)) → c67(ACTIVE(U13(mark(z0))), U13'(mark(z0)), MARK(z0))
MARK(isNeList(z0)) → c68(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(U21(z0, z1, z2)) → c69(ACTIVE(U21(mark(z0), z1, z2)), U21'(mark(z0), z1, z2), MARK(z0))
MARK(U22(z0, z1, z2)) → c70(ACTIVE(U22(mark(z0), z1, z2)), U22'(mark(z0), z1, z2), MARK(z0))
MARK(U23(z0, z1, z2)) → c71(ACTIVE(U23(mark(z0), z1, z2)), U23'(mark(z0), z1, z2), MARK(z0))
MARK(U24(z0, z1, z2)) → c72(ACTIVE(U24(mark(z0), z1, z2)), U24'(mark(z0), z1, z2), MARK(z0))
MARK(U25(z0, z1)) → c73(ACTIVE(U25(mark(z0), z1)), U25'(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c74(ACTIVE(isList(z0)), ISLIST(z0))
MARK(U26(z0)) → c75(ACTIVE(U26(mark(z0))), U26'(mark(z0)), MARK(z0))
MARK(U31(z0, z1)) → c76(ACTIVE(U31(mark(z0), z1)), U31'(mark(z0), z1), MARK(z0))
MARK(U32(z0, z1)) → c77(ACTIVE(U32(mark(z0), z1)), U32'(mark(z0), z1), MARK(z0))
MARK(U33(z0)) → c78(ACTIVE(U33(mark(z0))), U33'(mark(z0)), MARK(z0))
MARK(isQid(z0)) → c79(ACTIVE(isQid(z0)), ISQID(z0))
MARK(U41(z0, z1, z2)) → c80(ACTIVE(U41(mark(z0), z1, z2)), U41'(mark(z0), z1, z2), MARK(z0))
MARK(U42(z0, z1, z2)) → c81(ACTIVE(U42(mark(z0), z1, z2)), U42'(mark(z0), z1, z2), MARK(z0))
MARK(U43(z0, z1, z2)) → c82(ACTIVE(U43(mark(z0), z1, z2)), U43'(mark(z0), z1, z2), MARK(z0))
MARK(U44(z0, z1, z2)) → c83(ACTIVE(U44(mark(z0), z1, z2)), U44'(mark(z0), z1, z2), MARK(z0))
MARK(U45(z0, z1)) → c84(ACTIVE(U45(mark(z0), z1)), U45'(mark(z0), z1), MARK(z0))
MARK(U46(z0)) → c85(ACTIVE(U46(mark(z0))), U46'(mark(z0)), MARK(z0))
MARK(U51(z0, z1, z2)) → c86(ACTIVE(U51(mark(z0), z1, z2)), U51'(mark(z0), z1, z2), MARK(z0))
MARK(U52(z0, z1, z2)) → c87(ACTIVE(U52(mark(z0), z1, z2)), U52'(mark(z0), z1, z2), MARK(z0))
MARK(U53(z0, z1, z2)) → c88(ACTIVE(U53(mark(z0), z1, z2)), U53'(mark(z0), z1, z2), MARK(z0))
MARK(U54(z0, z1, z2)) → c89(ACTIVE(U54(mark(z0), z1, z2)), U54'(mark(z0), z1, z2), MARK(z0))
MARK(U55(z0, z1)) → c90(ACTIVE(U55(mark(z0), z1)), U55'(mark(z0), z1), MARK(z0))
MARK(U56(z0)) → c91(ACTIVE(U56(mark(z0))), U56'(mark(z0)), MARK(z0))
MARK(U61(z0, z1)) → c92(ACTIVE(U61(mark(z0), z1)), U61'(mark(z0), z1), MARK(z0))
MARK(U62(z0, z1)) → c93(ACTIVE(U62(mark(z0), z1)), U62'(mark(z0), z1), MARK(z0))
MARK(U63(z0)) → c94(ACTIVE(U63(mark(z0))), U63'(mark(z0)), MARK(z0))
MARK(U71(z0, z1, z2)) → c95(ACTIVE(U71(mark(z0), z1, z2)), U71'(mark(z0), z1, z2), MARK(z0))
MARK(U72(z0, z1)) → c96(ACTIVE(U72(mark(z0), z1)), U72'(mark(z0), z1), MARK(z0))
MARK(U73(z0, z1)) → c97(ACTIVE(U73(mark(z0), z1)), U73'(mark(z0), z1), MARK(z0))
MARK(isPal(z0)) → c98(ACTIVE(isPal(z0)), ISPAL(z0))
MARK(U74(z0)) → c99(ACTIVE(U74(mark(z0))), U74'(mark(z0)), MARK(z0))
MARK(U81(z0, z1)) → c100(ACTIVE(U81(mark(z0), z1)), U81'(mark(z0), z1), MARK(z0))
MARK(U82(z0, z1)) → c101(ACTIVE(U82(mark(z0), z1)), U82'(mark(z0), z1), MARK(z0))
MARK(U83(z0)) → c102(ACTIVE(U83(mark(z0))), U83'(mark(z0)), MARK(z0))
MARK(isNePal(z0)) → c103(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(U91(z0, z1)) → c104(ACTIVE(U91(mark(z0), z1)), U91'(mark(z0), z1), MARK(z0))
MARK(U92(z0)) → c105(ACTIVE(U92(mark(z0))), U92'(mark(z0)), MARK(z0))
MARK(a) → c106(ACTIVE(a))
MARK(e) → c107(ACTIVE(e))
MARK(i) → c108(ACTIVE(i))
MARK(o) → c109(ACTIVE(o))
MARK(u) → c110(ACTIVE(u))
__'(mark(z0), z1) → c111(__'(z0, z1))
__'(z0, mark(z1)) → c112(__'(z0, z1))
__'(active(z0), z1) → c113(__'(z0, z1))
__'(z0, active(z1)) → c114(__'(z0, z1))
U11'(mark(z0), z1) → c115(U11'(z0, z1))
U11'(z0, mark(z1)) → c116(U11'(z0, z1))
U11'(active(z0), z1) → c117(U11'(z0, z1))
U11'(z0, active(z1)) → c118(U11'(z0, z1))
U12'(mark(z0), z1) → c119(U12'(z0, z1))
U12'(z0, mark(z1)) → c120(U12'(z0, z1))
U12'(active(z0), z1) → c121(U12'(z0, z1))
U12'(z0, active(z1)) → c122(U12'(z0, z1))
ISPALLISTKIND(mark(z0)) → c123(ISPALLISTKIND(z0))
ISPALLISTKIND(active(z0)) → c124(ISPALLISTKIND(z0))
U13'(mark(z0)) → c125(U13'(z0))
U13'(active(z0)) → c126(U13'(z0))
ISNELIST(mark(z0)) → c127(ISNELIST(z0))
ISNELIST(active(z0)) → c128(ISNELIST(z0))
U21'(mark(z0), z1, z2) → c129(U21'(z0, z1, z2))
U21'(z0, mark(z1), z2) → c130(U21'(z0, z1, z2))
U21'(z0, z1, mark(z2)) → c131(U21'(z0, z1, z2))
U21'(active(z0), z1, z2) → c132(U21'(z0, z1, z2))
U21'(z0, active(z1), z2) → c133(U21'(z0, z1, z2))
U21'(z0, z1, active(z2)) → c134(U21'(z0, z1, z2))
U22'(mark(z0), z1, z2) → c135(U22'(z0, z1, z2))
U22'(z0, mark(z1), z2) → c136(U22'(z0, z1, z2))
U22'(z0, z1, mark(z2)) → c137(U22'(z0, z1, z2))
U22'(active(z0), z1, z2) → c138(U22'(z0, z1, z2))
U22'(z0, active(z1), z2) → c139(U22'(z0, z1, z2))
U22'(z0, z1, active(z2)) → c140(U22'(z0, z1, z2))
U23'(mark(z0), z1, z2) → c141(U23'(z0, z1, z2))
U23'(z0, mark(z1), z2) → c142(U23'(z0, z1, z2))
U23'(z0, z1, mark(z2)) → c143(U23'(z0, z1, z2))
U23'(active(z0), z1, z2) → c144(U23'(z0, z1, z2))
U23'(z0, active(z1), z2) → c145(U23'(z0, z1, z2))
U23'(z0, z1, active(z2)) → c146(U23'(z0, z1, z2))
U24'(mark(z0), z1, z2) → c147(U24'(z0, z1, z2))
U24'(z0, mark(z1), z2) → c148(U24'(z0, z1, z2))
U24'(z0, z1, mark(z2)) → c149(U24'(z0, z1, z2))
U24'(active(z0), z1, z2) → c150(U24'(z0, z1, z2))
U24'(z0, active(z1), z2) → c151(U24'(z0, z1, z2))
U24'(z0, z1, active(z2)) → c152(U24'(z0, z1, z2))
U25'(mark(z0), z1) → c153(U25'(z0, z1))
U25'(z0, mark(z1)) → c154(U25'(z0, z1))
U25'(active(z0), z1) → c155(U25'(z0, z1))
U25'(z0, active(z1)) → c156(U25'(z0, z1))
ISLIST(mark(z0)) → c157(ISLIST(z0))
ISLIST(active(z0)) → c158(ISLIST(z0))
U26'(mark(z0)) → c159(U26'(z0))
U26'(active(z0)) → c160(U26'(z0))
U31'(mark(z0), z1) → c161(U31'(z0, z1))
U31'(z0, mark(z1)) → c162(U31'(z0, z1))
U31'(active(z0), z1) → c163(U31'(z0, z1))
U31'(z0, active(z1)) → c164(U31'(z0, z1))
U32'(mark(z0), z1) → c165(U32'(z0, z1))
U32'(z0, mark(z1)) → c166(U32'(z0, z1))
U32'(active(z0), z1) → c167(U32'(z0, z1))
U32'(z0, active(z1)) → c168(U32'(z0, z1))
U33'(mark(z0)) → c169(U33'(z0))
U33'(active(z0)) → c170(U33'(z0))
ISQID(mark(z0)) → c171(ISQID(z0))
ISQID(active(z0)) → c172(ISQID(z0))
U41'(mark(z0), z1, z2) → c173(U41'(z0, z1, z2))
U41'(z0, mark(z1), z2) → c174(U41'(z0, z1, z2))
U41'(z0, z1, mark(z2)) → c175(U41'(z0, z1, z2))
U41'(active(z0), z1, z2) → c176(U41'(z0, z1, z2))
U41'(z0, active(z1), z2) → c177(U41'(z0, z1, z2))
U41'(z0, z1, active(z2)) → c178(U41'(z0, z1, z2))
U42'(mark(z0), z1, z2) → c179(U42'(z0, z1, z2))
U42'(z0, mark(z1), z2) → c180(U42'(z0, z1, z2))
U42'(z0, z1, mark(z2)) → c181(U42'(z0, z1, z2))
U42'(active(z0), z1, z2) → c182(U42'(z0, z1, z2))
U42'(z0, active(z1), z2) → c183(U42'(z0, z1, z2))
U42'(z0, z1, active(z2)) → c184(U42'(z0, z1, z2))
U43'(mark(z0), z1, z2) → c185(U43'(z0, z1, z2))
U43'(z0, mark(z1), z2) → c186(U43'(z0, z1, z2))
U43'(z0, z1, mark(z2)) → c187(U43'(z0, z1, z2))
U43'(active(z0), z1, z2) → c188(U43'(z0, z1, z2))
U43'(z0, active(z1), z2) → c189(U43'(z0, z1, z2))
U43'(z0, z1, active(z2)) → c190(U43'(z0, z1, z2))
U44'(mark(z0), z1, z2) → c191(U44'(z0, z1, z2))
U44'(z0, mark(z1), z2) → c192(U44'(z0, z1, z2))
U44'(z0, z1, mark(z2)) → c193(U44'(z0, z1, z2))
U44'(active(z0), z1, z2) → c194(U44'(z0, z1, z2))
U44'(z0, active(z1), z2) → c195(U44'(z0, z1, z2))
U44'(z0, z1, active(z2)) → c196(U44'(z0, z1, z2))
U45'(mark(z0), z1) → c197(U45'(z0, z1))
U45'(z0, mark(z1)) → c198(U45'(z0, z1))
U45'(active(z0), z1) → c199(U45'(z0, z1))
U45'(z0, active(z1)) → c200(U45'(z0, z1))
U46'(mark(z0)) → c201(U46'(z0))
U46'(active(z0)) → c202(U46'(z0))
U51'(mark(z0), z1, z2) → c203(U51'(z0, z1, z2))
U51'(z0, mark(z1), z2) → c204(U51'(z0, z1, z2))
U51'(z0, z1, mark(z2)) → c205(U51'(z0, z1, z2))
U51'(active(z0), z1, z2) → c206(U51'(z0, z1, z2))
U51'(z0, active(z1), z2) → c207(U51'(z0, z1, z2))
U51'(z0, z1, active(z2)) → c208(U51'(z0, z1, z2))
U52'(mark(z0), z1, z2) → c209(U52'(z0, z1, z2))
U52'(z0, mark(z1), z2) → c210(U52'(z0, z1, z2))
U52'(z0, z1, mark(z2)) → c211(U52'(z0, z1, z2))
U52'(active(z0), z1, z2) → c212(U52'(z0, z1, z2))
U52'(z0, active(z1), z2) → c213(U52'(z0, z1, z2))
U52'(z0, z1, active(z2)) → c214(U52'(z0, z1, z2))
U53'(mark(z0), z1, z2) → c215(U53'(z0, z1, z2))
U53'(z0, mark(z1), z2) → c216(U53'(z0, z1, z2))
U53'(z0, z1, mark(z2)) → c217(U53'(z0, z1, z2))
U53'(active(z0), z1, z2) → c218(U53'(z0, z1, z2))
U53'(z0, active(z1), z2) → c219(U53'(z0, z1, z2))
U53'(z0, z1, active(z2)) → c220(U53'(z0, z1, z2))
U54'(mark(z0), z1, z2) → c221(U54'(z0, z1, z2))
U54'(z0, mark(z1), z2) → c222(U54'(z0, z1, z2))
U54'(z0, z1, mark(z2)) → c223(U54'(z0, z1, z2))
U54'(active(z0), z1, z2) → c224(U54'(z0, z1, z2))
U54'(z0, active(z1), z2) → c225(U54'(z0, z1, z2))
U54'(z0, z1, active(z2)) → c226(U54'(z0, z1, z2))
U55'(mark(z0), z1) → c227(U55'(z0, z1))
U55'(z0, mark(z1)) → c228(U55'(z0, z1))
U55'(active(z0), z1) → c229(U55'(z0, z1))
U55'(z0, active(z1)) → c230(U55'(z0, z1))
U56'(mark(z0)) → c231(U56'(z0))
U56'(active(z0)) → c232(U56'(z0))
U61'(mark(z0), z1) → c233(U61'(z0, z1))
U61'(z0, mark(z1)) → c234(U61'(z0, z1))
U61'(active(z0), z1) → c235(U61'(z0, z1))
U61'(z0, active(z1)) → c236(U61'(z0, z1))
U62'(mark(z0), z1) → c237(U62'(z0, z1))
U62'(z0, mark(z1)) → c238(U62'(z0, z1))
U62'(active(z0), z1) → c239(U62'(z0, z1))
U62'(z0, active(z1)) → c240(U62'(z0, z1))
U63'(mark(z0)) → c241(U63'(z0))
U63'(active(z0)) → c242(U63'(z0))
U71'(mark(z0), z1, z2) → c243(U71'(z0, z1, z2))
U71'(z0, mark(z1), z2) → c244(U71'(z0, z1, z2))
U71'(z0, z1, mark(z2)) → c245(U71'(z0, z1, z2))
U71'(active(z0), z1, z2) → c246(U71'(z0, z1, z2))
U71'(z0, active(z1), z2) → c247(U71'(z0, z1, z2))
U71'(z0, z1, active(z2)) → c248(U71'(z0, z1, z2))
U72'(mark(z0), z1) → c249(U72'(z0, z1))
U72'(z0, mark(z1)) → c250(U72'(z0, z1))
U72'(active(z0), z1) → c251(U72'(z0, z1))
U72'(z0, active(z1)) → c252(U72'(z0, z1))
U73'(mark(z0), z1) → c253(U73'(z0, z1))
U73'(z0, mark(z1)) → c254(U73'(z0, z1))
U73'(active(z0), z1) → c255(U73'(z0, z1))
U73'(z0, active(z1)) → c256(U73'(z0, z1))
ISPAL(mark(z0)) → c257(ISPAL(z0))
ISPAL(active(z0)) → c258(ISPAL(z0))
U74'(mark(z0)) → c259(U74'(z0))
U74'(active(z0)) → c260(U74'(z0))
U81'(mark(z0), z1) → c261(U81'(z0, z1))
U81'(z0, mark(z1)) → c262(U81'(z0, z1))
U81'(active(z0), z1) → c263(U81'(z0, z1))
U81'(z0, active(z1)) → c264(U81'(z0, z1))
U82'(mark(z0), z1) → c265(U82'(z0, z1))
U82'(z0, mark(z1)) → c266(U82'(z0, z1))
U82'(active(z0), z1) → c267(U82'(z0, z1))
U82'(z0, active(z1)) → c268(U82'(z0, z1))
U83'(mark(z0)) → c269(U83'(z0))
U83'(active(z0)) → c270(U83'(z0))
ISNEPAL(mark(z0)) → c271(ISNEPAL(z0))
ISNEPAL(active(z0)) → c272(ISNEPAL(z0))
U91'(mark(z0), z1) → c273(U91'(z0, z1))
U91'(z0, mark(z1)) → c274(U91'(z0, z1))
U91'(active(z0), z1) → c275(U91'(z0, z1))
U91'(z0, active(z1)) → c276(U91'(z0, z1))
U92'(mark(z0)) → c277(U92'(z0))
U92'(active(z0)) → c278(U92'(z0))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(U11(tt, z0)) → c3(MARK(U12(isPalListKind(z0), z0)), U12'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U12(tt, z0)) → c4(MARK(U13(isNeList(z0))), U13'(isNeList(z0)), ISNELIST(z0))
ACTIVE(U13(tt)) → c5(MARK(tt))
ACTIVE(U21(tt, z0, z1)) → c6(MARK(U22(isPalListKind(z0), z0, z1)), U22'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U22(tt, z0, z1)) → c7(MARK(U23(isPalListKind(z1), z0, z1)), U23'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U23(tt, z0, z1)) → c8(MARK(U24(isPalListKind(z1), z0, z1)), U24'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U24(tt, z0, z1)) → c9(MARK(U25(isList(z0), z1)), U25'(isList(z0), z1), ISLIST(z0))
ACTIVE(U25(tt, z0)) → c10(MARK(U26(isList(z0))), U26'(isList(z0)), ISLIST(z0))
ACTIVE(U26(tt)) → c11(MARK(tt))
ACTIVE(U31(tt, z0)) → c12(MARK(U32(isPalListKind(z0), z0)), U32'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U32(tt, z0)) → c13(MARK(U33(isQid(z0))), U33'(isQid(z0)), ISQID(z0))
ACTIVE(U33(tt)) → c14(MARK(tt))
ACTIVE(U41(tt, z0, z1)) → c15(MARK(U42(isPalListKind(z0), z0, z1)), U42'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U42(tt, z0, z1)) → c16(MARK(U43(isPalListKind(z1), z0, z1)), U43'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U43(tt, z0, z1)) → c17(MARK(U44(isPalListKind(z1), z0, z1)), U44'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U44(tt, z0, z1)) → c18(MARK(U45(isList(z0), z1)), U45'(isList(z0), z1), ISLIST(z0))
ACTIVE(U45(tt, z0)) → c19(MARK(U46(isNeList(z0))), U46'(isNeList(z0)), ISNELIST(z0))
ACTIVE(U46(tt)) → c20(MARK(tt))
ACTIVE(U51(tt, z0, z1)) → c21(MARK(U52(isPalListKind(z0), z0, z1)), U52'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U52(tt, z0, z1)) → c22(MARK(U53(isPalListKind(z1), z0, z1)), U53'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U53(tt, z0, z1)) → c23(MARK(U54(isPalListKind(z1), z0, z1)), U54'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U54(tt, z0, z1)) → c24(MARK(U55(isNeList(z0), z1)), U55'(isNeList(z0), z1), ISNELIST(z0))
ACTIVE(U55(tt, z0)) → c25(MARK(U56(isList(z0))), U56'(isList(z0)), ISLIST(z0))
ACTIVE(U56(tt)) → c26(MARK(tt))
ACTIVE(U61(tt, z0)) → c27(MARK(U62(isPalListKind(z0), z0)), U62'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U62(tt, z0)) → c28(MARK(U63(isQid(z0))), U63'(isQid(z0)), ISQID(z0))
ACTIVE(U63(tt)) → c29(MARK(tt))
ACTIVE(U71(tt, z0, z1)) → c30(MARK(U72(isPalListKind(z0), z1)), U72'(isPalListKind(z0), z1), ISPALLISTKIND(z0))
ACTIVE(U72(tt, z0)) → c31(MARK(U73(isPal(z0), z0)), U73'(isPal(z0), z0), ISPAL(z0))
ACTIVE(U73(tt, z0)) → c32(MARK(U74(isPalListKind(z0))), U74'(isPalListKind(z0)), ISPALLISTKIND(z0))
ACTIVE(U74(tt)) → c33(MARK(tt))
ACTIVE(U81(tt, z0)) → c34(MARK(U82(isPalListKind(z0), z0)), U82'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U82(tt, z0)) → c35(MARK(U83(isNePal(z0))), U83'(isNePal(z0)), ISNEPAL(z0))
ACTIVE(U83(tt)) → c36(MARK(tt))
ACTIVE(U91(tt, z0)) → c37(MARK(U92(isPalListKind(z0))), U92'(isPalListKind(z0)), ISPALLISTKIND(z0))
ACTIVE(U92(tt)) → c38(MARK(tt))
ACTIVE(isList(z0)) → c39(MARK(U11(isPalListKind(z0), z0)), U11'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isList(nil)) → c40(MARK(tt))
ACTIVE(isList(__(z0, z1))) → c41(MARK(U21(isPalListKind(z0), z0, z1)), U21'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNeList(z0)) → c42(MARK(U31(isPalListKind(z0), z0)), U31'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isNeList(__(z0, z1))) → c43(MARK(U41(isPalListKind(z0), z0, z1)), U41'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNeList(__(z0, z1))) → c44(MARK(U51(isPalListKind(z0), z0, z1)), U51'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNePal(z0)) → c45(MARK(U61(isPalListKind(z0), z0)), U61'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c46(MARK(U71(isQid(z0), z0, z1)), U71'(isQid(z0), z0, z1), ISQID(z0))
ACTIVE(isPal(z0)) → c47(MARK(U81(isPalListKind(z0), z0)), U81'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isPal(nil)) → c48(MARK(tt))
ACTIVE(isPalListKind(a)) → c49(MARK(tt))
ACTIVE(isPalListKind(e)) → c50(MARK(tt))
ACTIVE(isPalListKind(i)) → c51(MARK(tt))
ACTIVE(isPalListKind(nil)) → c52(MARK(tt))
ACTIVE(isPalListKind(o)) → c53(MARK(tt))
ACTIVE(isPalListKind(u)) → c54(MARK(tt))
ACTIVE(isPalListKind(__(z0, z1))) → c55(MARK(U91(isPalListKind(z0), z1)), U91'(isPalListKind(z0), z1), ISPALLISTKIND(z0))
ACTIVE(isQid(a)) → c56(MARK(tt))
ACTIVE(isQid(e)) → c57(MARK(tt))
ACTIVE(isQid(i)) → c58(MARK(tt))
ACTIVE(isQid(o)) → c59(MARK(tt))
ACTIVE(isQid(u)) → c60(MARK(tt))
MARK(__(z0, z1)) → c61(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(nil) → c62(ACTIVE(nil))
MARK(U11(z0, z1)) → c63(ACTIVE(U11(mark(z0), z1)), U11'(mark(z0), z1), MARK(z0))
MARK(tt) → c64(ACTIVE(tt))
MARK(U12(z0, z1)) → c65(ACTIVE(U12(mark(z0), z1)), U12'(mark(z0), z1), MARK(z0))
MARK(isPalListKind(z0)) → c66(ACTIVE(isPalListKind(z0)), ISPALLISTKIND(z0))
MARK(U13(z0)) → c67(ACTIVE(U13(mark(z0))), U13'(mark(z0)), MARK(z0))
MARK(isNeList(z0)) → c68(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(U21(z0, z1, z2)) → c69(ACTIVE(U21(mark(z0), z1, z2)), U21'(mark(z0), z1, z2), MARK(z0))
MARK(U22(z0, z1, z2)) → c70(ACTIVE(U22(mark(z0), z1, z2)), U22'(mark(z0), z1, z2), MARK(z0))
MARK(U23(z0, z1, z2)) → c71(ACTIVE(U23(mark(z0), z1, z2)), U23'(mark(z0), z1, z2), MARK(z0))
MARK(U24(z0, z1, z2)) → c72(ACTIVE(U24(mark(z0), z1, z2)), U24'(mark(z0), z1, z2), MARK(z0))
MARK(U25(z0, z1)) → c73(ACTIVE(U25(mark(z0), z1)), U25'(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c74(ACTIVE(isList(z0)), ISLIST(z0))
MARK(U26(z0)) → c75(ACTIVE(U26(mark(z0))), U26'(mark(z0)), MARK(z0))
MARK(U31(z0, z1)) → c76(ACTIVE(U31(mark(z0), z1)), U31'(mark(z0), z1), MARK(z0))
MARK(U32(z0, z1)) → c77(ACTIVE(U32(mark(z0), z1)), U32'(mark(z0), z1), MARK(z0))
MARK(U33(z0)) → c78(ACTIVE(U33(mark(z0))), U33'(mark(z0)), MARK(z0))
MARK(isQid(z0)) → c79(ACTIVE(isQid(z0)), ISQID(z0))
MARK(U41(z0, z1, z2)) → c80(ACTIVE(U41(mark(z0), z1, z2)), U41'(mark(z0), z1, z2), MARK(z0))
MARK(U42(z0, z1, z2)) → c81(ACTIVE(U42(mark(z0), z1, z2)), U42'(mark(z0), z1, z2), MARK(z0))
MARK(U43(z0, z1, z2)) → c82(ACTIVE(U43(mark(z0), z1, z2)), U43'(mark(z0), z1, z2), MARK(z0))
MARK(U44(z0, z1, z2)) → c83(ACTIVE(U44(mark(z0), z1, z2)), U44'(mark(z0), z1, z2), MARK(z0))
MARK(U45(z0, z1)) → c84(ACTIVE(U45(mark(z0), z1)), U45'(mark(z0), z1), MARK(z0))
MARK(U46(z0)) → c85(ACTIVE(U46(mark(z0))), U46'(mark(z0)), MARK(z0))
MARK(U51(z0, z1, z2)) → c86(ACTIVE(U51(mark(z0), z1, z2)), U51'(mark(z0), z1, z2), MARK(z0))
MARK(U52(z0, z1, z2)) → c87(ACTIVE(U52(mark(z0), z1, z2)), U52'(mark(z0), z1, z2), MARK(z0))
MARK(U53(z0, z1, z2)) → c88(ACTIVE(U53(mark(z0), z1, z2)), U53'(mark(z0), z1, z2), MARK(z0))
MARK(U54(z0, z1, z2)) → c89(ACTIVE(U54(mark(z0), z1, z2)), U54'(mark(z0), z1, z2), MARK(z0))
MARK(U55(z0, z1)) → c90(ACTIVE(U55(mark(z0), z1)), U55'(mark(z0), z1), MARK(z0))
MARK(U56(z0)) → c91(ACTIVE(U56(mark(z0))), U56'(mark(z0)), MARK(z0))
MARK(U61(z0, z1)) → c92(ACTIVE(U61(mark(z0), z1)), U61'(mark(z0), z1), MARK(z0))
MARK(U62(z0, z1)) → c93(ACTIVE(U62(mark(z0), z1)), U62'(mark(z0), z1), MARK(z0))
MARK(U63(z0)) → c94(ACTIVE(U63(mark(z0))), U63'(mark(z0)), MARK(z0))
MARK(U71(z0, z1, z2)) → c95(ACTIVE(U71(mark(z0), z1, z2)), U71'(mark(z0), z1, z2), MARK(z0))
MARK(U72(z0, z1)) → c96(ACTIVE(U72(mark(z0), z1)), U72'(mark(z0), z1), MARK(z0))
MARK(U73(z0, z1)) → c97(ACTIVE(U73(mark(z0), z1)), U73'(mark(z0), z1), MARK(z0))
MARK(isPal(z0)) → c98(ACTIVE(isPal(z0)), ISPAL(z0))
MARK(U74(z0)) → c99(ACTIVE(U74(mark(z0))), U74'(mark(z0)), MARK(z0))
MARK(U81(z0, z1)) → c100(ACTIVE(U81(mark(z0), z1)), U81'(mark(z0), z1), MARK(z0))
MARK(U82(z0, z1)) → c101(ACTIVE(U82(mark(z0), z1)), U82'(mark(z0), z1), MARK(z0))
MARK(U83(z0)) → c102(ACTIVE(U83(mark(z0))), U83'(mark(z0)), MARK(z0))
MARK(isNePal(z0)) → c103(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(U91(z0, z1)) → c104(ACTIVE(U91(mark(z0), z1)), U91'(mark(z0), z1), MARK(z0))
MARK(U92(z0)) → c105(ACTIVE(U92(mark(z0))), U92'(mark(z0)), MARK(z0))
MARK(a) → c106(ACTIVE(a))
MARK(e) → c107(ACTIVE(e))
MARK(i) → c108(ACTIVE(i))
MARK(o) → c109(ACTIVE(o))
MARK(u) → c110(ACTIVE(u))
__'(mark(z0), z1) → c111(__'(z0, z1))
__'(z0, mark(z1)) → c112(__'(z0, z1))
__'(active(z0), z1) → c113(__'(z0, z1))
__'(z0, active(z1)) → c114(__'(z0, z1))
U11'(mark(z0), z1) → c115(U11'(z0, z1))
U11'(z0, mark(z1)) → c116(U11'(z0, z1))
U11'(active(z0), z1) → c117(U11'(z0, z1))
U11'(z0, active(z1)) → c118(U11'(z0, z1))
U12'(mark(z0), z1) → c119(U12'(z0, z1))
U12'(z0, mark(z1)) → c120(U12'(z0, z1))
U12'(active(z0), z1) → c121(U12'(z0, z1))
U12'(z0, active(z1)) → c122(U12'(z0, z1))
ISPALLISTKIND(mark(z0)) → c123(ISPALLISTKIND(z0))
ISPALLISTKIND(active(z0)) → c124(ISPALLISTKIND(z0))
U13'(mark(z0)) → c125(U13'(z0))
U13'(active(z0)) → c126(U13'(z0))
ISNELIST(mark(z0)) → c127(ISNELIST(z0))
ISNELIST(active(z0)) → c128(ISNELIST(z0))
U21'(mark(z0), z1, z2) → c129(U21'(z0, z1, z2))
U21'(z0, mark(z1), z2) → c130(U21'(z0, z1, z2))
U21'(z0, z1, mark(z2)) → c131(U21'(z0, z1, z2))
U21'(active(z0), z1, z2) → c132(U21'(z0, z1, z2))
U21'(z0, active(z1), z2) → c133(U21'(z0, z1, z2))
U21'(z0, z1, active(z2)) → c134(U21'(z0, z1, z2))
U22'(mark(z0), z1, z2) → c135(U22'(z0, z1, z2))
U22'(z0, mark(z1), z2) → c136(U22'(z0, z1, z2))
U22'(z0, z1, mark(z2)) → c137(U22'(z0, z1, z2))
U22'(active(z0), z1, z2) → c138(U22'(z0, z1, z2))
U22'(z0, active(z1), z2) → c139(U22'(z0, z1, z2))
U22'(z0, z1, active(z2)) → c140(U22'(z0, z1, z2))
U23'(mark(z0), z1, z2) → c141(U23'(z0, z1, z2))
U23'(z0, mark(z1), z2) → c142(U23'(z0, z1, z2))
U23'(z0, z1, mark(z2)) → c143(U23'(z0, z1, z2))
U23'(active(z0), z1, z2) → c144(U23'(z0, z1, z2))
U23'(z0, active(z1), z2) → c145(U23'(z0, z1, z2))
U23'(z0, z1, active(z2)) → c146(U23'(z0, z1, z2))
U24'(mark(z0), z1, z2) → c147(U24'(z0, z1, z2))
U24'(z0, mark(z1), z2) → c148(U24'(z0, z1, z2))
U24'(z0, z1, mark(z2)) → c149(U24'(z0, z1, z2))
U24'(active(z0), z1, z2) → c150(U24'(z0, z1, z2))
U24'(z0, active(z1), z2) → c151(U24'(z0, z1, z2))
U24'(z0, z1, active(z2)) → c152(U24'(z0, z1, z2))
U25'(mark(z0), z1) → c153(U25'(z0, z1))
U25'(z0, mark(z1)) → c154(U25'(z0, z1))
U25'(active(z0), z1) → c155(U25'(z0, z1))
U25'(z0, active(z1)) → c156(U25'(z0, z1))
ISLIST(mark(z0)) → c157(ISLIST(z0))
ISLIST(active(z0)) → c158(ISLIST(z0))
U26'(mark(z0)) → c159(U26'(z0))
U26'(active(z0)) → c160(U26'(z0))
U31'(mark(z0), z1) → c161(U31'(z0, z1))
U31'(z0, mark(z1)) → c162(U31'(z0, z1))
U31'(active(z0), z1) → c163(U31'(z0, z1))
U31'(z0, active(z1)) → c164(U31'(z0, z1))
U32'(mark(z0), z1) → c165(U32'(z0, z1))
U32'(z0, mark(z1)) → c166(U32'(z0, z1))
U32'(active(z0), z1) → c167(U32'(z0, z1))
U32'(z0, active(z1)) → c168(U32'(z0, z1))
U33'(mark(z0)) → c169(U33'(z0))
U33'(active(z0)) → c170(U33'(z0))
ISQID(mark(z0)) → c171(ISQID(z0))
ISQID(active(z0)) → c172(ISQID(z0))
U41'(mark(z0), z1, z2) → c173(U41'(z0, z1, z2))
U41'(z0, mark(z1), z2) → c174(U41'(z0, z1, z2))
U41'(z0, z1, mark(z2)) → c175(U41'(z0, z1, z2))
U41'(active(z0), z1, z2) → c176(U41'(z0, z1, z2))
U41'(z0, active(z1), z2) → c177(U41'(z0, z1, z2))
U41'(z0, z1, active(z2)) → c178(U41'(z0, z1, z2))
U42'(mark(z0), z1, z2) → c179(U42'(z0, z1, z2))
U42'(z0, mark(z1), z2) → c180(U42'(z0, z1, z2))
U42'(z0, z1, mark(z2)) → c181(U42'(z0, z1, z2))
U42'(active(z0), z1, z2) → c182(U42'(z0, z1, z2))
U42'(z0, active(z1), z2) → c183(U42'(z0, z1, z2))
U42'(z0, z1, active(z2)) → c184(U42'(z0, z1, z2))
U43'(mark(z0), z1, z2) → c185(U43'(z0, z1, z2))
U43'(z0, mark(z1), z2) → c186(U43'(z0, z1, z2))
U43'(z0, z1, mark(z2)) → c187(U43'(z0, z1, z2))
U43'(active(z0), z1, z2) → c188(U43'(z0, z1, z2))
U43'(z0, active(z1), z2) → c189(U43'(z0, z1, z2))
U43'(z0, z1, active(z2)) → c190(U43'(z0, z1, z2))
U44'(mark(z0), z1, z2) → c191(U44'(z0, z1, z2))
U44'(z0, mark(z1), z2) → c192(U44'(z0, z1, z2))
U44'(z0, z1, mark(z2)) → c193(U44'(z0, z1, z2))
U44'(active(z0), z1, z2) → c194(U44'(z0, z1, z2))
U44'(z0, active(z1), z2) → c195(U44'(z0, z1, z2))
U44'(z0, z1, active(z2)) → c196(U44'(z0, z1, z2))
U45'(mark(z0), z1) → c197(U45'(z0, z1))
U45'(z0, mark(z1)) → c198(U45'(z0, z1))
U45'(active(z0), z1) → c199(U45'(z0, z1))
U45'(z0, active(z1)) → c200(U45'(z0, z1))
U46'(mark(z0)) → c201(U46'(z0))
U46'(active(z0)) → c202(U46'(z0))
U51'(mark(z0), z1, z2) → c203(U51'(z0, z1, z2))
U51'(z0, mark(z1), z2) → c204(U51'(z0, z1, z2))
U51'(z0, z1, mark(z2)) → c205(U51'(z0, z1, z2))
U51'(active(z0), z1, z2) → c206(U51'(z0, z1, z2))
U51'(z0, active(z1), z2) → c207(U51'(z0, z1, z2))
U51'(z0, z1, active(z2)) → c208(U51'(z0, z1, z2))
U52'(mark(z0), z1, z2) → c209(U52'(z0, z1, z2))
U52'(z0, mark(z1), z2) → c210(U52'(z0, z1, z2))
U52'(z0, z1, mark(z2)) → c211(U52'(z0, z1, z2))
U52'(active(z0), z1, z2) → c212(U52'(z0, z1, z2))
U52'(z0, active(z1), z2) → c213(U52'(z0, z1, z2))
U52'(z0, z1, active(z2)) → c214(U52'(z0, z1, z2))
U53'(mark(z0), z1, z2) → c215(U53'(z0, z1, z2))
U53'(z0, mark(z1), z2) → c216(U53'(z0, z1, z2))
U53'(z0, z1, mark(z2)) → c217(U53'(z0, z1, z2))
U53'(active(z0), z1, z2) → c218(U53'(z0, z1, z2))
U53'(z0, active(z1), z2) → c219(U53'(z0, z1, z2))
U53'(z0, z1, active(z2)) → c220(U53'(z0, z1, z2))
U54'(mark(z0), z1, z2) → c221(U54'(z0, z1, z2))
U54'(z0, mark(z1), z2) → c222(U54'(z0, z1, z2))
U54'(z0, z1, mark(z2)) → c223(U54'(z0, z1, z2))
U54'(active(z0), z1, z2) → c224(U54'(z0, z1, z2))
U54'(z0, active(z1), z2) → c225(U54'(z0, z1, z2))
U54'(z0, z1, active(z2)) → c226(U54'(z0, z1, z2))
U55'(mark(z0), z1) → c227(U55'(z0, z1))
U55'(z0, mark(z1)) → c228(U55'(z0, z1))
U55'(active(z0), z1) → c229(U55'(z0, z1))
U55'(z0, active(z1)) → c230(U55'(z0, z1))
U56'(mark(z0)) → c231(U56'(z0))
U56'(active(z0)) → c232(U56'(z0))
U61'(mark(z0), z1) → c233(U61'(z0, z1))
U61'(z0, mark(z1)) → c234(U61'(z0, z1))
U61'(active(z0), z1) → c235(U61'(z0, z1))
U61'(z0, active(z1)) → c236(U61'(z0, z1))
U62'(mark(z0), z1) → c237(U62'(z0, z1))
U62'(z0, mark(z1)) → c238(U62'(z0, z1))
U62'(active(z0), z1) → c239(U62'(z0, z1))
U62'(z0, active(z1)) → c240(U62'(z0, z1))
U63'(mark(z0)) → c241(U63'(z0))
U63'(active(z0)) → c242(U63'(z0))
U71'(mark(z0), z1, z2) → c243(U71'(z0, z1, z2))
U71'(z0, mark(z1), z2) → c244(U71'(z0, z1, z2))
U71'(z0, z1, mark(z2)) → c245(U71'(z0, z1, z2))
U71'(active(z0), z1, z2) → c246(U71'(z0, z1, z2))
U71'(z0, active(z1), z2) → c247(U71'(z0, z1, z2))
U71'(z0, z1, active(z2)) → c248(U71'(z0, z1, z2))
U72'(mark(z0), z1) → c249(U72'(z0, z1))
U72'(z0, mark(z1)) → c250(U72'(z0, z1))
U72'(active(z0), z1) → c251(U72'(z0, z1))
U72'(z0, active(z1)) → c252(U72'(z0, z1))
U73'(mark(z0), z1) → c253(U73'(z0, z1))
U73'(z0, mark(z1)) → c254(U73'(z0, z1))
U73'(active(z0), z1) → c255(U73'(z0, z1))
U73'(z0, active(z1)) → c256(U73'(z0, z1))
ISPAL(mark(z0)) → c257(ISPAL(z0))
ISPAL(active(z0)) → c258(ISPAL(z0))
U74'(mark(z0)) → c259(U74'(z0))
U74'(active(z0)) → c260(U74'(z0))
U81'(mark(z0), z1) → c261(U81'(z0, z1))
U81'(z0, mark(z1)) → c262(U81'(z0, z1))
U81'(active(z0), z1) → c263(U81'(z0, z1))
U81'(z0, active(z1)) → c264(U81'(z0, z1))
U82'(mark(z0), z1) → c265(U82'(z0, z1))
U82'(z0, mark(z1)) → c266(U82'(z0, z1))
U82'(active(z0), z1) → c267(U82'(z0, z1))
U82'(z0, active(z1)) → c268(U82'(z0, z1))
U83'(mark(z0)) → c269(U83'(z0))
U83'(active(z0)) → c270(U83'(z0))
ISNEPAL(mark(z0)) → c271(ISNEPAL(z0))
ISNEPAL(active(z0)) → c272(ISNEPAL(z0))
U91'(mark(z0), z1) → c273(U91'(z0, z1))
U91'(z0, mark(z1)) → c274(U91'(z0, z1))
U91'(active(z0), z1) → c275(U91'(z0, z1))
U91'(z0, active(z1)) → c276(U91'(z0, z1))
U92'(mark(z0)) → c277(U92'(z0))
U92'(active(z0)) → c278(U92'(z0))

K tuples:none
Defined Rule Symbols:

active, mark, __, U11, U12, isPalListKind, U13, isNeList, U21, U22, U23, U24, U25, isList, U26, U31, U32, U33, isQid, U41, U42, U43, U44, U45, U46, U51, U52, U53, U54, U55, U56, U61, U62, U63, U71, U72, U73, isPal, U74, U81, U82, U83, isNePal, U91, U92

Defined Pair Symbols:

ACTIVE, MARK, __', U11', U12', ISPALLISTKIND, U13', ISNELIST, U21', U22', U23', U24', U25', ISLIST, U26', U31', U32', U33', ISQID, U41', U42', U43', U44', U45', U46', U51', U52', U53', U54', U55', U56', U61', U62', U63', U71', U72', U73', ISPAL, U74', U81', U82', U83', ISNEPAL, U91', U92'

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c68, c69, c70, c71, c72, c73, c74, c75, c76, c77, c78, c79, c80, c81, c82, c83, c84, c85, c86, c87, c88, c89, c90, c91, c92, c93, c94, c95, c96, c97, c98, c99, c100, c101, c102, c103, c104, c105, c106, c107, c108, c109, c110, c111, c112, c113, c114, c115, c116, c117, c118, c119, c120, c121, c122, c123, c124, c125, c126, c127, c128, c129, c130, c131, c132, c133, c134, c135, c136, c137, c138, c139, c140, c141, c142, c143, c144, c145, c146, c147, c148, c149, c150, c151, c152, c153, c154, c155, c156, c157, c158, c159, c160, c161, c162, c163, c164, c165, c166, c167, c168, c169, c170, c171, c172, c173, c174, c175, c176, c177, c178, c179, c180, c181, c182, c183, c184, c185, c186, c187, c188, c189, c190, c191, c192, c193, c194, c195, c196, c197, c198, c199, c200, c201, c202, c203, c204, c205, c206, c207, c208, c209, c210, c211, c212, c213, c214, c215, c216, c217, c218, c219, c220, c221, c222, c223, c224, c225, c226, c227, c228, c229, c230, c231, c232, c233, c234, c235, c236, c237, c238, c239, c240, c241, c242, c243, c244, c245, c246, c247, c248, c249, c250, c251, c252, c253, c254, c255, c256, c257, c258, c259, c260, c261, c262, c263, c264, c265, c266, c267, c268, c269, c270, c271, c272, c273, c274, c275, c276, c277, c278

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(U11(tt, z0)) → c3(MARK(U12(isPalListKind(z0), z0)), U12'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U12(tt, z0)) → c4(MARK(U13(isNeList(z0))), U13'(isNeList(z0)), ISNELIST(z0))
ACTIVE(U13(tt)) → c5(MARK(tt))
ACTIVE(U21(tt, z0, z1)) → c6(MARK(U22(isPalListKind(z0), z0, z1)), U22'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U22(tt, z0, z1)) → c7(MARK(U23(isPalListKind(z1), z0, z1)), U23'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U23(tt, z0, z1)) → c8(MARK(U24(isPalListKind(z1), z0, z1)), U24'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U24(tt, z0, z1)) → c9(MARK(U25(isList(z0), z1)), U25'(isList(z0), z1), ISLIST(z0))
ACTIVE(U25(tt, z0)) → c10(MARK(U26(isList(z0))), U26'(isList(z0)), ISLIST(z0))
ACTIVE(U26(tt)) → c11(MARK(tt))
ACTIVE(U31(tt, z0)) → c12(MARK(U32(isPalListKind(z0), z0)), U32'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U32(tt, z0)) → c13(MARK(U33(isQid(z0))), U33'(isQid(z0)), ISQID(z0))
ACTIVE(U33(tt)) → c14(MARK(tt))
ACTIVE(U41(tt, z0, z1)) → c15(MARK(U42(isPalListKind(z0), z0, z1)), U42'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U42(tt, z0, z1)) → c16(MARK(U43(isPalListKind(z1), z0, z1)), U43'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U43(tt, z0, z1)) → c17(MARK(U44(isPalListKind(z1), z0, z1)), U44'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U44(tt, z0, z1)) → c18(MARK(U45(isList(z0), z1)), U45'(isList(z0), z1), ISLIST(z0))
ACTIVE(U45(tt, z0)) → c19(MARK(U46(isNeList(z0))), U46'(isNeList(z0)), ISNELIST(z0))
ACTIVE(U46(tt)) → c20(MARK(tt))
ACTIVE(U51(tt, z0, z1)) → c21(MARK(U52(isPalListKind(z0), z0, z1)), U52'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(U52(tt, z0, z1)) → c22(MARK(U53(isPalListKind(z1), z0, z1)), U53'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U53(tt, z0, z1)) → c23(MARK(U54(isPalListKind(z1), z0, z1)), U54'(isPalListKind(z1), z0, z1), ISPALLISTKIND(z1))
ACTIVE(U54(tt, z0, z1)) → c24(MARK(U55(isNeList(z0), z1)), U55'(isNeList(z0), z1), ISNELIST(z0))
ACTIVE(U55(tt, z0)) → c25(MARK(U56(isList(z0))), U56'(isList(z0)), ISLIST(z0))
ACTIVE(U56(tt)) → c26(MARK(tt))
ACTIVE(U61(tt, z0)) → c27(MARK(U62(isPalListKind(z0), z0)), U62'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U62(tt, z0)) → c28(MARK(U63(isQid(z0))), U63'(isQid(z0)), ISQID(z0))
ACTIVE(U63(tt)) → c29(MARK(tt))
ACTIVE(U71(tt, z0, z1)) → c30(MARK(U72(isPalListKind(z0), z1)), U72'(isPalListKind(z0), z1), ISPALLISTKIND(z0))
ACTIVE(U72(tt, z0)) → c31(MARK(U73(isPal(z0), z0)), U73'(isPal(z0), z0), ISPAL(z0))
ACTIVE(U73(tt, z0)) → c32(MARK(U74(isPalListKind(z0))), U74'(isPalListKind(z0)), ISPALLISTKIND(z0))
ACTIVE(U74(tt)) → c33(MARK(tt))
ACTIVE(U81(tt, z0)) → c34(MARK(U82(isPalListKind(z0), z0)), U82'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(U82(tt, z0)) → c35(MARK(U83(isNePal(z0))), U83'(isNePal(z0)), ISNEPAL(z0))
ACTIVE(U83(tt)) → c36(MARK(tt))
ACTIVE(U91(tt, z0)) → c37(MARK(U92(isPalListKind(z0))), U92'(isPalListKind(z0)), ISPALLISTKIND(z0))
ACTIVE(U92(tt)) → c38(MARK(tt))
ACTIVE(isList(z0)) → c39(MARK(U11(isPalListKind(z0), z0)), U11'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isList(nil)) → c40(MARK(tt))
ACTIVE(isList(__(z0, z1))) → c41(MARK(U21(isPalListKind(z0), z0, z1)), U21'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNeList(z0)) → c42(MARK(U31(isPalListKind(z0), z0)), U31'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isNeList(__(z0, z1))) → c43(MARK(U41(isPalListKind(z0), z0, z1)), U41'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNeList(__(z0, z1))) → c44(MARK(U51(isPalListKind(z0), z0, z1)), U51'(isPalListKind(z0), z0, z1), ISPALLISTKIND(z0))
ACTIVE(isNePal(z0)) → c45(MARK(U61(isPalListKind(z0), z0)), U61'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c46(MARK(U71(isQid(z0), z0, z1)), U71'(isQid(z0), z0, z1), ISQID(z0))
ACTIVE(isPal(z0)) → c47(MARK(U81(isPalListKind(z0), z0)), U81'(isPalListKind(z0), z0), ISPALLISTKIND(z0))
ACTIVE(isPal(nil)) → c48(MARK(tt))
ACTIVE(isPalListKind(a)) → c49(MARK(tt))
ACTIVE(isPalListKind(e)) → c50(MARK(tt))
ACTIVE(isPalListKind(i)) → c51(MARK(tt))
ACTIVE(isPalListKind(nil)) → c52(MARK(tt))
ACTIVE(isPalListKind(o)) → c53(MARK(tt))
ACTIVE(isPalListKind(u)) → c54(MARK(tt))
ACTIVE(isPalListKind(__(z0, z1))) → c55(MARK(U91(isPalListKind(z0), z1)), U91'(isPalListKind(z0), z1), ISPALLISTKIND(z0))
ACTIVE(isQid(a)) → c56(MARK(tt))
ACTIVE(isQid(e)) → c57(MARK(tt))
ACTIVE(isQid(i)) → c58(MARK(tt))
ACTIVE(isQid(o)) → c59(MARK(tt))
ACTIVE(isQid(u)) → c60(MARK(tt))
MARK(__(z0, z1)) → c61(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(U11(z0, z1)) → c63(ACTIVE(U11(mark(z0), z1)), U11'(mark(z0), z1), MARK(z0))
MARK(U12(z0, z1)) → c65(ACTIVE(U12(mark(z0), z1)), U12'(mark(z0), z1), MARK(z0))
MARK(isPalListKind(z0)) → c66(ACTIVE(isPalListKind(z0)), ISPALLISTKIND(z0))
MARK(U13(z0)) → c67(ACTIVE(U13(mark(z0))), U13'(mark(z0)), MARK(z0))
MARK(isNeList(z0)) → c68(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(U21(z0, z1, z2)) → c69(ACTIVE(U21(mark(z0), z1, z2)), U21'(mark(z0), z1, z2), MARK(z0))
MARK(U22(z0, z1, z2)) → c70(ACTIVE(U22(mark(z0), z1, z2)), U22'(mark(z0), z1, z2), MARK(z0))
MARK(U23(z0, z1, z2)) → c71(ACTIVE(U23(mark(z0), z1, z2)), U23'(mark(z0), z1, z2), MARK(z0))
MARK(U24(z0, z1, z2)) → c72(ACTIVE(U24(mark(z0), z1, z2)), U24'(mark(z0), z1, z2), MARK(z0))
MARK(U25(z0, z1)) → c73(ACTIVE(U25(mark(z0), z1)), U25'(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c74(ACTIVE(isList(z0)), ISLIST(z0))
MARK(U26(z0)) → c75(ACTIVE(U26(mark(z0))), U26'(mark(z0)), MARK(z0))
MARK(U31(z0, z1)) → c76(ACTIVE(U31(mark(z0), z1)), U31'(mark(z0), z1), MARK(z0))
MARK(U32(z0, z1)) → c77(ACTIVE(U32(mark(z0), z1)), U32'(mark(z0), z1), MARK(z0))
MARK(U33(z0)) → c78(ACTIVE(U33(mark(z0))), U33'(mark(z0)), MARK(z0))
MARK(isQid(z0)) → c79(ACTIVE(isQid(z0)), ISQID(z0))
MARK(U41(z0, z1, z2)) → c80(ACTIVE(U41(mark(z0), z1, z2)), U41'(mark(z0), z1, z2), MARK(z0))
MARK(U42(z0, z1, z2)) → c81(ACTIVE(U42(mark(z0), z1, z2)), U42'(mark(z0), z1, z2), MARK(z0))
MARK(U43(z0, z1, z2)) → c82(ACTIVE(U43(mark(z0), z1, z2)), U43'(mark(z0), z1, z2), MARK(z0))
MARK(U44(z0, z1, z2)) → c83(ACTIVE(U44(mark(z0), z1, z2)), U44'(mark(z0), z1, z2), MARK(z0))
MARK(U45(z0, z1)) → c84(ACTIVE(U45(mark(z0), z1)), U45'(mark(z0), z1), MARK(z0))
MARK(U46(z0)) → c85(ACTIVE(U46(mark(z0))), U46'(mark(z0)), MARK(z0))
MARK(U51(z0, z1, z2)) → c86(ACTIVE(U51(mark(z0), z1, z2)), U51'(mark(z0), z1, z2), MARK(z0))
MARK(U52(z0, z1, z2)) → c87(ACTIVE(U52(mark(z0), z1, z2)), U52'(mark(z0), z1, z2), MARK(z0))
MARK(U53(z0, z1, z2)) → c88(ACTIVE(U53(mark(z0), z1, z2)), U53'(mark(z0), z1, z2), MARK(z0))
MARK(U54(z0, z1, z2)) → c89(ACTIVE(U54(mark(z0), z1, z2)), U54'(mark(z0), z1, z2), MARK(z0))
MARK(U55(z0, z1)) → c90(ACTIVE(U55(mark(z0), z1)), U55'(mark(z0), z1), MARK(z0))
MARK(U56(z0)) → c91(ACTIVE(U56(mark(z0))), U56'(mark(z0)), MARK(z0))
MARK(U61(z0, z1)) → c92(ACTIVE(U61(mark(z0), z1)), U61'(mark(z0), z1), MARK(z0))
MARK(U62(z0, z1)) → c93(ACTIVE(U62(mark(z0), z1)), U62'(mark(z0), z1), MARK(z0))
MARK(U63(z0)) → c94(ACTIVE(U63(mark(z0))), U63'(mark(z0)), MARK(z0))
MARK(U71(z0, z1, z2)) → c95(ACTIVE(U71(mark(z0), z1, z2)), U71'(mark(z0), z1, z2), MARK(z0))
MARK(U72(z0, z1)) → c96(ACTIVE(U72(mark(z0), z1)), U72'(mark(z0), z1), MARK(z0))
MARK(U73(z0, z1)) → c97(ACTIVE(U73(mark(z0), z1)), U73'(mark(z0), z1), MARK(z0))
MARK(isPal(z0)) → c98(ACTIVE(isPal(z0)), ISPAL(z0))
MARK(U74(z0)) → c99(ACTIVE(U74(mark(z0))), U74'(mark(z0)), MARK(z0))
MARK(U81(z0, z1)) → c100(ACTIVE(U81(mark(z0), z1)), U81'(mark(z0), z1), MARK(z0))
MARK(U82(z0, z1)) → c101(ACTIVE(U82(mark(z0), z1)), U82'(mark(z0), z1), MARK(z0))
MARK(U83(z0)) → c102(ACTIVE(U83(mark(z0))), U83'(mark(z0)), MARK(z0))
MARK(isNePal(z0)) → c103(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(U91(z0, z1)) → c104(ACTIVE(U91(mark(z0), z1)), U91'(mark(z0), z1), MARK(z0))
MARK(U92(z0)) → c105(ACTIVE(U92(mark(z0))), U92'(mark(z0)), MARK(z0))
__'(mark(z0), z1) → c111(__'(z0, z1))
__'(z0, mark(z1)) → c112(__'(z0, z1))
__'(active(z0), z1) → c113(__'(z0, z1))
__'(z0, active(z1)) → c114(__'(z0, z1))
U11'(mark(z0), z1) → c115(U11'(z0, z1))
U11'(z0, mark(z1)) → c116(U11'(z0, z1))
U11'(active(z0), z1) → c117(U11'(z0, z1))
U11'(z0, active(z1)) → c118(U11'(z0, z1))
U12'(mark(z0), z1) → c119(U12'(z0, z1))
U12'(z0, mark(z1)) → c120(U12'(z0, z1))
U12'(active(z0), z1) → c121(U12'(z0, z1))
U12'(z0, active(z1)) → c122(U12'(z0, z1))
ISPALLISTKIND(mark(z0)) → c123(ISPALLISTKIND(z0))
ISPALLISTKIND(active(z0)) → c124(ISPALLISTKIND(z0))
U13'(mark(z0)) → c125(U13'(z0))
U13'(active(z0)) → c126(U13'(z0))
ISNELIST(mark(z0)) → c127(ISNELIST(z0))
ISNELIST(active(z0)) → c128(ISNELIST(z0))
U21'(mark(z0), z1, z2) → c129(U21'(z0, z1, z2))
U21'(z0, mark(z1), z2) → c130(U21'(z0, z1, z2))
U21'(z0, z1, mark(z2)) → c131(U21'(z0, z1, z2))
U21'(active(z0), z1, z2) → c132(U21'(z0, z1, z2))
U21'(z0, active(z1), z2) → c133(U21'(z0, z1, z2))
U21'(z0, z1, active(z2)) → c134(U21'(z0, z1, z2))
U22'(mark(z0), z1, z2) → c135(U22'(z0, z1, z2))
U22'(z0, mark(z1), z2) → c136(U22'(z0, z1, z2))
U22'(z0, z1, mark(z2)) → c137(U22'(z0, z1, z2))
U22'(active(z0), z1, z2) → c138(U22'(z0, z1, z2))
U22'(z0, active(z1), z2) → c139(U22'(z0, z1, z2))
U22'(z0, z1, active(z2)) → c140(U22'(z0, z1, z2))
U23'(mark(z0), z1, z2) → c141(U23'(z0, z1, z2))
U23'(z0, mark(z1), z2) → c142(U23'(z0, z1, z2))
U23'(z0, z1, mark(z2)) → c143(U23'(z0, z1, z2))
U23'(active(z0), z1, z2) → c144(U23'(z0, z1, z2))
U23'(z0, active(z1), z2) → c145(U23'(z0, z1, z2))
U23'(z0, z1, active(z2)) → c146(U23'(z0, z1, z2))
U24'(mark(z0), z1, z2) → c147(U24'(z0, z1, z2))
U24'(z0, mark(z1), z2) → c148(U24'(z0, z1, z2))
U24'(z0, z1, mark(z2)) → c149(U24'(z0, z1, z2))
U24'(active(z0), z1, z2) → c150(U24'(z0, z1, z2))
U24'(z0, active(z1), z2) → c151(U24'(z0, z1, z2))
U24'(z0, z1, active(z2)) → c152(U24'(z0, z1, z2))
U25'(mark(z0), z1) → c153(U25'(z0, z1))
U25'(z0, mark(z1)) → c154(U25'(z0, z1))
U25'(active(z0), z1) → c155(U25'(z0, z1))
U25'(z0, active(z1)) → c156(U25'(z0, z1))
ISLIST(mark(z0)) → c157(ISLIST(z0))
ISLIST(active(z0)) → c158(ISLIST(z0))
U26'(mark(z0)) → c159(U26'(z0))
U26'(active(z0)) → c160(U26'(z0))
U31'(mark(z0), z1) → c161(U31'(z0, z1))
U31'(z0, mark(z1)) → c162(U31'(z0, z1))
U31'(active(z0), z1) → c163(U31'(z0, z1))
U31'(z0, active(z1)) → c164(U31'(z0, z1))
U32'(mark(z0), z1) → c165(U32'(z0, z1))
U32'(z0, mark(z1)) → c166(U32'(z0, z1))
U32'(active(z0), z1) → c167(U32'(z0, z1))
U32'(z0, active(z1)) → c168(U32'(z0, z1))
U33'(mark(z0)) → c169(U33'(z0))
U33'(active(z0)) → c170(U33'(z0))
ISQID(mark(z0)) → c171(ISQID(z0))
ISQID(active(z0)) → c172(ISQID(z0))
U41'(mark(z0), z1, z2) → c173(U41'(z0, z1, z2))
U41'(z0, mark(z1), z2) → c174(U41'(z0, z1, z2))
U41'(z0, z1, mark(z2)) → c175(U41'(z0, z1, z2))
U41'(active(z0), z1, z2) → c176(U41'(z0, z1, z2))
U41'(z0, active(z1), z2) → c177(U41'(z0, z1, z2))
U41'(z0, z1, active(z2)) → c178(U41'(z0, z1, z2))
U42'(mark(z0), z1, z2) → c179(U42'(z0, z1, z2))
U42'(z0, mark(z1), z2) → c180(U42'(z0, z1, z2))
U42'(z0, z1, mark(z2)) → c181(U42'(z0, z1, z2))
U42'(active(z0), z1, z2) → c182(U42'(z0, z1, z2))
U42'(z0, active(z1), z2) → c183(U42'(z0, z1, z2))
U42'(z0, z1, active(z2)) → c184(U42'(z0, z1, z2))
U43'(mark(z0), z1, z2) → c185(U43'(z0, z1, z2))
U43'(z0, mark(z1), z2) → c186(U43'(z0, z1, z2))
U43'(z0, z1, mark(z2)) → c187(U43'(z0, z1, z2))
U43'(active(z0), z1, z2) → c188(U43'(z0, z1, z2))
U43'(z0, active(z1), z2) → c189(U43'(z0, z1, z2))
U43'(z0, z1, active(z2)) → c190(U43'(z0, z1, z2))
U44'(mark(z0), z1, z2) → c191(U44'(z0, z1, z2))
U44'(z0, mark(z1), z2) → c192(U44'(z0, z1, z2))
U44'(z0, z1, mark(z2)) → c193(U44'(z0, z1, z2))
U44'(active(z0), z1, z2) → c194(U44'(z0, z1, z2))
U44'(z0, active(z1), z2) → c195(U44'(z0, z1, z2))
U44'(z0, z1, active(z2)) → c196(U44'(z0, z1, z2))
U45'(mark(z0), z1) → c197(U45'(z0, z1))
U45'(z0, mark(z1)) → c198(U45'(z0, z1))
U45'(active(z0), z1) → c199(U45'(z0, z1))
U45'(z0, active(z1)) → c200(U45'(z0, z1))
U46'(mark(z0)) → c201(U46'(z0))
U46'(active(z0)) → c202(U46'(z0))
U51'(mark(z0), z1, z2) → c203(U51'(z0, z1, z2))
U51'(z0, mark(z1), z2) → c204(U51'(z0, z1, z2))
U51'(z0, z1, mark(z2)) → c205(U51'(z0, z1, z2))
U51'(active(z0), z1, z2) → c206(U51'(z0, z1, z2))
U51'(z0, active(z1), z2) → c207(U51'(z0, z1, z2))
U51'(z0, z1, active(z2)) → c208(U51'(z0, z1, z2))
U52'(mark(z0), z1, z2) → c209(U52'(z0, z1, z2))
U52'(z0, mark(z1), z2) → c210(U52'(z0, z1, z2))
U52'(z0, z1, mark(z2)) → c211(U52'(z0, z1, z2))
U52'(active(z0), z1, z2) → c212(U52'(z0, z1, z2))
U52'(z0, active(z1), z2) → c213(U52'(z0, z1, z2))
U52'(z0, z1, active(z2)) → c214(U52'(z0, z1, z2))
U53'(mark(z0), z1, z2) → c215(U53'(z0, z1, z2))
U53'(z0, mark(z1), z2) → c216(U53'(z0, z1, z2))
U53'(z0, z1, mark(z2)) → c217(U53'(z0, z1, z2))
U53'(active(z0), z1, z2) → c218(U53'(z0, z1, z2))
U53'(z0, active(z1), z2) → c219(U53'(z0, z1, z2))
U53'(z0, z1, active(z2)) → c220(U53'(z0, z1, z2))
U54'(mark(z0), z1, z2) → c221(U54'(z0, z1, z2))
U54'(z0, mark(z1), z2) → c222(U54'(z0, z1, z2))
U54'(z0, z1, mark(z2)) → c223(U54'(z0, z1, z2))
U54'(active(z0), z1, z2) → c224(U54'(z0, z1, z2))
U54'(z0, active(z1), z2) → c225(U54'(z0, z1, z2))
U54'(z0, z1, active(z2)) → c226(U54'(z0, z1, z2))
U55'(mark(z0), z1) → c227(U55'(z0, z1))
U55'(z0, mark(z1)) → c228(U55'(z0, z1))
U55'(active(z0), z1) → c229(U55'(z0, z1))
U55'(z0, active(z1)) → c230(U55'(z0, z1))
U56'(mark(z0)) → c231(U56'(z0))
U56'(active(z0)) → c232(U56'(z0))
U61'(mark(z0), z1) → c233(U61'(z0, z1))
U61'(z0, mark(z1)) → c234(U61'(z0, z1))
U61'(active(z0), z1) → c235(U61'(z0, z1))
U61'(z0, active(z1)) → c236(U61'(z0, z1))
U62'(mark(z0), z1) → c237(U62'(z0, z1))
U62'(z0, mark(z1)) → c238(U62'(z0, z1))
U62'(active(z0), z1) → c239(U62'(z0, z1))
U62'(z0, active(z1)) → c240(U62'(z0, z1))
U63'(mark(z0)) → c241(U63'(z0))
U63'(active(z0)) → c242(U63'(z0))
U71'(mark(z0), z1, z2) → c243(U71'(z0, z1, z2))
U71'(z0, mark(z1), z2) → c244(U71'(z0, z1, z2))
U71'(z0, z1, mark(z2)) → c245(U71'(z0, z1, z2))
U71'(active(z0), z1, z2) → c246(U71'(z0, z1, z2))
U71'(z0, active(z1), z2) → c247(U71'(z0, z1, z2))
U71'(z0, z1, active(z2)) → c248(U71'(z0, z1, z2))
U72'(mark(z0), z1) → c249(U72'(z0, z1))
U72'(z0, mark(z1)) → c250(U72'(z0, z1))
U72'(active(z0), z1) → c251(U72'(z0, z1))
U72'(z0, active(z1)) → c252(U72'(z0, z1))
U73'(mark(z0), z1) → c253(U73'(z0, z1))
U73'(z0, mark(z1)) → c254(U73'(z0, z1))
U73'(active(z0), z1) → c255(U73'(z0, z1))
U73'(z0, active(z1)) → c256(U73'(z0, z1))
ISPAL(mark(z0)) → c257(ISPAL(z0))
ISPAL(active(z0)) → c258(ISPAL(z0))
U74'(mark(z0)) → c259(U74'(z0))
U74'(active(z0)) → c260(U74'(z0))
U81'(mark(z0), z1) → c261(U81'(z0, z1))
U81'(z0, mark(z1)) → c262(U81'(z0, z1))
U81'(active(z0), z1) → c263(U81'(z0, z1))
U81'(z0, active(z1)) → c264(U81'(z0, z1))
U82'(mark(z0), z1) → c265(U82'(z0, z1))
U82'(z0, mark(z1)) → c266(U82'(z0, z1))
U82'(active(z0), z1) → c267(U82'(z0, z1))
U82'(z0, active(z1)) → c268(U82'(z0, z1))
U83'(mark(z0)) → c269(U83'(z0))
U83'(active(z0)) → c270(U83'(z0))
ISNEPAL(mark(z0)) → c271(ISNEPAL(z0))
ISNEPAL(active(z0)) → c272(ISNEPAL(z0))
U91'(mark(z0), z1) → c273(U91'(z0, z1))
U91'(z0, mark(z1)) → c274(U91'(z0, z1))
U91'(active(z0), z1) → c275(U91'(z0, z1))
U91'(z0, active(z1)) → c276(U91'(z0, z1))
U92'(mark(z0)) → c277(U92'(z0))
U92'(active(z0)) → c278(U92'(z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(U11(tt, z0)) → mark(U12(isPalListKind(z0), z0))
active(U12(tt, z0)) → mark(U13(isNeList(z0)))
active(U13(tt)) → mark(tt)
active(U21(tt, z0, z1)) → mark(U22(isPalListKind(z0), z0, z1))
active(U22(tt, z0, z1)) → mark(U23(isPalListKind(z1), z0, z1))
active(U23(tt, z0, z1)) → mark(U24(isPalListKind(z1), z0, z1))
active(U24(tt, z0, z1)) → mark(U25(isList(z0), z1))
active(U25(tt, z0)) → mark(U26(isList(z0)))
active(U26(tt)) → mark(tt)
active(U31(tt, z0)) → mark(U32(isPalListKind(z0), z0))
active(U32(tt, z0)) → mark(U33(isQid(z0)))
active(U33(tt)) → mark(tt)
active(U41(tt, z0, z1)) → mark(U42(isPalListKind(z0), z0, z1))
active(U42(tt, z0, z1)) → mark(U43(isPalListKind(z1), z0, z1))
active(U43(tt, z0, z1)) → mark(U44(isPalListKind(z1), z0, z1))
active(U44(tt, z0, z1)) → mark(U45(isList(z0), z1))
active(U45(tt, z0)) → mark(U46(isNeList(z0)))
active(U46(tt)) → mark(tt)
active(U51(tt, z0, z1)) → mark(U52(isPalListKind(z0), z0, z1))
active(U52(tt, z0, z1)) → mark(U53(isPalListKind(z1), z0, z1))
active(U53(tt, z0, z1)) → mark(U54(isPalListKind(z1), z0, z1))
active(U54(tt, z0, z1)) → mark(U55(isNeList(z0), z1))
active(U55(tt, z0)) → mark(U56(isList(z0)))
active(U56(tt)) → mark(tt)
active(U61(tt, z0)) → mark(U62(isPalListKind(z0), z0))
active(U62(tt, z0)) → mark(U63(isQid(z0)))
active(U63(tt)) → mark(tt)
active(U71(tt, z0, z1)) → mark(U72(isPalListKind(z0), z1))
active(U72(tt, z0)) → mark(U73(isPal(z0), z0))
active(U73(tt, z0)) → mark(U74(isPalListKind(z0)))
active(U74(tt)) → mark(tt)
active(U81(tt, z0)) → mark(U82(isPalListKind(z0), z0))
active(U82(tt, z0)) → mark(U83(isNePal(z0)))
active(U83(tt)) → mark(tt)
active(U91(tt, z0)) → mark(U92(isPalListKind(z0)))
active(U92(tt)) → mark(tt)
active(isList(z0)) → mark(U11(isPalListKind(z0), z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(U21(isPalListKind(z0), z0, z1))
active(isNeList(z0)) → mark(U31(isPalListKind(z0), z0))
active(isNeList(__(z0, z1))) → mark(U41(isPalListKind(z0), z0, z1))
active(isNeList(__(z0, z1))) → mark(U51(isPalListKind(z0), z0, z1))
active(isNePal(z0)) → mark(U61(isPalListKind(z0), z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(U71(isQid(z0), z0, z1))
active(isPal(z0)) → mark(U81(isPalListKind(z0), z0))
active(isPal(nil)) → mark(tt)
active(isPalListKind(a)) → mark(tt)
active(isPalListKind(e)) → mark(tt)
active(isPalListKind(i)) → mark(tt)
active(isPalListKind(nil)) → mark(tt)
active(isPalListKind(o)) → mark(tt)
active(isPalListKind(u)) → mark(tt)
active(isPalListKind(__(z0, z1))) → mark(U91(isPalListKind(z0), z1))
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(U11(z0, z1)) → active(U11(mark(z0), z1))
mark(tt) → active(tt)
mark(U12(z0, z1)) → active(U12(mark(z0), z1))
mark(isPalListKind(z0)) → active(isPalListKind(z0))
mark(U13(z0)) → active(U13(mark(z0)))
mark(isNeList(z0)) → active(isNeList(z0))
mark(U21(z0, z1, z2)) → active(U21(mark(z0), z1, z2))
mark(U22(z0, z1, z2)) → active(U22(mark(z0), z1, z2))
mark(U23(z0, z1, z2)) → active(U23(mark(z0), z1, z2))
mark(U24(z0, z1, z2)) → active(U24(mark(z0), z1, z2))
mark(U25(z0, z1)) → active(U25(mark(z0), z1))
mark(isList(z0)) → active(isList(z0))
mark(U26(z0)) → active(U26(mark(z0)))
mark(U31(z0, z1)) → active(U31(mark(z0), z1))
mark(U32(z0, z1)) → active(U32(mark(z0), z1))
mark(U33(z0)) → active(U33(mark(z0)))
mark(isQid(z0)) → active(isQid(z0))
mark(U41(z0, z1, z2)) → active(U41(mark(z0), z1, z2))
mark(U42(z0, z1, z2)) → active(U42(mark(z0), z1, z2))
mark(U43(z0, z1, z2)) → active(U43(mark(z0), z1, z2))
mark(U44(z0, z1, z2)) → active(U44(mark(z0), z1, z2))
mark(U45(z0, z1)) → active(U45(mark(z0), z1))
mark(U46(z0)) → active(U46(mark(z0)))
mark(U51(z0, z1, z2)) → active(U51(mark(z0), z1, z2))
mark(U52(z0, z1, z2)) → active(U52(mark(z0), z1, z2))
mark(U53(z0, z1, z2)) → active(U53(mark(z0), z1, z2))
mark(U54(z0, z1, z2)) → active(U54(mark(z0), z1, z2))
mark(U55(z0, z1)) → active(U55(mark(z0), z1))
mark(U56(z0)) → active(U56(mark(z0)))
mark(U61(z0, z1)) → active(U61(mark(z0), z1))
mark(U62(z0, z1)) → active(U62(mark(z0), z1))
mark(U63(z0)) → active(U63(mark(z0)))
mark(U71(z0, z1, z2)) → active(U71(mark(z0), z1, z2))
mark(U72(z0, z1)) → active(U72(mark(z0), z1))
mark(U73(z0, z1)) → active(U73(mark(z0), z1))
mark(isPal(z0)) → active(isPal(z0))
mark(U74(z0)) → active(U74(mark(z0)))
mark(U81(z0, z1)) → active(U81(mark(z0), z1))
mark(U82(z0, z1)) → active(U82(mark(z0), z1))
mark(U83(z0)) → active(U83(mark(z0)))
mark(isNePal(z0)) → active(isNePal(z0))
mark(U91(z0, z1)) → active(U91(mark(z0), z1))
mark(U92(z0)) → active(U92(mark(z0)))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
U11(mark(z0), z1) → U11(z0, z1)
U11(z0, mark(z1)) → U11(z0, z1)
U11(active(z0), z1) → U11(z0, z1)
U11(z0, active(z1)) → U11(z0, z1)
U12(mark(z0), z1) → U12(z0, z1)
U12(z0, mark(z1)) → U12(z0, z1)
U12(active(z0), z1) → U12(z0, z1)
U12(z0, active(z1)) → U12(z0, z1)
isPalListKind(mark(z0)) → isPalListKind(z0)
isPalListKind(active(z0)) → isPalListKind(z0)
U13(mark(z0)) → U13(z0)
U13(active(z0)) → U13(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
U21(mark(z0), z1, z2) → U21(z0, z1, z2)
U21(z0, mark(z1), z2) → U21(z0, z1, z2)
U21(z0, z1, mark(z2)) → U21(z0, z1, z2)
U21(active(z0), z1, z2) → U21(z0, z1, z2)
U21(z0, active(z1), z2) → U21(z0, z1, z2)
U21(z0, z1, active(z2)) → U21(z0, z1, z2)
U22(mark(z0), z1, z2) → U22(z0, z1, z2)
U22(z0, mark(z1), z2) → U22(z0, z1, z2)
U22(z0, z1, mark(z2)) → U22(z0, z1, z2)
U22(active(z0), z1, z2) → U22(z0, z1, z2)
U22(z0, active(z1), z2) → U22(z0, z1, z2)
U22(z0, z1, active(z2)) → U22(z0, z1, z2)
U23(mark(z0), z1, z2) → U23(z0, z1, z2)
U23(z0, mark(z1), z2) → U23(z0, z1, z2)
U23(z0, z1, mark(z2)) → U23(z0, z1, z2)
U23(active(z0), z1, z2) → U23(z0, z1, z2)
U23(z0, active(z1), z2) → U23(z0, z1, z2)
U23(z0, z1, active(z2)) → U23(z0, z1, z2)
U24(mark(z0), z1, z2) → U24(z0, z1, z2)
U24(z0, mark(z1), z2) → U24(z0, z1, z2)
U24(z0, z1, mark(z2)) → U24(z0, z1, z2)
U24(active(z0), z1, z2) → U24(z0, z1, z2)
U24(z0, active(z1), z2) → U24(z0, z1, z2)
U24(z0, z1, active(z2)) → U24(z0, z1, z2)
U25(mark(z0), z1) → U25(z0, z1)
U25(z0, mark(z1)) → U25(z0, z1)
U25(active(z0), z1) → U25(z0, z1)
U25(z0, active(z1)) → U25(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
U26(mark(z0)) → U26(z0)
U26(active(z0)) → U26(z0)
U31(mark(z0), z1) → U31(z0, z1)
U31(z0, mark(z1)) → U31(z0, z1)
U31(active(z0), z1) → U31(z0, z1)
U31(z0, active(z1)) → U31(z0, z1)
U32(mark(z0), z1) → U32(z0, z1)
U32(z0, mark(z1)) → U32(z0, z1)
U32(active(z0), z1) → U32(z0, z1)
U32(z0, active(z1)) → U32(z0, z1)
U33(mark(z0)) → U33(z0)
U33(active(z0)) → U33(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
U41(mark(z0), z1, z2) → U41(z0, z1, z2)
U41(z0, mark(z1), z2) → U41(z0, z1, z2)
U41(z0, z1, mark(z2)) → U41(z0, z1, z2)
U41(active(z0), z1, z2) → U41(z0, z1, z2)
U41(z0, active(z1), z2) → U41(z0, z1, z2)
U41(z0, z1, active(z2)) → U41(z0, z1, z2)
U42(mark(z0), z1, z2) → U42(z0, z1, z2)
U42(z0, mark(z1), z2) → U42(z0, z1, z2)
U42(z0, z1, mark(z2)) → U42(z0, z1, z2)
U42(active(z0), z1, z2) → U42(z0, z1, z2)
U42(z0, active(z1), z2) → U42(z0, z1, z2)
U42(z0, z1, active(z2)) → U42(z0, z1, z2)
U43(mark(z0), z1, z2) → U43(z0, z1, z2)
U43(z0, mark(z1), z2) → U43(z0, z1, z2)
U43(z0, z1, mark(z2)) → U43(z0, z1, z2)
U43(active(z0), z1, z2) → U43(z0, z1, z2)
U43(z0, active(z1), z2) → U43(z0, z1, z2)
U43(z0, z1, active(z2)) → U43(z0, z1, z2)
U44(mark(z0), z1, z2) → U44(z0, z1, z2)
U44(z0, mark(z1), z2) → U44(z0, z1, z2)
U44(z0, z1, mark(z2)) → U44(z0, z1, z2)
U44(active(z0), z1, z2) → U44(z0, z1, z2)
U44(z0, active(z1), z2) → U44(z0, z1, z2)
U44(z0, z1, active(z2)) → U44(z0, z1, z2)
U45(mark(z0), z1) → U45(z0, z1)
U45(z0, mark(z1)) → U45(z0, z1)
U45(active(z0), z1) → U45(z0, z1)
U45(z0, active(z1)) → U45(z0, z1)
U46(mark(z0)) → U46(z0)
U46(active(z0)) → U46(z0)
U51(mark(z0), z1, z2) → U51(z0, z1, z2)
U51(z0, mark(z1), z2) → U51(z0, z1, z2)
U51(z0, z1, mark(z2)) → U51(z0, z1, z2)
U51(active(z0), z1, z2) → U51(z0, z1, z2)
U51(z0, active(z1), z2) → U51(z0, z1, z2)
U51(z0, z1, active(z2)) → U51(z0, z1, z2)
U52(mark(z0), z1, z2) → U52(z0, z1, z2)
U52(z0, mark(z1), z2) → U52(z0, z1, z2)
U52(z0, z1, mark(z2)) → U52(z0, z1, z2)
U52(active(z0), z1, z2) → U52(z0, z1, z2)
U52(z0, active(z1), z2) → U52(z0, z1, z2)
U52(z0, z1, active(z2)) → U52(z0, z1, z2)
U53(mark(z0), z1, z2) → U53(z0, z1, z2)
U53(z0, mark(z1), z2) → U53(z0, z1, z2)
U53(z0, z1, mark(z2)) → U53(z0, z1, z2)
U53(active(z0), z1, z2) → U53(z0, z1, z2)
U53(z0, active(z1), z2) → U53(z0, z1, z2)
U53(z0, z1, active(z2)) → U53(z0, z1, z2)
U54(mark(z0), z1, z2) → U54(z0, z1, z2)
U54(z0, mark(z1), z2) → U54(z0, z1, z2)
U54(z0, z1, mark(z2)) → U54(z0, z1, z2)
U54(active(z0), z1, z2) → U54(z0, z1, z2)
U54(z0, active(z1), z2) → U54(z0, z1, z2)
U54(z0, z1, active(z2)) → U54(z0, z1, z2)
U55(mark(z0), z1) → U55(z0, z1)
U55(z0, mark(z1)) → U55(z0, z1)
U55(active(z0), z1) → U55(z0, z1)
U55(z0, active(z1)) → U55(z0, z1)
U56(mark(z0)) → U56(z0)
U56(active(z0)) → U56(z0)
U61(mark(z0), z1) → U61(z0, z1)
U61(z0, mark(z1)) → U61(z0, z1)
U61(active(z0), z1) → U61(z0, z1)
U61(z0, active(z1)) → U61(z0, z1)
U62(mark(z0), z1) → U62(z0, z1)
U62(z0, mark(z1)) → U62(z0, z1)
U62(active(z0), z1) → U62(z0, z1)
U62(z0, active(z1)) → U62(z0, z1)
U63(mark(z0)) → U63(z0)
U63(active(z0)) → U63(z0)
U71(mark(z0), z1, z2) → U71(z0, z1, z2)
U71(z0, mark(z1), z2) → U71(z0, z1, z2)
U71(z0, z1, mark(z2)) → U71(z0, z1, z2)
U71(active(z0), z1, z2) → U71(z0, z1, z2)
U71(z0, active(z1), z2) → U71(z0, z1, z2)
U71(z0, z1, active(z2)) → U71(z0, z1, z2)
U72(mark(z0), z1) → U72(z0, z1)
U72(z0, mark(z1)) → U72(z0, z1)
U72(active(z0), z1) → U72(z0, z1)
U72(z0, active(z1)) → U72(z0, z1)
U73(mark(z0), z1) → U73(z0, z1)
U73(z0, mark(z1)) → U73(z0, z1)
U73(active(z0), z1) → U73(z0, z1)
U73(z0, active(z1)) → U73(z0, z1)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)
U74(mark(z0)) → U74(z0)
U74(active(z0)) → U74(z0)
U81(mark(z0), z1) → U81(z0, z1)
U81(z0, mark(z1)) → U81(z0, z1)
U81(active(z0), z1) → U81(z0, z1)
U81(z0, active(z1)) → U81(z0, z1)
U82(mark(z0), z1) → U82(z0, z1)
U82(z0, mark(z1)) → U82(z0, z1)
U82(active(z0), z1) → U82(z0, z1)
U82(z0, active(z1)) → U82(z0, z1)
U83(mark(z0)) → U83(z0)
U83(active(z0)) → U83(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
U91(mark(z0), z1) → U91(z0, z1)
U91(z0, mark(z1)) → U91(z0, z1)
U91(active(z0), z1) → U91(z0, z1)
U91(z0, active(z1)) → U91(z0, z1)
U92(mark(z0)) → U92(z0)
U92(active(z0)) → U92(z0)

Tuples:

MARK(nil) → c62(ACTIVE(nil))
MARK(tt) → c64(ACTIVE(tt))
MARK(a) → c106(ACTIVE(a))
MARK(e) → c107(ACTIVE(e))
MARK(i) → c108(ACTIVE(i))
MARK(o) → c109(ACTIVE(o))
MARK(u) → c110(ACTIVE(u))

S tuples:

MARK(nil) → c62(ACTIVE(nil))
MARK(tt) → c64(ACTIVE(tt))
MARK(a) → c106(ACTIVE(a))
MARK(e) → c107(ACTIVE(e))
MARK(i) → c108(ACTIVE(i))
MARK(o) → c109(ACTIVE(o))
MARK(u) → c110(ACTIVE(u))

K tuples:none
Defined Rule Symbols:

active, mark, __, U11, U12, isPalListKind, U13, isNeList, U21, U22, U23, U24, U25, isList, U26, U31, U32, U33, isQid, U41, U42, U43, U44, U45, U46, U51, U52, U53, U54, U55, U56, U61, U62, U63, U71, U72, U73, isPal, U74, U81, U82, U83, isNePal, U91, U92

Defined Pair Symbols:

MARK

Compound Symbols:

c62, c64, c106, c107, c108, c109, c110

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 7 trailing nodes:

MARK(nil) → c62(ACTIVE(nil))
MARK(tt) → c64(ACTIVE(tt))
MARK(o) → c109(ACTIVE(o))
MARK(e) → c107(ACTIVE(e))
MARK(u) → c110(ACTIVE(u))
MARK(a) → c106(ACTIVE(a))
MARK(i) → c108(ACTIVE(i))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(U11(tt, z0)) → mark(U12(isPalListKind(z0), z0))
active(U12(tt, z0)) → mark(U13(isNeList(z0)))
active(U13(tt)) → mark(tt)
active(U21(tt, z0, z1)) → mark(U22(isPalListKind(z0), z0, z1))
active(U22(tt, z0, z1)) → mark(U23(isPalListKind(z1), z0, z1))
active(U23(tt, z0, z1)) → mark(U24(isPalListKind(z1), z0, z1))
active(U24(tt, z0, z1)) → mark(U25(isList(z0), z1))
active(U25(tt, z0)) → mark(U26(isList(z0)))
active(U26(tt)) → mark(tt)
active(U31(tt, z0)) → mark(U32(isPalListKind(z0), z0))
active(U32(tt, z0)) → mark(U33(isQid(z0)))
active(U33(tt)) → mark(tt)
active(U41(tt, z0, z1)) → mark(U42(isPalListKind(z0), z0, z1))
active(U42(tt, z0, z1)) → mark(U43(isPalListKind(z1), z0, z1))
active(U43(tt, z0, z1)) → mark(U44(isPalListKind(z1), z0, z1))
active(U44(tt, z0, z1)) → mark(U45(isList(z0), z1))
active(U45(tt, z0)) → mark(U46(isNeList(z0)))
active(U46(tt)) → mark(tt)
active(U51(tt, z0, z1)) → mark(U52(isPalListKind(z0), z0, z1))
active(U52(tt, z0, z1)) → mark(U53(isPalListKind(z1), z0, z1))
active(U53(tt, z0, z1)) → mark(U54(isPalListKind(z1), z0, z1))
active(U54(tt, z0, z1)) → mark(U55(isNeList(z0), z1))
active(U55(tt, z0)) → mark(U56(isList(z0)))
active(U56(tt)) → mark(tt)
active(U61(tt, z0)) → mark(U62(isPalListKind(z0), z0))
active(U62(tt, z0)) → mark(U63(isQid(z0)))
active(U63(tt)) → mark(tt)
active(U71(tt, z0, z1)) → mark(U72(isPalListKind(z0), z1))
active(U72(tt, z0)) → mark(U73(isPal(z0), z0))
active(U73(tt, z0)) → mark(U74(isPalListKind(z0)))
active(U74(tt)) → mark(tt)
active(U81(tt, z0)) → mark(U82(isPalListKind(z0), z0))
active(U82(tt, z0)) → mark(U83(isNePal(z0)))
active(U83(tt)) → mark(tt)
active(U91(tt, z0)) → mark(U92(isPalListKind(z0)))
active(U92(tt)) → mark(tt)
active(isList(z0)) → mark(U11(isPalListKind(z0), z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(U21(isPalListKind(z0), z0, z1))
active(isNeList(z0)) → mark(U31(isPalListKind(z0), z0))
active(isNeList(__(z0, z1))) → mark(U41(isPalListKind(z0), z0, z1))
active(isNeList(__(z0, z1))) → mark(U51(isPalListKind(z0), z0, z1))
active(isNePal(z0)) → mark(U61(isPalListKind(z0), z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(U71(isQid(z0), z0, z1))
active(isPal(z0)) → mark(U81(isPalListKind(z0), z0))
active(isPal(nil)) → mark(tt)
active(isPalListKind(a)) → mark(tt)
active(isPalListKind(e)) → mark(tt)
active(isPalListKind(i)) → mark(tt)
active(isPalListKind(nil)) → mark(tt)
active(isPalListKind(o)) → mark(tt)
active(isPalListKind(u)) → mark(tt)
active(isPalListKind(__(z0, z1))) → mark(U91(isPalListKind(z0), z1))
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(U11(z0, z1)) → active(U11(mark(z0), z1))
mark(tt) → active(tt)
mark(U12(z0, z1)) → active(U12(mark(z0), z1))
mark(isPalListKind(z0)) → active(isPalListKind(z0))
mark(U13(z0)) → active(U13(mark(z0)))
mark(isNeList(z0)) → active(isNeList(z0))
mark(U21(z0, z1, z2)) → active(U21(mark(z0), z1, z2))
mark(U22(z0, z1, z2)) → active(U22(mark(z0), z1, z2))
mark(U23(z0, z1, z2)) → active(U23(mark(z0), z1, z2))
mark(U24(z0, z1, z2)) → active(U24(mark(z0), z1, z2))
mark(U25(z0, z1)) → active(U25(mark(z0), z1))
mark(isList(z0)) → active(isList(z0))
mark(U26(z0)) → active(U26(mark(z0)))
mark(U31(z0, z1)) → active(U31(mark(z0), z1))
mark(U32(z0, z1)) → active(U32(mark(z0), z1))
mark(U33(z0)) → active(U33(mark(z0)))
mark(isQid(z0)) → active(isQid(z0))
mark(U41(z0, z1, z2)) → active(U41(mark(z0), z1, z2))
mark(U42(z0, z1, z2)) → active(U42(mark(z0), z1, z2))
mark(U43(z0, z1, z2)) → active(U43(mark(z0), z1, z2))
mark(U44(z0, z1, z2)) → active(U44(mark(z0), z1, z2))
mark(U45(z0, z1)) → active(U45(mark(z0), z1))
mark(U46(z0)) → active(U46(mark(z0)))
mark(U51(z0, z1, z2)) → active(U51(mark(z0), z1, z2))
mark(U52(z0, z1, z2)) → active(U52(mark(z0), z1, z2))
mark(U53(z0, z1, z2)) → active(U53(mark(z0), z1, z2))
mark(U54(z0, z1, z2)) → active(U54(mark(z0), z1, z2))
mark(U55(z0, z1)) → active(U55(mark(z0), z1))
mark(U56(z0)) → active(U56(mark(z0)))
mark(U61(z0, z1)) → active(U61(mark(z0), z1))
mark(U62(z0, z1)) → active(U62(mark(z0), z1))
mark(U63(z0)) → active(U63(mark(z0)))
mark(U71(z0, z1, z2)) → active(U71(mark(z0), z1, z2))
mark(U72(z0, z1)) → active(U72(mark(z0), z1))
mark(U73(z0, z1)) → active(U73(mark(z0), z1))
mark(isPal(z0)) → active(isPal(z0))
mark(U74(z0)) → active(U74(mark(z0)))
mark(U81(z0, z1)) → active(U81(mark(z0), z1))
mark(U82(z0, z1)) → active(U82(mark(z0), z1))
mark(U83(z0)) → active(U83(mark(z0)))
mark(isNePal(z0)) → active(isNePal(z0))
mark(U91(z0, z1)) → active(U91(mark(z0), z1))
mark(U92(z0)) → active(U92(mark(z0)))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
U11(mark(z0), z1) → U11(z0, z1)
U11(z0, mark(z1)) → U11(z0, z1)
U11(active(z0), z1) → U11(z0, z1)
U11(z0, active(z1)) → U11(z0, z1)
U12(mark(z0), z1) → U12(z0, z1)
U12(z0, mark(z1)) → U12(z0, z1)
U12(active(z0), z1) → U12(z0, z1)
U12(z0, active(z1)) → U12(z0, z1)
isPalListKind(mark(z0)) → isPalListKind(z0)
isPalListKind(active(z0)) → isPalListKind(z0)
U13(mark(z0)) → U13(z0)
U13(active(z0)) → U13(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
U21(mark(z0), z1, z2) → U21(z0, z1, z2)
U21(z0, mark(z1), z2) → U21(z0, z1, z2)
U21(z0, z1, mark(z2)) → U21(z0, z1, z2)
U21(active(z0), z1, z2) → U21(z0, z1, z2)
U21(z0, active(z1), z2) → U21(z0, z1, z2)
U21(z0, z1, active(z2)) → U21(z0, z1, z2)
U22(mark(z0), z1, z2) → U22(z0, z1, z2)
U22(z0, mark(z1), z2) → U22(z0, z1, z2)
U22(z0, z1, mark(z2)) → U22(z0, z1, z2)
U22(active(z0), z1, z2) → U22(z0, z1, z2)
U22(z0, active(z1), z2) → U22(z0, z1, z2)
U22(z0, z1, active(z2)) → U22(z0, z1, z2)
U23(mark(z0), z1, z2) → U23(z0, z1, z2)
U23(z0, mark(z1), z2) → U23(z0, z1, z2)
U23(z0, z1, mark(z2)) → U23(z0, z1, z2)
U23(active(z0), z1, z2) → U23(z0, z1, z2)
U23(z0, active(z1), z2) → U23(z0, z1, z2)
U23(z0, z1, active(z2)) → U23(z0, z1, z2)
U24(mark(z0), z1, z2) → U24(z0, z1, z2)
U24(z0, mark(z1), z2) → U24(z0, z1, z2)
U24(z0, z1, mark(z2)) → U24(z0, z1, z2)
U24(active(z0), z1, z2) → U24(z0, z1, z2)
U24(z0, active(z1), z2) → U24(z0, z1, z2)
U24(z0, z1, active(z2)) → U24(z0, z1, z2)
U25(mark(z0), z1) → U25(z0, z1)
U25(z0, mark(z1)) → U25(z0, z1)
U25(active(z0), z1) → U25(z0, z1)
U25(z0, active(z1)) → U25(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
U26(mark(z0)) → U26(z0)
U26(active(z0)) → U26(z0)
U31(mark(z0), z1) → U31(z0, z1)
U31(z0, mark(z1)) → U31(z0, z1)
U31(active(z0), z1) → U31(z0, z1)
U31(z0, active(z1)) → U31(z0, z1)
U32(mark(z0), z1) → U32(z0, z1)
U32(z0, mark(z1)) → U32(z0, z1)
U32(active(z0), z1) → U32(z0, z1)
U32(z0, active(z1)) → U32(z0, z1)
U33(mark(z0)) → U33(z0)
U33(active(z0)) → U33(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
U41(mark(z0), z1, z2) → U41(z0, z1, z2)
U41(z0, mark(z1), z2) → U41(z0, z1, z2)
U41(z0, z1, mark(z2)) → U41(z0, z1, z2)
U41(active(z0), z1, z2) → U41(z0, z1, z2)
U41(z0, active(z1), z2) → U41(z0, z1, z2)
U41(z0, z1, active(z2)) → U41(z0, z1, z2)
U42(mark(z0), z1, z2) → U42(z0, z1, z2)
U42(z0, mark(z1), z2) → U42(z0, z1, z2)
U42(z0, z1, mark(z2)) → U42(z0, z1, z2)
U42(active(z0), z1, z2) → U42(z0, z1, z2)
U42(z0, active(z1), z2) → U42(z0, z1, z2)
U42(z0, z1, active(z2)) → U42(z0, z1, z2)
U43(mark(z0), z1, z2) → U43(z0, z1, z2)
U43(z0, mark(z1), z2) → U43(z0, z1, z2)
U43(z0, z1, mark(z2)) → U43(z0, z1, z2)
U43(active(z0), z1, z2) → U43(z0, z1, z2)
U43(z0, active(z1), z2) → U43(z0, z1, z2)
U43(z0, z1, active(z2)) → U43(z0, z1, z2)
U44(mark(z0), z1, z2) → U44(z0, z1, z2)
U44(z0, mark(z1), z2) → U44(z0, z1, z2)
U44(z0, z1, mark(z2)) → U44(z0, z1, z2)
U44(active(z0), z1, z2) → U44(z0, z1, z2)
U44(z0, active(z1), z2) → U44(z0, z1, z2)
U44(z0, z1, active(z2)) → U44(z0, z1, z2)
U45(mark(z0), z1) → U45(z0, z1)
U45(z0, mark(z1)) → U45(z0, z1)
U45(active(z0), z1) → U45(z0, z1)
U45(z0, active(z1)) → U45(z0, z1)
U46(mark(z0)) → U46(z0)
U46(active(z0)) → U46(z0)
U51(mark(z0), z1, z2) → U51(z0, z1, z2)
U51(z0, mark(z1), z2) → U51(z0, z1, z2)
U51(z0, z1, mark(z2)) → U51(z0, z1, z2)
U51(active(z0), z1, z2) → U51(z0, z1, z2)
U51(z0, active(z1), z2) → U51(z0, z1, z2)
U51(z0, z1, active(z2)) → U51(z0, z1, z2)
U52(mark(z0), z1, z2) → U52(z0, z1, z2)
U52(z0, mark(z1), z2) → U52(z0, z1, z2)
U52(z0, z1, mark(z2)) → U52(z0, z1, z2)
U52(active(z0), z1, z2) → U52(z0, z1, z2)
U52(z0, active(z1), z2) → U52(z0, z1, z2)
U52(z0, z1, active(z2)) → U52(z0, z1, z2)
U53(mark(z0), z1, z2) → U53(z0, z1, z2)
U53(z0, mark(z1), z2) → U53(z0, z1, z2)
U53(z0, z1, mark(z2)) → U53(z0, z1, z2)
U53(active(z0), z1, z2) → U53(z0, z1, z2)
U53(z0, active(z1), z2) → U53(z0, z1, z2)
U53(z0, z1, active(z2)) → U53(z0, z1, z2)
U54(mark(z0), z1, z2) → U54(z0, z1, z2)
U54(z0, mark(z1), z2) → U54(z0, z1, z2)
U54(z0, z1, mark(z2)) → U54(z0, z1, z2)
U54(active(z0), z1, z2) → U54(z0, z1, z2)
U54(z0, active(z1), z2) → U54(z0, z1, z2)
U54(z0, z1, active(z2)) → U54(z0, z1, z2)
U55(mark(z0), z1) → U55(z0, z1)
U55(z0, mark(z1)) → U55(z0, z1)
U55(active(z0), z1) → U55(z0, z1)
U55(z0, active(z1)) → U55(z0, z1)
U56(mark(z0)) → U56(z0)
U56(active(z0)) → U56(z0)
U61(mark(z0), z1) → U61(z0, z1)
U61(z0, mark(z1)) → U61(z0, z1)
U61(active(z0), z1) → U61(z0, z1)
U61(z0, active(z1)) → U61(z0, z1)
U62(mark(z0), z1) → U62(z0, z1)
U62(z0, mark(z1)) → U62(z0, z1)
U62(active(z0), z1) → U62(z0, z1)
U62(z0, active(z1)) → U62(z0, z1)
U63(mark(z0)) → U63(z0)
U63(active(z0)) → U63(z0)
U71(mark(z0), z1, z2) → U71(z0, z1, z2)
U71(z0, mark(z1), z2) → U71(z0, z1, z2)
U71(z0, z1, mark(z2)) → U71(z0, z1, z2)
U71(active(z0), z1, z2) → U71(z0, z1, z2)
U71(z0, active(z1), z2) → U71(z0, z1, z2)
U71(z0, z1, active(z2)) → U71(z0, z1, z2)
U72(mark(z0), z1) → U72(z0, z1)
U72(z0, mark(z1)) → U72(z0, z1)
U72(active(z0), z1) → U72(z0, z1)
U72(z0, active(z1)) → U72(z0, z1)
U73(mark(z0), z1) → U73(z0, z1)
U73(z0, mark(z1)) → U73(z0, z1)
U73(active(z0), z1) → U73(z0, z1)
U73(z0, active(z1)) → U73(z0, z1)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)
U74(mark(z0)) → U74(z0)
U74(active(z0)) → U74(z0)
U81(mark(z0), z1) → U81(z0, z1)
U81(z0, mark(z1)) → U81(z0, z1)
U81(active(z0), z1) → U81(z0, z1)
U81(z0, active(z1)) → U81(z0, z1)
U82(mark(z0), z1) → U82(z0, z1)
U82(z0, mark(z1)) → U82(z0, z1)
U82(active(z0), z1) → U82(z0, z1)
U82(z0, active(z1)) → U82(z0, z1)
U83(mark(z0)) → U83(z0)
U83(active(z0)) → U83(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
U91(mark(z0), z1) → U91(z0, z1)
U91(z0, mark(z1)) → U91(z0, z1)
U91(active(z0), z1) → U91(z0, z1)
U91(z0, active(z1)) → U91(z0, z1)
U92(mark(z0)) → U92(z0)
U92(active(z0)) → U92(z0)

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

active, mark, __, U11, U12, isPalListKind, U13, isNeList, U21, U22, U23, U24, U25, isList, U26, U31, U32, U33, isQid, U41, U42, U43, U44, U45, U46, U51, U52, U53, U54, U55, U56, U61, U62, U63, U71, U72, U73, isPal, U74, U81, U82, U83, isNePal, U91, U92

Defined Pair Symbols:none

Compound Symbols:none

(7) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtUnreachableProof (EQUIVALENT transformation)

(4) Obligation:

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) SIsEmptyProof (EQUIVALENT transformation)

(8) BOUNDS(O(1), O(1))