Left Termination proof of /tmp/tmp1nPR5u/lessleaves.pl

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇐)

        ↳11 QDP

        ↳12 NonTerminationProof (⇔)

        ↳13 NO

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇐)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇐)

        ↳25 QDP

        ↳26 NonTerminationProof (⇔)

        ↳27 NO

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇐)

        ↳32 QDP

        ↳33 NonTerminationProof (⇔)

        ↳34 NO

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇐)

        ↳39 QDP

        ↳40 MRRProof (⇔)

        ↳41 QDP

        ↳42 UsableRulesProof (⇔)

        ↳43 QDP

        ↳44 QReductionProof (⇔)

        ↳45 QDP

        ↳46 Narrowing (⇐)

        ↳47 QDP

        ↳48 Narrowing (⇐)

        ↳49 QDP

        ↳50 NonTerminationProof (⇔)

        ↳51 NO

    ↳52 PiDP

        ↳53 UsableRulesProof (⇔)

        ↳54 PiDP

        ↳55 PiDPToQDPProof (⇐)

        ↳56 QDP

        ↳57 NonTerminationProof (⇔)

        ↳58 NO

    ↳59 PiDP

        ↳60 UsableRulesProof (⇔)

        ↳61 PiDP

        ↳62 PiDPToQDPProof (⇐)

        ↳63 QDP

        ↳64 QDPSizeChangeProof (⇔)

        ↳65 YES

(0) Obligation:

Clauses:

lessleaves(nil, cons(X1, X2)).
lessleaves(cons(U, V), cons(W, Z)) :- ','(app(U, V, U1), ','(app(W, Z, W1), lessleaves(U1, W1))).
app(nil, Y, Z) :- ','(!, eq(Y, Z)).
app(X, Y, cons(U, Z)) :- ','(head(X, U), ','(tail(X, V), app(V, Y, Z))).
head([], X3).
head(.(X, X4), X).
tail([], []).
tail(.(X5, X), X).
eq(X, X).

Queries:

lessleaves(g,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: lessleaves(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: lessleaves(T1, T2), SCOPE: 1, CLAUSE: 0 | lessleaves(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | lessleaves(nil, cons(T5, T6)), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: lessleaves(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nlessleaves(T1, T2) !=? lessleaves(nil, cons(X8, X9))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: lessleaves(nil, cons(T5, T6)), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(app(T11, T12, X24), ','(app(T13, T14, X25), lessleaves(X24, X25)))\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX24 is free; \nX25 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(app(T11, T12, X24), ','(app(T13, T14, X25), lessleaves(X24, X25))), SCOPE: 2, CLAUSE: 2 | ','(app(T11, T12, X24), ','(app(T13, T14, X25), lessleaves(X24, X25))), SCOPE: 2, CLAUSE: 3\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX24 is free; \nX25 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(!_2, ','(eq(T17, X38), ','(app(T13, T14, X25), lessleaves(X38, X25)))) | ','(app(nil, T17, X24), ','(app(T13, T14, X25), lessleaves(X24, X25))), SCOPE: 2, CLAUSE: 3\n\nT13 is ground\nT14 is ground\nT17 is ground\nX24 is free; \nX25 is free; \nX38 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(app(T11, T12, X24), ','(app(T13, T14, X25), lessleaves(X24, X25))), SCOPE: 2, CLAUSE: 3\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX24 is free; \nX25 is free; \napp(T11, T12, X24) !=? app(nil, X36, X37)", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(eq(T17, X38), ','(app(T13, T14, X25), lessleaves(X38, X25)))\n\nT13 is ground\nT14 is ground\nT17 is ground\nX25 is free; \nX38 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(eq(T17, X38), ','(app(T13, T14, X25), lessleaves(X38, X25))), SCOPE: 3, CLAUSE: 8\n\nT13 is ground\nT14 is ground\nT17 is ground\nX25 is free; \nX38 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(app(T13, T14, X25), lessleaves(T22, X25))\n\nT13 is ground\nT14 is ground\nT22 is ground\nX25 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: app(T13, T14, X25)\n\nT13 is ground\nT14 is ground\nX25 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: lessleaves(T22, T24)\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: app(T13, T14, X25), SCOPE: 4, CLAUSE: 2 | app(T13, T14, X25), SCOPE: 4, CLAUSE: 3\n\nT13 is ground\nT14 is ground\nX25 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(!_4, eq(T28, X64)) | app(nil, T28, X25), SCOPE: 4, CLAUSE: 3\n\nT28 is ground\nX25 is free; \nX64 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: app(T13, T14, X25), SCOPE: 4, CLAUSE: 3\n\nT13 is ground\nT14 is ground\nX25 is free; \napp(T13, T14, X25) !=? app(nil, X62, X63)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: eq(T28, X64)\n\nT28 is ground\nX64 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: eq(T28, X64), SCOPE: 5, CLAUSE: 8\n\nT28 is ground\nX64 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(head(T37, X91), ','(tail(T37, X90), app(X90, T38, X92)))\n\nT37 is ground\nT38 is ground\nX91 is free; \nX92 is free; \nX90 is free; \napp(T37, T38, X25) !=? app(nil, X62, X63)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(head(T37, X91), ','(tail(T37, X90), app(X90, T38, X92))), SCOPE: 6, CLAUSE: 4 | ','(head(T37, X91), ','(tail(T37, X90), app(X90, T38, X92))), SCOPE: 6, CLAUSE: 5\n\nT37 is ground\nT38 is ground\nX91 is free; \nX92 is free; \nX90 is free; \napp(T37, T38, X25) !=? app(nil, X62, X63)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(head(T37, X91), ','(tail(T37, X90), app(X90, T38, X92))), SCOPE: 6, CLAUSE: 4\n\nT37 is ground\nT38 is ground\nX91 is free; \nX92 is free; \nX90 is free; \napp(T37, T38, X25) !=? app(nil, X62, X63)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(head(T37, X91), ','(tail(T37, X90), app(X90, T38, X92))), SCOPE: 6, CLAUSE: 5\n\nT37 is ground\nT38 is ground\nX91 is free; \nX92 is free; \nX90 is free; \napp(T37, T38, X25) !=? app(nil, X62, X63)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(tail([], X90), app(X90, T38, X92))\n\nT38 is ground\nX92 is free; \nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(tail([], X90), app(X90, T38, X92)), SCOPE: 7, CLAUSE: 6 | ','(tail([], X90), app(X90, T38, X92)), SCOPE: 7, CLAUSE: 7\n\nT38 is ground\nX92 is free; \nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(tail([], X90), app(X90, T38, X92)), SCOPE: 7, CLAUSE: 6\n\nT38 is ground\nX92 is free; \nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(tail([], X90), app(X90, T38, X92)), SCOPE: 7, CLAUSE: 7\n\nT38 is ground\nX92 is free; \nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: app([], T38, X92)\n\nT38 is ground\nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: app([], T38, X92), SCOPE: 8, CLAUSE: 2 | app([], T38, X92), SCOPE: 8, CLAUSE: 3\n\nT38 is ground\nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: app([], T38, X92), SCOPE: 8, CLAUSE: 3\n\nT38 is ground\nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(head([], X160), ','(tail([], X159), app(X159, T47, X161)))\n\nT47 is ground\nX160 is free; \nX161 is free; \nX159 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(head([], X160), ','(tail([], X159), app(X159, T47, X161))), SCOPE: 9, CLAUSE: 4 | ','(head([], X160), ','(tail([], X159), app(X159, T47, X161))), SCOPE: 9, CLAUSE: 5\n\nT47 is ground\nX160 is free; \nX161 is free; \nX159 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(head([], X160), ','(tail([], X159), app(X159, T47, X161))), SCOPE: 9, CLAUSE: 4\n\nT47 is ground\nX160 is free; \nX161 is free; \nX159 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(head([], X160), ','(tail([], X159), app(X159, T47, X161))), SCOPE: 9, CLAUSE: 5\n\nT47 is ground\nX160 is free; \nX161 is free; \nX159 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(tail([], X159), app(X159, T47, X161))\n\nT47 is ground\nX161 is free; \nX159 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(tail([], X159), app(X159, T47, X161)), SCOPE: 10, CLAUSE: 6 | ','(tail([], X159), app(X159, T47, X161)), SCOPE: 10, CLAUSE: 7\n\nT47 is ground\nX161 is free; \nX159 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(tail([], X159), app(X159, T47, X161)), SCOPE: 10, CLAUSE: 6\n\nT47 is ground\nX161 is free; \nX159 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(tail([], X159), app(X159, T47, X161)), SCOPE: 10, CLAUSE: 7\n\nT47 is ground\nX161 is free; \nX159 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: app([], T47, X161)\n\nT47 is ground\nX161 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(tail(.(T59, T60), X90), app(X90, T38, X92))\n\nT38 is ground\nT59 is ground\nT60 is ground\nX92 is free; \nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(tail(.(T59, T60), X90), app(X90, T38, X92)), SCOPE: 11, CLAUSE: 6 | ','(tail(.(T59, T60), X90), app(X90, T38, X92)), SCOPE: 11, CLAUSE: 7\n\nT38 is ground\nT59 is ground\nT60 is ground\nX92 is free; \nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(tail(.(T59, T60), X90), app(X90, T38, X92)), SCOPE: 11, CLAUSE: 7\n\nT38 is ground\nT59 is ground\nT60 is ground\nX92 is free; \nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: app(T68, T38, X92)\n\nT38 is ground\nT68 is ground\nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: lessleaves(T22, T24), SCOPE: 12, CLAUSE: 0 | lessleaves(T22, T24), SCOPE: 12, CLAUSE: 1\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: lessleaves(T22, T24), SCOPE: 12, CLAUSE: 0\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: lessleaves(T22, T24), SCOPE: 12, CLAUSE: 1\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(app(T92, T93, X270), ','(app(T96, T97, X271), lessleaves(X270, X271)))\n\nT92 is ground\nT93 is ground\nX270 is free; \nX271 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: app(T92, T93, X270)\n\nT92 is ground\nT93 is ground\nX270 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(app(T96, T97, X271), lessleaves(T99, X271))\n\nX271 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: app(T96, T97, X271)\n\nX271 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: lessleaves(T103, T102)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: app(T96, T97, X271), SCOPE: 13, CLAUSE: 2 | app(T96, T97, X271), SCOPE: 13, CLAUSE: 3\n\nX271 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(!_13, eq(T108, X296)) | app(T96, T97, X271), SCOPE: 13, CLAUSE: 3\n\nX271 is free\nX296 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: app(T96, T97, X271), SCOPE: 13, CLAUSE: 3\n\nX271 is free\napp(T96, T97, X271) !=? app(nil, X294, X295)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: eq(T108, X296)\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: eq(T108, X296), SCOPE: 14, CLAUSE: 8\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(head(T121, X323), ','(tail(T121, X322), app(X322, T122, X324)))\n\nX323 is free\nX324 is free; \nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(head(T121, X323), ','(tail(T121, X322), app(X322, T122, X324))), SCOPE: 15, CLAUSE: 4 | ','(head(T121, X323), ','(tail(T121, X322), app(X322, T122, X324))), SCOPE: 15, CLAUSE: 5\n\nX323 is free\nX324 is free; \nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(head(T121, X323), ','(tail(T121, X322), app(X322, T122, X324))), SCOPE: 15, CLAUSE: 4\n\nX323 is free\nX324 is free; \nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(head(T121, X323), ','(tail(T121, X322), app(X322, T122, X324))), SCOPE: 15, CLAUSE: 5\n\nX323 is free\nX324 is free; \nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(tail([], X322), app(X322, T124, X324))\n\nX324 is free\nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(tail([], X322), app(X322, T124, X324)), SCOPE: 16, CLAUSE: 6 | ','(tail([], X322), app(X322, T124, X324)), SCOPE: 16, CLAUSE: 7\n\nX324 is free\nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(tail([], X322), app(X322, T124, X324)), SCOPE: 16, CLAUSE: 6\n\nX324 is free\nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(tail([], X322), app(X322, T124, X324)), SCOPE: 16, CLAUSE: 7\n\nX324 is free\nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: app([], T124, X324)\n\nX324 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: app([], T124, X324), SCOPE: 17, CLAUSE: 2 | app([], T124, X324), SCOPE: 17, CLAUSE: 3\n\nX324 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: app([], T124, X324), SCOPE: 17, CLAUSE: 3\n\nX324 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(head([], X392), ','(tail([], X391), app(X391, T134, X393)))\n\nX392 is free\nX393 is free; \nX391 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(head([], X392), ','(tail([], X391), app(X391, T134, X393))), SCOPE: 18, CLAUSE: 4 | ','(head([], X392), ','(tail([], X391), app(X391, T134, X393))), SCOPE: 18, CLAUSE: 5\n\nX392 is free\nX393 is free; \nX391 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(head([], X392), ','(tail([], X391), app(X391, T134, X393))), SCOPE: 18, CLAUSE: 4\n\nX392 is free\nX393 is free; \nX391 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(head([], X392), ','(tail([], X391), app(X391, T134, X393))), SCOPE: 18, CLAUSE: 5\n\nX392 is free\nX393 is free; \nX391 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(tail([], X391), app(X391, T134, X393))\n\nX393 is free\nX391 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(tail([], X391), app(X391, T134, X393)), SCOPE: 19, CLAUSE: 6 | ','(tail([], X391), app(X391, T134, X393)), SCOPE: 19, CLAUSE: 7\n\nX393 is free\nX391 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(tail([], X391), app(X391, T134, X393)), SCOPE: 19, CLAUSE: 6\n\nX393 is free\nX391 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(tail([], X391), app(X391, T134, X393)), SCOPE: 19, CLAUSE: 7\n\nX393 is free\nX391 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: app([], T134, X393)\n\nX393 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(tail(.(T148, T149), X322), app(X322, T150, X324))\n\nX324 is free\nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(tail(.(T148, T149), X322), app(X322, T150, X324)), SCOPE: 20, CLAUSE: 6 | ','(tail(.(T148, T149), X322), app(X322, T150, X324)), SCOPE: 20, CLAUSE: 7\n\nX324 is free\nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(tail(.(T148, T149), X322), app(X322, T150, X324)), SCOPE: 20, CLAUSE: 7\n\nX324 is free\nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: app(T161, T162, X324)\n\nX324 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: lessleaves(T103, T102), SCOPE: 21, CLAUSE: 0 | lessleaves(T103, T102), SCOPE: 21, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: lessleaves(T103, T102), SCOPE: 21, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: lessleaves(T103, T102), SCOPE: 21, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(app(T190, T191, X502), ','(app(T192, T193, X503), lessleaves(X502, X503)))\n\nX502 is free\nX503 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: app(T190, T191, X502)\n\nX502 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(app(T196, T197, X503), lessleaves(T195, X503))\n\nX503 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(head(T205, X538), ','(tail(T205, X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X538, X539), X25)))))\n\nT13 is ground\nT14 is ground\nT205 is ground\nT206 is ground\nX25 is free; \nX538 is free; \nX539 is free; \nX537 is free; \napp(T205, T206, X24) !=? app(nil, X36, X37)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(head(T205, X538), ','(tail(T205, X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X538, X539), X25))))), SCOPE: 22, CLAUSE: 4 | ','(head(T205, X538), ','(tail(T205, X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X538, X539), X25))))), SCOPE: 22, CLAUSE: 5\n\nT13 is ground\nT14 is ground\nT205 is ground\nT206 is ground\nX25 is free; \nX538 is free; \nX539 is free; \nX537 is free; \napp(T205, T206, X24) !=? app(nil, X36, X37)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(head(T205, X538), ','(tail(T205, X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X538, X539), X25))))), SCOPE: 22, CLAUSE: 4\n\nT13 is ground\nT14 is ground\nT205 is ground\nT206 is ground\nX25 is free; \nX538 is free; \nX539 is free; \nX537 is free; \napp(T205, T206, X24) !=? app(nil, X36, X37)", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(head(T205, X538), ','(tail(T205, X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X538, X539), X25))))), SCOPE: 22, CLAUSE: 5\n\nT13 is ground\nT14 is ground\nT205 is ground\nT206 is ground\nX25 is free; \nX538 is free; \nX539 is free; \nX537 is free; \napp(T205, T206, X24) !=? app(nil, X36, X37)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(tail([], X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X552, X539), X25))))\n\nT13 is ground\nT14 is ground\nT206 is ground\nX25 is free; \nX539 is free; \nX537 is free; \nX552 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(tail([], X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X552, X539), X25)))), SCOPE: 23, CLAUSE: 6 | ','(tail([], X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X552, X539), X25)))), SCOPE: 23, CLAUSE: 7\n\nT13 is ground\nT14 is ground\nT206 is ground\nX25 is free; \nX539 is free; \nX537 is free; \nX552 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(tail([], X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X552, X539), X25)))), SCOPE: 23, CLAUSE: 6\n\nT13 is ground\nT14 is ground\nT206 is ground\nX25 is free; \nX539 is free; \nX537 is free; \nX552 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(tail([], X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X552, X539), X25)))), SCOPE: 23, CLAUSE: 7\n\nT13 is ground\nT14 is ground\nT206 is ground\nX25 is free; \nX539 is free; \nX537 is free; \nX552 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(app([], T206, X539), ','(app(T13, T14, X25), lessleaves(cons(X552, X539), X25)))\n\nT13 is ground\nT14 is ground\nT206 is ground\nX25 is free; \nX539 is free; \nX552 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: app([], T206, X539)\n\nT206 is ground\nX539 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(app(T13, T14, X25), lessleaves(cons(X552, T212), X25))\n\nT13 is ground\nT14 is ground\nX25 is free; \nX552 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(tail(.(T219, T220), X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(T219, X539), X25))))\n\nT13 is ground\nT14 is ground\nT206 is ground\nT219 is ground\nT220 is ground\nX25 is free; \nX539 is free; \nX537 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(tail(.(T219, T220), X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(T219, X539), X25)))), SCOPE: 24, CLAUSE: 6 | ','(tail(.(T219, T220), X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(T219, X539), X25)))), SCOPE: 24, CLAUSE: 7\n\nT13 is ground\nT14 is ground\nT206 is ground\nT219 is ground\nT220 is ground\nX25 is free; \nX539 is free; \nX537 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(tail(.(T219, T220), X537), ','(app(X537, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(T219, X539), X25)))), SCOPE: 24, CLAUSE: 7\n\nT13 is ground\nT14 is ground\nT206 is ground\nT219 is ground\nT220 is ground\nX25 is free; \nX539 is free; \nX537 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(app(T228, T206, X539), ','(app(T13, T14, X25), lessleaves(cons(T227, X539), X25)))\n\nT13 is ground\nT14 is ground\nT206 is ground\nT227 is ground\nT228 is ground\nX25 is free; \nX539 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: app(T228, T206, X539)\n\nT206 is ground\nT228 is ground\nX539 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(app(T13, T14, X25), lessleaves(cons(T227, T230), X25))\n\nT13 is ground\nT14 is ground\nT227 is ground\nX25 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 131 [arrowhead = none ];
131 -> 2;

132 [label="EVAL with clause\nlessleaves(nil, cons(X8, X9)).\nand substitution\nT1 -> nil\nX8 -> T5\nX9 -> T6\nT2 -> cons(T5, T6)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 132 [arrowhead = none ];
132 -> 3;

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

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

135 [label="EVAL with clause\nlessleaves(cons(X20, X21), cons(X22, X23)) :- ','(app(X20, X21, X24), ','(app(X22, X23, X25), lessleaves(X24, X25))).\nand substitution\nX20 -> T11\nX21 -> T12\nT1 -> cons(T11, T12)\nX22 -> T13\nX23 -> T14\nT2 -> cons(T13, T14)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 135 [arrowhead = none ];
135 -> 7;

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

137 [label="BACKTRACK\nfor clause: lessleaves(cons(U, V), cons(W, Z)) :- ','(app(U, V, U1), ','(app(W, Z, W1), lessleaves(U1, W1)))because of non-unification", fontsize=14, style = filled, fillcolor = white];
5 -> 137 [arrowhead = none ];
137 -> 6;

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

139 [label="EVAL with clause\napp(nil, X36, X37) :- ','(!_2, eq(X36, X37)).\nand substitution\nT11 -> nil\nT12 -> T17\nX36 -> T17\nX24 -> X38\nX37 -> X38", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 139 [arrowhead = none ];
139 -> 10;

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

141 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 141 [arrowhead = none ];
141 -> 12;

142 [label="ONLY EVAL with clause\napp(X533, X534, cons(X535, X536)) :- ','(head(X533, X535), ','(tail(X533, X537), app(X537, X534, X536))).\nand substitution\nT11 -> T205\nX533 -> T205\nT12 -> T206\nX534 -> T206\nX535 -> X538\nX536 -> X539\nX24 -> cons(X538, X539)", fontsize=14, style = filled, fillcolor = white];
11 -> 142 [arrowhead = none ];
142 -> 111;

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

144 [label="ONLY EVAL with clause\neq(X49, X49).\nand substitution\nT17 -> T22\nX49 -> T22\nX38 -> T22", fontsize=14, style = filled, fillcolor = white];
13 -> 144 [arrowhead = none ];
144 -> 14;

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

146 [label="SPLIT 2\nreplacements:\nX25 -> T24", fontsize=14, style = filled, fillcolor = violet];
14 -> 146 [arrowhead = none ];
146 -> 16;

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

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

149 [label="EVAL with clause\napp(nil, X62, X63) :- ','(!_4, eq(X62, X63)).\nand substitution\nT13 -> nil\nT14 -> T28\nX62 -> T28\nX25 -> X64\nX63 -> X64", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 149 [arrowhead = none ];
149 -> 18;

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

151 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 151 [arrowhead = none ];
151 -> 20;

152 [label="ONLY EVAL with clause\napp(X86, X87, cons(X88, X89)) :- ','(head(X86, X88), ','(tail(X86, X90), app(X90, X87, X89))).\nand substitution\nT13 -> T37\nX86 -> T37\nT14 -> T38\nX87 -> T38\nX88 -> X91\nX89 -> X92\nX25 -> cons(X91, X92)", fontsize=14, style = filled, fillcolor = white];
19 -> 152 [arrowhead = none ];
152 -> 24;

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

154 [label="ONLY EVAL with clause\neq(X69, X69).\nand substitution\nT28 -> T31\nX69 -> T31\nX64 -> T31", fontsize=14, style = filled, fillcolor = white];
21 -> 154 [arrowhead = none ];
154 -> 22;

155 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 155 [arrowhead = none ];
155 -> 23;

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

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

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

159 [label="EVAL with clause\nhead([], X104).\nand substitution\nT37 -> []\nX91 -> X105\nX104 -> X105", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 159 [arrowhead = none ];
159 -> 28;

160 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 160 [arrowhead = none ];
160 -> 29;

161 [label="EVAL with clause\nhead(.(X221, X222), X221).\nand substitution\nX221 -> T59\nX222 -> T60\nT37 -> .(T59, T60)\nX91 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 161 [arrowhead = none ];
161 -> 48;

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

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

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

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

166 [label="ONLY EVAL with clause\ntail([], []).\nand substitution\nX90 -> []", fontsize=14, style = filled, fillcolor = white];
31 -> 166 [arrowhead = none ];
166 -> 33;

167 [label="BACKTRACK\nfor clause: tail(.(X5, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
32 -> 167 [arrowhead = none ];
167 -> 47;

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

169 [label="BACKTRACK\nfor clause: app(nil, Y, Z) :- ','(!, eq(Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = white];
34 -> 169 [arrowhead = none ];
169 -> 35;

170 [label="ONLY EVAL with clause\napp(X155, X156, cons(X157, X158)) :- ','(head(X155, X157), ','(tail(X155, X159), app(X159, X156, X158))).\nand substitution\nX155 -> []\nT38 -> T47\nX156 -> T47\nX157 -> X160\nX158 -> X161\nX92 -> cons(X160, X161)", fontsize=14, style = filled, fillcolor = white];
35 -> 170 [arrowhead = none ];
170 -> 36;

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

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

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

174 [label="ONLY EVAL with clause\nhead([], X179).\nand substitution\nX160 -> X180\nX179 -> X180", fontsize=14, style = filled, fillcolor = white];
38 -> 174 [arrowhead = none ];
174 -> 40;

175 [label="BACKTRACK\nfor clause: head(.(X, X4), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
39 -> 175 [arrowhead = none ];
175 -> 46;

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

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

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

179 [label="ONLY EVAL with clause\ntail([], []).\nand substitution\nX159 -> []", fontsize=14, style = filled, fillcolor = white];
42 -> 179 [arrowhead = none ];
179 -> 44;

180 [label="BACKTRACK\nfor clause: tail(.(X5, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
43 -> 180 [arrowhead = none ];
180 -> 45;

181 [label="INSTANCE with matching:\nT38 -> T47\nX92 -> X161", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 181 [arrowhead = none , style=dashed];
181 -> 33[style=dashed];

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

183 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
50 -> 183 [arrowhead = none ];
183 -> 51;

184 [label="ONLY EVAL with clause\ntail(.(X235, X236), X236).\nand substitution\nT59 -> T67\nX235 -> T67\nT60 -> T68\nX236 -> T68\nX90 -> T68", fontsize=14, style = filled, fillcolor = white];
51 -> 184 [arrowhead = none ];
184 -> 52;

185 [label="INSTANCE with matching:\nT13 -> T68\nT14 -> T38\nX25 -> X92", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 185 [arrowhead = none , style=dashed];
185 -> 15[style=dashed];

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

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

188 [label="EVAL with clause\nlessleaves(nil, cons(X252, X253)).\nand substitution\nT22 -> nil\nX252 -> T82\nX253 -> T83\nT24 -> cons(T82, T83)", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 188 [arrowhead = none ];
188 -> 56;

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

190 [label="EVAL with clause\nlessleaves(cons(X266, X267), cons(X268, X269)) :- ','(app(X266, X267, X270), ','(app(X268, X269, X271), lessleaves(X270, X271))).\nand substitution\nX266 -> T92\nX267 -> T93\nT22 -> cons(T92, T93)\nX268 -> T96\nX269 -> T97\nT24 -> cons(T96, T97)\nT94 -> T96\nT95 -> T97", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 190 [arrowhead = none ];
190 -> 59;

191 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 191 [arrowhead = none ];
191 -> 60;

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

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

194 [label="SPLIT 2\nreplacements:\nX270 -> T99", fontsize=14, style = filled, fillcolor = violet];
59 -> 194 [arrowhead = none ];
194 -> 62;

195 [label="INSTANCE with matching:\nT13 -> T92\nT14 -> T93\nX25 -> X270", fontsize=14, style = filled, fillcolor = lightgrey];
61 -> 195 [arrowhead = none , style=dashed];
195 -> 15[style=dashed];

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

197 [label="SPLIT 2\nreplacements:\nX271 -> T102\nT99 -> T103", fontsize=14, style = filled, fillcolor = violet];
62 -> 197 [arrowhead = none ];
197 -> 64;

198 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
63 -> 198 [arrowhead = none ];
198 -> 65;

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

200 [label="EVAL with clause\napp(nil, X294, X295) :- ','(!_13, eq(X294, X295)).\nand substitution\nT96 -> nil\nT97 -> T108\nX294 -> T108\nX271 -> X296\nX295 -> X296\nT107 -> T108", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 200 [arrowhead = none ];
200 -> 66;

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

202 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 202 [arrowhead = none ];
202 -> 68;

203 [label="ONLY EVAL with clause\napp(X318, X319, cons(X320, X321)) :- ','(head(X318, X320), ','(tail(X318, X322), app(X322, X319, X321))).\nand substitution\nT96 -> T121\nX318 -> T121\nT97 -> T122\nX319 -> T122\nX320 -> X323\nX321 -> X324\nX271 -> cons(X323, X324)\nT119 -> T121\nT120 -> T122", fontsize=14, style = filled, fillcolor = white];
67 -> 203 [arrowhead = none ];
203 -> 72;

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

205 [label="ONLY EVAL with clause\neq(X301, X301).\nand substitution\nT108 -> T111\nX301 -> T111\nX296 -> T111", fontsize=14, style = filled, fillcolor = white];
69 -> 205 [arrowhead = none ];
205 -> 70;

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

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

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

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

210 [label="EVAL with clause\nhead([], X336).\nand substitution\nT121 -> []\nX323 -> X337\nX336 -> X337\nT122 -> T124", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 210 [arrowhead = none ];
210 -> 76;

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

212 [label="EVAL with clause\nhead(.(X453, X454), X453).\nand substitution\nX453 -> T148\nX454 -> T149\nT121 -> .(T148, T149)\nX323 -> T148\nT146 -> T148\nT147 -> T149\nT122 -> T150", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 212 [arrowhead = none ];
212 -> 96;

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

214 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
76 -> 214 [arrowhead = none ];
214 -> 78;

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

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

217 [label="ONLY EVAL with clause\ntail([], []).\nand substitution\nX322 -> []", fontsize=14, style = filled, fillcolor = white];
79 -> 217 [arrowhead = none ];
217 -> 81;

218 [label="BACKTRACK\nfor clause: tail(.(X5, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
80 -> 218 [arrowhead = none ];
218 -> 95;

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

220 [label="BACKTRACK\nfor clause: app(nil, Y, Z) :- ','(!, eq(Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = white];
82 -> 220 [arrowhead = none ];
220 -> 83;

221 [label="ONLY EVAL with clause\napp(X387, X388, cons(X389, X390)) :- ','(head(X387, X389), ','(tail(X387, X391), app(X391, X388, X390))).\nand substitution\nX387 -> []\nT124 -> T134\nX388 -> T134\nX389 -> X392\nX390 -> X393\nX324 -> cons(X392, X393)\nT133 -> T134", fontsize=14, style = filled, fillcolor = white];
83 -> 221 [arrowhead = none ];
221 -> 84;

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

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

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

225 [label="ONLY EVAL with clause\nhead([], X411).\nand substitution\nX392 -> X412\nX411 -> X412", fontsize=14, style = filled, fillcolor = white];
86 -> 225 [arrowhead = none ];
225 -> 88;

226 [label="BACKTRACK\nfor clause: head(.(X, X4), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
87 -> 226 [arrowhead = none ];
226 -> 94;

227 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
88 -> 227 [arrowhead = none ];
227 -> 89;

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

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

230 [label="ONLY EVAL with clause\ntail([], []).\nand substitution\nX391 -> []", fontsize=14, style = filled, fillcolor = white];
90 -> 230 [arrowhead = none ];
230 -> 92;

231 [label="BACKTRACK\nfor clause: tail(.(X5, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
91 -> 231 [arrowhead = none ];
231 -> 93;

232 [label="INSTANCE with matching:\nT124 -> T134\nX324 -> X393", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 232 [arrowhead = none , style=dashed];
232 -> 81[style=dashed];

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

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

235 [label="ONLY EVAL with clause\ntail(.(X467, X468), X468).\nand substitution\nT148 -> T159\nX467 -> T159\nT149 -> T161\nX468 -> T161\nX322 -> T161\nT160 -> T161\nT150 -> T162", fontsize=14, style = filled, fillcolor = white];
99 -> 235 [arrowhead = none ];
235 -> 100;

236 [label="INSTANCE with matching:\nT96 -> T161\nT97 -> T162\nX271 -> X324", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 236 [arrowhead = none , style=dashed];
236 -> 63[style=dashed];

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

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

239 [label="EVAL with clause\nlessleaves(nil, cons(X484, X485)).\nand substitution\nT103 -> nil\nX484 -> T176\nX485 -> T177\nT102 -> cons(T176, T177)", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 239 [arrowhead = none ];
239 -> 104;

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

241 [label="EVAL with clause\nlessleaves(cons(X498, X499), cons(X500, X501)) :- ','(app(X498, X499, X502), ','(app(X500, X501, X503), lessleaves(X502, X503))).\nand substitution\nX498 -> T190\nX499 -> T191\nT103 -> cons(T190, T191)\nX500 -> T192\nX501 -> T193\nT102 -> cons(T192, T193)\nT186 -> T190\nT187 -> T191\nT188 -> T192\nT189 -> T193", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 241 [arrowhead = none ];
241 -> 107;

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

243 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 243 [arrowhead = none ];
243 -> 106;

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

245 [label="SPLIT 2\nreplacements:\nX502 -> T195\nT192 -> T196\nT193 -> T197", fontsize=14, style = filled, fillcolor = violet];
107 -> 245 [arrowhead = none ];
245 -> 110;

246 [label="INSTANCE with matching:\nT96 -> T190\nT97 -> T191\nX271 -> X502", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 246 [arrowhead = none , style=dashed];
246 -> 63[style=dashed];

247 [label="INSTANCE with matching:\nT96 -> T196\nT97 -> T197\nX271 -> X503\nT99 -> T195", fontsize=14, style = filled, fillcolor = lightgrey];
110 -> 247 [arrowhead = none , style=dashed];
247 -> 62[style=dashed];

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

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

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

251 [label="EVAL with clause\nhead([], X551).\nand substitution\nT205 -> []\nX538 -> X552\nX551 -> X552", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 251 [arrowhead = none ];
251 -> 115;

252 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 252 [arrowhead = none ];
252 -> 116;

253 [label="EVAL with clause\nhead(.(X602, X603), X602).\nand substitution\nX602 -> T219\nX603 -> T220\nT205 -> .(T219, T220)\nX538 -> T219", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 253 [arrowhead = none ];
253 -> 124;

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

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

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

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

258 [label="ONLY EVAL with clause\ntail([], []).\nand substitution\nX537 -> []", fontsize=14, style = filled, fillcolor = white];
118 -> 258 [arrowhead = none ];
258 -> 120;

259 [label="BACKTRACK\nfor clause: tail(.(X5, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
119 -> 259 [arrowhead = none ];
259 -> 123;

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

261 [label="SPLIT 2\nreplacements:\nX539 -> T212", fontsize=14, style = filled, fillcolor = violet];
120 -> 261 [arrowhead = none ];
261 -> 122;

262 [label="INSTANCE with matching:\nT38 -> T206\nX92 -> X539", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 262 [arrowhead = none , style=dashed];
262 -> 33[style=dashed];

263 [label="INSTANCE with matching:\nT96 -> T13\nT97 -> T14\nX271 -> X25\nT99 -> cons(X552, T212)", fontsize=14, style = filled, fillcolor = lightgrey];
122 -> 263 [arrowhead = none , style=dashed];
263 -> 62[style=dashed];

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

265 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
126 -> 265 [arrowhead = none ];
265 -> 127;

266 [label="ONLY EVAL with clause\ntail(.(X616, X617), X617).\nand substitution\nT219 -> T227\nX616 -> T227\nT220 -> T228\nX617 -> T228\nX537 -> T228", fontsize=14, style = filled, fillcolor = white];
127 -> 266 [arrowhead = none ];
266 -> 128;

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

268 [label="SPLIT 2\nreplacements:\nX539 -> T230", fontsize=14, style = filled, fillcolor = violet];
128 -> 268 [arrowhead = none ];
268 -> 130;

269 [label="INSTANCE with matching:\nT13 -> T228\nT14 -> T206\nX25 -> X539", fontsize=14, style = filled, fillcolor = lightgrey];
129 -> 269 [arrowhead = none , style=dashed];
269 -> 15[style=dashed];

270 [label="INSTANCE with matching:\nT96 -> T13\nT97 -> T14\nX271 -> X25\nT99 -> cons(T227, T230)", fontsize=14, style = filled, fillcolor = lightgrey];
130 -> 270 [arrowhead = none , style=dashed];
270 -> 62[style=dashed];

}

(2) Obligation:

Triples:

app33(T47, cons(X180, X161)) :- app33(T47, X161).
app15([], T38, cons(X105, X92)) :- app33(T38, X92).
app15(.(T67, T68), T38, cons(T67, X92)) :- app15(T68, T38, X92).
app81(T134, cons(X412, X393)) :- app81(T134, X393).
app63([], T124, cons(X337, X324)) :- app81(T124, X324).
app63(.(T159, T161), T162, cons(T159, X324)) :- app63(T161, T162, X324).
p62(T96, T97, X271, T99) :- app63(T96, T97, X271).
p62(T96, T97, cons(T192, T193), cons(T190, T191)) :- ','(appc63(T96, T97, cons(T192, T193)), app63(T190, T191, X502)).
p62(T96, T97, cons(T196, T197), cons(T190, T191)) :- ','(appc63(T96, T97, cons(T196, T197)), ','(appc63(T190, T191, T195), p62(T196, T197, X503, T195))).
lessleaves1(cons(nil, T22), cons(T13, T14)) :- app15(T13, T14, X25).
lessleaves1(cons(nil, cons(T92, T93)), cons(T13, T14)) :- ','(appc15(T13, T14, cons(T96, T97)), app15(T92, T93, X270)).
lessleaves1(cons(nil, cons(T92, T93)), cons(T13, T14)) :- ','(appc15(T13, T14, cons(T96, T97)), ','(appc15(T92, T93, T99), p62(T96, T97, X271, T99))).
lessleaves1(cons([], T206), cons(T13, T14)) :- app33(T206, X539).
lessleaves1(cons([], T206), cons(T13, T14)) :- ','(appc33(T206, T212), p62(T13, T14, X25, cons(X552, T212))).
lessleaves1(cons(.(T227, T228), T206), cons(T13, T14)) :- app15(T228, T206, X539).
lessleaves1(cons(.(T227, T228), T206), cons(T13, T14)) :- ','(appc15(T228, T206, T230), p62(T13, T14, X25, cons(T227, T230))).

Clauses:

appc33(T47, cons(X180, X161)) :- appc33(T47, X161).
appc15(nil, T31, T31).
appc15([], T38, cons(X105, X92)) :- appc33(T38, X92).
appc15(.(T67, T68), T38, cons(T67, X92)) :- appc15(T68, T38, X92).
appc81(T134, cons(X412, X393)) :- appc81(T134, X393).
appc63(nil, T111, T111).
appc63([], T124, cons(X337, X324)) :- appc81(T124, X324).
appc63(.(T159, T161), T162, cons(T159, X324)) :- appc63(T161, T162, X324).
qc62(T96, T97, cons(T176, T177), nil) :- appc63(T96, T97, cons(T176, T177)).
qc62(T96, T97, cons(T196, T197), cons(T190, T191)) :- ','(appc63(T96, T97, cons(T196, T197)), ','(appc63(T190, T191, T195), qc62(T196, T197, X503, T195))).

Afs:

lessleaves1(x1, x2) = lessleaves1(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
lessleaves1_in: (b,b)
app15_in: (b,b,f)
app33_in: (b,f)
appc15_in: (b,b,f)
appc33_in: (b,f)
p62_in: (f,f,f,f) (b,b,f,f)
app63_in: (f,f,f) (b,b,f)
app81_in: (f,f) (b,f)
appc63_in: (f,f,f) (b,b,f)
appc81_in: (f,f) (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

LESSLEAVES1_IN_GG(cons(nil, T22), cons(T13, T14)) → U13_GG(T22, T13, T14, app15_in_gga(T13, T14, X25))
LESSLEAVES1_IN_GG(cons(nil, T22), cons(T13, T14)) → APP15_IN_GGA(T13, T14, X25)
APP15_IN_GGA([], T38, cons(X105, X92)) → U2_GGA(T38, X105, X92, app33_in_ga(T38, X92))
APP15_IN_GGA([], T38, cons(X105, X92)) → APP33_IN_GA(T38, X92)
APP33_IN_GA(T47, cons(X180, X161)) → U1_GA(T47, X180, X161, app33_in_ga(T47, X161))
APP33_IN_GA(T47, cons(X180, X161)) → APP33_IN_GA(T47, X161)
APP15_IN_GGA(.(T67, T68), T38, cons(T67, X92)) → U3_GGA(T67, T68, T38, X92, app15_in_gga(T68, T38, X92))
APP15_IN_GGA(.(T67, T68), T38, cons(T67, X92)) → APP15_IN_GGA(T68, T38, X92)
LESSLEAVES1_IN_GG(cons(nil, cons(T92, T93)), cons(T13, T14)) → U14_GG(T92, T93, T13, T14, appc15_in_gga(T13, T14, cons(T96, T97)))
U14_GG(T92, T93, T13, T14, appc15_out_gga(T13, T14, cons(T96, T97))) → U15_GG(T92, T93, T13, T14, app15_in_gga(T92, T93, X270))
U14_GG(T92, T93, T13, T14, appc15_out_gga(T13, T14, cons(T96, T97))) → APP15_IN_GGA(T92, T93, X270)
U14_GG(T92, T93, T13, T14, appc15_out_gga(T13, T14, cons(T96, T97))) → U16_GG(T92, T93, T13, T14, T96, T97, appc15_in_gga(T92, T93, T99))
U16_GG(T92, T93, T13, T14, T96, T97, appc15_out_gga(T92, T93, T99)) → U17_GG(T92, T93, T13, T14, p62_in_aaaa(T96, T97, X271, T99))
U16_GG(T92, T93, T13, T14, T96, T97, appc15_out_gga(T92, T93, T99)) → P62_IN_AAAA(T96, T97, X271, T99)
P62_IN_AAAA(T96, T97, X271, T99) → U7_AAAA(T96, T97, X271, T99, app63_in_aaa(T96, T97, X271))
P62_IN_AAAA(T96, T97, X271, T99) → APP63_IN_AAA(T96, T97, X271)
APP63_IN_AAA([], T124, cons(X337, X324)) → U5_AAA(T124, X337, X324, app81_in_aa(T124, X324))
APP63_IN_AAA([], T124, cons(X337, X324)) → APP81_IN_AA(T124, X324)
APP81_IN_AA(T134, cons(X412, X393)) → U4_AA(T134, X412, X393, app81_in_aa(T134, X393))
APP81_IN_AA(T134, cons(X412, X393)) → APP81_IN_AA(T134, X393)
APP63_IN_AAA(.(T159, T161), T162, cons(T159, X324)) → U6_AAA(T159, T161, T162, X324, app63_in_aaa(T161, T162, X324))
APP63_IN_AAA(.(T159, T161), T162, cons(T159, X324)) → APP63_IN_AAA(T161, T162, X324)
P62_IN_AAAA(T96, T97, cons(T192, T193), cons(T190, T191)) → U8_AAAA(T96, T97, T192, T193, T190, T191, appc63_in_aaa(T96, T97, cons(T192, T193)))
U8_AAAA(T96, T97, T192, T193, T190, T191, appc63_out_aaa(T96, T97, cons(T192, T193))) → U9_AAAA(T96, T97, T192, T193, T190, T191, app63_in_aaa(T190, T191, X502))
U8_AAAA(T96, T97, T192, T193, T190, T191, appc63_out_aaa(T96, T97, cons(T192, T193))) → APP63_IN_AAA(T190, T191, X502)
P62_IN_AAAA(T96, T97, cons(T196, T197), cons(T190, T191)) → U10_AAAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T96, T97, cons(T196, T197)))
U10_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T96, T97, cons(T196, T197))) → U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T190, T191, T195))
U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → U12_AAAA(T96, T97, T196, T197, T190, T191, p62_in_aaaa(T196, T197, X503, T195))
U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → P62_IN_AAAA(T196, T197, X503, T195)
LESSLEAVES1_IN_GG(cons([], T206), cons(T13, T14)) → U18_GG(T206, T13, T14, app33_in_ga(T206, X539))
LESSLEAVES1_IN_GG(cons([], T206), cons(T13, T14)) → APP33_IN_GA(T206, X539)
LESSLEAVES1_IN_GG(cons([], T206), cons(T13, T14)) → U19_GG(T206, T13, T14, appc33_in_ga(T206, T212))
U19_GG(T206, T13, T14, appc33_out_ga(T206, T212)) → U20_GG(T206, T13, T14, p62_in_ggaa(T13, T14, X25, cons(X552, T212)))
U19_GG(T206, T13, T14, appc33_out_ga(T206, T212)) → P62_IN_GGAA(T13, T14, X25, cons(X552, T212))
P62_IN_GGAA(T96, T97, X271, T99) → U7_GGAA(T96, T97, X271, T99, app63_in_gga(T96, T97, X271))
P62_IN_GGAA(T96, T97, X271, T99) → APP63_IN_GGA(T96, T97, X271)
APP63_IN_GGA([], T124, cons(X337, X324)) → U5_GGA(T124, X337, X324, app81_in_ga(T124, X324))
APP63_IN_GGA([], T124, cons(X337, X324)) → APP81_IN_GA(T124, X324)
APP81_IN_GA(T134, cons(X412, X393)) → U4_GA(T134, X412, X393, app81_in_ga(T134, X393))
APP81_IN_GA(T134, cons(X412, X393)) → APP81_IN_GA(T134, X393)
APP63_IN_GGA(.(T159, T161), T162, cons(T159, X324)) → U6_GGA(T159, T161, T162, X324, app63_in_gga(T161, T162, X324))
APP63_IN_GGA(.(T159, T161), T162, cons(T159, X324)) → APP63_IN_GGA(T161, T162, X324)
P62_IN_GGAA(T96, T97, cons(T192, T193), cons(T190, T191)) → U8_GGAA(T96, T97, T192, T193, T190, T191, appc63_in_gga(T96, T97, cons(T192, T193)))
U8_GGAA(T96, T97, T192, T193, T190, T191, appc63_out_gga(T96, T97, cons(T192, T193))) → U9_GGAA(T96, T97, T192, T193, T190, T191, app63_in_aaa(T190, T191, X502))
U8_GGAA(T96, T97, T192, T193, T190, T191, appc63_out_gga(T96, T97, cons(T192, T193))) → APP63_IN_AAA(T190, T191, X502)
P62_IN_GGAA(T96, T97, cons(T196, T197), cons(T190, T191)) → U10_GGAA(T96, T97, T196, T197, T190, T191, appc63_in_gga(T96, T97, cons(T196, T197)))
U10_GGAA(T96, T97, T196, T197, T190, T191, appc63_out_gga(T96, T97, cons(T196, T197))) → U11_GGAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T190, T191, T195))
U11_GGAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → U12_GGAA(T96, T97, T196, T197, T190, T191, p62_in_aaaa(T196, T197, X503, T195))
U11_GGAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → P62_IN_AAAA(T196, T197, X503, T195)
LESSLEAVES1_IN_GG(cons(.(T227, T228), T206), cons(T13, T14)) → U21_GG(T227, T228, T206, T13, T14, app15_in_gga(T228, T206, X539))
LESSLEAVES1_IN_GG(cons(.(T227, T228), T206), cons(T13, T14)) → APP15_IN_GGA(T228, T206, X539)
LESSLEAVES1_IN_GG(cons(.(T227, T228), T206), cons(T13, T14)) → U22_GG(T227, T228, T206, T13, T14, appc15_in_gga(T228, T206, T230))
U22_GG(T227, T228, T206, T13, T14, appc15_out_gga(T228, T206, T230)) → U23_GG(T227, T228, T206, T13, T14, p62_in_ggaa(T13, T14, X25, cons(T227, T230)))
U22_GG(T227, T228, T206, T13, T14, appc15_out_gga(T228, T206, T230)) → P62_IN_GGAA(T13, T14, X25, cons(T227, T230))

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
app15_in_gga(x1, x2, x3) = app15_in_gga(x1, x2)
[] = []
app33_in_ga(x1, x2) = app33_in_ga(x1)
.(x1, x2) = .(x1, x2)
appc15_in_gga(x1, x2, x3) = appc15_in_gga(x1, x2)
appc15_out_gga(x1, x2, x3) = appc15_out_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x4)
appc33_in_ga(x1, x2) = appc33_in_ga(x1)
U25_ga(x1, x2, x3, x4) = U25_ga(x1, x4)
appc33_out_ga(x1, x2) = appc33_out_ga(x1)
U27_gga(x1, x2, x3, x4, x5) = U27_gga(x1, x2, x3, x5)
p62_in_aaaa(x1, x2, x3, x4) = p62_in_aaaa
app63_in_aaa(x1, x2, x3) = app63_in_aaa
app81_in_aa(x1, x2) = app81_in_aa
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
p62_in_ggaa(x1, x2, x3, x4) = p62_in_ggaa(x1, x2)
app63_in_gga(x1, x2, x3) = app63_in_gga(x1, x2)
app81_in_ga(x1, x2) = app81_in_ga(x1)
appc63_in_gga(x1, x2, x3) = appc63_in_gga(x1, x2)
appc63_out_gga(x1, x2, x3) = appc63_out_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x4)
appc81_in_ga(x1, x2) = appc81_in_ga(x1)
U28_ga(x1, x2, x3, x4) = U28_ga(x1, x4)
appc81_out_ga(x1, x2) = appc81_out_ga(x1)
U30_gga(x1, x2, x3, x4, x5) = U30_gga(x1, x2, x3, x5)
LESSLEAVES1_IN_GG(x1, x2) = LESSLEAVES1_IN_GG(x1, x2)
U13_GG(x1, x2, x3, x4) = U13_GG(x1, x2, x3, x4)
APP15_IN_GGA(x1, x2, x3) = APP15_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x4)
APP33_IN_GA(x1, x2) = APP33_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x1, x4)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U14_GG(x1, x2, x3, x4, x5) = U14_GG(x1, x2, x3, x4, x5)
U15_GG(x1, x2, x3, x4, x5) = U15_GG(x1, x2, x3, x4, x5)
U16_GG(x1, x2, x3, x4, x5, x6, x7) = U16_GG(x1, x2, x3, x4, x7)
U17_GG(x1, x2, x3, x4, x5) = U17_GG(x1, x2, x3, x4, x5)
P62_IN_AAAA(x1, x2, x3, x4) = P62_IN_AAAA
U7_AAAA(x1, x2, x3, x4, x5) = U7_AAAA(x5)
APP63_IN_AAA(x1, x2, x3) = APP63_IN_AAA
U5_AAA(x1, x2, x3, x4) = U5_AAA(x4)
APP81_IN_AA(x1, x2) = APP81_IN_AA
U4_AA(x1, x2, x3, x4) = U4_AA(x4)
U6_AAA(x1, x2, x3, x4, x5) = U6_AAA(x5)
U8_AAAA(x1, x2, x3, x4, x5, x6, x7) = U8_AAAA(x7)
U9_AAAA(x1, x2, x3, x4, x5, x6, x7) = U9_AAAA(x7)
U10_AAAA(x1, x2, x3, x4, x5, x6, x7) = U10_AAAA(x7)
U11_AAAA(x1, x2, x3, x4, x5, x6, x7) = U11_AAAA(x7)
U12_AAAA(x1, x2, x3, x4, x5, x6, x7) = U12_AAAA(x7)
U18_GG(x1, x2, x3, x4) = U18_GG(x1, x2, x3, x4)
U19_GG(x1, x2, x3, x4) = U19_GG(x1, x2, x3, x4)
U20_GG(x1, x2, x3, x4) = U20_GG(x1, x2, x3, x4)
P62_IN_GGAA(x1, x2, x3, x4) = P62_IN_GGAA(x1, x2)
U7_GGAA(x1, x2, x3, x4, x5) = U7_GGAA(x1, x2, x5)
APP63_IN_GGA(x1, x2, x3) = APP63_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4) = U5_GGA(x1, x4)
APP81_IN_GA(x1, x2) = APP81_IN_GA(x1)
U4_GA(x1, x2, x3, x4) = U4_GA(x1, x4)
U6_GGA(x1, x2, x3, x4, x5) = U6_GGA(x1, x2, x3, x5)
U8_GGAA(x1, x2, x3, x4, x5, x6, x7) = U8_GGAA(x1, x2, x7)
U9_GGAA(x1, x2, x3, x4, x5, x6, x7) = U9_GGAA(x1, x2, x7)
U10_GGAA(x1, x2, x3, x4, x5, x6, x7) = U10_GGAA(x1, x2, x7)
U11_GGAA(x1, x2, x3, x4, x5, x6, x7) = U11_GGAA(x1, x2, x7)
U12_GGAA(x1, x2, x3, x4, x5, x6, x7) = U12_GGAA(x1, x2, x7)
U21_GG(x1, x2, x3, x4, x5, x6) = U21_GG(x1, x2, x3, x4, x5, x6)
U22_GG(x1, x2, x3, x4, x5, x6) = U22_GG(x1, x2, x3, x4, x5, x6)
U23_GG(x1, x2, x3, x4, x5, x6) = U23_GG(x1, x2, x3, x4, x5, x6)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

LESSLEAVES1_IN_GG(cons(nil, T22), cons(T13, T14)) → U13_GG(T22, T13, T14, app15_in_gga(T13, T14, X25))
LESSLEAVES1_IN_GG(cons(nil, T22), cons(T13, T14)) → APP15_IN_GGA(T13, T14, X25)
APP15_IN_GGA([], T38, cons(X105, X92)) → U2_GGA(T38, X105, X92, app33_in_ga(T38, X92))
APP15_IN_GGA([], T38, cons(X105, X92)) → APP33_IN_GA(T38, X92)
APP33_IN_GA(T47, cons(X180, X161)) → U1_GA(T47, X180, X161, app33_in_ga(T47, X161))
APP33_IN_GA(T47, cons(X180, X161)) → APP33_IN_GA(T47, X161)
APP15_IN_GGA(.(T67, T68), T38, cons(T67, X92)) → U3_GGA(T67, T68, T38, X92, app15_in_gga(T68, T38, X92))
APP15_IN_GGA(.(T67, T68), T38, cons(T67, X92)) → APP15_IN_GGA(T68, T38, X92)
LESSLEAVES1_IN_GG(cons(nil, cons(T92, T93)), cons(T13, T14)) → U14_GG(T92, T93, T13, T14, appc15_in_gga(T13, T14, cons(T96, T97)))
U14_GG(T92, T93, T13, T14, appc15_out_gga(T13, T14, cons(T96, T97))) → U15_GG(T92, T93, T13, T14, app15_in_gga(T92, T93, X270))
U14_GG(T92, T93, T13, T14, appc15_out_gga(T13, T14, cons(T96, T97))) → APP15_IN_GGA(T92, T93, X270)
U14_GG(T92, T93, T13, T14, appc15_out_gga(T13, T14, cons(T96, T97))) → U16_GG(T92, T93, T13, T14, T96, T97, appc15_in_gga(T92, T93, T99))
U16_GG(T92, T93, T13, T14, T96, T97, appc15_out_gga(T92, T93, T99)) → U17_GG(T92, T93, T13, T14, p62_in_aaaa(T96, T97, X271, T99))
U16_GG(T92, T93, T13, T14, T96, T97, appc15_out_gga(T92, T93, T99)) → P62_IN_AAAA(T96, T97, X271, T99)
P62_IN_AAAA(T96, T97, X271, T99) → U7_AAAA(T96, T97, X271, T99, app63_in_aaa(T96, T97, X271))
P62_IN_AAAA(T96, T97, X271, T99) → APP63_IN_AAA(T96, T97, X271)
APP63_IN_AAA([], T124, cons(X337, X324)) → U5_AAA(T124, X337, X324, app81_in_aa(T124, X324))
APP63_IN_AAA([], T124, cons(X337, X324)) → APP81_IN_AA(T124, X324)
APP81_IN_AA(T134, cons(X412, X393)) → U4_AA(T134, X412, X393, app81_in_aa(T134, X393))
APP81_IN_AA(T134, cons(X412, X393)) → APP81_IN_AA(T134, X393)
APP63_IN_AAA(.(T159, T161), T162, cons(T159, X324)) → U6_AAA(T159, T161, T162, X324, app63_in_aaa(T161, T162, X324))
APP63_IN_AAA(.(T159, T161), T162, cons(T159, X324)) → APP63_IN_AAA(T161, T162, X324)
P62_IN_AAAA(T96, T97, cons(T192, T193), cons(T190, T191)) → U8_AAAA(T96, T97, T192, T193, T190, T191, appc63_in_aaa(T96, T97, cons(T192, T193)))
U8_AAAA(T96, T97, T192, T193, T190, T191, appc63_out_aaa(T96, T97, cons(T192, T193))) → U9_AAAA(T96, T97, T192, T193, T190, T191, app63_in_aaa(T190, T191, X502))
U8_AAAA(T96, T97, T192, T193, T190, T191, appc63_out_aaa(T96, T97, cons(T192, T193))) → APP63_IN_AAA(T190, T191, X502)
P62_IN_AAAA(T96, T97, cons(T196, T197), cons(T190, T191)) → U10_AAAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T96, T97, cons(T196, T197)))
U10_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T96, T97, cons(T196, T197))) → U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T190, T191, T195))
U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → U12_AAAA(T96, T97, T196, T197, T190, T191, p62_in_aaaa(T196, T197, X503, T195))
U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → P62_IN_AAAA(T196, T197, X503, T195)
LESSLEAVES1_IN_GG(cons([], T206), cons(T13, T14)) → U18_GG(T206, T13, T14, app33_in_ga(T206, X539))
LESSLEAVES1_IN_GG(cons([], T206), cons(T13, T14)) → APP33_IN_GA(T206, X539)
LESSLEAVES1_IN_GG(cons([], T206), cons(T13, T14)) → U19_GG(T206, T13, T14, appc33_in_ga(T206, T212))
U19_GG(T206, T13, T14, appc33_out_ga(T206, T212)) → U20_GG(T206, T13, T14, p62_in_ggaa(T13, T14, X25, cons(X552, T212)))
U19_GG(T206, T13, T14, appc33_out_ga(T206, T212)) → P62_IN_GGAA(T13, T14, X25, cons(X552, T212))
P62_IN_GGAA(T96, T97, X271, T99) → U7_GGAA(T96, T97, X271, T99, app63_in_gga(T96, T97, X271))
P62_IN_GGAA(T96, T97, X271, T99) → APP63_IN_GGA(T96, T97, X271)
APP63_IN_GGA([], T124, cons(X337, X324)) → U5_GGA(T124, X337, X324, app81_in_ga(T124, X324))
APP63_IN_GGA([], T124, cons(X337, X324)) → APP81_IN_GA(T124, X324)
APP81_IN_GA(T134, cons(X412, X393)) → U4_GA(T134, X412, X393, app81_in_ga(T134, X393))
APP81_IN_GA(T134, cons(X412, X393)) → APP81_IN_GA(T134, X393)
APP63_IN_GGA(.(T159, T161), T162, cons(T159, X324)) → U6_GGA(T159, T161, T162, X324, app63_in_gga(T161, T162, X324))
APP63_IN_GGA(.(T159, T161), T162, cons(T159, X324)) → APP63_IN_GGA(T161, T162, X324)
P62_IN_GGAA(T96, T97, cons(T192, T193), cons(T190, T191)) → U8_GGAA(T96, T97, T192, T193, T190, T191, appc63_in_gga(T96, T97, cons(T192, T193)))
U8_GGAA(T96, T97, T192, T193, T190, T191, appc63_out_gga(T96, T97, cons(T192, T193))) → U9_GGAA(T96, T97, T192, T193, T190, T191, app63_in_aaa(T190, T191, X502))
U8_GGAA(T96, T97, T192, T193, T190, T191, appc63_out_gga(T96, T97, cons(T192, T193))) → APP63_IN_AAA(T190, T191, X502)
P62_IN_GGAA(T96, T97, cons(T196, T197), cons(T190, T191)) → U10_GGAA(T96, T97, T196, T197, T190, T191, appc63_in_gga(T96, T97, cons(T196, T197)))
U10_GGAA(T96, T97, T196, T197, T190, T191, appc63_out_gga(T96, T97, cons(T196, T197))) → U11_GGAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T190, T191, T195))
U11_GGAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → U12_GGAA(T96, T97, T196, T197, T190, T191, p62_in_aaaa(T196, T197, X503, T195))
U11_GGAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → P62_IN_AAAA(T196, T197, X503, T195)
LESSLEAVES1_IN_GG(cons(.(T227, T228), T206), cons(T13, T14)) → U21_GG(T227, T228, T206, T13, T14, app15_in_gga(T228, T206, X539))
LESSLEAVES1_IN_GG(cons(.(T227, T228), T206), cons(T13, T14)) → APP15_IN_GGA(T228, T206, X539)
LESSLEAVES1_IN_GG(cons(.(T227, T228), T206), cons(T13, T14)) → U22_GG(T227, T228, T206, T13, T14, appc15_in_gga(T228, T206, T230))
U22_GG(T227, T228, T206, T13, T14, appc15_out_gga(T228, T206, T230)) → U23_GG(T227, T228, T206, T13, T14, p62_in_ggaa(T13, T14, X25, cons(T227, T230)))
U22_GG(T227, T228, T206, T13, T14, appc15_out_gga(T228, T206, T230)) → P62_IN_GGAA(T13, T14, X25, cons(T227, T230))

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 7 SCCs with 45 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

APP81_IN_GA(T134, cons(X412, X393)) → APP81_IN_GA(T134, X393)

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
[] = []
.(x1, x2) = .(x1, x2)
appc15_in_gga(x1, x2, x3) = appc15_in_gga(x1, x2)
appc15_out_gga(x1, x2, x3) = appc15_out_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x4)
appc33_in_ga(x1, x2) = appc33_in_ga(x1)
U25_ga(x1, x2, x3, x4) = U25_ga(x1, x4)
appc33_out_ga(x1, x2) = appc33_out_ga(x1)
U27_gga(x1, x2, x3, x4, x5) = U27_gga(x1, x2, x3, x5)
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
appc63_in_gga(x1, x2, x3) = appc63_in_gga(x1, x2)
appc63_out_gga(x1, x2, x3) = appc63_out_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x4)
appc81_in_ga(x1, x2) = appc81_in_ga(x1)
U28_ga(x1, x2, x3, x4) = U28_ga(x1, x4)
appc81_out_ga(x1, x2) = appc81_out_ga(x1)
U30_gga(x1, x2, x3, x4, x5) = U30_gga(x1, x2, x3, x5)
APP81_IN_GA(x1, x2) = APP81_IN_GA(x1)

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

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

APP81_IN_GA(T134, cons(X412, X393)) → APP81_IN_GA(T134, X393)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
APP81_IN_GA(x1, x2) = APP81_IN_GA(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:

APP81_IN_GA(T134) → APP81_IN_GA(T134)

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

(12) NonTerminationProof (EQUIVALENT transformation)

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

s = APP81_IN_GA(T134) evaluates to t =APP81_IN_GA(T134)

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

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP81_IN_GA(T134) to APP81_IN_GA(T134).

(13) NO

(14) Obligation:

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

APP63_IN_GGA(.(T159, T161), T162, cons(T159, X324)) → APP63_IN_GGA(T161, T162, X324)

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
[] = []
.(x1, x2) = .(x1, x2)
appc15_in_gga(x1, x2, x3) = appc15_in_gga(x1, x2)
appc15_out_gga(x1, x2, x3) = appc15_out_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x4)
appc33_in_ga(x1, x2) = appc33_in_ga(x1)
U25_ga(x1, x2, x3, x4) = U25_ga(x1, x4)
appc33_out_ga(x1, x2) = appc33_out_ga(x1)
U27_gga(x1, x2, x3, x4, x5) = U27_gga(x1, x2, x3, x5)
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
appc63_in_gga(x1, x2, x3) = appc63_in_gga(x1, x2)
appc63_out_gga(x1, x2, x3) = appc63_out_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x4)
appc81_in_ga(x1, x2) = appc81_in_ga(x1)
U28_ga(x1, x2, x3, x4) = U28_ga(x1, x4)
appc81_out_ga(x1, x2) = appc81_out_ga(x1)
U30_gga(x1, x2, x3, x4, x5) = U30_gga(x1, x2, x3, x5)
APP63_IN_GGA(x1, x2, x3) = APP63_IN_GGA(x1, x2)

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

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

APP63_IN_GGA(.(T159, T161), T162, cons(T159, X324)) → APP63_IN_GGA(T161, T162, X324)

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

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:

APP63_IN_GGA(.(T159, T161), T162) → APP63_IN_GGA(T161, T162)

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

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

APP63_IN_GGA(.(T159, T161), T162) → APP63_IN_GGA(T161, T162)
The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

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

APP81_IN_AA(T134, cons(X412, X393)) → APP81_IN_AA(T134, X393)

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
[] = []
.(x1, x2) = .(x1, x2)
appc15_in_gga(x1, x2, x3) = appc15_in_gga(x1, x2)
appc15_out_gga(x1, x2, x3) = appc15_out_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x4)
appc33_in_ga(x1, x2) = appc33_in_ga(x1)
U25_ga(x1, x2, x3, x4) = U25_ga(x1, x4)
appc33_out_ga(x1, x2) = appc33_out_ga(x1)
U27_gga(x1, x2, x3, x4, x5) = U27_gga(x1, x2, x3, x5)
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
appc63_in_gga(x1, x2, x3) = appc63_in_gga(x1, x2)
appc63_out_gga(x1, x2, x3) = appc63_out_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x4)
appc81_in_ga(x1, x2) = appc81_in_ga(x1)
U28_ga(x1, x2, x3, x4) = U28_ga(x1, x4)
appc81_out_ga(x1, x2) = appc81_out_ga(x1)
U30_gga(x1, x2, x3, x4, x5) = U30_gga(x1, x2, x3, x5)
APP81_IN_AA(x1, x2) = APP81_IN_AA

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

APP81_IN_AA(T134, cons(X412, X393)) → APP81_IN_AA(T134, X393)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

APP81_IN_AA → APP81_IN_AA

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

(26) NonTerminationProof (EQUIVALENT transformation)

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

s = APP81_IN_AA evaluates to t =APP81_IN_AA

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

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

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

(27) NO

(28) Obligation:

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

APP63_IN_AAA(.(T159, T161), T162, cons(T159, X324)) → APP63_IN_AAA(T161, T162, X324)

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
[] = []
.(x1, x2) = .(x1, x2)
appc15_in_gga(x1, x2, x3) = appc15_in_gga(x1, x2)
appc15_out_gga(x1, x2, x3) = appc15_out_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x4)
appc33_in_ga(x1, x2) = appc33_in_ga(x1)
U25_ga(x1, x2, x3, x4) = U25_ga(x1, x4)
appc33_out_ga(x1, x2) = appc33_out_ga(x1)
U27_gga(x1, x2, x3, x4, x5) = U27_gga(x1, x2, x3, x5)
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
appc63_in_gga(x1, x2, x3) = appc63_in_gga(x1, x2)
appc63_out_gga(x1, x2, x3) = appc63_out_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x4)
appc81_in_ga(x1, x2) = appc81_in_ga(x1)
U28_ga(x1, x2, x3, x4) = U28_ga(x1, x4)
appc81_out_ga(x1, x2) = appc81_out_ga(x1)
U30_gga(x1, x2, x3, x4, x5) = U30_gga(x1, x2, x3, x5)
APP63_IN_AAA(x1, x2, x3) = APP63_IN_AAA

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

APP63_IN_AAA(.(T159, T161), T162, cons(T159, X324)) → APP63_IN_AAA(T161, T162, X324)

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

APP63_IN_AAA → APP63_IN_AAA

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

(33) NonTerminationProof (EQUIVALENT transformation)

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

s = APP63_IN_AAA evaluates to t =APP63_IN_AAA

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

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

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

(34) NO

(35) Obligation:

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

P62_IN_AAAA(T96, T97, cons(T196, T197), cons(T190, T191)) → U10_AAAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T96, T97, cons(T196, T197)))
U10_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T96, T97, cons(T196, T197))) → U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T190, T191, T195))
U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → P62_IN_AAAA(T196, T197, X503, T195)

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
[] = []
.(x1, x2) = .(x1, x2)
appc15_in_gga(x1, x2, x3) = appc15_in_gga(x1, x2)
appc15_out_gga(x1, x2, x3) = appc15_out_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x4)
appc33_in_ga(x1, x2) = appc33_in_ga(x1)
U25_ga(x1, x2, x3, x4) = U25_ga(x1, x4)
appc33_out_ga(x1, x2) = appc33_out_ga(x1)
U27_gga(x1, x2, x3, x4, x5) = U27_gga(x1, x2, x3, x5)
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
appc63_in_gga(x1, x2, x3) = appc63_in_gga(x1, x2)
appc63_out_gga(x1, x2, x3) = appc63_out_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x4)
appc81_in_ga(x1, x2) = appc81_in_ga(x1)
U28_ga(x1, x2, x3, x4) = U28_ga(x1, x4)
appc81_out_ga(x1, x2) = appc81_out_ga(x1)
U30_gga(x1, x2, x3, x4, x5) = U30_gga(x1, x2, x3, x5)
P62_IN_AAAA(x1, x2, x3, x4) = P62_IN_AAAA
U10_AAAA(x1, x2, x3, x4, x5, x6, x7) = U10_AAAA(x7)
U11_AAAA(x1, x2, x3, x4, x5, x6, x7) = U11_AAAA(x7)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

