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 (293ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
| – Problem 6 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (14ms), PolynomialLinearRange4iUR (6509ms), DependencyGraph (9ms), PolynomialLinearRange8NegiUR (30000ms), DependencyGraph (timeout), ReductionPairSAT (6363ms), DependencyGraph (9ms), SizeChangePrinciple (timeout)].
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (2ms).
The following open problems remain:
Open Dependency Pair Problem 6
Dependency Pairs
| if1#(store, m, false) | → | if3#(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) | | if2#(store, m, false) | → | process#(app(map_f(self, nil), sndsplit(m, store)), m) |
| if1#(store, m, true) | → | if2#(store, m, empty(fstsplit(m, store))) | | process#(store, m) | → | if1#(store, m, leq(m, length(store))) |
| if3#(store, m, false) | → | process#(sndsplit(m, app(map_f(self, nil), store)), m) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | if1(store, m, leq(m, length(store))) |
| if1(store, m, true) | → | if2(store, m, empty(fstsplit(m, store))) | | if1(store, m, false) | → | if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if2(store, m, false) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) | | if3(store, m, false) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, if3, true, self, if1, if2, process, fstsplit, 0, s, sndsplit, empty, length, false, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| process#(store, m) | → | leq#(m, length(store)) | | if2#(store, m, false) | → | map_f#(self, nil) |
| leq#(s(n), s(m)) | → | leq#(n, m) | | if3#(store, m, false) | → | app#(map_f(self, nil), store) |
| if3#(store, m, false) | → | sndsplit#(m, app(map_f(self, nil), store)) | | if1#(store, m, true) | → | fstsplit#(m, store) |
| length#(cons(h, t)) | → | length#(t) | | if3#(store, m, false) | → | map_f#(self, nil) |
| process#(store, m) | → | if1#(store, m, leq(m, length(store))) | | if3#(store, m, false) | → | process#(sndsplit(m, app(map_f(self, nil), store)), m) |
| if1#(store, m, false) | → | empty#(fstsplit(m, app(map_f(self, nil), store))) | | if1#(store, m, false) | → | if3#(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if1#(store, m, false) | → | app#(map_f(self, nil), store) | | process#(store, m) | → | length#(store) |
| fstsplit#(s(n), cons(h, t)) | → | fstsplit#(n, t) | | if1#(store, m, false) | → | fstsplit#(m, app(map_f(self, nil), store)) |
| map_f#(pid, cons(h, t)) | → | app#(f(pid, h), map_f(pid, t)) | | if2#(store, m, false) | → | sndsplit#(m, store) |
| if1#(store, m, true) | → | empty#(fstsplit(m, store)) | | if2#(store, m, false) | → | process#(app(map_f(self, nil), sndsplit(m, store)), m) |
| if1#(store, m, true) | → | if2#(store, m, empty(fstsplit(m, store))) | | app#(cons(h, t), x) | → | app#(t, x) |
| if2#(store, m, false) | → | app#(map_f(self, nil), sndsplit(m, store)) | | sndsplit#(s(n), cons(h, t)) | → | sndsplit#(n, t) |
| if1#(store, m, false) | → | map_f#(self, nil) | | map_f#(pid, cons(h, t)) | → | map_f#(pid, t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | if1(store, m, leq(m, length(store))) |
| if1(store, m, true) | → | if2(store, m, empty(fstsplit(m, store))) | | if1(store, m, false) | → | if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if2(store, m, false) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) | | if3(store, m, false) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, if3, true, self, if1, if2, process, fstsplit, 0, s, sndsplit, length, empty, false, cons, nil
Strategy
The following SCCs where found
| length#(cons(h, t)) → length#(t) |
| fstsplit#(s(n), cons(h, t)) → fstsplit#(n, t) |
| app#(cons(h, t), x) → app#(t, x) |
| leq#(s(n), s(m)) → leq#(n, m) |
| if1#(store, m, false) → if3#(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) | if2#(store, m, false) → process#(app(map_f(self, nil), sndsplit(m, store)), m) |
| if1#(store, m, true) → if2#(store, m, empty(fstsplit(m, store))) | process#(store, m) → if1#(store, m, leq(m, length(store))) |
| if3#(store, m, false) → process#(sndsplit(m, app(map_f(self, nil), store)), m) |
| sndsplit#(s(n), cons(h, t)) → sndsplit#(n, t) |
| map_f#(pid, cons(h, t)) → map_f#(pid, t) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sndsplit#(s(n), cons(h, t)) | → | sndsplit#(n, t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | if1(store, m, leq(m, length(store))) |
| if1(store, m, true) | → | if2(store, m, empty(fstsplit(m, store))) | | if1(store, m, false) | → | if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if2(store, m, false) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) | | if3(store, m, false) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, if3, true, self, if1, if2, process, fstsplit, 0, s, sndsplit, length, empty, false, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sndsplit#(s(n), cons(h, t)) | → | sndsplit#(n, t) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| app#(cons(h, t), x) | → | app#(t, x) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | if1(store, m, leq(m, length(store))) |
| if1(store, m, true) | → | if2(store, m, empty(fstsplit(m, store))) | | if1(store, m, false) | → | if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if2(store, m, false) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) | | if3(store, m, false) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, if3, true, self, if1, if2, process, fstsplit, 0, s, sndsplit, length, empty, false, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| app#(cons(h, t), x) | → | app#(t, x) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(cons(h, t)) | → | length#(t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | if1(store, m, leq(m, length(store))) |
| if1(store, m, true) | → | if2(store, m, empty(fstsplit(m, store))) | | if1(store, m, false) | → | if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if2(store, m, false) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) | | if3(store, m, false) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, if3, true, self, if1, if2, process, fstsplit, 0, s, sndsplit, length, empty, false, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| length#(cons(h, t)) | → | length#(t) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| fstsplit#(s(n), cons(h, t)) | → | fstsplit#(n, t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | if1(store, m, leq(m, length(store))) |
| if1(store, m, true) | → | if2(store, m, empty(fstsplit(m, store))) | | if1(store, m, false) | → | if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if2(store, m, false) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) | | if3(store, m, false) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, if3, true, self, if1, if2, process, fstsplit, 0, s, sndsplit, length, empty, false, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| fstsplit#(s(n), cons(h, t)) | → | fstsplit#(n, t) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| leq#(s(n), s(m)) | → | leq#(n, m) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | if1(store, m, leq(m, length(store))) |
| if1(store, m, true) | → | if2(store, m, empty(fstsplit(m, store))) | | if1(store, m, false) | → | if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if2(store, m, false) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) | | if3(store, m, false) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, if3, true, self, if1, if2, process, fstsplit, 0, s, sndsplit, length, empty, false, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| leq#(s(n), s(m)) | → | leq#(n, m) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| map_f#(pid, cons(h, t)) | → | map_f#(pid, t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | if1(store, m, leq(m, length(store))) |
| if1(store, m, true) | → | if2(store, m, empty(fstsplit(m, store))) | | if1(store, m, false) | → | if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store)))) |
| if2(store, m, false) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) | | if3(store, m, false) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, if3, true, self, if1, if2, process, fstsplit, 0, s, sndsplit, length, empty, false, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| map_f#(pid, cons(h, t)) | → | map_f#(pid, t) |