Left Termination proof of /tmp/tmp6lxkNH/plumer356.pl

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

    ↳3 PrologToPiTRSProof (⇐)

        ↳4 PiTRS

            ↳5 DependencyPairsProof (⇔)

                ↳6 PiDP

                    ↳7 DependencyGraphProof (⇔)

                        ↳8 PiDP

                            ↳9 UsableRulesProof (⇔)

                                ↳10 PiDP

                                    ↳11 PiDPToQDPProof (⇐)

                                        ↳12 QDP

                                            ↳13 NonTerminationProof (⇔)

                                                ↳14 FALSE

    ↳15 PrologToPiTRSProof (⇐)

        ↳16 PiTRS

            ↳17 DependencyPairsProof (⇔)

                ↳18 PiDP

                    ↳19 DependencyGraphProof (⇔)

                        ↳20 PiDP

                            ↳21 UsableRulesProof (⇔)

                                ↳22 PiDP

                                    ↳23 PiDPToQDPProof (⇐)

                                        ↳24 QDP

                                            ↳25 NonTerminationProof (⇔)

                                                ↳26 FALSE

(0) Obligation:

Clauses:

p(X) :- ','(l(X), ','(!, q(X))).
q(.(A, [])).
r(1).
l([]).
l(.(H, T)) :- ','(r(H), l(T)).

Queries:

