Left Termination proof of /tmp/tmpG8v

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇐)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇐)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇐)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔)

        ↳34 YES

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇐)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔)

        ↳41 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:

times(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: times(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: times(T1, T2, T3), SCOPE: 1, CLAUSE: 38 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 39 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 39 | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: times(T1, T2, T3), SCOPE: 1, CLAUSE: 39 | times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground\ntimes(T1, T2, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: times(one(b), T5, T3), SCOPE: 1, CLAUSE: 39 | times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: times(one(b), T5, T3), SCOPE: 1, CLAUSE: 40\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(times(b, T8, X13), add(T8, zero(X13), T10))\n\nT8 is ground\nX13 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(times(b, T8, X13), add(T8, zero(X13), T10)), SCOPE: 2, CLAUSE: 38 | ','(times(b, T8, X13), add(T8, zero(X13), T10)), SCOPE: 2, CLAUSE: 39 | ','(times(b, T8, X13), add(T8, zero(X13), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX13 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(times(b, T8, X13), add(T8, zero(X13), T10)), SCOPE: 2, CLAUSE: 39 | ','(times(b, T8, X13), add(T8, zero(X13), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX13 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(times(b, T8, X13), add(T8, zero(X13), T10)), SCOPE: 2, CLAUSE: 40\n\nT8 is ground\nX13 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: times(T14, T15, T17) | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: times(T1, T2, T3), SCOPE: 1, CLAUSE: 40\n\nT1 is ground\nT2 is ground\ntimes(T1, T2, T3) !=? times(one(b), X2, X2)\ntimes(T1, T2, T3) !=? times(zero(X24), X25, zero(X26))", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: times(T14, T15, T17), SCOPE: 3, CLAUSE: 38 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 39 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: times(T14, T15, T17), SCOPE: 3, CLAUSE: 38\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: times(T14, T15, T17), SCOPE: 3, CLAUSE: 39 | times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: times(T14, T15, T17), SCOPE: 3, CLAUSE: 39\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: times(T14, T15, T17), SCOPE: 3, CLAUSE: 40 | ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: times(T35, T36, T38)\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: times(T14, T15, T17), SCOPE: 3, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ?_3 | times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(times(T53, T54, X73), add(T54, zero(X73), T56))\n\nT53 is ground\nT54 is ground\nX73 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: times(T53, T54, X73)\n\nT53 is ground\nT54 is ground\nX73 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: add(T54, zero(T59), T56)\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: times(T53, T54, X73), SCOPE: 4, CLAUSE: 38 | times(T53, T54, X73), SCOPE: 4, CLAUSE: 39 | times(T53, T54, X73), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX73 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: times(T53, T54, X73), SCOPE: 4, CLAUSE: 38\n\nT53 is ground\nT54 is ground\nX73 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: times(T53, T54, X73), SCOPE: 4, CLAUSE: 39 | times(T53, T54, X73), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX73 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: times(T53, T54, X73), SCOPE: 4, CLAUSE: 39\n\nT53 is ground\nT54 is ground\nX73 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: times(T53, T54, X73), SCOPE: 4, CLAUSE: 40\n\nT53 is ground\nT54 is ground\nX73 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: times(T75, T76, X106)\n\nT75 is ground\nT76 is ground\nX106 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(times(T83, T84, X124), add(T84, zero(X124), X125))\n\nT83 is ground\nT84 is ground\nX125 is free; \nX124 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: times(T83, T84, X124)\n\nT83 is ground\nT84 is ground\nX124 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: add(T84, zero(T87), X125)\n\nT84 is ground\nT87 is ground\nX125 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 0 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 1 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 1 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2 | add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 2\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: add(T54, zero(T59), T56), SCOPE: 5, CLAUSE: 3\n\nT54 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: binaryZ(zero(T99))\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: binaryZ(zero(T99)), SCOPE: 6, CLAUSE: 31 | binaryZ(zero(T99)), SCOPE: 6, CLAUSE: 32\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: binaryZ(zero(T99)), SCOPE: 6, CLAUSE: 31\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: binaryZ(zero(T99)), SCOPE: 6, CLAUSE: 32\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: binaryZ(T107)\n\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: binaryZ(T107), SCOPE: 7, CLAUSE: 31 | binaryZ(T107), SCOPE: 7, CLAUSE: 32\n\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: binaryZ(T107), SCOPE: 7, CLAUSE: 31\n\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: binaryZ(T107), SCOPE: 7, CLAUSE: 32\n\nT107 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: binaryZ(T113)\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: binary(T117)\n\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: binary(T117), SCOPE: 8, CLAUSE: 28 | binary(T117), SCOPE: 8, CLAUSE: 29 | binary(T117), SCOPE: 8, CLAUSE: 30\n\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: binary(T117), SCOPE: 8, CLAUSE: 28\n\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: binary(T117), SCOPE: 8, CLAUSE: 29 | binary(T117), SCOPE: 8, CLAUSE: 30\n\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: binary(T117), SCOPE: 8, CLAUSE: 29\n\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: binary(T117), SCOPE: 8, CLAUSE: 30\n\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: binaryZ(T122)\n\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: binary(T126)\n\nT126 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: addz(T137, zero(T138), T140)\n\nT137 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 10 | addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 11 | addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 12 | addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 13\n\nT137 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 10\n\nT137 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 11 | addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 12 | addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 13\n\nT137 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: addz(T156, T157, T159)\n\nT156 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: addz(T156, T157, T159), SCOPE: 10, CLAUSE: 10 | addz(T156, T157, T159), SCOPE: 10, CLAUSE: 11 | addz(T156, T157, T159), SCOPE: 10, CLAUSE: 12 | addz(T156, T157, T159), SCOPE: 10, CLAUSE: 13\n\nT156 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: addz(T156, T157, T159), SCOPE: 10, CLAUSE: 10\n\nT156 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: addz(T156, T157, T159), SCOPE: 10, CLAUSE: 11 | addz(T156, T157, T159), SCOPE: 10, CLAUSE: 12 | addz(T156, T157, T159), SCOPE: 10, CLAUSE: 13\n\nT156 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: addz(T175, T176, T178)\n\nT175 is ground\nT176 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: addz(T156, T157, T159), SCOPE: 10, CLAUSE: 11\n\nT156 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: addz(T156, T157, T159), SCOPE: 10, CLAUSE: 12 | addz(T156, T157, T159), SCOPE: 10, CLAUSE: 13\n\nT156 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: addx(T194, T195, T197)\n\nT194 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: addx(T194, T195, T197), SCOPE: 11, CLAUSE: 4 | addx(T194, T195, T197), SCOPE: 11, CLAUSE: 5 | addx(T194, T195, T197), SCOPE: 11, CLAUSE: 6\n\nT194 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: addx(T194, T195, T197), SCOPE: 11, CLAUSE: 4\n\nT194 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: addx(T194, T195, T197), SCOPE: 11, CLAUSE: 5 | addx(T194, T195, T197), SCOPE: 11, CLAUSE: 6\n\nT194 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: binary(T203)\n\nT203 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: addx(T194, T195, T197), SCOPE: 11, CLAUSE: 5\n\nT194 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: addx(T194, T195, T197), SCOPE: 11, CLAUSE: 6\n\nT194 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: binaryZ(T208)\n\nT208 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: addz(T220, T221, T223)\n\nT220 is ground\nT221 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: addz(T156, T157, T159), SCOPE: 10, CLAUSE: 12\n\nT156 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: addz(T156, T157, T159), SCOPE: 10, CLAUSE: 13\n\nT156 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: addy(T239, T240, T242)\n\nT239 is ground\nT240 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: addy(T239, T240, T242), SCOPE: 12, CLAUSE: 7 | addy(T239, T240, T242), SCOPE: 12, CLAUSE: 8 | addy(T239, T240, T242), SCOPE: 12, CLAUSE: 9\n\nT239 is ground\nT240 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: addy(T239, T240, T242), SCOPE: 12, CLAUSE: 7\n\nT239 is ground\nT240 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: addy(T239, T240, T242), SCOPE: 12, CLAUSE: 8 | addy(T239, T240, T242), SCOPE: 12, CLAUSE: 9\n\nT239 is ground\nT240 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: binary(T248)\n\nT248 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: addy(T239, T240, T242), SCOPE: 12, CLAUSE: 8\n\nT239 is ground\nT240 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: addy(T239, T240, T242), SCOPE: 12, CLAUSE: 9\n\nT239 is ground\nT240 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: binaryZ(T253)\n\nT253 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: addz(T265, T266, T268)\n\nT265 is ground\nT266 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: addc(T278, T279, T281)\n\nT278 is ground\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: addc(T278, T279, T281), SCOPE: 13, CLAUSE: 14 | addc(T278, T279, T281), SCOPE: 13, CLAUSE: 15 | addc(T278, T279, T281), SCOPE: 13, CLAUSE: 16 | addc(T278, T279, T281), SCOPE: 13, CLAUSE: 17\n\nT278 is ground\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: addc(T278, T279, T281), SCOPE: 13, CLAUSE: 14\n\nT278 is ground\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: addc(T278, T279, T281), SCOPE: 13, CLAUSE: 15 | addc(T278, T279, T281), SCOPE: 13, CLAUSE: 16 | addc(T278, T279, T281), SCOPE: 13, CLAUSE: 17\n\nT278 is ground\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: addc(T278, T279, T281), SCOPE: 13, CLAUSE: 15\n\nT278 is ground\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: addc(T278, T279, T281), SCOPE: 13, CLAUSE: 16 | addc(T278, T279, T281), SCOPE: 13, CLAUSE: 17\n\nT278 is ground\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: succZ(T290, T292)\n\nT290 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: succZ(T290, T292), SCOPE: 14, CLAUSE: 36 | succZ(T290, T292), SCOPE: 14, CLAUSE: 37\n\nT290 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: succZ(T290, T292), SCOPE: 14, CLAUSE: 36\n\nT290 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: succZ(T290, T292), SCOPE: 14, CLAUSE: 37\n\nT290 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: binaryZ(T298)\n\nT298 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: succ(T304, T306)\n\nT304 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: succ(T304, T306), SCOPE: 15, CLAUSE: 33 | succ(T304, T306), SCOPE: 15, CLAUSE: 34 | succ(T304, T306), SCOPE: 15, CLAUSE: 35\n\nT304 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: succ(T304, T306), SCOPE: 15, CLAUSE: 33\n\nT304 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: succ(T304, T306), SCOPE: 15, CLAUSE: 34 | succ(T304, T306), SCOPE: 15, CLAUSE: 35\n\nT304 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: succ(T304, T306), SCOPE: 15, CLAUSE: 34\n\nT304 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: succ(T304, T306), SCOPE: 15, CLAUSE: 35\n\nT304 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: binaryZ(T311)\n\nT311 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: succ(T317, T319)\n\nT317 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: addc(T278, T279, T281), SCOPE: 13, CLAUSE: 16\n\nT278 is ground\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: addc(T278, T279, T281), SCOPE: 13, CLAUSE: 17\n\nT278 is ground\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: succZ(T328, T330)\n\nT328 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: addC(T342, T343, T345)\n\nT342 is ground\nT343 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: addC(T342, T343, T345), SCOPE: 16, CLAUSE: 24 | addC(T342, T343, T345), SCOPE: 16, CLAUSE: 25 | addC(T342, T343, T345), SCOPE: 16, CLAUSE: 26 | addC(T342, T343, T345), SCOPE: 16, CLAUSE: 27\n\nT342 is ground\nT343 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: addC(T342, T343, T345), SCOPE: 16, CLAUSE: 24\n\nT342 is ground\nT343 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: addC(T342, T343, T345), SCOPE: 16, CLAUSE: 25 | addC(T342, T343, T345), SCOPE: 16, CLAUSE: 26 | addC(T342, T343, T345), SCOPE: 16, CLAUSE: 27\n\nT342 is ground\nT343 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: addz(T361, T362, T364)\n\nT361 is ground\nT362 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: addC(T342, T343, T345), SCOPE: 16, CLAUSE: 25\n\nT342 is ground\nT343 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: addC(T342, T343, T345), SCOPE: 16, CLAUSE: 26 | addC(T342, T343, T345), SCOPE: 16, CLAUSE: 27\n\nT342 is ground\nT343 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: addX(T380, T381, T383)\n\nT380 is ground\nT381 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: addX(T380, T381, T383), SCOPE: 17, CLAUSE: 18 | addX(T380, T381, T383), SCOPE: 17, CLAUSE: 19 | addX(T380, T381, T383), SCOPE: 17, CLAUSE: 20\n\nT380 is ground\nT381 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: addX(T380, T381, T383), SCOPE: 17, CLAUSE: 18\n\nT380 is ground\nT381 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: addX(T380, T381, T383), SCOPE: 17, CLAUSE: 19 | addX(T380, T381, T383), SCOPE: 17, CLAUSE: 20\n\nT380 is ground\nT381 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: binaryZ(T389)\n\nT389 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: addX(T380, T381, T383), SCOPE: 17, CLAUSE: 19\n\nT380 is ground\nT381 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: addX(T380, T381, T383), SCOPE: 17, CLAUSE: 20\n\nT380 is ground\nT381 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: succ(T399, T401)\n\nT399 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: addC(T412, T413, T415)\n\nT412 is ground\nT413 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: addC(T342, T343, T345), SCOPE: 16, CLAUSE: 26\n\nT342 is ground\nT343 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: addC(T342, T343, T345), SCOPE: 16, CLAUSE: 27\n\nT342 is ground\nT343 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: addY(T431, T432, T434)\n\nT431 is ground\nT432 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: addY(T431, T432, T434), SCOPE: 18, CLAUSE: 21 | addY(T431, T432, T434), SCOPE: 18, CLAUSE: 22 | addY(T431, T432, T434), SCOPE: 18, CLAUSE: 23\n\nT431 is ground\nT432 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: addY(T431, T432, T434), SCOPE: 18, CLAUSE: 21\n\nT431 is ground\nT432 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: addY(T431, T432, T434), SCOPE: 18, CLAUSE: 22 | addY(T431, T432, T434), SCOPE: 18, CLAUSE: 23\n\nT431 is ground\nT432 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: binaryZ(T440)\n\nT440 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: addY(T431, T432, T434), SCOPE: 18, CLAUSE: 22\n\nT431 is ground\nT432 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: addY(T431, T432, T434), SCOPE: 18, CLAUSE: 23\n\nT431 is ground\nT432 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: succ(T450, T452)\n\nT450 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: addC(T463, T464, T466)\n\nT463 is ground\nT464 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: addc(T476, T477, T479)\n\nT476 is ground\nT477 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 12 | addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 13\n\nT137 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 12\n\nT137 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: addz(T137, zero(T138), T140), SCOPE: 9, CLAUSE: 13\n\nT137 is ground\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: addy(T493, T494, T496)\n\nT493 is ground\nT494 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: times(zero(T14), T15, T3), SCOPE: 1, CLAUSE: 40\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(times(T502, T503, X583), add(T503, zero(X583), T505))\n\nT502 is ground\nT503 is ground\nX583 is free; \ntimes(one(T502), T503, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(times(T502, T503, X583), add(T503, zero(X583), T505)), SCOPE: 19, CLAUSE: 38 | ','(times(T502, T503, X583), add(T503, zero(X583), T505)), SCOPE: 19, CLAUSE: 39 | ','(times(T502, T503, X583), add(T503, zero(X583), T505)), SCOPE: 19, CLAUSE: 40\n\nT502 is ground\nT503 is ground\nX583 is free; \ntimes(one(T502), T503, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(times(T502, T503, X583), add(T503, zero(X583), T505)), SCOPE: 19, CLAUSE: 38\n\nT502 is ground\nT503 is ground\nX583 is free; \ntimes(one(T502), T503, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(times(T502, T503, X583), add(T503, zero(X583), T505)), SCOPE: 19, CLAUSE: 39 | ','(times(T502, T503, X583), add(T503, zero(X583), T505)), SCOPE: 19, CLAUSE: 40\n\nT502 is ground\nT503 is ground\nX583 is free; \ntimes(one(T502), T503, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: add(T510, zero(T510), T505)\n\nT510 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ','(times(T502, T503, X583), add(T503, zero(X583), T505)), SCOPE: 19, CLAUSE: 39\n\nT502 is ground\nT503 is ground\nX583 is free; \ntimes(one(T502), T503, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(times(T502, T503, X583), add(T503, zero(X583), T505)), SCOPE: 19, CLAUSE: 40\n\nT502 is ground\nT503 is ground\nX583 is free; \ntimes(one(T502), T503, T3) !=? times(one(b), X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(times(T520, T521, X614), add(T521, zero(zero(X614)), T505))\n\nT520 is ground\nT521 is ground\nX614 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: times(T520, T521, X614)\n\nT520 is ground\nT521 is ground\nX614 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: add(T521, zero(zero(T524)), T505)\n\nT521 is ground\nT524 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(times(T533, T534, X636), ','(add(T534, zero(X636), X637), add(T534, zero(X637), T505)))\n\nT533 is ground\nT534 is ground\nX637 is free; \nX636 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: times(T533, T534, X636)\n\nT533 is ground\nT534 is ground\nX636 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(add(T534, zero(T537), X637), add(T534, zero(X637), T505))\n\nT534 is ground\nT537 is ground\nX637 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: add(T534, zero(T537), X637)\n\nT534 is ground\nT537 is ground\nX637 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: add(T534, zero(T542), T505)\n\nT534 is ground\nT542 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 212 [arrowhead = none ];
212 -> 2;

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

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

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

216 [label="EVAL with clause\ntimes(zero(X24), X25, zero(X26)) :- times(X24, X25, X26).\nand substitution\nX24 -> T14\nT1 -> zero(T14)\nT2 -> T15\nX25 -> T15\nX26 -> T17\nT3 -> zero(T17)\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 216 [arrowhead = none ];
216 -> 12;

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

218 [label="BACKTRACK\nfor clause: times(zero(R), S, zero(RS)) :- times(R, S, RS)because of non-unification", fontsize=14, style = filled, fillcolor = white];
5 -> 218 [arrowhead = none ];
218 -> 6;

219 [label="ONLY EVAL with clause\ntimes(one(X10), X11, X12) :- ','(times(X10, X11, X13), add(X11, zero(X13), X12)).\nand substitution\nX10 -> b\nT5 -> T8\nX11 -> T8\nT3 -> T10\nX12 -> T10\nT9 -> T10", fontsize=14, style = filled, fillcolor = white];
6 -> 219 [arrowhead = none ];
219 -> 7;

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

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

222 [label="BACKTRACK\nfor clause: times(zero(R), S, zero(RS)) :- times(R, S, RS)because of non-unification", fontsize=14, style = filled, fillcolor = white];
9 -> 222 [arrowhead = none ];
222 -> 10;

223 [label="BACKTRACK\nfor clause: times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS))because of non-unification", fontsize=14, style = filled, fillcolor = white];
10 -> 223 [arrowhead = none ];
223 -> 11;

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

225 [label="EVAL with clause\ntimes(one(X580), X581, X582) :- ','(times(X580, X581, X583), add(X581, zero(X583), X582)).\nand substitution\nX580 -> T502\nT1 -> one(T502)\nT2 -> T503\nX581 -> T503\nT3 -> T505\nX582 -> T505\nT504 -> T505", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 225 [arrowhead = none ];
225 -> 193;

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

227 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 227 [arrowhead = none ];
227 -> 15;

228 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 228 [arrowhead = none ];
228 -> 16;

229 [label="EVAL with clause\ntimes(one(b), X34, X34).\nand substitution\nT14 -> one(b)\nT15 -> T22\nX34 -> T22\nT17 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 229 [arrowhead = none ];
229 -> 17;

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

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

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

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

234 [label="EVAL with clause\ntimes(zero(X48), X49, zero(X50)) :- times(X48, X49, X50).\nand substitution\nX48 -> T35\nT14 -> zero(T35)\nT15 -> T36\nX49 -> T36\nX50 -> T38\nT17 -> zero(T38)\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 234 [arrowhead = none ];
234 -> 22;

235 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 235 [arrowhead = none ];
235 -> 23;

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

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

238 [label="INSTANCE with matching:\nT1 -> T35\nT2 -> T36\nT3 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 238 [arrowhead = none , style=dashed];
238 -> 1[style=dashed];

239 [label="EVAL with clause\ntimes(one(X70), X71, X72) :- ','(times(X70, X71, X73), add(X71, zero(X73), X72)).\nand substitution\nX70 -> T53\nT14 -> one(T53)\nT15 -> T54\nX71 -> T54\nT17 -> T56\nX72 -> T56\nT55 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 239 [arrowhead = none ];
239 -> 26;

240 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 240 [arrowhead = none ];
240 -> 27;

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

242 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
26 -> 242 [arrowhead = none ];
242 -> 28;

243 [label="SPLIT 2\nnew knowledge:\nT59 is ground\nreplacements:\nX73 -> T59", fontsize=14, style = filled, fillcolor = violet];
26 -> 243 [arrowhead = none ];
243 -> 29;

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

245 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
29 -> 245 [arrowhead = none ];
245 -> 44;

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

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

248 [label="EVAL with clause\ntimes(one(b), X85, X85).\nand substitution\nT53 -> one(b)\nT54 -> T66\nX85 -> T66\nX73 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 248 [arrowhead = none ];
248 -> 33;

249 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 249 [arrowhead = none ];
249 -> 34;

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

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

252 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 252 [arrowhead = none ];
252 -> 35;

253 [label="EVAL with clause\ntimes(zero(X103), X104, zero(X105)) :- times(X103, X104, X105).\nand substitution\nX103 -> T75\nT53 -> zero(T75)\nT54 -> T76\nX104 -> T76\nX105 -> X106\nX73 -> zero(X106)", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 253 [arrowhead = none ];
253 -> 38;

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

255 [label="EVAL with clause\ntimes(one(X121), X122, X123) :- ','(times(X121, X122, X124), add(X122, zero(X124), X123)).\nand substitution\nX121 -> T83\nT53 -> one(T83)\nT54 -> T84\nX122 -> T84\nX73 -> X125\nX123 -> X125", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 255 [arrowhead = none ];
255 -> 40;

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

257 [label="INSTANCE with matching:\nT53 -> T75\nT54 -> T76\nX73 -> X106", fontsize=14, style = filled, fillcolor = lightgrey];
38 -> 257 [arrowhead = none , style=dashed];
257 -> 28[style=dashed];

258 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 258 [arrowhead = none ];
258 -> 42;

259 [label="SPLIT 2\nnew knowledge:\nT87 is ground\nreplacements:\nX124 -> T87", fontsize=14, style = filled, fillcolor = violet];
40 -> 259 [arrowhead = none ];
259 -> 43;

260 [label="INSTANCE with matching:\nT53 -> T83\nT54 -> T84\nX73 -> X124", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 260 [arrowhead = none , style=dashed];
260 -> 28[style=dashed];

261 [label="INSTANCE with matching:\nT54 -> T84\nT59 -> T87\nT56 -> X125", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 261 [arrowhead = none , style=dashed];
261 -> 29[style=dashed];

262 [label="BACKTRACK\nfor clause: add(b, b, b)because of non-unification", fontsize=14, style = filled, fillcolor = white];
44 -> 262 [arrowhead = none ];
262 -> 45;

263 [label="BACKTRACK\nfor clause: add(X, b, X) :- binaryZ(X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
45 -> 263 [arrowhead = none ];
263 -> 46;

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

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

266 [label="EVAL with clause\nadd(b, X142, X142) :- binaryZ(X142).\nand substitution\nT54 -> b\nT59 -> T99\nX142 -> zero(T99)\nT56 -> zero(T99)", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 266 [arrowhead = none ];
266 -> 49;

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

268 [label="ONLY EVAL with clause\nadd(X185, X186, X187) :- addz(X185, X186, X187).\nand substitution\nT54 -> T137\nX185 -> T137\nT59 -> T138\nX186 -> zero(T138)\nT56 -> T140\nX187 -> T140\nT139 -> T140", fontsize=14, style = filled, fillcolor = white];
48 -> 268 [arrowhead = none ];
268 -> 75;

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

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

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

272 [label="ONLY EVAL with clause\nbinaryZ(zero(X151)) :- binaryZ(X151).\nand substitution\nT99 -> T107\nX151 -> T107", fontsize=14, style = filled, fillcolor = white];
52 -> 272 [arrowhead = none ];
272 -> 54;

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

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

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

276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 276 [arrowhead = none ];
276 -> 57;

277 [label="EVAL with clause\nbinaryZ(zero(X157)) :- binaryZ(X157).\nand substitution\nX157 -> T113\nT107 -> zero(T113)", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 277 [arrowhead = none ];
277 -> 58;

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

279 [label="EVAL with clause\nbinaryZ(one(X162)) :- binary(X162).\nand substitution\nX162 -> T117\nT107 -> one(T117)", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 279 [arrowhead = none ];
279 -> 60;

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

281 [label="INSTANCE with matching:\nT107 -> T113", fontsize=14, style = filled, fillcolor = lightgrey];
58 -> 281 [arrowhead = none , style=dashed];
281 -> 54[style=dashed];

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

283 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 283 [arrowhead = none ];
283 -> 63;

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

285 [label="EVAL with clause\nbinary(b).\nand substitution\nT117 -> b", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 285 [arrowhead = none ];
285 -> 65;

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

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

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

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

290 [label="EVAL with clause\nbinary(zero(X168)) :- binaryZ(X168).\nand substitution\nX168 -> T122\nT117 -> zero(T122)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 290 [arrowhead = none ];
290 -> 70;

291 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 291 [arrowhead = none ];
291 -> 71;

292 [label="EVAL with clause\nbinary(one(X173)) :- binary(X173).\nand substitution\nX173 -> T126\nT117 -> one(T126)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 292 [arrowhead = none ];
292 -> 72;

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

294 [label="INSTANCE with matching:\nT107 -> T122", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 294 [arrowhead = none , style=dashed];
294 -> 54[style=dashed];

295 [label="INSTANCE with matching:\nT117 -> T126", fontsize=14, style = filled, fillcolor = lightgrey];
72 -> 295 [arrowhead = none , style=dashed];
295 -> 60[style=dashed];

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

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

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

299 [label="EVAL with clause\naddz(zero(X203), zero(X204), zero(X205)) :- addz(X203, X204, X205).\nand substitution\nX203 -> T156\nT137 -> zero(T156)\nT138 -> T157\nX204 -> T157\nX205 -> T159\nT140 -> zero(T159)\nT158 -> T159", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 299 [arrowhead = none ];
299 -> 79;

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

301 [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];
78 -> 301 [arrowhead = none ];
301 -> 185;

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

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

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

305 [label="EVAL with clause\naddz(zero(X224), zero(X225), zero(X226)) :- addz(X224, X225, X226).\nand substitution\nX224 -> T175\nT156 -> zero(T175)\nX225 -> T176\nT157 -> zero(T176)\nX226 -> T178\nT159 -> zero(T178)\nT177 -> T178", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 305 [arrowhead = none ];
305 -> 84;

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

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

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

309 [label="INSTANCE with matching:\nT156 -> T175\nT157 -> T176\nT159 -> T178", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 309 [arrowhead = none , style=dashed];
309 -> 79[style=dashed];

310 [label="EVAL with clause\naddz(zero(X245), one(X246), one(X247)) :- addx(X245, X246, X247).\nand substitution\nX245 -> T194\nT156 -> zero(T194)\nX246 -> T195\nT157 -> one(T195)\nX247 -> T197\nT159 -> one(T197)\nT196 -> T197", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 310 [arrowhead = none ];
310 -> 88;

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

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

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

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

315 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
90 -> 315 [arrowhead = none ];
315 -> 91;

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

317 [label="EVAL with clause\naddx(one(X256), b, one(X256)) :- binary(X256).\nand substitution\nX256 -> T203\nT194 -> one(T203)\nT195 -> b\nT197 -> one(T203)", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 317 [arrowhead = none ];
317 -> 93;

318 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 318 [arrowhead = none ];
318 -> 94;

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

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

321 [label="INSTANCE with matching:\nT117 -> T203", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 321 [arrowhead = none , style=dashed];
321 -> 60[style=dashed];

322 [label="EVAL with clause\naddx(zero(X262), b, zero(X262)) :- binaryZ(X262).\nand substitution\nX262 -> T208\nT194 -> zero(T208)\nT195 -> b\nT197 -> zero(T208)", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 322 [arrowhead = none ];
322 -> 97;

323 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 323 [arrowhead = none ];
323 -> 98;

324 [label="ONLY EVAL with clause\naddx(X274, X275, X276) :- addz(X274, X275, X276).\nand substitution\nT194 -> T220\nX274 -> T220\nT195 -> T221\nX275 -> T221\nT197 -> T223\nX276 -> T223\nT222 -> T223", fontsize=14, style = filled, fillcolor = white];
96 -> 324 [arrowhead = none ];
324 -> 99;

325 [label="INSTANCE with matching:\nT107 -> T208", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 325 [arrowhead = none , style=dashed];
325 -> 54[style=dashed];

326 [label="INSTANCE with matching:\nT156 -> T220\nT157 -> T221\nT159 -> T223", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 326 [arrowhead = none , style=dashed];
326 -> 79[style=dashed];

327 [label="EVAL with clause\naddz(one(X292), zero(X293), one(X294)) :- addy(X292, X293, X294).\nand substitution\nX292 -> T239\nT156 -> one(T239)\nX293 -> T240\nT157 -> zero(T240)\nX294 -> T242\nT159 -> one(T242)\nT241 -> T242", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 327 [arrowhead = none ];
327 -> 102;

328 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 328 [arrowhead = none ];
328 -> 103;

329 [label="EVAL with clause\naddz(one(X333), one(X334), zero(X335)) :- addc(X333, X334, X335).\nand substitution\nX333 -> T278\nT156 -> one(T278)\nX334 -> T279\nT157 -> one(T279)\nX335 -> T281\nT159 -> zero(T281)\nT280 -> T281", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 329 [arrowhead = none ];
329 -> 114;

330 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 330 [arrowhead = none ];
330 -> 115;

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

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

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

334 [label="EVAL with clause\naddy(b, one(X303), one(X303)) :- binary(X303).\nand substitution\nT239 -> b\nX303 -> T248\nT240 -> one(T248)\nT242 -> one(T248)", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 334 [arrowhead = none ];
334 -> 107;

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

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

337 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
106 -> 337 [arrowhead = none ];
337 -> 110;

338 [label="INSTANCE with matching:\nT117 -> T248", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 338 [arrowhead = none , style=dashed];
338 -> 60[style=dashed];

339 [label="EVAL with clause\naddy(b, zero(X309), zero(X309)) :- binaryZ(X309).\nand substitution\nT239 -> b\nX309 -> T253\nT240 -> zero(T253)\nT242 -> zero(T253)", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 339 [arrowhead = none ];
339 -> 111;

340 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 340 [arrowhead = none ];
340 -> 112;

341 [label="ONLY EVAL with clause\naddy(X321, X322, X323) :- addz(X321, X322, X323).\nand substitution\nT239 -> T265\nX321 -> T265\nT240 -> T266\nX322 -> T266\nT242 -> T268\nX323 -> T268\nT267 -> T268", fontsize=14, style = filled, fillcolor = white];
110 -> 341 [arrowhead = none ];
341 -> 113;

342 [label="INSTANCE with matching:\nT208 -> T253", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 342 [arrowhead = none , style=dashed];
342 -> 97[style=dashed];

343 [label="INSTANCE with matching:\nT156 -> T265\nT157 -> T266\nT159 -> T268", fontsize=14, style = filled, fillcolor = lightgrey];
113 -> 343 [arrowhead = none , style=dashed];
343 -> 79[style=dashed];

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

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

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

347 [label="EVAL with clause\naddc(b, b, one(b)).\nand substitution\nT278 -> b\nT279 -> b\nT281 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 347 [arrowhead = none ];
347 -> 119;

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

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

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

351 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 351 [arrowhead = none ];
351 -> 121;

352 [label="EVAL with clause\naddc(X347, b, X348) :- succZ(X347, X348).\nand substitution\nT278 -> T290\nX347 -> T290\nT279 -> b\nT281 -> T292\nX348 -> T292\nT291 -> T292", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 352 [arrowhead = none ];
352 -> 124;

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

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

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

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

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

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

359 [label="EVAL with clause\nsuccZ(zero(X356), one(X356)) :- binaryZ(X356).\nand substitution\nX356 -> T298\nT290 -> zero(T298)\nT292 -> one(T298)", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 359 [arrowhead = none ];
359 -> 129;

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

361 [label="EVAL with clause\nsuccZ(one(X363), zero(X364)) :- succ(X363, X364).\nand substitution\nX363 -> T304\nT290 -> one(T304)\nX364 -> T306\nT292 -> zero(T306)\nT305 -> T306", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 361 [arrowhead = none ];
361 -> 131;

362 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 362 [arrowhead = none ];
362 -> 132;

363 [label="INSTANCE with matching:\nT208 -> T298", fontsize=14, style = filled, fillcolor = lightgrey];
129 -> 363 [arrowhead = none , style=dashed];
363 -> 97[style=dashed];

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

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

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

367 [label="EVAL with clause\nsucc(b, one(b)).\nand substitution\nT304 -> b\nT306 -> one(b)", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 367 [arrowhead = none ];
367 -> 136;

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

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

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

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

372 [label="EVAL with clause\nsucc(zero(X371), one(X371)) :- binaryZ(X371).\nand substitution\nX371 -> T311\nT304 -> zero(T311)\nT306 -> one(T311)", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 372 [arrowhead = none ];
372 -> 141;

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

374 [label="EVAL with clause\nsucc(one(X378), zero(X379)) :- succ(X378, X379).\nand substitution\nX378 -> T317\nT304 -> one(T317)\nX379 -> T319\nT306 -> zero(T319)\nT318 -> T319", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 374 [arrowhead = none ];
374 -> 143;

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

376 [label="INSTANCE with matching:\nT208 -> T311", fontsize=14, style = filled, fillcolor = lightgrey];
141 -> 376 [arrowhead = none , style=dashed];
376 -> 97[style=dashed];

377 [label="INSTANCE with matching:\nT304 -> T317\nT306 -> T319", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 377 [arrowhead = none , style=dashed];
377 -> 131[style=dashed];

378 [label="EVAL with clause\naddc(b, X390, X391) :- succZ(X390, X391).\nand substitution\nT278 -> b\nT279 -> T328\nX390 -> T328\nT281 -> T330\nX391 -> T330\nT329 -> T330", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 378 [arrowhead = none ];
378 -> 147;

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

380 [label="ONLY EVAL with clause\naddc(X404, X405, X406) :- addC(X404, X405, X406).\nand substitution\nT278 -> T342\nX404 -> T342\nT279 -> T343\nX405 -> T343\nT281 -> T345\nX406 -> T345\nT344 -> T345", fontsize=14, style = filled, fillcolor = white];
146 -> 380 [arrowhead = none ];
380 -> 149;

381 [label="INSTANCE with matching:\nT290 -> T328\nT292 -> T330", fontsize=14, style = filled, fillcolor = lightgrey];
147 -> 381 [arrowhead = none , style=dashed];
381 -> 124[style=dashed];

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

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

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

385 [label="EVAL with clause\naddC(zero(X422), zero(X423), one(X424)) :- addz(X422, X423, X424).\nand substitution\nX422 -> T361\nT342 -> zero(T361)\nX423 -> T362\nT343 -> zero(T362)\nX424 -> T364\nT345 -> one(T364)\nT363 -> T364", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 385 [arrowhead = none ];
385 -> 153;

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

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

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

389 [label="INSTANCE with matching:\nT156 -> T361\nT157 -> T362\nT159 -> T364", fontsize=14, style = filled, fillcolor = lightgrey];
153 -> 389 [arrowhead = none , style=dashed];
389 -> 79[style=dashed];

390 [label="EVAL with clause\naddC(zero(X443), one(X444), zero(X445)) :- addX(X443, X444, X445).\nand substitution\nX443 -> T380\nT342 -> zero(T380)\nX444 -> T381\nT343 -> one(T381)\nX445 -> T383\nT345 -> zero(T383)\nT382 -> T383", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 390 [arrowhead = none ];
390 -> 157;

391 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 391 [arrowhead = none ];
391 -> 158;

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

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

394 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
157 -> 394 [arrowhead = none ];
394 -> 159;

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

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

397 [label="EVAL with clause\naddX(zero(X454), b, one(X454)) :- binaryZ(X454).\nand substitution\nX454 -> T389\nT380 -> zero(T389)\nT381 -> b\nT383 -> one(T389)", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 397 [arrowhead = none ];
397 -> 162;

398 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 398 [arrowhead = none ];
398 -> 163;

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

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

401 [label="INSTANCE with matching:\nT208 -> T389", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 401 [arrowhead = none , style=dashed];
401 -> 97[style=dashed];

402 [label="EVAL with clause\naddX(one(X465), b, zero(X466)) :- succ(X465, X466).\nand substitution\nX465 -> T399\nT380 -> one(T399)\nT381 -> b\nX466 -> T401\nT383 -> zero(T401)\nT400 -> T401", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 402 [arrowhead = none ];
402 -> 166;

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

404 [label="ONLY EVAL with clause\naddX(X478, X479, X480) :- addC(X478, X479, X480).\nand substitution\nT380 -> T412\nX478 -> T412\nT381 -> T413\nX479 -> T413\nT383 -> T415\nX480 -> T415\nT414 -> T415", fontsize=14, style = filled, fillcolor = white];
165 -> 404 [arrowhead = none ];
404 -> 168;

405 [label="INSTANCE with matching:\nT304 -> T399\nT306 -> T401", fontsize=14, style = filled, fillcolor = lightgrey];
166 -> 405 [arrowhead = none , style=dashed];
405 -> 131[style=dashed];

406 [label="INSTANCE with matching:\nT342 -> T412\nT343 -> T413\nT345 -> T415", fontsize=14, style = filled, fillcolor = lightgrey];
168 -> 406 [arrowhead = none , style=dashed];
406 -> 149[style=dashed];

407 [label="EVAL with clause\naddC(one(X496), zero(X497), zero(X498)) :- addY(X496, X497, X498).\nand substitution\nX496 -> T431\nT342 -> one(T431)\nX497 -> T432\nT343 -> zero(T432)\nX498 -> T434\nT345 -> zero(T434)\nT433 -> T434", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 407 [arrowhead = none ];
407 -> 171;

408 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 408 [arrowhead = none ];
408 -> 172;

409 [label="EVAL with clause\naddC(one(X543), one(X544), one(X545)) :- addc(X543, X544, X545).\nand substitution\nX543 -> T476\nT342 -> one(T476)\nX544 -> T477\nT343 -> one(T477)\nX545 -> T479\nT345 -> one(T479)\nT478 -> T479", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 409 [arrowhead = none ];
409 -> 183;

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

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

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

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

414 [label="EVAL with clause\naddY(b, zero(X507), one(X507)) :- binaryZ(X507).\nand substitution\nT431 -> b\nX507 -> T440\nT432 -> zero(T440)\nT434 -> one(T440)", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 414 [arrowhead = none ];
414 -> 176;

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

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

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

418 [label="INSTANCE with matching:\nT208 -> T440", fontsize=14, style = filled, fillcolor = lightgrey];
176 -> 418 [arrowhead = none , style=dashed];
418 -> 97[style=dashed];

419 [label="EVAL with clause\naddY(b, one(X518), zero(X519)) :- succ(X518, X519).\nand substitution\nT431 -> b\nX518 -> T450\nT432 -> one(T450)\nX519 -> T452\nT434 -> zero(T452)\nT451 -> T452", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 419 [arrowhead = none ];
419 -> 180;

420 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 420 [arrowhead = none ];
420 -> 181;

421 [label="ONLY EVAL with clause\naddY(X531, X532, X533) :- addC(X531, X532, X533).\nand substitution\nT431 -> T463\nX531 -> T463\nT432 -> T464\nX532 -> T464\nT434 -> T466\nX533 -> T466\nT465 -> T466", fontsize=14, style = filled, fillcolor = white];
179 -> 421 [arrowhead = none ];
421 -> 182;

422 [label="INSTANCE with matching:\nT304 -> T450\nT306 -> T452", fontsize=14, style = filled, fillcolor = lightgrey];
180 -> 422 [arrowhead = none , style=dashed];
422 -> 131[style=dashed];

423 [label="INSTANCE with matching:\nT342 -> T463\nT343 -> T464\nT345 -> T466", fontsize=14, style = filled, fillcolor = lightgrey];
182 -> 423 [arrowhead = none , style=dashed];
423 -> 149[style=dashed];

424 [label="INSTANCE with matching:\nT278 -> T476\nT279 -> T477\nT281 -> T479", fontsize=14, style = filled, fillcolor = lightgrey];
183 -> 424 [arrowhead = none , style=dashed];
424 -> 114[style=dashed];

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

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

427 [label="EVAL with clause\naddz(one(X564), zero(X565), one(X566)) :- addy(X564, X565, X566).\nand substitution\nX564 -> T493\nT137 -> one(T493)\nT138 -> T494\nX565 -> T494\nX566 -> T496\nT140 -> one(T496)\nT495 -> T496", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 427 [arrowhead = none ];
427 -> 188;

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

429 [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];
187 -> 429 [arrowhead = none ];
429 -> 190;

430 [label="INSTANCE with matching:\nT239 -> T493\nT240 -> T494\nT242 -> T496", fontsize=14, style = filled, fillcolor = lightgrey];
188 -> 430 [arrowhead = none , style=dashed];
430 -> 102[style=dashed];

431 [label="BACKTRACK\nfor clause: times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS))because of non-unification", fontsize=14, style = filled, fillcolor = white];
191 -> 431 [arrowhead = none ];
431 -> 192;

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

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

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

435 [label="EVAL with clause\ntimes(one(b), X591, X591).\nand substitution\nT502 -> one(b)\nT503 -> T510\nX591 -> T510\nX583 -> T510", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 435 [arrowhead = none ];
435 -> 198;

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

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

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

439 [label="INSTANCE with matching:\nT54 -> T510\nT59 -> T510\nT56 -> T505", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 439 [arrowhead = none , style=dashed];
439 -> 29[style=dashed];

440 [label="EVAL with clause\ntimes(zero(X611), X612, zero(X613)) :- times(X611, X612, X613).\nand substitution\nX611 -> T520\nT502 -> zero(T520)\nT503 -> T521\nX612 -> T521\nX613 -> X614\nX583 -> zero(X614)", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 440 [arrowhead = none ];
440 -> 202;

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

442 [label="EVAL with clause\ntimes(one(X633), X634, X635) :- ','(times(X633, X634, X636), add(X634, zero(X636), X635)).\nand substitution\nX633 -> T533\nT502 -> one(T533)\nT503 -> T534\nX634 -> T534\nX583 -> X637\nX635 -> X637", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 442 [arrowhead = none ];
442 -> 206;

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

444 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
202 -> 444 [arrowhead = none ];
444 -> 204;

445 [label="SPLIT 2\nnew knowledge:\nT524 is ground\nreplacements:\nX614 -> T524", fontsize=14, style = filled, fillcolor = violet];
202 -> 445 [arrowhead = none ];
445 -> 205;

446 [label="INSTANCE with matching:\nT53 -> T520\nT54 -> T521\nX73 -> X614", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 446 [arrowhead = none , style=dashed];
446 -> 28[style=dashed];

447 [label="INSTANCE with matching:\nT54 -> T521\nT59 -> zero(T524)\nT56 -> T505", fontsize=14, style = filled, fillcolor = lightgrey];
205 -> 447 [arrowhead = none , style=dashed];
447 -> 29[style=dashed];

448 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
206 -> 448 [arrowhead = none ];
448 -> 208;

449 [label="SPLIT 2\nnew knowledge:\nT537 is ground\nreplacements:\nX636 -> T537", fontsize=14, style = filled, fillcolor = violet];
206 -> 449 [arrowhead = none ];
449 -> 209;

450 [label="INSTANCE with matching:\nT53 -> T533\nT54 -> T534\nX73 -> X636", fontsize=14, style = filled, fillcolor = lightgrey];
208 -> 450 [arrowhead = none , style=dashed];
450 -> 28[style=dashed];

451 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
209 -> 451 [arrowhead = none ];
451 -> 210;

452 [label="SPLIT 2\nnew knowledge:\nT542 is ground\nreplacements:\nX637 -> T542", fontsize=14, style = filled, fillcolor = violet];
209 -> 452 [arrowhead = none ];
452 -> 211;

453 [label="INSTANCE with matching:\nT54 -> T534\nT59 -> T537\nT56 -> X637", fontsize=14, style = filled, fillcolor = lightgrey];
210 -> 453 [arrowhead = none , style=dashed];
453 -> 29[style=dashed];

454 [label="INSTANCE with matching:\nT54 -> T534\nT59 -> T542\nT56 -> T505", fontsize=14, style = filled, fillcolor = lightgrey];
211 -> 454 [arrowhead = none , style=dashed];
454 -> 29[style=dashed];

}

(2) Obligation:

Triples:

times28(zero(T75), T76, zero(X106)) :- times28(T75, T76, X106).
times28(one(T83), T84, X125) :- times28(T83, T84, X124).
times28(one(T83), T84, X125) :- ','(timesc28(T83, T84, T87), add29(T84, T87, X125)).
add29(b, T107, zero(T107)) :- binaryZ54(T107).
add29(zero(T156), T157, zero(T159)) :- addz79(T156, T157, T159).
add29(one(T493), T494, one(T496)) :- addy102(T493, T494, T496).
binaryZ54(zero(T113)) :- binaryZ54(T113).
binaryZ54(one(T117)) :- binary60(T117).
binary60(zero(T122)) :- binaryZ54(T122).
binary60(one(T126)) :- binary60(T126).
addz79(zero(T175), zero(T176), zero(T178)) :- addz79(T175, T176, T178).
addz79(zero(one(T203)), one(b), one(one(T203))) :- binary60(T203).
addz79(zero(zero(T208)), one(b), one(zero(T208))) :- binaryZ54(T208).
addz79(zero(T220), one(T221), one(T223)) :- addz79(T220, T221, T223).
addz79(one(T239), zero(T240), one(T242)) :- addy102(T239, T240, T242).
addz79(one(T278), one(T279), zero(T281)) :- addc114(T278, T279, T281).
succ131(zero(T311), one(T311)) :- binaryZ54(T311).
succ131(one(T317), zero(T319)) :- succ131(T317, T319).
succZ124(zero(T298), one(T298)) :- binaryZ54(T298).
succZ124(one(T304), zero(T306)) :- succ131(T304, T306).
addC149(zero(T361), zero(T362), one(T364)) :- addz79(T361, T362, T364).
addC149(zero(zero(T389)), one(b), zero(one(T389))) :- binaryZ54(T389).
addC149(zero(one(T399)), one(b), zero(zero(T401))) :- succ131(T399, T401).
addC149(zero(T412), one(T413), zero(T415)) :- addC149(T412, T413, T415).
addC149(one(b), zero(zero(T440)), zero(one(T440))) :- binaryZ54(T440).
addC149(one(b), zero(one(T450)), zero(zero(T452))) :- succ131(T450, T452).
addC149(one(T463), zero(T464), zero(T466)) :- addC149(T463, T464, T466).
addC149(one(T476), one(T477), one(T479)) :- addc114(T476, T477, T479).
addc114(T290, b, T292) :- succZ124(T290, T292).
addc114(b, T328, T330) :- succZ124(T328, T330).
addc114(T342, T343, T345) :- addC149(T342, T343, T345).
addy102(b, one(T248), one(T248)) :- binary60(T248).
addy102(b, zero(T253), zero(T253)) :- binaryZ54(T253).
addy102(T265, T266, T268) :- addz79(T265, T266, T268).
times1(zero(zero(T35)), T36, zero(zero(T38))) :- times1(T35, T36, T38).
times1(zero(one(T53)), T54, zero(T56)) :- times28(T53, T54, X73).
times1(zero(one(T53)), T54, zero(T56)) :- ','(timesc28(T53, T54, T59), add29(T54, T59, T56)).
times1(one(one(b)), T510, T505) :- add29(T510, T510, T505).
times1(one(zero(T520)), T521, T505) :- times28(T520, T521, X614).
times1(one(zero(T520)), T521, T505) :- ','(timesc28(T520, T521, T524), add29(T521, zero(T524), T505)).
times1(one(one(T533)), T534, T505) :- times28(T533, T534, X636).
times1(one(one(T533)), T534, T505) :- ','(timesc28(T533, T534, T537), add29(T534, T537, X637)).
times1(one(one(T533)), T534, T505) :- ','(timesc28(T533, T534, T537), ','(addc29(T534, T537, T542), add29(T534, T542, T505))).

Clauses:

timesc1(one(b), T5, T5).
timesc1(zero(one(b)), T22, zero(T22)).
timesc1(zero(zero(T35)), T36, zero(zero(T38))) :- timesc1(T35, T36, T38).
timesc1(zero(one(T53)), T54, zero(T56)) :- ','(timesc28(T53, T54, T59), addc29(T54, T59, T56)).
timesc1(one(one(b)), T510, T505) :- addc29(T510, T510, T505).
timesc1(one(zero(T520)), T521, T505) :- ','(timesc28(T520, T521, T524), addc29(T521, zero(T524), T505)).
timesc1(one(one(T533)), T534, T505) :- ','(timesc28(T533, T534, T537), ','(addc29(T534, T537, T542), addc29(T534, T542, T505))).
timesc28(one(b), T66, T66).
timesc28(zero(T75), T76, zero(X106)) :- timesc28(T75, T76, X106).
timesc28(one(T83), T84, X125) :- ','(timesc28(T83, T84, T87), addc29(T84, T87, X125)).
addc29(b, T107, zero(T107)) :- binaryZc54(T107).
addc29(zero(T156), T157, zero(T159)) :- addzc79(T156, T157, T159).
addc29(one(T493), T494, one(T496)) :- addyc102(T493, T494, T496).
binaryZc54(zero(T113)) :- binaryZc54(T113).
binaryZc54(one(T117)) :- binaryc60(T117).
binaryc60(b).
binaryc60(zero(T122)) :- binaryZc54(T122).
binaryc60(one(T126)) :- binaryc60(T126).
addzc79(zero(T175), zero(T176), zero(T178)) :- addzc79(T175, T176, T178).
addzc79(zero(one(T203)), one(b), one(one(T203))) :- binaryc60(T203).
addzc79(zero(zero(T208)), one(b), one(zero(T208))) :- binaryZc54(T208).
addzc79(zero(T220), one(T221), one(T223)) :- addzc79(T220, T221, T223).
addzc79(one(T239), zero(T240), one(T242)) :- addyc102(T239, T240, T242).
addzc79(one(T278), one(T279), zero(T281)) :- addcc114(T278, T279, T281).
succc131(b, one(b)).
succc131(zero(T311), one(T311)) :- binaryZc54(T311).
succc131(one(T317), zero(T319)) :- succc131(T317, T319).
succZc124(zero(T298), one(T298)) :- binaryZc54(T298).
succZc124(one(T304), zero(T306)) :- succc131(T304, T306).
addCc149(zero(T361), zero(T362), one(T364)) :- addzc79(T361, T362, T364).
addCc149(zero(zero(T389)), one(b), zero(one(T389))) :- binaryZc54(T389).
addCc149(zero(one(T399)), one(b), zero(zero(T401))) :- succc131(T399, T401).
addCc149(zero(T412), one(T413), zero(T415)) :- addCc149(T412, T413, T415).
addCc149(one(b), zero(zero(T440)), zero(one(T440))) :- binaryZc54(T440).
addCc149(one(b), zero(one(T450)), zero(zero(T452))) :- succc131(T450, T452).
addCc149(one(T463), zero(T464), zero(T466)) :- addCc149(T463, T464, T466).
addCc149(one(T476), one(T477), one(T479)) :- addcc114(T476, T477, T479).
addcc114(b, b, one(b)).
addcc114(T290, b, T292) :- succZc124(T290, T292).
addcc114(b, T328, T330) :- succZc124(T328, T330).
addcc114(T342, T343, T345) :- addCc149(T342, T343, T345).
addyc102(b, one(T248), one(T248)) :- binaryc60(T248).
addyc102(b, zero(T253), zero(T253)) :- binaryZc54(T253).
addyc102(T265, T266, T268) :- addzc79(T265, T266, T268).

Afs:

times1(x1, x2, x3) = times1(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
times1_in: (b,b,f)
times28_in: (b,b,f)
timesc28_in: (b,b,f)
addc29_in: (b,b,f)
binaryZc54_in: (b)
binaryc60_in: (b)
addzc79_in: (b,b,f)
addyc102_in: (b,b,f)
addcc114_in: (b,b,f)
succZc124_in: (b,f)
succc131_in: (b,f)
addCc149_in: (b,b,f)
add29_in: (b,b,f)
binaryZ54_in: (b)
binary60_in: (b)
addz79_in: (b,b,f)
addy102_in: (b,b,f)
addc114_in: (b,b,f)
succZ124_in: (b,f)
succ131_in: (b,f)
addC149_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

TIMES1_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → U36_GGA(T35, T36, T38, times1_in_gga(T35, T36, T38))
TIMES1_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → TIMES1_IN_GGA(T35, T36, T38)
TIMES1_IN_GGA(zero(one(T53)), T54, zero(T56)) → U37_GGA(T53, T54, T56, times28_in_gga(T53, T54, X73))
TIMES1_IN_GGA(zero(one(T53)), T54, zero(T56)) → TIMES28_IN_GGA(T53, T54, X73)
TIMES28_IN_GGA(zero(T75), T76, zero(X106)) → U1_GGA(T75, T76, X106, times28_in_gga(T75, T76, X106))
TIMES28_IN_GGA(zero(T75), T76, zero(X106)) → TIMES28_IN_GGA(T75, T76, X106)
TIMES28_IN_GGA(one(T83), T84, X125) → U2_GGA(T83, T84, X125, times28_in_gga(T83, T84, X124))
TIMES28_IN_GGA(one(T83), T84, X125) → TIMES28_IN_GGA(T83, T84, X124)
TIMES28_IN_GGA(one(T83), T84, X125) → U3_GGA(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U3_GGA(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U4_GGA(T83, T84, X125, add29_in_gga(T84, T87, X125))
U3_GGA(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → ADD29_IN_GGA(T84, T87, X125)
ADD29_IN_GGA(b, T107, zero(T107)) → U5_GGA(T107, binaryZ54_in_g(T107))
ADD29_IN_GGA(b, T107, zero(T107)) → BINARYZ54_IN_G(T107)
BINARYZ54_IN_G(zero(T113)) → U8_G(T113, binaryZ54_in_g(T113))
BINARYZ54_IN_G(zero(T113)) → BINARYZ54_IN_G(T113)
BINARYZ54_IN_G(one(T117)) → U9_G(T117, binary60_in_g(T117))
BINARYZ54_IN_G(one(T117)) → BINARY60_IN_G(T117)
BINARY60_IN_G(zero(T122)) → U10_G(T122, binaryZ54_in_g(T122))
BINARY60_IN_G(zero(T122)) → BINARYZ54_IN_G(T122)
BINARY60_IN_G(one(T126)) → U11_G(T126, binary60_in_g(T126))
BINARY60_IN_G(one(T126)) → BINARY60_IN_G(T126)
ADD29_IN_GGA(zero(T156), T157, zero(T159)) → U6_GGA(T156, T157, T159, addz79_in_gga(T156, T157, T159))
ADD29_IN_GGA(zero(T156), T157, zero(T159)) → ADDZ79_IN_GGA(T156, T157, T159)
ADDZ79_IN_GGA(zero(T175), zero(T176), zero(T178)) → U12_GGA(T175, T176, T178, addz79_in_gga(T175, T176, T178))
ADDZ79_IN_GGA(zero(T175), zero(T176), zero(T178)) → ADDZ79_IN_GGA(T175, T176, T178)
ADDZ79_IN_GGA(zero(one(T203)), one(b), one(one(T203))) → U13_GGA(T203, binary60_in_g(T203))
ADDZ79_IN_GGA(zero(one(T203)), one(b), one(one(T203))) → BINARY60_IN_G(T203)
ADDZ79_IN_GGA(zero(zero(T208)), one(b), one(zero(T208))) → U14_GGA(T208, binaryZ54_in_g(T208))
ADDZ79_IN_GGA(zero(zero(T208)), one(b), one(zero(T208))) → BINARYZ54_IN_G(T208)
ADDZ79_IN_GGA(zero(T220), one(T221), one(T223)) → U15_GGA(T220, T221, T223, addz79_in_gga(T220, T221, T223))
ADDZ79_IN_GGA(zero(T220), one(T221), one(T223)) → ADDZ79_IN_GGA(T220, T221, T223)
ADDZ79_IN_GGA(one(T239), zero(T240), one(T242)) → U16_GGA(T239, T240, T242, addy102_in_gga(T239, T240, T242))
ADDZ79_IN_GGA(one(T239), zero(T240), one(T242)) → ADDY102_IN_GGA(T239, T240, T242)
ADDY102_IN_GGA(b, one(T248), one(T248)) → U33_GGA(T248, binary60_in_g(T248))
ADDY102_IN_GGA(b, one(T248), one(T248)) → BINARY60_IN_G(T248)
ADDY102_IN_GGA(b, zero(T253), zero(T253)) → U34_GGA(T253, binaryZ54_in_g(T253))
ADDY102_IN_GGA(b, zero(T253), zero(T253)) → BINARYZ54_IN_G(T253)
ADDY102_IN_GGA(T265, T266, T268) → U35_GGA(T265, T266, T268, addz79_in_gga(T265, T266, T268))
ADDY102_IN_GGA(T265, T266, T268) → ADDZ79_IN_GGA(T265, T266, T268)
ADDZ79_IN_GGA(one(T278), one(T279), zero(T281)) → U17_GGA(T278, T279, T281, addc114_in_gga(T278, T279, T281))
ADDZ79_IN_GGA(one(T278), one(T279), zero(T281)) → ADDC114_IN_GGA(T278, T279, T281)
ADDC114_IN_GGA(T290, b, T292) → U30_GGA(T290, T292, succZ124_in_ga(T290, T292))
ADDC114_IN_GGA(T290, b, T292) → SUCCZ124_IN_GA(T290, T292)
SUCCZ124_IN_GA(zero(T298), one(T298)) → U20_GA(T298, binaryZ54_in_g(T298))
SUCCZ124_IN_GA(zero(T298), one(T298)) → BINARYZ54_IN_G(T298)
SUCCZ124_IN_GA(one(T304), zero(T306)) → U21_GA(T304, T306, succ131_in_ga(T304, T306))
SUCCZ124_IN_GA(one(T304), zero(T306)) → SUCC131_IN_GA(T304, T306)
SUCC131_IN_GA(zero(T311), one(T311)) → U18_GA(T311, binaryZ54_in_g(T311))
SUCC131_IN_GA(zero(T311), one(T311)) → BINARYZ54_IN_G(T311)
SUCC131_IN_GA(one(T317), zero(T319)) → U19_GA(T317, T319, succ131_in_ga(T317, T319))
SUCC131_IN_GA(one(T317), zero(T319)) → SUCC131_IN_GA(T317, T319)
ADDC114_IN_GGA(b, T328, T330) → U31_GGA(T328, T330, succZ124_in_ga(T328, T330))
ADDC114_IN_GGA(b, T328, T330) → SUCCZ124_IN_GA(T328, T330)
ADDC114_IN_GGA(T342, T343, T345) → U32_GGA(T342, T343, T345, addC149_in_gga(T342, T343, T345))
ADDC114_IN_GGA(T342, T343, T345) → ADDC149_IN_GGA(T342, T343, T345)
ADDC149_IN_GGA(zero(T361), zero(T362), one(T364)) → U22_GGA(T361, T362, T364, addz79_in_gga(T361, T362, T364))
ADDC149_IN_GGA(zero(T361), zero(T362), one(T364)) → ADDZ79_IN_GGA(T361, T362, T364)
ADDC149_IN_GGA(zero(zero(T389)), one(b), zero(one(T389))) → U23_GGA(T389, binaryZ54_in_g(T389))
ADDC149_IN_GGA(zero(zero(T389)), one(b), zero(one(T389))) → BINARYZ54_IN_G(T389)
ADDC149_IN_GGA(zero(one(T399)), one(b), zero(zero(T401))) → U24_GGA(T399, T401, succ131_in_ga(T399, T401))
ADDC149_IN_GGA(zero(one(T399)), one(b), zero(zero(T401))) → SUCC131_IN_GA(T399, T401)
ADDC149_IN_GGA(zero(T412), one(T413), zero(T415)) → U25_GGA(T412, T413, T415, addC149_in_gga(T412, T413, T415))
ADDC149_IN_GGA(zero(T412), one(T413), zero(T415)) → ADDC149_IN_GGA(T412, T413, T415)
ADDC149_IN_GGA(one(b), zero(zero(T440)), zero(one(T440))) → U26_GGA(T440, binaryZ54_in_g(T440))
ADDC149_IN_GGA(one(b), zero(zero(T440)), zero(one(T440))) → BINARYZ54_IN_G(T440)
ADDC149_IN_GGA(one(b), zero(one(T450)), zero(zero(T452))) → U27_GGA(T450, T452, succ131_in_ga(T450, T452))
ADDC149_IN_GGA(one(b), zero(one(T450)), zero(zero(T452))) → SUCC131_IN_GA(T450, T452)
ADDC149_IN_GGA(one(T463), zero(T464), zero(T466)) → U28_GGA(T463, T464, T466, addC149_in_gga(T463, T464, T466))
ADDC149_IN_GGA(one(T463), zero(T464), zero(T466)) → ADDC149_IN_GGA(T463, T464, T466)
ADDC149_IN_GGA(one(T476), one(T477), one(T479)) → U29_GGA(T476, T477, T479, addc114_in_gga(T476, T477, T479))
ADDC149_IN_GGA(one(T476), one(T477), one(T479)) → ADDC114_IN_GGA(T476, T477, T479)
ADD29_IN_GGA(one(T493), T494, one(T496)) → U7_GGA(T493, T494, T496, addy102_in_gga(T493, T494, T496))
ADD29_IN_GGA(one(T493), T494, one(T496)) → ADDY102_IN_GGA(T493, T494, T496)
TIMES1_IN_GGA(zero(one(T53)), T54, zero(T56)) → U38_GGA(T53, T54, T56, timesc28_in_gga(T53, T54, T59))
U38_GGA(T53, T54, T56, timesc28_out_gga(T53, T54, T59)) → U39_GGA(T53, T54, T56, add29_in_gga(T54, T59, T56))
U38_GGA(T53, T54, T56, timesc28_out_gga(T53, T54, T59)) → ADD29_IN_GGA(T54, T59, T56)
TIMES1_IN_GGA(one(one(b)), T510, T505) → U40_GGA(T510, T505, add29_in_gga(T510, T510, T505))
TIMES1_IN_GGA(one(one(b)), T510, T505) → ADD29_IN_GGA(T510, T510, T505)
TIMES1_IN_GGA(one(zero(T520)), T521, T505) → U41_GGA(T520, T521, T505, times28_in_gga(T520, T521, X614))
TIMES1_IN_GGA(one(zero(T520)), T521, T505) → TIMES28_IN_GGA(T520, T521, X614)
TIMES1_IN_GGA(one(zero(T520)), T521, T505) → U42_GGA(T520, T521, T505, timesc28_in_gga(T520, T521, T524))
U42_GGA(T520, T521, T505, timesc28_out_gga(T520, T521, T524)) → U43_GGA(T520, T521, T505, add29_in_gga(T521, zero(T524), T505))
U42_GGA(T520, T521, T505, timesc28_out_gga(T520, T521, T524)) → ADD29_IN_GGA(T521, zero(T524), T505)
TIMES1_IN_GGA(one(one(T533)), T534, T505) → U44_GGA(T533, T534, T505, times28_in_gga(T533, T534, X636))
TIMES1_IN_GGA(one(one(T533)), T534, T505) → TIMES28_IN_GGA(T533, T534, X636)
TIMES1_IN_GGA(one(one(T533)), T534, T505) → U45_GGA(T533, T534, T505, timesc28_in_gga(T533, T534, T537))
U45_GGA(T533, T534, T505, timesc28_out_gga(T533, T534, T537)) → U46_GGA(T533, T534, T505, add29_in_gga(T534, T537, X637))
U45_GGA(T533, T534, T505, timesc28_out_gga(T533, T534, T537)) → ADD29_IN_GGA(T534, T537, X637)
U45_GGA(T533, T534, T505, timesc28_out_gga(T533, T534, T537)) → U47_GGA(T533, T534, T505, addc29_in_gga(T534, T537, T542))
U47_GGA(T533, T534, T505, addc29_out_gga(T534, T537, T542)) → U48_GGA(T533, T534, T505, add29_in_gga(T534, T542, T505))
U47_GGA(T533, T534, T505, addc29_out_gga(T534, T537, T542)) → ADD29_IN_GGA(T534, T542, T505)

The TRS R consists of the following rules:

timesc28_in_gga(one(b), T66, T66) → timesc28_out_gga(one(b), T66, T66)
timesc28_in_gga(zero(T75), T76, zero(X106)) → U59_gga(T75, T76, X106, timesc28_in_gga(T75, T76, X106))
timesc28_in_gga(one(T83), T84, X125) → U60_gga(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U60_gga(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U61_gga(T83, T84, X125, addc29_in_gga(T84, T87, X125))
addc29_in_gga(b, T107, zero(T107)) → U62_gga(T107, binaryZc54_in_g(T107))
binaryZc54_in_g(zero(T113)) → U65_g(T113, binaryZc54_in_g(T113))
binaryZc54_in_g(one(T117)) → U66_g(T117, binaryc60_in_g(T117))
binaryc60_in_g(b) → binaryc60_out_g(b)
binaryc60_in_g(zero(T122)) → U67_g(T122, binaryZc54_in_g(T122))
U67_g(T122, binaryZc54_out_g(T122)) → binaryc60_out_g(zero(T122))
binaryc60_in_g(one(T126)) → U68_g(T126, binaryc60_in_g(T126))
U68_g(T126, binaryc60_out_g(T126)) → binaryc60_out_g(one(T126))
U66_g(T117, binaryc60_out_g(T117)) → binaryZc54_out_g(one(T117))
U65_g(T113, binaryZc54_out_g(T113)) → binaryZc54_out_g(zero(T113))
U62_gga(T107, binaryZc54_out_g(T107)) → addc29_out_gga(b, T107, zero(T107))
addc29_in_gga(zero(T156), T157, zero(T159)) → U63_gga(T156, T157, T159, addzc79_in_gga(T156, T157, T159))
addzc79_in_gga(zero(T175), zero(T176), zero(T178)) → U69_gga(T175, T176, T178, addzc79_in_gga(T175, T176, T178))
addzc79_in_gga(zero(one(T203)), one(b), one(one(T203))) → U70_gga(T203, binaryc60_in_g(T203))
U70_gga(T203, binaryc60_out_g(T203)) → addzc79_out_gga(zero(one(T203)), one(b), one(one(T203)))
addzc79_in_gga(zero(zero(T208)), one(b), one(zero(T208))) → U71_gga(T208, binaryZc54_in_g(T208))
U71_gga(T208, binaryZc54_out_g(T208)) → addzc79_out_gga(zero(zero(T208)), one(b), one(zero(T208)))
addzc79_in_gga(zero(T220), one(T221), one(T223)) → U72_gga(T220, T221, T223, addzc79_in_gga(T220, T221, T223))
addzc79_in_gga(one(T239), zero(T240), one(T242)) → U73_gga(T239, T240, T242, addyc102_in_gga(T239, T240, T242))
addyc102_in_gga(b, one(T248), one(T248)) → U90_gga(T248, binaryc60_in_g(T248))
U90_gga(T248, binaryc60_out_g(T248)) → addyc102_out_gga(b, one(T248), one(T248))
addyc102_in_gga(b, zero(T253), zero(T253)) → U91_gga(T253, binaryZc54_in_g(T253))
U91_gga(T253, binaryZc54_out_g(T253)) → addyc102_out_gga(b, zero(T253), zero(T253))
addyc102_in_gga(T265, T266, T268) → U92_gga(T265, T266, T268, addzc79_in_gga(T265, T266, T268))
addzc79_in_gga(one(T278), one(T279), zero(T281)) → U74_gga(T278, T279, T281, addcc114_in_gga(T278, T279, T281))
addcc114_in_gga(b, b, one(b)) → addcc114_out_gga(b, b, one(b))
addcc114_in_gga(T290, b, T292) → U87_gga(T290, T292, succZc124_in_ga(T290, T292))
succZc124_in_ga(zero(T298), one(T298)) → U77_ga(T298, binaryZc54_in_g(T298))
U77_ga(T298, binaryZc54_out_g(T298)) → succZc124_out_ga(zero(T298), one(T298))
succZc124_in_ga(one(T304), zero(T306)) → U78_ga(T304, T306, succc131_in_ga(T304, T306))
succc131_in_ga(b, one(b)) → succc131_out_ga(b, one(b))
succc131_in_ga(zero(T311), one(T311)) → U75_ga(T311, binaryZc54_in_g(T311))
U75_ga(T311, binaryZc54_out_g(T311)) → succc131_out_ga(zero(T311), one(T311))
succc131_in_ga(one(T317), zero(T319)) → U76_ga(T317, T319, succc131_in_ga(T317, T319))
U76_ga(T317, T319, succc131_out_ga(T317, T319)) → succc131_out_ga(one(T317), zero(T319))
U78_ga(T304, T306, succc131_out_ga(T304, T306)) → succZc124_out_ga(one(T304), zero(T306))
U87_gga(T290, T292, succZc124_out_ga(T290, T292)) → addcc114_out_gga(T290, b, T292)
addcc114_in_gga(b, T328, T330) → U88_gga(T328, T330, succZc124_in_ga(T328, T330))
U88_gga(T328, T330, succZc124_out_ga(T328, T330)) → addcc114_out_gga(b, T328, T330)
addcc114_in_gga(T342, T343, T345) → U89_gga(T342, T343, T345, addCc149_in_gga(T342, T343, T345))
addCc149_in_gga(zero(T361), zero(T362), one(T364)) → U79_gga(T361, T362, T364, addzc79_in_gga(T361, T362, T364))
U79_gga(T361, T362, T364, addzc79_out_gga(T361, T362, T364)) → addCc149_out_gga(zero(T361), zero(T362), one(T364))
addCc149_in_gga(zero(zero(T389)), one(b), zero(one(T389))) → U80_gga(T389, binaryZc54_in_g(T389))
U80_gga(T389, binaryZc54_out_g(T389)) → addCc149_out_gga(zero(zero(T389)), one(b), zero(one(T389)))
addCc149_in_gga(zero(one(T399)), one(b), zero(zero(T401))) → U81_gga(T399, T401, succc131_in_ga(T399, T401))
U81_gga(T399, T401, succc131_out_ga(T399, T401)) → addCc149_out_gga(zero(one(T399)), one(b), zero(zero(T401)))
addCc149_in_gga(zero(T412), one(T413), zero(T415)) → U82_gga(T412, T413, T415, addCc149_in_gga(T412, T413, T415))
addCc149_in_gga(one(b), zero(zero(T440)), zero(one(T440))) → U83_gga(T440, binaryZc54_in_g(T440))
U83_gga(T440, binaryZc54_out_g(T440)) → addCc149_out_gga(one(b), zero(zero(T440)), zero(one(T440)))
addCc149_in_gga(one(b), zero(one(T450)), zero(zero(T452))) → U84_gga(T450, T452, succc131_in_ga(T450, T452))
U84_gga(T450, T452, succc131_out_ga(T450, T452)) → addCc149_out_gga(one(b), zero(one(T450)), zero(zero(T452)))
addCc149_in_gga(one(T463), zero(T464), zero(T466)) → U85_gga(T463, T464, T466, addCc149_in_gga(T463, T464, T466))
addCc149_in_gga(one(T476), one(T477), one(T479)) → U86_gga(T476, T477, T479, addcc114_in_gga(T476, T477, T479))
U86_gga(T476, T477, T479, addcc114_out_gga(T476, T477, T479)) → addCc149_out_gga(one(T476), one(T477), one(T479))
U85_gga(T463, T464, T466, addCc149_out_gga(T463, T464, T466)) → addCc149_out_gga(one(T463), zero(T464), zero(T466))
U82_gga(T412, T413, T415, addCc149_out_gga(T412, T413, T415)) → addCc149_out_gga(zero(T412), one(T413), zero(T415))
U89_gga(T342, T343, T345, addCc149_out_gga(T342, T343, T345)) → addcc114_out_gga(T342, T343, T345)
U74_gga(T278, T279, T281, addcc114_out_gga(T278, T279, T281)) → addzc79_out_gga(one(T278), one(T279), zero(T281))
U92_gga(T265, T266, T268, addzc79_out_gga(T265, T266, T268)) → addyc102_out_gga(T265, T266, T268)
U73_gga(T239, T240, T242, addyc102_out_gga(T239, T240, T242)) → addzc79_out_gga(one(T239), zero(T240), one(T242))
U72_gga(T220, T221, T223, addzc79_out_gga(T220, T221, T223)) → addzc79_out_gga(zero(T220), one(T221), one(T223))
U69_gga(T175, T176, T178, addzc79_out_gga(T175, T176, T178)) → addzc79_out_gga(zero(T175), zero(T176), zero(T178))
U63_gga(T156, T157, T159, addzc79_out_gga(T156, T157, T159)) → addc29_out_gga(zero(T156), T157, zero(T159))
addc29_in_gga(one(T493), T494, one(T496)) → U64_gga(T493, T494, T496, addyc102_in_gga(T493, T494, T496))
U64_gga(T493, T494, T496, addyc102_out_gga(T493, T494, T496)) → addc29_out_gga(one(T493), T494, one(T496))
U61_gga(T83, T84, X125, addc29_out_gga(T84, T87, X125)) → timesc28_out_gga(one(T83), T84, X125)
U59_gga(T75, T76, X106, timesc28_out_gga(T75, T76, X106)) → timesc28_out_gga(zero(T75), T76, zero(X106))

The argument filtering Pi contains the following mapping:
times1_in_gga(x1, x2, x3) = times1_in_gga(x1, x2)
zero(x1) = zero(x1)
one(x1) = one(x1)
times28_in_gga(x1, x2, x3) = times28_in_gga(x1, x2)
timesc28_in_gga(x1, x2, x3) = timesc28_in_gga(x1, x2)
b = b
timesc28_out_gga(x1, x2, x3) = timesc28_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addc29_in_gga(x1, x2, x3) = addc29_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZc54_in_g(x1) = binaryZc54_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binaryc60_in_g(x1) = binaryc60_in_g(x1)
binaryc60_out_g(x1) = binaryc60_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZc54_out_g(x1) = binaryZc54_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addc29_out_gga(x1, x2, x3) = addc29_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzc79_in_gga(x1, x2, x3) = addzc79_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzc79_out_gga(x1, x2, x3) = addzc79_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addyc102_in_gga(x1, x2, x3) = addyc102_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addyc102_out_gga(x1, x2, x3) = addyc102_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addcc114_in_gga(x1, x2, x3) = addcc114_in_gga(x1, x2)
addcc114_out_gga(x1, x2, x3) = addcc114_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZc124_in_ga(x1, x2) = succZc124_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZc124_out_ga(x1, x2) = succZc124_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succc131_in_ga(x1, x2) = succc131_in_ga(x1)
succc131_out_ga(x1, x2) = succc131_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCc149_in_gga(x1, x2, x3) = addCc149_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCc149_out_gga(x1, x2, x3) = addCc149_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
add29_in_gga(x1, x2, x3) = add29_in_gga(x1, x2)
binaryZ54_in_g(x1) = binaryZ54_in_g(x1)
binary60_in_g(x1) = binary60_in_g(x1)
addz79_in_gga(x1, x2, x3) = addz79_in_gga(x1, x2)
addy102_in_gga(x1, x2, x3) = addy102_in_gga(x1, x2)
addc114_in_gga(x1, x2, x3) = addc114_in_gga(x1, x2)
succZ124_in_ga(x1, x2) = succZ124_in_ga(x1)
succ131_in_ga(x1, x2) = succ131_in_ga(x1)
addC149_in_gga(x1, x2, x3) = addC149_in_gga(x1, x2)
TIMES1_IN_GGA(x1, x2, x3) = TIMES1_IN_GGA(x1, x2)
U36_GGA(x1, x2, x3, x4) = U36_GGA(x1, x2, x4)
U37_GGA(x1, x2, x3, x4) = U37_GGA(x1, x2, x4)
TIMES28_IN_GGA(x1, x2, x3) = TIMES28_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4) = U4_GGA(x1, x2, x4)
ADD29_IN_GGA(x1, x2, x3) = ADD29_IN_GGA(x1, x2)
U5_GGA(x1, x2) = U5_GGA(x1, x2)
BINARYZ54_IN_G(x1) = BINARYZ54_IN_G(x1)
U8_G(x1, x2) = U8_G(x1, x2)
U9_G(x1, x2) = U9_G(x1, x2)
BINARY60_IN_G(x1) = BINARY60_IN_G(x1)
U10_G(x1, x2) = U10_G(x1, x2)
U11_G(x1, x2) = U11_G(x1, x2)
U6_GGA(x1, x2, x3, x4) = U6_GGA(x1, x2, x4)
ADDZ79_IN_GGA(x1, x2, x3) = ADDZ79_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3, x4) = U12_GGA(x1, x2, x4)
U13_GGA(x1, x2) = U13_GGA(x1, x2)
U14_GGA(x1, x2) = U14_GGA(x1, x2)
U15_GGA(x1, x2, x3, x4) = U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4) = U16_GGA(x1, x2, x4)
ADDY102_IN_GGA(x1, x2, x3) = ADDY102_IN_GGA(x1, x2)
U33_GGA(x1, x2) = U33_GGA(x1, x2)
U34_GGA(x1, x2) = U34_GGA(x1, x2)
U35_GGA(x1, x2, x3, x4) = U35_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4) = U17_GGA(x1, x2, x4)
ADDC114_IN_GGA(x1, x2, x3) = ADDC114_IN_GGA(x1, x2)
U30_GGA(x1, x2, x3) = U30_GGA(x1, x3)
SUCCZ124_IN_GA(x1, x2) = SUCCZ124_IN_GA(x1)
U20_GA(x1, x2) = U20_GA(x1, x2)
U21_GA(x1, x2, x3) = U21_GA(x1, x3)
SUCC131_IN_GA(x1, x2) = SUCC131_IN_GA(x1)
U18_GA(x1, x2) = U18_GA(x1, x2)
U19_GA(x1, x2, x3) = U19_GA(x1, x3)
U31_GGA(x1, x2, x3) = U31_GGA(x1, x3)
U32_GGA(x1, x2, x3, x4) = U32_GGA(x1, x2, x4)
ADDC149_IN_GGA(x1, x2, x3) = ADDC149_IN_GGA(x1, x2)
U22_GGA(x1, x2, x3, x4) = U22_GGA(x1, x2, x4)
U23_GGA(x1, x2) = U23_GGA(x1, x2)
U24_GGA(x1, x2, x3) = U24_GGA(x1, x3)
U25_GGA(x1, x2, x3, x4) = U25_GGA(x1, x2, x4)
U26_GGA(x1, x2) = U26_GGA(x1, x2)
U27_GGA(x1, x2, x3) = U27_GGA(x1, x3)
U28_GGA(x1, x2, x3, x4) = U28_GGA(x1, x2, x4)
U29_GGA(x1, x2, x3, x4) = U29_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4) = U7_GGA(x1, x2, x4)
U38_GGA(x1, x2, x3, x4) = U38_GGA(x1, x2, x4)
U39_GGA(x1, x2, x3, x4) = U39_GGA(x1, x2, x4)
U40_GGA(x1, x2, x3) = U40_GGA(x1, x3)
U41_GGA(x1, x2, x3, x4) = U41_GGA(x1, x2, x4)
U42_GGA(x1, x2, x3, x4) = U42_GGA(x1, x2, x4)
U43_GGA(x1, x2, x3, x4) = U43_GGA(x1, x2, x4)
U44_GGA(x1, x2, x3, x4) = U44_GGA(x1, x2, x4)
U45_GGA(x1, x2, x3, x4) = U45_GGA(x1, x2, x4)
U46_GGA(x1, x2, x3, x4) = U46_GGA(x1, x2, x4)
U47_GGA(x1, x2, x3, x4) = U47_GGA(x1, x2, x4)
U48_GGA(x1, x2, x3, x4) = U48_GGA(x1, x2, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

TIMES1_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → U36_GGA(T35, T36, T38, times1_in_gga(T35, T36, T38))
TIMES1_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → TIMES1_IN_GGA(T35, T36, T38)
TIMES1_IN_GGA(zero(one(T53)), T54, zero(T56)) → U37_GGA(T53, T54, T56, times28_in_gga(T53, T54, X73))
TIMES1_IN_GGA(zero(one(T53)), T54, zero(T56)) → TIMES28_IN_GGA(T53, T54, X73)
TIMES28_IN_GGA(zero(T75), T76, zero(X106)) → U1_GGA(T75, T76, X106, times28_in_gga(T75, T76, X106))
TIMES28_IN_GGA(zero(T75), T76, zero(X106)) → TIMES28_IN_GGA(T75, T76, X106)
TIMES28_IN_GGA(one(T83), T84, X125) → U2_GGA(T83, T84, X125, times28_in_gga(T83, T84, X124))
TIMES28_IN_GGA(one(T83), T84, X125) → TIMES28_IN_GGA(T83, T84, X124)
TIMES28_IN_GGA(one(T83), T84, X125) → U3_GGA(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U3_GGA(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U4_GGA(T83, T84, X125, add29_in_gga(T84, T87, X125))
U3_GGA(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → ADD29_IN_GGA(T84, T87, X125)
ADD29_IN_GGA(b, T107, zero(T107)) → U5_GGA(T107, binaryZ54_in_g(T107))
ADD29_IN_GGA(b, T107, zero(T107)) → BINARYZ54_IN_G(T107)
BINARYZ54_IN_G(zero(T113)) → U8_G(T113, binaryZ54_in_g(T113))
BINARYZ54_IN_G(zero(T113)) → BINARYZ54_IN_G(T113)
BINARYZ54_IN_G(one(T117)) → U9_G(T117, binary60_in_g(T117))
BINARYZ54_IN_G(one(T117)) → BINARY60_IN_G(T117)
BINARY60_IN_G(zero(T122)) → U10_G(T122, binaryZ54_in_g(T122))
BINARY60_IN_G(zero(T122)) → BINARYZ54_IN_G(T122)
BINARY60_IN_G(one(T126)) → U11_G(T126, binary60_in_g(T126))
BINARY60_IN_G(one(T126)) → BINARY60_IN_G(T126)
ADD29_IN_GGA(zero(T156), T157, zero(T159)) → U6_GGA(T156, T157, T159, addz79_in_gga(T156, T157, T159))
ADD29_IN_GGA(zero(T156), T157, zero(T159)) → ADDZ79_IN_GGA(T156, T157, T159)
ADDZ79_IN_GGA(zero(T175), zero(T176), zero(T178)) → U12_GGA(T175, T176, T178, addz79_in_gga(T175, T176, T178))
ADDZ79_IN_GGA(zero(T175), zero(T176), zero(T178)) → ADDZ79_IN_GGA(T175, T176, T178)
ADDZ79_IN_GGA(zero(one(T203)), one(b), one(one(T203))) → U13_GGA(T203, binary60_in_g(T203))
ADDZ79_IN_GGA(zero(one(T203)), one(b), one(one(T203))) → BINARY60_IN_G(T203)
ADDZ79_IN_GGA(zero(zero(T208)), one(b), one(zero(T208))) → U14_GGA(T208, binaryZ54_in_g(T208))
ADDZ79_IN_GGA(zero(zero(T208)), one(b), one(zero(T208))) → BINARYZ54_IN_G(T208)
ADDZ79_IN_GGA(zero(T220), one(T221), one(T223)) → U15_GGA(T220, T221, T223, addz79_in_gga(T220, T221, T223))
ADDZ79_IN_GGA(zero(T220), one(T221), one(T223)) → ADDZ79_IN_GGA(T220, T221, T223)
ADDZ79_IN_GGA(one(T239), zero(T240), one(T242)) → U16_GGA(T239, T240, T242, addy102_in_gga(T239, T240, T242))
ADDZ79_IN_GGA(one(T239), zero(T240), one(T242)) → ADDY102_IN_GGA(T239, T240, T242)
ADDY102_IN_GGA(b, one(T248), one(T248)) → U33_GGA(T248, binary60_in_g(T248))
ADDY102_IN_GGA(b, one(T248), one(T248)) → BINARY60_IN_G(T248)
ADDY102_IN_GGA(b, zero(T253), zero(T253)) → U34_GGA(T253, binaryZ54_in_g(T253))
ADDY102_IN_GGA(b, zero(T253), zero(T253)) → BINARYZ54_IN_G(T253)
ADDY102_IN_GGA(T265, T266, T268) → U35_GGA(T265, T266, T268, addz79_in_gga(T265, T266, T268))
ADDY102_IN_GGA(T265, T266, T268) → ADDZ79_IN_GGA(T265, T266, T268)
ADDZ79_IN_GGA(one(T278), one(T279), zero(T281)) → U17_GGA(T278, T279, T281, addc114_in_gga(T278, T279, T281))
ADDZ79_IN_GGA(one(T278), one(T279), zero(T281)) → ADDC114_IN_GGA(T278, T279, T281)
ADDC114_IN_GGA(T290, b, T292) → U30_GGA(T290, T292, succZ124_in_ga(T290, T292))
ADDC114_IN_GGA(T290, b, T292) → SUCCZ124_IN_GA(T290, T292)
SUCCZ124_IN_GA(zero(T298), one(T298)) → U20_GA(T298, binaryZ54_in_g(T298))
SUCCZ124_IN_GA(zero(T298), one(T298)) → BINARYZ54_IN_G(T298)
SUCCZ124_IN_GA(one(T304), zero(T306)) → U21_GA(T304, T306, succ131_in_ga(T304, T306))
SUCCZ124_IN_GA(one(T304), zero(T306)) → SUCC131_IN_GA(T304, T306)
SUCC131_IN_GA(zero(T311), one(T311)) → U18_GA(T311, binaryZ54_in_g(T311))
SUCC131_IN_GA(zero(T311), one(T311)) → BINARYZ54_IN_G(T311)
SUCC131_IN_GA(one(T317), zero(T319)) → U19_GA(T317, T319, succ131_in_ga(T317, T319))
SUCC131_IN_GA(one(T317), zero(T319)) → SUCC131_IN_GA(T317, T319)
ADDC114_IN_GGA(b, T328, T330) → U31_GGA(T328, T330, succZ124_in_ga(T328, T330))
ADDC114_IN_GGA(b, T328, T330) → SUCCZ124_IN_GA(T328, T330)
ADDC114_IN_GGA(T342, T343, T345) → U32_GGA(T342, T343, T345, addC149_in_gga(T342, T343, T345))
ADDC114_IN_GGA(T342, T343, T345) → ADDC149_IN_GGA(T342, T343, T345)
ADDC149_IN_GGA(zero(T361), zero(T362), one(T364)) → U22_GGA(T361, T362, T364, addz79_in_gga(T361, T362, T364))
ADDC149_IN_GGA(zero(T361), zero(T362), one(T364)) → ADDZ79_IN_GGA(T361, T362, T364)
ADDC149_IN_GGA(zero(zero(T389)), one(b), zero(one(T389))) → U23_GGA(T389, binaryZ54_in_g(T389))
ADDC149_IN_GGA(zero(zero(T389)), one(b), zero(one(T389))) → BINARYZ54_IN_G(T389)
ADDC149_IN_GGA(zero(one(T399)), one(b), zero(zero(T401))) → U24_GGA(T399, T401, succ131_in_ga(T399, T401))
ADDC149_IN_GGA(zero(one(T399)), one(b), zero(zero(T401))) → SUCC131_IN_GA(T399, T401)
ADDC149_IN_GGA(zero(T412), one(T413), zero(T415)) → U25_GGA(T412, T413, T415, addC149_in_gga(T412, T413, T415))
ADDC149_IN_GGA(zero(T412), one(T413), zero(T415)) → ADDC149_IN_GGA(T412, T413, T415)
ADDC149_IN_GGA(one(b), zero(zero(T440)), zero(one(T440))) → U26_GGA(T440, binaryZ54_in_g(T440))
ADDC149_IN_GGA(one(b), zero(zero(T440)), zero(one(T440))) → BINARYZ54_IN_G(T440)
ADDC149_IN_GGA(one(b), zero(one(T450)), zero(zero(T452))) → U27_GGA(T450, T452, succ131_in_ga(T450, T452))
ADDC149_IN_GGA(one(b), zero(one(T450)), zero(zero(T452))) → SUCC131_IN_GA(T450, T452)
ADDC149_IN_GGA(one(T463), zero(T464), zero(T466)) → U28_GGA(T463, T464, T466, addC149_in_gga(T463, T464, T466))
ADDC149_IN_GGA(one(T463), zero(T464), zero(T466)) → ADDC149_IN_GGA(T463, T464, T466)
ADDC149_IN_GGA(one(T476), one(T477), one(T479)) → U29_GGA(T476, T477, T479, addc114_in_gga(T476, T477, T479))
ADDC149_IN_GGA(one(T476), one(T477), one(T479)) → ADDC114_IN_GGA(T476, T477, T479)
ADD29_IN_GGA(one(T493), T494, one(T496)) → U7_GGA(T493, T494, T496, addy102_in_gga(T493, T494, T496))
ADD29_IN_GGA(one(T493), T494, one(T496)) → ADDY102_IN_GGA(T493, T494, T496)
TIMES1_IN_GGA(zero(one(T53)), T54, zero(T56)) → U38_GGA(T53, T54, T56, timesc28_in_gga(T53, T54, T59))
U38_GGA(T53, T54, T56, timesc28_out_gga(T53, T54, T59)) → U39_GGA(T53, T54, T56, add29_in_gga(T54, T59, T56))
U38_GGA(T53, T54, T56, timesc28_out_gga(T53, T54, T59)) → ADD29_IN_GGA(T54, T59, T56)
TIMES1_IN_GGA(one(one(b)), T510, T505) → U40_GGA(T510, T505, add29_in_gga(T510, T510, T505))
TIMES1_IN_GGA(one(one(b)), T510, T505) → ADD29_IN_GGA(T510, T510, T505)
TIMES1_IN_GGA(one(zero(T520)), T521, T505) → U41_GGA(T520, T521, T505, times28_in_gga(T520, T521, X614))
TIMES1_IN_GGA(one(zero(T520)), T521, T505) → TIMES28_IN_GGA(T520, T521, X614)
TIMES1_IN_GGA(one(zero(T520)), T521, T505) → U42_GGA(T520, T521, T505, timesc28_in_gga(T520, T521, T524))
U42_GGA(T520, T521, T505, timesc28_out_gga(T520, T521, T524)) → U43_GGA(T520, T521, T505, add29_in_gga(T521, zero(T524), T505))
U42_GGA(T520, T521, T505, timesc28_out_gga(T520, T521, T524)) → ADD29_IN_GGA(T521, zero(T524), T505)
TIMES1_IN_GGA(one(one(T533)), T534, T505) → U44_GGA(T533, T534, T505, times28_in_gga(T533, T534, X636))
TIMES1_IN_GGA(one(one(T533)), T534, T505) → TIMES28_IN_GGA(T533, T534, X636)
TIMES1_IN_GGA(one(one(T533)), T534, T505) → U45_GGA(T533, T534, T505, timesc28_in_gga(T533, T534, T537))
U45_GGA(T533, T534, T505, timesc28_out_gga(T533, T534, T537)) → U46_GGA(T533, T534, T505, add29_in_gga(T534, T537, X637))
U45_GGA(T533, T534, T505, timesc28_out_gga(T533, T534, T537)) → ADD29_IN_GGA(T534, T537, X637)
U45_GGA(T533, T534, T505, timesc28_out_gga(T533, T534, T537)) → U47_GGA(T533, T534, T505, addc29_in_gga(T534, T537, T542))
U47_GGA(T533, T534, T505, addc29_out_gga(T534, T537, T542)) → U48_GGA(T533, T534, T505, add29_in_gga(T534, T542, T505))
U47_GGA(T533, T534, T505, addc29_out_gga(T534, T537, T542)) → ADD29_IN_GGA(T534, T542, T505)

The TRS R consists of the following rules:

timesc28_in_gga(one(b), T66, T66) → timesc28_out_gga(one(b), T66, T66)
timesc28_in_gga(zero(T75), T76, zero(X106)) → U59_gga(T75, T76, X106, timesc28_in_gga(T75, T76, X106))
timesc28_in_gga(one(T83), T84, X125) → U60_gga(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U60_gga(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U61_gga(T83, T84, X125, addc29_in_gga(T84, T87, X125))
addc29_in_gga(b, T107, zero(T107)) → U62_gga(T107, binaryZc54_in_g(T107))
binaryZc54_in_g(zero(T113)) → U65_g(T113, binaryZc54_in_g(T113))
binaryZc54_in_g(one(T117)) → U66_g(T117, binaryc60_in_g(T117))
binaryc60_in_g(b) → binaryc60_out_g(b)
binaryc60_in_g(zero(T122)) → U67_g(T122, binaryZc54_in_g(T122))
U67_g(T122, binaryZc54_out_g(T122)) → binaryc60_out_g(zero(T122))
binaryc60_in_g(one(T126)) → U68_g(T126, binaryc60_in_g(T126))
U68_g(T126, binaryc60_out_g(T126)) → binaryc60_out_g(one(T126))
U66_g(T117, binaryc60_out_g(T117)) → binaryZc54_out_g(one(T117))
U65_g(T113, binaryZc54_out_g(T113)) → binaryZc54_out_g(zero(T113))
U62_gga(T107, binaryZc54_out_g(T107)) → addc29_out_gga(b, T107, zero(T107))
addc29_in_gga(zero(T156), T157, zero(T159)) → U63_gga(T156, T157, T159, addzc79_in_gga(T156, T157, T159))
addzc79_in_gga(zero(T175), zero(T176), zero(T178)) → U69_gga(T175, T176, T178, addzc79_in_gga(T175, T176, T178))
addzc79_in_gga(zero(one(T203)), one(b), one(one(T203))) → U70_gga(T203, binaryc60_in_g(T203))
U70_gga(T203, binaryc60_out_g(T203)) → addzc79_out_gga(zero(one(T203)), one(b), one(one(T203)))
addzc79_in_gga(zero(zero(T208)), one(b), one(zero(T208))) → U71_gga(T208, binaryZc54_in_g(T208))
U71_gga(T208, binaryZc54_out_g(T208)) → addzc79_out_gga(zero(zero(T208)), one(b), one(zero(T208)))
addzc79_in_gga(zero(T220), one(T221), one(T223)) → U72_gga(T220, T221, T223, addzc79_in_gga(T220, T221, T223))
addzc79_in_gga(one(T239), zero(T240), one(T242)) → U73_gga(T239, T240, T242, addyc102_in_gga(T239, T240, T242))
addyc102_in_gga(b, one(T248), one(T248)) → U90_gga(T248, binaryc60_in_g(T248))
U90_gga(T248, binaryc60_out_g(T248)) → addyc102_out_gga(b, one(T248), one(T248))
addyc102_in_gga(b, zero(T253), zero(T253)) → U91_gga(T253, binaryZc54_in_g(T253))
U91_gga(T253, binaryZc54_out_g(T253)) → addyc102_out_gga(b, zero(T253), zero(T253))
addyc102_in_gga(T265, T266, T268) → U92_gga(T265, T266, T268, addzc79_in_gga(T265, T266, T268))
addzc79_in_gga(one(T278), one(T279), zero(T281)) → U74_gga(T278, T279, T281, addcc114_in_gga(T278, T279, T281))
addcc114_in_gga(b, b, one(b)) → addcc114_out_gga(b, b, one(b))
addcc114_in_gga(T290, b, T292) → U87_gga(T290, T292, succZc124_in_ga(T290, T292))
succZc124_in_ga(zero(T298), one(T298)) → U77_ga(T298, binaryZc54_in_g(T298))
U77_ga(T298, binaryZc54_out_g(T298)) → succZc124_out_ga(zero(T298), one(T298))
succZc124_in_ga(one(T304), zero(T306)) → U78_ga(T304, T306, succc131_in_ga(T304, T306))
succc131_in_ga(b, one(b)) → succc131_out_ga(b, one(b))
succc131_in_ga(zero(T311), one(T311)) → U75_ga(T311, binaryZc54_in_g(T311))
U75_ga(T311, binaryZc54_out_g(T311)) → succc131_out_ga(zero(T311), one(T311))
succc131_in_ga(one(T317), zero(T319)) → U76_ga(T317, T319, succc131_in_ga(T317, T319))
U76_ga(T317, T319, succc131_out_ga(T317, T319)) → succc131_out_ga(one(T317), zero(T319))
U78_ga(T304, T306, succc131_out_ga(T304, T306)) → succZc124_out_ga(one(T304), zero(T306))
U87_gga(T290, T292, succZc124_out_ga(T290, T292)) → addcc114_out_gga(T290, b, T292)
addcc114_in_gga(b, T328, T330) → U88_gga(T328, T330, succZc124_in_ga(T328, T330))
U88_gga(T328, T330, succZc124_out_ga(T328, T330)) → addcc114_out_gga(b, T328, T330)
addcc114_in_gga(T342, T343, T345) → U89_gga(T342, T343, T345, addCc149_in_gga(T342, T343, T345))
addCc149_in_gga(zero(T361), zero(T362), one(T364)) → U79_gga(T361, T362, T364, addzc79_in_gga(T361, T362, T364))
U79_gga(T361, T362, T364, addzc79_out_gga(T361, T362, T364)) → addCc149_out_gga(zero(T361), zero(T362), one(T364))
addCc149_in_gga(zero(zero(T389)), one(b), zero(one(T389))) → U80_gga(T389, binaryZc54_in_g(T389))
U80_gga(T389, binaryZc54_out_g(T389)) → addCc149_out_gga(zero(zero(T389)), one(b), zero(one(T389)))
addCc149_in_gga(zero(one(T399)), one(b), zero(zero(T401))) → U81_gga(T399, T401, succc131_in_ga(T399, T401))
U81_gga(T399, T401, succc131_out_ga(T399, T401)) → addCc149_out_gga(zero(one(T399)), one(b), zero(zero(T401)))
addCc149_in_gga(zero(T412), one(T413), zero(T415)) → U82_gga(T412, T413, T415, addCc149_in_gga(T412, T413, T415))
addCc149_in_gga(one(b), zero(zero(T440)), zero(one(T440))) → U83_gga(T440, binaryZc54_in_g(T440))
U83_gga(T440, binaryZc54_out_g(T440)) → addCc149_out_gga(one(b), zero(zero(T440)), zero(one(T440)))
addCc149_in_gga(one(b), zero(one(T450)), zero(zero(T452))) → U84_gga(T450, T452, succc131_in_ga(T450, T452))
U84_gga(T450, T452, succc131_out_ga(T450, T452)) → addCc149_out_gga(one(b), zero(one(T450)), zero(zero(T452)))
addCc149_in_gga(one(T463), zero(T464), zero(T466)) → U85_gga(T463, T464, T466, addCc149_in_gga(T463, T464, T466))
addCc149_in_gga(one(T476), one(T477), one(T479)) → U86_gga(T476, T477, T479, addcc114_in_gga(T476, T477, T479))
U86_gga(T476, T477, T479, addcc114_out_gga(T476, T477, T479)) → addCc149_out_gga(one(T476), one(T477), one(T479))
U85_gga(T463, T464, T466, addCc149_out_gga(T463, T464, T466)) → addCc149_out_gga(one(T463), zero(T464), zero(T466))
U82_gga(T412, T413, T415, addCc149_out_gga(T412, T413, T415)) → addCc149_out_gga(zero(T412), one(T413), zero(T415))
U89_gga(T342, T343, T345, addCc149_out_gga(T342, T343, T345)) → addcc114_out_gga(T342, T343, T345)
U74_gga(T278, T279, T281, addcc114_out_gga(T278, T279, T281)) → addzc79_out_gga(one(T278), one(T279), zero(T281))
U92_gga(T265, T266, T268, addzc79_out_gga(T265, T266, T268)) → addyc102_out_gga(T265, T266, T268)
U73_gga(T239, T240, T242, addyc102_out_gga(T239, T240, T242)) → addzc79_out_gga(one(T239), zero(T240), one(T242))
U72_gga(T220, T221, T223, addzc79_out_gga(T220, T221, T223)) → addzc79_out_gga(zero(T220), one(T221), one(T223))
U69_gga(T175, T176, T178, addzc79_out_gga(T175, T176, T178)) → addzc79_out_gga(zero(T175), zero(T176), zero(T178))
U63_gga(T156, T157, T159, addzc79_out_gga(T156, T157, T159)) → addc29_out_gga(zero(T156), T157, zero(T159))
addc29_in_gga(one(T493), T494, one(T496)) → U64_gga(T493, T494, T496, addyc102_in_gga(T493, T494, T496))
U64_gga(T493, T494, T496, addyc102_out_gga(T493, T494, T496)) → addc29_out_gga(one(T493), T494, one(T496))
U61_gga(T83, T84, X125, addc29_out_gga(T84, T87, X125)) → timesc28_out_gga(one(T83), T84, X125)
U59_gga(T75, T76, X106, timesc28_out_gga(T75, T76, X106)) → timesc28_out_gga(zero(T75), T76, zero(X106))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 73 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

BINARYZ54_IN_G(one(T117)) → BINARY60_IN_G(T117)
BINARY60_IN_G(zero(T122)) → BINARYZ54_IN_G(T122)
BINARYZ54_IN_G(zero(T113)) → BINARYZ54_IN_G(T113)
BINARY60_IN_G(one(T126)) → BINARY60_IN_G(T126)

The TRS R consists of the following rules:

timesc28_in_gga(one(b), T66, T66) → timesc28_out_gga(one(b), T66, T66)
timesc28_in_gga(zero(T75), T76, zero(X106)) → U59_gga(T75, T76, X106, timesc28_in_gga(T75, T76, X106))
timesc28_in_gga(one(T83), T84, X125) → U60_gga(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U60_gga(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U61_gga(T83, T84, X125, addc29_in_gga(T84, T87, X125))
addc29_in_gga(b, T107, zero(T107)) → U62_gga(T107, binaryZc54_in_g(T107))
binaryZc54_in_g(zero(T113)) → U65_g(T113, binaryZc54_in_g(T113))
binaryZc54_in_g(one(T117)) → U66_g(T117, binaryc60_in_g(T117))
binaryc60_in_g(b) → binaryc60_out_g(b)
binaryc60_in_g(zero(T122)) → U67_g(T122, binaryZc54_in_g(T122))
U67_g(T122, binaryZc54_out_g(T122)) → binaryc60_out_g(zero(T122))
binaryc60_in_g(one(T126)) → U68_g(T126, binaryc60_in_g(T126))
U68_g(T126, binaryc60_out_g(T126)) → binaryc60_out_g(one(T126))
U66_g(T117, binaryc60_out_g(T117)) → binaryZc54_out_g(one(T117))
U65_g(T113, binaryZc54_out_g(T113)) → binaryZc54_out_g(zero(T113))
U62_gga(T107, binaryZc54_out_g(T107)) → addc29_out_gga(b, T107, zero(T107))
addc29_in_gga(zero(T156), T157, zero(T159)) → U63_gga(T156, T157, T159, addzc79_in_gga(T156, T157, T159))
addzc79_in_gga(zero(T175), zero(T176), zero(T178)) → U69_gga(T175, T176, T178, addzc79_in_gga(T175, T176, T178))
addzc79_in_gga(zero(one(T203)), one(b), one(one(T203))) → U70_gga(T203, binaryc60_in_g(T203))
U70_gga(T203, binaryc60_out_g(T203)) → addzc79_out_gga(zero(one(T203)), one(b), one(one(T203)))
addzc79_in_gga(zero(zero(T208)), one(b), one(zero(T208))) → U71_gga(T208, binaryZc54_in_g(T208))
U71_gga(T208, binaryZc54_out_g(T208)) → addzc79_out_gga(zero(zero(T208)), one(b), one(zero(T208)))
addzc79_in_gga(zero(T220), one(T221), one(T223)) → U72_gga(T220, T221, T223, addzc79_in_gga(T220, T221, T223))
addzc79_in_gga(one(T239), zero(T240), one(T242)) → U73_gga(T239, T240, T242, addyc102_in_gga(T239, T240, T242))
addyc102_in_gga(b, one(T248), one(T248)) → U90_gga(T248, binaryc60_in_g(T248))
U90_gga(T248, binaryc60_out_g(T248)) → addyc102_out_gga(b, one(T248), one(T248))
addyc102_in_gga(b, zero(T253), zero(T253)) → U91_gga(T253, binaryZc54_in_g(T253))
U91_gga(T253, binaryZc54_out_g(T253)) → addyc102_out_gga(b, zero(T253), zero(T253))
addyc102_in_gga(T265, T266, T268) → U92_gga(T265, T266, T268, addzc79_in_gga(T265, T266, T268))
addzc79_in_gga(one(T278), one(T279), zero(T281)) → U74_gga(T278, T279, T281, addcc114_in_gga(T278, T279, T281))
addcc114_in_gga(b, b, one(b)) → addcc114_out_gga(b, b, one(b))
addcc114_in_gga(T290, b, T292) → U87_gga(T290, T292, succZc124_in_ga(T290, T292))
succZc124_in_ga(zero(T298), one(T298)) → U77_ga(T298, binaryZc54_in_g(T298))
U77_ga(T298, binaryZc54_out_g(T298)) → succZc124_out_ga(zero(T298), one(T298))
succZc124_in_ga(one(T304), zero(T306)) → U78_ga(T304, T306, succc131_in_ga(T304, T306))
succc131_in_ga(b, one(b)) → succc131_out_ga(b, one(b))
succc131_in_ga(zero(T311), one(T311)) → U75_ga(T311, binaryZc54_in_g(T311))
U75_ga(T311, binaryZc54_out_g(T311)) → succc131_out_ga(zero(T311), one(T311))
succc131_in_ga(one(T317), zero(T319)) → U76_ga(T317, T319, succc131_in_ga(T317, T319))
U76_ga(T317, T319, succc131_out_ga(T317, T319)) → succc131_out_ga(one(T317), zero(T319))
U78_ga(T304, T306, succc131_out_ga(T304, T306)) → succZc124_out_ga(one(T304), zero(T306))
U87_gga(T290, T292, succZc124_out_ga(T290, T292)) → addcc114_out_gga(T290, b, T292)
addcc114_in_gga(b, T328, T330) → U88_gga(T328, T330, succZc124_in_ga(T328, T330))
U88_gga(T328, T330, succZc124_out_ga(T328, T330)) → addcc114_out_gga(b, T328, T330)
addcc114_in_gga(T342, T343, T345) → U89_gga(T342, T343, T345, addCc149_in_gga(T342, T343, T345))
addCc149_in_gga(zero(T361), zero(T362), one(T364)) → U79_gga(T361, T362, T364, addzc79_in_gga(T361, T362, T364))
U79_gga(T361, T362, T364, addzc79_out_gga(T361, T362, T364)) → addCc149_out_gga(zero(T361), zero(T362), one(T364))
addCc149_in_gga(zero(zero(T389)), one(b), zero(one(T389))) → U80_gga(T389, binaryZc54_in_g(T389))
U80_gga(T389, binaryZc54_out_g(T389)) → addCc149_out_gga(zero(zero(T389)), one(b), zero(one(T389)))
addCc149_in_gga(zero(one(T399)), one(b), zero(zero(T401))) → U81_gga(T399, T401, succc131_in_ga(T399, T401))
U81_gga(T399, T401, succc131_out_ga(T399, T401)) → addCc149_out_gga(zero(one(T399)), one(b), zero(zero(T401)))
addCc149_in_gga(zero(T412), one(T413), zero(T415)) → U82_gga(T412, T413, T415, addCc149_in_gga(T412, T413, T415))
addCc149_in_gga(one(b), zero(zero(T440)), zero(one(T440))) → U83_gga(T440, binaryZc54_in_g(T440))
U83_gga(T440, binaryZc54_out_g(T440)) → addCc149_out_gga(one(b), zero(zero(T440)), zero(one(T440)))
addCc149_in_gga(one(b), zero(one(T450)), zero(zero(T452))) → U84_gga(T450, T452, succc131_in_ga(T450, T452))
U84_gga(T450, T452, succc131_out_ga(T450, T452)) → addCc149_out_gga(one(b), zero(one(T450)), zero(zero(T452)))
addCc149_in_gga(one(T463), zero(T464), zero(T466)) → U85_gga(T463, T464, T466, addCc149_in_gga(T463, T464, T466))
addCc149_in_gga(one(T476), one(T477), one(T479)) → U86_gga(T476, T477, T479, addcc114_in_gga(T476, T477, T479))
U86_gga(T476, T477, T479, addcc114_out_gga(T476, T477, T479)) → addCc149_out_gga(one(T476), one(T477), one(T479))
U85_gga(T463, T464, T466, addCc149_out_gga(T463, T464, T466)) → addCc149_out_gga(one(T463), zero(T464), zero(T466))
U82_gga(T412, T413, T415, addCc149_out_gga(T412, T413, T415)) → addCc149_out_gga(zero(T412), one(T413), zero(T415))
U89_gga(T342, T343, T345, addCc149_out_gga(T342, T343, T345)) → addcc114_out_gga(T342, T343, T345)
U74_gga(T278, T279, T281, addcc114_out_gga(T278, T279, T281)) → addzc79_out_gga(one(T278), one(T279), zero(T281))
U92_gga(T265, T266, T268, addzc79_out_gga(T265, T266, T268)) → addyc102_out_gga(T265, T266, T268)
U73_gga(T239, T240, T242, addyc102_out_gga(T239, T240, T242)) → addzc79_out_gga(one(T239), zero(T240), one(T242))
U72_gga(T220, T221, T223, addzc79_out_gga(T220, T221, T223)) → addzc79_out_gga(zero(T220), one(T221), one(T223))
U69_gga(T175, T176, T178, addzc79_out_gga(T175, T176, T178)) → addzc79_out_gga(zero(T175), zero(T176), zero(T178))
U63_gga(T156, T157, T159, addzc79_out_gga(T156, T157, T159)) → addc29_out_gga(zero(T156), T157, zero(T159))
addc29_in_gga(one(T493), T494, one(T496)) → U64_gga(T493, T494, T496, addyc102_in_gga(T493, T494, T496))
U64_gga(T493, T494, T496, addyc102_out_gga(T493, T494, T496)) → addc29_out_gga(one(T493), T494, one(T496))
U61_gga(T83, T84, X125, addc29_out_gga(T84, T87, X125)) → timesc28_out_gga(one(T83), T84, X125)
U59_gga(T75, T76, X106, timesc28_out_gga(T75, T76, X106)) → timesc28_out_gga(zero(T75), T76, zero(X106))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timesc28_in_gga(x1, x2, x3) = timesc28_in_gga(x1, x2)
b = b
timesc28_out_gga(x1, x2, x3) = timesc28_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addc29_in_gga(x1, x2, x3) = addc29_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZc54_in_g(x1) = binaryZc54_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binaryc60_in_g(x1) = binaryc60_in_g(x1)
binaryc60_out_g(x1) = binaryc60_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZc54_out_g(x1) = binaryZc54_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addc29_out_gga(x1, x2, x3) = addc29_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzc79_in_gga(x1, x2, x3) = addzc79_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzc79_out_gga(x1, x2, x3) = addzc79_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addyc102_in_gga(x1, x2, x3) = addyc102_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addyc102_out_gga(x1, x2, x3) = addyc102_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addcc114_in_gga(x1, x2, x3) = addcc114_in_gga(x1, x2)
addcc114_out_gga(x1, x2, x3) = addcc114_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZc124_in_ga(x1, x2) = succZc124_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZc124_out_ga(x1, x2) = succZc124_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succc131_in_ga(x1, x2) = succc131_in_ga(x1)
succc131_out_ga(x1, x2) = succc131_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCc149_in_gga(x1, x2, x3) = addCc149_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCc149_out_gga(x1, x2, x3) = addCc149_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
BINARYZ54_IN_G(x1) = BINARYZ54_IN_G(x1)
BINARY60_IN_G(x1) = BINARY60_IN_G(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

BINARYZ54_IN_G(one(T117)) → BINARY60_IN_G(T117)
BINARY60_IN_G(zero(T122)) → BINARYZ54_IN_G(T122)
BINARYZ54_IN_G(zero(T113)) → BINARYZ54_IN_G(T113)
BINARY60_IN_G(one(T126)) → BINARY60_IN_G(T126)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

BINARYZ54_IN_G(one(T117)) → BINARY60_IN_G(T117)
BINARY60_IN_G(zero(T122)) → BINARYZ54_IN_G(T122)
BINARYZ54_IN_G(zero(T113)) → BINARYZ54_IN_G(T113)
BINARY60_IN_G(one(T126)) → BINARY60_IN_G(T126)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

BINARY60_IN_G(zero(T122)) → BINARYZ54_IN_G(T122)
The graph contains the following edges 1 > 1
BINARY60_IN_G(one(T126)) → BINARY60_IN_G(T126)
The graph contains the following edges 1 > 1
BINARYZ54_IN_G(zero(T113)) → BINARYZ54_IN_G(T113)
The graph contains the following edges 1 > 1
BINARYZ54_IN_G(one(T117)) → BINARY60_IN_G(T117)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

SUCC131_IN_GA(one(T317), zero(T319)) → SUCC131_IN_GA(T317, T319)

The TRS R consists of the following rules:

timesc28_in_gga(one(b), T66, T66) → timesc28_out_gga(one(b), T66, T66)
timesc28_in_gga(zero(T75), T76, zero(X106)) → U59_gga(T75, T76, X106, timesc28_in_gga(T75, T76, X106))
timesc28_in_gga(one(T83), T84, X125) → U60_gga(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U60_gga(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U61_gga(T83, T84, X125, addc29_in_gga(T84, T87, X125))
addc29_in_gga(b, T107, zero(T107)) → U62_gga(T107, binaryZc54_in_g(T107))
binaryZc54_in_g(zero(T113)) → U65_g(T113, binaryZc54_in_g(T113))
binaryZc54_in_g(one(T117)) → U66_g(T117, binaryc60_in_g(T117))
binaryc60_in_g(b) → binaryc60_out_g(b)
binaryc60_in_g(zero(T122)) → U67_g(T122, binaryZc54_in_g(T122))
U67_g(T122, binaryZc54_out_g(T122)) → binaryc60_out_g(zero(T122))
binaryc60_in_g(one(T126)) → U68_g(T126, binaryc60_in_g(T126))
U68_g(T126, binaryc60_out_g(T126)) → binaryc60_out_g(one(T126))
U66_g(T117, binaryc60_out_g(T117)) → binaryZc54_out_g(one(T117))
U65_g(T113, binaryZc54_out_g(T113)) → binaryZc54_out_g(zero(T113))
U62_gga(T107, binaryZc54_out_g(T107)) → addc29_out_gga(b, T107, zero(T107))
addc29_in_gga(zero(T156), T157, zero(T159)) → U63_gga(T156, T157, T159, addzc79_in_gga(T156, T157, T159))
addzc79_in_gga(zero(T175), zero(T176), zero(T178)) → U69_gga(T175, T176, T178, addzc79_in_gga(T175, T176, T178))
addzc79_in_gga(zero(one(T203)), one(b), one(one(T203))) → U70_gga(T203, binaryc60_in_g(T203))
U70_gga(T203, binaryc60_out_g(T203)) → addzc79_out_gga(zero(one(T203)), one(b), one(one(T203)))
addzc79_in_gga(zero(zero(T208)), one(b), one(zero(T208))) → U71_gga(T208, binaryZc54_in_g(T208))
U71_gga(T208, binaryZc54_out_g(T208)) → addzc79_out_gga(zero(zero(T208)), one(b), one(zero(T208)))
addzc79_in_gga(zero(T220), one(T221), one(T223)) → U72_gga(T220, T221, T223, addzc79_in_gga(T220, T221, T223))
addzc79_in_gga(one(T239), zero(T240), one(T242)) → U73_gga(T239, T240, T242, addyc102_in_gga(T239, T240, T242))
addyc102_in_gga(b, one(T248), one(T248)) → U90_gga(T248, binaryc60_in_g(T248))
U90_gga(T248, binaryc60_out_g(T248)) → addyc102_out_gga(b, one(T248), one(T248))
addyc102_in_gga(b, zero(T253), zero(T253)) → U91_gga(T253, binaryZc54_in_g(T253))
U91_gga(T253, binaryZc54_out_g(T253)) → addyc102_out_gga(b, zero(T253), zero(T253))
addyc102_in_gga(T265, T266, T268) → U92_gga(T265, T266, T268, addzc79_in_gga(T265, T266, T268))
addzc79_in_gga(one(T278), one(T279), zero(T281)) → U74_gga(T278, T279, T281, addcc114_in_gga(T278, T279, T281))
addcc114_in_gga(b, b, one(b)) → addcc114_out_gga(b, b, one(b))
addcc114_in_gga(T290, b, T292) → U87_gga(T290, T292, succZc124_in_ga(T290, T292))
succZc124_in_ga(zero(T298), one(T298)) → U77_ga(T298, binaryZc54_in_g(T298))
U77_ga(T298, binaryZc54_out_g(T298)) → succZc124_out_ga(zero(T298), one(T298))
succZc124_in_ga(one(T304), zero(T306)) → U78_ga(T304, T306, succc131_in_ga(T304, T306))
succc131_in_ga(b, one(b)) → succc131_out_ga(b, one(b))
succc131_in_ga(zero(T311), one(T311)) → U75_ga(T311, binaryZc54_in_g(T311))
U75_ga(T311, binaryZc54_out_g(T311)) → succc131_out_ga(zero(T311), one(T311))
succc131_in_ga(one(T317), zero(T319)) → U76_ga(T317, T319, succc131_in_ga(T317, T319))
U76_ga(T317, T319, succc131_out_ga(T317, T319)) → succc131_out_ga(one(T317), zero(T319))
U78_ga(T304, T306, succc131_out_ga(T304, T306)) → succZc124_out_ga(one(T304), zero(T306))
U87_gga(T290, T292, succZc124_out_ga(T290, T292)) → addcc114_out_gga(T290, b, T292)
addcc114_in_gga(b, T328, T330) → U88_gga(T328, T330, succZc124_in_ga(T328, T330))
U88_gga(T328, T330, succZc124_out_ga(T328, T330)) → addcc114_out_gga(b, T328, T330)
addcc114_in_gga(T342, T343, T345) → U89_gga(T342, T343, T345, addCc149_in_gga(T342, T343, T345))
addCc149_in_gga(zero(T361), zero(T362), one(T364)) → U79_gga(T361, T362, T364, addzc79_in_gga(T361, T362, T364))
U79_gga(T361, T362, T364, addzc79_out_gga(T361, T362, T364)) → addCc149_out_gga(zero(T361), zero(T362), one(T364))
addCc149_in_gga(zero(zero(T389)), one(b), zero(one(T389))) → U80_gga(T389, binaryZc54_in_g(T389))
U80_gga(T389, binaryZc54_out_g(T389)) → addCc149_out_gga(zero(zero(T389)), one(b), zero(one(T389)))
addCc149_in_gga(zero(one(T399)), one(b), zero(zero(T401))) → U81_gga(T399, T401, succc131_in_ga(T399, T401))
U81_gga(T399, T401, succc131_out_ga(T399, T401)) → addCc149_out_gga(zero(one(T399)), one(b), zero(zero(T401)))
addCc149_in_gga(zero(T412), one(T413), zero(T415)) → U82_gga(T412, T413, T415, addCc149_in_gga(T412, T413, T415))
addCc149_in_gga(one(b), zero(zero(T440)), zero(one(T440))) → U83_gga(T440, binaryZc54_in_g(T440))
U83_gga(T440, binaryZc54_out_g(T440)) → addCc149_out_gga(one(b), zero(zero(T440)), zero(one(T440)))
addCc149_in_gga(one(b), zero(one(T450)), zero(zero(T452))) → U84_gga(T450, T452, succc131_in_ga(T450, T452))
U84_gga(T450, T452, succc131_out_ga(T450, T452)) → addCc149_out_gga(one(b), zero(one(T450)), zero(zero(T452)))
addCc149_in_gga(one(T463), zero(T464), zero(T466)) → U85_gga(T463, T464, T466, addCc149_in_gga(T463, T464, T466))
addCc149_in_gga(one(T476), one(T477), one(T479)) → U86_gga(T476, T477, T479, addcc114_in_gga(T476, T477, T479))
U86_gga(T476, T477, T479, addcc114_out_gga(T476, T477, T479)) → addCc149_out_gga(one(T476), one(T477), one(T479))
U85_gga(T463, T464, T466, addCc149_out_gga(T463, T464, T466)) → addCc149_out_gga(one(T463), zero(T464), zero(T466))
U82_gga(T412, T413, T415, addCc149_out_gga(T412, T413, T415)) → addCc149_out_gga(zero(T412), one(T413), zero(T415))
U89_gga(T342, T343, T345, addCc149_out_gga(T342, T343, T345)) → addcc114_out_gga(T342, T343, T345)
U74_gga(T278, T279, T281, addcc114_out_gga(T278, T279, T281)) → addzc79_out_gga(one(T278), one(T279), zero(T281))
U92_gga(T265, T266, T268, addzc79_out_gga(T265, T266, T268)) → addyc102_out_gga(T265, T266, T268)
U73_gga(T239, T240, T242, addyc102_out_gga(T239, T240, T242)) → addzc79_out_gga(one(T239), zero(T240), one(T242))
U72_gga(T220, T221, T223, addzc79_out_gga(T220, T221, T223)) → addzc79_out_gga(zero(T220), one(T221), one(T223))
U69_gga(T175, T176, T178, addzc79_out_gga(T175, T176, T178)) → addzc79_out_gga(zero(T175), zero(T176), zero(T178))
U63_gga(T156, T157, T159, addzc79_out_gga(T156, T157, T159)) → addc29_out_gga(zero(T156), T157, zero(T159))
addc29_in_gga(one(T493), T494, one(T496)) → U64_gga(T493, T494, T496, addyc102_in_gga(T493, T494, T496))
U64_gga(T493, T494, T496, addyc102_out_gga(T493, T494, T496)) → addc29_out_gga(one(T493), T494, one(T496))
U61_gga(T83, T84, X125, addc29_out_gga(T84, T87, X125)) → timesc28_out_gga(one(T83), T84, X125)
U59_gga(T75, T76, X106, timesc28_out_gga(T75, T76, X106)) → timesc28_out_gga(zero(T75), T76, zero(X106))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timesc28_in_gga(x1, x2, x3) = timesc28_in_gga(x1, x2)
b = b
timesc28_out_gga(x1, x2, x3) = timesc28_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addc29_in_gga(x1, x2, x3) = addc29_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZc54_in_g(x1) = binaryZc54_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binaryc60_in_g(x1) = binaryc60_in_g(x1)
binaryc60_out_g(x1) = binaryc60_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZc54_out_g(x1) = binaryZc54_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addc29_out_gga(x1, x2, x3) = addc29_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzc79_in_gga(x1, x2, x3) = addzc79_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzc79_out_gga(x1, x2, x3) = addzc79_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addyc102_in_gga(x1, x2, x3) = addyc102_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addyc102_out_gga(x1, x2, x3) = addyc102_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addcc114_in_gga(x1, x2, x3) = addcc114_in_gga(x1, x2)
addcc114_out_gga(x1, x2, x3) = addcc114_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZc124_in_ga(x1, x2) = succZc124_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZc124_out_ga(x1, x2) = succZc124_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succc131_in_ga(x1, x2) = succc131_in_ga(x1)
succc131_out_ga(x1, x2) = succc131_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCc149_in_gga(x1, x2, x3) = addCc149_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCc149_out_gga(x1, x2, x3) = addCc149_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
SUCC131_IN_GA(x1, x2) = SUCC131_IN_GA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

SUCC131_IN_GA(one(T317), zero(T319)) → SUCC131_IN_GA(T317, T319)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

SUCC131_IN_GA(one(T317)) → SUCC131_IN_GA(T317)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

SUCC131_IN_GA(one(T317)) → SUCC131_IN_GA(T317)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

ADDZ79_IN_GGA(zero(T220), one(T221), one(T223)) → ADDZ79_IN_GGA(T220, T221, T223)
ADDZ79_IN_GGA(zero(T175), zero(T176), zero(T178)) → ADDZ79_IN_GGA(T175, T176, T178)
ADDZ79_IN_GGA(one(T239), zero(T240), one(T242)) → ADDY102_IN_GGA(T239, T240, T242)
ADDY102_IN_GGA(T265, T266, T268) → ADDZ79_IN_GGA(T265, T266, T268)
ADDZ79_IN_GGA(one(T278), one(T279), zero(T281)) → ADDC114_IN_GGA(T278, T279, T281)
ADDC114_IN_GGA(T342, T343, T345) → ADDC149_IN_GGA(T342, T343, T345)
ADDC149_IN_GGA(zero(T361), zero(T362), one(T364)) → ADDZ79_IN_GGA(T361, T362, T364)
ADDC149_IN_GGA(zero(T412), one(T413), zero(T415)) → ADDC149_IN_GGA(T412, T413, T415)
ADDC149_IN_GGA(one(T463), zero(T464), zero(T466)) → ADDC149_IN_GGA(T463, T464, T466)
ADDC149_IN_GGA(one(T476), one(T477), one(T479)) → ADDC114_IN_GGA(T476, T477, T479)

The TRS R consists of the following rules:

timesc28_in_gga(one(b), T66, T66) → timesc28_out_gga(one(b), T66, T66)
timesc28_in_gga(zero(T75), T76, zero(X106)) → U59_gga(T75, T76, X106, timesc28_in_gga(T75, T76, X106))
timesc28_in_gga(one(T83), T84, X125) → U60_gga(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U60_gga(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U61_gga(T83, T84, X125, addc29_in_gga(T84, T87, X125))
addc29_in_gga(b, T107, zero(T107)) → U62_gga(T107, binaryZc54_in_g(T107))
binaryZc54_in_g(zero(T113)) → U65_g(T113, binaryZc54_in_g(T113))
binaryZc54_in_g(one(T117)) → U66_g(T117, binaryc60_in_g(T117))
binaryc60_in_g(b) → binaryc60_out_g(b)
binaryc60_in_g(zero(T122)) → U67_g(T122, binaryZc54_in_g(T122))
U67_g(T122, binaryZc54_out_g(T122)) → binaryc60_out_g(zero(T122))
binaryc60_in_g(one(T126)) → U68_g(T126, binaryc60_in_g(T126))
U68_g(T126, binaryc60_out_g(T126)) → binaryc60_out_g(one(T126))
U66_g(T117, binaryc60_out_g(T117)) → binaryZc54_out_g(one(T117))
U65_g(T113, binaryZc54_out_g(T113)) → binaryZc54_out_g(zero(T113))
U62_gga(T107, binaryZc54_out_g(T107)) → addc29_out_gga(b, T107, zero(T107))
addc29_in_gga(zero(T156), T157, zero(T159)) → U63_gga(T156, T157, T159, addzc79_in_gga(T156, T157, T159))
addzc79_in_gga(zero(T175), zero(T176), zero(T178)) → U69_gga(T175, T176, T178, addzc79_in_gga(T175, T176, T178))
addzc79_in_gga(zero(one(T203)), one(b), one(one(T203))) → U70_gga(T203, binaryc60_in_g(T203))
U70_gga(T203, binaryc60_out_g(T203)) → addzc79_out_gga(zero(one(T203)), one(b), one(one(T203)))
addzc79_in_gga(zero(zero(T208)), one(b), one(zero(T208))) → U71_gga(T208, binaryZc54_in_g(T208))
U71_gga(T208, binaryZc54_out_g(T208)) → addzc79_out_gga(zero(zero(T208)), one(b), one(zero(T208)))
addzc79_in_gga(zero(T220), one(T221), one(T223)) → U72_gga(T220, T221, T223, addzc79_in_gga(T220, T221, T223))
addzc79_in_gga(one(T239), zero(T240), one(T242)) → U73_gga(T239, T240, T242, addyc102_in_gga(T239, T240, T242))
addyc102_in_gga(b, one(T248), one(T248)) → U90_gga(T248, binaryc60_in_g(T248))
U90_gga(T248, binaryc60_out_g(T248)) → addyc102_out_gga(b, one(T248), one(T248))
addyc102_in_gga(b, zero(T253), zero(T253)) → U91_gga(T253, binaryZc54_in_g(T253))
U91_gga(T253, binaryZc54_out_g(T253)) → addyc102_out_gga(b, zero(T253), zero(T253))
addyc102_in_gga(T265, T266, T268) → U92_gga(T265, T266, T268, addzc79_in_gga(T265, T266, T268))
addzc79_in_gga(one(T278), one(T279), zero(T281)) → U74_gga(T278, T279, T281, addcc114_in_gga(T278, T279, T281))
addcc114_in_gga(b, b, one(b)) → addcc114_out_gga(b, b, one(b))
addcc114_in_gga(T290, b, T292) → U87_gga(T290, T292, succZc124_in_ga(T290, T292))
succZc124_in_ga(zero(T298), one(T298)) → U77_ga(T298, binaryZc54_in_g(T298))
U77_ga(T298, binaryZc54_out_g(T298)) → succZc124_out_ga(zero(T298), one(T298))
succZc124_in_ga(one(T304), zero(T306)) → U78_ga(T304, T306, succc131_in_ga(T304, T306))
succc131_in_ga(b, one(b)) → succc131_out_ga(b, one(b))
succc131_in_ga(zero(T311), one(T311)) → U75_ga(T311, binaryZc54_in_g(T311))
U75_ga(T311, binaryZc54_out_g(T311)) → succc131_out_ga(zero(T311), one(T311))
succc131_in_ga(one(T317), zero(T319)) → U76_ga(T317, T319, succc131_in_ga(T317, T319))
U76_ga(T317, T319, succc131_out_ga(T317, T319)) → succc131_out_ga(one(T317), zero(T319))
U78_ga(T304, T306, succc131_out_ga(T304, T306)) → succZc124_out_ga(one(T304), zero(T306))
U87_gga(T290, T292, succZc124_out_ga(T290, T292)) → addcc114_out_gga(T290, b, T292)
addcc114_in_gga(b, T328, T330) → U88_gga(T328, T330, succZc124_in_ga(T328, T330))
U88_gga(T328, T330, succZc124_out_ga(T328, T330)) → addcc114_out_gga(b, T328, T330)
addcc114_in_gga(T342, T343, T345) → U89_gga(T342, T343, T345, addCc149_in_gga(T342, T343, T345))
addCc149_in_gga(zero(T361), zero(T362), one(T364)) → U79_gga(T361, T362, T364, addzc79_in_gga(T361, T362, T364))
U79_gga(T361, T362, T364, addzc79_out_gga(T361, T362, T364)) → addCc149_out_gga(zero(T361), zero(T362), one(T364))
addCc149_in_gga(zero(zero(T389)), one(b), zero(one(T389))) → U80_gga(T389, binaryZc54_in_g(T389))
U80_gga(T389, binaryZc54_out_g(T389)) → addCc149_out_gga(zero(zero(T389)), one(b), zero(one(T389)))
addCc149_in_gga(zero(one(T399)), one(b), zero(zero(T401))) → U81_gga(T399, T401, succc131_in_ga(T399, T401))
U81_gga(T399, T401, succc131_out_ga(T399, T401)) → addCc149_out_gga(zero(one(T399)), one(b), zero(zero(T401)))
addCc149_in_gga(zero(T412), one(T413), zero(T415)) → U82_gga(T412, T413, T415, addCc149_in_gga(T412, T413, T415))
addCc149_in_gga(one(b), zero(zero(T440)), zero(one(T440))) → U83_gga(T440, binaryZc54_in_g(T440))
U83_gga(T440, binaryZc54_out_g(T440)) → addCc149_out_gga(one(b), zero(zero(T440)), zero(one(T440)))
addCc149_in_gga(one(b), zero(one(T450)), zero(zero(T452))) → U84_gga(T450, T452, succc131_in_ga(T450, T452))
U84_gga(T450, T452, succc131_out_ga(T450, T452)) → addCc149_out_gga(one(b), zero(one(T450)), zero(zero(T452)))
addCc149_in_gga(one(T463), zero(T464), zero(T466)) → U85_gga(T463, T464, T466, addCc149_in_gga(T463, T464, T466))
addCc149_in_gga(one(T476), one(T477), one(T479)) → U86_gga(T476, T477, T479, addcc114_in_gga(T476, T477, T479))
U86_gga(T476, T477, T479, addcc114_out_gga(T476, T477, T479)) → addCc149_out_gga(one(T476), one(T477), one(T479))
U85_gga(T463, T464, T466, addCc149_out_gga(T463, T464, T466)) → addCc149_out_gga(one(T463), zero(T464), zero(T466))
U82_gga(T412, T413, T415, addCc149_out_gga(T412, T413, T415)) → addCc149_out_gga(zero(T412), one(T413), zero(T415))
U89_gga(T342, T343, T345, addCc149_out_gga(T342, T343, T345)) → addcc114_out_gga(T342, T343, T345)
U74_gga(T278, T279, T281, addcc114_out_gga(T278, T279, T281)) → addzc79_out_gga(one(T278), one(T279), zero(T281))
U92_gga(T265, T266, T268, addzc79_out_gga(T265, T266, T268)) → addyc102_out_gga(T265, T266, T268)
U73_gga(T239, T240, T242, addyc102_out_gga(T239, T240, T242)) → addzc79_out_gga(one(T239), zero(T240), one(T242))
U72_gga(T220, T221, T223, addzc79_out_gga(T220, T221, T223)) → addzc79_out_gga(zero(T220), one(T221), one(T223))
U69_gga(T175, T176, T178, addzc79_out_gga(T175, T176, T178)) → addzc79_out_gga(zero(T175), zero(T176), zero(T178))
U63_gga(T156, T157, T159, addzc79_out_gga(T156, T157, T159)) → addc29_out_gga(zero(T156), T157, zero(T159))
addc29_in_gga(one(T493), T494, one(T496)) → U64_gga(T493, T494, T496, addyc102_in_gga(T493, T494, T496))
U64_gga(T493, T494, T496, addyc102_out_gga(T493, T494, T496)) → addc29_out_gga(one(T493), T494, one(T496))
U61_gga(T83, T84, X125, addc29_out_gga(T84, T87, X125)) → timesc28_out_gga(one(T83), T84, X125)
U59_gga(T75, T76, X106, timesc28_out_gga(T75, T76, X106)) → timesc28_out_gga(zero(T75), T76, zero(X106))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timesc28_in_gga(x1, x2, x3) = timesc28_in_gga(x1, x2)
b = b
timesc28_out_gga(x1, x2, x3) = timesc28_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addc29_in_gga(x1, x2, x3) = addc29_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZc54_in_g(x1) = binaryZc54_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binaryc60_in_g(x1) = binaryc60_in_g(x1)
binaryc60_out_g(x1) = binaryc60_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZc54_out_g(x1) = binaryZc54_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addc29_out_gga(x1, x2, x3) = addc29_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzc79_in_gga(x1, x2, x3) = addzc79_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzc79_out_gga(x1, x2, x3) = addzc79_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addyc102_in_gga(x1, x2, x3) = addyc102_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addyc102_out_gga(x1, x2, x3) = addyc102_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addcc114_in_gga(x1, x2, x3) = addcc114_in_gga(x1, x2)
addcc114_out_gga(x1, x2, x3) = addcc114_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZc124_in_ga(x1, x2) = succZc124_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZc124_out_ga(x1, x2) = succZc124_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succc131_in_ga(x1, x2) = succc131_in_ga(x1)
succc131_out_ga(x1, x2) = succc131_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCc149_in_gga(x1, x2, x3) = addCc149_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCc149_out_gga(x1, x2, x3) = addCc149_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
ADDZ79_IN_GGA(x1, x2, x3) = ADDZ79_IN_GGA(x1, x2)
ADDY102_IN_GGA(x1, x2, x3) = ADDY102_IN_GGA(x1, x2)
ADDC114_IN_GGA(x1, x2, x3) = ADDC114_IN_GGA(x1, x2)
ADDC149_IN_GGA(x1, x2, x3) = ADDC149_IN_GGA(x1, x2)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

ADDZ79_IN_GGA(zero(T220), one(T221), one(T223)) → ADDZ79_IN_GGA(T220, T221, T223)
ADDZ79_IN_GGA(zero(T175), zero(T176), zero(T178)) → ADDZ79_IN_GGA(T175, T176, T178)
ADDZ79_IN_GGA(one(T239), zero(T240), one(T242)) → ADDY102_IN_GGA(T239, T240, T242)
ADDY102_IN_GGA(T265, T266, T268) → ADDZ79_IN_GGA(T265, T266, T268)
ADDZ79_IN_GGA(one(T278), one(T279), zero(T281)) → ADDC114_IN_GGA(T278, T279, T281)
ADDC114_IN_GGA(T342, T343, T345) → ADDC149_IN_GGA(T342, T343, T345)
ADDC149_IN_GGA(zero(T361), zero(T362), one(T364)) → ADDZ79_IN_GGA(T361, T362, T364)
ADDC149_IN_GGA(zero(T412), one(T413), zero(T415)) → ADDC149_IN_GGA(T412, T413, T415)
ADDC149_IN_GGA(one(T463), zero(T464), zero(T466)) → ADDC149_IN_GGA(T463, T464, T466)
ADDC149_IN_GGA(one(T476), one(T477), one(T479)) → ADDC114_IN_GGA(T476, T477, T479)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
ADDZ79_IN_GGA(x1, x2, x3) = ADDZ79_IN_GGA(x1, x2)
ADDY102_IN_GGA(x1, x2, x3) = ADDY102_IN_GGA(x1, x2)
ADDC114_IN_GGA(x1, x2, x3) = ADDC114_IN_GGA(x1, x2)
ADDC149_IN_GGA(x1, x2, x3) = ADDC149_IN_GGA(x1, x2)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

ADDZ79_IN_GGA(zero(T220), one(T221)) → ADDZ79_IN_GGA(T220, T221)
ADDZ79_IN_GGA(zero(T175), zero(T176)) → ADDZ79_IN_GGA(T175, T176)
ADDZ79_IN_GGA(one(T239), zero(T240)) → ADDY102_IN_GGA(T239, T240)
ADDY102_IN_GGA(T265, T266) → ADDZ79_IN_GGA(T265, T266)
ADDZ79_IN_GGA(one(T278), one(T279)) → ADDC114_IN_GGA(T278, T279)
ADDC114_IN_GGA(T342, T343) → ADDC149_IN_GGA(T342, T343)
ADDC149_IN_GGA(zero(T361), zero(T362)) → ADDZ79_IN_GGA(T361, T362)
ADDC149_IN_GGA(zero(T412), one(T413)) → ADDC149_IN_GGA(T412, T413)
ADDC149_IN_GGA(one(T463), zero(T464)) → ADDC149_IN_GGA(T463, T464)
ADDC149_IN_GGA(one(T476), one(T477)) → ADDC114_IN_GGA(T476, T477)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

ADDY102_IN_GGA(T265, T266) → ADDZ79_IN_GGA(T265, T266)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDC149_IN_GGA(zero(T361), zero(T362)) → ADDZ79_IN_GGA(T361, T362)
The graph contains the following edges 1 > 1, 2 > 2
ADDZ79_IN_GGA(one(T239), zero(T240)) → ADDY102_IN_GGA(T239, T240)
The graph contains the following edges 1 > 1, 2 > 2
ADDZ79_IN_GGA(one(T278), one(T279)) → ADDC114_IN_GGA(T278, T279)
The graph contains the following edges 1 > 1, 2 > 2
ADDC114_IN_GGA(T342, T343) → ADDC149_IN_GGA(T342, T343)
The graph contains the following edges 1 >= 1, 2 >= 2
ADDC149_IN_GGA(one(T476), one(T477)) → ADDC114_IN_GGA(T476, T477)
The graph contains the following edges 1 > 1, 2 > 2
ADDZ79_IN_GGA(zero(T220), one(T221)) → ADDZ79_IN_GGA(T220, T221)
The graph contains the following edges 1 > 1, 2 > 2
ADDZ79_IN_GGA(zero(T175), zero(T176)) → ADDZ79_IN_GGA(T175, T176)
The graph contains the following edges 1 > 1, 2 > 2
ADDC149_IN_GGA(zero(T412), one(T413)) → ADDC149_IN_GGA(T412, T413)
The graph contains the following edges 1 > 1, 2 > 2
ADDC149_IN_GGA(one(T463), zero(T464)) → ADDC149_IN_GGA(T463, T464)
The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

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

TIMES28_IN_GGA(one(T83), T84, X125) → TIMES28_IN_GGA(T83, T84, X124)
TIMES28_IN_GGA(zero(T75), T76, zero(X106)) → TIMES28_IN_GGA(T75, T76, X106)

The TRS R consists of the following rules:

timesc28_in_gga(one(b), T66, T66) → timesc28_out_gga(one(b), T66, T66)
timesc28_in_gga(zero(T75), T76, zero(X106)) → U59_gga(T75, T76, X106, timesc28_in_gga(T75, T76, X106))
timesc28_in_gga(one(T83), T84, X125) → U60_gga(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U60_gga(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U61_gga(T83, T84, X125, addc29_in_gga(T84, T87, X125))
addc29_in_gga(b, T107, zero(T107)) → U62_gga(T107, binaryZc54_in_g(T107))
binaryZc54_in_g(zero(T113)) → U65_g(T113, binaryZc54_in_g(T113))
binaryZc54_in_g(one(T117)) → U66_g(T117, binaryc60_in_g(T117))
binaryc60_in_g(b) → binaryc60_out_g(b)
binaryc60_in_g(zero(T122)) → U67_g(T122, binaryZc54_in_g(T122))
U67_g(T122, binaryZc54_out_g(T122)) → binaryc60_out_g(zero(T122))
binaryc60_in_g(one(T126)) → U68_g(T126, binaryc60_in_g(T126))
U68_g(T126, binaryc60_out_g(T126)) → binaryc60_out_g(one(T126))
U66_g(T117, binaryc60_out_g(T117)) → binaryZc54_out_g(one(T117))
U65_g(T113, binaryZc54_out_g(T113)) → binaryZc54_out_g(zero(T113))
U62_gga(T107, binaryZc54_out_g(T107)) → addc29_out_gga(b, T107, zero(T107))
addc29_in_gga(zero(T156), T157, zero(T159)) → U63_gga(T156, T157, T159, addzc79_in_gga(T156, T157, T159))
addzc79_in_gga(zero(T175), zero(T176), zero(T178)) → U69_gga(T175, T176, T178, addzc79_in_gga(T175, T176, T178))
addzc79_in_gga(zero(one(T203)), one(b), one(one(T203))) → U70_gga(T203, binaryc60_in_g(T203))
U70_gga(T203, binaryc60_out_g(T203)) → addzc79_out_gga(zero(one(T203)), one(b), one(one(T203)))
addzc79_in_gga(zero(zero(T208)), one(b), one(zero(T208))) → U71_gga(T208, binaryZc54_in_g(T208))
U71_gga(T208, binaryZc54_out_g(T208)) → addzc79_out_gga(zero(zero(T208)), one(b), one(zero(T208)))
addzc79_in_gga(zero(T220), one(T221), one(T223)) → U72_gga(T220, T221, T223, addzc79_in_gga(T220, T221, T223))
addzc79_in_gga(one(T239), zero(T240), one(T242)) → U73_gga(T239, T240, T242, addyc102_in_gga(T239, T240, T242))
addyc102_in_gga(b, one(T248), one(T248)) → U90_gga(T248, binaryc60_in_g(T248))
U90_gga(T248, binaryc60_out_g(T248)) → addyc102_out_gga(b, one(T248), one(T248))
addyc102_in_gga(b, zero(T253), zero(T253)) → U91_gga(T253, binaryZc54_in_g(T253))
U91_gga(T253, binaryZc54_out_g(T253)) → addyc102_out_gga(b, zero(T253), zero(T253))
addyc102_in_gga(T265, T266, T268) → U92_gga(T265, T266, T268, addzc79_in_gga(T265, T266, T268))
addzc79_in_gga(one(T278), one(T279), zero(T281)) → U74_gga(T278, T279, T281, addcc114_in_gga(T278, T279, T281))
addcc114_in_gga(b, b, one(b)) → addcc114_out_gga(b, b, one(b))
addcc114_in_gga(T290, b, T292) → U87_gga(T290, T292, succZc124_in_ga(T290, T292))
succZc124_in_ga(zero(T298), one(T298)) → U77_ga(T298, binaryZc54_in_g(T298))
U77_ga(T298, binaryZc54_out_g(T298)) → succZc124_out_ga(zero(T298), one(T298))
succZc124_in_ga(one(T304), zero(T306)) → U78_ga(T304, T306, succc131_in_ga(T304, T306))
succc131_in_ga(b, one(b)) → succc131_out_ga(b, one(b))
succc131_in_ga(zero(T311), one(T311)) → U75_ga(T311, binaryZc54_in_g(T311))
U75_ga(T311, binaryZc54_out_g(T311)) → succc131_out_ga(zero(T311), one(T311))
succc131_in_ga(one(T317), zero(T319)) → U76_ga(T317, T319, succc131_in_ga(T317, T319))
U76_ga(T317, T319, succc131_out_ga(T317, T319)) → succc131_out_ga(one(T317), zero(T319))
U78_ga(T304, T306, succc131_out_ga(T304, T306)) → succZc124_out_ga(one(T304), zero(T306))
U87_gga(T290, T292, succZc124_out_ga(T290, T292)) → addcc114_out_gga(T290, b, T292)
addcc114_in_gga(b, T328, T330) → U88_gga(T328, T330, succZc124_in_ga(T328, T330))
U88_gga(T328, T330, succZc124_out_ga(T328, T330)) → addcc114_out_gga(b, T328, T330)
addcc114_in_gga(T342, T343, T345) → U89_gga(T342, T343, T345, addCc149_in_gga(T342, T343, T345))
addCc149_in_gga(zero(T361), zero(T362), one(T364)) → U79_gga(T361, T362, T364, addzc79_in_gga(T361, T362, T364))
U79_gga(T361, T362, T364, addzc79_out_gga(T361, T362, T364)) → addCc149_out_gga(zero(T361), zero(T362), one(T364))
addCc149_in_gga(zero(zero(T389)), one(b), zero(one(T389))) → U80_gga(T389, binaryZc54_in_g(T389))
U80_gga(T389, binaryZc54_out_g(T389)) → addCc149_out_gga(zero(zero(T389)), one(b), zero(one(T389)))
addCc149_in_gga(zero(one(T399)), one(b), zero(zero(T401))) → U81_gga(T399, T401, succc131_in_ga(T399, T401))
U81_gga(T399, T401, succc131_out_ga(T399, T401)) → addCc149_out_gga(zero(one(T399)), one(b), zero(zero(T401)))
addCc149_in_gga(zero(T412), one(T413), zero(T415)) → U82_gga(T412, T413, T415, addCc149_in_gga(T412, T413, T415))
addCc149_in_gga(one(b), zero(zero(T440)), zero(one(T440))) → U83_gga(T440, binaryZc54_in_g(T440))
U83_gga(T440, binaryZc54_out_g(T440)) → addCc149_out_gga(one(b), zero(zero(T440)), zero(one(T440)))
addCc149_in_gga(one(b), zero(one(T450)), zero(zero(T452))) → U84_gga(T450, T452, succc131_in_ga(T450, T452))
U84_gga(T450, T452, succc131_out_ga(T450, T452)) → addCc149_out_gga(one(b), zero(one(T450)), zero(zero(T452)))
addCc149_in_gga(one(T463), zero(T464), zero(T466)) → U85_gga(T463, T464, T466, addCc149_in_gga(T463, T464, T466))
addCc149_in_gga(one(T476), one(T477), one(T479)) → U86_gga(T476, T477, T479, addcc114_in_gga(T476, T477, T479))
U86_gga(T476, T477, T479, addcc114_out_gga(T476, T477, T479)) → addCc149_out_gga(one(T476), one(T477), one(T479))
U85_gga(T463, T464, T466, addCc149_out_gga(T463, T464, T466)) → addCc149_out_gga(one(T463), zero(T464), zero(T466))
U82_gga(T412, T413, T415, addCc149_out_gga(T412, T413, T415)) → addCc149_out_gga(zero(T412), one(T413), zero(T415))
U89_gga(T342, T343, T345, addCc149_out_gga(T342, T343, T345)) → addcc114_out_gga(T342, T343, T345)
U74_gga(T278, T279, T281, addcc114_out_gga(T278, T279, T281)) → addzc79_out_gga(one(T278), one(T279), zero(T281))
U92_gga(T265, T266, T268, addzc79_out_gga(T265, T266, T268)) → addyc102_out_gga(T265, T266, T268)
U73_gga(T239, T240, T242, addyc102_out_gga(T239, T240, T242)) → addzc79_out_gga(one(T239), zero(T240), one(T242))
U72_gga(T220, T221, T223, addzc79_out_gga(T220, T221, T223)) → addzc79_out_gga(zero(T220), one(T221), one(T223))
U69_gga(T175, T176, T178, addzc79_out_gga(T175, T176, T178)) → addzc79_out_gga(zero(T175), zero(T176), zero(T178))
U63_gga(T156, T157, T159, addzc79_out_gga(T156, T157, T159)) → addc29_out_gga(zero(T156), T157, zero(T159))
addc29_in_gga(one(T493), T494, one(T496)) → U64_gga(T493, T494, T496, addyc102_in_gga(T493, T494, T496))
U64_gga(T493, T494, T496, addyc102_out_gga(T493, T494, T496)) → addc29_out_gga(one(T493), T494, one(T496))
U61_gga(T83, T84, X125, addc29_out_gga(T84, T87, X125)) → timesc28_out_gga(one(T83), T84, X125)
U59_gga(T75, T76, X106, timesc28_out_gga(T75, T76, X106)) → timesc28_out_gga(zero(T75), T76, zero(X106))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timesc28_in_gga(x1, x2, x3) = timesc28_in_gga(x1, x2)
b = b
timesc28_out_gga(x1, x2, x3) = timesc28_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addc29_in_gga(x1, x2, x3) = addc29_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZc54_in_g(x1) = binaryZc54_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binaryc60_in_g(x1) = binaryc60_in_g(x1)
binaryc60_out_g(x1) = binaryc60_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZc54_out_g(x1) = binaryZc54_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addc29_out_gga(x1, x2, x3) = addc29_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzc79_in_gga(x1, x2, x3) = addzc79_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzc79_out_gga(x1, x2, x3) = addzc79_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addyc102_in_gga(x1, x2, x3) = addyc102_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addyc102_out_gga(x1, x2, x3) = addyc102_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addcc114_in_gga(x1, x2, x3) = addcc114_in_gga(x1, x2)
addcc114_out_gga(x1, x2, x3) = addcc114_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZc124_in_ga(x1, x2) = succZc124_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZc124_out_ga(x1, x2) = succZc124_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succc131_in_ga(x1, x2) = succc131_in_ga(x1)
succc131_out_ga(x1, x2) = succc131_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCc149_in_gga(x1, x2, x3) = addCc149_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCc149_out_gga(x1, x2, x3) = addCc149_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
TIMES28_IN_GGA(x1, x2, x3) = TIMES28_IN_GGA(x1, x2)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

TIMES28_IN_GGA(one(T83), T84, X125) → TIMES28_IN_GGA(T83, T84, X124)
TIMES28_IN_GGA(zero(T75), T76, zero(X106)) → TIMES28_IN_GGA(T75, T76, X106)

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

TIMES28_IN_GGA(one(T83), T84) → TIMES28_IN_GGA(T83, T84)
TIMES28_IN_GGA(zero(T75), T76) → TIMES28_IN_GGA(T75, T76)

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

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

TIMES28_IN_GGA(one(T83), T84) → TIMES28_IN_GGA(T83, T84)
The graph contains the following edges 1 > 1, 2 >= 2
TIMES28_IN_GGA(zero(T75), T76) → TIMES28_IN_GGA(T75, T76)
The graph contains the following edges 1 > 1, 2 >= 2

(34) YES

(35) Obligation:

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

TIMES1_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → TIMES1_IN_GGA(T35, T36, T38)

The TRS R consists of the following rules:

timesc28_in_gga(one(b), T66, T66) → timesc28_out_gga(one(b), T66, T66)
timesc28_in_gga(zero(T75), T76, zero(X106)) → U59_gga(T75, T76, X106, timesc28_in_gga(T75, T76, X106))
timesc28_in_gga(one(T83), T84, X125) → U60_gga(T83, T84, X125, timesc28_in_gga(T83, T84, T87))
U60_gga(T83, T84, X125, timesc28_out_gga(T83, T84, T87)) → U61_gga(T83, T84, X125, addc29_in_gga(T84, T87, X125))
addc29_in_gga(b, T107, zero(T107)) → U62_gga(T107, binaryZc54_in_g(T107))
binaryZc54_in_g(zero(T113)) → U65_g(T113, binaryZc54_in_g(T113))
binaryZc54_in_g(one(T117)) → U66_g(T117, binaryc60_in_g(T117))
binaryc60_in_g(b) → binaryc60_out_g(b)
binaryc60_in_g(zero(T122)) → U67_g(T122, binaryZc54_in_g(T122))
U67_g(T122, binaryZc54_out_g(T122)) → binaryc60_out_g(zero(T122))
binaryc60_in_g(one(T126)) → U68_g(T126, binaryc60_in_g(T126))
U68_g(T126, binaryc60_out_g(T126)) → binaryc60_out_g(one(T126))
U66_g(T117, binaryc60_out_g(T117)) → binaryZc54_out_g(one(T117))
U65_g(T113, binaryZc54_out_g(T113)) → binaryZc54_out_g(zero(T113))
U62_gga(T107, binaryZc54_out_g(T107)) → addc29_out_gga(b, T107, zero(T107))
addc29_in_gga(zero(T156), T157, zero(T159)) → U63_gga(T156, T157, T159, addzc79_in_gga(T156, T157, T159))
addzc79_in_gga(zero(T175), zero(T176), zero(T178)) → U69_gga(T175, T176, T178, addzc79_in_gga(T175, T176, T178))
addzc79_in_gga(zero(one(T203)), one(b), one(one(T203))) → U70_gga(T203, binaryc60_in_g(T203))
U70_gga(T203, binaryc60_out_g(T203)) → addzc79_out_gga(zero(one(T203)), one(b), one(one(T203)))
addzc79_in_gga(zero(zero(T208)), one(b), one(zero(T208))) → U71_gga(T208, binaryZc54_in_g(T208))
U71_gga(T208, binaryZc54_out_g(T208)) → addzc79_out_gga(zero(zero(T208)), one(b), one(zero(T208)))
addzc79_in_gga(zero(T220), one(T221), one(T223)) → U72_gga(T220, T221, T223, addzc79_in_gga(T220, T221, T223))
addzc79_in_gga(one(T239), zero(T240), one(T242)) → U73_gga(T239, T240, T242, addyc102_in_gga(T239, T240, T242))
addyc102_in_gga(b, one(T248), one(T248)) → U90_gga(T248, binaryc60_in_g(T248))
U90_gga(T248, binaryc60_out_g(T248)) → addyc102_out_gga(b, one(T248), one(T248))
addyc102_in_gga(b, zero(T253), zero(T253)) → U91_gga(T253, binaryZc54_in_g(T253))
U91_gga(T253, binaryZc54_out_g(T253)) → addyc102_out_gga(b, zero(T253), zero(T253))
addyc102_in_gga(T265, T266, T268) → U92_gga(T265, T266, T268, addzc79_in_gga(T265, T266, T268))
addzc79_in_gga(one(T278), one(T279), zero(T281)) → U74_gga(T278, T279, T281, addcc114_in_gga(T278, T279, T281))
addcc114_in_gga(b, b, one(b)) → addcc114_out_gga(b, b, one(b))
addcc114_in_gga(T290, b, T292) → U87_gga(T290, T292, succZc124_in_ga(T290, T292))
succZc124_in_ga(zero(T298), one(T298)) → U77_ga(T298, binaryZc54_in_g(T298))
U77_ga(T298, binaryZc54_out_g(T298)) → succZc124_out_ga(zero(T298), one(T298))
succZc124_in_ga(one(T304), zero(T306)) → U78_ga(T304, T306, succc131_in_ga(T304, T306))
succc131_in_ga(b, one(b)) → succc131_out_ga(b, one(b))
succc131_in_ga(zero(T311), one(T311)) → U75_ga(T311, binaryZc54_in_g(T311))
U75_ga(T311, binaryZc54_out_g(T311)) → succc131_out_ga(zero(T311), one(T311))
succc131_in_ga(one(T317), zero(T319)) → U76_ga(T317, T319, succc131_in_ga(T317, T319))
U76_ga(T317, T319, succc131_out_ga(T317, T319)) → succc131_out_ga(one(T317), zero(T319))
U78_ga(T304, T306, succc131_out_ga(T304, T306)) → succZc124_out_ga(one(T304), zero(T306))
U87_gga(T290, T292, succZc124_out_ga(T290, T292)) → addcc114_out_gga(T290, b, T292)
addcc114_in_gga(b, T328, T330) → U88_gga(T328, T330, succZc124_in_ga(T328, T330))
U88_gga(T328, T330, succZc124_out_ga(T328, T330)) → addcc114_out_gga(b, T328, T330)
addcc114_in_gga(T342, T343, T345) → U89_gga(T342, T343, T345, addCc149_in_gga(T342, T343, T345))
addCc149_in_gga(zero(T361), zero(T362), one(T364)) → U79_gga(T361, T362, T364, addzc79_in_gga(T361, T362, T364))
U79_gga(T361, T362, T364, addzc79_out_gga(T361, T362, T364)) → addCc149_out_gga(zero(T361), zero(T362), one(T364))
addCc149_in_gga(zero(zero(T389)), one(b), zero(one(T389))) → U80_gga(T389, binaryZc54_in_g(T389))
U80_gga(T389, binaryZc54_out_g(T389)) → addCc149_out_gga(zero(zero(T389)), one(b), zero(one(T389)))
addCc149_in_gga(zero(one(T399)), one(b), zero(zero(T401))) → U81_gga(T399, T401, succc131_in_ga(T399, T401))
U81_gga(T399, T401, succc131_out_ga(T399, T401)) → addCc149_out_gga(zero(one(T399)), one(b), zero(zero(T401)))
addCc149_in_gga(zero(T412), one(T413), zero(T415)) → U82_gga(T412, T413, T415, addCc149_in_gga(T412, T413, T415))
addCc149_in_gga(one(b), zero(zero(T440)), zero(one(T440))) → U83_gga(T440, binaryZc54_in_g(T440))
U83_gga(T440, binaryZc54_out_g(T440)) → addCc149_out_gga(one(b), zero(zero(T440)), zero(one(T440)))
addCc149_in_gga(one(b), zero(one(T450)), zero(zero(T452))) → U84_gga(T450, T452, succc131_in_ga(T450, T452))
U84_gga(T450, T452, succc131_out_ga(T450, T452)) → addCc149_out_gga(one(b), zero(one(T450)), zero(zero(T452)))
addCc149_in_gga(one(T463), zero(T464), zero(T466)) → U85_gga(T463, T464, T466, addCc149_in_gga(T463, T464, T466))
addCc149_in_gga(one(T476), one(T477), one(T479)) → U86_gga(T476, T477, T479, addcc114_in_gga(T476, T477, T479))
U86_gga(T476, T477, T479, addcc114_out_gga(T476, T477, T479)) → addCc149_out_gga(one(T476), one(T477), one(T479))
U85_gga(T463, T464, T466, addCc149_out_gga(T463, T464, T466)) → addCc149_out_gga(one(T463), zero(T464), zero(T466))
U82_gga(T412, T413, T415, addCc149_out_gga(T412, T413, T415)) → addCc149_out_gga(zero(T412), one(T413), zero(T415))
U89_gga(T342, T343, T345, addCc149_out_gga(T342, T343, T345)) → addcc114_out_gga(T342, T343, T345)
U74_gga(T278, T279, T281, addcc114_out_gga(T278, T279, T281)) → addzc79_out_gga(one(T278), one(T279), zero(T281))
U92_gga(T265, T266, T268, addzc79_out_gga(T265, T266, T268)) → addyc102_out_gga(T265, T266, T268)
U73_gga(T239, T240, T242, addyc102_out_gga(T239, T240, T242)) → addzc79_out_gga(one(T239), zero(T240), one(T242))
U72_gga(T220, T221, T223, addzc79_out_gga(T220, T221, T223)) → addzc79_out_gga(zero(T220), one(T221), one(T223))
U69_gga(T175, T176, T178, addzc79_out_gga(T175, T176, T178)) → addzc79_out_gga(zero(T175), zero(T176), zero(T178))
U63_gga(T156, T157, T159, addzc79_out_gga(T156, T157, T159)) → addc29_out_gga(zero(T156), T157, zero(T159))
addc29_in_gga(one(T493), T494, one(T496)) → U64_gga(T493, T494, T496, addyc102_in_gga(T493, T494, T496))
U64_gga(T493, T494, T496, addyc102_out_gga(T493, T494, T496)) → addc29_out_gga(one(T493), T494, one(T496))
U61_gga(T83, T84, X125, addc29_out_gga(T84, T87, X125)) → timesc28_out_gga(one(T83), T84, X125)
U59_gga(T75, T76, X106, timesc28_out_gga(T75, T76, X106)) → timesc28_out_gga(zero(T75), T76, zero(X106))

The argument filtering Pi contains the following mapping:
zero(x1) = zero(x1)
one(x1) = one(x1)
timesc28_in_gga(x1, x2, x3) = timesc28_in_gga(x1, x2)
b = b
timesc28_out_gga(x1, x2, x3) = timesc28_out_gga(x1, x2, x3)
U59_gga(x1, x2, x3, x4) = U59_gga(x1, x2, x4)
U60_gga(x1, x2, x3, x4) = U60_gga(x1, x2, x4)
U61_gga(x1, x2, x3, x4) = U61_gga(x1, x2, x4)
addc29_in_gga(x1, x2, x3) = addc29_in_gga(x1, x2)
U62_gga(x1, x2) = U62_gga(x1, x2)
binaryZc54_in_g(x1) = binaryZc54_in_g(x1)
U65_g(x1, x2) = U65_g(x1, x2)
U66_g(x1, x2) = U66_g(x1, x2)
binaryc60_in_g(x1) = binaryc60_in_g(x1)
binaryc60_out_g(x1) = binaryc60_out_g(x1)
U67_g(x1, x2) = U67_g(x1, x2)
binaryZc54_out_g(x1) = binaryZc54_out_g(x1)
U68_g(x1, x2) = U68_g(x1, x2)
addc29_out_gga(x1, x2, x3) = addc29_out_gga(x1, x2, x3)
U63_gga(x1, x2, x3, x4) = U63_gga(x1, x2, x4)
addzc79_in_gga(x1, x2, x3) = addzc79_in_gga(x1, x2)
U69_gga(x1, x2, x3, x4) = U69_gga(x1, x2, x4)
U70_gga(x1, x2) = U70_gga(x1, x2)
addzc79_out_gga(x1, x2, x3) = addzc79_out_gga(x1, x2, x3)
U71_gga(x1, x2) = U71_gga(x1, x2)
U72_gga(x1, x2, x3, x4) = U72_gga(x1, x2, x4)
U73_gga(x1, x2, x3, x4) = U73_gga(x1, x2, x4)
addyc102_in_gga(x1, x2, x3) = addyc102_in_gga(x1, x2)
U90_gga(x1, x2) = U90_gga(x1, x2)
addyc102_out_gga(x1, x2, x3) = addyc102_out_gga(x1, x2, x3)
U91_gga(x1, x2) = U91_gga(x1, x2)
U92_gga(x1, x2, x3, x4) = U92_gga(x1, x2, x4)
U74_gga(x1, x2, x3, x4) = U74_gga(x1, x2, x4)
addcc114_in_gga(x1, x2, x3) = addcc114_in_gga(x1, x2)
addcc114_out_gga(x1, x2, x3) = addcc114_out_gga(x1, x2, x3)
U87_gga(x1, x2, x3) = U87_gga(x1, x3)
succZc124_in_ga(x1, x2) = succZc124_in_ga(x1)
U77_ga(x1, x2) = U77_ga(x1, x2)
succZc124_out_ga(x1, x2) = succZc124_out_ga(x1, x2)
U78_ga(x1, x2, x3) = U78_ga(x1, x3)
succc131_in_ga(x1, x2) = succc131_in_ga(x1)
succc131_out_ga(x1, x2) = succc131_out_ga(x1, x2)
U75_ga(x1, x2) = U75_ga(x1, x2)
U76_ga(x1, x2, x3) = U76_ga(x1, x3)
U88_gga(x1, x2, x3) = U88_gga(x1, x3)
U89_gga(x1, x2, x3, x4) = U89_gga(x1, x2, x4)
addCc149_in_gga(x1, x2, x3) = addCc149_in_gga(x1, x2)
U79_gga(x1, x2, x3, x4) = U79_gga(x1, x2, x4)
addCc149_out_gga(x1, x2, x3) = addCc149_out_gga(x1, x2, x3)
U80_gga(x1, x2) = U80_gga(x1, x2)
U81_gga(x1, x2, x3) = U81_gga(x1, x3)
U82_gga(x1, x2, x3, x4) = U82_gga(x1, x2, x4)
U83_gga(x1, x2) = U83_gga(x1, x2)
U84_gga(x1, x2, x3) = U84_gga(x1, x3)
U85_gga(x1, x2, x3, x4) = U85_gga(x1, x2, x4)
U86_gga(x1, x2, x3, x4) = U86_gga(x1, x2, x4)
U64_gga(x1, x2, x3, x4) = U64_gga(x1, x2, x4)
TIMES1_IN_GGA(x1, x2, x3) = TIMES1_IN_GGA(x1, x2)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

TIMES1_IN_GGA(zero(zero(T35)), T36, zero(zero(T38))) → TIMES1_IN_GGA(T35, T36, T38)

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

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

TIMES1_IN_GGA(zero(zero(T35)), T36) → TIMES1_IN_GGA(T35, T36)

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

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

TIMES1_IN_GGA(zero(zero(T35)), T36) → TIMES1_IN_GGA(T35, T36)
The graph contains the following edges 1 > 1, 2 >= 2

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES