TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (112ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor BackwardInstantiation (6ms).
| | – Problem 5 was processed with processor ForwardInstantiation (5ms).
| | | – Problem 7 was processed with processor Propagation (12ms).
| | | | – Problem 8 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (3ms), ForwardInstantiation (3ms), Propagation (1ms)].
| – Problem 4 was processed with processor BackwardInstantiation (1ms).
| | – Problem 6 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms), ForwardNarrowing (1ms), BackwardInstantiation (3ms), ForwardInstantiation (1ms), Propagation (1ms)].
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| if2#(false, x, y) | → | int#(p(x), p(y)) | | if_int#(true, b, x, y) | → | if1#(b, x, y) |
| if1#(false, x, y) | → | int#(s(0), y) | | if_int#(false, b, x, y) | → | if2#(b, x, y) |
| int#(x, y) | → | if_int#(zero(x), zero(y), x, y) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, y)) | → | false |
| tail(nil) | → | nil | | tail(cons(x, y)) | → | y |
| head(cons(x, y)) | → | x | | zero(0) | → | true |
| zero(s(x)) | → | false | | p(0) | → | 0 |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| intlist(x) | → | if_intlist(empty(x), x) | | if_intlist(true, x) | → | nil |
| if_intlist(false, x) | → | cons(s(head(x)), intlist(tail(x))) | | int(x, y) | → | if_int(zero(x), zero(y), x, y) |
| if_int(true, b, x, y) | → | if1(b, x, y) | | if_int(false, b, x, y) | → | if2(b, x, y) |
| if1(true, x, y) | → | cons(0, nil) | | if1(false, x, y) | → | cons(0, int(s(0), y)) |
| if2(true, x, y) | → | nil | | if2(false, x, y) | → | intlist(int(p(x), p(y))) |
Original Signature
Termination of terms over the following signature is verified: int, true, if1, if2, zero, if_int, tail, if_intlist, 0, s, p, empty, false, intlist, head, nil, cons
Open Dependency Pair Problem 4
Dependency Pairs
| intlist#(x) | → | if_intlist#(empty(x), x) | | if_intlist#(false, x) | → | intlist#(tail(x)) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, y)) | → | false |
| tail(nil) | → | nil | | tail(cons(x, y)) | → | y |
| head(cons(x, y)) | → | x | | zero(0) | → | true |
| zero(s(x)) | → | false | | p(0) | → | 0 |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| intlist(x) | → | if_intlist(empty(x), x) | | if_intlist(true, x) | → | nil |
| if_intlist(false, x) | → | cons(s(head(x)), intlist(tail(x))) | | int(x, y) | → | if_int(zero(x), zero(y), x, y) |
| if_int(true, b, x, y) | → | if1(b, x, y) | | if_int(false, b, x, y) | → | if2(b, x, y) |
| if1(true, x, y) | → | cons(0, nil) | | if1(false, x, y) | → | cons(0, int(s(0), y)) |
| if2(true, x, y) | → | nil | | if2(false, x, y) | → | intlist(int(p(x), p(y))) |
Original Signature
Termination of terms over the following signature is verified: int, true, if1, if2, zero, if_int, tail, if_intlist, 0, s, p, empty, false, intlist, head, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if_intlist#(false, x) | → | head#(x) | | if_int#(true, b, x, y) | → | if1#(b, x, y) |
| int#(x, y) | → | zero#(y) | | intlist#(x) | → | empty#(x) |
| if2#(false, x, y) | → | p#(x) | | if2#(false, x, y) | → | p#(y) |
| if2#(false, x, y) | → | int#(p(x), p(y)) | | if2#(false, x, y) | → | intlist#(int(p(x), p(y))) |
| int#(x, y) | → | zero#(x) | | intlist#(x) | → | if_intlist#(empty(x), x) |
| if1#(false, x, y) | → | int#(s(0), y) | | if_intlist#(false, x) | → | intlist#(tail(x)) |
| if_int#(false, b, x, y) | → | if2#(b, x, y) | | if_intlist#(false, x) | → | tail#(x) |
| p#(s(s(x))) | → | p#(s(x)) | | int#(x, y) | → | if_int#(zero(x), zero(y), x, y) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, y)) | → | false |
| tail(nil) | → | nil | | tail(cons(x, y)) | → | y |
| head(cons(x, y)) | → | x | | zero(0) | → | true |
| zero(s(x)) | → | false | | p(0) | → | 0 |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| intlist(x) | → | if_intlist(empty(x), x) | | if_intlist(true, x) | → | nil |
| if_intlist(false, x) | → | cons(s(head(x)), intlist(tail(x))) | | int(x, y) | → | if_int(zero(x), zero(y), x, y) |
| if_int(true, b, x, y) | → | if1(b, x, y) | | if_int(false, b, x, y) | → | if2(b, x, y) |
| if1(true, x, y) | → | cons(0, nil) | | if1(false, x, y) | → | cons(0, int(s(0), y)) |
| if2(true, x, y) | → | nil | | if2(false, x, y) | → | intlist(int(p(x), p(y))) |
Original Signature
Termination of terms over the following signature is verified: int, true, if1, if2, zero, if_int, tail, if_intlist, 0, s, p, empty, false, intlist, head, cons, nil
Strategy
The following SCCs where found
| if2#(false, x, y) → int#(p(x), p(y)) | if_int#(true, b, x, y) → if1#(b, x, y) |
| if1#(false, x, y) → int#(s(0), y) | if_int#(false, b, x, y) → if2#(b, x, y) |
| int#(x, y) → if_int#(zero(x), zero(y), x, y) |
| intlist#(x) → if_intlist#(empty(x), x) | if_intlist#(false, x) → intlist#(tail(x)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, y)) | → | false |
| tail(nil) | → | nil | | tail(cons(x, y)) | → | y |
| head(cons(x, y)) | → | x | | zero(0) | → | true |
| zero(s(x)) | → | false | | p(0) | → | 0 |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| intlist(x) | → | if_intlist(empty(x), x) | | if_intlist(true, x) | → | nil |
| if_intlist(false, x) | → | cons(s(head(x)), intlist(tail(x))) | | int(x, y) | → | if_int(zero(x), zero(y), x, y) |
| if_int(true, b, x, y) | → | if1(b, x, y) | | if_int(false, b, x, y) | → | if2(b, x, y) |
| if1(true, x, y) | → | cons(0, nil) | | if1(false, x, y) | → | cons(0, int(s(0), y)) |
| if2(true, x, y) | → | nil | | if2(false, x, y) | → | intlist(int(p(x), p(y))) |
Original Signature
Termination of terms over the following signature is verified: int, true, if1, if2, zero, if_int, tail, if_intlist, 0, s, p, empty, false, intlist, head, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if2#(false, x, y) | → | int#(p(x), p(y)) | | if_int#(true, b, x, y) | → | if1#(b, x, y) |
| if1#(false, x, y) | → | int#(s(0), y) | | if_int#(false, b, x, y) | → | if2#(b, x, y) |
| int#(x, y) | → | if_int#(zero(x), zero(y), x, y) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, y)) | → | false |
| tail(nil) | → | nil | | tail(cons(x, y)) | → | y |
| head(cons(x, y)) | → | x | | zero(0) | → | true |
| zero(s(x)) | → | false | | p(0) | → | 0 |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| intlist(x) | → | if_intlist(empty(x), x) | | if_intlist(true, x) | → | nil |
| if_intlist(false, x) | → | cons(s(head(x)), intlist(tail(x))) | | int(x, y) | → | if_int(zero(x), zero(y), x, y) |
| if_int(true, b, x, y) | → | if1(b, x, y) | | if_int(false, b, x, y) | → | if2(b, x, y) |
| if1(true, x, y) | → | cons(0, nil) | | if1(false, x, y) | → | cons(0, int(s(0), y)) |
| if2(true, x, y) | → | nil | | if2(false, x, y) | → | intlist(int(p(x), p(y))) |
Original Signature
Termination of terms over the following signature is verified: int, true, if1, if2, zero, if_int, tail, if_intlist, 0, s, p, empty, false, intlist, head, cons, nil
Strategy
Instantiation
For all potential predecessors l → r of the rule int
#(
x,
y) → if_int
#(zero(
x), zero(
y),
x,
y) on dependency pair chains it holds that:
- int#(x, y) matches r,
- all variables of int#(x, y) are embedded in constructor contexts, i.e., each subterm of int#(x, y), containing a variable is rooted by a constructor symbol.
Thus, int
#(
x,
y) → if_int
#(zero(
x), zero(
y),
x,
y) is replaced by instances determined through the above matching. These instances are:
| int#(s(0), _y) → if_int#(zero(s(0)), zero(_y), s(0), _y) | int#(p(_x), p(_y)) → if_int#(zero(p(_x)), zero(p(_y)), p(_x), p(_y)) |
Problem 5: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if2#(false, x, y) | → | int#(p(x), p(y)) | | int#(s(0), _y) | → | if_int#(zero(s(0)), zero(_y), s(0), _y) |
| if_int#(true, b, x, y) | → | if1#(b, x, y) | | int#(p(_x), p(_y)) | → | if_int#(zero(p(_x)), zero(p(_y)), p(_x), p(_y)) |
| if1#(false, x, y) | → | int#(s(0), y) | | if_int#(false, b, x, y) | → | if2#(b, x, y) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, y)) | → | false |
| tail(nil) | → | nil | | tail(cons(x, y)) | → | y |
| head(cons(x, y)) | → | x | | zero(0) | → | true |
| zero(s(x)) | → | false | | p(0) | → | 0 |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| intlist(x) | → | if_intlist(empty(x), x) | | if_intlist(true, x) | → | nil |
| if_intlist(false, x) | → | cons(s(head(x)), intlist(tail(x))) | | int(x, y) | → | if_int(zero(x), zero(y), x, y) |
| if_int(true, b, x, y) | → | if1(b, x, y) | | if_int(false, b, x, y) | → | if2(b, x, y) |
| if1(true, x, y) | → | cons(0, nil) | | if1(false, x, y) | → | cons(0, int(s(0), y)) |
| if2(true, x, y) | → | nil | | if2(false, x, y) | → | intlist(int(p(x), p(y))) |
Original Signature
Termination of terms over the following signature is verified: int, true, if1, if2, zero, if_int, tail, if_intlist, 0, s, p, empty, false, intlist, head, nil, cons
Strategy
Instantiation
For all potential successors l → r of the rule if_int
#(true,
b,
x,
y) → if1
#(
b,
x,
y) on dependency pair chains it holds that:
- if1#(b, x, y) matches l,
- all variables of if1#(b, x, y) are embedded in constructor contexts, i.e., each subterm of if1#(b, x, y) containing a variable is rooted by a constructor symbol.
Thus, if_int
#(true,
b,
x,
y) → if1
#(
b,
x,
y) is replaced by instances determined through the above matching. These instances are:
| if_int#(true, false, x, y) → if1#(false, x, y) |
Instantiation
For all potential successors l → r of the rule if_int
#(false,
b,
x,
y) → if2
#(
b,
x,
y) on dependency pair chains it holds that:
- if2#(b, x, y) matches l,
- all variables of if2#(b, x, y) are embedded in constructor contexts, i.e., each subterm of if2#(b, x, y) containing a variable is rooted by a constructor symbol.
Thus, if_int
#(false,
b,
x,
y) → if2
#(
b,
x,
y) is replaced by instances determined through the above matching. These instances are:
| if_int#(false, false, x, y) → if2#(false, x, y) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| int#(s(0), _y) | → | if_int#(zero(s(0)), zero(_y), s(0), _y) | | if2#(false, x, y) | → | int#(p(x), p(y)) |
| int#(p(_x), p(_y)) | → | if_int#(zero(p(_x)), zero(p(_y)), p(_x), p(_y)) | | if1#(false, x, y) | → | int#(s(0), y) |
| if_int#(false, false, x, y) | → | if2#(false, x, y) | | if_int#(true, false, x, y) | → | if1#(false, x, y) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, y)) | → | false |
| tail(nil) | → | nil | | tail(cons(x, y)) | → | y |
| head(cons(x, y)) | → | x | | zero(0) | → | true |
| zero(s(x)) | → | false | | p(0) | → | 0 |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| intlist(x) | → | if_intlist(empty(x), x) | | if_intlist(true, x) | → | nil |
| if_intlist(false, x) | → | cons(s(head(x)), intlist(tail(x))) | | int(x, y) | → | if_int(zero(x), zero(y), x, y) |
| if_int(true, b, x, y) | → | if1(b, x, y) | | if_int(false, b, x, y) | → | if2(b, x, y) |
| if1(true, x, y) | → | cons(0, nil) | | if1(false, x, y) | → | cons(0, int(s(0), y)) |
| if2(true, x, y) | → | nil | | if2(false, x, y) | → | intlist(int(p(x), p(y))) |
Original Signature
Termination of terms over the following signature is verified: int, true, if1, if2, zero, if_int, tail, if_intlist, 0, s, p, empty, false, intlist, head, cons, nil
Strategy
The dependency pairs if_int
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → int
#(p(
x), p(
y)) are consolidated into the rule if_int
#(false, false,
x,
y) → int
#(p(
x), p(
y)) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if_int#(false, false, x, y) and int#(p(x), p(y))
The dependency pairs if_int
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → int
#(p(
x), p(
y)) are consolidated into the rule if_int
#(false, false,
x,
y) → int
#(p(
x), p(
y)) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if_int#(false, false, x, y) and int#(p(x), p(y))
The dependency pairs if_int
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → int
#(p(
x), p(
y)) are consolidated into the rule if_int
#(false, false,
x,
y) → int
#(p(
x), p(
y)) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if_int#(false, false, x, y) and int#(p(x), p(y))
The dependency pairs if_int
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → int
#(p(
x), p(
y)) are consolidated into the rule if_int
#(false, false,
x,
y) → int
#(p(
x), p(
y)) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if_int#(false, false, x, y) and int#(p(x), p(y))
The dependency pairs if_int
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → int
#(p(
x), p(
y)) are consolidated into the rule if_int
#(false, false,
x,
y) → int
#(p(
x), p(
y)) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if_int#(false, false, x, y) and int#(p(x), p(y))
The dependency pairs if_int
#(false, false,
x,
y) → if2
#(false,
x,
y) and if2
#(false,
x,
y) → int
#(p(
x), p(
y)) are consolidated into the rule if_int
#(false, false,
x,
y) → int
#(p(
x), p(
y)) .
This is possible as
- all subterms of if2#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, x, y), but non-replacing in both if_int#(false, false, x, y) and int#(p(x), p(y))
The dependency pairs if_int
#(true, false,
x,
y) → if1
#(false,
x,
y) and if1
#(false,
x,
y) → int
#(s(0),
y) are consolidated into the rule if_int
#(true, false,
x,
y) → int
#(s(0),
y) .
This is possible as
- all subterms of if1#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if1#(false, x, y), but non-replacing in both if_int#(true, false, x, y) and int#(s(0), y)
The dependency pairs if_int
#(true, false,
x,
y) → if1
#(false,
x,
y) and if1
#(false,
x,
y) → int
#(s(0),
y) are consolidated into the rule if_int
#(true, false,
x,
y) → int
#(s(0),
y) .
This is possible as
- all subterms of if1#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if1#(false, x, y), but non-replacing in both if_int#(true, false, x, y) and int#(s(0), y)
The dependency pairs if_int
#(true, false,
x,
y) → if1
#(false,
x,
y) and if1
#(false,
x,
y) → int
#(s(0),
y) are consolidated into the rule if_int
#(true, false,
x,
y) → int
#(s(0),
y) .
This is possible as
- all subterms of if1#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if1#(false, x, y), but non-replacing in both if_int#(true, false, x, y) and int#(s(0), y)
The dependency pairs if_int
#(true, false,
x,
y) → if1
#(false,
x,
y) and if1
#(false,
x,
y) → int
#(s(0),
y) are consolidated into the rule if_int
#(true, false,
x,
y) → int
#(s(0),
y) .
This is possible as
- all subterms of if1#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if1#(false, x, y), but non-replacing in both if_int#(true, false, x, y) and int#(s(0), y)
The dependency pairs if_int
#(true, false,
x,
y) → if1
#(false,
x,
y) and if1
#(false,
x,
y) → int
#(s(0),
y) are consolidated into the rule if_int
#(true, false,
x,
y) → int
#(s(0),
y) .
This is possible as
- all subterms of if1#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if1#(false, x, y), but non-replacing in both if_int#(true, false, x, y) and int#(s(0), y)
The dependency pairs if_int
#(true, false,
x,
y) → if1
#(false,
x,
y) and if1
#(false,
x,
y) → int
#(s(0),
y) are consolidated into the rule if_int
#(true, false,
x,
y) → int
#(s(0),
y) .
This is possible as
- all subterms of if1#(false, x, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if1#(false, x, y), but non-replacing in both if_int#(true, false, x, y) and int#(s(0), y)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| if2#(false, x, y) → int#(p(x), p(y)) | if_int#(false, false, x, y) → int#(p(x), p(y)) |
| if1#(false, x, y) → int#(s(0), y) | if_int#(true, false, x, y) → int#(s(0), y) |
| if_int#(false, false, x, y) → if2#(false, x, y) | |
| if_int#(true, false, x, y) → if1#(false, x, y) | |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| intlist#(x) | → | if_intlist#(empty(x), x) | | if_intlist#(false, x) | → | intlist#(tail(x)) |
Rewrite Rules
| empty(nil) | → | true | | empty(cons(x, y)) | → | false |
| tail(nil) | → | nil | | tail(cons(x, y)) | → | y |
| head(cons(x, y)) | → | x | | zero(0) | → | true |
| zero(s(x)) | → | false | | p(0) | → | 0 |
| p(s(0)) | → | 0 | | p(s(s(x))) | → | s(p(s(x))) |
| intlist(x) | → | if_intlist(empty(x), x) | | if_intlist(true, x) | → | nil |
| if_intlist(false, x) | → | cons(s(head(x)), intlist(tail(x))) | | int(x, y) | → | if_int(zero(x), zero(y), x, y) |
| if_int(true, b, x, y) | → | if1(b, x, y) | | if_int(false, b, x, y) | → | if2(b, x, y) |
| if1(true, x, y) | → | cons(0, nil) | | if1(false, x, y) | → | cons(0, int(s(0), y)) |
| if2(true, x, y) | → | nil | | if2(false, x, y) | → | intlist(int(p(x), p(y))) |
Original Signature
Termination of terms over the following signature is verified: int, true, if1, if2, zero, if_int, tail, if_intlist, 0, s, p, empty, false, intlist, head, cons, nil
Strategy
Instantiation
For all potential predecessors l → r of the rule intlist
#(
x) → if_intlist
#(empty(
x),
x) on dependency pair chains it holds that:
- intlist#(x) matches r,
- all variables of intlist#(x) are embedded in constructor contexts, i.e., each subterm of intlist#(x), containing a variable is rooted by a constructor symbol.
Thus, intlist
#(
x) → if_intlist
#(empty(
x),
x) is replaced by instances determined through the above matching. These instances are:
| intlist#(tail(_x)) → if_intlist#(empty(tail(_x)), tail(_x)) |