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