When i execute this code(shown below) , it always sets implicit kind of constraint.
As you can see below , it always says that D1 = D2 but there is no such explicit constraints nor any pattern matching which forces this.
Or in otherwords there is some reference between D1 and D2 such that whenever D1 gets initialized, D2 gets automatically initialized. I can't see how this is happening. Can someone explain me, i tried ot figure it out with debugger but it did not help.
It's a puzzle "GERALD + DONALD = ROBERT", initially three lists contains these variables.

I add code below if anyone wants to test it:
sum(N1,N2,N):-
sum1(N1,N2,N,0,0,[0,1,2,3,4,5,6,7,8,9],_).
sum1([],[],[],0,0,Digits,Digits).
sum1([D1|N1],[D2|N2],[D|N],C1,C,Digs1,Digs2):-
sum1(N1,N2,N,C1,C2,Digs1,Digs2),
digitSum(D1,D2,C2,D,C,Digs2,Digs).
digitSum(D1,D2,C1,D,C,Digs1,Digs):-
del(D1,Digs1,Digs2),
del(D2,Digs2,Digs3),
del(D,Digs3,Digs),
S is D1 + D2 + C1,
D is S mod 10,
C is D div 10.
del(A,L,L):-
nonvar(A),!.
del(A,[A|L],L).
del(A,[B|L],[B|L1]):-
del(A,L,L1).
Query:
?- sum( [D,O,N,A,L,D], [G,E,R,A,L,D], [R,O,B,E,R,T] ).
When it says
D1 = D2then you should see that bothD1andD2have same variable from the list and List is a functor and one variable is visible in whole functor.You should see that when the recursion ends, then you have have
D's(last element) fromGERALDandDONALD, since this D is visible in whole functor,D1andD2both refer to same variable.