MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , nil^#() -> c_5() , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(X) -> c_15(X) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , U26^#(tt()) -> c_35() , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_33() , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U46^#(tt()) -> c_49() , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U56^#(tt()) -> c_55() , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U63^#(tt()) -> c_58() , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , U74^#(tt()) -> c_64() , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , isPal^#(n__nil()) -> c_63() , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , U83^#(tt()) -> c_67() , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , U92^#(tt()) -> c_71() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , nil^#() -> c_5() , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(X) -> c_15(X) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , U26^#(tt()) -> c_35() , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_33() , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U46^#(tt()) -> c_49() , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U56^#(tt()) -> c_55() , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U63^#(tt()) -> c_58() , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , U74^#(tt()) -> c_64() , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , isPal^#(n__nil()) -> c_63() , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , U83^#(tt()) -> c_67() , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , U92^#(tt()) -> c_71() } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,8,9,11,12,13,14,15,25,26,27,28,29,41,43,46,47,48,49,50,51,56,61,64,68,70,73,76} by applications of Pre({5,8,9,11,12,13,14,15,25,26,27,28,29,41,43,46,47,48,49,50,51,56,61,64,68,70,73,76}) = {1,2,4,7,16,17,18,20,21,22,23,24,40,45,55,60,63,67,72}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1(X1, X2) , 2: __^#(X, nil()) -> c_2(X) , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , 4: __^#(nil(), X) -> c_4(X) , 5: nil^#() -> c_5() , 6: U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , 7: U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , 8: U13^#(tt()) -> c_23() , 9: isPalListKind^#(n__nil()) -> c_8() , 10: isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , 11: isPalListKind^#(n__a()) -> c_10() , 12: isPalListKind^#(n__e()) -> c_11() , 13: isPalListKind^#(n__i()) -> c_12() , 14: isPalListKind^#(n__o()) -> c_13() , 15: isPalListKind^#(n__u()) -> c_14() , 16: U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , 17: activate^#(X) -> c_15(X) , 18: activate^#(n__nil()) -> c_16(nil^#()) , 19: activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , 20: activate^#(n__a()) -> c_18(a^#()) , 21: activate^#(n__e()) -> c_19(e^#()) , 22: activate^#(n__i()) -> c_20(i^#()) , 23: activate^#(n__o()) -> c_21(o^#()) , 24: activate^#(n__u()) -> c_22(u^#()) , 25: a^#() -> c_72() , 26: e^#() -> c_73() , 27: i^#() -> c_74() , 28: o^#() -> c_75() , 29: u^#() -> c_76() , 30: isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , 31: isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 32: isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 33: U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , 34: U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 35: U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 36: U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 37: U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 38: U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 39: U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , 40: U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , 41: U26^#(tt()) -> c_35() , 42: isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , 43: isList^#(n__nil()) -> c_33() , 44: isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 45: U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , 46: U33^#(tt()) -> c_38() , 47: isQid^#(n__a()) -> c_39() , 48: isQid^#(n__e()) -> c_40() , 49: isQid^#(n__i()) -> c_41() , 50: isQid^#(n__o()) -> c_42() , 51: isQid^#(n__u()) -> c_43() , 52: U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 53: U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 54: U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , 55: U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , 56: U46^#(tt()) -> c_49() , 57: U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 58: U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 59: U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , 60: U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , 61: U56^#(tt()) -> c_55() , 62: U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , 63: U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , 64: U63^#(tt()) -> c_58() , 65: U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , 66: U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , 67: U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , 68: U74^#(tt()) -> c_64() , 69: isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , 70: isPal^#(n__nil()) -> c_63() , 71: U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , 72: U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , 73: U83^#(tt()) -> c_67() , 74: isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , 75: isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , 76: U92^#(tt()) -> c_71() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(X) -> c_15(X) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , U26^#(tt()) -> c_35() , isList^#(n__nil()) -> c_33() , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U46^#(tt()) -> c_49() , U56^#(tt()) -> c_55() , U63^#(tt()) -> c_58() , U74^#(tt()) -> c_64() , isPal^#(n__nil()) -> c_63() , U83^#(tt()) -> c_67() , U92^#(tt()) -> c_71() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {6,8,10,12,13,14,15,16,27,30,34,38,40,43,46} by applications of Pre({6,8,10,12,13,14,15,16,27,30,34,38,40,43,46}) = {1,2,4,5,7,9,20,26,33,37,39,42,45}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1(X1, X2) , 2: __^#(X, nil()) -> c_2(X) , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , 4: __^#(nil(), X) -> c_4(X) , 5: U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , 6: U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , 7: isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , 8: U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , 9: activate^#(X) -> c_15(X) , 10: activate^#(n__nil()) -> c_16(nil^#()) , 11: activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , 12: activate^#(n__a()) -> c_18(a^#()) , 13: activate^#(n__e()) -> c_19(e^#()) , 14: activate^#(n__i()) -> c_20(i^#()) , 15: activate^#(n__o()) -> c_21(o^#()) , 16: activate^#(n__u()) -> c_22(u^#()) , 17: isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , 18: isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 19: isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 20: U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , 21: U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 22: U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 23: U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 24: U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 25: U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 26: U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , 27: U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , 28: isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , 29: isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 30: U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , 31: U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 32: U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 33: U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , 34: U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , 35: U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 36: U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 37: U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , 38: U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , 39: U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , 40: U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , 41: U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , 42: U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , 43: U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , 44: isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , 45: U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , 46: U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , 47: isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , 48: isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , 49: nil^#() -> c_5() , 50: U13^#(tt()) -> c_23() , 51: isPalListKind^#(n__nil()) -> c_8() , 52: isPalListKind^#(n__a()) -> c_10() , 53: isPalListKind^#(n__e()) -> c_11() , 54: isPalListKind^#(n__i()) -> c_12() , 55: isPalListKind^#(n__o()) -> c_13() , 56: isPalListKind^#(n__u()) -> c_14() , 57: a^#() -> c_72() , 58: e^#() -> c_73() , 59: i^#() -> c_74() , 60: o^#() -> c_75() , 61: u^#() -> c_76() , 62: U26^#(tt()) -> c_35() , 63: isList^#(n__nil()) -> c_33() , 64: U33^#(tt()) -> c_38() , 65: isQid^#(n__a()) -> c_39() , 66: isQid^#(n__e()) -> c_40() , 67: isQid^#(n__i()) -> c_41() , 68: isQid^#(n__o()) -> c_42() , 69: isQid^#(n__u()) -> c_43() , 70: U46^#(tt()) -> c_49() , 71: U56^#(tt()) -> c_55() , 72: U63^#(tt()) -> c_58() , 73: U74^#(tt()) -> c_64() , 74: isPal^#(n__nil()) -> c_63() , 75: U83^#(tt()) -> c_67() , 76: U92^#(tt()) -> c_71() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , activate^#(X) -> c_15(X) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , U26^#(tt()) -> c_35() , isList^#(n__nil()) -> c_33() , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U46^#(tt()) -> c_49() , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U56^#(tt()) -> c_55() , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U63^#(tt()) -> c_58() , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , U74^#(tt()) -> c_64() , isPal^#(n__nil()) -> c_63() , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , U83^#(tt()) -> c_67() , U92^#(tt()) -> c_71() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,6,12,18,23,26,27,29,31} by applications of Pre({5,6,12,18,23,26,27,29,31}) = {1,2,4,7,9,17,19,22,25,28,30,32}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1(X1, X2) , 2: __^#(X, nil()) -> c_2(X) , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , 4: __^#(nil(), X) -> c_4(X) , 5: U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , 6: isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , 7: activate^#(X) -> c_15(X) , 8: activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , 9: isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , 10: isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 11: isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 12: U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , 13: U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 14: U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 15: U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 16: U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 17: U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 18: U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , 19: isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , 20: isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 21: U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 22: U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 23: U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , 24: U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 25: U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 26: U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , 27: U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , 28: U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , 29: U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , 30: isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , 31: U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , 32: isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , 33: isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , 34: nil^#() -> c_5() , 35: U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , 36: U13^#(tt()) -> c_23() , 37: isPalListKind^#(n__nil()) -> c_8() , 38: isPalListKind^#(n__a()) -> c_10() , 39: isPalListKind^#(n__e()) -> c_11() , 40: isPalListKind^#(n__i()) -> c_12() , 41: isPalListKind^#(n__o()) -> c_13() , 42: isPalListKind^#(n__u()) -> c_14() , 43: U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , 44: activate^#(n__nil()) -> c_16(nil^#()) , 45: activate^#(n__a()) -> c_18(a^#()) , 46: activate^#(n__e()) -> c_19(e^#()) , 47: activate^#(n__i()) -> c_20(i^#()) , 48: activate^#(n__o()) -> c_21(o^#()) , 49: activate^#(n__u()) -> c_22(u^#()) , 50: a^#() -> c_72() , 51: e^#() -> c_73() , 52: i^#() -> c_74() , 53: o^#() -> c_75() , 54: u^#() -> c_76() , 55: U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , 56: U26^#(tt()) -> c_35() , 57: isList^#(n__nil()) -> c_33() , 58: U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , 59: U33^#(tt()) -> c_38() , 60: isQid^#(n__a()) -> c_39() , 61: isQid^#(n__e()) -> c_40() , 62: isQid^#(n__i()) -> c_41() , 63: isQid^#(n__o()) -> c_42() , 64: isQid^#(n__u()) -> c_43() , 65: U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , 66: U46^#(tt()) -> c_49() , 67: U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , 68: U56^#(tt()) -> c_55() , 69: U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , 70: U63^#(tt()) -> c_58() , 71: U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , 72: U74^#(tt()) -> c_64() , 73: isPal^#(n__nil()) -> c_63() , 74: U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , 75: U83^#(tt()) -> c_67() , 76: U92^#(tt()) -> c_71() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , activate^#(X) -> c_15(X) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , U26^#(tt()) -> c_35() , isList^#(n__nil()) -> c_33() , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U46^#(tt()) -> c_49() , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U56^#(tt()) -> c_55() , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U63^#(tt()) -> c_58() , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , U74^#(tt()) -> c_64() , isPal^#(n__nil()) -> c_63() , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , U83^#(tt()) -> c_67() , U92^#(tt()) -> c_71() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {7,14,15,18,20,21,22,23} by applications of Pre({7,14,15,18,20,21,22,23}) = {1,2,4,5,13,17,19,24}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1(X1, X2) , 2: __^#(X, nil()) -> c_2(X) , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , 4: __^#(nil(), X) -> c_4(X) , 5: activate^#(X) -> c_15(X) , 6: activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , 7: isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , 8: isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 9: isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 10: U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 11: U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 12: U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 13: U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 14: U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 15: isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , 16: isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 17: U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 18: U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 19: U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 20: U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 21: U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , 22: isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , 23: isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , 24: isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , 25: nil^#() -> c_5() , 26: U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , 27: U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , 28: U13^#(tt()) -> c_23() , 29: isPalListKind^#(n__nil()) -> c_8() , 30: isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , 31: isPalListKind^#(n__a()) -> c_10() , 32: isPalListKind^#(n__e()) -> c_11() , 33: isPalListKind^#(n__i()) -> c_12() , 34: isPalListKind^#(n__o()) -> c_13() , 35: isPalListKind^#(n__u()) -> c_14() , 36: U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , 37: activate^#(n__nil()) -> c_16(nil^#()) , 38: activate^#(n__a()) -> c_18(a^#()) , 39: activate^#(n__e()) -> c_19(e^#()) , 40: activate^#(n__i()) -> c_20(i^#()) , 41: activate^#(n__o()) -> c_21(o^#()) , 42: activate^#(n__u()) -> c_22(u^#()) , 43: a^#() -> c_72() , 44: e^#() -> c_73() , 45: i^#() -> c_74() , 46: o^#() -> c_75() , 47: u^#() -> c_76() , 48: U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , 49: U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , 50: U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , 51: U26^#(tt()) -> c_35() , 52: isList^#(n__nil()) -> c_33() , 53: U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , 54: U33^#(tt()) -> c_38() , 55: isQid^#(n__a()) -> c_39() , 56: isQid^#(n__e()) -> c_40() , 57: isQid^#(n__i()) -> c_41() , 58: isQid^#(n__o()) -> c_42() , 59: isQid^#(n__u()) -> c_43() , 60: U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , 61: U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , 62: U46^#(tt()) -> c_49() , 63: U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , 64: U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , 65: U56^#(tt()) -> c_55() , 66: U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , 67: U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , 68: U63^#(tt()) -> c_58() , 69: U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , 70: U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , 71: U74^#(tt()) -> c_64() , 72: isPal^#(n__nil()) -> c_63() , 73: U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , 74: U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , 75: U83^#(tt()) -> c_67() , 76: U92^#(tt()) -> c_71() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , activate^#(X) -> c_15(X) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , U26^#(tt()) -> c_35() , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_33() , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U46^#(tt()) -> c_49() , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U56^#(tt()) -> c_55() , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U63^#(tt()) -> c_58() , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , U74^#(tt()) -> c_64() , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , isPal^#(n__nil()) -> c_63() , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , U83^#(tt()) -> c_67() , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , U92^#(tt()) -> c_71() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {12,14,15,16} by applications of Pre({12,14,15,16}) = {1,2,4,5,9,10,11}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1(X1, X2) , 2: __^#(X, nil()) -> c_2(X) , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , 4: __^#(nil(), X) -> c_4(X) , 5: activate^#(X) -> c_15(X) , 6: activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , 7: isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 8: isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 9: U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 10: U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 11: U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 12: U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 13: isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 14: U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 15: U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 16: isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , 17: nil^#() -> c_5() , 18: U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , 19: U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , 20: U13^#(tt()) -> c_23() , 21: isPalListKind^#(n__nil()) -> c_8() , 22: isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , 23: isPalListKind^#(n__a()) -> c_10() , 24: isPalListKind^#(n__e()) -> c_11() , 25: isPalListKind^#(n__i()) -> c_12() , 26: isPalListKind^#(n__o()) -> c_13() , 27: isPalListKind^#(n__u()) -> c_14() , 28: U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , 29: activate^#(n__nil()) -> c_16(nil^#()) , 30: activate^#(n__a()) -> c_18(a^#()) , 31: activate^#(n__e()) -> c_19(e^#()) , 32: activate^#(n__i()) -> c_20(i^#()) , 33: activate^#(n__o()) -> c_21(o^#()) , 34: activate^#(n__u()) -> c_22(u^#()) , 35: a^#() -> c_72() , 36: e^#() -> c_73() , 37: i^#() -> c_74() , 38: o^#() -> c_75() , 39: u^#() -> c_76() , 40: isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , 41: U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , 42: U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 43: U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , 44: U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , 45: U26^#(tt()) -> c_35() , 46: isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , 47: isList^#(n__nil()) -> c_33() , 48: U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , 49: U33^#(tt()) -> c_38() , 50: isQid^#(n__a()) -> c_39() , 51: isQid^#(n__e()) -> c_40() , 52: isQid^#(n__i()) -> c_41() , 53: isQid^#(n__o()) -> c_42() , 54: isQid^#(n__u()) -> c_43() , 55: U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 56: U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , 57: U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , 58: U46^#(tt()) -> c_49() , 59: U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 60: U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , 61: U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , 62: U56^#(tt()) -> c_55() , 63: U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , 64: U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , 65: U63^#(tt()) -> c_58() , 66: U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , 67: U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , 68: U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , 69: U74^#(tt()) -> c_64() , 70: isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , 71: isPal^#(n__nil()) -> c_63() , 72: U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , 73: U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , 74: U83^#(tt()) -> c_67() , 75: isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , 76: U92^#(tt()) -> c_71() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , activate^#(X) -> c_15(X) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , U26^#(tt()) -> c_35() , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_33() , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U46^#(tt()) -> c_49() , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U56^#(tt()) -> c_55() , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U63^#(tt()) -> c_58() , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , U74^#(tt()) -> c_64() , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , isPal^#(n__nil()) -> c_63() , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , U83^#(tt()) -> c_67() , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , U92^#(tt()) -> c_71() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {9,10,11} by applications of Pre({9,10,11}) = {1,2,4,5,7,8,12}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1(X1, X2) , 2: __^#(X, nil()) -> c_2(X) , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , 4: __^#(nil(), X) -> c_4(X) , 5: activate^#(X) -> c_15(X) , 6: activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , 7: isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 8: isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 9: U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 10: U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 11: U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 12: isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 13: nil^#() -> c_5() , 14: U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , 15: U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , 16: U13^#(tt()) -> c_23() , 17: isPalListKind^#(n__nil()) -> c_8() , 18: isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , 19: isPalListKind^#(n__a()) -> c_10() , 20: isPalListKind^#(n__e()) -> c_11() , 21: isPalListKind^#(n__i()) -> c_12() , 22: isPalListKind^#(n__o()) -> c_13() , 23: isPalListKind^#(n__u()) -> c_14() , 24: U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , 25: activate^#(n__nil()) -> c_16(nil^#()) , 26: activate^#(n__a()) -> c_18(a^#()) , 27: activate^#(n__e()) -> c_19(e^#()) , 28: activate^#(n__i()) -> c_20(i^#()) , 29: activate^#(n__o()) -> c_21(o^#()) , 30: activate^#(n__u()) -> c_22(u^#()) , 31: a^#() -> c_72() , 32: e^#() -> c_73() , 33: i^#() -> c_74() , 34: o^#() -> c_75() , 35: u^#() -> c_76() , 36: isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , 37: U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , 38: U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 39: U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 40: U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , 41: U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , 42: U26^#(tt()) -> c_35() , 43: isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , 44: isList^#(n__nil()) -> c_33() , 45: U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , 46: U33^#(tt()) -> c_38() , 47: isQid^#(n__a()) -> c_39() , 48: isQid^#(n__e()) -> c_40() , 49: isQid^#(n__i()) -> c_41() , 50: isQid^#(n__o()) -> c_42() , 51: isQid^#(n__u()) -> c_43() , 52: U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 53: U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 54: U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , 55: U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , 56: U46^#(tt()) -> c_49() , 57: U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 58: U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 59: U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , 60: U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , 61: U56^#(tt()) -> c_55() , 62: U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , 63: U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , 64: U63^#(tt()) -> c_58() , 65: U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , 66: U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , 67: U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , 68: U74^#(tt()) -> c_64() , 69: isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , 70: isPal^#(n__nil()) -> c_63() , 71: U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , 72: U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , 73: U83^#(tt()) -> c_67() , 74: isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , 75: isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , 76: U92^#(tt()) -> c_71() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , activate^#(X) -> c_15(X) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , U26^#(tt()) -> c_35() , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_33() , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U46^#(tt()) -> c_49() , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U56^#(tt()) -> c_55() , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U63^#(tt()) -> c_58() , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , U74^#(tt()) -> c_64() , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , isPal^#(n__nil()) -> c_63() , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , U83^#(tt()) -> c_67() , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , U92^#(tt()) -> c_71() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {7,8,9} by applications of Pre({7,8,9}) = {1,2,4,5}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1(X1, X2) , 2: __^#(X, nil()) -> c_2(X) , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , 4: __^#(nil(), X) -> c_4(X) , 5: activate^#(X) -> c_15(X) , 6: activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) , 7: isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 8: isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 9: isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 10: nil^#() -> c_5() , 11: U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , 12: U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , 13: U13^#(tt()) -> c_23() , 14: isPalListKind^#(n__nil()) -> c_8() , 15: isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , 16: isPalListKind^#(n__a()) -> c_10() , 17: isPalListKind^#(n__e()) -> c_11() , 18: isPalListKind^#(n__i()) -> c_12() , 19: isPalListKind^#(n__o()) -> c_13() , 20: isPalListKind^#(n__u()) -> c_14() , 21: U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , 22: activate^#(n__nil()) -> c_16(nil^#()) , 23: activate^#(n__a()) -> c_18(a^#()) , 24: activate^#(n__e()) -> c_19(e^#()) , 25: activate^#(n__i()) -> c_20(i^#()) , 26: activate^#(n__o()) -> c_21(o^#()) , 27: activate^#(n__u()) -> c_22(u^#()) , 28: a^#() -> c_72() , 29: e^#() -> c_73() , 30: i^#() -> c_74() , 31: o^#() -> c_75() , 32: u^#() -> c_76() , 33: isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , 34: U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , 35: U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 36: U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 37: U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , 38: U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 39: U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 40: U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , 41: U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , 42: U26^#(tt()) -> c_35() , 43: isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , 44: isList^#(n__nil()) -> c_33() , 45: U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , 46: U33^#(tt()) -> c_38() , 47: isQid^#(n__a()) -> c_39() , 48: isQid^#(n__e()) -> c_40() , 49: isQid^#(n__i()) -> c_41() , 50: isQid^#(n__o()) -> c_42() , 51: isQid^#(n__u()) -> c_43() , 52: U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 53: U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 54: U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , 55: U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , 56: U46^#(tt()) -> c_49() , 57: U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 58: U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , 59: U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , 60: U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , 61: U56^#(tt()) -> c_55() , 62: U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , 63: U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , 64: U63^#(tt()) -> c_58() , 65: U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , 66: U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , 67: U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , 68: U74^#(tt()) -> c_64() , 69: isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , 70: isPal^#(n__nil()) -> c_63() , 71: U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , 72: U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , 73: U83^#(tt()) -> c_67() , 74: isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , 75: isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , 76: U92^#(tt()) -> c_71() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, X2) -> c_1(X1, X2) , __^#(X, nil()) -> c_2(X) , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_4(X) , activate^#(X) -> c_15(X) , activate^#(n____(X1, X2)) -> c_17(__^#(X1, X2)) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt(), V) -> U12(isPalListKind(activate(V)), activate(V)) , U12(tt(), V) -> U13(isNeList(activate(V))) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> U91(isPalListKind(activate(V1)), activate(V2)) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U13(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U21(tt(), V1, V2) -> U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U22(tt(), V1, V2) -> U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U23(tt(), V1, V2) -> U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U24(tt(), V1, V2) -> U25(isList(activate(V1)), activate(V2)) , U25(tt(), V2) -> U26(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U26(tt()) -> tt() , U31(tt(), V) -> U32(isPalListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isQid(activate(V))) , U33(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , U41(tt(), V1, V2) -> U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isList(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNeList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) , U52(tt(), V1, V2) -> U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U53(tt(), V1, V2) -> U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) , U54(tt(), V1, V2) -> U55(isNeList(activate(V1)), activate(V2)) , U55(tt(), V2) -> U56(isList(activate(V2))) , U56(tt()) -> tt() , U61(tt(), V) -> U62(isPalListKind(activate(V)), activate(V)) , U62(tt(), V) -> U63(isQid(activate(V))) , U63(tt()) -> tt() , U71(tt(), I, P) -> U72(isPalListKind(activate(I)), activate(P)) , U72(tt(), P) -> U73(isPal(activate(P)), activate(P)) , U73(tt(), P) -> U74(isPalListKind(activate(P))) , isPal(V) -> U81(isPalListKind(activate(V)), activate(V)) , isPal(n__nil()) -> tt() , U74(tt()) -> tt() , U81(tt(), V) -> U82(isPalListKind(activate(V)), activate(V)) , U82(tt(), V) -> U83(isNePal(activate(V))) , U83(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(I), activate(P)) , U91(tt(), V2) -> U92(isPalListKind(activate(V2))) , U92(tt()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U11^#(tt(), V) -> c_6(U12^#(isPalListKind(activate(V)), activate(V))) , U12^#(tt(), V) -> c_7(U13^#(isNeList(activate(V)))) , U13^#(tt()) -> c_23() , isPalListKind^#(n__nil()) -> c_8() , isPalListKind^#(n____(V1, V2)) -> c_9(U91^#(isPalListKind(activate(V1)), activate(V2))) , isPalListKind^#(n__a()) -> c_10() , isPalListKind^#(n__e()) -> c_11() , isPalListKind^#(n__i()) -> c_12() , isPalListKind^#(n__o()) -> c_13() , isPalListKind^#(n__u()) -> c_14() , U91^#(tt(), V2) -> c_70(U92^#(isPalListKind(activate(V2)))) , activate^#(n__nil()) -> c_16(nil^#()) , activate^#(n__a()) -> c_18(a^#()) , activate^#(n__e()) -> c_19(e^#()) , activate^#(n__i()) -> c_20(i^#()) , activate^#(n__o()) -> c_21(o^#()) , activate^#(n__u()) -> c_22(u^#()) , a^#() -> c_72() , e^#() -> c_73() , i^#() -> c_74() , o^#() -> c_75() , u^#() -> c_76() , isNeList^#(V) -> c_24(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_25(U41^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_26(U51^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_36(U32^#(isPalListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_44(U42^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U51^#(tt(), V1, V2) -> c_50(U52^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U21^#(tt(), V1, V2) -> c_27(U22^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U22^#(tt(), V1, V2) -> c_28(U23^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U23^#(tt(), V1, V2) -> c_29(U24^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U24^#(tt(), V1, V2) -> c_30(U25^#(isList(activate(V1)), activate(V2))) , U25^#(tt(), V2) -> c_31(U26^#(isList(activate(V2)))) , U26^#(tt()) -> c_35() , isList^#(V) -> c_32(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_33() , isList^#(n____(V1, V2)) -> c_34(U21^#(isPalListKind(activate(V1)), activate(V1), activate(V2))) , U32^#(tt(), V) -> c_37(U33^#(isQid(activate(V)))) , U33^#(tt()) -> c_38() , isQid^#(n__a()) -> c_39() , isQid^#(n__e()) -> c_40() , isQid^#(n__i()) -> c_41() , isQid^#(n__o()) -> c_42() , isQid^#(n__u()) -> c_43() , U42^#(tt(), V1, V2) -> c_45(U43^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_46(U44^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_47(U45^#(isList(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_48(U46^#(isNeList(activate(V2)))) , U46^#(tt()) -> c_49() , U52^#(tt(), V1, V2) -> c_51(U53^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U53^#(tt(), V1, V2) -> c_52(U54^#(isPalListKind(activate(V2)), activate(V1), activate(V2))) , U54^#(tt(), V1, V2) -> c_53(U55^#(isNeList(activate(V1)), activate(V2))) , U55^#(tt(), V2) -> c_54(U56^#(isList(activate(V2)))) , U56^#(tt()) -> c_55() , U61^#(tt(), V) -> c_56(U62^#(isPalListKind(activate(V)), activate(V))) , U62^#(tt(), V) -> c_57(U63^#(isQid(activate(V)))) , U63^#(tt()) -> c_58() , U71^#(tt(), I, P) -> c_59(U72^#(isPalListKind(activate(I)), activate(P))) , U72^#(tt(), P) -> c_60(U73^#(isPal(activate(P)), activate(P))) , U73^#(tt(), P) -> c_61(U74^#(isPalListKind(activate(P)))) , U74^#(tt()) -> c_64() , isPal^#(V) -> c_62(U81^#(isPalListKind(activate(V)), activate(V))) , isPal^#(n__nil()) -> c_63() , U81^#(tt(), V) -> c_65(U82^#(isPalListKind(activate(V)), activate(V))) , U82^#(tt(), V) -> c_66(U83^#(isNePal(activate(V)))) , U83^#(tt()) -> c_67() , isNePal^#(V) -> c_68(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, __(P, I))) -> c_69(U71^#(isQid(activate(I)), activate(I), activate(P))) , U92^#(tt()) -> c_71() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..