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 (148ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (901ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (7619ms), DependencyGraph (5ms), ReductionPairSAT (1169ms), DependencyGraph (6ms), SizeChangePrinciple (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (0ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| cond1#(false, n, l) | → | cond2#(gt(n, max(l)), n, l) | | cond1#(true, n, l) | → | st#(s(n), l) |
| cond2#(false, n, l) | → | st#(s(n), l) | | st#(n, l) | → | cond1#(member(n, l), n, l) |
Rewrite Rules
| sort(l) | → | st(0, l) | | st(n, l) | → | cond1(member(n, l), n, l) |
| cond1(true, n, l) | → | cons(n, st(s(n), l)) | | cond1(false, n, l) | → | cond2(gt(n, max(l)), n, l) |
| cond2(true, n, l) | → | nil | | cond2(false, n, l) | → | st(s(n), l) |
| member(n, nil) | → | false | | member(n, cons(m, l)) | → | or(equal(n, m), member(n, l)) |
| or(x, true) | → | true | | or(x, false) | → | x |
| equal(0, 0) | → | true | | equal(s(x), 0) | → | false |
| equal(0, s(y)) | → | false | | equal(s(x), s(y)) | → | equal(x, y) |
| gt(0, v) | → | false | | gt(s(u), 0) | → | true |
| gt(s(u), s(v)) | → | gt(u, v) | | max(nil) | → | 0 |
| max(cons(u, l)) | → | if(gt(u, max(l)), u, max(l)) | | if(true, u, v) | → | u |
| if(false, u, v) | → | v |
Original Signature
Termination of terms over the following signature is verified: member, sort, max, or, true, equal, cond1, cond2, 0, s, if, false, gt, st, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| cond1#(false, n, l) | → | cond2#(gt(n, max(l)), n, l) | | sort#(l) | → | st#(0, l) |
| gt#(s(u), s(v)) | → | gt#(u, v) | | st#(n, l) | → | cond1#(member(n, l), n, l) |
| st#(n, l) | → | member#(n, l) | | max#(cons(u, l)) | → | max#(l) |
| max#(cons(u, l)) | → | if#(gt(u, max(l)), u, max(l)) | | equal#(s(x), s(y)) | → | equal#(x, y) |
| cond1#(true, n, l) | → | st#(s(n), l) | | cond2#(false, n, l) | → | st#(s(n), l) |
| member#(n, cons(m, l)) | → | or#(equal(n, m), member(n, l)) | | member#(n, cons(m, l)) | → | member#(n, l) |
| max#(cons(u, l)) | → | gt#(u, max(l)) | | cond1#(false, n, l) | → | max#(l) |
| cond1#(false, n, l) | → | gt#(n, max(l)) | | member#(n, cons(m, l)) | → | equal#(n, m) |
Rewrite Rules
| sort(l) | → | st(0, l) | | st(n, l) | → | cond1(member(n, l), n, l) |
| cond1(true, n, l) | → | cons(n, st(s(n), l)) | | cond1(false, n, l) | → | cond2(gt(n, max(l)), n, l) |
| cond2(true, n, l) | → | nil | | cond2(false, n, l) | → | st(s(n), l) |
| member(n, nil) | → | false | | member(n, cons(m, l)) | → | or(equal(n, m), member(n, l)) |
| or(x, true) | → | true | | or(x, false) | → | x |
| equal(0, 0) | → | true | | equal(s(x), 0) | → | false |
| equal(0, s(y)) | → | false | | equal(s(x), s(y)) | → | equal(x, y) |
| gt(0, v) | → | false | | gt(s(u), 0) | → | true |
| gt(s(u), s(v)) | → | gt(u, v) | | max(nil) | → | 0 |
| max(cons(u, l)) | → | if(gt(u, max(l)), u, max(l)) | | if(true, u, v) | → | u |
| if(false, u, v) | → | v |
Original Signature
Termination of terms over the following signature is verified: member, sort, max, or, true, equal, cond1, cond2, 0, s, if, false, gt, st, nil, cons
Strategy
The following SCCs where found
| equal#(s(x), s(y)) → equal#(x, y) |
| cond1#(false, n, l) → cond2#(gt(n, max(l)), n, l) | cond1#(true, n, l) → st#(s(n), l) |
| cond2#(false, n, l) → st#(s(n), l) | st#(n, l) → cond1#(member(n, l), n, l) |
| member#(n, cons(m, l)) → member#(n, l) |
| gt#(s(u), s(v)) → gt#(u, v) |
| max#(cons(u, l)) → max#(l) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| equal#(s(x), s(y)) | → | equal#(x, y) |
Rewrite Rules
| sort(l) | → | st(0, l) | | st(n, l) | → | cond1(member(n, l), n, l) |
| cond1(true, n, l) | → | cons(n, st(s(n), l)) | | cond1(false, n, l) | → | cond2(gt(n, max(l)), n, l) |
| cond2(true, n, l) | → | nil | | cond2(false, n, l) | → | st(s(n), l) |
| member(n, nil) | → | false | | member(n, cons(m, l)) | → | or(equal(n, m), member(n, l)) |
| or(x, true) | → | true | | or(x, false) | → | x |
| equal(0, 0) | → | true | | equal(s(x), 0) | → | false |
| equal(0, s(y)) | → | false | | equal(s(x), s(y)) | → | equal(x, y) |
| gt(0, v) | → | false | | gt(s(u), 0) | → | true |
| gt(s(u), s(v)) | → | gt(u, v) | | max(nil) | → | 0 |
| max(cons(u, l)) | → | if(gt(u, max(l)), u, max(l)) | | if(true, u, v) | → | u |
| if(false, u, v) | → | v |
Original Signature
Termination of terms over the following signature is verified: member, sort, max, or, true, equal, cond1, cond2, 0, s, if, false, gt, st, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| equal#(s(x), s(y)) | → | equal#(x, y) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| member#(n, cons(m, l)) | → | member#(n, l) |
Rewrite Rules
| sort(l) | → | st(0, l) | | st(n, l) | → | cond1(member(n, l), n, l) |
| cond1(true, n, l) | → | cons(n, st(s(n), l)) | | cond1(false, n, l) | → | cond2(gt(n, max(l)), n, l) |
| cond2(true, n, l) | → | nil | | cond2(false, n, l) | → | st(s(n), l) |
| member(n, nil) | → | false | | member(n, cons(m, l)) | → | or(equal(n, m), member(n, l)) |
| or(x, true) | → | true | | or(x, false) | → | x |
| equal(0, 0) | → | true | | equal(s(x), 0) | → | false |
| equal(0, s(y)) | → | false | | equal(s(x), s(y)) | → | equal(x, y) |
| gt(0, v) | → | false | | gt(s(u), 0) | → | true |
| gt(s(u), s(v)) | → | gt(u, v) | | max(nil) | → | 0 |
| max(cons(u, l)) | → | if(gt(u, max(l)), u, max(l)) | | if(true, u, v) | → | u |
| if(false, u, v) | → | v |
Original Signature
Termination of terms over the following signature is verified: member, sort, max, or, true, equal, cond1, cond2, 0, s, if, false, gt, st, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| member#(n, cons(m, l)) | → | member#(n, l) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| max#(cons(u, l)) | → | max#(l) |
Rewrite Rules
| sort(l) | → | st(0, l) | | st(n, l) | → | cond1(member(n, l), n, l) |
| cond1(true, n, l) | → | cons(n, st(s(n), l)) | | cond1(false, n, l) | → | cond2(gt(n, max(l)), n, l) |
| cond2(true, n, l) | → | nil | | cond2(false, n, l) | → | st(s(n), l) |
| member(n, nil) | → | false | | member(n, cons(m, l)) | → | or(equal(n, m), member(n, l)) |
| or(x, true) | → | true | | or(x, false) | → | x |
| equal(0, 0) | → | true | | equal(s(x), 0) | → | false |
| equal(0, s(y)) | → | false | | equal(s(x), s(y)) | → | equal(x, y) |
| gt(0, v) | → | false | | gt(s(u), 0) | → | true |
| gt(s(u), s(v)) | → | gt(u, v) | | max(nil) | → | 0 |
| max(cons(u, l)) | → | if(gt(u, max(l)), u, max(l)) | | if(true, u, v) | → | u |
| if(false, u, v) | → | v |
Original Signature
Termination of terms over the following signature is verified: member, sort, max, or, true, equal, cond1, cond2, 0, s, if, false, gt, st, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| max#(cons(u, l)) | → | max#(l) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| gt#(s(u), s(v)) | → | gt#(u, v) |
Rewrite Rules
| sort(l) | → | st(0, l) | | st(n, l) | → | cond1(member(n, l), n, l) |
| cond1(true, n, l) | → | cons(n, st(s(n), l)) | | cond1(false, n, l) | → | cond2(gt(n, max(l)), n, l) |
| cond2(true, n, l) | → | nil | | cond2(false, n, l) | → | st(s(n), l) |
| member(n, nil) | → | false | | member(n, cons(m, l)) | → | or(equal(n, m), member(n, l)) |
| or(x, true) | → | true | | or(x, false) | → | x |
| equal(0, 0) | → | true | | equal(s(x), 0) | → | false |
| equal(0, s(y)) | → | false | | equal(s(x), s(y)) | → | equal(x, y) |
| gt(0, v) | → | false | | gt(s(u), 0) | → | true |
| gt(s(u), s(v)) | → | gt(u, v) | | max(nil) | → | 0 |
| max(cons(u, l)) | → | if(gt(u, max(l)), u, max(l)) | | if(true, u, v) | → | u |
| if(false, u, v) | → | v |
Original Signature
Termination of terms over the following signature is verified: member, sort, max, or, true, equal, cond1, cond2, 0, s, if, false, gt, st, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| gt#(s(u), s(v)) | → | gt#(u, v) |