P62_IN_AAAA(T96, T97, cons(T196, T197), cons(T190, T191)) → U10_AAAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T96, T97, cons(T196, T197)))
U10_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T96, T97, cons(T196, T197))) → U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_in_aaa(T190, T191, T195))
U11_AAAA(T96, T97, T196, T197, T190, T191, appc63_out_aaa(T190, T191, T195)) → P62_IN_AAAA(T196, T197, X503, T195)

The TRS R consists of the following rules:

appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
[] = []
.(x1, x2) = .(x1, x2)
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
P62_IN_AAAA(x1, x2, x3, x4) = P62_IN_AAAA
U10_AAAA(x1, x2, x3, x4, x5, x6, x7) = U10_AAAA(x7)
U11_AAAA(x1, x2, x3, x4, x5, x6, x7) = U11_AAAA(x7)

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

P62_IN_AAAA → U10_AAAA(appc63_in_aaa)
U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_in_aaa)
U11_AAAA(appc63_out_aaa) → P62_IN_AAAA

The TRS R consists of the following rules:

appc63_in_aaa → appc63_out_aaa
appc63_in_aaa → U29_aaa(appc81_in_aa)
appc63_in_aaa → U30_aaa(appc63_in_aaa)
U29_aaa(appc81_out_aa(T124)) → appc63_out_aaa
U30_aaa(appc63_out_aaa) → appc63_out_aaa
appc81_in_aa → U28_aa(appc81_in_aa)
U28_aa(appc81_out_aa(T134)) → appc81_out_aa(T134)

