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

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

↳3 PrologToPiTRSProof (⇐)

↳4 PiTRS

↳5 DependencyPairsProof (⇔)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇔)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇐)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔)

        ↳22 YES

    ↳23 PiDP

        ↳24 UsableRulesProof (⇔)

        ↳25 PiDP

        ↳26 PiDPToQDPProof (⇐)

        ↳27 QDP

        ↳28 QDPSizeChangeProof (⇔)

        ↳29 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)).

Queries:

add(g,g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: add(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: add(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | add(b, b, T3), SCOPE: 1, CLAUSE: 1 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: add(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nadd(T1, T2, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: add(b, b, T3), SCOPE: 1, CLAUSE: 1 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: binaryZ(b) | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: binaryZ(b), SCOPE: 2, CLAUSE: 31 | binaryZ(b), SCOPE: 2, CLAUSE: 32 | ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: binaryZ(b), SCOPE: 2, CLAUSE: 32 | ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ?_2 | add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: add(b, b, T3), SCOPE: 1, CLAUSE: 2 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: add(b, b, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: binaryZ(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: binaryZ(b), SCOPE: 3, CLAUSE: 31 | binaryZ(b), SCOPE: 3, CLAUSE: 32\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: binaryZ(b), SCOPE: 3, CLAUSE: 32\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: addz(b, b, T8)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: addz(b, b, T8), SCOPE: 4, CLAUSE: 10 | addz(b, b, T8), SCOPE: 4, CLAUSE: 11 | addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: addz(b, b, T8), SCOPE: 4, CLAUSE: 11 | addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: addz(b, b, T8), SCOPE: 4, CLAUSE: 12 | addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: addz(b, b, T8), SCOPE: 4, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: binaryZ(b) | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nadd(b, b, T3) !=? add(X2, b, X2)\nadd(b, b, T3) !=? add(b, X62, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: binaryZ(b), SCOPE: 5, CLAUSE: 31 | binaryZ(b), SCOPE: 5, CLAUSE: 32 | ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: binaryZ(b), SCOPE: 5, CLAUSE: 32 | ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ?_5 | add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: add(b, b, T3), SCOPE: 1, CLAUSE: 3\n\nadd(b, b, T3) !=? add(X2, b, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: addz(b, b, T13)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: addz(b, b, T16)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: addz(b, b, T16), SCOPE: 6, CLAUSE: 10 | addz(b, b, T16), SCOPE: 6, CLAUSE: 11 | addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: addz(b, b, T16), SCOPE: 6, CLAUSE: 11 | addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: addz(b, b, T16), SCOPE: 6, CLAUSE: 12 | addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: addz(b, b, T16), SCOPE: 6, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: binaryZ(T18) | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: add(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nadd(T1, T2, T3) !=? add(b, b, b)\nadd(T1, T2, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: binaryZ(T18), SCOPE: 7, CLAUSE: 31 | binaryZ(T18), SCOPE: 7, CLAUSE: 32 | ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: binaryZ(T18), SCOPE: 7, CLAUSE: 31\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: binaryZ(T18), SCOPE: 7, CLAUSE: 32 | ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: binaryZ(T23)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: binaryZ(T23), SCOPE: 8, CLAUSE: 31 | binaryZ(T23), SCOPE: 8, CLAUSE: 32\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: binaryZ(T23), SCOPE: 8, CLAUSE: 31\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: binaryZ(T23), SCOPE: 8, CLAUSE: 32\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: binaryZ(T29)\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: binary(T33)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: binary(T33), SCOPE: 9, CLAUSE: 28 | binary(T33), SCOPE: 9, CLAUSE: 29 | binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: binary(T33), SCOPE: 9, CLAUSE: 28\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: binary(T33), SCOPE: 9, CLAUSE: 29 | binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: binary(T33), SCOPE: 9, CLAUSE: 29\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: binary(T33), SCOPE: 9, CLAUSE: 30\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: binaryZ(T38)\n\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: binary(T42)\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: binaryZ(T18), SCOPE: 7, CLAUSE: 32\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ?_7 | add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: binary(T47)\n\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: add(T18, b, T3), SCOPE: 1, CLAUSE: 2 | add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: add(T18, b, T3), SCOPE: 1, CLAUSE: 2\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: add(T18, b, T3), SCOPE: 1, CLAUSE: 3\n\nT18 is ground\nadd(T18, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: binaryZ(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: addz(T57, b, T59)\n\nT57 is ground\nadd(T57, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: addz(T57, b, T59), SCOPE: 10, CLAUSE: 10 | addz(T57, b, T59), SCOPE: 10, CLAUSE: 11 | addz(T57, b, T59), SCOPE: 10, CLAUSE: 12 | addz(T57, b, T59), SCOPE: 10, CLAUSE: 13\n\nT57 is ground\nadd(T57, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: addz(T57, b, T59), SCOPE: 10, CLAUSE: 11 | addz(T57, b, T59), SCOPE: 10, CLAUSE: 12 | addz(T57, b, T59), SCOPE: 10, CLAUSE: 13\n\nT57 is ground\nadd(T57, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: addz(T57, b, T59), SCOPE: 10, CLAUSE: 12 | addz(T57, b, T59), SCOPE: 10, CLAUSE: 13\n\nT57 is ground\nadd(T57, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: addz(T57, b, T59), SCOPE: 10, CLAUSE: 13\n\nT57 is ground\nadd(T57, b, T3) !=? add(b, b, b)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: binaryZ(T69) | add(b, T69, T3), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nadd(b, T69, T3) !=? add(b, b, b)\nadd(b, T69, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: add(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nadd(T1, T2, T3) !=? add(b, b, b)\nadd(T1, T2, T3) !=? add(X118, b, X118)\nadd(T1, T2, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: binaryZ(T69), SCOPE: 11, CLAUSE: 31 | binaryZ(T69), SCOPE: 11, CLAUSE: 32 | ?_11 | add(b, T69, T3), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nadd(b, T69, T3) !=? add(b, b, b)\nadd(b, T69, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: binaryZ(T69), SCOPE: 11, CLAUSE: 31\n\nT69 is ground\nadd(b, T69, T3) !=? add(b, b, b)\nadd(b, T69, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: binaryZ(T69), SCOPE: 11, CLAUSE: 32 | ?_11 | add(b, T69, T3), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nadd(b, T69, T3) !=? add(b, b, b)\nadd(b, T69, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: binaryZ(T74)\n\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: binaryZ(T69), SCOPE: 11, CLAUSE: 32\n\nT69 is ground\nadd(b, T69, T3) !=? add(b, b, b)\nadd(b, T69, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ?_11 | add(b, T69, T3), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nadd(b, T69, T3) !=? add(b, b, b)\nadd(b, T69, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: binary(T80)\n\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: add(b, T69, T3), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nadd(b, T69, T3) !=? add(b, b, b)\nadd(b, T69, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: addz(b, T86, T88)\n\nT86 is ground\nadd(b, T86, T3) !=? add(b, b, b)\nadd(b, T86, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: addz(b, T86, T88), SCOPE: 12, CLAUSE: 10 | addz(b, T86, T88), SCOPE: 12, CLAUSE: 11 | addz(b, T86, T88), SCOPE: 12, CLAUSE: 12 | addz(b, T86, T88), SCOPE: 12, CLAUSE: 13\n\nT86 is ground\nadd(b, T86, T3) !=? add(b, b, b)\nadd(b, T86, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: addz(b, T86, T88), SCOPE: 12, CLAUSE: 11 | addz(b, T86, T88), SCOPE: 12, CLAUSE: 12 | addz(b, T86, T88), SCOPE: 12, CLAUSE: 13\n\nT86 is ground\nadd(b, T86, T3) !=? add(b, b, b)\nadd(b, T86, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: addz(b, T86, T88), SCOPE: 12, CLAUSE: 12 | addz(b, T86, T88), SCOPE: 12, CLAUSE: 13\n\nT86 is ground\nadd(b, T86, T3) !=? add(b, b, b)\nadd(b, T86, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: addz(b, T86, T88), SCOPE: 12, CLAUSE: 13\n\nT86 is ground\nadd(b, T86, T3) !=? add(b, b, b)\nadd(b, T86, T3) !=? add(X118, b, X118)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: addz(T92, T93, T95)\n\nT92 is ground\nT93 is ground\nadd(T92, T93, T3) !=? add(b, b, b)\nadd(T92, T93, T3) !=? add(X118, b, X118)\nadd(T92, T93, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: addz(T92, T93, T95), SCOPE: 13, CLAUSE: 10 | addz(T92, T93, T95), SCOPE: 13, CLAUSE: 11 | addz(T92, T93, T95), SCOPE: 13, CLAUSE: 12 | addz(T92, T93, T95), SCOPE: 13, CLAUSE: 13\n\nT92 is ground\nT93 is ground\nadd(T92, T93, T3) !=? add(b, b, b)\nadd(T92, T93, T3) !=? add(X118, b, X118)\nadd(T92, T93, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: addz(T92, T93, T95), SCOPE: 13, CLAUSE: 10\n\nT92 is ground\nT93 is ground\nadd(T92, T93, T3) !=? add(b, b, b)\nadd(T92, T93, T3) !=? add(X118, b, X118)\nadd(T92, T93, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: addz(T92, T93, T95), SCOPE: 13, CLAUSE: 11 | addz(T92, T93, T95), SCOPE: 13, CLAUSE: 12 | addz(T92, T93, T95), SCOPE: 13, CLAUSE: 13\n\nT92 is ground\nT93 is ground\nadd(T92, T93, T3) !=? add(b, b, b)\nadd(T92, T93, T3) !=? add(X118, b, X118)\nadd(T92, T93, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: addz(T108, T109, T111)\n\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: addz(T108, T109, T111), SCOPE: 14, CLAUSE: 10 | addz(T108, T109, T111), SCOPE: 14, CLAUSE: 11 | addz(T108, T109, T111), SCOPE: 14, CLAUSE: 12 | addz(T108, T109, T111), SCOPE: 14, CLAUSE: 13\n\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: addz(T108, T109, T111), SCOPE: 14, CLAUSE: 10\n\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: addz(T108, T109, T111), SCOPE: 14, CLAUSE: 11 | addz(T108, T109, T111), SCOPE: 14, CLAUSE: 12 | addz(T108, T109, T111), SCOPE: 14, CLAUSE: 13\n\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: addz(T127, T128, T130)\n\nT127 is ground\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: addz(T108, T109, T111), SCOPE: 14, CLAUSE: 11\n\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: addz(T108, T109, T111), SCOPE: 14, CLAUSE: 12 | addz(T108, T109, T111), SCOPE: 14, CLAUSE: 13\n\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: addx(T146, T147, T149)\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: addx(T146, T147, T149), SCOPE: 15, CLAUSE: 4 | addx(T146, T147, T149), SCOPE: 15, CLAUSE: 5 | addx(T146, T147, T149), SCOPE: 15, CLAUSE: 6\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: addx(T146, T147, T149), SCOPE: 15, CLAUSE: 4\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: addx(T146, T147, T149), SCOPE: 15, CLAUSE: 5 | addx(T146, T147, T149), SCOPE: 15, CLAUSE: 6\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: binary(T155)\n\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: addx(T146, T147, T149), SCOPE: 15, CLAUSE: 5\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: addx(T146, T147, T149), SCOPE: 15, CLAUSE: 6\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: binaryZ(T160)\n\nT160 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: addz(T172, T173, T175)\n\nT172 is ground\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: addz(T108, T109, T111), SCOPE: 14, CLAUSE: 12\n\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: addz(T108, T109, T111), SCOPE: 14, CLAUSE: 13\n\nT108 is ground\nT109 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: addy(T191, T192, T194)\n\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: addy(T191, T192, T194), SCOPE: 16, CLAUSE: 7 | addy(T191, T192, T194), SCOPE: 16, CLAUSE: 8 | addy(T191, T192, T194), SCOPE: 16, CLAUSE: 9\n\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: addy(T191, T192, T194), SCOPE: 16, CLAUSE: 7\n\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: addy(T191, T192, T194), SCOPE: 16, CLAUSE: 8 | addy(T191, T192, T194), SCOPE: 16, CLAUSE: 9\n\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: binary(T200)\n\nT200 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: addy(T191, T192, T194), SCOPE: 16, CLAUSE: 8\n\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: addy(T191, T192, T194), SCOPE: 16, CLAUSE: 9\n\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: binaryZ(T205)\n\nT205 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: addz(T217, T218, T220)\n\nT217 is ground\nT218 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: addc(T230, T231, T233)\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: addc(T230, T231, T233), SCOPE: 17, CLAUSE: 14 | addc(T230, T231, T233), SCOPE: 17, CLAUSE: 15 | addc(T230, T231, T233), SCOPE: 17, CLAUSE: 16 | addc(T230, T231, T233), SCOPE: 17, CLAUSE: 17\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: addc(T230, T231, T233), SCOPE: 17, CLAUSE: 14\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: addc(T230, T231, T233), SCOPE: 17, CLAUSE: 15 | addc(T230, T231, T233), SCOPE: 17, CLAUSE: 16 | addc(T230, T231, T233), SCOPE: 17, CLAUSE: 17\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: addc(T230, T231, T233), SCOPE: 17, CLAUSE: 15\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: addc(T230, T231, T233), SCOPE: 17, CLAUSE: 16 | addc(T230, T231, T233), SCOPE: 17, CLAUSE: 17\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: succZ(T242, T244)\n\nT242 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: succZ(T242, T244), SCOPE: 18, CLAUSE: 36 | succZ(T242, T244), SCOPE: 18, CLAUSE: 37\n\nT242 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: succZ(T242, T244), SCOPE: 18, CLAUSE: 36\n\nT242 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: succZ(T242, T244), SCOPE: 18, CLAUSE: 37\n\nT242 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: binaryZ(T250)\n\nT250 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: succ(T256, T258)\n\nT256 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: succ(T256, T258), SCOPE: 19, CLAUSE: 33 | succ(T256, T258), SCOPE: 19, CLAUSE: 34 | succ(T256, T258), SCOPE: 19, CLAUSE: 35\n\nT256 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: succ(T256, T258), SCOPE: 19, CLAUSE: 33\n\nT256 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: succ(T256, T258), SCOPE: 19, CLAUSE: 34 | succ(T256, T258), SCOPE: 19, CLAUSE: 35\n\nT256 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: succ(T256, T258), SCOPE: 19, CLAUSE: 34\n\nT256 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: succ(T256, T258), SCOPE: 19, CLAUSE: 35\n\nT256 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: binaryZ(T263)\n\nT263 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: succ(T269, T271)\n\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: addc(T230, T231, T233), SCOPE: 17, CLAUSE: 16\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: addc(T230, T231, T233), SCOPE: 17, CLAUSE: 17\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: succZ(T280, T282)\n\nT280 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: addC(T294, T295, T297)\n\nT294 is ground\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: addC(T294, T295, T297), SCOPE: 20, CLAUSE: 24 | addC(T294, T295, T297), SCOPE: 20, CLAUSE: 25 | addC(T294, T295, T297), SCOPE: 20, CLAUSE: 26 | addC(T294, T295, T297), SCOPE: 20, CLAUSE: 27\n\nT294 is ground\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: addC(T294, T295, T297), SCOPE: 20, CLAUSE: 24\n\nT294 is ground\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: addC(T294, T295, T297), SCOPE: 20, CLAUSE: 25 | addC(T294, T295, T297), SCOPE: 20, CLAUSE: 26 | addC(T294, T295, T297), SCOPE: 20, CLAUSE: 27\n\nT294 is ground\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: addz(T313, T314, T316)\n\nT313 is ground\nT314 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: addC(T294, T295, T297), SCOPE: 20, CLAUSE: 25\n\nT294 is ground\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: addC(T294, T295, T297), SCOPE: 20, CLAUSE: 26 | addC(T294, T295, T297), SCOPE: 20, CLAUSE: 27\n\nT294 is ground\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: addX(T332, T333, T335)\n\nT332 is ground\nT333 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: addX(T332, T333, T335), SCOPE: 21, CLAUSE: 18 | addX(T332, T333, T335), SCOPE: 21, CLAUSE: 19 | addX(T332, T333, T335), SCOPE: 21, CLAUSE: 20\n\nT332 is ground\nT333 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: addX(T332, T333, T335), SCOPE: 21, CLAUSE: 18\n\nT332 is ground\nT333 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: addX(T332, T333, T335), SCOPE: 21, CLAUSE: 19 | addX(T332, T333, T335), SCOPE: 21, CLAUSE: 20\n\nT332 is ground\nT333 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: binaryZ(T341)\n\nT341 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: addX(T332, T333, T335), SCOPE: 21, CLAUSE: 19\n\nT332 is ground\nT333 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: addX(T332, T333, T335), SCOPE: 21, CLAUSE: 20\n\nT332 is ground\nT333 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: succ(T351, T353)\n\nT351 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: addC(T364, T365, T367)\n\nT364 is ground\nT365 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: addC(T294, T295, T297), SCOPE: 20, CLAUSE: 26\n\nT294 is ground\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: addC(T294, T295, T297), SCOPE: 20, CLAUSE: 27\n\nT294 is ground\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: addY(T383, T384, T386)\n\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: addY(T383, T384, T386), SCOPE: 22, CLAUSE: 21 | addY(T383, T384, T386), SCOPE: 22, CLAUSE: 22 | addY(T383, T384, T386), SCOPE: 22, CLAUSE: 23\n\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: addY(T383, T384, T386), SCOPE: 22, CLAUSE: 21\n\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: addY(T383, T384, T386), SCOPE: 22, CLAUSE: 22 | addY(T383, T384, T386), SCOPE: 22, CLAUSE: 23\n\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: binaryZ(T392)\n\nT392 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: addY(T383, T384, T386), SCOPE: 22, CLAUSE: 22\n\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: addY(T383, T384, T386), SCOPE: 22, CLAUSE: 23\n\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: succ(T402, T404)\n\nT402 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: addC(T415, T416, T418)\n\nT415 is ground\nT416 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: addc(T428, T429, T431)\n\nT428 is ground\nT429 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: addz(T92, T93, T95), SCOPE: 13, CLAUSE: 11\n\nT92 is ground\nT93 is ground\nadd(T92, T93, T3) !=? add(b, b, b)\nadd(T92, T93, T3) !=? add(X118, b, X118)\nadd(T92, T93, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: addz(T92, T93, T95), SCOPE: 13, CLAUSE: 12 | addz(T92, T93, T95), SCOPE: 13, CLAUSE: 13\n\nT92 is ground\nT93 is ground\nadd(T92, T93, T3) !=? add(b, b, b)\nadd(T92, T93, T3) !=? add(X118, b, X118)\nadd(T92, T93, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: addx(T444, T445, T447)\n\nT444 is ground\nT445 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: addz(T92, T93, T95), SCOPE: 13, CLAUSE: 12\n\nT92 is ground\nT93 is ground\nadd(T92, T93, T3) !=? add(b, b, b)\nadd(T92, T93, T3) !=? add(X118, b, X118)\nadd(T92, T93, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: addz(T92, T93, T95), SCOPE: 13, CLAUSE: 13\n\nT92 is ground\nT93 is ground\nadd(T92, T93, T3) !=? add(b, b, b)\nadd(T92, T93, T3) !=? add(X118, b, X118)\nadd(T92, T93, T3) !=? add(b, X209, X209)", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: addy(T461, T462, T464)\n\nT461 is ground\nT462 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: addc(T472, T473, T475)\n\nT472 is ground\nT473 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 217 [arrowhead = none ];
217 -> 2;

218 [label="EVAL with clause\nadd(b, b, b).\nand substitution\nT1 -> b\nT2 -> b\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 218 [arrowhead = none ];
218 -> 3;

219 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 219 [arrowhead = none ];
219 -> 4;

220 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 220 [arrowhead = none ];
220 -> 5;

221 [label="EVAL with clause\nadd(X118, b, X118) :- binaryZ(X118).\nand substitution\nT1 -> T18\nX118 -> T18\nT2 -> b\nT3 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 221 [arrowhead = none ];
221 -> 38;

222 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 222 [arrowhead = none ];
222 -> 39;

223 [label="EVAL with clause\nadd(X2, b, X2) :- binaryZ(X2).\nand substitution\nX2 -> b\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 223 [arrowhead = none ];
223 -> 6;

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

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

226 [label="EVAL with clause\nadd(b, X62, X62) :- binaryZ(X62).\nand substitution\nX62 -> b\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 226 [arrowhead = none ];
226 -> 25;

227 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 227 [arrowhead = none ];
227 -> 26;

228 [label="BACKTRACK\nfor clause: binaryZ(zero(X)) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
8 -> 228 [arrowhead = none ];
228 -> 9;

229 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
9 -> 229 [arrowhead = none ];
229 -> 10;

230 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 230 [arrowhead = none ];
230 -> 11;

231 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 231 [arrowhead = none ];
231 -> 12;

232 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
11 -> 232 [arrowhead = none ];
232 -> 13;

233 [label="EVAL with clause\nadd(b, X10, X10) :- binaryZ(X10).\nand substitution\nX10 -> b\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 233 [arrowhead = none ];
233 -> 14;

234 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 234 [arrowhead = none ];
234 -> 15;

235 [label="ONLY EVAL with clause\nadd(X34, X35, X36) :- addz(X34, X35, X36).\nand substitution\nX34 -> b\nX35 -> b\nT3 -> T8\nX36 -> T8\nT7 -> T8", fontsize=14, style = filled, fillcolor = white];
13 -> 235 [arrowhead = none ];
235 -> 19;

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

237 [label="BACKTRACK\nfor clause: binaryZ(zero(X)) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
16 -> 237 [arrowhead = none ];
237 -> 17;

238 [label="BACKTRACK\nfor clause: binaryZ(one(X)) :- binary(X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
17 -> 238 [arrowhead = none ];
238 -> 18;

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

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

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

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

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

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

245 [label="ONLY EVAL with clause\nadd(X102, X103, X104) :- addz(X102, X103, X104).\nand substitution\nX102 -> b\nX103 -> b\nT3 -> T16\nX104 -> T16\nT15 -> T16", fontsize=14, style = filled, fillcolor = white];
26 -> 245 [arrowhead = none ];
245 -> 32;

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

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

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

249 [label="ONLY EVAL with clause\nadd(X84, X85, X86) :- addz(X84, X85, X86).\nand substitution\nX84 -> b\nX85 -> b\nT3 -> T13\nX86 -> T13\nT12 -> T13", fontsize=14, style = filled, fillcolor = white];
30 -> 249 [arrowhead = none ];
249 -> 31;

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

251 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 251 [arrowhead = none ];
251 -> 33;

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

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

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

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

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

257 [label="EVAL with clause\nadd(b, X209, X209) :- binaryZ(X209).\nand substitution\nT1 -> b\nT2 -> T69\nX209 -> T69\nT3 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 257 [arrowhead = none ];
257 -> 79;

258 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 258 [arrowhead = none ];
258 -> 80;

259 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 259 [arrowhead = none ];
259 -> 41;

260 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 260 [arrowhead = none ];
260 -> 42;

261 [label="EVAL with clause\nbinaryZ(zero(X124)) :- binaryZ(X124).\nand substitution\nX124 -> T23\nT18 -> zero(T23)", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 261 [arrowhead = none ];
261 -> 43;

262 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 262 [arrowhead = none ];
262 -> 44;

263 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 263 [arrowhead = none ];
263 -> 64;

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 264 [arrowhead = none ];
264 -> 65;

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

266 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 266 [arrowhead = none ];
266 -> 46;

267 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 267 [arrowhead = none ];
267 -> 47;

268 [label="EVAL with clause\nbinaryZ(zero(X131)) :- binaryZ(X131).\nand substitution\nX131 -> T29\nT23 -> zero(T29)", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 268 [arrowhead = none ];
268 -> 48;

269 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 269 [arrowhead = none ];
269 -> 49;

270 [label="EVAL with clause\nbinaryZ(one(X136)) :- binary(X136).\nand substitution\nX136 -> T33\nT23 -> one(T33)", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 270 [arrowhead = none ];
270 -> 50;

271 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 271 [arrowhead = none ];
271 -> 51;

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

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

274 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 274 [arrowhead = none ];
274 -> 53;

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

276 [label="EVAL with clause\nbinary(b).\nand substitution\nT33 -> b", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 276 [arrowhead = none ];
276 -> 55;

277 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 277 [arrowhead = none ];
277 -> 56;

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

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

280 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 280 [arrowhead = none ];
280 -> 57;

281 [label="EVAL with clause\nbinary(zero(X142)) :- binaryZ(X142).\nand substitution\nX142 -> T38\nT33 -> zero(T38)", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 281 [arrowhead = none ];
281 -> 60;

282 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 282 [arrowhead = none ];
282 -> 61;

283 [label="EVAL with clause\nbinary(one(X147)) :- binary(X147).\nand substitution\nX147 -> T42\nT33 -> one(T42)", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 283 [arrowhead = none ];
283 -> 62;

284 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 284 [arrowhead = none ];
284 -> 63;

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

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

287 [label="EVAL with clause\nbinaryZ(one(X153)) :- binary(X153).\nand substitution\nX153 -> T47\nT18 -> one(T47)", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 287 [arrowhead = none ];
287 -> 66;

288 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 288 [arrowhead = none ];
288 -> 67;

289 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 289 [arrowhead = none ];
289 -> 68;

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

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

292 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 292 [arrowhead = none ];
292 -> 70;

293 [label="EVAL with clause\nadd(b, X159, X159) :- binaryZ(X159).\nand substitution\nT18 -> b\nX159 -> b\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 293 [arrowhead = none ];
293 -> 71;

294 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 294 [arrowhead = none ];
294 -> 72;

295 [label="ONLY EVAL with clause\nadd(X181, X182, X183) :- addz(X181, X182, X183).\nand substitution\nT18 -> T57\nX181 -> T57\nX182 -> b\nT3 -> T59\nX183 -> T59\nT58 -> T59", fontsize=14, style = filled, fillcolor = white];
70 -> 295 [arrowhead = none ];
295 -> 73;

296 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 296 [arrowhead = none , style=dashed];
296 -> 14[style=dashed];

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

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

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

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

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

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

303 [label="ONLY EVAL with clause\nadd(X272, X273, X274) :- addz(X272, X273, X274).\nand substitution\nT1 -> T92\nX272 -> T92\nT2 -> T93\nX273 -> T93\nT3 -> T95\nX274 -> T95\nT94 -> T95", fontsize=14, style = filled, fillcolor = white];
80 -> 303 [arrowhead = none ];
303 -> 97;

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

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

306 [label="EVAL with clause\nbinaryZ(zero(X215)) :- binaryZ(X215).\nand substitution\nX215 -> T74\nT69 -> zero(T74)", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 306 [arrowhead = none ];
306 -> 84;

307 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 307 [arrowhead = none ];
307 -> 85;

308 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 308 [arrowhead = none ];
308 -> 86;

309 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
83 -> 309 [arrowhead = none ];
309 -> 87;

310 [label="INSTANCE with matching:\nT23 -> T74", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 310 [arrowhead = none , style=dashed];
310 -> 43[style=dashed];

311 [label="EVAL with clause\nbinaryZ(one(X222)) :- binary(X222).\nand substitution\nX222 -> T80\nT69 -> one(T80)", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 311 [arrowhead = none ];
311 -> 88;

312 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 312 [arrowhead = none ];
312 -> 89;

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

314 [label="INSTANCE with matching:\nT47 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 314 [arrowhead = none , style=dashed];
314 -> 66[style=dashed];

315 [label="ONLY EVAL with clause\nadd(X242, X243, X244) :- addz(X242, X243, X244).\nand substitution\nX242 -> b\nT69 -> T86\nX243 -> T86\nT3 -> T88\nX244 -> T88\nT87 -> T88", fontsize=14, style = filled, fillcolor = white];
90 -> 315 [arrowhead = none ];
315 -> 91;

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

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

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

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

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

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

322 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 322 [arrowhead = none ];
322 -> 99;

323 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 323 [arrowhead = none ];
323 -> 100;

324 [label="EVAL with clause\naddz(zero(X287), zero(X288), zero(X289)) :- addz(X287, X288, X289).\nand substitution\nX287 -> T108\nT92 -> zero(T108)\nX288 -> T109\nT93 -> zero(T109)\nX289 -> T111\nT95 -> zero(T111)\nT110 -> T111", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 324 [arrowhead = none ];
324 -> 101;

325 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 325 [arrowhead = none ];
325 -> 102;

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

327 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
100 -> 327 [arrowhead = none ];
327 -> 208;

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

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

330 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
103 -> 330 [arrowhead = none ];
330 -> 105;

331 [label="EVAL with clause\naddz(zero(X308), zero(X309), zero(X310)) :- addz(X308, X309, X310).\nand substitution\nX308 -> T127\nT108 -> zero(T127)\nX309 -> T128\nT109 -> zero(T128)\nX310 -> T130\nT111 -> zero(T130)\nT129 -> T130", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 331 [arrowhead = none ];
331 -> 106;

332 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 332 [arrowhead = none ];
332 -> 107;

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

334 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
105 -> 334 [arrowhead = none ];
334 -> 109;

335 [label="INSTANCE with matching:\nT108 -> T127\nT109 -> T128\nT111 -> T130", fontsize=14, style = filled, fillcolor = lightgrey];
106 -> 335 [arrowhead = none , style=dashed];
335 -> 101[style=dashed];

336 [label="EVAL with clause\naddz(zero(X329), one(X330), one(X331)) :- addx(X329, X330, X331).\nand substitution\nX329 -> T146\nT108 -> zero(T146)\nX330 -> T147\nT109 -> one(T147)\nX331 -> T149\nT111 -> one(T149)\nT148 -> T149", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 336 [arrowhead = none ];
336 -> 110;

337 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 337 [arrowhead = none ];
337 -> 111;

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

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

340 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
110 -> 340 [arrowhead = none ];
340 -> 112;

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

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

343 [label="EVAL with clause\naddx(one(X340), b, one(X340)) :- binary(X340).\nand substitution\nX340 -> T155\nT146 -> one(T155)\nT147 -> b\nT149 -> one(T155)", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 343 [arrowhead = none ];
343 -> 115;

344 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 344 [arrowhead = none ];
344 -> 116;

345 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
114 -> 345 [arrowhead = none ];
345 -> 117;

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

347 [label="INSTANCE with matching:\nT47 -> T155", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 347 [arrowhead = none , style=dashed];
347 -> 66[style=dashed];

348 [label="EVAL with clause\naddx(zero(X346), b, zero(X346)) :- binaryZ(X346).\nand substitution\nX346 -> T160\nT146 -> zero(T160)\nT147 -> b\nT149 -> zero(T160)", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 348 [arrowhead = none ];
348 -> 119;

349 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 349 [arrowhead = none ];
349 -> 120;

350 [label="ONLY EVAL with clause\naddx(X358, X359, X360) :- addz(X358, X359, X360).\nand substitution\nT146 -> T172\nX358 -> T172\nT147 -> T173\nX359 -> T173\nT149 -> T175\nX360 -> T175\nT174 -> T175", fontsize=14, style = filled, fillcolor = white];
118 -> 350 [arrowhead = none ];
350 -> 121;

351 [label="INSTANCE with matching:\nT23 -> T160", fontsize=14, style = filled, fillcolor = lightgrey];
119 -> 351 [arrowhead = none , style=dashed];
351 -> 43[style=dashed];

352 [label="INSTANCE with matching:\nT108 -> T172\nT109 -> T173\nT111 -> T175", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 352 [arrowhead = none , style=dashed];
352 -> 101[style=dashed];

353 [label="EVAL with clause\naddz(one(X376), zero(X377), one(X378)) :- addy(X376, X377, X378).\nand substitution\nX376 -> T191\nT108 -> one(T191)\nX377 -> T192\nT109 -> zero(T192)\nX378 -> T194\nT111 -> one(T194)\nT193 -> T194", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 353 [arrowhead = none ];
353 -> 124;

354 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 354 [arrowhead = none ];
354 -> 125;

355 [label="EVAL with clause\naddz(one(X417), one(X418), zero(X419)) :- addc(X417, X418, X419).\nand substitution\nX417 -> T230\nT108 -> one(T230)\nX418 -> T231\nT109 -> one(T231)\nX419 -> T233\nT111 -> zero(T233)\nT232 -> T233", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 355 [arrowhead = none ];
355 -> 136;

356 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 356 [arrowhead = none ];
356 -> 137;

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

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

359 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 359 [arrowhead = none ];
359 -> 128;

360 [label="EVAL with clause\naddy(b, one(X387), one(X387)) :- binary(X387).\nand substitution\nT191 -> b\nX387 -> T200\nT192 -> one(T200)\nT194 -> one(T200)", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 360 [arrowhead = none ];
360 -> 129;

361 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 361 [arrowhead = none ];
361 -> 130;

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

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

364 [label="INSTANCE with matching:\nT47 -> T200", fontsize=14, style = filled, fillcolor = lightgrey];
129 -> 364 [arrowhead = none , style=dashed];
364 -> 66[style=dashed];

365 [label="EVAL with clause\naddy(b, zero(X393), zero(X393)) :- binaryZ(X393).\nand substitution\nT191 -> b\nX393 -> T205\nT192 -> zero(T205)\nT194 -> zero(T205)", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 365 [arrowhead = none ];
365 -> 133;

366 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 366 [arrowhead = none ];
366 -> 134;

367 [label="ONLY EVAL with clause\naddy(X405, X406, X407) :- addz(X405, X406, X407).\nand substitution\nT191 -> T217\nX405 -> T217\nT192 -> T218\nX406 -> T218\nT194 -> T220\nX407 -> T220\nT219 -> T220", fontsize=14, style = filled, fillcolor = white];
132 -> 367 [arrowhead = none ];
367 -> 135;

368 [label="INSTANCE with matching:\nT23 -> T205", fontsize=14, style = filled, fillcolor = lightgrey];
133 -> 368 [arrowhead = none , style=dashed];
368 -> 43[style=dashed];

369 [label="INSTANCE with matching:\nT108 -> T217\nT109 -> T218\nT111 -> T220", fontsize=14, style = filled, fillcolor = lightgrey];
135 -> 369 [arrowhead = none , style=dashed];
369 -> 101[style=dashed];

370 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
136 -> 370 [arrowhead = none ];
370 -> 138;

371 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 371 [arrowhead = none ];
371 -> 139;

372 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 372 [arrowhead = none ];
372 -> 140;

373 [label="EVAL with clause\naddc(b, b, one(b)).\nand substitution\nT230 -> b\nT231 -> b\nT233 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 373 [arrowhead = none ];
373 -> 141;

374 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 374 [arrowhead = none ];
374 -> 142;

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

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

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

378 [label="EVAL with clause\naddc(X431, b, X432) :- succZ(X431, X432).\nand substitution\nT230 -> T242\nX431 -> T242\nT231 -> b\nT233 -> T244\nX432 -> T244\nT243 -> T244", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 378 [arrowhead = none ];
378 -> 146;

379 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 379 [arrowhead = none ];
379 -> 147;

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

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

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

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

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

385 [label="EVAL with clause\nsuccZ(zero(X440), one(X440)) :- binaryZ(X440).\nand substitution\nX440 -> T250\nT242 -> zero(T250)\nT244 -> one(T250)", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 385 [arrowhead = none ];
385 -> 151;

386 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 386 [arrowhead = none ];
386 -> 152;

387 [label="EVAL with clause\nsuccZ(one(X447), zero(X448)) :- succ(X447, X448).\nand substitution\nX447 -> T256\nT242 -> one(T256)\nX448 -> T258\nT244 -> zero(T258)\nT257 -> T258", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 387 [arrowhead = none ];
387 -> 153;

388 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 388 [arrowhead = none ];
388 -> 154;

389 [label="INSTANCE with matching:\nT23 -> T250", fontsize=14, style = filled, fillcolor = lightgrey];
151 -> 389 [arrowhead = none , style=dashed];
389 -> 43[style=dashed];

390 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
153 -> 390 [arrowhead = none ];
390 -> 155;

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

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

393 [label="EVAL with clause\nsucc(b, one(b)).\nand substitution\nT256 -> b\nT258 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 393 [arrowhead = none ];
393 -> 158;

394 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 394 [arrowhead = none ];
394 -> 159;

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

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

397 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 397 [arrowhead = none ];
397 -> 160;

398 [label="EVAL with clause\nsucc(zero(X455), one(X455)) :- binaryZ(X455).\nand substitution\nX455 -> T263\nT256 -> zero(T263)\nT258 -> one(T263)", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 398 [arrowhead = none ];
398 -> 163;

399 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 399 [arrowhead = none ];
399 -> 164;

400 [label="EVAL with clause\nsucc(one(X462), zero(X463)) :- succ(X462, X463).\nand substitution\nX462 -> T269\nT256 -> one(T269)\nX463 -> T271\nT258 -> zero(T271)\nT270 -> T271", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 400 [arrowhead = none ];
400 -> 165;

401 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 401 [arrowhead = none ];
401 -> 166;

402 [label="INSTANCE with matching:\nT23 -> T263", fontsize=14, style = filled, fillcolor = lightgrey];
163 -> 402 [arrowhead = none , style=dashed];
402 -> 43[style=dashed];

403 [label="INSTANCE with matching:\nT256 -> T269\nT258 -> T271", fontsize=14, style = filled, fillcolor = lightgrey];
165 -> 403 [arrowhead = none , style=dashed];
403 -> 153[style=dashed];

404 [label="EVAL with clause\naddc(b, X474, X475) :- succZ(X474, X475).\nand substitution\nT230 -> b\nT231 -> T280\nX474 -> T280\nT233 -> T282\nX475 -> T282\nT281 -> T282", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 404 [arrowhead = none ];
404 -> 169;

405 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 405 [arrowhead = none ];
405 -> 170;

406 [label="ONLY EVAL with clause\naddc(X488, X489, X490) :- addC(X488, X489, X490).\nand substitution\nT230 -> T294\nX488 -> T294\nT231 -> T295\nX489 -> T295\nT233 -> T297\nX490 -> T297\nT296 -> T297", fontsize=14, style = filled, fillcolor = white];
168 -> 406 [arrowhead = none ];
406 -> 171;

407 [label="INSTANCE with matching:\nT242 -> T280\nT244 -> T282", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 407 [arrowhead = none , style=dashed];
407 -> 146[style=dashed];

408 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
171 -> 408 [arrowhead = none ];
408 -> 172;

409 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
172 -> 409 [arrowhead = none ];
409 -> 173;

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

411 [label="EVAL with clause\naddC(zero(X506), zero(X507), one(X508)) :- addz(X506, X507, X508).\nand substitution\nX506 -> T313\nT294 -> zero(T313)\nX507 -> T314\nT295 -> zero(T314)\nX508 -> T316\nT297 -> one(T316)\nT315 -> T316", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 411 [arrowhead = none ];
411 -> 175;

412 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 412 [arrowhead = none ];
412 -> 176;

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

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

415 [label="INSTANCE with matching:\nT108 -> T313\nT109 -> T314\nT111 -> T316", fontsize=14, style = filled, fillcolor = lightgrey];
175 -> 415 [arrowhead = none , style=dashed];
415 -> 101[style=dashed];

416 [label="EVAL with clause\naddC(zero(X527), one(X528), zero(X529)) :- addX(X527, X528, X529).\nand substitution\nX527 -> T332\nT294 -> zero(T332)\nX528 -> T333\nT295 -> one(T333)\nX529 -> T335\nT297 -> zero(T335)\nT334 -> T335", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 416 [arrowhead = none ];
416 -> 179;

417 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 417 [arrowhead = none ];
417 -> 180;

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

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

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

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

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

423 [label="EVAL with clause\naddX(zero(X538), b, one(X538)) :- binaryZ(X538).\nand substitution\nX538 -> T341\nT332 -> zero(T341)\nT333 -> b\nT335 -> one(T341)", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 423 [arrowhead = none ];
423 -> 184;

424 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 424 [arrowhead = none ];
424 -> 185;

425 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
183 -> 425 [arrowhead = none ];
425 -> 186;

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

427 [label="INSTANCE with matching:\nT23 -> T341", fontsize=14, style = filled, fillcolor = lightgrey];
184 -> 427 [arrowhead = none , style=dashed];
427 -> 43[style=dashed];

428 [label="EVAL with clause\naddX(one(X549), b, zero(X550)) :- succ(X549, X550).\nand substitution\nX549 -> T351\nT332 -> one(T351)\nT333 -> b\nX550 -> T353\nT335 -> zero(T353)\nT352 -> T353", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 428 [arrowhead = none ];
428 -> 188;

429 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 429 [arrowhead = none ];
429 -> 189;

430 [label="ONLY EVAL with clause\naddX(X562, X563, X564) :- addC(X562, X563, X564).\nand substitution\nT332 -> T364\nX562 -> T364\nT333 -> T365\nX563 -> T365\nT335 -> T367\nX564 -> T367\nT366 -> T367", fontsize=14, style = filled, fillcolor = white];
187 -> 430 [arrowhead = none ];
430 -> 190;

431 [label="INSTANCE with matching:\nT256 -> T351\nT258 -> T353", fontsize=14, style = filled, fillcolor = lightgrey];
188 -> 431 [arrowhead = none , style=dashed];
431 -> 153[style=dashed];

432 [label="INSTANCE with matching:\nT294 -> T364\nT295 -> T365\nT297 -> T367", fontsize=14, style = filled, fillcolor = lightgrey];
190 -> 432 [arrowhead = none , style=dashed];
432 -> 171[style=dashed];

433 [label="EVAL with clause\naddC(one(X580), zero(X581), zero(X582)) :- addY(X580, X581, X582).\nand substitution\nX580 -> T383\nT294 -> one(T383)\nX581 -> T384\nT295 -> zero(T384)\nX582 -> T386\nT297 -> zero(T386)\nT385 -> T386", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 433 [arrowhead = none ];
433 -> 193;

434 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 434 [arrowhead = none ];
434 -> 194;

435 [label="EVAL with clause\naddC(one(X627), one(X628), one(X629)) :- addc(X627, X628, X629).\nand substitution\nX627 -> T428\nT294 -> one(T428)\nX628 -> T429\nT295 -> one(T429)\nX629 -> T431\nT297 -> one(T431)\nT430 -> T431", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 435 [arrowhead = none ];
435 -> 205;

436 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 436 [arrowhead = none ];
436 -> 206;

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

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

439 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 439 [arrowhead = none ];
439 -> 197;

440 [label="EVAL with clause\naddY(b, zero(X591), one(X591)) :- binaryZ(X591).\nand substitution\nT383 -> b\nX591 -> T392\nT384 -> zero(T392)\nT386 -> one(T392)", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 440 [arrowhead = none ];
440 -> 198;

441 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 441 [arrowhead = none ];
441 -> 199;

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

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

444 [label="INSTANCE with matching:\nT23 -> T392", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 444 [arrowhead = none , style=dashed];
444 -> 43[style=dashed];

445 [label="EVAL with clause\naddY(b, one(X602), zero(X603)) :- succ(X602, X603).\nand substitution\nT383 -> b\nX602 -> T402\nT384 -> one(T402)\nX603 -> T404\nT386 -> zero(T404)\nT403 -> T404", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 445 [arrowhead = none ];
445 -> 202;

446 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 446 [arrowhead = none ];
446 -> 203;

447 [label="ONLY EVAL with clause\naddY(X615, X616, X617) :- addC(X615, X616, X617).\nand substitution\nT383 -> T415\nX615 -> T415\nT384 -> T416\nX616 -> T416\nT386 -> T418\nX617 -> T418\nT417 -> T418", fontsize=14, style = filled, fillcolor = white];
201 -> 447 [arrowhead = none ];
447 -> 204;

448 [label="INSTANCE with matching:\nT256 -> T402\nT258 -> T404", fontsize=14, style = filled, fillcolor = lightgrey];
202 -> 448 [arrowhead = none , style=dashed];
448 -> 153[style=dashed];

449 [label="INSTANCE with matching:\nT294 -> T415\nT295 -> T416\nT297 -> T418", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 449 [arrowhead = none , style=dashed];
449 -> 171[style=dashed];

450 [label="INSTANCE with matching:\nT230 -> T428\nT231 -> T429\nT233 -> T431", fontsize=14, style = filled, fillcolor = lightgrey];
205 -> 450 [arrowhead = none , style=dashed];
450 -> 136[style=dashed];

451 [label="EVAL with clause\naddz(zero(X645), one(X646), one(X647)) :- addx(X645, X646, X647).\nand substitution\nX645 -> T444\nT92 -> zero(T444)\nX646 -> T445\nT93 -> one(T445)\nX647 -> T447\nT95 -> one(T447)\nT446 -> T447", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 451 [arrowhead = none ];
451 -> 209;

452 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 452 [arrowhead = none ];
452 -> 210;

453 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
208 -> 453 [arrowhead = none ];
453 -> 211;

454 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
208 -> 454 [arrowhead = none ];
454 -> 212;

455 [label="INSTANCE with matching:\nT146 -> T444\nT147 -> T445\nT149 -> T447", fontsize=14, style = filled, fillcolor = lightgrey];
209 -> 455 [arrowhead = none , style=dashed];
455 -> 110[style=dashed];

456 [label="EVAL with clause\naddz(one(X664), zero(X665), one(X666)) :- addy(X664, X665, X666).\nand substitution\nX664 -> T461\nT92 -> one(T461)\nX665 -> T462\nT93 -> zero(T462)\nX666 -> T464\nT95 -> one(T464)\nT463 -> T464", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 456 [arrowhead = none ];
456 -> 213;

457 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 457 [arrowhead = none ];
457 -> 214;

458 [label="EVAL with clause\naddz(one(X677), one(X678), zero(X679)) :- addc(X677, X678, X679).\nand substitution\nX677 -> T472\nT92 -> one(T472)\nX678 -> T473\nT93 -> one(T473)\nX679 -> T475\nT95 -> zero(T475)\nT474 -> T475", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 458 [arrowhead = none ];
458 -> 215;

459 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 459 [arrowhead = none ];
459 -> 216;

460 [label="INSTANCE with matching:\nT191 -> T461\nT192 -> T462\nT194 -> T464", fontsize=14, style = filled, fillcolor = lightgrey];
213 -> 460 [arrowhead = none , style=dashed];
460 -> 124[style=dashed];

461 [label="INSTANCE with matching:\nT230 -> T472\nT231 -> T473\nT233 -> T475", fontsize=14, style = filled, fillcolor = lightgrey];
215 -> 461 [arrowhead = none , style=dashed];
461 -> 136[style=dashed];

}

(2) Obligation:

Clauses:

binaryZ43(zero(T29)) :- binaryZ43(T29).
binaryZ43(one(T33)) :- binary50(T33).
binary50(b).
binary50(zero(T38)) :- binaryZ43(T38).
binary50(one(T42)) :- binary50(T42).
addz101(zero(T127), zero(T128), zero(T130)) :- addz101(T127, T128, T130).
addz101(zero(T146), one(T147), one(T149)) :- addx110(T146, T147, T149).
addz101(one(T191), zero(T192), one(T194)) :- addy124(T191, T192, T194).
addz101(one(T230), one(T231), zero(T233)) :- addc136(T230, T231, T233).
succ153(b, one(b)).
succ153(zero(T263), one(T263)) :- binaryZ43(T263).
succ153(one(T269), zero(T271)) :- succ153(T269, T271).
succZ146(zero(T250), one(T250)) :- binaryZ43(T250).
succZ146(one(T256), zero(T258)) :- succ153(T256, T258).
addC171(zero(T313), zero(T314), one(T316)) :- addz101(T313, T314, T316).
addC171(zero(zero(T341)), one(b), zero(one(T341))) :- binaryZ43(T341).
addC171(zero(one(T351)), one(b), zero(zero(T353))) :- succ153(T351, T353).
addC171(zero(T364), one(T365), zero(T367)) :- addC171(T364, T365, T367).
addC171(one(b), zero(zero(T392)), zero(one(T392))) :- binaryZ43(T392).
addC171(one(b), zero(one(T402)), zero(zero(T404))) :- succ153(T402, T404).
addC171(one(T415), zero(T416), zero(T418)) :- addC171(T415, T416, T418).
addC171(one(T428), one(T429), one(T431)) :- addc136(T428, T429, T431).
addc136(b, b, one(b)).
addc136(T242, b, T244) :- succZ146(T242, T244).
addc136(b, T280, T282) :- succZ146(T280, T282).
addc136(T294, T295, T297) :- addC171(T294, T295, T297).
addx110(one(T155), b, one(T155)) :- binary50(T155).
addx110(zero(T160), b, zero(T160)) :- binaryZ43(T160).
addx110(T172, T173, T175) :- addz101(T172, T173, T175).
addy124(b, one(T200), one(T200)) :- binary50(T200).
addy124(b, zero(T205), zero(T205)) :- binaryZ43(T205).
addy124(T217, T218, T220) :- addz101(T217, T218, T220).
add1(b, b, b).
add1(zero(T23), b, zero(T23)) :- binaryZ43(T23).
add1(one(T47), b, one(T47)) :- binary50(T47).
add1(b, zero(T74), zero(T74)) :- binaryZ43(T74).
add1(b, one(T80), one(T80)) :- binary50(T80).
add1(zero(T108), zero(T109), zero(T111)) :- addz101(T108, T109, T111).
add1(zero(T444), one(T445), one(T447)) :- addx110(T444, T445, T447).
add1(one(T461), zero(T462), one(T464)) :- addy124(T461, T462, T464).
add1(one(T472), one(T473), zero(T475)) :- addc136(T472, T473, T475).

Queries:

add1(g,g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
add1_in: (b,b,f)
binaryZ43_in: (b)
binary50_in: (b)
addz101_in: (b,b,f)
addx110_in: (b,b,f)
addy124_in: (b,b,f)
addc136_in: (b,b,f)
succZ146_in: (b,f)
succ153_in: (b,f)
addC171_in: (b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

add1_in_gga(b, b, b) → add1_out_gga(b, b, b)
add1_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZ43_in_g(T23))
binaryZ43_in_g(zero(T29)) → U1_g(T29, binaryZ43_in_g(T29))
binaryZ43_in_g(one(T33)) → U2_g(T33, binary50_in_g(T33))
binary50_in_g(b) → binary50_out_g(b)
binary50_in_g(zero(T38)) → U3_g(T38, binaryZ43_in_g(T38))
U3_g(T38, binaryZ43_out_g(T38)) → binary50_out_g(zero(T38))
binary50_in_g(one(T42)) → U4_g(T42, binary50_in_g(T42))
U4_g(T42, binary50_out_g(T42)) → binary50_out_g(one(T42))
U2_g(T33, binary50_out_g(T33)) → binaryZ43_out_g(one(T33))
U1_g(T29, binaryZ43_out_g(T29)) → binaryZ43_out_g(zero(T29))
U30_gga(T23, binaryZ43_out_g(T23)) → add1_out_gga(zero(T23), b, zero(T23))
add1_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binary50_in_g(T47))
U31_gga(T47, binary50_out_g(T47)) → add1_out_gga(one(T47), b, one(T47))
add1_in_gga(b, zero(T74), zero(T74)) → U32_gga(T74, binaryZ43_in_g(T74))
U32_gga(T74, binaryZ43_out_g(T74)) → add1_out_gga(b, zero(T74), zero(T74))
add1_in_gga(b, one(T80), one(T80)) → U33_gga(T80, binary50_in_g(T80))
U33_gga(T80, binary50_out_g(T80)) → add1_out_gga(b, one(T80), one(T80))
add1_in_gga(zero(T108), zero(T109), zero(T111)) → U34_gga(T108, T109, T111, addz101_in_gga(T108, T109, T111))
addz101_in_gga(zero(T127), zero(T128), zero(T130)) → U5_gga(T127, T128, T130, addz101_in_gga(T127, T128, T130))
addz101_in_gga(zero(T146), one(T147), one(T149)) → U6_gga(T146, T147, T149, addx110_in_gga(T146, T147, T149))
addx110_in_gga(one(T155), b, one(T155)) → U24_gga(T155, binary50_in_g(T155))
U24_gga(T155, binary50_out_g(T155)) → addx110_out_gga(one(T155), b, one(T155))
addx110_in_gga(zero(T160), b, zero(T160)) → U25_gga(T160, binaryZ43_in_g(T160))
U25_gga(T160, binaryZ43_out_g(T160)) → addx110_out_gga(zero(T160), b, zero(T160))
addx110_in_gga(T172, T173, T175) → U26_gga(T172, T173, T175, addz101_in_gga(T172, T173, T175))
addz101_in_gga(one(T191), zero(T192), one(T194)) → U7_gga(T191, T192, T194, addy124_in_gga(T191, T192, T194))
addy124_in_gga(b, one(T200), one(T200)) → U27_gga(T200, binary50_in_g(T200))
U27_gga(T200, binary50_out_g(T200)) → addy124_out_gga(b, one(T200), one(T200))
addy124_in_gga(b, zero(T205), zero(T205)) → U28_gga(T205, binaryZ43_in_g(T205))
U28_gga(T205, binaryZ43_out_g(T205)) → addy124_out_gga(b, zero(T205), zero(T205))
addy124_in_gga(T217, T218, T220) → U29_gga(T217, T218, T220, addz101_in_gga(T217, T218, T220))
addz101_in_gga(one(T230), one(T231), zero(T233)) → U8_gga(T230, T231, T233, addc136_in_gga(T230, T231, T233))
addc136_in_gga(b, b, one(b)) → addc136_out_gga(b, b, one(b))
addc136_in_gga(T242, b, T244) → U21_gga(T242, T244, succZ146_in_ga(T242, T244))
succZ146_in_ga(zero(T250), one(T250)) → U11_ga(T250, binaryZ43_in_g(T250))
U11_ga(T250, binaryZ43_out_g(T250)) → succZ146_out_ga(zero(T250), one(T250))
succZ146_in_ga(one(T256), zero(T258)) → U12_ga(T256, T258, succ153_in_ga(T256, T258))
succ153_in_ga(b, one(b)) → succ153_out_ga(b, one(b))
succ153_in_ga(zero(T263), one(T263)) → U9_ga(T263, binaryZ43_in_g(T263))
U9_ga(T263, binaryZ43_out_g(T263)) → succ153_out_ga(zero(T263), one(T263))
succ153_in_ga(one(T269), zero(T271)) → U10_ga(T269, T271, succ153_in_ga(T269, T271))
U10_ga(T269, T271, succ153_out_ga(T269, T271)) → succ153_out_ga(one(T269), zero(T271))
U12_ga(T256, T258, succ153_out_ga(T256, T258)) → succZ146_out_ga(one(T256), zero(T258))
U21_gga(T242, T244, succZ146_out_ga(T242, T244)) → addc136_out_gga(T242, b, T244)
addc136_in_gga(b, T280, T282) → U22_gga(T280, T282, succZ146_in_ga(T280, T282))
U22_gga(T280, T282, succZ146_out_ga(T280, T282)) → addc136_out_gga(b, T280, T282)
addc136_in_gga(T294, T295, T297) → U23_gga(T294, T295, T297, addC171_in_gga(T294, T295, T297))
addC171_in_gga(zero(T313), zero(T314), one(T316)) → U13_gga(T313, T314, T316, addz101_in_gga(T313, T314, T316))
U13_gga(T313, T314, T316, addz101_out_gga(T313, T314, T316)) → addC171_out_gga(zero(T313), zero(T314), one(T316))
addC171_in_gga(zero(zero(T341)), one(b), zero(one(T341))) → U14_gga(T341, binaryZ43_in_g(T341))
U14_gga(T341, binaryZ43_out_g(T341)) → addC171_out_gga(zero(zero(T341)), one(b), zero(one(T341)))
addC171_in_gga(zero(one(T351)), one(b), zero(zero(T353))) → U15_gga(T351, T353, succ153_in_ga(T351, T353))
U15_gga(T351, T353, succ153_out_ga(T351, T353)) → addC171_out_gga(zero(one(T351)), one(b), zero(zero(T353)))
addC171_in_gga(zero(T364), one(T365), zero(T367)) → U16_gga(T364, T365, T367, addC171_in_gga(T364, T365, T367))
addC171_in_gga(one(b), zero(zero(T392)), zero(one(T392))) → U17_gga(T392, binaryZ43_in_g(T392))
U17_gga(T392, binaryZ43_out_g(T392)) → addC171_out_gga(one(b), zero(zero(T392)), zero(one(T392)))
addC171_in_gga(one(b), zero(one(T402)), zero(zero(T404))) → U18_gga(T402, T404, succ153_in_ga(T402, T404))
U18_gga(T402, T404, succ153_out_ga(T402, T404)) → addC171_out_gga(one(b), zero(one(T402)), zero(zero(T404)))
addC171_in_gga(one(T415), zero(T416), zero(T418)) → U19_gga(T415, T416, T418, addC171_in_gga(T415, T416, T418))
addC171_in_gga(one(T428), one(T429), one(T431)) → U20_gga(T428, T429, T431, addc136_in_gga(T428, T429, T431))
U20_gga(T428, T429, T431, addc136_out_gga(T428, T429, T431)) → addC171_out_gga(one(T428), one(T429), one(T431))
U19_gga(T415, T416, T418, addC171_out_gga(T415, T416, T418)) → addC171_out_gga(one(T415), zero(T416), zero(T418))
U16_gga(T364, T365, T367, addC171_out_gga(T364, T365, T367)) → addC171_out_gga(zero(T364), one(T365), zero(T367))
U23_gga(T294, T295, T297, addC171_out_gga(T294, T295, T297)) → addc136_out_gga(T294, T295, T297)
U8_gga(T230, T231, T233, addc136_out_gga(T230, T231, T233)) → addz101_out_gga(one(T230), one(T231), zero(T233))
U29_gga(T217, T218, T220, addz101_out_gga(T217, T218, T220)) → addy124_out_gga(T217, T218, T220)
U7_gga(T191, T192, T194, addy124_out_gga(T191, T192, T194)) → addz101_out_gga(one(T191), zero(T192), one(T194))
U26_gga(T172, T173, T175, addz101_out_gga(T172, T173, T175)) → addx110_out_gga(T172, T173, T175)
U6_gga(T146, T147, T149, addx110_out_gga(T146, T147, T149)) → addz101_out_gga(zero(T146), one(T147), one(T149))
U5_gga(T127, T128, T130, addz101_out_gga(T127, T128, T130)) → addz101_out_gga(zero(T127), zero(T128), zero(T130))
U34_gga(T108, T109, T111, addz101_out_gga(T108, T109, T111)) → add1_out_gga(zero(T108), zero(T109), zero(T111))
add1_in_gga(zero(T444), one(T445), one(T447)) → U35_gga(T444, T445, T447, addx110_in_gga(T444, T445, T447))
U35_gga(T444, T445, T447, addx110_out_gga(T444, T445, T447)) → add1_out_gga(zero(T444), one(T445), one(T447))
add1_in_gga(one(T461), zero(T462), one(T464)) → U36_gga(T461, T462, T464, addy124_in_gga(T461, T462, T464))
U36_gga(T461, T462, T464, addy124_out_gga(T461, T462, T464)) → add1_out_gga(one(T461), zero(T462), one(T464))
add1_in_gga(one(T472), one(T473), zero(T475)) → U37_gga(T472, T473, T475, addc136_in_gga(T472, T473, T475))
U37_gga(T472, T473, T475, addc136_out_gga(T472, T473, T475)) → add1_out_gga(one(T472), one(T473), zero(T475))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

add1_in_gga(b, b, b) → add1_out_gga(b, b, b)
add1_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZ43_in_g(T23))
binaryZ43_in_g(zero(T29)) → U1_g(T29, binaryZ43_in_g(T29))
binaryZ43_in_g(one(T33)) → U2_g(T33, binary50_in_g(T33))
binary50_in_g(b) → binary50_out_g(b)
binary50_in_g(zero(T38)) → U3_g(T38, binaryZ43_in_g(T38))
U3_g(T38, binaryZ43_out_g(T38)) → binary50_out_g(zero(T38))
binary50_in_g(one(T42)) → U4_g(T42, binary50_in_g(T42))
U4_g(T42, binary50_out_g(T42)) → binary50_out_g(one(T42))
U2_g(T33, binary50_out_g(T33)) → binaryZ43_out_g(one(T33))
U1_g(T29, binaryZ43_out_g(T29)) → binaryZ43_out_g(zero(T29))
U30_gga(T23, binaryZ43_out_g(T23)) → add1_out_gga(zero(T23), b, zero(T23))
add1_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binary50_in_g(T47))
U31_gga(T47, binary50_out_g(T47)) → add1_out_gga(one(T47), b, one(T47))
add1_in_gga(b, zero(T74), zero(T74)) → U32_gga(T74, binaryZ43_in_g(T74))
U32_gga(T74, binaryZ43_out_g(T74)) → add1_out_gga(b, zero(T74), zero(T74))
add1_in_gga(b, one(T80), one(T80)) → U33_gga(T80, binary50_in_g(T80))
U33_gga(T80, binary50_out_g(T80)) → add1_out_gga(b, one(T80), one(T80))
add1_in_gga(zero(T108), zero(T109), zero(T111)) → U34_gga(T108, T109, T111, addz101_in_gga(T108, T109, T111))
addz101_in_gga(zero(T127), zero(T128), zero(T130)) → U5_gga(T127, T128, T130, addz101_in_gga(T127, T128, T130))
addz101_in_gga(zero(T146), one(T147), one(T149)) → U6_gga(T146, T147, T149, addx110_in_gga(T146, T147, T149))
addx110_in_gga(one(T155), b, one(T155)) → U24_gga(T155, binary50_in_g(T155))
U24_gga(T155, binary50_out_g(T155)) → addx110_out_gga(one(T155), b, one(T155))
addx110_in_gga(zero(T160), b, zero(T160)) → U25_gga(T160, binaryZ43_in_g(T160))
U25_gga(T160, binaryZ43_out_g(T160)) → addx110_out_gga(zero(T160), b, zero(T160))
addx110_in_gga(T172, T173, T175) → U26_gga(T172, T173, T175, addz101_in_gga(T172, T173, T175))
addz101_in_gga(one(T191), zero(T192), one(T194)) → U7_gga(T191, T192, T194, addy124_in_gga(T191, T192, T194))
addy124_in_gga(b, one(T200), one(T200)) → U27_gga(T200, binary50_in_g(T200))
U27_gga(T200, binary50_out_g(T200)) → addy124_out_gga(b, one(T200), one(T200))
addy124_in_gga(b, zero(T205), zero(T205)) → U28_gga(T205, binaryZ43_in_g(T205))
U28_gga(T205, binaryZ43_out_g(T205)) → addy124_out_gga(b, zero(T205), zero(T205))
addy124_in_gga(T217, T218, T220) → U29_gga(T217, T218, T220, addz101_in_gga(T217, T218, T220))
addz101_in_gga(one(T230), one(T231), zero(T233)) → U8_gga(T230, T231, T233, addc136_in_gga(T230, T231, T233))
addc136_in_gga(b, b, one(b)) → addc136_out_gga(b, b, one(b))
addc136_in_gga(T242, b, T244) → U21_gga(T242, T244, succZ146_in_ga(T242, T244))
succZ146_in_ga(zero(T250), one(T250)) → U11_ga(T250, binaryZ43_in_g(T250))
U11_ga(T250, binaryZ43_out_g(T250)) → succZ146_out_ga(zero(T250), one(T250))
succZ146_in_ga(one(T256), zero(T258)) → U12_ga(T256, T258, succ153_in_ga(T256, T258))
succ153_in_ga(b, one(b)) → succ153_out_ga(b, one(b))
succ153_in_ga(zero(T263), one(T263)) → U9_ga(T263, binaryZ43_in_g(T263))
U9_ga(T263, binaryZ43_out_g(T263)) → succ153_out_ga(zero(T263), one(T263))
succ153_in_ga(one(T269), zero(T271)) → U10_ga(T269, T271, succ153_in_ga(T269, T271))
U10_ga(T269, T271, succ153_out_ga(T269, T271)) → succ153_out_ga(one(T269), zero(T271))
U12_ga(T256, T258, succ153_out_ga(T256, T258)) → succZ146_out_ga(one(T256), zero(T258))
U21_gga(T242, T244, succZ146_out_ga(T242, T244)) → addc136_out_gga(T242, b, T244)
addc136_in_gga(b, T280, T282) → U22_gga(T280, T282, succZ146_in_ga(T280, T282))
U22_gga(T280, T282, succZ146_out_ga(T280, T282)) → addc136_out_gga(b, T280, T282)
addc136_in_gga(T294, T295, T297) → U23_gga(T294, T295, T297, addC171_in_gga(T294, T295, T297))
addC171_in_gga(zero(T313), zero(T314), one(T316)) → U13_gga(T313, T314, T316, addz101_in_gga(T313, T314, T316))
U13_gga(T313, T314, T316, addz101_out_gga(T313, T314, T316)) → addC171_out_gga(zero(T313), zero(T314), one(T316))
addC171_in_gga(zero(zero(T341)), one(b), zero(one(T341))) → U14_gga(T341, binaryZ43_in_g(T341))
U14_gga(T341, binaryZ43_out_g(T341)) → addC171_out_gga(zero(zero(T341)), one(b), zero(one(T341)))
addC171_in_gga(zero(one(T351)), one(b), zero(zero(T353))) → U15_gga(T351, T353, succ153_in_ga(T351, T353))
U15_gga(T351, T353, succ153_out_ga(T351, T353)) → addC171_out_gga(zero(one(T351)), one(b), zero(zero(T353)))
addC171_in_gga(zero(T364), one(T365), zero(T367)) → U16_gga(T364, T365, T367, addC171_in_gga(T364, T365, T367))
addC171_in_gga(one(b), zero(zero(T392)), zero(one(T392))) → U17_gga(T392, binaryZ43_in_g(T392))
U17_gga(T392, binaryZ43_out_g(T392)) → addC171_out_gga(one(b), zero(zero(T392)), zero(one(T392)))
addC171_in_gga(one(b), zero(one(T402)), zero(zero(T404))) → U18_gga(T402, T404, succ153_in_ga(T402, T404))
U18_gga(T402, T404, succ153_out_ga(T402, T404)) → addC171_out_gga(one(b), zero(one(T402)), zero(zero(T404)))
addC171_in_gga(one(T415), zero(T416), zero(T418)) → U19_gga(T415, T416, T418, addC171_in_gga(T415, T416, T418))
addC171_in_gga(one(T428), one(T429), one(T431)) → U20_gga(T428, T429, T431, addc136_in_gga(T428, T429, T431))
U20_gga(T428, T429, T431, addc136_out_gga(T428, T429, T431)) → addC171_out_gga(one(T428), one(T429), one(T431))
U19_gga(T415, T416, T418, addC171_out_gga(T415, T416, T418)) → addC171_out_gga(one(T415), zero(T416), zero(T418))
U16_gga(T364, T365, T367, addC171_out_gga(T364, T365, T367)) → addC171_out_gga(zero(T364), one(T365), zero(T367))
U23_gga(T294, T295, T297, addC171_out_gga(T294, T295, T297)) → addc136_out_gga(T294, T295, T297)
U8_gga(T230, T231, T233, addc136_out_gga(T230, T231, T233)) → addz101_out_gga(one(T230), one(T231), zero(T233))
U29_gga(T217, T218, T220, addz101_out_gga(T217, T218, T220)) → addy124_out_gga(T217, T218, T220)
U7_gga(T191, T192, T194, addy124_out_gga(T191, T192, T194)) → addz101_out_gga(one(T191), zero(T192), one(T194))
U26_gga(T172, T173, T175, addz101_out_gga(T172, T173, T175)) → addx110_out_gga(T172, T173, T175)
U6_gga(T146, T147, T149, addx110_out_gga(T146, T147, T149)) → addz101_out_gga(zero(T146), one(T147), one(T149))
U5_gga(T127, T128, T130, addz101_out_gga(T127, T128, T130)) → addz101_out_gga(zero(T127), zero(T128), zero(T130))
U34_gga(T108, T109, T111, addz101_out_gga(T108, T109, T111)) → add1_out_gga(zero(T108), zero(T109), zero(T111))
add1_in_gga(zero(T444), one(T445), one(T447)) → U35_gga(T444, T445, T447, addx110_in_gga(T444, T445, T447))
U35_gga(T444, T445, T447, addx110_out_gga(T444, T445, T447)) → add1_out_gga(zero(T444), one(T445), one(T447))
add1_in_gga(one(T461), zero(T462), one(T464)) → U36_gga(T461, T462, T464, addy124_in_gga(T461, T462, T464))
U36_gga(T461, T462, T464, addy124_out_gga(T461, T462, T464)) → add1_out_gga(one(T461), zero(T462), one(T464))
add1_in_gga(one(T472), one(T473), zero(T475)) → U37_gga(T472, T473, T475, addc136_in_gga(T472, T473, T475))
U37_gga(T472, T473, T475, addc136_out_gga(T472, T473, T475)) → add1_out_gga(one(T472), one(T473), zero(T475))

(5) DependencyPairsProof (EQUIVALENT transformation)

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

ADD1_IN_GGA(zero(T23), b, zero(T23)) → U30_GGA(T23, binaryZ43_in_g(T23))
ADD1_IN_GGA(zero(T23), b, zero(T23)) → BINARYZ43_IN_G(T23)
BINARYZ43_IN_G(zero(T29)) → U1_G(T29, binaryZ43_in_g(T29))
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARYZ43_IN_G(one(T33)) → U2_G(T33, binary50_in_g(T33))
BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → U3_G(T38, binaryZ43_in_g(T38))
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARY50_IN_G(one(T42)) → U4_G(T42, binary50_in_g(T42))
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)
ADD1_IN_GGA(one(T47), b, one(T47)) → U31_GGA(T47, binary50_in_g(T47))
ADD1_IN_GGA(one(T47), b, one(T47)) → BINARY50_IN_G(T47)
ADD1_IN_GGA(b, zero(T74), zero(T74)) → U32_GGA(T74, binaryZ43_in_g(T74))
ADD1_IN_GGA(b, zero(T74), zero(T74)) → BINARYZ43_IN_G(T74)
ADD1_IN_GGA(b, one(T80), one(T80)) → U33_GGA(T80, binary50_in_g(T80))
ADD1_IN_GGA(b, one(T80), one(T80)) → BINARY50_IN_G(T80)
ADD1_IN_GGA(zero(T108), zero(T109), zero(T111)) → U34_GGA(T108, T109, T111, addz101_in_gga(T108, T109, T111))
ADD1_IN_GGA(zero(T108), zero(T109), zero(T111)) → ADDZ101_IN_GGA(T108, T109, T111)
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → U5_GGA(T127, T128, T130, addz101_in_gga(T127, T128, T130))
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → ADDZ101_IN_GGA(T127, T128, T130)
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → U6_GGA(T146, T147, T149, addx110_in_gga(T146, T147, T149))
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → ADDX110_IN_GGA(T146, T147, T149)
ADDX110_IN_GGA(one(T155), b, one(T155)) → U24_GGA(T155, binary50_in_g(T155))
ADDX110_IN_GGA(one(T155), b, one(T155)) → BINARY50_IN_G(T155)
ADDX110_IN_GGA(zero(T160), b, zero(T160)) → U25_GGA(T160, binaryZ43_in_g(T160))
ADDX110_IN_GGA(zero(T160), b, zero(T160)) → BINARYZ43_IN_G(T160)
ADDX110_IN_GGA(T172, T173, T175) → U26_GGA(T172, T173, T175, addz101_in_gga(T172, T173, T175))
ADDX110_IN_GGA(T172, T173, T175) → ADDZ101_IN_GGA(T172, T173, T175)
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → U7_GGA(T191, T192, T194, addy124_in_gga(T191, T192, T194))
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → ADDY124_IN_GGA(T191, T192, T194)
ADDY124_IN_GGA(b, one(T200), one(T200)) → U27_GGA(T200, binary50_in_g(T200))
ADDY124_IN_GGA(b, one(T200), one(T200)) → BINARY50_IN_G(T200)
ADDY124_IN_GGA(b, zero(T205), zero(T205)) → U28_GGA(T205, binaryZ43_in_g(T205))
ADDY124_IN_GGA(b, zero(T205), zero(T205)) → BINARYZ43_IN_G(T205)
ADDY124_IN_GGA(T217, T218, T220) → U29_GGA(T217, T218, T220, addz101_in_gga(T217, T218, T220))
ADDY124_IN_GGA(T217, T218, T220) → ADDZ101_IN_GGA(T217, T218, T220)
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → U8_GGA(T230, T231, T233, addc136_in_gga(T230, T231, T233))
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → ADDC136_IN_GGA(T230, T231, T233)
ADDC136_IN_GGA(T242, b, T244) → U21_GGA(T242, T244, succZ146_in_ga(T242, T244))
ADDC136_IN_GGA(T242, b, T244) → SUCCZ146_IN_GA(T242, T244)
SUCCZ146_IN_GA(zero(T250), one(T250)) → U11_GA(T250, binaryZ43_in_g(T250))
SUCCZ146_IN_GA(zero(T250), one(T250)) → BINARYZ43_IN_G(T250)
SUCCZ146_IN_GA(one(T256), zero(T258)) → U12_GA(T256, T258, succ153_in_ga(T256, T258))
SUCCZ146_IN_GA(one(T256), zero(T258)) → SUCC153_IN_GA(T256, T258)
SUCC153_IN_GA(zero(T263), one(T263)) → U9_GA(T263, binaryZ43_in_g(T263))
SUCC153_IN_GA(zero(T263), one(T263)) → BINARYZ43_IN_G(T263)
SUCC153_IN_GA(one(T269), zero(T271)) → U10_GA(T269, T271, succ153_in_ga(T269, T271))
SUCC153_IN_GA(one(T269), zero(T271)) → SUCC153_IN_GA(T269, T271)
ADDC136_IN_GGA(b, T280, T282) → U22_GGA(T280, T282, succZ146_in_ga(T280, T282))
ADDC136_IN_GGA(b, T280, T282) → SUCCZ146_IN_GA(T280, T282)
ADDC136_IN_GGA(T294, T295, T297) → U23_GGA(T294, T295, T297, addC171_in_gga(T294, T295, T297))
ADDC136_IN_GGA(T294, T295, T297) → ADDC171_IN_GGA(T294, T295, T297)
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → U13_GGA(T313, T314, T316, addz101_in_gga(T313, T314, T316))
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → ADDZ101_IN_GGA(T313, T314, T316)
ADDC171_IN_GGA(zero(zero(T341)), one(b), zero(one(T341))) → U14_GGA(T341, binaryZ43_in_g(T341))
ADDC171_IN_GGA(zero(zero(T341)), one(b), zero(one(T341))) → BINARYZ43_IN_G(T341)
ADDC171_IN_GGA(zero(one(T351)), one(b), zero(zero(T353))) → U15_GGA(T351, T353, succ153_in_ga(T351, T353))
ADDC171_IN_GGA(zero(one(T351)), one(b), zero(zero(T353))) → SUCC153_IN_GA(T351, T353)
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → U16_GGA(T364, T365, T367, addC171_in_gga(T364, T365, T367))
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → ADDC171_IN_GGA(T364, T365, T367)
ADDC171_IN_GGA(one(b), zero(zero(T392)), zero(one(T392))) → U17_GGA(T392, binaryZ43_in_g(T392))
ADDC171_IN_GGA(one(b), zero(zero(T392)), zero(one(T392))) → BINARYZ43_IN_G(T392)
ADDC171_IN_GGA(one(b), zero(one(T402)), zero(zero(T404))) → U18_GGA(T402, T404, succ153_in_ga(T402, T404))
ADDC171_IN_GGA(one(b), zero(one(T402)), zero(zero(T404))) → SUCC153_IN_GA(T402, T404)
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → U19_GGA(T415, T416, T418, addC171_in_gga(T415, T416, T418))
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → ADDC171_IN_GGA(T415, T416, T418)
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → U20_GGA(T428, T429, T431, addc136_in_gga(T428, T429, T431))
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → ADDC136_IN_GGA(T428, T429, T431)
ADD1_IN_GGA(zero(T444), one(T445), one(T447)) → U35_GGA(T444, T445, T447, addx110_in_gga(T444, T445, T447))
ADD1_IN_GGA(zero(T444), one(T445), one(T447)) → ADDX110_IN_GGA(T444, T445, T447)
ADD1_IN_GGA(one(T461), zero(T462), one(T464)) → U36_GGA(T461, T462, T464, addy124_in_gga(T461, T462, T464))
ADD1_IN_GGA(one(T461), zero(T462), one(T464)) → ADDY124_IN_GGA(T461, T462, T464)
ADD1_IN_GGA(one(T472), one(T473), zero(T475)) → U37_GGA(T472, T473, T475, addc136_in_gga(T472, T473, T475))
ADD1_IN_GGA(one(T472), one(T473), zero(T475)) → ADDC136_IN_GGA(T472, T473, T475)

The TRS R consists of the following rules:

add1_in_gga(b, b, b) → add1_out_gga(b, b, b)
add1_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZ43_in_g(T23))
binaryZ43_in_g(zero(T29)) → U1_g(T29, binaryZ43_in_g(T29))
binaryZ43_in_g(one(T33)) → U2_g(T33, binary50_in_g(T33))
binary50_in_g(b) → binary50_out_g(b)
binary50_in_g(zero(T38)) → U3_g(T38, binaryZ43_in_g(T38))
U3_g(T38, binaryZ43_out_g(T38)) → binary50_out_g(zero(T38))
binary50_in_g(one(T42)) → U4_g(T42, binary50_in_g(T42))
U4_g(T42, binary50_out_g(T42)) → binary50_out_g(one(T42))
U2_g(T33, binary50_out_g(T33)) → binaryZ43_out_g(one(T33))
U1_g(T29, binaryZ43_out_g(T29)) → binaryZ43_out_g(zero(T29))
U30_gga(T23, binaryZ43_out_g(T23)) → add1_out_gga(zero(T23), b, zero(T23))
add1_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binary50_in_g(T47))
U31_gga(T47, binary50_out_g(T47)) → add1_out_gga(one(T47), b, one(T47))
add1_in_gga(b, zero(T74), zero(T74)) → U32_gga(T74, binaryZ43_in_g(T74))
U32_gga(T74, binaryZ43_out_g(T74)) → add1_out_gga(b, zero(T74), zero(T74))
add1_in_gga(b, one(T80), one(T80)) → U33_gga(T80, binary50_in_g(T80))
U33_gga(T80, binary50_out_g(T80)) → add1_out_gga(b, one(T80), one(T80))
add1_in_gga(zero(T108), zero(T109), zero(T111)) → U34_gga(T108, T109, T111, addz101_in_gga(T108, T109, T111))
addz101_in_gga(zero(T127), zero(T128), zero(T130)) → U5_gga(T127, T128, T130, addz101_in_gga(T127, T128, T130))
addz101_in_gga(zero(T146), one(T147), one(T149)) → U6_gga(T146, T147, T149, addx110_in_gga(T146, T147, T149))
addx110_in_gga(one(T155), b, one(T155)) → U24_gga(T155, binary50_in_g(T155))
U24_gga(T155, binary50_out_g(T155)) → addx110_out_gga(one(T155), b, one(T155))
addx110_in_gga(zero(T160), b, zero(T160)) → U25_gga(T160, binaryZ43_in_g(T160))
U25_gga(T160, binaryZ43_out_g(T160)) → addx110_out_gga(zero(T160), b, zero(T160))
addx110_in_gga(T172, T173, T175) → U26_gga(T172, T173, T175, addz101_in_gga(T172, T173, T175))
addz101_in_gga(one(T191), zero(T192), one(T194)) → U7_gga(T191, T192, T194, addy124_in_gga(T191, T192, T194))
addy124_in_gga(b, one(T200), one(T200)) → U27_gga(T200, binary50_in_g(T200))
U27_gga(T200, binary50_out_g(T200)) → addy124_out_gga(b, one(T200), one(T200))
addy124_in_gga(b, zero(T205), zero(T205)) → U28_gga(T205, binaryZ43_in_g(T205))
U28_gga(T205, binaryZ43_out_g(T205)) → addy124_out_gga(b, zero(T205), zero(T205))
addy124_in_gga(T217, T218, T220) → U29_gga(T217, T218, T220, addz101_in_gga(T217, T218, T220))
addz101_in_gga(one(T230), one(T231), zero(T233)) → U8_gga(T230, T231, T233, addc136_in_gga(T230, T231, T233))
addc136_in_gga(b, b, one(b)) → addc136_out_gga(b, b, one(b))
addc136_in_gga(T242, b, T244) → U21_gga(T242, T244, succZ146_in_ga(T242, T244))
succZ146_in_ga(zero(T250), one(T250)) → U11_ga(T250, binaryZ43_in_g(T250))
U11_ga(T250, binaryZ43_out_g(T250)) → succZ146_out_ga(zero(T250), one(T250))
succZ146_in_ga(one(T256), zero(T258)) → U12_ga(T256, T258, succ153_in_ga(T256, T258))
succ153_in_ga(b, one(b)) → succ153_out_ga(b, one(b))
succ153_in_ga(zero(T263), one(T263)) → U9_ga(T263, binaryZ43_in_g(T263))
U9_ga(T263, binaryZ43_out_g(T263)) → succ153_out_ga(zero(T263), one(T263))
succ153_in_ga(one(T269), zero(T271)) → U10_ga(T269, T271, succ153_in_ga(T269, T271))
U10_ga(T269, T271, succ153_out_ga(T269, T271)) → succ153_out_ga(one(T269), zero(T271))
U12_ga(T256, T258, succ153_out_ga(T256, T258)) → succZ146_out_ga(one(T256), zero(T258))
U21_gga(T242, T244, succZ146_out_ga(T242, T244)) → addc136_out_gga(T242, b, T244)
addc136_in_gga(b, T280, T282) → U22_gga(T280, T282, succZ146_in_ga(T280, T282))
U22_gga(T280, T282, succZ146_out_ga(T280, T282)) → addc136_out_gga(b, T280, T282)
addc136_in_gga(T294, T295, T297) → U23_gga(T294, T295, T297, addC171_in_gga(T294, T295, T297))
addC171_in_gga(zero(T313), zero(T314), one(T316)) → U13_gga(T313, T314, T316, addz101_in_gga(T313, T314, T316))
U13_gga(T313, T314, T316, addz101_out_gga(T313, T314, T316)) → addC171_out_gga(zero(T313), zero(T314), one(T316))
addC171_in_gga(zero(zero(T341)), one(b), zero(one(T341))) → U14_gga(T341, binaryZ43_in_g(T341))
U14_gga(T341, binaryZ43_out_g(T341)) → addC171_out_gga(zero(zero(T341)), one(b), zero(one(T341)))
addC171_in_gga(zero(one(T351)), one(b), zero(zero(T353))) → U15_gga(T351, T353, succ153_in_ga(T351, T353))
U15_gga(T351, T353, succ153_out_ga(T351, T353)) → addC171_out_gga(zero(one(T351)), one(b), zero(zero(T353)))
addC171_in_gga(zero(T364), one(T365), zero(T367)) → U16_gga(T364, T365, T367, addC171_in_gga(T364, T365, T367))
addC171_in_gga(one(b), zero(zero(T392)), zero(one(T392))) → U17_gga(T392, binaryZ43_in_g(T392))
U17_gga(T392, binaryZ43_out_g(T392)) → addC171_out_gga(one(b), zero(zero(T392)), zero(one(T392)))
addC171_in_gga(one(b), zero(one(T402)), zero(zero(T404))) → U18_gga(T402, T404, succ153_in_ga(T402, T404))
U18_gga(T402, T404, succ153_out_ga(T402, T404)) → addC171_out_gga(one(b), zero(one(T402)), zero(zero(T404)))
addC171_in_gga(one(T415), zero(T416), zero(T418)) → U19_gga(T415, T416, T418, addC171_in_gga(T415, T416, T418))
addC171_in_gga(one(T428), one(T429), one(T431)) → U20_gga(T428, T429, T431, addc136_in_gga(T428, T429, T431))
U20_gga(T428, T429, T431, addc136_out_gga(T428, T429, T431)) → addC171_out_gga(one(T428), one(T429), one(T431))
U19_gga(T415, T416, T418, addC171_out_gga(T415, T416, T418)) → addC171_out_gga(one(T415), zero(T416), zero(T418))
U16_gga(T364, T365, T367, addC171_out_gga(T364, T365, T367)) → addC171_out_gga(zero(T364), one(T365), zero(T367))
U23_gga(T294, T295, T297, addC171_out_gga(T294, T295, T297)) → addc136_out_gga(T294, T295, T297)
U8_gga(T230, T231, T233, addc136_out_gga(T230, T231, T233)) → addz101_out_gga(one(T230), one(T231), zero(T233))
U29_gga(T217, T218, T220, addz101_out_gga(T217, T218, T220)) → addy124_out_gga(T217, T218, T220)
U7_gga(T191, T192, T194, addy124_out_gga(T191, T192, T194)) → addz101_out_gga(one(T191), zero(T192), one(T194))
U26_gga(T172, T173, T175, addz101_out_gga(T172, T173, T175)) → addx110_out_gga(T172, T173, T175)
U6_gga(T146, T147, T149, addx110_out_gga(T146, T147, T149)) → addz101_out_gga(zero(T146), one(T147), one(T149))
U5_gga(T127, T128, T130, addz101_out_gga(T127, T128, T130)) → addz101_out_gga(zero(T127), zero(T128), zero(T130))
U34_gga(T108, T109, T111, addz101_out_gga(T108, T109, T111)) → add1_out_gga(zero(T108), zero(T109), zero(T111))
add1_in_gga(zero(T444), one(T445), one(T447)) → U35_gga(T444, T445, T447, addx110_in_gga(T444, T445, T447))
U35_gga(T444, T445, T447, addx110_out_gga(T444, T445, T447)) → add1_out_gga(zero(T444), one(T445), one(T447))
add1_in_gga(one(T461), zero(T462), one(T464)) → U36_gga(T461, T462, T464, addy124_in_gga(T461, T462, T464))
U36_gga(T461, T462, T464, addy124_out_gga(T461, T462, T464)) → add1_out_gga(one(T461), zero(T462), one(T464))
add1_in_gga(one(T472), one(T473), zero(T475)) → U37_gga(T472, T473, T475, addc136_in_gga(T472, T473, T475))
U37_gga(T472, T473, T475, addc136_out_gga(T472, T473, T475)) → add1_out_gga(one(T472), one(T473), zero(T475))

The argument filtering Pi contains the following mapping:
add1_in_gga(x1, x2, x3) = add1_in_gga(x1, x2)
b = b
add1_out_gga(x1, x2, x3) = add1_out_gga(x3)
zero(x1) = zero(x1)
U30_gga(x1, x2) = U30_gga(x1, x2)
binaryZ43_in_g(x1) = binaryZ43_in_g(x1)
U1_g(x1, x2) = U1_g(x2)
one(x1) = one(x1)
U2_g(x1, x2) = U2_g(x2)
binary50_in_g(x1) = binary50_in_g(x1)
binary50_out_g(x1) = binary50_out_g
U3_g(x1, x2) = U3_g(x2)
binaryZ43_out_g(x1) = binaryZ43_out_g
U4_g(x1, x2) = U4_g(x2)
U31_gga(x1, x2) = U31_gga(x1, x2)
U32_gga(x1, x2) = U32_gga(x1, x2)
U33_gga(x1, x2) = U33_gga(x1, x2)
U34_gga(x1, x2, x3, x4) = U34_gga(x4)
addz101_in_gga(x1, x2, x3) = addz101_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4) = U5_gga(x4)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
addx110_in_gga(x1, x2, x3) = addx110_in_gga(x1, x2)
U24_gga(x1, x2) = U24_gga(x1, x2)
addx110_out_gga(x1, x2, x3) = addx110_out_gga(x3)
U25_gga(x1, x2) = U25_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x4)
U7_gga(x1, x2, x3, x4) = U7_gga(x4)
addy124_in_gga(x1, x2, x3) = addy124_in_gga(x1, x2)
U27_gga(x1, x2) = U27_gga(x1, x2)
addy124_out_gga(x1, x2, x3) = addy124_out_gga(x3)
U28_gga(x1, x2) = U28_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x4)
U8_gga(x1, x2, x3, x4) = U8_gga(x4)
addc136_in_gga(x1, x2, x3) = addc136_in_gga(x1, x2)
addc136_out_gga(x1, x2, x3) = addc136_out_gga(x3)
U21_gga(x1, x2, x3) = U21_gga(x3)
succZ146_in_ga(x1, x2) = succZ146_in_ga(x1)
U11_ga(x1, x2) = U11_ga(x1, x2)
succZ146_out_ga(x1, x2) = succZ146_out_ga(x2)
U12_ga(x1, x2, x3) = U12_ga(x3)
succ153_in_ga(x1, x2) = succ153_in_ga(x1)
succ153_out_ga(x1, x2) = succ153_out_ga(x2)
U9_ga(x1, x2) = U9_ga(x1, x2)
U10_ga(x1, x2, x3) = U10_ga(x3)
U22_gga(x1, x2, x3) = U22_gga(x3)
U23_gga(x1, x2, x3, x4) = U23_gga(x4)
addC171_in_gga(x1, x2, x3) = addC171_in_gga(x1, x2)
U13_gga(x1, x2, x3, x4) = U13_gga(x4)
addz101_out_gga(x1, x2, x3) = addz101_out_gga(x3)
addC171_out_gga(x1, x2, x3) = addC171_out_gga(x3)
U14_gga(x1, x2) = U14_gga(x1, x2)
U15_gga(x1, x2, x3) = U15_gga(x3)
U16_gga(x1, x2, x3, x4) = U16_gga(x4)
U17_gga(x1, x2) = U17_gga(x1, x2)
U18_gga(x1, x2, x3) = U18_gga(x3)
U19_gga(x1, x2, x3, x4) = U19_gga(x4)
U20_gga(x1, x2, x3, x4) = U20_gga(x4)
U35_gga(x1, x2, x3, x4) = U35_gga(x4)
U36_gga(x1, x2, x3, x4) = U36_gga(x4)
U37_gga(x1, x2, x3, x4) = U37_gga(x4)
ADD1_IN_GGA(x1, x2, x3) = ADD1_IN_GGA(x1, x2)
U30_GGA(x1, x2) = U30_GGA(x1, x2)
BINARYZ43_IN_G(x1) = BINARYZ43_IN_G(x1)
U1_G(x1, x2) = U1_G(x2)
U2_G(x1, x2) = U2_G(x2)
BINARY50_IN_G(x1) = BINARY50_IN_G(x1)
U3_G(x1, x2) = U3_G(x2)
U4_G(x1, x2) = U4_G(x2)
U31_GGA(x1, x2) = U31_GGA(x1, x2)
U32_GGA(x1, x2) = U32_GGA(x1, x2)
U33_GGA(x1, x2) = U33_GGA(x1, x2)
U34_GGA(x1, x2, x3, x4) = U34_GGA(x4)
ADDZ101_IN_GGA(x1, x2, x3) = ADDZ101_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4) = U5_GGA(x4)
U6_GGA(x1, x2, x3, x4) = U6_GGA(x4)
ADDX110_IN_GGA(x1, x2, x3) = ADDX110_IN_GGA(x1, x2)
U24_GGA(x1, x2) = U24_GGA(x1, x2)
U25_GGA(x1, x2) = U25_GGA(x1, x2)
U26_GGA(x1, x2, x3, x4) = U26_GGA(x4)
U7_GGA(x1, x2, x3, x4) = U7_GGA(x4)
ADDY124_IN_GGA(x1, x2, x3) = ADDY124_IN_GGA(x1, x2)
U27_GGA(x1, x2) = U27_GGA(x1, x2)
U28_GGA(x1, x2) = U28_GGA(x1, x2)
U29_GGA(x1, x2, x3, x4) = U29_GGA(x4)
U8_GGA(x1, x2, x3, x4) = U8_GGA(x4)
ADDC136_IN_GGA(x1, x2, x3) = ADDC136_IN_GGA(x1, x2)
U21_GGA(x1, x2, x3) = U21_GGA(x3)
SUCCZ146_IN_GA(x1, x2) = SUCCZ146_IN_GA(x1)
U11_GA(x1, x2) = U11_GA(x1, x2)
U12_GA(x1, x2, x3) = U12_GA(x3)
SUCC153_IN_GA(x1, x2) = SUCC153_IN_GA(x1)
U9_GA(x1, x2) = U9_GA(x1, x2)
U10_GA(x1, x2, x3) = U10_GA(x3)
U22_GGA(x1, x2, x3) = U22_GGA(x3)
U23_GGA(x1, x2, x3, x4) = U23_GGA(x4)
ADDC171_IN_GGA(x1, x2, x3) = ADDC171_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4) = U13_GGA(x4)
U14_GGA(x1, x2) = U14_GGA(x1, x2)
U15_GGA(x1, x2, x3) = U15_GGA(x3)
U16_GGA(x1, x2, x3, x4) = U16_GGA(x4)
U17_GGA(x1, x2) = U17_GGA(x1, x2)
U18_GGA(x1, x2, x3) = U18_GGA(x3)
U19_GGA(x1, x2, x3, x4) = U19_GGA(x4)
U20_GGA(x1, x2, x3, x4) = U20_GGA(x4)
U35_GGA(x1, x2, x3, x4) = U35_GGA(x4)
U36_GGA(x1, x2, x3, x4) = U36_GGA(x4)
U37_GGA(x1, x2, x3, x4) = U37_GGA(x4)

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

(6) Obligation:

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

ADD1_IN_GGA(zero(T23), b, zero(T23)) → U30_GGA(T23, binaryZ43_in_g(T23))
ADD1_IN_GGA(zero(T23), b, zero(T23)) → BINARYZ43_IN_G(T23)
BINARYZ43_IN_G(zero(T29)) → U1_G(T29, binaryZ43_in_g(T29))
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARYZ43_IN_G(one(T33)) → U2_G(T33, binary50_in_g(T33))
BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → U3_G(T38, binaryZ43_in_g(T38))
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARY50_IN_G(one(T42)) → U4_G(T42, binary50_in_g(T42))
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)
ADD1_IN_GGA(one(T47), b, one(T47)) → U31_GGA(T47, binary50_in_g(T47))
ADD1_IN_GGA(one(T47), b, one(T47)) → BINARY50_IN_G(T47)
ADD1_IN_GGA(b, zero(T74), zero(T74)) → U32_GGA(T74, binaryZ43_in_g(T74))
ADD1_IN_GGA(b, zero(T74), zero(T74)) → BINARYZ43_IN_G(T74)
ADD1_IN_GGA(b, one(T80), one(T80)) → U33_GGA(T80, binary50_in_g(T80))
ADD1_IN_GGA(b, one(T80), one(T80)) → BINARY50_IN_G(T80)
ADD1_IN_GGA(zero(T108), zero(T109), zero(T111)) → U34_GGA(T108, T109, T111, addz101_in_gga(T108, T109, T111))
ADD1_IN_GGA(zero(T108), zero(T109), zero(T111)) → ADDZ101_IN_GGA(T108, T109, T111)
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → U5_GGA(T127, T128, T130, addz101_in_gga(T127, T128, T130))
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → ADDZ101_IN_GGA(T127, T128, T130)
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → U6_GGA(T146, T147, T149, addx110_in_gga(T146, T147, T149))
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → ADDX110_IN_GGA(T146, T147, T149)
ADDX110_IN_GGA(one(T155), b, one(T155)) → U24_GGA(T155, binary50_in_g(T155))
ADDX110_IN_GGA(one(T155), b, one(T155)) → BINARY50_IN_G(T155)
ADDX110_IN_GGA(zero(T160), b, zero(T160)) → U25_GGA(T160, binaryZ43_in_g(T160))
ADDX110_IN_GGA(zero(T160), b, zero(T160)) → BINARYZ43_IN_G(T160)
ADDX110_IN_GGA(T172, T173, T175) → U26_GGA(T172, T173, T175, addz101_in_gga(T172, T173, T175))
ADDX110_IN_GGA(T172, T173, T175) → ADDZ101_IN_GGA(T172, T173, T175)
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → U7_GGA(T191, T192, T194, addy124_in_gga(T191, T192, T194))
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → ADDY124_IN_GGA(T191, T192, T194)
ADDY124_IN_GGA(b, one(T200), one(T200)) → U27_GGA(T200, binary50_in_g(T200))
ADDY124_IN_GGA(b, one(T200), one(T200)) → BINARY50_IN_G(T200)
ADDY124_IN_GGA(b, zero(T205), zero(T205)) → U28_GGA(T205, binaryZ43_in_g(T205))
ADDY124_IN_GGA(b, zero(T205), zero(T205)) → BINARYZ43_IN_G(T205)
ADDY124_IN_GGA(T217, T218, T220) → U29_GGA(T217, T218, T220, addz101_in_gga(T217, T218, T220))
ADDY124_IN_GGA(T217, T218, T220) → ADDZ101_IN_GGA(T217, T218, T220)
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → U8_GGA(T230, T231, T233, addc136_in_gga(T230, T231, T233))
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → ADDC136_IN_GGA(T230, T231, T233)
ADDC136_IN_GGA(T242, b, T244) → U21_GGA(T242, T244, succZ146_in_ga(T242, T244))
ADDC136_IN_GGA(T242, b, T244) → SUCCZ146_IN_GA(T242, T244)
SUCCZ146_IN_GA(zero(T250), one(T250)) → U11_GA(T250, binaryZ43_in_g(T250))
SUCCZ146_IN_GA(zero(T250), one(T250)) → BINARYZ43_IN_G(T250)
SUCCZ146_IN_GA(one(T256), zero(T258)) → U12_GA(T256, T258, succ153_in_ga(T256, T258))
SUCCZ146_IN_GA(one(T256), zero(T258)) → SUCC153_IN_GA(T256, T258)
SUCC153_IN_GA(zero(T263), one(T263)) → U9_GA(T263, binaryZ43_in_g(T263))
SUCC153_IN_GA(zero(T263), one(T263)) → BINARYZ43_IN_G(T263)
SUCC153_IN_GA(one(T269), zero(T271)) → U10_GA(T269, T271, succ153_in_ga(T269, T271))
SUCC153_IN_GA(one(T269), zero(T271)) → SUCC153_IN_GA(T269, T271)
ADDC136_IN_GGA(b, T280, T282) → U22_GGA(T280, T282, succZ146_in_ga(T280, T282))
ADDC136_IN_GGA(b, T280, T282) → SUCCZ146_IN_GA(T280, T282)
ADDC136_IN_GGA(T294, T295, T297) → U23_GGA(T294, T295, T297, addC171_in_gga(T294, T295, T297))
ADDC136_IN_GGA(T294, T295, T297) → ADDC171_IN_GGA(T294, T295, T297)
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → U13_GGA(T313, T314, T316, addz101_in_gga(T313, T314, T316))
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → ADDZ101_IN_GGA(T313, T314, T316)
ADDC171_IN_GGA(zero(zero(T341)), one(b), zero(one(T341))) → U14_GGA(T341, binaryZ43_in_g(T341))
ADDC171_IN_GGA(zero(zero(T341)), one(b), zero(one(T341))) → BINARYZ43_IN_G(T341)
ADDC171_IN_GGA(zero(one(T351)), one(b), zero(zero(T353))) → U15_GGA(T351, T353, succ153_in_ga(T351, T353))
ADDC171_IN_GGA(zero(one(T351)), one(b), zero(zero(T353))) → SUCC153_IN_GA(T351, T353)
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → U16_GGA(T364, T365, T367, addC171_in_gga(T364, T365, T367))
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → ADDC171_IN_GGA(T364, T365, T367)
ADDC171_IN_GGA(one(b), zero(zero(T392)), zero(one(T392))) → U17_GGA(T392, binaryZ43_in_g(T392))
ADDC171_IN_GGA(one(b), zero(zero(T392)), zero(one(T392))) → BINARYZ43_IN_G(T392)
ADDC171_IN_GGA(one(b), zero(one(T402)), zero(zero(T404))) → U18_GGA(T402, T404, succ153_in_ga(T402, T404))
ADDC171_IN_GGA(one(b), zero(one(T402)), zero(zero(T404))) → SUCC153_IN_GA(T402, T404)
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → U19_GGA(T415, T416, T418, addC171_in_gga(T415, T416, T418))
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → ADDC171_IN_GGA(T415, T416, T418)
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → U20_GGA(T428, T429, T431, addc136_in_gga(T428, T429, T431))
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → ADDC136_IN_GGA(T428, T429, T431)
ADD1_IN_GGA(zero(T444), one(T445), one(T447)) → U35_GGA(T444, T445, T447, addx110_in_gga(T444, T445, T447))
ADD1_IN_GGA(zero(T444), one(T445), one(T447)) → ADDX110_IN_GGA(T444, T445, T447)
ADD1_IN_GGA(one(T461), zero(T462), one(T464)) → U36_GGA(T461, T462, T464, addy124_in_gga(T461, T462, T464))
ADD1_IN_GGA(one(T461), zero(T462), one(T464)) → ADDY124_IN_GGA(T461, T462, T464)
ADD1_IN_GGA(one(T472), one(T473), zero(T475)) → U37_GGA(T472, T473, T475, addc136_in_gga(T472, T473, T475))
ADD1_IN_GGA(one(T472), one(T473), zero(T475)) → ADDC136_IN_GGA(T472, T473, T475)

The TRS R consists of the following rules:

add1_in_gga(b, b, b) → add1_out_gga(b, b, b)
add1_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZ43_in_g(T23))
binaryZ43_in_g(zero(T29)) → U1_g(T29, binaryZ43_in_g(T29))
binaryZ43_in_g(one(T33)) → U2_g(T33, binary50_in_g(T33))
binary50_in_g(b) → binary50_out_g(b)
binary50_in_g(zero(T38)) → U3_g(T38, binaryZ43_in_g(T38))
U3_g(T38, binaryZ43_out_g(T38)) → binary50_out_g(zero(T38))
binary50_in_g(one(T42)) → U4_g(T42, binary50_in_g(T42))
U4_g(T42, binary50_out_g(T42)) → binary50_out_g(one(T42))
U2_g(T33, binary50_out_g(T33)) → binaryZ43_out_g(one(T33))
U1_g(T29, binaryZ43_out_g(T29)) → binaryZ43_out_g(zero(T29))
U30_gga(T23, binaryZ43_out_g(T23)) → add1_out_gga(zero(T23), b, zero(T23))
add1_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binary50_in_g(T47))
U31_gga(T47, binary50_out_g(T47)) → add1_out_gga(one(T47), b, one(T47))
add1_in_gga(b, zero(T74), zero(T74)) → U32_gga(T74, binaryZ43_in_g(T74))
U32_gga(T74, binaryZ43_out_g(T74)) → add1_out_gga(b, zero(T74), zero(T74))
add1_in_gga(b, one(T80), one(T80)) → U33_gga(T80, binary50_in_g(T80))
U33_gga(T80, binary50_out_g(T80)) → add1_out_gga(b, one(T80), one(T80))
add1_in_gga(zero(T108), zero(T109), zero(T111)) → U34_gga(T108, T109, T111, addz101_in_gga(T108, T109, T111))
addz101_in_gga(zero(T127), zero(T128), zero(T130)) → U5_gga(T127, T128, T130, addz101_in_gga(T127, T128, T130))
addz101_in_gga(zero(T146), one(T147), one(T149)) → U6_gga(T146, T147, T149, addx110_in_gga(T146, T147, T149))
addx110_in_gga(one(T155), b, one(T155)) → U24_gga(T155, binary50_in_g(T155))
U24_gga(T155, binary50_out_g(T155)) → addx110_out_gga(one(T155), b, one(T155))
addx110_in_gga(zero(T160), b, zero(T160)) → U25_gga(T160, binaryZ43_in_g(T160))
U25_gga(T160, binaryZ43_out_g(T160)) → addx110_out_gga(zero(T160), b, zero(T160))
addx110_in_gga(T172, T173, T175) → U26_gga(T172, T173, T175, addz101_in_gga(T172, T173, T175))
addz101_in_gga(one(T191), zero(T192), one(T194)) → U7_gga(T191, T192, T194, addy124_in_gga(T191, T192, T194))
addy124_in_gga(b, one(T200), one(T200)) → U27_gga(T200, binary50_in_g(T200))
U27_gga(T200, binary50_out_g(T200)) → addy124_out_gga(b, one(T200), one(T200))
addy124_in_gga(b, zero(T205), zero(T205)) → U28_gga(T205, binaryZ43_in_g(T205))
U28_gga(T205, binaryZ43_out_g(T205)) → addy124_out_gga(b, zero(T205), zero(T205))
addy124_in_gga(T217, T218, T220) → U29_gga(T217, T218, T220, addz101_in_gga(T217, T218, T220))
addz101_in_gga(one(T230), one(T231), zero(T233)) → U8_gga(T230, T231, T233, addc136_in_gga(T230, T231, T233))
addc136_in_gga(b, b, one(b)) → addc136_out_gga(b, b, one(b))
addc136_in_gga(T242, b, T244) → U21_gga(T242, T244, succZ146_in_ga(T242, T244))
succZ146_in_ga(zero(T250), one(T250)) → U11_ga(T250, binaryZ43_in_g(T250))
U11_ga(T250, binaryZ43_out_g(T250)) → succZ146_out_ga(zero(T250), one(T250))
succZ146_in_ga(one(T256), zero(T258)) → U12_ga(T256, T258, succ153_in_ga(T256, T258))
succ153_in_ga(b, one(b)) → succ153_out_ga(b, one(b))
succ153_in_ga(zero(T263), one(T263)) → U9_ga(T263, binaryZ43_in_g(T263))
U9_ga(T263, binaryZ43_out_g(T263)) → succ153_out_ga(zero(T263), one(T263))
succ153_in_ga(one(T269), zero(T271)) → U10_ga(T269, T271, succ153_in_ga(T269, T271))
U10_ga(T269, T271, succ153_out_ga(T269, T271)) → succ153_out_ga(one(T269), zero(T271))
U12_ga(T256, T258, succ153_out_ga(T256, T258)) → succZ146_out_ga(one(T256), zero(T258))
U21_gga(T242, T244, succZ146_out_ga(T242, T244)) → addc136_out_gga(T242, b, T244)
addc136_in_gga(b, T280, T282) → U22_gga(T280, T282, succZ146_in_ga(T280, T282))
U22_gga(T280, T282, succZ146_out_ga(T280, T282)) → addc136_out_gga(b, T280, T282)
addc136_in_gga(T294, T295, T297) → U23_gga(T294, T295, T297, addC171_in_gga(T294, T295, T297))
addC171_in_gga(zero(T313), zero(T314), one(T316)) → U13_gga(T313, T314, T316, addz101_in_gga(T313, T314, T316))
U13_gga(T313, T314, T316, addz101_out_gga(T313, T314, T316)) → addC171_out_gga(zero(T313), zero(T314), one(T316))
addC171_in_gga(zero(zero(T341)), one(b), zero(one(T341))) → U14_gga(T341, binaryZ43_in_g(T341))
U14_gga(T341, binaryZ43_out_g(T341)) → addC171_out_gga(zero(zero(T341)), one(b), zero(one(T341)))
addC171_in_gga(zero(one(T351)), one(b), zero(zero(T353))) → U15_gga(T351, T353, succ153_in_ga(T351, T353))
U15_gga(T351, T353, succ153_out_ga(T351, T353)) → addC171_out_gga(zero(one(T351)), one(b), zero(zero(T353)))
addC171_in_gga(zero(T364), one(T365), zero(T367)) → U16_gga(T364, T365, T367, addC171_in_gga(T364, T365, T367))
addC171_in_gga(one(b), zero(zero(T392)), zero(one(T392))) → U17_gga(T392, binaryZ43_in_g(T392))
U17_gga(T392, binaryZ43_out_g(T392)) → addC171_out_gga(one(b), zero(zero(T392)), zero(one(T392)))
addC171_in_gga(one(b), zero(one(T402)), zero(zero(T404))) → U18_gga(T402, T404, succ153_in_ga(T402, T404))
U18_gga(T402, T404, succ153_out_ga(T402, T404)) → addC171_out_gga(one(b), zero(one(T402)), zero(zero(T404)))
addC171_in_gga(one(T415), zero(T416), zero(T418)) → U19_gga(T415, T416, T418, addC171_in_gga(T415, T416, T418))
addC171_in_gga(one(T428), one(T429), one(T431)) → U20_gga(T428, T429, T431, addc136_in_gga(T428, T429, T431))
U20_gga(T428, T429, T431, addc136_out_gga(T428, T429, T431)) → addC171_out_gga(one(T428), one(T429), one(T431))
U19_gga(T415, T416, T418, addC171_out_gga(T415, T416, T418)) → addC171_out_gga(one(T415), zero(T416), zero(T418))
U16_gga(T364, T365, T367, addC171_out_gga(T364, T365, T367)) → addC171_out_gga(zero(T364), one(T365), zero(T367))
U23_gga(T294, T295, T297, addC171_out_gga(T294, T295, T297)) → addc136_out_gga(T294, T295, T297)
U8_gga(T230, T231, T233, addc136_out_gga(T230, T231, T233)) → addz101_out_gga(one(T230), one(T231), zero(T233))
U29_gga(T217, T218, T220, addz101_out_gga(T217, T218, T220)) → addy124_out_gga(T217, T218, T220)
U7_gga(T191, T192, T194, addy124_out_gga(T191, T192, T194)) → addz101_out_gga(one(T191), zero(T192), one(T194))
U26_gga(T172, T173, T175, addz101_out_gga(T172, T173, T175)) → addx110_out_gga(T172, T173, T175)
U6_gga(T146, T147, T149, addx110_out_gga(T146, T147, T149)) → addz101_out_gga(zero(T146), one(T147), one(T149))
U5_gga(T127, T128, T130, addz101_out_gga(T127, T128, T130)) → addz101_out_gga(zero(T127), zero(T128), zero(T130))
U34_gga(T108, T109, T111, addz101_out_gga(T108, T109, T111)) → add1_out_gga(zero(T108), zero(T109), zero(T111))
add1_in_gga(zero(T444), one(T445), one(T447)) → U35_gga(T444, T445, T447, addx110_in_gga(T444, T445, T447))
U35_gga(T444, T445, T447, addx110_out_gga(T444, T445, T447)) → add1_out_gga(zero(T444), one(T445), one(T447))
add1_in_gga(one(T461), zero(T462), one(T464)) → U36_gga(T461, T462, T464, addy124_in_gga(T461, T462, T464))
U36_gga(T461, T462, T464, addy124_out_gga(T461, T462, T464)) → add1_out_gga(one(T461), zero(T462), one(T464))
add1_in_gga(one(T472), one(T473), zero(T475)) → U37_gga(T472, T473, T475, addc136_in_gga(T472, T473, T475))
U37_gga(T472, T473, T475, addc136_out_gga(T472, T473, T475)) → add1_out_gga(one(T472), one(T473), zero(T475))

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)

The TRS R consists of the following rules:

add1_in_gga(b, b, b) → add1_out_gga(b, b, b)
add1_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZ43_in_g(T23))
binaryZ43_in_g(zero(T29)) → U1_g(T29, binaryZ43_in_g(T29))
binaryZ43_in_g(one(T33)) → U2_g(T33, binary50_in_g(T33))
binary50_in_g(b) → binary50_out_g(b)
binary50_in_g(zero(T38)) → U3_g(T38, binaryZ43_in_g(T38))
U3_g(T38, binaryZ43_out_g(T38)) → binary50_out_g(zero(T38))
binary50_in_g(one(T42)) → U4_g(T42, binary50_in_g(T42))
U4_g(T42, binary50_out_g(T42)) → binary50_out_g(one(T42))
U2_g(T33, binary50_out_g(T33)) → binaryZ43_out_g(one(T33))
U1_g(T29, binaryZ43_out_g(T29)) → binaryZ43_out_g(zero(T29))
U30_gga(T23, binaryZ43_out_g(T23)) → add1_out_gga(zero(T23), b, zero(T23))
add1_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binary50_in_g(T47))
U31_gga(T47, binary50_out_g(T47)) → add1_out_gga(one(T47), b, one(T47))
add1_in_gga(b, zero(T74), zero(T74)) → U32_gga(T74, binaryZ43_in_g(T74))
U32_gga(T74, binaryZ43_out_g(T74)) → add1_out_gga(b, zero(T74), zero(T74))
add1_in_gga(b, one(T80), one(T80)) → U33_gga(T80, binary50_in_g(T80))
U33_gga(T80, binary50_out_g(T80)) → add1_out_gga(b, one(T80), one(T80))
add1_in_gga(zero(T108), zero(T109), zero(T111)) → U34_gga(T108, T109, T111, addz101_in_gga(T108, T109, T111))
addz101_in_gga(zero(T127), zero(T128), zero(T130)) → U5_gga(T127, T128, T130, addz101_in_gga(T127, T128, T130))
addz101_in_gga(zero(T146), one(T147), one(T149)) → U6_gga(T146, T147, T149, addx110_in_gga(T146, T147, T149))
addx110_in_gga(one(T155), b, one(T155)) → U24_gga(T155, binary50_in_g(T155))
U24_gga(T155, binary50_out_g(T155)) → addx110_out_gga(one(T155), b, one(T155))
addx110_in_gga(zero(T160), b, zero(T160)) → U25_gga(T160, binaryZ43_in_g(T160))
U25_gga(T160, binaryZ43_out_g(T160)) → addx110_out_gga(zero(T160), b, zero(T160))
addx110_in_gga(T172, T173, T175) → U26_gga(T172, T173, T175, addz101_in_gga(T172, T173, T175))
addz101_in_gga(one(T191), zero(T192), one(T194)) → U7_gga(T191, T192, T194, addy124_in_gga(T191, T192, T194))
addy124_in_gga(b, one(T200), one(T200)) → U27_gga(T200, binary50_in_g(T200))
U27_gga(T200, binary50_out_g(T200)) → addy124_out_gga(b, one(T200), one(T200))
addy124_in_gga(b, zero(T205), zero(T205)) → U28_gga(T205, binaryZ43_in_g(T205))
U28_gga(T205, binaryZ43_out_g(T205)) → addy124_out_gga(b, zero(T205), zero(T205))
addy124_in_gga(T217, T218, T220) → U29_gga(T217, T218, T220, addz101_in_gga(T217, T218, T220))
addz101_in_gga(one(T230), one(T231), zero(T233)) → U8_gga(T230, T231, T233, addc136_in_gga(T230, T231, T233))
addc136_in_gga(b, b, one(b)) → addc136_out_gga(b, b, one(b))
addc136_in_gga(T242, b, T244) → U21_gga(T242, T244, succZ146_in_ga(T242, T244))
succZ146_in_ga(zero(T250), one(T250)) → U11_ga(T250, binaryZ43_in_g(T250))
U11_ga(T250, binaryZ43_out_g(T250)) → succZ146_out_ga(zero(T250), one(T250))
succZ146_in_ga(one(T256), zero(T258)) → U12_ga(T256, T258, succ153_in_ga(T256, T258))
succ153_in_ga(b, one(b)) → succ153_out_ga(b, one(b))
succ153_in_ga(zero(T263), one(T263)) → U9_ga(T263, binaryZ43_in_g(T263))
U9_ga(T263, binaryZ43_out_g(T263)) → succ153_out_ga(zero(T263), one(T263))
succ153_in_ga(one(T269), zero(T271)) → U10_ga(T269, T271, succ153_in_ga(T269, T271))
U10_ga(T269, T271, succ153_out_ga(T269, T271)) → succ153_out_ga(one(T269), zero(T271))
U12_ga(T256, T258, succ153_out_ga(T256, T258)) → succZ146_out_ga(one(T256), zero(T258))
U21_gga(T242, T244, succZ146_out_ga(T242, T244)) → addc136_out_gga(T242, b, T244)
addc136_in_gga(b, T280, T282) → U22_gga(T280, T282, succZ146_in_ga(T280, T282))
U22_gga(T280, T282, succZ146_out_ga(T280, T282)) → addc136_out_gga(b, T280, T282)
addc136_in_gga(T294, T295, T297) → U23_gga(T294, T295, T297, addC171_in_gga(T294, T295, T297))
addC171_in_gga(zero(T313), zero(T314), one(T316)) → U13_gga(T313, T314, T316, addz101_in_gga(T313, T314, T316))
U13_gga(T313, T314, T316, addz101_out_gga(T313, T314, T316)) → addC171_out_gga(zero(T313), zero(T314), one(T316))
addC171_in_gga(zero(zero(T341)), one(b), zero(one(T341))) → U14_gga(T341, binaryZ43_in_g(T341))
U14_gga(T341, binaryZ43_out_g(T341)) → addC171_out_gga(zero(zero(T341)), one(b), zero(one(T341)))
addC171_in_gga(zero(one(T351)), one(b), zero(zero(T353))) → U15_gga(T351, T353, succ153_in_ga(T351, T353))
U15_gga(T351, T353, succ153_out_ga(T351, T353)) → addC171_out_gga(zero(one(T351)), one(b), zero(zero(T353)))
addC171_in_gga(zero(T364), one(T365), zero(T367)) → U16_gga(T364, T365, T367, addC171_in_gga(T364, T365, T367))
addC171_in_gga(one(b), zero(zero(T392)), zero(one(T392))) → U17_gga(T392, binaryZ43_in_g(T392))
U17_gga(T392, binaryZ43_out_g(T392)) → addC171_out_gga(one(b), zero(zero(T392)), zero(one(T392)))
addC171_in_gga(one(b), zero(one(T402)), zero(zero(T404))) → U18_gga(T402, T404, succ153_in_ga(T402, T404))
U18_gga(T402, T404, succ153_out_ga(T402, T404)) → addC171_out_gga(one(b), zero(one(T402)), zero(zero(T404)))
addC171_in_gga(one(T415), zero(T416), zero(T418)) → U19_gga(T415, T416, T418, addC171_in_gga(T415, T416, T418))
addC171_in_gga(one(T428), one(T429), one(T431)) → U20_gga(T428, T429, T431, addc136_in_gga(T428, T429, T431))
U20_gga(T428, T429, T431, addc136_out_gga(T428, T429, T431)) → addC171_out_gga(one(T428), one(T429), one(T431))
U19_gga(T415, T416, T418, addC171_out_gga(T415, T416, T418)) → addC171_out_gga(one(T415), zero(T416), zero(T418))
U16_gga(T364, T365, T367, addC171_out_gga(T364, T365, T367)) → addC171_out_gga(zero(T364), one(T365), zero(T367))
U23_gga(T294, T295, T297, addC171_out_gga(T294, T295, T297)) → addc136_out_gga(T294, T295, T297)
U8_gga(T230, T231, T233, addc136_out_gga(T230, T231, T233)) → addz101_out_gga(one(T230), one(T231), zero(T233))
U29_gga(T217, T218, T220, addz101_out_gga(T217, T218, T220)) → addy124_out_gga(T217, T218, T220)
U7_gga(T191, T192, T194, addy124_out_gga(T191, T192, T194)) → addz101_out_gga(one(T191), zero(T192), one(T194))
U26_gga(T172, T173, T175, addz101_out_gga(T172, T173, T175)) → addx110_out_gga(T172, T173, T175)
U6_gga(T146, T147, T149, addx110_out_gga(T146, T147, T149)) → addz101_out_gga(zero(T146), one(T147), one(T149))
U5_gga(T127, T128, T130, addz101_out_gga(T127, T128, T130)) → addz101_out_gga(zero(T127), zero(T128), zero(T130))
U34_gga(T108, T109, T111, addz101_out_gga(T108, T109, T111)) → add1_out_gga(zero(T108), zero(T109), zero(T111))
add1_in_gga(zero(T444), one(T445), one(T447)) → U35_gga(T444, T445, T447, addx110_in_gga(T444, T445, T447))
U35_gga(T444, T445, T447, addx110_out_gga(T444, T445, T447)) → add1_out_gga(zero(T444), one(T445), one(T447))
add1_in_gga(one(T461), zero(T462), one(T464)) → U36_gga(T461, T462, T464, addy124_in_gga(T461, T462, T464))
U36_gga(T461, T462, T464, addy124_out_gga(T461, T462, T464)) → add1_out_gga(one(T461), zero(T462), one(T464))
add1_in_gga(one(T472), one(T473), zero(T475)) → U37_gga(T472, T473, T475, addc136_in_gga(T472, T473, T475))
U37_gga(T472, T473, T475, addc136_out_gga(T472, T473, T475)) → add1_out_gga(one(T472), one(T473), zero(T475))

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)

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

(12) PiDPToQDPProof (EQUIVALENT transformation)

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

(13) Obligation:

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

BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(15) YES

(16) Obligation:

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

SUCC153_IN_GA(one(T269), zero(T271)) → SUCC153_IN_GA(T269, T271)

The TRS R consists of the following rules:

add1_in_gga(b, b, b) → add1_out_gga(b, b, b)
add1_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZ43_in_g(T23))
binaryZ43_in_g(zero(T29)) → U1_g(T29, binaryZ43_in_g(T29))
binaryZ43_in_g(one(T33)) → U2_g(T33, binary50_in_g(T33))
binary50_in_g(b) → binary50_out_g(b)
binary50_in_g(zero(T38)) → U3_g(T38, binaryZ43_in_g(T38))
U3_g(T38, binaryZ43_out_g(T38)) → binary50_out_g(zero(T38))
binary50_in_g(one(T42)) → U4_g(T42, binary50_in_g(T42))
U4_g(T42, binary50_out_g(T42)) → binary50_out_g(one(T42))
U2_g(T33, binary50_out_g(T33)) → binaryZ43_out_g(one(T33))
U1_g(T29, binaryZ43_out_g(T29)) → binaryZ43_out_g(zero(T29))
U30_gga(T23, binaryZ43_out_g(T23)) → add1_out_gga(zero(T23), b, zero(T23))
add1_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binary50_in_g(T47))
U31_gga(T47, binary50_out_g(T47)) → add1_out_gga(one(T47), b, one(T47))
add1_in_gga(b, zero(T74), zero(T74)) → U32_gga(T74, binaryZ43_in_g(T74))
U32_gga(T74, binaryZ43_out_g(T74)) → add1_out_gga(b, zero(T74), zero(T74))
add1_in_gga(b, one(T80), one(T80)) → U33_gga(T80, binary50_in_g(T80))
U33_gga(T80, binary50_out_g(T80)) → add1_out_gga(b, one(T80), one(T80))
add1_in_gga(zero(T108), zero(T109), zero(T111)) → U34_gga(T108, T109, T111, addz101_in_gga(T108, T109, T111))
addz101_in_gga(zero(T127), zero(T128), zero(T130)) → U5_gga(T127, T128, T130, addz101_in_gga(T127, T128, T130))
addz101_in_gga(zero(T146), one(T147), one(T149)) → U6_gga(T146, T147, T149, addx110_in_gga(T146, T147, T149))
addx110_in_gga(one(T155), b, one(T155)) → U24_gga(T155, binary50_in_g(T155))
U24_gga(T155, binary50_out_g(T155)) → addx110_out_gga(one(T155), b, one(T155))
addx110_in_gga(zero(T160), b, zero(T160)) → U25_gga(T160, binaryZ43_in_g(T160))
U25_gga(T160, binaryZ43_out_g(T160)) → addx110_out_gga(zero(T160), b, zero(T160))
addx110_in_gga(T172, T173, T175) → U26_gga(T172, T173, T175, addz101_in_gga(T172, T173, T175))
addz101_in_gga(one(T191), zero(T192), one(T194)) → U7_gga(T191, T192, T194, addy124_in_gga(T191, T192, T194))
addy124_in_gga(b, one(T200), one(T200)) → U27_gga(T200, binary50_in_g(T200))
U27_gga(T200, binary50_out_g(T200)) → addy124_out_gga(b, one(T200), one(T200))
addy124_in_gga(b, zero(T205), zero(T205)) → U28_gga(T205, binaryZ43_in_g(T205))
U28_gga(T205, binaryZ43_out_g(T205)) → addy124_out_gga(b, zero(T205), zero(T205))
addy124_in_gga(T217, T218, T220) → U29_gga(T217, T218, T220, addz101_in_gga(T217, T218, T220))
addz101_in_gga(one(T230), one(T231), zero(T233)) → U8_gga(T230, T231, T233, addc136_in_gga(T230, T231, T233))
addc136_in_gga(b, b, one(b)) → addc136_out_gga(b, b, one(b))
addc136_in_gga(T242, b, T244) → U21_gga(T242, T244, succZ146_in_ga(T242, T244))
succZ146_in_ga(zero(T250), one(T250)) → U11_ga(T250, binaryZ43_in_g(T250))
U11_ga(T250, binaryZ43_out_g(T250)) → succZ146_out_ga(zero(T250), one(T250))
succZ146_in_ga(one(T256), zero(T258)) → U12_ga(T256, T258, succ153_in_ga(T256, T258))
succ153_in_ga(b, one(b)) → succ153_out_ga(b, one(b))
succ153_in_ga(zero(T263), one(T263)) → U9_ga(T263, binaryZ43_in_g(T263))
U9_ga(T263, binaryZ43_out_g(T263)) → succ153_out_ga(zero(T263), one(T263))
succ153_in_ga(one(T269), zero(T271)) → U10_ga(T269, T271, succ153_in_ga(T269, T271))
U10_ga(T269, T271, succ153_out_ga(T269, T271)) → succ153_out_ga(one(T269), zero(T271))
U12_ga(T256, T258, succ153_out_ga(T256, T258)) → succZ146_out_ga(one(T256), zero(T258))
U21_gga(T242, T244, succZ146_out_ga(T242, T244)) → addc136_out_gga(T242, b, T244)
addc136_in_gga(b, T280, T282) → U22_gga(T280, T282, succZ146_in_ga(T280, T282))
U22_gga(T280, T282, succZ146_out_ga(T280, T282)) → addc136_out_gga(b, T280, T282)
addc136_in_gga(T294, T295, T297) → U23_gga(T294, T295, T297, addC171_in_gga(T294, T295, T297))
addC171_in_gga(zero(T313), zero(T314), one(T316)) → U13_gga(T313, T314, T316, addz101_in_gga(T313, T314, T316))
U13_gga(T313, T314, T316, addz101_out_gga(T313, T314, T316)) → addC171_out_gga(zero(T313), zero(T314), one(T316))
addC171_in_gga(zero(zero(T341)), one(b), zero(one(T341))) → U14_gga(T341, binaryZ43_in_g(T341))
U14_gga(T341, binaryZ43_out_g(T341)) → addC171_out_gga(zero(zero(T341)), one(b), zero(one(T341)))
addC171_in_gga(zero(one(T351)), one(b), zero(zero(T353))) → U15_gga(T351, T353, succ153_in_ga(T351, T353))
U15_gga(T351, T353, succ153_out_ga(T351, T353)) → addC171_out_gga(zero(one(T351)), one(b), zero(zero(T353)))
addC171_in_gga(zero(T364), one(T365), zero(T367)) → U16_gga(T364, T365, T367, addC171_in_gga(T364, T365, T367))
addC171_in_gga(one(b), zero(zero(T392)), zero(one(T392))) → U17_gga(T392, binaryZ43_in_g(T392))
U17_gga(T392, binaryZ43_out_g(T392)) → addC171_out_gga(one(b), zero(zero(T392)), zero(one(T392)))
addC171_in_gga(one(b), zero(one(T402)), zero(zero(T404))) → U18_gga(T402, T404, succ153_in_ga(T402, T404))
U18_gga(T402, T404, succ153_out_ga(T402, T404)) → addC171_out_gga(one(b), zero(one(T402)), zero(zero(T404)))
addC171_in_gga(one(T415), zero(T416), zero(T418)) → U19_gga(T415, T416, T418, addC171_in_gga(T415, T416, T418))
addC171_in_gga(one(T428), one(T429), one(T431)) → U20_gga(T428, T429, T431, addc136_in_gga(T428, T429, T431))
U20_gga(T428, T429, T431, addc136_out_gga(T428, T429, T431)) → addC171_out_gga(one(T428), one(T429), one(T431))
U19_gga(T415, T416, T418, addC171_out_gga(T415, T416, T418)) → addC171_out_gga(one(T415), zero(T416), zero(T418))
U16_gga(T364, T365, T367, addC171_out_gga(T364, T365, T367)) → addC171_out_gga(zero(T364), one(T365), zero(T367))
U23_gga(T294, T295, T297, addC171_out_gga(T294, T295, T297)) → addc136_out_gga(T294, T295, T297)
U8_gga(T230, T231, T233, addc136_out_gga(T230, T231, T233)) → addz101_out_gga(one(T230), one(T231), zero(T233))
U29_gga(T217, T218, T220, addz101_out_gga(T217, T218, T220)) → addy124_out_gga(T217, T218, T220)
U7_gga(T191, T192, T194, addy124_out_gga(T191, T192, T194)) → addz101_out_gga(one(T191), zero(T192), one(T194))
U26_gga(T172, T173, T175, addz101_out_gga(T172, T173, T175)) → addx110_out_gga(T172, T173, T175)
U6_gga(T146, T147, T149, addx110_out_gga(T146, T147, T149)) → addz101_out_gga(zero(T146), one(T147), one(T149))
U5_gga(T127, T128, T130, addz101_out_gga(T127, T128, T130)) → addz101_out_gga(zero(T127), zero(T128), zero(T130))
U34_gga(T108, T109, T111, addz101_out_gga(T108, T109, T111)) → add1_out_gga(zero(T108), zero(T109), zero(T111))
add1_in_gga(zero(T444), one(T445), one(T447)) → U35_gga(T444, T445, T447, addx110_in_gga(T444, T445, T447))
U35_gga(T444, T445, T447, addx110_out_gga(T444, T445, T447)) → add1_out_gga(zero(T444), one(T445), one(T447))
add1_in_gga(one(T461), zero(T462), one(T464)) → U36_gga(T461, T462, T464, addy124_in_gga(T461, T462, T464))
U36_gga(T461, T462, T464, addy124_out_gga(T461, T462, T464)) → add1_out_gga(one(T461), zero(T462), one(T464))
add1_in_gga(one(T472), one(T473), zero(T475)) → U37_gga(T472, T473, T475, addc136_in_gga(T472, T473, T475))
U37_gga(T472, T473, T475, addc136_out_gga(T472, T473, T475)) → add1_out_gga(one(T472), one(T473), zero(T475))

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

SUCC153_IN_GA(one(T269), zero(T271)) → SUCC153_IN_GA(T269, T271)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

SUCC153_IN_GA(one(T269)) → SUCC153_IN_GA(T269)

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

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

SUCC153_IN_GA(one(T269)) → SUCC153_IN_GA(T269)
The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

ADDX110_IN_GGA(T172, T173, T175) → ADDZ101_IN_GGA(T172, T173, T175)
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → ADDZ101_IN_GGA(T127, T128, T130)
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → ADDX110_IN_GGA(T146, T147, T149)
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → ADDY124_IN_GGA(T191, T192, T194)
ADDY124_IN_GGA(T217, T218, T220) → ADDZ101_IN_GGA(T217, T218, T220)
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → ADDC136_IN_GGA(T230, T231, T233)
ADDC136_IN_GGA(T294, T295, T297) → ADDC171_IN_GGA(T294, T295, T297)
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → ADDZ101_IN_GGA(T313, T314, T316)
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → ADDC171_IN_GGA(T364, T365, T367)
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → ADDC171_IN_GGA(T415, T416, T418)
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → ADDC136_IN_GGA(T428, T429, T431)

The TRS R consists of the following rules:

add1_in_gga(b, b, b) → add1_out_gga(b, b, b)
add1_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZ43_in_g(T23))
binaryZ43_in_g(zero(T29)) → U1_g(T29, binaryZ43_in_g(T29))
binaryZ43_in_g(one(T33)) → U2_g(T33, binary50_in_g(T33))
binary50_in_g(b) → binary50_out_g(b)
binary50_in_g(zero(T38)) → U3_g(T38, binaryZ43_in_g(T38))
U3_g(T38, binaryZ43_out_g(T38)) → binary50_out_g(zero(T38))
binary50_in_g(one(T42)) → U4_g(T42, binary50_in_g(T42))
U4_g(T42, binary50_out_g(T42)) → binary50_out_g(one(T42))
U2_g(T33, binary50_out_g(T33)) → binaryZ43_out_g(one(T33))
U1_g(T29, binaryZ43_out_g(T29)) → binaryZ43_out_g(zero(T29))
U30_gga(T23, binaryZ43_out_g(T23)) → add1_out_gga(zero(T23), b, zero(T23))
add1_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binary50_in_g(T47))
U31_gga(T47, binary50_out_g(T47)) → add1_out_gga(one(T47), b, one(T47))
add1_in_gga(b, zero(T74), zero(T74)) → U32_gga(T74, binaryZ43_in_g(T74))
U32_gga(T74, binaryZ43_out_g(T74)) → add1_out_gga(b, zero(T74), zero(T74))
add1_in_gga(b, one(T80), one(T80)) → U33_gga(T80, binary50_in_g(T80))
U33_gga(T80, binary50_out_g(T80)) → add1_out_gga(b, one(T80), one(T80))
add1_in_gga(zero(T108), zero(T109), zero(T111)) → U34_gga(T108, T109, T111, addz101_in_gga(T108, T109, T111))
addz101_in_gga(zero(T127), zero(T128), zero(T130)) → U5_gga(T127, T128, T130, addz101_in_gga(T127, T128, T130))
addz101_in_gga(zero(T146), one(T147), one(T149)) → U6_gga(T146, T147, T149, addx110_in_gga(T146, T147, T149))
addx110_in_gga(one(T155), b, one(T155)) → U24_gga(T155, binary50_in_g(T155))
U24_gga(T155, binary50_out_g(T155)) → addx110_out_gga(one(T155), b, one(T155))
addx110_in_gga(zero(T160), b, zero(T160)) → U25_gga(T160, binaryZ43_in_g(T160))
U25_gga(T160, binaryZ43_out_g(T160)) → addx110_out_gga(zero(T160), b, zero(T160))
addx110_in_gga(T172, T173, T175) → U26_gga(T172, T173, T175, addz101_in_gga(T172, T173, T175))
addz101_in_gga(one(T191), zero(T192), one(T194)) → U7_gga(T191, T192, T194, addy124_in_gga(T191, T192, T194))
addy124_in_gga(b, one(T200), one(T200)) → U27_gga(T200, binary50_in_g(T200))
U27_gga(T200, binary50_out_g(T200)) → addy124_out_gga(b, one(T200), one(T200))
addy124_in_gga(b, zero(T205), zero(T205)) → U28_gga(T205, binaryZ43_in_g(T205))
U28_gga(T205, binaryZ43_out_g(T205)) → addy124_out_gga(b, zero(T205), zero(T205))
addy124_in_gga(T217, T218, T220) → U29_gga(T217, T218, T220, addz101_in_gga(T217, T218, T220))
addz101_in_gga(one(T230), one(T231), zero(T233)) → U8_gga(T230, T231, T233, addc136_in_gga(T230, T231, T233))
addc136_in_gga(b, b, one(b)) → addc136_out_gga(b, b, one(b))
addc136_in_gga(T242, b, T244) → U21_gga(T242, T244, succZ146_in_ga(T242, T244))
succZ146_in_ga(zero(T250), one(T250)) → U11_ga(T250, binaryZ43_in_g(T250))
U11_ga(T250, binaryZ43_out_g(T250)) → succZ146_out_ga(zero(T250), one(T250))
succZ146_in_ga(one(T256), zero(T258)) → U12_ga(T256, T258, succ153_in_ga(T256, T258))
succ153_in_ga(b, one(b)) → succ153_out_ga(b, one(b))
succ153_in_ga(zero(T263), one(T263)) → U9_ga(T263, binaryZ43_in_g(T263))
U9_ga(T263, binaryZ43_out_g(T263)) → succ153_out_ga(zero(T263), one(T263))
succ153_in_ga(one(T269), zero(T271)) → U10_ga(T269, T271, succ153_in_ga(T269, T271))
U10_ga(T269, T271, succ153_out_ga(T269, T271)) → succ153_out_ga(one(T269), zero(T271))
U12_ga(T256, T258, succ153_out_ga(T256, T258)) → succZ146_out_ga(one(T256), zero(T258))
U21_gga(T242, T244, succZ146_out_ga(T242, T244)) → addc136_out_gga(T242, b, T244)
addc136_in_gga(b, T280, T282) → U22_gga(T280, T282, succZ146_in_ga(T280, T282))
U22_gga(T280, T282, succZ146_out_ga(T280, T282)) → addc136_out_gga(b, T280, T282)
addc136_in_gga(T294, T295, T297) → U23_gga(T294, T295, T297, addC171_in_gga(T294, T295, T297))
addC171_in_gga(zero(T313), zero(T314), one(T316)) → U13_gga(T313, T314, T316, addz101_in_gga(T313, T314, T316))
U13_gga(T313, T314, T316, addz101_out_gga(T313, T314, T316)) → addC171_out_gga(zero(T313), zero(T314), one(T316))
addC171_in_gga(zero(zero(T341)), one(b), zero(one(T341))) → U14_gga(T341, binaryZ43_in_g(T341))
U14_gga(T341, binaryZ43_out_g(T341)) → addC171_out_gga(zero(zero(T341)), one(b), zero(one(T341)))
addC171_in_gga(zero(one(T351)), one(b), zero(zero(T353))) → U15_gga(T351, T353, succ153_in_ga(T351, T353))
U15_gga(T351, T353, succ153_out_ga(T351, T353)) → addC171_out_gga(zero(one(T351)), one(b), zero(zero(T353)))
addC171_in_gga(zero(T364), one(T365), zero(T367)) → U16_gga(T364, T365, T367, addC171_in_gga(T364, T365, T367))
addC171_in_gga(one(b), zero(zero(T392)), zero(one(T392))) → U17_gga(T392, binaryZ43_in_g(T392))
U17_gga(T392, binaryZ43_out_g(T392)) → addC171_out_gga(one(b), zero(zero(T392)), zero(one(T392)))
addC171_in_gga(one(b), zero(one(T402)), zero(zero(T404))) → U18_gga(T402, T404, succ153_in_ga(T402, T404))
U18_gga(T402, T404, succ153_out_ga(T402, T404)) → addC171_out_gga(one(b), zero(one(T402)), zero(zero(T404)))
addC171_in_gga(one(T415), zero(T416), zero(T418)) → U19_gga(T415, T416, T418, addC171_in_gga(T415, T416, T418))
addC171_in_gga(one(T428), one(T429), one(T431)) → U20_gga(T428, T429, T431, addc136_in_gga(T428, T429, T431))
U20_gga(T428, T429, T431, addc136_out_gga(T428, T429, T431)) → addC171_out_gga(one(T428), one(T429), one(T431))
U19_gga(T415, T416, T418, addC171_out_gga(T415, T416, T418)) → addC171_out_gga(one(T415), zero(T416), zero(T418))
U16_gga(T364, T365, T367, addC171_out_gga(T364, T365, T367)) → addC171_out_gga(zero(T364), one(T365), zero(T367))
U23_gga(T294, T295, T297, addC171_out_gga(T294, T295, T297)) → addc136_out_gga(T294, T295, T297)
U8_gga(T230, T231, T233, addc136_out_gga(T230, T231, T233)) → addz101_out_gga(one(T230), one(T231), zero(T233))
U29_gga(T217, T218, T220, addz101_out_gga(T217, T218, T220)) → addy124_out_gga(T217, T218, T220)
U7_gga(T191, T192, T194, addy124_out_gga(T191, T192, T194)) → addz101_out_gga(one(T191), zero(T192), one(T194))
U26_gga(T172, T173, T175, addz101_out_gga(T172, T173, T175)) → addx110_out_gga(T172, T173, T175)
U6_gga(T146, T147, T149, addx110_out_gga(T146, T147, T149)) → addz101_out_gga(zero(T146), one(T147), one(T149))
U5_gga(T127, T128, T130, addz101_out_gga(T127, T128, T130)) → addz101_out_gga(zero(T127), zero(T128), zero(T130))
U34_gga(T108, T109, T111, addz101_out_gga(T108, T109, T111)) → add1_out_gga(zero(T108), zero(T109), zero(T111))
add1_in_gga(zero(T444), one(T445), one(T447)) → U35_gga(T444, T445, T447, addx110_in_gga(T444, T445, T447))
U35_gga(T444, T445, T447, addx110_out_gga(T444, T445, T447)) → add1_out_gga(zero(T444), one(T445), one(T447))
add1_in_gga(one(T461), zero(T462), one(T464)) → U36_gga(T461, T462, T464, addy124_in_gga(T461, T462, T464))
U36_gga(T461, T462, T464, addy124_out_gga(T461, T462, T464)) → add1_out_gga(one(T461), zero(T462), one(T464))
add1_in_gga(one(T472), one(T473), zero(T475)) → U37_gga(T472, T473, T475, addc136_in_gga(T472, T473, T475))
U37_gga(T472, T473, T475, addc136_out_gga(T472, T473, T475)) → add1_out_gga(one(T472), one(T473), zero(T475))

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

ADDX110_IN_GGA(T172, T173, T175) → ADDZ101_IN_GGA(T172, T173, T175)
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → ADDZ101_IN_GGA(T127, T128, T130)
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → ADDX110_IN_GGA(T146, T147, T149)
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → ADDY124_IN_GGA(T191, T192, T194)
ADDY124_IN_GGA(T217, T218, T220) → ADDZ101_IN_GGA(T217, T218, T220)
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → ADDC136_IN_GGA(T230, T231, T233)
ADDC136_IN_GGA(T294, T295, T297) → ADDC171_IN_GGA(T294, T295, T297)
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → ADDZ101_IN_GGA(T313, T314, T316)
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → ADDC171_IN_GGA(T364, T365, T367)
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → ADDC171_IN_GGA(T415, T416, T418)
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → ADDC136_IN_GGA(T428, T429, T431)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
ADDZ101_IN_GGA(x1, x2, x3) = ADDZ101_IN_GGA(x1, x2)
ADDX110_IN_GGA(x1, x2, x3) = ADDX110_IN_GGA(x1, x2)
ADDY124_IN_GGA(x1, x2, x3) = ADDY124_IN_GGA(x1, x2)
ADDC136_IN_GGA(x1, x2, x3) = ADDC136_IN_GGA(x1, x2)
ADDC171_IN_GGA(x1, x2, x3) = ADDC171_IN_GGA(x1, x2)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

ADDX110_IN_GGA(T172, T173) → ADDZ101_IN_GGA(T172, T173)
ADDZ101_IN_GGA(zero(T127), zero(T128)) → ADDZ101_IN_GGA(T127, T128)
ADDZ101_IN_GGA(zero(T146), one(T147)) → ADDX110_IN_GGA(T146, T147)
ADDZ101_IN_GGA(one(T191), zero(T192)) → ADDY124_IN_GGA(T191, T192)
ADDY124_IN_GGA(T217, T218) → ADDZ101_IN_GGA(T217, T218)
ADDZ101_IN_GGA(one(T230), one(T231)) → ADDC136_IN_GGA(T230, T231)
ADDC136_IN_GGA(T294, T295) → ADDC171_IN_GGA(T294, T295)
ADDC171_IN_GGA(zero(T313), zero(T314)) → ADDZ101_IN_GGA(T313, T314)
ADDC171_IN_GGA(zero(T364), one(T365)) → ADDC171_IN_GGA(T364, T365)
ADDC171_IN_GGA(one(T415), zero(T416)) → ADDC171_IN_GGA(T415, T416)
ADDC171_IN_GGA(one(T428), one(T429)) → ADDC136_IN_GGA(T428, T429)

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

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

ADDZ101_IN_GGA(zero(T146), one(T147)) → ADDX110_IN_GGA(T146, T147)
The graph contains the following edges 1 > 1, 2 > 2
ADDZ101_IN_GGA(zero(T127), zero(T128)) → ADDZ101_IN_GGA(T127, T128)
The graph contains the following edges 1 > 1, 2 > 2
ADDX110_IN_GGA(T172, T173) → ADDZ101_IN_GGA(T172, T173)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDY124_IN_GGA(T217, T218) → ADDZ101_IN_GGA(T217, T218)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDC171_IN_GGA(zero(T313), zero(T314)) → ADDZ101_IN_GGA(T313, T314)
The graph contains the following edges 1 > 1, 2 > 2
ADDZ101_IN_GGA(one(T191), zero(T192)) → ADDY124_IN_GGA(T191, T192)
The graph contains the following edges 1 > 1, 2 > 2
ADDZ101_IN_GGA(one(T230), one(T231)) → ADDC136_IN_GGA(T230, T231)
The graph contains the following edges 1 > 1, 2 > 2
ADDC136_IN_GGA(T294, T295) → ADDC171_IN_GGA(T294, T295)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDC171_IN_GGA(one(T428), one(T429)) → ADDC136_IN_GGA(T428, T429)
The graph contains the following edges 1 > 1, 2 > 2
ADDC171_IN_GGA(zero(T364), one(T365)) → ADDC171_IN_GGA(T364, T365)
The graph contains the following edges 1 > 1, 2 > 2
ADDC171_IN_GGA(one(T415), zero(T416)) → ADDC171_IN_GGA(T415, T416)
The graph contains the following edges 1 > 1, 2 > 2

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) QDPSizeChangeProof (EQUIVALENT transformation)

(29) YES