The TRS could not be proven terminating. The proof attempt took 60000 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (333ms), SubtermCriterion (1ms), DependencyGraph (290ms), PolynomialLinearRange4iUR (4819ms), DependencyGraph (319ms), PolynomialLinearRange8NegiUR (17054ms), DependencyGraph (334ms), ReductionPairSAT (timeout)].
| app#(app(app(app(rec, t), u), v), app(s, x)) | → | app#(app(app(rec, t), u), v) | app#(app(app(app(rec, t), u), v), app(s, x)) | → | app#(app(app(app(rec, t), u), v), x) | |
| app#(app(app(app(rec, t), u), v), app(lim, f)) | → | app#(app(app(rectuv, t), u), v) | app#(app(app(app(rectuv, t), u), v), n) | → | app#(rec, t) | |
| app#(app(app(app(rectuv, t), u), v), n) | → | app#(app(rec, t), u) | app#(app(app(app(rec, t), u), v), app(lim, f)) | → | app#(rectuv, t) | |
| app#(app(app(app(rec, t), u), v), app(lim, f)) | → | app#(f, n) | app#(app(app(app(rectuv, t), u), v), n) | → | app#(app(app(rec, t), u), v) | |
| app#(app(app(app(rec, t), u), v), app(lim, f)) | → | app#(app(v, f), app(app(app(app(rectuv, t), u), v), app(f, n))) | app#(app(app(app(rec, t), u), v), app(s, x)) | → | app#(u, x) | |
| app#(app(app(app(rec, t), u), v), app(s, x)) | → | app#(rec, t) | app#(app(app(app(rec, t), u), v), app(lim, f)) | → | app#(app(rectuv, t), u) | |
| app#(app(app(app(rectuv, t), u), v), n) | → | app#(app(app(app(rec, t), u), v), n) | app#(app(app(app(rec, t), u), v), app(s, x)) | → | app#(app(u, x), app(app(app(app(rec, t), u), v), x)) | |
| app#(app(app(app(rec, t), u), v), app(lim, f)) | → | app#(v, f) | app#(app(app(app(rec, t), u), v), app(lim, f)) | → | app#(app(app(app(rectuv, t), u), v), app(f, n)) | |
| app#(app(app(app(rec, t), u), v), app(s, x)) | → | app#(app(rec, t), u) |
| app(app(app(app(rec, t), u), v), 0) | → | t | app(app(app(app(rec, t), u), v), app(s, x)) | → | app(app(u, x), app(app(app(app(rec, t), u), v), x)) | |
| app(app(app(app(rec, t), u), v), app(lim, f)) | → | app(app(v, f), app(app(app(app(rectuv, t), u), v), app(f, n))) | app(app(app(app(rectuv, t), u), v), n) | → | app(app(app(app(rec, t), u), v), n) |
Termination of terms over the following signature is verified: app, rec, 0, s, lim, n, rectuv