MAYBE

The TRS could not be proven terminating. The proof attempt took 1061 ms.

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (17ms), SubtermCriterion (1ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (165ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (379ms), DependencyGraph (25ms), ReductionPairSAT (337ms), DependencyGraph (3ms), SizeChangePrinciple (11ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

f#(X, f(Y, Z)) → f#(Y, Y)f#(f(X, Y), Z) → f#(X, f(Y, Z))
f#(f(X, Y), Z) → f#(Y, Z)

Rewrite Rules

f(f(X, Y), Z) → f(X, f(Y, Z))f(X, f(Y, Z)) → f(Y, Y)

Original Signature

Termination of terms over the following signature is verified: f