TIMEOUT

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (timeout)].

The following open problems remain:



Open Dependency Pair Problem 1

Dependency Pairs

mark#(U32(X))U32#(mark(X))U62#(X1, active(X2))U62#(X1, X2)
active#(U52(tt, V2))isNatList#(V2)active#(U61(tt, V1, V2))isNat#(V1)
mark#(take(X1, X2))active#(take(mark(X1), mark(X2)))U11#(mark(X1), X2)U11#(X1, X2)
active#(take(s(M), cons(N, IL)))isNatKind#(M)U91#(active(X1), X2, X3, X4)U91#(X1, X2, X3, X4)
U61#(X1, active(X2), X3)U61#(X1, X2, X3)U61#(X1, X2, mark(X3))U61#(X1, X2, X3)
U52#(X1, active(X2))U52#(X1, X2)active#(U61(tt, V1, V2))mark#(U62(isNat(V1), V2))
active#(isNatIListKind(cons(V1, V2)))isNatKind#(V1)isNat#(active(X))isNat#(X)
U21#(X1, active(X2))U21#(X1, X2)active#(take(s(M), cons(N, IL)))and#(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
mark#(s(X))mark#(X)mark#(U11(X1, X2))active#(U11(mark(X1), X2))
length#(mark(X))length#(X)mark#(U81(X))active#(U81(mark(X)))
U81#(mark(X))U81#(X)U62#(X1, mark(X2))U62#(X1, X2)
mark#(U53(X))active#(U53(mark(X)))and#(mark(X1), X2)and#(X1, X2)
active#(U21(tt, V1))isNat#(V1)U42#(mark(X1), X2)U42#(X1, X2)
mark#(U12(X))active#(U12(mark(X)))U11#(X1, mark(X2))U11#(X1, X2)
active#(length(cons(N, L)))mark#(U71(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active#(U12(tt))mark#(tt)
U41#(X1, active(X2), X3)U41#(X1, X2, X3)U53#(mark(X))U53#(X)
mark#(U41(X1, X2, X3))mark#(X1)active#(isNatList(take(V1, V2)))U61#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
active#(take(0, IL))mark#(U81(and(isNatIList(IL), isNatIListKind(IL))))mark#(U22(X))active#(U22(mark(X)))
mark#(U22(X))U22#(mark(X))mark#(U53(X))U53#(mark(X))
U61#(active(X1), X2, X3)U61#(X1, X2, X3)mark#(U32(X))mark#(X)
active#(take(s(M), cons(N, IL)))isNat#(N)mark#(U62(X1, X2))mark#(X1)
U32#(mark(X))U32#(X)active#(isNatIListKind(take(V1, V2)))isNatKind#(V1)
mark#(U21(X1, X2))active#(U21(mark(X1), X2))active#(isNatIListKind(cons(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))
mark#(U42(X1, X2))U42#(mark(X1), X2)active#(isNatIListKind(take(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))
cons#(X1, mark(X2))cons#(X1, X2)U61#(mark(X1), X2, X3)U61#(X1, X2, X3)
U41#(X1, X2, active(X3))U41#(X1, X2, X3)isNatKind#(mark(X))isNatKind#(X)
mark#(isNatKind(X))isNatKind#(X)active#(U41(tt, V1, V2))U42#(isNat(V1), V2)
active#(take(s(M), cons(N, IL)))mark#(U91(and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N))U52#(X1, mark(X2))U52#(X1, X2)
active#(isNatIList(cons(V1, V2)))isNatIListKind#(V2)mark#(U42(X1, X2))mark#(X1)
active#(isNatList(take(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))active#(length(cons(N, L)))and#(isNatList(L), isNatIListKind(L))
U21#(active(X1), X2)U21#(X1, X2)mark#(U61(X1, X2, X3))U61#(mark(X1), X2, X3)
cons#(active(X1), X2)cons#(X1, X2)U91#(mark(X1), X2, X3, X4)U91#(X1, X2, X3, X4)
isNatList#(mark(X))isNatList#(X)active#(isNat(s(V1)))U21#(isNatKind(V1), V1)
mark#(isNatList(X))isNatList#(X)mark#(U41(X1, X2, X3))active#(U41(mark(X1), X2, X3))
U42#(active(X1), X2)U42#(X1, X2)active#(U11(tt, V1))isNatList#(V1)
mark#(take(X1, X2))mark#(X1)U52#(mark(X1), X2)U52#(X1, X2)
active#(U91(tt, IL, M, N))take#(M, IL)active#(isNatList(take(V1, V2)))isNatKind#(V1)
active#(take(s(M), cons(N, IL)))U91#(and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)active#(take(0, IL))isNatIListKind#(IL)
active#(take(s(M), cons(N, IL)))isNatIList#(IL)active#(U42(tt, V2))isNatIList#(V2)
active#(U81(tt))mark#(nil)mark#(U52(X1, X2))U52#(mark(X1), X2)
U12#(mark(X))U12#(X)mark#(s(X))s#(mark(X))
active#(U41(tt, V1, V2))mark#(U42(isNat(V1), V2))active#(U11(tt, V1))U12#(isNatList(V1))
active#(take(s(M), cons(N, IL)))and#(isNat(M), isNatKind(M))U22#(mark(X))U22#(X)
isNatList#(active(X))isNatList#(X)active#(take(s(M), cons(N, IL)))isNatKind#(N)
U51#(X1, mark(X2), X3)U51#(X1, X2, X3)active#(isNat(0))mark#(tt)
mark#(and(X1, X2))and#(mark(X1), X2)active#(length(cons(N, L)))and#(isNat(N), isNatKind(N))
active#(isNatIListKind(cons(V1, V2)))isNatIListKind#(V2)take#(X1, mark(X2))take#(X1, X2)
active#(isNatIList(cons(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))isNatIList#(mark(X))isNatIList#(X)
active#(take(0, IL))U81#(and(isNatIList(IL), isNatIListKind(IL)))mark#(isNatIList(X))isNatIList#(X)
mark#(U71(X1, X2))mark#(X1)active#(U21(tt, V1))U22#(isNat(V1))
cons#(X1, active(X2))cons#(X1, X2)isNatKind#(active(X))isNatKind#(X)
U12#(active(X))U12#(X)active#(isNatList(take(V1, V2)))mark#(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
active#(isNat(length(V1)))U11#(isNatIListKind(V1), V1)U22#(active(X))U22#(X)
U51#(active(X1), X2, X3)U51#(X1, X2, X3)U43#(active(X))U43#(X)
mark#(U62(X1, X2))U62#(mark(X1), X2)active#(isNatKind(length(V1)))mark#(isNatIListKind(V1))
mark#(U41(X1, X2, X3))U41#(mark(X1), X2, X3)take#(mark(X1), X2)take#(X1, X2)
and#(X1, active(X2))and#(X1, X2)active#(length(cons(N, L)))isNatKind#(N)
mark#(U21(X1, X2))U21#(mark(X1), X2)mark#(U21(X1, X2))mark#(X1)
isNat#(mark(X))isNat#(X)mark#(isNat(X))isNat#(X)
active#(length(cons(N, L)))and#(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))active#(length(cons(N, L)))isNatList#(L)
active#(isNatList(nil))mark#(tt)mark#(nil)active#(nil)
active#(U62(tt, V2))mark#(U63(isNatIList(V2)))take#(X1, active(X2))take#(X1, X2)
active#(length(cons(N, L)))isNat#(N)mark#(isNatIListKind(X))active#(isNatIListKind(X))
active#(isNatIList(zeros))mark#(tt)mark#(cons(X1, X2))cons#(mark(X1), X2)
and#(X1, mark(X2))and#(X1, X2)active#(isNatIListKind(take(V1, V2)))mark#(and(isNatKind(V1), isNatIListKind(V2)))
mark#(U91(X1, X2, X3, X4))active#(U91(mark(X1), X2, X3, X4))mark#(length(X))length#(mark(X))
U43#(mark(X))U43#(X)active#(isNat(s(V1)))mark#(U21(isNatKind(V1), V1))
mark#(take(X1, X2))take#(mark(X1), mark(X2))s#(mark(X))s#(X)
active#(U91(tt, IL, M, N))cons#(N, take(M, IL))mark#(U31(X1, X2))U31#(mark(X1), X2)
U63#(mark(X))U63#(X)mark#(U51(X1, X2, X3))U51#(mark(X1), X2, X3)
mark#(U32(X))active#(U32(mark(X)))active#(isNatIList(V))U31#(isNatIListKind(V), V)
mark#(U42(X1, X2))active#(U42(mark(X1), X2))U91#(X1, X2, X3, active(X4))U91#(X1, X2, X3, X4)
mark#(length(X))active#(length(mark(X)))active#(take(0, IL))isNatIList#(IL)
mark#(U43(X))U43#(mark(X))active#(U61(tt, V1, V2))U62#(isNat(V1), V2)
active#(isNatKind(0))mark#(tt)mark#(U11(X1, X2))mark#(X1)
isNatIListKind#(active(X))isNatIListKind#(X)active#(isNatIList(V))isNatIListKind#(V)
U71#(X1, mark(X2))U71#(X1, X2)active#(length(nil))mark#(0)
U62#(active(X1), X2)U62#(X1, X2)active#(U11(tt, V1))mark#(U12(isNatList(V1)))
U81#(active(X))U81#(X)active#(U22(tt))mark#(tt)
active#(U62(tt, V2))isNatIList#(V2)active#(isNat(length(V1)))mark#(U11(isNatIListKind(V1), V1))
active#(length(cons(N, L)))U71#(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)mark#(U53(X))mark#(X)
U51#(X1, X2, active(X3))U51#(X1, X2, X3)U11#(active(X1), X2)U11#(X1, X2)
active#(U53(tt))mark#(tt)mark#(U63(X))active#(U63(mark(X)))
mark#(U71(X1, X2))U71#(mark(X1), X2)active#(U51(tt, V1, V2))U52#(isNat(V1), V2)
mark#(cons(X1, X2))mark#(X1)active#(U52(tt, V2))U53#(isNatList(V2))
U11#(X1, active(X2))U11#(X1, X2)active#(isNatKind(length(V1)))isNatIListKind#(V1)
active#(isNat(s(V1)))isNatKind#(V1)mark#(and(X1, X2))mark#(X1)
active#(isNatList(cons(V1, V2)))isNatIListKind#(V2)active#(take(s(M), cons(N, IL)))isNat#(M)
mark#(U63(X))mark#(X)active#(U71(tt, L))mark#(s(length(L)))
active#(U31(tt, V))U32#(isNatList(V))active#(isNatList(cons(V1, V2)))U51#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
mark#(U62(X1, X2))active#(U62(mark(X1), X2))cons#(mark(X1), X2)cons#(X1, X2)
mark#(tt)active#(tt)U31#(X1, active(X2))U31#(X1, X2)
active#(take(s(M), cons(N, IL)))isNatIListKind#(IL)active#(isNatList(cons(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))
U21#(X1, mark(X2))U21#(X1, X2)mark#(U51(X1, X2, X3))mark#(X1)
U71#(mark(X1), X2)U71#(X1, X2)mark#(length(X))mark#(X)
active#(isNatKind(s(V1)))mark#(isNatKind(V1))mark#(zeros)active#(zeros)
mark#(U31(X1, X2))active#(U31(mark(X1), X2))active#(isNat(length(V1)))isNatIListKind#(V1)
mark#(U63(X))U63#(mark(X))U51#(mark(X1), X2, X3)U51#(X1, X2, X3)
mark#(0)active#(0)mark#(s(X))active#(s(mark(X)))
U41#(X1, X2, mark(X3))U41#(X1, X2, X3)U52#(active(X1), X2)U52#(X1, X2)
U91#(X1, mark(X2), X3, X4)U91#(X1, X2, X3, X4)mark#(U43(X))active#(U43(mark(X)))
mark#(U22(X))mark#(X)mark#(U43(X))mark#(X)
active#(isNatIListKind(nil))mark#(tt)active#(zeros)cons#(0, zeros)
mark#(U51(X1, X2, X3))active#(U51(mark(X1), X2, X3))active#(isNatList(take(V1, V2)))isNatIListKind#(V2)
isNatIListKind#(mark(X))isNatIListKind#(X)mark#(isNatIListKind(X))isNatIListKind#(X)
active#(isNatIListKind(take(V1, V2)))isNatIListKind#(V2)mark#(cons(X1, X2))active#(cons(mark(X1), X2))
active#(U21(tt, V1))mark#(U22(isNat(V1)))mark#(isNatKind(X))active#(isNatKind(X))
active#(isNatIListKind(zeros))mark#(tt)active#(U51(tt, V1, V2))isNat#(V1)
active#(isNatIList(V))mark#(U31(isNatIListKind(V), V))U53#(active(X))U53#(X)
active#(U71(tt, L))length#(L)active#(take(s(M), cons(N, IL)))and#(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))))
U51#(X1, active(X2), X3)U51#(X1, X2, X3)active#(U42(tt, V2))mark#(U43(isNatIList(V2)))
U91#(X1, X2, active(X3), X4)U91#(X1, X2, X3, X4)U63#(active(X))U63#(X)
active#(U42(tt, V2))U43#(isNatIList(V2))length#(active(X))length#(X)
mark#(U81(X))mark#(X)U42#(X1, mark(X2))U42#(X1, X2)
U31#(active(X1), X2)U31#(X1, X2)active#(U31(tt, V))mark#(U32(isNatList(V)))
mark#(U31(X1, X2))mark#(X1)active#(U52(tt, V2))mark#(U53(isNatList(V2)))
U62#(mark(X1), X2)U62#(X1, X2)active#(U32(tt))mark#(tt)
mark#(isNatIList(X))active#(isNatIList(X))U61#(X1, mark(X2), X3)U61#(X1, X2, X3)
active#(take(s(M), cons(N, IL)))and#(isNatIList(IL), isNatIListKind(IL))mark#(U12(X))U12#(mark(X))
isNatIList#(active(X))isNatIList#(X)active#(isNatList(cons(V1, V2)))mark#(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
active#(U62(tt, V2))U63#(isNatIList(V2))active#(U31(tt, V))isNatList#(V)
U71#(X1, active(X2))U71#(X1, X2)active#(length(cons(N, L)))isNatIListKind#(L)
active#(U91(tt, IL, M, N))mark#(cons(N, take(M, IL)))U41#(active(X1), X2, X3)U41#(X1, X2, X3)
active#(take(0, IL))and#(isNatIList(IL), isNatIListKind(IL))active#(isNatIList(cons(V1, V2)))mark#(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
active#(U43(tt))mark#(tt)and#(active(X1), X2)and#(X1, X2)
mark#(U52(X1, X2))active#(U52(mark(X1), X2))active#(take(s(M), cons(N, IL)))and#(isNat(N), isNatKind(N))
mark#(isNat(X))active#(isNat(X))U42#(X1, active(X2))U42#(X1, X2)
mark#(U61(X1, X2, X3))active#(U61(mark(X1), X2, X3))mark#(U61(X1, X2, X3))mark#(X1)
active#(U63(tt))mark#(tt)mark#(U81(X))U81#(mark(X))
U31#(X1, mark(X2))U31#(X1, X2)active#(U41(tt, V1, V2))isNat#(V1)
active#(isNatIListKind(cons(V1, V2)))mark#(and(isNatKind(V1), isNatIListKind(V2)))mark#(U11(X1, X2))U11#(mark(X1), X2)
mark#(U71(X1, X2))active#(U71(mark(X1), X2))U41#(mark(X1), X2, X3)U41#(X1, X2, X3)
mark#(and(X1, X2))active#(and(mark(X1), X2))active#(U51(tt, V1, V2))mark#(U52(isNat(V1), V2))
active#(U71(tt, L))s#(length(L))active#(isNatKind(s(V1)))isNatKind#(V1)
U32#(active(X))U32#(X)mark#(U12(X))mark#(X)
mark#(U91(X1, X2, X3, X4))U91#(mark(X1), X2, X3, X4)mark#(U52(X1, X2))mark#(X1)
active#(isNatIList(cons(V1, V2)))isNatKind#(V1)U51#(X1, X2, mark(X3))U51#(X1, X2, X3)
U41#(X1, mark(X2), X3)U41#(X1, X2, X3)active#(and(tt, X))mark#(X)
U31#(mark(X1), X2)U31#(X1, X2)U61#(X1, X2, active(X3))U61#(X1, X2, X3)
mark#(U91(X1, X2, X3, X4))mark#(X1)active#(isNatIList(cons(V1, V2)))U41#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
U71#(active(X1), X2)U71#(X1, X2)U21#(mark(X1), X2)U21#(X1, X2)
active#(isNatList(cons(V1, V2)))isNatKind#(V1)mark#(take(X1, X2))mark#(X2)
active#(zeros)mark#(cons(0, zeros))s#(active(X))s#(X)
U91#(X1, active(X2), X3, X4)U91#(X1, X2, X3, X4)U91#(X1, X2, mark(X3), X4)U91#(X1, X2, X3, X4)
mark#(isNatList(X))active#(isNatList(X))take#(active(X1), X2)take#(X1, X2)
U91#(X1, X2, X3, mark(X4))U91#(X1, X2, X3, X4)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, V1, V2))mark(U62(isNat(V1), V2))
active(U62(tt, V2))mark(U63(isNatIList(V2)))active(U63(tt))mark(tt)
active(U71(tt, L))mark(s(length(L)))active(U81(tt))mark(nil)
active(U91(tt, IL, M, N))mark(cons(N, take(M, IL)))active(and(tt, X))mark(X)
active(isNat(0))mark(tt)active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))
active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))active(isNatIList(V))mark(U31(isNatIListKind(V), V))
active(isNatIList(zeros))mark(tt)active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
active(isNatIListKind(nil))mark(tt)active(isNatIListKind(zeros))mark(tt)
active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))active(isNatIListKind(take(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatList(take(V1, V2)))mark(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
active(length(nil))mark(0)active(length(cons(N, L)))mark(U71(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))
active(take(0, IL))mark(U81(and(isNatIList(IL), isNatIListKind(IL))))active(take(s(M), cons(N, IL)))mark(U91(and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U11(X1, X2))active(U11(mark(X1), X2))
mark(tt)active(tt)mark(U12(X))active(U12(mark(X)))
mark(isNatList(X))active(isNatList(X))mark(U21(X1, X2))active(U21(mark(X1), X2))
mark(U22(X))active(U22(mark(X)))mark(isNat(X))active(isNat(X))
mark(U31(X1, X2))active(U31(mark(X1), X2))mark(U32(X))active(U32(mark(X)))
mark(U41(X1, X2, X3))active(U41(mark(X1), X2, X3))mark(U42(X1, X2))active(U42(mark(X1), X2))
mark(U43(X))active(U43(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U51(X1, X2, X3))active(U51(mark(X1), X2, X3))mark(U52(X1, X2))active(U52(mark(X1), X2))
mark(U53(X))active(U53(mark(X)))mark(U61(X1, X2, X3))active(U61(mark(X1), X2, X3))
mark(U62(X1, X2))active(U62(mark(X1), X2))mark(U63(X))active(U63(mark(X)))
mark(U71(X1, X2))active(U71(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(length(X))active(length(mark(X)))mark(U81(X))active(U81(mark(X)))
mark(nil)active(nil)mark(U91(X1, X2, X3, X4))active(U91(mark(X1), X2, X3, X4))
mark(take(X1, X2))active(take(mark(X1), mark(X2)))mark(and(X1, X2))active(and(mark(X1), X2))
mark(isNatIListKind(X))active(isNatIListKind(X))mark(isNatKind(X))active(isNatKind(X))
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(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(X))U12(X)U12(active(X))U12(X)
isNatList(mark(X))isNatList(X)isNatList(active(X))isNatList(X)
U21(mark(X1), X2)U21(X1, X2)U21(X1, mark(X2))U21(X1, X2)
U21(active(X1), X2)U21(X1, X2)U21(X1, active(X2))U21(X1, X2)
U22(mark(X))U22(X)U22(active(X))U22(X)
isNat(mark(X))isNat(X)isNat(active(X))isNat(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(X))U32(X)U32(active(X))U32(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)U42(X1, X2)U42(X1, mark(X2))U42(X1, X2)
U42(active(X1), X2)U42(X1, X2)U42(X1, active(X2))U42(X1, X2)
U43(mark(X))U43(X)U43(active(X))U43(X)
isNatIList(mark(X))isNatIList(X)isNatIList(active(X))isNatIList(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)U52(X1, X2)U52(X1, mark(X2))U52(X1, X2)
U52(active(X1), X2)U52(X1, X2)U52(X1, active(X2))U52(X1, X2)
U53(mark(X))U53(X)U53(active(X))U53(X)
U61(mark(X1), X2, X3)U61(X1, X2, X3)U61(X1, mark(X2), X3)U61(X1, X2, X3)
U61(X1, X2, mark(X3))U61(X1, X2, X3)U61(active(X1), X2, X3)U61(X1, X2, X3)
U61(X1, active(X2), X3)U61(X1, X2, X3)U61(X1, X2, active(X3))U61(X1, X2, X3)
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)U71(X1, X2)U71(X1, mark(X2))U71(X1, X2)
U71(active(X1), X2)U71(X1, X2)U71(X1, active(X2))U71(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
length(mark(X))length(X)length(active(X))length(X)
U81(mark(X))U81(X)U81(active(X))U81(X)
U91(mark(X1), X2, X3, X4)U91(X1, X2, X3, X4)U91(X1, mark(X2), X3, X4)U91(X1, X2, X3, X4)
U91(X1, X2, mark(X3), X4)U91(X1, X2, X3, X4)U91(X1, X2, X3, mark(X4))U91(X1, X2, X3, X4)
U91(active(X1), X2, X3, X4)U91(X1, X2, X3, X4)U91(X1, active(X2), X3, X4)U91(X1, X2, X3, X4)
U91(X1, X2, active(X3), X4)U91(X1, X2, X3, X4)U91(X1, X2, X3, active(X4))U91(X1, X2, X3, X4)
take(mark(X1), X2)take(X1, X2)take(X1, mark(X2))take(X1, X2)
take(active(X1), X2)take(X1, X2)take(X1, active(X2))take(X1, X2)
and(mark(X1), X2)and(X1, X2)and(X1, mark(X2))and(X1, X2)
and(active(X1), X2)and(X1, X2)and(X1, active(X2))and(X1, X2)
isNatIListKind(mark(X))isNatIListKind(X)isNatIListKind(active(X))isNatIListKind(X)
isNatKind(mark(X))isNatKind(X)isNatKind(active(X))isNatKind(X)

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U63, U62, U43, U61, U42, U41, U91, length, U21, U22, cons, isNatIList, isNatKind, mark, and, U71, 0, isNatList, U51, s, tt, zeros, take, U53, U81, U52, U11, active, U12, U31, U32, nil