TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60001 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (11535ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (6164ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (6107ms), PolynomialLinearRange8NegiUR (timeout)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

mark#(U11(X1, X2)) → mark#(X1)a____#(__(X, Y), Z) → mark#(Y)
a____#(__(X, Y), Z) → a____#(mark(Y), mark(Z))mark#(U22(X1, X2)) → a__U22#(mark(X1), X2)
a__isPal#(V) → a__isPalListKind#(V)a____#(__(X, Y), Z) → mark#(X)
mark#(isList(X)) → a__isList#(X)a__and#(tt, X) → mark#(X)
a__isNeList#(__(V1, V2)) → a__U41#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)mark#(U31(X1, X2)) → mark#(X1)
a__U11#(tt, V) → a__isNeList#(V)a__isNePal#(__(I, __(P, I))) → a__and#(a__isQid(I), isPalListKind(I))
a__isNePal#(__(I, __(P, I))) → a__and#(a__and(a__isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))mark#(U71(X1, X2)) → a__U71#(mark(X1), X2)
mark#(__(X1, X2)) → mark#(X2)mark#(U72(X)) → mark#(X)
mark#(U53(X)) → mark#(X)mark#(U42(X1, X2)) → a__U42#(mark(X1), X2)
a__U42#(tt, V2) → a__isNeList#(V2)a__isPalListKind#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))
a__isNeList#(__(V1, V2)) → a__isPalListKind#(V1)a__U51#(tt, V1, V2) → a__U52#(a__isNeList(V1), V2)
mark#(U71(X1, X2)) → mark#(X1)a__isList#(__(V1, V2)) → a__isPalListKind#(V1)
mark#(and(X1, X2)) → mark#(X1)a__isList#(V) → a__U11#(a__isPalListKind(V), V)
a__U52#(tt, V2) → a__isList#(V2)mark#(and(X1, X2)) → a__and#(mark(X1), X2)
mark#(U41(X1, X2, X3)) → mark#(X1)a__isNePal#(V) → a__isPalListKind#(V)
mark#(U62(X)) → mark#(X)mark#(U21(X1, X2, X3)) → mark#(X1)
a__isList#(V) → a__isPalListKind#(V)mark#(__(X1, X2)) → mark#(X1)
mark#(U61(X1, X2)) → mark#(X1)mark#(isNePal(X)) → a__isNePal#(X)
mark#(__(X1, X2)) → a____#(mark(X1), mark(X2))a__isNeList#(__(V1, V2)) → a__U51#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)
mark#(U32(X)) → mark#(X)a____#(nil, X) → mark#(X)
mark#(U41(X1, X2, X3)) → a__U41#(mark(X1), X2, X3)a__U71#(tt, V) → a__isNePal#(V)
a____#(X, nil) → mark#(X)a__isList#(__(V1, V2)) → a__U21#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)
a____#(__(X, Y), Z) → mark#(Z)mark#(U51(X1, X2, X3)) → mark#(X1)
mark#(U23(X)) → mark#(X)mark#(U22(X1, X2)) → mark#(X1)
a__U41#(tt, V1, V2) → a__isList#(V1)a____#(__(X, Y), Z) → a____#(mark(X), a____(mark(Y), mark(Z)))
a__isNeList#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))a__isList#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))
mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)a__isNeList#(V) → a__isPalListKind#(V)
a__U22#(tt, V2) → a__isList#(V2)a__U51#(tt, V1, V2) → a__isNeList#(V1)
a__U21#(tt, V1, V2) → a__isList#(V1)mark#(U12(X)) → mark#(X)
a__isPal#(V) → a__U71#(a__isPalListKind(V), V)mark#(U42(X1, X2)) → mark#(X1)
mark#(U52(X1, X2)) → mark#(X1)mark#(U21(X1, X2, X3)) → a__U21#(mark(X1), X2, X3)
mark#(isPalListKind(X)) → a__isPalListKind#(X)mark#(U51(X1, X2, X3)) → a__U51#(mark(X1), X2, X3)
mark#(U43(X)) → mark#(X)a__isPalListKind#(__(V1, V2)) → a__isPalListKind#(V1)
a__U41#(tt, V1, V2) → a__U42#(a__isList(V1), V2)mark#(isNeList(X)) → a__isNeList#(X)
a__U21#(tt, V1, V2) → a__U22#(a__isList(V1), V2)mark#(isPal(X)) → a__isPal#(X)
mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)

