%--------------------------------------------------------------------------
% 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 tptp -t rm_equality:rstfp PUZ005-1.p 
%--------------------------------------------------------------------------
input_clause(it_is_a_day,axiom,
    [++ monday(X),
     ++ tuesday(X),
     ++ wednesday(X),
     ++ thursday(X),
     ++ friday(X),
     ++ saturday(X),
     ++ sunday(X)]).

input_clause(monday_not_tuesday,axiom,
    [-- monday(X),
     -- tuesday(X)]).

input_clause(monday_not_wednesday,axiom,
    [-- monday(X),
     -- wednesday(X)]).

input_clause(monday_not_thursday,axiom,
    [-- monday(X),
     -- thursday(X)]).

input_clause(monday_not_friday,axiom,
    [-- monday(X),
     -- friday(X)]).

input_clause(monday_not_saturday,axiom,
    [-- monday(X),
     -- saturday(X)]).

input_clause(monday_not_sunday,axiom,
    [-- monday(X),
     -- sunday(X)]).

input_clause(tuesday_not_wednesday,axiom,
    [-- tuesday(X),
     -- wednesday(X)]).

input_clause(tuesday_not_thursday,axiom,
    [-- tuesday(X),
     -- thursday(X)]).

input_clause(tuesday_not_friday,axiom,
    [-- tuesday(X),
     -- friday(X)]).

input_clause(tuesday_not_saturday,axiom,
    [-- tuesday(X),
     -- saturday(X)]).

input_clause(tuesday_not_sunday,axiom,
    [-- tuesday(X),
     -- sunday(X)]).

input_clause(wednesday_not_thursday,axiom,
    [-- wednesday(X),
     -- thursday(X)]).

input_clause(wednesday_not_friday,axiom,
    [-- wednesday(X),
     -- friday(X)]).

input_clause(wednesday_not_saturday,axiom,
    [-- wednesday(X),
     -- saturday(X)]).

input_clause(wednesday_not_sunday,axiom,
    [-- wednesday(X),
     -- sunday(X)]).

input_clause(thursday_not_friday,axiom,
    [-- thursday(X),
     -- friday(X)]).

input_clause(thursday_not_saturday,axiom,
    [-- thursday(X),
     -- saturday(X)]).

input_clause(thursday_not_sunday,axiom,
    [-- thursday(X),
     -- sunday(X)]).

input_clause(friday_not_saturday,axiom,
    [-- friday(X),
     -- saturday(X)]).

input_clause(friday_not_sunday,axiom,
    [-- friday(X),
     -- sunday(X)]).

input_clause(saturday_not_sunday,axiom,
    [-- saturday(X),
     -- sunday(X)]).

input_clause(monday_yesterday,axiom,
    [-- monday(yesterday(X)),
     ++ tuesday(X)]).

input_clause(tuesday_yesterday,axiom,
    [-- tuesday(yesterday(X)),
     ++ wednesday(X)]).

input_clause(wednesday_yesterday,axiom,
    [-- wednesday(yesterday(X)),
     ++ thursday(X)]).

input_clause(thursday_yesterday,axiom,
    [-- thursday(yesterday(X)),
     ++ friday(X)]).

input_clause(friday_yesterday,axiom,
    [-- friday(yesterday(X)),
     ++ saturday(X)]).

input_clause(saturday_yesterday,axiom,
    [-- saturday(yesterday(X)),
     ++ sunday(X)]).

input_clause(sunday_yesterday,axiom,
    [-- sunday(yesterday(X)),
     ++ monday(X)]).

input_clause(yesterday_monday,axiom,
    [++ monday(yesterday(X)),
     -- tuesday(X)]).

input_clause(yesterday_tuesday,axiom,
    [++ tuesday(yesterday(X)),
     -- wednesday(X)]).

input_clause(yesterday_wednesday,axiom,
    [++ wednesday(yesterday(X)),
     -- thursday(X)]).

input_clause(yesterday_thursday,axiom,
    [++ thursday(yesterday(X)),
     -- friday(X)]).

input_clause(yesterday_friday,axiom,
    [++ friday(yesterday(X)),
     -- saturday(X)]).

input_clause(yesterday_saturday,axiom,
    [++ saturday(yesterday(X)),
     -- sunday(X)]).

input_clause(yesterday_sunday,axiom,
    [++ sunday(yesterday(X)),
     -- monday(X)]).

input_clause(lions_lying_days,axiom,
    [-- member(X, lying_days(lion)),
     ++ monday(X),
     ++ tuesday(X),
     ++ wednesday(X)]).

input_clause(unicorns_lying_days,axiom,
    [-- member(X, lying_days(unicorn)),
     ++ thursday(X),
     ++ friday(X),
     ++ saturday(X)]).

input_clause(lion_lies_on_monday,axiom,
    [-- monday(X),
     ++ member(X, lying_days(lion))]).

input_clause(lion_lies_on_tuesday,axiom,
    [-- tuesday(X),
     ++ member(X, lying_days(lion))]).

input_clause(lion_lies_on_wednesday,axiom,
    [-- wednesday(X),
     ++ member(X, lying_days(lion))]).

input_clause(unicorn_lies_on_thursday,axiom,
    [-- thursday(X),
     ++ member(X, lying_days(unicorn))]).

input_clause(unicorn_lies_on_friday,axiom,
    [-- friday(X),
     ++ member(X, lying_days(unicorn))]).

input_clause(unicorn_lies_on_saturday,axiom,
    [-- saturday(X),
     ++ member(X, lying_days(unicorn))]).

input_clause(admissions1,axiom,
    [++ member(X, lying_days(T)),
     -- admits(T, X, Y),
     ++ member(Y, lying_days(T))]).

input_clause(admissions2,axiom,
    [++ member(X, lying_days(T)),
     ++ admits(T, X, Y),
     -- member(Y, lying_days(T))]).

input_clause(admissions3,axiom,
    [-- member(X, lying_days(T)),
     -- admits(T, X, Y),
     -- member(Y, lying_days(T))]).

input_clause(admissions4,axiom,
    [-- member(X, lying_days(T)),
     ++ admits(T, X, Y),
     ++ member(Y, lying_days(T))]).

input_clause(admissions5,axiom,
    [++ admits(lion, today, yesterday(today))]).

input_clause(admissions6,axiom,
    [++ admits(unicorn, today, yesterday(today))]).

input_clause(prove_today_is_thursday,conjecture,
    [-- thursday(today)]).
%--------------------------------------------------------------------------