%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PUZ161_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.bd1Sts4nD7 true
% Computer : n012.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:49:58 PM UTC 2026
% Result : Theorem 0.43s 0.52s
% Output : Refutation 0.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 21
% Syntax : Number of formulae : 63 ( 35 unt; 0 typ; 0 def)
% Number of atoms : 210 ( 0 equ; 0 cnn)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 730 ( 144 ~; 127 |; 14 &; 439 @)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 8 avg)
% Number of types : 7 ( 6 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 27 ( 26 usr; 13 con; 0-3 aty)
% Number of variables : 112 ( 0 ^; 112 !; 0 ?; 112 :)
% Comments :
%------------------------------------------------------------------------------
thf(constrCont_type,type,
constrCont: $tType ).
thf(govt_type,type,
govt: $tType ).
thf(event_type,type,
event: $tType ).
thf(person_type,type,
person: $tType ).
thf(geographicalRegion_type,type,
geographicalRegion: $tType ).
thf(table_side_type,type,
table_side: $tType ).
thf(armistice_type,type,
armistice: event > $o ).
thf(seatedAtSide_type,type,
seatedAtSide: event > table_side > $o ).
thf(subEvents_type,type,
subEvents: event > event > $o ).
thf(macron_type,type,
macron: person ).
thf(govtRepresentedBy_type,type,
govtRepresentedBy: event > govt > person > $o ).
thf(foch_type,type,
foch: person ).
thf(narrativeSuccessor_type,type,
narrativeSuccessor: constrCont > govt > govt > $o ).
thf(eventOccursAt_type,type,
eventOccursAt: event > geographicalRegion > $o ).
thf(rethondesCompiegne_type,type,
rethondesCompiegne: geographicalRegion ).
thf(performedBy_type,type,
performedBy: event > person > $o ).
thf(diplomaticEvent_type,type,
diplomaticEvent: event > $o ).
thf(contentiousEvent_type,type,
contentiousEvent: event > $o ).
thf(cwlTableSideA_type,type,
cwlTableSideA: table_side ).
thf(armistice1918AlliedSeating_type,type,
armistice1918AlliedSeating: event ).
thf(marianne_type,type,
marianne: constrCont ).
thf(armistice1940_type,type,
armistice1940: event ).
thf(endsBeforeStartOf_type,type,
endsBeforeStartOf: event > event > $o ).
thf(seatingEvent_type,type,
seatingEvent: event > $o ).
thf(fifthRepublicFrench_type,type,
fifthRepublicFrench: govt ).
thf(friendlyEvent_type,type,
friendlyEvent: event > $o ).
thf(armistice1918_type,type,
armistice1918: event ).
thf(compiegneVisit2018_type,type,
compiegneVisit2018: event ).
thf(thirdRepublicFrench_type,type,
thirdRepublicFrench: govt ).
thf(pastColocatedDiplomaticEvent_type,type,
pastColocatedDiplomaticEvent: event > event > $o ).
thf(avoidTableSide_type,type,
avoidTableSide: person > event > table_side > $o ).
thf(fourthRepublicFrench_type,type,
fourthRepublicFrench: govt ).
thf(marianne_03,axiom,
narrativeSuccessor @ marianne @ fourthRepublicFrench @ fifthRepublicFrench ).
thf(zip_derived_cl17,plain,
narrativeSuccessor @ marianne @ fourthRepublicFrench @ fifthRepublicFrench,
inference(cnf,[status(esa)],[marianne_03]) ).
thf(marianne_02,axiom,
narrativeSuccessor @ marianne @ thirdRepublicFrench @ fourthRepublicFrench ).
thf(zip_derived_cl16,plain,
narrativeSuccessor @ marianne @ thirdRepublicFrench @ fourthRepublicFrench,
inference(cnf,[status(esa)],[marianne_02]) ).
thf(narrativeSuccessor_ax,axiom,
! [CC: constrCont,PR: govt,LT: govt,BW: govt] :
( ( ( narrativeSuccessor @ CC @ PR @ BW )
& ( narrativeSuccessor @ CC @ BW @ LT ) )
=> ( narrativeSuccessor @ CC @ PR @ LT ) ) ).
thf(zip_derived_cl10,plain,
! [X0: constrCont,X1: govt,X2: govt,X3: govt] :
( ( narrativeSuccessor @ X0 @ X1 @ X2 )
| ~ ( narrativeSuccessor @ X0 @ X1 @ X3 )
| ~ ( narrativeSuccessor @ X0 @ X3 @ X2 ) ),
inference(cnf,[status(esa)],[narrativeSuccessor_ax]) ).
thf(zip_derived_cl119,plain,
! [X0: govt] :
( ( narrativeSuccessor @ marianne @ thirdRepublicFrench @ X0 )
| ~ ( narrativeSuccessor @ marianne @ fourthRepublicFrench @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl16,zip_derived_cl10]) ).
thf(zip_derived_cl161,plain,
narrativeSuccessor @ marianne @ thirdRepublicFrench @ fifthRepublicFrench,
inference('s_sup-',[status(thm)],[zip_derived_cl17,zip_derived_cl119]) ).
thf(compiegneVisit2018_macron,axiom,
govtRepresentedBy @ compiegneVisit2018 @ fifthRepublicFrench @ macron ).
thf(zip_derived_cl51,plain,
govtRepresentedBy @ compiegneVisit2018 @ fifthRepublicFrench @ macron,
inference(cnf,[status(esa)],[compiegneVisit2018_macron]) ).
thf(compiegneVisit2018_where,axiom,
eventOccursAt @ compiegneVisit2018 @ rethondesCompiegne ).
thf(zip_derived_cl47,plain,
eventOccursAt @ compiegneVisit2018 @ rethondesCompiegne,
inference(cnf,[status(esa)],[compiegneVisit2018_where]) ).
thf(armistice1918_AS_ax3,axiom,
seatedAtSide @ armistice1918AlliedSeating @ cwlTableSideA ).
thf(zip_derived_cl25,plain,
seatedAtSide @ armistice1918AlliedSeating @ cwlTableSideA,
inference(cnf,[status(esa)],[armistice1918_AS_ax3]) ).
thf(armistice1918_AS_ax2,axiom,
performedBy @ armistice1918AlliedSeating @ foch ).
thf(zip_derived_cl24,plain,
performedBy @ armistice1918AlliedSeating @ foch,
inference(cnf,[status(esa)],[armistice1918_AS_ax2]) ).
thf(armistice1918_AS_ax0,axiom,
seatingEvent @ armistice1918AlliedSeating ).
thf(zip_derived_cl22,plain,
seatingEvent @ armistice1918AlliedSeating,
inference(cnf,[status(esa)],[armistice1918_AS_ax0]) ).
thf(armistice1918_AS_ax1,axiom,
subEvents @ armistice1918 @ armistice1918AlliedSeating ).
thf(zip_derived_cl23,plain,
subEvents @ armistice1918 @ armistice1918AlliedSeating,
inference(cnf,[status(esa)],[armistice1918_AS_ax1]) ).
thf(armisticesAreContentious,axiom,
! [E: event] :
( ( armistice @ E )
=> ( contentiousEvent @ E ) ) ).
thf(zip_derived_cl3,plain,
! [X0: event] :
( ( contentiousEvent @ X0 )
| ~ ( armistice @ X0 ) ),
inference(cnf,[status(esa)],[armisticesAreContentious]) ).
thf(compiegneVisit2018_friendly,axiom,
friendlyEvent @ compiegneVisit2018 ).
thf(zip_derived_cl49,plain,
friendlyEvent @ compiegneVisit2018,
inference(cnf,[status(esa)],[compiegneVisit2018_friendly]) ).
thf(armisticesAreDiplomatic,axiom,
! [E: event] :
( ( armistice @ E )
=> ( diplomaticEvent @ E ) ) ).
thf(zip_derived_cl4,plain,
! [X0: event] :
( ( diplomaticEvent @ X0 )
| ~ ( armistice @ X0 ) ),
inference(cnf,[status(esa)],[armisticesAreDiplomatic]) ).
thf(pastColocatedDiplomaticEvent_rule,axiom,
! [DE: event,VE: event,LOC: geographicalRegion] :
( ( ( diplomaticEvent @ DE )
& ( eventOccursAt @ DE @ LOC )
& ( eventOccursAt @ VE @ LOC )
& ( endsBeforeStartOf @ DE @ VE ) )
=> ( pastColocatedDiplomaticEvent @ VE @ DE ) ) ).
thf(zip_derived_cl53,plain,
! [X0: event,X1: event,X2: geographicalRegion] :
( ( pastColocatedDiplomaticEvent @ X0 @ X1 )
| ~ ( endsBeforeStartOf @ X1 @ X0 )
| ~ ( diplomaticEvent @ X1 )
| ~ ( eventOccursAt @ X1 @ X2 )
| ~ ( eventOccursAt @ X0 @ X2 ) ),
inference(cnf,[status(esa)],[pastColocatedDiplomaticEvent_rule]) ).
thf(dontSitWherePastConflictSat,axiom,
! [P: person,RP: person,PASTGOVT: govt,GOVT: govt,CC: constrCont,VE: event,DE: event,SE: event,TS: table_side] :
( ( ( pastColocatedDiplomaticEvent @ VE @ DE )
& ( contentiousEvent @ DE )
& ( subEvents @ DE @ SE )
& ( seatingEvent @ SE )
& ( performedBy @ SE @ RP )
& ( seatedAtSide @ SE @ TS )
& ( govtRepresentedBy @ DE @ PASTGOVT @ RP )
& ( narrativeSuccessor @ CC @ PASTGOVT @ GOVT )
& ( friendlyEvent @ VE )
& ( govtRepresentedBy @ VE @ GOVT @ P ) )
=> ( avoidTableSide @ P @ VE @ TS ) ) ).
thf(zip_derived_cl54,plain,
! [X0: event,X1: govt,X2: person,X3: constrCont,X4: govt,X5: event,X6: person,X7: event,X8: table_side] :
( ~ ( govtRepresentedBy @ X0 @ X1 @ X2 )
| ~ ( friendlyEvent @ X0 )
| ~ ( narrativeSuccessor @ X3 @ X4 @ X1 )
| ~ ( govtRepresentedBy @ X5 @ X4 @ X6 )
| ~ ( performedBy @ X7 @ X6 )
| ~ ( seatingEvent @ X7 )
| ~ ( subEvents @ X5 @ X7 )
| ~ ( contentiousEvent @ X5 )
| ~ ( pastColocatedDiplomaticEvent @ X0 @ X5 )
| ~ ( seatedAtSide @ X7 @ X8 )
| ( avoidTableSide @ X2 @ X0 @ X8 ) ),
inference(cnf,[status(esa)],[dontSitWherePastConflictSat]) ).
thf(whereShouldMacronSit,conjecture,
avoidTableSide @ macron @ compiegneVisit2018 @ cwlTableSideA ).
thf(zf_stmt_0,negated_conjecture,
~ ( avoidTableSide @ macron @ compiegneVisit2018 @ cwlTableSideA ),
inference('cnf.neg',[status(esa)],[whereShouldMacronSit]) ).
thf(zip_derived_cl55,plain,
~ ( avoidTableSide @ macron @ compiegneVisit2018 @ cwlTableSideA ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl56,plain,
! [X0: event,X1: event,X2: person,X3: govt,X4: govt,X5: constrCont] :
( ~ ( seatedAtSide @ X0 @ cwlTableSideA )
| ~ ( pastColocatedDiplomaticEvent @ compiegneVisit2018 @ X1 )
| ~ ( contentiousEvent @ X1 )
| ~ ( subEvents @ X1 @ X0 )
| ~ ( seatingEvent @ X0 )
| ~ ( performedBy @ X0 @ X2 )
| ~ ( govtRepresentedBy @ X1 @ X3 @ X2 )
| ~ ( narrativeSuccessor @ X5 @ X3 @ X4 )
| ~ ( friendlyEvent @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X4 @ macron ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl54,zip_derived_cl55]) ).
thf(zip_derived_cl57,plain,
! [X0: govt,X1: govt,X2: constrCont,X3: person,X4: event,X5: event,X6: geographicalRegion] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X6 )
| ~ ( eventOccursAt @ X4 @ X6 )
| ~ ( diplomaticEvent @ X4 )
| ~ ( endsBeforeStartOf @ X4 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X0 @ macron )
| ~ ( friendlyEvent @ compiegneVisit2018 )
| ~ ( narrativeSuccessor @ X2 @ X1 @ X0 )
| ~ ( govtRepresentedBy @ X4 @ X1 @ X3 )
| ~ ( performedBy @ X5 @ X3 )
| ~ ( seatingEvent @ X5 )
| ~ ( subEvents @ X4 @ X5 )
| ~ ( contentiousEvent @ X4 )
| ~ ( seatedAtSide @ X5 @ cwlTableSideA ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl53,zip_derived_cl56]) ).
thf(zip_derived_cl58,plain,
! [X0: event,X1: event,X2: person,X3: govt,X4: govt,X5: constrCont,X6: geographicalRegion] :
( ~ ( armistice @ X1 )
| ~ ( seatedAtSide @ X0 @ cwlTableSideA )
| ~ ( contentiousEvent @ X1 )
| ~ ( subEvents @ X1 @ X0 )
| ~ ( seatingEvent @ X0 )
| ~ ( performedBy @ X0 @ X2 )
| ~ ( govtRepresentedBy @ X1 @ X3 @ X2 )
| ~ ( narrativeSuccessor @ X5 @ X3 @ X4 )
| ~ ( friendlyEvent @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X4 @ macron )
| ~ ( endsBeforeStartOf @ X1 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ X1 @ X6 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X6 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl4,zip_derived_cl57]) ).
thf(zip_derived_cl66,plain,
! [X0: geographicalRegion,X1: event,X2: govt,X3: govt,X4: constrCont,X5: person,X6: event] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X0 )
| ~ ( eventOccursAt @ X1 @ X0 )
| ~ ( endsBeforeStartOf @ X1 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X2 @ macron )
| ~ ( narrativeSuccessor @ X4 @ X3 @ X2 )
| ~ ( govtRepresentedBy @ X1 @ X3 @ X5 )
| ~ ( performedBy @ X6 @ X5 )
| ~ ( seatingEvent @ X6 )
| ~ ( subEvents @ X1 @ X6 )
| ~ ( contentiousEvent @ X1 )
| ~ ( seatedAtSide @ X6 @ cwlTableSideA )
| ~ ( armistice @ X1 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl49,zip_derived_cl58]) ).
thf(zip_derived_cl74,plain,
! [X0: event,X1: event,X2: person,X3: govt,X4: govt,X5: constrCont,X6: geographicalRegion] :
( ~ ( armistice @ X0 )
| ~ ( armistice @ X0 )
| ~ ( seatedAtSide @ X1 @ cwlTableSideA )
| ~ ( subEvents @ X0 @ X1 )
| ~ ( seatingEvent @ X1 )
| ~ ( performedBy @ X1 @ X2 )
| ~ ( govtRepresentedBy @ X0 @ X3 @ X2 )
| ~ ( narrativeSuccessor @ X5 @ X3 @ X4 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X4 @ macron )
| ~ ( endsBeforeStartOf @ X0 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ X0 @ X6 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X6 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl3,zip_derived_cl66]) ).
thf(zip_derived_cl84,plain,
! [X0: geographicalRegion,X1: govt,X2: govt,X3: constrCont,X4: person] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X0 )
| ~ ( eventOccursAt @ armistice1918 @ X0 )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ macron )
| ~ ( narrativeSuccessor @ X3 @ X2 @ X1 )
| ~ ( govtRepresentedBy @ armistice1918 @ X2 @ X4 )
| ~ ( performedBy @ armistice1918AlliedSeating @ X4 )
| ~ ( seatingEvent @ armistice1918AlliedSeating )
| ~ ( seatedAtSide @ armistice1918AlliedSeating @ cwlTableSideA )
| ~ ( armistice @ armistice1918 )
| ~ ( armistice @ armistice1918 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl23,zip_derived_cl74]) ).
thf(zip_derived_cl88,plain,
! [X0: person,X1: govt,X2: govt,X3: constrCont,X4: geographicalRegion] :
( ~ ( armistice @ armistice1918 )
| ~ ( armistice @ armistice1918 )
| ~ ( seatedAtSide @ armistice1918AlliedSeating @ cwlTableSideA )
| ~ ( performedBy @ armistice1918AlliedSeating @ X0 )
| ~ ( govtRepresentedBy @ armistice1918 @ X1 @ X0 )
| ~ ( narrativeSuccessor @ X3 @ X1 @ X2 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X2 @ macron )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ armistice1918 @ X4 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X4 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl22,zip_derived_cl84]) ).
thf(zip_derived_cl92,plain,
! [X0: geographicalRegion,X1: govt,X2: govt,X3: constrCont] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X0 )
| ~ ( eventOccursAt @ armistice1918 @ X0 )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ macron )
| ~ ( narrativeSuccessor @ X3 @ X2 @ X1 )
| ~ ( govtRepresentedBy @ armistice1918 @ X2 @ foch )
| ~ ( seatedAtSide @ armistice1918AlliedSeating @ cwlTableSideA )
| ~ ( armistice @ armistice1918 )
| ~ ( armistice @ armistice1918 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl24,zip_derived_cl88]) ).
thf(zip_derived_cl96,plain,
! [X0: govt,X1: govt,X2: constrCont,X3: geographicalRegion] :
( ~ ( armistice @ armistice1918 )
| ~ ( armistice @ armistice1918 )
| ~ ( govtRepresentedBy @ armistice1918 @ X0 @ foch )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ macron )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ armistice1918 @ X3 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X3 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl25,zip_derived_cl92]) ).
thf(zip_derived_cl123,plain,
! [X0: govt,X1: govt,X2: constrCont,X3: geographicalRegion] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X3 )
| ~ ( eventOccursAt @ armistice1918 @ X3 )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ macron )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ armistice1918 @ X0 @ foch )
| ~ ( armistice @ armistice1918 ) ),
inference(simplify,[status(thm)],[zip_derived_cl96]) ).
thf(armistice2018_past1940,axiom,
endsBeforeStartOf @ armistice1940 @ compiegneVisit2018 ).
thf(zip_derived_cl52,plain,
endsBeforeStartOf @ armistice1940 @ compiegneVisit2018,
inference(cnf,[status(esa)],[armistice2018_past1940]) ).
thf(armistice1940_past1918,axiom,
endsBeforeStartOf @ armistice1918 @ armistice1940 ).
thf(zip_derived_cl36,plain,
endsBeforeStartOf @ armistice1918 @ armistice1940,
inference(cnf,[status(esa)],[armistice1940_past1918]) ).
thf(endsBeforeStartOf_trans,axiom,
! [X: event,Y: event,Z: event] :
( ( ( endsBeforeStartOf @ X @ Y )
& ( endsBeforeStartOf @ Y @ Z ) )
=> ( endsBeforeStartOf @ X @ Z ) ) ).
thf(zip_derived_cl0,plain,
! [X0: event,X1: event,X2: event] :
( ~ ( endsBeforeStartOf @ X0 @ X1 )
| ~ ( endsBeforeStartOf @ X1 @ X2 )
| ( endsBeforeStartOf @ X0 @ X2 ) ),
inference(cnf,[status(esa)],[endsBeforeStartOf_trans]) ).
thf(zip_derived_cl109,plain,
! [X0: event] :
( ~ ( endsBeforeStartOf @ armistice1940 @ X0 )
| ( endsBeforeStartOf @ armistice1918 @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl36,zip_derived_cl0]) ).
thf(zip_derived_cl112,plain,
endsBeforeStartOf @ armistice1918 @ compiegneVisit2018,
inference('s_sup-',[status(thm)],[zip_derived_cl52,zip_derived_cl109]) ).
thf(armistice1918_typing,axiom,
armistice @ armistice1918 ).
thf(zip_derived_cl18,plain,
armistice @ armistice1918,
inference(cnf,[status(esa)],[armistice1918_typing]) ).
thf(zip_derived_cl124,plain,
! [X0: govt,X1: govt,X2: constrCont,X3: geographicalRegion] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X3 )
| ~ ( eventOccursAt @ armistice1918 @ X3 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ macron )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ armistice1918 @ X0 @ foch ) ),
inference(demod,[status(thm)],[zip_derived_cl123,zip_derived_cl112,zip_derived_cl18]) ).
thf(zip_derived_cl126,plain,
! [X0: govt,X1: govt,X2: constrCont] :
( ~ ( eventOccursAt @ armistice1918 @ rethondesCompiegne )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X0 @ macron )
| ~ ( narrativeSuccessor @ X2 @ X1 @ X0 )
| ~ ( govtRepresentedBy @ armistice1918 @ X1 @ foch ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl47,zip_derived_cl124]) ).
thf(armistice1918_where,axiom,
eventOccursAt @ armistice1918 @ rethondesCompiegne ).
thf(zip_derived_cl19,plain,
eventOccursAt @ armistice1918 @ rethondesCompiegne,
inference(cnf,[status(esa)],[armistice1918_where]) ).
thf(zip_derived_cl128,plain,
! [X0: govt,X1: govt,X2: constrCont] :
( ~ ( govtRepresentedBy @ compiegneVisit2018 @ X0 @ macron )
| ~ ( narrativeSuccessor @ X2 @ X1 @ X0 )
| ~ ( govtRepresentedBy @ armistice1918 @ X1 @ foch ) ),
inference(demod,[status(thm)],[zip_derived_cl126,zip_derived_cl19]) ).
thf(zip_derived_cl129,plain,
! [X0: govt,X1: constrCont] :
( ~ ( narrativeSuccessor @ X1 @ X0 @ fifthRepublicFrench )
| ~ ( govtRepresentedBy @ armistice1918 @ X0 @ foch ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl51,zip_derived_cl128]) ).
thf(zip_derived_cl163,plain,
~ ( govtRepresentedBy @ armistice1918 @ thirdRepublicFrench @ foch ),
inference('s_sup-',[status(thm)],[zip_derived_cl161,zip_derived_cl129]) ).
thf(armistice1918_french,axiom,
govtRepresentedBy @ armistice1918 @ thirdRepublicFrench @ foch ).
thf(zip_derived_cl20,plain,
govtRepresentedBy @ armistice1918 @ thirdRepublicFrench @ foch,
inference(cnf,[status(esa)],[armistice1918_french]) ).
thf(zip_derived_cl166,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl163,zip_derived_cl20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : PUZ161_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.07 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.bd1Sts4nD7 true
% 0.08/0.25 % Computer : n012.cluster.edu
% 0.08/0.25 % Model : x86_64 x86_64
% 0.08/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.25 % Memory : 8042.1875MB
% 0.08/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.25 % CPULimit : 300
% 0.08/0.25 % WCLimit : 300
% 0.08/0.25 % DateTime : Tue May 5 05:02:15 EDT 2026
% 0.08/0.25 % CPUTime :
% 0.08/0.25 % Running portfolio for 300 s
% 0.08/0.25 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.25 % Number of cores: 8
% 0.08/0.25 % Python version: Python 3.6.8
% 0.08/0.25 % Running in FO mode
% 0.16/0.40 % Total configuration time : 435
% 0.16/0.40 % Estimated wc time : 1092
% 0.16/0.40 % Estimated cpu time (7 cpus) : 156.0
% 0.43/0.46 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.43/0.46 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.43/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.43/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.43/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.43/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.43/0.48 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.43/0.50 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 0.43/0.50 % /export/starexec/sandbox2/solver/bin/fo/fo17_bce.sh running for 50s
% 0.43/0.51 % /export/starexec/sandbox2/solver/bin/fo/fo8.sh running for 50s
% 0.43/0.52 % Solved by fo/fo6_bce.sh.
% 0.43/0.52 % BCE start: 56
% 0.43/0.52 % BCE eliminated: 4
% 0.43/0.52 % PE start: 52
% 0.43/0.52 logic: neq
% 0.43/0.52 % PE eliminated: 21
% 0.43/0.52 % done 63 iterations in 0.040s
% 0.43/0.52 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.43/0.52 % SZS output start Refutation
% See solution above
% 0.43/0.53
% 0.43/0.53
% 0.43/0.53 % Terminating...
% 0.32/300.02 Terminated
% 0.32/300.02 % Zipperpin 1.5 exiting
% 0.32/300.02 /usr/lib64/python3.6/multiprocessing/semaphore_tracker.py:143: UserWarning: semaphore_tracker: There appear to be 4 leaked semaphores to clean up at shutdown
% 0.32/300.02 len(cache))
%------------------------------------------------------------------------------