Left Termination proof of /tmp/tmppJsvAU/untupled_bal

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 637 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 425 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 11 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

(0) Obligation:

Clauses:

balance(T, TB) :- balance55(T, XX0, XX1, [], .(','(nil, -(XX0, XX0)), XX1), [], .(','(TB, -(I, [])), X), X, I, []).
balance55(nil, C, T, T, A, B, A, B, X, X).
balance55(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT) :- ','(balance55(L, XX0, XX1, .(','(nil, -(XX2, XX2)), XX3), HR1, TR1, H, T, IH, .(V, IT1)), balance55(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)).
balance5(nil, C, T, T, A, B, A, B, X, X) :- balance55(nil, C, T, T, A, B, A, B, X, X).
balance5(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT) :- balance55(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT).
balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)) :- balance5(nil, C, T, T, A, B, A, B, X, X).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(.(','(nil, -(XX0, XX0)), XX1), NT)) :- balance5(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT).

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];
5 [label="5: balance(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, [])\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, []), SCOPE: 2, CLAUSE: 1 | balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, []), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, []), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, []), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="B: ','(balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), balance55(T22, X115, X116, [], .(','(nil, -(X120, X120)), X121), [], X117, X118, X119, []))\n\nT20 is ground\nT21 is ground\nT22 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="G: balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119))\n\nT20 is ground\nT21 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="E: balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, [])\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), SCOPE: 3, CLAUSE: 1 | balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nT21 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), SCOPE: 3, CLAUSE: 1\n\nT20 is ground\nT21 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nT21 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="H: ','(balance55(T139, X303, X304, .(','(nil, -(X298, X298)), X299), X300, X301, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, .(T140, X302)), balance55(T141, X298, X299, .(','(nil, -(X305, X305)), X306), X307, X308, X300, X301, X302, .(T152, X309)))\n\nT139 is ground\nT140 is ground\nT141 is ground\nT152 is ground\nX303 is free\nX304 is free\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free\nX298 is free\nX299 is free\nX300 is free\nX301 is free\nX302 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: balance55(T139, X303, X304, .(','(nil, -(X298, X298)), X299), X300, X301, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, .(T140, X302))\n\nT139 is ground\nT140 is ground\nX303 is free\nX304 is free\nX298 is free\nX299 is free\nX300 is free\nX301 is free\nX302 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="C: balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309))\n\nT141 is ground\nT152 is ground\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309)), SCOPE: 4, CLAUSE: 1 | balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309)), SCOPE: 4, CLAUSE: 2\n\nT141 is ground\nT152 is ground\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309)), SCOPE: 4, CLAUSE: 1\n\nT141 is ground\nT152 is ground\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309)), SCOPE: 4, CLAUSE: 2\n\nT141 is ground\nT152 is ground\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="D: ','(balance55(T306, T321, T322, .(','(nil, -(X472, X472)), X473), X474, X475, T323, T324, T325, .(T307, X476)), balance55(T308, X472, X473, .(','(nil, -(X477, X477)), X478), X479, X480, X474, X475, X476, .(T320, X481)))\n\nT306 is ground\nT307 is ground\nT308 is ground\nT320 is ground\nX477 is free\nX478 is free\nX479 is free\nX480 is free\nX481 is free\nX472 is free\nX473 is free\nX474 is free\nX475 is free\nX476 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: balance55(T306, T321, T322, .(','(nil, -(X472, X472)), X473), X474, X475, T323, T324, T325, .(T307, X476))\n\nT306 is ground\nT307 is ground\nX472 is free\nX473 is free\nX474 is free\nX475 is free\nX476 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: balance55(T308, T344, T345, .(','(nil, -(X477, X477)), X478), X479, X480, T346, T347, T348, .(T320, X481))\n\nT308 is ground\nT320 is ground\nX477 is free\nX478 is free\nX479 is free\nX480 is free\nX481 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, []), SCOPE: 5, CLAUSE: 1 | balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, []), SCOPE: 5, CLAUSE: 2\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, []), SCOPE: 5, CLAUSE: 1\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, []), SCOPE: 5, CLAUSE: 2\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="F: ','(balance55(T452, T468, T469, .(','(nil, -(X618, X618)), X619), X620, X621, T470, T471, T472, .(T453, X622)), balance55(T454, X618, X619, [], .(','(nil, -(T474, T474)), T473), [], X620, X621, X622, []))\n\nT452 is ground\nT453 is ground\nT454 is ground\nX618 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: balance55(T452, T468, T469, .(','(nil, -(X618, X618)), X619), X620, X621, T470, T471, T472, .(T453, X622))\n\nT452 is ground\nT453 is ground\nX618 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: balance55(T454, T493, T494, [], .(','(nil, -(T498, T498)), T499), [], T495, T496, T497, [])\n\nT454 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 114 [arrowhead = none ];
114 -> 5;

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

116 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 116 [arrowhead = none ];
116 -> 10;

117 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 117 [arrowhead = none ];
117 -> 12;

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

