MAYBE

Problem:
 __(__(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()

Proof:
 DP Processor:
  DPs:
   __#(__(X,Y),Z) -> __#(Y,Z)
   __#(__(X,Y),Z) -> __#(X,__(Y,Z))
   U21#(tt()) -> isList#()
   U21#(tt()) -> U22#(isList())
   U41#(tt()) -> isNeList#()
   U41#(tt()) -> U42#(isNeList())
   U51#(tt()) -> isList#()
   U51#(tt()) -> U52#(isList())
   U71#(tt()) -> isPal#()
   U71#(tt()) -> U72#(isPal())
   isList#() -> isNeList#()
   isList#() -> U11#(isNeList())
   isList#() -> isList#()
   isList#() -> U21#(isList())
   isNeList#() -> isQid#()
   isNeList#() -> U31#(isQid())
   isNeList#() -> isList#()
   isNeList#() -> U41#(isList())
   isNeList#() -> isNeList#()
   isNeList#() -> U51#(isNeList())
   isNePal#() -> isQid#()
   isNePal#() -> U61#(isQid())
   isNePal#() -> U71#(isQid())
   isPal#() -> isNePal#()
   isPal#() -> U81#(isNePal())
  TRS:
   __(__(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()
  TDG Processor:
   DPs:
    __#(__(X,Y),Z) -> __#(Y,Z)
    __#(__(X,Y),Z) -> __#(X,__(Y,Z))
    U21#(tt()) -> isList#()
    U21#(tt()) -> U22#(isList())
    U41#(tt()) -> isNeList#()
    U41#(tt()) -> U42#(isNeList())
    U51#(tt()) -> isList#()
    U51#(tt()) -> U52#(isList())
    U71#(tt()) -> isPal#()
    U71#(tt()) -> U72#(isPal())
    isList#() -> isNeList#()
    isList#() -> U11#(isNeList())
    isList#() -> isList#()
    isList#() -> U21#(isList())
    isNeList#() -> isQid#()
    isNeList#() -> U31#(isQid())
    isNeList#() -> isList#()
    isNeList#() -> U41#(isList())
    isNeList#() -> isNeList#()
    isNeList#() -> U51#(isNeList())
    isNePal#() -> isQid#()
    isNePal#() -> U61#(isQid())
    isNePal#() -> U71#(isQid())
    isPal#() -> isNePal#()
    isPal#() -> U81#(isNePal())
   TRS:
    __(__(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()
   graph:
    isNePal#() -> U71#(isQid()) -> U71#(tt()) -> U72#(isPal())
    isNePal#() -> U71#(isQid()) -> U71#(tt()) -> isPal#()
    isPal#() -> isNePal#() -> isNePal#() -> U71#(isQid())
    isPal#() -> isNePal#() -> isNePal#() -> U61#(isQid())
    isPal#() -> isNePal#() -> isNePal#() -> isQid#()
    U71#(tt()) -> isPal#() -> isPal#() -> U81#(isNePal())
    U71#(tt()) -> isPal#() -> isPal#() -> isNePal#()
    U51#(tt()) -> isList#() -> isList#() -> U21#(isList())
    U51#(tt()) -> isList#() -> isList#() -> isList#()
    U51#(tt()) -> isList#() -> isList#() -> U11#(isNeList())
    U51#(tt()) -> isList#() -> isList#() -> isNeList#()
    isNeList#() -> U51#(isNeList()) -> U51#(tt()) -> U52#(isList())
    isNeList#() -> U51#(isNeList()) -> U51#(tt()) -> isList#()
    isNeList#() -> isNeList#() -> isNeList#() -> U51#(isNeList())
    isNeList#() -> isNeList#() -> isNeList#() -> isNeList#()
    isNeList#() -> isNeList#() -> isNeList#() -> U41#(isList())
    isNeList#() -> isNeList#() -> isNeList#() -> isList#()
    isNeList#() -> isNeList#() -> isNeList#() -> U31#(isQid())
    isNeList#() -> isNeList#() -> isNeList#() -> isQid#()
    isNeList#() -> U41#(isList()) -> U41#(tt()) -> U42#(isNeList())
    isNeList#() -> U41#(isList()) -> U41#(tt()) -> isNeList#()
    isNeList#() -> isList#() -> isList#() -> U21#(isList())
    isNeList#() -> isList#() -> isList#() -> isList#()
    isNeList#() -> isList#() -> isList#() -> U11#(isNeList())
    isNeList#() -> isList#() -> isList#() -> isNeList#()
    U41#(tt()) -> isNeList#() -> isNeList#() -> U51#(isNeList())
    U41#(tt()) -> isNeList#() -> isNeList#() -> isNeList#()
    U41#(tt()) -> isNeList#() -> isNeList#() -> U41#(isList())
    U41#(tt()) -> isNeList#() -> isNeList#() -> isList#()
    U41#(tt()) -> isNeList#() -> isNeList#() -> U31#(isQid())
    U41#(tt()) -> isNeList#() -> isNeList#() -> isQid#()
    isList#() -> isNeList#() -> isNeList#() -> U51#(isNeList())
    isList#() -> isNeList#() -> isNeList#() -> isNeList#()
    isList#() -> isNeList#() -> isNeList#() -> U41#(isList())
    isList#() -> isNeList#() -> isNeList#() -> isList#()
    isList#() -> isNeList#() -> isNeList#() -> U31#(isQid())
    isList#() -> isNeList#() -> isNeList#() -> isQid#()
    isList#() -> isList#() -> isList#() -> U21#(isList())
    isList#() -> isList#() -> isList#() -> isList#()
    isList#() -> isList#() -> isList#() -> U11#(isNeList())
    isList#() -> isList#() -> isList#() -> isNeList#()
    isList#() -> U21#(isList()) -> U21#(tt()) -> U22#(isList())
    isList#() -> U21#(isList()) -> U21#(tt()) -> isList#()
    U21#(tt()) -> isList#() -> isList#() -> U21#(isList())
    U21#(tt()) -> isList#() -> isList#() -> isList#()
    U21#(tt()) -> isList#() -> isList#() -> U11#(isNeList())
    U21#(tt()) -> isList#() -> isList#() -> isNeList#()
    __#(__(X,Y),Z) -> __#(Y,Z) -> __#(__(X,Y),Z) -> __#(X,__(Y,Z))
    __#(__(X,Y),Z) -> __#(Y,Z) -> __#(__(X,Y),Z) -> __#(Y,Z)
    __#(__(X,Y),Z) -> __#(X,__(Y,Z)) ->
    __#(__(X,Y),Z) -> __#(X,__(Y,Z))
    __#(__(X,Y),Z) -> __#(X,__(Y,Z)) -> __#(__(X,Y),Z) -> __#(Y,Z)
   SCC Processor:
    #sccs: 3
    #rules: 15
    #arcs: 51/625
    DPs:
     __#(__(X,Y),Z) -> __#(Y,Z)
     __#(__(X,Y),Z) -> __#(X,__(Y,Z))
    TRS:
     __(__(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()
    Open
    
    DPs:
     U51#(tt()) -> isList#()
     isList#() -> isNeList#()
     isNeList#() -> isList#()
     isList#() -> isList#()
     isList#() -> U21#(isList())
     U21#(tt()) -> isList#()
     isNeList#() -> U41#(isList())
     U41#(tt()) -> isNeList#()
     isNeList#() -> isNeList#()
     isNeList#() -> U51#(isNeList())
    TRS:
     __(__(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()
    Open
    
    DPs:
     isNePal#() -> U71#(isQid())
     U71#(tt()) -> isPal#()
     isPal#() -> isNePal#()
    TRS:
     __(__(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()
    Open