%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.HQ1qbXsrko true
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:25:19 AM UTC 2026
% Result : Theorem 0.49s 0.85s
% Output : Refutation 0.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 16
% Syntax : Number of formulae : 61 ( 33 unt; 0 typ; 0 def)
% Number of atoms : 135 ( 0 equ; 0 cnn)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 840 ( 52 ~; 49 |; 17 &; 714 @)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 10 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 34 ( 33 usr; 18 con; 0-10 aty)
% Number of variables : 158 ( 0 ^; 130 !; 28 ?; 158 :)
% Comments :
%------------------------------------------------------------------------------
thf(authObj_type,type,
authObj: $i > $i > $i > $i ).
thf(ssAccess_type,type,
ssAccess: $i > $i > $o ).
thf(np__1_type,type,
np__1: $i ).
thf(compositeRoleEntry_type,type,
compositeRoleEntry: $i > $i > $i ).
thf(ssNB_type,type,
ssNB: $i ).
thf(ssMUELLER_type,type,
ssMUELLER: $i ).
thf(ssSTAR_type,type,
ssSTAR: $i ).
thf(ssEKGRP_type,type,
ssEKGRP: $i ).
thf(ssS_TCODE_type,type,
ssS_TCODE: $i ).
thf(ssSingleRole_type,type,
ssSingleRole: $i > $o ).
thf(singleRoleEntry_type,type,
singleRoleEntry: $i > $i > $i ).
thf(ssCompositeRole_type,type,
ssCompositeRole: $i > $o ).
thf(ssME51N_type,type,
ssME51N: $i ).
thf(ssZBANF_WRK_INF_ED_type,type,
ssZBANF_WRK_INF_ED: $i ).
thf(ssRequisition_type,type,
ssRequisition: $i > $i > $i > $i > $i > $i > $i > $i > $i > $o ).
thf(ssINF_type,type,
ssINF: $i ).
thf(ssHolds_type,type,
ssHolds: $i > $i > $o ).
thf(ssRequisitionReleased_type,type,
ssRequisitionReleased: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $o ).
thf(ssM_BANF_EKG_type,type,
ssM_BANF_EKG: $i ).
thf(ssI26_type,type,
ssI26: $i ).
thf(ssBSART_type,type,
ssBSART: $i ).
thf(ssRequisitionCreated_type,type,
ssRequisitionCreated: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $o ).
thf(ssProfile_type,type,
ssProfile: $i > $o ).
thf(ssOrderCreated_type,type,
ssOrderCreated: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $o ).
thf(ssACTVT_type,type,
ssACTVT: $i ).
thf(ssStandardPurchase_type,type,
ssStandardPurchase: $i > $o ).
thf(ssUserProfile_type,type,
ssUserProfile: $i > $o ).
thf(ssM_BANF_WRK_type,type,
ssM_BANF_WRK: $i ).
thf(ssTCD_type,type,
ssTCD: $i ).
thf(profileEntry_type,type,
profileEntry: $i > $i > $i ).
thf(ssWERKS_type,type,
ssWERKS: $i ).
thf(ssM_BANF_BSA_type,type,
ssM_BANF_BSA: $i ).
thf(userProfileEntry_type,type,
userProfileEntry: $i > $i > $i ).
thf(ax20,axiom,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ ssI26 ) ) ).
thf(zip_derived_cl19,plain,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ ssI26 ) ),
inference(cnf,[status(esa)],[ax20]) ).
thf(ax114,axiom,
ssHolds @ ssMUELLER @ ssZBANF_WRK_INF_ED ).
thf(zip_derived_cl113,plain,
ssHolds @ ssMUELLER @ ssZBANF_WRK_INF_ED,
inference(cnf,[status(esa)],[ax114]) ).
thf(ax141,axiom,
! [U: $i,V: $i,W: $i,X: $i,Y: $i,Z: $i,X1: $i] :
( ( ( ( ssProfile @ ( profileEntry @ V @ ( authObj @ Y @ Z @ X1 ) ) )
& ( ssHolds @ U @ V ) )
| ( ( ssSingleRole @ ( singleRoleEntry @ W @ ( authObj @ Y @ Z @ X1 ) ) )
& ( ssHolds @ U @ W ) )
| ( ( ssCompositeRole @ ( compositeRoleEntry @ X @ W ) )
& ( ssSingleRole @ ( singleRoleEntry @ W @ ( authObj @ Y @ Z @ X1 ) ) )
& ( ssHolds @ U @ X ) ) )
=> ( ssUserProfile @ ( userProfileEntry @ U @ ( authObj @ Y @ Z @ X1 ) ) ) ) ).
thf(zip_derived_cl148,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( ssUserProfile @ ( userProfileEntry @ X0 @ ( authObj @ X1 @ X2 @ X3 ) ) )
| ~ ( ssSingleRole @ ( singleRoleEntry @ X4 @ ( authObj @ X1 @ X2 @ X3 ) ) )
| ~ ( ssHolds @ X0 @ X4 ) ),
inference(cnf,[status(esa)],[ax141]) ).
thf(zip_derived_cl291,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X2 @ X1 @ X0 ) ) )
| ( ssUserProfile @ ( userProfileEntry @ ssMUELLER @ ( authObj @ X2 @ X1 @ X0 ) ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl113,zip_derived_cl148]) ).
thf(ax137,axiom,
! [U: $i,V: $i,W: $i,X: $i] :
( ( ssUserProfile @ ( userProfileEntry @ U @ ( authObj @ V @ W @ X ) ) )
=> ( ssAccess @ U @ ( authObj @ V @ W @ X ) ) ) ).
thf(zip_derived_cl142,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ssAccess @ X0 @ ( authObj @ X1 @ X2 @ X3 ) )
| ~ ( ssUserProfile @ ( userProfileEntry @ X0 @ ( authObj @ X1 @ X2 @ X3 ) ) ) ),
inference(cnf,[status(esa)],[ax137]) ).
thf(zip_derived_cl369,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X2 @ X1 @ X0 ) ) )
| ( ssAccess @ ssMUELLER @ ( authObj @ X2 @ X1 @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl291,zip_derived_cl142]) ).
thf(zip_derived_cl382,plain,
ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ ssI26 ),
inference('s_sup-',[status(thm)],[zip_derived_cl19,zip_derived_cl369]) ).
thf(ax118,axiom,
ssStandardPurchase @ ssNB ).
thf(zip_derived_cl117,plain,
ssStandardPurchase @ ssNB,
inference(cnf,[status(esa)],[ax118]) ).
thf(ax149,axiom,
! [U: $i,V: $i,W: $i,X: $i,Y: $i,Z: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( ( ssRequisition @ W @ Z @ X1 @ V @ X @ X2 @ Y @ X3 @ X4 )
& ( ssStandardPurchase @ W )
& ( ssAccess @ U @ ssME51N )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ V ) )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_BSA @ ssBSART @ W ) )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X ) ) )
=> ( ssRequisitionCreated @ U @ W @ Z @ X1 @ V @ X @ X2 @ Y @ X3 @ X4 ) ) ).
thf(zip_derived_cl157,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] :
( ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X1 ) )
| ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_BSA @ ssBSART @ X2 ) )
| ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ X3 ) )
| ~ ( ssAccess @ X0 @ ssME51N )
| ~ ( ssStandardPurchase @ X2 )
| ~ ( ssRequisition @ X2 @ X4 @ X5 @ X3 @ X1 @ X6 @ X7 @ X8 @ X9 )
| ( ssRequisitionCreated @ X0 @ X2 @ X4 @ X5 @ X3 @ X1 @ X6 @ X7 @ X8 @ X9 ) ),
inference(cnf,[status(esa)],[ax149]) ).
thf(zip_derived_cl179,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( ( ssRequisitionCreated @ X8 @ ssNB @ X7 @ X6 @ X5 @ X4 @ X3 @ X2 @ X1 @ X0 )
| ~ ( ssRequisition @ ssNB @ X7 @ X6 @ X5 @ X4 @ X3 @ X2 @ X1 @ X0 )
| ~ ( ssAccess @ X8 @ ssME51N )
| ~ ( ssAccess @ X8 @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ X5 ) )
| ~ ( ssAccess @ X8 @ ( authObj @ ssM_BANF_BSA @ ssBSART @ ssNB ) )
| ~ ( ssAccess @ X8 @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X4 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl117,zip_derived_cl157]) ).
thf(ax155,axiom,
~ ? [U: $i,V: $i,W: $i,X: $i,Y: $i,Z: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( ssRequisition @ Z @ X1 @ X2 @ V @ W @ X @ Y @ X3 @ X4 )
=> ( ( ssRequisitionCreated @ U @ Z @ X1 @ X2 @ V @ W @ X @ Y @ X3 @ X4 )
& ( ssRequisitionReleased @ U @ Z @ X1 @ X2 @ V @ W @ X @ Y @ X3 @ X4 )
& ( ssOrderCreated @ U @ Z @ X1 @ X2 @ V @ W @ X @ Y @ X3 @ X4 ) ) ) ).
thf(zip_derived_cl172,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : ( ssRequisition @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 ),
inference(cnf,[status(esa)],[ax155]) ).
thf(zip_derived_cl411,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( ( ssRequisitionCreated @ X8 @ ssNB @ X7 @ X6 @ X5 @ X4 @ X3 @ X2 @ X1 @ X0 )
| ~ ( ssAccess @ X8 @ ssME51N )
| ~ ( ssAccess @ X8 @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ X5 ) )
| ~ ( ssAccess @ X8 @ ( authObj @ ssM_BANF_BSA @ ssBSART @ ssNB ) )
| ~ ( ssAccess @ X8 @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X4 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl179,zip_derived_cl172]) ).
thf(co1,conjecture,
? [U: $i,V: $i,W: $i,X: $i,Y: $i,Z: $i,X1: $i,X2: $i,X3: $i] :
( ( ssRequisition @ Y @ Z @ X1 @ U @ ssINF @ W @ X @ X2 @ X3 )
=> ( ssRequisitionCreated @ ssMUELLER @ Y @ Z @ X1 @ ssINF @ V @ W @ X @ X2 @ X3 ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ? [U: $i,V: $i,W: $i,X: $i,Y: $i,Z: $i,X1: $i,X2: $i,X3: $i] :
( ( ssRequisition @ Y @ Z @ X1 @ U @ ssINF @ W @ X @ X2 @ X3 )
=> ( ssRequisitionCreated @ ssMUELLER @ Y @ Z @ X1 @ ssINF @ V @ W @ X @ X2 @ X3 ) ),
inference('cnf.neg',[status(esa)],[co1]) ).
thf(zip_derived_cl177,plain,
! [X0: $i,X1: $i,X2: $i,X4: $i,X5: $i,X6: $i,X8: $i,X9: $i] :
~ ( ssRequisitionCreated @ ssMUELLER @ X0 @ X1 @ X2 @ ssINF @ X8 @ X4 @ X5 @ X6 @ X9 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl413,plain,
! [X4: $i] :
( ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X4 ) )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_BSA @ ssBSART @ ssNB ) )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ ssINF ) )
| ~ ( ssAccess @ ssMUELLER @ ssME51N ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl411,zip_derived_cl177]) ).
thf(ax18,axiom,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_BSA @ ssBSART @ ssSTAR ) ) ).
thf(zip_derived_cl17,plain,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_BSA @ ssBSART @ ssSTAR ) ),
inference(cnf,[status(esa)],[ax18]) ).
thf(zip_derived_cl291_001,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X2 @ X1 @ X0 ) ) )
| ( ssUserProfile @ ( userProfileEntry @ ssMUELLER @ ( authObj @ X2 @ X1 @ X0 ) ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl113,zip_derived_cl148]) ).
thf(ax138,axiom,
! [U: $i,V: $i,W: $i,X: $i] :
( ( ssUserProfile @ ( userProfileEntry @ U @ ( authObj @ V @ W @ ssSTAR ) ) )
=> ( ssAccess @ U @ ( authObj @ V @ W @ X ) ) ) ).
thf(zip_derived_cl143,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( ssUserProfile @ ( userProfileEntry @ X0 @ ( authObj @ X1 @ X2 @ ssSTAR ) ) )
| ( ssAccess @ X0 @ ( authObj @ X1 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[ax138]) ).
thf(zip_derived_cl370,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X1 @ X0 @ ssSTAR ) ) )
| ( ssAccess @ ssMUELLER @ ( authObj @ X1 @ X0 @ X2 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl291,zip_derived_cl143]) ).
thf(zip_derived_cl384,plain,
! [X0: $i] : ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_BSA @ ssBSART @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl17,zip_derived_cl370]) ).
thf(ax16,axiom,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ ssINF ) ) ).
thf(zip_derived_cl15,plain,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ ssINF ) ),
inference(cnf,[status(esa)],[ax16]) ).
thf(zip_derived_cl369_002,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X2 @ X1 @ X0 ) ) )
| ( ssAccess @ ssMUELLER @ ( authObj @ X2 @ X1 @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl291,zip_derived_cl142]) ).
thf(zip_derived_cl378,plain,
ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ ssINF ),
inference('s_sup-',[status(thm)],[zip_derived_cl15,zip_derived_cl369]) ).
thf(zip_derived_cl382_003,plain,
ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ ssI26 ),
inference('s_sup-',[status(thm)],[zip_derived_cl19,zip_derived_cl369]) ).
thf(zip_derived_cl378_004,plain,
ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ ssINF ),
inference('s_sup-',[status(thm)],[zip_derived_cl15,zip_derived_cl369]) ).
thf(ax19,axiom,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_EKG @ ssACTVT @ ssSTAR ) ) ).
thf(zip_derived_cl18,plain,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_EKG @ ssACTVT @ ssSTAR ) ),
inference(cnf,[status(esa)],[ax19]) ).
thf(zip_derived_cl370_005,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X1 @ X0 @ ssSTAR ) ) )
| ( ssAccess @ ssMUELLER @ ( authObj @ X1 @ X0 @ X2 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl291,zip_derived_cl143]) ).
thf(zip_derived_cl385,plain,
! [X0: $i] : ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_EKG @ ssACTVT @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl18,zip_derived_cl370]) ).
thf(ax142,axiom,
! [U: $i,V: $i,W: $i,X: $i] :
( ( ( ssAccess @ U @ ( authObj @ ssS_TCODE @ ssTCD @ ssME51N ) )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_WRK @ ssACTVT @ np__1 ) )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ V ) )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_BSA @ ssACTVT @ np__1 ) )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_BSA @ ssBSART @ W ) )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_EKG @ ssACTVT @ np__1 ) )
& ( ssAccess @ U @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X ) ) )
=> ( ssAccess @ U @ ssME51N ) ) ).
thf(zip_derived_cl150,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ssAccess @ X0 @ ssME51N )
| ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_EKG @ ssACTVT @ np__1 ) )
| ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_BSA @ ssBSART @ X1 ) )
| ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_BSA @ ssACTVT @ np__1 ) )
| ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ X2 ) )
| ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_WRK @ ssACTVT @ np__1 ) )
| ~ ( ssAccess @ X0 @ ( authObj @ ssS_TCODE @ ssTCD @ ssME51N ) )
| ~ ( ssAccess @ X0 @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X3 ) ) ),
inference(cnf,[status(esa)],[ax142]) ).
thf(zip_derived_cl386,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ssAccess @ ssMUELLER @ ssME51N )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_BSA @ ssBSART @ X0 ) )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_BSA @ ssACTVT @ np__1 ) )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ X1 ) )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_WRK @ ssACTVT @ np__1 ) )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssS_TCODE @ ssTCD @ ssME51N ) )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X2 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl385,zip_derived_cl150]) ).
thf(zip_derived_cl384_006,plain,
! [X0: $i] : ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_BSA @ ssBSART @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl17,zip_derived_cl370]) ).
thf(ax17,axiom,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_BSA @ ssACTVT @ ssSTAR ) ) ).
thf(zip_derived_cl16,plain,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_BSA @ ssACTVT @ ssSTAR ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl370_007,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X1 @ X0 @ ssSTAR ) ) )
| ( ssAccess @ ssMUELLER @ ( authObj @ X1 @ X0 @ X2 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl291,zip_derived_cl143]) ).
thf(zip_derived_cl383,plain,
! [X0: $i] : ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_BSA @ ssACTVT @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl16,zip_derived_cl370]) ).
thf(ax13,axiom,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_WRK @ ssACTVT @ np__1 ) ) ).
thf(zip_derived_cl12,plain,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssM_BANF_WRK @ ssACTVT @ np__1 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl369_008,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X2 @ X1 @ X0 ) ) )
| ( ssAccess @ ssMUELLER @ ( authObj @ X2 @ X1 @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl291,zip_derived_cl142]) ).
thf(zip_derived_cl375,plain,
ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_WRK @ ssACTVT @ np__1 ),
inference('s_sup-',[status(thm)],[zip_derived_cl12,zip_derived_cl369]) ).
thf(ax12,axiom,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssS_TCODE @ ssTCD @ ssME51N ) ) ).
thf(zip_derived_cl11,plain,
ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ ssS_TCODE @ ssTCD @ ssME51N ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl369_009,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( ssSingleRole @ ( singleRoleEntry @ ssZBANF_WRK_INF_ED @ ( authObj @ X2 @ X1 @ X0 ) ) )
| ( ssAccess @ ssMUELLER @ ( authObj @ X2 @ X1 @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl291,zip_derived_cl142]) ).
thf(zip_derived_cl374,plain,
ssAccess @ ssMUELLER @ ( authObj @ ssS_TCODE @ ssTCD @ ssME51N ),
inference('s_sup-',[status(thm)],[zip_derived_cl11,zip_derived_cl369]) ).
thf(zip_derived_cl388,plain,
! [X1: $i,X2: $i] :
( ( ssAccess @ ssMUELLER @ ssME51N )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_WRK @ ssWERKS @ X1 ) )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X2 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl386,zip_derived_cl384,zip_derived_cl383,zip_derived_cl375,zip_derived_cl374]) ).
thf(zip_derived_cl390,plain,
! [X0: $i] :
( ( ssAccess @ ssMUELLER @ ssME51N )
| ~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl378,zip_derived_cl388]) ).
thf(zip_derived_cl391,plain,
ssAccess @ ssMUELLER @ ssME51N,
inference('s_sup-',[status(thm)],[zip_derived_cl382,zip_derived_cl390]) ).
thf(zip_derived_cl414,plain,
! [X4: $i] :
~ ( ssAccess @ ssMUELLER @ ( authObj @ ssM_BANF_EKG @ ssEKGRP @ X4 ) ),
inference(demod,[status(thm)],[zip_derived_cl413,zip_derived_cl384,zip_derived_cl378,zip_derived_cl391]) ).
thf(zip_derived_cl415,plain,
$false,
inference('s_sup-',[status(thm)],[zip_derived_cl382,zip_derived_cl414]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% 0.00/0.05 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.HQ1qbXsrko true
% 0.12/0.37 % Computer : n018.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 7 13:53:07 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 % Running portfolio for 300 s
% 0.12/0.37 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.38 % Number of cores: 8
% 0.12/0.38 % Python version: Python 3.12.3
% 0.12/0.38 % Running in FO mode
% 0.45/0.66 % Total configuration time : 435
% 0.45/0.66 % Estimated wc time : 1092
% 0.45/0.66 % Estimated cpu time (7 cpus) : 156.0
% 0.48/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.49/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.49/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.49/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.49/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.49/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.49/0.85 % Solved by fo/fo6_bce.sh.
% 0.49/0.85 % BCE start: 178
% 0.49/0.85 % BCE eliminated: 2
% 0.49/0.85 % PE start: 176
% 0.49/0.85 logic: neq
% 0.49/0.85 % PE eliminated: 7
% 0.49/0.85 % done 180 iterations in 0.092s
% 0.49/0.85 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.49/0.85 % SZS output start Refutation
% See solution above
% 0.49/0.86
% 0.49/0.86
% 0.49/0.86 % Terminating...
% 0.49/0.89 % Runner terminated.
% 1.74/0.91 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------