119 [label="EVAL with clause\nbalance55(nil, X37, X38, X38, X39, X40, X39, X40, X41, X41).\nand substitutionT5 -> nil,\nX5 -> [],\nX37 -> [],\nX6 -> [],\nX38 -> [],\nX43 -> [],\nX39 -> .(','(nil, -([], [])), []),\nX40 -> [],\nT7 -> nil,\nX7 -> [],\nX42 -> [],\nX8 -> [],\nX41 -> []", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 119 [arrowhead = none ];
119 -> 17;

120 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 120 [arrowhead = none ];
120 -> 19;

121 [label="EVAL with clause\nbalance55(tree(X97, X98, X99), X100, X101, X102, X103, X104, .(','(tree(X105, X106, X107), -(X108, X109)), X110), .(','(X105, -(X108, .(X106, X111))), .(','(X107, -(X111, X109)), X112)), X113, X114) :- ','(balance55(X97, X100, X101, .(','(nil, -(X115, X115)), X116), X117, X118, X110, X112, X113, .(X98, X119)), balance55(X99, X115, X116, X102, X103, X104, X117, X118, X119, X114)).\nand substitutionX97 -> T20,\nX98 -> T21,\nX99 -> T22,\nT5 -> tree(T20, T21, T22),\nX5 -> X120,\nX100 -> X120,\nX6 -> X121,\nX101 -> X121,\nX102 -> [],\nX103 -> .(','(nil, -(X120, X120)), X121),\nX104 -> [],\nX105 -> T28,\nX106 -> T29,\nX107 -> T31,\nT7 -> tree(T28, T29, T31),\nX7 -> T27,\nX108 -> T27,\nX109 -> [],\nX8 -> .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)),\nX110 -> .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)),\nX111 -> T30,\nX112 -> T26,\nX123 -> .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)),\nX113 -> T27,\nX114 -> [],\nX125 -> T26,\nX122 -> T27,\nT23 -> T28,\nT24 -> T29,\nX124 -> T30,\nT25 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 121 [arrowhead = none ];
121 -> 29;

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

123 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 123 [arrowhead = none ];
123 -> 20;

124 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
29 -> 124 [arrowhead = none ];
124 -> 35;

125 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nreplacements:X120 -> T48,\nX121 -> T49,\nX115 -> T50,\nX116 -> T51,\nX117 -> T52,\nX118 -> T53,\nX119 -> T54", fontsize=14, style = filled, fillcolor = violet];
29 -> 125 [arrowhead = none ];
125 -> 36;

126 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 126 [arrowhead = none ];
126 -> 39;

127 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
36 -> 127 [arrowhead = none ];
127 -> 90;

128 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 128 [arrowhead = none ];
128 -> 44;

129 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 129 [arrowhead = none ];
129 -> 45;

130 [label="EVAL with clause\nbalance55(nil, X214, X215, X215, X216, X217, X216, X217, X218, X218).\nand substitutionT20 -> nil,\nX120 -> X219,\nX214 -> X219,\nX121 -> .(','(nil, -(X221, X221)), X222),\nX215 -> .(','(nil, -(X221, X221)), X222),\nX115 -> X221,\nX116 -> X222,\nX220 -> .(','(nil, -(X221, X221)), X222),\nX117 -> .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)),\nX216 -> .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)),\nX118 -> T108,\nX217 -> T108,\nT28 -> T103,\nT27 -> .(T109, T110),\nT29 -> T105,\nT30 -> T106,\nT31 -> T107,\nT26 -> T108,\nX223 -> .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)),\nX224 -> T108,\nX218 -> .(T109, T110),\nT21 -> T109,\nX119 -> T110,\nT104 -> .(T109, T110)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 130 [arrowhead = none ];
130 -> 49;

131 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 131 [arrowhead = none ];
131 -> 50;

132 [label="EVAL with clause\nbalance55(tree(X280, X281, X282), X283, X284, X285, X286, X287, .(','(tree(X288, X289, X290), -(X291, X292)), X293), .(','(X288, -(X291, .(X289, X294))), .(','(X290, -(X294, X292)), X295)), X296, X297) :- ','(balance55(X280, X283, X284, .(','(nil, -(X298, X298)), X299), X300, X301, X293, X295, X296, .(X281, X302)), balance55(X282, X298, X299, X285, X286, X287, X300, X301, X302, X297)).\nand substitutionX280 -> T139,\nX281 -> T140,\nX282 -> T141,\nT20 -> tree(T139, T140, T141),\nX120 -> X303,\nX283 -> X303,\nX121 -> X304,\nX284 -> X304,\nX115 -> X305,\nX116 -> X306,\nX285 -> .(','(nil, -(X305, X305)), X306),\nX117 -> X307,\nX286 -> X307,\nX118 -> X308,\nX287 -> X308,\nX288 -> T157,\nX289 -> T158,\nX290 -> T160,\nT28 -> tree(T157, T158, T160),\nT27 -> T154,\nX291 -> T154,\nT29 -> T161,\nT30 -> T156,\nX292 -> .(T161, T156),\nT31 -> T155,\nT26 -> .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)),\nX293 -> .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))),\nX294 -> T159,\nX295 -> T153,\nT149 -> .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)),\nX296 -> T154,\nT21 -> T152,\nX119 -> X309,\nX297 -> .(T152, X309),\nT151 -> T153,\nT145 -> T154,\nT148 -> T155,\nT147 -> T156,\nT142 -> T157,\nT143 -> T158,\nT150 -> T159,\nT144 -> T160,\nT146 -> T161", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 132 [arrowhead = none ];
132 -> 57;

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

134 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 134 [arrowhead = none ];
134 -> 51;

135 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
57 -> 135 [arrowhead = none ];
135 -> 61;

136 [label="SPLIT 2\nnew knowledge:\nT139 is ground\nreplacements:X303 -> T184,\nX304 -> T185,\nX298 -> T186,\nX299 -> T187,\nX300 -> T188,\nX301 -> T189,\nX302 -> T190", fontsize=14, style = filled, fillcolor = violet];
57 -> 136 [arrowhead = none ];
136 -> 62;

137 [label="INSTANCE with matching:\nT141 -> T139\nT186 -> X303\nT187 -> X304\nX305 -> X298\nX306 -> X299\nX307 -> X300\nX308 -> X301\nT188 -> .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)))\nT189 -> T153\nT190 -> T154\nT152 -> T140\nX309 -> X302", fontsize=14, style = filled, fillcolor = lightgrey];
61 -> 137 [arrowhead = none , style=dashed];
137 -> 62[style=dashed];

138 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
62 -> 138 [arrowhead = none ];
138 -> 67;

139 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 139 [arrowhead = none ];
139 -> 70;

140 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 140 [arrowhead = none ];
140 -> 71;

141 [label="EVAL with clause\nbalance55(nil, X396, X397, X397, X398, X399, X398, X399, X400, X400).\nand substitutionT141 -> nil,\nT186 -> T267,\nX396 -> T267,\nT187 -> .(','(nil, -(T269, T269)), T270),\nX397 -> .(','(nil, -(T269, T269)), T270),\nX305 -> T269,\nX306 -> T270,\nT268 -> .(','(nil, -(T269, T269)), T270),\nX307 -> T271,\nX398 -> T271,\nX308 -> T272,\nX399 -> T272,\nT188 -> T271,\nX401 -> T271,\nT189 -> T272,\nX402 -> T272,\nT190 -> .(T274, T275),\nX400 -> .(T274, T275),\nT152 -> T274,\nX309 -> T275,\nT273 -> .(T274, T275)", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 141 [arrowhead = none ];
141 -> 75;

142 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 142 [arrowhead = none ];
142 -> 76;

143 [label="EVAL with clause\nbalance55(tree(X454, X455, X456), X457, X458, X459, X460, X461, .(','(tree(X462, X463, X464), -(X465, X466)), X467), .(','(X462, -(X465, .(X463, X468))), .(','(X464, -(X468, X466)), X469)), X470, X471) :- ','(balance55(X454, X457, X458, .(','(nil, -(X472, X472)), X473), X474, X475, X467, X469, X470, .(X455, X476)), balance55(X456, X472, X473, X459, X460, X461, X474, X475, X476, X471)).\nand substitutionX454 -> T306,\nX455 -> T307,\nX456 -> T308,\nT141 -> tree(T306, T307, T308),\nT186 -> T321,\nX457 -> T321,\nT187 -> T322,\nX458 -> T322,\nX305 -> X477,\nX306 -> X478,\nX459 -> .(','(nil, -(X477, X477)), X478),\nX307 -> X479,\nX460 -> X479,\nX308 -> X480,\nX461 -> X480,\nX462 -> T311,\nX463 -> T312,\nX464 -> T313,\nX465 -> T314,\nX466 -> T315,\nX467 -> T323,\nT188 -> .(','(tree(T311, T312, T313), -(T314, T315)), T323),\nX468 -> T317,\nX469 -> T324,\nT189 -> .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)),\nT190 -> T325,\nX470 -> T325,\nT152 -> T320,\nX309 -> X481,\nX471 -> .(T320, X481),\nT309 -> T321,\nT310 -> T322,\nT316 -> T323,\nT318 -> T324,\nT319 -> T325", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 143 [arrowhead = none ];
143 -> 82;

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

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

146 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
82 -> 146 [arrowhead = none ];
146 -> 84;

147 [label="SPLIT 2\nnew knowledge:\nT306 is ground\nreplacements:X472 -> T344,\nX473 -> T345,\nX474 -> T346,\nX475 -> T347,\nX476 -> T348", fontsize=14, style = filled, fillcolor = violet];
82 -> 147 [arrowhead = none ];
147 -> 85;

148 [label="INSTANCE with matching:\nT141 -> T306\nT186 -> T321\nT187 -> T322\nX305 -> X472\nX306 -> X473\nX307 -> X474\nX308 -> X475\nT188 -> T323\nT189 -> T324\nT190 -> T325\nT152 -> T307\nX309 -> X476", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 148 [arrowhead = none , style=dashed];
148 -> 62[style=dashed];

149 [label="INSTANCE with matching:\nT141 -> T308\nT186 -> T344\nT187 -> T345\nX305 -> X477\nX306 -> X478\nX307 -> X479\nX308 -> X480\nT188 -> T346\nT189 -> T347\nT190 -> T348\nT152 -> T320\nX309 -> X481", fontsize=14, style = filled, fillcolor = lightgrey];
85 -> 149 [arrowhead = none , style=dashed];
149 -> 62[style=dashed];

150 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
90 -> 150 [arrowhead = none ];
150 -> 91;

151 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
90 -> 151 [arrowhead = none ];
151 -> 92;

152 [label="EVAL with clause\nbalance55(nil, X554, X555, X555, X556, X557, X556, X557, X558, X558).\nand substitutionT22 -> nil,\nT50 -> T415,\nX554 -> T415,\nT51 -> [],\nX555 -> [],\nT416 -> [],\nT48 -> T417,\nT49 -> T418,\nX556 -> .(','(nil, -(T417, T417)), T418),\nX557 -> [],\nT52 -> .(','(nil, -(T417, T417)), T418),\nT53 -> [],\nT54 -> [],\nX558 -> [],\nT419 -> []", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 152 [arrowhead = none ];
152 -> 94;

153 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 153 [arrowhead = none ];
153 -> 95;

154 [label="EVAL with clause\nbalance55(tree(X600, X601, X602), X603, X604, X605, X606, X607, .(','(tree(X608, X609, X610), -(X611, X612)), X613), .(','(X608, -(X611, .(X609, X614))), .(','(X610, -(X614, X612)), X615)), X616, X617) :- ','(balance55(X600, X603, X604, .(','(nil, -(X618, X618)), X619), X620, X621, X613, X615, X616, .(X601, X622)), balance55(X602, X618, X619, X605, X606, X607, X620, X621, X622, X617)).\nand substitutionX600 -> T452,\nX601 -> T453,\nX602 -> T454,\nT22 -> tree(T452, T453, T454),\nT50 -> T468,\nX603 -> T468,\nT51 -> T469,\nX604 -> T469,\nX605 -> [],\nT48 -> T474,\nT49 -> T473,\nX606 -> .(','(nil, -(T474, T474)), T473),\nX607 -> [],\nX608 -> T459,\nX609 -> T460,\nX610 -> T461,\nX611 -> T462,\nX612 -> T463,\nX613 -> T470,\nT52 -> .(','(tree(T459, T460, T461), -(T462, T463)), T470),\nX614 -> T465,\nX615 -> T471,\nT53 -> .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)),\nT54 -> T472,\nX616 -> T472,\nX617 -> [],\nT455 -> T468,\nT456 -> T469,\nT464 -> T470,\nT466 -> T471,\nT467 -> T472,\nT458 -> T473,\nT457 -> T474", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 154 [arrowhead = none ];
154 -> 108;

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

156 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 156 [arrowhead = none ];
156 -> 96;

157 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
108 -> 157 [arrowhead = none ];
157 -> 112;

158 [label="SPLIT 2\nnew knowledge:\nT452 is ground\nreplacements:X618 -> T493,\nX619 -> T494,\nX620 -> T495,\nX621 -> T496,\nX622 -> T497,\nT474 -> T498,\nT473 -> T499", fontsize=14, style = filled, fillcolor = violet];
108 -> 158 [arrowhead = none ];
158 -> 113;

159 [label="INSTANCE with matching:\nT141 -> T452\nT186 -> T468\nT187 -> T469\nX305 -> X618\nX306 -> X619\nX307 -> X620\nX308 -> X621\nT188 -> T470\nT189 -> T471\nT190 -> T472\nT152 -> T453\nX309 -> X622", fontsize=14, style = filled, fillcolor = lightgrey];
112 -> 159 [arrowhead = none , style=dashed];
159 -> 62[style=dashed];

160 [label="INSTANCE with matching:\nT22 -> T454\nT50 -> T493\nT51 -> T494\nT48 -> T498\nT49 -> T499\nT52 -> T495\nT53 -> T496\nT54 -> T497", fontsize=14, style = filled, fillcolor = lightgrey];
113 -> 160 [arrowhead = none , style=dashed];
160 -> 36[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(T20, T21, T22), tree(T28, T29, T31)) → U1_ga(T20, T21, T22, T28, T29, T31, pB_in_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22))
pB_in_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
balance55G_in_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55G_out_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55G_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309))
pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
balance55C_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55C_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)) → pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481)
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481)
U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309))
U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309)) → pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309)
U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309)) → balance55G_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309)
U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance55E_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance55E_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
balance55E_in_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_in_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473))
pF_in_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → pF_out_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499)
U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_out_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)) → balance55E_out_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472)
U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → pB_out_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22)
U1_ga(T20, T21, T22, T28, T29, T31, pB_out_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22)) → balanceA_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

