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() ADG 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()) -> isPal#() isNePal#() -> U71#(isQid()) -> U71#(tt()) -> U72#(isPal()) isPal#() -> isNePal#() -> isNePal#() -> isQid#() isPal#() -> isNePal#() -> isNePal#() -> U61#(isQid()) isPal#() -> isNePal#() -> isNePal#() -> U71#(isQid()) U71#(tt()) -> isPal#() -> isPal#() -> isNePal#() U71#(tt()) -> isPal#() -> isPal#() -> U81#(isNePal()) U51#(tt()) -> isList#() -> isList#() -> isNeList#() U51#(tt()) -> isList#() -> isList#() -> U11#(isNeList()) U51#(tt()) -> isList#() -> isList#() -> isList#() U51#(tt()) -> isList#() -> isList#() -> U21#(isList()) isNeList#() -> U51#(isNeList()) -> U51#(tt()) -> isList#() isNeList#() -> U51#(isNeList()) -> U51#(tt()) -> U52#(isList()) isNeList#() -> isNeList#() -> isNeList#() -> isQid#() isNeList#() -> isNeList#() -> isNeList#() -> U31#(isQid()) isNeList#() -> isNeList#() -> isNeList#() -> isList#() isNeList#() -> isNeList#() -> isNeList#() -> U41#(isList()) isNeList#() -> isNeList#() -> isNeList#() -> isNeList#() isNeList#() -> isNeList#() -> isNeList#() -> U51#(isNeList()) isNeList#() -> U41#(isList()) -> U41#(tt()) -> isNeList#() isNeList#() -> U41#(isList()) -> U41#(tt()) -> U42#(isNeList()) isNeList#() -> isList#() -> isList#() -> isNeList#() isNeList#() -> isList#() -> isList#() -> U11#(isNeList()) isNeList#() -> isList#() -> isList#() -> isList#() isNeList#() -> isList#() -> isList#() -> U21#(isList()) U41#(tt()) -> isNeList#() -> isNeList#() -> isQid#() U41#(tt()) -> isNeList#() -> isNeList#() -> U31#(isQid()) U41#(tt()) -> isNeList#() -> isNeList#() -> isList#() U41#(tt()) -> isNeList#() -> isNeList#() -> U41#(isList()) U41#(tt()) -> isNeList#() -> isNeList#() -> isNeList#() U41#(tt()) -> isNeList#() -> isNeList#() -> U51#(isNeList()) isList#() -> isNeList#() -> isNeList#() -> isQid#() isList#() -> isNeList#() -> isNeList#() -> U31#(isQid()) isList#() -> isNeList#() -> isNeList#() -> isList#() isList#() -> isNeList#() -> isNeList#() -> U41#(isList()) isList#() -> isNeList#() -> isNeList#() -> isNeList#() isList#() -> isNeList#() -> isNeList#() -> U51#(isNeList()) isList#() -> isList#() -> isList#() -> isNeList#() isList#() -> isList#() -> isList#() -> U11#(isNeList()) isList#() -> isList#() -> isList#() -> isList#() isList#() -> isList#() -> isList#() -> U21#(isList()) isList#() -> U21#(isList()) -> U21#(tt()) -> isList#() isList#() -> U21#(isList()) -> U21#(tt()) -> U22#(isList()) U21#(tt()) -> isList#() -> isList#() -> isNeList#() U21#(tt()) -> isList#() -> isList#() -> U11#(isNeList()) U21#(tt()) -> isList#() -> isList#() -> isList#() U21#(tt()) -> isList#() -> isList#() -> U21#(isList()) __#(__(X,Y),Z) -> __#(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) -> __#(Y,Z) __#(__(X,Y),Z) -> __#(X,__(Y,Z)) -> __#(__(X,Y),Z) -> __#(X,__(Y,Z)) Restore Modifier: 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() 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#() -> U21#(isList()) U21#(tt()) -> isList#() isList#() -> isList#() isList#() -> isNeList#() isNeList#() -> U51#(isNeList()) isNeList#() -> isNeList#() isNeList#() -> U41#(isList()) U41#(tt()) -> isNeList#() isNeList#() -> isList#() 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