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

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇐)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇐)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔)
        ↳20 YES

(0) Obligation:

Clauses:

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

Queries:

balance(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

balance23(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) :- balance23(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432).
balance23(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) :- ','(balancec23(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326), balance23(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)).
balance13(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) :- balance23(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582).
balance13(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) :- ','(balancec23(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454), balance13(T420, T451, T452, T453, T455, T454)).
balance1(tree(tree(T142, T143, T144), T146, T27), tree(tree(T160, T161, T163), T164, T158)) :- balance23(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275).
balance1(tree(tree(T142, T143, T144), T146, T27), tree(tree(T160, T161, T163), T164, T158)) :- ','(balancec23(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191), balance23(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)).
balance1(tree(T25, T26, T27), tree(T33, T34, T36)) :- ','(balancec12(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57), balance13(T27, T53, T54, T55, T56, T57)).

Clauses:

balancec23(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262).
balancec23(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) :- ','(balancec23(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326), balancec23(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)).
balancec13(nil, [], T386, [], T386, .(','(nil, -(T388, T388)), [])).
balancec13(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) :- ','(balancec23(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454), balancec13(T420, T451, T452, T453, T455, T454)).
balancec12(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201).
balancec12(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) :- ','(balancec23(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191), balancec23(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)).

Afs:

balance1(x1, x2)  =  balance1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
balance1_in: (b,f)
balance23_in: (b,f,b,f,f,f,f,f,f,f)
balancec23_in: (b,f,b,f,f,f,f,f,f,f)
balancec12_in: (b,f,b,f,f,f,f,f,f,f,f,f,f)
balance13_in: (b,f,f,f,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

BALANCE1_IN_GA(tree(tree(T142, T143, T144), T146, T27), tree(tree(T160, T161, T163), T164, T158)) → U7_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
BALANCE1_IN_GA(tree(tree(T142, T143, T144), T146, T27), tree(tree(T160, T161, T163), T164, T158)) → BALANCE23_IN_GAGAAAAAAA(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → BALANCE23_IN_GAGAAAAAAA(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCE23_IN_GAGAAAAAAA(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)
BALANCE1_IN_GA(tree(tree(T142, T143, T144), T146, T27), tree(tree(T160, T161, T163), T164, T158)) → U8_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balancec23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balancec23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U8_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balancec23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → BALANCE23_IN_GAGAAAAAAA(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_GA(T25, T26, T27, T33, T34, T36, balancec12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U10_GA(T25, T26, T27, T33, T34, T36, balancec12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U11_GA(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
U10_GA(T25, T26, T27, T33, T34, T36, balancec12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → BALANCE13_IN_GAAAAA(T27, T53, T54, T55, T56, T57)
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → BALANCE23_IN_GAGAAAAAAA(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCE13_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balancec23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balancec23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balancec23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balancec23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
balancec12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balancec12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balancec12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U17_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balancec23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U17_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balancec23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U18_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U18_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balancec12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance23_in_gagaaaaaaa(x1, x3)
balancec23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancec23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
balancec12_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_in_gagaaaaaaaaaa(x1, x3)
balancec12_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_out_gagaaaaaaaaaa(x1, x3)
U17_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U18_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_gagaaaaaaaaaa(x1, x2, x3, x5, x23)
balance13_in_gaaaaa(x1, x2, x3, x4, x5, x6)  =  balance13_in_gaaaaa(x1)
BALANCE1_IN_GA(x1, x2)  =  BALANCE1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_GA(x1, x2, x3, x4, x5, x11)
BALANCE23_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE23_IN_GAGAAAAAAA(x1, x3)
U1_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U1_GAGAAAAAAA(x1, x2, x3, x5, x19)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_GAGAAAAAAA(x1, x2, x3, x5, x19)
U3_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U3_GAGAAAAAAA(x1, x2, x3, x5, x19)
U8_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_GA(x1, x2, x3, x4, x5, x11)
U9_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_GA(x1, x2, x3, x4, x5, x11)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x7)
BALANCE13_IN_GAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCE13_IN_GAAAAA(x1)
U4_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U4_GAAAAA(x1, x2, x3, x15)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_GAAAAA(x1, x2, x3, x15)
U6_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U6_GAAAAA(x1, x2, x3, x15)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

BALANCE1_IN_GA(tree(tree(T142, T143, T144), T146, T27), tree(tree(T160, T161, T163), T164, T158)) → U7_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balance23_in_gagaaaaaaa(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275))
BALANCE1_IN_GA(tree(tree(T142, T143, T144), T146, T27), tree(tree(T160, T161, T163), T164, T158)) → BALANCE23_IN_GAGAAAAAAA(T142, T156, T143, X272, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, X273, X274, X279, X275)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U1_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432))
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → BALANCE23_IN_GAGAAAAAAA(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U3_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balance23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCE23_IN_GAGAAAAAAA(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)
BALANCE1_IN_GA(tree(tree(T142, T143, T144), T146, T27), tree(tree(T160, T161, T163), T164, T158)) → U8_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balancec23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U8_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balancec23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U9_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balance23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U8_GA(T142, T143, T144, T146, T27, T160, T161, T163, T164, T158, balancec23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → BALANCE23_IN_GAGAAAAAAA(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_GA(tree(T25, T26, T27), tree(T33, T34, T36)) → U10_GA(T25, T26, T27, T33, T34, T36, balancec12_in_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57))
U10_GA(T25, T26, T27, T33, T34, T36, balancec12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → U11_GA(T25, T26, T27, T33, T34, T36, balance13_in_gaaaaa(T27, T53, T54, T55, T56, T57))
U10_GA(T25, T26, T27, T33, T34, T36, balancec12_out_gagaaaaaaaaaa(T25, T31, T26, T53, T33, T34, T35, T36, T32, T54, T55, T56, T57)) → BALANCE13_IN_GAAAAA(T27, T53, T54, T55, T56, T57)
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → U4_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T436, T435, balance23_in_gagaaaaaaa(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582))
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T436, T435) → BALANCE23_IN_GAGAAAAAAA(T418, T432, T419, X579, T433, T434, X580, X581, T435, X582)
BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → U6_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balance13_in_gaaaaa(T420, T451, T452, T453, T455, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCE13_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balancec23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balancec23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balancec23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balancec23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
balancec12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balancec12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balancec12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U17_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balancec23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U17_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balancec23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U18_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U18_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balancec12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balance23_in_gagaaaaaaa(x1, x3)
balancec23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancec23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
balancec12_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_in_gagaaaaaaaaaa(x1, x3)
balancec12_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_out_gagaaaaaaaaaa(x1, x3)
U17_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U18_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_gagaaaaaaaaaa(x1, x2, x3, x5, x23)
balance13_in_gaaaaa(x1, x2, x3, x4, x5, x6)  =  balance13_in_gaaaaa(x1)
BALANCE1_IN_GA(x1, x2)  =  BALANCE1_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_GA(x1, x2, x3, x4, x5, x11)
BALANCE23_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE23_IN_GAGAAAAAAA(x1, x3)
U1_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U1_GAGAAAAAAA(x1, x2, x3, x5, x19)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_GAGAAAAAAA(x1, x2, x3, x5, x19)
U3_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U3_GAGAAAAAAA(x1, x2, x3, x5, x19)
U8_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_GA(x1, x2, x3, x4, x5, x11)
U9_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_GA(x1, x2, x3, x4, x5, x11)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x7)
BALANCE13_IN_GAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCE13_IN_GAAAAA(x1)
U4_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U4_GAAAAA(x1, x2, x3, x15)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_GAAAAA(x1, x2, x3, x15)
U6_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U6_GAAAAA(x1, x2, x3, x15)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCE23_IN_GAGAAAAAAA(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → BALANCE23_IN_GAGAAAAAAA(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)

The TRS R consists of the following rules:

balancec23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balancec23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balancec23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balancec23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
balancec12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balancec12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balancec12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U17_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balancec23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U17_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balancec23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U18_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U18_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balancec12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancec23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancec23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
balancec12_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_in_gagaaaaaaaaaa(x1, x3)
balancec12_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_out_gagaaaaaaaaaa(x1, x3)
U17_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U18_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_gagaaaaaaaaaa(x1, x2, x3, x5, x23)
BALANCE23_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE23_IN_GAGAAAAAAA(x1, x3)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_GAGAAAAAAA(x1, x2, x3, x5, x19)

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

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

BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U2_GAGAAAAAAA(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → BALANCE23_IN_GAGAAAAAAA(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → BALANCE23_IN_GAGAAAAAAA(T291, T305, T292, X429, T306, T307, X430, X431, T308, X432)

The TRS R consists of the following rules:

balancec23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balancec23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balancec23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balancec23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancec23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancec23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
BALANCE23_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCE23_IN_GAGAAAAAAA(x1, x3)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_GAGAAAAAAA(x1, x2, x3, x5, x19)

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:

BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → U2_GAGAAAAAAA(T291, T292, T293, T295, balancec23_in_gagaaaaaaa(T291, T292))
U2_GAGAAAAAAA(T291, T292, T293, T295, balancec23_out_gagaaaaaaa(T291, T292)) → BALANCE23_IN_GAGAAAAAAA(T293, T295)
BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → BALANCE23_IN_GAGAAAAAAA(T291, T292)

The TRS R consists of the following rules:

balancec23_in_gagaaaaaaa(nil, T257) → balancec23_out_gagaaaaaaa(nil, T257)
balancec23_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U13_gagaaaaaaa(T291, T292, T293, T295, balancec23_in_gagaaaaaaa(T291, T292))
U13_gagaaaaaaa(T291, T292, T293, T295, balancec23_out_gagaaaaaaa(T291, T292)) → U14_gagaaaaaaa(T291, T292, T293, T295, balancec23_in_gagaaaaaaa(T293, T295))
U14_gagaaaaaaa(T291, T292, T293, T295, balancec23_out_gagaaaaaaa(T293, T295)) → balancec23_out_gagaaaaaaa(tree(T291, T292, T293), T295)

The set Q consists of the following terms:

balancec23_in_gagaaaaaaa(x0, x1)
U13_gagaaaaaaa(x0, x1, x2, x3, x4)
U14_gagaaaaaaa(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:

  • U2_GAGAAAAAAA(T291, T292, T293, T295, balancec23_out_gagaaaaaaa(T291, T292)) → BALANCE23_IN_GAGAAAAAAA(T293, T295)
    The graph contains the following edges 3 >= 1, 4 >= 2

  • BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → BALANCE23_IN_GAGAAAAAAA(T291, T292)
    The graph contains the following edges 1 > 1, 1 > 2

  • BALANCE23_IN_GAGAAAAAAA(tree(T291, T292, T293), T295) → U2_GAGAAAAAAA(T291, T292, T293, T295, balancec23_in_gagaaaaaaa(T291, T292))
    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:

BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCE13_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balancec23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balancec23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balancec23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balancec23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)
balancec12_in_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201) → balancec12_out_gagaaaaaaaaaa(nil, .(T107, T108), T107, T108, T109, T110, T111, T112, T113, .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)), T113, .(','(nil, -(X200, X200)), X201), X201)
balancec12_in_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280) → U17_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balancec23_in_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191))
U17_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, balancec23_out_gagaaaaaaa(T142, T156, T143, T187, .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157, T188, T189, T190, T191)) → U18_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_in_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280))
U18_gagaaaaaaaaaa(T142, T143, T144, T156, T146, X276, T160, T161, T163, T164, T159, T158, T162, T157, X277, X278, T190, X280, T187, T188, T189, T191, balancec23_out_gagaaaaaaa(T144, T187, T146, X276, T188, T189, X277, X278, T191, X280)) → balancec12_out_gagaaaaaaaaaa(tree(T142, T143, T144), T156, T146, X276, tree(T160, T161, T163), T164, T159, T158, .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)), X277, X278, T190, X280)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancec23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancec23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
balancec12_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_in_gagaaaaaaaaaa(x1, x3)
balancec12_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancec12_out_gagaaaaaaaaaa(x1, x3)
U17_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U18_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_gagaaaaaaaaaa(x1, x2, x3, x5, x23)
BALANCE13_IN_GAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCE13_IN_GAAAAA(x1)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_GAAAAA(x1, x2, x3, x15)

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

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

BALANCE13_IN_GAAAAA(tree(T418, T419, T420), T432, .(','(tree(T422, T423, T424), -(T425, T426)), T433), .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)), T455, T435) → U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_in_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454))
U5_GAAAAA(T418, T419, T420, T432, T422, T423, T424, T425, T426, T433, T428, T434, T455, T435, balancec23_out_gagaaaaaaa(T418, T432, T419, T451, T433, T434, T452, T453, T435, T454)) → BALANCE13_IN_GAAAAA(T420, T451, T452, T453, T455, T454)

The TRS R consists of the following rules:

balancec23_in_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262) → balancec23_out_gagaaaaaaa(nil, .(T257, T258), T257, T258, T259, T260, T259, T260, .(','(nil, -(T261, T261)), T262), T262)
balancec23_in_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436) → U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_in_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326))
U13_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, balancec23_out_gagaaaaaaa(T291, T305, T292, T323, T306, T307, T324, T325, T308, T326)) → U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_in_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436))
U14_gagaaaaaaa(T291, T292, T293, T305, T295, X433, T296, T297, T298, T299, T300, T306, T302, T307, X434, X435, T308, X436, T323, T324, T325, T326, balancec23_out_gagaaaaaaa(T293, T323, T295, X433, T324, T325, X434, X435, T326, X436)) → balancec23_out_gagaaaaaaa(tree(T291, T292, T293), T305, T295, X433, .(','(tree(T296, T297, T298), -(T299, T300)), T306), .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)), X434, X435, T308, X436)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancec23_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancec23_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancec23_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
BALANCE13_IN_GAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCE13_IN_GAAAAA(x1)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_GAAAAA(x1, x2, x3, x15)

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:

BALANCE13_IN_GAAAAA(tree(T418, T419, T420)) → U5_GAAAAA(T418, T419, T420, balancec23_in_gagaaaaaaa(T418, T419))
U5_GAAAAA(T418, T419, T420, balancec23_out_gagaaaaaaa(T418, T419)) → BALANCE13_IN_GAAAAA(T420)

The TRS R consists of the following rules:

balancec23_in_gagaaaaaaa(nil, T257) → balancec23_out_gagaaaaaaa(nil, T257)
balancec23_in_gagaaaaaaa(tree(T291, T292, T293), T295) → U13_gagaaaaaaa(T291, T292, T293, T295, balancec23_in_gagaaaaaaa(T291, T292))
U13_gagaaaaaaa(T291, T292, T293, T295, balancec23_out_gagaaaaaaa(T291, T292)) → U14_gagaaaaaaa(T291, T292, T293, T295, balancec23_in_gagaaaaaaa(T293, T295))
U14_gagaaaaaaa(T291, T292, T293, T295, balancec23_out_gagaaaaaaa(T293, T295)) → balancec23_out_gagaaaaaaa(tree(T291, T292, T293), T295)

The set Q consists of the following terms:

balancec23_in_gagaaaaaaa(x0, x1)
U13_gagaaaaaaa(x0, x1, x2, x3, x4)
U14_gagaaaaaaa(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:

  • U5_GAAAAA(T418, T419, T420, balancec23_out_gagaaaaaaa(T418, T419)) → BALANCE13_IN_GAAAAA(T420)
    The graph contains the following edges 3 >= 1

  • BALANCE13_IN_GAAAAA(tree(T418, T419, T420)) → U5_GAAAAA(T418, T419, T420, balancec23_in_gagaaaaaaa(T418, T419))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

(20) YES