(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(T20, T21, T22), tree(T28, T29, T31)) → U1_GA(T20, T21, T22, T28, T29, T31, pB_in_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22))
BALANCEA_IN_GA(tree(T20, T21, T22), tree(T28, T29, T31)) → PB_IN_GAAAAAAAAAAAAGAG(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22)
PB_IN_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → U5_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
PB_IN_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → BALANCE55G_IN_GAAAAAAAAAAAAGA(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)
BALANCE55G_IN_GAAAAAAAAAAAAGA(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → U4_GAAAAAAAAAAAAGA(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309))
BALANCE55G_IN_GAAAAAAAAAAAAGA(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → PH_IN_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309)
PH_IN_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → U7_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
PH_IN_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → BALANCE55C_IN_GAAAAAAAAAGA(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)
BALANCE55C_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
BALANCE55C_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → BALANCE55C_IN_GAAAAAAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)
U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → BALANCE55C_IN_GAAAAAAAAAGA(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)
U7_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U8_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309))
U7_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → BALANCE55C_IN_GAAAAAAAAAGA(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309)
U5_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U6_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
U5_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → BALANCE55E_IN_GAAAAAAA(T22, T50, T51, T48, T49, T52, T53, T54)
BALANCE55E_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U3_GAAAAAAA(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_in_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473))
BALANCE55E_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → PF_IN_GAAAAAAAAAGAGAA(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)
PF_IN_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
PF_IN_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → BALANCE55C_IN_GAAAAAAAAAGA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)
U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U12_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → BALANCE55E_IN_GAAAAAAA(T454, T493, T494, T498, T499, T495, T496, T497)

