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 (1562ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (709ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (560ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (601ms), ReductionPairSAT (13012ms), DependencyGraph (577ms), SizeChangePrinciple (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(N, IL))isNat#(activate(N))
length#(cons(N, L))isNat#(N)activate#(n__length(X))activate#(X)
isNatList#(n__take(N, IL))activate#(IL)activate#(n__s(X))activate#(X)
uLength#(tt, L)length#(activate(L))isNatList#(n__take(N, IL))isNatIList#(activate(IL))
uTake2#(tt, M, N, IL)activate#(IL)activate#(n__take(X1, X2))take#(activate(X1), activate(X2))
isNat#(n__length(L))isNatList#(activate(L))isNatList#(n__cons(N, L))isNatList#(activate(L))
uTake2#(tt, M, N, IL)activate#(M)activate#(n__cons(X1, X2))activate#(X1)
isNatIList#(IL)activate#(IL)isNatIList#(n__cons(N, IL))isNat#(activate(N))
isNat#(n__s(N))isNat#(activate(N))take#(s(M), cons(N, IL))isNat#(N)
isNatList#(n__cons(N, L))activate#(L)activate#(n__take(X1, X2))activate#(X2)
isNat#(n__length(L))activate#(L)length#(cons(N, L))uLength#(and(isNat(N), isNatList(activate(L))), activate(L))
isNatList#(n__take(N, IL))activate#(N)isNatList#(n__cons(N, L))activate#(N)
isNatIList#(n__cons(N, IL))isNatIList#(activate(IL))isNatIList#(IL)isNatList#(activate(IL))
uLength#(tt, L)activate#(L)isNat#(n__s(N))activate#(N)
take#(s(M), cons(N, IL))uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))activate#(n__length(X))length#(activate(X))
isNatIList#(n__cons(N, IL))activate#(IL)uTake2#(tt, M, N, IL)activate#(N)
length#(cons(N, L))isNatList#(activate(L))isNatList#(n__cons(N, L))isNat#(activate(N))
activate#(n__take(X1, X2))activate#(X1)isNatIList#(n__cons(N, IL))activate#(N)
take#(s(M), cons(N, IL))activate#(IL)take#(0, IL)isNatIList#(IL)
take#(s(M), cons(N, IL))isNat#(M)length#(cons(N, L))activate#(L)

Rewrite Rules

and(tt, T)TisNatIList(IL)isNatList(activate(IL))
isNat(n__0)ttisNat(n__s(N))isNat(activate(N))
isNat(n__length(L))isNatList(activate(L))isNatIList(n__zeros)tt
isNatIList(n__cons(N, IL))and(isNat(activate(N)), isNatIList(activate(IL)))isNatList(n__nil)tt
isNatList(n__cons(N, L))and(isNat(activate(N)), isNatList(activate(L)))isNatList(n__take(N, IL))and(isNat(activate(N)), isNatIList(activate(IL)))
zeroscons(0, n__zeros)take(0, IL)uTake1(isNatIList(IL))
uTake1(tt)niltake(s(M), cons(N, IL))uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL)cons(activate(N), n__take(activate(M), activate(IL)))length(cons(N, L))uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L)s(length(activate(L)))0n__0
s(X)n__s(X)length(X)n__length(X)
zerosn__zeroscons(X1, X2)n__cons(X1, X2)
niln__niltake(X1, X2)n__take(X1, X2)
activate(n__0)0activate(n__s(X))s(activate(X))
activate(n__length(X))length(activate(X))activate(n__zeros)zeros
activate(n__cons(X1, X2))cons(activate(X1), X2)activate(n__nil)nil
activate(n__take(X1, X2))take(activate(X1), activate(X2))activate(X)X

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, n__length, n__take, and, uTake1, activate, isNat, n__s, n__cons, uTake2, 0, n__0, s, isNatList, zeros, tt, take, length, n__nil, n__zeros, nil, cons


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

take#(s(M), cons(N, IL))isNatIList#(activate(IL))isNatList#(n__take(N, IL))isNat#(activate(N))
zeros#0#uLength#(tt, L)length#(activate(L))
uTake1#(tt)nil#activate#(n__take(X1, X2))take#(activate(X1), activate(X2))
uTake2#(tt, M, N, IL)activate#(IL)activate#(n__cons(X1, X2))cons#(activate(X1), X2)
uTake2#(tt, M, N, IL)activate#(M)activate#(n__cons(X1, X2))activate#(X1)
take#(s(M), cons(N, IL))and#(isNat(N), isNatIList(activate(IL)))isNat#(n__s(N))isNat#(activate(N))
isNatList#(n__cons(N, L))activate#(L)isNat#(n__length(L))activate#(L)
isNatList#(n__take(N, IL))activate#(N)uLength#(tt, L)s#(length(activate(L)))
isNatList#(n__cons(N, L))activate#(N)isNatIList#(n__cons(N, IL))and#(isNat(activate(N)), isNatIList(activate(IL)))
isNatIList#(IL)isNatList#(activate(IL))uLength#(tt, L)activate#(L)
isNat#(n__s(N))activate#(N)take#(s(M), cons(N, IL))uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
activate#(n__length(X))length#(activate(X))length#(cons(N, L))isNatList#(activate(L))
uTake2#(tt, M, N, IL)activate#(N)isNatIList#(n__cons(N, IL))activate#(N)
activate#(n__0)0#take#(s(M), cons(N, IL))activate#(IL)
activate#(n__zeros)zeros#length#(cons(N, L))isNat#(N)
activate#(n__length(X))activate#(X)isNatList#(n__take(N, IL))activate#(IL)
activate#(n__s(X))activate#(X)take#(s(M), cons(N, IL))and#(isNat(M), and(isNat(N), isNatIList(activate(IL))))
isNatList#(n__take(N, IL))isNatIList#(activate(IL))uTake2#(tt, M, N, IL)cons#(activate(N), n__take(activate(M), activate(IL)))
isNat#(n__length(L))isNatList#(activate(L))isNatList#(n__cons(N, L))isNatList#(activate(L))
isNatIList#(IL)activate#(IL)isNatIList#(n__cons(N, IL))isNat#(activate(N))
take#(s(M), cons(N, IL))isNat#(N)activate#(n__take(X1, X2))activate#(X2)
length#(cons(N, L))uLength#(and(isNat(N), isNatList(activate(L))), activate(L))zeros#cons#(0, n__zeros)
length#(cons(N, L))and#(isNat(N), isNatList(activate(L)))isNatIList#(n__cons(N, IL))isNatIList#(activate(IL))
take#(0, IL)uTake1#(isNatIList(IL))isNatList#(n__cons(N, L))and#(isNat(activate(N)), isNatList(activate(L)))
isNatIList#(n__cons(N, IL))activate#(IL)activate#(n__nil)nil#
isNatList#(n__cons(N, L))isNat#(activate(N))activate#(n__take(X1, X2))activate#(X1)
isNatList#(n__take(N, IL))and#(isNat(activate(N)), isNatIList(activate(IL)))activate#(n__s(X))s#(activate(X))
take#(0, IL)isNatIList#(IL)take#(s(M), cons(N, IL))isNat#(M)
length#(cons(N, L))activate#(L)

Rewrite Rules

and(tt, T)TisNatIList(IL)isNatList(activate(IL))
isNat(n__0)ttisNat(n__s(N))isNat(activate(N))
isNat(n__length(L))isNatList(activate(L))isNatIList(n__zeros)tt
isNatIList(n__cons(N, IL))and(isNat(activate(N)), isNatIList(activate(IL)))isNatList(n__nil)tt
isNatList(n__cons(N, L))and(isNat(activate(N)), isNatList(activate(L)))isNatList(n__take(N, IL))and(isNat(activate(N)), isNatIList(activate(IL)))
zeroscons(0, n__zeros)take(0, IL)uTake1(isNatIList(IL))
uTake1(tt)niltake(s(M), cons(N, IL))uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL)cons(activate(N), n__take(activate(M), activate(IL)))length(cons(N, L))uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L)s(length(activate(L)))0n__0
s(X)n__s(X)length(X)n__length(X)
zerosn__zeroscons(X1, X2)n__cons(X1, X2)
niln__niltake(X1, X2)n__take(X1, X2)
activate(n__0)0activate(n__s(X))s(activate(X))
activate(n__length(X))length(activate(X))activate(n__zeros)zeros
activate(n__cons(X1, X2))cons(activate(X1), X2)activate(n__nil)nil
activate(n__take(X1, X2))take(activate(X1), activate(X2))activate(X)X

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, n__length, n__take, and, uTake1, activate, isNat, n__s, n__cons, uTake2, 0, n__0, isNatList, s, tt, zeros, take, length, n__nil, n__zeros, cons, nil

