%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PUZ161_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:21:29 AM UTC 2026
% Result : Theorem 4.51s 2.06s
% Output : Refutation 4.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 55
% Syntax : Number of formulae : 112 ( 92 unt; 0 typ; 0 def)
% Number of atoms : 164 ( 0 equ; 0 cnn)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 387 ( 6 ~; 0 |; 32 &; 329 @)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Number of types : 8 ( 7 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 47 ( 46 usr; 31 con; 0-3 aty)
% Number of variables : 58 ( 0 ^; 58 !; 0 ?; 58 :)
% Comments :
%------------------------------------------------------------------------------
thf(geographicalRegion_type,type,
geographicalRegion: $tType ).
thf(event_type,type,
event: $tType ).
thf(constrCont_type,type,
constrCont: $tType ).
thf(govt_type,type,
govt: $tType ).
thf(person_type,type,
person: $tType ).
thf(table_side_type,type,
table_side: $tType ).
thf(table_type,type,
table: $tType ).
thf(diplomaticEvent_decl,type,
diplomaticEvent: event > $o ).
thf(seatingEvent_decl,type,
seatingEvent: event > $o ).
thf(subEvents_decl,type,
subEvents: event > event > $o ).
thf(endsBeforeStartOf_decl,type,
endsBeforeStartOf: event > event > $o ).
thf(contentiousEvent_decl,type,
contentiousEvent: event > $o ).
thf(friendlyEvent_decl,type,
friendlyEvent: event > $o ).
thf(armistice_decl,type,
armistice: event > $o ).
thf(eventOccursAt_decl,type,
eventOccursAt: event > geographicalRegion > $o ).
thf(subRegions_decl,type,
subRegions: geographicalRegion > geographicalRegion > $o ).
thf(rethondesCompiegne_decl,type,
rethondesCompiegne: geographicalRegion ).
thf(picardy_decl,type,
picardy: geographicalRegion ).
thf(hautsDeFrance_decl,type,
hautsDeFrance: geographicalRegion ).
thf(germania_decl,type,
germania: constrCont ).
thf(marianne_decl,type,
marianne: constrCont ).
thf(germanEmpire_decl,type,
germanEmpire: govt ).
thf(weimarRepublic_decl,type,
weimarRepublic: govt ).
thf(thirdReich_decl,type,
thirdReich: govt ).
thf(alliedOccupiedGermany_decl,type,
alliedOccupiedGermany: govt ).
thf(federalGermanRepublic_decl,type,
federalGermanRepublic: govt ).
thf(empireOfNapoleonIII_decl,type,
empireOfNapoleonIII: govt ).
thf(thirdRepublicFrench_decl,type,
thirdRepublicFrench: govt ).
thf(fourthRepublicFrench_decl,type,
fourthRepublicFrench: govt ).
thf(fifthRepublicFrench_decl,type,
fifthRepublicFrench: govt ).
thf(narrativeSuccessor_decl,type,
narrativeSuccessor: constrCont > govt > govt > $o ).
thf(performedBy_decl,type,
performedBy: event > person > $o ).
thf(govtRepresentedBy_decl,type,
govtRepresentedBy: event > govt > person > $o ).
thf(tableUsed_decl,type,
tableUsed: event > table > $o ).
thf(seatedAtSide_decl,type,
seatedAtSide: event > table_side > $o ).
thf(cwlTable2419d_decl,type,
cwlTable2419d: table ).
thf(cwlTableSideA_decl,type,
cwlTableSideA: table_side ).
thf(cwlTableSideC_decl,type,
cwlTableSideC: table_side ).
thf(foch_decl,type,
foch: person ).
thf(erzberger_decl,type,
erzberger: person ).
thf(armistice1918_decl,type,
armistice1918: event ).
thf(armistice1918AlliedSeating_decl,type,
armistice1918AlliedSeating: event ).
thf(armistice1918GermanSeating_decl,type,
armistice1918GermanSeating: event ).
thf(hitler_decl,type,
hitler: person ).
thf(hutzinger_decl,type,
hutzinger: person ).
thf(armistice1940_decl,type,
armistice1940: event ).
thf(armistice1940GermanSeating_decl,type,
armistice1940GermanSeating: event ).
thf(armistice1940FrenchSeating_decl,type,
armistice1940FrenchSeating: event ).
thf(merkel_decl,type,
merkel: person ).
thf(macron_decl,type,
macron: person ).
thf(compiegneVisit2018_decl,type,
compiegneVisit2018: event ).
thf(avoidTableSide_decl,type,
avoidTableSide: person > event > table_side > $o ).
thf(pastColocatedDiplomaticEvent_decl,type,
pastColocatedDiplomaticEvent: event > event > $o ).
thf(44,axiom,
rethondesCompiegne @ ( armistice1918 @ eventOccursAt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_where) ).
thf(110,plain,
rethondesCompiegne @ ( armistice1918 @ eventOccursAt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(13,axiom,
rethondesCompiegne @ ( picardy @ subRegions ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rethondes_in_picardy) ).
thf(70,plain,
rethondesCompiegne @ ( picardy @ subRegions ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(8,axiom,
fifthRepublicFrench @ ( fourthRepublicFrench @ ( marianne @ narrativeSuccessor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',marianne_03) ).
thf(64,plain,
fifthRepublicFrench @ ( fourthRepublicFrench @ ( marianne @ narrativeSuccessor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(52,axiom,
! [A: person,B: person,C: govt,D: govt,E: constrCont,F: event,G: event,H: event,I: table_side] :
( ( ( A @ ( D @ ( F @ govtRepresentedBy ) ) )
& ( F @ friendlyEvent )
& ( D @ ( C @ ( E @ narrativeSuccessor ) ) )
& ( B @ ( C @ ( G @ govtRepresentedBy ) ) )
& ( I @ ( H @ seatedAtSide ) )
& ( B @ ( H @ performedBy ) )
& ( H @ seatingEvent )
& ( H @ ( G @ subEvents ) )
& ( G @ contentiousEvent )
& ( G @ ( F @ pastColocatedDiplomaticEvent ) ) )
=> ( I @ ( F @ ( A @ avoidTableSide ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dontSitWherePastConflictSat) ).
thf(118,plain,
! [A: person,B: person,C: govt,D: govt,E: constrCont,F: event,G: event,H: event,I: table_side] :
( ( ( A @ ( D @ ( F @ govtRepresentedBy ) ) )
& ( F @ friendlyEvent )
& ( D @ ( C @ ( E @ narrativeSuccessor ) ) )
& ( B @ ( C @ ( G @ govtRepresentedBy ) ) )
& ( I @ ( H @ seatedAtSide ) )
& ( B @ ( H @ performedBy ) )
& ( H @ seatingEvent )
& ( H @ ( G @ subEvents ) )
& ( G @ contentiousEvent )
& ( G @ ( F @ pastColocatedDiplomaticEvent ) ) )
=> ( I @ ( F @ ( A @ avoidTableSide ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(14,axiom,
federalGermanRepublic @ ( alliedOccupiedGermany @ ( germania @ narrativeSuccessor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',germania_04) ).
thf(71,plain,
federalGermanRepublic @ ( alliedOccupiedGermany @ ( germania @ narrativeSuccessor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(22,axiom,
rethondesCompiegne @ ( armistice1940 @ eventOccursAt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_where) ).
thf(80,plain,
rethondesCompiegne @ ( armistice1940 @ eventOccursAt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(7,axiom,
picardy @ ( hautsDeFrance @ subRegions ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',picardyInHautsDeFrance) ).
thf(63,plain,
picardy @ ( hautsDeFrance @ subRegions ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(15,axiom,
cwlTable2419d @ ( armistice1940GermanSeating @ tableUsed ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax4) ).
thf(72,plain,
cwlTable2419d @ ( armistice1940GermanSeating @ tableUsed ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(48,axiom,
cwlTableSideA @ ( armistice1918AlliedSeating @ seatedAtSide ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_AS_ax3) ).
thf(114,plain,
cwlTableSideA @ ( armistice1918AlliedSeating @ seatedAtSide ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(12,axiom,
hitler @ ( thirdReich @ ( armistice1940 @ govtRepresentedBy ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_hitler) ).
thf(69,plain,
hitler @ ( thirdReich @ ( armistice1940 @ govtRepresentedBy ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(37,axiom,
armistice1918GermanSeating @ ( armistice1918 @ subEvents ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_GS_ax1) ).
thf(101,plain,
armistice1918GermanSeating @ ( armistice1918 @ subEvents ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(28,axiom,
hitler @ ( armistice1940GermanSeating @ performedBy ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax2) ).
thf(88,plain,
hitler @ ( armistice1940GermanSeating @ performedBy ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(49,axiom,
merkel @ ( federalGermanRepublic @ ( compiegneVisit2018 @ govtRepresentedBy ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compiegneVisit2018_merkel) ).
thf(115,plain,
merkel @ ( federalGermanRepublic @ ( compiegneVisit2018 @ govtRepresentedBy ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(53,axiom,
compiegneVisit2018 @ diplomaticEvent,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compiegneVisit2018_diplomatic) ).
thf(120,plain,
compiegneVisit2018 @ diplomaticEvent,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(31,axiom,
hutzinger @ ( thirdRepublicFrench @ ( armistice1940 @ govtRepresentedBy ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_hutzinger) ).
thf(93,plain,
hutzinger @ ( thirdRepublicFrench @ ( armistice1940 @ govtRepresentedBy ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(1,conjecture,
cwlTableSideA @ ( compiegneVisit2018 @ ( macron @ avoidTableSide ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',whereShouldMacronSit) ).
thf(2,negated_conjecture,
~ ( cwlTableSideA @ ( compiegneVisit2018 @ ( macron @ avoidTableSide ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(57,plain,
~ ( cwlTableSideA @ ( compiegneVisit2018 @ ( macron @ avoidTableSide ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(20,axiom,
cwlTableSideC @ ( armistice1940FrenchSeating @ seatedAtSide ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_FS_ax3) ).
thf(78,plain,
cwlTableSideC @ ( armistice1940FrenchSeating @ seatedAtSide ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(41,axiom,
! [A: event] :
( ( A @ friendlyEvent )
=> ~ ( A @ contentiousEvent ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',friendlyIsNotContentious_ax) ).
thf(106,plain,
! [A: event] :
( ( A @ friendlyEvent )
=> ~ ( A @ contentiousEvent ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(54,axiom,
rethondesCompiegne @ ( compiegneVisit2018 @ eventOccursAt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compiegneVisit2018_where) ).
thf(121,plain,
rethondesCompiegne @ ( compiegneVisit2018 @ eventOccursAt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(26,axiom,
! [A: event,B: event,C: geographicalRegion] :
( ( ( B @ ( A @ endsBeforeStartOf ) )
& ( C @ ( B @ eventOccursAt ) )
& ( C @ ( A @ eventOccursAt ) )
& ( A @ diplomaticEvent ) )
=> ( A @ ( B @ pastColocatedDiplomaticEvent ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pastColocatedDiplomaticEvent_rule) ).
thf(84,plain,
! [A: event,B: event,C: geographicalRegion] :
( ( ( B @ ( A @ endsBeforeStartOf ) )
& ( C @ ( B @ eventOccursAt ) )
& ( C @ ( A @ eventOccursAt ) )
& ( A @ diplomaticEvent ) )
=> ( A @ ( B @ pastColocatedDiplomaticEvent ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(5,axiom,
armistice1918 @ armistice,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_typing) ).
thf(61,plain,
armistice1918 @ armistice,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(29,axiom,
hutzinger @ ( armistice1940FrenchSeating @ performedBy ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_FS_ax2) ).
thf(89,plain,
hutzinger @ ( armistice1940FrenchSeating @ performedBy ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(50,axiom,
compiegneVisit2018 @ friendlyEvent,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compiegneVisit2018_friendly) ).
thf(116,plain,
compiegneVisit2018 @ friendlyEvent,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(17,axiom,
erzberger @ ( armistice1918GermanSeating @ performedBy ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_GS_ax2) ).
thf(74,plain,
erzberger @ ( armistice1918GermanSeating @ performedBy ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(38,axiom,
erzberger @ ( germanEmpire @ ( armistice1918 @ govtRepresentedBy ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_german) ).
thf(102,plain,
erzberger @ ( germanEmpire @ ( armistice1918 @ govtRepresentedBy ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(4,axiom,
cwlTable2419d @ ( armistice1918GermanSeating @ tableUsed ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_GS_ax4) ).
thf(60,plain,
cwlTable2419d @ ( armistice1918GermanSeating @ tableUsed ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(51,axiom,
compiegneVisit2018 @ ( armistice1940 @ endsBeforeStartOf ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice2018_past1940) ).
thf(117,plain,
compiegneVisit2018 @ ( armistice1940 @ endsBeforeStartOf ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(9,axiom,
armistice1918AlliedSeating @ seatingEvent,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_AS_ax0) ).
thf(65,plain,
armistice1918AlliedSeating @ seatingEvent,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(34,axiom,
! [A: event,B: event,C: event] :
( ( ( C @ ( B @ endsBeforeStartOf ) )
& ( B @ ( A @ endsBeforeStartOf ) ) )
=> ( C @ ( A @ endsBeforeStartOf ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',endsBeforeStartOf_trans) ).
thf(97,plain,
! [A: event,B: event,C: event] :
( ( ( C @ ( B @ endsBeforeStartOf ) )
& ( B @ ( A @ endsBeforeStartOf ) ) )
=> ( C @ ( A @ endsBeforeStartOf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(43,axiom,
cwlTable2419d @ ( armistice1918AlliedSeating @ tableUsed ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_AS_ax4) ).
thf(109,plain,
cwlTable2419d @ ( armistice1918AlliedSeating @ tableUsed ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(19,axiom,
alliedOccupiedGermany @ ( thirdReich @ ( germania @ narrativeSuccessor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',germania_03) ).
thf(77,plain,
alliedOccupiedGermany @ ( thirdReich @ ( germania @ narrativeSuccessor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(33,axiom,
fourthRepublicFrench @ ( thirdRepublicFrench @ ( marianne @ narrativeSuccessor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',marianne_02) ).
thf(96,plain,
fourthRepublicFrench @ ( thirdRepublicFrench @ ( marianne @ narrativeSuccessor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(16,axiom,
cwlTableSideC @ ( armistice1918GermanSeating @ seatedAtSide ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_GS_ax3) ).
thf(73,plain,
cwlTableSideC @ ( armistice1918GermanSeating @ seatedAtSide ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(40,axiom,
weimarRepublic @ ( germanEmpire @ ( germania @ narrativeSuccessor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',germania_01) ).
thf(105,plain,
weimarRepublic @ ( germanEmpire @ ( germania @ narrativeSuccessor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(47,axiom,
foch @ ( armistice1918AlliedSeating @ performedBy ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_AS_ax2) ).
thf(113,plain,
foch @ ( armistice1918AlliedSeating @ performedBy ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(23,axiom,
armistice1940 @ armistice,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_typing) ).
thf(81,plain,
armistice1940 @ armistice,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(39,axiom,
! [A: event] :
( ( A @ armistice )
=> ( A @ contentiousEvent ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armisticesAreContentious) ).
thf(103,plain,
! [A: event] :
( ( A @ armistice )
=> ( A @ contentiousEvent ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(10,axiom,
! [A: event] :
( ( A @ armistice )
=> ( A @ diplomaticEvent ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armisticesAreDiplomatic) ).
thf(66,plain,
! [A: event] :
( ( A @ armistice )
=> ( A @ diplomaticEvent ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(42,axiom,
armistice1918AlliedSeating @ ( armistice1918 @ subEvents ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_AS_ax1) ).
thf(108,plain,
armistice1918AlliedSeating @ ( armistice1918 @ subEvents ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(46,axiom,
armistice1940GermanSeating @ ( armistice1940 @ subEvents ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax1) ).
thf(112,plain,
armistice1940GermanSeating @ ( armistice1940 @ subEvents ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(56,axiom,
cwlTableSideA @ ( armistice1940GermanSeating @ seatedAtSide ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax3) ).
thf(123,plain,
cwlTableSideA @ ( armistice1940GermanSeating @ seatedAtSide ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(35,axiom,
armistice1918GermanSeating @ seatingEvent,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_GS_ax0) ).
thf(99,plain,
armistice1918GermanSeating @ seatingEvent,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(27,axiom,
foch @ ( thirdRepublicFrench @ ( armistice1918 @ govtRepresentedBy ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1918_french) ).
thf(87,plain,
foch @ ( thirdRepublicFrench @ ( armistice1918 @ govtRepresentedBy ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(18,axiom,
! [A: event] :
( ( A @ contentiousEvent )
=> ~ ( A @ friendlyEvent ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',contentiousIsNotFriendly_ax) ).
thf(75,plain,
! [A: event] :
( ( A @ contentiousEvent )
=> ~ ( A @ friendlyEvent ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(3,axiom,
! [A: geographicalRegion,B: geographicalRegion,C: geographicalRegion] :
( ( ( C @ ( B @ subRegions ) )
& ( B @ ( A @ subRegions ) ) )
=> ( C @ ( A @ subRegions ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subRegions_trans) ).
thf(58,plain,
! [A: geographicalRegion,B: geographicalRegion,C: geographicalRegion] :
( ( ( C @ ( B @ subRegions ) )
& ( B @ ( A @ subRegions ) ) )
=> ( C @ ( A @ subRegions ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(24,axiom,
thirdReich @ ( weimarRepublic @ ( germania @ narrativeSuccessor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',germania_02) ).
thf(82,plain,
thirdReich @ ( weimarRepublic @ ( germania @ narrativeSuccessor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(21,axiom,
thirdRepublicFrench @ ( empireOfNapoleonIII @ ( marianne @ narrativeSuccessor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',marianne_01) ).
thf(79,plain,
thirdRepublicFrench @ ( empireOfNapoleonIII @ ( marianne @ narrativeSuccessor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(32,axiom,
! [A: geographicalRegion,B: geographicalRegion,C: event] :
( ( ( A @ ( B @ subRegions ) )
& ( A @ ( C @ eventOccursAt ) ) )
=> ( B @ ( C @ eventOccursAt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',eventOccursAt_trans) ).
thf(94,plain,
! [A: geographicalRegion,B: geographicalRegion,C: event] :
( ( ( A @ ( B @ subRegions ) )
& ( A @ ( C @ eventOccursAt ) ) )
=> ( B @ ( C @ eventOccursAt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(11,axiom,
armistice1940FrenchSeating @ seatingEvent,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_FS_ax0) ).
thf(68,plain,
armistice1940FrenchSeating @ seatingEvent,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(6,axiom,
cwlTable2419d @ ( armistice1940FrenchSeating @ tableUsed ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_FS_ax4) ).
thf(62,plain,
cwlTable2419d @ ( armistice1940FrenchSeating @ tableUsed ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(55,axiom,
macron @ ( fifthRepublicFrench @ ( compiegneVisit2018 @ govtRepresentedBy ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compiegneVisit2018_macron) ).
thf(122,plain,
macron @ ( fifthRepublicFrench @ ( compiegneVisit2018 @ govtRepresentedBy ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(25,axiom,
armistice1940GermanSeating @ seatingEvent,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax0) ).
thf(83,plain,
armistice1940GermanSeating @ seatingEvent,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(36,axiom,
armistice1940FrenchSeating @ ( armistice1940 @ subEvents ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_FS_ax1) ).
thf(100,plain,
armistice1940FrenchSeating @ ( armistice1940 @ subEvents ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(30,axiom,
! [A: constrCont,B: govt,C: govt,D: govt] :
( ( ( C @ ( D @ ( A @ narrativeSuccessor ) ) )
& ( D @ ( B @ ( A @ narrativeSuccessor ) ) ) )
=> ( C @ ( B @ ( A @ narrativeSuccessor ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',narrativeSuccessor_ax) ).
thf(90,plain,
! [A: constrCont,B: govt,C: govt,D: govt] :
( ( ( C @ ( D @ ( A @ narrativeSuccessor ) ) )
& ( D @ ( B @ ( A @ narrativeSuccessor ) ) ) )
=> ( C @ ( B @ ( A @ narrativeSuccessor ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(45,axiom,
armistice1940 @ ( armistice1918 @ endsBeforeStartOf ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_past1918) ).
thf(111,plain,
armistice1940 @ ( armistice1918 @ endsBeforeStartOf ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(127,plain,
$false,
inference(e,[status(thm)],[110,70,64,118,71,80,63,72,114,69,101,88,115,120,93,57,78,106,121,84,61,89,116,74,102,60,117,65,97,109,77,96,73,105,113,81,103,66,108,112,123,99,87,75,58,82,79,94,68,62,122,83,100,90,111]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ161_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.39 % Computer : n006.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sat Sep 26 05:20:55 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.83/0.99 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.34/1.14 % [INFO] Parsing done (147ms).
% 1.34/1.14 % [INFO] Running in sequential loop mode.
% 1.93/1.36 % [INFO] eprover registered as external prover.
% 1.93/1.37 % [INFO] Scanning for conjecture ...
% 2.21/1.43 % [INFO] Found a conjecture (or negated_conjecture) and 55 axioms. Running axiom selection ...
% 2.21/1.48 % [INFO] Axiom selection finished. Selected 54 axioms (removed 1 axioms).
% 2.46/1.52 % [INFO] Problem is typed first-order (TPTP TFF).
% 2.46/1.53 % [INFO] Type checking passed.
% 2.46/1.53 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 4.51/2.05 % External prover 'e' found a proof!
% 4.51/2.05 % [INFO] Killing All external provers ...
% 4.51/2.05 % Time passed: 1515ms (effective reasoning time: 906ms)
% 4.51/2.05 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 4.51/2.05 % Axioms used in derivation (54): compiegneVisit2018_where, armistice1940_GS_ax2, germania_02, armistice1940_typing, armistice1940_FS_ax1, armistice1940_hitler, armistice1918_GS_ax2, pastColocatedDiplomaticEvent_rule, armistice2018_past1940, narrativeSuccessor_ax, subRegions_trans, friendlyIsNotContentious_ax, contentiousIsNotFriendly_ax, armistice1918_german, armistice1940_FS_ax0, armistice1940_GS_ax1, armistice1918_AS_ax1, armistice1918_GS_ax0, armistice1918_AS_ax2, armistice1918_GS_ax4, armistice1918_GS_ax3, compiegneVisit2018_friendly, marianne_03, endsBeforeStartOf_trans, eventOccursAt_trans, armistice1940_where, armistice1918_AS_ax0, armistice1940_GS_ax3, compiegneVisit2018_macron, armistice1940_FS_ax2, armistice1940_past1918, armistice1918_AS_ax3, armistice1918_where, armistice1940_FS_ax4, rethondes_in_picardy, dontSitWherePastConflictSat, armistice1918_french, germania_04, compiegneVisit2018_merkel, marianne_01, germania_01, armistice1940_hutzinger, compiegneVisit2018_diplomatic, armistice1918_AS_ax4, marianne_02, armisticesAreDiplomatic, armistice1940_GS_ax4, armistice1940_FS_ax3, armistice1918_GS_ax1, armistice1918_typing, picardyInHautsDeFrance, germania_03, armisticesAreContentious, armistice1940_GS_ax0
% 4.51/2.05 % No. of inferences in proof: 112
% 4.51/2.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 1515 ms resp. 906 ms w/o parsing
% 4.51/2.10 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 4.51/2.11 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------