The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U1_ga(T20, T21, T22, T28, T29, T31, pB_in_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22))
pB_in_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
balance55G_in_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55G_out_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55G_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309))
pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
balance55C_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55C_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)) → pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481)
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481)
U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309))
U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309)) → pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309)
U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309)) → balance55G_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309)
U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance55E_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance55E_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
balance55E_in_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_in_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473))
pF_in_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → pF_out_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499)
U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_out_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)) → balance55E_out_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472)
U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → pB_out_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22)
U1_ga(T20, T21, T22, T28, T29, T31, pB_out_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22)) → balanceA_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

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_gaaaaaaaaaaaagag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = pB_in_gaaaaaaaaaaaagag(x1, x14, x16)
U5_gaaaaaaaaaaaagag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U5_gaaaaaaaaaaaagag(x1, x14, x16, x17)
balance55G_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = balance55G_in_gaaaaaaaaaaaaga(x1, x14)
balance55G_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = balance55G_out_gaaaaaaaaaaaaga(x1, x14)
U4_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U4_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
pH_in_gaaaaaaaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25) = pH_in_gaaaaaaaaaaaaaaagagaaaaga(x1, x17, x19, x24)
U7_gaaaaaaaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26) = U7_gaaaaaaaaaaaaaaagagaaaaga(x1, x17, x19, x24, x26)
balance55C_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance55C_in_gaaaaaaaaaga(x1, x11)
balance55C_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance55C_out_gaaaaaaaaaga(x1, x11)
U2_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U2_gaaaaaaaaaga(x1, x2, x3, x19, x21)
pD_in_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = pD_in_gaaaaaaaaagagaaaaga(x1, x11, x13, x18)
U9_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U9_gaaaaaaaaagagaaaaga(x1, x11, x13, x18, x20)
U10_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U10_gaaaaaaaaagagaaaaga(x1, x11, x13, x18, x20)
pD_out_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = pD_out_gaaaaaaaaagagaaaaga(x1, x11, x13, x18)
U8_gaaaaaaaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26) = U8_gaaaaaaaaaaaaaaagagaaaaga(x1, x17, x19, x24, x26)
pH_out_gaaaaaaaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25) = pH_out_gaaaaaaaaaaaaaaagagaaaaga(x1, x17, x19, x24)
U6_gaaaaaaaaaaaagag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U6_gaaaaaaaaaaaagag(x1, x14, x16, x17)
balance55E_in_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = balance55E_in_gaaaaaaa(x1)
balance55E_out_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = balance55E_out_gaaaaaaa(x1)
U3_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U3_gaaaaaaa(x1, x2, x3, x17)
pF_in_gaaaaaaaaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = pF_in_gaaaaaaaaagagaa(x1, x11, x13)
U11_gaaaaaaaaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U11_gaaaaaaaaagagaa(x1, x11, x13, x16)
U12_gaaaaaaaaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U12_gaaaaaaaaagagaa(x1, x11, x13, x16)
pF_out_gaaaaaaaaagagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = pF_out_gaaaaaaaaagagaa(x1, x11, x13)
pB_out_gaaaaaaaaaaaagag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = pB_out_gaaaaaaaaaaaagag(x1, x14, x16)
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_GAAAAAAAAAAAAGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = PB_IN_GAAAAAAAAAAAAGAG(x1, x14, x16)
U5_GAAAAAAAAAAAAGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U5_GAAAAAAAAAAAAGAG(x1, x14, x16, x17)
BALANCE55G_IN_GAAAAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = BALANCE55G_IN_GAAAAAAAAAAAAGA(x1, x14)
U4_GAAAAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U4_GAAAAAAAAAAAAGA(x1, x2, x3, x19, x21)
PH_IN_GAAAAAAAAAAAAAAAGAGAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25) = PH_IN_GAAAAAAAAAAAAAAAGAGAAAAGA(x1, x17, x19, x24)
U7_GAAAAAAAAAAAAAAAGAGAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26) = U7_GAAAAAAAAAAAAAAAGAGAAAAGA(x1, x17, x19, x24, x26)
BALANCE55C_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = BALANCE55C_IN_GAAAAAAAAAGA(x1, x11)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
PD_IN_GAAAAAAAAAGAGAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = PD_IN_GAAAAAAAAAGAGAAAAGA(x1, x11, x13, x18)
U9_GAAAAAAAAAGAGAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U9_GAAAAAAAAAGAGAAAAGA(x1, x11, x13, x18, x20)
U10_GAAAAAAAAAGAGAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U10_GAAAAAAAAAGAGAAAAGA(x1, x11, x13, x18, x20)
U8_GAAAAAAAAAAAAAAAGAGAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26) = U8_GAAAAAAAAAAAAAAAGAGAAAAGA(x1, x17, x19, x24, x26)
U6_GAAAAAAAAAAAAGAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U6_GAAAAAAAAAAAAGAG(x1, x14, x16, x17)
BALANCE55E_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = BALANCE55E_IN_GAAAAAAA(x1)
U3_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U3_GAAAAAAA(x1, x2, x3, x17)
PF_IN_GAAAAAAAAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = PF_IN_GAAAAAAAAAGAGAA(x1, x11, x13)
U11_GAAAAAAAAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U11_GAAAAAAAAAGAGAA(x1, x11, x13, x16)
U12_GAAAAAAAAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U12_GAAAAAAAAAGAGAA(x1, x11, x13, x16)

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(T20, T21, T22), tree(T28, T29, T31)) → U1_GA(T20, T21, T22, T28, T29, T31, pB_in_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22))
BALANCEA_IN_GA(tree(T20, T21, T22), tree(T28, T29, T31)) → PB_IN_GAAAAAAAAAAAAGAG(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22)
PB_IN_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → U5_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
PB_IN_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → BALANCE55G_IN_GAAAAAAAAAAAAGA(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)
BALANCE55G_IN_GAAAAAAAAAAAAGA(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → U4_GAAAAAAAAAAAAGA(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309))
BALANCE55G_IN_GAAAAAAAAAAAAGA(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → PH_IN_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309)
PH_IN_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → U7_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
PH_IN_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → BALANCE55C_IN_GAAAAAAAAAGA(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)
BALANCE55C_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_GAAAAAAAAAGA(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
BALANCE55C_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → BALANCE55C_IN_GAAAAAAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)
U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → BALANCE55C_IN_GAAAAAAAAAGA(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)
U7_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U8_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309))
U7_GAAAAAAAAAAAAAAAGAGAAAAGA(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → BALANCE55C_IN_GAAAAAAAAAGA(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309)
U5_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U6_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
U5_GAAAAAAAAAAAAGAG(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → BALANCE55E_IN_GAAAAAAA(T22, T50, T51, T48, T49, T52, T53, T54)
BALANCE55E_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U3_GAAAAAAA(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_in_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473))
BALANCE55E_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → PF_IN_GAAAAAAAAAGAGAA(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)
PF_IN_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
PF_IN_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → BALANCE55C_IN_GAAAAAAAAAGA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)
U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U12_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → BALANCE55E_IN_GAAAAAAA(T454, T493, T494, T498, T499, T495, T496, T497)

