TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60189 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1174ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (47ms), PolynomialOrderingProcessor (0ms), DependencyGraph (2ms), PolynomialLinearRange4 (488ms), DependencyGraph (2ms), ReductionPairSAT (1632ms), DependencyGraph (0ms), SizeChangePrinciple (timeout)].
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (138ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (219ms), PolynomialOrderingProcessor (15ms), DependencyGraph (136ms), PolynomialLinearRange4 (634ms), DependencyGraph (134ms), ReductionPairSAT (879ms), DependencyGraph (93ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS) | | U81#(tt, N, X, XS) | → | splitAt#(N, XS) |
Rewrite Rules
| U101(tt, N, XS) | → | fst(splitAt(N, XS)) | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U21(tt, X) | → | X | | U31(tt, N) | → | N |
| U41(tt, N) | → | cons(N, natsFrom(s(N))) | | U51(tt, N, XS) | → | head(afterNth(N, XS)) |
| U61(tt, Y) | → | Y | | U71(tt, XS) | → | pair(nil, XS) |
| U81(tt, N, X, XS) | → | U82(splitAt(N, XS), X) | | U82(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U91(tt, XS) | → | XS | | afterNth(N, XS) | → | U11(and(isNatural(N), isLNat(XS)), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(isLNat(X), isLNat(Y)), X) |
| head(cons(N, XS)) | → | U31(and(isNatural(N), isLNat(XS)), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isLNat(cons(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) |
| isLNat(fst(V1)) | → | isPLNat(V1) | | isLNat(natsFrom(V1)) | → | isNatural(V1) |
| isLNat(snd(V1)) | → | isPLNat(V1) | | isLNat(tail(V1)) | → | isLNat(V1) |
| isLNat(take(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | isLNat(V1) | | isNatural(s(V1)) | → | isNatural(V1) |
| isNatural(sel(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isPLNat(pair(V1, V2)) | → | and(isLNat(V1), isLNat(V2)) |
| isPLNat(splitAt(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | natsFrom(N) | → | U41(isNatural(N), N) |
| sel(N, XS) | → | U51(and(isNatural(N), isLNat(XS)), N, XS) | | snd(pair(X, Y)) | → | U61(and(isLNat(X), isLNat(Y)), Y) |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS) |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), isLNat(XS)), XS) | | take(N, XS) | → | U101(and(isNatural(N), isLNat(XS)), N, XS) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, isNatural, fst, U61, U41, U91, head, U21, cons, snd, isPLNat, tail, splitAt, U71, and, 0, U51, s, tt, take, U82, U81, isLNat, U11, U31, afterNth, sel, U101, nil
Open Dependency Pair Problem 3
Dependency Pairs
| isLNat#(cons(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) | | isLNat#(fst(V1)) | → | isPLNat#(V1) |
| T(isLNat(V2)) | → | isLNat#(V2) | | isNatural#(head(V1)) | → | isLNat#(V1) |
| isLNat#(afterNth(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) | | isNatural#(sel(V1, V2)) | → | isNatural#(V1) |
| isPLNat#(splitAt(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) | | T(and(x_1, x_2)) | → | T(x_1) |
| isLNat#(natsFrom(V1)) | → | isNatural#(V1) | | T(isNatural(X)) | → | isNatural#(X) |
| isLNat#(cons(V1, V2)) | → | isNatural#(V1) | | isNatural#(sel(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) |
| isLNat#(afterNth(V1, V2)) | → | isNatural#(V1) | | T(s(x_1)) | → | T(x_1) |
| isNatural#(s(V1)) | → | isNatural#(V1) | | isLNat#(take(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) |
| isLNat#(take(V1, V2)) | → | isNatural#(V1) | | T(isLNat(x_1)) | → | T(x_1) |
| isPLNat#(pair(V1, V2)) | → | isLNat#(V1) | | T(natsFrom(x_1)) | → | T(x_1) |
| and#(tt, X) | → | T(X) | | isPLNat#(pair(V1, V2)) | → | and#(isLNat(V1), isLNat(V2)) |
| natsFrom#(N) | → | U41#(isNatural(N), N) | | isLNat#(snd(V1)) | → | isPLNat#(V1) |
| natsFrom#(N) | → | isNatural#(N) | | T(natsFrom(s(N))) | → | natsFrom#(s(N)) |
| isLNat#(tail(V1)) | → | isLNat#(V1) | | T(and(isNatural(X), isLNat(XS))) | → | and#(isNatural(X), isLNat(XS)) |
| T(isNatural(x_1)) | → | T(x_1) | | isPLNat#(splitAt(V1, V2)) | → | isNatural#(V1) |
| T(and(x_1, x_2)) | → | T(x_2) | | U41#(tt, N) | → | T(N) |
| T(isLNat(XS)) | → | isLNat#(XS) | | T(isLNat(Y)) | → | isLNat#(Y) |
Rewrite Rules
| U101(tt, N, XS) | → | fst(splitAt(N, XS)) | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U21(tt, X) | → | X | | U31(tt, N) | → | N |
| U41(tt, N) | → | cons(N, natsFrom(s(N))) | | U51(tt, N, XS) | → | head(afterNth(N, XS)) |
| U61(tt, Y) | → | Y | | U71(tt, XS) | → | pair(nil, XS) |
| U81(tt, N, X, XS) | → | U82(splitAt(N, XS), X) | | U82(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U91(tt, XS) | → | XS | | afterNth(N, XS) | → | U11(and(isNatural(N), isLNat(XS)), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(isLNat(X), isLNat(Y)), X) |
| head(cons(N, XS)) | → | U31(and(isNatural(N), isLNat(XS)), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isLNat(cons(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) |
| isLNat(fst(V1)) | → | isPLNat(V1) | | isLNat(natsFrom(V1)) | → | isNatural(V1) |
| isLNat(snd(V1)) | → | isPLNat(V1) | | isLNat(tail(V1)) | → | isLNat(V1) |
| isLNat(take(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | isLNat(V1) | | isNatural(s(V1)) | → | isNatural(V1) |
| isNatural(sel(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isPLNat(pair(V1, V2)) | → | and(isLNat(V1), isLNat(V2)) |
| isPLNat(splitAt(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | natsFrom(N) | → | U41(isNatural(N), N) |
| sel(N, XS) | → | U51(and(isNatural(N), isLNat(XS)), N, XS) | | snd(pair(X, Y)) | → | U61(and(isLNat(X), isLNat(Y)), Y) |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS) |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), isLNat(XS)), XS) | | take(N, XS) | → | U101(and(isNatural(N), isLNat(XS)), N, XS) |
Original Signature
Termination of terms over the following signature is verified: pair, natsFrom, isNatural, fst, U61, U41, U91, head, U21, cons, snd, isPLNat, tail, splitAt, U71, and, 0, U51, s, tt, take, U82, U81, isLNat, U11, U31, afterNth, sel, U101, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | | splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS) |
| isLNat#(cons(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) | | sel#(N, XS) | → | and#(isNatural(N), isLNat(XS)) |
| U81#(tt, N, X, XS) | → | U82#(splitAt(N, XS), X) | | isNatural#(head(V1)) | → | isLNat#(V1) |
| take#(N, XS) | → | and#(isNatural(N), isLNat(XS)) | | U11#(tt, N, XS) | → | splitAt#(N, XS) |
| isLNat#(afterNth(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) | | T(and(x_1, x_2)) | → | T(x_1) |
| isPLNat#(splitAt(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) | | afterNth#(N, XS) | → | and#(isNatural(N), isLNat(XS)) |
| tail#(cons(N, XS)) | → | isNatural#(N) | | U101#(tt, N, XS) | → | splitAt#(N, XS) |
| isLNat#(natsFrom(V1)) | → | isNatural#(V1) | | T(isNatural(X)) | → | isNatural#(X) |
| isLNat#(cons(V1, V2)) | → | isNatural#(V1) | | U11#(tt, N, XS) | → | T(N) |
| isLNat#(afterNth(V1, V2)) | → | isNatural#(V1) | | U51#(tt, N, XS) | → | T(N) |
| head#(cons(N, XS)) | → | isNatural#(N) | | T(s(x_1)) | → | T(x_1) |
| isNatural#(s(V1)) | → | isNatural#(V1) | | U71#(tt, XS) | → | T(XS) |
| isLNat#(take(V1, V2)) | → | isNatural#(V1) | | snd#(pair(X, Y)) | → | isLNat#(X) |
| U61#(tt, Y) | → | T(Y) | | splitAt#(0, XS) | → | isLNat#(XS) |
| and#(tt, X) | → | T(X) | | isPLNat#(pair(V1, V2)) | → | and#(isLNat(V1), isLNat(V2)) |
| isLNat#(snd(V1)) | → | isPLNat#(V1) | | natsFrom#(N) | → | isNatural#(N) |
| U51#(tt, N, XS) | → | head#(afterNth(N, XS)) | | T(natsFrom(s(N))) | → | natsFrom#(s(N)) |
| splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), and(isNatural(X), isLNat(XS))) | | isLNat#(tail(V1)) | → | isLNat#(V1) |
| U51#(tt, N, XS) | → | afterNth#(N, XS) | | fst#(pair(X, Y)) | → | and#(isLNat(X), isLNat(Y)) |
| U101#(tt, N, XS) | → | T(N) | | T(isNatural(x_1)) | → | T(x_1) |
| T(and(x_1, x_2)) | → | T(x_2) | | sel#(N, XS) | → | U51#(and(isNatural(N), isLNat(XS)), N, XS) |
| U41#(tt, N) | → | T(N) | | T(isLNat(Y)) | → | isLNat#(Y) |
| fst#(pair(X, Y)) | → | U21#(and(isLNat(X), isLNat(Y)), X) | | fst#(pair(X, Y)) | → | isLNat#(X) |
| tail#(cons(N, XS)) | → | and#(isNatural(N), isLNat(XS)) | | sel#(N, XS) | → | isNatural#(N) |
| isLNat#(fst(V1)) | → | isPLNat#(V1) | | T(isLNat(V2)) | → | isLNat#(V2) |
| isNatural#(sel(V1, V2)) | → | isNatural#(V1) | | take#(N, XS) | → | isNatural#(N) |
| U81#(tt, N, X, XS) | → | T(XS) | | U101#(tt, N, XS) | → | T(XS) |
| splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | | head#(cons(N, XS)) | → | U31#(and(isNatural(N), isLNat(XS)), N) |
| isNatural#(sel(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) | | snd#(pair(X, Y)) | → | U61#(and(isLNat(X), isLNat(Y)), Y) |
| head#(cons(N, XS)) | → | and#(isNatural(N), isLNat(XS)) | | U11#(tt, N, XS) | → | T(XS) |
| isLNat#(take(V1, V2)) | → | and#(isNatural(V1), isLNat(V2)) | | afterNth#(N, XS) | → | isNatural#(N) |
| T(isLNat(x_1)) | → | T(x_1) | | isPLNat#(pair(V1, V2)) | → | isLNat#(V1) |
| U31#(tt, N) | → | T(N) | | T(natsFrom(x_1)) | → | T(x_1) |
| natsFrom#(N) | → | U41#(isNatural(N), N) | | U91#(tt, XS) | → | T(XS) |
| afterNth#(N, XS) | → | U11#(and(isNatural(N), isLNat(XS)), N, XS) | | U21#(tt, X) | → | T(X) |
| U51#(tt, N, XS) | → | T(XS) | | U81#(tt, N, X, XS) | → | splitAt#(N, XS) |
| snd#(pair(X, Y)) | → | and#(isLNat(X), isLNat(Y)) | | T(and(isNatural(X), isLNat(XS))) | → | and#(isNatural(X), isLNat(XS)) |
| U11#(tt, N, XS) | → | snd#(splitAt(N, XS)) | | U82#(pair(YS, ZS), X) | → | T(X) |
| isPLNat#(splitAt(V1, V2)) | → | isNatural#(V1) | | U101#(tt, N, XS) | → | fst#(splitAt(N, XS)) |
| U81#(tt, N, X, XS) | → | T(N) | | take#(N, XS) | → | U101#(and(isNatural(N), isLNat(XS)), N, XS) |
| T(isLNat(XS)) | → | isLNat#(XS) | | tail#(cons(N, XS)) | → | U91#(and(isNatural(N), isLNat(XS)), XS) |
Rewrite Rules
| U101(tt, N, XS) | → | fst(splitAt(N, XS)) | | U11(tt, N, XS) | → | snd(splitAt(N, XS)) |
| U21(tt, X) | → | X | | U31(tt, N) | → | N |
| U41(tt, N) | → | cons(N, natsFrom(s(N))) | | U51(tt, N, XS) | → | head(afterNth(N, XS)) |
| U61(tt, Y) | → | Y | | U71(tt, XS) | → | pair(nil, XS) |
| U81(tt, N, X, XS) | → | U82(splitAt(N, XS), X) | | U82(pair(YS, ZS), X) | → | pair(cons(X, YS), ZS) |
| U91(tt, XS) | → | XS | | afterNth(N, XS) | → | U11(and(isNatural(N), isLNat(XS)), N, XS) |
| and(tt, X) | → | X | | fst(pair(X, Y)) | → | U21(and(isLNat(X), isLNat(Y)), X) |
| head(cons(N, XS)) | → | U31(and(isNatural(N), isLNat(XS)), N) | | isLNat(nil) | → | tt |
| isLNat(afterNth(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isLNat(cons(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) |
| isLNat(fst(V1)) | → | isPLNat(V1) | | isLNat(natsFrom(V1)) | → | isNatural(V1) |
| isLNat(snd(V1)) | → | isPLNat(V1) | | isLNat(tail(V1)) | → | isLNat(V1) |
| isLNat(take(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isNatural(0) | → | tt |
| isNatural(head(V1)) | → | isLNat(V1) | | isNatural(s(V1)) | → | isNatural(V1) |
| isNatural(sel(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | isPLNat(pair(V1, V2)) | → | and(isLNat(V1), isLNat(V2)) |
| isPLNat(splitAt(V1, V2)) | → | and(isNatural(V1), isLNat(V2)) | | natsFrom(N) | → | U41(isNatural(N), N) |
| sel(N, XS) | → | U51(and(isNatural(N), isLNat(XS)), N, XS) | | snd(pair(X, Y)) | → | U61(and(isLNat(X), isLNat(Y)), Y) |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS) |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), isLNat(XS)), XS) | | take(N, XS) | → | U101(and(isNatural(N), isLNat(XS)), N, XS) |
Original Signature
Termination of terms over the following signature is verified: pair, isNatural, natsFrom, fst, U61, U41, U91, head, U21, snd, cons, isPLNat, tail, splitAt, U71, and, 0, U51, s, tt, take, U82, U81, isLNat, U11, afterNth, U31, sel, nil, U101
Strategy
Context-sensitive strategy:
μ(isNatural#) = μ(isPLNat) = μ(0) = μ(isLNat) = μ(isLNat#) = μ(isNatural) = μ(T) = μ(tt) = μ(isPLNat#) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(natsFrom) = μ(U21#) = μ(tail#) = μ(fst) = μ(U41#) = μ(U61) = μ(snd#) = μ(head) = μ(U21) = μ(U61#) = μ(U51#) = μ(tail) = μ(and) = μ(U71) = μ(U71#) = μ(U31) = μ(U91#) = μ(U81#) = μ(and#) = μ(U41) = μ(U91) = μ(cons) = μ(snd) = μ(U101#) = μ(U82#) = μ(U51) = μ(s) = μ(U82) = μ(U81) = μ(U11) = μ(head#) = μ(U101) = {1}
μ(sel#) = μ(take#) = μ(splitAt#) = μ(pair) = μ(splitAt) = μ(afterNth#) = μ(take) = μ(afterNth) = μ(sel) = {1, 2}
The following SCCs where found
| splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS) | U81#(tt, N, X, XS) → splitAt#(N, XS) |
| isLNat#(cons(V1, V2)) → and#(isNatural(V1), isLNat(V2)) | T(isLNat(V2)) → isLNat#(V2) |
| isLNat#(fst(V1)) → isPLNat#(V1) | isNatural#(head(V1)) → isLNat#(V1) |
| isNatural#(sel(V1, V2)) → isNatural#(V1) | isLNat#(afterNth(V1, V2)) → and#(isNatural(V1), isLNat(V2)) |
| T(and(x_1, x_2)) → T(x_1) | isPLNat#(splitAt(V1, V2)) → and#(isNatural(V1), isLNat(V2)) |
| T(isNatural(X)) → isNatural#(X) | isLNat#(natsFrom(V1)) → isNatural#(V1) |
| isLNat#(cons(V1, V2)) → isNatural#(V1) | isLNat#(afterNth(V1, V2)) → isNatural#(V1) |
| isNatural#(sel(V1, V2)) → and#(isNatural(V1), isLNat(V2)) | T(s(x_1)) → T(x_1) |
| isNatural#(s(V1)) → isNatural#(V1) | isLNat#(take(V1, V2)) → and#(isNatural(V1), isLNat(V2)) |
| T(isLNat(x_1)) → T(x_1) | isLNat#(take(V1, V2)) → isNatural#(V1) |
| isPLNat#(pair(V1, V2)) → isLNat#(V1) | and#(tt, X) → T(X) |
| T(natsFrom(x_1)) → T(x_1) | natsFrom#(N) → U41#(isNatural(N), N) |
| isPLNat#(pair(V1, V2)) → and#(isLNat(V1), isLNat(V2)) | isLNat#(snd(V1)) → isPLNat#(V1) |
| natsFrom#(N) → isNatural#(N) | T(natsFrom(s(N))) → natsFrom#(s(N)) |
| isLNat#(tail(V1)) → isLNat#(V1) | T(and(isNatural(X), isLNat(XS))) → and#(isNatural(X), isLNat(XS)) |
| T(isNatural(x_1)) → T(x_1) | T(and(x_1, x_2)) → T(x_2) |
| isPLNat#(splitAt(V1, V2)) → isNatural#(V1) | U41#(tt, N) → T(N) |
| T(isLNat(XS)) → isLNat#(XS) | T(isLNat(Y)) → isLNat#(Y) |