The set Q consists of the following terms:

appc63_in_aaa
U29_aaa(x0)
U30_aaa(x0)
appc81_in_aa
U28_aa(x0)

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

(40) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

appc63_in_aaa → U29_aaa(appc81_in_aa)
U29_aaa(appc81_out_aa(T124)) → appc63_out_aaa

Used ordering: Polynomial interpretation [POLO]:

POL(P62_IN_AAAA) = 1
POL(U10_AAAA(x₁)) = x₁
POL(U11_AAAA(x₁)) = x₁
POL(U28_aa(x₁)) = x₁
POL(U29_aaa(x₁)) = x₁
POL(U30_aaa(x₁)) = x₁
POL(appc63_in_aaa) = 1
POL(appc63_out_aaa) = 1
POL(appc81_in_aa) = 0
POL(appc81_out_aa(x₁)) = 2 + x₁

(41) Obligation:

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

P62_IN_AAAA → U10_AAAA(appc63_in_aaa)
U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_in_aaa)
U11_AAAA(appc63_out_aaa) → P62_IN_AAAA

The TRS R consists of the following rules:

appc63_in_aaa → appc63_out_aaa
appc63_in_aaa → U30_aaa(appc63_in_aaa)
U30_aaa(appc63_out_aaa) → appc63_out_aaa
appc81_in_aa → U28_aa(appc81_in_aa)
U28_aa(appc81_out_aa(T134)) → appc81_out_aa(T134)

