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