%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:11:30 AM UTC 2026
% Result : Theorem 1.00s 0.53s
% Output : CNFRefutation 1.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 16
% Syntax : Number of formulae : 79 ( 44 unt; 0 def)
% Number of atoms : 166 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 151 ( 64 ~; 62 |; 17 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-10 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-3 aty)
% Number of variables : 121 ( 35 sgn 29 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,plain,
? [U,V,W,X,Y,Z,X1,X2,X3] :
( ssRequisition(Y,Z,X1,U,ssINF,W,X,X2,X3)
=> ssRequisitionCreated(ssMUELLER,Y,Z,X1,ssINF,V,W,X,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(co1_negated,plain,
~ ? [U,V,W,X,Y,Z,X1,X2,X3] :
( ssRequisition(Y,Z,X1,U,ssINF,W,X,X2,X3)
=> ssRequisitionCreated(ssMUELLER,Y,Z,X1,ssINF,V,W,X,X2,X3) ),
inference(negate_conjecture,[status(cth)],[co1]) ).
cnf(176,plain,
~ ssRequisitionCreated(ssMUELLER,X0,X1,X2,ssINF,X3,X4,X5,X6,X7),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l0,plain,
~ ssRequisitionCreated(ssMUELLER,ssNB,X1_295,X2_295,ssINF,ssI26,X5_295,X6_295,X7_295,X8_295),
inference(instantiation,[status(thm)],[176]) ).
fof(ax149,plain,
! [U,V,W,X,Y,Z,X1,X2,X3,X4] :
( ( 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax149) ).
cnf(157,plain,
( ~ ssRequisition(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ ssAccess(X9,ssME51N)
| ~ ssAccess(X9,authObj(ssM_BANF_EKG,ssEKGRP,X4))
| ~ ssAccess(X9,authObj(ssM_BANF_WRK,ssWERKS,X3))
| ~ ssAccess(X9,authObj(ssM_BANF_BSA,ssBSART,X0))
| ~ ssStandardPurchase(X0)
| ssRequisitionCreated(X9,X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(cnf,[status(esa)],[ax149]) ).
cnf(l1,plain,
( ~ ssRequisition(ssNB,X1_295,X2_295,ssINF,ssI26,X5_295,X6_295,X7_295,X8_295)
| ~ ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB))
| ~ ssStandardPurchase(ssNB)
| ssRequisitionCreated(ssMUELLER,ssNB,X1_295,X2_295,ssINF,ssI26,X5_295,X6_295,X7_295,X8_295) ),
inference(instantiation,[status(thm)],[157]) ).
fof(ax155,plain,
~ ? [U,V,W,X,Y,Z,X1,X2,X3,X4] :
( 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) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax155) ).
cnf(171,plain,
ssRequisition(X0,X1,X2,X3,X4,X5,X6,X7,X8),
inference(cnf,[status(esa)],[ax155]) ).
cnf(l295,plain,
ssRequisition(ssNB,X1_295,X2_295,ssINF,ssI26,X5_295,X6_295,X7_295,X8_295),
inference(instantiation,[status(thm)],[171]) ).
fof(ax142,plain,
! [U,V,W,X] :
( ( 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax142) ).
cnf(150,plain,
( ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssEKGRP,X1))
| ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssWERKS,X2))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssBSART,X3))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssS_TCODE,ssTCD,ssME51N))
| ssAccess(X0,ssME51N) ),
inference(cnf,[status(esa)],[ax142]) ).
cnf(l2,plain,
( ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X3_42))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))
| ssAccess(ssMUELLER,ssME51N) ),
inference(instantiation,[status(thm)],[150]) ).
fof(ax138,plain,
! [U,V,W,X] :
( ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))
=> ssAccess(U,authObj(V,W,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax138) ).
cnf(143,plain,
( ~ ssUserProfile(userProfileEntry(X0,authObj(X1,X2,ssSTAR)))
| ssAccess(X0,authObj(X1,X2,X3)) ),
inference(cnf,[status(esa)],[ax138]) ).
cnf(l42,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X3_42)) ),
inference(instantiation,[status(thm)],[143]) ).
fof(ax137,plain,
! [U,V,W,X] :
( ssUserProfile(userProfileEntry(U,authObj(V,W,X)))
=> ssAccess(U,authObj(V,W,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax137) ).
cnf(142,plain,
( ~ ssUserProfile(userProfileEntry(X0,authObj(X1,X2,X3)))
| ssAccess(X0,authObj(X1,X2,X3)) ),
inference(cnf,[status(esa)],[ax137]) ).
cnf(l5,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)) ),
inference(instantiation,[status(thm)],[142]) ).
fof(ax141,plain,
! [U,V,W,X,Y,Z,X1] :
( ( ( 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))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax141) ).
cnf(148,plain,
( ~ ssHolds(X0,X1)
| ~ ssSingleRole(singleRoleEntry(X1,authObj(X2,X3,X4)))
| ssUserProfile(userProfileEntry(X0,authObj(X2,X3,X4))) ),
inference(cnf,[status(esa)],[ax141]) ).
cnf(l152,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l7,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) ),
inference(instantiation,[status(thm)],[143]) ).
cnf(l30,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))) ),
inference(instantiation,[status(thm)],[148]) ).
fof(ax18,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
cnf(17,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(cnf,[status(esa)],[ax18]) ).
cnf(l389,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(instantiation,[status(thm)],[17]) ).
fof(ax118,plain,
ssStandardPurchase(ssNB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax118) ).
cnf(117,plain,
ssStandardPurchase(ssNB),
inference(cnf,[status(esa)],[ax118]) ).
cnf(l48,plain,
ssStandardPurchase(ssNB),
inference(instantiation,[status(thm)],[117]) ).
cnf(l4,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)) ),
inference(instantiation,[status(thm)],[142]) ).
fof(ax114,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax114) ).
cnf(113,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(cnf,[status(esa)],[ax114]) ).
cnf(l384,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
cnf(l192,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
cnf(l10,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) ),
inference(instantiation,[status(thm)],[142]) ).
cnf(l16,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)))
| ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)) ),
inference(instantiation,[status(thm)],[142]) ).
cnf(l138,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB)) ),
inference(instantiation,[status(thm)],[143]) ).
cnf(l65,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)) ),
inference(instantiation,[status(thm)],[142]) ).
cnf(l27,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l164,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
fof(ax16,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
cnf(15,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(cnf,[status(esa)],[ax16]) ).
cnf(l360,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(instantiation,[status(thm)],[15]) ).
cnf(l216,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l80,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l92,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1)) ),
inference(instantiation,[status(thm)],[143]) ).
cnf(l189,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l54,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))) ),
inference(instantiation,[status(thm)],[148]) ).
fof(ax19,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
cnf(18,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
inference(cnf,[status(esa)],[ax19]) ).
cnf(l190,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
inference(instantiation,[status(thm)],[18]) ).
cnf(l24,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l127,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
cnf(l385,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
cnf(l439,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
fof(ax20,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
cnf(19,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(cnf,[status(esa)],[ax20]) ).
cnf(l387,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(instantiation,[status(thm)],[19]) ).
cnf(l310,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
cnf(l147,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l93,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(instantiation,[status(thm)],[19]) ).
cnf(l33,plain,
( ~ ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))
| ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)) ),
inference(instantiation,[status(thm)],[142]) ).
fof(ax17,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
cnf(16,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
inference(cnf,[status(esa)],[ax17]) ).
cnf(l34,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
inference(instantiation,[status(thm)],[16]) ).
cnf(l379,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
cnf(l197,plain,
( ~ ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))
| ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) ),
inference(instantiation,[status(thm)],[148]) ).
fof(ax12,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
cnf(11,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
inference(cnf,[status(esa)],[ax12]) ).
cnf(l382,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
inference(instantiation,[status(thm)],[11]) ).
cnf(l62,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
cnf(l203,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(instantiation,[status(thm)],[15]) ).
cnf(l438,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(instantiation,[status(thm)],[113]) ).
fof(ax13,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
cnf(12,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
inference(cnf,[status(esa)],[ax13]) ).
cnf(l151,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
inference(instantiation,[status(thm)],[12]) ).
cnf(l352,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(instantiation,[status(thm)],[17]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l295,l2,l42,l5,l152,l7,l30,l389,l48,l4,l384,l192,l10,l16,l138,l65,l27,l164,l360,l216,l80,l92,l189,l54,l190,l24,l127,l385,l439,l387,l310,l147,l93,l33,l34,l379,l197,l382,l62,l203,l438,l151,l352]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n006.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 7 13:51:01 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % launching worker at depth: 1
% 0.13/0.37 % launching worker at depth: 6
% 0.13/0.37 % launching worker at depth: 7
% 0.13/0.37 % launching worker at depth: 8
% 0.13/0.37 % launching worker at depth: 4
% 0.13/0.37 % launching worker at depth: 2
% 0.13/0.37 % launching worker at depth: 3
% 0.13/0.37 % launching worker at depth: 5
% 0.13/0.37 % launching worker at depth: 9
% 0.13/0.38 % launching worker at depth: 10
% 0.13/0.38 % launching worker at depth: 11
% 0.13/0.39 % launching worker at depth: 12
% 1.00/0.53 % SZS status Theorem for theBenchmark
% 1.00/0.53 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------