YES

The TRS could be proven terminating. The proof took 6024 ms.

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (2791ms).
 | – Problem 2 was processed with processor DependencyGraph (20ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4iUR (1489ms).
 |    |    | – Problem 4 was processed with processor DependencyGraph (23ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (717ms).
 |    |    |    |    | – Problem 6 was processed with processor DependencyGraph (5ms).
 |    |    |    |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (525ms).
 |    |    |    |    |    |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (7ms).

Problem 1: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

a__sieve#(cons(s(N), Y))mark#(N)mark#(filter(X1, X2, X3))mark#(X3)
mark#(zprimes)a__zprimes#mark#(cons(X1, X2))mark#(X1)
a__zprimes#a__sieve#(a__nats(s(s(0))))a__filter#(cons(X, Y), s(N), M)mark#(X)
a__nats#(N)mark#(N)mark#(sieve(X))a__sieve#(mark(X))
mark#(nats(X))a__nats#(mark(X))mark#(filter(X1, X2, X3))mark#(X1)
mark#(filter(X1, X2, X3))mark#(X2)mark#(nats(X))mark#(X)
a__zprimes#a__nats#(s(s(0)))mark#(s(X))mark#(X)
mark#(filter(X1, X2, X3))a__filter#(mark(X1), mark(X2), mark(X3))mark#(sieve(X))mark#(X)

Rewrite Rules

a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y))cons(0, sieve(Y))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N)cons(mark(N), nats(s(N)))a__zprimesa__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))mark(sieve(X))a__sieve(mark(X))
mark(nats(X))a__nats(mark(X))mark(zprimes)a__zprimes
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)a__nats(X)nats(X)
a__zprimeszprimes

Original Signature

Termination of terms over the following signature is verified: a__filter, nats, 0, s, sieve, mark, a__zprimes, zprimes, filter, a__nats, cons, a__sieve

Strategy


Polynomial Interpretation

Improved Usable rules

a__nats(N)cons(mark(N), nats(s(N)))mark(cons(X1, X2))cons(mark(X1), X2)
a__nats(X)nats(X)mark(0)0
a__sieve(cons(0, Y))cons(0, sieve(Y))a__zprimeszprimes
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))a__zprimesa__sieve(a__nats(s(s(0))))
a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))mark(s(X))s(mark(X))
mark(sieve(X))a__sieve(mark(X))mark(zprimes)a__zprimes
mark(nats(X))a__nats(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)

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

mark#(zprimes)a__zprimes#

Problem 2: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__sieve#(cons(s(N), Y))mark#(N)mark#(filter(X1, X2, X3))mark#(X3)
mark#(cons(X1, X2))mark#(X1)a__zprimes#a__sieve#(a__nats(s(s(0))))
a__filter#(cons(X, Y), s(N), M)mark#(X)a__nats#(N)mark#(N)
mark#(sieve(X))a__sieve#(mark(X))mark#(nats(X))a__nats#(mark(X))
mark#(filter(X1, X2, X3))mark#(X1)mark#(filter(X1, X2, X3))mark#(X2)
mark#(nats(X))mark#(X)a__zprimes#a__nats#(s(s(0)))
mark#(s(X))mark#(X)mark#(filter(X1, X2, X3))a__filter#(mark(X1), mark(X2), mark(X3))
mark#(sieve(X))mark#(X)

Rewrite Rules

a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y))cons(0, sieve(Y))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N)cons(mark(N), nats(s(N)))a__zprimesa__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))mark(sieve(X))a__sieve(mark(X))
mark(nats(X))a__nats(mark(X))mark(zprimes)a__zprimes
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)a__nats(X)nats(X)
a__zprimeszprimes

Original Signature

Termination of terms over the following signature is verified: a__filter, nats, 0, sieve, s, a__zprimes, mark, zprimes, a__nats, filter, a__sieve, cons

Strategy


The following SCCs where found

a__sieve#(cons(s(N), Y)) → mark#(N)mark#(filter(X1, X2, X3)) → mark#(X3)
mark#(cons(X1, X2)) → mark#(X1)a__filter#(cons(X, Y), s(N), M) → mark#(X)
a__nats#(N) → mark#(N)mark#(sieve(X)) → a__sieve#(mark(X))
mark#(nats(X)) → a__nats#(mark(X))mark#(filter(X1, X2, X3)) → mark#(X1)
mark#(filter(X1, X2, X3)) → mark#(X2)mark#(nats(X)) → mark#(X)
mark#(s(X)) → mark#(X)mark#(filter(X1, X2, X3)) → a__filter#(mark(X1), mark(X2), mark(X3))
mark#(sieve(X)) → mark#(X)

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(filter(X1, X2, X3))mark#(X3)a__sieve#(cons(s(N), Y))mark#(N)
mark#(cons(X1, X2))mark#(X1)a__filter#(cons(X, Y), s(N), M)mark#(X)
a__nats#(N)mark#(N)mark#(sieve(X))a__sieve#(mark(X))
mark#(nats(X))a__nats#(mark(X))mark#(nats(X))mark#(X)
mark#(filter(X1, X2, X3))mark#(X2)mark#(filter(X1, X2, X3))mark#(X1)
mark#(s(X))mark#(X)mark#(filter(X1, X2, X3))a__filter#(mark(X1), mark(X2), mark(X3))
mark#(sieve(X))mark#(X)

