The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (180ms), SubtermCriterion (0ms), DependencyGraph (143ms), PolynomialLinearRange4iUR (2843ms), DependencyGraph (137ms), PolynomialLinearRange8NegiUR (10202ms), DependencyGraph (130ms), ReductionPairSAT (timeout)].
| app#(app(flatwithsub, f), app(app(cons, x), xs)) | → | app#(flatwith, f) | app#(app(flatwithsub, f), app(app(cons, x), xs)) | → | app#(app(flatwith, f), x) | |
| app#(app(append, app(app(cons, x), xs)), ys) | → | app#(app(append, xs), ys) | app#(app(flatwith, f), app(node, xs)) | → | app#(app(flatwithsub, f), xs) | |
| app#(app(flatwithsub, f), app(app(cons, x), xs)) | → | app#(flatwithsub, f) | app#(app(flatwith, f), app(leaf, x)) | → | app#(f, x) | |
| app#(app(append, app(app(cons, x), xs)), ys) | → | app#(app(cons, x), app(app(append, xs), ys)) | app#(app(flatwith, f), app(leaf, x)) | → | app#(app(cons, app(f, x)), nil) | |
| app#(app(flatwith, f), app(leaf, x)) | → | app#(cons, app(f, x)) | app#(app(flatwith, f), app(node, xs)) | → | app#(flatwithsub, f) | |
| app#(app(flatwithsub, f), app(app(cons, x), xs)) | → | app#(app(flatwithsub, f), xs) | app#(app(append, app(app(cons, x), xs)), ys) | → | app#(append, xs) | |
| app#(app(flatwithsub, f), app(app(cons, x), xs)) | → | app#(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs)) | app#(app(flatwithsub, f), app(app(cons, x), xs)) | → | app#(append, app(app(flatwith, f), x)) | |
| app#(app(append, app(app(cons, x), xs)), ys) | → | app#(cons, x) |
| 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(flatwith, f), app(leaf, x)) | → | app(app(cons, app(f, x)), nil) | app(app(flatwith, f), app(node, xs)) | → | app(app(flatwithsub, f), xs) | |
| app(app(flatwithsub, f), nil) | → | nil | app(app(flatwithsub, f), app(app(cons, x), xs)) | → | app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs)) |
Termination of terms over the following signature is verified: append, app, node, flatwith, flatwithsub, leaf, cons, nil