Left Termination proof of /tmp/tmp5obk6g/NJ4.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 163 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 26 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 PiDP

↳7 UsableRulesProof (⇔, 0 ms)

↳8 PiDP

↳9 PiDPToQDPProof (⇒, 25 ms)

↳10 QDP

↳11 QDPSizeChangeProof (⇔, 0 ms)

↳12 YES

(0) Obligation:

Clauses:

p(M, N, s(R), RES) :- p(M, R, N, RES).
p(M, s(N), R, RES) :- p(R, N, M, RES).
p(M, X1, X2, M).

Query: p(g,g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: p(T1, T2, T3, T4)\n\nT1 is ground\nT2 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: p(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 0 | p(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 1 | p(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: p(T9, T11, T10, T13) | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 1 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: p(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 1 | p(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nT3 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T1, T2, T3, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 0 | p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 1 | p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 2 | ?_2 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 1 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 0\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 1 | p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 2 | ?_2 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 1 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: p(T30, T32, T31, T34)\n\nT30 is ground\nT31 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 2 | ?_2 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 1 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: p(T57, T56, T55, T59)\n\nT55 is ground\nT56 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: p(T9, T11, T10, T13), SCOPE: 2, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ?_2 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 1 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 1 | p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 1\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: p(T9, T10, s(T11), T4), SCOPE: 1, CLAUSE: 2\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: p(s(T97), T96, T95, T99)\n\nT95 is ground\nT96 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: p(T119, T118, T117, T121) | p(T117, s(T118), T119, T4), SCOPE: 1, CLAUSE: 2\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: p(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nT3 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\nX111 is free\nX112 is free\nX113 is free\nX114 is free\np(T1, T2, T3, T4) !=? p(X7, X8, s(X9), X10)\np(T1, T2, T3, T4) !=? p(X111, s(X112), X113, X114)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 0 | p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 1 | p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 2 | ?_3 | p(T117, s(T118), T119, T4), SCOPE: 1, CLAUSE: 2\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 0\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 1 | p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 2 | ?_3 | p(T117, s(T118), T119, T4), SCOPE: 1, CLAUSE: 2\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: p(T138, T140, T139, T142)\n\nT138 is ground\nT139 is ground\nT140 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(s(T140), s(T139), T138, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 1\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 2 | ?_3 | p(T117, s(T118), T119, T4), SCOPE: 1, CLAUSE: 2\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: p(T165, T164, T163, T167)\n\nT163 is ground\nT164 is ground\nT165 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T165, s(s(T164)), T163, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: p(T119, T118, T117, T121), SCOPE: 3, CLAUSE: 2\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ?_3 | p(T117, s(T118), T119, T4), SCOPE: 1, CLAUSE: 2\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: p(T117, s(T118), T119, T4), SCOPE: 1, CLAUSE: 2\n\nT117 is ground\nT118 is ground\nT119 is ground\nX7 is free\nX8 is free\nX9 is free\nX10 is free\np(T117, s(T118), T119, T4) !=? p(X7, X8, s(X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 128 [arrowhead = none ];
128 -> 4;

129 [label="EVAL with clause\np(X7, X8, s(X9), X10) :- p(X7, X9, X8, X10).\nand substitutionT1 -> T9,\nX7 -> T9,\nT2 -> T10,\nX8 -> T10,\nX9 -> T11,\nT3 -> s(T11),\nT4 -> T13,\nX10 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 129 [arrowhead = none ];
129 -> 10;

130 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 130 [arrowhead = none ];
130 -> 13;

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

132 [label="EVAL with clause\np(X111, s(X112), X113, X114) :- p(X113, X112, X111, X114).\nand substitutionT1 -> T117,\nX111 -> T117,\nX112 -> T118,\nT2 -> s(T118),\nT3 -> T119,\nX113 -> T119,\nT4 -> T121,\nX114 -> T121,\nT120 -> T121", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 132 [arrowhead = none ];
132 -> 63;

133 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 133 [arrowhead = none ];
133 -> 64;

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

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

136 [label="EVAL with clause\np(X27, X28, s(X29), X30) :- p(X27, X29, X28, X30).\nand substitutionT9 -> T30,\nX27 -> T30,\nT11 -> T31,\nX28 -> T31,\nX29 -> T32,\nT10 -> s(T32),\nT13 -> T34,\nX30 -> T34,\nT33 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 136 [arrowhead = none ];
136 -> 21;

137 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 137 [arrowhead = none ];
137 -> 22;

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

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

140 [label="INSTANCE with matching:\nT1 -> T30\nT2 -> T32\nT3 -> T31\nT4 -> T34", fontsize=14, style = filled, fillcolor = lightgrey];
21 -> 140 [arrowhead = none , style=dashed];
140 -> 2[style=dashed];

141 [label="EVAL with clause\np(X51, s(X52), X53, X54) :- p(X53, X52, X51, X54).\nand substitutionT9 -> T55,\nX51 -> T55,\nX52 -> T56,\nT11 -> s(T56),\nT10 -> T57,\nX53 -> T57,\nT13 -> T59,\nX54 -> T59,\nT58 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 141 [arrowhead = none ];
141 -> 34;

142 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 142 [arrowhead = none ];
142 -> 35;

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

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

145 [label="INSTANCE with matching:\nT1 -> T57\nT2 -> T56\nT3 -> T55\nT4 -> T59", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 145 [arrowhead = none , style=dashed];
145 -> 2[style=dashed];

146 [label="EVAL with clause\np(X71, X72, X73, X71).\nand substitutionT9 -> T76,\nX71 -> T76,\nT11 -> T77,\nX72 -> T77,\nT10 -> T78,\nX73 -> T78,\nT13 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 146 [arrowhead = none ];
146 -> 38;

147 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 147 [arrowhead = none ];
147 -> 39;

148 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 148 [arrowhead = none ];
148 -> 41;

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

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

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

152 [label="EVAL with clause\np(X90, s(X91), X92, X93) :- p(X92, X91, X90, X93).\nand substitutionT9 -> T95,\nX90 -> T95,\nX91 -> T96,\nT10 -> s(T96),\nT11 -> T97,\nX92 -> s(T97),\nT4 -> T99,\nX93 -> T99,\nT98 -> T99", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 152 [arrowhead = none ];
152 -> 50;

153 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 153 [arrowhead = none ];
153 -> 59;

154 [label="EVAL with clause\np(X104, X105, X106, X104).\nand substitutionT9 -> T110,\nX104 -> T110,\nT10 -> T111,\nX105 -> T111,\nT11 -> T112,\nX106 -> s(T112),\nT4 -> T110", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 154 [arrowhead = none ];
154 -> 60;

155 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 155 [arrowhead = none ];
155 -> 61;

156 [label="INSTANCE with matching:\nT1 -> s(T97)\nT2 -> T96\nT3 -> T95\nT4 -> T99", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 156 [arrowhead = none , style=dashed];
156 -> 2[style=dashed];

157 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 157 [arrowhead = none ];
157 -> 62;

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

159 [label="EVAL with clause\np(X194, X195, X196, X194).\nand substitutionT1 -> T203,\nX194 -> T203,\nT2 -> T204,\nX195 -> T204,\nT3 -> T205,\nX196 -> T205,\nT4 -> T203", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 159 [arrowhead = none ];
159 -> 124;

160 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 160 [arrowhead = none ];
160 -> 126;

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

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

163 [label="EVAL with clause\np(X131, X132, s(X133), X134) :- p(X131, X133, X132, X134).\nand substitutionT119 -> T138,\nX131 -> T138,\nT118 -> T139,\nX132 -> T139,\nX133 -> T140,\nT117 -> s(T140),\nT121 -> T142,\nX134 -> T142,\nT141 -> T142", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 163 [arrowhead = none ];
163 -> 74;

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

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

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

167 [label="INSTANCE with matching:\nT1 -> T138\nT2 -> T140\nT3 -> T139\nT4 -> T142", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 167 [arrowhead = none , style=dashed];
167 -> 2[style=dashed];

168 [label="EVAL with clause\np(X155, s(X156), X157, X158) :- p(X157, X156, X155, X158).\nand substitutionT119 -> T163,\nX155 -> T163,\nX156 -> T164,\nT118 -> s(T164),\nT117 -> T165,\nX157 -> T165,\nT121 -> T167,\nX158 -> T167,\nT166 -> T167", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 168 [arrowhead = none ];
168 -> 86;

169 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 169 [arrowhead = none ];
169 -> 87;

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

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

172 [label="INSTANCE with matching:\nT1 -> T165\nT2 -> T164\nT3 -> T163\nT4 -> T167", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 172 [arrowhead = none , style=dashed];
172 -> 2[style=dashed];

173 [label="EVAL with clause\np(X179, X180, X181, X179).\nand substitutionT119 -> T188,\nX179 -> T188,\nT118 -> T189,\nX180 -> T189,\nT117 -> T190,\nX181 -> T190,\nT121 -> T188", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 173 [arrowhead = none ];
173 -> 92;

174 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 174 [arrowhead = none ];
174 -> 93;

175 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 175 [arrowhead = none ];
175 -> 99;

176 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 176 [arrowhead = none ];
176 -> 96;

177 [label="EVAL with clause\np(X188, X189, X190, X188).\nand substitutionT117 -> T197,\nX188 -> T197,\nT118 -> T198,\nX189 -> s(T198),\nT119 -> T199,\nX190 -> T199,\nT4 -> T197", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 177 [arrowhead = none ];
177 -> 118;

178 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 178 [arrowhead = none ];
178 -> 120;

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

180 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 180 [arrowhead = none ];
180 -> 127;

}

(2) Obligation:

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

pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

PA_IN_GGGA(T30, s(T32), s(T31), T34) → U1_GGGA(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
PA_IN_GGGA(T30, s(T32), s(T31), T34) → PA_IN_GGGA(T30, T32, T31, T34)
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → U2_GGGA(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → PA_IN_GGGA(T57, T56, T55, T59)
PA_IN_GGGA(T95, s(T96), s(T97), T99) → U3_GGGA(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
PA_IN_GGGA(T95, s(T96), s(T97), T99) → PA_IN_GGGA(s(T97), T96, T95, T99)
PA_IN_GGGA(s(T140), s(T139), T138, T142) → U4_GGGA(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
PA_IN_GGGA(s(T140), s(T139), T138, T142) → PA_IN_GGGA(T138, T140, T139, T142)
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → U5_GGGA(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → PA_IN_GGGA(T165, T164, T163, T167)

The TRS R consists of the following rules:

pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)

The argument filtering Pi contains the following mapping:
pA_in_ggga(x1, x2, x3, x4) = pA_in_ggga(x1, x2, x3)
s(x1) = s(x1)
U1_ggga(x1, x2, x3, x4, x5) = U1_ggga(x1, x2, x3, x5)
U2_ggga(x1, x2, x3, x4, x5) = U2_ggga(x1, x2, x3, x5)
pA_out_ggga(x1, x2, x3, x4) = pA_out_ggga(x1, x2, x3, x4)
U3_ggga(x1, x2, x3, x4, x5) = U3_ggga(x1, x2, x3, x5)
U4_ggga(x1, x2, x3, x4, x5) = U4_ggga(x1, x2, x3, x5)
U5_ggga(x1, x2, x3, x4, x5) = U5_ggga(x1, x2, x3, x5)
PA_IN_GGGA(x1, x2, x3, x4) = PA_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5) = U1_GGGA(x1, x2, x3, x5)
U2_GGGA(x1, x2, x3, x4, x5) = U2_GGGA(x1, x2, x3, x5)
U3_GGGA(x1, x2, x3, x4, x5) = U3_GGGA(x1, x2, x3, x5)
U4_GGGA(x1, x2, x3, x4, x5) = U4_GGGA(x1, x2, x3, x5)
U5_GGGA(x1, x2, x3, x4, x5) = U5_GGGA(x1, x2, x3, x5)

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

(4) Obligation:

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

PA_IN_GGGA(T30, s(T32), s(T31), T34) → U1_GGGA(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
PA_IN_GGGA(T30, s(T32), s(T31), T34) → PA_IN_GGGA(T30, T32, T31, T34)
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → U2_GGGA(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → PA_IN_GGGA(T57, T56, T55, T59)
PA_IN_GGGA(T95, s(T96), s(T97), T99) → U3_GGGA(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
PA_IN_GGGA(T95, s(T96), s(T97), T99) → PA_IN_GGGA(s(T97), T96, T95, T99)
PA_IN_GGGA(s(T140), s(T139), T138, T142) → U4_GGGA(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
PA_IN_GGGA(s(T140), s(T139), T138, T142) → PA_IN_GGGA(T138, T140, T139, T142)
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → U5_GGGA(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → PA_IN_GGGA(T165, T164, T163, T167)

The TRS R consists of the following rules:

pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

PA_IN_GGGA(T55, T57, s(s(T56)), T59) → PA_IN_GGGA(T57, T56, T55, T59)
PA_IN_GGGA(T30, s(T32), s(T31), T34) → PA_IN_GGGA(T30, T32, T31, T34)
PA_IN_GGGA(T95, s(T96), s(T97), T99) → PA_IN_GGGA(s(T97), T96, T95, T99)
PA_IN_GGGA(s(T140), s(T139), T138, T142) → PA_IN_GGGA(T138, T140, T139, T142)
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → PA_IN_GGGA(T165, T164, T163, T167)

The TRS R consists of the following rules:

pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

PA_IN_GGGA(T55, T57, s(s(T56)), T59) → PA_IN_GGGA(T57, T56, T55, T59)
PA_IN_GGGA(T30, s(T32), s(T31), T34) → PA_IN_GGGA(T30, T32, T31, T34)
PA_IN_GGGA(T95, s(T96), s(T97), T99) → PA_IN_GGGA(s(T97), T96, T95, T99)
PA_IN_GGGA(s(T140), s(T139), T138, T142) → PA_IN_GGGA(T138, T140, T139, T142)
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → PA_IN_GGGA(T165, T164, T163, T167)

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

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

(9) PiDPToQDPProof (SOUND transformation)

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

(10) Obligation:

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

PA_IN_GGGA(T55, T57, s(s(T56))) → PA_IN_GGGA(T57, T56, T55)
PA_IN_GGGA(T30, s(T32), s(T31)) → PA_IN_GGGA(T30, T32, T31)
PA_IN_GGGA(T95, s(T96), s(T97)) → PA_IN_GGGA(s(T97), T96, T95)
PA_IN_GGGA(s(T140), s(T139), T138) → PA_IN_GGGA(T138, T140, T139)
PA_IN_GGGA(T165, s(s(T164)), T163) → PA_IN_GGGA(T165, T164, T163)

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

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

PA_IN_GGGA(T55, T57, s(s(T56))) → PA_IN_GGGA(T57, T56, T55)
The graph contains the following edges 2 >= 1, 3 > 2, 1 >= 3
PA_IN_GGGA(T30, s(T32), s(T31)) → PA_IN_GGGA(T30, T32, T31)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3
PA_IN_GGGA(T95, s(T96), s(T97)) → PA_IN_GGGA(s(T97), T96, T95)
The graph contains the following edges 3 >= 1, 2 > 2, 1 >= 3
PA_IN_GGGA(s(T140), s(T139), T138) → PA_IN_GGGA(T138, T140, T139)
The graph contains the following edges 3 >= 1, 1 > 2, 2 > 3
PA_IN_GGGA(T165, s(s(T164)), T163) → PA_IN_GGGA(T165, T164, T163)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Obligation:

(7) UsableRulesProof (EQUIVALENT transformation)

(8) Obligation:

(9) PiDPToQDPProof (SOUND transformation)

(10) Obligation:

(11) QDPSizeChangeProof (EQUIVALENT transformation)

(12) YES