How to formulate an exception for findall/3 correctly?

I have startet to learn Prolog and I want to get a list of opponents of players with findall/3. In the Generalization I just want to add only the opponents to the list who are actually players, except the player I am asking for itself. How can I formulate this exception? I know about the negation as failure concept but I am not sure if and how I need it here.

player(irina).
player(anton).
player(michael).

opponent(irina, anton).
opponent(irina, maria).
opponent(irina, michael).

% Only opponents who are also players should be added to the list, 
% except the player of interest itself 
opponent(X, Y) :- X \= Y, player(Y).

% the query
?- findall(O, opponent(irina,O) , OpponentList).

% the result
% only the first three results from the facts, 
% the results from the rule, a second entry of
% anton and michael are missing.
OpponentList = [anton, maria, michael].

I actually expected, that the resolution would work as follows:

opponent(irina, irina) :- irina \= irina, player(irina).
%                              false          true
%                                      false
% false, hence not added to the list

opponent(irina, anton) :- irina \= anton, player(anton).
%                              true          true
%                                     true
% true, hence added to the list

What am I missing? Many thanks in advance!

Solution

Code:

player(irina).
player(anton).
player(michael).

opponent(irina, anton).
opponent(irina, maria).
opponent(irina, michael).

opponent(X, Y) :- 
   format("Called with X = ~q, Y = ~q\n",[X,Y]),
   X \= Y,     % this will fail if Y is still fresh because X and Y can be unified!
   player(Y).

opponent_mod(X, Y) :-
   format("Called with X = ~q, Y = ~q\n",[X,Y]),
   player(Y),  % this will set Y to various players  
   X \= Y.     % the test for un-unifiability of two set vars may or may not succeed 

% query helpfully as code:

q(Who,OpponentList) :- findall(O, opponent(Who,O) , OpponentList).

q_mod(Who,OpponentList) :- findall(O, opponent_mod(Who,O) , OpponentList).

% even better

q_mod_set(Who,OpponentList) :- setof(O, opponent_mod(Who,O) , OpponentList).

Run it:

Not expected:

?- q(irina,X).
Called with X = irina, Y = _19654
X = [anton, maria, michael].

Expected:

?- q_mod(irina,X).
Called with X = irina, Y = _20568
X = [anton, michael].

So what happens in the "not expected" case with Who = irina:

findall/3 tries to collect all values Y such that opponent(Who,O)
It finds anton, maria, michal through the facts
- opponent(irina, anton).
- opponent(irina, maria).
- opponent(irina, michael).
It also tries the rule opponent(X, Y) :- ... with X = irina (once only). But the test X \= Y fails because X has been constrained to be irina but Y is still fresh (completely unconstrained). This means that a unification of X and Y could succeed if it were attempted (which is what is being tested, = does not as such mean "is not equal"). So X \= Y is false at this point of computation. If you move X \= Y after player(Y), then Y will have been constrained to whatever was grabbed from the player/1 facts, and this would reduce to an actual comparison of the values of X and Y.