TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (343ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (4141ms).
 |    | – Problem 3 was processed with processor DependencyGraph (68ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (1917ms).
 |    |    |    | – Problem 5 was processed with processor DependencyGraph (19ms).
 |    |    |    |    | – Problem 6 remains open; application of the following processors failed [PolynomialLinearRange4iUR (647ms), DependencyGraph (10ms), PolynomialLinearRange8NegiUR (10250ms), DependencyGraph (12ms), ReductionPairSAT (1914ms), DependencyGraph (10ms), SizeChangePrinciple (timeout)].

The following open problems remain:



Open Dependency Pair Problem 6

Dependency Pairs

activate#(n__oddNs)oddNs#activate#(n__cons(X1, X2))activate#(X1)
activate#(n__incr(X))incr#(activate(X))oddNs#incr#(pairNs)
incr#(cons(X, XS))activate#(XS)activate#(n__incr(X))activate#(X)

Rewrite Rules

pairNscons(0, n__incr(n__oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
oddNsn__oddNstake(X1, X2)n__take(X1, X2)
zip(X1, X2)n__zip(X1, X2)cons(X1, X2)n__cons(X1, X2)
repItems(X)n__repItems(X)activate(n__incr(X))incr(activate(X))
activate(n__oddNs)oddNsactivate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__zip(X1, X2))zip(activate(X1), activate(X2))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__repItems(X))repItems(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, n__oddNs, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

zip#(cons(X, XS), cons(Y, YS))cons#(pair(X, Y), n__zip(activate(XS), activate(YS)))activate#(n__incr(X))activate#(X)
activate#(n__take(X1, X2))take#(activate(X1), activate(X2))tail#(cons(X, XS))activate#(XS)
activate#(n__cons(X1, X2))cons#(activate(X1), X2)zip#(cons(X, XS), cons(Y, YS))activate#(XS)
activate#(n__cons(X1, X2))activate#(X1)activate#(n__incr(X))incr#(activate(X))
repItems#(cons(X, XS))activate#(XS)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
pairNs#cons#(0, n__incr(n__oddNs))activate#(n__take(X1, X2))activate#(X2)
activate#(n__oddNs)oddNs#incr#(cons(X, XS))cons#(s(X), n__incr(activate(XS)))
oddNs#incr#(pairNs)incr#(cons(X, XS))activate#(XS)
activate#(n__zip(X1, X2))activate#(X2)take#(s(N), cons(X, XS))activate#(XS)
activate#(n__repItems(X))repItems#(activate(X))activate#(n__repItems(X))activate#(X)
activate#(n__take(X1, X2))activate#(X1)activate#(n__zip(X1, X2))zip#(activate(X1), activate(X2))
oddNs#pairNs#activate#(n__zip(X1, X2))activate#(X1)
take#(s(N), cons(X, XS))cons#(X, n__take(N, activate(XS)))repItems#(cons(X, XS))cons#(X, n__cons(X, n__repItems(activate(XS))))

Rewrite Rules

pairNscons(0, n__incr(n__oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
oddNsn__oddNstake(X1, X2)n__take(X1, X2)
zip(X1, X2)n__zip(X1, X2)cons(X1, X2)n__cons(X1, X2)
repItems(X)n__repItems(X)activate(n__incr(X))incr(activate(X))
activate(n__oddNs)oddNsactivate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__zip(X1, X2))zip(activate(X1), activate(X2))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__repItems(X))repItems(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, n__oddNs, pairNs, s, take, repItems, n__zip, incr, oddNs, nil, cons

Strategy


The following SCCs where found

activate#(n__oddNs) → oddNs#oddNs# → incr#(pairNs)
incr#(cons(X, XS)) → activate#(XS)activate#(n__incr(X)) → activate#(X)
activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2))activate#(n__zip(X1, X2)) → activate#(X2)
activate#(n__repItems(X)) → repItems#(activate(X))take#(s(N), cons(X, XS)) → activate#(XS)
activate#(n__repItems(X)) → activate#(X)zip#(cons(X, XS), cons(Y, YS)) → activate#(XS)
activate#(n__cons(X1, X2)) → activate#(X1)activate#(n__incr(X)) → incr#(activate(X))
activate#(n__zip(X1, X2)) → zip#(activate(X1), activate(X2))repItems#(cons(X, XS)) → activate#(XS)
activate#(n__take(X1, X2)) → activate#(X1)zip#(cons(X, XS), cons(Y, YS)) → activate#(YS)
activate#(n__zip(X1, X2)) → activate#(X1)activate#(n__take(X1, X2)) → activate#(X2)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__oddNs)oddNs#oddNs#incr#(pairNs)
incr#(cons(X, XS))activate#(XS)activate#(n__incr(X))activate#(X)
activate#(n__take(X1, X2))take#(activate(X1), activate(X2))activate#(n__zip(X1, X2))activate#(X2)
take#(s(N), cons(X, XS))activate#(XS)activate#(n__repItems(X))repItems#(activate(X))
activate#(n__repItems(X))activate#(X)zip#(cons(X, XS), cons(Y, YS))activate#(XS)
activate#(n__cons(X1, X2))activate#(X1)activate#(n__incr(X))incr#(activate(X))
activate#(n__zip(X1, X2))zip#(activate(X1), activate(X2))repItems#(cons(X, XS))activate#(XS)
activate#(n__take(X1, X2))activate#(X1)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
activate#(n__zip(X1, X2))activate#(X1)activate#(n__take(X1, X2))activate#(X2)

Rewrite Rules

pairNscons(0, n__incr(n__oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
oddNsn__oddNstake(X1, X2)n__take(X1, X2)
zip(X1, X2)n__zip(X1, X2)cons(X1, X2)n__cons(X1, X2)
repItems(X)n__repItems(X)activate(n__incr(X))incr(activate(X))
activate(n__oddNs)oddNsactivate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__zip(X1, X2))zip(activate(X1), activate(X2))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__repItems(X))repItems(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, n__oddNs, pairNs, s, take, repItems, n__zip, incr, oddNs, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

repItems(X)n__repItems(X)zip(nil, XS)nil
take(0, XS)niltake(X1, X2)n__take(X1, X2)
oddNsn__oddNszip(X, nil)nil
activate(n__oddNs)oddNsoddNsincr(pairNs)
activate(n__repItems(X))repItems(activate(X))cons(X1, X2)n__cons(X1, X2)
activate(n__take(X1, X2))take(activate(X1), activate(X2))activate(n__incr(X))incr(activate(X))
pairNscons(0, n__incr(n__oddNs))activate(X)X
activate(n__zip(X1, X2))zip(activate(X1), activate(X2))incr(X)n__incr(X)
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
activate(n__cons(X1, X2))cons(activate(X1), X2)zip(X1, X2)n__zip(X1, X2)
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))
repItems(nil)nil

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

activate#(n__zip(X1, X2))activate#(X2)activate#(n__zip(X1, X2))zip#(activate(X1), activate(X2))
activate#(n__zip(X1, X2))activate#(X1)

Problem 3: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__oddNs)oddNs#oddNs#incr#(pairNs)
incr#(cons(X, XS))activate#(XS)activate#(n__incr(X))activate#(X)
activate#(n__take(X1, X2))take#(activate(X1), activate(X2))take#(s(N), cons(X, XS))activate#(XS)
activate#(n__repItems(X))repItems#(activate(X))activate#(n__repItems(X))activate#(X)
zip#(cons(X, XS), cons(Y, YS))activate#(XS)activate#(n__cons(X1, X2))activate#(X1)
activate#(n__incr(X))incr#(activate(X))repItems#(cons(X, XS))activate#(XS)
activate#(n__take(X1, X2))activate#(X1)zip#(cons(X, XS), cons(Y, YS))activate#(YS)
activate#(n__take(X1, X2))activate#(X2)

