The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (1352ms), SubtermCriterion (1ms), DependencyGraph (1253ms), PolynomialLinearRange4iUR (9155ms), DependencyGraph (1204ms), PolynomialLinearRange8NegiUR (timeout), PolynomialLinearRange8NegiUR (-7ms), ReductionPairSAT (timeout)].
| app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(app(g, x), y) | app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(f, x) | |
| app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(insert, f) | app#(dsort, z) | → | app#(app(app(sort, max), min), z) | |
| app#(app(max, app(s, x)), app(s, y)) | → | app#(app(max, x), y) | app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(app(insert, f), g) | |
| app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(cons, app(app(f, x), y)) | app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(app(app(insert, f), g), z) | |
| app#(dsort, z) | → | app#(sort, max) | app#(app(app(sort, f), g), app(app(cons, x), y)) | → | app#(app(sort, f), g) | |
| app#(app(app(sort, f), g), app(app(cons, x), y)) | → | app#(sort, f) | app#(app(app(sort, f), g), app(app(cons, x), y)) | → | app#(app(insert, f), g) | |
| app#(app(min, app(s, x)), app(s, y)) | → | app#(app(min, x), y) | app#(asort, z) | → | app#(sort, min) | |
| app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(app(f, x), y) | app#(app(app(app(insert, f), g), nil), y) | → | app#(cons, y) | |
| app#(app(max, app(s, x)), app(s, y)) | → | app#(max, x) | app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(app(app(app(insert, f), g), z), app(app(g, x), y)) | |
| app#(app(app(app(insert, f), g), nil), y) | → | app#(app(cons, y), nil) | app#(app(min, app(s, x)), app(s, y)) | → | app#(min, x) | |
| app#(app(app(sort, f), g), app(app(cons, x), y)) | → | app#(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x) | app#(asort, z) | → | app#(app(app(sort, min), max), z) | |
| app#(dsort, z) | → | app#(app(sort, max), min) | app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(g, x) | |
| app#(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app#(app(cons, app(app(f, x), y)), app(app(app(app(insert, f), g), z), app(app(g, x), y))) | app#(app(app(sort, f), g), app(app(cons, x), y)) | → | app#(insert, f) | |
| app#(app(app(sort, f), g), app(app(cons, x), y)) | → | app#(app(app(sort, f), g), y) | app#(app(app(sort, f), g), app(app(cons, x), y)) | → | app#(app(app(insert, f), g), app(app(app(sort, f), g), y)) | |
| app#(asort, z) | → | app#(app(sort, min), max) |
| app(app(app(sort, f), g), nil) | → | nil | app(app(app(sort, f), g), app(app(cons, x), y)) | → | app(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x) | |
| app(app(app(app(insert, f), g), nil), y) | → | app(app(cons, y), nil) | app(app(app(app(insert, f), g), app(app(cons, x), z)), y) | → | app(app(cons, app(app(f, x), y)), app(app(app(app(insert, f), g), z), app(app(g, x), y))) | |
| app(app(max, 0), y) | → | y | app(app(max, x), 0) | → | x | |
| app(app(max, app(s, x)), app(s, y)) | → | app(app(max, x), y) | app(app(min, 0), y) | → | 0 | |
| app(app(min, x), 0) | → | 0 | app(app(min, app(s, x)), app(s, y)) | → | app(app(min, x), y) | |
| app(asort, z) | → | app(app(app(sort, min), max), z) | app(dsort, z) | → | app(app(app(sort, max), min), z) |
Termination of terms over the following signature is verified: min, app, max, 0, sort, s, dsort, insert, asort, cons, nil