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(isNeList(activate(V))) , U12(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isPalListKind(X)) -> isPalListKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) , U22(tt(), V2) -> U23(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isQid(activate(V))) , U32(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(isList(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNeList(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V) -> U62(isQid(activate(V))) , U62(tt()) -> tt() , U71(tt(), V) -> U72(isNePal(activate(V))) , U72(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, n____(P, I))) -> and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isPalListKind(X) -> n__isPalListKind(X) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> 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) '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) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) '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 2) '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 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^#(isNeList(activate(V)))) , U12^#(tt()) -> c_7() , isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , activate^#(X) -> c_11(X) , activate^#(n__nil()) -> c_12(nil^#()) , activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , activate^#(n__a()) -> c_17(a^#()) , activate^#(n__e()) -> c_18(e^#()) , activate^#(n__i()) -> c_19(i^#()) , activate^#(n__o()) -> c_20(o^#()) , activate^#(n__u()) -> c_21(u^#()) , isPalListKind^#(X) -> c_49(X) , isPalListKind^#(n__nil()) -> c_50() , isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , isPalListKind^#(n__a()) -> c_52() , isPalListKind^#(n__e()) -> c_53() , isPalListKind^#(n__i()) -> c_54() , isPalListKind^#(n__o()) -> c_55() , isPalListKind^#(n__u()) -> c_56() , and^#(X1, X2) -> c_47(X1, X2) , and^#(tt(), X) -> c_48(activate^#(X)) , isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , isPal^#(X) -> c_58(X) , isPal^#(n__nil()) -> c_59() , a^#() -> c_60() , e^#() -> c_61() , i^#() -> c_62() , o^#() -> c_63() , u^#() -> c_64() , U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , U23^#(tt()) -> c_27() , isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_25() , isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U32^#(tt()) -> c_29() , isQid^#(n__a()) -> c_30() , isQid^#(n__e()) -> c_31() , isQid^#(n__i()) -> c_32() , isQid^#(n__o()) -> c_33() , isQid^#(n__u()) -> c_34() , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , U43^#(tt()) -> c_37() , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , U53^#(tt()) -> c_40() , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , U62^#(tt()) -> c_42() , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , U72^#(tt()) -> c_44() , isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 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^#(isNeList(activate(V)))) , U12^#(tt()) -> c_7() , isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , activate^#(X) -> c_11(X) , activate^#(n__nil()) -> c_12(nil^#()) , activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , activate^#(n__a()) -> c_17(a^#()) , activate^#(n__e()) -> c_18(e^#()) , activate^#(n__i()) -> c_19(i^#()) , activate^#(n__o()) -> c_20(o^#()) , activate^#(n__u()) -> c_21(u^#()) , isPalListKind^#(X) -> c_49(X) , isPalListKind^#(n__nil()) -> c_50() , isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , isPalListKind^#(n__a()) -> c_52() , isPalListKind^#(n__e()) -> c_53() , isPalListKind^#(n__i()) -> c_54() , isPalListKind^#(n__o()) -> c_55() , isPalListKind^#(n__u()) -> c_56() , and^#(X1, X2) -> c_47(X1, X2) , and^#(tt(), X) -> c_48(activate^#(X)) , isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , isPal^#(X) -> c_58(X) , isPal^#(n__nil()) -> c_59() , a^#() -> c_60() , e^#() -> c_61() , i^#() -> c_62() , o^#() -> c_63() , u^#() -> c_64() , U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , U23^#(tt()) -> c_27() , isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_25() , isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U32^#(tt()) -> c_29() , isQid^#(n__a()) -> c_30() , isQid^#(n__e()) -> c_31() , isQid^#(n__i()) -> c_32() , isQid^#(n__o()) -> c_33() , isQid^#(n__u()) -> c_34() , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , U43^#(tt()) -> c_37() , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , U53^#(tt()) -> c_40() , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , U62^#(tt()) -> c_42() , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , U72^#(tt()) -> c_44() , isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(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(isNeList(activate(V))) , U12(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isPalListKind(X)) -> isPalListKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) , U22(tt(), V2) -> U23(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isQid(activate(V))) , U32(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(isList(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNeList(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V) -> U62(isQid(activate(V))) , U62(tt()) -> tt() , U71(tt(), V) -> U72(isNePal(activate(V))) , U72(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, n____(P, I))) -> and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isPalListKind(X) -> n__isPalListKind(X) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> 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,7,26,28,29,30,31,32,37,38,39,40,41,42,45,47,49,50,51,52,53,54,56,58,60,62} by applications of Pre({5,7,26,28,29,30,31,32,37,38,39,40,41,42,45,47,49,50,51,52,53,54,56,58,60,62}) = {1,2,4,6,11,14,15,17,19,20,21,22,23,24,25,33,36,44,55,57,59,61}. 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^#(isNeList(activate(V)))) , 7: U12^#(tt()) -> c_7() , 8: isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , 9: isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 10: isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 11: U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , 12: U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , 13: U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , 14: activate^#(X) -> c_11(X) , 15: activate^#(n__nil()) -> c_12(nil^#()) , 16: activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , 17: activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , 18: activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , 19: activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , 20: activate^#(n__a()) -> c_17(a^#()) , 21: activate^#(n__e()) -> c_18(e^#()) , 22: activate^#(n__i()) -> c_19(i^#()) , 23: activate^#(n__o()) -> c_20(o^#()) , 24: activate^#(n__u()) -> c_21(u^#()) , 25: isPalListKind^#(X) -> c_49(X) , 26: isPalListKind^#(n__nil()) -> c_50() , 27: isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , 28: isPalListKind^#(n__a()) -> c_52() , 29: isPalListKind^#(n__e()) -> c_53() , 30: isPalListKind^#(n__i()) -> c_54() , 31: isPalListKind^#(n__o()) -> c_55() , 32: isPalListKind^#(n__u()) -> c_56() , 33: and^#(X1, X2) -> c_47(X1, X2) , 34: and^#(tt(), X) -> c_48(activate^#(X)) , 35: isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , 36: isPal^#(X) -> c_58(X) , 37: isPal^#(n__nil()) -> c_59() , 38: a^#() -> c_60() , 39: e^#() -> c_61() , 40: i^#() -> c_62() , 41: o^#() -> c_63() , 42: u^#() -> c_64() , 43: U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , 44: U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , 45: U23^#(tt()) -> c_27() , 46: isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , 47: isList^#(n__nil()) -> c_25() , 48: isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 49: U32^#(tt()) -> c_29() , 50: isQid^#(n__a()) -> c_30() , 51: isQid^#(n__e()) -> c_31() , 52: isQid^#(n__i()) -> c_32() , 53: isQid^#(n__o()) -> c_33() , 54: isQid^#(n__u()) -> c_34() , 55: U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , 56: U43^#(tt()) -> c_37() , 57: U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , 58: U53^#(tt()) -> c_40() , 59: U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , 60: U62^#(tt()) -> c_42() , 61: U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , 62: U72^#(tt()) -> c_44() , 63: isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) , 64: isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 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^#(isNeList(activate(V)))) , isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , activate^#(X) -> c_11(X) , activate^#(n__nil()) -> c_12(nil^#()) , activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , activate^#(n__a()) -> c_17(a^#()) , activate^#(n__e()) -> c_18(e^#()) , activate^#(n__i()) -> c_19(i^#()) , activate^#(n__o()) -> c_20(o^#()) , activate^#(n__u()) -> c_21(u^#()) , isPalListKind^#(X) -> c_49(X) , isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , and^#(X1, X2) -> c_47(X1, X2) , and^#(tt(), X) -> c_48(activate^#(X)) , isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , isPal^#(X) -> c_58(X) , U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(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(isNeList(activate(V))) , U12(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isPalListKind(X)) -> isPalListKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) , U22(tt(), V2) -> U23(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isQid(activate(V))) , U32(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(isList(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNeList(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V) -> U62(isQid(activate(V))) , U62(tt()) -> tt() , U71(tt(), V) -> U72(isNePal(activate(V))) , U72(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, n____(P, I))) -> and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isPalListKind(X) -> n__isPalListKind(X) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U12^#(tt()) -> c_7() , isPalListKind^#(n__nil()) -> c_50() , isPalListKind^#(n__a()) -> c_52() , isPalListKind^#(n__e()) -> c_53() , isPalListKind^#(n__i()) -> c_54() , isPalListKind^#(n__o()) -> c_55() , isPalListKind^#(n__u()) -> c_56() , isPal^#(n__nil()) -> c_59() , a^#() -> c_60() , e^#() -> c_61() , i^#() -> c_62() , o^#() -> c_63() , u^#() -> c_64() , U23^#(tt()) -> c_27() , isList^#(n__nil()) -> c_25() , U32^#(tt()) -> c_29() , isQid^#(n__a()) -> c_30() , isQid^#(n__e()) -> c_31() , isQid^#(n__i()) -> c_32() , isQid^#(n__o()) -> c_33() , isQid^#(n__u()) -> c_34() , U43^#(tt()) -> c_37() , U53^#(tt()) -> c_40() , U62^#(tt()) -> c_42() , U72^#(tt()) -> c_44() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,9,13,18,19,20,21,22,30,33,34,35,36} by applications of Pre({5,9,13,18,19,20,21,22,30,33,34,35,36}) = {1,2,4,6,10,11,12,23,25,26,27,28,29,31,37}. 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^#(isNeList(activate(V)))) , 6: isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , 7: isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 8: isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 9: U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , 10: U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , 11: U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , 12: activate^#(X) -> c_11(X) , 13: activate^#(n__nil()) -> c_12(nil^#()) , 14: activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , 15: activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , 16: activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , 17: activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , 18: activate^#(n__a()) -> c_17(a^#()) , 19: activate^#(n__e()) -> c_18(e^#()) , 20: activate^#(n__i()) -> c_19(i^#()) , 21: activate^#(n__o()) -> c_20(o^#()) , 22: activate^#(n__u()) -> c_21(u^#()) , 23: isPalListKind^#(X) -> c_49(X) , 24: isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , 25: and^#(X1, X2) -> c_47(X1, X2) , 26: and^#(tt(), X) -> c_48(activate^#(X)) , 27: isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , 28: isPal^#(X) -> c_58(X) , 29: U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , 30: U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , 31: isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , 32: isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 33: U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , 34: U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , 35: U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , 36: U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , 37: isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) , 38: isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) , 39: nil^#() -> c_5() , 40: U12^#(tt()) -> c_7() , 41: isPalListKind^#(n__nil()) -> c_50() , 42: isPalListKind^#(n__a()) -> c_52() , 43: isPalListKind^#(n__e()) -> c_53() , 44: isPalListKind^#(n__i()) -> c_54() , 45: isPalListKind^#(n__o()) -> c_55() , 46: isPalListKind^#(n__u()) -> c_56() , 47: isPal^#(n__nil()) -> c_59() , 48: a^#() -> c_60() , 49: e^#() -> c_61() , 50: i^#() -> c_62() , 51: o^#() -> c_63() , 52: u^#() -> c_64() , 53: U23^#(tt()) -> c_27() , 54: isList^#(n__nil()) -> c_25() , 55: U32^#(tt()) -> c_29() , 56: isQid^#(n__a()) -> c_30() , 57: isQid^#(n__e()) -> c_31() , 58: isQid^#(n__i()) -> c_32() , 59: isQid^#(n__o()) -> c_33() , 60: isQid^#(n__u()) -> c_34() , 61: U43^#(tt()) -> c_37() , 62: U53^#(tt()) -> c_40() , 63: U62^#(tt()) -> c_42() , 64: U72^#(tt()) -> c_44() } 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) , isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , activate^#(X) -> c_11(X) , activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , isPalListKind^#(X) -> c_49(X) , isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , and^#(X1, X2) -> c_47(X1, X2) , and^#(tt(), X) -> c_48(activate^#(X)) , isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , isPal^#(X) -> c_58(X) , U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(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(isNeList(activate(V))) , U12(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isPalListKind(X)) -> isPalListKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) , U22(tt(), V2) -> U23(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isQid(activate(V))) , U32(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(isList(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNeList(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V) -> U62(isQid(activate(V))) , U62(tt()) -> tt() , U71(tt(), V) -> U72(isNePal(activate(V))) , U72(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, n____(P, I))) -> and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isPalListKind(X) -> n__isPalListKind(X) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> 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^#(isNeList(activate(V)))) , U12^#(tt()) -> c_7() , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , activate^#(n__nil()) -> c_12(nil^#()) , activate^#(n__a()) -> c_17(a^#()) , activate^#(n__e()) -> c_18(e^#()) , activate^#(n__i()) -> c_19(i^#()) , activate^#(n__o()) -> c_20(o^#()) , activate^#(n__u()) -> c_21(u^#()) , isPalListKind^#(n__nil()) -> c_50() , isPalListKind^#(n__a()) -> c_52() , isPalListKind^#(n__e()) -> c_53() , isPalListKind^#(n__i()) -> c_54() , isPalListKind^#(n__o()) -> c_55() , isPalListKind^#(n__u()) -> c_56() , isPal^#(n__nil()) -> c_59() , a^#() -> c_60() , e^#() -> c_61() , i^#() -> c_62() , o^#() -> c_63() , u^#() -> c_64() , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , U23^#(tt()) -> c_27() , isList^#(n__nil()) -> c_25() , U32^#(tt()) -> c_29() , isQid^#(n__a()) -> c_30() , isQid^#(n__e()) -> c_31() , isQid^#(n__i()) -> c_32() , isQid^#(n__o()) -> c_33() , isQid^#(n__u()) -> c_34() , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , U43^#(tt()) -> c_37() , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , U53^#(tt()) -> c_40() , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , U62^#(tt()) -> c_42() , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , U72^#(tt()) -> c_44() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,8,9,19,21,22,24} by applications of Pre({5,8,9,19,21,22,24}) = {1,2,4,6,7,10,14,15,17,20,23}. 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: isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , 6: isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 7: isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 8: U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , 9: U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , 10: activate^#(X) -> c_11(X) , 11: activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , 12: activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , 13: activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , 14: activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , 15: isPalListKind^#(X) -> c_49(X) , 16: isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , 17: and^#(X1, X2) -> c_47(X1, X2) , 18: and^#(tt(), X) -> c_48(activate^#(X)) , 19: isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , 20: isPal^#(X) -> c_58(X) , 21: U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , 22: isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , 23: isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 24: isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) , 25: isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) , 26: nil^#() -> c_5() , 27: U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) , 28: U12^#(tt()) -> c_7() , 29: U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , 30: activate^#(n__nil()) -> c_12(nil^#()) , 31: activate^#(n__a()) -> c_17(a^#()) , 32: activate^#(n__e()) -> c_18(e^#()) , 33: activate^#(n__i()) -> c_19(i^#()) , 34: activate^#(n__o()) -> c_20(o^#()) , 35: activate^#(n__u()) -> c_21(u^#()) , 36: isPalListKind^#(n__nil()) -> c_50() , 37: isPalListKind^#(n__a()) -> c_52() , 38: isPalListKind^#(n__e()) -> c_53() , 39: isPalListKind^#(n__i()) -> c_54() , 40: isPalListKind^#(n__o()) -> c_55() , 41: isPalListKind^#(n__u()) -> c_56() , 42: isPal^#(n__nil()) -> c_59() , 43: a^#() -> c_60() , 44: e^#() -> c_61() , 45: i^#() -> c_62() , 46: o^#() -> c_63() , 47: u^#() -> c_64() , 48: U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , 49: U23^#(tt()) -> c_27() , 50: isList^#(n__nil()) -> c_25() , 51: U32^#(tt()) -> c_29() , 52: isQid^#(n__a()) -> c_30() , 53: isQid^#(n__e()) -> c_31() , 54: isQid^#(n__i()) -> c_32() , 55: isQid^#(n__o()) -> c_33() , 56: isQid^#(n__u()) -> c_34() , 57: U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , 58: U43^#(tt()) -> c_37() , 59: U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , 60: U53^#(tt()) -> c_40() , 61: U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , 62: U62^#(tt()) -> c_42() , 63: U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , 64: U72^#(tt()) -> c_44() } 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) , isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , activate^#(X) -> c_11(X) , activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , isPalListKind^#(X) -> c_49(X) , isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , and^#(X1, X2) -> c_47(X1, X2) , and^#(tt(), X) -> c_48(activate^#(X)) , isPal^#(X) -> c_58(X) , isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(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(isNeList(activate(V))) , U12(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isPalListKind(X)) -> isPalListKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) , U22(tt(), V2) -> U23(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isQid(activate(V))) , U32(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(isList(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNeList(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V) -> U62(isQid(activate(V))) , U62(tt()) -> tt() , U71(tt(), V) -> U72(isNePal(activate(V))) , U72(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, n____(P, I))) -> and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isPalListKind(X) -> n__isPalListKind(X) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> 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^#(isNeList(activate(V)))) , U12^#(tt()) -> c_7() , isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , activate^#(n__nil()) -> c_12(nil^#()) , activate^#(n__a()) -> c_17(a^#()) , activate^#(n__e()) -> c_18(e^#()) , activate^#(n__i()) -> c_19(i^#()) , activate^#(n__o()) -> c_20(o^#()) , activate^#(n__u()) -> c_21(u^#()) , isPalListKind^#(n__nil()) -> c_50() , isPalListKind^#(n__a()) -> c_52() , isPalListKind^#(n__e()) -> c_53() , isPalListKind^#(n__i()) -> c_54() , isPalListKind^#(n__o()) -> c_55() , isPalListKind^#(n__u()) -> c_56() , isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , isPal^#(n__nil()) -> c_59() , a^#() -> c_60() , e^#() -> c_61() , i^#() -> c_62() , o^#() -> c_63() , u^#() -> c_64() , U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , U23^#(tt()) -> c_27() , isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_25() , U32^#(tt()) -> c_29() , isQid^#(n__a()) -> c_30() , isQid^#(n__e()) -> c_31() , isQid^#(n__i()) -> c_32() , isQid^#(n__o()) -> c_33() , isQid^#(n__u()) -> c_34() , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , U43^#(tt()) -> c_37() , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , U53^#(tt()) -> c_40() , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , U62^#(tt()) -> c_42() , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , U72^#(tt()) -> c_44() , isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,6,17} by applications of Pre({5,6,17}) = {1,2,4,7,12,14,16}. 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: isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 6: isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 7: activate^#(X) -> c_11(X) , 8: activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , 9: activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , 10: activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , 11: activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , 12: isPalListKind^#(X) -> c_49(X) , 13: isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , 14: and^#(X1, X2) -> c_47(X1, X2) , 15: and^#(tt(), X) -> c_48(activate^#(X)) , 16: isPal^#(X) -> c_58(X) , 17: isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , 18: isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) , 19: nil^#() -> c_5() , 20: U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) , 21: U12^#(tt()) -> c_7() , 22: isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , 23: U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , 24: U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , 25: U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , 26: activate^#(n__nil()) -> c_12(nil^#()) , 27: activate^#(n__a()) -> c_17(a^#()) , 28: activate^#(n__e()) -> c_18(e^#()) , 29: activate^#(n__i()) -> c_19(i^#()) , 30: activate^#(n__o()) -> c_20(o^#()) , 31: activate^#(n__u()) -> c_21(u^#()) , 32: isPalListKind^#(n__nil()) -> c_50() , 33: isPalListKind^#(n__a()) -> c_52() , 34: isPalListKind^#(n__e()) -> c_53() , 35: isPalListKind^#(n__i()) -> c_54() , 36: isPalListKind^#(n__o()) -> c_55() , 37: isPalListKind^#(n__u()) -> c_56() , 38: isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , 39: isPal^#(n__nil()) -> c_59() , 40: a^#() -> c_60() , 41: e^#() -> c_61() , 42: i^#() -> c_62() , 43: o^#() -> c_63() , 44: u^#() -> c_64() , 45: U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , 46: U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , 47: U23^#(tt()) -> c_27() , 48: isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , 49: isList^#(n__nil()) -> c_25() , 50: U32^#(tt()) -> c_29() , 51: isQid^#(n__a()) -> c_30() , 52: isQid^#(n__e()) -> c_31() , 53: isQid^#(n__i()) -> c_32() , 54: isQid^#(n__o()) -> c_33() , 55: isQid^#(n__u()) -> c_34() , 56: U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , 57: U43^#(tt()) -> c_37() , 58: U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , 59: U53^#(tt()) -> c_40() , 60: U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , 61: U62^#(tt()) -> c_42() , 62: U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , 63: U72^#(tt()) -> c_44() , 64: isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) } 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_11(X) , activate^#(n____(X1, X2)) -> c_13(__^#(activate(X1), activate(X2))) , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) , isPalListKind^#(X) -> c_49(X) , isPalListKind^#(n____(V1, V2)) -> c_51(and^#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) , and^#(X1, X2) -> c_47(X1, X2) , and^#(tt(), X) -> c_48(activate^#(X)) , isPal^#(X) -> c_58(X) , isNePal^#(n____(I, n____(P, I))) -> c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(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(isNeList(activate(V))) , U12(tt()) -> tt() , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) , isNeList(n____(V1, V2)) -> U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , isNeList(n____(V1, V2)) -> U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isPalListKind(X)) -> isPalListKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isPal(X)) -> isPal(X) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) , U22(tt(), V2) -> U23(isList(activate(V2))) , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isQid(activate(V))) , U32(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(isList(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNeList(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V) -> U62(isQid(activate(V))) , U62(tt()) -> tt() , U71(tt(), V) -> U72(isNePal(activate(V))) , U72(tt()) -> tt() , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) , isNePal(n____(I, n____(P, I))) -> and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isPalListKind(X) -> n__isPalListKind(X) , isPalListKind(n__nil()) -> tt() , isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) , isPalListKind(n__a()) -> tt() , isPalListKind(n__e()) -> tt() , isPalListKind(n__i()) -> tt() , isPalListKind(n__o()) -> tt() , isPalListKind(n__u()) -> tt() , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) , isPal(X) -> n__isPal(X) , isPal(n__nil()) -> 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^#(isNeList(activate(V)))) , U12^#(tt()) -> c_7() , isNeList^#(V) -> c_8(U31^#(isPalListKind(activate(V)), activate(V))) , isNeList^#(n____(V1, V2)) -> c_9(U41^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_10(U51^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) , U41^#(tt(), V1, V2) -> c_35(U42^#(isList(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_38(U52^#(isNeList(activate(V1)), activate(V2))) , activate^#(n__nil()) -> c_12(nil^#()) , activate^#(n__a()) -> c_17(a^#()) , activate^#(n__e()) -> c_18(e^#()) , activate^#(n__i()) -> c_19(i^#()) , activate^#(n__o()) -> c_20(o^#()) , activate^#(n__u()) -> c_21(u^#()) , isPalListKind^#(n__nil()) -> c_50() , isPalListKind^#(n__a()) -> c_52() , isPalListKind^#(n__e()) -> c_53() , isPalListKind^#(n__i()) -> c_54() , isPalListKind^#(n__o()) -> c_55() , isPalListKind^#(n__u()) -> c_56() , isPal^#(V) -> c_57(U71^#(isPalListKind(activate(V)), activate(V))) , isPal^#(n__nil()) -> c_59() , a^#() -> c_60() , e^#() -> c_61() , i^#() -> c_62() , o^#() -> c_63() , u^#() -> c_64() , U21^#(tt(), V1, V2) -> c_22(U22^#(isList(activate(V1)), activate(V2))) , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) , U23^#(tt()) -> c_27() , isList^#(V) -> c_24(U11^#(isPalListKind(activate(V)), activate(V))) , isList^#(n__nil()) -> c_25() , isList^#(n____(V1, V2)) -> c_26(U21^#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) , U32^#(tt()) -> c_29() , isQid^#(n__a()) -> c_30() , isQid^#(n__e()) -> c_31() , isQid^#(n__i()) -> c_32() , isQid^#(n__o()) -> c_33() , isQid^#(n__u()) -> c_34() , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) , U43^#(tt()) -> c_37() , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) , U53^#(tt()) -> c_40() , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) , U62^#(tt()) -> c_42() , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) , U72^#(tt()) -> c_44() , isNePal^#(V) -> c_45(U61^#(isPalListKind(activate(V)), activate(V))) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..