%--------------------------------------------------------------------------
% File     : PUZ006-1 : TPTP v2.1.0. Released v1.0.0.
% Domain   : Puzzles
% Problem  : Determine sex and race on Mars and Venus
% Version  : Special.
% English  : 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.
%            Ork says "Bog is from Venus."  Bog says "Ork is from Mars." 
%            Ork says "Bog is male."  Bog says "Ork is female." Who's 
%            what?  (sex & race).

% Refs     : 
% Source   : [ANL]
% Names    : mars_venus.in [ANL]

% Status   : unsatisfiable
% Rating   : 0.09 v2.1.0, 0.00 v2.0.0
% Syntax   : Number of clauses    :   29 (   4 non-Horn;   5 unit;  25 RR)
%            Number of literals   :   60 (   1 equality)
%            Maximal clause size  :    3 (   2 average)
%            Number of predicates :    9 (   0 propositional; 1-2 arity)
%            Number of functors   :    7 (   6 constant; 0-1 arity)
%            Number of variables  :   20 (   1 singleton)
%            Maximal term depth   :    2 (   1 average)

% Comments : 
%          : tptp2X -f tptp -t rm_equality:rstfp PUZ006-1.p 
%--------------------------------------------------------------------------
input_clause(from_mars_or_venus,axiom,
    [++ from_mars(X),
     ++ from_venus(X)]).

input_clause(not_from_mars_and_venus,axiom,
    [-- from_mars(X),
     -- from_venus(X)]).

input_clause(male_or_female,axiom,
    [++ male(X),
     ++ female(X)]).

input_clause(not_male_and_female,axiom,
    [-- male(X),
     -- female(X)]).

input_clause(truthteller_or_liar,axiom,
    [++ truthteller(X),
     ++ liar(X)]).

input_clause(not_truthteller_and_liar,axiom,
    [-- truthteller(X),
     -- liar(X)]).

input_clause(statements_are_true_or_not,axiom,
    [-- says(X, Y),
     ++ a_truth(Y),
     -- a_truth(Y)]).

input_clause(people_say_their_statements,axiom,
    [-- says(X, Y),
     ++ equal(Y, statement_by(X))]).

input_clause(true_statements_made_by_truthtellers,axiom,
    [-- a_truth(statement_by(X)),
     ++ truthteller(X)]).

input_clause(false_statements_made_by_liars,axiom,
    [++ a_truth(statement_by(X)),
     ++ liar(X)]).

input_clause(venusian_female_are_truthtellers,axiom,
    [-- from_venus(X),
     -- female(X),
     ++ truthteller(X)]).

input_clause(venusian_males_are_liars,axiom,
    [-- from_venus(X),
     -- male(X),
     ++ liar(X)]).

input_clause(marsian_males_are_truthtellers,axiom,
    [-- from_mars(X),
     -- male(X),
     ++ truthteller(X)]).

input_clause(marsian_females_are_liars,axiom,
    [-- from_mars(X),
     -- female(X),
     ++ liar(X)]).

input_clause(truthtellers_make_true_statements,axiom,
    [-- truthteller(X),
     -- says(X, Y),
     ++ a_truth(Y)]).

input_clause(liars_make_false_statements,axiom,
    [-- liar(X),
     -- says(X, Y),
     -- a_truth(Y)]).

input_clause(ork_says_bog_is_from_venus,hypothesis,
    [++ says(ork, bog_is_from_venus)]).

input_clause(bog_says_ork_is_from_mar,hypothesis,
    [++ says(bog, ork_is_from_mars)]).

input_clause(ork_says_bog_is_male,hypothesis,
    [++ says(ork, bog_is_male)]).

input_clause(bog_says_ork_is_female,hypothesis,
    [++ says(bog, ork_is_female)]).

input_clause(bog_is_from_venus1,hypothesis,
    [-- a_truth(bog_is_from_venus),
     ++ from_venus(bog)]).

input_clause(ork_is_from_mars1,hypothesis,
    [-- a_truth(ork_is_from_mars),
     ++ from_mars(ork)]).

input_clause(bog_is_male1,hypothesis,
    [-- a_truth(bog_is_male),
     ++ male(bog)]).

input_clause(ork_is_female1,hypothesis,
    [-- a_truth(ork_is_female),
     ++ female(ork)]).

input_clause(bog_is_from_venus2,hypothesis,
    [-- from_venus(bog),
     ++ a_truth(bog_is_from_venus)]).

input_clause(ork_is_from_mars2,hypothesis,
    [-- from_mars(ork),
     ++ a_truth(ork_is_from_mars)]).

input_clause(bog_is_male2,hypothesis,
    [-- male(bog),
     ++ a_truth(bog_is_male)]).

input_clause(ork_is_female2,hypothesis,
    [-- female(ork),
     ++ a_truth(ork_is_female)]).

input_clause(prove_bog_is_female,conjecture,
    [-- female(bog)]).
%--------------------------------------------------------------------------