TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60045 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (293ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (437ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (243ms).
| | – Problem 6 was processed with processor PolynomialLinearRange4iUR (153ms).
| | | – Problem 7 was processed with processor DependencyGraph (2ms).
| | | | – Problem 8 was processed with processor PolynomialLinearRange4iUR (15ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (2120ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (2051ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (1771ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (1763ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (0ms), ReductionPairSAT (21028ms), DependencyGraph (0ms)].
The following open problems remain:
Open Dependency Pair Problem 5
Dependency Pairs
| tp#(mark(x)) | → | tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Rewrite Rules
| active(f(x)) | → | mark(f(f(x))) | | chk(no(f(x))) | → | f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | chk(no(c)) | → | active(c) |
| mat(f(x), c) | → | no(c) | | f(active(x)) | → | active(f(x)) |
| f(no(x)) | → | no(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| tp(mark(x)) | → | tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Original Signature
Termination of terms over the following signature is verified: f, chk, c, no, tp, mat, active, mark, X, y
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(no(x)) | → | f#(x) | | tp#(mark(x)) | → | f#(f(f(f(f(f(f(f(f(f(X)))))))))) |
| chk#(no(f(x))) | → | mat#(f(f(f(f(f(f(f(f(f(f(X)))))))))), x) | | mat#(f(x), f(y)) | → | f#(mat(x, y)) |
| tp#(mark(x)) | → | f#(f(f(f(f(f(f(f(f(X))))))))) | | tp#(mark(x)) | → | f#(X) |
| tp#(mark(x)) | → | f#(f(f(f(f(f(f(X))))))) | | tp#(mark(x)) | → | f#(f(f(f(f(X))))) |
| chk#(no(f(x))) | → | f#(f(f(f(X)))) | | chk#(no(f(x))) | → | chk#(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)) |
| chk#(no(f(x))) | → | f#(f(X)) | | tp#(mark(x)) | → | f#(f(f(f(f(f(X)))))) |
| tp#(mark(x)) | → | f#(f(f(f(X)))) | | chk#(no(f(x))) | → | f#(f(f(f(f(X))))) |
| chk#(no(f(x))) | → | f#(f(f(X))) | | chk#(no(f(x))) | → | f#(f(f(f(f(f(f(X))))))) |
| active#(f(x)) | → | f#(f(x)) | | f#(mark(x)) | → | f#(x) |
| tp#(mark(x)) | → | tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) | | tp#(mark(x)) | → | mat#(f(f(f(f(f(f(f(f(f(f(X)))))))))), x) |
| chk#(no(f(x))) | → | f#(f(f(f(f(f(f(f(f(X))))))))) | | chk#(no(f(x))) | → | f#(X) |
| active#(f(x)) | → | f#(x) | | f#(active(x)) | → | f#(x) |
| chk#(no(f(x))) | → | f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) | | tp#(mark(x)) | → | f#(f(f(X))) |
| tp#(mark(x)) | → | f#(f(X)) | | chk#(no(c)) | → | active#(c) |
| tp#(mark(x)) | → | chk#(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)) | | tp#(mark(x)) | → | f#(f(f(f(f(f(f(f(X)))))))) |
| f#(active(x)) | → | active#(f(x)) | | chk#(no(f(x))) | → | f#(f(f(f(f(f(f(f(f(f(X)))))))))) |
| chk#(no(f(x))) | → | f#(f(f(f(f(f(f(f(X)))))))) | | mat#(f(x), f(y)) | → | mat#(x, y) |
| chk#(no(f(x))) | → | f#(f(f(f(f(f(X)))))) |
Rewrite Rules
| active(f(x)) | → | mark(f(f(x))) | | chk(no(f(x))) | → | f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | chk(no(c)) | → | active(c) |
| mat(f(x), c) | → | no(c) | | f(active(x)) | → | active(f(x)) |
| f(no(x)) | → | no(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| tp(mark(x)) | → | tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Original Signature
Termination of terms over the following signature is verified: f, chk, c, no, mat, tp, active, mark, X, y
Strategy
The following SCCs where found
| tp#(mark(x)) → tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| chk#(no(f(x))) → chk#(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)) |
| f#(mark(x)) → f#(x) | active#(f(x)) → f#(f(x)) |
| f#(no(x)) → f#(x) | f#(active(x)) → f#(x) |
| active#(f(x)) → f#(x) | f#(active(x)) → active#(f(x)) |
| mat#(f(x), f(y)) → mat#(x, y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| chk#(no(f(x))) | → | chk#(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)) |
Rewrite Rules
| active(f(x)) | → | mark(f(f(x))) | | chk(no(f(x))) | → | f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | chk(no(c)) | → | active(c) |
| mat(f(x), c) | → | no(c) | | f(active(x)) | → | active(f(x)) |
| f(no(x)) | → | no(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| tp(mark(x)) | → | tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Original Signature
Termination of terms over the following signature is verified: f, chk, c, no, mat, tp, active, mark, X, y
Strategy
Polynomial Interpretation
- X: 0
- active(x): 1
- c: 1
- chk(x): 0
- chk#(x): 2x
- f(x): 2x
- mark(x): 1
- mat(x,y): 2y
- no(x): x + 1
- tp(x): 0
- y: 0
Improved Usable rules
| f(active(x)) | → | active(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| active(f(x)) | → | mark(f(f(x))) | | mat(f(x), c) | → | no(c) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | f(no(x)) | → | no(f(x)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| chk#(no(f(x))) | → | chk#(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(mark(x)) | → | f#(x) | | active#(f(x)) | → | f#(f(x)) |
| f#(no(x)) | → | f#(x) | | f#(active(x)) | → | f#(x) |
| active#(f(x)) | → | f#(x) | | f#(active(x)) | → | active#(f(x)) |
Rewrite Rules
| active(f(x)) | → | mark(f(f(x))) | | chk(no(f(x))) | → | f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | chk(no(c)) | → | active(c) |
| mat(f(x), c) | → | no(c) | | f(active(x)) | → | active(f(x)) |
| f(no(x)) | → | no(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| tp(mark(x)) | → | tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Original Signature
Termination of terms over the following signature is verified: f, chk, c, no, mat, tp, active, mark, X, y
Strategy
Polynomial Interpretation
- X: 0
- active(x): 3x
- active#(x): 3x
- c: 0
- chk(x): 0
- f(x): 3x
- f#(x): 3x
- mark(x): x
- mat(x,y): 0
- no(x): 3x + 1
- tp(x): 0
- y: 0
Improved Usable rules
| f(active(x)) | → | active(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| active(f(x)) | → | mark(f(f(x))) | | f(no(x)) | → | no(f(x)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 6: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| active#(f(x)) | → | f#(f(x)) | | f#(mark(x)) | → | f#(x) |
| active#(f(x)) | → | f#(x) | | f#(active(x)) | → | f#(x) |
| f#(active(x)) | → | active#(f(x)) |
Rewrite Rules
| active(f(x)) | → | mark(f(f(x))) | | chk(no(f(x))) | → | f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | chk(no(c)) | → | active(c) |
| mat(f(x), c) | → | no(c) | | f(active(x)) | → | active(f(x)) |
| f(no(x)) | → | no(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| tp(mark(x)) | → | tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Original Signature
Termination of terms over the following signature is verified: f, chk, c, no, tp, mat, active, mark, X, y
Strategy
Polynomial Interpretation
- X: 0
- active(x): 3x + 1
- active#(x): 3x
- c: 0
- chk(x): 0
- f(x): 3x
- f#(x): 3x
- mark(x): x
- mat(x,y): 0
- no(x): x
- tp(x): 0
- y: 0
Improved Usable rules
| f(active(x)) | → | active(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| active(f(x)) | → | mark(f(f(x))) | | f(no(x)) | → | no(f(x)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(active(x)) | → | f#(x) | | f#(active(x)) | → | active#(f(x)) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(mark(x)) | → | f#(x) | | active#(f(x)) | → | f#(f(x)) |
| active#(f(x)) | → | f#(x) |
Rewrite Rules
| active(f(x)) | → | mark(f(f(x))) | | chk(no(f(x))) | → | f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | chk(no(c)) | → | active(c) |
| mat(f(x), c) | → | no(c) | | f(active(x)) | → | active(f(x)) |
| f(no(x)) | → | no(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| tp(mark(x)) | → | tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Original Signature
Termination of terms over the following signature is verified: f, chk, c, no, mat, tp, active, mark, X, y
Strategy
The following SCCs where found
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| active(f(x)) | → | mark(f(f(x))) | | chk(no(f(x))) | → | f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | chk(no(c)) | → | active(c) |
| mat(f(x), c) | → | no(c) | | f(active(x)) | → | active(f(x)) |
| f(no(x)) | → | no(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| tp(mark(x)) | → | tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Original Signature
Termination of terms over the following signature is verified: f, chk, c, no, mat, tp, active, mark, X, y
Strategy
Polynomial Interpretation
- X: 0
- active(x): 0
- c: 0
- chk(x): 0
- f(x): 0
- f#(x): x
- mark(x): x + 2
- mat(x,y): 0
- no(x): 0
- tp(x): 0
- y: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| mat#(f(x), f(y)) | → | mat#(x, y) |
Rewrite Rules
| active(f(x)) | → | mark(f(f(x))) | | chk(no(f(x))) | → | f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
| mat(f(x), f(y)) | → | f(mat(x, y)) | | chk(no(c)) | → | active(c) |
| mat(f(x), c) | → | no(c) | | f(active(x)) | → | active(f(x)) |
| f(no(x)) | → | no(f(x)) | | f(mark(x)) | → | mark(f(x)) |
| tp(mark(x)) | → | tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))) |
Original Signature
Termination of terms over the following signature is verified: f, chk, c, no, mat, tp, active, mark, X, y
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| mat#(f(x), f(y)) | → | mat#(x, y) |