The TRS could not be proven terminating. The proof attempt took 12625 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (45ms), SubtermCriterion (0ms), DependencyGraph (19ms), PolynomialLinearRange4iUR (770ms), DependencyGraph (14ms), PolynomialLinearRange8NegiUR (4324ms), DependencyGraph (10ms), ReductionPairSAT (7306ms), DependencyGraph (11ms), SizeChangePrinciple (18ms)].
| f#(y, f(x, f(a, x))) | → | f#(a, f(x, a)) | f#(y, f(x, f(a, x))) | → | f#(f(a, f(x, a)), f(a, y)) | |
| 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#(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(a, 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