The TRS could not be proven terminating. The proof attempt took 60031 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (128ms), SubtermCriterion (0ms), DependencyGraph (66ms), PolynomialLinearRange4iUR (1841ms), DependencyGraph (62ms), PolynomialLinearRange8NegiUR (4919ms), DependencyGraph (55ms), ReductionPairSAT (timeout)].
| app#(app(twice, f), x) | → | app#(f, x) | app#(app(map, f), app(app(cons, h), t)) | → | app#(f, h) | |
| app#(app(fmap, app(app(cons, f), t_f)), x) | → | app#(app(fmap, t_f), x) | app#(app(fmap, app(app(cons, f), t_f)), x) | → | app#(cons, app(f, x)) | |
| app#(app(fmap, app(app(cons, f), t_f)), x) | → | app#(f, x) | app#(app(fmap, app(app(cons, f), t_f)), x) | → | app#(app(cons, app(f, x)), app(app(fmap, t_f), x)) | |
| app#(app(twice, f), x) | → | app#(f, app(f, x)) | app#(app(map, f), app(app(cons, h), t)) | → | app#(cons, app(f, h)) | |
| 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#(map, f) | |
| app#(app(map, f), app(app(cons, h), t)) | → | app#(app(map, f), t) | app#(app(fmap, app(app(cons, f), t_f)), x) | → | app#(fmap, t_f) |
| app(app(twice, f), x) | → | app(f, app(f, x)) | 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(fmap, nil), x) | → | nil | |
| app(app(fmap, app(app(cons, f), t_f)), x) | → | app(app(cons, app(f, x)), app(app(fmap, t_f), x)) |
Termination of terms over the following signature is verified: app, twice, fmap, map, t_f, cons, nil