The TRS could not be proven terminating. The proof attempt took 60041 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (874ms), SubtermCriterion (1ms), DependencyGraph (793ms), PolynomialLinearRange4iUR (7715ms), DependencyGraph (711ms), PolynomialLinearRange8NegiUR (24687ms), DependencyGraph (728ms), ReductionPairSAT (timeout)].
| 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(combine, xs), app(app(cons, ys), yss)) | → | app#(app(zip, xs), ys) | app#(levels, app(app(node, x), xs)) | → | app#(app(map, levels), xs) | |
| app#(levels, app(app(node, x), xs)) | → | app#(cons, app(app(cons, x), nil)) | app#(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) | → | app#(app(zip, xss), yss) | |
| app#(levels, app(app(node, x), xs)) | → | app#(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs))) | app#(levels, app(app(node, x), xs)) | → | app#(app(combine, nil), app(app(map, levels), xs)) | |
| app#(app(append, app(app(cons, x), xs)), ys) | → | app#(app(cons, x), app(app(append, xs), ys)) | app#(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) | → | app#(zip, xss) | |
| app#(app(append, app(app(cons, x), xs)), ys) | → | app#(append, xs) | app#(levels, app(app(node, x), xs)) | → | app#(cons, x) | |
| app#(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) | → | app#(app(append, xs), ys) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(map, f) | |
| app#(levels, app(app(node, x), xs)) | → | app#(app(cons, x), nil) | app#(levels, app(app(node, x), xs)) | → | app#(combine, nil) | |
| app#(levels, app(app(node, x), xs)) | → | app#(map, levels) | app#(app(combine, xs), app(app(cons, ys), yss)) | → | app#(combine, app(app(zip, xs), ys)) | |
| app#(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) | → | app#(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss)) | app#(app(combine, xs), app(app(cons, ys), yss)) | → | app#(zip, xs) | |
| app#(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) | → | app#(append, 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#(app(combine, xs), app(app(cons, ys), yss)) | → | app#(app(combine, app(app(zip, xs), ys)), yss) | |
| app#(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) | → | app#(cons, app(app(append, xs), ys)) | 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), nil) | → | nil | app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | |
| app(app(append, xs), nil) | → | xs | app(app(append, nil), ys) | → | ys | |
| app(app(append, app(app(cons, x), xs)), ys) | → | app(app(cons, x), app(app(append, xs), ys)) | app(app(zip, nil), yss) | → | yss | |
| app(app(zip, xss), nil) | → | xss | app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) | → | app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss)) | |
| app(app(combine, xs), nil) | → | xs | app(app(combine, xs), app(app(cons, ys), yss)) | → | app(app(combine, app(app(zip, xs), ys)), yss) | |
| app(levels, app(app(node, x), xs)) | → | app(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs))) |
Termination of terms over the following signature is verified: zip, append, app, node, levels, combine, map, cons, nil