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 (45ms).
 | – Problem 2 was processed with processor PolynomialLinearRange8NegiUR (2047ms).
 |    | – Problem 4 was processed with processor ForwardNarrowing (3ms).
 |    |    | – Problem 5 was processed with processor ForwardNarrowing (1ms).
 |    |    |    | – Problem 6 was processed with processor ForwardInstantiation (5ms).
 |    |    |    |    | – Problem 8 was processed with processor ForwardInstantiation (7ms).
 |    |    |    |    |    | – Problem 10 was processed with processor Propagation (24ms).
 |    |    |    |    |    |    | – Problem 11 was processed with processor BackwardInstantiation (10ms).
 |    |    |    |    |    |    |    | – Problem 13 was processed with processor ForwardInstantiation (30ms).
 |    |    |    |    |    |    |    |    | – Problem 14 was processed with processor Propagation (245ms).
 |    |    |    |    |    |    |    |    |    | – Problem 15 remains open; application of the following processors failed [].
 | – Problem 3 was processed with processor BackwardInstantiation (1ms).
 |    | – Problem 7 was processed with processor BackwardInstantiation (2ms).
 |    |    | – Problem 9 was processed with processor BackwardInstantiation (1ms).
 |    |    |    | – Problem 12 remains open; application of the following processors failed [ForwardInstantiation (0ms), Propagation (2ms)].

The following open problems remain:

Open Dependency Pair Problem 3

Dependency Pairs

from#(X) → from#(s(X))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Open Dependency Pair Problem 4

Dependency Pairs

sieve#(cons(X, Y)) → filter#(X, sieve(Y))filter#(s(s(X)), cons(Y, Z)) → sieve#(Y)
sieve#(cons(X, Y)) → sieve#(Y)filter#(s(s(X)), cons(Y, Z)) → filter#(X, sieve(Y))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

sieve#(cons(X, Y)) → filter#(X, sieve(Y))filter#(s(s(X)), cons(Y, Z)) → if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
filter#(s(s(X)), cons(Y, Z)) → filter#(s(s(X)), Z)primes# → from#(s(s(0)))
from#(X) → from#(s(X))filter#(s(s(X)), cons(Y, Z)) → sieve#(Y)
primes# → sieve#(from(s(s(0))))sieve#(cons(X, Y)) → sieve#(Y)
filter#(s(s(X)), cons(Y, Z)) → filter#(X, sieve(Y))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

The following SCCs where found

from#(X) → from#(s(X))
sieve#(cons(X, Y)) → filter#(X, sieve(Y))filter#(s(s(X)), cons(Y, Z)) → filter#(s(s(X)), Z)
filter#(s(s(X)), cons(Y, Z)) → sieve#(Y)sieve#(cons(X, Y)) → sieve#(Y)
filter#(s(s(X)), cons(Y, Z)) → filter#(X, sieve(Y))

Problem 2: PolynomialLinearRange8NegiUR

Dependency Pair Problem

Dependency Pairs

sieve#(cons(X, Y)) → filter#(X, sieve(Y))filter#(s(s(X)), cons(Y, Z)) → filter#(s(s(X)), Z)
filter#(s(s(X)), cons(Y, Z)) → sieve#(Y)sieve#(cons(X, Y)) → sieve#(Y)
filter#(s(s(X)), cons(Y, Z)) → filter#(X, sieve(Y))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Polynomial Interpretation

Improved Usable rules

sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
if(false, X, Y) → Yif(true, X, Y) → X

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

filter#(s(s(X)), cons(Y, Z)) → filter#(s(s(X)), Z)

Problem 4: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

sieve#(cons(X, Y)) → filter#(X, sieve(Y))filter#(s(s(X)), cons(Y, Z)) → sieve#(Y)
sieve#(cons(X, Y)) → sieve#(Y)filter#(s(s(X)), cons(Y, Z)) → filter#(X, sieve(Y))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

The right-hand side of the rule sieve#(cons(X, Y)) → filter#(X, sieve(Y)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
filter#(X, cons(_x32, filter(_x32, sieve(_x31)))) 
Thus, the rule sieve#(cons(X, Y)) → filter#(X, sieve(Y)) is replaced by the following rules:
sieve#(cons(X, cons(_x32, _x31))) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))

Problem 5: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

