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

(0) Obligation:

Clauses:

init_vars(E1, E2, E1init, E2init) :- ','(find_all_vars(E1, Vars1), ','(find_all_vars(E2, Vars2), ','(intersect(Vars1, Vars2, _X, Notin1, Notin2), ','(init_vars2(Notin1, E1, E1init), init_vars2(Notin2, E2, E2init))))).
find_all_vars(E, Vars) :- ','(find_all_vars2(E, Vars0), sort(Vars0, Vars)).
find_all_vars2([], []).
find_all_vars2(.(=(Vars, _Values), Es), AllVars) :- ','(append(Vars, AllVars1, AllVars), find_all_vars2(Es, AllVars1)).
init_vars2(Notin, E, Einit) :- ','(init_vars3(Notin, E, Einit0), sort(Einit0, Einit)).
init_vars3([], E, E).
init_vars3(.(Var, Vars), E, .(=(.(Var, []), .(unbound, [])), Es)) :- init_vars3(Vars, E, Es).
append([], A, A).
append(.(A, B), C, .(A, D)) :- append(B, C, D).
intersect(As, [], [], [], As) :- !.
intersect([], Bs, [], Bs, []) :- !.
intersect(.(A, As), .(B, Bs), Cs, Ds, Es) :- ;(;(->(=(A, B), ','(=(Cs, .(A, Cs2)), intersect(As, Bs, Cs2, Ds, Es))), ->(@<(A, B), ','(=(Es, .(A, Es2)), intersect(As, .(B, Bs), Cs, Ds, Es2)))), ','(=(Ds, .(B, Ds2)), intersect(.(A, As), Bs, Cs, Ds2, Es))).
get_query(E1, E2) :- ','(=(E1, .(=(X, .(a, [])), .(=(X, .(a, [])), .(=(X, .(a, [])), .(=(X, .(a, [])), []))))), ','(=(E2, .(=(Y, .(a, [])), .(=(Y, .(a, [])), .(=(Y, .(a, [])), .(=(Y, .(a, [])), []))))), ','(=(X, .(5, .(7, .(8, .(3, .(2, .(4, .(1, .(6, .(9, .(15, .(17, .(18, .(13, .(12, .(14, .(11, .(16, .(19, .(25, .(27, .(28, .(23, .(22, .(24, .(21, .(26, .(29, [])))))))))))))))))))))))))))), =(Y, .(15, .(17, .(18, .(13, .(12, .(14, .(11, .(16, .(19, .(35, .(37, .(38, .(33, .(32, .(34, .(5, .(7, .(8, .(3, .(2, .(4, .(1, .(6, .(9, .(31, .(36, .(39, []))))))))))))))))))))))))))))))).

