The TRS could not be proven terminating. The proof attempt took 1455 ms.
Problem 1 was processed with processor SubtermCriterion (0ms). | – Problem 2 remains open; application of the following processors failed [DependencyGraph (4ms), PolynomialLinearRange4iUR (102ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (195ms), DependencyGraph (3ms), ReductionPairSAT (913ms), DependencyGraph (2ms), SizeChangePrinciple (7ms)].
| f#(x, g(y), z) | → | f#(x, y, z) | f#(0, 1, x) | → | f#(g(x), g(x), x) | |
| f#(g(x), y, z) | → | f#(x, y, z) |
| f(0, 1, x) | → | f(g(x), g(x), x) | f(g(x), y, z) | → | g(f(x, y, z)) | |
| f(x, g(y), z) | → | g(f(x, y, z)) | f(x, y, g(z)) | → | g(f(x, y, z)) |
Termination of terms over the following signature is verified: f, g, 1, 0
| f#(x, y, g(z)) | → | f#(x, y, z) | f#(x, g(y), z) | → | f#(x, y, z) | |
| f#(0, 1, x) | → | f#(g(x), g(x), x) | f#(g(x), y, z) | → | f#(x, y, z) |
| f(0, 1, x) | → | f(g(x), g(x), x) | f(g(x), y, z) | → | g(f(x, y, z)) | |
| f(x, g(y), z) | → | g(f(x, y, z)) | f(x, y, g(z)) | → | g(f(x, y, z)) |
Termination of terms over the following signature is verified: f, g, 1, 0
The following projection was used:
Thus, the following dependency pairs are removed:
| f#(x, y, g(z)) | → | f#(x, y, z) |