Left Termination proof of /tmp/tmpQwuKz2/balance

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

    ↳3 PrologToPiTRSProof (⇐)

        ↳4 PiTRS

        ↳5 DependencyPairsProof (⇔)

        ↳6 PiDP

        ↳7 DependencyGraphProof (⇔)

        ↳8 AND

            ↳9 PiDP

                ↳10 UsableRulesProof (⇔)

                ↳11 PiDP

                ↳12 PiDPToQDPProof (⇐)

                ↳13 QDP

                ↳14 Narrowing (⇐)

                ↳15 QDP

                ↳16 NonTerminationProof (⇔)

                ↳17 NO

            ↳18 PiDP

                ↳19 UsableRulesProof (⇔)

                ↳20 PiDP

                ↳21 PiDPToQDPProof (⇐)

                ↳22 QDP

                ↳23 Narrowing (⇐)

                ↳24 QDP

                ↳25 NonTerminationProof (⇔)

                ↳26 NO

    ↳27 PrologToPiTRSProof (⇐)

        ↳28 PiTRS

        ↳29 DependencyPairsProof (⇔)

        ↳30 PiDP

        ↳31 DependencyGraphProof (⇔)

        ↳32 AND

            ↳33 PiDP

                ↳34 UsableRulesProof (⇔)

                ↳35 PiDP

                ↳36 PiDPToQDPProof (⇐)

                ↳37 QDP

                ↳38 Narrowing (⇐)

                ↳39 QDP

                ↳40 NonTerminationProof (⇔)

                ↳41 NO

            ↳42 PiDP

                ↳43 UsableRulesProof (⇔)

                ↳44 PiDP

                ↳45 PiDPToQDPProof (⇐)

                ↳46 QDP

                ↳47 Narrowing (⇐)

                ↳48 QDP

                ↳49 NonTerminationProof (⇔)

                ↳50 NO

(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(a,g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

balance23(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264).
balance23(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) :- balance23(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432).
balance23(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) :- ','(balance23(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332), balance23(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)).
balance13(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])).
balance13(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) :- balance23(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582).
balance13(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) :- ','(balance23(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465), balance13(T466, T462, T463, T464, T467, T465)).
balance12(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201).
balance12(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) :- balance23(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275).
balance12(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) :- ','(balance23(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191), balance23(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)).
balance1(nil, nil).
balance1(tree(T31, T33, T36), tree(T28, T29, T30)) :- balance12(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116).
balance1(tree(T31, T33, T58), tree(T28, T29, T30)) :- ','(balance12(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57), balance13(T58, T53, T54, T55, T56, T57)).

Queries:

balance1(a,g).

