0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔)
↳11 PiDP
↳12 PiDPToQDPProof (⇐)
↳13 QDP
↳14 NonTerminationProof (⇔)
↳15 FALSE
↳16 PiDP
↳17 UsableRulesProof (⇔)
↳18 PiDP
↳19 PiDPToQDPProof (⇐)
↳20 QDP
↳21 NonTerminationProof (⇔)
↳22 FALSE
↳23 PiDP
↳24 UsableRulesProof (⇔)
↳25 PiDP
↳26 PiDPToQDPProof (⇐)
↳27 QDP
↳28 QDPSizeChangeProof (⇔)
↳29 TRUE
↳30 PiDP
↳31 UsableRulesProof (⇔)
↳32 PiDP
↳33 PiDPToQDPProof (⇔)
↳34 QDP
↳35 QDPSizeChangeProof (⇔)
↳36 TRUE
↳37 PiDP
↳38 UsableRulesProof (⇔)
↳39 PiDP
↳40 PiDPToQDPProof (⇐)
↳41 QDP
↳42 QDPSizeChangeProof (⇔)
↳43 TRUE
↳44 PrologToPiTRSProof (⇐)
↳45 PiTRS
↳46 DependencyPairsProof (⇔)
↳47 PiDP
↳48 DependencyGraphProof (⇔)
↳49 AND
↳50 PiDP
↳51 UsableRulesProof (⇔)
↳52 PiDP
↳53 PiDPToQDPProof (⇐)
↳54 QDP
↳55 NonTerminationProof (⇔)
↳56 FALSE
↳57 PiDP
↳58 UsableRulesProof (⇔)
↳59 PiDP
↳60 PiDPToQDPProof (⇐)
↳61 QDP
↳62 NonTerminationProof (⇔)
↳63 FALSE
↳64 PiDP
↳65 UsableRulesProof (⇔)
↳66 PiDP
↳67 PiDPToQDPProof (⇐)
↳68 QDP
↳69 QDPSizeChangeProof (⇔)
↳70 TRUE
↳71 PiDP
↳72 UsableRulesProof (⇔)
↳73 PiDP
↳74 PiDPToQDPProof (⇔)
↳75 QDP
↳76 QDPSizeChangeProof (⇔)
↳77 TRUE
↳78 PiDP
↳79 UsableRulesProof (⇔)
↳80 PiDP
↳81 PiDPToQDPProof (⇐)
↳82 QDP
↳83 QDPSizeChangeProof (⇔)
↳84 TRUE
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
GOAL1_IN_G(T5) → U10_G(T5, s2t4_in_ga(T5, X15))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, X15)
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → U1_GA(T8, X34, X35, s2t4_in_ga(T8, X34))
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → S2T4_IN_GA(T8, X34)
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → U2_GA(T10, X48, X49, s2t4_in_ga(T10, X49))
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → S2T4_IN_GA(T10, X49)
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → U3_GA(T12, X62, X63, s2t4_in_ga(T12, X62))
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → S2T4_IN_GA(T12, X62)
GOAL1_IN_G(T5) → U11_G(T5, s2t4_in_gg(T5, nil))
GOAL1_IN_G(T5) → S2T4_IN_GG(T5, nil)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → U1_GG(T8, X34, X35, s2t4_in_gg(T8, X34))
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → U2_GG(T10, X48, X49, s2t4_in_gg(T10, X49))
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → U3_GG(T12, X62, X63, s2t4_in_gg(T12, X62))
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
U11_G(T5, s2t4_out_gg(T5, nil)) → U12_G(T5, tappend5_in_gaa(nil, X210, X211))
U11_G(T5, s2t4_out_gg(T5, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → U4_GAA(X210, X211, tappend5_in_gaa(nil, X210, X211))
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_GAA(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_GAA(T83, X210, X211)
TAPPEND5_IN_GAA(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_GAA(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → U7_GAA(X268, tappend5_in_gaa(nil, X265, X268))
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_GAA(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_GAA(T117, X265, X268)
TAPPEND5_IN_GAA(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_GAA(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U11_G(T5, s2t4_out_gg(T5, nil)) → U13_G(T5, tappend5_in_gaa(nil, X265, X268))
GOAL1_IN_G(T5) → U14_G(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(nil, T25, T26))
GOAL1_IN_G(T5) → U15_G(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
GOAL1_IN_G(T5) → U16_G(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(T51, T52, nil))
GOAL1_IN_G(T5) → U17_G(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
GOAL1_IN_G(T5) → U18_G(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(T83, T81, T82))
U18_G(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_G(T5, tappend5_in_aaa(T83, X210, X211))
U18_G(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA(nil, X210, node(X211, nil, nil)) → U4_AAA(X210, X211, tappend5_in_gaa(nil, X210, X211))
TAPPEND5_IN_AAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_AAA(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_AAA(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
TAPPEND5_IN_AAA(nil, nil, node(nil, nil, X268)) → U7_AAA(X268, tappend5_in_gaa(nil, X265, X268))
TAPPEND5_IN_AAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_AAA(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_AAA(T117, X265, X268)
TAPPEND5_IN_AAA(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_AAA(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
GOAL1_IN_G(T5) → U20_G(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_G(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_G(T5, tappend5_in_aaa(T99, X210, X211))
U20_G(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → TAPPEND5_IN_AAA(T99, X210, X211)
GOAL1_IN_G(T5) → U22_G(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_G(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_G(T5, tappend5_in_aaa(T117, X265, X268))
U22_G(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → TAPPEND5_IN_AAA(T117, X265, X268)
GOAL1_IN_G(T5) → U24_G(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_G(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_G(T5, tappend5_in_aaa(T133, X265, X268))
U24_G(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → TAPPEND5_IN_AAA(T133, X265, X268)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
GOAL1_IN_G(T5) → U10_G(T5, s2t4_in_ga(T5, X15))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, X15)
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → U1_GA(T8, X34, X35, s2t4_in_ga(T8, X34))
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → S2T4_IN_GA(T8, X34)
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → U2_GA(T10, X48, X49, s2t4_in_ga(T10, X49))
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → S2T4_IN_GA(T10, X49)
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → U3_GA(T12, X62, X63, s2t4_in_ga(T12, X62))
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → S2T4_IN_GA(T12, X62)
GOAL1_IN_G(T5) → U11_G(T5, s2t4_in_gg(T5, nil))
GOAL1_IN_G(T5) → S2T4_IN_GG(T5, nil)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → U1_GG(T8, X34, X35, s2t4_in_gg(T8, X34))
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → U2_GG(T10, X48, X49, s2t4_in_gg(T10, X49))
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → U3_GG(T12, X62, X63, s2t4_in_gg(T12, X62))
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
U11_G(T5, s2t4_out_gg(T5, nil)) → U12_G(T5, tappend5_in_gaa(nil, X210, X211))
U11_G(T5, s2t4_out_gg(T5, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → U4_GAA(X210, X211, tappend5_in_gaa(nil, X210, X211))
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_GAA(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_GAA(T83, X210, X211)
TAPPEND5_IN_GAA(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_GAA(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → U7_GAA(X268, tappend5_in_gaa(nil, X265, X268))
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_GAA(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_GAA(T117, X265, X268)
TAPPEND5_IN_GAA(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_GAA(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U11_G(T5, s2t4_out_gg(T5, nil)) → U13_G(T5, tappend5_in_gaa(nil, X265, X268))
GOAL1_IN_G(T5) → U14_G(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(nil, T25, T26))
GOAL1_IN_G(T5) → U15_G(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
GOAL1_IN_G(T5) → U16_G(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(T51, T52, nil))
GOAL1_IN_G(T5) → U17_G(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
GOAL1_IN_G(T5) → U18_G(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(T83, T81, T82))
U18_G(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_G(T5, tappend5_in_aaa(T83, X210, X211))
U18_G(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA(nil, X210, node(X211, nil, nil)) → U4_AAA(X210, X211, tappend5_in_gaa(nil, X210, X211))
TAPPEND5_IN_AAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_AAA(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_AAA(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
TAPPEND5_IN_AAA(nil, nil, node(nil, nil, X268)) → U7_AAA(X268, tappend5_in_gaa(nil, X265, X268))
TAPPEND5_IN_AAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_AAA(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_AAA(T117, X265, X268)
TAPPEND5_IN_AAA(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_AAA(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
GOAL1_IN_G(T5) → U20_G(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_G(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_G(T5, tappend5_in_aaa(T99, X210, X211))
U20_G(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → TAPPEND5_IN_AAA(T99, X210, X211)
GOAL1_IN_G(T5) → U22_G(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_G(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_G(T5, tappend5_in_aaa(T117, X265, X268))
U22_G(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → TAPPEND5_IN_AAA(T117, X265, X268)
GOAL1_IN_G(T5) → U24_G(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_G(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_G(T5, tappend5_in_aaa(T133, X265, X268))
U24_G(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → TAPPEND5_IN_AAA(T133, X265, X268)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(nil) → TAPPEND5_IN_GAA(nil)
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_AAA(T117, X265, X268)
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_AAA(T83, X210, X211)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_AAA(T117, X265, X268)
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA → TAPPEND5_IN_AAA
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_GAA(T117, X265, X268)
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_GAA(T83, X210, X211)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_GAA(T117, X265, X268)
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_GAA(T83, X210, X211)
TAPPEND5_IN_GAA(node(T114, T115, T117)) → TAPPEND5_IN_GAA(T117)
TAPPEND5_IN_GAA(node(T83, T81, T82)) → TAPPEND5_IN_GAA(T83)
From the DPs we obtained the following set of size-change graphs:
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
From the DPs we obtained the following set of size-change graphs:
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → S2T4_IN_GA(T10, X49)
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → S2T4_IN_GA(T8, X34)
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → S2T4_IN_GA(T12, X62)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → S2T4_IN_GA(T10, X49)
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → S2T4_IN_GA(T8, X34)
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → S2T4_IN_GA(T12, X62)
S2T4_IN_GA(s(T10)) → S2T4_IN_GA(T10)
From the DPs we obtained the following set of size-change graphs:
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
GOAL1_IN_G(T5) → U10_G(T5, s2t4_in_ga(T5, X15))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, X15)
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → U1_GA(T8, X34, X35, s2t4_in_ga(T8, X34))
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → S2T4_IN_GA(T8, X34)
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → U2_GA(T10, X48, X49, s2t4_in_ga(T10, X49))
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → S2T4_IN_GA(T10, X49)
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → U3_GA(T12, X62, X63, s2t4_in_ga(T12, X62))
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → S2T4_IN_GA(T12, X62)
GOAL1_IN_G(T5) → U11_G(T5, s2t4_in_gg(T5, nil))
GOAL1_IN_G(T5) → S2T4_IN_GG(T5, nil)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → U1_GG(T8, X34, X35, s2t4_in_gg(T8, X34))
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → U2_GG(T10, X48, X49, s2t4_in_gg(T10, X49))
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → U3_GG(T12, X62, X63, s2t4_in_gg(T12, X62))
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
U11_G(T5, s2t4_out_gg(T5, nil)) → U12_G(T5, tappend5_in_gaa(nil, X210, X211))
U11_G(T5, s2t4_out_gg(T5, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → U4_GAA(X210, X211, tappend5_in_gaa(nil, X210, X211))
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_GAA(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_GAA(T83, X210, X211)
TAPPEND5_IN_GAA(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_GAA(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → U7_GAA(X268, tappend5_in_gaa(nil, X265, X268))
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_GAA(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_GAA(T117, X265, X268)
TAPPEND5_IN_GAA(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_GAA(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U11_G(T5, s2t4_out_gg(T5, nil)) → U13_G(T5, tappend5_in_gaa(nil, X265, X268))
GOAL1_IN_G(T5) → U14_G(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(nil, T25, T26))
GOAL1_IN_G(T5) → U15_G(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
GOAL1_IN_G(T5) → U16_G(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(T51, T52, nil))
GOAL1_IN_G(T5) → U17_G(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
GOAL1_IN_G(T5) → U18_G(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(T83, T81, T82))
U18_G(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_G(T5, tappend5_in_aaa(T83, X210, X211))
U18_G(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA(nil, X210, node(X211, nil, nil)) → U4_AAA(X210, X211, tappend5_in_gaa(nil, X210, X211))
TAPPEND5_IN_AAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_AAA(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_AAA(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
TAPPEND5_IN_AAA(nil, nil, node(nil, nil, X268)) → U7_AAA(X268, tappend5_in_gaa(nil, X265, X268))
TAPPEND5_IN_AAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_AAA(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_AAA(T117, X265, X268)
TAPPEND5_IN_AAA(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_AAA(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
GOAL1_IN_G(T5) → U20_G(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_G(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_G(T5, tappend5_in_aaa(T99, X210, X211))
U20_G(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → TAPPEND5_IN_AAA(T99, X210, X211)
GOAL1_IN_G(T5) → U22_G(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_G(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_G(T5, tappend5_in_aaa(T117, X265, X268))
U22_G(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → TAPPEND5_IN_AAA(T117, X265, X268)
GOAL1_IN_G(T5) → U24_G(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_G(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_G(T5, tappend5_in_aaa(T133, X265, X268))
U24_G(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → TAPPEND5_IN_AAA(T133, X265, X268)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
GOAL1_IN_G(T5) → U10_G(T5, s2t4_in_ga(T5, X15))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, X15)
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → U1_GA(T8, X34, X35, s2t4_in_ga(T8, X34))
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → S2T4_IN_GA(T8, X34)
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → U2_GA(T10, X48, X49, s2t4_in_ga(T10, X49))
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → S2T4_IN_GA(T10, X49)
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → U3_GA(T12, X62, X63, s2t4_in_ga(T12, X62))
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → S2T4_IN_GA(T12, X62)
GOAL1_IN_G(T5) → U11_G(T5, s2t4_in_gg(T5, nil))
GOAL1_IN_G(T5) → S2T4_IN_GG(T5, nil)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → U1_GG(T8, X34, X35, s2t4_in_gg(T8, X34))
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → U2_GG(T10, X48, X49, s2t4_in_gg(T10, X49))
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → U3_GG(T12, X62, X63, s2t4_in_gg(T12, X62))
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
U11_G(T5, s2t4_out_gg(T5, nil)) → U12_G(T5, tappend5_in_gaa(nil, X210, X211))
U11_G(T5, s2t4_out_gg(T5, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → U4_GAA(X210, X211, tappend5_in_gaa(nil, X210, X211))
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_GAA(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_GAA(T83, X210, X211)
TAPPEND5_IN_GAA(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_GAA(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → U7_GAA(X268, tappend5_in_gaa(nil, X265, X268))
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_GAA(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_GAA(T117, X265, X268)
TAPPEND5_IN_GAA(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_GAA(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U11_G(T5, s2t4_out_gg(T5, nil)) → U13_G(T5, tappend5_in_gaa(nil, X265, X268))
GOAL1_IN_G(T5) → U14_G(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(nil, T25, T26))
GOAL1_IN_G(T5) → U15_G(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
GOAL1_IN_G(T5) → U16_G(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(T51, T52, nil))
GOAL1_IN_G(T5) → U17_G(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
GOAL1_IN_G(T5) → U18_G(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
GOAL1_IN_G(T5) → S2T4_IN_GA(T5, node(T83, T81, T82))
U18_G(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_G(T5, tappend5_in_aaa(T83, X210, X211))
U18_G(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA(nil, X210, node(X211, nil, nil)) → U4_AAA(X210, X211, tappend5_in_gaa(nil, X210, X211))
TAPPEND5_IN_AAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_AAA(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_AAA(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
TAPPEND5_IN_AAA(nil, nil, node(nil, nil, X268)) → U7_AAA(X268, tappend5_in_gaa(nil, X265, X268))
TAPPEND5_IN_AAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_AAA(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_AAA(T117, X265, X268)
TAPPEND5_IN_AAA(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_AAA(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
GOAL1_IN_G(T5) → U20_G(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_G(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_G(T5, tappend5_in_aaa(T99, X210, X211))
U20_G(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → TAPPEND5_IN_AAA(T99, X210, X211)
GOAL1_IN_G(T5) → U22_G(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_G(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_G(T5, tappend5_in_aaa(T117, X265, X268))
U22_G(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → TAPPEND5_IN_AAA(T117, X265, X268)
GOAL1_IN_G(T5) → U24_G(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_G(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_G(T5, tappend5_in_aaa(T133, X265, X268))
U24_G(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → TAPPEND5_IN_AAA(T133, X265, X268)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
TAPPEND5_IN_GAA(nil, nil, node(nil, nil, X268)) → TAPPEND5_IN_GAA(nil, X265, X268)
TAPPEND5_IN_GAA(nil, X210, node(X211, nil, nil)) → TAPPEND5_IN_GAA(nil, X210, X211)
TAPPEND5_IN_GAA(nil) → TAPPEND5_IN_GAA(nil)
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_AAA(T117, X265, X268)
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_AAA(T83, X210, X211)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
TAPPEND5_IN_AAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_AAA(T117, X265, X268)
TAPPEND5_IN_AAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_AAA(T83, X210, X211)
TAPPEND5_IN_AAA → TAPPEND5_IN_AAA
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_GAA(T117, X265, X268)
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_GAA(T83, X210, X211)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
TAPPEND5_IN_GAA(node(T114, T115, T117), T114, node(T114, T115, X268)) → TAPPEND5_IN_GAA(T117, X265, X268)
TAPPEND5_IN_GAA(node(T83, T81, T82), X210, node(X211, T81, T82)) → TAPPEND5_IN_GAA(T83, X210, X211)
TAPPEND5_IN_GAA(node(T114, T115, T117)) → TAPPEND5_IN_GAA(T117)
TAPPEND5_IN_GAA(node(T83, T81, T82)) → TAPPEND5_IN_GAA(T83)
From the DPs we obtained the following set of size-change graphs:
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
S2T4_IN_GG(s(T10), node(nil, X48, X49)) → S2T4_IN_GG(T10, X49)
S2T4_IN_GG(s(T8), node(X34, X35, X34)) → S2T4_IN_GG(T8, X34)
S2T4_IN_GG(s(T12), node(X62, X63, nil)) → S2T4_IN_GG(T12, X62)
From the DPs we obtained the following set of size-change graphs:
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → S2T4_IN_GA(T10, X49)
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → S2T4_IN_GA(T8, X34)
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → S2T4_IN_GA(T12, X62)
goal1_in_g(T5) → U10_g(T5, s2t4_in_ga(T5, X15))
s2t4_in_ga(0, nil) → s2t4_out_ga(0, nil)
s2t4_in_ga(s(T8), node(X34, X35, X34)) → U1_ga(T8, X34, X35, s2t4_in_ga(T8, X34))
s2t4_in_ga(s(T10), node(nil, X48, X49)) → U2_ga(T10, X48, X49, s2t4_in_ga(T10, X49))
s2t4_in_ga(s(T12), node(X62, X63, nil)) → U3_ga(T12, X62, X63, s2t4_in_ga(T12, X62))
s2t4_in_ga(T13, node(nil, X70, nil)) → s2t4_out_ga(T13, node(nil, X70, nil))
U3_ga(T12, X62, X63, s2t4_out_ga(T12, X62)) → s2t4_out_ga(s(T12), node(X62, X63, nil))
U2_ga(T10, X48, X49, s2t4_out_ga(T10, X49)) → s2t4_out_ga(s(T10), node(nil, X48, X49))
U1_ga(T8, X34, X35, s2t4_out_ga(T8, X34)) → s2t4_out_ga(s(T8), node(X34, X35, X34))
U10_g(T5, s2t4_out_ga(T5, X15)) → goal1_out_g(T5)
goal1_in_g(T5) → U11_g(T5, s2t4_in_gg(T5, nil))
s2t4_in_gg(0, nil) → s2t4_out_gg(0, nil)
s2t4_in_gg(s(T8), node(X34, X35, X34)) → U1_gg(T8, X34, X35, s2t4_in_gg(T8, X34))
s2t4_in_gg(s(T10), node(nil, X48, X49)) → U2_gg(T10, X48, X49, s2t4_in_gg(T10, X49))
s2t4_in_gg(s(T12), node(X62, X63, nil)) → U3_gg(T12, X62, X63, s2t4_in_gg(T12, X62))
s2t4_in_gg(T13, node(nil, X70, nil)) → s2t4_out_gg(T13, node(nil, X70, nil))
U3_gg(T12, X62, X63, s2t4_out_gg(T12, X62)) → s2t4_out_gg(s(T12), node(X62, X63, nil))
U2_gg(T10, X48, X49, s2t4_out_gg(T10, X49)) → s2t4_out_gg(s(T10), node(nil, X48, X49))
U1_gg(T8, X34, X35, s2t4_out_gg(T8, X34)) → s2t4_out_gg(s(T8), node(X34, X35, X34))
U11_g(T5, s2t4_out_gg(T5, nil)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U12_g(T5, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(nil, X79, X79) → tappend5_out_gaa(nil, X79, X79)
tappend5_in_gaa(nil, X92, node(X92, nil, nil)) → tappend5_out_gaa(nil, X92, node(X92, nil, nil))
tappend5_in_gaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_gaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_gaa(nil, X149, node(nil, nil, X149)) → tappend5_out_gaa(nil, X149, node(nil, nil, X149))
tappend5_in_gaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_gaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_gaa(nil, X210, node(X211, nil, nil)) → U4_gaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
tappend5_in_gaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_gaa(T83, T81, T82, X210, X211, tappend5_in_gaa(T83, X210, X211))
tappend5_in_gaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_gaa(T99, T97, T98, X210, X211, tappend5_in_gaa(T99, X210, X211))
tappend5_in_gaa(nil, nil, node(nil, nil, X268)) → U7_gaa(X268, tappend5_in_gaa(nil, X265, X268))
tappend5_in_gaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_gaa(T114, T115, T117, X268, tappend5_in_gaa(T117, X265, X268))
tappend5_in_gaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_gaa(T130, T131, T133, X268, tappend5_in_gaa(T133, X265, X268))
U9_gaa(T130, T131, T133, X268, tappend5_out_gaa(T133, X265, X268)) → tappend5_out_gaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_gaa(T114, T115, T117, X268, tappend5_out_gaa(T117, X265, X268)) → tappend5_out_gaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U7_gaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_gaa(nil, nil, node(nil, nil, X268))
U6_gaa(T99, T97, T98, X210, X211, tappend5_out_gaa(T99, X210, X211)) → tappend5_out_gaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_gaa(T83, T81, T82, X210, X211, tappend5_out_gaa(T83, X210, X211)) → tappend5_out_gaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U4_gaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_gaa(nil, X210, node(X211, nil, nil))
U12_g(T5, tappend5_out_gaa(nil, X210, X211)) → goal1_out_g(T5)
U11_g(T5, s2t4_out_gg(T5, nil)) → U13_g(T5, tappend5_in_gaa(nil, X265, X268))
U13_g(T5, tappend5_out_gaa(nil, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U14_g(T5, s2t4_in_ga(T5, node(nil, T25, T26)))
U14_g(T5, s2t4_out_ga(T5, node(nil, T25, T26))) → goal1_out_g(T5)
goal1_in_g(T5) → U15_g(T5, s2t4_in_ga(T5, node(nil, T36, T37)))
U15_g(T5, s2t4_out_ga(T5, node(nil, T36, T37))) → goal1_out_g(T5)
goal1_in_g(T5) → U16_g(T5, s2t4_in_ga(T5, node(T51, T52, nil)))
U16_g(T5, s2t4_out_ga(T5, node(T51, T52, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U17_g(T5, s2t4_in_ga(T5, node(T64, T65, nil)))
U17_g(T5, s2t4_out_ga(T5, node(T64, T65, nil))) → goal1_out_g(T5)
goal1_in_g(T5) → U18_g(T5, s2t4_in_ga(T5, node(T83, T81, T82)))
U18_g(T5, s2t4_out_ga(T5, node(T83, T81, T82))) → U19_g(T5, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(nil, X79, X79) → tappend5_out_aaa(nil, X79, X79)
tappend5_in_aaa(nil, X92, node(X92, nil, nil)) → tappend5_out_aaa(nil, X92, node(X92, nil, nil))
tappend5_in_aaa(node(nil, T25, T26), X92, node(X92, T25, T26)) → tappend5_out_aaa(node(nil, T25, T26), X92, node(X92, T25, T26))
tappend5_in_aaa(nil, X149, node(nil, nil, X149)) → tappend5_out_aaa(nil, X149, node(nil, nil, X149))
tappend5_in_aaa(node(T51, T52, nil), X149, node(T51, T52, X149)) → tappend5_out_aaa(node(T51, T52, nil), X149, node(T51, T52, X149))
tappend5_in_aaa(nil, X210, node(X211, nil, nil)) → U4_aaa(X210, X211, tappend5_in_gaa(nil, X210, X211))
U4_aaa(X210, X211, tappend5_out_gaa(nil, X210, X211)) → tappend5_out_aaa(nil, X210, node(X211, nil, nil))
tappend5_in_aaa(node(T83, T81, T82), X210, node(X211, T81, T82)) → U5_aaa(T83, T81, T82, X210, X211, tappend5_in_aaa(T83, X210, X211))
tappend5_in_aaa(node(T99, T97, T98), X210, node(X211, T97, T98)) → U6_aaa(T99, T97, T98, X210, X211, tappend5_in_aaa(T99, X210, X211))
tappend5_in_aaa(nil, nil, node(nil, nil, X268)) → U7_aaa(X268, tappend5_in_gaa(nil, X265, X268))
U7_aaa(X268, tappend5_out_gaa(nil, X265, X268)) → tappend5_out_aaa(nil, nil, node(nil, nil, X268))
tappend5_in_aaa(node(T114, T115, T117), T114, node(T114, T115, X268)) → U8_aaa(T114, T115, T117, X268, tappend5_in_aaa(T117, X265, X268))
tappend5_in_aaa(node(T130, T131, T133), T130, node(T130, T131, X268)) → U9_aaa(T130, T131, T133, X268, tappend5_in_aaa(T133, X265, X268))
U9_aaa(T130, T131, T133, X268, tappend5_out_aaa(T133, X265, X268)) → tappend5_out_aaa(node(T130, T131, T133), T130, node(T130, T131, X268))
U8_aaa(T114, T115, T117, X268, tappend5_out_aaa(T117, X265, X268)) → tappend5_out_aaa(node(T114, T115, T117), T114, node(T114, T115, X268))
U6_aaa(T99, T97, T98, X210, X211, tappend5_out_aaa(T99, X210, X211)) → tappend5_out_aaa(node(T99, T97, T98), X210, node(X211, T97, T98))
U5_aaa(T83, T81, T82, X210, X211, tappend5_out_aaa(T83, X210, X211)) → tappend5_out_aaa(node(T83, T81, T82), X210, node(X211, T81, T82))
U19_g(T5, tappend5_out_aaa(T83, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U20_g(T5, s2t4_in_ga(T5, node(T99, T97, T98)))
U20_g(T5, s2t4_out_ga(T5, node(T99, T97, T98))) → U21_g(T5, tappend5_in_aaa(T99, X210, X211))
U21_g(T5, tappend5_out_aaa(T99, X210, X211)) → goal1_out_g(T5)
goal1_in_g(T5) → U22_g(T5, s2t4_in_ga(T5, node(T114, T115, T117)))
U22_g(T5, s2t4_out_ga(T5, node(T114, T115, T117))) → U23_g(T5, tappend5_in_aaa(T117, X265, X268))
U23_g(T5, tappend5_out_aaa(T117, X265, X268)) → goal1_out_g(T5)
goal1_in_g(T5) → U24_g(T5, s2t4_in_ga(T5, node(T130, T131, T133)))
U24_g(T5, s2t4_out_ga(T5, node(T130, T131, T133))) → U25_g(T5, tappend5_in_aaa(T133, X265, X268))
U25_g(T5, tappend5_out_aaa(T133, X265, X268)) → goal1_out_g(T5)
S2T4_IN_GA(s(T10), node(nil, X48, X49)) → S2T4_IN_GA(T10, X49)
S2T4_IN_GA(s(T8), node(X34, X35, X34)) → S2T4_IN_GA(T8, X34)
S2T4_IN_GA(s(T12), node(X62, X63, nil)) → S2T4_IN_GA(T12, X62)
S2T4_IN_GA(s(T10)) → S2T4_IN_GA(T10)
From the DPs we obtained the following set of size-change graphs: