Left Termination proof of /tmp/tmpcYFqr6/grammar2.pl

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇒, 383 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 0 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 0 ms)

↳6 PiDP

↳7 PisEmptyProof (⇔, 0 ms)

↳8 YES

(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: parse(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: parse(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: parse(T1, T2), SCOPE: 1, CLAUSE: 1 | parse(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(np(T5, X5, T7), verb(X5, [], T7)) | parse(T5, T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(np(T5, X5, T7), verb(X5, [], T7)), SCOPE: 2, CLAUSE: 3 | ?_2 | parse(T5, T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(np(T5, X5, T7), verb(X5, [], T7)), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ?_2 | parse(T5, T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(','(det(T18, X31, X32), ','(noun(X31, X34, X33), comb(X32, X33, T20))), verb(X34, [], T20))\n\nT18 is ground\nX34 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(','(det(T18, X31, X32), ','(noun(X31, X34, X33), comb(X32, X33, T20))), verb(X34, [], T20)), SCOPE: 3, CLAUSE: 6 | ','(','(det(T18, X31, X32), ','(noun(X31, X34, X33), comb(X32, X33, T20))), verb(X34, [], T20)), SCOPE: 3, CLAUSE: 7\n\nT18 is ground\nX34 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(','(det(T18, X31, X32), ','(noun(X31, X34, X33), comb(X32, X33, T20))), verb(X34, [], T20)), SCOPE: 3, CLAUSE: 6\n\nT18 is ground\nX34 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(','(det(T18, X31, X32), ','(noun(X31, X34, X33), comb(X32, X33, T20))), verb(X34, [], T20)), SCOPE: 3, CLAUSE: 7\n\nT18 is ground\nX34 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20))\n\nT25 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 8 | ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 9 | ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 10 | ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 11\n\nT25 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 8\n\nT25 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 9 | ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 10 | ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 11\n\nT25 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(comb(a, -(book, s), T20), verb(T30, [], T20))\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(comb(a, -(book, s), T20), verb(T30, [], T20)), SCOPE: 5, CLAUSE: 4 | ','(comb(a, -(book, s), T20), verb(T30, [], T20)), SCOPE: 5, CLAUSE: 5\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(comb(a, -(book, s), T20), verb(T30, [], T20)), SCOPE: 5, CLAUSE: 4\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(comb(a, -(book, s), T20), verb(T30, [], T20)), SCOPE: 5, CLAUSE: 5\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: verb(T30, [], s(s, book, T36))\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 12 | verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 13 | verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 14 | verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 15\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 12\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 13 | verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 14 | verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 15\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 14 | verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 15\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 14\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: verb(T30, [], s(s, book, T36)), SCOPE: 6, CLAUSE: 15\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 9\n\nT25 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 10 | ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 11\n\nT25 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(comb(a, -(book, p), T20), verb(T53, [], T20))\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(comb(a, -(book, p), T20), verb(T53, [], T20)), SCOPE: 7, CLAUSE: 4 | ','(comb(a, -(book, p), T20), verb(T53, [], T20)), SCOPE: 7, CLAUSE: 5\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(comb(a, -(book, p), T20), verb(T53, [], T20)), SCOPE: 7, CLAUSE: 5\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 10\n\nT25 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(','(noun(T25, X34, X33), comb(a, X33, T20)), verb(X34, [], T20)), SCOPE: 4, CLAUSE: 11\n\nT25 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(comb(a, -(box, s), T20), verb(T58, [], T20))\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(comb(a, -(box, s), T20), verb(T58, [], T20)), SCOPE: 8, CLAUSE: 4 | ','(comb(a, -(box, s), T20), verb(T58, [], T20)), SCOPE: 8, CLAUSE: 5\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(comb(a, -(box, s), T20), verb(T58, [], T20)), SCOPE: 8, CLAUSE: 4\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(comb(a, -(box, s), T20), verb(T58, [], T20)), SCOPE: 8, CLAUSE: 5\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: verb(T58, [], s(s, box, T64))\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 12 | verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 13 | verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 14 | verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 15\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 12\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 13 | verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 14 | verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 15\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 14 | verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 15\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 14\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: verb(T58, [], s(s, box, T64)), SCOPE: 9, CLAUSE: 15\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(comb(a, -(box, p), T20), verb(T79, [], T20))\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(comb(a, -(box, p), T20), verb(T79, [], T20)), SCOPE: 10, CLAUSE: 4 | ','(comb(a, -(box, p), T20), verb(T79, [], T20)), SCOPE: 10, CLAUSE: 5\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(comb(a, -(box, p), T20), verb(T79, [], T20)), SCOPE: 10, CLAUSE: 5\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20))\n\nT82 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 8 | ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 9 | ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 10 | ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 11\n\nT82 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 8\n\nT82 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 9 | ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 10 | ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 11\n\nT82 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(comb(the, -(book, s), T20), verb(T87, [], T20))\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(comb(the, -(book, s), T20), verb(T87, [], T20)), SCOPE: 12, CLAUSE: 4 | ','(comb(the, -(book, s), T20), verb(T87, [], T20)), SCOPE: 12, CLAUSE: 5\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(comb(the, -(book, s), T20), verb(T87, [], T20)), SCOPE: 12, CLAUSE: 5\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: verb(T87, [], s(s, book, T91))\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 12 | verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 13 | verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 14 | verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 15\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 12\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 13 | verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 14 | verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 15\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 14 | verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 15\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 14\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: verb(T87, [], s(s, book, T91)), SCOPE: 13, CLAUSE: 15\n\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 9\n\nT82 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 10 | ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 11\n\nT82 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(comb(the, -(book, p), T20), verb(T108, [], T20))\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(comb(the, -(book, p), T20), verb(T108, [], T20)), SCOPE: 14, CLAUSE: 4 | ','(comb(the, -(book, p), T20), verb(T108, [], T20)), SCOPE: 14, CLAUSE: 5\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(comb(the, -(book, p), T20), verb(T108, [], T20)), SCOPE: 14, CLAUSE: 5\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: verb(T108, [], s(p, book, T112))\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 12 | verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 13 | verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 14 | verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 15\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 13 | verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 14 | verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 15\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 13\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 14 | verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 15\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: verb(T108, [], s(p, book, T112)), SCOPE: 15, CLAUSE: 15\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 10\n\nT82 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(','(noun(T82, X34, X33), comb(the, X33, T20)), verb(X34, [], T20)), SCOPE: 11, CLAUSE: 11\n\nT82 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(comb(the, -(box, s), T20), verb(T127, [], T20))\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(comb(the, -(box, s), T20), verb(T127, [], T20)), SCOPE: 16, CLAUSE: 4 | ','(comb(the, -(box, s), T20), verb(T127, [], T20)), SCOPE: 16, CLAUSE: 5\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(comb(the, -(box, s), T20), verb(T127, [], T20)), SCOPE: 16, CLAUSE: 5\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: verb(T127, [], s(s, box, T131))\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 12 | verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 13 | verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 14 | verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 15\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 12\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 13 | verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 14 | verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 15\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 14 | verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 15\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 14\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: verb(T127, [], s(s, box, T131)), SCOPE: 17, CLAUSE: 15\n\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(comb(the, -(box, p), T20), verb(T146, [], T20))\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(comb(the, -(box, p), T20), verb(T146, [], T20)), SCOPE: 18, CLAUSE: 4 | ','(comb(the, -(box, p), T20), verb(T146, [], T20)), SCOPE: 18, CLAUSE: 5\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(comb(the, -(box, p), T20), verb(T146, [], T20)), SCOPE: 18, CLAUSE: 5\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: verb(T146, [], s(p, box, T150))\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 12 | verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 13 | verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 14 | verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 15\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 13 | verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 14 | verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 15\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 13\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 14 | verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 15\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: verb(T146, [], s(p, box, T150)), SCOPE: 19, CLAUSE: 15\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: parse(T5, T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(np(T166, X303, T168), ','(verb(X303, X304, T168), =(X304, [])))\n\nT166 is ground\nX303 is free\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(np(T166, X303, T168), ','(verb(X303, X304, T168), =(X304, []))), SCOPE: 20, CLAUSE: 3\n\nT166 is ground\nX303 is free\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(','(det(T174, X319, X320), ','(noun(X319, X322, X321), comb(X320, X321, T176))), ','(verb(X322, X304, T176), =(X304, [])))\n\nT174 is ground\nX304 is free\nX322 is free\nX319 is free\nX320 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(','(det(T174, X319, X320), ','(noun(X319, X322, X321), comb(X320, X321, T176))), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 21, CLAUSE: 6 | ','(','(det(T174, X319, X320), ','(noun(X319, X322, X321), comb(X320, X321, T176))), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 21, CLAUSE: 7\n\nT174 is ground\nX304 is free\nX322 is free\nX319 is free\nX320 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ','(','(det(T174, X319, X320), ','(noun(X319, X322, X321), comb(X320, X321, T176))), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 21, CLAUSE: 6\n\nT174 is ground\nX304 is free\nX322 is free\nX319 is free\nX320 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(','(det(T174, X319, X320), ','(noun(X319, X322, X321), comb(X320, X321, T176))), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 21, CLAUSE: 7\n\nT174 is ground\nX304 is free\nX322 is free\nX319 is free\nX320 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, [])))\n\nT181 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 8 | ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 9 | ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 10 | ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 11\n\nT181 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 8\n\nT181 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 9 | ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 10 | ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 11\n\nT181 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(comb(a, -(book, s), T176), ','(verb(T186, X304, T176), =(X304, [])))\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(comb(a, -(book, s), T176), ','(verb(T186, X304, T176), =(X304, []))), SCOPE: 23, CLAUSE: 4 | ','(comb(a, -(book, s), T176), ','(verb(T186, X304, T176), =(X304, []))), SCOPE: 23, CLAUSE: 5\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(comb(a, -(book, s), T176), ','(verb(T186, X304, T176), =(X304, []))), SCOPE: 23, CLAUSE: 4\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(comb(a, -(book, s), T176), ','(verb(T186, X304, T176), =(X304, []))), SCOPE: 23, CLAUSE: 5\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(verb(T186, X304, s(s, book, T192)), =(X304, []))\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 12 | ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 13 | ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 14 | ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 15\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 12\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 13 | ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 14 | ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 15\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: =(T197, [])\n\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 14 | ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 15\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 14\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ','(verb(T186, X304, s(s, book, T192)), =(X304, [])), SCOPE: 24, CLAUSE: 15\n\nT186 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: =(T203, [])\n\nT203 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 9\n\nT181 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 10 | ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 11\n\nT181 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(comb(a, -(book, p), T176), ','(verb(T209, X304, T176), =(X304, [])))\n\nT209 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(comb(a, -(book, p), T176), ','(verb(T209, X304, T176), =(X304, []))), SCOPE: 25, CLAUSE: 4 | ','(comb(a, -(book, p), T176), ','(verb(T209, X304, T176), =(X304, []))), SCOPE: 25, CLAUSE: 5\n\nT209 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(comb(a, -(book, p), T176), ','(verb(T209, X304, T176), =(X304, []))), SCOPE: 25, CLAUSE: 5\n\nT209 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 10\n\nT181 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(','(noun(T181, X322, X321), comb(a, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 22, CLAUSE: 11\n\nT181 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(comb(a, -(box, s), T176), ','(verb(T214, X304, T176), =(X304, [])))\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(comb(a, -(box, s), T176), ','(verb(T214, X304, T176), =(X304, []))), SCOPE: 26, CLAUSE: 4 | ','(comb(a, -(box, s), T176), ','(verb(T214, X304, T176), =(X304, []))), SCOPE: 26, CLAUSE: 5\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(comb(a, -(box, s), T176), ','(verb(T214, X304, T176), =(X304, []))), SCOPE: 26, CLAUSE: 4\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ','(comb(a, -(box, s), T176), ','(verb(T214, X304, T176), =(X304, []))), SCOPE: 26, CLAUSE: 5\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: ','(verb(T214, X304, s(s, box, T220)), =(X304, []))\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 12 | ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 13 | ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 14 | ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 15\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 12\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 13 | ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 14 | ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 15\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: =(T225, [])\n\nT225 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 14 | ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 15\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 14\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(verb(T214, X304, s(s, box, T220)), =(X304, [])), SCOPE: 27, CLAUSE: 15\n\nT214 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: =(T231, [])\n\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ','(comb(a, -(box, p), T176), ','(verb(T235, X304, T176), =(X304, [])))\n\nT235 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: ','(comb(a, -(box, p), T176), ','(verb(T235, X304, T176), =(X304, []))), SCOPE: 28, CLAUSE: 4 | ','(comb(a, -(box, p), T176), ','(verb(T235, X304, T176), =(X304, []))), SCOPE: 28, CLAUSE: 5\n\nT235 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: ','(comb(a, -(box, p), T176), ','(verb(T235, X304, T176), =(X304, []))), SCOPE: 28, CLAUSE: 5\n\nT235 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, [])))\n\nT238 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 8 | ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 9 | ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 10 | ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 11\n\nT238 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 8\n\nT238 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 9 | ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 10 | ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 11\n\nT238 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(comb(the, -(book, s), T176), ','(verb(T243, X304, T176), =(X304, [])))\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: ','(comb(the, -(book, s), T176), ','(verb(T243, X304, T176), =(X304, []))), SCOPE: 30, CLAUSE: 4 | ','(comb(the, -(book, s), T176), ','(verb(T243, X304, T176), =(X304, []))), SCOPE: 30, CLAUSE: 5\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: ','(comb(the, -(book, s), T176), ','(verb(T243, X304, T176), =(X304, []))), SCOPE: 30, CLAUSE: 5\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ','(verb(T243, X304, s(s, book, T247)), =(X304, []))\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 12 | ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 13 | ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 14 | ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 15\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 12\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 13 | ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 14 | ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 15\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: =(T252, [])\n\nT252 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 14 | ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 15\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 14\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ','(verb(T243, X304, s(s, book, T247)), =(X304, [])), SCOPE: 31, CLAUSE: 15\n\nT243 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: =(T258, [])\n\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 9\n\nT238 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 10 | ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 11\n\nT238 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: ','(comb(the, -(book, p), T176), ','(verb(T264, X304, T176), =(X304, [])))\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(comb(the, -(book, p), T176), ','(verb(T264, X304, T176), =(X304, []))), SCOPE: 32, CLAUSE: 4 | ','(comb(the, -(book, p), T176), ','(verb(T264, X304, T176), =(X304, []))), SCOPE: 32, CLAUSE: 5\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: ','(comb(the, -(book, p), T176), ','(verb(T264, X304, T176), =(X304, []))), SCOPE: 32, CLAUSE: 5\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: ','(verb(T264, X304, s(p, book, T268)), =(X304, []))\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 12 | ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 13 | ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 14 | ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 15\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 13 | ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 14 | ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 15\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 13\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 14 | ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 15\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: =(T274, [])\n\nT274 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: ','(verb(T264, X304, s(p, book, T268)), =(X304, [])), SCOPE: 33, CLAUSE: 15\n\nT264 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: =(T278, [])\n\nT278 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 10\n\nT238 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: ','(','(noun(T238, X322, X321), comb(the, X321, T176)), ','(verb(X322, X304, T176), =(X304, []))), SCOPE: 29, CLAUSE: 11\n\nT238 is ground\nX304 is free\nX322 is free\nX321 is free", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: ','(comb(the, -(box, s), T176), ','(verb(T283, X304, T176), =(X304, [])))\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: ','(comb(the, -(box, s), T176), ','(verb(T283, X304, T176), =(X304, []))), SCOPE: 34, CLAUSE: 4 | ','(comb(the, -(box, s), T176), ','(verb(T283, X304, T176), =(X304, []))), SCOPE: 34, CLAUSE: 5\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: ','(comb(the, -(box, s), T176), ','(verb(T283, X304, T176), =(X304, []))), SCOPE: 34, CLAUSE: 5\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: ','(verb(T283, X304, s(s, box, T287)), =(X304, []))\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 12 | ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 13 | ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 14 | ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 15\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 12\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 13 | ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 14 | ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 15\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: =(T292, [])\n\nT292 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
293 [label="293: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 14 | ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 15\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 14\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: ','(verb(T283, X304, s(s, box, T287)), =(X304, [])), SCOPE: 35, CLAUSE: 15\n\nT283 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: =(T298, [])\n\nT298 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: ','(comb(the, -(box, p), T176), ','(verb(T302, X304, T176), =(X304, [])))\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: ','(comb(the, -(box, p), T176), ','(verb(T302, X304, T176), =(X304, []))), SCOPE: 36, CLAUSE: 4 | ','(comb(the, -(box, p), T176), ','(verb(T302, X304, T176), =(X304, []))), SCOPE: 36, CLAUSE: 5\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
308 [label="308: ','(comb(the, -(box, p), T176), ','(verb(T302, X304, T176), =(X304, []))), SCOPE: 36, CLAUSE: 5\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
309 [label="309: ','(verb(T302, X304, s(p, box, T306)), =(X304, []))\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
310 [label="310: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
311 [label="311: ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 12 | ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 13 | ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 14 | ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 15\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
312 [label="312: ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 13 | ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 14 | ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 15\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
313 [label="313: ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 13\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 14 | ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 15\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: =(T312, [])\n\nT312 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="317: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: ','(verb(T302, X304, s(p, box, T306)), =(X304, [])), SCOPE: 37, CLAUSE: 15\n\nT302 is ground\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: =(T316, [])\n\nT316 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
325 [label="325: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 326 [arrowhead = none ];
326 -> 2;

327 [label="ONLY EVAL with clause\nparse(X3, X4) :- ','(np(X3, X5, X4), verb(X5, [], X4)).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T7,\nX4 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 327 [arrowhead = none ];
327 -> 3;

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

329 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 329 [arrowhead = none ];
329 -> 5;

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

331 [label="ONLY EVAL with clause\nnp(X28, X29, X30) :- ','(det(X28, X31, X32), ','(noun(X31, X29, X33), comb(X32, X33, X30))).\nand substitutionT5 -> T18,\nX28 -> T18,\nX5 -> X34,\nX29 -> X34,\nT7 -> T20,\nX30 -> T20,\nT19 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 331 [arrowhead = none ];
331 -> 7;

332 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 332 [arrowhead = none ];
332 -> 153;

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

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

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

336 [label="EVAL with clause\ndet(.(a, X39), X39, a).\nand substitutionX39 -> T25,\nT18 -> .(a, T25),\nX31 -> T25,\nX32 -> a", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 336 [arrowhead = none ];
336 -> 11;

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

338 [label="EVAL with clause\ndet(.(the, X144), X144, the).\nand substitutionX144 -> T82,\nT18 -> .(the, T82),\nX31 -> T82,\nX32 -> the", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 338 [arrowhead = none ];
338 -> 72;

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

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

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

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

343 [label="EVAL with clause\nnoun(.(book, X44), X44, -(book, s)).\nand substitutionX44 -> T30,\nT25 -> .(book, T30),\nX34 -> T30,\nX33 -> -(book, s)", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 343 [arrowhead = none ];
343 -> 16;

344 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 344 [arrowhead = none ];
344 -> 17;

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

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

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

348 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 348 [arrowhead = none ];
348 -> 19;

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

350 [label="EVAL with clause\ncomb(a, -(X53, s), s(s, X53, X54)).\nand substitutionX53 -> book,\nX54 -> T36,\nT20 -> s(s, book, T36),\nT35 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 350 [arrowhead = none ];
350 -> 21;

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

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

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

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

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

356 [label="EVAL with clause\nverb(.(falls, X63), X63, s(s, X64, fall)).\nand substitutionX63 -> [],\nT30 -> .(falls, []),\nT41 -> [],\nX64 -> book,\nT36 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 356 [arrowhead = none ];
356 -> 26;

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

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

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

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

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

362 [label="EVAL with clause\nverb(.(flies, X75), X75, s(s, X76, fly)).\nand substitutionX75 -> [],\nT30 -> .(flies, []),\nT47 -> [],\nX76 -> book,\nT36 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 362 [arrowhead = none ];
362 -> 32;

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

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

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

366 [label="EVAL with clause\nnoun(.(books, X86), X86, -(book, p)).\nand substitutionX86 -> T53,\nT25 -> .(books, T53),\nX34 -> T53,\nX33 -> -(book, p)", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 366 [arrowhead = none ];
366 -> 39;

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

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

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

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

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

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

373 [label="EVAL with clause\nnoun(.(box, X96), X96, -(box, s)).\nand substitutionX96 -> T58,\nT25 -> .(box, T58),\nX34 -> T58,\nX33 -> -(box, s)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 373 [arrowhead = none ];
373 -> 46;

374 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 374 [arrowhead = none ];
374 -> 47;

375 [label="EVAL with clause\nnoun(.(boxes, X136), X136, -(box, p)).\nand substitutionX136 -> T79,\nT25 -> .(boxes, T79),\nX34 -> T79,\nX33 -> -(box, p)", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 375 [arrowhead = none ];
375 -> 67;

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

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

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

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

380 [label="EVAL with clause\ncomb(a, -(X105, s), s(s, X105, X106)).\nand substitutionX105 -> box,\nX106 -> T64,\nT20 -> s(s, box, T64),\nT63 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 380 [arrowhead = none ];
380 -> 51;

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

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

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

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

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

386 [label="EVAL with clause\nverb(.(falls, X115), X115, s(s, X116, fall)).\nand substitutionX115 -> [],\nT58 -> .(falls, []),\nT69 -> [],\nX116 -> box,\nT64 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 386 [arrowhead = none ];
386 -> 56;

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

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

389 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 389 [arrowhead = none ];
389 -> 58;

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

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

392 [label="EVAL with clause\nverb(.(flies, X127), X127, s(s, X128, fly)).\nand substitutionX127 -> [],\nT58 -> .(flies, []),\nT75 -> [],\nX128 -> box,\nT64 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 392 [arrowhead = none ];
392 -> 62;

393 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 393 [arrowhead = none ];
393 -> 63;

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

395 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 395 [arrowhead = none ];
395 -> 64;

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

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

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

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

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

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

402 [label="EVAL with clause\nnoun(.(book, X149), X149, -(book, s)).\nand substitutionX149 -> T87,\nT82 -> .(book, T87),\nX34 -> T87,\nX33 -> -(book, s)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 402 [arrowhead = none ];
402 -> 77;

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

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

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

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

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

408 [label="EVAL with clause\ncomb(the, -(X158, X159), s(X159, X158, X160)).\nand substitutionX158 -> book,\nX159 -> s,\nX160 -> T91,\nT20 -> s(s, book, T91),\nT90 -> T91", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 408 [arrowhead = none ];
408 -> 81;

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

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

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

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

413 [label="EVAL with clause\nverb(.(falls, X169), X169, s(s, X170, fall)).\nand substitutionX169 -> [],\nT87 -> .(falls, []),\nT96 -> [],\nX170 -> book,\nT91 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 413 [arrowhead = none ];
413 -> 86;

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

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

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

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

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

419 [label="EVAL with clause\nverb(.(flies, X181), X181, s(s, X182, fly)).\nand substitutionX181 -> [],\nT87 -> .(flies, []),\nT102 -> [],\nX182 -> book,\nT91 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 419 [arrowhead = none ];
419 -> 92;

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

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

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

423 [label="EVAL with clause\nnoun(.(books, X189), X189, -(book, p)).\nand substitutionX189 -> T108,\nT82 -> .(books, T108),\nX34 -> T108,\nX33 -> -(book, p)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 423 [arrowhead = none ];
423 -> 98;

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

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

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

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

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

429 [label="EVAL with clause\ncomb(the, -(X198, X199), s(X199, X198, X200)).\nand substitutionX198 -> book,\nX199 -> p,\nX200 -> T112,\nT20 -> s(p, book, T112),\nT111 -> T112", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 429 [arrowhead = none ];
429 -> 102;

430 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 430 [arrowhead = none ];
430 -> 103;

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

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

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

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

435 [label="EVAL with clause\nverb(.(fall, X211), X211, s(p, X212, fall)).\nand substitutionX211 -> [],\nT108 -> .(fall, []),\nT118 -> [],\nX212 -> book,\nT112 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 435 [arrowhead = none ];
435 -> 108;

436 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 436 [arrowhead = none ];
436 -> 109;

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

438 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 438 [arrowhead = none ];
438 -> 110;

439 [label="EVAL with clause\nverb(.(fly, X219), X219, s(p, X220, fly)).\nand substitutionX219 -> [],\nT108 -> .(fly, []),\nT122 -> [],\nX220 -> book,\nT112 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 439 [arrowhead = none ];
439 -> 112;

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

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

442 [label="EVAL with clause\nnoun(.(box, X225), X225, -(box, s)).\nand substitutionX225 -> T127,\nT82 -> .(box, T127),\nX34 -> T127,\nX33 -> -(box, s)", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 442 [arrowhead = none ];
442 -> 117;

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

444 [label="EVAL with clause\nnoun(.(boxes, X263), X263, -(box, p)).\nand substitutionX263 -> T146,\nT82 -> .(boxes, T146),\nX34 -> T146,\nX33 -> -(box, p)", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 444 [arrowhead = none ];
444 -> 136;

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

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

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

448 [label="EVAL with clause\ncomb(the, -(X234, X235), s(X235, X234, X236)).\nand substitutionX234 -> box,\nX235 -> s,\nX236 -> T131,\nT20 -> s(s, box, T131),\nT130 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 448 [arrowhead = none ];
448 -> 121;

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

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

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

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

453 [label="EVAL with clause\nverb(.(falls, X245), X245, s(s, X246, fall)).\nand substitutionX245 -> [],\nT127 -> .(falls, []),\nT136 -> [],\nX246 -> box,\nT131 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 453 [arrowhead = none ];
453 -> 126;

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

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

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

457 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
129 -> 457 [arrowhead = none ];
457 -> 130;

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

459 [label="EVAL with clause\nverb(.(flies, X257), X257, s(s, X258, fly)).\nand substitutionX257 -> [],\nT127 -> .(flies, []),\nT142 -> [],\nX258 -> box,\nT131 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 459 [arrowhead = none ];
459 -> 132;

460 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
130 -> 460 [arrowhead = none ];
460 -> 133;

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

462 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 462 [arrowhead = none ];
462 -> 134;

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

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

465 [label="EVAL with clause\ncomb(the, -(X272, X273), s(X273, X272, X274)).\nand substitutionX272 -> box,\nX273 -> p,\nX274 -> T150,\nT20 -> s(p, box, T150),\nT149 -> T150", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 465 [arrowhead = none ];
465 -> 140;

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

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

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

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

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

471 [label="EVAL with clause\nverb(.(fall, X285), X285, s(p, X286, fall)).\nand substitutionX285 -> [],\nT146 -> .(fall, []),\nT156 -> [],\nX286 -> box,\nT150 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 471 [arrowhead = none ];
471 -> 146;

472 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 472 [arrowhead = none ];
472 -> 147;

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

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

475 [label="EVAL with clause\nverb(.(fly, X293), X293, s(p, X294, fly)).\nand substitutionX293 -> [],\nT146 -> .(fly, []),\nT160 -> [],\nX294 -> box,\nT150 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 475 [arrowhead = none ];
475 -> 150;

476 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 476 [arrowhead = none ];
476 -> 151;

477 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
150 -> 477 [arrowhead = none ];
477 -> 152;

478 [label="ONLY EVAL with clause\nparse(X301, X302) :- ','(np(X301, X303, X302), ','(verb(X303, X304, X302), =(X304, []))).\nand substitutionT5 -> T166,\nX301 -> T166,\nT2 -> T168,\nX302 -> T168,\nT167 -> T168", fontsize=14, style = filled, fillcolor = lightblue];
153 -> 478 [arrowhead = none ];
478 -> 154;

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

480 [label="ONLY EVAL with clause\nnp(X316, X317, X318) :- ','(det(X316, X319, X320), ','(noun(X319, X317, X321), comb(X320, X321, X318))).\nand substitutionT166 -> T174,\nX316 -> T174,\nX303 -> X322,\nX317 -> X322,\nT168 -> T176,\nX318 -> T176,\nT175 -> T176", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 480 [arrowhead = none ];
480 -> 156;

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

482 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
157 -> 482 [arrowhead = none ];
482 -> 158;

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

484 [label="EVAL with clause\ndet(.(a, X327), X327, a).\nand substitutionX327 -> T181,\nT174 -> .(a, T181),\nX319 -> T181,\nX320 -> a", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 484 [arrowhead = none ];
484 -> 160;

485 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 485 [arrowhead = none ];
485 -> 161;

486 [label="EVAL with clause\ndet(.(the, X432), X432, the).\nand substitutionX432 -> T238,\nT174 -> .(the, T238),\nX319 -> T238,\nX320 -> the", fontsize=14, style = filled, fillcolor = lightblue];
159 -> 486 [arrowhead = none ];
486 -> 229;

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

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

489 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
162 -> 489 [arrowhead = none ];
489 -> 163;

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

491 [label="EVAL with clause\nnoun(.(book, X332), X332, -(book, s)).\nand substitutionX332 -> T186,\nT181 -> .(book, T186),\nX322 -> T186,\nX321 -> -(book, s)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 491 [arrowhead = none ];
491 -> 165;

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

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

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

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

496 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
167 -> 496 [arrowhead = none ];
496 -> 168;

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

498 [label="EVAL with clause\ncomb(a, -(X341, s), s(s, X341, X342)).\nand substitutionX341 -> book,\nX342 -> T192,\nT176 -> s(s, book, T192),\nT191 -> T192", fontsize=14, style = filled, fillcolor = lightblue];
168 -> 498 [arrowhead = none ];
498 -> 170;

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

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

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

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

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

504 [label="EVAL with clause\nverb(.(falls, X351), X351, s(s, X352, fall)).\nand substitutionX351 -> T197,\nT186 -> .(falls, T197),\nX304 -> T197,\nX352 -> book,\nT192 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 504 [arrowhead = none ];
504 -> 175;

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

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

507 [label="UNIFY CASE with substitutionT197 -> []", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 507 [arrowhead = none ];
507 -> 177;

508 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
175 -> 508 [arrowhead = none ];
508 -> 178;

509 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 509 [arrowhead = none ];
509 -> 179;

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

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

512 [label="EVAL with clause\nverb(.(flies, X363), X363, s(s, X364, fly)).\nand substitutionX363 -> T203,\nT186 -> .(flies, T203),\nX304 -> T203,\nX364 -> book,\nT192 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 512 [arrowhead = none ];
512 -> 183;

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

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

515 [label="UNIFY CASE with substitutionT203 -> []", fontsize=14, style = filled, fillcolor = lightblue];
183 -> 515 [arrowhead = none ];
515 -> 185;

516 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
183 -> 516 [arrowhead = none ];
516 -> 186;

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

518 [label="EVAL with clause\nnoun(.(books, X374), X374, -(book, p)).\nand substitutionX374 -> T209,\nT181 -> .(books, T209),\nX322 -> T209,\nX321 -> -(book, p)", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 518 [arrowhead = none ];
518 -> 192;

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

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

521 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
191 -> 521 [arrowhead = none ];
521 -> 198;

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

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

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

525 [label="EVAL with clause\nnoun(.(box, X384), X384, -(box, s)).\nand substitutionX384 -> T214,\nT181 -> .(box, T214),\nX322 -> T214,\nX321 -> -(box, s)", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 525 [arrowhead = none ];
525 -> 199;

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

527 [label="EVAL with clause\nnoun(.(boxes, X424), X424, -(box, p)).\nand substitutionX424 -> T235,\nT181 -> .(boxes, T235),\nX322 -> T235,\nX321 -> -(box, p)", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 527 [arrowhead = none ];
527 -> 224;

528 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
198 -> 528 [arrowhead = none ];
528 -> 225;

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

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

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

532 [label="EVAL with clause\ncomb(a, -(X393, s), s(s, X393, X394)).\nand substitutionX393 -> box,\nX394 -> T220,\nT176 -> s(s, box, T220),\nT219 -> T220", fontsize=14, style = filled, fillcolor = lightblue];
202 -> 532 [arrowhead = none ];
532 -> 204;

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

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

535 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
204 -> 535 [arrowhead = none ];
535 -> 206;

536 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
206 -> 536 [arrowhead = none ];
536 -> 207;

537 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
206 -> 537 [arrowhead = none ];
537 -> 208;

538 [label="EVAL with clause\nverb(.(falls, X403), X403, s(s, X404, fall)).\nand substitutionX403 -> T225,\nT214 -> .(falls, T225),\nX304 -> T225,\nX404 -> box,\nT220 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 538 [arrowhead = none ];
538 -> 209;

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

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

541 [label="UNIFY CASE with substitutionT225 -> []", fontsize=14, style = filled, fillcolor = lightblue];
209 -> 541 [arrowhead = none ];
541 -> 211;

542 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 542 [arrowhead = none ];
542 -> 212;

543 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
211 -> 543 [arrowhead = none ];
543 -> 213;

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

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

546 [label="EVAL with clause\nverb(.(flies, X415), X415, s(s, X416, fly)).\nand substitutionX415 -> T231,\nT214 -> .(flies, T231),\nX304 -> T231,\nX416 -> box,\nT220 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 546 [arrowhead = none ];
546 -> 217;

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

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

549 [label="UNIFY CASE with substitutionT231 -> []", fontsize=14, style = filled, fillcolor = lightblue];
217 -> 549 [arrowhead = none ];
549 -> 219;

550 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 550 [arrowhead = none ];
550 -> 220;

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

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

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

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

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

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

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

558 [label="EVAL with clause\nnoun(.(book, X437), X437, -(book, s)).\nand substitutionX437 -> T243,\nT238 -> .(book, T243),\nX322 -> T243,\nX321 -> -(book, s)", fontsize=14, style = filled, fillcolor = lightblue];
232 -> 558 [arrowhead = none ];
558 -> 234;

559 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
232 -> 559 [arrowhead = none ];
559 -> 235;

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

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

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

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

564 [label="EVAL with clause\ncomb(the, -(X446, X447), s(X447, X446, X448)).\nand substitutionX446 -> book,\nX447 -> s,\nX448 -> T247,\nT176 -> s(s, book, T247),\nT246 -> T247", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 564 [arrowhead = none ];
564 -> 238;

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

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

567 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
240 -> 567 [arrowhead = none ];
567 -> 241;

568 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
240 -> 568 [arrowhead = none ];
568 -> 242;

569 [label="EVAL with clause\nverb(.(falls, X457), X457, s(s, X458, fall)).\nand substitutionX457 -> T252,\nT243 -> .(falls, T252),\nX304 -> T252,\nX458 -> book,\nT247 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
241 -> 569 [arrowhead = none ];
569 -> 243;

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

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

572 [label="UNIFY CASE with substitutionT252 -> []", fontsize=14, style = filled, fillcolor = lightblue];
243 -> 572 [arrowhead = none ];
572 -> 245;

573 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
243 -> 573 [arrowhead = none ];
573 -> 246;

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

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

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

577 [label="EVAL with clause\nverb(.(flies, X469), X469, s(s, X470, fly)).\nand substitutionX469 -> T258,\nT243 -> .(flies, T258),\nX304 -> T258,\nX470 -> book,\nT247 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
249 -> 577 [arrowhead = none ];
577 -> 251;

578 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
249 -> 578 [arrowhead = none ];
578 -> 252;

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

580 [label="UNIFY CASE with substitutionT258 -> []", fontsize=14, style = filled, fillcolor = lightblue];
251 -> 580 [arrowhead = none ];
580 -> 253;

581 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
251 -> 581 [arrowhead = none ];
581 -> 254;

582 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
253 -> 582 [arrowhead = none ];
582 -> 255;

583 [label="EVAL with clause\nnoun(.(books, X477), X477, -(book, p)).\nand substitutionX477 -> T264,\nT238 -> .(books, T264),\nX322 -> T264,\nX321 -> -(book, p)", fontsize=14, style = filled, fillcolor = lightblue];
257 -> 583 [arrowhead = none ];
583 -> 259;

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

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

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

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

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

589 [label="EVAL with clause\ncomb(the, -(X486, X487), s(X487, X486, X488)).\nand substitutionX486 -> book,\nX487 -> p,\nX488 -> T268,\nT176 -> s(p, book, T268),\nT267 -> T268", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 589 [arrowhead = none ];
589 -> 263;

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

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

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

593 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
266 -> 593 [arrowhead = none ];
593 -> 267;

594 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
266 -> 594 [arrowhead = none ];
594 -> 268;

595 [label="EVAL with clause\nverb(.(fall, X499), X499, s(p, X500, fall)).\nand substitutionX499 -> T274,\nT264 -> .(fall, T274),\nX304 -> T274,\nX500 -> book,\nT268 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
267 -> 595 [arrowhead = none ];
595 -> 269;

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

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

598 [label="UNIFY CASE with substitutionT274 -> []", fontsize=14, style = filled, fillcolor = lightblue];
269 -> 598 [arrowhead = none ];
598 -> 271;

599 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
269 -> 599 [arrowhead = none ];
599 -> 272;

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

601 [label="EVAL with clause\nverb(.(fly, X507), X507, s(p, X508, fly)).\nand substitutionX507 -> T278,\nT264 -> .(fly, T278),\nX304 -> T278,\nX508 -> book,\nT268 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
274 -> 601 [arrowhead = none ];
601 -> 275;

602 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
274 -> 602 [arrowhead = none ];
602 -> 276;

603 [label="UNIFY CASE with substitutionT278 -> []", fontsize=14, style = filled, fillcolor = lightblue];
275 -> 603 [arrowhead = none ];
603 -> 277;

604 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
275 -> 604 [arrowhead = none ];
604 -> 278;

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

606 [label="EVAL with clause\nnoun(.(box, X513), X513, -(box, s)).\nand substitutionX513 -> T283,\nT238 -> .(box, T283),\nX322 -> T283,\nX321 -> -(box, s)", fontsize=14, style = filled, fillcolor = lightblue];
280 -> 606 [arrowhead = none ];
606 -> 282;

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

608 [label="EVAL with clause\nnoun(.(boxes, X551), X551, -(box, p)).\nand substitutionX551 -> T302,\nT238 -> .(boxes, T302),\nX322 -> T302,\nX321 -> -(box, p)", fontsize=14, style = filled, fillcolor = lightblue];
281 -> 608 [arrowhead = none ];
608 -> 305;

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

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

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

612 [label="EVAL with clause\ncomb(the, -(X522, X523), s(X523, X522, X524)).\nand substitutionX522 -> box,\nX523 -> s,\nX524 -> T287,\nT176 -> s(s, box, T287),\nT286 -> T287", fontsize=14, style = filled, fillcolor = lightblue];
285 -> 612 [arrowhead = none ];
612 -> 286;

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

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

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

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

617 [label="EVAL with clause\nverb(.(falls, X533), X533, s(s, X534, fall)).\nand substitutionX533 -> T292,\nT283 -> .(falls, T292),\nX304 -> T292,\nX534 -> box,\nT287 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
289 -> 617 [arrowhead = none ];
617 -> 291;

618 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
289 -> 618 [arrowhead = none ];
618 -> 292;

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

620 [label="UNIFY CASE with substitutionT292 -> []", fontsize=14, style = filled, fillcolor = lightblue];
291 -> 620 [arrowhead = none ];
620 -> 293;

621 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
291 -> 621 [arrowhead = none ];
621 -> 294;

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

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

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

625 [label="EVAL with clause\nverb(.(flies, X545), X545, s(s, X546, fly)).\nand substitutionX545 -> T298,\nT283 -> .(flies, T298),\nX304 -> T298,\nX546 -> box,\nT287 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
297 -> 625 [arrowhead = none ];
625 -> 299;

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

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

628 [label="UNIFY CASE with substitutionT298 -> []", fontsize=14, style = filled, fillcolor = lightblue];
299 -> 628 [arrowhead = none ];
628 -> 301;

629 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
299 -> 629 [arrowhead = none ];
629 -> 302;

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

631 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
305 -> 631 [arrowhead = none ];
631 -> 307;

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

633 [label="EVAL with clause\ncomb(the, -(X560, X561), s(X561, X560, X562)).\nand substitutionX560 -> box,\nX561 -> p,\nX562 -> T306,\nT176 -> s(p, box, T306),\nT305 -> T306", fontsize=14, style = filled, fillcolor = lightblue];
308 -> 633 [arrowhead = none ];
633 -> 309;

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

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

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

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

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

639 [label="EVAL with clause\nverb(.(fall, X573), X573, s(p, X574, fall)).\nand substitutionX573 -> T312,\nT302 -> .(fall, T312),\nX304 -> T312,\nX574 -> box,\nT306 -> fall", fontsize=14, style = filled, fillcolor = lightblue];
313 -> 639 [arrowhead = none ];
639 -> 315;

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

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

642 [label="UNIFY CASE with substitutionT312 -> []", fontsize=14, style = filled, fillcolor = lightblue];
315 -> 642 [arrowhead = none ];
642 -> 317;

643 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
315 -> 643 [arrowhead = none ];
643 -> 318;

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

645 [label="EVAL with clause\nverb(.(fly, X581), X581, s(p, X582, fly)).\nand substitutionX581 -> T316,\nT302 -> .(fly, T316),\nX304 -> T316,\nX582 -> box,\nT306 -> fly", fontsize=14, style = filled, fillcolor = lightblue];
320 -> 645 [arrowhead = none ];
645 -> 321;

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

647 [label="UNIFY CASE with substitutionT316 -> []", fontsize=14, style = filled, fillcolor = lightblue];
321 -> 647 [arrowhead = none ];
647 -> 323;

648 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
321 -> 648 [arrowhead = none ];
648 -> 324;

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

}

(2) Obligation:

Clauses:

parseA(.(a, .(book, .(falls, []))), s(s, book, fall)).
parseA(.(a, .(book, .(flies, []))), s(s, book, fly)).
parseA(.(a, .(box, .(falls, []))), s(s, box, fall)).
parseA(.(a, .(box, .(flies, []))), s(s, box, fly)).
parseA(.(the, .(book, .(falls, []))), s(s, book, fall)).
parseA(.(the, .(book, .(flies, []))), s(s, book, fly)).
parseA(.(the, .(books, .(fall, []))), s(p, book, fall)).
parseA(.(the, .(books, .(fly, []))), s(p, book, fly)).
parseA(.(the, .(box, .(falls, []))), s(s, box, fall)).
parseA(.(the, .(box, .(flies, []))), s(s, box, fly)).
parseA(.(the, .(boxes, .(fall, []))), s(p, box, fall)).
parseA(.(the, .(boxes, .(fly, []))), s(p, box, fly)).
parseA(.(a, .(book, .(falls, []))), s(s, book, fall)).
parseA(.(a, .(book, .(flies, []))), s(s, book, fly)).
parseA(.(a, .(box, .(falls, []))), s(s, box, fall)).
parseA(.(a, .(box, .(flies, []))), s(s, box, fly)).
parseA(.(the, .(book, .(falls, []))), s(s, book, fall)).
parseA(.(the, .(book, .(flies, []))), s(s, book, fly)).
parseA(.(the, .(books, .(fall, []))), s(p, book, fall)).
parseA(.(the, .(books, .(fly, []))), s(p, book, fly)).
parseA(.(the, .(box, .(falls, []))), s(s, box, fall)).
parseA(.(the, .(box, .(flies, []))), s(s, box, fly)).
parseA(.(the, .(boxes, .(fall, []))), s(p, box, fall)).
parseA(.(the, .(boxes, .(fly, []))), s(p, box, fly)).

Query: parseA(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

parseA_in_ga(.(a, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(a, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(a, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(a, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(a, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(a, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(a, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(a, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(the, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(the, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(the, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(the, .(books, .(fall, []))), s(p, book, fall)) → parseA_out_ga(.(the, .(books, .(fall, []))), s(p, book, fall))
parseA_in_ga(.(the, .(books, .(fly, []))), s(p, book, fly)) → parseA_out_ga(.(the, .(books, .(fly, []))), s(p, book, fly))
parseA_in_ga(.(the, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(the, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(the, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(the, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall)) → parseA_out_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall))
parseA_in_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly)) → parseA_out_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly))

The argument filtering Pi contains the following mapping:
parseA_in_ga(x1, x2) = parseA_in_ga(x1)
.(x1, x2) = .(x1, x2)
a = a
book = book
falls = falls
[] = []
parseA_out_ga(x1, x2) = parseA_out_ga(x2)
flies = flies
box = box
the = the
books = books
fall = fall
fly = fly
boxes = boxes

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

parseA_in_ga(.(a, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(a, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(a, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(a, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(a, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(a, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(a, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(a, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(the, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(the, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(the, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(the, .(books, .(fall, []))), s(p, book, fall)) → parseA_out_ga(.(the, .(books, .(fall, []))), s(p, book, fall))
parseA_in_ga(.(the, .(books, .(fly, []))), s(p, book, fly)) → parseA_out_ga(.(the, .(books, .(fly, []))), s(p, book, fly))
parseA_in_ga(.(the, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(the, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(the, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(the, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall)) → parseA_out_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall))
parseA_in_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly)) → parseA_out_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly))

(5) DependencyPairsProof (EQUIVALENT transformation)

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

parseA_in_ga(.(a, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(a, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(a, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(a, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(a, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(a, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(a, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(a, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(the, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(the, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(the, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(the, .(books, .(fall, []))), s(p, book, fall)) → parseA_out_ga(.(the, .(books, .(fall, []))), s(p, book, fall))
parseA_in_ga(.(the, .(books, .(fly, []))), s(p, book, fly)) → parseA_out_ga(.(the, .(books, .(fly, []))), s(p, book, fly))
parseA_in_ga(.(the, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(the, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(the, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(the, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall)) → parseA_out_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall))
parseA_in_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly)) → parseA_out_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly))

(6) Obligation:

Pi DP problem:
P is empty.
The TRS R consists of the following rules:

parseA_in_ga(.(a, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(a, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(a, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(a, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(a, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(a, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(a, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(a, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(book, .(falls, []))), s(s, book, fall)) → parseA_out_ga(.(the, .(book, .(falls, []))), s(s, book, fall))
parseA_in_ga(.(the, .(book, .(flies, []))), s(s, book, fly)) → parseA_out_ga(.(the, .(book, .(flies, []))), s(s, book, fly))
parseA_in_ga(.(the, .(books, .(fall, []))), s(p, book, fall)) → parseA_out_ga(.(the, .(books, .(fall, []))), s(p, book, fall))
parseA_in_ga(.(the, .(books, .(fly, []))), s(p, book, fly)) → parseA_out_ga(.(the, .(books, .(fly, []))), s(p, book, fly))
parseA_in_ga(.(the, .(box, .(falls, []))), s(s, box, fall)) → parseA_out_ga(.(the, .(box, .(falls, []))), s(s, box, fall))
parseA_in_ga(.(the, .(box, .(flies, []))), s(s, box, fly)) → parseA_out_ga(.(the, .(box, .(flies, []))), s(s, box, fly))
parseA_in_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall)) → parseA_out_ga(.(the, .(boxes, .(fall, []))), s(p, box, fall))
parseA_in_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly)) → parseA_out_ga(.(the, .(boxes, .(fly, []))), s(p, box, fly))

(7) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,R,Pi) chain.