0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 319 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 1198 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 49 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 5 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 PiDP
↳38 PiDPToQDPProof (⇒, 0 ms)
↳39 QDP
↳40 QDPOrderProof (⇔, 294 ms)
↳41 QDP
↳42 DependencyGraphProof (⇔, 0 ms)
↳43 TRUE
↳44 PiDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 PiDP
↳47 PiDPToQDPProof (⇒, 0 ms)
↳48 QDP
↳49 QDPSizeChangeProof (⇔, 0 ms)
↳50 YES
↳51 PiDP
↳52 UsableRulesProof (⇔, 0 ms)
↳53 PiDP
↳54 PiDPToQDPProof (⇒, 0 ms)
↳55 QDP
↳56 QDPOrderProof (⇔, 310 ms)
↳57 QDP
↳58 DependencyGraphProof (⇔, 0 ms)
↳59 TRUE
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
QSA_IN_GA(cons(T14, []), T9) → U1_GA(T14, T9, pB_in_aaga(X12, X13, T14, T9))
QSA_IN_GA(cons(T14, []), T9) → PB_IN_AAGA(X12, X13, T14, T9)
PB_IN_AAGA(T19, X13, T14, T9) → U11_AAGA(T19, X13, T14, T9, qsE_in_a(T19))
PB_IN_AAGA(T19, X13, T14, T9) → QSE_IN_A(T19)
U11_AAGA(T19, X13, T14, T9, qsE_out_a(T19)) → U12_AAGA(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
U11_AAGA(T19, X13, T14, T9, qsE_out_a(T19)) → PO_IN_AGGA(X13, T19, T14, T9)
PO_IN_AGGA(T24, T19, T14, T9) → U13_AGGA(T24, T19, T14, T9, qsE_in_a(T24))
PO_IN_AGGA(T24, T19, T14, T9) → QSE_IN_A(T24)
U13_AGGA(T24, T19, T14, T9, qsE_out_a(T24)) → U14_AGGA(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
U13_AGGA(T24, T19, T14, T9, qsE_out_a(T24)) → APPENDF_IN_GGGA(T19, T14, T24, T9)
APPENDF_IN_GGGA(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_GGGA(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
APPENDF_IN_GGGA(cons(T49, T50), T51, T52, cons(T49, T54)) → APPENDF_IN_GGGA(T50, T51, T52, T54)
QSA_IN_GA(cons(T73, cons(T71, T72)), T9) → U2_GA(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
QSA_IN_GA(cons(T73, cons(T71, T72)), T9) → PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9)
PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9) → U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9) → LESSG_IN_GG(T71, T73)
LESSG_IN_GG(s(T87), s(T88)) → U5_GG(T87, T88, lessG_in_gg(T87, T88))
LESSG_IN_GG(s(T87), s(T88)) → LESSG_IN_GG(T87, T88)
U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → PP_IN_GGAAGAAA(T72, T73, X84, X85, T71, X12, X13, T9)
PP_IN_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9) → U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
PP_IN_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9) → SPLITH_IN_GGAA(T72, T73, T93, T94)
SPLITH_IN_GGAA(cons(T114, T115), T116, cons(T114, X145), X146) → U6_GGAA(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
SPLITH_IN_GGAA(cons(T114, T115), T116, cons(T114, X145), X146) → PI_IN_GGGAA(T114, T116, T115, X145, X146)
PI_IN_GGGAA(T114, T116, T115, X145, X146) → U21_GGGAA(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
PI_IN_GGGAA(T114, T116, T115, X145, X146) → LESSG_IN_GG(T114, T116)
U21_GGGAA(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_GGGAA(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
U21_GGGAA(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → SPLITH_IN_GGAA(T115, T116, X145, X146)
SPLITH_IN_GGAA(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_GGAA(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
SPLITH_IN_GGAA(cons(T129, T130), T131, X172, cons(T129, X173)) → PJ_IN_GGGAA(T129, T131, T130, X172, X173)
PJ_IN_GGGAA(T129, T131, T130, X172, X173) → U23_GGGAA(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
PJ_IN_GGGAA(T129, T131, T130, X172, X173) → GEQK_IN_GG(T129, T131)
GEQK_IN_GG(s(T150), s(T151)) → U8_GG(T150, T151, geqK_in_gg(T150, T151))
GEQK_IN_GG(s(T150), s(T151)) → GEQK_IN_GG(T150, T151)
U23_GGGAA(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_GGGAA(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U23_GGGAA(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → SPLITH_IN_GGAA(T130, T131, X172, X173)
U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → PQ_IN_GGAGAGA(T71, T93, X12, T94, X13, T73, T9)
PQ_IN_GGAGAGA(T71, T93, T156, T94, X13, T73, T9) → U19_GGAGAGA(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
PQ_IN_GGAGAGA(T71, T93, T156, T94, X13, T73, T9) → QSA_IN_GA(cons(T71, T93), T156)
QSA_IN_GA(cons(T214, cons(T212, T213)), T9) → U3_GA(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
QSA_IN_GA(cons(T214, cons(T212, T213)), T9) → PD_IN_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9)
PD_IN_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9) → U33_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
PD_IN_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9) → GEQK_IN_GG(T212, T214)
U33_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
U33_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → PU_IN_GGAAAGAA(T213, T214, X267, X268, X12, T212, X13, T9)
PU_IN_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9) → U35_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
PU_IN_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9) → SPLITH_IN_GGAA(T213, T214, T221, T222)
U35_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
U35_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → PV_IN_GAGGAGA(T221, X12, T212, T222, X13, T214, T9)
PV_IN_GAGGAGA(T221, T225, T212, T222, X13, T214, T9) → U37_GAGGAGA(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
PV_IN_GAGGAGA(T221, T225, T212, T222, X13, T214, T9) → QSL_IN_GA(T221, T225)
QSL_IN_GA(cons(T162, T163), X217) → U9_GA(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
QSL_IN_GA(cons(T162, T163), X217) → PM_IN_GGAAAAA(T163, T162, X213, X214, X215, X216, X217)
PM_IN_GGAAAAA(T163, T162, T166, T167, X215, X216, X217) → U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
PM_IN_GGAAAAA(T163, T162, T166, T167, X215, X216, X217) → SPLITH_IN_GGAA(T163, T162, T166, T167)
U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → PS_IN_GAGAGA(T166, X215, T167, X216, T162, X217)
PS_IN_GAGAGA(T166, T170, T167, X216, T162, X217) → U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
PS_IN_GAGAGA(T166, T170, T167, X216, T162, X217) → QSL_IN_GA(T166, T170)
U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_GAGAGA(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → PT_IN_GAGGA(T167, X216, T170, T162, X217)
PT_IN_GAGGA(T167, T171, T170, T162, X217) → U31_GAGGA(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
PT_IN_GAGGA(T167, T171, T170, T162, X217) → QSL_IN_GA(T167, T171)
U31_GAGGA(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_GAGGA(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
U31_GAGGA(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → APPENDN_IN_GGGA(T170, T162, T171, X217)
APPENDN_IN_GGGA(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_GGGA(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
APPENDN_IN_GGGA(cons(T194, T195), T196, T197, cons(T194, X243)) → APPENDN_IN_GGGA(T195, T196, T197, X243)
U37_GAGGAGA(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_GAGGAGA(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
U37_GAGGAGA(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → PR_IN_GAGGA(cons(T212, T222), X13, T225, T214, T9)
PR_IN_GAGGA(T94, T157, T156, T73, T9) → U25_GAGGA(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
PR_IN_GAGGA(T94, T157, T156, T73, T9) → QSL_IN_GA(T94, T157)
U25_GAGGA(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_GAGGA(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U25_GAGGA(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → APPENDF_IN_GGGA(T156, T73, T157, T9)
U19_GGAGAGA(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_GGAGAGA(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U19_GGAGAGA(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → PR_IN_GAGGA(T94, X13, T156, T73, T9)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
QSA_IN_GA(cons(T14, []), T9) → U1_GA(T14, T9, pB_in_aaga(X12, X13, T14, T9))
QSA_IN_GA(cons(T14, []), T9) → PB_IN_AAGA(X12, X13, T14, T9)
PB_IN_AAGA(T19, X13, T14, T9) → U11_AAGA(T19, X13, T14, T9, qsE_in_a(T19))
PB_IN_AAGA(T19, X13, T14, T9) → QSE_IN_A(T19)
U11_AAGA(T19, X13, T14, T9, qsE_out_a(T19)) → U12_AAGA(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
U11_AAGA(T19, X13, T14, T9, qsE_out_a(T19)) → PO_IN_AGGA(X13, T19, T14, T9)
PO_IN_AGGA(T24, T19, T14, T9) → U13_AGGA(T24, T19, T14, T9, qsE_in_a(T24))
PO_IN_AGGA(T24, T19, T14, T9) → QSE_IN_A(T24)
U13_AGGA(T24, T19, T14, T9, qsE_out_a(T24)) → U14_AGGA(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
U13_AGGA(T24, T19, T14, T9, qsE_out_a(T24)) → APPENDF_IN_GGGA(T19, T14, T24, T9)
APPENDF_IN_GGGA(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_GGGA(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
APPENDF_IN_GGGA(cons(T49, T50), T51, T52, cons(T49, T54)) → APPENDF_IN_GGGA(T50, T51, T52, T54)
QSA_IN_GA(cons(T73, cons(T71, T72)), T9) → U2_GA(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
QSA_IN_GA(cons(T73, cons(T71, T72)), T9) → PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9)
PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9) → U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9) → LESSG_IN_GG(T71, T73)
LESSG_IN_GG(s(T87), s(T88)) → U5_GG(T87, T88, lessG_in_gg(T87, T88))
LESSG_IN_GG(s(T87), s(T88)) → LESSG_IN_GG(T87, T88)
U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → PP_IN_GGAAGAAA(T72, T73, X84, X85, T71, X12, X13, T9)
PP_IN_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9) → U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
PP_IN_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9) → SPLITH_IN_GGAA(T72, T73, T93, T94)
SPLITH_IN_GGAA(cons(T114, T115), T116, cons(T114, X145), X146) → U6_GGAA(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
SPLITH_IN_GGAA(cons(T114, T115), T116, cons(T114, X145), X146) → PI_IN_GGGAA(T114, T116, T115, X145, X146)
PI_IN_GGGAA(T114, T116, T115, X145, X146) → U21_GGGAA(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
PI_IN_GGGAA(T114, T116, T115, X145, X146) → LESSG_IN_GG(T114, T116)
U21_GGGAA(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_GGGAA(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
U21_GGGAA(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → SPLITH_IN_GGAA(T115, T116, X145, X146)
SPLITH_IN_GGAA(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_GGAA(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
SPLITH_IN_GGAA(cons(T129, T130), T131, X172, cons(T129, X173)) → PJ_IN_GGGAA(T129, T131, T130, X172, X173)
PJ_IN_GGGAA(T129, T131, T130, X172, X173) → U23_GGGAA(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
PJ_IN_GGGAA(T129, T131, T130, X172, X173) → GEQK_IN_GG(T129, T131)
GEQK_IN_GG(s(T150), s(T151)) → U8_GG(T150, T151, geqK_in_gg(T150, T151))
GEQK_IN_GG(s(T150), s(T151)) → GEQK_IN_GG(T150, T151)
U23_GGGAA(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_GGGAA(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U23_GGGAA(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → SPLITH_IN_GGAA(T130, T131, X172, X173)
U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → PQ_IN_GGAGAGA(T71, T93, X12, T94, X13, T73, T9)
PQ_IN_GGAGAGA(T71, T93, T156, T94, X13, T73, T9) → U19_GGAGAGA(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
PQ_IN_GGAGAGA(T71, T93, T156, T94, X13, T73, T9) → QSA_IN_GA(cons(T71, T93), T156)
QSA_IN_GA(cons(T214, cons(T212, T213)), T9) → U3_GA(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
QSA_IN_GA(cons(T214, cons(T212, T213)), T9) → PD_IN_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9)
PD_IN_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9) → U33_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
PD_IN_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9) → GEQK_IN_GG(T212, T214)
U33_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
U33_GGGAAAAA(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → PU_IN_GGAAAGAA(T213, T214, X267, X268, X12, T212, X13, T9)
PU_IN_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9) → U35_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
PU_IN_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9) → SPLITH_IN_GGAA(T213, T214, T221, T222)
U35_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
U35_GGAAAGAA(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → PV_IN_GAGGAGA(T221, X12, T212, T222, X13, T214, T9)
PV_IN_GAGGAGA(T221, T225, T212, T222, X13, T214, T9) → U37_GAGGAGA(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
PV_IN_GAGGAGA(T221, T225, T212, T222, X13, T214, T9) → QSL_IN_GA(T221, T225)
QSL_IN_GA(cons(T162, T163), X217) → U9_GA(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
QSL_IN_GA(cons(T162, T163), X217) → PM_IN_GGAAAAA(T163, T162, X213, X214, X215, X216, X217)
PM_IN_GGAAAAA(T163, T162, T166, T167, X215, X216, X217) → U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
PM_IN_GGAAAAA(T163, T162, T166, T167, X215, X216, X217) → SPLITH_IN_GGAA(T163, T162, T166, T167)
U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → PS_IN_GAGAGA(T166, X215, T167, X216, T162, X217)
PS_IN_GAGAGA(T166, T170, T167, X216, T162, X217) → U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
PS_IN_GAGAGA(T166, T170, T167, X216, T162, X217) → QSL_IN_GA(T166, T170)
U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_GAGAGA(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → PT_IN_GAGGA(T167, X216, T170, T162, X217)
PT_IN_GAGGA(T167, T171, T170, T162, X217) → U31_GAGGA(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
PT_IN_GAGGA(T167, T171, T170, T162, X217) → QSL_IN_GA(T167, T171)
U31_GAGGA(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_GAGGA(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
U31_GAGGA(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → APPENDN_IN_GGGA(T170, T162, T171, X217)
APPENDN_IN_GGGA(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_GGGA(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
APPENDN_IN_GGGA(cons(T194, T195), T196, T197, cons(T194, X243)) → APPENDN_IN_GGGA(T195, T196, T197, X243)
U37_GAGGAGA(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_GAGGAGA(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
U37_GAGGAGA(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → PR_IN_GAGGA(cons(T212, T222), X13, T225, T214, T9)
PR_IN_GAGGA(T94, T157, T156, T73, T9) → U25_GAGGA(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
PR_IN_GAGGA(T94, T157, T156, T73, T9) → QSL_IN_GA(T94, T157)
U25_GAGGA(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_GAGGA(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U25_GAGGA(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → APPENDF_IN_GGGA(T156, T73, T157, T9)
U19_GGAGAGA(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_GGAGAGA(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U19_GGAGAGA(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → PR_IN_GAGGA(T94, X13, T156, T73, T9)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
APPENDN_IN_GGGA(cons(T194, T195), T196, T197, cons(T194, X243)) → APPENDN_IN_GGGA(T195, T196, T197, X243)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
APPENDN_IN_GGGA(cons(T194, T195), T196, T197, cons(T194, X243)) → APPENDN_IN_GGGA(T195, T196, T197, X243)
APPENDN_IN_GGGA(cons(T194, T195), T196, T197) → APPENDN_IN_GGGA(T195, T196, T197)
From the DPs we obtained the following set of size-change graphs:
GEQK_IN_GG(s(T150), s(T151)) → GEQK_IN_GG(T150, T151)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
GEQK_IN_GG(s(T150), s(T151)) → GEQK_IN_GG(T150, T151)
GEQK_IN_GG(s(T150), s(T151)) → GEQK_IN_GG(T150, T151)
From the DPs we obtained the following set of size-change graphs:
LESSG_IN_GG(s(T87), s(T88)) → LESSG_IN_GG(T87, T88)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
LESSG_IN_GG(s(T87), s(T88)) → LESSG_IN_GG(T87, T88)
LESSG_IN_GG(s(T87), s(T88)) → LESSG_IN_GG(T87, T88)
From the DPs we obtained the following set of size-change graphs:
PI_IN_GGGAA(T114, T116, T115, X145, X146) → U21_GGGAA(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_GGGAA(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → SPLITH_IN_GGAA(T115, T116, X145, X146)
SPLITH_IN_GGAA(cons(T114, T115), T116, cons(T114, X145), X146) → PI_IN_GGGAA(T114, T116, T115, X145, X146)
SPLITH_IN_GGAA(cons(T129, T130), T131, X172, cons(T129, X173)) → PJ_IN_GGGAA(T129, T131, T130, X172, X173)
PJ_IN_GGGAA(T129, T131, T130, X172, X173) → U23_GGGAA(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
U23_GGGAA(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → SPLITH_IN_GGAA(T130, T131, X172, X173)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
PI_IN_GGGAA(T114, T116, T115, X145, X146) → U21_GGGAA(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_GGGAA(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → SPLITH_IN_GGAA(T115, T116, X145, X146)
SPLITH_IN_GGAA(cons(T114, T115), T116, cons(T114, X145), X146) → PI_IN_GGGAA(T114, T116, T115, X145, X146)
SPLITH_IN_GGAA(cons(T129, T130), T131, X172, cons(T129, X173)) → PJ_IN_GGGAA(T129, T131, T130, X172, X173)
PJ_IN_GGGAA(T129, T131, T130, X172, X173) → U23_GGGAA(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
U23_GGGAA(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → SPLITH_IN_GGAA(T130, T131, X172, X173)
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
PI_IN_GGGAA(T114, T116, T115) → U21_GGGAA(T114, T116, T115, lessG_in_gg(T114, T116))
U21_GGGAA(T114, T116, T115, lessG_out_gg(T114, T116)) → SPLITH_IN_GGAA(T115, T116)
SPLITH_IN_GGAA(cons(T114, T115), T116) → PI_IN_GGGAA(T114, T116, T115)
SPLITH_IN_GGAA(cons(T129, T130), T131) → PJ_IN_GGGAA(T129, T131, T130)
PJ_IN_GGGAA(T129, T131, T130) → U23_GGGAA(T129, T131, T130, geqK_in_gg(T129, T131))
U23_GGGAA(T129, T131, T130, geqK_out_gg(T129, T131)) → SPLITH_IN_GGAA(T130, T131)
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
lessG_in_gg(x0, x1)
geqK_in_gg(x0, x1)
U5_gg(x0, x1, x2)
U8_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
PM_IN_GGAAAAA(T163, T162, T166, T167, X215, X216, X217) → U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → PS_IN_GAGAGA(T166, X215, T167, X216, T162, X217)
PS_IN_GAGAGA(T166, T170, T167, X216, T162, X217) → U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → PT_IN_GAGGA(T167, X216, T170, T162, X217)
PT_IN_GAGGA(T167, T171, T170, T162, X217) → QSL_IN_GA(T167, T171)
QSL_IN_GA(cons(T162, T163), X217) → PM_IN_GGAAAAA(T163, T162, X213, X214, X215, X216, X217)
PS_IN_GAGAGA(T166, T170, T167, X216, T162, X217) → QSL_IN_GA(T166, T170)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
PM_IN_GGAAAAA(T163, T162, T166, T167, X215, X216, X217) → U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_GGAAAAA(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → PS_IN_GAGAGA(T166, X215, T167, X216, T162, X217)
PS_IN_GAGAGA(T166, T170, T167, X216, T162, X217) → U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_GAGAGA(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → PT_IN_GAGGA(T167, X216, T170, T162, X217)
PT_IN_GAGGA(T167, T171, T170, T162, X217) → QSL_IN_GA(T167, T171)
QSL_IN_GA(cons(T162, T163), X217) → PM_IN_GGAAAAA(T163, T162, X213, X214, X215, X216, X217)
PS_IN_GAGAGA(T166, T170, T167, X216, T162, X217) → QSL_IN_GA(T166, T170)
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
PM_IN_GGAAAAA(T163, T162) → U27_GGAAAAA(T163, T162, splitH_in_ggaa(T163, T162))
U27_GGAAAAA(T163, T162, splitH_out_ggaa(T163, T162, T166, T167)) → PS_IN_GAGAGA(T166, T167, T162)
PS_IN_GAGAGA(T166, T167, T162) → U29_GAGAGA(T166, T167, T162, qsL_in_ga(T166))
U29_GAGAGA(T166, T167, T162, qsL_out_ga(T166, T170)) → PT_IN_GAGGA(T167, T170, T162)
PT_IN_GAGGA(T167, T170, T162) → QSL_IN_GA(T167)
QSL_IN_GA(cons(T162, T163)) → PM_IN_GGAAAAA(T163, T162)
PS_IN_GAGAGA(T166, T167, T162) → QSL_IN_GA(T166)
splitH_in_ggaa([], T101) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116) → U6_ggaa(T114, T115, T116, pI_in_gggaa(T114, T116, T115))
splitH_in_ggaa(cons(T129, T130), T131) → U7_ggaa(T129, T130, T131, pJ_in_gggaa(T129, T131, T130))
qsL_in_ga([]) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163)) → U9_ga(T162, T163, pM_in_ggaaaaa(T163, T162))
U6_ggaa(T114, T115, T116, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U7_ggaa(T129, T130, T131, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U9_ga(T162, T163, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
pI_in_gggaa(T114, T116, T115) → U21_gggaa(T114, T116, T115, lessG_in_gg(T114, T116))
pJ_in_gggaa(T129, T131, T130) → U23_gggaa(T129, T131, T130, geqK_in_gg(T129, T131))
pM_in_ggaaaaa(T163, T162) → U27_ggaaaaa(T163, T162, splitH_in_ggaa(T163, T162))
U21_gggaa(T114, T116, T115, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, splitH_in_ggaa(T115, T116))
U23_gggaa(T129, T131, T130, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, splitH_in_ggaa(T130, T131))
U27_ggaaaaa(T163, T162, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, pS_in_gagaga(T166, T167, T162))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U22_gggaa(T114, T116, T115, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U24_gggaa(T129, T131, T130, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U28_ggaaaaa(T163, T162, T166, T167, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
pS_in_gagaga(T166, T167, T162) → U29_gagaga(T166, T167, T162, qsL_in_ga(T166))
U29_gagaga(T166, T167, T162, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, T162, pT_in_gagga(T167, T170, T162))
U30_gagaga(T166, T170, T167, T162, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
pT_in_gagga(T167, T170, T162) → U31_gagga(T167, T170, T162, qsL_in_ga(T167))
U31_gagga(T167, T170, T162, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, appendN_in_ggga(T170, T162, T171))
U32_gagga(T167, T171, T170, T162, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
appendN_in_ggga([], T184, T185) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197) → U10_ggga(T194, T195, T196, T197, appendN_in_ggga(T195, T196, T197))
U10_ggga(T194, T195, T196, T197, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
splitH_in_ggaa(x0, x1)
qsL_in_ga(x0)
U6_ggaa(x0, x1, x2, x3)
U7_ggaa(x0, x1, x2, x3)
U9_ga(x0, x1, x2)
pI_in_gggaa(x0, x1, x2)
pJ_in_gggaa(x0, x1, x2)
pM_in_ggaaaaa(x0, x1)
U21_gggaa(x0, x1, x2, x3)
U23_gggaa(x0, x1, x2, x3)
U27_ggaaaaa(x0, x1, x2)
lessG_in_gg(x0, x1)
U22_gggaa(x0, x1, x2, x3)
geqK_in_gg(x0, x1)
U24_gggaa(x0, x1, x2, x3)
U28_ggaaaaa(x0, x1, x2, x3, x4)
U5_gg(x0, x1, x2)
U8_gg(x0, x1, x2)
pS_in_gagaga(x0, x1, x2)
U29_gagaga(x0, x1, x2, x3)
U30_gagaga(x0, x1, x2, x3, x4)
pT_in_gagga(x0, x1, x2)
U31_gagga(x0, x1, x2, x3)
U32_gagga(x0, x1, x2, x3, x4)
appendN_in_ggga(x0, x1, x2)
U10_ggga(x0, x1, x2, x3, x4)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PM_IN_GGAAAAA(T163, T162) → U27_GGAAAAA(T163, T162, splitH_in_ggaa(T163, T162))
POL(0) = 0
POL(PM_IN_GGAAAAA(x1, x2)) = 1 + x1
POL(PS_IN_GAGAGA(x1, x2, x3)) = x1 + x2
POL(PT_IN_GAGGA(x1, x2, x3)) = x1
POL(QSL_IN_GA(x1)) = x1
POL(U10_ggga(x1, x2, x3, x4, x5)) = 0
POL(U21_gggaa(x1, x2, x3, x4)) = 1 + x3
POL(U22_gggaa(x1, x2, x3, x4)) = 1 + x4
POL(U23_gggaa(x1, x2, x3, x4)) = x3
POL(U24_gggaa(x1, x2, x3, x4)) = x4
POL(U27_GGAAAAA(x1, x2, x3)) = x3
POL(U27_ggaaaaa(x1, x2, x3)) = 0
POL(U28_ggaaaaa(x1, x2, x3, x4, x5)) = 0
POL(U29_GAGAGA(x1, x2, x3, x4)) = x2
POL(U29_gagaga(x1, x2, x3, x4)) = 0
POL(U30_gagaga(x1, x2, x3, x4, x5)) = 0
POL(U31_gagga(x1, x2, x3, x4)) = 0
POL(U32_gagga(x1, x2, x3, x4, x5)) = 0
POL(U5_gg(x1, x2, x3)) = 0
POL(U6_ggaa(x1, x2, x3, x4)) = x4
POL(U7_ggaa(x1, x2, x3, x4)) = 1 + x4
POL(U8_gg(x1, x2, x3)) = 0
POL(U9_ga(x1, x2, x3)) = 0
POL([]) = 0
POL(appendN_in_ggga(x1, x2, x3)) = 0
POL(appendN_out_ggga(x1, x2, x3, x4)) = 0
POL(cons(x1, x2)) = 1 + x2
POL(geqK_in_gg(x1, x2)) = 0
POL(geqK_out_gg(x1, x2)) = 0
POL(lessG_in_gg(x1, x2)) = 0
POL(lessG_out_gg(x1, x2)) = 0
POL(pI_in_gggaa(x1, x2, x3)) = 1 + x3
POL(pI_out_gggaa(x1, x2, x3, x4, x5)) = 1 + x4 + x5
POL(pJ_in_gggaa(x1, x2, x3)) = x3
POL(pJ_out_gggaa(x1, x2, x3, x4, x5)) = x4 + x5
POL(pM_in_ggaaaaa(x1, x2)) = 0
POL(pM_out_ggaaaaa(x1, x2, x3, x4, x5, x6, x7)) = 0
POL(pS_in_gagaga(x1, x2, x3)) = 0
POL(pS_out_gagaga(x1, x2, x3, x4, x5, x6)) = 0
POL(pT_in_gagga(x1, x2, x3)) = 0
POL(pT_out_gagga(x1, x2, x3, x4, x5)) = 0
POL(qsL_in_ga(x1)) = 0
POL(qsL_out_ga(x1, x2)) = 0
POL(s(x1)) = 0
POL(splitH_in_ggaa(x1, x2)) = x1
POL(splitH_out_ggaa(x1, x2, x3, x4)) = x3 + x4
splitH_in_ggaa([], T101) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116) → U6_ggaa(T114, T115, T116, pI_in_gggaa(T114, T116, T115))
splitH_in_ggaa(cons(T129, T130), T131) → U7_ggaa(T129, T130, T131, pJ_in_gggaa(T129, T131, T130))
U6_ggaa(T114, T115, T116, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
pI_in_gggaa(T114, T116, T115) → U21_gggaa(T114, T116, T115, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, splitH_in_ggaa(T115, T116))
U22_gggaa(T114, T116, T115, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U7_ggaa(T129, T130, T131, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
pJ_in_gggaa(T129, T131, T130) → U23_gggaa(T129, T131, T130, geqK_in_gg(T129, T131))
U23_gggaa(T129, T131, T130, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, splitH_in_ggaa(T130, T131))
U24_gggaa(T129, T131, T130, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U27_GGAAAAA(T163, T162, splitH_out_ggaa(T163, T162, T166, T167)) → PS_IN_GAGAGA(T166, T167, T162)
PS_IN_GAGAGA(T166, T167, T162) → U29_GAGAGA(T166, T167, T162, qsL_in_ga(T166))
U29_GAGAGA(T166, T167, T162, qsL_out_ga(T166, T170)) → PT_IN_GAGGA(T167, T170, T162)
PT_IN_GAGGA(T167, T170, T162) → QSL_IN_GA(T167)
QSL_IN_GA(cons(T162, T163)) → PM_IN_GGAAAAA(T163, T162)
PS_IN_GAGAGA(T166, T167, T162) → QSL_IN_GA(T166)
splitH_in_ggaa([], T101) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116) → U6_ggaa(T114, T115, T116, pI_in_gggaa(T114, T116, T115))
splitH_in_ggaa(cons(T129, T130), T131) → U7_ggaa(T129, T130, T131, pJ_in_gggaa(T129, T131, T130))
qsL_in_ga([]) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163)) → U9_ga(T162, T163, pM_in_ggaaaaa(T163, T162))
U6_ggaa(T114, T115, T116, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U7_ggaa(T129, T130, T131, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U9_ga(T162, T163, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
pI_in_gggaa(T114, T116, T115) → U21_gggaa(T114, T116, T115, lessG_in_gg(T114, T116))
pJ_in_gggaa(T129, T131, T130) → U23_gggaa(T129, T131, T130, geqK_in_gg(T129, T131))
pM_in_ggaaaaa(T163, T162) → U27_ggaaaaa(T163, T162, splitH_in_ggaa(T163, T162))
U21_gggaa(T114, T116, T115, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, splitH_in_ggaa(T115, T116))
U23_gggaa(T129, T131, T130, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, splitH_in_ggaa(T130, T131))
U27_ggaaaaa(T163, T162, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, pS_in_gagaga(T166, T167, T162))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U22_gggaa(T114, T116, T115, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U24_gggaa(T129, T131, T130, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U28_ggaaaaa(T163, T162, T166, T167, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
pS_in_gagaga(T166, T167, T162) → U29_gagaga(T166, T167, T162, qsL_in_ga(T166))
U29_gagaga(T166, T167, T162, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, T162, pT_in_gagga(T167, T170, T162))
U30_gagaga(T166, T170, T167, T162, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
pT_in_gagga(T167, T170, T162) → U31_gagga(T167, T170, T162, qsL_in_ga(T167))
U31_gagga(T167, T170, T162, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, appendN_in_ggga(T170, T162, T171))
U32_gagga(T167, T171, T170, T162, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
appendN_in_ggga([], T184, T185) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197) → U10_ggga(T194, T195, T196, T197, appendN_in_ggga(T195, T196, T197))
U10_ggga(T194, T195, T196, T197, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
splitH_in_ggaa(x0, x1)
qsL_in_ga(x0)
U6_ggaa(x0, x1, x2, x3)
U7_ggaa(x0, x1, x2, x3)
U9_ga(x0, x1, x2)
pI_in_gggaa(x0, x1, x2)
pJ_in_gggaa(x0, x1, x2)
pM_in_ggaaaaa(x0, x1)
U21_gggaa(x0, x1, x2, x3)
U23_gggaa(x0, x1, x2, x3)
U27_ggaaaaa(x0, x1, x2)
lessG_in_gg(x0, x1)
U22_gggaa(x0, x1, x2, x3)
geqK_in_gg(x0, x1)
U24_gggaa(x0, x1, x2, x3)
U28_ggaaaaa(x0, x1, x2, x3, x4)
U5_gg(x0, x1, x2)
U8_gg(x0, x1, x2)
pS_in_gagaga(x0, x1, x2)
U29_gagaga(x0, x1, x2, x3)
U30_gagaga(x0, x1, x2, x3, x4)
pT_in_gagga(x0, x1, x2)
U31_gagga(x0, x1, x2, x3)
U32_gagga(x0, x1, x2, x3, x4)
appendN_in_ggga(x0, x1, x2)
U10_ggga(x0, x1, x2, x3, x4)
APPENDF_IN_GGGA(cons(T49, T50), T51, T52, cons(T49, T54)) → APPENDF_IN_GGGA(T50, T51, T52, T54)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
APPENDF_IN_GGGA(cons(T49, T50), T51, T52, cons(T49, T54)) → APPENDF_IN_GGGA(T50, T51, T52, T54)
APPENDF_IN_GGGA(cons(T49, T50), T51, T52) → APPENDF_IN_GGGA(T50, T51, T52)
From the DPs we obtained the following set of size-change graphs:
QSA_IN_GA(cons(T73, cons(T71, T72)), T9) → PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9)
PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9) → U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → PP_IN_GGAAGAAA(T72, T73, X84, X85, T71, X12, X13, T9)
PP_IN_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9) → U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → PQ_IN_GGAGAGA(T71, T93, X12, T94, X13, T73, T9)
PQ_IN_GGAGAGA(T71, T93, T156, T94, X13, T73, T9) → QSA_IN_GA(cons(T71, T93), T156)
qsA_in_ga([], []) → qsA_out_ga([], [])
qsA_in_ga(cons(T14, []), T9) → U1_ga(T14, T9, pB_in_aaga(X12, X13, T14, T9))
pB_in_aaga(T19, X13, T14, T9) → U11_aaga(T19, X13, T14, T9, qsE_in_a(T19))
qsE_in_a([]) → qsE_out_a([])
U11_aaga(T19, X13, T14, T9, qsE_out_a(T19)) → U12_aaga(T19, X13, T14, T9, pO_in_agga(X13, T19, T14, T9))
pO_in_agga(T24, T19, T14, T9) → U13_agga(T24, T19, T14, T9, qsE_in_a(T24))
U13_agga(T24, T19, T14, T9, qsE_out_a(T24)) → U14_agga(T24, T19, T14, T9, appendF_in_ggga(T19, T14, T24, T9))
appendF_in_ggga([], T37, T38, cons(T37, T38)) → appendF_out_ggga([], T37, T38, cons(T37, T38))
appendF_in_ggga(cons(T49, T50), T51, T52, cons(T49, T54)) → U4_ggga(T49, T50, T51, T52, T54, appendF_in_ggga(T50, T51, T52, T54))
U4_ggga(T49, T50, T51, T52, T54, appendF_out_ggga(T50, T51, T52, T54)) → appendF_out_ggga(cons(T49, T50), T51, T52, cons(T49, T54))
U14_agga(T24, T19, T14, T9, appendF_out_ggga(T19, T14, T24, T9)) → pO_out_agga(T24, T19, T14, T9)
U12_aaga(T19, X13, T14, T9, pO_out_agga(X13, T19, T14, T9)) → pB_out_aaga(T19, X13, T14, T9)
U1_ga(T14, T9, pB_out_aaga(X12, X13, T14, T9)) → qsA_out_ga(cons(T14, []), T9)
qsA_in_ga(cons(T73, cons(T71, T72)), T9) → U2_ga(T73, T71, T72, T9, pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9))
pC_in_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9) → U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U15_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_in_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9))
pP_in_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9) → U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U17_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_in_ggagaga(T71, T93, X12, T94, X13, T73, T9))
pQ_in_ggagaga(T71, T93, T156, T94, X13, T73, T9) → U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_in_ga(cons(T71, T93), T156))
qsA_in_ga(cons(T214, cons(T212, T213)), T9) → U3_ga(T214, T212, T213, T9, pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9))
pD_in_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9) → U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_in_gg(T212, T214))
U33_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, geqK_out_gg(T212, T214)) → U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_in_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9))
pU_in_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9) → U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_in_ggaa(T213, T214, T221, T222))
U35_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, splitH_out_ggaa(T213, T214, T221, T222)) → U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_in_gaggaga(T221, X12, T212, T222, X13, T214, T9))
pV_in_gaggaga(T221, T225, T212, T222, X13, T214, T9) → U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_in_ga(T221, T225))
qsL_in_ga([], []) → qsL_out_ga([], [])
qsL_in_ga(cons(T162, T163), X217) → U9_ga(T162, T163, X217, pM_in_ggaaaaa(T163, T162, X213, X214, X215, X216, X217))
pM_in_ggaaaaa(T163, T162, T166, T167, X215, X216, X217) → U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_in_ggaa(T163, T162, T166, T167))
U27_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, splitH_out_ggaa(T163, T162, T166, T167)) → U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_in_gagaga(T166, X215, T167, X216, T162, X217))
pS_in_gagaga(T166, T170, T167, X216, T162, X217) → U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_in_ga(T166, T170))
U29_gagaga(T166, T170, T167, X216, T162, X217, qsL_out_ga(T166, T170)) → U30_gagaga(T166, T170, T167, X216, T162, X217, pT_in_gagga(T167, X216, T170, T162, X217))
pT_in_gagga(T167, T171, T170, T162, X217) → U31_gagga(T167, T171, T170, T162, X217, qsL_in_ga(T167, T171))
U31_gagga(T167, T171, T170, T162, X217, qsL_out_ga(T167, T171)) → U32_gagga(T167, T171, T170, T162, X217, appendN_in_ggga(T170, T162, T171, X217))
appendN_in_ggga([], T184, T185, cons(T184, T185)) → appendN_out_ggga([], T184, T185, cons(T184, T185))
appendN_in_ggga(cons(T194, T195), T196, T197, cons(T194, X243)) → U10_ggga(T194, T195, T196, T197, X243, appendN_in_ggga(T195, T196, T197, X243))
U10_ggga(T194, T195, T196, T197, X243, appendN_out_ggga(T195, T196, T197, X243)) → appendN_out_ggga(cons(T194, T195), T196, T197, cons(T194, X243))
U32_gagga(T167, T171, T170, T162, X217, appendN_out_ggga(T170, T162, T171, X217)) → pT_out_gagga(T167, T171, T170, T162, X217)
U30_gagaga(T166, T170, T167, X216, T162, X217, pT_out_gagga(T167, X216, T170, T162, X217)) → pS_out_gagaga(T166, T170, T167, X216, T162, X217)
U28_ggaaaaa(T163, T162, T166, T167, X215, X216, X217, pS_out_gagaga(T166, X215, T167, X216, T162, X217)) → pM_out_ggaaaaa(T163, T162, T166, T167, X215, X216, X217)
U9_ga(T162, T163, X217, pM_out_ggaaaaa(T163, T162, X213, X214, X215, X216, X217)) → qsL_out_ga(cons(T162, T163), X217)
U37_gaggaga(T221, T225, T212, T222, X13, T214, T9, qsL_out_ga(T221, T225)) → U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_in_gagga(cons(T212, T222), X13, T225, T214, T9))
pR_in_gagga(T94, T157, T156, T73, T9) → U25_gagga(T94, T157, T156, T73, T9, qsL_in_ga(T94, T157))
U25_gagga(T94, T157, T156, T73, T9, qsL_out_ga(T94, T157)) → U26_gagga(T94, T157, T156, T73, T9, appendF_in_ggga(T156, T73, T157, T9))
U26_gagga(T94, T157, T156, T73, T9, appendF_out_ggga(T156, T73, T157, T9)) → pR_out_gagga(T94, T157, T156, T73, T9)
U38_gaggaga(T221, T225, T212, T222, X13, T214, T9, pR_out_gagga(cons(T212, T222), X13, T225, T214, T9)) → pV_out_gaggaga(T221, T225, T212, T222, X13, T214, T9)
U36_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9, pV_out_gaggaga(T221, X12, T212, T222, X13, T214, T9)) → pU_out_ggaaagaa(T213, T214, T221, T222, X12, T212, X13, T9)
U34_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9, pU_out_ggaaagaa(T213, T214, X267, X268, X12, T212, X13, T9)) → pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)
U3_ga(T214, T212, T213, T9, pD_out_gggaaaaa(T212, T214, T213, X267, X268, X12, X13, T9)) → qsA_out_ga(cons(T214, cons(T212, T213)), T9)
U19_ggagaga(T71, T93, T156, T94, X13, T73, T9, qsA_out_ga(cons(T71, T93), T156)) → U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_in_gagga(T94, X13, T156, T73, T9))
U20_ggagaga(T71, T93, T156, T94, X13, T73, T9, pR_out_gagga(T94, X13, T156, T73, T9)) → pQ_out_ggagaga(T71, T93, T156, T94, X13, T73, T9)
U18_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9, pQ_out_ggagaga(T71, T93, X12, T94, X13, T73, T9)) → pP_out_ggaagaaa(T72, T73, T93, T94, T71, X12, X13, T9)
U16_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9, pP_out_ggaagaaa(T72, T73, X84, X85, T71, X12, X13, T9)) → pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)
U2_ga(T73, T71, T72, T9, pC_out_gggaaaaa(T71, T73, T72, X84, X85, X12, X13, T9)) → qsA_out_ga(cons(T73, cons(T71, T72)), T9)
QSA_IN_GA(cons(T73, cons(T71, T72)), T9) → PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9)
PC_IN_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9) → U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_in_gg(T71, T73))
U15_GGGAAAAA(T71, T73, T72, X84, X85, X12, X13, T9, lessG_out_gg(T71, T73)) → PP_IN_GGAAGAAA(T72, T73, X84, X85, T71, X12, X13, T9)
PP_IN_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9) → U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_in_ggaa(T72, T73, T93, T94))
U17_GGAAGAAA(T72, T73, T93, T94, T71, X12, X13, T9, splitH_out_ggaa(T72, T73, T93, T94)) → PQ_IN_GGAGAGA(T71, T93, X12, T94, X13, T73, T9)
PQ_IN_GGAGAGA(T71, T93, T156, T94, X13, T73, T9) → QSA_IN_GA(cons(T71, T93), T156)
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
splitH_in_ggaa([], T101, [], []) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116, cons(T114, X145), X146) → U6_ggaa(T114, T115, T116, X145, X146, pI_in_gggaa(T114, T116, T115, X145, X146))
splitH_in_ggaa(cons(T129, T130), T131, X172, cons(T129, X173)) → U7_ggaa(T129, T130, T131, X172, X173, pJ_in_gggaa(T129, T131, T130, X172, X173))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U6_ggaa(T114, T115, T116, X145, X146, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U7_ggaa(T129, T130, T131, X172, X173, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
pI_in_gggaa(T114, T116, T115, X145, X146) → U21_gggaa(T114, T116, T115, X145, X146, lessG_in_gg(T114, T116))
pJ_in_gggaa(T129, T131, T130, X172, X173) → U23_gggaa(T129, T131, T130, X172, X173, geqK_in_gg(T129, T131))
U21_gggaa(T114, T116, T115, X145, X146, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, X145, X146, splitH_in_ggaa(T115, T116, X145, X146))
U23_gggaa(T129, T131, T130, X172, X173, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, X172, X173, splitH_in_ggaa(T130, T131, X172, X173))
U22_gggaa(T114, T116, T115, X145, X146, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U24_gggaa(T129, T131, T130, X172, X173, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
QSA_IN_GA(cons(T73, cons(T71, T72))) → PC_IN_GGGAAAAA(T71, T73, T72)
PC_IN_GGGAAAAA(T71, T73, T72) → U15_GGGAAAAA(T71, T73, T72, lessG_in_gg(T71, T73))
U15_GGGAAAAA(T71, T73, T72, lessG_out_gg(T71, T73)) → PP_IN_GGAAGAAA(T72, T73, T71)
PP_IN_GGAAGAAA(T72, T73, T71) → U17_GGAAGAAA(T72, T73, T71, splitH_in_ggaa(T72, T73))
U17_GGAAGAAA(T72, T73, T71, splitH_out_ggaa(T72, T73, T93, T94)) → PQ_IN_GGAGAGA(T71, T93, T94, T73)
PQ_IN_GGAGAGA(T71, T93, T94, T73) → QSA_IN_GA(cons(T71, T93))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
splitH_in_ggaa([], T101) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116) → U6_ggaa(T114, T115, T116, pI_in_gggaa(T114, T116, T115))
splitH_in_ggaa(cons(T129, T130), T131) → U7_ggaa(T129, T130, T131, pJ_in_gggaa(T129, T131, T130))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U6_ggaa(T114, T115, T116, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U7_ggaa(T129, T130, T131, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
pI_in_gggaa(T114, T116, T115) → U21_gggaa(T114, T116, T115, lessG_in_gg(T114, T116))
pJ_in_gggaa(T129, T131, T130) → U23_gggaa(T129, T131, T130, geqK_in_gg(T129, T131))
U21_gggaa(T114, T116, T115, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, splitH_in_ggaa(T115, T116))
U23_gggaa(T129, T131, T130, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, splitH_in_ggaa(T130, T131))
U22_gggaa(T114, T116, T115, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U24_gggaa(T129, T131, T130, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
lessG_in_gg(x0, x1)
splitH_in_ggaa(x0, x1)
U5_gg(x0, x1, x2)
U6_ggaa(x0, x1, x2, x3)
U7_ggaa(x0, x1, x2, x3)
pI_in_gggaa(x0, x1, x2)
pJ_in_gggaa(x0, x1, x2)
U21_gggaa(x0, x1, x2, x3)
U23_gggaa(x0, x1, x2, x3)
U22_gggaa(x0, x1, x2, x3)
geqK_in_gg(x0, x1)
U24_gggaa(x0, x1, x2, x3)
U8_gg(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QSA_IN_GA(cons(T73, cons(T71, T72))) → PC_IN_GGGAAAAA(T71, T73, T72)
POL( U15_GGGAAAAA(x1, ..., x4) ) = max{0, 2x4 - 1}
POL( U17_GGAAGAAA(x1, ..., x4) ) = 2x3 + 1
POL( U21_gggaa(x1, ..., x4) ) = max{0, -2}
POL( lessG_in_gg(x1, x2) ) = x2
POL( 0 ) = 0
POL( s(x1) ) = x1 + 2
POL( lessG_out_gg(x1, x2) ) = x1 + 1
POL( U5_gg(x1, ..., x3) ) = x3 + 2
POL( splitH_in_ggaa(x1, x2) ) = 0
POL( [] ) = 1
POL( splitH_out_ggaa(x1, ..., x4) ) = max{0, x2 + x4 - 2}
POL( cons(x1, x2) ) = x1
POL( U6_ggaa(x1, ..., x4) ) = 2x2 + 2x4 + 2
POL( pI_in_gggaa(x1, ..., x3) ) = 2
POL( U7_ggaa(x1, ..., x4) ) = 2x3 + 2x4 + 2
POL( pJ_in_gggaa(x1, ..., x3) ) = 0
POL( U22_gggaa(x1, ..., x4) ) = max{0, 2x3 - 2}
POL( pI_out_gggaa(x1, ..., x5) ) = x1 + x2 + 2x4
POL( pJ_out_gggaa(x1, ..., x5) ) = 2x1 + 2x2 + 2x3 + 2x4 + x5
POL( U23_gggaa(x1, ..., x4) ) = max{0, x1 + x3 - 2}
POL( geqK_in_gg(x1, x2) ) = x2
POL( geqK_out_gg(x1, x2) ) = max{0, -2}
POL( U8_gg(x1, ..., x3) ) = x1 + 2x2 + 2
POL( U24_gggaa(x1, ..., x4) ) = x2 + x3 + 2
POL( QSA_IN_GA(x1) ) = 2x1 + 1
POL( PC_IN_GGGAAAAA(x1, ..., x3) ) = 2x2
POL( PP_IN_GGAAGAAA(x1, ..., x3) ) = 2x3 + 1
POL( PQ_IN_GGAGAGA(x1, ..., x4) ) = 2x1 + 1
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
PC_IN_GGGAAAAA(T71, T73, T72) → U15_GGGAAAAA(T71, T73, T72, lessG_in_gg(T71, T73))
U15_GGGAAAAA(T71, T73, T72, lessG_out_gg(T71, T73)) → PP_IN_GGAAGAAA(T72, T73, T71)
PP_IN_GGAAGAAA(T72, T73, T71) → U17_GGAAGAAA(T72, T73, T71, splitH_in_ggaa(T72, T73))
U17_GGAAGAAA(T72, T73, T71, splitH_out_ggaa(T72, T73, T93, T94)) → PQ_IN_GGAGAGA(T71, T93, T94, T73)
PQ_IN_GGAGAGA(T71, T93, T94, T73) → QSA_IN_GA(cons(T71, T93))
lessG_in_gg(0, s(T82)) → lessG_out_gg(0, s(T82))
lessG_in_gg(s(T87), s(T88)) → U5_gg(T87, T88, lessG_in_gg(T87, T88))
splitH_in_ggaa([], T101) → splitH_out_ggaa([], T101, [], [])
splitH_in_ggaa(cons(T114, T115), T116) → U6_ggaa(T114, T115, T116, pI_in_gggaa(T114, T116, T115))
splitH_in_ggaa(cons(T129, T130), T131) → U7_ggaa(T129, T130, T131, pJ_in_gggaa(T129, T131, T130))
U5_gg(T87, T88, lessG_out_gg(T87, T88)) → lessG_out_gg(s(T87), s(T88))
U6_ggaa(T114, T115, T116, pI_out_gggaa(T114, T116, T115, X145, X146)) → splitH_out_ggaa(cons(T114, T115), T116, cons(T114, X145), X146)
U7_ggaa(T129, T130, T131, pJ_out_gggaa(T129, T131, T130, X172, X173)) → splitH_out_ggaa(cons(T129, T130), T131, X172, cons(T129, X173))
pI_in_gggaa(T114, T116, T115) → U21_gggaa(T114, T116, T115, lessG_in_gg(T114, T116))
pJ_in_gggaa(T129, T131, T130) → U23_gggaa(T129, T131, T130, geqK_in_gg(T129, T131))
U21_gggaa(T114, T116, T115, lessG_out_gg(T114, T116)) → U22_gggaa(T114, T116, T115, splitH_in_ggaa(T115, T116))
U23_gggaa(T129, T131, T130, geqK_out_gg(T129, T131)) → U24_gggaa(T129, T131, T130, splitH_in_ggaa(T130, T131))
U22_gggaa(T114, T116, T115, splitH_out_ggaa(T115, T116, X145, X146)) → pI_out_gggaa(T114, T116, T115, X145, X146)
geqK_in_gg(T140, T140) → geqK_out_gg(T140, T140)
geqK_in_gg(s(T145), 0) → geqK_out_gg(s(T145), 0)
geqK_in_gg(s(T150), s(T151)) → U8_gg(T150, T151, geqK_in_gg(T150, T151))
U24_gggaa(T129, T131, T130, splitH_out_ggaa(T130, T131, X172, X173)) → pJ_out_gggaa(T129, T131, T130, X172, X173)
U8_gg(T150, T151, geqK_out_gg(T150, T151)) → geqK_out_gg(s(T150), s(T151))
lessG_in_gg(x0, x1)
splitH_in_ggaa(x0, x1)
U5_gg(x0, x1, x2)
U6_ggaa(x0, x1, x2, x3)
U7_ggaa(x0, x1, x2, x3)
pI_in_gggaa(x0, x1, x2)
pJ_in_gggaa(x0, x1, x2)
U21_gggaa(x0, x1, x2, x3)
U23_gggaa(x0, x1, x2, x3)
U22_gggaa(x0, x1, x2, x3)
geqK_in_gg(x0, x1)
U24_gggaa(x0, x1, x2, x3)
U8_gg(x0, x1, x2)