% use only the (binary) resolution inference rule
set(binary_res).  

formula_list(usable).

% Some general rules for the kinship domain
%
all x y (Mother(x,y) <-> Female(x) & Parent(x,y)).
all x y (Father(x,y) <-> Male(x) & Parent(x, y)).
all x y (Parent(x,y) & Male(y) <-> Son(y,x)).
all x y (Parent(x,y) & Female(y) <-> Daughter(y,x)).
all x y z (Siblings(x,y) & Parent(z,x) -> Parent(z,y)).
all x y (Siblings(x,y) <-> Siblings(y,x)).
all x y (Siblings(x,y) & Male(x) <-> Brother(x,y)).
all x y (Siblings(x,y) & Female(x) <-> Sister(x,y)).

% Specific facts for this problem
%
Brother(Bob, Alice).
Mother(Diane, Bob).
Father(Carl, Alice).

end_of_list.

formula_list(sos).

% Try to prove Father(Carl, Bob), so add its negation to the SOS
%
-Father(Carl, Bob).

end_of_list.