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() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , 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() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(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: 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() , and^#(tt(), X) -> c_6(activate^#(X)) , activate^#(X) -> c_7(X) , activate^#(n__nil()) -> c_8(nil^#()) , activate^#(n____(X1, X2)) -> c_9(__^#(activate(X1), activate(X2))) , activate^#(n__isList(X)) -> c_10(isList^#(X)) , activate^#(n__isNeList(X)) -> c_11(isNeList^#(X)) , activate^#(n__isPal(X)) -> c_12(isPal^#(X)) , activate^#(n__a()) -> c_13(a^#()) , activate^#(n__e()) -> c_14(e^#()) , activate^#(n__i()) -> c_15(i^#()) , activate^#(n__o()) -> c_16(o^#()) , activate^#(n__u()) -> c_17(u^#()) , isList^#(V) -> c_18(isNeList^#(activate(V))) , isList^#(X) -> c_19(X) , isList^#(n__nil()) -> c_20() , isList^#(n____(V1, V2)) -> c_21(and^#(isList(activate(V1)), n__isList(activate(V2)))) , isNeList^#(V) -> c_22(isQid^#(activate(V))) , isNeList^#(X) -> c_23(X) , isNeList^#(n____(V1, V2)) -> c_24(and^#(isList(activate(V1)), n__isNeList(activate(V2)))) , isNeList^#(n____(V1, V2)) -> c_25(and^#(isNeList(activate(V1)), n__isList(activate(V2)))) , isPal^#(V) -> c_33(isNePal^#(activate(V))) , isPal^#(X) -> c_34(X) , isPal^#(n__nil()) -> c_35() , a^#() -> c_36() , e^#() -> c_37() , i^#() -> c_38() , o^#() -> c_39() , u^#() -> c_40() , isQid^#(n__a()) -> c_26() , isQid^#(n__e()) -> c_27() , isQid^#(n__i()) -> c_28() , isQid^#(n__o()) -> c_29() , isQid^#(n__u()) -> c_30() , isNePal^#(V) -> c_31(isQid^#(activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_32(and^#(isQid(activate(I)), n__isPal(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() , and^#(tt(), X) -> c_6(activate^#(X)) , activate^#(X) -> c_7(X) , activate^#(n__nil()) -> c_8(nil^#()) , activate^#(n____(X1, X2)) -> c_9(__^#(activate(X1), activate(X2))) , activate^#(n__isList(X)) -> c_10(isList^#(X)) , activate^#(n__isNeList(X)) -> c_11(isNeList^#(X)) , activate^#(n__isPal(X)) -> c_12(isPal^#(X)) , activate^#(n__a()) -> c_13(a^#()) , activate^#(n__e()) -> c_14(e^#()) , activate^#(n__i()) -> c_15(i^#()) , activate^#(n__o()) -> c_16(o^#()) , activate^#(n__u()) -> c_17(u^#()) , isList^#(V) -> c_18(isNeList^#(activate(V))) , isList^#(X) -> c_19(X) , isList^#(n__nil()) -> c_20() , isList^#(n____(V1, V2)) -> c_21(and^#(isList(activate(V1)), n__isList(activate(V2)))) , isNeList^#(V) -> c_22(isQid^#(activate(V))) , isNeList^#(X) -> c_23(X) , isNeList^#(n____(V1, V2)) -> c_24(and^#(isList(activate(V1)), n__isNeList(activate(V2)))) , isNeList^#(n____(V1, V2)) -> c_25(and^#(isNeList(activate(V1)), n__isList(activate(V2)))) , isPal^#(V) -> c_33(isNePal^#(activate(V))) , isPal^#(X) -> c_34(X) , isPal^#(n__nil()) -> c_35() , a^#() -> c_36() , e^#() -> c_37() , i^#() -> c_38() , o^#() -> c_39() , u^#() -> c_40() , isQid^#(n__a()) -> c_26() , isQid^#(n__e()) -> c_27() , isQid^#(n__i()) -> c_28() , isQid^#(n__o()) -> c_29() , isQid^#(n__u()) -> c_30() , isNePal^#(V) -> c_31(isQid^#(activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_32(and^#(isQid(activate(I)), n__isPal(activate(P)))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , 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() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(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,20,28,29,30,31,32,33,34,35,36,37,38} by applications of Pre({5,20,28,29,30,31,32,33,34,35,36,37,38}) = {1,2,4,7,8,10,12,13,14,15,16,17,19,22,23,27,39}. 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: and^#(tt(), X) -> c_6(activate^#(X)) , 7: activate^#(X) -> c_7(X) , 8: activate^#(n__nil()) -> c_8(nil^#()) , 9: activate^#(n____(X1, X2)) -> c_9(__^#(activate(X1), activate(X2))) , 10: activate^#(n__isList(X)) -> c_10(isList^#(X)) , 11: activate^#(n__isNeList(X)) -> c_11(isNeList^#(X)) , 12: activate^#(n__isPal(X)) -> c_12(isPal^#(X)) , 13: activate^#(n__a()) -> c_13(a^#()) , 14: activate^#(n__e()) -> c_14(e^#()) , 15: activate^#(n__i()) -> c_15(i^#()) , 16: activate^#(n__o()) -> c_16(o^#()) , 17: activate^#(n__u()) -> c_17(u^#()) , 18: isList^#(V) -> c_18(isNeList^#(activate(V))) , 19: isList^#(X) -> c_19(X) , 20: isList^#(n__nil()) -> c_20() , 21: isList^#(n____(V1, V2)) -> c_21(and^#(isList(activate(V1)), n__isList(activate(V2)))) , 22: isNeList^#(V) -> c_22(isQid^#(activate(V))) , 23: isNeList^#(X) -> c_23(X) , 24: isNeList^#(n____(V1, V2)) -> c_24(and^#(isList(activate(V1)), n__isNeList(activate(V2)))) , 25: isNeList^#(n____(V1, V2)) -> c_25(and^#(isNeList(activate(V1)), n__isList(activate(V2)))) , 26: isPal^#(V) -> c_33(isNePal^#(activate(V))) , 27: isPal^#(X) -> c_34(X) , 28: isPal^#(n__nil()) -> c_35() , 29: a^#() -> c_36() , 30: e^#() -> c_37() , 31: i^#() -> c_38() , 32: o^#() -> c_39() , 33: u^#() -> c_40() , 34: isQid^#(n__a()) -> c_26() , 35: isQid^#(n__e()) -> c_27() , 36: isQid^#(n__i()) -> c_28() , 37: isQid^#(n__o()) -> c_29() , 38: isQid^#(n__u()) -> c_30() , 39: isNePal^#(V) -> c_31(isQid^#(activate(V))) , 40: isNePal^#(n____(I, n____(P, I))) -> c_32(and^#(isQid(activate(I)), n__isPal(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) , and^#(tt(), X) -> c_6(activate^#(X)) , activate^#(X) -> c_7(X) , activate^#(n__nil()) -> c_8(nil^#()) , activate^#(n____(X1, X2)) -> c_9(__^#(activate(X1), activate(X2))) , activate^#(n__isList(X)) -> c_10(isList^#(X)) , activate^#(n__isNeList(X)) -> c_11(isNeList^#(X)) , activate^#(n__isPal(X)) -> c_12(isPal^#(X)) , activate^#(n__a()) -> c_13(a^#()) , activate^#(n__e()) -> c_14(e^#()) , activate^#(n__i()) -> c_15(i^#()) , activate^#(n__o()) -> c_16(o^#()) , activate^#(n__u()) -> c_17(u^#()) , isList^#(V) -> c_18(isNeList^#(activate(V))) , isList^#(X) -> c_19(X) , isList^#(n____(V1, V2)) -> c_21(and^#(isList(activate(V1)), n__isList(activate(V2)))) , isNeList^#(V) -> c_22(isQid^#(activate(V))) , isNeList^#(X) -> c_23(X) , isNeList^#(n____(V1, V2)) -> c_24(and^#(isList(activate(V1)), n__isNeList(activate(V2)))) , isNeList^#(n____(V1, V2)) -> c_25(and^#(isNeList(activate(V1)), n__isList(activate(V2)))) , isPal^#(V) -> c_33(isNePal^#(activate(V))) , isPal^#(X) -> c_34(X) , isNePal^#(V) -> c_31(isQid^#(activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_32(and^#(isQid(activate(I)), n__isPal(activate(P)))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , 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() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(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() , isList^#(n__nil()) -> c_20() , isPal^#(n__nil()) -> c_35() , a^#() -> c_36() , e^#() -> c_37() , i^#() -> c_38() , o^#() -> c_39() , u^#() -> c_40() , isQid^#(n__a()) -> c_26() , isQid^#(n__e()) -> c_27() , isQid^#(n__i()) -> c_28() , isQid^#(n__o()) -> c_29() , isQid^#(n__u()) -> c_30() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {7,12,13,14,15,16,20,26} by applications of Pre({7,12,13,14,15,16,20,26}) = {1,2,4,5,6,10,17,18,21,24,25}. 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: and^#(tt(), X) -> c_6(activate^#(X)) , 6: activate^#(X) -> c_7(X) , 7: activate^#(n__nil()) -> c_8(nil^#()) , 8: activate^#(n____(X1, X2)) -> c_9(__^#(activate(X1), activate(X2))) , 9: activate^#(n__isList(X)) -> c_10(isList^#(X)) , 10: activate^#(n__isNeList(X)) -> c_11(isNeList^#(X)) , 11: activate^#(n__isPal(X)) -> c_12(isPal^#(X)) , 12: activate^#(n__a()) -> c_13(a^#()) , 13: activate^#(n__e()) -> c_14(e^#()) , 14: activate^#(n__i()) -> c_15(i^#()) , 15: activate^#(n__o()) -> c_16(o^#()) , 16: activate^#(n__u()) -> c_17(u^#()) , 17: isList^#(V) -> c_18(isNeList^#(activate(V))) , 18: isList^#(X) -> c_19(X) , 19: isList^#(n____(V1, V2)) -> c_21(and^#(isList(activate(V1)), n__isList(activate(V2)))) , 20: isNeList^#(V) -> c_22(isQid^#(activate(V))) , 21: isNeList^#(X) -> c_23(X) , 22: isNeList^#(n____(V1, V2)) -> c_24(and^#(isList(activate(V1)), n__isNeList(activate(V2)))) , 23: isNeList^#(n____(V1, V2)) -> c_25(and^#(isNeList(activate(V1)), n__isList(activate(V2)))) , 24: isPal^#(V) -> c_33(isNePal^#(activate(V))) , 25: isPal^#(X) -> c_34(X) , 26: isNePal^#(V) -> c_31(isQid^#(activate(V))) , 27: isNePal^#(n____(I, n____(P, I))) -> c_32(and^#(isQid(activate(I)), n__isPal(activate(P)))) , 28: nil^#() -> c_5() , 29: isList^#(n__nil()) -> c_20() , 30: isPal^#(n__nil()) -> c_35() , 31: a^#() -> c_36() , 32: e^#() -> c_37() , 33: i^#() -> c_38() , 34: o^#() -> c_39() , 35: u^#() -> c_40() , 36: isQid^#(n__a()) -> c_26() , 37: isQid^#(n__e()) -> c_27() , 38: isQid^#(n__i()) -> c_28() , 39: isQid^#(n__o()) -> c_29() , 40: isQid^#(n__u()) -> c_30() } 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) , and^#(tt(), X) -> c_6(activate^#(X)) , activate^#(X) -> c_7(X) , activate^#(n____(X1, X2)) -> c_9(__^#(activate(X1), activate(X2))) , activate^#(n__isList(X)) -> c_10(isList^#(X)) , activate^#(n__isNeList(X)) -> c_11(isNeList^#(X)) , activate^#(n__isPal(X)) -> c_12(isPal^#(X)) , isList^#(V) -> c_18(isNeList^#(activate(V))) , isList^#(X) -> c_19(X) , isList^#(n____(V1, V2)) -> c_21(and^#(isList(activate(V1)), n__isList(activate(V2)))) , isNeList^#(X) -> c_23(X) , isNeList^#(n____(V1, V2)) -> c_24(and^#(isList(activate(V1)), n__isNeList(activate(V2)))) , isNeList^#(n____(V1, V2)) -> c_25(and^#(isNeList(activate(V1)), n__isList(activate(V2)))) , isPal^#(V) -> c_33(isNePal^#(activate(V))) , isPal^#(X) -> c_34(X) , isNePal^#(n____(I, n____(P, I))) -> c_32(and^#(isQid(activate(I)), n__isPal(activate(P)))) } Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__isList(X)) -> isList(X) , activate(n__isNeList(X)) -> isNeList(X) , 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() , isList(V) -> isNeList(activate(V)) , isList(X) -> n__isList(X) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))) , isNeList(V) -> isQid(activate(V)) , isNeList(X) -> n__isNeList(X) , isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))) , isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))) , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> isQid(activate(V)) , isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))) , isPal(V) -> isNePal(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() , activate^#(n__nil()) -> c_8(nil^#()) , activate^#(n__a()) -> c_13(a^#()) , activate^#(n__e()) -> c_14(e^#()) , activate^#(n__i()) -> c_15(i^#()) , activate^#(n__o()) -> c_16(o^#()) , activate^#(n__u()) -> c_17(u^#()) , isList^#(n__nil()) -> c_20() , isNeList^#(V) -> c_22(isQid^#(activate(V))) , isPal^#(n__nil()) -> c_35() , a^#() -> c_36() , e^#() -> c_37() , i^#() -> c_38() , o^#() -> c_39() , u^#() -> c_40() , isQid^#(n__a()) -> c_26() , isQid^#(n__e()) -> c_27() , isQid^#(n__i()) -> c_28() , isQid^#(n__o()) -> c_29() , isQid^#(n__u()) -> c_30() , isNePal^#(V) -> c_31(isQid^#(activate(V))) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..