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