Rewrite Rules

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))a____(X, nil) → mark(X)
a____(nil, X) → mark(X)a__U11(tt, V) → a__U12(a__isNeList(V))
a__U12(tt) → tta__U21(tt, V1, V2) → a__U22(a__isList(V1), V2)
a__U22(tt, V2) → a__U23(a__isList(V2))a__U23(tt) → tt
a__U31(tt, V) → a__U32(a__isQid(V))a__U32(tt) → tt
a__U41(tt, V1, V2) → a__U42(a__isList(V1), V2)a__U42(tt, V2) → a__U43(a__isNeList(V2))
a__U43(tt) → tta__U51(tt, V1, V2) → a__U52(a__isNeList(V1), V2)
a__U52(tt, V2) → a__U53(a__isList(V2))a__U53(tt) → tt
a__U61(tt, V) → a__U62(a__isQid(V))a__U62(tt) → tt
a__U71(tt, V) → a__U72(a__isNePal(V))a__U72(tt) → tt
a__and(tt, X) → mark(X)a__isList(V) → a__U11(a__isPalListKind(V), V)
a__isList(nil) → tta__isList(__(V1, V2)) → a__U21(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)
a__isNeList(V) → a__U31(a__isPalListKind(V), V)a__isNeList(__(V1, V2)) → a__U41(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)
a__isNeList(__(V1, V2)) → a__U51(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)a__isNePal(V) → a__U61(a__isPalListKind(V), V)
a__isNePal(__(I, __(P, I))) → a__and(a__and(a__isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))a__isPal(V) → a__U71(a__isPalListKind(V), V)
a__isPal(nil) → tta__isPalListKind(a) → tt
a__isPalListKind(e) → tta__isPalListKind(i) → tt
a__isPalListKind(nil) → tta__isPalListKind(o) → tt
a__isPalListKind(u) → tta__isPalListKind(__(V1, V2)) → a__and(a__isPalListKind(V1), isPalListKind(V2))
a__isQid(a) → tta__isQid(e) → tt
a__isQid(i) → tta__isQid(o) → tt
a__isQid(u) → ttmark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X1, X2)) → a__U11(mark(X1), X2)mark(U12(X)) → a__U12(mark(X))
mark(isNeList(X)) → a__isNeList(X)mark(U21(X1, X2, X3)) → a__U21(mark(X1), X2, X3)
mark(U22(X1, X2)) → a__U22(mark(X1), X2)mark(isList(X)) → a__isList(X)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(isQid(X)) → a__isQid(X)
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)mark(U42(X1, X2)) → a__U42(mark(X1), X2)
mark(U43(X)) → a__U43(mark(X))mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)mark(U53(X)) → a__U53(mark(X))
mark(U61(X1, X2)) → a__U61(mark(X1), X2)mark(U62(X)) → a__U62(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)mark(U72(X)) → a__U72(mark(X))
mark(isNePal(X)) → a__isNePal(X)mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isPalListKind(X)) → a__isPalListKind(X)mark(isPal(X)) → a__isPal(X)
mark(nil) → nilmark(tt) → tt
mark(a) → amark(e) → e
mark(i) → imark(o) → o
mark(u) → ua____(X1, X2) → __(X1, X2)
a__U11(X1, X2) → U11(X1, X2)a__U12(X) → U12(X)
a__isNeList(X) → isNeList(X)a__U21(X1, X2, X3) → U21(X1, X2, X3)
a__U22(X1, X2) → U22(X1, X2)a__isList(X) → isList(X)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__isQid(X) → isQid(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)a__U42(X1, X2) → U42(X1, X2)
a__U43(X) → U43(X)a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2) → U52(X1, X2)a__U53(X) → U53(X)
a__U61(X1, X2) → U61(X1, X2)a__U62(X) → U62(X)
a__U71(X1, X2) → U71(X1, X2)a__U72(X) → U72(X)
a__isNePal(X) → isNePal(X)a__and(X1, X2) → and(X1, X2)
a__isPalListKind(X) → isPalListKind(X)a__isPal(X) → isPal(X)

