MAYBE
The TRS could not be proven terminating. The proof attempt took 3862 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 (4ms), PolynomialLinearRange4iUR (484ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (1704ms), DependencyGraph (2ms), ReductionPairSAT (1355ms), DependencyGraph (4ms), SizeChangePrinciple (161ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| b#(b(y, z), c(a, a, a)) | → | c#(z, y, z) | | c#(y, x, f(z)) | → | b#(z, x) |
| c#(y, x, f(z)) | → | b#(f(b(z, x)), z) |
Rewrite Rules
| b(b(y, z), c(a, a, a)) | → | f(c(z, y, z)) | | f(b(b(a, z), c(a, x, y))) | → | z |
| c(y, x, f(z)) | → | b(f(b(z, x)), z) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| b#(b(y, z), c(a, a, a)) | → | c#(z, y, z) | | b#(b(y, z), c(a, a, a)) | → | f#(c(z, y, z)) |
| c#(y, x, f(z)) | → | b#(z, x) | | c#(y, x, f(z)) | → | b#(f(b(z, x)), z) |
| c#(y, x, f(z)) | → | f#(b(z, x)) |
Rewrite Rules
| b(b(y, z), c(a, a, a)) | → | f(c(z, y, z)) | | f(b(b(a, z), c(a, x, y))) | → | z |
| c(y, x, f(z)) | → | b(f(b(z, x)), z) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
The following SCCs where found
| b#(b(y, z), c(a, a, a)) → c#(z, y, z) | c#(y, x, f(z)) → b#(z, x) |
| c#(y, x, f(z)) → b#(f(b(z, x)), z) |