The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U1_ga(T20, T21, T22, T28, T29, T31, pB_in_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22))
pB_in_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
balance55G_in_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55G_out_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55G_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309))
pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
balance55C_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55C_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)) → pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481)
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481)
U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309))
U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309)) → pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309)
U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309)) → balance55G_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309)
U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance55E_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance55E_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
balance55E_in_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_in_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473))
pF_in_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → pF_out_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499)
U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_out_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)) → balance55E_out_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472)
U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → pB_out_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22)
U1_ga(T20, T21, T22, T28, T29, T31, pB_out_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22)) → balanceA_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

(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:

BALANCE55C_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → BALANCE55C_IN_GAAAAAAAAAGA(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → BALANCE55C_IN_GAAAAAAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)

The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U1_ga(T20, T21, T22, T28, T29, T31, pB_in_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22))
pB_in_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
balance55G_in_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55G_out_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55G_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309))
pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
balance55C_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55C_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)) → pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481)
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481)
U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309))
U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309)) → pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309)
U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309)) → balance55G_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309)
U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance55E_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance55E_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
balance55E_in_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_in_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473))
pF_in_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → pF_out_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499)
U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_out_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)) → balance55E_out_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472)
U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → pB_out_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22)
U1_ga(T20, T21, T22, T28, T29, T31, pB_out_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22)) → balanceA_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

(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:

BALANCE55C_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → BALANCE55C_IN_GAAAAAAAAAGA(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → BALANCE55C_IN_GAAAAAAAAAGA(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)

The TRS R consists of the following rules:

balance55C_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55C_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481)
pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)) → pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balance55C_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance55C_in_gaaaaaaaaaga(x1, x11)
balance55C_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance55C_out_gaaaaaaaaaga(x1, x11)
U2_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U2_gaaaaaaaaaga(x1, x2, x3, x19, x21)
pD_in_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = pD_in_gaaaaaaaaagagaaaaga(x1, x11, x13, x18)
U9_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U9_gaaaaaaaaagagaaaaga(x1, x11, x13, x18, x20)
U10_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U10_gaaaaaaaaagagaaaaga(x1, x11, x13, x18, x20)
pD_out_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = pD_out_gaaaaaaaaagagaaaaga(x1, x11, x13, x18)
BALANCE55C_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = BALANCE55C_IN_GAAAAAAAAAGA(x1, x11)
PD_IN_GAAAAAAAAAGAGAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = PD_IN_GAAAAAAAAAGAGAAAAGA(x1, x11, x13, x18)
U9_GAAAAAAAAAGAGAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U9_GAAAAAAAAAGAGAAAAGA(x1, x11, x13, x18, x20)

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:

BALANCE55C_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T320) → PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320)
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320) → U9_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320, balance55C_in_gaaaaaaaaaga(T306, T307))
U9_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320, balance55C_out_gaaaaaaaaaga(T306, T307)) → BALANCE55C_IN_GAAAAAAAAAGA(T308, T320)
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320) → BALANCE55C_IN_GAAAAAAAAAGA(T306, T307)

The TRS R consists of the following rules:

balance55C_in_gaaaaaaaaaga(nil, T274) → balance55C_out_gaaaaaaaaaga(nil, T274)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T320) → U2_gaaaaaaaaaga(T306, T307, T308, T320, pD_in_gaaaaaaaaagagaaaaga(T306, T307, T308, T320))
U2_gaaaaaaaaaga(T306, T307, T308, T320, pD_out_gaaaaaaaaagagaaaaga(T306, T307, T308, T320)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T320)
pD_in_gaaaaaaaaagagaaaaga(T306, T307, T308, T320) → U9_gaaaaaaaaagagaaaaga(T306, T307, T308, T320, balance55C_in_gaaaaaaaaaga(T306, T307))
U9_gaaaaaaaaagagaaaaga(T306, T307, T308, T320, balance55C_out_gaaaaaaaaaga(T306, T307)) → U10_gaaaaaaaaagagaaaaga(T306, T307, T308, T320, balance55C_in_gaaaaaaaaaga(T308, T320))
U10_gaaaaaaaaagagaaaaga(T306, T307, T308, T320, balance55C_out_gaaaaaaaaaga(T308, T320)) → pD_out_gaaaaaaaaagagaaaaga(T306, T307, T308, T320)

The set Q consists of the following terms:

balance55C_in_gaaaaaaaaaga(x0, x1)
U2_gaaaaaaaaaga(x0, x1, x2, x3, x4)
pD_in_gaaaaaaaaagagaaaaga(x0, x1, x2, x3)
U9_gaaaaaaaaagagaaaaga(x0, x1, x2, x3, x4)
U10_gaaaaaaaaagagaaaaga(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_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320) → BALANCE55C_IN_GAAAAAAAAAGA(T306, T307)
The graph contains the following edges 1 >= 1, 2 >= 2
PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320) → U9_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320, balance55C_in_gaaaaaaaaaga(T306, T307))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
U9_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320, balance55C_out_gaaaaaaaaaga(T306, T307)) → BALANCE55C_IN_GAAAAAAAAAGA(T308, T320)
The graph contains the following edges 3 >= 1, 4 >= 2
BALANCE55C_IN_GAAAAAAAAAGA(tree(T306, T307, T308), T320) → PD_IN_GAAAAAAAAAGAGAAAAGA(T306, T307, T308, T320)
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_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → BALANCE55E_IN_GAAAAAAA(T454, T493, T494, T498, T499, T495, T496, T497)
BALANCE55E_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → PF_IN_GAAAAAAAAAGAGAA(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)

The TRS R consists of the following rules:

balanceA_in_ga(nil, nil) → balanceA_out_ga(nil, nil)
balanceA_in_ga(tree(T20, T21, T22), tree(T28, T29, T31)) → U1_ga(T20, T21, T22, T28, T29, T31, pB_in_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22))
pB_in_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22) → U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_in_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54))
balance55G_in_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110) → balance55G_out_gaaaaaaaaaaaaga(nil, X219, .(','(nil, -(X221, X221)), X222), X221, X222, .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)), T108, T103, .(T109, T110), T105, T106, T107, T108, T109, T110)
balance55G_in_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309) → U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309))
pH_in_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309) → U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190))
balance55C_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55C_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)) → pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481)
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481)
U7_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T139, T184, T185, T186, T187, T188, T189, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, T140, T190)) → U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_in_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309))
U8_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309, balance55C_out_gaaaaaaaaaga(T141, T186, T187, X305, X306, X307, X308, T188, T189, T190, T152, X309)) → pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, T184, T185, T186, T187, T188, T189, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, T190, T141, X305, X306, X307, X308, T152, X309)
U4_gaaaaaaaaaaaaga(T139, T140, T141, X303, X304, X305, X306, X307, X308, T157, T158, T160, T154, T161, T156, T155, T159, T153, T152, X309, pH_out_gaaaaaaaaaaaaaaagagaaaaga(T139, X303, X304, X298, X299, X300, X301, T155, T156, T157, T154, T158, T159, T160, T161, T153, T140, X302, T141, X305, X306, X307, X308, T152, X309)) → balance55G_out_gaaaaaaaaaaaaga(tree(T139, T140, T141), X303, X304, X305, X306, X307, X308, tree(T157, T158, T160), T154, T161, T156, T155, .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)), T152, X309)
U5_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55G_out_gaaaaaaaaaaaaga(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54)) → U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_in_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54))
balance55E_in_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], []) → balance55E_out_gaaaaaaa(nil, T415, [], T417, T418, .(','(nil, -(T417, T417)), T418), [], [])
balance55E_in_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_in_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473))
pF_in_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U11_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_in_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497))
U12_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55E_out_gaaaaaaa(T454, T493, T494, T498, T499, T495, T496, T497)) → pF_out_gaaaaaaaaagagaa(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499)
U3_gaaaaaaa(T452, T453, T454, T468, T469, T474, T473, T459, T460, T461, T462, T463, T470, T465, T471, T472, pF_out_gaaaaaaaaagagaa(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)) → balance55E_out_gaaaaaaa(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472)
U6_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22, balance55E_out_gaaaaaaa(T22, T50, T51, T48, T49, T52, T53, T54)) → pB_out_gaaaaaaaaaaaagag(T20, T48, T49, T50, T51, T52, T53, T28, T27, T29, T30, T31, T26, T21, T54, T22)
U1_ga(T20, T21, T22, T28, T29, T31, pB_out_gaaaaaaaaaaaagag(T20, X120, X121, X115, X116, X117, X118, T28, T27, T29, T30, T31, T26, T21, X119, T22)) → balanceA_out_ga(tree(T20, T21, T22), tree(T28, T29, T31))

(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_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499) → U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_in_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497))
U11_GAAAAAAAAAGAGAA(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497, T454, T498, T499, balance55C_out_gaaaaaaaaaga(T452, T468, T469, T493, T494, T495, T496, T470, T471, T472, T453, T497)) → BALANCE55E_IN_GAAAAAAA(T454, T493, T494, T498, T499, T495, T496, T497)
BALANCE55E_IN_GAAAAAAA(tree(T452, T453, T454), T468, T469, T474, T473, .(','(tree(T459, T460, T461), -(T462, T463)), T470), .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)), T472) → PF_IN_GAAAAAAAAAGAGAA(T452, T468, T469, X618, X619, X620, X621, T470, T471, T472, T453, X622, T454, T474, T473)

