Input TRS: 1: __(__(X,Y),Z) -> __(X,__(Y,Z)) 2: __(X,nil()) -> X 3: __(nil(),X) -> X 4: U11(tt()) -> U12(isPalListKind()) 5: U12(tt()) -> U13(isNeList()) 6: U13(tt()) -> tt() 7: U21(tt()) -> U22(isPalListKind()) 8: U22(tt()) -> U23(isPalListKind()) 9: U23(tt()) -> U24(isPalListKind()) 10: U24(tt()) -> U25(isList()) 11: U25(tt()) -> U26(isList()) 12: U26(tt()) -> tt() 13: U31(tt()) -> U32(isPalListKind()) 14: U32(tt()) -> U33(isQid()) 15: U33(tt()) -> tt() 16: U41(tt()) -> U42(isPalListKind()) 17: U42(tt()) -> U43(isPalListKind()) 18: U43(tt()) -> U44(isPalListKind()) 19: U44(tt()) -> U45(isList()) 20: U45(tt()) -> U46(isNeList()) 21: U46(tt()) -> tt() 22: U51(tt()) -> U52(isPalListKind()) 23: U52(tt()) -> U53(isPalListKind()) 24: U53(tt()) -> U54(isPalListKind()) 25: U54(tt()) -> U55(isNeList()) 26: U55(tt()) -> U56(isList()) 27: U56(tt()) -> tt() 28: U61(tt()) -> U62(isPalListKind()) 29: U62(tt()) -> U63(isQid()) 30: U63(tt()) -> tt() 31: U71(tt()) -> U72(isPalListKind()) 32: U72(tt()) -> U73(isPal()) 33: U73(tt()) -> U74(isPalListKind()) 34: U74(tt()) -> tt() 35: U81(tt()) -> U82(isPalListKind()) 36: U82(tt()) -> U83(isNePal()) 37: U83(tt()) -> tt() 38: U91(tt()) -> U92(isPalListKind()) 39: U92(tt()) -> tt() 40: isList() -> U11(isPalListKind()) 41: isList() -> tt() 42: isList() -> U21(isPalListKind()) 43: isNeList() -> U31(isPalListKind()) 44: isNeList() -> U41(isPalListKind()) 45: isNeList() -> U51(isPalListKind()) 46: isNePal() -> U61(isPalListKind()) 47: isNePal() -> U71(isQid()) 48: isPal() -> U81(isPalListKind()) 49: isPal() -> tt() 50: isPalListKind() -> tt() 51: isPalListKind() -> U91(isPalListKind()) 52: isQid() -> tt() Number of strict rules: 52 Direct Order(PosReal,>,Poly) ... removes: 1 3 2 U21(x1) weight: x1 U11(x1) weight: x1 U24(x1) weight: x1 U25(x1) weight: x1 isNeList() weight: 0 U56(x1) weight: x1 isPal() weight: 0 U42(x1) weight: x1 U91(x1) weight: x1 U26(x1) weight: x1 U71(x1) weight: x1 U43(x1) weight: x1 U44(x1) weight: x1 U55(x1) weight: x1 U23(x1) weight: x1 U63(x1) weight: x1 isNePal() weight: 0 U72(x1) weight: x1 U12(x1) weight: x1 isQid() weight: 0 U54(x1) weight: x1 U83(x1) weight: x1 isList() weight: 0 U73(x1) weight: x1 nil() weight: 0 U62(x1) weight: x1 U45(x1) weight: x1 U32(x1) weight: x1 U33(x1) weight: x1 U46(x1) weight: x1 U52(x1) weight: x1 U61(x1) weight: x1 U31(x1) weight: x1 U92(x1) weight: x1 U81(x1) weight: x1 U82(x1) weight: x1 tt() weight: 0 U13(x1) weight: x1 U22(x1) weight: x1 U51(x1) weight: x1 U74(x1) weight: x1 isPalListKind() weight: 0 U53(x1) weight: x1 U41(x1) weight: x1 __(x1,x2) weight: (/ 1 4) + 2 * x1 + x2 Number of strict rules: 49 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #isNeList() -> #U31(isPalListKind()) #2: #isNeList() -> #isPalListKind() #3: #U62(tt()) -> #U63(isQid()) #4: #U62(tt()) -> #isQid() #5: #U81(tt()) -> #U82(isPalListKind()) #6: #U81(tt()) -> #isPalListKind() #7: #isNePal() -> #U61(isPalListKind()) #8: #isNePal() -> #isPalListKind() #9: #isList() -> #U21(isPalListKind()) #10: #isList() -> #isPalListKind() #11: #isNePal() -> #U71(isQid()) #12: #isNePal() -> #isQid() #13: #isPal() -> #U81(isPalListKind()) #14: #isPal() -> #isPalListKind() #15: #U91(tt()) -> #U92(isPalListKind()) #16: #U91(tt()) -> #isPalListKind() #17: #isList() -> #U11(isPalListKind()) #18: #isList() -> #isPalListKind() #19: #isPalListKind() -> #U91(isPalListKind()) #20: #isPalListKind() -> #isPalListKind() #21: #U31(tt()) -> #U32(isPalListKind()) #22: #U31(tt()) -> #isPalListKind() #23: #U23(tt()) -> #U24(isPalListKind()) #24: #U23(tt()) -> #isPalListKind() #25: #U25(tt()) -> #U26(isList()) #26: #U25(tt()) -> #isList() #27: #U53(tt()) -> #U54(isPalListKind()) #28: #U53(tt()) -> #isPalListKind() #29: #U52(tt()) -> #U53(isPalListKind()) #30: #U52(tt()) -> #isPalListKind() #31: #isNeList() -> #U51(isPalListKind()) #32: #isNeList() -> #isPalListKind() #33: #U71(tt()) -> #U72(isPalListKind()) #34: #U71(tt()) -> #isPalListKind() #35: #U32(tt()) -> #U33(isQid()) #36: #U32(tt()) -> #isQid() #37: #U54(tt()) -> #U55(isNeList()) #38: #U54(tt()) -> #isNeList() #39: #U45(tt()) -> #U46(isNeList()) #40: #U45(tt()) -> #isNeList() #41: #U21(tt()) -> #U22(isPalListKind()) #42: #U21(tt()) -> #isPalListKind() #43: #U24(tt()) -> #U25(isList()) #44: #U24(tt()) -> #isList() #45: #U73(tt()) -> #U74(isPalListKind()) #46: #U73(tt()) -> #isPalListKind() #47: #U12(tt()) -> #U13(isNeList()) #48: #U12(tt()) -> #isNeList() #49: #isNeList() -> #U41(isPalListKind()) #50: #isNeList() -> #isPalListKind() #51: #U61(tt()) -> #U62(isPalListKind()) #52: #U61(tt()) -> #isPalListKind() #53: #U51(tt()) -> #U52(isPalListKind()) #54: #U51(tt()) -> #isPalListKind() #55: #U42(tt()) -> #U43(isPalListKind()) #56: #U42(tt()) -> #isPalListKind() #57: #U72(tt()) -> #U73(isPal()) #58: #U72(tt()) -> #isPal() #59: #U44(tt()) -> #U45(isList()) #60: #U44(tt()) -> #isList() #61: #U55(tt()) -> #U56(isList()) #62: #U55(tt()) -> #isList() #63: #U82(tt()) -> #U83(isNePal()) #64: #U82(tt()) -> #isNePal() #65: #U41(tt()) -> #U42(isPalListKind()) #66: #U41(tt()) -> #isPalListKind() #67: #U22(tt()) -> #U23(isPalListKind()) #68: #U22(tt()) -> #isPalListKind() #69: #U11(tt()) -> #U12(isPalListKind()) #70: #U11(tt()) -> #isPalListKind() #71: #U43(tt()) -> #U44(isPalListKind()) #72: #U43(tt()) -> #isPalListKind() Number of SCCs: 3, DPs: 33, edges: 45 SCC { #16 #19 #20 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed. Removing edges: failed. Finding a loop... found. #isPalListKind() -#20-> #isPalListKind() --->* #isPalListKind() Looping with: [ ] NO