%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PUZ159_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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n029.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 5.96s 2.36s
% Output : CNFRefutation 6.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 26
% Syntax : Number of formulae : 86 ( 56 unt; 0 typ; 0 def)
% Number of atoms : 214 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 244 ( 116 ~; 108 |; 14 &)
% ( 0 <=>; 6 =>; 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 : 90 ( 90 !; 0 ?; 90 :)
% 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(merkel,compiegneVisit2018,cwlTableSideA),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',whereShouldMerkelSit) ).
tff(f_113,axiom,
subEvents(armistice1940,armistice1940GermanSeating),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax1) ).
tff(f_112,axiom,
seatingEvent(armistice1940GermanSeating),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax0) ).
tff(f_114,axiom,
performedBy(armistice1940GermanSeating,hitler),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax2) ).
tff(f_115,axiom,
seatedAtSide(armistice1940GermanSeating,cwlTableSideA),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_GS_ax3) ).
tff(f_107,axiom,
armistice(armistice1940),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_typing) ).
tff(f_53,axiom,
! [E: event] :
( armistice(E)
=> contentiousEvent(E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armisticesAreContentious) ).
tff(f_57,axiom,
! [E: event] :
( armistice(E)
=> diplomaticEvent(E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armisticesAreDiplomatic) ).
tff(f_108,axiom,
eventOccursAt(armistice1940,rethondesCompiegne),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_where) ).
tff(f_71,axiom,
subRegions(picardy,rethondesCompiegne),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',eventOccursAt_trans) ).
tff(f_72,axiom,
subRegions(hautsDeFrance,picardy),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',picardyInHautsDeFrance) ).
tff(f_128,axiom,
endsBeforeStartOf(armistice1940,compiegneVisit2018),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice2018_past1940) ).
tff(f_123,axiom,
eventOccursAt(compiegneVisit2018,rethondesCompiegne),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',pastColocatedDiplomaticEvent_rule) ).
tff(f_109,axiom,
govtRepresentedBy(armistice1940,thirdRepublicFrench,hutzinger),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_hutzinger) ).
tff(f_86,axiom,
narrativeSuccessor(marianne,thirdRepublicFrench,fourthRepublicFrench),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',marianne_02) ).
tff(f_87,axiom,
narrativeSuccessor(marianne,fourthRepublicFrench,fifthRepublicFrench),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',marianne_03) ).
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/sandbox/benchmark/theBenchmark.p',narrativeSuccessor_ax) ).
tff(f_125,axiom,
friendlyEvent(compiegneVisit2018),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compiegneVisit2018_friendly) ).
tff(f_127,axiom,
govtRepresentedBy(compiegneVisit2018,fifthRepublicFrench,macron),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',dontSitWherePastConflictSat) ).
tff(f_83,axiom,
narrativeSuccessor(germania,thirdReich,alliedOccupiedGermany),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',germania_03) ).
tff(f_110,axiom,
govtRepresentedBy(armistice1940,thirdReich,hitler),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',armistice1940_hitler) ).
tff(f_84,axiom,
narrativeSuccessor(germania,alliedOccupiedGermany,federalGermanRepublic),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',germania_04) ).
tff(f_126,axiom,
govtRepresentedBy(compiegneVisit2018,federalGermanRepublic,merkel),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compiegneVisit2018_merkel) ).
tff(c_112,plain,
~ avoidTableSide(merkel,compiegneVisit2018,cwlTableSideA),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_78,plain,
subEvents(armistice1940,armistice1940GermanSeating),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_76,plain,
seatingEvent(armistice1940GermanSeating),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_80,plain,
performedBy(armistice1940GermanSeating,hitler),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_82,plain,
seatedAtSide(armistice1940GermanSeating,cwlTableSideA),
inference(cnfTransformation,[status(thm)],[f_115]) ).
tff(c_66,plain,
armistice(armistice1940),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_8,plain,
! [E_6: event] :
( contentiousEvent(E_6)
| ~ armistice(E_6) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_10,plain,
! [E_7: event] :
( diplomaticEvent(E_7)
| ~ armistice(E_7) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_68,plain,
eventOccursAt(armistice1940,rethondesCompiegne),
inference(cnfTransformation,[status(thm)],[f_108]) ).
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_146,plain,
eventOccursAt(armistice1940,picardy),
inference(resolution,[status(thm)],[c_68,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_159,plain,
eventOccursAt(armistice1940,hautsDeFrance),
inference(resolution,[status(thm)],[c_146,c_131]) ).
tff(c_106,plain,
endsBeforeStartOf(armistice1940,compiegneVisit2018),
inference(cnfTransformation,[status(thm)],[f_128]) ).
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_70,plain,
govtRepresentedBy(armistice1940,thirdRepublicFrench,hutzinger),
inference(cnfTransformation,[status(thm)],[f_109]) ).
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_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_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_1015,plain,
! [TS_156: table_side,SE_159: event] :
( avoidTableSide(macron,compiegneVisit2018,TS_156)
| ~ seatedAtSide(SE_159,TS_156)
| ~ performedBy(SE_159,hutzinger)
| ~ seatingEvent(SE_159)
| ~ subEvents(armistice1940,SE_159)
| ~ contentiousEvent(armistice1940)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,armistice1940) ),
inference(resolution,[status(thm)],[c_70,c_1009]) ).
tff(c_1129,plain,
~ pastColocatedDiplomaticEvent(compiegneVisit2018,armistice1940),
inference(splitLeft,[status(thm)],[c_1015]) ).
tff(c_1135,plain,
( ~ endsBeforeStartOf(armistice1940,compiegneVisit2018)
| ~ eventOccursAt(armistice1940,hautsDeFrance)
| ~ diplomaticEvent(armistice1940) ),
inference(resolution,[status(thm)],[c_250,c_1129]) ).
tff(c_1147,plain,
~ diplomaticEvent(armistice1940),
inference(demodulation,[status(thm),theory(equality)],[c_159,c_106,c_1135]) ).
tff(c_1156,plain,
~ armistice(armistice1940),
inference(resolution,[status(thm)],[c_10,c_1147]) ).
tff(c_1160,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_66,c_1156]) ).
tff(c_1161,plain,
! [TS_156: table_side,SE_159: event] :
( ~ contentiousEvent(armistice1940)
| avoidTableSide(macron,compiegneVisit2018,TS_156)
| ~ seatedAtSide(SE_159,TS_156)
| ~ performedBy(SE_159,hutzinger)
| ~ seatingEvent(SE_159)
| ~ subEvents(armistice1940,SE_159) ),
inference(splitRight,[status(thm)],[c_1015]) ).
tff(c_1190,plain,
~ contentiousEvent(armistice1940),
inference(splitLeft,[status(thm)],[c_1161]) ).
tff(c_1193,plain,
~ armistice(armistice1940),
inference(resolution,[status(thm)],[c_8,c_1190]) ).
tff(c_1197,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_66,c_1193]) ).
tff(c_1199,plain,
contentiousEvent(armistice1940),
inference(splitRight,[status(thm)],[c_1161]) ).
tff(c_28,plain,
narrativeSuccessor(germania,thirdReich,alliedOccupiedGermany),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_1162,plain,
pastColocatedDiplomaticEvent(compiegneVisit2018,armistice1940),
inference(splitRight,[status(thm)],[c_1015]) ).
tff(c_72,plain,
govtRepresentedBy(armistice1940,thirdReich,hitler),
inference(cnfTransformation,[status(thm)],[f_110]) ).
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_1167,plain,
! [TS_166: table_side,SE_169: event] :
( avoidTableSide(merkel,compiegneVisit2018,TS_166)
| ~ seatedAtSide(SE_169,TS_166)
| ~ performedBy(SE_169,hitler)
| ~ seatingEvent(SE_169)
| ~ subEvents(armistice1940,SE_169)
| ~ contentiousEvent(armistice1940)
| ~ pastColocatedDiplomaticEvent(compiegneVisit2018,armistice1940)
| ~ narrativeSuccessor(germania,thirdReich,alliedOccupiedGermany) ),
inference(resolution,[status(thm)],[c_72,c_1163]) ).
tff(c_1179,plain,
! [TS_166: table_side,SE_169: event] :
( avoidTableSide(merkel,compiegneVisit2018,TS_166)
| ~ seatedAtSide(SE_169,TS_166)
| ~ performedBy(SE_169,hitler)
| ~ seatingEvent(SE_169)
| ~ subEvents(armistice1940,SE_169)
| ~ contentiousEvent(armistice1940) ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_1162,c_1167]) ).
tff(c_1284,plain,
! [TS_176: table_side,SE_177: event] :
( avoidTableSide(merkel,compiegneVisit2018,TS_176)
| ~ seatedAtSide(SE_177,TS_176)
| ~ performedBy(SE_177,hitler)
| ~ seatingEvent(SE_177)
| ~ subEvents(armistice1940,SE_177) ),
inference(demodulation,[status(thm),theory(equality)],[c_1199,c_1179]) ).
tff(c_1292,plain,
( avoidTableSide(merkel,compiegneVisit2018,cwlTableSideA)
| ~ performedBy(armistice1940GermanSeating,hitler)
| ~ seatingEvent(armistice1940GermanSeating)
| ~ subEvents(armistice1940,armistice1940GermanSeating) ),
inference(resolution,[status(thm)],[c_82,c_1284]) ).
tff(c_1305,plain,
avoidTableSide(merkel,compiegneVisit2018,cwlTableSideA),
inference(demodulation,[status(thm),theory(equality)],[c_78,c_76,c_80,c_1292]) ).
tff(c_1307,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_112,c_1305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ159_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.15/0.33 % Computer : n029.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 05:00:29 EDT 2026
% 0.15/0.33 % CPUTime :
% 5.96/2.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.96/2.37
% 5.96/2.37 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------