(3) PrologToPiTRSProof (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: (f,b)
balance12_in: (f,f,f,f,b,b,f,b,f,f,f,f,f)
balance23_in: (f,f,f,f,f,f,f,f,f,f)
balance13_in: (f,f,f,f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

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

BALANCE1_IN_AG(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_AG(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
BALANCE1_IN_AG(tree(T31, T33, T36), tree(T28, T29, T30)) → BALANCE12_IN_AAAAGGAGAAAAA(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_AAAAGGAGAAAAA(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → BALANCE23_IN_AAAAAAAAAA(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_AAAAAAAAAA(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → BALANCE23_IN_AAAAAAAAAA(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_AG(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_AG(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_AG(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_AG(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
U11_AG(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → BALANCE13_IN_AAAAAA(T58, T53, T54, T55, T56, T57)
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_AAAAAA(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → BALANCE23_IN_AAAAAAAAAA(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)
BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

The argument filtering Pi contains the following mapping:
balance1_in_ag(x1, x2) = balance1_in_ag(x2)
nil = nil
balance1_out_ag(x1, x2) = balance1_out_ag(x2)
tree(x1, x2, x3) = tree(x1, x2, x3)
U10_ag(x1, x2, x3, x4, x5, x6, x7) = U10_ag(x4, x5, x6, x7)
balance12_in_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balance12_in_aaaaggagaaaaa(x5, x6, x8)
balance12_out_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balance12_out_aaaaggagaaaaa(x5, x6, x8)
U7_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U7_aaaaggagaaaaa(x7, x8, x9, x10, x12, x19)
balance23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_in_aaaaaaaaaa
balance23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_out_aaaaaaaaaa
U1_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_aaaaaaaaaa(x19)
U2_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_aaaaaaaaaa(x19)
U3_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_aaaaaaaaaa(x19)
U8_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U8_aaaaggagaaaaa(x7, x8, x9, x10, x12, x19)
U9_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_aaaaggagaaaaa(x7, x8, x9, x10, x12, x19)
U11_ag(x1, x2, x3, x4, x5, x6, x7) = U11_ag(x4, x5, x6, x7)
U12_ag(x1, x2, x3, x4, x5, x6, x7) = U12_ag(x4, x5, x6, x7)
balance13_in_aaaaaa(x1, x2, x3, x4, x5, x6) = balance13_in_aaaaaa
balance13_out_aaaaaa(x1, x2, x3, x4, x5, x6) = balance13_out_aaaaaa
U4_aaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U4_aaaaaa(x15)
U5_aaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_aaaaaa(x15)
U6_aaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_aaaaaa(x15)
BALANCE1_IN_AG(x1, x2) = BALANCE1_IN_AG(x2)
U10_AG(x1, x2, x3, x4, x5, x6, x7) = U10_AG(x4, x5, x6, x7)
BALANCE12_IN_AAAAGGAGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = BALANCE12_IN_AAAAGGAGAAAAA(x5, x6, x8)
U7_AAAAGGAGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U7_AAAAGGAGAAAAA(x7, x8, x9, x10, x12, x19)
BALANCE23_IN_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCE23_IN_AAAAAAAAAA
U1_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_AAAAAAAAAA(x19)
U2_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_AAAAAAAAAA(x19)
U3_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_AAAAAAAAAA(x19)
U8_AAAAGGAGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U8_AAAAGGAGAAAAA(x7, x8, x9, x10, x12, x19)
U9_AAAAGGAGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_AAAAGGAGAAAAA(x7, x8, x9, x10, x12, x19)
U11_AG(x1, x2, x3, x4, x5, x6, x7) = U11_AG(x4, x5, x6, x7)
U12_AG(x1, x2, x3, x4, x5, x6, x7) = U12_AG(x4, x5, x6, x7)
BALANCE13_IN_AAAAAA(x1, x2, x3, x4, x5, x6) = BALANCE13_IN_AAAAAA
U4_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U4_AAAAAA(x15)
U5_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_AAAAAA(x15)
U6_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_AAAAAA(x15)

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

(6) Obligation:

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

BALANCE1_IN_AG(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_AG(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
BALANCE1_IN_AG(tree(T31, T33, T36), tree(T28, T29, T30)) → BALANCE12_IN_AAAAGGAGAAAAA(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_AAAAGGAGAAAAA(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → BALANCE23_IN_AAAAAAAAAA(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_AAAAAAAAAA(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → BALANCE23_IN_AAAAAAAAAA(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_AG(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_AG(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_AG(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_AG(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
U11_AG(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → BALANCE13_IN_AAAAAA(T58, T53, T54, T55, T56, T57)
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_AAAAAA(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → BALANCE23_IN_AAAAAAAAAA(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)
BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)

The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balance23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_in_aaaaaaaaaa
balance23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_out_aaaaaaaaaa
U1_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_aaaaaaaaaa(x19)
U2_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_aaaaaaaaaa(x19)
U3_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_aaaaaaaaaa(x19)
BALANCE23_IN_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCE23_IN_AAAAAAAAAA
U2_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_AAAAAAAAAA(x19)

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balance23_in_aaaaaaaaaa)
U2_AAAAAAAAAA(balance23_out_aaaaaaaaaa) → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → BALANCE23_IN_AAAAAAAAAA

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa → balance23_out_aaaaaaaaaa
balance23_in_aaaaaaaaaa → U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
balance23_in_aaaaaaaaaa → U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U1_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa
U2_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → U3_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U3_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa

The set Q consists of the following terms:

balance23_in_aaaaaaaaaa
U1_aaaaaaaaaa(x0)
U2_aaaaaaaaaa(x0)
U3_aaaaaaaaaa(x0)

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

(14) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balance23_in_aaaaaaaaaa) at position [0] we obtained the following new rules [LPAR04]:

BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balance23_out_aaaaaaaaaa)
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa))
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa))

(15) Obligation:

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

U2_AAAAAAAAAA(balance23_out_aaaaaaaaaa) → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balance23_out_aaaaaaaaaa)
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa))
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa))

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa → balance23_out_aaaaaaaaaa
balance23_in_aaaaaaaaaa → U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
balance23_in_aaaaaaaaaa → U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U1_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa
U2_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → U3_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U3_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa

The set Q consists of the following terms:

balance23_in_aaaaaaaaaa
U1_aaaaaaaaaa(x0)
U2_aaaaaaaaaa(x0)
U3_aaaaaaaaaa(x0)

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

(16) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = BALANCE23_IN_AAAAAAAAAA evaluates to t =BALANCE23_IN_AAAAAAAAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from BALANCE23_IN_AAAAAAAAAA to BALANCE23_IN_AAAAAAAAAA.

(17) NO

(18) Obligation:

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

BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

(19) UsableRulesProof (EQUIVALENT transformation)

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

(20) Obligation:

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

BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balance23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_in_aaaaaaaaaa
balance23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_out_aaaaaaaaaa
U1_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_aaaaaaaaaa(x19)
U2_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_aaaaaaaaaa(x19)
U3_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_aaaaaaaaaa(x19)
BALANCE13_IN_AAAAAA(x1, x2, x3, x4, x5, x6) = BALANCE13_IN_AAAAAA
U5_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_AAAAAA(x15)

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

(21) PiDPToQDPProof (SOUND transformation)

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

(22) Obligation:

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

BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_in_aaaaaaaaaa)
U5_AAAAAA(balance23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa → balance23_out_aaaaaaaaaa
balance23_in_aaaaaaaaaa → U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
balance23_in_aaaaaaaaaa → U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U1_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa
U2_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → U3_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U3_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa

The set Q consists of the following terms:

balance23_in_aaaaaaaaaa
U1_aaaaaaaaaa(x0)
U2_aaaaaaaaaa(x0)
U3_aaaaaaaaaa(x0)

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

(23) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_in_aaaaaaaaaa) at position [0] we obtained the following new rules [LPAR04]:

BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_out_aaaaaaaaaa)
BALANCE13_IN_AAAAAA → U5_AAAAAA(U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa))
BALANCE13_IN_AAAAAA → U5_AAAAAA(U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa))

(24) Obligation:

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

U5_AAAAAA(balance23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA
BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_out_aaaaaaaaaa)
BALANCE13_IN_AAAAAA → U5_AAAAAA(U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa))
BALANCE13_IN_AAAAAA → U5_AAAAAA(U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa))

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa → balance23_out_aaaaaaaaaa
balance23_in_aaaaaaaaaa → U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
balance23_in_aaaaaaaaaa → U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U1_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa
U2_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → U3_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U3_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa

The set Q consists of the following terms:

balance23_in_aaaaaaaaaa
U1_aaaaaaaaaa(x0)
U2_aaaaaaaaaa(x0)
U3_aaaaaaaaaa(x0)

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

(25) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = BALANCE13_IN_AAAAAA evaluates to t =BALANCE13_IN_AAAAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_out_aaaaaaaaaa)
with rule BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_out_aaaaaaaaaa) at position [] and matcher [ ]

U5_AAAAAA(balance23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA
with rule U5_AAAAAA(balance23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

(26) NO

(27) PrologToPiTRSProof (SOUND transformation)

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(28) Obligation:

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

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

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

BALANCE1_IN_AG(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_AG(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
BALANCE1_IN_AG(tree(T31, T33, T36), tree(T28, T29, T30)) → BALANCE12_IN_AAAAGGAGAAAAA(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_AAAAGGAGAAAAA(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → BALANCE23_IN_AAAAAAAAAA(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_AAAAAAAAAA(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → BALANCE23_IN_AAAAAAAAAA(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_AG(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_AG(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_AG(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_AG(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
U11_AG(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → BALANCE13_IN_AAAAAA(T58, T53, T54, T55, T56, T57)
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_AAAAAA(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → BALANCE23_IN_AAAAAAAAAA(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)
BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

The argument filtering Pi contains the following mapping:
balance1_in_ag(x1, x2) = balance1_in_ag(x2)
nil = nil
balance1_out_ag(x1, x2) = balance1_out_ag
tree(x1, x2, x3) = tree(x1, x2, x3)
U10_ag(x1, x2, x3, x4, x5, x6, x7) = U10_ag(x7)
balance12_in_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balance12_in_aaaaggagaaaaa(x5, x6, x8)
balance12_out_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = balance12_out_aaaaggagaaaaa
U7_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U7_aaaaggagaaaaa(x19)
balance23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_in_aaaaaaaaaa
balance23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_out_aaaaaaaaaa
U1_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_aaaaaaaaaa(x19)
U2_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_aaaaaaaaaa(x19)
U3_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_aaaaaaaaaa(x19)
U8_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U8_aaaaggagaaaaa(x19)
U9_aaaaggagaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_aaaaggagaaaaa(x19)
U11_ag(x1, x2, x3, x4, x5, x6, x7) = U11_ag(x7)
U12_ag(x1, x2, x3, x4, x5, x6, x7) = U12_ag(x7)
balance13_in_aaaaaa(x1, x2, x3, x4, x5, x6) = balance13_in_aaaaaa
balance13_out_aaaaaa(x1, x2, x3, x4, x5, x6) = balance13_out_aaaaaa
U4_aaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U4_aaaaaa(x15)
U5_aaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_aaaaaa(x15)
U6_aaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_aaaaaa(x15)
BALANCE1_IN_AG(x1, x2) = BALANCE1_IN_AG(x2)
U10_AG(x1, x2, x3, x4, x5, x6, x7) = U10_AG(x7)
BALANCE12_IN_AAAAGGAGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = BALANCE12_IN_AAAAGGAGAAAAA(x5, x6, x8)
U7_AAAAGGAGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U7_AAAAGGAGAAAAA(x19)
BALANCE23_IN_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = BALANCE23_IN_AAAAAAAAAA
U1_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_AAAAAAAAAA(x19)
U2_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_AAAAAAAAAA(x19)
U3_AAAAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_AAAAAAAAAA(x19)
U8_AAAAGGAGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U8_AAAAGGAGAAAAA(x19)
U9_AAAAGGAGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9_AAAAGGAGAAAAA(x19)
U11_AG(x1, x2, x3, x4, x5, x6, x7) = U11_AG(x7)
U12_AG(x1, x2, x3, x4, x5, x6, x7) = U12_AG(x7)
BALANCE13_IN_AAAAAA(x1, x2, x3, x4, x5, x6) = BALANCE13_IN_AAAAAA
U4_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U4_AAAAAA(x15)
U5_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_AAAAAA(x15)
U6_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U6_AAAAAA(x15)

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

(30) Obligation:

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

BALANCE1_IN_AG(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_AG(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
BALANCE1_IN_AG(tree(T31, T33, T36), tree(T28, T29, T30)) → BALANCE12_IN_AAAAGGAGAAAAA(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_AAAAGGAGAAAAA(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → BALANCE23_IN_AAAAAAAAAA(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_AAAAAAAAAA(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE12_IN_AAAAGGAGAAAAA(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U8_AAAAGGAGAAAAA(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → BALANCE23_IN_AAAAAAAAAA(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)
BALANCE1_IN_AG(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_AG(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_AG(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_AG(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
U11_AG(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → BALANCE13_IN_AAAAAA(T58, T53, T54, T55, T56, T57)
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_AAAAAA(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
BALANCE13_IN_AAAAAA(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → BALANCE23_IN_AAAAAAAAAA(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)
BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

(31) DependencyGraphProof (EQUIVALENT transformation)

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

(32) Complex Obligation (AND)

(33) Obligation:

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

BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)

The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

(34) UsableRulesProof (EQUIVALENT transformation)

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

(35) Obligation:

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

BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_AAAAAAAAAA(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → BALANCE23_IN_AAAAAAAAAA(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)
BALANCE23_IN_AAAAAAAAAA(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → BALANCE23_IN_AAAAAAAAAA(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)

(36) PiDPToQDPProof (SOUND transformation)

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

(37) Obligation:

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

BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balance23_in_aaaaaaaaaa)
U2_AAAAAAAAAA(balance23_out_aaaaaaaaaa) → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → BALANCE23_IN_AAAAAAAAAA

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa → balance23_out_aaaaaaaaaa
balance23_in_aaaaaaaaaa → U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
balance23_in_aaaaaaaaaa → U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U1_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa
U2_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → U3_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U3_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa

The set Q consists of the following terms:

balance23_in_aaaaaaaaaa
U1_aaaaaaaaaa(x0)
U2_aaaaaaaaaa(x0)
U3_aaaaaaaaaa(x0)

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

(38) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balance23_in_aaaaaaaaaa) at position [0] we obtained the following new rules [LPAR04]:

BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balance23_out_aaaaaaaaaa)
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa))
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa))

(39) Obligation:

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

U2_AAAAAAAAAA(balance23_out_aaaaaaaaaa) → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → BALANCE23_IN_AAAAAAAAAA
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(balance23_out_aaaaaaaaaa)
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa))
BALANCE23_IN_AAAAAAAAAA → U2_AAAAAAAAAA(U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa))

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa → balance23_out_aaaaaaaaaa
balance23_in_aaaaaaaaaa → U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
balance23_in_aaaaaaaaaa → U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U1_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa
U2_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → U3_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U3_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa

The set Q consists of the following terms:

balance23_in_aaaaaaaaaa
U1_aaaaaaaaaa(x0)
U2_aaaaaaaaaa(x0)
U3_aaaaaaaaaa(x0)

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

(40) NonTerminationProof (EQUIVALENT transformation)

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from BALANCE23_IN_AAAAAAAAAA to BALANCE23_IN_AAAAAAAAAA.

(41) NO

(42) Obligation:

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

BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balance1_in_ag(nil, nil) → balance1_out_ag(nil, nil)
balance1_in_ag(tree(T31, T33, T36), tree(T28, T29, T30)) → U10_ag(T31, T33, T36, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116))
balance12_in_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201) → balance12_out_aaaaggagaaaaa(nil, .(T108, T109), T108, T109, T110, T111, T112, T113, T114, .(','(T110, -(.(T108, T109), .(T111, T112))), .(','(T113, -(T112, [])), T114)), T114, .(','(nil, -(X200, X200)), X201), X201)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280) → U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275))
balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U7_aaaaggagaaaaa(T157, T159, T163, T158, T164, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, X279, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, X272, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, X273, X274, X279, X275)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T163), T158, T164, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, X279, X280)
balance12_in_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280) → U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191))
U8_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T157, T158, T159, T187, .(','(T153, -(T161, [])), .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160))), T160, T188, T189, T190, T191)) → U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_in_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280))
U9_aaaaggagaaaaa(T157, T159, T192, T158, T193, X276, T148, T149, T150, T151, T161, T153, T162, T160, X277, X278, T190, X280, balance23_out_aaaaaaaaaa(T192, T187, T193, X276, T188, T189, X277, X278, T191, X280)) → balance12_out_aaaaggagaaaaa(tree(T157, T159, T192), T158, T193, X276, tree(T148, T149, T150), T151, T161, T153, .(','(T148, -(T158, .(T149, T162))), .(','(T150, -(T162, .(T151, T161))), T160)), X277, X278, T190, X280)
U10_ag(T31, T33, T36, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, X113, T28, T29, T35, T30, T34, X114, X115, X121, X116)) → balance1_out_ag(tree(T31, T33, T36), tree(T28, T29, T30))
balance1_in_ag(tree(T31, T33, T58), tree(T28, T29, T30)) → U11_ag(T31, T33, T58, T28, T29, T30, balance12_in_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57))
U11_ag(T31, T33, T58, T28, T29, T30, balance12_out_aaaaggagaaaaa(T31, T32, T33, T53, T28, T29, T35, T30, T34, T54, T55, T56, T57)) → U12_ag(T31, T33, T58, T28, T29, T30, balance13_in_aaaaaa(T58, T53, T54, T55, T56, T57))
balance13_in_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), [])) → balance13_out_aaaaaa(nil, [], T394, [], T394, .(','(nil, -(T396, T396)), []))
balance13_in_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445) → U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582))
U4_aaaaaa(T440, T442, T446, T441, T430, T431, T432, T433, T434, T443, T436, T444, T447, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, X579, T443, T444, X580, X581, T445, X582)) → balance13_out_aaaaaa(tree(T440, T442, T446), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T447, T445)
balance13_in_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_in_aaaaaa(T466, T462, T463, T464, T467, T465))
U6_aaaaaa(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance13_out_aaaaaa(T466, T462, T463, T464, T467, T465)) → balance13_out_aaaaaa(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445)
U12_ag(T31, T33, T58, T28, T29, T30, balance13_out_aaaaaa(T58, T53, T54, T55, T56, T57)) → balance1_out_ag(tree(T31, T33, T58), tree(T28, T29, T30))

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

BALANCE13_IN_AAAAAA(tree(T440, T442, T466), T441, .(','(tree(T430, T431, T432), -(T433, T434)), T443), .(','(T430, -(T433, .(T431, T436))), .(','(T432, -(T436, T434)), T444)), T467, T445) → U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_in_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465))
U5_AAAAAA(T440, T442, T466, T441, T430, T431, T432, T433, T434, T443, T436, T444, T467, T445, balance23_out_aaaaaaaaaa(T440, T441, T442, T462, T443, T444, T463, T464, T445, T465)) → BALANCE13_IN_AAAAAA(T466, T462, T463, T464, T467, T465)

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264) → balance23_out_aaaaaaaaaa(nil, .(T259, T260), T259, T260, T261, T262, T261, T262, .(','(nil, -(T263, T263)), T264), T264)
balance23_in_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432))
balance23_in_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436) → U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332))
U1_aaaaaaaaaa(T307, T309, T313, T308, T314, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, X429, T310, T311, X430, X431, T312, X432)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T313), T308, T314, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)
U2_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T307, T308, T309, T329, T310, T311, T330, T331, T312, T332)) → U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_in_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436))
U3_aaaaaaaaaa(T307, T309, T333, T308, T334, X433, T298, T299, T300, T301, T302, T310, T304, T311, X434, X435, T312, X436, balance23_out_aaaaaaaaaa(T333, T329, T334, X433, T330, T331, X434, X435, T332, X436)) → balance23_out_aaaaaaaaaa(tree(T307, T309, T333), T308, T334, X433, .(','(tree(T298, T299, T300), -(T301, T302)), T310), .(','(T298, -(T301, .(T299, T304))), .(','(T300, -(T304, T302)), T311)), X434, X435, T312, X436)

The argument filtering Pi contains the following mapping:
nil = nil
tree(x1, x2, x3) = tree(x1, x2, x3)
balance23_in_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_in_aaaaaaaaaa
balance23_out_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = balance23_out_aaaaaaaaaa
U1_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U1_aaaaaaaaaa(x19)
U2_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U2_aaaaaaaaaa(x19)
U3_aaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U3_aaaaaaaaaa(x19)
BALANCE13_IN_AAAAAA(x1, x2, x3, x4, x5, x6) = BALANCE13_IN_AAAAAA
U5_AAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = U5_AAAAAA(x15)

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_in_aaaaaaaaaa)
U5_AAAAAA(balance23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa → balance23_out_aaaaaaaaaa
balance23_in_aaaaaaaaaa → U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
balance23_in_aaaaaaaaaa → U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U1_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa
U2_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → U3_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U3_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa

The set Q consists of the following terms:

balance23_in_aaaaaaaaaa
U1_aaaaaaaaaa(x0)
U2_aaaaaaaaaa(x0)
U3_aaaaaaaaaa(x0)

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

(47) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_in_aaaaaaaaaa) at position [0] we obtained the following new rules [LPAR04]:

BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_out_aaaaaaaaaa)
BALANCE13_IN_AAAAAA → U5_AAAAAA(U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa))
BALANCE13_IN_AAAAAA → U5_AAAAAA(U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa))

(48) Obligation:

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

U5_AAAAAA(balance23_out_aaaaaaaaaa) → BALANCE13_IN_AAAAAA
BALANCE13_IN_AAAAAA → U5_AAAAAA(balance23_out_aaaaaaaaaa)
BALANCE13_IN_AAAAAA → U5_AAAAAA(U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa))
BALANCE13_IN_AAAAAA → U5_AAAAAA(U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa))

The TRS R consists of the following rules:

balance23_in_aaaaaaaaaa → balance23_out_aaaaaaaaaa
balance23_in_aaaaaaaaaa → U1_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
balance23_in_aaaaaaaaaa → U2_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U1_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa
U2_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → U3_aaaaaaaaaa(balance23_in_aaaaaaaaaa)
U3_aaaaaaaaaa(balance23_out_aaaaaaaaaa) → balance23_out_aaaaaaaaaa

The set Q consists of the following terms:

balance23_in_aaaaaaaaaa
U1_aaaaaaaaaa(x0)
U2_aaaaaaaaaa(x0)
U3_aaaaaaaaaa(x0)

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

(49) NonTerminationProof (EQUIVALENT transformation)

Semiunifier: [ ]
Matcher: [ ]

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) Narrowing (SOUND transformation)

(15) Obligation:

(16) NonTerminationProof (EQUIVALENT transformation)

(17) NO

(18) Obligation:

(19) UsableRulesProof (EQUIVALENT transformation)

(20) Obligation:

(21) PiDPToQDPProof (SOUND transformation)

(22) Obligation:

(23) Narrowing (SOUND transformation)

(24) Obligation:

(25) NonTerminationProof (EQUIVALENT transformation)

(26) NO

(27) PrologToPiTRSProof (SOUND transformation)

(28) Obligation:

(29) DependencyPairsProof (EQUIVALENT transformation)

(30) Obligation:

(31) DependencyGraphProof (EQUIVALENT transformation)

(32) Complex Obligation (AND)

(33) Obligation:

(34) UsableRulesProof (EQUIVALENT transformation)

(35) Obligation:

(36) PiDPToQDPProof (SOUND transformation)

(37) Obligation:

(38) Narrowing (SOUND transformation)

(39) Obligation:

(40) NonTerminationProof (EQUIVALENT transformation)

(41) NO

(42) Obligation:

(43) UsableRulesProof (EQUIVALENT transformation)

(44) Obligation:

(45) PiDPToQDPProof (SOUND transformation)

(46) Obligation:

(47) Narrowing (SOUND transformation)

(48) Obligation:

(49) NonTerminationProof (EQUIVALENT transformation)

(50) NO