TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (118ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (1036ms).
| | – Problem 4 was processed with processor PolynomialLinearRange4iUR (997ms).
| | | – Problem 5 remains open; application of the following processors failed [DependencyGraph (8ms), PolynomialLinearRange4iUR (1661ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (10ms), ReductionPairSAT (340ms), DependencyGraph (6ms), SizeChangePrinciple (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 5
Dependency Pairs
| activate#(n__s(X)) | → | activate#(X) | | if#(true, X, Y) | → | activate#(X) |
| if#(false, X, Y) | → | activate#(Y) | | diff#(X, Y) | → | if#(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| activate#(n__diff(X1, X2)) | → | diff#(activate(X1), activate(X2)) |
Rewrite Rules
| p(0) | → | 0 | | p(s(X)) | → | X |
| leq(0, Y) | → | true | | leq(s(X), 0) | → | false |
| leq(s(X), s(Y)) | → | leq(X, Y) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| 0 | → | n__0 | | s(X) | → | n__s(X) |
| diff(X1, X2) | → | n__diff(X1, X2) | | p(X) | → | n__p(X) |
| activate(n__0) | → | 0 | | activate(n__s(X)) | → | s(activate(X)) |
| activate(n__diff(X1, X2)) | → | diff(activate(X1), activate(X2)) | | activate(n__p(X)) | → | p(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: diff, leq, true, activate, n__s, 0, n__0, s, if, p, n__p, n__diff, false
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| leq#(s(X), s(Y)) | → | leq#(X, Y) | | activate#(n__s(X)) | → | activate#(X) |
| p#(0) | → | 0# | | activate#(n__diff(X1, X2)) | → | diff#(activate(X1), activate(X2)) |
| activate#(n__diff(X1, X2)) | → | activate#(X2) | | activate#(n__p(X)) | → | p#(activate(X)) |
| activate#(n__diff(X1, X2)) | → | activate#(X1) | | if#(true, X, Y) | → | activate#(X) |
| if#(false, X, Y) | → | activate#(Y) | | diff#(X, Y) | → | if#(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| activate#(n__p(X)) | → | activate#(X) | | activate#(n__0) | → | 0# |
| activate#(n__s(X)) | → | s#(activate(X)) | | diff#(X, Y) | → | leq#(X, Y) |
Rewrite Rules
| p(0) | → | 0 | | p(s(X)) | → | X |
| leq(0, Y) | → | true | | leq(s(X), 0) | → | false |
| leq(s(X), s(Y)) | → | leq(X, Y) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| 0 | → | n__0 | | s(X) | → | n__s(X) |
| diff(X1, X2) | → | n__diff(X1, X2) | | p(X) | → | n__p(X) |
| activate(n__0) | → | 0 | | activate(n__s(X)) | → | s(activate(X)) |
| activate(n__diff(X1, X2)) | → | diff(activate(X1), activate(X2)) | | activate(n__p(X)) | → | p(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: diff, leq, true, activate, n__s, 0, n__0, s, if, p, n__p, n__diff, false
Strategy
The following SCCs where found
| activate#(n__diff(X1, X2)) → activate#(X1) | if#(false, X, Y) → activate#(Y) |
| if#(true, X, Y) → activate#(X) | activate#(n__s(X)) → activate#(X) |
| diff#(X, Y) → if#(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) | activate#(n__p(X)) → activate#(X) |
| activate#(n__diff(X1, X2)) → diff#(activate(X1), activate(X2)) | activate#(n__diff(X1, X2)) → activate#(X2) |
| leq#(s(X), s(Y)) → leq#(X, Y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__diff(X1, X2)) | → | activate#(X1) | | if#(false, X, Y) | → | activate#(Y) |
| if#(true, X, Y) | → | activate#(X) | | activate#(n__s(X)) | → | activate#(X) |
| diff#(X, Y) | → | if#(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) | | activate#(n__p(X)) | → | activate#(X) |
| activate#(n__diff(X1, X2)) | → | diff#(activate(X1), activate(X2)) | | activate#(n__diff(X1, X2)) | → | activate#(X2) |
Rewrite Rules
| p(0) | → | 0 | | p(s(X)) | → | X |
| leq(0, Y) | → | true | | leq(s(X), 0) | → | false |
| leq(s(X), s(Y)) | → | leq(X, Y) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| 0 | → | n__0 | | s(X) | → | n__s(X) |
| diff(X1, X2) | → | n__diff(X1, X2) | | p(X) | → | n__p(X) |
| activate(n__0) | → | 0 | | activate(n__s(X)) | → | s(activate(X)) |
| activate(n__diff(X1, X2)) | → | diff(activate(X1), activate(X2)) | | activate(n__p(X)) | → | p(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: diff, leq, true, activate, n__s, 0, n__0, s, if, p, n__p, n__diff, false
Strategy
Polynomial Interpretation
- 0: 0
- activate(x): x
- activate#(x): 2x
- diff(x,y): y + x + 1
- diff#(x,y): 2y + 2x + 2
- false: 0
- if(x,y,z): z + y
- if#(x,y,z): 2z + 3y
- leq(x,y): 0
- n__0: 0
- n__diff(x,y): y + x + 1
- n__p(x): x
- n__s(x): x
- p(x): x
- s(x): x
- true: 0
Improved Usable rules
| if(false, X, Y) | → | activate(Y) | | diff(X1, X2) | → | n__diff(X1, X2) |
| p(0) | → | 0 | | activate(n__0) | → | 0 |
| 0 | → | n__0 | | p(s(X)) | → | X |
| s(X) | → | n__s(X) | | if(true, X, Y) | → | activate(X) |
| activate(X) | → | X | | activate(n__diff(X1, X2)) | → | diff(activate(X1), activate(X2)) |
| p(X) | → | n__p(X) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| activate(n__p(X)) | → | p(activate(X)) | | activate(n__s(X)) | → | s(activate(X)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| activate#(n__diff(X1, X2)) | → | activate#(X1) | | activate#(n__diff(X1, X2)) | → | activate#(X2) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| activate#(n__s(X)) | → | activate#(X) | | if#(true, X, Y) | → | activate#(X) |
| if#(false, X, Y) | → | activate#(Y) | | diff#(X, Y) | → | if#(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| activate#(n__p(X)) | → | activate#(X) | | activate#(n__diff(X1, X2)) | → | diff#(activate(X1), activate(X2)) |
Rewrite Rules
| p(0) | → | 0 | | p(s(X)) | → | X |
| leq(0, Y) | → | true | | leq(s(X), 0) | → | false |
| leq(s(X), s(Y)) | → | leq(X, Y) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| 0 | → | n__0 | | s(X) | → | n__s(X) |
| diff(X1, X2) | → | n__diff(X1, X2) | | p(X) | → | n__p(X) |
| activate(n__0) | → | 0 | | activate(n__s(X)) | → | s(activate(X)) |
| activate(n__diff(X1, X2)) | → | diff(activate(X1), activate(X2)) | | activate(n__p(X)) | → | p(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: diff, leq, true, activate, n__s, 0, n__0, s, if, p, n__p, n__diff, false
Strategy
Polynomial Interpretation
- 0: 2
- activate(x): 0
- activate#(x): 2x
- diff(x,y): y + 2x + 2
- diff#(x,y): 0
- false: 0
- if(x,y,z): 2z + 3y
- if#(x,y,z): 2z + 2y
- leq(x,y): y + x
- n__0: 0
- n__diff(x,y): 0
- n__p(x): x + 1
- n__s(x): x
- p(x): 0
- s(x): 1
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| activate#(n__p(X)) | → | activate#(X) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| leq#(s(X), s(Y)) | → | leq#(X, Y) |
Rewrite Rules
| p(0) | → | 0 | | p(s(X)) | → | X |
| leq(0, Y) | → | true | | leq(s(X), 0) | → | false |
| leq(s(X), s(Y)) | → | leq(X, Y) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | diff(X, Y) | → | if(leq(X, Y), n__0, n__s(n__diff(n__p(X), Y))) |
| 0 | → | n__0 | | s(X) | → | n__s(X) |
| diff(X1, X2) | → | n__diff(X1, X2) | | p(X) | → | n__p(X) |
| activate(n__0) | → | 0 | | activate(n__s(X)) | → | s(activate(X)) |
| activate(n__diff(X1, X2)) | → | diff(activate(X1), activate(X2)) | | activate(n__p(X)) | → | p(activate(X)) |
| activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: diff, leq, true, activate, n__s, 0, n__0, s, if, p, n__p, n__diff, false
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| leq#(s(X), s(Y)) | → | leq#(X, Y) |