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

(0) Obligation:

Clauses:

div(0, Y, 0) :- no(zero(Y)).
div(X, Y, s(Z)) :- ','(no(zero(X)), ','(no(zero(Y)), ','(minus(X, Y, U), div(U, Y, Z)))).
minus(0, Y, 0).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X1).
failure(b).

Query: div(g,g,a)

(1) 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];
5 [label="5: div(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: no(zero(T5)) | div(0, T5, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: div(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nX3 is free\ndiv(T1, T2, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: no(zero(T5)), SCOPE: 2, CLAUSE: 6 | no(zero(T5)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T5, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(call(zero(T8)), ','(!_2, failure(a))) | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(zero(T8), ','(!_2, failure(a))) | ?_3 | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(zero(T8), ','(!_2, failure(a))), SCOPE: 4, CLAUSE: 5 | ?_4 | ?_3 | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(!_2, failure(a)) | ?_4 | ?_3 | no(zero(0)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ?_4 | ?_3 | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: failure(a) | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: failure(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: failure(a), SCOPE: 5, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12))))\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 6 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(','(call(zero(0)), ','(!_6, failure(a))), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))) | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(zero(0), ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12))))) | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(zero(0), ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12))))), SCOPE: 8, CLAUSE: 5 | ?_8 | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))) | ?_8 | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12))))\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 9, CLAUSE: 8\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ?_3 | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: no(zero(T8)), SCOPE: 2, CLAUSE: 7\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(no(zero(0)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24))))\n\nT22 is ground\nX40 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(no(zero(0)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))), SCOPE: 10, CLAUSE: 6 | ','(no(zero(0)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))), SCOPE: 10, CLAUSE: 7\n\nT22 is ground\nX40 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(','(call(zero(0)), ','(!_10, failure(a))), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))) | ','(no(zero(0)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))), SCOPE: 10, CLAUSE: 7\n\nT22 is ground\nX40 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(zero(0), ','(','(!_10, failure(a)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24))))) | ?_11 | ','(no(zero(0)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))), SCOPE: 10, CLAUSE: 7\n\nT22 is ground\nX40 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(zero(0), ','(','(!_10, failure(a)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24))))), SCOPE: 12, CLAUSE: 5 | ?_12 | ?_11 | ','(no(zero(0)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))), SCOPE: 10, CLAUSE: 7\n\nT22 is ground\nX40 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(','(!_10, failure(a)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))) | ?_12 | ?_11 | ','(no(zero(0)), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))), SCOPE: 10, CLAUSE: 7\n\nT22 is ground\nX40 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(failure(a), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24))))\n\nT22 is ground\nX40 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(failure(a), ','(no(zero(T22)), ','(minus(0, T22, X40), div(X40, T22, T24)))), SCOPE: 13, CLAUSE: 8\n\nT22 is ground\nX40 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(no(zero(T32)), ','(no(zero(T33)), ','(minus(T32, T33, X54), div(X54, T33, T35))))\n\nT32 is ground\nT33 is ground\nX3 is free\nX54 is free\ndiv(T32, T33, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(no(zero(T32)), ','(no(zero(T33)), ','(minus(T32, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 6 | ','(no(zero(T32)), ','(no(zero(T33)), ','(minus(T32, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 7\n\nT32 is ground\nT33 is ground\nX3 is free\nX54 is free\ndiv(T32, T33, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(','(call(zero(T38)), ','(!_14, failure(a))), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35)))) | ','(no(zero(T38)), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 7\n\nT33 is ground\nT38 is ground\nX3 is free\nX54 is free\ndiv(T38, T33, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(zero(T38), ','(','(!_14, failure(a)), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35))))) | ?_15 | ','(no(zero(T38)), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 7\n\nT33 is ground\nT38 is ground\nX3 is free\nX54 is free\ndiv(T38, T33, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(zero(T38), ','(','(!_14, failure(a)), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35))))), SCOPE: 16, CLAUSE: 5 | ?_16 | ?_15 | ','(no(zero(T38)), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 7\n\nT33 is ground\nT38 is ground\nX3 is free\nX54 is free\ndiv(T38, T33, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(','(!_14, failure(a)), ','(no(zero(T33)), ','(minus(0, T33, X54), div(X54, T33, T35)))) | ?_16 | ?_15 | ','(no(zero(0)), ','(no(zero(T33)), ','(minus(0, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 7\n\nT33 is ground\nX3 is free\nX54 is free\ndiv(0, T33, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ?_16 | ?_15 | ','(no(zero(T38)), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 7\n\nT33 is ground\nT38 is ground\nX3 is free\nX54 is free\ndiv(T38, T33, T3) !=? div(0, X3, 0)\nzero(T38) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(failure(a), ','(no(zero(T33)), ','(minus(0, T33, X54), div(X54, T33, T35))))\n\nT33 is ground\nX3 is free\nX54 is free\ndiv(0, T33, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(failure(a), ','(no(zero(T33)), ','(minus(0, T33, X54), div(X54, T33, T35)))), SCOPE: 17, CLAUSE: 8\n\nT33 is ground\nX3 is free\nX54 is free\ndiv(0, T33, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ?_15 | ','(no(zero(T38)), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 7\n\nT33 is ground\nT38 is ground\nX3 is free\nX54 is free\ndiv(T38, T33, T3) !=? div(0, X3, 0)\nzero(T38) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(no(zero(T38)), ','(no(zero(T33)), ','(minus(T38, T33, X54), div(X54, T33, T35)))), SCOPE: 14, CLAUSE: 7\n\nT33 is ground\nT38 is ground\nX3 is free\nX54 is free\ndiv(T38, T33, T3) !=? div(0, X3, 0)\nzero(T38) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(no(zero(T33)), ','(minus(T47, T33, X54), div(X54, T33, T35)))\n\nT33 is ground\nT47 is ground\nX3 is free\nX54 is free\ndiv(T47, T33, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(no(zero(T33)), ','(minus(T47, T33, X54), div(X54, T33, T35))), SCOPE: 18, CLAUSE: 6 | ','(no(zero(T33)), ','(minus(T47, T33, X54), div(X54, T33, T35))), SCOPE: 18, CLAUSE: 7\n\nT33 is ground\nT47 is ground\nX3 is free\nX54 is free\ndiv(T47, T33, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(','(call(zero(T54)), ','(!_18, failure(a))), ','(minus(T47, T54, X54), div(X54, T54, T35))) | ','(no(zero(T54)), ','(minus(T47, T54, X54), div(X54, T54, T35))), SCOPE: 18, CLAUSE: 7\n\nT47 is ground\nT54 is ground\nX3 is free\nX54 is free\ndiv(T47, T54, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(zero(T54), ','(','(!_18, failure(a)), ','(minus(T47, T54, X54), div(X54, T54, T35)))) | ?_19 | ','(no(zero(T54)), ','(minus(T47, T54, X54), div(X54, T54, T35))), SCOPE: 18, CLAUSE: 7\n\nT47 is ground\nT54 is ground\nX3 is free\nX54 is free\ndiv(T47, T54, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(zero(T54), ','(','(!_18, failure(a)), ','(minus(T47, T54, X54), div(X54, T54, T35)))), SCOPE: 20, CLAUSE: 5 | ?_20 | ?_19 | ','(no(zero(T54)), ','(minus(T47, T54, X54), div(X54, T54, T35))), SCOPE: 18, CLAUSE: 7\n\nT47 is ground\nT54 is ground\nX3 is free\nX54 is free\ndiv(T47, T54, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: ','(','(!_18, failure(a)), ','(minus(T47, 0, X54), div(X54, 0, T35))) | ?_20 | ?_19 | ','(no(zero(0)), ','(minus(T47, 0, X54), div(X54, 0, T35))), SCOPE: 18, CLAUSE: 7\n\nT47 is ground\nX3 is free\nX54 is free\ndiv(T47, 0, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ?_20 | ?_19 | ','(no(zero(T54)), ','(minus(T47, T54, X54), div(X54, T54, T35))), SCOPE: 18, CLAUSE: 7\n\nT47 is ground\nT54 is ground\nX3 is free\nX54 is free\ndiv(T47, T54, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)\nzero(T54) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ','(failure(a), ','(minus(T47, 0, X54), div(X54, 0, T35)))\n\nT47 is ground\nX3 is free\nX54 is free\ndiv(T47, 0, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(failure(a), ','(minus(T47, 0, X54), div(X54, 0, T35))), SCOPE: 21, CLAUSE: 8\n\nT47 is ground\nX3 is free\nX54 is free\ndiv(T47, 0, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ?_19 | ','(no(zero(T54)), ','(minus(T47, T54, X54), div(X54, T54, T35))), SCOPE: 18, CLAUSE: 7\n\nT47 is ground\nT54 is ground\nX3 is free\nX54 is free\ndiv(T47, T54, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)\nzero(T54) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: ','(no(zero(T54)), ','(minus(T47, T54, X54), div(X54, T54, T35))), SCOPE: 18, CLAUSE: 7\n\nT47 is ground\nT54 is ground\nX3 is free\nX54 is free\ndiv(T47, T54, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)\nzero(T54) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="B: ','(minus(T47, T64, X54), div(X54, T64, T35))\n\nT47 is ground\nT64 is ground\nX3 is free\nX54 is free\ndiv(T47, T64, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)\nzero(T64) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="D: minus(T47, T64, X54)\n\nT47 is ground\nT64 is ground\nX3 is free\nX54 is free\ndiv(T47, T64, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)\nzero(T64) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: div(T71, T64, T35)\n\nT47 is ground\nT64 is ground\nT71 is ground\nX3 is free\ndiv(T47, T64, T3) !=? div(0, X3, 0)\nzero(T64) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: minus(T47, T64, X54), SCOPE: 22, CLAUSE: 2 | minus(T47, T64, X54), SCOPE: 22, CLAUSE: 3 | minus(T47, T64, X54), SCOPE: 22, CLAUSE: 4\n\nT47 is ground\nT64 is ground\nX3 is free\nX54 is free\ndiv(T47, T64, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)\nzero(T64) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: minus(T47, T64, X54), SCOPE: 22, CLAUSE: 3 | minus(T47, T64, X54), SCOPE: 22, CLAUSE: 4\n\nT47 is ground\nT64 is ground\nX3 is free\nX54 is free\ndiv(T47, T64, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)\nzero(T64) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: minus(T47, T64, X54), SCOPE: 22, CLAUSE: 4\n\nT47 is ground\nT64 is ground\nX3 is free\nX54 is free\ndiv(T47, T64, T3) !=? div(0, X3, 0)\nzero(T47) !=? zero(0)\nzero(T64) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="C: minus(T84, T85, X118)\n\nT84 is ground\nT85 is ground\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: minus(T84, T85, X118), SCOPE: 23, CLAUSE: 2 | minus(T84, T85, X118), SCOPE: 23, CLAUSE: 3 | minus(T84, T85, X118), SCOPE: 23, CLAUSE: 4\n\nT84 is ground\nT85 is ground\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: minus(T84, T85, X118), SCOPE: 23, CLAUSE: 2\n\nT84 is ground\nT85 is ground\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: minus(T84, T85, X118), SCOPE: 23, CLAUSE: 3 | minus(T84, T85, X118), SCOPE: 23, CLAUSE: 4\n\nT84 is ground\nT85 is ground\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: minus(T84, T85, X118), SCOPE: 23, CLAUSE: 3\n\nT84 is ground\nT85 is ground\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: minus(T84, T85, X118), SCOPE: 23, CLAUSE: 4\n\nT84 is ground\nT85 is ground\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: minus(T102, T103, X142)\n\nT102 is ground\nT103 is ground\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 222 [arrowhead = none ];
222 -> 5;

223 [label="EVAL with clause\ndiv(0, X3, 0) :- no(zero(X3)).\nand substitutionT1 -> 0,\nT2 -> T5,\nX3 -> T5,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 223 [arrowhead = none ];
223 -> 9;

224 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 224 [arrowhead = none ];
224 -> 13;

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

226 [label="EVAL with clause\ndiv(X51, X52, s(X53)) :- ','(no(zero(X51)), ','(no(zero(X52)), ','(minus(X51, X52, X54), div(X54, X52, X53)))).\nand substitutionT1 -> T32,\nX51 -> T32,\nT2 -> T33,\nX52 -> T33,\nX53 -> T35,\nT3 -> s(T35),\nT34 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 226 [arrowhead = none ];
226 -> 119;

227 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 227 [arrowhead = none ];
227 -> 123;

228 [label="ONLY EVAL with clause\nno(X6) :- ','(call(X6), ','(!_2, failure(a))).\nand substitutionT5 -> T8,\nX6 -> zero(T8)", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 228 [arrowhead = none ];
228 -> 19;

229 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 229 [arrowhead = none ];
229 -> 21;

230 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
21 -> 230 [arrowhead = none ];
230 -> 24;

231 [label="EVAL with clause\nzero(0).\nand substitutionT8 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 231 [arrowhead = none ];
231 -> 27;

232 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 232 [arrowhead = none ];
232 -> 28;

233 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 233 [arrowhead = none ];
233 -> 31;

234 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 234 [arrowhead = none ];
234 -> 71;

235 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 235 [arrowhead = none ];
235 -> 37;

236 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 236 [arrowhead = none ];
236 -> 38;

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

238 [label="EVAL with clause\ndiv(X14, X15, s(X16)) :- ','(no(zero(X14)), ','(no(zero(X15)), ','(minus(X14, X15, X17), div(X17, X15, X16)))).\nand substitutionX14 -> 0,\nX15 -> 0,\nX16 -> T12,\nT3 -> s(T12),\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 238 [arrowhead = none ];
238 -> 50;

239 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 239 [arrowhead = none ];
239 -> 53;

240 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 240 [arrowhead = none ];
240 -> 43;

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

242 [label="ONLY EVAL with clause\nno(X22) :- ','(call(X22), ','(!_6, failure(a))).\nand substitutionX22 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 242 [arrowhead = none ];
242 -> 59;

243 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 243 [arrowhead = none ];
243 -> 60;

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

245 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 245 [arrowhead = none ];
245 -> 64;

246 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 246 [arrowhead = none ];
246 -> 66;

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

248 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 248 [arrowhead = none ];
248 -> 70;

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

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

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

252 [label="ONLY EVAL with clause\nno(X29).\nand substitutionT8 -> T17,\nX29 -> zero(T17)", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 252 [arrowhead = none ];
252 -> 80;

253 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 253 [arrowhead = none ];
253 -> 83;

254 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 254 [arrowhead = none ];
254 -> 81;

255 [label="EVAL with clause\ndiv(X37, X38, s(X39)) :- ','(no(zero(X37)), ','(no(zero(X38)), ','(minus(X37, X38, X40), div(X40, X38, X39)))).\nand substitutionX37 -> 0,\nT8 -> T22,\nX38 -> T22,\nX39 -> T24,\nT3 -> s(T24),\nT23 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 255 [arrowhead = none ];
255 -> 92;

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

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

258 [label="ONLY EVAL with clause\nno(X45) :- ','(call(X45), ','(!_10, failure(a))).\nand substitutionX45 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 258 [arrowhead = none ];
258 -> 100;

259 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
100 -> 259 [arrowhead = none ];
259 -> 101;

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

261 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 261 [arrowhead = none ];
261 -> 104;

262 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 262 [arrowhead = none ];
262 -> 106;

263 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
106 -> 263 [arrowhead = none ];
263 -> 109;

264 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 264 [arrowhead = none ];
264 -> 111;

265 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
119 -> 265 [arrowhead = none ];
265 -> 125;

266 [label="ONLY EVAL with clause\nno(X57) :- ','(call(X57), ','(!_14, failure(a))).\nand substitutionT32 -> T38,\nX57 -> zero(T38)", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 266 [arrowhead = none ];
266 -> 132;

267 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
132 -> 267 [arrowhead = none ];
267 -> 133;

268 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
133 -> 268 [arrowhead = none ];
268 -> 135;

269 [label="EVAL with clause\nzero(0).\nand substitutionT38 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 269 [arrowhead = none ];
269 -> 137;

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

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

272 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 272 [arrowhead = none ];
272 -> 155;

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

274 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 274 [arrowhead = none ];
274 -> 153;

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

276 [label="ONLY EVAL with clause\nno(X66).\nand substitutionT38 -> T47,\nX66 -> zero(T47)", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 276 [arrowhead = none ];
276 -> 160;

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

278 [label="ONLY EVAL with clause\nno(X73) :- ','(call(X73), ','(!_18, failure(a))).\nand substitutionT33 -> T54,\nX73 -> zero(T54)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 278 [arrowhead = none ];
278 -> 166;

279 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
166 -> 279 [arrowhead = none ];
279 -> 168;

280 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
168 -> 280 [arrowhead = none ];
280 -> 170;

281 [label="EVAL with clause\nzero(0).\nand substitutionT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 281 [arrowhead = none ];
281 -> 173;

282 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
170 -> 282 [arrowhead = none ];
282 -> 174;

283 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 283 [arrowhead = none ];
283 -> 175;

284 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
174 -> 284 [arrowhead = none ];
284 -> 178;

285 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
175 -> 285 [arrowhead = none ];
285 -> 176;

286 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 286 [arrowhead = none ];
286 -> 177;

287 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
178 -> 287 [arrowhead = none ];
287 -> 180;

288 [label="ONLY EVAL with clause\nno(X88).\nand substitutionT54 -> T64,\nX88 -> zero(T64)", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 288 [arrowhead = none ];
288 -> 183;

289 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
183 -> 289 [arrowhead = none ];
289 -> 186;

290 [label="SPLIT 2\nnew knowledge:\nT47 is ground\nT64 is ground\nT71 is ground\nreplacements:X54 -> T71", fontsize=14, style = filled, fillcolor = violet];
183 -> 290 [arrowhead = none ];
290 -> 187;

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

292 [label="INSTANCE with matching:\nT1 -> T71\nT2 -> T64\nT3 -> T35", fontsize=14, style = filled, fillcolor = lightgrey];
187 -> 292 [arrowhead = none , style=dashed];
292 -> 1[style=dashed];

293 [label="BACKTRACK\nfor clause: minus(0, Y, 0)\nwith clash: (zero(T47), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
191 -> 293 [arrowhead = none ];
293 -> 192;

294 [label="BACKTRACK\nfor clause: minus(X, 0, X)\nwith clash: (zero(T64), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
192 -> 294 [arrowhead = none ];
294 -> 193;

295 [label="EVAL with clause\nminus(s(X115), s(X116), X117) :- minus(X115, X116, X117).\nand substitutionX115 -> T84,\nT47 -> s(T84),\nX116 -> T85,\nT64 -> s(T85),\nX54 -> X118,\nX117 -> X118", fontsize=14, style = filled, fillcolor = lightblue];
193 -> 295 [arrowhead = none ];
295 -> 195;

296 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
193 -> 296 [arrowhead = none ];
296 -> 197;

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

298 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
199 -> 298 [arrowhead = none ];
298 -> 200;

299 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
199 -> 299 [arrowhead = none ];
299 -> 201;

300 [label="EVAL with clause\nminus(0, X125, 0).\nand substitutionT84 -> 0,\nT85 -> T92,\nX125 -> T92,\nX118 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 300 [arrowhead = none ];
300 -> 203;

301 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 301 [arrowhead = none ];
301 -> 204;

302 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
201 -> 302 [arrowhead = none ];
302 -> 206;

303 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
201 -> 303 [arrowhead = none ];
303 -> 207;

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

305 [label="EVAL with clause\nminus(X130, 0, X130).\nand substitutionT84 -> T97,\nX130 -> T97,\nT85 -> 0,\nX118 -> T97", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 305 [arrowhead = none ];
305 -> 209;

306 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
206 -> 306 [arrowhead = none ];
306 -> 211;

307 [label="EVAL with clause\nminus(s(X139), s(X140), X141) :- minus(X139, X140, X141).\nand substitutionX139 -> T102,\nT84 -> s(T102),\nX140 -> T103,\nT85 -> s(T103),\nX118 -> X142,\nX141 -> X142", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 307 [arrowhead = none ];
307 -> 220;

308 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
207 -> 308 [arrowhead = none ];
308 -> 221;

309 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 309 [arrowhead = none ];
309 -> 212;

310 [label="INSTANCE with matching:\nT84 -> T102\nT85 -> T103\nX118 -> X142", fontsize=14, style = filled, fillcolor = lightgrey];
220 -> 310 [arrowhead = none , style=dashed];
310 -> 195[style=dashed];

}

(2) Obligation:

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

divA_in_gga(0, T17, 0) → divA_out_gga(0, T17, 0)
divA_in_gga(T47, T64, s(T35)) → U1_gga(T47, T64, T35, pB_in_ggaa(T47, T64, X54, T35))
pB_in_ggaa(T47, T64, T71, T35) → U4_ggaa(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
minusD_in_gga(s(T84), s(T85), X118) → U3_gga(T84, T85, X118, minusC_in_gga(T84, T85, X118))
minusC_in_gga(0, T92, 0) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0, T97) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103), X142) → U2_gga(T102, T103, X142, minusC_in_gga(T102, T103, X142))
U2_gga(T102, T103, X142, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)
U3_gga(T84, T85, X118, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
U4_ggaa(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → U5_ggaa(T47, T64, T71, T35, divA_in_gga(T71, T64, T35))
U5_ggaa(T47, T64, T71, T35, divA_out_gga(T71, T64, T35)) → pB_out_ggaa(T47, T64, T71, T35)
U1_gga(T47, T64, T35, pB_out_ggaa(T47, T64, X54, T35)) → divA_out_gga(T47, T64, s(T35))

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_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_ggaa(x1, x2, x5)
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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x3, x5)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

DIVA_IN_GGA(T47, T64, s(T35)) → U1_GGA(T47, T64, T35, pB_in_ggaa(T47, T64, X54, T35))
DIVA_IN_GGA(T47, T64, s(T35)) → PB_IN_GGAA(T47, T64, X54, T35)
PB_IN_GGAA(T47, T64, T71, T35) → U4_GGAA(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
PB_IN_GGAA(T47, T64, T71, T35) → MINUSD_IN_GGA(T47, T64, T71)
MINUSD_IN_GGA(s(T84), s(T85), X118) → U3_GGA(T84, T85, X118, minusC_in_gga(T84, T85, X118))
MINUSD_IN_GGA(s(T84), s(T85), X118) → MINUSC_IN_GGA(T84, T85, X118)
MINUSC_IN_GGA(s(T102), s(T103), X142) → U2_GGA(T102, T103, X142, minusC_in_gga(T102, T103, X142))
MINUSC_IN_GGA(s(T102), s(T103), X142) → MINUSC_IN_GGA(T102, T103, X142)
U4_GGAA(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → U5_GGAA(T47, T64, T71, T35, divA_in_gga(T71, T64, T35))
U4_GGAA(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → DIVA_IN_GGA(T71, T64, T35)

The TRS R consists of the following rules:

divA_in_gga(0, T17, 0) → divA_out_gga(0, T17, 0)
divA_in_gga(T47, T64, s(T35)) → U1_gga(T47, T64, T35, pB_in_ggaa(T47, T64, X54, T35))
pB_in_ggaa(T47, T64, T71, T35) → U4_ggaa(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
minusD_in_gga(s(T84), s(T85), X118) → U3_gga(T84, T85, X118, minusC_in_gga(T84, T85, X118))
minusC_in_gga(0, T92, 0) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0, T97) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103), X142) → U2_gga(T102, T103, X142, minusC_in_gga(T102, T103, X142))
U2_gga(T102, T103, X142, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)
U3_gga(T84, T85, X118, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
U4_ggaa(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → U5_ggaa(T47, T64, T71, T35, divA_in_gga(T71, T64, T35))
U5_ggaa(T47, T64, T71, T35, divA_out_gga(T71, T64, T35)) → pB_out_ggaa(T47, T64, T71, T35)
U1_gga(T47, T64, T35, pB_out_ggaa(T47, T64, X54, T35)) → divA_out_gga(T47, T64, s(T35))

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_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_ggaa(x1, x2, x5)
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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x3, x5)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
DIVA_IN_GGA(x1, x2, x3)  =  DIVA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x1, x2, x5)
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)
U5_GGAA(x1, x2, x3, x4, x5)  =  U5_GGAA(x1, x2, x3, x5)

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

(4) Obligation:

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

DIVA_IN_GGA(T47, T64, s(T35)) → U1_GGA(T47, T64, T35, pB_in_ggaa(T47, T64, X54, T35))
DIVA_IN_GGA(T47, T64, s(T35)) → PB_IN_GGAA(T47, T64, X54, T35)
PB_IN_GGAA(T47, T64, T71, T35) → U4_GGAA(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
PB_IN_GGAA(T47, T64, T71, T35) → MINUSD_IN_GGA(T47, T64, T71)
MINUSD_IN_GGA(s(T84), s(T85), X118) → U3_GGA(T84, T85, X118, minusC_in_gga(T84, T85, X118))
MINUSD_IN_GGA(s(T84), s(T85), X118) → MINUSC_IN_GGA(T84, T85, X118)
MINUSC_IN_GGA(s(T102), s(T103), X142) → U2_GGA(T102, T103, X142, minusC_in_gga(T102, T103, X142))
MINUSC_IN_GGA(s(T102), s(T103), X142) → MINUSC_IN_GGA(T102, T103, X142)
U4_GGAA(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → U5_GGAA(T47, T64, T71, T35, divA_in_gga(T71, T64, T35))
U4_GGAA(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → DIVA_IN_GGA(T71, T64, T35)

The TRS R consists of the following rules:

divA_in_gga(0, T17, 0) → divA_out_gga(0, T17, 0)
divA_in_gga(T47, T64, s(T35)) → U1_gga(T47, T64, T35, pB_in_ggaa(T47, T64, X54, T35))
pB_in_ggaa(T47, T64, T71, T35) → U4_ggaa(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
minusD_in_gga(s(T84), s(T85), X118) → U3_gga(T84, T85, X118, minusC_in_gga(T84, T85, X118))
minusC_in_gga(0, T92, 0) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0, T97) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103), X142) → U2_gga(T102, T103, X142, minusC_in_gga(T102, T103, X142))
U2_gga(T102, T103, X142, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)
U3_gga(T84, T85, X118, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
U4_ggaa(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → U5_ggaa(T47, T64, T71, T35, divA_in_gga(T71, T64, T35))
U5_ggaa(T47, T64, T71, T35, divA_out_gga(T71, T64, T35)) → pB_out_ggaa(T47, T64, T71, T35)
U1_gga(T47, T64, T35, pB_out_ggaa(T47, T64, X54, T35)) → divA_out_gga(T47, T64, s(T35))

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_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_ggaa(x1, x2, x5)
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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x3, x5)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
DIVA_IN_GGA(x1, x2, x3)  =  DIVA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x1, x2, x5)
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)
U5_GGAA(x1, x2, x3, x4, x5)  =  U5_GGAA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

MINUSC_IN_GGA(s(T102), s(T103), X142) → MINUSC_IN_GGA(T102, T103, X142)

The TRS R consists of the following rules:

divA_in_gga(0, T17, 0) → divA_out_gga(0, T17, 0)
divA_in_gga(T47, T64, s(T35)) → U1_gga(T47, T64, T35, pB_in_ggaa(T47, T64, X54, T35))
pB_in_ggaa(T47, T64, T71, T35) → U4_ggaa(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
minusD_in_gga(s(T84), s(T85), X118) → U3_gga(T84, T85, X118, minusC_in_gga(T84, T85, X118))
minusC_in_gga(0, T92, 0) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0, T97) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103), X142) → U2_gga(T102, T103, X142, minusC_in_gga(T102, T103, X142))
U2_gga(T102, T103, X142, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)
U3_gga(T84, T85, X118, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
U4_ggaa(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → U5_ggaa(T47, T64, T71, T35, divA_in_gga(T71, T64, T35))
U5_ggaa(T47, T64, T71, T35, divA_out_gga(T71, T64, T35)) → pB_out_ggaa(T47, T64, T71, T35)
U1_gga(T47, T64, T35, pB_out_ggaa(T47, T64, X54, T35)) → divA_out_gga(T47, T64, s(T35))

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_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_ggaa(x1, x2, x5)
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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x3, x5)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
MINUSC_IN_GGA(x1, x2, x3)  =  MINUSC_IN_GGA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

MINUSC_IN_GGA(s(T102), s(T103), X142) → MINUSC_IN_GGA(T102, T103, X142)

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

MINUSC_IN_GGA(s(T102), s(T103)) → MINUSC_IN_GGA(T102, T103)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(13) YES

(14) Obligation:

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

DIVA_IN_GGA(T47, T64, s(T35)) → PB_IN_GGAA(T47, T64, X54, T35)
PB_IN_GGAA(T47, T64, T71, T35) → U4_GGAA(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
U4_GGAA(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → DIVA_IN_GGA(T71, T64, T35)

The TRS R consists of the following rules:

divA_in_gga(0, T17, 0) → divA_out_gga(0, T17, 0)
divA_in_gga(T47, T64, s(T35)) → U1_gga(T47, T64, T35, pB_in_ggaa(T47, T64, X54, T35))
pB_in_ggaa(T47, T64, T71, T35) → U4_ggaa(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
minusD_in_gga(s(T84), s(T85), X118) → U3_gga(T84, T85, X118, minusC_in_gga(T84, T85, X118))
minusC_in_gga(0, T92, 0) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0, T97) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103), X142) → U2_gga(T102, T103, X142, minusC_in_gga(T102, T103, X142))
U2_gga(T102, T103, X142, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)
U3_gga(T84, T85, X118, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
U4_ggaa(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → U5_ggaa(T47, T64, T71, T35, divA_in_gga(T71, T64, T35))
U5_ggaa(T47, T64, T71, T35, divA_out_gga(T71, T64, T35)) → pB_out_ggaa(T47, T64, T71, T35)
U1_gga(T47, T64, T35, pB_out_ggaa(T47, T64, X54, T35)) → divA_out_gga(T47, T64, s(T35))

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_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U4_ggaa(x1, x2, x3, x4, x5)  =  U4_ggaa(x1, x2, x5)
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)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x3, x5)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
DIVA_IN_GGA(x1, x2, x3)  =  DIVA_IN_GGA(x1, x2)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x1, x2, x5)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

DIVA_IN_GGA(T47, T64, s(T35)) → PB_IN_GGAA(T47, T64, X54, T35)
PB_IN_GGAA(T47, T64, T71, T35) → U4_GGAA(T47, T64, T71, T35, minusD_in_gga(T47, T64, T71))
U4_GGAA(T47, T64, T71, T35, minusD_out_gga(T47, T64, T71)) → DIVA_IN_GGA(T71, T64, T35)

The TRS R consists of the following rules:

minusD_in_gga(s(T84), s(T85), X118) → U3_gga(T84, T85, X118, minusC_in_gga(T84, T85, X118))
U3_gga(T84, T85, X118, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
minusC_in_gga(0, T92, 0) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0, T97) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103), X142) → U2_gga(T102, T103, X142, minusC_in_gga(T102, T103, X142))
U2_gga(T102, T103, X142, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)

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)
DIVA_IN_GGA(x1, x2, x3)  =  DIVA_IN_GGA(x1, x2)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x1, x2, x5)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

DIVA_IN_GGA(T47, T64) → PB_IN_GGAA(T47, T64)
PB_IN_GGAA(T47, T64) → U4_GGAA(T47, T64, minusD_in_gga(T47, T64))
U4_GGAA(T47, T64, minusD_out_gga(T47, T64, T71)) → DIVA_IN_GGA(T71, T64)

The TRS R consists of the following rules:

minusD_in_gga(s(T84), s(T85)) → U3_gga(T84, T85, minusC_in_gga(T84, T85))
U3_gga(T84, T85, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
minusC_in_gga(0, T92) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103)) → U2_gga(T102, T103, minusC_in_gga(T102, T103))
U2_gga(T102, T103, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)

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.

(19) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

DIVA_IN_GGA(T47, T64) → PB_IN_GGAA(T47, T64)

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

POL(0) = 0   
POL(DIVA_IN_GGA(x₁, x₂)) = 1 + x₁   
POL(PB_IN_GGAA(x₁, x₂)) = x₁   
POL(U2_gga(x₁, x₂, x₃)) = x₃   
POL(U3_gga(x₁, x₂, x₃)) = 1 + x₃   
POL(U4_GGAA(x₁, x₂, x₃)) = x₃   
POL(minusC_in_gga(x₁, x₂)) = x₁   
POL(minusC_out_gga(x₁, x₂, x₃)) = 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(T84), s(T85)) → U3_gga(T84, T85, minusC_in_gga(T84, T85))
minusC_in_gga(0, T92) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103)) → U2_gga(T102, T103, minusC_in_gga(T102, T103))
U3_gga(T84, T85, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
U2_gga(T102, T103, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)

(20) Obligation:

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

PB_IN_GGAA(T47, T64) → U4_GGAA(T47, T64, minusD_in_gga(T47, T64))
U4_GGAA(T47, T64, minusD_out_gga(T47, T64, T71)) → DIVA_IN_GGA(T71, T64)

The TRS R consists of the following rules:

minusD_in_gga(s(T84), s(T85)) → U3_gga(T84, T85, minusC_in_gga(T84, T85))
U3_gga(T84, T85, minusC_out_gga(T84, T85, X118)) → minusD_out_gga(s(T84), s(T85), X118)
minusC_in_gga(0, T92) → minusC_out_gga(0, T92, 0)
minusC_in_gga(T97, 0) → minusC_out_gga(T97, 0, T97)
minusC_in_gga(s(T102), s(T103)) → U2_gga(T102, T103, minusC_in_gga(T102, T103))
U2_gga(T102, T103, minusC_out_gga(T102, T103, X142)) → minusC_out_gga(s(T102), s(T103), X142)

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) DependencyGraphProof (EQUIVALENT transformation)

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

(22) TRUE