%------------------------------------------------------------------------------
% File     : PUZ162_1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Puzzles
% Problem  : Where should Angela Merkel sit in the Compiegne Lit Wagon?
% Version  : Especial.
% English  : Given that the A-side of the Compiegne Lit Wagon table is 
%            associated with Foch and Hitler, while the C side is associated 
%            with Erzberger and Hutzinger, and no one can take Merkel's and 
%            Macron's picture if she sits at B, Merkel and Macron should sit 
%            at D.

% Refs     : [Kal00] Kahlert (2000), Email to Geoff Sutcliffe
% Source   : [Kal00]
% Names    : merkel-seating.tptp [Kal00]

% Status   : Theorem
% Rating   : 0.00 v9.3.0
% Syntax   : Number of formulae    :  115 (  46 unt;  59 typ;   0 def)
%            Number of atoms       :   82 (   0 equ)
%            Maximal formula atoms :   11 (   1 avg)
%            Number of connectives :   28 (   2   ~;   0   |;  16   &)
%                                         (   0 <=>;  10  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   20 (   2 avg)
%            Maximal term depth    :    1 (   1 avg)
%            Number of types       :    8 (   7 usr)
%            Number of type conns  :   34 (  18   >;  16   *;   0   +;   0  <<)
%            Number of predicates  :   18 (  18 usr;   0 prp; 1-3 aty)
%            Number of functors    :   34 (  34 usr;  34 con; 0-0 aty)
%            Number of variables   :   29 (  29   !;   0   ?;  29   :)
% SPC      : TF0_THM_NEQ_NAR

% Comments : The year 2000 in [Kal00] might be wrong.
%------------------------------------------------------------------------------
tff(geographicalRegion_type,type,
    geographicalRegion: $tType ).

tff(event_type,type,
    event: $tType ).

tff(diplomaticEvent_attrib,type,
    diplomaticEvent: event > $o ).

tff(seatingEvent_attrib,type,
    seatingEvent: event > $o ).

tff(subEvents_rel,type,
    subEvents: ( event * event ) > $o ).

tff(endsBeforeStartOf_rel,type,
    endsBeforeStartOf: ( event * event ) > $o ).

tff(endsBeforeStartOf_trans,axiom,
    ! [X: event,Y: event,Z: event] :
      ( ( endsBeforeStartOf(X,Y)
        & endsBeforeStartOf(Y,Z) )
     => endsBeforeStartOf(X,Z) ) ).

% tff(subEventsOverlap, axiom, (
%     ![X: event, Y:event] :
%      (subEvents(X,Y) => (~endsBeforeStartOf(X,Y) & ~endsBeforeStartOf(Y,X))))).

tff(contentiousEvent_attrib,type,
    contentiousEvent: event > $o ).

tff(friendlyEvent_attrib,type,
    friendlyEvent: event > $o ).

tff(friendlyIsNotContentious_ax,axiom,
    ! [E: event] :
      ( friendlyEvent(E)
     => ~ contentiousEvent(E) ) ).

tff(contentiousIsNotFriendly_ax,axiom,
    ! [E: event] :
      ( contentiousEvent(E)
     => ~ friendlyEvent(E) ) ).

tff(armistice_attrib,type,
    armistice: event > $o ).

tff(armisticesAreContentious,axiom,
    ! [E: event] :
      ( armistice(E)
     => contentiousEvent(E) ) ).

tff(armisticesAreDiplomatic,axiom,
    ! [E: event] :
      ( armistice(E)
     => diplomaticEvent(E) ) ).

%---- geographical infrastructure ----
tff(eventOccursAt_attr,type,
    eventOccursAt: ( event * geographicalRegion ) > $o ).

tff(subRegions_rel,type,
    subRegions: ( geographicalRegion * geographicalRegion ) > $o ).

tff(subRegions_trans,axiom,
    ! [X: geographicalRegion,Y: geographicalRegion,Z: geographicalRegion] :
      ( ( subRegions(X,Y)
        & subRegions(Y,Z) )
     => subRegions(X,Z) ) ).

tff(eventOccursAt_trans,axiom,
    ! [X: geographicalRegion,Y: geographicalRegion,Z: event] :
      ( ( eventOccursAt(Z,X)
        & subRegions(Y,X) )
     => eventOccursAt(Z,Y) ) ).

tff(rethondes_inst,type,
    rethondesCompiegne: geographicalRegion ).

tff(picardy_inst,type,
    picardy: geographicalRegion ).

tff(rethondes_in_picardy,axiom,
    subRegions(picardy,rethondesCompiegne) ).

tff(hautsDeFrance_inst,type,
    hautsDeFrance: geographicalRegion ).

tff(picardyInHautsDeFrance,axiom,
    subRegions(hautsDeFrance,picardy) ).

tff(france_inst,type,
    france: geographicalRegion ).

tff(hautsDeFranceInFrance,axiom,
    subRegions(france,hautsDeFrance) ).

%---- government hierarchy
tff(constructedContinuity,type,
    constrCont: $tType ).

tff(germaniaGermanyStar,type,
    germania: constrCont ).

tff(marianneFranceStar,type,
    marianne: constrCont ).

tff(government_type,type,
    govt: $tType ).

tff(germanEmpireGovt,type,
    germanEmpire: govt ).

tff(weimarRepublicGovt,type,
    weimarRepublic: govt ).

tff(thirdReichGovt,type,
    thirdReich: govt ).

tff(alliedOccupiedGermanyGovt,type,
    alliedOccupiedGermany: govt ).

tff(federalGermanRepublicGovt,type,
    federalGermanRepublic: govt ).

tff(empireOfNapoleon3Govt,type,
    empireOfNapoleonIII: govt ).

tff(thirdRepublicOfFrance,type,
    thirdRepublicFrench: govt ).

tff(fourthRepublicOfFrance,type,
    fourthRepublicFrench: govt ).

tff(fifthRepublicOfFrance,type,
    fifthRepublicFrench: govt ).

tff(narrativeSuccessor_rel,type,
    narrativeSuccessor: ( constrCont * govt * govt ) > $o ).

tff(narrativeSuccessor_ax,axiom,
    ! [CC: constrCont,PR: govt,LT: govt,BW: govt] :
      ( ( narrativeSuccessor(CC,PR,BW)
        & narrativeSuccessor(CC,BW,LT) )
     => narrativeSuccessor(CC,PR,LT) ) ).

tff(germania_01,axiom,
    narrativeSuccessor(germania,germanEmpire,weimarRepublic) ).

tff(germania_02,axiom,
    narrativeSuccessor(germania,weimarRepublic,thirdReich) ).

tff(germania_03,axiom,
    narrativeSuccessor(germania,thirdReich,alliedOccupiedGermany) ).

tff(germania_04,axiom,
    narrativeSuccessor(germania,alliedOccupiedGermany,federalGermanRepublic) ).

tff(marianne_01,axiom,
    narrativeSuccessor(marianne,empireOfNapoleonIII,thirdRepublicFrench) ).

tff(marianne_02,axiom,
    narrativeSuccessor(marianne,thirdRepublicFrench,fourthRepublicFrench) ).

tff(marianne_03,axiom,
    narrativeSuccessor(marianne,fourthRepublicFrench,fifthRepublicFrench) ).

%---- actor hierarchy
tff(person_type,type,
    person: $tType ).

tff(performedBy_rel,type,
    performedBy: ( event * person ) > $o ).

tff(govtRepresentedBy_3rel,type,
    govtRepresentedBy: ( event * govt * person ) > $o ).

tff(dictatedBy_rel,type,
    dictatedBy: ( event * govt ) > $o ).

tff(dictatedTo_rel,type,
    dictatedTo: ( event * govt ) > $o ).

%--- table and seating infrastructure ---
tff(table_side_type,type,
    table_side: $tType ).

tff(table_type,type,
    table: $tType ).

tff(tableUsed_rel,type,
    tableUsed: ( event * table ) > $o ).

tff(seatedAtSide_rel,type,
    seatedAtSide: ( event * table_side ) > $o ).

%--- Construct the CWL table
tff(cwlTable_inst_1,type,
    cwlTable2419d: table ).

tff(cwlTable_inst_2,type,
    cwlTable2439d: table ).

tff(cwlTableSideA_inst,type,
    cwlTableSideA: table_side ).

tff(cwlTableSideB_inst,type,
    cwlTableSideB: table_side ).

tff(cwlTableSideC_inst,type,
    cwlTableSideC: table_side ).

tff(cwlTableSideD_inst,type,
    cwlTableSideD: table_side ).

% ==== Armistice of 1918 ====
tff(foch_inst,type,
    foch: person ).

tff(erzberger_inst,type,
    erzberger: person ).

tff(armistice1918_event,type,
    armistice1918: event ).

tff(armistice1918_typing,axiom,
    armistice(armistice1918) ).

tff(armistice1918_where,axiom,
    eventOccursAt(armistice1918,rethondesCompiegne) ).

tff(armistice1918_french,axiom,
    govtRepresentedBy(armistice1918,thirdRepublicFrench,foch) ).

tff(armistice1918_german,axiom,
    govtRepresentedBy(armistice1918,germanEmpire,erzberger) ).

tff(armistice1918AlliedSeating_event,type,
    armistice1918AlliedSeating: event ).

tff(armistice1918_AS_ax0,axiom,
    seatingEvent(armistice1918AlliedSeating) ).

tff(armistice1918_AS_ax1,axiom,
    subEvents(armistice1918,armistice1918AlliedSeating) ).

tff(armistice1918_AS_ax2,axiom,
    performedBy(armistice1918AlliedSeating,foch) ).

tff(armistice1918_AS_ax3,axiom,
    seatedAtSide(armistice1918AlliedSeating,cwlTableSideA) ).

tff(armistice1918_AS_ax4,axiom,
    tableUsed(armistice1918AlliedSeating,cwlTable2419d) ).

tff(armistice1918GermanSeating_event,type,
    armistice1918GermanSeating: event ).

tff(armistice1918_GS_ax0,axiom,
    seatingEvent(armistice1918GermanSeating) ).

tff(armistice1918_GS_ax1,axiom,
    subEvents(armistice1918,armistice1918GermanSeating) ).

tff(armistice1918_GS_ax2,axiom,
    performedBy(armistice1918GermanSeating,erzberger) ).

tff(armistice1918_GS_ax3,axiom,
    seatedAtSide(armistice1918GermanSeating,cwlTableSideC) ).

tff(armistice1918_GS_ax4,axiom,
    tableUsed(armistice1918GermanSeating,cwlTable2419d) ).

% ===== Armistice of 1940 =====
tff(hitler_inst,type,
    hitler: person ).

tff(hutzinger_inst,type,
    hutzinger: person ).

tff(armistice1940_event,type,
    armistice1940: event ).

tff(armistice1940_typing,axiom,
    armistice(armistice1940) ).

tff(armistice1940_where,axiom,
    eventOccursAt(armistice1940,rethondesCompiegne) ).

tff(armistice1940_hutzinger,axiom,
    govtRepresentedBy(armistice1940,thirdRepublicFrench,hutzinger) ).

tff(armistice1940_hitler,axiom,
    govtRepresentedBy(armistice1940,thirdReich,hitler) ).

tff(armistice1940_past1918,axiom,
    endsBeforeStartOf(armistice1918,armistice1940) ).

tff(armistice1940GermanSeating_event,type,
    armistice1940GermanSeating: event ).

tff(armistice1940_GS_ax0,axiom,
    seatingEvent(armistice1940GermanSeating) ).

tff(armistice1940_GS_ax1,axiom,
    subEvents(armistice1940,armistice1940GermanSeating) ).

tff(armistice1940_GS_ax2,axiom,
    performedBy(armistice1940GermanSeating,hitler) ).

tff(armistice1940_GS_ax3,axiom,
    seatedAtSide(armistice1940GermanSeating,cwlTableSideA) ).

tff(armistice1940_GS_ax4,axiom,
    tableUsed(armistice1940GermanSeating,cwlTable2419d) ).

tff(armistice1940FrenchSeating_event,type,
    armistice1940FrenchSeating: event ).

tff(armistice1940_FS_ax0,axiom,
    seatingEvent(armistice1940FrenchSeating) ).

tff(armistice1940_FS_ax1,axiom,
    subEvents(armistice1940,armistice1940FrenchSeating) ).

tff(armistice1940_FS_ax2,axiom,
    performedBy(armistice1940FrenchSeating,hutzinger) ).

tff(armistice1940_FS_ax3,axiom,
    seatedAtSide(armistice1940FrenchSeating,cwlTableSideC) ).

tff(armistice1940_FS_ax4,axiom,
    tableUsed(armistice1940FrenchSeating,cwlTable2419d) ).

% ===== The Visit in 2018 ======

tff(merkel_inst,type,
    merkel: person ).

tff(macron_inst,type,
    macron: person ).

tff(compiegneVisit2018_event,type,
    compiegneVisit2018: event ).

tff(compiegneVisit2018_where,axiom,
    eventOccursAt(compiegneVisit2018,rethondesCompiegne) ).

tff(compiegneVisit2018_diplomatic,axiom,
    diplomaticEvent(compiegneVisit2018) ).

tff(compiegneVisit2018_friendly,axiom,
    friendlyEvent(compiegneVisit2018) ).

tff(compiegneVisit2018_merkel,axiom,
    govtRepresentedBy(compiegneVisit2018,federalGermanRepublic,merkel) ).

tff(compiegneVisit2018_macron,axiom,
    govtRepresentedBy(compiegneVisit2018,fifthRepublicFrench,macron) ).

tff(armistice2018_past1940,axiom,
    endsBeforeStartOf(armistice1940,compiegneVisit2018) ).

tff(avoidTableSide_rel,type,
    avoidTableSide: ( person * event * table_side ) > $o ).

tff(pastColocatedDiplomaticEvent_rel,type,
    pastColocatedDiplomaticEvent: ( event * event ) > $o ).

tff(pastColocatedDiplomaticEvent_rule,axiom,
    ! [DE: event,VE: event,LOC: geographicalRegion] :
      ( ( diplomaticEvent(DE)
        & eventOccursAt(DE,LOC)
        & eventOccursAt(VE,LOC)
        & endsBeforeStartOf(DE,VE) )
     => pastColocatedDiplomaticEvent(VE,DE) ) ).

tff(dontSitWherePastConflictSat,axiom,
    ! [P: person,RP: person,PASTGOVT: govt,GOVT: govt,CC: constrCont,VE: event,DE: event,SE: event,TS: table_side] :
      ( ( pastColocatedDiplomaticEvent(VE,DE)
        & contentiousEvent(DE)
        & subEvents(DE,SE)
        & seatingEvent(SE)
        & performedBy(SE,RP)
        & seatedAtSide(SE,TS)
        & govtRepresentedBy(DE,PASTGOVT,RP)
        & narrativeSuccessor(CC,PASTGOVT,GOVT)
        & friendlyEvent(VE)
        & govtRepresentedBy(VE,GOVT,P) )
     => avoidTableSide(P,VE,TS) ) ).

tff(whereShouldMacronSit,conjecture,
    avoidTableSide(macron,compiegneVisit2018,cwlTableSideC) ).

%------------------------------------------------------------------------------