TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (2874ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (3ms), DependencyGraph (1355ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (1117ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (1074ms), ReductionPairSAT (timeout)].

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))U91#(tt, IL, M, N) → activate#(M)
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)length#(cons(N, L)) → isNatList#(activate(L))
isNat#(n__length(V1)) → isNatList#(activate(V1))isNatList#(n__take(V1, V2)) → activate#(V2)
U41#(tt, V2) → isNatIList#(activate(V2))U72#(tt, L) → length#(activate(L))
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)) → isNat#(activate(V1))isNatIList#(n__cons(V1, V2)) → activate#(V2)
U51#(tt, V2) → isNatList#(activate(V2))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)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__length(X)) → length#(X)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)activate#(n__take(X1, X2)) → take#(X1, X2)
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)

Rewrite Rules

zeros → cons(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)zeros → n__zeros
take(X1, X2) → n__take(X1, X2)0 → n__0
length(X) → n__length(X)s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)nil → n__nil
activate(n__zeros) → zerosactivate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)activate(n__cons(X1, X2)) → cons(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))
U91#(tt, IL, M, N) → activate#(M)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) → cons#(activate(N), n__take(activate(M), activate(IL)))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)U61#(tt, V2) → U62#(isNatIList(activate(V2)))
length#(cons(N, L)) → isNatList#(activate(L))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))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)))
U91#(tt, IL, M, N) → isNat#(activate(M))U41#(tt, V2) → activate#(V2)
U51#(tt, V2) → U52#(isNatList(activate(V2)))U91#(tt, IL, M, N) → U92#(isNat(activate(M)), activate(IL), activate(M), activate(N))
U61#(tt, V2) → activate#(V2)isNatIList#(V) → activate#(V)
activate#(n__cons(X1, X2)) → cons#(X1, 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__s(X)) → s#(X)
activate#(n__length(X)) → length#(X)activate#(n__nil) → nil#
U72#(tt, L) → s#(length(activate(L)))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)activate#(n__take(X1, X2)) → take#(X1, X2)
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)

Rewrite Rules

zeros → cons(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)zeros → n__zeros
take(X1, X2) → n__take(X1, X2)0 → n__0
length(X) → n__length(X)s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)nil → n__nil
activate(n__zeros) → zerosactivate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)activate(n__cons(X1, X2)) → cons(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))U91#(tt, IL, M, N) → activate#(M)
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)length#(cons(N, L)) → isNatList#(activate(L))
U41#(tt, V2) → isNatIList#(activate(V2))isNatList#(n__take(V1, V2)) → activate#(V2)
isNat#(n__length(V1)) → isNatList#(activate(V1))U72#(tt, L) → length#(activate(L))
isNatIList#(n__cons(V1, V2)) → isNat#(activate(V1))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)) → activate#(V2)
U51#(tt, V2) → isNatList#(activate(V2))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))
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__length(X)) → length#(X)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)activate#(n__take(X1, X2)) → take#(X1, X2)
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)