Left Termination proof of /tmp/tmpgBURAZ/at.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 59 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 PiDP

↳5 PisEmptyProof (⇔, 0 ms)

↳6 YES

(0) Obligation:

Clauses:

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

Query: at(a,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: at(T1, T2)\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: at(T1, T2), SCOPE: 1, CLAUSE: 0 | at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(at(T5, mary), near(T5)) | at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\nX2 is free\nat(T1, T2) !=? at(X2, fido)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(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: 2 | ?_2 | at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 1 | ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 2 | ?_2 | at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 2 | ?_2 | at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: near(ta)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: near(ta), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(at(T5, mary), near(T5)), SCOPE: 2, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ?_2 | at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: near(jm)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: near(jm), SCOPE: 4, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: at(T1, T2), SCOPE: 1, CLAUSE: 1 | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: at(T1, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: at(T1, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: true | at(T1, T2), SCOPE: 1, CLAUSE: 2\n\nX2 is free\nat(T1, T2) !=? at(X2, fido)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: at(T1, T2), SCOPE: 1, CLAUSE: 2\n\nX2 is free\nat(T1, T2) !=? at(X2, fido)\nat(T1, T2) !=? at(ta, mary)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: at(T1, T2), SCOPE: 1, CLAUSE: 2\n\nX2 is free\nat(T1, T2) !=? at(X2, fido)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 105 [arrowhead = none ];
105 -> 4;

106 [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];
4 -> 106 [arrowhead = none ];
106 -> 10;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

121 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 121 [arrowhead = none ];
121 -> 30;

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

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

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

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

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

127 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 127 [arrowhead = none ];
127 -> 56;

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

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

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

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

132 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 132 [arrowhead = none ];
132 -> 66;

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

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

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

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

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

138 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 138 [arrowhead = none ];
138 -> 100;

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

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

}

(2) Obligation:

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

atA_in_aa(jm, fido) → atA_out_aa(jm, fido)
atA_in_aa(ta, mary) → atA_out_aa(ta, mary)
atA_in_aa(jm, mary) → atA_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
atA_in_aa(x1, x2) = atA_in_aa
atA_out_aa(x1, x2) = atA_out_aa(x1, x2)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

atA_in_aa(jm, fido) → atA_out_aa(jm, fido)
atA_in_aa(ta, mary) → atA_out_aa(ta, mary)
atA_in_aa(jm, mary) → atA_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
atA_in_aa(x1, x2) = atA_in_aa
atA_out_aa(x1, x2) = atA_out_aa(x1, x2)

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

(4) Obligation:

Pi DP problem:
P is empty.
The TRS R consists of the following rules:

atA_in_aa(jm, fido) → atA_out_aa(jm, fido)
atA_in_aa(ta, mary) → atA_out_aa(ta, mary)
atA_in_aa(jm, mary) → atA_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
atA_in_aa(x1, x2) = atA_in_aa
atA_out_aa(x1, x2) = atA_out_aa(x1, x2)

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

(5) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,R,Pi) chain.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) PisEmptyProof (EQUIVALENT transformation)

(6) YES