MAYBE 896.77/297.14 MAYBE 896.77/297.14 896.77/297.14 We are left with following problem, upon which TcT provides the 896.77/297.14 certificate MAYBE. 896.77/297.14 896.77/297.14 Strict Trs: 896.77/297.14 { __(X1, X2) -> n____(X1, X2) 896.77/297.14 , __(X, nil()) -> X 896.77/297.14 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 896.77/297.14 , __(nil(), X) -> X 896.77/297.14 , nil() -> n__nil() 896.77/297.14 , U11(tt(), V) -> U12(isNeList(activate(V))) 896.77/297.14 , U12(tt()) -> tt() 896.77/297.14 , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isNeList(n____(V1, V2)) -> 896.77/297.14 U41(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2)) 896.77/297.14 , isNeList(n____(V1, V2)) -> 896.77/297.14 U51(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2)) 896.77/297.14 , activate(X) -> X 896.77/297.14 , activate(n__nil()) -> nil() 896.77/297.14 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 896.77/297.14 , activate(n__isPalListKind(X)) -> isPalListKind(X) 896.77/297.14 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 896.77/297.14 , activate(n__isPal(X)) -> isPal(X) 896.77/297.14 , activate(n__a()) -> a() 896.77/297.14 , activate(n__e()) -> e() 896.77/297.14 , activate(n__i()) -> i() 896.77/297.14 , activate(n__o()) -> o() 896.77/297.14 , activate(n__u()) -> u() 896.77/297.14 , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) 896.77/297.14 , U22(tt(), V2) -> U23(isList(activate(V2))) 896.77/297.14 , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isList(n__nil()) -> tt() 896.77/297.14 , isList(n____(V1, V2)) -> 896.77/297.14 U21(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2)) 896.77/297.14 , U23(tt()) -> tt() 896.77/297.14 , U31(tt(), V) -> U32(isQid(activate(V))) 896.77/297.14 , U32(tt()) -> tt() 896.77/297.14 , isQid(n__a()) -> tt() 896.77/297.14 , isQid(n__e()) -> tt() 896.77/297.14 , isQid(n__i()) -> tt() 896.77/297.14 , isQid(n__o()) -> tt() 896.77/297.14 , isQid(n__u()) -> tt() 896.77/297.14 , U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)) 896.77/297.14 , U42(tt(), V2) -> U43(isNeList(activate(V2))) 896.77/297.14 , U43(tt()) -> tt() 896.77/297.14 , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) 896.77/297.14 , U52(tt(), V2) -> U53(isList(activate(V2))) 896.77/297.14 , U53(tt()) -> tt() 896.77/297.14 , U61(tt(), V) -> U62(isQid(activate(V))) 896.77/297.14 , U62(tt()) -> tt() 896.77/297.14 , U71(tt(), V) -> U72(isNePal(activate(V))) 896.77/297.14 , U72(tt()) -> tt() 896.77/297.14 , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isNePal(n____(I, n____(P, I))) -> 896.77/297.14 and(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.14 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) 896.77/297.14 , and(X1, X2) -> n__and(X1, X2) 896.77/297.14 , and(tt(), X) -> activate(X) 896.77/297.14 , isPalListKind(X) -> n__isPalListKind(X) 896.77/297.14 , isPalListKind(n__nil()) -> tt() 896.77/297.14 , isPalListKind(n____(V1, V2)) -> 896.77/297.14 and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) 896.77/297.14 , isPalListKind(n__a()) -> tt() 896.77/297.14 , isPalListKind(n__e()) -> tt() 896.77/297.14 , isPalListKind(n__i()) -> tt() 896.77/297.14 , isPalListKind(n__o()) -> tt() 896.77/297.14 , isPalListKind(n__u()) -> tt() 896.77/297.14 , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isPal(X) -> n__isPal(X) 896.77/297.14 , isPal(n__nil()) -> tt() 896.77/297.14 , a() -> n__a() 896.77/297.14 , e() -> n__e() 896.77/297.14 , i() -> n__i() 896.77/297.14 , o() -> n__o() 896.77/297.14 , u() -> n__u() } 896.77/297.14 Obligation: 896.77/297.14 runtime complexity 896.77/297.14 Answer: 896.77/297.14 MAYBE 896.77/297.14 896.77/297.14 None of the processors succeeded. 896.77/297.14 896.77/297.14 Details of failed attempt(s): 896.77/297.14 ----------------------------- 896.77/297.14 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 896.77/297.14 following reason: 896.77/297.14 896.77/297.14 Computation stopped due to timeout after 297.0 seconds. 896.77/297.14 896.77/297.14 2) 'Best' failed due to the following reason: 896.77/297.14 896.77/297.14 None of the processors succeeded. 896.77/297.14 896.77/297.14 Details of failed attempt(s): 896.77/297.14 ----------------------------- 896.77/297.14 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 896.77/297.14 seconds)' failed due to the following reason: 896.77/297.14 896.77/297.14 Computation stopped due to timeout after 148.0 seconds. 896.77/297.14 896.77/297.14 2) 'Best' failed due to the following reason: 896.77/297.14 896.77/297.14 None of the processors succeeded. 896.77/297.14 896.77/297.14 Details of failed attempt(s): 896.77/297.14 ----------------------------- 896.77/297.14 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 896.77/297.14 following reason: 896.77/297.14 896.77/297.14 The processor is inapplicable, reason: 896.77/297.14 Processor only applicable for innermost runtime complexity analysis 896.77/297.14 896.77/297.14 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 896.77/297.14 to the following reason: 896.77/297.14 896.77/297.14 The processor is inapplicable, reason: 896.77/297.14 Processor only applicable for innermost runtime complexity analysis 896.77/297.14 896.77/297.14 896.77/297.14 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 896.77/297.14 failed due to the following reason: 896.77/297.14 896.77/297.14 None of the processors succeeded. 896.77/297.14 896.77/297.14 Details of failed attempt(s): 896.77/297.14 ----------------------------- 896.77/297.14 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 896.77/297.14 failed due to the following reason: 896.77/297.14 896.77/297.14 match-boundness of the problem could not be verified. 896.77/297.14 896.77/297.14 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 896.77/297.14 failed due to the following reason: 896.77/297.14 896.77/297.14 match-boundness of the problem could not be verified. 896.77/297.14 896.77/297.14 896.77/297.14 896.77/297.14 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 896.77/297.14 the following reason: 896.77/297.14 896.77/297.14 We add the following weak dependency pairs: 896.77/297.14 896.77/297.14 Strict DPs: 896.77/297.14 { __^#(X1, X2) -> c_1(X1, X2) 896.77/297.14 , __^#(X, nil()) -> c_2(X) 896.77/297.14 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.14 , __^#(nil(), X) -> c_4(X) 896.77/297.14 , nil^#() -> c_5() 896.77/297.14 , U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.14 , U12^#(tt()) -> c_7() 896.77/297.14 , isNeList^#(V) -> 896.77/297.14 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isNeList^#(n____(V1, V2)) -> 896.77/297.14 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , isNeList^#(n____(V1, V2)) -> 896.77/297.14 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.14 , U41^#(tt(), V1, V2) -> 896.77/297.14 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.14 , U51^#(tt(), V1, V2) -> 896.77/297.14 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.14 , activate^#(X) -> c_11(X) 896.77/297.14 , activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.14 , activate^#(n____(X1, X2)) -> 896.77/297.14 c_13(__^#(activate(X1), activate(X2))) 896.77/297.14 , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.14 , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.14 , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.14 , activate^#(n__a()) -> c_17(a^#()) 896.77/297.14 , activate^#(n__e()) -> c_18(e^#()) 896.77/297.14 , activate^#(n__i()) -> c_19(i^#()) 896.77/297.14 , activate^#(n__o()) -> c_20(o^#()) 896.77/297.14 , activate^#(n__u()) -> c_21(u^#()) 896.77/297.14 , isPalListKind^#(X) -> c_49(X) 896.77/297.14 , isPalListKind^#(n__nil()) -> c_50() 896.77/297.14 , isPalListKind^#(n____(V1, V2)) -> 896.77/297.14 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2)))) 896.77/297.14 , isPalListKind^#(n__a()) -> c_52() 896.77/297.14 , isPalListKind^#(n__e()) -> c_53() 896.77/297.14 , isPalListKind^#(n__i()) -> c_54() 896.77/297.14 , isPalListKind^#(n__o()) -> c_55() 896.77/297.14 , isPalListKind^#(n__u()) -> c_56() 896.77/297.14 , and^#(X1, X2) -> c_47(X1, X2) 896.77/297.14 , and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.14 , isPal^#(V) -> 896.77/297.14 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isPal^#(X) -> c_58(X) 896.77/297.14 , isPal^#(n__nil()) -> c_59() 896.77/297.14 , a^#() -> c_60() 896.77/297.14 , e^#() -> c_61() 896.77/297.14 , i^#() -> c_62() 896.77/297.14 , o^#() -> c_63() 896.77/297.14 , u^#() -> c_64() 896.77/297.14 , U21^#(tt(), V1, V2) -> 896.77/297.14 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.14 , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.14 , U23^#(tt()) -> c_27() 896.77/297.14 , isList^#(V) -> 896.77/297.14 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isList^#(n__nil()) -> c_25() 896.77/297.14 , isList^#(n____(V1, V2)) -> 896.77/297.14 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , U32^#(tt()) -> c_29() 896.77/297.14 , isQid^#(n__a()) -> c_30() 896.77/297.14 , isQid^#(n__e()) -> c_31() 896.77/297.14 , isQid^#(n__i()) -> c_32() 896.77/297.14 , isQid^#(n__o()) -> c_33() 896.77/297.14 , isQid^#(n__u()) -> c_34() 896.77/297.14 , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.14 , U43^#(tt()) -> c_37() 896.77/297.14 , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.14 , U53^#(tt()) -> c_40() 896.77/297.14 , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.14 , U62^#(tt()) -> c_42() 896.77/297.14 , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.14 , U72^#(tt()) -> c_44() 896.77/297.14 , isNePal^#(V) -> 896.77/297.14 c_45(U61^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isNePal^#(n____(I, n____(P, I))) -> 896.77/297.14 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.14 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 896.77/297.14 896.77/297.14 and mark the set of starting terms. 896.77/297.14 896.77/297.14 We are left with following problem, upon which TcT provides the 896.77/297.14 certificate MAYBE. 896.77/297.14 896.77/297.14 Strict DPs: 896.77/297.14 { __^#(X1, X2) -> c_1(X1, X2) 896.77/297.14 , __^#(X, nil()) -> c_2(X) 896.77/297.14 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.14 , __^#(nil(), X) -> c_4(X) 896.77/297.14 , nil^#() -> c_5() 896.77/297.14 , U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.14 , U12^#(tt()) -> c_7() 896.77/297.14 , isNeList^#(V) -> 896.77/297.14 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isNeList^#(n____(V1, V2)) -> 896.77/297.14 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , isNeList^#(n____(V1, V2)) -> 896.77/297.14 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.14 , U41^#(tt(), V1, V2) -> 896.77/297.14 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.14 , U51^#(tt(), V1, V2) -> 896.77/297.14 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.14 , activate^#(X) -> c_11(X) 896.77/297.14 , activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.14 , activate^#(n____(X1, X2)) -> 896.77/297.14 c_13(__^#(activate(X1), activate(X2))) 896.77/297.14 , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.14 , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.14 , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.14 , activate^#(n__a()) -> c_17(a^#()) 896.77/297.14 , activate^#(n__e()) -> c_18(e^#()) 896.77/297.14 , activate^#(n__i()) -> c_19(i^#()) 896.77/297.14 , activate^#(n__o()) -> c_20(o^#()) 896.77/297.14 , activate^#(n__u()) -> c_21(u^#()) 896.77/297.14 , isPalListKind^#(X) -> c_49(X) 896.77/297.14 , isPalListKind^#(n__nil()) -> c_50() 896.77/297.14 , isPalListKind^#(n____(V1, V2)) -> 896.77/297.14 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2)))) 896.77/297.14 , isPalListKind^#(n__a()) -> c_52() 896.77/297.14 , isPalListKind^#(n__e()) -> c_53() 896.77/297.14 , isPalListKind^#(n__i()) -> c_54() 896.77/297.14 , isPalListKind^#(n__o()) -> c_55() 896.77/297.14 , isPalListKind^#(n__u()) -> c_56() 896.77/297.14 , and^#(X1, X2) -> c_47(X1, X2) 896.77/297.14 , and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.14 , isPal^#(V) -> 896.77/297.14 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isPal^#(X) -> c_58(X) 896.77/297.14 , isPal^#(n__nil()) -> c_59() 896.77/297.14 , a^#() -> c_60() 896.77/297.14 , e^#() -> c_61() 896.77/297.14 , i^#() -> c_62() 896.77/297.14 , o^#() -> c_63() 896.77/297.14 , u^#() -> c_64() 896.77/297.14 , U21^#(tt(), V1, V2) -> 896.77/297.14 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.14 , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.14 , U23^#(tt()) -> c_27() 896.77/297.14 , isList^#(V) -> 896.77/297.14 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isList^#(n__nil()) -> c_25() 896.77/297.14 , isList^#(n____(V1, V2)) -> 896.77/297.14 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , U32^#(tt()) -> c_29() 896.77/297.14 , isQid^#(n__a()) -> c_30() 896.77/297.14 , isQid^#(n__e()) -> c_31() 896.77/297.14 , isQid^#(n__i()) -> c_32() 896.77/297.14 , isQid^#(n__o()) -> c_33() 896.77/297.14 , isQid^#(n__u()) -> c_34() 896.77/297.14 , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.14 , U43^#(tt()) -> c_37() 896.77/297.14 , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.14 , U53^#(tt()) -> c_40() 896.77/297.14 , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.14 , U62^#(tt()) -> c_42() 896.77/297.14 , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.14 , U72^#(tt()) -> c_44() 896.77/297.14 , isNePal^#(V) -> 896.77/297.14 c_45(U61^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isNePal^#(n____(I, n____(P, I))) -> 896.77/297.14 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.14 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 896.77/297.14 Strict Trs: 896.77/297.14 { __(X1, X2) -> n____(X1, X2) 896.77/297.14 , __(X, nil()) -> X 896.77/297.14 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 896.77/297.14 , __(nil(), X) -> X 896.77/297.14 , nil() -> n__nil() 896.77/297.14 , U11(tt(), V) -> U12(isNeList(activate(V))) 896.77/297.14 , U12(tt()) -> tt() 896.77/297.14 , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isNeList(n____(V1, V2)) -> 896.77/297.14 U41(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2)) 896.77/297.14 , isNeList(n____(V1, V2)) -> 896.77/297.14 U51(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2)) 896.77/297.14 , activate(X) -> X 896.77/297.14 , activate(n__nil()) -> nil() 896.77/297.14 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 896.77/297.14 , activate(n__isPalListKind(X)) -> isPalListKind(X) 896.77/297.14 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 896.77/297.14 , activate(n__isPal(X)) -> isPal(X) 896.77/297.14 , activate(n__a()) -> a() 896.77/297.14 , activate(n__e()) -> e() 896.77/297.14 , activate(n__i()) -> i() 896.77/297.14 , activate(n__o()) -> o() 896.77/297.14 , activate(n__u()) -> u() 896.77/297.14 , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) 896.77/297.14 , U22(tt(), V2) -> U23(isList(activate(V2))) 896.77/297.14 , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isList(n__nil()) -> tt() 896.77/297.14 , isList(n____(V1, V2)) -> 896.77/297.14 U21(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2)) 896.77/297.14 , U23(tt()) -> tt() 896.77/297.14 , U31(tt(), V) -> U32(isQid(activate(V))) 896.77/297.14 , U32(tt()) -> tt() 896.77/297.14 , isQid(n__a()) -> tt() 896.77/297.14 , isQid(n__e()) -> tt() 896.77/297.14 , isQid(n__i()) -> tt() 896.77/297.14 , isQid(n__o()) -> tt() 896.77/297.14 , isQid(n__u()) -> tt() 896.77/297.14 , U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)) 896.77/297.14 , U42(tt(), V2) -> U43(isNeList(activate(V2))) 896.77/297.14 , U43(tt()) -> tt() 896.77/297.14 , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) 896.77/297.14 , U52(tt(), V2) -> U53(isList(activate(V2))) 896.77/297.14 , U53(tt()) -> tt() 896.77/297.14 , U61(tt(), V) -> U62(isQid(activate(V))) 896.77/297.14 , U62(tt()) -> tt() 896.77/297.14 , U71(tt(), V) -> U72(isNePal(activate(V))) 896.77/297.14 , U72(tt()) -> tt() 896.77/297.14 , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isNePal(n____(I, n____(P, I))) -> 896.77/297.14 and(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.14 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) 896.77/297.14 , and(X1, X2) -> n__and(X1, X2) 896.77/297.14 , and(tt(), X) -> activate(X) 896.77/297.14 , isPalListKind(X) -> n__isPalListKind(X) 896.77/297.14 , isPalListKind(n__nil()) -> tt() 896.77/297.14 , isPalListKind(n____(V1, V2)) -> 896.77/297.14 and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) 896.77/297.14 , isPalListKind(n__a()) -> tt() 896.77/297.14 , isPalListKind(n__e()) -> tt() 896.77/297.14 , isPalListKind(n__i()) -> tt() 896.77/297.14 , isPalListKind(n__o()) -> tt() 896.77/297.14 , isPalListKind(n__u()) -> tt() 896.77/297.14 , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isPal(X) -> n__isPal(X) 896.77/297.14 , isPal(n__nil()) -> tt() 896.77/297.14 , a() -> n__a() 896.77/297.14 , e() -> n__e() 896.77/297.14 , i() -> n__i() 896.77/297.14 , o() -> n__o() 896.77/297.14 , u() -> n__u() } 896.77/297.14 Obligation: 896.77/297.14 runtime complexity 896.77/297.14 Answer: 896.77/297.14 MAYBE 896.77/297.14 896.77/297.14 We estimate the number of application of 896.77/297.14 {5,7,26,28,29,30,31,32,37,38,39,40,41,42,45,47,49,50,51,52,53,54,56,58,60,62} 896.77/297.14 by applications of 896.77/297.14 Pre({5,7,26,28,29,30,31,32,37,38,39,40,41,42,45,47,49,50,51,52,53,54,56,58,60,62}) 896.77/297.14 = {1,2,4,6,11,14,15,17,19,20,21,22,23,24,25,33,36,44,55,57,59,61}. 896.77/297.14 Here rules are labeled as follows: 896.77/297.14 896.77/297.14 DPs: 896.77/297.14 { 1: __^#(X1, X2) -> c_1(X1, X2) 896.77/297.14 , 2: __^#(X, nil()) -> c_2(X) 896.77/297.14 , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.14 , 4: __^#(nil(), X) -> c_4(X) 896.77/297.14 , 5: nil^#() -> c_5() 896.77/297.14 , 6: U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.14 , 7: U12^#(tt()) -> c_7() 896.77/297.14 , 8: isNeList^#(V) -> 896.77/297.14 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , 9: isNeList^#(n____(V1, V2)) -> 896.77/297.14 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , 10: isNeList^#(n____(V1, V2)) -> 896.77/297.14 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , 11: U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.14 , 12: U41^#(tt(), V1, V2) -> 896.77/297.14 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.14 , 13: U51^#(tt(), V1, V2) -> 896.77/297.14 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.14 , 14: activate^#(X) -> c_11(X) 896.77/297.14 , 15: activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.14 , 16: activate^#(n____(X1, X2)) -> 896.77/297.14 c_13(__^#(activate(X1), activate(X2))) 896.77/297.14 , 17: activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.14 , 18: activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.14 , 19: activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.14 , 20: activate^#(n__a()) -> c_17(a^#()) 896.77/297.14 , 21: activate^#(n__e()) -> c_18(e^#()) 896.77/297.14 , 22: activate^#(n__i()) -> c_19(i^#()) 896.77/297.14 , 23: activate^#(n__o()) -> c_20(o^#()) 896.77/297.14 , 24: activate^#(n__u()) -> c_21(u^#()) 896.77/297.14 , 25: isPalListKind^#(X) -> c_49(X) 896.77/297.14 , 26: isPalListKind^#(n__nil()) -> c_50() 896.77/297.14 , 27: isPalListKind^#(n____(V1, V2)) -> 896.77/297.14 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2)))) 896.77/297.14 , 28: isPalListKind^#(n__a()) -> c_52() 896.77/297.14 , 29: isPalListKind^#(n__e()) -> c_53() 896.77/297.14 , 30: isPalListKind^#(n__i()) -> c_54() 896.77/297.14 , 31: isPalListKind^#(n__o()) -> c_55() 896.77/297.14 , 32: isPalListKind^#(n__u()) -> c_56() 896.77/297.14 , 33: and^#(X1, X2) -> c_47(X1, X2) 896.77/297.14 , 34: and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.14 , 35: isPal^#(V) -> 896.77/297.14 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , 36: isPal^#(X) -> c_58(X) 896.77/297.14 , 37: isPal^#(n__nil()) -> c_59() 896.77/297.14 , 38: a^#() -> c_60() 896.77/297.14 , 39: e^#() -> c_61() 896.77/297.14 , 40: i^#() -> c_62() 896.77/297.14 , 41: o^#() -> c_63() 896.77/297.14 , 42: u^#() -> c_64() 896.77/297.14 , 43: U21^#(tt(), V1, V2) -> 896.77/297.14 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.14 , 44: U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.14 , 45: U23^#(tt()) -> c_27() 896.77/297.14 , 46: isList^#(V) -> 896.77/297.14 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , 47: isList^#(n__nil()) -> c_25() 896.77/297.14 , 48: isList^#(n____(V1, V2)) -> 896.77/297.14 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , 49: U32^#(tt()) -> c_29() 896.77/297.14 , 50: isQid^#(n__a()) -> c_30() 896.77/297.14 , 51: isQid^#(n__e()) -> c_31() 896.77/297.14 , 52: isQid^#(n__i()) -> c_32() 896.77/297.14 , 53: isQid^#(n__o()) -> c_33() 896.77/297.14 , 54: isQid^#(n__u()) -> c_34() 896.77/297.14 , 55: U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.14 , 56: U43^#(tt()) -> c_37() 896.77/297.14 , 57: U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.14 , 58: U53^#(tt()) -> c_40() 896.77/297.14 , 59: U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.14 , 60: U62^#(tt()) -> c_42() 896.77/297.14 , 61: U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.14 , 62: U72^#(tt()) -> c_44() 896.77/297.14 , 63: isNePal^#(V) -> 896.77/297.14 c_45(U61^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , 64: isNePal^#(n____(I, n____(P, I))) -> 896.77/297.14 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.14 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 896.77/297.14 896.77/297.14 We are left with following problem, upon which TcT provides the 896.77/297.14 certificate MAYBE. 896.77/297.14 896.77/297.14 Strict DPs: 896.77/297.14 { __^#(X1, X2) -> c_1(X1, X2) 896.77/297.14 , __^#(X, nil()) -> c_2(X) 896.77/297.14 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.14 , __^#(nil(), X) -> c_4(X) 896.77/297.14 , U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.14 , isNeList^#(V) -> 896.77/297.14 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isNeList^#(n____(V1, V2)) -> 896.77/297.14 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , isNeList^#(n____(V1, V2)) -> 896.77/297.14 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.14 , U41^#(tt(), V1, V2) -> 896.77/297.14 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.14 , U51^#(tt(), V1, V2) -> 896.77/297.14 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.14 , activate^#(X) -> c_11(X) 896.77/297.14 , activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.14 , activate^#(n____(X1, X2)) -> 896.77/297.14 c_13(__^#(activate(X1), activate(X2))) 896.77/297.14 , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.14 , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.14 , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.14 , activate^#(n__a()) -> c_17(a^#()) 896.77/297.14 , activate^#(n__e()) -> c_18(e^#()) 896.77/297.14 , activate^#(n__i()) -> c_19(i^#()) 896.77/297.14 , activate^#(n__o()) -> c_20(o^#()) 896.77/297.14 , activate^#(n__u()) -> c_21(u^#()) 896.77/297.14 , isPalListKind^#(X) -> c_49(X) 896.77/297.14 , isPalListKind^#(n____(V1, V2)) -> 896.77/297.14 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2)))) 896.77/297.14 , and^#(X1, X2) -> c_47(X1, X2) 896.77/297.14 , and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.14 , isPal^#(V) -> 896.77/297.14 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isPal^#(X) -> c_58(X) 896.77/297.14 , U21^#(tt(), V1, V2) -> 896.77/297.14 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.14 , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.14 , isList^#(V) -> 896.77/297.14 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isList^#(n____(V1, V2)) -> 896.77/297.14 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2))) 896.77/297.14 , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.14 , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.14 , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.14 , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.14 , isNePal^#(V) -> 896.77/297.14 c_45(U61^#(isPalListKind(activate(V)), activate(V))) 896.77/297.14 , isNePal^#(n____(I, n____(P, I))) -> 896.77/297.14 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.14 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 896.77/297.14 Strict Trs: 896.77/297.14 { __(X1, X2) -> n____(X1, X2) 896.77/297.14 , __(X, nil()) -> X 896.77/297.14 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 896.77/297.14 , __(nil(), X) -> X 896.77/297.14 , nil() -> n__nil() 896.77/297.14 , U11(tt(), V) -> U12(isNeList(activate(V))) 896.77/297.14 , U12(tt()) -> tt() 896.77/297.14 , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) 896.77/297.14 , isNeList(n____(V1, V2)) -> 896.77/297.14 U41(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2)) 896.77/297.14 , isNeList(n____(V1, V2)) -> 896.77/297.14 U51(and(isPalListKind(activate(V1)), 896.77/297.14 n__isPalListKind(activate(V2))), 896.77/297.14 activate(V1), 896.77/297.14 activate(V2)) 896.77/297.14 , activate(X) -> X 896.77/297.14 , activate(n__nil()) -> nil() 896.77/297.14 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 896.77/297.14 , activate(n__isPalListKind(X)) -> isPalListKind(X) 896.77/297.14 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 896.77/297.14 , activate(n__isPal(X)) -> isPal(X) 896.77/297.14 , activate(n__a()) -> a() 896.77/297.14 , activate(n__e()) -> e() 896.77/297.14 , activate(n__i()) -> i() 896.77/297.14 , activate(n__o()) -> o() 896.77/297.14 , activate(n__u()) -> u() 896.77/297.14 , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) 896.77/297.14 , U22(tt(), V2) -> U23(isList(activate(V2))) 896.77/297.14 , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) 896.77/297.15 , isList(n__nil()) -> tt() 896.77/297.15 , isList(n____(V1, V2)) -> 896.77/297.15 U21(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2)) 896.77/297.15 , U23(tt()) -> tt() 896.77/297.15 , U31(tt(), V) -> U32(isQid(activate(V))) 896.77/297.15 , U32(tt()) -> tt() 896.77/297.15 , isQid(n__a()) -> tt() 896.77/297.15 , isQid(n__e()) -> tt() 896.77/297.15 , isQid(n__i()) -> tt() 896.77/297.15 , isQid(n__o()) -> tt() 896.77/297.15 , isQid(n__u()) -> tt() 896.77/297.15 , U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)) 896.77/297.15 , U42(tt(), V2) -> U43(isNeList(activate(V2))) 896.77/297.15 , U43(tt()) -> tt() 896.77/297.15 , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) 896.77/297.15 , U52(tt(), V2) -> U53(isList(activate(V2))) 896.77/297.15 , U53(tt()) -> tt() 896.77/297.15 , U61(tt(), V) -> U62(isQid(activate(V))) 896.77/297.15 , U62(tt()) -> tt() 896.77/297.15 , U71(tt(), V) -> U72(isNePal(activate(V))) 896.77/297.15 , U72(tt()) -> tt() 896.77/297.15 , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) 896.77/297.15 , isNePal(n____(I, n____(P, I))) -> 896.77/297.15 and(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.15 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) 896.77/297.15 , and(X1, X2) -> n__and(X1, X2) 896.77/297.15 , and(tt(), X) -> activate(X) 896.77/297.15 , isPalListKind(X) -> n__isPalListKind(X) 896.77/297.15 , isPalListKind(n__nil()) -> tt() 896.77/297.15 , isPalListKind(n____(V1, V2)) -> 896.77/297.15 and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) 896.77/297.15 , isPalListKind(n__a()) -> tt() 896.77/297.15 , isPalListKind(n__e()) -> tt() 896.77/297.15 , isPalListKind(n__i()) -> tt() 896.77/297.15 , isPalListKind(n__o()) -> tt() 896.77/297.15 , isPalListKind(n__u()) -> tt() 896.77/297.15 , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) 896.77/297.15 , isPal(X) -> n__isPal(X) 896.77/297.15 , isPal(n__nil()) -> tt() 896.77/297.15 , a() -> n__a() 896.77/297.15 , e() -> n__e() 896.77/297.15 , i() -> n__i() 896.77/297.15 , o() -> n__o() 896.77/297.15 , u() -> n__u() } 896.77/297.15 Weak DPs: 896.77/297.15 { nil^#() -> c_5() 896.77/297.15 , U12^#(tt()) -> c_7() 896.77/297.15 , isPalListKind^#(n__nil()) -> c_50() 896.77/297.15 , isPalListKind^#(n__a()) -> c_52() 896.77/297.15 , isPalListKind^#(n__e()) -> c_53() 896.77/297.15 , isPalListKind^#(n__i()) -> c_54() 896.77/297.15 , isPalListKind^#(n__o()) -> c_55() 896.77/297.15 , isPalListKind^#(n__u()) -> c_56() 896.77/297.15 , isPal^#(n__nil()) -> c_59() 896.77/297.15 , a^#() -> c_60() 896.77/297.15 , e^#() -> c_61() 896.77/297.15 , i^#() -> c_62() 896.77/297.15 , o^#() -> c_63() 896.77/297.15 , u^#() -> c_64() 896.77/297.15 , U23^#(tt()) -> c_27() 896.77/297.15 , isList^#(n__nil()) -> c_25() 896.77/297.15 , U32^#(tt()) -> c_29() 896.77/297.15 , isQid^#(n__a()) -> c_30() 896.77/297.15 , isQid^#(n__e()) -> c_31() 896.77/297.15 , isQid^#(n__i()) -> c_32() 896.77/297.15 , isQid^#(n__o()) -> c_33() 896.77/297.15 , isQid^#(n__u()) -> c_34() 896.77/297.15 , U43^#(tt()) -> c_37() 896.77/297.15 , U53^#(tt()) -> c_40() 896.77/297.15 , U62^#(tt()) -> c_42() 896.77/297.15 , U72^#(tt()) -> c_44() } 896.77/297.15 Obligation: 896.77/297.15 runtime complexity 896.77/297.15 Answer: 896.77/297.15 MAYBE 896.77/297.15 896.77/297.15 We estimate the number of application of 896.77/297.15 {5,9,13,18,19,20,21,22,30,33,34,35,36} by applications of 896.77/297.15 Pre({5,9,13,18,19,20,21,22,30,33,34,35,36}) = 896.77/297.15 {1,2,4,6,10,11,12,23,25,26,27,28,29,31,37}. Here rules are labeled 896.77/297.15 as follows: 896.77/297.15 896.77/297.15 DPs: 896.77/297.15 { 1: __^#(X1, X2) -> c_1(X1, X2) 896.77/297.15 , 2: __^#(X, nil()) -> c_2(X) 896.77/297.15 , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.15 , 4: __^#(nil(), X) -> c_4(X) 896.77/297.15 , 5: U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.15 , 6: isNeList^#(V) -> 896.77/297.15 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , 7: isNeList^#(n____(V1, V2)) -> 896.77/297.15 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2))) 896.77/297.15 , 8: isNeList^#(n____(V1, V2)) -> 896.77/297.15 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2))) 896.77/297.15 , 9: U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.15 , 10: U41^#(tt(), V1, V2) -> 896.77/297.15 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.15 , 11: U51^#(tt(), V1, V2) -> 896.77/297.15 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.15 , 12: activate^#(X) -> c_11(X) 896.77/297.15 , 13: activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.15 , 14: activate^#(n____(X1, X2)) -> 896.77/297.15 c_13(__^#(activate(X1), activate(X2))) 896.77/297.15 , 15: activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.15 , 16: activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.15 , 17: activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.15 , 18: activate^#(n__a()) -> c_17(a^#()) 896.77/297.15 , 19: activate^#(n__e()) -> c_18(e^#()) 896.77/297.15 , 20: activate^#(n__i()) -> c_19(i^#()) 896.77/297.15 , 21: activate^#(n__o()) -> c_20(o^#()) 896.77/297.15 , 22: activate^#(n__u()) -> c_21(u^#()) 896.77/297.15 , 23: isPalListKind^#(X) -> c_49(X) 896.77/297.15 , 24: isPalListKind^#(n____(V1, V2)) -> 896.77/297.15 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2)))) 896.77/297.15 , 25: and^#(X1, X2) -> c_47(X1, X2) 896.77/297.15 , 26: and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.15 , 27: isPal^#(V) -> 896.77/297.15 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , 28: isPal^#(X) -> c_58(X) 896.77/297.15 , 29: U21^#(tt(), V1, V2) -> 896.77/297.15 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.15 , 30: U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.15 , 31: isList^#(V) -> 896.77/297.15 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , 32: isList^#(n____(V1, V2)) -> 896.77/297.15 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2))) 896.77/297.15 , 33: U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.15 , 34: U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.15 , 35: U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.15 , 36: U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.15 , 37: isNePal^#(V) -> 896.77/297.15 c_45(U61^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , 38: isNePal^#(n____(I, n____(P, I))) -> 896.77/297.15 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.15 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) 896.77/297.15 , 39: nil^#() -> c_5() 896.77/297.15 , 40: U12^#(tt()) -> c_7() 896.77/297.15 , 41: isPalListKind^#(n__nil()) -> c_50() 896.77/297.15 , 42: isPalListKind^#(n__a()) -> c_52() 896.77/297.15 , 43: isPalListKind^#(n__e()) -> c_53() 896.77/297.15 , 44: isPalListKind^#(n__i()) -> c_54() 896.77/297.15 , 45: isPalListKind^#(n__o()) -> c_55() 896.77/297.15 , 46: isPalListKind^#(n__u()) -> c_56() 896.77/297.15 , 47: isPal^#(n__nil()) -> c_59() 896.77/297.15 , 48: a^#() -> c_60() 896.77/297.15 , 49: e^#() -> c_61() 896.77/297.15 , 50: i^#() -> c_62() 896.77/297.15 , 51: o^#() -> c_63() 896.77/297.15 , 52: u^#() -> c_64() 896.77/297.15 , 53: U23^#(tt()) -> c_27() 896.77/297.15 , 54: isList^#(n__nil()) -> c_25() 896.77/297.15 , 55: U32^#(tt()) -> c_29() 896.77/297.15 , 56: isQid^#(n__a()) -> c_30() 896.77/297.15 , 57: isQid^#(n__e()) -> c_31() 896.77/297.15 , 58: isQid^#(n__i()) -> c_32() 896.77/297.15 , 59: isQid^#(n__o()) -> c_33() 896.77/297.15 , 60: isQid^#(n__u()) -> c_34() 896.77/297.15 , 61: U43^#(tt()) -> c_37() 896.77/297.15 , 62: U53^#(tt()) -> c_40() 896.77/297.15 , 63: U62^#(tt()) -> c_42() 896.77/297.15 , 64: U72^#(tt()) -> c_44() } 896.77/297.15 896.77/297.15 We are left with following problem, upon which TcT provides the 896.77/297.15 certificate MAYBE. 896.77/297.15 896.77/297.15 Strict DPs: 896.77/297.15 { __^#(X1, X2) -> c_1(X1, X2) 896.77/297.15 , __^#(X, nil()) -> c_2(X) 896.77/297.15 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.15 , __^#(nil(), X) -> c_4(X) 896.77/297.15 , isNeList^#(V) -> 896.77/297.15 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , isNeList^#(n____(V1, V2)) -> 896.77/297.15 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2))) 896.77/297.15 , isNeList^#(n____(V1, V2)) -> 896.77/297.15 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2))) 896.77/297.15 , U41^#(tt(), V1, V2) -> 896.77/297.15 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.15 , U51^#(tt(), V1, V2) -> 896.77/297.15 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.15 , activate^#(X) -> c_11(X) 896.77/297.15 , activate^#(n____(X1, X2)) -> 896.77/297.15 c_13(__^#(activate(X1), activate(X2))) 896.77/297.15 , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.15 , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.15 , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.15 , isPalListKind^#(X) -> c_49(X) 896.77/297.15 , isPalListKind^#(n____(V1, V2)) -> 896.77/297.15 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2)))) 896.77/297.15 , and^#(X1, X2) -> c_47(X1, X2) 896.77/297.15 , and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.15 , isPal^#(V) -> 896.77/297.15 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , isPal^#(X) -> c_58(X) 896.77/297.15 , U21^#(tt(), V1, V2) -> 896.77/297.15 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.15 , isList^#(V) -> 896.77/297.15 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , isList^#(n____(V1, V2)) -> 896.77/297.15 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2))) 896.77/297.15 , isNePal^#(V) -> 896.77/297.15 c_45(U61^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , isNePal^#(n____(I, n____(P, I))) -> 896.77/297.15 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.15 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 896.77/297.15 Strict Trs: 896.77/297.15 { __(X1, X2) -> n____(X1, X2) 896.77/297.15 , __(X, nil()) -> X 896.77/297.15 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 896.77/297.15 , __(nil(), X) -> X 896.77/297.15 , nil() -> n__nil() 896.77/297.15 , U11(tt(), V) -> U12(isNeList(activate(V))) 896.77/297.15 , U12(tt()) -> tt() 896.77/297.15 , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) 896.77/297.15 , isNeList(n____(V1, V2)) -> 896.77/297.15 U41(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2)) 896.77/297.15 , isNeList(n____(V1, V2)) -> 896.77/297.15 U51(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2)) 896.77/297.15 , activate(X) -> X 896.77/297.15 , activate(n__nil()) -> nil() 896.77/297.15 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 896.77/297.15 , activate(n__isPalListKind(X)) -> isPalListKind(X) 896.77/297.15 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 896.77/297.15 , activate(n__isPal(X)) -> isPal(X) 896.77/297.15 , activate(n__a()) -> a() 896.77/297.15 , activate(n__e()) -> e() 896.77/297.15 , activate(n__i()) -> i() 896.77/297.15 , activate(n__o()) -> o() 896.77/297.15 , activate(n__u()) -> u() 896.77/297.15 , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) 896.77/297.15 , U22(tt(), V2) -> U23(isList(activate(V2))) 896.77/297.15 , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) 896.77/297.15 , isList(n__nil()) -> tt() 896.77/297.15 , isList(n____(V1, V2)) -> 896.77/297.15 U21(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2)) 896.77/297.15 , U23(tt()) -> tt() 896.77/297.15 , U31(tt(), V) -> U32(isQid(activate(V))) 896.77/297.15 , U32(tt()) -> tt() 896.77/297.15 , isQid(n__a()) -> tt() 896.77/297.15 , isQid(n__e()) -> tt() 896.77/297.15 , isQid(n__i()) -> tt() 896.77/297.15 , isQid(n__o()) -> tt() 896.77/297.15 , isQid(n__u()) -> tt() 896.77/297.15 , U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)) 896.77/297.15 , U42(tt(), V2) -> U43(isNeList(activate(V2))) 896.77/297.15 , U43(tt()) -> tt() 896.77/297.15 , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) 896.77/297.15 , U52(tt(), V2) -> U53(isList(activate(V2))) 896.77/297.15 , U53(tt()) -> tt() 896.77/297.15 , U61(tt(), V) -> U62(isQid(activate(V))) 896.77/297.15 , U62(tt()) -> tt() 896.77/297.15 , U71(tt(), V) -> U72(isNePal(activate(V))) 896.77/297.15 , U72(tt()) -> tt() 896.77/297.15 , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) 896.77/297.15 , isNePal(n____(I, n____(P, I))) -> 896.77/297.15 and(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.15 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) 896.77/297.15 , and(X1, X2) -> n__and(X1, X2) 896.77/297.15 , and(tt(), X) -> activate(X) 896.77/297.15 , isPalListKind(X) -> n__isPalListKind(X) 896.77/297.15 , isPalListKind(n__nil()) -> tt() 896.77/297.15 , isPalListKind(n____(V1, V2)) -> 896.77/297.15 and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) 896.77/297.15 , isPalListKind(n__a()) -> tt() 896.77/297.15 , isPalListKind(n__e()) -> tt() 896.77/297.15 , isPalListKind(n__i()) -> tt() 896.77/297.15 , isPalListKind(n__o()) -> tt() 896.77/297.15 , isPalListKind(n__u()) -> tt() 896.77/297.15 , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) 896.77/297.15 , isPal(X) -> n__isPal(X) 896.77/297.15 , isPal(n__nil()) -> tt() 896.77/297.15 , a() -> n__a() 896.77/297.15 , e() -> n__e() 896.77/297.15 , i() -> n__i() 896.77/297.15 , o() -> n__o() 896.77/297.15 , u() -> n__u() } 896.77/297.15 Weak DPs: 896.77/297.15 { nil^#() -> c_5() 896.77/297.15 , U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.15 , U12^#(tt()) -> c_7() 896.77/297.15 , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.15 , activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.15 , activate^#(n__a()) -> c_17(a^#()) 896.77/297.15 , activate^#(n__e()) -> c_18(e^#()) 896.77/297.15 , activate^#(n__i()) -> c_19(i^#()) 896.77/297.15 , activate^#(n__o()) -> c_20(o^#()) 896.77/297.15 , activate^#(n__u()) -> c_21(u^#()) 896.77/297.15 , isPalListKind^#(n__nil()) -> c_50() 896.77/297.15 , isPalListKind^#(n__a()) -> c_52() 896.77/297.15 , isPalListKind^#(n__e()) -> c_53() 896.77/297.15 , isPalListKind^#(n__i()) -> c_54() 896.77/297.15 , isPalListKind^#(n__o()) -> c_55() 896.77/297.15 , isPalListKind^#(n__u()) -> c_56() 896.77/297.15 , isPal^#(n__nil()) -> c_59() 896.77/297.15 , a^#() -> c_60() 896.77/297.15 , e^#() -> c_61() 896.77/297.15 , i^#() -> c_62() 896.77/297.15 , o^#() -> c_63() 896.77/297.15 , u^#() -> c_64() 896.77/297.15 , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.15 , U23^#(tt()) -> c_27() 896.77/297.15 , isList^#(n__nil()) -> c_25() 896.77/297.15 , U32^#(tt()) -> c_29() 896.77/297.15 , isQid^#(n__a()) -> c_30() 896.77/297.15 , isQid^#(n__e()) -> c_31() 896.77/297.15 , isQid^#(n__i()) -> c_32() 896.77/297.15 , isQid^#(n__o()) -> c_33() 896.77/297.15 , isQid^#(n__u()) -> c_34() 896.77/297.15 , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.15 , U43^#(tt()) -> c_37() 896.77/297.15 , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.15 , U53^#(tt()) -> c_40() 896.77/297.15 , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.15 , U62^#(tt()) -> c_42() 896.77/297.15 , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.15 , U72^#(tt()) -> c_44() } 896.77/297.15 Obligation: 896.77/297.15 runtime complexity 896.77/297.15 Answer: 896.77/297.15 MAYBE 896.77/297.15 896.77/297.15 We estimate the number of application of {5,8,9,19,21,22,24} by 896.77/297.15 applications of Pre({5,8,9,19,21,22,24}) = 896.77/297.15 {1,2,4,6,7,10,14,15,17,20,23}. Here rules are labeled as follows: 896.77/297.15 896.77/297.15 DPs: 896.77/297.15 { 1: __^#(X1, X2) -> c_1(X1, X2) 896.77/297.15 , 2: __^#(X, nil()) -> c_2(X) 896.77/297.15 , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.15 , 4: __^#(nil(), X) -> c_4(X) 896.77/297.15 , 5: isNeList^#(V) -> 896.77/297.15 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , 6: isNeList^#(n____(V1, V2)) -> 896.77/297.15 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2))) 896.77/297.15 , 7: isNeList^#(n____(V1, V2)) -> 896.77/297.15 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2))), 896.77/297.15 activate(V1), 896.77/297.15 activate(V2))) 896.77/297.15 , 8: U41^#(tt(), V1, V2) -> 896.77/297.15 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.15 , 9: U51^#(tt(), V1, V2) -> 896.77/297.15 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.15 , 10: activate^#(X) -> c_11(X) 896.77/297.15 , 11: activate^#(n____(X1, X2)) -> 896.77/297.15 c_13(__^#(activate(X1), activate(X2))) 896.77/297.15 , 12: activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.15 , 13: activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.15 , 14: activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.15 , 15: isPalListKind^#(X) -> c_49(X) 896.77/297.15 , 16: isPalListKind^#(n____(V1, V2)) -> 896.77/297.15 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.15 n__isPalListKind(activate(V2)))) 896.77/297.15 , 17: and^#(X1, X2) -> c_47(X1, X2) 896.77/297.15 , 18: and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.15 , 19: isPal^#(V) -> 896.77/297.15 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , 20: isPal^#(X) -> c_58(X) 896.77/297.15 , 21: U21^#(tt(), V1, V2) -> 896.77/297.15 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.15 , 22: isList^#(V) -> 896.77/297.15 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.15 , 23: isList^#(n____(V1, V2)) -> 896.77/297.15 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , 24: isNePal^#(V) -> 896.77/297.16 c_45(U61^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , 25: isNePal^#(n____(I, n____(P, I))) -> 896.77/297.16 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.16 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) 896.77/297.16 , 26: nil^#() -> c_5() 896.77/297.16 , 27: U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.16 , 28: U12^#(tt()) -> c_7() 896.77/297.16 , 29: U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.16 , 30: activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.16 , 31: activate^#(n__a()) -> c_17(a^#()) 896.77/297.16 , 32: activate^#(n__e()) -> c_18(e^#()) 896.77/297.16 , 33: activate^#(n__i()) -> c_19(i^#()) 896.77/297.16 , 34: activate^#(n__o()) -> c_20(o^#()) 896.77/297.16 , 35: activate^#(n__u()) -> c_21(u^#()) 896.77/297.16 , 36: isPalListKind^#(n__nil()) -> c_50() 896.77/297.16 , 37: isPalListKind^#(n__a()) -> c_52() 896.77/297.16 , 38: isPalListKind^#(n__e()) -> c_53() 896.77/297.16 , 39: isPalListKind^#(n__i()) -> c_54() 896.77/297.16 , 40: isPalListKind^#(n__o()) -> c_55() 896.77/297.16 , 41: isPalListKind^#(n__u()) -> c_56() 896.77/297.16 , 42: isPal^#(n__nil()) -> c_59() 896.77/297.16 , 43: a^#() -> c_60() 896.77/297.16 , 44: e^#() -> c_61() 896.77/297.16 , 45: i^#() -> c_62() 896.77/297.16 , 46: o^#() -> c_63() 896.77/297.16 , 47: u^#() -> c_64() 896.77/297.16 , 48: U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.16 , 49: U23^#(tt()) -> c_27() 896.77/297.16 , 50: isList^#(n__nil()) -> c_25() 896.77/297.16 , 51: U32^#(tt()) -> c_29() 896.77/297.16 , 52: isQid^#(n__a()) -> c_30() 896.77/297.16 , 53: isQid^#(n__e()) -> c_31() 896.77/297.16 , 54: isQid^#(n__i()) -> c_32() 896.77/297.16 , 55: isQid^#(n__o()) -> c_33() 896.77/297.16 , 56: isQid^#(n__u()) -> c_34() 896.77/297.16 , 57: U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.16 , 58: U43^#(tt()) -> c_37() 896.77/297.16 , 59: U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.16 , 60: U53^#(tt()) -> c_40() 896.77/297.16 , 61: U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.16 , 62: U62^#(tt()) -> c_42() 896.77/297.16 , 63: U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.16 , 64: U72^#(tt()) -> c_44() } 896.77/297.16 896.77/297.16 We are left with following problem, upon which TcT provides the 896.77/297.16 certificate MAYBE. 896.77/297.16 896.77/297.16 Strict DPs: 896.77/297.16 { __^#(X1, X2) -> c_1(X1, X2) 896.77/297.16 , __^#(X, nil()) -> c_2(X) 896.77/297.16 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.16 , __^#(nil(), X) -> c_4(X) 896.77/297.16 , isNeList^#(n____(V1, V2)) -> 896.77/297.16 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , isNeList^#(n____(V1, V2)) -> 896.77/297.16 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , activate^#(X) -> c_11(X) 896.77/297.16 , activate^#(n____(X1, X2)) -> 896.77/297.16 c_13(__^#(activate(X1), activate(X2))) 896.77/297.16 , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.16 , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.16 , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.16 , isPalListKind^#(X) -> c_49(X) 896.77/297.16 , isPalListKind^#(n____(V1, V2)) -> 896.77/297.16 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2)))) 896.77/297.16 , and^#(X1, X2) -> c_47(X1, X2) 896.77/297.16 , and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.16 , isPal^#(X) -> c_58(X) 896.77/297.16 , isList^#(n____(V1, V2)) -> 896.77/297.16 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , isNePal^#(n____(I, n____(P, I))) -> 896.77/297.16 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.16 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 896.77/297.16 Strict Trs: 896.77/297.16 { __(X1, X2) -> n____(X1, X2) 896.77/297.16 , __(X, nil()) -> X 896.77/297.16 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 896.77/297.16 , __(nil(), X) -> X 896.77/297.16 , nil() -> n__nil() 896.77/297.16 , U11(tt(), V) -> U12(isNeList(activate(V))) 896.77/297.16 , U12(tt()) -> tt() 896.77/297.16 , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) 896.77/297.16 , isNeList(n____(V1, V2)) -> 896.77/297.16 U41(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2)) 896.77/297.16 , isNeList(n____(V1, V2)) -> 896.77/297.16 U51(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2)) 896.77/297.16 , activate(X) -> X 896.77/297.16 , activate(n__nil()) -> nil() 896.77/297.16 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 896.77/297.16 , activate(n__isPalListKind(X)) -> isPalListKind(X) 896.77/297.16 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 896.77/297.16 , activate(n__isPal(X)) -> isPal(X) 896.77/297.16 , activate(n__a()) -> a() 896.77/297.16 , activate(n__e()) -> e() 896.77/297.16 , activate(n__i()) -> i() 896.77/297.16 , activate(n__o()) -> o() 896.77/297.16 , activate(n__u()) -> u() 896.77/297.16 , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) 896.77/297.16 , U22(tt(), V2) -> U23(isList(activate(V2))) 896.77/297.16 , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) 896.77/297.16 , isList(n__nil()) -> tt() 896.77/297.16 , isList(n____(V1, V2)) -> 896.77/297.16 U21(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2)) 896.77/297.16 , U23(tt()) -> tt() 896.77/297.16 , U31(tt(), V) -> U32(isQid(activate(V))) 896.77/297.16 , U32(tt()) -> tt() 896.77/297.16 , isQid(n__a()) -> tt() 896.77/297.16 , isQid(n__e()) -> tt() 896.77/297.16 , isQid(n__i()) -> tt() 896.77/297.16 , isQid(n__o()) -> tt() 896.77/297.16 , isQid(n__u()) -> tt() 896.77/297.16 , U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)) 896.77/297.16 , U42(tt(), V2) -> U43(isNeList(activate(V2))) 896.77/297.16 , U43(tt()) -> tt() 896.77/297.16 , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) 896.77/297.16 , U52(tt(), V2) -> U53(isList(activate(V2))) 896.77/297.16 , U53(tt()) -> tt() 896.77/297.16 , U61(tt(), V) -> U62(isQid(activate(V))) 896.77/297.16 , U62(tt()) -> tt() 896.77/297.16 , U71(tt(), V) -> U72(isNePal(activate(V))) 896.77/297.16 , U72(tt()) -> tt() 896.77/297.16 , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) 896.77/297.16 , isNePal(n____(I, n____(P, I))) -> 896.77/297.16 and(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.16 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) 896.77/297.16 , and(X1, X2) -> n__and(X1, X2) 896.77/297.16 , and(tt(), X) -> activate(X) 896.77/297.16 , isPalListKind(X) -> n__isPalListKind(X) 896.77/297.16 , isPalListKind(n__nil()) -> tt() 896.77/297.16 , isPalListKind(n____(V1, V2)) -> 896.77/297.16 and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) 896.77/297.16 , isPalListKind(n__a()) -> tt() 896.77/297.16 , isPalListKind(n__e()) -> tt() 896.77/297.16 , isPalListKind(n__i()) -> tt() 896.77/297.16 , isPalListKind(n__o()) -> tt() 896.77/297.16 , isPalListKind(n__u()) -> tt() 896.77/297.16 , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) 896.77/297.16 , isPal(X) -> n__isPal(X) 896.77/297.16 , isPal(n__nil()) -> tt() 896.77/297.16 , a() -> n__a() 896.77/297.16 , e() -> n__e() 896.77/297.16 , i() -> n__i() 896.77/297.16 , o() -> n__o() 896.77/297.16 , u() -> n__u() } 896.77/297.16 Weak DPs: 896.77/297.16 { nil^#() -> c_5() 896.77/297.16 , U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.16 , U12^#(tt()) -> c_7() 896.77/297.16 , isNeList^#(V) -> 896.77/297.16 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.16 , U41^#(tt(), V1, V2) -> 896.77/297.16 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.16 , U51^#(tt(), V1, V2) -> 896.77/297.16 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.16 , activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.16 , activate^#(n__a()) -> c_17(a^#()) 896.77/297.16 , activate^#(n__e()) -> c_18(e^#()) 896.77/297.16 , activate^#(n__i()) -> c_19(i^#()) 896.77/297.16 , activate^#(n__o()) -> c_20(o^#()) 896.77/297.16 , activate^#(n__u()) -> c_21(u^#()) 896.77/297.16 , isPalListKind^#(n__nil()) -> c_50() 896.77/297.16 , isPalListKind^#(n__a()) -> c_52() 896.77/297.16 , isPalListKind^#(n__e()) -> c_53() 896.77/297.16 , isPalListKind^#(n__i()) -> c_54() 896.77/297.16 , isPalListKind^#(n__o()) -> c_55() 896.77/297.16 , isPalListKind^#(n__u()) -> c_56() 896.77/297.16 , isPal^#(V) -> 896.77/297.16 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , isPal^#(n__nil()) -> c_59() 896.77/297.16 , a^#() -> c_60() 896.77/297.16 , e^#() -> c_61() 896.77/297.16 , i^#() -> c_62() 896.77/297.16 , o^#() -> c_63() 896.77/297.16 , u^#() -> c_64() 896.77/297.16 , U21^#(tt(), V1, V2) -> 896.77/297.16 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.16 , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.16 , U23^#(tt()) -> c_27() 896.77/297.16 , isList^#(V) -> 896.77/297.16 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , isList^#(n__nil()) -> c_25() 896.77/297.16 , U32^#(tt()) -> c_29() 896.77/297.16 , isQid^#(n__a()) -> c_30() 896.77/297.16 , isQid^#(n__e()) -> c_31() 896.77/297.16 , isQid^#(n__i()) -> c_32() 896.77/297.16 , isQid^#(n__o()) -> c_33() 896.77/297.16 , isQid^#(n__u()) -> c_34() 896.77/297.16 , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.16 , U43^#(tt()) -> c_37() 896.77/297.16 , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.16 , U53^#(tt()) -> c_40() 896.77/297.16 , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.16 , U62^#(tt()) -> c_42() 896.77/297.16 , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.16 , U72^#(tt()) -> c_44() 896.77/297.16 , isNePal^#(V) -> 896.77/297.16 c_45(U61^#(isPalListKind(activate(V)), activate(V))) } 896.77/297.16 Obligation: 896.77/297.16 runtime complexity 896.77/297.16 Answer: 896.77/297.16 MAYBE 896.77/297.16 896.77/297.16 We estimate the number of application of {5,6,17} by applications 896.77/297.16 of Pre({5,6,17}) = {1,2,4,7,12,14,16}. Here rules are labeled as 896.77/297.16 follows: 896.77/297.16 896.77/297.16 DPs: 896.77/297.16 { 1: __^#(X1, X2) -> c_1(X1, X2) 896.77/297.16 , 2: __^#(X, nil()) -> c_2(X) 896.77/297.16 , 3: __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.16 , 4: __^#(nil(), X) -> c_4(X) 896.77/297.16 , 5: isNeList^#(n____(V1, V2)) -> 896.77/297.16 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , 6: isNeList^#(n____(V1, V2)) -> 896.77/297.16 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , 7: activate^#(X) -> c_11(X) 896.77/297.16 , 8: activate^#(n____(X1, X2)) -> 896.77/297.16 c_13(__^#(activate(X1), activate(X2))) 896.77/297.16 , 9: activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.16 , 10: activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.16 , 11: activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.16 , 12: isPalListKind^#(X) -> c_49(X) 896.77/297.16 , 13: isPalListKind^#(n____(V1, V2)) -> 896.77/297.16 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2)))) 896.77/297.16 , 14: and^#(X1, X2) -> c_47(X1, X2) 896.77/297.16 , 15: and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.16 , 16: isPal^#(X) -> c_58(X) 896.77/297.16 , 17: isList^#(n____(V1, V2)) -> 896.77/297.16 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , 18: isNePal^#(n____(I, n____(P, I))) -> 896.77/297.16 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.16 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) 896.77/297.16 , 19: nil^#() -> c_5() 896.77/297.16 , 20: U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.16 , 21: U12^#(tt()) -> c_7() 896.77/297.16 , 22: isNeList^#(V) -> 896.77/297.16 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , 23: U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.16 , 24: U41^#(tt(), V1, V2) -> 896.77/297.16 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.16 , 25: U51^#(tt(), V1, V2) -> 896.77/297.16 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.16 , 26: activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.16 , 27: activate^#(n__a()) -> c_17(a^#()) 896.77/297.16 , 28: activate^#(n__e()) -> c_18(e^#()) 896.77/297.16 , 29: activate^#(n__i()) -> c_19(i^#()) 896.77/297.16 , 30: activate^#(n__o()) -> c_20(o^#()) 896.77/297.16 , 31: activate^#(n__u()) -> c_21(u^#()) 896.77/297.16 , 32: isPalListKind^#(n__nil()) -> c_50() 896.77/297.16 , 33: isPalListKind^#(n__a()) -> c_52() 896.77/297.16 , 34: isPalListKind^#(n__e()) -> c_53() 896.77/297.16 , 35: isPalListKind^#(n__i()) -> c_54() 896.77/297.16 , 36: isPalListKind^#(n__o()) -> c_55() 896.77/297.16 , 37: isPalListKind^#(n__u()) -> c_56() 896.77/297.16 , 38: isPal^#(V) -> 896.77/297.16 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , 39: isPal^#(n__nil()) -> c_59() 896.77/297.16 , 40: a^#() -> c_60() 896.77/297.16 , 41: e^#() -> c_61() 896.77/297.16 , 42: i^#() -> c_62() 896.77/297.16 , 43: o^#() -> c_63() 896.77/297.16 , 44: u^#() -> c_64() 896.77/297.16 , 45: U21^#(tt(), V1, V2) -> 896.77/297.16 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.16 , 46: U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.16 , 47: U23^#(tt()) -> c_27() 896.77/297.16 , 48: isList^#(V) -> 896.77/297.16 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , 49: isList^#(n__nil()) -> c_25() 896.77/297.16 , 50: U32^#(tt()) -> c_29() 896.77/297.16 , 51: isQid^#(n__a()) -> c_30() 896.77/297.16 , 52: isQid^#(n__e()) -> c_31() 896.77/297.16 , 53: isQid^#(n__i()) -> c_32() 896.77/297.16 , 54: isQid^#(n__o()) -> c_33() 896.77/297.16 , 55: isQid^#(n__u()) -> c_34() 896.77/297.16 , 56: U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.16 , 57: U43^#(tt()) -> c_37() 896.77/297.16 , 58: U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.16 , 59: U53^#(tt()) -> c_40() 896.77/297.16 , 60: U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.16 , 61: U62^#(tt()) -> c_42() 896.77/297.16 , 62: U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.16 , 63: U72^#(tt()) -> c_44() 896.77/297.16 , 64: isNePal^#(V) -> 896.77/297.16 c_45(U61^#(isPalListKind(activate(V)), activate(V))) } 896.77/297.16 896.77/297.16 We are left with following problem, upon which TcT provides the 896.77/297.16 certificate MAYBE. 896.77/297.16 896.77/297.16 Strict DPs: 896.77/297.16 { __^#(X1, X2) -> c_1(X1, X2) 896.77/297.16 , __^#(X, nil()) -> c_2(X) 896.77/297.16 , __^#(__(X, Y), Z) -> c_3(__^#(X, __(Y, Z))) 896.77/297.16 , __^#(nil(), X) -> c_4(X) 896.77/297.16 , activate^#(X) -> c_11(X) 896.77/297.16 , activate^#(n____(X1, X2)) -> 896.77/297.16 c_13(__^#(activate(X1), activate(X2))) 896.77/297.16 , activate^#(n__isPalListKind(X)) -> c_14(isPalListKind^#(X)) 896.77/297.16 , activate^#(n__and(X1, X2)) -> c_15(and^#(activate(X1), X2)) 896.77/297.16 , activate^#(n__isPal(X)) -> c_16(isPal^#(X)) 896.77/297.16 , isPalListKind^#(X) -> c_49(X) 896.77/297.16 , isPalListKind^#(n____(V1, V2)) -> 896.77/297.16 c_51(and^#(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2)))) 896.77/297.16 , and^#(X1, X2) -> c_47(X1, X2) 896.77/297.16 , and^#(tt(), X) -> c_48(activate^#(X)) 896.77/297.16 , isPal^#(X) -> c_58(X) 896.77/297.16 , isNePal^#(n____(I, n____(P, I))) -> 896.77/297.16 c_46(and^#(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.16 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))) } 896.77/297.16 Strict Trs: 896.77/297.16 { __(X1, X2) -> n____(X1, X2) 896.77/297.16 , __(X, nil()) -> X 896.77/297.16 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 896.77/297.16 , __(nil(), X) -> X 896.77/297.16 , nil() -> n__nil() 896.77/297.16 , U11(tt(), V) -> U12(isNeList(activate(V))) 896.77/297.16 , U12(tt()) -> tt() 896.77/297.16 , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V)) 896.77/297.16 , isNeList(n____(V1, V2)) -> 896.77/297.16 U41(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2)) 896.77/297.16 , isNeList(n____(V1, V2)) -> 896.77/297.16 U51(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2)) 896.77/297.16 , activate(X) -> X 896.77/297.16 , activate(n__nil()) -> nil() 896.77/297.16 , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) 896.77/297.16 , activate(n__isPalListKind(X)) -> isPalListKind(X) 896.77/297.16 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 896.77/297.16 , activate(n__isPal(X)) -> isPal(X) 896.77/297.16 , activate(n__a()) -> a() 896.77/297.16 , activate(n__e()) -> e() 896.77/297.16 , activate(n__i()) -> i() 896.77/297.16 , activate(n__o()) -> o() 896.77/297.16 , activate(n__u()) -> u() 896.77/297.16 , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)) 896.77/297.16 , U22(tt(), V2) -> U23(isList(activate(V2))) 896.77/297.16 , isList(V) -> U11(isPalListKind(activate(V)), activate(V)) 896.77/297.16 , isList(n__nil()) -> tt() 896.77/297.16 , isList(n____(V1, V2)) -> 896.77/297.16 U21(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2)) 896.77/297.16 , U23(tt()) -> tt() 896.77/297.16 , U31(tt(), V) -> U32(isQid(activate(V))) 896.77/297.16 , U32(tt()) -> tt() 896.77/297.16 , isQid(n__a()) -> tt() 896.77/297.16 , isQid(n__e()) -> tt() 896.77/297.16 , isQid(n__i()) -> tt() 896.77/297.16 , isQid(n__o()) -> tt() 896.77/297.16 , isQid(n__u()) -> tt() 896.77/297.16 , U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)) 896.77/297.16 , U42(tt(), V2) -> U43(isNeList(activate(V2))) 896.77/297.16 , U43(tt()) -> tt() 896.77/297.16 , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)) 896.77/297.16 , U52(tt(), V2) -> U53(isList(activate(V2))) 896.77/297.16 , U53(tt()) -> tt() 896.77/297.16 , U61(tt(), V) -> U62(isQid(activate(V))) 896.77/297.16 , U62(tt()) -> tt() 896.77/297.16 , U71(tt(), V) -> U72(isNePal(activate(V))) 896.77/297.16 , U72(tt()) -> tt() 896.77/297.16 , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V)) 896.77/297.16 , isNePal(n____(I, n____(P, I))) -> 896.77/297.16 and(and(isQid(activate(I)), n__isPalListKind(activate(I))), 896.77/297.16 n__and(n__isPal(activate(P)), n__isPalListKind(activate(P)))) 896.77/297.16 , and(X1, X2) -> n__and(X1, X2) 896.77/297.16 , and(tt(), X) -> activate(X) 896.77/297.16 , isPalListKind(X) -> n__isPalListKind(X) 896.77/297.16 , isPalListKind(n__nil()) -> tt() 896.77/297.16 , isPalListKind(n____(V1, V2)) -> 896.77/297.16 and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) 896.77/297.16 , isPalListKind(n__a()) -> tt() 896.77/297.16 , isPalListKind(n__e()) -> tt() 896.77/297.16 , isPalListKind(n__i()) -> tt() 896.77/297.16 , isPalListKind(n__o()) -> tt() 896.77/297.16 , isPalListKind(n__u()) -> tt() 896.77/297.16 , isPal(V) -> U71(isPalListKind(activate(V)), activate(V)) 896.77/297.16 , isPal(X) -> n__isPal(X) 896.77/297.16 , isPal(n__nil()) -> tt() 896.77/297.16 , a() -> n__a() 896.77/297.16 , e() -> n__e() 896.77/297.16 , i() -> n__i() 896.77/297.16 , o() -> n__o() 896.77/297.16 , u() -> n__u() } 896.77/297.16 Weak DPs: 896.77/297.16 { nil^#() -> c_5() 896.77/297.16 , U11^#(tt(), V) -> c_6(U12^#(isNeList(activate(V)))) 896.77/297.16 , U12^#(tt()) -> c_7() 896.77/297.16 , isNeList^#(V) -> 896.77/297.16 c_8(U31^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , isNeList^#(n____(V1, V2)) -> 896.77/297.16 c_9(U41^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , isNeList^#(n____(V1, V2)) -> 896.77/297.16 c_10(U51^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , U31^#(tt(), V) -> c_28(U32^#(isQid(activate(V)))) 896.77/297.16 , U41^#(tt(), V1, V2) -> 896.77/297.16 c_35(U42^#(isList(activate(V1)), activate(V2))) 896.77/297.16 , U51^#(tt(), V1, V2) -> 896.77/297.16 c_38(U52^#(isNeList(activate(V1)), activate(V2))) 896.77/297.16 , activate^#(n__nil()) -> c_12(nil^#()) 896.77/297.16 , activate^#(n__a()) -> c_17(a^#()) 896.77/297.16 , activate^#(n__e()) -> c_18(e^#()) 896.77/297.16 , activate^#(n__i()) -> c_19(i^#()) 896.77/297.16 , activate^#(n__o()) -> c_20(o^#()) 896.77/297.16 , activate^#(n__u()) -> c_21(u^#()) 896.77/297.16 , isPalListKind^#(n__nil()) -> c_50() 896.77/297.16 , isPalListKind^#(n__a()) -> c_52() 896.77/297.16 , isPalListKind^#(n__e()) -> c_53() 896.77/297.16 , isPalListKind^#(n__i()) -> c_54() 896.77/297.16 , isPalListKind^#(n__o()) -> c_55() 896.77/297.16 , isPalListKind^#(n__u()) -> c_56() 896.77/297.16 , isPal^#(V) -> 896.77/297.16 c_57(U71^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , isPal^#(n__nil()) -> c_59() 896.77/297.16 , a^#() -> c_60() 896.77/297.16 , e^#() -> c_61() 896.77/297.16 , i^#() -> c_62() 896.77/297.16 , o^#() -> c_63() 896.77/297.16 , u^#() -> c_64() 896.77/297.16 , U21^#(tt(), V1, V2) -> 896.77/297.16 c_22(U22^#(isList(activate(V1)), activate(V2))) 896.77/297.16 , U22^#(tt(), V2) -> c_23(U23^#(isList(activate(V2)))) 896.77/297.16 , U23^#(tt()) -> c_27() 896.77/297.16 , isList^#(V) -> 896.77/297.16 c_24(U11^#(isPalListKind(activate(V)), activate(V))) 896.77/297.16 , isList^#(n__nil()) -> c_25() 896.77/297.16 , isList^#(n____(V1, V2)) -> 896.77/297.16 c_26(U21^#(and(isPalListKind(activate(V1)), 896.77/297.16 n__isPalListKind(activate(V2))), 896.77/297.16 activate(V1), 896.77/297.16 activate(V2))) 896.77/297.16 , U32^#(tt()) -> c_29() 896.77/297.16 , isQid^#(n__a()) -> c_30() 896.77/297.16 , isQid^#(n__e()) -> c_31() 896.77/297.16 , isQid^#(n__i()) -> c_32() 896.77/297.16 , isQid^#(n__o()) -> c_33() 896.77/297.16 , isQid^#(n__u()) -> c_34() 896.77/297.16 , U42^#(tt(), V2) -> c_36(U43^#(isNeList(activate(V2)))) 896.77/297.16 , U43^#(tt()) -> c_37() 896.77/297.16 , U52^#(tt(), V2) -> c_39(U53^#(isList(activate(V2)))) 896.77/297.16 , U53^#(tt()) -> c_40() 896.77/297.16 , U61^#(tt(), V) -> c_41(U62^#(isQid(activate(V)))) 896.77/297.16 , U62^#(tt()) -> c_42() 896.77/297.16 , U71^#(tt(), V) -> c_43(U72^#(isNePal(activate(V)))) 896.77/297.16 , U72^#(tt()) -> c_44() 896.77/297.16 , isNePal^#(V) -> 896.77/297.16 c_45(U61^#(isPalListKind(activate(V)), activate(V))) } 896.77/297.16 Obligation: 896.77/297.16 runtime complexity 896.77/297.16 Answer: 896.77/297.16 MAYBE 896.77/297.16 896.77/297.16 Empty strict component of the problem is NOT empty. 896.77/297.16 896.77/297.16 896.77/297.16 Arrrr.. 896.99/297.27 EOF