Runtime Complexity proof of /tmp/tmpyP0e6O/dependency2.pl

Runtime Complexity of the query pattern
h(g)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(n^1)).

0 Prolog

↳1 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 131 ms)

↳2 CdtProblem

    ↳3 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳4 CdtProblem

    ↳5 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtKnowledgeProof (⇔, 0 ms)

    ↳8 CdtProblem

    ↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 227 ms)

    ↳10 CdtProblem

    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 51 ms)

    ↳12 CdtProblem

    ↳13 SIsEmptyProof (⇔, 0 ms)

    ↳14 BOUNDS(O(1), O(1))

↳15 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 476 ms)

↳16 CdtProblem

    ↳17 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtKnowledgeProof (⇔, 0 ms)

    ↳22 CdtProblem

(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) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: h(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: h(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(f(T6), g(T6))\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: f(T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: g(T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: f(T6), SCOPE: 2, CLAUSE: 1 | f(T6), SCOPE: 2, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: true | f(c(0, T13)), SCOPE: 2, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: f(T6), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nX15 is free\nf(T6) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: f(c(0, T13)), SCOPE: 2, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(no(zero(0)), ','(p(0, X24), f(c(X24, s(T17)))))\n\nT17 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(no(zero(0)), ','(p(0, X24), f(c(X24, s(T17))))), SCOPE: 3, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X24), f(c(X24, s(T17))))), SCOPE: 3, CLAUSE: 9\n\nT17 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(','(call(zero(0)), ','(!_3, failure(a))), ','(p(0, X24), f(c(X24, s(T17))))) | ','(no(zero(0)), ','(p(0, X24), f(c(X24, s(T17))))), SCOPE: 3, CLAUSE: 9\n\nT17 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(zero(0), ','(','(!_3, failure(a)), ','(p(0, X24), f(c(X24, s(T17)))))) | ?_4 | ','(no(zero(0)), ','(p(0, X24), f(c(X24, s(T17))))), SCOPE: 3, CLAUSE: 9\n\nT17 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(zero(0), ','(','(!_3, failure(a)), ','(p(0, X24), f(c(X24, s(T17)))))), SCOPE: 5, CLAUSE: 7 | ?_5 | ?_4 | ','(no(zero(0)), ','(p(0, X24), f(c(X24, s(T17))))), SCOPE: 3, CLAUSE: 9\n\nT17 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(','(!_3, failure(a)), ','(p(0, X24), f(c(X24, s(T17))))) | ?_5 | ?_4 | ','(no(zero(0)), ','(p(0, X24), f(c(X24, s(T17))))), SCOPE: 3, CLAUSE: 9\n\nT17 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(failure(a), ','(p(0, X24), f(c(X24, s(T17)))))\n\nT17 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(failure(a), ','(p(0, X24), f(c(X24, s(T17))))), SCOPE: 6, CLAUSE: 10\n\nT17 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(no(zero(T24)), ','(p(T24, X37), f(c(X37, s(T25)))))\n\nT24 is ground\nT25 is ground\nX15 is free\nX37 is free\nf(c(T24, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(no(zero(T24)), ','(p(T24, X37), f(c(X37, s(T25))))), SCOPE: 7, CLAUSE: 8 | ','(no(zero(T24)), ','(p(T24, X37), f(c(X37, s(T25))))), SCOPE: 7, CLAUSE: 9\n\nT24 is ground\nT25 is ground\nX15 is free\nX37 is free\nf(c(T24, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(','(call(zero(T29)), ','(!_7, failure(a))), ','(p(T29, X37), f(c(X37, s(T25))))) | ','(no(zero(T29)), ','(p(T29, X37), f(c(X37, s(T25))))), SCOPE: 7, CLAUSE: 9\n\nT25 is ground\nT29 is ground\nX15 is free\nX37 is free\nf(c(T29, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(zero(T29), ','(','(!_7, failure(a)), ','(p(T29, X37), f(c(X37, s(T25)))))) | ?_8 | ','(no(zero(T29)), ','(p(T29, X37), f(c(X37, s(T25))))), SCOPE: 7, CLAUSE: 9\n\nT25 is ground\nT29 is ground\nX15 is free\nX37 is free\nf(c(T29, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(zero(T29), ','(','(!_7, failure(a)), ','(p(T29, X37), f(c(X37, s(T25)))))), SCOPE: 9, CLAUSE: 7 | ?_9 | ?_8 | ','(no(zero(T29)), ','(p(T29, X37), f(c(X37, s(T25))))), SCOPE: 7, CLAUSE: 9\n\nT25 is ground\nT29 is ground\nX15 is free\nX37 is free\nf(c(T29, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ?_9 | ?_8 | ','(no(zero(T29)), ','(p(T29, X37), f(c(X37, s(T25))))), SCOPE: 7, CLAUSE: 9\n\nT25 is ground\nT29 is ground\nX15 is free\nX37 is free\nf(c(T29, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ?_8 | ','(no(zero(T29)), ','(p(T29, X37), f(c(X37, s(T25))))), SCOPE: 7, CLAUSE: 9\n\nT25 is ground\nT29 is ground\nX15 is free\nX37 is free\nf(c(T29, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(no(zero(T29)), ','(p(T29, X37), f(c(X37, s(T25))))), SCOPE: 7, CLAUSE: 9\n\nT25 is ground\nT29 is ground\nX15 is free\nX37 is free\nf(c(T29, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(p(T33, X37), f(c(X37, s(T25))))\n\nT25 is ground\nT33 is ground\nX15 is free\nX37 is free\nf(c(T33, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(p(T33, X37), f(c(X37, s(T25)))), SCOPE: 10, CLAUSE: 5 | ','(p(T33, X37), f(c(X37, s(T25)))), SCOPE: 10, CLAUSE: 6\n\nT25 is ground\nT33 is ground\nX15 is free\nX37 is free\nf(c(T33, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(p(T33, X37), f(c(X37, s(T25)))), SCOPE: 10, CLAUSE: 6\n\nT25 is ground\nT33 is ground\nX15 is free\nX37 is free\nf(c(T33, T25)) !=? f(c(0, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: f(c(T37, s(T25)))\n\nT25 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: g(T6), SCOPE: 11, CLAUSE: 3 | g(T6), SCOPE: 11, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true | g(c(T44, 0)), SCOPE: 11, CLAUSE: 4\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: g(T6), SCOPE: 11, CLAUSE: 4\n\nT6 is ground\nX56 is free\ng(T6) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: g(c(T44, 0)), SCOPE: 11, CLAUSE: 4\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(no(zero(0)), ','(p(0, X65), g(c(s(T48), X65))))\n\nT48 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(no(zero(0)), ','(p(0, X65), g(c(s(T48), X65)))), SCOPE: 12, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X65), g(c(s(T48), X65)))), SCOPE: 12, CLAUSE: 9\n\nT48 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(','(call(zero(0)), ','(!_12, failure(a))), ','(p(0, X65), g(c(s(T48), X65)))) | ','(no(zero(0)), ','(p(0, X65), g(c(s(T48), X65)))), SCOPE: 12, CLAUSE: 9\n\nT48 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(zero(0), ','(','(!_12, failure(a)), ','(p(0, X65), g(c(s(T48), X65))))) | ?_13 | ','(no(zero(0)), ','(p(0, X65), g(c(s(T48), X65)))), SCOPE: 12, CLAUSE: 9\n\nT48 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(zero(0), ','(','(!_12, failure(a)), ','(p(0, X65), g(c(s(T48), X65))))), SCOPE: 14, CLAUSE: 7 | ?_14 | ?_13 | ','(no(zero(0)), ','(p(0, X65), g(c(s(T48), X65)))), SCOPE: 12, CLAUSE: 9\n\nT48 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(','(!_12, failure(a)), ','(p(0, X65), g(c(s(T48), X65)))) | ?_14 | ?_13 | ','(no(zero(0)), ','(p(0, X65), g(c(s(T48), X65)))), SCOPE: 12, CLAUSE: 9\n\nT48 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(failure(a), ','(p(0, X65), g(c(s(T48), X65))))\n\nT48 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(failure(a), ','(p(0, X65), g(c(s(T48), X65)))), SCOPE: 15, CLAUSE: 10\n\nT48 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(no(zero(T56)), ','(p(T56, X78), g(c(s(T55), X78))))\n\nT55 is ground\nT56 is ground\nX56 is free\nX78 is free\ng(c(T55, T56)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(no(zero(T56)), ','(p(T56, X78), g(c(s(T55), X78)))), SCOPE: 16, CLAUSE: 8 | ','(no(zero(T56)), ','(p(T56, X78), g(c(s(T55), X78)))), SCOPE: 16, CLAUSE: 9\n\nT55 is ground\nT56 is ground\nX56 is free\nX78 is free\ng(c(T55, T56)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(','(call(zero(T60)), ','(!_16, failure(a))), ','(p(T60, X78), g(c(s(T55), X78)))) | ','(no(zero(T60)), ','(p(T60, X78), g(c(s(T55), X78)))), SCOPE: 16, CLAUSE: 9\n\nT55 is ground\nT60 is ground\nX56 is free\nX78 is free\ng(c(T55, T60)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(zero(T60), ','(','(!_16, failure(a)), ','(p(T60, X78), g(c(s(T55), X78))))) | ?_17 | ','(no(zero(T60)), ','(p(T60, X78), g(c(s(T55), X78)))), SCOPE: 16, CLAUSE: 9\n\nT55 is ground\nT60 is ground\nX56 is free\nX78 is free\ng(c(T55, T60)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(zero(T60), ','(','(!_16, failure(a)), ','(p(T60, X78), g(c(s(T55), X78))))), SCOPE: 18, CLAUSE: 7 | ?_18 | ?_17 | ','(no(zero(T60)), ','(p(T60, X78), g(c(s(T55), X78)))), SCOPE: 16, CLAUSE: 9\n\nT55 is ground\nT60 is ground\nX56 is free\nX78 is free\ng(c(T55, T60)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ?_18 | ?_17 | ','(no(zero(T60)), ','(p(T60, X78), g(c(s(T55), X78)))), SCOPE: 16, CLAUSE: 9\n\nT55 is ground\nT60 is ground\nX56 is free\nX78 is free\ng(c(T55, T60)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ?_17 | ','(no(zero(T60)), ','(p(T60, X78), g(c(s(T55), X78)))), SCOPE: 16, CLAUSE: 9\n\nT55 is ground\nT60 is ground\nX56 is free\nX78 is free\ng(c(T55, T60)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(no(zero(T60)), ','(p(T60, X78), g(c(s(T55), X78)))), SCOPE: 16, CLAUSE: 9\n\nT55 is ground\nT60 is ground\nX56 is free\nX78 is free\ng(c(T55, T60)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(p(T64, X78), g(c(s(T55), X78)))\n\nT55 is ground\nT64 is ground\nX56 is free\nX78 is free\ng(c(T55, T64)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(p(T64, X78), g(c(s(T55), X78))), SCOPE: 19, CLAUSE: 5 | ','(p(T64, X78), g(c(s(T55), X78))), SCOPE: 19, CLAUSE: 6\n\nT55 is ground\nT64 is ground\nX56 is free\nX78 is free\ng(c(T55, T64)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(p(T64, X78), g(c(s(T55), X78))), SCOPE: 19, CLAUSE: 6\n\nT55 is ground\nT64 is ground\nX56 is free\nX78 is free\ng(c(T55, T64)) !=? g(c(X56, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: g(c(s(T55), T68))\n\nT55 is ground\nT68 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 146 [arrowhead = none ];
146 -> 3;

147 [label="ONLY EVAL with clause\nh(X8) :- ','(f(X8), g(X8)).\nand substitutionT1 -> T6,\nX8 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 147 [arrowhead = none ];
147 -> 6;

148 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
6 -> 148 [arrowhead = none ];
148 -> 13;

149 [label="SPLIT 2\nnew knowledge:\nT6 is ground", fontsize=14, style = filled, fillcolor = violet];
6 -> 149 [arrowhead = none ];
149 -> 14;

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

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

152 [label="EVAL with clause\nf(c(0, X15)).\nand substitutionX15 -> T13,\nT6 -> c(0, T13)", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 152 [arrowhead = none ];
152 -> 24;

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

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

155 [label="EVAL with clause\nf(c(X35, X36)) :- ','(no(zero(X35)), ','(p(X35, X37), f(c(X37, s(X36))))).\nand substitutionX35 -> T24,\nX36 -> T25,\nT6 -> c(T24, T25)", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 155 [arrowhead = none ];
155 -> 50;

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

157 [label="ONLY EVAL with clause\nf(c(X22, X23)) :- ','(no(zero(X22)), ','(p(X22, X24), f(c(X24, s(X23))))).\nand substitutionX22 -> 0,\nT13 -> T17,\nX23 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 157 [arrowhead = none ];
157 -> 31;

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

159 [label="ONLY EVAL with clause\nno(X28) :- ','(call(X28), ','(!_3, failure(a))).\nand substitutionX28 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 159 [arrowhead = none ];
159 -> 34;

160 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
34 -> 160 [arrowhead = none ];
160 -> 36;

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

162 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 162 [arrowhead = none ];
162 -> 43;

163 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 163 [arrowhead = none ];
163 -> 44;

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

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

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

167 [label="ONLY EVAL with clause\nno(X41) :- ','(call(X41), ','(!_7, failure(a))).\nand substitutionT24 -> T29,\nX41 -> zero(T29)", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 167 [arrowhead = none ];
167 -> 68;

168 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 168 [arrowhead = none ];
168 -> 70;

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

170 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (f(c(T29, T25)), f(c(0, X15)))", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 170 [arrowhead = none ];
170 -> 72;

171 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 171 [arrowhead = none ];
171 -> 73;

172 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 172 [arrowhead = none ];
172 -> 74;

173 [label="ONLY EVAL with clause\nno(X45).\nand substitutionT29 -> T33,\nX45 -> zero(T33)", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 173 [arrowhead = none ];
173 -> 76;

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

175 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(c(T33, T25)), f(c(0, X15)))", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 175 [arrowhead = none ];
175 -> 88;

176 [label="EVAL with clause\np(s(X49), X49).\nand substitutionX49 -> T37,\nT33 -> s(T37),\nX37 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 176 [arrowhead = none ];
176 -> 91;

177 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 177 [arrowhead = none ];
177 -> 92;

178 [label="INSTANCE with matching:\nT6 -> c(T37, s(T25))", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 178 [arrowhead = none , style=dashed];
178 -> 13[style=dashed];

179 [label="EVAL with clause\ng(c(X56, 0)).\nand substitutionX56 -> T44,\nT6 -> c(T44, 0)", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 179 [arrowhead = none ];
179 -> 98;

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

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

182 [label="EVAL with clause\ng(c(X76, X77)) :- ','(no(zero(X77)), ','(p(X77, X78), g(c(s(X76), X78)))).\nand substitutionX76 -> T55,\nX77 -> T56,\nT6 -> c(T55, T56)", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 182 [arrowhead = none ];
182 -> 120;

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

184 [label="ONLY EVAL with clause\ng(c(X63, X64)) :- ','(no(zero(X64)), ','(p(X64, X65), g(c(s(X63), X65)))).\nand substitutionT44 -> T48,\nX63 -> T48,\nX64 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 184 [arrowhead = none ];
184 -> 103;

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

186 [label="ONLY EVAL with clause\nno(X69) :- ','(call(X69), ','(!_12, failure(a))).\nand substitutionX69 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 186 [arrowhead = none ];
186 -> 110;

187 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
110 -> 187 [arrowhead = none ];
187 -> 111;

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

189 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 189 [arrowhead = none ];
189 -> 115;

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

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

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

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

194 [label="ONLY EVAL with clause\nno(X82) :- ','(call(X82), ','(!_16, failure(a))).\nand substitutionT56 -> T60,\nX82 -> zero(T60)", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 194 [arrowhead = none ];
194 -> 126;

195 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
126 -> 195 [arrowhead = none ];
195 -> 128;

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

197 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(T55, T60)), g(c(X56, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
131 -> 197 [arrowhead = none ];
197 -> 133;

198 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 198 [arrowhead = none ];
198 -> 134;

199 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 199 [arrowhead = none ];
199 -> 135;

200 [label="ONLY EVAL with clause\nno(X86).\nand substitutionT60 -> T64,\nX86 -> zero(T64)", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 200 [arrowhead = none ];
200 -> 137;

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

202 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(T55, T64)), g(c(X56, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 202 [arrowhead = none ];
202 -> 141;

203 [label="EVAL with clause\np(s(X90), X90).\nand substitutionX90 -> T68,\nT64 -> s(T68),\nX78 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 203 [arrowhead = none ];
203 -> 144;

204 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 204 [arrowhead = none ];
204 -> 145;

205 [label="INSTANCE with matching:\nT6 -> c(s(T55), T68)", fontsize=14, style = filled, fillcolor = lightgrey];
144 -> 205 [arrowhead = none , style=dashed];
205 -> 14[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f13_in(c(0, z0)) → f13_out1
f13_in(c(s(z0), z1)) → U2(f13_in(c(z0, s(z1))), c(s(z0), z1))
U2(f13_out1, c(s(z0), z1)) → f13_out1
f14_in(c(z0, 0)) → f14_out1
f14_in(c(z0, s(z1))) → U3(f14_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f14_out1, c(z0, s(z1))) → f14_out1
f6_in(z0) → U4(f13_in(z0), z0)
U4(f13_out1, z0) → U5(f14_in(z0), z0)
U5(f14_out1, z0) → f6_out1

Tuples:

F2_IN(z0) → c1(U1'(f6_in(z0), z0), F6_IN(z0))
F13_IN(c(s(z0), z1)) → c4(U2'(f13_in(c(z0, s(z1))), c(s(z0), z1)), F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(U3'(f14_in(c(s(z0), z1)), c(z0, s(z1))), F14_IN(c(s(z0), z1)))
F6_IN(z0) → c9(U4'(f13_in(z0), z0), F13_IN(z0))
U4'(f13_out1, z0) → c10(U5'(f14_in(z0), z0), F14_IN(z0))

S tuples:

F2_IN(z0) → c1(U1'(f6_in(z0), z0), F6_IN(z0))
F13_IN(c(s(z0), z1)) → c4(U2'(f13_in(c(z0, s(z1))), c(s(z0), z1)), F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(U3'(f14_in(c(s(z0), z1)), c(z0, s(z1))), F14_IN(c(s(z0), z1)))
F6_IN(z0) → c9(U4'(f13_in(z0), z0), F13_IN(z0))
U4'(f13_out1, z0) → c10(U5'(f14_in(z0), z0), F14_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f13_in, U2, f14_in, U3, f6_in, U4, U5

Defined Pair Symbols:

F2_IN, F13_IN, F14_IN, F6_IN, U4'

Compound Symbols:

c1, c4, c7, c9, c10

(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f13_in(c(0, z0)) → f13_out1
f13_in(c(s(z0), z1)) → U2(f13_in(c(z0, s(z1))), c(s(z0), z1))
U2(f13_out1, c(s(z0), z1)) → f13_out1
f14_in(c(z0, 0)) → f14_out1
f14_in(c(z0, s(z1))) → U3(f14_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f14_out1, c(z0, s(z1))) → f14_out1
f6_in(z0) → U4(f13_in(z0), z0)
U4(f13_out1, z0) → U5(f14_in(z0), z0)
U5(f14_out1, z0) → f6_out1

Tuples:

F13_IN(c(s(z0), z1)) → c4(U2'(f13_in(c(z0, s(z1))), c(s(z0), z1)), F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(U3'(f14_in(c(s(z0), z1)), c(z0, s(z1))), F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2(U1'(f6_in(z0), z0))
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(U5'(f14_in(z0), z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))

S tuples:

F13_IN(c(s(z0), z1)) → c4(U2'(f13_in(c(z0, s(z1))), c(s(z0), z1)), F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(U3'(f14_in(c(s(z0), z1)), c(z0, s(z1))), F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2(U1'(f6_in(z0), z0))
F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(U5'(f14_in(z0), z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f13_in, U2, f14_in, U3, f6_in, U4, U5

Defined Pair Symbols:

F13_IN, F14_IN, F2_IN, F6_IN, U4'

Compound Symbols:

c4, c7, c2

(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f13_in(c(0, z0)) → f13_out1
f13_in(c(s(z0), z1)) → U2(f13_in(c(z0, s(z1))), c(s(z0), z1))
U2(f13_out1, c(s(z0), z1)) → f13_out1
f14_in(c(z0, 0)) → f14_out1
f14_in(c(z0, s(z1))) → U3(f14_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f14_out1, c(z0, s(z1))) → f14_out1
f6_in(z0) → U4(f13_in(z0), z0)
U4(f13_out1, z0) → U5(f14_in(z0), z0)
U5(f14_out1, z0) → f6_out1

Tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2

S tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2

K tuples:none
Defined Rule Symbols:

f2_in, U1, f13_in, U2, f14_in, U3, f6_in, U4, U5

Defined Pair Symbols:

F2_IN, F6_IN, U4', F13_IN, F14_IN

Compound Symbols:

c2, c4, c7, c2

(7) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
U4'(f13_out1, z0) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f13_in(c(0, z0)) → f13_out1
f13_in(c(s(z0), z1)) → U2(f13_in(c(z0, s(z1))), c(s(z0), z1))
U2(f13_out1, c(s(z0), z1)) → f13_out1
f14_in(c(z0, 0)) → f14_out1
f14_in(c(z0, s(z1))) → U3(f14_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f14_out1, c(z0, s(z1))) → f14_out1
f6_in(z0) → U4(f13_in(z0), z0)
U4(f13_out1, z0) → U5(f14_in(z0), z0)
U5(f14_out1, z0) → f6_out1

Tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2

S tuples:

F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))

K tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2

Defined Rule Symbols:

f2_in, U1, f13_in, U2, f14_in, U3, f6_in, U4, U5

Defined Pair Symbols:

F2_IN, F6_IN, U4', F13_IN, F14_IN

Compound Symbols:

c2, c4, c7, c2

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))

We considered the (Usable) Rules:

f13_in(c(0, z0)) → f13_out1
f13_in(c(s(z0), z1)) → U2(f13_in(c(z0, s(z1))), c(s(z0), z1))
U2(f13_out1, c(s(z0), z1)) → f13_out1

And the Tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(F13_IN(x₁)) = [2]
POL(F14_IN(x₁)) = [2] + x₁
POL(F2_IN(x₁)) = [3] + [3]x₁
POL(F6_IN(x₁)) = [3] + [3]x₁
POL(U2(x₁, x₂)) = 0
POL(U4'(x₁, x₂)) = [2] + [2]x₂
POL(c(x₁, x₂)) = x₂
POL(c2) = 0
POL(c2(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(f13_in(x₁)) = 0
POL(f13_out1) = 0
POL(s(x₁)) = [1] + x₁

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f13_in(c(0, z0)) → f13_out1
f13_in(c(s(z0), z1)) → U2(f13_in(c(z0, s(z1))), c(s(z0), z1))
U2(f13_out1, c(s(z0), z1)) → f13_out1
f14_in(c(z0, 0)) → f14_out1
f14_in(c(z0, s(z1))) → U3(f14_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f14_out1, c(z0, s(z1))) → f14_out1
f6_in(z0) → U4(f13_in(z0), z0)
U4(f13_out1, z0) → U5(f14_in(z0), z0)
U5(f14_out1, z0) → f6_out1

Tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2

S tuples:

F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))

K tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))

Defined Rule Symbols:

f2_in, U1, f13_in, U2, f14_in, U3, f6_in, U4, U5

Defined Pair Symbols:

F2_IN, F6_IN, U4', F13_IN, F14_IN

Compound Symbols:

c2, c4, c7, c2

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))

We considered the (Usable) Rules:

f13_in(c(0, z0)) → f13_out1
f13_in(c(s(z0), z1)) → U2(f13_in(c(z0, s(z1))), c(s(z0), z1))
U2(f13_out1, c(s(z0), z1)) → f13_out1

And the Tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(F13_IN(x₁)) = [1] + x₁
POL(F14_IN(x₁)) = 0
POL(F2_IN(x₁)) = [1] + [2]x₁
POL(F6_IN(x₁)) = [1] + [2]x₁
POL(U2(x₁, x₂)) = 0
POL(U4'(x₁, x₂)) = 0
POL(c(x₁, x₂)) = x₁
POL(c2) = 0
POL(c2(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(f13_in(x₁)) = 0
POL(f13_out1) = 0
POL(s(x₁)) = [1] + x₁

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f6_in(z0), z0)
U1(f6_out1, z0) → f2_out1
f13_in(c(0, z0)) → f13_out1
f13_in(c(s(z0), z1)) → U2(f13_in(c(z0, s(z1))), c(s(z0), z1))
U2(f13_out1, c(s(z0), z1)) → f13_out1
f14_in(c(z0, 0)) → f14_out1
f14_in(c(z0, s(z1))) → U3(f14_in(c(s(z0), z1)), c(z0, s(z1)))
U3(f14_out1, c(z0, s(z1))) → f14_out1
f6_in(z0) → U4(f13_in(z0), z0)
U4(f13_out1, z0) → U5(f14_in(z0), z0)
U5(f14_out1, z0) → f6_out1

Tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2

S tuples:none
K tuples:

F2_IN(z0) → c2(F6_IN(z0))
F6_IN(z0) → c2(U4'(f13_in(z0), z0))
F6_IN(z0) → c2(F13_IN(z0))
U4'(f13_out1, z0) → c2(F14_IN(z0))
F2_IN(z0) → c2
U4'(f13_out1, z0) → c2
F14_IN(c(z0, s(z1))) → c7(F14_IN(c(s(z0), z1)))
F13_IN(c(s(z0), z1)) → c4(F13_IN(c(z0, s(z1))))

Defined Rule Symbols:

f2_in, U1, f13_in, U2, f14_in, U3, f6_in, U4, U5

Defined Pair Symbols:

F2_IN, F6_IN, U4', F13_IN, F14_IN

Compound Symbols:

c2, c4, c7, c2

(13) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(14) BOUNDS(O(1), O(1))

(15) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: h(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: h(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(f(T3), g(T3))\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(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];
8 [label="8: 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];
9 [label="9: ','(f(T3), g(T3)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nX8 is free\nf(T3) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: g(c(0, T6))\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(f(c(0, T6)), g(c(0, T6))), SCOPE: 2, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: 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];
15 [label="15: true | g(c(0, 0)), SCOPE: 3, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: g(c(0, T6)), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX15 is free\ng(c(0, T6)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: g(c(0, 0)), SCOPE: 3, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(no(zero(0)), ','(p(0, X24), g(c(s(0), X24))))\n\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(no(zero(0)), ','(p(0, X24), g(c(s(0), X24)))), SCOPE: 4, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X24), g(c(s(0), X24)))), SCOPE: 4, CLAUSE: 9\n\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(','(call(zero(0)), ','(!_4, failure(a))), ','(p(0, X24), g(c(s(0), X24)))) | ','(no(zero(0)), ','(p(0, X24), g(c(s(0), X24)))), SCOPE: 4, CLAUSE: 9\n\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(zero(0), ','(','(!_4, failure(a)), ','(p(0, X24), g(c(s(0), X24))))) | ?_5 | ','(no(zero(0)), ','(p(0, X24), g(c(s(0), X24)))), SCOPE: 4, CLAUSE: 9\n\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(zero(0), ','(','(!_4, failure(a)), ','(p(0, X24), g(c(s(0), X24))))), SCOPE: 6, CLAUSE: 7 | ?_6 | ?_5 | ','(no(zero(0)), ','(p(0, X24), g(c(s(0), X24)))), SCOPE: 4, CLAUSE: 9\n\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(','(!_4, failure(a)), ','(p(0, X24), g(c(s(0), X24)))) | ?_6 | ?_5 | ','(no(zero(0)), ','(p(0, X24), g(c(s(0), X24)))), SCOPE: 4, CLAUSE: 9\n\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(failure(a), ','(p(0, X24), g(c(s(0), X24))))\n\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(failure(a), ','(p(0, X24), g(c(s(0), X24)))), SCOPE: 7, CLAUSE: 10\n\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(no(zero(T9)), ','(p(T9, X38), g(c(s(0), X38))))\n\nT9 is ground\nX15 is free\nX38 is free\ng(c(0, T9)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(no(zero(T9)), ','(p(T9, X38), g(c(s(0), X38)))), SCOPE: 8, CLAUSE: 8 | ','(no(zero(T9)), ','(p(T9, X38), g(c(s(0), X38)))), SCOPE: 8, CLAUSE: 9\n\nT9 is ground\nX15 is free\nX38 is free\ng(c(0, T9)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(','(call(zero(T12)), ','(!_8, failure(a))), ','(p(T12, X38), g(c(s(0), X38)))) | ','(no(zero(T12)), ','(p(T12, X38), g(c(s(0), X38)))), SCOPE: 8, CLAUSE: 9\n\nT12 is ground\nX15 is free\nX38 is free\ng(c(0, T12)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(zero(T12), ','(','(!_8, failure(a)), ','(p(T12, X38), g(c(s(0), X38))))) | ?_9 | ','(no(zero(T12)), ','(p(T12, X38), g(c(s(0), X38)))), SCOPE: 8, CLAUSE: 9\n\nT12 is ground\nX15 is free\nX38 is free\ng(c(0, T12)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(zero(T12), ','(','(!_8, failure(a)), ','(p(T12, X38), g(c(s(0), X38))))), SCOPE: 10, CLAUSE: 7 | ?_10 | ?_9 | ','(no(zero(T12)), ','(p(T12, X38), g(c(s(0), X38)))), SCOPE: 8, CLAUSE: 9\n\nT12 is ground\nX15 is free\nX38 is free\ng(c(0, T12)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ?_10 | ?_9 | ','(no(zero(T12)), ','(p(T12, X38), g(c(s(0), X38)))), SCOPE: 8, CLAUSE: 9\n\nT12 is ground\nX15 is free\nX38 is free\ng(c(0, T12)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ?_9 | ','(no(zero(T12)), ','(p(T12, X38), g(c(s(0), X38)))), SCOPE: 8, CLAUSE: 9\n\nT12 is ground\nX15 is free\nX38 is free\ng(c(0, T12)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(no(zero(T12)), ','(p(T12, X38), g(c(s(0), X38)))), SCOPE: 8, CLAUSE: 9\n\nT12 is ground\nX15 is free\nX38 is free\ng(c(0, T12)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(p(T15, X38), g(c(s(0), X38)))\n\nT15 is ground\nX15 is free\nX38 is free\ng(c(0, T15)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(p(T15, X38), g(c(s(0), X38))), SCOPE: 11, CLAUSE: 5 | ','(p(T15, X38), g(c(s(0), X38))), SCOPE: 11, CLAUSE: 6\n\nT15 is ground\nX15 is free\nX38 is free\ng(c(0, T15)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(p(T15, X38), g(c(s(0), X38))), SCOPE: 11, CLAUSE: 6\n\nT15 is ground\nX15 is free\nX38 is free\ng(c(0, T15)) !=? g(c(X15, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: g(c(s(0), T18))\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: g(c(s(0), T18)), SCOPE: 12, CLAUSE: 3 | g(c(s(0), T18)), SCOPE: 12, CLAUSE: 4\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: true | g(c(s(0), 0)), SCOPE: 12, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: g(c(s(0), T18)), SCOPE: 12, CLAUSE: 4\n\nT18 is ground\nX55 is free\ng(c(s(0), T18)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: g(c(s(0), 0)), SCOPE: 12, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(no(zero(0)), ','(p(0, X64), g(c(s(s(0)), X64))))\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(no(zero(0)), ','(p(0, X64), g(c(s(s(0)), X64)))), SCOPE: 13, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X64), g(c(s(s(0)), X64)))), SCOPE: 13, CLAUSE: 9\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(','(call(zero(0)), ','(!_13, failure(a))), ','(p(0, X64), g(c(s(s(0)), X64)))) | ','(no(zero(0)), ','(p(0, X64), g(c(s(s(0)), X64)))), SCOPE: 13, CLAUSE: 9\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(zero(0), ','(','(!_13, failure(a)), ','(p(0, X64), g(c(s(s(0)), X64))))) | ?_14 | ','(no(zero(0)), ','(p(0, X64), g(c(s(s(0)), X64)))), SCOPE: 13, CLAUSE: 9\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(zero(0), ','(','(!_13, failure(a)), ','(p(0, X64), g(c(s(s(0)), X64))))), SCOPE: 15, CLAUSE: 7 | ?_15 | ?_14 | ','(no(zero(0)), ','(p(0, X64), g(c(s(s(0)), X64)))), SCOPE: 13, CLAUSE: 9\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(','(!_13, failure(a)), ','(p(0, X64), g(c(s(s(0)), X64)))) | ?_15 | ?_14 | ','(no(zero(0)), ','(p(0, X64), g(c(s(s(0)), X64)))), SCOPE: 13, CLAUSE: 9\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(failure(a), ','(p(0, X64), g(c(s(s(0)), X64))))\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(failure(a), ','(p(0, X64), g(c(s(s(0)), X64)))), SCOPE: 16, CLAUSE: 10\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(no(zero(T21)), ','(p(T21, X78), g(c(s(s(0)), X78))))\n\nT21 is ground\nX55 is free\nX78 is free\ng(c(s(0), T21)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(no(zero(T21)), ','(p(T21, X78), g(c(s(s(0)), X78)))), SCOPE: 17, CLAUSE: 8 | ','(no(zero(T21)), ','(p(T21, X78), g(c(s(s(0)), X78)))), SCOPE: 17, CLAUSE: 9\n\nT21 is ground\nX55 is free\nX78 is free\ng(c(s(0), T21)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(','(call(zero(T24)), ','(!_17, failure(a))), ','(p(T24, X78), g(c(s(s(0)), X78)))) | ','(no(zero(T24)), ','(p(T24, X78), g(c(s(s(0)), X78)))), SCOPE: 17, CLAUSE: 9\n\nT24 is ground\nX55 is free\nX78 is free\ng(c(s(0), T24)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(zero(T24), ','(','(!_17, failure(a)), ','(p(T24, X78), g(c(s(s(0)), X78))))) | ?_18 | ','(no(zero(T24)), ','(p(T24, X78), g(c(s(s(0)), X78)))), SCOPE: 17, CLAUSE: 9\n\nT24 is ground\nX55 is free\nX78 is free\ng(c(s(0), T24)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(zero(T24), ','(','(!_17, failure(a)), ','(p(T24, X78), g(c(s(s(0)), X78))))), SCOPE: 19, CLAUSE: 7 | ?_19 | ?_18 | ','(no(zero(T24)), ','(p(T24, X78), g(c(s(s(0)), X78)))), SCOPE: 17, CLAUSE: 9\n\nT24 is ground\nX55 is free\nX78 is free\ng(c(s(0), T24)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ?_19 | ?_18 | ','(no(zero(T24)), ','(p(T24, X78), g(c(s(s(0)), X78)))), SCOPE: 17, CLAUSE: 9\n\nT24 is ground\nX55 is free\nX78 is free\ng(c(s(0), T24)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ?_18 | ','(no(zero(T24)), ','(p(T24, X78), g(c(s(s(0)), X78)))), SCOPE: 17, CLAUSE: 9\n\nT24 is ground\nX55 is free\nX78 is free\ng(c(s(0), T24)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(no(zero(T24)), ','(p(T24, X78), g(c(s(s(0)), X78)))), SCOPE: 17, CLAUSE: 9\n\nT24 is ground\nX55 is free\nX78 is free\ng(c(s(0), T24)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(p(T27, X78), g(c(s(s(0)), X78)))\n\nT27 is ground\nX55 is free\nX78 is free\ng(c(s(0), T27)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(p(T27, X78), g(c(s(s(0)), X78))), SCOPE: 20, CLAUSE: 5 | ','(p(T27, X78), g(c(s(s(0)), X78))), SCOPE: 20, CLAUSE: 6\n\nT27 is ground\nX55 is free\nX78 is free\ng(c(s(0), T27)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(p(T27, X78), g(c(s(s(0)), X78))), SCOPE: 20, CLAUSE: 6\n\nT27 is ground\nX55 is free\nX78 is free\ng(c(s(0), T27)) !=? g(c(X55, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: g(c(s(s(0)), T30))\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: g(c(s(s(0)), T30)), SCOPE: 21, CLAUSE: 3 | g(c(s(s(0)), T30)), SCOPE: 21, CLAUSE: 4\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: true | g(c(s(s(0)), 0)), SCOPE: 21, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: g(c(s(s(0)), T30)), SCOPE: 21, CLAUSE: 4\n\nT30 is ground\nX95 is free\ng(c(s(s(0)), T30)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: g(c(s(s(0)), 0)), SCOPE: 21, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(no(zero(0)), ','(p(0, X104), g(c(s(s(s(0))), X104))))\n\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(no(zero(0)), ','(p(0, X104), g(c(s(s(s(0))), X104)))), SCOPE: 22, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X104), g(c(s(s(s(0))), X104)))), SCOPE: 22, CLAUSE: 9\n\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(','(call(zero(0)), ','(!_22, failure(a))), ','(p(0, X104), g(c(s(s(s(0))), X104)))) | ','(no(zero(0)), ','(p(0, X104), g(c(s(s(s(0))), X104)))), SCOPE: 22, CLAUSE: 9\n\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(zero(0), ','(','(!_22, failure(a)), ','(p(0, X104), g(c(s(s(s(0))), X104))))) | ?_23 | ','(no(zero(0)), ','(p(0, X104), g(c(s(s(s(0))), X104)))), SCOPE: 22, CLAUSE: 9\n\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(zero(0), ','(','(!_22, failure(a)), ','(p(0, X104), g(c(s(s(s(0))), X104))))), SCOPE: 24, CLAUSE: 7 | ?_24 | ?_23 | ','(no(zero(0)), ','(p(0, X104), g(c(s(s(s(0))), X104)))), SCOPE: 22, CLAUSE: 9\n\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(','(!_22, failure(a)), ','(p(0, X104), g(c(s(s(s(0))), X104)))) | ?_24 | ?_23 | ','(no(zero(0)), ','(p(0, X104), g(c(s(s(s(0))), X104)))), SCOPE: 22, CLAUSE: 9\n\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(failure(a), ','(p(0, X104), g(c(s(s(s(0))), X104))))\n\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(failure(a), ','(p(0, X104), g(c(s(s(s(0))), X104)))), SCOPE: 25, CLAUSE: 10\n\nX104 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(no(zero(T33)), ','(p(T33, X118), g(c(s(s(s(0))), X118))))\n\nT33 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T33)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(no(zero(T33)), ','(p(T33, X118), g(c(s(s(s(0))), X118)))), SCOPE: 26, CLAUSE: 8 | ','(no(zero(T33)), ','(p(T33, X118), g(c(s(s(s(0))), X118)))), SCOPE: 26, CLAUSE: 9\n\nT33 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T33)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(','(call(zero(T36)), ','(!_26, failure(a))), ','(p(T36, X118), g(c(s(s(s(0))), X118)))) | ','(no(zero(T36)), ','(p(T36, X118), g(c(s(s(s(0))), X118)))), SCOPE: 26, CLAUSE: 9\n\nT36 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T36)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(zero(T36), ','(','(!_26, failure(a)), ','(p(T36, X118), g(c(s(s(s(0))), X118))))) | ?_27 | ','(no(zero(T36)), ','(p(T36, X118), g(c(s(s(s(0))), X118)))), SCOPE: 26, CLAUSE: 9\n\nT36 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T36)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(zero(T36), ','(','(!_26, failure(a)), ','(p(T36, X118), g(c(s(s(s(0))), X118))))), SCOPE: 28, CLAUSE: 7 | ?_28 | ?_27 | ','(no(zero(T36)), ','(p(T36, X118), g(c(s(s(s(0))), X118)))), SCOPE: 26, CLAUSE: 9\n\nT36 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T36)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ?_28 | ?_27 | ','(no(zero(T36)), ','(p(T36, X118), g(c(s(s(s(0))), X118)))), SCOPE: 26, CLAUSE: 9\n\nT36 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T36)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ?_27 | ','(no(zero(T36)), ','(p(T36, X118), g(c(s(s(s(0))), X118)))), SCOPE: 26, CLAUSE: 9\n\nT36 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T36)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(no(zero(T36)), ','(p(T36, X118), g(c(s(s(s(0))), X118)))), SCOPE: 26, CLAUSE: 9\n\nT36 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T36)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(p(T39, X118), g(c(s(s(s(0))), X118)))\n\nT39 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T39)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(p(T39, X118), g(c(s(s(s(0))), X118))), SCOPE: 29, CLAUSE: 5 | ','(p(T39, X118), g(c(s(s(s(0))), X118))), SCOPE: 29, CLAUSE: 6\n\nT39 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T39)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(p(T39, X118), g(c(s(s(s(0))), X118))), SCOPE: 29, CLAUSE: 6\n\nT39 is ground\nX95 is free\nX118 is free\ng(c(s(s(0)), T39)) !=? g(c(X95, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: g(c(s(s(s(0))), T42))\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: g(c(s(s(s(0))), T42)), SCOPE: 30, CLAUSE: 3 | g(c(s(s(s(0))), T42)), SCOPE: 30, CLAUSE: 4\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: true | g(c(s(s(s(0))), 0)), SCOPE: 30, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: g(c(s(s(s(0))), T42)), SCOPE: 30, CLAUSE: 4\n\nT42 is ground\nX135 is free\ng(c(s(s(s(0))), T42)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: g(c(s(s(s(0))), 0)), SCOPE: 30, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(no(zero(0)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144))))\n\nX144 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(no(zero(0)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))), SCOPE: 31, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))), SCOPE: 31, CLAUSE: 9\n\nX144 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(','(call(zero(0)), ','(!_31, failure(a))), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))) | ','(no(zero(0)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))), SCOPE: 31, CLAUSE: 9\n\nX144 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(zero(0), ','(','(!_31, failure(a)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144))))) | ?_32 | ','(no(zero(0)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))), SCOPE: 31, CLAUSE: 9\n\nX144 is free", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(zero(0), ','(','(!_31, failure(a)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144))))), SCOPE: 33, CLAUSE: 7 | ?_33 | ?_32 | ','(no(zero(0)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))), SCOPE: 31, CLAUSE: 9\n\nX144 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(','(!_31, failure(a)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))) | ?_33 | ?_32 | ','(no(zero(0)), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))), SCOPE: 31, CLAUSE: 9\n\nX144 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(failure(a), ','(p(0, X144), g(c(s(s(s(s(0)))), X144))))\n\nX144 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(failure(a), ','(p(0, X144), g(c(s(s(s(s(0)))), X144)))), SCOPE: 34, CLAUSE: 10\n\nX144 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(no(zero(T45)), ','(p(T45, X158), g(c(s(s(s(s(0)))), X158))))\n\nT45 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T45)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(no(zero(T45)), ','(p(T45, X158), g(c(s(s(s(s(0)))), X158)))), SCOPE: 35, CLAUSE: 8 | ','(no(zero(T45)), ','(p(T45, X158), g(c(s(s(s(s(0)))), X158)))), SCOPE: 35, CLAUSE: 9\n\nT45 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T45)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(','(call(zero(T48)), ','(!_35, failure(a))), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158)))) | ','(no(zero(T48)), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158)))), SCOPE: 35, CLAUSE: 9\n\nT48 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T48)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: ','(zero(T48), ','(','(!_35, failure(a)), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158))))) | ?_36 | ','(no(zero(T48)), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158)))), SCOPE: 35, CLAUSE: 9\n\nT48 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T48)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(zero(T48), ','(','(!_35, failure(a)), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158))))), SCOPE: 37, CLAUSE: 7 | ?_37 | ?_36 | ','(no(zero(T48)), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158)))), SCOPE: 35, CLAUSE: 9\n\nT48 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T48)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ?_37 | ?_36 | ','(no(zero(T48)), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158)))), SCOPE: 35, CLAUSE: 9\n\nT48 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T48)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ?_36 | ','(no(zero(T48)), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158)))), SCOPE: 35, CLAUSE: 9\n\nT48 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T48)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(no(zero(T48)), ','(p(T48, X158), g(c(s(s(s(s(0)))), X158)))), SCOPE: 35, CLAUSE: 9\n\nT48 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T48)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(p(T51, X158), g(c(s(s(s(s(0)))), X158)))\n\nT51 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T51)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(p(T51, X158), g(c(s(s(s(s(0)))), X158))), SCOPE: 38, CLAUSE: 5 | ','(p(T51, X158), g(c(s(s(s(s(0)))), X158))), SCOPE: 38, CLAUSE: 6\n\nT51 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T51)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(p(T51, X158), g(c(s(s(s(s(0)))), X158))), SCOPE: 38, CLAUSE: 6\n\nT51 is ground\nX135 is free\nX158 is free\ng(c(s(s(s(0))), T51)) !=? g(c(X135, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: g(c(s(s(s(s(0)))), T54))\n\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: g(c(s(s(s(s(0)))), T54)), SCOPE: 39, CLAUSE: 3 | g(c(s(s(s(s(0)))), T54)), SCOPE: 39, CLAUSE: 4\n\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: true | g(c(s(s(s(s(0)))), 0)), SCOPE: 39, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: g(c(s(s(s(s(0)))), T54)), SCOPE: 39, CLAUSE: 4\n\nT54 is ground\nX175 is free\ng(c(s(s(s(s(0)))), T54)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: g(c(s(s(s(s(0)))), 0)), SCOPE: 39, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(no(zero(0)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184))))\n\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(no(zero(0)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))), SCOPE: 40, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))), SCOPE: 40, CLAUSE: 9\n\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ','(','(call(zero(0)), ','(!_40, failure(a))), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))) | ','(no(zero(0)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))), SCOPE: 40, CLAUSE: 9\n\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(zero(0), ','(','(!_40, failure(a)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184))))) | ?_41 | ','(no(zero(0)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))), SCOPE: 40, CLAUSE: 9\n\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: ','(zero(0), ','(','(!_40, failure(a)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184))))), SCOPE: 42, CLAUSE: 7 | ?_42 | ?_41 | ','(no(zero(0)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))), SCOPE: 40, CLAUSE: 9\n\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ','(','(!_40, failure(a)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))) | ?_42 | ?_41 | ','(no(zero(0)), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))), SCOPE: 40, CLAUSE: 9\n\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ','(failure(a), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184))))\n\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ','(failure(a), ','(p(0, X184), g(c(s(s(s(s(s(0))))), X184)))), SCOPE: 43, CLAUSE: 10\n\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(no(zero(T57)), ','(p(T57, X198), g(c(s(s(s(s(s(0))))), X198))))\n\nT57 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T57)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(no(zero(T57)), ','(p(T57, X198), g(c(s(s(s(s(s(0))))), X198)))), SCOPE: 44, CLAUSE: 8 | ','(no(zero(T57)), ','(p(T57, X198), g(c(s(s(s(s(s(0))))), X198)))), SCOPE: 44, CLAUSE: 9\n\nT57 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T57)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(','(call(zero(T60)), ','(!_44, failure(a))), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198)))) | ','(no(zero(T60)), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198)))), SCOPE: 44, CLAUSE: 9\n\nT60 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T60)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(zero(T60), ','(','(!_44, failure(a)), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198))))) | ?_45 | ','(no(zero(T60)), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198)))), SCOPE: 44, CLAUSE: 9\n\nT60 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T60)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(zero(T60), ','(','(!_44, failure(a)), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198))))), SCOPE: 46, CLAUSE: 7 | ?_46 | ?_45 | ','(no(zero(T60)), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198)))), SCOPE: 44, CLAUSE: 9\n\nT60 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T60)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ?_46 | ?_45 | ','(no(zero(T60)), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198)))), SCOPE: 44, CLAUSE: 9\n\nT60 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T60)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ?_45 | ','(no(zero(T60)), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198)))), SCOPE: 44, CLAUSE: 9\n\nT60 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T60)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(no(zero(T60)), ','(p(T60, X198), g(c(s(s(s(s(s(0))))), X198)))), SCOPE: 44, CLAUSE: 9\n\nT60 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T60)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(p(T63, X198), g(c(s(s(s(s(s(0))))), X198)))\n\nT63 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T63)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(p(T63, X198), g(c(s(s(s(s(s(0))))), X198))), SCOPE: 47, CLAUSE: 5 | ','(p(T63, X198), g(c(s(s(s(s(s(0))))), X198))), SCOPE: 47, CLAUSE: 6\n\nT63 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T63)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ','(p(T63, X198), g(c(s(s(s(s(s(0))))), X198))), SCOPE: 47, CLAUSE: 6\n\nT63 is ground\nX175 is free\nX198 is free\ng(c(s(s(s(s(0)))), T63)) !=? g(c(X175, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: g(c(s(s(s(s(s(0))))), T66))\n\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: g(c(s(s(s(s(s(0))))), T66)), SCOPE: 48, CLAUSE: 3 | g(c(s(s(s(s(s(0))))), T66)), SCOPE: 48, CLAUSE: 4\n\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: true | g(c(s(s(s(s(s(0))))), 0)), SCOPE: 48, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: g(c(s(s(s(s(s(0))))), T66)), SCOPE: 48, CLAUSE: 4\n\nT66 is ground\nX215 is free\ng(c(s(s(s(s(s(0))))), T66)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: g(c(s(s(s(s(s(0))))), 0)), SCOPE: 48, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(no(zero(0)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224))))\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(no(zero(0)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))), SCOPE: 49, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))), SCOPE: 49, CLAUSE: 9\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(','(call(zero(0)), ','(!_49, failure(a))), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))) | ','(no(zero(0)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))), SCOPE: 49, CLAUSE: 9\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(zero(0), ','(','(!_49, failure(a)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224))))) | ?_50 | ','(no(zero(0)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))), SCOPE: 49, CLAUSE: 9\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ','(zero(0), ','(','(!_49, failure(a)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224))))), SCOPE: 51, CLAUSE: 7 | ?_51 | ?_50 | ','(no(zero(0)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))), SCOPE: 49, CLAUSE: 9\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ','(','(!_49, failure(a)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))) | ?_51 | ?_50 | ','(no(zero(0)), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))), SCOPE: 49, CLAUSE: 9\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(failure(a), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224))))\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(failure(a), ','(p(0, X224), g(c(s(s(s(s(s(s(0)))))), X224)))), SCOPE: 52, CLAUSE: 10\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(no(zero(T69)), ','(p(T69, X238), g(c(s(s(s(s(s(s(0)))))), X238))))\n\nT69 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T69)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(no(zero(T69)), ','(p(T69, X238), g(c(s(s(s(s(s(s(0)))))), X238)))), SCOPE: 53, CLAUSE: 8 | ','(no(zero(T69)), ','(p(T69, X238), g(c(s(s(s(s(s(s(0)))))), X238)))), SCOPE: 53, CLAUSE: 9\n\nT69 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T69)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(','(call(zero(T72)), ','(!_53, failure(a))), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238)))) | ','(no(zero(T72)), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238)))), SCOPE: 53, CLAUSE: 9\n\nT72 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T72)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: ','(zero(T72), ','(','(!_53, failure(a)), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238))))) | ?_54 | ','(no(zero(T72)), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238)))), SCOPE: 53, CLAUSE: 9\n\nT72 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T72)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(zero(T72), ','(','(!_53, failure(a)), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238))))), SCOPE: 55, CLAUSE: 7 | ?_55 | ?_54 | ','(no(zero(T72)), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238)))), SCOPE: 53, CLAUSE: 9\n\nT72 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T72)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: ?_55 | ?_54 | ','(no(zero(T72)), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238)))), SCOPE: 53, CLAUSE: 9\n\nT72 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T72)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: ?_54 | ','(no(zero(T72)), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238)))), SCOPE: 53, CLAUSE: 9\n\nT72 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T72)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: ','(no(zero(T72)), ','(p(T72, X238), g(c(s(s(s(s(s(s(0)))))), X238)))), SCOPE: 53, CLAUSE: 9\n\nT72 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T72)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(p(T75, X238), g(c(s(s(s(s(s(s(0)))))), X238)))\n\nT75 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T75)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(p(T75, X238), g(c(s(s(s(s(s(s(0)))))), X238))), SCOPE: 56, CLAUSE: 5 | ','(p(T75, X238), g(c(s(s(s(s(s(s(0)))))), X238))), SCOPE: 56, CLAUSE: 6\n\nT75 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T75)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: ','(p(T75, X238), g(c(s(s(s(s(s(s(0)))))), X238))), SCOPE: 56, CLAUSE: 6\n\nT75 is ground\nX215 is free\nX238 is free\ng(c(s(s(s(s(s(0))))), T75)) !=? g(c(X215, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: g(c(s(s(s(s(s(s(0)))))), T78))\n\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: g(c(s(s(s(s(s(s(0)))))), T78)), SCOPE: 57, CLAUSE: 3 | g(c(s(s(s(s(s(s(0)))))), T78)), SCOPE: 57, CLAUSE: 4\n\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: true | g(c(s(s(s(s(s(s(0)))))), 0)), SCOPE: 57, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: g(c(s(s(s(s(s(s(0)))))), T78)), SCOPE: 57, CLAUSE: 4\n\nT78 is ground\nX255 is free\ng(c(s(s(s(s(s(s(0)))))), T78)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: g(c(s(s(s(s(s(s(0)))))), 0)), SCOPE: 57, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: ','(no(zero(0)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264))))\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(no(zero(0)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))), SCOPE: 58, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))), SCOPE: 58, CLAUSE: 9\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ','(','(call(zero(0)), ','(!_58, failure(a))), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))) | ','(no(zero(0)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))), SCOPE: 58, CLAUSE: 9\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: ','(zero(0), ','(','(!_58, failure(a)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264))))) | ?_59 | ','(no(zero(0)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))), SCOPE: 58, CLAUSE: 9\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: ','(zero(0), ','(','(!_58, failure(a)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264))))), SCOPE: 60, CLAUSE: 7 | ?_60 | ?_59 | ','(no(zero(0)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))), SCOPE: 58, CLAUSE: 9\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: ','(','(!_58, failure(a)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))) | ?_60 | ?_59 | ','(no(zero(0)), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))), SCOPE: 58, CLAUSE: 9\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: ','(failure(a), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264))))\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: ','(failure(a), ','(p(0, X264), g(c(s(s(s(s(s(s(s(0))))))), X264)))), SCOPE: 61, CLAUSE: 10\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: ','(no(zero(T81)), ','(p(T81, X278), g(c(s(s(s(s(s(s(s(0))))))), X278))))\n\nT81 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T81)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: ','(no(zero(T81)), ','(p(T81, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))), SCOPE: 62, CLAUSE: 8 | ','(no(zero(T81)), ','(p(T81, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))), SCOPE: 62, CLAUSE: 9\n\nT81 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T81)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: ','(','(call(zero(T84)), ','(!_62, failure(a))), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))) | ','(no(zero(T84)), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))), SCOPE: 62, CLAUSE: 9\n\nT84 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T84)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: ','(zero(T84), ','(','(!_62, failure(a)), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278))))) | ?_63 | ','(no(zero(T84)), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))), SCOPE: 62, CLAUSE: 9\n\nT84 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T84)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(zero(T84), ','(','(!_62, failure(a)), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278))))), SCOPE: 64, CLAUSE: 7 | ?_64 | ?_63 | ','(no(zero(T84)), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))), SCOPE: 62, CLAUSE: 9\n\nT84 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T84)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: ?_64 | ?_63 | ','(no(zero(T84)), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))), SCOPE: 62, CLAUSE: 9\n\nT84 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T84)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: ?_63 | ','(no(zero(T84)), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))), SCOPE: 62, CLAUSE: 9\n\nT84 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T84)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: ','(no(zero(T84)), ','(p(T84, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))), SCOPE: 62, CLAUSE: 9\n\nT84 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T84)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: ','(p(T87, X278), g(c(s(s(s(s(s(s(s(0))))))), X278)))\n\nT87 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T87)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: ','(p(T87, X278), g(c(s(s(s(s(s(s(s(0))))))), X278))), SCOPE: 65, CLAUSE: 5 | ','(p(T87, X278), g(c(s(s(s(s(s(s(s(0))))))), X278))), SCOPE: 65, CLAUSE: 6\n\nT87 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T87)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: ','(p(T87, X278), g(c(s(s(s(s(s(s(s(0))))))), X278))), SCOPE: 65, CLAUSE: 6\n\nT87 is ground\nX255 is free\nX278 is free\ng(c(s(s(s(s(s(s(0)))))), T87)) !=? g(c(X255, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: g(c(s(s(s(s(s(s(s(0))))))), T90))\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: g(c(s(s(s(s(s(s(s(0))))))), T90)), SCOPE: 66, CLAUSE: 3 | g(c(s(s(s(s(s(s(s(0))))))), T90)), SCOPE: 66, CLAUSE: 4\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: true | g(c(s(s(s(s(s(s(s(0))))))), 0)), SCOPE: 66, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: g(c(s(s(s(s(s(s(s(0))))))), T90)), SCOPE: 66, CLAUSE: 4\n\nT90 is ground\nX295 is free\ng(c(s(s(s(s(s(s(s(0))))))), T90)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: g(c(s(s(s(s(s(s(s(0))))))), 0)), SCOPE: 66, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: ','(no(zero(0)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304))))\n\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: ','(no(zero(0)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))), SCOPE: 67, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))), SCOPE: 67, CLAUSE: 9\n\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: ','(','(call(zero(0)), ','(!_67, failure(a))), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))) | ','(no(zero(0)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))), SCOPE: 67, CLAUSE: 9\n\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: ','(zero(0), ','(','(!_67, failure(a)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304))))) | ?_68 | ','(no(zero(0)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))), SCOPE: 67, CLAUSE: 9\n\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: ','(zero(0), ','(','(!_67, failure(a)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304))))), SCOPE: 69, CLAUSE: 7 | ?_69 | ?_68 | ','(no(zero(0)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))), SCOPE: 67, CLAUSE: 9\n\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: ','(','(!_67, failure(a)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))) | ?_69 | ?_68 | ','(no(zero(0)), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))), SCOPE: 67, CLAUSE: 9\n\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: ','(failure(a), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304))))\n\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: ','(failure(a), ','(p(0, X304), g(c(s(s(s(s(s(s(s(s(0)))))))), X304)))), SCOPE: 70, CLAUSE: 10\n\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: ','(no(zero(T93)), ','(p(T93, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318))))\n\nT93 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T93)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: ','(no(zero(T93)), ','(p(T93, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))), SCOPE: 71, CLAUSE: 8 | ','(no(zero(T93)), ','(p(T93, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))), SCOPE: 71, CLAUSE: 9\n\nT93 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T93)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: ','(','(call(zero(T96)), ','(!_71, failure(a))), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))) | ','(no(zero(T96)), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))), SCOPE: 71, CLAUSE: 9\n\nT96 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T96)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: ','(zero(T96), ','(','(!_71, failure(a)), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318))))) | ?_72 | ','(no(zero(T96)), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))), SCOPE: 71, CLAUSE: 9\n\nT96 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T96)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: ','(zero(T96), ','(','(!_71, failure(a)), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318))))), SCOPE: 73, CLAUSE: 7 | ?_73 | ?_72 | ','(no(zero(T96)), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))), SCOPE: 71, CLAUSE: 9\n\nT96 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T96)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: ?_73 | ?_72 | ','(no(zero(T96)), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))), SCOPE: 71, CLAUSE: 9\n\nT96 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T96)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: ?_72 | ','(no(zero(T96)), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))), SCOPE: 71, CLAUSE: 9\n\nT96 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T96)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: ','(no(zero(T96)), ','(p(T96, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))), SCOPE: 71, CLAUSE: 9\n\nT96 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T96)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: ','(p(T99, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318)))\n\nT99 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T99)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: ','(p(T99, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318))), SCOPE: 74, CLAUSE: 5 | ','(p(T99, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318))), SCOPE: 74, CLAUSE: 6\n\nT99 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T99)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: ','(p(T99, X318), g(c(s(s(s(s(s(s(s(s(0)))))))), X318))), SCOPE: 74, CLAUSE: 6\n\nT99 is ground\nX295 is free\nX318 is free\ng(c(s(s(s(s(s(s(s(0))))))), T99)) !=? g(c(X295, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: g(c(s(s(s(s(s(s(s(s(0)))))))), T102))\n\nT102 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: g(c(s(T103), T102))\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: g(c(s(T103), T102)), SCOPE: 75, CLAUSE: 3 | g(c(s(T103), T102)), SCOPE: 75, CLAUSE: 4\n\nT102 is ground\nT103 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="317: true | g(c(s(T108), 0)), SCOPE: 75, CLAUSE: 4\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: g(c(s(T103), T102)), SCOPE: 75, CLAUSE: 4\n\nT102 is ground\nT103 is ground\nX337 is free\ng(c(s(T103), T102)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: g(c(s(T108), 0)), SCOPE: 75, CLAUSE: 4\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: ','(no(zero(0)), ','(p(0, X346), g(c(s(s(T112)), X346))))\n\nT112 is ground\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: ','(no(zero(0)), ','(p(0, X346), g(c(s(s(T112)), X346)))), SCOPE: 76, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X346), g(c(s(s(T112)), X346)))), SCOPE: 76, CLAUSE: 9\n\nT112 is ground\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: ','(','(call(zero(0)), ','(!_76, failure(a))), ','(p(0, X346), g(c(s(s(T112)), X346)))) | ','(no(zero(0)), ','(p(0, X346), g(c(s(s(T112)), X346)))), SCOPE: 76, CLAUSE: 9\n\nT112 is ground\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: ','(zero(0), ','(','(!_76, failure(a)), ','(p(0, X346), g(c(s(s(T112)), X346))))) | ?_77 | ','(no(zero(0)), ','(p(0, X346), g(c(s(s(T112)), X346)))), SCOPE: 76, CLAUSE: 9\n\nT112 is ground\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: ','(zero(0), ','(','(!_76, failure(a)), ','(p(0, X346), g(c(s(s(T112)), X346))))), SCOPE: 78, CLAUSE: 7 | ?_78 | ?_77 | ','(no(zero(0)), ','(p(0, X346), g(c(s(s(T112)), X346)))), SCOPE: 76, CLAUSE: 9\n\nT112 is ground\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
325 [label="325: ','(','(!_76, failure(a)), ','(p(0, X346), g(c(s(s(T112)), X346)))) | ?_78 | ?_77 | ','(no(zero(0)), ','(p(0, X346), g(c(s(s(T112)), X346)))), SCOPE: 76, CLAUSE: 9\n\nT112 is ground\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: ','(failure(a), ','(p(0, X346), g(c(s(s(T112)), X346))))\n\nT112 is ground\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="327: ','(failure(a), ','(p(0, X346), g(c(s(s(T112)), X346)))), SCOPE: 79, CLAUSE: 10\n\nT112 is ground\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: ','(no(zero(T121)), ','(p(T121, X360), g(c(s(s(T120)), X360))))\n\nT120 is ground\nT121 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T121)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: ','(no(zero(T121)), ','(p(T121, X360), g(c(s(s(T120)), X360)))), SCOPE: 80, CLAUSE: 8 | ','(no(zero(T121)), ','(p(T121, X360), g(c(s(s(T120)), X360)))), SCOPE: 80, CLAUSE: 9\n\nT120 is ground\nT121 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T121)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: ','(','(call(zero(T125)), ','(!_80, failure(a))), ','(p(T125, X360), g(c(s(s(T120)), X360)))) | ','(no(zero(T125)), ','(p(T125, X360), g(c(s(s(T120)), X360)))), SCOPE: 80, CLAUSE: 9\n\nT120 is ground\nT125 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T125)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
332 [label="332: ','(zero(T125), ','(','(!_80, failure(a)), ','(p(T125, X360), g(c(s(s(T120)), X360))))) | ?_81 | ','(no(zero(T125)), ','(p(T125, X360), g(c(s(s(T120)), X360)))), SCOPE: 80, CLAUSE: 9\n\nT120 is ground\nT125 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T125)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: ','(zero(T125), ','(','(!_80, failure(a)), ','(p(T125, X360), g(c(s(s(T120)), X360))))), SCOPE: 82, CLAUSE: 7 | ?_82 | ?_81 | ','(no(zero(T125)), ','(p(T125, X360), g(c(s(s(T120)), X360)))), SCOPE: 80, CLAUSE: 9\n\nT120 is ground\nT125 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T125)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: ?_82 | ?_81 | ','(no(zero(T125)), ','(p(T125, X360), g(c(s(s(T120)), X360)))), SCOPE: 80, CLAUSE: 9\n\nT120 is ground\nT125 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T125)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: ?_81 | ','(no(zero(T125)), ','(p(T125, X360), g(c(s(s(T120)), X360)))), SCOPE: 80, CLAUSE: 9\n\nT120 is ground\nT125 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T125)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: ','(no(zero(T125)), ','(p(T125, X360), g(c(s(s(T120)), X360)))), SCOPE: 80, CLAUSE: 9\n\nT120 is ground\nT125 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T125)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
337 [label="337: ','(p(T129, X360), g(c(s(s(T120)), X360)))\n\nT120 is ground\nT129 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T129)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: ','(p(T129, X360), g(c(s(s(T120)), X360))), SCOPE: 83, CLAUSE: 5 | ','(p(T129, X360), g(c(s(s(T120)), X360))), SCOPE: 83, CLAUSE: 6\n\nT120 is ground\nT129 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T129)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: ','(p(T129, X360), g(c(s(s(T120)), X360))), SCOPE: 83, CLAUSE: 6\n\nT120 is ground\nT129 is ground\nX337 is free\nX360 is free\ng(c(s(T120), T129)) !=? g(c(X337, 0))", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: g(c(s(s(T120)), T133))\n\nT120 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
345 [label="345: ','(','(no(zero(0)), ','(p(0, X385), f(c(X385, s(T139))))), g(c(0, T139)))\n\nT139 is ground\nX385 is free", fontsize=16, style=filled, fillcolor=lightyellow];
346 [label="346: ','(','(no(zero(0)), ','(p(0, X385), f(c(X385, s(T139))))), g(c(0, T139))), SCOPE: 84, CLAUSE: 8 | ','(','(no(zero(0)), ','(p(0, X385), f(c(X385, s(T139))))), g(c(0, T139))), SCOPE: 84, CLAUSE: 9\n\nT139 is ground\nX385 is free", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: ','(','(call(zero(0)), ','(!_84, failure(a))), ','(','(p(0, X385), f(c(X385, s(T139)))), g(c(0, T139)))) | ','(','(no(zero(0)), ','(p(0, X385), f(c(X385, s(T139))))), g(c(0, T139))), SCOPE: 84, CLAUSE: 9\n\nT139 is ground\nX385 is free", fontsize=16, style=filled, fillcolor=lightyellow];
350 [label="350: ','(zero(0), ','(','(!_84, failure(a)), ','(','(p(0, X385), f(c(X385, s(T139)))), g(c(0, T139))))) | ?_85 | ','(','(no(zero(0)), ','(p(0, X385), f(c(X385, s(T139))))), g(c(0, T139))), SCOPE: 84, CLAUSE: 9\n\nT139 is ground\nX385 is free", fontsize=16, style=filled, fillcolor=lightyellow];
351 [label="351: ','(zero(0), ','(','(!_84, failure(a)), ','(','(p(0, X385), f(c(X385, s(T139)))), g(c(0, T139))))), SCOPE: 86, CLAUSE: 7 | ?_86 | ?_85 | ','(','(no(zero(0)), ','(p(0, X385), f(c(X385, s(T139))))), g(c(0, T139))), SCOPE: 84, CLAUSE: 9\n\nT139 is ground\nX385 is free", fontsize=16, style=filled, fillcolor=lightyellow];
352 [label="352: ','(','(!_84, failure(a)), ','(','(p(0, X385), f(c(X385, s(T139)))), g(c(0, T139)))) | ?_86 | ?_85 | ','(','(no(zero(0)), ','(p(0, X385), f(c(X385, s(T139))))), g(c(0, T139))), SCOPE: 84, CLAUSE: 9\n\nT139 is ground\nX385 is free", fontsize=16, style=filled, fillcolor=lightyellow];
353 [label="353: ','(failure(a), ','(','(p(0, X385), f(c(X385, s(T139)))), g(c(0, T139))))\n\nT139 is ground\nX385 is free", fontsize=16, style=filled, fillcolor=lightyellow];
354 [label="354: ','(failure(a), ','(','(p(0, X385), f(c(X385, s(T139)))), g(c(0, T139)))), SCOPE: 87, CLAUSE: 10\n\nT139 is ground\nX385 is free", fontsize=16, style=filled, fillcolor=lightyellow];
355 [label="355: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
359 [label="359: ','(','(no(zero(T146)), ','(p(T146, X402), f(c(X402, s(T147))))), g(c(T146, T147)))\n\nT146 is ground\nT147 is ground\nX8 is free\nX402 is free\nf(c(T146, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
360 [label="360: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
362 [label="362: ','(','(no(zero(T146)), ','(p(T146, X402), f(c(X402, s(T147))))), g(c(T146, T147))), SCOPE: 88, CLAUSE: 8 | ','(','(no(zero(T146)), ','(p(T146, X402), f(c(X402, s(T147))))), g(c(T146, T147))), SCOPE: 88, CLAUSE: 9\n\nT146 is ground\nT147 is ground\nX8 is free\nX402 is free\nf(c(T146, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
363 [label="363: ','(','(call(zero(T153)), ','(!_88, failure(a))), ','(','(p(T153, X402), f(c(X402, s(T147)))), g(c(T153, T147)))) | ','(','(no(zero(T153)), ','(p(T153, X402), f(c(X402, s(T147))))), g(c(T153, T147))), SCOPE: 88, CLAUSE: 9\n\nT147 is ground\nT153 is ground\nX8 is free\nX402 is free\nf(c(T153, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
364 [label="364: ','(zero(T153), ','(','(!_88, failure(a)), ','(','(p(T153, X402), f(c(X402, s(T147)))), g(c(T153, T147))))) | ?_89 | ','(','(no(zero(T153)), ','(p(T153, X402), f(c(X402, s(T147))))), g(c(T153, T147))), SCOPE: 88, CLAUSE: 9\n\nT147 is ground\nT153 is ground\nX8 is free\nX402 is free\nf(c(T153, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: ','(zero(T153), ','(','(!_88, failure(a)), ','(','(p(T153, X402), f(c(X402, s(T147)))), g(c(T153, T147))))), SCOPE: 90, CLAUSE: 7 | ?_90 | ?_89 | ','(','(no(zero(T153)), ','(p(T153, X402), f(c(X402, s(T147))))), g(c(T153, T147))), SCOPE: 88, CLAUSE: 9\n\nT147 is ground\nT153 is ground\nX8 is free\nX402 is free\nf(c(T153, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: ?_90 | ?_89 | ','(','(no(zero(T153)), ','(p(T153, X402), f(c(X402, s(T147))))), g(c(T153, T147))), SCOPE: 88, CLAUSE: 9\n\nT147 is ground\nT153 is ground\nX8 is free\nX402 is free\nf(c(T153, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
367 [label="367: ?_89 | ','(','(no(zero(T153)), ','(p(T153, X402), f(c(X402, s(T147))))), g(c(T153, T147))), SCOPE: 88, CLAUSE: 9\n\nT147 is ground\nT153 is ground\nX8 is free\nX402 is free\nf(c(T153, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
368 [label="368: ','(','(no(zero(T153)), ','(p(T153, X402), f(c(X402, s(T147))))), g(c(T153, T147))), SCOPE: 88, CLAUSE: 9\n\nT147 is ground\nT153 is ground\nX8 is free\nX402 is free\nf(c(T153, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
369 [label="369: ','(','(p(T159, X402), f(c(X402, s(T147)))), g(c(T159, T147)))\n\nT147 is ground\nT159 is ground\nX8 is free\nX402 is free\nf(c(T159, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: ','(','(p(T159, X402), f(c(X402, s(T147)))), g(c(T159, T147))), SCOPE: 91, CLAUSE: 5 | ','(','(p(T159, X402), f(c(X402, s(T147)))), g(c(T159, T147))), SCOPE: 91, CLAUSE: 6\n\nT147 is ground\nT159 is ground\nX8 is free\nX402 is free\nf(c(T159, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: ','(','(p(T159, X402), f(c(X402, s(T147)))), g(c(T159, T147))), SCOPE: 91, CLAUSE: 6\n\nT147 is ground\nT159 is ground\nX8 is free\nX402 is free\nf(c(T159, T147)) !=? f(c(0, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
372 [label="372: ','(f(c(T165, s(T147))), g(c(s(T165), T147)))\n\nT147 is ground\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="373: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
374 [label="374: f(c(T165, s(T147)))\n\nT147 is ground\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: g(c(s(T165), T147))\n\nT147 is ground\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: f(c(T165, s(T147))), SCOPE: 92, CLAUSE: 1 | f(c(T165, s(T147))), SCOPE: 92, CLAUSE: 2\n\nT147 is ground\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
377 [label="377: true | f(c(0, s(T172))), SCOPE: 92, CLAUSE: 2\n\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
378 [label="378: f(c(T165, s(T147))), SCOPE: 92, CLAUSE: 2\n\nT147 is ground\nT165 is ground\nX427 is free\nf(c(T165, s(T147))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: f(c(0, s(T172))), SCOPE: 92, CLAUSE: 2\n\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
380 [label="380: ','(no(zero(0)), ','(p(0, X436), f(c(X436, s(s(T176))))))\n\nT176 is ground\nX436 is free", fontsize=16, style=filled, fillcolor=lightyellow];
381 [label="381: ','(no(zero(0)), ','(p(0, X436), f(c(X436, s(s(T176)))))), SCOPE: 93, CLAUSE: 8 | ','(no(zero(0)), ','(p(0, X436), f(c(X436, s(s(T176)))))), SCOPE: 93, CLAUSE: 9\n\nT176 is ground\nX436 is free", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: ','(','(call(zero(0)), ','(!_93, failure(a))), ','(p(0, X436), f(c(X436, s(s(T176)))))) | ','(no(zero(0)), ','(p(0, X436), f(c(X436, s(s(T176)))))), SCOPE: 93, CLAUSE: 9\n\nT176 is ground\nX436 is free", fontsize=16, style=filled, fillcolor=lightyellow];
383 [label="383: ','(zero(0), ','(','(!_93, failure(a)), ','(p(0, X436), f(c(X436, s(s(T176))))))) | ?_94 | ','(no(zero(0)), ','(p(0, X436), f(c(X436, s(s(T176)))))), SCOPE: 93, CLAUSE: 9\n\nT176 is ground\nX436 is free", fontsize=16, style=filled, fillcolor=lightyellow];
384 [label="384: ','(zero(0), ','(','(!_93, failure(a)), ','(p(0, X436), f(c(X436, s(s(T176))))))), SCOPE: 95, CLAUSE: 7 | ?_95 | ?_94 | ','(no(zero(0)), ','(p(0, X436), f(c(X436, s(s(T176)))))), SCOPE: 93, CLAUSE: 9\n\nT176 is ground\nX436 is free", fontsize=16, style=filled, fillcolor=lightyellow];
385 [label="385: ','(','(!_93, failure(a)), ','(p(0, X436), f(c(X436, s(s(T176)))))) | ?_95 | ?_94 | ','(no(zero(0)), ','(p(0, X436), f(c(X436, s(s(T176)))))), SCOPE: 93, CLAUSE: 9\n\nT176 is ground\nX436 is free", fontsize=16, style=filled, fillcolor=lightyellow];
386 [label="386: ','(failure(a), ','(p(0, X436), f(c(X436, s(s(T176))))))\n\nT176 is ground\nX436 is free", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: ','(failure(a), ','(p(0, X436), f(c(X436, s(s(T176)))))), SCOPE: 96, CLAUSE: 10\n\nT176 is ground\nX436 is free", fontsize=16, style=filled, fillcolor=lightyellow];
388 [label="388: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: ','(no(zero(T184)), ','(p(T184, X450), f(c(X450, s(s(T185))))))\n\nT184 is ground\nT185 is ground\nX427 is free\nX450 is free\nf(c(T184, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
390 [label="390: ','(no(zero(T184)), ','(p(T184, X450), f(c(X450, s(s(T185)))))), SCOPE: 97, CLAUSE: 8 | ','(no(zero(T184)), ','(p(T184, X450), f(c(X450, s(s(T185)))))), SCOPE: 97, CLAUSE: 9\n\nT184 is ground\nT185 is ground\nX427 is free\nX450 is free\nf(c(T184, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
391 [label="391: ','(','(call(zero(T189)), ','(!_97, failure(a))), ','(p(T189, X450), f(c(X450, s(s(T185)))))) | ','(no(zero(T189)), ','(p(T189, X450), f(c(X450, s(s(T185)))))), SCOPE: 97, CLAUSE: 9\n\nT185 is ground\nT189 is ground\nX427 is free\nX450 is free\nf(c(T189, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
392 [label="392: ','(zero(T189), ','(','(!_97, failure(a)), ','(p(T189, X450), f(c(X450, s(s(T185))))))) | ?_98 | ','(no(zero(T189)), ','(p(T189, X450), f(c(X450, s(s(T185)))))), SCOPE: 97, CLAUSE: 9\n\nT185 is ground\nT189 is ground\nX427 is free\nX450 is free\nf(c(T189, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
393 [label="393: ','(zero(T189), ','(','(!_97, failure(a)), ','(p(T189, X450), f(c(X450, s(s(T185))))))), SCOPE: 99, CLAUSE: 7 | ?_99 | ?_98 | ','(no(zero(T189)), ','(p(T189, X450), f(c(X450, s(s(T185)))))), SCOPE: 97, CLAUSE: 9\n\nT185 is ground\nT189 is ground\nX427 is free\nX450 is free\nf(c(T189, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
394 [label="394: ?_99 | ?_98 | ','(no(zero(T189)), ','(p(T189, X450), f(c(X450, s(s(T185)))))), SCOPE: 97, CLAUSE: 9\n\nT185 is ground\nT189 is ground\nX427 is free\nX450 is free\nf(c(T189, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
395 [label="395: ?_98 | ','(no(zero(T189)), ','(p(T189, X450), f(c(X450, s(s(T185)))))), SCOPE: 97, CLAUSE: 9\n\nT185 is ground\nT189 is ground\nX427 is free\nX450 is free\nf(c(T189, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
396 [label="396: ','(no(zero(T189)), ','(p(T189, X450), f(c(X450, s(s(T185)))))), SCOPE: 97, CLAUSE: 9\n\nT185 is ground\nT189 is ground\nX427 is free\nX450 is free\nf(c(T189, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
397 [label="397: ','(p(T193, X450), f(c(X450, s(s(T185)))))\n\nT185 is ground\nT193 is ground\nX427 is free\nX450 is free\nf(c(T193, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
398 [label="398: ','(p(T193, X450), f(c(X450, s(s(T185))))), SCOPE: 100, CLAUSE: 5 | ','(p(T193, X450), f(c(X450, s(s(T185))))), SCOPE: 100, CLAUSE: 6\n\nT185 is ground\nT193 is ground\nX427 is free\nX450 is free\nf(c(T193, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
399 [label="399: ','(p(T193, X450), f(c(X450, s(s(T185))))), SCOPE: 100, CLAUSE: 6\n\nT185 is ground\nT193 is ground\nX427 is free\nX450 is free\nf(c(T193, s(T185))) !=? f(c(0, X427))", fontsize=16, style=filled, fillcolor=lightyellow];
400 [label="400: f(c(T197, s(s(T185))))\n\nT185 is ground\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
401 [label="401: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
402 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 402 [arrowhead = none ];
402 -> 4;

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

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

405 [label="EVAL with clause\nf(c(0, X8)).\nand substitutionX8 -> T6,\nT3 -> c(0, T6)", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 405 [arrowhead = none ];
405 -> 8;

406 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 406 [arrowhead = none ];
406 -> 9;

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

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

409 [label="EVAL with clause\nf(c(X400, X401)) :- ','(no(zero(X400)), ','(p(X400, X402), f(c(X402, s(X401))))).\nand substitutionX400 -> T146,\nX401 -> T147,\nT3 -> c(T146, T147)", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 409 [arrowhead = none ];
409 -> 359;

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

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

412 [label="ONLY EVAL with clause\nf(c(X383, X384)) :- ','(no(zero(X383)), ','(p(X383, X385), f(c(X385, s(X384))))).\nand substitutionX383 -> 0,\nT6 -> T139,\nX384 -> T139", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 412 [arrowhead = none ];
412 -> 345;

413 [label="EVAL with clause\ng(c(X15, 0)).\nand substitutionX15 -> 0,\nT6 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 413 [arrowhead = none ];
413 -> 15;

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

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

416 [label="ONLY EVAL with clause\ng(c(X36, X37)) :- ','(no(zero(X37)), ','(p(X37, X38), g(c(s(X36), X38)))).\nand substitutionX36 -> 0,\nT6 -> T9,\nX37 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 416 [arrowhead = none ];
416 -> 33;

417 [label="ONLY EVAL with clause\ng(c(X22, X23)) :- ','(no(zero(X23)), ','(p(X23, X24), g(c(s(X22), X24)))).\nand substitutionX22 -> 0,\nX23 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 417 [arrowhead = none ];
417 -> 18;

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

419 [label="ONLY EVAL with clause\nno(X28) :- ','(call(X28), ','(!_4, failure(a))).\nand substitutionX28 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 419 [arrowhead = none ];
419 -> 20;

420 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
20 -> 420 [arrowhead = none ];
420 -> 21;

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

422 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 422 [arrowhead = none ];
422 -> 25;

423 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 423 [arrowhead = none ];
423 -> 26;

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

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

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

427 [label="ONLY EVAL with clause\nno(X42) :- ','(call(X42), ','(!_8, failure(a))).\nand substitutionT9 -> T12,\nX42 -> zero(T12)", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 427 [arrowhead = none ];
427 -> 37;

428 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
37 -> 428 [arrowhead = none ];
428 -> 38;

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

430 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(0, T12)), g(c(X15, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 430 [arrowhead = none ];
430 -> 41;

431 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 431 [arrowhead = none ];
431 -> 42;

432 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 432 [arrowhead = none ];
432 -> 45;

433 [label="ONLY EVAL with clause\nno(X46).\nand substitutionT12 -> T15,\nX46 -> zero(T15)", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 433 [arrowhead = none ];
433 -> 48;

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

435 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(0, T15)), g(c(X15, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 435 [arrowhead = none ];
435 -> 51;

436 [label="EVAL with clause\np(s(X50), X50).\nand substitutionX50 -> T18,\nT15 -> s(T18),\nX38 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 436 [arrowhead = none ];
436 -> 53;

437 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 437 [arrowhead = none ];
437 -> 54;

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

439 [label="EVAL with clause\ng(c(X55, 0)).\nand substitutionX55 -> s(0),\nT18 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 439 [arrowhead = none ];
439 -> 57;

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

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

442 [label="ONLY EVAL with clause\ng(c(X76, X77)) :- ','(no(zero(X77)), ','(p(X77, X78), g(c(s(X76), X78)))).\nand substitutionX76 -> s(0),\nT18 -> T21,\nX77 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 442 [arrowhead = none ];
442 -> 75;

443 [label="ONLY EVAL with clause\ng(c(X62, X63)) :- ','(no(zero(X63)), ','(p(X63, X64), g(c(s(X62), X64)))).\nand substitutionX62 -> s(0),\nX63 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 443 [arrowhead = none ];
443 -> 60;

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

445 [label="ONLY EVAL with clause\nno(X68) :- ','(call(X68), ','(!_13, failure(a))).\nand substitutionX68 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 445 [arrowhead = none ];
445 -> 62;

446 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
62 -> 446 [arrowhead = none ];
446 -> 63;

447 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
63 -> 447 [arrowhead = none ];
447 -> 64;

448 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 448 [arrowhead = none ];
448 -> 65;

449 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 449 [arrowhead = none ];
449 -> 66;

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

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

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

453 [label="ONLY EVAL with clause\nno(X82) :- ','(call(X82), ','(!_17, failure(a))).\nand substitutionT21 -> T24,\nX82 -> zero(T24)", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 453 [arrowhead = none ];
453 -> 78;

454 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
78 -> 454 [arrowhead = none ];
454 -> 79;

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

456 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(s(0), T24)), g(c(X55, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 456 [arrowhead = none ];
456 -> 81;

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

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

459 [label="ONLY EVAL with clause\nno(X86).\nand substitutionT24 -> T27,\nX86 -> zero(T27)", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 459 [arrowhead = none ];
459 -> 84;

460 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
84 -> 460 [arrowhead = none ];
460 -> 85;

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

462 [label="EVAL with clause\np(s(X90), X90).\nand substitutionX90 -> T30,\nT27 -> s(T30),\nX78 -> T30", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 462 [arrowhead = none ];
462 -> 89;

463 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 463 [arrowhead = none ];
463 -> 90;

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

465 [label="EVAL with clause\ng(c(X95, 0)).\nand substitutionX95 -> s(s(0)),\nT30 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 465 [arrowhead = none ];
465 -> 94;

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

467 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 467 [arrowhead = none ];
467 -> 96;

468 [label="ONLY EVAL with clause\ng(c(X116, X117)) :- ','(no(zero(X117)), ','(p(X117, X118), g(c(s(X116), X118)))).\nand substitutionX116 -> s(s(0)),\nT30 -> T33,\nX117 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 468 [arrowhead = none ];
468 -> 119;

469 [label="ONLY EVAL with clause\ng(c(X102, X103)) :- ','(no(zero(X103)), ','(p(X103, X104), g(c(s(X102), X104)))).\nand substitutionX102 -> s(s(0)),\nX103 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 469 [arrowhead = none ];
469 -> 101;

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

471 [label="ONLY EVAL with clause\nno(X108) :- ','(call(X108), ','(!_22, failure(a))).\nand substitutionX108 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 471 [arrowhead = none ];
471 -> 104;

472 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
104 -> 472 [arrowhead = none ];
472 -> 105;

473 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
105 -> 473 [arrowhead = none ];
473 -> 107;

474 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 474 [arrowhead = none ];
474 -> 108;

475 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 475 [arrowhead = none ];
475 -> 109;

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

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

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

479 [label="ONLY EVAL with clause\nno(X122) :- ','(call(X122), ','(!_26, failure(a))).\nand substitutionT33 -> T36,\nX122 -> zero(T36)", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 479 [arrowhead = none ];
479 -> 124;

480 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
124 -> 480 [arrowhead = none ];
480 -> 125;

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

482 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(s(s(0)), T36)), g(c(X95, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 482 [arrowhead = none ];
482 -> 129;

483 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 483 [arrowhead = none ];
483 -> 130;

484 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
130 -> 484 [arrowhead = none ];
484 -> 132;

485 [label="ONLY EVAL with clause\nno(X126).\nand substitutionT36 -> T39,\nX126 -> zero(T39)", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 485 [arrowhead = none ];
485 -> 136;

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

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

488 [label="EVAL with clause\np(s(X130), X130).\nand substitutionX130 -> T42,\nT39 -> s(T42),\nX118 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 488 [arrowhead = none ];
488 -> 142;

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

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

491 [label="EVAL with clause\ng(c(X135, 0)).\nand substitutionX135 -> s(s(s(0))),\nT42 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 491 [arrowhead = none ];
491 -> 147;

492 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
146 -> 492 [arrowhead = none ];
492 -> 148;

493 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 493 [arrowhead = none ];
493 -> 149;

494 [label="ONLY EVAL with clause\ng(c(X156, X157)) :- ','(no(zero(X157)), ','(p(X157, X158), g(c(s(X156), X158)))).\nand substitutionX156 -> s(s(s(0))),\nT42 -> T45,\nX157 -> T45", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 494 [arrowhead = none ];
494 -> 159;

495 [label="ONLY EVAL with clause\ng(c(X142, X143)) :- ','(no(zero(X143)), ','(p(X143, X144), g(c(s(X142), X144)))).\nand substitutionX142 -> s(s(s(0))),\nX143 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 495 [arrowhead = none ];
495 -> 150;

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

497 [label="ONLY EVAL with clause\nno(X148) :- ','(call(X148), ','(!_31, failure(a))).\nand substitutionX148 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 497 [arrowhead = none ];
497 -> 152;

498 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
152 -> 498 [arrowhead = none ];
498 -> 153;

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

500 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 500 [arrowhead = none ];
500 -> 155;

501 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 501 [arrowhead = none ];
501 -> 156;

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

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

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

505 [label="ONLY EVAL with clause\nno(X162) :- ','(call(X162), ','(!_35, failure(a))).\nand substitutionT45 -> T48,\nX162 -> zero(T48)", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 505 [arrowhead = none ];
505 -> 161;

506 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
161 -> 506 [arrowhead = none ];
506 -> 162;

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

508 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(s(s(s(0))), T48)), g(c(X135, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
163 -> 508 [arrowhead = none ];
508 -> 164;

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

510 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
165 -> 510 [arrowhead = none ];
510 -> 166;

511 [label="ONLY EVAL with clause\nno(X166).\nand substitutionT48 -> T51,\nX166 -> zero(T51)", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 511 [arrowhead = none ];
511 -> 167;

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

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

514 [label="EVAL with clause\np(s(X170), X170).\nand substitutionX170 -> T54,\nT51 -> s(T54),\nX158 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 514 [arrowhead = none ];
514 -> 170;

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

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

517 [label="EVAL with clause\ng(c(X175, 0)).\nand substitutionX175 -> s(s(s(s(0)))),\nT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 517 [arrowhead = none ];
517 -> 173;

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

519 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 519 [arrowhead = none ];
519 -> 175;

520 [label="ONLY EVAL with clause\ng(c(X196, X197)) :- ','(no(zero(X197)), ','(p(X197, X198), g(c(s(X196), X198)))).\nand substitutionX196 -> s(s(s(s(0)))),\nT54 -> T57,\nX197 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 520 [arrowhead = none ];
520 -> 185;

521 [label="ONLY EVAL with clause\ng(c(X182, X183)) :- ','(no(zero(X183)), ','(p(X183, X184), g(c(s(X182), X184)))).\nand substitutionX182 -> s(s(s(s(0)))),\nX183 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 521 [arrowhead = none ];
521 -> 176;

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

523 [label="ONLY EVAL with clause\nno(X188) :- ','(call(X188), ','(!_40, failure(a))).\nand substitutionX188 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 523 [arrowhead = none ];
523 -> 178;

524 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
178 -> 524 [arrowhead = none ];
524 -> 179;

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

526 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 526 [arrowhead = none ];
526 -> 181;

527 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 527 [arrowhead = none ];
527 -> 182;

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

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

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

531 [label="ONLY EVAL with clause\nno(X202) :- ','(call(X202), ','(!_44, failure(a))).\nand substitutionT57 -> T60,\nX202 -> zero(T60)", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 531 [arrowhead = none ];
531 -> 192;

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

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

534 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(s(s(s(s(0)))), T60)), g(c(X175, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
194 -> 534 [arrowhead = none ];
534 -> 195;

535 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
195 -> 535 [arrowhead = none ];
535 -> 196;

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

537 [label="ONLY EVAL with clause\nno(X206).\nand substitutionT60 -> T63,\nX206 -> zero(T63)", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 537 [arrowhead = none ];
537 -> 198;

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

539 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(0)))), T63)), g(c(X175, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
199 -> 539 [arrowhead = none ];
539 -> 200;

540 [label="EVAL with clause\np(s(X210), X210).\nand substitutionX210 -> T66,\nT63 -> s(T66),\nX198 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 540 [arrowhead = none ];
540 -> 201;

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

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

543 [label="EVAL with clause\ng(c(X215, 0)).\nand substitutionX215 -> s(s(s(s(s(0))))),\nT66 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
203 -> 543 [arrowhead = none ];
543 -> 204;

544 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
203 -> 544 [arrowhead = none ];
544 -> 205;

545 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
204 -> 545 [arrowhead = none ];
545 -> 206;

546 [label="ONLY EVAL with clause\ng(c(X236, X237)) :- ','(no(zero(X237)), ','(p(X237, X238), g(c(s(X236), X238)))).\nand substitutionX236 -> s(s(s(s(s(0))))),\nT66 -> T69,\nX237 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
205 -> 546 [arrowhead = none ];
546 -> 216;

547 [label="ONLY EVAL with clause\ng(c(X222, X223)) :- ','(no(zero(X223)), ','(p(X223, X224), g(c(s(X222), X224)))).\nand substitutionX222 -> s(s(s(s(s(0))))),\nX223 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 547 [arrowhead = none ];
547 -> 207;

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

549 [label="ONLY EVAL with clause\nno(X228) :- ','(call(X228), ','(!_49, failure(a))).\nand substitutionX228 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
208 -> 549 [arrowhead = none ];
549 -> 209;

550 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
209 -> 550 [arrowhead = none ];
550 -> 210;

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

552 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 552 [arrowhead = none ];
552 -> 212;

553 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
212 -> 553 [arrowhead = none ];
553 -> 213;

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

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

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

557 [label="ONLY EVAL with clause\nno(X242) :- ','(call(X242), ','(!_53, failure(a))).\nand substitutionT69 -> T72,\nX242 -> zero(T72)", fontsize=14, style = filled, fillcolor = lightblue];
217 -> 557 [arrowhead = none ];
557 -> 218;

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

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

560 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(s(s(s(s(s(0))))), T72)), g(c(X215, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
225 -> 560 [arrowhead = none ];
560 -> 226;

561 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
226 -> 561 [arrowhead = none ];
561 -> 227;

562 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
227 -> 562 [arrowhead = none ];
562 -> 228;

563 [label="ONLY EVAL with clause\nno(X246).\nand substitutionT72 -> T75,\nX246 -> zero(T75)", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 563 [arrowhead = none ];
563 -> 232;

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

565 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(0))))), T75)), g(c(X215, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
234 -> 565 [arrowhead = none ];
565 -> 237;

566 [label="EVAL with clause\np(s(X250), X250).\nand substitutionX250 -> T78,\nT75 -> s(T78),\nX238 -> T78", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 566 [arrowhead = none ];
566 -> 238;

567 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
237 -> 567 [arrowhead = none ];
567 -> 239;

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

569 [label="EVAL with clause\ng(c(X255, 0)).\nand substitutionX255 -> s(s(s(s(s(s(0)))))),\nT78 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
244 -> 569 [arrowhead = none ];
569 -> 245;

570 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
244 -> 570 [arrowhead = none ];
570 -> 246;

571 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
245 -> 571 [arrowhead = none ];
571 -> 247;

572 [label="ONLY EVAL with clause\ng(c(X276, X277)) :- ','(no(zero(X277)), ','(p(X277, X278), g(c(s(X276), X278)))).\nand substitutionX276 -> s(s(s(s(s(s(0)))))),\nT78 -> T81,\nX277 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
246 -> 572 [arrowhead = none ];
572 -> 257;

573 [label="ONLY EVAL with clause\ng(c(X262, X263)) :- ','(no(zero(X263)), ','(p(X263, X264), g(c(s(X262), X264)))).\nand substitutionX262 -> s(s(s(s(s(s(0)))))),\nX263 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
247 -> 573 [arrowhead = none ];
573 -> 248;

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

575 [label="ONLY EVAL with clause\nno(X268) :- ','(call(X268), ','(!_58, failure(a))).\nand substitutionX268 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
249 -> 575 [arrowhead = none ];
575 -> 250;

576 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
250 -> 576 [arrowhead = none ];
576 -> 251;

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

578 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
252 -> 578 [arrowhead = none ];
578 -> 253;

579 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
253 -> 579 [arrowhead = none ];
579 -> 254;

580 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
254 -> 580 [arrowhead = none ];
580 -> 255;

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

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

583 [label="ONLY EVAL with clause\nno(X282) :- ','(call(X282), ','(!_62, failure(a))).\nand substitutionT81 -> T84,\nX282 -> zero(T84)", fontsize=14, style = filled, fillcolor = lightblue];
258 -> 583 [arrowhead = none ];
583 -> 259;

584 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
259 -> 584 [arrowhead = none ];
584 -> 260;

585 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
260 -> 585 [arrowhead = none ];
585 -> 261;

586 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(s(s(s(s(s(s(0)))))), T84)), g(c(X255, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
261 -> 586 [arrowhead = none ];
586 -> 262;

587 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
262 -> 587 [arrowhead = none ];
587 -> 263;

588 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
263 -> 588 [arrowhead = none ];
588 -> 264;

589 [label="ONLY EVAL with clause\nno(X286).\nand substitutionT84 -> T87,\nX286 -> zero(T87)", fontsize=14, style = filled, fillcolor = lightblue];
264 -> 589 [arrowhead = none ];
589 -> 265;

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

591 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(s(0)))))), T87)), g(c(X255, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
266 -> 591 [arrowhead = none ];
591 -> 267;

592 [label="EVAL with clause\np(s(X290), X290).\nand substitutionX290 -> T90,\nT87 -> s(T90),\nX278 -> T90", fontsize=14, style = filled, fillcolor = lightblue];
267 -> 592 [arrowhead = none ];
592 -> 268;

593 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
267 -> 593 [arrowhead = none ];
593 -> 269;

594 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
268 -> 594 [arrowhead = none ];
594 -> 270;

595 [label="EVAL with clause\ng(c(X295, 0)).\nand substitutionX295 -> s(s(s(s(s(s(s(0))))))),\nT90 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
270 -> 595 [arrowhead = none ];
595 -> 271;

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

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

598 [label="ONLY EVAL with clause\ng(c(X316, X317)) :- ','(no(zero(X317)), ','(p(X317, X318), g(c(s(X316), X318)))).\nand substitutionX316 -> s(s(s(s(s(s(s(0))))))),\nT90 -> T93,\nX317 -> T93", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 598 [arrowhead = none ];
598 -> 294;

599 [label="ONLY EVAL with clause\ng(c(X302, X303)) :- ','(no(zero(X303)), ','(p(X303, X304), g(c(s(X302), X304)))).\nand substitutionX302 -> s(s(s(s(s(s(s(0))))))),\nX303 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
273 -> 599 [arrowhead = none ];
599 -> 274;

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

601 [label="ONLY EVAL with clause\nno(X308) :- ','(call(X308), ','(!_67, failure(a))).\nand substitutionX308 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
275 -> 601 [arrowhead = none ];
601 -> 276;

602 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
276 -> 602 [arrowhead = none ];
602 -> 277;

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

604 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
278 -> 604 [arrowhead = none ];
604 -> 279;

605 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
279 -> 605 [arrowhead = none ];
605 -> 280;

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

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

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

609 [label="ONLY EVAL with clause\nno(X322) :- ','(call(X322), ','(!_71, failure(a))).\nand substitutionT93 -> T96,\nX322 -> zero(T96)", fontsize=14, style = filled, fillcolor = lightblue];
295 -> 609 [arrowhead = none ];
609 -> 296;

610 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
296 -> 610 [arrowhead = none ];
610 -> 297;

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

612 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(s(s(s(s(s(s(s(0))))))), T96)), g(c(X295, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
298 -> 612 [arrowhead = none ];
612 -> 299;

613 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
299 -> 613 [arrowhead = none ];
613 -> 300;

614 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
300 -> 614 [arrowhead = none ];
614 -> 301;

615 [label="ONLY EVAL with clause\nno(X326).\nand substitutionT96 -> T99,\nX326 -> zero(T99)", fontsize=14, style = filled, fillcolor = lightblue];
301 -> 615 [arrowhead = none ];
615 -> 302;

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

617 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(s(s(s(s(s(s(0))))))), T99)), g(c(X295, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
303 -> 617 [arrowhead = none ];
617 -> 304;

618 [label="EVAL with clause\np(s(X330), X330).\nand substitutionX330 -> T102,\nT99 -> s(T102),\nX318 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
304 -> 618 [arrowhead = none ];
618 -> 305;

619 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
304 -> 619 [arrowhead = none ];
619 -> 306;

620 [label="GENERALIZATION\nT103 <-- s(s(s(s(s(s(s(0)))))))\n\nNew Knowledge:\nT103 is ground", fontsize=14, style = filled, fillcolor = violet];
305 -> 620 [arrowhead = none ];
620 -> 315;

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

622 [label="EVAL with clause\ng(c(X337, 0)).\nand substitutionT103 -> T108,\nX337 -> s(T108),\nT102 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
316 -> 622 [arrowhead = none ];
622 -> 317;

623 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
316 -> 623 [arrowhead = none ];
623 -> 318;

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

625 [label="ONLY EVAL with clause\ng(c(X358, X359)) :- ','(no(zero(X359)), ','(p(X359, X360), g(c(s(X358), X360)))).\nand substitutionT103 -> T120,\nX358 -> s(T120),\nT102 -> T121,\nX359 -> T121", fontsize=14, style = filled, fillcolor = lightblue];
318 -> 625 [arrowhead = none ];
625 -> 329;

626 [label="ONLY EVAL with clause\ng(c(X344, X345)) :- ','(no(zero(X345)), ','(p(X345, X346), g(c(s(X344), X346)))).\nand substitutionT108 -> T112,\nX344 -> s(T112),\nX345 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
319 -> 626 [arrowhead = none ];
626 -> 320;

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

628 [label="ONLY EVAL with clause\nno(X350) :- ','(call(X350), ','(!_76, failure(a))).\nand substitutionX350 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
321 -> 628 [arrowhead = none ];
628 -> 322;

629 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
322 -> 629 [arrowhead = none ];
629 -> 323;

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

631 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
324 -> 631 [arrowhead = none ];
631 -> 325;

632 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
325 -> 632 [arrowhead = none ];
632 -> 326;

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

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

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

636 [label="ONLY EVAL with clause\nno(X364) :- ','(call(X364), ','(!_80, failure(a))).\nand substitutionT121 -> T125,\nX364 -> zero(T125)", fontsize=14, style = filled, fillcolor = lightblue];
330 -> 636 [arrowhead = none ];
636 -> 331;

637 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
331 -> 637 [arrowhead = none ];
637 -> 332;

638 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
332 -> 638 [arrowhead = none ];
638 -> 333;

639 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (g(c(s(T120), T125)), g(c(X337, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
333 -> 639 [arrowhead = none ];
639 -> 334;

640 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
334 -> 640 [arrowhead = none ];
640 -> 335;

641 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
335 -> 641 [arrowhead = none ];
641 -> 336;

642 [label="ONLY EVAL with clause\nno(X368).\nand substitutionT125 -> T129,\nX368 -> zero(T129)", fontsize=14, style = filled, fillcolor = lightblue];
336 -> 642 [arrowhead = none ];
642 -> 337;

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

644 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (g(c(s(T120), T129)), g(c(X337, 0)))", fontsize=14, style = filled, fillcolor = lightgreen];
338 -> 644 [arrowhead = none ];
644 -> 339;

645 [label="EVAL with clause\np(s(X372), X372).\nand substitutionX372 -> T133,\nT129 -> s(T133),\nX360 -> T133", fontsize=14, style = filled, fillcolor = lightblue];
339 -> 645 [arrowhead = none ];
645 -> 340;

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

647 [label="INSTANCE with matching:\nT103 -> s(T120)\nT102 -> T133", fontsize=14, style = filled, fillcolor = lightgrey];
340 -> 647 [arrowhead = none , style=dashed];
647 -> 315[style=dashed];

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

649 [label="ONLY EVAL with clause\nno(X391) :- ','(call(X391), ','(!_84, failure(a))).\nand substitutionX391 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
346 -> 649 [arrowhead = none ];
649 -> 349;

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

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

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

653 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
352 -> 653 [arrowhead = none ];
653 -> 353;

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

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

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

657 [label="ONLY EVAL with clause\nno(X408) :- ','(call(X408), ','(!_88, failure(a))).\nand substitutionT146 -> T153,\nX408 -> zero(T153)", fontsize=14, style = filled, fillcolor = lightblue];
362 -> 657 [arrowhead = none ];
657 -> 363;

658 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
363 -> 658 [arrowhead = none ];
658 -> 364;

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

660 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (f(c(T153, T147)), f(c(0, X8)))", fontsize=14, style = filled, fillcolor = lightgreen];
365 -> 660 [arrowhead = none ];
660 -> 366;

661 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
366 -> 661 [arrowhead = none ];
661 -> 367;

662 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
367 -> 662 [arrowhead = none ];
662 -> 368;

663 [label="ONLY EVAL with clause\nno(X414).\nand substitutionT153 -> T159,\nX414 -> zero(T159)", fontsize=14, style = filled, fillcolor = lightblue];
368 -> 663 [arrowhead = none ];
663 -> 369;

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

665 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(c(T159, T147)), f(c(0, X8)))", fontsize=14, style = filled, fillcolor = lightgreen];
370 -> 665 [arrowhead = none ];
665 -> 371;

666 [label="EVAL with clause\np(s(X420), X420).\nand substitutionX420 -> T165,\nT159 -> s(T165),\nX402 -> T165", fontsize=14, style = filled, fillcolor = lightblue];
371 -> 666 [arrowhead = none ];
666 -> 372;

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

668 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
372 -> 668 [arrowhead = none ];
668 -> 374;

669 [label="SPLIT 2\nnew knowledge:\nT165 is ground\nT147 is ground", fontsize=14, style = filled, fillcolor = violet];
372 -> 669 [arrowhead = none ];
669 -> 375;

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

671 [label="INSTANCE with matching:\nT103 -> T165\nT102 -> T147", fontsize=14, style = filled, fillcolor = lightgrey];
375 -> 671 [arrowhead = none , style=dashed];
671 -> 315[style=dashed];

672 [label="EVAL with clause\nf(c(0, X427)).\nand substitutionT165 -> 0,\nT147 -> T172,\nX427 -> s(T172)", fontsize=14, style = filled, fillcolor = lightblue];
376 -> 672 [arrowhead = none ];
672 -> 377;

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

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

675 [label="ONLY EVAL with clause\nf(c(X448, X449)) :- ','(no(zero(X448)), ','(p(X448, X450), f(c(X450, s(X449))))).\nand substitutionT165 -> T184,\nX448 -> T184,\nT147 -> T185,\nX449 -> s(T185)", fontsize=14, style = filled, fillcolor = lightblue];
378 -> 675 [arrowhead = none ];
675 -> 389;

676 [label="ONLY EVAL with clause\nf(c(X434, X435)) :- ','(no(zero(X434)), ','(p(X434, X436), f(c(X436, s(X435))))).\nand substitutionX434 -> 0,\nT172 -> T176,\nX435 -> s(T176)", fontsize=14, style = filled, fillcolor = lightblue];
379 -> 676 [arrowhead = none ];
676 -> 380;

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

678 [label="ONLY EVAL with clause\nno(X440) :- ','(call(X440), ','(!_93, failure(a))).\nand substitutionX440 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
381 -> 678 [arrowhead = none ];
678 -> 382;

679 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
382 -> 679 [arrowhead = none ];
679 -> 383;

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

681 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
384 -> 681 [arrowhead = none ];
681 -> 385;

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

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

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

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

686 [label="ONLY EVAL with clause\nno(X454) :- ','(call(X454), ','(!_97, failure(a))).\nand substitutionT184 -> T189,\nX454 -> zero(T189)", fontsize=14, style = filled, fillcolor = lightblue];
390 -> 686 [arrowhead = none ];
686 -> 391;

687 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
391 -> 687 [arrowhead = none ];
687 -> 392;

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

689 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (f(c(T189, s(T185))), f(c(0, X427)))", fontsize=14, style = filled, fillcolor = lightgreen];
393 -> 689 [arrowhead = none ];
689 -> 394;

690 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
394 -> 690 [arrowhead = none ];
690 -> 395;

691 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
395 -> 691 [arrowhead = none ];
691 -> 396;

692 [label="ONLY EVAL with clause\nno(X458).\nand substitutionT189 -> T193,\nX458 -> zero(T193)", fontsize=14, style = filled, fillcolor = lightblue];
396 -> 692 [arrowhead = none ];
692 -> 397;

693 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
397 -> 693 [arrowhead = none ];
693 -> 398;

694 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(c(T193, s(T185))), f(c(0, X427)))", fontsize=14, style = filled, fillcolor = lightgreen];
398 -> 694 [arrowhead = none ];
694 -> 399;

695 [label="EVAL with clause\np(s(X462), X462).\nand substitutionX462 -> T197,\nT193 -> s(T197),\nX450 -> T197", fontsize=14, style = filled, fillcolor = lightblue];
399 -> 695 [arrowhead = none ];
695 -> 400;

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

697 [label="INSTANCE with matching:\nT165 -> T197\nT147 -> s(T185)", fontsize=14, style = filled, fillcolor = lightgrey];
400 -> 697 [arrowhead = none , style=dashed];
697 -> 374[style=dashed];

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(c(0, z0)) → U1(f8_in(z0), c(0, z0))
f1_in(c(s(z0), z1)) → U2(f372_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(0, z0)) → f1_out1
U1(f8_out2, c(0, z0)) → f1_out1
U2(f372_out1, c(s(z0), z1)) → f1_out1
f315_in(z0, 0) → f315_out1
f315_in(z0, s(z1)) → U3(f315_in(s(z0), z1), z0, s(z1))
U3(f315_out1, z0, s(z1)) → f315_out1
f374_in(0, z0) → f374_out1
f374_in(s(z0), z1) → U4(f374_in(z0, s(z1)), s(z0), z1)
U4(f374_out1, s(z0), z1) → f374_out1
f10_in(0) → f10_out1
f10_in(s(0)) → f10_out1
f10_in(s(s(0))) → f10_out1
f10_in(s(s(s(0)))) → f10_out1
f10_in(s(s(s(s(0))))) → f10_out1
f10_in(s(s(s(s(s(0)))))) → f10_out1
f10_in(s(s(s(s(s(s(0))))))) → f10_out1
f10_in(s(s(s(s(s(s(s(0)))))))) → f10_out1
f10_in(s(s(s(s(s(s(s(s(z0))))))))) → U5(f315_in(s(s(s(s(s(s(s(0))))))), z0), s(s(s(s(s(s(s(s(z0)))))))))
U5(f315_out1, s(s(s(s(s(s(s(s(z0))))))))) → f10_out1
f372_in(z0, z1) → U6(f374_in(z0, z1), z0, z1)
U6(f374_out1, z0, z1) → U7(f315_in(z0, z1), z0, z1)
U7(f315_out1, z0, z1) → f372_out1
f8_in(z0) → U8(f10_in(z0), f11_in(z0), z0)
U8(f10_out1, z0, z1) → f8_out1
U8(z0, f11_out1, z1) → f8_out2

Tuples:

F1_IN(c(0, z0)) → c1(U1'(f8_in(z0), c(0, z0)), F8_IN(z0))
F1_IN(c(s(z0), z1)) → c2(U2'(f372_in(z0, z1), c(s(z0), z1)), F372_IN(z0, z1))
F315_IN(z0, s(z1)) → c7(U3'(f315_in(s(z0), z1), z0, s(z1)), F315_IN(s(z0), z1))
F374_IN(s(z0), z1) → c10(U4'(f374_in(z0, s(z1)), s(z0), z1), F374_IN(z0, s(z1)))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c20(U5'(f315_in(s(s(s(s(s(s(s(0))))))), z0), s(s(s(s(s(s(s(s(z0))))))))), F315_IN(s(s(s(s(s(s(s(0))))))), z0))
F372_IN(z0, z1) → c22(U6'(f374_in(z0, z1), z0, z1), F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c23(U7'(f315_in(z0, z1), z0, z1), F315_IN(z0, z1))
F8_IN(z0) → c25(U8'(f10_in(z0), f11_in(z0), z0), F10_IN(z0))

S tuples:

F1_IN(c(0, z0)) → c1(U1'(f8_in(z0), c(0, z0)), F8_IN(z0))
F1_IN(c(s(z0), z1)) → c2(U2'(f372_in(z0, z1), c(s(z0), z1)), F372_IN(z0, z1))
F315_IN(z0, s(z1)) → c7(U3'(f315_in(s(z0), z1), z0, s(z1)), F315_IN(s(z0), z1))
F374_IN(s(z0), z1) → c10(U4'(f374_in(z0, s(z1)), s(z0), z1), F374_IN(z0, s(z1)))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c20(U5'(f315_in(s(s(s(s(s(s(s(0))))))), z0), s(s(s(s(s(s(s(s(z0))))))))), F315_IN(s(s(s(s(s(s(s(0))))))), z0))
F372_IN(z0, z1) → c22(U6'(f374_in(z0, z1), z0, z1), F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c23(U7'(f315_in(z0, z1), z0, z1), F315_IN(z0, z1))
F8_IN(z0) → c25(U8'(f10_in(z0), f11_in(z0), z0), F10_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f315_in, U3, f374_in, U4, f10_in, U5, f372_in, U6, U7, f8_in, U8

Defined Pair Symbols:

F1_IN, F315_IN, F374_IN, F10_IN, F372_IN, U6', F8_IN

Compound Symbols:

c1, c2, c7, c10, c20, c22, c23, c25

(17) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(c(0, z0)) → U1(f8_in(z0), c(0, z0))
f1_in(c(s(z0), z1)) → U2(f372_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(0, z0)) → f1_out1
U1(f8_out2, c(0, z0)) → f1_out1
U2(f372_out1, c(s(z0), z1)) → f1_out1
f315_in(z0, 0) → f315_out1
f315_in(z0, s(z1)) → U3(f315_in(s(z0), z1), z0, s(z1))
U3(f315_out1, z0, s(z1)) → f315_out1
f374_in(0, z0) → f374_out1
f374_in(s(z0), z1) → U4(f374_in(z0, s(z1)), s(z0), z1)
U4(f374_out1, s(z0), z1) → f374_out1
f10_in(0) → f10_out1
f10_in(s(0)) → f10_out1
f10_in(s(s(0))) → f10_out1
f10_in(s(s(s(0)))) → f10_out1
f10_in(s(s(s(s(0))))) → f10_out1
f10_in(s(s(s(s(s(0)))))) → f10_out1
f10_in(s(s(s(s(s(s(0))))))) → f10_out1
f10_in(s(s(s(s(s(s(s(0)))))))) → f10_out1
f10_in(s(s(s(s(s(s(s(s(z0))))))))) → U5(f315_in(s(s(s(s(s(s(s(0))))))), z0), s(s(s(s(s(s(s(s(z0)))))))))
U5(f315_out1, s(s(s(s(s(s(s(s(z0))))))))) → f10_out1
f372_in(z0, z1) → U6(f374_in(z0, z1), z0, z1)
U6(f374_out1, z0, z1) → U7(f315_in(z0, z1), z0, z1)
U7(f315_out1, z0, z1) → f372_out1
f8_in(z0) → U8(f10_in(z0), f11_in(z0), z0)
U8(f10_out1, z0, z1) → f8_out1
U8(z0, f11_out1, z1) → f8_out2

Tuples:

F315_IN(z0, s(z1)) → c7(U3'(f315_in(s(z0), z1), z0, s(z1)), F315_IN(s(z0), z1))
F374_IN(s(z0), z1) → c10(U4'(f374_in(z0, s(z1)), s(z0), z1), F374_IN(z0, s(z1)))
F1_IN(c(0, z0)) → c3(U1'(f8_in(z0), c(0, z0)))
F1_IN(c(0, z0)) → c3(F8_IN(z0))
F1_IN(c(s(z0), z1)) → c3(U2'(f372_in(z0, z1), c(s(z0), z1)))
F1_IN(c(s(z0), z1)) → c3(F372_IN(z0, z1))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(U5'(f315_in(s(s(s(s(s(s(s(0))))))), z0), s(s(s(s(s(s(s(s(z0))))))))))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(F315_IN(s(s(s(s(s(s(s(0))))))), z0))
F372_IN(z0, z1) → c3(U6'(f374_in(z0, z1), z0, z1))
F372_IN(z0, z1) → c3(F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3(U7'(f315_in(z0, z1), z0, z1))
U6'(f374_out1, z0, z1) → c3(F315_IN(z0, z1))
F8_IN(z0) → c3(U8'(f10_in(z0), f11_in(z0), z0))
F8_IN(z0) → c3(F10_IN(z0))

S tuples:

F315_IN(z0, s(z1)) → c7(U3'(f315_in(s(z0), z1), z0, s(z1)), F315_IN(s(z0), z1))
F374_IN(s(z0), z1) → c10(U4'(f374_in(z0, s(z1)), s(z0), z1), F374_IN(z0, s(z1)))
F1_IN(c(0, z0)) → c3(U1'(f8_in(z0), c(0, z0)))
F1_IN(c(0, z0)) → c3(F8_IN(z0))
F1_IN(c(s(z0), z1)) → c3(U2'(f372_in(z0, z1), c(s(z0), z1)))
F1_IN(c(s(z0), z1)) → c3(F372_IN(z0, z1))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(U5'(f315_in(s(s(s(s(s(s(s(0))))))), z0), s(s(s(s(s(s(s(s(z0))))))))))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(F315_IN(s(s(s(s(s(s(s(0))))))), z0))
F372_IN(z0, z1) → c3(U6'(f374_in(z0, z1), z0, z1))
F372_IN(z0, z1) → c3(F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3(U7'(f315_in(z0, z1), z0, z1))
U6'(f374_out1, z0, z1) → c3(F315_IN(z0, z1))
F8_IN(z0) → c3(U8'(f10_in(z0), f11_in(z0), z0))
F8_IN(z0) → c3(F10_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f315_in, U3, f374_in, U4, f10_in, U5, f372_in, U6, U7, f8_in, U8

Defined Pair Symbols:

F315_IN, F374_IN, F1_IN, F10_IN, F372_IN, U6', F8_IN

Compound Symbols:

c7, c10, c3

(19) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 7 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(c(0, z0)) → U1(f8_in(z0), c(0, z0))
f1_in(c(s(z0), z1)) → U2(f372_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(0, z0)) → f1_out1
U1(f8_out2, c(0, z0)) → f1_out1
U2(f372_out1, c(s(z0), z1)) → f1_out1
f315_in(z0, 0) → f315_out1
f315_in(z0, s(z1)) → U3(f315_in(s(z0), z1), z0, s(z1))
U3(f315_out1, z0, s(z1)) → f315_out1
f374_in(0, z0) → f374_out1
f374_in(s(z0), z1) → U4(f374_in(z0, s(z1)), s(z0), z1)
U4(f374_out1, s(z0), z1) → f374_out1
f10_in(0) → f10_out1
f10_in(s(0)) → f10_out1
f10_in(s(s(0))) → f10_out1
f10_in(s(s(s(0)))) → f10_out1
f10_in(s(s(s(s(0))))) → f10_out1
f10_in(s(s(s(s(s(0)))))) → f10_out1
f10_in(s(s(s(s(s(s(0))))))) → f10_out1
f10_in(s(s(s(s(s(s(s(0)))))))) → f10_out1
f10_in(s(s(s(s(s(s(s(s(z0))))))))) → U5(f315_in(s(s(s(s(s(s(s(0))))))), z0), s(s(s(s(s(s(s(s(z0)))))))))
U5(f315_out1, s(s(s(s(s(s(s(s(z0))))))))) → f10_out1
f372_in(z0, z1) → U6(f374_in(z0, z1), z0, z1)
U6(f374_out1, z0, z1) → U7(f315_in(z0, z1), z0, z1)
U7(f315_out1, z0, z1) → f372_out1
f8_in(z0) → U8(f10_in(z0), f11_in(z0), z0)
U8(f10_out1, z0, z1) → f8_out1
U8(z0, f11_out1, z1) → f8_out2

Tuples:

F1_IN(c(0, z0)) → c3(F8_IN(z0))
F1_IN(c(s(z0), z1)) → c3(F372_IN(z0, z1))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(F315_IN(s(s(s(s(s(s(s(0))))))), z0))
F372_IN(z0, z1) → c3(U6'(f374_in(z0, z1), z0, z1))
F372_IN(z0, z1) → c3(F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3(F315_IN(z0, z1))
F8_IN(z0) → c3(F10_IN(z0))
F315_IN(z0, s(z1)) → c7(F315_IN(s(z0), z1))
F374_IN(s(z0), z1) → c10(F374_IN(z0, s(z1)))
F1_IN(c(0, z0)) → c3
F1_IN(c(s(z0), z1)) → c3
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3
U6'(f374_out1, z0, z1) → c3
F8_IN(z0) → c3

S tuples:

F1_IN(c(0, z0)) → c3(F8_IN(z0))
F1_IN(c(s(z0), z1)) → c3(F372_IN(z0, z1))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(F315_IN(s(s(s(s(s(s(s(0))))))), z0))
F372_IN(z0, z1) → c3(U6'(f374_in(z0, z1), z0, z1))
F372_IN(z0, z1) → c3(F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3(F315_IN(z0, z1))
F8_IN(z0) → c3(F10_IN(z0))
F315_IN(z0, s(z1)) → c7(F315_IN(s(z0), z1))
F374_IN(s(z0), z1) → c10(F374_IN(z0, s(z1)))
F1_IN(c(0, z0)) → c3
F1_IN(c(s(z0), z1)) → c3
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3
U6'(f374_out1, z0, z1) → c3
F8_IN(z0) → c3

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f315_in, U3, f374_in, U4, f10_in, U5, f372_in, U6, U7, f8_in, U8

Defined Pair Symbols:

F1_IN, F10_IN, F372_IN, U6', F8_IN, F315_IN, F374_IN

Compound Symbols:

c3, c7, c10, c3

(21) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F1_IN(c(0, z0)) → c3(F8_IN(z0))
F1_IN(c(s(z0), z1)) → c3(F372_IN(z0, z1))
F372_IN(z0, z1) → c3(U6'(f374_in(z0, z1), z0, z1))
F372_IN(z0, z1) → c3(F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3(F315_IN(z0, z1))
F8_IN(z0) → c3(F10_IN(z0))
F1_IN(c(0, z0)) → c3
F1_IN(c(s(z0), z1)) → c3
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3
U6'(f374_out1, z0, z1) → c3
F8_IN(z0) → c3
F8_IN(z0) → c3(F10_IN(z0))
F8_IN(z0) → c3
F372_IN(z0, z1) → c3(U6'(f374_in(z0, z1), z0, z1))
F372_IN(z0, z1) → c3(F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3(F315_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(F315_IN(s(s(s(s(s(s(s(0))))))), z0))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(c(0, z0)) → U1(f8_in(z0), c(0, z0))
f1_in(c(s(z0), z1)) → U2(f372_in(z0, z1), c(s(z0), z1))
U1(f8_out1, c(0, z0)) → f1_out1
U1(f8_out2, c(0, z0)) → f1_out1
U2(f372_out1, c(s(z0), z1)) → f1_out1
f315_in(z0, 0) → f315_out1
f315_in(z0, s(z1)) → U3(f315_in(s(z0), z1), z0, s(z1))
U3(f315_out1, z0, s(z1)) → f315_out1
f374_in(0, z0) → f374_out1
f374_in(s(z0), z1) → U4(f374_in(z0, s(z1)), s(z0), z1)
U4(f374_out1, s(z0), z1) → f374_out1
f10_in(0) → f10_out1
f10_in(s(0)) → f10_out1
f10_in(s(s(0))) → f10_out1
f10_in(s(s(s(0)))) → f10_out1
f10_in(s(s(s(s(0))))) → f10_out1
f10_in(s(s(s(s(s(0)))))) → f10_out1
f10_in(s(s(s(s(s(s(0))))))) → f10_out1
f10_in(s(s(s(s(s(s(s(0)))))))) → f10_out1
f10_in(s(s(s(s(s(s(s(s(z0))))))))) → U5(f315_in(s(s(s(s(s(s(s(0))))))), z0), s(s(s(s(s(s(s(s(z0)))))))))
U5(f315_out1, s(s(s(s(s(s(s(s(z0))))))))) → f10_out1
f372_in(z0, z1) → U6(f374_in(z0, z1), z0, z1)
U6(f374_out1, z0, z1) → U7(f315_in(z0, z1), z0, z1)
U7(f315_out1, z0, z1) → f372_out1
f8_in(z0) → U8(f10_in(z0), f11_in(z0), z0)
U8(f10_out1, z0, z1) → f8_out1
U8(z0, f11_out1, z1) → f8_out2

Tuples:

F1_IN(c(0, z0)) → c3(F8_IN(z0))
F1_IN(c(s(z0), z1)) → c3(F372_IN(z0, z1))
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(F315_IN(s(s(s(s(s(s(s(0))))))), z0))
F372_IN(z0, z1) → c3(U6'(f374_in(z0, z1), z0, z1))
F372_IN(z0, z1) → c3(F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3(F315_IN(z0, z1))
F8_IN(z0) → c3(F10_IN(z0))
F315_IN(z0, s(z1)) → c7(F315_IN(s(z0), z1))
F374_IN(s(z0), z1) → c10(F374_IN(z0, s(z1)))
F1_IN(c(0, z0)) → c3
F1_IN(c(s(z0), z1)) → c3
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3
U6'(f374_out1, z0, z1) → c3
F8_IN(z0) → c3

S tuples:

F315_IN(z0, s(z1)) → c7(F315_IN(s(z0), z1))
F374_IN(s(z0), z1) → c10(F374_IN(z0, s(z1)))

K tuples:

F1_IN(c(0, z0)) → c3(F8_IN(z0))
F1_IN(c(s(z0), z1)) → c3(F372_IN(z0, z1))
F372_IN(z0, z1) → c3(U6'(f374_in(z0, z1), z0, z1))
F372_IN(z0, z1) → c3(F374_IN(z0, z1))
U6'(f374_out1, z0, z1) → c3(F315_IN(z0, z1))
F8_IN(z0) → c3(F10_IN(z0))
F1_IN(c(0, z0)) → c3
F1_IN(c(s(z0), z1)) → c3
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3
U6'(f374_out1, z0, z1) → c3
F8_IN(z0) → c3
F10_IN(s(s(s(s(s(s(s(s(z0))))))))) → c3(F315_IN(s(s(s(s(s(s(s(0))))))), z0))

Defined Rule Symbols:

f1_in, U1, U2, f315_in, U3, f374_in, U4, f10_in, U5, f372_in, U6, U7, f8_in, U8

Defined Pair Symbols:

F1_IN, F10_IN, F372_IN, U6', F8_IN, F315_IN, F374_IN

Compound Symbols:

c3, c7, c10, c3