Rewrite Rules

a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y))cons(0, sieve(Y))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N)cons(mark(N), nats(s(N)))a__zprimesa__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))mark(sieve(X))a__sieve(mark(X))
mark(nats(X))a__nats(mark(X))mark(zprimes)a__zprimes
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)a__nats(X)nats(X)
a__zprimeszprimes

Original Signature

Termination of terms over the following signature is verified: a__filter, nats, 0, sieve, s, a__zprimes, mark, zprimes, a__nats, filter, a__sieve, cons

Strategy


Polynomial Interpretation

Improved Usable rules

mark(cons(X1, X2))cons(mark(X1), X2)a__nats(N)cons(mark(N), nats(s(N)))
mark(0)0a__nats(X)nats(X)
a__sieve(cons(0, Y))cons(0, sieve(Y))a__zprimeszprimes
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))a__zprimesa__sieve(a__nats(s(s(0))))
a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))mark(s(X))s(mark(X))
mark(sieve(X))a__sieve(mark(X))mark(zprimes)a__zprimes
mark(nats(X))a__nats(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)

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

mark#(nats(X))a__nats#(mark(X))mark#(nats(X))mark#(X)

Problem 4: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__sieve#(cons(s(N), Y))mark#(N)mark#(filter(X1, X2, X3))mark#(X3)
mark#(sieve(X))a__sieve#(mark(X))mark#(filter(X1, X2, X3))mark#(X1)
mark#(filter(X1, X2, X3))mark#(X2)mark#(cons(X1, X2))mark#(X1)
mark#(s(X))mark#(X)mark#(filter(X1, X2, X3))a__filter#(mark(X1), mark(X2), mark(X3))
mark#(sieve(X))mark#(X)a__filter#(cons(X, Y), s(N), M)mark#(X)
a__nats#(N)mark#(N)

Rewrite Rules

a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y))cons(0, sieve(Y))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N)cons(mark(N), nats(s(N)))a__zprimesa__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))mark(sieve(X))a__sieve(mark(X))
mark(nats(X))a__nats(mark(X))mark(zprimes)a__zprimes
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)a__nats(X)nats(X)
a__zprimeszprimes

Original Signature

Termination of terms over the following signature is verified: a__filter, nats, 0, s, sieve, mark, a__zprimes, zprimes, filter, a__nats, cons, a__sieve

Strategy


The following SCCs where found

a__sieve#(cons(s(N), Y)) → mark#(N)mark#(filter(X1, X2, X3)) → mark#(X3)
mark#(sieve(X)) → a__sieve#(mark(X))mark#(cons(X1, X2)) → mark#(X1)
mark#(filter(X1, X2, X3)) → mark#(X1)mark#(filter(X1, X2, X3)) → mark#(X2)
mark#(s(X)) → mark#(X)mark#(filter(X1, X2, X3)) → a__filter#(mark(X1), mark(X2), mark(X3))
a__filter#(cons(X, Y), s(N), M) → mark#(X)mark#(sieve(X)) → mark#(X)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

a__sieve#(cons(s(N), Y))mark#(N)mark#(filter(X1, X2, X3))mark#(X3)
mark#(sieve(X))a__sieve#(mark(X))mark#(cons(X1, X2))mark#(X1)
mark#(filter(X1, X2, X3))mark#(X1)mark#(filter(X1, X2, X3))mark#(X2)
mark#(s(X))mark#(X)mark#(filter(X1, X2, X3))a__filter#(mark(X1), mark(X2), mark(X3))
a__filter#(cons(X, Y), s(N), M)mark#(X)mark#(sieve(X))mark#(X)

Rewrite Rules

a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y))cons(0, sieve(Y))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N)cons(mark(N), nats(s(N)))a__zprimesa__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))mark(sieve(X))a__sieve(mark(X))
mark(nats(X))a__nats(mark(X))mark(zprimes)a__zprimes
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)a__nats(X)nats(X)
a__zprimeszprimes

Original Signature

Termination of terms over the following signature is verified: a__filter, nats, 0, s, sieve, mark, a__zprimes, zprimes, filter, a__nats, cons, a__sieve

Strategy


Polynomial Interpretation

Improved Usable rules

mark(cons(X1, X2))cons(mark(X1), X2)a__nats(N)cons(mark(N), nats(s(N)))
mark(0)0a__nats(X)nats(X)
a__sieve(cons(0, Y))cons(0, sieve(Y))a__zprimeszprimes
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))a__zprimesa__sieve(a__nats(s(s(0))))
a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))mark(s(X))s(mark(X))
mark(sieve(X))a__sieve(mark(X))mark(zprimes)a__zprimes
mark(nats(X))a__nats(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)

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

