%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT067+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.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 : Fri Sep 25 02:11:54 PM UTC 2026
% Result : Theorem 3.09s 0.84s
% Output : Proof 3.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 16
% Syntax : Number of formulae : 91 ( 46 unt; 0 def)
% Number of atoms : 230 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 254 ( 115 ~; 106 |; 25 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 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 : 266 ( 72 sgn 125 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f140,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/sandbox2/benchmark/theBenchmark.p',ax141) ).
fof(f140_nnf,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(nnf_transformation,[status(thm)],[f140]) ).
fof(f140_sk,plain,
! [V,Y,Z,X1,U,W,X] :
( 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(skolemisation,[status(esa)],[f140_nnf]) ).
cnf(c148,plain,
( ssUserProfile(userProfileEntry(X0,authObj(X4,X5,X6)))
| ~ ssHolds(X0,X2)
| ~ ssSingleRole(singleRoleEntry(X2,authObj(X4,X5,X6))) ),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
fof(f11,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f11_nnf,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(p202,plain,
( ssUserProfile(userProfileEntry(X0,authObj(ssS_TCODE,ssTCD,ssME51N)))
| ~ ssHolds(X0,ssZBANF_WRK_INF_ED) ),
inference(resolution,[status(thm)],[c148,c11]) ).
fof(f113,axiom,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax114) ).
fof(f113_nnf,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(nnf_transformation,[status(thm)],[f113]) ).
cnf(c113,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(cnf_transformation,[status(esa)],[f113_nnf]) ).
cnf(p306,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))),
inference(resolution,[status(thm)],[p202,c113]) ).
fof(f136,axiom,
! [U,V,W,X] :
( ssUserProfile(userProfileEntry(U,authObj(V,W,X)))
=> ssAccess(U,authObj(V,W,X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax137) ).
fof(f136_nnf,plain,
! [U,V,W,X] :
( ssAccess(U,authObj(V,W,X))
| ~ ssUserProfile(userProfileEntry(U,authObj(V,W,X))) ),
inference(nnf_transformation,[status(thm)],[f136]) ).
fof(f136_sk,plain,
! [U,V,W,X] :
( ssAccess(U,authObj(V,W,X))
| ~ ssUserProfile(userProfileEntry(U,authObj(V,W,X))) ),
inference(skolemisation,[status(esa)],[f136_nnf]) ).
cnf(c142,plain,
( ssAccess(X0,authObj(X1,X2,X3))
| ~ ssUserProfile(userProfileEntry(X0,authObj(X1,X2,X3))) ),
inference(cnf_transformation,[status(esa)],[f136_sk]) ).
cnf(p414,plain,
ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)),
inference(resolution,[status(thm)],[p306,c142]) ).
fof(f141,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/sandbox2/benchmark/theBenchmark.p',ax142) ).
fof(f141_nnf,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(nnf_transformation,[status(thm)],[f141]) ).
fof(f141_sk,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(skolemisation,[status(esa)],[f141_nnf]) ).
cnf(c150,plain,
( 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(esa)],[f141_sk]) ).
cnf(p521,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X2))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) ),
inference(resolution,[status(thm)],[p414,c150]) ).
fof(f12,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f12_nnf,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(p203,plain,
( ssUserProfile(userProfileEntry(X0,authObj(ssM_BANF_WRK,ssACTVT,np__1)))
| ~ ssHolds(X0,ssZBANF_WRK_INF_ED) ),
inference(resolution,[status(thm)],[c148,c12]) ).
cnf(p307,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
inference(resolution,[status(thm)],[p203,c113]) ).
cnf(p415,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)),
inference(resolution,[status(thm)],[p307,c142]) ).
cnf(p621,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X2))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0)) ),
inference(resolution,[status(thm)],[p521,p415]) ).
fof(f15,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f15_nnf,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(p206,plain,
( ssUserProfile(userProfileEntry(X0,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))
| ~ ssHolds(X0,ssZBANF_WRK_INF_ED) ),
inference(resolution,[status(thm)],[c148,c15]) ).
cnf(p310,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(resolution,[status(thm)],[p206,c113]) ).
cnf(p418,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)),
inference(resolution,[status(thm)],[p310,c142]) ).
cnf(p638,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X0))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) ),
inference(resolution,[status(thm)],[p621,p418]) ).
fof(f16,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f16_nnf,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(p207,plain,
( ssUserProfile(userProfileEntry(X0,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))
| ~ ssHolds(X0,ssZBANF_WRK_INF_ED) ),
inference(resolution,[status(thm)],[c148,c16]) ).
cnf(p311,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
inference(resolution,[status(thm)],[p207,c113]) ).
fof(f137,axiom,
! [U,V,W,X] :
( ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))
=> ssAccess(U,authObj(V,W,X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax138) ).
fof(f137_nnf,plain,
! [U,V,W,X] :
( ssAccess(U,authObj(V,W,X))
| ~ ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR))) ),
inference(nnf_transformation,[status(thm)],[f137]) ).
fof(f137_sk,plain,
! [U,V,W,X] :
( ssAccess(U,authObj(V,W,X))
| ~ ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR))) ),
inference(skolemisation,[status(esa)],[f137_nnf]) ).
cnf(c143,plain,
( ssAccess(X0,authObj(X1,X2,X3))
| ~ ssUserProfile(userProfileEntry(X0,authObj(X1,X2,ssSTAR))) ),
inference(cnf_transformation,[status(esa)],[f137_sk]) ).
cnf(p420,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,X0)),
inference(resolution,[status(thm)],[p311,c143]) ).
cnf(p653,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X0)) ),
inference(resolution,[status(thm)],[p638,p420]) ).
fof(f17,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
fof(f17_nnf,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(p208,plain,
( ssUserProfile(userProfileEntry(X0,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))
| ~ ssHolds(X0,ssZBANF_WRK_INF_ED) ),
inference(resolution,[status(thm)],[c148,c17]) ).
cnf(p312,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(resolution,[status(thm)],[p208,c113]) ).
cnf(p422,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X0)),
inference(resolution,[status(thm)],[p312,c143]) ).
cnf(p665,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X0))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1)) ),
inference(resolution,[status(thm)],[p653,p422]) ).
fof(f18,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
fof(f18_nnf,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(p209,plain,
( ssUserProfile(userProfileEntry(X0,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))
| ~ ssHolds(X0,ssZBANF_WRK_INF_ED) ),
inference(resolution,[status(thm)],[c148,c18]) ).
cnf(p313,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
inference(resolution,[status(thm)],[p209,c113]) ).
cnf(p424,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,X0)),
inference(resolution,[status(thm)],[p313,c143]) ).
cnf(p674,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X0)) ),
inference(resolution,[status(thm)],[p665,p424]) ).
fof(f19,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f19_nnf,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(p210,plain,
( ssUserProfile(userProfileEntry(X0,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))
| ~ ssHolds(X0,ssZBANF_WRK_INF_ED) ),
inference(resolution,[status(thm)],[c148,c19]) ).
cnf(p314,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(resolution,[status(thm)],[p210,c113]) ).
cnf(p425,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)),
inference(resolution,[status(thm)],[p314,c142]) ).
cnf(p683,plain,
ssAccess(ssMUELLER,ssME51N),
inference(resolution,[status(thm)],[p674,p425]) ).
fof(f154,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/sandbox2/benchmark/theBenchmark.p',ax155) ).
fof(f154_nnf,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(nnf_transformation,[status(thm)],[f154]) ).
fof(f154_sk,plain,
! [Z,X1,X2,V,W,X,Y,X3,X4,U] :
( ( ~ 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(skolemisation,[status(esa)],[f154_nnf]) ).
cnf(c174,plain,
ssRequisition(X5,X6,X7,X1,X2,X3,X4,X8,X9),
inference(cnf_transformation,[status(esa)],[f154_sk]) ).
fof(f148,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/sandbox2/benchmark/theBenchmark.p',ax149) ).
fof(f148_nnf,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(nnf_transformation,[status(thm)],[f148]) ).
fof(f148_sk,plain,
! [W,Z,X1,V,X,X2,Y,X3,X4,U] :
( 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(skolemisation,[status(esa)],[f148_nnf]) ).
cnf(c157,plain,
( ssRequisitionCreated(X0,X2,X5,X6,X1,X3,X7,X4,X8,X9)
| ~ ssAccess(X0,authObj(ssM_BANF_EKG,ssEKGRP,X3))
| ~ ssAccess(X0,authObj(ssM_BANF_BSA,ssBSART,X2))
| ~ ssAccess(X0,authObj(ssM_BANF_WRK,ssWERKS,X1))
| ~ ssAccess(X0,ssME51N)
| ~ ssStandardPurchase(X2)
| ~ ssRequisition(X2,X5,X6,X1,X3,X7,X4,X8,X9) ),
inference(cnf_transformation,[status(esa)],[f148_sk]) ).
cnf(p302,plain,
( 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(resolution,[status(thm)],[c174,c157]) ).
fof(f117,axiom,
ssStandardPurchase(ssNB),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax118) ).
fof(f117_nnf,plain,
ssStandardPurchase(ssNB),
inference(nnf_transformation,[status(thm)],[f117]) ).
cnf(c117,plain,
ssStandardPurchase(ssNB),
inference(cnf_transformation,[status(esa)],[f117_nnf]) ).
cnf(p410,plain,
( 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)],[p302,c117]) ).
cnf(p692,plain,
( ssRequisitionCreated(ssMUELLER,ssNB,X2,X3,X0,X1,X4,X5,X6,X7)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0)) ),
inference(resolution,[status(thm)],[p683,p410]) ).
cnf(p701,plain,
( ssRequisitionCreated(ssMUELLER,ssNB,X1,X2,ssINF,X0,X3,X4,X5,X6)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X0))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB)) ),
inference(resolution,[status(thm)],[p692,p418]) ).
cnf(p710,plain,
( ssRequisitionCreated(ssMUELLER,ssNB,X1,X2,ssINF,X0,X3,X4,X5,X6)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X0)) ),
inference(resolution,[status(thm)],[p701,p422]) ).
cnf(p719,plain,
ssRequisitionCreated(ssMUELLER,ssNB,X0,X1,ssINF,ssI26,X2,X3,X4,X5),
inference(resolution,[status(thm)],[p710,p425]) ).
fof(f157,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/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f157_neg,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)],[f157]) ).
fof(f157_nnf,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(nnf_transformation,[status(thm)],[f157_neg]) ).
fof(f157_sk,plain,
! [Y,Z,X1,U,W,X,X2,X3,V] :
( ~ ssRequisitionCreated(ssMUELLER,Y,Z,X1,ssINF,V,W,X,X2,X3)
& ssRequisition(Y,Z,X1,U,ssINF,W,X,X2,X3) ),
inference(skolemisation,[status(esa)],[f157_nnf]) ).
cnf(c179,plain,
~ ssRequisitionCreated(ssMUELLER,X4,X5,X6,ssINF,X1,X2,X3,X7,X8),
inference(cnf_transformation,[status(esa)],[f157_sk]) ).
cnf(p739,plain,
$false,
inference(resolution,[status(thm)],[p719,c179]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 01:20:35 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 3.09/0.84 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.09/0.84 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------