%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT067+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 : Thu Sep 24 01:25:32 PM UTC 2026
% Result : Theorem 0.15s 0.59s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 25
% Syntax : Number of formulae : 107 ( 30 unt; 9 def)
% Number of atoms : 290 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 341 ( 158 ~; 141 |; 25 &)
% ( 9 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 10 prp; 0-10 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-3 aty)
% Number of variables : 266 ( 238 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,axiom,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,axiom,
ssStandardPurchase(ssNB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [U,V,W,X] :
( ssUserProfile(userProfileEntry(U,authObj(V,W,X)))
=> ssAccess(U,authObj(V,W,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [U,V,W,X] :
( ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))
=> ssAccess(U,authObj(V,W,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [U,V,W,X,Y,Z,X1] :
( ( ( ssHolds(U,X)
& ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1)))
& ssCompositeRole(compositeRoleEntry(X,W)) )
| ( ssHolds(U,W)
& ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1))) )
| ( ssHolds(U,V)
& ssProfile(profileEntry(V,authObj(Y,Z,X1))) ) )
=> ssUserProfile(userProfileEntry(U,authObj(Y,Z,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,axiom,
! [U,V,W,X] :
( ( ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X))
& ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__1))
& ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W))
& ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1))
& ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V))
& ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__1))
& ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME51N)) )
=> ssAccess(U,ssME51N) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [U,V,W,X,Y,Z,X1,X2,X3,X4] :
( ( ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X))
& ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W))
& ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V))
& ssAccess(U,ssME51N)
& ssStandardPurchase(W)
& ssRequisition(W,Z,X1,V,X,X2,Y,X3,X4) )
=> ssRequisitionCreated(U,W,Z,X1,V,X,X2,Y,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,axiom,
~ ? [U,V,W,X,Y,Z,X1,X2,X3,X4] :
( ssRequisition(Z,X1,X2,V,W,X,Y,X3,X4)
=> ( ssOrderCreated(U,Z,X1,X2,V,W,X,Y,X3,X4)
& ssRequisitionReleased(U,Z,X1,X2,V,W,X,Y,X3,X4)
& ssRequisitionCreated(U,Z,X1,X2,V,W,X,Y,X3,X4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,conjecture,
? [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') ).
fof(f159,negated_conjecture,
~ ? [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(negated_conjecture,[status(cth)],[f158]) ).
fof(f171,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f172,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f175,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f176,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f177,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f178,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f179,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f273,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f277,plain,
ssStandardPurchase(ssNB),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f311,plain,
! [U,V,W,X] :
( ssAccess(U,authObj(V,W,X))
| ~ ssUserProfile(userProfileEntry(U,authObj(V,W,X))) ),
inference(pre_NNF_transformation,[status(thm)],[f137]) ).
fof(f312,plain,
! [X0,X1,X2,X3] :
( ssAccess(X0,authObj(X1,X2,X3))
| ~ ssUserProfile(userProfileEntry(X0,authObj(X1,X2,X3))) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f313,plain,
! [U,V,W,X] :
( ssAccess(U,authObj(V,W,X))
| ~ ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR))) ),
inference(pre_NNF_transformation,[status(thm)],[f138]) ).
fof(f314,plain,
! [U,V,W] :
( ! [X] : ssAccess(U,authObj(V,W,X))
| ~ ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR))) ),
inference(miniscoping,[status(thm)],[f313]) ).
fof(f315,plain,
! [X0,X1,X2,X3] :
( ssAccess(X0,authObj(X1,X2,X3))
| ~ ssUserProfile(userProfileEntry(X0,authObj(X1,X2,ssSTAR))) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f321,plain,
! [U,V,W,X,Y,Z,X1] :
( ssUserProfile(userProfileEntry(U,authObj(Y,Z,X1)))
| ( ( ~ ssHolds(U,X)
| ~ ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1)))
| ~ ssCompositeRole(compositeRoleEntry(X,W)) )
& ( ~ ssHolds(U,W)
| ~ ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1))) )
& ( ~ ssHolds(U,V)
| ~ ssProfile(profileEntry(V,authObj(Y,Z,X1))) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f141]) ).
fof(f322,plain,
! [U,Y,Z,X1] :
( ssUserProfile(userProfileEntry(U,authObj(Y,Z,X1)))
| ( ! [X] :
( ~ ssHolds(U,X)
| ! [W] :
( ~ ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1)))
| ~ ssCompositeRole(compositeRoleEntry(X,W)) ) )
& ! [W] :
( ~ ssHolds(U,W)
| ~ ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1))) )
& ! [V] :
( ~ ssHolds(U,V)
| ~ ssProfile(profileEntry(V,authObj(Y,Z,X1))) ) ) ),
inference(miniscoping,[status(thm)],[f321]) ).
fof(f324,plain,
! [X0,X1,X2,X3,X4] :
( ssUserProfile(userProfileEntry(X4,authObj(X1,X2,X3)))
| ~ ssHolds(X4,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(X1,X2,X3))) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f326,plain,
! [U,V,W,X] :
( ssAccess(U,ssME51N)
| ~ ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X))
| ~ ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W))
| ~ ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V))
| ~ ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__1))
| ~ ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME51N)) ),
inference(pre_NNF_transformation,[status(thm)],[f142]) ).
fof(f327,plain,
! [U] :
( ssAccess(U,ssME51N)
| ! [X] : ~ ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X))
| ~ ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ! [W] : ~ ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W))
| ~ ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ! [V] : ~ ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V))
| ~ ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__1))
| ~ ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME51N)) ),
inference(miniscoping,[status(thm)],[f326]) ).
fof(f328,plain,
! [X0,X1,X2,X3] :
( ssAccess(X0,ssME51N)
| ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssEKGRP,X3))
| ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssBSART,X2))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssWERKS,X1))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssS_TCODE,ssTCD,ssME51N)) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f347,plain,
! [U,V,W,X,Y,Z,X1,X2,X3,X4] :
( ssRequisitionCreated(U,W,Z,X1,V,X,X2,Y,X3,X4)
| ~ ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X))
| ~ ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W))
| ~ ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V))
| ~ ssAccess(U,ssME51N)
| ~ ssStandardPurchase(W)
| ~ ssRequisition(W,Z,X1,V,X,X2,Y,X3,X4) ),
inference(pre_NNF_transformation,[status(thm)],[f149]) ).
fof(f348,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ssRequisitionCreated(X9,X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ ssAccess(X9,authObj(ssM_BANF_EKG,ssEKGRP,X4))
| ~ ssAccess(X9,authObj(ssM_BANF_BSA,ssBSART,X0))
| ~ ssAccess(X9,authObj(ssM_BANF_WRK,ssWERKS,X3))
| ~ ssAccess(X9,ssME51N)
| ~ ssStandardPurchase(X0)
| ~ ssRequisition(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f371,plain,
! [U,V,W,X,Y,Z,X1,X2,X3,X4] :
( ( ~ ssOrderCreated(U,Z,X1,X2,V,W,X,Y,X3,X4)
| ~ ssRequisitionReleased(U,Z,X1,X2,V,W,X,Y,X3,X4)
| ~ ssRequisitionCreated(U,Z,X1,X2,V,W,X,Y,X3,X4) )
& ssRequisition(Z,X1,X2,V,W,X,Y,X3,X4) ),
inference(pre_NNF_transformation,[status(thm)],[f155]) ).
fof(f372,plain,
( ! [U,V,W,X,Y,Z,X1,X2,X3,X4] :
( ~ ssOrderCreated(U,Z,X1,X2,V,W,X,Y,X3,X4)
| ~ ssRequisitionReleased(U,Z,X1,X2,V,W,X,Y,X3,X4)
| ~ ssRequisitionCreated(U,Z,X1,X2,V,W,X,Y,X3,X4) )
& ! [V,W,X,Y,Z,X1,X2,X3,X4] : ssRequisition(Z,X1,X2,V,W,X,Y,X3,X4) ),
inference(miniscoping,[status(thm)],[f371]) ).
fof(f373,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : ssRequisition(X0,X1,X2,X3,X4,X5,X6,X7,X8),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f383,plain,
! [U,V,W,X,Y,Z,X1,X2,X3] :
( ~ ssRequisitionCreated(ssMUELLER,Y,Z,X1,ssINF,V,W,X,X2,X3)
& ssRequisition(Y,Z,X1,U,ssINF,W,X,X2,X3) ),
inference(pre_NNF_transformation,[status(thm)],[f159]) ).
fof(f384,plain,
( ! [V,W,X,Y,Z,X1,X2,X3] : ~ ssRequisitionCreated(ssMUELLER,Y,Z,X1,ssINF,V,W,X,X2,X3)
& ! [U,W,X,Y,Z,X1,X2,X3] : ssRequisition(Y,Z,X1,U,ssINF,W,X,X2,X3) ),
inference(miniscoping,[status(thm)],[f383]) ).
fof(f386,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : ~ ssRequisitionCreated(ssMUELLER,X0,X1,X2,ssINF,X3,X4,X5,X6,X7),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f397,plain,
! [X0,X1,X2,X3,X4] :
( ssAccess(X3,authObj(X1,X2,X4))
| ~ ssHolds(X3,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(X1,X2,ssSTAR))) ),
inference(resolution,[status(thm)],[f324,f315]) ).
fof(f398,plain,
! [X0,X1,X2,X3,X4] :
( ssAccess(X4,authObj(X1,X2,X3))
| ~ ssHolds(X4,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(X1,X2,X3))) ),
inference(resolution,[status(thm)],[f324,f312]) ).
fof(f478,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ssRequisitionCreated(X1,X0,X4,X5,X2,X3,X6,X7,X8,X9)
| ~ ssAccess(X1,authObj(ssM_BANF_EKG,ssEKGRP,X3))
| ~ ssAccess(X1,authObj(ssM_BANF_BSA,ssBSART,X0))
| ~ ssAccess(X1,authObj(ssM_BANF_WRK,ssWERKS,X2))
| ~ ssAccess(X1,ssME51N)
| ~ ssStandardPurchase(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f348,f373]) ).
fof(f479,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ssRequisitionCreated(X0,ssNB,X3,X4,X1,X2,X5,X6,X7,X8)
| ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssEKGRP,X2))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssBSART,ssNB))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssWERKS,X1))
| ~ ssAccess(X0,ssME51N) ),
inference(resolution,[status(thm)],[f478,f277]) ).
fof(f480,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssEKGRP,X11))
| ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssBSART,X10))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssWERKS,X9))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssACTVT,np__1))
| ~ ssAccess(X0,authObj(ssS_TCODE,ssTCD,ssME51N))
| ssRequisitionCreated(X0,ssNB,X3,X4,X1,X2,X5,X6,X7,X8)
| ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssEKGRP,X2))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssBSART,ssNB))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssWERKS,X1)) ),
inference(resolution,[status(thm)],[f479,f328]) ).
fof(f481,plain,
! [X0,X1,X2,X3] :
( ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X3))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X2))
| ~ 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,X0))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)) ),
inference(resolution,[status(thm)],[f480,f386]) ).
fof(f482,definition,
( sQ10_spl
<=> ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f484,plain,
( sQ10_spl
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)) ),
inference(component_clause,[status(thm)],[f482]) ).
fof(f485,definition,
( sQ11_spl
<=> ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f487,plain,
( sQ11_spl
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB)) ),
inference(component_clause,[status(thm)],[f485]) ).
fof(f488,definition,
! [X0] :
( sQ12_spl
<=> ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X0)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f489,plain,
! [X0] :
( ~ sQ12_spl
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X0)) ),
inference(component_clause,[status(thm)],[f488]) ).
fof(f491,definition,
( sQ13_spl
<=> ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( sQ13_spl
| ~ ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)) ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,definition,
( sQ14_spl
<=> ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f496,plain,
( sQ14_spl
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,definition,
! [X1] :
( sQ15_spl
<=> ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X1)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f498,plain,
! [X0] :
( ~ sQ15_spl
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0)) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,definition,
( sQ16_spl
<=> ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f502,plain,
( sQ16_spl
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,definition,
! [X2] :
( sQ17_spl
<=> ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X2)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f504,plain,
! [X0] :
( ~ sQ17_spl
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X0)) ),
inference(component_clause,[status(thm)],[f503]) ).
fof(f506,definition,
( sQ18_spl
<=> ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( sQ18_spl
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1)) ),
inference(component_clause,[status(thm)],[f506]) ).
fof(f509,plain,
( ~ sQ18_spl
| sQ17_spl
| ~ sQ16_spl
| sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f481,f482,f485,f488,f491,f494,f497,f500,f503,f506]) ).
fof(f512,plain,
! [X0] :
( sQ18_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) ),
inference(resolution,[status(thm)],[f508,f397]) ).
fof(f515,plain,
( sQ18_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) ),
inference(resolution,[status(thm)],[f512,f273]) ).
fof(f516,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f178]) ).
fof(f517,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f516]) ).
fof(f521,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssM_BANF_BSA,ssBSART,X1))) ),
inference(resolution,[status(thm)],[f504,f398]) ).
fof(f522,plain,
! [X0] :
( ~ sQ17_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,X0))) ),
inference(resolution,[status(thm)],[f521,f273]) ).
fof(f523,plain,
( ~ sQ17_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f177,f522]) ).
fof(f524,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f523]) ).
fof(f527,plain,
! [X0] :
( sQ16_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))) ),
inference(resolution,[status(thm)],[f502,f397]) ).
fof(f530,plain,
( sQ16_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))) ),
inference(resolution,[status(thm)],[f527,f273]) ).
fof(f531,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f530,f176]) ).
fof(f532,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f531]) ).
fof(f536,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssM_BANF_WRK,ssWERKS,X1))) ),
inference(resolution,[status(thm)],[f498,f398]) ).
fof(f537,plain,
! [X0] :
( ~ sQ15_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,X0))) ),
inference(resolution,[status(thm)],[f536,f273]) ).
fof(f538,plain,
( ~ sQ15_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f175,f537]) ).
fof(f539,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f538]) ).
fof(f543,plain,
! [X0] :
( sQ14_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssM_BANF_WRK,ssACTVT,np__1))) ),
inference(resolution,[status(thm)],[f496,f398]) ).
fof(f544,plain,
( sQ14_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))) ),
inference(resolution,[status(thm)],[f543,f273]) ).
fof(f545,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f544,f172]) ).
fof(f546,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f545]) ).
fof(f550,plain,
! [X0] :
( sQ13_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssS_TCODE,ssTCD,ssME51N))) ),
inference(resolution,[status(thm)],[f493,f398]) ).
fof(f551,plain,
( sQ13_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))) ),
inference(resolution,[status(thm)],[f550,f273]) ).
fof(f552,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f551,f171]) ).
fof(f553,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f552]) ).
fof(f557,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssM_BANF_EKG,ssEKGRP,X1))) ),
inference(resolution,[status(thm)],[f489,f398]) ).
fof(f558,plain,
! [X0] :
( ~ sQ12_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,X0))) ),
inference(resolution,[status(thm)],[f557,f273]) ).
fof(f559,plain,
( ~ sQ12_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f179,f558]) ).
fof(f560,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f559]) ).
fof(f564,plain,
! [X0] :
( sQ10_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) ),
inference(resolution,[status(thm)],[f484,f398]) ).
fof(f565,plain,
( sQ10_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) ),
inference(resolution,[status(thm)],[f564,f273]) ).
fof(f566,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f175]) ).
fof(f567,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f566]) ).
fof(f570,plain,
! [X0] :
( sQ11_spl
| ~ ssHolds(ssMUELLER,X0)
| ~ ssSingleRole(singleRoleEntry(X0,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) ),
inference(resolution,[status(thm)],[f487,f397]) ).
fof(f572,plain,
( sQ11_spl
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) ),
inference(resolution,[status(thm)],[f570,f273]) ).
fof(f573,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f572,f177]) ).
fof(f574,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f573]) ).
fof(f575,plain,
$false,
inference(sat_refutation,[status(thm)],[f509,f517,f524,f532,f539,f546,f553,f560,f567,f574]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.55 % Computer : n011.cluster.edu
% 0.11/0.55 % Model : x86_64 x86_64
% 0.11/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.55 % Memory : 8046.5625MB
% 0.11/0.55 % OS : Linux 6.8.0-71-generic
% 0.11/0.55 % CPULimit : 300
% 0.11/0.55 % WCLimit : 300
% 0.11/0.55 % DateTime : Mon Sep 21 01:25:11 UTC 2026
% 0.11/0.55 % CPUTime :
% 0.15/0.56 % Drodi V4.1.1
% 0.15/0.59 % Refutation found
% 0.15/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.61 % Elapsed time: 0.056560 seconds
% 0.15/0.61 % CPU time: 0.167630 seconds
% 0.15/0.61 % Total memory used: 29.695 MB
% 0.15/0.61 % Net memory used: 29.552 MB
%------------------------------------------------------------------------------