sieve#(cons(X, cons(_x32, _x31))) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))filter#(s(s(X)), cons(Y, Z)) → sieve#(Y)
sieve#(cons(X, Y)) → sieve#(Y)filter#(s(s(X)), cons(Y, Z)) → filter#(X, sieve(Y))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

The right-hand side of the rule filter#(s(s(X)), cons(Y, Z)) → filter#(X, sieve(Y)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
filter#(X, cons(_x32, filter(_x32, sieve(_x31)))) 
Thus, the rule filter#(s(s(X)), cons(Y, Z)) → filter#(X, sieve(Y)) is replaced by the following rules:
filter#(s(s(X)), cons(cons(_x32, _x31), Z)) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))

Problem 6: ForwardInstantiation

Dependency Pair Problem

Dependency Pairs

sieve#(cons(X, cons(_x32, _x31))) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))filter#(s(s(X)), cons(Y, Z)) → sieve#(Y)
sieve#(cons(X, Y)) → sieve#(Y)filter#(s(s(X)), cons(cons(_x32, _x31), Z)) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Instantiation

For all potential successors l → r of the rule filter#(s(s(X)), cons(Y, Z)) → sieve#(Y) on dependency pair chains it holds that: Thus, filter#(s(s(X)), cons(Y, Z)) → sieve#(Y) is replaced by instances determined through the above matching. These instances are:
filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31)))filter#(s(s(X)), cons(cons(_X, _Y), Z)) → sieve#(cons(_X, _Y))

Instantiation

For all potential successors l → r of the rule sieve#(cons(X, Y)) → sieve#(Y) on dependency pair chains it holds that: Thus, sieve#(cons(X, Y)) → sieve#(Y) is replaced by instances determined through the above matching. These instances are:
sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31)))sieve#(cons(X, cons(_X, _Y))) → sieve#(cons(_X, _Y))

Problem 8: ForwardInstantiation

Dependency Pair Problem

Dependency Pairs

sieve#(cons(X, cons(_x32, _x31))) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31)))
sieve#(cons(X, cons(_X, _Y))) → sieve#(cons(_X, _Y))filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31)))
filter#(s(s(X)), cons(cons(_x32, _x31), Z)) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))filter#(s(s(X)), cons(cons(_X, _Y), Z)) → sieve#(cons(_X, _Y))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Instantiation

For all potential successors l → r of the rule sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31))) on dependency pair chains it holds that: Thus, sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31))) is replaced by instances determined through the above matching. These instances are:
sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31)))sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))

Instantiation

For all potential successors l → r of the rule sieve#(cons(X, cons(_X, _Y))) → sieve#(cons(_X, _Y)) on dependency pair chains it holds that: Thus, sieve#(cons(X, cons(_X, _Y))) → sieve#(cons(_X, _Y)) is replaced by instances determined through the above matching. These instances are:
sieve#(cons(_X, cons(_X, cons(_x32, _x31)))) → sieve#(cons(_X, cons(_x32, _x31)))sieve#(cons(X, cons(_X, cons(___X, ___Y)))) → sieve#(cons(_X, cons(___X, ___Y)))
sieve#(cons(_X, cons(_X, cons(_X, cons(_x32, _x31))))) → sieve#(cons(_X, cons(_X, cons(_x32, _x31))))

Instantiation

For all potential successors l → r of the rule filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31))) on dependency pair chains it holds that: Thus, filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31))) is replaced by instances determined through the above matching. These instances are:
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(__x32, __x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31)))

Instantiation

For all potential successors l → r of the rule filter#(s(s(X)), cons(cons(_X, _Y), Z)) → sieve#(cons(_X, _Y)) on dependency pair chains it holds that: Thus, filter#(s(s(X)), cons(cons(_X, _Y), Z)) → sieve#(cons(_X, _Y)) is replaced by instances determined through the above matching. These instances are:
filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_X, cons(_x32, _x31))))filter#(s(s(X)), cons(cons(_X, cons(___X, ___Y)), Z)) → sieve#(cons(_X, cons(___X, ___Y)))
filter#(s(s(_X)), cons(cons(_X, cons(_x32, _x31)), Z)) → sieve#(cons(_X, cons(_x32, _x31)))

Problem 10: Propagation

Dependency Pair Problem

Dependency Pairs

filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_X, cons(_x32, _x31))))sieve#(cons(X, cons(_x32, _x31))) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(__x32, __x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31)))
filter#(s(s(X)), cons(cons(_X, cons(___X, ___Y)), Z)) → sieve#(cons(_X, cons(___X, ___Y)))filter#(s(s(_X)), cons(cons(_X, cons(_x32, _x31)), Z)) → sieve#(cons(_X, cons(_x32, _x31)))
filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31)))sieve#(cons(_X, cons(_X, cons(_x32, _x31)))) → sieve#(cons(_X, cons(_x32, _x31)))
filter#(s(s(X)), cons(cons(_x32, _x31), Z)) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))sieve#(cons(X, cons(_X, cons(___X, ___Y)))) → sieve#(cons(_X, cons(___X, ___Y)))
sieve#(cons(_X, cons(_X, cons(_X, cons(_x32, _x31))))) → sieve#(cons(_X, cons(_X, cons(_x32, _x31))))sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

The dependency pairs filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_X, cons(_x32, _x31)))) and sieve#(cons(_X, cons(_X, cons(_x32, _x31)))) → sieve#(cons(_X, cons(_x32, _x31))) are consolidated into the rule filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_x32, _x31))) .

This is possible as

Summary

Removed Dependency PairsAdded Dependency Pairs
filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_X, cons(_x32, _x31))))filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_x32, _x31)))
sieve#(cons(_X, cons(_X, cons(_x32, _x31)))) → sieve#(cons(_X, cons(_x32, _x31))) 

Problem 11: BackwardInstantiation

Dependency Pair Problem

Dependency Pairs

sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31)))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(__x32, __x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))
sieve#(cons(X, cons(_x32, _x31))) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))filter#(s(s(_X)), cons(cons(_X, cons(_x32, _x31)), Z)) → sieve#(cons(_X, cons(_x32, _x31)))
filter#(s(s(X)), cons(cons(_X, cons(___X, ___Y)), Z)) → sieve#(cons(_X, cons(___X, ___Y)))filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31)))
filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_x32, _x31)))sieve#(cons(_X, cons(_X, cons(_X, cons(_x32, _x31))))) → sieve#(cons(_X, cons(_X, cons(_x32, _x31))))
sieve#(cons(X, cons(_X, cons(___X, ___Y)))) → sieve#(cons(_X, cons(___X, ___Y)))filter#(s(s(X)), cons(cons(_x32, _x31), Z)) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))
sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Instantiation

For all potential predecessors l → r of the rule sieve#(cons(X, cons(_x32, _x31))) → filter#(X, cons(_x32, filter(_x32, sieve(_x31)))) on dependency pair chains it holds that: Thus, sieve#(cons(X, cons(_x32, _x31))) → filter#(X, cons(_x32, filter(_x32, sieve(_x31)))) is replaced by instances determined through the above matching. These instances are:
sieve#(cons(__X, cons(__X, cons(__x32, __x31)))) → filter#(__X, cons(__X, filter(__X, sieve(cons(__x32, __x31)))))sieve#(cons(__X, cons(__x32, __x31))) → filter#(__X, cons(__x32, filter(__x32, sieve(__x31))))
sieve#(cons(_X, cons(__x32, __x31))) → filter#(_X, cons(__x32, filter(__x32, sieve(__x31))))sieve#(cons(_X, cons(___X, ___Y))) → filter#(_X, cons(___X, filter(___X, sieve(___Y))))
sieve#(cons(__x32, cons(__x32, cons(___x32, ___x31)))) → filter#(__x32, cons(__x32, filter(__x32, sieve(cons(___x32, ___x31)))))

Problem 13: ForwardInstantiation

Dependency Pair Problem

Dependency Pairs