Strategy


The following SCCs where found

take#(s(M), cons(N, IL)) → isNatIList#(activate(IL))isNatList#(n__take(N, IL)) → isNat#(activate(N))
length#(cons(N, L)) → isNat#(N)activate#(n__length(X)) → activate#(X)
isNatList#(n__take(N, IL)) → activate#(IL)activate#(n__s(X)) → activate#(X)
uLength#(tt, L) → length#(activate(L))isNatList#(n__take(N, IL)) → isNatIList#(activate(IL))
activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2))uTake2#(tt, M, N, IL) → activate#(IL)
isNat#(n__length(L)) → isNatList#(activate(L))isNatList#(n__cons(N, L)) → isNatList#(activate(L))
uTake2#(tt, M, N, IL) → activate#(M)activate#(n__cons(X1, X2)) → activate#(X1)
isNatIList#(IL) → activate#(IL)isNatIList#(n__cons(N, IL)) → isNat#(activate(N))
isNat#(n__s(N)) → isNat#(activate(N))take#(s(M), cons(N, IL)) → isNat#(N)
isNatList#(n__cons(N, L)) → activate#(L)isNat#(n__length(L)) → activate#(L)
activate#(n__take(X1, X2)) → activate#(X2)length#(cons(N, L)) → uLength#(and(isNat(N), isNatList(activate(L))), activate(L))
isNatList#(n__take(N, IL)) → activate#(N)isNatIList#(n__cons(N, IL)) → isNatIList#(activate(IL))
isNatList#(n__cons(N, L)) → activate#(N)isNatIList#(IL) → isNatList#(activate(IL))
isNat#(n__s(N)) → activate#(N)uLength#(tt, L) → activate#(L)
take#(s(M), cons(N, IL)) → uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))activate#(n__length(X)) → length#(activate(X))
isNatIList#(n__cons(N, IL)) → activate#(IL)length#(cons(N, L)) → isNatList#(activate(L))
uTake2#(tt, M, N, IL) → activate#(N)isNatList#(n__cons(N, L)) → isNat#(activate(N))
activate#(n__take(X1, X2)) → activate#(X1)isNatIList#(n__cons(N, IL)) → activate#(N)
take#(s(M), cons(N, IL)) → activate#(IL)take#(0, IL) → isNatIList#(IL)
take#(s(M), cons(N, IL)) → isNat#(M)length#(cons(N, L)) → activate#(L)