Left Termination proof of /tmp/tmpfDvVhm/dependency2.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 331 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 4 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

(0) Obligation:

Clauses:

h(X) :- ','(f(X), g(X)).
f(c(0, X1)).
f(c(X, Y)) :- ','(no(zero(X)), ','(p(X, P), f(c(P, s(Y))))).
g(c(X2, 0)).
g(c(X, Y)) :- ','(no(zero(Y)), ','(p(Y, P), g(c(s(X), P)))).
p(0, 0).
p(s(X), X).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X3).
failure(b).

Query: h(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: h(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: h(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(f(T3), g(T3))\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 1 | ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: g(c(0, T8))\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: g(c(0, T8)), SCOPE: 3, CLAUSE: 3 | g(c(0, T8)), SCOPE: 3, CLAUSE: 4\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: g(c(0, T8)), SCOPE: 3, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: g(c(0, T8)), SCOPE: 3, CLAUSE: 4\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(no(zero(T11)), ','(p(T11, X26), g(c(s(0), X26))))\n\nT11 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(no(zero(T11)), ','(p(T11, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 8 | ','(no(zero(T11)), ','(p(T11, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 9\n\nT11 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(','(call(zero(T14)), ','(!_4, failure(a))), ','(p(T14, X26), g(c(s(0), X26)))) | ','(no(zero(T14)), ','(p(T14, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 9\n\nT14 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(zero(T14), ','(','(!_4, failure(a)), ','(p(T14, X26), g(c(s(0), X26))))) | ?_5 | ','(no(zero(T14)), ','(p(T14, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 9\n\nT14 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(zero(T14), ','(','(!_4, failure(a)), ','(p(T14, X26), g(c(s(0), X26))))), SCOPE: 6, CLAUSE: 7 | ?_6 | ?_5 | ','(no(zero(T14)), ','(p(T14, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 9\n\nT14 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(','(!_4, failure(a)), ','(p(0, X26), g(c(s(0), X26)))) | ?_6 | ?_5 | ','(no(zero(0)), ','(p(0, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 9\n\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ?_6 | ?_5 | ','(no(zero(T14)), ','(p(T14, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 9\n\nT14 is ground\nX26 is free\nzero(T14) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(failure(a), ','(p(0, X26), g(c(s(0), X26))))\n\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(failure(a), ','(p(0, X26), g(c(s(0), X26)))), SCOPE: 7, CLAUSE: 10\n\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ?_5 | ','(no(zero(T14)), ','(p(T14, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 9\n\nT14 is ground\nX26 is free\nzero(T14) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(no(zero(T14)), ','(p(T14, X26), g(c(s(0), X26)))), SCOPE: 4, CLAUSE: 9\n\nT14 is ground\nX26 is free\nzero(T14) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(p(T17, X26), g(c(s(0), X26)))\n\nT17 is ground\nX26 is free\nzero(T17) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(p(T17, X26), g(c(s(0), X26))), SCOPE: 8, CLAUSE: 5 | ','(p(T17, X26), g(c(s(0), X26))), SCOPE: 8, CLAUSE: 6\n\nT17 is ground\nX26 is free\nzero(T17) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(p(T17, X26), g(c(s(0), X26))), SCOPE: 8, CLAUSE: 6\n\nT17 is ground\nX26 is free\nzero(T17) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: g(c(s(0), T20))\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: g(c(s(0), T20)), SCOPE: 9, CLAUSE: 3 | g(c(s(0), T20)), SCOPE: 9, CLAUSE: 4\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: g(c(s(0), T20)), SCOPE: 9, CLAUSE: 3\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: g(c(s(0), T20)), SCOPE: 9, CLAUSE: 4\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(no(zero(T23)), ','(p(T23, X55), g(c(s(s(0)), X55))))\n\nT23 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(no(zero(T23)), ','(p(T23, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 8 | ','(no(zero(T23)), ','(p(T23, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 9\n\nT23 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(','(call(zero(T26)), ','(!_10, failure(a))), ','(p(T26, X55), g(c(s(s(0)), X55)))) | ','(no(zero(T26)), ','(p(T26, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 9\n\nT26 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(zero(T26), ','(','(!_10, failure(a)), ','(p(T26, X55), g(c(s(s(0)), X55))))) | ?_11 | ','(no(zero(T26)), ','(p(T26, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 9\n\nT26 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(zero(T26), ','(','(!_10, failure(a)), ','(p(T26, X55), g(c(s(s(0)), X55))))), SCOPE: 12, CLAUSE: 7 | ?_12 | ?_11 | ','(no(zero(T26)), ','(p(T26, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 9\n\nT26 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ','(','(!_10, failure(a)), ','(p(0, X55), g(c(s(s(0)), X55)))) | ?_12 | ?_11 | ','(no(zero(0)), ','(p(0, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 9\n\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ?_12 | ?_11 | ','(no(zero(T26)), ','(p(T26, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 9\n\nT26 is ground\nX55 is free\nzero(T26) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(failure(a), ','(p(0, X55), g(c(s(s(0)), X55))))\n\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(failure(a), ','(p(0, X55), g(c(s(s(0)), X55)))), SCOPE: 13, CLAUSE: 10\n\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ?_11 | ','(no(zero(T26)), ','(p(T26, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 9\n\nT26 is ground\nX55 is free\nzero(T26) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(no(zero(T26)), ','(p(T26, X55), g(c(s(s(0)), X55)))), SCOPE: 10, CLAUSE: 9\n\nT26 is ground\nX55 is free\nzero(T26) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(p(T29, X55), g(c(s(s(0)), X55)))\n\nT29 is ground\nX55 is free\nzero(T29) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(p(T29, X55), g(c(s(s(0)), X55))), SCOPE: 14, CLAUSE: 5 | ','(p(T29, X55), g(c(s(s(0)), X55))), SCOPE: 14, CLAUSE: 6\n\nT29 is ground\nX55 is free\nzero(T29) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(p(T29, X55), g(c(s(s(0)), X55))), SCOPE: 14, CLAUSE: 6\n\nT29 is ground\nX55 is free\nzero(T29) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: g(c(s(s(0)), T32))\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: g(c(s(s(0)), T32)), SCOPE: 15, CLAUSE: 3 | g(c(s(s(0)), T32)), SCOPE: 15, CLAUSE: 4\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: g(c(s(s(0)), T32)), SCOPE: 15, CLAUSE: 3\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: g(c(s(s(0)), T32)), SCOPE: 15, CLAUSE: 4\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(no(zero(T35)), ','(p(T35, X84), g(c(s(s(s(0))), X84))))\n\nT35 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(no(zero(T35)), ','(p(T35, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 8 | ','(no(zero(T35)), ','(p(T35, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 9\n\nT35 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(','(call(zero(T38)), ','(!_16, failure(a))), ','(p(T38, X84), g(c(s(s(s(0))), X84)))) | ','(no(zero(T38)), ','(p(T38, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 9\n\nT38 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(zero(T38), ','(','(!_16, failure(a)), ','(p(T38, X84), g(c(s(s(s(0))), X84))))) | ?_17 | ','(no(zero(T38)), ','(p(T38, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 9\n\nT38 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(zero(T38), ','(','(!_16, failure(a)), ','(p(T38, X84), g(c(s(s(s(0))), X84))))), SCOPE: 18, CLAUSE: 7 | ?_18 | ?_17 | ','(no(zero(T38)), ','(p(T38, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 9\n\nT38 is ground\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(','(!_16, failure(a)), ','(p(0, X84), g(c(s(s(s(0))), X84)))) | ?_18 | ?_17 | ','(no(zero(0)), ','(p(0, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 9\n\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ?_18 | ?_17 | ','(no(zero(T38)), ','(p(T38, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 9\n\nT38 is ground\nX84 is free\nzero(T38) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(failure(a), ','(p(0, X84), g(c(s(s(s(0))), X84))))\n\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(failure(a), ','(p(0, X84), g(c(s(s(s(0))), X84)))), SCOPE: 19, CLAUSE: 10\n\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ?_17 | ','(no(zero(T38)), ','(p(T38, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 9\n\nT38 is ground\nX84 is free\nzero(T38) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(no(zero(T38)), ','(p(T38, X84), g(c(s(s(s(0))), X84)))), SCOPE: 16, CLAUSE: 9\n\nT38 is ground\nX84 is free\nzero(T38) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(p(T41, X84), g(c(s(s(s(0))), X84)))\n\nT41 is ground\nX84 is free\nzero(T41) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ','(p(T41, X84), g(c(s(s(s(0))), X84))), SCOPE: 20, CLAUSE: 5 | ','(p(T41, X84), g(c(s(s(s(0))), X84))), SCOPE: 20, CLAUSE: 6\n\nT41 is ground\nX84 is free\nzero(T41) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ','(p(T41, X84), g(c(s(s(s(0))), X84))), SCOPE: 20, CLAUSE: 6\n\nT41 is ground\nX84 is free\nzero(T41) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: g(c(s(s(s(0))), T44))\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: g(c(s(s(s(0))), T44)), SCOPE: 21, CLAUSE: 3 | g(c(s(s(s(0))), T44)), SCOPE: 21, CLAUSE: 4\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: g(c(s(s(s(0))), T44)), SCOPE: 21, CLAUSE: 3\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: g(c(s(s(s(0))), T44)), SCOPE: 21, CLAUSE: 4\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(no(zero(T47)), ','(p(T47, X113), g(c(s(s(s(s(0)))), X113))))\n\nT47 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: ','(no(zero(T47)), ','(p(T47, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 8 | ','(no(zero(T47)), ','(p(T47, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 9\n\nT47 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(','(call(zero(T50)), ','(!_22, failure(a))), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113)))) | ','(no(zero(T50)), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 9\n\nT50 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: ','(zero(T50), ','(','(!_22, failure(a)), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113))))) | ?_23 | ','(no(zero(T50)), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 9\n\nT50 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: ','(zero(T50), ','(','(!_22, failure(a)), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113))))), SCOPE: 24, CLAUSE: 7 | ?_24 | ?_23 | ','(no(zero(T50)), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 9\n\nT50 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: ','(','(!_22, failure(a)), ','(p(0, X113), g(c(s(s(s(s(0)))), X113)))) | ?_24 | ?_23 | ','(no(zero(0)), ','(p(0, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 9\n\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ?_24 | ?_23 | ','(no(zero(T50)), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 9\n\nT50 is ground\nX113 is free\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: ','(failure(a), ','(p(0, X113), g(c(s(s(s(s(0)))), X113))))\n\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: ','(failure(a), ','(p(0, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 25, CLAUSE: 10\n\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: ?_23 | ','(no(zero(T50)), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 9\n\nT50 is ground\nX113 is free\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: ','(no(zero(T50)), ','(p(T50, X113), g(c(s(s(s(s(0)))), X113)))), SCOPE: 22, CLAUSE: 9\n\nT50 is ground\nX113 is free\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(p(T53, X113), g(c(s(s(s(s(0)))), X113)))\n\nT53 is ground\nX113 is free\nzero(T53) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ','(p(T53, X113), g(c(s(s(s(s(0)))), X113))), SCOPE: 26, CLAUSE: 5 | ','(p(T53, X113), g(c(s(s(s(s(0)))), X113))), SCOPE: 26, CLAUSE: 6\n\nT53 is ground\nX113 is free\nzero(T53) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: ','(p(T53, X113), g(c(s(s(s(s(0)))), X113))), SCOPE: 26, CLAUSE: 6\n\nT53 is ground\nX113 is free\nzero(T53) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: g(c(s(s(s(s(0)))), T56))\n\nT56 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: g(c(s(s(s(s(0)))), T56)), SCOPE: 27, CLAUSE: 3 | g(c(s(s(s(s(0)))), T56)), SCOPE: 27, CLAUSE: 4\n\nT56 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: g(c(s(s(s(s(0)))), T56)), SCOPE: 27, CLAUSE: 3\n\nT56 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: g(c(s(s(s(s(0)))), T56)), SCOPE: 27, CLAUSE: 4\n\nT56 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: ','(no(zero(T59)), ','(p(T59, X142), g(c(s(s(s(s(s(0))))), X142))))\n\nT59 is ground\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: ','(no(zero(T59)), ','(p(T59, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 8 | ','(no(zero(T59)), ','(p(T59, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 9\n\nT59 is ground\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: ','(','(call(zero(T62)), ','(!_28, failure(a))), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142)))) | ','(no(zero(T62)), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 9\n\nT62 is ground\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: ','(zero(T62), ','(','(!_28, failure(a)), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142))))) | ?_29 | ','(no(zero(T62)), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 9\n\nT62 is ground\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: ','(zero(T62), ','(','(!_28, failure(a)), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142))))), SCOPE: 30, CLAUSE: 7 | ?_30 | ?_29 | ','(no(zero(T62)), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 9\n\nT62 is ground\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: ','(','(!_28, failure(a)), ','(p(0, X142), g(c(s(s(s(s(s(0))))), X142)))) | ?_30 | ?_29 | ','(no(zero(0)), ','(p(0, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 9\n\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: ?_30 | ?_29 | ','(no(zero(T62)), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 9\n\nT62 is ground\nX142 is free\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: ','(failure(a), ','(p(0, X142), g(c(s(s(s(s(s(0))))), X142))))\n\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: ','(failure(a), ','(p(0, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 31, CLAUSE: 10\n\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: ?_29 | ','(no(zero(T62)), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 9\n\nT62 is ground\nX142 is free\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: ','(no(zero(T62)), ','(p(T62, X142), g(c(s(s(s(s(s(0))))), X142)))), SCOPE: 28, CLAUSE: 9\n\nT62 is ground\nX142 is free\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: ','(p(T65, X142), g(c(s(s(s(s(s(0))))), X142)))\n\nT65 is ground\nX142 is free\nzero(T65) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: ','(p(T65, X142), g(c(s(s(s(s(s(0))))), X142))), SCOPE: 32, CLAUSE: 5 | ','(p(T65, X142), g(c(s(s(s(s(s(0))))), X142))), SCOPE: 32, CLAUSE: 6\n\nT65 is ground\nX142 is free\nzero(T65) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
293 [label="293: ','(p(T65, X142), g(c(s(s(s(s(s(0))))), X142))), SCOPE: 32, CLAUSE: 6\n\nT65 is ground\nX142 is free\nzero(T65) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: g(c(s(s(s(s(s(0))))), T68))\n\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: g(c(s(s(s(s(s(0))))), T68)), SCOPE: 33, CLAUSE: 3 | g(c(s(s(s(s(s(0))))), T68)), SCOPE: 33, CLAUSE: 4\n\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: g(c(s(s(s(s(s(0))))), T68)), SCOPE: 33, CLAUSE: 3\n\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: g(c(s(s(s(s(s(0))))), T68)), SCOPE: 33, CLAUSE: 4\n\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="317: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: ','(no(zero(T71)), ','(p(T71, X171), g(c(s(s(s(s(s(s(0)))))), X171))))\n\nT71 is ground\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: ','(no(zero(T71)), ','(p(T71, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 8 | ','(no(zero(T71)), ','(p(T71, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 9\n\nT71 is ground\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: ','(','(call(zero(T74)), ','(!_34, failure(a))), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171)))) | ','(no(zero(T74)), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 9\n\nT74 is ground\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: ','(zero(T74), ','(','(!_34, failure(a)), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171))))) | ?_35 | ','(no(zero(T74)), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 9\n\nT74 is ground\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: ','(zero(T74), ','(','(!_34, failure(a)), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171))))), SCOPE: 36, CLAUSE: 7 | ?_36 | ?_35 | ','(no(zero(T74)), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 9\n\nT74 is ground\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
347 [label="347: ','(','(!_34, failure(a)), ','(p(0, X171), g(c(s(s(s(s(s(s(0)))))), X171)))) | ?_36 | ?_35 | ','(no(zero(0)), ','(p(0, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 9\n\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
348 [label="348: ?_36 | ?_35 | ','(no(zero(T74)), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 9\n\nT74 is ground\nX171 is free\nzero(T74) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: ','(failure(a), ','(p(0, X171), g(c(s(s(s(s(s(s(0)))))), X171))))\n\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
350 [label="350: ','(failure(a), ','(p(0, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 37, CLAUSE: 10\n\nX171 is free", fontsize=16, style=filled, fillcolor=lightyellow];
352 [label="352: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
353 [label="353: ?_35 | ','(no(zero(T74)), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 9\n\nT74 is ground\nX171 is free\nzero(T74) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
354 [label="354: ','(no(zero(T74)), ','(p(T74, X171), g(c(s(s(s(s(s(s(0)))))), X171)))), SCOPE: 34, CLAUSE: 9\n\nT74 is ground\nX171 is free\nzero(T74) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: ','(p(T77, X171), g(c(s(s(s(s(s(s(0)))))), X171)))\n\nT77 is ground\nX171 is free\nzero(T77) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
357 [label="357: ','(p(T77, X171), g(c(s(s(s(s(s(s(0)))))), X171))), SCOPE: 38, CLAUSE: 5 | ','(p(T77, X171), g(c(s(s(s(s(s(s(0)))))), X171))), SCOPE: 38, CLAUSE: 6\n\nT77 is ground\nX171 is free\nzero(T77) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
358 [label="358: ','(p(T77, X171), g(c(s(s(s(s(s(s(0)))))), X171))), SCOPE: 38, CLAUSE: 6\n\nT77 is ground\nX171 is free\nzero(T77) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
360 [label="360: g(c(s(s(s(s(s(s(0)))))), T80))\n\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
362 [label="362: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
369 [label="369: g(c(s(s(s(s(s(s(0)))))), T80)), SCOPE: 39, CLAUSE: 3 | g(c(s(s(s(s(s(s(0)))))), T80)), SCOPE: 39, CLAUSE: 4\n\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: g(c(s(s(s(s(s(s(0)))))), T80)), SCOPE: 39, CLAUSE: 3\n\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: g(c(s(s(s(s(s(s(0)))))), T80)), SCOPE: 39, CLAUSE: 4\n\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
372 [label="372: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="373: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
374 [label="374: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: ','(no(zero(T83)), ','(p(T83, X200), g(c(s(s(s(s(s(s(s(0))))))), X200))))\n\nT83 is ground\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: ','(no(zero(T83)), ','(p(T83, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 8 | ','(no(zero(T83)), ','(p(T83, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 9\n\nT83 is ground\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
377 [label="377: ','(','(call(zero(T86)), ','(!_40, failure(a))), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))) | ','(no(zero(T86)), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 9\n\nT86 is ground\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: ','(zero(T86), ','(','(!_40, failure(a)), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200))))) | ?_41 | ','(no(zero(T86)), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 9\n\nT86 is ground\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: ','(zero(T86), ','(','(!_40, failure(a)), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200))))), SCOPE: 42, CLAUSE: 7 | ?_42 | ?_41 | ','(no(zero(T86)), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 9\n\nT86 is ground\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
383 [label="383: ','(','(!_40, failure(a)), ','(p(0, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))) | ?_42 | ?_41 | ','(no(zero(0)), ','(p(0, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 9\n\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
384 [label="384: ?_42 | ?_41 | ','(no(zero(T86)), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 9\n\nT86 is ground\nX200 is free\nzero(T86) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
385 [label="385: ','(failure(a), ','(p(0, X200), g(c(s(s(s(s(s(s(s(0))))))), X200))))\n\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
386 [label="386: ','(failure(a), ','(p(0, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 43, CLAUSE: 10\n\nX200 is free", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: ?_41 | ','(no(zero(T86)), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 9\n\nT86 is ground\nX200 is free\nzero(T86) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
390 [label="390: ','(no(zero(T86)), ','(p(T86, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))), SCOPE: 40, CLAUSE: 9\n\nT86 is ground\nX200 is free\nzero(T86) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
392 [label="392: ','(p(T89, X200), g(c(s(s(s(s(s(s(s(0))))))), X200)))\n\nT89 is ground\nX200 is free\nzero(T89) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
394 [label="394: ','(p(T89, X200), g(c(s(s(s(s(s(s(s(0))))))), X200))), SCOPE: 44, CLAUSE: 5 | ','(p(T89, X200), g(c(s(s(s(s(s(s(s(0))))))), X200))), SCOPE: 44, CLAUSE: 6\n\nT89 is ground\nX200 is free\nzero(T89) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
396 [label="396: ','(p(T89, X200), g(c(s(s(s(s(s(s(s(0))))))), X200))), SCOPE: 44, CLAUSE: 6\n\nT89 is ground\nX200 is free\nzero(T89) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
399 [label="399: g(c(s(s(s(s(s(s(s(0))))))), T92))\n\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
401 [label="401: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
408 [label="408: g(c(s(s(s(s(s(s(s(0))))))), T92)), SCOPE: 45, CLAUSE: 3 | g(c(s(s(s(s(s(s(s(0))))))), T92)), SCOPE: 45, CLAUSE: 4\n\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
409 [label="409: g(c(s(s(s(s(s(s(s(0))))))), T92)), SCOPE: 45, CLAUSE: 3\n\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
410 [label="410: g(c(s(s(s(s(s(s(s(0))))))), T92)), SCOPE: 45, CLAUSE: 4\n\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
411 [label="411: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
412 [label="412: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
413 [label="413: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
414 [label="414: ','(no(zero(T95)), ','(p(T95, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229))))\n\nT95 is ground\nX229 is free", fontsize=16, style=filled, fillcolor=lightyellow];
415 [label="415: ','(no(zero(T95)), ','(p(T95, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 8 | ','(no(zero(T95)), ','(p(T95, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 9\n\nT95 is ground\nX229 is free", fontsize=16, style=filled, fillcolor=lightyellow];
416 [label="416: ','(','(call(zero(T98)), ','(!_46, failure(a))), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))) | ','(no(zero(T98)), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 9\n\nT98 is ground\nX229 is free", fontsize=16, style=filled, fillcolor=lightyellow];
417 [label="417: ','(zero(T98), ','(','(!_46, failure(a)), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229))))) | ?_47 | ','(no(zero(T98)), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 9\n\nT98 is ground\nX229 is free", fontsize=16, style=filled, fillcolor=lightyellow];
418 [label="418: ','(zero(T98), ','(','(!_46, failure(a)), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229))))), SCOPE: 48, CLAUSE: 7 | ?_48 | ?_47 | ','(no(zero(T98)), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 9\n\nT98 is ground\nX229 is free", fontsize=16, style=filled, fillcolor=lightyellow];
419 [label="419: ','(','(!_46, failure(a)), ','(p(0, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))) | ?_48 | ?_47 | ','(no(zero(0)), ','(p(0, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 9\n\nX229 is free", fontsize=16, style=filled, fillcolor=lightyellow];
420 [label="420: ?_48 | ?_47 | ','(no(zero(T98)), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 9\n\nT98 is ground\nX229 is free\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
421 [label="421: ','(failure(a), ','(p(0, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229))))\n\nX229 is free", fontsize=16, style=filled, fillcolor=lightyellow];
422 [label="422: ','(failure(a), ','(p(0, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 49, CLAUSE: 10\n\nX229 is free", fontsize=16, style=filled, fillcolor=lightyellow];
424 [label="424: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
425 [label="425: ?_47 | ','(no(zero(T98)), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 9\n\nT98 is ground\nX229 is free\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
427 [label="427: ','(no(zero(T98)), ','(p(T98, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))), SCOPE: 46, CLAUSE: 9\n\nT98 is ground\nX229 is free\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
430 [label="430: ','(p(T101, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229)))\n\nT101 is ground\nX229 is free\nzero(T101) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
431 [label="431: ','(p(T101, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229))), SCOPE: 50, CLAUSE: 5 | ','(p(T101, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229))), SCOPE: 50, CLAUSE: 6\n\nT101 is ground\nX229 is free\nzero(T101) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
432 [label="432: ','(p(T101, X229), g(c(s(s(s(s(s(s(s(s(0)))))))), X229))), SCOPE: 50, CLAUSE: 6\n\nT101 is ground\nX229 is free\nzero(T101) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
433 [label="433: g(c(s(s(s(s(s(s(s(s(0)))))))), T104))\n\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
434 [label="434: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
441 [label="B: g(c(s(T105), T104))\n\nT104 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
442 [label="442: g(c(s(T105), T104)), SCOPE: 51, CLAUSE: 3 | g(c(s(T105), T104)), SCOPE: 51, CLAUSE: 4\n\nT104 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
443 [label="443: g(c(s(T105), T104)), SCOPE: 51, CLAUSE: 3\n\nT104 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
444 [label="444: g(c(s(T105), T104)), SCOPE: 51, CLAUSE: 4\n\nT104 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
445 [label="445: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
446 [label="446: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
447 [label="447: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
448 [label="448: ','(no(zero(T119)), ','(p(T119, X260), g(c(s(s(T118)), X260))))\n\nT118 is ground\nT119 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
449 [label="449: ','(no(zero(T119)), ','(p(T119, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 8 | ','(no(zero(T119)), ','(p(T119, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 9\n\nT118 is ground\nT119 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
450 [label="450: ','(','(call(zero(T123)), ','(!_52, failure(a))), ','(p(T123, X260), g(c(s(s(T118)), X260)))) | ','(no(zero(T123)), ','(p(T123, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 9\n\nT118 is ground\nT123 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: ','(zero(T123), ','(','(!_52, failure(a)), ','(p(T123, X260), g(c(s(s(T118)), X260))))) | ?_53 | ','(no(zero(T123)), ','(p(T123, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 9\n\nT118 is ground\nT123 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
452 [label="452: ','(zero(T123), ','(','(!_52, failure(a)), ','(p(T123, X260), g(c(s(s(T118)), X260))))), SCOPE: 54, CLAUSE: 7 | ?_54 | ?_53 | ','(no(zero(T123)), ','(p(T123, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 9\n\nT118 is ground\nT123 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
453 [label="453: ','(','(!_52, failure(a)), ','(p(0, X260), g(c(s(s(T118)), X260)))) | ?_54 | ?_53 | ','(no(zero(0)), ','(p(0, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 9\n\nT118 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
454 [label="454: ?_54 | ?_53 | ','(no(zero(T123)), ','(p(T123, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 9\n\nT118 is ground\nT123 is ground\nX260 is free\nzero(T123) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
455 [label="455: ','(failure(a), ','(p(0, X260), g(c(s(s(T118)), X260))))\n\nT118 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
457 [label="457: ','(failure(a), ','(p(0, X260), g(c(s(s(T118)), X260)))), SCOPE: 55, CLAUSE: 10\n\nT118 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
458 [label="458: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
459 [label="459: ?_53 | ','(no(zero(T123)), ','(p(T123, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 9\n\nT118 is ground\nT123 is ground\nX260 is free\nzero(T123) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
460 [label="460: ','(no(zero(T123)), ','(p(T123, X260), g(c(s(s(T118)), X260)))), SCOPE: 52, CLAUSE: 9\n\nT118 is ground\nT123 is ground\nX260 is free\nzero(T123) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
463 [label="463: ','(p(T128, X260), g(c(s(s(T118)), X260)))\n\nT118 is ground\nT128 is ground\nX260 is free\nzero(T128) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
466 [label="466: ','(p(T128, X260), g(c(s(s(T118)), X260))), SCOPE: 56, CLAUSE: 5 | ','(p(T128, X260), g(c(s(s(T118)), X260))), SCOPE: 56, CLAUSE: 6\n\nT118 is ground\nT128 is ground\nX260 is free\nzero(T128) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
467 [label="467: ','(p(T128, X260), g(c(s(s(T118)), X260))), SCOPE: 56, CLAUSE: 6\n\nT118 is ground\nT128 is ground\nX260 is free\nzero(T128) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
472 [label="472: g(c(s(s(T118)), T132))\n\nT118 is ground\nT132 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
475 [label="475: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
482 [label="482: ','(','(no(zero(T139)), ','(p(T139, X283), f(c(X283, s(T140))))), g(c(T139, T140)))\n\nT139 is ground\nT140 is ground\nX283 is free", fontsize=16, style=filled, fillcolor=lightyellow];
483 [label="483: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
484 [label="484: ','(','(no(zero(T139)), ','(p(T139, X283), f(c(X283, s(T140))))), g(c(T139, T140))), SCOPE: 57, CLAUSE: 8 | ','(','(no(zero(T139)), ','(p(T139, X283), f(c(X283, s(T140))))), g(c(T139, T140))), SCOPE: 57, CLAUSE: 9\n\nT139 is ground\nT140 is ground\nX283 is free", fontsize=16, style=filled, fillcolor=lightyellow];
485 [label="485: ','(','(call(zero(T146)), ','(!_57, failure(a))), ','(','(p(T146, X283), f(c(X283, s(T140)))), g(c(T146, T140)))) | ','(','(no(zero(T146)), ','(p(T146, X283), f(c(X283, s(T140))))), g(c(T146, T140))), SCOPE: 57, CLAUSE: 9\n\nT140 is ground\nT146 is ground\nX283 is free", fontsize=16, style=filled, fillcolor=lightyellow];
486 [label="486: ','(zero(T146), ','(','(!_57, failure(a)), ','(','(p(T146, X283), f(c(X283, s(T140)))), g(c(T146, T140))))) | ?_58 | ','(','(no(zero(T146)), ','(p(T146, X283), f(c(X283, s(T140))))), g(c(T146, T140))), SCOPE: 57, CLAUSE: 9\n\nT140 is ground\nT146 is ground\nX283 is free", fontsize=16, style=filled, fillcolor=lightyellow];
487 [label="487: ','(zero(T146), ','(','(!_57, failure(a)), ','(','(p(T146, X283), f(c(X283, s(T140)))), g(c(T146, T140))))), SCOPE: 59, CLAUSE: 7 | ?_59 | ?_58 | ','(','(no(zero(T146)), ','(p(T146, X283), f(c(X283, s(T140))))), g(c(T146, T140))), SCOPE: 57, CLAUSE: 9\n\nT140 is ground\nT146 is ground\nX283 is free", fontsize=16, style=filled, fillcolor=lightyellow];
488 [label="488: ','(','(!_57, failure(a)), ','(','(p(0, X283), f(c(X283, s(T140)))), g(c(0, T140)))) | ?_59 | ?_58 | ','(','(no(zero(0)), ','(p(0, X283), f(c(X283, s(T140))))), g(c(0, T140))), SCOPE: 57, CLAUSE: 9\n\nT140 is ground\nX283 is free", fontsize=16, style=filled, fillcolor=lightyellow];
489 [label="489: ?_59 | ?_58 | ','(','(no(zero(T146)), ','(p(T146, X283), f(c(X283, s(T140))))), g(c(T146, T140))), SCOPE: 57, CLAUSE: 9\n\nT140 is ground\nT146 is ground\nX283 is free\nzero(T146) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
490 [label="490: ','(failure(a), ','(','(p(0, X283), f(c(X283, s(T140)))), g(c(0, T140))))\n\nT140 is ground\nX283 is free", fontsize=16, style=filled, fillcolor=lightyellow];
491 [label="491: ','(failure(a), ','(','(p(0, X283), f(c(X283, s(T140)))), g(c(0, T140)))), SCOPE: 60, CLAUSE: 10\n\nT140 is ground\nX283 is free", fontsize=16, style=filled, fillcolor=lightyellow];
492 [label="492: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
493 [label="493: ?_58 | ','(','(no(zero(T146)), ','(p(T146, X283), f(c(X283, s(T140))))), g(c(T146, T140))), SCOPE: 57, CLAUSE: 9\n\nT140 is ground\nT146 is ground\nX283 is free\nzero(T146) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
494 [label="494: ','(','(no(zero(T146)), ','(p(T146, X283), f(c(X283, s(T140))))), g(c(T146, T140))), SCOPE: 57, CLAUSE: 9\n\nT140 is ground\nT146 is ground\nX283 is free\nzero(T146) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
495 [label="495: ','(','(p(T153, X283), f(c(X283, s(T140)))), g(c(T153, T140)))\n\nT140 is ground\nT153 is ground\nX283 is free\nzero(T153) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
496 [label="496: ','(','(p(T153, X283), f(c(X283, s(T140)))), g(c(T153, T140))), SCOPE: 61, CLAUSE: 5 | ','(','(p(T153, X283), f(c(X283, s(T140)))), g(c(T153, T140))), SCOPE: 61, CLAUSE: 6\n\nT140 is ground\nT153 is ground\nX283 is free\nzero(T153) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
497 [label="497: ','(','(p(T153, X283), f(c(X283, s(T140)))), g(c(T153, T140))), SCOPE: 61, CLAUSE: 6\n\nT140 is ground\nT153 is ground\nX283 is free\nzero(T153) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
498 [label="C: ','(f(c(T159, s(T140))), g(c(s(T159), T140)))\n\nT140 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
499 [label="499: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
507 [label="D: f(c(T159, s(T140)))\n\nT140 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
508 [label="508: g(c(s(T159), T140))\n\nT140 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
509 [label="509: f(c(T159, s(T140))), SCOPE: 62, CLAUSE: 1 | f(c(T159, s(T140))), SCOPE: 62, CLAUSE: 2\n\nT140 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
510 [label="510: f(c(T159, s(T140))), SCOPE: 62, CLAUSE: 1\n\nT140 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
511 [label="511: f(c(T159, s(T140))), SCOPE: 62, CLAUSE: 2\n\nT140 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
512 [label="512: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
513 [label="513: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
514 [label="514: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
515 [label="515: ','(no(zero(T174)), ','(p(T174, X322), f(c(X322, s(s(T175))))))\n\nT174 is ground\nT175 is ground\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
516 [label="516: ','(no(zero(T174)), ','(p(T174, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 8 | ','(no(zero(T174)), ','(p(T174, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 9\n\nT174 is ground\nT175 is ground\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
517 [label="517: ','(','(call(zero(T179)), ','(!_63, failure(a))), ','(p(T179, X322), f(c(X322, s(s(T175)))))) | ','(no(zero(T179)), ','(p(T179, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 9\n\nT175 is ground\nT179 is ground\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
518 [label="518: ','(zero(T179), ','(','(!_63, failure(a)), ','(p(T179, X322), f(c(X322, s(s(T175))))))) | ?_64 | ','(no(zero(T179)), ','(p(T179, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 9\n\nT175 is ground\nT179 is ground\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
519 [label="519: ','(zero(T179), ','(','(!_63, failure(a)), ','(p(T179, X322), f(c(X322, s(s(T175))))))), SCOPE: 65, CLAUSE: 7 | ?_65 | ?_64 | ','(no(zero(T179)), ','(p(T179, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 9\n\nT175 is ground\nT179 is ground\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
520 [label="520: ','(','(!_63, failure(a)), ','(p(0, X322), f(c(X322, s(s(T175)))))) | ?_65 | ?_64 | ','(no(zero(0)), ','(p(0, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 9\n\nT175 is ground\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
521 [label="521: ?_65 | ?_64 | ','(no(zero(T179)), ','(p(T179, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 9\n\nT175 is ground\nT179 is ground\nX322 is free\nzero(T179) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
522 [label="522: ','(failure(a), ','(p(0, X322), f(c(X322, s(s(T175))))))\n\nT175 is ground\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
523 [label="523: ','(failure(a), ','(p(0, X322), f(c(X322, s(s(T175)))))), SCOPE: 66, CLAUSE: 10\n\nT175 is ground\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
524 [label="524: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
525 [label="525: ?_64 | ','(no(zero(T179)), ','(p(T179, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 9\n\nT175 is ground\nT179 is ground\nX322 is free\nzero(T179) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
526 [label="526: ','(no(zero(T179)), ','(p(T179, X322), f(c(X322, s(s(T175)))))), SCOPE: 63, CLAUSE: 9\n\nT175 is ground\nT179 is ground\nX322 is free\nzero(T179) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
529 [label="529: ','(p(T184, X322), f(c(X322, s(s(T175)))))\n\nT175 is ground\nT184 is ground\nX322 is free\nzero(T184) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
530 [label="530: ','(p(T184, X322), f(c(X322, s(s(T175))))), SCOPE: 67, CLAUSE: 5 | ','(p(T184, X322), f(c(X322, s(s(T175))))), SCOPE: 67, CLAUSE: 6\n\nT175 is ground\nT184 is ground\nX322 is free\nzero(T184) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
532 [label="532: ','(p(T184, X322), f(c(X322, s(s(T175))))), SCOPE: 67, CLAUSE: 6\n\nT175 is ground\nT184 is ground\nX322 is free\nzero(T184) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
538 [label="538: f(c(T188, s(s(T175))))\n\nT175 is ground\nT188 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
539 [label="539: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
540 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 540 [arrowhead = none ];
540 -> 6;

541 [label="ONLY EVAL with clause\nh(X5) :- ','(f(X5), g(X5)).\nand substitutionT1 -> T3,\nX5 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 541 [arrowhead = none ];
541 -> 8;

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

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

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

545 [label="EVAL with clause\nf(c(0, X10)).\nand substitutionX10 -> T8,\nT3 -> c(0, T8)", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 545 [arrowhead = none ];
545 -> 16;

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

547 [label="EVAL with clause\nf(c(X281, X282)) :- ','(no(zero(X281)), ','(p(X281, X283), f(c(X283, s(X282))))).\nand substitutionX281 -> T139,\nX282 -> T140,\nT3 -> c(T139, T140)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 547 [arrowhead = none ];
547 -> 482;

548 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 548 [arrowhead = none ];
548 -> 483;

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

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

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

552 [label="EVAL with clause\ng(c(X17, 0)).\nand substitutionX17 -> 0,\nT8 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 552 [arrowhead = none ];
552 -> 32;

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

554 [label="ONLY EVAL with clause\ng(c(X24, X25)) :- ','(no(zero(X25)), ','(p(X25, X26), g(c(s(X24), X26)))).\nand substitutionX24 -> 0,\nT8 -> T11,\nX25 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 554 [arrowhead = none ];
554 -> 40;

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

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

557 [label="ONLY EVAL with clause\nno(X30) :- ','(call(X30), ','(!_4, failure(a))).\nand substitutionT11 -> T14,\nX30 -> zero(T14)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 557 [arrowhead = none ];
557 -> 47;

558 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
47 -> 558 [arrowhead = none ];
558 -> 48;

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

560 [label="EVAL with clause\nzero(0).\nand substitutionT14 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 560 [arrowhead = none ];
560 -> 60;

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

562 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 562 [arrowhead = none ];
562 -> 62;

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

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

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

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

567 [label="ONLY EVAL with clause\nno(X35).\nand substitutionT14 -> T17,\nX35 -> zero(T17)", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 567 [arrowhead = none ];
567 -> 87;

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

569 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T17), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 569 [arrowhead = none ];
569 -> 89;

570 [label="EVAL with clause\np(s(X39), X39).\nand substitutionX39 -> T20,\nT17 -> s(T20),\nX26 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 570 [arrowhead = none ];
570 -> 96;

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

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

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

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

575 [label="EVAL with clause\ng(c(X46, 0)).\nand substitutionX46 -> s(0),\nT20 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 575 [arrowhead = none ];
575 -> 123;

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

577 [label="ONLY EVAL with clause\ng(c(X53, X54)) :- ','(no(zero(X54)), ','(p(X54, X55), g(c(s(X53), X55)))).\nand substitutionX53 -> s(0),\nT20 -> T23,\nX54 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 577 [arrowhead = none ];
577 -> 151;

578 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 578 [arrowhead = none ];
578 -> 126;

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

580 [label="ONLY EVAL with clause\nno(X59) :- ','(call(X59), ','(!_10, failure(a))).\nand substitutionT23 -> T26,\nX59 -> zero(T26)", fontsize=14, style = filled, fillcolor = lightblue];
152 -> 580 [arrowhead = none ];
580 -> 155;

581 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
155 -> 581 [arrowhead = none ];
581 -> 156;

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

583 [label="EVAL with clause\nzero(0).\nand substitutionT26 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 583 [arrowhead = none ];
583 -> 158;

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

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

586 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
159 -> 586 [arrowhead = none ];
586 -> 163;

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

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

589 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
163 -> 589 [arrowhead = none ];
589 -> 164;

590 [label="ONLY EVAL with clause\nno(X64).\nand substitutionT26 -> T29,\nX64 -> zero(T29)", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 590 [arrowhead = none ];
590 -> 165;

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

592 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T29), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
166 -> 592 [arrowhead = none ];
592 -> 167;

593 [label="EVAL with clause\np(s(X68), X68).\nand substitutionX68 -> T32,\nT29 -> s(T32),\nX55 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 593 [arrowhead = none ];
593 -> 168;

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

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

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

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

598 [label="EVAL with clause\ng(c(X75, 0)).\nand substitutionX75 -> s(s(0)),\nT32 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 598 [arrowhead = none ];
598 -> 181;

599 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 599 [arrowhead = none ];
599 -> 183;

600 [label="ONLY EVAL with clause\ng(c(X82, X83)) :- ','(no(zero(X83)), ','(p(X83, X84), g(c(s(X82), X84)))).\nand substitutionX82 -> s(s(0)),\nT32 -> T35,\nX83 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 600 [arrowhead = none ];
600 -> 188;

601 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 601 [arrowhead = none ];
601 -> 184;

602 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
188 -> 602 [arrowhead = none ];
602 -> 190;

603 [label="ONLY EVAL with clause\nno(X88) :- ','(call(X88), ','(!_16, failure(a))).\nand substitutionT35 -> T38,\nX88 -> zero(T38)", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 603 [arrowhead = none ];
603 -> 193;

604 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
193 -> 604 [arrowhead = none ];
604 -> 194;

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

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

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

608 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 608 [arrowhead = none ];
608 -> 198;

609 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 609 [arrowhead = none ];
609 -> 208;

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

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

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

613 [label="ONLY EVAL with clause\nno(X93).\nand substitutionT38 -> T41,\nX93 -> zero(T41)", fontsize=14, style = filled, fillcolor = lightblue];
209 -> 613 [arrowhead = none ];
613 -> 210;

614 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
210 -> 614 [arrowhead = none ];
614 -> 211;

615 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T41), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
211 -> 615 [arrowhead = none ];
615 -> 212;

616 [label="EVAL with clause\np(s(X97), X97).\nand substitutionX97 -> T44,\nT41 -> s(T44),\nX84 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 616 [arrowhead = none ];
616 -> 213;

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

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

619 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
215 -> 619 [arrowhead = none ];
619 -> 216;

620 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
215 -> 620 [arrowhead = none ];
620 -> 217;

621 [label="EVAL with clause\ng(c(X104, 0)).\nand substitutionX104 -> s(s(s(0))),\nT44 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
216 -> 621 [arrowhead = none ];
621 -> 218;

622 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
216 -> 622 [arrowhead = none ];
622 -> 219;

623 [label="ONLY EVAL with clause\ng(c(X111, X112)) :- ','(no(zero(X112)), ','(p(X112, X113), g(c(s(X111), X113)))).\nand substitutionX111 -> s(s(s(0))),\nT44 -> T47,\nX112 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
217 -> 623 [arrowhead = none ];
623 -> 225;

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

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

626 [label="ONLY EVAL with clause\nno(X117) :- ','(call(X117), ','(!_22, failure(a))).\nand substitutionT47 -> T50,\nX117 -> zero(T50)", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 626 [arrowhead = none ];
626 -> 234;

627 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
234 -> 627 [arrowhead = none ];
627 -> 235;

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

629 [label="EVAL with clause\nzero(0).\nand substitutionT50 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
236 -> 629 [arrowhead = none ];
629 -> 237;

630 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
236 -> 630 [arrowhead = none ];
630 -> 238;

631 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
237 -> 631 [arrowhead = none ];
631 -> 239;

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

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

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

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

636 [label="ONLY EVAL with clause\nno(X122).\nand substitutionT50 -> T53,\nX122 -> zero(T53)", fontsize=14, style = filled, fillcolor = lightblue];
248 -> 636 [arrowhead = none ];
636 -> 249;

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

638 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T53), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
250 -> 638 [arrowhead = none ];
638 -> 251;

639 [label="EVAL with clause\np(s(X126), X126).\nand substitutionX126 -> T56,\nT53 -> s(T56),\nX113 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
251 -> 639 [arrowhead = none ];
639 -> 252;

640 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
251 -> 640 [arrowhead = none ];
640 -> 253;

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

642 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
257 -> 642 [arrowhead = none ];
642 -> 261;

643 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
257 -> 643 [arrowhead = none ];
643 -> 262;

644 [label="EVAL with clause\ng(c(X133, 0)).\nand substitutionX133 -> s(s(s(s(0)))),\nT56 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
261 -> 644 [arrowhead = none ];
644 -> 263;

645 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
261 -> 645 [arrowhead = none ];
645 -> 264;

646 [label="ONLY EVAL with clause\ng(c(X140, X141)) :- ','(no(zero(X141)), ','(p(X141, X142), g(c(s(X140), X142)))).\nand substitutionX140 -> s(s(s(s(0)))),\nT56 -> T59,\nX141 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 646 [arrowhead = none ];
646 -> 266;

647 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
263 -> 647 [arrowhead = none ];
647 -> 265;

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

649 [label="ONLY EVAL with clause\nno(X146) :- ','(call(X146), ','(!_28, failure(a))).\nand substitutionT59 -> T62,\nX146 -> zero(T62)", fontsize=14, style = filled, fillcolor = lightblue];
275 -> 649 [arrowhead = none ];
649 -> 280;

650 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
280 -> 650 [arrowhead = none ];
650 -> 281;

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

652 [label="EVAL with clause\nzero(0).\nand substitutionT62 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
282 -> 652 [arrowhead = none ];
652 -> 284;

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

654 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
284 -> 654 [arrowhead = none ];
654 -> 286;

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

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

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

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

659 [label="ONLY EVAL with clause\nno(X151).\nand substitutionT62 -> T65,\nX151 -> zero(T65)", fontsize=14, style = filled, fillcolor = lightblue];
290 -> 659 [arrowhead = none ];
659 -> 291;

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

661 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T65), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
292 -> 661 [arrowhead = none ];
661 -> 293;

662 [label="EVAL with clause\np(s(X155), X155).\nand substitutionX155 -> T68,\nT65 -> s(T68),\nX142 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
293 -> 662 [arrowhead = none ];
662 -> 294;

663 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
293 -> 663 [arrowhead = none ];
663 -> 295;

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

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

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

667 [label="EVAL with clause\ng(c(X162, 0)).\nand substitutionX162 -> s(s(s(s(s(0))))),\nT68 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
297 -> 667 [arrowhead = none ];
667 -> 299;

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

669 [label="ONLY EVAL with clause\ng(c(X169, X170)) :- ','(no(zero(X170)), ','(p(X170, X171), g(c(s(X169), X171)))).\nand substitutionX169 -> s(s(s(s(s(0))))),\nT68 -> T71,\nX170 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
298 -> 669 [arrowhead = none ];
669 -> 319;

670 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
299 -> 670 [arrowhead = none ];
670 -> 318;

671 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
319 -> 671 [arrowhead = none ];
671 -> 320;

672 [label="ONLY EVAL with clause\nno(X175) :- ','(call(X175), ','(!_34, failure(a))).\nand substitutionT71 -> T74,\nX175 -> zero(T74)", fontsize=14, style = filled, fillcolor = lightblue];
320 -> 672 [arrowhead = none ];
672 -> 321;

673 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
321 -> 673 [arrowhead = none ];
673 -> 328;

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

675 [label="EVAL with clause\nzero(0).\nand substitutionT74 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
340 -> 675 [arrowhead = none ];
675 -> 347;

676 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
340 -> 676 [arrowhead = none ];
676 -> 348;

677 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
347 -> 677 [arrowhead = none ];
677 -> 349;

678 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
348 -> 678 [arrowhead = none ];
678 -> 353;

679 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
349 -> 679 [arrowhead = none ];
679 -> 350;

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

681 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
353 -> 681 [arrowhead = none ];
681 -> 354;

682 [label="ONLY EVAL with clause\nno(X180).\nand substitutionT74 -> T77,\nX180 -> zero(T77)", fontsize=14, style = filled, fillcolor = lightblue];
354 -> 682 [arrowhead = none ];
682 -> 356;

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

684 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T77), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
357 -> 684 [arrowhead = none ];
684 -> 358;

685 [label="EVAL with clause\np(s(X184), X184).\nand substitutionX184 -> T80,\nT77 -> s(T80),\nX171 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
358 -> 685 [arrowhead = none ];
685 -> 360;

686 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
358 -> 686 [arrowhead = none ];
686 -> 362;

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

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

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

690 [label="EVAL with clause\ng(c(X191, 0)).\nand substitutionX191 -> s(s(s(s(s(s(0)))))),\nT80 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
370 -> 690 [arrowhead = none ];
690 -> 372;

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

692 [label="ONLY EVAL with clause\ng(c(X198, X199)) :- ','(no(zero(X199)), ','(p(X199, X200), g(c(s(X198), X200)))).\nand substitutionX198 -> s(s(s(s(s(s(0)))))),\nT80 -> T83,\nX199 -> T83", fontsize=14, style = filled, fillcolor = lightblue];
371 -> 692 [arrowhead = none ];
692 -> 375;

693 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
372 -> 693 [arrowhead = none ];
693 -> 374;

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

695 [label="ONLY EVAL with clause\nno(X204) :- ','(call(X204), ','(!_40, failure(a))).\nand substitutionT83 -> T86,\nX204 -> zero(T86)", fontsize=14, style = filled, fillcolor = lightblue];
376 -> 695 [arrowhead = none ];
695 -> 377;

696 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
377 -> 696 [arrowhead = none ];
696 -> 379;

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

698 [label="EVAL with clause\nzero(0).\nand substitutionT86 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
382 -> 698 [arrowhead = none ];
698 -> 383;

699 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
382 -> 699 [arrowhead = none ];
699 -> 384;

700 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
383 -> 700 [arrowhead = none ];
700 -> 385;

701 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
384 -> 701 [arrowhead = none ];
701 -> 389;

702 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
385 -> 702 [arrowhead = none ];
702 -> 386;

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

704 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
389 -> 704 [arrowhead = none ];
704 -> 390;

705 [label="ONLY EVAL with clause\nno(X209).\nand substitutionT86 -> T89,\nX209 -> zero(T89)", fontsize=14, style = filled, fillcolor = lightblue];
390 -> 705 [arrowhead = none ];
705 -> 392;

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

707 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T89), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
394 -> 707 [arrowhead = none ];
707 -> 396;

708 [label="EVAL with clause\np(s(X213), X213).\nand substitutionX213 -> T92,\nT89 -> s(T92),\nX200 -> T92", fontsize=14, style = filled, fillcolor = lightblue];
396 -> 708 [arrowhead = none ];
708 -> 399;

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

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

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

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

713 [label="EVAL with clause\ng(c(X220, 0)).\nand substitutionX220 -> s(s(s(s(s(s(s(0))))))),\nT92 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
409 -> 713 [arrowhead = none ];
713 -> 411;

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

715 [label="ONLY EVAL with clause\ng(c(X227, X228)) :- ','(no(zero(X228)), ','(p(X228, X229), g(c(s(X227), X229)))).\nand substitutionX227 -> s(s(s(s(s(s(s(0))))))),\nT92 -> T95,\nX228 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
410 -> 715 [arrowhead = none ];
715 -> 414;

716 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
411 -> 716 [arrowhead = none ];
716 -> 413;

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

718 [label="ONLY EVAL with clause\nno(X233) :- ','(call(X233), ','(!_46, failure(a))).\nand substitutionT95 -> T98,\nX233 -> zero(T98)", fontsize=14, style = filled, fillcolor = lightblue];
415 -> 718 [arrowhead = none ];
718 -> 416;

719 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
416 -> 719 [arrowhead = none ];
719 -> 417;

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

721 [label="EVAL with clause\nzero(0).\nand substitutionT98 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
418 -> 721 [arrowhead = none ];
721 -> 419;

722 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
418 -> 722 [arrowhead = none ];
722 -> 420;

723 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
419 -> 723 [arrowhead = none ];
723 -> 421;

724 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
420 -> 724 [arrowhead = none ];
724 -> 425;

725 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
421 -> 725 [arrowhead = none ];
725 -> 422;

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

727 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
425 -> 727 [arrowhead = none ];
727 -> 427;

728 [label="ONLY EVAL with clause\nno(X238).\nand substitutionT98 -> T101,\nX238 -> zero(T101)", fontsize=14, style = filled, fillcolor = lightblue];
427 -> 728 [arrowhead = none ];
728 -> 430;

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

730 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T101), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
431 -> 730 [arrowhead = none ];
730 -> 432;

731 [label="EVAL with clause\np(s(X242), X242).\nand substitutionX242 -> T104,\nT101 -> s(T104),\nX229 -> T104", fontsize=14, style = filled, fillcolor = lightblue];
432 -> 731 [arrowhead = none ];
731 -> 433;

732 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
432 -> 732 [arrowhead = none ];
732 -> 434;

733 [label="GENERALIZATION\nT105 <-- s(s(s(s(s(s(s(0)))))))\n\nNew Knowledge:\nT105 is ground", fontsize=14, style = filled, fillcolor = violet];
433 -> 733 [arrowhead = none ];
733 -> 441;

734 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
441 -> 734 [arrowhead = none ];
734 -> 442;

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

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

737 [label="EVAL with clause\ng(c(X251, 0)).\nand substitutionT105 -> T112,\nX251 -> s(T112),\nT104 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
443 -> 737 [arrowhead = none ];
737 -> 445;

738 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
443 -> 738 [arrowhead = none ];
738 -> 446;

739 [label="ONLY EVAL with clause\ng(c(X258, X259)) :- ','(no(zero(X259)), ','(p(X259, X260), g(c(s(X258), X260)))).\nand substitutionT105 -> T118,\nX258 -> s(T118),\nT104 -> T119,\nX259 -> T119", fontsize=14, style = filled, fillcolor = lightblue];
444 -> 739 [arrowhead = none ];
739 -> 448;

740 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
445 -> 740 [arrowhead = none ];
740 -> 447;

741 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
448 -> 741 [arrowhead = none ];
741 -> 449;

742 [label="ONLY EVAL with clause\nno(X264) :- ','(call(X264), ','(!_52, failure(a))).\nand substitutionT119 -> T123,\nX264 -> zero(T123)", fontsize=14, style = filled, fillcolor = lightblue];
449 -> 742 [arrowhead = none ];
742 -> 450;

743 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
450 -> 743 [arrowhead = none ];
743 -> 451;

744 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
451 -> 744 [arrowhead = none ];
744 -> 452;

745 [label="EVAL with clause\nzero(0).\nand substitutionT123 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
452 -> 745 [arrowhead = none ];
745 -> 453;

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

747 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
453 -> 747 [arrowhead = none ];
747 -> 455;

748 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
454 -> 748 [arrowhead = none ];
748 -> 459;

749 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
455 -> 749 [arrowhead = none ];
749 -> 457;

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

751 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
459 -> 751 [arrowhead = none ];
751 -> 460;

752 [label="ONLY EVAL with clause\nno(X269).\nand substitutionT123 -> T128,\nX269 -> zero(T128)", fontsize=14, style = filled, fillcolor = lightblue];
460 -> 752 [arrowhead = none ];
752 -> 463;

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

754 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T128), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
466 -> 754 [arrowhead = none ];
754 -> 467;

755 [label="EVAL with clause\np(s(X273), X273).\nand substitutionX273 -> T132,\nT128 -> s(T132),\nX260 -> T132", fontsize=14, style = filled, fillcolor = lightblue];
467 -> 755 [arrowhead = none ];
755 -> 472;

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

757 [label="INSTANCE with matching:\nT105 -> s(T118)\nT104 -> T132", fontsize=14, style = filled, fillcolor = lightgrey];
472 -> 757 [arrowhead = none , style=dashed];
757 -> 441[style=dashed];

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

759 [label="ONLY EVAL with clause\nno(X289) :- ','(call(X289), ','(!_57, failure(a))).\nand substitutionT139 -> T146,\nX289 -> zero(T146)", fontsize=14, style = filled, fillcolor = lightblue];
484 -> 759 [arrowhead = none ];
759 -> 485;

760 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
485 -> 760 [arrowhead = none ];
760 -> 486;

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

762 [label="EVAL with clause\nzero(0).\nand substitutionT146 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
487 -> 762 [arrowhead = none ];
762 -> 488;

763 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
487 -> 763 [arrowhead = none ];
763 -> 489;

764 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
488 -> 764 [arrowhead = none ];
764 -> 490;

765 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
489 -> 765 [arrowhead = none ];
765 -> 493;

766 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
490 -> 766 [arrowhead = none ];
766 -> 491;

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

768 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
493 -> 768 [arrowhead = none ];
768 -> 494;

769 [label="ONLY EVAL with clause\nno(X298).\nand substitutionT146 -> T153,\nX298 -> zero(T153)", fontsize=14, style = filled, fillcolor = lightblue];
494 -> 769 [arrowhead = none ];
769 -> 495;

770 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
495 -> 770 [arrowhead = none ];
770 -> 496;

771 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T153), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
496 -> 771 [arrowhead = none ];
771 -> 497;

772 [label="EVAL with clause\np(s(X304), X304).\nand substitutionX304 -> T159,\nT153 -> s(T159),\nX283 -> T159", fontsize=14, style = filled, fillcolor = lightblue];
497 -> 772 [arrowhead = none ];
772 -> 498;

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

774 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
498 -> 774 [arrowhead = none ];
774 -> 507;

775 [label="SPLIT 2\nnew knowledge:\nT159 is ground\nT140 is ground", fontsize=14, style = filled, fillcolor = violet];
498 -> 775 [arrowhead = none ];
775 -> 508;

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

777 [label="INSTANCE with matching:\nT105 -> T159\nT104 -> T140", fontsize=14, style = filled, fillcolor = lightgrey];
508 -> 777 [arrowhead = none , style=dashed];
777 -> 441[style=dashed];

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

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

780 [label="EVAL with clause\nf(c(0, X313)).\nand substitutionT159 -> 0,\nT140 -> T168,\nX313 -> s(T168)", fontsize=14, style = filled, fillcolor = lightblue];
510 -> 780 [arrowhead = none ];
780 -> 512;

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

782 [label="ONLY EVAL with clause\nf(c(X320, X321)) :- ','(no(zero(X320)), ','(p(X320, X322), f(c(X322, s(X321))))).\nand substitutionT159 -> T174,\nX320 -> T174,\nT140 -> T175,\nX321 -> s(T175)", fontsize=14, style = filled, fillcolor = lightblue];
511 -> 782 [arrowhead = none ];
782 -> 515;

783 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
512 -> 783 [arrowhead = none ];
783 -> 514;

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

785 [label="ONLY EVAL with clause\nno(X326) :- ','(call(X326), ','(!_63, failure(a))).\nand substitutionT174 -> T179,\nX326 -> zero(T179)", fontsize=14, style = filled, fillcolor = lightblue];
516 -> 785 [arrowhead = none ];
785 -> 517;

786 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
517 -> 786 [arrowhead = none ];
786 -> 518;

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

788 [label="EVAL with clause\nzero(0).\nand substitutionT179 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
519 -> 788 [arrowhead = none ];
788 -> 520;

789 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
519 -> 789 [arrowhead = none ];
789 -> 521;

790 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
520 -> 790 [arrowhead = none ];
790 -> 522;

791 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
521 -> 791 [arrowhead = none ];
791 -> 525;

792 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
522 -> 792 [arrowhead = none ];
792 -> 523;

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

794 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
525 -> 794 [arrowhead = none ];
794 -> 526;

795 [label="ONLY EVAL with clause\nno(X331).\nand substitutionT179 -> T184,\nX331 -> zero(T184)", fontsize=14, style = filled, fillcolor = lightblue];
526 -> 795 [arrowhead = none ];
795 -> 529;

796 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
529 -> 796 [arrowhead = none ];
796 -> 530;

797 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T184), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
530 -> 797 [arrowhead = none ];
797 -> 532;

798 [label="EVAL with clause\np(s(X335), X335).\nand substitutionX335 -> T188,\nT184 -> s(T188),\nX322 -> T188", fontsize=14, style = filled, fillcolor = lightblue];
532 -> 798 [arrowhead = none ];
798 -> 538;

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

800 [label="INSTANCE with matching:\nT159 -> T188\nT140 -> s(T175)", fontsize=14, style = filled, fillcolor = lightgrey];
538 -> 800 [arrowhead = none , style=dashed];
800 -> 507[style=dashed];

}

(2) Obligation:

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

hA_in_g(c(0, 0)) → hA_out_g(c(0, 0))
hA_in_g(c(0, s(0))) → hA_out_g(c(0, s(0)))
hA_in_g(c(0, s(s(0)))) → hA_out_g(c(0, s(s(0))))
hA_in_g(c(0, s(s(s(0))))) → hA_out_g(c(0, s(s(s(0)))))
hA_in_g(c(0, s(s(s(s(0)))))) → hA_out_g(c(0, s(s(s(s(0))))))
hA_in_g(c(0, s(s(s(s(s(0))))))) → hA_out_g(c(0, s(s(s(s(s(0)))))))
hA_in_g(c(0, s(s(s(s(s(s(0)))))))) → hA_out_g(c(0, s(s(s(s(s(s(0))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hA_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → U1_g(T104, gB_in_gg(s(s(s(s(s(s(s(0))))))), T104))
gB_in_gg(T112, 0) → gB_out_gg(T112, 0)
gB_in_gg(T118, s(T132)) → U3_gg(T118, T132, gB_in_gg(s(T118), T132))
U3_gg(T118, T132, gB_out_gg(s(T118), T132)) → gB_out_gg(T118, s(T132))
U1_g(T104, gB_out_gg(s(s(s(s(s(s(s(0))))))), T104)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T104))))))))))
hA_in_g(c(s(T159), T140)) → U2_g(T159, T140, pC_in_gg(T159, T140))
pC_in_gg(T159, T140) → U5_gg(T159, T140, fD_in_gg(T159, T140))
fD_in_gg(0, T168) → fD_out_gg(0, T168)
fD_in_gg(s(T188), T175) → U4_gg(T188, T175, fD_in_gg(T188, s(T175)))
U4_gg(T188, T175, fD_out_gg(T188, s(T175))) → fD_out_gg(s(T188), T175)
U5_gg(T159, T140, fD_out_gg(T159, T140)) → U6_gg(T159, T140, gB_in_gg(T159, T140))
U6_gg(T159, T140, gB_out_gg(T159, T140)) → pC_out_gg(T159, T140)
U2_g(T159, T140, pC_out_gg(T159, T140)) → hA_out_g(c(s(T159), T140))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

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

HA_IN_G(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → U1_G(T104, gB_in_gg(s(s(s(s(s(s(s(0))))))), T104))
HA_IN_G(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → GB_IN_GG(s(s(s(s(s(s(s(0))))))), T104)
GB_IN_GG(T118, s(T132)) → U3_GG(T118, T132, gB_in_gg(s(T118), T132))
GB_IN_GG(T118, s(T132)) → GB_IN_GG(s(T118), T132)
HA_IN_G(c(s(T159), T140)) → U2_G(T159, T140, pC_in_gg(T159, T140))
HA_IN_G(c(s(T159), T140)) → PC_IN_GG(T159, T140)
PC_IN_GG(T159, T140) → U5_GG(T159, T140, fD_in_gg(T159, T140))
PC_IN_GG(T159, T140) → FD_IN_GG(T159, T140)
FD_IN_GG(s(T188), T175) → U4_GG(T188, T175, fD_in_gg(T188, s(T175)))
FD_IN_GG(s(T188), T175) → FD_IN_GG(T188, s(T175))
U5_GG(T159, T140, fD_out_gg(T159, T140)) → U6_GG(T159, T140, gB_in_gg(T159, T140))
U5_GG(T159, T140, fD_out_gg(T159, T140)) → GB_IN_GG(T159, T140)

The TRS R consists of the following rules:

hA_in_g(c(0, 0)) → hA_out_g(c(0, 0))
hA_in_g(c(0, s(0))) → hA_out_g(c(0, s(0)))
hA_in_g(c(0, s(s(0)))) → hA_out_g(c(0, s(s(0))))
hA_in_g(c(0, s(s(s(0))))) → hA_out_g(c(0, s(s(s(0)))))
hA_in_g(c(0, s(s(s(s(0)))))) → hA_out_g(c(0, s(s(s(s(0))))))
hA_in_g(c(0, s(s(s(s(s(0))))))) → hA_out_g(c(0, s(s(s(s(s(0)))))))
hA_in_g(c(0, s(s(s(s(s(s(0)))))))) → hA_out_g(c(0, s(s(s(s(s(s(0))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hA_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → U1_g(T104, gB_in_gg(s(s(s(s(s(s(s(0))))))), T104))
gB_in_gg(T112, 0) → gB_out_gg(T112, 0)
gB_in_gg(T118, s(T132)) → U3_gg(T118, T132, gB_in_gg(s(T118), T132))
U3_gg(T118, T132, gB_out_gg(s(T118), T132)) → gB_out_gg(T118, s(T132))
U1_g(T104, gB_out_gg(s(s(s(s(s(s(s(0))))))), T104)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T104))))))))))
hA_in_g(c(s(T159), T140)) → U2_g(T159, T140, pC_in_gg(T159, T140))
pC_in_gg(T159, T140) → U5_gg(T159, T140, fD_in_gg(T159, T140))
fD_in_gg(0, T168) → fD_out_gg(0, T168)
fD_in_gg(s(T188), T175) → U4_gg(T188, T175, fD_in_gg(T188, s(T175)))
U4_gg(T188, T175, fD_out_gg(T188, s(T175))) → fD_out_gg(s(T188), T175)
U5_gg(T159, T140, fD_out_gg(T159, T140)) → U6_gg(T159, T140, gB_in_gg(T159, T140))
U6_gg(T159, T140, gB_out_gg(T159, T140)) → pC_out_gg(T159, T140)
U2_g(T159, T140, pC_out_gg(T159, T140)) → hA_out_g(c(s(T159), T140))

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

(4) Obligation:

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

HA_IN_G(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → U1_G(T104, gB_in_gg(s(s(s(s(s(s(s(0))))))), T104))
HA_IN_G(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → GB_IN_GG(s(s(s(s(s(s(s(0))))))), T104)
GB_IN_GG(T118, s(T132)) → U3_GG(T118, T132, gB_in_gg(s(T118), T132))
GB_IN_GG(T118, s(T132)) → GB_IN_GG(s(T118), T132)
HA_IN_G(c(s(T159), T140)) → U2_G(T159, T140, pC_in_gg(T159, T140))
HA_IN_G(c(s(T159), T140)) → PC_IN_GG(T159, T140)
PC_IN_GG(T159, T140) → U5_GG(T159, T140, fD_in_gg(T159, T140))
PC_IN_GG(T159, T140) → FD_IN_GG(T159, T140)
FD_IN_GG(s(T188), T175) → U4_GG(T188, T175, fD_in_gg(T188, s(T175)))
FD_IN_GG(s(T188), T175) → FD_IN_GG(T188, s(T175))
U5_GG(T159, T140, fD_out_gg(T159, T140)) → U6_GG(T159, T140, gB_in_gg(T159, T140))
U5_GG(T159, T140, fD_out_gg(T159, T140)) → GB_IN_GG(T159, T140)

The TRS R consists of the following rules:

hA_in_g(c(0, 0)) → hA_out_g(c(0, 0))
hA_in_g(c(0, s(0))) → hA_out_g(c(0, s(0)))
hA_in_g(c(0, s(s(0)))) → hA_out_g(c(0, s(s(0))))
hA_in_g(c(0, s(s(s(0))))) → hA_out_g(c(0, s(s(s(0)))))
hA_in_g(c(0, s(s(s(s(0)))))) → hA_out_g(c(0, s(s(s(s(0))))))
hA_in_g(c(0, s(s(s(s(s(0))))))) → hA_out_g(c(0, s(s(s(s(s(0)))))))
hA_in_g(c(0, s(s(s(s(s(s(0)))))))) → hA_out_g(c(0, s(s(s(s(s(s(0))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hA_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → U1_g(T104, gB_in_gg(s(s(s(s(s(s(s(0))))))), T104))
gB_in_gg(T112, 0) → gB_out_gg(T112, 0)
gB_in_gg(T118, s(T132)) → U3_gg(T118, T132, gB_in_gg(s(T118), T132))
U3_gg(T118, T132, gB_out_gg(s(T118), T132)) → gB_out_gg(T118, s(T132))
U1_g(T104, gB_out_gg(s(s(s(s(s(s(s(0))))))), T104)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T104))))))))))
hA_in_g(c(s(T159), T140)) → U2_g(T159, T140, pC_in_gg(T159, T140))
pC_in_gg(T159, T140) → U5_gg(T159, T140, fD_in_gg(T159, T140))
fD_in_gg(0, T168) → fD_out_gg(0, T168)
fD_in_gg(s(T188), T175) → U4_gg(T188, T175, fD_in_gg(T188, s(T175)))
U4_gg(T188, T175, fD_out_gg(T188, s(T175))) → fD_out_gg(s(T188), T175)
U5_gg(T159, T140, fD_out_gg(T159, T140)) → U6_gg(T159, T140, gB_in_gg(T159, T140))
U6_gg(T159, T140, gB_out_gg(T159, T140)) → pC_out_gg(T159, T140)
U2_g(T159, T140, pC_out_gg(T159, T140)) → hA_out_g(c(s(T159), T140))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

FD_IN_GG(s(T188), T175) → FD_IN_GG(T188, s(T175))

The TRS R consists of the following rules:

hA_in_g(c(0, 0)) → hA_out_g(c(0, 0))
hA_in_g(c(0, s(0))) → hA_out_g(c(0, s(0)))
hA_in_g(c(0, s(s(0)))) → hA_out_g(c(0, s(s(0))))
hA_in_g(c(0, s(s(s(0))))) → hA_out_g(c(0, s(s(s(0)))))
hA_in_g(c(0, s(s(s(s(0)))))) → hA_out_g(c(0, s(s(s(s(0))))))
hA_in_g(c(0, s(s(s(s(s(0))))))) → hA_out_g(c(0, s(s(s(s(s(0)))))))
hA_in_g(c(0, s(s(s(s(s(s(0)))))))) → hA_out_g(c(0, s(s(s(s(s(s(0))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hA_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → U1_g(T104, gB_in_gg(s(s(s(s(s(s(s(0))))))), T104))
gB_in_gg(T112, 0) → gB_out_gg(T112, 0)
gB_in_gg(T118, s(T132)) → U3_gg(T118, T132, gB_in_gg(s(T118), T132))
U3_gg(T118, T132, gB_out_gg(s(T118), T132)) → gB_out_gg(T118, s(T132))
U1_g(T104, gB_out_gg(s(s(s(s(s(s(s(0))))))), T104)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T104))))))))))
hA_in_g(c(s(T159), T140)) → U2_g(T159, T140, pC_in_gg(T159, T140))
pC_in_gg(T159, T140) → U5_gg(T159, T140, fD_in_gg(T159, T140))
fD_in_gg(0, T168) → fD_out_gg(0, T168)
fD_in_gg(s(T188), T175) → U4_gg(T188, T175, fD_in_gg(T188, s(T175)))
U4_gg(T188, T175, fD_out_gg(T188, s(T175))) → fD_out_gg(s(T188), T175)
U5_gg(T159, T140, fD_out_gg(T159, T140)) → U6_gg(T159, T140, gB_in_gg(T159, T140))
U6_gg(T159, T140, gB_out_gg(T159, T140)) → pC_out_gg(T159, T140)
U2_g(T159, T140, pC_out_gg(T159, T140)) → hA_out_g(c(s(T159), T140))

Pi is empty.
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:

FD_IN_GG(s(T188), T175) → FD_IN_GG(T188, s(T175))

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:

FD_IN_GG(s(T188), T175) → FD_IN_GG(T188, s(T175))

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:

FD_IN_GG(s(T188), T175) → FD_IN_GG(T188, s(T175))
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

GB_IN_GG(T118, s(T132)) → GB_IN_GG(s(T118), T132)

The TRS R consists of the following rules:

hA_in_g(c(0, 0)) → hA_out_g(c(0, 0))
hA_in_g(c(0, s(0))) → hA_out_g(c(0, s(0)))
hA_in_g(c(0, s(s(0)))) → hA_out_g(c(0, s(s(0))))
hA_in_g(c(0, s(s(s(0))))) → hA_out_g(c(0, s(s(s(0)))))
hA_in_g(c(0, s(s(s(s(0)))))) → hA_out_g(c(0, s(s(s(s(0))))))
hA_in_g(c(0, s(s(s(s(s(0))))))) → hA_out_g(c(0, s(s(s(s(s(0)))))))
hA_in_g(c(0, s(s(s(s(s(s(0)))))))) → hA_out_g(c(0, s(s(s(s(s(s(0))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(0))))))))) → hA_out_g(c(0, s(s(s(s(s(s(s(0)))))))))
hA_in_g(c(0, s(s(s(s(s(s(s(s(T104)))))))))) → U1_g(T104, gB_in_gg(s(s(s(s(s(s(s(0))))))), T104))
gB_in_gg(T112, 0) → gB_out_gg(T112, 0)
gB_in_gg(T118, s(T132)) → U3_gg(T118, T132, gB_in_gg(s(T118), T132))
U3_gg(T118, T132, gB_out_gg(s(T118), T132)) → gB_out_gg(T118, s(T132))
U1_g(T104, gB_out_gg(s(s(s(s(s(s(s(0))))))), T104)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T104))))))))))
hA_in_g(c(s(T159), T140)) → U2_g(T159, T140, pC_in_gg(T159, T140))
pC_in_gg(T159, T140) → U5_gg(T159, T140, fD_in_gg(T159, T140))
fD_in_gg(0, T168) → fD_out_gg(0, T168)
fD_in_gg(s(T188), T175) → U4_gg(T188, T175, fD_in_gg(T188, s(T175)))
U4_gg(T188, T175, fD_out_gg(T188, s(T175))) → fD_out_gg(s(T188), T175)
U5_gg(T159, T140, fD_out_gg(T159, T140)) → U6_gg(T159, T140, gB_in_gg(T159, T140))
U6_gg(T159, T140, gB_out_gg(T159, T140)) → pC_out_gg(T159, T140)
U2_g(T159, T140, pC_out_gg(T159, T140)) → hA_out_g(c(s(T159), T140))

Pi is empty.
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:

GB_IN_GG(T118, s(T132)) → GB_IN_GG(s(T118), T132)

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

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

GB_IN_GG(T118, s(T132)) → GB_IN_GG(s(T118), T132)

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:

GB_IN_GG(T118, s(T132)) → GB_IN_GG(s(T118), T132)
The graph contains the following edges 2 > 2

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (EQUIVALENT transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES