Left Termination proof of /tmp/tmpANgMOg/balance

Left Termination of the query pattern
balance(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 457 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 493 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 37 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

(0) Obligation:

Clauses:

balance(T, TB) :- balance(T, -(I, []), -(.(','(TB, -(I, [])), X), X), -(Rest, []), -(Rest, [])).
balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(NH, NT)) :- ','(balance(L, -(IH, .(V, IT1)), -(H, T), -(HR1, TR1), -(NH, NT1)), balance(R, -(IT1, IT), -(HR1, TR1), -(HR, TR), -(NT1, NT))).

Query: balance(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: balance(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: balance(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, []))\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 1 | balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="B: ','(balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), balance(T27, -(X108, []), -(X109, X110), -(X116, []), -(X111, [])))\n\nT25 is ground\nT26 is ground\nT27 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="G: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111))\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="E: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, []))\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 1 | balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 1\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="H: ','(balance(T142, -(T156, .(T143, X245)), -(.(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157), -(X246, X247), -(X252, X248)), balance(T144, -(X245, .(T146, X249)), -(X246, X247), -(X250, X251), -(X248, X253)))\n\nT142 is ground\nT143 is ground\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX252 is free\nX253 is free\nX245 is free\nX246 is free\nX247 is free\nX248 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: balance(T142, -(T156, .(T143, X245)), -(.(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157), -(X246, X247), -(X252, X248))\n\nT142 is ground\nT143 is ground\nX252 is free\nX245 is free\nX246 is free\nX247 is free\nX248 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="C: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253))\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 1 | balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 2\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 1\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 2\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="D: ','(balance(T291, -(T305, .(T292, X380)), -(T306, T307), -(X381, X382), -(T308, X383)), balance(T293, -(X380, .(T295, X384)), -(X381, X382), -(X385, X386), -(X383, X387)))\n\nT291 is ground\nT292 is ground\nT293 is ground\nT295 is ground\nX384 is free\nX385 is free\nX386 is free\nX387 is free\nX380 is free\nX381 is free\nX382 is free\nX383 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: balance(T291, -(T305, .(T292, X380)), -(T306, T307), -(X381, X382), -(T308, X383))\n\nT291 is ground\nT292 is ground\nX380 is free\nX381 is free\nX382 is free\nX383 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: balance(T293, -(T323, .(T295, X384)), -(T324, T325), -(X385, X386), -(T326, X387))\n\nT293 is ground\nT295 is ground\nX384 is free\nX385 is free\nX386 is free\nX387 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 1 | balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 1\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="F: ','(balance(T418, -(T432, .(T419, X508)), -(T433, T434), -(X509, X510), -(T435, X511)), balance(T420, -(X508, []), -(X509, X510), -(T436, []), -(X511, [])))\n\nT418 is ground\nT419 is ground\nT420 is ground\nX508 is free\nX509 is free\nX510 is free\nX511 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: balance(T418, -(T432, .(T419, X508)), -(T433, T434), -(X509, X510), -(T435, X511))\n\nT418 is ground\nT419 is ground\nX508 is free\nX509 is free\nX510 is free\nX511 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: balance(T420, -(T451, []), -(T452, T453), -(T455, []), -(T454, []))\n\nT420 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 116 [arrowhead = none ];
116 -> 6;

117 [label="ONLY EVAL with clause\nbalance(X3, X4) :- balance(X3, -(X5, []), -(.(','(X4, -(X5, [])), X6), X6), -(X7, []), -(X7, [])).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T7,\nX4 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 117 [arrowhead = none ];
117 -> 8;

118 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 118 [arrowhead = none ];
118 -> 9;

119 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 119 [arrowhead = none ];
119 -> 14;

120 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 120 [arrowhead = none ];
120 -> 15;

121 [label="EVAL with clause\nbalance(nil, -(X36, X36), -(X37, X38), -(X37, X38), -(.(','(nil, -(X39, X39)), X40), X40)).\nand substitutionT5 -> nil,\nX5 -> [],\nX36 -> [],\nX41 -> [],\nT7 -> nil,\nX6 -> [],\nX37 -> .(','(nil, -([], [])), []),\nX38 -> [],\nX7 -> .(','(nil, -([], [])), []),\nX42 -> [],\nT12 -> nil,\nX39 -> [],\nX40 -> []", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 121 [arrowhead = none ];
121 -> 19;

122 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 122 [arrowhead = none ];
122 -> 20;

123 [label="EVAL with clause\nbalance(tree(X91, X92, X93), -(X94, X95), -(.(','(tree(X96, X97, X98), -(X99, X100)), X101), .(','(X96, -(X99, .(X97, X102))), .(','(X98, -(X102, X100)), X103))), -(X104, X105), -(X106, X107)) :- ','(balance(X91, -(X94, .(X92, X108)), -(X101, X103), -(X109, X110), -(X106, X111)), balance(X93, -(X108, X95), -(X109, X110), -(X104, X105), -(X111, X107))).\nand substitutionX91 -> T25,\nX92 -> T26,\nX93 -> T27,\nT5 -> tree(T25, T26, T27),\nX5 -> T31,\nX94 -> T31,\nX95 -> [],\nX96 -> T33,\nX97 -> T34,\nX98 -> T36,\nT7 -> tree(T33, T34, T36),\nX99 -> T31,\nX100 -> [],\nX6 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX101 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX102 -> T35,\nX103 -> T32,\nX113 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX7 -> X116,\nX104 -> X116,\nX105 -> [],\nX106 -> X116,\nX107 -> [],\nX112 -> T31,\nX115 -> T32,\nT28 -> T33,\nT29 -> T34,\nX114 -> T35,\nT30 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 123 [arrowhead = none ];
123 -> 27;

124 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 124 [arrowhead = none ];
124 -> 33;

125 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 125 [arrowhead = none ];
125 -> 21;

126 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
27 -> 126 [arrowhead = none ];
126 -> 42;

127 [label="SPLIT 2\nnew knowledge:\nT25 is ground\nreplacements:X108 -> T53,\nX109 -> T54,\nX110 -> T55,\nX116 -> T56,\nX111 -> T57", fontsize=14, style = filled, fillcolor = violet];
27 -> 127 [arrowhead = none ];
127 -> 43;

128 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
42 -> 128 [arrowhead = none ];
128 -> 47;

129 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 129 [arrowhead = none ];
129 -> 93;

130 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
47 -> 130 [arrowhead = none ];
130 -> 48;

131 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
47 -> 131 [arrowhead = none ];
131 -> 49;

132 [label="EVAL with clause\nbalance(nil, -(X173, X173), -(X174, X175), -(X174, X175), -(.(','(nil, -(X176, X176)), X177), X177)).\nand substitutionT25 -> nil,\nT31 -> .(T107, T108),\nX173 -> .(T107, T108),\nT26 -> T107,\nX108 -> T108,\nT106 -> .(T107, T108),\nT33 -> T109,\nT34 -> T110,\nT35 -> T111,\nT36 -> T112,\nT32 -> T113,\nX174 -> .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)),\nX175 -> T113,\nX109 -> .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)),\nX110 -> T113,\nX176 -> X178,\nX177 -> X179,\nX116 -> .(','(nil, -(X178, X178)), X179),\nX111 -> X179", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 132 [arrowhead = none ];
132 -> 54;

133 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 133 [arrowhead = none ];
133 -> 55;

134 [label="EVAL with clause\nbalance(tree(X228, X229, X230), -(X231, X232), -(.(','(tree(X233, X234, X235), -(X236, X237)), X238), .(','(X233, -(X236, .(X234, X239))), .(','(X235, -(X239, X237)), X240))), -(X241, X242), -(X243, X244)) :- ','(balance(X228, -(X231, .(X229, X245)), -(X238, X240), -(X246, X247), -(X243, X248)), balance(X230, -(X245, X232), -(X246, X247), -(X241, X242), -(X248, X244))).\nand substitutionX228 -> T142,\nX229 -> T143,\nX230 -> T144,\nT25 -> tree(T142, T143, T144),\nT31 -> T156,\nX231 -> T156,\nT26 -> T146,\nX108 -> X249,\nX232 -> .(T146, X249),\nX233 -> T160,\nX234 -> T161,\nX235 -> T163,\nT33 -> tree(T160, T161, T163),\nX236 -> T156,\nT34 -> T164,\nT35 -> T159,\nX237 -> .(T164, T159),\nT36 -> T158,\nT32 -> .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)),\nX238 -> .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))),\nX239 -> T162,\nX240 -> T157,\nT153 -> .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)),\nX109 -> X250,\nX241 -> X250,\nX110 -> X251,\nX242 -> X251,\nX116 -> X252,\nX243 -> X252,\nX111 -> X253,\nX244 -> X253,\nT145 -> T156,\nT155 -> T157,\nT152 -> T158,\nT151 -> T159,\nT147 -> T160,\nT148 -> T161,\nT154 -> T162,\nT149 -> T163,\nT150 -> T164", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 134 [arrowhead = none ];
134 -> 63;

135 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 135 [arrowhead = none ];
135 -> 64;

136 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 136 [arrowhead = none ];
136 -> 56;

137 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
63 -> 137 [arrowhead = none ];
137 -> 67;

138 [label="SPLIT 2\nnew knowledge:\nT142 is ground\nreplacements:X245 -> T187,\nX246 -> T188,\nX247 -> T189,\nX252 -> T190,\nX248 -> T191", fontsize=14, style = filled, fillcolor = violet];
63 -> 138 [arrowhead = none ];
138 -> 68;

139 [label="INSTANCE with matching:\nT144 -> T142\nT187 -> T156\nT146 -> T143\nX249 -> X245\nT188 -> .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)))\nT189 -> T157\nX250 -> X246\nX251 -> X247\nT191 -> X252\nX253 -> X248", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 139 [arrowhead = none , style=dashed];
139 -> 68[style=dashed];

140 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 140 [arrowhead = none ];
140 -> 72;

141 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
72 -> 141 [arrowhead = none ];
141 -> 73;

142 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
72 -> 142 [arrowhead = none ];
142 -> 74;

143 [label="EVAL with clause\nbalance(nil, -(X312, X312), -(X313, X314), -(X313, X314), -(.(','(nil, -(X315, X315)), X316), X316)).\nand substitutionT144 -> nil,\nT187 -> .(T257, T258),\nX312 -> .(T257, T258),\nT146 -> T257,\nX249 -> T258,\nT256 -> .(T257, T258),\nT188 -> T259,\nX313 -> T259,\nT189 -> T260,\nX314 -> T260,\nX250 -> T259,\nX251 -> T260,\nX315 -> T261,\nX316 -> T262,\nT191 -> .(','(nil, -(T261, T261)), T262),\nX253 -> T262", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 143 [arrowhead = none ];
143 -> 77;

144 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 144 [arrowhead = none ];
144 -> 78;

145 [label="EVAL with clause\nbalance(tree(X363, X364, X365), -(X366, X367), -(.(','(tree(X368, X369, X370), -(X371, X372)), X373), .(','(X368, -(X371, .(X369, X374))), .(','(X370, -(X374, X372)), X375))), -(X376, X377), -(X378, X379)) :- ','(balance(X363, -(X366, .(X364, X380)), -(X373, X375), -(X381, X382), -(X378, X383)), balance(X365, -(X380, X367), -(X381, X382), -(X376, X377), -(X383, X379))).\nand substitutionX363 -> T291,\nX364 -> T292,\nX365 -> T293,\nT144 -> tree(T291, T292, T293),\nT187 -> T305,\nX366 -> T305,\nT146 -> T295,\nX249 -> X384,\nX367 -> .(T295, X384),\nX368 -> T296,\nX369 -> T297,\nX370 -> T298,\nX371 -> T299,\nX372 -> T300,\nX373 -> T306,\nT188 -> .(','(tree(T296, T297, T298), -(T299, T300)), T306),\nX374 -> T302,\nX375 -> T307,\nT189 -> .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)),\nX250 -> X385,\nX376 -> X385,\nX251 -> X386,\nX377 -> X386,\nT191 -> T308,\nX378 -> T308,\nX253 -> X387,\nX379 -> X387,\nT294 -> T305,\nT301 -> T306,\nT303 -> T307,\nT304 -> T308", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 145 [arrowhead = none ];
145 -> 86;

146 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 146 [arrowhead = none ];
146 -> 87;

147 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 147 [arrowhead = none ];
147 -> 79;

148 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
86 -> 148 [arrowhead = none ];
148 -> 88;

149 [label="SPLIT 2\nnew knowledge:\nT291 is ground\nreplacements:X380 -> T323,\nX381 -> T324,\nX382 -> T325,\nX383 -> T326", fontsize=14, style = filled, fillcolor = violet];
86 -> 149 [arrowhead = none ];
149 -> 89;

150 [label="INSTANCE with matching:\nT144 -> T291\nT187 -> T305\nT146 -> T292\nX249 -> X380\nT188 -> T306\nT189 -> T307\nX250 -> X381\nX251 -> X382\nT191 -> T308\nX253 -> X383", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 150 [arrowhead = none , style=dashed];
150 -> 68[style=dashed];

151 [label="INSTANCE with matching:\nT144 -> T293\nT187 -> T323\nT146 -> T295\nX249 -> X384\nT188 -> T324\nT189 -> T325\nX250 -> X385\nX251 -> X386\nT191 -> T326\nX253 -> X387", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 151 [arrowhead = none , style=dashed];
151 -> 68[style=dashed];

152 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
93 -> 152 [arrowhead = none ];
152 -> 97;

153 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
93 -> 153 [arrowhead = none ];
153 -> 98;

154 [label="EVAL with clause\nbalance(nil, -(X448, X448), -(X449, X450), -(X449, X450), -(.(','(nil, -(X451, X451)), X452), X452)).\nand substitutionT27 -> nil,\nT53 -> [],\nX448 -> [],\nT385 -> [],\nT54 -> T386,\nX449 -> T386,\nT55 -> [],\nX450 -> [],\nT56 -> T386,\nT387 -> [],\nX451 -> T388,\nX452 -> [],\nT57 -> .(','(nil, -(T388, T388)), []),\nT389 -> []", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 154 [arrowhead = none ];
154 -> 102;

155 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 155 [arrowhead = none ];
155 -> 103;

156 [label="EVAL with clause\nbalance(tree(X491, X492, X493), -(X494, X495), -(.(','(tree(X496, X497, X498), -(X499, X500)), X501), .(','(X496, -(X499, .(X497, X502))), .(','(X498, -(X502, X500)), X503))), -(X504, X505), -(X506, X507)) :- ','(balance(X491, -(X494, .(X492, X508)), -(X501, X503), -(X509, X510), -(X506, X511)), balance(X493, -(X508, X495), -(X509, X510), -(X504, X505), -(X511, X507))).\nand substitutionX491 -> T418,\nX492 -> T419,\nX493 -> T420,\nT27 -> tree(T418, T419, T420),\nT53 -> T432,\nX494 -> T432,\nX495 -> [],\nX496 -> T422,\nX497 -> T423,\nX498 -> T424,\nX499 -> T425,\nX500 -> T426,\nX501 -> T433,\nT54 -> .(','(tree(T422, T423, T424), -(T425, T426)), T433),\nX502 -> T428,\nX503 -> T434,\nT55 -> .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)),\nT56 -> T436,\nX504 -> T436,\nX505 -> [],\nT57 -> T435,\nX506 -> T435,\nX507 -> [],\nT421 -> T432,\nT427 -> T433,\nT429 -> T434,\nT431 -> T435,\nT430 -> T436", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 156 [arrowhead = none ];
156 -> 110;

157 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 157 [arrowhead = none ];
157 -> 111;

158 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 158 [arrowhead = none ];
158 -> 104;

159 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
110 -> 159 [arrowhead = none ];
159 -> 114;

160 [label="SPLIT 2\nnew knowledge:\nT418 is ground\nreplacements:X508 -> T451,\nX509 -> T452,\nX510 -> T453,\nX511 -> T454,\nT436 -> T455", fontsize=14, style = filled, fillcolor = violet];
110 -> 160 [arrowhead = none ];
160 -> 115;

161 [label="INSTANCE with matching:\nT144 -> T418\nT187 -> T432\nT146 -> T419\nX249 -> X508\nT188 -> T433\nT189 -> T434\nX250 -> X509\nX251 -> X510\nT191 -> T435\nX253 -> X511", fontsize=14, style = filled, fillcolor = lightgrey];
114 -> 161 [arrowhead = none , style=dashed];
161 -> 68[style=dashed];

162 [label="INSTANCE with matching:\nT27 -> T420\nT53 -> T451\nT54 -> T452\nT55 -> T453\nT56 -> T455\nT57 -> T454", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 162 [arrowhead = none , style=dashed];
162 -> 43[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U1_ga(T25, T26, T27, T33, T34, T36, pB_in_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27))
pB_in_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
balanceG_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceG_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceG_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253))
pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
balanceC_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceC_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
pD_in_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → pD_out_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_out_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253)
U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253)) → balanceG_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceE_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceE_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceE_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_in_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436))
pF_in_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → pF_out_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455)
U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_out_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)) → balanceE_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → pB_out_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27)
U1_ga(T25, T26, T27, T33, T34, T36, pB_out_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27)) → balanceA_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

BALANCEA_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U1_GA(T25, T26, T27, T33, T34, T36, pB_in_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27))
BALANCEA_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → PB_IN_GAGAAAAAAAAAAG(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27)
PB_IN_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → U5_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
PB_IN_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → BALANCEG_IN_GAGAAAAAAAAAA(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)
BALANCEG_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U4_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253))
BALANCEG_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → PH_IN_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253)
PH_IN_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → U7_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
PH_IN_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → BALANCEC_IN_GAGAAAAAAA(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)
BALANCEC_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
BALANCEC_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)
PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → BALANCEC_IN_GAGAAAAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)
U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCEC_IN_GAGAAAAAAA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)
U7_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U8_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U7_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → BALANCEC_IN_GAGAAAAAAA(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)
U5_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U6_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_in_gaaaaa(T27, T53, T54, T55, T56, T57))
U5_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → BALANCEE_IN_GAAAAA(T27, T53, T54, T55, T56, T57)
BALANCEE_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U3_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_in_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436))
BALANCEE_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → PF_IN_GAGAAAAAAAGA(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)
PF_IN_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
PF_IN_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → BALANCEC_IN_GAGAAAAAAA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)
U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U12_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCEE_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U1_ga(T25, T26, T27, T33, T34, T36, pB_in_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27))
pB_in_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
balanceG_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceG_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceG_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253))
pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
balanceC_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceC_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
pD_in_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → pD_out_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_out_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253)
U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253)) → balanceG_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceE_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceE_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceE_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_in_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436))
pF_in_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → pF_out_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455)
U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_out_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)) → balanceE_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → pB_out_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27)
U1_ga(T25, T26, T27, T33, T34, T36, pB_out_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27)) → balanceA_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

