TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60004 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

active#(U133(tt, IL, M, N))mark#(U134(isNatKind(M), IL, M, N))mark#(U104(X1, X2, X3))U104#(mark(X1), X2, X3)
active#(U11(tt, V1))mark#(U12(isNatIListKind(V1), V1))mark#(U102(X1, X2, X3))U102#(mark(X1), X2, X3)
mark#(U132(X1, X2, X3, X4))active#(U132(mark(X1), X2, X3, X4))mark#(U102(X1, X2, X3))active#(U102(mark(X1), X2, X3))
active#(U111(tt, L, N))U112#(isNatIListKind(L), L, N)U94#(mark(X1), X2, X3)U94#(X1, X2, X3)
U136#(X1, X2, X3, mark(X4))U136#(X1, X2, X3, X4)mark#(U51(X1, X2))U51#(mark(X1), X2)
mark#(take(X1, X2))active#(take(mark(X1), mark(X2)))active#(U104(tt, V1, V2))mark#(U105(isNat(V1), V2))
U51#(mark(X1), X2)U51#(X1, X2)active#(isNatIListKind(cons(V1, V2)))isNatKind#(V1)
U21#(X1, active(X2))U21#(X1, X2)mark#(s(X))mark#(X)
active#(take(0, IL))mark#(U121(isNatIList(IL), IL))active#(isNatList(cons(V1, V2)))mark#(U91(isNatKind(V1), V1, V2))
U133#(active(X1), X2, X3, X4)U133#(X1, X2, X3, X4)U114#(X1, mark(X2))U114#(X1, X2)
U114#(X1, active(X2))U114#(X1, X2)U81#(mark(X))U81#(X)
U102#(X1, X2, active(X3))U102#(X1, X2, X3)active#(isNatIListKind(cons(V1, V2)))mark#(U51(isNatKind(V1), V2))
mark#(U136(X1, X2, X3, X4))active#(U136(mark(X1), X2, X3, X4))mark#(U52(X))mark#(X)
U136#(X1, X2, active(X3), X4)U136#(X1, X2, X3, X4)active#(U95(tt, V2))mark#(U96(isNatList(V2)))
U113#(X1, X2, active(X3))U113#(X1, X2, X3)U11#(X1, mark(X2))U11#(X1, X2)
active#(U101(tt, V1, V2))U102#(isNatKind(V1), V1, V2)U43#(active(X1), X2, X3)U43#(X1, X2, X3)
active#(U91(tt, V1, V2))isNatKind#(V1)mark#(U41(X1, X2, X3))mark#(X1)
mark#(U112(X1, X2, X3))mark#(X1)active#(U32(tt, V))U33#(isNatList(V))
mark#(U45(X1, X2))mark#(X1)U102#(mark(X1), X2, X3)U102#(X1, X2, X3)
mark#(U95(X1, X2))mark#(X1)active#(U43(tt, V1, V2))U44#(isNatIListKind(V2), V1, V2)
mark#(U62(X))active#(U62(mark(X)))U12#(X1, active(X2))U12#(X1, X2)
mark#(U131(X1, X2, X3, X4))active#(U131(mark(X1), X2, X3, X4))active#(U132(tt, IL, M, N))mark#(U133(isNat(M), IL, M, N))
active#(U93(tt, V1, V2))U94#(isNatIListKind(V2), V1, V2)active#(U32(tt, V))mark#(U33(isNatList(V)))
active#(U136(tt, IL, M, N))mark#(cons(N, take(M, IL)))active#(U132(tt, IL, M, N))isNat#(M)
mark#(U22(X1, X2))mark#(X1)mark#(U21(X1, X2))active#(U21(mark(X1), X2))
active#(U45(tt, V2))U46#(isNatIList(V2))mark#(U96(X))U96#(mark(X))
mark#(U33(X))active#(U33(mark(X)))U41#(X1, X2, active(X3))U41#(X1, X2, X3)
mark#(U113(X1, X2, X3))mark#(X1)mark#(U106(X))active#(U106(mark(X)))
mark#(U104(X1, X2, X3))active#(U104(mark(X1), X2, X3))active#(isNatKind(length(V1)))U71#(isNatIListKind(V1))
mark#(U46(X))active#(U46(mark(X)))U131#(X1, X2, X3, mark(X4))U131#(X1, X2, X3, X4)
active#(U12(tt, V1))isNatList#(V1)mark#(U92(X1, X2, X3))mark#(X1)
U131#(X1, X2, active(X3), X4)U131#(X1, X2, X3, X4)mark#(U101(X1, X2, X3))U101#(mark(X1), X2, X3)
mark#(U93(X1, X2, X3))U93#(mark(X1), X2, X3)U45#(X1, mark(X2))U45#(X1, X2)
cons#(active(X1), X2)cons#(X1, X2)U135#(X1, active(X2), X3, X4)U135#(X1, X2, X3, X4)
mark#(U131(X1, X2, X3, X4))U131#(mark(X1), X2, X3, X4)U111#(mark(X1), X2, X3)U111#(X1, X2, X3)
active#(U51(tt, V2))isNatIListKind#(V2)mark#(U96(X))active#(U96(mark(X)))
mark#(U41(X1, X2, X3))active#(U41(mark(X1), X2, X3))active#(U112(tt, L, N))U113#(isNat(N), L, N)
active#(U31(tt, V))U32#(isNatIListKind(V), V)U133#(X1, X2, X3, active(X4))U133#(X1, X2, X3, X4)
active#(isNatKind(s(V1)))U81#(isNatKind(V1))mark#(U121(X1, X2))active#(U121(mark(X1), X2))
active#(take(s(M), cons(N, IL)))isNatIList#(IL)active#(U101(tt, V1, V2))isNatKind#(V1)
U61#(active(X1), X2)U61#(X1, X2)U112#(active(X1), X2, X3)U112#(X1, X2, X3)
U131#(X1, active(X2), X3, X4)U131#(X1, X2, X3, X4)U61#(mark(X1), X2)U61#(X1, X2)
mark#(U46(X))U46#(mark(X))U104#(active(X1), X2, X3)U104#(X1, X2, X3)
U91#(X1, X2, active(X3))U91#(X1, X2, X3)mark#(U93(X1, X2, X3))active#(U93(mark(X1), X2, X3))
U93#(active(X1), X2, X3)U93#(X1, X2, X3)U92#(X1, X2, active(X3))U92#(X1, X2, X3)
U71#(mark(X))U71#(X)active#(U62(tt))mark#(tt)
mark#(U112(X1, X2, X3))active#(U112(mark(X1), X2, X3))active#(U51(tt, V2))mark#(U52(isNatIListKind(V2)))
U113#(X1, X2, mark(X3))U113#(X1, X2, X3)active#(isNat(0))mark#(tt)
active#(U11(tt, V1))isNatIListKind#(V1)mark#(U114(X1, X2))U114#(mark(X1), X2)
take#(X1, mark(X2))take#(X1, X2)mark#(isNatIList(X))isNatIList#(X)
isNatIList#(mark(X))isNatIList#(X)U43#(X1, X2, mark(X3))U43#(X1, X2, X3)
isNatKind#(active(X))isNatKind#(X)U103#(X1, mark(X2), X3)U103#(X1, X2, X3)
mark#(U121(X1, X2))mark#(X1)U134#(X1, X2, mark(X3), X4)U134#(X1, X2, X3, X4)
active#(isNat(length(V1)))U11#(isNatIListKind(V1), V1)mark#(U46(X))mark#(X)
U92#(X1, X2, mark(X3))U92#(X1, X2, X3)active#(U46(tt))mark#(tt)
mark#(U41(X1, X2, X3))U41#(mark(X1), X2, X3)active#(U43(tt, V1, V2))isNatIListKind#(V2)
U104#(X1, X2, mark(X3))U104#(X1, X2, X3)U133#(X1, X2, X3, mark(X4))U133#(X1, X2, X3, X4)
mark#(U21(X1, X2))mark#(X1)U61#(X1, mark(X2))U61#(X1, X2)
active#(U91(tt, V1, V2))U92#(isNatKind(V1), V1, V2)U134#(mark(X1), X2, X3, X4)U134#(X1, X2, X3, X4)
U131#(X1, X2, X3, active(X4))U131#(X1, X2, X3, X4)mark#(nil)active#(nil)
U23#(active(X))U23#(X)take#(X1, active(X2))take#(X1, X2)
active#(U114(tt, L))s#(length(L))U106#(active(X))U106#(X)
U101#(X1, X2, active(X3))U101#(X1, X2, X3)mark#(cons(X1, X2))cons#(mark(X1), X2)
active#(U13(tt))mark#(tt)mark#(U22(X1, X2))active#(U22(mark(X1), X2))
mark#(U44(X1, X2, X3))active#(U44(mark(X1), X2, X3))mark#(U32(X1, X2))active#(U32(mark(X1), X2))
U95#(X1, mark(X2))U95#(X1, X2)U92#(active(X1), X2, X3)U92#(X1, X2, X3)
active#(U105(tt, V2))isNatIList#(V2)U92#(X1, active(X2), X3)U92#(X1, X2, X3)
U113#(X1, mark(X2), X3)U113#(X1, X2, X3)active#(U71(tt))mark#(tt)
s#(mark(X))s#(X)active#(U31(tt, V))isNatIListKind#(V)
active#(U136(tt, IL, M, N))cons#(N, take(M, IL))U32#(active(X1), X2)U32#(X1, X2)
mark#(U31(X1, X2))U31#(mark(X1), X2)U135#(X1, mark(X2), X3, X4)U135#(X1, X2, X3, X4)
active#(U101(tt, V1, V2))mark#(U102(isNatKind(V1), V1, V2))U52#(mark(X))U52#(X)
U122#(mark(X))U122#(X)active#(isNatIList(V))U31#(isNatIListKind(V), V)
active#(U105(tt, V2))U106#(isNatIList(V2))mark#(length(X))active#(length(mark(X)))
mark#(U13(X))mark#(X)active#(isNatKind(0))mark#(tt)
mark#(U11(X1, X2))mark#(X1)active#(U132(tt, IL, M, N))U133#(isNat(M), IL, M, N)
active#(length(nil))mark#(0)active#(U94(tt, V1, V2))U95#(isNat(V1), V2)
U81#(active(X))U81#(X)active#(U131(tt, IL, M, N))mark#(U132(isNatIListKind(IL), IL, M, N))
mark#(U22(X1, X2))U22#(mark(X1), X2)mark#(U94(X1, X2, X3))mark#(X1)
mark#(U136(X1, X2, X3, X4))mark#(X1)active#(U92(tt, V1, V2))isNatIListKind#(V2)
active#(U22(tt, V1))isNat#(V1)active#(U42(tt, V1, V2))U43#(isNatIListKind(V2), V1, V2)
U11#(active(X1), X2)U11#(X1, X2)active#(U43(tt, V1, V2))mark#(U44(isNatIListKind(V2), V1, V2))
U131#(X1, mark(X2), X3, X4)U131#(X1, X2, X3, X4)mark#(cons(X1, X2))mark#(X1)
mark#(U42(X1, X2, X3))mark#(X1)mark#(U51(X1, X2))active#(U51(mark(X1), X2))
active#(isNatList(cons(V1, V2)))U91#(isNatKind(V1), V1, V2)active#(U22(tt, V1))mark#(U23(isNat(V1)))
U43#(X1, X2, active(X3))U43#(X1, X2, X3)U42#(X1, active(X2), X3)U42#(X1, X2, X3)
active#(isNatKind(length(V1)))isNatIListKind#(V1)active#(U102(tt, V1, V2))isNatIListKind#(V2)
active#(U94(tt, V1, V2))isNat#(V1)U111#(X1, X2, mark(X3))U111#(X1, X2, X3)
U91#(X1, mark(X2), X3)U91#(X1, X2, X3)active#(U104(tt, V1, V2))U105#(isNat(V1), V2)
mark#(U32(X1, X2))mark#(X1)mark#(U134(X1, X2, X3, X4))U134#(mark(X1), X2, X3, X4)
U51#(X1, active(X2))U51#(X1, X2)active#(U61(tt, V2))mark#(U62(isNatIListKind(V2)))
U131#(mark(X1), X2, X3, X4)U131#(X1, X2, X3, X4)U22#(mark(X1), X2)U22#(X1, X2)
U44#(X1, X2, active(X3))U44#(X1, X2, X3)mark#(U23(X))active#(U23(mark(X)))
mark#(U33(X))mark#(X)U45#(X1, active(X2))U45#(X1, X2)
active#(U121(tt, IL))mark#(U122(isNatIListKind(IL)))U136#(mark(X1), X2, X3, X4)U136#(X1, X2, X3, X4)
mark#(U122(X))active#(U122(mark(X)))U104#(X1, X2, active(X3))U104#(X1, X2, X3)
U45#(mark(X1), X2)U45#(X1, X2)U61#(X1, active(X2))U61#(X1, X2)
U13#(mark(X))U13#(X)U101#(X1, X2, mark(X3))U101#(X1, X2, X3)
mark#(U136(X1, X2, X3, X4))U136#(mark(X1), X2, X3, X4)mark#(U31(X1, X2))active#(U31(mark(X1), X2))
active#(U21(tt, V1))mark#(U22(isNatKind(V1), V1))U94#(X1, X2, mark(X3))U94#(X1, X2, X3)
active#(isNat(length(V1)))isNatIListKind#(V1)U122#(active(X))U122#(X)
mark#(0)active#(0)U41#(X1, X2, mark(X3))U41#(X1, X2, X3)
mark#(U105(X1, X2))mark#(X1)mark#(U43(X1, X2, X3))active#(U43(mark(X1), X2, X3))
U132#(active(X1), X2, X3, X4)U132#(X1, X2, X3, X4)U135#(X1, X2, X3, mark(X4))U135#(X1, X2, X3, X4)
mark#(U71(X))active#(U71(mark(X)))mark#(U133(X1, X2, X3, X4))mark#(X1)
mark#(U62(X))U62#(mark(X))mark#(U105(X1, X2))U105#(mark(X1), X2)
active#(U121(tt, IL))isNatIListKind#(IL)mark#(U12(X1, X2))active#(U12(mark(X1), X2))
U13#(active(X))U13#(X)active#(U105(tt, V2))mark#(U106(isNatIList(V2)))
active#(U133(tt, IL, M, N))U134#(isNatKind(M), IL, M, N)active#(U103(tt, V1, V2))isNatIListKind#(V2)
mark#(U71(X))mark#(X)mark#(isNatIListKind(X))isNatIListKind#(X)
isNatIListKind#(mark(X))isNatIListKind#(X)U42#(X1, X2, active(X3))U42#(X1, X2, X3)
U92#(mark(X1), X2, X3)U92#(X1, X2, X3)mark#(U103(X1, X2, X3))mark#(X1)
active#(U136(tt, IL, M, N))take#(M, IL)U135#(active(X1), X2, X3, X4)U135#(X1, X2, X3, X4)
U91#(X1, X2, mark(X3))U91#(X1, X2, X3)active#(U45(tt, V2))isNatIList#(V2)
active#(U33(tt))mark#(tt)length#(active(X))length#(X)
mark#(U81(X))mark#(X)mark#(U92(X1, X2, X3))active#(U92(mark(X1), X2, X3))
U93#(mark(X1), X2, X3)U93#(X1, X2, X3)U133#(X1, X2, mark(X3), X4)U133#(X1, X2, X3, X4)
U93#(X1, X2, active(X3))U93#(X1, X2, X3)U42#(mark(X1), X2, X3)U42#(X1, X2, X3)
isNatIList#(active(X))isNatIList#(X)mark#(U106(X))mark#(X)
active#(U81(tt))mark#(tt)active#(U114(tt, L))mark#(s(length(L)))
U42#(X1, mark(X2), X3)U42#(X1, X2, X3)mark#(U42(X1, X2, X3))U42#(mark(X1), X2, X3)
U41#(active(X1), X2, X3)U41#(X1, X2, X3)U44#(X1, X2, mark(X3))U44#(X1, X2, X3)
active#(U134(tt, IL, M, N))isNat#(N)active#(U103(tt, V1, V2))U104#(isNatIListKind(V2), V1, V2)
active#(U103(tt, V1, V2))mark#(U104(isNatIListKind(V2), V1, V2))active#(U113(tt, L, N))U114#(isNatKind(N), L)
U104#(X1, mark(X2), X3)U104#(X1, X2, X3)U132#(X1, active(X2), X3, X4)U132#(X1, X2, X3, X4)
active#(U112(tt, L, N))mark#(U113(isNat(N), L, N))U22#(X1, mark(X2))U22#(X1, X2)
mark#(U133(X1, X2, X3, X4))active#(U133(mark(X1), X2, X3, X4))U94#(active(X1), X2, X3)U94#(X1, X2, X3)
U112#(mark(X1), X2, X3)U112#(X1, X2, X3)U41#(mark(X1), X2, X3)U41#(X1, X2, X3)
active#(U44(tt, V1, V2))isNat#(V1)active#(isNatKind(s(V1)))isNatKind#(V1)
active#(U104(tt, V1, V2))isNat#(V1)U101#(X1, mark(X2), X3)U101#(X1, X2, X3)
U41#(X1, mark(X2), X3)U41#(X1, X2, X3)U46#(mark(X))U46#(X)
active#(U23(tt))mark#(tt)mark#(U94(X1, X2, X3))U94#(mark(X1), X2, X3)
mark#(U135(X1, X2, X3, X4))U135#(mark(X1), X2, X3, X4)U95#(mark(X1), X2)U95#(X1, X2)
U131#(active(X1), X2, X3, X4)U131#(X1, X2, X3, X4)active#(take(0, IL))U121#(isNatIList(IL), IL)
active#(U12(tt, V1))U13#(isNatList(V1))U21#(mark(X1), X2)U21#(X1, X2)
active#(isNatList(cons(V1, V2)))isNatKind#(V1)mark#(take(X1, X2))mark#(X2)
mark#(U122(X))U122#(mark(X))active#(isNatKind(s(V1)))mark#(U81(isNatKind(V1)))
U91#(X1, active(X2), X3)U91#(X1, X2, X3)U12#(active(X1), X2)U12#(X1, X2)
U102#(active(X1), X2, X3)U102#(X1, X2, X3)mark#(U106(X))U106#(mark(X))
U134#(active(X1), X2, X3, X4)U134#(X1, X2, X3, X4)U94#(X1, active(X2), X3)U94#(X1, X2, X3)
U11#(mark(X1), X2)U11#(X1, X2)U102#(X1, X2, mark(X3))U102#(X1, X2, X3)
active#(isNatIListKind(cons(V1, V2)))U51#(isNatKind(V1), V2)U111#(X1, mark(X2), X3)U111#(X1, X2, X3)
U91#(mark(X1), X2, X3)U91#(X1, X2, X3)active#(U135(tt, IL, M, N))isNatKind#(N)
active#(isNatIList(cons(V1, V2)))U41#(isNatKind(V1), V1, V2)isNat#(active(X))isNat#(X)
mark#(U11(X1, X2))active#(U11(mark(X1), X2))mark#(U12(X1, X2))mark#(X1)
length#(mark(X))length#(X)active#(U96(tt))mark#(tt)
mark#(U81(X))active#(U81(mark(X)))U43#(mark(X1), X2, X3)U43#(X1, X2, X3)
active#(U42(tt, V1, V2))mark#(U43(isNatIListKind(V2), V1, V2))U121#(active(X1), X2)U121#(X1, X2)
active#(U41(tt, V1, V2))isNatKind#(V1)U104#(X1, active(X2), X3)U104#(X1, X2, X3)
mark#(U122(X))mark#(X)active#(U21(tt, V1))isNatKind#(V1)
U96#(active(X))U96#(X)U132#(mark(X1), X2, X3, X4)U132#(X1, X2, X3, X4)
U41#(X1, active(X2), X3)U41#(X1, X2, X3)U135#(mark(X1), X2, X3, X4)U135#(X1, X2, X3, X4)
mark#(U133(X1, X2, X3, X4))U133#(mark(X1), X2, X3, X4)mark#(U93(X1, X2, X3))mark#(X1)
mark#(U71(X))U71#(mark(X))U103#(X1, active(X2), X3)U103#(X1, X2, X3)
active#(U31(tt, V))mark#(U32(isNatIListKind(V), V))U132#(X1, X2, X3, active(X4))U132#(X1, X2, X3, X4)
mark#(U13(X))U13#(mark(X))mark#(U43(X1, X2, X3))mark#(X1)
U136#(active(X1), X2, X3, X4)U136#(X1, X2, X3, X4)active#(U111(tt, L, N))mark#(U112(isNatIListKind(L), L, N))
active#(U113(tt, L, N))mark#(U114(isNatKind(N), L))active#(U44(tt, V1, V2))U45#(isNat(V1), V2)
active#(U131(tt, IL, M, N))U132#(isNatIListKind(IL), IL, M, N)U136#(X1, X2, X3, active(X4))U136#(X1, X2, X3, X4)
active#(length(cons(N, L)))U111#(isNatList(L), L, N)active#(isNatIListKind(take(V1, V2)))isNatKind#(V1)
U32#(X1, active(X2))U32#(X1, X2)U132#(X1, X2, mark(X3), X4)U132#(X1, X2, X3, X4)
active#(U92(tt, V1, V2))U93#(isNatIListKind(V2), V1, V2)mark#(U112(X1, X2, X3))U112#(mark(X1), X2, X3)
U95#(active(X1), X2)U95#(X1, X2)cons#(X1, mark(X2))cons#(X1, X2)
U93#(X1, X2, mark(X3))U93#(X1, X2, X3)U134#(X1, mark(X2), X3, X4)U134#(X1, X2, X3, X4)
mark#(U95(X1, X2))active#(U95(mark(X1), X2))mark#(isNatKind(X))isNatKind#(X)
active#(U94(tt, V1, V2))mark#(U95(isNat(V1), V2))isNatKind#(mark(X))isNatKind#(X)
active#(U12(tt, V1))mark#(U13(isNatList(V1)))U62#(active(X))U62#(X)
active#(isNatList(take(V1, V2)))U101#(isNatKind(V1), V1, V2)active#(U122(tt))mark#(nil)
U21#(active(X1), X2)U21#(X1, X2)U111#(active(X1), X2, X3)U111#(X1, X2, X3)
U33#(mark(X))U33#(X)U94#(X1, mark(X2), X3)U94#(X1, X2, X3)
active#(length(cons(N, L)))mark#(U111(isNatList(L), L, N))U51#(X1, mark(X2))U51#(X1, X2)
isNatList#(mark(X))isNatList#(X)active#(isNat(s(V1)))U21#(isNatKind(V1), V1)
mark#(isNatList(X))isNatList#(X)U33#(active(X))U33#(X)
U102#(X1, active(X2), X3)U102#(X1, X2, X3)U103#(X1, X2, active(X3))U103#(X1, X2, X3)
active#(U131(tt, IL, M, N))isNatIListKind#(IL)mark#(U135(X1, X2, X3, X4))active#(U135(mark(X1), X2, X3, X4))
U42#(X1, X2, mark(X3))U42#(X1, X2, X3)active#(U92(tt, V1, V2))mark#(U93(isNatIListKind(V2), V1, V2))
active#(U41(tt, V1, V2))U42#(isNatKind(V1), V1, V2)mark#(U91(X1, X2, X3))U91#(mark(X1), X2, X3)
mark#(take(X1, X2))mark#(X1)U133#(X1, active(X2), X3, X4)U133#(X1, X2, X3, X4)
active#(isNatList(take(V1, V2)))isNatKind#(V1)active#(U133(tt, IL, M, N))isNatKind#(M)
mark#(U134(X1, X2, X3, X4))mark#(X1)mark#(U45(X1, X2))active#(U45(mark(X1), X2))
U135#(X1, X2, X3, active(X4))U135#(X1, X2, X3, X4)U71#(active(X))U71#(X)
active#(U95(tt, V2))isNatList#(V2)U93#(X1, active(X2), X3)U93#(X1, X2, X3)
mark#(s(X))s#(mark(X))active#(U21(tt, V1))U22#(isNatKind(V1), V1)
U52#(active(X))U52#(X)U12#(mark(X1), X2)U12#(X1, X2)
isNatList#(active(X))isNatList#(X)U93#(X1, mark(X2), X3)U93#(X1, X2, X3)
U105#(mark(X1), X2)U105#(X1, X2)U121#(X1, active(X2))U121#(X1, X2)
U42#(active(X1), X2, X3)U42#(X1, X2, X3)active#(U102(tt, V1, V2))U103#(isNatIListKind(V2), V1, V2)
U133#(X1, mark(X2), X3, X4)U133#(X1, X2, X3, X4)U102#(X1, mark(X2), X3)U102#(X1, X2, X3)
U101#(active(X1), X2, X3)U101#(X1, X2, X3)active#(U22(tt, V1))U23#(isNat(V1))
mark#(U61(X1, X2))active#(U61(mark(X1), X2))mark#(U105(X1, X2))active#(U105(mark(X1), X2))
cons#(X1, active(X2))cons#(X1, X2)U132#(X1, X2, X3, mark(X4))U132#(X1, X2, X3, X4)
active#(U51(tt, V2))U52#(isNatIListKind(V2))U114#(active(X1), X2)U114#(X1, X2)
U113#(X1, active(X2), X3)U113#(X1, X2, X3)active#(U52(tt))mark#(tt)
U105#(X1, mark(X2))U105#(X1, X2)active#(U113(tt, L, N))isNatKind#(N)
mark#(U61(X1, X2))mark#(X1)active#(isNatIListKind(take(V1, V2)))mark#(U61(isNatKind(V1), V2))
take#(mark(X1), X2)take#(X1, X2)mark#(U101(X1, X2, X3))active#(U101(mark(X1), X2, X3))
U101#(X1, active(X2), X3)U101#(X1, X2, X3)mark#(U21(X1, X2))U21#(mark(X1), X2)
mark#(isNat(X))isNat#(X)active#(U61(tt, V2))isNatIListKind#(V2)
mark#(U135(X1, X2, X3, X4))mark#(X1)isNat#(mark(X))isNat#(X)
mark#(U113(X1, X2, X3))U113#(mark(X1), X2, X3)mark#(U114(X1, X2))active#(U114(mark(X1), X2))
active#(length(cons(N, L)))isNatList#(L)active#(isNatList(nil))mark#(tt)
mark#(U42(X1, X2, X3))active#(U42(mark(X1), X2, X3))U136#(X1, active(X2), X3, X4)U136#(X1, X2, X3, X4)
U131#(X1, X2, mark(X3), X4)U131#(X1, X2, X3, X4)mark#(U102(X1, X2, X3))mark#(X1)
mark#(isNatIListKind(X))active#(isNatIListKind(X))active#(U11(tt, V1))U12#(isNatIListKind(V1), V1)
active#(isNatIList(zeros))mark#(tt)mark#(U111(X1, X2, X3))active#(U111(mark(X1), X2, X3))
U12#(X1, mark(X2))U12#(X1, X2)mark#(length(X))length#(mark(X))
mark#(U134(X1, X2, X3, X4))active#(U134(mark(X1), X2, X3, X4))U121#(mark(X1), X2)U121#(X1, X2)
U104#(mark(X1), X2, X3)U104#(X1, X2, X3)active#(isNat(s(V1)))mark#(U21(isNatKind(V1), V1))
active#(U102(tt, V1, V2))mark#(U103(isNatIListKind(V2), V1, V2))mark#(take(X1, X2))take#(mark(X1), mark(X2))
mark#(U12(X1, X2))U12#(mark(X1), X2)mark#(U103(X1, X2, X3))active#(U103(mark(X1), X2, X3))
active#(U134(tt, IL, M, N))U135#(isNat(N), IL, M, N)active#(U111(tt, L, N))isNatIListKind#(L)
mark#(U111(X1, X2, X3))U111#(mark(X1), X2, X3)active#(take(0, IL))isNatIList#(IL)
mark#(U101(X1, X2, X3))mark#(X1)mark#(U95(X1, X2))U95#(mark(X1), X2)
active#(U41(tt, V1, V2))mark#(U42(isNatKind(V1), V1, V2))isNatIListKind#(active(X))isNatIListKind#(X)
active#(isNatIList(V))isNatIListKind#(V)U46#(active(X))U46#(X)
U134#(X1, active(X2), X3, X4)U134#(X1, X2, X3, X4)U95#(X1, active(X2))U95#(X1, X2)
U44#(active(X1), X2, X3)U44#(X1, X2, X3)active#(U32(tt, V))isNatList#(V)
active#(U95(tt, V2))U96#(isNatList(V2))U105#(active(X1), X2)U105#(X1, X2)
mark#(U44(X1, X2, X3))U44#(mark(X1), X2, X3)active#(U42(tt, V1, V2))isNatIListKind#(V2)
U105#(X1, active(X2))U105#(X1, X2)active#(isNat(length(V1)))mark#(U11(isNatIListKind(V1), V1))
active#(U45(tt, V2))mark#(U46(isNatIList(V2)))U44#(mark(X1), X2, X3)U44#(X1, X2, X3)
U22#(active(X1), X2)U22#(X1, X2)active#(take(s(M), cons(N, IL)))mark#(U131(isNatIList(IL), IL, M, N))
U136#(X1, mark(X2), X3, X4)U136#(X1, X2, X3, X4)mark#(U91(X1, X2, X3))active#(U91(mark(X1), X2, X3))
active#(isNatKind(length(V1)))mark#(U71(isNatIListKind(V1)))active#(U135(tt, IL, M, N))mark#(U136(isNatKind(N), IL, M, N))
mark#(U33(X))U33#(mark(X))U112#(X1, mark(X2), X3)U112#(X1, X2, X3)
active#(isNat(s(V1)))isNatKind#(V1)U11#(X1, active(X2))U11#(X1, X2)
mark#(U45(X1, X2))U45#(mark(X1), X2)mark#(U62(X))mark#(X)
U135#(X1, X2, active(X3), X4)U135#(X1, X2, X3, X4)mark#(U103(X1, X2, X3))U103#(mark(X1), X2, X3)
U103#(mark(X1), X2, X3)U103#(X1, X2, X3)mark#(U91(X1, X2, X3))mark#(X1)
U43#(X1, active(X2), X3)U43#(X1, X2, X3)U43#(X1, mark(X2), X3)U43#(X1, X2, X3)
mark#(tt)active#(tt)cons#(mark(X1), X2)cons#(X1, X2)
U31#(X1, active(X2))U31#(X1, X2)mark#(U96(X))mark#(X)
active#(U114(tt, L))length#(L)mark#(U61(X1, X2))U61#(mark(X1), X2)
U22#(X1, active(X2))U22#(X1, X2)active#(U135(tt, IL, M, N))U136#(isNatKind(N), IL, M, N)
active#(take(s(M), cons(N, IL)))U131#(isNatIList(IL), IL, M, N)mark#(U52(X))active#(U52(mark(X)))
U21#(X1, mark(X2))U21#(X1, X2)mark#(U23(X))mark#(X)
U45#(active(X1), X2)U45#(X1, X2)U132#(X1, mark(X2), X3, X4)U132#(X1, X2, X3, X4)
U62#(mark(X))U62#(X)mark#(length(X))mark#(X)
mark#(U13(X))active#(U13(mark(X)))U135#(X1, X2, mark(X3), X4)U135#(X1, X2, X3, X4)
U114#(mark(X1), X2)U114#(X1, X2)mark#(zeros)active#(zeros)
U111#(X1, active(X2), X3)U111#(X1, X2, X3)active#(U61(tt, V2))U62#(isNatIListKind(V2))
mark#(s(X))active#(s(mark(X)))U132#(X1, X2, active(X3), X4)U132#(X1, X2, X3, X4)
U92#(X1, mark(X2), X3)U92#(X1, X2, X3)mark#(U131(X1, X2, X3, X4))mark#(X1)
U94#(X1, X2, active(X3))U94#(X1, X2, X3)active#(isNatIListKind(nil))mark#(tt)
active#(zeros)cons#(0, zeros)U96#(mark(X))U96#(X)
U113#(active(X1), X2, X3)U113#(X1, X2, X3)U106#(mark(X))U106#(X)
active#(U44(tt, V1, V2))mark#(U45(isNat(V1), V2))mark#(cons(X1, X2))active#(cons(mark(X1), X2))
U134#(X1, X2, X3, mark(X4))U134#(X1, X2, X3, X4)mark#(isNatKind(X))active#(isNatKind(X))
active#(isNatIListKind(zeros))mark#(tt)active#(U121(tt, IL))U122#(isNatIListKind(IL))
active#(isNatIList(V))mark#(U31(isNatIListKind(V), V))active#(U106(tt))mark#(tt)
mark#(U104(X1, X2, X3))mark#(X1)U23#(mark(X))U23#(X)
mark#(U43(X1, X2, X3))U43#(mark(X1), X2, X3)U44#(X1, mark(X2), X3)U44#(X1, X2, X3)
mark#(U52(X))U52#(mark(X))U91#(active(X1), X2, X3)U91#(X1, X2, X3)
U31#(active(X1), X2)U31#(X1, X2)U136#(X1, X2, mark(X3), X4)U136#(X1, X2, X3, X4)
mark#(U31(X1, X2))mark#(X1)U112#(X1, X2, mark(X3))U112#(X1, X2, X3)
U112#(X1, X2, active(X3))U112#(X1, X2, X3)mark#(U23(X))U23#(mark(X))
mark#(U94(X1, X2, X3))active#(U94(mark(X1), X2, X3))mark#(isNatIList(X))active#(isNatIList(X))
U103#(X1, X2, mark(X3))U103#(X1, X2, X3)U133#(X1, X2, active(X3), X4)U133#(X1, X2, X3, X4)
U133#(mark(X1), X2, X3, X4)U133#(X1, X2, X3, X4)mark#(U32(X1, X2))U32#(mark(X1), X2)
mark#(U121(X1, X2))U121#(mark(X1), X2)mark#(U114(X1, X2))mark#(X1)
mark#(isNat(X))active#(isNat(X))active#(isNatIList(cons(V1, V2)))mark#(U41(isNatKind(V1), V1, V2))
active#(U93(tt, V1, V2))isNatIListKind#(V2)active#(isNatList(take(V1, V2)))mark#(U101(isNatKind(V1), V1, V2))
U51#(active(X1), X2)U51#(X1, X2)U112#(X1, active(X2), X3)U112#(X1, X2, X3)
U121#(X1, mark(X2))U121#(X1, X2)mark#(U81(X))U81#(mark(X))
U134#(X1, X2, active(X3), X4)U134#(X1, X2, X3, X4)mark#(U51(X1, X2))mark#(X1)
U101#(mark(X1), X2, X3)U101#(X1, X2, X3)U31#(X1, mark(X2))U31#(X1, X2)
active#(U93(tt, V1, V2))mark#(U94(isNatIListKind(V2), V1, V2))active#(U91(tt, V1, V2))mark#(U92(isNatKind(V1), V1, V2))
mark#(U44(X1, X2, X3))mark#(X1)U32#(X1, mark(X2))U32#(X1, X2)
active#(U112(tt, L, N))isNat#(N)mark#(U92(X1, X2, X3))U92#(mark(X1), X2, X3)
mark#(U11(X1, X2))U11#(mark(X1), X2)mark#(U111(X1, X2, X3))mark#(X1)
mark#(U132(X1, X2, X3, X4))U132#(mark(X1), X2, X3, X4)U111#(X1, X2, active(X3))U111#(X1, X2, X3)
active#(U134(tt, IL, M, N))mark#(U135(isNat(N), IL, M, N))active#(isNatIList(cons(V1, V2)))isNatKind#(V1)
mark#(U113(X1, X2, X3))active#(U113(mark(X1), X2, X3))U31#(mark(X1), X2)U31#(X1, X2)
U134#(X1, X2, X3, active(X4))U134#(X1, X2, X3, X4)U44#(X1, active(X2), X3)U44#(X1, X2, X3)
mark#(U132(X1, X2, X3, X4))mark#(X1)U32#(mark(X1), X2)U32#(X1, X2)
U113#(mark(X1), X2, X3)U113#(X1, X2, X3)active#(zeros)mark#(cons(0, zeros))
s#(active(X))s#(X)active#(isNatIListKind(take(V1, V2)))U61#(isNatKind(V1), V2)
mark#(isNatList(X))active#(isNatList(X))take#(active(X1), X2)take#(X1, X2)
U103#(active(X1), X2, X3)U103#(X1, X2, X3)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U101(tt, V1, V2))mark(U102(isNatKind(V1), V1, V2))
active(U102(tt, V1, V2))mark(U103(isNatIListKind(V2), V1, V2))active(U103(tt, V1, V2))mark(U104(isNatIListKind(V2), V1, V2))
active(U104(tt, V1, V2))mark(U105(isNat(V1), V2))active(U105(tt, V2))mark(U106(isNatIList(V2)))
active(U106(tt))mark(tt)active(U11(tt, V1))mark(U12(isNatIListKind(V1), V1))
active(U111(tt, L, N))mark(U112(isNatIListKind(L), L, N))active(U112(tt, L, N))mark(U113(isNat(N), L, N))
active(U113(tt, L, N))mark(U114(isNatKind(N), L))active(U114(tt, L))mark(s(length(L)))
active(U12(tt, V1))mark(U13(isNatList(V1)))active(U121(tt, IL))mark(U122(isNatIListKind(IL)))
active(U122(tt))mark(nil)active(U13(tt))mark(tt)
active(U131(tt, IL, M, N))mark(U132(isNatIListKind(IL), IL, M, N))active(U132(tt, IL, M, N))mark(U133(isNat(M), IL, M, N))
active(U133(tt, IL, M, N))mark(U134(isNatKind(M), IL, M, N))active(U134(tt, IL, M, N))mark(U135(isNat(N), IL, M, N))
active(U135(tt, IL, M, N))mark(U136(isNatKind(N), IL, M, N))active(U136(tt, IL, M, N))mark(cons(N, take(M, IL)))
active(U21(tt, V1))mark(U22(isNatKind(V1), V1))active(U22(tt, V1))mark(U23(isNat(V1)))
active(U23(tt))mark(tt)active(U31(tt, V))mark(U32(isNatIListKind(V), V))
active(U32(tt, V))mark(U33(isNatList(V)))active(U33(tt))mark(tt)
active(U41(tt, V1, V2))mark(U42(isNatKind(V1), V1, V2))active(U42(tt, V1, V2))mark(U43(isNatIListKind(V2), V1, V2))
active(U43(tt, V1, V2))mark(U44(isNatIListKind(V2), V1, V2))active(U44(tt, V1, V2))mark(U45(isNat(V1), V2))
active(U45(tt, V2))mark(U46(isNatIList(V2)))active(U46(tt))mark(tt)
active(U51(tt, V2))mark(U52(isNatIListKind(V2)))active(U52(tt))mark(tt)
active(U61(tt, V2))mark(U62(isNatIListKind(V2)))active(U62(tt))mark(tt)
active(U71(tt))mark(tt)active(U81(tt))mark(tt)
active(U91(tt, V1, V2))mark(U92(isNatKind(V1), V1, V2))active(U92(tt, V1, V2))mark(U93(isNatIListKind(V2), V1, V2))
active(U93(tt, V1, V2))mark(U94(isNatIListKind(V2), V1, V2))active(U94(tt, V1, V2))mark(U95(isNat(V1), V2))
active(U95(tt, V2))mark(U96(isNatList(V2)))active(U96(tt))mark(tt)
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(isNatKind(V1), V1, V2))
active(isNatIListKind(nil))mark(tt)active(isNatIListKind(zeros))mark(tt)
active(isNatIListKind(cons(V1, V2)))mark(U51(isNatKind(V1), V2))active(isNatIListKind(take(V1, V2)))mark(U61(isNatKind(V1), V2))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(U71(isNatIListKind(V1)))
active(isNatKind(s(V1)))mark(U81(isNatKind(V1)))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U91(isNatKind(V1), V1, V2))active(isNatList(take(V1, V2)))mark(U101(isNatKind(V1), V1, V2))
active(length(nil))mark(0)active(length(cons(N, L)))mark(U111(isNatList(L), L, N))
active(take(0, IL))mark(U121(isNatIList(IL), IL))active(take(s(M), cons(N, IL)))mark(U131(isNatIList(IL), IL, M, N))
mark(zeros)active(zeros)mark(cons(X1, X2))active(cons(mark(X1), X2))
mark(0)active(0)mark(U101(X1, X2, X3))active(U101(mark(X1), X2, X3))
mark(tt)active(tt)mark(U102(X1, X2, X3))active(U102(mark(X1), X2, X3))
mark(isNatKind(X))active(isNatKind(X))mark(U103(X1, X2, X3))active(U103(mark(X1), X2, X3))
mark(isNatIListKind(X))active(isNatIListKind(X))mark(U104(X1, X2, X3))active(U104(mark(X1), X2, X3))
mark(U105(X1, X2))active(U105(mark(X1), X2))mark(isNat(X))active(isNat(X))
mark(U106(X))active(U106(mark(X)))mark(isNatIList(X))active(isNatIList(X))
mark(U11(X1, X2))active(U11(mark(X1), X2))mark(U12(X1, X2))active(U12(mark(X1), X2))
mark(U111(X1, X2, X3))active(U111(mark(X1), X2, X3))mark(U112(X1, X2, X3))active(U112(mark(X1), X2, X3))
mark(U113(X1, X2, X3))active(U113(mark(X1), X2, X3))mark(U114(X1, X2))active(U114(mark(X1), X2))
mark(s(X))active(s(mark(X)))mark(length(X))active(length(mark(X)))
mark(U13(X))active(U13(mark(X)))mark(isNatList(X))active(isNatList(X))
mark(U121(X1, X2))active(U121(mark(X1), X2))mark(U122(X))active(U122(mark(X)))
mark(nil)active(nil)mark(U131(X1, X2, X3, X4))active(U131(mark(X1), X2, X3, X4))
mark(U132(X1, X2, X3, X4))active(U132(mark(X1), X2, X3, X4))mark(U133(X1, X2, X3, X4))active(U133(mark(X1), X2, X3, X4))
mark(U134(X1, X2, X3, X4))active(U134(mark(X1), X2, X3, X4))mark(U135(X1, X2, X3, X4))active(U135(mark(X1), X2, X3, X4))
mark(U136(X1, X2, X3, X4))active(U136(mark(X1), X2, X3, X4))mark(take(X1, X2))active(take(mark(X1), mark(X2)))
mark(U21(X1, X2))active(U21(mark(X1), X2))mark(U22(X1, X2))active(U22(mark(X1), X2))
mark(U23(X))active(U23(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(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))active(U51(mark(X1), X2))mark(U52(X))active(U52(mark(X)))
mark(U61(X1, X2))active(U61(mark(X1), X2))mark(U62(X))active(U62(mark(X)))
mark(U71(X))active(U71(mark(X)))mark(U81(X))active(U81(mark(X)))
mark(U91(X1, X2, X3))active(U91(mark(X1), X2, X3))mark(U92(X1, X2, X3))active(U92(mark(X1), X2, X3))
mark(U93(X1, X2, X3))active(U93(mark(X1), X2, X3))mark(U94(X1, X2, X3))active(U94(mark(X1), X2, X3))
mark(U95(X1, X2))active(U95(mark(X1), X2))mark(U96(X))active(U96(mark(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)
U101(mark(X1), X2, X3)U101(X1, X2, X3)U101(X1, mark(X2), X3)U101(X1, X2, X3)
U101(X1, X2, mark(X3))U101(X1, X2, X3)U101(active(X1), X2, X3)U101(X1, X2, X3)
U101(X1, active(X2), X3)U101(X1, X2, X3)U101(X1, X2, active(X3))U101(X1, X2, X3)
U102(mark(X1), X2, X3)U102(X1, X2, X3)U102(X1, mark(X2), X3)U102(X1, X2, X3)
U102(X1, X2, mark(X3))U102(X1, X2, X3)U102(active(X1), X2, X3)U102(X1, X2, X3)
U102(X1, active(X2), X3)U102(X1, X2, X3)U102(X1, X2, active(X3))U102(X1, X2, X3)
isNatKind(mark(X))isNatKind(X)isNatKind(active(X))isNatKind(X)
U103(mark(X1), X2, X3)U103(X1, X2, X3)U103(X1, mark(X2), X3)U103(X1, X2, X3)
U103(X1, X2, mark(X3))U103(X1, X2, X3)U103(active(X1), X2, X3)U103(X1, X2, X3)
U103(X1, active(X2), X3)U103(X1, X2, X3)U103(X1, X2, active(X3))U103(X1, X2, X3)
isNatIListKind(mark(X))isNatIListKind(X)isNatIListKind(active(X))isNatIListKind(X)
U104(mark(X1), X2, X3)U104(X1, X2, X3)U104(X1, mark(X2), X3)U104(X1, X2, X3)
U104(X1, X2, mark(X3))U104(X1, X2, X3)U104(active(X1), X2, X3)U104(X1, X2, X3)
U104(X1, active(X2), X3)U104(X1, X2, X3)U104(X1, X2, active(X3))U104(X1, X2, X3)
U105(mark(X1), X2)U105(X1, X2)U105(X1, mark(X2))U105(X1, X2)
U105(active(X1), X2)U105(X1, X2)U105(X1, active(X2))U105(X1, X2)
isNat(mark(X))isNat(X)isNat(active(X))isNat(X)
U106(mark(X))U106(X)U106(active(X))U106(X)
isNatIList(mark(X))isNatIList(X)isNatIList(active(X))isNatIList(X)
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)
U111(mark(X1), X2, X3)U111(X1, X2, X3)U111(X1, mark(X2), X3)U111(X1, X2, X3)
U111(X1, X2, mark(X3))U111(X1, X2, X3)U111(active(X1), X2, X3)U111(X1, X2, X3)
U111(X1, active(X2), X3)U111(X1, X2, X3)U111(X1, X2, active(X3))U111(X1, X2, X3)
U112(mark(X1), X2, X3)U112(X1, X2, X3)U112(X1, mark(X2), X3)U112(X1, X2, X3)
U112(X1, X2, mark(X3))U112(X1, X2, X3)U112(active(X1), X2, X3)U112(X1, X2, X3)
U112(X1, active(X2), X3)U112(X1, X2, X3)U112(X1, X2, active(X3))U112(X1, X2, X3)
U113(mark(X1), X2, X3)U113(X1, X2, X3)U113(X1, mark(X2), X3)U113(X1, X2, X3)
U113(X1, X2, mark(X3))U113(X1, X2, X3)U113(active(X1), X2, X3)U113(X1, X2, X3)
U113(X1, active(X2), X3)U113(X1, X2, X3)U113(X1, X2, active(X3))U113(X1, X2, X3)
U114(mark(X1), X2)U114(X1, X2)U114(X1, mark(X2))U114(X1, X2)
U114(active(X1), X2)U114(X1, X2)U114(X1, active(X2))U114(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
length(mark(X))length(X)length(active(X))length(X)
U13(mark(X))U13(X)U13(active(X))U13(X)
isNatList(mark(X))isNatList(X)isNatList(active(X))isNatList(X)
U121(mark(X1), X2)U121(X1, X2)U121(X1, mark(X2))U121(X1, X2)
U121(active(X1), X2)U121(X1, X2)U121(X1, active(X2))U121(X1, X2)
U122(mark(X))U122(X)U122(active(X))U122(X)
U131(mark(X1), X2, X3, X4)U131(X1, X2, X3, X4)U131(X1, mark(X2), X3, X4)U131(X1, X2, X3, X4)
U131(X1, X2, mark(X3), X4)U131(X1, X2, X3, X4)U131(X1, X2, X3, mark(X4))U131(X1, X2, X3, X4)
U131(active(X1), X2, X3, X4)U131(X1, X2, X3, X4)U131(X1, active(X2), X3, X4)U131(X1, X2, X3, X4)
U131(X1, X2, active(X3), X4)U131(X1, X2, X3, X4)U131(X1, X2, X3, active(X4))U131(X1, X2, X3, X4)
U132(mark(X1), X2, X3, X4)U132(X1, X2, X3, X4)U132(X1, mark(X2), X3, X4)U132(X1, X2, X3, X4)
U132(X1, X2, mark(X3), X4)U132(X1, X2, X3, X4)U132(X1, X2, X3, mark(X4))U132(X1, X2, X3, X4)
U132(active(X1), X2, X3, X4)U132(X1, X2, X3, X4)U132(X1, active(X2), X3, X4)U132(X1, X2, X3, X4)
U132(X1, X2, active(X3), X4)U132(X1, X2, X3, X4)U132(X1, X2, X3, active(X4))U132(X1, X2, X3, X4)
U133(mark(X1), X2, X3, X4)U133(X1, X2, X3, X4)U133(X1, mark(X2), X3, X4)U133(X1, X2, X3, X4)
U133(X1, X2, mark(X3), X4)U133(X1, X2, X3, X4)U133(X1, X2, X3, mark(X4))U133(X1, X2, X3, X4)
U133(active(X1), X2, X3, X4)U133(X1, X2, X3, X4)U133(X1, active(X2), X3, X4)U133(X1, X2, X3, X4)
U133(X1, X2, active(X3), X4)U133(X1, X2, X3, X4)U133(X1, X2, X3, active(X4))U133(X1, X2, X3, X4)
U134(mark(X1), X2, X3, X4)U134(X1, X2, X3, X4)U134(X1, mark(X2), X3, X4)U134(X1, X2, X3, X4)
U134(X1, X2, mark(X3), X4)U134(X1, X2, X3, X4)U134(X1, X2, X3, mark(X4))U134(X1, X2, X3, X4)
U134(active(X1), X2, X3, X4)U134(X1, X2, X3, X4)U134(X1, active(X2), X3, X4)U134(X1, X2, X3, X4)
U134(X1, X2, active(X3), X4)U134(X1, X2, X3, X4)U134(X1, X2, X3, active(X4))U134(X1, X2, X3, X4)
U135(mark(X1), X2, X3, X4)U135(X1, X2, X3, X4)U135(X1, mark(X2), X3, X4)U135(X1, X2, X3, X4)
U135(X1, X2, mark(X3), X4)U135(X1, X2, X3, X4)U135(X1, X2, X3, mark(X4))U135(X1, X2, X3, X4)
U135(active(X1), X2, X3, X4)U135(X1, X2, X3, X4)U135(X1, active(X2), X3, X4)U135(X1, X2, X3, X4)
U135(X1, X2, active(X3), X4)U135(X1, X2, X3, X4)U135(X1, X2, X3, active(X4))U135(X1, X2, X3, X4)
U136(mark(X1), X2, X3, X4)U136(X1, X2, X3, X4)U136(X1, mark(X2), X3, X4)U136(X1, X2, X3, X4)
U136(X1, X2, mark(X3), X4)U136(X1, X2, X3, X4)U136(X1, X2, X3, mark(X4))U136(X1, X2, X3, X4)
U136(active(X1), X2, X3, X4)U136(X1, X2, X3, X4)U136(X1, active(X2), X3, X4)U136(X1, X2, X3, X4)
U136(X1, X2, active(X3), X4)U136(X1, X2, X3, X4)U136(X1, X2, X3, active(X4))U136(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)
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(X1), X2)U22(X1, X2)U22(X1, mark(X2))U22(X1, X2)
U22(active(X1), X2)U22(X1, X2)U22(X1, active(X2))U22(X1, X2)
U23(mark(X))U23(X)U23(active(X))U23(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)
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)U51(X1, X2)U51(X1, mark(X2))U51(X1, X2)
U51(active(X1), X2)U51(X1, X2)U51(X1, active(X2))U51(X1, X2)
U52(mark(X))U52(X)U52(active(X))U52(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(X))U62(X)U62(active(X))U62(X)
U71(mark(X))U71(X)U71(active(X))U71(X)
U81(mark(X))U81(X)U81(active(X))U81(X)
U91(mark(X1), X2, X3)U91(X1, X2, X3)U91(X1, mark(X2), X3)U91(X1, X2, X3)
U91(X1, X2, mark(X3))U91(X1, X2, X3)U91(active(X1), X2, X3)U91(X1, X2, X3)
U91(X1, active(X2), X3)U91(X1, X2, X3)U91(X1, X2, active(X3))U91(X1, X2, X3)
U92(mark(X1), X2, X3)U92(X1, X2, X3)U92(X1, mark(X2), X3)U92(X1, X2, X3)
U92(X1, X2, mark(X3))U92(X1, X2, X3)U92(active(X1), X2, X3)U92(X1, X2, X3)
U92(X1, active(X2), X3)U92(X1, X2, X3)U92(X1, X2, active(X3))U92(X1, X2, X3)
U93(mark(X1), X2, X3)U93(X1, X2, X3)U93(X1, mark(X2), X3)U93(X1, X2, X3)
U93(X1, X2, mark(X3))U93(X1, X2, X3)U93(active(X1), X2, X3)U93(X1, X2, X3)
U93(X1, active(X2), X3)U93(X1, X2, X3)U93(X1, X2, active(X3))U93(X1, X2, X3)
U94(mark(X1), X2, X3)U94(X1, X2, X3)U94(X1, mark(X2), X3)U94(X1, X2, X3)
U94(X1, X2, mark(X3))U94(X1, X2, X3)U94(active(X1), X2, X3)U94(X1, X2, X3)
U94(X1, active(X2), X3)U94(X1, X2, X3)U94(X1, X2, active(X3))U94(X1, X2, X3)
U95(mark(X1), X2)U95(X1, X2)U95(X1, mark(X2))U95(X1, X2)
U95(active(X1), X2)U95(X1, X2)U95(X1, active(X2))U95(X1, X2)
U96(mark(X))U96(X)U96(active(X))U96(X)

Original Signature

Termination of terms over the following signature is verified: U104, U105, U106, U112, U111, U62, U114, U61, U113, U23, U21, U22, isNatIList, isNatKind, mark, U71, 0, U122, U121, zeros, active, U31, U32, U33, isNatIListKind, U96, U94, U95, isNat, U46, U45, U132, U44, U131, U43, U93, U134, U42, U92, U133, U41, U91, U136, U135, length, cons, isNatList, s, U51, tt, take, U81, U52, U11, U12, U13, U102, U103, U101, nil