Query: init_vars(g,g,a,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: init_vars(T1, T2, T3, T4)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: init_vars(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(find_all_vars(T9, X9), ','(find_all_vars(T10, X10), ','(intersect(X9, X10, X11, X12, X13), ','(init_vars2(X12, T9, T13), init_vars2(X13, T10, T14)))))\n\nT9 is ground\nT10 is ground\nX9 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(find_all_vars(T9, X9), ','(find_all_vars(T10, X10), ','(intersect(X9, X10, X11, X12, X13), ','(init_vars2(X12, T9, T13), init_vars2(X13, T10, T14))))), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nT10 is ground\nX9 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="B: ','(','(find_all_vars2(T17, X23), sort(X23, X24)), ','(find_all_vars(T10, X10), ','(intersect(X24, X10, X11, X12, X13), ','(init_vars2(X12, T17, T13), init_vars2(X13, T10, T14)))))\n\nT10 is ground\nT17 is ground\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nX24 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="G: find_all_vars2(T17, X23)\n\nT17 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="I: ','(sort(T18, X24), ','(find_all_vars(T10, X10), ','(intersect(X24, X10, X11, X12, X13), ','(init_vars2(X12, T17, T13), init_vars2(X13, T10, T14)))))\n\nT10 is ground\nT17 is ground\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: find_all_vars2(T17, X23), SCOPE: 3, CLAUSE: 2 | find_all_vars2(T17, X23), SCOPE: 3, CLAUSE: 3\n\nT17 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: find_all_vars2(T17, X23), SCOPE: 3, CLAUSE: 2\n\nT17 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: find_all_vars2(T17, X23), SCOPE: 3, CLAUSE: 3\n\nT17 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="H: ','(append(T25, X40, X41), find_all_vars2(T27, X40))\n\nT25 is ground\nT27 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="C: append(T25, X40, X41)\n\nT25 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="D: find_all_vars2(T27, T28)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: append(T25, X40, X41), SCOPE: 4, CLAUSE: 7 | append(T25, X40, X41), SCOPE: 4, CLAUSE: 8\n\nT25 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: append(T25, X40, X41), SCOPE: 4, CLAUSE: 7\n\nT25 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: append(T25, X40, X41), SCOPE: 4, CLAUSE: 8\n\nT25 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: append(T35, X76, X77)\n\nT35 is ground\nX76 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: find_all_vars2(T27, T28), SCOPE: 5, CLAUSE: 2 | find_all_vars2(T27, T28), SCOPE: 5, CLAUSE: 3\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: find_all_vars2(T27, T28), SCOPE: 5, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: find_all_vars2(T27, T28), SCOPE: 5, CLAUSE: 3\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="E: ','(append(T44, X95, T48), find_all_vars2(T46, X95))\n\nT44 is ground\nT46 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="F: append(T44, X95, T48)\n\nT44 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: find_all_vars2(T46, T51)\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: append(T44, X95, T48), SCOPE: 6, CLAUSE: 7 | append(T44, X95, T48), SCOPE: 6, CLAUSE: 8\n\nT44 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: append(T44, X95, T48), SCOPE: 6, CLAUSE: 7\n\nT44 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: append(T44, X95, T48), SCOPE: 6, CLAUSE: 8\n\nT44 is ground\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: append(T66, X128, T68)\n\nT66 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 160 [arrowhead = none ];
160 -> 6;

161 [label="ONLY EVAL with clause\ninit_vars(X5, X6, X7, X8) :- ','(find_all_vars(X5, X9), ','(find_all_vars(X6, X10), ','(intersect(X9, X10, X11, X12, X13), ','(init_vars2(X12, X5, X7), init_vars2(X13, X6, X8))))).\nand substitutionT1 -> T9,\nX5 -> T9,\nT2 -> T10,\nX6 -> T10,\nT3 -> T13,\nX7 -> T13,\nT4 -> T14,\nX8 -> T14,\nT11 -> T13,\nT12 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 161 [arrowhead = none ];
161 -> 8;

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

163 [label="ONLY EVAL with clause\nfind_all_vars(X21, X22) :- ','(find_all_vars2(X21, X23), sort(X23, X22)).\nand substitutionT9 -> T17,\nX21 -> T17,\nX9 -> X24,\nX22 -> X24", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 163 [arrowhead = none ];
163 -> 13;

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

165 [label="SPLIT 2\nnew knowledge:\nT17 is ground\nreplacements:X23 -> T18", fontsize=14, style = filled, fillcolor = violet];
13 -> 165 [arrowhead = none ];
165 -> 19;

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

167 [label="UNDEFINED ERROR", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 167 [arrowhead = none ];
167 -> 159;

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

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

170 [label="EVAL with clause\nfind_all_vars2([], []).\nand substitutionT17 -> [],\nX23 -> []", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 170 [arrowhead = none ];
170 -> 43;

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

172 [label="EVAL with clause\nfind_all_vars2(.(=(X36, X37), X38), X39) :- ','(append(X36, X40, X39), find_all_vars2(X38, X40)).\nand substitutionX36 -> T25,\nX37 -> T26,\nX38 -> T27,\nT17 -> .(=(T25, T26), T27),\nX23 -> X41,\nX39 -> X41", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 172 [arrowhead = none ];
172 -> 63;

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

174 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 174 [arrowhead = none ];
174 -> 45;

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

176 [label="SPLIT 2\nnew knowledge:\nT25 is ground\nreplacements:X40 -> T28,\nX41 -> T29", fontsize=14, style = filled, fillcolor = violet];
63 -> 176 [arrowhead = none ];
176 -> 67;

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

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

179 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
72 -> 179 [arrowhead = none ];
179 -> 77;

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

181 [label="EVAL with clause\nappend([], X58, X58).\nand substitutionT25 -> [],\nX40 -> X59,\nX58 -> X59,\nX41 -> X59", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 181 [arrowhead = none ];
181 -> 79;

182 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 182 [arrowhead = none ];
182 -> 81;

183 [label="EVAL with clause\nappend(.(X72, X73), X74, .(X72, X75)) :- append(X73, X74, X75).\nand substitutionX72 -> T34,\nX73 -> T35,\nT25 -> .(T34, T35),\nX40 -> X76,\nX74 -> X76,\nX75 -> X77,\nX41 -> .(T34, X77)", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 183 [arrowhead = none ];
183 -> 103;

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

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

186 [label="INSTANCE with matching:\nT25 -> T35\nX40 -> X76\nX41 -> X77", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 186 [arrowhead = none , style=dashed];
186 -> 66[style=dashed];

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

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

189 [label="EVAL with clause\nfind_all_vars2([], []).\nand substitutionT27 -> [],\nT28 -> []", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 189 [arrowhead = none ];
189 -> 118;

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

191 [label="EVAL with clause\nfind_all_vars2(.(=(X91, X92), X93), X94) :- ','(append(X91, X95, X94), find_all_vars2(X93, X95)).\nand substitutionX91 -> T44,\nX92 -> T45,\nX93 -> T46,\nT27 -> .(=(T44, T45), T46),\nT28 -> T48,\nX94 -> T48,\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 191 [arrowhead = none ];
191 -> 122;

192 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 192 [arrowhead = none ];
192 -> 123;

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

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

195 [label="SPLIT 2\nnew knowledge:\nT44 is ground\nreplacements:X95 -> T51", fontsize=14, style = filled, fillcolor = violet];
122 -> 195 [arrowhead = none ];
195 -> 127;

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

197 [label="INSTANCE with matching:\nT27 -> T46\nT28 -> T51", fontsize=14, style = filled, fillcolor = lightgrey];
127 -> 197 [arrowhead = none , style=dashed];
197 -> 67[style=dashed];

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

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

200 [label="EVAL with clause\nappend([], X112, X112).\nand substitutionT44 -> [],\nX95 -> T58,\nX112 -> T58,\nT48 -> T58,\nX113 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 200 [arrowhead = none ];
200 -> 138;

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

202 [label="EVAL with clause\nappend(.(X124, X125), X126, .(X124, X127)) :- append(X125, X126, X127).\nand substitutionX124 -> T65,\nX125 -> T66,\nT44 -> .(T65, T66),\nX95 -> X128,\nX126 -> X128,\nX127 -> T68,\nT48 -> .(T65, T68),\nT67 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 202 [arrowhead = none ];
202 -> 155;

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

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

205 [label="INSTANCE with matching:\nT44 -> T66\nX95 -> X128\nT48 -> T68", fontsize=14, style = filled, fillcolor = lightgrey];
155 -> 205 [arrowhead = none , style=dashed];
205 -> 126[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
R is empty.
Pi is empty.

(3) RisEmptyProof (EQUIVALENT transformation)

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

(4) YES