TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3368ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (1580ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (1450ms), PolynomialLinearRange8NegiUR (30033ms), DependencyGraph (timeout), ReductionPairSAT (13527ms)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

take#(s(M), cons(N, IL))isNatIList#(activate(IL))isNatList#(n__take(V1, V2))activate#(V1)
isNatList#(n__cons(V1, V2))isNat#(activate(V1))isNatList#(n__take(V1, V2))U61#(isNat(activate(V1)), activate(V2))
U61#(tt, V2)isNatIList#(activate(V2))activate#(n__take(X1, X2))take#(activate(X1), activate(X2))
U91#(tt, IL, M, N)activate#(M)activate#(n__cons(X1, X2))activate#(X1)
U92#(tt, IL, M, N)activate#(IL)isNatIList#(n__cons(V1, V2))U41#(isNat(activate(V1)), activate(V2))
U72#(tt, L)activate#(L)U93#(tt, IL, M, N)activate#(N)
U51#(tt, V2)activate#(V2)isNat#(n__s(V1))activate#(V1)
isNat#(n__length(V1))activate#(V1)isNatList#(n__cons(V1, V2))activate#(V2)
U92#(tt, IL, M, N)activate#(N)U93#(tt, IL, M, N)activate#(M)
isNatList#(n__take(V1, V2))isNat#(activate(V1))length#(cons(N, L))U71#(isNatList(activate(L)), activate(L), N)
U91#(tt, IL, M, N)activate#(N)activate#(n__length(X))length#(activate(X))
length#(cons(N, L))isNatList#(activate(L))isNatList#(n__take(V1, V2))activate#(V2)
isNat#(n__length(V1))isNatList#(activate(V1))U41#(tt, V2)isNatIList#(activate(V2))
U72#(tt, L)length#(activate(L))isNatIList#(n__cons(V1, V2))isNat#(activate(V1))
take#(s(M), cons(N, IL))U91#(isNatIList(activate(IL)), activate(IL), M, N)take#(s(M), cons(N, IL))activate#(IL)
isNatIList#(n__cons(V1, V2))activate#(V2)U51#(tt, V2)isNatList#(activate(V2))
activate#(n__length(X))activate#(X)activate#(n__s(X))activate#(X)
U92#(tt, IL, M, N)activate#(M)U93#(tt, IL, M, N)activate#(IL)
U41#(tt, V2)activate#(V2)U91#(tt, IL, M, N)isNat#(activate(M))
isNatIList#(V)activate#(V)U61#(tt, V2)activate#(V2)
U91#(tt, IL, M, N)U92#(isNat(activate(M)), activate(IL), activate(M), activate(N))activate#(n__take(X1, X2))activate#(X2)
U91#(tt, IL, M, N)activate#(IL)isNatIList#(V)isNatList#(activate(V))
U71#(tt, L, N)U72#(isNat(activate(N)), activate(L))U71#(tt, L, N)activate#(N)
U92#(tt, IL, M, N)U93#(isNat(activate(N)), activate(IL), activate(M), activate(N))U92#(tt, IL, M, N)isNat#(activate(N))
activate#(n__take(X1, X2))activate#(X1)isNat#(n__s(V1))isNat#(activate(V1))
isNatList#(n__cons(V1, V2))U51#(isNat(activate(V1)), activate(V2))U71#(tt, L, N)activate#(L)
isNatList#(n__cons(V1, V2))activate#(V1)take#(0, IL)isNatIList#(IL)
U71#(tt, L, N)isNat#(activate(N))isNatIList#(n__cons(V1, V2))activate#(V1)
length#(cons(N, L))activate#(L)

Rewrite Rules

zeroscons(0, n__zeros)U11(tt)tt
U21(tt)ttU31(tt)tt
U41(tt, V2)U42(isNatIList(activate(V2)))U42(tt)tt
U51(tt, V2)U52(isNatList(activate(V2)))U52(tt)tt
U61(tt, V2)U62(isNatIList(activate(V2)))U62(tt)tt
U71(tt, L, N)U72(isNat(activate(N)), activate(L))U72(tt, L)s(length(activate(L)))
U81(tt)nilU91(tt, IL, M, N)U92(isNat(activate(M)), activate(IL), activate(M), activate(N))
U92(tt, IL, M, N)U93(isNat(activate(N)), activate(IL), activate(M), activate(N))U93(tt, IL, M, N)cons(activate(N), n__take(activate(M), activate(IL)))
isNat(n__0)ttisNat(n__length(V1))U11(isNatList(activate(V1)))
isNat(n__s(V1))U21(isNat(activate(V1)))isNatIList(V)U31(isNatList(activate(V)))
isNatIList(n__zeros)ttisNatIList(n__cons(V1, V2))U41(isNat(activate(V1)), activate(V2))
isNatList(n__nil)ttisNatList(n__cons(V1, V2))U51(isNat(activate(V1)), activate(V2))
isNatList(n__take(V1, V2))U61(isNat(activate(V1)), activate(V2))length(nil)0
length(cons(N, L))U71(isNatList(activate(L)), activate(L), N)take(0, IL)U81(isNatIList(IL))
take(s(M), cons(N, IL))U91(isNatIList(activate(IL)), activate(IL), M, N)zerosn__zeros
take(X1, X2)n__take(X1, X2)0n__0
length(X)n__length(X)s(X)n__s(X)
cons(X1, X2)n__cons(X1, X2)niln__nil
activate(n__zeros)zerosactivate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__0)0activate(n__length(X))length(activate(X))
activate(n__s(X))s(activate(X))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(X)X