sieve#(cons(__X, cons(__X, cons(__x32, __x31)))) → filter#(__X, cons(__X, filter(__X, sieve(cons(__x32, __x31)))))sieve#(cons(_X, cons(__x32, __x31))) → filter#(_X, cons(__x32, filter(__x32, sieve(__x31))))
filter#(s(s(X)), cons(cons(_X, cons(___X, ___Y)), Z)) → sieve#(cons(_X, cons(___X, ___Y)))filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_x32, _x31)))
sieve#(cons(X, cons(_X, cons(___X, ___Y)))) → sieve#(cons(_X, cons(___X, ___Y)))sieve#(cons(_X, cons(_X, cons(_X, cons(_x32, _x31))))) → sieve#(cons(_X, cons(_X, cons(_x32, _x31))))
sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(__x32, __x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))
sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31)))sieve#(cons(__X, cons(__x32, __x31))) → filter#(__X, cons(__x32, filter(__x32, sieve(__x31))))
sieve#(cons(_X, cons(___X, ___Y))) → filter#(_X, cons(___X, filter(___X, sieve(___Y))))filter#(s(s(_X)), cons(cons(_X, cons(_x32, _x31)), Z)) → sieve#(cons(_X, cons(_x32, _x31)))
filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31)))filter#(s(s(X)), cons(cons(_x32, _x31), Z)) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))
sieve#(cons(__x32, cons(__x32, cons(___x32, ___x31)))) → filter#(__x32, cons(__x32, filter(__x32, sieve(cons(___x32, ___x31)))))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Instantiation

For all potential successors l → r of the rule filter#(s(s(X)), cons(cons(_X, cons(___X, ___Y)), Z)) → sieve#(cons(_X, cons(___X, ___Y))) on dependency pair chains it holds that: Thus, filter#(s(s(X)), cons(cons(_X, cons(___X, ___Y)), Z)) → sieve#(cons(_X, cons(___X, ___Y))) is replaced by instances determined through the above matching. These instances are:
filter#(s(s(X)), cons(cons(_X, cons(___X, ___Y)), Z)) → sieve#(cons(_X, cons(___X, ___Y)))filter#(s(s(X)), cons(cons(_X, cons(___X, cons(_______X, _______Y))), Z)) → sieve#(cons(_X, cons(___X, cons(_______X, _______Y))))
filter#(s(s(___X)), cons(cons(___X, cons(___X, cons(_x32, _x31))), Z)) → sieve#(cons(___X, cons(___X, cons(_x32, _x31))))filter#(s(s(X)), cons(cons(___X, cons(___X, cons(__x32, __x31))), Z)) → sieve#(cons(___X, cons(___X, cons(__x32, __x31))))
filter#(s(s(X)), cons(cons(___X, cons(___X, cons(___X, cons(__x32, __x31)))), Z)) → sieve#(cons(___X, cons(___X, cons(___X, cons(__x32, __x31)))))filter#(s(s(X)), cons(cons(___X, cons(___X, cons(___x32, ___x31))), Z)) → sieve#(cons(___X, cons(___X, cons(___x32, ___x31))))

Instantiation

For all potential successors l → r of the rule filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_x32, _x31))) on dependency pair chains it holds that: Thus, filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_x32, _x31))) is replaced by instances determined through the above matching. These instances are:
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31))))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))
filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, cons(_____X, _____Y)))), Z)) → sieve#(cons(_X, cons(_x32, cons(_____X, _____Y))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(___x32, ___x31))))
filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_x32, _x31)))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))

Instantiation

For all potential successors l → r of the rule sieve#(cons(X, cons(_X, cons(___X, ___Y)))) → sieve#(cons(_X, cons(___X, ___Y))) on dependency pair chains it holds that: Thus, sieve#(cons(X, cons(_X, cons(___X, ___Y)))) → sieve#(cons(_X, cons(___X, ___Y))) is replaced by instances determined through the above matching. These instances are:
sieve#(cons(X, cons(___X, cons(___X, cons(___X, cons(__x32, __x31)))))) → sieve#(cons(___X, cons(___X, cons(___X, cons(__x32, __x31)))))sieve#(cons(___X, cons(___X, cons(___X, cons(_x32, _x31))))) → sieve#(cons(___X, cons(___X, cons(_x32, _x31))))
sieve#(cons(X, cons(___X, cons(___X, cons(__x32, __x31))))) → sieve#(cons(___X, cons(___X, cons(__x32, __x31))))sieve#(cons(X, cons(___X, cons(___X, cons(___x32, ___x31))))) → sieve#(cons(___X, cons(___X, cons(___x32, ___x31))))
sieve#(cons(X, cons(_X, cons(___X, ___Y)))) → sieve#(cons(_X, cons(___X, ___Y)))sieve#(cons(X, cons(_X, cons(___X, cons(_______X, _______Y))))) → sieve#(cons(_X, cons(___X, cons(_______X, _______Y))))

Instantiation