Original Signature

Termination of terms over the following signature is verified: a____, a__isNePal, U62, U61, a__U41, a__U72, a__U43, a__U42, a__U71, U23, U21, U22, mark, isPal, U71, and, U72, a__U32, a__isPal, a__U31, U31, isQid, U32, a__U51, a__U52, a__U53, isList, a__isQid, isNeList, __, a__isPalListKind, a__and, U43, U42, U41, isNePal, a__isNeList, a__U23, a__U22, a__U21, a__U62, e, isPalListKind, a, o, i, a__isList, u, U51, tt, U53, U52, U11, a__U12, U12, a__U11, a__U61, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(U11(X1, X2)) → mark#(X1)a__U61#(tt, V) → a__U62#(a__isQid(V))
a____#(__(X, Y), Z) → mark#(Y)mark#(U62(X)) → a__U62#(mark(X))
a__U61#(tt, V) → a__isQid#(V)a____#(__(X, Y), Z) → a____#(mark(Y), mark(Z))
mark#(U22(X1, X2)) → a__U22#(mark(X1), X2)mark#(U72(X)) → a__U72#(mark(X))
a__isPal#(V) → a__isPalListKind#(V)a____#(__(X, Y), Z) → mark#(X)
mark#(isList(X)) → a__isList#(X)mark#(U23(X)) → a__U23#(mark(X))
mark#(U53(X)) → a__U53#(mark(X))a__and#(tt, X) → mark#(X)
a__isNeList#(__(V1, V2)) → a__U41#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)a__U11#(tt, V) → a__isNeList#(V)
mark#(U31(X1, X2)) → mark#(X1)a__isNePal#(__(I, __(P, I))) → a__and#(a__isQid(I), isPalListKind(I))
a__isNePal#(__(I, __(P, I))) → a__and#(a__and(a__isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))mark#(__(X1, X2)) → mark#(X2)
mark#(U71(X1, X2)) → a__U71#(mark(X1), X2)mark#(U72(X)) → mark#(X)
mark#(U53(X)) → mark#(X)mark#(U42(X1, X2)) → a__U42#(mark(X1), X2)
a__U42#(tt, V2) → a__isNeList#(V2)a__isPalListKind#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))
a__isNeList#(__(V1, V2)) → a__isPalListKind#(V1)mark#(U71(X1, X2)) → mark#(X1)
a__U51#(tt, V1, V2) → a__U52#(a__isNeList(V1), V2)mark#(and(X1, X2)) → mark#(X1)
mark#(U61(X1, X2)) → a__U61#(mark(X1), X2)a__isList#(__(V1, V2)) → a__isPalListKind#(V1)
a__isNePal#(__(I, __(P, I))) → a__isQid#(I)a__U52#(tt, V2) → a__U53#(a__isList(V2))
a__isList#(V) → a__U11#(a__isPalListKind(V), V)mark#(and(X1, X2)) → a__and#(mark(X1), X2)
mark#(U41(X1, X2, X3)) → mark#(X1)a__U52#(tt, V2) → a__isList#(V2)
a__U31#(tt, V) → a__isQid#(V)a__isNePal#(V) → a__isPalListKind#(V)
mark#(U62(X)) → mark#(X)a__U22#(tt, V2) → a__U23#(a__isList(V2))
mark#(U21(X1, X2, X3)) → mark#(X1)mark#(__(X1, X2)) → mark#(X1)
a__isList#(V) → a__isPalListKind#(V)mark#(U61(X1, X2)) → mark#(X1)
mark#(U43(X)) → a__U43#(mark(X))mark#(isNePal(X)) → a__isNePal#(X)
mark#(__(X1, X2)) → a____#(mark(X1), mark(X2))a__U42#(tt, V2) → a__U43#(a__isNeList(V2))
mark#(U32(X)) → a__U32#(mark(X))a__isNeList#(__(V1, V2)) → a__U51#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)
mark#(U32(X)) → mark#(X)a____#(nil, X) → mark#(X)
a__U71#(tt, V) → a__isNePal#(V)a__U31#(tt, V) → a__U32#(a__isQid(V))
mark#(U31(X1, X2)) → a__U31#(mark(X1), X2)mark#(U41(X1, X2, X3)) → a__U41#(mark(X1), X2, X3)
a____#(X, nil) → mark#(X)a__isList#(__(V1, V2)) → a__U21#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)
a____#(__(X, Y), Z) → mark#(Z)mark#(U51(X1, X2, X3)) → mark#(X1)
mark#(U22(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
a____#(__(X, Y), Z) → a____#(mark(X), a____(mark(Y), mark(Z)))a__U41#(tt, V1, V2) → a__isList#(V1)
a__isNeList#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))a__isNePal#(V) → a__U61#(a__isPalListKind(V), V)
a__isList#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)
a__isNeList#(V) → a__isPalListKind#(V)a__U22#(tt, V2) → a__isList#(V2)
a__U21#(tt, V1, V2) → a__isList#(V1)a__U51#(tt, V1, V2) → a__isNeList#(V1)
mark#(U12(X)) → mark#(X)a__isPal#(V) → a__U71#(a__isPalListKind(V), V)
mark#(isQid(X)) → a__isQid#(X)mark#(U42(X1, X2)) → mark#(X1)
a__U71#(tt, V) → a__U72#(a__isNePal(V))mark#(U52(X1, X2)) → mark#(X1)
a__U11#(tt, V) → a__U12#(a__isNeList(V))mark#(U12(X)) → a__U12#(mark(X))
mark#(U21(X1, X2, X3)) → a__U21#(mark(X1), X2, X3)mark#(isPalListKind(X)) → a__isPalListKind#(X)
mark#(U51(X1, X2, X3)) → a__U51#(mark(X1), X2, X3)a__isPalListKind#(__(V1, V2)) → a__isPalListKind#(V1)
mark#(U43(X)) → mark#(X)a__U41#(tt, V1, V2) → a__U42#(a__isList(V1), V2)
mark#(isNeList(X)) → a__isNeList#(X)a__U21#(tt, V1, V2) → a__U22#(a__isList(V1), V2)
mark#(isPal(X)) → a__isPal#(X)mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)
a__isNeList#(V) → a__U31#(a__isPalListKind(V), V)

