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

(0) Obligation:

Clauses:

p(a, b).
p(b, c).
tc(X, X).
tc(X, Y) :- ','(p(X, Z), tc(Z, Y)).

Queries:

tc(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

tc10(T15) :- tc21(T15).
tc1(a, T9) :- tc10(T9).
tc1(b, T9) :- tc21(T9).
tc1(a, T28) :- tc10(T28).
tc1(b, T28) :- tc21(T28).

Clauses:

tcc21(c).
tcc10(b).
tcc10(T15) :- tcc21(T15).

Afs:

tc1(x1, x2)  =  tc1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:


Clauses:

tcc21(c).
tcc10(b).
tcc10(T15) :- tcc21(T15).

Afs:

tc1(x1, x2)  =  tc1(x1)

(5) TPisEmptyProof (EQUIVALENT transformation)

There are no more dependency triples. Hence, the dependency triple problem trivially terminates.

(6) YES