%--------------------------------------------------------------------------
% File     : PUZ018-1 : TPTP v2.4.1. Bugfixed v1.2.0.
% Domain   : Puzzles
% Problem  : The Interns
% Version  : Especial.
% English  : Three interns are residents of the same hospital. On only one 
%            day of the week are all three interns on call. No intern 
%            is on call on three consecutiveutive days. No two interns are 
%            off on the same day more than once a week. The first intern 
%            is off on Sunday, Tuesday, and Thursday. The second intern 
%            is off on Thursday and Saturday. The third intern is off 
%            on Sunday.  Which day of the week are all three interns 
%            on call?

% Refs     : [Rap95] Raptis (1995), Email to G. Sutcliffe
% Source   : [ANL]
% Names    : interns.ver1.in [ANL]

% Status   : unsatisfiable
% Rating   : 0.25 v2.4.0, 0.00 v2.1.0, 0.00 v2.0.0
% Syntax   : Number of clauses    :   48 (   2 non-Horn;  40 unit;  45 RR)
%            Number of literals   :   72 (   0 equality)
%            Maximal clause size  :    7 (   1 average)
%            Number of predicates :    5 (   0 propositional; 1-2 arity)
%            Number of functors   :   10 (  10 constant; 0-0 arity)
%            Number of variables  :   17 (   1 singleton)
%            Maximal term depth   :    1 (   1 average)

% Comments : Dimitris Raptis pointed out [Rap95] that this was trivially
%            unsatisfiable, by resolving prove_all_on_one_day
%            [--all_on(Day)] with all_on_one_day.
%          : tptp2X -f tptp PUZ018-1.p 
% Bugfixes : v1.2.0 - Theorem clause prove_all_on_one_day grounded.
%--------------------------------------------------------------------------
input_clause(all_on_a_on,axiom,
    [-- all_on(X),
     ++ on(a, X)]).

input_clause(all_on_b_on,axiom,
    [-- all_on(X),
     ++ on(b, X)]).

input_clause(all_on_c_on,axiom,
    [-- all_on(X),
     ++ on(c, X)]).

input_clause(all_on,axiom,
    [++ all_on(X),
     -- on(a, X),
     -- on(b, X),
     -- on(c, X)]).

input_clause(all_on_well_defined,axiom,
    [-- all_on(X),
     -- all_on(Y),
     ++ same_day(X, Y)]).

input_clause(monday_follows_sunday,axiom,
    [++ consecutive(sunday, monday)]).

input_clause(tuesday_follows_monday,axiom,
    [++ consecutive(monday, tuesday)]).

input_clause(wednesday_follows_tuesday,axiom,
    [++ consecutive(tuesday, wednesday)]).

input_clause(thursday_follows_wednesday,axiom,
    [++ consecutive(wednesday, thursday)]).

input_clause(friday_follows_thursday,axiom,
    [++ consecutive(thursday, friday)]).

input_clause(staurday_follows_friday,axiom,
    [++ consecutive(friday, saturday)]).

input_clause(sunday_follows_saturday,axiom,
    [++ consecutive(saturday, sunday)]).

input_clause(reflexivity_for_same_person,axiom,
    [++ same_person(X, X)]).

input_clause(a_not_b,axiom,
    [-- same_person(a, b)]).

input_clause(a_not_c,axiom,
    [-- same_person(a, c)]).

input_clause(b_not_c,axiom,
    [-- same_person(b, c)]).

input_clause(reflexivity_for_same_day,axiom,
    [++ same_day(X, X)]).

input_clause(sunday_not_monday,axiom,
    [-- same_day(sunday, monday)]).

input_clause(sunday_not_tuesday,axiom,
    [-- same_day(sunday, tuesday)]).

input_clause(sunday_not_wednesday,axiom,
    [-- same_day(sunday, wednesday)]).

input_clause(sunday_not_thursday,axiom,
    [-- same_day(sunday, thursday)]).

input_clause(sunday_not_friday,axiom,
    [-- same_day(sunday, friday)]).

input_clause(sunday_not_saturday,axiom,
    [-- same_day(sunday, saturday)]).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

input_clause(all_on_one_day,hypothesis,
    [++ all_on(sunday),
     ++ all_on(monday),
     ++ all_on(tuesday),
     ++ all_on(wednesday),
     ++ all_on(thursday),
     ++ all_on(friday),
     ++ all_on(saturday)]).

input_clause(not_on_for_3_days,hypothesis,
    [-- consecutive(X, Y),
     -- consecutive(Y, Z),
     -- consecutive(Z, W),
     -- on(U, X),
     -- on(U, Y),
     -- on(U, Z)]).

input_clause(no_two_off_twice_together,hypothesis,
    [++ on(X, Y),
     ++ on(X, Z),
     ++ on(W, Y),
     ++ on(W, Z),
     ++ same_person(X, W),
     ++ same_day(Y, Z)]).

input_clause(a_off_sunday,hypothesis,
    [-- on(a, sunday)]).

input_clause(a_off_tuesday,hypothesis,
    [-- on(a, tuesday)]).

input_clause(a_off_thursday,hypothesis,
    [-- on(a, thursday)]).

input_clause(b_off_thursday,hypothesis,
    [-- on(b, thursday)]).

input_clause(b_off_saturday,hypothesis,
    [-- on(b, saturday)]).

input_clause(c_off_sunday,hypothesis,
    [-- on(c, sunday)]).

input_clause(prove_all_on_friday,conjecture,
    [-- all_on(friday)]).
%--------------------------------------------------------------------------