Rewrite Rules

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))a____(X, nil) → mark(X)
a____(nil, X) → mark(X)a__U11(tt, V) → a__U12(a__isNeList(V))
a__U12(tt) → tta__U21(tt, V1, V2) → a__U22(a__isList(V1), V2)
a__U22(tt, V2) → a__U23(a__isList(V2))a__U23(tt) → tt
a__U31(tt, V) → a__U32(a__isQid(V))a__U32(tt) → tt
a__U41(tt, V1, V2) → a__U42(a__isList(V1), V2)a__U42(tt, V2) → a__U43(a__isNeList(V2))
a__U43(tt) → tta__U51(tt, V1, V2) → a__U52(a__isNeList(V1), V2)
a__U52(tt, V2) → a__U53(a__isList(V2))a__U53(tt) → tt
a__U61(tt, V) → a__U62(a__isQid(V))a__U62(tt) → tt
a__U71(tt, V) → a__U72(a__isNePal(V))a__U72(tt) → tt
a__and(tt, X) → mark(X)a__isList(V) → a__U11(a__isPalListKind(V), V)
a__isList(nil) → tta__isList(__(V1, V2)) → a__U21(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)
a__isNeList(V) → a__U31(a__isPalListKind(V), V)a__isNeList(__(V1, V2)) → a__U41(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)
a__isNeList(__(V1, V2)) → a__U51(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)a__isNePal(V) → a__U61(a__isPalListKind(V), V)
a__isNePal(__(I, __(P, I))) → a__and(a__and(a__isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))a__isPal(V) → a__U71(a__isPalListKind(V), V)
a__isPal(nil) → tta__isPalListKind(a) → tt
a__isPalListKind(e) → tta__isPalListKind(i) → tt
a__isPalListKind(nil) → tta__isPalListKind(o) → tt
a__isPalListKind(u) → tta__isPalListKind(__(V1, V2)) → a__and(a__isPalListKind(V1), isPalListKind(V2))
a__isQid(a) → tta__isQid(e) → tt
a__isQid(i) → tta__isQid(o) → tt
a__isQid(u) → ttmark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X1, X2)) → a__U11(mark(X1), X2)mark(U12(X)) → a__U12(mark(X))
mark(isNeList(X)) → a__isNeList(X)mark(U21(X1, X2, X3)) → a__U21(mark(X1), X2, X3)
mark(U22(X1, X2)) → a__U22(mark(X1), X2)mark(isList(X)) → a__isList(X)
mark(U23(X)) → a__U23(mark(X))mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))mark(isQid(X)) → a__isQid(X)
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)mark(U42(X1, X2)) → a__U42(mark(X1), X2)
mark(U43(X)) → a__U43(mark(X))mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)mark(U53(X)) → a__U53(mark(X))
mark(U61(X1, X2)) → a__U61(mark(X1), X2)mark(U62(X)) → a__U62(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)mark(U72(X)) → a__U72(mark(X))
mark(isNePal(X)) → a__isNePal(X)mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isPalListKind(X)) → a__isPalListKind(X)mark(isPal(X)) → a__isPal(X)
mark(nil) → nilmark(tt) → tt
mark(a) → amark(e) → e
mark(i) → imark(o) → o
mark(u) → ua____(X1, X2) → __(X1, X2)
a__U11(X1, X2) → U11(X1, X2)a__U12(X) → U12(X)
a__isNeList(X) → isNeList(X)a__U21(X1, X2, X3) → U21(X1, X2, X3)
a__U22(X1, X2) → U22(X1, X2)a__isList(X) → isList(X)
a__U23(X) → U23(X)a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)a__isQid(X) → isQid(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)a__U42(X1, X2) → U42(X1, X2)
a__U43(X) → U43(X)a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2) → U52(X1, X2)a__U53(X) → U53(X)
a__U61(X1, X2) → U61(X1, X2)a__U62(X) → U62(X)
a__U71(X1, X2) → U71(X1, X2)a__U72(X) → U72(X)
a__isNePal(X) → isNePal(X)a__and(X1, X2) → and(X1, X2)
a__isPalListKind(X) → isPalListKind(X)a__isPal(X) → isPal(X)

