#--------------------------------------------------------------------------
# File     : PUZ005-1 : TPTP v2.1.0. Released v1.0.0.
# Domain   : Puzzles
# Problem  : Lions and Unicorns
# Version  : Special.
# English  : Lion lies on Monday, Tuesday and Wednesday. Unicorn lies 
#            on Thursday, Friday and Saturday. Both tell truth on other 
#            days. Both say yesterday was one of their lying days. Prove 
#            that today is Thursday.

# Refs     : [Smu78] Smullyan (1978), What is the Name of This Book? The Ri
#          : [OS85]  Ohlbach & Schmidt-Schauss M. (1985), The Lion and the 
# Source   : [OS85]
# Names    : Lion and the Unicorn [OS85]

# Status   : unsatisfiable
# Rating   : 0.33 v2.1.0, 0.00 v2.0.0
# Syntax   : Number of clauses    :   51 (   6 non-Horn;   3 unit;  48 RR)
#            Number of literals   :  112 (   0 equality)
#            Maximal clause size  :    7 (   2 average)
#            Number of predicates :    9 (   0 propositional; 1-3 arity)
#            Number of functors   :    5 (   3 constant; 0-1 arity)
#            Number of variables  :   56 (   0 singleton)
#            Maximal term depth   :    2 (   1 average)

# Comments : 
#          : tptp2X -f setheo:sign -t rm_equality:rstfp PUZ005-1.p 
#--------------------------------------------------------------------------
# it_is_a_day, axiom.
monday(X);
tuesday(X);
wednesday(X);
thursday(X);
friday(X);
saturday(X);
sunday(X) <- .

# monday_not_tuesday, axiom.
 <- monday(X),
    tuesday(X).

# monday_not_wednesday, axiom.
 <- monday(X),
    wednesday(X).

# monday_not_thursday, axiom.
 <- monday(X),
    thursday(X).

# monday_not_friday, axiom.
 <- monday(X),
    friday(X).

# monday_not_saturday, axiom.
 <- monday(X),
    saturday(X).

# monday_not_sunday, axiom.
 <- monday(X),
    sunday(X).

# tuesday_not_wednesday, axiom.
 <- tuesday(X),
    wednesday(X).

# tuesday_not_thursday, axiom.
 <- tuesday(X),
    thursday(X).

# tuesday_not_friday, axiom.
 <- tuesday(X),
    friday(X).

# tuesday_not_saturday, axiom.
 <- tuesday(X),
    saturday(X).

# tuesday_not_sunday, axiom.
 <- tuesday(X),
    sunday(X).

# wednesday_not_thursday, axiom.
 <- wednesday(X),
    thursday(X).

# wednesday_not_friday, axiom.
 <- wednesday(X),
    friday(X).

# wednesday_not_saturday, axiom.
 <- wednesday(X),
    saturday(X).

# wednesday_not_sunday, axiom.
 <- wednesday(X),
    sunday(X).

# thursday_not_friday, axiom.
 <- thursday(X),
    friday(X).

# thursday_not_saturday, axiom.
 <- thursday(X),
    saturday(X).

# thursday_not_sunday, axiom.
 <- thursday(X),
    sunday(X).

# friday_not_saturday, axiom.
 <- friday(X),
    saturday(X).

# friday_not_sunday, axiom.
 <- friday(X),
    sunday(X).

# saturday_not_sunday, axiom.
 <- saturday(X),
    sunday(X).

# monday_yesterday, axiom.
tuesday(X) <- 
    monday(yesterday(X)).

# tuesday_yesterday, axiom.
wednesday(X) <- 
    tuesday(yesterday(X)).

# wednesday_yesterday, axiom.
thursday(X) <- 
    wednesday(yesterday(X)).

# thursday_yesterday, axiom.
friday(X) <- 
    thursday(yesterday(X)).

# friday_yesterday, axiom.
saturday(X) <- 
    friday(yesterday(X)).

# saturday_yesterday, axiom.
sunday(X) <- 
    saturday(yesterday(X)).

# sunday_yesterday, axiom.
monday(X) <- 
    sunday(yesterday(X)).

# yesterday_monday, axiom.
monday(yesterday(X)) <- 
    tuesday(X).

# yesterday_tuesday, axiom.
tuesday(yesterday(X)) <- 
    wednesday(X).

# yesterday_wednesday, axiom.
wednesday(yesterday(X)) <- 
    thursday(X).

# yesterday_thursday, axiom.
thursday(yesterday(X)) <- 
    friday(X).

# yesterday_friday, axiom.
friday(yesterday(X)) <- 
    saturday(X).

# yesterday_saturday, axiom.
saturday(yesterday(X)) <- 
    sunday(X).

# yesterday_sunday, axiom.
sunday(yesterday(X)) <- 
    monday(X).

# lions_lying_days, axiom.
monday(X);
tuesday(X);
wednesday(X) <- 
    member(X, lying_days(lion)).

# unicorns_lying_days, axiom.
thursday(X);
friday(X);
saturday(X) <- 
    member(X, lying_days(unicorn)).

# lion_lies_on_monday, axiom.
member(X, lying_days(lion)) <- 
    monday(X).

# lion_lies_on_tuesday, axiom.
member(X, lying_days(lion)) <- 
    tuesday(X).

# lion_lies_on_wednesday, axiom.
member(X, lying_days(lion)) <- 
    wednesday(X).

# unicorn_lies_on_thursday, axiom.
member(X, lying_days(unicorn)) <- 
    thursday(X).

# unicorn_lies_on_friday, axiom.
member(X, lying_days(unicorn)) <- 
    friday(X).

# unicorn_lies_on_saturday, axiom.
member(X, lying_days(unicorn)) <- 
    saturday(X).

# admissions1, axiom.
member(X, lying_days(T));
member(Y, lying_days(T)) <- 
    admits(T, X, Y).

# admissions2, axiom.
member(X, lying_days(T));
admits(T, X, Y) <- 
    member(Y, lying_days(T)).

# admissions3, axiom.
 <- member(X, lying_days(T)),
    admits(T, X, Y),
    member(Y, lying_days(T)).

# admissions4, axiom.
admits(T, X, Y);
member(Y, lying_days(T)) <- 
    member(X, lying_days(T)).

# admissions5, axiom.
admits(lion, today, yesterday(today)) <- .

# admissions6, axiom.
admits(unicorn, today, yesterday(today)) <- .

# prove_today_is_thursday, conjecture.
 <- thursday(today).

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