The argument filtering Pi contains the following mapping:
balanceA_in_ga(x1, x2) = balanceA_in_ga(x1)
nil = nil
balanceA_out_ga(x1, x2) = balanceA_out_ga(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4, x5, x6, x7) = U1_ga(x1, x2, x3, x7)
pB_in_gagaaaaaaaaaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) = pB_in_gagaaaaaaaaaag(x1, x3, x14)
U5_gagaaaaaaaaaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_gagaaaaaaaaaag(x1, x3, x14, x15)
balanceG_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balanceG_in_gagaaaaaaaaaa(x1, x3)
balanceG_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balanceG_out_gagaaaaaaaaaa(x1, x3)
U4_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U4_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
pH_in_gagaaaaaaaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22) = pH_in_gagaaaaaaaaaaaaaggaaaa(x1, x3, x17, x18)
U7_gagaaaaaaaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23) = U7_gagaaaaaaaaaaaaaggaaaa(x1, x3, x17, x18, x23)
balanceC_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceC_in_gagaaaaaaa(x1, x3)
balanceC_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceC_out_gagaaaaaaa(x1, x3)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x1, x2, x3, x5, x19)
pD_in_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = pD_in_gagaaaaaaaggaaaa(x1, x3, x11, x12)
U9_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U9_gagaaaaaaaggaaaa(x1, x3, x11, x12, x17)
U10_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U10_gagaaaaaaaggaaaa(x1, x3, x11, x12, x17)
pD_out_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = pD_out_gagaaaaaaaggaaaa(x1, x3, x11, x12)
U8_gagaaaaaaaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23) = U8_gagaaaaaaaaaaaaaggaaaa(x1, x3, x17, x18, x23)
pH_out_gagaaaaaaaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22) = pH_out_gagaaaaaaaaaaaaaggaaaa(x1, x3, x17, x18)
U6_gagaaaaaaaaaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_gagaaaaaaaaaag(x1, x3, x14, x15)
balanceE_in_gaaaaa(x1, x2, x3, x4, x5, x6) = balanceE_in_gaaaaa(x1)
balanceE_out_gaaaaa(x1, x2, x3, x4, x5, x6) = balanceE_out_gaaaaa(x1)
U3_gaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U3_gaaaaa(x1, x2, x3, x15)
pF_in_gagaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = pF_in_gagaaaaaaaga(x1, x3, x11)
U11_gagaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U11_gagaaaaaaaga(x1, x3, x11, x13)
U12_gagaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U12_gagaaaaaaaga(x1, x3, x11, x13)
pF_out_gagaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = pF_out_gagaaaaaaaga(x1, x3, x11)
pB_out_gagaaaaaaaaaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) = pB_out_gagaaaaaaaaaag(x1, x3, x14)
BALANCEA_IN_GA(x1, x2) = BALANCEA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6, x7) = U1_GA(x1, x2, x3, x7)
PB_IN_GAGAAAAAAAAAAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) = PB_IN_GAGAAAAAAAAAAG(x1, x3, x14)
U5_GAGAAAAAAAAAAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_GAGAAAAAAAAAAG(x1, x3, x14, x15)
BALANCEG_IN_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = BALANCEG_IN_GAGAAAAAAAAAA(x1, x3)
U4_GAGAAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U4_GAGAAAAAAAAAA(x1, x2, x3, x5, x19)
PH_IN_GAGAAAAAAAAAAAAAGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22) = PH_IN_GAGAAAAAAAAAAAAAGGAAAA(x1, x3, x17, x18)
U7_GAGAAAAAAAAAAAAAGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23) = U7_GAGAAAAAAAAAAAAAGGAAAA(x1, x3, x17, x18, x23)
BALANCEC_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCEC_IN_GAGAAAAAAA(x1, x3)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_GAGAAAAAAA(x1, x2, x3, x5, x19)
PD_IN_GAGAAAAAAAGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = PD_IN_GAGAAAAAAAGGAAAA(x1, x3, x11, x12)
U9_GAGAAAAAAAGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U9_GAGAAAAAAAGGAAAA(x1, x3, x11, x12, x17)
U10_GAGAAAAAAAGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U10_GAGAAAAAAAGGAAAA(x1, x3, x11, x12, x17)
U8_GAGAAAAAAAAAAAAAGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23) = U8_GAGAAAAAAAAAAAAAGGAAAA(x1, x3, x17, x18, x23)
U6_GAGAAAAAAAAAAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_GAGAAAAAAAAAAG(x1, x3, x14, x15)
BALANCEE_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = BALANCEE_IN_GAAAAA(x1)
U3_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U3_GAAAAA(x1, x2, x3, x15)
PF_IN_GAGAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = PF_IN_GAGAAAAAAAGA(x1, x3, x11)
U11_GAGAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U11_GAGAAAAAAAGA(x1, x3, x11, x13)
U12_GAGAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U12_GAGAAAAAAAGA(x1, x3, x11, x13)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEA_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U1_GA(T25, T26, T27, T33, T34, T36, pB_in_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27))
BALANCEA_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → PB_IN_GAGAAAAAAAAAAG(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27)
PB_IN_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → U5_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
PB_IN_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → BALANCEG_IN_GAGAAAAAAAAAA(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)
BALANCEG_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U4_GAGAAAAAAAAAA(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253))
BALANCEG_IN_GAGAAAAAAAAAA(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → PH_IN_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253)
PH_IN_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → U7_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
PH_IN_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → BALANCEC_IN_GAGAAAAAAA(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)
BALANCEC_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
BALANCEC_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)
PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → BALANCEC_IN_GAGAAAAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)
U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCEC_IN_GAGAAAAAAA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)
U7_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U8_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U7_GAGAAAAAAAAAAAAAGGAAAA(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → BALANCEC_IN_GAGAAAAAAA(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)
U5_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U6_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_in_gaaaaa(T27, T53, T54, T55, T56, T57))
U5_GAGAAAAAAAAAAG(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → BALANCEE_IN_GAAAAA(T27, T53, T54, T55, T56, T57)
BALANCEE_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U3_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_in_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436))
BALANCEE_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → PF_IN_GAGAAAAAAAGA(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)
PF_IN_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
PF_IN_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → BALANCEC_IN_GAGAAAAAAA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)
U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U12_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCEE_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U1_ga(T25, T26, T27, T33, T34, T36, pB_in_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27))
pB_in_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
balanceG_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceG_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceG_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253))
pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
balanceC_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceC_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
pD_in_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → pD_out_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_out_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253)
U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253)) → balanceG_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceE_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceE_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceE_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_in_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436))
pF_in_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → pF_out_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455)
U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_out_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)) → balanceE_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → pB_out_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27)
U1_ga(T25, T26, T27, T33, T34, T36, pB_out_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27)) → balanceA_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 17 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEC_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)
PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCEC_IN_GAGAAAAAAA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)
PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → BALANCEC_IN_GAGAAAAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)

The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U1_ga(T25, T26, T27, T33, T34, T36, pB_in_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27))
pB_in_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
balanceG_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceG_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceG_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253))
pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
balanceC_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceC_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
pD_in_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → pD_out_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_out_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253)
U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253)) → balanceG_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceE_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceE_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceE_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_in_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436))
pF_in_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → pF_out_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455)
U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_out_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)) → balanceE_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → pB_out_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27)
U1_ga(T25, T26, T27, T33, T34, T36, pB_out_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27)) → balanceA_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEC_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)
PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCEC_IN_GAGAAAAAAA(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)
PD_IN_GAGAAAAAAAGGAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → BALANCEC_IN_GAGAAAAAAA(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)

The TRS R consists of the following rules:

balanceC_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceC_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_out_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
pD_in_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → pD_out_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balanceC_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceC_in_gagaaaaaaa(x1, x3)
balanceC_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceC_out_gagaaaaaaa(x1, x3)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x1, x2, x3, x5, x19)
pD_in_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = pD_in_gagaaaaaaaggaaaa(x1, x3, x11, x12)
U9_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U9_gagaaaaaaaggaaaa(x1, x3, x11, x12, x17)
U10_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U10_gagaaaaaaaggaaaa(x1, x3, x11, x12, x17)
pD_out_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = pD_out_gagaaaaaaaggaaaa(x1, x3, x11, x12)
BALANCEC_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCEC_IN_GAGAAAAAAA(x1, x3)
PD_IN_GAGAAAAAAAGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = PD_IN_GAGAAAAAAAGGAAAA(x1, x3, x11, x12)
U9_GAGAAAAAAAGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U9_GAGAAAAAAAGGAAAA(x1, x3, x11, x12, x17)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BALANCEC_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → PD_IN_GAGAAAAAAAGGAAAA(T291, T292, T293, T295)
PD_IN_GAGAAAAAAAGGAAAA(T291, T292, T293, T295) → U9_GAGAAAAAAAGGAAAA(T291, T292, T293, T295, balanceC_in_gagaaaaaaa(T291, T292))
U9_GAGAAAAAAAGGAAAA(T291, T292, T293, T295, balanceC_out_gagaaaaaaa(T291, T292)) → BALANCEC_IN_GAGAAAAAAA(T293, T295)
PD_IN_GAGAAAAAAAGGAAAA(T291, T292, T293, T295) → BALANCEC_IN_GAGAAAAAAA(T291, T292)

