The TRS could not be proven terminating. The proof attempt took 21372 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (11ms), SubtermCriterion (1ms), DependencyGraph (9ms), PolynomialLinearRange4iUR (183ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (296ms), DependencyGraph (1ms), ReductionPairSAT (20755ms), DependencyGraph (4ms), SizeChangePrinciple (18ms)].
f#(f(x, y, a), z, w) | → | f#(z, w, f(y, x, z)) | f#(f(x, y, a), z, w) | → | f#(y, x, z) |
f(f(x, y, a), z, w) | → | f(z, w, f(y, x, z)) |
Termination of terms over the following signature is verified: f, a