% problem-set/puzzles/truth.lies/mars_venus2.in
% created : 08/08/88
% revised : 08/17/89

% description :
%
%  Here's the situation: human observers in this exclusive club on
%  Ganymede can't distinguish Martians from Venusians, males from
%  females, except for the fact that Venusian women and Martian
%  men always tell the truth and Venusian men and Martian women
%  always lie.  

% representation :
%
% t(x) = x is a truthteller
% l(x) = x is a liar
% f(x) = x is female
% m(x) = x is male
% M(x) = x is from Mars
% V(x) = x is from Venus
% s(x,y) = x makes the statement y
% S(x) refers to the statement made by x

set(hyper_res).
set(para_from).
set(para_into).
set(para_from_left).
assign(max_literals,5).
set(unit_deletion).

list(axioms).

eq(x,x).

%	everyone's either from Mars or Venus, male or female, and statements
%	are true or false.
M(x) | V(x).
-M(x) | -V(x).
m(x) | f(x).
-m(x) | -f(x).
t(x) | l(x).
-t(x) | -l(x).
-s(x,y) | true(y) | -true(y).

%	rules about statements:
-s(x,y) | eq(y,S(x)).
-true(S(x)) | t(x).
true(S(x)) | l(x).

%	who's a liar, who's not:
-V(x) | -f(x) | t(x).
-V(x) | -m(x) | l(x).
-M(x) | -m(x) | t(x).
-M(x) | -f(x) | l(x).

%	what truthtellers say is true, what liars say is false:
-t(x) | -s(x,y) | true(y).
-l(x) | -s(x,y) | -true(y).

end_of_list.


list(sos).

%	A says "I'm from Mars"
%	B exclaims "That's not true!"
%	A and B are married; are they a mixed couple?
s(A,AMars).
s(B,NTrue).
-M(A) | true(AMars).
M(A) | -true(AMars).
-true(AMars) | -true(S(B)).
Eq(S(B),NTrue).
Eq(S(A),AMars).
true(AMars) | true(S(B)).
-f(A) | m(B).
-m(A) | f(B).

%	conclude that they are NOT a mixed couple.
%	denial of the conclusion: either M(A) & V(B) or V(A) & M(B).
M(B) | M(A).
V(A) | V(B).

%	two clauses deleted due to tautology: M(A) | V(A), V(B) | M(B).

end_of_list.

