%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PUZ160_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.zHdZDqqjsb true
% Computer : n026.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.52s 0.74s
% Output : Refutation 0.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 23
% Syntax : Number of formulae : 73 ( 41 unt; 0 typ; 0 def)
% Number of atoms : 226 ( 0 equ; 0 cnn)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 790 ( 150 ~; 133 |; 14 &; 487 @)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 7 avg)
% Number of types : 7 ( 6 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 28 usr; 15 con; 0-3 aty)
% Number of variables : 122 ( 0 ^; 122 !; 0 ?; 122 :)
% 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(germania_type,type,
germania: constrCont ).
thf(seatedAtSide_type,type,
seatedAtSide: event > table_side > $o ).
thf(erzberger_type,type,
erzberger: person ).
thf(subEvents_type,type,
subEvents: event > event > $o ).
thf(govtRepresentedBy_type,type,
govtRepresentedBy: event > govt > person > $o ).
thf(germanEmpire_type,type,
germanEmpire: govt ).
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(weimarRepublic_type,type,
weimarRepublic: govt ).
thf(diplomaticEvent_type,type,
diplomaticEvent: event > $o ).
thf(contentiousEvent_type,type,
contentiousEvent: event > $o ).
thf(federalGermanRepublic_type,type,
federalGermanRepublic: govt ).
thf(armistice1940_type,type,
armistice1940: event ).
thf(armistice1918GermanSeating_type,type,
armistice1918GermanSeating: event ).
thf(endsBeforeStartOf_type,type,
endsBeforeStartOf: event > event > $o ).
thf(seatingEvent_type,type,
seatingEvent: event > $o ).
thf(friendlyEvent_type,type,
friendlyEvent: event > $o ).
thf(armistice1918_type,type,
armistice1918: event ).
thf(compiegneVisit2018_type,type,
compiegneVisit2018: event ).
thf(cwlTableSideC_type,type,
cwlTableSideC: table_side ).
thf(merkel_type,type,
merkel: person ).
thf(thirdReich_type,type,
thirdReich: govt ).
thf(pastColocatedDiplomaticEvent_type,type,
pastColocatedDiplomaticEvent: event > event > $o ).
thf(avoidTableSide_type,type,
avoidTableSide: person > event > table_side > $o ).
thf(alliedOccupiedGermany_type,type,
alliedOccupiedGermany: govt ).
thf(germania_04,axiom,
narrativeSuccessor @ germania @ alliedOccupiedGermany @ federalGermanRepublic ).
thf(zip_derived_cl14,plain,
narrativeSuccessor @ germania @ alliedOccupiedGermany @ federalGermanRepublic,
inference(cnf,[status(esa)],[germania_04]) ).
thf(germania_03,axiom,
narrativeSuccessor @ germania @ thirdReich @ alliedOccupiedGermany ).
thf(zip_derived_cl13,plain,
narrativeSuccessor @ germania @ thirdReich @ alliedOccupiedGermany,
inference(cnf,[status(esa)],[germania_03]) ).
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_cl116,plain,
! [X0: govt] :
( ( narrativeSuccessor @ germania @ thirdReich @ X0 )
| ~ ( narrativeSuccessor @ germania @ alliedOccupiedGermany @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl13,zip_derived_cl10]) ).
thf(zip_derived_cl152,plain,
narrativeSuccessor @ germania @ thirdReich @ federalGermanRepublic,
inference('s_sup-',[status(thm)],[zip_derived_cl14,zip_derived_cl116]) ).
thf(germania_02,axiom,
narrativeSuccessor @ germania @ weimarRepublic @ thirdReich ).
thf(zip_derived_cl12,plain,
narrativeSuccessor @ germania @ weimarRepublic @ thirdReich,
inference(cnf,[status(esa)],[germania_02]) ).
thf(zip_derived_cl10_001,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_cl115,plain,
! [X0: govt] :
( ( narrativeSuccessor @ germania @ weimarRepublic @ X0 )
| ~ ( narrativeSuccessor @ germania @ thirdReich @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl12,zip_derived_cl10]) ).
thf(zip_derived_cl157,plain,
narrativeSuccessor @ germania @ weimarRepublic @ federalGermanRepublic,
inference('s_sup-',[status(thm)],[zip_derived_cl152,zip_derived_cl115]) ).
thf(germania_01,axiom,
narrativeSuccessor @ germania @ germanEmpire @ weimarRepublic ).
thf(zip_derived_cl11,plain,
narrativeSuccessor @ germania @ germanEmpire @ weimarRepublic,
inference(cnf,[status(esa)],[germania_01]) ).
thf(zip_derived_cl10_002,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_cl114,plain,
! [X0: govt] :
( ( narrativeSuccessor @ germania @ germanEmpire @ X0 )
| ~ ( narrativeSuccessor @ germania @ weimarRepublic @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl11,zip_derived_cl10]) ).
thf(zip_derived_cl161,plain,
narrativeSuccessor @ germania @ germanEmpire @ federalGermanRepublic,
inference('s_sup-',[status(thm)],[zip_derived_cl157,zip_derived_cl114]) ).
thf(compiegneVisit2018_merkel,axiom,
govtRepresentedBy @ compiegneVisit2018 @ federalGermanRepublic @ merkel ).
thf(zip_derived_cl50,plain,
govtRepresentedBy @ compiegneVisit2018 @ federalGermanRepublic @ merkel,
inference(cnf,[status(esa)],[compiegneVisit2018_merkel]) ).
thf(compiegneVisit2018_where,axiom,
eventOccursAt @ compiegneVisit2018 @ rethondesCompiegne ).
thf(zip_derived_cl47,plain,
eventOccursAt @ compiegneVisit2018 @ rethondesCompiegne,
inference(cnf,[status(esa)],[compiegneVisit2018_where]) ).
thf(armistice1918_GS_ax3,axiom,
seatedAtSide @ armistice1918GermanSeating @ cwlTableSideC ).
thf(zip_derived_cl30,plain,
seatedAtSide @ armistice1918GermanSeating @ cwlTableSideC,
inference(cnf,[status(esa)],[armistice1918_GS_ax3]) ).
thf(armistice1918_GS_ax2,axiom,
performedBy @ armistice1918GermanSeating @ erzberger ).
thf(zip_derived_cl29,plain,
performedBy @ armistice1918GermanSeating @ erzberger,
inference(cnf,[status(esa)],[armistice1918_GS_ax2]) ).
thf(armistice1918_GS_ax0,axiom,
seatingEvent @ armistice1918GermanSeating ).
thf(zip_derived_cl27,plain,
seatingEvent @ armistice1918GermanSeating,
inference(cnf,[status(esa)],[armistice1918_GS_ax0]) ).
thf(armistice1918_GS_ax1,axiom,
subEvents @ armistice1918 @ armistice1918GermanSeating ).
thf(zip_derived_cl28,plain,
subEvents @ armistice1918 @ armistice1918GermanSeating,
inference(cnf,[status(esa)],[armistice1918_GS_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(whereShouldMerkelSit,conjecture,
avoidTableSide @ merkel @ compiegneVisit2018 @ cwlTableSideC ).
thf(zf_stmt_0,negated_conjecture,
~ ( avoidTableSide @ merkel @ compiegneVisit2018 @ cwlTableSideC ),
inference('cnf.neg',[status(esa)],[whereShouldMerkelSit]) ).
thf(zip_derived_cl55,plain,
~ ( avoidTableSide @ merkel @ compiegneVisit2018 @ cwlTableSideC ),
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 @ cwlTableSideC )
| ~ ( 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 @ merkel ) ),
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 @ merkel )
| ~ ( friendlyEvent @ compiegneVisit2018 )
| ~ ( narrativeSuccessor @ X2 @ X1 @ X0 )
| ~ ( govtRepresentedBy @ X4 @ X1 @ X3 )
| ~ ( performedBy @ X5 @ X3 )
| ~ ( seatingEvent @ X5 )
| ~ ( subEvents @ X4 @ X5 )
| ~ ( contentiousEvent @ X4 )
| ~ ( seatedAtSide @ X5 @ cwlTableSideC ) ),
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 @ cwlTableSideC )
| ~ ( contentiousEvent @ X1 )
| ~ ( subEvents @ X1 @ X0 )
| ~ ( seatingEvent @ X0 )
| ~ ( performedBy @ X0 @ X2 )
| ~ ( govtRepresentedBy @ X1 @ X3 @ X2 )
| ~ ( narrativeSuccessor @ X5 @ X3 @ X4 )
| ~ ( friendlyEvent @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X4 @ merkel )
| ~ ( 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 @ merkel )
| ~ ( narrativeSuccessor @ X4 @ X3 @ X2 )
| ~ ( govtRepresentedBy @ X1 @ X3 @ X5 )
| ~ ( performedBy @ X6 @ X5 )
| ~ ( seatingEvent @ X6 )
| ~ ( subEvents @ X1 @ X6 )
| ~ ( contentiousEvent @ X1 )
| ~ ( seatedAtSide @ X6 @ cwlTableSideC )
| ~ ( 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 @ cwlTableSideC )
| ~ ( subEvents @ X0 @ X1 )
| ~ ( seatingEvent @ X1 )
| ~ ( performedBy @ X1 @ X2 )
| ~ ( govtRepresentedBy @ X0 @ X3 @ X2 )
| ~ ( narrativeSuccessor @ X5 @ X3 @ X4 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X4 @ merkel )
| ~ ( endsBeforeStartOf @ X0 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ X0 @ X6 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X6 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl3,zip_derived_cl66]) ).
thf(zip_derived_cl85,plain,
! [X0: geographicalRegion,X1: govt,X2: govt,X3: constrCont,X4: person] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X0 )
| ~ ( eventOccursAt @ armistice1918 @ X0 )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ merkel )
| ~ ( narrativeSuccessor @ X3 @ X2 @ X1 )
| ~ ( govtRepresentedBy @ armistice1918 @ X2 @ X4 )
| ~ ( performedBy @ armistice1918GermanSeating @ X4 )
| ~ ( seatingEvent @ armistice1918GermanSeating )
| ~ ( seatedAtSide @ armistice1918GermanSeating @ cwlTableSideC )
| ~ ( armistice @ armistice1918 )
| ~ ( armistice @ armistice1918 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl28,zip_derived_cl74]) ).
thf(zip_derived_cl89,plain,
! [X0: person,X1: govt,X2: govt,X3: constrCont,X4: geographicalRegion] :
( ~ ( armistice @ armistice1918 )
| ~ ( armistice @ armistice1918 )
| ~ ( seatedAtSide @ armistice1918GermanSeating @ cwlTableSideC )
| ~ ( performedBy @ armistice1918GermanSeating @ X0 )
| ~ ( govtRepresentedBy @ armistice1918 @ X1 @ X0 )
| ~ ( narrativeSuccessor @ X3 @ X1 @ X2 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X2 @ merkel )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ armistice1918 @ X4 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X4 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl27,zip_derived_cl85]) ).
thf(zip_derived_cl93,plain,
! [X0: geographicalRegion,X1: govt,X2: govt,X3: constrCont] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X0 )
| ~ ( eventOccursAt @ armistice1918 @ X0 )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ merkel )
| ~ ( narrativeSuccessor @ X3 @ X2 @ X1 )
| ~ ( govtRepresentedBy @ armistice1918 @ X2 @ erzberger )
| ~ ( seatedAtSide @ armistice1918GermanSeating @ cwlTableSideC )
| ~ ( armistice @ armistice1918 )
| ~ ( armistice @ armistice1918 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl29,zip_derived_cl89]) ).
thf(zip_derived_cl96,plain,
! [X0: govt,X1: govt,X2: constrCont,X3: geographicalRegion] :
( ~ ( armistice @ armistice1918 )
| ~ ( armistice @ armistice1918 )
| ~ ( govtRepresentedBy @ armistice1918 @ X0 @ erzberger )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ merkel )
| ~ ( endsBeforeStartOf @ armistice1918 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ armistice1918 @ X3 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X3 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl30,zip_derived_cl93]) ).
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 @ merkel )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ armistice1918 @ X0 @ erzberger )
| ~ ( 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 @ merkel )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ armistice1918 @ X0 @ erzberger ) ),
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 @ merkel )
| ~ ( narrativeSuccessor @ X2 @ X1 @ X0 )
| ~ ( govtRepresentedBy @ armistice1918 @ X1 @ erzberger ) ),
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 @ merkel )
| ~ ( narrativeSuccessor @ X2 @ X1 @ X0 )
| ~ ( govtRepresentedBy @ armistice1918 @ X1 @ erzberger ) ),
inference(demod,[status(thm)],[zip_derived_cl126,zip_derived_cl19]) ).
thf(zip_derived_cl129,plain,
! [X0: govt,X1: constrCont] :
( ~ ( narrativeSuccessor @ X1 @ X0 @ federalGermanRepublic )
| ~ ( govtRepresentedBy @ armistice1918 @ X0 @ erzberger ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl50,zip_derived_cl128]) ).
thf(zip_derived_cl163,plain,
~ ( govtRepresentedBy @ armistice1918 @ germanEmpire @ erzberger ),
inference('s_sup-',[status(thm)],[zip_derived_cl161,zip_derived_cl129]) ).
thf(armistice1918_german,axiom,
govtRepresentedBy @ armistice1918 @ germanEmpire @ erzberger ).
thf(zip_derived_cl21,plain,
govtRepresentedBy @ armistice1918 @ germanEmpire @ erzberger,
inference(cnf,[status(esa)],[armistice1918_german]) ).
thf(zip_derived_cl165,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl163,zip_derived_cl21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ160_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.zHdZDqqjsb true
% 0.15/0.33 % Computer : n026.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:02:23 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 % Running portfolio for 300 s
% 0.15/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Number of cores: 8
% 0.15/0.34 % Python version: Python 3.6.8
% 0.15/0.34 % Running in FO mode
% 0.52/0.63 % Total configuration time : 435
% 0.52/0.63 % Estimated wc time : 1092
% 0.52/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.52/0.68 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.52/0.74 % Solved by fo/fo6_bce.sh.
% 0.52/0.74 % BCE start: 56
% 0.52/0.74 % BCE eliminated: 4
% 0.52/0.74 % PE start: 52
% 0.52/0.74 logic: neq
% 0.52/0.74 % PE eliminated: 21
% 0.52/0.74 % done 61 iterations in 0.032s
% 0.52/0.74 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.52/0.74 % SZS output start Refutation
% See solution above
% 0.52/0.74
% 0.52/0.74
% 0.52/0.74 % Terminating...
% 0.60/300.04 Terminated
% 0.60/300.04 % Zipperpin 1.5 exiting
% 0.60/300.04 /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.60/300.04 len(cache))
%------------------------------------------------------------------------------