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 (497ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (426ms), PolynomialLinearRange4iUR (10001ms), PolynomialLinearRange8NegiUR (30005ms), ReductionPairSAT (14374ms), DependencyGraph (359ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| mark#(filter(X1, X2)) | → | mark#(X1) | | a__from#(X) | → | mark#(X) |
| mark#(from(X)) | → | a__from#(mark(X)) | | mark#(divides(X1, X2)) | → | mark#(X1) |
| a__primes# | → | a__sieve#(a__from(s(s(0)))) | | mark#(filter(X1, X2)) | → | mark#(X2) |
| mark#(sieve(X)) | → | a__sieve#(mark(X)) | | mark#(head(X)) | → | mark#(X) |
| a__sieve#(cons(X, Y)) | → | mark#(X) | | a__primes# | → | a__from#(s(s(0))) |
| mark#(head(X)) | → | a__head#(mark(X)) | | a__filter#(s(s(X)), cons(Y, Z)) | → | mark#(Y) |
| mark#(tail(X)) | → | a__tail#(mark(X)) | | mark#(s(X)) | → | mark#(X) |
| a__filter#(s(s(X)), cons(Y, Z)) | → | mark#(X) | | mark#(if(X1, X2, X3)) | → | a__if#(mark(X1), X2, X3) |
| a__head#(cons(X, Y)) | → | mark#(X) | | mark#(from(X)) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | a__if#(true, X, Y) | → | mark#(X) |
| mark#(tail(X)) | → | mark#(X) | | mark#(primes) | → | a__primes# |
| a__if#(false, X, Y) | → | mark#(Y) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| mark#(filter(X1, X2)) | → | a__filter#(mark(X1), mark(X2)) | | mark#(divides(X1, X2)) | → | mark#(X2) |
| a__tail#(cons(X, Y)) | → | mark#(Y) | | mark#(sieve(X)) | → | mark#(X) |
Rewrite Rules
| a__primes | → | a__sieve(a__from(s(s(0)))) | | a__from(X) | → | cons(mark(X), from(s(X))) |
| a__head(cons(X, Y)) | → | mark(X) | | a__tail(cons(X, Y)) | → | mark(Y) |
| a__if(true, X, Y) | → | mark(X) | | a__if(false, X, Y) | → | mark(Y) |
| a__filter(s(s(X)), cons(Y, Z)) | → | a__if(divides(s(s(mark(X))), mark(Y)), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))) | | a__sieve(cons(X, Y)) | → | cons(mark(X), filter(X, sieve(Y))) |
| mark(primes) | → | a__primes | | mark(sieve(X)) | → | a__sieve(mark(X)) |
| mark(from(X)) | → | a__from(mark(X)) | | mark(head(X)) | → | a__head(mark(X)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(if(X1, X2, X3)) | → | a__if(mark(X1), X2, X3) |
| mark(filter(X1, X2)) | → | a__filter(mark(X1), mark(X2)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(true) | → | true | | mark(false) | → | false |
| mark(divides(X1, X2)) | → | divides(mark(X1), mark(X2)) | | a__primes | → | primes |
| a__sieve(X) | → | sieve(X) | | a__from(X) | → | from(X) |
| a__head(X) | → | head(X) | | a__tail(X) | → | tail(X) |
| a__if(X1, X2, X3) | → | if(X1, X2, X3) | | a__filter(X1, X2) | → | filter(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, a__primes, mark, from, tail, a__sieve, a__tail, a__filter, 0, s, a__if, if, false, primes, head, a__head, filter, a__from, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(filter(X1, X2)) | → | mark#(X1) | | a__from#(X) | → | mark#(X) |
| mark#(from(X)) | → | a__from#(mark(X)) | | mark#(divides(X1, X2)) | → | mark#(X1) |
| a__primes# | → | a__sieve#(a__from(s(s(0)))) | | mark#(filter(X1, X2)) | → | mark#(X2) |
| mark#(sieve(X)) | → | a__sieve#(mark(X)) | | mark#(head(X)) | → | mark#(X) |
| a__sieve#(cons(X, Y)) | → | mark#(X) | | a__primes# | → | a__from#(s(s(0))) |
| mark#(head(X)) | → | a__head#(mark(X)) | | a__filter#(s(s(X)), cons(Y, Z)) | → | mark#(Y) |
| mark#(s(X)) | → | mark#(X) | | mark#(tail(X)) | → | a__tail#(mark(X)) |
| a__filter#(s(s(X)), cons(Y, Z)) | → | mark#(X) | | mark#(if(X1, X2, X3)) | → | a__if#(mark(X1), X2, X3) |
| a__head#(cons(X, Y)) | → | mark#(X) | | a__filter#(s(s(X)), cons(Y, Z)) | → | a__if#(divides(s(s(mark(X))), mark(Y)), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))) |
| mark#(from(X)) | → | mark#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__if#(true, X, Y) | → | mark#(X) | | mark#(primes) | → | a__primes# |
| mark#(tail(X)) | → | mark#(X) | | a__if#(false, X, Y) | → | mark#(Y) |
| mark#(filter(X1, X2)) | → | a__filter#(mark(X1), mark(X2)) | | mark#(if(X1, X2, X3)) | → | mark#(X1) |
| a__tail#(cons(X, Y)) | → | mark#(Y) | | mark#(divides(X1, X2)) | → | mark#(X2) |
| mark#(sieve(X)) | → | mark#(X) |
Rewrite Rules
| a__primes | → | a__sieve(a__from(s(s(0)))) | | a__from(X) | → | cons(mark(X), from(s(X))) |
| a__head(cons(X, Y)) | → | mark(X) | | a__tail(cons(X, Y)) | → | mark(Y) |
| a__if(true, X, Y) | → | mark(X) | | a__if(false, X, Y) | → | mark(Y) |
| a__filter(s(s(X)), cons(Y, Z)) | → | a__if(divides(s(s(mark(X))), mark(Y)), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))) | | a__sieve(cons(X, Y)) | → | cons(mark(X), filter(X, sieve(Y))) |
| mark(primes) | → | a__primes | | mark(sieve(X)) | → | a__sieve(mark(X)) |
| mark(from(X)) | → | a__from(mark(X)) | | mark(head(X)) | → | a__head(mark(X)) |
| mark(tail(X)) | → | a__tail(mark(X)) | | mark(if(X1, X2, X3)) | → | a__if(mark(X1), X2, X3) |
| mark(filter(X1, X2)) | → | a__filter(mark(X1), mark(X2)) | | mark(s(X)) | → | s(mark(X)) |
| mark(0) | → | 0 | | mark(cons(X1, X2)) | → | cons(mark(X1), X2) |
| mark(true) | → | true | | mark(false) | → | false |
| mark(divides(X1, X2)) | → | divides(mark(X1), mark(X2)) | | a__primes | → | primes |
| a__sieve(X) | → | sieve(X) | | a__from(X) | → | from(X) |
| a__head(X) | → | head(X) | | a__tail(X) | → | tail(X) |
| a__if(X1, X2, X3) | → | if(X1, X2, X3) | | a__filter(X1, X2) | → | filter(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: sieve, true, divides, a__primes, mark, from, tail, a__sieve, a__tail, a__filter, 0, s, a__if, if, false, primes, a__head, head, a__from, filter, cons
Strategy
The following SCCs where found
| mark#(filter(X1, X2)) → mark#(X1) | a__from#(X) → mark#(X) |
| mark#(from(X)) → a__from#(mark(X)) | mark#(divides(X1, X2)) → mark#(X1) |
| a__primes# → a__sieve#(a__from(s(s(0)))) | mark#(filter(X1, X2)) → mark#(X2) |
| mark#(sieve(X)) → a__sieve#(mark(X)) | mark#(head(X)) → mark#(X) |
| a__sieve#(cons(X, Y)) → mark#(X) | a__primes# → a__from#(s(s(0))) |
| mark#(head(X)) → a__head#(mark(X)) | a__filter#(s(s(X)), cons(Y, Z)) → mark#(Y) |
| mark#(s(X)) → mark#(X) | mark#(tail(X)) → a__tail#(mark(X)) |
| a__filter#(s(s(X)), cons(Y, Z)) → mark#(X) | mark#(if(X1, X2, X3)) → a__if#(mark(X1), X2, X3) |
| a__head#(cons(X, Y)) → mark#(X) | mark#(from(X)) → mark#(X) |
| mark#(cons(X1, X2)) → mark#(X1) | a__if#(true, X, Y) → mark#(X) |
| mark#(primes) → a__primes# | mark#(tail(X)) → mark#(X) |
| a__if#(false, X, Y) → mark#(Y) | mark#(filter(X1, X2)) → a__filter#(mark(X1), mark(X2)) |
| mark#(if(X1, X2, X3)) → mark#(X1) | a__tail#(cons(X, Y)) → mark#(Y) |
| mark#(divides(X1, X2)) → mark#(X2) | mark#(sieve(X)) → mark#(X) |