Original Signature

Termination of terms over the following signature is verified: a____, a__isNePal, U62, U61, a__U41, a__U72, a__U43, a__U42, a__U71, U23, U21, U22, mark, isPal, and, U71, U72, a__isPal, a__U32, a__U31, isQid, U31, U32, a__U51, a__U52, a__U53, isList, a__isQid, isNeList, __, a__isPalListKind, a__and, U43, U42, U41, isNePal, a__isNeList, a__U23, a__U22, a__U21, a__U62, e, isPalListKind, a, o, i, a__isList, u, U51, tt, U53, U52, U11, U12, a__U12, a__U11, a__U61, nil

Strategy


The following SCCs where found

a____#(__(X, Y), Z) → mark#(Y)mark#(U11(X1, X2)) → mark#(X1)
a____#(__(X, Y), Z) → a____#(mark(Y), mark(Z))mark#(U22(X1, X2)) → a__U22#(mark(X1), X2)
a__isPal#(V) → a__isPalListKind#(V)a____#(__(X, Y), Z) → mark#(X)
mark#(isList(X)) → a__isList#(X)a__and#(tt, X) → mark#(X)
a__isNeList#(__(V1, V2)) → a__U41#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)a__U11#(tt, V) → a__isNeList#(V)
mark#(U31(X1, X2)) → mark#(X1)a__isNePal#(__(I, __(P, I))) → a__and#(a__isQid(I), isPalListKind(I))
mark#(__(X1, X2)) → mark#(X2)mark#(U71(X1, X2)) → a__U71#(mark(X1), X2)
a__isNePal#(__(I, __(P, I))) → a__and#(a__and(a__isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))mark#(U72(X)) → mark#(X)
mark#(U53(X)) → mark#(X)mark#(U42(X1, X2)) → a__U42#(mark(X1), X2)
a__U42#(tt, V2) → a__isNeList#(V2)a__isPalListKind#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))
a__isNeList#(__(V1, V2)) → a__isPalListKind#(V1)mark#(U71(X1, X2)) → mark#(X1)
a__U51#(tt, V1, V2) → a__U52#(a__isNeList(V1), V2)mark#(and(X1, X2)) → mark#(X1)
a__isList#(__(V1, V2)) → a__isPalListKind#(V1)a__isList#(V) → a__U11#(a__isPalListKind(V), V)
mark#(U41(X1, X2, X3)) → mark#(X1)mark#(and(X1, X2)) → a__and#(mark(X1), X2)
a__U52#(tt, V2) → a__isList#(V2)a__isNePal#(V) → a__isPalListKind#(V)
mark#(U62(X)) → mark#(X)mark#(U21(X1, X2, X3)) → mark#(X1)
mark#(__(X1, X2)) → mark#(X1)a__isList#(V) → a__isPalListKind#(V)
mark#(U61(X1, X2)) → mark#(X1)mark#(isNePal(X)) → a__isNePal#(X)
mark#(__(X1, X2)) → a____#(mark(X1), mark(X2))mark#(U32(X)) → mark#(X)
a__isNeList#(__(V1, V2)) → a__U51#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)a____#(nil, X) → mark#(X)
a__U71#(tt, V) → a__isNePal#(V)mark#(U41(X1, X2, X3)) → a__U41#(mark(X1), X2, X3)
a____#(X, nil) → mark#(X)a____#(__(X, Y), Z) → mark#(Z)
a__isList#(__(V1, V2)) → a__U21#(a__and(a__isPalListKind(V1), isPalListKind(V2)), V1, V2)mark#(U51(X1, X2, X3)) → mark#(X1)
mark#(U22(X1, X2)) → mark#(X1)mark#(U23(X)) → mark#(X)
a____#(__(X, Y), Z) → a____#(mark(X), a____(mark(Y), mark(Z)))a__U41#(tt, V1, V2) → a__isList#(V1)
a__isNeList#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))mark#(U52(X1, X2)) → a__U52#(mark(X1), X2)
a__isList#(__(V1, V2)) → a__and#(a__isPalListKind(V1), isPalListKind(V2))a__U22#(tt, V2) → a__isList#(V2)
a__isNeList#(V) → a__isPalListKind#(V)a__U21#(tt, V1, V2) → a__isList#(V1)
a__U51#(tt, V1, V2) → a__isNeList#(V1)mark#(U12(X)) → mark#(X)
mark#(U42(X1, X2)) → mark#(X1)a__isPal#(V) → a__U71#(a__isPalListKind(V), V)
mark#(U52(X1, X2)) → mark#(X1)mark#(U21(X1, X2, X3)) → a__U21#(mark(X1), X2, X3)
mark#(isPalListKind(X)) → a__isPalListKind#(X)mark#(U51(X1, X2, X3)) → a__U51#(mark(X1), X2, X3)
a__isPalListKind#(__(V1, V2)) → a__isPalListKind#(V1)mark#(U43(X)) → mark#(X)
mark#(isNeList(X)) → a__isNeList#(X)a__U41#(tt, V1, V2) → a__U42#(a__isList(V1), V2)
mark#(isPal(X)) → a__isPal#(X)a__U21#(tt, V1, V2) → a__U22#(a__isList(V1), V2)
mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)