MAYBE 814.88/297.06 MAYBE 814.88/297.06 814.88/297.06 We are left with following problem, upon which TcT provides the 814.88/297.06 certificate MAYBE. 814.88/297.06 814.88/297.06 Strict Trs: 814.88/297.06 { __(X1, X2) -> n____(X1, X2) 814.88/297.06 , __(X, nil()) -> X 814.88/297.06 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 814.88/297.06 , __(nil(), X) -> X 814.88/297.06 , nil() -> n__nil() 814.88/297.06 , U11(tt()) -> tt() 814.88/297.06 , U21(tt(), V2) -> U22(isList(activate(V2))) 814.88/297.06 , U22(tt()) -> tt() 814.88/297.06 , isList(V) -> U11(isNeList(activate(V))) 814.88/297.06 , isList(n__nil()) -> tt() 814.88/297.06 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 814.88/297.06 , activate(X) -> X 814.88/297.06 , activate(n__nil()) -> nil() 814.88/297.06 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 814.88/297.06 , activate(n__a()) -> a() 814.88/297.06 , activate(n__e()) -> e() 814.88/297.06 , activate(n__i()) -> i() 814.88/297.06 , activate(n__o()) -> o() 814.88/297.06 , activate(n__u()) -> u() 814.88/297.06 , U31(tt()) -> tt() 814.88/297.06 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 814.88/297.06 , U42(tt()) -> tt() 814.88/297.06 , isNeList(V) -> U31(isQid(activate(V))) 814.88/297.06 , isNeList(n____(V1, V2)) -> 814.88/297.06 U41(isList(activate(V1)), activate(V2)) 814.88/297.06 , isNeList(n____(V1, V2)) -> 814.88/297.06 U51(isNeList(activate(V1)), activate(V2)) 814.88/297.06 , U51(tt(), V2) -> U52(isList(activate(V2))) 814.88/297.06 , U52(tt()) -> tt() 814.88/297.06 , U61(tt()) -> tt() 814.88/297.06 , U71(tt(), P) -> U72(isPal(activate(P))) 814.88/297.06 , U72(tt()) -> tt() 814.88/297.06 , isPal(V) -> U81(isNePal(activate(V))) 814.88/297.06 , isPal(n__nil()) -> tt() 814.88/297.06 , U81(tt()) -> tt() 814.88/297.06 , isQid(n__a()) -> tt() 814.88/297.06 , isQid(n__e()) -> tt() 814.88/297.06 , isQid(n__i()) -> tt() 814.88/297.06 , isQid(n__o()) -> tt() 814.88/297.06 , isQid(n__u()) -> tt() 814.88/297.06 , isNePal(V) -> U61(isQid(activate(V))) 814.88/297.06 , isNePal(n____(I, n____(P, I))) -> 814.88/297.06 U71(isQid(activate(I)), activate(P)) 814.88/297.06 , a() -> n__a() 814.88/297.06 , e() -> n__e() 814.88/297.06 , i() -> n__i() 814.88/297.06 , o() -> n__o() 814.88/297.06 , u() -> n__u() } 814.88/297.06 Obligation: 814.88/297.06 runtime complexity 814.88/297.06 Answer: 814.88/297.06 MAYBE 814.88/297.06 814.88/297.06 None of the processors succeeded. 814.88/297.06 814.88/297.06 Details of failed attempt(s): 814.88/297.06 ----------------------------- 814.88/297.06 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 814.88/297.06 following reason: 814.88/297.06 814.88/297.06 Computation stopped due to timeout after 297.0 seconds. 814.88/297.06 814.88/297.06 2) 'Best' failed due to the following reason: 814.88/297.06 814.88/297.06 None of the processors succeeded. 814.88/297.06 814.88/297.06 Details of failed attempt(s): 814.88/297.06 ----------------------------- 814.88/297.06 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 814.88/297.06 seconds)' failed due to the following reason: 814.88/297.06 814.88/297.06 Computation stopped due to timeout after 148.0 seconds. 814.88/297.06 814.88/297.06 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 814.88/297.06 failed due to the following reason: 814.88/297.06 814.88/297.06 Computation stopped due to timeout after 24.0 seconds. 814.88/297.06 814.88/297.06 3) 'Best' failed due to the following reason: 814.88/297.06 814.88/297.06 None of the processors succeeded. 814.88/297.06 814.88/297.06 Details of failed attempt(s): 814.88/297.06 ----------------------------- 814.88/297.06 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 814.88/297.06 following reason: 814.88/297.06 814.88/297.06 The processor is inapplicable, reason: 814.88/297.06 Processor only applicable for innermost runtime complexity analysis 814.88/297.06 814.88/297.06 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 814.88/297.06 to the following reason: 814.88/297.06 814.88/297.06 The processor is inapplicable, reason: 814.88/297.06 Processor only applicable for innermost runtime complexity analysis 814.88/297.06 814.88/297.06 814.88/297.06 814.88/297.06 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 814.88/297.06 the following reason: 814.88/297.06 814.88/297.06 We add the following weak dependency pairs: 814.88/297.06 814.88/297.06 Strict DPs: 814.88/297.06 { __^#(X1, X2) -> c_1(X1, X2) 814.88/297.06 , __^#(X, nil()) -> c_2(X) 814.88/297.06 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 814.88/297.06 , __^#(nil(), X) -> c_4(X) 814.88/297.06 , nil^#() -> c_5() 814.88/297.06 , U11^#(tt()) -> c_6() 814.88/297.06 , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) 814.88/297.06 , U22^#(tt()) -> c_8() 814.88/297.06 , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) 814.88/297.06 , isList^#(n__nil()) -> c_10() 814.88/297.06 , isList^#(n____(V1, V2)) -> 814.88/297.06 c_11(U21^#(isList(activate(V1)), activate(V2))) 814.88/297.06 , activate^#(X) -> c_12(X) 814.88/297.06 , activate^#(n__nil()) -> c_13(nil^#()) 814.88/297.06 , activate^#(n____(X1, X2)) -> 814.88/297.06 c_14(__^#(activate(X1), activate(X2))) 814.88/297.06 , activate^#(n__a()) -> c_15(a^#()) 814.88/297.06 , activate^#(n__e()) -> c_16(e^#()) 814.88/297.06 , activate^#(n__i()) -> c_17(i^#()) 814.88/297.06 , activate^#(n__o()) -> c_18(o^#()) 814.88/297.06 , activate^#(n__u()) -> c_19(u^#()) 814.88/297.07 , a^#() -> c_41() 814.88/297.07 , e^#() -> c_42() 814.88/297.07 , i^#() -> c_43() 814.88/297.07 , o^#() -> c_44() 814.88/297.07 , u^#() -> c_45() 814.88/297.07 , U31^#(tt()) -> c_20() 814.88/297.07 , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) 814.88/297.07 , U42^#(tt()) -> c_22() 814.88/297.07 , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_24(U41^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_25(U51^#(isNeList(activate(V1)), activate(V2))) 814.88/297.07 , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) 814.88/297.07 , U52^#(tt()) -> c_27() 814.88/297.07 , U61^#(tt()) -> c_28() 814.88/297.07 , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) 814.88/297.07 , U72^#(tt()) -> c_30() 814.88/297.07 , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) 814.88/297.07 , isPal^#(n__nil()) -> c_32() 814.88/297.07 , U81^#(tt()) -> c_33() 814.88/297.07 , isQid^#(n__a()) -> c_34() 814.88/297.07 , isQid^#(n__e()) -> c_35() 814.88/297.07 , isQid^#(n__i()) -> c_36() 814.88/297.07 , isQid^#(n__o()) -> c_37() 814.88/297.07 , isQid^#(n__u()) -> c_38() 814.88/297.07 , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) 814.88/297.07 , isNePal^#(n____(I, n____(P, I))) -> 814.88/297.07 c_40(U71^#(isQid(activate(I)), activate(P))) } 814.88/297.07 814.88/297.07 and mark the set of starting terms. 814.88/297.07 814.88/297.07 We are left with following problem, upon which TcT provides the 814.88/297.07 certificate MAYBE. 814.88/297.07 814.88/297.07 Strict DPs: 814.88/297.07 { __^#(X1, X2) -> c_1(X1, X2) 814.88/297.07 , __^#(X, nil()) -> c_2(X) 814.88/297.07 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 814.88/297.07 , __^#(nil(), X) -> c_4(X) 814.88/297.07 , nil^#() -> c_5() 814.88/297.07 , U11^#(tt()) -> c_6() 814.88/297.07 , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) 814.88/297.07 , U22^#(tt()) -> c_8() 814.88/297.07 , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) 814.88/297.07 , isList^#(n__nil()) -> c_10() 814.88/297.07 , isList^#(n____(V1, V2)) -> 814.88/297.07 c_11(U21^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , activate^#(X) -> c_12(X) 814.88/297.07 , activate^#(n__nil()) -> c_13(nil^#()) 814.88/297.07 , activate^#(n____(X1, X2)) -> 814.88/297.07 c_14(__^#(activate(X1), activate(X2))) 814.88/297.07 , activate^#(n__a()) -> c_15(a^#()) 814.88/297.07 , activate^#(n__e()) -> c_16(e^#()) 814.88/297.07 , activate^#(n__i()) -> c_17(i^#()) 814.88/297.07 , activate^#(n__o()) -> c_18(o^#()) 814.88/297.07 , activate^#(n__u()) -> c_19(u^#()) 814.88/297.07 , a^#() -> c_41() 814.88/297.07 , e^#() -> c_42() 814.88/297.07 , i^#() -> c_43() 814.88/297.07 , o^#() -> c_44() 814.88/297.07 , u^#() -> c_45() 814.88/297.07 , U31^#(tt()) -> c_20() 814.88/297.07 , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) 814.88/297.07 , U42^#(tt()) -> c_22() 814.88/297.07 , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_24(U41^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_25(U51^#(isNeList(activate(V1)), activate(V2))) 814.88/297.07 , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) 814.88/297.07 , U52^#(tt()) -> c_27() 814.88/297.07 , U61^#(tt()) -> c_28() 814.88/297.07 , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) 814.88/297.07 , U72^#(tt()) -> c_30() 814.88/297.07 , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) 814.88/297.07 , isPal^#(n__nil()) -> c_32() 814.88/297.07 , U81^#(tt()) -> c_33() 814.88/297.07 , isQid^#(n__a()) -> c_34() 814.88/297.07 , isQid^#(n__e()) -> c_35() 814.88/297.07 , isQid^#(n__i()) -> c_36() 814.88/297.07 , isQid^#(n__o()) -> c_37() 814.88/297.07 , isQid^#(n__u()) -> c_38() 814.88/297.07 , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) 814.88/297.07 , isNePal^#(n____(I, n____(P, I))) -> 814.88/297.07 c_40(U71^#(isQid(activate(I)), activate(P))) } 814.88/297.07 Strict Trs: 814.88/297.07 { __(X1, X2) -> n____(X1, X2) 814.88/297.07 , __(X, nil()) -> X 814.88/297.07 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 814.88/297.07 , __(nil(), X) -> X 814.88/297.07 , nil() -> n__nil() 814.88/297.07 , U11(tt()) -> tt() 814.88/297.07 , U21(tt(), V2) -> U22(isList(activate(V2))) 814.88/297.07 , U22(tt()) -> tt() 814.88/297.07 , isList(V) -> U11(isNeList(activate(V))) 814.88/297.07 , isList(n__nil()) -> tt() 814.88/297.07 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 814.88/297.07 , activate(X) -> X 814.88/297.07 , activate(n__nil()) -> nil() 814.88/297.07 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 814.88/297.07 , activate(n__a()) -> a() 814.88/297.07 , activate(n__e()) -> e() 814.88/297.07 , activate(n__i()) -> i() 814.88/297.07 , activate(n__o()) -> o() 814.88/297.07 , activate(n__u()) -> u() 814.88/297.07 , U31(tt()) -> tt() 814.88/297.07 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 814.88/297.07 , U42(tt()) -> tt() 814.88/297.07 , isNeList(V) -> U31(isQid(activate(V))) 814.88/297.07 , isNeList(n____(V1, V2)) -> 814.88/297.07 U41(isList(activate(V1)), activate(V2)) 814.88/297.07 , isNeList(n____(V1, V2)) -> 814.88/297.07 U51(isNeList(activate(V1)), activate(V2)) 814.88/297.07 , U51(tt(), V2) -> U52(isList(activate(V2))) 814.88/297.07 , U52(tt()) -> tt() 814.88/297.07 , U61(tt()) -> tt() 814.88/297.07 , U71(tt(), P) -> U72(isPal(activate(P))) 814.88/297.07 , U72(tt()) -> tt() 814.88/297.07 , isPal(V) -> U81(isNePal(activate(V))) 814.88/297.07 , isPal(n__nil()) -> tt() 814.88/297.07 , U81(tt()) -> tt() 814.88/297.07 , isQid(n__a()) -> tt() 814.88/297.07 , isQid(n__e()) -> tt() 814.88/297.07 , isQid(n__i()) -> tt() 814.88/297.07 , isQid(n__o()) -> tt() 814.88/297.07 , isQid(n__u()) -> tt() 814.88/297.07 , isNePal(V) -> U61(isQid(activate(V))) 814.88/297.07 , isNePal(n____(I, n____(P, I))) -> 814.88/297.07 U71(isQid(activate(I)), activate(P)) 814.88/297.07 , a() -> n__a() 814.88/297.07 , e() -> n__e() 814.88/297.07 , i() -> n__i() 814.88/297.07 , o() -> n__o() 814.88/297.07 , u() -> n__u() } 814.88/297.07 Obligation: 814.88/297.07 runtime complexity 814.88/297.07 Answer: 814.88/297.07 MAYBE 814.88/297.07 814.88/297.07 We estimate the number of application of 814.88/297.07 {5,6,8,10,20,21,22,23,24,25,27,32,33,35,37,38,39,40,41,42,43} by 814.88/297.07 applications of 814.88/297.07 Pre({5,6,8,10,20,21,22,23,24,25,27,32,33,35,37,38,39,40,41,42,43}) 814.88/297.07 = {1,2,4,7,9,12,13,15,16,17,18,19,26,28,31,34,36,44}. Here rules 814.88/297.07 are labeled as follows: 814.88/297.07 814.88/297.07 DPs: 814.88/297.07 { 1: __^#(X1, X2) -> c_1(X1, X2) 814.88/297.07 , 2: __^#(X, nil()) -> c_2(X) 814.88/297.07 , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 814.88/297.07 , 4: __^#(nil(), X) -> c_4(X) 814.88/297.07 , 5: nil^#() -> c_5() 814.88/297.07 , 6: U11^#(tt()) -> c_6() 814.88/297.07 , 7: U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) 814.88/297.07 , 8: U22^#(tt()) -> c_8() 814.88/297.07 , 9: isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) 814.88/297.07 , 10: isList^#(n__nil()) -> c_10() 814.88/297.07 , 11: isList^#(n____(V1, V2)) -> 814.88/297.07 c_11(U21^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , 12: activate^#(X) -> c_12(X) 814.88/297.07 , 13: activate^#(n__nil()) -> c_13(nil^#()) 814.88/297.07 , 14: activate^#(n____(X1, X2)) -> 814.88/297.07 c_14(__^#(activate(X1), activate(X2))) 814.88/297.07 , 15: activate^#(n__a()) -> c_15(a^#()) 814.88/297.07 , 16: activate^#(n__e()) -> c_16(e^#()) 814.88/297.07 , 17: activate^#(n__i()) -> c_17(i^#()) 814.88/297.07 , 18: activate^#(n__o()) -> c_18(o^#()) 814.88/297.07 , 19: activate^#(n__u()) -> c_19(u^#()) 814.88/297.07 , 20: a^#() -> c_41() 814.88/297.07 , 21: e^#() -> c_42() 814.88/297.07 , 22: i^#() -> c_43() 814.88/297.07 , 23: o^#() -> c_44() 814.88/297.07 , 24: u^#() -> c_45() 814.88/297.07 , 25: U31^#(tt()) -> c_20() 814.88/297.07 , 26: U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) 814.88/297.07 , 27: U42^#(tt()) -> c_22() 814.88/297.07 , 28: isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) 814.88/297.07 , 29: isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_24(U41^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , 30: isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_25(U51^#(isNeList(activate(V1)), activate(V2))) 814.88/297.07 , 31: U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) 814.88/297.07 , 32: U52^#(tt()) -> c_27() 814.88/297.07 , 33: U61^#(tt()) -> c_28() 814.88/297.07 , 34: U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) 814.88/297.07 , 35: U72^#(tt()) -> c_30() 814.88/297.07 , 36: isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) 814.88/297.07 , 37: isPal^#(n__nil()) -> c_32() 814.88/297.07 , 38: U81^#(tt()) -> c_33() 814.88/297.07 , 39: isQid^#(n__a()) -> c_34() 814.88/297.07 , 40: isQid^#(n__e()) -> c_35() 814.88/297.07 , 41: isQid^#(n__i()) -> c_36() 814.88/297.07 , 42: isQid^#(n__o()) -> c_37() 814.88/297.07 , 43: isQid^#(n__u()) -> c_38() 814.88/297.07 , 44: isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) 814.88/297.07 , 45: isNePal^#(n____(I, n____(P, I))) -> 814.88/297.07 c_40(U71^#(isQid(activate(I)), activate(P))) } 814.88/297.07 814.88/297.07 We are left with following problem, upon which TcT provides the 814.88/297.07 certificate MAYBE. 814.88/297.07 814.88/297.07 Strict DPs: 814.88/297.07 { __^#(X1, X2) -> c_1(X1, X2) 814.88/297.07 , __^#(X, nil()) -> c_2(X) 814.88/297.07 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 814.88/297.07 , __^#(nil(), X) -> c_4(X) 814.88/297.07 , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) 814.88/297.07 , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) 814.88/297.07 , isList^#(n____(V1, V2)) -> 814.88/297.07 c_11(U21^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , activate^#(X) -> c_12(X) 814.88/297.07 , activate^#(n__nil()) -> c_13(nil^#()) 814.88/297.07 , activate^#(n____(X1, X2)) -> 814.88/297.07 c_14(__^#(activate(X1), activate(X2))) 814.88/297.07 , activate^#(n__a()) -> c_15(a^#()) 814.88/297.07 , activate^#(n__e()) -> c_16(e^#()) 814.88/297.07 , activate^#(n__i()) -> c_17(i^#()) 814.88/297.07 , activate^#(n__o()) -> c_18(o^#()) 814.88/297.07 , activate^#(n__u()) -> c_19(u^#()) 814.88/297.07 , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) 814.88/297.07 , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_24(U41^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_25(U51^#(isNeList(activate(V1)), activate(V2))) 814.88/297.07 , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) 814.88/297.07 , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) 814.88/297.07 , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) 814.88/297.07 , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) 814.88/297.07 , isNePal^#(n____(I, n____(P, I))) -> 814.88/297.07 c_40(U71^#(isQid(activate(I)), activate(P))) } 814.88/297.07 Strict Trs: 814.88/297.07 { __(X1, X2) -> n____(X1, X2) 814.88/297.07 , __(X, nil()) -> X 814.88/297.07 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 814.88/297.07 , __(nil(), X) -> X 814.88/297.07 , nil() -> n__nil() 814.88/297.07 , U11(tt()) -> tt() 814.88/297.07 , U21(tt(), V2) -> U22(isList(activate(V2))) 814.88/297.07 , U22(tt()) -> tt() 814.88/297.07 , isList(V) -> U11(isNeList(activate(V))) 814.88/297.07 , isList(n__nil()) -> tt() 814.88/297.07 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 814.88/297.07 , activate(X) -> X 814.88/297.07 , activate(n__nil()) -> nil() 814.88/297.07 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 814.88/297.07 , activate(n__a()) -> a() 814.88/297.07 , activate(n__e()) -> e() 814.88/297.07 , activate(n__i()) -> i() 814.88/297.07 , activate(n__o()) -> o() 814.88/297.07 , activate(n__u()) -> u() 814.88/297.07 , U31(tt()) -> tt() 814.88/297.07 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 814.88/297.07 , U42(tt()) -> tt() 814.88/297.07 , isNeList(V) -> U31(isQid(activate(V))) 814.88/297.07 , isNeList(n____(V1, V2)) -> 814.88/297.07 U41(isList(activate(V1)), activate(V2)) 814.88/297.07 , isNeList(n____(V1, V2)) -> 814.88/297.07 U51(isNeList(activate(V1)), activate(V2)) 814.88/297.07 , U51(tt(), V2) -> U52(isList(activate(V2))) 814.88/297.07 , U52(tt()) -> tt() 814.88/297.07 , U61(tt()) -> tt() 814.88/297.07 , U71(tt(), P) -> U72(isPal(activate(P))) 814.88/297.07 , U72(tt()) -> tt() 814.88/297.07 , isPal(V) -> U81(isNePal(activate(V))) 814.88/297.07 , isPal(n__nil()) -> tt() 814.88/297.07 , U81(tt()) -> tt() 814.88/297.07 , isQid(n__a()) -> tt() 814.88/297.07 , isQid(n__e()) -> tt() 814.88/297.07 , isQid(n__i()) -> tt() 814.88/297.07 , isQid(n__o()) -> tt() 814.88/297.07 , isQid(n__u()) -> tt() 814.88/297.07 , isNePal(V) -> U61(isQid(activate(V))) 814.88/297.07 , isNePal(n____(I, n____(P, I))) -> 814.88/297.07 U71(isQid(activate(I)), activate(P)) 814.88/297.07 , a() -> n__a() 814.88/297.07 , e() -> n__e() 814.88/297.07 , i() -> n__i() 814.88/297.07 , o() -> n__o() 814.88/297.07 , u() -> n__u() } 814.88/297.07 Weak DPs: 814.88/297.07 { nil^#() -> c_5() 814.88/297.07 , U11^#(tt()) -> c_6() 814.88/297.07 , U22^#(tt()) -> c_8() 814.88/297.07 , isList^#(n__nil()) -> c_10() 814.88/297.07 , a^#() -> c_41() 814.88/297.07 , e^#() -> c_42() 814.88/297.07 , i^#() -> c_43() 814.88/297.07 , o^#() -> c_44() 814.88/297.07 , u^#() -> c_45() 814.88/297.07 , U31^#(tt()) -> c_20() 814.88/297.07 , U42^#(tt()) -> c_22() 814.88/297.07 , U52^#(tt()) -> c_27() 814.88/297.07 , U61^#(tt()) -> c_28() 814.88/297.07 , U72^#(tt()) -> c_30() 814.88/297.07 , isPal^#(n__nil()) -> c_32() 814.88/297.07 , U81^#(tt()) -> c_33() 814.88/297.07 , isQid^#(n__a()) -> c_34() 814.88/297.07 , isQid^#(n__e()) -> c_35() 814.88/297.07 , isQid^#(n__i()) -> c_36() 814.88/297.07 , isQid^#(n__o()) -> c_37() 814.88/297.07 , isQid^#(n__u()) -> c_38() } 814.88/297.07 Obligation: 814.88/297.07 runtime complexity 814.88/297.07 Answer: 814.88/297.07 MAYBE 814.88/297.07 814.88/297.07 We estimate the number of application of 814.88/297.07 {5,6,9,11,12,13,14,15,16,17,20,21,22,23} by applications of 814.88/297.07 Pre({5,6,9,11,12,13,14,15,16,17,20,21,22,23}) = 814.88/297.07 {1,2,4,7,8,18,19,24}. Here rules are labeled as follows: 814.88/297.07 814.88/297.07 DPs: 814.88/297.07 { 1: __^#(X1, X2) -> c_1(X1, X2) 814.88/297.07 , 2: __^#(X, nil()) -> c_2(X) 814.88/297.07 , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 814.88/297.07 , 4: __^#(nil(), X) -> c_4(X) 814.88/297.07 , 5: U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) 814.88/297.07 , 6: isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) 814.88/297.07 , 7: isList^#(n____(V1, V2)) -> 814.88/297.07 c_11(U21^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , 8: activate^#(X) -> c_12(X) 814.88/297.07 , 9: activate^#(n__nil()) -> c_13(nil^#()) 814.88/297.07 , 10: activate^#(n____(X1, X2)) -> 814.88/297.07 c_14(__^#(activate(X1), activate(X2))) 814.88/297.07 , 11: activate^#(n__a()) -> c_15(a^#()) 814.88/297.07 , 12: activate^#(n__e()) -> c_16(e^#()) 814.88/297.07 , 13: activate^#(n__i()) -> c_17(i^#()) 814.88/297.07 , 14: activate^#(n__o()) -> c_18(o^#()) 814.88/297.07 , 15: activate^#(n__u()) -> c_19(u^#()) 814.88/297.07 , 16: U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) 814.88/297.07 , 17: isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) 814.88/297.07 , 18: isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_24(U41^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , 19: isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_25(U51^#(isNeList(activate(V1)), activate(V2))) 814.88/297.07 , 20: U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) 814.88/297.07 , 21: U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) 814.88/297.07 , 22: isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) 814.88/297.07 , 23: isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) 814.88/297.07 , 24: isNePal^#(n____(I, n____(P, I))) -> 814.88/297.07 c_40(U71^#(isQid(activate(I)), activate(P))) 814.88/297.07 , 25: nil^#() -> c_5() 814.88/297.07 , 26: U11^#(tt()) -> c_6() 814.88/297.07 , 27: U22^#(tt()) -> c_8() 814.88/297.07 , 28: isList^#(n__nil()) -> c_10() 814.88/297.07 , 29: a^#() -> c_41() 814.88/297.07 , 30: e^#() -> c_42() 814.88/297.07 , 31: i^#() -> c_43() 814.88/297.07 , 32: o^#() -> c_44() 814.88/297.07 , 33: u^#() -> c_45() 814.88/297.07 , 34: U31^#(tt()) -> c_20() 814.88/297.07 , 35: U42^#(tt()) -> c_22() 814.88/297.07 , 36: U52^#(tt()) -> c_27() 814.88/297.07 , 37: U61^#(tt()) -> c_28() 814.88/297.07 , 38: U72^#(tt()) -> c_30() 814.88/297.07 , 39: isPal^#(n__nil()) -> c_32() 814.88/297.07 , 40: U81^#(tt()) -> c_33() 814.88/297.07 , 41: isQid^#(n__a()) -> c_34() 814.88/297.07 , 42: isQid^#(n__e()) -> c_35() 814.88/297.07 , 43: isQid^#(n__i()) -> c_36() 814.88/297.07 , 44: isQid^#(n__o()) -> c_37() 814.88/297.07 , 45: isQid^#(n__u()) -> c_38() } 814.88/297.07 814.88/297.07 We are left with following problem, upon which TcT provides the 814.88/297.07 certificate MAYBE. 814.88/297.07 814.88/297.07 Strict DPs: 814.88/297.07 { __^#(X1, X2) -> c_1(X1, X2) 814.88/297.07 , __^#(X, nil()) -> c_2(X) 814.88/297.07 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 814.88/297.07 , __^#(nil(), X) -> c_4(X) 814.88/297.07 , isList^#(n____(V1, V2)) -> 814.88/297.07 c_11(U21^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , activate^#(X) -> c_12(X) 814.88/297.07 , activate^#(n____(X1, X2)) -> 814.88/297.07 c_14(__^#(activate(X1), activate(X2))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_24(U41^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_25(U51^#(isNeList(activate(V1)), activate(V2))) 814.88/297.07 , isNePal^#(n____(I, n____(P, I))) -> 814.88/297.07 c_40(U71^#(isQid(activate(I)), activate(P))) } 814.88/297.07 Strict Trs: 814.88/297.07 { __(X1, X2) -> n____(X1, X2) 814.88/297.07 , __(X, nil()) -> X 814.88/297.07 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 814.88/297.07 , __(nil(), X) -> X 814.88/297.07 , nil() -> n__nil() 814.88/297.07 , U11(tt()) -> tt() 814.88/297.07 , U21(tt(), V2) -> U22(isList(activate(V2))) 814.88/297.07 , U22(tt()) -> tt() 814.88/297.07 , isList(V) -> U11(isNeList(activate(V))) 814.88/297.07 , isList(n__nil()) -> tt() 814.88/297.07 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 814.88/297.07 , activate(X) -> X 814.88/297.07 , activate(n__nil()) -> nil() 814.88/297.07 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 814.88/297.07 , activate(n__a()) -> a() 814.88/297.07 , activate(n__e()) -> e() 814.88/297.07 , activate(n__i()) -> i() 814.88/297.07 , activate(n__o()) -> o() 814.88/297.07 , activate(n__u()) -> u() 814.88/297.07 , U31(tt()) -> tt() 814.88/297.07 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 814.88/297.07 , U42(tt()) -> tt() 814.88/297.07 , isNeList(V) -> U31(isQid(activate(V))) 814.88/297.07 , isNeList(n____(V1, V2)) -> 814.88/297.07 U41(isList(activate(V1)), activate(V2)) 814.88/297.07 , isNeList(n____(V1, V2)) -> 814.88/297.07 U51(isNeList(activate(V1)), activate(V2)) 814.88/297.07 , U51(tt(), V2) -> U52(isList(activate(V2))) 814.88/297.07 , U52(tt()) -> tt() 814.88/297.07 , U61(tt()) -> tt() 814.88/297.07 , U71(tt(), P) -> U72(isPal(activate(P))) 814.88/297.07 , U72(tt()) -> tt() 814.88/297.07 , isPal(V) -> U81(isNePal(activate(V))) 814.88/297.07 , isPal(n__nil()) -> tt() 814.88/297.07 , U81(tt()) -> tt() 814.88/297.07 , isQid(n__a()) -> tt() 814.88/297.07 , isQid(n__e()) -> tt() 814.88/297.07 , isQid(n__i()) -> tt() 814.88/297.07 , isQid(n__o()) -> tt() 814.88/297.07 , isQid(n__u()) -> tt() 814.88/297.07 , isNePal(V) -> U61(isQid(activate(V))) 814.88/297.07 , isNePal(n____(I, n____(P, I))) -> 814.88/297.07 U71(isQid(activate(I)), activate(P)) 814.88/297.07 , a() -> n__a() 814.88/297.07 , e() -> n__e() 814.88/297.07 , i() -> n__i() 814.88/297.07 , o() -> n__o() 814.88/297.07 , u() -> n__u() } 814.88/297.07 Weak DPs: 814.88/297.07 { nil^#() -> c_5() 814.88/297.07 , U11^#(tt()) -> c_6() 814.88/297.07 , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) 814.88/297.07 , U22^#(tt()) -> c_8() 814.88/297.07 , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) 814.88/297.07 , isList^#(n__nil()) -> c_10() 814.88/297.07 , activate^#(n__nil()) -> c_13(nil^#()) 814.88/297.07 , activate^#(n__a()) -> c_15(a^#()) 814.88/297.07 , activate^#(n__e()) -> c_16(e^#()) 814.88/297.07 , activate^#(n__i()) -> c_17(i^#()) 814.88/297.07 , activate^#(n__o()) -> c_18(o^#()) 814.88/297.07 , activate^#(n__u()) -> c_19(u^#()) 814.88/297.07 , a^#() -> c_41() 814.88/297.07 , e^#() -> c_42() 814.88/297.07 , i^#() -> c_43() 814.88/297.07 , o^#() -> c_44() 814.88/297.07 , u^#() -> c_45() 814.88/297.07 , U31^#(tt()) -> c_20() 814.88/297.07 , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) 814.88/297.07 , U42^#(tt()) -> c_22() 814.88/297.07 , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) 814.88/297.07 , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) 814.88/297.07 , U52^#(tt()) -> c_27() 814.88/297.07 , U61^#(tt()) -> c_28() 814.88/297.07 , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) 814.88/297.07 , U72^#(tt()) -> c_30() 814.88/297.07 , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) 814.88/297.07 , isPal^#(n__nil()) -> c_32() 814.88/297.07 , U81^#(tt()) -> c_33() 814.88/297.07 , isQid^#(n__a()) -> c_34() 814.88/297.07 , isQid^#(n__e()) -> c_35() 814.88/297.07 , isQid^#(n__i()) -> c_36() 814.88/297.07 , isQid^#(n__o()) -> c_37() 814.88/297.07 , isQid^#(n__u()) -> c_38() 814.88/297.07 , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) } 814.88/297.07 Obligation: 814.88/297.07 runtime complexity 814.88/297.07 Answer: 814.88/297.07 MAYBE 814.88/297.07 814.88/297.07 We estimate the number of application of {5,8,9,10} by applications 814.88/297.07 of Pre({5,8,9,10}) = {1,2,4,6}. Here rules are labeled as follows: 814.88/297.07 814.88/297.07 DPs: 814.88/297.07 { 1: __^#(X1, X2) -> c_1(X1, X2) 814.88/297.07 , 2: __^#(X, nil()) -> c_2(X) 814.88/297.07 , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 814.88/297.07 , 4: __^#(nil(), X) -> c_4(X) 814.88/297.07 , 5: isList^#(n____(V1, V2)) -> 814.88/297.07 c_11(U21^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , 6: activate^#(X) -> c_12(X) 814.88/297.07 , 7: activate^#(n____(X1, X2)) -> 814.88/297.07 c_14(__^#(activate(X1), activate(X2))) 814.88/297.07 , 8: isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_24(U41^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , 9: isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_25(U51^#(isNeList(activate(V1)), activate(V2))) 814.88/297.07 , 10: isNePal^#(n____(I, n____(P, I))) -> 814.88/297.07 c_40(U71^#(isQid(activate(I)), activate(P))) 814.88/297.07 , 11: nil^#() -> c_5() 814.88/297.07 , 12: U11^#(tt()) -> c_6() 814.88/297.07 , 13: U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) 814.88/297.07 , 14: U22^#(tt()) -> c_8() 814.88/297.07 , 15: isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) 814.88/297.07 , 16: isList^#(n__nil()) -> c_10() 814.88/297.07 , 17: activate^#(n__nil()) -> c_13(nil^#()) 814.88/297.07 , 18: activate^#(n__a()) -> c_15(a^#()) 814.88/297.07 , 19: activate^#(n__e()) -> c_16(e^#()) 814.88/297.07 , 20: activate^#(n__i()) -> c_17(i^#()) 814.88/297.07 , 21: activate^#(n__o()) -> c_18(o^#()) 814.88/297.07 , 22: activate^#(n__u()) -> c_19(u^#()) 814.88/297.07 , 23: a^#() -> c_41() 814.88/297.07 , 24: e^#() -> c_42() 814.88/297.07 , 25: i^#() -> c_43() 814.88/297.07 , 26: o^#() -> c_44() 814.88/297.07 , 27: u^#() -> c_45() 814.88/297.07 , 28: U31^#(tt()) -> c_20() 814.88/297.07 , 29: U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) 814.88/297.07 , 30: U42^#(tt()) -> c_22() 814.88/297.07 , 31: isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) 814.88/297.07 , 32: U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) 814.88/297.07 , 33: U52^#(tt()) -> c_27() 814.88/297.07 , 34: U61^#(tt()) -> c_28() 814.88/297.07 , 35: U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) 814.88/297.07 , 36: U72^#(tt()) -> c_30() 814.88/297.07 , 37: isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) 814.88/297.07 , 38: isPal^#(n__nil()) -> c_32() 814.88/297.07 , 39: U81^#(tt()) -> c_33() 814.88/297.07 , 40: isQid^#(n__a()) -> c_34() 814.88/297.07 , 41: isQid^#(n__e()) -> c_35() 814.88/297.07 , 42: isQid^#(n__i()) -> c_36() 814.88/297.07 , 43: isQid^#(n__o()) -> c_37() 814.88/297.07 , 44: isQid^#(n__u()) -> c_38() 814.88/297.07 , 45: isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) } 814.88/297.07 814.88/297.07 We are left with following problem, upon which TcT provides the 814.88/297.07 certificate MAYBE. 814.88/297.07 814.88/297.07 Strict DPs: 814.88/297.07 { __^#(X1, X2) -> c_1(X1, X2) 814.88/297.07 , __^#(X, nil()) -> c_2(X) 814.88/297.07 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 814.88/297.07 , __^#(nil(), X) -> c_4(X) 814.88/297.07 , activate^#(X) -> c_12(X) 814.88/297.07 , activate^#(n____(X1, X2)) -> 814.88/297.07 c_14(__^#(activate(X1), activate(X2))) } 814.88/297.07 Strict Trs: 814.88/297.07 { __(X1, X2) -> n____(X1, X2) 814.88/297.07 , __(X, nil()) -> X 814.88/297.07 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 814.88/297.07 , __(nil(), X) -> X 814.88/297.07 , nil() -> n__nil() 814.88/297.07 , U11(tt()) -> tt() 814.88/297.07 , U21(tt(), V2) -> U22(isList(activate(V2))) 814.88/297.07 , U22(tt()) -> tt() 814.88/297.07 , isList(V) -> U11(isNeList(activate(V))) 814.88/297.07 , isList(n__nil()) -> tt() 814.88/297.07 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 814.88/297.07 , activate(X) -> X 814.88/297.07 , activate(n__nil()) -> nil() 814.88/297.07 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 814.88/297.07 , activate(n__a()) -> a() 814.88/297.07 , activate(n__e()) -> e() 814.88/297.07 , activate(n__i()) -> i() 814.88/297.07 , activate(n__o()) -> o() 814.88/297.07 , activate(n__u()) -> u() 814.88/297.07 , U31(tt()) -> tt() 814.88/297.07 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 814.88/297.07 , U42(tt()) -> tt() 814.88/297.07 , isNeList(V) -> U31(isQid(activate(V))) 814.88/297.07 , isNeList(n____(V1, V2)) -> 814.88/297.07 U41(isList(activate(V1)), activate(V2)) 814.88/297.07 , isNeList(n____(V1, V2)) -> 814.88/297.07 U51(isNeList(activate(V1)), activate(V2)) 814.88/297.07 , U51(tt(), V2) -> U52(isList(activate(V2))) 814.88/297.07 , U52(tt()) -> tt() 814.88/297.07 , U61(tt()) -> tt() 814.88/297.07 , U71(tt(), P) -> U72(isPal(activate(P))) 814.88/297.07 , U72(tt()) -> tt() 814.88/297.07 , isPal(V) -> U81(isNePal(activate(V))) 814.88/297.07 , isPal(n__nil()) -> tt() 814.88/297.07 , U81(tt()) -> tt() 814.88/297.07 , isQid(n__a()) -> tt() 814.88/297.07 , isQid(n__e()) -> tt() 814.88/297.07 , isQid(n__i()) -> tt() 814.88/297.07 , isQid(n__o()) -> tt() 814.88/297.07 , isQid(n__u()) -> tt() 814.88/297.07 , isNePal(V) -> U61(isQid(activate(V))) 814.88/297.07 , isNePal(n____(I, n____(P, I))) -> 814.88/297.07 U71(isQid(activate(I)), activate(P)) 814.88/297.07 , a() -> n__a() 814.88/297.07 , e() -> n__e() 814.88/297.07 , i() -> n__i() 814.88/297.07 , o() -> n__o() 814.88/297.07 , u() -> n__u() } 814.88/297.07 Weak DPs: 814.88/297.07 { nil^#() -> c_5() 814.88/297.07 , U11^#(tt()) -> c_6() 814.88/297.07 , U21^#(tt(), V2) -> c_7(U22^#(isList(activate(V2)))) 814.88/297.07 , U22^#(tt()) -> c_8() 814.88/297.07 , isList^#(V) -> c_9(U11^#(isNeList(activate(V)))) 814.88/297.07 , isList^#(n__nil()) -> c_10() 814.88/297.07 , isList^#(n____(V1, V2)) -> 814.88/297.07 c_11(U21^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , activate^#(n__nil()) -> c_13(nil^#()) 814.88/297.07 , activate^#(n__a()) -> c_15(a^#()) 814.88/297.07 , activate^#(n__e()) -> c_16(e^#()) 814.88/297.07 , activate^#(n__i()) -> c_17(i^#()) 814.88/297.07 , activate^#(n__o()) -> c_18(o^#()) 814.88/297.07 , activate^#(n__u()) -> c_19(u^#()) 814.88/297.07 , a^#() -> c_41() 814.88/297.07 , e^#() -> c_42() 814.88/297.07 , i^#() -> c_43() 814.88/297.07 , o^#() -> c_44() 814.88/297.07 , u^#() -> c_45() 814.88/297.07 , U31^#(tt()) -> c_20() 814.88/297.07 , U41^#(tt(), V2) -> c_21(U42^#(isNeList(activate(V2)))) 814.88/297.07 , U42^#(tt()) -> c_22() 814.88/297.07 , isNeList^#(V) -> c_23(U31^#(isQid(activate(V)))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_24(U41^#(isList(activate(V1)), activate(V2))) 814.88/297.07 , isNeList^#(n____(V1, V2)) -> 814.88/297.07 c_25(U51^#(isNeList(activate(V1)), activate(V2))) 814.88/297.07 , U51^#(tt(), V2) -> c_26(U52^#(isList(activate(V2)))) 814.88/297.07 , U52^#(tt()) -> c_27() 814.88/297.07 , U61^#(tt()) -> c_28() 814.88/297.07 , U71^#(tt(), P) -> c_29(U72^#(isPal(activate(P)))) 814.88/297.07 , U72^#(tt()) -> c_30() 814.88/297.07 , isPal^#(V) -> c_31(U81^#(isNePal(activate(V)))) 814.88/297.07 , isPal^#(n__nil()) -> c_32() 814.88/297.07 , U81^#(tt()) -> c_33() 814.88/297.07 , isQid^#(n__a()) -> c_34() 814.88/297.07 , isQid^#(n__e()) -> c_35() 814.88/297.07 , isQid^#(n__i()) -> c_36() 814.88/297.07 , isQid^#(n__o()) -> c_37() 814.88/297.07 , isQid^#(n__u()) -> c_38() 814.88/297.07 , isNePal^#(V) -> c_39(U61^#(isQid(activate(V)))) 814.88/297.07 , isNePal^#(n____(I, n____(P, I))) -> 814.88/297.07 c_40(U71^#(isQid(activate(I)), activate(P))) } 814.88/297.07 Obligation: 814.88/297.07 runtime complexity 814.88/297.07 Answer: 814.88/297.07 MAYBE 814.88/297.07 814.88/297.07 Empty strict component of the problem is NOT empty. 814.88/297.07 814.88/297.07 814.88/297.07 Arrrr.. 815.23/297.32 EOF