For all potential successors l → r of the rule sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31))) on dependency pair chains it holds that: Thus, sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31))) is replaced by instances determined through the above matching. These instances are:
sieve#(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31)))
sieve#(cons(X, cons(X, cons(_x32, cons(____X, ____Y))))) → sieve#(cons(X, cons(_x32, cons(____X, ____Y))))sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31))))) → sieve#(cons(_x32, cons(_x32, cons(___x32, ___x31))))
sieve#(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))

Instantiation

For all potential successors l → r of the rule filter#(s(s(_X)), cons(cons(_X, cons(_x32, _x31)), Z)) → sieve#(cons(_X, cons(_x32, _x31))) on dependency pair chains it holds that: Thus, filter#(s(s(_X)), cons(cons(_X, cons(_x32, _x31)), Z)) → sieve#(cons(_X, cons(_x32, _x31))) is replaced by instances determined through the above matching. These instances are:
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(__x32, __x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))
filter#(s(s(_X)), cons(cons(_X, cons(_x32, cons(_____X, _____Y))), Z)) → sieve#(cons(_X, cons(_x32, cons(_____X, _____Y))))filter#(s(s(_X)), cons(cons(_X, cons(_x32, _x31)), Z)) → sieve#(cons(_X, cons(_x32, _x31)))
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(___x32, ___x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(___x32, ___x31))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))

Instantiation

For all potential successors l → r of the rule filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31))) on dependency pair chains it holds that: Thus, filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31))) is replaced by instances determined through the above matching. These instances are:
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(__x32, __x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))
filter#(s(s(X)), cons(cons(X, cons(_x32, cons(____X, ____Y))), Z)) → sieve#(cons(X, cons(_x32, cons(____X, ____Y))))filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31)))
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(___x32, ___x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(___x32, ___x31))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))

Problem 14: Propagation

Dependency Pair Problem

Dependency Pairs

sieve#(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))
sieve#(cons(__X, cons(__X, cons(__x32, __x31)))) → filter#(__X, cons(__X, filter(__X, sieve(cons(__x32, __x31)))))sieve#(cons(X, cons(___X, cons(___X, cons(___X, cons(__x32, __x31)))))) → sieve#(cons(___X, cons(___X, cons(___X, cons(__x32, __x31)))))
filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, cons(_____X, _____Y)))), Z)) → sieve#(cons(_X, cons(_x32, cons(_____X, _____Y))))filter#(s(s(X)), cons(cons(_X, cons(___X, ___Y)), Z)) → sieve#(cons(_X, cons(___X, ___Y)))
filter#(s(s(_X)), cons(cons(_X, cons(_x32, cons(_____X, _____Y))), Z)) → sieve#(cons(_X, cons(_x32, cons(_____X, _____Y))))sieve#(cons(___X, cons(___X, cons(___X, cons(_x32, _x31))))) → sieve#(cons(___X, cons(___X, cons(_x32, _x31))))
filter#(s(s(X)), cons(cons(_X, cons(___X, cons(_______X, _______Y))), Z)) → sieve#(cons(_X, cons(___X, cons(_______X, _______Y))))filter#(s(s(_X)), cons(cons(_X, cons(_X, cons(_x32, _x31))), Z)) → sieve#(cons(_X, cons(_x32, _x31)))
sieve#(cons(X, cons(___X, cons(___X, cons(__x32, __x31))))) → sieve#(cons(___X, cons(___X, cons(__x32, __x31))))sieve#(cons(X, cons(___X, cons(___X, cons(___x32, ___x31))))) → sieve#(cons(___X, cons(___X, cons(___x32, ___x31))))
sieve#(cons(X, cons(_X, cons(___X, ___Y)))) → sieve#(cons(_X, cons(___X, ___Y)))sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31))))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))filter#(s(s(X)), cons(cons(X, cons(_x32, cons(____X, ____Y))), Z)) → sieve#(cons(X, cons(_x32, cons(____X, ____Y))))
filter#(s(s(_X)), cons(cons(_X, cons(_x32, _x31)), Z)) → sieve#(cons(_X, cons(_x32, _x31)))sieve#(cons(X, cons(X, cons(_x32, cons(____X, ____Y))))) → sieve#(cons(X, cons(_x32, cons(____X, ____Y))))
filter#(s(s(X)), cons(cons(X, cons(_x32, _x31)), Z)) → sieve#(cons(X, cons(_x32, _x31)))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))
filter#(s(s(X)), cons(cons(_x32, _x31), Z)) → filter#(X, cons(_x32, filter(_x32, sieve(_x31))))filter#(s(s(X)), cons(cons(___X, cons(___X, cons(__x32, __x31))), Z)) → sieve#(cons(___X, cons(___X, cons(__x32, __x31))))
sieve#(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))filter#(s(s(X)), cons(cons(___X, cons(___X, cons(___X, cons(__x32, __x31)))), Z)) → sieve#(cons(___X, cons(___X, cons(___X, cons(__x32, __x31)))))
sieve#(cons(_X, cons(__x32, __x31))) → filter#(_X, cons(__x32, filter(__x32, sieve(__x31))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(___x32, ___x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(___x32, ___x31))))
sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31))))) → sieve#(cons(_x32, cons(_x32, cons(___x32, ___x31))))sieve#(cons(_X, cons(_X, cons(_X, cons(_x32, _x31))))) → sieve#(cons(_X, cons(_X, cons(_x32, _x31))))
filter#(s(s(X)), cons(cons(___X, cons(___X, cons(___x32, ___x31))), Z)) → sieve#(cons(___X, cons(___X, cons(___x32, ___x31))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))))
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(__x32, __x31))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))sieve#(cons(__X, cons(__x32, __x31))) → filter#(__X, cons(__x32, filter(__x32, sieve(__x31))))
sieve#(cons(X, cons(X, cons(_x32, _x31)))) → sieve#(cons(X, cons(_x32, _x31)))sieve#(cons(_X, cons(___X, ___Y))) → filter#(_X, cons(___X, filter(___X, sieve(___Y))))
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(___x32, ___x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(___x32, ___x31))))filter#(s(s(___X)), cons(cons(___X, cons(___X, cons(_x32, _x31))), Z)) → sieve#(cons(___X, cons(___X, cons(_x32, _x31))))
sieve#(cons(__x32, cons(__x32, cons(___x32, ___x31)))) → filter#(__x32, cons(__x32, filter(__x32, sieve(cons(___x32, ___x31)))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))
sieve#(cons(X, cons(_X, cons(___X, cons(_______X, _______Y))))) → sieve#(cons(_X, cons(___X, cons(_______X, _______Y))))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

