TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60002 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (281ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (29ms), PolynomialLinearRange4iUR (1336ms), DependencyGraph (29ms), PolynomialLinearRange8NegiUR (13699ms), DependencyGraph (21ms), ReductionPairSAT (timeout)].
| – Problem 4 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| reach#(x, y, i, h) | → | if1#(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h) | | if4#(false, x, y, i, h) | → | reach#(to(i), y, union(rest(i), h), empty) |
| if4#(false, x, y, i, h) | → | reach#(x, y, rest(i), h) | | if3#(true, b3, x, y, i, h) | → | if4#(b3, x, y, i, h) |
| if1#(false, b1, b2, b3, x, y, i, h) | → | if2#(b1, b2, b3, x, y, i, h) | | if2#(false, b2, b3, x, y, i, h) | → | if3#(b2, b3, x, y, i, h) |
| if3#(false, b3, x, y, i, h) | → | reach#(x, y, rest(i), edge(from(i), to(i), h)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| isEmpty(empty) | → | true | | isEmpty(edge(x, y, i)) | → | false |
| from(edge(x, y, i)) | → | x | | to(edge(x, y, i)) | → | y |
| rest(edge(x, y, i)) | → | i | | rest(empty) | → | empty |
| reach(x, y, i, h) | → | if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h) | | if1(true, b1, b2, b3, x, y, i, h) | → | true |
| if1(false, b1, b2, b3, x, y, i, h) | → | if2(b1, b2, b3, x, y, i, h) | | if2(true, b2, b3, x, y, i, h) | → | false |
| if2(false, b2, b3, x, y, i, h) | → | if3(b2, b3, x, y, i, h) | | if3(false, b3, x, y, i, h) | → | reach(x, y, rest(i), edge(from(i), to(i), h)) |
| if3(true, b3, x, y, i, h) | → | if4(b3, x, y, i, h) | | if4(true, x, y, i, h) | → | true |
| if4(false, x, y, i, h) | → | or(reach(x, y, rest(i), h), reach(to(i), y, union(rest(i), h), empty)) |
Original Signature
Termination of terms over the following signature is verified: to, edge, or, if3, if4, true, if1, if2, from, reach, isEmpty, 0, s, union, empty, false, rest, eq
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| reach#(x, y, i, h) | → | if1#(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h) | | if3#(false, b3, x, y, i, h) | → | from#(i) |
| if3#(true, b3, x, y, i, h) | → | if4#(b3, x, y, i, h) | | if1#(false, b1, b2, b3, x, y, i, h) | → | if2#(b1, b2, b3, x, y, i, h) |
| reach#(x, y, i, h) | → | eq#(x, from(i)) | | if2#(false, b2, b3, x, y, i, h) | → | if3#(b2, b3, x, y, i, h) |
| reach#(x, y, i, h) | → | isEmpty#(i) | | if3#(false, b3, x, y, i, h) | → | reach#(x, y, rest(i), edge(from(i), to(i), h)) |
| if4#(false, x, y, i, h) | → | or#(reach(x, y, rest(i), h), reach(to(i), y, union(rest(i), h), empty)) | | reach#(x, y, i, h) | → | eq#(x, y) |
| if3#(false, b3, x, y, i, h) | → | rest#(i) | | if4#(false, x, y, i, h) | → | reach#(to(i), y, union(rest(i), h), empty) |
| reach#(x, y, i, h) | → | to#(i) | | reach#(x, y, i, h) | → | from#(i) |
| reach#(x, y, i, h) | → | eq#(y, to(i)) | | if4#(false, x, y, i, h) | → | reach#(x, y, rest(i), h) |
| if4#(false, x, y, i, h) | → | rest#(i) | | eq#(s(x), s(y)) | → | eq#(x, y) |
| if4#(false, x, y, i, h) | → | union#(rest(i), h) | | union#(edge(x, y, i), h) | → | union#(i, h) |
| if3#(false, b3, x, y, i, h) | → | to#(i) | | if4#(false, x, y, i, h) | → | to#(i) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| isEmpty(empty) | → | true | | isEmpty(edge(x, y, i)) | → | false |
| from(edge(x, y, i)) | → | x | | to(edge(x, y, i)) | → | y |
| rest(edge(x, y, i)) | → | i | | rest(empty) | → | empty |
| reach(x, y, i, h) | → | if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h) | | if1(true, b1, b2, b3, x, y, i, h) | → | true |
| if1(false, b1, b2, b3, x, y, i, h) | → | if2(b1, b2, b3, x, y, i, h) | | if2(true, b2, b3, x, y, i, h) | → | false |
| if2(false, b2, b3, x, y, i, h) | → | if3(b2, b3, x, y, i, h) | | if3(false, b3, x, y, i, h) | → | reach(x, y, rest(i), edge(from(i), to(i), h)) |
| if3(true, b3, x, y, i, h) | → | if4(b3, x, y, i, h) | | if4(true, x, y, i, h) | → | true |
| if4(false, x, y, i, h) | → | or(reach(x, y, rest(i), h), reach(to(i), y, union(rest(i), h), empty)) |
Original Signature
Termination of terms over the following signature is verified: to, edge, or, if3, if4, true, if1, if2, from, reach, isEmpty, 0, s, union, empty, false, rest, eq
Strategy
The following SCCs where found
| if4#(false, x, y, i, h) → reach#(to(i), y, union(rest(i), h), empty) | reach#(x, y, i, h) → if1#(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h) |
| if3#(true, b3, x, y, i, h) → if4#(b3, x, y, i, h) | if4#(false, x, y, i, h) → reach#(x, y, rest(i), h) |
| if1#(false, b1, b2, b3, x, y, i, h) → if2#(b1, b2, b3, x, y, i, h) | if2#(false, b2, b3, x, y, i, h) → if3#(b2, b3, x, y, i, h) |
| if3#(false, b3, x, y, i, h) → reach#(x, y, rest(i), edge(from(i), to(i), h)) |
| eq#(s(x), s(y)) → eq#(x, y) |
| union#(edge(x, y, i), h) → union#(i, h) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| union#(edge(x, y, i), h) | → | union#(i, h) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| isEmpty(empty) | → | true | | isEmpty(edge(x, y, i)) | → | false |
| from(edge(x, y, i)) | → | x | | to(edge(x, y, i)) | → | y |
| rest(edge(x, y, i)) | → | i | | rest(empty) | → | empty |
| reach(x, y, i, h) | → | if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h) | | if1(true, b1, b2, b3, x, y, i, h) | → | true |
| if1(false, b1, b2, b3, x, y, i, h) | → | if2(b1, b2, b3, x, y, i, h) | | if2(true, b2, b3, x, y, i, h) | → | false |
| if2(false, b2, b3, x, y, i, h) | → | if3(b2, b3, x, y, i, h) | | if3(false, b3, x, y, i, h) | → | reach(x, y, rest(i), edge(from(i), to(i), h)) |
| if3(true, b3, x, y, i, h) | → | if4(b3, x, y, i, h) | | if4(true, x, y, i, h) | → | true |
| if4(false, x, y, i, h) | → | or(reach(x, y, rest(i), h), reach(to(i), y, union(rest(i), h), empty)) |
Original Signature
Termination of terms over the following signature is verified: to, edge, or, if3, if4, true, if1, if2, from, reach, isEmpty, 0, s, union, empty, false, rest, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| union#(edge(x, y, i), h) | → | union#(i, h) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(s(x), s(y)) | → | eq#(x, y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| isEmpty(empty) | → | true | | isEmpty(edge(x, y, i)) | → | false |
| from(edge(x, y, i)) | → | x | | to(edge(x, y, i)) | → | y |
| rest(edge(x, y, i)) | → | i | | rest(empty) | → | empty |
| reach(x, y, i, h) | → | if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h) | | if1(true, b1, b2, b3, x, y, i, h) | → | true |
| if1(false, b1, b2, b3, x, y, i, h) | → | if2(b1, b2, b3, x, y, i, h) | | if2(true, b2, b3, x, y, i, h) | → | false |
| if2(false, b2, b3, x, y, i, h) | → | if3(b2, b3, x, y, i, h) | | if3(false, b3, x, y, i, h) | → | reach(x, y, rest(i), edge(from(i), to(i), h)) |
| if3(true, b3, x, y, i, h) | → | if4(b3, x, y, i, h) | | if4(true, x, y, i, h) | → | true |
| if4(false, x, y, i, h) | → | or(reach(x, y, rest(i), h), reach(to(i), y, union(rest(i), h), empty)) |
Original Signature
Termination of terms over the following signature is verified: to, edge, or, if3, if4, true, if1, if2, from, reach, isEmpty, 0, s, union, empty, false, rest, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(s(x), s(y)) | → | eq#(x, y) |