Original Signature

Termination of terms over the following signature is verified: n__s, activate, isNat, U62, n__0, U61, U93, U42, U41, U92, U91, length, n__nil, n__zeros, U21, cons, isNatIList, n__length, n__take, U71, n__cons, U72, 0, isNatList, U51, s, tt, zeros, take, U52, U81, U11, U31, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

take#(s(M), cons(N, IL))isNatIList#(activate(IL))zeros#0#
isNatList#(n__take(V1, V2))activate#(V1)isNatList#(n__cons(V1, V2))isNat#(activate(V1))
isNatList#(n__take(V1, V2))U61#(isNat(activate(V1)), activate(V2))U61#(tt, V2)isNatIList#(activate(V2))
activate#(n__take(X1, X2))take#(activate(X1), activate(X2))activate#(n__cons(X1, X2))cons#(activate(X1), X2)
U91#(tt, IL, M, N)activate#(M)activate#(n__cons(X1, X2))activate#(X1)
U92#(tt, IL, M, N)activate#(IL)isNatIList#(n__cons(V1, V2))U41#(isNat(activate(V1)), activate(V2))
U93#(tt, IL, M, N)cons#(activate(N), n__take(activate(M), activate(IL)))U72#(tt, L)activate#(L)
U93#(tt, IL, M, N)activate#(N)U51#(tt, V2)activate#(V2)
isNat#(n__s(V1))activate#(V1)isNat#(n__length(V1))activate#(V1)
U81#(tt)nil#length#(nil)0#
isNatList#(n__cons(V1, V2))activate#(V2)U92#(tt, IL, M, N)activate#(N)
U93#(tt, IL, M, N)activate#(M)isNatList#(n__take(V1, V2))isNat#(activate(V1))
length#(cons(N, L))U71#(isNatList(activate(L)), activate(L), N)U91#(tt, IL, M, N)activate#(N)
activate#(n__length(X))length#(activate(X))length#(cons(N, L))isNatList#(activate(L))
U61#(tt, V2)U62#(isNatIList(activate(V2)))isNatList#(n__take(V1, V2))activate#(V2)
U41#(tt, V2)isNatIList#(activate(V2))isNat#(n__length(V1))isNatList#(activate(V1))
isNat#(n__s(V1))U21#(isNat(activate(V1)))U72#(tt, L)length#(activate(L))
activate#(n__0)0#take#(s(M), cons(N, IL))activate#(IL)
take#(s(M), cons(N, IL))U91#(isNatIList(activate(IL)), activate(IL), M, N)isNatIList#(n__cons(V1, V2))isNat#(activate(V1))
activate#(n__zeros)zeros#isNatIList#(n__cons(V1, V2))activate#(V2)
U51#(tt, V2)isNatList#(activate(V2))activate#(n__length(X))activate#(X)
activate#(n__s(X))activate#(X)U92#(tt, IL, M, N)activate#(M)
take#(0, IL)U81#(isNatIList(IL))U93#(tt, IL, M, N)activate#(IL)
isNat#(n__length(V1))U11#(isNatList(activate(V1)))U41#(tt, V2)U42#(isNatIList(activate(V2)))
U41#(tt, V2)activate#(V2)U91#(tt, IL, M, N)isNat#(activate(M))
U51#(tt, V2)U52#(isNatList(activate(V2)))isNatIList#(V)activate#(V)
U61#(tt, V2)activate#(V2)U91#(tt, IL, M, N)U92#(isNat(activate(M)), activate(IL), activate(M), activate(N))
activate#(n__take(X1, X2))activate#(X2)U91#(tt, IL, M, N)activate#(IL)
isNatIList#(V)isNatList#(activate(V))U71#(tt, L, N)U72#(isNat(activate(N)), activate(L))
zeros#cons#(0, n__zeros)U71#(tt, L, N)activate#(N)
isNatIList#(V)U31#(isNatList(activate(V)))U92#(tt, IL, M, N)U93#(isNat(activate(N)), activate(IL), activate(M), activate(N))
U92#(tt, IL, M, N)isNat#(activate(N))activate#(n__nil)nil#
U72#(tt, L)s#(length(activate(L)))activate#(n__take(X1, X2))activate#(X1)
isNat#(n__s(V1))isNat#(activate(V1))isNatList#(n__cons(V1, V2))U51#(isNat(activate(V1)), activate(V2))
isNatList#(n__cons(V1, V2))activate#(V1)U71#(tt, L, N)activate#(L)
U71#(tt, L, N)isNat#(activate(N))take#(0, IL)isNatIList#(IL)
activate#(n__s(X))s#(activate(X))isNatIList#(n__cons(V1, V2))activate#(V1)
length#(cons(N, L))activate#(L)

