%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PUZ159_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.jW1g4ezq0r true
% Computer : n031.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.54s 0.73s
% Output : Refutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 19
% Syntax : Number of formulae : 57 ( 32 unt; 0 typ; 0 def)
% Number of atoms : 199 ( 0 equ; 0 cnn)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 700 ( 141 ~; 124 |; 13 &; 417 @)
% ( 0 <=>; 5 =>; 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 : 26 ( 25 usr; 12 con; 0-3 aty)
% Number of variables : 105 ( 0 ^; 105 !; 0 ?; 105 :)
% 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(subEvents_type,type,
subEvents: event > event > $o ).
thf(govtRepresentedBy_type,type,
govtRepresentedBy: event > govt > person > $o ).
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(federalGermanRepublic_type,type,
federalGermanRepublic: govt ).
thf(hitler_type,type,
hitler: person ).
thf(armistice1940_type,type,
armistice1940: event ).
thf(endsBeforeStartOf_type,type,
endsBeforeStartOf: event > event > $o ).
thf(seatingEvent_type,type,
seatingEvent: event > $o ).
thf(armistice1940GermanSeating_type,type,
armistice1940GermanSeating: event ).
thf(friendlyEvent_type,type,
friendlyEvent: event > $o ).
thf(compiegneVisit2018_type,type,
compiegneVisit2018: event ).
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(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(armistice1940_GS_ax3,axiom,
seatedAtSide @ armistice1940GermanSeating @ cwlTableSideA ).
thf(zip_derived_cl40,plain,
seatedAtSide @ armistice1940GermanSeating @ cwlTableSideA,
inference(cnf,[status(esa)],[armistice1940_GS_ax3]) ).
thf(armistice1940_GS_ax2,axiom,
performedBy @ armistice1940GermanSeating @ hitler ).
thf(zip_derived_cl39,plain,
performedBy @ armistice1940GermanSeating @ hitler,
inference(cnf,[status(esa)],[armistice1940_GS_ax2]) ).
thf(armistice1940_GS_ax0,axiom,
seatingEvent @ armistice1940GermanSeating ).
thf(zip_derived_cl37,plain,
seatingEvent @ armistice1940GermanSeating,
inference(cnf,[status(esa)],[armistice1940_GS_ax0]) ).
thf(armistice1940_GS_ax1,axiom,
subEvents @ armistice1940 @ armistice1940GermanSeating ).
thf(zip_derived_cl38,plain,
subEvents @ armistice1940 @ armistice1940GermanSeating,
inference(cnf,[status(esa)],[armistice1940_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 @ cwlTableSideA ).
thf(zf_stmt_0,negated_conjecture,
~ ( avoidTableSide @ merkel @ compiegneVisit2018 @ cwlTableSideA ),
inference('cnf.neg',[status(esa)],[whereShouldMerkelSit]) ).
thf(zip_derived_cl55,plain,
~ ( avoidTableSide @ merkel @ 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 @ 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 @ 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 @ 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 @ 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 @ merkel )
| ~ ( endsBeforeStartOf @ X0 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ X0 @ X6 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X6 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl3,zip_derived_cl66]) ).
thf(zip_derived_cl86,plain,
! [X0: geographicalRegion,X1: govt,X2: govt,X3: constrCont,X4: person] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X0 )
| ~ ( eventOccursAt @ armistice1940 @ X0 )
| ~ ( endsBeforeStartOf @ armistice1940 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ merkel )
| ~ ( narrativeSuccessor @ X3 @ X2 @ X1 )
| ~ ( govtRepresentedBy @ armistice1940 @ X2 @ X4 )
| ~ ( performedBy @ armistice1940GermanSeating @ X4 )
| ~ ( seatingEvent @ armistice1940GermanSeating )
| ~ ( seatedAtSide @ armistice1940GermanSeating @ cwlTableSideA )
| ~ ( armistice @ armistice1940 )
| ~ ( armistice @ armistice1940 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl38,zip_derived_cl74]) ).
thf(zip_derived_cl90,plain,
! [X0: person,X1: govt,X2: govt,X3: constrCont,X4: geographicalRegion] :
( ~ ( armistice @ armistice1940 )
| ~ ( armistice @ armistice1940 )
| ~ ( seatedAtSide @ armistice1940GermanSeating @ cwlTableSideA )
| ~ ( performedBy @ armistice1940GermanSeating @ X0 )
| ~ ( govtRepresentedBy @ armistice1940 @ X1 @ X0 )
| ~ ( narrativeSuccessor @ X3 @ X1 @ X2 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X2 @ merkel )
| ~ ( endsBeforeStartOf @ armistice1940 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ armistice1940 @ X4 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X4 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl37,zip_derived_cl86]) ).
thf(zip_derived_cl94,plain,
! [X0: geographicalRegion,X1: govt,X2: govt,X3: constrCont] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X0 )
| ~ ( eventOccursAt @ armistice1940 @ X0 )
| ~ ( endsBeforeStartOf @ armistice1940 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ merkel )
| ~ ( narrativeSuccessor @ X3 @ X2 @ X1 )
| ~ ( govtRepresentedBy @ armistice1940 @ X2 @ hitler )
| ~ ( seatedAtSide @ armistice1940GermanSeating @ cwlTableSideA )
| ~ ( armistice @ armistice1940 )
| ~ ( armistice @ armistice1940 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl39,zip_derived_cl90]) ).
thf(zip_derived_cl97,plain,
! [X0: govt,X1: govt,X2: constrCont,X3: geographicalRegion] :
( ~ ( armistice @ armistice1940 )
| ~ ( armistice @ armistice1940 )
| ~ ( govtRepresentedBy @ armistice1940 @ X0 @ hitler )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ merkel )
| ~ ( endsBeforeStartOf @ armistice1940 @ compiegneVisit2018 )
| ~ ( eventOccursAt @ armistice1940 @ X3 )
| ~ ( eventOccursAt @ compiegneVisit2018 @ X3 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl40,zip_derived_cl94]) ).
thf(zip_derived_cl132,plain,
! [X0: govt,X1: govt,X2: constrCont,X3: geographicalRegion] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X3 )
| ~ ( eventOccursAt @ armistice1940 @ X3 )
| ~ ( endsBeforeStartOf @ armistice1940 @ compiegneVisit2018 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ merkel )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ armistice1940 @ X0 @ hitler )
| ~ ( armistice @ armistice1940 ) ),
inference(simplify,[status(thm)],[zip_derived_cl97]) ).
thf(armistice2018_past1940,axiom,
endsBeforeStartOf @ armistice1940 @ compiegneVisit2018 ).
thf(zip_derived_cl52,plain,
endsBeforeStartOf @ armistice1940 @ compiegneVisit2018,
inference(cnf,[status(esa)],[armistice2018_past1940]) ).
thf(armistice1940_typing,axiom,
armistice @ armistice1940 ).
thf(zip_derived_cl32,plain,
armistice @ armistice1940,
inference(cnf,[status(esa)],[armistice1940_typing]) ).
thf(zip_derived_cl133,plain,
! [X0: govt,X1: govt,X2: constrCont,X3: geographicalRegion] :
( ~ ( eventOccursAt @ compiegneVisit2018 @ X3 )
| ~ ( eventOccursAt @ armistice1940 @ X3 )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X1 @ merkel )
| ~ ( narrativeSuccessor @ X2 @ X0 @ X1 )
| ~ ( govtRepresentedBy @ armistice1940 @ X0 @ hitler ) ),
inference(demod,[status(thm)],[zip_derived_cl132,zip_derived_cl52,zip_derived_cl32]) ).
thf(zip_derived_cl136,plain,
! [X0: govt,X1: govt,X2: constrCont] :
( ~ ( eventOccursAt @ armistice1940 @ rethondesCompiegne )
| ~ ( govtRepresentedBy @ compiegneVisit2018 @ X0 @ merkel )
| ~ ( narrativeSuccessor @ X2 @ X1 @ X0 )
| ~ ( govtRepresentedBy @ armistice1940 @ X1 @ hitler ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl47,zip_derived_cl133]) ).
thf(armistice1940_where,axiom,
eventOccursAt @ armistice1940 @ rethondesCompiegne ).
thf(zip_derived_cl33,plain,
eventOccursAt @ armistice1940 @ rethondesCompiegne,
inference(cnf,[status(esa)],[armistice1940_where]) ).
thf(zip_derived_cl138,plain,
! [X0: govt,X1: govt,X2: constrCont] :
( ~ ( govtRepresentedBy @ compiegneVisit2018 @ X0 @ merkel )
| ~ ( narrativeSuccessor @ X2 @ X1 @ X0 )
| ~ ( govtRepresentedBy @ armistice1940 @ X1 @ hitler ) ),
inference(demod,[status(thm)],[zip_derived_cl136,zip_derived_cl33]) ).
thf(zip_derived_cl144,plain,
! [X0: govt,X1: constrCont] :
( ~ ( narrativeSuccessor @ X1 @ X0 @ federalGermanRepublic )
| ~ ( govtRepresentedBy @ armistice1940 @ X0 @ hitler ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl50,zip_derived_cl138]) ).
thf(zip_derived_cl156,plain,
~ ( govtRepresentedBy @ armistice1940 @ thirdReich @ hitler ),
inference('s_sup-',[status(thm)],[zip_derived_cl152,zip_derived_cl144]) ).
thf(armistice1940_hitler,axiom,
govtRepresentedBy @ armistice1940 @ thirdReich @ hitler ).
thf(zip_derived_cl35,plain,
govtRepresentedBy @ armistice1940 @ thirdReich @ hitler,
inference(cnf,[status(esa)],[armistice1940_hitler]) ).
thf(zip_derived_cl158,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl156,zip_derived_cl35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ159_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.jW1g4ezq0r true
% 0.18/0.34 % Computer : n031.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Tue May 5 05:03:08 EDT 2026
% 0.18/0.34 % CPUTime :
% 0.18/0.34 % Running portfolio for 300 s
% 0.18/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.34 % Number of cores: 8
% 0.18/0.34 % Python version: Python 3.6.8
% 0.18/0.34 % Running in FO mode
% 0.46/0.62 % Total configuration time : 435
% 0.46/0.62 % Estimated wc time : 1092
% 0.46/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.54/0.73 % Solved by fo/fo6_bce.sh.
% 0.54/0.73 % BCE start: 56
% 0.54/0.73 % BCE eliminated: 4
% 0.54/0.73 % PE start: 52
% 0.54/0.73 logic: neq
% 0.54/0.73 % PE eliminated: 21
% 0.54/0.73 % done 55 iterations in 0.029s
% 0.54/0.73 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.54/0.73 % SZS output start Refutation
% See solution above
% 0.54/0.73
% 0.54/0.73
% 0.54/0.73 % Terminating...
% 0.61/0.83 % Runner terminated.
% 0.61/0.84 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------