Left Termination proof of /tmp/tmpS3lduZ/shapes.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 255 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 1073 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 34 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 22 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPOrderProof (⇔, 323 ms)

        ↳20 QDP

        ↳21 DependencyGraphProof (⇔, 0 ms)

        ↳22 TRUE

    ↳23 PiDP

        ↳24 UsableRulesProof (⇔, 0 ms)

        ↳25 PiDP

        ↳26 PiDPToQDPProof (⇒, 42 ms)

        ↳27 QDP

        ↳28 QDPSizeChangeProof (⇔, 0 ms)

        ↳29 YES

    ↳30 PiDP

        ↳31 UsableRulesProof (⇔, 0 ms)

        ↳32 PiDP

        ↳33 PiDPToQDPProof (⇒, 23 ms)

        ↳34 QDP

        ↳35 QDPSizeChangeProof (⇔, 0 ms)

        ↳36 YES

(0) Obligation:

Clauses:

shapes(Matrix, N) :- ','(varmat(Matrix, MatrixWithVars), unif_matrx(MatrixWithVars)).
varmat([], []).
varmat(.(L, Ls), .(VL, VLs)) :- ','(varmat(L, VL), varmat(Ls, VLs)).
varmat(.(black, Xs), .(black, VXs)) :- varmat(Xs, VXs).
varmat(.(white, Xs), .(w(X1), VXs)) :- varmat(Xs, VXs).
unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls))).
unif_matrx(.(X2, [])).
unif_lines(.(W, .(X, L1s)), .(Y, .(Z, L2s))) :- ','(unif_pairs(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))), unif_lines(.(X, L1s), .(Z, L2s))).
unif_lines(.(X3, []), .(X4, [])).
unif_pairs([]).
unif_pairs(.(A, .(B, Pairs))) :- ','(unif(A, B), unif_pairs(Pairs)).
unif(w(A), w(A)).
unif(black, black).
unif(black, w(X5)).
unif(w(X6), black).

