TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (140ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (47ms), PolynomialLinearRange4iUR (2090ms), DependencyGraph (48ms), PolynomialLinearRange8NegiUR (12397ms), DependencyGraph (41ms), ReductionPairSAT (9212ms), DependencyGraph (37ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| activate#(n__nats(X)) | → | activate#(X) | | activate#(n__s(X)) | → | activate#(X) |
| activate#(n__filter(X1, X2, X3)) | → | filter#(activate(X1), activate(X2), activate(X3)) | | filter#(cons(X, Y), 0, M) | → | activate#(Y) |
| activate#(n__filter(X1, X2, X3)) | → | activate#(X3) | | activate#(n__filter(X1, X2, X3)) | → | activate#(X2) |
| filter#(cons(X, Y), s(N), M) | → | activate#(Y) | | sieve#(cons(s(N), Y)) | → | activate#(Y) |
| activate#(n__sieve(X)) | → | activate#(X) | | sieve#(cons(0, Y)) | → | activate#(Y) |
| activate#(n__sieve(X)) | → | sieve#(activate(X)) | | activate#(n__filter(X1, X2, X3)) | → | activate#(X1) |
Rewrite Rules
| filter(cons(X, Y), 0, M) | → | cons(0, n__filter(activate(Y), M, M)) | | filter(cons(X, Y), s(N), M) | → | cons(X, n__filter(activate(Y), N, M)) |
| sieve(cons(0, Y)) | → | cons(0, n__sieve(activate(Y))) | | sieve(cons(s(N), Y)) | → | cons(s(N), n__sieve(n__filter(activate(Y), N, N))) |
| nats(N) | → | cons(N, n__nats(n__s(N))) | | zprimes | → | sieve(nats(s(s(0)))) |
| filter(X1, X2, X3) | → | n__filter(X1, X2, X3) | | sieve(X) | → | n__sieve(X) |
| nats(X) | → | n__nats(X) | | s(X) | → | n__s(X) |
| activate(n__filter(X1, X2, X3)) | → | filter(activate(X1), activate(X2), activate(X3)) | | activate(n__sieve(X)) | → | sieve(activate(X)) |
| activate(n__nats(X)) | → | nats(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__nats, n__s, activate, nats, 0, sieve, s, n__filter, zprimes, n__sieve, filter, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| sieve#(cons(s(N), Y)) | → | s#(N) | | activate#(n__nats(X)) | → | activate#(X) |
| activate#(n__s(X)) | → | activate#(X) | | activate#(n__filter(X1, X2, X3)) | → | filter#(activate(X1), activate(X2), activate(X3)) |
| activate#(n__nats(X)) | → | nats#(activate(X)) | | filter#(cons(X, Y), 0, M) | → | activate#(Y) |
| activate#(n__filter(X1, X2, X3)) | → | activate#(X3) | | zprimes# | → | s#(0) |
| zprimes# | → | nats#(s(s(0))) | | zprimes# | → | sieve#(nats(s(s(0)))) |
| zprimes# | → | s#(s(0)) | | activate#(n__filter(X1, X2, X3)) | → | activate#(X2) |
| filter#(cons(X, Y), s(N), M) | → | activate#(Y) | | sieve#(cons(s(N), Y)) | → | activate#(Y) |
| activate#(n__sieve(X)) | → | activate#(X) | | sieve#(cons(0, Y)) | → | activate#(Y) |
| activate#(n__sieve(X)) | → | sieve#(activate(X)) | | activate#(n__filter(X1, X2, X3)) | → | activate#(X1) |
| activate#(n__s(X)) | → | s#(activate(X)) |
Rewrite Rules
| filter(cons(X, Y), 0, M) | → | cons(0, n__filter(activate(Y), M, M)) | | filter(cons(X, Y), s(N), M) | → | cons(X, n__filter(activate(Y), N, M)) |
| sieve(cons(0, Y)) | → | cons(0, n__sieve(activate(Y))) | | sieve(cons(s(N), Y)) | → | cons(s(N), n__sieve(n__filter(activate(Y), N, N))) |
| nats(N) | → | cons(N, n__nats(n__s(N))) | | zprimes | → | sieve(nats(s(s(0)))) |
| filter(X1, X2, X3) | → | n__filter(X1, X2, X3) | | sieve(X) | → | n__sieve(X) |
| nats(X) | → | n__nats(X) | | s(X) | → | n__s(X) |
| activate(n__filter(X1, X2, X3)) | → | filter(activate(X1), activate(X2), activate(X3)) | | activate(n__sieve(X)) | → | sieve(activate(X)) |
| activate(n__nats(X)) | → | nats(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, n__s, n__nats, nats, 0, s, sieve, n__filter, zprimes, filter, n__sieve, cons
Strategy
The following SCCs where found
| activate#(n__filter(X1, X2, X3)) → activate#(X2) | filter#(cons(X, Y), s(N), M) → activate#(Y) |
| sieve#(cons(s(N), Y)) → activate#(Y) | activate#(n__nats(X)) → activate#(X) |
| activate#(n__filter(X1, X2, X3)) → filter#(activate(X1), activate(X2), activate(X3)) | activate#(n__s(X)) → activate#(X) |
| activate#(n__sieve(X)) → activate#(X) | filter#(cons(X, Y), 0, M) → activate#(Y) |
| activate#(n__filter(X1, X2, X3)) → activate#(X3) | sieve#(cons(0, Y)) → activate#(Y) |
| activate#(n__sieve(X)) → sieve#(activate(X)) | activate#(n__filter(X1, X2, X3)) → activate#(X1) |