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