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

(0) Obligation:

Clauses:

goal :- ','(np(S1, S2, S), verb(S2, S3, S)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), verb(S1, [], Meaning)).
parse(S0, Meaning) :- ','(np(S0, S1, Meaning), ','(verb(S1, S2, Meaning), =(S2, []))).
np(Si, So, S) :- ','(det(Si, St, T), ','(noun(St, So, N), comb(T, N, S))).
comb(a, -(N, s), s(s, N, V)).
comb(the, -(N, P), s(P, N, V)).
det(.(a, S), S, a).
det(.(the, S), S, the).
noun(.(book, S), S, -(book, s)).
noun(.(books, S), S, -(book, p)).
noun(.(box, S), S, -(box, s)).
noun(.(boxes, S), S, -(box, p)).
verb(.(falls, So), So, s(s, N, fall)).
verb(.(fall, So), So, s(p, N, fall)).
verb(.(flies, So), So, s(s, N, fly)).
verb(.(fly, So), So, s(p, N, fly)).

Query: goal()

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: goal\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: goal, SCOPE: 1, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(np(X1, X2, X3), verb(X2, X4, X3))\n\nX1 is free\nX2 is free\nX3 is free\nX4 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(np(X1, X2, X3), verb(X2, X4, X3)), SCOPE: 2, CLAUSE: 3\n\nX1 is free\nX2 is free\nX3 is free\nX4 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(','(det(X26, X23, X24), ','(noun(X23, X27, X25), comb(X24, X25, X28))), verb(X27, X4, X28))\n\nX4 is free\nX26 is free\nX27 is free\nX28 is free\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(','(det(X26, X23, X24), ','(noun(X23, X27, X25), comb(X24, X25, X28))), verb(X27, X4, X28)), SCOPE: 3, CLAUSE: 6 | ','(','(det(X26, X23, X24), ','(noun(X23, X27, X25), comb(X24, X25, X28))), verb(X27, X4, X28)), SCOPE: 3, CLAUSE: 7\n\nX4 is free\nX26 is free\nX27 is free\nX28 is free\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(','(det(X26, X23, X24), ','(noun(X23, X27, X25), comb(X24, X25, X28))), verb(X27, X4, X28)), SCOPE: 3, CLAUSE: 6\n\nX4 is free\nX26 is free\nX27 is free\nX28 is free\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(','(det(X26, X23, X24), ','(noun(X23, X27, X25), comb(X24, X25, X28))), verb(X27, X4, X28)), SCOPE: 3, CLAUSE: 7\n\nX4 is free\nX26 is free\nX27 is free\nX28 is free\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28))\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 8 | ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 9 | ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 10 | ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 11\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 8\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 9 | ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 10 | ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 11\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(comb(a, -(book, s), X28), verb(X48, X4, X28))\n\nX4 is free\nX28 is free\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(comb(a, -(book, s), X28), verb(X48, X4, X28)), SCOPE: 5, CLAUSE: 4 | ','(comb(a, -(book, s), X28), verb(X48, X4, X28)), SCOPE: 5, CLAUSE: 5\n\nX4 is free\nX28 is free\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(comb(a, -(book, s), X28), verb(X48, X4, X28)), SCOPE: 5, CLAUSE: 4\n\nX4 is free\nX28 is free\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(comb(a, -(book, s), X28), verb(X48, X4, X28)), SCOPE: 5, CLAUSE: 5\n\nX4 is free\nX28 is free\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: verb(X48, X4, s(s, book, X63))\n\nX4 is free\nX48 is free\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 12 | verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 13 | verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 14 | verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 15\n\nX4 is free\nX48 is free\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 12\n\nX4 is free\nX48 is free\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 13 | verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 14 | verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 15\n\nX4 is free\nX48 is free\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 14 | verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 15\n\nX4 is free\nX48 is free\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 14\n\nX4 is free\nX48 is free\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: verb(X48, X4, s(s, book, X63)), SCOPE: 6, CLAUSE: 15\n\nX4 is free\nX48 is free\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 9\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 10 | ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 11\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(comb(a, -(book, p), X28), verb(X112, X4, X28))\n\nX4 is free\nX28 is free\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(comb(a, -(book, p), X28), verb(X112, X4, X28)), SCOPE: 7, CLAUSE: 4 | ','(comb(a, -(book, p), X28), verb(X112, X4, X28)), SCOPE: 7, CLAUSE: 5\n\nX4 is free\nX28 is free\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(comb(a, -(book, p), X28), verb(X112, X4, X28)), SCOPE: 7, CLAUSE: 5\n\nX4 is free\nX28 is free\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 10\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(','(noun(X38, X27, X25), comb(a, X25, X28)), verb(X27, X4, X28)), SCOPE: 4, CLAUSE: 11\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(comb(a, -(box, s), X28), verb(X127, X4, X28))\n\nX4 is free\nX28 is free\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(comb(a, -(box, s), X28), verb(X127, X4, X28)), SCOPE: 8, CLAUSE: 4 | ','(comb(a, -(box, s), X28), verb(X127, X4, X28)), SCOPE: 8, CLAUSE: 5\n\nX4 is free\nX28 is free\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(comb(a, -(box, s), X28), verb(X127, X4, X28)), SCOPE: 8, CLAUSE: 4\n\nX4 is free\nX28 is free\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(comb(a, -(box, s), X28), verb(X127, X4, X28)), SCOPE: 8, CLAUSE: 5\n\nX4 is free\nX28 is free\nX127 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: verb(X127, X4, s(s, box, X142))\n\nX4 is free\nX127 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 12 | verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 13 | verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 14 | verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 15\n\nX4 is free\nX127 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 12\n\nX4 is free\nX127 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 13 | verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 14 | verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 15\n\nX4 is free\nX127 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 14 | verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 15\n\nX4 is free\nX127 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 14\n\nX4 is free\nX127 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: verb(X127, X4, s(s, box, X142)), SCOPE: 9, CLAUSE: 15\n\nX4 is free\nX127 is free\nX142 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(comb(a, -(box, p), X28), verb(X187, X4, X28))\n\nX4 is free\nX28 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(comb(a, -(box, p), X28), verb(X187, X4, X28)), SCOPE: 10, CLAUSE: 4 | ','(comb(a, -(box, p), X28), verb(X187, X4, X28)), SCOPE: 10, CLAUSE: 5\n\nX4 is free\nX28 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(comb(a, -(box, p), X28), verb(X187, X4, X28)), SCOPE: 10, CLAUSE: 5\n\nX4 is free\nX28 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28))\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 8 | ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 9 | ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 10 | ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 11\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 8\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 9 | ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 10 | ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 11\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(comb(the, -(book, s), X28), verb(X208, X4, X28))\n\nX4 is free\nX28 is free\nX208 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(comb(the, -(book, s), X28), verb(X208, X4, X28)), SCOPE: 12, CLAUSE: 4 | ','(comb(the, -(book, s), X28), verb(X208, X4, X28)), SCOPE: 12, CLAUSE: 5\n\nX4 is free\nX28 is free\nX208 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(comb(the, -(book, s), X28), verb(X208, X4, X28)), SCOPE: 12, CLAUSE: 5\n\nX4 is free\nX28 is free\nX208 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: verb(X208, X4, s(s, book, X222))\n\nX4 is free\nX208 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 12 | verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 13 | verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 14 | verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 15\n\nX4 is free\nX208 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 12\n\nX4 is free\nX208 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 13 | verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 14 | verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 15\n\nX4 is free\nX208 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 14 | verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 15\n\nX4 is free\nX208 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 14\n\nX4 is free\nX208 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: verb(X208, X4, s(s, book, X222)), SCOPE: 13, CLAUSE: 15\n\nX4 is free\nX208 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 9\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 10 | ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 11\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: ','(comb(the, -(book, p), X28), verb(X268, X4, X28))\n\nX4 is free\nX28 is free\nX268 is free", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: ','(comb(the, -(book, p), X28), verb(X268, X4, X28)), SCOPE: 14, CLAUSE: 4 | ','(comb(the, -(book, p), X28), verb(X268, X4, X28)), SCOPE: 14, CLAUSE: 5\n\nX4 is free\nX28 is free\nX268 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: ','(comb(the, -(book, p), X28), verb(X268, X4, X28)), SCOPE: 14, CLAUSE: 5\n\nX4 is free\nX28 is free\nX268 is free", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: verb(X268, X4, s(p, book, X282))\n\nX4 is free\nX268 is free\nX282 is free", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 12 | verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 13 | verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 14 | verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 15\n\nX4 is free\nX268 is free\nX282 is free", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 13 | verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 14 | verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 15\n\nX4 is free\nX268 is free\nX282 is free", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 13\n\nX4 is free\nX268 is free\nX282 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 14 | verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 15\n\nX4 is free\nX268 is free\nX282 is free", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: verb(X268, X4, s(p, book, X282)), SCOPE: 15, CLAUSE: 15\n\nX4 is free\nX268 is free\nX282 is free", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 10\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: ','(','(noun(X198, X27, X25), comb(the, X25, X28)), verb(X27, X4, X28)), SCOPE: 11, CLAUSE: 11\n\nX4 is free\nX27 is free\nX28 is free\nX25 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: ','(comb(the, -(box, s), X28), verb(X322, X4, X28))\n\nX4 is free\nX28 is free\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: ','(comb(the, -(box, s), X28), verb(X322, X4, X28)), SCOPE: 16, CLAUSE: 4 | ','(comb(the, -(box, s), X28), verb(X322, X4, X28)), SCOPE: 16, CLAUSE: 5\n\nX4 is free\nX28 is free\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: ','(comb(the, -(box, s), X28), verb(X322, X4, X28)), SCOPE: 16, CLAUSE: 5\n\nX4 is free\nX28 is free\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: verb(X322, X4, s(s, box, X336))\n\nX4 is free\nX322 is free\nX336 is free", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 12 | verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 13 | verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 14 | verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 15\n\nX4 is free\nX322 is free\nX336 is free", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 12\n\nX4 is free\nX322 is free\nX336 is free", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 13 | verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 14 | verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 15\n\nX4 is free\nX322 is free\nX336 is free", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 14 | verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 15\n\nX4 is free\nX322 is free\nX336 is free", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 14\n\nX4 is free\nX322 is free\nX336 is free", fontsize=16, style=filled, fillcolor=lightyellow];
308 [label="308: verb(X322, X4, s(s, box, X336)), SCOPE: 17, CLAUSE: 15\n\nX4 is free\nX322 is free\nX336 is free", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="317: ','(comb(the, -(box, p), X28), verb(X378, X4, X28))\n\nX4 is free\nX28 is free\nX378 is free", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: ','(comb(the, -(box, p), X28), verb(X378, X4, X28)), SCOPE: 18, CLAUSE: 4 | ','(comb(the, -(box, p), X28), verb(X378, X4, X28)), SCOPE: 18, CLAUSE: 5\n\nX4 is free\nX28 is free\nX378 is free", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: ','(comb(the, -(box, p), X28), verb(X378, X4, X28)), SCOPE: 18, CLAUSE: 5\n\nX4 is free\nX28 is free\nX378 is free", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: verb(X378, X4, s(p, box, X392))\n\nX4 is free\nX378 is free\nX392 is free", fontsize=16, style=filled, fillcolor=lightyellow];
325 [label="325: verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 12 | verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 13 | verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 14 | verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 15\n\nX4 is free\nX378 is free\nX392 is free", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 13 | verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 14 | verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 15\n\nX4 is free\nX378 is free\nX392 is free", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 13\n\nX4 is free\nX378 is free\nX392 is free", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 14 | verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 15\n\nX4 is free\nX378 is free\nX392 is free", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: verb(X378, X4, s(p, box, X392)), SCOPE: 19, CLAUSE: 15\n\nX4 is free\nX378 is free\nX392 is free", fontsize=16, style=filled, fillcolor=lightyellow];
337 [label="337: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 339 [arrowhead = none ];
339 -> 4;

340 [label="ONLY EVAL with clause\ngoal :- ','(np(X1, X2, X3), verb(X2, X4, X3)).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 340 [arrowhead = none ];
340 -> 8;

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

342 [label="ONLY EVAL with clause\nnp(X20, X21, X22) :- ','(det(X20, X23, X24), ','(noun(X23, X21, X25), comb(X24, X25, X22))).\nand substitutionX1 -> X26,\nX20 -> X26,\nX2 -> X27,\nX21 -> X27,\nX3 -> X28,\nX22 -> X28", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 342 [arrowhead = none ];
342 -> 15;

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

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

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

346 [label="ONLY EVAL with clause\ndet(.(a, X37), X37, a).\nand substitutionX37 -> X38,\nX26 -> .(a, X38),\nX23 -> X38,\nX24 -> a", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 346 [arrowhead = none ];
346 -> 29;

347 [label="ONLY EVAL with clause\ndet(.(the, X197), X197, the).\nand substitutionX197 -> X198,\nX26 -> .(the, X198),\nX23 -> X198,\nX24 -> the", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 347 [arrowhead = none ];
347 -> 179;

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

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

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

351 [label="ONLY EVAL with clause\nnoun(.(book, X47), X47, -(book, s)).\nand substitutionX47 -> X48,\nX38 -> .(book, X48),\nX27 -> X48,\nX25 -> -(book, s)", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 351 [arrowhead = none ];
351 -> 37;

352 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 352 [arrowhead = none ];
352 -> 73;

353 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 353 [arrowhead = none ];
353 -> 75;

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

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

356 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
38 -> 356 [arrowhead = none ];
356 -> 43;

357 [label="ONLY EVAL with clause\ncomb(a, -(X61, s), s(s, X61, X62)).\nand substitutionX61 -> book,\nX62 -> X63,\nX28 -> s(s, book, X63)", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 357 [arrowhead = none ];
357 -> 45;

358 [label="BACKTRACK\nfor clause: comb(the, -(N, P), s(P, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 358 [arrowhead = none ];
358 -> 71;

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

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

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

362 [label="ONLY EVAL with clause\nverb(.(falls, X76), X76, s(s, X77, fall)).\nand substitutionX76 -> X78,\nX48 -> .(falls, X78),\nX4 -> X78,\nX77 -> book,\nX63 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 362 [arrowhead = none ];
362 -> 49;

363 [label="BACKTRACK\nfor clause: verb(.(fall, So), So, s(p, N, fall))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 363 [arrowhead = none ];
363 -> 55;

364 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 364 [arrowhead = none ];
364 -> 50;

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

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

367 [label="ONLY EVAL with clause\nverb(.(flies, X94), X94, s(s, X95, fly)).\nand substitutionX94 -> X96,\nX48 -> .(flies, X96),\nX4 -> X96,\nX95 -> book,\nX63 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 367 [arrowhead = none ];
367 -> 67;

368 [label="BACKTRACK\nfor clause: verb(.(fly, So), So, s(p, N, fly))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 368 [arrowhead = none ];
368 -> 69;

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

370 [label="ONLY EVAL with clause\nnoun(.(books, X111), X111, -(book, p)).\nand substitutionX111 -> X112,\nX38 -> .(books, X112),\nX27 -> X112,\nX25 -> -(book, p)", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 370 [arrowhead = none ];
370 -> 80;

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

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

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

374 [label="BACKTRACK\nfor clause: comb(a, -(N, s), s(s, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 374 [arrowhead = none ];
374 -> 84;

375 [label="BACKTRACK\nfor clause: comb(the, -(N, P), s(P, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 375 [arrowhead = none ];
375 -> 88;

376 [label="ONLY EVAL with clause\nnoun(.(box, X126), X126, -(box, s)).\nand substitutionX126 -> X127,\nX38 -> .(box, X127),\nX27 -> X127,\nX25 -> -(box, s)", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 376 [arrowhead = none ];
376 -> 119;

377 [label="ONLY EVAL with clause\nnoun(.(boxes, X186), X186, -(box, p)).\nand substitutionX186 -> X187,\nX38 -> .(boxes, X187),\nX27 -> X187,\nX25 -> -(box, p)", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 377 [arrowhead = none ];
377 -> 166;

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

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

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

381 [label="ONLY EVAL with clause\ncomb(a, -(X140, s), s(s, X140, X141)).\nand substitutionX140 -> box,\nX141 -> X142,\nX28 -> s(s, box, X142)", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 381 [arrowhead = none ];
381 -> 130;

382 [label="BACKTRACK\nfor clause: comb(the, -(N, P), s(P, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 382 [arrowhead = none ];
382 -> 162;

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

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

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

386 [label="ONLY EVAL with clause\nverb(.(falls, X155), X155, s(s, X156, fall)).\nand substitutionX155 -> X157,\nX127 -> .(falls, X157),\nX4 -> X157,\nX156 -> box,\nX142 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 386 [arrowhead = none ];
386 -> 148;

387 [label="BACKTRACK\nfor clause: verb(.(fall, So), So, s(p, N, fall))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 387 [arrowhead = none ];
387 -> 152;

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

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

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

391 [label="ONLY EVAL with clause\nverb(.(flies, X173), X173, s(s, X174, fly)).\nand substitutionX173 -> X175,\nX127 -> .(flies, X175),\nX4 -> X175,\nX174 -> box,\nX142 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
153 -> 391 [arrowhead = none ];
391 -> 159;

392 [label="BACKTRACK\nfor clause: verb(.(fly, So), So, s(p, N, fly))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 392 [arrowhead = none ];
392 -> 161;

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

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

395 [label="BACKTRACK\nfor clause: comb(a, -(N, s), s(s, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
168 -> 395 [arrowhead = none ];
395 -> 169;

396 [label="BACKTRACK\nfor clause: comb(the, -(N, P), s(P, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
169 -> 396 [arrowhead = none ];
396 -> 170;

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

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

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

400 [label="ONLY EVAL with clause\nnoun(.(book, X207), X207, -(book, s)).\nand substitutionX207 -> X208,\nX198 -> .(book, X208),\nX27 -> X208,\nX25 -> -(book, s)", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 400 [arrowhead = none ];
400 -> 191;

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

402 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
188 -> 402 [arrowhead = none ];
402 -> 238;

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

404 [label="BACKTRACK\nfor clause: comb(a, -(N, s), s(s, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
193 -> 404 [arrowhead = none ];
404 -> 195;

405 [label="ONLY EVAL with clause\ncomb(the, -(X219, X220), s(X220, X219, X221)).\nand substitutionX219 -> book,\nX220 -> s,\nX221 -> X222,\nX28 -> s(s, book, X222)", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 405 [arrowhead = none ];
405 -> 197;

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

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

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

409 [label="ONLY EVAL with clause\nverb(.(falls, X235), X235, s(s, X236, fall)).\nand substitutionX235 -> X237,\nX208 -> .(falls, X237),\nX4 -> X237,\nX236 -> book,\nX222 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
202 -> 409 [arrowhead = none ];
409 -> 208;

410 [label="BACKTRACK\nfor clause: verb(.(fall, So), So, s(p, N, fall))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
203 -> 410 [arrowhead = none ];
410 -> 213;

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

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

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

414 [label="ONLY EVAL with clause\nverb(.(flies, X253), X253, s(s, X254, fly)).\nand substitutionX253 -> X255,\nX208 -> .(flies, X255),\nX4 -> X255,\nX254 -> book,\nX222 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
216 -> 414 [arrowhead = none ];
414 -> 220;

415 [label="BACKTRACK\nfor clause: verb(.(fly, So), So, s(p, N, fly))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 415 [arrowhead = none ];
415 -> 223;

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

417 [label="ONLY EVAL with clause\nnoun(.(books, X267), X267, -(book, p)).\nand substitutionX267 -> X268,\nX198 -> .(books, X268),\nX27 -> X268,\nX25 -> -(book, p)", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 417 [arrowhead = none ];
417 -> 241;

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

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

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

421 [label="BACKTRACK\nfor clause: comb(a, -(N, s), s(s, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
242 -> 421 [arrowhead = none ];
421 -> 243;

422 [label="ONLY EVAL with clause\ncomb(the, -(X279, X280), s(X280, X279, X281)).\nand substitutionX279 -> book,\nX280 -> p,\nX281 -> X282,\nX28 -> s(p, book, X282)", fontsize=14, style = filled, fillcolor = lightblue];
243 -> 422 [arrowhead = none ];
422 -> 247;

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

424 [label="BACKTRACK\nfor clause: verb(.(falls, So), So, s(s, N, fall))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
248 -> 424 [arrowhead = none ];
424 -> 249;

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

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

427 [label="ONLY EVAL with clause\nverb(.(fall, X298), X298, s(p, X299, fall)).\nand substitutionX298 -> X300,\nX268 -> .(fall, X300),\nX4 -> X300,\nX299 -> book,\nX282 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
258 -> 427 [arrowhead = none ];
427 -> 262;

428 [label="BACKTRACK\nfor clause: verb(.(flies, So), So, s(s, N, fly))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
259 -> 428 [arrowhead = none ];
428 -> 266;

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

430 [label="ONLY EVAL with clause\nverb(.(fly, X310), X310, s(p, X311, fly)).\nand substitutionX310 -> X312,\nX268 -> .(fly, X312),\nX4 -> X312,\nX311 -> book,\nX282 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
266 -> 430 [arrowhead = none ];
430 -> 269;

431 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
269 -> 431 [arrowhead = none ];
431 -> 270;

432 [label="ONLY EVAL with clause\nnoun(.(box, X321), X321, -(box, s)).\nand substitutionX321 -> X322,\nX198 -> .(box, X322),\nX27 -> X322,\nX25 -> -(box, s)", fontsize=14, style = filled, fillcolor = lightblue];
271 -> 432 [arrowhead = none ];
432 -> 276;

433 [label="ONLY EVAL with clause\nnoun(.(boxes, X377), X377, -(box, p)).\nand substitutionX377 -> X378,\nX198 -> .(boxes, X378),\nX27 -> X378,\nX25 -> -(box, p)", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 433 [arrowhead = none ];
433 -> 317;

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

435 [label="BACKTRACK\nfor clause: comb(a, -(N, s), s(s, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
277 -> 435 [arrowhead = none ];
435 -> 278;

436 [label="ONLY EVAL with clause\ncomb(the, -(X333, X334), s(X334, X333, X335)).\nand substitutionX333 -> box,\nX334 -> s,\nX335 -> X336,\nX28 -> s(s, box, X336)", fontsize=14, style = filled, fillcolor = lightblue];
278 -> 436 [arrowhead = none ];
436 -> 283;

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

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

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

440 [label="ONLY EVAL with clause\nverb(.(falls, X349), X349, s(s, X350, fall)).\nand substitutionX349 -> X351,\nX322 -> .(falls, X351),\nX4 -> X351,\nX350 -> box,\nX336 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
291 -> 440 [arrowhead = none ];
440 -> 299;

441 [label="BACKTRACK\nfor clause: verb(.(fall, So), So, s(p, N, fall))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
292 -> 441 [arrowhead = none ];
441 -> 301;

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

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

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

445 [label="ONLY EVAL with clause\nverb(.(flies, X367), X367, s(s, X368, fly)).\nand substitutionX367 -> X369,\nX322 -> .(flies, X369),\nX4 -> X369,\nX368 -> box,\nX336 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
307 -> 445 [arrowhead = none ];
445 -> 314;

446 [label="BACKTRACK\nfor clause: verb(.(fly, So), So, s(p, N, fly))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
308 -> 446 [arrowhead = none ];
446 -> 316;

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

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

449 [label="BACKTRACK\nfor clause: comb(a, -(N, s), s(s, N, V))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
318 -> 449 [arrowhead = none ];
449 -> 319;

450 [label="ONLY EVAL with clause\ncomb(the, -(X389, X390), s(X390, X389, X391)).\nand substitutionX389 -> box,\nX390 -> p,\nX391 -> X392,\nX28 -> s(p, box, X392)", fontsize=14, style = filled, fillcolor = lightblue];
319 -> 450 [arrowhead = none ];
450 -> 324;

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

452 [label="BACKTRACK\nfor clause: verb(.(falls, So), So, s(s, N, fall))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
325 -> 452 [arrowhead = none ];
452 -> 326;

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

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

455 [label="ONLY EVAL with clause\nverb(.(fall, X408), X408, s(p, X409, fall)).\nand substitutionX408 -> X410,\nX378 -> .(fall, X410),\nX4 -> X410,\nX409 -> box,\nX392 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
330 -> 455 [arrowhead = none ];
455 -> 334;

456 [label="BACKTRACK\nfor clause: verb(.(flies, So), So, s(s, N, fly))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
331 -> 456 [arrowhead = none ];
456 -> 336;

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

458 [label="ONLY EVAL with clause\nverb(.(fly, X420), X420, s(p, X421, fly)).\nand substitutionX420 -> X422,\nX378 -> .(fly, X422),\nX4 -> X422,\nX421 -> box,\nX392 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
336 -> 458 [arrowhead = none ];
458 -> 337;

459 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
337 -> 459 [arrowhead = none ];
459 -> 338;

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f2_in → f2_out1

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:

f2_in > f2_out1

and weight map:

f2_in=1
f2_out1=1

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f2_in → f2_out1

(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) YES