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(isNeList(V))) , active(U12(X)) -> U12(active(X)) , active(U12(tt())) -> mark(tt()) , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) , active(isNeList(__(V1, V2))) -> mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(isNeList(__(V1, V2))) -> mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) , active(U21(tt(), V1, V2)) -> mark(U22(isList(V1), V2)) , active(U22(X1, X2)) -> U22(active(X1), X2) , active(U22(tt(), V2)) -> mark(U23(isList(V2))) , active(isList(V)) -> mark(U11(isPalListKind(V), V)) , active(isList(__(V1, V2))) -> mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(isList(nil())) -> mark(tt()) , active(U23(X)) -> U23(active(X)) , active(U23(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isQid(V))) , active(U32(X)) -> U32(active(X)) , active(U32(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(isList(V1), V2)) , active(U42(X1, X2)) -> U42(active(X1), X2) , active(U42(tt(), V2)) -> mark(U43(isNeList(V2))) , active(U43(X)) -> U43(active(X)) , active(U43(tt())) -> mark(tt()) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), V1, V2)) -> mark(U52(isNeList(V1), V2)) , active(U52(X1, X2)) -> U52(active(X1), X2) , active(U52(tt(), V2)) -> mark(U53(isList(V2))) , active(U53(X)) -> U53(active(X)) , active(U53(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V)) -> mark(U62(isQid(V))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X1, X2)) -> U71(active(X1), X2) , active(U71(tt(), V)) -> mark(U72(isNePal(V))) , active(U72(X)) -> U72(active(X)) , active(U72(tt())) -> mark(tt()) , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) , active(isNePal(__(I, __(P, I)))) -> mark(and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isPalListKind(__(V1, V2))) -> mark(and(isPalListKind(V1), isPalListKind(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(isPal(V)) -> mark(U71(isPalListKind(V), V)) , active(isPal(nil())) -> 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(X)) -> mark(U12(X)) , U12(ok(X)) -> ok(U12(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) -> mark(U22(X1, X2)) , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , U23(mark(X)) -> mark(U23(X)) , U23(ok(X)) -> ok(U23(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X)) -> mark(U32(X)) , U32(ok(X)) -> ok(U32(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) -> mark(U42(X1, X2)) , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) , U43(mark(X)) -> mark(U43(X)) , U43(ok(X)) -> ok(U43(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) -> mark(U52(X1, X2)) , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) , U53(mark(X)) -> mark(U53(X)) , U53(ok(X)) -> ok(U53(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X1), X2) -> mark(U71(X1, X2)) , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) , U72(mark(X)) -> mark(U72(X)) , U72(ok(X)) -> ok(U72(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isPalListKind(ok(X)) -> ok(isPalListKind(X)) , isPal(ok(X)) -> ok(isPal(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(X)) -> U12(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(U21(X1, X2, X3)) -> U21(proper(X1), proper(X2), proper(X3)) , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) , proper(isList(X)) -> isList(proper(X)) , proper(U23(X)) -> U23(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X)) -> U32(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) , proper(U43(X)) -> U43(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) , proper(U53(X)) -> U53(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) , proper(U72(X)) -> U72(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isPalListKind(X)) -> isPalListKind(proper(X)) , proper(isPal(X)) -> isPal(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) '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) '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) '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^#(isNeList(V))) , active^#(U12(X)) -> c_8(U12^#(active(X))) , active^#(U12(tt())) -> c_9() , active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) , active^#(isNeList(__(V1, V2))) -> c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active^#(isNeList(__(V1, V2))) -> c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) , active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) , active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) , active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) , active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) , active^#(isList(__(V1, V2))) -> c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active^#(isList(nil())) -> c_19() , active^#(U23(X)) -> c_20(U23^#(active(X))) , active^#(U23(tt())) -> c_21() , active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) , active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) , active^#(U32(X)) -> c_24(U32^#(active(X))) , active^#(U32(tt())) -> c_25() , active^#(isQid(a())) -> c_26() , active^#(isQid(e())) -> c_27() , active^#(isQid(i())) -> c_28() , active^#(isQid(o())) -> c_29() , active^#(isQid(u())) -> c_30() , active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) , active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) , active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) , active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) , active^#(U43(X)) -> c_35(U43^#(active(X))) , active^#(U43(tt())) -> c_36() , active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) , active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) , active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) , active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) , active^#(U53(X)) -> c_41(U53^#(active(X))) , active^#(U53(tt())) -> c_42() , active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) , active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) , active^#(U62(X)) -> c_45(U62^#(active(X))) , active^#(U62(tt())) -> c_46() , active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) , active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) , active^#(U72(X)) -> c_49(U72^#(active(X))) , active^#(U72(tt())) -> c_50() , active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) , active^#(isNePal(__(I, __(P, I)))) -> c_52(and^#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) , active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) , active^#(and(tt(), X)) -> c_54(X) , active^#(isPalListKind(__(V1, V2))) -> c_55(and^#(isPalListKind(V1), isPalListKind(V2))) , active^#(isPalListKind(nil())) -> c_56() , active^#(isPalListKind(a())) -> c_57() , active^#(isPalListKind(e())) -> c_58() , active^#(isPalListKind(i())) -> c_59() , active^#(isPalListKind(o())) -> c_60() , active^#(isPalListKind(u())) -> c_61() , active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) , active^#(isPal(nil())) -> c_63() , __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) , __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) , __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) , U12^#(mark(X)) -> c_69(U12^#(X)) , U12^#(ok(X)) -> c_70(U12^#(X)) , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) , U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) , U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) , U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) , U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) , U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) , U23^#(mark(X)) -> c_77(U23^#(X)) , U23^#(ok(X)) -> c_78(U23^#(X)) , U32^#(mark(X)) -> c_81(U32^#(X)) , U32^#(ok(X)) -> c_82(U32^#(X)) , U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) , U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) , U43^#(mark(X)) -> c_88(U43^#(X)) , U43^#(ok(X)) -> c_89(U43^#(X)) , U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) , U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) , U53^#(mark(X)) -> c_94(U53^#(X)) , U53^#(ok(X)) -> c_95(U53^#(X)) , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , U62^#(mark(X)) -> c_98(U62^#(X)) , U62^#(ok(X)) -> c_99(U62^#(X)) , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) , U72^#(mark(X)) -> c_102(U72^#(X)) , U72^#(ok(X)) -> c_103(U72^#(X)) , and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) , isNeList^#(ok(X)) -> c_71(isNeList^#(X)) , isList^#(ok(X)) -> c_76(isList^#(X)) , isQid^#(ok(X)) -> c_83(isQid^#(X)) , isNePal^#(ok(X)) -> c_104(isNePal^#(X)) , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , isPal^#(ok(X)) -> c_108(isPal^#(X)) , proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) , proper^#(nil()) -> c_110() , proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) , proper^#(tt()) -> c_112() , proper^#(U12(X)) -> c_113(U12^#(proper(X))) , proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) , proper^#(U21(X1, X2, X3)) -> c_115(U21^#(proper(X1), proper(X2), proper(X3))) , proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) , proper^#(isList(X)) -> c_117(isList^#(proper(X))) , proper^#(U23(X)) -> c_118(U23^#(proper(X))) , proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) , proper^#(U32(X)) -> c_120(U32^#(proper(X))) , proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) , proper^#(U41(X1, X2, X3)) -> c_122(U41^#(proper(X1), proper(X2), proper(X3))) , proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) , proper^#(U43(X)) -> c_124(U43^#(proper(X))) , proper^#(U51(X1, X2, X3)) -> c_125(U51^#(proper(X1), proper(X2), proper(X3))) , proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) , proper^#(U53(X)) -> c_127(U53^#(proper(X))) , proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) , proper^#(U62(X)) -> c_129(U62^#(proper(X))) , proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) , proper^#(U72(X)) -> c_131(U72^#(proper(X))) , proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) , proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) , proper^#(isPalListKind(X)) -> c_134(isPalListKind^#(proper(X))) , proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) , proper^#(a()) -> c_136() , proper^#(e()) -> c_137() , proper^#(i()) -> c_138() , proper^#(o()) -> c_139() , proper^#(u()) -> c_140() , top^#(mark(X)) -> c_141(top^#(proper(X))) , top^#(ok(X)) -> c_142(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^#(isNeList(V))) , active^#(U12(X)) -> c_8(U12^#(active(X))) , active^#(U12(tt())) -> c_9() , active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) , active^#(isNeList(__(V1, V2))) -> c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active^#(isNeList(__(V1, V2))) -> c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) , active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) , active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) , active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) , active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) , active^#(isList(__(V1, V2))) -> c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active^#(isList(nil())) -> c_19() , active^#(U23(X)) -> c_20(U23^#(active(X))) , active^#(U23(tt())) -> c_21() , active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) , active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) , active^#(U32(X)) -> c_24(U32^#(active(X))) , active^#(U32(tt())) -> c_25() , active^#(isQid(a())) -> c_26() , active^#(isQid(e())) -> c_27() , active^#(isQid(i())) -> c_28() , active^#(isQid(o())) -> c_29() , active^#(isQid(u())) -> c_30() , active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) , active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) , active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) , active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) , active^#(U43(X)) -> c_35(U43^#(active(X))) , active^#(U43(tt())) -> c_36() , active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) , active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) , active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) , active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) , active^#(U53(X)) -> c_41(U53^#(active(X))) , active^#(U53(tt())) -> c_42() , active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) , active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) , active^#(U62(X)) -> c_45(U62^#(active(X))) , active^#(U62(tt())) -> c_46() , active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) , active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) , active^#(U72(X)) -> c_49(U72^#(active(X))) , active^#(U72(tt())) -> c_50() , active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) , active^#(isNePal(__(I, __(P, I)))) -> c_52(and^#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) , active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) , active^#(and(tt(), X)) -> c_54(X) , active^#(isPalListKind(__(V1, V2))) -> c_55(and^#(isPalListKind(V1), isPalListKind(V2))) , active^#(isPalListKind(nil())) -> c_56() , active^#(isPalListKind(a())) -> c_57() , active^#(isPalListKind(e())) -> c_58() , active^#(isPalListKind(i())) -> c_59() , active^#(isPalListKind(o())) -> c_60() , active^#(isPalListKind(u())) -> c_61() , active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) , active^#(isPal(nil())) -> c_63() , __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) , __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) , __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) , U12^#(mark(X)) -> c_69(U12^#(X)) , U12^#(ok(X)) -> c_70(U12^#(X)) , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) , U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) , U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) , U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) , U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) , U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) , U23^#(mark(X)) -> c_77(U23^#(X)) , U23^#(ok(X)) -> c_78(U23^#(X)) , U32^#(mark(X)) -> c_81(U32^#(X)) , U32^#(ok(X)) -> c_82(U32^#(X)) , U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) , U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) , U43^#(mark(X)) -> c_88(U43^#(X)) , U43^#(ok(X)) -> c_89(U43^#(X)) , U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) , U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) , U53^#(mark(X)) -> c_94(U53^#(X)) , U53^#(ok(X)) -> c_95(U53^#(X)) , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , U62^#(mark(X)) -> c_98(U62^#(X)) , U62^#(ok(X)) -> c_99(U62^#(X)) , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) , U72^#(mark(X)) -> c_102(U72^#(X)) , U72^#(ok(X)) -> c_103(U72^#(X)) , and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) , isNeList^#(ok(X)) -> c_71(isNeList^#(X)) , isList^#(ok(X)) -> c_76(isList^#(X)) , isQid^#(ok(X)) -> c_83(isQid^#(X)) , isNePal^#(ok(X)) -> c_104(isNePal^#(X)) , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , isPal^#(ok(X)) -> c_108(isPal^#(X)) , proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) , proper^#(nil()) -> c_110() , proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) , proper^#(tt()) -> c_112() , proper^#(U12(X)) -> c_113(U12^#(proper(X))) , proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) , proper^#(U21(X1, X2, X3)) -> c_115(U21^#(proper(X1), proper(X2), proper(X3))) , proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) , proper^#(isList(X)) -> c_117(isList^#(proper(X))) , proper^#(U23(X)) -> c_118(U23^#(proper(X))) , proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) , proper^#(U32(X)) -> c_120(U32^#(proper(X))) , proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) , proper^#(U41(X1, X2, X3)) -> c_122(U41^#(proper(X1), proper(X2), proper(X3))) , proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) , proper^#(U43(X)) -> c_124(U43^#(proper(X))) , proper^#(U51(X1, X2, X3)) -> c_125(U51^#(proper(X1), proper(X2), proper(X3))) , proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) , proper^#(U53(X)) -> c_127(U53^#(proper(X))) , proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) , proper^#(U62(X)) -> c_129(U62^#(proper(X))) , proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) , proper^#(U72(X)) -> c_131(U72^#(proper(X))) , proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) , proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) , proper^#(isPalListKind(X)) -> c_134(isPalListKind^#(proper(X))) , proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) , proper^#(a()) -> c_136() , proper^#(e()) -> c_137() , proper^#(i()) -> c_138() , proper^#(o()) -> c_139() , proper^#(u()) -> c_140() , top^#(mark(X)) -> c_141(top^#(proper(X))) , top^#(ok(X)) -> c_142(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(isNeList(V))) , active(U12(X)) -> U12(active(X)) , active(U12(tt())) -> mark(tt()) , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) , active(isNeList(__(V1, V2))) -> mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(isNeList(__(V1, V2))) -> mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) , active(U21(tt(), V1, V2)) -> mark(U22(isList(V1), V2)) , active(U22(X1, X2)) -> U22(active(X1), X2) , active(U22(tt(), V2)) -> mark(U23(isList(V2))) , active(isList(V)) -> mark(U11(isPalListKind(V), V)) , active(isList(__(V1, V2))) -> mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(isList(nil())) -> mark(tt()) , active(U23(X)) -> U23(active(X)) , active(U23(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isQid(V))) , active(U32(X)) -> U32(active(X)) , active(U32(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(isList(V1), V2)) , active(U42(X1, X2)) -> U42(active(X1), X2) , active(U42(tt(), V2)) -> mark(U43(isNeList(V2))) , active(U43(X)) -> U43(active(X)) , active(U43(tt())) -> mark(tt()) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), V1, V2)) -> mark(U52(isNeList(V1), V2)) , active(U52(X1, X2)) -> U52(active(X1), X2) , active(U52(tt(), V2)) -> mark(U53(isList(V2))) , active(U53(X)) -> U53(active(X)) , active(U53(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V)) -> mark(U62(isQid(V))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X1, X2)) -> U71(active(X1), X2) , active(U71(tt(), V)) -> mark(U72(isNePal(V))) , active(U72(X)) -> U72(active(X)) , active(U72(tt())) -> mark(tt()) , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) , active(isNePal(__(I, __(P, I)))) -> mark(and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isPalListKind(__(V1, V2))) -> mark(and(isPalListKind(V1), isPalListKind(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(isPal(V)) -> mark(U71(isPalListKind(V), V)) , active(isPal(nil())) -> 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(X)) -> mark(U12(X)) , U12(ok(X)) -> ok(U12(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) -> mark(U22(X1, X2)) , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , U23(mark(X)) -> mark(U23(X)) , U23(ok(X)) -> ok(U23(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X)) -> mark(U32(X)) , U32(ok(X)) -> ok(U32(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) -> mark(U42(X1, X2)) , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) , U43(mark(X)) -> mark(U43(X)) , U43(ok(X)) -> ok(U43(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) -> mark(U52(X1, X2)) , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) , U53(mark(X)) -> mark(U53(X)) , U53(ok(X)) -> ok(U53(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X1), X2) -> mark(U71(X1, X2)) , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) , U72(mark(X)) -> mark(U72(X)) , U72(ok(X)) -> ok(U72(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isPalListKind(ok(X)) -> ok(isPalListKind(X)) , isPal(ok(X)) -> ok(isPal(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(X)) -> U12(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(U21(X1, X2, X3)) -> U21(proper(X1), proper(X2), proper(X3)) , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) , proper(isList(X)) -> isList(proper(X)) , proper(U23(X)) -> U23(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X)) -> U32(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) , proper(U43(X)) -> U43(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) , proper(U53(X)) -> U53(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) , proper(U72(X)) -> U72(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isPalListKind(X)) -> isPalListKind(proper(X)) , proper(isPal(X)) -> isPal(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_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 2: active^#(__(X1, X2)) -> c_2(__^#(active(X1), X2)) -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 3: active^#(__(X, nil())) -> c_3(X) -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 -->_1 proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) :135 -->_1 proper^#(isPalListKind(X)) -> c_134(isPalListKind^#(proper(X))) :134 -->_1 proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) :133 -->_1 proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) :132 -->_1 proper^#(U72(X)) -> c_131(U72^#(proper(X))) :131 -->_1 proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) :130 -->_1 proper^#(U62(X)) -> c_129(U62^#(proper(X))) :129 -->_1 proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) :128 -->_1 proper^#(U53(X)) -> c_127(U53^#(proper(X))) :127 -->_1 proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) :126 -->_1 proper^#(U51(X1, X2, X3)) -> c_125(U51^#(proper(X1), proper(X2), proper(X3))) :125 -->_1 proper^#(U43(X)) -> c_124(U43^#(proper(X))) :124 -->_1 proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) :123 -->_1 proper^#(U41(X1, X2, X3)) -> c_122(U41^#(proper(X1), proper(X2), proper(X3))) :122 -->_1 proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) :121 -->_1 proper^#(U32(X)) -> c_120(U32^#(proper(X))) :120 -->_1 proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) :119 -->_1 proper^#(U23(X)) -> c_118(U23^#(proper(X))) :118 -->_1 proper^#(isList(X)) -> c_117(isList^#(proper(X))) :117 -->_1 proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) :116 -->_1 proper^#(U21(X1, X2, X3)) -> c_115(U21^#(proper(X1), proper(X2), proper(X3))) :115 -->_1 proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) :114 -->_1 proper^#(U12(X)) -> c_113(U12^#(proper(X))) :113 -->_1 proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) :111 -->_1 proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) :109 -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 -->_1 active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) :62 -->_1 active^#(isPalListKind(__(V1, V2))) -> c_55(and^#(isPalListKind(V1), isPalListKind(V2))) :55 -->_1 active^#(and(tt(), X)) -> c_54(X) :54 -->_1 active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) :53 -->_1 active^#(isNePal(__(I, __(P, I)))) -> c_52(and^#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) :52 -->_1 active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) :51 -->_1 active^#(U72(X)) -> c_49(U72^#(active(X))) :49 -->_1 active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) :48 -->_1 active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) :47 -->_1 active^#(U62(X)) -> c_45(U62^#(active(X))) :45 -->_1 active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) :44 -->_1 active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) :43 -->_1 active^#(U53(X)) -> c_41(U53^#(active(X))) :41 -->_1 active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) :40 -->_1 active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) :39 -->_1 active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) :38 -->_1 active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) :37 -->_1 active^#(U43(X)) -> c_35(U43^#(active(X))) :35 -->_1 active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) :34 -->_1 active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) :33 -->_1 active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) :32 -->_1 active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) :31 -->_1 active^#(U32(X)) -> c_24(U32^#(active(X))) :24 -->_1 active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) :23 -->_1 active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) :22 -->_1 active^#(U23(X)) -> c_20(U23^#(active(X))) :20 -->_1 active^#(isList(__(V1, V2))) -> c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :18 -->_1 active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) :17 -->_1 active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) :16 -->_1 active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) :15 -->_1 active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) :14 -->_1 active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) :13 -->_1 active^#(isNeList(__(V1, V2))) -> c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :12 -->_1 active^#(isNeList(__(V1, V2))) -> c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :11 -->_1 active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) :10 -->_1 active^#(U12(X)) -> c_8(U12^#(active(X))) :8 -->_1 active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(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_140() :140 -->_1 proper^#(o()) -> c_139() :139 -->_1 proper^#(i()) -> c_138() :138 -->_1 proper^#(e()) -> c_137() :137 -->_1 proper^#(a()) -> c_136() :136 -->_1 proper^#(tt()) -> c_112() :112 -->_1 proper^#(nil()) -> c_110() :110 -->_1 active^#(isPal(nil())) -> c_63() :63 -->_1 active^#(isPalListKind(u())) -> c_61() :61 -->_1 active^#(isPalListKind(o())) -> c_60() :60 -->_1 active^#(isPalListKind(i())) -> c_59() :59 -->_1 active^#(isPalListKind(e())) -> c_58() :58 -->_1 active^#(isPalListKind(a())) -> c_57() :57 -->_1 active^#(isPalListKind(nil())) -> c_56() :56 -->_1 active^#(U72(tt())) -> c_50() :50 -->_1 active^#(U62(tt())) -> c_46() :46 -->_1 active^#(U53(tt())) -> c_42() :42 -->_1 active^#(U43(tt())) -> c_36() :36 -->_1 active^#(isQid(u())) -> c_30() :30 -->_1 active^#(isQid(o())) -> c_29() :29 -->_1 active^#(isQid(i())) -> c_28() :28 -->_1 active^#(isQid(e())) -> c_27() :27 -->_1 active^#(isQid(a())) -> c_26() :26 -->_1 active^#(U32(tt())) -> c_25() :25 -->_1 active^#(U23(tt())) -> c_21() :21 -->_1 active^#(isList(nil())) -> c_19() :19 -->_1 active^#(U12(tt())) -> c_9() :9 -->_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_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 5: active^#(__(nil(), X)) -> c_5(X) -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 -->_1 proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) :135 -->_1 proper^#(isPalListKind(X)) -> c_134(isPalListKind^#(proper(X))) :134 -->_1 proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) :133 -->_1 proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) :132 -->_1 proper^#(U72(X)) -> c_131(U72^#(proper(X))) :131 -->_1 proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) :130 -->_1 proper^#(U62(X)) -> c_129(U62^#(proper(X))) :129 -->_1 proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) :128 -->_1 proper^#(U53(X)) -> c_127(U53^#(proper(X))) :127 -->_1 proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) :126 -->_1 proper^#(U51(X1, X2, X3)) -> c_125(U51^#(proper(X1), proper(X2), proper(X3))) :125 -->_1 proper^#(U43(X)) -> c_124(U43^#(proper(X))) :124 -->_1 proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) :123 -->_1 proper^#(U41(X1, X2, X3)) -> c_122(U41^#(proper(X1), proper(X2), proper(X3))) :122 -->_1 proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) :121 -->_1 proper^#(U32(X)) -> c_120(U32^#(proper(X))) :120 -->_1 proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) :119 -->_1 proper^#(U23(X)) -> c_118(U23^#(proper(X))) :118 -->_1 proper^#(isList(X)) -> c_117(isList^#(proper(X))) :117 -->_1 proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) :116 -->_1 proper^#(U21(X1, X2, X3)) -> c_115(U21^#(proper(X1), proper(X2), proper(X3))) :115 -->_1 proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) :114 -->_1 proper^#(U12(X)) -> c_113(U12^#(proper(X))) :113 -->_1 proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) :111 -->_1 proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) :109 -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 -->_1 active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) :62 -->_1 active^#(isPalListKind(__(V1, V2))) -> c_55(and^#(isPalListKind(V1), isPalListKind(V2))) :55 -->_1 active^#(and(tt(), X)) -> c_54(X) :54 -->_1 active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) :53 -->_1 active^#(isNePal(__(I, __(P, I)))) -> c_52(and^#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) :52 -->_1 active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) :51 -->_1 active^#(U72(X)) -> c_49(U72^#(active(X))) :49 -->_1 active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) :48 -->_1 active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) :47 -->_1 active^#(U62(X)) -> c_45(U62^#(active(X))) :45 -->_1 active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) :44 -->_1 active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) :43 -->_1 active^#(U53(X)) -> c_41(U53^#(active(X))) :41 -->_1 active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) :40 -->_1 active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) :39 -->_1 active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) :38 -->_1 active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) :37 -->_1 active^#(U43(X)) -> c_35(U43^#(active(X))) :35 -->_1 active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) :34 -->_1 active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) :33 -->_1 active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) :32 -->_1 active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) :31 -->_1 active^#(U32(X)) -> c_24(U32^#(active(X))) :24 -->_1 active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) :23 -->_1 active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) :22 -->_1 active^#(U23(X)) -> c_20(U23^#(active(X))) :20 -->_1 active^#(isList(__(V1, V2))) -> c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :18 -->_1 active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) :17 -->_1 active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) :16 -->_1 active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) :15 -->_1 active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) :14 -->_1 active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) :13 -->_1 active^#(isNeList(__(V1, V2))) -> c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :12 -->_1 active^#(isNeList(__(V1, V2))) -> c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :11 -->_1 active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) :10 -->_1 active^#(U12(X)) -> c_8(U12^#(active(X))) :8 -->_1 active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(V))) :7 -->_1 active^#(U11(X1, X2)) -> c_6(U11^#(active(X1), X2)) :6 -->_1 proper^#(u()) -> c_140() :140 -->_1 proper^#(o()) -> c_139() :139 -->_1 proper^#(i()) -> c_138() :138 -->_1 proper^#(e()) -> c_137() :137 -->_1 proper^#(a()) -> c_136() :136 -->_1 proper^#(tt()) -> c_112() :112 -->_1 proper^#(nil()) -> c_110() :110 -->_1 active^#(isPal(nil())) -> c_63() :63 -->_1 active^#(isPalListKind(u())) -> c_61() :61 -->_1 active^#(isPalListKind(o())) -> c_60() :60 -->_1 active^#(isPalListKind(i())) -> c_59() :59 -->_1 active^#(isPalListKind(e())) -> c_58() :58 -->_1 active^#(isPalListKind(a())) -> c_57() :57 -->_1 active^#(isPalListKind(nil())) -> c_56() :56 -->_1 active^#(U72(tt())) -> c_50() :50 -->_1 active^#(U62(tt())) -> c_46() :46 -->_1 active^#(U53(tt())) -> c_42() :42 -->_1 active^#(U43(tt())) -> c_36() :36 -->_1 active^#(isQid(u())) -> c_30() :30 -->_1 active^#(isQid(o())) -> c_29() :29 -->_1 active^#(isQid(i())) -> c_28() :28 -->_1 active^#(isQid(e())) -> c_27() :27 -->_1 active^#(isQid(a())) -> c_26() :26 -->_1 active^#(U32(tt())) -> c_25() :25 -->_1 active^#(U23(tt())) -> c_21() :21 -->_1 active^#(isList(nil())) -> c_19() :19 -->_1 active^#(U12(tt())) -> c_9() :9 -->_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_68(U11^#(X1, X2)) :68 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 7: active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(V))) -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 8: active^#(U12(X)) -> c_8(U12^#(active(X))) -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 9: active^#(U12(tt())) -> c_9() 10: active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 11: active^#(isNeList(__(V1, V2))) -> c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 12: active^#(isNeList(__(V1, V2))) -> c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 13: active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 14: active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 15: active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 16: active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 17: active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 18: active^#(isList(__(V1, V2))) -> c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 19: active^#(isList(nil())) -> c_19() 20: active^#(U23(X)) -> c_20(U23^#(active(X))) -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 21: active^#(U23(tt())) -> c_21() 22: active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 23: active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 24: active^#(U32(X)) -> c_24(U32^#(active(X))) -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 25: active^#(U32(tt())) -> c_25() 26: active^#(isQid(a())) -> c_26() 27: active^#(isQid(e())) -> c_27() 28: active^#(isQid(i())) -> c_28() 29: active^#(isQid(o())) -> c_29() 30: active^#(isQid(u())) -> c_30() 31: active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 32: active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 33: active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 34: active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 35: active^#(U43(X)) -> c_35(U43^#(active(X))) -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 36: active^#(U43(tt())) -> c_36() 37: active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 38: active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 39: active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 40: active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 41: active^#(U53(X)) -> c_41(U53^#(active(X))) -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 42: active^#(U53(tt())) -> c_42() 43: active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 44: active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 45: active^#(U62(X)) -> c_45(U62^#(active(X))) -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 46: active^#(U62(tt())) -> c_46() 47: active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 48: active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 49: active^#(U72(X)) -> c_49(U72^#(active(X))) -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 50: active^#(U72(tt())) -> c_50() 51: active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 52: active^#(isNePal(__(I, __(P, I)))) -> c_52(and^#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 53: active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 54: active^#(and(tt(), X)) -> c_54(X) -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 -->_1 proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) :135 -->_1 proper^#(isPalListKind(X)) -> c_134(isPalListKind^#(proper(X))) :134 -->_1 proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) :133 -->_1 proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) :132 -->_1 proper^#(U72(X)) -> c_131(U72^#(proper(X))) :131 -->_1 proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) :130 -->_1 proper^#(U62(X)) -> c_129(U62^#(proper(X))) :129 -->_1 proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) :128 -->_1 proper^#(U53(X)) -> c_127(U53^#(proper(X))) :127 -->_1 proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) :126 -->_1 proper^#(U51(X1, X2, X3)) -> c_125(U51^#(proper(X1), proper(X2), proper(X3))) :125 -->_1 proper^#(U43(X)) -> c_124(U43^#(proper(X))) :124 -->_1 proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) :123 -->_1 proper^#(U41(X1, X2, X3)) -> c_122(U41^#(proper(X1), proper(X2), proper(X3))) :122 -->_1 proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) :121 -->_1 proper^#(U32(X)) -> c_120(U32^#(proper(X))) :120 -->_1 proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) :119 -->_1 proper^#(U23(X)) -> c_118(U23^#(proper(X))) :118 -->_1 proper^#(isList(X)) -> c_117(isList^#(proper(X))) :117 -->_1 proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) :116 -->_1 proper^#(U21(X1, X2, X3)) -> c_115(U21^#(proper(X1), proper(X2), proper(X3))) :115 -->_1 proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) :114 -->_1 proper^#(U12(X)) -> c_113(U12^#(proper(X))) :113 -->_1 proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) :111 -->_1 proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) :109 -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 -->_1 active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) :62 -->_1 active^#(isPalListKind(__(V1, V2))) -> c_55(and^#(isPalListKind(V1), isPalListKind(V2))) :55 -->_1 proper^#(u()) -> c_140() :140 -->_1 proper^#(o()) -> c_139() :139 -->_1 proper^#(i()) -> c_138() :138 -->_1 proper^#(e()) -> c_137() :137 -->_1 proper^#(a()) -> c_136() :136 -->_1 proper^#(tt()) -> c_112() :112 -->_1 proper^#(nil()) -> c_110() :110 -->_1 active^#(isPal(nil())) -> c_63() :63 -->_1 active^#(isPalListKind(u())) -> c_61() :61 -->_1 active^#(isPalListKind(o())) -> c_60() :60 -->_1 active^#(isPalListKind(i())) -> c_59() :59 -->_1 active^#(isPalListKind(e())) -> c_58() :58 -->_1 active^#(isPalListKind(a())) -> c_57() :57 -->_1 active^#(isPalListKind(nil())) -> c_56() :56 -->_1 active^#(and(tt(), X)) -> c_54(X) :54 -->_1 active^#(and(X1, X2)) -> c_53(and^#(active(X1), X2)) :53 -->_1 active^#(isNePal(__(I, __(P, I)))) -> c_52(and^#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) :52 -->_1 active^#(isNePal(V)) -> c_51(U61^#(isPalListKind(V), V)) :51 -->_1 active^#(U72(tt())) -> c_50() :50 -->_1 active^#(U72(X)) -> c_49(U72^#(active(X))) :49 -->_1 active^#(U71(tt(), V)) -> c_48(U72^#(isNePal(V))) :48 -->_1 active^#(U71(X1, X2)) -> c_47(U71^#(active(X1), X2)) :47 -->_1 active^#(U62(tt())) -> c_46() :46 -->_1 active^#(U62(X)) -> c_45(U62^#(active(X))) :45 -->_1 active^#(U61(tt(), V)) -> c_44(U62^#(isQid(V))) :44 -->_1 active^#(U61(X1, X2)) -> c_43(U61^#(active(X1), X2)) :43 -->_1 active^#(U53(tt())) -> c_42() :42 -->_1 active^#(U53(X)) -> c_41(U53^#(active(X))) :41 -->_1 active^#(U52(tt(), V2)) -> c_40(U53^#(isList(V2))) :40 -->_1 active^#(U52(X1, X2)) -> c_39(U52^#(active(X1), X2)) :39 -->_1 active^#(U51(tt(), V1, V2)) -> c_38(U52^#(isNeList(V1), V2)) :38 -->_1 active^#(U51(X1, X2, X3)) -> c_37(U51^#(active(X1), X2, X3)) :37 -->_1 active^#(U43(tt())) -> c_36() :36 -->_1 active^#(U43(X)) -> c_35(U43^#(active(X))) :35 -->_1 active^#(U42(tt(), V2)) -> c_34(U43^#(isNeList(V2))) :34 -->_1 active^#(U42(X1, X2)) -> c_33(U42^#(active(X1), X2)) :33 -->_1 active^#(U41(tt(), V1, V2)) -> c_32(U42^#(isList(V1), V2)) :32 -->_1 active^#(U41(X1, X2, X3)) -> c_31(U41^#(active(X1), X2, X3)) :31 -->_1 active^#(isQid(u())) -> c_30() :30 -->_1 active^#(isQid(o())) -> c_29() :29 -->_1 active^#(isQid(i())) -> c_28() :28 -->_1 active^#(isQid(e())) -> c_27() :27 -->_1 active^#(isQid(a())) -> c_26() :26 -->_1 active^#(U32(tt())) -> c_25() :25 -->_1 active^#(U32(X)) -> c_24(U32^#(active(X))) :24 -->_1 active^#(U31(tt(), V)) -> c_23(U32^#(isQid(V))) :23 -->_1 active^#(U31(X1, X2)) -> c_22(U31^#(active(X1), X2)) :22 -->_1 active^#(U23(tt())) -> c_21() :21 -->_1 active^#(U23(X)) -> c_20(U23^#(active(X))) :20 -->_1 active^#(isList(nil())) -> c_19() :19 -->_1 active^#(isList(__(V1, V2))) -> c_18(U21^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :18 -->_1 active^#(isList(V)) -> c_17(U11^#(isPalListKind(V), V)) :17 -->_1 active^#(U22(tt(), V2)) -> c_16(U23^#(isList(V2))) :16 -->_1 active^#(U22(X1, X2)) -> c_15(U22^#(active(X1), X2)) :15 -->_1 active^#(U21(tt(), V1, V2)) -> c_14(U22^#(isList(V1), V2)) :14 -->_1 active^#(U21(X1, X2, X3)) -> c_13(U21^#(active(X1), X2, X3)) :13 -->_1 active^#(isNeList(__(V1, V2))) -> c_12(U51^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :12 -->_1 active^#(isNeList(__(V1, V2))) -> c_11(U41^#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) :11 -->_1 active^#(isNeList(V)) -> c_10(U31^#(isPalListKind(V), V)) :10 -->_1 active^#(U12(tt())) -> c_9() :9 -->_1 active^#(U12(X)) -> c_8(U12^#(active(X))) :8 -->_1 active^#(U11(tt(), V)) -> c_7(U12^#(isNeList(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 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 55: active^#(isPalListKind(__(V1, V2))) -> c_55(and^#(isPalListKind(V1), isPalListKind(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 56: active^#(isPalListKind(nil())) -> c_56() 57: active^#(isPalListKind(a())) -> c_57() 58: active^#(isPalListKind(e())) -> c_58() 59: active^#(isPalListKind(i())) -> c_59() 60: active^#(isPalListKind(o())) -> c_60() 61: active^#(isPalListKind(u())) -> c_61() 62: active^#(isPal(V)) -> c_62(U71^#(isPalListKind(V), V)) -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 63: active^#(isPal(nil())) -> c_63() 64: __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 65: __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 66: __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 67: U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 68: U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 69: U12^#(mark(X)) -> c_69(U12^#(X)) -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 70: U12^#(ok(X)) -> c_70(U12^#(X)) -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 71: U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 72: U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 73: U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 74: U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 75: U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 76: U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 77: U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 78: U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 79: U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 80: U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 81: U23^#(mark(X)) -> c_77(U23^#(X)) -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 82: U23^#(ok(X)) -> c_78(U23^#(X)) -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 83: U32^#(mark(X)) -> c_81(U32^#(X)) -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 84: U32^#(ok(X)) -> c_82(U32^#(X)) -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 85: U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 86: U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 87: U43^#(mark(X)) -> c_88(U43^#(X)) -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 88: U43^#(ok(X)) -> c_89(U43^#(X)) -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 89: U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 90: U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 91: U53^#(mark(X)) -> c_94(U53^#(X)) -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 92: U53^#(ok(X)) -> c_95(U53^#(X)) -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 93: U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 94: U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 95: U62^#(mark(X)) -> c_98(U62^#(X)) -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 96: U62^#(ok(X)) -> c_99(U62^#(X)) -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 97: U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 98: U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 99: U72^#(mark(X)) -> c_102(U72^#(X)) -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 100: U72^#(ok(X)) -> c_103(U72^#(X)) -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 101: and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 102: and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 103: isNeList^#(ok(X)) -> c_71(isNeList^#(X)) -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 104: isList^#(ok(X)) -> c_76(isList^#(X)) -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 105: isQid^#(ok(X)) -> c_83(isQid^#(X)) -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 106: isNePal^#(ok(X)) -> c_104(isNePal^#(X)) -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 107: isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 108: isPal^#(ok(X)) -> c_108(isPal^#(X)) -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 109: proper^#(__(X1, X2)) -> c_109(__^#(proper(X1), proper(X2))) -->_1 __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) :66 -->_1 __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) :65 -->_1 __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) :64 110: proper^#(nil()) -> c_110() 111: proper^#(U11(X1, X2)) -> c_111(U11^#(proper(X1), proper(X2))) -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 112: proper^#(tt()) -> c_112() 113: proper^#(U12(X)) -> c_113(U12^#(proper(X))) -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 114: proper^#(isNeList(X)) -> c_114(isNeList^#(proper(X))) -->_1 isNeList^#(ok(X)) -> c_71(isNeList^#(X)) :103 115: proper^#(U21(X1, X2, X3)) -> c_115(U21^#(proper(X1), proper(X2), proper(X3))) -->_1 U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) :78 -->_1 U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) :77 116: proper^#(U22(X1, X2)) -> c_116(U22^#(proper(X1), proper(X2))) -->_1 U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) :80 -->_1 U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) :79 117: proper^#(isList(X)) -> c_117(isList^#(proper(X))) -->_1 isList^#(ok(X)) -> c_76(isList^#(X)) :104 118: proper^#(U23(X)) -> c_118(U23^#(proper(X))) -->_1 U23^#(ok(X)) -> c_78(U23^#(X)) :82 -->_1 U23^#(mark(X)) -> c_77(U23^#(X)) :81 119: proper^#(U31(X1, X2)) -> c_119(U31^#(proper(X1), proper(X2))) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :72 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :71 120: proper^#(U32(X)) -> c_120(U32^#(proper(X))) -->_1 U32^#(ok(X)) -> c_82(U32^#(X)) :84 -->_1 U32^#(mark(X)) -> c_81(U32^#(X)) :83 121: proper^#(isQid(X)) -> c_121(isQid^#(proper(X))) -->_1 isQid^#(ok(X)) -> c_83(isQid^#(X)) :105 122: proper^#(U41(X1, X2, X3)) -> c_122(U41^#(proper(X1), proper(X2), proper(X3))) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) :74 -->_1 U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) :73 123: proper^#(U42(X1, X2)) -> c_123(U42^#(proper(X1), proper(X2))) -->_1 U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) :86 -->_1 U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) :85 124: proper^#(U43(X)) -> c_124(U43^#(proper(X))) -->_1 U43^#(ok(X)) -> c_89(U43^#(X)) :88 -->_1 U43^#(mark(X)) -> c_88(U43^#(X)) :87 125: proper^#(U51(X1, X2, X3)) -> c_125(U51^#(proper(X1), proper(X2), proper(X3))) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) :76 -->_1 U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) :75 126: proper^#(U52(X1, X2)) -> c_126(U52^#(proper(X1), proper(X2))) -->_1 U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) :90 -->_1 U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) :89 127: proper^#(U53(X)) -> c_127(U53^#(proper(X))) -->_1 U53^#(ok(X)) -> c_95(U53^#(X)) :92 -->_1 U53^#(mark(X)) -> c_94(U53^#(X)) :91 128: proper^#(U61(X1, X2)) -> c_128(U61^#(proper(X1), proper(X2))) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :94 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :93 129: proper^#(U62(X)) -> c_129(U62^#(proper(X))) -->_1 U62^#(ok(X)) -> c_99(U62^#(X)) :96 -->_1 U62^#(mark(X)) -> c_98(U62^#(X)) :95 130: proper^#(U71(X1, X2)) -> c_130(U71^#(proper(X1), proper(X2))) -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 131: proper^#(U72(X)) -> c_131(U72^#(proper(X))) -->_1 U72^#(ok(X)) -> c_103(U72^#(X)) :100 -->_1 U72^#(mark(X)) -> c_102(U72^#(X)) :99 132: proper^#(isNePal(X)) -> c_132(isNePal^#(proper(X))) -->_1 isNePal^#(ok(X)) -> c_104(isNePal^#(X)) :106 133: proper^#(and(X1, X2)) -> c_133(and^#(proper(X1), proper(X2))) -->_1 and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) :102 -->_1 and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) :101 134: proper^#(isPalListKind(X)) -> c_134(isPalListKind^#(proper(X))) -->_1 isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) :107 135: proper^#(isPal(X)) -> c_135(isPal^#(proper(X))) -->_1 isPal^#(ok(X)) -> c_108(isPal^#(X)) :108 136: proper^#(a()) -> c_136() 137: proper^#(e()) -> c_137() 138: proper^#(i()) -> c_138() 139: proper^#(o()) -> c_139() 140: proper^#(u()) -> c_140() 141: top^#(mark(X)) -> c_141(top^#(proper(X))) -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 142: top^#(ok(X)) -> c_142(top^#(active(X))) -->_1 top^#(ok(X)) -> c_142(top^#(active(X))) :142 -->_1 top^#(mark(X)) -> c_141(top^#(proper(X))) :141 Only the nodes {64,66,65,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,110,112,136,137,138,139,140,141,142} are reachable from nodes {64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,110,112,136,137,138,139,140,141,142} 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_64(__^#(X1, X2)) , __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) , __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) , U12^#(mark(X)) -> c_69(U12^#(X)) , U12^#(ok(X)) -> c_70(U12^#(X)) , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) , U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) , U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) , U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) , U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) , U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) , U23^#(mark(X)) -> c_77(U23^#(X)) , U23^#(ok(X)) -> c_78(U23^#(X)) , U32^#(mark(X)) -> c_81(U32^#(X)) , U32^#(ok(X)) -> c_82(U32^#(X)) , U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) , U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) , U43^#(mark(X)) -> c_88(U43^#(X)) , U43^#(ok(X)) -> c_89(U43^#(X)) , U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) , U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) , U53^#(mark(X)) -> c_94(U53^#(X)) , U53^#(ok(X)) -> c_95(U53^#(X)) , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , U62^#(mark(X)) -> c_98(U62^#(X)) , U62^#(ok(X)) -> c_99(U62^#(X)) , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) , U72^#(mark(X)) -> c_102(U72^#(X)) , U72^#(ok(X)) -> c_103(U72^#(X)) , and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) , isNeList^#(ok(X)) -> c_71(isNeList^#(X)) , isList^#(ok(X)) -> c_76(isList^#(X)) , isQid^#(ok(X)) -> c_83(isQid^#(X)) , isNePal^#(ok(X)) -> c_104(isNePal^#(X)) , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , isPal^#(ok(X)) -> c_108(isPal^#(X)) , proper^#(nil()) -> c_110() , proper^#(tt()) -> c_112() , proper^#(a()) -> c_136() , proper^#(e()) -> c_137() , proper^#(i()) -> c_138() , proper^#(o()) -> c_139() , proper^#(u()) -> c_140() , top^#(mark(X)) -> c_141(top^#(proper(X))) , top^#(ok(X)) -> c_142(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(isNeList(V))) , active(U12(X)) -> U12(active(X)) , active(U12(tt())) -> mark(tt()) , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) , active(isNeList(__(V1, V2))) -> mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(isNeList(__(V1, V2))) -> mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) , active(U21(tt(), V1, V2)) -> mark(U22(isList(V1), V2)) , active(U22(X1, X2)) -> U22(active(X1), X2) , active(U22(tt(), V2)) -> mark(U23(isList(V2))) , active(isList(V)) -> mark(U11(isPalListKind(V), V)) , active(isList(__(V1, V2))) -> mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(isList(nil())) -> mark(tt()) , active(U23(X)) -> U23(active(X)) , active(U23(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isQid(V))) , active(U32(X)) -> U32(active(X)) , active(U32(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(isList(V1), V2)) , active(U42(X1, X2)) -> U42(active(X1), X2) , active(U42(tt(), V2)) -> mark(U43(isNeList(V2))) , active(U43(X)) -> U43(active(X)) , active(U43(tt())) -> mark(tt()) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), V1, V2)) -> mark(U52(isNeList(V1), V2)) , active(U52(X1, X2)) -> U52(active(X1), X2) , active(U52(tt(), V2)) -> mark(U53(isList(V2))) , active(U53(X)) -> U53(active(X)) , active(U53(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V)) -> mark(U62(isQid(V))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X1, X2)) -> U71(active(X1), X2) , active(U71(tt(), V)) -> mark(U72(isNePal(V))) , active(U72(X)) -> U72(active(X)) , active(U72(tt())) -> mark(tt()) , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) , active(isNePal(__(I, __(P, I)))) -> mark(and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isPalListKind(__(V1, V2))) -> mark(and(isPalListKind(V1), isPalListKind(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(isPal(V)) -> mark(U71(isPalListKind(V), V)) , active(isPal(nil())) -> 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(X)) -> mark(U12(X)) , U12(ok(X)) -> ok(U12(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) -> mark(U22(X1, X2)) , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , U23(mark(X)) -> mark(U23(X)) , U23(ok(X)) -> ok(U23(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X)) -> mark(U32(X)) , U32(ok(X)) -> ok(U32(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) -> mark(U42(X1, X2)) , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) , U43(mark(X)) -> mark(U43(X)) , U43(ok(X)) -> ok(U43(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) -> mark(U52(X1, X2)) , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) , U53(mark(X)) -> mark(U53(X)) , U53(ok(X)) -> ok(U53(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X1), X2) -> mark(U71(X1, X2)) , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) , U72(mark(X)) -> mark(U72(X)) , U72(ok(X)) -> ok(U72(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isPalListKind(ok(X)) -> ok(isPalListKind(X)) , isPal(ok(X)) -> ok(isPal(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(X)) -> U12(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(U21(X1, X2, X3)) -> U21(proper(X1), proper(X2), proper(X3)) , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) , proper(isList(X)) -> isList(proper(X)) , proper(U23(X)) -> U23(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X)) -> U32(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) , proper(U43(X)) -> U43(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) , proper(U53(X)) -> U53(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) , proper(U72(X)) -> U72(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isPalListKind(X)) -> isPalListKind(proper(X)) , proper(isPal(X)) -> isPal(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 {46,47,48,49,50,51,52} by applications of Pre({46,47,48,49,50,51,52}) = {}. Here rules are labeled as follows: DPs: { 1: __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) , 2: __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) , 3: __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) , 4: U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) , 5: U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) , 6: U12^#(mark(X)) -> c_69(U12^#(X)) , 7: U12^#(ok(X)) -> c_70(U12^#(X)) , 8: U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , 9: U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , 10: U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) , 11: U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) , 12: U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) , 13: U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) , 14: U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) , 15: U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) , 16: U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) , 17: U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) , 18: U23^#(mark(X)) -> c_77(U23^#(X)) , 19: U23^#(ok(X)) -> c_78(U23^#(X)) , 20: U32^#(mark(X)) -> c_81(U32^#(X)) , 21: U32^#(ok(X)) -> c_82(U32^#(X)) , 22: U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) , 23: U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) , 24: U43^#(mark(X)) -> c_88(U43^#(X)) , 25: U43^#(ok(X)) -> c_89(U43^#(X)) , 26: U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) , 27: U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) , 28: U53^#(mark(X)) -> c_94(U53^#(X)) , 29: U53^#(ok(X)) -> c_95(U53^#(X)) , 30: U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , 31: U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , 32: U62^#(mark(X)) -> c_98(U62^#(X)) , 33: U62^#(ok(X)) -> c_99(U62^#(X)) , 34: U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) , 35: U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) , 36: U72^#(mark(X)) -> c_102(U72^#(X)) , 37: U72^#(ok(X)) -> c_103(U72^#(X)) , 38: and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) , 39: and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) , 40: isNeList^#(ok(X)) -> c_71(isNeList^#(X)) , 41: isList^#(ok(X)) -> c_76(isList^#(X)) , 42: isQid^#(ok(X)) -> c_83(isQid^#(X)) , 43: isNePal^#(ok(X)) -> c_104(isNePal^#(X)) , 44: isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , 45: isPal^#(ok(X)) -> c_108(isPal^#(X)) , 46: proper^#(nil()) -> c_110() , 47: proper^#(tt()) -> c_112() , 48: proper^#(a()) -> c_136() , 49: proper^#(e()) -> c_137() , 50: proper^#(i()) -> c_138() , 51: proper^#(o()) -> c_139() , 52: proper^#(u()) -> c_140() , 53: top^#(mark(X)) -> c_141(top^#(proper(X))) , 54: top^#(ok(X)) -> c_142(top^#(active(X))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X1, mark(X2)) -> c_64(__^#(X1, X2)) , __^#(mark(X1), X2) -> c_65(__^#(X1, X2)) , __^#(ok(X1), ok(X2)) -> c_66(__^#(X1, X2)) , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) , U12^#(mark(X)) -> c_69(U12^#(X)) , U12^#(ok(X)) -> c_70(U12^#(X)) , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_84(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_85(U41^#(X1, X2, X3)) , U51^#(mark(X1), X2, X3) -> c_90(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_91(U51^#(X1, X2, X3)) , U21^#(mark(X1), X2, X3) -> c_72(U21^#(X1, X2, X3)) , U21^#(ok(X1), ok(X2), ok(X3)) -> c_73(U21^#(X1, X2, X3)) , U22^#(mark(X1), X2) -> c_74(U22^#(X1, X2)) , U22^#(ok(X1), ok(X2)) -> c_75(U22^#(X1, X2)) , U23^#(mark(X)) -> c_77(U23^#(X)) , U23^#(ok(X)) -> c_78(U23^#(X)) , U32^#(mark(X)) -> c_81(U32^#(X)) , U32^#(ok(X)) -> c_82(U32^#(X)) , U42^#(mark(X1), X2) -> c_86(U42^#(X1, X2)) , U42^#(ok(X1), ok(X2)) -> c_87(U42^#(X1, X2)) , U43^#(mark(X)) -> c_88(U43^#(X)) , U43^#(ok(X)) -> c_89(U43^#(X)) , U52^#(mark(X1), X2) -> c_92(U52^#(X1, X2)) , U52^#(ok(X1), ok(X2)) -> c_93(U52^#(X1, X2)) , U53^#(mark(X)) -> c_94(U53^#(X)) , U53^#(ok(X)) -> c_95(U53^#(X)) , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , U62^#(mark(X)) -> c_98(U62^#(X)) , U62^#(ok(X)) -> c_99(U62^#(X)) , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) , U72^#(mark(X)) -> c_102(U72^#(X)) , U72^#(ok(X)) -> c_103(U72^#(X)) , and^#(mark(X1), X2) -> c_105(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_106(and^#(X1, X2)) , isNeList^#(ok(X)) -> c_71(isNeList^#(X)) , isList^#(ok(X)) -> c_76(isList^#(X)) , isQid^#(ok(X)) -> c_83(isQid^#(X)) , isNePal^#(ok(X)) -> c_104(isNePal^#(X)) , isPalListKind^#(ok(X)) -> c_107(isPalListKind^#(X)) , isPal^#(ok(X)) -> c_108(isPal^#(X)) , top^#(mark(X)) -> c_141(top^#(proper(X))) , top^#(ok(X)) -> c_142(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(isNeList(V))) , active(U12(X)) -> U12(active(X)) , active(U12(tt())) -> mark(tt()) , active(isNeList(V)) -> mark(U31(isPalListKind(V), V)) , active(isNeList(__(V1, V2))) -> mark(U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(isNeList(__(V1, V2))) -> mark(U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(U21(X1, X2, X3)) -> U21(active(X1), X2, X3) , active(U21(tt(), V1, V2)) -> mark(U22(isList(V1), V2)) , active(U22(X1, X2)) -> U22(active(X1), X2) , active(U22(tt(), V2)) -> mark(U23(isList(V2))) , active(isList(V)) -> mark(U11(isPalListKind(V), V)) , active(isList(__(V1, V2))) -> mark(U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)) , active(isList(nil())) -> mark(tt()) , active(U23(X)) -> U23(active(X)) , active(U23(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isQid(V))) , active(U32(X)) -> U32(active(X)) , active(U32(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(isList(V1), V2)) , active(U42(X1, X2)) -> U42(active(X1), X2) , active(U42(tt(), V2)) -> mark(U43(isNeList(V2))) , active(U43(X)) -> U43(active(X)) , active(U43(tt())) -> mark(tt()) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), V1, V2)) -> mark(U52(isNeList(V1), V2)) , active(U52(X1, X2)) -> U52(active(X1), X2) , active(U52(tt(), V2)) -> mark(U53(isList(V2))) , active(U53(X)) -> U53(active(X)) , active(U53(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V)) -> mark(U62(isQid(V))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X1, X2)) -> U71(active(X1), X2) , active(U71(tt(), V)) -> mark(U72(isNePal(V))) , active(U72(X)) -> U72(active(X)) , active(U72(tt())) -> mark(tt()) , active(isNePal(V)) -> mark(U61(isPalListKind(V), V)) , active(isNePal(__(I, __(P, I)))) -> mark(and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isPalListKind(__(V1, V2))) -> mark(and(isPalListKind(V1), isPalListKind(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(isPal(V)) -> mark(U71(isPalListKind(V), V)) , active(isPal(nil())) -> 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(X)) -> mark(U12(X)) , U12(ok(X)) -> ok(U12(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) -> mark(U22(X1, X2)) , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) , isList(ok(X)) -> ok(isList(X)) , U23(mark(X)) -> mark(U23(X)) , U23(ok(X)) -> ok(U23(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X)) -> mark(U32(X)) , U32(ok(X)) -> ok(U32(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) -> mark(U42(X1, X2)) , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) , U43(mark(X)) -> mark(U43(X)) , U43(ok(X)) -> ok(U43(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) -> mark(U52(X1, X2)) , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) , U53(mark(X)) -> mark(U53(X)) , U53(ok(X)) -> ok(U53(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X1), X2) -> mark(U71(X1, X2)) , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) , U72(mark(X)) -> mark(U72(X)) , U72(ok(X)) -> ok(U72(X)) , isNePal(ok(X)) -> ok(isNePal(X)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isPalListKind(ok(X)) -> ok(isPalListKind(X)) , isPal(ok(X)) -> ok(isPal(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(X)) -> U12(proper(X)) , proper(isNeList(X)) -> isNeList(proper(X)) , proper(U21(X1, X2, X3)) -> U21(proper(X1), proper(X2), proper(X3)) , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) , proper(isList(X)) -> isList(proper(X)) , proper(U23(X)) -> U23(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X)) -> U32(proper(X)) , proper(isQid(X)) -> isQid(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) , proper(U43(X)) -> U43(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) , proper(U53(X)) -> U53(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) , proper(U72(X)) -> U72(proper(X)) , proper(isNePal(X)) -> isNePal(proper(X)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isPalListKind(X)) -> isPalListKind(proper(X)) , proper(isPal(X)) -> isPal(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_110() , proper^#(tt()) -> c_112() , proper^#(a()) -> c_136() , proper^#(e()) -> c_137() , proper^#(i()) -> c_138() , proper^#(o()) -> c_139() , proper^#(u()) -> c_140() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..