p(a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: p(T1)\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: p(T1), SCOPE: 1, CLAUSE: 0 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(l(T3), ','(!_1, q(T3))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(l(T3), ','(!_1, q(T3))), SCOPE: 2, CLAUSE: 3 | ','(l(T3), ','(!_1, q(T3))), SCOPE: 2, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(!_1, q([])) | ','(l(T3), ','(!_1, q(T3))), SCOPE: 2, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(l(T3), ','(!_1, q(T3))), SCOPE: 2, CLAUSE: 4 | ?_1\n\nl(T3) !=? l([])", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: q([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: q([]), SCOPE: 3, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(r(T6), ','(l(T7), ','(!_1, q(.(T6, T7))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\nX6 is free\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(r(T6), ','(l(T7), ','(!_1, q(.(T6, T7))))), SCOPE: 4, CLAUSE: 2 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(l(T8), ','(!_1, q(.(1, T8)))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(l(T8), ','(!_1, q(.(1, T8)))), SCOPE: 5, CLAUSE: 3 | ','(l(T8), ','(!_1, q(.(1, T8)))), SCOPE: 5, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(!_1, q(.(1, []))) | ','(l(T8), ','(!_1, q(.(1, T8)))), SCOPE: 5, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(l(T8), ','(!_1, q(.(1, T8)))), SCOPE: 5, CLAUSE: 4 | ?_1\n\nl(T8) !=? l([])", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: q(.(1, []))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: q(.(1, [])), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(r(T11), ','(l(T12), ','(!_1, q(.(1, .(T11, T12)))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\nX12 is free\nX13 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(r(T11), ','(l(T12), ','(!_1, q(.(1, .(T11, T12)))))), SCOPE: 7, CLAUSE: 2 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(l(T13), ','(!_1, q(.(1, .(1, T13))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(l(T13), ','(!_1, q(.(1, .(1, T13))))), SCOPE: 8, CLAUSE: 3 | ','(l(T13), ','(!_1, q(.(1, .(1, T13))))), SCOPE: 8, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(!_1, q(.(1, .(1, [])))) | ','(l(T13), ','(!_1, q(.(1, .(1, T13))))), SCOPE: 8, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(l(T13), ','(!_1, q(.(1, .(1, T13))))), SCOPE: 8, CLAUSE: 4 | ?_1\n\nl(T13) !=? l([])", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: q(.(1, .(1, [])))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: q(.(1, .(1, []))), SCOPE: 9, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(r(T16), ','(l(T17), ','(!_1, q(.(1, .(1, .(T16, T17))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\nX17 is free\nX18 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(r(T16), ','(l(T17), ','(!_1, q(.(1, .(1, .(T16, T17))))))), SCOPE: 10, CLAUSE: 2 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(l(T18), ','(!_1, q(.(1, .(1, .(1, T18)))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(l(T18), ','(!_1, q(.(1, .(1, .(1, T18)))))), SCOPE: 11, CLAUSE: 3 | ','(l(T18), ','(!_1, q(.(1, .(1, .(1, T18)))))), SCOPE: 11, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(!_1, q(.(1, .(1, .(1, []))))) | ','(l(T18), ','(!_1, q(.(1, .(1, .(1, T18)))))), SCOPE: 11, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(l(T18), ','(!_1, q(.(1, .(1, .(1, T18)))))), SCOPE: 11, CLAUSE: 4 | ?_1\n\nl(T18) !=? l([])", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: q(.(1, .(1, .(1, []))))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: q(.(1, .(1, .(1, [])))), SCOPE: 12, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(r(T21), ','(l(T22), ','(!_1, q(.(1, .(1, .(1, .(T21, T22)))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\nX22 is free\nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(r(T21), ','(l(T22), ','(!_1, q(.(1, .(1, .(1, .(T21, T22)))))))), SCOPE: 13, CLAUSE: 2 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(l(T23), ','(!_1, q(.(1, .(1, .(1, .(1, T23))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(l(T23), ','(!_1, q(.(1, .(1, .(1, .(1, T23))))))), SCOPE: 14, CLAUSE: 3 | ','(l(T23), ','(!_1, q(.(1, .(1, .(1, .(1, T23))))))), SCOPE: 14, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(!_1, q(.(1, .(1, .(1, .(1, [])))))) | ','(l(T23), ','(!_1, q(.(1, .(1, .(1, .(1, T23))))))), SCOPE: 14, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(l(T23), ','(!_1, q(.(1, .(1, .(1, .(1, T23))))))), SCOPE: 14, CLAUSE: 4 | ?_1\n\nl(T23) !=? l([])", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: q(.(1, .(1, .(1, .(1, [])))))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: q(.(1, .(1, .(1, .(1, []))))), SCOPE: 15, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(r(T26), ','(l(T27), ','(!_1, q(.(1, .(1, .(1, .(1, .(T26, T27))))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\nX27 is free\nX28 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(r(T26), ','(l(T27), ','(!_1, q(.(1, .(1, .(1, .(1, .(T26, T27))))))))), SCOPE: 16, CLAUSE: 2 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(l(T28), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, T28)))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(l(T28), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, T28)))))))), SCOPE: 17, CLAUSE: 3 | ','(l(T28), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, T28)))))))), SCOPE: 17, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(!_1, q(.(1, .(1, .(1, .(1, .(1, []))))))) | ','(l(T28), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, T28)))))))), SCOPE: 17, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(l(T28), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, T28)))))))), SCOPE: 17, CLAUSE: 4 | ?_1\n\nl(T28) !=? l([])", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: q(.(1, .(1, .(1, .(1, .(1, []))))))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: q(.(1, .(1, .(1, .(1, .(1, [])))))), SCOPE: 18, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(r(T31), ','(l(T32), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(T31, T32)))))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\nX32 is free\nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(r(T31), ','(l(T32), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(T31, T32)))))))))), SCOPE: 19, CLAUSE: 2 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(l(T33), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, T33))))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(l(T33), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, T33))))))))), SCOPE: 20, CLAUSE: 3 | ','(l(T33), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, T33))))))))), SCOPE: 20, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, [])))))))) | ','(l(T33), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, T33))))))))), SCOPE: 20, CLAUSE: 4 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(l(T33), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, T33))))))))), SCOPE: 20, CLAUSE: 4 | ?_1\n\nl(T33) !=? l([])", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: q(.(1, .(1, .(1, .(1, .(1, .(1, [])))))))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: q(.(1, .(1, .(1, .(1, .(1, .(1, []))))))), SCOPE: 21, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(r(T36), ','(l(T37), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, .(T36, T37))))))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\nX37 is free\nX38 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(r(T36), ','(l(T37), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, .(T36, T37))))))))))), SCOPE: 22, CLAUSE: 2 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(l(T38), ','(!_1, q(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))))) | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(l(T38), ','(!_1, q(.(T39, T40))))\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: l(T38)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(!_1, q(.(T39, T41)))\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: l(T38), SCOPE: 23, CLAUSE: 3 | l(T38), SCOPE: 23, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: l(T38), SCOPE: 23, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: l(T38), SCOPE: 23, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(r(T44), l(T45))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\nX41 is free\nX42 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(r(T44), l(T45)), SCOPE: 24, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: l(T46)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: q(.(T39, T41))\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: q(.(T39, T41)), SCOPE: 25, CLAUSE: 1\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 101 [arrowhead = none ];
101 -> 2;

