Runtime Complexity of the query pattern
at(a,a)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(1)).

(0) Obligation:

Clauses:

at(X, fido) :- ','(at(X, mary), near(X)).
at(ta, mary).
at(jm, mary).
near(jm).

Query: at(a,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

at(ta, mary).
at(jm, mary).
near(jm).
at(X, fido) :- ','(at(X, mary), near(X)).

Query: at(a,a)

(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: at(T1, T2)\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: at(T1, T2), SCOPE: 1, CLAUSE: 0 | at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 3\n\nat(T1, T2) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | at(T1, T2), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: at(T1, T2), SCOPE: 1, CLAUSE: 3\n\nat(T1, T2) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: at(T1, T2), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(at(T5, mary), near(T5))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 0 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 1 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: near(ta) | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 1 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 1 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\nat(T5, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: near(ta), SCOPE: 3, CLAUSE: 2 | ?_3 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 1 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ?_3 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 1 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 1 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: near(jm) | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\nat(T5, mary) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: near(jm), SCOPE: 4, CLAUSE: 2 | ?_4 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true | ?_4 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ?_4 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: near(jm) | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\nat(T5, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\nat(T5, mary) !=? at(ta, mary)\nat(T5, mary) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: near(jm), SCOPE: 5, CLAUSE: 2 | ?_5 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\nat(T5, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: true | ?_5 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\nat(T5, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ?_5 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\nat(T5, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 3\n\nat(T5, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(at(T12, mary), near(T12))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 0 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 1 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: near(ta) | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 1 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 1 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\nat(T12, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: near(ta), SCOPE: 7, CLAUSE: 2 | ?_7 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 1 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ?_7 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 1 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 1 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: near(jm) | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\nat(T12, mary) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: near(jm), SCOPE: 8, CLAUSE: 2 | ?_8 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: true | ?_8 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ?_8 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: near(jm) | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\nat(T12, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\nat(T12, mary) !=? at(ta, mary)\nat(T12, mary) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: near(jm), SCOPE: 9, CLAUSE: 2 | ?_9 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\nat(T12, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: true | ?_9 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\nat(T12, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ?_9 | ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\nat(T12, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(at(T12, mary), near(T12)), SCOPE: 6, CLAUSE: 3\n\nat(T12, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: true | at(T1, T2), SCOPE: 1, CLAUSE: 3\n\nat(T1, T2) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: at(T1, T2), SCOPE: 1, CLAUSE: 3\n\nat(T1, T2) !=? at(ta, mary)\nat(T1, T2) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: at(T1, T2), SCOPE: 1, CLAUSE: 3\n\nat(T1, T2) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(at(T19, mary), near(T19))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 0 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 1 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: near(ta) | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 1 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 1 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\nat(T19, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: near(ta), SCOPE: 11, CLAUSE: 2 | ?_11 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 1 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ?_11 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 1 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 1 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: near(jm) | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\nat(T19, mary) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: near(jm), SCOPE: 12, CLAUSE: 2 | ?_12 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: true | ?_12 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ?_12 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: near(jm) | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\nat(T19, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\nat(T19, mary) !=? at(ta, mary)\nat(T19, mary) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: near(jm), SCOPE: 13, CLAUSE: 2 | ?_13 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\nat(T19, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true | ?_13 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\nat(T19, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ?_13 | ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\nat(T19, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(at(T19, mary), near(T19)), SCOPE: 10, CLAUSE: 3\n\nat(T19, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(at(T26, mary), near(T26))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 0 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 1 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: near(ta) | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 1 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 1 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\nat(T26, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: near(ta), SCOPE: 15, CLAUSE: 2 | ?_15 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 1 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ?_15 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 1 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 1 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: near(jm) | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\nat(T26, mary) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: near(jm), SCOPE: 16, CLAUSE: 2 | ?_16 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: true | ?_16 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ?_16 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: near(jm) | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\nat(T26, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\nat(T26, mary) !=? at(ta, mary)\nat(T26, mary) !=? at(jm, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: near(jm), SCOPE: 17, CLAUSE: 2 | ?_17 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\nat(T26, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: true | ?_17 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\nat(T26, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ?_17 | ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\nat(T26, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(at(T26, mary), near(T26)), SCOPE: 14, CLAUSE: 3\n\nat(T26, mary) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 147 [arrowhead = none ];
147 -> 3;

148 [label="EVAL with clause\nat(ta, mary).\nand substitutionT1 -> ta,\nT2 -> mary", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 148 [arrowhead = none ];
148 -> 5;

149 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 149 [arrowhead = none ];
149 -> 7;

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

151 [label="EVAL with clause\nat(jm, mary).\nand substitutionT1 -> jm,\nT2 -> mary", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 151 [arrowhead = none ];
151 -> 92;

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

153 [label="EVAL with clause\nat(jm, mary).\nand substitutionT1 -> jm,\nT2 -> mary", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 153 [arrowhead = none ];
153 -> 11;

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

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

156 [label="EVAL with clause\nat(X8, fido) :- ','(at(X8, mary), near(X8)).\nand substitutionT1 -> T12,\nX8 -> T12,\nT2 -> fido,\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 156 [arrowhead = none ];
156 -> 53;

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

158 [label="EVAL with clause\nat(X2, fido) :- ','(at(X2, mary), near(X2)).\nand substitutionT1 -> T5,\nX2 -> T5,\nT2 -> fido,\nT4 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 158 [arrowhead = none ];
158 -> 17;

159 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 159 [arrowhead = none ];
159 -> 18;

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

161 [label="EVAL with clause\nat(ta, mary).\nand substitutionT5 -> ta", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 161 [arrowhead = none ];
161 -> 22;

162 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 162 [arrowhead = none ];
162 -> 23;

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

164 [label="EVAL with clause\nat(jm, mary).\nand substitutionT5 -> jm", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 164 [arrowhead = none ];
164 -> 37;

165 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 165 [arrowhead = none ];
165 -> 38;

166 [label="BACKTRACK\nfor clause: near(jm)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 166 [arrowhead = none ];
166 -> 25;

167 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 167 [arrowhead = none ];
167 -> 26;

168 [label="EVAL with clause\nat(jm, mary).\nand substitutionT5 -> jm", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 168 [arrowhead = none ];
168 -> 27;

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

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

171 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 171 [arrowhead = none ];
171 -> 35;

172 [label="ONLY EVAL with clause\nnear(jm).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 172 [arrowhead = none ];
172 -> 30;

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

174 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 174 [arrowhead = none ];
174 -> 32;

175 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 175 [arrowhead = none ];
175 -> 33;

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

177 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 177 [arrowhead = none ];
177 -> 48;

178 [label="ONLY EVAL with clause\nnear(jm).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 178 [arrowhead = none ];
178 -> 41;

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

180 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 180 [arrowhead = none ];
180 -> 44;

181 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 181 [arrowhead = none ];
181 -> 47;

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

183 [label="EVAL with clause\nat(ta, mary).\nand substitutionT12 -> ta", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 183 [arrowhead = none ];
183 -> 58;

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

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

186 [label="EVAL with clause\nat(jm, mary).\nand substitutionT12 -> jm", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 186 [arrowhead = none ];
186 -> 81;

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

188 [label="BACKTRACK\nfor clause: near(jm)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 188 [arrowhead = none ];
188 -> 64;

189 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 189 [arrowhead = none ];
189 -> 66;

190 [label="EVAL with clause\nat(jm, mary).\nand substitutionT12 -> jm", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 190 [arrowhead = none ];
190 -> 68;

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

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

193 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 193 [arrowhead = none ];
193 -> 80;

194 [label="ONLY EVAL with clause\nnear(jm).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 194 [arrowhead = none ];
194 -> 74;

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

196 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 196 [arrowhead = none ];
196 -> 76;

197 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 197 [arrowhead = none ];
197 -> 78;

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

199 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 199 [arrowhead = none ];
199 -> 89;

200 [label="ONLY EVAL with clause\nnear(jm).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 200 [arrowhead = none ];
200 -> 84;

201 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 201 [arrowhead = none ];
201 -> 85;

202 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 202 [arrowhead = none ];
202 -> 86;

203 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 203 [arrowhead = none ];
203 -> 88;

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

205 [label="EVAL with clause\nat(X20, fido) :- ','(at(X20, mary), near(X20)).\nand substitutionT1 -> T26,\nX20 -> T26,\nT2 -> fido,\nT25 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 205 [arrowhead = none ];
205 -> 123;

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

207 [label="EVAL with clause\nat(X14, fido) :- ','(at(X14, mary), near(X14)).\nand substitutionT1 -> T19,\nX14 -> T19,\nT2 -> fido,\nT18 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 207 [arrowhead = none ];
207 -> 97;

208 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 208 [arrowhead = none ];
208 -> 98;

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

210 [label="EVAL with clause\nat(ta, mary).\nand substitutionT19 -> ta", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 210 [arrowhead = none ];
210 -> 100;

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

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

213 [label="EVAL with clause\nat(jm, mary).\nand substitutionT19 -> jm", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 213 [arrowhead = none ];
213 -> 115;

214 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 214 [arrowhead = none ];
214 -> 116;

215 [label="BACKTRACK\nfor clause: near(jm)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 215 [arrowhead = none ];
215 -> 104;

216 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 216 [arrowhead = none ];
216 -> 105;

217 [label="EVAL with clause\nat(jm, mary).\nand substitutionT19 -> jm", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 217 [arrowhead = none ];
217 -> 107;

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

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

220 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 220 [arrowhead = none ];
220 -> 114;

221 [label="ONLY EVAL with clause\nnear(jm).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 221 [arrowhead = none ];
221 -> 110;

222 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 222 [arrowhead = none ];
222 -> 111;

223 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 223 [arrowhead = none ];
223 -> 112;

224 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 224 [arrowhead = none ];
224 -> 113;

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

226 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 226 [arrowhead = none ];
226 -> 122;

227 [label="ONLY EVAL with clause\nnear(jm).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 227 [arrowhead = none ];
227 -> 118;

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

229 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 229 [arrowhead = none ];
229 -> 120;

230 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 230 [arrowhead = none ];
230 -> 121;

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

232 [label="EVAL with clause\nat(ta, mary).\nand substitutionT26 -> ta", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 232 [arrowhead = none ];
232 -> 126;

233 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 233 [arrowhead = none ];
233 -> 127;

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

235 [label="EVAL with clause\nat(jm, mary).\nand substitutionT26 -> jm", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 235 [arrowhead = none ];
235 -> 139;

236 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 236 [arrowhead = none ];
236 -> 140;

237 [label="BACKTRACK\nfor clause: near(jm)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 237 [arrowhead = none ];
237 -> 129;

238 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 238 [arrowhead = none ];
238 -> 130;

239 [label="EVAL with clause\nat(jm, mary).\nand substitutionT26 -> jm", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 239 [arrowhead = none ];
239 -> 131;

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

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

242 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 242 [arrowhead = none ];
242 -> 138;

243 [label="ONLY EVAL with clause\nnear(jm).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 243 [arrowhead = none ];
243 -> 134;

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

245 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 245 [arrowhead = none ];
245 -> 136;

246 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 246 [arrowhead = none ];
246 -> 137;

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

248 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 248 [arrowhead = none ];
248 -> 146;

249 [label="ONLY EVAL with clause\nnear(jm).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 249 [arrowhead = none ];
249 -> 142;

250 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
142 -> 250 [arrowhead = none ];
250 -> 143;

251 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 251 [arrowhead = none ];
251 -> 144;

252 [label="BACKTRACK\nfor clause: at(X, fido) :- ','(at(X, mary), near(X))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 252 [arrowhead = none ];
252 -> 145;

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in → f2_out1(ta, mary)
f2_in → f2_out1(jm, mary)
f2_in → f2_out1(jm, fido)

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

f2_in

Defined Pair Symbols:none

Compound Symbols:none

(5) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(6) BOUNDS(O(1), O(1))