The set Q consists of the following terms:

appc63_in_aaa
U29_aaa(x0)
U30_aaa(x0)
appc81_in_aa
U28_aa(x0)

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

(42) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(43) Obligation:

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

P62_IN_AAAA → U10_AAAA(appc63_in_aaa)
U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_in_aaa)
U11_AAAA(appc63_out_aaa) → P62_IN_AAAA

The TRS R consists of the following rules:

appc63_in_aaa → appc63_out_aaa
appc63_in_aaa → U30_aaa(appc63_in_aaa)
U30_aaa(appc63_out_aaa) → appc63_out_aaa

The set Q consists of the following terms:

appc63_in_aaa
U29_aaa(x0)
U30_aaa(x0)
appc81_in_aa
U28_aa(x0)

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

(44) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

U29_aaa(x0)
appc81_in_aa
U28_aa(x0)

(45) Obligation:

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

P62_IN_AAAA → U10_AAAA(appc63_in_aaa)
U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_in_aaa)
U11_AAAA(appc63_out_aaa) → P62_IN_AAAA

The TRS R consists of the following rules:

appc63_in_aaa → appc63_out_aaa
appc63_in_aaa → U30_aaa(appc63_in_aaa)
U30_aaa(appc63_out_aaa) → appc63_out_aaa