Rewrite Rules

zeroscons(0, n__zeros)U11(tt)tt
U21(tt)ttU31(tt)tt
U41(tt, V2)U42(isNatIList(activate(V2)))U42(tt)tt
U51(tt, V2)U52(isNatList(activate(V2)))U52(tt)tt
U61(tt, V2)U62(isNatIList(activate(V2)))U62(tt)tt
U71(tt, L, N)U72(isNat(activate(N)), activate(L))U72(tt, L)s(length(activate(L)))
U81(tt)nilU91(tt, IL, M, N)U92(isNat(activate(M)), activate(IL), activate(M), activate(N))
U92(tt, IL, M, N)U93(isNat(activate(N)), activate(IL), activate(M), activate(N))U93(tt, IL, M, N)cons(activate(N), n__take(activate(M), activate(IL)))
isNat(n__0)ttisNat(n__length(V1))U11(isNatList(activate(V1)))
isNat(n__s(V1))U21(isNat(activate(V1)))isNatIList(V)U31(isNatList(activate(V)))
isNatIList(n__zeros)ttisNatIList(n__cons(V1, V2))U41(isNat(activate(V1)), activate(V2))
isNatList(n__nil)ttisNatList(n__cons(V1, V2))U51(isNat(activate(V1)), activate(V2))
isNatList(n__take(V1, V2))U61(isNat(activate(V1)), activate(V2))length(nil)0
length(cons(N, L))U71(isNatList(activate(L)), activate(L), N)take(0, IL)U81(isNatIList(IL))
take(s(M), cons(N, IL))U91(isNatIList(activate(IL)), activate(IL), M, N)zerosn__zeros
take(X1, X2)n__take(X1, X2)0n__0
length(X)n__length(X)s(X)n__s(X)
cons(X1, X2)n__cons(X1, X2)niln__nil
activate(n__zeros)zerosactivate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__0)0activate(n__length(X))length(activate(X))
activate(n__s(X))s(activate(X))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__nil)nilactivate(X)X

