The TRS could not be proven terminating. The proof attempt took 9890 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (40ms), SubtermCriterion (1ms), DependencyGraph (23ms), PolynomialLinearRange4iUR (706ms), DependencyGraph (13ms), PolynomialLinearRange8NegiUR (2215ms), DependencyGraph (10ms), ReductionPairSAT (6708ms), DependencyGraph (10ms), SizeChangePrinciple (31ms)].
| f#(f(s(x), s(y)), f(z, w)) | → | f#(x, y) | f#(f(s(x), s(y)), f(z, w)) | → | f#(f(x, y), f(z, w)) | |
| f#(f(s(x), 0), f(y, z)) | → | f#(f(y, z), f(y, s(z))) | f#(f(s(x), s(y)), f(z, w)) | → | f#(z, w) | |
| f#(f(s(x), 0), f(y, z)) | → | f#(y, z) | f#(f(s(x), 0), f(y, z)) | → | f#(y, s(z)) |
| f(f(s(x), 0), f(y, z)) | → | f(f(y, z), f(y, s(z))) | f(f(s(x), s(y)), f(z, w)) | → | f(f(x, y), f(z, w)) |
Termination of terms over the following signature is verified: f, 0, s