Input TRS: 1: __(__(X,Y),Z) -> __(X,__(Y,Z)) 2: __(X,nil()) -> X 3: __(nil(),X) -> X 4: U11(tt(),V) -> U12(isNeList(activate(V))) 5: U12(tt()) -> tt() 6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) 7: U22(tt(),V2) -> U23(isList(activate(V2))) 8: U23(tt()) -> tt() 9: U31(tt(),V) -> U32(isQid(activate(V))) 10: U32(tt()) -> tt() 11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) 12: U42(tt(),V2) -> U43(isNeList(activate(V2))) 13: U43(tt()) -> tt() 14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) 15: U52(tt(),V2) -> U53(isList(activate(V2))) 16: U53(tt()) -> tt() 17: U61(tt(),V) -> U62(isQid(activate(V))) 18: U62(tt()) -> tt() 19: U71(tt(),V) -> U72(isNePal(activate(V))) 20: U72(tt()) -> tt() 21: and(tt(),X) -> activate(X) 22: isList(V) -> U11(isPalListKind(activate(V)),activate(V)) 23: isList(n__nil()) -> tt() 24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) 25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) 26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) 27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) 28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) 29: isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) 30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) 31: isPal(n__nil()) -> tt() 32: isPalListKind(n__a()) -> tt() 33: isPalListKind(n__e()) -> tt() 34: isPalListKind(n__i()) -> tt() 35: isPalListKind(n__nil()) -> tt() 36: isPalListKind(n__o()) -> tt() 37: isPalListKind(n__u()) -> tt() 38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) 39: isQid(n__a()) -> tt() 40: isQid(n__e()) -> tt() 41: isQid(n__i()) -> tt() 42: isQid(n__o()) -> tt() 43: isQid(n__u()) -> tt() 44: nil() -> n__nil() 45: __(X1,X2) -> n____(X1,X2) 46: isPalListKind(X) -> n__isPalListKind(X) 47: and(X1,X2) -> n__and(X1,X2) 48: a() -> n__a() 49: e() -> n__e() 50: i() -> n__i() 51: o() -> n__o() 52: u() -> n__u() 53: activate(n__nil()) -> nil() 54: activate(n____(X1,X2)) -> __(X1,X2) 55: activate(n__isPalListKind(X)) -> isPalListKind(X) 56: activate(n__and(X1,X2)) -> and(X1,X2) 57: activate(n__a()) -> a() 58: activate(n__e()) -> e() 59: activate(n__i()) -> i() 60: activate(n__o()) -> o() 61: activate(n__u()) -> u() 62: activate(X) -> X Number of strict rules: 62 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #isNePal(n____(I,__(P,I))) -> #and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) #2: #isNePal(n____(I,__(P,I))) -> #and(isQid(activate(I)),n__isPalListKind(activate(I))) #3: #isNePal(n____(I,__(P,I))) -> #isQid(activate(I)) #4: #isNePal(n____(I,__(P,I))) -> #activate(I) #5: #isNePal(n____(I,__(P,I))) -> #activate(I) #6: #isNePal(n____(I,__(P,I))) -> #isPal(activate(P)) #7: #isNePal(n____(I,__(P,I))) -> #activate(P) #8: #isNePal(n____(I,__(P,I))) -> #activate(P) #9: #activate(n__nil()) -> #nil() #10: #activate(n__e()) -> #e() #11: #activate(n__u()) -> #u() #12: #isPalListKind(n____(V1,V2)) -> #and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) #13: #isPalListKind(n____(V1,V2)) -> #isPalListKind(activate(V1)) #14: #isPalListKind(n____(V1,V2)) -> #activate(V1) #15: #isPalListKind(n____(V1,V2)) -> #activate(V2) #16: #U21(tt(),V1,V2) -> #U22(isList(activate(V1)),activate(V2)) #17: #U21(tt(),V1,V2) -> #isList(activate(V1)) #18: #U21(tt(),V1,V2) -> #activate(V1) #19: #U21(tt(),V1,V2) -> #activate(V2) #20: #activate(n__i()) -> #i() #21: #activate(n__isPalListKind(X)) -> #isPalListKind(X) #22: #U31(tt(),V) -> #U32(isQid(activate(V))) #23: #U31(tt(),V) -> #isQid(activate(V)) #24: #U31(tt(),V) -> #activate(V) #25: #U41(tt(),V1,V2) -> #U42(isList(activate(V1)),activate(V2)) #26: #U41(tt(),V1,V2) -> #isList(activate(V1)) #27: #U41(tt(),V1,V2) -> #activate(V1) #28: #U41(tt(),V1,V2) -> #activate(V2) #29: #activate(n__a()) -> #a() #30: #isList(n____(V1,V2)) -> #U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) #31: #isList(n____(V1,V2)) -> #and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) #32: #isList(n____(V1,V2)) -> #isPalListKind(activate(V1)) #33: #isList(n____(V1,V2)) -> #activate(V1) #34: #isList(n____(V1,V2)) -> #activate(V2) #35: #isList(n____(V1,V2)) -> #activate(V1) #36: #isList(n____(V1,V2)) -> #activate(V2) #37: #U42(tt(),V2) -> #U43(isNeList(activate(V2))) #38: #U42(tt(),V2) -> #isNeList(activate(V2)) #39: #U42(tt(),V2) -> #activate(V2) #40: #activate(n__and(X1,X2)) -> #and(X1,X2) #41: #U51(tt(),V1,V2) -> #U52(isNeList(activate(V1)),activate(V2)) #42: #U51(tt(),V1,V2) -> #isNeList(activate(V1)) #43: #U51(tt(),V1,V2) -> #activate(V1) #44: #U51(tt(),V1,V2) -> #activate(V2) #45: #isPal(V) -> #U71(isPalListKind(activate(V)),activate(V)) #46: #isPal(V) -> #isPalListKind(activate(V)) #47: #isPal(V) -> #activate(V) #48: #isPal(V) -> #activate(V) #49: #isNeList(V) -> #U31(isPalListKind(activate(V)),activate(V)) #50: #isNeList(V) -> #isPalListKind(activate(V)) #51: #isNeList(V) -> #activate(V) #52: #isNeList(V) -> #activate(V) #53: #U22(tt(),V2) -> #U23(isList(activate(V2))) #54: #U22(tt(),V2) -> #isList(activate(V2)) #55: #U22(tt(),V2) -> #activate(V2) #56: #isNePal(V) -> #U61(isPalListKind(activate(V)),activate(V)) #57: #isNePal(V) -> #isPalListKind(activate(V)) #58: #isNePal(V) -> #activate(V) #59: #isNePal(V) -> #activate(V) #60: #isList(V) -> #U11(isPalListKind(activate(V)),activate(V)) #61: #isList(V) -> #isPalListKind(activate(V)) #62: #isList(V) -> #activate(V) #63: #isList(V) -> #activate(V) #64: #isNeList(n____(V1,V2)) -> #U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) #65: #isNeList(n____(V1,V2)) -> #and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) #66: #isNeList(n____(V1,V2)) -> #isPalListKind(activate(V1)) #67: #isNeList(n____(V1,V2)) -> #activate(V1) #68: #isNeList(n____(V1,V2)) -> #activate(V2) #69: #isNeList(n____(V1,V2)) -> #activate(V1) #70: #isNeList(n____(V1,V2)) -> #activate(V2) #71: #activate(n__o()) -> #o() #72: #U61(tt(),V) -> #U62(isQid(activate(V))) #73: #U61(tt(),V) -> #isQid(activate(V)) #74: #U61(tt(),V) -> #activate(V) #75: #U71(tt(),V) -> #U72(isNePal(activate(V))) #76: #U71(tt(),V) -> #isNePal(activate(V)) #77: #U71(tt(),V) -> #activate(V) #78: #isNeList(n____(V1,V2)) -> #U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) #79: #isNeList(n____(V1,V2)) -> #and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) #80: #isNeList(n____(V1,V2)) -> #isPalListKind(activate(V1)) #81: #isNeList(n____(V1,V2)) -> #activate(V1) #82: #isNeList(n____(V1,V2)) -> #activate(V2) #83: #isNeList(n____(V1,V2)) -> #activate(V1) #84: #isNeList(n____(V1,V2)) -> #activate(V2) #85: #and(tt(),X) -> #activate(X) #86: #__(__(X,Y),Z) -> #__(X,__(Y,Z)) #87: #__(__(X,Y),Z) -> #__(Y,Z) #88: #activate(n____(X1,X2)) -> #__(X1,X2) #89: #U52(tt(),V2) -> #U53(isList(activate(V2))) #90: #U52(tt(),V2) -> #isList(activate(V2)) #91: #U52(tt(),V2) -> #activate(V2) #92: #U11(tt(),V) -> #U12(isNeList(activate(V))) #93: #U11(tt(),V) -> #isNeList(activate(V)) #94: #U11(tt(),V) -> #activate(V) Number of SCCs: 4, DPs: 26, edges: 47 SCC { #86 #87 } Removing DPs: Order(PosReal,>,Sum)... succeeded. a() weight: 0 n__a() weight: 0 #U72(x1) weight: 0 #U32(x1) weight: 0 U21(x1,x2,x3) weight: 0 #isPalListKind(x1) weight: 0 U11(x1,x2) weight: 0 n__o() weight: 0 isNeList(x1) weight: 0 isPal(x1) weight: 0 U42(x1,x2) weight: 0 #e() weight: 0 u() weight: 0 activate(x1) weight: 0 U71(x1,x2) weight: 0 and(x1,x2) weight: 0 #u() weight: 0 #isNeList(x1) weight: 0 U43(x1) weight: 0 #activate(x1) weight: 0 n__i() weight: 0 #U23(x1) weight: 0 #U53(x1) weight: 0 #__(x1,x2) weight: x1 #U43(x1) weight: 0 U23(x1) weight: 0 isNePal(x1) weight: 0 U72(x1) weight: 0 #isQid(x1) weight: 0 #isPal(x1) weight: 0 n__nil() weight: 0 #U52(x1,x2) weight: 0 U12(x1) weight: 0 isQid(x1) weight: 0 n____(x1,x2) weight: (/ 1 2) n__e() weight: 0 o() weight: 0 n__isPalListKind(x1) weight: 0 #U42(x1,x2) weight: 0 #U12(x1) weight: 0 #U62(x1) weight: 0 isList(x1) weight: 0 #isNePal(x1) weight: 0 nil() weight: 0 n__u() weight: 0 #o() weight: 0 U62(x1) weight: 0 #nil() weight: 0 #isList(x1) weight: 0 U32(x1) weight: 0 i() weight: 0 U52(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 e() weight: 0 #U11(x1,x2) weight: 0 U31(x1,x2) weight: 0 #U41(x1,x2,x3) weight: 0 #a() weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2) weight: 0 tt() weight: 0 n__and(x1,x2) weight: 0 #U71(x1,x2) weight: 0 U22(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 isPalListKind(x1) weight: 0 U53(x1) weight: 0 U41(x1,x2,x3) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 __(x1,x2) weight: (/ 1 4) + x1 + x2 #U61(x1,x2) weight: 0 #i() weight: 0 Usable rules: { } Removed DPs: #86 #87 Number of SCCs: 3, DPs: 24, edges: 43 SCC { #6 #45 #76 } Removing DPs: Order(PosReal,>,Sum)... succeeded. a() weight: 0 n__a() weight: 0 #U72(x1) weight: 0 #U32(x1) weight: 0 U21(x1,x2,x3) weight: 0 #isPalListKind(x1) weight: 0 U11(x1,x2) weight: 0 n__o() weight: 0 isNeList(x1) weight: 0 isPal(x1) weight: 0 U42(x1,x2) weight: 0 #e() weight: 0 u() weight: 0 activate(x1) weight: (/ 1 8) + x1 U71(x1,x2) weight: 0 and(x1,x2) weight: (/ 1 8) + x2 #u() weight: 0 #isNeList(x1) weight: 0 U43(x1) weight: 0 #activate(x1) weight: 0 n__i() weight: 0 #U23(x1) weight: 0 #U53(x1) weight: 0 #__(x1,x2) weight: 0 #U43(x1) weight: 0 U23(x1) weight: 0 isNePal(x1) weight: 0 U72(x1) weight: 0 #isQid(x1) weight: 0 #isPal(x1) weight: (/ 1 2) + x1 n__nil() weight: 0 #U52(x1,x2) weight: 0 U12(x1) weight: 0 isQid(x1) weight: 0 n____(x1,x2) weight: (/ 3 8) + x1 + x2 n__e() weight: 0 o() weight: 0 n__isPalListKind(x1) weight: (/ 1 8) #U42(x1,x2) weight: 0 #U12(x1) weight: 0 #U62(x1) weight: 0 isList(x1) weight: 0 #isNePal(x1) weight: x1 nil() weight: 0 n__u() weight: 0 #o() weight: 0 U62(x1) weight: 0 #nil() weight: 0 #isList(x1) weight: 0 U32(x1) weight: 0 i() weight: 0 U52(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 e() weight: 0 #U11(x1,x2) weight: 0 U31(x1,x2) weight: 0 #U41(x1,x2,x3) weight: 0 #a() weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2) weight: 0 tt() weight: 0 n__and(x1,x2) weight: (/ 1 8) + x2 #U71(x1,x2) weight: (/ 1 4) + x2 U22(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 isPalListKind(x1) weight: (/ 1 4) U53(x1) weight: 0 U41(x1,x2,x3) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 __(x1,x2) weight: (/ 3 8) + x1 + x2 #U61(x1,x2) weight: 0 #i() weight: 0 Usable rules: { 1..3 21 32..38 44..62 } Removed DPs: #6 #45 #76 Number of SCCs: 2, DPs: 21, edges: 40 SCC { #12..15 #21 #40 #85 } Removing DPs: Order(PosReal,>,Sum)... succeeded. a() weight: 0 n__a() weight: 0 #U72(x1) weight: 0 #U32(x1) weight: 0 U21(x1,x2,x3) weight: 0 #isPalListKind(x1) weight: x1 U11(x1,x2) weight: 0 n__o() weight: 0 isNeList(x1) weight: 0 isPal(x1) weight: 0 U42(x1,x2) weight: 0 #e() weight: 0 u() weight: 0 activate(x1) weight: (/ 1 8) + x1 U71(x1,x2) weight: 0 and(x1,x2) weight: (/ 1 4) + x2 #u() weight: 0 #isNeList(x1) weight: 0 U43(x1) weight: 0 #activate(x1) weight: x1 n__i() weight: 0 #U23(x1) weight: 0 #U53(x1) weight: 0 #__(x1,x2) weight: 0 #U43(x1) weight: 0 U23(x1) weight: 0 isNePal(x1) weight: 0 U72(x1) weight: 0 #isQid(x1) weight: 0 #isPal(x1) weight: (/ 1 2) + x1 n__nil() weight: 0 #U52(x1,x2) weight: 0 U12(x1) weight: 0 isQid(x1) weight: 0 n____(x1,x2) weight: (/ 1 2) + x1 + x2 n__e() weight: 0 o() weight: 0 n__isPalListKind(x1) weight: (/ 1 8) + x1 #U42(x1,x2) weight: 0 #U12(x1) weight: 0 #U62(x1) weight: 0 isList(x1) weight: 0 #isNePal(x1) weight: x1 nil() weight: 0 n__u() weight: 0 #o() weight: 0 U62(x1) weight: 0 #nil() weight: 0 #isList(x1) weight: 0 U32(x1) weight: 0 i() weight: 0 U52(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 e() weight: 0 #U11(x1,x2) weight: 0 U31(x1,x2) weight: 0 #U41(x1,x2,x3) weight: 0 #a() weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2) weight: 0 tt() weight: 0 n__and(x1,x2) weight: (/ 1 4) + x2 #U71(x1,x2) weight: (/ 1 4) + x2 U22(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 isPalListKind(x1) weight: (/ 1 8) + x1 U53(x1) weight: 0 U41(x1,x2,x3) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: (/ 1 8) + x2 __(x1,x2) weight: (/ 5 8) + x1 + x2 #U61(x1,x2) weight: 0 #i() weight: 0 Usable rules: { 1..3 21 32..38 44..62 } Removed DPs: #12..15 #21 #40 #85 Number of SCCs: 1, DPs: 14, edges: 24 SCC { #16 #17 #25 #26 #30 #38 #41 #42 #54 #60 #64 #78 #90 #93 } Removing DPs: Order(PosReal,>,Sum)... succeeded. a() weight: 0 n__a() weight: 0 #U72(x1) weight: 0 #U32(x1) weight: 0 U21(x1,x2,x3) weight: 0 #isPalListKind(x1) weight: x1 U11(x1,x2) weight: 0 n__o() weight: 0 isNeList(x1) weight: x1 isPal(x1) weight: 0 U42(x1,x2) weight: (/ 1 2) #e() weight: 0 u() weight: 0 activate(x1) weight: (/ 1 16) + x1 U71(x1,x2) weight: 0 and(x1,x2) weight: (/ 1 16) + x2 #u() weight: 0 #isNeList(x1) weight: x1 U43(x1) weight: (/ 9 16) #activate(x1) weight: 0 n__i() weight: 0 #U23(x1) weight: 0 #U53(x1) weight: 0 #__(x1,x2) weight: 0 #U43(x1) weight: 0 U23(x1) weight: 0 isNePal(x1) weight: 0 U72(x1) weight: 0 #isQid(x1) weight: 0 #isPal(x1) weight: (/ 1 4) + x1 n__nil() weight: 0 #U52(x1,x2) weight: (/ 3 8) + x2 U12(x1) weight: 0 isQid(x1) weight: (/ 1 16) n____(x1,x2) weight: (/ 11 16) + x1 + x2 n__e() weight: 0 o() weight: 0 n__isPalListKind(x1) weight: (/ 1 16) + x1 #U42(x1,x2) weight: (/ 1 8) + x2 #U12(x1) weight: 0 #U62(x1) weight: 0 isList(x1) weight: (/ 1 16) #isNePal(x1) weight: x1 nil() weight: 0 n__u() weight: 0 #o() weight: 0 U62(x1) weight: 0 #nil() weight: 0 #isList(x1) weight: (/ 1 4) + x1 U32(x1) weight: (/ 1 16) i() weight: 0 U52(x1,x2) weight: (/ 9 16) U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: (/ 1 2) + x2 + x3 e() weight: 0 #U11(x1,x2) weight: (/ 1 8) + x2 U31(x1,x2) weight: x1 + x2 #U41(x1,x2,x3) weight: (/ 3 8) + x2 + x3 #a() weight: 0 #U21(x1,x2,x3) weight: (/ 9 16) + x2 + x3 #U22(x1,x2) weight: (/ 3 8) + x1 + x2 tt() weight: 0 n__and(x1,x2) weight: (/ 1 16) + x2 #U71(x1,x2) weight: (/ 1 8) + x2 U22(x1,x2) weight: 0 U51(x1,x2,x3) weight: (/ 1 2) + x1 + x3 isPalListKind(x1) weight: (/ 1 16) + x1 U53(x1) weight: (/ 5 8) U41(x1,x2,x3) weight: (/ 7 16) + x1 + x2 + x3 #U31(x1,x2) weight: 0 #and(x1,x2) weight: (/ 1 16) + x2 __(x1,x2) weight: (/ 3 4) + x1 + x2 #U61(x1,x2) weight: 0 #i() weight: 0 Usable rules: { 1..8 21..24 32..62 } Removed DPs: #16 #17 #25 #26 #30 #38 #41 #42 #54 #60 #64 #78 #90 #93 Number of SCCs: 0, DPs: 0, edges: 0 YES