#--------------------------------------------------------------------------
# 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 setheo:sign -t rm_equality:rstfp PUZ006-1.p 
#--------------------------------------------------------------------------
# from_mars_or_venus, axiom.
from_mars(X);
from_venus(X) <- .

# not_from_mars_and_venus, axiom.
 <- from_mars(X),
    from_venus(X).

# male_or_female, axiom.
male(X);
female(X) <- .

# not_male_and_female, axiom.
 <- male(X),
    female(X).

# truthteller_or_liar, axiom.
truthteller(X);
liar(X) <- .

# not_truthteller_and_liar, axiom.
 <- truthteller(X),
    liar(X).

# statements_are_true_or_not, axiom.
a_truth(Y) <- 
    says(X, Y),
    a_truth(Y).

# people_say_their_statements, axiom.
equal(Y, statement_by(X)) <- 
    says(X, Y).

# true_statements_made_by_truthtellers, axiom.
truthteller(X) <- 
    a_truth(statement_by(X)).

# false_statements_made_by_liars, axiom.
a_truth(statement_by(X));
liar(X) <- .

# venusian_female_are_truthtellers, axiom.
truthteller(X) <- 
    from_venus(X),
    female(X).

# venusian_males_are_liars, axiom.
liar(X) <- 
    from_venus(X),
    male(X).

# marsian_males_are_truthtellers, axiom.
truthteller(X) <- 
    from_mars(X),
    male(X).

# marsian_females_are_liars, axiom.
liar(X) <- 
    from_mars(X),
    female(X).

# truthtellers_make_true_statements, axiom.
a_truth(Y) <- 
    truthteller(X),
    says(X, Y).

# liars_make_false_statements, axiom.
 <- liar(X),
    says(X, Y),
    a_truth(Y).

# ork_says_bog_is_from_venus, hypothesis.
says(ork, bog_is_from_venus) <- .

# bog_says_ork_is_from_mar, hypothesis.
says(bog, ork_is_from_mars) <- .

# ork_says_bog_is_male, hypothesis.
says(ork, bog_is_male) <- .

# bog_says_ork_is_female, hypothesis.
says(bog, ork_is_female) <- .

# bog_is_from_venus1, hypothesis.
from_venus(bog) <- 
    a_truth(bog_is_from_venus).

# ork_is_from_mars1, hypothesis.
from_mars(ork) <- 
    a_truth(ork_is_from_mars).

# bog_is_male1, hypothesis.
male(bog) <- 
    a_truth(bog_is_male).

# ork_is_female1, hypothesis.
female(ork) <- 
    a_truth(ork_is_female).

# bog_is_from_venus2, hypothesis.
a_truth(bog_is_from_venus) <- 
    from_venus(bog).

# ork_is_from_mars2, hypothesis.
a_truth(ork_is_from_mars) <- 
    from_mars(ork).

# bog_is_male2, hypothesis.
a_truth(bog_is_male) <- 
    male(bog).

# ork_is_female2, hypothesis.
a_truth(ork_is_female) <- 
    female(ork).

# prove_bog_is_female, conjecture.
 <- female(bog).

#--------------------------------------------------------------------------