TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (474ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (375ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (287ms), PolynomialLinearRange8NegiUR (30036ms), DependencyGraph (timeout), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

mark#(U11(X1, X2)) → mark#(X1)mark#(take(X1, X2)) → mark#(X1)
a__U12#(tt, L) → a__length#(mark(L))mark#(U23(X1, X2, X3, X4)) → a__U23#(mark(X1), X2, X3, X4)
mark#(length(X)) → a__length#(mark(X))mark#(U21(X1, X2, X3, X4)) → a__U21#(mark(X1), X2, X3, X4)
a__take#(s(M), cons(N, IL)) → a__U21#(tt, IL, M, N)mark#(length(X)) → mark#(X)
mark#(s(X)) → mark#(X)mark#(U12(X1, X2)) → mark#(X1)
mark#(U21(X1, X2, X3, X4)) → mark#(X1)a__U21#(tt, IL, M, N) → a__U22#(tt, IL, M, N)
mark#(U22(X1, X2, X3, X4)) → mark#(X1)mark#(cons(X1, X2)) → mark#(X1)
mark#(U22(X1, X2, X3, X4)) → a__U22#(mark(X1), X2, X3, X4)a__U12#(tt, L) → mark#(L)
mark#(U23(X1, X2, X3, X4)) → mark#(X1)a__U22#(tt, IL, M, N) → a__U23#(tt, IL, M, N)
mark#(take(X1, X2)) → a__take#(mark(X1), mark(X2))mark#(U12(X1, X2)) → a__U12#(mark(X1), X2)
mark#(take(X1, X2)) → mark#(X2)mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)
a__U11#(tt, L) → a__U12#(tt, L)a__length#(cons(N, L)) → a__U11#(tt, L)
a__U23#(tt, IL, M, N) → mark#(N)

Rewrite Rules

a__zeros → cons(0, zeros)a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(nil) → 0a__length(cons(N, L)) → a__U11(tt, L)
a__take(0, IL) → nila__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zerosmark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)mark(0) → 0
mark(tt) → ttmark(s(X)) → s(mark(X))
mark(nil) → nila__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__zeros, a__take, a__length, mark, 0, s, zeros, tt, take, length, a__U23, U11, a__U22, U12, a__U12, a__U11, U23, U21, a__U21, U22, nil, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark#(U11(X1, X2)) → mark#(X1)mark#(take(X1, X2)) → mark#(X1)
mark#(zeros) → a__zeros#a__U12#(tt, L) → a__length#(mark(L))
mark#(U23(X1, X2, X3, X4)) → a__U23#(mark(X1), X2, X3, X4)mark#(U21(X1, X2, X3, X4)) → a__U21#(mark(X1), X2, X3, X4)
mark#(length(X)) → a__length#(mark(X))a__take#(s(M), cons(N, IL)) → a__U21#(tt, IL, M, N)
mark#(length(X)) → mark#(X)mark#(s(X)) → mark#(X)
mark#(U12(X1, X2)) → mark#(X1)mark#(U21(X1, X2, X3, X4)) → mark#(X1)
a__U21#(tt, IL, M, N) → a__U22#(tt, IL, M, N)mark#(U22(X1, X2, X3, X4)) → mark#(X1)
mark#(cons(X1, X2)) → mark#(X1)mark#(U22(X1, X2, X3, X4)) → a__U22#(mark(X1), X2, X3, X4)
a__U12#(tt, L) → mark#(L)mark#(U23(X1, X2, X3, X4)) → mark#(X1)
mark#(U12(X1, X2)) → a__U12#(mark(X1), X2)a__U22#(tt, IL, M, N) → a__U23#(tt, IL, M, N)
mark#(take(X1, X2)) → a__take#(mark(X1), mark(X2))mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)
mark#(take(X1, X2)) → mark#(X2)a__U11#(tt, L) → a__U12#(tt, L)
a__U23#(tt, IL, M, N) → mark#(N)a__length#(cons(N, L)) → a__U11#(tt, L)

Rewrite Rules

a__zeros → cons(0, zeros)a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(nil) → 0a__length(cons(N, L)) → a__U11(tt, L)
a__take(0, IL) → nila__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zerosmark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)mark(0) → 0
mark(tt) → ttmark(s(X)) → s(mark(X))
mark(nil) → nila__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)

Original Signature

Termination of terms over the following signature is verified: a__zeros, a__take, a__length, mark, 0, s, zeros, tt, take, length, a__U23, U11, a__U22, a__U12, U12, a__U11, U23, a__U21, U21, cons, nil, U22

Strategy

The following SCCs where found

mark#(U11(X1, X2)) → mark#(X1)mark#(take(X1, X2)) → mark#(X1)
a__U12#(tt, L) → a__length#(mark(L))mark#(U23(X1, X2, X3, X4)) → a__U23#(mark(X1), X2, X3, X4)
mark#(U21(X1, X2, X3, X4)) → a__U21#(mark(X1), X2, X3, X4)mark#(length(X)) → a__length#(mark(X))
a__take#(s(M), cons(N, IL)) → a__U21#(tt, IL, M, N)mark#(length(X)) → mark#(X)
mark#(s(X)) → mark#(X)mark#(U12(X1, X2)) → mark#(X1)
mark#(U21(X1, X2, X3, X4)) → mark#(X1)a__U21#(tt, IL, M, N) → a__U22#(tt, IL, M, N)
mark#(cons(X1, X2)) → mark#(X1)mark#(U22(X1, X2, X3, X4)) → mark#(X1)
mark#(U22(X1, X2, X3, X4)) → a__U22#(mark(X1), X2, X3, X4)a__U12#(tt, L) → mark#(L)
mark#(U23(X1, X2, X3, X4)) → mark#(X1)mark#(U12(X1, X2)) → a__U12#(mark(X1), X2)
mark#(take(X1, X2)) → a__take#(mark(X1), mark(X2))a__U22#(tt, IL, M, N) → a__U23#(tt, IL, M, N)
mark#(U11(X1, X2)) → a__U11#(mark(X1), X2)mark#(take(X1, X2)) → mark#(X2)
a__U11#(tt, L) → a__U12#(tt, L)a__U23#(tt, IL, M, N) → mark#(N)
a__length#(cons(N, L)) → a__U11#(tt, L)