Left Termination of the query pattern front_in_2(a, g) w.r.t. the given Prolog program could not be shown:

(0) Obligation:

Clauses:

front(void, []).
front(tree(X, void, void), .(X, [])).
front(tree(X1, L, R), Xs) :- ','(front(L, Ls), ','(front(R, Rs), app(Ls, Rs, Xs))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Queries:

front(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: front(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: front(T1, T2), SCOPE: 1, CLAUSE: 0 | front(T1, T2), SCOPE: 1, CLAUSE: 1 | front(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | front(T1, []), SCOPE: 1, CLAUSE: 1 | front(T1, []), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: front(T1, T2), SCOPE: 1, CLAUSE: 1 | front(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nfront(T1, T2) !=? front(void, [])", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: front(T1, []), SCOPE: 1, CLAUSE: 1 | front(T1, []), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: front(T1, []), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, [])))\n\nX11 is free\nX12 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, []))), SCOPE: 2, CLAUSE: 0 | ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, []))), SCOPE: 2, CLAUSE: 1 | ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, []))), SCOPE: 2, CLAUSE: 2\n\nX11 is free\nX12 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, []))), SCOPE: 2, CLAUSE: 0\n\nX11 is free\nX12 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, []))), SCOPE: 2, CLAUSE: 1 | ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, []))), SCOPE: 2, CLAUSE: 2\n\nX11 is free\nX12 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(front(T12, X12), app([], X12, []))\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: front(T12, X12)\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: app([], T13, [])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: front(T12, X12), SCOPE: 3, CLAUSE: 0 | front(T12, X12), SCOPE: 3, CLAUSE: 1 | front(T12, X12), SCOPE: 3, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: front(T12, X12), SCOPE: 3, CLAUSE: 0\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: front(T12, X12), SCOPE: 3, CLAUSE: 1 | front(T12, X12), SCOPE: 3, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: front(T12, X12), SCOPE: 3, CLAUSE: 1\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: front(T12, X12), SCOPE: 3, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(front(T28, X39), ','(front(T29, X40), app(X39, X40, X41)))\n\nX41 is free\nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: front(T28, X39)\n\nX39 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(front(T31, X40), app(T30, X40, X41))\n\nX41 is free\nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: front(T31, X40)\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: app(T33, T32, X41)\n\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: app(T33, T32, X41), SCOPE: 4, CLAUSE: 3 | app(T33, T32, X41), SCOPE: 4, CLAUSE: 4\n\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: app(T33, T32, X41), SCOPE: 4, CLAUSE: 3\n\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: app(T33, T32, X41), SCOPE: 4, CLAUSE: 4\n\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: app(T50, T51, X68)\n\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: app([], T13, []), SCOPE: 5, CLAUSE: 3 | app([], T13, []), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: app([], T13, []), SCOPE: 5, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: app([], T13, []), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, []))), SCOPE: 2, CLAUSE: 1\n\nX11 is free\nX12 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(front(T10, X11), ','(front(T11, X12), app(X11, X12, []))), SCOPE: 2, CLAUSE: 2\n\nX11 is free\nX12 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(front(T66, X12), app(.(T67, []), X12, []))\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: front(T66, X12)\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: app(.(T69, []), T68, [])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: app(.(T69, []), T68, []), SCOPE: 6, CLAUSE: 3 | app(.(T69, []), T68, []), SCOPE: 6, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: app(.(T69, []), T68, []), SCOPE: 6, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(front(T83, X120), ','(front(T84, X121), ','(app(X120, X121, X122), ','(front(T85, X12), app(X122, X12, [])))))\n\nX12 is free\nX122 is free; \nX120 is free; \nX121 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: front(T83, X120)\n\nX120 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(front(T87, X121), ','(app(T86, X121, X122), ','(front(T88, X12), app(X122, X12, []))))\n\nX12 is free\nX122 is free; \nX121 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: front(T87, X121)\n\nX121 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(app(T90, T89, X122), ','(front(T91, X12), app(X122, X12, [])))\n\nX12 is free\nX122 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: app(T90, T89, X122)\n\nX122 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(front(T95, X12), app(T94, X12, []))\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: front(T95, X12)\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: app(T99, T98, [])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: app(T99, T98, []), SCOPE: 7, CLAUSE: 3 | app(T99, T98, []), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: app(T99, T98, []), SCOPE: 7, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: app(T99, T98, []), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: true | front(T1, .(T111, [])), SCOPE: 1, CLAUSE: 2\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: front(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nfront(T1, T2) !=? front(void, [])\nfront(T1, T2) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: front(T1, .(T111, [])), SCOPE: 1, CLAUSE: 2\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, []))))\n\nT119 is ground\nX154 is free; \nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, [])))), SCOPE: 8, CLAUSE: 0 | ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, [])))), SCOPE: 8, CLAUSE: 1 | ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, [])))), SCOPE: 8, CLAUSE: 2\n\nT119 is ground\nX154 is free; \nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, [])))), SCOPE: 8, CLAUSE: 0\n\nT119 is ground\nX154 is free; \nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, [])))), SCOPE: 8, CLAUSE: 1 | ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, [])))), SCOPE: 8, CLAUSE: 2\n\nT119 is ground\nX154 is free; \nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(front(T122, X155), app([], X155, .(T119, [])))\n\nT119 is ground\nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: front(T122, X155)\n\nX155 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: app([], T123, .(T119, []))\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: app([], T123, .(T119, [])), SCOPE: 9, CLAUSE: 3 | app([], T123, .(T119, [])), SCOPE: 9, CLAUSE: 4\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: app([], T123, .(T119, [])), SCOPE: 9, CLAUSE: 3\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: app([], T123, .(T119, [])), SCOPE: 9, CLAUSE: 4\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, [])))), SCOPE: 8, CLAUSE: 1\n\nT119 is ground\nX154 is free; \nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(front(T120, X154), ','(front(T121, X155), app(X154, X155, .(T119, [])))), SCOPE: 8, CLAUSE: 2\n\nT119 is ground\nX154 is free; \nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(front(T143, X155), app(.(T144, []), X155, .(T119, [])))\n\nT119 is ground\nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: front(T143, X155)\n\nX155 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: app(.(T146, []), T145, .(T119, []))\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: app(.(T146, []), T145, .(T119, [])), SCOPE: 10, CLAUSE: 3 | app(.(T146, []), T145, .(T119, [])), SCOPE: 10, CLAUSE: 4\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: app(.(T146, []), T145, .(T119, [])), SCOPE: 10, CLAUSE: 4\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: app([], T155, [])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(front(T167, X219), ','(front(T168, X220), ','(app(X219, X220, X221), ','(front(T169, X155), app(X221, X155, .(T119, []))))))\n\nT119 is ground\nX155 is free; \nX221 is free; \nX219 is free; \nX220 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: front(T167, X219)\n\nX219 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(front(T171, X220), ','(app(T170, X220, X221), ','(front(T172, X155), app(X221, X155, .(T119, [])))))\n\nT119 is ground\nX155 is free; \nX221 is free; \nX220 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: front(T171, X220)\n\nX220 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(app(T174, T173, X221), ','(front(T175, X155), app(X221, X155, .(T119, []))))\n\nT119 is ground\nX155 is free; \nX221 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: app(T174, T173, X221)\n\nX221 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(front(T179, X155), app(T178, X155, .(T119, [])))\n\nT119 is ground\nX155 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: front(T179, X155)\n\nX155 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: app(T183, T182, .(T119, []))\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: app(T183, T182, .(T119, [])), SCOPE: 11, CLAUSE: 3 | app(T183, T182, .(T119, [])), SCOPE: 11, CLAUSE: 4\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: app(T183, T182, .(T119, [])), SCOPE: 11, CLAUSE: 3\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: app(T183, T182, .(T119, [])), SCOPE: 11, CLAUSE: 4\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: app(T207, T208, [])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218)))\n\nT218 is ground\nX264 is free; \nX265 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218))), SCOPE: 12, CLAUSE: 0 | ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218))), SCOPE: 12, CLAUSE: 1 | ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218))), SCOPE: 12, CLAUSE: 2\n\nT218 is ground\nX264 is free; \nX265 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218))), SCOPE: 12, CLAUSE: 0\n\nT218 is ground\nX264 is free; \nX265 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218))), SCOPE: 12, CLAUSE: 1 | ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218))), SCOPE: 12, CLAUSE: 2\n\nT218 is ground\nX264 is free; \nX265 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(front(T221, X265), app([], X265, T218))\n\nT218 is ground\nX265 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: front(T221, X265)\n\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: app([], T222, T218)\n\nT218 is ground\nfront(T223, T218) !=? front(void, [])\nfront(T223, T218) !=? front(tree(T224, void, void), .(T224, []))", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: app([], T222, T218), SCOPE: 13, CLAUSE: 3 | app([], T222, T218), SCOPE: 13, CLAUSE: 4\n\nT218 is ground\nfront(T223, T218) !=? front(void, [])\nfront(T223, T218) !=? front(tree(T224, void, void), .(T224, []))", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: app([], T222, T218), SCOPE: 13, CLAUSE: 3\n\nT218 is ground\nfront(T223, T218) !=? front(void, [])\nfront(T223, T218) !=? front(tree(T224, void, void), .(T224, []))", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: app([], T222, T218), SCOPE: 13, CLAUSE: 4\n\nT218 is ground\nfront(T223, T218) !=? front(void, [])\nfront(T223, T218) !=? front(tree(T224, void, void), .(T224, []))", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: true\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: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218))), SCOPE: 12, CLAUSE: 1\n\nT218 is ground\nX264 is free; \nX265 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(front(T219, X264), ','(front(T220, X265), app(X264, X265, T218))), SCOPE: 12, CLAUSE: 2\n\nT218 is ground\nX264 is free; \nX265 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(front(T237, X265), app(.(T238, []), X265, T218))\n\nT218 is ground\nX265 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: front(T237, X265)\n\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: app(.(T240, []), T239, T218)\n\nT218 is ground\nfront(T241, T218) !=? front(void, [])\nfront(T241, T218) !=? front(tree(T242, void, void), .(T242, []))", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: app(.(T240, []), T239, T218), SCOPE: 14, CLAUSE: 3 | app(.(T240, []), T239, T218), SCOPE: 14, CLAUSE: 4\n\nT218 is ground\nfront(T241, T218) !=? front(void, [])\nfront(T241, T218) !=? front(tree(T242, void, void), .(T242, []))", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: app(.(T240, []), T239, T218), SCOPE: 14, CLAUSE: 4\n\nT218 is ground\nfront(T241, T218) !=? front(void, [])\nfront(T241, T218) !=? front(tree(T242, void, void), .(T242, []))", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: app([], T255, T254)\n\nT254 is ground\nfront(T241, .(T252, T254)) !=? front(tree(T242, void, void), .(T242, []))", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: app([], T255, T254), SCOPE: 15, CLAUSE: 3 | app([], T255, T254), SCOPE: 15, CLAUSE: 4\n\nT254 is ground\nfront(T241, .(T252, T254)) !=? front(tree(T242, void, void), .(T242, []))", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: app([], T255, T254), SCOPE: 15, CLAUSE: 3\n\nT254 is ground\nfront(T241, .(T252, T254)) !=? front(tree(T242, void, void), .(T242, []))", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: app([], T255, T254), SCOPE: 15, CLAUSE: 4\n\nT254 is ground\nfront(T241, .(T252, T254)) !=? front(tree(T242, void, void), .(T242, []))", 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: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(front(T272, X339), ','(front(T273, X340), ','(app(X339, X340, X341), ','(front(T274, X265), app(X341, X265, T218)))))\n\nT218 is ground\nX265 is free; \nX341 is free; \nX339 is free; \nX340 is free; \nfront(T1, T218) !=? front(void, [])\nfront(T1, T218) !=? front(tree(X144, void, void), .(X144, []))", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: front(T272, X339)\n\nX339 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(front(T276, X340), ','(app(T275, X340, X341), ','(front(T277, X265), app(X341, X265, T218))))\n\nT218 is ground\nX265 is free; \nX341 is free; \nX340 is free; \nfront(T278, T218) !=? front(void, [])\nfront(T278, T218) !=? front(tree(T279, void, void), .(T279, []))", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: front(T276, X340)\n\nX340 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(app(T281, T280, X341), ','(front(T282, X265), app(X341, X265, T218)))\n\nT218 is ground\nX265 is free; \nX341 is free; \nfront(T283, T218) !=? front(void, [])\nfront(T283, T218) !=? front(tree(T284, void, void), .(T284, []))", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: app(T281, T280, X341)\n\nX341 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(front(T288, X265), app(T287, X265, T218))\n\nT218 is ground\nX265 is free; \nfront(T289, T218) !=? front(void, [])\nfront(T289, T218) !=? front(tree(T290, void, void), .(T290, []))", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: front(T288, X265)\n\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: app(T294, T293, T218)\n\nT218 is ground\nfront(T295, T218) !=? front(void, [])\nfront(T295, T218) !=? front(tree(T296, void, void), .(T296, []))", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: app(T294, T293, T218), SCOPE: 16, CLAUSE: 3 | app(T294, T293, T218), SCOPE: 16, CLAUSE: 4\n\nT218 is ground\nfront(T295, T218) !=? front(void, [])\nfront(T295, T218) !=? front(tree(T296, void, void), .(T296, []))", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: app(T294, T293, T218), SCOPE: 16, CLAUSE: 3\n\nT218 is ground\nfront(T295, T218) !=? front(void, [])\nfront(T295, T218) !=? front(tree(T296, void, void), .(T296, []))", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: app(T294, T293, T218), SCOPE: 16, CLAUSE: 4\n\nT218 is ground\nfront(T295, T218) !=? front(void, [])\nfront(T295, T218) !=? front(tree(T296, void, void), .(T296, []))", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: app(T316, T317, T315)\n\nT315 is ground\nfront(T295, .(T312, T315)) !=? front(tree(T296, void, void), .(T296, []))", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: app(T316, T317, T315), SCOPE: 17, CLAUSE: 3 | app(T316, T317, T315), SCOPE: 17, CLAUSE: 4\n\nT315 is ground\nfront(T295, .(T312, T315)) !=? front(tree(T296, void, void), .(T296, []))", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: app(T316, T317, T315), SCOPE: 17, CLAUSE: 3\n\nT315 is ground\nfront(T295, .(T312, T315)) !=? front(tree(T296, void, void), .(T296, []))", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: app(T316, T317, T315), SCOPE: 17, CLAUSE: 4\n\nT315 is ground\nfront(T295, .(T312, T315)) !=? front(tree(T296, void, void), .(T296, []))", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: app(T337, T338, T336)\n\nT336 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: app(T337, T338, T336), SCOPE: 18, CLAUSE: 3 | app(T337, T338, T336), SCOPE: 18, CLAUSE: 4\n\nT336 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: app(T337, T338, T336), SCOPE: 18, CLAUSE: 3\n\nT336 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: app(T337, T338, T336), SCOPE: 18, CLAUSE: 4\n\nT336 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: app(T358, T359, T357)\n\nT357 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 188 [arrowhead = none ];
188 -> 2;

189 [label="EVAL with clause\nfront(void, []).\nand substitution\nT1 -> void\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 189 [arrowhead = none ];
189 -> 3;

190 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 190 [arrowhead = none ];
190 -> 4;

191 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 191 [arrowhead = none ];
191 -> 5;

192 [label="EVAL with clause\nfront(tree(X144, void, void), .(X144, [])).\nand substitution\nX144 -> T111\nT1 -> tree(T111, void, void)\nT2 -> .(T111, [])", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 192 [arrowhead = none ];
192 -> 74;

193 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 193 [arrowhead = none ];
193 -> 75;

194 [label="BACKTRACK\nfor clause: front(tree(X, void, void), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = white];
5 -> 194 [arrowhead = none ];
194 -> 6;

195 [label="EVAL with clause\nfront(tree(X7, X8, X9), X10) :- ','(front(X8, X11), ','(front(X9, X12), app(X11, X12, X10))).\nand substitution\nX7 -> T7\nX8 -> T10\nX9 -> T11\nT1 -> tree(T7, T10, T11)\nX10 -> []\nT8 -> T10\nT9 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 195 [arrowhead = none ];
195 -> 7;

196 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 196 [arrowhead = none ];
196 -> 8;

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

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

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

200 [label="EVAL with clause\nfront(void, []).\nand substitution\nT10 -> void\nX11 -> []\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 200 [arrowhead = none ];
200 -> 12;

201 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 201 [arrowhead = none ];
201 -> 13;

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

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

204 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
12 -> 204 [arrowhead = none ];
204 -> 14;

205 [label="SPLIT 2\nreplacements:\nX12 -> T13", fontsize=14, style = filled, fillcolor = violet];
12 -> 205 [arrowhead = none ];
205 -> 15;

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

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

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

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

210 [label="EVAL with clause\nfront(void, []).\nand substitution\nT12 -> void\nX12 -> []", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 210 [arrowhead = none ];
210 -> 19;

211 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 211 [arrowhead = none ];
211 -> 20;

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

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

214 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 214 [arrowhead = none ];
214 -> 21;

215 [label="EVAL with clause\nfront(tree(X21, void, void), .(X21, [])).\nand substitution\nX21 -> T18\nT12 -> tree(T18, void, void)\nX12 -> .(T18, [])", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 215 [arrowhead = none ];
215 -> 24;

216 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 216 [arrowhead = none ];
216 -> 25;

217 [label="EVAL with clause\nfront(tree(X35, X36, X37), X38) :- ','(front(X36, X39), ','(front(X37, X40), app(X39, X40, X38))).\nand substitution\nX35 -> T25\nX36 -> T28\nX37 -> T29\nT12 -> tree(T25, T28, T29)\nX12 -> X41\nX38 -> X41\nT26 -> T28\nT27 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 217 [arrowhead = none ];
217 -> 27;

218 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 218 [arrowhead = none ];
218 -> 28;

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

220 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
27 -> 220 [arrowhead = none ];
220 -> 29;

221 [label="SPLIT 2\nreplacements:\nX39 -> T30\nT29 -> T31", fontsize=14, style = filled, fillcolor = violet];
27 -> 221 [arrowhead = none ];
221 -> 30;

222 [label="INSTANCE with matching:\nT12 -> T28\nX12 -> X39", fontsize=14, style = filled, fillcolor = lightgrey];
29 -> 222 [arrowhead = none , style=dashed];
222 -> 14[style=dashed];

223 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
30 -> 223 [arrowhead = none ];
223 -> 31;

224 [label="SPLIT 2\nreplacements:\nX40 -> T32\nT30 -> T33", fontsize=14, style = filled, fillcolor = violet];
30 -> 224 [arrowhead = none ];
224 -> 32;

225 [label="INSTANCE with matching:\nT12 -> T31\nX12 -> X40", fontsize=14, style = filled, fillcolor = lightgrey];
31 -> 225 [arrowhead = none , style=dashed];
225 -> 14[style=dashed];

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

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

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

229 [label="EVAL with clause\napp([], X52, X52).\nand substitution\nT33 -> []\nT32 -> T40\nX52 -> T40\nX41 -> T40", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 229 [arrowhead = none ];
229 -> 36;

230 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 230 [arrowhead = none ];
230 -> 37;

231 [label="EVAL with clause\napp(.(X64, X65), X66, .(X64, X67)) :- app(X65, X66, X67).\nand substitution\nX64 -> T47\nX65 -> T50\nT33 -> .(T47, T50)\nT32 -> T51\nX66 -> T51\nX67 -> X68\nX41 -> .(T47, X68)\nT48 -> T50\nT49 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 231 [arrowhead = none ];
231 -> 39;

232 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 232 [arrowhead = none ];
232 -> 40;

233 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 233 [arrowhead = none ];
233 -> 38;

234 [label="INSTANCE with matching:\nT33 -> T50\nT32 -> T51\nX41 -> X68", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 234 [arrowhead = none , style=dashed];
234 -> 32[style=dashed];

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

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

237 [label="EVAL with clause\napp([], X81, X81).\nand substitution\nT13 -> []\nX81 -> []\nT60 -> []", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 237 [arrowhead = none ];
237 -> 44;

238 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 238 [arrowhead = none ];
238 -> 45;

239 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = white];
43 -> 239 [arrowhead = none ];
239 -> 47;

240 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 240 [arrowhead = none ];
240 -> 46;

241 [label="EVAL with clause\nfront(tree(X91, void, void), .(X91, [])).\nand substitution\nX91 -> T67\nT10 -> tree(T67, void, void)\nX11 -> .(T67, [])\nT11 -> T66\nT65 -> T67", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 241 [arrowhead = none ];
241 -> 50;

242 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 242 [arrowhead = none ];
242 -> 51;

243 [label="EVAL with clause\nfront(tree(X116, X117, X118), X119) :- ','(front(X117, X120), ','(front(X118, X121), app(X120, X121, X119))).\nand substitution\nX116 -> T80\nX117 -> T83\nX118 -> T84\nT10 -> tree(T80, T83, T84)\nX11 -> X122\nX119 -> X122\nT81 -> T83\nT82 -> T84\nT11 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 243 [arrowhead = none ];
243 -> 57;

244 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 244 [arrowhead = none ];
244 -> 58;

245 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
50 -> 245 [arrowhead = none ];
245 -> 52;

246 [label="SPLIT 2\nreplacements:\nX12 -> T68\nT67 -> T69", fontsize=14, style = filled, fillcolor = violet];
50 -> 246 [arrowhead = none ];
246 -> 53;

247 [label="INSTANCE with matching:\nT12 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 247 [arrowhead = none , style=dashed];
247 -> 14[style=dashed];

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

249 [label="BACKTRACK\nfor clause: app([], X, X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
54 -> 249 [arrowhead = none ];
249 -> 55;

250 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = white];
55 -> 250 [arrowhead = none ];
250 -> 56;

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

252 [label="SPLIT 2\nreplacements:\nX120 -> T86\nT84 -> T87\nT85 -> T88", fontsize=14, style = filled, fillcolor = violet];
57 -> 252 [arrowhead = none ];
252 -> 60;

253 [label="INSTANCE with matching:\nT12 -> T83\nX12 -> X120", fontsize=14, style = filled, fillcolor = lightgrey];
59 -> 253 [arrowhead = none , style=dashed];
253 -> 14[style=dashed];

254 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
60 -> 254 [arrowhead = none ];
254 -> 61;

255 [label="SPLIT 2\nreplacements:\nX121 -> T89\nT86 -> T90\nT88 -> T91", fontsize=14, style = filled, fillcolor = violet];
60 -> 255 [arrowhead = none ];
255 -> 62;

256 [label="INSTANCE with matching:\nT12 -> T87\nX12 -> X121", fontsize=14, style = filled, fillcolor = lightgrey];
61 -> 256 [arrowhead = none , style=dashed];
256 -> 14[style=dashed];

257 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
62 -> 257 [arrowhead = none ];
257 -> 63;

258 [label="SPLIT 2\nreplacements:\nX122 -> T94\nT91 -> T95", fontsize=14, style = filled, fillcolor = violet];
62 -> 258 [arrowhead = none ];
258 -> 64;

259 [label="INSTANCE with matching:\nT33 -> T90\nT32 -> T89\nX41 -> X122", fontsize=14, style = filled, fillcolor = lightgrey];
63 -> 259 [arrowhead = none , style=dashed];
259 -> 32[style=dashed];

260 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
64 -> 260 [arrowhead = none ];
260 -> 65;

261 [label="SPLIT 2\nreplacements:\nX12 -> T98\nT94 -> T99", fontsize=14, style = filled, fillcolor = violet];
64 -> 261 [arrowhead = none ];
261 -> 66;

262 [label="INSTANCE with matching:\nT12 -> T95", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 262 [arrowhead = none , style=dashed];
262 -> 14[style=dashed];

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

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 264 [arrowhead = none ];
264 -> 68;

265 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 265 [arrowhead = none ];
265 -> 69;

266 [label="EVAL with clause\napp([], X137, X137).\nand substitution\nT99 -> []\nT98 -> []\nX137 -> []\nT106 -> []", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 266 [arrowhead = none ];
266 -> 70;

267 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 267 [arrowhead = none ];
267 -> 71;

268 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = white];
69 -> 268 [arrowhead = none ];
268 -> 73;

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

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

271 [label="EVAL with clause\nfront(tree(X260, X261, X262), X263) :- ','(front(X261, X264), ','(front(X262, X265), app(X264, X265, X263))).\nand substitution\nX260 -> T215\nX261 -> T219\nX262 -> T220\nT1 -> tree(T215, T219, T220)\nT2 -> T218\nX263 -> T218\nT216 -> T219\nT217 -> T220", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 271 [arrowhead = none ];
271 -> 121;

272 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 272 [arrowhead = none ];
272 -> 122;

273 [label="EVAL with clause\nfront(tree(X150, X151, X152), X153) :- ','(front(X151, X154), ','(front(X152, X155), app(X154, X155, X153))).\nand substitution\nX150 -> T116\nX151 -> T120\nX152 -> T121\nT1 -> tree(T116, T120, T121)\nT111 -> T119\nX153 -> .(T119, [])\nT117 -> T120\nT118 -> T121", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 273 [arrowhead = none ];
273 -> 77;

274 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 274 [arrowhead = none ];
274 -> 78;

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

276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
79 -> 276 [arrowhead = none ];
276 -> 80;

277 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
79 -> 277 [arrowhead = none ];
277 -> 81;

278 [label="EVAL with clause\nfront(void, []).\nand substitution\nT120 -> void\nX154 -> []\nT121 -> T122", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 278 [arrowhead = none ];
278 -> 82;

279 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 279 [arrowhead = none ];
279 -> 83;

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

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

282 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
82 -> 282 [arrowhead = none ];
282 -> 84;

283 [label="SPLIT 2\nreplacements:\nX155 -> T123", fontsize=14, style = filled, fillcolor = violet];
82 -> 283 [arrowhead = none ];
283 -> 85;

284 [label="INSTANCE with matching:\nT12 -> T122\nX12 -> X155", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 284 [arrowhead = none , style=dashed];
284 -> 14[style=dashed];

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

286 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
86 -> 286 [arrowhead = none ];
286 -> 87;

287 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
86 -> 287 [arrowhead = none ];
287 -> 88;

288 [label="EVAL with clause\napp([], X166, X166).\nand substitution\nT123 -> .(T137, [])\nX166 -> .(T137, [])\nT119 -> T137\nT136 -> .(T137, [])", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 288 [arrowhead = none ];
288 -> 89;

289 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 289 [arrowhead = none ];
289 -> 90;

290 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = white];
88 -> 290 [arrowhead = none ];
290 -> 92;

291 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 291 [arrowhead = none ];
291 -> 91;

292 [label="EVAL with clause\nfront(tree(X176, void, void), .(X176, [])).\nand substitution\nX176 -> T144\nT120 -> tree(T144, void, void)\nX154 -> .(T144, [])\nT121 -> T143\nT142 -> T144", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 292 [arrowhead = none ];
292 -> 95;

293 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 293 [arrowhead = none ];
293 -> 96;

294 [label="EVAL with clause\nfront(tree(X215, X216, X217), X218) :- ','(front(X216, X219), ','(front(X217, X220), app(X219, X220, X218))).\nand substitution\nX215 -> T164\nX216 -> T167\nX217 -> T168\nT120 -> tree(T164, T167, T168)\nX154 -> X221\nX218 -> X221\nT165 -> T167\nT166 -> T168\nT121 -> T169", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 294 [arrowhead = none ];
294 -> 103;

295 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 295 [arrowhead = none ];
295 -> 104;

296 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
95 -> 296 [arrowhead = none ];
296 -> 97;

297 [label="SPLIT 2\nreplacements:\nX155 -> T145\nT144 -> T146", fontsize=14, style = filled, fillcolor = violet];
95 -> 297 [arrowhead = none ];
297 -> 98;

298 [label="INSTANCE with matching:\nT12 -> T143\nX12 -> X155", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 298 [arrowhead = none , style=dashed];
298 -> 14[style=dashed];

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

300 [label="BACKTRACK\nfor clause: app([], X, X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
99 -> 300 [arrowhead = none ];
300 -> 100;

301 [label="EVAL with clause\napp(.(X193, X194), X195, .(X193, X196)) :- app(X194, X195, X196).\nand substitution\nT146 -> T153\nX193 -> T153\nX194 -> []\nT145 -> T155\nX195 -> T155\nT119 -> T153\nX196 -> []\nT154 -> T155", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 301 [arrowhead = none ];
301 -> 101;

302 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 302 [arrowhead = none ];
302 -> 102;

303 [label="INSTANCE with matching:\nT13 -> T155", fontsize=14, style = filled, fillcolor = lightgrey];
101 -> 303 [arrowhead = none , style=dashed];
303 -> 15[style=dashed];

304 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
103 -> 304 [arrowhead = none ];
304 -> 105;

305 [label="SPLIT 2\nreplacements:\nX219 -> T170\nT168 -> T171\nT169 -> T172", fontsize=14, style = filled, fillcolor = violet];
103 -> 305 [arrowhead = none ];
305 -> 106;

306 [label="INSTANCE with matching:\nT12 -> T167\nX12 -> X219", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 306 [arrowhead = none , style=dashed];
306 -> 14[style=dashed];

307 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
106 -> 307 [arrowhead = none ];
307 -> 107;

308 [label="SPLIT 2\nreplacements:\nX220 -> T173\nT170 -> T174\nT172 -> T175", fontsize=14, style = filled, fillcolor = violet];
106 -> 308 [arrowhead = none ];
308 -> 108;

309 [label="INSTANCE with matching:\nT12 -> T171\nX12 -> X220", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 309 [arrowhead = none , style=dashed];
309 -> 14[style=dashed];

310 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
108 -> 310 [arrowhead = none ];
310 -> 109;

311 [label="SPLIT 2\nreplacements:\nX221 -> T178\nT175 -> T179", fontsize=14, style = filled, fillcolor = violet];
108 -> 311 [arrowhead = none ];
311 -> 110;

312 [label="INSTANCE with matching:\nT90 -> T174\nT89 -> T173\nX122 -> X221", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 312 [arrowhead = none , style=dashed];
312 -> 63[style=dashed];

313 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
110 -> 313 [arrowhead = none ];
313 -> 111;

314 [label="SPLIT 2\nreplacements:\nX155 -> T182\nT178 -> T183", fontsize=14, style = filled, fillcolor = violet];
110 -> 314 [arrowhead = none ];
314 -> 112;

315 [label="INSTANCE with matching:\nT12 -> T179\nX12 -> X155", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 315 [arrowhead = none , style=dashed];
315 -> 14[style=dashed];

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

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

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

319 [label="EVAL with clause\napp([], X236, X236).\nand substitution\nT183 -> []\nT182 -> .(T197, [])\nX236 -> .(T197, [])\nT119 -> T197\nT196 -> .(T197, [])", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 319 [arrowhead = none ];
319 -> 116;

320 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 320 [arrowhead = none ];
320 -> 117;

321 [label="EVAL with clause\napp(.(X246, X247), X248, .(X246, X249)) :- app(X247, X248, X249).\nand substitution\nX246 -> T204\nX247 -> T207\nT183 -> .(T204, T207)\nT182 -> T208\nX248 -> T208\nT119 -> T204\nX249 -> []\nT205 -> T207\nT206 -> T208", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 321 [arrowhead = none ];
321 -> 119;

322 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 322 [arrowhead = none ];
322 -> 120;

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

324 [label="INSTANCE with matching:\nT99 -> T207\nT98 -> T208", fontsize=14, style = filled, fillcolor = lightgrey];
119 -> 324 [arrowhead = none , style=dashed];
324 -> 66[style=dashed];

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

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

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

328 [label="EVAL with clause\nfront(void, []).\nand substitution\nT219 -> void\nX264 -> []\nT220 -> T221", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 328 [arrowhead = none ];
328 -> 126;

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

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

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

332 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
126 -> 332 [arrowhead = none ];
332 -> 128;

333 [label="SPLIT 2\nreplacements:\nX265 -> T222\nT1 -> T223\nX144 -> T224", fontsize=14, style = filled, fillcolor = violet];
126 -> 333 [arrowhead = none ];
333 -> 129;

334 [label="INSTANCE with matching:\nT12 -> T221\nX12 -> X265", fontsize=14, style = filled, fillcolor = lightgrey];
128 -> 334 [arrowhead = none , style=dashed];
334 -> 14[style=dashed];

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

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

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

338 [label="EVAL with clause\napp([], X276, X276).\nand substitution\nT222 -> T231\nX276 -> T231\nT218 -> T231", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 338 [arrowhead = none ];
338 -> 133;

339 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 339 [arrowhead = none ];
339 -> 134;

340 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = white];
132 -> 340 [arrowhead = none ];
340 -> 136;

341 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 341 [arrowhead = none ];
341 -> 135;

342 [label="EVAL with clause\nfront(tree(X286, void, void), .(X286, [])).\nand substitution\nX286 -> T238\nT219 -> tree(T238, void, void)\nX264 -> .(T238, [])\nT220 -> T237\nT236 -> T238", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 342 [arrowhead = none ];
342 -> 139;

343 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 343 [arrowhead = none ];
343 -> 140;

344 [label="EVAL with clause\nfront(tree(X335, X336, X337), X338) :- ','(front(X336, X339), ','(front(X337, X340), app(X339, X340, X338))).\nand substitution\nX335 -> T269\nX336 -> T272\nX337 -> T273\nT219 -> tree(T269, T272, T273)\nX264 -> X341\nX338 -> X341\nT270 -> T272\nT271 -> T273\nT220 -> T274", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 344 [arrowhead = none ];
344 -> 154;

345 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 345 [arrowhead = none ];
345 -> 155;

346 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
139 -> 346 [arrowhead = none ];
346 -> 141;

347 [label="SPLIT 2\nreplacements:\nX265 -> T239\nT238 -> T240\nT1 -> T241\nX144 -> T242", fontsize=14, style = filled, fillcolor = violet];
139 -> 347 [arrowhead = none ];
347 -> 142;

348 [label="INSTANCE with matching:\nT221 -> T237", fontsize=14, style = filled, fillcolor = lightgrey];
141 -> 348 [arrowhead = none , style=dashed];
348 -> 128[style=dashed];

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

350 [label="BACKTRACK\nfor clause: app([], X, X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
143 -> 350 [arrowhead = none ];
350 -> 144;

351 [label="EVAL with clause\napp(.(X303, X304), X305, .(X303, X306)) :- app(X304, X305, X306).\nand substitution\nT240 -> T252\nX303 -> T252\nX304 -> []\nT239 -> T255\nX305 -> T255\nX306 -> T254\nT218 -> .(T252, T254)\nT253 -> T255", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 351 [arrowhead = none ];
351 -> 145;

352 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 352 [arrowhead = none ];
352 -> 146;

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

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

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

356 [label="EVAL with clause\napp([], X317, X317).\nand substitution\nT255 -> T262\nX317 -> T262\nT254 -> T262", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 356 [arrowhead = none ];
356 -> 150;

357 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 357 [arrowhead = none ];
357 -> 151;

358 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = white];
149 -> 358 [arrowhead = none ];
358 -> 153;

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

360 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
154 -> 360 [arrowhead = none ];
360 -> 156;

361 [label="SPLIT 2\nreplacements:\nX339 -> T275\nT273 -> T276\nT274 -> T277\nT1 -> T278\nX144 -> T279", fontsize=14, style = filled, fillcolor = violet];
154 -> 361 [arrowhead = none ];
361 -> 157;

362 [label="INSTANCE with matching:\nT221 -> T272\nX265 -> X339", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 362 [arrowhead = none , style=dashed];
362 -> 128[style=dashed];

363 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
157 -> 363 [arrowhead = none ];
363 -> 158;

364 [label="SPLIT 2\nreplacements:\nX340 -> T280\nT275 -> T281\nT277 -> T282\nT278 -> T283\nT279 -> T284", fontsize=14, style = filled, fillcolor = violet];
157 -> 364 [arrowhead = none ];
364 -> 159;

365 [label="INSTANCE with matching:\nT221 -> T276\nX265 -> X340", fontsize=14, style = filled, fillcolor = lightgrey];
158 -> 365 [arrowhead = none , style=dashed];
365 -> 128[style=dashed];

366 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
159 -> 366 [arrowhead = none ];
366 -> 160;

367 [label="SPLIT 2\nreplacements:\nX341 -> T287\nT282 -> T288\nT283 -> T289\nT284 -> T290", fontsize=14, style = filled, fillcolor = violet];
159 -> 367 [arrowhead = none ];
367 -> 161;

368 [label="INSTANCE with matching:\nT90 -> T281\nT89 -> T280\nX122 -> X341", fontsize=14, style = filled, fillcolor = lightgrey];
160 -> 368 [arrowhead = none , style=dashed];
368 -> 63[style=dashed];

369 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
161 -> 369 [arrowhead = none ];
369 -> 162;

370 [label="SPLIT 2\nreplacements:\nX265 -> T293\nT287 -> T294\nT289 -> T295\nT290 -> T296", fontsize=14, style = filled, fillcolor = violet];
161 -> 370 [arrowhead = none ];
370 -> 163;

371 [label="INSTANCE with matching:\nT221 -> T288", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 371 [arrowhead = none , style=dashed];
371 -> 128[style=dashed];

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

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

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

375 [label="EVAL with clause\napp([], X356, X356).\nand substitution\nT294 -> []\nT293 -> T303\nX356 -> T303\nT218 -> T303", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 375 [arrowhead = none ];
375 -> 167;

376 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 376 [arrowhead = none ];
376 -> 168;

377 [label="EVAL with clause\napp(.(X366, X367), X368, .(X366, X369)) :- app(X367, X368, X369).\nand substitution\nX366 -> T312\nX367 -> T316\nT294 -> .(T312, T316)\nT293 -> T317\nX368 -> T317\nX369 -> T315\nT218 -> .(T312, T315)\nT313 -> T316\nT314 -> T317", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 377 [arrowhead = none ];
377 -> 170;

378 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 378 [arrowhead = none ];
378 -> 171;

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

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

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

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

383 [label="EVAL with clause\napp([], X380, X380).\nand substitution\nT316 -> []\nT317 -> T324\nX380 -> T324\nT315 -> T324", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 383 [arrowhead = none ];
383 -> 175;

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

385 [label="EVAL with clause\napp(.(X390, X391), X392, .(X390, X393)) :- app(X391, X392, X393).\nand substitution\nX390 -> T333\nX391 -> T337\nT316 -> .(T333, T337)\nT317 -> T338\nX392 -> T338\nX393 -> T336\nT315 -> .(T333, T336)\nT334 -> T337\nT335 -> T338", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 385 [arrowhead = none ];
385 -> 178;

386 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 386 [arrowhead = none ];
386 -> 179;

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

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

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

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

391 [label="EVAL with clause\napp([], X404, X404).\nand substitution\nT337 -> []\nT338 -> T345\nX404 -> T345\nT336 -> T345", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 391 [arrowhead = none ];
391 -> 183;

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

393 [label="EVAL with clause\napp(.(X414, X415), X416, .(X414, X417)) :- app(X415, X416, X417).\nand substitution\nX414 -> T354\nX415 -> T358\nT337 -> .(T354, T358)\nT338 -> T359\nX416 -> T359\nX417 -> T357\nT336 -> .(T354, T357)\nT355 -> T358\nT356 -> T359", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 393 [arrowhead = none ];
393 -> 186;

394 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 394 [arrowhead = none ];
394 -> 187;

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

396 [label="INSTANCE with matching:\nT337 -> T358\nT338 -> T359\nT336 -> T357", fontsize=14, style = filled, fillcolor = lightgrey];
186 -> 396 [arrowhead = none , style=dashed];
396 -> 178[style=dashed];

}

(2) Obligation:

Triples:

front14(tree(T25, T28, T29), X41) :- front14(T28, X39).
front14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T30), front14(T31, X40)).
front14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T33), ','(frontc14(T31, T32), app32(T33, T32, X41))).
app32(.(T47, T50), T51, .(T47, X68)) :- app32(T50, T51, X68).
app178(.(T354, T358), T359, .(T354, T357)) :- app178(T358, T359, T357).
front1(tree(T7, void, T12), []) :- front14(T12, X12).
front1(tree(T7, void, T12), []) :- ','(frontc14(T12, T13), app15(T13)).
front1(tree(T7, tree(T67, void, void), T66), []) :- front14(T66, X12).
front1(tree(T7, tree(T80, T83, T84), T85), []) :- front14(T83, X120).
front1(tree(T7, tree(T80, T83, T87), T88), []) :- ','(frontc14(T83, T86), front14(T87, X121)).
front1(tree(T7, tree(T80, T83, T87), T91), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), app32(T90, T89, X122))).
front1(tree(T7, tree(T80, T83, T87), T95), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), ','(appc32(T90, T89, T94), front14(T95, X12)))).
front1(tree(T7, tree(T80, T83, T87), T95), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), ','(appc32(T90, T89, T99), ','(frontc14(T95, T98), app66(T99, T98))))).
front1(tree(T116, void, T122), .(T119, [])) :- front14(T122, X155).
front1(tree(T116, tree(T144, void, void), T143), .(T119, [])) :- front14(T143, X155).
front1(tree(T116, tree(T153, void, void), T143), .(T153, [])) :- ','(frontc14(T143, T155), app15(T155)).
front1(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) :- front14(T167, X219).
front1(tree(T116, tree(T164, T167, T171), T172), .(T119, [])) :- ','(frontc14(T167, T170), front14(T171, X220)).
front1(tree(T116, tree(T164, T167, T171), T175), .(T119, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), app32(T174, T173, X221))).
front1(tree(T116, tree(T164, T167, T171), T179), .(T119, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), ','(appc32(T174, T173, T178), front14(T179, X155)))).
front1(tree(T116, tree(T164, T167, T171), T179), .(T204, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), ','(appc32(T174, T173, .(T204, T207)), ','(frontc14(T179, T208), app66(T207, T208))))).
front1(tree(T215, void, T221), T218) :- front14(T221, X265).
front1(tree(T215, tree(T238, void, void), T237), T218) :- front14(T237, X265).
front1(tree(T215, tree(T269, T272, T273), T274), T218) :- front14(T272, X339).
front1(tree(T215, tree(T269, T272, T276), T277), T218) :- ','(frontc14(T272, T275), front14(T276, X340)).
front1(tree(T215, tree(T269, T272, T276), T282), T218) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), app32(T281, T280, X341))).
front1(tree(T215, tree(T269, T272, T276), T288), T218) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), ','(appc32(T281, T280, T287), front14(T288, X265)))).
front1(tree(T215, tree(T269, T272, T276), T288), .(T312, .(T333, T336))) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), ','(appc32(T281, T280, .(T312, .(T333, T337))), ','(frontc14(T288, T338), app178(T337, T338, T336))))).

Clauses:

frontc14(void, []).
frontc14(tree(T18, void, void), .(T18, [])).
frontc14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T33), ','(frontc14(T31, T32), appc32(T33, T32, X41))).
appc32([], T40, T40).
appc32(.(T47, T50), T51, .(T47, X68)) :- appc32(T50, T51, X68).
appc15([]).
appc66([], []).
appc178([], T345, T345).
appc178(.(T354, T358), T359, .(T354, T357)) :- appc178(T358, T359, T357).

Afs:

front1(x1, x2)  =  front1(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

front14(tree(T25, T28, T29), X41) :- front14(T28, X39).
front14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T30), front14(T31, X40)).
front14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T33), ','(frontc14(T31, T32), app32(T33, T32, X41))).
app32(.(T47, T50), T51, .(T47, X68)) :- app32(T50, T51, X68).
app178(.(T354, T358), T359, .(T354, T357)) :- app178(T358, T359, T357).
front1(tree(T7, void, T12), []) :- front14(T12, X12).
front1(tree(T7, tree(T67, void, void), T66), []) :- front14(T66, X12).
front1(tree(T7, tree(T80, T83, T84), T85), []) :- front14(T83, X120).
front1(tree(T7, tree(T80, T83, T87), T88), []) :- ','(frontc14(T83, T86), front14(T87, X121)).
front1(tree(T7, tree(T80, T83, T87), T91), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), app32(T90, T89, X122))).
front1(tree(T7, tree(T80, T83, T87), T95), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), ','(appc32(T90, T89, T94), front14(T95, X12)))).
front1(tree(T116, void, T122), .(T119, [])) :- front14(T122, X155).
front1(tree(T116, tree(T144, void, void), T143), .(T119, [])) :- front14(T143, X155).
front1(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) :- front14(T167, X219).
front1(tree(T116, tree(T164, T167, T171), T172), .(T119, [])) :- ','(frontc14(T167, T170), front14(T171, X220)).
front1(tree(T116, tree(T164, T167, T171), T175), .(T119, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), app32(T174, T173, X221))).
front1(tree(T116, tree(T164, T167, T171), T179), .(T119, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), ','(appc32(T174, T173, T178), front14(T179, X155)))).
front1(tree(T215, void, T221), T218) :- front14(T221, X265).
front1(tree(T215, tree(T238, void, void), T237), T218) :- front14(T237, X265).
front1(tree(T215, tree(T269, T272, T273), T274), T218) :- front14(T272, X339).
front1(tree(T215, tree(T269, T272, T276), T277), T218) :- ','(frontc14(T272, T275), front14(T276, X340)).
front1(tree(T215, tree(T269, T272, T276), T282), T218) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), app32(T281, T280, X341))).
front1(tree(T215, tree(T269, T272, T276), T288), T218) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), ','(appc32(T281, T280, T287), front14(T288, X265)))).
front1(tree(T215, tree(T269, T272, T276), T288), .(T312, .(T333, T336))) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), ','(appc32(T281, T280, .(T312, .(T333, T337))), ','(frontc14(T288, T338), app178(T337, T338, T336))))).

Clauses:

frontc14(void, []).
frontc14(tree(T18, void, void), .(T18, [])).
frontc14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T33), ','(frontc14(T31, T32), appc32(T33, T32, X41))).
appc32([], T40, T40).
appc32(.(T47, T50), T51, .(T47, X68)) :- appc32(T50, T51, X68).
appc15([]).
appc66([], []).
appc178([], T345, T345).
appc178(.(T354, T358), T359, .(T354, T357)) :- appc178(T358, T359, T357).

Afs:

front1(x1, x2)  =  front1(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
front1_in: (f,b)
front14_in: (f,f)
frontc14_in: (f,f)
appc32_in: (b,b,f)
app32_in: (b,b,f)
app178_in: (b,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FRONT1_IN_AG(tree(T7, void, T12), []) → U9_AG(T7, T12, front14_in_aa(T12, X12))
FRONT1_IN_AG(tree(T7, void, T12), []) → FRONT14_IN_AA(T12, X12)
FRONT14_IN_AA(tree(T25, T28, T29), X41) → U1_AA(T25, T28, T29, X41, front14_in_aa(T28, X39))
FRONT14_IN_AA(tree(T25, T28, T29), X41) → FRONT14_IN_AA(T28, X39)
FRONT14_IN_AA(tree(T25, T28, T31), X41) → U2_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T30))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → U3_AA(T25, T28, T31, X41, front14_in_aa(T31, X40))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → FRONT14_IN_AA(T31, X40)
FRONT14_IN_AA(tree(T25, T28, T31), X41) → U4_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U4_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U5_AA(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U5_AA(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U6_AA(T25, T28, T31, X41, app32_in_gga(T33, T32, X41))
U5_AA(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → APP32_IN_GGA(T33, T32, X41)
APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → U7_GGA(T47, T50, T51, X68, app32_in_gga(T50, T51, X68))
APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → APP32_IN_GGA(T50, T51, X68)
FRONT1_IN_AG(tree(T7, tree(T67, void, void), T66), []) → U10_AG(T7, T67, T66, front14_in_aa(T66, X12))
FRONT1_IN_AG(tree(T7, tree(T67, void, void), T66), []) → FRONT14_IN_AA(T66, X12)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T84), T85), []) → U11_AG(T7, T80, T83, T84, T85, front14_in_aa(T83, X120))
FRONT1_IN_AG(tree(T7, tree(T80, T83, T84), T85), []) → FRONT14_IN_AA(T83, X120)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T88), []) → U12_AG(T7, T80, T83, T87, T88, frontc14_in_aa(T83, T86))
U12_AG(T7, T80, T83, T87, T88, frontc14_out_aa(T83, T86)) → U13_AG(T7, T80, T83, T87, T88, front14_in_aa(T87, X121))
U12_AG(T7, T80, T83, T87, T88, frontc14_out_aa(T83, T86)) → FRONT14_IN_AA(T87, X121)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T91), []) → U14_AG(T7, T80, T83, T87, T91, frontc14_in_aa(T83, T90))
U14_AG(T7, T80, T83, T87, T91, frontc14_out_aa(T83, T90)) → U15_AG(T7, T80, T83, T87, T91, T90, frontc14_in_aa(T87, T89))
U15_AG(T7, T80, T83, T87, T91, T90, frontc14_out_aa(T87, T89)) → U16_AG(T7, T80, T83, T87, T91, app32_in_gga(T90, T89, X122))
U15_AG(T7, T80, T83, T87, T91, T90, frontc14_out_aa(T87, T89)) → APP32_IN_GGA(T90, T89, X122)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T95), []) → U17_AG(T7, T80, T83, T87, T95, frontc14_in_aa(T83, T90))
U17_AG(T7, T80, T83, T87, T95, frontc14_out_aa(T83, T90)) → U18_AG(T7, T80, T83, T87, T95, T90, frontc14_in_aa(T87, T89))
U18_AG(T7, T80, T83, T87, T95, T90, frontc14_out_aa(T87, T89)) → U19_AG(T7, T80, T83, T87, T95, appc32_in_gga(T90, T89, T94))
U19_AG(T7, T80, T83, T87, T95, appc32_out_gga(T90, T89, T94)) → U20_AG(T7, T80, T83, T87, T95, front14_in_aa(T95, X12))
U19_AG(T7, T80, T83, T87, T95, appc32_out_gga(T90, T89, T94)) → FRONT14_IN_AA(T95, X12)
FRONT1_IN_AG(tree(T116, void, T122), .(T119, [])) → U21_AG(T116, T122, T119, front14_in_aa(T122, X155))
FRONT1_IN_AG(tree(T116, void, T122), .(T119, [])) → FRONT14_IN_AA(T122, X155)
FRONT1_IN_AG(tree(T116, tree(T144, void, void), T143), .(T119, [])) → U22_AG(T116, T144, T143, T119, front14_in_aa(T143, X155))
FRONT1_IN_AG(tree(T116, tree(T144, void, void), T143), .(T119, [])) → FRONT14_IN_AA(T143, X155)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) → U23_AG(T116, T164, T167, T168, T169, T119, front14_in_aa(T167, X219))
FRONT1_IN_AG(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) → FRONT14_IN_AA(T167, X219)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T172), .(T119, [])) → U24_AG(T116, T164, T167, T171, T172, T119, frontc14_in_aa(T167, T170))
U24_AG(T116, T164, T167, T171, T172, T119, frontc14_out_aa(T167, T170)) → U25_AG(T116, T164, T167, T171, T172, T119, front14_in_aa(T171, X220))
U24_AG(T116, T164, T167, T171, T172, T119, frontc14_out_aa(T167, T170)) → FRONT14_IN_AA(T171, X220)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T175), .(T119, [])) → U26_AG(T116, T164, T167, T171, T175, T119, frontc14_in_aa(T167, T174))
U26_AG(T116, T164, T167, T171, T175, T119, frontc14_out_aa(T167, T174)) → U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_in_aa(T171, T173))
U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_out_aa(T171, T173)) → U28_AG(T116, T164, T167, T171, T175, T119, app32_in_gga(T174, T173, X221))
U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_out_aa(T171, T173)) → APP32_IN_GGA(T174, T173, X221)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T179), .(T119, [])) → U29_AG(T116, T164, T167, T171, T179, T119, frontc14_in_aa(T167, T174))
U29_AG(T116, T164, T167, T171, T179, T119, frontc14_out_aa(T167, T174)) → U30_AG(T116, T164, T167, T171, T179, T119, T174, frontc14_in_aa(T171, T173))
U30_AG(T116, T164, T167, T171, T179, T119, T174, frontc14_out_aa(T171, T173)) → U31_AG(T116, T164, T167, T171, T179, T119, appc32_in_gga(T174, T173, T178))
U31_AG(T116, T164, T167, T171, T179, T119, appc32_out_gga(T174, T173, T178)) → U32_AG(T116, T164, T167, T171, T179, T119, front14_in_aa(T179, X155))
U31_AG(T116, T164, T167, T171, T179, T119, appc32_out_gga(T174, T173, T178)) → FRONT14_IN_AA(T179, X155)
FRONT1_IN_AG(tree(T215, void, T221), T218) → U33_AG(T215, T221, T218, front14_in_aa(T221, X265))
FRONT1_IN_AG(tree(T215, void, T221), T218) → FRONT14_IN_AA(T221, X265)
FRONT1_IN_AG(tree(T215, tree(T238, void, void), T237), T218) → U34_AG(T215, T238, T237, T218, front14_in_aa(T237, X265))
FRONT1_IN_AG(tree(T215, tree(T238, void, void), T237), T218) → FRONT14_IN_AA(T237, X265)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T273), T274), T218) → U35_AG(T215, T269, T272, T273, T274, T218, front14_in_aa(T272, X339))
FRONT1_IN_AG(tree(T215, tree(T269, T272, T273), T274), T218) → FRONT14_IN_AA(T272, X339)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T277), T218) → U36_AG(T215, T269, T272, T276, T277, T218, frontc14_in_aa(T272, T275))
U36_AG(T215, T269, T272, T276, T277, T218, frontc14_out_aa(T272, T275)) → U37_AG(T215, T269, T272, T276, T277, T218, front14_in_aa(T276, X340))
U36_AG(T215, T269, T272, T276, T277, T218, frontc14_out_aa(T272, T275)) → FRONT14_IN_AA(T276, X340)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T282), T218) → U38_AG(T215, T269, T272, T276, T282, T218, frontc14_in_aa(T272, T281))
U38_AG(T215, T269, T272, T276, T282, T218, frontc14_out_aa(T272, T281)) → U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_in_aa(T276, T280))
U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_out_aa(T276, T280)) → U40_AG(T215, T269, T272, T276, T282, T218, app32_in_gga(T281, T280, X341))
U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_out_aa(T276, T280)) → APP32_IN_GGA(T281, T280, X341)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T288), T218) → U41_AG(T215, T269, T272, T276, T288, T218, frontc14_in_aa(T272, T281))
U41_AG(T215, T269, T272, T276, T288, T218, frontc14_out_aa(T272, T281)) → U42_AG(T215, T269, T272, T276, T288, T218, T281, frontc14_in_aa(T276, T280))
U42_AG(T215, T269, T272, T276, T288, T218, T281, frontc14_out_aa(T276, T280)) → U43_AG(T215, T269, T272, T276, T288, T218, appc32_in_gga(T281, T280, T287))
U43_AG(T215, T269, T272, T276, T288, T218, appc32_out_gga(T281, T280, T287)) → U44_AG(T215, T269, T272, T276, T288, T218, front14_in_aa(T288, X265))
U43_AG(T215, T269, T272, T276, T288, T218, appc32_out_gga(T281, T280, T287)) → FRONT14_IN_AA(T288, X265)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T288), .(T312, .(T333, T336))) → U45_AG(T215, T269, T272, T276, T288, T312, T333, T336, frontc14_in_aa(T272, T281))
U45_AG(T215, T269, T272, T276, T288, T312, T333, T336, frontc14_out_aa(T272, T281)) → U46_AG(T215, T269, T272, T276, T288, T312, T333, T336, T281, frontc14_in_aa(T276, T280))
U46_AG(T215, T269, T272, T276, T288, T312, T333, T336, T281, frontc14_out_aa(T276, T280)) → U47_AG(T215, T269, T272, T276, T288, T312, T333, T336, appc32_in_gga(T281, T280, .(T312, .(T333, T337))))
U47_AG(T215, T269, T272, T276, T288, T312, T333, T336, appc32_out_gga(T281, T280, .(T312, .(T333, T337)))) → U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_in_aa(T288, T338))
U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_out_aa(T288, T338)) → U49_AG(T215, T269, T272, T276, T288, T312, T333, T336, app178_in_ggg(T337, T338, T336))
U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_out_aa(T288, T338)) → APP178_IN_GGG(T337, T338, T336)
APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → U8_GGG(T354, T358, T359, T357, app178_in_ggg(T358, T359, T357))
APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → APP178_IN_GGG(T358, T359, T357)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
front14_in_aa(x1, x2)  =  front14_in_aa
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
app32_in_gga(x1, x2, x3)  =  app32_in_gga(x1, x2)
app178_in_ggg(x1, x2, x3)  =  app178_in_ggg(x1, x2, x3)
FRONT1_IN_AG(x1, x2)  =  FRONT1_IN_AG(x2)
U9_AG(x1, x2, x3)  =  U9_AG(x3)
FRONT14_IN_AA(x1, x2)  =  FRONT14_IN_AA
U1_AA(x1, x2, x3, x4, x5)  =  U1_AA(x5)
U2_AA(x1, x2, x3, x4, x5)  =  U2_AA(x5)
U3_AA(x1, x2, x3, x4, x5)  =  U3_AA(x5)
U4_AA(x1, x2, x3, x4, x5)  =  U4_AA(x5)
U5_AA(x1, x2, x3, x4, x5, x6)  =  U5_AA(x5, x6)
U6_AA(x1, x2, x3, x4, x5)  =  U6_AA(x5)
APP32_IN_GGA(x1, x2, x3)  =  APP32_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4, x5)  =  U7_GGA(x2, x3, x5)
U10_AG(x1, x2, x3, x4)  =  U10_AG(x4)
U11_AG(x1, x2, x3, x4, x5, x6)  =  U11_AG(x6)
U12_AG(x1, x2, x3, x4, x5, x6)  =  U12_AG(x6)
U13_AG(x1, x2, x3, x4, x5, x6)  =  U13_AG(x6)
U14_AG(x1, x2, x3, x4, x5, x6)  =  U14_AG(x6)
U15_AG(x1, x2, x3, x4, x5, x6, x7)  =  U15_AG(x6, x7)
U16_AG(x1, x2, x3, x4, x5, x6)  =  U16_AG(x6)
U17_AG(x1, x2, x3, x4, x5, x6)  =  U17_AG(x6)
U18_AG(x1, x2, x3, x4, x5, x6, x7)  =  U18_AG(x6, x7)
U19_AG(x1, x2, x3, x4, x5, x6)  =  U19_AG(x6)
U20_AG(x1, x2, x3, x4, x5, x6)  =  U20_AG(x6)
U21_AG(x1, x2, x3, x4)  =  U21_AG(x4)
U22_AG(x1, x2, x3, x4, x5)  =  U22_AG(x5)
U23_AG(x1, x2, x3, x4, x5, x6, x7)  =  U23_AG(x7)
U24_AG(x1, x2, x3, x4, x5, x6, x7)  =  U24_AG(x7)
U25_AG(x1, x2, x3, x4, x5, x6, x7)  =  U25_AG(x7)
U26_AG(x1, x2, x3, x4, x5, x6, x7)  =  U26_AG(x7)
U27_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_AG(x7, x8)
U28_AG(x1, x2, x3, x4, x5, x6, x7)  =  U28_AG(x7)
U29_AG(x1, x2, x3, x4, x5, x6, x7)  =  U29_AG(x7)
U30_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U30_AG(x7, x8)
U31_AG(x1, x2, x3, x4, x5, x6, x7)  =  U31_AG(x7)
U32_AG(x1, x2, x3, x4, x5, x6, x7)  =  U32_AG(x7)
U33_AG(x1, x2, x3, x4)  =  U33_AG(x3, x4)
U34_AG(x1, x2, x3, x4, x5)  =  U34_AG(x4, x5)
U35_AG(x1, x2, x3, x4, x5, x6, x7)  =  U35_AG(x6, x7)
U36_AG(x1, x2, x3, x4, x5, x6, x7)  =  U36_AG(x6, x7)
U37_AG(x1, x2, x3, x4, x5, x6, x7)  =  U37_AG(x6, x7)
U38_AG(x1, x2, x3, x4, x5, x6, x7)  =  U38_AG(x6, x7)
U39_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_AG(x6, x7, x8)
U40_AG(x1, x2, x3, x4, x5, x6, x7)  =  U40_AG(x6, x7)
U41_AG(x1, x2, x3, x4, x5, x6, x7)  =  U41_AG(x6, x7)
U42_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_AG(x6, x7, x8)
U43_AG(x1, x2, x3, x4, x5, x6, x7)  =  U43_AG(x6, x7)
U44_AG(x1, x2, x3, x4, x5, x6, x7)  =  U44_AG(x6, x7)
U45_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U45_AG(x8, x9)
U46_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U46_AG(x8, x9, x10)
U47_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_AG(x8, x9)
U48_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U48_AG(x8, x9, x10)
U49_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_AG(x8, x9)
APP178_IN_GGG(x1, x2, x3)  =  APP178_IN_GGG(x1, x2, x3)
U8_GGG(x1, x2, x3, x4, x5)  =  U8_GGG(x2, x3, x4, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

FRONT1_IN_AG(tree(T7, void, T12), []) → U9_AG(T7, T12, front14_in_aa(T12, X12))
FRONT1_IN_AG(tree(T7, void, T12), []) → FRONT14_IN_AA(T12, X12)
FRONT14_IN_AA(tree(T25, T28, T29), X41) → U1_AA(T25, T28, T29, X41, front14_in_aa(T28, X39))
FRONT14_IN_AA(tree(T25, T28, T29), X41) → FRONT14_IN_AA(T28, X39)
FRONT14_IN_AA(tree(T25, T28, T31), X41) → U2_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T30))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → U3_AA(T25, T28, T31, X41, front14_in_aa(T31, X40))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → FRONT14_IN_AA(T31, X40)
FRONT14_IN_AA(tree(T25, T28, T31), X41) → U4_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U4_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U5_AA(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U5_AA(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U6_AA(T25, T28, T31, X41, app32_in_gga(T33, T32, X41))
U5_AA(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → APP32_IN_GGA(T33, T32, X41)
APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → U7_GGA(T47, T50, T51, X68, app32_in_gga(T50, T51, X68))
APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → APP32_IN_GGA(T50, T51, X68)
FRONT1_IN_AG(tree(T7, tree(T67, void, void), T66), []) → U10_AG(T7, T67, T66, front14_in_aa(T66, X12))
FRONT1_IN_AG(tree(T7, tree(T67, void, void), T66), []) → FRONT14_IN_AA(T66, X12)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T84), T85), []) → U11_AG(T7, T80, T83, T84, T85, front14_in_aa(T83, X120))
FRONT1_IN_AG(tree(T7, tree(T80, T83, T84), T85), []) → FRONT14_IN_AA(T83, X120)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T88), []) → U12_AG(T7, T80, T83, T87, T88, frontc14_in_aa(T83, T86))
U12_AG(T7, T80, T83, T87, T88, frontc14_out_aa(T83, T86)) → U13_AG(T7, T80, T83, T87, T88, front14_in_aa(T87, X121))
U12_AG(T7, T80, T83, T87, T88, frontc14_out_aa(T83, T86)) → FRONT14_IN_AA(T87, X121)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T91), []) → U14_AG(T7, T80, T83, T87, T91, frontc14_in_aa(T83, T90))
U14_AG(T7, T80, T83, T87, T91, frontc14_out_aa(T83, T90)) → U15_AG(T7, T80, T83, T87, T91, T90, frontc14_in_aa(T87, T89))
U15_AG(T7, T80, T83, T87, T91, T90, frontc14_out_aa(T87, T89)) → U16_AG(T7, T80, T83, T87, T91, app32_in_gga(T90, T89, X122))
U15_AG(T7, T80, T83, T87, T91, T90, frontc14_out_aa(T87, T89)) → APP32_IN_GGA(T90, T89, X122)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T95), []) → U17_AG(T7, T80, T83, T87, T95, frontc14_in_aa(T83, T90))
U17_AG(T7, T80, T83, T87, T95, frontc14_out_aa(T83, T90)) → U18_AG(T7, T80, T83, T87, T95, T90, frontc14_in_aa(T87, T89))
U18_AG(T7, T80, T83, T87, T95, T90, frontc14_out_aa(T87, T89)) → U19_AG(T7, T80, T83, T87, T95, appc32_in_gga(T90, T89, T94))
U19_AG(T7, T80, T83, T87, T95, appc32_out_gga(T90, T89, T94)) → U20_AG(T7, T80, T83, T87, T95, front14_in_aa(T95, X12))
U19_AG(T7, T80, T83, T87, T95, appc32_out_gga(T90, T89, T94)) → FRONT14_IN_AA(T95, X12)
FRONT1_IN_AG(tree(T116, void, T122), .(T119, [])) → U21_AG(T116, T122, T119, front14_in_aa(T122, X155))
FRONT1_IN_AG(tree(T116, void, T122), .(T119, [])) → FRONT14_IN_AA(T122, X155)
FRONT1_IN_AG(tree(T116, tree(T144, void, void), T143), .(T119, [])) → U22_AG(T116, T144, T143, T119, front14_in_aa(T143, X155))
FRONT1_IN_AG(tree(T116, tree(T144, void, void), T143), .(T119, [])) → FRONT14_IN_AA(T143, X155)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) → U23_AG(T116, T164, T167, T168, T169, T119, front14_in_aa(T167, X219))
FRONT1_IN_AG(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) → FRONT14_IN_AA(T167, X219)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T172), .(T119, [])) → U24_AG(T116, T164, T167, T171, T172, T119, frontc14_in_aa(T167, T170))
U24_AG(T116, T164, T167, T171, T172, T119, frontc14_out_aa(T167, T170)) → U25_AG(T116, T164, T167, T171, T172, T119, front14_in_aa(T171, X220))
U24_AG(T116, T164, T167, T171, T172, T119, frontc14_out_aa(T167, T170)) → FRONT14_IN_AA(T171, X220)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T175), .(T119, [])) → U26_AG(T116, T164, T167, T171, T175, T119, frontc14_in_aa(T167, T174))
U26_AG(T116, T164, T167, T171, T175, T119, frontc14_out_aa(T167, T174)) → U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_in_aa(T171, T173))
U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_out_aa(T171, T173)) → U28_AG(T116, T164, T167, T171, T175, T119, app32_in_gga(T174, T173, X221))
U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_out_aa(T171, T173)) → APP32_IN_GGA(T174, T173, X221)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T179), .(T119, [])) → U29_AG(T116, T164, T167, T171, T179, T119, frontc14_in_aa(T167, T174))
U29_AG(T116, T164, T167, T171, T179, T119, frontc14_out_aa(T167, T174)) → U30_AG(T116, T164, T167, T171, T179, T119, T174, frontc14_in_aa(T171, T173))
U30_AG(T116, T164, T167, T171, T179, T119, T174, frontc14_out_aa(T171, T173)) → U31_AG(T116, T164, T167, T171, T179, T119, appc32_in_gga(T174, T173, T178))
U31_AG(T116, T164, T167, T171, T179, T119, appc32_out_gga(T174, T173, T178)) → U32_AG(T116, T164, T167, T171, T179, T119, front14_in_aa(T179, X155))
U31_AG(T116, T164, T167, T171, T179, T119, appc32_out_gga(T174, T173, T178)) → FRONT14_IN_AA(T179, X155)
FRONT1_IN_AG(tree(T215, void, T221), T218) → U33_AG(T215, T221, T218, front14_in_aa(T221, X265))
FRONT1_IN_AG(tree(T215, void, T221), T218) → FRONT14_IN_AA(T221, X265)
FRONT1_IN_AG(tree(T215, tree(T238, void, void), T237), T218) → U34_AG(T215, T238, T237, T218, front14_in_aa(T237, X265))
FRONT1_IN_AG(tree(T215, tree(T238, void, void), T237), T218) → FRONT14_IN_AA(T237, X265)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T273), T274), T218) → U35_AG(T215, T269, T272, T273, T274, T218, front14_in_aa(T272, X339))
FRONT1_IN_AG(tree(T215, tree(T269, T272, T273), T274), T218) → FRONT14_IN_AA(T272, X339)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T277), T218) → U36_AG(T215, T269, T272, T276, T277, T218, frontc14_in_aa(T272, T275))
U36_AG(T215, T269, T272, T276, T277, T218, frontc14_out_aa(T272, T275)) → U37_AG(T215, T269, T272, T276, T277, T218, front14_in_aa(T276, X340))
U36_AG(T215, T269, T272, T276, T277, T218, frontc14_out_aa(T272, T275)) → FRONT14_IN_AA(T276, X340)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T282), T218) → U38_AG(T215, T269, T272, T276, T282, T218, frontc14_in_aa(T272, T281))
U38_AG(T215, T269, T272, T276, T282, T218, frontc14_out_aa(T272, T281)) → U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_in_aa(T276, T280))
U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_out_aa(T276, T280)) → U40_AG(T215, T269, T272, T276, T282, T218, app32_in_gga(T281, T280, X341))
U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_out_aa(T276, T280)) → APP32_IN_GGA(T281, T280, X341)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T288), T218) → U41_AG(T215, T269, T272, T276, T288, T218, frontc14_in_aa(T272, T281))
U41_AG(T215, T269, T272, T276, T288, T218, frontc14_out_aa(T272, T281)) → U42_AG(T215, T269, T272, T276, T288, T218, T281, frontc14_in_aa(T276, T280))
U42_AG(T215, T269, T272, T276, T288, T218, T281, frontc14_out_aa(T276, T280)) → U43_AG(T215, T269, T272, T276, T288, T218, appc32_in_gga(T281, T280, T287))
U43_AG(T215, T269, T272, T276, T288, T218, appc32_out_gga(T281, T280, T287)) → U44_AG(T215, T269, T272, T276, T288, T218, front14_in_aa(T288, X265))
U43_AG(T215, T269, T272, T276, T288, T218, appc32_out_gga(T281, T280, T287)) → FRONT14_IN_AA(T288, X265)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T288), .(T312, .(T333, T336))) → U45_AG(T215, T269, T272, T276, T288, T312, T333, T336, frontc14_in_aa(T272, T281))
U45_AG(T215, T269, T272, T276, T288, T312, T333, T336, frontc14_out_aa(T272, T281)) → U46_AG(T215, T269, T272, T276, T288, T312, T333, T336, T281, frontc14_in_aa(T276, T280))
U46_AG(T215, T269, T272, T276, T288, T312, T333, T336, T281, frontc14_out_aa(T276, T280)) → U47_AG(T215, T269, T272, T276, T288, T312, T333, T336, appc32_in_gga(T281, T280, .(T312, .(T333, T337))))
U47_AG(T215, T269, T272, T276, T288, T312, T333, T336, appc32_out_gga(T281, T280, .(T312, .(T333, T337)))) → U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_in_aa(T288, T338))
U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_out_aa(T288, T338)) → U49_AG(T215, T269, T272, T276, T288, T312, T333, T336, app178_in_ggg(T337, T338, T336))
U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_out_aa(T288, T338)) → APP178_IN_GGG(T337, T338, T336)
APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → U8_GGG(T354, T358, T359, T357, app178_in_ggg(T358, T359, T357))
APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → APP178_IN_GGG(T358, T359, T357)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
front14_in_aa(x1, x2)  =  front14_in_aa
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
app32_in_gga(x1, x2, x3)  =  app32_in_gga(x1, x2)
app178_in_ggg(x1, x2, x3)  =  app178_in_ggg(x1, x2, x3)
FRONT1_IN_AG(x1, x2)  =  FRONT1_IN_AG(x2)
U9_AG(x1, x2, x3)  =  U9_AG(x3)
FRONT14_IN_AA(x1, x2)  =  FRONT14_IN_AA
U1_AA(x1, x2, x3, x4, x5)  =  U1_AA(x5)
U2_AA(x1, x2, x3, x4, x5)  =  U2_AA(x5)
U3_AA(x1, x2, x3, x4, x5)  =  U3_AA(x5)
U4_AA(x1, x2, x3, x4, x5)  =  U4_AA(x5)
U5_AA(x1, x2, x3, x4, x5, x6)  =  U5_AA(x5, x6)
U6_AA(x1, x2, x3, x4, x5)  =  U6_AA(x5)
APP32_IN_GGA(x1, x2, x3)  =  APP32_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4, x5)  =  U7_GGA(x2, x3, x5)
U10_AG(x1, x2, x3, x4)  =  U10_AG(x4)
U11_AG(x1, x2, x3, x4, x5, x6)  =  U11_AG(x6)
U12_AG(x1, x2, x3, x4, x5, x6)  =  U12_AG(x6)
U13_AG(x1, x2, x3, x4, x5, x6)  =  U13_AG(x6)
U14_AG(x1, x2, x3, x4, x5, x6)  =  U14_AG(x6)
U15_AG(x1, x2, x3, x4, x5, x6, x7)  =  U15_AG(x6, x7)
U16_AG(x1, x2, x3, x4, x5, x6)  =  U16_AG(x6)
U17_AG(x1, x2, x3, x4, x5, x6)  =  U17_AG(x6)
U18_AG(x1, x2, x3, x4, x5, x6, x7)  =  U18_AG(x6, x7)
U19_AG(x1, x2, x3, x4, x5, x6)  =  U19_AG(x6)
U20_AG(x1, x2, x3, x4, x5, x6)  =  U20_AG(x6)
U21_AG(x1, x2, x3, x4)  =  U21_AG(x4)
U22_AG(x1, x2, x3, x4, x5)  =  U22_AG(x5)
U23_AG(x1, x2, x3, x4, x5, x6, x7)  =  U23_AG(x7)
U24_AG(x1, x2, x3, x4, x5, x6, x7)  =  U24_AG(x7)
U25_AG(x1, x2, x3, x4, x5, x6, x7)  =  U25_AG(x7)
U26_AG(x1, x2, x3, x4, x5, x6, x7)  =  U26_AG(x7)
U27_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_AG(x7, x8)
U28_AG(x1, x2, x3, x4, x5, x6, x7)  =  U28_AG(x7)
U29_AG(x1, x2, x3, x4, x5, x6, x7)  =  U29_AG(x7)
U30_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U30_AG(x7, x8)
U31_AG(x1, x2, x3, x4, x5, x6, x7)  =  U31_AG(x7)
U32_AG(x1, x2, x3, x4, x5, x6, x7)  =  U32_AG(x7)
U33_AG(x1, x2, x3, x4)  =  U33_AG(x3, x4)
U34_AG(x1, x2, x3, x4, x5)  =  U34_AG(x4, x5)
U35_AG(x1, x2, x3, x4, x5, x6, x7)  =  U35_AG(x6, x7)
U36_AG(x1, x2, x3, x4, x5, x6, x7)  =  U36_AG(x6, x7)
U37_AG(x1, x2, x3, x4, x5, x6, x7)  =  U37_AG(x6, x7)
U38_AG(x1, x2, x3, x4, x5, x6, x7)  =  U38_AG(x6, x7)
U39_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_AG(x6, x7, x8)
U40_AG(x1, x2, x3, x4, x5, x6, x7)  =  U40_AG(x6, x7)
U41_AG(x1, x2, x3, x4, x5, x6, x7)  =  U41_AG(x6, x7)
U42_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_AG(x6, x7, x8)
U43_AG(x1, x2, x3, x4, x5, x6, x7)  =  U43_AG(x6, x7)
U44_AG(x1, x2, x3, x4, x5, x6, x7)  =  U44_AG(x6, x7)
U45_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U45_AG(x8, x9)
U46_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U46_AG(x8, x9, x10)
U47_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_AG(x8, x9)
U48_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U48_AG(x8, x9, x10)
U49_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_AG(x8, x9)
APP178_IN_GGG(x1, x2, x3)  =  APP178_IN_GGG(x1, x2, x3)
U8_GGG(x1, x2, x3, x4, x5)  =  U8_GGG(x2, x3, x4, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 68 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → APP178_IN_GGG(T358, T359, T357)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
APP178_IN_GGG(x1, x2, x3)  =  APP178_IN_GGG(x1, x2, x3)

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

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

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

APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → APP178_IN_GGG(T358, T359, T357)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
APP178_IN_GGG(x1, x2, x3)  =  APP178_IN_GGG(x1, x2, x3)

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

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

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

APP178_IN_GGG(.(T358), T359, .(T357)) → APP178_IN_GGG(T358, T359, T357)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• APP178_IN_GGG(.(T358), T359, .(T357)) → APP178_IN_GGG(T358, T359, T357)
  The graph contains the following edges 1 > 1, 2 >= 2, 3 > 3

(15) YES

(16) Obligation:

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

APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → APP32_IN_GGA(T50, T51, X68)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
APP32_IN_GGA(x1, x2, x3)  =  APP32_IN_GGA(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

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

APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → APP32_IN_GGA(T50, T51, X68)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
APP32_IN_GGA(x1, x2, x3)  =  APP32_IN_GGA(x1, x2)

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

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

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

APP32_IN_GGA(.(T50), T51) → APP32_IN_GGA(T50, T51)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• APP32_IN_GGA(.(T50), T51) → APP32_IN_GGA(T50, T51)
  The graph contains the following edges 1 > 1, 2 >= 2

(22) YES

(23) Obligation:

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

FRONT14_IN_AA(tree(T25, T28, T31), X41) → U2_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T30))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → FRONT14_IN_AA(T31, X40)
FRONT14_IN_AA(tree(T25, T28, T29), X41) → FRONT14_IN_AA(T28, X39)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
FRONT14_IN_AA(x1, x2)  =  FRONT14_IN_AA
U2_AA(x1, x2, x3, x4, x5)  =  U2_AA(x5)

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

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

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