The dependency pairs filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) and sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31)))) are consolidated into the rule filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31)))) .

This is possible as

Summary

Removed Dependency PairsAdded Dependency Pairs
filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))), Z)) → sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31)))))filter#(s(s(_x32)), cons(cons(_x32, cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))), Z)) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31))))
sieve#(cons(_x32, cons(_x32, cons(_x32, cons(__x32, __x31))))) → sieve#(cons(_x32, cons(_x32, cons(__x32, __x31)))) 

Problem 3: BackwardInstantiation

Dependency Pair Problem

Dependency Pairs

from#(X) → from#(s(X))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Instantiation

For all potential predecessors l → r of the rule from#(X) → from#(s(X)) on dependency pair chains it holds that: Thus, from#(X) → from#(s(X)) is replaced by instances determined through the above matching. These instances are:
from#(s(_X)) → from#(s(s(_X)))

Problem 7: BackwardInstantiation

Dependency Pair Problem

Dependency Pairs

from#(s(_X)) → from#(s(s(_X)))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Instantiation

For all potential predecessors l → r of the rule from#(s(_X)) → from#(s(s(_X))) on dependency pair chains it holds that: Thus, from#(s(_X)) → from#(s(s(_X))) is replaced by instances determined through the above matching. These instances are:
from#(s(s(__X))) → from#(s(s(s(__X))))

Problem 9: BackwardInstantiation

Dependency Pair Problem

Dependency Pairs

from#(s(s(__X))) → from#(s(s(s(__X))))

Rewrite Rules

primes → sieve(from(s(s(0))))from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → Xtail(cons(X, Y)) → Y
if(true, X, Y) → Xif(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

Original Signature

Termination of terms over the following signature is verified: sieve, true, divides, from, tail, 0, s, if, false, primes, head, filter, cons

Strategy

Instantiation

For all potential predecessors l → r of the rule from#(s(s(__X))) → from#(s(s(s(__X)))) on dependency pair chains it holds that: Thus, from#(s(s(__X))) → from#(s(s(s(__X)))) is replaced by instances determined through the above matching. These instances are:
from#(s(s(s(___X)))) → from#(s(s(s(s(___X)))))