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 (673ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (16ms), ReductionPairSAT (999ms), DependencyGraph (3ms), SizeChangePrinciple (timeout)].
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (150ms), PolynomialLinearRange4iUR (22ms), DependencyGraph (111ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (108ms), ReductionPairSAT (2567ms), DependencyGraph (106ms)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

U41#(tt, V2)isNatIList#(activate(V2))isNatIList#(n__cons(V1, V2))U41#(isNat(activate(V1)), activate(V2))

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, L, N)U62(isNat(activate(N)), activate(L))U62(tt, L)s(length(activate(L)))
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))
length(nil)0length(cons(N, L))U61(isNatList(activate(L)), activate(L), N)
zerosn__zeros0n__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__0)0
activate(n__length(X))length(X)activate(n__s(X))s(X)
activate(n__cons(X1, X2))cons(X1, X2)activate(n__nil)nil
activate(X)X

Original Signature

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




Open Dependency Pair Problem 3

Dependency Pairs

U61#(tt, L, N)activate#(N)U51#(tt, V2)isNatList#(activate(V2))
isNatList#(n__cons(V1, V2))activate#(V2)isNatList#(n__cons(V1, V2))isNat#(activate(V1))
U61#(tt, L, N)activate#(L)U62#(tt, L)length#(activate(L))
length#(cons(N, L))isNatList#(activate(L))activate#(n__length(X))length#(X)
isNat#(n__length(V1))isNatList#(activate(V1))U61#(tt, L, N)isNat#(activate(N))
isNat#(n__s(V1))isNat#(activate(V1))isNatList#(n__cons(V1, V2))U51#(isNat(activate(V1)), activate(V2))
U61#(tt, L, N)U62#(isNat(activate(N)), activate(L))isNatList#(n__cons(V1, V2))activate#(V1)
length#(cons(N, L))U61#(isNatList(activate(L)), activate(L), N)U51#(tt, V2)activate#(V2)
isNat#(n__length(V1))activate#(V1)isNat#(n__s(V1))activate#(V1)
U62#(tt, L)activate#(L)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, L, N)U62(isNat(activate(N)), activate(L))U62(tt, L)s(length(activate(L)))
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))
length(nil)0length(cons(N, L))U61(isNatList(activate(L)), activate(L), N)
zerosn__zeros0n__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__0)0
activate(n__length(X))length(X)activate(n__s(X))s(X)
activate(n__cons(X1, X2))cons(X1, X2)activate(n__nil)nil
activate(X)X

Original Signature

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


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

U61#(tt, L, N)activate#(N)isNatIList#(n__cons(V1, V2))activate#(V2)
activate#(n__zeros)zeros#U51#(tt, V2)isNatList#(activate(V2))
zeros#0#isNatList#(n__cons(V1, V2))isNat#(activate(V1))
U62#(tt, L)length#(activate(L))isNat#(n__length(V1))U11#(isNatList(activate(V1)))
U41#(tt, V2)U42#(isNatIList(activate(V2)))U41#(tt, V2)activate#(V2)
isNatIList#(n__cons(V1, V2))U41#(isNat(activate(V1)), activate(V2))U51#(tt, V2)U52#(isNatList(activate(V2)))
length#(cons(N, L))U61#(isNatList(activate(L)), activate(L), N)isNatIList#(V)activate#(V)
activate#(n__cons(X1, X2))cons#(X1, X2)U51#(tt, V2)activate#(V2)
isNat#(n__length(V1))activate#(V1)isNat#(n__s(V1))activate#(V1)
length#(nil)0#isNatIList#(V)isNatList#(activate(V))
zeros#cons#(0, n__zeros)isNatList#(n__cons(V1, V2))activate#(V2)
isNatIList#(V)U31#(isNatList(activate(V)))U62#(tt, L)s#(length(activate(L)))
U61#(tt, L, N)activate#(L)activate#(n__s(X))s#(X)
length#(cons(N, L))isNatList#(activate(L))activate#(n__length(X))length#(X)
activate#(n__nil)nil#isNat#(n__length(V1))isNatList#(activate(V1))
U41#(tt, V2)isNatIList#(activate(V2))isNat#(n__s(V1))U21#(isNat(activate(V1)))
U61#(tt, L, N)isNat#(activate(N))isNat#(n__s(V1))isNat#(activate(V1))
isNatList#(n__cons(V1, V2))U51#(isNat(activate(V1)), activate(V2))U61#(tt, L, N)U62#(isNat(activate(N)), activate(L))
isNatList#(n__cons(V1, V2))activate#(V1)activate#(n__0)0#
isNatIList#(n__cons(V1, V2))isNat#(activate(V1))isNatIList#(n__cons(V1, V2))activate#(V1)
U62#(tt, L)activate#(L)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, L, N)U62(isNat(activate(N)), activate(L))U62(tt, L)s(length(activate(L)))
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))
length(nil)0length(cons(N, L))U61(isNatList(activate(L)), activate(L), N)
zerosn__zeros0n__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__0)0
activate(n__length(X))length(X)activate(n__s(X))s(X)
activate(n__cons(X1, X2))cons(X1, X2)activate(n__nil)nil
activate(X)X

Original Signature

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

Strategy


The following SCCs where found

U61#(tt, L, N) → activate#(N)isNatList#(n__cons(V1, V2)) → activate#(V2)
U51#(tt, V2) → isNatList#(activate(V2))isNatList#(n__cons(V1, V2)) → isNat#(activate(V1))
U61#(tt, L, N) → activate#(L)U62#(tt, L) → length#(activate(L))
activate#(n__length(X)) → length#(X)length#(cons(N, L)) → isNatList#(activate(L))
isNat#(n__length(V1)) → isNatList#(activate(V1))U61#(tt, L, N) → isNat#(activate(N))
isNat#(n__s(V1)) → isNat#(activate(V1))isNatList#(n__cons(V1, V2)) → U51#(isNat(activate(V1)), activate(V2))
U61#(tt, L, N) → U62#(isNat(activate(N)), activate(L))isNatList#(n__cons(V1, V2)) → activate#(V1)
length#(cons(N, L)) → U61#(isNatList(activate(L)), activate(L), N)U51#(tt, V2) → activate#(V2)
isNat#(n__s(V1)) → activate#(V1)isNat#(n__length(V1)) → activate#(V1)
U62#(tt, L) → activate#(L)length#(cons(N, L)) → activate#(L)

U41#(tt, V2) → isNatIList#(activate(V2))isNatIList#(n__cons(V1, V2)) → U41#(isNat(activate(V1)), activate(V2))