Rewrite Rules

pairNscons(0, n__incr(n__oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
oddNsn__oddNstake(X1, X2)n__take(X1, X2)
zip(X1, X2)n__zip(X1, X2)cons(X1, X2)n__cons(X1, X2)
repItems(X)n__repItems(X)activate(n__incr(X))incr(activate(X))
activate(n__oddNs)oddNsactivate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__zip(X1, X2))zip(activate(X1), activate(X2))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__repItems(X))repItems(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, n__oddNs, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil

Strategy


The following SCCs where found

activate#(n__oddNs) → oddNs#oddNs# → incr#(pairNs)
incr#(cons(X, XS)) → activate#(XS)activate#(n__incr(X)) → activate#(X)
activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2))take#(s(N), cons(X, XS)) → activate#(XS)
activate#(n__repItems(X)) → repItems#(activate(X))activate#(n__repItems(X)) → activate#(X)
activate#(n__cons(X1, X2)) → activate#(X1)activate#(n__incr(X)) → incr#(activate(X))
repItems#(cons(X, XS)) → activate#(XS)activate#(n__take(X1, X2)) → activate#(X1)
activate#(n__take(X1, X2)) → activate#(X2)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

activate#(n__oddNs)oddNs#oddNs#incr#(pairNs)
incr#(cons(X, XS))activate#(XS)activate#(n__incr(X))activate#(X)
activate#(n__take(X1, X2))take#(activate(X1), activate(X2))activate#(n__repItems(X))repItems#(activate(X))
take#(s(N), cons(X, XS))activate#(XS)activate#(n__repItems(X))activate#(X)
activate#(n__cons(X1, X2))activate#(X1)activate#(n__incr(X))incr#(activate(X))
activate#(n__take(X1, X2))activate#(X1)repItems#(cons(X, XS))activate#(XS)
activate#(n__take(X1, X2))activate#(X2)