Query: shapes(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: shapes(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: shapes(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(varmat(T5, X11), unif_matrx(X11))\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 1 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 2 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 3 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 2 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 3 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: unif_matrx([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: unif_matrx([]), SCOPE: 3, CLAUSE: 5 | unif_matrx([]), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: unif_matrx([]), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 3 | ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="B: ','(','(varmat(T15, X47), varmat(T16, X48)), unif_matrx(.(X47, X48)))\n\nT15 is ground\nT16 is ground\nX47 is free\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="E: varmat(T15, X47)\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="D: ','(varmat(T16, X48), unif_matrx(.(T17, X48)))\n\nT16 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: varmat(T15, X47), SCOPE: 4, CLAUSE: 1 | varmat(T15, X47), SCOPE: 4, CLAUSE: 2 | varmat(T15, X47), SCOPE: 4, CLAUSE: 3 | varmat(T15, X47), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: varmat(T15, X47), SCOPE: 4, CLAUSE: 1\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: varmat(T15, X47), SCOPE: 4, CLAUSE: 2 | varmat(T15, X47), SCOPE: 4, CLAUSE: 3 | varmat(T15, X47), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: true\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];
78 [label="78: varmat(T15, X47), SCOPE: 4, CLAUSE: 2\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: varmat(T15, X47), SCOPE: 4, CLAUSE: 3 | varmat(T15, X47), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="F: ','(varmat(T26, X77), varmat(T27, X78))\n\nT26 is ground\nT27 is ground\nX77 is free\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: varmat(T26, X77)\n\nT26 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: varmat(T27, X78)\n\nT27 is ground\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: varmat(T15, X47), SCOPE: 4, CLAUSE: 3\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: varmat(T15, X47), SCOPE: 4, CLAUSE: 4\n\nT15 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: varmat(T33, X93)\n\nT33 is ground\nX93 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: varmat(T36, X108)\n\nT36 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: varmat(T16, X48)\n\nT16 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="G: unif_matrx(.(T17, T37))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: unif_matrx(.(T17, T37)), SCOPE: 5, CLAUSE: 5 | unif_matrx(.(T17, T37)), SCOPE: 5, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: unif_matrx(.(T17, T37)), SCOPE: 5, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: unif_matrx(.(T17, T37)), SCOPE: 5, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="H: ','(unif_lines(T56, T57), unif_matrx(.(T57, T58)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="I: unif_lines(T56, T57)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: unif_matrx(.(T65, T66))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: unif_lines(T56, T57), SCOPE: 6, CLAUSE: 7 | unif_lines(T56, T57), SCOPE: 6, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: unif_lines(T56, T57), SCOPE: 6, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: unif_lines(T56, T57), SCOPE: 6, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: ','(unif_pairs(.(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))))), unif_lines(.(T104, T107), .(T106, T108)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="J: ','(unif_pairs(.(T103, T109)), unif_lines(.(T104, T107), .(T106, T108)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="L: unif_pairs(.(T103, T109))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: unif_lines(.(T110, T111), .(T112, T113))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: unif_pairs(.(T103, T109)), SCOPE: 7, CLAUSE: 9 | unif_pairs(.(T103, T109)), SCOPE: 7, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: unif_pairs(.(T103, T109)), SCOPE: 7, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: ','(unif(T123, T124), unif_pairs(T125))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 11 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 12 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 13 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 11\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 12 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 13 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="K: unif_pairs(T131)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: unif_pairs(T131), SCOPE: 9, CLAUSE: 9 | unif_pairs(T131), SCOPE: 9, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: unif_pairs(T131), SCOPE: 9, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: unif_pairs(T131), SCOPE: 9, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: ','(unif(T141, T142), unif_pairs(T143))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 11 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 12 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 13 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 11\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 12 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 13 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: unif_pairs(T149)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 12\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 13 | ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: unif_pairs(T150)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: ','(unif(T141, T142), unif_pairs(T143)), SCOPE: 10, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: unif_pairs(T156)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: unif_pairs(T160)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 12\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 13 | ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: unif_pairs(T161)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: ','(unif(T123, T124), unif_pairs(T125)), SCOPE: 8, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: unif_pairs(T167)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: unif_pairs(T171)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
308 [label="308: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 3\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
309 [label="309: ','(varmat(T5, X11), unif_matrx(X11)), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
310 [label="C: ','(varmat(T194, X245), unif_matrx(.(black, X245)))\n\nT194 is ground\nX245 is free", fontsize=16, style=filled, fillcolor=lightyellow];
311 [label="311: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
312 [label="312: varmat(T194, X245)\n\nT194 is ground\nX245 is free", fontsize=16, style=filled, fillcolor=lightyellow];
313 [label="M: unif_matrx(.(black, T195))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: unif_matrx(.(black, T195)), SCOPE: 11, CLAUSE: 5 | unif_matrx(.(black, T195)), SCOPE: 11, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: unif_matrx(.(black, T195)), SCOPE: 11, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: unif_matrx(.(black, T195)), SCOPE: 11, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="N: ','(unif_lines(black, T208), unif_matrx(.(T208, T209)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="O: unif_lines(black, T208)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: unif_matrx(.(T210, T211))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: unif_lines(black, T208), SCOPE: 12, CLAUSE: 7 | unif_lines(black, T208), SCOPE: 12, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: unif_lines(black, T208), SCOPE: 12, CLAUSE: 8\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
325 [label="325: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="327: ','(varmat(T217, X304), unif_matrx(.(w(X303), X304)))\n\nT217 is ground\nX303 is free\nX304 is free", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 329 [arrowhead = none ];
329 -> 6;

330 [label="ONLY EVAL with clause\nshapes(X9, X10) :- ','(varmat(X9, X11), unif_matrx(X11)).\nand substitutionT1 -> T5,\nX9 -> T5,\nT2 -> T6,\nX10 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 330 [arrowhead = none ];
330 -> 8;

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

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

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

334 [label="EVAL with clause\nvarmat([], []).\nand substitutionT5 -> [],\nX11 -> []", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 334 [arrowhead = none ];
334 -> 17;

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

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

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

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

339 [label="BACKTRACK\nfor clause: unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 339 [arrowhead = none ];
339 -> 23;

340 [label="BACKTRACK\nfor clause: unif_matrx(.(X2, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 340 [arrowhead = none ];
340 -> 27;

341 [label="EVAL with clause\nvarmat(.(X43, X44), .(X45, X46)) :- ','(varmat(X43, X45), varmat(X44, X46)).\nand substitutionX43 -> T15,\nX44 -> T16,\nT5 -> .(T15, T16),\nX45 -> X47,\nX46 -> X48,\nX11 -> .(X47, X48)", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 341 [arrowhead = none ];
341 -> 42;

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

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

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

345 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
42 -> 345 [arrowhead = none ];
345 -> 58;

346 [label="SPLIT 2\nnew knowledge:\nT15 is ground\nreplacements:X47 -> T17", fontsize=14, style = filled, fillcolor = violet];
42 -> 346 [arrowhead = none ];
346 -> 59;

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

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

349 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nreplacements:X48 -> T37", fontsize=14, style = filled, fillcolor = violet];
59 -> 349 [arrowhead = none ];
349 -> 147;

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

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

352 [label="EVAL with clause\nvarmat([], []).\nand substitutionT15 -> [],\nX47 -> []", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 352 [arrowhead = none ];
352 -> 71;

353 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 353 [arrowhead = none ];
353 -> 72;

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

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

356 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 356 [arrowhead = none ];
356 -> 73;

357 [label="EVAL with clause\nvarmat(.(X73, X74), .(X75, X76)) :- ','(varmat(X73, X75), varmat(X74, X76)).\nand substitutionX73 -> T26,\nX74 -> T27,\nT15 -> .(T26, T27),\nX75 -> X77,\nX76 -> X78,\nX47 -> .(X77, X78)", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 357 [arrowhead = none ];
357 -> 91;

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

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

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

361 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
91 -> 361 [arrowhead = none ];
361 -> 96;

362 [label="SPLIT 2\nnew knowledge:\nT26 is ground\nreplacements:X77 -> T28", fontsize=14, style = filled, fillcolor = violet];
91 -> 362 [arrowhead = none ];
362 -> 97;

363 [label="INSTANCE with matching:\nT15 -> T26\nX47 -> X77", fontsize=14, style = filled, fillcolor = lightgrey];
96 -> 363 [arrowhead = none , style=dashed];
363 -> 58[style=dashed];

364 [label="INSTANCE with matching:\nT15 -> T27\nX47 -> X78", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 364 [arrowhead = none , style=dashed];
364 -> 58[style=dashed];

365 [label="EVAL with clause\nvarmat(.(black, X91), .(black, X92)) :- varmat(X91, X92).\nand substitutionX91 -> T33,\nT15 -> .(black, T33),\nX92 -> X93,\nX47 -> .(black, X93)", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 365 [arrowhead = none ];
365 -> 112;

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

367 [label="EVAL with clause\nvarmat(.(white, X104), .(w(X105), X106)) :- varmat(X104, X106).\nand substitutionX104 -> T36,\nT15 -> .(white, T36),\nX105 -> X107,\nX106 -> X108,\nX47 -> .(w(X107), X108)", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 367 [arrowhead = none ];
367 -> 137;

368 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 368 [arrowhead = none ];
368 -> 138;

369 [label="INSTANCE with matching:\nT15 -> T33\nX47 -> X93", fontsize=14, style = filled, fillcolor = lightgrey];
112 -> 369 [arrowhead = none , style=dashed];
369 -> 58[style=dashed];

370 [label="INSTANCE with matching:\nT15 -> T36\nX47 -> X108", fontsize=14, style = filled, fillcolor = lightgrey];
137 -> 370 [arrowhead = none , style=dashed];
370 -> 58[style=dashed];

371 [label="INSTANCE with matching:\nT15 -> T16\nX47 -> X48", fontsize=14, style = filled, fillcolor = lightgrey];
146 -> 371 [arrowhead = none , style=dashed];
371 -> 58[style=dashed];

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

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

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

375 [label="EVAL with clause\nunif_matrx(.(X124, .(X125, X126))) :- ','(unif_lines(X124, X125), unif_matrx(.(X125, X126))).\nand substitutionT17 -> T56,\nX124 -> T56,\nX125 -> T57,\nX126 -> T58,\nT37 -> .(T57, T58),\nT53 -> T56,\nT54 -> T57,\nT55 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 375 [arrowhead = none ];
375 -> 176;

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

377 [label="EVAL with clause\nunif_matrx(.(X230, [])).\nand substitutionT17 -> T189,\nX230 -> T189,\nT37 -> []", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 377 [arrowhead = none ];
377 -> 305;

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

379 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
176 -> 379 [arrowhead = none ];
379 -> 207;

380 [label="SPLIT 2\nreplacements:T57 -> T65,\nT58 -> T66", fontsize=14, style = filled, fillcolor = violet];
176 -> 380 [arrowhead = none ];
380 -> 208;

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

382 [label="INSTANCE with matching:\nT17 -> T65\nT37 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
208 -> 382 [arrowhead = none , style=dashed];
382 -> 147[style=dashed];

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

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

385 [label="EVAL with clause\nunif_lines(.(X163, .(X164, X165)), .(X166, .(X167, X168))) :- ','(unif_pairs(.(X163, .(X164, .(X166, .(X167, .(X163, .(X166, .(X164, .(X167, .(X163, .(X167, .(X164, .(X166, []))))))))))))), unif_lines(.(X164, X165), .(X167, X168))).\nand substitutionX163 -> T103,\nX164 -> T104,\nX165 -> T107,\nT56 -> .(T103, .(T104, T107)),\nX166 -> T105,\nX167 -> T106,\nX168 -> T108,\nT57 -> .(T105, .(T106, T108)),\nT97 -> T103,\nT98 -> T104,\nT100 -> T105,\nT101 -> T106,\nT99 -> T107,\nT102 -> T108", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 385 [arrowhead = none ];
385 -> 231;

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

387 [label="EVAL with clause\nunif_lines(.(X223, []), .(X224, [])).\nand substitutionX223 -> T182,\nT56 -> .(T182, []),\nX224 -> T183,\nT57 -> .(T183, [])", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 387 [arrowhead = none ];
387 -> 302;

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

389 [label="GENERALIZATION\nT109 <-- .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, [])))))))))))", fontsize=14, style = filled, fillcolor = violet];
231 -> 389 [arrowhead = none ];
389 -> 233;

390 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
233 -> 390 [arrowhead = none ];
390 -> 237;

391 [label="SPLIT 2\nreplacements:T104 -> T110,\nT107 -> T111,\nT106 -> T112,\nT108 -> T113", fontsize=14, style = filled, fillcolor = violet];
233 -> 391 [arrowhead = none ];
391 -> 239;

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

393 [label="INSTANCE with matching:\nT56 -> .(T110, T111)\nT57 -> .(T112, T113)", fontsize=14, style = filled, fillcolor = lightgrey];
239 -> 393 [arrowhead = none , style=dashed];
393 -> 207[style=dashed];

394 [label="BACKTRACK\nfor clause: unif_pairs([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
241 -> 394 [arrowhead = none ];
394 -> 242;

395 [label="EVAL with clause\nunif_pairs(.(X175, .(X176, X177))) :- ','(unif(X175, X176), unif_pairs(X177)).\nand substitutionT103 -> T123,\nX175 -> T123,\nX176 -> T124,\nX177 -> T125,\nT109 -> .(T124, T125),\nT120 -> T123,\nT121 -> T124,\nT122 -> T125", fontsize=14, style = filled, fillcolor = lightblue];
242 -> 395 [arrowhead = none ];
395 -> 245;

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

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

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

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

400 [label="EVAL with clause\nunif(w(X182), w(X182)).\nand substitutionX182 -> T130,\nT123 -> w(T130),\nT124 -> w(T130),\nT125 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
250 -> 400 [arrowhead = none ];
400 -> 252;

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

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

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

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

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

406 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
254 -> 406 [arrowhead = none ];
406 -> 256;

407 [label="EVAL with clause\nunif_pairs([]).\nand substitutionT131 -> []", fontsize=14, style = filled, fillcolor = lightblue];
255 -> 407 [arrowhead = none ];
407 -> 257;

408 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
255 -> 408 [arrowhead = none ];
408 -> 258;

409 [label="EVAL with clause\nunif_pairs(.(X189, .(X190, X191))) :- ','(unif(X189, X190), unif_pairs(X191)).\nand substitutionX189 -> T141,\nX190 -> T142,\nX191 -> T143,\nT131 -> .(T141, .(T142, T143)),\nT138 -> T141,\nT139 -> T142,\nT140 -> T143", fontsize=14, style = filled, fillcolor = lightblue];
256 -> 409 [arrowhead = none ];
409 -> 263;

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

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

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

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

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

415 [label="EVAL with clause\nunif(w(X196), w(X196)).\nand substitutionX196 -> T148,\nT141 -> w(T148),\nT142 -> w(T148),\nT143 -> T149", fontsize=14, style = filled, fillcolor = lightblue];
266 -> 415 [arrowhead = none ];
415 -> 269;

416 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
266 -> 416 [arrowhead = none ];
416 -> 271;

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

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

419 [label="INSTANCE with matching:\nT131 -> T149", fontsize=14, style = filled, fillcolor = lightgrey];
269 -> 419 [arrowhead = none , style=dashed];
419 -> 252[style=dashed];

420 [label="EVAL with clause\nunif(black, black).\nand substitutionT141 -> black,\nT142 -> black,\nT143 -> T150", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 420 [arrowhead = none ];
420 -> 274;

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

422 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
273 -> 422 [arrowhead = none ];
422 -> 278;

423 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
273 -> 423 [arrowhead = none ];
423 -> 279;

424 [label="INSTANCE with matching:\nT131 -> T150", fontsize=14, style = filled, fillcolor = lightgrey];
274 -> 424 [arrowhead = none , style=dashed];
424 -> 252[style=dashed];

425 [label="EVAL with clause\nunif(black, w(X201)).\nand substitutionT141 -> black,\nX201 -> T155,\nT142 -> w(T155),\nT143 -> T156", fontsize=14, style = filled, fillcolor = lightblue];
278 -> 425 [arrowhead = none ];
425 -> 280;

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

427 [label="EVAL with clause\nunif(w(X204), black).\nand substitutionX204 -> T159,\nT141 -> w(T159),\nT142 -> black,\nT143 -> T160", fontsize=14, style = filled, fillcolor = lightblue];
279 -> 427 [arrowhead = none ];
427 -> 283;

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

429 [label="INSTANCE with matching:\nT131 -> T156", fontsize=14, style = filled, fillcolor = lightgrey];
280 -> 429 [arrowhead = none , style=dashed];
429 -> 252[style=dashed];

430 [label="INSTANCE with matching:\nT131 -> T160", fontsize=14, style = filled, fillcolor = lightgrey];
283 -> 430 [arrowhead = none , style=dashed];
430 -> 252[style=dashed];

431 [label="EVAL with clause\nunif(black, black).\nand substitutionT123 -> black,\nT124 -> black,\nT125 -> T161", fontsize=14, style = filled, fillcolor = lightblue];
287 -> 431 [arrowhead = none ];
431 -> 289;

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

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

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

435 [label="INSTANCE with matching:\nT131 -> T161", fontsize=14, style = filled, fillcolor = lightgrey];
289 -> 435 [arrowhead = none , style=dashed];
435 -> 252[style=dashed];

436 [label="EVAL with clause\nunif(black, w(X209)).\nand substitutionT123 -> black,\nX209 -> T166,\nT124 -> w(T166),\nT125 -> T167", fontsize=14, style = filled, fillcolor = lightblue];
296 -> 436 [arrowhead = none ];
436 -> 298;

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

438 [label="EVAL with clause\nunif(w(X212), black).\nand substitutionX212 -> T170,\nT123 -> w(T170),\nT124 -> black,\nT125 -> T171", fontsize=14, style = filled, fillcolor = lightblue];
297 -> 438 [arrowhead = none ];
438 -> 300;

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

440 [label="INSTANCE with matching:\nT131 -> T167", fontsize=14, style = filled, fillcolor = lightgrey];
298 -> 440 [arrowhead = none , style=dashed];
440 -> 252[style=dashed];

441 [label="INSTANCE with matching:\nT131 -> T171", fontsize=14, style = filled, fillcolor = lightgrey];
300 -> 441 [arrowhead = none , style=dashed];
441 -> 252[style=dashed];

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

443 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
305 -> 443 [arrowhead = none ];
443 -> 307;

444 [label="EVAL with clause\nvarmat(.(black, X243), .(black, X244)) :- varmat(X243, X244).\nand substitutionX243 -> T194,\nT5 -> .(black, T194),\nX244 -> X245,\nX11 -> .(black, X245)", fontsize=14, style = filled, fillcolor = lightblue];
308 -> 444 [arrowhead = none ];
444 -> 310;

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

446 [label="EVAL with clause\nvarmat(.(white, X300), .(w(X301), X302)) :- varmat(X300, X302).\nand substitutionX300 -> T217,\nT5 -> .(white, T217),\nX301 -> X303,\nX302 -> X304,\nX11 -> .(w(X303), X304)", fontsize=14, style = filled, fillcolor = lightblue];
309 -> 446 [arrowhead = none ];
446 -> 327;

447 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
309 -> 447 [arrowhead = none ];
447 -> 328;

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

449 [label="SPLIT 2\nnew knowledge:\nT194 is ground\nreplacements:X245 -> T195", fontsize=14, style = filled, fillcolor = violet];
310 -> 449 [arrowhead = none ];
449 -> 313;

450 [label="INSTANCE with matching:\nT15 -> T194\nX47 -> X245", fontsize=14, style = filled, fillcolor = lightgrey];
312 -> 450 [arrowhead = none , style=dashed];
450 -> 58[style=dashed];

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

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

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

454 [label="EVAL with clause\nunif_matrx(.(X261, .(X262, X263))) :- ','(unif_lines(X261, X262), unif_matrx(.(X262, X263))).\nand substitutionX261 -> black,\nX262 -> T208,\nX263 -> T209,\nT195 -> .(T208, T209),\nT206 -> T208,\nT207 -> T209", fontsize=14, style = filled, fillcolor = lightblue];
315 -> 454 [arrowhead = none ];
454 -> 317;

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

456 [label="EVAL with clause\nunif_matrx(.(X289, [])).\nand substitutionX289 -> black,\nT195 -> []", fontsize=14, style = filled, fillcolor = lightblue];
316 -> 456 [arrowhead = none ];
456 -> 324;

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

458 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
317 -> 458 [arrowhead = none ];
458 -> 319;

459 [label="SPLIT 2\nreplacements:T208 -> T210,\nT209 -> T211", fontsize=14, style = filled, fillcolor = violet];
317 -> 459 [arrowhead = none ];
459 -> 320;

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

461 [label="INSTANCE with matching:\nT17 -> T210\nT37 -> T211", fontsize=14, style = filled, fillcolor = lightgrey];
320 -> 461 [arrowhead = none , style=dashed];
461 -> 147[style=dashed];

462 [label="BACKTRACK\nfor clause: unif_lines(.(W, .(X, L1s)), .(Y, .(Z, L2s))) :- ','(unif_pairs(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))), unif_lines(.(X, L1s), .(Z, L2s)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
321 -> 462 [arrowhead = none ];
462 -> 322;

463 [label="BACKTRACK\nfor clause: unif_lines(.(X3, []), .(X4, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
322 -> 463 [arrowhead = none ];
463 -> 323;

464 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
324 -> 464 [arrowhead = none ];
464 -> 326;

465 [label="INSTANCE with matching:\nT16 -> T217\nX48 -> X304\nT17 -> w(X303)", fontsize=14, style = filled, fillcolor = lightgrey];
327 -> 465 [arrowhead = none , style=dashed];
465 -> 59[style=dashed];

}

(2) Obligation:

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

shapesA_in_ga(.(T15, T16), T6) → U1_ga(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
pB_in_gaga(T15, T17, T16, X48) → U17_gaga(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
varmatE_in_ga([], []) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27), .(X77, X78)) → U4_ga(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
pF_in_gaga(T26, T28, T27, X78) → U21_gaga(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
varmatE_in_ga(.(black, T33), .(black, X93)) → U5_ga(T33, X93, varmatE_in_ga(T33, X93))
varmatE_in_ga(.(white, T36), .(w(X107), X108)) → U6_ga(T36, X107, X108, varmatE_in_ga(T36, X108))
U6_ga(T36, X107, X108, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w(X107), X108))
U5_ga(T33, X93, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U21_gaga(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U22_gaga(T26, T28, T27, X78, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)
U4_ga(T26, T27, X77, X78, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U17_gaga(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_gaga(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
pD_in_gag(T16, T37, T17) → U19_gag(T16, T37, T17, varmatE_in_ga(T16, T37))
U19_gag(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_gag(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
unif_matrxG_in_gg(T56, .(T57, T58)) → U7_gg(T56, T57, T58, pH_in_ggg(T56, T57, T58))
pH_in_ggg(T56, T65, T66) → U23_ggg(T56, T65, T66, unif_linesI_in_gg(T56, T65))
unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
U23_ggg(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_ggg(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
unif_matrxG_in_gg(T189, []) → unif_matrxG_out_gg(T189, [])
U24_ggg(T56, T65, T66, unif_matrxG_out_gg(T65, T66)) → pH_out_ggg(T56, T65, T66)
U7_gg(T56, T57, T58, pH_out_ggg(T56, T57, T58)) → unif_matrxG_out_gg(T56, .(T57, T58))
U20_gag(T16, T37, T17, unif_matrxG_out_gg(T17, T37)) → pD_out_gag(T16, T37, T17)
U18_gaga(T15, T17, T16, X48, pD_out_gag(T16, X48, T17)) → pB_out_gaga(T15, T17, T16, X48)
U1_ga(T15, T16, T6, pB_out_gaga(T15, X47, T16, X48)) → shapesA_out_ga(.(T15, T16), T6)
shapesA_in_ga(.(black, T194), T6) → U2_ga(T194, T6, pC_in_ga(T194, X245))
pC_in_ga(T194, T195) → U27_ga(T194, T195, varmatE_in_ga(T194, T195))
U27_ga(T194, T195, varmatE_out_ga(T194, T195)) → U28_ga(T194, T195, unif_matrxM_in_g(T195))
unif_matrxM_in_g([]) → unif_matrxM_out_g([])
U28_ga(T194, T195, unif_matrxM_out_g(T195)) → pC_out_ga(T194, T195)
U2_ga(T194, T6, pC_out_ga(T194, X245)) → shapesA_out_ga(.(black, T194), T6)
shapesA_in_ga(.(white, T217), T6) → U3_ga(T217, T6, pD_in_gag(T217, X304, w(X303)))
U3_ga(T217, T6, pD_out_gag(T217, X304, w(X303))) → shapesA_out_ga(.(white, T217), T6)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

SHAPESA_IN_GA(.(T15, T16), T6) → U1_GA(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
SHAPESA_IN_GA(.(T15, T16), T6) → PB_IN_GAGA(T15, X47, T16, X48)
PB_IN_GAGA(T15, T17, T16, X48) → U17_GAGA(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
PB_IN_GAGA(T15, T17, T16, X48) → VARMATE_IN_GA(T15, T17)
VARMATE_IN_GA(.(T26, T27), .(X77, X78)) → U4_GA(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
VARMATE_IN_GA(.(T26, T27), .(X77, X78)) → PF_IN_GAGA(T26, X77, T27, X78)
PF_IN_GAGA(T26, T28, T27, X78) → U21_GAGA(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
PF_IN_GAGA(T26, T28, T27, X78) → VARMATE_IN_GA(T26, T28)
VARMATE_IN_GA(.(black, T33), .(black, X93)) → U5_GA(T33, X93, varmatE_in_ga(T33, X93))
VARMATE_IN_GA(.(black, T33), .(black, X93)) → VARMATE_IN_GA(T33, X93)
VARMATE_IN_GA(.(white, T36), .(w(X107), X108)) → U6_GA(T36, X107, X108, varmatE_in_ga(T36, X108))
VARMATE_IN_GA(.(white, T36), .(w(X107), X108)) → VARMATE_IN_GA(T36, X108)
U21_GAGA(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_GAGA(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U21_GAGA(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → VARMATE_IN_GA(T27, X78)
U17_GAGA(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_GAGA(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
U17_GAGA(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → PD_IN_GAG(T16, X48, T17)
PD_IN_GAG(T16, T37, T17) → U19_GAG(T16, T37, T17, varmatE_in_ga(T16, T37))
PD_IN_GAG(T16, T37, T17) → VARMATE_IN_GA(T16, T37)
U19_GAG(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_GAG(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
U19_GAG(T16, T37, T17, varmatE_out_ga(T16, T37)) → UNIF_MATRXG_IN_GG(T17, T37)
UNIF_MATRXG_IN_GG(T56, .(T57, T58)) → U7_GG(T56, T57, T58, pH_in_ggg(T56, T57, T58))
UNIF_MATRXG_IN_GG(T56, .(T57, T58)) → PH_IN_GGG(T56, T57, T58)
PH_IN_GGG(T56, T65, T66) → U23_GGG(T56, T65, T66, unif_linesI_in_gg(T56, T65))
PH_IN_GGG(T56, T65, T66) → UNIF_LINESI_IN_GG(T56, T65)
UNIF_LINESI_IN_GG(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_GG(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
UNIF_LINESI_IN_GG(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → PJ_IN_GGGGGG(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)
PJ_IN_GGGGGG(T103, T109, T110, T111, T112, T113) → U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
PJ_IN_GGGGGG(T103, T109, T110, T111, T112, T113) → UNIF_PAIRSL_IN_GG(T103, T109)
UNIF_PAIRSL_IN_GG(w(T130), .(w(T130), T131)) → U13_GG(T130, T131, unif_pairsK_in_g(T131))
UNIF_PAIRSL_IN_GG(w(T130), .(w(T130), T131)) → UNIF_PAIRSK_IN_G(T131)
UNIF_PAIRSK_IN_G(.(w(T148), .(w(T148), T149))) → U9_G(T148, T149, unif_pairsK_in_g(T149))
UNIF_PAIRSK_IN_G(.(w(T148), .(w(T148), T149))) → UNIF_PAIRSK_IN_G(T149)
UNIF_PAIRSK_IN_G(.(black, .(black, T150))) → U10_G(T150, unif_pairsK_in_g(T150))
UNIF_PAIRSK_IN_G(.(black, .(black, T150))) → UNIF_PAIRSK_IN_G(T150)
UNIF_PAIRSK_IN_G(.(black, .(w(T155), T156))) → U11_G(T155, T156, unif_pairsK_in_g(T156))
UNIF_PAIRSK_IN_G(.(black, .(w(T155), T156))) → UNIF_PAIRSK_IN_G(T156)
UNIF_PAIRSK_IN_G(.(w(T159), .(black, T160))) → U12_G(T159, T160, unif_pairsK_in_g(T160))
UNIF_PAIRSK_IN_G(.(w(T159), .(black, T160))) → UNIF_PAIRSK_IN_G(T160)
UNIF_PAIRSL_IN_GG(black, .(black, T161)) → U14_GG(T161, unif_pairsK_in_g(T161))
UNIF_PAIRSL_IN_GG(black, .(black, T161)) → UNIF_PAIRSK_IN_G(T161)
UNIF_PAIRSL_IN_GG(black, .(w(T166), T167)) → U15_GG(T166, T167, unif_pairsK_in_g(T167))
UNIF_PAIRSL_IN_GG(black, .(w(T166), T167)) → UNIF_PAIRSK_IN_G(T167)
UNIF_PAIRSL_IN_GG(w(T170), .(black, T171)) → U16_GG(T170, T171, unif_pairsK_in_g(T171))
UNIF_PAIRSL_IN_GG(w(T170), .(black, T171)) → UNIF_PAIRSK_IN_G(T171)
U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_GGGGGG(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → UNIF_LINESI_IN_GG(.(T110, T111), .(T112, T113))
U23_GGG(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_GGG(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
U23_GGG(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → UNIF_MATRXG_IN_GG(T65, T66)
SHAPESA_IN_GA(.(black, T194), T6) → U2_GA(T194, T6, pC_in_ga(T194, X245))
SHAPESA_IN_GA(.(black, T194), T6) → PC_IN_GA(T194, X245)
PC_IN_GA(T194, T195) → U27_GA(T194, T195, varmatE_in_ga(T194, T195))
PC_IN_GA(T194, T195) → VARMATE_IN_GA(T194, T195)
U27_GA(T194, T195, varmatE_out_ga(T194, T195)) → U28_GA(T194, T195, unif_matrxM_in_g(T195))
U27_GA(T194, T195, varmatE_out_ga(T194, T195)) → UNIF_MATRXM_IN_G(T195)
SHAPESA_IN_GA(.(white, T217), T6) → U3_GA(T217, T6, pD_in_gag(T217, X304, w(X303)))
SHAPESA_IN_GA(.(white, T217), T6) → PD_IN_GAG(T217, X304, w(X303))

The TRS R consists of the following rules:

shapesA_in_ga(.(T15, T16), T6) → U1_ga(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
pB_in_gaga(T15, T17, T16, X48) → U17_gaga(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
varmatE_in_ga([], []) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27), .(X77, X78)) → U4_ga(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
pF_in_gaga(T26, T28, T27, X78) → U21_gaga(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
varmatE_in_ga(.(black, T33), .(black, X93)) → U5_ga(T33, X93, varmatE_in_ga(T33, X93))
varmatE_in_ga(.(white, T36), .(w(X107), X108)) → U6_ga(T36, X107, X108, varmatE_in_ga(T36, X108))
U6_ga(T36, X107, X108, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w(X107), X108))
U5_ga(T33, X93, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U21_gaga(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U22_gaga(T26, T28, T27, X78, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)
U4_ga(T26, T27, X77, X78, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U17_gaga(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_gaga(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
pD_in_gag(T16, T37, T17) → U19_gag(T16, T37, T17, varmatE_in_ga(T16, T37))
U19_gag(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_gag(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
unif_matrxG_in_gg(T56, .(T57, T58)) → U7_gg(T56, T57, T58, pH_in_ggg(T56, T57, T58))
pH_in_ggg(T56, T65, T66) → U23_ggg(T56, T65, T66, unif_linesI_in_gg(T56, T65))
unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
U23_ggg(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_ggg(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
unif_matrxG_in_gg(T189, []) → unif_matrxG_out_gg(T189, [])
U24_ggg(T56, T65, T66, unif_matrxG_out_gg(T65, T66)) → pH_out_ggg(T56, T65, T66)
U7_gg(T56, T57, T58, pH_out_ggg(T56, T57, T58)) → unif_matrxG_out_gg(T56, .(T57, T58))
U20_gag(T16, T37, T17, unif_matrxG_out_gg(T17, T37)) → pD_out_gag(T16, T37, T17)
U18_gaga(T15, T17, T16, X48, pD_out_gag(T16, X48, T17)) → pB_out_gaga(T15, T17, T16, X48)
U1_ga(T15, T16, T6, pB_out_gaga(T15, X47, T16, X48)) → shapesA_out_ga(.(T15, T16), T6)
shapesA_in_ga(.(black, T194), T6) → U2_ga(T194, T6, pC_in_ga(T194, X245))
pC_in_ga(T194, T195) → U27_ga(T194, T195, varmatE_in_ga(T194, T195))
U27_ga(T194, T195, varmatE_out_ga(T194, T195)) → U28_ga(T194, T195, unif_matrxM_in_g(T195))
unif_matrxM_in_g([]) → unif_matrxM_out_g([])
U28_ga(T194, T195, unif_matrxM_out_g(T195)) → pC_out_ga(T194, T195)
U2_ga(T194, T6, pC_out_ga(T194, X245)) → shapesA_out_ga(.(black, T194), T6)
shapesA_in_ga(.(white, T217), T6) → U3_ga(T217, T6, pD_in_gag(T217, X304, w(X303)))
U3_ga(T217, T6, pD_out_gag(T217, X304, w(X303))) → shapesA_out_ga(.(white, T217), T6)

The argument filtering Pi contains the following mapping:
shapesA_in_ga(x1, x2) = shapesA_in_ga(x1)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x1, x2, x4)
pB_in_gaga(x1, x2, x3, x4) = pB_in_gaga(x1, x3)
U17_gaga(x1, x2, x3, x4, x5) = U17_gaga(x1, x3, x5)
varmatE_in_ga(x1, x2) = varmatE_in_ga(x1)
[] = []
varmatE_out_ga(x1, x2) = varmatE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x5)
pF_in_gaga(x1, x2, x3, x4) = pF_in_gaga(x1, x3)
U21_gaga(x1, x2, x3, x4, x5) = U21_gaga(x1, x3, x5)
black = black
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
white = white
U6_ga(x1, x2, x3, x4) = U6_ga(x1, x4)
w(x1) = w
U22_gaga(x1, x2, x3, x4, x5) = U22_gaga(x1, x2, x3, x5)
pF_out_gaga(x1, x2, x3, x4) = pF_out_gaga(x1, x2, x3, x4)
U18_gaga(x1, x2, x3, x4, x5) = U18_gaga(x1, x2, x3, x5)
pD_in_gag(x1, x2, x3) = pD_in_gag(x1, x3)
U19_gag(x1, x2, x3, x4) = U19_gag(x1, x3, x4)
U20_gag(x1, x2, x3, x4) = U20_gag(x1, x2, x3, x4)
unif_matrxG_in_gg(x1, x2) = unif_matrxG_in_gg(x1, x2)
U7_gg(x1, x2, x3, x4) = U7_gg(x1, x2, x3, x4)
pH_in_ggg(x1, x2, x3) = pH_in_ggg(x1, x2, x3)
U23_ggg(x1, x2, x3, x4) = U23_ggg(x1, x2, x3, x4)
unif_linesI_in_gg(x1, x2) = unif_linesI_in_gg(x1, x2)
U8_gg(x1, x2, x3, x4, x5, x6, x7) = U8_gg(x1, x2, x3, x4, x5, x6, x7)
pJ_in_gggggg(x1, x2, x3, x4, x5, x6) = pJ_in_gggggg(x1, x2, x3, x4, x5, x6)
U25_gggggg(x1, x2, x3, x4, x5, x6, x7) = U25_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_pairsL_in_gg(x1, x2) = unif_pairsL_in_gg(x1, x2)
U13_gg(x1, x2, x3) = U13_gg(x2, x3)
unif_pairsK_in_g(x1) = unif_pairsK_in_g(x1)
unif_pairsK_out_g(x1) = unif_pairsK_out_g(x1)
U9_g(x1, x2, x3) = U9_g(x2, x3)
U10_g(x1, x2) = U10_g(x1, x2)
U11_g(x1, x2, x3) = U11_g(x2, x3)
U12_g(x1, x2, x3) = U12_g(x2, x3)
unif_pairsL_out_gg(x1, x2) = unif_pairsL_out_gg(x1, x2)
U14_gg(x1, x2) = U14_gg(x1, x2)
U15_gg(x1, x2, x3) = U15_gg(x2, x3)
U16_gg(x1, x2, x3) = U16_gg(x2, x3)
U26_gggggg(x1, x2, x3, x4, x5, x6, x7) = U26_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_linesI_out_gg(x1, x2) = unif_linesI_out_gg(x1, x2)
pJ_out_gggggg(x1, x2, x3, x4, x5, x6) = pJ_out_gggggg(x1, x2, x3, x4, x5, x6)
U24_ggg(x1, x2, x3, x4) = U24_ggg(x1, x2, x3, x4)
unif_matrxG_out_gg(x1, x2) = unif_matrxG_out_gg(x1, x2)
pH_out_ggg(x1, x2, x3) = pH_out_ggg(x1, x2, x3)
pD_out_gag(x1, x2, x3) = pD_out_gag(x1, x2, x3)
pB_out_gaga(x1, x2, x3, x4) = pB_out_gaga(x1, x2, x3, x4)
shapesA_out_ga(x1, x2) = shapesA_out_ga(x1)
U2_ga(x1, x2, x3) = U2_ga(x1, x3)
pC_in_ga(x1, x2) = pC_in_ga(x1)
U27_ga(x1, x2, x3) = U27_ga(x1, x3)
U28_ga(x1, x2, x3) = U28_ga(x1, x2, x3)
unif_matrxM_in_g(x1) = unif_matrxM_in_g(x1)
unif_matrxM_out_g(x1) = unif_matrxM_out_g(x1)
pC_out_ga(x1, x2) = pC_out_ga(x1, x2)
U3_ga(x1, x2, x3) = U3_ga(x1, x3)
SHAPESA_IN_GA(x1, x2) = SHAPESA_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x1, x2, x4)
PB_IN_GAGA(x1, x2, x3, x4) = PB_IN_GAGA(x1, x3)
U17_GAGA(x1, x2, x3, x4, x5) = U17_GAGA(x1, x3, x5)
VARMATE_IN_GA(x1, x2) = VARMATE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x1, x2, x5)
PF_IN_GAGA(x1, x2, x3, x4) = PF_IN_GAGA(x1, x3)
U21_GAGA(x1, x2, x3, x4, x5) = U21_GAGA(x1, x3, x5)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
U6_GA(x1, x2, x3, x4) = U6_GA(x1, x4)
U22_GAGA(x1, x2, x3, x4, x5) = U22_GAGA(x1, x2, x3, x5)
U18_GAGA(x1, x2, x3, x4, x5) = U18_GAGA(x1, x2, x3, x5)
PD_IN_GAG(x1, x2, x3) = PD_IN_GAG(x1, x3)
U19_GAG(x1, x2, x3, x4) = U19_GAG(x1, x3, x4)
U20_GAG(x1, x2, x3, x4) = U20_GAG(x1, x2, x3, x4)
UNIF_MATRXG_IN_GG(x1, x2) = UNIF_MATRXG_IN_GG(x1, x2)
U7_GG(x1, x2, x3, x4) = U7_GG(x1, x2, x3, x4)
PH_IN_GGG(x1, x2, x3) = PH_IN_GGG(x1, x2, x3)
U23_GGG(x1, x2, x3, x4) = U23_GGG(x1, x2, x3, x4)
UNIF_LINESI_IN_GG(x1, x2) = UNIF_LINESI_IN_GG(x1, x2)
U8_GG(x1, x2, x3, x4, x5, x6, x7) = U8_GG(x1, x2, x3, x4, x5, x6, x7)
PJ_IN_GGGGGG(x1, x2, x3, x4, x5, x6) = PJ_IN_GGGGGG(x1, x2, x3, x4, x5, x6)
U25_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U25_GGGGGG(x1, x2, x3, x4, x5, x6, x7)
UNIF_PAIRSL_IN_GG(x1, x2) = UNIF_PAIRSL_IN_GG(x1, x2)
U13_GG(x1, x2, x3) = U13_GG(x2, x3)
UNIF_PAIRSK_IN_G(x1) = UNIF_PAIRSK_IN_G(x1)
U9_G(x1, x2, x3) = U9_G(x2, x3)
U10_G(x1, x2) = U10_G(x1, x2)
U11_G(x1, x2, x3) = U11_G(x2, x3)
U12_G(x1, x2, x3) = U12_G(x2, x3)
U14_GG(x1, x2) = U14_GG(x1, x2)
U15_GG(x1, x2, x3) = U15_GG(x2, x3)
U16_GG(x1, x2, x3) = U16_GG(x2, x3)
U26_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U26_GGGGGG(x1, x2, x3, x4, x5, x6, x7)
U24_GGG(x1, x2, x3, x4) = U24_GGG(x1, x2, x3, x4)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
PC_IN_GA(x1, x2) = PC_IN_GA(x1)
U27_GA(x1, x2, x3) = U27_GA(x1, x3)
U28_GA(x1, x2, x3) = U28_GA(x1, x2, x3)
UNIF_MATRXM_IN_G(x1) = UNIF_MATRXM_IN_G(x1)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)

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

(4) Obligation:

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

SHAPESA_IN_GA(.(T15, T16), T6) → U1_GA(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
SHAPESA_IN_GA(.(T15, T16), T6) → PB_IN_GAGA(T15, X47, T16, X48)
PB_IN_GAGA(T15, T17, T16, X48) → U17_GAGA(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
PB_IN_GAGA(T15, T17, T16, X48) → VARMATE_IN_GA(T15, T17)
VARMATE_IN_GA(.(T26, T27), .(X77, X78)) → U4_GA(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
VARMATE_IN_GA(.(T26, T27), .(X77, X78)) → PF_IN_GAGA(T26, X77, T27, X78)
PF_IN_GAGA(T26, T28, T27, X78) → U21_GAGA(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
PF_IN_GAGA(T26, T28, T27, X78) → VARMATE_IN_GA(T26, T28)
VARMATE_IN_GA(.(black, T33), .(black, X93)) → U5_GA(T33, X93, varmatE_in_ga(T33, X93))
VARMATE_IN_GA(.(black, T33), .(black, X93)) → VARMATE_IN_GA(T33, X93)
VARMATE_IN_GA(.(white, T36), .(w(X107), X108)) → U6_GA(T36, X107, X108, varmatE_in_ga(T36, X108))
VARMATE_IN_GA(.(white, T36), .(w(X107), X108)) → VARMATE_IN_GA(T36, X108)
U21_GAGA(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_GAGA(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U21_GAGA(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → VARMATE_IN_GA(T27, X78)
U17_GAGA(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_GAGA(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
U17_GAGA(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → PD_IN_GAG(T16, X48, T17)
PD_IN_GAG(T16, T37, T17) → U19_GAG(T16, T37, T17, varmatE_in_ga(T16, T37))
PD_IN_GAG(T16, T37, T17) → VARMATE_IN_GA(T16, T37)
U19_GAG(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_GAG(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
U19_GAG(T16, T37, T17, varmatE_out_ga(T16, T37)) → UNIF_MATRXG_IN_GG(T17, T37)
UNIF_MATRXG_IN_GG(T56, .(T57, T58)) → U7_GG(T56, T57, T58, pH_in_ggg(T56, T57, T58))
UNIF_MATRXG_IN_GG(T56, .(T57, T58)) → PH_IN_GGG(T56, T57, T58)
PH_IN_GGG(T56, T65, T66) → U23_GGG(T56, T65, T66, unif_linesI_in_gg(T56, T65))
PH_IN_GGG(T56, T65, T66) → UNIF_LINESI_IN_GG(T56, T65)
UNIF_LINESI_IN_GG(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_GG(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
UNIF_LINESI_IN_GG(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → PJ_IN_GGGGGG(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)
PJ_IN_GGGGGG(T103, T109, T110, T111, T112, T113) → U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
PJ_IN_GGGGGG(T103, T109, T110, T111, T112, T113) → UNIF_PAIRSL_IN_GG(T103, T109)
UNIF_PAIRSL_IN_GG(w(T130), .(w(T130), T131)) → U13_GG(T130, T131, unif_pairsK_in_g(T131))
UNIF_PAIRSL_IN_GG(w(T130), .(w(T130), T131)) → UNIF_PAIRSK_IN_G(T131)
UNIF_PAIRSK_IN_G(.(w(T148), .(w(T148), T149))) → U9_G(T148, T149, unif_pairsK_in_g(T149))
UNIF_PAIRSK_IN_G(.(w(T148), .(w(T148), T149))) → UNIF_PAIRSK_IN_G(T149)
UNIF_PAIRSK_IN_G(.(black, .(black, T150))) → U10_G(T150, unif_pairsK_in_g(T150))
UNIF_PAIRSK_IN_G(.(black, .(black, T150))) → UNIF_PAIRSK_IN_G(T150)
UNIF_PAIRSK_IN_G(.(black, .(w(T155), T156))) → U11_G(T155, T156, unif_pairsK_in_g(T156))
UNIF_PAIRSK_IN_G(.(black, .(w(T155), T156))) → UNIF_PAIRSK_IN_G(T156)
UNIF_PAIRSK_IN_G(.(w(T159), .(black, T160))) → U12_G(T159, T160, unif_pairsK_in_g(T160))
UNIF_PAIRSK_IN_G(.(w(T159), .(black, T160))) → UNIF_PAIRSK_IN_G(T160)
UNIF_PAIRSL_IN_GG(black, .(black, T161)) → U14_GG(T161, unif_pairsK_in_g(T161))
UNIF_PAIRSL_IN_GG(black, .(black, T161)) → UNIF_PAIRSK_IN_G(T161)
UNIF_PAIRSL_IN_GG(black, .(w(T166), T167)) → U15_GG(T166, T167, unif_pairsK_in_g(T167))
UNIF_PAIRSL_IN_GG(black, .(w(T166), T167)) → UNIF_PAIRSK_IN_G(T167)
UNIF_PAIRSL_IN_GG(w(T170), .(black, T171)) → U16_GG(T170, T171, unif_pairsK_in_g(T171))
UNIF_PAIRSL_IN_GG(w(T170), .(black, T171)) → UNIF_PAIRSK_IN_G(T171)
U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_GGGGGG(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → UNIF_LINESI_IN_GG(.(T110, T111), .(T112, T113))
U23_GGG(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_GGG(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
U23_GGG(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → UNIF_MATRXG_IN_GG(T65, T66)
SHAPESA_IN_GA(.(black, T194), T6) → U2_GA(T194, T6, pC_in_ga(T194, X245))
SHAPESA_IN_GA(.(black, T194), T6) → PC_IN_GA(T194, X245)
PC_IN_GA(T194, T195) → U27_GA(T194, T195, varmatE_in_ga(T194, T195))
PC_IN_GA(T194, T195) → VARMATE_IN_GA(T194, T195)
U27_GA(T194, T195, varmatE_out_ga(T194, T195)) → U28_GA(T194, T195, unif_matrxM_in_g(T195))
U27_GA(T194, T195, varmatE_out_ga(T194, T195)) → UNIF_MATRXM_IN_G(T195)
SHAPESA_IN_GA(.(white, T217), T6) → U3_GA(T217, T6, pD_in_gag(T217, X304, w(X303)))
SHAPESA_IN_GA(.(white, T217), T6) → PD_IN_GAG(T217, X304, w(X303))

The TRS R consists of the following rules:

shapesA_in_ga(.(T15, T16), T6) → U1_ga(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
pB_in_gaga(T15, T17, T16, X48) → U17_gaga(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
varmatE_in_ga([], []) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27), .(X77, X78)) → U4_ga(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
pF_in_gaga(T26, T28, T27, X78) → U21_gaga(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
varmatE_in_ga(.(black, T33), .(black, X93)) → U5_ga(T33, X93, varmatE_in_ga(T33, X93))
varmatE_in_ga(.(white, T36), .(w(X107), X108)) → U6_ga(T36, X107, X108, varmatE_in_ga(T36, X108))
U6_ga(T36, X107, X108, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w(X107), X108))
U5_ga(T33, X93, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U21_gaga(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U22_gaga(T26, T28, T27, X78, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)
U4_ga(T26, T27, X77, X78, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U17_gaga(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_gaga(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
pD_in_gag(T16, T37, T17) → U19_gag(T16, T37, T17, varmatE_in_ga(T16, T37))
U19_gag(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_gag(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
unif_matrxG_in_gg(T56, .(T57, T58)) → U7_gg(T56, T57, T58, pH_in_ggg(T56, T57, T58))
pH_in_ggg(T56, T65, T66) → U23_ggg(T56, T65, T66, unif_linesI_in_gg(T56, T65))
unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
U23_ggg(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_ggg(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
unif_matrxG_in_gg(T189, []) → unif_matrxG_out_gg(T189, [])
U24_ggg(T56, T65, T66, unif_matrxG_out_gg(T65, T66)) → pH_out_ggg(T56, T65, T66)
U7_gg(T56, T57, T58, pH_out_ggg(T56, T57, T58)) → unif_matrxG_out_gg(T56, .(T57, T58))
U20_gag(T16, T37, T17, unif_matrxG_out_gg(T17, T37)) → pD_out_gag(T16, T37, T17)
U18_gaga(T15, T17, T16, X48, pD_out_gag(T16, X48, T17)) → pB_out_gaga(T15, T17, T16, X48)
U1_ga(T15, T16, T6, pB_out_gaga(T15, X47, T16, X48)) → shapesA_out_ga(.(T15, T16), T6)
shapesA_in_ga(.(black, T194), T6) → U2_ga(T194, T6, pC_in_ga(T194, X245))
pC_in_ga(T194, T195) → U27_ga(T194, T195, varmatE_in_ga(T194, T195))
U27_ga(T194, T195, varmatE_out_ga(T194, T195)) → U28_ga(T194, T195, unif_matrxM_in_g(T195))
unif_matrxM_in_g([]) → unif_matrxM_out_g([])
U28_ga(T194, T195, unif_matrxM_out_g(T195)) → pC_out_ga(T194, T195)
U2_ga(T194, T6, pC_out_ga(T194, X245)) → shapesA_out_ga(.(black, T194), T6)
shapesA_in_ga(.(white, T217), T6) → U3_ga(T217, T6, pD_in_gag(T217, X304, w(X303)))
U3_ga(T217, T6, pD_out_gag(T217, X304, w(X303))) → shapesA_out_ga(.(white, T217), T6)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 40 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

UNIF_PAIRSK_IN_G(.(black, .(black, T150))) → UNIF_PAIRSK_IN_G(T150)
UNIF_PAIRSK_IN_G(.(w(T148), .(w(T148), T149))) → UNIF_PAIRSK_IN_G(T149)
UNIF_PAIRSK_IN_G(.(black, .(w(T155), T156))) → UNIF_PAIRSK_IN_G(T156)
UNIF_PAIRSK_IN_G(.(w(T159), .(black, T160))) → UNIF_PAIRSK_IN_G(T160)

The TRS R consists of the following rules:

shapesA_in_ga(.(T15, T16), T6) → U1_ga(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
pB_in_gaga(T15, T17, T16, X48) → U17_gaga(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
varmatE_in_ga([], []) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27), .(X77, X78)) → U4_ga(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
pF_in_gaga(T26, T28, T27, X78) → U21_gaga(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
varmatE_in_ga(.(black, T33), .(black, X93)) → U5_ga(T33, X93, varmatE_in_ga(T33, X93))
varmatE_in_ga(.(white, T36), .(w(X107), X108)) → U6_ga(T36, X107, X108, varmatE_in_ga(T36, X108))
U6_ga(T36, X107, X108, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w(X107), X108))
U5_ga(T33, X93, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U21_gaga(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U22_gaga(T26, T28, T27, X78, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)
U4_ga(T26, T27, X77, X78, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U17_gaga(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_gaga(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
pD_in_gag(T16, T37, T17) → U19_gag(T16, T37, T17, varmatE_in_ga(T16, T37))
U19_gag(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_gag(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
unif_matrxG_in_gg(T56, .(T57, T58)) → U7_gg(T56, T57, T58, pH_in_ggg(T56, T57, T58))
pH_in_ggg(T56, T65, T66) → U23_ggg(T56, T65, T66, unif_linesI_in_gg(T56, T65))
unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
U23_ggg(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_ggg(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
unif_matrxG_in_gg(T189, []) → unif_matrxG_out_gg(T189, [])
U24_ggg(T56, T65, T66, unif_matrxG_out_gg(T65, T66)) → pH_out_ggg(T56, T65, T66)
U7_gg(T56, T57, T58, pH_out_ggg(T56, T57, T58)) → unif_matrxG_out_gg(T56, .(T57, T58))
U20_gag(T16, T37, T17, unif_matrxG_out_gg(T17, T37)) → pD_out_gag(T16, T37, T17)
U18_gaga(T15, T17, T16, X48, pD_out_gag(T16, X48, T17)) → pB_out_gaga(T15, T17, T16, X48)
U1_ga(T15, T16, T6, pB_out_gaga(T15, X47, T16, X48)) → shapesA_out_ga(.(T15, T16), T6)
shapesA_in_ga(.(black, T194), T6) → U2_ga(T194, T6, pC_in_ga(T194, X245))
pC_in_ga(T194, T195) → U27_ga(T194, T195, varmatE_in_ga(T194, T195))
U27_ga(T194, T195, varmatE_out_ga(T194, T195)) → U28_ga(T194, T195, unif_matrxM_in_g(T195))
unif_matrxM_in_g([]) → unif_matrxM_out_g([])
U28_ga(T194, T195, unif_matrxM_out_g(T195)) → pC_out_ga(T194, T195)
U2_ga(T194, T6, pC_out_ga(T194, X245)) → shapesA_out_ga(.(black, T194), T6)
shapesA_in_ga(.(white, T217), T6) → U3_ga(T217, T6, pD_in_gag(T217, X304, w(X303)))
U3_ga(T217, T6, pD_out_gag(T217, X304, w(X303))) → shapesA_out_ga(.(white, T217), T6)

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

UNIF_PAIRSK_IN_G(.(black, .(black, T150))) → UNIF_PAIRSK_IN_G(T150)
UNIF_PAIRSK_IN_G(.(w(T148), .(w(T148), T149))) → UNIF_PAIRSK_IN_G(T149)
UNIF_PAIRSK_IN_G(.(black, .(w(T155), T156))) → UNIF_PAIRSK_IN_G(T156)
UNIF_PAIRSK_IN_G(.(w(T159), .(black, T160))) → UNIF_PAIRSK_IN_G(T160)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
black = black
w(x1) = w
UNIF_PAIRSK_IN_G(x1) = UNIF_PAIRSK_IN_G(x1)

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

UNIF_PAIRSK_IN_G(.(black, .(black, T150))) → UNIF_PAIRSK_IN_G(T150)
UNIF_PAIRSK_IN_G(.(w, .(w, T149))) → UNIF_PAIRSK_IN_G(T149)
UNIF_PAIRSK_IN_G(.(black, .(w, T156))) → UNIF_PAIRSK_IN_G(T156)
UNIF_PAIRSK_IN_G(.(w, .(black, T160))) → UNIF_PAIRSK_IN_G(T160)

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

(12) 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:

UNIF_PAIRSK_IN_G(.(black, .(black, T150))) → UNIF_PAIRSK_IN_G(T150)
The graph contains the following edges 1 > 1
UNIF_PAIRSK_IN_G(.(w, .(w, T149))) → UNIF_PAIRSK_IN_G(T149)
The graph contains the following edges 1 > 1
UNIF_PAIRSK_IN_G(.(black, .(w, T156))) → UNIF_PAIRSK_IN_G(T156)
The graph contains the following edges 1 > 1
UNIF_PAIRSK_IN_G(.(w, .(black, T160))) → UNIF_PAIRSK_IN_G(T160)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

UNIF_LINESI_IN_GG(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → PJ_IN_GGGGGG(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)
PJ_IN_GGGGGG(T103, T109, T110, T111, T112, T113) → U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → UNIF_LINESI_IN_GG(.(T110, T111), .(T112, T113))

The TRS R consists of the following rules:

shapesA_in_ga(.(T15, T16), T6) → U1_ga(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
pB_in_gaga(T15, T17, T16, X48) → U17_gaga(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
varmatE_in_ga([], []) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27), .(X77, X78)) → U4_ga(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
pF_in_gaga(T26, T28, T27, X78) → U21_gaga(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
varmatE_in_ga(.(black, T33), .(black, X93)) → U5_ga(T33, X93, varmatE_in_ga(T33, X93))
varmatE_in_ga(.(white, T36), .(w(X107), X108)) → U6_ga(T36, X107, X108, varmatE_in_ga(T36, X108))
U6_ga(T36, X107, X108, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w(X107), X108))
U5_ga(T33, X93, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U21_gaga(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U22_gaga(T26, T28, T27, X78, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)
U4_ga(T26, T27, X77, X78, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U17_gaga(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_gaga(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
pD_in_gag(T16, T37, T17) → U19_gag(T16, T37, T17, varmatE_in_ga(T16, T37))
U19_gag(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_gag(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
unif_matrxG_in_gg(T56, .(T57, T58)) → U7_gg(T56, T57, T58, pH_in_ggg(T56, T57, T58))
pH_in_ggg(T56, T65, T66) → U23_ggg(T56, T65, T66, unif_linesI_in_gg(T56, T65))
unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
U23_ggg(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_ggg(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
unif_matrxG_in_gg(T189, []) → unif_matrxG_out_gg(T189, [])
U24_ggg(T56, T65, T66, unif_matrxG_out_gg(T65, T66)) → pH_out_ggg(T56, T65, T66)
U7_gg(T56, T57, T58, pH_out_ggg(T56, T57, T58)) → unif_matrxG_out_gg(T56, .(T57, T58))
U20_gag(T16, T37, T17, unif_matrxG_out_gg(T17, T37)) → pD_out_gag(T16, T37, T17)
U18_gaga(T15, T17, T16, X48, pD_out_gag(T16, X48, T17)) → pB_out_gaga(T15, T17, T16, X48)
U1_ga(T15, T16, T6, pB_out_gaga(T15, X47, T16, X48)) → shapesA_out_ga(.(T15, T16), T6)
shapesA_in_ga(.(black, T194), T6) → U2_ga(T194, T6, pC_in_ga(T194, X245))
pC_in_ga(T194, T195) → U27_ga(T194, T195, varmatE_in_ga(T194, T195))
U27_ga(T194, T195, varmatE_out_ga(T194, T195)) → U28_ga(T194, T195, unif_matrxM_in_g(T195))
unif_matrxM_in_g([]) → unif_matrxM_out_g([])
U28_ga(T194, T195, unif_matrxM_out_g(T195)) → pC_out_ga(T194, T195)
U2_ga(T194, T6, pC_out_ga(T194, X245)) → shapesA_out_ga(.(black, T194), T6)
shapesA_in_ga(.(white, T217), T6) → U3_ga(T217, T6, pD_in_gag(T217, X304, w(X303)))
U3_ga(T217, T6, pD_out_gag(T217, X304, w(X303))) → shapesA_out_ga(.(white, T217), T6)

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

UNIF_LINESI_IN_GG(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → PJ_IN_GGGGGG(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)
PJ_IN_GGGGGG(T103, T109, T110, T111, T112, T113) → U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → UNIF_LINESI_IN_GG(.(T110, T111), .(T112, T113))

The TRS R consists of the following rules:

unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
[] = []
black = black
w(x1) = w
unif_pairsL_in_gg(x1, x2) = unif_pairsL_in_gg(x1, x2)
U13_gg(x1, x2, x3) = U13_gg(x2, x3)
unif_pairsK_in_g(x1) = unif_pairsK_in_g(x1)
unif_pairsK_out_g(x1) = unif_pairsK_out_g(x1)
U9_g(x1, x2, x3) = U9_g(x2, x3)
U10_g(x1, x2) = U10_g(x1, x2)
U11_g(x1, x2, x3) = U11_g(x2, x3)
U12_g(x1, x2, x3) = U12_g(x2, x3)
unif_pairsL_out_gg(x1, x2) = unif_pairsL_out_gg(x1, x2)
U14_gg(x1, x2) = U14_gg(x1, x2)
U15_gg(x1, x2, x3) = U15_gg(x2, x3)
U16_gg(x1, x2, x3) = U16_gg(x2, x3)
UNIF_LINESI_IN_GG(x1, x2) = UNIF_LINESI_IN_GG(x1, x2)
PJ_IN_GGGGGG(x1, x2, x3, x4, x5, x6) = PJ_IN_GGGGGG(x1, x2, x3, x4, x5, x6)
U25_GGGGGG(x1, x2, x3, x4, x5, x6, x7) = U25_GGGGGG(x1, x2, x3, x4, x5, x6, x7)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

UNIF_LINESI_IN_GG(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → PJ_IN_GGGGGG(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)
PJ_IN_GGGGGG(T103, T109, T110, T111, T112, T113) → U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → UNIF_LINESI_IN_GG(.(T110, T111), .(T112, T113))

The TRS R consists of the following rules:

unif_pairsL_in_gg(w, .(w, T131)) → U13_gg(T131, unif_pairsK_in_g(T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
unif_pairsL_in_gg(black, .(w, T167)) → U15_gg(T167, unif_pairsK_in_g(T167))
unif_pairsL_in_gg(w, .(black, T171)) → U16_gg(T171, unif_pairsK_in_g(T171))
U13_gg(T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w, .(w, T131))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
U15_gg(T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w, T167))
U16_gg(T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w, .(black, T171))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w, .(w, T149))) → U9_g(T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w, T156))) → U11_g(T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w, .(black, T160))) → U12_g(T160, unif_pairsK_in_g(T160))
U9_g(T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w, .(w, T149)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U11_g(T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w, T156)))
U12_g(T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w, .(black, T160)))

The set Q consists of the following terms:

unif_pairsL_in_gg(x0, x1)
U13_gg(x0, x1)
U14_gg(x0, x1)
U15_gg(x0, x1)
U16_gg(x0, x1)
unif_pairsK_in_g(x0)
U9_g(x0, x1)
U10_g(x0, x1)
U11_g(x0, x1)
U12_g(x0, x1)

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

UNIF_LINESI_IN_GG(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → PJ_IN_GGGGGG(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(PJ_IN_GGGGGG(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₆
POL(U10_g(x₁, x₂)) = 0
POL(U11_g(x₁, x₂)) = 0
POL(U12_g(x₁, x₂)) = 0
POL(U13_gg(x₁, x₂)) = 0
POL(U14_gg(x₁, x₂)) = 0
POL(U15_gg(x₁, x₂)) = 0
POL(U16_gg(x₁, x₂)) = 0
POL(U25_GGGGGG(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 1 + x₆
POL(U9_g(x₁, x₂)) = 0
POL(UNIF_LINESI_IN_GG(x₁, x₂)) = x₂
POL([]) = 0
POL(black) = 0
POL(unif_pairsK_in_g(x₁)) = 0
POL(unif_pairsK_out_g(x₁)) = 0
POL(unif_pairsL_in_gg(x₁, x₂)) = 0
POL(unif_pairsL_out_gg(x₁, x₂)) = 0
POL(w) = 0

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(20) Obligation:

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

PJ_IN_GGGGGG(T103, T109, T110, T111, T112, T113) → U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
U25_GGGGGG(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → UNIF_LINESI_IN_GG(.(T110, T111), .(T112, T113))

The TRS R consists of the following rules:

unif_pairsL_in_gg(w, .(w, T131)) → U13_gg(T131, unif_pairsK_in_g(T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
unif_pairsL_in_gg(black, .(w, T167)) → U15_gg(T167, unif_pairsK_in_g(T167))
unif_pairsL_in_gg(w, .(black, T171)) → U16_gg(T171, unif_pairsK_in_g(T171))
U13_gg(T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w, .(w, T131))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
U15_gg(T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w, T167))
U16_gg(T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w, .(black, T171))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w, .(w, T149))) → U9_g(T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w, T156))) → U11_g(T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w, .(black, T160))) → U12_g(T160, unif_pairsK_in_g(T160))
U9_g(T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w, .(w, T149)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U11_g(T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w, T156)))
U12_g(T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w, .(black, T160)))

The set Q consists of the following terms:

unif_pairsL_in_gg(x0, x1)
U13_gg(x0, x1)
U14_gg(x0, x1)
U15_gg(x0, x1)
U16_gg(x0, x1)
unif_pairsK_in_g(x0)
U9_g(x0, x1)
U10_g(x0, x1)
U11_g(x0, x1)
U12_g(x0, x1)

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

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(22) TRUE

(23) Obligation:

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

UNIF_MATRXG_IN_GG(T56, .(T57, T58)) → PH_IN_GGG(T56, T57, T58)
PH_IN_GGG(T56, T65, T66) → U23_GGG(T56, T65, T66, unif_linesI_in_gg(T56, T65))
U23_GGG(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → UNIF_MATRXG_IN_GG(T65, T66)

The TRS R consists of the following rules:

shapesA_in_ga(.(T15, T16), T6) → U1_ga(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
pB_in_gaga(T15, T17, T16, X48) → U17_gaga(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
varmatE_in_ga([], []) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27), .(X77, X78)) → U4_ga(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
pF_in_gaga(T26, T28, T27, X78) → U21_gaga(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
varmatE_in_ga(.(black, T33), .(black, X93)) → U5_ga(T33, X93, varmatE_in_ga(T33, X93))
varmatE_in_ga(.(white, T36), .(w(X107), X108)) → U6_ga(T36, X107, X108, varmatE_in_ga(T36, X108))
U6_ga(T36, X107, X108, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w(X107), X108))
U5_ga(T33, X93, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U21_gaga(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U22_gaga(T26, T28, T27, X78, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)
U4_ga(T26, T27, X77, X78, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U17_gaga(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_gaga(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
pD_in_gag(T16, T37, T17) → U19_gag(T16, T37, T17, varmatE_in_ga(T16, T37))
U19_gag(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_gag(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
unif_matrxG_in_gg(T56, .(T57, T58)) → U7_gg(T56, T57, T58, pH_in_ggg(T56, T57, T58))
pH_in_ggg(T56, T65, T66) → U23_ggg(T56, T65, T66, unif_linesI_in_gg(T56, T65))
unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
U23_ggg(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_ggg(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
unif_matrxG_in_gg(T189, []) → unif_matrxG_out_gg(T189, [])
U24_ggg(T56, T65, T66, unif_matrxG_out_gg(T65, T66)) → pH_out_ggg(T56, T65, T66)
U7_gg(T56, T57, T58, pH_out_ggg(T56, T57, T58)) → unif_matrxG_out_gg(T56, .(T57, T58))
U20_gag(T16, T37, T17, unif_matrxG_out_gg(T17, T37)) → pD_out_gag(T16, T37, T17)
U18_gaga(T15, T17, T16, X48, pD_out_gag(T16, X48, T17)) → pB_out_gaga(T15, T17, T16, X48)
U1_ga(T15, T16, T6, pB_out_gaga(T15, X47, T16, X48)) → shapesA_out_ga(.(T15, T16), T6)
shapesA_in_ga(.(black, T194), T6) → U2_ga(T194, T6, pC_in_ga(T194, X245))
pC_in_ga(T194, T195) → U27_ga(T194, T195, varmatE_in_ga(T194, T195))
U27_ga(T194, T195, varmatE_out_ga(T194, T195)) → U28_ga(T194, T195, unif_matrxM_in_g(T195))
unif_matrxM_in_g([]) → unif_matrxM_out_g([])
U28_ga(T194, T195, unif_matrxM_out_g(T195)) → pC_out_ga(T194, T195)
U2_ga(T194, T6, pC_out_ga(T194, X245)) → shapesA_out_ga(.(black, T194), T6)
shapesA_in_ga(.(white, T217), T6) → U3_ga(T217, T6, pD_in_gag(T217, X304, w(X303)))
U3_ga(T217, T6, pD_out_gag(T217, X304, w(X303))) → shapesA_out_ga(.(white, T217), T6)

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

UNIF_MATRXG_IN_GG(T56, .(T57, T58)) → PH_IN_GGG(T56, T57, T58)
PH_IN_GGG(T56, T65, T66) → U23_GGG(T56, T65, T66, unif_linesI_in_gg(T56, T65))
U23_GGG(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → UNIF_MATRXG_IN_GG(T65, T66)

The TRS R consists of the following rules:

unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
[] = []
black = black
w(x1) = w
unif_linesI_in_gg(x1, x2) = unif_linesI_in_gg(x1, x2)
U8_gg(x1, x2, x3, x4, x5, x6, x7) = U8_gg(x1, x2, x3, x4, x5, x6, x7)
pJ_in_gggggg(x1, x2, x3, x4, x5, x6) = pJ_in_gggggg(x1, x2, x3, x4, x5, x6)
U25_gggggg(x1, x2, x3, x4, x5, x6, x7) = U25_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_pairsL_in_gg(x1, x2) = unif_pairsL_in_gg(x1, x2)
U13_gg(x1, x2, x3) = U13_gg(x2, x3)
unif_pairsK_in_g(x1) = unif_pairsK_in_g(x1)
unif_pairsK_out_g(x1) = unif_pairsK_out_g(x1)
U9_g(x1, x2, x3) = U9_g(x2, x3)
U10_g(x1, x2) = U10_g(x1, x2)
U11_g(x1, x2, x3) = U11_g(x2, x3)
U12_g(x1, x2, x3) = U12_g(x2, x3)
unif_pairsL_out_gg(x1, x2) = unif_pairsL_out_gg(x1, x2)
U14_gg(x1, x2) = U14_gg(x1, x2)
U15_gg(x1, x2, x3) = U15_gg(x2, x3)
U16_gg(x1, x2, x3) = U16_gg(x2, x3)
U26_gggggg(x1, x2, x3, x4, x5, x6, x7) = U26_gggggg(x1, x2, x3, x4, x5, x6, x7)
unif_linesI_out_gg(x1, x2) = unif_linesI_out_gg(x1, x2)
pJ_out_gggggg(x1, x2, x3, x4, x5, x6) = pJ_out_gggggg(x1, x2, x3, x4, x5, x6)
UNIF_MATRXG_IN_GG(x1, x2) = UNIF_MATRXG_IN_GG(x1, x2)
PH_IN_GGG(x1, x2, x3) = PH_IN_GGG(x1, x2, x3)
U23_GGG(x1, x2, x3, x4) = U23_GGG(x1, x2, x3, x4)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

UNIF_MATRXG_IN_GG(T56, .(T57, T58)) → PH_IN_GGG(T56, T57, T58)
PH_IN_GGG(T56, T65, T66) → U23_GGG(T56, T65, T66, unif_linesI_in_gg(T56, T65))
U23_GGG(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → UNIF_MATRXG_IN_GG(T65, T66)

The TRS R consists of the following rules:

unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_pairsL_in_gg(w, .(w, T131)) → U13_gg(T131, unif_pairsK_in_g(T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
unif_pairsL_in_gg(black, .(w, T167)) → U15_gg(T167, unif_pairsK_in_g(T167))
unif_pairsL_in_gg(w, .(black, T171)) → U16_gg(T171, unif_pairsK_in_g(T171))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U13_gg(T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w, .(w, T131))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
U15_gg(T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w, T167))
U16_gg(T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w, .(black, T171))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w, .(w, T149))) → U9_g(T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w, T156))) → U11_g(T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w, .(black, T160))) → U12_g(T160, unif_pairsK_in_g(T160))
U9_g(T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w, .(w, T149)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U11_g(T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w, T156)))
U12_g(T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w, .(black, T160)))

The set Q consists of the following terms:

unif_linesI_in_gg(x0, x1)
U8_gg(x0, x1, x2, x3, x4, x5, x6)
pJ_in_gggggg(x0, x1, x2, x3, x4, x5)
U25_gggggg(x0, x1, x2, x3, x4, x5, x6)
unif_pairsL_in_gg(x0, x1)
U26_gggggg(x0, x1, x2, x3, x4, x5, x6)
U13_gg(x0, x1)
U14_gg(x0, x1)
U15_gg(x0, x1)
U16_gg(x0, x1)
unif_pairsK_in_g(x0)
U9_g(x0, x1)
U10_g(x0, x1)
U11_g(x0, x1)
U12_g(x0, x1)

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

(28) 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:

PH_IN_GGG(T56, T65, T66) → U23_GGG(T56, T65, T66, unif_linesI_in_gg(T56, T65))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U23_GGG(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → UNIF_MATRXG_IN_GG(T65, T66)
The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2
UNIF_MATRXG_IN_GG(T56, .(T57, T58)) → PH_IN_GGG(T56, T57, T58)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(29) YES

(30) Obligation:

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

VARMATE_IN_GA(.(T26, T27), .(X77, X78)) → PF_IN_GAGA(T26, X77, T27, X78)
PF_IN_GAGA(T26, T28, T27, X78) → U21_GAGA(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
U21_GAGA(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → VARMATE_IN_GA(T27, X78)
VARMATE_IN_GA(.(black, T33), .(black, X93)) → VARMATE_IN_GA(T33, X93)
VARMATE_IN_GA(.(white, T36), .(w(X107), X108)) → VARMATE_IN_GA(T36, X108)
PF_IN_GAGA(T26, T28, T27, X78) → VARMATE_IN_GA(T26, T28)

The TRS R consists of the following rules:

shapesA_in_ga(.(T15, T16), T6) → U1_ga(T15, T16, T6, pB_in_gaga(T15, X47, T16, X48))
pB_in_gaga(T15, T17, T16, X48) → U17_gaga(T15, T17, T16, X48, varmatE_in_ga(T15, T17))
varmatE_in_ga([], []) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27), .(X77, X78)) → U4_ga(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
pF_in_gaga(T26, T28, T27, X78) → U21_gaga(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
varmatE_in_ga(.(black, T33), .(black, X93)) → U5_ga(T33, X93, varmatE_in_ga(T33, X93))
varmatE_in_ga(.(white, T36), .(w(X107), X108)) → U6_ga(T36, X107, X108, varmatE_in_ga(T36, X108))
U6_ga(T36, X107, X108, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w(X107), X108))
U5_ga(T33, X93, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U21_gaga(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U22_gaga(T26, T28, T27, X78, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)
U4_ga(T26, T27, X77, X78, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U17_gaga(T15, T17, T16, X48, varmatE_out_ga(T15, T17)) → U18_gaga(T15, T17, T16, X48, pD_in_gag(T16, X48, T17))
pD_in_gag(T16, T37, T17) → U19_gag(T16, T37, T17, varmatE_in_ga(T16, T37))
U19_gag(T16, T37, T17, varmatE_out_ga(T16, T37)) → U20_gag(T16, T37, T17, unif_matrxG_in_gg(T17, T37))
unif_matrxG_in_gg(T56, .(T57, T58)) → U7_gg(T56, T57, T58, pH_in_ggg(T56, T57, T58))
pH_in_ggg(T56, T65, T66) → U23_ggg(T56, T65, T66, unif_linesI_in_gg(T56, T65))
unif_linesI_in_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108))) → U8_gg(T103, T104, T107, T105, T106, T108, pJ_in_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108))
pJ_in_gggggg(T103, T109, T110, T111, T112, T113) → U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_in_gg(T103, T109))
unif_pairsL_in_gg(w(T130), .(w(T130), T131)) → U13_gg(T130, T131, unif_pairsK_in_g(T131))
unif_pairsK_in_g([]) → unif_pairsK_out_g([])
unif_pairsK_in_g(.(w(T148), .(w(T148), T149))) → U9_g(T148, T149, unif_pairsK_in_g(T149))
unif_pairsK_in_g(.(black, .(black, T150))) → U10_g(T150, unif_pairsK_in_g(T150))
unif_pairsK_in_g(.(black, .(w(T155), T156))) → U11_g(T155, T156, unif_pairsK_in_g(T156))
unif_pairsK_in_g(.(w(T159), .(black, T160))) → U12_g(T159, T160, unif_pairsK_in_g(T160))
U12_g(T159, T160, unif_pairsK_out_g(T160)) → unif_pairsK_out_g(.(w(T159), .(black, T160)))
U11_g(T155, T156, unif_pairsK_out_g(T156)) → unif_pairsK_out_g(.(black, .(w(T155), T156)))
U10_g(T150, unif_pairsK_out_g(T150)) → unif_pairsK_out_g(.(black, .(black, T150)))
U9_g(T148, T149, unif_pairsK_out_g(T149)) → unif_pairsK_out_g(.(w(T148), .(w(T148), T149)))
U13_gg(T130, T131, unif_pairsK_out_g(T131)) → unif_pairsL_out_gg(w(T130), .(w(T130), T131))
unif_pairsL_in_gg(black, .(black, T161)) → U14_gg(T161, unif_pairsK_in_g(T161))
U14_gg(T161, unif_pairsK_out_g(T161)) → unif_pairsL_out_gg(black, .(black, T161))
unif_pairsL_in_gg(black, .(w(T166), T167)) → U15_gg(T166, T167, unif_pairsK_in_g(T167))
U15_gg(T166, T167, unif_pairsK_out_g(T167)) → unif_pairsL_out_gg(black, .(w(T166), T167))
unif_pairsL_in_gg(w(T170), .(black, T171)) → U16_gg(T170, T171, unif_pairsK_in_g(T171))
U16_gg(T170, T171, unif_pairsK_out_g(T171)) → unif_pairsL_out_gg(w(T170), .(black, T171))
U25_gggggg(T103, T109, T110, T111, T112, T113, unif_pairsL_out_gg(T103, T109)) → U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_in_gg(.(T110, T111), .(T112, T113)))
unif_linesI_in_gg(.(T182, []), .(T183, [])) → unif_linesI_out_gg(.(T182, []), .(T183, []))
U26_gggggg(T103, T109, T110, T111, T112, T113, unif_linesI_out_gg(.(T110, T111), .(T112, T113))) → pJ_out_gggggg(T103, T109, T110, T111, T112, T113)
U8_gg(T103, T104, T107, T105, T106, T108, pJ_out_gggggg(T103, .(T104, .(T105, .(T106, .(T103, .(T105, .(T104, .(T106, .(T103, .(T106, .(T104, .(T105, []))))))))))), T104, T107, T106, T108)) → unif_linesI_out_gg(.(T103, .(T104, T107)), .(T105, .(T106, T108)))
U23_ggg(T56, T65, T66, unif_linesI_out_gg(T56, T65)) → U24_ggg(T56, T65, T66, unif_matrxG_in_gg(T65, T66))
unif_matrxG_in_gg(T189, []) → unif_matrxG_out_gg(T189, [])
U24_ggg(T56, T65, T66, unif_matrxG_out_gg(T65, T66)) → pH_out_ggg(T56, T65, T66)
U7_gg(T56, T57, T58, pH_out_ggg(T56, T57, T58)) → unif_matrxG_out_gg(T56, .(T57, T58))
U20_gag(T16, T37, T17, unif_matrxG_out_gg(T17, T37)) → pD_out_gag(T16, T37, T17)
U18_gaga(T15, T17, T16, X48, pD_out_gag(T16, X48, T17)) → pB_out_gaga(T15, T17, T16, X48)
U1_ga(T15, T16, T6, pB_out_gaga(T15, X47, T16, X48)) → shapesA_out_ga(.(T15, T16), T6)
shapesA_in_ga(.(black, T194), T6) → U2_ga(T194, T6, pC_in_ga(T194, X245))
pC_in_ga(T194, T195) → U27_ga(T194, T195, varmatE_in_ga(T194, T195))
U27_ga(T194, T195, varmatE_out_ga(T194, T195)) → U28_ga(T194, T195, unif_matrxM_in_g(T195))
unif_matrxM_in_g([]) → unif_matrxM_out_g([])
U28_ga(T194, T195, unif_matrxM_out_g(T195)) → pC_out_ga(T194, T195)
U2_ga(T194, T6, pC_out_ga(T194, X245)) → shapesA_out_ga(.(black, T194), T6)
shapesA_in_ga(.(white, T217), T6) → U3_ga(T217, T6, pD_in_gag(T217, X304, w(X303)))
U3_ga(T217, T6, pD_out_gag(T217, X304, w(X303))) → shapesA_out_ga(.(white, T217), T6)

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

VARMATE_IN_GA(.(T26, T27), .(X77, X78)) → PF_IN_GAGA(T26, X77, T27, X78)
PF_IN_GAGA(T26, T28, T27, X78) → U21_GAGA(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
U21_GAGA(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → VARMATE_IN_GA(T27, X78)
VARMATE_IN_GA(.(black, T33), .(black, X93)) → VARMATE_IN_GA(T33, X93)
VARMATE_IN_GA(.(white, T36), .(w(X107), X108)) → VARMATE_IN_GA(T36, X108)
PF_IN_GAGA(T26, T28, T27, X78) → VARMATE_IN_GA(T26, T28)

The TRS R consists of the following rules:

varmatE_in_ga([], []) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27), .(X77, X78)) → U4_ga(T26, T27, X77, X78, pF_in_gaga(T26, X77, T27, X78))
varmatE_in_ga(.(black, T33), .(black, X93)) → U5_ga(T33, X93, varmatE_in_ga(T33, X93))
varmatE_in_ga(.(white, T36), .(w(X107), X108)) → U6_ga(T36, X107, X108, varmatE_in_ga(T36, X108))
U4_ga(T26, T27, X77, X78, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U5_ga(T33, X93, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U6_ga(T36, X107, X108, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w(X107), X108))
pF_in_gaga(T26, T28, T27, X78) → U21_gaga(T26, T28, T27, X78, varmatE_in_ga(T26, T28))
U21_gaga(T26, T28, T27, X78, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, X78, varmatE_in_ga(T27, X78))
U22_gaga(T26, T28, T27, X78, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
varmatE_in_ga(x1, x2) = varmatE_in_ga(x1)
[] = []
varmatE_out_ga(x1, x2) = varmatE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x5)
pF_in_gaga(x1, x2, x3, x4) = pF_in_gaga(x1, x3)
U21_gaga(x1, x2, x3, x4, x5) = U21_gaga(x1, x3, x5)
black = black
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
white = white
U6_ga(x1, x2, x3, x4) = U6_ga(x1, x4)
w(x1) = w
U22_gaga(x1, x2, x3, x4, x5) = U22_gaga(x1, x2, x3, x5)
pF_out_gaga(x1, x2, x3, x4) = pF_out_gaga(x1, x2, x3, x4)
VARMATE_IN_GA(x1, x2) = VARMATE_IN_GA(x1)
PF_IN_GAGA(x1, x2, x3, x4) = PF_IN_GAGA(x1, x3)
U21_GAGA(x1, x2, x3, x4, x5) = U21_GAGA(x1, x3, x5)

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

VARMATE_IN_GA(.(T26, T27)) → PF_IN_GAGA(T26, T27)
PF_IN_GAGA(T26, T27) → U21_GAGA(T26, T27, varmatE_in_ga(T26))
U21_GAGA(T26, T27, varmatE_out_ga(T26, T28)) → VARMATE_IN_GA(T27)
VARMATE_IN_GA(.(black, T33)) → VARMATE_IN_GA(T33)
VARMATE_IN_GA(.(white, T36)) → VARMATE_IN_GA(T36)
PF_IN_GAGA(T26, T27) → VARMATE_IN_GA(T26)

The TRS R consists of the following rules:

varmatE_in_ga([]) → varmatE_out_ga([], [])
varmatE_in_ga(.(T26, T27)) → U4_ga(T26, T27, pF_in_gaga(T26, T27))
varmatE_in_ga(.(black, T33)) → U5_ga(T33, varmatE_in_ga(T33))
varmatE_in_ga(.(white, T36)) → U6_ga(T36, varmatE_in_ga(T36))
U4_ga(T26, T27, pF_out_gaga(T26, X77, T27, X78)) → varmatE_out_ga(.(T26, T27), .(X77, X78))
U5_ga(T33, varmatE_out_ga(T33, X93)) → varmatE_out_ga(.(black, T33), .(black, X93))
U6_ga(T36, varmatE_out_ga(T36, X108)) → varmatE_out_ga(.(white, T36), .(w, X108))
pF_in_gaga(T26, T27) → U21_gaga(T26, T27, varmatE_in_ga(T26))
U21_gaga(T26, T27, varmatE_out_ga(T26, T28)) → U22_gaga(T26, T28, T27, varmatE_in_ga(T27))
U22_gaga(T26, T28, T27, varmatE_out_ga(T27, X78)) → pF_out_gaga(T26, T28, T27, X78)

The set Q consists of the following terms:

varmatE_in_ga(x0)
U4_ga(x0, x1, x2)
U5_ga(x0, x1)
U6_ga(x0, x1)
pF_in_gaga(x0, x1)
U21_gaga(x0, x1, x2)
U22_gaga(x0, x1, x2, x3)

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

(35) 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:

PF_IN_GAGA(T26, T27) → VARMATE_IN_GA(T26)
The graph contains the following edges 1 >= 1
PF_IN_GAGA(T26, T27) → U21_GAGA(T26, T27, varmatE_in_ga(T26))
The graph contains the following edges 1 >= 1, 2 >= 2
VARMATE_IN_GA(.(T26, T27)) → PF_IN_GAGA(T26, T27)
The graph contains the following edges 1 > 1, 1 > 2
U21_GAGA(T26, T27, varmatE_out_ga(T26, T28)) → VARMATE_IN_GA(T27)
The graph contains the following edges 2 >= 1
VARMATE_IN_GA(.(black, T33)) → VARMATE_IN_GA(T33)
The graph contains the following edges 1 > 1
VARMATE_IN_GA(.(white, T36)) → VARMATE_IN_GA(T36)
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPOrderProof (EQUIVALENT transformation)

(20) Obligation:

(21) DependencyGraphProof (EQUIVALENT transformation)

(22) TRUE

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) QDPSizeChangeProof (EQUIVALENT transformation)

(29) YES

(30) Obligation:

(31) UsableRulesProof (EQUIVALENT transformation)

(32) Obligation:

(33) PiDPToQDPProof (SOUND transformation)

(34) Obligation:

(35) QDPSizeChangeProof (EQUIVALENT transformation)

(36) YES