MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { active(__(X1, X2)) -> __(X1, active(X2)) , active(__(X1, X2)) -> __(active(X1), X2) , active(__(X, nil())) -> mark(X) , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(nil(), X)) -> mark(X) , active(U11(X1, X2)) -> U11(active(X1), X2) , active(U11(tt(), V)) -> mark(U12(isPalListKind(V), V)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V)) -> mark(U13(isNeList(V))) , active(isPalListKind(__(V1, V2))) -> mark(U91(isPalListKind(V1), V2)) , active(isPalListKind(nil())) -> mark(tt()) , active(isPalListKind(a())) -> mark(tt()) , active(isPalListKind(e())) -> mark(tt()) , active(isPalListKind(i())) -> mark(tt()) , active(isPalListKind(o())) -> mark(tt()) , active(isPalListKind(u())) -> mark(tt()) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) , active(isNeList(__(V1, V2))) -> mark(U41(isPalListKind(V1), V1, V2)) , active(isNeList(__(V1, V2))) -> mark(U51(isPalListKind(V1), V1, V2)) , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) , active(U21(tt(), V1, V2)) -> mark(U22(isPalListKind(V1), V1, V2)) , active(U22(X1, X2, X3)) -> U22(active(X1), X2, X3) , active(U22(tt(), V1, V2)) -> mark(U23(isPalListKind(V2), V1, V2)) , active(U23(X1, X2, X3)) -> U23(active(X1), X2, X3) , active(U23(tt(), V1, V2)) -> mark(U24(isPalListKind(V2), V1, V2)) , active(U24(X1, X2, X3)) -> U24(active(X1), X2, X3) , active(U24(tt(), V1, V2)) -> mark(U25(isList(V1), V2)) , active(U25(X1, X2)) -> U25(active(X1), X2) , active(U25(tt(), V2)) -> mark(U26(isList(V2))) , active(isList(V)) -> mark(U11(isPalListKind(V), V)) , active(isList(__(V1, V2))) -> mark(U21(isPalListKind(V1), V1, V2)) , active(isList(nil())) -> mark(tt()) , active(U26(X)) -> U26(active(X)) , active(U26(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isPalListKind(V), V)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V)) -> mark(U33(isQid(V))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(isQid(a())) -> mark(tt()) , active(isQid(e())) -> mark(tt()) , active(isQid(i())) -> mark(tt()) , active(isQid(o())) -> mark(tt()) , active(isQid(u())) -> mark(tt()) , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) , active(U41(tt(), V1, V2)) -> mark(U42(isPalListKind(V1), V1, V2)) , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) , active(U42(tt(), V1, V2)) -> mark(U43(isPalListKind(V2), V1, V2)) , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) , active(U43(tt(), V1, V2)) -> mark(U44(isPalListKind(V2), V1, V2)) , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) , active(U44(tt(), V1, V2)) -> mark(U45(isList(V1), V2)) , active(U45(X1, X2)) -> U45(active(X1), X2) , active(U45(tt(), V2)) -> mark(U46(isNeList(V2))) , active(U46(X)) -> U46(active(X)) , active(U46(tt())) -> mark(tt()) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), V1, V2)) -> mark(U52(isPalListKind(V1), V1, V2)) , active(U52(X1, X2, X3)) -> U52(active(X1), X2, X3) , active(U52(tt(), V1, V2)) -> mark(U53(isPalListKind(V2), V1, V2)) , active(U53(X1, X2, X3)) -> U53(active(X1), X2, X3) , active(U53(tt(), V1, V2)) -> mark(U54(isPalListKind(V2), V1, V2)) , active(U54(X1, X2, X3)) -> U54(active(X1), X2, X3) , active(U54(tt(), V1, V2)) -> mark(U55(isNeList(V1), V2)) , active(U55(X1, X2)) -> U55(active(X1), X2) , active(U55(tt(), V2)) -> mark(U56(isList(V2))) , active(U56(X)) -> U56(active(X)) , active(U56(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V)) -> mark(U62(isPalListKind(V), V)) , active(U62(X1, X2)) -> U62(active(X1), X2) , active(U62(tt(), V)) -> mark(U63(isQid(V))) , active(U63(X)) -> U63(active(X)) , active(U63(tt())) -> mark(tt()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), I, P)) -> mark(U72(isPalListKind(I), P)) , active(U72(X1, X2)) -> U72(active(X1), X2) , active(U72(tt(), P)) -> mark(U73(isPal(P), P)) , active(U73(X1, X2)) -> U73(active(X1), X2) , active(U73(tt(), P)) -> mark(U74(isPalListKind(P))) , active(isPal(V)) -> mark(U81(isPalListKind(V), V)) , active(isPal(nil())) -> mark(tt()) , active(U74(X)) -> U74(active(X)) , active(U74(tt())) -> mark(tt()) , active(U81(X1, X2)) -> U81(active(X1), X2) , active(U81(tt(), V)) -> mark(U82(isPalListKind(V), V)) , active(U82(X1, X2)) -> U82(active(X1), X2) , active(U82(tt(), V)) -> mark(U83(isNePal(V))) , active(U83(X)) -> U83(active(X)) , active(U83(tt())) -> mark(tt()) , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) , active(isNePal(__(I, __(P, I)))) -> mark(U71(isQid(I), I, P)) , active(U91(X1, X2)) -> U91(active(X1), X2) , active(U91(tt(), V2)) -> mark(U92(isPalListKind(V2))) , active(U92(X)) -> U92(active(X)) , active(U92(tt())) -> mark(tt()) , __(X1, mark(X2)) -> mark(__(X1, X2)) , __(mark(X1), X2) -> mark(__(X1, X2)) , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) , U11(mark(X1), X2) -> mark(U11(X1, X2)) , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , isPalListKind(ok(X)) -> ok(isPalListKind(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , isNeList(ok(X)) -> ok(isNeList(X)) , U21(mark(X1), X2, X3) -> mark(U21(X1, X2, X3)) , U21(ok(X1), ok(X2), ok(X3)) -> ok(U21(X1, X2, X3)) , U22(mark(X1), X2, X3) -> mark(U22(X1, X2, X3)) , U22(ok(X1), ok(X2), ok(X3)) -> ok(U22(X1, X2, X3)) , U23(mark(X1), X2, X3) -> mark(U23(X1, X2, X3)) , U23(ok(X1), ok(X2), ok(X3)) -> ok(U23(X1, X2, X3)) , U24(mark(X1), X2, X3) -> mark(U24(X1, X2, X3)) , U24(ok(X1), ok(X2), ok(X3)) -> ok(U24(X1, X2, X3)) , U25(mark(X1), X2) -> mark(U25(X1, X2)) , U25(ok(X1), ok(X2)) -> ok(U25(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , U26(mark(X)) -> mark(U26(X)) , U26(ok(X)) -> ok(U26(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , isQid(ok(X)) -> ok(isQid(X)) , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) , U45(mark(X1), X2) -> mark(U45(X1, X2)) , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) , U46(mark(X)) -> mark(U46(X)) , U46(ok(X)) -> ok(U46(X)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , U52(mark(X1), X2, X3) -> mark(U52(X1, X2, X3)) , U52(ok(X1), ok(X2), ok(X3)) -> ok(U52(X1, X2, X3)) , U53(mark(X1), X2, X3) -> mark(U53(X1, X2, X3)) , U53(ok(X1), ok(X2), ok(X3)) -> ok(U53(X1, X2, X3)) , U54(mark(X1), X2, X3) -> mark(U54(X1, X2, X3)) , U54(ok(X1), ok(X2), ok(X3)) -> ok(U54(X1, X2, X3)) , U55(mark(X1), X2) -> mark(U55(X1, X2)) , U55(ok(X1), ok(X2)) -> ok(U55(X1, X2)) , U56(mark(X)) -> mark(U56(X)) , U56(ok(X)) -> ok(U56(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X1), X2) -> mark(U62(X1, X2)) , U62(ok(X1), ok(X2)) -> ok(U62(X1, X2)) , U63(mark(X)) -> mark(U63(X)) , U63(ok(X)) -> ok(U63(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , U72(mark(X1), X2) -> mark(U72(X1, X2)) , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) , U73(mark(X1), X2) -> mark(U73(X1, X2)) , U73(ok(X1), ok(X2)) -> ok(U73(X1, X2)) , isPal(ok(X)) -> ok(isPal(X)) , U74(mark(X)) -> mark(U74(X)) , U74(ok(X)) -> ok(U74(X)) , U81(mark(X1), X2) -> mark(U81(X1, X2)) , U81(ok(X1), ok(X2)) -> ok(U81(X1, X2)) , U82(mark(X1), X2) -> mark(U82(X1, X2)) , U82(ok(X1), ok(X2)) -> ok(U82(X1, X2)) , U83(mark(X)) -> mark(U83(X)) , U83(ok(X)) -> ok(U83(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , U91(mark(X1), X2) -> mark(U91(X1, X2)) , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) , U92(mark(X)) -> mark(U92(X)) , U92(ok(X)) -> ok(U92(X)) , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) , proper(tt()) -> ok(tt()) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(isPalListKind(X)) -> isPalListKind(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(U21(X1, X2, X3)) -> U21(proper(X1), proper(X2), proper(X3)) , proper(U22(X1, X2, X3)) -> U22(proper(X1), proper(X2), proper(X3)) , proper(U23(X1, X2, X3)) -> U23(proper(X1), proper(X2), proper(X3)) , proper(U24(X1, X2, X3)) -> U24(proper(X1), proper(X2), proper(X3)) , proper(U25(X1, X2)) -> U25(proper(X1), proper(X2)) , proper(isList(X)) -> isList(proper(X)) , proper(U26(X)) -> U26(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2, X3)) -> U42(proper(X1), proper(X2), proper(X3)) , proper(U43(X1, X2, X3)) -> U43(proper(X1), proper(X2), proper(X3)) , proper(U44(X1, X2, X3)) -> U44(proper(X1), proper(X2), proper(X3)) , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) , proper(U46(X)) -> U46(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(U52(X1, X2, X3)) -> U52(proper(X1), proper(X2), proper(X3)) , proper(U53(X1, X2, X3)) -> U53(proper(X1), proper(X2), proper(X3)) , proper(U54(X1, X2, X3)) -> U54(proper(X1), proper(X2), proper(X3)) , proper(U55(X1, X2)) -> U55(proper(X1), proper(X2)) , proper(U56(X)) -> U56(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X1, X2)) -> U62(proper(X1), proper(X2)) , proper(U63(X)) -> U63(proper(X)) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) , proper(U73(X1, X2)) -> U73(proper(X1), proper(X2)) , proper(isPal(X)) -> isPal(proper(X)) , proper(U74(X)) -> U74(proper(X)) , proper(U81(X1, X2)) -> U81(proper(X1), proper(X2)) , proper(U82(X1, X2)) -> U82(proper(X1), proper(X2)) , proper(U83(X)) -> U83(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) , proper(U92(X)) -> U92(proper(X)) , proper(a()) -> ok(a()) , proper(e()) -> ok(e()) , proper(i()) -> ok(i()) , proper(o()) -> ok(o()) , proper(u()) -> ok(u()) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) , active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) , active^#(__(X, nil())) -> c_3(X) , active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) , active^#(__(nil(), X)) -> c_5(X) , active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) , active^#(U11(tt(), V)) -> c_7(U12^#(isPalListKind(V), V)) , active^#(U12(X1, X2)) -> c_8(U12^#(active(X1), X2)) , active^#(U12(tt(), V)) -> c_9(U13^#(isNeList(V))) , active^#(isPalListKind(__(V1, V2))) -> c_10(U91^#(isPalListKind(V1), V2)) , active^#(isPalListKind(nil())) -> c_11() , active^#(isPalListKind(a())) -> c_12() , active^#(isPalListKind(e())) -> c_13() , active^#(isPalListKind(i())) -> c_14() , active^#(isPalListKind(o())) -> c_15() , active^#(isPalListKind(u())) -> c_16() , active^#(U13(X)) -> c_17(U13^#(active(X))) , active^#(U13(tt())) -> c_18() , active^#(isNeList(V)) -> c_19(U31^#(isPalListKind(V), V)) , active^#(isNeList(__(V1, V2))) -> c_20(U41^#(isPalListKind(V1), V1, V2)) , active^#(isNeList(__(V1, V2))) -> c_21(U51^#(isPalListKind(V1), V1, V2)) , active^#(U21(X1, X2, X3)) -> c_22(U21^#(active(X1), X2, X3)) , active^#(U21(tt(), V1, V2)) -> c_23(U22^#(isPalListKind(V1), V1, V2)) , active^#(U22(X1, X2, X3)) -> c_24(U22^#(active(X1), X2, X3)) , active^#(U22(tt(), V1, V2)) -> c_25(U23^#(isPalListKind(V2), V1, V2)) , active^#(U23(X1, X2, X3)) -> c_26(U23^#(active(X1), X2, X3)) , active^#(U23(tt(), V1, V2)) -> c_27(U24^#(isPalListKind(V2), V1, V2)) , active^#(U24(X1, X2, X3)) -> c_28(U24^#(active(X1), X2, X3)) , active^#(U24(tt(), V1, V2)) -> c_29(U25^#(isList(V1), V2)) , active^#(U25(X1, X2)) -> c_30(U25^#(active(X1), X2)) , active^#(U25(tt(), V2)) -> c_31(U26^#(isList(V2))) , active^#(isList(V)) -> c_32(U11^#(isPalListKind(V), V)) , active^#(isList(__(V1, V2))) -> c_33(U21^#(isPalListKind(V1), V1, V2)) , active^#(isList(nil())) -> c_34() , active^#(U26(X)) -> c_35(U26^#(active(X))) , active^#(U26(tt())) -> c_36() , active^#(U31(X1, X2)) -> c_37(U31^#(active(X1), X2)) , active^#(U31(tt(), V)) -> c_38(U32^#(isPalListKind(V), V)) , active^#(U32(X1, X2)) -> c_39(U32^#(active(X1), X2)) , active^#(U32(tt(), V)) -> c_40(U33^#(isQid(V))) , active^#(U33(X)) -> c_41(U33^#(active(X))) , active^#(U33(tt())) -> c_42() , active^#(isQid(a())) -> c_43() , active^#(isQid(e())) -> c_44() , active^#(isQid(i())) -> c_45() , active^#(isQid(o())) -> c_46() , active^#(isQid(u())) -> c_47() , active^#(U41(X1, X2, X3)) -> c_48(U41^#(active(X1), X2, X3)) , active^#(U41(tt(), V1, V2)) -> c_49(U42^#(isPalListKind(V1), V1, V2)) , active^#(U42(X1, X2, X3)) -> c_50(U42^#(active(X1), X2, X3)) , active^#(U42(tt(), V1, V2)) -> c_51(U43^#(isPalListKind(V2), V1, V2)) , active^#(U43(X1, X2, X3)) -> c_52(U43^#(active(X1), X2, X3)) , active^#(U43(tt(), V1, V2)) -> c_53(U44^#(isPalListKind(V2), V1, V2)) , active^#(U44(X1, X2, X3)) -> c_54(U44^#(active(X1), X2, X3)) , active^#(U44(tt(), V1, V2)) -> c_55(U45^#(isList(V1), V2)) , active^#(U45(X1, X2)) -> c_56(U45^#(active(X1), X2)) , active^#(U45(tt(), V2)) -> c_57(U46^#(isNeList(V2))) , active^#(U46(X)) -> c_58(U46^#(active(X))) , active^#(U46(tt())) -> c_59() , active^#(U51(X1, X2, X3)) -> c_60(U51^#(active(X1), X2, X3)) , active^#(U51(tt(), V1, V2)) -> c_61(U52^#(isPalListKind(V1), V1, V2)) , active^#(U52(X1, X2, X3)) -> c_62(U52^#(active(X1), X2, X3)) , active^#(U52(tt(), V1, V2)) -> c_63(U53^#(isPalListKind(V2), V1, V2)) , active^#(U53(X1, X2, X3)) -> c_64(U53^#(active(X1), X2, X3)) , active^#(U53(tt(), V1, V2)) -> c_65(U54^#(isPalListKind(V2), V1, V2)) , active^#(U54(X1, X2, X3)) -> c_66(U54^#(active(X1), X2, X3)) , active^#(U54(tt(), V1, V2)) -> c_67(U55^#(isNeList(V1), V2)) , active^#(U55(X1, X2)) -> c_68(U55^#(active(X1), X2)) , active^#(U55(tt(), V2)) -> c_69(U56^#(isList(V2))) , active^#(U56(X)) -> c_70(U56^#(active(X))) , active^#(U56(tt())) -> c_71() , active^#(U61(X1, X2)) -> c_72(U61^#(active(X1), X2)) , active^#(U61(tt(), V)) -> c_73(U62^#(isPalListKind(V), V)) , active^#(U62(X1, X2)) -> c_74(U62^#(active(X1), X2)) , active^#(U62(tt(), V)) -> c_75(U63^#(isQid(V))) , active^#(U63(X)) -> c_76(U63^#(active(X))) , active^#(U63(tt())) -> c_77() , active^#(U71(X1, X2, X3)) -> c_78(U71^#(active(X1), X2, X3)) , active^#(U71(tt(), I, P)) -> c_79(U72^#(isPalListKind(I), P)) , active^#(U72(X1, X2)) -> c_80(U72^#(active(X1), X2)) , active^#(U72(tt(), P)) -> c_81(U73^#(isPal(P), P)) , active^#(U73(X1, X2)) -> c_82(U73^#(active(X1), X2)) , active^#(U73(tt(), P)) -> c_83(U74^#(isPalListKind(P))) , active^#(isPal(V)) -> c_84(U81^#(isPalListKind(V), V)) , active^#(isPal(nil())) -> c_85() , active^#(U74(X)) -> c_86(U74^#(active(X))) , active^#(U74(tt())) -> c_87() , active^#(U81(X1, X2)) -> c_88(U81^#(active(X1), X2)) , active^#(U81(tt(), V)) -> c_89(U82^#(isPalListKind(V), V)) , active^#(U82(X1, X2)) -> c_90(U82^#(active(X1), X2)) , active^#(U82(tt(), V)) -> c_91(U83^#(isNePal(V))) , active^#(U83(X)) -> c_92(U83^#(active(X))) , active^#(U83(tt())) -> c_93() , active^#(isNePal(V)) -> c_94(U61^#(isPalListKind(V), V)) , active^#(isNePal(__(I, __(P, I)))) -> c_95(U71^#(isQid(I), I, P)) , active^#(U91(X1, X2)) -> c_96(U91^#(active(X1), X2)) , active^#(U91(tt(), V2)) -> c_97(U92^#(isPalListKind(V2))) , active^#(U92(X)) -> c_98(U92^#(active(X))) , active^#(U92(tt())) -> c_99() , __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) , __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) , __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) , U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) , U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) , U13^#(mark(X)) -> c_108(U13^#(X)) , U13^#(ok(X)) -> c_109(U13^#(X)) , U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) , U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) , U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) , U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) , U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) , U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) , U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) , U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) , U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) , U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) , U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) , U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) , U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) , U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) , U26^#(mark(X)) -> c_122(U26^#(X)) , U26^#(ok(X)) -> c_123(U26^#(X)) , U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) , U33^#(mark(X)) -> c_128(U33^#(X)) , U33^#(ok(X)) -> c_129(U33^#(X)) , U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) , U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) , U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) , U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) , U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) , U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) , U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) , U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) , U46^#(mark(X)) -> c_141(U46^#(X)) , U46^#(ok(X)) -> c_142(U46^#(X)) , U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) , U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) , U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) , U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) , U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) , U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) , U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) , U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) , U56^#(mark(X)) -> c_153(U56^#(X)) , U56^#(ok(X)) -> c_154(U56^#(X)) , U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) , U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) , U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) , U63^#(mark(X)) -> c_159(U63^#(X)) , U63^#(ok(X)) -> c_160(U63^#(X)) , U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) , U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) , U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) , U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) , U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) , U74^#(mark(X)) -> c_168(U74^#(X)) , U74^#(ok(X)) -> c_169(U74^#(X)) , U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) , U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) , U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) , U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) , U83^#(mark(X)) -> c_174(U83^#(X)) , U83^#(ok(X)) -> c_175(U83^#(X)) , U92^#(mark(X)) -> c_179(U92^#(X)) , U92^#(ok(X)) -> c_180(U92^#(X)) , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , isNeList^#(ok(X)) -> c_110(isNeList^#(X)) , isList^#(ok(X)) -> c_121(isList^#(X)) , isQid^#(ok(X)) -> c_130(isQid^#(X)) , isPal^#(ok(X)) -> c_167(isPal^#(X)) , isNePal^#(ok(X)) -> c_176(isNePal^#(X)) , proper^#(__(X1, X2)) -> c_181(__^#(proper(X1), proper(X2))) , proper^#(nil()) -> c_182() , proper^#(U11(X1, X2)) -> c_183(U11^#(proper(X1), proper(X2))) , proper^#(tt()) -> c_184() , proper^#(U12(X1, X2)) -> c_185(U12^#(proper(X1), proper(X2))) , proper^#(isPalListKind(X)) -> c_186(isPalListKind^#(proper(X))) , proper^#(U13(X)) -> c_187(U13^#(proper(X))) , proper^#(isNeList(X)) -> c_188(isNeList^#(proper(X))) , proper^#(U21(X1, X2, X3)) -> c_189(U21^#(proper(X1), proper(X2), proper(X3))) , proper^#(U22(X1, X2, X3)) -> c_190(U22^#(proper(X1), proper(X2), proper(X3))) , proper^#(U23(X1, X2, X3)) -> c_191(U23^#(proper(X1), proper(X2), proper(X3))) , proper^#(U24(X1, X2, X3)) -> c_192(U24^#(proper(X1), proper(X2), proper(X3))) , proper^#(U25(X1, X2)) -> c_193(U25^#(proper(X1), proper(X2))) , proper^#(isList(X)) -> c_194(isList^#(proper(X))) , proper^#(U26(X)) -> c_195(U26^#(proper(X))) , proper^#(U31(X1, X2)) -> c_196(U31^#(proper(X1), proper(X2))) , proper^#(U32(X1, X2)) -> c_197(U32^#(proper(X1), proper(X2))) , proper^#(U33(X)) -> c_198(U33^#(proper(X))) , proper^#(isQid(X)) -> c_199(isQid^#(proper(X))) , proper^#(U41(X1, X2, X3)) -> c_200(U41^#(proper(X1), proper(X2), proper(X3))) , proper^#(U42(X1, X2, X3)) -> c_201(U42^#(proper(X1), proper(X2), proper(X3))) , proper^#(U43(X1, X2, X3)) -> c_202(U43^#(proper(X1), proper(X2), proper(X3))) , proper^#(U44(X1, X2, X3)) -> c_203(U44^#(proper(X1), proper(X2), proper(X3))) , proper^#(U45(X1, X2)) -> c_204(U45^#(proper(X1), proper(X2))) , proper^#(U46(X)) -> c_205(U46^#(proper(X))) , proper^#(U51(X1, X2, X3)) -> c_206(U51^#(proper(X1), proper(X2), proper(X3))) , proper^#(U52(X1, X2, X3)) -> c_207(U52^#(proper(X1), proper(X2), proper(X3))) , proper^#(U53(X1, X2, X3)) -> c_208(U53^#(proper(X1), proper(X2), proper(X3))) , proper^#(U54(X1, X2, X3)) -> c_209(U54^#(proper(X1), proper(X2), proper(X3))) , proper^#(U55(X1, X2)) -> c_210(U55^#(proper(X1), proper(X2))) , proper^#(U56(X)) -> c_211(U56^#(proper(X))) , proper^#(U61(X1, X2)) -> c_212(U61^#(proper(X1), proper(X2))) , proper^#(U62(X1, X2)) -> c_213(U62^#(proper(X1), proper(X2))) , proper^#(U63(X)) -> c_214(U63^#(proper(X))) , proper^#(U71(X1, X2, X3)) -> c_215(U71^#(proper(X1), proper(X2), proper(X3))) , proper^#(U72(X1, X2)) -> c_216(U72^#(proper(X1), proper(X2))) , proper^#(U73(X1, X2)) -> c_217(U73^#(proper(X1), proper(X2))) , proper^#(isPal(X)) -> c_218(isPal^#(proper(X))) , proper^#(U74(X)) -> c_219(U74^#(proper(X))) , proper^#(U81(X1, X2)) -> c_220(U81^#(proper(X1), proper(X2))) , proper^#(U82(X1, X2)) -> c_221(U82^#(proper(X1), proper(X2))) , proper^#(U83(X)) -> c_222(U83^#(proper(X))) , proper^#(isNePal(X)) -> c_223(isNePal^#(proper(X))) , proper^#(U91(X1, X2)) -> c_224(U91^#(proper(X1), proper(X2))) , proper^#(U92(X)) -> c_225(U92^#(proper(X))) , proper^#(a()) -> c_226() , proper^#(e()) -> c_227() , proper^#(i()) -> c_228() , proper^#(o()) -> c_229() , proper^#(u()) -> c_230() , top^#(mark(X)) -> c_231(top^#(proper(X))) , top^#(ok(X)) -> c_232(top^#(active(X))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) , active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) , active^#(__(X, nil())) -> c_3(X) , active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) , active^#(__(nil(), X)) -> c_5(X) , active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) , active^#(U11(tt(), V)) -> c_7(U12^#(isPalListKind(V), V)) , active^#(U12(X1, X2)) -> c_8(U12^#(active(X1), X2)) , active^#(U12(tt(), V)) -> c_9(U13^#(isNeList(V))) , active^#(isPalListKind(__(V1, V2))) -> c_10(U91^#(isPalListKind(V1), V2)) , active^#(isPalListKind(nil())) -> c_11() , active^#(isPalListKind(a())) -> c_12() , active^#(isPalListKind(e())) -> c_13() , active^#(isPalListKind(i())) -> c_14() , active^#(isPalListKind(o())) -> c_15() , active^#(isPalListKind(u())) -> c_16() , active^#(U13(X)) -> c_17(U13^#(active(X))) , active^#(U13(tt())) -> c_18() , active^#(isNeList(V)) -> c_19(U31^#(isPalListKind(V), V)) , active^#(isNeList(__(V1, V2))) -> c_20(U41^#(isPalListKind(V1), V1, V2)) , active^#(isNeList(__(V1, V2))) -> c_21(U51^#(isPalListKind(V1), V1, V2)) , active^#(U21(X1, X2, X3)) -> c_22(U21^#(active(X1), X2, X3)) , active^#(U21(tt(), V1, V2)) -> c_23(U22^#(isPalListKind(V1), V1, V2)) , active^#(U22(X1, X2, X3)) -> c_24(U22^#(active(X1), X2, X3)) , active^#(U22(tt(), V1, V2)) -> c_25(U23^#(isPalListKind(V2), V1, V2)) , active^#(U23(X1, X2, X3)) -> c_26(U23^#(active(X1), X2, X3)) , active^#(U23(tt(), V1, V2)) -> c_27(U24^#(isPalListKind(V2), V1, V2)) , active^#(U24(X1, X2, X3)) -> c_28(U24^#(active(X1), X2, X3)) , active^#(U24(tt(), V1, V2)) -> c_29(U25^#(isList(V1), V2)) , active^#(U25(X1, X2)) -> c_30(U25^#(active(X1), X2)) , active^#(U25(tt(), V2)) -> c_31(U26^#(isList(V2))) , active^#(isList(V)) -> c_32(U11^#(isPalListKind(V), V)) , active^#(isList(__(V1, V2))) -> c_33(U21^#(isPalListKind(V1), V1, V2)) , active^#(isList(nil())) -> c_34() , active^#(U26(X)) -> c_35(U26^#(active(X))) , active^#(U26(tt())) -> c_36() , active^#(U31(X1, X2)) -> c_37(U31^#(active(X1), X2)) , active^#(U31(tt(), V)) -> c_38(U32^#(isPalListKind(V), V)) , active^#(U32(X1, X2)) -> c_39(U32^#(active(X1), X2)) , active^#(U32(tt(), V)) -> c_40(U33^#(isQid(V))) , active^#(U33(X)) -> c_41(U33^#(active(X))) , active^#(U33(tt())) -> c_42() , active^#(isQid(a())) -> c_43() , active^#(isQid(e())) -> c_44() , active^#(isQid(i())) -> c_45() , active^#(isQid(o())) -> c_46() , active^#(isQid(u())) -> c_47() , active^#(U41(X1, X2, X3)) -> c_48(U41^#(active(X1), X2, X3)) , active^#(U41(tt(), V1, V2)) -> c_49(U42^#(isPalListKind(V1), V1, V2)) , active^#(U42(X1, X2, X3)) -> c_50(U42^#(active(X1), X2, X3)) , active^#(U42(tt(), V1, V2)) -> c_51(U43^#(isPalListKind(V2), V1, V2)) , active^#(U43(X1, X2, X3)) -> c_52(U43^#(active(X1), X2, X3)) , active^#(U43(tt(), V1, V2)) -> c_53(U44^#(isPalListKind(V2), V1, V2)) , active^#(U44(X1, X2, X3)) -> c_54(U44^#(active(X1), X2, X3)) , active^#(U44(tt(), V1, V2)) -> c_55(U45^#(isList(V1), V2)) , active^#(U45(X1, X2)) -> c_56(U45^#(active(X1), X2)) , active^#(U45(tt(), V2)) -> c_57(U46^#(isNeList(V2))) , active^#(U46(X)) -> c_58(U46^#(active(X))) , active^#(U46(tt())) -> c_59() , active^#(U51(X1, X2, X3)) -> c_60(U51^#(active(X1), X2, X3)) , active^#(U51(tt(), V1, V2)) -> c_61(U52^#(isPalListKind(V1), V1, V2)) , active^#(U52(X1, X2, X3)) -> c_62(U52^#(active(X1), X2, X3)) , active^#(U52(tt(), V1, V2)) -> c_63(U53^#(isPalListKind(V2), V1, V2)) , active^#(U53(X1, X2, X3)) -> c_64(U53^#(active(X1), X2, X3)) , active^#(U53(tt(), V1, V2)) -> c_65(U54^#(isPalListKind(V2), V1, V2)) , active^#(U54(X1, X2, X3)) -> c_66(U54^#(active(X1), X2, X3)) , active^#(U54(tt(), V1, V2)) -> c_67(U55^#(isNeList(V1), V2)) , active^#(U55(X1, X2)) -> c_68(U55^#(active(X1), X2)) , active^#(U55(tt(), V2)) -> c_69(U56^#(isList(V2))) , active^#(U56(X)) -> c_70(U56^#(active(X))) , active^#(U56(tt())) -> c_71() , active^#(U61(X1, X2)) -> c_72(U61^#(active(X1), X2)) , active^#(U61(tt(), V)) -> c_73(U62^#(isPalListKind(V), V)) , active^#(U62(X1, X2)) -> c_74(U62^#(active(X1), X2)) , active^#(U62(tt(), V)) -> c_75(U63^#(isQid(V))) , active^#(U63(X)) -> c_76(U63^#(active(X))) , active^#(U63(tt())) -> c_77() , active^#(U71(X1, X2, X3)) -> c_78(U71^#(active(X1), X2, X3)) , active^#(U71(tt(), I, P)) -> c_79(U72^#(isPalListKind(I), P)) , active^#(U72(X1, X2)) -> c_80(U72^#(active(X1), X2)) , active^#(U72(tt(), P)) -> c_81(U73^#(isPal(P), P)) , active^#(U73(X1, X2)) -> c_82(U73^#(active(X1), X2)) , active^#(U73(tt(), P)) -> c_83(U74^#(isPalListKind(P))) , active^#(isPal(V)) -> c_84(U81^#(isPalListKind(V), V)) , active^#(isPal(nil())) -> c_85() , active^#(U74(X)) -> c_86(U74^#(active(X))) , active^#(U74(tt())) -> c_87() , active^#(U81(X1, X2)) -> c_88(U81^#(active(X1), X2)) , active^#(U81(tt(), V)) -> c_89(U82^#(isPalListKind(V), V)) , active^#(U82(X1, X2)) -> c_90(U82^#(active(X1), X2)) , active^#(U82(tt(), V)) -> c_91(U83^#(isNePal(V))) , active^#(U83(X)) -> c_92(U83^#(active(X))) , active^#(U83(tt())) -> c_93() , active^#(isNePal(V)) -> c_94(U61^#(isPalListKind(V), V)) , active^#(isNePal(__(I, __(P, I)))) -> c_95(U71^#(isQid(I), I, P)) , active^#(U91(X1, X2)) -> c_96(U91^#(active(X1), X2)) , active^#(U91(tt(), V2)) -> c_97(U92^#(isPalListKind(V2))) , active^#(U92(X)) -> c_98(U92^#(active(X))) , active^#(U92(tt())) -> c_99() , __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) , __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) , __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) , U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) , U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) , U13^#(mark(X)) -> c_108(U13^#(X)) , U13^#(ok(X)) -> c_109(U13^#(X)) , U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) , U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) , U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) , U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) , U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) , U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) , U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) , U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) , U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) , U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) , U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) , U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) , U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) , U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) , U26^#(mark(X)) -> c_122(U26^#(X)) , U26^#(ok(X)) -> c_123(U26^#(X)) , U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) , U33^#(mark(X)) -> c_128(U33^#(X)) , U33^#(ok(X)) -> c_129(U33^#(X)) , U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) , U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) , U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) , U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) , U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) , U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) , U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) , U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) , U46^#(mark(X)) -> c_141(U46^#(X)) , U46^#(ok(X)) -> c_142(U46^#(X)) , U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) , U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) , U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) , U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) , U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) , U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) , U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) , U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) , U56^#(mark(X)) -> c_153(U56^#(X)) , U56^#(ok(X)) -> c_154(U56^#(X)) , U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) , U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) , U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) , U63^#(mark(X)) -> c_159(U63^#(X)) , U63^#(ok(X)) -> c_160(U63^#(X)) , U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) , U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) , U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) , U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) , U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) , U74^#(mark(X)) -> c_168(U74^#(X)) , U74^#(ok(X)) -> c_169(U74^#(X)) , U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) , U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) , U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) , U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) , U83^#(mark(X)) -> c_174(U83^#(X)) , U83^#(ok(X)) -> c_175(U83^#(X)) , U92^#(mark(X)) -> c_179(U92^#(X)) , U92^#(ok(X)) -> c_180(U92^#(X)) , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , isNeList^#(ok(X)) -> c_110(isNeList^#(X)) , isList^#(ok(X)) -> c_121(isList^#(X)) , isQid^#(ok(X)) -> c_130(isQid^#(X)) , isPal^#(ok(X)) -> c_167(isPal^#(X)) , isNePal^#(ok(X)) -> c_176(isNePal^#(X)) , proper^#(__(X1, X2)) -> c_181(__^#(proper(X1), proper(X2))) , proper^#(nil()) -> c_182() , proper^#(U11(X1, X2)) -> c_183(U11^#(proper(X1), proper(X2))) , proper^#(tt()) -> c_184() , proper^#(U12(X1, X2)) -> c_185(U12^#(proper(X1), proper(X2))) , proper^#(isPalListKind(X)) -> c_186(isPalListKind^#(proper(X))) , proper^#(U13(X)) -> c_187(U13^#(proper(X))) , proper^#(isNeList(X)) -> c_188(isNeList^#(proper(X))) , proper^#(U21(X1, X2, X3)) -> c_189(U21^#(proper(X1), proper(X2), proper(X3))) , proper^#(U22(X1, X2, X3)) -> c_190(U22^#(proper(X1), proper(X2), proper(X3))) , proper^#(U23(X1, X2, X3)) -> c_191(U23^#(proper(X1), proper(X2), proper(X3))) , proper^#(U24(X1, X2, X3)) -> c_192(U24^#(proper(X1), proper(X2), proper(X3))) , proper^#(U25(X1, X2)) -> c_193(U25^#(proper(X1), proper(X2))) , proper^#(isList(X)) -> c_194(isList^#(proper(X))) , proper^#(U26(X)) -> c_195(U26^#(proper(X))) , proper^#(U31(X1, X2)) -> c_196(U31^#(proper(X1), proper(X2))) , proper^#(U32(X1, X2)) -> c_197(U32^#(proper(X1), proper(X2))) , proper^#(U33(X)) -> c_198(U33^#(proper(X))) , proper^#(isQid(X)) -> c_199(isQid^#(proper(X))) , proper^#(U41(X1, X2, X3)) -> c_200(U41^#(proper(X1), proper(X2), proper(X3))) , proper^#(U42(X1, X2, X3)) -> c_201(U42^#(proper(X1), proper(X2), proper(X3))) , proper^#(U43(X1, X2, X3)) -> c_202(U43^#(proper(X1), proper(X2), proper(X3))) , proper^#(U44(X1, X2, X3)) -> c_203(U44^#(proper(X1), proper(X2), proper(X3))) , proper^#(U45(X1, X2)) -> c_204(U45^#(proper(X1), proper(X2))) , proper^#(U46(X)) -> c_205(U46^#(proper(X))) , proper^#(U51(X1, X2, X3)) -> c_206(U51^#(proper(X1), proper(X2), proper(X3))) , proper^#(U52(X1, X2, X3)) -> c_207(U52^#(proper(X1), proper(X2), proper(X3))) , proper^#(U53(X1, X2, X3)) -> c_208(U53^#(proper(X1), proper(X2), proper(X3))) , proper^#(U54(X1, X2, X3)) -> c_209(U54^#(proper(X1), proper(X2), proper(X3))) , proper^#(U55(X1, X2)) -> c_210(U55^#(proper(X1), proper(X2))) , proper^#(U56(X)) -> c_211(U56^#(proper(X))) , proper^#(U61(X1, X2)) -> c_212(U61^#(proper(X1), proper(X2))) , proper^#(U62(X1, X2)) -> c_213(U62^#(proper(X1), proper(X2))) , proper^#(U63(X)) -> c_214(U63^#(proper(X))) , proper^#(U71(X1, X2, X3)) -> c_215(U71^#(proper(X1), proper(X2), proper(X3))) , proper^#(U72(X1, X2)) -> c_216(U72^#(proper(X1), proper(X2))) , proper^#(U73(X1, X2)) -> c_217(U73^#(proper(X1), proper(X2))) , proper^#(isPal(X)) -> c_218(isPal^#(proper(X))) , proper^#(U74(X)) -> c_219(U74^#(proper(X))) , proper^#(U81(X1, X2)) -> c_220(U81^#(proper(X1), proper(X2))) , proper^#(U82(X1, X2)) -> c_221(U82^#(proper(X1), proper(X2))) , proper^#(U83(X)) -> c_222(U83^#(proper(X))) , proper^#(isNePal(X)) -> c_223(isNePal^#(proper(X))) , proper^#(U91(X1, X2)) -> c_224(U91^#(proper(X1), proper(X2))) , proper^#(U92(X)) -> c_225(U92^#(proper(X))) , proper^#(a()) -> c_226() , proper^#(e()) -> c_227() , proper^#(i()) -> c_228() , proper^#(o()) -> c_229() , proper^#(u()) -> c_230() , top^#(mark(X)) -> c_231(top^#(proper(X))) , top^#(ok(X)) -> c_232(top^#(active(X))) } Strict Trs: { active(__(X1, X2)) -> __(X1, active(X2)) , active(__(X1, X2)) -> __(active(X1), X2) , active(__(X, nil())) -> mark(X) , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(nil(), X)) -> mark(X) , active(U11(X1, X2)) -> U11(active(X1), X2) , active(U11(tt(), V)) -> mark(U12(isPalListKind(V), V)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V)) -> mark(U13(isNeList(V))) , active(isPalListKind(__(V1, V2))) -> mark(U91(isPalListKind(V1), V2)) , active(isPalListKind(nil())) -> mark(tt()) , active(isPalListKind(a())) -> mark(tt()) , active(isPalListKind(e())) -> mark(tt()) , active(isPalListKind(i())) -> mark(tt()) , active(isPalListKind(o())) -> mark(tt()) , active(isPalListKind(u())) -> mark(tt()) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) , active(isNeList(__(V1, V2))) -> mark(U41(isPalListKind(V1), V1, V2)) , active(isNeList(__(V1, V2))) -> mark(U51(isPalListKind(V1), V1, V2)) , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) , active(U21(tt(), V1, V2)) -> mark(U22(isPalListKind(V1), V1, V2)) , active(U22(X1, X2, X3)) -> U22(active(X1), X2, X3) , active(U22(tt(), V1, V2)) -> mark(U23(isPalListKind(V2), V1, V2)) , active(U23(X1, X2, X3)) -> U23(active(X1), X2, X3) , active(U23(tt(), V1, V2)) -> mark(U24(isPalListKind(V2), V1, V2)) , active(U24(X1, X2, X3)) -> U24(active(X1), X2, X3) , active(U24(tt(), V1, V2)) -> mark(U25(isList(V1), V2)) , active(U25(X1, X2)) -> U25(active(X1), X2) , active(U25(tt(), V2)) -> mark(U26(isList(V2))) , active(isList(V)) -> mark(U11(isPalListKind(V), V)) , active(isList(__(V1, V2))) -> mark(U21(isPalListKind(V1), V1, V2)) , active(isList(nil())) -> mark(tt()) , active(U26(X)) -> U26(active(X)) , active(U26(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isPalListKind(V), V)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V)) -> mark(U33(isQid(V))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(isQid(a())) -> mark(tt()) , active(isQid(e())) -> mark(tt()) , active(isQid(i())) -> mark(tt()) , active(isQid(o())) -> mark(tt()) , active(isQid(u())) -> mark(tt()) , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) , active(U41(tt(), V1, V2)) -> mark(U42(isPalListKind(V1), V1, V2)) , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) , active(U42(tt(), V1, V2)) -> mark(U43(isPalListKind(V2), V1, V2)) , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) , active(U43(tt(), V1, V2)) -> mark(U44(isPalListKind(V2), V1, V2)) , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) , active(U44(tt(), V1, V2)) -> mark(U45(isList(V1), V2)) , active(U45(X1, X2)) -> U45(active(X1), X2) , active(U45(tt(), V2)) -> mark(U46(isNeList(V2))) , active(U46(X)) -> U46(active(X)) , active(U46(tt())) -> mark(tt()) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), V1, V2)) -> mark(U52(isPalListKind(V1), V1, V2)) , active(U52(X1, X2, X3)) -> U52(active(X1), X2, X3) , active(U52(tt(), V1, V2)) -> mark(U53(isPalListKind(V2), V1, V2)) , active(U53(X1, X2, X3)) -> U53(active(X1), X2, X3) , active(U53(tt(), V1, V2)) -> mark(U54(isPalListKind(V2), V1, V2)) , active(U54(X1, X2, X3)) -> U54(active(X1), X2, X3) , active(U54(tt(), V1, V2)) -> mark(U55(isNeList(V1), V2)) , active(U55(X1, X2)) -> U55(active(X1), X2) , active(U55(tt(), V2)) -> mark(U56(isList(V2))) , active(U56(X)) -> U56(active(X)) , active(U56(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V)) -> mark(U62(isPalListKind(V), V)) , active(U62(X1, X2)) -> U62(active(X1), X2) , active(U62(tt(), V)) -> mark(U63(isQid(V))) , active(U63(X)) -> U63(active(X)) , active(U63(tt())) -> mark(tt()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), I, P)) -> mark(U72(isPalListKind(I), P)) , active(U72(X1, X2)) -> U72(active(X1), X2) , active(U72(tt(), P)) -> mark(U73(isPal(P), P)) , active(U73(X1, X2)) -> U73(active(X1), X2) , active(U73(tt(), P)) -> mark(U74(isPalListKind(P))) , active(isPal(V)) -> mark(U81(isPalListKind(V), V)) , active(isPal(nil())) -> mark(tt()) , active(U74(X)) -> U74(active(X)) , active(U74(tt())) -> mark(tt()) , active(U81(X1, X2)) -> U81(active(X1), X2) , active(U81(tt(), V)) -> mark(U82(isPalListKind(V), V)) , active(U82(X1, X2)) -> U82(active(X1), X2) , active(U82(tt(), V)) -> mark(U83(isNePal(V))) , active(U83(X)) -> U83(active(X)) , active(U83(tt())) -> mark(tt()) , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) , active(isNePal(__(I, __(P, I)))) -> mark(U71(isQid(I), I, P)) , active(U91(X1, X2)) -> U91(active(X1), X2) , active(U91(tt(), V2)) -> mark(U92(isPalListKind(V2))) , active(U92(X)) -> U92(active(X)) , active(U92(tt())) -> mark(tt()) , __(X1, mark(X2)) -> mark(__(X1, X2)) , __(mark(X1), X2) -> mark(__(X1, X2)) , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) , U11(mark(X1), X2) -> mark(U11(X1, X2)) , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , isPalListKind(ok(X)) -> ok(isPalListKind(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , isNeList(ok(X)) -> ok(isNeList(X)) , U21(mark(X1), X2, X3) -> mark(U21(X1, X2, X3)) , U21(ok(X1), ok(X2), ok(X3)) -> ok(U21(X1, X2, X3)) , U22(mark(X1), X2, X3) -> mark(U22(X1, X2, X3)) , U22(ok(X1), ok(X2), ok(X3)) -> ok(U22(X1, X2, X3)) , U23(mark(X1), X2, X3) -> mark(U23(X1, X2, X3)) , U23(ok(X1), ok(X2), ok(X3)) -> ok(U23(X1, X2, X3)) , U24(mark(X1), X2, X3) -> mark(U24(X1, X2, X3)) , U24(ok(X1), ok(X2), ok(X3)) -> ok(U24(X1, X2, X3)) , U25(mark(X1), X2) -> mark(U25(X1, X2)) , U25(ok(X1), ok(X2)) -> ok(U25(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , U26(mark(X)) -> mark(U26(X)) , U26(ok(X)) -> ok(U26(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , isQid(ok(X)) -> ok(isQid(X)) , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) , U45(mark(X1), X2) -> mark(U45(X1, X2)) , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) , U46(mark(X)) -> mark(U46(X)) , U46(ok(X)) -> ok(U46(X)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , U52(mark(X1), X2, X3) -> mark(U52(X1, X2, X3)) , U52(ok(X1), ok(X2), ok(X3)) -> ok(U52(X1, X2, X3)) , U53(mark(X1), X2, X3) -> mark(U53(X1, X2, X3)) , U53(ok(X1), ok(X2), ok(X3)) -> ok(U53(X1, X2, X3)) , U54(mark(X1), X2, X3) -> mark(U54(X1, X2, X3)) , U54(ok(X1), ok(X2), ok(X3)) -> ok(U54(X1, X2, X3)) , U55(mark(X1), X2) -> mark(U55(X1, X2)) , U55(ok(X1), ok(X2)) -> ok(U55(X1, X2)) , U56(mark(X)) -> mark(U56(X)) , U56(ok(X)) -> ok(U56(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X1), X2) -> mark(U62(X1, X2)) , U62(ok(X1), ok(X2)) -> ok(U62(X1, X2)) , U63(mark(X)) -> mark(U63(X)) , U63(ok(X)) -> ok(U63(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , U72(mark(X1), X2) -> mark(U72(X1, X2)) , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) , U73(mark(X1), X2) -> mark(U73(X1, X2)) , U73(ok(X1), ok(X2)) -> ok(U73(X1, X2)) , isPal(ok(X)) -> ok(isPal(X)) , U74(mark(X)) -> mark(U74(X)) , U74(ok(X)) -> ok(U74(X)) , U81(mark(X1), X2) -> mark(U81(X1, X2)) , U81(ok(X1), ok(X2)) -> ok(U81(X1, X2)) , U82(mark(X1), X2) -> mark(U82(X1, X2)) , U82(ok(X1), ok(X2)) -> ok(U82(X1, X2)) , U83(mark(X)) -> mark(U83(X)) , U83(ok(X)) -> ok(U83(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , U91(mark(X1), X2) -> mark(U91(X1, X2)) , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) , U92(mark(X)) -> mark(U92(X)) , U92(ok(X)) -> ok(U92(X)) , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) , proper(tt()) -> ok(tt()) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(isPalListKind(X)) -> isPalListKind(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(U21(X1, X2, X3)) -> U21(proper(X1), proper(X2), proper(X3)) , proper(U22(X1, X2, X3)) -> U22(proper(X1), proper(X2), proper(X3)) , proper(U23(X1, X2, X3)) -> U23(proper(X1), proper(X2), proper(X3)) , proper(U24(X1, X2, X3)) -> U24(proper(X1), proper(X2), proper(X3)) , proper(U25(X1, X2)) -> U25(proper(X1), proper(X2)) , proper(isList(X)) -> isList(proper(X)) , proper(U26(X)) -> U26(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2, X3)) -> U42(proper(X1), proper(X2), proper(X3)) , proper(U43(X1, X2, X3)) -> U43(proper(X1), proper(X2), proper(X3)) , proper(U44(X1, X2, X3)) -> U44(proper(X1), proper(X2), proper(X3)) , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) , proper(U46(X)) -> U46(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(U52(X1, X2, X3)) -> U52(proper(X1), proper(X2), proper(X3)) , proper(U53(X1, X2, X3)) -> U53(proper(X1), proper(X2), proper(X3)) , proper(U54(X1, X2, X3)) -> U54(proper(X1), proper(X2), proper(X3)) , proper(U55(X1, X2)) -> U55(proper(X1), proper(X2)) , proper(U56(X)) -> U56(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X1, X2)) -> U62(proper(X1), proper(X2)) , proper(U63(X)) -> U63(proper(X)) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) , proper(U73(X1, X2)) -> U73(proper(X1), proper(X2)) , proper(isPal(X)) -> isPal(proper(X)) , proper(U74(X)) -> U74(proper(X)) , proper(U81(X1, X2)) -> U81(proper(X1), proper(X2)) , proper(U82(X1, X2)) -> U82(proper(X1), proper(X2)) , proper(U83(X)) -> U83(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) , proper(U92(X)) -> U92(proper(X)) , proper(a()) -> ok(a()) , proper(e()) -> ok(e()) , proper(i()) -> ok(i()) , proper(o()) -> ok(o()) , proper(u()) -> ok(u()) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE Consider the dependency graph: 1: active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 2: active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 3: active^#(__(X, nil())) -> c_3(X) -->_1 top^#(ok(X)) -> c_232(top^#(active(X))) :232 -->_1 top^#(mark(X)) -> c_231(top^#(proper(X))) :231 -->_1 proper^#(U92(X)) -> c_225(U92^#(proper(X))) :225 -->_1 proper^#(U91(X1, X2)) -> c_224(U91^#(proper(X1), proper(X2))) :224 -->_1 proper^#(isNePal(X)) -> c_223(isNePal^#(proper(X))) :223 -->_1 proper^#(U83(X)) -> c_222(U83^#(proper(X))) :222 -->_1 proper^#(U82(X1, X2)) -> c_221(U82^#(proper(X1), proper(X2))) :221 -->_1 proper^#(U81(X1, X2)) -> c_220(U81^#(proper(X1), proper(X2))) :220 -->_1 proper^#(U74(X)) -> c_219(U74^#(proper(X))) :219 -->_1 proper^#(isPal(X)) -> c_218(isPal^#(proper(X))) :218 -->_1 proper^#(U73(X1, X2)) -> c_217(U73^#(proper(X1), proper(X2))) :217 -->_1 proper^#(U72(X1, X2)) -> c_216(U72^#(proper(X1), proper(X2))) :216 -->_1 proper^#(U71(X1, X2, X3)) -> c_215(U71^#(proper(X1), proper(X2), proper(X3))) :215 -->_1 proper^#(U63(X)) -> c_214(U63^#(proper(X))) :214 -->_1 proper^#(U62(X1, X2)) -> c_213(U62^#(proper(X1), proper(X2))) :213 -->_1 proper^#(U61(X1, X2)) -> c_212(U61^#(proper(X1), proper(X2))) :212 -->_1 proper^#(U56(X)) -> c_211(U56^#(proper(X))) :211 -->_1 proper^#(U55(X1, X2)) -> c_210(U55^#(proper(X1), proper(X2))) :210 -->_1 proper^#(U54(X1, X2, X3)) -> c_209(U54^#(proper(X1), proper(X2), proper(X3))) :209 -->_1 proper^#(U53(X1, X2, X3)) -> c_208(U53^#(proper(X1), proper(X2), proper(X3))) :208 -->_1 proper^#(U52(X1, X2, X3)) -> c_207(U52^#(proper(X1), proper(X2), proper(X3))) :207 -->_1 proper^#(U51(X1, X2, X3)) -> c_206(U51^#(proper(X1), proper(X2), proper(X3))) :206 -->_1 proper^#(U46(X)) -> c_205(U46^#(proper(X))) :205 -->_1 proper^#(U45(X1, X2)) -> c_204(U45^#(proper(X1), proper(X2))) :204 -->_1 proper^#(U44(X1, X2, X3)) -> c_203(U44^#(proper(X1), proper(X2), proper(X3))) :203 -->_1 proper^#(U43(X1, X2, X3)) -> c_202(U43^#(proper(X1), proper(X2), proper(X3))) :202 -->_1 proper^#(U42(X1, X2, X3)) -> c_201(U42^#(proper(X1), proper(X2), proper(X3))) :201 -->_1 proper^#(U41(X1, X2, X3)) -> c_200(U41^#(proper(X1), proper(X2), proper(X3))) :200 -->_1 proper^#(isQid(X)) -> c_199(isQid^#(proper(X))) :199 -->_1 proper^#(U33(X)) -> c_198(U33^#(proper(X))) :198 -->_1 proper^#(U32(X1, X2)) -> c_197(U32^#(proper(X1), proper(X2))) :197 -->_1 proper^#(U31(X1, X2)) -> c_196(U31^#(proper(X1), proper(X2))) :196 -->_1 proper^#(U26(X)) -> c_195(U26^#(proper(X))) :195 -->_1 proper^#(isList(X)) -> c_194(isList^#(proper(X))) :194 -->_1 proper^#(U25(X1, X2)) -> c_193(U25^#(proper(X1), proper(X2))) :193 -->_1 proper^#(U24(X1, X2, X3)) -> c_192(U24^#(proper(X1), proper(X2), proper(X3))) :192 -->_1 proper^#(U23(X1, X2, X3)) -> c_191(U23^#(proper(X1), proper(X2), proper(X3))) :191 -->_1 proper^#(U22(X1, X2, X3)) -> c_190(U22^#(proper(X1), proper(X2), proper(X3))) :190 -->_1 proper^#(U21(X1, X2, X3)) -> c_189(U21^#(proper(X1), proper(X2), proper(X3))) :189 -->_1 proper^#(isNeList(X)) -> c_188(isNeList^#(proper(X))) :188 -->_1 proper^#(U13(X)) -> c_187(U13^#(proper(X))) :187 -->_1 proper^#(isPalListKind(X)) -> c_186(isPalListKind^#(proper(X))) :186 -->_1 proper^#(U12(X1, X2)) -> c_185(U12^#(proper(X1), proper(X2))) :185 -->_1 proper^#(U11(X1, X2)) -> c_183(U11^#(proper(X1), proper(X2))) :183 -->_1 proper^#(__(X1, X2)) -> c_181(__^#(proper(X1), proper(X2))) :181 -->_1 isNePal^#(ok(X)) -> c_176(isNePal^#(X)) :180 -->_1 isPal^#(ok(X)) -> c_167(isPal^#(X)) :179 -->_1 isQid^#(ok(X)) -> c_130(isQid^#(X)) :178 -->_1 isList^#(ok(X)) -> c_121(isList^#(X)) :177 -->_1 isNeList^#(ok(X)) -> c_110(isNeList^#(X)) :176 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :175 -->_1 U92^#(ok(X)) -> c_180(U92^#(X)) :174 -->_1 U92^#(mark(X)) -> c_179(U92^#(X)) :173 -->_1 U83^#(ok(X)) -> c_175(U83^#(X)) :172 -->_1 U83^#(mark(X)) -> c_174(U83^#(X)) :171 -->_1 U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) :170 -->_1 U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) :169 -->_1 U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) :168 -->_1 U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) :167 -->_1 U74^#(ok(X)) -> c_169(U74^#(X)) :166 -->_1 U74^#(mark(X)) -> c_168(U74^#(X)) :165 -->_1 U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) :164 -->_1 U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) :163 -->_1 U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) :162 -->_1 U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) :161 -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) :160 -->_1 U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) :159 -->_1 U63^#(ok(X)) -> c_160(U63^#(X)) :158 -->_1 U63^#(mark(X)) -> c_159(U63^#(X)) :157 -->_1 U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) :156 -->_1 U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) :155 -->_1 U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) :154 -->_1 U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) :153 -->_1 U56^#(ok(X)) -> c_154(U56^#(X)) :152 -->_1 U56^#(mark(X)) -> c_153(U56^#(X)) :151 -->_1 U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) :150 -->_1 U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) :149 -->_1 U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) :148 -->_1 U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) :147 -->_1 U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) :146 -->_1 U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) :145 -->_1 U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) :144 -->_1 U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) :143 -->_1 U46^#(ok(X)) -> c_142(U46^#(X)) :142 -->_1 U46^#(mark(X)) -> c_141(U46^#(X)) :141 -->_1 U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) :140 -->_1 U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) :139 -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) :138 -->_1 U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) :137 -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) :136 -->_1 U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) :135 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) :134 -->_1 U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) :133 -->_1 U33^#(ok(X)) -> c_129(U33^#(X)) :132 -->_1 U33^#(mark(X)) -> c_128(U33^#(X)) :131 -->_1 U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) :130 -->_1 U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) :129 -->_1 U26^#(ok(X)) -> c_123(U26^#(X)) :128 -->_1 U26^#(mark(X)) -> c_122(U26^#(X)) :127 -->_1 U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) :126 -->_1 U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) :125 -->_1 U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) :124 -->_1 U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) :123 -->_1 U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) :122 -->_1 U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) :121 -->_1 U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) :120 -->_1 U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) :119 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) :118 -->_1 U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) :117 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) :116 -->_1 U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) :115 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) :114 -->_1 U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) :113 -->_1 U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) :112 -->_1 U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) :111 -->_1 U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) :110 -->_1 U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) :109 -->_1 U13^#(ok(X)) -> c_109(U13^#(X)) :108 -->_1 U13^#(mark(X)) -> c_108(U13^#(X)) :107 -->_1 U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) :106 -->_1 U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) :105 -->_1 U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) :104 -->_1 U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) :103 -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 -->_1 active^#(U92(X)) -> c_98(U92^#(active(X))) :98 -->_1 active^#(U91(tt(), V2)) -> c_97(U92^#(isPalListKind(V2))) :97 -->_1 active^#(U91(X1, X2)) -> c_96(U91^#(active(X1), X2)) :96 -->_1 active^#(isNePal(__(I, __(P, I)))) -> c_95(U71^#(isQid(I), I, P)) :95 -->_1 active^#(isNePal(V)) -> c_94(U61^#(isPalListKind(V), V)) :94 -->_1 active^#(U83(X)) -> c_92(U83^#(active(X))) :92 -->_1 active^#(U82(tt(), V)) -> c_91(U83^#(isNePal(V))) :91 -->_1 active^#(U82(X1, X2)) -> c_90(U82^#(active(X1), X2)) :90 -->_1 active^#(U81(tt(), V)) -> c_89(U82^#(isPalListKind(V), V)) :89 -->_1 active^#(U81(X1, X2)) -> c_88(U81^#(active(X1), X2)) :88 -->_1 active^#(U74(X)) -> c_86(U74^#(active(X))) :86 -->_1 active^#(isPal(V)) -> c_84(U81^#(isPalListKind(V), V)) :84 -->_1 active^#(U73(tt(), P)) -> c_83(U74^#(isPalListKind(P))) :83 -->_1 active^#(U73(X1, X2)) -> c_82(U73^#(active(X1), X2)) :82 -->_1 active^#(U72(tt(), P)) -> c_81(U73^#(isPal(P), P)) :81 -->_1 active^#(U72(X1, X2)) -> c_80(U72^#(active(X1), X2)) :80 -->_1 active^#(U71(tt(), I, P)) -> c_79(U72^#(isPalListKind(I), P)) :79 -->_1 active^#(U71(X1, X2, X3)) -> c_78(U71^#(active(X1), X2, X3)) :78 -->_1 active^#(U63(X)) -> c_76(U63^#(active(X))) :76 -->_1 active^#(U62(tt(), V)) -> c_75(U63^#(isQid(V))) :75 -->_1 active^#(U62(X1, X2)) -> c_74(U62^#(active(X1), X2)) :74 -->_1 active^#(U61(tt(), V)) -> c_73(U62^#(isPalListKind(V), V)) :73 -->_1 active^#(U61(X1, X2)) -> c_72(U61^#(active(X1), X2)) :72 -->_1 active^#(U56(X)) -> c_70(U56^#(active(X))) :70 -->_1 active^#(U55(tt(), V2)) -> c_69(U56^#(isList(V2))) :69 -->_1 active^#(U55(X1, X2)) -> c_68(U55^#(active(X1), X2)) :68 -->_1 active^#(U54(tt(), V1, V2)) -> c_67(U55^#(isNeList(V1), V2)) :67 -->_1 active^#(U54(X1, X2, X3)) -> c_66(U54^#(active(X1), X2, X3)) :66 -->_1 active^#(U53(tt(), V1, V2)) -> c_65(U54^#(isPalListKind(V2), V1, V2)) :65 -->_1 active^#(U53(X1, X2, X3)) -> c_64(U53^#(active(X1), X2, X3)) :64 -->_1 active^#(U52(tt(), V1, V2)) -> c_63(U53^#(isPalListKind(V2), V1, V2)) :63 -->_1 active^#(U52(X1, X2, X3)) -> c_62(U52^#(active(X1), X2, X3)) :62 -->_1 active^#(U51(tt(), V1, V2)) -> c_61(U52^#(isPalListKind(V1), V1, V2)) :61 -->_1 active^#(U51(X1, X2, X3)) -> c_60(U51^#(active(X1), X2, X3)) :60 -->_1 active^#(U46(X)) -> c_58(U46^#(active(X))) :58 -->_1 active^#(U45(tt(), V2)) -> c_57(U46^#(isNeList(V2))) :57 -->_1 active^#(U45(X1, X2)) -> c_56(U45^#(active(X1), X2)) :56 -->_1 active^#(U44(tt(), V1, V2)) -> c_55(U45^#(isList(V1), V2)) :55 -->_1 active^#(U44(X1, X2, X3)) -> c_54(U44^#(active(X1), X2, X3)) :54 -->_1 active^#(U43(tt(), V1, V2)) -> c_53(U44^#(isPalListKind(V2), V1, V2)) :53 -->_1 active^#(U43(X1, X2, X3)) -> c_52(U43^#(active(X1), X2, X3)) :52 -->_1 active^#(U42(tt(), V1, V2)) -> c_51(U43^#(isPalListKind(V2), V1, V2)) :51 -->_1 active^#(U42(X1, X2, X3)) -> c_50(U42^#(active(X1), X2, X3)) :50 -->_1 active^#(U41(tt(), V1, V2)) -> c_49(U42^#(isPalListKind(V1), V1, V2)) :49 -->_1 active^#(U41(X1, X2, X3)) -> c_48(U41^#(active(X1), X2, X3)) :48 -->_1 active^#(U33(X)) -> c_41(U33^#(active(X))) :41 -->_1 active^#(U32(tt(), V)) -> c_40(U33^#(isQid(V))) :40 -->_1 active^#(U32(X1, X2)) -> c_39(U32^#(active(X1), X2)) :39 -->_1 active^#(U31(tt(), V)) -> c_38(U32^#(isPalListKind(V), V)) :38 -->_1 active^#(U31(X1, X2)) -> c_37(U31^#(active(X1), X2)) :37 -->_1 active^#(U26(X)) -> c_35(U26^#(active(X))) :35 -->_1 active^#(isList(__(V1, V2))) -> c_33(U21^#(isPalListKind(V1), V1, V2)) :33 -->_1 active^#(isList(V)) -> c_32(U11^#(isPalListKind(V), V)) :32 -->_1 active^#(U25(tt(), V2)) -> c_31(U26^#(isList(V2))) :31 -->_1 active^#(U25(X1, X2)) -> c_30(U25^#(active(X1), X2)) :30 -->_1 active^#(U24(tt(), V1, V2)) -> c_29(U25^#(isList(V1), V2)) :29 -->_1 active^#(U24(X1, X2, X3)) -> c_28(U24^#(active(X1), X2, X3)) :28 -->_1 active^#(U23(tt(), V1, V2)) -> c_27(U24^#(isPalListKind(V2), V1, V2)) :27 -->_1 active^#(U23(X1, X2, X3)) -> c_26(U23^#(active(X1), X2, X3)) :26 -->_1 active^#(U22(tt(), V1, V2)) -> c_25(U23^#(isPalListKind(V2), V1, V2)) :25 -->_1 active^#(U22(X1, X2, X3)) -> c_24(U22^#(active(X1), X2, X3)) :24 -->_1 active^#(U21(tt(), V1, V2)) -> c_23(U22^#(isPalListKind(V1), V1, V2)) :23 -->_1 active^#(U21(X1, X2, X3)) -> c_22(U21^#(active(X1), X2, X3)) :22 -->_1 active^#(isNeList(__(V1, V2))) -> c_21(U51^#(isPalListKind(V1), V1, V2)) :21 -->_1 active^#(isNeList(__(V1, V2))) -> c_20(U41^#(isPalListKind(V1), V1, V2)) :20 -->_1 active^#(isNeList(V)) -> c_19(U31^#(isPalListKind(V), V)) :19 -->_1 active^#(U13(X)) -> c_17(U13^#(active(X))) :17 -->_1 active^#(isPalListKind(__(V1, V2))) -> c_10(U91^#(isPalListKind(V1), V2)) :10 -->_1 active^#(U12(tt(), V)) -> c_9(U13^#(isNeList(V))) :9 -->_1 active^#(U12(X1, X2)) -> c_8(U12^#(active(X1), X2)) :8 -->_1 active^#(U11(tt(), V)) -> c_7(U12^#(isPalListKind(V), V)) :7 -->_1 active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) :6 -->_1 active^#(__(nil(), X)) -> c_5(X) :5 -->_1 active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) :4 -->_1 proper^#(u()) -> c_230() :230 -->_1 proper^#(o()) -> c_229() :229 -->_1 proper^#(i()) -> c_228() :228 -->_1 proper^#(e()) -> c_227() :227 -->_1 proper^#(a()) -> c_226() :226 -->_1 proper^#(tt()) -> c_184() :184 -->_1 proper^#(nil()) -> c_182() :182 -->_1 active^#(U92(tt())) -> c_99() :99 -->_1 active^#(U83(tt())) -> c_93() :93 -->_1 active^#(U74(tt())) -> c_87() :87 -->_1 active^#(isPal(nil())) -> c_85() :85 -->_1 active^#(U63(tt())) -> c_77() :77 -->_1 active^#(U56(tt())) -> c_71() :71 -->_1 active^#(U46(tt())) -> c_59() :59 -->_1 active^#(isQid(u())) -> c_47() :47 -->_1 active^#(isQid(o())) -> c_46() :46 -->_1 active^#(isQid(i())) -> c_45() :45 -->_1 active^#(isQid(e())) -> c_44() :44 -->_1 active^#(isQid(a())) -> c_43() :43 -->_1 active^#(U33(tt())) -> c_42() :42 -->_1 active^#(U26(tt())) -> c_36() :36 -->_1 active^#(isList(nil())) -> c_34() :34 -->_1 active^#(U13(tt())) -> c_18() :18 -->_1 active^#(isPalListKind(u())) -> c_16() :16 -->_1 active^#(isPalListKind(o())) -> c_15() :15 -->_1 active^#(isPalListKind(i())) -> c_14() :14 -->_1 active^#(isPalListKind(e())) -> c_13() :13 -->_1 active^#(isPalListKind(a())) -> c_12() :12 -->_1 active^#(isPalListKind(nil())) -> c_11() :11 -->_1 active^#(__(X, nil())) -> c_3(X) :3 -->_1 active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) :2 -->_1 active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) :1 4: active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 5: active^#(__(nil(), X)) -> c_5(X) -->_1 top^#(ok(X)) -> c_232(top^#(active(X))) :232 -->_1 top^#(mark(X)) -> c_231(top^#(proper(X))) :231 -->_1 proper^#(U92(X)) -> c_225(U92^#(proper(X))) :225 -->_1 proper^#(U91(X1, X2)) -> c_224(U91^#(proper(X1), proper(X2))) :224 -->_1 proper^#(isNePal(X)) -> c_223(isNePal^#(proper(X))) :223 -->_1 proper^#(U83(X)) -> c_222(U83^#(proper(X))) :222 -->_1 proper^#(U82(X1, X2)) -> c_221(U82^#(proper(X1), proper(X2))) :221 -->_1 proper^#(U81(X1, X2)) -> c_220(U81^#(proper(X1), proper(X2))) :220 -->_1 proper^#(U74(X)) -> c_219(U74^#(proper(X))) :219 -->_1 proper^#(isPal(X)) -> c_218(isPal^#(proper(X))) :218 -->_1 proper^#(U73(X1, X2)) -> c_217(U73^#(proper(X1), proper(X2))) :217 -->_1 proper^#(U72(X1, X2)) -> c_216(U72^#(proper(X1), proper(X2))) :216 -->_1 proper^#(U71(X1, X2, X3)) -> c_215(U71^#(proper(X1), proper(X2), proper(X3))) :215 -->_1 proper^#(U63(X)) -> c_214(U63^#(proper(X))) :214 -->_1 proper^#(U62(X1, X2)) -> c_213(U62^#(proper(X1), proper(X2))) :213 -->_1 proper^#(U61(X1, X2)) -> c_212(U61^#(proper(X1), proper(X2))) :212 -->_1 proper^#(U56(X)) -> c_211(U56^#(proper(X))) :211 -->_1 proper^#(U55(X1, X2)) -> c_210(U55^#(proper(X1), proper(X2))) :210 -->_1 proper^#(U54(X1, X2, X3)) -> c_209(U54^#(proper(X1), proper(X2), proper(X3))) :209 -->_1 proper^#(U53(X1, X2, X3)) -> c_208(U53^#(proper(X1), proper(X2), proper(X3))) :208 -->_1 proper^#(U52(X1, X2, X3)) -> c_207(U52^#(proper(X1), proper(X2), proper(X3))) :207 -->_1 proper^#(U51(X1, X2, X3)) -> c_206(U51^#(proper(X1), proper(X2), proper(X3))) :206 -->_1 proper^#(U46(X)) -> c_205(U46^#(proper(X))) :205 -->_1 proper^#(U45(X1, X2)) -> c_204(U45^#(proper(X1), proper(X2))) :204 -->_1 proper^#(U44(X1, X2, X3)) -> c_203(U44^#(proper(X1), proper(X2), proper(X3))) :203 -->_1 proper^#(U43(X1, X2, X3)) -> c_202(U43^#(proper(X1), proper(X2), proper(X3))) :202 -->_1 proper^#(U42(X1, X2, X3)) -> c_201(U42^#(proper(X1), proper(X2), proper(X3))) :201 -->_1 proper^#(U41(X1, X2, X3)) -> c_200(U41^#(proper(X1), proper(X2), proper(X3))) :200 -->_1 proper^#(isQid(X)) -> c_199(isQid^#(proper(X))) :199 -->_1 proper^#(U33(X)) -> c_198(U33^#(proper(X))) :198 -->_1 proper^#(U32(X1, X2)) -> c_197(U32^#(proper(X1), proper(X2))) :197 -->_1 proper^#(U31(X1, X2)) -> c_196(U31^#(proper(X1), proper(X2))) :196 -->_1 proper^#(U26(X)) -> c_195(U26^#(proper(X))) :195 -->_1 proper^#(isList(X)) -> c_194(isList^#(proper(X))) :194 -->_1 proper^#(U25(X1, X2)) -> c_193(U25^#(proper(X1), proper(X2))) :193 -->_1 proper^#(U24(X1, X2, X3)) -> c_192(U24^#(proper(X1), proper(X2), proper(X3))) :192 -->_1 proper^#(U23(X1, X2, X3)) -> c_191(U23^#(proper(X1), proper(X2), proper(X3))) :191 -->_1 proper^#(U22(X1, X2, X3)) -> c_190(U22^#(proper(X1), proper(X2), proper(X3))) :190 -->_1 proper^#(U21(X1, X2, X3)) -> c_189(U21^#(proper(X1), proper(X2), proper(X3))) :189 -->_1 proper^#(isNeList(X)) -> c_188(isNeList^#(proper(X))) :188 -->_1 proper^#(U13(X)) -> c_187(U13^#(proper(X))) :187 -->_1 proper^#(isPalListKind(X)) -> c_186(isPalListKind^#(proper(X))) :186 -->_1 proper^#(U12(X1, X2)) -> c_185(U12^#(proper(X1), proper(X2))) :185 -->_1 proper^#(U11(X1, X2)) -> c_183(U11^#(proper(X1), proper(X2))) :183 -->_1 proper^#(__(X1, X2)) -> c_181(__^#(proper(X1), proper(X2))) :181 -->_1 isNePal^#(ok(X)) -> c_176(isNePal^#(X)) :180 -->_1 isPal^#(ok(X)) -> c_167(isPal^#(X)) :179 -->_1 isQid^#(ok(X)) -> c_130(isQid^#(X)) :178 -->_1 isList^#(ok(X)) -> c_121(isList^#(X)) :177 -->_1 isNeList^#(ok(X)) -> c_110(isNeList^#(X)) :176 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :175 -->_1 U92^#(ok(X)) -> c_180(U92^#(X)) :174 -->_1 U92^#(mark(X)) -> c_179(U92^#(X)) :173 -->_1 U83^#(ok(X)) -> c_175(U83^#(X)) :172 -->_1 U83^#(mark(X)) -> c_174(U83^#(X)) :171 -->_1 U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) :170 -->_1 U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) :169 -->_1 U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) :168 -->_1 U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) :167 -->_1 U74^#(ok(X)) -> c_169(U74^#(X)) :166 -->_1 U74^#(mark(X)) -> c_168(U74^#(X)) :165 -->_1 U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) :164 -->_1 U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) :163 -->_1 U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) :162 -->_1 U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) :161 -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) :160 -->_1 U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) :159 -->_1 U63^#(ok(X)) -> c_160(U63^#(X)) :158 -->_1 U63^#(mark(X)) -> c_159(U63^#(X)) :157 -->_1 U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) :156 -->_1 U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) :155 -->_1 U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) :154 -->_1 U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) :153 -->_1 U56^#(ok(X)) -> c_154(U56^#(X)) :152 -->_1 U56^#(mark(X)) -> c_153(U56^#(X)) :151 -->_1 U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) :150 -->_1 U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) :149 -->_1 U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) :148 -->_1 U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) :147 -->_1 U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) :146 -->_1 U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) :145 -->_1 U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) :144 -->_1 U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) :143 -->_1 U46^#(ok(X)) -> c_142(U46^#(X)) :142 -->_1 U46^#(mark(X)) -> c_141(U46^#(X)) :141 -->_1 U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) :140 -->_1 U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) :139 -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) :138 -->_1 U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) :137 -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) :136 -->_1 U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) :135 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) :134 -->_1 U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) :133 -->_1 U33^#(ok(X)) -> c_129(U33^#(X)) :132 -->_1 U33^#(mark(X)) -> c_128(U33^#(X)) :131 -->_1 U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) :130 -->_1 U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) :129 -->_1 U26^#(ok(X)) -> c_123(U26^#(X)) :128 -->_1 U26^#(mark(X)) -> c_122(U26^#(X)) :127 -->_1 U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) :126 -->_1 U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) :125 -->_1 U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) :124 -->_1 U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) :123 -->_1 U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) :122 -->_1 U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) :121 -->_1 U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) :120 -->_1 U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) :119 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) :118 -->_1 U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) :117 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) :116 -->_1 U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) :115 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) :114 -->_1 U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) :113 -->_1 U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) :112 -->_1 U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) :111 -->_1 U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) :110 -->_1 U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) :109 -->_1 U13^#(ok(X)) -> c_109(U13^#(X)) :108 -->_1 U13^#(mark(X)) -> c_108(U13^#(X)) :107 -->_1 U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) :106 -->_1 U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) :105 -->_1 U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) :104 -->_1 U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) :103 -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 -->_1 active^#(U92(X)) -> c_98(U92^#(active(X))) :98 -->_1 active^#(U91(tt(), V2)) -> c_97(U92^#(isPalListKind(V2))) :97 -->_1 active^#(U91(X1, X2)) -> c_96(U91^#(active(X1), X2)) :96 -->_1 active^#(isNePal(__(I, __(P, I)))) -> c_95(U71^#(isQid(I), I, P)) :95 -->_1 active^#(isNePal(V)) -> c_94(U61^#(isPalListKind(V), V)) :94 -->_1 active^#(U83(X)) -> c_92(U83^#(active(X))) :92 -->_1 active^#(U82(tt(), V)) -> c_91(U83^#(isNePal(V))) :91 -->_1 active^#(U82(X1, X2)) -> c_90(U82^#(active(X1), X2)) :90 -->_1 active^#(U81(tt(), V)) -> c_89(U82^#(isPalListKind(V), V)) :89 -->_1 active^#(U81(X1, X2)) -> c_88(U81^#(active(X1), X2)) :88 -->_1 active^#(U74(X)) -> c_86(U74^#(active(X))) :86 -->_1 active^#(isPal(V)) -> c_84(U81^#(isPalListKind(V), V)) :84 -->_1 active^#(U73(tt(), P)) -> c_83(U74^#(isPalListKind(P))) :83 -->_1 active^#(U73(X1, X2)) -> c_82(U73^#(active(X1), X2)) :82 -->_1 active^#(U72(tt(), P)) -> c_81(U73^#(isPal(P), P)) :81 -->_1 active^#(U72(X1, X2)) -> c_80(U72^#(active(X1), X2)) :80 -->_1 active^#(U71(tt(), I, P)) -> c_79(U72^#(isPalListKind(I), P)) :79 -->_1 active^#(U71(X1, X2, X3)) -> c_78(U71^#(active(X1), X2, X3)) :78 -->_1 active^#(U63(X)) -> c_76(U63^#(active(X))) :76 -->_1 active^#(U62(tt(), V)) -> c_75(U63^#(isQid(V))) :75 -->_1 active^#(U62(X1, X2)) -> c_74(U62^#(active(X1), X2)) :74 -->_1 active^#(U61(tt(), V)) -> c_73(U62^#(isPalListKind(V), V)) :73 -->_1 active^#(U61(X1, X2)) -> c_72(U61^#(active(X1), X2)) :72 -->_1 active^#(U56(X)) -> c_70(U56^#(active(X))) :70 -->_1 active^#(U55(tt(), V2)) -> c_69(U56^#(isList(V2))) :69 -->_1 active^#(U55(X1, X2)) -> c_68(U55^#(active(X1), X2)) :68 -->_1 active^#(U54(tt(), V1, V2)) -> c_67(U55^#(isNeList(V1), V2)) :67 -->_1 active^#(U54(X1, X2, X3)) -> c_66(U54^#(active(X1), X2, X3)) :66 -->_1 active^#(U53(tt(), V1, V2)) -> c_65(U54^#(isPalListKind(V2), V1, V2)) :65 -->_1 active^#(U53(X1, X2, X3)) -> c_64(U53^#(active(X1), X2, X3)) :64 -->_1 active^#(U52(tt(), V1, V2)) -> c_63(U53^#(isPalListKind(V2), V1, V2)) :63 -->_1 active^#(U52(X1, X2, X3)) -> c_62(U52^#(active(X1), X2, X3)) :62 -->_1 active^#(U51(tt(), V1, V2)) -> c_61(U52^#(isPalListKind(V1), V1, V2)) :61 -->_1 active^#(U51(X1, X2, X3)) -> c_60(U51^#(active(X1), X2, X3)) :60 -->_1 active^#(U46(X)) -> c_58(U46^#(active(X))) :58 -->_1 active^#(U45(tt(), V2)) -> c_57(U46^#(isNeList(V2))) :57 -->_1 active^#(U45(X1, X2)) -> c_56(U45^#(active(X1), X2)) :56 -->_1 active^#(U44(tt(), V1, V2)) -> c_55(U45^#(isList(V1), V2)) :55 -->_1 active^#(U44(X1, X2, X3)) -> c_54(U44^#(active(X1), X2, X3)) :54 -->_1 active^#(U43(tt(), V1, V2)) -> c_53(U44^#(isPalListKind(V2), V1, V2)) :53 -->_1 active^#(U43(X1, X2, X3)) -> c_52(U43^#(active(X1), X2, X3)) :52 -->_1 active^#(U42(tt(), V1, V2)) -> c_51(U43^#(isPalListKind(V2), V1, V2)) :51 -->_1 active^#(U42(X1, X2, X3)) -> c_50(U42^#(active(X1), X2, X3)) :50 -->_1 active^#(U41(tt(), V1, V2)) -> c_49(U42^#(isPalListKind(V1), V1, V2)) :49 -->_1 active^#(U41(X1, X2, X3)) -> c_48(U41^#(active(X1), X2, X3)) :48 -->_1 active^#(U33(X)) -> c_41(U33^#(active(X))) :41 -->_1 active^#(U32(tt(), V)) -> c_40(U33^#(isQid(V))) :40 -->_1 active^#(U32(X1, X2)) -> c_39(U32^#(active(X1), X2)) :39 -->_1 active^#(U31(tt(), V)) -> c_38(U32^#(isPalListKind(V), V)) :38 -->_1 active^#(U31(X1, X2)) -> c_37(U31^#(active(X1), X2)) :37 -->_1 active^#(U26(X)) -> c_35(U26^#(active(X))) :35 -->_1 active^#(isList(__(V1, V2))) -> c_33(U21^#(isPalListKind(V1), V1, V2)) :33 -->_1 active^#(isList(V)) -> c_32(U11^#(isPalListKind(V), V)) :32 -->_1 active^#(U25(tt(), V2)) -> c_31(U26^#(isList(V2))) :31 -->_1 active^#(U25(X1, X2)) -> c_30(U25^#(active(X1), X2)) :30 -->_1 active^#(U24(tt(), V1, V2)) -> c_29(U25^#(isList(V1), V2)) :29 -->_1 active^#(U24(X1, X2, X3)) -> c_28(U24^#(active(X1), X2, X3)) :28 -->_1 active^#(U23(tt(), V1, V2)) -> c_27(U24^#(isPalListKind(V2), V1, V2)) :27 -->_1 active^#(U23(X1, X2, X3)) -> c_26(U23^#(active(X1), X2, X3)) :26 -->_1 active^#(U22(tt(), V1, V2)) -> c_25(U23^#(isPalListKind(V2), V1, V2)) :25 -->_1 active^#(U22(X1, X2, X3)) -> c_24(U22^#(active(X1), X2, X3)) :24 -->_1 active^#(U21(tt(), V1, V2)) -> c_23(U22^#(isPalListKind(V1), V1, V2)) :23 -->_1 active^#(U21(X1, X2, X3)) -> c_22(U21^#(active(X1), X2, X3)) :22 -->_1 active^#(isNeList(__(V1, V2))) -> c_21(U51^#(isPalListKind(V1), V1, V2)) :21 -->_1 active^#(isNeList(__(V1, V2))) -> c_20(U41^#(isPalListKind(V1), V1, V2)) :20 -->_1 active^#(isNeList(V)) -> c_19(U31^#(isPalListKind(V), V)) :19 -->_1 active^#(U13(X)) -> c_17(U13^#(active(X))) :17 -->_1 active^#(isPalListKind(__(V1, V2))) -> c_10(U91^#(isPalListKind(V1), V2)) :10 -->_1 active^#(U12(tt(), V)) -> c_9(U13^#(isNeList(V))) :9 -->_1 active^#(U12(X1, X2)) -> c_8(U12^#(active(X1), X2)) :8 -->_1 active^#(U11(tt(), V)) -> c_7(U12^#(isPalListKind(V), V)) :7 -->_1 active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) :6 -->_1 proper^#(u()) -> c_230() :230 -->_1 proper^#(o()) -> c_229() :229 -->_1 proper^#(i()) -> c_228() :228 -->_1 proper^#(e()) -> c_227() :227 -->_1 proper^#(a()) -> c_226() :226 -->_1 proper^#(tt()) -> c_184() :184 -->_1 proper^#(nil()) -> c_182() :182 -->_1 active^#(U92(tt())) -> c_99() :99 -->_1 active^#(U83(tt())) -> c_93() :93 -->_1 active^#(U74(tt())) -> c_87() :87 -->_1 active^#(isPal(nil())) -> c_85() :85 -->_1 active^#(U63(tt())) -> c_77() :77 -->_1 active^#(U56(tt())) -> c_71() :71 -->_1 active^#(U46(tt())) -> c_59() :59 -->_1 active^#(isQid(u())) -> c_47() :47 -->_1 active^#(isQid(o())) -> c_46() :46 -->_1 active^#(isQid(i())) -> c_45() :45 -->_1 active^#(isQid(e())) -> c_44() :44 -->_1 active^#(isQid(a())) -> c_43() :43 -->_1 active^#(U33(tt())) -> c_42() :42 -->_1 active^#(U26(tt())) -> c_36() :36 -->_1 active^#(isList(nil())) -> c_34() :34 -->_1 active^#(U13(tt())) -> c_18() :18 -->_1 active^#(isPalListKind(u())) -> c_16() :16 -->_1 active^#(isPalListKind(o())) -> c_15() :15 -->_1 active^#(isPalListKind(i())) -> c_14() :14 -->_1 active^#(isPalListKind(e())) -> c_13() :13 -->_1 active^#(isPalListKind(a())) -> c_12() :12 -->_1 active^#(isPalListKind(nil())) -> c_11() :11 -->_1 active^#(__(nil(), X)) -> c_5(X) :5 -->_1 active^#(__(__(X, Y), Z)) -> c_4(__^#(X, __(Y, Z))) :4 -->_1 active^#(__(X, nil())) -> c_3(X) :3 -->_1 active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) :2 -->_1 active^#(__(X1, X2)) -> c_1(__^#(X1, active(X2))) :1 6: active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) -->_1 U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) :104 -->_1 U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) :103 7: active^#(U11(tt(), V)) -> c_7(U12^#(isPalListKind(V), V)) -->_1 U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) :106 -->_1 U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) :105 8: active^#(U12(X1, X2)) -> c_8(U12^#(active(X1), X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) :106 -->_1 U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) :105 9: active^#(U12(tt(), V)) -> c_9(U13^#(isNeList(V))) -->_1 U13^#(ok(X)) -> c_109(U13^#(X)) :108 -->_1 U13^#(mark(X)) -> c_108(U13^#(X)) :107 10: active^#(isPalListKind(__(V1, V2))) -> c_10(U91^#(isPalListKind(V1), V2)) -->_1 U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) :110 -->_1 U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) :109 11: active^#(isPalListKind(nil())) -> c_11() 12: active^#(isPalListKind(a())) -> c_12() 13: active^#(isPalListKind(e())) -> c_13() 14: active^#(isPalListKind(i())) -> c_14() 15: active^#(isPalListKind(o())) -> c_15() 16: active^#(isPalListKind(u())) -> c_16() 17: active^#(U13(X)) -> c_17(U13^#(active(X))) -->_1 U13^#(ok(X)) -> c_109(U13^#(X)) :108 -->_1 U13^#(mark(X)) -> c_108(U13^#(X)) :107 18: active^#(U13(tt())) -> c_18() 19: active^#(isNeList(V)) -> c_19(U31^#(isPalListKind(V), V)) -->_1 U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) :112 -->_1 U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) :111 20: active^#(isNeList(__(V1, V2))) -> c_20(U41^#(isPalListKind(V1), V1, V2)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) :114 -->_1 U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) :113 21: active^#(isNeList(__(V1, V2))) -> c_21(U51^#(isPalListKind(V1), V1, V2)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) :116 -->_1 U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) :115 22: active^#(U21(X1, X2, X3)) -> c_22(U21^#(active(X1), X2, X3)) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) :118 -->_1 U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) :117 23: active^#(U21(tt(), V1, V2)) -> c_23(U22^#(isPalListKind(V1), V1, V2)) -->_1 U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) :120 -->_1 U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) :119 24: active^#(U22(X1, X2, X3)) -> c_24(U22^#(active(X1), X2, X3)) -->_1 U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) :120 -->_1 U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) :119 25: active^#(U22(tt(), V1, V2)) -> c_25(U23^#(isPalListKind(V2), V1, V2)) -->_1 U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) :122 -->_1 U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) :121 26: active^#(U23(X1, X2, X3)) -> c_26(U23^#(active(X1), X2, X3)) -->_1 U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) :122 -->_1 U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) :121 27: active^#(U23(tt(), V1, V2)) -> c_27(U24^#(isPalListKind(V2), V1, V2)) -->_1 U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) :124 -->_1 U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) :123 28: active^#(U24(X1, X2, X3)) -> c_28(U24^#(active(X1), X2, X3)) -->_1 U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) :124 -->_1 U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) :123 29: active^#(U24(tt(), V1, V2)) -> c_29(U25^#(isList(V1), V2)) -->_1 U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) :126 -->_1 U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) :125 30: active^#(U25(X1, X2)) -> c_30(U25^#(active(X1), X2)) -->_1 U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) :126 -->_1 U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) :125 31: active^#(U25(tt(), V2)) -> c_31(U26^#(isList(V2))) -->_1 U26^#(ok(X)) -> c_123(U26^#(X)) :128 -->_1 U26^#(mark(X)) -> c_122(U26^#(X)) :127 32: active^#(isList(V)) -> c_32(U11^#(isPalListKind(V), V)) -->_1 U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) :104 -->_1 U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) :103 33: active^#(isList(__(V1, V2))) -> c_33(U21^#(isPalListKind(V1), V1, V2)) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) :118 -->_1 U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) :117 34: active^#(isList(nil())) -> c_34() 35: active^#(U26(X)) -> c_35(U26^#(active(X))) -->_1 U26^#(ok(X)) -> c_123(U26^#(X)) :128 -->_1 U26^#(mark(X)) -> c_122(U26^#(X)) :127 36: active^#(U26(tt())) -> c_36() 37: active^#(U31(X1, X2)) -> c_37(U31^#(active(X1), X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) :112 -->_1 U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) :111 38: active^#(U31(tt(), V)) -> c_38(U32^#(isPalListKind(V), V)) -->_1 U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) :130 -->_1 U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) :129 39: active^#(U32(X1, X2)) -> c_39(U32^#(active(X1), X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) :130 -->_1 U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) :129 40: active^#(U32(tt(), V)) -> c_40(U33^#(isQid(V))) -->_1 U33^#(ok(X)) -> c_129(U33^#(X)) :132 -->_1 U33^#(mark(X)) -> c_128(U33^#(X)) :131 41: active^#(U33(X)) -> c_41(U33^#(active(X))) -->_1 U33^#(ok(X)) -> c_129(U33^#(X)) :132 -->_1 U33^#(mark(X)) -> c_128(U33^#(X)) :131 42: active^#(U33(tt())) -> c_42() 43: active^#(isQid(a())) -> c_43() 44: active^#(isQid(e())) -> c_44() 45: active^#(isQid(i())) -> c_45() 46: active^#(isQid(o())) -> c_46() 47: active^#(isQid(u())) -> c_47() 48: active^#(U41(X1, X2, X3)) -> c_48(U41^#(active(X1), X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) :114 -->_1 U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) :113 49: active^#(U41(tt(), V1, V2)) -> c_49(U42^#(isPalListKind(V1), V1, V2)) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) :134 -->_1 U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) :133 50: active^#(U42(X1, X2, X3)) -> c_50(U42^#(active(X1), X2, X3)) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) :134 -->_1 U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) :133 51: active^#(U42(tt(), V1, V2)) -> c_51(U43^#(isPalListKind(V2), V1, V2)) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) :136 -->_1 U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) :135 52: active^#(U43(X1, X2, X3)) -> c_52(U43^#(active(X1), X2, X3)) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) :136 -->_1 U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) :135 53: active^#(U43(tt(), V1, V2)) -> c_53(U44^#(isPalListKind(V2), V1, V2)) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) :138 -->_1 U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) :137 54: active^#(U44(X1, X2, X3)) -> c_54(U44^#(active(X1), X2, X3)) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) :138 -->_1 U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) :137 55: active^#(U44(tt(), V1, V2)) -> c_55(U45^#(isList(V1), V2)) -->_1 U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) :140 -->_1 U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) :139 56: active^#(U45(X1, X2)) -> c_56(U45^#(active(X1), X2)) -->_1 U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) :140 -->_1 U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) :139 57: active^#(U45(tt(), V2)) -> c_57(U46^#(isNeList(V2))) -->_1 U46^#(ok(X)) -> c_142(U46^#(X)) :142 -->_1 U46^#(mark(X)) -> c_141(U46^#(X)) :141 58: active^#(U46(X)) -> c_58(U46^#(active(X))) -->_1 U46^#(ok(X)) -> c_142(U46^#(X)) :142 -->_1 U46^#(mark(X)) -> c_141(U46^#(X)) :141 59: active^#(U46(tt())) -> c_59() 60: active^#(U51(X1, X2, X3)) -> c_60(U51^#(active(X1), X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) :116 -->_1 U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) :115 61: active^#(U51(tt(), V1, V2)) -> c_61(U52^#(isPalListKind(V1), V1, V2)) -->_1 U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) :144 -->_1 U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) :143 62: active^#(U52(X1, X2, X3)) -> c_62(U52^#(active(X1), X2, X3)) -->_1 U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) :144 -->_1 U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) :143 63: active^#(U52(tt(), V1, V2)) -> c_63(U53^#(isPalListKind(V2), V1, V2)) -->_1 U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) :146 -->_1 U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) :145 64: active^#(U53(X1, X2, X3)) -> c_64(U53^#(active(X1), X2, X3)) -->_1 U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) :146 -->_1 U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) :145 65: active^#(U53(tt(), V1, V2)) -> c_65(U54^#(isPalListKind(V2), V1, V2)) -->_1 U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) :148 -->_1 U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) :147 66: active^#(U54(X1, X2, X3)) -> c_66(U54^#(active(X1), X2, X3)) -->_1 U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) :148 -->_1 U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) :147 67: active^#(U54(tt(), V1, V2)) -> c_67(U55^#(isNeList(V1), V2)) -->_1 U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) :150 -->_1 U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) :149 68: active^#(U55(X1, X2)) -> c_68(U55^#(active(X1), X2)) -->_1 U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) :150 -->_1 U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) :149 69: active^#(U55(tt(), V2)) -> c_69(U56^#(isList(V2))) -->_1 U56^#(ok(X)) -> c_154(U56^#(X)) :152 -->_1 U56^#(mark(X)) -> c_153(U56^#(X)) :151 70: active^#(U56(X)) -> c_70(U56^#(active(X))) -->_1 U56^#(ok(X)) -> c_154(U56^#(X)) :152 -->_1 U56^#(mark(X)) -> c_153(U56^#(X)) :151 71: active^#(U56(tt())) -> c_71() 72: active^#(U61(X1, X2)) -> c_72(U61^#(active(X1), X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) :154 -->_1 U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) :153 73: active^#(U61(tt(), V)) -> c_73(U62^#(isPalListKind(V), V)) -->_1 U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) :156 -->_1 U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) :155 74: active^#(U62(X1, X2)) -> c_74(U62^#(active(X1), X2)) -->_1 U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) :156 -->_1 U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) :155 75: active^#(U62(tt(), V)) -> c_75(U63^#(isQid(V))) -->_1 U63^#(ok(X)) -> c_160(U63^#(X)) :158 -->_1 U63^#(mark(X)) -> c_159(U63^#(X)) :157 76: active^#(U63(X)) -> c_76(U63^#(active(X))) -->_1 U63^#(ok(X)) -> c_160(U63^#(X)) :158 -->_1 U63^#(mark(X)) -> c_159(U63^#(X)) :157 77: active^#(U63(tt())) -> c_77() 78: active^#(U71(X1, X2, X3)) -> c_78(U71^#(active(X1), X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) :160 -->_1 U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) :159 79: active^#(U71(tt(), I, P)) -> c_79(U72^#(isPalListKind(I), P)) -->_1 U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) :162 -->_1 U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) :161 80: active^#(U72(X1, X2)) -> c_80(U72^#(active(X1), X2)) -->_1 U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) :162 -->_1 U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) :161 81: active^#(U72(tt(), P)) -> c_81(U73^#(isPal(P), P)) -->_1 U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) :164 -->_1 U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) :163 82: active^#(U73(X1, X2)) -> c_82(U73^#(active(X1), X2)) -->_1 U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) :164 -->_1 U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) :163 83: active^#(U73(tt(), P)) -> c_83(U74^#(isPalListKind(P))) -->_1 U74^#(ok(X)) -> c_169(U74^#(X)) :166 -->_1 U74^#(mark(X)) -> c_168(U74^#(X)) :165 84: active^#(isPal(V)) -> c_84(U81^#(isPalListKind(V), V)) -->_1 U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) :168 -->_1 U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) :167 85: active^#(isPal(nil())) -> c_85() 86: active^#(U74(X)) -> c_86(U74^#(active(X))) -->_1 U74^#(ok(X)) -> c_169(U74^#(X)) :166 -->_1 U74^#(mark(X)) -> c_168(U74^#(X)) :165 87: active^#(U74(tt())) -> c_87() 88: active^#(U81(X1, X2)) -> c_88(U81^#(active(X1), X2)) -->_1 U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) :168 -->_1 U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) :167 89: active^#(U81(tt(), V)) -> c_89(U82^#(isPalListKind(V), V)) -->_1 U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) :170 -->_1 U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) :169 90: active^#(U82(X1, X2)) -> c_90(U82^#(active(X1), X2)) -->_1 U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) :170 -->_1 U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) :169 91: active^#(U82(tt(), V)) -> c_91(U83^#(isNePal(V))) -->_1 U83^#(ok(X)) -> c_175(U83^#(X)) :172 -->_1 U83^#(mark(X)) -> c_174(U83^#(X)) :171 92: active^#(U83(X)) -> c_92(U83^#(active(X))) -->_1 U83^#(ok(X)) -> c_175(U83^#(X)) :172 -->_1 U83^#(mark(X)) -> c_174(U83^#(X)) :171 93: active^#(U83(tt())) -> c_93() 94: active^#(isNePal(V)) -> c_94(U61^#(isPalListKind(V), V)) -->_1 U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) :154 -->_1 U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) :153 95: active^#(isNePal(__(I, __(P, I)))) -> c_95(U71^#(isQid(I), I, P)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) :160 -->_1 U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) :159 96: active^#(U91(X1, X2)) -> c_96(U91^#(active(X1), X2)) -->_1 U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) :110 -->_1 U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) :109 97: active^#(U91(tt(), V2)) -> c_97(U92^#(isPalListKind(V2))) -->_1 U92^#(ok(X)) -> c_180(U92^#(X)) :174 -->_1 U92^#(mark(X)) -> c_179(U92^#(X)) :173 98: active^#(U92(X)) -> c_98(U92^#(active(X))) -->_1 U92^#(ok(X)) -> c_180(U92^#(X)) :174 -->_1 U92^#(mark(X)) -> c_179(U92^#(X)) :173 99: active^#(U92(tt())) -> c_99() 100: __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 101: __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 102: __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 103: U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) -->_1 U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) :104 -->_1 U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) :103 104: U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) -->_1 U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) :104 -->_1 U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) :103 105: U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) :106 -->_1 U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) :105 106: U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) :106 -->_1 U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) :105 107: U13^#(mark(X)) -> c_108(U13^#(X)) -->_1 U13^#(ok(X)) -> c_109(U13^#(X)) :108 -->_1 U13^#(mark(X)) -> c_108(U13^#(X)) :107 108: U13^#(ok(X)) -> c_109(U13^#(X)) -->_1 U13^#(ok(X)) -> c_109(U13^#(X)) :108 -->_1 U13^#(mark(X)) -> c_108(U13^#(X)) :107 109: U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) -->_1 U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) :110 -->_1 U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) :109 110: U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) -->_1 U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) :110 -->_1 U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) :109 111: U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) :112 -->_1 U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) :111 112: U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) :112 -->_1 U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) :111 113: U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) :114 -->_1 U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) :113 114: U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) :114 -->_1 U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) :113 115: U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) :116 -->_1 U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) :115 116: U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) :116 -->_1 U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) :115 117: U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) :118 -->_1 U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) :117 118: U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) :118 -->_1 U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) :117 119: U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) -->_1 U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) :120 -->_1 U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) :119 120: U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) -->_1 U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) :120 -->_1 U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) :119 121: U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) -->_1 U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) :122 -->_1 U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) :121 122: U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) -->_1 U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) :122 -->_1 U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) :121 123: U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) -->_1 U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) :124 -->_1 U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) :123 124: U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) -->_1 U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) :124 -->_1 U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) :123 125: U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) -->_1 U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) :126 -->_1 U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) :125 126: U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) -->_1 U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) :126 -->_1 U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) :125 127: U26^#(mark(X)) -> c_122(U26^#(X)) -->_1 U26^#(ok(X)) -> c_123(U26^#(X)) :128 -->_1 U26^#(mark(X)) -> c_122(U26^#(X)) :127 128: U26^#(ok(X)) -> c_123(U26^#(X)) -->_1 U26^#(ok(X)) -> c_123(U26^#(X)) :128 -->_1 U26^#(mark(X)) -> c_122(U26^#(X)) :127 129: U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) :130 -->_1 U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) :129 130: U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) :130 -->_1 U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) :129 131: U33^#(mark(X)) -> c_128(U33^#(X)) -->_1 U33^#(ok(X)) -> c_129(U33^#(X)) :132 -->_1 U33^#(mark(X)) -> c_128(U33^#(X)) :131 132: U33^#(ok(X)) -> c_129(U33^#(X)) -->_1 U33^#(ok(X)) -> c_129(U33^#(X)) :132 -->_1 U33^#(mark(X)) -> c_128(U33^#(X)) :131 133: U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) :134 -->_1 U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) :133 134: U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) :134 -->_1 U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) :133 135: U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) :136 -->_1 U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) :135 136: U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) :136 -->_1 U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) :135 137: U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) :138 -->_1 U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) :137 138: U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) :138 -->_1 U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) :137 139: U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) -->_1 U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) :140 -->_1 U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) :139 140: U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) -->_1 U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) :140 -->_1 U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) :139 141: U46^#(mark(X)) -> c_141(U46^#(X)) -->_1 U46^#(ok(X)) -> c_142(U46^#(X)) :142 -->_1 U46^#(mark(X)) -> c_141(U46^#(X)) :141 142: U46^#(ok(X)) -> c_142(U46^#(X)) -->_1 U46^#(ok(X)) -> c_142(U46^#(X)) :142 -->_1 U46^#(mark(X)) -> c_141(U46^#(X)) :141 143: U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) -->_1 U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) :144 -->_1 U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) :143 144: U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) -->_1 U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) :144 -->_1 U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) :143 145: U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) -->_1 U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) :146 -->_1 U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) :145 146: U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) -->_1 U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) :146 -->_1 U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) :145 147: U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) -->_1 U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) :148 -->_1 U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) :147 148: U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) -->_1 U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) :148 -->_1 U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) :147 149: U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) -->_1 U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) :150 -->_1 U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) :149 150: U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) -->_1 U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) :150 -->_1 U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) :149 151: U56^#(mark(X)) -> c_153(U56^#(X)) -->_1 U56^#(ok(X)) -> c_154(U56^#(X)) :152 -->_1 U56^#(mark(X)) -> c_153(U56^#(X)) :151 152: U56^#(ok(X)) -> c_154(U56^#(X)) -->_1 U56^#(ok(X)) -> c_154(U56^#(X)) :152 -->_1 U56^#(mark(X)) -> c_153(U56^#(X)) :151 153: U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) :154 -->_1 U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) :153 154: U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) :154 -->_1 U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) :153 155: U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) -->_1 U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) :156 -->_1 U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) :155 156: U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) -->_1 U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) :156 -->_1 U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) :155 157: U63^#(mark(X)) -> c_159(U63^#(X)) -->_1 U63^#(ok(X)) -> c_160(U63^#(X)) :158 -->_1 U63^#(mark(X)) -> c_159(U63^#(X)) :157 158: U63^#(ok(X)) -> c_160(U63^#(X)) -->_1 U63^#(ok(X)) -> c_160(U63^#(X)) :158 -->_1 U63^#(mark(X)) -> c_159(U63^#(X)) :157 159: U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) :160 -->_1 U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) :159 160: U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) :160 -->_1 U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) :159 161: U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) -->_1 U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) :162 -->_1 U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) :161 162: U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) -->_1 U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) :162 -->_1 U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) :161 163: U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) -->_1 U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) :164 -->_1 U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) :163 164: U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) -->_1 U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) :164 -->_1 U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) :163 165: U74^#(mark(X)) -> c_168(U74^#(X)) -->_1 U74^#(ok(X)) -> c_169(U74^#(X)) :166 -->_1 U74^#(mark(X)) -> c_168(U74^#(X)) :165 166: U74^#(ok(X)) -> c_169(U74^#(X)) -->_1 U74^#(ok(X)) -> c_169(U74^#(X)) :166 -->_1 U74^#(mark(X)) -> c_168(U74^#(X)) :165 167: U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) -->_1 U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) :168 -->_1 U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) :167 168: U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) -->_1 U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) :168 -->_1 U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) :167 169: U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) -->_1 U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) :170 -->_1 U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) :169 170: U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) -->_1 U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) :170 -->_1 U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) :169 171: U83^#(mark(X)) -> c_174(U83^#(X)) -->_1 U83^#(ok(X)) -> c_175(U83^#(X)) :172 -->_1 U83^#(mark(X)) -> c_174(U83^#(X)) :171 172: U83^#(ok(X)) -> c_175(U83^#(X)) -->_1 U83^#(ok(X)) -> c_175(U83^#(X)) :172 -->_1 U83^#(mark(X)) -> c_174(U83^#(X)) :171 173: U92^#(mark(X)) -> c_179(U92^#(X)) -->_1 U92^#(ok(X)) -> c_180(U92^#(X)) :174 -->_1 U92^#(mark(X)) -> c_179(U92^#(X)) :173 174: U92^#(ok(X)) -> c_180(U92^#(X)) -->_1 U92^#(ok(X)) -> c_180(U92^#(X)) :174 -->_1 U92^#(mark(X)) -> c_179(U92^#(X)) :173 175: isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :175 176: isNeList^#(ok(X)) -> c_110(isNeList^#(X)) -->_1 isNeList^#(ok(X)) -> c_110(isNeList^#(X)) :176 177: isList^#(ok(X)) -> c_121(isList^#(X)) -->_1 isList^#(ok(X)) -> c_121(isList^#(X)) :177 178: isQid^#(ok(X)) -> c_130(isQid^#(X)) -->_1 isQid^#(ok(X)) -> c_130(isQid^#(X)) :178 179: isPal^#(ok(X)) -> c_167(isPal^#(X)) -->_1 isPal^#(ok(X)) -> c_167(isPal^#(X)) :179 180: isNePal^#(ok(X)) -> c_176(isNePal^#(X)) -->_1 isNePal^#(ok(X)) -> c_176(isNePal^#(X)) :180 181: proper^#(__(X1, X2)) -> c_181(__^#(proper(X1), proper(X2))) -->_1 __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) :102 -->_1 __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) :101 -->_1 __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) :100 182: proper^#(nil()) -> c_182() 183: proper^#(U11(X1, X2)) -> c_183(U11^#(proper(X1), proper(X2))) -->_1 U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) :104 -->_1 U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) :103 184: proper^#(tt()) -> c_184() 185: proper^#(U12(X1, X2)) -> c_185(U12^#(proper(X1), proper(X2))) -->_1 U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) :106 -->_1 U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) :105 186: proper^#(isPalListKind(X)) -> c_186(isPalListKind^#(proper(X))) -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :175 187: proper^#(U13(X)) -> c_187(U13^#(proper(X))) -->_1 U13^#(ok(X)) -> c_109(U13^#(X)) :108 -->_1 U13^#(mark(X)) -> c_108(U13^#(X)) :107 188: proper^#(isNeList(X)) -> c_188(isNeList^#(proper(X))) -->_1 isNeList^#(ok(X)) -> c_110(isNeList^#(X)) :176 189: proper^#(U21(X1, X2, X3)) -> c_189(U21^#(proper(X1), proper(X2), proper(X3))) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) :118 -->_1 U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) :117 190: proper^#(U22(X1, X2, X3)) -> c_190(U22^#(proper(X1), proper(X2), proper(X3))) -->_1 U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) :120 -->_1 U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) :119 191: proper^#(U23(X1, X2, X3)) -> c_191(U23^#(proper(X1), proper(X2), proper(X3))) -->_1 U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) :122 -->_1 U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) :121 192: proper^#(U24(X1, X2, X3)) -> c_192(U24^#(proper(X1), proper(X2), proper(X3))) -->_1 U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) :124 -->_1 U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) :123 193: proper^#(U25(X1, X2)) -> c_193(U25^#(proper(X1), proper(X2))) -->_1 U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) :126 -->_1 U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) :125 194: proper^#(isList(X)) -> c_194(isList^#(proper(X))) -->_1 isList^#(ok(X)) -> c_121(isList^#(X)) :177 195: proper^#(U26(X)) -> c_195(U26^#(proper(X))) -->_1 U26^#(ok(X)) -> c_123(U26^#(X)) :128 -->_1 U26^#(mark(X)) -> c_122(U26^#(X)) :127 196: proper^#(U31(X1, X2)) -> c_196(U31^#(proper(X1), proper(X2))) -->_1 U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) :112 -->_1 U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) :111 197: proper^#(U32(X1, X2)) -> c_197(U32^#(proper(X1), proper(X2))) -->_1 U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) :130 -->_1 U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) :129 198: proper^#(U33(X)) -> c_198(U33^#(proper(X))) -->_1 U33^#(ok(X)) -> c_129(U33^#(X)) :132 -->_1 U33^#(mark(X)) -> c_128(U33^#(X)) :131 199: proper^#(isQid(X)) -> c_199(isQid^#(proper(X))) -->_1 isQid^#(ok(X)) -> c_130(isQid^#(X)) :178 200: proper^#(U41(X1, X2, X3)) -> c_200(U41^#(proper(X1), proper(X2), proper(X3))) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) :114 -->_1 U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) :113 201: proper^#(U42(X1, X2, X3)) -> c_201(U42^#(proper(X1), proper(X2), proper(X3))) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) :134 -->_1 U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) :133 202: proper^#(U43(X1, X2, X3)) -> c_202(U43^#(proper(X1), proper(X2), proper(X3))) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) :136 -->_1 U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) :135 203: proper^#(U44(X1, X2, X3)) -> c_203(U44^#(proper(X1), proper(X2), proper(X3))) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) :138 -->_1 U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) :137 204: proper^#(U45(X1, X2)) -> c_204(U45^#(proper(X1), proper(X2))) -->_1 U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) :140 -->_1 U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) :139 205: proper^#(U46(X)) -> c_205(U46^#(proper(X))) -->_1 U46^#(ok(X)) -> c_142(U46^#(X)) :142 -->_1 U46^#(mark(X)) -> c_141(U46^#(X)) :141 206: proper^#(U51(X1, X2, X3)) -> c_206(U51^#(proper(X1), proper(X2), proper(X3))) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) :116 -->_1 U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) :115 207: proper^#(U52(X1, X2, X3)) -> c_207(U52^#(proper(X1), proper(X2), proper(X3))) -->_1 U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) :144 -->_1 U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) :143 208: proper^#(U53(X1, X2, X3)) -> c_208(U53^#(proper(X1), proper(X2), proper(X3))) -->_1 U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) :146 -->_1 U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) :145 209: proper^#(U54(X1, X2, X3)) -> c_209(U54^#(proper(X1), proper(X2), proper(X3))) -->_1 U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) :148 -->_1 U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) :147 210: proper^#(U55(X1, X2)) -> c_210(U55^#(proper(X1), proper(X2))) -->_1 U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) :150 -->_1 U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) :149 211: proper^#(U56(X)) -> c_211(U56^#(proper(X))) -->_1 U56^#(ok(X)) -> c_154(U56^#(X)) :152 -->_1 U56^#(mark(X)) -> c_153(U56^#(X)) :151 212: proper^#(U61(X1, X2)) -> c_212(U61^#(proper(X1), proper(X2))) -->_1 U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) :154 -->_1 U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) :153 213: proper^#(U62(X1, X2)) -> c_213(U62^#(proper(X1), proper(X2))) -->_1 U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) :156 -->_1 U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) :155 214: proper^#(U63(X)) -> c_214(U63^#(proper(X))) -->_1 U63^#(ok(X)) -> c_160(U63^#(X)) :158 -->_1 U63^#(mark(X)) -> c_159(U63^#(X)) :157 215: proper^#(U71(X1, X2, X3)) -> c_215(U71^#(proper(X1), proper(X2), proper(X3))) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) :160 -->_1 U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) :159 216: proper^#(U72(X1, X2)) -> c_216(U72^#(proper(X1), proper(X2))) -->_1 U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) :162 -->_1 U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) :161 217: proper^#(U73(X1, X2)) -> c_217(U73^#(proper(X1), proper(X2))) -->_1 U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) :164 -->_1 U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) :163 218: proper^#(isPal(X)) -> c_218(isPal^#(proper(X))) -->_1 isPal^#(ok(X)) -> c_167(isPal^#(X)) :179 219: proper^#(U74(X)) -> c_219(U74^#(proper(X))) -->_1 U74^#(ok(X)) -> c_169(U74^#(X)) :166 -->_1 U74^#(mark(X)) -> c_168(U74^#(X)) :165 220: proper^#(U81(X1, X2)) -> c_220(U81^#(proper(X1), proper(X2))) -->_1 U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) :168 -->_1 U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) :167 221: proper^#(U82(X1, X2)) -> c_221(U82^#(proper(X1), proper(X2))) -->_1 U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) :170 -->_1 U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) :169 222: proper^#(U83(X)) -> c_222(U83^#(proper(X))) -->_1 U83^#(ok(X)) -> c_175(U83^#(X)) :172 -->_1 U83^#(mark(X)) -> c_174(U83^#(X)) :171 223: proper^#(isNePal(X)) -> c_223(isNePal^#(proper(X))) -->_1 isNePal^#(ok(X)) -> c_176(isNePal^#(X)) :180 224: proper^#(U91(X1, X2)) -> c_224(U91^#(proper(X1), proper(X2))) -->_1 U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) :110 -->_1 U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) :109 225: proper^#(U92(X)) -> c_225(U92^#(proper(X))) -->_1 U92^#(ok(X)) -> c_180(U92^#(X)) :174 -->_1 U92^#(mark(X)) -> c_179(U92^#(X)) :173 226: proper^#(a()) -> c_226() 227: proper^#(e()) -> c_227() 228: proper^#(i()) -> c_228() 229: proper^#(o()) -> c_229() 230: proper^#(u()) -> c_230() 231: top^#(mark(X)) -> c_231(top^#(proper(X))) -->_1 top^#(ok(X)) -> c_232(top^#(active(X))) :232 -->_1 top^#(mark(X)) -> c_231(top^#(proper(X))) :231 232: top^#(ok(X)) -> c_232(top^#(active(X))) -->_1 top^#(ok(X)) -> c_232(top^#(active(X))) :232 -->_1 top^#(mark(X)) -> c_231(top^#(proper(X))) :231 Only the nodes {100,102,101,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,182,184,226,227,228,229,230,231,232} are reachable from nodes {100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,182,184,226,227,228,229,230,231,232} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) , __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) , __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) , U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) , U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) , U13^#(mark(X)) -> c_108(U13^#(X)) , U13^#(ok(X)) -> c_109(U13^#(X)) , U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) , U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) , U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) , U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) , U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) , U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) , U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) , U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) , U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) , U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) , U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) , U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) , U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) , U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) , U26^#(mark(X)) -> c_122(U26^#(X)) , U26^#(ok(X)) -> c_123(U26^#(X)) , U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) , U33^#(mark(X)) -> c_128(U33^#(X)) , U33^#(ok(X)) -> c_129(U33^#(X)) , U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) , U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) , U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) , U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) , U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) , U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) , U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) , U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) , U46^#(mark(X)) -> c_141(U46^#(X)) , U46^#(ok(X)) -> c_142(U46^#(X)) , U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) , U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) , U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) , U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) , U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) , U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) , U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) , U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) , U56^#(mark(X)) -> c_153(U56^#(X)) , U56^#(ok(X)) -> c_154(U56^#(X)) , U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) , U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) , U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) , U63^#(mark(X)) -> c_159(U63^#(X)) , U63^#(ok(X)) -> c_160(U63^#(X)) , U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) , U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) , U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) , U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) , U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) , U74^#(mark(X)) -> c_168(U74^#(X)) , U74^#(ok(X)) -> c_169(U74^#(X)) , U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) , U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) , U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) , U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) , U83^#(mark(X)) -> c_174(U83^#(X)) , U83^#(ok(X)) -> c_175(U83^#(X)) , U92^#(mark(X)) -> c_179(U92^#(X)) , U92^#(ok(X)) -> c_180(U92^#(X)) , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , isNeList^#(ok(X)) -> c_110(isNeList^#(X)) , isList^#(ok(X)) -> c_121(isList^#(X)) , isQid^#(ok(X)) -> c_130(isQid^#(X)) , isPal^#(ok(X)) -> c_167(isPal^#(X)) , isNePal^#(ok(X)) -> c_176(isNePal^#(X)) , proper^#(nil()) -> c_182() , proper^#(tt()) -> c_184() , proper^#(a()) -> c_226() , proper^#(e()) -> c_227() , proper^#(i()) -> c_228() , proper^#(o()) -> c_229() , proper^#(u()) -> c_230() , top^#(mark(X)) -> c_231(top^#(proper(X))) , top^#(ok(X)) -> c_232(top^#(active(X))) } Strict Trs: { active(__(X1, X2)) -> __(X1, active(X2)) , active(__(X1, X2)) -> __(active(X1), X2) , active(__(X, nil())) -> mark(X) , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(nil(), X)) -> mark(X) , active(U11(X1, X2)) -> U11(active(X1), X2) , active(U11(tt(), V)) -> mark(U12(isPalListKind(V), V)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V)) -> mark(U13(isNeList(V))) , active(isPalListKind(__(V1, V2))) -> mark(U91(isPalListKind(V1), V2)) , active(isPalListKind(nil())) -> mark(tt()) , active(isPalListKind(a())) -> mark(tt()) , active(isPalListKind(e())) -> mark(tt()) , active(isPalListKind(i())) -> mark(tt()) , active(isPalListKind(o())) -> mark(tt()) , active(isPalListKind(u())) -> mark(tt()) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) , active(isNeList(__(V1, V2))) -> mark(U41(isPalListKind(V1), V1, V2)) , active(isNeList(__(V1, V2))) -> mark(U51(isPalListKind(V1), V1, V2)) , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) , active(U21(tt(), V1, V2)) -> mark(U22(isPalListKind(V1), V1, V2)) , active(U22(X1, X2, X3)) -> U22(active(X1), X2, X3) , active(U22(tt(), V1, V2)) -> mark(U23(isPalListKind(V2), V1, V2)) , active(U23(X1, X2, X3)) -> U23(active(X1), X2, X3) , active(U23(tt(), V1, V2)) -> mark(U24(isPalListKind(V2), V1, V2)) , active(U24(X1, X2, X3)) -> U24(active(X1), X2, X3) , active(U24(tt(), V1, V2)) -> mark(U25(isList(V1), V2)) , active(U25(X1, X2)) -> U25(active(X1), X2) , active(U25(tt(), V2)) -> mark(U26(isList(V2))) , active(isList(V)) -> mark(U11(isPalListKind(V), V)) , active(isList(__(V1, V2))) -> mark(U21(isPalListKind(V1), V1, V2)) , active(isList(nil())) -> mark(tt()) , active(U26(X)) -> U26(active(X)) , active(U26(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isPalListKind(V), V)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V)) -> mark(U33(isQid(V))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(isQid(a())) -> mark(tt()) , active(isQid(e())) -> mark(tt()) , active(isQid(i())) -> mark(tt()) , active(isQid(o())) -> mark(tt()) , active(isQid(u())) -> mark(tt()) , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) , active(U41(tt(), V1, V2)) -> mark(U42(isPalListKind(V1), V1, V2)) , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) , active(U42(tt(), V1, V2)) -> mark(U43(isPalListKind(V2), V1, V2)) , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) , active(U43(tt(), V1, V2)) -> mark(U44(isPalListKind(V2), V1, V2)) , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) , active(U44(tt(), V1, V2)) -> mark(U45(isList(V1), V2)) , active(U45(X1, X2)) -> U45(active(X1), X2) , active(U45(tt(), V2)) -> mark(U46(isNeList(V2))) , active(U46(X)) -> U46(active(X)) , active(U46(tt())) -> mark(tt()) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), V1, V2)) -> mark(U52(isPalListKind(V1), V1, V2)) , active(U52(X1, X2, X3)) -> U52(active(X1), X2, X3) , active(U52(tt(), V1, V2)) -> mark(U53(isPalListKind(V2), V1, V2)) , active(U53(X1, X2, X3)) -> U53(active(X1), X2, X3) , active(U53(tt(), V1, V2)) -> mark(U54(isPalListKind(V2), V1, V2)) , active(U54(X1, X2, X3)) -> U54(active(X1), X2, X3) , active(U54(tt(), V1, V2)) -> mark(U55(isNeList(V1), V2)) , active(U55(X1, X2)) -> U55(active(X1), X2) , active(U55(tt(), V2)) -> mark(U56(isList(V2))) , active(U56(X)) -> U56(active(X)) , active(U56(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V)) -> mark(U62(isPalListKind(V), V)) , active(U62(X1, X2)) -> U62(active(X1), X2) , active(U62(tt(), V)) -> mark(U63(isQid(V))) , active(U63(X)) -> U63(active(X)) , active(U63(tt())) -> mark(tt()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), I, P)) -> mark(U72(isPalListKind(I), P)) , active(U72(X1, X2)) -> U72(active(X1), X2) , active(U72(tt(), P)) -> mark(U73(isPal(P), P)) , active(U73(X1, X2)) -> U73(active(X1), X2) , active(U73(tt(), P)) -> mark(U74(isPalListKind(P))) , active(isPal(V)) -> mark(U81(isPalListKind(V), V)) , active(isPal(nil())) -> mark(tt()) , active(U74(X)) -> U74(active(X)) , active(U74(tt())) -> mark(tt()) , active(U81(X1, X2)) -> U81(active(X1), X2) , active(U81(tt(), V)) -> mark(U82(isPalListKind(V), V)) , active(U82(X1, X2)) -> U82(active(X1), X2) , active(U82(tt(), V)) -> mark(U83(isNePal(V))) , active(U83(X)) -> U83(active(X)) , active(U83(tt())) -> mark(tt()) , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) , active(isNePal(__(I, __(P, I)))) -> mark(U71(isQid(I), I, P)) , active(U91(X1, X2)) -> U91(active(X1), X2) , active(U91(tt(), V2)) -> mark(U92(isPalListKind(V2))) , active(U92(X)) -> U92(active(X)) , active(U92(tt())) -> mark(tt()) , __(X1, mark(X2)) -> mark(__(X1, X2)) , __(mark(X1), X2) -> mark(__(X1, X2)) , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) , U11(mark(X1), X2) -> mark(U11(X1, X2)) , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , isPalListKind(ok(X)) -> ok(isPalListKind(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , isNeList(ok(X)) -> ok(isNeList(X)) , U21(mark(X1), X2, X3) -> mark(U21(X1, X2, X3)) , U21(ok(X1), ok(X2), ok(X3)) -> ok(U21(X1, X2, X3)) , U22(mark(X1), X2, X3) -> mark(U22(X1, X2, X3)) , U22(ok(X1), ok(X2), ok(X3)) -> ok(U22(X1, X2, X3)) , U23(mark(X1), X2, X3) -> mark(U23(X1, X2, X3)) , U23(ok(X1), ok(X2), ok(X3)) -> ok(U23(X1, X2, X3)) , U24(mark(X1), X2, X3) -> mark(U24(X1, X2, X3)) , U24(ok(X1), ok(X2), ok(X3)) -> ok(U24(X1, X2, X3)) , U25(mark(X1), X2) -> mark(U25(X1, X2)) , U25(ok(X1), ok(X2)) -> ok(U25(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , U26(mark(X)) -> mark(U26(X)) , U26(ok(X)) -> ok(U26(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , isQid(ok(X)) -> ok(isQid(X)) , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) , U45(mark(X1), X2) -> mark(U45(X1, X2)) , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) , U46(mark(X)) -> mark(U46(X)) , U46(ok(X)) -> ok(U46(X)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , U52(mark(X1), X2, X3) -> mark(U52(X1, X2, X3)) , U52(ok(X1), ok(X2), ok(X3)) -> ok(U52(X1, X2, X3)) , U53(mark(X1), X2, X3) -> mark(U53(X1, X2, X3)) , U53(ok(X1), ok(X2), ok(X3)) -> ok(U53(X1, X2, X3)) , U54(mark(X1), X2, X3) -> mark(U54(X1, X2, X3)) , U54(ok(X1), ok(X2), ok(X3)) -> ok(U54(X1, X2, X3)) , U55(mark(X1), X2) -> mark(U55(X1, X2)) , U55(ok(X1), ok(X2)) -> ok(U55(X1, X2)) , U56(mark(X)) -> mark(U56(X)) , U56(ok(X)) -> ok(U56(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X1), X2) -> mark(U62(X1, X2)) , U62(ok(X1), ok(X2)) -> ok(U62(X1, X2)) , U63(mark(X)) -> mark(U63(X)) , U63(ok(X)) -> ok(U63(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , U72(mark(X1), X2) -> mark(U72(X1, X2)) , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) , U73(mark(X1), X2) -> mark(U73(X1, X2)) , U73(ok(X1), ok(X2)) -> ok(U73(X1, X2)) , isPal(ok(X)) -> ok(isPal(X)) , U74(mark(X)) -> mark(U74(X)) , U74(ok(X)) -> ok(U74(X)) , U81(mark(X1), X2) -> mark(U81(X1, X2)) , U81(ok(X1), ok(X2)) -> ok(U81(X1, X2)) , U82(mark(X1), X2) -> mark(U82(X1, X2)) , U82(ok(X1), ok(X2)) -> ok(U82(X1, X2)) , U83(mark(X)) -> mark(U83(X)) , U83(ok(X)) -> ok(U83(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , U91(mark(X1), X2) -> mark(U91(X1, X2)) , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) , U92(mark(X)) -> mark(U92(X)) , U92(ok(X)) -> ok(U92(X)) , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) , proper(tt()) -> ok(tt()) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(isPalListKind(X)) -> isPalListKind(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(U21(X1, X2, X3)) -> U21(proper(X1), proper(X2), proper(X3)) , proper(U22(X1, X2, X3)) -> U22(proper(X1), proper(X2), proper(X3)) , proper(U23(X1, X2, X3)) -> U23(proper(X1), proper(X2), proper(X3)) , proper(U24(X1, X2, X3)) -> U24(proper(X1), proper(X2), proper(X3)) , proper(U25(X1, X2)) -> U25(proper(X1), proper(X2)) , proper(isList(X)) -> isList(proper(X)) , proper(U26(X)) -> U26(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2, X3)) -> U42(proper(X1), proper(X2), proper(X3)) , proper(U43(X1, X2, X3)) -> U43(proper(X1), proper(X2), proper(X3)) , proper(U44(X1, X2, X3)) -> U44(proper(X1), proper(X2), proper(X3)) , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) , proper(U46(X)) -> U46(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(U52(X1, X2, X3)) -> U52(proper(X1), proper(X2), proper(X3)) , proper(U53(X1, X2, X3)) -> U53(proper(X1), proper(X2), proper(X3)) , proper(U54(X1, X2, X3)) -> U54(proper(X1), proper(X2), proper(X3)) , proper(U55(X1, X2)) -> U55(proper(X1), proper(X2)) , proper(U56(X)) -> U56(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X1, X2)) -> U62(proper(X1), proper(X2)) , proper(U63(X)) -> U63(proper(X)) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) , proper(U73(X1, X2)) -> U73(proper(X1), proper(X2)) , proper(isPal(X)) -> isPal(proper(X)) , proper(U74(X)) -> U74(proper(X)) , proper(U81(X1, X2)) -> U81(proper(X1), proper(X2)) , proper(U82(X1, X2)) -> U82(proper(X1), proper(X2)) , proper(U83(X)) -> U83(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) , proper(U92(X)) -> U92(proper(X)) , proper(a()) -> ok(a()) , proper(e()) -> ok(e()) , proper(i()) -> ok(i()) , proper(o()) -> ok(o()) , proper(u()) -> ok(u()) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {82,83,84,85,86,87,88} by applications of Pre({82,83,84,85,86,87,88}) = {}. Here rules are labeled as follows: DPs: { 1: __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) , 2: __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) , 3: __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) , 4: U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) , 5: U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) , 6: U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) , 7: U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) , 8: U13^#(mark(X)) -> c_108(U13^#(X)) , 9: U13^#(ok(X)) -> c_109(U13^#(X)) , 10: U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) , 11: U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) , 12: U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) , 13: U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) , 14: U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) , 15: U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) , 16: U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) , 17: U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) , 18: U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) , 19: U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) , 20: U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) , 21: U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) , 22: U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) , 23: U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) , 24: U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) , 25: U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) , 26: U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) , 27: U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) , 28: U26^#(mark(X)) -> c_122(U26^#(X)) , 29: U26^#(ok(X)) -> c_123(U26^#(X)) , 30: U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) , 31: U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) , 32: U33^#(mark(X)) -> c_128(U33^#(X)) , 33: U33^#(ok(X)) -> c_129(U33^#(X)) , 34: U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) , 35: U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) , 36: U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) , 37: U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) , 38: U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) , 39: U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) , 40: U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) , 41: U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) , 42: U46^#(mark(X)) -> c_141(U46^#(X)) , 43: U46^#(ok(X)) -> c_142(U46^#(X)) , 44: U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) , 45: U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) , 46: U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) , 47: U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) , 48: U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) , 49: U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) , 50: U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) , 51: U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) , 52: U56^#(mark(X)) -> c_153(U56^#(X)) , 53: U56^#(ok(X)) -> c_154(U56^#(X)) , 54: U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) , 55: U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) , 56: U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) , 57: U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) , 58: U63^#(mark(X)) -> c_159(U63^#(X)) , 59: U63^#(ok(X)) -> c_160(U63^#(X)) , 60: U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) , 61: U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) , 62: U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) , 63: U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) , 64: U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) , 65: U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) , 66: U74^#(mark(X)) -> c_168(U74^#(X)) , 67: U74^#(ok(X)) -> c_169(U74^#(X)) , 68: U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) , 69: U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) , 70: U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) , 71: U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) , 72: U83^#(mark(X)) -> c_174(U83^#(X)) , 73: U83^#(ok(X)) -> c_175(U83^#(X)) , 74: U92^#(mark(X)) -> c_179(U92^#(X)) , 75: U92^#(ok(X)) -> c_180(U92^#(X)) , 76: isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , 77: isNeList^#(ok(X)) -> c_110(isNeList^#(X)) , 78: isList^#(ok(X)) -> c_121(isList^#(X)) , 79: isQid^#(ok(X)) -> c_130(isQid^#(X)) , 80: isPal^#(ok(X)) -> c_167(isPal^#(X)) , 81: isNePal^#(ok(X)) -> c_176(isNePal^#(X)) , 82: proper^#(nil()) -> c_182() , 83: proper^#(tt()) -> c_184() , 84: proper^#(a()) -> c_226() , 85: proper^#(e()) -> c_227() , 86: proper^#(i()) -> c_228() , 87: proper^#(o()) -> c_229() , 88: proper^#(u()) -> c_230() , 89: top^#(mark(X)) -> c_231(top^#(proper(X))) , 90: top^#(ok(X)) -> c_232(top^#(active(X))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, mark(X2)) -> c_100(__^#(X1, X2)) , __^#(mark(X1), X2) -> c_101(__^#(X1, X2)) , __^#(ok(X1), ok(X2)) -> c_102(__^#(X1, X2)) , U11^#(mark(X1), X2) -> c_103(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_104(U11^#(X1, X2)) , U12^#(mark(X1), X2) -> c_105(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_106(U12^#(X1, X2)) , U13^#(mark(X)) -> c_108(U13^#(X)) , U13^#(ok(X)) -> c_109(U13^#(X)) , U91^#(mark(X1), X2) -> c_177(U91^#(X1, X2)) , U91^#(ok(X1), ok(X2)) -> c_178(U91^#(X1, X2)) , U31^#(mark(X1), X2) -> c_124(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_125(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_131(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_132(U41^#(X1, X2, X3)) , U51^#(mark(X1), X2, X3) -> c_143(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_144(U51^#(X1, X2, X3)) , U21^#(mark(X1), X2, X3) -> c_111(U21^#(X1, X2, X3)) , U21^#(ok(X1), ok(X2), ok(X3)) -> c_112(U21^#(X1, X2, X3)) , U22^#(mark(X1), X2, X3) -> c_113(U22^#(X1, X2, X3)) , U22^#(ok(X1), ok(X2), ok(X3)) -> c_114(U22^#(X1, X2, X3)) , U23^#(mark(X1), X2, X3) -> c_115(U23^#(X1, X2, X3)) , U23^#(ok(X1), ok(X2), ok(X3)) -> c_116(U23^#(X1, X2, X3)) , U24^#(mark(X1), X2, X3) -> c_117(U24^#(X1, X2, X3)) , U24^#(ok(X1), ok(X2), ok(X3)) -> c_118(U24^#(X1, X2, X3)) , U25^#(mark(X1), X2) -> c_119(U25^#(X1, X2)) , U25^#(ok(X1), ok(X2)) -> c_120(U25^#(X1, X2)) , U26^#(mark(X)) -> c_122(U26^#(X)) , U26^#(ok(X)) -> c_123(U26^#(X)) , U32^#(mark(X1), X2) -> c_126(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_127(U32^#(X1, X2)) , U33^#(mark(X)) -> c_128(U33^#(X)) , U33^#(ok(X)) -> c_129(U33^#(X)) , U42^#(mark(X1), X2, X3) -> c_133(U42^#(X1, X2, X3)) , U42^#(ok(X1), ok(X2), ok(X3)) -> c_134(U42^#(X1, X2, X3)) , U43^#(mark(X1), X2, X3) -> c_135(U43^#(X1, X2, X3)) , U43^#(ok(X1), ok(X2), ok(X3)) -> c_136(U43^#(X1, X2, X3)) , U44^#(mark(X1), X2, X3) -> c_137(U44^#(X1, X2, X3)) , U44^#(ok(X1), ok(X2), ok(X3)) -> c_138(U44^#(X1, X2, X3)) , U45^#(mark(X1), X2) -> c_139(U45^#(X1, X2)) , U45^#(ok(X1), ok(X2)) -> c_140(U45^#(X1, X2)) , U46^#(mark(X)) -> c_141(U46^#(X)) , U46^#(ok(X)) -> c_142(U46^#(X)) , U52^#(mark(X1), X2, X3) -> c_145(U52^#(X1, X2, X3)) , U52^#(ok(X1), ok(X2), ok(X3)) -> c_146(U52^#(X1, X2, X3)) , U53^#(mark(X1), X2, X3) -> c_147(U53^#(X1, X2, X3)) , U53^#(ok(X1), ok(X2), ok(X3)) -> c_148(U53^#(X1, X2, X3)) , U54^#(mark(X1), X2, X3) -> c_149(U54^#(X1, X2, X3)) , U54^#(ok(X1), ok(X2), ok(X3)) -> c_150(U54^#(X1, X2, X3)) , U55^#(mark(X1), X2) -> c_151(U55^#(X1, X2)) , U55^#(ok(X1), ok(X2)) -> c_152(U55^#(X1, X2)) , U56^#(mark(X)) -> c_153(U56^#(X)) , U56^#(ok(X)) -> c_154(U56^#(X)) , U61^#(mark(X1), X2) -> c_155(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_156(U61^#(X1, X2)) , U62^#(mark(X1), X2) -> c_157(U62^#(X1, X2)) , U62^#(ok(X1), ok(X2)) -> c_158(U62^#(X1, X2)) , U63^#(mark(X)) -> c_159(U63^#(X)) , U63^#(ok(X)) -> c_160(U63^#(X)) , U71^#(mark(X1), X2, X3) -> c_161(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_162(U71^#(X1, X2, X3)) , U72^#(mark(X1), X2) -> c_163(U72^#(X1, X2)) , U72^#(ok(X1), ok(X2)) -> c_164(U72^#(X1, X2)) , U73^#(mark(X1), X2) -> c_165(U73^#(X1, X2)) , U73^#(ok(X1), ok(X2)) -> c_166(U73^#(X1, X2)) , U74^#(mark(X)) -> c_168(U74^#(X)) , U74^#(ok(X)) -> c_169(U74^#(X)) , U81^#(mark(X1), X2) -> c_170(U81^#(X1, X2)) , U81^#(ok(X1), ok(X2)) -> c_171(U81^#(X1, X2)) , U82^#(mark(X1), X2) -> c_172(U82^#(X1, X2)) , U82^#(ok(X1), ok(X2)) -> c_173(U82^#(X1, X2)) , U83^#(mark(X)) -> c_174(U83^#(X)) , U83^#(ok(X)) -> c_175(U83^#(X)) , U92^#(mark(X)) -> c_179(U92^#(X)) , U92^#(ok(X)) -> c_180(U92^#(X)) , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , isNeList^#(ok(X)) -> c_110(isNeList^#(X)) , isList^#(ok(X)) -> c_121(isList^#(X)) , isQid^#(ok(X)) -> c_130(isQid^#(X)) , isPal^#(ok(X)) -> c_167(isPal^#(X)) , isNePal^#(ok(X)) -> c_176(isNePal^#(X)) , top^#(mark(X)) -> c_231(top^#(proper(X))) , top^#(ok(X)) -> c_232(top^#(active(X))) } Strict Trs: { active(__(X1, X2)) -> __(X1, active(X2)) , active(__(X1, X2)) -> __(active(X1), X2) , active(__(X, nil())) -> mark(X) , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(nil(), X)) -> mark(X) , active(U11(X1, X2)) -> U11(active(X1), X2) , active(U11(tt(), V)) -> mark(U12(isPalListKind(V), V)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V)) -> mark(U13(isNeList(V))) , active(isPalListKind(__(V1, V2))) -> mark(U91(isPalListKind(V1), V2)) , active(isPalListKind(nil())) -> mark(tt()) , active(isPalListKind(a())) -> mark(tt()) , active(isPalListKind(e())) -> mark(tt()) , active(isPalListKind(i())) -> mark(tt()) , active(isPalListKind(o())) -> mark(tt()) , active(isPalListKind(u())) -> mark(tt()) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) , active(isNeList(__(V1, V2))) -> mark(U41(isPalListKind(V1), V1, V2)) , active(isNeList(__(V1, V2))) -> mark(U51(isPalListKind(V1), V1, V2)) , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) , active(U21(tt(), V1, V2)) -> mark(U22(isPalListKind(V1), V1, V2)) , active(U22(X1, X2, X3)) -> U22(active(X1), X2, X3) , active(U22(tt(), V1, V2)) -> mark(U23(isPalListKind(V2), V1, V2)) , active(U23(X1, X2, X3)) -> U23(active(X1), X2, X3) , active(U23(tt(), V1, V2)) -> mark(U24(isPalListKind(V2), V1, V2)) , active(U24(X1, X2, X3)) -> U24(active(X1), X2, X3) , active(U24(tt(), V1, V2)) -> mark(U25(isList(V1), V2)) , active(U25(X1, X2)) -> U25(active(X1), X2) , active(U25(tt(), V2)) -> mark(U26(isList(V2))) , active(isList(V)) -> mark(U11(isPalListKind(V), V)) , active(isList(__(V1, V2))) -> mark(U21(isPalListKind(V1), V1, V2)) , active(isList(nil())) -> mark(tt()) , active(U26(X)) -> U26(active(X)) , active(U26(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isPalListKind(V), V)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V)) -> mark(U33(isQid(V))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(isQid(a())) -> mark(tt()) , active(isQid(e())) -> mark(tt()) , active(isQid(i())) -> mark(tt()) , active(isQid(o())) -> mark(tt()) , active(isQid(u())) -> mark(tt()) , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) , active(U41(tt(), V1, V2)) -> mark(U42(isPalListKind(V1), V1, V2)) , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) , active(U42(tt(), V1, V2)) -> mark(U43(isPalListKind(V2), V1, V2)) , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) , active(U43(tt(), V1, V2)) -> mark(U44(isPalListKind(V2), V1, V2)) , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) , active(U44(tt(), V1, V2)) -> mark(U45(isList(V1), V2)) , active(U45(X1, X2)) -> U45(active(X1), X2) , active(U45(tt(), V2)) -> mark(U46(isNeList(V2))) , active(U46(X)) -> U46(active(X)) , active(U46(tt())) -> mark(tt()) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), V1, V2)) -> mark(U52(isPalListKind(V1), V1, V2)) , active(U52(X1, X2, X3)) -> U52(active(X1), X2, X3) , active(U52(tt(), V1, V2)) -> mark(U53(isPalListKind(V2), V1, V2)) , active(U53(X1, X2, X3)) -> U53(active(X1), X2, X3) , active(U53(tt(), V1, V2)) -> mark(U54(isPalListKind(V2), V1, V2)) , active(U54(X1, X2, X3)) -> U54(active(X1), X2, X3) , active(U54(tt(), V1, V2)) -> mark(U55(isNeList(V1), V2)) , active(U55(X1, X2)) -> U55(active(X1), X2) , active(U55(tt(), V2)) -> mark(U56(isList(V2))) , active(U56(X)) -> U56(active(X)) , active(U56(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V)) -> mark(U62(isPalListKind(V), V)) , active(U62(X1, X2)) -> U62(active(X1), X2) , active(U62(tt(), V)) -> mark(U63(isQid(V))) , active(U63(X)) -> U63(active(X)) , active(U63(tt())) -> mark(tt()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), I, P)) -> mark(U72(isPalListKind(I), P)) , active(U72(X1, X2)) -> U72(active(X1), X2) , active(U72(tt(), P)) -> mark(U73(isPal(P), P)) , active(U73(X1, X2)) -> U73(active(X1), X2) , active(U73(tt(), P)) -> mark(U74(isPalListKind(P))) , active(isPal(V)) -> mark(U81(isPalListKind(V), V)) , active(isPal(nil())) -> mark(tt()) , active(U74(X)) -> U74(active(X)) , active(U74(tt())) -> mark(tt()) , active(U81(X1, X2)) -> U81(active(X1), X2) , active(U81(tt(), V)) -> mark(U82(isPalListKind(V), V)) , active(U82(X1, X2)) -> U82(active(X1), X2) , active(U82(tt(), V)) -> mark(U83(isNePal(V))) , active(U83(X)) -> U83(active(X)) , active(U83(tt())) -> mark(tt()) , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) , active(isNePal(__(I, __(P, I)))) -> mark(U71(isQid(I), I, P)) , active(U91(X1, X2)) -> U91(active(X1), X2) , active(U91(tt(), V2)) -> mark(U92(isPalListKind(V2))) , active(U92(X)) -> U92(active(X)) , active(U92(tt())) -> mark(tt()) , __(X1, mark(X2)) -> mark(__(X1, X2)) , __(mark(X1), X2) -> mark(__(X1, X2)) , __(ok(X1), ok(X2)) -> ok(__(X1, X2)) , U11(mark(X1), X2) -> mark(U11(X1, X2)) , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , isPalListKind(ok(X)) -> ok(isPalListKind(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , isNeList(ok(X)) -> ok(isNeList(X)) , U21(mark(X1), X2, X3) -> mark(U21(X1, X2, X3)) , U21(ok(X1), ok(X2), ok(X3)) -> ok(U21(X1, X2, X3)) , U22(mark(X1), X2, X3) -> mark(U22(X1, X2, X3)) , U22(ok(X1), ok(X2), ok(X3)) -> ok(U22(X1, X2, X3)) , U23(mark(X1), X2, X3) -> mark(U23(X1, X2, X3)) , U23(ok(X1), ok(X2), ok(X3)) -> ok(U23(X1, X2, X3)) , U24(mark(X1), X2, X3) -> mark(U24(X1, X2, X3)) , U24(ok(X1), ok(X2), ok(X3)) -> ok(U24(X1, X2, X3)) , U25(mark(X1), X2) -> mark(U25(X1, X2)) , U25(ok(X1), ok(X2)) -> ok(U25(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , U26(mark(X)) -> mark(U26(X)) , U26(ok(X)) -> ok(U26(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , isQid(ok(X)) -> ok(isQid(X)) , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) , U45(mark(X1), X2) -> mark(U45(X1, X2)) , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) , U46(mark(X)) -> mark(U46(X)) , U46(ok(X)) -> ok(U46(X)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , U52(mark(X1), X2, X3) -> mark(U52(X1, X2, X3)) , U52(ok(X1), ok(X2), ok(X3)) -> ok(U52(X1, X2, X3)) , U53(mark(X1), X2, X3) -> mark(U53(X1, X2, X3)) , U53(ok(X1), ok(X2), ok(X3)) -> ok(U53(X1, X2, X3)) , U54(mark(X1), X2, X3) -> mark(U54(X1, X2, X3)) , U54(ok(X1), ok(X2), ok(X3)) -> ok(U54(X1, X2, X3)) , U55(mark(X1), X2) -> mark(U55(X1, X2)) , U55(ok(X1), ok(X2)) -> ok(U55(X1, X2)) , U56(mark(X)) -> mark(U56(X)) , U56(ok(X)) -> ok(U56(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X1), X2) -> mark(U62(X1, X2)) , U62(ok(X1), ok(X2)) -> ok(U62(X1, X2)) , U63(mark(X)) -> mark(U63(X)) , U63(ok(X)) -> ok(U63(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , U72(mark(X1), X2) -> mark(U72(X1, X2)) , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) , U73(mark(X1), X2) -> mark(U73(X1, X2)) , U73(ok(X1), ok(X2)) -> ok(U73(X1, X2)) , isPal(ok(X)) -> ok(isPal(X)) , U74(mark(X)) -> mark(U74(X)) , U74(ok(X)) -> ok(U74(X)) , U81(mark(X1), X2) -> mark(U81(X1, X2)) , U81(ok(X1), ok(X2)) -> ok(U81(X1, X2)) , U82(mark(X1), X2) -> mark(U82(X1, X2)) , U82(ok(X1), ok(X2)) -> ok(U82(X1, X2)) , U83(mark(X)) -> mark(U83(X)) , U83(ok(X)) -> ok(U83(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , U91(mark(X1), X2) -> mark(U91(X1, X2)) , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) , U92(mark(X)) -> mark(U92(X)) , U92(ok(X)) -> ok(U92(X)) , proper(__(X1, X2)) -> __(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) , proper(tt()) -> ok(tt()) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(isPalListKind(X)) -> isPalListKind(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(U21(X1, X2, X3)) -> U21(proper(X1), proper(X2), proper(X3)) , proper(U22(X1, X2, X3)) -> U22(proper(X1), proper(X2), proper(X3)) , proper(U23(X1, X2, X3)) -> U23(proper(X1), proper(X2), proper(X3)) , proper(U24(X1, X2, X3)) -> U24(proper(X1), proper(X2), proper(X3)) , proper(U25(X1, X2)) -> U25(proper(X1), proper(X2)) , proper(isList(X)) -> isList(proper(X)) , proper(U26(X)) -> U26(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2, X3)) -> U42(proper(X1), proper(X2), proper(X3)) , proper(U43(X1, X2, X3)) -> U43(proper(X1), proper(X2), proper(X3)) , proper(U44(X1, X2, X3)) -> U44(proper(X1), proper(X2), proper(X3)) , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) , proper(U46(X)) -> U46(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(U52(X1, X2, X3)) -> U52(proper(X1), proper(X2), proper(X3)) , proper(U53(X1, X2, X3)) -> U53(proper(X1), proper(X2), proper(X3)) , proper(U54(X1, X2, X3)) -> U54(proper(X1), proper(X2), proper(X3)) , proper(U55(X1, X2)) -> U55(proper(X1), proper(X2)) , proper(U56(X)) -> U56(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X1, X2)) -> U62(proper(X1), proper(X2)) , proper(U63(X)) -> U63(proper(X)) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) , proper(U73(X1, X2)) -> U73(proper(X1), proper(X2)) , proper(isPal(X)) -> isPal(proper(X)) , proper(U74(X)) -> U74(proper(X)) , proper(U81(X1, X2)) -> U81(proper(X1), proper(X2)) , proper(U82(X1, X2)) -> U82(proper(X1), proper(X2)) , proper(U83(X)) -> U83(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) , proper(U92(X)) -> U92(proper(X)) , proper(a()) -> ok(a()) , proper(e()) -> ok(e()) , proper(i()) -> ok(i()) , proper(o()) -> ok(o()) , proper(u()) -> ok(u()) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Weak DPs: { proper^#(nil()) -> c_182() , proper^#(tt()) -> c_184() , proper^#(a()) -> c_226() , proper^#(e()) -> c_227() , proper^#(i()) -> c_228() , proper^#(o()) -> c_229() , proper^#(u()) -> c_230() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..