The TRS R consists of the following rules:

balanceC_in_gagaaaaaaa(nil, T257) → balanceC_out_gagaaaaaaa(nil, T257)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U2_gagaaaaaaa(T291, T292, T293, T295, pD_in_gagaaaaaaaggaaaa(T291, T292, T293, T295))
U2_gagaaaaaaa(T291, T292, T293, T295, pD_out_gagaaaaaaaggaaaa(T291, T292, T293, T295)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T295)
pD_in_gagaaaaaaaggaaaa(T291, T292, T293, T295) → U9_gagaaaaaaaggaaaa(T291, T292, T293, T295, balanceC_in_gagaaaaaaa(T291, T292))
U9_gagaaaaaaaggaaaa(T291, T292, T293, T295, balanceC_out_gagaaaaaaa(T291, T292)) → U10_gagaaaaaaaggaaaa(T291, T292, T293, T295, balanceC_in_gagaaaaaaa(T293, T295))
U10_gagaaaaaaaggaaaa(T291, T292, T293, T295, balanceC_out_gagaaaaaaa(T293, T295)) → pD_out_gagaaaaaaaggaaaa(T291, T292, T293, T295)

The set Q consists of the following terms:

balanceC_in_gagaaaaaaa(x0, x1)
U2_gagaaaaaaa(x0, x1, x2, x3, x4)
pD_in_gagaaaaaaaggaaaa(x0, x1, x2, x3)
U9_gagaaaaaaaggaaaa(x0, x1, x2, x3, x4)
U10_gagaaaaaaaggaaaa(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

PD_IN_GAGAAAAAAAGGAAAA(T291, T292, T293, T295) → BALANCEC_IN_GAGAAAAAAA(T291, T292)
The graph contains the following edges 1 >= 1, 2 >= 2
PD_IN_GAGAAAAAAAGGAAAA(T291, T292, T293, T295) → U9_GAGAAAAAAAGGAAAA(T291, T292, T293, T295, balanceC_in_gagaaaaaaa(T291, T292))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
U9_GAGAAAAAAAGGAAAA(T291, T292, T293, T295, balanceC_out_gagaaaaaaa(T291, T292)) → BALANCEC_IN_GAGAAAAAAA(T293, T295)
The graph contains the following edges 3 >= 1, 4 >= 2
BALANCEC_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → PD_IN_GAGAAAAAAAGGAAAA(T291, T292, T293, T295)
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3, 2 >= 4

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PF_IN_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCEE_IN_GAAAAA(T420, T451, T452, T453, T455, T454)
BALANCEE_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → PF_IN_GAGAAAAAAAGA(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)

The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T25, T26, T27), tree(T33, T34, T36)) → U1_ga(T25, T26, T27, T33, T34, T36, pB_in_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27))
pB_in_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27) → U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
balanceG_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179) → balanceG_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X178, X178)), X179), X179)
balanceG_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253) → U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253))
pH_in_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253) → U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
balanceC_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceC_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
pD_in_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → pD_out_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387)
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_out_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
U7_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_in_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253))
U8_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253, balanceC_out_gagaaaaaaa(T144, T187, T146, X249, T188, T189, X250, X251, T191, X253)) → pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, T187, T158, T159, T160, T161, T162, T163, T164, T157, T188, T189, T190, T191, T144, T146, X249, X250, X251, X253)
U4_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X249, T160, T161, T163, T164, T159, T158, T162, T157, X250, X251, X252, X253, pH_out_gagaaaaaaaaaaaaaggaaaa(T142, T156, T143, X245, T158, T159, T160, T161, T162, T163, T164, T157, X246, X247, X252, X248, T144, T146, X249, X250, X251, X253)) → balanceG_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X249, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X250, X251, X252, X253)
U5_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceG_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_in_gaaaaa(T27, T53, T54, T55, T56, T57))
balanceE_in_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])) → balanceE_out_gaaaaa(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), []))
balanceE_in_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_in_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436))
pF_in_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U11_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U12_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceE_out_gaaaaa(T420, T451, T452, T453, T455, T454)) → pF_out_gagaaaaaaaga(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455)
U3_gaaaaa(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, pF_out_gagaaaaaaaga(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)) → balanceE_out_gaaaaa(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435)
U6_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27, balanceE_out_gaaaaa(T27, T53, T54, T55, T56, T57)) → pB_out_gagaaaaaaaaaag(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57, T27)
U1_ga(T25, T26, T27, T33, T34, T36, pB_out_gagaaaaaaaaaag(T25, T31, T26, X108, T33, T34, T35, T36, T32, X109, X110, X116, X111, T27)) → balanceA_out_ga(tree(T25, T26, T27), tree(T33, T34, T36))

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PF_IN_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455) → U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U11_GAGAAAAAAAGA(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454, T420, T455, balanceC_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCEE_IN_GAAAAA(T420, T451, T452, T453, T455, T454)
BALANCEE_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → PF_IN_GAGAAAAAAAGA(T418, T432, T419, X508, T433, T434, X509, X510, T435, X511, T420, T436)

The TRS R consists of the following rules:

balanceC_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balanceC_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387) → U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_in_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387))
U2_gagaaaaaaa(T291, T292, T293, T305, T295, X384, T296, T297, T298, T299, T300, T306, T302, T307, X385, X386, T308, X387, pD_out_gagaaaaaaaggaaaa(T291, T305, T292, X380, T306, T307, X381, X382, T308, X383, T293, T295, X384, X385, X386, X387)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X384, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X385, X386, T308, X387)
pD_in_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387) → U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U9_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_in_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387))
U10_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387, balanceC_out_gagaaaaaaa(T293, T323, T295, X384, T324, T325, X385, X386, T326, X387)) → pD_out_gagaaaaaaaggaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326, T293, T295, X384, X385, X386, X387)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balanceC_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceC_in_gagaaaaaaa(x1, x3)
balanceC_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balanceC_out_gagaaaaaaa(x1, x3)
U2_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_gagaaaaaaa(x1, x2, x3, x5, x19)
pD_in_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = pD_in_gagaaaaaaaggaaaa(x1, x3, x11, x12)
U9_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U9_gagaaaaaaaggaaaa(x1, x3, x11, x12, x17)
U10_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U10_gagaaaaaaaggaaaa(x1, x3, x11, x12, x17)
pD_out_gagaaaaaaaggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = pD_out_gagaaaaaaaggaaaa(x1, x3, x11, x12)
BALANCEE_IN_GAAAAA(x1, x2, x3, x4, x5, x6) = BALANCEE_IN_GAAAAA(x1)
PF_IN_GAGAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = PF_IN_GAGAAAAAAAGA(x1, x3, x11)
U11_GAGAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U11_GAGAAAAAAAGA(x1, x3, x11, x13)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PF_IN_GAGAAAAAAAGA(T418, T419, T420) → U11_GAGAAAAAAAGA(T418, T419, T420, balanceC_in_gagaaaaaaa(T418, T419))
U11_GAGAAAAAAAGA(T418, T419, T420, balanceC_out_gagaaaaaaa(T418, T419)) → BALANCEE_IN_GAAAAA(T420)
BALANCEE_IN_GAAAAA(tree(T418, T419, T420)) → PF_IN_GAGAAAAAAAGA(T418, T419, T420)

