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

(0) Obligation:

Clauses:

minus(X, Y, Z) :- ','(=(X, 0), ','(!, =(Z, 0))).
minus(X, Y, Z) :- ','(=(Y, 0), ','(!, =(Z, X))).
minus(X, Y, Z) :- ','(=(X, s(A)), ','(=(Y, s(B)), minus(A, B, Z))).
div(X, Y, Z) :- ','(=(Y, 0), ','(!, fail)).
div(X, Y, Z) :- ','(=(X, 0), ','(!, =(Z, 0))).
div(X, Y, Z) :- ','(minus(X, Y, U), ','(div(U, Y, V), =(Z, s(V)))).
=(X, X).

Query: div(g,g,a)

(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

minus(X, Y, Z) :- ','(user_defined_=(X, 0), ','(!, user_defined_=(Z, 0))).
minus(X, Y, Z) :- ','(user_defined_=(Y, 0), ','(!, user_defined_=(Z, X))).
minus(X, Y, Z) :- ','(user_defined_=(X, s(A)), ','(user_defined_=(Y, s(B)), minus(A, B, Z))).
div(X, Y, Z) :- ','(user_defined_=(Y, 0), ','(!, fail)).
div(X, Y, Z) :- ','(user_defined_=(X, 0), ','(!, user_defined_=(Z, 0))).
div(X, Y, Z) :- ','(minus(X, Y, U), ','(div(U, Y, V), user_defined_=(Z, s(V)))).
user_defined_=(X, X).

Query: div(g,g,a)

(3) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: div(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: div(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 4 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(user_defined_=(T8, 0), ','(!_1, fail)) | div(T7, T8, T3), SCOPE: 1, CLAUSE: 4 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(user_defined_=(T8, 0), ','(!_1, fail)), SCOPE: 2, CLAUSE: 6 | ?_2 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 4 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(!_1, fail) | ?_2 | div(T7, 0, T3), SCOPE: 1, CLAUSE: 4 | div(T7, 0, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ?_2 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 4 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground\nT8 is ground\nX9 is free\nuser_defined_=(T8, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: fail\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: div(T7, T8, T3), SCOPE: 1, CLAUSE: 4 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground\nT8 is ground\nX9 is free\nuser_defined_=(T8, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(user_defined_=(T20, 0), ','(!_1, user_defined_=(T23, 0))) | div(T20, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT20 is ground\nT21 is ground\nX9 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(user_defined_=(T20, 0), ','(!_1, user_defined_=(T23, 0))), SCOPE: 3, CLAUSE: 6 | ?_3 | div(T20, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT20 is ground\nT21 is ground\nX9 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(!_1, user_defined_=(T23, 0)) | ?_3 | div(0, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT21 is ground\nX9 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ?_3 | div(T20, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT20 is ground\nT21 is ground\nX9 is free\nX21 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T20, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: user_defined_=(T23, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: user_defined_=(T23, 0), SCOPE: 4, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: div(T20, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT20 is ground\nT21 is ground\nX9 is free\nX21 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T20, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="B: ','(minus(T39, T40, X40), ','(div(X40, T40, X41), user_defined_=(T42, s(X41))))\n\nT39 is ground\nT40 is ground\nX9 is free\nX21 is free\nX40 is free\nX41 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T39, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="D: minus(T39, T40, X40)\n\nT39 is ground\nT40 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T39, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="I: ','(div(T45, T40, X41), user_defined_=(T42, s(X41)))\n\nT40 is ground\nT45 is ground\nX9 is free\nX41 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: minus(T39, T40, X40), SCOPE: 5, CLAUSE: 0 | minus(T39, T40, X40), SCOPE: 5, CLAUSE: 1 | minus(T39, T40, X40), SCOPE: 5, CLAUSE: 2\n\nT39 is ground\nT40 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T39, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(user_defined_=(T52, 0), ','(!_5, user_defined_=(X61, 0))) | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 1 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 2\n\nT52 is ground\nT53 is ground\nX9 is free\nX21 is free\nX40 is free\nX61 is free\nuser_defined_=(T53, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T52, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(user_defined_=(T52, 0), ','(!_5, user_defined_=(X61, 0))), SCOPE: 6, CLAUSE: 6 | ?_6 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 1 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 2\n\nT52 is ground\nT53 is ground\nX9 is free\nX21 is free\nX40 is free\nX61 is free\nuser_defined_=(T53, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T52, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ?_6 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 1 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 2\n\nT52 is ground\nT53 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T53, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T52, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: minus(T52, T53, X40), SCOPE: 5, CLAUSE: 1 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 2\n\nT52 is ground\nT53 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T53, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T52, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(user_defined_=(T60, 0), ','(!_5, user_defined_=(X74, T59))) | minus(T59, T60, X40), SCOPE: 5, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nX9 is free\nX21 is free\nX40 is free\nX74 is free\nuser_defined_=(T60, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T59, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(user_defined_=(T60, 0), ','(!_5, user_defined_=(X74, T59))), SCOPE: 7, CLAUSE: 6 | ?_7 | minus(T59, T60, X40), SCOPE: 5, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nX9 is free\nX21 is free\nX40 is free\nX74 is free\nuser_defined_=(T60, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T59, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ?_7 | minus(T59, T60, X40), SCOPE: 5, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T60, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T59, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: minus(T59, T60, X40), SCOPE: 5, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T60, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T59, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(user_defined_=(T66, s(X95)), ','(user_defined_=(T67, s(X96)), minus(X95, X96, X97)))\n\nT66 is ground\nT67 is ground\nX9 is free\nX21 is free\nX97 is free\nX95 is free\nX96 is free\nuser_defined_=(T67, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T66, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(user_defined_=(T66, s(X95)), ','(user_defined_=(T67, s(X96)), minus(X95, X96, X97))), SCOPE: 8, CLAUSE: 6\n\nT66 is ground\nT67 is ground\nX9 is free\nX21 is free\nX97 is free\nX95 is free\nX96 is free\nuser_defined_=(T67, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T66, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(user_defined_=(T67, s(X96)), minus(T73, X96, X97))\n\nT67 is ground\nT73 is ground\nX9 is free\nX97 is free\nX96 is free\nuser_defined_=(T67, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(user_defined_=(T67, s(X96)), minus(T73, X96, X97)), SCOPE: 9, CLAUSE: 6\n\nT67 is ground\nT73 is ground\nX9 is free\nX97 is free\nX96 is free\nuser_defined_=(T67, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="C: minus(T73, T80, X97)\n\nT73 is ground\nT80 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: minus(T73, T80, X97), SCOPE: 10, CLAUSE: 0 | minus(T73, T80, X97), SCOPE: 10, CLAUSE: 1 | minus(T73, T80, X97), SCOPE: 10, CLAUSE: 2\n\nT73 is ground\nT80 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(user_defined_=(T87, 0), ','(!_10, user_defined_=(X130, 0))) | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT87 is ground\nT88 is ground\nX97 is free\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(user_defined_=(T87, 0), ','(!_10, user_defined_=(X130, 0))), SCOPE: 11, CLAUSE: 6 | ?_11 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT87 is ground\nT88 is ground\nX97 is free\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(!_10, user_defined_=(X130, 0)) | ?_11 | minus(0, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(0, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT88 is ground\nX97 is free\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ?_11 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT87 is ground\nT88 is ground\nX97 is free\nX133 is free\nuser_defined_=(T87, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: user_defined_=(X130, 0)\n\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: user_defined_=(X130, 0), SCOPE: 12, CLAUSE: 6\n\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: minus(T87, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT87 is ground\nT88 is ground\nX97 is free\nX133 is free\nuser_defined_=(T87, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(user_defined_=(T97, 0), ','(!_10, user_defined_=(X151, T96))) | minus(T96, T97, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nT97 is ground\nX97 is free\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(user_defined_=(T97, 0), ','(!_10, user_defined_=(X151, T96))), SCOPE: 13, CLAUSE: 6 | ?_13 | minus(T96, T97, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nT97 is ground\nX97 is free\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(!_10, user_defined_=(X151, T96)) | ?_13 | minus(T96, 0, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nX97 is free\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ?_13 | minus(T96, T97, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nT97 is ground\nX97 is free\nX133 is free\nX154 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)\nuser_defined_=(T97, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: user_defined_=(X151, T96)\n\nT96 is ground\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: user_defined_=(X151, T96), SCOPE: 14, CLAUSE: 6\n\nT96 is ground\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: minus(T96, T97, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nT97 is ground\nX97 is free\nX133 is free\nX154 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)\nuser_defined_=(T97, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(user_defined_=(T108, s(X180)), ','(user_defined_=(T109, s(X181)), minus(X180, X181, X182)))\n\nT108 is ground\nT109 is ground\nX133 is free\nX154 is free\nX182 is free\nX180 is free\nX181 is free\nuser_defined_=(T108, 0) !=? user_defined_=(X133, X133)\nuser_defined_=(T109, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(user_defined_=(T108, s(X180)), ','(user_defined_=(T109, s(X181)), minus(X180, X181, X182))), SCOPE: 15, CLAUSE: 6\n\nT108 is ground\nT109 is ground\nX133 is free\nX154 is free\nX182 is free\nX180 is free\nX181 is free\nuser_defined_=(T108, 0) !=? user_defined_=(X133, X133)\nuser_defined_=(T109, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(user_defined_=(T109, s(X181)), minus(T115, X181, X182))\n\nT109 is ground\nT115 is ground\nX154 is free\nX182 is free\nX181 is free\nuser_defined_=(T109, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(user_defined_=(T109, s(X181)), minus(T115, X181, X182)), SCOPE: 16, CLAUSE: 6\n\nT109 is ground\nT115 is ground\nX154 is free\nX182 is free\nX181 is free\nuser_defined_=(T109, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: minus(T115, T122, X182)\n\nT115 is ground\nT122 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="E: div(T45, T40, X41)\n\nT40 is ground\nT45 is ground\nX9 is free\nX41 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="G: user_defined_=(T42, s(T127))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: div(T45, T40, X41), SCOPE: 17, CLAUSE: 3 | div(T45, T40, X41), SCOPE: 17, CLAUSE: 4 | div(T45, T40, X41), SCOPE: 17, CLAUSE: 5\n\nT40 is ground\nT45 is ground\nX9 is free\nX41 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ','(user_defined_=(T135, 0), ','(!_17, fail)) | div(T134, T135, X41), SCOPE: 17, CLAUSE: 4 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 5\n\nT134 is ground\nT135 is ground\nX9 is free\nX41 is free\nuser_defined_=(T135, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(user_defined_=(T135, 0), ','(!_17, fail)), SCOPE: 18, CLAUSE: 6 | ?_18 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 4 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 5\n\nT134 is ground\nT135 is ground\nX9 is free\nX41 is free\nuser_defined_=(T135, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ?_18 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 4 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 5\n\nT134 is ground\nT135 is ground\nX9 is free\nX41 is free\nuser_defined_=(T135, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: div(T134, T135, X41), SCOPE: 17, CLAUSE: 4 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 5\n\nT134 is ground\nT135 is ground\nX9 is free\nX41 is free\nuser_defined_=(T135, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(user_defined_=(T141, 0), ','(!_17, user_defined_=(X236, 0))) | div(T141, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT141 is ground\nT142 is ground\nX9 is free\nX41 is free\nX236 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(user_defined_=(T141, 0), ','(!_17, user_defined_=(X236, 0))), SCOPE: 19, CLAUSE: 6 | ?_19 | div(T141, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT141 is ground\nT142 is ground\nX9 is free\nX41 is free\nX236 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(!_17, user_defined_=(X236, 0)) | ?_19 | div(0, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT142 is ground\nX9 is free\nX41 is free\nX236 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ?_19 | div(T141, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT141 is ground\nT142 is ground\nX9 is free\nX41 is free\nX239 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T141, 0) !=? user_defined_=(X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: user_defined_=(X236, 0)\n\nX236 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: user_defined_=(X236, 0), SCOPE: 20, CLAUSE: 6\n\nX236 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: div(T141, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT141 is ground\nT142 is ground\nX9 is free\nX41 is free\nX239 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T141, 0) !=? user_defined_=(X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="F: ','(minus(T152, T153, X263), ','(div(X263, T153, X264), user_defined_=(X265, s(X264))))\n\nT152 is ground\nT153 is ground\nX9 is free\nX239 is free\nX265 is free\nX263 is free\nX264 is free\nuser_defined_=(T153, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T152, 0) !=? user_defined_=(X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: minus(T152, T153, X263)\n\nT152 is ground\nT153 is ground\nX9 is free\nX239 is free\nX263 is free\nuser_defined_=(T153, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T152, 0) !=? user_defined_=(X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="J: ','(div(T156, T153, X264), user_defined_=(X265, s(X264)))\n\nT153 is ground\nT156 is ground\nX9 is free\nX265 is free\nX264 is free\nuser_defined_=(T153, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: div(T156, T153, X264)\n\nT153 is ground\nT156 is ground\nX9 is free\nX264 is free\nuser_defined_=(T153, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="H: user_defined_=(X265, s(T161))\n\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: user_defined_=(X265, s(T161)), SCOPE: 21, CLAUSE: 6\n\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: user_defined_=(T42, s(T127)), SCOPE: 22, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 248 [arrowhead = none ];
248 -> 6;

249 [label="ONLY EVAL with clause\ndiv(X4, X5, X6) :- ','(user_defined_=(X5, 0), ','(!_1, fail)).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T8,\nX5 -> T8,\nT3 -> T9,\nX6 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 249 [arrowhead = none ];
249 -> 8;

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

251 [label="EVAL with clause\nuser_defined_=(X9, X9).\nand substitutionT8 -> 0,\nX9 -> 0,\nT12 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 251 [arrowhead = none ];
251 -> 15;

252 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 252 [arrowhead = none ];
252 -> 18;

253 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 253 [arrowhead = none ];
253 -> 20;

254 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 254 [arrowhead = none ];
254 -> 25;

255 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 255 [arrowhead = none ];
255 -> 24;

256 [label="ONLY EVAL with clause\ndiv(X16, X17, X18) :- ','(user_defined_=(X16, 0), ','(!_1, user_defined_=(X18, 0))).\nand substitutionT7 -> T20,\nX16 -> T20,\nT8 -> T21,\nX17 -> T21,\nT3 -> T23,\nX18 -> T23,\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 256 [arrowhead = none ];
256 -> 28;

257 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
28 -> 257 [arrowhead = none ];
257 -> 31;

258 [label="EVAL with clause\nuser_defined_=(X21, X21).\nand substitutionT20 -> 0,\nX21 -> 0,\nT26 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 258 [arrowhead = none ];
258 -> 34;

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

260 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 260 [arrowhead = none ];
260 -> 38;

261 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 261 [arrowhead = none ];
261 -> 50;

262 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
38 -> 262 [arrowhead = none ];
262 -> 40;

263 [label="EVAL with clause\nuser_defined_=(X24, X24).\nand substitutionT23 -> 0,\nX24 -> 0,\nT29 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 263 [arrowhead = none ];
263 -> 43;

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

265 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 265 [arrowhead = none ];
265 -> 46;

266 [label="ONLY EVAL with clause\ndiv(X37, X38, X39) :- ','(minus(X37, X38, X40), ','(div(X40, X38, X41), user_defined_=(X39, s(X41)))).\nand substitutionT20 -> T39,\nX37 -> T39,\nT21 -> T40,\nX38 -> T40,\nT3 -> T42,\nX39 -> T42,\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 266 [arrowhead = none ];
266 -> 59;

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

268 [label="SPLIT 2\nnew knowledge:\nT39 is ground\nT40 is ground\nT45 is ground\nreplacements:X40 -> T45", fontsize=14, style = filled, fillcolor = violet];
59 -> 268 [arrowhead = none ];
268 -> 63;

269 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
61 -> 269 [arrowhead = none ];
269 -> 66;

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

271 [label="SPLIT 2\nnew knowledge:\nT45 is ground\nT40 is ground\nreplacements:X41 -> T127", fontsize=14, style = filled, fillcolor = violet];
63 -> 271 [arrowhead = none ];
271 -> 179;

272 [label="ONLY EVAL with clause\nminus(X58, X59, X60) :- ','(user_defined_=(X58, 0), ','(!_5, user_defined_=(X60, 0))).\nand substitutionT39 -> T52,\nX58 -> T52,\nT40 -> T53,\nX59 -> T53,\nX40 -> X61,\nX60 -> X61", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 272 [arrowhead = none ];
272 -> 68;

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

274 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T52, 0), user_defined_=(X21, X21))", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 274 [arrowhead = none ];
274 -> 72;

275 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 275 [arrowhead = none ];
275 -> 73;

276 [label="ONLY EVAL with clause\nminus(X71, X72, X73) :- ','(user_defined_=(X72, 0), ','(!_5, user_defined_=(X73, X71))).\nand substitutionT52 -> T59,\nX71 -> T59,\nT53 -> T60,\nX72 -> T60,\nX40 -> X74,\nX73 -> X74", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 276 [arrowhead = none ];
276 -> 78;

277 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
78 -> 277 [arrowhead = none ];
277 -> 80;

278 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T60, 0), user_defined_=(X9, X9))", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 278 [arrowhead = none ];
278 -> 82;

279 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 279 [arrowhead = none ];
279 -> 85;

280 [label="ONLY EVAL with clause\nminus(X92, X93, X94) :- ','(user_defined_=(X92, s(X95)), ','(user_defined_=(X93, s(X96)), minus(X95, X96, X94))).\nand substitutionT59 -> T66,\nX92 -> T66,\nT60 -> T67,\nX93 -> T67,\nX40 -> X97,\nX94 -> X97", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 280 [arrowhead = none ];
280 -> 88;

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

282 [label="EVAL with clause\nuser_defined_=(X106, X106).\nand substitutionT66 -> s(T73),\nX106 -> s(T73),\nX95 -> T73,\nT72 -> s(T73)", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 282 [arrowhead = none ];
282 -> 95;

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

284 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
95 -> 284 [arrowhead = none ];
284 -> 99;

285 [label="EVAL with clause\nuser_defined_=(X114, X114).\nand substitutionT67 -> s(T80),\nX114 -> s(T80),\nX96 -> T80,\nT79 -> s(T80)", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 285 [arrowhead = none ];
285 -> 102;

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

287 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
102 -> 287 [arrowhead = none ];
287 -> 108;

288 [label="ONLY EVAL with clause\nminus(X127, X128, X129) :- ','(user_defined_=(X127, 0), ','(!_10, user_defined_=(X129, 0))).\nand substitutionT73 -> T87,\nX127 -> T87,\nT80 -> T88,\nX128 -> T88,\nX97 -> X130,\nX129 -> X130", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 288 [arrowhead = none ];
288 -> 111;

289 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
111 -> 289 [arrowhead = none ];
289 -> 113;

290 [label="EVAL with clause\nuser_defined_=(X133, X133).\nand substitutionT87 -> 0,\nX133 -> 0,\nT91 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 290 [arrowhead = none ];
290 -> 115;

291 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 291 [arrowhead = none ];
291 -> 118;

292 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 292 [arrowhead = none ];
292 -> 120;

293 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 293 [arrowhead = none ];
293 -> 127;

294 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
120 -> 294 [arrowhead = none ];
294 -> 121;

295 [label="ONLY EVAL with clause\nuser_defined_=(X138, X138).\nand substitutionX130 -> 0,\nX138 -> 0,\nX139 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 295 [arrowhead = none ];
295 -> 125;

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

297 [label="ONLY EVAL with clause\nminus(X148, X149, X150) :- ','(user_defined_=(X149, 0), ','(!_10, user_defined_=(X150, X148))).\nand substitutionT87 -> T96,\nX148 -> T96,\nT88 -> T97,\nX149 -> T97,\nX97 -> X151,\nX150 -> X151", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 297 [arrowhead = none ];
297 -> 129;

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

299 [label="EVAL with clause\nuser_defined_=(X154, X154).\nand substitutionT97 -> 0,\nX154 -> 0,\nT100 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 299 [arrowhead = none ];
299 -> 133;

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

301 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 301 [arrowhead = none ];
301 -> 137;

302 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 302 [arrowhead = none ];
302 -> 146;

303 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
137 -> 303 [arrowhead = none ];
303 -> 139;

304 [label="ONLY EVAL with clause\nuser_defined_=(X159, X159).\nand substitutionX151 -> T103,\nX159 -> T103,\nT96 -> T103,\nX160 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 304 [arrowhead = none ];
304 -> 143;

305 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 305 [arrowhead = none ];
305 -> 144;

306 [label="ONLY EVAL with clause\nminus(X177, X178, X179) :- ','(user_defined_=(X177, s(X180)), ','(user_defined_=(X178, s(X181)), minus(X180, X181, X179))).\nand substitutionT96 -> T108,\nX177 -> T108,\nT97 -> T109,\nX178 -> T109,\nX97 -> X182,\nX179 -> X182", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 306 [arrowhead = none ];
306 -> 152;

307 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
152 -> 307 [arrowhead = none ];
307 -> 154;

308 [label="EVAL with clause\nuser_defined_=(X191, X191).\nand substitutionT108 -> s(T115),\nX191 -> s(T115),\nX180 -> T115,\nT114 -> s(T115)", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 308 [arrowhead = none ];
308 -> 156;

309 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 309 [arrowhead = none ];
309 -> 158;

310 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
156 -> 310 [arrowhead = none ];
310 -> 160;

311 [label="EVAL with clause\nuser_defined_=(X199, X199).\nand substitutionT109 -> s(T122),\nX199 -> s(T122),\nX181 -> T122,\nT121 -> s(T122)", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 311 [arrowhead = none ];
311 -> 164;

312 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 312 [arrowhead = none ];
312 -> 166;

313 [label="INSTANCE with matching:\nT73 -> T115\nT80 -> T122\nX97 -> X182", fontsize=14, style = filled, fillcolor = lightgrey];
164 -> 313 [arrowhead = none , style=dashed];
313 -> 102[style=dashed];

314 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
177 -> 314 [arrowhead = none ];
314 -> 182;

315 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
179 -> 315 [arrowhead = none ];
315 -> 241;

316 [label="ONLY EVAL with clause\ndiv(X220, X221, X222) :- ','(user_defined_=(X221, 0), ','(!_17, fail)).\nand substitutionT45 -> T134,\nX220 -> T134,\nT40 -> T135,\nX221 -> T135,\nX41 -> X223,\nX222 -> X223", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 316 [arrowhead = none ];
316 -> 184;

317 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
184 -> 317 [arrowhead = none ];
317 -> 186;

318 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T135, 0), user_defined_=(X9, X9))", fontsize=14, style = filled, fillcolor = lightgreen];
186 -> 318 [arrowhead = none ];
318 -> 189;

319 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
189 -> 319 [arrowhead = none ];
319 -> 190;

320 [label="ONLY EVAL with clause\ndiv(X233, X234, X235) :- ','(user_defined_=(X233, 0), ','(!_17, user_defined_=(X235, 0))).\nand substitutionT134 -> T141,\nX233 -> T141,\nT135 -> T142,\nX234 -> T142,\nX41 -> X236,\nX235 -> X236", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 320 [arrowhead = none ];
320 -> 193;

321 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
193 -> 321 [arrowhead = none ];
321 -> 195;

322 [label="EVAL with clause\nuser_defined_=(X239, X239).\nand substitutionT141 -> 0,\nX239 -> 0,\nT145 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 322 [arrowhead = none ];
322 -> 196;

323 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
195 -> 323 [arrowhead = none ];
323 -> 198;

324 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 324 [arrowhead = none ];
324 -> 200;

325 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
198 -> 325 [arrowhead = none ];
325 -> 210;

326 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
200 -> 326 [arrowhead = none ];
326 -> 202;

327 [label="ONLY EVAL with clause\nuser_defined_=(X244, X244).\nand substitutionX236 -> 0,\nX244 -> 0,\nX245 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
202 -> 327 [arrowhead = none ];
327 -> 205;

328 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 328 [arrowhead = none ];
328 -> 206;

329 [label="ONLY EVAL with clause\ndiv(X260, X261, X262) :- ','(minus(X260, X261, X263), ','(div(X263, X261, X264), user_defined_=(X262, s(X264)))).\nand substitutionT141 -> T152,\nX260 -> T152,\nT142 -> T153,\nX261 -> T153,\nX41 -> X265,\nX262 -> X265", fontsize=14, style = filled, fillcolor = lightblue];
210 -> 329 [arrowhead = none ];
329 -> 219;

330 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
219 -> 330 [arrowhead = none ];
330 -> 223;

331 [label="SPLIT 2\nnew knowledge:\nT152 is ground\nT153 is ground\nT156 is ground\nreplacements:X263 -> T156", fontsize=14, style = filled, fillcolor = violet];
219 -> 331 [arrowhead = none ];
331 -> 225;

332 [label="INSTANCE with matching:\nT39 -> T152\nT40 -> T153\nX40 -> X263\nX21 -> X239", fontsize=14, style = filled, fillcolor = lightgrey];
223 -> 332 [arrowhead = none , style=dashed];
332 -> 61[style=dashed];

333 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
225 -> 333 [arrowhead = none ];
333 -> 232;

334 [label="SPLIT 2\nnew knowledge:\nT156 is ground\nT153 is ground\nreplacements:X264 -> T161", fontsize=14, style = filled, fillcolor = violet];
225 -> 334 [arrowhead = none ];
334 -> 233;

335 [label="INSTANCE with matching:\nT45 -> T156\nT40 -> T153\nX41 -> X264", fontsize=14, style = filled, fillcolor = lightgrey];
232 -> 335 [arrowhead = none , style=dashed];
335 -> 177[style=dashed];

336 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
233 -> 336 [arrowhead = none ];
336 -> 235;

337 [label="ONLY EVAL with clause\nuser_defined_=(X286, X286).\nand substitutionX265 -> s(T166),\nX286 -> s(T166),\nT161 -> T166,\nX287 -> s(T166)", fontsize=14, style = filled, fillcolor = lightblue];
235 -> 337 [arrowhead = none ];
337 -> 238;

338 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
238 -> 338 [arrowhead = none ];
338 -> 239;

339 [label="EVAL with clause\nuser_defined_=(X290, X290).\nand substitutionT42 -> s(T172),\nX290 -> s(T172),\nT127 -> T172,\nT171 -> s(T172)", fontsize=14, style = filled, fillcolor = lightblue];
241 -> 339 [arrowhead = none ];
339 -> 243;

340 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
241 -> 340 [arrowhead = none ];
340 -> 245;

341 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
243 -> 341 [arrowhead = none ];
341 -> 247;

}

(4) Obligation:

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

divA_in_gga(0, T21, 0) → divA_out_gga(0, T21, 0)
divA_in_gga(T39, T40, T42) → U1_gga(T39, T40, T42, pB_in_ggaaa(T39, T40, X40, X41, T42))
pB_in_ggaaa(T39, T40, T45, X41, T42) → U5_ggaaa(T39, T40, T45, X41, T42, minusD_in_gga(T39, T40, T45))
minusD_in_gga(s(T73), s(T80), X97) → U3_gga(T73, T80, X97, minusC_in_gga(T73, T80, X97))
minusC_in_gga(0, T88, 0) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0, T103) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122), X182) → U2_gga(T115, T122, X182, minusC_in_gga(T115, T122, X182))
U2_gga(T115, T122, X182, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)
U3_gga(T73, T80, X97, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
U5_ggaaa(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → U6_ggaaa(T39, T40, T45, X41, T42, pI_in_ggaa(T45, T40, X41, T42))
pI_in_ggaa(T45, T40, T127, T42) → U7_ggaa(T45, T40, T127, T42, divE_in_gga(T45, T40, T127))
divE_in_gga(0, T142, 0) → divE_out_gga(0, T142, 0)
divE_in_gga(T152, T153, X265) → U4_gga(T152, T153, X265, pF_in_ggaaa(T152, T153, X263, X264, X265))
pF_in_ggaaa(T152, T153, T156, X264, X265) → U9_ggaaa(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
U9_ggaaa(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → U10_ggaaa(T152, T153, T156, X264, X265, pJ_in_ggaa(T156, T153, X264, X265))
pJ_in_ggaa(T156, T153, T161, X265) → U11_ggaa(T156, T153, T161, X265, divE_in_gga(T156, T153, T161))
U11_ggaa(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → U12_ggaa(T156, T153, T161, X265, user_defined_=H_in_ag(X265, T161))
user_defined_=H_in_ag(s(T166), T166) → user_defined_=H_out_ag(s(T166), T166)
U12_ggaa(T156, T153, T161, X265, user_defined_=H_out_ag(X265, T161)) → pJ_out_ggaa(T156, T153, T161, X265)
U10_ggaaa(T152, T153, T156, X264, X265, pJ_out_ggaa(T156, T153, X264, X265)) → pF_out_ggaaa(T152, T153, T156, X264, X265)
U4_gga(T152, T153, X265, pF_out_ggaaa(T152, T153, X263, X264, X265)) → divE_out_gga(T152, T153, X265)
U7_ggaa(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → U8_ggaa(T45, T40, T127, T42, user_defined_=G_in_ag(T42, T127))
user_defined_=G_in_ag(s(T172), T172) → user_defined_=G_out_ag(s(T172), T172)
U8_ggaa(T45, T40, T127, T42, user_defined_=G_out_ag(T42, T127)) → pI_out_ggaa(T45, T40, T127, T42)
U6_ggaaa(T39, T40, T45, X41, T42, pI_out_ggaa(T45, T40, X41, T42)) → pB_out_ggaaa(T39, T40, T45, X41, T42)
U1_gga(T39, T40, T42, pB_out_ggaaa(T39, T40, X40, X41, T42)) → divA_out_gga(T39, T40, T42)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
0  =  0
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x6)
minusD_in_gga(x1, x2, x3)  =  minusD_in_gga(x1, x2)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3)  =  minusD_out_gga(x1, x2, x3)
U6_ggaaa(x1, x2, x3, x4, x5, x6)  =  U6_ggaaa(x1, x2, x3, x6)
pI_in_ggaa(x1, x2, x3, x4)  =  pI_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
divE_in_gga(x1, x2, x3)  =  divE_in_gga(x1, x2)
divE_out_gga(x1, x2, x3)  =  divE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pF_in_ggaaa(x1, x2, x3, x4, x5)  =  pF_in_ggaaa(x1, x2)
U9_ggaaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaaa(x1, x2, x6)
U10_ggaaa(x1, x2, x3, x4, x5, x6)  =  U10_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
user_defined_=H_in_ag(x1, x2)  =  user_defined_=H_in_ag(x2)
user_defined_=H_out_ag(x1, x2)  =  user_defined_=H_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pF_out_ggaaa(x1, x2, x3, x4, x5)  =  pF_out_ggaaa(x1, x2, x3, x4, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
user_defined_=G_in_ag(x1, x2)  =  user_defined_=G_in_ag(x2)
user_defined_=G_out_ag(x1, x2)  =  user_defined_=G_out_ag(x1, x2)
pI_out_ggaa(x1, x2, x3, x4)  =  pI_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)

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

DIVA_IN_GGA(T39, T40, T42) → U1_GGA(T39, T40, T42, pB_in_ggaaa(T39, T40, X40, X41, T42))
DIVA_IN_GGA(T39, T40, T42) → PB_IN_GGAAA(T39, T40, X40, X41, T42)
PB_IN_GGAAA(T39, T40, T45, X41, T42) → U5_GGAAA(T39, T40, T45, X41, T42, minusD_in_gga(T39, T40, T45))
PB_IN_GGAAA(T39, T40, T45, X41, T42) → MINUSD_IN_GGA(T39, T40, T45)
MINUSD_IN_GGA(s(T73), s(T80), X97) → U3_GGA(T73, T80, X97, minusC_in_gga(T73, T80, X97))
MINUSD_IN_GGA(s(T73), s(T80), X97) → MINUSC_IN_GGA(T73, T80, X97)
MINUSC_IN_GGA(s(T115), s(T122), X182) → U2_GGA(T115, T122, X182, minusC_in_gga(T115, T122, X182))
MINUSC_IN_GGA(s(T115), s(T122), X182) → MINUSC_IN_GGA(T115, T122, X182)
U5_GGAAA(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → U6_GGAAA(T39, T40, T45, X41, T42, pI_in_ggaa(T45, T40, X41, T42))
U5_GGAAA(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → PI_IN_GGAA(T45, T40, X41, T42)
PI_IN_GGAA(T45, T40, T127, T42) → U7_GGAA(T45, T40, T127, T42, divE_in_gga(T45, T40, T127))
PI_IN_GGAA(T45, T40, T127, T42) → DIVE_IN_GGA(T45, T40, T127)
DIVE_IN_GGA(T152, T153, X265) → U4_GGA(T152, T153, X265, pF_in_ggaaa(T152, T153, X263, X264, X265))
DIVE_IN_GGA(T152, T153, X265) → PF_IN_GGAAA(T152, T153, X263, X264, X265)
PF_IN_GGAAA(T152, T153, T156, X264, X265) → U9_GGAAA(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
PF_IN_GGAAA(T152, T153, T156, X264, X265) → MINUSD_IN_GGA(T152, T153, T156)
U9_GGAAA(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → U10_GGAAA(T152, T153, T156, X264, X265, pJ_in_ggaa(T156, T153, X264, X265))
U9_GGAAA(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → PJ_IN_GGAA(T156, T153, X264, X265)
PJ_IN_GGAA(T156, T153, T161, X265) → U11_GGAA(T156, T153, T161, X265, divE_in_gga(T156, T153, T161))
PJ_IN_GGAA(T156, T153, T161, X265) → DIVE_IN_GGA(T156, T153, T161)
U11_GGAA(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → U12_GGAA(T156, T153, T161, X265, user_defined_=H_in_ag(X265, T161))
U11_GGAA(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → USER_DEFINED_=H_IN_AG(X265, T161)
U7_GGAA(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → U8_GGAA(T45, T40, T127, T42, user_defined_=G_in_ag(T42, T127))
U7_GGAA(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → USER_DEFINED_=G_IN_AG(T42, T127)

The TRS R consists of the following rules:

divA_in_gga(0, T21, 0) → divA_out_gga(0, T21, 0)
divA_in_gga(T39, T40, T42) → U1_gga(T39, T40, T42, pB_in_ggaaa(T39, T40, X40, X41, T42))
pB_in_ggaaa(T39, T40, T45, X41, T42) → U5_ggaaa(T39, T40, T45, X41, T42, minusD_in_gga(T39, T40, T45))
minusD_in_gga(s(T73), s(T80), X97) → U3_gga(T73, T80, X97, minusC_in_gga(T73, T80, X97))
minusC_in_gga(0, T88, 0) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0, T103) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122), X182) → U2_gga(T115, T122, X182, minusC_in_gga(T115, T122, X182))
U2_gga(T115, T122, X182, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)
U3_gga(T73, T80, X97, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
U5_ggaaa(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → U6_ggaaa(T39, T40, T45, X41, T42, pI_in_ggaa(T45, T40, X41, T42))
pI_in_ggaa(T45, T40, T127, T42) → U7_ggaa(T45, T40, T127, T42, divE_in_gga(T45, T40, T127))
divE_in_gga(0, T142, 0) → divE_out_gga(0, T142, 0)
divE_in_gga(T152, T153, X265) → U4_gga(T152, T153, X265, pF_in_ggaaa(T152, T153, X263, X264, X265))
pF_in_ggaaa(T152, T153, T156, X264, X265) → U9_ggaaa(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
U9_ggaaa(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → U10_ggaaa(T152, T153, T156, X264, X265, pJ_in_ggaa(T156, T153, X264, X265))
pJ_in_ggaa(T156, T153, T161, X265) → U11_ggaa(T156, T153, T161, X265, divE_in_gga(T156, T153, T161))
U11_ggaa(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → U12_ggaa(T156, T153, T161, X265, user_defined_=H_in_ag(X265, T161))
user_defined_=H_in_ag(s(T166), T166) → user_defined_=H_out_ag(s(T166), T166)
U12_ggaa(T156, T153, T161, X265, user_defined_=H_out_ag(X265, T161)) → pJ_out_ggaa(T156, T153, T161, X265)
U10_ggaaa(T152, T153, T156, X264, X265, pJ_out_ggaa(T156, T153, X264, X265)) → pF_out_ggaaa(T152, T153, T156, X264, X265)
U4_gga(T152, T153, X265, pF_out_ggaaa(T152, T153, X263, X264, X265)) → divE_out_gga(T152, T153, X265)
U7_ggaa(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → U8_ggaa(T45, T40, T127, T42, user_defined_=G_in_ag(T42, T127))
user_defined_=G_in_ag(s(T172), T172) → user_defined_=G_out_ag(s(T172), T172)
U8_ggaa(T45, T40, T127, T42, user_defined_=G_out_ag(T42, T127)) → pI_out_ggaa(T45, T40, T127, T42)
U6_ggaaa(T39, T40, T45, X41, T42, pI_out_ggaa(T45, T40, X41, T42)) → pB_out_ggaaa(T39, T40, T45, X41, T42)
U1_gga(T39, T40, T42, pB_out_ggaaa(T39, T40, X40, X41, T42)) → divA_out_gga(T39, T40, T42)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
0  =  0
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x6)
minusD_in_gga(x1, x2, x3)  =  minusD_in_gga(x1, x2)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3)  =  minusD_out_gga(x1, x2, x3)
U6_ggaaa(x1, x2, x3, x4, x5, x6)  =  U6_ggaaa(x1, x2, x3, x6)
pI_in_ggaa(x1, x2, x3, x4)  =  pI_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
divE_in_gga(x1, x2, x3)  =  divE_in_gga(x1, x2)
divE_out_gga(x1, x2, x3)  =  divE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pF_in_ggaaa(x1, x2, x3, x4, x5)  =  pF_in_ggaaa(x1, x2)
U9_ggaaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaaa(x1, x2, x6)
U10_ggaaa(x1, x2, x3, x4, x5, x6)  =  U10_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
user_defined_=H_in_ag(x1, x2)  =  user_defined_=H_in_ag(x2)
user_defined_=H_out_ag(x1, x2)  =  user_defined_=H_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pF_out_ggaaa(x1, x2, x3, x4, x5)  =  pF_out_ggaaa(x1, x2, x3, x4, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
user_defined_=G_in_ag(x1, x2)  =  user_defined_=G_in_ag(x2)
user_defined_=G_out_ag(x1, x2)  =  user_defined_=G_out_ag(x1, x2)
pI_out_ggaa(x1, x2, x3, x4)  =  pI_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
DIVA_IN_GGA(x1, x2, x3)  =  DIVA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
U5_GGAAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAAA(x1, x2, x6)
MINUSD_IN_GGA(x1, x2, x3)  =  MINUSD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
MINUSC_IN_GGA(x1, x2, x3)  =  MINUSC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U6_GGAAA(x1, x2, x3, x4, x5, x6)  =  U6_GGAAA(x1, x2, x3, x6)
PI_IN_GGAA(x1, x2, x3, x4)  =  PI_IN_GGAA(x1, x2)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x1, x2, x5)
DIVE_IN_GGA(x1, x2, x3)  =  DIVE_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
PF_IN_GGAAA(x1, x2, x3, x4, x5)  =  PF_IN_GGAAA(x1, x2)
U9_GGAAA(x1, x2, x3, x4, x5, x6)  =  U9_GGAAA(x1, x2, x6)
U10_GGAAA(x1, x2, x3, x4, x5, x6)  =  U10_GGAAA(x1, x2, x3, x6)
PJ_IN_GGAA(x1, x2, x3, x4)  =  PJ_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
USER_DEFINED_=H_IN_AG(x1, x2)  =  USER_DEFINED_=H_IN_AG(x2)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x1, x2, x3, x5)
USER_DEFINED_=G_IN_AG(x1, x2)  =  USER_DEFINED_=G_IN_AG(x2)

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

(6) Obligation:

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

DIVA_IN_GGA(T39, T40, T42) → U1_GGA(T39, T40, T42, pB_in_ggaaa(T39, T40, X40, X41, T42))
DIVA_IN_GGA(T39, T40, T42) → PB_IN_GGAAA(T39, T40, X40, X41, T42)
PB_IN_GGAAA(T39, T40, T45, X41, T42) → U5_GGAAA(T39, T40, T45, X41, T42, minusD_in_gga(T39, T40, T45))
PB_IN_GGAAA(T39, T40, T45, X41, T42) → MINUSD_IN_GGA(T39, T40, T45)
MINUSD_IN_GGA(s(T73), s(T80), X97) → U3_GGA(T73, T80, X97, minusC_in_gga(T73, T80, X97))
MINUSD_IN_GGA(s(T73), s(T80), X97) → MINUSC_IN_GGA(T73, T80, X97)
MINUSC_IN_GGA(s(T115), s(T122), X182) → U2_GGA(T115, T122, X182, minusC_in_gga(T115, T122, X182))
MINUSC_IN_GGA(s(T115), s(T122), X182) → MINUSC_IN_GGA(T115, T122, X182)
U5_GGAAA(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → U6_GGAAA(T39, T40, T45, X41, T42, pI_in_ggaa(T45, T40, X41, T42))
U5_GGAAA(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → PI_IN_GGAA(T45, T40, X41, T42)
PI_IN_GGAA(T45, T40, T127, T42) → U7_GGAA(T45, T40, T127, T42, divE_in_gga(T45, T40, T127))
PI_IN_GGAA(T45, T40, T127, T42) → DIVE_IN_GGA(T45, T40, T127)
DIVE_IN_GGA(T152, T153, X265) → U4_GGA(T152, T153, X265, pF_in_ggaaa(T152, T153, X263, X264, X265))
DIVE_IN_GGA(T152, T153, X265) → PF_IN_GGAAA(T152, T153, X263, X264, X265)
PF_IN_GGAAA(T152, T153, T156, X264, X265) → U9_GGAAA(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
PF_IN_GGAAA(T152, T153, T156, X264, X265) → MINUSD_IN_GGA(T152, T153, T156)
U9_GGAAA(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → U10_GGAAA(T152, T153, T156, X264, X265, pJ_in_ggaa(T156, T153, X264, X265))
U9_GGAAA(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → PJ_IN_GGAA(T156, T153, X264, X265)
PJ_IN_GGAA(T156, T153, T161, X265) → U11_GGAA(T156, T153, T161, X265, divE_in_gga(T156, T153, T161))
PJ_IN_GGAA(T156, T153, T161, X265) → DIVE_IN_GGA(T156, T153, T161)
U11_GGAA(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → U12_GGAA(T156, T153, T161, X265, user_defined_=H_in_ag(X265, T161))
U11_GGAA(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → USER_DEFINED_=H_IN_AG(X265, T161)
U7_GGAA(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → U8_GGAA(T45, T40, T127, T42, user_defined_=G_in_ag(T42, T127))
U7_GGAA(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → USER_DEFINED_=G_IN_AG(T42, T127)

The TRS R consists of the following rules:

divA_in_gga(0, T21, 0) → divA_out_gga(0, T21, 0)
divA_in_gga(T39, T40, T42) → U1_gga(T39, T40, T42, pB_in_ggaaa(T39, T40, X40, X41, T42))
pB_in_ggaaa(T39, T40, T45, X41, T42) → U5_ggaaa(T39, T40, T45, X41, T42, minusD_in_gga(T39, T40, T45))
minusD_in_gga(s(T73), s(T80), X97) → U3_gga(T73, T80, X97, minusC_in_gga(T73, T80, X97))
minusC_in_gga(0, T88, 0) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0, T103) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122), X182) → U2_gga(T115, T122, X182, minusC_in_gga(T115, T122, X182))
U2_gga(T115, T122, X182, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)
U3_gga(T73, T80, X97, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
U5_ggaaa(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → U6_ggaaa(T39, T40, T45, X41, T42, pI_in_ggaa(T45, T40, X41, T42))
pI_in_ggaa(T45, T40, T127, T42) → U7_ggaa(T45, T40, T127, T42, divE_in_gga(T45, T40, T127))
divE_in_gga(0, T142, 0) → divE_out_gga(0, T142, 0)
divE_in_gga(T152, T153, X265) → U4_gga(T152, T153, X265, pF_in_ggaaa(T152, T153, X263, X264, X265))
pF_in_ggaaa(T152, T153, T156, X264, X265) → U9_ggaaa(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
U9_ggaaa(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → U10_ggaaa(T152, T153, T156, X264, X265, pJ_in_ggaa(T156, T153, X264, X265))
pJ_in_ggaa(T156, T153, T161, X265) → U11_ggaa(T156, T153, T161, X265, divE_in_gga(T156, T153, T161))
U11_ggaa(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → U12_ggaa(T156, T153, T161, X265, user_defined_=H_in_ag(X265, T161))
user_defined_=H_in_ag(s(T166), T166) → user_defined_=H_out_ag(s(T166), T166)
U12_ggaa(T156, T153, T161, X265, user_defined_=H_out_ag(X265, T161)) → pJ_out_ggaa(T156, T153, T161, X265)
U10_ggaaa(T152, T153, T156, X264, X265, pJ_out_ggaa(T156, T153, X264, X265)) → pF_out_ggaaa(T152, T153, T156, X264, X265)
U4_gga(T152, T153, X265, pF_out_ggaaa(T152, T153, X263, X264, X265)) → divE_out_gga(T152, T153, X265)
U7_ggaa(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → U8_ggaa(T45, T40, T127, T42, user_defined_=G_in_ag(T42, T127))
user_defined_=G_in_ag(s(T172), T172) → user_defined_=G_out_ag(s(T172), T172)
U8_ggaa(T45, T40, T127, T42, user_defined_=G_out_ag(T42, T127)) → pI_out_ggaa(T45, T40, T127, T42)
U6_ggaaa(T39, T40, T45, X41, T42, pI_out_ggaa(T45, T40, X41, T42)) → pB_out_ggaaa(T39, T40, T45, X41, T42)
U1_gga(T39, T40, T42, pB_out_ggaaa(T39, T40, X40, X41, T42)) → divA_out_gga(T39, T40, T42)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
0  =  0
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x6)
minusD_in_gga(x1, x2, x3)  =  minusD_in_gga(x1, x2)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3)  =  minusD_out_gga(x1, x2, x3)
U6_ggaaa(x1, x2, x3, x4, x5, x6)  =  U6_ggaaa(x1, x2, x3, x6)
pI_in_ggaa(x1, x2, x3, x4)  =  pI_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
divE_in_gga(x1, x2, x3)  =  divE_in_gga(x1, x2)
divE_out_gga(x1, x2, x3)  =  divE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pF_in_ggaaa(x1, x2, x3, x4, x5)  =  pF_in_ggaaa(x1, x2)
U9_ggaaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaaa(x1, x2, x6)
U10_ggaaa(x1, x2, x3, x4, x5, x6)  =  U10_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
user_defined_=H_in_ag(x1, x2)  =  user_defined_=H_in_ag(x2)
user_defined_=H_out_ag(x1, x2)  =  user_defined_=H_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pF_out_ggaaa(x1, x2, x3, x4, x5)  =  pF_out_ggaaa(x1, x2, x3, x4, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
user_defined_=G_in_ag(x1, x2)  =  user_defined_=G_in_ag(x2)
user_defined_=G_out_ag(x1, x2)  =  user_defined_=G_out_ag(x1, x2)
pI_out_ggaa(x1, x2, x3, x4)  =  pI_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
DIVA_IN_GGA(x1, x2, x3)  =  DIVA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
U5_GGAAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAAA(x1, x2, x6)
MINUSD_IN_GGA(x1, x2, x3)  =  MINUSD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
MINUSC_IN_GGA(x1, x2, x3)  =  MINUSC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U6_GGAAA(x1, x2, x3, x4, x5, x6)  =  U6_GGAAA(x1, x2, x3, x6)
PI_IN_GGAA(x1, x2, x3, x4)  =  PI_IN_GGAA(x1, x2)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x1, x2, x5)
DIVE_IN_GGA(x1, x2, x3)  =  DIVE_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
PF_IN_GGAAA(x1, x2, x3, x4, x5)  =  PF_IN_GGAAA(x1, x2)
U9_GGAAA(x1, x2, x3, x4, x5, x6)  =  U9_GGAAA(x1, x2, x6)
U10_GGAAA(x1, x2, x3, x4, x5, x6)  =  U10_GGAAA(x1, x2, x3, x6)
PJ_IN_GGAA(x1, x2, x3, x4)  =  PJ_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
USER_DEFINED_=H_IN_AG(x1, x2)  =  USER_DEFINED_=H_IN_AG(x2)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x1, x2, x3, x5)
USER_DEFINED_=G_IN_AG(x1, x2)  =  USER_DEFINED_=G_IN_AG(x2)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

MINUSC_IN_GGA(s(T115), s(T122), X182) → MINUSC_IN_GGA(T115, T122, X182)

The TRS R consists of the following rules:

divA_in_gga(0, T21, 0) → divA_out_gga(0, T21, 0)
divA_in_gga(T39, T40, T42) → U1_gga(T39, T40, T42, pB_in_ggaaa(T39, T40, X40, X41, T42))
pB_in_ggaaa(T39, T40, T45, X41, T42) → U5_ggaaa(T39, T40, T45, X41, T42, minusD_in_gga(T39, T40, T45))
minusD_in_gga(s(T73), s(T80), X97) → U3_gga(T73, T80, X97, minusC_in_gga(T73, T80, X97))
minusC_in_gga(0, T88, 0) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0, T103) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122), X182) → U2_gga(T115, T122, X182, minusC_in_gga(T115, T122, X182))
U2_gga(T115, T122, X182, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)
U3_gga(T73, T80, X97, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
U5_ggaaa(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → U6_ggaaa(T39, T40, T45, X41, T42, pI_in_ggaa(T45, T40, X41, T42))
pI_in_ggaa(T45, T40, T127, T42) → U7_ggaa(T45, T40, T127, T42, divE_in_gga(T45, T40, T127))
divE_in_gga(0, T142, 0) → divE_out_gga(0, T142, 0)
divE_in_gga(T152, T153, X265) → U4_gga(T152, T153, X265, pF_in_ggaaa(T152, T153, X263, X264, X265))
pF_in_ggaaa(T152, T153, T156, X264, X265) → U9_ggaaa(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
U9_ggaaa(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → U10_ggaaa(T152, T153, T156, X264, X265, pJ_in_ggaa(T156, T153, X264, X265))
pJ_in_ggaa(T156, T153, T161, X265) → U11_ggaa(T156, T153, T161, X265, divE_in_gga(T156, T153, T161))
U11_ggaa(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → U12_ggaa(T156, T153, T161, X265, user_defined_=H_in_ag(X265, T161))
user_defined_=H_in_ag(s(T166), T166) → user_defined_=H_out_ag(s(T166), T166)
U12_ggaa(T156, T153, T161, X265, user_defined_=H_out_ag(X265, T161)) → pJ_out_ggaa(T156, T153, T161, X265)
U10_ggaaa(T152, T153, T156, X264, X265, pJ_out_ggaa(T156, T153, X264, X265)) → pF_out_ggaaa(T152, T153, T156, X264, X265)
U4_gga(T152, T153, X265, pF_out_ggaaa(T152, T153, X263, X264, X265)) → divE_out_gga(T152, T153, X265)
U7_ggaa(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → U8_ggaa(T45, T40, T127, T42, user_defined_=G_in_ag(T42, T127))
user_defined_=G_in_ag(s(T172), T172) → user_defined_=G_out_ag(s(T172), T172)
U8_ggaa(T45, T40, T127, T42, user_defined_=G_out_ag(T42, T127)) → pI_out_ggaa(T45, T40, T127, T42)
U6_ggaaa(T39, T40, T45, X41, T42, pI_out_ggaa(T45, T40, X41, T42)) → pB_out_ggaaa(T39, T40, T45, X41, T42)
U1_gga(T39, T40, T42, pB_out_ggaaa(T39, T40, X40, X41, T42)) → divA_out_gga(T39, T40, T42)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
0  =  0
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x6)
minusD_in_gga(x1, x2, x3)  =  minusD_in_gga(x1, x2)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3)  =  minusD_out_gga(x1, x2, x3)
U6_ggaaa(x1, x2, x3, x4, x5, x6)  =  U6_ggaaa(x1, x2, x3, x6)
pI_in_ggaa(x1, x2, x3, x4)  =  pI_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
divE_in_gga(x1, x2, x3)  =  divE_in_gga(x1, x2)
divE_out_gga(x1, x2, x3)  =  divE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pF_in_ggaaa(x1, x2, x3, x4, x5)  =  pF_in_ggaaa(x1, x2)
U9_ggaaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaaa(x1, x2, x6)
U10_ggaaa(x1, x2, x3, x4, x5, x6)  =  U10_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
user_defined_=H_in_ag(x1, x2)  =  user_defined_=H_in_ag(x2)
user_defined_=H_out_ag(x1, x2)  =  user_defined_=H_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pF_out_ggaaa(x1, x2, x3, x4, x5)  =  pF_out_ggaaa(x1, x2, x3, x4, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
user_defined_=G_in_ag(x1, x2)  =  user_defined_=G_in_ag(x2)
user_defined_=G_out_ag(x1, x2)  =  user_defined_=G_out_ag(x1, x2)
pI_out_ggaa(x1, x2, x3, x4)  =  pI_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
MINUSC_IN_GGA(x1, x2, x3)  =  MINUSC_IN_GGA(x1, x2)

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

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

MINUSC_IN_GGA(s(T115), s(T122), X182) → MINUSC_IN_GGA(T115, T122, X182)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MINUSC_IN_GGA(x1, x2, x3)  =  MINUSC_IN_GGA(x1, x2)

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:

MINUSC_IN_GGA(s(T115), s(T122)) → MINUSC_IN_GGA(T115, T122)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• MINUSC_IN_GGA(s(T115), s(T122)) → MINUSC_IN_GGA(T115, T122)
  The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

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

PF_IN_GGAAA(T152, T153, T156, X264, X265) → U9_GGAAA(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
U9_GGAAA(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → PJ_IN_GGAA(T156, T153, X264, X265)
PJ_IN_GGAA(T156, T153, T161, X265) → DIVE_IN_GGA(T156, T153, T161)
DIVE_IN_GGA(T152, T153, X265) → PF_IN_GGAAA(T152, T153, X263, X264, X265)

The TRS R consists of the following rules:

divA_in_gga(0, T21, 0) → divA_out_gga(0, T21, 0)
divA_in_gga(T39, T40, T42) → U1_gga(T39, T40, T42, pB_in_ggaaa(T39, T40, X40, X41, T42))
pB_in_ggaaa(T39, T40, T45, X41, T42) → U5_ggaaa(T39, T40, T45, X41, T42, minusD_in_gga(T39, T40, T45))
minusD_in_gga(s(T73), s(T80), X97) → U3_gga(T73, T80, X97, minusC_in_gga(T73, T80, X97))
minusC_in_gga(0, T88, 0) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0, T103) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122), X182) → U2_gga(T115, T122, X182, minusC_in_gga(T115, T122, X182))
U2_gga(T115, T122, X182, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)
U3_gga(T73, T80, X97, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
U5_ggaaa(T39, T40, T45, X41, T42, minusD_out_gga(T39, T40, T45)) → U6_ggaaa(T39, T40, T45, X41, T42, pI_in_ggaa(T45, T40, X41, T42))
pI_in_ggaa(T45, T40, T127, T42) → U7_ggaa(T45, T40, T127, T42, divE_in_gga(T45, T40, T127))
divE_in_gga(0, T142, 0) → divE_out_gga(0, T142, 0)
divE_in_gga(T152, T153, X265) → U4_gga(T152, T153, X265, pF_in_ggaaa(T152, T153, X263, X264, X265))
pF_in_ggaaa(T152, T153, T156, X264, X265) → U9_ggaaa(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
U9_ggaaa(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → U10_ggaaa(T152, T153, T156, X264, X265, pJ_in_ggaa(T156, T153, X264, X265))
pJ_in_ggaa(T156, T153, T161, X265) → U11_ggaa(T156, T153, T161, X265, divE_in_gga(T156, T153, T161))
U11_ggaa(T156, T153, T161, X265, divE_out_gga(T156, T153, T161)) → U12_ggaa(T156, T153, T161, X265, user_defined_=H_in_ag(X265, T161))
user_defined_=H_in_ag(s(T166), T166) → user_defined_=H_out_ag(s(T166), T166)
U12_ggaa(T156, T153, T161, X265, user_defined_=H_out_ag(X265, T161)) → pJ_out_ggaa(T156, T153, T161, X265)
U10_ggaaa(T152, T153, T156, X264, X265, pJ_out_ggaa(T156, T153, X264, X265)) → pF_out_ggaaa(T152, T153, T156, X264, X265)
U4_gga(T152, T153, X265, pF_out_ggaaa(T152, T153, X263, X264, X265)) → divE_out_gga(T152, T153, X265)
U7_ggaa(T45, T40, T127, T42, divE_out_gga(T45, T40, T127)) → U8_ggaa(T45, T40, T127, T42, user_defined_=G_in_ag(T42, T127))
user_defined_=G_in_ag(s(T172), T172) → user_defined_=G_out_ag(s(T172), T172)
U8_ggaa(T45, T40, T127, T42, user_defined_=G_out_ag(T42, T127)) → pI_out_ggaa(T45, T40, T127, T42)
U6_ggaaa(T39, T40, T45, X41, T42, pI_out_ggaa(T45, T40, X41, T42)) → pB_out_ggaaa(T39, T40, T45, X41, T42)
U1_gga(T39, T40, T42, pB_out_ggaaa(T39, T40, X40, X41, T42)) → divA_out_gga(T39, T40, T42)

The argument filtering Pi contains the following mapping:
divA_in_gga(x1, x2, x3)  =  divA_in_gga(x1, x2)
0  =  0
divA_out_gga(x1, x2, x3)  =  divA_out_gga(x1, x2, x3)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x6)
minusD_in_gga(x1, x2, x3)  =  minusD_in_gga(x1, x2)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3)  =  minusD_out_gga(x1, x2, x3)
U6_ggaaa(x1, x2, x3, x4, x5, x6)  =  U6_ggaaa(x1, x2, x3, x6)
pI_in_ggaa(x1, x2, x3, x4)  =  pI_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
divE_in_gga(x1, x2, x3)  =  divE_in_gga(x1, x2)
divE_out_gga(x1, x2, x3)  =  divE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pF_in_ggaaa(x1, x2, x3, x4, x5)  =  pF_in_ggaaa(x1, x2)
U9_ggaaa(x1, x2, x3, x4, x5, x6)  =  U9_ggaaa(x1, x2, x6)
U10_ggaaa(x1, x2, x3, x4, x5, x6)  =  U10_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
user_defined_=H_in_ag(x1, x2)  =  user_defined_=H_in_ag(x2)
user_defined_=H_out_ag(x1, x2)  =  user_defined_=H_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pF_out_ggaaa(x1, x2, x3, x4, x5)  =  pF_out_ggaaa(x1, x2, x3, x4, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
user_defined_=G_in_ag(x1, x2)  =  user_defined_=G_in_ag(x2)
user_defined_=G_out_ag(x1, x2)  =  user_defined_=G_out_ag(x1, x2)
pI_out_ggaa(x1, x2, x3, x4)  =  pI_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
DIVE_IN_GGA(x1, x2, x3)  =  DIVE_IN_GGA(x1, x2)
PF_IN_GGAAA(x1, x2, x3, x4, x5)  =  PF_IN_GGAAA(x1, x2)
U9_GGAAA(x1, x2, x3, x4, x5, x6)  =  U9_GGAAA(x1, x2, x6)
PJ_IN_GGAA(x1, x2, x3, x4)  =  PJ_IN_GGAA(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

PF_IN_GGAAA(T152, T153, T156, X264, X265) → U9_GGAAA(T152, T153, T156, X264, X265, minusD_in_gga(T152, T153, T156))
U9_GGAAA(T152, T153, T156, X264, X265, minusD_out_gga(T152, T153, T156)) → PJ_IN_GGAA(T156, T153, X264, X265)
PJ_IN_GGAA(T156, T153, T161, X265) → DIVE_IN_GGA(T156, T153, T161)
DIVE_IN_GGA(T152, T153, X265) → PF_IN_GGAAA(T152, T153, X263, X264, X265)

The TRS R consists of the following rules:

minusD_in_gga(s(T73), s(T80), X97) → U3_gga(T73, T80, X97, minusC_in_gga(T73, T80, X97))
U3_gga(T73, T80, X97, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
minusC_in_gga(0, T88, 0) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0, T103) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122), X182) → U2_gga(T115, T122, X182, minusC_in_gga(T115, T122, X182))
U2_gga(T115, T122, X182, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)

The argument filtering Pi contains the following mapping:
0  =  0
minusD_in_gga(x1, x2, x3)  =  minusD_in_gga(x1, x2)
s(x1)  =  s(x1)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3)  =  minusD_out_gga(x1, x2, x3)
DIVE_IN_GGA(x1, x2, x3)  =  DIVE_IN_GGA(x1, x2)
PF_IN_GGAAA(x1, x2, x3, x4, x5)  =  PF_IN_GGAAA(x1, x2)
U9_GGAAA(x1, x2, x3, x4, x5, x6)  =  U9_GGAAA(x1, x2, x6)
PJ_IN_GGAA(x1, x2, x3, x4)  =  PJ_IN_GGAA(x1, x2)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

PF_IN_GGAAA(T152, T153) → U9_GGAAA(T152, T153, minusD_in_gga(T152, T153))
U9_GGAAA(T152, T153, minusD_out_gga(T152, T153, T156)) → PJ_IN_GGAA(T156, T153)
PJ_IN_GGAA(T156, T153) → DIVE_IN_GGA(T156, T153)
DIVE_IN_GGA(T152, T153) → PF_IN_GGAAA(T152, T153)

The TRS R consists of the following rules:

minusD_in_gga(s(T73), s(T80)) → U3_gga(T73, T80, minusC_in_gga(T73, T80))
U3_gga(T73, T80, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
minusC_in_gga(0, T88) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122)) → U2_gga(T115, T122, minusC_in_gga(T115, T122))
U2_gga(T115, T122, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)

The set Q consists of the following terms:

minusD_in_gga(x0, x1)
U3_gga(x0, x1, x2)
minusC_in_gga(x0, x1)
U2_gga(x0, x1, x2)

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

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PF_IN_GGAAA(T152, T153) → U9_GGAAA(T152, T153, minusD_in_gga(T152, T153))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(DIVE_IN_GGA(x₁, x₂)) = 1 + x₁   
POL(PF_IN_GGAAA(x₁, x₂)) = 1 + x₁   
POL(PJ_IN_GGAA(x₁, x₂)) = 1 + x₁   
POL(U2_gga(x₁, x₂, x₃)) = 1 + x₃   
POL(U3_gga(x₁, x₂, x₃)) = x₃   
POL(U9_GGAAA(x₁, x₂, x₃)) = x₃   
POL(minusC_in_gga(x₁, x₂)) = 1 + x₁   
POL(minusC_out_gga(x₁, x₂, x₃)) = 1 + x₃   
POL(minusD_in_gga(x₁, x₂)) = x₁   
POL(minusD_out_gga(x₁, x₂, x₃)) = 1 + x₃   
POL(s(x₁)) = 1 + x₁   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

minusD_in_gga(s(T73), s(T80)) → U3_gga(T73, T80, minusC_in_gga(T73, T80))
minusC_in_gga(0, T88) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122)) → U2_gga(T115, T122, minusC_in_gga(T115, T122))
U3_gga(T73, T80, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
U2_gga(T115, T122, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)

(22) Obligation:

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

U9_GGAAA(T152, T153, minusD_out_gga(T152, T153, T156)) → PJ_IN_GGAA(T156, T153)
PJ_IN_GGAA(T156, T153) → DIVE_IN_GGA(T156, T153)
DIVE_IN_GGA(T152, T153) → PF_IN_GGAAA(T152, T153)

The TRS R consists of the following rules:

minusD_in_gga(s(T73), s(T80)) → U3_gga(T73, T80, minusC_in_gga(T73, T80))
U3_gga(T73, T80, minusC_out_gga(T73, T80, X97)) → minusD_out_gga(s(T73), s(T80), X97)
minusC_in_gga(0, T88) → minusC_out_gga(0, T88, 0)
minusC_in_gga(T103, 0) → minusC_out_gga(T103, 0, T103)
minusC_in_gga(s(T115), s(T122)) → U2_gga(T115, T122, minusC_in_gga(T115, T122))
U2_gga(T115, T122, minusC_out_gga(T115, T122, X182)) → minusC_out_gga(s(T115), s(T122), X182)

The set Q consists of the following terms:

minusD_in_gga(x0, x1)
U3_gga(x0, x1, x2)
minusC_in_gga(x0, x1)
U2_gga(x0, x1, x2)

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

(23) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(24) TRUE