%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PUZ162_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 : n018.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.94s 2.43s
% Output : CNFRefutation 5.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 22
% Syntax : Number of formulae : 70 ( 46 unt; 0 typ; 0 def)
% Number of atoms : 160 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 168 ( 78 ~; 70 |; 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 : 68 ( 68 !; 0 ?; 68 :)
% 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,cwlTableSideC),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',whereShouldMacronSit) ).
tff(f_118,axiom,
subEvents(armistice1940,armistice1940FrenchSeating),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1940_FS_ax1) ).
tff(f_117,axiom,
seatingEvent(armistice1940FrenchSeating),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1940_FS_ax0) ).
tff(f_119,axiom,
performedBy(armistice1940FrenchSeating,hutzinger),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1940_FS_ax2) ).
tff(f_120,axiom,
seatedAtSide(armistice1940FrenchSeating,cwlTableSideC),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1940_FS_ax3) ).
tff(f_107,axiom,
armistice(armistice1940),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1940_typing) ).
tff(f_53,axiom,
! [E: event] :
( armistice(E)
=> contentiousEvent(E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armisticesAreContentious) ).
tff(f_57,axiom,
! [E: event] :
( armistice(E)
=> diplomaticEvent(E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armisticesAreDiplomatic) ).
tff(f_108,axiom,
eventOccursAt(armistice1940,rethondesCompiegne),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1940_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_128,axiom,
endsBeforeStartOf(armistice1940,compiegneVisit2018),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice2018_past1940) ).
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_109,axiom,
govtRepresentedBy(armistice1940,thirdRepublicFrench,hutzinger),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',armistice1940_hutzinger) ).
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_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_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(c_112,plain,
~ avoidTableSide(macron,compiegneVisit2018,cwlTableSideC),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_88,plain,
subEvents(armistice1940,armistice1940FrenchSeating),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_86,plain,
seatingEvent(armistice1940FrenchSeating),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_90,plain,
performedBy(armistice1940FrenchSeating,hutzinger),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_92,plain,
seatedAtSide(armistice1940FrenchSeating,cwlTableSideC),
inference(cnfTransformation,[status(thm)],[f_120]) ).
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_1210,plain,
! [TS_170: table_side,SE_171: event] :
( avoidTableSide(macron,compiegneVisit2018,TS_170)
| ~ seatedAtSide(SE_171,TS_170)
| ~ performedBy(SE_171,hutzinger)
| ~ seatingEvent(SE_171)
| ~ subEvents(armistice1940,SE_171) ),
inference(splitRight,[status(thm)],[c_1161]) ).
tff(c_1216,plain,
( avoidTableSide(macron,compiegneVisit2018,cwlTableSideC)
| ~ performedBy(armistice1940FrenchSeating,hutzinger)
| ~ seatingEvent(armistice1940FrenchSeating)
| ~ subEvents(armistice1940,armistice1940FrenchSeating) ),
inference(resolution,[status(thm)],[c_92,c_1210]) ).
tff(c_1228,plain,
avoidTableSide(macron,compiegneVisit2018,cwlTableSideC),
inference(demodulation,[status(thm),theory(equality)],[c_88,c_86,c_90,c_1216]) ).
tff(c_1230,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_112,c_1228]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.28 % Problem : PUZ162_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.29 % 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.15/0.49 % Computer : n018.cluster.edu
% 0.15/0.49 % Model : x86_64 x86_64
% 0.15/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.49 % Memory : 8042.1875MB
% 0.15/0.49 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.49 % CPULimit : 300
% 0.15/0.49 % WCLimit : 300
% 0.15/0.49 % DateTime : Tue May 5 05:02:32 EDT 2026
% 0.15/0.49 % CPUTime :
% 5.94/2.43 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.94/2.44
% 5.94/2.44 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------