FRONT14_IN_AA → U2_AA(frontc14_in_aa)
U2_AA(frontc14_out_aa(T28, T30)) → FRONT14_IN_AA
FRONT14_IN_AA → FRONT14_IN_AA

The TRS R consists of the following rules:

frontc14_in_aa → frontc14_out_aa(void, [])
frontc14_in_aa → frontc14_out_aa(tree(void, void), .([]))
frontc14_in_aa → U51_aa(frontc14_in_aa)
U51_aa(frontc14_out_aa(T28, T33)) → U52_aa(T28, T33, frontc14_in_aa)
U52_aa(T28, T33, frontc14_out_aa(T31, T32)) → U53_aa(T28, T31, appc32_in_gga(T33, T32))
appc32_in_gga([], T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T50), T51) → U54_gga(T50, T51, appc32_in_gga(T50, T51))
U54_gga(T50, T51, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T50), T51, .(X68))
U53_aa(T28, T31, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T28, T31), X41)

The set Q consists of the following terms:

frontc14_in_aa
U51_aa(x0)
U52_aa(x0, x1, x2)
appc32_in_gga(x0, x1)
U54_gga(x0, x1, x2)
U53_aa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(26) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule FRONT14_IN_AA → U2_AA(frontc14_in_aa) at position [0] we obtained the following new rules [LPAR04]:

FRONT14_IN_AA → U2_AA(frontc14_out_aa(void, []))
FRONT14_IN_AA → U2_AA(frontc14_out_aa(tree(void, void), .([])))
FRONT14_IN_AA → U2_AA(U51_aa(frontc14_in_aa))

(27) Obligation:

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

U2_AA(frontc14_out_aa(T28, T30)) → FRONT14_IN_AA
FRONT14_IN_AA → FRONT14_IN_AA
FRONT14_IN_AA → U2_AA(frontc14_out_aa(void, []))
FRONT14_IN_AA → U2_AA(frontc14_out_aa(tree(void, void), .([])))
FRONT14_IN_AA → U2_AA(U51_aa(frontc14_in_aa))

The TRS R consists of the following rules:

frontc14_in_aa → frontc14_out_aa(void, [])
frontc14_in_aa → frontc14_out_aa(tree(void, void), .([]))
frontc14_in_aa → U51_aa(frontc14_in_aa)
U51_aa(frontc14_out_aa(T28, T33)) → U52_aa(T28, T33, frontc14_in_aa)
U52_aa(T28, T33, frontc14_out_aa(T31, T32)) → U53_aa(T28, T31, appc32_in_gga(T33, T32))
appc32_in_gga([], T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T50), T51) → U54_gga(T50, T51, appc32_in_gga(T50, T51))
U54_gga(T50, T51, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T50), T51, .(X68))
U53_aa(T28, T31, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T28, T31), X41)

The set Q consists of the following terms:

frontc14_in_aa
U51_aa(x0)
U52_aa(x0, x1, x2)
appc32_in_gga(x0, x1)
U54_gga(x0, x1, x2)
U53_aa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(28) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = FRONT14_IN_AA evaluates to t =FRONT14_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from FRONT14_IN_AA to FRONT14_IN_AA.

(29) NO