%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PUZ161_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:48:51 PM UTC 2026
% Result : Theorem 6.01s 2.31s
% Output : CNFRefutation 6.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 30
% Syntax : Number of formulae : 103 ( 67 unt; 0 typ; 0 def)
% Number of atoms : 239 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 261 ( 125 ~; 114 |; 15 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 8 ( 7 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-3 aty)
% Number of functors : 34 ( 34 usr; 34 con; 0-0 aty)
% Number of variables : 99 ( 99 !; 0 ?; 99 :)
% Comments :
%------------------------------------------------------------------------------
%$ narrativeSuccessor > govtRepresentedBy > avoidTableSide > tableUsed > subRegions > subEvents > seatedAtSide > performedBy > pastColocatedDiplomaticEvent > eventOccursAt > endsBeforeStartOf > dictatedTo > dictatedBy > seatingEvent > friendlyEvent > diplomaticEvent > contentiousEvent > armistice > #nlpp > weimarRepublic > thirdRepublicFrench > thirdReich > rethondesCompiegne > picardy > merkel > marianne > macron > hutzinger > hitler > hautsDeFrance > germania > germanEmpire > france > fourthRepublicFrench > foch > fifthRepublicFrench > federalGermanRepublic > erzberger > empireOfNapoleonIII > cwlTableSideD > cwlTableSideC > cwlTableSideB > cwlTableSideA > cwlTable2439d > cwlTable2419d > compiegneVisit2018 > armistice1940GermanSeating > armistice1940FrenchSeating > armistice1940 > armistice1918GermanSeating > armistice1918AlliedSeating > armistice1918 > alliedOccupiedGermany
%Foreground sorts:
tff(event,type,
event: $tType ).
tff(table_side,type,
table_side: $tType ).
tff(table,type,
table: $tType ).
tff(person,type,
person: $tType ).
tff(constrCont,type,
constrCont: $tType ).
tff(geographicalRegion,type,
geographicalRegion: $tType ).
tff(govt,type,
govt: $tType ).
%Background operators:
%Foreground operators:
tff(eventOccursAt,type,
eventOccursAt: ( event * geographicalRegion ) > $o ).
tff(contentiousEvent,type,
contentiousEvent: event > $o ).
tff(subEvents,type,
subEvents: ( event * event ) > $o ).
tff(france,type,
france: geographicalRegion ).
tff(cwlTableSideC,type,
cwlTableSideC: table_side ).
tff(germania,type,
germania: constrCont ).
tff(fifthRepublicFrench,type,
fifthRepublicFrench: govt ).
tff(cwlTableSideA,type,
cwlTableSideA: table_side ).
tff(erzberger,type,
erzberger: person ).
tff(hutzinger,type,
hutzinger: person ).
tff(govtRepresentedBy,type,
govtRepresentedBy: ( event * govt * person ) > $o ).
tff(performedBy,type,
performedBy: ( event * person ) > $o ).
tff(germanEmpire,type,
germanEmpire: govt ).
tff(hitler,type,
hitler: person ).
tff(avoidTableSide,type,
avoidTableSide: ( person * event * table_side ) > $o ).
tff(cwlTableSideD,type,
cwlTableSideD: table_side ).
tff(empireOfNapoleonIII,type,
empireOfNapoleonIII: govt ).
tff(alliedOccupiedGermany,type,
alliedOccupiedGermany: govt ).
tff(armistice1918GermanSeating,type,
armistice1918GermanSeating: event ).
tff(armistice,type,
armistice: event > $o ).
tff(armistice1918,type,
armistice1918: event ).
tff(rethondesCompiegne,type,
rethondesCompiegne: geographicalRegion ).
tff(macron,type,
macron: person ).
tff(narrativeSuccessor,type,
narrativeSuccessor: ( constrCont * govt * govt ) > $o ).
tff(weimarRepublic,type,
weimarRepublic: govt ).
tff(tableUsed,type,
tableUsed: ( event * table ) > $o ).
tff(cwlTableSideB,type,
cwlTableSideB: table_side ).
tff(armistice1940,type,
armistice1940: event ).
tff(cwlTable2439d,type,
cwlTable2439d: table ).
tff(armistice1940GermanSeating,type,
armistice1940GermanSeating: event ).
tff(marianne,type,
marianne: constrCont ).
tff(armistice1940FrenchSeating,type,
armistice1940FrenchSeating: event ).
tff(fourthRepublicFrench,type,
fourthRepublicFrench: govt ).
tff(merkel,type,
merkel: person ).
tff(hautsDeFrance,type,
hautsDeFrance: geographicalRegion ).
tff(seatedAtSide,type,
seatedAtSide: ( event * table_side ) > $o ).
tff(cwlTable2419d,type,
cwlTable2419d: table ).
tff(subRegions,type,
subRegions: ( geographicalRegion * geographicalRegion ) > $o ).
tff(endsBeforeStartOf,type,
endsBeforeStartOf: ( event * event ) > $o ).
tff(pastColocatedDiplomaticEvent,type,
pastColocatedDiplomaticEvent: ( event * event ) > $o ).
tff(seatingEvent,type,
seatingEvent: event > $o ).
tff(thirdReich,type,
thirdReich: govt ).
tff(diplomaticEvent,type,
diplomaticEvent: event > $o ).
tff(picardy,type,
picardy: geographicalRegion ).
tff(dictatedTo,type,
dictatedTo: ( event * govt ) > $o ).
tff(dictatedBy,type,
dictatedBy: ( event * govt ) > $o ).
tff(federalGermanRepublic,type,
federalGermanRepublic: govt ).
tff(compiegneVisit2018,type,
compiegneVisit2018: event ).
tff(thirdRepublicFrench,type,
thirdRepublicFrench: govt ).
tff(armistice1918AlliedSeating,type,
armistice1918AlliedSeating: event ).
tff(friendlyEvent,type,
friendlyEvent: event > $o ).
tff(foch,type,
foch: person ).
tff(f_162,negated_conjecture,
~ avoidTableSide(macron,compiegneVisit2018,cwlTableSideA),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',whereShouldMacronSit) ).
tff(f_97,axiom,
subEvents(armistice1918,armistice1918AlliedSeating),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1918_AS_ax1) ).
tff(f_96,axiom,
seatingEvent(armistice1918AlliedSeating),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1918_AS_ax0) ).
tff(f_98,axiom,
performedBy(armistice1918AlliedSeating,foch),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1918_AS_ax2) ).
tff(f_99,axiom,
seatedAtSide(armistice1918AlliedSeating,cwlTableSideA),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1918_AS_ax3) ).
tff(f_92,axiom,
armistice(armistice1918),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1918_typing) ).
tff(f_53,axiom,
! [E: event] :
( armistice(E)
=> contentiousEvent(E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armisticesAreContentious) ).
tff(f_81,axiom,
narrativeSuccessor(germania,germanEmpire,weimarRepublic),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',germania_01) ).
tff(f_82,axiom,
narrativeSuccessor(germania,weimarRepublic,thirdReich),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',germania_02) ).
tff(f_80,axiom,
! [CC: constrCont,PR: govt,LT: govt,BW: govt] :
( ( narrativeSuccessor(CC,PR,BW)
& narrativeSuccessor(CC,BW,LT) )
=> narrativeSuccessor(CC,PR,LT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',narrativeSuccessor_ax) ).
tff(f_83,axiom,
narrativeSuccessor(germania,thirdReich,alliedOccupiedGermany),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',germania_03) ).
tff(f_111,axiom,
endsBeforeStartOf(armistice1918,armistice1940),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1940_past1918) ).
tff(f_128,axiom,
endsBeforeStartOf(armistice1940,compiegneVisit2018),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice2018_past1940) ).
tff(f_36,axiom,
! [X: event,Y: event,Z: event] :
( ( endsBeforeStartOf(X,Y)
& endsBeforeStartOf(Y,Z) )
=> endsBeforeStartOf(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',endsBeforeStartOf_trans) ).
tff(f_57,axiom,
! [E: event] :
( armistice(E)
=> diplomaticEvent(E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armisticesAreDiplomatic) ).
tff(f_93,axiom,
eventOccursAt(armistice1918,rethondesCompiegne),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1918_where) ).
tff(f_71,axiom,
subRegions(picardy,rethondesCompiegne),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rethondes_in_picardy) ).
tff(f_70,axiom,
! [X: geographicalRegion,Y: geographicalRegion,Z: event] :
( ( eventOccursAt(Z,X)
& subRegions(Y,X) )
=> eventOccursAt(Z,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eventOccursAt_trans) ).
tff(f_72,axiom,
subRegions(hautsDeFrance,picardy),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',picardyInHautsDeFrance) ).
tff(f_123,axiom,
eventOccursAt(compiegneVisit2018,rethondesCompiegne),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compiegneVisit2018_where) ).
tff(f_138,axiom,
! [DE: event,VE: event,LOC: geographicalRegion] :
( ( diplomaticEvent(DE)
& eventOccursAt(DE,LOC)
& eventOccursAt(VE,LOC)
& endsBeforeStartOf(DE,VE) )
=> pastColocatedDiplomaticEvent(VE,DE) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pastColocatedDiplomaticEvent_rule) ).
tff(f_94,axiom,
govtRepresentedBy(armistice1918,thirdRepublicFrench,foch),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1918_french) ).
tff(f_86,axiom,
narrativeSuccessor(marianne,thirdRepublicFrench,fourthRepublicFrench),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',marianne_02) ).
tff(f_87,axiom,
narrativeSuccessor(marianne,fourthRepublicFrench,fifthRepublicFrench),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',marianne_03) ).
tff(f_125,axiom,
friendlyEvent(compiegneVisit2018),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compiegneVisit2018_friendly) ).
tff(f_127,axiom,
govtRepresentedBy(compiegneVisit2018,fifthRepublicFrench,macron),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compiegneVisit2018_macron) ).
tff(f_160,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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dontSitWherePastConflictSat) ).
tff(f_95,axiom,
govtRepresentedBy(armistice1918,germanEmpire,erzberger),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1918_german) ).
tff(f_84,axiom,
narrativeSuccessor(germania,alliedOccupiedGermany,federalGermanRepublic),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',germania_04) ).
tff(f_126,axiom,
govtRepresentedBy(compiegneVisit2018,federalGermanRepublic,merkel),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compiegneVisit2018_merkel) ).
tff(c_112,plain,
~ avoidTableSide(macron,compiegneVisit2018,cwlTableSideA),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_48,plain,
subEvents(armistice1918,armistice1918AlliedSeating),
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_46,plain,
seatingEvent(armistice1918AlliedSeating),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_50,plain,
performedBy(armistice1918AlliedSeating,foch),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_52,plain,
seatedAtSide(armistice1918AlliedSeating,cwlTableSideA),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_38,plain,
armistice(armistice1918),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_8,plain,
! [E_6: event] :
( contentiousEvent(E_6)
| ~ armistice(E_6) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_24,plain,
narrativeSuccessor(germania,germanEmpire,weimarRepublic),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_26,plain,
narrativeSuccessor(germania,weimarRepublic,thirdReich),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_190,plain,
! [CC_45: constrCont,PR_46: govt,LT_47: govt,BW_48: govt] :
( narrativeSuccessor(CC_45,PR_46,LT_47)
| ~ narrativeSuccessor(CC_45,BW_48,LT_47)
| ~ narrativeSuccessor(CC_45,PR_46,BW_48) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_344,plain,
! [PR_71: govt] :
( narrativeSuccessor(germania,PR_71,thirdReich)
| ~ narrativeSuccessor(germania,PR_71,weimarRepublic) ),
inference(resolution,[status(thm)],[c_26,c_190]) ).
tff(c_348,plain,
narrativeSuccessor(germania,germanEmpire,thirdReich),
inference(resolution,[status(thm)],[c_24,c_344]) ).
tff(c_28,plain,
narrativeSuccessor(germania,thirdReich,alliedOccupiedGermany),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_205,plain,
! [PR_46: govt] :
( narrativeSuccessor(germania,PR_46,alliedOccupiedGermany)
| ~ narrativeSuccessor(germania,PR_46,thirdReich) ),
inference(resolution,[status(thm)],[c_28,c_190]) ).
tff(c_354,plain,
narrativeSuccessor(germania,germanEmpire,alliedOccupiedGermany),
inference(resolution,[status(thm)],[c_348,c_205]) ).
tff(c_74,plain,
endsBeforeStartOf(armistice1918,armistice1940),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_106,plain,
endsBeforeStartOf(armistice1940,compiegneVisit2018),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_149,plain,
! [X_39: event,Z_40: event,Y_41: event] :
( endsBeforeStartOf(X_39,Z_40)
| ~ endsBeforeStartOf(Y_41,Z_40)
| ~ endsBeforeStartOf(X_39,Y_41) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_154,plain,
! [X_39: event] :
( endsBeforeStartOf(X_39,compiegneVisit2018)
| ~ endsBeforeStartOf(X_39,armistice1940) ),
inference(resolution,[status(thm)],[c_106,c_149]) ).
tff(c_10,plain,
! [E_7: event] :
( diplomaticEvent(E_7)
| ~ armistice(E_7) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_40,plain,
eventOccursAt(armistice1918,rethondesCompiegne),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_16,plain,
subRegions(picardy,rethondesCompiegne),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_124,plain,
! [Z_33: event,Y_34: geographicalRegion,X_35: geographicalRegion] :
( eventOccursAt(Z_33,Y_34)
| ~ subRegions(Y_34,X_35)
| ~ eventOccursAt(Z_33,X_35) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_136,plain,
! [Z_38: event] :
( eventOccursAt(Z_38,picardy)
| ~ eventOccursAt(Z_38,rethondesCompiegne) ),
inference(resolution,[status(thm)],[c_16,c_124]) ).
tff(c_148,plain,
eventOccursAt(armistice1918,picardy),
inference(resolution,[status(thm)],[c_40,c_136]) ).
tff(c_18,plain,
subRegions(hautsDeFrance,picardy),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_131,plain,
! [Z_33: event] :
( eventOccursAt(Z_33,hautsDeFrance)
| ~ eventOccursAt(Z_33,picardy) ),
inference(resolution,[status(thm)],[c_18,c_124]) ).
tff(c_167,plain,
eventOccursAt(armistice1918,hautsDeFrance),
inference(resolution,[status(thm)],[c_148,c_131]) ).
tff(c_96,plain,
eventOccursAt(compiegneVisit2018,rethondesCompiegne),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_147,plain,
eventOccursAt(compiegneVisit2018,picardy),
inference(resolution,[status(thm)],[c_96,c_136]) ).
tff(c_163,plain,
eventOccursAt(compiegneVisit2018,hautsDeFrance),
inference(resolution,[status(thm)],[c_147,c_131]) ).
tff(c_220,plain,
! [VE_51: event,DE_52: event,LOC_53: geographicalRegion] :
( pastColocatedDiplomaticEvent(VE_51,DE_52)
| ~ endsBeforeStartOf(DE_52,VE_51)
| ~ eventOccursAt(VE_51,LOC_53)
| ~ eventOccursAt(DE_52,LOC_53)
| ~ diplomaticEvent(DE_52) ),
inference(cnfTransformation,[status(thm)],[f_138]) ).
tff(c_250,plain,
! [DE_52: event] :
( pastColocatedDiplomaticEvent(compiegneVisit2018,DE_52)
| ~ endsBeforeStartOf(DE_52,compiegneVisit2018)
| ~ eventOccursAt(DE_52,hautsDeFrance)
| ~ diplomaticEvent(DE_52) ),
inference(resolution,[status(thm)],[c_163,c_220]) ).
tff(c_42,plain,
govtRepresentedBy(armistice1918,thirdRepublicFrench,foch),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_34,plain,
narrativeSuccessor(marianne,thirdRepublicFrench,fourthRepublicFrench),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_36,plain,
narrativeSuccessor(marianne,fourthRepublicFrench,fifthRepublicFrench),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_329,plain,
! [PR_70: govt] :
( narrativeSuccessor(marianne,PR_70,fifthRepublicFrench)
| ~ narrativeSuccessor(marianne,PR_70,fourthRepublicFrench) ),
inference(resolution,[status(thm)],[c_36,c_190]) ).
tff(c_337,plain,
narrativeSuccessor(marianne,thirdRepublicFrench,fifthRepublicFrench),
inference(resolution,[status(thm)],[c_34,c_329]) ).
tff(c_100,plain,
friendlyEvent(compiegneVisit2018),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_104,plain,
govtRepresentedBy(compiegneVisit2018,fifthRepublicFrench,macron),
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_286,plain,
! [CC_65: constrCont,GOVT_62: govt,SE_66: event,VE_63: event,TS_59: table_side,DE_60: event,P_64: person,RP_61: person,PASTGOVT_58: govt] :
( avoidTableSide(P_64,VE_63,TS_59)
| ~ govtRepresentedBy(VE_63,GOVT_62,P_64)
| ~ friendlyEvent(VE_63)
| ~ narrativeSuccessor(CC_65,PASTGOVT_58,GOVT_62)
| ~ govtRepresentedBy(DE_60,PASTGOVT_58,RP_61)
| ~ seatedAtSide(SE_66,TS_59)
| ~ performedBy(SE_66,RP_61)
| ~ seatingEvent(SE_66)
| ~ subEvents(DE_60,SE_66)
| ~ contentiousEvent(DE_60)
| ~ pastColocatedDiplomaticEvent(VE_63,DE_60) ),
inference(cnfTransformation,[status(thm)],[f_160]) ).
tff(c_294,plain,
! [CC_65: constrCont,SE_66: event,TS_59: table_side,DE_60: event,RP_61: person,PASTGOVT_58: govt] :
( avoidTableSide(macron,compiegneVisit2018,TS_59)
| ~ friendlyEvent(compiegneVisit2018)
| ~ narrativeSuccessor(CC_65,PASTGOVT_58,fifthRepublicFrench)
| ~ govtRepresentedBy(DE_60,PASTGOVT_58,RP_61)
| ~ seatedAtSide(SE_66,TS_59)
| ~ performedBy(SE_66,RP_61)
| ~ seatingEvent(SE_66)
| ~ subEvents(DE_60,SE_66)
| ~ contentiousEvent(DE_60)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,DE_60) ),
inference(resolution,[status(thm)],[c_104,c_286]) ).
tff(c_631,plain,
! [SE_112: event,DE_111: event,TS_114: table_side,CC_113: constrCont,PASTGOVT_110: govt,RP_109: person] :
( avoidTableSide(macron,compiegneVisit2018,TS_114)
| ~ narrativeSuccessor(CC_113,PASTGOVT_110,fifthRepublicFrench)
| ~ govtRepresentedBy(DE_111,PASTGOVT_110,RP_109)
| ~ seatedAtSide(SE_112,TS_114)
| ~ performedBy(SE_112,RP_109)
| ~ seatingEvent(SE_112)
| ~ subEvents(DE_111,SE_112)
| ~ contentiousEvent(DE_111)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,DE_111) ),
inference(demodulation,[status(thm),theory(equality)],[c_100,c_294]) ).
tff(c_1009,plain,
! [TS_156: table_side,DE_157: event,RP_158: person,SE_159: event] :
( avoidTableSide(macron,compiegneVisit2018,TS_156)
| ~ govtRepresentedBy(DE_157,thirdRepublicFrench,RP_158)
| ~ seatedAtSide(SE_159,TS_156)
| ~ performedBy(SE_159,RP_158)
| ~ seatingEvent(SE_159)
| ~ subEvents(DE_157,SE_159)
| ~ contentiousEvent(DE_157)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,DE_157) ),
inference(resolution,[status(thm)],[c_337,c_631]) ).
tff(c_1014,plain,
! [TS_156: table_side,SE_159: event] :
( avoidTableSide(macron,compiegneVisit2018,TS_156)
| ~ seatedAtSide(SE_159,TS_156)
| ~ performedBy(SE_159,foch)
| ~ seatingEvent(SE_159)
| ~ subEvents(armistice1918,SE_159)
| ~ contentiousEvent(armistice1918)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,armistice1918) ),
inference(resolution,[status(thm)],[c_42,c_1009]) ).
tff(c_1016,plain,
~ pastColocatedDiplomaticEvent(compiegneVisit2018,armistice1918),
inference(splitLeft,[status(thm)],[c_1014]) ).
tff(c_1045,plain,
( ~ endsBeforeStartOf(armistice1918,compiegneVisit2018)
| ~ eventOccursAt(armistice1918,hautsDeFrance)
| ~ diplomaticEvent(armistice1918) ),
inference(resolution,[status(thm)],[c_250,c_1016]) ).
tff(c_1057,plain,
( ~ endsBeforeStartOf(armistice1918,compiegneVisit2018)
| ~ diplomaticEvent(armistice1918) ),
inference(demodulation,[status(thm),theory(equality)],[c_167,c_1045]) ).
tff(c_1064,plain,
~ diplomaticEvent(armistice1918),
inference(splitLeft,[status(thm)],[c_1057]) ).
tff(c_1067,plain,
~ armistice(armistice1918),
inference(resolution,[status(thm)],[c_10,c_1064]) ).
tff(c_1071,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_38,c_1067]) ).
tff(c_1072,plain,
~ endsBeforeStartOf(armistice1918,compiegneVisit2018),
inference(splitRight,[status(thm)],[c_1057]) ).
tff(c_1122,plain,
~ endsBeforeStartOf(armistice1918,armistice1940),
inference(resolution,[status(thm)],[c_154,c_1072]) ).
tff(c_1126,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_74,c_1122]) ).
tff(c_1128,plain,
pastColocatedDiplomaticEvent(compiegneVisit2018,armistice1918),
inference(splitRight,[status(thm)],[c_1014]) ).
tff(c_44,plain,
govtRepresentedBy(armistice1918,germanEmpire,erzberger),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_30,plain,
narrativeSuccessor(germania,alliedOccupiedGermany,federalGermanRepublic),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_208,plain,
! [PR_46: govt] :
( narrativeSuccessor(germania,PR_46,federalGermanRepublic)
| ~ narrativeSuccessor(germania,PR_46,alliedOccupiedGermany) ),
inference(resolution,[status(thm)],[c_30,c_190]) ).
tff(c_102,plain,
govtRepresentedBy(compiegneVisit2018,federalGermanRepublic,merkel),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_288,plain,
! [CC_65: constrCont,SE_66: event,TS_59: table_side,DE_60: event,RP_61: person,PASTGOVT_58: govt] :
( avoidTableSide(merkel,compiegneVisit2018,TS_59)
| ~ friendlyEvent(compiegneVisit2018)
| ~ narrativeSuccessor(CC_65,PASTGOVT_58,federalGermanRepublic)
| ~ govtRepresentedBy(DE_60,PASTGOVT_58,RP_61)
| ~ seatedAtSide(SE_66,TS_59)
| ~ performedBy(SE_66,RP_61)
| ~ seatingEvent(SE_66)
| ~ subEvents(DE_60,SE_66)
| ~ contentiousEvent(DE_60)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,DE_60) ),
inference(resolution,[status(thm)],[c_102,c_286]) ).
tff(c_549,plain,
! [SE_102: event,PASTGOVT_100: govt,RP_99: person,TS_104: table_side,DE_101: event,CC_103: constrCont] :
( avoidTableSide(merkel,compiegneVisit2018,TS_104)
| ~ narrativeSuccessor(CC_103,PASTGOVT_100,federalGermanRepublic)
| ~ govtRepresentedBy(DE_101,PASTGOVT_100,RP_99)
| ~ seatedAtSide(SE_102,TS_104)
| ~ performedBy(SE_102,RP_99)
| ~ seatingEvent(SE_102)
| ~ subEvents(DE_101,SE_102)
| ~ contentiousEvent(DE_101)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,DE_101) ),
inference(demodulation,[status(thm),theory(equality)],[c_100,c_288]) ).
tff(c_1163,plain,
! [RP_165: person,TS_166: table_side,DE_167: event,PR_168: govt,SE_169: event] :
( avoidTableSide(merkel,compiegneVisit2018,TS_166)
| ~ govtRepresentedBy(DE_167,PR_168,RP_165)
| ~ seatedAtSide(SE_169,TS_166)
| ~ performedBy(SE_169,RP_165)
| ~ seatingEvent(SE_169)
| ~ subEvents(DE_167,SE_169)
| ~ contentiousEvent(DE_167)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,DE_167)
| ~ narrativeSuccessor(germania,PR_168,alliedOccupiedGermany) ),
inference(resolution,[status(thm)],[c_208,c_549]) ).
tff(c_1173,plain,
! [TS_166: table_side,SE_169: event] :
( avoidTableSide(merkel,compiegneVisit2018,TS_166)
| ~ seatedAtSide(SE_169,TS_166)
| ~ performedBy(SE_169,erzberger)
| ~ seatingEvent(SE_169)
| ~ subEvents(armistice1918,SE_169)
| ~ contentiousEvent(armistice1918)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,armistice1918)
| ~ narrativeSuccessor(germania,germanEmpire,alliedOccupiedGermany) ),
inference(resolution,[status(thm)],[c_44,c_1163]) ).
tff(c_1186,plain,
! [TS_166: table_side,SE_169: event] :
( avoidTableSide(merkel,compiegneVisit2018,TS_166)
| ~ seatedAtSide(SE_169,TS_166)
| ~ performedBy(SE_169,erzberger)
| ~ seatingEvent(SE_169)
| ~ subEvents(armistice1918,SE_169)
| ~ contentiousEvent(armistice1918) ),
inference(demodulation,[status(thm),theory(equality)],[c_354,c_1128,c_1173]) ).
tff(c_1200,plain,
~ contentiousEvent(armistice1918),
inference(splitLeft,[status(thm)],[c_1186]) ).
tff(c_1203,plain,
~ armistice(armistice1918),
inference(resolution,[status(thm)],[c_8,c_1200]) ).
tff(c_1207,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_38,c_1203]) ).
tff(c_1209,plain,
contentiousEvent(armistice1918),
inference(splitRight,[status(thm)],[c_1186]) ).
tff(c_1127,plain,
! [TS_156: table_side,SE_159: event] :
( ~ contentiousEvent(armistice1918)
| avoidTableSide(macron,compiegneVisit2018,TS_156)
| ~ seatedAtSide(SE_159,TS_156)
| ~ performedBy(SE_159,foch)
| ~ seatingEvent(SE_159)
| ~ subEvents(armistice1918,SE_159) ),
inference(splitRight,[status(thm)],[c_1014]) ).
tff(c_1261,plain,
! [TS_174: table_side,SE_175: event] :
( avoidTableSide(macron,compiegneVisit2018,TS_174)
| ~ seatedAtSide(SE_175,TS_174)
| ~ performedBy(SE_175,foch)
| ~ seatingEvent(SE_175)
| ~ subEvents(armistice1918,SE_175) ),
inference(demodulation,[status(thm),theory(equality)],[c_1209,c_1127]) ).
tff(c_1265,plain,
( avoidTableSide(macron,compiegneVisit2018,cwlTableSideA)
| ~ performedBy(armistice1918AlliedSeating,foch)
| ~ seatingEvent(armistice1918AlliedSeating)
| ~ subEvents(armistice1918,armistice1918AlliedSeating) ),
inference(resolution,[status(thm)],[c_52,c_1261]) ).
tff(c_1275,plain,
avoidTableSide(macron,compiegneVisit2018,cwlTableSideA),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_46,c_50,c_1265]) ).
tff(c_1277,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_112,c_1275]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : PUZ161_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.16/0.33 % Computer : n004.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 05:01:32 EDT 2026
% 0.16/0.33 % CPUTime :
% 6.01/2.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.01/2.32
% 6.01/2.32 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------