102 [label="EVAL with clause\np(X2) :- ','(l(X2), ','(!, q(X2))).\nand substitution\nT1 -> T3\nX2 -> T3\nT2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 102 [arrowhead = none ];
102 -> 3;

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

104 [label="EVAL with clause\nl([]).\nand substitution\nT3 -> []", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 104 [arrowhead = none ];
104 -> 5;

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

106 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 106 [arrowhead = none ];
106 -> 7;

107 [label="EVAL with clause\nl(.(X6, X7)) :- ','(r(X6), l(X7)).\nand substitution\nX6 -> T6\nX7 -> T7\nT3 -> .(T6, T7)\nT4 -> T6\nT5 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 107 [arrowhead = none ];
107 -> 10;

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

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

110 [label="BACKTRACK\nfor clause: q(.(A, []))because of non-unification", fontsize=14, style = filled, fillcolor = white];
8 -> 110 [arrowhead = none ];
110 -> 9;

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

112 [label="EVAL with clause\nr(1).\nand substitution\nT6 -> 1\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 112 [arrowhead = none ];
112 -> 13;

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

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

115 [label="EVAL with clause\nl([]).\nand substitution\nT8 -> []", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 115 [arrowhead = none ];
115 -> 16;

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

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

118 [label="EVAL with clause\nl(.(X12, X13)) :- ','(r(X12), l(X13)).\nand substitution\nX12 -> T11\nX13 -> T12\nT8 -> .(T11, T12)\nT9 -> T11\nT10 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 118 [arrowhead = none ];
118 -> 22;

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

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

121 [label="EVAL with clause\nq(.(X9, [])).\nand substitution\nX9 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 121 [arrowhead = none ];
121 -> 20;

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

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

124 [label="EVAL with clause\nr(1).\nand substitution\nT11 -> 1\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 124 [arrowhead = none ];
124 -> 25;

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

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

127 [label="EVAL with clause\nl([]).\nand substitution\nT13 -> []", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 127 [arrowhead = none ];
127 -> 28;

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

129 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 129 [arrowhead = none ];
129 -> 30;

130 [label="EVAL with clause\nl(.(X17, X18)) :- ','(r(X17), l(X18)).\nand substitution\nX17 -> T16\nX18 -> T17\nT13 -> .(T16, T17)\nT14 -> T16\nT15 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 130 [arrowhead = none ];
130 -> 33;

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

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

133 [label="BACKTRACK\nfor clause: q(.(A, []))because of non-unification", fontsize=14, style = filled, fillcolor = white];
31 -> 133 [arrowhead = none ];
133 -> 32;

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

135 [label="EVAL with clause\nr(1).\nand substitution\nT16 -> 1\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 135 [arrowhead = none ];
135 -> 36;

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

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

138 [label="EVAL with clause\nl([]).\nand substitution\nT18 -> []", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 138 [arrowhead = none ];
138 -> 39;

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

140 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 140 [arrowhead = none ];
140 -> 41;

141 [label="EVAL with clause\nl(.(X22, X23)) :- ','(r(X22), l(X23)).\nand substitution\nX22 -> T21\nX23 -> T22\nT18 -> .(T21, T22)\nT19 -> T21\nT20 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 141 [arrowhead = none ];
141 -> 44;

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

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

144 [label="BACKTRACK\nfor clause: q(.(A, []))because of non-unification", fontsize=14, style = filled, fillcolor = white];
42 -> 144 [arrowhead = none ];
144 -> 43;

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

146 [label="EVAL with clause\nr(1).\nand substitution\nT21 -> 1\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 146 [arrowhead = none ];
146 -> 47;

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

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

149 [label="EVAL with clause\nl([]).\nand substitution\nT23 -> []", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 149 [arrowhead = none ];
149 -> 50;

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

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

152 [label="EVAL with clause\nl(.(X27, X28)) :- ','(r(X27), l(X28)).\nand substitution\nX27 -> T26\nX28 -> T27\nT23 -> .(T26, T27)\nT24 -> T26\nT25 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 152 [arrowhead = none ];
152 -> 55;

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

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

155 [label="BACKTRACK\nfor clause: q(.(A, []))because of non-unification", fontsize=14, style = filled, fillcolor = white];
53 -> 155 [arrowhead = none ];
155 -> 54;

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

157 [label="EVAL with clause\nr(1).\nand substitution\nT26 -> 1\nT27 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 157 [arrowhead = none ];
157 -> 58;

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

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

160 [label="EVAL with clause\nl([]).\nand substitution\nT28 -> []", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 160 [arrowhead = none ];
160 -> 61;

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

162 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 162 [arrowhead = none ];
162 -> 63;

163 [label="EVAL with clause\nl(.(X32, X33)) :- ','(r(X32), l(X33)).\nand substitution\nX32 -> T31\nX33 -> T32\nT28 -> .(T31, T32)\nT29 -> T31\nT30 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 163 [arrowhead = none ];
163 -> 66;

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

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

166 [label="BACKTRACK\nfor clause: q(.(A, []))because of non-unification", fontsize=14, style = filled, fillcolor = white];
64 -> 166 [arrowhead = none ];
166 -> 65;

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

168 [label="EVAL with clause\nr(1).\nand substitution\nT31 -> 1\nT32 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 168 [arrowhead = none ];
168 -> 69;

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

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

171 [label="EVAL with clause\nl([]).\nand substitution\nT33 -> []", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 171 [arrowhead = none ];
171 -> 72;

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

173 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 173 [arrowhead = none ];
173 -> 74;

174 [label="EVAL with clause\nl(.(X37, X38)) :- ','(r(X37), l(X38)).\nand substitution\nX37 -> T36\nX38 -> T37\nT33 -> .(T36, T37)\nT34 -> T36\nT35 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 174 [arrowhead = none ];
174 -> 77;

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

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

177 [label="BACKTRACK\nfor clause: q(.(A, []))because of non-unification", fontsize=14, style = filled, fillcolor = white];
75 -> 177 [arrowhead = none ];
177 -> 76;

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

179 [label="EVAL with clause\nr(1).\nand substitution\nT36 -> 1\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 179 [arrowhead = none ];
179 -> 80;

180 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 180 [arrowhead = none ];
180 -> 81;

181 [label="GENERALIZATION\nT39 <-- 1\nT40 <-- .(1, .(1, .(1, .(1, .(1, .(1, T38))))))\n\nNew Knowledge:\nT39 is ground", fontsize=14, style = filled, fillcolor = violet];
80 -> 181 [arrowhead = none ];
181 -> 82;

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

183 [label="SPLIT 2\nnew knowledge:\nT38 is ground\nreplacements:\nT40 -> T41", fontsize=14, style = filled, fillcolor = violet];
82 -> 183 [arrowhead = none ];
183 -> 84;

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

185 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 185 [arrowhead = none ];
185 -> 96;

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

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

188 [label="EVAL with clause\nl([]).\nand substitution\nT38 -> []", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 188 [arrowhead = none ];
188 -> 88;

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

190 [label="EVAL with clause\nl(.(X41, X42)) :- ','(r(X41), l(X42)).\nand substitution\nX41 -> T44\nX42 -> T45\nT38 -> .(T44, T45)\nT42 -> T44\nT43 -> T45", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 190 [arrowhead = none ];
190 -> 91;

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

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

193 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 193 [arrowhead = none ];
193 -> 93;

194 [label="EVAL with clause\nr(1).\nand substitution\nT44 -> 1\nT45 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 194 [arrowhead = none ];
194 -> 94;

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

196 [label="INSTANCE with matching:\nT38 -> T46", fontsize=14, style = filled, fillcolor = lightgrey];
94 -> 196 [arrowhead = none , style=dashed];
196 -> 83[style=dashed];

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

198 [label="EVAL with clause\nq(.(X44, [])).\nand substitution\nT39 -> T47\nX44 -> T47\nT41 -> []", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 198 [arrowhead = none ];
198 -> 98;

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

200 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 200 [arrowhead = none ];
200 -> 100;

}

(2) Obligation:

Clauses:

l83([]).
l83(.(1, T46)) :- l83(T46).
p1(.(1, [])).
p1(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) :- l83(T38).
p1(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) :- l83(T38).

Queries:

p1(a).

(3) PrologToPiTRSProof (SOUND transformation)

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

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

(5) DependencyPairsProof (EQUIVALENT transformation)

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

P1_IN_A(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_A(T38, l83_in_a(T38))
P1_IN_A(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → L83_IN_A(T38)
L83_IN_A(.(1, T46)) → U1_A(T46, l83_in_a(T46))
L83_IN_A(.(1, T46)) → L83_IN_A(T46)

The TRS R consists of the following rules:

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

The argument filtering Pi contains the following mapping:
p1_in_a(x1) = p1_in_a
p1_out_a(x1) = p1_out_a(x1)
U2_a(x1, x2) = U2_a(x2)
l83_in_a(x1) = l83_in_a
l83_out_a(x1) = l83_out_a(x1)
U1_a(x1, x2) = U1_a(x2)
.(x1, x2) = .(x1, x2)
1 = 1
P1_IN_A(x1) = P1_IN_A
U2_A(x1, x2) = U2_A(x2)
L83_IN_A(x1) = L83_IN_A
U1_A(x1, x2) = U1_A(x2)

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

(6) Obligation:

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

P1_IN_A(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_A(T38, l83_in_a(T38))
P1_IN_A(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → L83_IN_A(T38)
L83_IN_A(.(1, T46)) → U1_A(T46, l83_in_a(T46))
L83_IN_A(.(1, T46)) → L83_IN_A(T46)

The TRS R consists of the following rules:

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(8) Obligation:

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

L83_IN_A(.(1, T46)) → L83_IN_A(T46)

The TRS R consists of the following rules:

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

The argument filtering Pi contains the following mapping:
p1_in_a(x1) = p1_in_a
p1_out_a(x1) = p1_out_a(x1)
U2_a(x1, x2) = U2_a(x2)
l83_in_a(x1) = l83_in_a
l83_out_a(x1) = l83_out_a(x1)
U1_a(x1, x2) = U1_a(x2)
.(x1, x2) = .(x1, x2)
1 = 1
L83_IN_A(x1) = L83_IN_A

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

(9) UsableRulesProof (EQUIVALENT transformation)

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

(10) Obligation:

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

L83_IN_A(.(1, T46)) → L83_IN_A(T46)

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

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

(11) PiDPToQDPProof (SOUND transformation)

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

(12) Obligation:

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

L83_IN_A → L83_IN_A

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

(13) 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 = L83_IN_A evaluates to t =L83_IN_A

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 L83_IN_A to L83_IN_A.

(14) FALSE

(15) PrologToPiTRSProof (SOUND transformation)

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(16) Obligation:

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

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

(17) DependencyPairsProof (EQUIVALENT transformation)

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

P1_IN_A(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_A(T38, l83_in_a(T38))
P1_IN_A(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → L83_IN_A(T38)
L83_IN_A(.(1, T46)) → U1_A(T46, l83_in_a(T46))
L83_IN_A(.(1, T46)) → L83_IN_A(T46)

The TRS R consists of the following rules:

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

(18) Obligation:

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

P1_IN_A(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_A(T38, l83_in_a(T38))
P1_IN_A(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → L83_IN_A(T38)
L83_IN_A(.(1, T46)) → U1_A(T46, l83_in_a(T46))
L83_IN_A(.(1, T46)) → L83_IN_A(T46)

The TRS R consists of the following rules:

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

(19) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(20) Obligation:

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

L83_IN_A(.(1, T46)) → L83_IN_A(T46)

The TRS R consists of the following rules:

p1_in_a(.(1, [])) → p1_out_a(.(1, []))
p1_in_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38)))))))) → U2_a(T38, l83_in_a(T38))
l83_in_a([]) → l83_out_a([])
l83_in_a(.(1, T46)) → U1_a(T46, l83_in_a(T46))
U1_a(T46, l83_out_a(T46)) → l83_out_a(.(1, T46))
U2_a(T38, l83_out_a(T38)) → p1_out_a(.(1, .(1, .(1, .(1, .(1, .(1, .(1, T38))))))))

The argument filtering Pi contains the following mapping:
p1_in_a(x1) = p1_in_a
p1_out_a(x1) = p1_out_a(x1)
U2_a(x1, x2) = U2_a(x2)
l83_in_a(x1) = l83_in_a
l83_out_a(x1) = l83_out_a(x1)
U1_a(x1, x2) = U1_a(x2)
.(x1, x2) = .(x1, x2)
1 = 1
L83_IN_A(x1) = L83_IN_A

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

(21) UsableRulesProof (EQUIVALENT transformation)

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

(22) Obligation:

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

L83_IN_A(.(1, T46)) → L83_IN_A(T46)

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

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

(23) PiDPToQDPProof (SOUND transformation)

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

(24) Obligation:

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

L83_IN_A → L83_IN_A

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

(25) NonTerminationProof (EQUIVALENT transformation)

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

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

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Obligation:

(9) UsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

(11) PiDPToQDPProof (SOUND transformation)

(12) Obligation:

(13) NonTerminationProof (EQUIVALENT transformation)

(14) FALSE

(15) PrologToPiTRSProof (SOUND transformation)

(16) Obligation:

(17) DependencyPairsProof (EQUIVALENT transformation)

(18) Obligation:

(19) DependencyGraphProof (EQUIVALENT transformation)

(20) Obligation:

(21) UsableRulesProof (EQUIVALENT transformation)

(22) Obligation:

(23) PiDPToQDPProof (SOUND transformation)

(24) Obligation:

(25) NonTerminationProof (EQUIVALENT transformation)

(26) FALSE