The TRS could not be proven terminating. The proof attempt took 60007 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (62ms), SubtermCriterion (1ms), DependencyGraph (39ms), PolynomialLinearRange4iUR (1389ms), DependencyGraph (28ms), PolynomialLinearRange8NegiUR (5447ms), DependencyGraph (48ms), ReductionPairSAT (timeout)].
| app#(sum, l) | → | app#(fold, add) | app#(sum, l) | → | app#(app(fold, add), l) | |
| app#(sum, l) | → | app#(app(app(fold, add), l), 0) | app#(app(app(fold, f), app(app(cons, h), t)), x) | → | app#(app(app(fold, f), t), app(app(f, x), h)) | |
| app#(app(app(fold, f), app(app(cons, h), t)), x) | → | app#(f, x) | app#(app(app(fold, f), app(app(cons, h), t)), x) | → | app#(fold, f) | |
| app#(app(app(fold, f), app(app(cons, h), t)), x) | → | app#(app(fold, f), t) | app#(app(app(fold, mul), l), 1) | → | app#(prod, l) | |
| app#(app(app(fold, f), app(app(cons, h), t)), x) | → | app#(app(f, x), h) |
| app(app(app(fold, f), nil), x) | → | x | app(app(app(fold, f), app(app(cons, h), t)), x) | → | app(app(app(fold, f), t), app(app(f, x), h)) | |
| app(sum, l) | → | app(app(app(fold, add), l), 0) | app(app(app(fold, mul), l), 1) | → | app(prod, l) |
Termination of terms over the following signature is verified: app, 1, 0, sum, mul, add, fold, prod, cons, nil