TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60005 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (78ms).
| – Problem 2 was processed with processor PolynomialLinearRange8NegiUR (6261ms).
| | – Problem 3 was processed with processor PolynomialLinearRange8NegiUR (11221ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange8NegiUR (15488ms).
| | | | – Problem 5 was processed with processor PolynomialLinearRange8NegiUR (2299ms).
| | | | | – Problem 6 remains open; application of the following processors failed [DependencyGraph (1ms), PolynomialLinearRange8NegiUR (timeout)].
The following open problems remain:
Open Dependency Pair Problem 6
Dependency Pairs
| b#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) | | a#(0, b(0, x)) | → | b#(0, a(0, x)) |
Rewrite Rules
| a(0, b(0, x)) | → | b(0, a(0, x)) | | a(0, x) | → | b(0, b(0, x)) |
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, b, a
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| b#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) | | a#(0, b(0, x)) | → | b#(0, a(0, x)) |
| a#(0, a(1, a(x, y))) | → | a#(1, a(0, a(x, y))) | | b#(0, a(1, a(x, y))) | → | b#(1, a(0, a(x, y))) |
| a#(0, a(x, y)) | → | a#(x, y) | | a#(0, b(0, x)) | → | a#(0, x) |
| a#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) | | b#(0, a(1, a(x, y))) | → | a#(x, y) |
| a#(0, a(1, a(x, y))) | → | a#(x, y) | | a#(0, a(x, y)) | → | a#(1, a(1, a(x, y))) |
| a#(0, x) | → | b#(0, b(0, x)) | | a#(0, x) | → | b#(0, x) |
| a#(0, a(x, y)) | → | a#(1, a(x, y)) |
Rewrite Rules
| a(0, b(0, x)) | → | b(0, a(0, x)) | | a(0, x) | → | b(0, b(0, x)) |
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, b, a
Strategy
The following SCCs where found
| b#(0, a(1, a(x, y))) → a#(0, a(x, y)) | a#(0, b(0, x)) → b#(0, a(0, x)) |
| b#(0, a(1, a(x, y))) → a#(x, y) | a#(0, a(1, a(x, y))) → a#(x, y) |
| a#(0, x) → b#(0, b(0, x)) | a#(0, a(x, y)) → a#(x, y) |
| a#(0, x) → b#(0, x) | a#(0, a(1, a(x, y))) → a#(0, a(x, y)) |
| a#(0, b(0, x)) → a#(0, x) |
Problem 2: PolynomialLinearRange8NegiUR
Dependency Pair Problem
Dependency Pairs
| b#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) | | a#(0, b(0, x)) | → | b#(0, a(0, x)) |
| b#(0, a(1, a(x, y))) | → | a#(x, y) | | a#(0, a(1, a(x, y))) | → | a#(x, y) |
| a#(0, x) | → | b#(0, b(0, x)) | | a#(0, a(x, y)) | → | a#(x, y) |
| a#(0, x) | → | b#(0, x) | | a#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) |
| a#(0, b(0, x)) | → | a#(0, x) |
Rewrite Rules
| a(0, b(0, x)) | → | b(0, a(0, x)) | | a(0, x) | → | b(0, b(0, x)) |
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, b, a
Strategy
Polynomial Interpretation
- 0: 2
- 1: 1
- a(x,y): y + x
- a#(x,y): 2y + x - 2
- b(x,y): y + x - 1
- b#(x,y): 2y - 2
Improved Usable rules
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | a(0, b(0, x)) | → | b(0, a(0, x)) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) | | a(0, x) | → | b(0, b(0, x)) |
| b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a#(0, a(1, a(x, y))) | → | a#(x, y) | | a#(0, b(0, x)) | → | a#(0, x) |
| a#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) |
Problem 3: PolynomialLinearRange8NegiUR
Dependency Pair Problem
Dependency Pairs
| b#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) | | a#(0, b(0, x)) | → | b#(0, a(0, x)) |
| b#(0, a(1, a(x, y))) | → | a#(x, y) | | a#(0, a(x, y)) | → | a#(x, y) |
| a#(0, x) | → | b#(0, b(0, x)) | | a#(0, x) | → | b#(0, x) |
Rewrite Rules
| a(0, b(0, x)) | → | b(0, a(0, x)) | | a(0, x) | → | b(0, b(0, x)) |
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, b, a
Strategy
Polynomial Interpretation
- 0: 1
- 1: -2
- a(x,y): y + x + 1
- a#(x,y): y + x - 1
- b(x,y): y + 2x - 1
- b#(x,y): y - 1
Improved Usable rules
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | a(0, b(0, x)) | → | b(0, a(0, x)) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) | | a(0, x) | → | b(0, b(0, x)) |
| b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| b#(0, a(1, a(x, y))) | → | a#(x, y) | | a#(0, a(x, y)) | → | a#(x, y) |
Problem 4: PolynomialLinearRange8NegiUR
Dependency Pair Problem
Dependency Pairs
| b#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) | | a#(0, b(0, x)) | → | b#(0, a(0, x)) |
| a#(0, x) | → | b#(0, b(0, x)) | | a#(0, x) | → | b#(0, x) |
Rewrite Rules
| a(0, b(0, x)) | → | b(0, a(0, x)) | | a(0, x) | → | b(0, b(0, x)) |
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, b, a
Strategy
Polynomial Interpretation
- 0: 2
- 1: 1
- a(x,y): y + x
- a#(x,y): y + x - 1
- b(x,y): y + x - 1
- b#(x,y): y + x - 2
Improved Usable rules
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | a(0, b(0, x)) | → | b(0, a(0, x)) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) | | a(0, x) | → | b(0, b(0, x)) |
| b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 5: PolynomialLinearRange8NegiUR
Dependency Pair Problem
Dependency Pairs
| b#(0, a(1, a(x, y))) | → | a#(0, a(x, y)) | | a#(0, b(0, x)) | → | b#(0, a(0, x)) |
| a#(0, x) | → | b#(0, b(0, x)) |
Rewrite Rules
| a(0, b(0, x)) | → | b(0, a(0, x)) | | a(0, x) | → | b(0, b(0, x)) |
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, b, a
Strategy
Polynomial Interpretation
- 0: 2
- 1: -1
- a(x,y): 1
- a#(x,y): x
- b(x,y): -1
- b#(x,y): 2y + x - 2
Improved Usable rules
| a(0, a(1, a(x, y))) | → | a(1, a(0, a(x, y))) | | a(0, b(0, x)) | → | b(0, a(0, x)) |
| a(0, a(x, y)) | → | a(1, a(1, a(x, y))) | | a(0, x) | → | b(0, b(0, x)) |
| b(0, a(1, a(x, y))) | → | b(1, a(0, a(x, y))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a#(0, x) | → | b#(0, b(0, x)) |