The TRS could not be proven terminating. The proof attempt took 60018 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (1099ms), SubtermCriterion (1ms), DependencyGraph (1052ms), PolynomialLinearRange4iUR (7233ms), DependencyGraph (1016ms), PolynomialLinearRange8NegiUR (19784ms), DependencyGraph (981ms), ReductionPairSAT (timeout)].
| app#(app(*, app(s, x)), y) | → | app#(*, x) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) | 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#(app(app(app(filter2, true), f), x), xs) | → | app#(filter, f) | |
| app#(app(+, x), app(s, y)) | → | app#(app(+, x), y) | app#(app(app(app(filter2, true), f), x), xs) | → | app#(app(filter, f), xs) | |
| app#(fact, app(s, x)) | → | app#(app(*, app(s, x)), app(fact, app(p, app(s, x)))) | app#(app(filter, f), app(app(cons, x), xs)) | → | app#(app(app(app(filter2, app(f, x)), f), x), xs) | |
| app#(app(*, app(s, x)), y) | → | app#(app(+, app(app(*, x), y)), y) | app#(app(filter, f), app(app(cons, x), xs)) | → | app#(filter2, app(f, x)) | |
| app#(fact, app(s, x)) | → | app#(p, app(s, x)) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(map, f) | |
| app#(app(app(app(filter2, false), f), x), xs) | → | app#(filter, f) | app#(fact, app(s, x)) | → | app#(s, x) | |
| app#(fact, 0) | → | app#(s, 0) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | |
| app#(app(*, app(s, x)), y) | → | app#(app(*, x), y) | app#(app(*, app(s, x)), y) | → | app#(+, app(app(*, x), y)) | |
| app#(app(filter, f), app(app(cons, x), xs)) | → | app#(app(app(filter2, app(f, x)), f), x) | app#(app(filter, f), app(app(cons, x), xs)) | → | app#(app(filter2, app(f, x)), f) | |
| app#(app(app(app(filter2, true), f), x), xs) | → | app#(cons, x) | app#(fact, app(s, x)) | → | app#(fact, app(p, app(s, x))) | |
| app#(app(+, x), app(s, y)) | → | app#(+, x) | app#(app(app(app(filter2, false), f), x), xs) | → | app#(app(filter, f), xs) | |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(cons, app(f, x)) | app#(app(+, x), app(s, y)) | → | app#(s, app(app(+, x), y)) | |
| app#(fact, app(s, x)) | → | app#(*, app(s, x)) |
| app(p, app(s, x)) | → | x | app(fact, 0) | → | app(s, 0) | |
| app(fact, app(s, x)) | → | app(app(*, app(s, x)), app(fact, app(p, app(s, x)))) | app(app(*, 0), y) | → | 0 | |
| app(app(*, app(s, x)), y) | → | app(app(+, app(app(*, x), y)), y) | app(app(+, x), 0) | → | x | |
| app(app(+, x), app(s, y)) | → | app(s, app(app(+, x), 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: app, *, +, true, fact, 0, s, p, map, false, filter2, filter, nil, cons