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