Improving Wang's algorithm in Prolog

The error is mine, not Ben Hudson’s. I was inspired by Jen Otten’s code:

% axiom
prove(G > D,_) :- member(A,G), member(B,D),
                  unify_with_occurs_check(A,B).

but again, I misunderstood maybe also Otten’s code and translated wrongly, because Jen Otten wrote another prover. I see that you explained your point on the page dedicated to the implementation of Wang prover. Thanks a lot for your patience.