% Professors Dodds, Stone, and Thom go to their favorite bars for beer.
% Each prof prefers a different beer (one of Anchor, Bud, and Miller)
% and frequents a different bar (one of Alice's, Harry's, or Joe's).
% Each bar serves a unique beer.
%
% Professor Stone prefers Bud.                          (Clue 1)
% 
% Professor Thom doesn't prefer Miller.                 (Clue 2)
% 
% The prof who prefers Miller frequents Alice's bar.    (Clue 3)
% 
% The prof who prefers Anchor does not frequent Joe's.  (Clue 4)
%
%
% Which bar does each prof frequent and what beer does each prefer?

% Solution in Otter follows (run with otter < beer.in).

set(auto).
list(usable).

% Clauses corresponding to the clues:

prefer(Stone, Bud).                                     % Clue 1

-prefer(Thom, Miller).                                  % Clue 2

-prefer(x, Miller) | frequent(x, Alice).                % Clue 3

-prefer(x, Anchor) | -frequent(x, Joe).                 % Clue 4


% Individuals

prof(Dodds).
prof(Stone).
prof(Thom).

beer(Anchor).
beer(Bud).
beer(Miller).

bar(Alice).
bar(Harry).
bar(Joe).

% We need to state explicitly that the constants are distinct.
% Although they do not unify, they could conceivably be equal.

Dodds != Stone.  Dodds != Thom. 
Dodds != Anchor. Dodds != Bud.   Dodds != Miller.
Dodds != Alice.  Dodds != Harry. Dodds != Joe.

Stone != Thom. 
Stone != Anchor. Stone != Bud.   Stone != Miller.
Stone != Alice.  Stone != Harry. Stone != Joe.

Anchor != Bud.    Anchor != Miller.
Anchor != Alice.  Anchor != Harry.  Anchor != Joe.

Bud != Miller.
Bud != Alice.  Bud != Harry.  Bud != Joe.

Alice != Harry. Alice != Joe.
Harry != Joe.


% Any bar that a professor frequents serves beers that he or she prefers.

-frequent(x, y) | serves(y, z) | prefer(x, z).


% Distribution and uniqueness requirements.

% Every bar is frequented by some prof.

-bar(y) | frequent(Dodds, y) | frequent(Stone, y) | frequent(Thom, y).


% Every beer is preferred by some prof.

-beer(y) | prefer(Dodds, y) | prefer(Stone, y) | prefer(Thom, y).


% Each bar serves a unique beer.

-serves(x, y) | -serves(x, z) | y = z.


% Each prof prefers a unique beer.

-prefer(x, y) | -prefer(x, z) | y = z.


% Each prof frequents a unique bar.

-frequent(x, y) | -frequent(x, z) | y = z.


% Which bars are frequented, and which beers preferred, by which professors?

 -frequent(Dodds, x)     | -frequent(Stone, y) | -frequent(Thom, z)
|  -prefer(Dodds, u)     |  - prefer(Stone, v) |   -prefer(Thom, w)
| $answer([Dodds, x, u],            [Stone, y, v],        [Thom, z, w]).

end_of_list.