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

(0) Obligation:

Clauses:

h(X) :- ','(f(X), g(X)).
f(c(0, X1)) :- !.
f(c(X, Y)) :- ','(p(X, P), f(c(P, s(Y)))).
g(c(X2, 0)) :- !.
g(c(X, Y)) :- ','(p(Y, P), g(c(s(X), P))).
p(0, 0).
p(s(X), X).

Query: h(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [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];
11 [label="11: ','(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: ','(!_2, g(c(0, T6))) | ','(f(c(0, T6)), g(c(0, T6))), SCOPE: 2, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nX7 is free\nf(T3) !=? f(c(0, X7))", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: g(c(0, T6))\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: g(c(0, T6)), SCOPE: 3, CLAUSE: 3 | g(c(0, T6)), SCOPE: 3, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: !_3 | g(c(0, 0)), SCOPE: 3, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: g(c(0, T6)), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX11 is free\ng(c(0, T6)) !=? g(c(X11, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(p(T9, X20), g(c(s(0), X20)))\n\nT9 is ground\nX11 is free\nX20 is free\ng(c(0, T9)) !=? g(c(X11, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(p(T9, X20), g(c(s(0), X20))), SCOPE: 4, CLAUSE: 5 | ','(p(T9, X20), g(c(s(0), X20))), SCOPE: 4, CLAUSE: 6\n\nT9 is ground\nX11 is free\nX20 is free\ng(c(0, T9)) !=? g(c(X11, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(p(T9, X20), g(c(s(0), X20))), SCOPE: 4, CLAUSE: 6\n\nT9 is ground\nX11 is free\nX20 is free\ng(c(0, T9)) !=? g(c(X11, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: g(c(s(0), T12))\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: g(c(s(0), T12)), SCOPE: 5, CLAUSE: 3 | g(c(s(0), T12)), SCOPE: 5, CLAUSE: 4\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: !_5 | g(c(s(0), 0)), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: g(c(s(0), T12)), SCOPE: 5, CLAUSE: 4\n\nT12 is ground\nX28 is free\ng(c(s(0), T12)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(p(T15, X37), g(c(s(s(0)), X37)))\n\nT15 is ground\nX28 is free\nX37 is free\ng(c(s(0), T15)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(p(T15, X37), g(c(s(s(0)), X37))), SCOPE: 6, CLAUSE: 5 | ','(p(T15, X37), g(c(s(s(0)), X37))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX28 is free\nX37 is free\ng(c(s(0), T15)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(p(T15, X37), g(c(s(s(0)), X37))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX28 is free\nX37 is free\ng(c(s(0), T15)) !=? g(c(X28, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: g(c(s(s(0)), T18))\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: g(c(s(s(0)), T18)), SCOPE: 7, CLAUSE: 3 | g(c(s(s(0)), T18)), SCOPE: 7, CLAUSE: 4\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: !_7 | g(c(s(s(0)), 0)), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: g(c(s(s(0)), T18)), SCOPE: 7, CLAUSE: 4\n\nT18 is ground\nX45 is free\ng(c(s(s(0)), T18)) !=? g(c(X45, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(p(T21, X54), g(c(s(s(s(0))), X54)))\n\nT21 is ground\nX45 is free\nX54 is free\ng(c(s(s(0)), T21)) !=? g(c(X45, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(p(T21, X54), g(c(s(s(s(0))), X54))), SCOPE: 8, CLAUSE: 5 | ','(p(T21, X54), g(c(s(s(s(0))), X54))), SCOPE: 8, CLAUSE: 6\n\nT21 is ground\nX45 is free\nX54 is free\ng(c(s(s(0)), T21)) !=? g(c(X45, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(p(T21, X54), g(c(s(s(s(0))), X54))), SCOPE: 8, CLAUSE: 6\n\nT21 is ground\nX45 is free\nX54 is free\ng(c(s(s(0)), T21)) !=? g(c(X45, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: g(c(s(s(s(0))), T24))\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: g(c(s(s(s(0))), T24)), SCOPE: 9, CLAUSE: 3 | g(c(s(s(s(0))), T24)), SCOPE: 9, CLAUSE: 4\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: !_9 | g(c(s(s(s(0))), 0)), SCOPE: 9, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: g(c(s(s(s(0))), T24)), SCOPE: 9, CLAUSE: 4\n\nT24 is ground\nX62 is free\ng(c(s(s(s(0))), T24)) !=? g(c(X62, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(p(T27, X71), g(c(s(s(s(s(0)))), X71)))\n\nT27 is ground\nX62 is free\nX71 is free\ng(c(s(s(s(0))), T27)) !=? g(c(X62, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(p(T27, X71), g(c(s(s(s(s(0)))), X71))), SCOPE: 10, CLAUSE: 5 | ','(p(T27, X71), g(c(s(s(s(s(0)))), X71))), SCOPE: 10, CLAUSE: 6\n\nT27 is ground\nX62 is free\nX71 is free\ng(c(s(s(s(0))), T27)) !=? g(c(X62, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(p(T27, X71), g(c(s(s(s(s(0)))), X71))), SCOPE: 10, CLAUSE: 6\n\nT27 is ground\nX62 is free\nX71 is free\ng(c(s(s(s(0))), T27)) !=? g(c(X62, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: g(c(s(s(s(s(0)))), T30))\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: g(c(s(s(s(s(0)))), T30)), SCOPE: 11, CLAUSE: 3 | g(c(s(s(s(s(0)))), T30)), SCOPE: 11, CLAUSE: 4\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: !_11 | g(c(s(s(s(s(0)))), 0)), SCOPE: 11, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: g(c(s(s(s(s(0)))), T30)), SCOPE: 11, CLAUSE: 4\n\nT30 is ground\nX79 is free\ng(c(s(s(s(s(0)))), T30)) !=? g(c(X79, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(p(T33, X88), g(c(s(s(s(s(s(0))))), X88)))\n\nT33 is ground\nX79 is free\nX88 is free\ng(c(s(s(s(s(0)))), T33)) !=? g(c(X79, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(p(T33, X88), g(c(s(s(s(s(s(0))))), X88))), SCOPE: 12, CLAUSE: 5 | ','(p(T33, X88), g(c(s(s(s(s(s(0))))), X88))), SCOPE: 12, CLAUSE: 6\n\nT33 is ground\nX79 is free\nX88 is free\ng(c(s(s(s(s(0)))), T33)) !=? g(c(X79, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(p(T33, X88), g(c(s(s(s(s(s(0))))), X88))), SCOPE: 12, CLAUSE: 6\n\nT33 is ground\nX79 is free\nX88 is free\ng(c(s(s(s(s(0)))), T33)) !=? g(c(X79, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: g(c(s(s(s(s(s(0))))), T36))\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: g(c(s(s(s(s(s(0))))), T36)), SCOPE: 13, CLAUSE: 3 | g(c(s(s(s(s(s(0))))), T36)), SCOPE: 13, CLAUSE: 4\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: !_13 | g(c(s(s(s(s(s(0))))), 0)), SCOPE: 13, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: g(c(s(s(s(s(s(0))))), T36)), SCOPE: 13, CLAUSE: 4\n\nT36 is ground\nX96 is free\ng(c(s(s(s(s(s(0))))), T36)) !=? g(c(X96, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(p(T39, X105), g(c(s(s(s(s(s(s(0)))))), X105)))\n\nT39 is ground\nX96 is free\nX105 is free\ng(c(s(s(s(s(s(0))))), T39)) !=? g(c(X96, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(p(T39, X105), g(c(s(s(s(s(s(s(0)))))), X105))), SCOPE: 14, CLAUSE: 5 | ','(p(T39, X105), g(c(s(s(s(s(s(s(0)))))), X105))), SCOPE: 14, CLAUSE: 6\n\nT39 is ground\nX96 is free\nX105 is free\ng(c(s(s(s(s(s(0))))), T39)) !=? g(c(X96, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(p(T39, X105), g(c(s(s(s(s(s(s(0)))))), X105))), SCOPE: 14, CLAUSE: 6\n\nT39 is ground\nX96 is free\nX105 is free\ng(c(s(s(s(s(s(0))))), T39)) !=? g(c(X96, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: g(c(s(s(s(s(s(s(0)))))), T42))\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: g(c(s(s(s(s(s(s(0)))))), T42)), SCOPE: 15, CLAUSE: 3 | g(c(s(s(s(s(s(s(0)))))), T42)), SCOPE: 15, CLAUSE: 4\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: !_15 | g(c(s(s(s(s(s(s(0)))))), 0)), SCOPE: 15, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: g(c(s(s(s(s(s(s(0)))))), T42)), SCOPE: 15, CLAUSE: 4\n\nT42 is ground\nX113 is free\ng(c(s(s(s(s(s(s(0)))))), T42)) !=? g(c(X113, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(p(T45, X122), g(c(s(s(s(s(s(s(s(0))))))), X122)))\n\nT45 is ground\nX113 is free\nX122 is free\ng(c(s(s(s(s(s(s(0)))))), T45)) !=? g(c(X113, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(p(T45, X122), g(c(s(s(s(s(s(s(s(0))))))), X122))), SCOPE: 16, CLAUSE: 5 | ','(p(T45, X122), g(c(s(s(s(s(s(s(s(0))))))), X122))), SCOPE: 16, CLAUSE: 6\n\nT45 is ground\nX113 is free\nX122 is free\ng(c(s(s(s(s(s(s(0)))))), T45)) !=? g(c(X113, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(p(T45, X122), g(c(s(s(s(s(s(s(s(0))))))), X122))), SCOPE: 16, CLAUSE: 6\n\nT45 is ground\nX113 is free\nX122 is free\ng(c(s(s(s(s(s(s(0)))))), T45)) !=? g(c(X113, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: g(c(s(s(s(s(s(s(s(0))))))), T48))\n\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: g(c(s(s(s(s(s(s(s(0))))))), T48)), SCOPE: 17, CLAUSE: 3 | g(c(s(s(s(s(s(s(s(0))))))), T48)), SCOPE: 17, CLAUSE: 4\n\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: !_17 | g(c(s(s(s(s(s(s(s(0))))))), 0)), SCOPE: 17, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: g(c(s(s(s(s(s(s(s(0))))))), T48)), SCOPE: 17, CLAUSE: 4\n\nT48 is ground\nX130 is free\ng(c(s(s(s(s(s(s(s(0))))))), T48)) !=? g(c(X130, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(p(T51, X139), g(c(s(s(s(s(s(s(s(s(0)))))))), X139)))\n\nT51 is ground\nX130 is free\nX139 is free\ng(c(s(s(s(s(s(s(s(0))))))), T51)) !=? g(c(X130, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(p(T51, X139), g(c(s(s(s(s(s(s(s(s(0)))))))), X139))), SCOPE: 18, CLAUSE: 5 | ','(p(T51, X139), g(c(s(s(s(s(s(s(s(s(0)))))))), X139))), SCOPE: 18, CLAUSE: 6\n\nT51 is ground\nX130 is free\nX139 is free\ng(c(s(s(s(s(s(s(s(0))))))), T51)) !=? g(c(X130, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(p(T51, X139), g(c(s(s(s(s(s(s(s(s(0)))))))), X139))), SCOPE: 18, CLAUSE: 6\n\nT51 is ground\nX130 is free\nX139 is free\ng(c(s(s(s(s(s(s(s(0))))))), T51)) !=? g(c(X130, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: g(c(s(s(s(s(s(s(s(s(0)))))))), T54))\n\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="B: g(c(s(T55), T54))\n\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: g(c(s(T55), T54)), SCOPE: 19, CLAUSE: 3 | g(c(s(T55), T54)), SCOPE: 19, CLAUSE: 4\n\nT54 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: !_19 | g(c(s(T59), 0)), SCOPE: 19, CLAUSE: 4\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: g(c(s(T55), T54)), SCOPE: 19, CLAUSE: 4\n\nT54 is ground\nT55 is ground\nX148 is free\ng(c(s(T55), T54)) !=? g(c(X148, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: ','(p(T66, X157), g(c(s(s(T65)), X157)))\n\nT65 is ground\nT66 is ground\nX148 is free\nX157 is free\ng(c(s(T65), T66)) !=? g(c(X148, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: ','(p(T66, X157), g(c(s(s(T65)), X157))), SCOPE: 20, CLAUSE: 5 | ','(p(T66, X157), g(c(s(s(T65)), X157))), SCOPE: 20, CLAUSE: 6\n\nT65 is ground\nT66 is ground\nX148 is free\nX157 is free\ng(c(s(T65), T66)) !=? g(c(X148, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: ','(p(T66, X157), g(c(s(s(T65)), X157))), SCOPE: 20, CLAUSE: 6\n\nT65 is ground\nT66 is ground\nX148 is free\nX157 is free\ng(c(s(T65), T66)) !=? g(c(X148, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: g(c(s(s(T65)), T70))\n\nT65 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: ','(','(p(T76, X170), f(c(X170, s(T77)))), g(c(T76, T77)))\n\nT76 is ground\nT77 is ground\nX7 is free\nX170 is free\nf(c(T76, T77)) !=? f(c(0, X7))", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: ','(','(p(T76, X170), f(c(X170, s(T77)))), g(c(T76, T77))), SCOPE: 21, CLAUSE: 5 | ','(','(p(T76, X170), f(c(X170, s(T77)))), g(c(T76, T77))), SCOPE: 21, CLAUSE: 6\n\nT76 is ground\nT77 is ground\nX7 is free\nX170 is free\nf(c(T76, T77)) !=? f(c(0, X7))", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: ','(','(p(T76, X170), f(c(X170, s(T77)))), g(c(T76, T77))), SCOPE: 21, CLAUSE: 6\n\nT76 is ground\nT77 is ground\nX7 is free\nX170 is free\nf(c(T76, T77)) !=? f(c(0, X7))", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="C: ','(f(c(T81, s(T77))), g(c(s(T81), T77)))\n\nT77 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="D: f(c(T81, s(T77)))\n\nT77 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: g(c(s(T81), T77))\n\nT77 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: f(c(T81, s(T77))), SCOPE: 22, CLAUSE: 1 | f(c(T81, s(T77))), SCOPE: 22, CLAUSE: 2\n\nT77 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: !_22 | f(c(0, s(T86))), SCOPE: 22, CLAUSE: 2\n\nT86 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: f(c(T81, s(T77))), SCOPE: 22, CLAUSE: 2\n\nT77 is ground\nT81 is ground\nX179 is free\nf(c(T81, s(T77))) !=? f(c(0, X179))", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: ','(p(T92, X188), f(c(X188, s(s(T93)))))\n\nT92 is ground\nT93 is ground\nX179 is free\nX188 is free\nf(c(T92, s(T93))) !=? f(c(0, X179))", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: ','(p(T92, X188), f(c(X188, s(s(T93))))), SCOPE: 23, CLAUSE: 5 | ','(p(T92, X188), f(c(X188, s(s(T93))))), SCOPE: 23, CLAUSE: 6\n\nT92 is ground\nT93 is ground\nX179 is free\nX188 is free\nf(c(T92, s(T93))) !=? f(c(0, X179))", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: ','(p(T92, X188), f(c(X188, s(s(T93))))), SCOPE: 23, CLAUSE: 6\n\nT92 is ground\nT93 is ground\nX179 is free\nX188 is free\nf(c(T92, s(T93))) !=? f(c(0, X179))", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: f(c(T97, s(s(T93))))\n\nT93 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 280 [arrowhead = none ];
280 -> 6;

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

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

283 [label="EVAL with clause\nf(c(0, X7)) :- !_2.\nand substitutionX7 -> T6,\nT3 -> c(0, T6)", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 283 [arrowhead = none ];
283 -> 13;

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

285 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 285 [arrowhead = none ];
285 -> 16;

286 [label="EVAL with clause\nf(c(X168, X169)) :- ','(p(X168, X170), f(c(X170, s(X169)))).\nand substitutionX168 -> T76,\nX169 -> T77,\nT3 -> c(T76, T77)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 286 [arrowhead = none ];
286 -> 240;

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

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

289 [label="EVAL with clause\ng(c(X11, 0)) :- !_3.\nand substitutionX11 -> 0,\nT6 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 289 [arrowhead = none ];
289 -> 23;

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

291 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 291 [arrowhead = none ];
291 -> 28;

292 [label="ONLY EVAL with clause\ng(c(X18, X19)) :- ','(p(X19, X20), g(c(s(X18), X20))).\nand substitutionX18 -> 0,\nT6 -> T9,\nX19 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 292 [arrowhead = none ];
292 -> 36;

293 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 293 [arrowhead = none ];
293 -> 29;

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

295 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(0, T9)), g(c(X11, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 295 [arrowhead = none ];
295 -> 42;

296 [label="EVAL with clause\np(s(X24), X24).\nand substitutionX24 -> T12,\nT9 -> s(T12),\nX20 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 296 [arrowhead = none ];
296 -> 46;

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

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

299 [label="EVAL with clause\ng(c(X28, 0)) :- !_5.\nand substitutionX28 -> s(0),\nT12 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 299 [arrowhead = none ];
299 -> 54;

300 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 300 [arrowhead = none ];
300 -> 58;

301 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 301 [arrowhead = none ];
301 -> 59;

302 [label="ONLY EVAL with clause\ng(c(X35, X36)) :- ','(p(X36, X37), g(c(s(X35), X37))).\nand substitutionX35 -> s(0),\nT12 -> T15,\nX36 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 302 [arrowhead = none ];
302 -> 67;

303 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 303 [arrowhead = none ];
303 -> 60;

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

305 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(0), T15)), g(c(X28, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 305 [arrowhead = none ];
305 -> 71;

306 [label="EVAL with clause\np(s(X41), X41).\nand substitutionX41 -> T18,\nT15 -> s(T18),\nX37 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 306 [arrowhead = none ];
306 -> 76;

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

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

309 [label="EVAL with clause\ng(c(X45, 0)) :- !_7.\nand substitutionX45 -> s(s(0)),\nT18 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 309 [arrowhead = none ];
309 -> 84;

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

311 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 311 [arrowhead = none ];
311 -> 86;

312 [label="ONLY EVAL with clause\ng(c(X52, X53)) :- ','(p(X53, X54), g(c(s(X52), X54))).\nand substitutionX52 -> s(s(0)),\nT18 -> T21,\nX53 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 312 [arrowhead = none ];
312 -> 95;

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

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

315 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(0)), T21)), g(c(X45, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 315 [arrowhead = none ];
315 -> 98;

316 [label="EVAL with clause\np(s(X58), X58).\nand substitutionX58 -> T24,\nT21 -> s(T24),\nX54 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 316 [arrowhead = none ];
316 -> 100;

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

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

319 [label="EVAL with clause\ng(c(X62, 0)) :- !_9.\nand substitutionX62 -> s(s(s(0))),\nT24 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 319 [arrowhead = none ];
319 -> 111;

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

321 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 321 [arrowhead = none ];
321 -> 115;

322 [label="ONLY EVAL with clause\ng(c(X69, X70)) :- ','(p(X70, X71), g(c(s(X69), X71))).\nand substitutionX69 -> s(s(s(0))),\nT24 -> T27,\nX70 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 322 [arrowhead = none ];
322 -> 125;

323 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 323 [arrowhead = none ];
323 -> 116;

324 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
125 -> 324 [arrowhead = none ];
324 -> 128;

325 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(0))), T27)), g(c(X62, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 325 [arrowhead = none ];
325 -> 129;

326 [label="EVAL with clause\np(s(X75), X75).\nand substitutionX75 -> T30,\nT27 -> s(T30),\nX71 -> T30", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 326 [arrowhead = none ];
326 -> 131;

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

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

329 [label="EVAL with clause\ng(c(X79, 0)) :- !_11.\nand substitutionX79 -> s(s(s(s(0)))),\nT30 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 329 [arrowhead = none ];
329 -> 138;

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

331 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 331 [arrowhead = none ];
331 -> 140;

332 [label="ONLY EVAL with clause\ng(c(X86, X87)) :- ','(p(X87, X88), g(c(s(X86), X88))).\nand substitutionX86 -> s(s(s(s(0)))),\nT30 -> T33,\nX87 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 332 [arrowhead = none ];
332 -> 148;

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

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

335 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(0)))), T33)), g(c(X79, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
150 -> 335 [arrowhead = none ];
335 -> 154;

336 [label="EVAL with clause\np(s(X92), X92).\nand substitutionX92 -> T36,\nT33 -> s(T36),\nX88 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 336 [arrowhead = none ];
336 -> 155;

337 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 337 [arrowhead = none ];
337 -> 156;

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

339 [label="EVAL with clause\ng(c(X96, 0)) :- !_13.\nand substitutionX96 -> s(s(s(s(s(0))))),\nT36 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 339 [arrowhead = none ];
339 -> 158;

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

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

342 [label="ONLY EVAL with clause\ng(c(X103, X104)) :- ','(p(X104, X105), g(c(s(X103), X105))).\nand substitutionX103 -> s(s(s(s(s(0))))),\nT36 -> T39,\nX104 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
159 -> 342 [arrowhead = none ];
342 -> 166;

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

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

345 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(0))))), T39)), g(c(X96, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
168 -> 345 [arrowhead = none ];
345 -> 169;

346 [label="EVAL with clause\np(s(X109), X109).\nand substitutionX109 -> T42,\nT39 -> s(T42),\nX105 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 346 [arrowhead = none ];
346 -> 170;

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

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

349 [label="EVAL with clause\ng(c(X113, 0)) :- !_15.\nand substitutionX113 -> s(s(s(s(s(s(0)))))),\nT42 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 349 [arrowhead = none ];
349 -> 183;

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

351 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
183 -> 351 [arrowhead = none ];
351 -> 185;

352 [label="ONLY EVAL with clause\ng(c(X120, X121)) :- ','(p(X121, X122), g(c(s(X120), X122))).\nand substitutionX120 -> s(s(s(s(s(s(0)))))),\nT42 -> T45,\nX121 -> T45", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 352 [arrowhead = none ];
352 -> 188;

353 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
185 -> 353 [arrowhead = none ];
353 -> 186;

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

355 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(s(0)))))), T45)), g(c(X113, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
189 -> 355 [arrowhead = none ];
355 -> 190;

356 [label="EVAL with clause\np(s(X126), X126).\nand substitutionX126 -> T48,\nT45 -> s(T48),\nX122 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 356 [arrowhead = none ];
356 -> 191;

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

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

359 [label="EVAL with clause\ng(c(X130, 0)) :- !_17.\nand substitutionX130 -> s(s(s(s(s(s(s(0))))))),\nT48 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 359 [arrowhead = none ];
359 -> 197;

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

361 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 361 [arrowhead = none ];
361 -> 202;

362 [label="ONLY EVAL with clause\ng(c(X137, X138)) :- ','(p(X138, X139), g(c(s(X137), X139))).\nand substitutionX137 -> s(s(s(s(s(s(s(0))))))),\nT48 -> T51,\nX138 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 362 [arrowhead = none ];
362 -> 208;

363 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
202 -> 363 [arrowhead = none ];
363 -> 203;

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

365 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(s(s(0))))))), T51)), g(c(X130, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 365 [arrowhead = none ];
365 -> 210;

366 [label="EVAL with clause\np(s(X143), X143).\nand substitutionX143 -> T54,\nT51 -> s(T54),\nX139 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
210 -> 366 [arrowhead = none ];
366 -> 211;

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

368 [label="GENERALIZATION\nT55 <-- s(s(s(s(s(s(s(0)))))))\n\nNew Knowledge:\nT55 is ground", fontsize=14, style = filled, fillcolor = violet];
211 -> 368 [arrowhead = none ];
368 -> 215;

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

370 [label="EVAL with clause\ng(c(X148, 0)) :- !_19.\nand substitutionT55 -> T59,\nX148 -> s(T59),\nT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
218 -> 370 [arrowhead = none ];
370 -> 223;

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

372 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
223 -> 372 [arrowhead = none ];
372 -> 225;

373 [label="ONLY EVAL with clause\ng(c(X155, X156)) :- ','(p(X156, X157), g(c(s(X155), X157))).\nand substitutionT55 -> T65,\nX155 -> s(T65),\nT54 -> T66,\nX156 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 373 [arrowhead = none ];
373 -> 227;

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

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

376 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(T65), T66)), g(c(X148, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
228 -> 376 [arrowhead = none ];
376 -> 229;

377 [label="EVAL with clause\np(s(X161), X161).\nand substitutionX161 -> T70,\nT66 -> s(T70),\nX157 -> T70", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 377 [arrowhead = none ];
377 -> 230;

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

379 [label="INSTANCE with matching:\nT55 -> s(T65)\nT54 -> T70", fontsize=14, style = filled, fillcolor = lightgrey];
230 -> 379 [arrowhead = none , style=dashed];
379 -> 215[style=dashed];

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

381 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(c(T76, T77)), f(c(0, X7)))", fontsize=14, style = filled, fillcolor = lightgreen];
244 -> 381 [arrowhead = none ];
381 -> 245;

382 [label="EVAL with clause\np(s(X174), X174).\nand substitutionX174 -> T81,\nT76 -> s(T81),\nX170 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
245 -> 382 [arrowhead = none ];
382 -> 246;

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

384 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
246 -> 384 [arrowhead = none ];
384 -> 251;

385 [label="SPLIT 2\nnew knowledge:\nT81 is ground\nT77 is ground", fontsize=14, style = filled, fillcolor = violet];
246 -> 385 [arrowhead = none ];
385 -> 252;

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

387 [label="INSTANCE with matching:\nT55 -> T81\nT54 -> T77", fontsize=14, style = filled, fillcolor = lightgrey];
252 -> 387 [arrowhead = none , style=dashed];
387 -> 215[style=dashed];

388 [label="EVAL with clause\nf(c(0, X179)) :- !_22.\nand substitutionT81 -> 0,\nT77 -> T86,\nX179 -> s(T86)", fontsize=14, style = filled, fillcolor = lightblue];
253 -> 388 [arrowhead = none ];
388 -> 271;

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

390 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
271 -> 390 [arrowhead = none ];
390 -> 273;

391 [label="ONLY EVAL with clause\nf(c(X186, X187)) :- ','(p(X186, X188), f(c(X188, s(X187)))).\nand substitutionT81 -> T92,\nX186 -> T92,\nT77 -> T93,\nX187 -> s(T93)", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 391 [arrowhead = none ];
391 -> 275;

392 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
273 -> 392 [arrowhead = none ];
392 -> 274;

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

394 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(c(T92, s(T93))), f(c(0, X179)))", fontsize=14, style = filled, fillcolor = lightgreen];
276 -> 394 [arrowhead = none ];
394 -> 277;

395 [label="EVAL with clause\np(s(X192), X192).\nand substitutionX192 -> T97,\nT92 -> s(T97),\nX188 -> T97", fontsize=14, style = filled, fillcolor = lightblue];
277 -> 395 [arrowhead = none ];
395 -> 278;

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

397 [label="INSTANCE with matching:\nT81 -> T97\nT77 -> s(T93)", fontsize=14, style = filled, fillcolor = lightgrey];
278 -> 397 [arrowhead = none , style=dashed];
397 -> 251[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(T54)))))))))) → U1_g(T54, gB_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gB_in_gg(T59, 0) → gB_out_gg(T59, 0)
gB_in_gg(T65, s(T70)) → U3_gg(T65, T70, gB_in_gg(s(T65), T70))
U3_gg(T65, T70, gB_out_gg(s(T65), T70)) → gB_out_gg(T65, s(T70))
U1_g(T54, gB_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hA_in_g(c(s(T81), T77)) → U2_g(T81, T77, pC_in_gg(T81, T77))
pC_in_gg(T81, T77) → U5_gg(T81, T77, fD_in_gg(T81, T77))
fD_in_gg(0, T86) → fD_out_gg(0, T86)
fD_in_gg(s(T97), T93) → U4_gg(T97, T93, fD_in_gg(T97, s(T93)))
U4_gg(T97, T93, fD_out_gg(T97, s(T93))) → fD_out_gg(s(T97), T93)
U5_gg(T81, T77, fD_out_gg(T81, T77)) → U6_gg(T81, T77, gB_in_gg(T81, T77))
U6_gg(T81, T77, gB_out_gg(T81, T77)) → pC_out_gg(T81, T77)
U2_g(T81, T77, pC_out_gg(T81, T77)) → hA_out_g(c(s(T81), T77))

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(T54)))))))))) → U1_G(T54, gB_in_gg(s(s(s(s(s(s(s(0))))))), T54))
HA_IN_G(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → GB_IN_GG(s(s(s(s(s(s(s(0))))))), T54)
GB_IN_GG(T65, s(T70)) → U3_GG(T65, T70, gB_in_gg(s(T65), T70))
GB_IN_GG(T65, s(T70)) → GB_IN_GG(s(T65), T70)
HA_IN_G(c(s(T81), T77)) → U2_G(T81, T77, pC_in_gg(T81, T77))
HA_IN_G(c(s(T81), T77)) → PC_IN_GG(T81, T77)
PC_IN_GG(T81, T77) → U5_GG(T81, T77, fD_in_gg(T81, T77))
PC_IN_GG(T81, T77) → FD_IN_GG(T81, T77)
FD_IN_GG(s(T97), T93) → U4_GG(T97, T93, fD_in_gg(T97, s(T93)))
FD_IN_GG(s(T97), T93) → FD_IN_GG(T97, s(T93))
U5_GG(T81, T77, fD_out_gg(T81, T77)) → U6_GG(T81, T77, gB_in_gg(T81, T77))
U5_GG(T81, T77, fD_out_gg(T81, T77)) → GB_IN_GG(T81, T77)

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(T54)))))))))) → U1_g(T54, gB_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gB_in_gg(T59, 0) → gB_out_gg(T59, 0)
gB_in_gg(T65, s(T70)) → U3_gg(T65, T70, gB_in_gg(s(T65), T70))
U3_gg(T65, T70, gB_out_gg(s(T65), T70)) → gB_out_gg(T65, s(T70))
U1_g(T54, gB_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hA_in_g(c(s(T81), T77)) → U2_g(T81, T77, pC_in_gg(T81, T77))
pC_in_gg(T81, T77) → U5_gg(T81, T77, fD_in_gg(T81, T77))
fD_in_gg(0, T86) → fD_out_gg(0, T86)
fD_in_gg(s(T97), T93) → U4_gg(T97, T93, fD_in_gg(T97, s(T93)))
U4_gg(T97, T93, fD_out_gg(T97, s(T93))) → fD_out_gg(s(T97), T93)
U5_gg(T81, T77, fD_out_gg(T81, T77)) → U6_gg(T81, T77, gB_in_gg(T81, T77))
U6_gg(T81, T77, gB_out_gg(T81, T77)) → pC_out_gg(T81, T77)
U2_g(T81, T77, pC_out_gg(T81, T77)) → hA_out_g(c(s(T81), T77))

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(T54)))))))))) → U1_G(T54, gB_in_gg(s(s(s(s(s(s(s(0))))))), T54))
HA_IN_G(c(0, s(s(s(s(s(s(s(s(T54)))))))))) → GB_IN_GG(s(s(s(s(s(s(s(0))))))), T54)
GB_IN_GG(T65, s(T70)) → U3_GG(T65, T70, gB_in_gg(s(T65), T70))
GB_IN_GG(T65, s(T70)) → GB_IN_GG(s(T65), T70)
HA_IN_G(c(s(T81), T77)) → U2_G(T81, T77, pC_in_gg(T81, T77))
HA_IN_G(c(s(T81), T77)) → PC_IN_GG(T81, T77)
PC_IN_GG(T81, T77) → U5_GG(T81, T77, fD_in_gg(T81, T77))
PC_IN_GG(T81, T77) → FD_IN_GG(T81, T77)
FD_IN_GG(s(T97), T93) → U4_GG(T97, T93, fD_in_gg(T97, s(T93)))
FD_IN_GG(s(T97), T93) → FD_IN_GG(T97, s(T93))
U5_GG(T81, T77, fD_out_gg(T81, T77)) → U6_GG(T81, T77, gB_in_gg(T81, T77))
U5_GG(T81, T77, fD_out_gg(T81, T77)) → GB_IN_GG(T81, T77)

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(T54)))))))))) → U1_g(T54, gB_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gB_in_gg(T59, 0) → gB_out_gg(T59, 0)
gB_in_gg(T65, s(T70)) → U3_gg(T65, T70, gB_in_gg(s(T65), T70))
U3_gg(T65, T70, gB_out_gg(s(T65), T70)) → gB_out_gg(T65, s(T70))
U1_g(T54, gB_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hA_in_g(c(s(T81), T77)) → U2_g(T81, T77, pC_in_gg(T81, T77))
pC_in_gg(T81, T77) → U5_gg(T81, T77, fD_in_gg(T81, T77))
fD_in_gg(0, T86) → fD_out_gg(0, T86)
fD_in_gg(s(T97), T93) → U4_gg(T97, T93, fD_in_gg(T97, s(T93)))
U4_gg(T97, T93, fD_out_gg(T97, s(T93))) → fD_out_gg(s(T97), T93)
U5_gg(T81, T77, fD_out_gg(T81, T77)) → U6_gg(T81, T77, gB_in_gg(T81, T77))
U6_gg(T81, T77, gB_out_gg(T81, T77)) → pC_out_gg(T81, T77)
U2_g(T81, T77, pC_out_gg(T81, T77)) → hA_out_g(c(s(T81), T77))

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(T97), T93) → FD_IN_GG(T97, s(T93))

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(T54)))))))))) → U1_g(T54, gB_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gB_in_gg(T59, 0) → gB_out_gg(T59, 0)
gB_in_gg(T65, s(T70)) → U3_gg(T65, T70, gB_in_gg(s(T65), T70))
U3_gg(T65, T70, gB_out_gg(s(T65), T70)) → gB_out_gg(T65, s(T70))
U1_g(T54, gB_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hA_in_g(c(s(T81), T77)) → U2_g(T81, T77, pC_in_gg(T81, T77))
pC_in_gg(T81, T77) → U5_gg(T81, T77, fD_in_gg(T81, T77))
fD_in_gg(0, T86) → fD_out_gg(0, T86)
fD_in_gg(s(T97), T93) → U4_gg(T97, T93, fD_in_gg(T97, s(T93)))
U4_gg(T97, T93, fD_out_gg(T97, s(T93))) → fD_out_gg(s(T97), T93)
U5_gg(T81, T77, fD_out_gg(T81, T77)) → U6_gg(T81, T77, gB_in_gg(T81, T77))
U6_gg(T81, T77, gB_out_gg(T81, T77)) → pC_out_gg(T81, T77)
U2_g(T81, T77, pC_out_gg(T81, T77)) → hA_out_g(c(s(T81), T77))

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(T97), T93) → FD_IN_GG(T97, s(T93))

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(T97), T93) → FD_IN_GG(T97, s(T93))

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(T97), T93) → FD_IN_GG(T97, s(T93))
  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(T65, s(T70)) → GB_IN_GG(s(T65), T70)

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(T54)))))))))) → U1_g(T54, gB_in_gg(s(s(s(s(s(s(s(0))))))), T54))
gB_in_gg(T59, 0) → gB_out_gg(T59, 0)
gB_in_gg(T65, s(T70)) → U3_gg(T65, T70, gB_in_gg(s(T65), T70))
U3_gg(T65, T70, gB_out_gg(s(T65), T70)) → gB_out_gg(T65, s(T70))
U1_g(T54, gB_out_gg(s(s(s(s(s(s(s(0))))))), T54)) → hA_out_g(c(0, s(s(s(s(s(s(s(s(T54))))))))))
hA_in_g(c(s(T81), T77)) → U2_g(T81, T77, pC_in_gg(T81, T77))
pC_in_gg(T81, T77) → U5_gg(T81, T77, fD_in_gg(T81, T77))
fD_in_gg(0, T86) → fD_out_gg(0, T86)
fD_in_gg(s(T97), T93) → U4_gg(T97, T93, fD_in_gg(T97, s(T93)))
U4_gg(T97, T93, fD_out_gg(T97, s(T93))) → fD_out_gg(s(T97), T93)
U5_gg(T81, T77, fD_out_gg(T81, T77)) → U6_gg(T81, T77, gB_in_gg(T81, T77))
U6_gg(T81, T77, gB_out_gg(T81, T77)) → pC_out_gg(T81, T77)
U2_g(T81, T77, pC_out_gg(T81, T77)) → hA_out_g(c(s(T81), T77))

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(T65, s(T70)) → GB_IN_GG(s(T65), T70)

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(T65, s(T70)) → GB_IN_GG(s(T65), T70)

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(T65, s(T70)) → GB_IN_GG(s(T65), T70)
  The graph contains the following edges 2 > 2

(20) YES