Termination w.r.t. Q proof of /tmp/tmp5M50jq/PALINDROME_complete-noand

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

0 QTRS

↳1 QTRSRRRProof (⇔)

↳2 QTRS

↳3 QTRSRRRProof (⇔)

↳4 QTRS

↳5 QTRSRRRProof (⇔)

↳6 QTRS

↳7 DependencyPairsProof (⇔)

↳8 QDP

↳9 DependencyGraphProof (⇔)

↳10 AND

  ↳11 QDP

    ↳12 UsableRulesProof (⇔)

    ↳13 QDP

    ↳14 Narrowing (⇔)

    ↳15 QDP

    ↳16 NonTerminationProof (⇔)

    ↳17 FALSE

  ↳18 QDP

    ↳19 UsableRulesProof (⇔)

    ↳20 QDP

    ↳21 Narrowing (⇔)

    ↳22 QDP

    ↳23 UsableRulesProof (⇔)

    ↳24 QDP

    ↳25 Narrowing (⇔)

    ↳26 QDP

    ↳27 Narrowing (⇔)

    ↳28 QDP

    ↳29 Narrowing (⇔)

    ↳30 QDP

    ↳31 NonTerminationProof (⇔)

    ↳32 FALSE

  ↳33 QDP

    ↳34 UsableRulesProof (⇔)

    ↳35 QDP

    ↳36 Narrowing (⇔)

    ↳37 QDP

    ↳38 Narrowing (⇔)

    ↳39 QDP

    ↳40 Narrowing (⇔)

    ↳41 QDP

    ↳42 Narrowing (⇔)

    ↳43 QDP

    ↳44 Narrowing (⇔)

    ↳45 QDP

    ↳46 Narrowing (⇔)

    ↳47 QDP

    ↳48 Narrowing (⇔)

    ↳49 QDP

    ↳50 Narrowing (⇔)

    ↳51 QDP

    ↳52 Narrowing (⇔)

    ↳53 QDP

    ↳54 Narrowing (⇔)

    ↳55 QDP

    ↳56 Narrowing (⇔)

    ↳57 QDP

    ↳58 Narrowing (⇔)

    ↳59 QDP

    ↳60 Narrowing (⇔)

    ↳61 QDP

    ↳62 Narrowing (⇔)

    ↳63 QDP

    ↳64 Narrowing (⇔)

    ↳65 QDP

    ↳66 Narrowing (⇔)

    ↳67 QDP

    ↳68 Narrowing (⇔)

    ↳69 QDP

    ↳70 NonTerminationProof (⇔)

    ↳71 FALSE

(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) → 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 → U91(isPalListKind)
isQid → tt

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x₁)) = x₁
POL(U12(x₁)) = x₁
POL(U13(x₁)) = x₁
POL(U21(x₁)) = x₁
POL(U22(x₁)) = x₁
POL(U23(x₁)) = x₁
POL(U24(x₁)) = x₁
POL(U25(x₁)) = x₁
POL(U26(x₁)) = x₁
POL(U31(x₁)) = x₁
POL(U32(x₁)) = x₁
POL(U33(x₁)) = x₁
POL(U41(x₁)) = x₁
POL(U42(x₁)) = x₁
POL(U43(x₁)) = x₁
POL(U44(x₁)) = x₁
POL(U45(x₁)) = x₁
POL(U46(x₁)) = x₁
POL(U51(x₁)) = x₁
POL(U52(x₁)) = x₁
POL(U53(x₁)) = x₁
POL(U54(x₁)) = x₁
POL(U55(x₁)) = x₁
POL(U56(x₁)) = x₁
POL(U61(x₁)) = 3 + x₁
POL(U62(x₁)) = 2 + x₁
POL(U63(x₁)) = 1 + x₁
POL(U71(x₁)) = 4 + x₁
POL(U72(x₁)) = 4 + x₁
POL(U73(x₁)) = x₁
POL(U74(x₁)) = x₁
POL(U81(x₁)) = 4 + x₁
POL(U82(x₁)) = 4 + x₁
POL(U83(x₁)) = x₁
POL(U91(x₁)) = x₁
POL(U92(x₁)) = x₁
POL(__(x₁, x₂)) = x₁ + x₂
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 4
POL(isPal) = 4
POL(isPalListKind) = 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:

U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
isNePal → U61(isPalListKind)
isPal → tt

(2) 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) → 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
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 → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x₁)) = x₁
POL(U12(x₁)) = x₁
POL(U13(x₁)) = x₁
POL(U21(x₁)) = x₁
POL(U22(x₁)) = x₁
POL(U23(x₁)) = x₁
POL(U24(x₁)) = x₁
POL(U25(x₁)) = x₁
POL(U26(x₁)) = x₁
POL(U31(x₁)) = x₁
POL(U32(x₁)) = x₁
POL(U33(x₁)) = x₁
POL(U41(x₁)) = x₁
POL(U42(x₁)) = x₁
POL(U43(x₁)) = x₁
POL(U44(x₁)) = x₁
POL(U45(x₁)) = x₁
POL(U46(x₁)) = x₁
POL(U51(x₁)) = x₁
POL(U52(x₁)) = x₁
POL(U53(x₁)) = x₁
POL(U54(x₁)) = x₁
POL(U55(x₁)) = x₁
POL(U56(x₁)) = x₁
POL(U71(x₁)) = x₁
POL(U72(x₁)) = x₁
POL(U73(x₁)) = x₁
POL(U74(x₁)) = x₁
POL(U81(x₁)) = x₁
POL(U82(x₁)) = x₁
POL(U83(x₁)) = x₁
POL(U91(x₁)) = x₁
POL(U92(x₁)) = x₁
POL(__(x₁, x₂)) = 1 + x₁ + x₂
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 0
POL(isPal) = 0
POL(isPalListKind) = 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, nil) → X
__(nil, X) → X

(4) Obligation:

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

