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

0 Prolog
  ↳1 PrologToPiTRSProof (⇐)
    ↳2 PiTRS
    ↳3 DependencyPairsProof (⇔)
    ↳4 PiDP
  ↳5 PrologToPiTRSProof (⇐)
    ↳6 PiTRS
    ↳7 DependencyPairsProof (⇔)
    ↳8 PiDP
    ↳9 DependencyGraphProof (⇔)
    ↳10 TRUE

(0) Obligation:

Clauses:

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

Queries:

at(a,a).

(1) PrologToPiTRSProof (SOUND transformation)

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

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)

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

AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)

The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)
AT_IN_AA(x1, x2)  =  AT_IN_AA
U1_AA(x1, x2)  =  U1_AA(x2)
AT_IN_AG(x1, x2)  =  AT_IN_AG(x2)
U1_AG(x1, x2)  =  U1_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x1, x2)
NEAR_IN_G(x1)  =  NEAR_IN_G(x1)
U2_AA(x1, x2)  =  U2_AA(x1, x2)

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

(4) Obligation:

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

AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)

The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)
AT_IN_AA(x1, x2)  =  AT_IN_AA
U1_AA(x1, x2)  =  U1_AA(x2)
AT_IN_AG(x1, x2)  =  AT_IN_AG(x2)
U1_AG(x1, x2)  =  U1_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x1, x2)
NEAR_IN_G(x1)  =  NEAR_IN_G(x1)
U2_AA(x1, x2)  =  U2_AA(x1, x2)

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

(5) PrologToPiTRSProof (SOUND transformation)

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

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g(x1)
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

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

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g(x1)
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)

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

AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)

The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g(x1)
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)
AT_IN_AA(x1, x2)  =  AT_IN_AA
U1_AA(x1, x2)  =  U1_AA(x2)
AT_IN_AG(x1, x2)  =  AT_IN_AG(x2)
U1_AG(x1, x2)  =  U1_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x1, x2)
NEAR_IN_G(x1)  =  NEAR_IN_G(x1)
U2_AA(x1, x2)  =  U2_AA(x1, x2)

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

(8) Obligation:

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

AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)

The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g(x1)
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)
AT_IN_AA(x1, x2)  =  AT_IN_AA
U1_AA(x1, x2)  =  U1_AA(x2)
AT_IN_AG(x1, x2)  =  AT_IN_AG(x2)
U1_AG(x1, x2)  =  U1_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x1, x2)
NEAR_IN_G(x1)  =  NEAR_IN_G(x1)
U2_AA(x1, x2)  =  U2_AA(x1, x2)

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

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 8 less nodes.

(10) TRUE