Left Termination proof of /tmp/tmpH71HXM/binary.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 621 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 1481 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 16 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

(0) Obligation:

Clauses:

add(b, b, b).
add(X, b, X) :- binaryZ(X).
add(b, Y, Y) :- binaryZ(Y).
add(X, Y, Z) :- addz(X, Y, Z).
addx(one(X), b, one(X)) :- binary(X).
addx(zero(X), b, zero(X)) :- binaryZ(X).
addx(X, Y, Z) :- addz(X, Y, Z).
addy(b, one(Y), one(Y)) :- binary(Y).
addy(b, zero(Y), zero(Y)) :- binaryZ(Y).
addy(X, Y, Z) :- addz(X, Y, Z).
addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z).
addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z).
addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z).
addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z).
addc(b, b, one(b)).
addc(X, b, Z) :- succZ(X, Z).
addc(b, Y, Z) :- succZ(Y, Z).
addc(X, Y, Z) :- addC(X, Y, Z).
addX(zero(X), b, one(X)) :- binaryZ(X).
addX(one(X), b, zero(Z)) :- succ(X, Z).
addX(X, Y, Z) :- addC(X, Y, Z).
addY(b, zero(Y), one(Y)) :- binaryZ(Y).
addY(b, one(Y), zero(Z)) :- succ(Y, Z).
addY(X, Y, Z) :- addC(X, Y, Z).
addC(zero(X), zero(Y), one(Z)) :- addz(X, Y, Z).
addC(zero(X), one(Y), zero(Z)) :- addX(X, Y, Z).
addC(one(X), zero(Y), zero(Z)) :- addY(X, Y, Z).
addC(one(X), one(Y), one(Z)) :- addc(X, Y, Z).
binary(b).
binary(zero(X)) :- binaryZ(X).
binary(one(X)) :- binary(X).
binaryZ(zero(X)) :- binaryZ(X).
binaryZ(one(X)) :- binary(X).
succ(b, one(b)).
succ(zero(X), one(X)) :- binaryZ(X).
succ(one(X), zero(Z)) :- succ(X, Z).
succZ(zero(X), one(X)) :- binaryZ(X).
succZ(one(X), zero(Z)) :- succ(X, Z).
times(one(b), X, X).
times(zero(R), S, zero(RS)) :- times(R, S, RS).
times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS)).