Rewrite Rules

pairNscons(0, n__incr(n__oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
oddNsn__oddNstake(X1, X2)n__take(X1, X2)
zip(X1, X2)n__zip(X1, X2)cons(X1, X2)n__cons(X1, X2)
repItems(X)n__repItems(X)activate(n__incr(X))incr(activate(X))
activate(n__oddNs)oddNsactivate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__zip(X1, X2))zip(activate(X1), activate(X2))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__repItems(X))repItems(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, n__oddNs, pairNs, s, repItems, take, n__zip, incr, oddNs, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

repItems(X)n__repItems(X)zip(nil, XS)nil
take(0, XS)niltake(X1, X2)n__take(X1, X2)
oddNsn__oddNszip(X, nil)nil
activate(n__oddNs)oddNsoddNsincr(pairNs)
activate(n__repItems(X))repItems(activate(X))cons(X1, X2)n__cons(X1, X2)
activate(n__take(X1, X2))take(activate(X1), activate(X2))activate(n__incr(X))incr(activate(X))
pairNscons(0, n__incr(n__oddNs))activate(X)X
activate(n__zip(X1, X2))zip(activate(X1), activate(X2))incr(X)n__incr(X)
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
activate(n__cons(X1, X2))cons(activate(X1), X2)zip(X1, X2)n__zip(X1, X2)
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))
repItems(nil)nil

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

activate#(n__take(X1, X2))take#(activate(X1), activate(X2))activate#(n__repItems(X))activate#(X)
activate#(n__take(X1, X2))activate#(X1)repItems#(cons(X, XS))activate#(XS)
activate#(n__take(X1, X2))activate#(X2)

Problem 5: DependencyGraph



Dependency Pair Problem

Dependency Pairs

take#(s(N), cons(X, XS))activate#(XS)activate#(n__repItems(X))repItems#(activate(X))
activate#(n__oddNs)oddNs#activate#(n__cons(X1, X2))activate#(X1)
activate#(n__incr(X))incr#(activate(X))oddNs#incr#(pairNs)
incr#(cons(X, XS))activate#(XS)activate#(n__incr(X))activate#(X)

Rewrite Rules

pairNscons(0, n__incr(n__oddNs))oddNsincr(pairNs)
incr(cons(X, XS))cons(s(X), n__incr(activate(XS)))take(0, XS)nil
take(s(N), cons(X, XS))cons(X, n__take(N, activate(XS)))zip(nil, XS)nil
zip(X, nil)nilzip(cons(X, XS), cons(Y, YS))cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS))activate(XS)repItems(nil)nil
repItems(cons(X, XS))cons(X, n__cons(X, n__repItems(activate(XS))))incr(X)n__incr(X)
oddNsn__oddNstake(X1, X2)n__take(X1, X2)
zip(X1, X2)n__zip(X1, X2)cons(X1, X2)n__cons(X1, X2)
repItems(X)n__repItems(X)activate(n__incr(X))incr(activate(X))
activate(n__oddNs)oddNsactivate(n__take(X1, X2))take(activate(X1), activate(X2))
activate(n__zip(X1, X2))zip(activate(X1), activate(X2))activate(n__cons(X1, X2))cons(activate(X1), X2)
activate(n__repItems(X))repItems(activate(X))activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, zip, pair, n__repItems, n__take, tail, activate, n__cons, 0, n__oddNs, pairNs, s, take, repItems, n__zip, incr, oddNs, nil, cons

Strategy


The following SCCs where found

activate#(n__oddNs) → oddNs#activate#(n__cons(X1, X2)) → activate#(X1)
activate#(n__incr(X)) → incr#(activate(X))oddNs# → incr#(pairNs)
incr#(cons(X, XS)) → activate#(XS)activate#(n__incr(X)) → activate#(X)