The TRS R consists of the following rules:

balanceC_in_gagaaaaaaa(nil, T257) → balanceC_out_gagaaaaaaa(nil, T257)
balanceC_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U2_gagaaaaaaa(T291, T292, T293, T295, pD_in_gagaaaaaaaggaaaa(T291, T292, T293, T295))
U2_gagaaaaaaa(T291, T292, T293, T295, pD_out_gagaaaaaaaggaaaa(T291, T292, T293, T295)) → balanceC_out_gagaaaaaaa(tree(T291, T292, T293), T295)
pD_in_gagaaaaaaaggaaaa(T291, T292, T293, T295) → U9_gagaaaaaaaggaaaa(T291, T292, T293, T295, balanceC_in_gagaaaaaaa(T291, T292))
U9_gagaaaaaaaggaaaa(T291, T292, T293, T295, balanceC_out_gagaaaaaaa(T291, T292)) → U10_gagaaaaaaaggaaaa(T291, T292, T293, T295, balanceC_in_gagaaaaaaa(T293, T295))
U10_gagaaaaaaaggaaaa(T291, T292, T293, T295, balanceC_out_gagaaaaaaa(T293, T295)) → pD_out_gagaaaaaaaggaaaa(T291, T292, T293, T295)

The set Q consists of the following terms:

balanceC_in_gagaaaaaaa(x0, x1)
U2_gagaaaaaaa(x0, x1, x2, x3, x4)
pD_in_gagaaaaaaaggaaaa(x0, x1, x2, x3)
U9_gagaaaaaaaggaaaa(x0, x1, x2, x3, x4)
U10_gagaaaaaaaggaaaa(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U11_GAGAAAAAAAGA(T418, T419, T420, balanceC_out_gagaaaaaaa(T418, T419)) → BALANCEE_IN_GAAAAA(T420)
The graph contains the following edges 3 >= 1
BALANCEE_IN_GAAAAA(tree(T418, T419, T420)) → PF_IN_GAGAAAAAAAGA(T418, T419, T420)
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3
PF_IN_GAGAAAAAAAGA(T418, T419, T420) → U11_GAGAAAAAAAGA(T418, T419, T420, balanceC_in_gagaaaaaaa(T418, T419))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES