NO
The TRS could be proven non-terminating. The proof took 60001 ms.
The following reduction sequence is a witness for non-termination:
isPalListKind# →* isPalListKind#
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1988ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (3ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (87ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (143ms), DependencyGraph (46ms), ReductionPairSAT (49ms), DependencyGraph (4ms), SizeChangePrinciple (8ms)].
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (17ms), PolynomialLinearRange4iUR (169ms), DependencyGraph (10ms), PolynomialLinearRange8NegiUR (1680ms), DependencyGraph (15ms), ReductionPairSAT (397ms), DependencyGraph (11ms), SizeChangePrinciple (21ms)].
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (228ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (162ms), PolynomialLinearRange8NegiUR (10000ms), DependencyGraph (161ms), ReductionPairSAT (7387ms), DependencyGraph (160ms), SizeChangePrinciple (timeout)].
| – Problem 5 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNeList# | → | U41#(isPalListKind) | | U82#(tt) | → | U83#(isNePal) |
| U42#(tt) | → | U43#(isPalListKind) | | U91#(tt) | → | U92#(isPalListKind) |
| isPalListKind# | → | U91#(isPalListKind) | | U31#(tt) | → | U32#(isPalListKind) |
| U54#(tt) | → | isNeList# | | isNePal# | → | isPalListKind# |
| isNePal# | → | U61#(isPalListKind) | | U24#(tt) | → | U25#(isList) |
| U23#(tt) | → | isPalListKind# | | U42#(tt) | → | isPalListKind# |
| U71#(tt) | → | isPalListKind# | | U25#(tt) | → | U26#(isList) |
| U81#(tt) | → | U82#(isPalListKind) | | U73#(tt) | → | U74#(isPalListKind) |
| U71#(tt) | → | U72#(isPalListKind) | | U53#(tt) | → | isPalListKind# |
| U45#(tt) | → | isNeList# | | U41#(tt) | → | isPalListKind# |
| U72#(tt) | → | isPal# | | U72#(tt) | → | U73#(isPal) |
| U32#(tt) | → | U33#(isQid) | | U11#(tt) | → | isPalListKind# |
| U21#(tt) | → | U22#(isPalListKind) | | isNeList# | → | isPalListKind# |
| U44#(tt) | → | U45#(isList) | | isList# | → | U21#(isPalListKind) |
| U12#(tt) | → | U13#(isNeList) | | U22#(tt) | → | U23#(isPalListKind) |
| isPalListKind# | → | isPalListKind# | | U25#(tt) | → | isList# |
| U53#(tt) | → | U54#(isPalListKind) | | U51#(tt) | → | isPalListKind# |
| U54#(tt) | → | U55#(isNeList) | | U81#(tt) | → | isPalListKind# |
| U23#(tt) | → | U24#(isPalListKind) | | U61#(tt) | → | U62#(isPalListKind) |
| U11#(tt) | → | U12#(isPalListKind) | | U43#(tt) | → | U44#(isPalListKind) |
| U44#(tt) | → | isList# | | isList# | → | U11#(isPalListKind) |
| U61#(tt) | → | isPalListKind# | | isNeList# | → | U31#(isPalListKind) |
| __#(__(X, Y), Z) | → | __#(Y, Z) | | U52#(tt) | → | isPalListKind# |
| isNeList# | → | U51#(isPalListKind) | | U45#(tt) | → | U46#(isNeList) |
| U21#(tt) | → | isPalListKind# | | U55#(tt) | → | U56#(isList) |
| U43#(tt) | → | isPalListKind# | | U22#(tt) | → | isPalListKind# |
| isPal# | → | isPalListKind# | | U91#(tt) | → | isPalListKind# |
| U12#(tt) | → | isNeList# | | __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) |
| U55#(tt) | → | isList# | | U62#(tt) | → | U63#(isQid) |
| U32#(tt) | → | isQid# | | U82#(tt) | → | isNePal# |
| U51#(tt) | → | U52#(isPalListKind) | | U41#(tt) | → | U42#(isPalListKind) |
| isPal# | → | U81#(isPalListKind) | | U24#(tt) | → | isList# |
| U73#(tt) | → | isPalListKind# | | isNePal# | → | isQid# |
| U62#(tt) | → | isQid# | | U31#(tt) | → | isPalListKind# |
| U52#(tt) | → | U53#(isPalListKind) | | isList# | → | isPalListKind# |
| isNePal# | → | U71#(isQid) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | U12(isPalListKind) |
| U12(tt) | → | U13(isNeList) | | U13(tt) | → | tt |
| U21(tt) | → | U22(isPalListKind) | | U22(tt) | → | U23(isPalListKind) |
| U23(tt) | → | U24(isPalListKind) | | U24(tt) | → | U25(isList) |
| U25(tt) | → | U26(isList) | | U26(tt) | → | tt |
| U31(tt) | → | U32(isPalListKind) | | U32(tt) | → | U33(isQid) |
| U33(tt) | → | tt | | U41(tt) | → | U42(isPalListKind) |
| U42(tt) | → | U43(isPalListKind) | | U43(tt) | → | U44(isPalListKind) |
| U44(tt) | → | U45(isList) | | U45(tt) | → | U46(isNeList) |
| U46(tt) | → | tt | | U51(tt) | → | U52(isPalListKind) |
| U52(tt) | → | U53(isPalListKind) | | U53(tt) | → | U54(isPalListKind) |
| U54(tt) | → | U55(isNeList) | | U55(tt) | → | U56(isList) |
| U56(tt) | → | tt | | U61(tt) | → | U62(isPalListKind) |
| U62(tt) | → | U63(isQid) | | U63(tt) | → | tt |
| U71(tt) | → | U72(isPalListKind) | | U72(tt) | → | U73(isPal) |
| U73(tt) | → | U74(isPalListKind) | | U74(tt) | → | tt |
| U81(tt) | → | U82(isPalListKind) | | U82(tt) | → | U83(isNePal) |
| U83(tt) | → | tt | | U91(tt) | → | U92(isPalListKind) |
| U92(tt) | → | tt | | isList | → | U11(isPalListKind) |
| isList | → | tt | | isList | → | U21(isPalListKind) |
| isNeList | → | U31(isPalListKind) | | isNeList | → | U41(isPalListKind) |
| isNeList | → | U51(isPalListKind) | | isNePal | → | U61(isPalListKind) |
| isNePal | → | U71(isQid) | | isPal | → | U81(isPalListKind) |
| isPal | → | tt | | isPalListKind | → | tt |
| isPalListKind | → | tt | | isPalListKind | → | tt |
| isPalListKind | → | tt | | isPalListKind | → | tt |
| isPalListKind | → | tt | | isPalListKind | → | U91(isPalListKind) |
| isQid | → | tt | | isQid | → | tt |
| isQid | → | tt | | isQid | → | tt |
| isQid | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U46, U45, U63, U44, U25, U62, U43, U26, U61, U42, U92, U41, U91, isNePal, U23, U24, U21, U22, isPalListKind, U83, isPal, U71, U55, U73, U54, U72, U56, U74, U51, tt, U53, U82, U52, U81, U11, U12, isQid, U31, U13, U32, U33, nil
Strategy
The following SCCs where found
| U81#(tt) → U82#(isPalListKind) | U71#(tt) → U72#(isPalListKind) |
| U82#(tt) → isNePal# | isPal# → U81#(isPalListKind) |
| U72#(tt) → isPal# | isNePal# → U71#(isQid) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
| isPalListKind# → U91#(isPalListKind) | isPalListKind# → isPalListKind# |
| U91#(tt) → isPalListKind# |
| U54#(tt) → U55#(isNeList) | isNeList# → U41#(isPalListKind) |
| U42#(tt) → U43#(isPalListKind) | U12#(tt) → isNeList# |
| U23#(tt) → U24#(isPalListKind) | U11#(tt) → U12#(isPalListKind) |
| U54#(tt) → isNeList# | U21#(tt) → U22#(isPalListKind) |
| U55#(tt) → isList# | U43#(tt) → U44#(isPalListKind) |
| U44#(tt) → isList# | isList# → U11#(isPalListKind) |
| U51#(tt) → U52#(isPalListKind) | U41#(tt) → U42#(isPalListKind) |
| U44#(tt) → U45#(isList) | U24#(tt) → U25#(isList) |
| isList# → U21#(isPalListKind) | isNeList# → U51#(isPalListKind) |
| U24#(tt) → isList# | U22#(tt) → U23#(isPalListKind) |
| U45#(tt) → isNeList# | U52#(tt) → U53#(isPalListKind) |
| U25#(tt) → isList# | U53#(tt) → U54#(isPalListKind) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | U12(isPalListKind) |
| U12(tt) | → | U13(isNeList) | | U13(tt) | → | tt |
| U21(tt) | → | U22(isPalListKind) | | U22(tt) | → | U23(isPalListKind) |
| U23(tt) | → | U24(isPalListKind) | | U24(tt) | → | U25(isList) |
| U25(tt) | → | U26(isList) | | U26(tt) | → | tt |
| U31(tt) | → | U32(isPalListKind) | | U32(tt) | → | U33(isQid) |
| U33(tt) | → | tt | | U41(tt) | → | U42(isPalListKind) |
| U42(tt) | → | U43(isPalListKind) | | U43(tt) | → | U44(isPalListKind) |
| U44(tt) | → | U45(isList) | | U45(tt) | → | U46(isNeList) |
| U46(tt) | → | tt | | U51(tt) | → | U52(isPalListKind) |
| U52(tt) | → | U53(isPalListKind) | | U53(tt) | → | U54(isPalListKind) |
| U54(tt) | → | U55(isNeList) | | U55(tt) | → | U56(isList) |
| U56(tt) | → | tt | | U61(tt) | → | U62(isPalListKind) |
| U62(tt) | → | U63(isQid) | | U63(tt) | → | tt |
| U71(tt) | → | U72(isPalListKind) | | U72(tt) | → | U73(isPal) |
| U73(tt) | → | U74(isPalListKind) | | U74(tt) | → | tt |
| U81(tt) | → | U82(isPalListKind) | | U82(tt) | → | U83(isNePal) |
| U83(tt) | → | tt | | U91(tt) | → | U92(isPalListKind) |
| U92(tt) | → | tt | | isList | → | U11(isPalListKind) |
| isList | → | tt | | isList | → | U21(isPalListKind) |
| isNeList | → | U31(isPalListKind) | | isNeList | → | U41(isPalListKind) |
| isNeList | → | U51(isPalListKind) | | isNePal | → | U61(isPalListKind) |
| isNePal | → | U71(isQid) | | isPal | → | U81(isPalListKind) |
| isPal | → | tt | | isPalListKind | → | tt |
| isPalListKind | → | tt | | isPalListKind | → | tt |
| isPalListKind | → | tt | | isPalListKind | → | tt |
| isPalListKind | → | tt | | isPalListKind | → | U91(isPalListKind) |
| isQid | → | tt | | isQid | → | tt |
| isQid | → | tt | | isQid | → | tt |
| isQid | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U46, U45, U63, U44, U25, U62, U43, U26, U61, U42, U92, U41, U91, isNePal, U23, U24, U21, U22, isPalListKind, U83, isPal, U71, U55, U73, U54, U72, U56, U74, U51, tt, U53, U82, U52, U81, U11, U12, isQid, U31, U13, U32, U33, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |