Input TRS: 1: __(__(X,Y),Z) -> __(X,__(Y,Z)) 2: __(X,nil()) -> X 3: __(nil(),X) -> X 4: U11(tt()) -> tt() 5: U21(tt(),V2) -> U22(isList(activate(V2))) 6: U22(tt()) -> tt() 7: U31(tt()) -> tt() 8: U41(tt(),V2) -> U42(isNeList(activate(V2))) 9: U42(tt()) -> tt() 10: U51(tt(),V2) -> U52(isList(activate(V2))) 11: U52(tt()) -> tt() 12: U61(tt()) -> tt() 13: U71(tt(),P) -> U72(isPal(activate(P))) 14: U72(tt()) -> tt() 15: U81(tt()) -> tt() 16: isList(V) -> U11(isNeList(activate(V))) 17: isList(n__nil()) -> tt() 18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 19: isNeList(V) -> U31(isQid(activate(V))) 20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 22: isNePal(V) -> U61(isQid(activate(V))) 23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) 24: isPal(V) -> U81(isNePal(activate(V))) 25: isPal(n__nil()) -> tt() 26: isQid(n__a()) -> tt() 27: isQid(n__e()) -> tt() 28: isQid(n__i()) -> tt() 29: isQid(n__o()) -> tt() 30: isQid(n__u()) -> tt() 31: nil() -> n__nil() 32: __(X1,X2) -> n____(X1,X2) 33: a() -> n__a() 34: e() -> n__e() 35: i() -> n__i() 36: o() -> n__o() 37: u() -> n__u() 38: activate(n__nil()) -> nil() 39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) 40: activate(n__a()) -> a() 41: activate(n__e()) -> e() 42: activate(n__i()) -> i() 43: activate(n__o()) -> o() 44: activate(n__u()) -> u() 45: activate(X) -> X Number of strict rules: 45 Direct Order(PosReal,>,Poly) ... removes: 18 4 15 8 3 16 21 26 19 17 27 22 28 5 10 7 20 25 30 14 12 23 24 11 9 13 6 29 2 a() weight: 0 n__a() weight: 0 U21(x1,x2) weight: (/ 120823 4) + x1 + x2 U11(x1) weight: (/ 1 4) + x1 n__o() weight: 0 isNeList(x1) weight: (/ 115527 4) + x1 isPal(x1) weight: (/ 232677 4) + x1 U42(x1) weight: (/ 1 4) + x1 u() weight: 0 activate(x1) weight: x1 U71(x1,x2) weight: (/ 241645 4) + x1 + x2 n__i() weight: 0 isNePal(x1) weight: (/ 3 4) + x1 U72(x1) weight: (/ 1 4) + x1 n__nil() weight: 0 isQid(x1) weight: (/ 1 4) + x1 n____(x1,x2) weight: 30206 + x1 + x2 n__e() weight: 0 o() weight: 0 isList(x1) weight: (/ 120821 4) + x1 nil() weight: 0 n__u() weight: 0 i() weight: 0 U52(x1) weight: (/ 1 4) + x1 U61(x1) weight: (/ 1 4) + x1 e() weight: 0 U31(x1) weight: (/ 115525 4) + x1 U81(x1) weight: (/ 1 4) + x1 tt() weight: 0 U22(x1) weight: (/ 1 4) + x1 U51(x1,x2) weight: (/ 120823 4) + x1 + x2 U41(x1,x2) weight: (/ 115529 4) + x1 + x2 __(x1,x2) weight: 30206 + x1 + x2 Number of strict rules: 16 Direct Order(PosReal,>,Poly) ... removes: 32 44 39 45 40 38 41 42 43 a() weight: 0 n__a() weight: 0 U21(x1,x2) weight: (/ 3 16) + x1 + x2 U11(x1) weight: x1 n__o() weight: 0 isNeList(x1) weight: (/ 1 16) + x1 isPal(x1) weight: (/ 5 8) + x1 U42(x1) weight: x1 u() weight: 0 activate(x1) weight: (/ 1 16) + 2 * x1 U71(x1,x2) weight: (/ 11 16) + x1 + x2 n__i() weight: 0 isNePal(x1) weight: (/ 3 16) + x1 U72(x1) weight: x1 n__nil() weight: 0 isQid(x1) weight: x1 n____(x1,x2) weight: (/ 5 16) + x1 + x2 n__e() weight: 0 o() weight: 0 isList(x1) weight: (/ 1 8) + x1 nil() weight: 0 n__u() weight: 0 i() weight: 0 U52(x1) weight: x1 U61(x1) weight: (/ 1 16) + x1 e() weight: 0 U31(x1) weight: x1 U81(x1) weight: (/ 1 16) + x1 tt() weight: 0 U22(x1) weight: x1 U51(x1,x2) weight: (/ 3 16) + x1 + x2 U41(x1,x2) weight: (/ 1 8) + x1 + x2 __(x1,x2) weight: (/ 3 8) + x1 + x2 Number of strict rules: 7 Direct Order(PosReal,>,Poly) ... removes: 1 a() weight: 0 n__a() weight: 0 U21(x1,x2) weight: (/ 3 16) + x1 + x2 U11(x1) weight: x1 n__o() weight: 0 isNeList(x1) weight: (/ 1 16) + x1 isPal(x1) weight: (/ 5 8) + x1 U42(x1) weight: x1 u() weight: 0 activate(x1) weight: (/ 1 16) + 2 * x1 U71(x1,x2) weight: (/ 11 16) + x1 + x2 n__i() weight: 0 isNePal(x1) weight: (/ 3 16) + x1 U72(x1) weight: x1 n__nil() weight: 0 isQid(x1) weight: x1 n____(x1,x2) weight: (/ 5 16) + x1 + x2 n__e() weight: 0 o() weight: 0 isList(x1) weight: (/ 1 8) + x1 nil() weight: 0 n__u() weight: 0 i() weight: 0 U52(x1) weight: x1 U61(x1) weight: (/ 1 16) + x1 e() weight: 0 U31(x1) weight: x1 U81(x1) weight: (/ 1 16) + x1 tt() weight: 0 U22(x1) weight: x1 U51(x1,x2) weight: (/ 3 16) + x1 + x2 U41(x1,x2) weight: (/ 1 8) + x1 + x2 __(x1,x2) weight: (/ 3 8) + 2 * x1 + x2 Number of strict rules: 6 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: Number of SCCs: 0, DPs: 0, edges: 0 YES