Query: add(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: add(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: add(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | add(b, b, T3), SCOPE: 1, CLAUSE: 1 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: add(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nadd(T1, T2, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: add(b, b, T3), SCOPE: 1, CLAUSE: 1 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: binaryZ(b) | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: binaryZ(b), SCOPE: 2, CLAUSE: 31 | binaryZ(b), SCOPE: 2, CLAUSE: 32 | ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: binaryZ(b), SCOPE: 2, CLAUSE: 32 | ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: add(b, b, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="B: binaryZ(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: binaryZ(b), SCOPE: 3, CLAUSE: 31 | binaryZ(b), SCOPE: 3, CLAUSE: 32\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: binaryZ(b), SCOPE: 3, CLAUSE: 32\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="C: addz(b, b, T8)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: addz(b, b, T8), SCOPE: 4, CLAUSE: 10 | addz(b, b, T8), SCOPE: 4, CLAUSE: 11 | addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: addz(b, b, T8), SCOPE: 4, CLAUSE: 11 | addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: binaryZ(b) | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nX41 is free\nadd(b, b, T3) !=? add(X2, b, X2)\nadd(b, b, T3) !=? add(b, X41, X41)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: binaryZ(b), SCOPE: 5, CLAUSE: 31 | binaryZ(b), SCOPE: 5, CLAUSE: 32 | ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: binaryZ(b), SCOPE: 5, CLAUSE: 32 | ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: addz(b, b, T13)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: addz(b, b, T16)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: addz(b, b, T16), SCOPE: 6, CLAUSE: 10 | addz(b, b, T16), SCOPE: 6, CLAUSE: 11 | addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: addz(b, b, T16), SCOPE: 6, CLAUSE: 11 | addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: binaryZ(T18) | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX78 is free\nadd(T1, T2, T3) !=? add(b, b, b)\nadd(T1, T2, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: binaryZ(T18), SCOPE: 7, CLAUSE: 31 | binaryZ(T18), SCOPE: 7, CLAUSE: 32 | ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: binaryZ(T18), SCOPE: 7, CLAUSE: 31\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: binaryZ(T18), SCOPE: 7, CLAUSE: 32 | ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="D: binaryZ(T23)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: binaryZ(T23), SCOPE: 8, CLAUSE: 31 | binaryZ(T23), SCOPE: 8, CLAUSE: 32\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: binaryZ(T23), SCOPE: 8, CLAUSE: 31\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: binaryZ(T23), SCOPE: 8, CLAUSE: 32\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: binaryZ(T29)\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="E: binary(T33)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: binary(T33), SCOPE: 9, CLAUSE: 28 | binary(T33), SCOPE: 9, CLAUSE: 29 | binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: binary(T33), SCOPE: 9, CLAUSE: 28\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: binary(T33), SCOPE: 9, CLAUSE: 29 | binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: binary(T33), SCOPE: 9, CLAUSE: 29\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: binaryZ(T38)\n\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: binary(T42)\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: binaryZ(T18), SCOPE: 7, CLAUSE: 32\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: binary(T47)\n\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: add(T18, b, T3), SCOPE: 1, CLAUSE: 2\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: binaryZ(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: addz(T54, b, T56)\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: addz(T54, b, T56), SCOPE: 10, CLAUSE: 10 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 11 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 12 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 13\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: addz(T54, b, T56), SCOPE: 10, CLAUSE: 11 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 12 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 13\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: addz(T54, b, T56), SCOPE: 10, CLAUSE: 12 | addz(T54, b, T56), SCOPE: 10, CLAUSE: 13\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: addz(T54, b, T56), SCOPE: 10, CLAUSE: 13\n\nT54 is ground\nadd(T54, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: binaryZ(T63) | add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX78 is free\nX142 is free\nadd(T1, T2, T3) !=? add(b, b, b)\nadd(T1, T2, T3) !=? add(X78, b, X78)\nadd(T1, T2, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: binaryZ(T63), SCOPE: 11, CLAUSE: 31 | binaryZ(T63), SCOPE: 11, CLAUSE: 32 | ?_11 | add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: binaryZ(T63), SCOPE: 11, CLAUSE: 31\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: binaryZ(T63), SCOPE: 11, CLAUSE: 32 | ?_11 | add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: binaryZ(T68)\n\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: binaryZ(T63), SCOPE: 11, CLAUSE: 32\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: ?_11 | add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: binary(T74)\n\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: add(b, T63, T3), SCOPE: 1, CLAUSE: 3\n\nT63 is ground\nX78 is free\nadd(b, T63, T3) !=? add(b, b, b)\nadd(b, T63, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: addz(b, T80, T82)\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: addz(b, T80, T82), SCOPE: 12, CLAUSE: 10 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 11 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 12 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 13\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: addz(b, T80, T82), SCOPE: 12, CLAUSE: 11 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 12 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 13\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: addz(b, T80, T82), SCOPE: 12, CLAUSE: 12 | addz(b, T80, T82), SCOPE: 12, CLAUSE: 13\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: addz(b, T80, T82), SCOPE: 12, CLAUSE: 13\n\nT80 is ground\nX78 is free\nadd(b, T80, T3) !=? add(b, b, b)\nadd(b, T80, T3) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: addz(T86, T87, T89)\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 10 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 11 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 12 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 13\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 10\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 11 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 12 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 13\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="F: addz(T102, T103, T105)\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 10 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 11 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 12 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 13\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 10\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 11 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 12 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 13\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: addz(T121, T122, T124)\n\nT121 is ground\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 11\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 12 | addz(T102, T103, T105), SCOPE: 14, CLAUSE: 13\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
312 [label="G: addx(T140, T141, T143)\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
313 [label="313: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 4 | addx(T140, T141, T143), SCOPE: 15, CLAUSE: 5 | addx(T140, T141, T143), SCOPE: 15, CLAUSE: 6\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 4\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 5 | addx(T140, T141, T143), SCOPE: 15, CLAUSE: 6\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: binary(T149)\n\nT149 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 5\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: addx(T140, T141, T143), SCOPE: 15, CLAUSE: 6\n\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: binaryZ(T154)\n\nT154 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: addz(T166, T167, T169)\n\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
342 [label="342: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 12\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
343 [label="343: addz(T102, T103, T105), SCOPE: 14, CLAUSE: 13\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
348 [label="H: addy(T185, T186, T188)\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
352 [label="352: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 7 | addy(T185, T186, T188), SCOPE: 16, CLAUSE: 8 | addy(T185, T186, T188), SCOPE: 16, CLAUSE: 9\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
354 [label="354: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 7\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
355 [label="355: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 8 | addy(T185, T186, T188), SCOPE: 16, CLAUSE: 9\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
358 [label="358: binary(T194)\n\nT194 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
359 [label="359: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
364 [label="364: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 8\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: addy(T185, T186, T188), SCOPE: 16, CLAUSE: 9\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
367 [label="367: binaryZ(T199)\n\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
369 [label="369: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="373: addz(T211, T212, T214)\n\nT211 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="I: addc(T224, T225, T227)\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
377 [label="377: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 14 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 15 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 16 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 17\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
383 [label="383: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 14\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
384 [label="384: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 15 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 16 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 17\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
385 [label="385: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
386 [label="386: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
388 [label="388: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 15\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
390 [label="390: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 16 | addc(T224, T225, T227), SCOPE: 17, CLAUSE: 17\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
398 [label="K: succZ(T236, T238)\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
399 [label="399: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
404 [label="404: succZ(T236, T238), SCOPE: 18, CLAUSE: 36 | succZ(T236, T238), SCOPE: 18, CLAUSE: 37\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
405 [label="405: succZ(T236, T238), SCOPE: 18, CLAUSE: 36\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
406 [label="406: succZ(T236, T238), SCOPE: 18, CLAUSE: 37\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
408 [label="408: binaryZ(T244)\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
409 [label="409: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
414 [label="J: succ(T250, T252)\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
415 [label="415: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
420 [label="420: succ(T250, T252), SCOPE: 19, CLAUSE: 33 | succ(T250, T252), SCOPE: 19, CLAUSE: 34 | succ(T250, T252), SCOPE: 19, CLAUSE: 35\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
421 [label="421: succ(T250, T252), SCOPE: 19, CLAUSE: 33\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
422 [label="422: succ(T250, T252), SCOPE: 19, CLAUSE: 34 | succ(T250, T252), SCOPE: 19, CLAUSE: 35\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
423 [label="423: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
424 [label="424: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
425 [label="425: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
428 [label="428: succ(T250, T252), SCOPE: 19, CLAUSE: 34\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
430 [label="430: succ(T250, T252), SCOPE: 19, CLAUSE: 35\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
436 [label="436: binaryZ(T257)\n\nT257 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
437 [label="437: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
447 [label="447: succ(T263, T265)\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
448 [label="448: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 16\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
452 [label="452: addc(T224, T225, T227), SCOPE: 17, CLAUSE: 17\n\nT224 is ground\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
455 [label="455: succZ(T274, T276)\n\nT274 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
456 [label="456: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
463 [label="L: addC(T288, T289, T291)\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
465 [label="465: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 24 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 25 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 26 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 27\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
467 [label="467: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 24\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
468 [label="468: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 25 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 26 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 27\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
471 [label="471: addz(T307, T308, T310)\n\nT307 is ground\nT308 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
472 [label="472: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
476 [label="476: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 25\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
477 [label="477: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 26 | addC(T288, T289, T291), SCOPE: 20, CLAUSE: 27\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
480 [label="480: addX(T326, T327, T329)\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
481 [label="481: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
484 [label="484: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 18 | addX(T326, T327, T329), SCOPE: 21, CLAUSE: 19 | addX(T326, T327, T329), SCOPE: 21, CLAUSE: 20\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
485 [label="485: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 18\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
486 [label="486: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 19 | addX(T326, T327, T329), SCOPE: 21, CLAUSE: 20\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
487 [label="487: binaryZ(T335)\n\nT335 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
488 [label="488: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
493 [label="493: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 19\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
494 [label="494: addX(T326, T327, T329), SCOPE: 21, CLAUSE: 20\n\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
496 [label="496: succ(T345, T347)\n\nT345 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
497 [label="497: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
505 [label="505: addC(T358, T359, T361)\n\nT358 is ground\nT359 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
508 [label="508: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 26\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
509 [label="509: addC(T288, T289, T291), SCOPE: 20, CLAUSE: 27\n\nT288 is ground\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
512 [label="512: addY(T377, T378, T380)\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
514 [label="514: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
518 [label="518: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 21 | addY(T377, T378, T380), SCOPE: 22, CLAUSE: 22 | addY(T377, T378, T380), SCOPE: 22, CLAUSE: 23\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
520 [label="520: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 21\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
521 [label="521: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 22 | addY(T377, T378, T380), SCOPE: 22, CLAUSE: 23\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
523 [label="523: binaryZ(T386)\n\nT386 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
524 [label="524: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
525 [label="525: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 22\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
526 [label="526: addY(T377, T378, T380), SCOPE: 22, CLAUSE: 23\n\nT377 is ground\nT378 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
528 [label="528: succ(T396, T398)\n\nT396 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
529 [label="529: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
530 [label="530: addC(T409, T410, T412)\n\nT409 is ground\nT410 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
537 [label="537: addc(T422, T423, T425)\n\nT422 is ground\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
540 [label="540: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
545 [label="545: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 11\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
546 [label="546: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 12 | addz(T86, T87, T89), SCOPE: 13, CLAUSE: 13\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
551 [label="551: addx(T438, T439, T441)\n\nT438 is ground\nT439 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
552 [label="552: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
553 [label="553: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 12\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
554 [label="554: addz(T86, T87, T89), SCOPE: 13, CLAUSE: 13\n\nT86 is ground\nT87 is ground\nX78 is free\nX142 is free\nadd(T86, T87, T3) !=? add(b, b, b)\nadd(T86, T87, T3) !=? add(X78, b, X78)\nadd(T86, T87, T3) !=? add(b, X142, X142)", fontsize=16, style=filled, fillcolor=lightyellow];
556 [label="556: addy(T455, T456, T458)\n\nT455 is ground\nT456 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
557 [label="557: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
562 [label="562: addc(T466, T467, T469)\n\nT466 is ground\nT467 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
563 [label="563: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
564 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 564 [arrowhead = none ];
564 -> 4;

565 [label="EVAL with clause\nadd(b, b, b).\nand substitutionT1 -> b,\nT2 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 565 [arrowhead = none ];
565 -> 11;

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

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

568 [label="EVAL with clause\nadd(X78, b, X78) :- binaryZ(X78).\nand substitutionT1 -> T18,\nX78 -> T18,\nT2 -> b,\nT3 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 568 [arrowhead = none ];
568 -> 111;

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

570 [label="EVAL with clause\nadd(X2, b, X2) :- binaryZ(X2).\nand substitutionX2 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 570 [arrowhead = none ];
570 -> 21;

571 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 571 [arrowhead = none ];
571 -> 23;

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

573 [label="EVAL with clause\nadd(b, X41, X41) :- binaryZ(X41).\nand substitutionX41 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 573 [arrowhead = none ];
573 -> 67;

574 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 574 [arrowhead = none ];
574 -> 74;

575 [label="BACKTRACK\nfor clause: binaryZ(zero(X)) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 575 [arrowhead = none ];
575 -> 27;

576 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 576 [arrowhead = none ];
576 -> 28;

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

578 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 578 [arrowhead = none ];
578 -> 33;

579 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 579 [arrowhead = none ];
579 -> 35;

580 [label="EVAL with clause\nadd(b, X9, X9) :- binaryZ(X9).\nand substitutionX9 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 580 [arrowhead = none ];
580 -> 37;

581 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 581 [arrowhead = none ];
581 -> 39;

582 [label="ONLY EVAL with clause\nadd(X22, X23, X24) :- addz(X22, X23, X24).\nand substitutionX22 -> b,\nX23 -> b,\nT3 -> T8,\nX24 -> T8,\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 582 [arrowhead = none ];
582 -> 49;

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

584 [label="BACKTRACK\nfor clause: binaryZ(zero(X)) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 584 [arrowhead = none ];
584 -> 45;

585 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 585 [arrowhead = none ];
585 -> 47;

586 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
49 -> 586 [arrowhead = none ];
586 -> 53;

587 [label="BACKTRACK\nfor clause: addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 587 [arrowhead = none ];
587 -> 57;

588 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 588 [arrowhead = none ];
588 -> 59;

589 [label="BACKTRACK\nfor clause: addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 589 [arrowhead = none ];
589 -> 61;

590 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 590 [arrowhead = none ];
590 -> 63;

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

592 [label="ONLY EVAL with clause\nadd(X62, X63, X64) :- addz(X62, X63, X64).\nand substitutionX62 -> b,\nX63 -> b,\nT3 -> T16,\nX64 -> T16,\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 592 [arrowhead = none ];
592 -> 97;

593 [label="BACKTRACK\nfor clause: binaryZ(zero(X)) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 593 [arrowhead = none ];
593 -> 83;

594 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 594 [arrowhead = none ];
594 -> 85;

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

596 [label="ONLY EVAL with clause\nadd(X53, X54, X55) :- addz(X53, X54, X55).\nand substitutionX53 -> b,\nX54 -> b,\nT3 -> T13,\nX55 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 596 [arrowhead = none ];
596 -> 95;

597 [label="INSTANCE with matching:\nT8 -> T13", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 597 [arrowhead = none , style=dashed];
597 -> 49[style=dashed];

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

599 [label="BACKTRACK\nfor clause: addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 599 [arrowhead = none ];
599 -> 102;

600 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 600 [arrowhead = none ];
600 -> 104;

601 [label="BACKTRACK\nfor clause: addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 601 [arrowhead = none ];
601 -> 107;

602 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 602 [arrowhead = none ];
602 -> 109;

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

604 [label="EVAL with clause\nadd(b, X142, X142) :- binaryZ(X142).\nand substitutionT1 -> b,\nT2 -> T63,\nX142 -> T63,\nT3 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 604 [arrowhead = none ];
604 -> 213;

605 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 605 [arrowhead = none ];
605 -> 217;

606 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
116 -> 606 [arrowhead = none ];
606 -> 119;

607 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
116 -> 607 [arrowhead = none ];
607 -> 120;

608 [label="EVAL with clause\nbinaryZ(zero(X83)) :- binaryZ(X83).\nand substitutionX83 -> T23,\nT18 -> zero(T23)", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 608 [arrowhead = none ];
608 -> 123;

609 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 609 [arrowhead = none ];
609 -> 124;

610 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
120 -> 610 [arrowhead = none ];
610 -> 174;

611 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
120 -> 611 [arrowhead = none ];
611 -> 175;

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

613 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
127 -> 613 [arrowhead = none ];
613 -> 131;

614 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
127 -> 614 [arrowhead = none ];
614 -> 132;

615 [label="EVAL with clause\nbinaryZ(zero(X89)) :- binaryZ(X89).\nand substitutionX89 -> T29,\nT23 -> zero(T29)", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 615 [arrowhead = none ];
615 -> 135;

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

617 [label="EVAL with clause\nbinaryZ(one(X93)) :- binary(X93).\nand substitutionX93 -> T33,\nT23 -> one(T33)", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 617 [arrowhead = none ];
617 -> 139;

618 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 618 [arrowhead = none ];
618 -> 140;

619 [label="INSTANCE with matching:\nT23 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
135 -> 619 [arrowhead = none , style=dashed];
619 -> 123[style=dashed];

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

621 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
145 -> 621 [arrowhead = none ];
621 -> 146;

622 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
145 -> 622 [arrowhead = none ];
622 -> 147;

623 [label="EVAL with clause\nbinary(b).\nand substitutionT33 -> b", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 623 [arrowhead = none ];
623 -> 148;

624 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
146 -> 624 [arrowhead = none ];
624 -> 149;

625 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
147 -> 625 [arrowhead = none ];
625 -> 157;

626 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
147 -> 626 [arrowhead = none ];
626 -> 158;

627 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 627 [arrowhead = none ];
627 -> 150;

628 [label="EVAL with clause\nbinary(zero(X98)) :- binaryZ(X98).\nand substitutionX98 -> T38,\nT33 -> zero(T38)", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 628 [arrowhead = none ];
628 -> 161;

629 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 629 [arrowhead = none ];
629 -> 162;

630 [label="EVAL with clause\nbinary(one(X102)) :- binary(X102).\nand substitutionX102 -> T42,\nT33 -> one(T42)", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 630 [arrowhead = none ];
630 -> 167;

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

632 [label="INSTANCE with matching:\nT23 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
161 -> 632 [arrowhead = none , style=dashed];
632 -> 123[style=dashed];

633 [label="INSTANCE with matching:\nT33 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
167 -> 633 [arrowhead = none , style=dashed];
633 -> 139[style=dashed];

634 [label="EVAL with clause\nbinaryZ(one(X107)) :- binary(X107).\nand substitutionX107 -> T47,\nT18 -> one(T47)", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 634 [arrowhead = none ];
634 -> 178;

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

636 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
175 -> 636 [arrowhead = none ];
636 -> 184;

637 [label="INSTANCE with matching:\nT33 -> T47", fontsize=14, style = filled, fillcolor = lightgrey];
178 -> 637 [arrowhead = none , style=dashed];
637 -> 139[style=dashed];

638 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
184 -> 638 [arrowhead = none ];
638 -> 187;

639 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
184 -> 639 [arrowhead = none ];
639 -> 189;

640 [label="EVAL with clause\nadd(b, X112, X112) :- binaryZ(X112).\nand substitutionT18 -> b,\nX112 -> b,\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
187 -> 640 [arrowhead = none ];
640 -> 193;

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

642 [label="ONLY EVAL with clause\nadd(X123, X124, X125) :- addz(X123, X124, X125).\nand substitutionT18 -> T54,\nX123 -> T54,\nX124 -> b,\nT3 -> T56,\nX125 -> T56,\nT55 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 642 [arrowhead = none ];
642 -> 199;

643 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
193 -> 643 [arrowhead = none , style=dashed];
643 -> 37[style=dashed];

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

645 [label="BACKTRACK\nfor clause: addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 645 [arrowhead = none ];
645 -> 203;

646 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
203 -> 646 [arrowhead = none ];
646 -> 207;

647 [label="BACKTRACK\nfor clause: addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
207 -> 647 [arrowhead = none ];
647 -> 209;

648 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 648 [arrowhead = none ];
648 -> 210;

649 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
213 -> 649 [arrowhead = none ];
649 -> 219;

650 [label="ONLY EVAL with clause\nadd(X184, X185, X186) :- addz(X184, X185, X186).\nand substitutionT1 -> T86,\nX184 -> T86,\nT2 -> T87,\nX185 -> T87,\nT3 -> T89,\nX186 -> T89,\nT88 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
217 -> 650 [arrowhead = none ];
650 -> 268;

651 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
219 -> 651 [arrowhead = none ];
651 -> 224;

652 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
219 -> 652 [arrowhead = none ];
652 -> 225;

653 [label="EVAL with clause\nbinaryZ(zero(X147)) :- binaryZ(X147).\nand substitutionX147 -> T68,\nT63 -> zero(T68)", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 653 [arrowhead = none ];
653 -> 230;

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

655 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
225 -> 655 [arrowhead = none ];
655 -> 237;

656 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
225 -> 656 [arrowhead = none ];
656 -> 239;

657 [label="INSTANCE with matching:\nT23 -> T68", fontsize=14, style = filled, fillcolor = lightgrey];
230 -> 657 [arrowhead = none , style=dashed];
657 -> 123[style=dashed];

658 [label="EVAL with clause\nbinaryZ(one(X153)) :- binary(X153).\nand substitutionX153 -> T74,\nT63 -> one(T74)", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 658 [arrowhead = none ];
658 -> 242;

659 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
237 -> 659 [arrowhead = none ];
659 -> 243;

660 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
239 -> 660 [arrowhead = none ];
660 -> 247;

661 [label="INSTANCE with matching:\nT33 -> T74", fontsize=14, style = filled, fillcolor = lightgrey];
242 -> 661 [arrowhead = none , style=dashed];
661 -> 139[style=dashed];

662 [label="ONLY EVAL with clause\nadd(X163, X164, X165) :- addz(X163, X164, X165).\nand substitutionX163 -> b,\nT63 -> T80,\nX164 -> T80,\nT3 -> T82,\nX165 -> T82,\nT81 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
247 -> 662 [arrowhead = none ];
662 -> 249;

663 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
249 -> 663 [arrowhead = none ];
663 -> 253;

664 [label="BACKTRACK\nfor clause: addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
253 -> 664 [arrowhead = none ];
664 -> 258;

665 [label="BACKTRACK\nfor clause: addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
258 -> 665 [arrowhead = none ];
665 -> 262;

666 [label="BACKTRACK\nfor clause: addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
262 -> 666 [arrowhead = none ];
666 -> 264;

667 [label="BACKTRACK\nfor clause: addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
264 -> 667 [arrowhead = none ];
667 -> 265;

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

669 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
270 -> 669 [arrowhead = none ];
669 -> 275;

670 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
270 -> 670 [arrowhead = none ];
670 -> 277;

671 [label="EVAL with clause\naddz(zero(X199), zero(X200), zero(X201)) :- addz(X199, X200, X201).\nand substitutionX199 -> T102,\nT86 -> zero(T102),\nX200 -> T103,\nT87 -> zero(T103),\nX201 -> T105,\nT89 -> zero(T105),\nT104 -> T105", fontsize=14, style = filled, fillcolor = lightblue];
275 -> 671 [arrowhead = none ];
671 -> 284;

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

673 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
277 -> 673 [arrowhead = none ];
673 -> 545;

674 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
277 -> 674 [arrowhead = none ];
674 -> 546;

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

676 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
288 -> 676 [arrowhead = none ];
676 -> 290;

677 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
288 -> 677 [arrowhead = none ];
677 -> 291;

678 [label="EVAL with clause\naddz(zero(X217), zero(X218), zero(X219)) :- addz(X217, X218, X219).\nand substitutionX217 -> T121,\nT102 -> zero(T121),\nX218 -> T122,\nT103 -> zero(T122),\nX219 -> T124,\nT105 -> zero(T124),\nT123 -> T124", fontsize=14, style = filled, fillcolor = lightblue];
290 -> 678 [arrowhead = none ];
678 -> 296;

679 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
290 -> 679 [arrowhead = none ];
679 -> 297;

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

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

682 [label="INSTANCE with matching:\nT102 -> T121\nT103 -> T122\nT105 -> T124", fontsize=14, style = filled, fillcolor = lightgrey];
296 -> 682 [arrowhead = none , style=dashed];
682 -> 284[style=dashed];

683 [label="EVAL with clause\naddz(zero(X235), one(X236), one(X237)) :- addx(X235, X236, X237).\nand substitutionX235 -> T140,\nT102 -> zero(T140),\nX236 -> T141,\nT103 -> one(T141),\nX237 -> T143,\nT105 -> one(T143),\nT142 -> T143", fontsize=14, style = filled, fillcolor = lightblue];
302 -> 683 [arrowhead = none ];
683 -> 312;

684 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
302 -> 684 [arrowhead = none ];
684 -> 313;

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

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

687 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
312 -> 687 [arrowhead = none ];
687 -> 316;

688 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
316 -> 688 [arrowhead = none ];
688 -> 318;

689 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
316 -> 689 [arrowhead = none ];
689 -> 319;

690 [label="EVAL with clause\naddx(one(X243), b, one(X243)) :- binary(X243).\nand substitutionX243 -> T149,\nT140 -> one(T149),\nT141 -> b,\nT143 -> one(T149)", fontsize=14, style = filled, fillcolor = lightblue];
318 -> 690 [arrowhead = none ];
690 -> 322;

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

692 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
319 -> 692 [arrowhead = none ];
692 -> 328;

693 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
319 -> 693 [arrowhead = none ];
693 -> 329;

694 [label="INSTANCE with matching:\nT33 -> T149", fontsize=14, style = filled, fillcolor = lightgrey];
322 -> 694 [arrowhead = none , style=dashed];
694 -> 139[style=dashed];

695 [label="EVAL with clause\naddx(zero(X248), b, zero(X248)) :- binaryZ(X248).\nand substitutionX248 -> T154,\nT140 -> zero(T154),\nT141 -> b,\nT143 -> zero(T154)", fontsize=14, style = filled, fillcolor = lightblue];
328 -> 695 [arrowhead = none ];
695 -> 334;

696 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
328 -> 696 [arrowhead = none ];
696 -> 335;

697 [label="ONLY EVAL with clause\naddx(X259, X260, X261) :- addz(X259, X260, X261).\nand substitutionT140 -> T166,\nX259 -> T166,\nT141 -> T167,\nX260 -> T167,\nT143 -> T169,\nX261 -> T169,\nT168 -> T169", fontsize=14, style = filled, fillcolor = lightblue];
329 -> 697 [arrowhead = none ];
697 -> 340;

698 [label="INSTANCE with matching:\nT23 -> T154", fontsize=14, style = filled, fillcolor = lightgrey];
334 -> 698 [arrowhead = none , style=dashed];
698 -> 123[style=dashed];

699 [label="INSTANCE with matching:\nT102 -> T166\nT103 -> T167\nT105 -> T169", fontsize=14, style = filled, fillcolor = lightgrey];
340 -> 699 [arrowhead = none , style=dashed];
699 -> 284[style=dashed];

700 [label="EVAL with clause\naddz(one(X277), zero(X278), one(X279)) :- addy(X277, X278, X279).\nand substitutionX277 -> T185,\nT102 -> one(T185),\nX278 -> T186,\nT103 -> zero(T186),\nX279 -> T188,\nT105 -> one(T188),\nT187 -> T188", fontsize=14, style = filled, fillcolor = lightblue];
342 -> 700 [arrowhead = none ];
700 -> 348;

701 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
342 -> 701 [arrowhead = none ];
701 -> 349;

702 [label="EVAL with clause\naddz(one(X313), one(X314), zero(X315)) :- addc(X313, X314, X315).\nand substitutionX313 -> T224,\nT102 -> one(T224),\nX314 -> T225,\nT103 -> one(T225),\nX315 -> T227,\nT105 -> zero(T227),\nT226 -> T227", fontsize=14, style = filled, fillcolor = lightblue];
343 -> 702 [arrowhead = none ];
702 -> 376;

703 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
343 -> 703 [arrowhead = none ];
703 -> 377;

704 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
348 -> 704 [arrowhead = none ];
704 -> 352;

705 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
352 -> 705 [arrowhead = none ];
705 -> 354;

706 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
352 -> 706 [arrowhead = none ];
706 -> 355;

707 [label="EVAL with clause\naddy(b, one(X285), one(X285)) :- binary(X285).\nand substitutionT185 -> b,\nX285 -> T194,\nT186 -> one(T194),\nT188 -> one(T194)", fontsize=14, style = filled, fillcolor = lightblue];
354 -> 707 [arrowhead = none ];
707 -> 358;

708 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
354 -> 708 [arrowhead = none ];
708 -> 359;

709 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
355 -> 709 [arrowhead = none ];
709 -> 364;

710 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
355 -> 710 [arrowhead = none ];
710 -> 365;

711 [label="INSTANCE with matching:\nT33 -> T194", fontsize=14, style = filled, fillcolor = lightgrey];
358 -> 711 [arrowhead = none , style=dashed];
711 -> 139[style=dashed];

712 [label="EVAL with clause\naddy(b, zero(X290), zero(X290)) :- binaryZ(X290).\nand substitutionT185 -> b,\nX290 -> T199,\nT186 -> zero(T199),\nT188 -> zero(T199)", fontsize=14, style = filled, fillcolor = lightblue];
364 -> 712 [arrowhead = none ];
712 -> 367;

713 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
364 -> 713 [arrowhead = none ];
713 -> 369;

714 [label="ONLY EVAL with clause\naddy(X301, X302, X303) :- addz(X301, X302, X303).\nand substitutionT185 -> T211,\nX301 -> T211,\nT186 -> T212,\nX302 -> T212,\nT188 -> T214,\nX303 -> T214,\nT213 -> T214", fontsize=14, style = filled, fillcolor = lightblue];
365 -> 714 [arrowhead = none ];
714 -> 373;

715 [label="INSTANCE with matching:\nT23 -> T199", fontsize=14, style = filled, fillcolor = lightgrey];
367 -> 715 [arrowhead = none , style=dashed];
715 -> 123[style=dashed];

716 [label="INSTANCE with matching:\nT102 -> T211\nT103 -> T212\nT105 -> T214", fontsize=14, style = filled, fillcolor = lightgrey];
373 -> 716 [arrowhead = none , style=dashed];
716 -> 284[style=dashed];

717 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
376 -> 717 [arrowhead = none ];
717 -> 382;

718 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
382 -> 718 [arrowhead = none ];
718 -> 383;

719 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
382 -> 719 [arrowhead = none ];
719 -> 384;

720 [label="EVAL with clause\naddc(b, b, one(b)).\nand substitutionT224 -> b,\nT225 -> b,\nT227 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
383 -> 720 [arrowhead = none ];
720 -> 385;

721 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
383 -> 721 [arrowhead = none ];
721 -> 386;

722 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
384 -> 722 [arrowhead = none ];
722 -> 388;

723 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
384 -> 723 [arrowhead = none ];
723 -> 390;

724 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
385 -> 724 [arrowhead = none ];
724 -> 387;

725 [label="EVAL with clause\naddc(X324, b, X325) :- succZ(X324, X325).\nand substitutionT224 -> T236,\nX324 -> T236,\nT225 -> b,\nT227 -> T238,\nX325 -> T238,\nT237 -> T238", fontsize=14, style = filled, fillcolor = lightblue];
388 -> 725 [arrowhead = none ];
725 -> 398;

726 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
388 -> 726 [arrowhead = none ];
726 -> 399;

727 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
390 -> 727 [arrowhead = none ];
727 -> 451;

728 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
390 -> 728 [arrowhead = none ];
728 -> 452;

729 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
398 -> 729 [arrowhead = none ];
729 -> 404;

730 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
404 -> 730 [arrowhead = none ];
730 -> 405;

731 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
404 -> 731 [arrowhead = none ];
731 -> 406;

732 [label="EVAL with clause\nsuccZ(zero(X331), one(X331)) :- binaryZ(X331).\nand substitutionX331 -> T244,\nT236 -> zero(T244),\nT238 -> one(T244)", fontsize=14, style = filled, fillcolor = lightblue];
405 -> 732 [arrowhead = none ];
732 -> 408;

733 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
405 -> 733 [arrowhead = none ];
733 -> 409;

734 [label="EVAL with clause\nsuccZ(one(X337), zero(X338)) :- succ(X337, X338).\nand substitutionX337 -> T250,\nT236 -> one(T250),\nX338 -> T252,\nT238 -> zero(T252),\nT251 -> T252", fontsize=14, style = filled, fillcolor = lightblue];
406 -> 734 [arrowhead = none ];
734 -> 414;

735 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
406 -> 735 [arrowhead = none ];
735 -> 415;

736 [label="INSTANCE with matching:\nT23 -> T244", fontsize=14, style = filled, fillcolor = lightgrey];
408 -> 736 [arrowhead = none , style=dashed];
736 -> 123[style=dashed];

737 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
414 -> 737 [arrowhead = none ];
737 -> 420;

738 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
420 -> 738 [arrowhead = none ];
738 -> 421;

739 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
420 -> 739 [arrowhead = none ];
739 -> 422;

740 [label="EVAL with clause\nsucc(b, one(b)).\nand substitutionT250 -> b,\nT252 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
421 -> 740 [arrowhead = none ];
740 -> 423;

741 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
421 -> 741 [arrowhead = none ];
741 -> 424;

742 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
422 -> 742 [arrowhead = none ];
742 -> 428;

743 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
422 -> 743 [arrowhead = none ];
743 -> 430;

744 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
423 -> 744 [arrowhead = none ];
744 -> 425;

745 [label="EVAL with clause\nsucc(zero(X343), one(X343)) :- binaryZ(X343).\nand substitutionX343 -> T257,\nT250 -> zero(T257),\nT252 -> one(T257)", fontsize=14, style = filled, fillcolor = lightblue];
428 -> 745 [arrowhead = none ];
745 -> 436;

746 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
428 -> 746 [arrowhead = none ];
746 -> 437;

747 [label="EVAL with clause\nsucc(one(X349), zero(X350)) :- succ(X349, X350).\nand substitutionX349 -> T263,\nT250 -> one(T263),\nX350 -> T265,\nT252 -> zero(T265),\nT264 -> T265", fontsize=14, style = filled, fillcolor = lightblue];
430 -> 747 [arrowhead = none ];
747 -> 447;

748 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
430 -> 748 [arrowhead = none ];
748 -> 448;

749 [label="INSTANCE with matching:\nT23 -> T257", fontsize=14, style = filled, fillcolor = lightgrey];
436 -> 749 [arrowhead = none , style=dashed];
749 -> 123[style=dashed];

750 [label="INSTANCE with matching:\nT250 -> T263\nT252 -> T265", fontsize=14, style = filled, fillcolor = lightgrey];
447 -> 750 [arrowhead = none , style=dashed];
750 -> 414[style=dashed];

751 [label="EVAL with clause\naddc(b, X359, X360) :- succZ(X359, X360).\nand substitutionT224 -> b,\nT225 -> T274,\nX359 -> T274,\nT227 -> T276,\nX360 -> T276,\nT275 -> T276", fontsize=14, style = filled, fillcolor = lightblue];
451 -> 751 [arrowhead = none ];
751 -> 455;

752 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
451 -> 752 [arrowhead = none ];
752 -> 456;

753 [label="ONLY EVAL with clause\naddc(X371, X372, X373) :- addC(X371, X372, X373).\nand substitutionT224 -> T288,\nX371 -> T288,\nT225 -> T289,\nX372 -> T289,\nT227 -> T291,\nX373 -> T291,\nT290 -> T291", fontsize=14, style = filled, fillcolor = lightblue];
452 -> 753 [arrowhead = none ];
753 -> 463;

754 [label="INSTANCE with matching:\nT236 -> T274\nT238 -> T276", fontsize=14, style = filled, fillcolor = lightgrey];
455 -> 754 [arrowhead = none , style=dashed];
754 -> 398[style=dashed];

755 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
463 -> 755 [arrowhead = none ];
755 -> 465;

756 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
465 -> 756 [arrowhead = none ];
756 -> 467;

757 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
465 -> 757 [arrowhead = none ];
757 -> 468;

758 [label="EVAL with clause\naddC(zero(X389), zero(X390), one(X391)) :- addz(X389, X390, X391).\nand substitutionX389 -> T307,\nT288 -> zero(T307),\nX390 -> T308,\nT289 -> zero(T308),\nX391 -> T310,\nT291 -> one(T310),\nT309 -> T310", fontsize=14, style = filled, fillcolor = lightblue];
467 -> 758 [arrowhead = none ];
758 -> 471;

759 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
467 -> 759 [arrowhead = none ];
759 -> 472;

760 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
468 -> 760 [arrowhead = none ];
760 -> 476;

761 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
468 -> 761 [arrowhead = none ];
761 -> 477;

762 [label="INSTANCE with matching:\nT102 -> T307\nT103 -> T308\nT105 -> T310", fontsize=14, style = filled, fillcolor = lightgrey];
471 -> 762 [arrowhead = none , style=dashed];
762 -> 284[style=dashed];

763 [label="EVAL with clause\naddC(zero(X407), one(X408), zero(X409)) :- addX(X407, X408, X409).\nand substitutionX407 -> T326,\nT288 -> zero(T326),\nX408 -> T327,\nT289 -> one(T327),\nX409 -> T329,\nT291 -> zero(T329),\nT328 -> T329", fontsize=14, style = filled, fillcolor = lightblue];
476 -> 763 [arrowhead = none ];
763 -> 480;

764 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
476 -> 764 [arrowhead = none ];
764 -> 481;

765 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
477 -> 765 [arrowhead = none ];
765 -> 508;

766 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
477 -> 766 [arrowhead = none ];
766 -> 509;

767 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
480 -> 767 [arrowhead = none ];
767 -> 484;

768 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
484 -> 768 [arrowhead = none ];
768 -> 485;

769 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
484 -> 769 [arrowhead = none ];
769 -> 486;

770 [label="EVAL with clause\naddX(zero(X415), b, one(X415)) :- binaryZ(X415).\nand substitutionX415 -> T335,\nT326 -> zero(T335),\nT327 -> b,\nT329 -> one(T335)", fontsize=14, style = filled, fillcolor = lightblue];
485 -> 770 [arrowhead = none ];
770 -> 487;

771 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
485 -> 771 [arrowhead = none ];
771 -> 488;

772 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
486 -> 772 [arrowhead = none ];
772 -> 493;

773 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
486 -> 773 [arrowhead = none ];
773 -> 494;

774 [label="INSTANCE with matching:\nT23 -> T335", fontsize=14, style = filled, fillcolor = lightgrey];
487 -> 774 [arrowhead = none , style=dashed];
774 -> 123[style=dashed];

775 [label="EVAL with clause\naddX(one(X425), b, zero(X426)) :- succ(X425, X426).\nand substitutionX425 -> T345,\nT326 -> one(T345),\nT327 -> b,\nX426 -> T347,\nT329 -> zero(T347),\nT346 -> T347", fontsize=14, style = filled, fillcolor = lightblue];
493 -> 775 [arrowhead = none ];
775 -> 496;

776 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
493 -> 776 [arrowhead = none ];
776 -> 497;

777 [label="ONLY EVAL with clause\naddX(X436, X437, X438) :- addC(X436, X437, X438).\nand substitutionT326 -> T358,\nX436 -> T358,\nT327 -> T359,\nX437 -> T359,\nT329 -> T361,\nX438 -> T361,\nT360 -> T361", fontsize=14, style = filled, fillcolor = lightblue];
494 -> 777 [arrowhead = none ];
777 -> 505;

778 [label="INSTANCE with matching:\nT250 -> T345\nT252 -> T347", fontsize=14, style = filled, fillcolor = lightgrey];
496 -> 778 [arrowhead = none , style=dashed];
778 -> 414[style=dashed];

779 [label="INSTANCE with matching:\nT288 -> T358\nT289 -> T359\nT291 -> T361", fontsize=14, style = filled, fillcolor = lightgrey];
505 -> 779 [arrowhead = none , style=dashed];
779 -> 463[style=dashed];

780 [label="EVAL with clause\naddC(one(X454), zero(X455), zero(X456)) :- addY(X454, X455, X456).\nand substitutionX454 -> T377,\nT288 -> one(T377),\nX455 -> T378,\nT289 -> zero(T378),\nX456 -> T380,\nT291 -> zero(T380),\nT379 -> T380", fontsize=14, style = filled, fillcolor = lightblue];
508 -> 780 [arrowhead = none ];
780 -> 512;

781 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
508 -> 781 [arrowhead = none ];
781 -> 514;

782 [label="EVAL with clause\naddC(one(X495), one(X496), one(X497)) :- addc(X495, X496, X497).\nand substitutionX495 -> T422,\nT288 -> one(T422),\nX496 -> T423,\nT289 -> one(T423),\nX497 -> T425,\nT291 -> one(T425),\nT424 -> T425", fontsize=14, style = filled, fillcolor = lightblue];
509 -> 782 [arrowhead = none ];
782 -> 537;

783 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
509 -> 783 [arrowhead = none ];
783 -> 540;

784 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
512 -> 784 [arrowhead = none ];
784 -> 518;

785 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
518 -> 785 [arrowhead = none ];
785 -> 520;

786 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
518 -> 786 [arrowhead = none ];
786 -> 521;

787 [label="EVAL with clause\naddY(b, zero(X462), one(X462)) :- binaryZ(X462).\nand substitutionT377 -> b,\nX462 -> T386,\nT378 -> zero(T386),\nT380 -> one(T386)", fontsize=14, style = filled, fillcolor = lightblue];
520 -> 787 [arrowhead = none ];
787 -> 523;

788 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
520 -> 788 [arrowhead = none ];
788 -> 524;

789 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
521 -> 789 [arrowhead = none ];
789 -> 525;

790 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
521 -> 790 [arrowhead = none ];
790 -> 526;

791 [label="INSTANCE with matching:\nT23 -> T386", fontsize=14, style = filled, fillcolor = lightgrey];
523 -> 791 [arrowhead = none , style=dashed];
791 -> 123[style=dashed];

792 [label="EVAL with clause\naddY(b, one(X472), zero(X473)) :- succ(X472, X473).\nand substitutionT377 -> b,\nX472 -> T396,\nT378 -> one(T396),\nX473 -> T398,\nT380 -> zero(T398),\nT397 -> T398", fontsize=14, style = filled, fillcolor = lightblue];
525 -> 792 [arrowhead = none ];
792 -> 528;

793 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
525 -> 793 [arrowhead = none ];
793 -> 529;

794 [label="ONLY EVAL with clause\naddY(X483, X484, X485) :- addC(X483, X484, X485).\nand substitutionT377 -> T409,\nX483 -> T409,\nT378 -> T410,\nX484 -> T410,\nT380 -> T412,\nX485 -> T412,\nT411 -> T412", fontsize=14, style = filled, fillcolor = lightblue];
526 -> 794 [arrowhead = none ];
794 -> 530;

795 [label="INSTANCE with matching:\nT250 -> T396\nT252 -> T398", fontsize=14, style = filled, fillcolor = lightgrey];
528 -> 795 [arrowhead = none , style=dashed];
795 -> 414[style=dashed];

796 [label="INSTANCE with matching:\nT288 -> T409\nT289 -> T410\nT291 -> T412", fontsize=14, style = filled, fillcolor = lightgrey];
530 -> 796 [arrowhead = none , style=dashed];
796 -> 463[style=dashed];

797 [label="INSTANCE with matching:\nT224 -> T422\nT225 -> T423\nT227 -> T425", fontsize=14, style = filled, fillcolor = lightgrey];
537 -> 797 [arrowhead = none , style=dashed];
797 -> 376[style=dashed];

798 [label="EVAL with clause\naddz(zero(X510), one(X511), one(X512)) :- addx(X510, X511, X512).\nand substitutionX510 -> T438,\nT86 -> zero(T438),\nX511 -> T439,\nT87 -> one(T439),\nX512 -> T441,\nT89 -> one(T441),\nT440 -> T441", fontsize=14, style = filled, fillcolor = lightblue];
545 -> 798 [arrowhead = none ];
798 -> 551;

799 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
545 -> 799 [arrowhead = none ];
799 -> 552;

800 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
546 -> 800 [arrowhead = none ];
800 -> 553;

801 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
546 -> 801 [arrowhead = none ];
801 -> 554;

802 [label="INSTANCE with matching:\nT140 -> T438\nT141 -> T439\nT143 -> T441", fontsize=14, style = filled, fillcolor = lightgrey];
551 -> 802 [arrowhead = none , style=dashed];
802 -> 312[style=dashed];

803 [label="EVAL with clause\naddz(one(X526), zero(X527), one(X528)) :- addy(X526, X527, X528).\nand substitutionX526 -> T455,\nT86 -> one(T455),\nX527 -> T456,\nT87 -> zero(T456),\nX528 -> T458,\nT89 -> one(T458),\nT457 -> T458", fontsize=14, style = filled, fillcolor = lightblue];
553 -> 803 [arrowhead = none ];
803 -> 556;

804 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
553 -> 804 [arrowhead = none ];
804 -> 557;

805 [label="EVAL with clause\naddz(one(X536), one(X537), zero(X538)) :- addc(X536, X537, X538).\nand substitutionX536 -> T466,\nT86 -> one(T466),\nX537 -> T467,\nT87 -> one(T467),\nX538 -> T469,\nT89 -> zero(T469),\nT468 -> T469", fontsize=14, style = filled, fillcolor = lightblue];
554 -> 805 [arrowhead = none ];
805 -> 562;

806 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
554 -> 806 [arrowhead = none ];
806 -> 563;

807 [label="INSTANCE with matching:\nT185 -> T455\nT186 -> T456\nT188 -> T458", fontsize=14, style = filled, fillcolor = lightgrey];
556 -> 807 [arrowhead = none , style=dashed];
807 -> 348[style=dashed];

808 [label="INSTANCE with matching:\nT224 -> T466\nT225 -> T467\nT227 -> T469", fontsize=14, style = filled, fillcolor = lightgrey];
562 -> 808 [arrowhead = none , style=dashed];
808 -> 376[style=dashed];

}

(2) Obligation:

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

addA_in_gga(b, b, b) → addA_out_gga(b, b, b)
addA_in_gga(zero(T23), b, zero(T23)) → U1_gga(T23, binaryZD_in_g(T23))
binaryZD_in_g(zero(T29)) → U9_g(T29, binaryZD_in_g(T29))
binaryZD_in_g(one(T33)) → U10_g(T33, binaryE_in_g(T33))
binaryE_in_g(b) → binaryE_out_g(b)
binaryE_in_g(zero(T38)) → U11_g(T38, binaryZD_in_g(T38))
U11_g(T38, binaryZD_out_g(T38)) → binaryE_out_g(zero(T38))
binaryE_in_g(one(T42)) → U12_g(T42, binaryE_in_g(T42))
U12_g(T42, binaryE_out_g(T42)) → binaryE_out_g(one(T42))
U10_g(T33, binaryE_out_g(T33)) → binaryZD_out_g(one(T33))
U9_g(T29, binaryZD_out_g(T29)) → binaryZD_out_g(zero(T29))
U1_gga(T23, binaryZD_out_g(T23)) → addA_out_gga(zero(T23), b, zero(T23))
addA_in_gga(one(T47), b, one(T47)) → U2_gga(T47, binaryE_in_g(T47))
U2_gga(T47, binaryE_out_g(T47)) → addA_out_gga(one(T47), b, one(T47))
addA_in_gga(b, zero(T68), zero(T68)) → U3_gga(T68, binaryZD_in_g(T68))
U3_gga(T68, binaryZD_out_g(T68)) → addA_out_gga(b, zero(T68), zero(T68))
addA_in_gga(b, one(T74), one(T74)) → U4_gga(T74, binaryE_in_g(T74))
U4_gga(T74, binaryE_out_g(T74)) → addA_out_gga(b, one(T74), one(T74))
addA_in_gga(zero(T102), zero(T103), zero(T105)) → U5_gga(T102, T103, T105, addzF_in_gga(T102, T103, T105))
addzF_in_gga(zero(T121), zero(T122), zero(T124)) → U13_gga(T121, T122, T124, addzF_in_gga(T121, T122, T124))
addzF_in_gga(zero(T140), one(T141), one(T143)) → U14_gga(T140, T141, T143, addxG_in_gga(T140, T141, T143))
addxG_in_gga(one(T149), b, one(T149)) → U32_gga(T149, binaryE_in_g(T149))
U32_gga(T149, binaryE_out_g(T149)) → addxG_out_gga(one(T149), b, one(T149))
addxG_in_gga(zero(T154), b, zero(T154)) → U33_gga(T154, binaryZD_in_g(T154))
U33_gga(T154, binaryZD_out_g(T154)) → addxG_out_gga(zero(T154), b, zero(T154))
addxG_in_gga(T166, T167, T169) → U34_gga(T166, T167, T169, addzF_in_gga(T166, T167, T169))
addzF_in_gga(one(T185), zero(T186), one(T188)) → U15_gga(T185, T186, T188, addyH_in_gga(T185, T186, T188))
addyH_in_gga(b, one(T194), one(T194)) → U35_gga(T194, binaryE_in_g(T194))
U35_gga(T194, binaryE_out_g(T194)) → addyH_out_gga(b, one(T194), one(T194))
addyH_in_gga(b, zero(T199), zero(T199)) → U36_gga(T199, binaryZD_in_g(T199))
U36_gga(T199, binaryZD_out_g(T199)) → addyH_out_gga(b, zero(T199), zero(T199))
addyH_in_gga(T211, T212, T214) → U37_gga(T211, T212, T214, addzF_in_gga(T211, T212, T214))
addzF_in_gga(one(T224), one(T225), zero(T227)) → U16_gga(T224, T225, T227, addcI_in_gga(T224, T225, T227))
addcI_in_gga(b, b, one(b)) → addcI_out_gga(b, b, one(b))
addcI_in_gga(T236, b, T238) → U29_gga(T236, T238, succZK_in_ga(T236, T238))
succZK_in_ga(zero(T244), one(T244)) → U19_ga(T244, binaryZD_in_g(T244))
U19_ga(T244, binaryZD_out_g(T244)) → succZK_out_ga(zero(T244), one(T244))
succZK_in_ga(one(T250), zero(T252)) → U20_ga(T250, T252, succJ_in_ga(T250, T252))
succJ_in_ga(b, one(b)) → succJ_out_ga(b, one(b))
succJ_in_ga(zero(T257), one(T257)) → U17_ga(T257, binaryZD_in_g(T257))
U17_ga(T257, binaryZD_out_g(T257)) → succJ_out_ga(zero(T257), one(T257))
succJ_in_ga(one(T263), zero(T265)) → U18_ga(T263, T265, succJ_in_ga(T263, T265))
U18_ga(T263, T265, succJ_out_ga(T263, T265)) → succJ_out_ga(one(T263), zero(T265))
U20_ga(T250, T252, succJ_out_ga(T250, T252)) → succZK_out_ga(one(T250), zero(T252))
U29_gga(T236, T238, succZK_out_ga(T236, T238)) → addcI_out_gga(T236, b, T238)
addcI_in_gga(b, T274, T276) → U30_gga(T274, T276, succZK_in_ga(T274, T276))
U30_gga(T274, T276, succZK_out_ga(T274, T276)) → addcI_out_gga(b, T274, T276)
addcI_in_gga(T288, T289, T291) → U31_gga(T288, T289, T291, addCL_in_gga(T288, T289, T291))
addCL_in_gga(zero(T307), zero(T308), one(T310)) → U21_gga(T307, T308, T310, addzF_in_gga(T307, T308, T310))
U21_gga(T307, T308, T310, addzF_out_gga(T307, T308, T310)) → addCL_out_gga(zero(T307), zero(T308), one(T310))
addCL_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U22_gga(T335, binaryZD_in_g(T335))
U22_gga(T335, binaryZD_out_g(T335)) → addCL_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCL_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U23_gga(T345, T347, succJ_in_ga(T345, T347))
U23_gga(T345, T347, succJ_out_ga(T345, T347)) → addCL_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCL_in_gga(zero(T358), one(T359), zero(T361)) → U24_gga(T358, T359, T361, addCL_in_gga(T358, T359, T361))
addCL_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U25_gga(T386, binaryZD_in_g(T386))
U25_gga(T386, binaryZD_out_g(T386)) → addCL_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCL_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U26_gga(T396, T398, succJ_in_ga(T396, T398))
U26_gga(T396, T398, succJ_out_ga(T396, T398)) → addCL_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCL_in_gga(one(T409), zero(T410), zero(T412)) → U27_gga(T409, T410, T412, addCL_in_gga(T409, T410, T412))
addCL_in_gga(one(T422), one(T423), one(T425)) → U28_gga(T422, T423, T425, addcI_in_gga(T422, T423, T425))
U28_gga(T422, T423, T425, addcI_out_gga(T422, T423, T425)) → addCL_out_gga(one(T422), one(T423), one(T425))
U27_gga(T409, T410, T412, addCL_out_gga(T409, T410, T412)) → addCL_out_gga(one(T409), zero(T410), zero(T412))
U24_gga(T358, T359, T361, addCL_out_gga(T358, T359, T361)) → addCL_out_gga(zero(T358), one(T359), zero(T361))
U31_gga(T288, T289, T291, addCL_out_gga(T288, T289, T291)) → addcI_out_gga(T288, T289, T291)
U16_gga(T224, T225, T227, addcI_out_gga(T224, T225, T227)) → addzF_out_gga(one(T224), one(T225), zero(T227))
U37_gga(T211, T212, T214, addzF_out_gga(T211, T212, T214)) → addyH_out_gga(T211, T212, T214)
U15_gga(T185, T186, T188, addyH_out_gga(T185, T186, T188)) → addzF_out_gga(one(T185), zero(T186), one(T188))
U34_gga(T166, T167, T169, addzF_out_gga(T166, T167, T169)) → addxG_out_gga(T166, T167, T169)
U14_gga(T140, T141, T143, addxG_out_gga(T140, T141, T143)) → addzF_out_gga(zero(T140), one(T141), one(T143))
U13_gga(T121, T122, T124, addzF_out_gga(T121, T122, T124)) → addzF_out_gga(zero(T121), zero(T122), zero(T124))
U5_gga(T102, T103, T105, addzF_out_gga(T102, T103, T105)) → addA_out_gga(zero(T102), zero(T103), zero(T105))
addA_in_gga(zero(T438), one(T439), one(T441)) → U6_gga(T438, T439, T441, addxG_in_gga(T438, T439, T441))
U6_gga(T438, T439, T441, addxG_out_gga(T438, T439, T441)) → addA_out_gga(zero(T438), one(T439), one(T441))
addA_in_gga(one(T455), zero(T456), one(T458)) → U7_gga(T455, T456, T458, addyH_in_gga(T455, T456, T458))
U7_gga(T455, T456, T458, addyH_out_gga(T455, T456, T458)) → addA_out_gga(one(T455), zero(T456), one(T458))
addA_in_gga(one(T466), one(T467), zero(T469)) → U8_gga(T466, T467, T469, addcI_in_gga(T466, T467, T469))
U8_gga(T466, T467, T469, addcI_out_gga(T466, T467, T469)) → addA_out_gga(one(T466), one(T467), zero(T469))

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

ADDA_IN_GGA(zero(T23), b, zero(T23)) → U1_GGA(T23, binaryZD_in_g(T23))
ADDA_IN_GGA(zero(T23), b, zero(T23)) → BINARYZD_IN_G(T23)
BINARYZD_IN_G(zero(T29)) → U9_G(T29, binaryZD_in_g(T29))
BINARYZD_IN_G(zero(T29)) → BINARYZD_IN_G(T29)
BINARYZD_IN_G(one(T33)) → U10_G(T33, binaryE_in_g(T33))
BINARYZD_IN_G(one(T33)) → BINARYE_IN_G(T33)
BINARYE_IN_G(zero(T38)) → U11_G(T38, binaryZD_in_g(T38))
BINARYE_IN_G(zero(T38)) → BINARYZD_IN_G(T38)
BINARYE_IN_G(one(T42)) → U12_G(T42, binaryE_in_g(T42))
BINARYE_IN_G(one(T42)) → BINARYE_IN_G(T42)
ADDA_IN_GGA(one(T47), b, one(T47)) → U2_GGA(T47, binaryE_in_g(T47))
ADDA_IN_GGA(one(T47), b, one(T47)) → BINARYE_IN_G(T47)
ADDA_IN_GGA(b, zero(T68), zero(T68)) → U3_GGA(T68, binaryZD_in_g(T68))
ADDA_IN_GGA(b, zero(T68), zero(T68)) → BINARYZD_IN_G(T68)
ADDA_IN_GGA(b, one(T74), one(T74)) → U4_GGA(T74, binaryE_in_g(T74))
ADDA_IN_GGA(b, one(T74), one(T74)) → BINARYE_IN_G(T74)
ADDA_IN_GGA(zero(T102), zero(T103), zero(T105)) → U5_GGA(T102, T103, T105, addzF_in_gga(T102, T103, T105))
ADDA_IN_GGA(zero(T102), zero(T103), zero(T105)) → ADDZF_IN_GGA(T102, T103, T105)
ADDZF_IN_GGA(zero(T121), zero(T122), zero(T124)) → U13_GGA(T121, T122, T124, addzF_in_gga(T121, T122, T124))
ADDZF_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZF_IN_GGA(T121, T122, T124)
ADDZF_IN_GGA(zero(T140), one(T141), one(T143)) → U14_GGA(T140, T141, T143, addxG_in_gga(T140, T141, T143))
ADDZF_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXG_IN_GGA(T140, T141, T143)
ADDXG_IN_GGA(one(T149), b, one(T149)) → U32_GGA(T149, binaryE_in_g(T149))
ADDXG_IN_GGA(one(T149), b, one(T149)) → BINARYE_IN_G(T149)
ADDXG_IN_GGA(zero(T154), b, zero(T154)) → U33_GGA(T154, binaryZD_in_g(T154))
ADDXG_IN_GGA(zero(T154), b, zero(T154)) → BINARYZD_IN_G(T154)
ADDXG_IN_GGA(T166, T167, T169) → U34_GGA(T166, T167, T169, addzF_in_gga(T166, T167, T169))
ADDXG_IN_GGA(T166, T167, T169) → ADDZF_IN_GGA(T166, T167, T169)
ADDZF_IN_GGA(one(T185), zero(T186), one(T188)) → U15_GGA(T185, T186, T188, addyH_in_gga(T185, T186, T188))
ADDZF_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYH_IN_GGA(T185, T186, T188)
ADDYH_IN_GGA(b, one(T194), one(T194)) → U35_GGA(T194, binaryE_in_g(T194))
ADDYH_IN_GGA(b, one(T194), one(T194)) → BINARYE_IN_G(T194)
ADDYH_IN_GGA(b, zero(T199), zero(T199)) → U36_GGA(T199, binaryZD_in_g(T199))
ADDYH_IN_GGA(b, zero(T199), zero(T199)) → BINARYZD_IN_G(T199)
ADDYH_IN_GGA(T211, T212, T214) → U37_GGA(T211, T212, T214, addzF_in_gga(T211, T212, T214))
ADDYH_IN_GGA(T211, T212, T214) → ADDZF_IN_GGA(T211, T212, T214)
ADDZF_IN_GGA(one(T224), one(T225), zero(T227)) → U16_GGA(T224, T225, T227, addcI_in_gga(T224, T225, T227))
ADDZF_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCI_IN_GGA(T224, T225, T227)
ADDCI_IN_GGA(T236, b, T238) → U29_GGA(T236, T238, succZK_in_ga(T236, T238))
ADDCI_IN_GGA(T236, b, T238) → SUCCZK_IN_GA(T236, T238)
SUCCZK_IN_GA(zero(T244), one(T244)) → U19_GA(T244, binaryZD_in_g(T244))
SUCCZK_IN_GA(zero(T244), one(T244)) → BINARYZD_IN_G(T244)
SUCCZK_IN_GA(one(T250), zero(T252)) → U20_GA(T250, T252, succJ_in_ga(T250, T252))
SUCCZK_IN_GA(one(T250), zero(T252)) → SUCCJ_IN_GA(T250, T252)
SUCCJ_IN_GA(zero(T257), one(T257)) → U17_GA(T257, binaryZD_in_g(T257))
SUCCJ_IN_GA(zero(T257), one(T257)) → BINARYZD_IN_G(T257)
SUCCJ_IN_GA(one(T263), zero(T265)) → U18_GA(T263, T265, succJ_in_ga(T263, T265))
SUCCJ_IN_GA(one(T263), zero(T265)) → SUCCJ_IN_GA(T263, T265)
ADDCI_IN_GGA(b, T274, T276) → U30_GGA(T274, T276, succZK_in_ga(T274, T276))
ADDCI_IN_GGA(b, T274, T276) → SUCCZK_IN_GA(T274, T276)
ADDCI_IN_GGA(T288, T289, T291) → U31_GGA(T288, T289, T291, addCL_in_gga(T288, T289, T291))
ADDCI_IN_GGA(T288, T289, T291) → ADDCL_IN_GGA(T288, T289, T291)
ADDCL_IN_GGA(zero(T307), zero(T308), one(T310)) → U21_GGA(T307, T308, T310, addzF_in_gga(T307, T308, T310))
ADDCL_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZF_IN_GGA(T307, T308, T310)
ADDCL_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → U22_GGA(T335, binaryZD_in_g(T335))
ADDCL_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → BINARYZD_IN_G(T335)
ADDCL_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → U23_GGA(T345, T347, succJ_in_ga(T345, T347))
ADDCL_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → SUCCJ_IN_GA(T345, T347)
ADDCL_IN_GGA(zero(T358), one(T359), zero(T361)) → U24_GGA(T358, T359, T361, addCL_in_gga(T358, T359, T361))
ADDCL_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCL_IN_GGA(T358, T359, T361)
ADDCL_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → U25_GGA(T386, binaryZD_in_g(T386))
ADDCL_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → BINARYZD_IN_G(T386)
ADDCL_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → U26_GGA(T396, T398, succJ_in_ga(T396, T398))
ADDCL_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → SUCCJ_IN_GA(T396, T398)
ADDCL_IN_GGA(one(T409), zero(T410), zero(T412)) → U27_GGA(T409, T410, T412, addCL_in_gga(T409, T410, T412))
ADDCL_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCL_IN_GGA(T409, T410, T412)
ADDCL_IN_GGA(one(T422), one(T423), one(T425)) → U28_GGA(T422, T423, T425, addcI_in_gga(T422, T423, T425))
ADDCL_IN_GGA(one(T422), one(T423), one(T425)) → ADDCI_IN_GGA(T422, T423, T425)
ADDA_IN_GGA(zero(T438), one(T439), one(T441)) → U6_GGA(T438, T439, T441, addxG_in_gga(T438, T439, T441))
ADDA_IN_GGA(zero(T438), one(T439), one(T441)) → ADDXG_IN_GGA(T438, T439, T441)
ADDA_IN_GGA(one(T455), zero(T456), one(T458)) → U7_GGA(T455, T456, T458, addyH_in_gga(T455, T456, T458))
ADDA_IN_GGA(one(T455), zero(T456), one(T458)) → ADDYH_IN_GGA(T455, T456, T458)
ADDA_IN_GGA(one(T466), one(T467), zero(T469)) → U8_GGA(T466, T467, T469, addcI_in_gga(T466, T467, T469))
ADDA_IN_GGA(one(T466), one(T467), zero(T469)) → ADDCI_IN_GGA(T466, T467, T469)

The TRS R consists of the following rules:

addA_in_gga(b, b, b) → addA_out_gga(b, b, b)
addA_in_gga(zero(T23), b, zero(T23)) → U1_gga(T23, binaryZD_in_g(T23))
binaryZD_in_g(zero(T29)) → U9_g(T29, binaryZD_in_g(T29))
binaryZD_in_g(one(T33)) → U10_g(T33, binaryE_in_g(T33))
binaryE_in_g(b) → binaryE_out_g(b)
binaryE_in_g(zero(T38)) → U11_g(T38, binaryZD_in_g(T38))
U11_g(T38, binaryZD_out_g(T38)) → binaryE_out_g(zero(T38))
binaryE_in_g(one(T42)) → U12_g(T42, binaryE_in_g(T42))
U12_g(T42, binaryE_out_g(T42)) → binaryE_out_g(one(T42))
U10_g(T33, binaryE_out_g(T33)) → binaryZD_out_g(one(T33))
U9_g(T29, binaryZD_out_g(T29)) → binaryZD_out_g(zero(T29))
U1_gga(T23, binaryZD_out_g(T23)) → addA_out_gga(zero(T23), b, zero(T23))
addA_in_gga(one(T47), b, one(T47)) → U2_gga(T47, binaryE_in_g(T47))
U2_gga(T47, binaryE_out_g(T47)) → addA_out_gga(one(T47), b, one(T47))
addA_in_gga(b, zero(T68), zero(T68)) → U3_gga(T68, binaryZD_in_g(T68))
U3_gga(T68, binaryZD_out_g(T68)) → addA_out_gga(b, zero(T68), zero(T68))
addA_in_gga(b, one(T74), one(T74)) → U4_gga(T74, binaryE_in_g(T74))
U4_gga(T74, binaryE_out_g(T74)) → addA_out_gga(b, one(T74), one(T74))
addA_in_gga(zero(T102), zero(T103), zero(T105)) → U5_gga(T102, T103, T105, addzF_in_gga(T102, T103, T105))
addzF_in_gga(zero(T121), zero(T122), zero(T124)) → U13_gga(T121, T122, T124, addzF_in_gga(T121, T122, T124))
addzF_in_gga(zero(T140), one(T141), one(T143)) → U14_gga(T140, T141, T143, addxG_in_gga(T140, T141, T143))
addxG_in_gga(one(T149), b, one(T149)) → U32_gga(T149, binaryE_in_g(T149))
U32_gga(T149, binaryE_out_g(T149)) → addxG_out_gga(one(T149), b, one(T149))
addxG_in_gga(zero(T154), b, zero(T154)) → U33_gga(T154, binaryZD_in_g(T154))
U33_gga(T154, binaryZD_out_g(T154)) → addxG_out_gga(zero(T154), b, zero(T154))
addxG_in_gga(T166, T167, T169) → U34_gga(T166, T167, T169, addzF_in_gga(T166, T167, T169))
addzF_in_gga(one(T185), zero(T186), one(T188)) → U15_gga(T185, T186, T188, addyH_in_gga(T185, T186, T188))
addyH_in_gga(b, one(T194), one(T194)) → U35_gga(T194, binaryE_in_g(T194))
U35_gga(T194, binaryE_out_g(T194)) → addyH_out_gga(b, one(T194), one(T194))
addyH_in_gga(b, zero(T199), zero(T199)) → U36_gga(T199, binaryZD_in_g(T199))
U36_gga(T199, binaryZD_out_g(T199)) → addyH_out_gga(b, zero(T199), zero(T199))
addyH_in_gga(T211, T212, T214) → U37_gga(T211, T212, T214, addzF_in_gga(T211, T212, T214))
addzF_in_gga(one(T224), one(T225), zero(T227)) → U16_gga(T224, T225, T227, addcI_in_gga(T224, T225, T227))
addcI_in_gga(b, b, one(b)) → addcI_out_gga(b, b, one(b))
addcI_in_gga(T236, b, T238) → U29_gga(T236, T238, succZK_in_ga(T236, T238))
succZK_in_ga(zero(T244), one(T244)) → U19_ga(T244, binaryZD_in_g(T244))
U19_ga(T244, binaryZD_out_g(T244)) → succZK_out_ga(zero(T244), one(T244))
succZK_in_ga(one(T250), zero(T252)) → U20_ga(T250, T252, succJ_in_ga(T250, T252))
succJ_in_ga(b, one(b)) → succJ_out_ga(b, one(b))
succJ_in_ga(zero(T257), one(T257)) → U17_ga(T257, binaryZD_in_g(T257))
U17_ga(T257, binaryZD_out_g(T257)) → succJ_out_ga(zero(T257), one(T257))
succJ_in_ga(one(T263), zero(T265)) → U18_ga(T263, T265, succJ_in_ga(T263, T265))
U18_ga(T263, T265, succJ_out_ga(T263, T265)) → succJ_out_ga(one(T263), zero(T265))
U20_ga(T250, T252, succJ_out_ga(T250, T252)) → succZK_out_ga(one(T250), zero(T252))
U29_gga(T236, T238, succZK_out_ga(T236, T238)) → addcI_out_gga(T236, b, T238)
addcI_in_gga(b, T274, T276) → U30_gga(T274, T276, succZK_in_ga(T274, T276))
U30_gga(T274, T276, succZK_out_ga(T274, T276)) → addcI_out_gga(b, T274, T276)
addcI_in_gga(T288, T289, T291) → U31_gga(T288, T289, T291, addCL_in_gga(T288, T289, T291))
addCL_in_gga(zero(T307), zero(T308), one(T310)) → U21_gga(T307, T308, T310, addzF_in_gga(T307, T308, T310))
U21_gga(T307, T308, T310, addzF_out_gga(T307, T308, T310)) → addCL_out_gga(zero(T307), zero(T308), one(T310))
addCL_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U22_gga(T335, binaryZD_in_g(T335))
U22_gga(T335, binaryZD_out_g(T335)) → addCL_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCL_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U23_gga(T345, T347, succJ_in_ga(T345, T347))
U23_gga(T345, T347, succJ_out_ga(T345, T347)) → addCL_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCL_in_gga(zero(T358), one(T359), zero(T361)) → U24_gga(T358, T359, T361, addCL_in_gga(T358, T359, T361))
addCL_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U25_gga(T386, binaryZD_in_g(T386))
U25_gga(T386, binaryZD_out_g(T386)) → addCL_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCL_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U26_gga(T396, T398, succJ_in_ga(T396, T398))
U26_gga(T396, T398, succJ_out_ga(T396, T398)) → addCL_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCL_in_gga(one(T409), zero(T410), zero(T412)) → U27_gga(T409, T410, T412, addCL_in_gga(T409, T410, T412))
addCL_in_gga(one(T422), one(T423), one(T425)) → U28_gga(T422, T423, T425, addcI_in_gga(T422, T423, T425))
U28_gga(T422, T423, T425, addcI_out_gga(T422, T423, T425)) → addCL_out_gga(one(T422), one(T423), one(T425))
U27_gga(T409, T410, T412, addCL_out_gga(T409, T410, T412)) → addCL_out_gga(one(T409), zero(T410), zero(T412))
U24_gga(T358, T359, T361, addCL_out_gga(T358, T359, T361)) → addCL_out_gga(zero(T358), one(T359), zero(T361))
U31_gga(T288, T289, T291, addCL_out_gga(T288, T289, T291)) → addcI_out_gga(T288, T289, T291)
U16_gga(T224, T225, T227, addcI_out_gga(T224, T225, T227)) → addzF_out_gga(one(T224), one(T225), zero(T227))
U37_gga(T211, T212, T214, addzF_out_gga(T211, T212, T214)) → addyH_out_gga(T211, T212, T214)
U15_gga(T185, T186, T188, addyH_out_gga(T185, T186, T188)) → addzF_out_gga(one(T185), zero(T186), one(T188))
U34_gga(T166, T167, T169, addzF_out_gga(T166, T167, T169)) → addxG_out_gga(T166, T167, T169)
U14_gga(T140, T141, T143, addxG_out_gga(T140, T141, T143)) → addzF_out_gga(zero(T140), one(T141), one(T143))
U13_gga(T121, T122, T124, addzF_out_gga(T121, T122, T124)) → addzF_out_gga(zero(T121), zero(T122), zero(T124))
U5_gga(T102, T103, T105, addzF_out_gga(T102, T103, T105)) → addA_out_gga(zero(T102), zero(T103), zero(T105))
addA_in_gga(zero(T438), one(T439), one(T441)) → U6_gga(T438, T439, T441, addxG_in_gga(T438, T439, T441))
U6_gga(T438, T439, T441, addxG_out_gga(T438, T439, T441)) → addA_out_gga(zero(T438), one(T439), one(T441))
addA_in_gga(one(T455), zero(T456), one(T458)) → U7_gga(T455, T456, T458, addyH_in_gga(T455, T456, T458))
U7_gga(T455, T456, T458, addyH_out_gga(T455, T456, T458)) → addA_out_gga(one(T455), zero(T456), one(T458))
addA_in_gga(one(T466), one(T467), zero(T469)) → U8_gga(T466, T467, T469, addcI_in_gga(T466, T467, T469))
U8_gga(T466, T467, T469, addcI_out_gga(T466, T467, T469)) → addA_out_gga(one(T466), one(T467), zero(T469))

The argument filtering Pi contains the following mapping:
addA_in_gga(x1, x2, x3) = addA_in_gga(x1, x2)
b = b
addA_out_gga(x1, x2, x3) = addA_out_gga(x1, x2, x3)
zero(x1) = zero(x1)
U1_gga(x1, x2) = U1_gga(x1, x2)
binaryZD_in_g(x1) = binaryZD_in_g(x1)
U9_g(x1, x2) = U9_g(x1, x2)
one(x1) = one(x1)
U10_g(x1, x2) = U10_g(x1, x2)
binaryE_in_g(x1) = binaryE_in_g(x1)
binaryE_out_g(x1) = binaryE_out_g(x1)
U11_g(x1, x2) = U11_g(x1, x2)
binaryZD_out_g(x1) = binaryZD_out_g(x1)
U12_g(x1, x2) = U12_g(x1, x2)
U2_gga(x1, x2) = U2_gga(x1, x2)
U3_gga(x1, x2) = U3_gga(x1, x2)
U4_gga(x1, x2) = U4_gga(x1, x2)
U5_gga(x1, x2, x3, x4) = U5_gga(x1, x2, x4)
addzF_in_gga(x1, x2, x3) = addzF_in_gga(x1, x2)
U13_gga(x1, x2, x3, x4) = U13_gga(x1, x2, x4)
U14_gga(x1, x2, x3, x4) = U14_gga(x1, x2, x4)
addxG_in_gga(x1, x2, x3) = addxG_in_gga(x1, x2)
U32_gga(x1, x2) = U32_gga(x1, x2)
addxG_out_gga(x1, x2, x3) = addxG_out_gga(x1, x2, x3)
U33_gga(x1, x2) = U33_gga(x1, x2)
U34_gga(x1, x2, x3, x4) = U34_gga(x1, x2, x4)
U15_gga(x1, x2, x3, x4) = U15_gga(x1, x2, x4)
addyH_in_gga(x1, x2, x3) = addyH_in_gga(x1, x2)
U35_gga(x1, x2) = U35_gga(x1, x2)
addyH_out_gga(x1, x2, x3) = addyH_out_gga(x1, x2, x3)
U36_gga(x1, x2) = U36_gga(x1, x2)
U37_gga(x1, x2, x3, x4) = U37_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4) = U16_gga(x1, x2, x4)
addcI_in_gga(x1, x2, x3) = addcI_in_gga(x1, x2)
addcI_out_gga(x1, x2, x3) = addcI_out_gga(x1, x2, x3)
U29_gga(x1, x2, x3) = U29_gga(x1, x3)
succZK_in_ga(x1, x2) = succZK_in_ga(x1)
U19_ga(x1, x2) = U19_ga(x1, x2)
succZK_out_ga(x1, x2) = succZK_out_ga(x1, x2)
U20_ga(x1, x2, x3) = U20_ga(x1, x3)
succJ_in_ga(x1, x2) = succJ_in_ga(x1)
succJ_out_ga(x1, x2) = succJ_out_ga(x1, x2)
U17_ga(x1, x2) = U17_ga(x1, x2)
U18_ga(x1, x2, x3) = U18_ga(x1, x3)
U30_gga(x1, x2, x3) = U30_gga(x1, x3)
U31_gga(x1, x2, x3, x4) = U31_gga(x1, x2, x4)
addCL_in_gga(x1, x2, x3) = addCL_in_gga(x1, x2)
U21_gga(x1, x2, x3, x4) = U21_gga(x1, x2, x4)
addzF_out_gga(x1, x2, x3) = addzF_out_gga(x1, x2, x3)
addCL_out_gga(x1, x2, x3) = addCL_out_gga(x1, x2, x3)
U22_gga(x1, x2) = U22_gga(x1, x2)
U23_gga(x1, x2, x3) = U23_gga(x1, x3)
U24_gga(x1, x2, x3, x4) = U24_gga(x1, x2, x4)
U25_gga(x1, x2) = U25_gga(x1, x2)
U26_gga(x1, x2, x3) = U26_gga(x1, x3)
U27_gga(x1, x2, x3, x4) = U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4) = U28_gga(x1, x2, x4)
U6_gga(x1, x2, x3, x4) = U6_gga(x1, x2, x4)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
U8_gga(x1, x2, x3, x4) = U8_gga(x1, x2, x4)
ADDA_IN_GGA(x1, x2, x3) = ADDA_IN_GGA(x1, x2)
U1_GGA(x1, x2) = U1_GGA(x1, x2)
BINARYZD_IN_G(x1) = BINARYZD_IN_G(x1)
U9_G(x1, x2) = U9_G(x1, x2)
U10_G(x1, x2) = U10_G(x1, x2)
BINARYE_IN_G(x1) = BINARYE_IN_G(x1)
U11_G(x1, x2) = U11_G(x1, x2)
U12_G(x1, x2) = U12_G(x1, x2)
U2_GGA(x1, x2) = U2_GGA(x1, x2)
U3_GGA(x1, x2) = U3_GGA(x1, x2)
U4_GGA(x1, x2) = U4_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4) = U5_GGA(x1, x2, x4)
ADDZF_IN_GGA(x1, x2, x3) = ADDZF_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4) = U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4) = U14_GGA(x1, x2, x4)
ADDXG_IN_GGA(x1, x2, x3) = ADDXG_IN_GGA(x1, x2)
U32_GGA(x1, x2) = U32_GGA(x1, x2)
U33_GGA(x1, x2) = U33_GGA(x1, x2)
U34_GGA(x1, x2, x3, x4) = U34_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4) = U15_GGA(x1, x2, x4)
ADDYH_IN_GGA(x1, x2, x3) = ADDYH_IN_GGA(x1, x2)
U35_GGA(x1, x2) = U35_GGA(x1, x2)
U36_GGA(x1, x2) = U36_GGA(x1, x2)
U37_GGA(x1, x2, x3, x4) = U37_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4) = U16_GGA(x1, x2, x4)
ADDCI_IN_GGA(x1, x2, x3) = ADDCI_IN_GGA(x1, x2)
U29_GGA(x1, x2, x3) = U29_GGA(x1, x3)
SUCCZK_IN_GA(x1, x2) = SUCCZK_IN_GA(x1)
U19_GA(x1, x2) = U19_GA(x1, x2)
U20_GA(x1, x2, x3) = U20_GA(x1, x3)
SUCCJ_IN_GA(x1, x2) = SUCCJ_IN_GA(x1)
U17_GA(x1, x2) = U17_GA(x1, x2)
U18_GA(x1, x2, x3) = U18_GA(x1, x3)
U30_GGA(x1, x2, x3) = U30_GGA(x1, x3)
U31_GGA(x1, x2, x3, x4) = U31_GGA(x1, x2, x4)
ADDCL_IN_GGA(x1, x2, x3) = ADDCL_IN_GGA(x1, x2)
U21_GGA(x1, x2, x3, x4) = U21_GGA(x1, x2, x4)
U22_GGA(x1, x2) = U22_GGA(x1, x2)
U23_GGA(x1, x2, x3) = U23_GGA(x1, x3)
U24_GGA(x1, x2, x3, x4) = U24_GGA(x1, x2, x4)
U25_GGA(x1, x2) = U25_GGA(x1, x2)
U26_GGA(x1, x2, x3) = U26_GGA(x1, x3)
U27_GGA(x1, x2, x3, x4) = U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4) = U28_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4) = U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4) = U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4) = U8_GGA(x1, x2, x4)

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

(4) Obligation:

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

ADDA_IN_GGA(zero(T23), b, zero(T23)) → U1_GGA(T23, binaryZD_in_g(T23))
ADDA_IN_GGA(zero(T23), b, zero(T23)) → BINARYZD_IN_G(T23)
BINARYZD_IN_G(zero(T29)) → U9_G(T29, binaryZD_in_g(T29))
BINARYZD_IN_G(zero(T29)) → BINARYZD_IN_G(T29)
BINARYZD_IN_G(one(T33)) → U10_G(T33, binaryE_in_g(T33))
BINARYZD_IN_G(one(T33)) → BINARYE_IN_G(T33)
BINARYE_IN_G(zero(T38)) → U11_G(T38, binaryZD_in_g(T38))
BINARYE_IN_G(zero(T38)) → BINARYZD_IN_G(T38)
BINARYE_IN_G(one(T42)) → U12_G(T42, binaryE_in_g(T42))
BINARYE_IN_G(one(T42)) → BINARYE_IN_G(T42)
ADDA_IN_GGA(one(T47), b, one(T47)) → U2_GGA(T47, binaryE_in_g(T47))
ADDA_IN_GGA(one(T47), b, one(T47)) → BINARYE_IN_G(T47)
ADDA_IN_GGA(b, zero(T68), zero(T68)) → U3_GGA(T68, binaryZD_in_g(T68))
ADDA_IN_GGA(b, zero(T68), zero(T68)) → BINARYZD_IN_G(T68)
ADDA_IN_GGA(b, one(T74), one(T74)) → U4_GGA(T74, binaryE_in_g(T74))
ADDA_IN_GGA(b, one(T74), one(T74)) → BINARYE_IN_G(T74)
ADDA_IN_GGA(zero(T102), zero(T103), zero(T105)) → U5_GGA(T102, T103, T105, addzF_in_gga(T102, T103, T105))
ADDA_IN_GGA(zero(T102), zero(T103), zero(T105)) → ADDZF_IN_GGA(T102, T103, T105)
ADDZF_IN_GGA(zero(T121), zero(T122), zero(T124)) → U13_GGA(T121, T122, T124, addzF_in_gga(T121, T122, T124))
ADDZF_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZF_IN_GGA(T121, T122, T124)
ADDZF_IN_GGA(zero(T140), one(T141), one(T143)) → U14_GGA(T140, T141, T143, addxG_in_gga(T140, T141, T143))
ADDZF_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXG_IN_GGA(T140, T141, T143)
ADDXG_IN_GGA(one(T149), b, one(T149)) → U32_GGA(T149, binaryE_in_g(T149))
ADDXG_IN_GGA(one(T149), b, one(T149)) → BINARYE_IN_G(T149)
ADDXG_IN_GGA(zero(T154), b, zero(T154)) → U33_GGA(T154, binaryZD_in_g(T154))
ADDXG_IN_GGA(zero(T154), b, zero(T154)) → BINARYZD_IN_G(T154)
ADDXG_IN_GGA(T166, T167, T169) → U34_GGA(T166, T167, T169, addzF_in_gga(T166, T167, T169))
ADDXG_IN_GGA(T166, T167, T169) → ADDZF_IN_GGA(T166, T167, T169)
ADDZF_IN_GGA(one(T185), zero(T186), one(T188)) → U15_GGA(T185, T186, T188, addyH_in_gga(T185, T186, T188))
ADDZF_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYH_IN_GGA(T185, T186, T188)
ADDYH_IN_GGA(b, one(T194), one(T194)) → U35_GGA(T194, binaryE_in_g(T194))
ADDYH_IN_GGA(b, one(T194), one(T194)) → BINARYE_IN_G(T194)
ADDYH_IN_GGA(b, zero(T199), zero(T199)) → U36_GGA(T199, binaryZD_in_g(T199))
ADDYH_IN_GGA(b, zero(T199), zero(T199)) → BINARYZD_IN_G(T199)
ADDYH_IN_GGA(T211, T212, T214) → U37_GGA(T211, T212, T214, addzF_in_gga(T211, T212, T214))
ADDYH_IN_GGA(T211, T212, T214) → ADDZF_IN_GGA(T211, T212, T214)
ADDZF_IN_GGA(one(T224), one(T225), zero(T227)) → U16_GGA(T224, T225, T227, addcI_in_gga(T224, T225, T227))
ADDZF_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCI_IN_GGA(T224, T225, T227)
ADDCI_IN_GGA(T236, b, T238) → U29_GGA(T236, T238, succZK_in_ga(T236, T238))
ADDCI_IN_GGA(T236, b, T238) → SUCCZK_IN_GA(T236, T238)
SUCCZK_IN_GA(zero(T244), one(T244)) → U19_GA(T244, binaryZD_in_g(T244))
SUCCZK_IN_GA(zero(T244), one(T244)) → BINARYZD_IN_G(T244)
SUCCZK_IN_GA(one(T250), zero(T252)) → U20_GA(T250, T252, succJ_in_ga(T250, T252))
SUCCZK_IN_GA(one(T250), zero(T252)) → SUCCJ_IN_GA(T250, T252)
SUCCJ_IN_GA(zero(T257), one(T257)) → U17_GA(T257, binaryZD_in_g(T257))
SUCCJ_IN_GA(zero(T257), one(T257)) → BINARYZD_IN_G(T257)
SUCCJ_IN_GA(one(T263), zero(T265)) → U18_GA(T263, T265, succJ_in_ga(T263, T265))
SUCCJ_IN_GA(one(T263), zero(T265)) → SUCCJ_IN_GA(T263, T265)
ADDCI_IN_GGA(b, T274, T276) → U30_GGA(T274, T276, succZK_in_ga(T274, T276))
ADDCI_IN_GGA(b, T274, T276) → SUCCZK_IN_GA(T274, T276)
ADDCI_IN_GGA(T288, T289, T291) → U31_GGA(T288, T289, T291, addCL_in_gga(T288, T289, T291))
ADDCI_IN_GGA(T288, T289, T291) → ADDCL_IN_GGA(T288, T289, T291)
ADDCL_IN_GGA(zero(T307), zero(T308), one(T310)) → U21_GGA(T307, T308, T310, addzF_in_gga(T307, T308, T310))
ADDCL_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZF_IN_GGA(T307, T308, T310)
ADDCL_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → U22_GGA(T335, binaryZD_in_g(T335))
ADDCL_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → BINARYZD_IN_G(T335)
ADDCL_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → U23_GGA(T345, T347, succJ_in_ga(T345, T347))
ADDCL_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → SUCCJ_IN_GA(T345, T347)
ADDCL_IN_GGA(zero(T358), one(T359), zero(T361)) → U24_GGA(T358, T359, T361, addCL_in_gga(T358, T359, T361))
ADDCL_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCL_IN_GGA(T358, T359, T361)
ADDCL_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → U25_GGA(T386, binaryZD_in_g(T386))
ADDCL_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → BINARYZD_IN_G(T386)
ADDCL_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → U26_GGA(T396, T398, succJ_in_ga(T396, T398))
ADDCL_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → SUCCJ_IN_GA(T396, T398)
ADDCL_IN_GGA(one(T409), zero(T410), zero(T412)) → U27_GGA(T409, T410, T412, addCL_in_gga(T409, T410, T412))
ADDCL_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCL_IN_GGA(T409, T410, T412)
ADDCL_IN_GGA(one(T422), one(T423), one(T425)) → U28_GGA(T422, T423, T425, addcI_in_gga(T422, T423, T425))
ADDCL_IN_GGA(one(T422), one(T423), one(T425)) → ADDCI_IN_GGA(T422, T423, T425)
ADDA_IN_GGA(zero(T438), one(T439), one(T441)) → U6_GGA(T438, T439, T441, addxG_in_gga(T438, T439, T441))
ADDA_IN_GGA(zero(T438), one(T439), one(T441)) → ADDXG_IN_GGA(T438, T439, T441)
ADDA_IN_GGA(one(T455), zero(T456), one(T458)) → U7_GGA(T455, T456, T458, addyH_in_gga(T455, T456, T458))
ADDA_IN_GGA(one(T455), zero(T456), one(T458)) → ADDYH_IN_GGA(T455, T456, T458)
ADDA_IN_GGA(one(T466), one(T467), zero(T469)) → U8_GGA(T466, T467, T469, addcI_in_gga(T466, T467, T469))
ADDA_IN_GGA(one(T466), one(T467), zero(T469)) → ADDCI_IN_GGA(T466, T467, T469)

The TRS R consists of the following rules:

addA_in_gga(b, b, b) → addA_out_gga(b, b, b)
addA_in_gga(zero(T23), b, zero(T23)) → U1_gga(T23, binaryZD_in_g(T23))
binaryZD_in_g(zero(T29)) → U9_g(T29, binaryZD_in_g(T29))
binaryZD_in_g(one(T33)) → U10_g(T33, binaryE_in_g(T33))
binaryE_in_g(b) → binaryE_out_g(b)
binaryE_in_g(zero(T38)) → U11_g(T38, binaryZD_in_g(T38))
U11_g(T38, binaryZD_out_g(T38)) → binaryE_out_g(zero(T38))
binaryE_in_g(one(T42)) → U12_g(T42, binaryE_in_g(T42))
U12_g(T42, binaryE_out_g(T42)) → binaryE_out_g(one(T42))
U10_g(T33, binaryE_out_g(T33)) → binaryZD_out_g(one(T33))
U9_g(T29, binaryZD_out_g(T29)) → binaryZD_out_g(zero(T29))
U1_gga(T23, binaryZD_out_g(T23)) → addA_out_gga(zero(T23), b, zero(T23))
addA_in_gga(one(T47), b, one(T47)) → U2_gga(T47, binaryE_in_g(T47))
U2_gga(T47, binaryE_out_g(T47)) → addA_out_gga(one(T47), b, one(T47))
addA_in_gga(b, zero(T68), zero(T68)) → U3_gga(T68, binaryZD_in_g(T68))
U3_gga(T68, binaryZD_out_g(T68)) → addA_out_gga(b, zero(T68), zero(T68))
addA_in_gga(b, one(T74), one(T74)) → U4_gga(T74, binaryE_in_g(T74))
U4_gga(T74, binaryE_out_g(T74)) → addA_out_gga(b, one(T74), one(T74))
addA_in_gga(zero(T102), zero(T103), zero(T105)) → U5_gga(T102, T103, T105, addzF_in_gga(T102, T103, T105))
addzF_in_gga(zero(T121), zero(T122), zero(T124)) → U13_gga(T121, T122, T124, addzF_in_gga(T121, T122, T124))
addzF_in_gga(zero(T140), one(T141), one(T143)) → U14_gga(T140, T141, T143, addxG_in_gga(T140, T141, T143))
addxG_in_gga(one(T149), b, one(T149)) → U32_gga(T149, binaryE_in_g(T149))
U32_gga(T149, binaryE_out_g(T149)) → addxG_out_gga(one(T149), b, one(T149))
addxG_in_gga(zero(T154), b, zero(T154)) → U33_gga(T154, binaryZD_in_g(T154))
U33_gga(T154, binaryZD_out_g(T154)) → addxG_out_gga(zero(T154), b, zero(T154))
addxG_in_gga(T166, T167, T169) → U34_gga(T166, T167, T169, addzF_in_gga(T166, T167, T169))
addzF_in_gga(one(T185), zero(T186), one(T188)) → U15_gga(T185, T186, T188, addyH_in_gga(T185, T186, T188))
addyH_in_gga(b, one(T194), one(T194)) → U35_gga(T194, binaryE_in_g(T194))
U35_gga(T194, binaryE_out_g(T194)) → addyH_out_gga(b, one(T194), one(T194))
addyH_in_gga(b, zero(T199), zero(T199)) → U36_gga(T199, binaryZD_in_g(T199))
U36_gga(T199, binaryZD_out_g(T199)) → addyH_out_gga(b, zero(T199), zero(T199))
addyH_in_gga(T211, T212, T214) → U37_gga(T211, T212, T214, addzF_in_gga(T211, T212, T214))
addzF_in_gga(one(T224), one(T225), zero(T227)) → U16_gga(T224, T225, T227, addcI_in_gga(T224, T225, T227))
addcI_in_gga(b, b, one(b)) → addcI_out_gga(b, b, one(b))
addcI_in_gga(T236, b, T238) → U29_gga(T236, T238, succZK_in_ga(T236, T238))
succZK_in_ga(zero(T244), one(T244)) → U19_ga(T244, binaryZD_in_g(T244))
U19_ga(T244, binaryZD_out_g(T244)) → succZK_out_ga(zero(T244), one(T244))
succZK_in_ga(one(T250), zero(T252)) → U20_ga(T250, T252, succJ_in_ga(T250, T252))
succJ_in_ga(b, one(b)) → succJ_out_ga(b, one(b))
succJ_in_ga(zero(T257), one(T257)) → U17_ga(T257, binaryZD_in_g(T257))
U17_ga(T257, binaryZD_out_g(T257)) → succJ_out_ga(zero(T257), one(T257))
succJ_in_ga(one(T263), zero(T265)) → U18_ga(T263, T265, succJ_in_ga(T263, T265))
U18_ga(T263, T265, succJ_out_ga(T263, T265)) → succJ_out_ga(one(T263), zero(T265))
U20_ga(T250, T252, succJ_out_ga(T250, T252)) → succZK_out_ga(one(T250), zero(T252))
U29_gga(T236, T238, succZK_out_ga(T236, T238)) → addcI_out_gga(T236, b, T238)
addcI_in_gga(b, T274, T276) → U30_gga(T274, T276, succZK_in_ga(T274, T276))
U30_gga(T274, T276, succZK_out_ga(T274, T276)) → addcI_out_gga(b, T274, T276)
addcI_in_gga(T288, T289, T291) → U31_gga(T288, T289, T291, addCL_in_gga(T288, T289, T291))
addCL_in_gga(zero(T307), zero(T308), one(T310)) → U21_gga(T307, T308, T310, addzF_in_gga(T307, T308, T310))
U21_gga(T307, T308, T310, addzF_out_gga(T307, T308, T310)) → addCL_out_gga(zero(T307), zero(T308), one(T310))
addCL_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U22_gga(T335, binaryZD_in_g(T335))
U22_gga(T335, binaryZD_out_g(T335)) → addCL_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCL_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U23_gga(T345, T347, succJ_in_ga(T345, T347))
U23_gga(T345, T347, succJ_out_ga(T345, T347)) → addCL_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCL_in_gga(zero(T358), one(T359), zero(T361)) → U24_gga(T358, T359, T361, addCL_in_gga(T358, T359, T361))
addCL_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U25_gga(T386, binaryZD_in_g(T386))
U25_gga(T386, binaryZD_out_g(T386)) → addCL_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCL_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U26_gga(T396, T398, succJ_in_ga(T396, T398))
U26_gga(T396, T398, succJ_out_ga(T396, T398)) → addCL_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCL_in_gga(one(T409), zero(T410), zero(T412)) → U27_gga(T409, T410, T412, addCL_in_gga(T409, T410, T412))
addCL_in_gga(one(T422), one(T423), one(T425)) → U28_gga(T422, T423, T425, addcI_in_gga(T422, T423, T425))
U28_gga(T422, T423, T425, addcI_out_gga(T422, T423, T425)) → addCL_out_gga(one(T422), one(T423), one(T425))
U27_gga(T409, T410, T412, addCL_out_gga(T409, T410, T412)) → addCL_out_gga(one(T409), zero(T410), zero(T412))
U24_gga(T358, T359, T361, addCL_out_gga(T358, T359, T361)) → addCL_out_gga(zero(T358), one(T359), zero(T361))
U31_gga(T288, T289, T291, addCL_out_gga(T288, T289, T291)) → addcI_out_gga(T288, T289, T291)
U16_gga(T224, T225, T227, addcI_out_gga(T224, T225, T227)) → addzF_out_gga(one(T224), one(T225), zero(T227))
U37_gga(T211, T212, T214, addzF_out_gga(T211, T212, T214)) → addyH_out_gga(T211, T212, T214)
U15_gga(T185, T186, T188, addyH_out_gga(T185, T186, T188)) → addzF_out_gga(one(T185), zero(T186), one(T188))
U34_gga(T166, T167, T169, addzF_out_gga(T166, T167, T169)) → addxG_out_gga(T166, T167, T169)
U14_gga(T140, T141, T143, addxG_out_gga(T140, T141, T143)) → addzF_out_gga(zero(T140), one(T141), one(T143))
U13_gga(T121, T122, T124, addzF_out_gga(T121, T122, T124)) → addzF_out_gga(zero(T121), zero(T122), zero(T124))
U5_gga(T102, T103, T105, addzF_out_gga(T102, T103, T105)) → addA_out_gga(zero(T102), zero(T103), zero(T105))
addA_in_gga(zero(T438), one(T439), one(T441)) → U6_gga(T438, T439, T441, addxG_in_gga(T438, T439, T441))
U6_gga(T438, T439, T441, addxG_out_gga(T438, T439, T441)) → addA_out_gga(zero(T438), one(T439), one(T441))
addA_in_gga(one(T455), zero(T456), one(T458)) → U7_gga(T455, T456, T458, addyH_in_gga(T455, T456, T458))
U7_gga(T455, T456, T458, addyH_out_gga(T455, T456, T458)) → addA_out_gga(one(T455), zero(T456), one(T458))
addA_in_gga(one(T466), one(T467), zero(T469)) → U8_gga(T466, T467, T469, addcI_in_gga(T466, T467, T469))
U8_gga(T466, T467, T469, addcI_out_gga(T466, T467, T469)) → addA_out_gga(one(T466), one(T467), zero(T469))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 58 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

BINARYZD_IN_G(one(T33)) → BINARYE_IN_G(T33)
BINARYE_IN_G(zero(T38)) → BINARYZD_IN_G(T38)
BINARYZD_IN_G(zero(T29)) → BINARYZD_IN_G(T29)
BINARYE_IN_G(one(T42)) → BINARYE_IN_G(T42)

The TRS R consists of the following rules:

addA_in_gga(b, b, b) → addA_out_gga(b, b, b)
addA_in_gga(zero(T23), b, zero(T23)) → U1_gga(T23, binaryZD_in_g(T23))
binaryZD_in_g(zero(T29)) → U9_g(T29, binaryZD_in_g(T29))
binaryZD_in_g(one(T33)) → U10_g(T33, binaryE_in_g(T33))
binaryE_in_g(b) → binaryE_out_g(b)
binaryE_in_g(zero(T38)) → U11_g(T38, binaryZD_in_g(T38))
U11_g(T38, binaryZD_out_g(T38)) → binaryE_out_g(zero(T38))
binaryE_in_g(one(T42)) → U12_g(T42, binaryE_in_g(T42))
U12_g(T42, binaryE_out_g(T42)) → binaryE_out_g(one(T42))
U10_g(T33, binaryE_out_g(T33)) → binaryZD_out_g(one(T33))
U9_g(T29, binaryZD_out_g(T29)) → binaryZD_out_g(zero(T29))
U1_gga(T23, binaryZD_out_g(T23)) → addA_out_gga(zero(T23), b, zero(T23))
addA_in_gga(one(T47), b, one(T47)) → U2_gga(T47, binaryE_in_g(T47))
U2_gga(T47, binaryE_out_g(T47)) → addA_out_gga(one(T47), b, one(T47))
addA_in_gga(b, zero(T68), zero(T68)) → U3_gga(T68, binaryZD_in_g(T68))
U3_gga(T68, binaryZD_out_g(T68)) → addA_out_gga(b, zero(T68), zero(T68))
addA_in_gga(b, one(T74), one(T74)) → U4_gga(T74, binaryE_in_g(T74))
U4_gga(T74, binaryE_out_g(T74)) → addA_out_gga(b, one(T74), one(T74))
addA_in_gga(zero(T102), zero(T103), zero(T105)) → U5_gga(T102, T103, T105, addzF_in_gga(T102, T103, T105))
addzF_in_gga(zero(T121), zero(T122), zero(T124)) → U13_gga(T121, T122, T124, addzF_in_gga(T121, T122, T124))
addzF_in_gga(zero(T140), one(T141), one(T143)) → U14_gga(T140, T141, T143, addxG_in_gga(T140, T141, T143))
addxG_in_gga(one(T149), b, one(T149)) → U32_gga(T149, binaryE_in_g(T149))
U32_gga(T149, binaryE_out_g(T149)) → addxG_out_gga(one(T149), b, one(T149))
addxG_in_gga(zero(T154), b, zero(T154)) → U33_gga(T154, binaryZD_in_g(T154))
U33_gga(T154, binaryZD_out_g(T154)) → addxG_out_gga(zero(T154), b, zero(T154))
addxG_in_gga(T166, T167, T169) → U34_gga(T166, T167, T169, addzF_in_gga(T166, T167, T169))
addzF_in_gga(one(T185), zero(T186), one(T188)) → U15_gga(T185, T186, T188, addyH_in_gga(T185, T186, T188))
addyH_in_gga(b, one(T194), one(T194)) → U35_gga(T194, binaryE_in_g(T194))
U35_gga(T194, binaryE_out_g(T194)) → addyH_out_gga(b, one(T194), one(T194))
addyH_in_gga(b, zero(T199), zero(T199)) → U36_gga(T199, binaryZD_in_g(T199))
U36_gga(T199, binaryZD_out_g(T199)) → addyH_out_gga(b, zero(T199), zero(T199))
addyH_in_gga(T211, T212, T214) → U37_gga(T211, T212, T214, addzF_in_gga(T211, T212, T214))
addzF_in_gga(one(T224), one(T225), zero(T227)) → U16_gga(T224, T225, T227, addcI_in_gga(T224, T225, T227))
addcI_in_gga(b, b, one(b)) → addcI_out_gga(b, b, one(b))
addcI_in_gga(T236, b, T238) → U29_gga(T236, T238, succZK_in_ga(T236, T238))
succZK_in_ga(zero(T244), one(T244)) → U19_ga(T244, binaryZD_in_g(T244))
U19_ga(T244, binaryZD_out_g(T244)) → succZK_out_ga(zero(T244), one(T244))
succZK_in_ga(one(T250), zero(T252)) → U20_ga(T250, T252, succJ_in_ga(T250, T252))
succJ_in_ga(b, one(b)) → succJ_out_ga(b, one(b))
succJ_in_ga(zero(T257), one(T257)) → U17_ga(T257, binaryZD_in_g(T257))
U17_ga(T257, binaryZD_out_g(T257)) → succJ_out_ga(zero(T257), one(T257))
succJ_in_ga(one(T263), zero(T265)) → U18_ga(T263, T265, succJ_in_ga(T263, T265))
U18_ga(T263, T265, succJ_out_ga(T263, T265)) → succJ_out_ga(one(T263), zero(T265))
U20_ga(T250, T252, succJ_out_ga(T250, T252)) → succZK_out_ga(one(T250), zero(T252))
U29_gga(T236, T238, succZK_out_ga(T236, T238)) → addcI_out_gga(T236, b, T238)
addcI_in_gga(b, T274, T276) → U30_gga(T274, T276, succZK_in_ga(T274, T276))
U30_gga(T274, T276, succZK_out_ga(T274, T276)) → addcI_out_gga(b, T274, T276)
addcI_in_gga(T288, T289, T291) → U31_gga(T288, T289, T291, addCL_in_gga(T288, T289, T291))
addCL_in_gga(zero(T307), zero(T308), one(T310)) → U21_gga(T307, T308, T310, addzF_in_gga(T307, T308, T310))
U21_gga(T307, T308, T310, addzF_out_gga(T307, T308, T310)) → addCL_out_gga(zero(T307), zero(T308), one(T310))
addCL_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U22_gga(T335, binaryZD_in_g(T335))
U22_gga(T335, binaryZD_out_g(T335)) → addCL_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCL_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U23_gga(T345, T347, succJ_in_ga(T345, T347))
U23_gga(T345, T347, succJ_out_ga(T345, T347)) → addCL_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCL_in_gga(zero(T358), one(T359), zero(T361)) → U24_gga(T358, T359, T361, addCL_in_gga(T358, T359, T361))
addCL_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U25_gga(T386, binaryZD_in_g(T386))
U25_gga(T386, binaryZD_out_g(T386)) → addCL_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCL_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U26_gga(T396, T398, succJ_in_ga(T396, T398))
U26_gga(T396, T398, succJ_out_ga(T396, T398)) → addCL_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCL_in_gga(one(T409), zero(T410), zero(T412)) → U27_gga(T409, T410, T412, addCL_in_gga(T409, T410, T412))
addCL_in_gga(one(T422), one(T423), one(T425)) → U28_gga(T422, T423, T425, addcI_in_gga(T422, T423, T425))
U28_gga(T422, T423, T425, addcI_out_gga(T422, T423, T425)) → addCL_out_gga(one(T422), one(T423), one(T425))
U27_gga(T409, T410, T412, addCL_out_gga(T409, T410, T412)) → addCL_out_gga(one(T409), zero(T410), zero(T412))
U24_gga(T358, T359, T361, addCL_out_gga(T358, T359, T361)) → addCL_out_gga(zero(T358), one(T359), zero(T361))
U31_gga(T288, T289, T291, addCL_out_gga(T288, T289, T291)) → addcI_out_gga(T288, T289, T291)
U16_gga(T224, T225, T227, addcI_out_gga(T224, T225, T227)) → addzF_out_gga(one(T224), one(T225), zero(T227))
U37_gga(T211, T212, T214, addzF_out_gga(T211, T212, T214)) → addyH_out_gga(T211, T212, T214)
U15_gga(T185, T186, T188, addyH_out_gga(T185, T186, T188)) → addzF_out_gga(one(T185), zero(T186), one(T188))
U34_gga(T166, T167, T169, addzF_out_gga(T166, T167, T169)) → addxG_out_gga(T166, T167, T169)
U14_gga(T140, T141, T143, addxG_out_gga(T140, T141, T143)) → addzF_out_gga(zero(T140), one(T141), one(T143))
U13_gga(T121, T122, T124, addzF_out_gga(T121, T122, T124)) → addzF_out_gga(zero(T121), zero(T122), zero(T124))
U5_gga(T102, T103, T105, addzF_out_gga(T102, T103, T105)) → addA_out_gga(zero(T102), zero(T103), zero(T105))
addA_in_gga(zero(T438), one(T439), one(T441)) → U6_gga(T438, T439, T441, addxG_in_gga(T438, T439, T441))
U6_gga(T438, T439, T441, addxG_out_gga(T438, T439, T441)) → addA_out_gga(zero(T438), one(T439), one(T441))
addA_in_gga(one(T455), zero(T456), one(T458)) → U7_gga(T455, T456, T458, addyH_in_gga(T455, T456, T458))
U7_gga(T455, T456, T458, addyH_out_gga(T455, T456, T458)) → addA_out_gga(one(T455), zero(T456), one(T458))
addA_in_gga(one(T466), one(T467), zero(T469)) → U8_gga(T466, T467, T469, addcI_in_gga(T466, T467, T469))
U8_gga(T466, T467, T469, addcI_out_gga(T466, T467, T469)) → addA_out_gga(one(T466), one(T467), zero(T469))

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

BINARYZD_IN_G(one(T33)) → BINARYE_IN_G(T33)
BINARYE_IN_G(zero(T38)) → BINARYZD_IN_G(T38)
BINARYZD_IN_G(zero(T29)) → BINARYZD_IN_G(T29)
BINARYE_IN_G(one(T42)) → BINARYE_IN_G(T42)

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

(10) PiDPToQDPProof (EQUIVALENT 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:

BINARYZD_IN_G(one(T33)) → BINARYE_IN_G(T33)
BINARYE_IN_G(zero(T38)) → BINARYZD_IN_G(T38)
BINARYZD_IN_G(zero(T29)) → BINARYZD_IN_G(T29)
BINARYE_IN_G(one(T42)) → BINARYE_IN_G(T42)

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:

BINARYE_IN_G(zero(T38)) → BINARYZD_IN_G(T38)
The graph contains the following edges 1 > 1
BINARYE_IN_G(one(T42)) → BINARYE_IN_G(T42)
The graph contains the following edges 1 > 1
BINARYZD_IN_G(zero(T29)) → BINARYZD_IN_G(T29)
The graph contains the following edges 1 > 1
BINARYZD_IN_G(one(T33)) → BINARYE_IN_G(T33)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

SUCCJ_IN_GA(one(T263), zero(T265)) → SUCCJ_IN_GA(T263, T265)

The TRS R consists of the following rules:

addA_in_gga(b, b, b) → addA_out_gga(b, b, b)
addA_in_gga(zero(T23), b, zero(T23)) → U1_gga(T23, binaryZD_in_g(T23))
binaryZD_in_g(zero(T29)) → U9_g(T29, binaryZD_in_g(T29))
binaryZD_in_g(one(T33)) → U10_g(T33, binaryE_in_g(T33))
binaryE_in_g(b) → binaryE_out_g(b)
binaryE_in_g(zero(T38)) → U11_g(T38, binaryZD_in_g(T38))
U11_g(T38, binaryZD_out_g(T38)) → binaryE_out_g(zero(T38))
binaryE_in_g(one(T42)) → U12_g(T42, binaryE_in_g(T42))
U12_g(T42, binaryE_out_g(T42)) → binaryE_out_g(one(T42))
U10_g(T33, binaryE_out_g(T33)) → binaryZD_out_g(one(T33))
U9_g(T29, binaryZD_out_g(T29)) → binaryZD_out_g(zero(T29))
U1_gga(T23, binaryZD_out_g(T23)) → addA_out_gga(zero(T23), b, zero(T23))
addA_in_gga(one(T47), b, one(T47)) → U2_gga(T47, binaryE_in_g(T47))
U2_gga(T47, binaryE_out_g(T47)) → addA_out_gga(one(T47), b, one(T47))
addA_in_gga(b, zero(T68), zero(T68)) → U3_gga(T68, binaryZD_in_g(T68))
U3_gga(T68, binaryZD_out_g(T68)) → addA_out_gga(b, zero(T68), zero(T68))
addA_in_gga(b, one(T74), one(T74)) → U4_gga(T74, binaryE_in_g(T74))
U4_gga(T74, binaryE_out_g(T74)) → addA_out_gga(b, one(T74), one(T74))
addA_in_gga(zero(T102), zero(T103), zero(T105)) → U5_gga(T102, T103, T105, addzF_in_gga(T102, T103, T105))
addzF_in_gga(zero(T121), zero(T122), zero(T124)) → U13_gga(T121, T122, T124, addzF_in_gga(T121, T122, T124))
addzF_in_gga(zero(T140), one(T141), one(T143)) → U14_gga(T140, T141, T143, addxG_in_gga(T140, T141, T143))
addxG_in_gga(one(T149), b, one(T149)) → U32_gga(T149, binaryE_in_g(T149))
U32_gga(T149, binaryE_out_g(T149)) → addxG_out_gga(one(T149), b, one(T149))
addxG_in_gga(zero(T154), b, zero(T154)) → U33_gga(T154, binaryZD_in_g(T154))
U33_gga(T154, binaryZD_out_g(T154)) → addxG_out_gga(zero(T154), b, zero(T154))
addxG_in_gga(T166, T167, T169) → U34_gga(T166, T167, T169, addzF_in_gga(T166, T167, T169))
addzF_in_gga(one(T185), zero(T186), one(T188)) → U15_gga(T185, T186, T188, addyH_in_gga(T185, T186, T188))
addyH_in_gga(b, one(T194), one(T194)) → U35_gga(T194, binaryE_in_g(T194))
U35_gga(T194, binaryE_out_g(T194)) → addyH_out_gga(b, one(T194), one(T194))
addyH_in_gga(b, zero(T199), zero(T199)) → U36_gga(T199, binaryZD_in_g(T199))
U36_gga(T199, binaryZD_out_g(T199)) → addyH_out_gga(b, zero(T199), zero(T199))
addyH_in_gga(T211, T212, T214) → U37_gga(T211, T212, T214, addzF_in_gga(T211, T212, T214))
addzF_in_gga(one(T224), one(T225), zero(T227)) → U16_gga(T224, T225, T227, addcI_in_gga(T224, T225, T227))
addcI_in_gga(b, b, one(b)) → addcI_out_gga(b, b, one(b))
addcI_in_gga(T236, b, T238) → U29_gga(T236, T238, succZK_in_ga(T236, T238))
succZK_in_ga(zero(T244), one(T244)) → U19_ga(T244, binaryZD_in_g(T244))
U19_ga(T244, binaryZD_out_g(T244)) → succZK_out_ga(zero(T244), one(T244))
succZK_in_ga(one(T250), zero(T252)) → U20_ga(T250, T252, succJ_in_ga(T250, T252))
succJ_in_ga(b, one(b)) → succJ_out_ga(b, one(b))
succJ_in_ga(zero(T257), one(T257)) → U17_ga(T257, binaryZD_in_g(T257))
U17_ga(T257, binaryZD_out_g(T257)) → succJ_out_ga(zero(T257), one(T257))
succJ_in_ga(one(T263), zero(T265)) → U18_ga(T263, T265, succJ_in_ga(T263, T265))
U18_ga(T263, T265, succJ_out_ga(T263, T265)) → succJ_out_ga(one(T263), zero(T265))
U20_ga(T250, T252, succJ_out_ga(T250, T252)) → succZK_out_ga(one(T250), zero(T252))
U29_gga(T236, T238, succZK_out_ga(T236, T238)) → addcI_out_gga(T236, b, T238)
addcI_in_gga(b, T274, T276) → U30_gga(T274, T276, succZK_in_ga(T274, T276))
U30_gga(T274, T276, succZK_out_ga(T274, T276)) → addcI_out_gga(b, T274, T276)
addcI_in_gga(T288, T289, T291) → U31_gga(T288, T289, T291, addCL_in_gga(T288, T289, T291))
addCL_in_gga(zero(T307), zero(T308), one(T310)) → U21_gga(T307, T308, T310, addzF_in_gga(T307, T308, T310))
U21_gga(T307, T308, T310, addzF_out_gga(T307, T308, T310)) → addCL_out_gga(zero(T307), zero(T308), one(T310))
addCL_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U22_gga(T335, binaryZD_in_g(T335))
U22_gga(T335, binaryZD_out_g(T335)) → addCL_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCL_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U23_gga(T345, T347, succJ_in_ga(T345, T347))
U23_gga(T345, T347, succJ_out_ga(T345, T347)) → addCL_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCL_in_gga(zero(T358), one(T359), zero(T361)) → U24_gga(T358, T359, T361, addCL_in_gga(T358, T359, T361))
addCL_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U25_gga(T386, binaryZD_in_g(T386))
U25_gga(T386, binaryZD_out_g(T386)) → addCL_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCL_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U26_gga(T396, T398, succJ_in_ga(T396, T398))
U26_gga(T396, T398, succJ_out_ga(T396, T398)) → addCL_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCL_in_gga(one(T409), zero(T410), zero(T412)) → U27_gga(T409, T410, T412, addCL_in_gga(T409, T410, T412))
addCL_in_gga(one(T422), one(T423), one(T425)) → U28_gga(T422, T423, T425, addcI_in_gga(T422, T423, T425))
U28_gga(T422, T423, T425, addcI_out_gga(T422, T423, T425)) → addCL_out_gga(one(T422), one(T423), one(T425))
U27_gga(T409, T410, T412, addCL_out_gga(T409, T410, T412)) → addCL_out_gga(one(T409), zero(T410), zero(T412))
U24_gga(T358, T359, T361, addCL_out_gga(T358, T359, T361)) → addCL_out_gga(zero(T358), one(T359), zero(T361))
U31_gga(T288, T289, T291, addCL_out_gga(T288, T289, T291)) → addcI_out_gga(T288, T289, T291)
U16_gga(T224, T225, T227, addcI_out_gga(T224, T225, T227)) → addzF_out_gga(one(T224), one(T225), zero(T227))
U37_gga(T211, T212, T214, addzF_out_gga(T211, T212, T214)) → addyH_out_gga(T211, T212, T214)
U15_gga(T185, T186, T188, addyH_out_gga(T185, T186, T188)) → addzF_out_gga(one(T185), zero(T186), one(T188))
U34_gga(T166, T167, T169, addzF_out_gga(T166, T167, T169)) → addxG_out_gga(T166, T167, T169)
U14_gga(T140, T141, T143, addxG_out_gga(T140, T141, T143)) → addzF_out_gga(zero(T140), one(T141), one(T143))
U13_gga(T121, T122, T124, addzF_out_gga(T121, T122, T124)) → addzF_out_gga(zero(T121), zero(T122), zero(T124))
U5_gga(T102, T103, T105, addzF_out_gga(T102, T103, T105)) → addA_out_gga(zero(T102), zero(T103), zero(T105))
addA_in_gga(zero(T438), one(T439), one(T441)) → U6_gga(T438, T439, T441, addxG_in_gga(T438, T439, T441))
U6_gga(T438, T439, T441, addxG_out_gga(T438, T439, T441)) → addA_out_gga(zero(T438), one(T439), one(T441))
addA_in_gga(one(T455), zero(T456), one(T458)) → U7_gga(T455, T456, T458, addyH_in_gga(T455, T456, T458))
U7_gga(T455, T456, T458, addyH_out_gga(T455, T456, T458)) → addA_out_gga(one(T455), zero(T456), one(T458))
addA_in_gga(one(T466), one(T467), zero(T469)) → U8_gga(T466, T467, T469, addcI_in_gga(T466, T467, T469))
U8_gga(T466, T467, T469, addcI_out_gga(T466, T467, T469)) → addA_out_gga(one(T466), one(T467), zero(T469))

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

SUCCJ_IN_GA(one(T263), zero(T265)) → SUCCJ_IN_GA(T263, T265)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
SUCCJ_IN_GA(x1, x2) = SUCCJ_IN_GA(x1)

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:

SUCCJ_IN_GA(one(T263)) → SUCCJ_IN_GA(T263)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

SUCCJ_IN_GA(one(T263)) → SUCCJ_IN_GA(T263)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

ADDXG_IN_GGA(T166, T167, T169) → ADDZF_IN_GGA(T166, T167, T169)
ADDZF_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZF_IN_GGA(T121, T122, T124)
ADDZF_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXG_IN_GGA(T140, T141, T143)
ADDZF_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYH_IN_GGA(T185, T186, T188)
ADDYH_IN_GGA(T211, T212, T214) → ADDZF_IN_GGA(T211, T212, T214)
ADDZF_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCI_IN_GGA(T224, T225, T227)
ADDCI_IN_GGA(T288, T289, T291) → ADDCL_IN_GGA(T288, T289, T291)
ADDCL_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZF_IN_GGA(T307, T308, T310)
ADDCL_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCL_IN_GGA(T358, T359, T361)
ADDCL_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCL_IN_GGA(T409, T410, T412)
ADDCL_IN_GGA(one(T422), one(T423), one(T425)) → ADDCI_IN_GGA(T422, T423, T425)

The TRS R consists of the following rules:

addA_in_gga(b, b, b) → addA_out_gga(b, b, b)
addA_in_gga(zero(T23), b, zero(T23)) → U1_gga(T23, binaryZD_in_g(T23))
binaryZD_in_g(zero(T29)) → U9_g(T29, binaryZD_in_g(T29))
binaryZD_in_g(one(T33)) → U10_g(T33, binaryE_in_g(T33))
binaryE_in_g(b) → binaryE_out_g(b)
binaryE_in_g(zero(T38)) → U11_g(T38, binaryZD_in_g(T38))
U11_g(T38, binaryZD_out_g(T38)) → binaryE_out_g(zero(T38))
binaryE_in_g(one(T42)) → U12_g(T42, binaryE_in_g(T42))
U12_g(T42, binaryE_out_g(T42)) → binaryE_out_g(one(T42))
U10_g(T33, binaryE_out_g(T33)) → binaryZD_out_g(one(T33))
U9_g(T29, binaryZD_out_g(T29)) → binaryZD_out_g(zero(T29))
U1_gga(T23, binaryZD_out_g(T23)) → addA_out_gga(zero(T23), b, zero(T23))
addA_in_gga(one(T47), b, one(T47)) → U2_gga(T47, binaryE_in_g(T47))
U2_gga(T47, binaryE_out_g(T47)) → addA_out_gga(one(T47), b, one(T47))
addA_in_gga(b, zero(T68), zero(T68)) → U3_gga(T68, binaryZD_in_g(T68))
U3_gga(T68, binaryZD_out_g(T68)) → addA_out_gga(b, zero(T68), zero(T68))
addA_in_gga(b, one(T74), one(T74)) → U4_gga(T74, binaryE_in_g(T74))
U4_gga(T74, binaryE_out_g(T74)) → addA_out_gga(b, one(T74), one(T74))
addA_in_gga(zero(T102), zero(T103), zero(T105)) → U5_gga(T102, T103, T105, addzF_in_gga(T102, T103, T105))
addzF_in_gga(zero(T121), zero(T122), zero(T124)) → U13_gga(T121, T122, T124, addzF_in_gga(T121, T122, T124))
addzF_in_gga(zero(T140), one(T141), one(T143)) → U14_gga(T140, T141, T143, addxG_in_gga(T140, T141, T143))
addxG_in_gga(one(T149), b, one(T149)) → U32_gga(T149, binaryE_in_g(T149))
U32_gga(T149, binaryE_out_g(T149)) → addxG_out_gga(one(T149), b, one(T149))
addxG_in_gga(zero(T154), b, zero(T154)) → U33_gga(T154, binaryZD_in_g(T154))
U33_gga(T154, binaryZD_out_g(T154)) → addxG_out_gga(zero(T154), b, zero(T154))
addxG_in_gga(T166, T167, T169) → U34_gga(T166, T167, T169, addzF_in_gga(T166, T167, T169))
addzF_in_gga(one(T185), zero(T186), one(T188)) → U15_gga(T185, T186, T188, addyH_in_gga(T185, T186, T188))
addyH_in_gga(b, one(T194), one(T194)) → U35_gga(T194, binaryE_in_g(T194))
U35_gga(T194, binaryE_out_g(T194)) → addyH_out_gga(b, one(T194), one(T194))
addyH_in_gga(b, zero(T199), zero(T199)) → U36_gga(T199, binaryZD_in_g(T199))
U36_gga(T199, binaryZD_out_g(T199)) → addyH_out_gga(b, zero(T199), zero(T199))
addyH_in_gga(T211, T212, T214) → U37_gga(T211, T212, T214, addzF_in_gga(T211, T212, T214))
addzF_in_gga(one(T224), one(T225), zero(T227)) → U16_gga(T224, T225, T227, addcI_in_gga(T224, T225, T227))
addcI_in_gga(b, b, one(b)) → addcI_out_gga(b, b, one(b))
addcI_in_gga(T236, b, T238) → U29_gga(T236, T238, succZK_in_ga(T236, T238))
succZK_in_ga(zero(T244), one(T244)) → U19_ga(T244, binaryZD_in_g(T244))
U19_ga(T244, binaryZD_out_g(T244)) → succZK_out_ga(zero(T244), one(T244))
succZK_in_ga(one(T250), zero(T252)) → U20_ga(T250, T252, succJ_in_ga(T250, T252))
succJ_in_ga(b, one(b)) → succJ_out_ga(b, one(b))
succJ_in_ga(zero(T257), one(T257)) → U17_ga(T257, binaryZD_in_g(T257))
U17_ga(T257, binaryZD_out_g(T257)) → succJ_out_ga(zero(T257), one(T257))
succJ_in_ga(one(T263), zero(T265)) → U18_ga(T263, T265, succJ_in_ga(T263, T265))
U18_ga(T263, T265, succJ_out_ga(T263, T265)) → succJ_out_ga(one(T263), zero(T265))
U20_ga(T250, T252, succJ_out_ga(T250, T252)) → succZK_out_ga(one(T250), zero(T252))
U29_gga(T236, T238, succZK_out_ga(T236, T238)) → addcI_out_gga(T236, b, T238)
addcI_in_gga(b, T274, T276) → U30_gga(T274, T276, succZK_in_ga(T274, T276))
U30_gga(T274, T276, succZK_out_ga(T274, T276)) → addcI_out_gga(b, T274, T276)
addcI_in_gga(T288, T289, T291) → U31_gga(T288, T289, T291, addCL_in_gga(T288, T289, T291))
addCL_in_gga(zero(T307), zero(T308), one(T310)) → U21_gga(T307, T308, T310, addzF_in_gga(T307, T308, T310))
U21_gga(T307, T308, T310, addzF_out_gga(T307, T308, T310)) → addCL_out_gga(zero(T307), zero(T308), one(T310))
addCL_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U22_gga(T335, binaryZD_in_g(T335))
U22_gga(T335, binaryZD_out_g(T335)) → addCL_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCL_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U23_gga(T345, T347, succJ_in_ga(T345, T347))
U23_gga(T345, T347, succJ_out_ga(T345, T347)) → addCL_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCL_in_gga(zero(T358), one(T359), zero(T361)) → U24_gga(T358, T359, T361, addCL_in_gga(T358, T359, T361))
addCL_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U25_gga(T386, binaryZD_in_g(T386))
U25_gga(T386, binaryZD_out_g(T386)) → addCL_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCL_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U26_gga(T396, T398, succJ_in_ga(T396, T398))
U26_gga(T396, T398, succJ_out_ga(T396, T398)) → addCL_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCL_in_gga(one(T409), zero(T410), zero(T412)) → U27_gga(T409, T410, T412, addCL_in_gga(T409, T410, T412))
addCL_in_gga(one(T422), one(T423), one(T425)) → U28_gga(T422, T423, T425, addcI_in_gga(T422, T423, T425))
U28_gga(T422, T423, T425, addcI_out_gga(T422, T423, T425)) → addCL_out_gga(one(T422), one(T423), one(T425))
U27_gga(T409, T410, T412, addCL_out_gga(T409, T410, T412)) → addCL_out_gga(one(T409), zero(T410), zero(T412))
U24_gga(T358, T359, T361, addCL_out_gga(T358, T359, T361)) → addCL_out_gga(zero(T358), one(T359), zero(T361))
U31_gga(T288, T289, T291, addCL_out_gga(T288, T289, T291)) → addcI_out_gga(T288, T289, T291)
U16_gga(T224, T225, T227, addcI_out_gga(T224, T225, T227)) → addzF_out_gga(one(T224), one(T225), zero(T227))
U37_gga(T211, T212, T214, addzF_out_gga(T211, T212, T214)) → addyH_out_gga(T211, T212, T214)
U15_gga(T185, T186, T188, addyH_out_gga(T185, T186, T188)) → addzF_out_gga(one(T185), zero(T186), one(T188))
U34_gga(T166, T167, T169, addzF_out_gga(T166, T167, T169)) → addxG_out_gga(T166, T167, T169)
U14_gga(T140, T141, T143, addxG_out_gga(T140, T141, T143)) → addzF_out_gga(zero(T140), one(T141), one(T143))
U13_gga(T121, T122, T124, addzF_out_gga(T121, T122, T124)) → addzF_out_gga(zero(T121), zero(T122), zero(T124))
U5_gga(T102, T103, T105, addzF_out_gga(T102, T103, T105)) → addA_out_gga(zero(T102), zero(T103), zero(T105))
addA_in_gga(zero(T438), one(T439), one(T441)) → U6_gga(T438, T439, T441, addxG_in_gga(T438, T439, T441))
U6_gga(T438, T439, T441, addxG_out_gga(T438, T439, T441)) → addA_out_gga(zero(T438), one(T439), one(T441))
addA_in_gga(one(T455), zero(T456), one(T458)) → U7_gga(T455, T456, T458, addyH_in_gga(T455, T456, T458))
U7_gga(T455, T456, T458, addyH_out_gga(T455, T456, T458)) → addA_out_gga(one(T455), zero(T456), one(T458))
addA_in_gga(one(T466), one(T467), zero(T469)) → U8_gga(T466, T467, T469, addcI_in_gga(T466, T467, T469))
U8_gga(T466, T467, T469, addcI_out_gga(T466, T467, T469)) → addA_out_gga(one(T466), one(T467), zero(T469))

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

ADDXG_IN_GGA(T166, T167, T169) → ADDZF_IN_GGA(T166, T167, T169)
ADDZF_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZF_IN_GGA(T121, T122, T124)
ADDZF_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXG_IN_GGA(T140, T141, T143)
ADDZF_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYH_IN_GGA(T185, T186, T188)
ADDYH_IN_GGA(T211, T212, T214) → ADDZF_IN_GGA(T211, T212, T214)
ADDZF_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCI_IN_GGA(T224, T225, T227)
ADDCI_IN_GGA(T288, T289, T291) → ADDCL_IN_GGA(T288, T289, T291)
ADDCL_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZF_IN_GGA(T307, T308, T310)
ADDCL_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCL_IN_GGA(T358, T359, T361)
ADDCL_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCL_IN_GGA(T409, T410, T412)
ADDCL_IN_GGA(one(T422), one(T423), one(T425)) → ADDCI_IN_GGA(T422, T423, T425)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
ADDZF_IN_GGA(x1, x2, x3) = ADDZF_IN_GGA(x1, x2)
ADDXG_IN_GGA(x1, x2, x3) = ADDXG_IN_GGA(x1, x2)
ADDYH_IN_GGA(x1, x2, x3) = ADDYH_IN_GGA(x1, x2)
ADDCI_IN_GGA(x1, x2, x3) = ADDCI_IN_GGA(x1, x2)
ADDCL_IN_GGA(x1, x2, x3) = ADDCL_IN_GGA(x1, x2)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

ADDXG_IN_GGA(T166, T167) → ADDZF_IN_GGA(T166, T167)
ADDZF_IN_GGA(zero(T121), zero(T122)) → ADDZF_IN_GGA(T121, T122)
ADDZF_IN_GGA(zero(T140), one(T141)) → ADDXG_IN_GGA(T140, T141)
ADDZF_IN_GGA(one(T185), zero(T186)) → ADDYH_IN_GGA(T185, T186)
ADDYH_IN_GGA(T211, T212) → ADDZF_IN_GGA(T211, T212)
ADDZF_IN_GGA(one(T224), one(T225)) → ADDCI_IN_GGA(T224, T225)
ADDCI_IN_GGA(T288, T289) → ADDCL_IN_GGA(T288, T289)
ADDCL_IN_GGA(zero(T307), zero(T308)) → ADDZF_IN_GGA(T307, T308)
ADDCL_IN_GGA(zero(T358), one(T359)) → ADDCL_IN_GGA(T358, T359)
ADDCL_IN_GGA(one(T409), zero(T410)) → ADDCL_IN_GGA(T409, T410)
ADDCL_IN_GGA(one(T422), one(T423)) → ADDCI_IN_GGA(T422, T423)

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

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

ADDZF_IN_GGA(zero(T140), one(T141)) → ADDXG_IN_GGA(T140, T141)
The graph contains the following edges 1 > 1, 2 > 2
ADDZF_IN_GGA(zero(T121), zero(T122)) → ADDZF_IN_GGA(T121, T122)
The graph contains the following edges 1 > 1, 2 > 2
ADDXG_IN_GGA(T166, T167) → ADDZF_IN_GGA(T166, T167)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDYH_IN_GGA(T211, T212) → ADDZF_IN_GGA(T211, T212)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDCL_IN_GGA(zero(T307), zero(T308)) → ADDZF_IN_GGA(T307, T308)
The graph contains the following edges 1 > 1, 2 > 2
ADDZF_IN_GGA(one(T185), zero(T186)) → ADDYH_IN_GGA(T185, T186)
The graph contains the following edges 1 > 1, 2 > 2
ADDZF_IN_GGA(one(T224), one(T225)) → ADDCI_IN_GGA(T224, T225)
The graph contains the following edges 1 > 1, 2 > 2
ADDCI_IN_GGA(T288, T289) → ADDCL_IN_GGA(T288, T289)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDCL_IN_GGA(one(T422), one(T423)) → ADDCI_IN_GGA(T422, T423)
The graph contains the following edges 1 > 1, 2 > 2
ADDCL_IN_GGA(zero(T358), one(T359)) → ADDCL_IN_GGA(T358, T359)
The graph contains the following edges 1 > 1, 2 > 2
ADDCL_IN_GGA(one(T409), zero(T410)) → ADDCL_IN_GGA(T409, T410)
The graph contains the following edges 1 > 1, 2 > 2

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES