The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (320ms), SubtermCriterion (1ms), DependencyGraph (271ms), PolynomialLinearRange4iUR (4421ms), DependencyGraph (243ms), PolynomialLinearRange8NegiUR (12473ms), DependencyGraph (269ms), ReductionPairSAT (timeout)].
| app#(app(map, f), app(app(append, l1), l2)) | → | app#(app(map, f), l2) | app#(app(map, f), app(app(append, l1), l2)) | → | app#(app(append, app(app(map, f), l1)), app(app(map, f), l2)) | |
| app#(app(append, app(app(cons, h), t)), l) | → | app#(cons, h) | app#(app(map, f), app(app(append, l1), l2)) | → | app#(app(map, f), l1) | |
| app#(app(append, app(app(append, l1), l2)), l3) | → | app#(append, l1) | app#(app(append, app(app(append, l1), l2)), l3) | → | app#(app(append, l2), l3) | |
| app#(app(map, f), app(app(cons, h), t)) | → | app#(f, h) | app#(app(append, app(app(cons, h), t)), l) | → | app#(app(append, t), l) | |
| app#(app(map, f), app(app(append, l1), l2)) | → | app#(append, app(app(map, f), l1)) | app#(app(append, app(app(cons, h), t)), l) | → | app#(append, t) | |
| app#(app(append, app(app(cons, h), t)), l) | → | app#(app(cons, h), app(app(append, t), l)) | app#(app(append, app(app(append, l1), l2)), l3) | → | app#(app(append, l1), app(app(append, l2), l3)) | |
| app#(app(map, f), app(app(cons, h), t)) | → | app#(app(cons, app(f, h)), app(app(map, f), t)) | app#(app(map, f), app(app(cons, h), t)) | → | app#(cons, app(f, h)) | |
| app#(app(map, f), app(app(append, l1), l2)) | → | app#(map, f) | app#(app(map, f), app(app(cons, h), t)) | → | app#(app(map, f), t) | |
| app#(app(map, f), app(app(cons, h), t)) | → | app#(map, f) | app#(app(append, app(app(append, l1), l2)), l3) | → | app#(append, l2) |
| app(app(append, nil), l) | → | l | app(app(append, app(app(cons, h), t)), l) | → | app(app(cons, h), app(app(append, t), l)) | |
| app(app(map, f), nil) | → | nil | app(app(map, f), app(app(cons, h), t)) | → | app(app(cons, app(f, h)), app(app(map, f), t)) | |
| app(app(append, app(app(append, l1), l2)), l3) | → | app(app(append, l1), app(app(append, l2), l3)) | app(app(map, f), app(app(append, l1), l2)) | → | app(app(append, app(app(map, f), l1)), app(app(map, f), l2)) |
Termination of terms over the following signature is verified: append, app, map, cons, nil