The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (19536ms), SubtermCriterion (3ms), DependencyGraph (18780ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (timeout)].
| app#(D, app(app(-, x), y)) | → | app#(app(-, app(D, x)), app(D, y)) | app#(D, app(app(-, x), y)) | → | app#(-, app(D, x)) | |
| app#(app(app(app(filter2, true), f), x), xs) | → | app#(app(filter, f), xs) | app#(D, app(app(div, x), y)) | → | app#(div, app(D, x)) | |
| app#(D, app(app(div, x), y)) | → | app#(*, x) | app#(D, app(app(pow, x), y)) | → | app#(D, y) | |
| app#(D, app(app(*, x), y)) | → | app#(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y))) | app#(D, app(app(pow, x), y)) | → | app#(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))) | |
| app#(D, app(app(*, x), y)) | → | app#(*, x) | app#(D, app(app(div, x), y)) | → | app#(D, y) | |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(map, f) | app#(D, app(app(div, x), y)) | → | app#(app(*, x), app(D, y)) | |
| app#(app(app(app(filter2, false), f), x), xs) | → | app#(filter, f) | app#(D, app(app(pow, x), y)) | → | app#(app(*, y), app(app(pow, x), app(app(-, y), 1))) | |
| app#(D, app(app(-, x), y)) | → | app#(D, y) | app#(D, app(app(pow, x), y)) | → | app#(*, app(app(pow, x), y)) | |
| app#(D, app(app(div, x), y)) | → | app#(div, app(app(*, x), app(D, y))) | app#(D, app(app(pow, x), y)) | → | app#(+, app(app(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))), app(D, x))) | |
| app#(D, app(app(*, x), y)) | → | app#(D, y) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | |
| app#(D, app(app(pow, x), y)) | → | app#(*, app(app(*, app(app(pow, x), y)), app(ln, x))) | app#(app(filter, f), app(app(cons, x), xs)) | → | app#(app(app(filter2, app(f, x)), f), x) | |
| app#(D, app(app(pow, x), y)) | → | app#(app(-, y), 1) | app#(D, app(app(+, x), y)) | → | app#(app(+, app(D, x)), app(D, y)) | |
| app#(D, app(ln, x)) | → | app#(D, x) | app#(D, app(app(pow, x), y)) | → | app#(D, x) | |
| app#(D, app(app(*, x), y)) | → | app#(app(*, y), app(D, x)) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(cons, app(f, x)) | |
| app#(D, app(app(pow, x), y)) | → | app#(-, y) | app#(D, app(app(+, x), y)) | → | app#(D, y) | |
| app#(D, app(app(*, x), y)) | → | app#(D, x) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) | |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | app#(app(app(app(filter2, true), f), x), xs) | → | app#(app(cons, x), app(app(filter, f), xs)) | |
| app#(app(filter, f), app(app(cons, x), xs)) | → | app#(f, x) | app#(D, app(app(pow, x), y)) | → | app#(app(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))), app(D, x)) | |
| app#(D, app(app(pow, x), y)) | → | app#(pow, x) | app#(app(app(app(filter2, true), f), x), xs) | → | app#(filter, f) | |
| app#(D, app(app(pow, x), y)) | → | app#(ln, x) | app#(D, app(app(div, x), y)) | → | app#(-, app(app(div, app(D, x)), y)) | |
| app#(D, app(app(div, x), y)) | → | app#(app(pow, y), 2) | app#(app(filter, f), app(app(cons, x), xs)) | → | app#(app(app(app(filter2, app(f, x)), f), x), xs) | |
| app#(D, app(app(div, x), y)) | → | app#(app(-, app(app(div, app(D, x)), y)), app(app(div, app(app(*, x), app(D, y))), app(app(pow, y), 2))) | app#(D, app(app(*, x), y)) | → | app#(+, app(app(*, y), app(D, x))) | |
| app#(D, app(app(*, x), y)) | → | app#(*, y) | app#(app(filter, f), app(app(cons, x), xs)) | → | app#(filter2, app(f, x)) | |
| app#(D, app(app(pow, x), y)) | → | app#(app(*, app(app(pow, x), y)), app(ln, x)) | app#(D, app(app(pow, x), y)) | → | app#(app(pow, x), app(app(-, y), 1)) | |
| app#(D, app(app(*, x), y)) | → | app#(app(*, x), app(D, y)) | app#(D, app(app(div, x), y)) | → | app#(pow, y) | |
| app#(D, app(app(pow, x), y)) | → | app#(app(+, app(app(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))), app(D, x))), app(app(*, app(app(*, app(app(pow, x), y)), app(ln, x))), app(D, y))) | app#(D, app(app(pow, x), y)) | → | app#(app(pow, x), y) | |
| app#(D, app(app(pow, x), y)) | → | app#(*, y) | app#(D, app(minus, x)) | → | app#(minus, app(D, x)) | |
| app#(D, app(app(-, x), y)) | → | app#(D, x) | app#(D, app(minus, x)) | → | app#(D, x) | |
| app#(D, app(ln, x)) | → | app#(div, app(D, x)) | app#(D, app(app(div, x), y)) | → | app#(D, x) | |
| app#(app(app(app(filter2, true), f), x), xs) | → | app#(cons, x) | app#(app(filter, f), app(app(cons, x), xs)) | → | app#(app(filter2, app(f, x)), f) | |
| app#(D, app(app(+, x), y)) | → | app#(+, app(D, x)) | app#(D, app(app(div, x), y)) | → | app#(app(div, app(D, x)), y) | |
| app#(D, app(app(+, x), y)) | → | app#(D, x) | app#(D, app(app(div, x), y)) | → | app#(app(div, app(app(*, x), app(D, y))), app(app(pow, y), 2)) | |
| app#(D, app(ln, x)) | → | app#(app(div, app(D, x)), x) | app#(D, app(app(pow, x), y)) | → | app#(app(*, app(app(*, app(app(pow, x), y)), app(ln, x))), app(D, y)) | |
| app#(app(app(app(filter2, false), f), x), xs) | → | app#(app(filter, f), xs) |
| app(D, t) | → | 1 | app(D, constant) | → | 0 | |
| app(D, app(app(+, x), y)) | → | app(app(+, app(D, x)), app(D, y)) | app(D, app(app(*, x), y)) | → | app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y))) | |
| app(D, app(app(-, x), y)) | → | app(app(-, app(D, x)), app(D, y)) | app(D, app(minus, x)) | → | app(minus, app(D, x)) | |
| app(D, app(app(div, x), y)) | → | app(app(-, app(app(div, app(D, x)), y)), app(app(div, app(app(*, x), app(D, y))), app(app(pow, y), 2))) | app(D, app(ln, x)) | → | app(app(div, app(D, x)), x) | |
| app(D, app(app(pow, x), y)) | → | app(app(+, app(app(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))), app(D, x))), app(app(*, app(app(*, app(app(pow, x), y)), app(ln, x))), app(D, y))) | app(app(map, f), nil) | → | nil | |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | app(app(filter, f), nil) | → | nil | |
| app(app(filter, f), app(app(cons, x), xs)) | → | app(app(app(app(filter2, app(f, x)), f), x), xs) | app(app(app(app(filter2, true), f), x), xs) | → | app(app(cons, x), app(app(filter, f), xs)) | |
| app(app(app(app(filter2, false), f), x), xs) | → | app(app(filter, f), xs) |
Termination of terms over the following signature is verified: D, ln, app, constant, minus, pow, *, div, true, +, -, 2, 1, t, 0, map, false, filter2, filter, cons, nil