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()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> tt() , isNeList(V) -> U31(isQid(activate(V))) , isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) , 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: Computation stopped due to timeout after 5.0 seconds. 3) '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) '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()) -> c_6() , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) , U22^#(tt()) -> c_8() , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) , isList^#(n__nil()) -> c_10() , isList^#(n____(V1, V2)) -> c_11(U21^#(isList(activate(V1)), activate(V2))) , activate^#(X) -> c_12(X) , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n____(X1, X2)) -> c_14(__^#(X1, X2)) , activate^#(n__a()) -> c_15(a^#()) , activate^#(n__e()) -> c_16(e^#()) , activate^#(n__i()) -> c_17(i^#()) , activate^#(n__o()) -> c_18(o^#()) , activate^#(n__u()) -> c_19(u^#()) , a^#() -> c_41() , e^#() -> c_42() , i^#() -> c_43() , o^#() -> c_44() , u^#() -> c_45() , U31^#(tt()) -> c_20() , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) , U42^#(tt()) -> c_22() , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) , isNeList^#(n____(V1, V2)) -> c_24(U41^#(isList(activate(V1)), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_25(U51^#(isNeList(activate(V1)), activate(V2))) , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) , U52^#(tt()) -> c_27() , U61^#(tt()) -> c_28() , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) , U72^#(tt()) -> c_30() , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) , isPal^#(n__nil()) -> c_32() , U81^#(tt()) -> c_33() , isQid^#(n__a()) -> c_34() , isQid^#(n__e()) -> c_35() , isQid^#(n__i()) -> c_36() , isQid^#(n__o()) -> c_37() , isQid^#(n__u()) -> c_38() , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) , isNePal^#(n____(I, __(P, I))) -> c_40(U71^#(isQid(activate(I)), 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()) -> c_6() , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) , U22^#(tt()) -> c_8() , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) , isList^#(n__nil()) -> c_10() , isList^#(n____(V1, V2)) -> c_11(U21^#(isList(activate(V1)), activate(V2))) , activate^#(X) -> c_12(X) , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n____(X1, X2)) -> c_14(__^#(X1, X2)) , activate^#(n__a()) -> c_15(a^#()) , activate^#(n__e()) -> c_16(e^#()) , activate^#(n__i()) -> c_17(i^#()) , activate^#(n__o()) -> c_18(o^#()) , activate^#(n__u()) -> c_19(u^#()) , a^#() -> c_41() , e^#() -> c_42() , i^#() -> c_43() , o^#() -> c_44() , u^#() -> c_45() , U31^#(tt()) -> c_20() , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) , U42^#(tt()) -> c_22() , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) , isNeList^#(n____(V1, V2)) -> c_24(U41^#(isList(activate(V1)), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_25(U51^#(isNeList(activate(V1)), activate(V2))) , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) , U52^#(tt()) -> c_27() , U61^#(tt()) -> c_28() , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) , U72^#(tt()) -> c_30() , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) , isPal^#(n__nil()) -> c_32() , U81^#(tt()) -> c_33() , isQid^#(n__a()) -> c_34() , isQid^#(n__e()) -> c_35() , isQid^#(n__i()) -> c_36() , isQid^#(n__o()) -> c_37() , isQid^#(n__u()) -> c_38() , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) , isNePal^#(n____(I, __(P, I))) -> c_40(U71^#(isQid(activate(I)), activate(P))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> tt() , isNeList(V) -> U31(isQid(activate(V))) , isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) , 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,6,8,10,20,21,22,23,24,25,27,32,33,35,37,38,39,40,41,42,43} by applications of Pre({5,6,8,10,20,21,22,23,24,25,27,32,33,35,37,38,39,40,41,42,43}) = {1,2,4,7,9,12,13,15,16,17,18,19,26,28,31,34,36,44}. 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()) -> c_6() , 7: U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) , 8: U22^#(tt()) -> c_8() , 9: isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) , 10: isList^#(n__nil()) -> c_10() , 11: isList^#(n____(V1, V2)) -> c_11(U21^#(isList(activate(V1)), activate(V2))) , 12: activate^#(X) -> c_12(X) , 13: activate^#(n__nil()) -> c_13(nil^#()) , 14: activate^#(n____(X1, X2)) -> c_14(__^#(X1, X2)) , 15: activate^#(n__a()) -> c_15(a^#()) , 16: activate^#(n__e()) -> c_16(e^#()) , 17: activate^#(n__i()) -> c_17(i^#()) , 18: activate^#(n__o()) -> c_18(o^#()) , 19: activate^#(n__u()) -> c_19(u^#()) , 20: a^#() -> c_41() , 21: e^#() -> c_42() , 22: i^#() -> c_43() , 23: o^#() -> c_44() , 24: u^#() -> c_45() , 25: U31^#(tt()) -> c_20() , 26: U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) , 27: U42^#(tt()) -> c_22() , 28: isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) , 29: isNeList^#(n____(V1, V2)) -> c_24(U41^#(isList(activate(V1)), activate(V2))) , 30: isNeList^#(n____(V1, V2)) -> c_25(U51^#(isNeList(activate(V1)), activate(V2))) , 31: U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) , 32: U52^#(tt()) -> c_27() , 33: U61^#(tt()) -> c_28() , 34: U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) , 35: U72^#(tt()) -> c_30() , 36: isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) , 37: isPal^#(n__nil()) -> c_32() , 38: U81^#(tt()) -> c_33() , 39: isQid^#(n__a()) -> c_34() , 40: isQid^#(n__e()) -> c_35() , 41: isQid^#(n__i()) -> c_36() , 42: isQid^#(n__o()) -> c_37() , 43: isQid^#(n__u()) -> c_38() , 44: isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) , 45: isNePal^#(n____(I, __(P, I))) -> c_40(U71^#(isQid(activate(I)), 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) , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) , isList^#(n____(V1, V2)) -> c_11(U21^#(isList(activate(V1)), activate(V2))) , activate^#(X) -> c_12(X) , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n____(X1, X2)) -> c_14(__^#(X1, X2)) , activate^#(n__a()) -> c_15(a^#()) , activate^#(n__e()) -> c_16(e^#()) , activate^#(n__i()) -> c_17(i^#()) , activate^#(n__o()) -> c_18(o^#()) , activate^#(n__u()) -> c_19(u^#()) , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) , isNeList^#(n____(V1, V2)) -> c_24(U41^#(isList(activate(V1)), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_25(U51^#(isNeList(activate(V1)), activate(V2))) , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) , isNePal^#(n____(I, __(P, I))) -> c_40(U71^#(isQid(activate(I)), activate(P))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> tt() , isNeList(V) -> U31(isQid(activate(V))) , isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U11^#(tt()) -> c_6() , U22^#(tt()) -> c_8() , isList^#(n__nil()) -> c_10() , a^#() -> c_41() , e^#() -> c_42() , i^#() -> c_43() , o^#() -> c_44() , u^#() -> c_45() , U31^#(tt()) -> c_20() , U42^#(tt()) -> c_22() , U52^#(tt()) -> c_27() , U61^#(tt()) -> c_28() , U72^#(tt()) -> c_30() , isPal^#(n__nil()) -> c_32() , U81^#(tt()) -> c_33() , isQid^#(n__a()) -> c_34() , isQid^#(n__e()) -> c_35() , isQid^#(n__i()) -> c_36() , isQid^#(n__o()) -> c_37() , isQid^#(n__u()) -> c_38() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,6,9,11,12,13,14,15,16,17,20,21,22,23} by applications of Pre({5,6,9,11,12,13,14,15,16,17,20,21,22,23}) = {1,2,4,7,8,18,19,24}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1(X1, X2) , 2: __^#(X, nil()) -> c_2(X) , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) , 4: __^#(nil(), X) -> c_4(X) , 5: U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) , 6: isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) , 7: isList^#(n____(V1, V2)) -> c_11(U21^#(isList(activate(V1)), activate(V2))) , 8: activate^#(X) -> c_12(X) , 9: activate^#(n__nil()) -> c_13(nil^#()) , 10: activate^#(n____(X1, X2)) -> c_14(__^#(X1, X2)) , 11: activate^#(n__a()) -> c_15(a^#()) , 12: activate^#(n__e()) -> c_16(e^#()) , 13: activate^#(n__i()) -> c_17(i^#()) , 14: activate^#(n__o()) -> c_18(o^#()) , 15: activate^#(n__u()) -> c_19(u^#()) , 16: U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) , 17: isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) , 18: isNeList^#(n____(V1, V2)) -> c_24(U41^#(isList(activate(V1)), activate(V2))) , 19: isNeList^#(n____(V1, V2)) -> c_25(U51^#(isNeList(activate(V1)), activate(V2))) , 20: U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) , 21: U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) , 22: isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) , 23: isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) , 24: isNePal^#(n____(I, __(P, I))) -> c_40(U71^#(isQid(activate(I)), activate(P))) , 25: nil^#() -> c_5() , 26: U11^#(tt()) -> c_6() , 27: U22^#(tt()) -> c_8() , 28: isList^#(n__nil()) -> c_10() , 29: a^#() -> c_41() , 30: e^#() -> c_42() , 31: i^#() -> c_43() , 32: o^#() -> c_44() , 33: u^#() -> c_45() , 34: U31^#(tt()) -> c_20() , 35: U42^#(tt()) -> c_22() , 36: U52^#(tt()) -> c_27() , 37: U61^#(tt()) -> c_28() , 38: U72^#(tt()) -> c_30() , 39: isPal^#(n__nil()) -> c_32() , 40: U81^#(tt()) -> c_33() , 41: isQid^#(n__a()) -> c_34() , 42: isQid^#(n__e()) -> c_35() , 43: isQid^#(n__i()) -> c_36() , 44: isQid^#(n__o()) -> c_37() , 45: isQid^#(n__u()) -> c_38() } 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) , isList^#(n____(V1, V2)) -> c_11(U21^#(isList(activate(V1)), activate(V2))) , activate^#(X) -> c_12(X) , activate^#(n____(X1, X2)) -> c_14(__^#(X1, X2)) , isNeList^#(n____(V1, V2)) -> c_24(U41^#(isList(activate(V1)), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_25(U51^#(isNeList(activate(V1)), activate(V2))) , isNePal^#(n____(I, __(P, I))) -> c_40(U71^#(isQid(activate(I)), activate(P))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> tt() , isNeList(V) -> U31(isQid(activate(V))) , isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U11^#(tt()) -> c_6() , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) , U22^#(tt()) -> c_8() , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) , isList^#(n__nil()) -> c_10() , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n__a()) -> c_15(a^#()) , activate^#(n__e()) -> c_16(e^#()) , activate^#(n__i()) -> c_17(i^#()) , activate^#(n__o()) -> c_18(o^#()) , activate^#(n__u()) -> c_19(u^#()) , a^#() -> c_41() , e^#() -> c_42() , i^#() -> c_43() , o^#() -> c_44() , u^#() -> c_45() , U31^#(tt()) -> c_20() , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) , U42^#(tt()) -> c_22() , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) , U52^#(tt()) -> c_27() , U61^#(tt()) -> c_28() , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) , U72^#(tt()) -> c_30() , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) , isPal^#(n__nil()) -> c_32() , U81^#(tt()) -> c_33() , isQid^#(n__a()) -> c_34() , isQid^#(n__e()) -> c_35() , isQid^#(n__i()) -> c_36() , isQid^#(n__o()) -> c_37() , isQid^#(n__u()) -> c_38() , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,8,9,10} by applications of Pre({5,8,9,10}) = {1,2,4,6}. 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: isList^#(n____(V1, V2)) -> c_11(U21^#(isList(activate(V1)), activate(V2))) , 6: activate^#(X) -> c_12(X) , 7: activate^#(n____(X1, X2)) -> c_14(__^#(X1, X2)) , 8: isNeList^#(n____(V1, V2)) -> c_24(U41^#(isList(activate(V1)), activate(V2))) , 9: isNeList^#(n____(V1, V2)) -> c_25(U51^#(isNeList(activate(V1)), activate(V2))) , 10: isNePal^#(n____(I, __(P, I))) -> c_40(U71^#(isQid(activate(I)), activate(P))) , 11: nil^#() -> c_5() , 12: U11^#(tt()) -> c_6() , 13: U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) , 14: U22^#(tt()) -> c_8() , 15: isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) , 16: isList^#(n__nil()) -> c_10() , 17: activate^#(n__nil()) -> c_13(nil^#()) , 18: activate^#(n__a()) -> c_15(a^#()) , 19: activate^#(n__e()) -> c_16(e^#()) , 20: activate^#(n__i()) -> c_17(i^#()) , 21: activate^#(n__o()) -> c_18(o^#()) , 22: activate^#(n__u()) -> c_19(u^#()) , 23: a^#() -> c_41() , 24: e^#() -> c_42() , 25: i^#() -> c_43() , 26: o^#() -> c_44() , 27: u^#() -> c_45() , 28: U31^#(tt()) -> c_20() , 29: U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) , 30: U42^#(tt()) -> c_22() , 31: isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) , 32: U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) , 33: U52^#(tt()) -> c_27() , 34: U61^#(tt()) -> c_28() , 35: U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) , 36: U72^#(tt()) -> c_30() , 37: isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) , 38: isPal^#(n__nil()) -> c_32() , 39: U81^#(tt()) -> c_33() , 40: isQid^#(n__a()) -> c_34() , 41: isQid^#(n__e()) -> c_35() , 42: isQid^#(n__i()) -> c_36() , 43: isQid^#(n__o()) -> c_37() , 44: isQid^#(n__u()) -> c_38() , 45: isNePal^#(V) -> c_39(U61^#(isQid(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_12(X) , activate^#(n____(X1, X2)) -> c_14(__^#(X1, X2)) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> tt() , isNeList(V) -> U31(isQid(activate(V))) , isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)) , isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Weak DPs: { nil^#() -> c_5() , U11^#(tt()) -> c_6() , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) , U22^#(tt()) -> c_8() , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) , isList^#(n__nil()) -> c_10() , isList^#(n____(V1, V2)) -> c_11(U21^#(isList(activate(V1)), activate(V2))) , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n__a()) -> c_15(a^#()) , activate^#(n__e()) -> c_16(e^#()) , activate^#(n__i()) -> c_17(i^#()) , activate^#(n__o()) -> c_18(o^#()) , activate^#(n__u()) -> c_19(u^#()) , a^#() -> c_41() , e^#() -> c_42() , i^#() -> c_43() , o^#() -> c_44() , u^#() -> c_45() , U31^#(tt()) -> c_20() , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) , U42^#(tt()) -> c_22() , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) , isNeList^#(n____(V1, V2)) -> c_24(U41^#(isList(activate(V1)), activate(V2))) , isNeList^#(n____(V1, V2)) -> c_25(U51^#(isNeList(activate(V1)), activate(V2))) , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) , U52^#(tt()) -> c_27() , U61^#(tt()) -> c_28() , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) , U72^#(tt()) -> c_30() , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) , isPal^#(n__nil()) -> c_32() , U81^#(tt()) -> c_33() , isQid^#(n__a()) -> c_34() , isQid^#(n__e()) -> c_35() , isQid^#(n__i()) -> c_36() , isQid^#(n__o()) -> c_37() , isQid^#(n__u()) -> c_38() , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) , isNePal^#(n____(I, __(P, I))) -> c_40(U71^#(isQid(activate(I)), activate(P))) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..