YES(?,O(n^2)) 44.13/13.83 YES(?,O(n^2)) 44.13/13.84 44.13/13.84 Problem: 44.13/13.84 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.84 __(X,nil()) -> X 44.13/13.84 __(nil(),X) -> X 44.13/13.84 U11(tt()) -> tt() 44.13/13.84 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.84 U22(tt()) -> tt() 44.13/13.84 U31(tt()) -> tt() 44.13/13.84 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.84 U42(tt()) -> tt() 44.13/13.84 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.84 U52(tt()) -> tt() 44.13/13.84 U61(tt()) -> tt() 44.13/13.84 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.84 U72(tt()) -> tt() 44.13/13.84 U81(tt()) -> tt() 44.13/13.84 isList(V) -> U11(isNeList(activate(V))) 44.13/13.84 isList(n__nil()) -> tt() 44.13/13.84 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.84 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.84 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.84 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.84 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.84 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.84 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.84 isPal(n__nil()) -> tt() 44.13/13.84 isQid(n__a()) -> tt() 44.13/13.84 isQid(n__e()) -> tt() 44.13/13.84 isQid(n__i()) -> tt() 44.13/13.84 isQid(n__o()) -> tt() 44.13/13.84 isQid(n__u()) -> tt() 44.13/13.84 nil() -> n__nil() 44.13/13.84 __(X1,X2) -> n____(X1,X2) 44.13/13.84 a() -> n__a() 44.13/13.84 e() -> n__e() 44.13/13.84 i() -> n__i() 44.13/13.84 o() -> n__o() 44.13/13.84 u() -> n__u() 44.13/13.84 activate(n__nil()) -> nil() 44.13/13.84 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.84 activate(n__a()) -> a() 44.13/13.84 activate(n__e()) -> e() 44.13/13.84 activate(n__i()) -> i() 44.13/13.84 activate(n__o()) -> o() 44.13/13.84 activate(n__u()) -> u() 44.13/13.84 activate(X) -> X 44.13/13.84 44.13/13.84 Proof: 44.13/13.84 Complexity Transformation Processor: 44.13/13.84 strict: 44.13/13.84 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.84 __(X,nil()) -> X 44.13/13.84 __(nil(),X) -> X 44.13/13.84 U11(tt()) -> tt() 44.13/13.84 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.84 U22(tt()) -> tt() 44.13/13.84 U31(tt()) -> tt() 44.13/13.84 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.84 U42(tt()) -> tt() 44.13/13.84 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.84 U52(tt()) -> tt() 44.13/13.84 U61(tt()) -> tt() 44.13/13.84 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.84 U72(tt()) -> tt() 44.13/13.84 U81(tt()) -> tt() 44.13/13.84 isList(V) -> U11(isNeList(activate(V))) 44.13/13.84 isList(n__nil()) -> tt() 44.13/13.84 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.84 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.84 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.84 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.84 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.84 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.84 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.84 isPal(n__nil()) -> tt() 44.13/13.84 isQid(n__a()) -> tt() 44.13/13.84 isQid(n__e()) -> tt() 44.13/13.84 isQid(n__i()) -> tt() 44.13/13.84 isQid(n__o()) -> tt() 44.13/13.84 isQid(n__u()) -> tt() 44.13/13.84 nil() -> n__nil() 44.13/13.84 __(X1,X2) -> n____(X1,X2) 44.13/13.84 a() -> n__a() 44.13/13.84 e() -> n__e() 44.13/13.84 i() -> n__i() 44.13/13.84 o() -> n__o() 44.13/13.84 u() -> n__u() 44.13/13.84 activate(n__nil()) -> nil() 44.13/13.84 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.84 activate(n__a()) -> a() 44.13/13.84 activate(n__e()) -> e() 44.13/13.84 activate(n__i()) -> i() 44.13/13.84 activate(n__o()) -> o() 44.13/13.84 activate(n__u()) -> u() 44.13/13.84 activate(X) -> X 44.13/13.84 weak: 44.13/13.84 44.13/13.84 Matrix Interpretation Processor: dim=1 44.13/13.84 44.13/13.84 max_matrix: 44.13/13.84 1 44.13/13.84 interpretation: 44.13/13.84 [u] = 0, 44.13/13.84 44.13/13.84 [o] = 0, 44.13/13.84 44.13/13.84 [i] = 0, 44.13/13.84 44.13/13.84 [e] = 0, 44.13/13.84 44.13/13.84 [a] = 0, 44.13/13.84 44.13/13.84 [n__u] = 3, 44.13/13.84 44.13/13.84 [n__o] = 6, 44.13/13.84 44.13/13.84 [n__i] = 0, 44.13/13.84 44.13/13.84 [n__e] = 8, 44.13/13.84 44.13/13.84 [n__a] = 12, 44.13/13.84 44.13/13.84 [isNePal](x0) = x0 + 14, 44.13/13.84 44.13/13.84 [isQid](x0) = x0 + 1, 44.13/13.84 44.13/13.84 [n____](x0, x1) = x0 + x1 + 1, 44.13/13.84 44.13/13.84 [n__nil] = 4, 44.13/13.84 44.13/13.84 [U81](x0) = x0 + 12, 44.13/13.84 44.13/13.84 [U72](x0) = x0 + 7, 44.13/13.84 44.13/13.84 [isPal](x0) = x0 + 14, 44.13/13.84 44.13/13.84 [U71](x0, x1) = x0 + x1 + 8, 44.13/13.84 44.13/13.84 [U61](x0) = x0 + 8, 44.13/13.84 44.13/13.84 [U52](x0) = x0 + 2, 44.13/13.84 44.13/13.84 [U51](x0, x1) = x0 + x1 + 10, 44.13/13.84 44.13/13.84 [U42](x0) = x0 + 2, 44.13/13.84 44.13/13.84 [isNeList](x0) = x0 + 14, 44.13/13.84 44.13/13.84 [U41](x0, x1) = x0 + x1 + 4, 44.13/13.84 44.13/13.84 [U31](x0) = x0 + 12, 44.13/13.84 44.13/13.84 [U22](x0) = x0 + 12, 44.13/13.84 44.13/13.84 [isList](x0) = x0 + 14, 44.13/13.84 44.13/13.84 [activate](x0) = x0 + 2, 44.13/13.84 44.13/13.84 [U21](x0, x1) = x0 + x1 + 11, 44.13/13.84 44.13/13.84 [U11](x0) = x0 + 14, 44.13/13.84 44.13/13.84 [tt] = 0, 44.13/13.84 44.13/13.84 [nil] = 8, 44.13/13.84 44.13/13.84 [__](x0, x1) = x0 + x1 44.13/13.84 orientation: 44.13/13.84 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 44.13/13.84 44.13/13.84 __(X,nil()) = X + 8 >= X = X 44.13/13.84 44.13/13.84 __(nil(),X) = X + 8 >= X = X 44.13/13.84 44.13/13.84 U11(tt()) = 14 >= 0 = tt() 44.13/13.84 44.13/13.84 U21(tt(),V2) = V2 + 11 >= V2 + 28 = U22(isList(activate(V2))) 44.13/13.84 44.13/13.84 U22(tt()) = 12 >= 0 = tt() 44.13/13.84 44.13/13.84 U31(tt()) = 12 >= 0 = tt() 44.13/13.84 44.13/13.84 U41(tt(),V2) = V2 + 4 >= V2 + 18 = U42(isNeList(activate(V2))) 44.13/13.84 44.13/13.84 U42(tt()) = 2 >= 0 = tt() 44.13/13.84 44.13/13.84 U51(tt(),V2) = V2 + 10 >= V2 + 18 = U52(isList(activate(V2))) 44.13/13.84 44.13/13.84 U52(tt()) = 2 >= 0 = tt() 44.13/13.84 44.13/13.84 U61(tt()) = 8 >= 0 = tt() 44.13/13.84 44.13/13.84 U71(tt(),P) = P + 8 >= P + 23 = U72(isPal(activate(P))) 44.13/13.84 44.13/13.84 U72(tt()) = 7 >= 0 = tt() 44.13/13.84 44.13/13.84 U81(tt()) = 12 >= 0 = tt() 44.13/13.84 44.13/13.84 isList(V) = V + 14 >= V + 30 = U11(isNeList(activate(V))) 44.13/13.84 44.13/13.84 isList(n__nil()) = 18 >= 0 = tt() 44.13/13.84 44.13/13.84 isList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 29 = U21(isList(activate(V1)),activate(V2)) 44.13/13.84 44.13/13.84 isNeList(V) = V + 14 >= V + 15 = U31(isQid(activate(V))) 44.13/13.84 44.13/13.84 isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 22 = U41(isList(activate(V1)),activate(V2)) 44.13/13.84 44.13/13.84 isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 28 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.84 44.13/13.84 isNePal(V) = V + 14 >= V + 11 = U61(isQid(activate(V))) 44.13/13.84 44.13/13.84 isNePal(n____(I,__(P,I))) = 2I + P + 15 >= I + P + 13 = U71(isQid(activate(I)),activate(P)) 44.13/13.84 44.13/13.84 isPal(V) = V + 14 >= V + 28 = U81(isNePal(activate(V))) 44.13/13.84 44.13/13.84 isPal(n__nil()) = 18 >= 0 = tt() 44.13/13.84 44.13/13.84 isQid(n__a()) = 13 >= 0 = tt() 44.13/13.84 44.13/13.84 isQid(n__e()) = 9 >= 0 = tt() 44.13/13.84 44.13/13.84 isQid(n__i()) = 1 >= 0 = tt() 44.13/13.84 44.13/13.84 isQid(n__o()) = 7 >= 0 = tt() 44.13/13.84 44.13/13.84 isQid(n__u()) = 4 >= 0 = tt() 44.13/13.84 44.13/13.84 nil() = 8 >= 4 = n__nil() 44.13/13.84 44.13/13.84 __(X1,X2) = X1 + X2 >= X1 + X2 + 1 = n____(X1,X2) 44.13/13.84 44.13/13.84 a() = 0 >= 12 = n__a() 44.13/13.84 44.13/13.84 e() = 0 >= 8 = n__e() 44.13/13.84 44.13/13.84 i() = 0 >= 0 = n__i() 44.13/13.84 44.13/13.84 o() = 0 >= 6 = n__o() 44.13/13.84 44.13/13.84 u() = 0 >= 3 = n__u() 44.13/13.84 44.13/13.84 activate(n__nil()) = 6 >= 8 = nil() 44.13/13.84 44.13/13.84 activate(n____(X1,X2)) = X1 + X2 + 3 >= X1 + X2 = __(X1,X2) 44.13/13.84 44.13/13.84 activate(n__a()) = 14 >= 0 = a() 44.13/13.84 44.13/13.84 activate(n__e()) = 10 >= 0 = e() 44.13/13.84 44.13/13.84 activate(n__i()) = 2 >= 0 = i() 44.13/13.84 44.13/13.84 activate(n__o()) = 8 >= 0 = o() 44.13/13.84 44.13/13.84 activate(n__u()) = 5 >= 0 = u() 44.13/13.84 44.13/13.84 activate(X) = X + 2 >= X = X 44.13/13.84 problem: 44.13/13.84 strict: 44.13/13.84 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.84 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.84 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.84 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.84 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.84 isList(V) -> U11(isNeList(activate(V))) 44.13/13.84 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.84 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.84 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.84 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.84 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.84 __(X1,X2) -> n____(X1,X2) 44.13/13.84 a() -> n__a() 44.13/13.84 e() -> n__e() 44.13/13.84 i() -> n__i() 44.13/13.84 o() -> n__o() 44.13/13.84 u() -> n__u() 44.13/13.84 activate(n__nil()) -> nil() 44.13/13.84 weak: 44.13/13.84 __(X,nil()) -> X 44.13/13.84 __(nil(),X) -> X 44.13/13.84 U11(tt()) -> tt() 44.13/13.84 U22(tt()) -> tt() 44.13/13.84 U31(tt()) -> tt() 44.13/13.84 U42(tt()) -> tt() 44.13/13.84 U52(tt()) -> tt() 44.13/13.84 U61(tt()) -> tt() 44.13/13.84 U72(tt()) -> tt() 44.13/13.84 U81(tt()) -> tt() 44.13/13.84 isList(n__nil()) -> tt() 44.13/13.84 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.84 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.84 isPal(n__nil()) -> tt() 44.13/13.84 isQid(n__a()) -> tt() 44.13/13.84 isQid(n__e()) -> tt() 44.13/13.84 isQid(n__i()) -> tt() 44.13/13.84 isQid(n__o()) -> tt() 44.13/13.84 isQid(n__u()) -> tt() 44.13/13.84 nil() -> n__nil() 44.13/13.84 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.84 activate(n__a()) -> a() 44.13/13.84 activate(n__e()) -> e() 44.13/13.84 activate(n__i()) -> i() 44.13/13.84 activate(n__o()) -> o() 44.13/13.84 activate(n__u()) -> u() 44.13/13.84 activate(X) -> X 44.13/13.84 Matrix Interpretation Processor: dim=1 44.13/13.84 44.13/13.84 max_matrix: 44.13/13.84 1 44.13/13.84 interpretation: 44.13/13.84 [u] = 0, 44.13/13.84 44.13/13.84 [o] = 0, 44.13/13.84 44.13/13.84 [i] = 2, 44.13/13.84 44.13/13.84 [e] = 1, 44.13/13.84 44.13/13.84 [a] = 1, 44.13/13.84 44.13/13.84 [n__u] = 14, 44.13/13.84 44.13/13.84 [n__o] = 3, 44.13/13.84 44.13/13.84 [n__i] = 2, 44.13/13.84 44.13/13.84 [n__e] = 1, 44.13/13.84 44.13/13.84 [n__a] = 1, 44.13/13.84 44.13/13.84 [isNePal](x0) = x0, 44.13/13.84 44.13/13.84 [isQid](x0) = x0, 44.13/13.84 44.13/13.84 [n____](x0, x1) = x0 + x1, 44.13/13.84 44.13/13.84 [n__nil] = 0, 44.13/13.84 44.13/13.84 [U81](x0) = x0, 44.13/13.84 44.13/13.84 [U72](x0) = x0, 44.13/13.84 44.13/13.84 [isPal](x0) = x0 + 1, 44.13/13.84 44.13/13.84 [U71](x0, x1) = x0 + x1, 44.13/13.84 44.13/13.84 [U61](x0) = x0, 44.13/13.84 44.13/13.84 [U52](x0) = x0, 44.13/13.84 44.13/13.85 [U51](x0, x1) = x0 + x1, 44.13/13.85 44.13/13.85 [U42](x0) = x0 + 14, 44.13/13.85 44.13/13.85 [isNeList](x0) = x0 + 10, 44.13/13.85 44.13/13.85 [U41](x0, x1) = x0 + x1 + 9, 44.13/13.85 44.13/13.85 [U31](x0) = x0 + 8, 44.13/13.85 44.13/13.85 [U22](x0) = x0 + 2, 44.13/13.85 44.13/13.85 [isList](x0) = x0 + 1, 44.13/13.85 44.13/13.85 [activate](x0) = x0, 44.13/13.85 44.13/13.85 [U21](x0, x1) = x0 + x1, 44.13/13.85 44.13/13.85 [U11](x0) = x0 + 12, 44.13/13.85 44.13/13.85 [tt] = 1, 44.13/13.85 44.13/13.85 [nil] = 0, 44.13/13.85 44.13/13.85 [__](x0, x1) = x0 + x1 44.13/13.85 orientation: 44.13/13.85 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 44.13/13.85 44.13/13.85 U21(tt(),V2) = V2 + 1 >= V2 + 3 = U22(isList(activate(V2))) 44.13/13.85 44.13/13.85 U41(tt(),V2) = V2 + 10 >= V2 + 24 = U42(isNeList(activate(V2))) 44.13/13.85 44.13/13.85 U51(tt(),V2) = V2 + 1 >= V2 + 1 = U52(isList(activate(V2))) 44.13/13.85 44.13/13.85 U71(tt(),P) = P + 1 >= P + 1 = U72(isPal(activate(P))) 44.13/13.85 44.13/13.85 isList(V) = V + 1 >= V + 22 = U11(isNeList(activate(V))) 44.13/13.85 44.13/13.85 isList(n____(V1,V2)) = V1 + V2 + 1 >= V1 + V2 + 1 = U21(isList(activate(V1)),activate(V2)) 44.13/13.85 44.13/13.85 isNeList(V) = V + 10 >= V + 8 = U31(isQid(activate(V))) 44.13/13.85 44.13/13.85 isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 10 = U41(isList(activate(V1)),activate(V2)) 44.13/13.85 44.13/13.85 isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 10 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.85 44.13/13.85 isPal(V) = V + 1 >= V = U81(isNePal(activate(V))) 44.13/13.85 44.13/13.85 __(X1,X2) = X1 + X2 >= X1 + X2 = n____(X1,X2) 44.13/13.85 44.13/13.85 a() = 1 >= 1 = n__a() 44.13/13.85 44.13/13.85 e() = 1 >= 1 = n__e() 44.13/13.85 44.13/13.85 i() = 2 >= 2 = n__i() 44.13/13.85 44.13/13.85 o() = 0 >= 3 = n__o() 44.13/13.85 44.13/13.85 u() = 0 >= 14 = n__u() 44.13/13.85 44.13/13.85 activate(n__nil()) = 0 >= 0 = nil() 44.13/13.85 44.13/13.85 __(X,nil()) = X >= X = X 44.13/13.85 44.13/13.85 __(nil(),X) = X >= X = X 44.13/13.85 44.13/13.85 U11(tt()) = 13 >= 1 = tt() 44.13/13.85 44.13/13.85 U22(tt()) = 3 >= 1 = tt() 44.13/13.85 44.13/13.85 U31(tt()) = 9 >= 1 = tt() 44.13/13.85 44.13/13.85 U42(tt()) = 15 >= 1 = tt() 44.13/13.85 44.13/13.85 U52(tt()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 U61(tt()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 U72(tt()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 U81(tt()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 isList(n__nil()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 isNePal(V) = V >= V = U61(isQid(activate(V))) 44.13/13.85 44.13/13.85 isNePal(n____(I,__(P,I))) = 2I + P >= I + P = U71(isQid(activate(I)),activate(P)) 44.13/13.85 44.13/13.85 isPal(n__nil()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__a()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__e()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__i()) = 2 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__o()) = 3 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__u()) = 14 >= 1 = tt() 44.13/13.85 44.13/13.85 nil() = 0 >= 0 = n__nil() 44.13/13.85 44.13/13.85 activate(n____(X1,X2)) = X1 + X2 >= X1 + X2 = __(X1,X2) 44.13/13.85 44.13/13.85 activate(n__a()) = 1 >= 1 = a() 44.13/13.85 44.13/13.85 activate(n__e()) = 1 >= 1 = e() 44.13/13.85 44.13/13.85 activate(n__i()) = 2 >= 2 = i() 44.13/13.85 44.13/13.85 activate(n__o()) = 3 >= 0 = o() 44.13/13.85 44.13/13.85 activate(n__u()) = 14 >= 0 = u() 44.13/13.85 44.13/13.85 activate(X) = X >= X = X 44.13/13.85 problem: 44.13/13.85 strict: 44.13/13.85 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.85 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.85 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.85 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.85 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.85 isList(V) -> U11(isNeList(activate(V))) 44.13/13.85 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.85 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.85 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.85 __(X1,X2) -> n____(X1,X2) 44.13/13.85 a() -> n__a() 44.13/13.85 e() -> n__e() 44.13/13.85 i() -> n__i() 44.13/13.85 o() -> n__o() 44.13/13.85 u() -> n__u() 44.13/13.85 activate(n__nil()) -> nil() 44.13/13.85 weak: 44.13/13.85 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.85 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.85 __(X,nil()) -> X 44.13/13.85 __(nil(),X) -> X 44.13/13.85 U11(tt()) -> tt() 44.13/13.85 U22(tt()) -> tt() 44.13/13.85 U31(tt()) -> tt() 44.13/13.85 U42(tt()) -> tt() 44.13/13.85 U52(tt()) -> tt() 44.13/13.85 U61(tt()) -> tt() 44.13/13.85 U72(tt()) -> tt() 44.13/13.85 U81(tt()) -> tt() 44.13/13.85 isList(n__nil()) -> tt() 44.13/13.85 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.85 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.85 isPal(n__nil()) -> tt() 44.13/13.85 isQid(n__a()) -> tt() 44.13/13.85 isQid(n__e()) -> tt() 44.13/13.85 isQid(n__i()) -> tt() 44.13/13.85 isQid(n__o()) -> tt() 44.13/13.85 isQid(n__u()) -> tt() 44.13/13.85 nil() -> n__nil() 44.13/13.85 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.85 activate(n__a()) -> a() 44.13/13.85 activate(n__e()) -> e() 44.13/13.85 activate(n__i()) -> i() 44.13/13.85 activate(n__o()) -> o() 44.13/13.85 activate(n__u()) -> u() 44.13/13.85 activate(X) -> X 44.13/13.85 Matrix Interpretation Processor: dim=1 44.13/13.85 44.13/13.85 max_matrix: 44.13/13.85 1 44.13/13.85 interpretation: 44.13/13.85 [u] = 0, 44.13/13.85 44.13/13.85 [o] = 0, 44.13/13.85 44.13/13.85 [i] = 0, 44.13/13.85 44.13/13.85 [e] = 0, 44.13/13.85 44.13/13.85 [a] = 1, 44.13/13.85 44.13/13.85 [n__u] = 3, 44.13/13.85 44.13/13.85 [n__o] = 7, 44.13/13.85 44.13/13.85 [n__i] = 8, 44.13/13.85 44.13/13.85 [n__e] = 1, 44.13/13.85 44.13/13.85 [n__a] = 1, 44.13/13.85 44.13/13.85 [isNePal](x0) = x0 + 13, 44.13/13.85 44.13/13.85 [isQid](x0) = x0, 44.13/13.85 44.13/13.85 [n____](x0, x1) = x0 + x1 + 10, 44.13/13.85 44.13/13.85 [n__nil] = 2, 44.13/13.85 44.13/13.85 [U81](x0) = x0 + 1, 44.13/13.85 44.13/13.85 [U72](x0) = x0 + 7, 44.13/13.85 44.13/13.85 [isPal](x0) = x0 + 14, 44.13/13.85 44.13/13.85 [U71](x0, x1) = x0 + x1 + 1, 44.13/13.85 44.13/13.85 [U61](x0) = x0 + 12, 44.13/13.85 44.13/13.85 [U52](x0) = x0 + 8, 44.13/13.85 44.13/13.85 [U51](x0, x1) = x0 + x1 + 2, 44.13/13.85 44.13/13.85 [U42](x0) = x0 + 10, 44.13/13.85 44.13/13.85 [isNeList](x0) = x0, 44.13/13.85 44.13/13.85 [U41](x0, x1) = x0 + x1 + 6, 44.13/13.85 44.13/13.85 [U31](x0) = x0, 44.13/13.85 44.13/13.85 [U22](x0) = x0 + 4, 44.13/13.85 44.13/13.85 [isList](x0) = x0 + 14, 44.13/13.85 44.13/13.85 [activate](x0) = x0, 44.13/13.85 44.13/13.85 [U21](x0, x1) = x0 + x1, 44.13/13.85 44.13/13.85 [U11](x0) = x0 + 11, 44.13/13.85 44.13/13.85 [tt] = 1, 44.13/13.85 44.13/13.85 [nil] = 3, 44.13/13.85 44.13/13.85 [__](x0, x1) = x0 + x1 + 3 44.13/13.85 orientation: 44.13/13.85 __(__(X,Y),Z) = X + Y + Z + 6 >= X + Y + Z + 6 = __(X,__(Y,Z)) 44.13/13.85 44.13/13.85 U21(tt(),V2) = V2 + 1 >= V2 + 18 = U22(isList(activate(V2))) 44.13/13.85 44.13/13.85 U41(tt(),V2) = V2 + 7 >= V2 + 10 = U42(isNeList(activate(V2))) 44.13/13.85 44.13/13.85 U51(tt(),V2) = V2 + 3 >= V2 + 22 = U52(isList(activate(V2))) 44.13/13.85 44.13/13.85 U71(tt(),P) = P + 2 >= P + 21 = U72(isPal(activate(P))) 44.13/13.85 44.13/13.85 isList(V) = V + 14 >= V + 11 = U11(isNeList(activate(V))) 44.13/13.85 44.13/13.85 isList(n____(V1,V2)) = V1 + V2 + 24 >= V1 + V2 + 14 = U21(isList(activate(V1)),activate(V2)) 44.13/13.85 44.13/13.85 isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 20 = U41(isList(activate(V1)),activate(V2)) 44.13/13.85 44.13/13.85 isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 2 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.85 44.13/13.85 __(X1,X2) = X1 + X2 + 3 >= X1 + X2 + 10 = n____(X1,X2) 44.13/13.85 44.13/13.85 a() = 1 >= 1 = n__a() 44.13/13.85 44.13/13.85 e() = 0 >= 1 = n__e() 44.13/13.85 44.13/13.85 i() = 0 >= 8 = n__i() 44.13/13.85 44.13/13.85 o() = 0 >= 7 = n__o() 44.13/13.85 44.13/13.85 u() = 0 >= 3 = n__u() 44.13/13.85 44.13/13.85 activate(n__nil()) = 2 >= 3 = nil() 44.13/13.85 44.13/13.85 isNeList(V) = V >= V = U31(isQid(activate(V))) 44.13/13.85 44.13/13.85 isPal(V) = V + 14 >= V + 14 = U81(isNePal(activate(V))) 44.13/13.85 44.13/13.85 __(X,nil()) = X + 6 >= X = X 44.13/13.85 44.13/13.85 __(nil(),X) = X + 6 >= X = X 44.13/13.85 44.13/13.85 U11(tt()) = 12 >= 1 = tt() 44.13/13.85 44.13/13.85 U22(tt()) = 5 >= 1 = tt() 44.13/13.85 44.13/13.85 U31(tt()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 U42(tt()) = 11 >= 1 = tt() 44.13/13.85 44.13/13.85 U52(tt()) = 9 >= 1 = tt() 44.13/13.85 44.13/13.85 U61(tt()) = 13 >= 1 = tt() 44.13/13.85 44.13/13.85 U72(tt()) = 8 >= 1 = tt() 44.13/13.85 44.13/13.85 U81(tt()) = 2 >= 1 = tt() 44.13/13.85 44.13/13.85 isList(n__nil()) = 16 >= 1 = tt() 44.13/13.85 44.13/13.85 isNePal(V) = V + 13 >= V + 12 = U61(isQid(activate(V))) 44.13/13.85 44.13/13.85 isNePal(n____(I,__(P,I))) = 2I + P + 26 >= I + P + 1 = U71(isQid(activate(I)),activate(P)) 44.13/13.85 44.13/13.85 isPal(n__nil()) = 16 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__a()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__e()) = 1 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__i()) = 8 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__o()) = 7 >= 1 = tt() 44.13/13.85 44.13/13.85 isQid(n__u()) = 3 >= 1 = tt() 44.13/13.85 44.13/13.85 nil() = 3 >= 2 = n__nil() 44.13/13.85 44.13/13.85 activate(n____(X1,X2)) = X1 + X2 + 10 >= X1 + X2 + 3 = __(X1,X2) 44.13/13.85 44.13/13.85 activate(n__a()) = 1 >= 1 = a() 44.13/13.85 44.13/13.85 activate(n__e()) = 1 >= 0 = e() 44.13/13.85 44.13/13.85 activate(n__i()) = 8 >= 0 = i() 44.13/13.85 44.13/13.85 activate(n__o()) = 7 >= 0 = o() 44.13/13.85 44.13/13.85 activate(n__u()) = 3 >= 0 = u() 44.13/13.85 44.13/13.85 activate(X) = X >= X = X 44.13/13.85 problem: 44.13/13.85 strict: 44.13/13.85 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.85 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.85 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.85 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.85 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.85 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.85 __(X1,X2) -> n____(X1,X2) 44.13/13.85 a() -> n__a() 44.13/13.85 e() -> n__e() 44.13/13.85 i() -> n__i() 44.13/13.85 o() -> n__o() 44.13/13.85 u() -> n__u() 44.13/13.85 activate(n__nil()) -> nil() 44.13/13.85 weak: 44.13/13.85 isList(V) -> U11(isNeList(activate(V))) 44.13/13.85 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.85 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.85 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.85 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.85 __(X,nil()) -> X 44.13/13.85 __(nil(),X) -> X 44.13/13.85 U11(tt()) -> tt() 44.13/13.85 U22(tt()) -> tt() 44.13/13.85 U31(tt()) -> tt() 44.13/13.85 U42(tt()) -> tt() 44.13/13.85 U52(tt()) -> tt() 44.13/13.85 U61(tt()) -> tt() 44.13/13.85 U72(tt()) -> tt() 44.13/13.85 U81(tt()) -> tt() 44.13/13.85 isList(n__nil()) -> tt() 44.13/13.85 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.85 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.85 isPal(n__nil()) -> tt() 44.13/13.85 isQid(n__a()) -> tt() 44.13/13.85 isQid(n__e()) -> tt() 44.13/13.85 isQid(n__i()) -> tt() 44.13/13.85 isQid(n__o()) -> tt() 44.13/13.85 isQid(n__u()) -> tt() 44.13/13.85 nil() -> n__nil() 44.13/13.85 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.85 activate(n__a()) -> a() 44.13/13.85 activate(n__e()) -> e() 44.13/13.85 activate(n__i()) -> i() 44.13/13.85 activate(n__o()) -> o() 44.13/13.85 activate(n__u()) -> u() 44.13/13.85 activate(X) -> X 44.13/13.85 Matrix Interpretation Processor: dim=1 44.13/13.85 44.13/13.85 max_matrix: 44.13/13.85 1 44.13/13.85 interpretation: 44.13/13.85 [u] = 0, 44.13/13.85 44.13/13.85 [o] = 0, 44.13/13.85 44.13/13.85 [i] = 0, 44.13/13.85 44.13/13.85 [e] = 0, 44.13/13.85 44.13/13.85 [a] = 0, 44.13/13.85 44.13/13.85 [n__u] = 0, 44.13/13.85 44.13/13.85 [n__o] = 0, 44.13/13.85 44.13/13.85 [n__i] = 0, 44.13/13.85 44.13/13.85 [n__e] = 11, 44.13/13.85 44.13/13.85 [n__a] = 4, 44.13/13.85 44.13/13.85 [isNePal](x0) = x0 + 8, 44.13/13.85 44.13/13.85 [isQid](x0) = x0, 44.13/13.85 44.13/13.85 [n____](x0, x1) = x0 + x1 + 4, 44.13/13.85 44.13/13.85 [n__nil] = 0, 44.13/13.85 44.13/13.85 [U81](x0) = x0 + 4, 44.13/13.85 44.13/13.85 [U72](x0) = x0 + 4, 44.13/13.85 44.13/13.85 [isPal](x0) = x0 + 12, 44.13/13.85 44.13/13.85 [U71](x0, x1) = x0 + x1 + 8, 44.13/13.85 44.13/13.85 [U61](x0) = x0 + 2, 44.13/13.85 44.13/13.85 [U52](x0) = x0 + 13, 44.13/13.85 44.13/13.85 [U51](x0, x1) = x0 + x1 + 4, 44.13/13.85 44.13/13.85 [U42](x0) = x0 + 2, 44.13/13.85 44.13/13.85 [isNeList](x0) = x0 + 3, 44.13/13.85 44.13/13.85 [U41](x0, x1) = x0 + x1 + 6, 44.13/13.85 44.13/13.85 [U31](x0) = x0 + 3, 44.13/13.85 44.13/13.85 [U22](x0) = x0 + 8, 44.13/13.85 44.13/13.85 [isList](x0) = x0 + 11, 44.13/13.85 44.13/13.85 [activate](x0) = x0, 44.13/13.85 44.13/13.85 [U21](x0, x1) = x0 + x1 + 4, 44.13/13.85 44.13/13.85 [U11](x0) = x0 + 8, 44.13/13.85 44.13/13.85 [tt] = 0, 44.13/13.85 44.13/13.85 [nil] = 0, 44.13/13.85 44.13/13.85 [__](x0, x1) = x0 + x1 44.13/13.85 orientation: 44.13/13.85 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 44.13/13.85 44.13/13.85 U21(tt(),V2) = V2 + 4 >= V2 + 19 = U22(isList(activate(V2))) 44.13/13.85 44.13/13.85 U41(tt(),V2) = V2 + 6 >= V2 + 5 = U42(isNeList(activate(V2))) 44.13/13.85 44.13/13.85 U51(tt(),V2) = V2 + 4 >= V2 + 24 = U52(isList(activate(V2))) 44.13/13.85 44.13/13.85 U71(tt(),P) = P + 8 >= P + 16 = U72(isPal(activate(P))) 44.13/13.85 44.13/13.85 isNeList(n____(V1,V2)) = V1 + V2 + 7 >= V1 + V2 + 17 = U41(isList(activate(V1)),activate(V2)) 44.13/13.85 44.13/13.85 __(X1,X2) = X1 + X2 >= X1 + X2 + 4 = n____(X1,X2) 44.13/13.85 44.13/13.85 a() = 0 >= 4 = n__a() 44.13/13.86 44.13/13.86 e() = 0 >= 11 = n__e() 44.13/13.86 44.13/13.86 i() = 0 >= 0 = n__i() 44.13/13.86 44.13/13.86 o() = 0 >= 0 = n__o() 44.13/13.86 44.13/13.86 u() = 0 >= 0 = n__u() 44.13/13.86 44.13/13.86 activate(n__nil()) = 0 >= 0 = nil() 44.13/13.86 44.13/13.86 isList(V) = V + 11 >= V + 11 = U11(isNeList(activate(V))) 44.13/13.86 44.13/13.86 isList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 15 = U21(isList(activate(V1)),activate(V2)) 44.13/13.86 44.13/13.86 isNeList(n____(V1,V2)) = V1 + V2 + 7 >= V1 + V2 + 7 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.86 44.13/13.86 isNeList(V) = V + 3 >= V + 3 = U31(isQid(activate(V))) 44.13/13.86 44.13/13.86 isPal(V) = V + 12 >= V + 12 = U81(isNePal(activate(V))) 44.13/13.86 44.13/13.86 __(X,nil()) = X >= X = X 44.13/13.86 44.13/13.86 __(nil(),X) = X >= X = X 44.13/13.86 44.13/13.86 U11(tt()) = 8 >= 0 = tt() 44.13/13.86 44.13/13.86 U22(tt()) = 8 >= 0 = tt() 44.13/13.86 44.13/13.86 U31(tt()) = 3 >= 0 = tt() 44.13/13.86 44.13/13.86 U42(tt()) = 2 >= 0 = tt() 44.13/13.86 44.13/13.86 U52(tt()) = 13 >= 0 = tt() 44.13/13.86 44.13/13.86 U61(tt()) = 2 >= 0 = tt() 44.13/13.86 44.13/13.86 U72(tt()) = 4 >= 0 = tt() 44.13/13.86 44.13/13.86 U81(tt()) = 4 >= 0 = tt() 44.13/13.86 44.13/13.86 isList(n__nil()) = 11 >= 0 = tt() 44.13/13.86 44.13/13.86 isNePal(V) = V + 8 >= V + 2 = U61(isQid(activate(V))) 44.13/13.86 44.13/13.86 isNePal(n____(I,__(P,I))) = 2I + P + 12 >= I + P + 8 = U71(isQid(activate(I)),activate(P)) 44.13/13.86 44.13/13.86 isPal(n__nil()) = 12 >= 0 = tt() 44.13/13.86 44.13/13.86 isQid(n__a()) = 4 >= 0 = tt() 44.13/13.86 44.13/13.86 isQid(n__e()) = 11 >= 0 = tt() 44.13/13.86 44.13/13.86 isQid(n__i()) = 0 >= 0 = tt() 44.13/13.86 44.13/13.86 isQid(n__o()) = 0 >= 0 = tt() 44.13/13.86 44.13/13.86 isQid(n__u()) = 0 >= 0 = tt() 44.13/13.86 44.13/13.86 nil() = 0 >= 0 = n__nil() 44.13/13.86 44.13/13.86 activate(n____(X1,X2)) = X1 + X2 + 4 >= X1 + X2 = __(X1,X2) 44.13/13.86 44.13/13.86 activate(n__a()) = 4 >= 0 = a() 44.13/13.86 44.13/13.86 activate(n__e()) = 11 >= 0 = e() 44.13/13.86 44.13/13.86 activate(n__i()) = 0 >= 0 = i() 44.13/13.86 44.13/13.86 activate(n__o()) = 0 >= 0 = o() 44.13/13.86 44.13/13.86 activate(n__u()) = 0 >= 0 = u() 44.13/13.86 44.13/13.86 activate(X) = X >= X = X 44.13/13.86 problem: 44.13/13.86 strict: 44.13/13.86 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.86 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.86 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.86 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.86 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.86 __(X1,X2) -> n____(X1,X2) 44.13/13.86 a() -> n__a() 44.13/13.86 e() -> n__e() 44.13/13.86 i() -> n__i() 44.13/13.86 o() -> n__o() 44.13/13.86 u() -> n__u() 44.13/13.86 activate(n__nil()) -> nil() 44.13/13.86 weak: 44.13/13.86 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.86 isList(V) -> U11(isNeList(activate(V))) 44.13/13.86 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.86 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.86 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.86 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.86 __(X,nil()) -> X 44.13/13.86 __(nil(),X) -> X 44.13/13.86 U11(tt()) -> tt() 44.13/13.86 U22(tt()) -> tt() 44.13/13.86 U31(tt()) -> tt() 44.13/13.86 U42(tt()) -> tt() 44.13/13.86 U52(tt()) -> tt() 44.13/13.86 U61(tt()) -> tt() 44.13/13.86 U72(tt()) -> tt() 44.13/13.86 U81(tt()) -> tt() 44.13/13.86 isList(n__nil()) -> tt() 44.13/13.86 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.86 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.86 isPal(n__nil()) -> tt() 44.13/13.86 isQid(n__a()) -> tt() 44.13/13.86 isQid(n__e()) -> tt() 44.13/13.86 isQid(n__i()) -> tt() 44.13/13.86 isQid(n__o()) -> tt() 44.13/13.86 isQid(n__u()) -> tt() 44.13/13.86 nil() -> n__nil() 44.13/13.86 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.86 activate(n__a()) -> a() 44.13/13.86 activate(n__e()) -> e() 44.13/13.86 activate(n__i()) -> i() 44.13/13.86 activate(n__o()) -> o() 44.13/13.86 activate(n__u()) -> u() 44.13/13.86 activate(X) -> X 44.13/13.86 Matrix Interpretation Processor: dim=1 44.13/13.86 44.13/13.86 max_matrix: 44.13/13.86 1 44.13/13.86 interpretation: 44.13/13.86 [u] = 0, 44.13/13.86 44.13/13.86 [o] = 0, 44.13/13.86 44.13/13.86 [i] = 17, 44.13/13.86 44.13/13.86 [e] = 17, 44.13/13.86 44.13/13.86 [a] = 0, 44.13/13.86 44.13/13.86 [n__u] = 7, 44.13/13.86 44.13/13.86 [n__o] = 9, 44.13/13.86 44.13/13.86 [n__i] = 7, 44.13/13.86 44.13/13.86 [n__e] = 16, 44.13/13.86 44.13/13.86 [n__a] = 7, 44.13/13.86 44.13/13.86 [isNePal](x0) = x0 + 24, 44.13/13.86 44.13/13.86 [isQid](x0) = x0 + 2, 44.13/13.86 44.13/13.86 [n____](x0, x1) = x0 + x1 + 56, 44.13/13.86 44.13/13.86 [n__nil] = 17, 44.13/13.86 44.13/13.86 [U81](x0) = x0 + 8, 44.13/13.86 44.13/13.86 [U72](x0) = x0 + 3, 44.13/13.86 44.13/13.86 [isPal](x0) = x0 + 57, 44.13/13.86 44.13/13.86 [U71](x0, x1) = x0 + x1 + 58, 44.13/13.86 44.13/13.86 [U61](x0) = x0, 44.13/13.86 44.13/13.86 [U52](x0) = x0 + 20, 44.13/13.86 44.13/13.86 [U51](x0, x1) = x0 + x1 + 32, 44.13/13.86 44.13/13.86 [U42](x0) = x0 + 11, 44.13/13.86 44.13/13.86 [isNeList](x0) = x0 + 40, 44.13/13.86 44.13/13.86 [U41](x0, x1) = x0 + x1 + 52, 44.13/13.86 44.13/13.86 [U31](x0) = x0 + 17, 44.13/13.86 44.13/13.86 [U22](x0) = x0 + 15, 44.13/13.86 44.13/13.86 [isList](x0) = x0 + 55, 44.13/13.86 44.13/13.86 [activate](x0) = x0 + 10, 44.13/13.86 44.13/13.86 [U21](x0, x1) = x0 + x1 + 24, 44.13/13.86 44.13/13.86 [U11](x0) = x0 + 5, 44.13/13.86 44.13/13.86 [tt] = 9, 44.13/13.86 44.13/13.86 [nil] = 17, 44.13/13.86 44.13/13.86 [__](x0, x1) = x0 + x1 44.13/13.86 orientation: 44.13/13.86 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 44.13/13.86 44.13/13.86 U21(tt(),V2) = V2 + 33 >= V2 + 80 = U22(isList(activate(V2))) 44.13/13.86 44.13/13.86 U51(tt(),V2) = V2 + 41 >= V2 + 85 = U52(isList(activate(V2))) 44.13/13.86 44.13/13.86 U71(tt(),P) = P + 67 >= P + 70 = U72(isPal(activate(P))) 44.13/13.86 44.13/13.86 isNeList(n____(V1,V2)) = V1 + V2 + 96 >= V1 + V2 + 127 = U41(isList(activate(V1)),activate(V2)) 44.13/13.86 44.13/13.86 __(X1,X2) = X1 + X2 >= X1 + X2 + 56 = n____(X1,X2) 44.13/13.86 44.13/13.86 a() = 0 >= 7 = n__a() 44.13/13.86 44.13/13.86 e() = 17 >= 16 = n__e() 44.13/13.86 44.13/13.86 i() = 17 >= 7 = n__i() 44.13/13.86 44.13/13.86 o() = 0 >= 9 = n__o() 44.13/13.86 44.13/13.86 u() = 0 >= 7 = n__u() 44.13/13.86 44.13/13.86 activate(n__nil()) = 27 >= 17 = nil() 44.13/13.86 44.13/13.86 U41(tt(),V2) = V2 + 61 >= V2 + 61 = U42(isNeList(activate(V2))) 44.13/13.86 44.13/13.86 isList(V) = V + 55 >= V + 55 = U11(isNeList(activate(V))) 44.13/13.86 44.13/13.86 isList(n____(V1,V2)) = V1 + V2 + 111 >= V1 + V2 + 99 = U21(isList(activate(V1)),activate(V2)) 44.13/13.86 44.13/13.86 isNeList(n____(V1,V2)) = V1 + V2 + 96 >= V1 + V2 + 92 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.86 44.13/13.86 isNeList(V) = V + 40 >= V + 29 = U31(isQid(activate(V))) 44.13/13.86 44.13/13.86 isPal(V) = V + 57 >= V + 42 = U81(isNePal(activate(V))) 44.13/13.86 44.13/13.86 __(X,nil()) = X + 17 >= X = X 44.13/13.86 44.13/13.86 __(nil(),X) = X + 17 >= X = X 44.13/13.86 44.13/13.86 U11(tt()) = 14 >= 9 = tt() 44.13/13.86 44.13/13.86 U22(tt()) = 24 >= 9 = tt() 44.13/13.86 44.13/13.86 U31(tt()) = 26 >= 9 = tt() 44.13/13.86 44.13/13.86 U42(tt()) = 20 >= 9 = tt() 44.13/13.86 44.13/13.86 U52(tt()) = 29 >= 9 = tt() 44.13/13.86 44.13/13.86 U61(tt()) = 9 >= 9 = tt() 44.13/13.86 44.13/13.86 U72(tt()) = 12 >= 9 = tt() 44.13/13.86 44.13/13.86 U81(tt()) = 17 >= 9 = tt() 44.13/13.86 44.13/13.86 isList(n__nil()) = 72 >= 9 = tt() 44.13/13.86 44.13/13.86 isNePal(V) = V + 24 >= V + 12 = U61(isQid(activate(V))) 44.13/13.86 44.13/13.86 isNePal(n____(I,__(P,I))) = 2I + P + 80 >= I + P + 80 = U71(isQid(activate(I)),activate(P)) 44.13/13.86 44.13/13.86 isPal(n__nil()) = 74 >= 9 = tt() 44.13/13.86 44.13/13.86 isQid(n__a()) = 9 >= 9 = tt() 44.13/13.86 44.13/13.86 isQid(n__e()) = 18 >= 9 = tt() 44.13/13.86 44.13/13.86 isQid(n__i()) = 9 >= 9 = tt() 44.13/13.86 44.13/13.86 isQid(n__o()) = 11 >= 9 = tt() 44.13/13.86 44.13/13.86 isQid(n__u()) = 9 >= 9 = tt() 44.13/13.86 44.13/13.86 nil() = 17 >= 17 = n__nil() 44.13/13.86 44.13/13.86 activate(n____(X1,X2)) = X1 + X2 + 66 >= X1 + X2 = __(X1,X2) 44.13/13.86 44.13/13.86 activate(n__a()) = 17 >= 0 = a() 44.13/13.86 44.13/13.86 activate(n__e()) = 26 >= 17 = e() 44.13/13.86 44.13/13.86 activate(n__i()) = 17 >= 17 = i() 44.13/13.86 44.13/13.86 activate(n__o()) = 19 >= 0 = o() 44.13/13.86 44.13/13.86 activate(n__u()) = 17 >= 0 = u() 44.13/13.86 44.13/13.86 activate(X) = X + 10 >= X = X 44.13/13.86 problem: 44.13/13.86 strict: 44.13/13.86 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.86 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.86 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.86 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.86 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.86 __(X1,X2) -> n____(X1,X2) 44.13/13.86 a() -> n__a() 44.13/13.86 o() -> n__o() 44.13/13.86 u() -> n__u() 44.13/13.86 weak: 44.13/13.86 e() -> n__e() 44.13/13.86 i() -> n__i() 44.13/13.86 activate(n__nil()) -> nil() 44.13/13.86 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.86 isList(V) -> U11(isNeList(activate(V))) 44.13/13.86 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.86 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.86 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.86 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.86 __(X,nil()) -> X 44.13/13.86 __(nil(),X) -> X 44.13/13.86 U11(tt()) -> tt() 44.13/13.86 U22(tt()) -> tt() 44.13/13.86 U31(tt()) -> tt() 44.13/13.86 U42(tt()) -> tt() 44.13/13.86 U52(tt()) -> tt() 44.13/13.86 U61(tt()) -> tt() 44.13/13.86 U72(tt()) -> tt() 44.13/13.86 U81(tt()) -> tt() 44.13/13.86 isList(n__nil()) -> tt() 44.13/13.86 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.86 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.86 isPal(n__nil()) -> tt() 44.13/13.86 isQid(n__a()) -> tt() 44.13/13.86 isQid(n__e()) -> tt() 44.13/13.86 isQid(n__i()) -> tt() 44.13/13.86 isQid(n__o()) -> tt() 44.13/13.86 isQid(n__u()) -> tt() 44.13/13.86 nil() -> n__nil() 44.13/13.86 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.86 activate(n__a()) -> a() 44.13/13.86 activate(n__e()) -> e() 44.13/13.86 activate(n__i()) -> i() 44.13/13.86 activate(n__o()) -> o() 44.13/13.87 activate(n__u()) -> u() 44.13/13.87 activate(X) -> X 44.13/13.87 Matrix Interpretation Processor: dim=1 44.13/13.87 44.13/13.87 max_matrix: 44.13/13.87 1 44.13/13.87 interpretation: 44.13/13.87 [u] = 0, 44.13/13.87 44.13/13.87 [o] = 0, 44.13/13.87 44.13/13.87 [i] = 3, 44.13/13.87 44.13/13.87 [e] = 3, 44.13/13.87 44.13/13.87 [a] = 0, 44.13/13.87 44.13/13.87 [n__u] = 3, 44.13/13.87 44.13/13.87 [n__o] = 3, 44.13/13.87 44.13/13.87 [n__i] = 3, 44.13/13.87 44.13/13.87 [n__e] = 3, 44.13/13.87 44.13/13.87 [n__a] = 3, 44.13/13.87 44.13/13.87 [isNePal](x0) = x0 + 6, 44.13/13.87 44.13/13.87 [isQid](x0) = x0 + 4, 44.13/13.87 44.13/13.87 [n____](x0, x1) = x0 + x1 + 4, 44.13/13.87 44.13/13.87 [n__nil] = 0, 44.13/13.87 44.13/13.87 [U81](x0) = x0 + 1, 44.13/13.87 44.13/13.87 [U72](x0) = x0, 44.13/13.87 44.13/13.87 [isPal](x0) = x0 + 7, 44.13/13.87 44.13/13.87 [U71](x0, x1) = x0 + x1 + 4, 44.13/13.87 44.13/13.87 [U61](x0) = x0, 44.13/13.87 44.13/13.87 [U52](x0) = x0 + 13, 44.13/13.87 44.13/13.87 [U51](x0, x1) = x0 + x1 + 4, 44.13/13.87 44.13/13.87 [U42](x0) = x0 + 8, 44.13/13.87 44.13/13.87 [isNeList](x0) = x0 + 8, 44.13/13.87 44.13/13.87 [U41](x0, x1) = x0 + x1 + 9, 44.13/13.87 44.13/13.87 [U31](x0) = x0 + 4, 44.13/13.87 44.13/13.87 [U22](x0) = x0 + 1, 44.13/13.87 44.13/13.87 [isList](x0) = x0 + 8, 44.13/13.87 44.13/13.87 [activate](x0) = x0, 44.13/13.87 44.13/13.87 [U21](x0, x1) = x0 + x1 + 4, 44.13/13.87 44.13/13.87 [U11](x0) = x0, 44.13/13.87 44.13/13.87 [tt] = 7, 44.13/13.87 44.13/13.87 [nil] = 0, 44.13/13.87 44.13/13.87 [__](x0, x1) = x0 + x1 44.13/13.87 orientation: 44.13/13.87 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 44.13/13.87 44.13/13.87 U21(tt(),V2) = V2 + 11 >= V2 + 9 = U22(isList(activate(V2))) 44.13/13.87 44.13/13.87 U51(tt(),V2) = V2 + 11 >= V2 + 21 = U52(isList(activate(V2))) 44.13/13.87 44.13/13.87 U71(tt(),P) = P + 11 >= P + 7 = U72(isPal(activate(P))) 44.13/13.87 44.13/13.87 isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 17 = U41(isList(activate(V1)),activate(V2)) 44.13/13.87 44.13/13.87 __(X1,X2) = X1 + X2 >= X1 + X2 + 4 = n____(X1,X2) 44.13/13.87 44.13/13.87 a() = 0 >= 3 = n__a() 44.13/13.87 44.13/13.87 o() = 0 >= 3 = n__o() 44.13/13.87 44.13/13.87 u() = 0 >= 3 = n__u() 44.13/13.87 44.13/13.87 e() = 3 >= 3 = n__e() 44.13/13.87 44.13/13.87 i() = 3 >= 3 = n__i() 44.13/13.87 44.13/13.87 activate(n__nil()) = 0 >= 0 = nil() 44.13/13.87 44.13/13.87 U41(tt(),V2) = V2 + 16 >= V2 + 16 = U42(isNeList(activate(V2))) 44.13/13.87 44.13/13.87 isList(V) = V + 8 >= V + 8 = U11(isNeList(activate(V))) 44.13/13.87 44.13/13.87 isList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U21(isList(activate(V1)),activate(V2)) 44.13/13.87 44.13/13.87 isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.87 44.13/13.87 isNeList(V) = V + 8 >= V + 8 = U31(isQid(activate(V))) 44.13/13.87 44.13/13.87 isPal(V) = V + 7 >= V + 7 = U81(isNePal(activate(V))) 44.13/13.87 44.13/13.87 __(X,nil()) = X >= X = X 44.13/13.87 44.13/13.87 __(nil(),X) = X >= X = X 44.13/13.87 44.13/13.87 U11(tt()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 U22(tt()) = 8 >= 7 = tt() 44.13/13.87 44.13/13.87 U31(tt()) = 11 >= 7 = tt() 44.13/13.87 44.13/13.87 U42(tt()) = 15 >= 7 = tt() 44.13/13.87 44.13/13.87 U52(tt()) = 20 >= 7 = tt() 44.13/13.87 44.13/13.87 U61(tt()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 U72(tt()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 U81(tt()) = 8 >= 7 = tt() 44.13/13.87 44.13/13.87 isList(n__nil()) = 8 >= 7 = tt() 44.13/13.87 44.13/13.87 isNePal(V) = V + 6 >= V + 4 = U61(isQid(activate(V))) 44.13/13.87 44.13/13.87 isNePal(n____(I,__(P,I))) = 2I + P + 10 >= I + P + 8 = U71(isQid(activate(I)),activate(P)) 44.13/13.87 44.13/13.87 isPal(n__nil()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 isQid(n__a()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 isQid(n__e()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 isQid(n__i()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 isQid(n__o()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 isQid(n__u()) = 7 >= 7 = tt() 44.13/13.87 44.13/13.87 nil() = 0 >= 0 = n__nil() 44.13/13.87 44.13/13.87 activate(n____(X1,X2)) = X1 + X2 + 4 >= X1 + X2 = __(X1,X2) 44.13/13.87 44.13/13.87 activate(n__a()) = 3 >= 0 = a() 44.13/13.87 44.13/13.87 activate(n__e()) = 3 >= 3 = e() 44.13/13.87 44.13/13.87 activate(n__i()) = 3 >= 3 = i() 44.13/13.87 44.13/13.87 activate(n__o()) = 3 >= 0 = o() 44.13/13.87 44.13/13.87 activate(n__u()) = 3 >= 0 = u() 44.13/13.87 44.13/13.87 activate(X) = X >= X = X 44.13/13.87 problem: 44.13/13.87 strict: 44.13/13.87 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.87 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.87 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.87 __(X1,X2) -> n____(X1,X2) 44.13/13.87 a() -> n__a() 44.13/13.87 o() -> n__o() 44.13/13.87 u() -> n__u() 44.13/13.87 weak: 44.13/13.87 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.87 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.87 e() -> n__e() 44.13/13.87 i() -> n__i() 44.13/13.87 activate(n__nil()) -> nil() 44.13/13.87 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.87 isList(V) -> U11(isNeList(activate(V))) 44.13/13.87 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.87 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.87 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.87 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.87 __(X,nil()) -> X 44.13/13.87 __(nil(),X) -> X 44.13/13.87 U11(tt()) -> tt() 44.13/13.87 U22(tt()) -> tt() 44.13/13.87 U31(tt()) -> tt() 44.13/13.87 U42(tt()) -> tt() 44.13/13.87 U52(tt()) -> tt() 44.13/13.87 U61(tt()) -> tt() 44.13/13.87 U72(tt()) -> tt() 44.13/13.87 U81(tt()) -> tt() 44.13/13.87 isList(n__nil()) -> tt() 44.13/13.87 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.87 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.87 isPal(n__nil()) -> tt() 44.13/13.87 isQid(n__a()) -> tt() 44.13/13.87 isQid(n__e()) -> tt() 44.13/13.87 isQid(n__i()) -> tt() 44.13/13.87 isQid(n__o()) -> tt() 44.13/13.87 isQid(n__u()) -> tt() 44.13/13.87 nil() -> n__nil() 44.13/13.87 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.87 activate(n__a()) -> a() 44.13/13.87 activate(n__e()) -> e() 44.13/13.87 activate(n__i()) -> i() 44.13/13.87 activate(n__o()) -> o() 44.13/13.87 activate(n__u()) -> u() 44.13/13.87 activate(X) -> X 44.13/13.87 Matrix Interpretation Processor: dim=1 44.13/13.87 44.13/13.87 max_matrix: 44.13/13.87 1 44.13/13.87 interpretation: 44.13/13.87 [u] = 0, 44.13/13.87 44.13/13.87 [o] = 0, 44.13/13.87 44.13/13.87 [i] = 1, 44.13/13.87 44.13/13.87 [e] = 0, 44.13/13.87 44.13/13.87 [a] = 0, 44.13/13.87 44.13/13.87 [n__u] = 4, 44.13/13.87 44.13/13.87 [n__o] = 6, 44.13/13.87 44.13/13.87 [n__i] = 1, 44.13/13.87 44.13/13.87 [n__e] = 0, 44.13/13.87 44.13/13.87 [n__a] = 4, 44.13/13.87 44.13/13.87 [isNePal](x0) = x0 + 6, 44.13/13.87 44.13/13.87 [isQid](x0) = x0 + 2, 44.13/13.87 44.13/13.87 [n____](x0, x1) = x0 + x1 + 8, 44.13/13.87 44.13/13.87 [n__nil] = 0, 44.13/13.87 44.13/13.87 [U81](x0) = x0 + 4, 44.13/13.87 44.13/13.87 [U72](x0) = x0 + 2, 44.13/13.87 44.13/13.87 [isPal](x0) = x0 + 10, 44.13/13.87 44.13/13.87 [U71](x0, x1) = x0 + x1 + 12, 44.13/13.87 44.13/13.87 [U61](x0) = x0 + 1, 44.13/13.87 44.13/13.87 [U52](x0) = x0 + 12, 44.13/13.87 44.13/13.87 [U51](x0, x1) = x0 + x1 + 8, 44.13/13.87 44.13/13.87 [U42](x0) = x0, 44.13/13.87 44.13/13.87 [isNeList](x0) = x0 + 4, 44.13/13.87 44.13/13.87 [U41](x0, x1) = x0 + x1 + 4, 44.13/13.87 44.13/13.87 [U31](x0) = x0 + 2, 44.13/13.87 44.13/13.87 [U22](x0) = x0 + 2, 44.13/13.87 44.13/13.87 [isList](x0) = x0 + 6, 44.13/13.87 44.13/13.87 [activate](x0) = x0, 44.13/13.87 44.13/13.87 [U21](x0, x1) = x0 + x1 + 8, 44.13/13.87 44.13/13.87 [U11](x0) = x0 + 2, 44.13/13.87 44.13/13.87 [tt] = 0, 44.13/13.87 44.13/13.87 [nil] = 0, 44.13/13.87 44.13/13.87 [__](x0, x1) = x0 + x1 44.13/13.87 orientation: 44.13/13.87 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 44.13/13.87 44.13/13.87 U51(tt(),V2) = V2 + 8 >= V2 + 18 = U52(isList(activate(V2))) 44.13/13.87 44.13/13.87 isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 10 = U41(isList(activate(V1)),activate(V2)) 44.13/13.87 44.13/13.87 __(X1,X2) = X1 + X2 >= X1 + X2 + 8 = n____(X1,X2) 44.13/13.87 44.13/13.87 a() = 0 >= 4 = n__a() 44.13/13.87 44.13/13.87 o() = 0 >= 6 = n__o() 44.13/13.87 44.13/13.87 u() = 0 >= 4 = n__u() 44.13/13.87 44.13/13.87 U21(tt(),V2) = V2 + 8 >= V2 + 8 = U22(isList(activate(V2))) 44.13/13.87 44.13/13.87 U71(tt(),P) = P + 12 >= P + 12 = U72(isPal(activate(P))) 44.13/13.87 44.13/13.87 e() = 0 >= 0 = n__e() 44.13/13.87 44.13/13.87 i() = 1 >= 1 = n__i() 44.13/13.87 44.13/13.87 activate(n__nil()) = 0 >= 0 = nil() 44.13/13.87 44.13/13.87 U41(tt(),V2) = V2 + 4 >= V2 + 4 = U42(isNeList(activate(V2))) 44.13/13.87 44.13/13.87 isList(V) = V + 6 >= V + 6 = U11(isNeList(activate(V))) 44.13/13.87 44.13/13.87 isList(n____(V1,V2)) = V1 + V2 + 14 >= V1 + V2 + 14 = U21(isList(activate(V1)),activate(V2)) 44.13/13.87 44.13/13.87 isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.87 44.13/13.87 isNeList(V) = V + 4 >= V + 4 = U31(isQid(activate(V))) 44.13/13.87 44.13/13.87 isPal(V) = V + 10 >= V + 10 = U81(isNePal(activate(V))) 44.13/13.87 44.13/13.87 __(X,nil()) = X >= X = X 44.13/13.87 44.13/13.87 __(nil(),X) = X >= X = X 44.13/13.87 44.13/13.87 U11(tt()) = 2 >= 0 = tt() 44.13/13.87 44.13/13.87 U22(tt()) = 2 >= 0 = tt() 44.13/13.87 44.13/13.87 U31(tt()) = 2 >= 0 = tt() 44.13/13.87 44.13/13.87 U42(tt()) = 0 >= 0 = tt() 44.13/13.87 44.13/13.87 U52(tt()) = 12 >= 0 = tt() 44.13/13.87 44.13/13.87 U61(tt()) = 1 >= 0 = tt() 44.13/13.87 44.13/13.87 U72(tt()) = 2 >= 0 = tt() 44.13/13.87 44.13/13.87 U81(tt()) = 4 >= 0 = tt() 44.13/13.87 44.13/13.87 isList(n__nil()) = 6 >= 0 = tt() 44.13/13.87 44.13/13.87 isNePal(V) = V + 6 >= V + 3 = U61(isQid(activate(V))) 44.13/13.87 44.13/13.87 isNePal(n____(I,__(P,I))) = 2I + P + 14 >= I + P + 14 = U71(isQid(activate(I)),activate(P)) 44.13/13.87 44.13/13.87 isPal(n__nil()) = 10 >= 0 = tt() 44.13/13.87 44.13/13.87 isQid(n__a()) = 6 >= 0 = tt() 44.13/13.87 44.13/13.87 isQid(n__e()) = 2 >= 0 = tt() 44.13/13.87 44.13/13.87 isQid(n__i()) = 3 >= 0 = tt() 44.13/13.87 44.13/13.87 isQid(n__o()) = 8 >= 0 = tt() 44.13/13.87 44.13/13.87 isQid(n__u()) = 6 >= 0 = tt() 44.13/13.87 44.13/13.87 nil() = 0 >= 0 = n__nil() 44.13/13.87 44.13/13.87 activate(n____(X1,X2)) = X1 + X2 + 8 >= X1 + X2 = __(X1,X2) 44.13/13.87 44.13/13.87 activate(n__a()) = 4 >= 0 = a() 44.13/13.87 44.13/13.87 activate(n__e()) = 0 >= 0 = e() 44.13/13.87 44.13/13.87 activate(n__i()) = 1 >= 1 = i() 44.13/13.87 44.13/13.87 activate(n__o()) = 6 >= 0 = o() 44.13/13.87 44.13/13.87 activate(n__u()) = 4 >= 0 = u() 44.13/13.87 44.13/13.87 activate(X) = X >= X = X 44.13/13.87 problem: 44.13/13.87 strict: 44.13/13.87 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.87 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.87 __(X1,X2) -> n____(X1,X2) 44.13/13.87 a() -> n__a() 44.13/13.87 o() -> n__o() 44.13/13.87 u() -> n__u() 44.13/13.87 weak: 44.13/13.87 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.87 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.87 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.87 e() -> n__e() 44.13/13.87 i() -> n__i() 44.13/13.87 activate(n__nil()) -> nil() 44.13/13.87 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.87 isList(V) -> U11(isNeList(activate(V))) 44.13/13.87 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.87 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.87 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.87 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.87 __(X,nil()) -> X 44.13/13.87 __(nil(),X) -> X 44.13/13.87 U11(tt()) -> tt() 44.13/13.87 U22(tt()) -> tt() 44.13/13.87 U31(tt()) -> tt() 44.13/13.87 U42(tt()) -> tt() 44.13/13.87 U52(tt()) -> tt() 44.13/13.87 U61(tt()) -> tt() 44.13/13.87 U72(tt()) -> tt() 44.13/13.87 U81(tt()) -> tt() 44.13/13.87 isList(n__nil()) -> tt() 44.13/13.87 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.87 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.87 isPal(n__nil()) -> tt() 44.13/13.87 isQid(n__a()) -> tt() 44.13/13.87 isQid(n__e()) -> tt() 44.13/13.87 isQid(n__i()) -> tt() 44.13/13.87 isQid(n__o()) -> tt() 44.13/13.87 isQid(n__u()) -> tt() 44.13/13.87 nil() -> n__nil() 44.13/13.87 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.87 activate(n__a()) -> a() 44.13/13.87 activate(n__e()) -> e() 44.13/13.87 activate(n__i()) -> i() 44.13/13.87 activate(n__o()) -> o() 44.13/13.87 activate(n__u()) -> u() 44.13/13.87 activate(X) -> X 44.13/13.87 Matrix Interpretation Processor: dim=1 44.13/13.87 44.13/13.87 max_matrix: 44.13/13.87 1 44.13/13.87 interpretation: 44.13/13.87 [u] = 0, 44.13/13.87 44.13/13.87 [o] = 0, 44.13/13.87 44.13/13.87 [i] = 3, 44.13/13.87 44.13/13.87 [e] = 10, 44.13/13.87 44.13/13.87 [a] = 3, 44.13/13.87 44.13/13.87 [n__u] = 8, 44.13/13.87 44.13/13.87 [n__o] = 3, 44.13/13.87 44.13/13.87 [n__i] = 3, 44.13/13.87 44.13/13.87 [n__e] = 10, 44.13/13.87 44.13/13.87 [n__a] = 3, 44.13/13.88 44.13/13.88 [isNePal](x0) = x0 + 9, 44.13/13.88 44.13/13.88 [isQid](x0) = x0 + 5, 44.13/13.88 44.13/13.88 [n____](x0, x1) = x0 + x1 + 10, 44.13/13.88 44.13/13.88 [n__nil] = 0, 44.13/13.88 44.13/13.88 [U81](x0) = x0 + 4, 44.13/13.88 44.13/13.88 [U72](x0) = x0 + 6, 44.13/13.88 44.13/13.88 [isPal](x0) = x0 + 13, 44.13/13.88 44.13/13.88 [U71](x0, x1) = x0 + x1 + 11, 44.13/13.88 44.13/13.88 [U61](x0) = x0 + 2, 44.13/13.88 44.13/13.88 [U52](x0) = x0 + 6, 44.13/13.88 44.13/13.88 [U51](x0, x1) = x0 + x1 + 10, 44.13/13.88 44.13/13.88 [U42](x0) = x0 + 8, 44.13/13.88 44.13/13.88 [isNeList](x0) = x0 + 7, 44.13/13.88 44.13/13.88 [U41](x0, x1) = x0 + x1 + 7, 44.13/13.88 44.13/13.88 [U31](x0) = x0 + 2, 44.13/13.88 44.13/13.88 [U22](x0) = x0 + 8, 44.13/13.88 44.13/13.88 [isList](x0) = x0 + 10, 44.13/13.88 44.13/13.88 [activate](x0) = x0, 44.13/13.88 44.13/13.88 [U21](x0, x1) = x0 + x1 + 10, 44.13/13.88 44.13/13.88 [U11](x0) = x0 + 3, 44.13/13.88 44.13/13.88 [tt] = 8, 44.13/13.88 44.13/13.88 [nil] = 0, 44.13/13.88 44.13/13.88 [__](x0, x1) = x0 + x1 44.13/13.88 orientation: 44.13/13.88 __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z)) 44.13/13.88 44.13/13.88 U51(tt(),V2) = V2 + 18 >= V2 + 16 = U52(isList(activate(V2))) 44.13/13.88 44.13/13.88 __(X1,X2) = X1 + X2 >= X1 + X2 + 10 = n____(X1,X2) 44.13/13.88 44.13/13.88 a() = 3 >= 3 = n__a() 44.13/13.88 44.13/13.88 o() = 0 >= 3 = n__o() 44.13/13.88 44.13/13.88 u() = 0 >= 8 = n__u() 44.13/13.88 44.13/13.88 isNeList(n____(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 17 = U41(isList(activate(V1)),activate(V2)) 44.13/13.88 44.13/13.88 U21(tt(),V2) = V2 + 18 >= V2 + 18 = U22(isList(activate(V2))) 44.13/13.88 44.13/13.88 U71(tt(),P) = P + 19 >= P + 19 = U72(isPal(activate(P))) 44.13/13.88 44.13/13.88 e() = 10 >= 10 = n__e() 44.13/13.88 44.13/13.88 i() = 3 >= 3 = n__i() 44.13/13.88 44.13/13.88 activate(n__nil()) = 0 >= 0 = nil() 44.13/13.88 44.13/13.88 U41(tt(),V2) = V2 + 15 >= V2 + 15 = U42(isNeList(activate(V2))) 44.13/13.88 44.13/13.88 isList(V) = V + 10 >= V + 10 = U11(isNeList(activate(V))) 44.13/13.88 44.13/13.88 isList(n____(V1,V2)) = V1 + V2 + 20 >= V1 + V2 + 20 = U21(isList(activate(V1)),activate(V2)) 44.13/13.88 44.13/13.88 isNeList(n____(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 17 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.88 44.13/13.88 isNeList(V) = V + 7 >= V + 7 = U31(isQid(activate(V))) 44.13/13.88 44.13/13.88 isPal(V) = V + 13 >= V + 13 = U81(isNePal(activate(V))) 44.13/13.88 44.13/13.88 __(X,nil()) = X >= X = X 44.13/13.88 44.13/13.88 __(nil(),X) = X >= X = X 44.13/13.88 44.13/13.88 U11(tt()) = 11 >= 8 = tt() 44.13/13.88 44.13/13.88 U22(tt()) = 16 >= 8 = tt() 44.13/13.88 44.13/13.88 U31(tt()) = 10 >= 8 = tt() 44.13/13.88 44.13/13.88 U42(tt()) = 16 >= 8 = tt() 44.13/13.88 44.13/13.88 U52(tt()) = 14 >= 8 = tt() 44.13/13.88 44.13/13.88 U61(tt()) = 10 >= 8 = tt() 44.13/13.88 44.13/13.88 U72(tt()) = 14 >= 8 = tt() 44.13/13.88 44.13/13.88 U81(tt()) = 12 >= 8 = tt() 44.13/13.88 44.13/13.88 isList(n__nil()) = 10 >= 8 = tt() 44.13/13.88 44.13/13.88 isNePal(V) = V + 9 >= V + 7 = U61(isQid(activate(V))) 44.13/13.88 44.13/13.88 isNePal(n____(I,__(P,I))) = 2I + P + 19 >= I + P + 16 = U71(isQid(activate(I)),activate(P)) 44.13/13.88 44.13/13.88 isPal(n__nil()) = 13 >= 8 = tt() 44.13/13.88 44.13/13.88 isQid(n__a()) = 8 >= 8 = tt() 44.13/13.88 44.13/13.88 isQid(n__e()) = 15 >= 8 = tt() 44.13/13.88 44.13/13.88 isQid(n__i()) = 8 >= 8 = tt() 44.13/13.88 44.13/13.88 isQid(n__o()) = 8 >= 8 = tt() 44.13/13.88 44.13/13.88 isQid(n__u()) = 13 >= 8 = tt() 44.13/13.88 44.13/13.88 nil() = 0 >= 0 = n__nil() 44.13/13.88 44.13/13.88 activate(n____(X1,X2)) = X1 + X2 + 10 >= X1 + X2 = __(X1,X2) 44.13/13.88 44.13/13.88 activate(n__a()) = 3 >= 3 = a() 44.13/13.88 44.13/13.88 activate(n__e()) = 10 >= 10 = e() 44.13/13.88 44.13/13.88 activate(n__i()) = 3 >= 3 = i() 44.13/13.88 44.13/13.88 activate(n__o()) = 3 >= 0 = o() 44.13/13.88 44.13/13.88 activate(n__u()) = 8 >= 0 = u() 44.13/13.88 44.13/13.88 activate(X) = X >= X = X 44.13/13.88 problem: 44.13/13.88 strict: 44.13/13.88 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.88 __(X1,X2) -> n____(X1,X2) 44.13/13.88 a() -> n__a() 44.13/13.88 o() -> n__o() 44.13/13.88 u() -> n__u() 44.13/13.88 weak: 44.13/13.88 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.88 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.88 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.88 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.88 e() -> n__e() 44.13/13.88 i() -> n__i() 44.13/13.88 activate(n__nil()) -> nil() 44.13/13.88 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.88 isList(V) -> U11(isNeList(activate(V))) 44.13/13.88 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.88 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.88 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.88 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.88 __(X,nil()) -> X 44.13/13.88 __(nil(),X) -> X 44.13/13.88 U11(tt()) -> tt() 44.13/13.88 U22(tt()) -> tt() 44.13/13.88 U31(tt()) -> tt() 44.13/13.88 U42(tt()) -> tt() 44.13/13.88 U52(tt()) -> tt() 44.13/13.88 U61(tt()) -> tt() 44.13/13.88 U72(tt()) -> tt() 44.13/13.88 U81(tt()) -> tt() 44.13/13.88 isList(n__nil()) -> tt() 44.13/13.88 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.88 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.88 isPal(n__nil()) -> tt() 44.13/13.88 isQid(n__a()) -> tt() 44.13/13.88 isQid(n__e()) -> tt() 44.13/13.88 isQid(n__i()) -> tt() 44.13/13.88 isQid(n__o()) -> tt() 44.13/13.88 isQid(n__u()) -> tt() 44.13/13.88 nil() -> n__nil() 44.13/13.88 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.88 activate(n__a()) -> a() 44.13/13.88 activate(n__e()) -> e() 44.13/13.88 activate(n__i()) -> i() 44.13/13.88 activate(n__o()) -> o() 44.13/13.88 activate(n__u()) -> u() 44.13/13.88 activate(X) -> X 44.13/13.88 Matrix Interpretation Processor: dim=1 44.13/13.88 44.13/13.88 max_matrix: 44.13/13.88 1 44.13/13.88 interpretation: 44.13/13.88 [u] = 0, 44.13/13.88 44.13/13.88 [o] = 13, 44.13/13.88 44.13/13.88 [i] = 2, 44.13/13.88 44.13/13.88 [e] = 0, 44.13/13.88 44.13/13.88 [a] = 9, 44.13/13.88 44.13/13.88 [n__u] = 8, 44.13/13.88 44.13/13.88 [n__o] = 12, 44.13/13.88 44.13/13.88 [n__i] = 2, 44.13/13.88 44.13/13.88 [n__e] = 0, 44.13/13.88 44.13/13.88 [n__a] = 8, 44.13/13.88 44.13/13.88 [isNePal](x0) = x0 + 8, 44.13/13.88 44.13/13.88 [isQid](x0) = x0, 44.13/13.88 44.13/13.88 [n____](x0, x1) = x0 + x1 + 8, 44.13/13.88 44.13/13.88 [n__nil] = 3, 44.13/13.88 44.13/13.88 [U81](x0) = x0 + 1, 44.13/13.88 44.13/13.88 [U72](x0) = x0 + 3, 44.13/13.88 44.13/13.88 [isPal](x0) = x0 + 10, 44.13/13.88 44.13/13.88 [U71](x0, x1) = x0 + x1 + 14, 44.13/13.88 44.13/13.88 [U61](x0) = x0 + 4, 44.13/13.88 44.13/13.88 [U52](x0) = x0, 44.13/13.88 44.13/13.88 [U51](x0, x1) = x0 + x1 + 6, 44.13/13.88 44.13/13.88 [U42](x0) = x0, 44.13/13.88 44.13/13.88 [isNeList](x0) = x0 + 1, 44.13/13.88 44.13/13.88 [U41](x0, x1) = x0 + x1 + 2, 44.13/13.88 44.13/13.88 [U31](x0) = x0, 44.13/13.88 44.13/13.88 [U22](x0) = x0, 44.13/13.88 44.13/13.88 [isList](x0) = x0 + 2, 44.13/13.88 44.13/13.88 [activate](x0) = x0 + 1, 44.13/13.88 44.13/13.88 [U21](x0, x1) = x0 + x1 + 3, 44.13/13.88 44.13/13.88 [U11](x0) = x0, 44.13/13.88 44.13/13.88 [tt] = 0, 44.13/13.88 44.13/13.88 [nil] = 4, 44.13/13.88 44.13/13.88 [__](x0, x1) = x0 + x1 + 9 44.13/13.88 orientation: 44.13/13.88 __(__(X,Y),Z) = X + Y + Z + 18 >= X + Y + Z + 18 = __(X,__(Y,Z)) 44.13/13.88 44.13/13.88 __(X1,X2) = X1 + X2 + 9 >= X1 + X2 + 8 = n____(X1,X2) 44.13/13.88 44.13/13.88 a() = 9 >= 8 = n__a() 44.13/13.88 44.13/13.88 o() = 13 >= 12 = n__o() 44.13/13.88 44.13/13.88 u() = 0 >= 8 = n__u() 44.13/13.88 44.13/13.88 U51(tt(),V2) = V2 + 6 >= V2 + 3 = U52(isList(activate(V2))) 44.13/13.88 44.13/13.88 isNeList(n____(V1,V2)) = V1 + V2 + 9 >= V1 + V2 + 6 = U41(isList(activate(V1)),activate(V2)) 44.13/13.88 44.13/13.88 U21(tt(),V2) = V2 + 3 >= V2 + 3 = U22(isList(activate(V2))) 44.13/13.88 44.13/13.88 U71(tt(),P) = P + 14 >= P + 14 = U72(isPal(activate(P))) 44.13/13.88 44.13/13.88 e() = 0 >= 0 = n__e() 44.13/13.88 44.13/13.88 i() = 2 >= 2 = n__i() 44.13/13.88 44.13/13.88 activate(n__nil()) = 4 >= 4 = nil() 44.13/13.89 44.13/13.89 U41(tt(),V2) = V2 + 2 >= V2 + 2 = U42(isNeList(activate(V2))) 44.13/13.89 44.13/13.89 isList(V) = V + 2 >= V + 2 = U11(isNeList(activate(V))) 44.13/13.89 44.13/13.89 isList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 7 = U21(isList(activate(V1)),activate(V2)) 44.13/13.89 44.13/13.89 isNeList(n____(V1,V2)) = V1 + V2 + 9 >= V1 + V2 + 9 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.89 44.13/13.89 isNeList(V) = V + 1 >= V + 1 = U31(isQid(activate(V))) 44.13/13.89 44.13/13.89 isPal(V) = V + 10 >= V + 10 = U81(isNePal(activate(V))) 44.13/13.89 44.13/13.89 __(X,nil()) = X + 13 >= X = X 44.13/13.89 44.13/13.89 __(nil(),X) = X + 13 >= X = X 44.13/13.89 44.13/13.89 U11(tt()) = 0 >= 0 = tt() 44.13/13.89 44.13/13.89 U22(tt()) = 0 >= 0 = tt() 44.13/13.89 44.13/13.89 U31(tt()) = 0 >= 0 = tt() 44.13/13.89 44.13/13.89 U42(tt()) = 0 >= 0 = tt() 44.13/13.89 44.13/13.89 U52(tt()) = 0 >= 0 = tt() 44.13/13.89 44.13/13.89 U61(tt()) = 4 >= 0 = tt() 44.13/13.89 44.13/13.89 U72(tt()) = 3 >= 0 = tt() 44.13/13.89 44.13/13.89 U81(tt()) = 1 >= 0 = tt() 44.13/13.89 44.13/13.89 isList(n__nil()) = 5 >= 0 = tt() 44.13/13.89 44.13/13.89 isNePal(V) = V + 8 >= V + 5 = U61(isQid(activate(V))) 44.13/13.89 44.13/13.89 isNePal(n____(I,__(P,I))) = 2I + P + 25 >= I + P + 16 = U71(isQid(activate(I)),activate(P)) 44.13/13.89 44.13/13.89 isPal(n__nil()) = 13 >= 0 = tt() 44.13/13.89 44.13/13.89 isQid(n__a()) = 8 >= 0 = tt() 44.13/13.89 44.13/13.89 isQid(n__e()) = 0 >= 0 = tt() 44.13/13.89 44.13/13.89 isQid(n__i()) = 2 >= 0 = tt() 44.13/13.89 44.13/13.89 isQid(n__o()) = 12 >= 0 = tt() 44.13/13.89 44.13/13.89 isQid(n__u()) = 8 >= 0 = tt() 44.13/13.89 44.13/13.89 nil() = 4 >= 3 = n__nil() 44.13/13.89 44.13/13.89 activate(n____(X1,X2)) = X1 + X2 + 9 >= X1 + X2 + 9 = __(X1,X2) 44.13/13.89 44.13/13.89 activate(n__a()) = 9 >= 9 = a() 44.13/13.89 44.13/13.89 activate(n__e()) = 1 >= 0 = e() 44.13/13.89 44.13/13.89 activate(n__i()) = 3 >= 2 = i() 44.13/13.89 44.13/13.89 activate(n__o()) = 13 >= 13 = o() 44.13/13.89 44.13/13.89 activate(n__u()) = 9 >= 0 = u() 44.13/13.89 44.13/13.89 activate(X) = X + 1 >= X = X 44.13/13.89 problem: 44.13/13.89 strict: 44.13/13.89 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.89 u() -> n__u() 44.13/13.89 weak: 44.13/13.89 __(X1,X2) -> n____(X1,X2) 44.13/13.89 a() -> n__a() 44.13/13.89 o() -> n__o() 44.13/13.89 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.89 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.89 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.89 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.89 e() -> n__e() 44.13/13.89 i() -> n__i() 44.13/13.89 activate(n__nil()) -> nil() 44.13/13.89 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.89 isList(V) -> U11(isNeList(activate(V))) 44.13/13.89 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.89 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.89 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.89 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.89 __(X,nil()) -> X 44.13/13.89 __(nil(),X) -> X 44.13/13.89 U11(tt()) -> tt() 44.13/13.89 U22(tt()) -> tt() 44.13/13.89 U31(tt()) -> tt() 44.13/13.89 U42(tt()) -> tt() 44.13/13.89 U52(tt()) -> tt() 44.13/13.89 U61(tt()) -> tt() 44.13/13.89 U72(tt()) -> tt() 44.13/13.89 U81(tt()) -> tt() 44.13/13.89 isList(n__nil()) -> tt() 44.13/13.89 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.89 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.89 isPal(n__nil()) -> tt() 44.13/13.89 isQid(n__a()) -> tt() 44.13/13.89 isQid(n__e()) -> tt() 44.13/13.89 isQid(n__i()) -> tt() 44.13/13.89 isQid(n__o()) -> tt() 44.13/13.89 isQid(n__u()) -> tt() 44.13/13.89 nil() -> n__nil() 44.13/13.89 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.89 activate(n__a()) -> a() 44.13/13.89 activate(n__e()) -> e() 44.13/13.89 activate(n__i()) -> i() 44.13/13.89 activate(n__o()) -> o() 44.13/13.89 activate(n__u()) -> u() 44.13/13.89 activate(X) -> X 44.13/13.89 Matrix Interpretation Processor: dim=1 44.13/13.89 44.13/13.89 max_matrix: 44.13/13.89 1 44.13/13.89 interpretation: 44.13/13.89 [u] = 15, 44.13/13.89 44.13/13.89 [o] = 14, 44.13/13.89 44.13/13.89 [i] = 14, 44.13/13.89 44.13/13.89 [e] = 15, 44.13/13.89 44.13/13.89 [a] = 15, 44.13/13.89 44.13/13.89 [n__u] = 14, 44.13/13.89 44.13/13.89 [n__o] = 14, 44.13/13.89 44.13/13.89 [n__i] = 14, 44.13/13.89 44.13/13.89 [n__e] = 14, 44.13/13.89 44.13/13.89 [n__a] = 15, 44.13/13.89 44.13/13.89 [isNePal](x0) = x0 + 1, 44.13/13.89 44.13/13.89 [isQid](x0) = x0, 44.13/13.89 44.13/13.89 [n____](x0, x1) = x0 + x1 + 15, 44.13/13.89 44.13/13.89 [n__nil] = 3, 44.13/13.89 44.13/13.89 [U81](x0) = x0 + 9, 44.13/13.89 44.13/13.89 [U72](x0) = x0 + 4, 44.13/13.89 44.13/13.89 [isPal](x0) = x0 + 11, 44.13/13.89 44.13/13.89 [U71](x0, x1) = x0 + x1 + 10, 44.13/13.89 44.13/13.89 [U61](x0) = x0, 44.13/13.89 44.13/13.89 [U52](x0) = x0 + 1, 44.13/13.89 44.13/13.89 [U51](x0, x1) = x0 + x1 + 4, 44.13/13.89 44.13/13.89 [U42](x0) = x0 + 2, 44.13/13.89 44.13/13.89 [isNeList](x0) = x0 + 11, 44.13/13.89 44.13/13.89 [U41](x0, x1) = x0 + x1 + 8, 44.13/13.89 44.13/13.89 [U31](x0) = x0 + 7, 44.13/13.89 44.13/13.89 [U22](x0) = x0 + 7, 44.13/13.89 44.13/13.89 [isList](x0) = x0 + 15, 44.13/13.89 44.13/13.89 [activate](x0) = x0 + 1, 44.13/13.89 44.13/13.89 [U21](x0, x1) = x0 + x1 + 9, 44.13/13.89 44.13/13.89 [U11](x0) = x0, 44.13/13.89 44.13/13.89 [tt] = 14, 44.13/13.89 44.13/13.89 [nil] = 3, 44.13/13.89 44.13/13.89 [__](x0, x1) = x0 + x1 + 15 44.13/13.89 orientation: 44.13/13.89 __(__(X,Y),Z) = X + Y + Z + 30 >= X + Y + Z + 30 = __(X,__(Y,Z)) 44.13/13.89 44.13/13.89 u() = 15 >= 14 = n__u() 44.13/13.89 44.13/13.89 __(X1,X2) = X1 + X2 + 15 >= X1 + X2 + 15 = n____(X1,X2) 44.13/13.89 44.13/13.89 a() = 15 >= 15 = n__a() 44.13/13.89 44.13/13.89 o() = 14 >= 14 = n__o() 44.13/13.89 44.13/13.89 U51(tt(),V2) = V2 + 18 >= V2 + 17 = U52(isList(activate(V2))) 44.13/13.89 44.13/13.89 isNeList(n____(V1,V2)) = V1 + V2 + 26 >= V1 + V2 + 25 = U41(isList(activate(V1)),activate(V2)) 44.13/13.89 44.13/13.89 U21(tt(),V2) = V2 + 23 >= V2 + 23 = U22(isList(activate(V2))) 44.13/13.89 44.13/13.89 U71(tt(),P) = P + 24 >= P + 16 = U72(isPal(activate(P))) 44.13/13.89 44.13/13.89 e() = 15 >= 14 = n__e() 44.13/13.89 44.13/13.89 i() = 14 >= 14 = n__i() 44.13/13.89 44.13/13.89 activate(n__nil()) = 4 >= 3 = nil() 44.13/13.89 44.13/13.89 U41(tt(),V2) = V2 + 22 >= V2 + 14 = U42(isNeList(activate(V2))) 44.13/13.89 44.13/13.89 isList(V) = V + 15 >= V + 12 = U11(isNeList(activate(V))) 44.13/13.89 44.13/13.89 isList(n____(V1,V2)) = V1 + V2 + 30 >= V1 + V2 + 26 = U21(isList(activate(V1)),activate(V2)) 44.13/13.89 44.13/13.89 isNeList(n____(V1,V2)) = V1 + V2 + 26 >= V1 + V2 + 17 = U51(isNeList(activate(V1)),activate(V2)) 44.13/13.89 44.13/13.89 isNeList(V) = V + 11 >= V + 8 = U31(isQid(activate(V))) 44.13/13.89 44.13/13.89 isPal(V) = V + 11 >= V + 11 = U81(isNePal(activate(V))) 44.13/13.89 44.13/13.89 __(X,nil()) = X + 18 >= X = X 44.13/13.89 44.13/13.89 __(nil(),X) = X + 18 >= X = X 44.13/13.89 44.13/13.89 U11(tt()) = 14 >= 14 = tt() 44.13/13.89 44.13/13.89 U22(tt()) = 21 >= 14 = tt() 44.13/13.89 44.13/13.89 U31(tt()) = 21 >= 14 = tt() 44.13/13.89 44.13/13.89 U42(tt()) = 16 >= 14 = tt() 44.13/13.89 44.13/13.89 U52(tt()) = 15 >= 14 = tt() 44.13/13.89 44.13/13.89 U61(tt()) = 14 >= 14 = tt() 44.13/13.89 44.13/13.89 U72(tt()) = 18 >= 14 = tt() 44.13/13.89 44.13/13.89 U81(tt()) = 23 >= 14 = tt() 44.13/13.89 44.13/13.89 isList(n__nil()) = 18 >= 14 = tt() 44.13/13.89 44.13/13.89 isNePal(V) = V + 1 >= V + 1 = U61(isQid(activate(V))) 44.13/13.89 44.13/13.89 isNePal(n____(I,__(P,I))) = 2I + P + 31 >= I + P + 12 = U71(isQid(activate(I)),activate(P)) 44.13/13.89 44.13/13.89 isPal(n__nil()) = 14 >= 14 = tt() 44.13/13.89 44.13/13.89 isQid(n__a()) = 15 >= 14 = tt() 44.13/13.89 44.13/13.89 isQid(n__e()) = 14 >= 14 = tt() 44.13/13.89 44.13/13.89 isQid(n__i()) = 14 >= 14 = tt() 44.13/13.89 44.13/13.89 isQid(n__o()) = 14 >= 14 = tt() 44.13/13.89 44.13/13.89 isQid(n__u()) = 14 >= 14 = tt() 44.13/13.89 44.13/13.89 nil() = 3 >= 3 = n__nil() 44.13/13.89 44.13/13.89 activate(n____(X1,X2)) = X1 + X2 + 16 >= X1 + X2 + 15 = __(X1,X2) 44.13/13.89 44.13/13.89 activate(n__a()) = 16 >= 15 = a() 44.13/13.89 44.13/13.89 activate(n__e()) = 15 >= 15 = e() 44.13/13.89 44.13/13.89 activate(n__i()) = 15 >= 14 = i() 44.13/13.89 44.13/13.89 activate(n__o()) = 15 >= 14 = o() 44.13/13.89 44.13/13.89 activate(n__u()) = 15 >= 15 = u() 44.13/13.89 44.13/13.89 activate(X) = X + 1 >= X = X 44.13/13.89 problem: 44.13/13.89 strict: 44.13/13.89 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.13/13.89 weak: 44.13/13.89 u() -> n__u() 44.13/13.89 __(X1,X2) -> n____(X1,X2) 44.13/13.89 a() -> n__a() 44.13/13.89 o() -> n__o() 44.13/13.89 U51(tt(),V2) -> U52(isList(activate(V2))) 44.13/13.89 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.13/13.89 U21(tt(),V2) -> U22(isList(activate(V2))) 44.13/13.89 U71(tt(),P) -> U72(isPal(activate(P))) 44.13/13.89 e() -> n__e() 44.13/13.89 i() -> n__i() 44.13/13.89 activate(n__nil()) -> nil() 44.13/13.89 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.13/13.89 isList(V) -> U11(isNeList(activate(V))) 44.13/13.89 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.13/13.89 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.13/13.89 isNeList(V) -> U31(isQid(activate(V))) 44.13/13.89 isPal(V) -> U81(isNePal(activate(V))) 44.13/13.89 __(X,nil()) -> X 44.13/13.89 __(nil(),X) -> X 44.13/13.89 U11(tt()) -> tt() 44.13/13.89 U22(tt()) -> tt() 44.13/13.89 U31(tt()) -> tt() 44.13/13.89 U42(tt()) -> tt() 44.13/13.89 U52(tt()) -> tt() 44.13/13.89 U61(tt()) -> tt() 44.13/13.89 U72(tt()) -> tt() 44.13/13.89 U81(tt()) -> tt() 44.13/13.89 isList(n__nil()) -> tt() 44.13/13.89 isNePal(V) -> U61(isQid(activate(V))) 44.13/13.89 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.13/13.89 isPal(n__nil()) -> tt() 44.13/13.89 isQid(n__a()) -> tt() 44.13/13.89 isQid(n__e()) -> tt() 44.13/13.89 isQid(n__i()) -> tt() 44.13/13.89 isQid(n__o()) -> tt() 44.13/13.89 isQid(n__u()) -> tt() 44.13/13.89 nil() -> n__nil() 44.13/13.89 activate(n____(X1,X2)) -> __(X1,X2) 44.13/13.89 activate(n__a()) -> a() 44.13/13.89 activate(n__e()) -> e() 44.13/13.89 activate(n__i()) -> i() 44.13/13.89 activate(n__o()) -> o() 44.13/13.89 activate(n__u()) -> u() 44.13/13.89 activate(X) -> X 44.13/13.89 Matrix Interpretation Processor: dim=2 44.13/13.89 44.13/13.89 max_matrix: 44.13/13.89 [1 3] 44.13/13.89 [0 1] 44.13/13.89 interpretation: 44.13/13.89 [3] 44.13/13.89 [u] = [0], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [o] = [0], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [i] = [1], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [e] = [0], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [a] = [0], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [n__u] = [0], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [n__o] = [0], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [n__i] = [1], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [n__e] = [0], 44.13/13.89 44.13/13.89 [3] 44.13/13.89 [n__a] = [0], 44.13/13.89 44.13/13.89 [1 0] [1] 44.13/13.89 [isNePal](x0) = [0 0]x0 + [0], 44.13/13.89 44.13/13.89 [1 0] [0] 44.13/13.89 [isQid](x0) = [0 0]x0 + [1], 44.13/13.89 44.13/13.89 [1 1] [2] 44.13/13.89 [n____](x0, x1) = [0 1]x0 + x1 + [1], 44.13/13.89 44.13/13.89 [2] 44.13/13.89 [n__nil] = [2], 44.13/13.89 44.13/13.89 [1 0] 44.13/13.89 [U81](x0) = [0 0]x0, 44.13/13.89 44.13/13.89 [1 0] [2] 44.13/13.89 [U72](x0) = [0 0]x0 + [0], 44.13/13.89 44.13/13.89 [1] 44.13/13.89 [isPal](x0) = x0 + [2], 44.13/13.89 44.26/13.90 [1 0] [1 1] 44.26/13.90 [U71](x0, x1) = [0 0]x0 + [0 0]x1, 44.26/13.90 44.26/13.90 [1 1] 44.26/13.90 [U61](x0) = [0 0]x0, 44.26/13.90 44.26/13.90 [1 2] 44.26/13.90 [U52](x0) = [0 0]x0, 44.26/13.90 44.26/13.90 [1 3] [1 1] 44.26/13.90 [U51](x0, x1) = [0 0]x0 + [0 0]x1, 44.26/13.90 44.26/13.90 [1 0] 44.26/13.90 [U42](x0) = [0 0]x0, 44.26/13.90 44.26/13.90 [1 1] 44.26/13.90 [isNeList](x0) = [0 0]x0, 44.26/13.90 44.26/13.90 [1 0] [1 1] 44.26/13.90 [U41](x0, x1) = [0 0]x0 + [0 0]x1, 44.26/13.90 44.26/13.90 [1 0] 44.26/13.90 [U31](x0) = [0 0]x0, 44.26/13.90 44.26/13.90 [1 1] [1] 44.26/13.90 [U22](x0) = [0 0]x0 + [0], 44.26/13.90 44.26/13.90 [1 1] [1] 44.26/13.90 [isList](x0) = [0 0]x0 + [1], 44.26/13.90 44.26/13.90 44.26/13.90 [activate](x0) = x0, 44.26/13.90 44.26/13.90 [1 3] [1 1] 44.26/13.90 [U21](x0, x1) = [0 0]x0 + [0 0]x1, 44.26/13.90 44.26/13.90 [1] 44.26/13.90 [U11](x0) = x0 + [0], 44.26/13.90 44.26/13.90 [3] 44.26/13.90 [tt] = [0], 44.26/13.90 44.26/13.90 [2] 44.26/13.90 [nil] = [2], 44.26/13.90 44.26/13.90 [1 1] [2] 44.26/13.90 [__](x0, x1) = [0 1]x0 + x1 + [1] 44.26/13.90 orientation: 44.26/13.90 [1 2] [1 1] [5] [1 1] [1 1] [4] 44.26/13.90 __(__(X,Y),Z) = [0 1]X + [0 1]Y + Z + [2] >= [0 1]X + [0 1]Y + Z + [2] = __(X,__(Y,Z)) 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 u() = [0] >= [0] = n__u() 44.26/13.90 44.26/13.90 [1 1] [2] [1 1] [2] 44.26/13.90 __(X1,X2) = [0 1]X1 + X2 + [1] >= [0 1]X1 + X2 + [1] = n____(X1,X2) 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 a() = [0] >= [0] = n__a() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 o() = [0] >= [0] = n__o() 44.26/13.90 44.26/13.90 [1 1] [3] [1 1] [3] 44.26/13.90 U51(tt(),V2) = [0 0]V2 + [0] >= [0 0]V2 + [0] = U52(isList(activate(V2))) 44.26/13.90 44.26/13.90 [1 2] [1 1] [3] [1 1] [1 1] [1] 44.26/13.90 isNeList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 + [0] >= [0 0]V1 + [0 0]V2 + [0] = U41(isList(activate(V1)),activate(V2)) 44.26/13.90 44.26/13.90 [1 1] [3] [1 1] [3] 44.26/13.90 U21(tt(),V2) = [0 0]V2 + [0] >= [0 0]V2 + [0] = U22(isList(activate(V2))) 44.26/13.90 44.26/13.90 [1 1] [3] [1 0] [3] 44.26/13.90 U71(tt(),P) = [0 0]P + [0] >= [0 0]P + [0] = U72(isPal(activate(P))) 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 e() = [0] >= [0] = n__e() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 i() = [1] >= [1] = n__i() 44.26/13.90 44.26/13.90 [2] [2] 44.26/13.90 activate(n__nil()) = [2] >= [2] = nil() 44.26/13.90 44.26/13.90 [1 1] [3] [1 1] 44.26/13.90 U41(tt(),V2) = [0 0]V2 + [0] >= [0 0]V2 = U42(isNeList(activate(V2))) 44.26/13.90 44.26/13.90 [1 1] [1] [1 1] [1] 44.26/13.90 isList(V) = [0 0]V + [1] >= [0 0]V + [0] = U11(isNeList(activate(V))) 44.26/13.90 44.26/13.90 [1 2] [1 1] [4] [1 1] [1 1] [4] 44.26/13.90 isList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 + [1] >= [0 0]V1 + [0 0]V2 + [0] = U21(isList(activate(V1)),activate(V2)) 44.26/13.90 44.26/13.90 [1 2] [1 1] [3] [1 1] [1 1] 44.26/13.90 isNeList(n____(V1,V2)) = [0 0]V1 + [0 0]V2 + [0] >= [0 0]V1 + [0 0]V2 = U51(isNeList(activate(V1)),activate(V2)) 44.26/13.90 44.26/13.90 [1 1] [1 0] 44.26/13.90 isNeList(V) = [0 0]V >= [0 0]V = U31(isQid(activate(V))) 44.26/13.90 44.26/13.90 [1] [1 0] [1] 44.26/13.90 isPal(V) = V + [2] >= [0 0]V + [0] = U81(isNePal(activate(V))) 44.26/13.90 44.26/13.90 [1 1] [4] 44.26/13.90 __(X,nil()) = [0 1]X + [3] >= X = X 44.26/13.90 44.26/13.90 [6] 44.26/13.90 __(nil(),X) = X + [3] >= X = X 44.26/13.90 44.26/13.90 [4] [3] 44.26/13.90 U11(tt()) = [0] >= [0] = tt() 44.26/13.90 44.26/13.90 [4] [3] 44.26/13.90 U22(tt()) = [0] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 U31(tt()) = [0] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 U42(tt()) = [0] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 U52(tt()) = [0] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 U61(tt()) = [0] >= [0] = tt() 44.26/13.90 44.26/13.90 [5] [3] 44.26/13.90 U72(tt()) = [0] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 U81(tt()) = [0] >= [0] = tt() 44.26/13.90 44.26/13.90 [5] [3] 44.26/13.90 isList(n__nil()) = [1] >= [0] = tt() 44.26/13.90 44.26/13.90 [1 0] [1] [1 0] [1] 44.26/13.90 isNePal(V) = [0 0]V + [0] >= [0 0]V + [0] = U61(isQid(activate(V))) 44.26/13.90 44.26/13.90 [2 1] [1 1] [5] [1 0] [1 1] 44.26/13.90 isNePal(n____(I,__(P,I))) = [0 0]I + [0 0]P + [0] >= [0 0]I + [0 0]P = U71(isQid(activate(I)),activate(P)) 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 isPal(n__nil()) = [4] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 isQid(n__a()) = [1] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 isQid(n__e()) = [1] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 isQid(n__i()) = [1] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 isQid(n__o()) = [1] >= [0] = tt() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 isQid(n__u()) = [1] >= [0] = tt() 44.26/13.90 44.26/13.90 [2] [2] 44.26/13.90 nil() = [2] >= [2] = n__nil() 44.26/13.90 44.26/13.90 [1 1] [2] [1 1] [2] 44.26/13.90 activate(n____(X1,X2)) = [0 1]X1 + X2 + [1] >= [0 1]X1 + X2 + [1] = __(X1,X2) 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 activate(n__a()) = [0] >= [0] = a() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 activate(n__e()) = [0] >= [0] = e() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 activate(n__i()) = [1] >= [1] = i() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 activate(n__o()) = [0] >= [0] = o() 44.26/13.90 44.26/13.90 [3] [3] 44.26/13.90 activate(n__u()) = [0] >= [0] = u() 44.26/13.90 44.26/13.90 44.26/13.90 activate(X) = X >= X = X 44.26/13.90 problem: 44.26/13.90 strict: 44.26/13.90 44.26/13.90 weak: 44.26/13.90 __(__(X,Y),Z) -> __(X,__(Y,Z)) 44.26/13.90 u() -> n__u() 44.26/13.90 __(X1,X2) -> n____(X1,X2) 44.26/13.90 a() -> n__a() 44.26/13.90 o() -> n__o() 44.26/13.90 U51(tt(),V2) -> U52(isList(activate(V2))) 44.26/13.90 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) 44.26/13.90 U21(tt(),V2) -> U22(isList(activate(V2))) 44.26/13.90 U71(tt(),P) -> U72(isPal(activate(P))) 44.26/13.90 e() -> n__e() 44.26/13.90 i() -> n__i() 44.26/13.90 activate(n__nil()) -> nil() 44.26/13.90 U41(tt(),V2) -> U42(isNeList(activate(V2))) 44.26/13.90 isList(V) -> U11(isNeList(activate(V))) 44.26/13.90 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) 44.26/13.90 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) 44.26/13.90 isNeList(V) -> U31(isQid(activate(V))) 44.26/13.90 isPal(V) -> U81(isNePal(activate(V))) 44.26/13.90 __(X,nil()) -> X 44.26/13.90 __(nil(),X) -> X 44.26/13.90 U11(tt()) -> tt() 44.26/13.90 U22(tt()) -> tt() 44.26/13.90 U31(tt()) -> tt() 44.26/13.90 U42(tt()) -> tt() 44.26/13.90 U52(tt()) -> tt() 44.26/13.90 U61(tt()) -> tt() 44.26/13.90 U72(tt()) -> tt() 44.26/13.90 U81(tt()) -> tt() 44.26/13.90 isList(n__nil()) -> tt() 44.26/13.90 isNePal(V) -> U61(isQid(activate(V))) 44.26/13.90 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) 44.26/13.90 isPal(n__nil()) -> tt() 44.26/13.90 isQid(n__a()) -> tt() 44.26/13.90 isQid(n__e()) -> tt() 44.26/13.90 isQid(n__i()) -> tt() 44.26/13.90 isQid(n__o()) -> tt() 44.26/13.90 isQid(n__u()) -> tt() 44.26/13.90 nil() -> n__nil() 44.26/13.90 activate(n____(X1,X2)) -> __(X1,X2) 44.26/13.90 activate(n__a()) -> a() 44.26/13.90 activate(n__e()) -> e() 44.26/13.90 activate(n__i()) -> i() 44.26/13.90 activate(n__o()) -> o() 44.26/13.90 activate(n__u()) -> u() 44.26/13.90 activate(X) -> X 44.26/13.90 Qed 44.26/13.91 EOF