The TRS could not be proven terminating. The proof attempt took 60000 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (1286ms), SubtermCriterion (1ms), DependencyGraph (1193ms), PolynomialLinearRange4iUR (9135ms), DependencyGraph (1096ms), PolynomialLinearRange8NegiUR (28848ms), DependencyGraph (1148ms), ReductionPairSAT (timeout)].
| app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(app(insert, f), g) | app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(insert, f) | |
| app#(app(app(sort, f), g), app(app(cons, h), t)) | → | app#(app(sort, f), g) | app#(descending_sort, l) | → | app#(app(sort, max), min) | |
| app#(ascending_sort, l) | → | app#(app(sort, min), max) | app#(app(max, app(s, x)), app(s, y)) | → | app#(app(max, x), y) | |
| app#(app(app(sort, f), g), app(app(cons, h), t)) | → | app#(sort, f) | app#(descending_sort, l) | → | app#(sort, max) | |
| app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(cons, app(app(f, x), h)) | app#(app(min, app(s, x)), app(s, y)) | → | app#(app(min, x), y) | |
| app#(app(app(sort, f), g), app(app(cons, h), t)) | → | app#(app(insert, f), g) | app#(app(max, app(s, x)), app(s, y)) | → | app#(max, x) | |
| app#(app(app(sort, f), g), app(app(cons, h), t)) | → | app#(app(app(sort, f), g), t) | app#(app(app(sort, f), g), app(app(cons, h), t)) | → | app#(app(app(insert, f), g), app(app(app(sort, f), g), t)) | |
| app#(app(min, app(s, x)), app(s, y)) | → | app#(min, x) | app#(app(app(sort, f), g), app(app(cons, h), t)) | → | app#(insert, f) | |
| app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(app(f, x), h) | app#(descending_sort, l) | → | app#(app(app(sort, max), min), l) | |
| app#(ascending_sort, l) | → | app#(sort, min) | app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(app(app(app(insert, f), g), t), app(app(g, x), h)) | |
| app#(app(app(app(insert, f), g), nil), x) | → | app#(app(cons, x), nil) | app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(g, x) | |
| app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(app(g, x), h) | app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(app(app(insert, f), g), t) | |
| app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(app(cons, app(app(f, x), h)), app(app(app(app(insert, f), g), t), app(app(g, x), h))) | app#(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app#(f, x) | |
| app#(app(app(app(insert, f), g), nil), x) | → | app#(cons, x) | app#(app(app(sort, f), g), app(app(cons, h), t)) | → | app#(app(app(app(insert, f), g), app(app(app(sort, f), g), t)), h) | |
| app#(ascending_sort, l) | → | app#(app(app(sort, min), max), l) |
| app(app(max, 0), x) | → | x | app(app(max, x), 0) | → | x | |
| app(app(max, app(s, x)), app(s, y)) | → | app(app(max, x), y) | app(app(min, 0), x) | → | 0 | |
| app(app(min, x), 0) | → | 0 | app(app(min, app(s, x)), app(s, y)) | → | app(app(min, x), y) | |
| app(app(app(app(insert, f), g), nil), x) | → | app(app(cons, x), nil) | app(app(app(app(insert, f), g), app(app(cons, h), t)), x) | → | app(app(cons, app(app(f, x), h)), app(app(app(app(insert, f), g), t), app(app(g, x), h))) | |
| app(app(app(sort, f), g), nil) | → | nil | app(app(app(sort, f), g), app(app(cons, h), t)) | → | app(app(app(app(insert, f), g), app(app(app(sort, f), g), t)), h) | |
| app(ascending_sort, l) | → | app(app(app(sort, min), max), l) | app(descending_sort, l) | → | app(app(app(sort, max), min), l) |
Termination of terms over the following signature is verified: min, app, ascending_sort, descending_sort, sort, max, 0, s, insert, nil, cons