The set Q consists of the following terms:

appc63_in_aaa
U30_aaa(x0)

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

(46) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P62_IN_AAAA → U10_AAAA(appc63_in_aaa) at position [0] we obtained the following new rules [LPAR04]:

P62_IN_AAAA → U10_AAAA(appc63_out_aaa)
P62_IN_AAAA → U10_AAAA(U30_aaa(appc63_in_aaa))

(47) Obligation:

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

U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_in_aaa)
U11_AAAA(appc63_out_aaa) → P62_IN_AAAA
P62_IN_AAAA → U10_AAAA(appc63_out_aaa)
P62_IN_AAAA → U10_AAAA(U30_aaa(appc63_in_aaa))

The TRS R consists of the following rules:

appc63_in_aaa → appc63_out_aaa
appc63_in_aaa → U30_aaa(appc63_in_aaa)
U30_aaa(appc63_out_aaa) → appc63_out_aaa

The set Q consists of the following terms:

appc63_in_aaa
U30_aaa(x0)

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

(48) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_in_aaa) at position [0] we obtained the following new rules [LPAR04]:

U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_out_aaa)
U10_AAAA(appc63_out_aaa) → U11_AAAA(U30_aaa(appc63_in_aaa))

(49) Obligation:

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

U11_AAAA(appc63_out_aaa) → P62_IN_AAAA
P62_IN_AAAA → U10_AAAA(appc63_out_aaa)
P62_IN_AAAA → U10_AAAA(U30_aaa(appc63_in_aaa))
U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_out_aaa)
U10_AAAA(appc63_out_aaa) → U11_AAAA(U30_aaa(appc63_in_aaa))

