(0) Obligation:

Clauses:

dcsolve(X, Y) :- ','(base(X), conquer(X, Y)).
dcsolve(X, Y) :- ','(divide(X, X0, X1, X2), ','(dcsolve(X1, Y1), ','(dcsolve(X2, Y2), merge(X0, Y1, Y2, Y)))).

Query: dcsolve(g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

(2) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(3) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(4) YES