TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (157ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (321ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (8154ms), DependencyGraph (2ms), ReductionPairSAT (14695ms), DependencyGraph (3ms), SizeChangePrinciple (69ms)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (1073ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (7866ms), DependencyGraph (25ms), ReductionPairSAT (2671ms), DependencyGraph (2ms), SizeChangePrinciple (timeout)].
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (0ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| if#(false, x, y, z) | → | loop#(x, double(y), s(z)) | | loop#(x, s(y), z) | → | if#(le(x, s(y)), x, s(y), z) |
Rewrite Rules
| le(s(x), 0) | → | false | | le(0, y) | → | true |
| le(s(x), s(y)) | → | le(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | log(0) | → | logError |
| log(s(x)) | → | loop(s(x), s(0), 0) | | loop(x, s(y), z) | → | if(le(x, s(y)), x, s(y), z) |
| if(true, x, y, z) | → | z | | if(false, x, y, z) | → | loop(x, double(y), s(z)) |
| maplog(xs) | → | mapIter(xs, nil) | | mapIter(xs, ys) | → | ifmap(isempty(xs), xs, ys) |
| ifmap(true, xs, ys) | → | ys | | ifmap(false, xs, ys) | → | mapIter(droplast(xs), cons(log(last(xs)), ys)) |
| isempty(nil) | → | true | | isempty(cons(x, xs)) | → | false |
| last(nil) | → | error | | last(cons(x, nil)) | → | x |
| last(cons(x, cons(y, xs))) | → | last(cons(y, xs)) | | droplast(nil) | → | nil |
| droplast(cons(x, nil)) | → | nil | | droplast(cons(x, cons(y, xs))) | → | cons(x, droplast(cons(y, xs))) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: b, error, last, c, a, ifmap, true, logError, double, log, 0, mapIter, le, s, isempty, if, loop, false, droplast, cons, nil, maplog
Open Dependency Pair Problem 4
Dependency Pairs
| mapIter#(xs, ys) | → | ifmap#(isempty(xs), xs, ys) | | ifmap#(false, xs, ys) | → | mapIter#(droplast(xs), cons(log(last(xs)), ys)) |
Rewrite Rules
| le(s(x), 0) | → | false | | le(0, y) | → | true |
| le(s(x), s(y)) | → | le(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | log(0) | → | logError |
| log(s(x)) | → | loop(s(x), s(0), 0) | | loop(x, s(y), z) | → | if(le(x, s(y)), x, s(y), z) |
| if(true, x, y, z) | → | z | | if(false, x, y, z) | → | loop(x, double(y), s(z)) |
| maplog(xs) | → | mapIter(xs, nil) | | mapIter(xs, ys) | → | ifmap(isempty(xs), xs, ys) |
| ifmap(true, xs, ys) | → | ys | | ifmap(false, xs, ys) | → | mapIter(droplast(xs), cons(log(last(xs)), ys)) |
| isempty(nil) | → | true | | isempty(cons(x, xs)) | → | false |
| last(nil) | → | error | | last(cons(x, nil)) | → | x |
| last(cons(x, cons(y, xs))) | → | last(cons(y, xs)) | | droplast(nil) | → | nil |
| droplast(cons(x, nil)) | → | nil | | droplast(cons(x, cons(y, xs))) | → | cons(x, droplast(cons(y, xs))) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: b, error, last, c, a, ifmap, true, logError, double, log, 0, mapIter, le, s, isempty, if, loop, false, droplast, cons, nil, maplog
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| last#(cons(x, cons(y, xs))) | → | last#(cons(y, xs)) | | log#(s(x)) | → | loop#(s(x), s(0), 0) |
| droplast#(cons(x, cons(y, xs))) | → | droplast#(cons(y, xs)) | | ifmap#(false, xs, ys) | → | mapIter#(droplast(xs), cons(log(last(xs)), ys)) |
| loop#(x, s(y), z) | → | if#(le(x, s(y)), x, s(y), z) | | ifmap#(false, xs, ys) | → | last#(xs) |
| ifmap#(false, xs, ys) | → | droplast#(xs) | | le#(s(x), s(y)) | → | le#(x, y) |
| if#(false, x, y, z) | → | loop#(x, double(y), s(z)) | | mapIter#(xs, ys) | → | ifmap#(isempty(xs), xs, ys) |
| double#(s(x)) | → | double#(x) | | maplog#(xs) | → | mapIter#(xs, nil) |
| ifmap#(false, xs, ys) | → | log#(last(xs)) | | if#(false, x, y, z) | → | double#(y) |
| mapIter#(xs, ys) | → | isempty#(xs) | | loop#(x, s(y), z) | → | le#(x, s(y)) |
Rewrite Rules
| le(s(x), 0) | → | false | | le(0, y) | → | true |
| le(s(x), s(y)) | → | le(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | log(0) | → | logError |
| log(s(x)) | → | loop(s(x), s(0), 0) | | loop(x, s(y), z) | → | if(le(x, s(y)), x, s(y), z) |
| if(true, x, y, z) | → | z | | if(false, x, y, z) | → | loop(x, double(y), s(z)) |
| maplog(xs) | → | mapIter(xs, nil) | | mapIter(xs, ys) | → | ifmap(isempty(xs), xs, ys) |
| ifmap(true, xs, ys) | → | ys | | ifmap(false, xs, ys) | → | mapIter(droplast(xs), cons(log(last(xs)), ys)) |
| isempty(nil) | → | true | | isempty(cons(x, xs)) | → | false |
| last(nil) | → | error | | last(cons(x, nil)) | → | x |
| last(cons(x, cons(y, xs))) | → | last(cons(y, xs)) | | droplast(nil) | → | nil |
| droplast(cons(x, nil)) | → | nil | | droplast(cons(x, cons(y, xs))) | → | cons(x, droplast(cons(y, xs))) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: b, error, last, c, a, ifmap, true, logError, double, log, 0, mapIter, s, le, isempty, if, loop, false, droplast, maplog, nil, cons
Strategy
The following SCCs where found
| last#(cons(x, cons(y, xs))) → last#(cons(y, xs)) |
| le#(s(x), s(y)) → le#(x, y) |
| if#(false, x, y, z) → loop#(x, double(y), s(z)) | loop#(x, s(y), z) → if#(le(x, s(y)), x, s(y), z) |
| droplast#(cons(x, cons(y, xs))) → droplast#(cons(y, xs)) |
| double#(s(x)) → double#(x) |
| mapIter#(xs, ys) → ifmap#(isempty(xs), xs, ys) | ifmap#(false, xs, ys) → mapIter#(droplast(xs), cons(log(last(xs)), ys)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| last#(cons(x, cons(y, xs))) | → | last#(cons(y, xs)) |
Rewrite Rules
| le(s(x), 0) | → | false | | le(0, y) | → | true |
| le(s(x), s(y)) | → | le(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | log(0) | → | logError |
| log(s(x)) | → | loop(s(x), s(0), 0) | | loop(x, s(y), z) | → | if(le(x, s(y)), x, s(y), z) |
| if(true, x, y, z) | → | z | | if(false, x, y, z) | → | loop(x, double(y), s(z)) |
| maplog(xs) | → | mapIter(xs, nil) | | mapIter(xs, ys) | → | ifmap(isempty(xs), xs, ys) |
| ifmap(true, xs, ys) | → | ys | | ifmap(false, xs, ys) | → | mapIter(droplast(xs), cons(log(last(xs)), ys)) |
| isempty(nil) | → | true | | isempty(cons(x, xs)) | → | false |
| last(nil) | → | error | | last(cons(x, nil)) | → | x |
| last(cons(x, cons(y, xs))) | → | last(cons(y, xs)) | | droplast(nil) | → | nil |
| droplast(cons(x, nil)) | → | nil | | droplast(cons(x, cons(y, xs))) | → | cons(x, droplast(cons(y, xs))) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: b, error, last, c, a, ifmap, true, logError, double, log, 0, mapIter, s, le, isempty, if, loop, false, droplast, maplog, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| last#(cons(x, cons(y, xs))) | → | last#(cons(y, xs)) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| droplast#(cons(x, cons(y, xs))) | → | droplast#(cons(y, xs)) |
Rewrite Rules
| le(s(x), 0) | → | false | | le(0, y) | → | true |
| le(s(x), s(y)) | → | le(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | log(0) | → | logError |
| log(s(x)) | → | loop(s(x), s(0), 0) | | loop(x, s(y), z) | → | if(le(x, s(y)), x, s(y), z) |
| if(true, x, y, z) | → | z | | if(false, x, y, z) | → | loop(x, double(y), s(z)) |
| maplog(xs) | → | mapIter(xs, nil) | | mapIter(xs, ys) | → | ifmap(isempty(xs), xs, ys) |
| ifmap(true, xs, ys) | → | ys | | ifmap(false, xs, ys) | → | mapIter(droplast(xs), cons(log(last(xs)), ys)) |
| isempty(nil) | → | true | | isempty(cons(x, xs)) | → | false |
| last(nil) | → | error | | last(cons(x, nil)) | → | x |
| last(cons(x, cons(y, xs))) | → | last(cons(y, xs)) | | droplast(nil) | → | nil |
| droplast(cons(x, nil)) | → | nil | | droplast(cons(x, cons(y, xs))) | → | cons(x, droplast(cons(y, xs))) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: b, error, last, c, a, ifmap, true, logError, double, log, 0, mapIter, s, le, isempty, if, loop, false, droplast, maplog, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| droplast#(cons(x, cons(y, xs))) | → | droplast#(cons(y, xs)) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(x), s(y)) | → | le#(x, y) |
Rewrite Rules
| le(s(x), 0) | → | false | | le(0, y) | → | true |
| le(s(x), s(y)) | → | le(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | log(0) | → | logError |
| log(s(x)) | → | loop(s(x), s(0), 0) | | loop(x, s(y), z) | → | if(le(x, s(y)), x, s(y), z) |
| if(true, x, y, z) | → | z | | if(false, x, y, z) | → | loop(x, double(y), s(z)) |
| maplog(xs) | → | mapIter(xs, nil) | | mapIter(xs, ys) | → | ifmap(isempty(xs), xs, ys) |
| ifmap(true, xs, ys) | → | ys | | ifmap(false, xs, ys) | → | mapIter(droplast(xs), cons(log(last(xs)), ys)) |
| isempty(nil) | → | true | | isempty(cons(x, xs)) | → | false |
| last(nil) | → | error | | last(cons(x, nil)) | → | x |
| last(cons(x, cons(y, xs))) | → | last(cons(y, xs)) | | droplast(nil) | → | nil |
| droplast(cons(x, nil)) | → | nil | | droplast(cons(x, cons(y, xs))) | → | cons(x, droplast(cons(y, xs))) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: b, error, last, c, a, ifmap, true, logError, double, log, 0, mapIter, s, le, isempty, if, loop, false, droplast, maplog, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(x), s(y)) | → | le#(x, y) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| double#(s(x)) | → | double#(x) |
Rewrite Rules
| le(s(x), 0) | → | false | | le(0, y) | → | true |
| le(s(x), s(y)) | → | le(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | log(0) | → | logError |
| log(s(x)) | → | loop(s(x), s(0), 0) | | loop(x, s(y), z) | → | if(le(x, s(y)), x, s(y), z) |
| if(true, x, y, z) | → | z | | if(false, x, y, z) | → | loop(x, double(y), s(z)) |
| maplog(xs) | → | mapIter(xs, nil) | | mapIter(xs, ys) | → | ifmap(isempty(xs), xs, ys) |
| ifmap(true, xs, ys) | → | ys | | ifmap(false, xs, ys) | → | mapIter(droplast(xs), cons(log(last(xs)), ys)) |
| isempty(nil) | → | true | | isempty(cons(x, xs)) | → | false |
| last(nil) | → | error | | last(cons(x, nil)) | → | x |
| last(cons(x, cons(y, xs))) | → | last(cons(y, xs)) | | droplast(nil) | → | nil |
| droplast(cons(x, nil)) | → | nil | | droplast(cons(x, cons(y, xs))) | → | cons(x, droplast(cons(y, xs))) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: b, error, last, c, a, ifmap, true, logError, double, log, 0, mapIter, s, le, isempty, if, loop, false, droplast, maplog, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| double#(s(x)) | → | double#(x) |