MAYBE
The TRS could not be proven terminating. The proof attempt took 5601 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (418ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (1183ms), DependencyGraph (2ms), ReductionPairSAT (3799ms), DependencyGraph (3ms), SizeChangePrinciple (21ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| b#(f(b(x, z)), y) | → | b#(z, b(y, z)) | | b#(f(b(x, z)), y) | → | b#(y, z) |
Rewrite Rules
| b(f(b(x, z)), y) | → | f(f(f(b(z, b(y, z))))) | | c(f(f(c(x, a, z))), a, y) | → | b(y, f(b(a, z))) |
| b(b(c(b(a, a), a, z), f(a)), y) | → | z |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| c#(f(f(c(x, a, z))), a, y) | → | b#(y, f(b(a, z))) | | c#(f(f(c(x, a, z))), a, y) | → | b#(a, z) |
| b#(f(b(x, z)), y) | → | b#(z, b(y, z)) | | b#(f(b(x, z)), y) | → | b#(y, z) |
Rewrite Rules
| b(f(b(x, z)), y) | → | f(f(f(b(z, b(y, z))))) | | c(f(f(c(x, a, z))), a, y) | → | b(y, f(b(a, z))) |
| b(b(c(b(a, a), a, z), f(a)), y) | → | z |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
The following SCCs where found
| b#(f(b(x, z)), y) → b#(z, b(y, z)) | b#(f(b(x, z)), y) → b#(y, z) |