Left Termination proof of /tmp/tmpiJDwu7/binary2.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 626 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 1184 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 0 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(a,a,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: add(T1, T2, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: 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\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | add(T1, T2, b), SCOPE: 1, CLAUSE: 1 | add(T1, T2, b), SCOPE: 1, CLAUSE: 2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: 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\nT3 is ground\nadd(T1, T2, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: add(T1, T2, b), SCOPE: 1, CLAUSE: 1 | add(T1, T2, b), SCOPE: 1, CLAUSE: 2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: binaryZ(b) | add(T1, T2, b), SCOPE: 1, CLAUSE: 2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: add(T1, T2, b), SCOPE: 1, CLAUSE: 2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(T1, T2, b) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: binaryZ(b), SCOPE: 2, CLAUSE: 31 | binaryZ(b), SCOPE: 2, CLAUSE: 32 | ?_2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: binaryZ(b), SCOPE: 2, CLAUSE: 32 | ?_2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ?_2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: add(T1, T2, b), SCOPE: 1, CLAUSE: 2 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: add(T1, T2, b), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: binaryZ(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: binaryZ(b), SCOPE: 3, CLAUSE: 31 | binaryZ(b), SCOPE: 3, CLAUSE: 32\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: binaryZ(b), SCOPE: 3, CLAUSE: 32\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="B: addz(T21, T22, b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: addz(T21, T22, b), SCOPE: 4, CLAUSE: 10 | addz(T21, T22, b), SCOPE: 4, CLAUSE: 11 | addz(T21, T22, b), SCOPE: 4, CLAUSE: 12 | addz(T21, T22, b), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: addz(T21, T22, b), SCOPE: 4, CLAUSE: 11 | addz(T21, T22, b), SCOPE: 4, CLAUSE: 12 | addz(T21, T22, b), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: addz(T21, T22, b), SCOPE: 4, CLAUSE: 12 | addz(T21, T22, b), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: addz(T21, T22, b), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: binaryZ(b) | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(T1, T2, b) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nX41 is free\nadd(T1, T2, b) !=? add(X2, b, X2)\nadd(T1, T2, b) !=? add(b, X41, X41)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: binaryZ(b), SCOPE: 5, CLAUSE: 31 | binaryZ(b), SCOPE: 5, CLAUSE: 32 | ?_5 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(T1, T2, b) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: binaryZ(b), SCOPE: 5, CLAUSE: 32 | ?_5 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(T1, T2, b) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ?_5 | add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(T1, T2, b) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: add(T1, T2, b), SCOPE: 1, CLAUSE: 3\n\nX2 is free\nadd(T1, T2, b) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: addz(T45, T46, b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: addz(T53, T54, b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: addz(T53, T54, b), SCOPE: 6, CLAUSE: 10 | addz(T53, T54, b), SCOPE: 6, CLAUSE: 11 | addz(T53, T54, b), SCOPE: 6, CLAUSE: 12 | addz(T53, T54, b), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: addz(T53, T54, b), SCOPE: 6, CLAUSE: 11 | addz(T53, T54, b), SCOPE: 6, CLAUSE: 12 | addz(T53, T54, b), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: addz(T53, T54, b), SCOPE: 6, CLAUSE: 12 | addz(T53, T54, b), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: addz(T53, T54, b), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: binaryZ(T64) | add(T1, T2, T64), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T64), SCOPE: 1, CLAUSE: 3\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT3 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];
111 [label="111: binaryZ(T64), SCOPE: 7, CLAUSE: 31 | binaryZ(T64), SCOPE: 7, CLAUSE: 32 | ?_7 | add(T1, T2, T64), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T64), SCOPE: 1, CLAUSE: 3\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: binaryZ(T64), SCOPE: 7, CLAUSE: 31\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: binaryZ(T64), SCOPE: 7, CLAUSE: 32 | ?_7 | add(T1, T2, T64), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T64), SCOPE: 1, CLAUSE: 3\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="C: binaryZ(T69)\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: binaryZ(T69), SCOPE: 8, CLAUSE: 31 | binaryZ(T69), SCOPE: 8, CLAUSE: 32\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: binaryZ(T69), SCOPE: 8, CLAUSE: 31\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: binaryZ(T69), SCOPE: 8, CLAUSE: 32\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: binaryZ(T75)\n\nT75 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="D: binary(T79)\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: binary(T79), SCOPE: 9, CLAUSE: 28 | binary(T79), SCOPE: 9, CLAUSE: 29 | binary(T79), SCOPE: 9, CLAUSE: 30\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: binary(T79), SCOPE: 9, CLAUSE: 28\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: binary(T79), SCOPE: 9, CLAUSE: 29 | binary(T79), SCOPE: 9, CLAUSE: 30\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: binary(T79), SCOPE: 9, CLAUSE: 29\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: binary(T79), SCOPE: 9, CLAUSE: 30\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: binaryZ(T84)\n\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: binary(T88)\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: binaryZ(T64), SCOPE: 7, CLAUSE: 32\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ?_7 | add(T1, T2, T64), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T64), SCOPE: 1, CLAUSE: 3\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: binary(T93)\n\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: add(T1, T2, T64), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T64), SCOPE: 1, CLAUSE: 3\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: add(T1, T2, T64), SCOPE: 1, CLAUSE: 2\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: add(T1, T2, T64), SCOPE: 1, CLAUSE: 3\n\nT64 is ground\nadd(T1, T2, T64) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: binaryZ(T98)\n\nT98 is ground\nadd(T1, T2, T98) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="E: addz(T114, T115, T113)\n\nT113 is ground\nadd(T1, T2, T113) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: addz(T114, T115, T113), SCOPE: 10, CLAUSE: 10 | addz(T114, T115, T113), SCOPE: 10, CLAUSE: 11 | addz(T114, T115, T113), SCOPE: 10, CLAUSE: 12 | addz(T114, T115, T113), SCOPE: 10, CLAUSE: 13\n\nT113 is ground\nadd(T1, T2, T113) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: addz(T114, T115, T113), SCOPE: 10, CLAUSE: 10\n\nT113 is ground\nadd(T1, T2, T113) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: addz(T114, T115, T113), SCOPE: 10, CLAUSE: 11 | addz(T114, T115, T113), SCOPE: 10, CLAUSE: 12 | addz(T114, T115, T113), SCOPE: 10, CLAUSE: 13\n\nT113 is ground\nadd(T1, T2, T113) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="F: addz(T134, T135, T133)\n\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: addz(T134, T135, T133), SCOPE: 11, CLAUSE: 10 | addz(T134, T135, T133), SCOPE: 11, CLAUSE: 11 | addz(T134, T135, T133), SCOPE: 11, CLAUSE: 12 | addz(T134, T135, T133), SCOPE: 11, CLAUSE: 13\n\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: addz(T134, T135, T133), SCOPE: 11, CLAUSE: 10\n\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: addz(T134, T135, T133), SCOPE: 11, CLAUSE: 11 | addz(T134, T135, T133), SCOPE: 11, CLAUSE: 12 | addz(T134, T135, T133), SCOPE: 11, CLAUSE: 13\n\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: addz(T154, T155, T153)\n\nT153 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: addz(T134, T135, T133), SCOPE: 11, CLAUSE: 11\n\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: addz(T134, T135, T133), SCOPE: 11, CLAUSE: 12 | addz(T134, T135, T133), SCOPE: 11, CLAUSE: 13\n\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="G: addx(T174, T175, T173)\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: addx(T174, T175, T173), SCOPE: 12, CLAUSE: 4 | addx(T174, T175, T173), SCOPE: 12, CLAUSE: 5 | addx(T174, T175, T173), SCOPE: 12, CLAUSE: 6\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: addx(T174, T175, T173), SCOPE: 12, CLAUSE: 4\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: addx(T174, T175, T173), SCOPE: 12, CLAUSE: 5 | addx(T174, T175, T173), SCOPE: 12, CLAUSE: 6\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: binary(T181)\n\nT181 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: addx(T174, T175, T173), SCOPE: 12, CLAUSE: 5\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: addx(T174, T175, T173), SCOPE: 12, CLAUSE: 6\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: binaryZ(T186)\n\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: addz(T202, T203, T201)\n\nT201 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: addz(T134, T135, T133), SCOPE: 11, CLAUSE: 12\n\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: addz(T134, T135, T133), SCOPE: 11, CLAUSE: 13\n\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="H: addy(T222, T223, T221)\n\nT221 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: addy(T222, T223, T221), SCOPE: 13, CLAUSE: 7 | addy(T222, T223, T221), SCOPE: 13, CLAUSE: 8 | addy(T222, T223, T221), SCOPE: 13, CLAUSE: 9\n\nT221 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: addy(T222, T223, T221), SCOPE: 13, CLAUSE: 7\n\nT221 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: addy(T222, T223, T221), SCOPE: 13, CLAUSE: 8 | addy(T222, T223, T221), SCOPE: 13, CLAUSE: 9\n\nT221 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: binary(T229)\n\nT229 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: addy(T222, T223, T221), SCOPE: 13, CLAUSE: 8\n\nT221 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: addy(T222, T223, T221), SCOPE: 13, CLAUSE: 9\n\nT221 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: binaryZ(T234)\n\nT234 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: addz(T250, T251, T249)\n\nT249 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="I: addc(T264, T265, T263)\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: addc(T264, T265, T263), SCOPE: 14, CLAUSE: 14 | addc(T264, T265, T263), SCOPE: 14, CLAUSE: 15 | addc(T264, T265, T263), SCOPE: 14, CLAUSE: 16 | addc(T264, T265, T263), SCOPE: 14, CLAUSE: 17\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: addc(T264, T265, T263), SCOPE: 14, CLAUSE: 14\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: addc(T264, T265, T263), SCOPE: 14, CLAUSE: 15 | addc(T264, T265, T263), SCOPE: 14, CLAUSE: 16 | addc(T264, T265, T263), SCOPE: 14, CLAUSE: 17\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
308 [label="308: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
309 [label="309: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
310 [label="310: addc(T264, T265, T263), SCOPE: 14, CLAUSE: 15\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
311 [label="311: addc(T264, T265, T263), SCOPE: 14, CLAUSE: 16 | addc(T264, T265, T263), SCOPE: 14, CLAUSE: 17\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="K: succZ(T276, T275)\n\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: succZ(T276, T275), SCOPE: 15, CLAUSE: 36 | succZ(T276, T275), SCOPE: 15, CLAUSE: 37\n\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: succZ(T276, T275), SCOPE: 15, CLAUSE: 36\n\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: succZ(T276, T275), SCOPE: 15, CLAUSE: 37\n\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: binaryZ(T282)\n\nT282 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="J: succ(T290, T289)\n\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: succ(T290, T289), SCOPE: 16, CLAUSE: 33 | succ(T290, T289), SCOPE: 16, CLAUSE: 34 | succ(T290, T289), SCOPE: 16, CLAUSE: 35\n\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: succ(T290, T289), SCOPE: 16, CLAUSE: 33\n\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: succ(T290, T289), SCOPE: 16, CLAUSE: 34 | succ(T290, T289), SCOPE: 16, CLAUSE: 35\n\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: succ(T290, T289), SCOPE: 16, CLAUSE: 34\n\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: succ(T290, T289), SCOPE: 16, CLAUSE: 35\n\nT289 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
342 [label="342: binaryZ(T295)\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
343 [label="343: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: succ(T303, T302)\n\nT302 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
350 [label="350: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
355 [label="355: addc(T264, T265, T263), SCOPE: 14, CLAUSE: 16\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: addc(T264, T265, T263), SCOPE: 14, CLAUSE: 17\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
359 [label="359: succZ(T314, T313)\n\nT313 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
360 [label="360: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="L: addC(T330, T331, T329)\n\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: addC(T330, T331, T329), SCOPE: 17, CLAUSE: 24 | addC(T330, T331, T329), SCOPE: 17, CLAUSE: 25 | addC(T330, T331, T329), SCOPE: 17, CLAUSE: 26 | addC(T330, T331, T329), SCOPE: 17, CLAUSE: 27\n\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
368 [label="368: addC(T330, T331, T329), SCOPE: 17, CLAUSE: 24\n\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
369 [label="369: addC(T330, T331, T329), SCOPE: 17, CLAUSE: 25 | addC(T330, T331, T329), SCOPE: 17, CLAUSE: 26 | addC(T330, T331, T329), SCOPE: 17, CLAUSE: 27\n\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: addz(T350, T351, T349)\n\nT349 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: addC(T330, T331, T329), SCOPE: 17, CLAUSE: 25\n\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: addC(T330, T331, T329), SCOPE: 17, CLAUSE: 26 | addC(T330, T331, T329), SCOPE: 17, CLAUSE: 27\n\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: addX(T370, T371, T369)\n\nT369 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
380 [label="380: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
383 [label="383: addX(T370, T371, T369), SCOPE: 18, CLAUSE: 18 | addX(T370, T371, T369), SCOPE: 18, CLAUSE: 19 | addX(T370, T371, T369), SCOPE: 18, CLAUSE: 20\n\nT369 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
386 [label="386: addX(T370, T371, T369), SCOPE: 18, CLAUSE: 18\n\nT369 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: addX(T370, T371, T369), SCOPE: 18, CLAUSE: 19 | addX(T370, T371, T369), SCOPE: 18, CLAUSE: 20\n\nT369 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
388 [label="388: binaryZ(T377)\n\nT377 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
396 [label="396: addX(T370, T371, T369), SCOPE: 18, CLAUSE: 19\n\nT369 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
397 [label="397: addX(T370, T371, T369), SCOPE: 18, CLAUSE: 20\n\nT369 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
402 [label="402: succ(T389, T388)\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
403 [label="403: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
408 [label="408: addC(T404, T405, T403)\n\nT403 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
413 [label="413: addC(T330, T331, T329), SCOPE: 17, CLAUSE: 26\n\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
414 [label="414: addC(T330, T331, T329), SCOPE: 17, CLAUSE: 27\n\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
415 [label="415: addY(T424, T425, T423)\n\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
416 [label="416: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
418 [label="418: addY(T424, T425, T423), SCOPE: 19, CLAUSE: 21 | addY(T424, T425, T423), SCOPE: 19, CLAUSE: 22 | addY(T424, T425, T423), SCOPE: 19, CLAUSE: 23\n\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
419 [label="419: addY(T424, T425, T423), SCOPE: 19, CLAUSE: 21\n\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
420 [label="420: addY(T424, T425, T423), SCOPE: 19, CLAUSE: 22 | addY(T424, T425, T423), SCOPE: 19, CLAUSE: 23\n\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
421 [label="421: binaryZ(T431)\n\nT431 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
422 [label="422: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
428 [label="428: addY(T424, T425, T423), SCOPE: 19, CLAUSE: 22\n\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
429 [label="429: addY(T424, T425, T423), SCOPE: 19, CLAUSE: 23\n\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
435 [label="435: succ(T443, T442)\n\nT442 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
436 [label="436: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
443 [label="443: addC(T458, T459, T457)\n\nT457 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
446 [label="446: addc(T472, T473, T471)\n\nT471 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
447 [label="447: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
450 [label="450: addz(T114, T115, T113), SCOPE: 10, CLAUSE: 11\n\nT113 is ground\nadd(T1, T2, T113) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: addz(T114, T115, T113), SCOPE: 10, CLAUSE: 12 | addz(T114, T115, T113), SCOPE: 10, CLAUSE: 13\n\nT113 is ground\nadd(T1, T2, T113) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
452 [label="452: addx(T489, T490, T488)\n\nT488 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
454 [label="454: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
466 [label="466: addz(T114, T115, T113), SCOPE: 10, CLAUSE: 12\n\nT113 is ground\nadd(T1, T2, T113) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
467 [label="467: addz(T114, T115, T113), SCOPE: 10, CLAUSE: 13\n\nT113 is ground\nadd(T1, T2, T113) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
470 [label="470: addy(T507, T508, T506)\n\nT506 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
471 [label="471: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
474 [label="474: addc(T519, T520, T518)\n\nT518 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
475 [label="475: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
476 [label="476: binaryZ(T522) | add(T1, T2, T522), SCOPE: 1, CLAUSE: 3\n\nT522 is ground\nX78 is free\nadd(T1, T2, T522) !=? add(b, b, b)\nadd(T1, T2, T522) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
477 [label="477: add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT3 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T3) !=? add(b, b, b)\nadd(T1, T2, T3) !=? add(X78, b, X78)\nadd(T1, T2, T3) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
478 [label="478: binaryZ(T522), SCOPE: 20, CLAUSE: 31 | binaryZ(T522), SCOPE: 20, CLAUSE: 32 | ?_20 | add(T1, T2, T522), SCOPE: 1, CLAUSE: 3\n\nT522 is ground\nX78 is free\nadd(T1, T2, T522) !=? add(b, b, b)\nadd(T1, T2, T522) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
479 [label="479: binaryZ(T522), SCOPE: 20, CLAUSE: 31\n\nT522 is ground\nX78 is free\nadd(T1, T2, T522) !=? add(b, b, b)\nadd(T1, T2, T522) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
480 [label="480: binaryZ(T522), SCOPE: 20, CLAUSE: 32 | ?_20 | add(T1, T2, T522), SCOPE: 1, CLAUSE: 3\n\nT522 is ground\nX78 is free\nadd(T1, T2, T522) !=? add(b, b, b)\nadd(T1, T2, T522) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
483 [label="483: binaryZ(T527)\n\nT527 is ground\nX78 is free\nadd(T1, T2, zero(T527)) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
484 [label="484: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
485 [label="485: binaryZ(T522), SCOPE: 20, CLAUSE: 32\n\nT522 is ground\nX78 is free\nadd(T1, T2, T522) !=? add(b, b, b)\nadd(T1, T2, T522) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
486 [label="486: ?_20 | add(T1, T2, T522), SCOPE: 1, CLAUSE: 3\n\nT522 is ground\nX78 is free\nadd(T1, T2, T522) !=? add(b, b, b)\nadd(T1, T2, T522) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
487 [label="487: binary(T533)\n\nT533 is ground\nX78 is free\nadd(T1, T2, one(T533)) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
488 [label="488: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
489 [label="489: add(T1, T2, T522), SCOPE: 1, CLAUSE: 3\n\nT522 is ground\nX78 is free\nadd(T1, T2, T522) !=? add(b, b, b)\nadd(T1, T2, T522) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
492 [label="492: addz(T548, T549, T547)\n\nT547 is ground\nX78 is free\nadd(T1, T2, T547) !=? add(b, b, b)\nadd(T1, T2, T547) !=? add(X78, b, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
493 [label="493: addz(T559, T560, T558)\n\nT558 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T558) !=? add(b, b, b)\nadd(T1, T2, T558) !=? add(X78, b, X78)\nadd(T1, T2, T558) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
494 [label="494: addz(T559, T560, T558), SCOPE: 21, CLAUSE: 10 | addz(T559, T560, T558), SCOPE: 21, CLAUSE: 11 | addz(T559, T560, T558), SCOPE: 21, CLAUSE: 12 | addz(T559, T560, T558), SCOPE: 21, CLAUSE: 13\n\nT558 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T558) !=? add(b, b, b)\nadd(T1, T2, T558) !=? add(X78, b, X78)\nadd(T1, T2, T558) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
497 [label="497: addz(T559, T560, T558), SCOPE: 21, CLAUSE: 10\n\nT558 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T558) !=? add(b, b, b)\nadd(T1, T2, T558) !=? add(X78, b, X78)\nadd(T1, T2, T558) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
498 [label="498: addz(T559, T560, T558), SCOPE: 21, CLAUSE: 11 | addz(T559, T560, T558), SCOPE: 21, CLAUSE: 12 | addz(T559, T560, T558), SCOPE: 21, CLAUSE: 13\n\nT558 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T558) !=? add(b, b, b)\nadd(T1, T2, T558) !=? add(X78, b, X78)\nadd(T1, T2, T558) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
499 [label="499: addz(T576, T577, T575)\n\nT575 is ground\nX78 is free\nX482 is free\nadd(T1, T2, zero(T575)) !=? add(X78, b, X78)\nadd(T1, T2, zero(T575)) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
500 [label="500: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
503 [label="503: addz(T559, T560, T558), SCOPE: 21, CLAUSE: 11\n\nT558 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T558) !=? add(b, b, b)\nadd(T1, T2, T558) !=? add(X78, b, X78)\nadd(T1, T2, T558) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
504 [label="504: addz(T559, T560, T558), SCOPE: 21, CLAUSE: 12 | addz(T559, T560, T558), SCOPE: 21, CLAUSE: 13\n\nT558 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T558) !=? add(b, b, b)\nadd(T1, T2, T558) !=? add(X78, b, X78)\nadd(T1, T2, T558) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
521 [label="521: addx(T596, T597, T595)\n\nT595 is ground\nX78 is free\nX482 is free\nadd(T1, T2, one(T595)) !=? add(X78, b, X78)\nadd(T1, T2, one(T595)) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
522 [label="522: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
532 [label="532: addz(T559, T560, T558), SCOPE: 21, CLAUSE: 12\n\nT558 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T558) !=? add(b, b, b)\nadd(T1, T2, T558) !=? add(X78, b, X78)\nadd(T1, T2, T558) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
533 [label="533: addz(T559, T560, T558), SCOPE: 21, CLAUSE: 13\n\nT558 is ground\nX78 is free\nX482 is free\nadd(T1, T2, T558) !=? add(b, b, b)\nadd(T1, T2, T558) !=? add(X78, b, X78)\nadd(T1, T2, T558) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
536 [label="536: addy(T614, T615, T613)\n\nT613 is ground\nX78 is free\nX482 is free\nadd(T1, T2, one(T613)) !=? add(X78, b, X78)\nadd(T1, T2, one(T613)) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
537 [label="537: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
538 [label="538: addc(T626, T627, T625)\n\nT625 is ground\nX78 is free\nX482 is free\nadd(T1, T2, zero(T625)) !=? add(X78, b, X78)\nadd(T1, T2, zero(T625)) !=? add(b, X482, X482)", fontsize=16, style=filled, fillcolor=lightyellow];
539 [label="539: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
540 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 540 [arrowhead = none ];
540 -> 5;

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

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

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

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

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

546 [label="EVAL with clause\nadd(X2, b, X2) :- binaryZ(X2).\nand substitutionT1 -> b,\nX2 -> b,\nT2 -> b,\nT5 -> b", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 546 [arrowhead = none ];
546 -> 16;

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

548 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 548 [arrowhead = none ];
548 -> 20;

549 [label="EVAL with clause\nadd(b, X41, X41) :- binaryZ(X41).\nand substitutionT1 -> b,\nT2 -> b,\nX41 -> b,\nT34 -> b", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 549 [arrowhead = none ];
549 -> 68;

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

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

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

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

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

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

556 [label="EVAL with clause\nadd(b, X9, X9) :- binaryZ(X9).\nand substitutionT1 -> b,\nT2 -> b,\nX9 -> b,\nT10 -> b", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 556 [arrowhead = none ];
556 -> 36;

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

558 [label="ONLY EVAL with clause\nadd(X22, X23, X24) :- addz(X22, X23, X24).\nand substitutionT1 -> T21,\nX22 -> T21,\nT2 -> T22,\nX23 -> T22,\nX24 -> b,\nT19 -> T21,\nT20 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 558 [arrowhead = none ];
558 -> 52;

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

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

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

562 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
52 -> 562 [arrowhead = none ];
562 -> 55;

563 [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];
55 -> 563 [arrowhead = none ];
563 -> 56;

564 [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];
56 -> 564 [arrowhead = none ];
564 -> 57;

565 [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];
57 -> 565 [arrowhead = none ];
565 -> 58;

566 [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];
58 -> 566 [arrowhead = none ];
566 -> 61;

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

568 [label="ONLY EVAL with clause\nadd(X62, X63, X64) :- addz(X62, X63, X64).\nand substitutionT1 -> T53,\nX62 -> T53,\nT2 -> T54,\nX63 -> T54,\nX64 -> b,\nT51 -> T53,\nT52 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 568 [arrowhead = none ];
568 -> 92;

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

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

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

572 [label="ONLY EVAL with clause\nadd(X53, X54, X55) :- addz(X53, X54, X55).\nand substitutionT1 -> T45,\nX53 -> T45,\nT2 -> T46,\nX54 -> T46,\nX55 -> b,\nT43 -> T45,\nT44 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 572 [arrowhead = none ];
572 -> 89;

573 [label="INSTANCE with matching:\nT21 -> T45\nT22 -> T46", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 573 [arrowhead = none , style=dashed];
573 -> 52[style=dashed];

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

575 [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];
93 -> 575 [arrowhead = none ];
575 -> 95;

576 [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];
95 -> 576 [arrowhead = none ];
576 -> 96;

577 [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];
96 -> 577 [arrowhead = none ];
577 -> 104;

578 [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];
104 -> 578 [arrowhead = none ];
578 -> 105;

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

580 [label="EVAL with clause\nadd(b, X482, X482) :- binaryZ(X482).\nand substitutionT1 -> b,\nT2 -> T522,\nX482 -> T522,\nT3 -> T522", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 580 [arrowhead = none ];
580 -> 476;

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

582 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
111 -> 582 [arrowhead = none ];
582 -> 112;

583 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
111 -> 583 [arrowhead = none ];
583 -> 113;

584 [label="EVAL with clause\nbinaryZ(zero(X83)) :- binaryZ(X83).\nand substitutionX83 -> T69,\nT64 -> zero(T69)", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 584 [arrowhead = none ];
584 -> 116;

585 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 585 [arrowhead = none ];
585 -> 117;

586 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
113 -> 586 [arrowhead = none ];
586 -> 155;

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

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

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

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

591 [label="EVAL with clause\nbinaryZ(zero(X89)) :- binaryZ(X89).\nand substitutionX89 -> T75,\nT69 -> zero(T75)", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 591 [arrowhead = none ];
591 -> 123;

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

593 [label="EVAL with clause\nbinaryZ(one(X93)) :- binary(X93).\nand substitutionX93 -> T79,\nT69 -> one(T79)", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 593 [arrowhead = none ];
593 -> 126;

594 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 594 [arrowhead = none ];
594 -> 127;

595 [label="INSTANCE with matching:\nT69 -> T75", fontsize=14, style = filled, fillcolor = lightgrey];
123 -> 595 [arrowhead = none , style=dashed];
595 -> 116[style=dashed];

596 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
126 -> 596 [arrowhead = none ];
596 -> 132;

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

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

599 [label="EVAL with clause\nbinary(b).\nand substitutionT79 -> b", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 599 [arrowhead = none ];
599 -> 136;

600 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 600 [arrowhead = none ];
600 -> 137;

601 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
134 -> 601 [arrowhead = none ];
601 -> 142;

602 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
134 -> 602 [arrowhead = none ];
602 -> 143;

603 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 603 [arrowhead = none ];
603 -> 138;

604 [label="EVAL with clause\nbinary(zero(X98)) :- binaryZ(X98).\nand substitutionX98 -> T84,\nT79 -> zero(T84)", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 604 [arrowhead = none ];
604 -> 145;

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

606 [label="EVAL with clause\nbinary(one(X102)) :- binary(X102).\nand substitutionX102 -> T88,\nT79 -> one(T88)", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 606 [arrowhead = none ];
606 -> 152;

607 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 607 [arrowhead = none ];
607 -> 153;

608 [label="INSTANCE with matching:\nT69 -> T84", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 608 [arrowhead = none , style=dashed];
608 -> 116[style=dashed];

609 [label="INSTANCE with matching:\nT79 -> T88", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 609 [arrowhead = none , style=dashed];
609 -> 126[style=dashed];

610 [label="EVAL with clause\nbinaryZ(one(X107)) :- binary(X107).\nand substitutionX107 -> T93,\nT64 -> one(T93)", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 610 [arrowhead = none ];
610 -> 158;

611 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 611 [arrowhead = none ];
611 -> 159;

612 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 612 [arrowhead = none ];
612 -> 161;

613 [label="INSTANCE with matching:\nT79 -> T93", fontsize=14, style = filled, fillcolor = lightgrey];
158 -> 613 [arrowhead = none , style=dashed];
613 -> 126[style=dashed];

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

615 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 615 [arrowhead = none ];
615 -> 163;

616 [label="EVAL with clause\nadd(b, X112, X112) :- binaryZ(X112).\nand substitutionT1 -> b,\nT2 -> T98,\nX112 -> T98,\nT64 -> T98", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 616 [arrowhead = none ];
616 -> 169;

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

618 [label="ONLY EVAL with clause\nadd(X123, X124, X125) :- addz(X123, X124, X125).\nand substitutionT1 -> T114,\nX123 -> T114,\nT2 -> T115,\nX124 -> T115,\nT64 -> T113,\nX125 -> T113,\nT111 -> T114,\nT112 -> T115", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 618 [arrowhead = none ];
618 -> 179;

619 [label="INSTANCE with matching:\nT69 -> T98", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 619 [arrowhead = none , style=dashed];
619 -> 116[style=dashed];

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

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

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

623 [label="EVAL with clause\naddz(zero(X141), zero(X142), zero(X143)) :- addz(X141, X142, X143).\nand substitutionX141 -> T134,\nT114 -> zero(T134),\nX142 -> T135,\nT115 -> zero(T135),\nX143 -> T133,\nT113 -> zero(T133),\nT131 -> T134,\nT132 -> T135", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 623 [arrowhead = none ];
623 -> 189;

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

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

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

627 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
189 -> 627 [arrowhead = none ];
627 -> 196;

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

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

630 [label="EVAL with clause\naddz(zero(X159), zero(X160), zero(X161)) :- addz(X159, X160, X161).\nand substitutionX159 -> T154,\nT134 -> zero(T154),\nX160 -> T155,\nT135 -> zero(T155),\nX161 -> T153,\nT133 -> zero(T153),\nT151 -> T154,\nT152 -> T155", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 630 [arrowhead = none ];
630 -> 213;

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

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

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

634 [label="INSTANCE with matching:\nT134 -> T154\nT135 -> T155\nT133 -> T153", fontsize=14, style = filled, fillcolor = lightgrey];
213 -> 634 [arrowhead = none , style=dashed];
634 -> 189[style=dashed];

635 [label="EVAL with clause\naddz(zero(X177), one(X178), one(X179)) :- addx(X177, X178, X179).\nand substitutionX177 -> T174,\nT134 -> zero(T174),\nX178 -> T175,\nT135 -> one(T175),\nX179 -> T173,\nT133 -> one(T173),\nT171 -> T174,\nT172 -> T175", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 635 [arrowhead = none ];
635 -> 229;

636 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
225 -> 636 [arrowhead = none ];
636 -> 230;

637 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
226 -> 637 [arrowhead = none ];
637 -> 271;

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

639 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
229 -> 639 [arrowhead = none ];
639 -> 234;

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

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

642 [label="EVAL with clause\naddx(one(X185), b, one(X185)) :- binary(X185).\nand substitutionX185 -> T181,\nT174 -> one(T181),\nT175 -> b,\nT173 -> one(T181)", fontsize=14, style = filled, fillcolor = lightblue];
235 -> 642 [arrowhead = none ];
642 -> 239;

643 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
235 -> 643 [arrowhead = none ];
643 -> 240;

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

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

646 [label="INSTANCE with matching:\nT79 -> T181", fontsize=14, style = filled, fillcolor = lightgrey];
239 -> 646 [arrowhead = none , style=dashed];
646 -> 126[style=dashed];

647 [label="EVAL with clause\naddx(zero(X190), b, zero(X190)) :- binaryZ(X190).\nand substitutionX190 -> T186,\nT174 -> zero(T186),\nT175 -> b,\nT173 -> zero(T186)", fontsize=14, style = filled, fillcolor = lightblue];
241 -> 647 [arrowhead = none ];
647 -> 248;

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

649 [label="ONLY EVAL with clause\naddx(X201, X202, X203) :- addz(X201, X202, X203).\nand substitutionT174 -> T202,\nX201 -> T202,\nT175 -> T203,\nX202 -> T203,\nT173 -> T201,\nX203 -> T201,\nT199 -> T202,\nT200 -> T203", fontsize=14, style = filled, fillcolor = lightblue];
242 -> 649 [arrowhead = none ];
649 -> 266;

650 [label="INSTANCE with matching:\nT69 -> T186", fontsize=14, style = filled, fillcolor = lightgrey];
248 -> 650 [arrowhead = none , style=dashed];
650 -> 116[style=dashed];

651 [label="INSTANCE with matching:\nT134 -> T202\nT135 -> T203\nT133 -> T201", fontsize=14, style = filled, fillcolor = lightgrey];
266 -> 651 [arrowhead = none , style=dashed];
651 -> 189[style=dashed];

652 [label="EVAL with clause\naddz(one(X219), zero(X220), one(X221)) :- addy(X219, X220, X221).\nand substitutionX219 -> T222,\nT134 -> one(T222),\nX220 -> T223,\nT135 -> zero(T223),\nX221 -> T221,\nT133 -> one(T221),\nT219 -> T222,\nT220 -> T223", fontsize=14, style = filled, fillcolor = lightblue];
271 -> 652 [arrowhead = none ];
652 -> 275;

653 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
271 -> 653 [arrowhead = none ];
653 -> 276;

654 [label="EVAL with clause\naddz(one(X255), one(X256), zero(X257)) :- addc(X255, X256, X257).\nand substitutionX255 -> T264,\nT134 -> one(T264),\nX256 -> T265,\nT135 -> one(T265),\nX257 -> T263,\nT133 -> zero(T263),\nT261 -> T264,\nT262 -> T265", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 654 [arrowhead = none ];
654 -> 302;

655 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
272 -> 655 [arrowhead = none ];
655 -> 303;

656 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
275 -> 656 [arrowhead = none ];
656 -> 278;

657 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
278 -> 657 [arrowhead = none ];
657 -> 279;

658 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
278 -> 658 [arrowhead = none ];
658 -> 280;

659 [label="EVAL with clause\naddy(b, one(X227), one(X227)) :- binary(X227).\nand substitutionT222 -> b,\nX227 -> T229,\nT223 -> one(T229),\nT221 -> one(T229)", fontsize=14, style = filled, fillcolor = lightblue];
279 -> 659 [arrowhead = none ];
659 -> 283;

660 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
279 -> 660 [arrowhead = none ];
660 -> 284;

661 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
280 -> 661 [arrowhead = none ];
661 -> 287;

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

663 [label="INSTANCE with matching:\nT79 -> T229", fontsize=14, style = filled, fillcolor = lightgrey];
283 -> 663 [arrowhead = none , style=dashed];
663 -> 126[style=dashed];

664 [label="EVAL with clause\naddy(b, zero(X232), zero(X232)) :- binaryZ(X232).\nand substitutionT222 -> b,\nX232 -> T234,\nT223 -> zero(T234),\nT221 -> zero(T234)", fontsize=14, style = filled, fillcolor = lightblue];
287 -> 664 [arrowhead = none ];
664 -> 290;

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

666 [label="ONLY EVAL with clause\naddy(X243, X244, X245) :- addz(X243, X244, X245).\nand substitutionT222 -> T250,\nX243 -> T250,\nT223 -> T251,\nX244 -> T251,\nT221 -> T249,\nX245 -> T249,\nT247 -> T250,\nT248 -> T251", fontsize=14, style = filled, fillcolor = lightblue];
288 -> 666 [arrowhead = none ];
666 -> 296;

667 [label="INSTANCE with matching:\nT69 -> T234", fontsize=14, style = filled, fillcolor = lightgrey];
290 -> 667 [arrowhead = none , style=dashed];
667 -> 116[style=dashed];

668 [label="INSTANCE with matching:\nT134 -> T250\nT135 -> T251\nT133 -> T249", fontsize=14, style = filled, fillcolor = lightgrey];
296 -> 668 [arrowhead = none , style=dashed];
668 -> 189[style=dashed];

669 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
302 -> 669 [arrowhead = none ];
669 -> 304;

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

671 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
304 -> 671 [arrowhead = none ];
671 -> 306;

672 [label="EVAL with clause\naddc(b, b, one(b)).\nand substitutionT264 -> b,\nT265 -> b,\nT263 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
305 -> 672 [arrowhead = none ];
672 -> 307;

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

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

675 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
306 -> 675 [arrowhead = none ];
675 -> 311;

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

677 [label="EVAL with clause\naddc(X266, b, X267) :- succZ(X266, X267).\nand substitutionT264 -> T276,\nX266 -> T276,\nT265 -> b,\nT263 -> T275,\nX267 -> T275,\nT274 -> T276", fontsize=14, style = filled, fillcolor = lightblue];
310 -> 677 [arrowhead = none ];
677 -> 314;

678 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
310 -> 678 [arrowhead = none ];
678 -> 315;

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

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

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

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

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

684 [label="EVAL with clause\nsuccZ(zero(X273), one(X273)) :- binaryZ(X273).\nand substitutionX273 -> T282,\nT276 -> zero(T282),\nT275 -> one(T282)", fontsize=14, style = filled, fillcolor = lightblue];
319 -> 684 [arrowhead = none ];
684 -> 323;

685 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
319 -> 685 [arrowhead = none ];
685 -> 324;

686 [label="EVAL with clause\nsuccZ(one(X279), zero(X280)) :- succ(X279, X280).\nand substitutionX279 -> T290,\nT276 -> one(T290),\nX280 -> T289,\nT275 -> zero(T289),\nT288 -> T290", fontsize=14, style = filled, fillcolor = lightblue];
320 -> 686 [arrowhead = none ];
686 -> 327;

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

688 [label="INSTANCE with matching:\nT69 -> T282", fontsize=14, style = filled, fillcolor = lightgrey];
323 -> 688 [arrowhead = none , style=dashed];
688 -> 116[style=dashed];

689 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
327 -> 689 [arrowhead = none ];
689 -> 329;

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

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

692 [label="EVAL with clause\nsucc(b, one(b)).\nand substitutionT290 -> b,\nT289 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
331 -> 692 [arrowhead = none ];
692 -> 334;

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

694 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
333 -> 694 [arrowhead = none ];
694 -> 338;

695 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
333 -> 695 [arrowhead = none ];
695 -> 339;

696 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
334 -> 696 [arrowhead = none ];
696 -> 336;

697 [label="EVAL with clause\nsucc(zero(X285), one(X285)) :- binaryZ(X285).\nand substitutionX285 -> T295,\nT290 -> zero(T295),\nT289 -> one(T295)", fontsize=14, style = filled, fillcolor = lightblue];
338 -> 697 [arrowhead = none ];
697 -> 342;

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

699 [label="EVAL with clause\nsucc(one(X291), zero(X292)) :- succ(X291, X292).\nand substitutionX291 -> T303,\nT290 -> one(T303),\nX292 -> T302,\nT289 -> zero(T302),\nT301 -> T303", fontsize=14, style = filled, fillcolor = lightblue];
339 -> 699 [arrowhead = none ];
699 -> 349;

700 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
339 -> 700 [arrowhead = none ];
700 -> 350;

701 [label="INSTANCE with matching:\nT69 -> T295", fontsize=14, style = filled, fillcolor = lightgrey];
342 -> 701 [arrowhead = none , style=dashed];
701 -> 116[style=dashed];

702 [label="INSTANCE with matching:\nT290 -> T303\nT289 -> T302", fontsize=14, style = filled, fillcolor = lightgrey];
349 -> 702 [arrowhead = none , style=dashed];
702 -> 327[style=dashed];

703 [label="EVAL with clause\naddc(b, X301, X302) :- succZ(X301, X302).\nand substitutionT264 -> b,\nT265 -> T314,\nX301 -> T314,\nT263 -> T313,\nX302 -> T313,\nT312 -> T314", fontsize=14, style = filled, fillcolor = lightblue];
355 -> 703 [arrowhead = none ];
703 -> 359;

704 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
355 -> 704 [arrowhead = none ];
704 -> 360;

705 [label="ONLY EVAL with clause\naddc(X313, X314, X315) :- addC(X313, X314, X315).\nand substitutionT264 -> T330,\nX313 -> T330,\nT265 -> T331,\nX314 -> T331,\nT263 -> T329,\nX315 -> T329,\nT327 -> T330,\nT328 -> T331", fontsize=14, style = filled, fillcolor = lightblue];
356 -> 705 [arrowhead = none ];
705 -> 365;

706 [label="INSTANCE with matching:\nT276 -> T314\nT275 -> T313", fontsize=14, style = filled, fillcolor = lightgrey];
359 -> 706 [arrowhead = none , style=dashed];
706 -> 314[style=dashed];

707 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
365 -> 707 [arrowhead = none ];
707 -> 366;

708 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
366 -> 708 [arrowhead = none ];
708 -> 368;

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

710 [label="EVAL with clause\naddC(zero(X331), zero(X332), one(X333)) :- addz(X331, X332, X333).\nand substitutionX331 -> T350,\nT330 -> zero(T350),\nX332 -> T351,\nT331 -> zero(T351),\nX333 -> T349,\nT329 -> one(T349),\nT347 -> T350,\nT348 -> T351", fontsize=14, style = filled, fillcolor = lightblue];
368 -> 710 [arrowhead = none ];
710 -> 370;

711 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
368 -> 711 [arrowhead = none ];
711 -> 371;

712 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
369 -> 712 [arrowhead = none ];
712 -> 375;

713 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
369 -> 713 [arrowhead = none ];
713 -> 376;

714 [label="INSTANCE with matching:\nT134 -> T350\nT135 -> T351\nT133 -> T349", fontsize=14, style = filled, fillcolor = lightgrey];
370 -> 714 [arrowhead = none , style=dashed];
714 -> 189[style=dashed];

715 [label="EVAL with clause\naddC(zero(X349), one(X350), zero(X351)) :- addX(X349, X350, X351).\nand substitutionX349 -> T370,\nT330 -> zero(T370),\nX350 -> T371,\nT331 -> one(T371),\nX351 -> T369,\nT329 -> zero(T369),\nT367 -> T370,\nT368 -> T371", fontsize=14, style = filled, fillcolor = lightblue];
375 -> 715 [arrowhead = none ];
715 -> 379;

716 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
375 -> 716 [arrowhead = none ];
716 -> 380;

717 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
376 -> 717 [arrowhead = none ];
717 -> 413;

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

719 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
379 -> 719 [arrowhead = none ];
719 -> 383;

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

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

722 [label="EVAL with clause\naddX(zero(X357), b, one(X357)) :- binaryZ(X357).\nand substitutionX357 -> T377,\nT370 -> zero(T377),\nT371 -> b,\nT369 -> one(T377)", fontsize=14, style = filled, fillcolor = lightblue];
386 -> 722 [arrowhead = none ];
722 -> 388;

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

724 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
387 -> 724 [arrowhead = none ];
724 -> 396;

725 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
387 -> 725 [arrowhead = none ];
725 -> 397;

726 [label="INSTANCE with matching:\nT69 -> T377", fontsize=14, style = filled, fillcolor = lightgrey];
388 -> 726 [arrowhead = none , style=dashed];
726 -> 116[style=dashed];

727 [label="EVAL with clause\naddX(one(X367), b, zero(X368)) :- succ(X367, X368).\nand substitutionX367 -> T389,\nT370 -> one(T389),\nT371 -> b,\nX368 -> T388,\nT369 -> zero(T388),\nT387 -> T389", fontsize=14, style = filled, fillcolor = lightblue];
396 -> 727 [arrowhead = none ];
727 -> 402;

728 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
396 -> 728 [arrowhead = none ];
728 -> 403;

729 [label="ONLY EVAL with clause\naddX(X378, X379, X380) :- addC(X378, X379, X380).\nand substitutionT370 -> T404,\nX378 -> T404,\nT371 -> T405,\nX379 -> T405,\nT369 -> T403,\nX380 -> T403,\nT401 -> T404,\nT402 -> T405", fontsize=14, style = filled, fillcolor = lightblue];
397 -> 729 [arrowhead = none ];
729 -> 408;

730 [label="INSTANCE with matching:\nT290 -> T389\nT289 -> T388", fontsize=14, style = filled, fillcolor = lightgrey];
402 -> 730 [arrowhead = none , style=dashed];
730 -> 327[style=dashed];

731 [label="INSTANCE with matching:\nT330 -> T404\nT331 -> T405\nT329 -> T403", fontsize=14, style = filled, fillcolor = lightgrey];
408 -> 731 [arrowhead = none , style=dashed];
731 -> 365[style=dashed];

732 [label="EVAL with clause\naddC(one(X396), zero(X397), zero(X398)) :- addY(X396, X397, X398).\nand substitutionX396 -> T424,\nT330 -> one(T424),\nX397 -> T425,\nT331 -> zero(T425),\nX398 -> T423,\nT329 -> zero(T423),\nT421 -> T424,\nT422 -> T425", fontsize=14, style = filled, fillcolor = lightblue];
413 -> 732 [arrowhead = none ];
732 -> 415;

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

734 [label="EVAL with clause\naddC(one(X437), one(X438), one(X439)) :- addc(X437, X438, X439).\nand substitutionX437 -> T472,\nT330 -> one(T472),\nX438 -> T473,\nT331 -> one(T473),\nX439 -> T471,\nT329 -> one(T471),\nT469 -> T472,\nT470 -> T473", fontsize=14, style = filled, fillcolor = lightblue];
414 -> 734 [arrowhead = none ];
734 -> 446;

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

736 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
415 -> 736 [arrowhead = none ];
736 -> 418;

737 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
418 -> 737 [arrowhead = none ];
737 -> 419;

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

739 [label="EVAL with clause\naddY(b, zero(X404), one(X404)) :- binaryZ(X404).\nand substitutionT424 -> b,\nX404 -> T431,\nT425 -> zero(T431),\nT423 -> one(T431)", fontsize=14, style = filled, fillcolor = lightblue];
419 -> 739 [arrowhead = none ];
739 -> 421;

740 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
419 -> 740 [arrowhead = none ];
740 -> 422;

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

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

743 [label="INSTANCE with matching:\nT69 -> T431", fontsize=14, style = filled, fillcolor = lightgrey];
421 -> 743 [arrowhead = none , style=dashed];
743 -> 116[style=dashed];

744 [label="EVAL with clause\naddY(b, one(X414), zero(X415)) :- succ(X414, X415).\nand substitutionT424 -> b,\nX414 -> T443,\nT425 -> one(T443),\nX415 -> T442,\nT423 -> zero(T442),\nT441 -> T443", fontsize=14, style = filled, fillcolor = lightblue];
428 -> 744 [arrowhead = none ];
744 -> 435;

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

746 [label="ONLY EVAL with clause\naddY(X425, X426, X427) :- addC(X425, X426, X427).\nand substitutionT424 -> T458,\nX425 -> T458,\nT425 -> T459,\nX426 -> T459,\nT423 -> T457,\nX427 -> T457,\nT455 -> T458,\nT456 -> T459", fontsize=14, style = filled, fillcolor = lightblue];
429 -> 746 [arrowhead = none ];
746 -> 443;

747 [label="INSTANCE with matching:\nT290 -> T443\nT289 -> T442", fontsize=14, style = filled, fillcolor = lightgrey];
435 -> 747 [arrowhead = none , style=dashed];
747 -> 327[style=dashed];

748 [label="INSTANCE with matching:\nT330 -> T458\nT331 -> T459\nT329 -> T457", fontsize=14, style = filled, fillcolor = lightgrey];
443 -> 748 [arrowhead = none , style=dashed];
748 -> 365[style=dashed];

749 [label="INSTANCE with matching:\nT264 -> T472\nT265 -> T473\nT263 -> T471", fontsize=14, style = filled, fillcolor = lightgrey];
446 -> 749 [arrowhead = none , style=dashed];
749 -> 302[style=dashed];

750 [label="EVAL with clause\naddz(zero(X452), one(X453), one(X454)) :- addx(X452, X453, X454).\nand substitutionX452 -> T489,\nT114 -> zero(T489),\nX453 -> T490,\nT115 -> one(T490),\nX454 -> T488,\nT113 -> one(T488),\nT486 -> T489,\nT487 -> T490", fontsize=14, style = filled, fillcolor = lightblue];
450 -> 750 [arrowhead = none ];
750 -> 452;

751 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
450 -> 751 [arrowhead = none ];
751 -> 454;

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

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

754 [label="INSTANCE with matching:\nT174 -> T489\nT175 -> T490\nT173 -> T488", fontsize=14, style = filled, fillcolor = lightgrey];
452 -> 754 [arrowhead = none , style=dashed];
754 -> 229[style=dashed];

755 [label="EVAL with clause\naddz(one(X468), zero(X469), one(X470)) :- addy(X468, X469, X470).\nand substitutionX468 -> T507,\nT114 -> one(T507),\nX469 -> T508,\nT115 -> zero(T508),\nX470 -> T506,\nT113 -> one(T506),\nT504 -> T507,\nT505 -> T508", fontsize=14, style = filled, fillcolor = lightblue];
466 -> 755 [arrowhead = none ];
755 -> 470;

756 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
466 -> 756 [arrowhead = none ];
756 -> 471;

757 [label="EVAL with clause\naddz(one(X478), one(X479), zero(X480)) :- addc(X478, X479, X480).\nand substitutionX478 -> T519,\nT114 -> one(T519),\nX479 -> T520,\nT115 -> one(T520),\nX480 -> T518,\nT113 -> zero(T518),\nT516 -> T519,\nT517 -> T520", fontsize=14, style = filled, fillcolor = lightblue];
467 -> 757 [arrowhead = none ];
757 -> 474;

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

759 [label="INSTANCE with matching:\nT222 -> T507\nT223 -> T508\nT221 -> T506", fontsize=14, style = filled, fillcolor = lightgrey];
470 -> 759 [arrowhead = none , style=dashed];
759 -> 275[style=dashed];

760 [label="INSTANCE with matching:\nT264 -> T519\nT265 -> T520\nT263 -> T518", fontsize=14, style = filled, fillcolor = lightgrey];
474 -> 760 [arrowhead = none , style=dashed];
760 -> 302[style=dashed];

761 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
476 -> 761 [arrowhead = none ];
761 -> 478;

762 [label="ONLY EVAL with clause\nadd(X512, X513, X514) :- addz(X512, X513, X514).\nand substitutionT1 -> T559,\nX512 -> T559,\nT2 -> T560,\nX513 -> T560,\nT3 -> T558,\nX514 -> T558,\nT556 -> T559,\nT557 -> T560", fontsize=14, style = filled, fillcolor = lightblue];
477 -> 762 [arrowhead = none ];
762 -> 493;

763 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
478 -> 763 [arrowhead = none ];
763 -> 479;

764 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
478 -> 764 [arrowhead = none ];
764 -> 480;

765 [label="EVAL with clause\nbinaryZ(zero(X487)) :- binaryZ(X487).\nand substitutionX487 -> T527,\nT522 -> zero(T527)", fontsize=14, style = filled, fillcolor = lightblue];
479 -> 765 [arrowhead = none ];
765 -> 483;

766 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
479 -> 766 [arrowhead = none ];
766 -> 484;

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

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

769 [label="INSTANCE with matching:\nT69 -> T527", fontsize=14, style = filled, fillcolor = lightgrey];
483 -> 769 [arrowhead = none , style=dashed];
769 -> 116[style=dashed];

770 [label="EVAL with clause\nbinaryZ(one(X493)) :- binary(X493).\nand substitutionX493 -> T533,\nT522 -> one(T533)", 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="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
486 -> 772 [arrowhead = none ];
772 -> 489;

773 [label="INSTANCE with matching:\nT79 -> T533", fontsize=14, style = filled, fillcolor = lightgrey];
487 -> 773 [arrowhead = none , style=dashed];
773 -> 126[style=dashed];

774 [label="ONLY EVAL with clause\nadd(X503, X504, X505) :- addz(X503, X504, X505).\nand substitutionT1 -> T548,\nX503 -> T548,\nT2 -> T549,\nX504 -> T549,\nT522 -> T547,\nX505 -> T547,\nT545 -> T548,\nT546 -> T549", fontsize=14, style = filled, fillcolor = lightblue];
489 -> 774 [arrowhead = none ];
774 -> 492;

775 [label="INSTANCE with matching:\nT114 -> T548\nT115 -> T549\nT113 -> T547", fontsize=14, style = filled, fillcolor = lightgrey];
492 -> 775 [arrowhead = none , style=dashed];
775 -> 179[style=dashed];

776 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
493 -> 776 [arrowhead = none ];
776 -> 494;

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

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

779 [label="EVAL with clause\naddz(zero(X527), zero(X528), zero(X529)) :- addz(X527, X528, X529).\nand substitutionX527 -> T576,\nT559 -> zero(T576),\nX528 -> T577,\nT560 -> zero(T577),\nX529 -> T575,\nT558 -> zero(T575),\nT573 -> T576,\nT574 -> T577", fontsize=14, style = filled, fillcolor = lightblue];
497 -> 779 [arrowhead = none ];
779 -> 499;

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

781 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
498 -> 781 [arrowhead = none ];
781 -> 503;

782 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
498 -> 782 [arrowhead = none ];
782 -> 504;

783 [label="INSTANCE with matching:\nT134 -> T576\nT135 -> T577\nT133 -> T575", fontsize=14, style = filled, fillcolor = lightgrey];
499 -> 783 [arrowhead = none , style=dashed];
783 -> 189[style=dashed];

784 [label="EVAL with clause\naddz(zero(X545), one(X546), one(X547)) :- addx(X545, X546, X547).\nand substitutionX545 -> T596,\nT559 -> zero(T596),\nX546 -> T597,\nT560 -> one(T597),\nX547 -> T595,\nT558 -> one(T595),\nT593 -> T596,\nT594 -> T597", fontsize=14, style = filled, fillcolor = lightblue];
503 -> 784 [arrowhead = none ];
784 -> 521;

785 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
503 -> 785 [arrowhead = none ];
785 -> 522;

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

787 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
504 -> 787 [arrowhead = none ];
787 -> 533;

788 [label="INSTANCE with matching:\nT174 -> T596\nT175 -> T597\nT173 -> T595", fontsize=14, style = filled, fillcolor = lightgrey];
521 -> 788 [arrowhead = none , style=dashed];
788 -> 229[style=dashed];

789 [label="EVAL with clause\naddz(one(X561), zero(X562), one(X563)) :- addy(X561, X562, X563).\nand substitutionX561 -> T614,\nT559 -> one(T614),\nX562 -> T615,\nT560 -> zero(T615),\nX563 -> T613,\nT558 -> one(T613),\nT611 -> T614,\nT612 -> T615", fontsize=14, style = filled, fillcolor = lightblue];
532 -> 789 [arrowhead = none ];
789 -> 536;

790 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
532 -> 790 [arrowhead = none ];
790 -> 537;

791 [label="EVAL with clause\naddz(one(X571), one(X572), zero(X573)) :- addc(X571, X572, X573).\nand substitutionX571 -> T626,\nT559 -> one(T626),\nX572 -> T627,\nT560 -> one(T627),\nX573 -> T625,\nT558 -> zero(T625),\nT623 -> T626,\nT624 -> T627", fontsize=14, style = filled, fillcolor = lightblue];
533 -> 791 [arrowhead = none ];
791 -> 538;

792 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
533 -> 792 [arrowhead = none ];
792 -> 539;

793 [label="INSTANCE with matching:\nT222 -> T614\nT223 -> T615\nT221 -> T613", fontsize=14, style = filled, fillcolor = lightgrey];
536 -> 793 [arrowhead = none , style=dashed];
793 -> 275[style=dashed];

794 [label="INSTANCE with matching:\nT264 -> T626\nT265 -> T627\nT263 -> T625", fontsize=14, style = filled, fillcolor = lightgrey];
538 -> 794 [arrowhead = none , style=dashed];
794 -> 302[style=dashed];

}

(2) Obligation:

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

addA_in_aag(b, b, b) → addA_out_aag(b, b, b)
addA_in_aag(zero(T69), b, zero(T69)) → U1_aag(T69, binaryZC_in_g(T69))
binaryZC_in_g(zero(T75)) → U12_g(T75, binaryZC_in_g(T75))
binaryZC_in_g(one(T79)) → U13_g(T79, binaryD_in_g(T79))
binaryD_in_g(b) → binaryD_out_g(b)
binaryD_in_g(zero(T84)) → U14_g(T84, binaryZC_in_g(T84))
U14_g(T84, binaryZC_out_g(T84)) → binaryD_out_g(zero(T84))
binaryD_in_g(one(T88)) → U15_g(T88, binaryD_in_g(T88))
U15_g(T88, binaryD_out_g(T88)) → binaryD_out_g(one(T88))
U13_g(T79, binaryD_out_g(T79)) → binaryZC_out_g(one(T79))
U12_g(T75, binaryZC_out_g(T75)) → binaryZC_out_g(zero(T75))
U1_aag(T69, binaryZC_out_g(T69)) → addA_out_aag(zero(T69), b, zero(T69))
addA_in_aag(one(T93), b, one(T93)) → U2_aag(T93, binaryD_in_g(T93))
U2_aag(T93, binaryD_out_g(T93)) → addA_out_aag(one(T93), b, one(T93))
addA_in_aag(b, T98, T98) → U3_aag(T98, binaryZC_in_g(T98))
U3_aag(T98, binaryZC_out_g(T98)) → addA_out_aag(b, T98, T98)
addA_in_aag(T114, T115, T113) → U4_aag(T114, T115, T113, addzE_in_aag(T114, T115, T113))
addzE_in_aag(zero(T134), zero(T135), zero(T133)) → U41_aag(T134, T135, T133, addzF_in_aag(T134, T135, T133))
addzF_in_aag(zero(T154), zero(T155), zero(T153)) → U16_aag(T154, T155, T153, addzF_in_aag(T154, T155, T153))
addzF_in_aag(zero(T174), one(T175), one(T173)) → U17_aag(T174, T175, T173, addxG_in_aag(T174, T175, T173))
addxG_in_aag(one(T181), b, one(T181)) → U35_aag(T181, binaryD_in_g(T181))
U35_aag(T181, binaryD_out_g(T181)) → addxG_out_aag(one(T181), b, one(T181))
addxG_in_aag(zero(T186), b, zero(T186)) → U36_aag(T186, binaryZC_in_g(T186))
U36_aag(T186, binaryZC_out_g(T186)) → addxG_out_aag(zero(T186), b, zero(T186))
addxG_in_aag(T202, T203, T201) → U37_aag(T202, T203, T201, addzF_in_aag(T202, T203, T201))
addzF_in_aag(one(T222), zero(T223), one(T221)) → U18_aag(T222, T223, T221, addyH_in_aag(T222, T223, T221))
addyH_in_aag(b, one(T229), one(T229)) → U38_aag(T229, binaryD_in_g(T229))
U38_aag(T229, binaryD_out_g(T229)) → addyH_out_aag(b, one(T229), one(T229))
addyH_in_aag(b, zero(T234), zero(T234)) → U39_aag(T234, binaryZC_in_g(T234))
U39_aag(T234, binaryZC_out_g(T234)) → addyH_out_aag(b, zero(T234), zero(T234))
addyH_in_aag(T250, T251, T249) → U40_aag(T250, T251, T249, addzF_in_aag(T250, T251, T249))
addzF_in_aag(one(T264), one(T265), zero(T263)) → U19_aag(T264, T265, T263, addcI_in_aag(T264, T265, T263))
addcI_in_aag(b, b, one(b)) → addcI_out_aag(b, b, one(b))
addcI_in_aag(T276, b, T275) → U32_aag(T276, T275, succZK_in_ag(T276, T275))
succZK_in_ag(zero(T282), one(T282)) → U22_ag(T282, binaryZC_in_g(T282))
U22_ag(T282, binaryZC_out_g(T282)) → succZK_out_ag(zero(T282), one(T282))
succZK_in_ag(one(T290), zero(T289)) → U23_ag(T290, T289, succJ_in_ag(T290, T289))
succJ_in_ag(b, one(b)) → succJ_out_ag(b, one(b))
succJ_in_ag(zero(T295), one(T295)) → U20_ag(T295, binaryZC_in_g(T295))
U20_ag(T295, binaryZC_out_g(T295)) → succJ_out_ag(zero(T295), one(T295))
succJ_in_ag(one(T303), zero(T302)) → U21_ag(T303, T302, succJ_in_ag(T303, T302))
U21_ag(T303, T302, succJ_out_ag(T303, T302)) → succJ_out_ag(one(T303), zero(T302))
U23_ag(T290, T289, succJ_out_ag(T290, T289)) → succZK_out_ag(one(T290), zero(T289))
U32_aag(T276, T275, succZK_out_ag(T276, T275)) → addcI_out_aag(T276, b, T275)
addcI_in_aag(b, T314, T313) → U33_aag(T314, T313, succZK_in_ag(T314, T313))
U33_aag(T314, T313, succZK_out_ag(T314, T313)) → addcI_out_aag(b, T314, T313)
addcI_in_aag(T330, T331, T329) → U34_aag(T330, T331, T329, addCL_in_aag(T330, T331, T329))
addCL_in_aag(zero(T350), zero(T351), one(T349)) → U24_aag(T350, T351, T349, addzF_in_aag(T350, T351, T349))
U24_aag(T350, T351, T349, addzF_out_aag(T350, T351, T349)) → addCL_out_aag(zero(T350), zero(T351), one(T349))
addCL_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U25_aag(T377, binaryZC_in_g(T377))
U25_aag(T377, binaryZC_out_g(T377)) → addCL_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCL_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U26_aag(T389, T388, succJ_in_ag(T389, T388))
U26_aag(T389, T388, succJ_out_ag(T389, T388)) → addCL_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCL_in_aag(zero(T404), one(T405), zero(T403)) → U27_aag(T404, T405, T403, addCL_in_aag(T404, T405, T403))
addCL_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U28_aag(T431, binaryZC_in_g(T431))
U28_aag(T431, binaryZC_out_g(T431)) → addCL_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCL_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U29_aag(T443, T442, succJ_in_ag(T443, T442))
U29_aag(T443, T442, succJ_out_ag(T443, T442)) → addCL_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCL_in_aag(one(T458), zero(T459), zero(T457)) → U30_aag(T458, T459, T457, addCL_in_aag(T458, T459, T457))
addCL_in_aag(one(T472), one(T473), one(T471)) → U31_aag(T472, T473, T471, addcI_in_aag(T472, T473, T471))
U31_aag(T472, T473, T471, addcI_out_aag(T472, T473, T471)) → addCL_out_aag(one(T472), one(T473), one(T471))
U30_aag(T458, T459, T457, addCL_out_aag(T458, T459, T457)) → addCL_out_aag(one(T458), zero(T459), zero(T457))
U27_aag(T404, T405, T403, addCL_out_aag(T404, T405, T403)) → addCL_out_aag(zero(T404), one(T405), zero(T403))
U34_aag(T330, T331, T329, addCL_out_aag(T330, T331, T329)) → addcI_out_aag(T330, T331, T329)
U19_aag(T264, T265, T263, addcI_out_aag(T264, T265, T263)) → addzF_out_aag(one(T264), one(T265), zero(T263))
U40_aag(T250, T251, T249, addzF_out_aag(T250, T251, T249)) → addyH_out_aag(T250, T251, T249)
U18_aag(T222, T223, T221, addyH_out_aag(T222, T223, T221)) → addzF_out_aag(one(T222), zero(T223), one(T221))
U37_aag(T202, T203, T201, addzF_out_aag(T202, T203, T201)) → addxG_out_aag(T202, T203, T201)
U17_aag(T174, T175, T173, addxG_out_aag(T174, T175, T173)) → addzF_out_aag(zero(T174), one(T175), one(T173))
U16_aag(T154, T155, T153, addzF_out_aag(T154, T155, T153)) → addzF_out_aag(zero(T154), zero(T155), zero(T153))
U41_aag(T134, T135, T133, addzF_out_aag(T134, T135, T133)) → addzE_out_aag(zero(T134), zero(T135), zero(T133))
addzE_in_aag(zero(T489), one(T490), one(T488)) → U42_aag(T489, T490, T488, addxG_in_aag(T489, T490, T488))
U42_aag(T489, T490, T488, addxG_out_aag(T489, T490, T488)) → addzE_out_aag(zero(T489), one(T490), one(T488))
addzE_in_aag(one(T507), zero(T508), one(T506)) → U43_aag(T507, T508, T506, addyH_in_aag(T507, T508, T506))
U43_aag(T507, T508, T506, addyH_out_aag(T507, T508, T506)) → addzE_out_aag(one(T507), zero(T508), one(T506))
addzE_in_aag(one(T519), one(T520), zero(T518)) → U44_aag(T519, T520, T518, addcI_in_aag(T519, T520, T518))
U44_aag(T519, T520, T518, addcI_out_aag(T519, T520, T518)) → addzE_out_aag(one(T519), one(T520), zero(T518))
U4_aag(T114, T115, T113, addzE_out_aag(T114, T115, T113)) → addA_out_aag(T114, T115, T113)
addA_in_aag(b, zero(T527), zero(T527)) → U5_aag(T527, binaryZC_in_g(T527))
U5_aag(T527, binaryZC_out_g(T527)) → addA_out_aag(b, zero(T527), zero(T527))
addA_in_aag(b, one(T533), one(T533)) → U6_aag(T533, binaryD_in_g(T533))
U6_aag(T533, binaryD_out_g(T533)) → addA_out_aag(b, one(T533), one(T533))
addA_in_aag(T548, T549, T547) → U7_aag(T548, T549, T547, addzE_in_aag(T548, T549, T547))
U7_aag(T548, T549, T547, addzE_out_aag(T548, T549, T547)) → addA_out_aag(T548, T549, T547)
addA_in_aag(zero(T576), zero(T577), zero(T575)) → U8_aag(T576, T577, T575, addzF_in_aag(T576, T577, T575))
U8_aag(T576, T577, T575, addzF_out_aag(T576, T577, T575)) → addA_out_aag(zero(T576), zero(T577), zero(T575))
addA_in_aag(zero(T596), one(T597), one(T595)) → U9_aag(T596, T597, T595, addxG_in_aag(T596, T597, T595))
U9_aag(T596, T597, T595, addxG_out_aag(T596, T597, T595)) → addA_out_aag(zero(T596), one(T597), one(T595))
addA_in_aag(one(T614), zero(T615), one(T613)) → U10_aag(T614, T615, T613, addyH_in_aag(T614, T615, T613))
U10_aag(T614, T615, T613, addyH_out_aag(T614, T615, T613)) → addA_out_aag(one(T614), zero(T615), one(T613))
addA_in_aag(one(T626), one(T627), zero(T625)) → U11_aag(T626, T627, T625, addcI_in_aag(T626, T627, T625))
U11_aag(T626, T627, T625, addcI_out_aag(T626, T627, T625)) → addA_out_aag(one(T626), one(T627), zero(T625))

(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_AAG(zero(T69), b, zero(T69)) → U1_AAG(T69, binaryZC_in_g(T69))
ADDA_IN_AAG(zero(T69), b, zero(T69)) → BINARYZC_IN_G(T69)
BINARYZC_IN_G(zero(T75)) → U12_G(T75, binaryZC_in_g(T75))
BINARYZC_IN_G(zero(T75)) → BINARYZC_IN_G(T75)
BINARYZC_IN_G(one(T79)) → U13_G(T79, binaryD_in_g(T79))
BINARYZC_IN_G(one(T79)) → BINARYD_IN_G(T79)
BINARYD_IN_G(zero(T84)) → U14_G(T84, binaryZC_in_g(T84))
BINARYD_IN_G(zero(T84)) → BINARYZC_IN_G(T84)
BINARYD_IN_G(one(T88)) → U15_G(T88, binaryD_in_g(T88))
BINARYD_IN_G(one(T88)) → BINARYD_IN_G(T88)
ADDA_IN_AAG(one(T93), b, one(T93)) → U2_AAG(T93, binaryD_in_g(T93))
ADDA_IN_AAG(one(T93), b, one(T93)) → BINARYD_IN_G(T93)
ADDA_IN_AAG(b, T98, T98) → U3_AAG(T98, binaryZC_in_g(T98))
ADDA_IN_AAG(b, T98, T98) → BINARYZC_IN_G(T98)
ADDA_IN_AAG(T114, T115, T113) → U4_AAG(T114, T115, T113, addzE_in_aag(T114, T115, T113))
ADDA_IN_AAG(T114, T115, T113) → ADDZE_IN_AAG(T114, T115, T113)
ADDZE_IN_AAG(zero(T134), zero(T135), zero(T133)) → U41_AAG(T134, T135, T133, addzF_in_aag(T134, T135, T133))
ADDZE_IN_AAG(zero(T134), zero(T135), zero(T133)) → ADDZF_IN_AAG(T134, T135, T133)
ADDZF_IN_AAG(zero(T154), zero(T155), zero(T153)) → U16_AAG(T154, T155, T153, addzF_in_aag(T154, T155, T153))
ADDZF_IN_AAG(zero(T154), zero(T155), zero(T153)) → ADDZF_IN_AAG(T154, T155, T153)
ADDZF_IN_AAG(zero(T174), one(T175), one(T173)) → U17_AAG(T174, T175, T173, addxG_in_aag(T174, T175, T173))
ADDZF_IN_AAG(zero(T174), one(T175), one(T173)) → ADDXG_IN_AAG(T174, T175, T173)
ADDXG_IN_AAG(one(T181), b, one(T181)) → U35_AAG(T181, binaryD_in_g(T181))
ADDXG_IN_AAG(one(T181), b, one(T181)) → BINARYD_IN_G(T181)
ADDXG_IN_AAG(zero(T186), b, zero(T186)) → U36_AAG(T186, binaryZC_in_g(T186))
ADDXG_IN_AAG(zero(T186), b, zero(T186)) → BINARYZC_IN_G(T186)
ADDXG_IN_AAG(T202, T203, T201) → U37_AAG(T202, T203, T201, addzF_in_aag(T202, T203, T201))
ADDXG_IN_AAG(T202, T203, T201) → ADDZF_IN_AAG(T202, T203, T201)
ADDZF_IN_AAG(one(T222), zero(T223), one(T221)) → U18_AAG(T222, T223, T221, addyH_in_aag(T222, T223, T221))
ADDZF_IN_AAG(one(T222), zero(T223), one(T221)) → ADDYH_IN_AAG(T222, T223, T221)
ADDYH_IN_AAG(b, one(T229), one(T229)) → U38_AAG(T229, binaryD_in_g(T229))
ADDYH_IN_AAG(b, one(T229), one(T229)) → BINARYD_IN_G(T229)
ADDYH_IN_AAG(b, zero(T234), zero(T234)) → U39_AAG(T234, binaryZC_in_g(T234))
ADDYH_IN_AAG(b, zero(T234), zero(T234)) → BINARYZC_IN_G(T234)
ADDYH_IN_AAG(T250, T251, T249) → U40_AAG(T250, T251, T249, addzF_in_aag(T250, T251, T249))
ADDYH_IN_AAG(T250, T251, T249) → ADDZF_IN_AAG(T250, T251, T249)
ADDZF_IN_AAG(one(T264), one(T265), zero(T263)) → U19_AAG(T264, T265, T263, addcI_in_aag(T264, T265, T263))
ADDZF_IN_AAG(one(T264), one(T265), zero(T263)) → ADDCI_IN_AAG(T264, T265, T263)
ADDCI_IN_AAG(T276, b, T275) → U32_AAG(T276, T275, succZK_in_ag(T276, T275))
ADDCI_IN_AAG(T276, b, T275) → SUCCZK_IN_AG(T276, T275)
SUCCZK_IN_AG(zero(T282), one(T282)) → U22_AG(T282, binaryZC_in_g(T282))
SUCCZK_IN_AG(zero(T282), one(T282)) → BINARYZC_IN_G(T282)
SUCCZK_IN_AG(one(T290), zero(T289)) → U23_AG(T290, T289, succJ_in_ag(T290, T289))
SUCCZK_IN_AG(one(T290), zero(T289)) → SUCCJ_IN_AG(T290, T289)
SUCCJ_IN_AG(zero(T295), one(T295)) → U20_AG(T295, binaryZC_in_g(T295))
SUCCJ_IN_AG(zero(T295), one(T295)) → BINARYZC_IN_G(T295)
SUCCJ_IN_AG(one(T303), zero(T302)) → U21_AG(T303, T302, succJ_in_ag(T303, T302))
SUCCJ_IN_AG(one(T303), zero(T302)) → SUCCJ_IN_AG(T303, T302)
ADDCI_IN_AAG(b, T314, T313) → U33_AAG(T314, T313, succZK_in_ag(T314, T313))
ADDCI_IN_AAG(b, T314, T313) → SUCCZK_IN_AG(T314, T313)
ADDCI_IN_AAG(T330, T331, T329) → U34_AAG(T330, T331, T329, addCL_in_aag(T330, T331, T329))
ADDCI_IN_AAG(T330, T331, T329) → ADDCL_IN_AAG(T330, T331, T329)
ADDCL_IN_AAG(zero(T350), zero(T351), one(T349)) → U24_AAG(T350, T351, T349, addzF_in_aag(T350, T351, T349))
ADDCL_IN_AAG(zero(T350), zero(T351), one(T349)) → ADDZF_IN_AAG(T350, T351, T349)
ADDCL_IN_AAG(zero(zero(T377)), one(b), zero(one(T377))) → U25_AAG(T377, binaryZC_in_g(T377))
ADDCL_IN_AAG(zero(zero(T377)), one(b), zero(one(T377))) → BINARYZC_IN_G(T377)
ADDCL_IN_AAG(zero(one(T389)), one(b), zero(zero(T388))) → U26_AAG(T389, T388, succJ_in_ag(T389, T388))
ADDCL_IN_AAG(zero(one(T389)), one(b), zero(zero(T388))) → SUCCJ_IN_AG(T389, T388)
ADDCL_IN_AAG(zero(T404), one(T405), zero(T403)) → U27_AAG(T404, T405, T403, addCL_in_aag(T404, T405, T403))
ADDCL_IN_AAG(zero(T404), one(T405), zero(T403)) → ADDCL_IN_AAG(T404, T405, T403)
ADDCL_IN_AAG(one(b), zero(zero(T431)), zero(one(T431))) → U28_AAG(T431, binaryZC_in_g(T431))
ADDCL_IN_AAG(one(b), zero(zero(T431)), zero(one(T431))) → BINARYZC_IN_G(T431)
ADDCL_IN_AAG(one(b), zero(one(T443)), zero(zero(T442))) → U29_AAG(T443, T442, succJ_in_ag(T443, T442))
ADDCL_IN_AAG(one(b), zero(one(T443)), zero(zero(T442))) → SUCCJ_IN_AG(T443, T442)
ADDCL_IN_AAG(one(T458), zero(T459), zero(T457)) → U30_AAG(T458, T459, T457, addCL_in_aag(T458, T459, T457))
ADDCL_IN_AAG(one(T458), zero(T459), zero(T457)) → ADDCL_IN_AAG(T458, T459, T457)
ADDCL_IN_AAG(one(T472), one(T473), one(T471)) → U31_AAG(T472, T473, T471, addcI_in_aag(T472, T473, T471))
ADDCL_IN_AAG(one(T472), one(T473), one(T471)) → ADDCI_IN_AAG(T472, T473, T471)
ADDZE_IN_AAG(zero(T489), one(T490), one(T488)) → U42_AAG(T489, T490, T488, addxG_in_aag(T489, T490, T488))
ADDZE_IN_AAG(zero(T489), one(T490), one(T488)) → ADDXG_IN_AAG(T489, T490, T488)
ADDZE_IN_AAG(one(T507), zero(T508), one(T506)) → U43_AAG(T507, T508, T506, addyH_in_aag(T507, T508, T506))
ADDZE_IN_AAG(one(T507), zero(T508), one(T506)) → ADDYH_IN_AAG(T507, T508, T506)
ADDZE_IN_AAG(one(T519), one(T520), zero(T518)) → U44_AAG(T519, T520, T518, addcI_in_aag(T519, T520, T518))
ADDZE_IN_AAG(one(T519), one(T520), zero(T518)) → ADDCI_IN_AAG(T519, T520, T518)
ADDA_IN_AAG(b, zero(T527), zero(T527)) → U5_AAG(T527, binaryZC_in_g(T527))
ADDA_IN_AAG(b, zero(T527), zero(T527)) → BINARYZC_IN_G(T527)
ADDA_IN_AAG(b, one(T533), one(T533)) → U6_AAG(T533, binaryD_in_g(T533))
ADDA_IN_AAG(b, one(T533), one(T533)) → BINARYD_IN_G(T533)
ADDA_IN_AAG(T548, T549, T547) → U7_AAG(T548, T549, T547, addzE_in_aag(T548, T549, T547))
ADDA_IN_AAG(zero(T576), zero(T577), zero(T575)) → U8_AAG(T576, T577, T575, addzF_in_aag(T576, T577, T575))
ADDA_IN_AAG(zero(T576), zero(T577), zero(T575)) → ADDZF_IN_AAG(T576, T577, T575)
ADDA_IN_AAG(zero(T596), one(T597), one(T595)) → U9_AAG(T596, T597, T595, addxG_in_aag(T596, T597, T595))
ADDA_IN_AAG(zero(T596), one(T597), one(T595)) → ADDXG_IN_AAG(T596, T597, T595)
ADDA_IN_AAG(one(T614), zero(T615), one(T613)) → U10_AAG(T614, T615, T613, addyH_in_aag(T614, T615, T613))
ADDA_IN_AAG(one(T614), zero(T615), one(T613)) → ADDYH_IN_AAG(T614, T615, T613)
ADDA_IN_AAG(one(T626), one(T627), zero(T625)) → U11_AAG(T626, T627, T625, addcI_in_aag(T626, T627, T625))
ADDA_IN_AAG(one(T626), one(T627), zero(T625)) → ADDCI_IN_AAG(T626, T627, T625)

The TRS R consists of the following rules:

addA_in_aag(b, b, b) → addA_out_aag(b, b, b)
addA_in_aag(zero(T69), b, zero(T69)) → U1_aag(T69, binaryZC_in_g(T69))
binaryZC_in_g(zero(T75)) → U12_g(T75, binaryZC_in_g(T75))
binaryZC_in_g(one(T79)) → U13_g(T79, binaryD_in_g(T79))
binaryD_in_g(b) → binaryD_out_g(b)
binaryD_in_g(zero(T84)) → U14_g(T84, binaryZC_in_g(T84))
U14_g(T84, binaryZC_out_g(T84)) → binaryD_out_g(zero(T84))
binaryD_in_g(one(T88)) → U15_g(T88, binaryD_in_g(T88))
U15_g(T88, binaryD_out_g(T88)) → binaryD_out_g(one(T88))
U13_g(T79, binaryD_out_g(T79)) → binaryZC_out_g(one(T79))
U12_g(T75, binaryZC_out_g(T75)) → binaryZC_out_g(zero(T75))
U1_aag(T69, binaryZC_out_g(T69)) → addA_out_aag(zero(T69), b, zero(T69))
addA_in_aag(one(T93), b, one(T93)) → U2_aag(T93, binaryD_in_g(T93))
U2_aag(T93, binaryD_out_g(T93)) → addA_out_aag(one(T93), b, one(T93))
addA_in_aag(b, T98, T98) → U3_aag(T98, binaryZC_in_g(T98))
U3_aag(T98, binaryZC_out_g(T98)) → addA_out_aag(b, T98, T98)
addA_in_aag(T114, T115, T113) → U4_aag(T114, T115, T113, addzE_in_aag(T114, T115, T113))
addzE_in_aag(zero(T134), zero(T135), zero(T133)) → U41_aag(T134, T135, T133, addzF_in_aag(T134, T135, T133))
addzF_in_aag(zero(T154), zero(T155), zero(T153)) → U16_aag(T154, T155, T153, addzF_in_aag(T154, T155, T153))
addzF_in_aag(zero(T174), one(T175), one(T173)) → U17_aag(T174, T175, T173, addxG_in_aag(T174, T175, T173))
addxG_in_aag(one(T181), b, one(T181)) → U35_aag(T181, binaryD_in_g(T181))
U35_aag(T181, binaryD_out_g(T181)) → addxG_out_aag(one(T181), b, one(T181))
addxG_in_aag(zero(T186), b, zero(T186)) → U36_aag(T186, binaryZC_in_g(T186))
U36_aag(T186, binaryZC_out_g(T186)) → addxG_out_aag(zero(T186), b, zero(T186))
addxG_in_aag(T202, T203, T201) → U37_aag(T202, T203, T201, addzF_in_aag(T202, T203, T201))
addzF_in_aag(one(T222), zero(T223), one(T221)) → U18_aag(T222, T223, T221, addyH_in_aag(T222, T223, T221))
addyH_in_aag(b, one(T229), one(T229)) → U38_aag(T229, binaryD_in_g(T229))
U38_aag(T229, binaryD_out_g(T229)) → addyH_out_aag(b, one(T229), one(T229))
addyH_in_aag(b, zero(T234), zero(T234)) → U39_aag(T234, binaryZC_in_g(T234))
U39_aag(T234, binaryZC_out_g(T234)) → addyH_out_aag(b, zero(T234), zero(T234))
addyH_in_aag(T250, T251, T249) → U40_aag(T250, T251, T249, addzF_in_aag(T250, T251, T249))
addzF_in_aag(one(T264), one(T265), zero(T263)) → U19_aag(T264, T265, T263, addcI_in_aag(T264, T265, T263))
addcI_in_aag(b, b, one(b)) → addcI_out_aag(b, b, one(b))
addcI_in_aag(T276, b, T275) → U32_aag(T276, T275, succZK_in_ag(T276, T275))
succZK_in_ag(zero(T282), one(T282)) → U22_ag(T282, binaryZC_in_g(T282))
U22_ag(T282, binaryZC_out_g(T282)) → succZK_out_ag(zero(T282), one(T282))
succZK_in_ag(one(T290), zero(T289)) → U23_ag(T290, T289, succJ_in_ag(T290, T289))
succJ_in_ag(b, one(b)) → succJ_out_ag(b, one(b))
succJ_in_ag(zero(T295), one(T295)) → U20_ag(T295, binaryZC_in_g(T295))
U20_ag(T295, binaryZC_out_g(T295)) → succJ_out_ag(zero(T295), one(T295))
succJ_in_ag(one(T303), zero(T302)) → U21_ag(T303, T302, succJ_in_ag(T303, T302))
U21_ag(T303, T302, succJ_out_ag(T303, T302)) → succJ_out_ag(one(T303), zero(T302))
U23_ag(T290, T289, succJ_out_ag(T290, T289)) → succZK_out_ag(one(T290), zero(T289))
U32_aag(T276, T275, succZK_out_ag(T276, T275)) → addcI_out_aag(T276, b, T275)
addcI_in_aag(b, T314, T313) → U33_aag(T314, T313, succZK_in_ag(T314, T313))
U33_aag(T314, T313, succZK_out_ag(T314, T313)) → addcI_out_aag(b, T314, T313)
addcI_in_aag(T330, T331, T329) → U34_aag(T330, T331, T329, addCL_in_aag(T330, T331, T329))
addCL_in_aag(zero(T350), zero(T351), one(T349)) → U24_aag(T350, T351, T349, addzF_in_aag(T350, T351, T349))
U24_aag(T350, T351, T349, addzF_out_aag(T350, T351, T349)) → addCL_out_aag(zero(T350), zero(T351), one(T349))
addCL_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U25_aag(T377, binaryZC_in_g(T377))
U25_aag(T377, binaryZC_out_g(T377)) → addCL_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCL_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U26_aag(T389, T388, succJ_in_ag(T389, T388))
U26_aag(T389, T388, succJ_out_ag(T389, T388)) → addCL_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCL_in_aag(zero(T404), one(T405), zero(T403)) → U27_aag(T404, T405, T403, addCL_in_aag(T404, T405, T403))
addCL_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U28_aag(T431, binaryZC_in_g(T431))
U28_aag(T431, binaryZC_out_g(T431)) → addCL_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCL_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U29_aag(T443, T442, succJ_in_ag(T443, T442))
U29_aag(T443, T442, succJ_out_ag(T443, T442)) → addCL_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCL_in_aag(one(T458), zero(T459), zero(T457)) → U30_aag(T458, T459, T457, addCL_in_aag(T458, T459, T457))
addCL_in_aag(one(T472), one(T473), one(T471)) → U31_aag(T472, T473, T471, addcI_in_aag(T472, T473, T471))
U31_aag(T472, T473, T471, addcI_out_aag(T472, T473, T471)) → addCL_out_aag(one(T472), one(T473), one(T471))
U30_aag(T458, T459, T457, addCL_out_aag(T458, T459, T457)) → addCL_out_aag(one(T458), zero(T459), zero(T457))
U27_aag(T404, T405, T403, addCL_out_aag(T404, T405, T403)) → addCL_out_aag(zero(T404), one(T405), zero(T403))
U34_aag(T330, T331, T329, addCL_out_aag(T330, T331, T329)) → addcI_out_aag(T330, T331, T329)
U19_aag(T264, T265, T263, addcI_out_aag(T264, T265, T263)) → addzF_out_aag(one(T264), one(T265), zero(T263))
U40_aag(T250, T251, T249, addzF_out_aag(T250, T251, T249)) → addyH_out_aag(T250, T251, T249)
U18_aag(T222, T223, T221, addyH_out_aag(T222, T223, T221)) → addzF_out_aag(one(T222), zero(T223), one(T221))
U37_aag(T202, T203, T201, addzF_out_aag(T202, T203, T201)) → addxG_out_aag(T202, T203, T201)
U17_aag(T174, T175, T173, addxG_out_aag(T174, T175, T173)) → addzF_out_aag(zero(T174), one(T175), one(T173))
U16_aag(T154, T155, T153, addzF_out_aag(T154, T155, T153)) → addzF_out_aag(zero(T154), zero(T155), zero(T153))
U41_aag(T134, T135, T133, addzF_out_aag(T134, T135, T133)) → addzE_out_aag(zero(T134), zero(T135), zero(T133))
addzE_in_aag(zero(T489), one(T490), one(T488)) → U42_aag(T489, T490, T488, addxG_in_aag(T489, T490, T488))
U42_aag(T489, T490, T488, addxG_out_aag(T489, T490, T488)) → addzE_out_aag(zero(T489), one(T490), one(T488))
addzE_in_aag(one(T507), zero(T508), one(T506)) → U43_aag(T507, T508, T506, addyH_in_aag(T507, T508, T506))
U43_aag(T507, T508, T506, addyH_out_aag(T507, T508, T506)) → addzE_out_aag(one(T507), zero(T508), one(T506))
addzE_in_aag(one(T519), one(T520), zero(T518)) → U44_aag(T519, T520, T518, addcI_in_aag(T519, T520, T518))
U44_aag(T519, T520, T518, addcI_out_aag(T519, T520, T518)) → addzE_out_aag(one(T519), one(T520), zero(T518))
U4_aag(T114, T115, T113, addzE_out_aag(T114, T115, T113)) → addA_out_aag(T114, T115, T113)
addA_in_aag(b, zero(T527), zero(T527)) → U5_aag(T527, binaryZC_in_g(T527))
U5_aag(T527, binaryZC_out_g(T527)) → addA_out_aag(b, zero(T527), zero(T527))
addA_in_aag(b, one(T533), one(T533)) → U6_aag(T533, binaryD_in_g(T533))
U6_aag(T533, binaryD_out_g(T533)) → addA_out_aag(b, one(T533), one(T533))
addA_in_aag(T548, T549, T547) → U7_aag(T548, T549, T547, addzE_in_aag(T548, T549, T547))
U7_aag(T548, T549, T547, addzE_out_aag(T548, T549, T547)) → addA_out_aag(T548, T549, T547)
addA_in_aag(zero(T576), zero(T577), zero(T575)) → U8_aag(T576, T577, T575, addzF_in_aag(T576, T577, T575))
U8_aag(T576, T577, T575, addzF_out_aag(T576, T577, T575)) → addA_out_aag(zero(T576), zero(T577), zero(T575))
addA_in_aag(zero(T596), one(T597), one(T595)) → U9_aag(T596, T597, T595, addxG_in_aag(T596, T597, T595))
U9_aag(T596, T597, T595, addxG_out_aag(T596, T597, T595)) → addA_out_aag(zero(T596), one(T597), one(T595))
addA_in_aag(one(T614), zero(T615), one(T613)) → U10_aag(T614, T615, T613, addyH_in_aag(T614, T615, T613))
U10_aag(T614, T615, T613, addyH_out_aag(T614, T615, T613)) → addA_out_aag(one(T614), zero(T615), one(T613))
addA_in_aag(one(T626), one(T627), zero(T625)) → U11_aag(T626, T627, T625, addcI_in_aag(T626, T627, T625))
U11_aag(T626, T627, T625, addcI_out_aag(T626, T627, T625)) → addA_out_aag(one(T626), one(T627), zero(T625))

The argument filtering Pi contains the following mapping:
addA_in_aag(x1, x2, x3) = addA_in_aag(x3)
b = b
addA_out_aag(x1, x2, x3) = addA_out_aag(x1, x2, x3)
zero(x1) = zero(x1)
U1_aag(x1, x2) = U1_aag(x1, x2)
binaryZC_in_g(x1) = binaryZC_in_g(x1)
U12_g(x1, x2) = U12_g(x1, x2)
one(x1) = one(x1)
U13_g(x1, x2) = U13_g(x1, x2)
binaryD_in_g(x1) = binaryD_in_g(x1)
binaryD_out_g(x1) = binaryD_out_g(x1)
U14_g(x1, x2) = U14_g(x1, x2)
binaryZC_out_g(x1) = binaryZC_out_g(x1)
U15_g(x1, x2) = U15_g(x1, x2)
U2_aag(x1, x2) = U2_aag(x1, x2)
U3_aag(x1, x2) = U3_aag(x1, x2)
U4_aag(x1, x2, x3, x4) = U4_aag(x3, x4)
addzE_in_aag(x1, x2, x3) = addzE_in_aag(x3)
U41_aag(x1, x2, x3, x4) = U41_aag(x3, x4)
addzF_in_aag(x1, x2, x3) = addzF_in_aag(x3)
U16_aag(x1, x2, x3, x4) = U16_aag(x3, x4)
U17_aag(x1, x2, x3, x4) = U17_aag(x3, x4)
addxG_in_aag(x1, x2, x3) = addxG_in_aag(x3)
U35_aag(x1, x2) = U35_aag(x1, x2)
addxG_out_aag(x1, x2, x3) = addxG_out_aag(x1, x2, x3)
U36_aag(x1, x2) = U36_aag(x1, x2)
U37_aag(x1, x2, x3, x4) = U37_aag(x3, x4)
U18_aag(x1, x2, x3, x4) = U18_aag(x3, x4)
addyH_in_aag(x1, x2, x3) = addyH_in_aag(x3)
U38_aag(x1, x2) = U38_aag(x1, x2)
addyH_out_aag(x1, x2, x3) = addyH_out_aag(x1, x2, x3)
U39_aag(x1, x2) = U39_aag(x1, x2)
U40_aag(x1, x2, x3, x4) = U40_aag(x3, x4)
U19_aag(x1, x2, x3, x4) = U19_aag(x3, x4)
addcI_in_aag(x1, x2, x3) = addcI_in_aag(x3)
addcI_out_aag(x1, x2, x3) = addcI_out_aag(x1, x2, x3)
U32_aag(x1, x2, x3) = U32_aag(x2, x3)
succZK_in_ag(x1, x2) = succZK_in_ag(x2)
U22_ag(x1, x2) = U22_ag(x1, x2)
succZK_out_ag(x1, x2) = succZK_out_ag(x1, x2)
U23_ag(x1, x2, x3) = U23_ag(x2, x3)
succJ_in_ag(x1, x2) = succJ_in_ag(x2)
succJ_out_ag(x1, x2) = succJ_out_ag(x1, x2)
U20_ag(x1, x2) = U20_ag(x1, x2)
U21_ag(x1, x2, x3) = U21_ag(x2, x3)
U33_aag(x1, x2, x3) = U33_aag(x2, x3)
U34_aag(x1, x2, x3, x4) = U34_aag(x3, x4)
addCL_in_aag(x1, x2, x3) = addCL_in_aag(x3)
U24_aag(x1, x2, x3, x4) = U24_aag(x3, x4)
addzF_out_aag(x1, x2, x3) = addzF_out_aag(x1, x2, x3)
addCL_out_aag(x1, x2, x3) = addCL_out_aag(x1, x2, x3)
U25_aag(x1, x2) = U25_aag(x1, x2)
U26_aag(x1, x2, x3) = U26_aag(x2, x3)
U27_aag(x1, x2, x3, x4) = U27_aag(x3, x4)
U28_aag(x1, x2) = U28_aag(x1, x2)
U29_aag(x1, x2, x3) = U29_aag(x2, x3)
U30_aag(x1, x2, x3, x4) = U30_aag(x3, x4)
U31_aag(x1, x2, x3, x4) = U31_aag(x3, x4)
addzE_out_aag(x1, x2, x3) = addzE_out_aag(x1, x2, x3)
U42_aag(x1, x2, x3, x4) = U42_aag(x3, x4)
U43_aag(x1, x2, x3, x4) = U43_aag(x3, x4)
U44_aag(x1, x2, x3, x4) = U44_aag(x3, x4)
U5_aag(x1, x2) = U5_aag(x1, x2)
U6_aag(x1, x2) = U6_aag(x1, x2)
U7_aag(x1, x2, x3, x4) = U7_aag(x3, x4)
U8_aag(x1, x2, x3, x4) = U8_aag(x3, x4)
U9_aag(x1, x2, x3, x4) = U9_aag(x3, x4)
U10_aag(x1, x2, x3, x4) = U10_aag(x3, x4)
U11_aag(x1, x2, x3, x4) = U11_aag(x3, x4)
ADDA_IN_AAG(x1, x2, x3) = ADDA_IN_AAG(x3)
U1_AAG(x1, x2) = U1_AAG(x1, x2)
BINARYZC_IN_G(x1) = BINARYZC_IN_G(x1)
U12_G(x1, x2) = U12_G(x1, x2)
U13_G(x1, x2) = U13_G(x1, x2)
BINARYD_IN_G(x1) = BINARYD_IN_G(x1)
U14_G(x1, x2) = U14_G(x1, x2)
U15_G(x1, x2) = U15_G(x1, x2)
U2_AAG(x1, x2) = U2_AAG(x1, x2)
U3_AAG(x1, x2) = U3_AAG(x1, x2)
U4_AAG(x1, x2, x3, x4) = U4_AAG(x3, x4)
ADDZE_IN_AAG(x1, x2, x3) = ADDZE_IN_AAG(x3)
U41_AAG(x1, x2, x3, x4) = U41_AAG(x3, x4)
ADDZF_IN_AAG(x1, x2, x3) = ADDZF_IN_AAG(x3)
U16_AAG(x1, x2, x3, x4) = U16_AAG(x3, x4)
U17_AAG(x1, x2, x3, x4) = U17_AAG(x3, x4)
ADDXG_IN_AAG(x1, x2, x3) = ADDXG_IN_AAG(x3)
U35_AAG(x1, x2) = U35_AAG(x1, x2)
U36_AAG(x1, x2) = U36_AAG(x1, x2)
U37_AAG(x1, x2, x3, x4) = U37_AAG(x3, x4)
U18_AAG(x1, x2, x3, x4) = U18_AAG(x3, x4)
ADDYH_IN_AAG(x1, x2, x3) = ADDYH_IN_AAG(x3)
U38_AAG(x1, x2) = U38_AAG(x1, x2)
U39_AAG(x1, x2) = U39_AAG(x1, x2)
U40_AAG(x1, x2, x3, x4) = U40_AAG(x3, x4)
U19_AAG(x1, x2, x3, x4) = U19_AAG(x3, x4)
ADDCI_IN_AAG(x1, x2, x3) = ADDCI_IN_AAG(x3)
U32_AAG(x1, x2, x3) = U32_AAG(x2, x3)
SUCCZK_IN_AG(x1, x2) = SUCCZK_IN_AG(x2)
U22_AG(x1, x2) = U22_AG(x1, x2)
U23_AG(x1, x2, x3) = U23_AG(x2, x3)
SUCCJ_IN_AG(x1, x2) = SUCCJ_IN_AG(x2)
U20_AG(x1, x2) = U20_AG(x1, x2)
U21_AG(x1, x2, x3) = U21_AG(x2, x3)
U33_AAG(x1, x2, x3) = U33_AAG(x2, x3)
U34_AAG(x1, x2, x3, x4) = U34_AAG(x3, x4)
ADDCL_IN_AAG(x1, x2, x3) = ADDCL_IN_AAG(x3)
U24_AAG(x1, x2, x3, x4) = U24_AAG(x3, x4)
U25_AAG(x1, x2) = U25_AAG(x1, x2)
U26_AAG(x1, x2, x3) = U26_AAG(x2, x3)
U27_AAG(x1, x2, x3, x4) = U27_AAG(x3, x4)
U28_AAG(x1, x2) = U28_AAG(x1, x2)
U29_AAG(x1, x2, x3) = U29_AAG(x2, x3)
U30_AAG(x1, x2, x3, x4) = U30_AAG(x3, x4)
U31_AAG(x1, x2, x3, x4) = U31_AAG(x3, x4)
U42_AAG(x1, x2, x3, x4) = U42_AAG(x3, x4)
U43_AAG(x1, x2, x3, x4) = U43_AAG(x3, x4)
U44_AAG(x1, x2, x3, x4) = U44_AAG(x3, x4)
U5_AAG(x1, x2) = U5_AAG(x1, x2)
U6_AAG(x1, x2) = U6_AAG(x1, x2)
U7_AAG(x1, x2, x3, x4) = U7_AAG(x3, x4)
U8_AAG(x1, x2, x3, x4) = U8_AAG(x3, x4)
U9_AAG(x1, x2, x3, x4) = U9_AAG(x3, x4)
U10_AAG(x1, x2, x3, x4) = U10_AAG(x3, x4)
U11_AAG(x1, x2, x3, x4) = U11_AAG(x3, 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_AAG(zero(T69), b, zero(T69)) → U1_AAG(T69, binaryZC_in_g(T69))
ADDA_IN_AAG(zero(T69), b, zero(T69)) → BINARYZC_IN_G(T69)
BINARYZC_IN_G(zero(T75)) → U12_G(T75, binaryZC_in_g(T75))
BINARYZC_IN_G(zero(T75)) → BINARYZC_IN_G(T75)
BINARYZC_IN_G(one(T79)) → U13_G(T79, binaryD_in_g(T79))
BINARYZC_IN_G(one(T79)) → BINARYD_IN_G(T79)
BINARYD_IN_G(zero(T84)) → U14_G(T84, binaryZC_in_g(T84))
BINARYD_IN_G(zero(T84)) → BINARYZC_IN_G(T84)
BINARYD_IN_G(one(T88)) → U15_G(T88, binaryD_in_g(T88))
BINARYD_IN_G(one(T88)) → BINARYD_IN_G(T88)
ADDA_IN_AAG(one(T93), b, one(T93)) → U2_AAG(T93, binaryD_in_g(T93))
ADDA_IN_AAG(one(T93), b, one(T93)) → BINARYD_IN_G(T93)
ADDA_IN_AAG(b, T98, T98) → U3_AAG(T98, binaryZC_in_g(T98))
ADDA_IN_AAG(b, T98, T98) → BINARYZC_IN_G(T98)
ADDA_IN_AAG(T114, T115, T113) → U4_AAG(T114, T115, T113, addzE_in_aag(T114, T115, T113))
ADDA_IN_AAG(T114, T115, T113) → ADDZE_IN_AAG(T114, T115, T113)
ADDZE_IN_AAG(zero(T134), zero(T135), zero(T133)) → U41_AAG(T134, T135, T133, addzF_in_aag(T134, T135, T133))
ADDZE_IN_AAG(zero(T134), zero(T135), zero(T133)) → ADDZF_IN_AAG(T134, T135, T133)
ADDZF_IN_AAG(zero(T154), zero(T155), zero(T153)) → U16_AAG(T154, T155, T153, addzF_in_aag(T154, T155, T153))
ADDZF_IN_AAG(zero(T154), zero(T155), zero(T153)) → ADDZF_IN_AAG(T154, T155, T153)
ADDZF_IN_AAG(zero(T174), one(T175), one(T173)) → U17_AAG(T174, T175, T173, addxG_in_aag(T174, T175, T173))
ADDZF_IN_AAG(zero(T174), one(T175), one(T173)) → ADDXG_IN_AAG(T174, T175, T173)
ADDXG_IN_AAG(one(T181), b, one(T181)) → U35_AAG(T181, binaryD_in_g(T181))
ADDXG_IN_AAG(one(T181), b, one(T181)) → BINARYD_IN_G(T181)
ADDXG_IN_AAG(zero(T186), b, zero(T186)) → U36_AAG(T186, binaryZC_in_g(T186))
ADDXG_IN_AAG(zero(T186), b, zero(T186)) → BINARYZC_IN_G(T186)
ADDXG_IN_AAG(T202, T203, T201) → U37_AAG(T202, T203, T201, addzF_in_aag(T202, T203, T201))
ADDXG_IN_AAG(T202, T203, T201) → ADDZF_IN_AAG(T202, T203, T201)
ADDZF_IN_AAG(one(T222), zero(T223), one(T221)) → U18_AAG(T222, T223, T221, addyH_in_aag(T222, T223, T221))
ADDZF_IN_AAG(one(T222), zero(T223), one(T221)) → ADDYH_IN_AAG(T222, T223, T221)
ADDYH_IN_AAG(b, one(T229), one(T229)) → U38_AAG(T229, binaryD_in_g(T229))
ADDYH_IN_AAG(b, one(T229), one(T229)) → BINARYD_IN_G(T229)
ADDYH_IN_AAG(b, zero(T234), zero(T234)) → U39_AAG(T234, binaryZC_in_g(T234))
ADDYH_IN_AAG(b, zero(T234), zero(T234)) → BINARYZC_IN_G(T234)
ADDYH_IN_AAG(T250, T251, T249) → U40_AAG(T250, T251, T249, addzF_in_aag(T250, T251, T249))
ADDYH_IN_AAG(T250, T251, T249) → ADDZF_IN_AAG(T250, T251, T249)
ADDZF_IN_AAG(one(T264), one(T265), zero(T263)) → U19_AAG(T264, T265, T263, addcI_in_aag(T264, T265, T263))
ADDZF_IN_AAG(one(T264), one(T265), zero(T263)) → ADDCI_IN_AAG(T264, T265, T263)
ADDCI_IN_AAG(T276, b, T275) → U32_AAG(T276, T275, succZK_in_ag(T276, T275))
ADDCI_IN_AAG(T276, b, T275) → SUCCZK_IN_AG(T276, T275)
SUCCZK_IN_AG(zero(T282), one(T282)) → U22_AG(T282, binaryZC_in_g(T282))
SUCCZK_IN_AG(zero(T282), one(T282)) → BINARYZC_IN_G(T282)
SUCCZK_IN_AG(one(T290), zero(T289)) → U23_AG(T290, T289, succJ_in_ag(T290, T289))
SUCCZK_IN_AG(one(T290), zero(T289)) → SUCCJ_IN_AG(T290, T289)
SUCCJ_IN_AG(zero(T295), one(T295)) → U20_AG(T295, binaryZC_in_g(T295))
SUCCJ_IN_AG(zero(T295), one(T295)) → BINARYZC_IN_G(T295)
SUCCJ_IN_AG(one(T303), zero(T302)) → U21_AG(T303, T302, succJ_in_ag(T303, T302))
SUCCJ_IN_AG(one(T303), zero(T302)) → SUCCJ_IN_AG(T303, T302)
ADDCI_IN_AAG(b, T314, T313) → U33_AAG(T314, T313, succZK_in_ag(T314, T313))
ADDCI_IN_AAG(b, T314, T313) → SUCCZK_IN_AG(T314, T313)
ADDCI_IN_AAG(T330, T331, T329) → U34_AAG(T330, T331, T329, addCL_in_aag(T330, T331, T329))
ADDCI_IN_AAG(T330, T331, T329) → ADDCL_IN_AAG(T330, T331, T329)
ADDCL_IN_AAG(zero(T350), zero(T351), one(T349)) → U24_AAG(T350, T351, T349, addzF_in_aag(T350, T351, T349))
ADDCL_IN_AAG(zero(T350), zero(T351), one(T349)) → ADDZF_IN_AAG(T350, T351, T349)
ADDCL_IN_AAG(zero(zero(T377)), one(b), zero(one(T377))) → U25_AAG(T377, binaryZC_in_g(T377))
ADDCL_IN_AAG(zero(zero(T377)), one(b), zero(one(T377))) → BINARYZC_IN_G(T377)
ADDCL_IN_AAG(zero(one(T389)), one(b), zero(zero(T388))) → U26_AAG(T389, T388, succJ_in_ag(T389, T388))
ADDCL_IN_AAG(zero(one(T389)), one(b), zero(zero(T388))) → SUCCJ_IN_AG(T389, T388)
ADDCL_IN_AAG(zero(T404), one(T405), zero(T403)) → U27_AAG(T404, T405, T403, addCL_in_aag(T404, T405, T403))
ADDCL_IN_AAG(zero(T404), one(T405), zero(T403)) → ADDCL_IN_AAG(T404, T405, T403)
ADDCL_IN_AAG(one(b), zero(zero(T431)), zero(one(T431))) → U28_AAG(T431, binaryZC_in_g(T431))
ADDCL_IN_AAG(one(b), zero(zero(T431)), zero(one(T431))) → BINARYZC_IN_G(T431)
ADDCL_IN_AAG(one(b), zero(one(T443)), zero(zero(T442))) → U29_AAG(T443, T442, succJ_in_ag(T443, T442))
ADDCL_IN_AAG(one(b), zero(one(T443)), zero(zero(T442))) → SUCCJ_IN_AG(T443, T442)
ADDCL_IN_AAG(one(T458), zero(T459), zero(T457)) → U30_AAG(T458, T459, T457, addCL_in_aag(T458, T459, T457))
ADDCL_IN_AAG(one(T458), zero(T459), zero(T457)) → ADDCL_IN_AAG(T458, T459, T457)
ADDCL_IN_AAG(one(T472), one(T473), one(T471)) → U31_AAG(T472, T473, T471, addcI_in_aag(T472, T473, T471))
ADDCL_IN_AAG(one(T472), one(T473), one(T471)) → ADDCI_IN_AAG(T472, T473, T471)
ADDZE_IN_AAG(zero(T489), one(T490), one(T488)) → U42_AAG(T489, T490, T488, addxG_in_aag(T489, T490, T488))
ADDZE_IN_AAG(zero(T489), one(T490), one(T488)) → ADDXG_IN_AAG(T489, T490, T488)
ADDZE_IN_AAG(one(T507), zero(T508), one(T506)) → U43_AAG(T507, T508, T506, addyH_in_aag(T507, T508, T506))
ADDZE_IN_AAG(one(T507), zero(T508), one(T506)) → ADDYH_IN_AAG(T507, T508, T506)
ADDZE_IN_AAG(one(T519), one(T520), zero(T518)) → U44_AAG(T519, T520, T518, addcI_in_aag(T519, T520, T518))
ADDZE_IN_AAG(one(T519), one(T520), zero(T518)) → ADDCI_IN_AAG(T519, T520, T518)
ADDA_IN_AAG(b, zero(T527), zero(T527)) → U5_AAG(T527, binaryZC_in_g(T527))
ADDA_IN_AAG(b, zero(T527), zero(T527)) → BINARYZC_IN_G(T527)
ADDA_IN_AAG(b, one(T533), one(T533)) → U6_AAG(T533, binaryD_in_g(T533))
ADDA_IN_AAG(b, one(T533), one(T533)) → BINARYD_IN_G(T533)
ADDA_IN_AAG(T548, T549, T547) → U7_AAG(T548, T549, T547, addzE_in_aag(T548, T549, T547))
ADDA_IN_AAG(zero(T576), zero(T577), zero(T575)) → U8_AAG(T576, T577, T575, addzF_in_aag(T576, T577, T575))
ADDA_IN_AAG(zero(T576), zero(T577), zero(T575)) → ADDZF_IN_AAG(T576, T577, T575)
ADDA_IN_AAG(zero(T596), one(T597), one(T595)) → U9_AAG(T596, T597, T595, addxG_in_aag(T596, T597, T595))
ADDA_IN_AAG(zero(T596), one(T597), one(T595)) → ADDXG_IN_AAG(T596, T597, T595)
ADDA_IN_AAG(one(T614), zero(T615), one(T613)) → U10_AAG(T614, T615, T613, addyH_in_aag(T614, T615, T613))
ADDA_IN_AAG(one(T614), zero(T615), one(T613)) → ADDYH_IN_AAG(T614, T615, T613)
ADDA_IN_AAG(one(T626), one(T627), zero(T625)) → U11_AAG(T626, T627, T625, addcI_in_aag(T626, T627, T625))
ADDA_IN_AAG(one(T626), one(T627), zero(T625)) → ADDCI_IN_AAG(T626, T627, T625)

The TRS R consists of the following rules:

addA_in_aag(b, b, b) → addA_out_aag(b, b, b)
addA_in_aag(zero(T69), b, zero(T69)) → U1_aag(T69, binaryZC_in_g(T69))
binaryZC_in_g(zero(T75)) → U12_g(T75, binaryZC_in_g(T75))
binaryZC_in_g(one(T79)) → U13_g(T79, binaryD_in_g(T79))
binaryD_in_g(b) → binaryD_out_g(b)
binaryD_in_g(zero(T84)) → U14_g(T84, binaryZC_in_g(T84))
U14_g(T84, binaryZC_out_g(T84)) → binaryD_out_g(zero(T84))
binaryD_in_g(one(T88)) → U15_g(T88, binaryD_in_g(T88))
U15_g(T88, binaryD_out_g(T88)) → binaryD_out_g(one(T88))
U13_g(T79, binaryD_out_g(T79)) → binaryZC_out_g(one(T79))
U12_g(T75, binaryZC_out_g(T75)) → binaryZC_out_g(zero(T75))
U1_aag(T69, binaryZC_out_g(T69)) → addA_out_aag(zero(T69), b, zero(T69))
addA_in_aag(one(T93), b, one(T93)) → U2_aag(T93, binaryD_in_g(T93))
U2_aag(T93, binaryD_out_g(T93)) → addA_out_aag(one(T93), b, one(T93))
addA_in_aag(b, T98, T98) → U3_aag(T98, binaryZC_in_g(T98))
U3_aag(T98, binaryZC_out_g(T98)) → addA_out_aag(b, T98, T98)
addA_in_aag(T114, T115, T113) → U4_aag(T114, T115, T113, addzE_in_aag(T114, T115, T113))
addzE_in_aag(zero(T134), zero(T135), zero(T133)) → U41_aag(T134, T135, T133, addzF_in_aag(T134, T135, T133))
addzF_in_aag(zero(T154), zero(T155), zero(T153)) → U16_aag(T154, T155, T153, addzF_in_aag(T154, T155, T153))
addzF_in_aag(zero(T174), one(T175), one(T173)) → U17_aag(T174, T175, T173, addxG_in_aag(T174, T175, T173))
addxG_in_aag(one(T181), b, one(T181)) → U35_aag(T181, binaryD_in_g(T181))
U35_aag(T181, binaryD_out_g(T181)) → addxG_out_aag(one(T181), b, one(T181))
addxG_in_aag(zero(T186), b, zero(T186)) → U36_aag(T186, binaryZC_in_g(T186))
U36_aag(T186, binaryZC_out_g(T186)) → addxG_out_aag(zero(T186), b, zero(T186))
addxG_in_aag(T202, T203, T201) → U37_aag(T202, T203, T201, addzF_in_aag(T202, T203, T201))
addzF_in_aag(one(T222), zero(T223), one(T221)) → U18_aag(T222, T223, T221, addyH_in_aag(T222, T223, T221))
addyH_in_aag(b, one(T229), one(T229)) → U38_aag(T229, binaryD_in_g(T229))
U38_aag(T229, binaryD_out_g(T229)) → addyH_out_aag(b, one(T229), one(T229))
addyH_in_aag(b, zero(T234), zero(T234)) → U39_aag(T234, binaryZC_in_g(T234))
U39_aag(T234, binaryZC_out_g(T234)) → addyH_out_aag(b, zero(T234), zero(T234))
addyH_in_aag(T250, T251, T249) → U40_aag(T250, T251, T249, addzF_in_aag(T250, T251, T249))
addzF_in_aag(one(T264), one(T265), zero(T263)) → U19_aag(T264, T265, T263, addcI_in_aag(T264, T265, T263))
addcI_in_aag(b, b, one(b)) → addcI_out_aag(b, b, one(b))
addcI_in_aag(T276, b, T275) → U32_aag(T276, T275, succZK_in_ag(T276, T275))
succZK_in_ag(zero(T282), one(T282)) → U22_ag(T282, binaryZC_in_g(T282))
U22_ag(T282, binaryZC_out_g(T282)) → succZK_out_ag(zero(T282), one(T282))
succZK_in_ag(one(T290), zero(T289)) → U23_ag(T290, T289, succJ_in_ag(T290, T289))
succJ_in_ag(b, one(b)) → succJ_out_ag(b, one(b))
succJ_in_ag(zero(T295), one(T295)) → U20_ag(T295, binaryZC_in_g(T295))
U20_ag(T295, binaryZC_out_g(T295)) → succJ_out_ag(zero(T295), one(T295))
succJ_in_ag(one(T303), zero(T302)) → U21_ag(T303, T302, succJ_in_ag(T303, T302))
U21_ag(T303, T302, succJ_out_ag(T303, T302)) → succJ_out_ag(one(T303), zero(T302))
U23_ag(T290, T289, succJ_out_ag(T290, T289)) → succZK_out_ag(one(T290), zero(T289))
U32_aag(T276, T275, succZK_out_ag(T276, T275)) → addcI_out_aag(T276, b, T275)
addcI_in_aag(b, T314, T313) → U33_aag(T314, T313, succZK_in_ag(T314, T313))
U33_aag(T314, T313, succZK_out_ag(T314, T313)) → addcI_out_aag(b, T314, T313)
addcI_in_aag(T330, T331, T329) → U34_aag(T330, T331, T329, addCL_in_aag(T330, T331, T329))
addCL_in_aag(zero(T350), zero(T351), one(T349)) → U24_aag(T350, T351, T349, addzF_in_aag(T350, T351, T349))
U24_aag(T350, T351, T349, addzF_out_aag(T350, T351, T349)) → addCL_out_aag(zero(T350), zero(T351), one(T349))
addCL_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U25_aag(T377, binaryZC_in_g(T377))
U25_aag(T377, binaryZC_out_g(T377)) → addCL_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCL_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U26_aag(T389, T388, succJ_in_ag(T389, T388))
U26_aag(T389, T388, succJ_out_ag(T389, T388)) → addCL_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCL_in_aag(zero(T404), one(T405), zero(T403)) → U27_aag(T404, T405, T403, addCL_in_aag(T404, T405, T403))
addCL_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U28_aag(T431, binaryZC_in_g(T431))
U28_aag(T431, binaryZC_out_g(T431)) → addCL_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCL_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U29_aag(T443, T442, succJ_in_ag(T443, T442))
U29_aag(T443, T442, succJ_out_ag(T443, T442)) → addCL_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCL_in_aag(one(T458), zero(T459), zero(T457)) → U30_aag(T458, T459, T457, addCL_in_aag(T458, T459, T457))
addCL_in_aag(one(T472), one(T473), one(T471)) → U31_aag(T472, T473, T471, addcI_in_aag(T472, T473, T471))
U31_aag(T472, T473, T471, addcI_out_aag(T472, T473, T471)) → addCL_out_aag(one(T472), one(T473), one(T471))
U30_aag(T458, T459, T457, addCL_out_aag(T458, T459, T457)) → addCL_out_aag(one(T458), zero(T459), zero(T457))
U27_aag(T404, T405, T403, addCL_out_aag(T404, T405, T403)) → addCL_out_aag(zero(T404), one(T405), zero(T403))
U34_aag(T330, T331, T329, addCL_out_aag(T330, T331, T329)) → addcI_out_aag(T330, T331, T329)
U19_aag(T264, T265, T263, addcI_out_aag(T264, T265, T263)) → addzF_out_aag(one(T264), one(T265), zero(T263))
U40_aag(T250, T251, T249, addzF_out_aag(T250, T251, T249)) → addyH_out_aag(T250, T251, T249)
U18_aag(T222, T223, T221, addyH_out_aag(T222, T223, T221)) → addzF_out_aag(one(T222), zero(T223), one(T221))
U37_aag(T202, T203, T201, addzF_out_aag(T202, T203, T201)) → addxG_out_aag(T202, T203, T201)
U17_aag(T174, T175, T173, addxG_out_aag(T174, T175, T173)) → addzF_out_aag(zero(T174), one(T175), one(T173))
U16_aag(T154, T155, T153, addzF_out_aag(T154, T155, T153)) → addzF_out_aag(zero(T154), zero(T155), zero(T153))
U41_aag(T134, T135, T133, addzF_out_aag(T134, T135, T133)) → addzE_out_aag(zero(T134), zero(T135), zero(T133))
addzE_in_aag(zero(T489), one(T490), one(T488)) → U42_aag(T489, T490, T488, addxG_in_aag(T489, T490, T488))
U42_aag(T489, T490, T488, addxG_out_aag(T489, T490, T488)) → addzE_out_aag(zero(T489), one(T490), one(T488))
addzE_in_aag(one(T507), zero(T508), one(T506)) → U43_aag(T507, T508, T506, addyH_in_aag(T507, T508, T506))
U43_aag(T507, T508, T506, addyH_out_aag(T507, T508, T506)) → addzE_out_aag(one(T507), zero(T508), one(T506))
addzE_in_aag(one(T519), one(T520), zero(T518)) → U44_aag(T519, T520, T518, addcI_in_aag(T519, T520, T518))
U44_aag(T519, T520, T518, addcI_out_aag(T519, T520, T518)) → addzE_out_aag(one(T519), one(T520), zero(T518))
U4_aag(T114, T115, T113, addzE_out_aag(T114, T115, T113)) → addA_out_aag(T114, T115, T113)
addA_in_aag(b, zero(T527), zero(T527)) → U5_aag(T527, binaryZC_in_g(T527))
U5_aag(T527, binaryZC_out_g(T527)) → addA_out_aag(b, zero(T527), zero(T527))
addA_in_aag(b, one(T533), one(T533)) → U6_aag(T533, binaryD_in_g(T533))
U6_aag(T533, binaryD_out_g(T533)) → addA_out_aag(b, one(T533), one(T533))
addA_in_aag(T548, T549, T547) → U7_aag(T548, T549, T547, addzE_in_aag(T548, T549, T547))
U7_aag(T548, T549, T547, addzE_out_aag(T548, T549, T547)) → addA_out_aag(T548, T549, T547)
addA_in_aag(zero(T576), zero(T577), zero(T575)) → U8_aag(T576, T577, T575, addzF_in_aag(T576, T577, T575))
U8_aag(T576, T577, T575, addzF_out_aag(T576, T577, T575)) → addA_out_aag(zero(T576), zero(T577), zero(T575))
addA_in_aag(zero(T596), one(T597), one(T595)) → U9_aag(T596, T597, T595, addxG_in_aag(T596, T597, T595))
U9_aag(T596, T597, T595, addxG_out_aag(T596, T597, T595)) → addA_out_aag(zero(T596), one(T597), one(T595))
addA_in_aag(one(T614), zero(T615), one(T613)) → U10_aag(T614, T615, T613, addyH_in_aag(T614, T615, T613))
U10_aag(T614, T615, T613, addyH_out_aag(T614, T615, T613)) → addA_out_aag(one(T614), zero(T615), one(T613))
addA_in_aag(one(T626), one(T627), zero(T625)) → U11_aag(T626, T627, T625, addcI_in_aag(T626, T627, T625))
U11_aag(T626, T627, T625, addcI_out_aag(T626, T627, T625)) → addA_out_aag(one(T626), one(T627), zero(T625))

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

BINARYZC_IN_G(one(T79)) → BINARYD_IN_G(T79)
BINARYD_IN_G(zero(T84)) → BINARYZC_IN_G(T84)
BINARYZC_IN_G(zero(T75)) → BINARYZC_IN_G(T75)
BINARYD_IN_G(one(T88)) → BINARYD_IN_G(T88)

The TRS R consists of the following rules:

addA_in_aag(b, b, b) → addA_out_aag(b, b, b)
addA_in_aag(zero(T69), b, zero(T69)) → U1_aag(T69, binaryZC_in_g(T69))
binaryZC_in_g(zero(T75)) → U12_g(T75, binaryZC_in_g(T75))
binaryZC_in_g(one(T79)) → U13_g(T79, binaryD_in_g(T79))
binaryD_in_g(b) → binaryD_out_g(b)
binaryD_in_g(zero(T84)) → U14_g(T84, binaryZC_in_g(T84))
U14_g(T84, binaryZC_out_g(T84)) → binaryD_out_g(zero(T84))
binaryD_in_g(one(T88)) → U15_g(T88, binaryD_in_g(T88))
U15_g(T88, binaryD_out_g(T88)) → binaryD_out_g(one(T88))
U13_g(T79, binaryD_out_g(T79)) → binaryZC_out_g(one(T79))
U12_g(T75, binaryZC_out_g(T75)) → binaryZC_out_g(zero(T75))
U1_aag(T69, binaryZC_out_g(T69)) → addA_out_aag(zero(T69), b, zero(T69))
addA_in_aag(one(T93), b, one(T93)) → U2_aag(T93, binaryD_in_g(T93))
U2_aag(T93, binaryD_out_g(T93)) → addA_out_aag(one(T93), b, one(T93))
addA_in_aag(b, T98, T98) → U3_aag(T98, binaryZC_in_g(T98))
U3_aag(T98, binaryZC_out_g(T98)) → addA_out_aag(b, T98, T98)
addA_in_aag(T114, T115, T113) → U4_aag(T114, T115, T113, addzE_in_aag(T114, T115, T113))
addzE_in_aag(zero(T134), zero(T135), zero(T133)) → U41_aag(T134, T135, T133, addzF_in_aag(T134, T135, T133))
addzF_in_aag(zero(T154), zero(T155), zero(T153)) → U16_aag(T154, T155, T153, addzF_in_aag(T154, T155, T153))
addzF_in_aag(zero(T174), one(T175), one(T173)) → U17_aag(T174, T175, T173, addxG_in_aag(T174, T175, T173))
addxG_in_aag(one(T181), b, one(T181)) → U35_aag(T181, binaryD_in_g(T181))
U35_aag(T181, binaryD_out_g(T181)) → addxG_out_aag(one(T181), b, one(T181))
addxG_in_aag(zero(T186), b, zero(T186)) → U36_aag(T186, binaryZC_in_g(T186))
U36_aag(T186, binaryZC_out_g(T186)) → addxG_out_aag(zero(T186), b, zero(T186))
addxG_in_aag(T202, T203, T201) → U37_aag(T202, T203, T201, addzF_in_aag(T202, T203, T201))
addzF_in_aag(one(T222), zero(T223), one(T221)) → U18_aag(T222, T223, T221, addyH_in_aag(T222, T223, T221))
addyH_in_aag(b, one(T229), one(T229)) → U38_aag(T229, binaryD_in_g(T229))
U38_aag(T229, binaryD_out_g(T229)) → addyH_out_aag(b, one(T229), one(T229))
addyH_in_aag(b, zero(T234), zero(T234)) → U39_aag(T234, binaryZC_in_g(T234))
U39_aag(T234, binaryZC_out_g(T234)) → addyH_out_aag(b, zero(T234), zero(T234))
addyH_in_aag(T250, T251, T249) → U40_aag(T250, T251, T249, addzF_in_aag(T250, T251, T249))
addzF_in_aag(one(T264), one(T265), zero(T263)) → U19_aag(T264, T265, T263, addcI_in_aag(T264, T265, T263))
addcI_in_aag(b, b, one(b)) → addcI_out_aag(b, b, one(b))
addcI_in_aag(T276, b, T275) → U32_aag(T276, T275, succZK_in_ag(T276, T275))
succZK_in_ag(zero(T282), one(T282)) → U22_ag(T282, binaryZC_in_g(T282))
U22_ag(T282, binaryZC_out_g(T282)) → succZK_out_ag(zero(T282), one(T282))
succZK_in_ag(one(T290), zero(T289)) → U23_ag(T290, T289, succJ_in_ag(T290, T289))
succJ_in_ag(b, one(b)) → succJ_out_ag(b, one(b))
succJ_in_ag(zero(T295), one(T295)) → U20_ag(T295, binaryZC_in_g(T295))
U20_ag(T295, binaryZC_out_g(T295)) → succJ_out_ag(zero(T295), one(T295))
succJ_in_ag(one(T303), zero(T302)) → U21_ag(T303, T302, succJ_in_ag(T303, T302))
U21_ag(T303, T302, succJ_out_ag(T303, T302)) → succJ_out_ag(one(T303), zero(T302))
U23_ag(T290, T289, succJ_out_ag(T290, T289)) → succZK_out_ag(one(T290), zero(T289))
U32_aag(T276, T275, succZK_out_ag(T276, T275)) → addcI_out_aag(T276, b, T275)
addcI_in_aag(b, T314, T313) → U33_aag(T314, T313, succZK_in_ag(T314, T313))
U33_aag(T314, T313, succZK_out_ag(T314, T313)) → addcI_out_aag(b, T314, T313)
addcI_in_aag(T330, T331, T329) → U34_aag(T330, T331, T329, addCL_in_aag(T330, T331, T329))
addCL_in_aag(zero(T350), zero(T351), one(T349)) → U24_aag(T350, T351, T349, addzF_in_aag(T350, T351, T349))
U24_aag(T350, T351, T349, addzF_out_aag(T350, T351, T349)) → addCL_out_aag(zero(T350), zero(T351), one(T349))
addCL_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U25_aag(T377, binaryZC_in_g(T377))
U25_aag(T377, binaryZC_out_g(T377)) → addCL_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCL_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U26_aag(T389, T388, succJ_in_ag(T389, T388))
U26_aag(T389, T388, succJ_out_ag(T389, T388)) → addCL_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCL_in_aag(zero(T404), one(T405), zero(T403)) → U27_aag(T404, T405, T403, addCL_in_aag(T404, T405, T403))
addCL_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U28_aag(T431, binaryZC_in_g(T431))
U28_aag(T431, binaryZC_out_g(T431)) → addCL_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCL_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U29_aag(T443, T442, succJ_in_ag(T443, T442))
U29_aag(T443, T442, succJ_out_ag(T443, T442)) → addCL_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCL_in_aag(one(T458), zero(T459), zero(T457)) → U30_aag(T458, T459, T457, addCL_in_aag(T458, T459, T457))
addCL_in_aag(one(T472), one(T473), one(T471)) → U31_aag(T472, T473, T471, addcI_in_aag(T472, T473, T471))
U31_aag(T472, T473, T471, addcI_out_aag(T472, T473, T471)) → addCL_out_aag(one(T472), one(T473), one(T471))
U30_aag(T458, T459, T457, addCL_out_aag(T458, T459, T457)) → addCL_out_aag(one(T458), zero(T459), zero(T457))
U27_aag(T404, T405, T403, addCL_out_aag(T404, T405, T403)) → addCL_out_aag(zero(T404), one(T405), zero(T403))
U34_aag(T330, T331, T329, addCL_out_aag(T330, T331, T329)) → addcI_out_aag(T330, T331, T329)
U19_aag(T264, T265, T263, addcI_out_aag(T264, T265, T263)) → addzF_out_aag(one(T264), one(T265), zero(T263))
U40_aag(T250, T251, T249, addzF_out_aag(T250, T251, T249)) → addyH_out_aag(T250, T251, T249)
U18_aag(T222, T223, T221, addyH_out_aag(T222, T223, T221)) → addzF_out_aag(one(T222), zero(T223), one(T221))
U37_aag(T202, T203, T201, addzF_out_aag(T202, T203, T201)) → addxG_out_aag(T202, T203, T201)
U17_aag(T174, T175, T173, addxG_out_aag(T174, T175, T173)) → addzF_out_aag(zero(T174), one(T175), one(T173))
U16_aag(T154, T155, T153, addzF_out_aag(T154, T155, T153)) → addzF_out_aag(zero(T154), zero(T155), zero(T153))
U41_aag(T134, T135, T133, addzF_out_aag(T134, T135, T133)) → addzE_out_aag(zero(T134), zero(T135), zero(T133))
addzE_in_aag(zero(T489), one(T490), one(T488)) → U42_aag(T489, T490, T488, addxG_in_aag(T489, T490, T488))
U42_aag(T489, T490, T488, addxG_out_aag(T489, T490, T488)) → addzE_out_aag(zero(T489), one(T490), one(T488))
addzE_in_aag(one(T507), zero(T508), one(T506)) → U43_aag(T507, T508, T506, addyH_in_aag(T507, T508, T506))
U43_aag(T507, T508, T506, addyH_out_aag(T507, T508, T506)) → addzE_out_aag(one(T507), zero(T508), one(T506))
addzE_in_aag(one(T519), one(T520), zero(T518)) → U44_aag(T519, T520, T518, addcI_in_aag(T519, T520, T518))
U44_aag(T519, T520, T518, addcI_out_aag(T519, T520, T518)) → addzE_out_aag(one(T519), one(T520), zero(T518))
U4_aag(T114, T115, T113, addzE_out_aag(T114, T115, T113)) → addA_out_aag(T114, T115, T113)
addA_in_aag(b, zero(T527), zero(T527)) → U5_aag(T527, binaryZC_in_g(T527))
U5_aag(T527, binaryZC_out_g(T527)) → addA_out_aag(b, zero(T527), zero(T527))
addA_in_aag(b, one(T533), one(T533)) → U6_aag(T533, binaryD_in_g(T533))
U6_aag(T533, binaryD_out_g(T533)) → addA_out_aag(b, one(T533), one(T533))
addA_in_aag(T548, T549, T547) → U7_aag(T548, T549, T547, addzE_in_aag(T548, T549, T547))
U7_aag(T548, T549, T547, addzE_out_aag(T548, T549, T547)) → addA_out_aag(T548, T549, T547)
addA_in_aag(zero(T576), zero(T577), zero(T575)) → U8_aag(T576, T577, T575, addzF_in_aag(T576, T577, T575))
U8_aag(T576, T577, T575, addzF_out_aag(T576, T577, T575)) → addA_out_aag(zero(T576), zero(T577), zero(T575))
addA_in_aag(zero(T596), one(T597), one(T595)) → U9_aag(T596, T597, T595, addxG_in_aag(T596, T597, T595))
U9_aag(T596, T597, T595, addxG_out_aag(T596, T597, T595)) → addA_out_aag(zero(T596), one(T597), one(T595))
addA_in_aag(one(T614), zero(T615), one(T613)) → U10_aag(T614, T615, T613, addyH_in_aag(T614, T615, T613))
U10_aag(T614, T615, T613, addyH_out_aag(T614, T615, T613)) → addA_out_aag(one(T614), zero(T615), one(T613))
addA_in_aag(one(T626), one(T627), zero(T625)) → U11_aag(T626, T627, T625, addcI_in_aag(T626, T627, T625))
U11_aag(T626, T627, T625, addcI_out_aag(T626, T627, T625)) → addA_out_aag(one(T626), one(T627), zero(T625))

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

BINARYZC_IN_G(one(T79)) → BINARYD_IN_G(T79)
BINARYD_IN_G(zero(T84)) → BINARYZC_IN_G(T84)
BINARYZC_IN_G(zero(T75)) → BINARYZC_IN_G(T75)
BINARYD_IN_G(one(T88)) → BINARYD_IN_G(T88)

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:

BINARYZC_IN_G(one(T79)) → BINARYD_IN_G(T79)
BINARYD_IN_G(zero(T84)) → BINARYZC_IN_G(T84)
BINARYZC_IN_G(zero(T75)) → BINARYZC_IN_G(T75)
BINARYD_IN_G(one(T88)) → BINARYD_IN_G(T88)

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:

BINARYD_IN_G(zero(T84)) → BINARYZC_IN_G(T84)
The graph contains the following edges 1 > 1
BINARYD_IN_G(one(T88)) → BINARYD_IN_G(T88)
The graph contains the following edges 1 > 1
BINARYZC_IN_G(zero(T75)) → BINARYZC_IN_G(T75)
The graph contains the following edges 1 > 1
BINARYZC_IN_G(one(T79)) → BINARYD_IN_G(T79)
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_AG(one(T303), zero(T302)) → SUCCJ_IN_AG(T303, T302)

The TRS R consists of the following rules:

addA_in_aag(b, b, b) → addA_out_aag(b, b, b)
addA_in_aag(zero(T69), b, zero(T69)) → U1_aag(T69, binaryZC_in_g(T69))
binaryZC_in_g(zero(T75)) → U12_g(T75, binaryZC_in_g(T75))
binaryZC_in_g(one(T79)) → U13_g(T79, binaryD_in_g(T79))
binaryD_in_g(b) → binaryD_out_g(b)
binaryD_in_g(zero(T84)) → U14_g(T84, binaryZC_in_g(T84))
U14_g(T84, binaryZC_out_g(T84)) → binaryD_out_g(zero(T84))
binaryD_in_g(one(T88)) → U15_g(T88, binaryD_in_g(T88))
U15_g(T88, binaryD_out_g(T88)) → binaryD_out_g(one(T88))
U13_g(T79, binaryD_out_g(T79)) → binaryZC_out_g(one(T79))
U12_g(T75, binaryZC_out_g(T75)) → binaryZC_out_g(zero(T75))
U1_aag(T69, binaryZC_out_g(T69)) → addA_out_aag(zero(T69), b, zero(T69))
addA_in_aag(one(T93), b, one(T93)) → U2_aag(T93, binaryD_in_g(T93))
U2_aag(T93, binaryD_out_g(T93)) → addA_out_aag(one(T93), b, one(T93))
addA_in_aag(b, T98, T98) → U3_aag(T98, binaryZC_in_g(T98))
U3_aag(T98, binaryZC_out_g(T98)) → addA_out_aag(b, T98, T98)
addA_in_aag(T114, T115, T113) → U4_aag(T114, T115, T113, addzE_in_aag(T114, T115, T113))
addzE_in_aag(zero(T134), zero(T135), zero(T133)) → U41_aag(T134, T135, T133, addzF_in_aag(T134, T135, T133))
addzF_in_aag(zero(T154), zero(T155), zero(T153)) → U16_aag(T154, T155, T153, addzF_in_aag(T154, T155, T153))
addzF_in_aag(zero(T174), one(T175), one(T173)) → U17_aag(T174, T175, T173, addxG_in_aag(T174, T175, T173))
addxG_in_aag(one(T181), b, one(T181)) → U35_aag(T181, binaryD_in_g(T181))
U35_aag(T181, binaryD_out_g(T181)) → addxG_out_aag(one(T181), b, one(T181))
addxG_in_aag(zero(T186), b, zero(T186)) → U36_aag(T186, binaryZC_in_g(T186))
U36_aag(T186, binaryZC_out_g(T186)) → addxG_out_aag(zero(T186), b, zero(T186))
addxG_in_aag(T202, T203, T201) → U37_aag(T202, T203, T201, addzF_in_aag(T202, T203, T201))
addzF_in_aag(one(T222), zero(T223), one(T221)) → U18_aag(T222, T223, T221, addyH_in_aag(T222, T223, T221))
addyH_in_aag(b, one(T229), one(T229)) → U38_aag(T229, binaryD_in_g(T229))
U38_aag(T229, binaryD_out_g(T229)) → addyH_out_aag(b, one(T229), one(T229))
addyH_in_aag(b, zero(T234), zero(T234)) → U39_aag(T234, binaryZC_in_g(T234))
U39_aag(T234, binaryZC_out_g(T234)) → addyH_out_aag(b, zero(T234), zero(T234))
addyH_in_aag(T250, T251, T249) → U40_aag(T250, T251, T249, addzF_in_aag(T250, T251, T249))
addzF_in_aag(one(T264), one(T265), zero(T263)) → U19_aag(T264, T265, T263, addcI_in_aag(T264, T265, T263))
addcI_in_aag(b, b, one(b)) → addcI_out_aag(b, b, one(b))
addcI_in_aag(T276, b, T275) → U32_aag(T276, T275, succZK_in_ag(T276, T275))
succZK_in_ag(zero(T282), one(T282)) → U22_ag(T282, binaryZC_in_g(T282))
U22_ag(T282, binaryZC_out_g(T282)) → succZK_out_ag(zero(T282), one(T282))
succZK_in_ag(one(T290), zero(T289)) → U23_ag(T290, T289, succJ_in_ag(T290, T289))
succJ_in_ag(b, one(b)) → succJ_out_ag(b, one(b))
succJ_in_ag(zero(T295), one(T295)) → U20_ag(T295, binaryZC_in_g(T295))
U20_ag(T295, binaryZC_out_g(T295)) → succJ_out_ag(zero(T295), one(T295))
succJ_in_ag(one(T303), zero(T302)) → U21_ag(T303, T302, succJ_in_ag(T303, T302))
U21_ag(T303, T302, succJ_out_ag(T303, T302)) → succJ_out_ag(one(T303), zero(T302))
U23_ag(T290, T289, succJ_out_ag(T290, T289)) → succZK_out_ag(one(T290), zero(T289))
U32_aag(T276, T275, succZK_out_ag(T276, T275)) → addcI_out_aag(T276, b, T275)
addcI_in_aag(b, T314, T313) → U33_aag(T314, T313, succZK_in_ag(T314, T313))
U33_aag(T314, T313, succZK_out_ag(T314, T313)) → addcI_out_aag(b, T314, T313)
addcI_in_aag(T330, T331, T329) → U34_aag(T330, T331, T329, addCL_in_aag(T330, T331, T329))
addCL_in_aag(zero(T350), zero(T351), one(T349)) → U24_aag(T350, T351, T349, addzF_in_aag(T350, T351, T349))
U24_aag(T350, T351, T349, addzF_out_aag(T350, T351, T349)) → addCL_out_aag(zero(T350), zero(T351), one(T349))
addCL_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U25_aag(T377, binaryZC_in_g(T377))
U25_aag(T377, binaryZC_out_g(T377)) → addCL_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCL_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U26_aag(T389, T388, succJ_in_ag(T389, T388))
U26_aag(T389, T388, succJ_out_ag(T389, T388)) → addCL_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCL_in_aag(zero(T404), one(T405), zero(T403)) → U27_aag(T404, T405, T403, addCL_in_aag(T404, T405, T403))
addCL_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U28_aag(T431, binaryZC_in_g(T431))
U28_aag(T431, binaryZC_out_g(T431)) → addCL_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCL_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U29_aag(T443, T442, succJ_in_ag(T443, T442))
U29_aag(T443, T442, succJ_out_ag(T443, T442)) → addCL_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCL_in_aag(one(T458), zero(T459), zero(T457)) → U30_aag(T458, T459, T457, addCL_in_aag(T458, T459, T457))
addCL_in_aag(one(T472), one(T473), one(T471)) → U31_aag(T472, T473, T471, addcI_in_aag(T472, T473, T471))
U31_aag(T472, T473, T471, addcI_out_aag(T472, T473, T471)) → addCL_out_aag(one(T472), one(T473), one(T471))
U30_aag(T458, T459, T457, addCL_out_aag(T458, T459, T457)) → addCL_out_aag(one(T458), zero(T459), zero(T457))
U27_aag(T404, T405, T403, addCL_out_aag(T404, T405, T403)) → addCL_out_aag(zero(T404), one(T405), zero(T403))
U34_aag(T330, T331, T329, addCL_out_aag(T330, T331, T329)) → addcI_out_aag(T330, T331, T329)
U19_aag(T264, T265, T263, addcI_out_aag(T264, T265, T263)) → addzF_out_aag(one(T264), one(T265), zero(T263))
U40_aag(T250, T251, T249, addzF_out_aag(T250, T251, T249)) → addyH_out_aag(T250, T251, T249)
U18_aag(T222, T223, T221, addyH_out_aag(T222, T223, T221)) → addzF_out_aag(one(T222), zero(T223), one(T221))
U37_aag(T202, T203, T201, addzF_out_aag(T202, T203, T201)) → addxG_out_aag(T202, T203, T201)
U17_aag(T174, T175, T173, addxG_out_aag(T174, T175, T173)) → addzF_out_aag(zero(T174), one(T175), one(T173))
U16_aag(T154, T155, T153, addzF_out_aag(T154, T155, T153)) → addzF_out_aag(zero(T154), zero(T155), zero(T153))
U41_aag(T134, T135, T133, addzF_out_aag(T134, T135, T133)) → addzE_out_aag(zero(T134), zero(T135), zero(T133))
addzE_in_aag(zero(T489), one(T490), one(T488)) → U42_aag(T489, T490, T488, addxG_in_aag(T489, T490, T488))
U42_aag(T489, T490, T488, addxG_out_aag(T489, T490, T488)) → addzE_out_aag(zero(T489), one(T490), one(T488))
addzE_in_aag(one(T507), zero(T508), one(T506)) → U43_aag(T507, T508, T506, addyH_in_aag(T507, T508, T506))
U43_aag(T507, T508, T506, addyH_out_aag(T507, T508, T506)) → addzE_out_aag(one(T507), zero(T508), one(T506))
addzE_in_aag(one(T519), one(T520), zero(T518)) → U44_aag(T519, T520, T518, addcI_in_aag(T519, T520, T518))
U44_aag(T519, T520, T518, addcI_out_aag(T519, T520, T518)) → addzE_out_aag(one(T519), one(T520), zero(T518))
U4_aag(T114, T115, T113, addzE_out_aag(T114, T115, T113)) → addA_out_aag(T114, T115, T113)
addA_in_aag(b, zero(T527), zero(T527)) → U5_aag(T527, binaryZC_in_g(T527))
U5_aag(T527, binaryZC_out_g(T527)) → addA_out_aag(b, zero(T527), zero(T527))
addA_in_aag(b, one(T533), one(T533)) → U6_aag(T533, binaryD_in_g(T533))
U6_aag(T533, binaryD_out_g(T533)) → addA_out_aag(b, one(T533), one(T533))
addA_in_aag(T548, T549, T547) → U7_aag(T548, T549, T547, addzE_in_aag(T548, T549, T547))
U7_aag(T548, T549, T547, addzE_out_aag(T548, T549, T547)) → addA_out_aag(T548, T549, T547)
addA_in_aag(zero(T576), zero(T577), zero(T575)) → U8_aag(T576, T577, T575, addzF_in_aag(T576, T577, T575))
U8_aag(T576, T577, T575, addzF_out_aag(T576, T577, T575)) → addA_out_aag(zero(T576), zero(T577), zero(T575))
addA_in_aag(zero(T596), one(T597), one(T595)) → U9_aag(T596, T597, T595, addxG_in_aag(T596, T597, T595))
U9_aag(T596, T597, T595, addxG_out_aag(T596, T597, T595)) → addA_out_aag(zero(T596), one(T597), one(T595))
addA_in_aag(one(T614), zero(T615), one(T613)) → U10_aag(T614, T615, T613, addyH_in_aag(T614, T615, T613))
U10_aag(T614, T615, T613, addyH_out_aag(T614, T615, T613)) → addA_out_aag(one(T614), zero(T615), one(T613))
addA_in_aag(one(T626), one(T627), zero(T625)) → U11_aag(T626, T627, T625, addcI_in_aag(T626, T627, T625))
U11_aag(T626, T627, T625, addcI_out_aag(T626, T627, T625)) → addA_out_aag(one(T626), one(T627), zero(T625))

(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_AG(one(T303), zero(T302)) → SUCCJ_IN_AG(T303, T302)

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

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_AG(zero(T302)) → SUCCJ_IN_AG(T302)

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_AG(zero(T302)) → SUCCJ_IN_AG(T302)
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_AAG(T202, T203, T201) → ADDZF_IN_AAG(T202, T203, T201)
ADDZF_IN_AAG(zero(T154), zero(T155), zero(T153)) → ADDZF_IN_AAG(T154, T155, T153)
ADDZF_IN_AAG(zero(T174), one(T175), one(T173)) → ADDXG_IN_AAG(T174, T175, T173)
ADDZF_IN_AAG(one(T222), zero(T223), one(T221)) → ADDYH_IN_AAG(T222, T223, T221)
ADDYH_IN_AAG(T250, T251, T249) → ADDZF_IN_AAG(T250, T251, T249)
ADDZF_IN_AAG(one(T264), one(T265), zero(T263)) → ADDCI_IN_AAG(T264, T265, T263)
ADDCI_IN_AAG(T330, T331, T329) → ADDCL_IN_AAG(T330, T331, T329)
ADDCL_IN_AAG(zero(T350), zero(T351), one(T349)) → ADDZF_IN_AAG(T350, T351, T349)
ADDCL_IN_AAG(zero(T404), one(T405), zero(T403)) → ADDCL_IN_AAG(T404, T405, T403)
ADDCL_IN_AAG(one(T458), zero(T459), zero(T457)) → ADDCL_IN_AAG(T458, T459, T457)
ADDCL_IN_AAG(one(T472), one(T473), one(T471)) → ADDCI_IN_AAG(T472, T473, T471)

The TRS R consists of the following rules:

addA_in_aag(b, b, b) → addA_out_aag(b, b, b)
addA_in_aag(zero(T69), b, zero(T69)) → U1_aag(T69, binaryZC_in_g(T69))
binaryZC_in_g(zero(T75)) → U12_g(T75, binaryZC_in_g(T75))
binaryZC_in_g(one(T79)) → U13_g(T79, binaryD_in_g(T79))
binaryD_in_g(b) → binaryD_out_g(b)
binaryD_in_g(zero(T84)) → U14_g(T84, binaryZC_in_g(T84))
U14_g(T84, binaryZC_out_g(T84)) → binaryD_out_g(zero(T84))
binaryD_in_g(one(T88)) → U15_g(T88, binaryD_in_g(T88))
U15_g(T88, binaryD_out_g(T88)) → binaryD_out_g(one(T88))
U13_g(T79, binaryD_out_g(T79)) → binaryZC_out_g(one(T79))
U12_g(T75, binaryZC_out_g(T75)) → binaryZC_out_g(zero(T75))
U1_aag(T69, binaryZC_out_g(T69)) → addA_out_aag(zero(T69), b, zero(T69))
addA_in_aag(one(T93), b, one(T93)) → U2_aag(T93, binaryD_in_g(T93))
U2_aag(T93, binaryD_out_g(T93)) → addA_out_aag(one(T93), b, one(T93))
addA_in_aag(b, T98, T98) → U3_aag(T98, binaryZC_in_g(T98))
U3_aag(T98, binaryZC_out_g(T98)) → addA_out_aag(b, T98, T98)
addA_in_aag(T114, T115, T113) → U4_aag(T114, T115, T113, addzE_in_aag(T114, T115, T113))
addzE_in_aag(zero(T134), zero(T135), zero(T133)) → U41_aag(T134, T135, T133, addzF_in_aag(T134, T135, T133))
addzF_in_aag(zero(T154), zero(T155), zero(T153)) → U16_aag(T154, T155, T153, addzF_in_aag(T154, T155, T153))
addzF_in_aag(zero(T174), one(T175), one(T173)) → U17_aag(T174, T175, T173, addxG_in_aag(T174, T175, T173))
addxG_in_aag(one(T181), b, one(T181)) → U35_aag(T181, binaryD_in_g(T181))
U35_aag(T181, binaryD_out_g(T181)) → addxG_out_aag(one(T181), b, one(T181))
addxG_in_aag(zero(T186), b, zero(T186)) → U36_aag(T186, binaryZC_in_g(T186))
U36_aag(T186, binaryZC_out_g(T186)) → addxG_out_aag(zero(T186), b, zero(T186))
addxG_in_aag(T202, T203, T201) → U37_aag(T202, T203, T201, addzF_in_aag(T202, T203, T201))
addzF_in_aag(one(T222), zero(T223), one(T221)) → U18_aag(T222, T223, T221, addyH_in_aag(T222, T223, T221))
addyH_in_aag(b, one(T229), one(T229)) → U38_aag(T229, binaryD_in_g(T229))
U38_aag(T229, binaryD_out_g(T229)) → addyH_out_aag(b, one(T229), one(T229))
addyH_in_aag(b, zero(T234), zero(T234)) → U39_aag(T234, binaryZC_in_g(T234))
U39_aag(T234, binaryZC_out_g(T234)) → addyH_out_aag(b, zero(T234), zero(T234))
addyH_in_aag(T250, T251, T249) → U40_aag(T250, T251, T249, addzF_in_aag(T250, T251, T249))
addzF_in_aag(one(T264), one(T265), zero(T263)) → U19_aag(T264, T265, T263, addcI_in_aag(T264, T265, T263))
addcI_in_aag(b, b, one(b)) → addcI_out_aag(b, b, one(b))
addcI_in_aag(T276, b, T275) → U32_aag(T276, T275, succZK_in_ag(T276, T275))
succZK_in_ag(zero(T282), one(T282)) → U22_ag(T282, binaryZC_in_g(T282))
U22_ag(T282, binaryZC_out_g(T282)) → succZK_out_ag(zero(T282), one(T282))
succZK_in_ag(one(T290), zero(T289)) → U23_ag(T290, T289, succJ_in_ag(T290, T289))
succJ_in_ag(b, one(b)) → succJ_out_ag(b, one(b))
succJ_in_ag(zero(T295), one(T295)) → U20_ag(T295, binaryZC_in_g(T295))
U20_ag(T295, binaryZC_out_g(T295)) → succJ_out_ag(zero(T295), one(T295))
succJ_in_ag(one(T303), zero(T302)) → U21_ag(T303, T302, succJ_in_ag(T303, T302))
U21_ag(T303, T302, succJ_out_ag(T303, T302)) → succJ_out_ag(one(T303), zero(T302))
U23_ag(T290, T289, succJ_out_ag(T290, T289)) → succZK_out_ag(one(T290), zero(T289))
U32_aag(T276, T275, succZK_out_ag(T276, T275)) → addcI_out_aag(T276, b, T275)
addcI_in_aag(b, T314, T313) → U33_aag(T314, T313, succZK_in_ag(T314, T313))
U33_aag(T314, T313, succZK_out_ag(T314, T313)) → addcI_out_aag(b, T314, T313)
addcI_in_aag(T330, T331, T329) → U34_aag(T330, T331, T329, addCL_in_aag(T330, T331, T329))
addCL_in_aag(zero(T350), zero(T351), one(T349)) → U24_aag(T350, T351, T349, addzF_in_aag(T350, T351, T349))
U24_aag(T350, T351, T349, addzF_out_aag(T350, T351, T349)) → addCL_out_aag(zero(T350), zero(T351), one(T349))
addCL_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U25_aag(T377, binaryZC_in_g(T377))
U25_aag(T377, binaryZC_out_g(T377)) → addCL_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCL_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U26_aag(T389, T388, succJ_in_ag(T389, T388))
U26_aag(T389, T388, succJ_out_ag(T389, T388)) → addCL_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCL_in_aag(zero(T404), one(T405), zero(T403)) → U27_aag(T404, T405, T403, addCL_in_aag(T404, T405, T403))
addCL_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U28_aag(T431, binaryZC_in_g(T431))
U28_aag(T431, binaryZC_out_g(T431)) → addCL_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCL_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U29_aag(T443, T442, succJ_in_ag(T443, T442))
U29_aag(T443, T442, succJ_out_ag(T443, T442)) → addCL_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCL_in_aag(one(T458), zero(T459), zero(T457)) → U30_aag(T458, T459, T457, addCL_in_aag(T458, T459, T457))
addCL_in_aag(one(T472), one(T473), one(T471)) → U31_aag(T472, T473, T471, addcI_in_aag(T472, T473, T471))
U31_aag(T472, T473, T471, addcI_out_aag(T472, T473, T471)) → addCL_out_aag(one(T472), one(T473), one(T471))
U30_aag(T458, T459, T457, addCL_out_aag(T458, T459, T457)) → addCL_out_aag(one(T458), zero(T459), zero(T457))
U27_aag(T404, T405, T403, addCL_out_aag(T404, T405, T403)) → addCL_out_aag(zero(T404), one(T405), zero(T403))
U34_aag(T330, T331, T329, addCL_out_aag(T330, T331, T329)) → addcI_out_aag(T330, T331, T329)
U19_aag(T264, T265, T263, addcI_out_aag(T264, T265, T263)) → addzF_out_aag(one(T264), one(T265), zero(T263))
U40_aag(T250, T251, T249, addzF_out_aag(T250, T251, T249)) → addyH_out_aag(T250, T251, T249)
U18_aag(T222, T223, T221, addyH_out_aag(T222, T223, T221)) → addzF_out_aag(one(T222), zero(T223), one(T221))
U37_aag(T202, T203, T201, addzF_out_aag(T202, T203, T201)) → addxG_out_aag(T202, T203, T201)
U17_aag(T174, T175, T173, addxG_out_aag(T174, T175, T173)) → addzF_out_aag(zero(T174), one(T175), one(T173))
U16_aag(T154, T155, T153, addzF_out_aag(T154, T155, T153)) → addzF_out_aag(zero(T154), zero(T155), zero(T153))
U41_aag(T134, T135, T133, addzF_out_aag(T134, T135, T133)) → addzE_out_aag(zero(T134), zero(T135), zero(T133))
addzE_in_aag(zero(T489), one(T490), one(T488)) → U42_aag(T489, T490, T488, addxG_in_aag(T489, T490, T488))
U42_aag(T489, T490, T488, addxG_out_aag(T489, T490, T488)) → addzE_out_aag(zero(T489), one(T490), one(T488))
addzE_in_aag(one(T507), zero(T508), one(T506)) → U43_aag(T507, T508, T506, addyH_in_aag(T507, T508, T506))
U43_aag(T507, T508, T506, addyH_out_aag(T507, T508, T506)) → addzE_out_aag(one(T507), zero(T508), one(T506))
addzE_in_aag(one(T519), one(T520), zero(T518)) → U44_aag(T519, T520, T518, addcI_in_aag(T519, T520, T518))
U44_aag(T519, T520, T518, addcI_out_aag(T519, T520, T518)) → addzE_out_aag(one(T519), one(T520), zero(T518))
U4_aag(T114, T115, T113, addzE_out_aag(T114, T115, T113)) → addA_out_aag(T114, T115, T113)
addA_in_aag(b, zero(T527), zero(T527)) → U5_aag(T527, binaryZC_in_g(T527))
U5_aag(T527, binaryZC_out_g(T527)) → addA_out_aag(b, zero(T527), zero(T527))
addA_in_aag(b, one(T533), one(T533)) → U6_aag(T533, binaryD_in_g(T533))
U6_aag(T533, binaryD_out_g(T533)) → addA_out_aag(b, one(T533), one(T533))
addA_in_aag(T548, T549, T547) → U7_aag(T548, T549, T547, addzE_in_aag(T548, T549, T547))
U7_aag(T548, T549, T547, addzE_out_aag(T548, T549, T547)) → addA_out_aag(T548, T549, T547)
addA_in_aag(zero(T576), zero(T577), zero(T575)) → U8_aag(T576, T577, T575, addzF_in_aag(T576, T577, T575))
U8_aag(T576, T577, T575, addzF_out_aag(T576, T577, T575)) → addA_out_aag(zero(T576), zero(T577), zero(T575))
addA_in_aag(zero(T596), one(T597), one(T595)) → U9_aag(T596, T597, T595, addxG_in_aag(T596, T597, T595))
U9_aag(T596, T597, T595, addxG_out_aag(T596, T597, T595)) → addA_out_aag(zero(T596), one(T597), one(T595))
addA_in_aag(one(T614), zero(T615), one(T613)) → U10_aag(T614, T615, T613, addyH_in_aag(T614, T615, T613))
U10_aag(T614, T615, T613, addyH_out_aag(T614, T615, T613)) → addA_out_aag(one(T614), zero(T615), one(T613))
addA_in_aag(one(T626), one(T627), zero(T625)) → U11_aag(T626, T627, T625, addcI_in_aag(T626, T627, T625))
U11_aag(T626, T627, T625, addcI_out_aag(T626, T627, T625)) → addA_out_aag(one(T626), one(T627), zero(T625))

(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_AAG(T202, T203, T201) → ADDZF_IN_AAG(T202, T203, T201)
ADDZF_IN_AAG(zero(T154), zero(T155), zero(T153)) → ADDZF_IN_AAG(T154, T155, T153)
ADDZF_IN_AAG(zero(T174), one(T175), one(T173)) → ADDXG_IN_AAG(T174, T175, T173)
ADDZF_IN_AAG(one(T222), zero(T223), one(T221)) → ADDYH_IN_AAG(T222, T223, T221)
ADDYH_IN_AAG(T250, T251, T249) → ADDZF_IN_AAG(T250, T251, T249)
ADDZF_IN_AAG(one(T264), one(T265), zero(T263)) → ADDCI_IN_AAG(T264, T265, T263)
ADDCI_IN_AAG(T330, T331, T329) → ADDCL_IN_AAG(T330, T331, T329)
ADDCL_IN_AAG(zero(T350), zero(T351), one(T349)) → ADDZF_IN_AAG(T350, T351, T349)
ADDCL_IN_AAG(zero(T404), one(T405), zero(T403)) → ADDCL_IN_AAG(T404, T405, T403)
ADDCL_IN_AAG(one(T458), zero(T459), zero(T457)) → ADDCL_IN_AAG(T458, T459, T457)
ADDCL_IN_AAG(one(T472), one(T473), one(T471)) → ADDCI_IN_AAG(T472, T473, T471)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
ADDZF_IN_AAG(x1, x2, x3) = ADDZF_IN_AAG(x3)
ADDXG_IN_AAG(x1, x2, x3) = ADDXG_IN_AAG(x3)
ADDYH_IN_AAG(x1, x2, x3) = ADDYH_IN_AAG(x3)
ADDCI_IN_AAG(x1, x2, x3) = ADDCI_IN_AAG(x3)
ADDCL_IN_AAG(x1, x2, x3) = ADDCL_IN_AAG(x3)

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_AAG(T201) → ADDZF_IN_AAG(T201)
ADDZF_IN_AAG(zero(T153)) → ADDZF_IN_AAG(T153)
ADDZF_IN_AAG(one(T173)) → ADDXG_IN_AAG(T173)
ADDZF_IN_AAG(one(T221)) → ADDYH_IN_AAG(T221)
ADDYH_IN_AAG(T249) → ADDZF_IN_AAG(T249)
ADDZF_IN_AAG(zero(T263)) → ADDCI_IN_AAG(T263)
ADDCI_IN_AAG(T329) → ADDCL_IN_AAG(T329)
ADDCL_IN_AAG(one(T349)) → ADDZF_IN_AAG(T349)
ADDCL_IN_AAG(zero(T403)) → ADDCL_IN_AAG(T403)
ADDCL_IN_AAG(one(T471)) → ADDCI_IN_AAG(T471)

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_AAG(one(T173)) → ADDXG_IN_AAG(T173)
The graph contains the following edges 1 > 1
ADDZF_IN_AAG(zero(T153)) → ADDZF_IN_AAG(T153)
The graph contains the following edges 1 > 1
ADDXG_IN_AAG(T201) → ADDZF_IN_AAG(T201)
The graph contains the following edges 1 >= 1
ADDYH_IN_AAG(T249) → ADDZF_IN_AAG(T249)
The graph contains the following edges 1 >= 1
ADDCL_IN_AAG(one(T349)) → ADDZF_IN_AAG(T349)
The graph contains the following edges 1 > 1
ADDZF_IN_AAG(one(T221)) → ADDYH_IN_AAG(T221)
The graph contains the following edges 1 > 1
ADDZF_IN_AAG(zero(T263)) → ADDCI_IN_AAG(T263)
The graph contains the following edges 1 > 1
ADDCI_IN_AAG(T329) → ADDCL_IN_AAG(T329)
The graph contains the following edges 1 >= 1
ADDCL_IN_AAG(one(T471)) → ADDCI_IN_AAG(T471)
The graph contains the following edges 1 > 1
ADDCL_IN_AAG(zero(T403)) → ADDCL_IN_AAG(T403)
The graph contains the following edges 1 > 1

(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