The TRS could not be proven terminating. The proof attempt took 60088 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (135ms), SubtermCriterion (1ms), DependencyGraph (76ms), PolynomialLinearRange4iUR (2620ms), DependencyGraph (69ms), PolynomialLinearRange8NegiUR (12901ms), DependencyGraph (61ms), ReductionPairSAT (44148ms), DependencyGraph (timeout)].
| app#(app(app(filtersub, true), f), app(app(cons, y), ys)) | → | app#(filter, f) | app#(app(filter, f), app(app(cons, y), ys)) | → | app#(filtersub, app(f, y)) | |
| app#(app(filter, f), app(app(cons, y), ys)) | → | app#(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys)) | app#(app(app(filtersub, false), f), app(app(cons, y), ys)) | → | app#(app(filter, f), ys) | |
| app#(app(filter, f), app(app(cons, y), ys)) | → | app#(app(filtersub, app(f, y)), f) | app#(app(app(filtersub, true), f), app(app(cons, y), ys)) | → | app#(app(cons, y), app(app(filter, f), ys)) | |
| app#(app(filter, f), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) | app#(app(app(filtersub, true), f), app(app(cons, y), ys)) | → | app#(cons, y) | |
| app#(app(app(filtersub, true), f), app(app(cons, y), ys)) | → | app#(app(filter, f), ys) | app#(app(filter, f), app(app(cons, y), ys)) | → | app#(cons, y) | |
| app#(app(app(filtersub, false), f), app(app(cons, y), ys)) | → | app#(filter, f) | app#(app(filter, f), app(app(cons, y), ys)) | → | app#(f, y) |
| app(app(filter, f), nil) | → | nil | app(app(filter, f), app(app(cons, y), ys)) | → | app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys)) | |
| app(app(app(filtersub, true), f), app(app(cons, y), ys)) | → | app(app(cons, y), app(app(filter, f), ys)) | app(app(app(filtersub, false), f), app(app(cons, y), ys)) | → | app(app(filter, f), ys) |
Termination of terms over the following signature is verified: app, false, true, filtersub, filter, cons, nil