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