The TRS R consists of the following rules:

appc63_in_aaa → appc63_out_aaa
appc63_in_aaa → U30_aaa(appc63_in_aaa)
U30_aaa(appc63_out_aaa) → appc63_out_aaa

The set Q consists of the following terms:

appc63_in_aaa
U30_aaa(x0)

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

(50) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = P62_IN_AAAA evaluates to t =P62_IN_AAAA

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

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

P62_IN_AAAA → U10_AAAA(appc63_out_aaa)
with rule P62_IN_AAAA → U10_AAAA(appc63_out_aaa) at position [] and matcher [ ]

U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_out_aaa)
with rule U10_AAAA(appc63_out_aaa) → U11_AAAA(appc63_out_aaa) at position [] and matcher [ ]

U11_AAAA(appc63_out_aaa) → P62_IN_AAAA
with rule U11_AAAA(appc63_out_aaa) → P62_IN_AAAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

(51) NO

(52) Obligation:

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

APP33_IN_GA(T47, cons(X180, X161)) → APP33_IN_GA(T47, X161)

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
[] = []
.(x1, x2) = .(x1, x2)
appc15_in_gga(x1, x2, x3) = appc15_in_gga(x1, x2)
appc15_out_gga(x1, x2, x3) = appc15_out_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x4)
appc33_in_ga(x1, x2) = appc33_in_ga(x1)
U25_ga(x1, x2, x3, x4) = U25_ga(x1, x4)
appc33_out_ga(x1, x2) = appc33_out_ga(x1)
U27_gga(x1, x2, x3, x4, x5) = U27_gga(x1, x2, x3, x5)
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
appc63_in_gga(x1, x2, x3) = appc63_in_gga(x1, x2)
appc63_out_gga(x1, x2, x3) = appc63_out_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x4)
appc81_in_ga(x1, x2) = appc81_in_ga(x1)
U28_ga(x1, x2, x3, x4) = U28_ga(x1, x4)
appc81_out_ga(x1, x2) = appc81_out_ga(x1)
U30_gga(x1, x2, x3, x4, x5) = U30_gga(x1, x2, x3, x5)
APP33_IN_GA(x1, x2) = APP33_IN_GA(x1)

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

