The TRS could not be proven terminating. The proof attempt took 60029 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (832ms), SubtermCriterion (3ms), DependencyGraph (717ms), PolynomialLinearRange4iUR (6577ms), DependencyGraph (680ms), PolynomialLinearRange8NegiUR (19255ms), DependencyGraph (657ms), ReductionPairSAT (timeout)].
| a#(a(divides, a(s, x)), a(s, y)) | → | a#(div2, x) | a#(sieve, a(a(cons, x), xs)) | → | a#(not, a(divides, x)) | |
| a#(sieve, a(a(cons, x), xs)) | → | a#(a(filter, a(not, a(divides, x))), xs) | a#(a(a(if, true), x), xs) | → | a#(cons, x) | |
| a#(a(a(div2, a(s, x)), y), a(s, z)) | → | a#(div2, x) | a#(a(filter, f), a(a(cons, x), xs)) | → | a#(f, x) | |
| a#(sieve, a(a(cons, x), xs)) | → | a#(filter, a(not, a(divides, x))) | a#(a(divides, a(s, x)), a(s, y)) | → | a#(a(a(div2, x), a(s, y)), y) | |
| a#(sieve, a(a(cons, x), xs)) | → | a#(cons, x) | a#(sieve, a(a(cons, x), xs)) | → | a#(sieve, a(a(filter, a(not, a(divides, x))), xs)) | |
| a#(a(divides, a(s, x)), a(s, y)) | → | a#(s, y) | a#(a(divides, a(s, x)), a(s, y)) | → | a#(a(div2, x), a(s, y)) | |
| a#(a(filter, f), a(a(cons, x), xs)) | → | a#(a(if, a(f, x)), x) | a#(a(a(div2, a(s, x)), y), a(s, z)) | → | a#(a(div2, x), y) | |
| a#(a(a(if, true), x), xs) | → | a#(a(cons, x), xs) | a#(a(a(div2, x), y), 0) | → | a#(divides, x) | |
| a#(a(a(div2, a(s, x)), y), a(s, z)) | → | a#(a(a(div2, x), y), z) | a#(a(not, f), x) | → | a#(f, x) | |
| a#(a(not, f), x) | → | a#(not2, a(f, x)) | a#(a(filter, f), a(a(cons, x), xs)) | → | a#(a(a(if, a(f, x)), x), a(a(filter, f), xs)) | |
| a#(sieve, a(a(cons, x), xs)) | → | a#(a(cons, x), a(sieve, a(a(filter, a(not, a(divides, x))), xs))) | a#(a(filter, f), a(a(cons, x), xs)) | → | a#(if, a(f, x)) | |
| a#(a(filter, f), a(a(cons, x), xs)) | → | a#(filter, f) | a#(a(filter, f), a(a(cons, x), xs)) | → | a#(a(filter, f), xs) | |
| a#(sieve, a(a(cons, x), xs)) | → | a#(divides, x) | a#(a(a(div2, x), y), 0) | → | a#(a(divides, x), y) |
| a(a(divides, 0), a(s, y)) | → | true | a(a(divides, a(s, x)), a(s, y)) | → | a(a(a(div2, x), a(s, y)), y) | |
| a(a(a(div2, x), y), 0) | → | a(a(divides, x), y) | a(a(a(div2, 0), y), a(s, z)) | → | false | |
| a(a(a(div2, a(s, x)), y), a(s, z)) | → | a(a(a(div2, x), y), z) | a(a(filter, f), nil) | → | nil | |
| a(a(filter, f), a(a(cons, x), xs)) | → | a(a(a(if, a(f, x)), x), a(a(filter, f), xs)) | a(a(a(if, true), x), xs) | → | a(a(cons, x), xs) | |
| a(a(a(if, false), x), xs) | → | xs | a(a(not, f), x) | → | a(not2, a(f, x)) | |
| a(not2, true) | → | false | a(not2, false) | → | true | |
| a(sieve, nil) | → | nil | a(sieve, a(a(cons, x), xs)) | → | a(a(cons, x), a(sieve, a(a(filter, a(not, a(divides, x))), xs))) |
Termination of terms over the following signature is verified: sieve, a, true, divides, not, 0, s, if, not2, false, div2, filter, nil, cons