Original Signature

Termination of terms over the following signature is verified: isNat, activate, n__s, U62, U61, n__0, U42, U93, U92, U41, U91, length, n__nil, n__zeros, U21, cons, isNatIList, n__length, n__take, U71, n__cons, U72, 0, s, isNatList, U51, zeros, tt, take, U81, U52, U11, U31, nil

Strategy


The following SCCs where found

take#(s(M), cons(N, IL)) → isNatIList#(activate(IL))isNatList#(n__take(V1, V2)) → activate#(V1)
isNatList#(n__cons(V1, V2)) → isNat#(activate(V1))isNatList#(n__take(V1, V2)) → U61#(isNat(activate(V1)), activate(V2))
U61#(tt, V2) → isNatIList#(activate(V2))activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2))
U91#(tt, IL, M, N) → activate#(M)activate#(n__cons(X1, X2)) → activate#(X1)
U92#(tt, IL, M, N) → activate#(IL)isNatIList#(n__cons(V1, V2)) → U41#(isNat(activate(V1)), activate(V2))
U72#(tt, L) → activate#(L)U93#(tt, IL, M, N) → activate#(N)
U51#(tt, V2) → activate#(V2)isNat#(n__length(V1)) → activate#(V1)
isNat#(n__s(V1)) → activate#(V1)isNatList#(n__cons(V1, V2)) → activate#(V2)
U92#(tt, IL, M, N) → activate#(N)U93#(tt, IL, M, N) → activate#(M)
isNatList#(n__take(V1, V2)) → isNat#(activate(V1))length#(cons(N, L)) → U71#(isNatList(activate(L)), activate(L), N)
U91#(tt, IL, M, N) → activate#(N)activate#(n__length(X)) → length#(activate(X))
length#(cons(N, L)) → isNatList#(activate(L))U41#(tt, V2) → isNatIList#(activate(V2))
isNat#(n__length(V1)) → isNatList#(activate(V1))isNatList#(n__take(V1, V2)) → activate#(V2)
U72#(tt, L) → length#(activate(L))take#(s(M), cons(N, IL)) → activate#(IL)
take#(s(M), cons(N, IL)) → U91#(isNatIList(activate(IL)), activate(IL), M, N)isNatIList#(n__cons(V1, V2)) → isNat#(activate(V1))
isNatIList#(n__cons(V1, V2)) → activate#(V2)U51#(tt, V2) → isNatList#(activate(V2))
activate#(n__length(X)) → activate#(X)activate#(n__s(X)) → activate#(X)
U92#(tt, IL, M, N) → activate#(M)U93#(tt, IL, M, N) → activate#(IL)
U91#(tt, IL, M, N) → isNat#(activate(M))U41#(tt, V2) → activate#(V2)
activate#(n__take(X1, X2)) → activate#(X2)U91#(tt, IL, M, N) → U92#(isNat(activate(M)), activate(IL), activate(M), activate(N))
U61#(tt, V2) → activate#(V2)isNatIList#(V) → activate#(V)
U91#(tt, IL, M, N) → activate#(IL)isNatIList#(V) → isNatList#(activate(V))
U71#(tt, L, N) → U72#(isNat(activate(N)), activate(L))U71#(tt, L, N) → activate#(N)
U92#(tt, IL, M, N) → U93#(isNat(activate(N)), activate(IL), activate(M), activate(N))U92#(tt, IL, M, N) → isNat#(activate(N))
activate#(n__take(X1, X2)) → activate#(X1)isNat#(n__s(V1)) → isNat#(activate(V1))
isNatList#(n__cons(V1, V2)) → U51#(isNat(activate(V1)), activate(V2))isNatList#(n__cons(V1, V2)) → activate#(V1)
U71#(tt, L, N) → activate#(L)U71#(tt, L, N) → isNat#(activate(N))
take#(0, IL) → isNatIList#(IL)isNatIList#(n__cons(V1, V2)) → activate#(V1)
length#(cons(N, L)) → activate#(L)