The TRS could not be proven terminating. The proof attempt took 60018 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (837ms), SubtermCriterion (1ms), DependencyGraph (786ms), PolynomialLinearRange4iUR (8850ms), DependencyGraph (725ms), PolynomialLinearRange8NegiUR (25385ms), DependencyGraph (697ms), ReductionPairSAT (timeout)].
| a#(a(append, a(a(cons, x), xs)), ys) | → | a#(a(append, xs), ys) | a#(qs, a(a(cons, x), xs)) | → | a#(qs, a(a(filter, a(not, a(le, x))), xs)) | |
| a#(qs, a(a(cons, x), xs)) | → | a#(a(filter, a(not, a(le, x))), xs) | a#(a(append, a(a(cons, x), xs)), ys) | → | a#(append, xs) | |
| a#(a(append, a(a(cons, x), xs)), ys) | → | a#(a(cons, x), a(a(append, xs), ys)) | a#(a(not, f), b) | → | a#(not2, a(f, b)) | |
| a#(a(not, f), b) | → | a#(f, b) | a#(a(a(if, true), x), xs) | → | a#(cons, x) | |
| a#(a(append, a(a(cons, x), xs)), ys) | → | a#(cons, x) | a#(qs, a(a(cons, x), xs)) | → | a#(filter, a(not, a(le, x))) | |
| a#(a(filter, f), a(a(cons, x), xs)) | → | a#(f, x) | a#(qs, a(a(cons, x), xs)) | → | a#(qs, a(a(filter, a(le, x)), xs)) | |
| a#(qs, a(a(cons, x), xs)) | → | a#(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs))) | a#(qs, a(a(cons, x), xs)) | → | a#(not, a(le, x)) | |
| a#(qs, a(a(cons, x), xs)) | → | a#(a(filter, a(le, x)), xs) | a#(a(le, a(s, x)), a(s, y)) | → | a#(le, x) | |
| a#(a(filter, f), a(a(cons, x), xs)) | → | a#(a(if, a(f, x)), x) | a#(qs, a(a(cons, x), xs)) | → | a#(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs)))) | |
| a#(a(a(if, true), x), xs) | → | a#(a(cons, x), xs) | a#(a(le, a(s, x)), a(s, y)) | → | a#(a(le, x), y) | |
| a#(qs, a(a(cons, x), xs)) | → | a#(append, a(qs, a(a(filter, a(le, x)), xs))) | a#(qs, a(a(cons, x), xs)) | → | a#(filter, a(le, x)) | |
| a#(qs, a(a(cons, x), xs)) | → | a#(cons, x) | a#(a(filter, f), a(a(cons, x), xs)) | → | a#(a(a(if, a(f, x)), x), a(a(filter, f), xs)) | |
| a#(a(filter, f), a(a(cons, x), xs)) | → | a#(filter, f) | a#(a(filter, f), a(a(cons, x), xs)) | → | a#(if, a(f, x)) | |
| a#(a(filter, f), a(a(cons, x), xs)) | → | a#(a(filter, f), xs) | a#(qs, a(a(cons, x), xs)) | → | a#(le, x) |
| a(a(append, nil), ys) | → | ys | a(a(append, a(a(cons, x), xs)), ys) | → | a(a(cons, x), a(a(append, xs), ys)) | |
| 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(le, 0), y) | → | true | a(a(le, a(s, x)), 0) | → | false | |
| a(a(le, a(s, x)), a(s, y)) | → | a(a(le, x), y) | a(a(a(if, true), x), xs) | → | a(a(cons, x), xs) | |
| a(a(a(if, false), x), xs) | → | xs | a(a(not, f), b) | → | a(not2, a(f, b)) | |
| a(not2, true) | → | false | a(not2, false) | → | true | |
| a(qs, nil) | → | nil | a(qs, a(a(cons, x), xs)) | → | a(a(append, a(qs, a(a(filter, a(le, x)), xs))), a(a(cons, x), a(qs, a(a(filter, a(not, a(le, x))), xs)))) |
Termination of terms over the following signature is verified: append, a, true, not, 0, le, s, if, not2, false, qs, filter, nil, cons