TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60015 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (40ms).
| – Problem 2 was processed with processor ForwardNarrowing (1ms).
| | – Problem 5 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (3ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (2ms)].
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (319ms).
| | – Problem 4 was processed with processor PolynomialLinearRange4iUR (209ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| f#(c(x, y, z)) | → | f#(b(y, z)) |
Rewrite Rules
| c(c(z, y, a), a, a) | → | b(z, y) | | f(c(x, y, z)) | → | c(z, f(b(y, z)), a) |
| b(z, b(c(a, y, a), f(f(x)))) | → | c(c(y, a, z), z, x) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(c(x, y, z)) | → | c#(z, f(b(y, z)), a) | | c#(c(z, y, a), a, a) | → | b#(z, y) |
| b#(z, b(c(a, y, a), f(f(x)))) | → | c#(y, a, z) | | b#(z, b(c(a, y, a), f(f(x)))) | → | c#(c(y, a, z), z, x) |
| f#(c(x, y, z)) | → | f#(b(y, z)) | | f#(c(x, y, z)) | → | b#(y, z) |
Rewrite Rules
| c(c(z, y, a), a, a) | → | b(z, y) | | f(c(x, y, z)) | → | c(z, f(b(y, z)), a) |
| b(z, b(c(a, y, a), f(f(x)))) | → | c(c(y, a, z), z, x) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
The following SCCs where found
| f#(c(x, y, z)) → f#(b(y, z)) |
| b#(z, b(c(a, y, a), f(f(x)))) → c#(y, a, z) | c#(c(z, y, a), a, a) → b#(z, y) |
| b#(z, b(c(a, y, a), f(f(x)))) → c#(c(y, a, z), z, x) |
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(c(x, y, z)) | → | f#(b(y, z)) |
Rewrite Rules
| c(c(z, y, a), a, a) | → | b(z, y) | | f(c(x, y, z)) | → | c(z, f(b(y, z)), a) |
| b(z, b(c(a, y, a), f(f(x)))) | → | c(c(y, a, z), z, x) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
The right-hand side of the rule f
#(c(
x,
y,
z)) → f
#(b(
y,
z)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| f#(c(c(_x22, a, _x21), _x21, _x23)) | |
Thus, the rule f
#(c(
x,
y,
z)) → f
#(b(
y,
z)) is replaced by the following rules:
| f#(c(x, _x21, b(c(a, _x22, a), f(f(_x23))))) → f#(c(c(_x22, a, _x21), _x21, _x23)) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| b#(z, b(c(a, y, a), f(f(x)))) | → | c#(y, a, z) | | c#(c(z, y, a), a, a) | → | b#(z, y) |
| b#(z, b(c(a, y, a), f(f(x)))) | → | c#(c(y, a, z), z, x) |
Rewrite Rules
| c(c(z, y, a), a, a) | → | b(z, y) | | f(c(x, y, z)) | → | c(z, f(b(y, z)), a) |
| b(z, b(c(a, y, a), f(f(x)))) | → | c(c(y, a, z), z, x) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Polynomial Interpretation
- a: 2
- b(x,y): y + x
- b#(x,y): y + 1
- c(x,y,z): y + x
- c#(x,y,z): x + 1
- f(x): 0
Improved Usable rules
| b(z, b(c(a, y, a), f(f(x)))) | → | c(c(y, a, z), z, x) | | c(c(z, y, a), a, a) | → | b(z, y) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| b#(z, b(c(a, y, a), f(f(x)))) | → | c#(y, a, z) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| c#(c(z, y, a), a, a) | → | b#(z, y) | | b#(z, b(c(a, y, a), f(f(x)))) | → | c#(c(y, a, z), z, x) |
Rewrite Rules
| c(c(z, y, a), a, a) | → | b(z, y) | | f(c(x, y, z)) | → | c(z, f(b(y, z)), a) |
| b(z, b(c(a, y, a), f(f(x)))) | → | c(c(y, a, z), z, x) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Polynomial Interpretation
- a: 0
- b(x,y): y + 2x
- b#(x,y): y + x
- c(x,y,z): 2y + 2x
- c#(x,y,z): 2x + 1
- f(x): 2
Improved Usable rules
| b(z, b(c(a, y, a), f(f(x)))) | → | c(c(y, a, z), z, x) | | c(c(z, y, a), a, a) | → | b(z, y) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| c#(c(z, y, a), a, a) | → | b#(z, y) | | b#(z, b(c(a, y, a), f(f(x)))) | → | c#(c(y, a, z), z, x) |