TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60288 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (177ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (72ms), PolynomialLinearRange4iUR (timeout), PolynomialLinearRange4iUR (-1ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (70ms), ReductionPairSAT (10937ms), DependencyGraph (57ms), SizeChangePrinciple (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| activate#(n__div(X1, X2)) | → | activate#(X1) | | activate#(n__div(X1, X2)) | → | div#(activate(X1), X2) |
| activate#(n__s(X)) | → | activate#(X) | | activate#(n__minus(X1, X2)) | → | minus#(X1, X2) |
| minus#(n__s(X), n__s(Y)) | → | minus#(activate(X), activate(Y)) | | minus#(n__s(X), n__s(Y)) | → | activate#(Y) |
| geq#(n__s(X), n__s(Y)) | → | activate#(X) | | div#(s(X), n__s(Y)) | → | activate#(Y) |
| geq#(n__s(X), n__s(Y)) | → | geq#(activate(X), activate(Y)) | | if#(true, X, Y) | → | activate#(X) |
| if#(false, X, Y) | → | activate#(Y) | | div#(s(X), n__s(Y)) | → | if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0) |
| div#(s(X), n__s(Y)) | → | geq#(X, activate(Y)) | | geq#(n__s(X), n__s(Y)) | → | activate#(Y) |
| minus#(n__s(X), n__s(Y)) | → | activate#(X) |
Rewrite Rules
| minus(n__0, Y) | → | 0 | | minus(n__s(X), n__s(Y)) | → | minus(activate(X), activate(Y)) |
| geq(X, n__0) | → | true | | geq(n__0, n__s(Y)) | → | false |
| geq(n__s(X), n__s(Y)) | → | geq(activate(X), activate(Y)) | | div(0, n__s(Y)) | → | 0 |
| div(s(X), n__s(Y)) | → | if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | 0 | → | n__0 |
| s(X) | → | n__s(X) | | div(X1, X2) | → | n__div(X1, X2) |
| minus(X1, X2) | → | n__minus(X1, X2) | | activate(n__0) | → | 0 |
| activate(n__s(X)) | → | s(activate(X)) | | activate(n__div(X1, X2)) | → | div(activate(X1), X2) |
| activate(n__minus(X1, X2)) | → | minus(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: geq, minus, div, true, n__div, activate, n__s, 0, n__0, n__minus, s, if, false
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__div(X1, X2)) | → | activate#(X1) | | activate#(n__div(X1, X2)) | → | div#(activate(X1), X2) |
| activate#(n__s(X)) | → | activate#(X) | | activate#(n__minus(X1, X2)) | → | minus#(X1, X2) |
| minus#(n__s(X), n__s(Y)) | → | minus#(activate(X), activate(Y)) | | minus#(n__s(X), n__s(Y)) | → | activate#(Y) |
| geq#(n__s(X), n__s(Y)) | → | activate#(X) | | div#(s(X), n__s(Y)) | → | activate#(Y) |
| minus#(n__0, Y) | → | 0# | | geq#(n__s(X), n__s(Y)) | → | geq#(activate(X), activate(Y)) |
| if#(true, X, Y) | → | activate#(X) | | if#(false, X, Y) | → | activate#(Y) |
| div#(0, n__s(Y)) | → | 0# | | activate#(n__0) | → | 0# |
| activate#(n__s(X)) | → | s#(activate(X)) | | div#(s(X), n__s(Y)) | → | if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0) |
| div#(s(X), n__s(Y)) | → | geq#(X, activate(Y)) | | geq#(n__s(X), n__s(Y)) | → | activate#(Y) |
| minus#(n__s(X), n__s(Y)) | → | activate#(X) |
Rewrite Rules
| minus(n__0, Y) | → | 0 | | minus(n__s(X), n__s(Y)) | → | minus(activate(X), activate(Y)) |
| geq(X, n__0) | → | true | | geq(n__0, n__s(Y)) | → | false |
| geq(n__s(X), n__s(Y)) | → | geq(activate(X), activate(Y)) | | div(0, n__s(Y)) | → | 0 |
| div(s(X), n__s(Y)) | → | if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0) | | if(true, X, Y) | → | activate(X) |
| if(false, X, Y) | → | activate(Y) | | 0 | → | n__0 |
| s(X) | → | n__s(X) | | div(X1, X2) | → | n__div(X1, X2) |
| minus(X1, X2) | → | n__minus(X1, X2) | | activate(n__0) | → | 0 |
| activate(n__s(X)) | → | s(activate(X)) | | activate(n__div(X1, X2)) | → | div(activate(X1), X2) |
| activate(n__minus(X1, X2)) | → | minus(X1, X2) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: geq, minus, div, true, n__div, activate, n__s, 0, n__0, n__minus, s, if, false
Strategy
The following SCCs where found
| activate#(n__div(X1, X2)) → activate#(X1) | activate#(n__div(X1, X2)) → div#(activate(X1), X2) |
| activate#(n__s(X)) → activate#(X) | activate#(n__minus(X1, X2)) → minus#(X1, X2) |
| minus#(n__s(X), n__s(Y)) → minus#(activate(X), activate(Y)) | geq#(n__s(X), n__s(Y)) → activate#(X) |
| minus#(n__s(X), n__s(Y)) → activate#(Y) | div#(s(X), n__s(Y)) → activate#(Y) |
| geq#(n__s(X), n__s(Y)) → geq#(activate(X), activate(Y)) | if#(false, X, Y) → activate#(Y) |
| if#(true, X, Y) → activate#(X) | div#(s(X), n__s(Y)) → if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0) |
| minus#(n__s(X), n__s(Y)) → activate#(X) | geq#(n__s(X), n__s(Y)) → activate#(Y) |
| div#(s(X), n__s(Y)) → geq#(X, activate(Y)) |