TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60056 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (110ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (106ms).
| | – Problem 6 was processed with processor PolynomialLinearRange4iUR (23ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (30ms).
| – Problem 4 was processed with processor Propagation (3ms).
| | – Problem 7 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (2ms), ForwardInstantiation (1ms), Propagation (1ms)].
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| permute#(x, y, a) | → | permute#(isZero(x), x, b) | | permute#(false, x, b) | → | permute#(ack(x, x), p(x), c) |
| permute#(y, x, c) | → | permute#(x, y, a) |
Rewrite Rules
| double(x) | → | permute(x, x, a) | | permute(x, y, a) | → | permute(isZero(x), x, b) |
| permute(false, x, b) | → | permute(ack(x, x), p(x), c) | | permute(true, x, b) | → | 0 |
| permute(y, x, c) | → | s(s(permute(x, y, a))) | | p(0) | → | 0 |
| p(s(x)) | → | x | | ack(0, x) | → | plus(x, s(0)) |
| ack(s(x), 0) | → | ack(x, s(0)) | | ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
| plus(0, y) | → | y | | plus(s(x), y) | → | plus(x, s(y)) |
| plus(x, s(s(y))) | → | s(plus(s(x), y)) | | plus(x, s(0)) | → | s(x) |
| plus(x, 0) | → | x | | isZero(0) | → | true |
| isZero(s(x)) | → | false |
Original Signature
Termination of terms over the following signature is verified: plus, b, c, ack, a, true, double, 0, s, p, false, permute, isZero
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| double#(x) | → | permute#(x, x, a) | | permute#(false, x, b) | → | p#(x) |
| plus#(x, s(s(y))) | → | plus#(s(x), y) | | ack#(0, x) | → | plus#(x, s(0)) |
| ack#(s(x), s(y)) | → | ack#(s(x), y) | | permute#(false, x, b) | → | permute#(ack(x, x), p(x), c) |
| permute#(x, y, a) | → | isZero#(x) | | permute#(y, x, c) | → | permute#(x, y, a) |
| permute#(false, x, b) | → | ack#(x, x) | | ack#(s(x), s(y)) | → | ack#(x, ack(s(x), y)) |
| permute#(x, y, a) | → | permute#(isZero(x), x, b) | | ack#(s(x), 0) | → | ack#(x, s(0)) |
| plus#(s(x), y) | → | plus#(x, s(y)) |
Rewrite Rules
| double(x) | → | permute(x, x, a) | | permute(x, y, a) | → | permute(isZero(x), x, b) |
| permute(false, x, b) | → | permute(ack(x, x), p(x), c) | | permute(true, x, b) | → | 0 |
| permute(y, x, c) | → | s(s(permute(x, y, a))) | | p(0) | → | 0 |
| p(s(x)) | → | x | | ack(0, x) | → | plus(x, s(0)) |
| ack(s(x), 0) | → | ack(x, s(0)) | | ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
| plus(0, y) | → | y | | plus(s(x), y) | → | plus(x, s(y)) |
| plus(x, s(s(y))) | → | s(plus(s(x), y)) | | plus(x, s(0)) | → | s(x) |
| plus(x, 0) | → | x | | isZero(0) | → | true |
| isZero(s(x)) | → | false |
Original Signature
Termination of terms over the following signature is verified: plus, b, c, ack, a, true, double, 0, s, p, false, permute, isZero
Strategy
The following SCCs where found
| ack#(s(x), s(y)) → ack#(s(x), y) | ack#(s(x), s(y)) → ack#(x, ack(s(x), y)) |
| ack#(s(x), 0) → ack#(x, s(0)) |
| plus#(x, s(s(y))) → plus#(s(x), y) | plus#(s(x), y) → plus#(x, s(y)) |
| permute#(false, x, b) → permute#(ack(x, x), p(x), c) | permute#(x, y, a) → permute#(isZero(x), x, b) |
| permute#(y, x, c) → permute#(x, y, a) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| plus#(x, s(s(y))) | → | plus#(s(x), y) | | plus#(s(x), y) | → | plus#(x, s(y)) |
Rewrite Rules
| double(x) | → | permute(x, x, a) | | permute(x, y, a) | → | permute(isZero(x), x, b) |
| permute(false, x, b) | → | permute(ack(x, x), p(x), c) | | permute(true, x, b) | → | 0 |
| permute(y, x, c) | → | s(s(permute(x, y, a))) | | p(0) | → | 0 |
| p(s(x)) | → | x | | ack(0, x) | → | plus(x, s(0)) |
| ack(s(x), 0) | → | ack(x, s(0)) | | ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
| plus(0, y) | → | y | | plus(s(x), y) | → | plus(x, s(y)) |
| plus(x, s(s(y))) | → | s(plus(s(x), y)) | | plus(x, s(0)) | → | s(x) |
| plus(x, 0) | → | x | | isZero(0) | → | true |
| isZero(s(x)) | → | false |
Original Signature
Termination of terms over the following signature is verified: plus, b, c, ack, a, true, double, 0, s, p, false, permute, isZero
Strategy
Polynomial Interpretation
- 0: 0
- a: 0
- ack(x,y): 0
- b: 0
- c: 0
- double(x): 0
- false: 0
- isZero(x): 0
- p(x): 0
- permute(x,y,z): 0
- plus(x,y): 0
- plus#(x,y): y + x
- s(x): x + 1
- true: 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:
| plus#(x, s(s(y))) | → | plus#(s(x), y) |
Problem 6: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, s(y)) |
Rewrite Rules
| double(x) | → | permute(x, x, a) | | permute(x, y, a) | → | permute(isZero(x), x, b) |
| permute(false, x, b) | → | permute(ack(x, x), p(x), c) | | permute(true, x, b) | → | 0 |
| permute(y, x, c) | → | s(s(permute(x, y, a))) | | p(0) | → | 0 |
| p(s(x)) | → | x | | ack(0, x) | → | plus(x, s(0)) |
| ack(s(x), 0) | → | ack(x, s(0)) | | ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
| plus(0, y) | → | y | | plus(s(x), y) | → | plus(x, s(y)) |
| plus(x, s(s(y))) | → | s(plus(s(x), y)) | | plus(x, s(0)) | → | s(x) |
| plus(x, 0) | → | x | | isZero(0) | → | true |
| isZero(s(x)) | → | false |
Original Signature
Termination of terms over the following signature is verified: plus, b, c, ack, a, true, double, 0, s, p, false, permute, isZero
Strategy
Polynomial Interpretation
- 0: 0
- a: 0
- ack(x,y): 0
- b: 0
- c: 0
- double(x): 0
- false: 0
- isZero(x): 0
- p(x): 0
- permute(x,y,z): 0
- plus(x,y): 0
- plus#(x,y): x
- s(x): x + 2
- true: 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:
| plus#(s(x), y) | → | plus#(x, s(y)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ack#(s(x), s(y)) | → | ack#(s(x), y) | | ack#(s(x), s(y)) | → | ack#(x, ack(s(x), y)) |
| ack#(s(x), 0) | → | ack#(x, s(0)) |
Rewrite Rules
| double(x) | → | permute(x, x, a) | | permute(x, y, a) | → | permute(isZero(x), x, b) |
| permute(false, x, b) | → | permute(ack(x, x), p(x), c) | | permute(true, x, b) | → | 0 |
| permute(y, x, c) | → | s(s(permute(x, y, a))) | | p(0) | → | 0 |
| p(s(x)) | → | x | | ack(0, x) | → | plus(x, s(0)) |
| ack(s(x), 0) | → | ack(x, s(0)) | | ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
| plus(0, y) | → | y | | plus(s(x), y) | → | plus(x, s(y)) |
| plus(x, s(s(y))) | → | s(plus(s(x), y)) | | plus(x, s(0)) | → | s(x) |
| plus(x, 0) | → | x | | isZero(0) | → | true |
| isZero(s(x)) | → | false |
Original Signature
Termination of terms over the following signature is verified: plus, b, c, ack, a, true, double, 0, s, p, false, permute, isZero
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ack#(s(x), s(y)) | → | ack#(x, ack(s(x), y)) | | ack#(s(x), 0) | → | ack#(x, s(0)) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ack#(s(x), s(y)) | → | ack#(s(x), y) |
Rewrite Rules
| double(x) | → | permute(x, x, a) | | permute(x, y, a) | → | permute(isZero(x), x, b) |
| permute(false, x, b) | → | permute(ack(x, x), p(x), c) | | permute(true, x, b) | → | 0 |
| permute(y, x, c) | → | s(s(permute(x, y, a))) | | p(0) | → | 0 |
| p(s(x)) | → | x | | ack(0, x) | → | plus(x, s(0)) |
| ack(s(x), 0) | → | ack(x, s(0)) | | ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
| plus(0, y) | → | y | | plus(s(x), y) | → | plus(x, s(y)) |
| plus(x, s(s(y))) | → | s(plus(s(x), y)) | | plus(x, s(0)) | → | s(x) |
| plus(x, 0) | → | x | | isZero(0) | → | true |
| isZero(s(x)) | → | false |
Original Signature
Termination of terms over the following signature is verified: plus, b, c, ack, a, true, double, 0, s, p, false, permute, isZero
Strategy
Polynomial Interpretation
- 0: 0
- a: 0
- ack(x,y): 0
- ack#(x,y): y
- b: 0
- c: 0
- double(x): 0
- false: 0
- isZero(x): 0
- p(x): 0
- permute(x,y,z): 0
- plus(x,y): 0
- s(x): 2x + 1
- true: 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:
| ack#(s(x), s(y)) | → | ack#(s(x), y) |
Problem 4: Propagation
Dependency Pair Problem
Dependency Pairs
| permute#(false, x, b) | → | permute#(ack(x, x), p(x), c) | | permute#(x, y, a) | → | permute#(isZero(x), x, b) |
| permute#(y, x, c) | → | permute#(x, y, a) |
Rewrite Rules
| double(x) | → | permute(x, x, a) | | permute(x, y, a) | → | permute(isZero(x), x, b) |
| permute(false, x, b) | → | permute(ack(x, x), p(x), c) | | permute(true, x, b) | → | 0 |
| permute(y, x, c) | → | s(s(permute(x, y, a))) | | p(0) | → | 0 |
| p(s(x)) | → | x | | ack(0, x) | → | plus(x, s(0)) |
| ack(s(x), 0) | → | ack(x, s(0)) | | ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
| plus(0, y) | → | y | | plus(s(x), y) | → | plus(x, s(y)) |
| plus(x, s(s(y))) | → | s(plus(s(x), y)) | | plus(x, s(0)) | → | s(x) |
| plus(x, 0) | → | x | | isZero(0) | → | true |
| isZero(s(x)) | → | false |
Original Signature
Termination of terms over the following signature is verified: plus, b, c, ack, a, true, double, 0, s, p, false, permute, isZero
Strategy
The dependency pairs permute
#(
y,
x, c) → permute
#(
x,
y, a) and permute
#(
x,
y, a) → permute
#(isZero(
x),
x, b) are consolidated into the rule permute
#(
y,
x, c) → permute
#(isZero(
x),
x, b) .
This is possible as
- all subterms of permute#(x, y, a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in permute#(x, y, a), but non-replacing in both permute#(y, x, c) and permute#(isZero(x), x, b)
The dependency pairs permute
#(
y,
x, c) → permute
#(
x,
y, a) and permute
#(
x,
y, a) → permute
#(isZero(
x),
x, b) are consolidated into the rule permute
#(
y,
x, c) → permute
#(isZero(
x),
x, b) .
This is possible as
- all subterms of permute#(x, y, a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in permute#(x, y, a), but non-replacing in both permute#(y, x, c) and permute#(isZero(x), x, b)
The dependency pairs permute
#(
y,
x, c) → permute
#(
x,
y, a) and permute
#(
x,
y, a) → permute
#(isZero(
x),
x, b) are consolidated into the rule permute
#(
y,
x, c) → permute
#(isZero(
x),
x, b) .
This is possible as
- all subterms of permute#(x, y, a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in permute#(x, y, a), but non-replacing in both permute#(y, x, c) and permute#(isZero(x), x, b)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| permute#(x, y, a) → permute#(isZero(x), x, b) | permute#(y, x, c) → permute#(isZero(x), x, b) |
| permute#(y, x, c) → permute#(x, y, a) | |