The TRS R consists of the following rules:

balance55C_in_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275) → balance55C_out_gaaaaaaaaaga(nil, T267, .(','(nil, -(T269, T269)), T270), T269, T270, T271, T272, T271, T272, .(T274, T275), T274, T275)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481) → U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481))
U2_gaaaaaaaaaga(T306, T307, T308, T321, T322, X477, X478, X479, X480, T311, T312, T313, T314, T315, T323, T317, T324, T325, T320, X481, pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, X472, X473, X474, X475, T323, T324, T325, T307, X476, T308, X477, X478, X479, X480, T320, X481)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T321, T322, X477, X478, X479, X480, .(','(tree(T311, T312, T313), -(T314, T315)), T323), .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)), T325, T320, X481)
pD_in_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481) → U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348))
U9_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348)) → U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_in_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481))
U10_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481, balance55C_out_gaaaaaaaaaga(T308, T344, T345, X477, X478, X479, X480, T346, T347, T348, T320, X481)) → pD_out_gaaaaaaaaagagaaaaga(T306, T321, T322, T344, T345, T346, T347, T323, T324, T325, T307, T348, T308, X477, X478, X479, X480, T320, X481)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balance55C_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance55C_in_gaaaaaaaaaga(x1, x11)
balance55C_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = balance55C_out_gaaaaaaaaaga(x1, x11)
U2_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U2_gaaaaaaaaaga(x1, x2, x3, x19, x21)
pD_in_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = pD_in_gaaaaaaaaagagaaaaga(x1, x11, x13, x18)
U9_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U9_gaaaaaaaaagagaaaaga(x1, x11, x13, x18, x20)
U10_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20) = U10_gaaaaaaaaagagaaaaga(x1, x11, x13, x18, x20)
pD_out_gaaaaaaaaagagaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = pD_out_gaaaaaaaaagagaaaaga(x1, x11, x13, x18)
BALANCE55E_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = BALANCE55E_IN_GAAAAAAA(x1)
PF_IN_GAAAAAAAAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = PF_IN_GAAAAAAAAAGAGAA(x1, x11, x13)
U11_GAAAAAAAAAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U11_GAAAAAAAAAGAGAA(x1, x11, x13, x16)

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_GAAAAAAAAAGAGAA(T452, T453, T454) → U11_GAAAAAAAAAGAGAA(T452, T453, T454, balance55C_in_gaaaaaaaaaga(T452, T453))
U11_GAAAAAAAAAGAGAA(T452, T453, T454, balance55C_out_gaaaaaaaaaga(T452, T453)) → BALANCE55E_IN_GAAAAAAA(T454)
BALANCE55E_IN_GAAAAAAA(tree(T452, T453, T454)) → PF_IN_GAAAAAAAAAGAGAA(T452, T453, T454)

The TRS R consists of the following rules:

balance55C_in_gaaaaaaaaaga(nil, T274) → balance55C_out_gaaaaaaaaaga(nil, T274)
balance55C_in_gaaaaaaaaaga(tree(T306, T307, T308), T320) → U2_gaaaaaaaaaga(T306, T307, T308, T320, pD_in_gaaaaaaaaagagaaaaga(T306, T307, T308, T320))
U2_gaaaaaaaaaga(T306, T307, T308, T320, pD_out_gaaaaaaaaagagaaaaga(T306, T307, T308, T320)) → balance55C_out_gaaaaaaaaaga(tree(T306, T307, T308), T320)
pD_in_gaaaaaaaaagagaaaaga(T306, T307, T308, T320) → U9_gaaaaaaaaagagaaaaga(T306, T307, T308, T320, balance55C_in_gaaaaaaaaaga(T306, T307))
U9_gaaaaaaaaagagaaaaga(T306, T307, T308, T320, balance55C_out_gaaaaaaaaaga(T306, T307)) → U10_gaaaaaaaaagagaaaaga(T306, T307, T308, T320, balance55C_in_gaaaaaaaaaga(T308, T320))
U10_gaaaaaaaaagagaaaaga(T306, T307, T308, T320, balance55C_out_gaaaaaaaaaga(T308, T320)) → pD_out_gaaaaaaaaagagaaaaga(T306, T307, T308, T320)

The set Q consists of the following terms:

balance55C_in_gaaaaaaaaaga(x0, x1)
U2_gaaaaaaaaaga(x0, x1, x2, x3, x4)
pD_in_gaaaaaaaaagagaaaaga(x0, x1, x2, x3)
U9_gaaaaaaaaagagaaaaga(x0, x1, x2, x3, x4)
U10_gaaaaaaaaagagaaaaga(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_GAAAAAAAAAGAGAA(T452, T453, T454, balance55C_out_gaaaaaaaaaga(T452, T453)) → BALANCE55E_IN_GAAAAAAA(T454)
The graph contains the following edges 3 >= 1
BALANCE55E_IN_GAAAAAAA(tree(T452, T453, T454)) → PF_IN_GAAAAAAAAAGAGAA(T452, T453, T454)
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3
PF_IN_GAAAAAAAAAGAGAA(T452, T453, T454) → U11_GAAAAAAAAAGAGAA(T452, T453, T454, balance55C_in_gaaaaaaaaaga(T452, T453))
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