The TRS could not be proven terminating. The proof attempt took 60002 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (192ms), SubtermCriterion (1ms), DependencyGraph (148ms), PolynomialLinearRange4iUR (3373ms), DependencyGraph (166ms), PolynomialLinearRange8NegiUR (11073ms), DependencyGraph (123ms), ReductionPairSAT (timeout)].
| 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#(flatten, app(app(node, x), xs)) | → | app#(app(map, flatten), xs) | app#(flatten, app(app(node, x), xs)) | → | app#(map, flatten) | |
| app#(flatten, app(app(node, x), xs)) | → | app#(concat, app(app(map, flatten), xs)) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | |
| app#(app(append, app(app(cons, x), xs)), ys) | → | app#(app(append, xs), ys) | app#(concat, app(app(cons, x), xs)) | → | app#(app(append, x), app(concat, xs)) | |
| app#(concat, app(app(cons, x), xs)) | → | app#(append, x) | app#(concat, app(app(cons, x), xs)) | → | app#(concat, xs) | |
| app#(app(append, app(app(cons, x), xs)), ys) | → | app#(app(cons, x), app(app(append, xs), ys)) | app#(app(append, app(app(cons, x), xs)), ys) | → | app#(append, xs) | |
| app#(flatten, app(app(node, x), xs)) | → | app#(app(cons, x), app(concat, app(app(map, flatten), xs))) | app#(app(append, app(app(cons, x), xs)), ys) | → | app#(cons, x) | |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(cons, app(f, x)) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(map, f) | |
| app#(flatten, app(app(node, x), xs)) | → | app#(cons, x) |
| 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(flatten, app(app(node, x), xs)) | → | app(app(cons, x), app(concat, app(app(map, flatten), xs))) | app(concat, nil) | → | nil | |
| app(concat, app(app(cons, x), xs)) | → | app(app(append, x), app(concat, xs)) | app(app(append, nil), xs) | → | xs | |
| app(app(append, app(app(cons, x), xs)), ys) | → | app(app(cons, x), app(app(append, xs), ys)) |
Termination of terms over the following signature is verified: append, app, node, flatten, map, concat, cons, nil