Termination w.r.t. Q of the given QTRS could be disproven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x₁)) = x₁   
POL(U21(x₁)) = 2·x₁   
POL(U22(x₁)) = x₁   
POL(U31(x₁)) = 2·x₁   
POL(U41(x₁)) = x₁   
POL(U42(x₁)) = x₁   
POL(U51(x₁)) = x₁   
POL(U52(x₁)) = 2·x₁   
POL(U61(x₁)) = 2·x₁   
POL(U71(x₁)) = 2·x₁   
POL(U72(x₁)) = x₁   
POL(U81(x₁)) = 2·x₁   
POL(__(x₁, x₂)) = 2 + 2·x₁ + x₂   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 0   
POL(isPal) = 0   
POL(isQid) = 0   
POL(nil) = 0   
POL(tt) = 0   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x₁)) = x₁   
POL(U21(x₁)) = 2·x₁   
POL(U22(x₁)) = 2·x₁   
POL(U31(x₁)) = 2·x₁   
POL(U41(x₁)) = 2·x₁   
POL(U42(x₁)) = x₁   
POL(U51(x₁)) = 2·x₁   
POL(U52(x₁)) = 2·x₁   
POL(U61(x₁)) = 1 + 2·x₁   
POL(U71(x₁)) = 1 + 2·x₁   
POL(U72(x₁)) = x₁   
POL(U81(x₁)) = x₁   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 1   
POL(isPal) = 1   
POL(isQid) = 0   
POL(tt) = 0   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U61(tt) → tt
isPal → tt

(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x₁)) = 2·x₁   
POL(U21(x₁)) = 2·x₁   
POL(U22(x₁)) = x₁   
POL(U31(x₁)) = x₁   
POL(U41(x₁)) = 2·x₁   
POL(U42(x₁)) = x₁   
POL(U51(x₁)) = x₁   
POL(U52(x₁)) = 2·x₁   
POL(U61(x₁)) = 2·x₁   
POL(U71(x₁)) = 1 + 2·x₁   
POL(U72(x₁)) = x₁   
POL(U81(x₁)) = x₁   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 1   
POL(isPal) = 1   
POL(isQid) = 0   
POL(tt) = 0   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNePal → U61(isQid)

(6) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U21¹(tt) → U22¹(isList)
U21¹(tt) → ISLIST
U41¹(tt) → U42¹(isNeList)
U41¹(tt) → ISNELIST
U51¹(tt) → U52¹(isList)
U51¹(tt) → ISLIST
U71¹(tt) → U72¹(isPal)
U71¹(tt) → ISPAL
ISLIST → U11¹(isNeList)
ISLIST → ISNELIST
ISLIST → U21¹(isList)
ISLIST → ISLIST
ISNELIST → U31¹(isQid)
ISNELIST → ISQID
ISNELIST → U41¹(isList)
ISNELIST → ISLIST
ISNELIST → U51¹(isNeList)
ISNELIST → ISNELIST
ISNEPAL → U71¹(isQid)
ISNEPAL → ISQID
ISPAL → U81¹(isNePal)
ISPAL → ISNEPAL

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 9 less nodes.

(10) Complex Obligation (AND)

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U71¹(tt) → ISPAL
ISPAL → ISNEPAL
ISNEPAL → U71¹(isQid)

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) NonLoopProof (EQUIVALENT transformation)

By Theorem 8 [NONLOOP] we deduce infiniteness of the QDP.
We apply the theorem with m = 1, b = 0,
σ' = [ ], and μ' = [ ] on the rule
U71¹(tt)[ ]ⁿ[ ] → U71¹(tt)[ ]ⁿ[ ]
This rule is correct for the QDP as the following derivation shows:

U71¹(tt)[ ]ⁿ[ ] → U71¹(tt)[ ]ⁿ[ ]
    by Narrowing at position: [0]
        U71¹(tt)[ ]ⁿ[ ] → U71¹(isQid)[ ]ⁿ[ ]
            by Narrowing at position: []
                U71¹(tt)[ ]ⁿ[ ] → ISNEPAL[ ]ⁿ[ ]
                    by Narrowing at position: []
                        U71¹(tt)[ ]ⁿ[ ] → ISPAL[ ]ⁿ[ ]
                            by OriginalRule from TRS P

                        ISPAL[ ]ⁿ[ ] → ISNEPAL[ ]ⁿ[ ]
                            by OriginalRule from TRS P

                ISNEPAL[ ]ⁿ[ ] → U71¹(isQid)[ ]ⁿ[ ]
                    by OriginalRule from TRS P

        isQid[ ]ⁿ[ ] → tt[ ]ⁿ[ ]
            by OriginalRule from TRS R

(13) NO

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U21¹(tt) → ISLIST
ISLIST → ISNELIST
ISNELIST → U41¹(isList)
U41¹(tt) → ISNELIST
ISNELIST → ISLIST
ISLIST → U21¹(isList)
ISLIST → ISLIST
ISNELIST → U51¹(isNeList)
U51¹(tt) → ISLIST
ISNELIST → ISNELIST

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(15) NonLoopProof (EQUIVALENT transformation)

By Theorem 8 [NONLOOP] we deduce infiniteness of the QDP.
We apply the theorem with m = 1, b = 0,
σ' = [ ], and μ' = [ ] on the rule
ISLIST[ ]ⁿ[ ] → ISLIST[ ]ⁿ[ ]
This rule is correct for the QDP as the following derivation shows:

ISLIST[ ]ⁿ[ ] → ISLIST[ ]ⁿ[ ]
    by OriginalRule from TRS P

(16) NO