TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60019 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (46ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (2012ms).
| | – Problem 3 was processed with processor PolynomialLinearRange4iUR (1763ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange8NegiUR (22398ms).
| | | | – Problem 5 remains open; application of the following processors failed [DependencyGraph (0ms), PolynomialLinearRange8NegiUR (11222ms), DependencyGraph (2ms), ReductionPairSAT (20607ms)].
The following open problems remain:
Open Dependency Pair Problem 5
Dependency Pairs
| f#(b(b(x, f(y)), z)) | → | f#(b(b(f(a), y), y)) |
Rewrite Rules
| f(c(c(a, y, a), b(x, z), a)) | → | b(y, f(c(f(a), z, z))) | | f(b(b(x, f(y)), z)) | → | c(z, x, f(b(b(f(a), y), y))) |
| c(b(a, a), b(y, z), x) | → | b(a, b(z, z)) |
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(c(a, y, a), b(x, z), a)) | → | f#(c(f(a), z, z)) | | f#(b(b(x, f(y)), z)) | → | f#(a) |
| f#(b(b(x, f(y)), z)) | → | f#(b(b(f(a), y), y)) | | f#(b(b(x, f(y)), z)) | → | c#(z, x, f(b(b(f(a), y), y))) |
| f#(c(c(a, y, a), b(x, z), a)) | → | c#(f(a), z, z) | | f#(c(c(a, y, a), b(x, z), a)) | → | f#(a) |
Rewrite Rules
| f(c(c(a, y, a), b(x, z), a)) | → | b(y, f(c(f(a), z, z))) | | f(b(b(x, f(y)), z)) | → | c(z, x, f(b(b(f(a), y), y))) |
| c(b(a, a), b(y, z), x) | → | b(a, b(z, z)) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
The following SCCs where found
| f#(c(c(a, y, a), b(x, z), a)) → f#(c(f(a), z, z)) | f#(b(b(x, f(y)), z)) → f#(a) |
| f#(b(b(x, f(y)), z)) → f#(b(b(f(a), y), y)) | f#(c(c(a, y, a), b(x, z), a)) → f#(a) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(c(c(a, y, a), b(x, z), a)) | → | f#(c(f(a), z, z)) | | f#(b(b(x, f(y)), z)) | → | f#(a) |
| f#(b(b(x, f(y)), z)) | → | f#(b(b(f(a), y), y)) | | f#(c(c(a, y, a), b(x, z), a)) | → | f#(a) |
Rewrite Rules
| f(c(c(a, y, a), b(x, z), a)) | → | b(y, f(c(f(a), z, z))) | | f(b(b(x, f(y)), z)) | → | c(z, x, f(b(b(f(a), y), y))) |
| c(b(a, a), b(y, z), x) | → | b(a, b(z, z)) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Polynomial Interpretation
- a: 0
- b(x,y): 0
- c(x,y,z): 1
- f(x): x
- f#(x): 2x
Improved Usable rules
| c(b(a, a), b(y, z), x) | → | b(a, b(z, z)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(c(c(a, y, a), b(x, z), a)) | → | f#(a) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(c(c(a, y, a), b(x, z), a)) | → | f#(c(f(a), z, z)) | | f#(b(b(x, f(y)), z)) | → | f#(a) |
| f#(b(b(x, f(y)), z)) | → | f#(b(b(f(a), y), y)) |
Rewrite Rules
| f(c(c(a, y, a), b(x, z), a)) | → | b(y, f(c(f(a), z, z))) | | f(b(b(x, f(y)), z)) | → | c(z, x, f(b(b(f(a), y), y))) |
| c(b(a, a), b(y, z), x) | → | b(a, b(z, z)) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Polynomial Interpretation
- a: 0
- b(x,y): 1
- c(x,y,z): 1
- f(x): 1
- f#(x): x
Improved Usable rules
| c(b(a, a), b(y, z), x) | → | b(a, b(z, z)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(b(b(x, f(y)), z)) | → | f#(a) |
Problem 4: PolynomialLinearRange8NegiUR
Dependency Pair Problem
Dependency Pairs
| f#(c(c(a, y, a), b(x, z), a)) | → | f#(c(f(a), z, z)) | | f#(b(b(x, f(y)), z)) | → | f#(b(b(f(a), y), y)) |
Rewrite Rules
| f(c(c(a, y, a), b(x, z), a)) | → | b(y, f(c(f(a), z, z))) | | f(b(b(x, f(y)), z)) | → | c(z, x, f(b(b(f(a), y), y))) |
| c(b(a, a), b(y, z), x) | → | b(a, b(z, z)) |
Original Signature
Termination of terms over the following signature is verified: f, b, c, a
Strategy
Polynomial Interpretation
- a: 0
- b(x,y): y + x + 1
- c(x,y,z): 2y + 2x
- f(x): 2x
- f#(x): 2x - 1
Improved Usable rules
| c(b(a, a), b(y, z), x) | → | b(a, b(z, z)) | | f(b(b(x, f(y)), z)) | → | c(z, x, f(b(b(f(a), y), y))) |
| f(c(c(a, y, a), b(x, z), a)) | → | b(y, f(c(f(a), z, z))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(c(c(a, y, a), b(x, z), a)) | → | f#(c(f(a), z, z)) |