(53) UsableRulesProof (EQUIVALENT transformation)

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

(54) Obligation:

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

APP33_IN_GA(T47, cons(X180, X161)) → APP33_IN_GA(T47, X161)

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

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

(55) PiDPToQDPProof (SOUND transformation)

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

(56) Obligation:

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

APP33_IN_GA(T47) → APP33_IN_GA(T47)

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

(57) NonTerminationProof (EQUIVALENT transformation)

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

s = APP33_IN_GA(T47) evaluates to t =APP33_IN_GA(T47)

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

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP33_IN_GA(T47) to APP33_IN_GA(T47).

(58) NO

(59) Obligation:

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

APP15_IN_GGA(.(T67, T68), T38, cons(T67, X92)) → APP15_IN_GGA(T68, T38, X92)

The TRS R consists of the following rules:

appc15_in_gga(nil, T31, T31) → appc15_out_gga(nil, T31, T31)
appc15_in_gga([], T38, cons(X105, X92)) → U26_gga(T38, X105, X92, appc33_in_ga(T38, X92))
appc33_in_ga(T47, cons(X180, X161)) → U25_ga(T47, X180, X161, appc33_in_ga(T47, X161))
U25_ga(T47, X180, X161, appc33_out_ga(T47, X161)) → appc33_out_ga(T47, cons(X180, X161))
U26_gga(T38, X105, X92, appc33_out_ga(T38, X92)) → appc15_out_gga([], T38, cons(X105, X92))
appc15_in_gga(.(T67, T68), T38, cons(T67, X92)) → U27_gga(T67, T68, T38, X92, appc15_in_gga(T68, T38, X92))
U27_gga(T67, T68, T38, X92, appc15_out_gga(T68, T38, X92)) → appc15_out_gga(.(T67, T68), T38, cons(T67, X92))
appc63_in_aaa(nil, T111, T111) → appc63_out_aaa(nil, T111, T111)
appc63_in_aaa([], T124, cons(X337, X324)) → U29_aaa(T124, X337, X324, appc81_in_aa(T124, X324))
appc81_in_aa(T134, cons(X412, X393)) → U28_aa(T134, X412, X393, appc81_in_aa(T134, X393))
U28_aa(T134, X412, X393, appc81_out_aa(T134, X393)) → appc81_out_aa(T134, cons(X412, X393))
U29_aaa(T124, X337, X324, appc81_out_aa(T124, X324)) → appc63_out_aaa([], T124, cons(X337, X324))
appc63_in_aaa(.(T159, T161), T162, cons(T159, X324)) → U30_aaa(T159, T161, T162, X324, appc63_in_aaa(T161, T162, X324))
U30_aaa(T159, T161, T162, X324, appc63_out_aaa(T161, T162, X324)) → appc63_out_aaa(.(T159, T161), T162, cons(T159, X324))
appc63_in_gga(nil, T111, T111) → appc63_out_gga(nil, T111, T111)
appc63_in_gga([], T124, cons(X337, X324)) → U29_gga(T124, X337, X324, appc81_in_ga(T124, X324))
appc81_in_ga(T134, cons(X412, X393)) → U28_ga(T134, X412, X393, appc81_in_ga(T134, X393))
U28_ga(T134, X412, X393, appc81_out_ga(T134, X393)) → appc81_out_ga(T134, cons(X412, X393))
U29_gga(T124, X337, X324, appc81_out_ga(T124, X324)) → appc63_out_gga([], T124, cons(X337, X324))
appc63_in_gga(.(T159, T161), T162, cons(T159, X324)) → U30_gga(T159, T161, T162, X324, appc63_in_gga(T161, T162, X324))
U30_gga(T159, T161, T162, X324, appc63_out_gga(T161, T162, X324)) → appc63_out_gga(.(T159, T161), T162, cons(T159, X324))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
nil = nil
[] = []
.(x1, x2) = .(x1, x2)
appc15_in_gga(x1, x2, x3) = appc15_in_gga(x1, x2)
appc15_out_gga(x1, x2, x3) = appc15_out_gga(x1, x2)
U26_gga(x1, x2, x3, x4) = U26_gga(x1, x4)
appc33_in_ga(x1, x2) = appc33_in_ga(x1)
U25_ga(x1, x2, x3, x4) = U25_ga(x1, x4)
appc33_out_ga(x1, x2) = appc33_out_ga(x1)
U27_gga(x1, x2, x3, x4, x5) = U27_gga(x1, x2, x3, x5)
appc63_in_aaa(x1, x2, x3) = appc63_in_aaa
appc63_out_aaa(x1, x2, x3) = appc63_out_aaa
U29_aaa(x1, x2, x3, x4) = U29_aaa(x4)
appc81_in_aa(x1, x2) = appc81_in_aa
U28_aa(x1, x2, x3, x4) = U28_aa(x4)
appc81_out_aa(x1, x2) = appc81_out_aa(x1)
U30_aaa(x1, x2, x3, x4, x5) = U30_aaa(x5)
appc63_in_gga(x1, x2, x3) = appc63_in_gga(x1, x2)
appc63_out_gga(x1, x2, x3) = appc63_out_gga(x1, x2)
U29_gga(x1, x2, x3, x4) = U29_gga(x1, x4)
appc81_in_ga(x1, x2) = appc81_in_ga(x1)
U28_ga(x1, x2, x3, x4) = U28_ga(x1, x4)
appc81_out_ga(x1, x2) = appc81_out_ga(x1)
U30_gga(x1, x2, x3, x4, x5) = U30_gga(x1, x2, x3, x5)
APP15_IN_GGA(x1, x2, x3) = APP15_IN_GGA(x1, x2)

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

(60) UsableRulesProof (EQUIVALENT transformation)

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

(61) Obligation:

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

APP15_IN_GGA(.(T67, T68), T38, cons(T67, X92)) → APP15_IN_GGA(T68, T38, X92)

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

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

(62) PiDPToQDPProof (SOUND transformation)

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

(63) Obligation:

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

APP15_IN_GGA(.(T67, T68), T38) → APP15_IN_GGA(T68, T38)

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

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

APP15_IN_GGA(.(T67, T68), T38) → APP15_IN_GGA(T68, T38)
The graph contains the following edges 1 > 1, 2 >= 2

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND 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) NonTerminationProof (EQUIVALENT transformation)

(13) NO

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) NonTerminationProof (EQUIVALENT transformation)

(27) NO

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) NonTerminationProof (EQUIVALENT transformation)

(34) NO

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) MRRProof (EQUIVALENT transformation)

(41) Obligation:

(42) UsableRulesProof (EQUIVALENT transformation)

(43) Obligation:

(44) QReductionProof (EQUIVALENT transformation)

(45) Obligation:

(46) Narrowing (SOUND transformation)

(47) Obligation:

(48) Narrowing (SOUND transformation)

(49) Obligation:

(50) NonTerminationProof (EQUIVALENT transformation)

(51) NO

(52) Obligation:

(53) UsableRulesProof (EQUIVALENT transformation)

(54) Obligation:

(55) PiDPToQDPProof (SOUND transformation)

(56) Obligation:

(57) NonTerminationProof (EQUIVALENT transformation)

(58) NO

(59) Obligation:

(60) UsableRulesProof (EQUIVALENT transformation)

(61) Obligation:

(62) PiDPToQDPProof (SOUND transformation)

(63) Obligation:

(64) QDPSizeChangeProof (EQUIVALENT transformation)

(65) YES