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 (55ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| | – Problem 5 was processed with processor DependencyGraph (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor BackwardInstantiation (4ms).
| | – Problem 6 was processed with processor BackwardInstantiation (2ms).
| | | – Problem 7 was processed with processor Propagation (5ms).
| | | | – Problem 8 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (0ms), ForwardInstantiation (1ms), Propagation (2ms)].
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| if2#(false, x, y) | → | test#(x, s(y)) | | if1#(true, x, y) | → | if2#(divides(x, y), x, y) |
| test#(x, y) | → | if1#(gt(x, y), x, y) |
Rewrite Rules
| gt(s(x), 0) | → | true | | gt(0, y) | → | false |
| gt(s(x), s(y)) | → | gt(x, y) | | divides(x, y) | → | div(x, y, y) |
| div(0, 0, z) | → | true | | div(0, s(x), z) | → | false |
| div(s(x), 0, s(z)) | → | div(s(x), s(z), s(z)) | | div(s(x), s(y), z) | → | div(x, y, z) |
| prime(x) | → | test(x, s(s(0))) | | test(x, y) | → | if1(gt(x, y), x, y) |
| if1(true, x, y) | → | if2(divides(x, y), x, y) | | if1(false, x, y) | → | true |
| if2(true, x, y) | → | false | | if2(false, x, y) | → | test(x, s(y)) |
Original Signature
Termination of terms over the following signature is verified: prime, 0, s, test, div, false, true, if1, divides, gt, if2
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| div#(s(x), 0, s(z)) | → | div#(s(x), s(z), s(z)) | | if2#(false, x, y) | → | test#(x, s(y)) |
| divides#(x, y) | → | div#(x, y, y) | | test#(x, y) | → | gt#(x, y) |
| test#(x, y) | → | if1#(gt(x, y), x, y) | | if1#(true, x, y) | → | if2#(divides(x, y), x, y) |
| gt#(s(x), s(y)) | → | gt#(x, y) | | if1#(true, x, y) | → | divides#(x, y) |
| prime#(x) | → | test#(x, s(s(0))) | | div#(s(x), s(y), z) | → | div#(x, y, z) |
Rewrite Rules
| gt(s(x), 0) | → | true | | gt(0, y) | → | false |
| gt(s(x), s(y)) | → | gt(x, y) | | divides(x, y) | → | div(x, y, y) |
| div(0, 0, z) | → | true | | div(0, s(x), z) | → | false |
| div(s(x), 0, s(z)) | → | div(s(x), s(z), s(z)) | | div(s(x), s(y), z) | → | div(x, y, z) |
| prime(x) | → | test(x, s(s(0))) | | test(x, y) | → | if1(gt(x, y), x, y) |
| if1(true, x, y) | → | if2(divides(x, y), x, y) | | if1(false, x, y) | → | true |
| if2(true, x, y) | → | false | | if2(false, x, y) | → | test(x, s(y)) |
Original Signature
Termination of terms over the following signature is verified: prime, 0, s, test, div, true, false, gt, divides, if1, if2
Strategy
The following SCCs where found
| gt#(s(x), s(y)) → gt#(x, y) |
| if2#(false, x, y) → test#(x, s(y)) | test#(x, y) → if1#(gt(x, y), x, y) |
| if1#(true, x, y) → if2#(divides(x, y), x, y) |
| div#(s(x), 0, s(z)) → div#(s(x), s(z), s(z)) | div#(s(x), s(y), z) → div#(x, y, z) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| div#(s(x), 0, s(z)) | → | div#(s(x), s(z), s(z)) | | div#(s(x), s(y), z) | → | div#(x, y, z) |
Rewrite Rules
| gt(s(x), 0) | → | true | | gt(0, y) | → | false |
| gt(s(x), s(y)) | → | gt(x, y) | | divides(x, y) | → | div(x, y, y) |
| div(0, 0, z) | → | true | | div(0, s(x), z) | → | false |
| div(s(x), 0, s(z)) | → | div(s(x), s(z), s(z)) | | div(s(x), s(y), z) | → | div(x, y, z) |
| prime(x) | → | test(x, s(s(0))) | | test(x, y) | → | if1(gt(x, y), x, y) |
| if1(true, x, y) | → | if2(divides(x, y), x, y) | | if1(false, x, y) | → | true |
| if2(true, x, y) | → | false | | if2(false, x, y) | → | test(x, s(y)) |
Original Signature
Termination of terms over the following signature is verified: prime, 0, s, test, div, true, false, gt, divides, if1, if2
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| div#(s(x), s(y), z) | → | div#(x, y, z) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| div#(s(x), 0, s(z)) | → | div#(s(x), s(z), s(z)) |
Rewrite Rules
| gt(s(x), 0) | → | true | | gt(0, y) | → | false |
| gt(s(x), s(y)) | → | gt(x, y) | | divides(x, y) | → | div(x, y, y) |
| div(0, 0, z) | → | true | | div(0, s(x), z) | → | false |
| div(s(x), 0, s(z)) | → | div(s(x), s(z), s(z)) | | div(s(x), s(y), z) | → | div(x, y, z) |
| prime(x) | → | test(x, s(s(0))) | | test(x, y) | → | if1(gt(x, y), x, y) |
| if1(true, x, y) | → | if2(divides(x, y), x, y) | | if1(false, x, y) | → | true |
| if2(true, x, y) | → | false | | if2(false, x, y) | → | test(x, s(y)) |
Original Signature
Termination of terms over the following signature is verified: prime, 0, s, test, div, false, true, if1, divides, gt, if2
Strategy
There are no SCCs!
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| gt#(s(x), s(y)) | → | gt#(x, y) |
Rewrite Rules
| gt(s(x), 0) | → | true | | gt(0, y) | → | false |
| gt(s(x), s(y)) | → | gt(x, y) | | divides(x, y) | → | div(x, y, y) |
| div(0, 0, z) | → | true | | div(0, s(x), z) | → | false |
| div(s(x), 0, s(z)) | → | div(s(x), s(z), s(z)) | | div(s(x), s(y), z) | → | div(x, y, z) |
| prime(x) | → | test(x, s(s(0))) | | test(x, y) | → | if1(gt(x, y), x, y) |
| if1(true, x, y) | → | if2(divides(x, y), x, y) | | if1(false, x, y) | → | true |
| if2(true, x, y) | → | false | | if2(false, x, y) | → | test(x, s(y)) |
Original Signature
Termination of terms over the following signature is verified: prime, 0, s, test, div, true, false, gt, divides, if1, if2
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| gt#(s(x), s(y)) | → | gt#(x, y) |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if2#(false, x, y) | → | test#(x, s(y)) | | test#(x, y) | → | if1#(gt(x, y), x, y) |
| if1#(true, x, y) | → | if2#(divides(x, y), x, y) |
Rewrite Rules
| gt(s(x), 0) | → | true | | gt(0, y) | → | false |
| gt(s(x), s(y)) | → | gt(x, y) | | divides(x, y) | → | div(x, y, y) |
| div(0, 0, z) | → | true | | div(0, s(x), z) | → | false |
| div(s(x), 0, s(z)) | → | div(s(x), s(z), s(z)) | | div(s(x), s(y), z) | → | div(x, y, z) |
| prime(x) | → | test(x, s(s(0))) | | test(x, y) | → | if1(gt(x, y), x, y) |
| if1(true, x, y) | → | if2(divides(x, y), x, y) | | if1(false, x, y) | → | true |
| if2(true, x, y) | → | false | | if2(false, x, y) | → | test(x, s(y)) |
Original Signature
Termination of terms over the following signature is verified: prime, 0, s, test, div, true, false, gt, divides, if1, if2
Strategy
Instantiation
For all potential predecessors l → r of the rule test
#(
x,
y) → if1
#(gt(
x,
y),
x,
y) on dependency pair chains it holds that:
- test#(x, y) matches r,
- all variables of test#(x, y) are embedded in constructor contexts, i.e., each subterm of test#(x, y), containing a variable is rooted by a constructor symbol.
Thus, test
#(
x,
y) → if1
#(gt(
x,
y),
x,
y) is replaced by instances determined through the above matching. These instances are:
| test#(_x, s(_y)) → if1#(gt(_x, s(_y)), _x, s(_y)) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if2#(false, x, y) | → | test#(x, s(y)) | | if1#(true, x, y) | → | if2#(divides(x, y), x, y) |
| test#(_x, s(_y)) | → | if1#(gt(_x, s(_y)), _x, s(_y)) |
Rewrite Rules
| gt(s(x), 0) | → | true | | gt(0, y) | → | false |
| gt(s(x), s(y)) | → | gt(x, y) | | divides(x, y) | → | div(x, y, y) |
| div(0, 0, z) | → | true | | div(0, s(x), z) | → | false |
| div(s(x), 0, s(z)) | → | div(s(x), s(z), s(z)) | | div(s(x), s(y), z) | → | div(x, y, z) |
| prime(x) | → | test(x, s(s(0))) | | test(x, y) | → | if1(gt(x, y), x, y) |
| if1(true, x, y) | → | if2(divides(x, y), x, y) | | if1(false, x, y) | → | true |
| if2(true, x, y) | → | false | | if2(false, x, y) | → | test(x, s(y)) |
Original Signature
Termination of terms over the following signature is verified: prime, 0, s, test, div, false, true, if1, divides, gt, if2
Strategy
Instantiation
For all potential predecessors l → r of the rule test
#(
_x, s(
_y)) → if1
#(gt(
_x, s(
_y)),
_x, s(
_y)) on dependency pair chains it holds that:
- test#(_x, s(_y)) matches r,
- all variables of test#(_x, s(_y)) are embedded in constructor contexts, i.e., each subterm of test#(_x, s(_y)), containing a variable is rooted by a constructor symbol.
Thus, test
#(
_x, s(
_y)) → if1
#(gt(
_x, s(
_y)),
_x, s(
_y)) is replaced by instances determined through the above matching. These instances are:
| test#(x, s(y)) → if1#(gt(x, s(y)), x, s(y)) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| if2#(false, x, y) | → | test#(x, s(y)) | | test#(x, s(y)) | → | if1#(gt(x, s(y)), x, s(y)) |
| if1#(true, x, y) | → | if2#(divides(x, y), x, y) |
Rewrite Rules
| gt(s(x), 0) | → | true | | gt(0, y) | → | false |
| gt(s(x), s(y)) | → | gt(x, y) | | divides(x, y) | → | div(x, y, y) |
| div(0, 0, z) | → | true | | div(0, s(x), z) | → | false |
| div(s(x), 0, s(z)) | → | div(s(x), s(z), s(z)) | | div(s(x), s(y), z) | → | div(x, y, z) |
| prime(x) | → | test(x, s(s(0))) | | test(x, y) | → | if1(gt(x, y), x, y) |
| if1(true, x, y) | → | if2(divides(x, y), x, y) | | if1(false, x, y) | → | true |
| if2(true, x, y) | → | false | | if2(false, x, y) | → | test(x, s(y)) |
Original Signature
Termination of terms over the following signature is verified: prime, 0, s, test, div, true, false, gt, divides, if1, if2
Strategy
The dependency pairs if2
#(false,
x,
y) → test
#(
x, s(
y)) and test
#(
x, s(
y)) → if1
#(gt(
x, s(
y)),
x, s(
y)) are consolidated into the rule if2
#(false,
x,
y) → if1
#(gt(
x, s(
y)),
x, s(
y)) .
This is possible as
- all subterms of test#(x, s(y)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in test#(x, s(y)), but non-replacing in both if2#(false, x, y) and if1#(gt(x, s(y)), x, s(y))
The dependency pairs if2
#(false,
x,
y) → test
#(
x, s(
y)) and test
#(
x, s(
y)) → if1
#(gt(
x, s(
y)),
x, s(
y)) are consolidated into the rule if2
#(false,
x,
y) → if1
#(gt(
x, s(
y)),
x, s(
y)) .
This is possible as
- all subterms of test#(x, s(y)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in test#(x, s(y)), but non-replacing in both if2#(false, x, y) and if1#(gt(x, s(y)), x, s(y))
The dependency pairs if2
#(false,
x,
y) → test
#(
x, s(
y)) and test
#(
x, s(
y)) → if1
#(gt(
x, s(
y)),
x, s(
y)) are consolidated into the rule if2
#(false,
x,
y) → if1
#(gt(
x, s(
y)),
x, s(
y)) .
This is possible as
- all subterms of test#(x, s(y)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in test#(x, s(y)), but non-replacing in both if2#(false, x, y) and if1#(gt(x, s(y)), x, s(y))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| test#(x, s(y)) → if1#(gt(x, s(y)), x, s(y)) | if2#(false, x, y) → if1#(gt(x, s(y)), x, s(y)) |
| if2#(false, x, y) → test#(x, s(y)) | |