__(__(X, Y), Z) → __(X, __(Y, Z))
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
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 → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U11(x₁)) = 2·x₁
POL(U12(x₁)) = x₁
POL(U13(x₁)) = 2·x₁
POL(U21(x₁)) = 2·x₁
POL(U22(x₁)) = 2·x₁
POL(U23(x₁)) = 2·x₁
POL(U24(x₁)) = 2·x₁
POL(U25(x₁)) = 2·x₁
POL(U26(x₁)) = x₁
POL(U31(x₁)) = 2·x₁
POL(U32(x₁)) = x₁
POL(U33(x₁)) = 2·x₁
POL(U41(x₁)) = 2·x₁
POL(U42(x₁)) = 2·x₁
POL(U43(x₁)) = 2·x₁
POL(U44(x₁)) = 2·x₁
POL(U45(x₁)) = x₁
POL(U46(x₁)) = 2·x₁
POL(U51(x₁)) = x₁
POL(U52(x₁)) = x₁
POL(U53(x₁)) = x₁
POL(U54(x₁)) = x₁
POL(U55(x₁)) = 2·x₁
POL(U56(x₁)) = 2·x₁
POL(U71(x₁)) = x₁
POL(U72(x₁)) = x₁
POL(U73(x₁)) = 2·x₁
POL(U74(x₁)) = x₁
POL(U81(x₁)) = x₁
POL(U82(x₁)) = 2·x₁
POL(U83(x₁)) = x₁
POL(U91(x₁)) = 2·x₁
POL(U92(x₁)) = x₁
POL(__(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 0
POL(isPal) = 0
POL(isPalListKind) = 0
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:

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

(6) Obligation:

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

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
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 → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
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:

U11¹(tt) → U12¹(isPalListKind)
U11¹(tt) → ISPALLISTKIND
U12¹(tt) → U13¹(isNeList)
U12¹(tt) → ISNELIST
U21¹(tt) → U22¹(isPalListKind)
U21¹(tt) → ISPALLISTKIND
U22¹(tt) → U23¹(isPalListKind)
U22¹(tt) → ISPALLISTKIND
U23¹(tt) → U24¹(isPalListKind)
U23¹(tt) → ISPALLISTKIND
U24¹(tt) → U25¹(isList)
U24¹(tt) → ISLIST
U25¹(tt) → U26¹(isList)
U25¹(tt) → ISLIST
U31¹(tt) → U32¹(isPalListKind)
U31¹(tt) → ISPALLISTKIND
U32¹(tt) → U33¹(isQid)
U32¹(tt) → ISQID
U41¹(tt) → U42¹(isPalListKind)
U41¹(tt) → ISPALLISTKIND
U42¹(tt) → U43¹(isPalListKind)
U42¹(tt) → ISPALLISTKIND
U43¹(tt) → U44¹(isPalListKind)
U43¹(tt) → ISPALLISTKIND
U44¹(tt) → U45¹(isList)
U44¹(tt) → ISLIST
U45¹(tt) → U46¹(isNeList)
U45¹(tt) → ISNELIST
U51¹(tt) → U52¹(isPalListKind)
U51¹(tt) → ISPALLISTKIND
U52¹(tt) → U53¹(isPalListKind)
U52¹(tt) → ISPALLISTKIND
U53¹(tt) → U54¹(isPalListKind)
U53¹(tt) → ISPALLISTKIND
U54¹(tt) → U55¹(isNeList)
U54¹(tt) → ISNELIST
U55¹(tt) → U56¹(isList)
U55¹(tt) → ISLIST
U71¹(tt) → U72¹(isPalListKind)
U71¹(tt) → ISPALLISTKIND
U72¹(tt) → U73¹(isPal)
U72¹(tt) → ISPAL
U73¹(tt) → U74¹(isPalListKind)
U73¹(tt) → ISPALLISTKIND
U81¹(tt) → U82¹(isPalListKind)
U81¹(tt) → ISPALLISTKIND
U82¹(tt) → U83¹(isNePal)
U82¹(tt) → ISNEPAL
U91¹(tt) → U92¹(isPalListKind)
U91¹(tt) → ISPALLISTKIND
ISLIST → U11¹(isPalListKind)
ISLIST → ISPALLISTKIND
ISLIST → U21¹(isPalListKind)
ISNELIST → U31¹(isPalListKind)
ISNELIST → ISPALLISTKIND
ISNELIST → U41¹(isPalListKind)
ISNELIST → U51¹(isPalListKind)
ISNEPAL → U71¹(isQid)
ISNEPAL → ISQID
ISPAL → U81¹(isPalListKind)
ISPAL → ISPALLISTKIND
ISPALLISTKIND → U91¹(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND

The TRS R consists of the following rules:

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
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 → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
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 3 SCCs with 30 less nodes.

(10) Complex Obligation (AND)

(11) Obligation:

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

U91¹(tt) → ISPALLISTKIND
ISPALLISTKIND → U91¹(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND

The TRS R consists of the following rules:

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
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 → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

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

(12) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(13) Obligation:

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

U91¹(tt) → ISPALLISTKIND
ISPALLISTKIND → U91¹(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

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

(14) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISPALLISTKIND → U91¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISPALLISTKIND → U91¹(tt)
ISPALLISTKIND → U91¹(U91(isPalListKind))

(15) Obligation:

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

U91¹(tt) → ISPALLISTKIND
ISPALLISTKIND → ISPALLISTKIND
ISPALLISTKIND → U91¹(tt)
ISPALLISTKIND → U91¹(U91(isPalListKind))

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

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

(16) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = ISPALLISTKIND evaluates to t =ISPALLISTKIND

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ISPALLISTKIND to ISPALLISTKIND.

(17) FALSE

(18) Obligation:

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

U72¹(tt) → ISPAL
ISPAL → U81¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
U82¹(tt) → ISNEPAL
ISNEPAL → U71¹(isQid)
U71¹(tt) → U72¹(isPalListKind)

The TRS R consists of the following rules:

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
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 → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

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

(19) UsableRulesProof (EQUIVALENT transformation)

(20) Obligation:

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

U72¹(tt) → ISPAL
ISPAL → U81¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
U82¹(tt) → ISNEPAL
ISNEPAL → U71¹(isQid)
U71¹(tt) → U72¹(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isQid → tt

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

(21) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNEPAL → U71¹(isQid) at position [0] we obtained the following new rules [LPAR04]:

ISNEPAL → U71¹(tt)

(22) Obligation:

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

U72¹(tt) → ISPAL
ISPAL → U81¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(isPalListKind)
ISNEPAL → U71¹(tt)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isQid → tt

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

(23) UsableRulesProof (EQUIVALENT transformation)

(24) Obligation:

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

U72¹(tt) → ISPAL
ISPAL → U81¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(isPalListKind)
ISNEPAL → U71¹(tt)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

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

(25) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISPAL → U81¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISPAL → U81¹(tt)
ISPAL → U81¹(U91(isPalListKind))

(26) Obligation:

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

U72¹(tt) → ISPAL
U81¹(tt) → U82¹(isPalListKind)
U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(isPalListKind)
ISNEPAL → U71¹(tt)
ISPAL → U81¹(tt)
ISPAL → U81¹(U91(isPalListKind))

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

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

(27) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U81¹(tt) → U82¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U81¹(tt) → U82¹(tt)
U81¹(tt) → U82¹(U91(isPalListKind))

(28) Obligation:

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

U72¹(tt) → ISPAL
U82¹(tt) → ISNEPAL
U71¹(tt) → U72¹(isPalListKind)
ISNEPAL → U71¹(tt)
ISPAL → U81¹(tt)
ISPAL → U81¹(U91(isPalListKind))
U81¹(tt) → U82¹(tt)
U81¹(tt) → U82¹(U91(isPalListKind))

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

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

(29) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U71¹(tt) → U72¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U71¹(tt) → U72¹(tt)
U71¹(tt) → U72¹(U91(isPalListKind))

(30) Obligation:

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

U72¹(tt) → ISPAL
U82¹(tt) → ISNEPAL
ISNEPAL → U71¹(tt)
ISPAL → U81¹(tt)
ISPAL → U81¹(U91(isPalListKind))
U81¹(tt) → U82¹(tt)
U81¹(tt) → U82¹(U91(isPalListKind))
U71¹(tt) → U72¹(tt)
U71¹(tt) → U72¹(U91(isPalListKind))

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

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

(31) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ISPAL evaluates to t =ISPAL

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

ISPAL → U81¹(tt)
with rule ISPAL → U81¹(tt) at position [] and matcher [ ]

U81¹(tt) → U82¹(tt)
with rule U81¹(tt) → U82¹(tt) at position [] and matcher [ ]

U82¹(tt) → ISNEPAL
with rule U82¹(tt) → ISNEPAL at position [] and matcher [ ]

ISNEPAL → U71¹(tt)
with rule ISNEPAL → U71¹(tt) at position [] and matcher [ ]

U71¹(tt) → U72¹(tt)
with rule U71¹(tt) → U72¹(tt) at position [] and matcher [ ]

U72¹(tt) → ISPAL
with rule U72¹(tt) → ISPAL

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

(32) FALSE

(33) Obligation:

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

U12¹(tt) → ISNELIST
ISNELIST → U41¹(isPalListKind)
U41¹(tt) → U42¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST

The TRS R consists of the following rules:

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
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 → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

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

(34) UsableRulesProof (EQUIVALENT transformation)

(35) Obligation:

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

U12¹(tt) → ISNELIST
ISNELIST → U41¹(isPalListKind)
U41¹(tt) → U42¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(36) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNELIST → U41¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))

(37) Obligation:

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

U12¹(tt) → ISNELIST
U41¹(tt) → U42¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(38) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U41¹(tt) → U42¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))

(39) Obligation:

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

U12¹(tt) → ISNELIST
U42¹(tt) → U43¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(40) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U42¹(tt) → U43¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))