a__sieve#(cons(s(N), Y))mark#(N)mark#(sieve(X))mark#(X)

Problem 6: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(filter(X1, X2, X3))mark#(X3)mark#(sieve(X))a__sieve#(mark(X))
mark#(filter(X1, X2, X3))mark#(X2)mark#(filter(X1, X2, X3))mark#(X1)
mark#(cons(X1, X2))mark#(X1)mark#(s(X))mark#(X)
mark#(filter(X1, X2, X3))a__filter#(mark(X1), mark(X2), mark(X3))a__filter#(cons(X, Y), s(N), M)mark#(X)

Rewrite Rules

a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y))cons(0, sieve(Y))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N)cons(mark(N), nats(s(N)))a__zprimesa__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))mark(sieve(X))a__sieve(mark(X))
mark(nats(X))a__nats(mark(X))mark(zprimes)a__zprimes
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)a__nats(X)nats(X)
a__zprimeszprimes

Original Signature

Termination of terms over the following signature is verified: a__filter, nats, 0, sieve, s, a__zprimes, mark, zprimes, a__nats, filter, a__sieve, cons

Strategy


The following SCCs where found

mark#(filter(X1, X2, X3)) → mark#(X3)mark#(cons(X1, X2)) → mark#(X1)
mark#(filter(X1, X2, X3)) → mark#(X1)mark#(filter(X1, X2, X3)) → mark#(X2)
mark#(s(X)) → mark#(X)mark#(filter(X1, X2, X3)) → a__filter#(mark(X1), mark(X2), mark(X3))
a__filter#(cons(X, Y), s(N), M) → mark#(X)

Problem 7: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(filter(X1, X2, X3))mark#(X3)mark#(cons(X1, X2))mark#(X1)
mark#(filter(X1, X2, X3))mark#(X1)mark#(filter(X1, X2, X3))mark#(X2)
mark#(s(X))mark#(X)mark#(filter(X1, X2, X3))a__filter#(mark(X1), mark(X2), mark(X3))
a__filter#(cons(X, Y), s(N), M)mark#(X)

Rewrite Rules

a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y))cons(0, sieve(Y))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N)cons(mark(N), nats(s(N)))a__zprimesa__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))mark(sieve(X))a__sieve(mark(X))
mark(nats(X))a__nats(mark(X))mark(zprimes)a__zprimes
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)a__nats(X)nats(X)
a__zprimeszprimes

Original Signature

Termination of terms over the following signature is verified: a__filter, nats, 0, sieve, s, a__zprimes, mark, zprimes, a__nats, filter, a__sieve, cons

Strategy


Polynomial Interpretation

Improved Usable rules

mark(cons(X1, X2))cons(mark(X1), X2)a__nats(N)cons(mark(N), nats(s(N)))
mark(0)0a__nats(X)nats(X)
a__sieve(cons(0, Y))cons(0, sieve(Y))a__zprimeszprimes
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))a__zprimesa__sieve(a__nats(s(s(0))))
a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))mark(s(X))s(mark(X))
mark(sieve(X))a__sieve(mark(X))mark(zprimes)a__zprimes
mark(nats(X))a__nats(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)

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

mark#(filter(X1, X2, X3))mark#(X3)mark#(filter(X1, X2, X3))mark#(X2)
mark#(filter(X1, X2, X3))mark#(X1)mark#(cons(X1, X2))mark#(X1)
mark#(filter(X1, X2, X3))a__filter#(mark(X1), mark(X2), mark(X3))a__filter#(cons(X, Y), s(N), M)mark#(X)

Problem 8: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(s(X))mark#(X)

Rewrite Rules

a__filter(cons(X, Y), 0, M)cons(0, filter(Y, M, M))a__filter(cons(X, Y), s(N), M)cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y))cons(0, sieve(Y))a__sieve(cons(s(N), Y))cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N)cons(mark(N), nats(s(N)))a__zprimesa__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3))a__filter(mark(X1), mark(X2), mark(X3))mark(sieve(X))a__sieve(mark(X))
mark(nats(X))a__nats(mark(X))mark(zprimes)a__zprimes
mark(cons(X1, X2))cons(mark(X1), X2)mark(0)0
mark(s(X))s(mark(X))a__filter(X1, X2, X3)filter(X1, X2, X3)
a__sieve(X)sieve(X)a__nats(X)nats(X)
a__zprimeszprimes

Original Signature

Termination of terms over the following signature is verified: a__filter, nats, 0, s, sieve, mark, a__zprimes, zprimes, filter, a__nats, cons, a__sieve

Strategy


Polynomial Interpretation

There are no usable rules

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

mark#(s(X))mark#(X)