The TRS could not be proven terminating. The proof attempt took 19109 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (68ms), SubtermCriterion (1ms), DependencyGraph (23ms), PolynomialLinearRange4iUR (916ms), DependencyGraph (16ms), PolynomialLinearRange8NegiUR (6447ms), DependencyGraph (14ms), ReductionPairSAT (11448ms), DependencyGraph (50ms), SizeChangePrinciple (24ms)].
| f#(y, f(x, f(a, x))) | → | f#(a, x) | f#(x, f(x, y)) | → | f#(x, a) | |
| f#(x, f(x, y)) | → | f#(f(x, a), a) | f#(y, f(x, f(a, x))) | → | f#(a, y) | |
| f#(y, f(x, f(a, x))) | → | f#(f(a, x), f(x, a)) | f#(y, f(x, f(a, x))) | → | f#(f(f(a, x), f(x, a)), f(a, y)) | |
| f#(x, f(x, y)) | → | f#(f(f(x, a), a), a) | f#(y, f(x, f(a, x))) | → | f#(x, a) |
| f(y, f(x, f(a, x))) | → | f(f(f(a, x), f(x, a)), f(a, y)) | f(x, f(x, y)) | → | f(f(f(x, a), a), a) |
Termination of terms over the following signature is verified: f, a