(41) Obligation:

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

U12¹(tt) → ISNELIST
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(42) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U43¹(tt) → U44¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))

(43) Obligation:

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

U12¹(tt) → ISNELIST
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(44) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U44¹(tt) → U45¹(isList) at position [0] we obtained the following new rules [LPAR04]:

U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))

(45) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(46) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNELIST → U51¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))

(47) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(48) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U51¹(tt) → U52¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))

(49) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(50) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U52¹(tt) → U53¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))

(51) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(52) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U53¹(tt) → U54¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))

(53) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(54) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U54¹(tt) → U55¹(isNeList) at position [0] we obtained the following new rules [LPAR04]:

U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))

(55) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(56) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISLIST → U11¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))

(57) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(58) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U11¹(tt) → U12¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))

(59) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(60) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISLIST → U21¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))

(61) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(62) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U21¹(tt) → U22¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))

(63) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(64) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U22¹(tt) → U23¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U22¹(tt) → U23¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))

(65) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(66) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U23¹(tt) → U24¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U23¹(tt) → U24¹(tt)
U23¹(tt) → U24¹(U91(isPalListKind))

(67) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U23¹(tt) → U24¹(U91(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(68) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U24¹(tt) → U25¹(isList) at position [0] we obtained the following new rules [LPAR04]:

U24¹(tt) → U25¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U24¹(tt) → U25¹(U21(isPalListKind))

(69) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U23¹(tt) → U24¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U24¹(tt) → U25¹(U21(isPalListKind))

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(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
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

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

(70) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ISLIST evaluates to t =ISLIST

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

ISLIST → U21¹(tt)
with rule ISLIST → U21¹(tt) at position [] and matcher [ ]

U21¹(tt) → U22¹(tt)
with rule U21¹(tt) → U22¹(tt) at position [] and matcher [ ]

U22¹(tt) → U23¹(tt)
with rule U22¹(tt) → U23¹(tt) at position [] and matcher [ ]

U23¹(tt) → U24¹(tt)
with rule U23¹(tt) → U24¹(tt) at position [] and matcher [ ]

U24¹(tt) → ISLIST
with rule U24¹(tt) → ISLIST

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

(0) Obligation:

(1) QTRSRRRProof (EQUIVALENT transformation)

(2) Obligation:

(3) QTRSRRRProof (EQUIVALENT transformation)

(4) Obligation:

(5) QTRSRRRProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyPairsProof (EQUIVALENT transformation)

(8) Obligation:

(9) DependencyGraphProof (EQUIVALENT transformation)

(10) Complex Obligation (AND)

(11) Obligation:

(12) UsableRulesProof (EQUIVALENT transformation)

(13) Obligation:

(14) Narrowing (EQUIVALENT transformation)

(15) Obligation:

(16) NonTerminationProof (EQUIVALENT transformation)

(17) FALSE

(18) Obligation:

(19) UsableRulesProof (EQUIVALENT transformation)

(20) Obligation:

(21) Narrowing (EQUIVALENT transformation)

(22) Obligation:

(23) UsableRulesProof (EQUIVALENT transformation)

(24) Obligation:

(25) Narrowing (EQUIVALENT transformation)

(26) Obligation:

(27) Narrowing (EQUIVALENT transformation)

(28) Obligation:

(29) Narrowing (EQUIVALENT transformation)

(30) Obligation:

(31) NonTerminationProof (EQUIVALENT transformation)

(32) FALSE

(33) Obligation:

(34) UsableRulesProof (EQUIVALENT transformation)

(35) Obligation:

(36) Narrowing (EQUIVALENT transformation)

(37) Obligation:

(38) Narrowing (EQUIVALENT transformation)

(39) Obligation:

(40) Narrowing (EQUIVALENT transformation)

(41) Obligation:

(42) Narrowing (EQUIVALENT transformation)

(43) Obligation:

(44) Narrowing (EQUIVALENT transformation)

(45) Obligation:

(46) Narrowing (EQUIVALENT transformation)

(47) Obligation:

(48) Narrowing (EQUIVALENT transformation)

(49) Obligation:

(50) Narrowing (EQUIVALENT transformation)

(51) Obligation:

(52) Narrowing (EQUIVALENT transformation)

(53) Obligation:

(54) Narrowing (EQUIVALENT transformation)

(55) Obligation:

(56) Narrowing (EQUIVALENT transformation)

(57) Obligation:

(58) Narrowing (EQUIVALENT transformation)

(59) Obligation:

(60) Narrowing (EQUIVALENT transformation)

(61) Obligation:

(62) Narrowing (EQUIVALENT transformation)

(63) Obligation:

(64) Narrowing (EQUIVALENT transformation)

(65) Obligation:

(66) Narrowing (EQUIVALENT transformation)

(67) Obligation:

(68) Narrowing (EQUIVALENT transformation)

(69) Obligation:

(70) NonTerminationProof (EQUIVALENT transformation)

(71) FALSE