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

(0) Obligation:

Clauses:

tree_member(X, tree(X, X1, X2)).
tree_member(X, tree(X3, Left, X4)) :- tree_member(X, Left).
tree_member(X, tree(X5, X6, Right)) :- tree_member(X, Right).

Queries:

tree_member(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: tree_member(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: tree_member(T1, T2), SCOPE: 1, CLAUSE: 0 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 1 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | tree_member(T6, T2), SCOPE: 1, CLAUSE: 1 | tree_member(T6, T2), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: tree_member(T1, T2), SCOPE: 1, CLAUSE: 1 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ntree_member(T1, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: tree_member(T6, T2), SCOPE: 1, CLAUSE: 1 | tree_member(T6, T2), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: tree_member(T13, T17) | tree_member(T13, T2), SCOPE: 1, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: tree_member(T6, T2), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\ntree_member(T6, T2) !=? tree_member(X20, tree(X21, X22, X23))", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: tree_member(T13, T17), SCOPE: 2, CLAUSE: 0 | tree_member(T13, T17), SCOPE: 2, CLAUSE: 1 | tree_member(T13, T17), SCOPE: 2, CLAUSE: 2 | ?_2 | tree_member(T13, T2), SCOPE: 1, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: tree_member(T13, T17), SCOPE: 2, CLAUSE: 0\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: tree_member(T13, T17), SCOPE: 2, CLAUSE: 1 | tree_member(T13, T17), SCOPE: 2, CLAUSE: 2 | ?_2 | tree_member(T13, T2), SCOPE: 1, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: tree_member(T13, T17), SCOPE: 2, CLAUSE: 1\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: tree_member(T13, T17), SCOPE: 2, CLAUSE: 2 | ?_2 | tree_member(T13, T2), SCOPE: 1, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: tree_member(T49, T53)\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: tree_member(T13, T17), SCOPE: 2, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ?_2 | tree_member(T13, T2), SCOPE: 1, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: tree_member(T76, T80)\n\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: tree_member(T13, T2), SCOPE: 1, CLAUSE: 2\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: tree_member(T95, T99)\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: tree_member(T110, T114)\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: tree_member(T110, T114), SCOPE: 3, CLAUSE: 0 | tree_member(T110, T114), SCOPE: 3, CLAUSE: 1 | tree_member(T110, T114), SCOPE: 3, CLAUSE: 2\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: tree_member(T110, T114), SCOPE: 3, CLAUSE: 0\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: tree_member(T110, T114), SCOPE: 3, CLAUSE: 1 | tree_member(T110, T114), SCOPE: 3, CLAUSE: 2\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: tree_member(T110, T114), SCOPE: 3, CLAUSE: 1\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: tree_member(T110, T114), SCOPE: 3, CLAUSE: 2\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: tree_member(T146, T150)\n\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: tree_member(T165, T169)\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: tree_member(T180, T184) | tree_member(T180, T2), SCOPE: 1, CLAUSE: 2\n\nT180 is ground\ntree_member(T180, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ntree_member(T1, T2) !=? tree_member(X10, tree(X10, X11, X12))\ntree_member(T1, T2) !=? tree_member(X214, tree(X215, X216, X217))", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: tree_member(T180, T184), SCOPE: 4, CLAUSE: 0 | tree_member(T180, T184), SCOPE: 4, CLAUSE: 1 | tree_member(T180, T184), SCOPE: 4, CLAUSE: 2 | ?_4 | tree_member(T180, T2), SCOPE: 1, CLAUSE: 2\n\nT180 is ground\ntree_member(T180, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: tree_member(T180, T184), SCOPE: 4, CLAUSE: 0\n\nT180 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: tree_member(T180, T184), SCOPE: 4, CLAUSE: 1 | tree_member(T180, T184), SCOPE: 4, CLAUSE: 2 | ?_4 | tree_member(T180, T2), SCOPE: 1, CLAUSE: 2\n\nT180 is ground\ntree_member(T180, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", 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: tree_member(T180, T184), SCOPE: 4, CLAUSE: 1\n\nT180 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: tree_member(T180, T184), SCOPE: 4, CLAUSE: 2 | ?_4 | tree_member(T180, T2), SCOPE: 1, CLAUSE: 2\n\nT180 is ground\ntree_member(T180, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: tree_member(T216, T220)\n\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: tree_member(T180, T184), SCOPE: 4, CLAUSE: 2\n\nT180 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ?_4 | tree_member(T180, T2), SCOPE: 1, CLAUSE: 2\n\nT180 is ground\ntree_member(T180, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: tree_member(T243, T247)\n\nT243 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: tree_member(T180, T2), SCOPE: 1, CLAUSE: 2\n\nT180 is ground\ntree_member(T180, T2) !=? tree_member(X10, tree(X10, X11, X12))", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: tree_member(T262, T266)\n\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: tree_member(T277, T281)\n\nT277 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: tree_member(T277, T281), SCOPE: 5, CLAUSE: 0 | tree_member(T277, T281), SCOPE: 5, CLAUSE: 1 | tree_member(T277, T281), SCOPE: 5, CLAUSE: 2\n\nT277 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: tree_member(T277, T281), SCOPE: 5, CLAUSE: 0\n\nT277 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: tree_member(T277, T281), SCOPE: 5, CLAUSE: 1 | tree_member(T277, T281), SCOPE: 5, CLAUSE: 2\n\nT277 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: tree_member(T277, T281), SCOPE: 5, CLAUSE: 1\n\nT277 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: tree_member(T277, T281), SCOPE: 5, CLAUSE: 2\n\nT277 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: tree_member(T313, T317)\n\nT313 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: tree_member(T332, T336)\n\nT332 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 72 [arrowhead = none ];
72 -> 2;

73 [label="EVAL with clause\ntree_member(X10, tree(X10, X11, X12)).\nand substitution\nT1 -> T6\nX10 -> T6\nX11 -> T7\nX12 -> T8\nT2 -> tree(T6, T7, T8)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 73 [arrowhead = none ];
73 -> 3;

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

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

76 [label="EVAL with clause\ntree_member(X214, tree(X215, X216, X217)) :- tree_member(X214, X216).\nand substitution\nT1 -> T180\nX214 -> T180\nX215 -> T181\nX216 -> T184\nX217 -> T183\nT2 -> tree(T181, T184, T183)\nT182 -> T184", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 76 [arrowhead = none ];
76 -> 39;

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

78 [label="EVAL with clause\ntree_member(X20, tree(X21, X22, X23)) :- tree_member(X20, X22).\nand substitution\nT6 -> T13\nX20 -> T13\nX21 -> T14\nX22 -> T17\nX23 -> T16\nT2 -> tree(T14, T17, T16)\nT15 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 78 [arrowhead = none ];
78 -> 6;

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

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

81 [label="EVAL with clause\ntree_member(X132, tree(X133, X134, X135)) :- tree_member(X132, X135).\nand substitution\nT6 -> T110\nX132 -> T110\nX133 -> T111\nX134 -> T112\nX135 -> T114\nT2 -> tree(T111, T112, T114)\nT113 -> T114", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 81 [arrowhead = none ];
81 -> 25;

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

83 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
8 -> 83 [arrowhead = none ];
83 -> 9;

84 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
8 -> 84 [arrowhead = none ];
84 -> 10;

85 [label="EVAL with clause\ntree_member(X40, tree(X40, X41, X42)).\nand substitution\nT13 -> T30\nX40 -> T30\nX41 -> T31\nX42 -> T32\nT17 -> tree(T30, T31, T32)", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 85 [arrowhead = none ];
85 -> 11;

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

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

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

89 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 89 [arrowhead = none ];
89 -> 13;

90 [label="EVAL with clause\ntree_member(X62, tree(X63, X64, X65)) :- tree_member(X62, X64).\nand substitution\nT13 -> T49\nX62 -> T49\nX63 -> T50\nX64 -> T53\nX65 -> T52\nT17 -> tree(T50, T53, T52)\nT51 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 90 [arrowhead = none ];
90 -> 16;

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

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

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

94 [label="INSTANCE with matching:\nT1 -> T49\nT2 -> T53", fontsize=14, style = filled, fillcolor = lightgrey];
16 -> 94 [arrowhead = none , style=dashed];
94 -> 1[style=dashed];

95 [label="EVAL with clause\ntree_member(X92, tree(X93, X94, X95)) :- tree_member(X92, X95).\nand substitution\nT13 -> T76\nX92 -> T76\nX93 -> T77\nX94 -> T78\nX95 -> T80\nT17 -> tree(T77, T78, T80)\nT79 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 95 [arrowhead = none ];
95 -> 20;

96 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 96 [arrowhead = none ];
96 -> 21;

97 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 97 [arrowhead = none ];
97 -> 22;

98 [label="INSTANCE with matching:\nT1 -> T76\nT2 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
20 -> 98 [arrowhead = none , style=dashed];
98 -> 1[style=dashed];

99 [label="EVAL with clause\ntree_member(X114, tree(X115, X116, X117)) :- tree_member(X114, X117).\nand substitution\nT13 -> T95\nX114 -> T95\nX115 -> T96\nX116 -> T97\nX117 -> T99\nT2 -> tree(T96, T97, T99)\nT98 -> T99", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 99 [arrowhead = none ];
99 -> 23;

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

101 [label="INSTANCE with matching:\nT1 -> T95\nT2 -> T99", fontsize=14, style = filled, fillcolor = lightgrey];
23 -> 101 [arrowhead = none , style=dashed];
101 -> 1[style=dashed];

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

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

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

105 [label="EVAL with clause\ntree_member(X152, tree(X152, X153, X154)).\nand substitution\nT110 -> T127\nX152 -> T127\nX153 -> T128\nX154 -> T129\nT114 -> tree(T127, T128, T129)", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 105 [arrowhead = none ];
105 -> 30;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 106 [arrowhead = none ];
106 -> 31;

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

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

109 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 109 [arrowhead = none ];
109 -> 32;

110 [label="EVAL with clause\ntree_member(X174, tree(X175, X176, X177)) :- tree_member(X174, X176).\nand substitution\nT110 -> T146\nX174 -> T146\nX175 -> T147\nX176 -> T150\nX177 -> T149\nT114 -> tree(T147, T150, T149)\nT148 -> T150", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 110 [arrowhead = none ];
110 -> 35;

111 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 111 [arrowhead = none ];
111 -> 36;

112 [label="EVAL with clause\ntree_member(X196, tree(X197, X198, X199)) :- tree_member(X196, X199).\nand substitution\nT110 -> T165\nX196 -> T165\nX197 -> T166\nX198 -> T167\nX199 -> T169\nT114 -> tree(T166, T167, T169)\nT168 -> T169", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 112 [arrowhead = none ];
112 -> 37;

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

114 [label="INSTANCE with matching:\nT1 -> T146\nT2 -> T150", fontsize=14, style = filled, fillcolor = lightgrey];
35 -> 114 [arrowhead = none , style=dashed];
114 -> 1[style=dashed];

115 [label="INSTANCE with matching:\nT1 -> T165\nT2 -> T169", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 115 [arrowhead = none , style=dashed];
115 -> 1[style=dashed];

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

117 [label="EVAL with clause\ntree_member(X326, tree(X327, X328, X329)) :- tree_member(X326, X329).\nand substitution\nT1 -> T277\nX326 -> T277\nX327 -> T278\nX328 -> T279\nX329 -> T281\nT2 -> tree(T278, T279, T281)\nT280 -> T281", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 117 [arrowhead = none ];
117 -> 58;

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

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

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

121 [label="EVAL with clause\ntree_member(X234, tree(X234, X235, X236)).\nand substitution\nT180 -> T197\nX234 -> T197\nX235 -> T198\nX236 -> T199\nT184 -> tree(T197, T198, T199)", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 121 [arrowhead = none ];
121 -> 44;

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

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

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

125 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 125 [arrowhead = none ];
125 -> 46;

126 [label="EVAL with clause\ntree_member(X256, tree(X257, X258, X259)) :- tree_member(X256, X258).\nand substitution\nT180 -> T216\nX256 -> T216\nX257 -> T217\nX258 -> T220\nX259 -> T219\nT184 -> tree(T217, T220, T219)\nT218 -> T220", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 126 [arrowhead = none ];
126 -> 49;

127 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 127 [arrowhead = none ];
127 -> 50;

128 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
48 -> 128 [arrowhead = none ];
128 -> 51;

129 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
48 -> 129 [arrowhead = none ];
129 -> 52;

130 [label="INSTANCE with matching:\nT1 -> T216\nT2 -> T220", fontsize=14, style = filled, fillcolor = lightgrey];
49 -> 130 [arrowhead = none , style=dashed];
130 -> 1[style=dashed];

131 [label="EVAL with clause\ntree_member(X286, tree(X287, X288, X289)) :- tree_member(X286, X289).\nand substitution\nT180 -> T243\nX286 -> T243\nX287 -> T244\nX288 -> T245\nX289 -> T247\nT184 -> tree(T244, T245, T247)\nT246 -> T247", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 131 [arrowhead = none ];
131 -> 53;

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

133 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 133 [arrowhead = none ];
133 -> 55;

134 [label="INSTANCE with matching:\nT1 -> T243\nT2 -> T247", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 134 [arrowhead = none , style=dashed];
134 -> 1[style=dashed];

135 [label="EVAL with clause\ntree_member(X308, tree(X309, X310, X311)) :- tree_member(X308, X311).\nand substitution\nT180 -> T262\nX308 -> T262\nX309 -> T263\nX310 -> T264\nX311 -> T266\nT2 -> tree(T263, T264, T266)\nT265 -> T266", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 135 [arrowhead = none ];
135 -> 56;

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

137 [label="INSTANCE with matching:\nT1 -> T262\nT2 -> T266", fontsize=14, style = filled, fillcolor = lightgrey];
56 -> 137 [arrowhead = none , style=dashed];
137 -> 1[style=dashed];

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

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

140 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
60 -> 140 [arrowhead = none ];
140 -> 62;

141 [label="EVAL with clause\ntree_member(X346, tree(X346, X347, X348)).\nand substitution\nT277 -> T294\nX346 -> T294\nX347 -> T295\nX348 -> T296\nT281 -> tree(T294, T295, T296)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 141 [arrowhead = none ];
141 -> 63;

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

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

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

145 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 145 [arrowhead = none ];
145 -> 65;

146 [label="EVAL with clause\ntree_member(X368, tree(X369, X370, X371)) :- tree_member(X368, X370).\nand substitution\nT277 -> T313\nX368 -> T313\nX369 -> T314\nX370 -> T317\nX371 -> T316\nT281 -> tree(T314, T317, T316)\nT315 -> T317", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 146 [arrowhead = none ];
146 -> 68;

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

148 [label="EVAL with clause\ntree_member(X390, tree(X391, X392, X393)) :- tree_member(X390, X393).\nand substitution\nT277 -> T332\nX390 -> T332\nX391 -> T333\nX392 -> T334\nX393 -> T336\nT281 -> tree(T333, T334, T336)\nT335 -> T336", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 148 [arrowhead = none ];
148 -> 70;

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

150 [label="INSTANCE with matching:\nT1 -> T313\nT2 -> T317", fontsize=14, style = filled, fillcolor = lightgrey];
68 -> 150 [arrowhead = none , style=dashed];
150 -> 1[style=dashed];

151 [label="INSTANCE with matching:\nT1 -> T332\nT2 -> T336", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 151 [arrowhead = none , style=dashed];
151 -> 1[style=dashed];

}

(2) Obligation:

Triples:

tree_member1(T49, tree(T14, tree(T50, T53, T52), T16)) :- tree_member1(T49, T53).
tree_member1(T76, tree(T14, tree(T77, T78, T80), T16)) :- tree_member1(T76, T80).
tree_member1(T95, tree(T96, T97, T99)) :- tree_member1(T95, T99).
tree_member1(T146, tree(T111, T112, tree(T147, T150, T149))) :- tree_member1(T146, T150).
tree_member1(T165, tree(T111, T112, tree(T166, T167, T169))) :- tree_member1(T165, T169).
tree_member1(T216, tree(T181, tree(T217, T220, T219), T183)) :- tree_member1(T216, T220).
tree_member1(T243, tree(T181, tree(T244, T245, T247), T183)) :- tree_member1(T243, T247).
tree_member1(T262, tree(T263, T264, T266)) :- tree_member1(T262, T266).
tree_member1(T313, tree(T278, T279, tree(T314, T317, T316))) :- tree_member1(T313, T317).
tree_member1(T332, tree(T278, T279, tree(T333, T334, T336))) :- tree_member1(T332, T336).

Clauses:

tree_memberc1(T6, tree(T6, T7, T8)).
tree_memberc1(T30, tree(T14, tree(T30, T31, T32), T16)).
tree_memberc1(T49, tree(T14, tree(T50, T53, T52), T16)) :- tree_memberc1(T49, T53).
tree_memberc1(T76, tree(T14, tree(T77, T78, T80), T16)) :- tree_memberc1(T76, T80).
tree_memberc1(T95, tree(T96, T97, T99)) :- tree_memberc1(T95, T99).
tree_memberc1(T127, tree(T111, T112, tree(T127, T128, T129))).
tree_memberc1(T146, tree(T111, T112, tree(T147, T150, T149))) :- tree_memberc1(T146, T150).
tree_memberc1(T165, tree(T111, T112, tree(T166, T167, T169))) :- tree_memberc1(T165, T169).
tree_memberc1(T197, tree(T181, tree(T197, T198, T199), T183)).
tree_memberc1(T216, tree(T181, tree(T217, T220, T219), T183)) :- tree_memberc1(T216, T220).
tree_memberc1(T243, tree(T181, tree(T244, T245, T247), T183)) :- tree_memberc1(T243, T247).
tree_memberc1(T262, tree(T263, T264, T266)) :- tree_memberc1(T262, T266).
tree_memberc1(T294, tree(T278, T279, tree(T294, T295, T296))).
tree_memberc1(T313, tree(T278, T279, tree(T314, T317, T316))) :- tree_memberc1(T313, T317).
tree_memberc1(T332, tree(T278, T279, tree(T333, T334, T336))) :- tree_memberc1(T332, T336).

Afs:

tree_member1(x1, x2)  =  tree_member1(x1)

(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:
tree_member1_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_GA(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_GA(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → U3_GA(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_GA(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_GA(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)
TREE_MEMBER1_IN_GA(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_GA(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
TREE_MEMBER1_IN_GA(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_GA(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
TREE_MEMBER1_IN_GA(T262, tree(T263, T264, T266)) → U8_GA(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
TREE_MEMBER1_IN_GA(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_GA(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
TREE_MEMBER1_IN_GA(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_GA(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))

R is empty.
The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GA(x1, x7)
U2_GA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GA(x1, x7)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
U4_GA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GA(x1, x7)
U5_GA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GA(x1, x7)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x1, x7)
U7_GA(x1, x2, x3, x4, x5, x6, x7)  =  U7_GA(x1, x7)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x5)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x1, x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x7)

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:

TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_GA(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_GA(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → U3_GA(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_GA(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_GA(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)
TREE_MEMBER1_IN_GA(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_GA(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
TREE_MEMBER1_IN_GA(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_GA(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
TREE_MEMBER1_IN_GA(T262, tree(T263, T264, T266)) → U8_GA(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
TREE_MEMBER1_IN_GA(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_GA(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
TREE_MEMBER1_IN_GA(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_GA(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))

R is empty.
The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GA(x1, x7)
U2_GA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GA(x1, x7)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
U4_GA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GA(x1, x7)
U5_GA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GA(x1, x7)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x1, x7)
U7_GA(x1, x2, x3, x4, x5, x6, x7)  =  U7_GA(x1, x7)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x5)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x1, x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x7)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)

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

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

(7) PiDPToQDPProof (SOUND transformation)

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

(8) Obligation:

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

TREE_MEMBER1_IN_GA(T76) → TREE_MEMBER1_IN_GA(T76)

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

(9) 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 = TREE_MEMBER1_IN_GA(T76) evaluates to t =TREE_MEMBER1_IN_GA(T76)

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 TREE_MEMBER1_IN_GA(T76) to TREE_MEMBER1_IN_GA(T76).

(10) NO