%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT067+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 : Sun Sep 27 08:03:03 AM UTC 2026
% Result : Theorem 0.17s 0.50s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 16
% Syntax : Number of formulae : 62 ( 37 unt; 0 def)
% Number of atoms : 143 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 141 ( 60 ~; 56 |; 17 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 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 : 147 ( 56 sgn 29 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax137,axiom,
! [U,V,W,X] :
( ssUserProfile(userProfileEntry(U,authObj(V,W,X)))
=> ssAccess(U,authObj(V,W,X)) ),
file('theBenchmark.p',ax137) ).
fof(ax138,axiom,
! [U,V,W,X] :
( ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))
=> ssAccess(U,authObj(V,W,X)) ),
file('theBenchmark.p',ax138) ).
fof(ax142,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('theBenchmark.p',ax142) ).
fof(ax149,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('theBenchmark.p',ax149) ).
fof(ax155,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('theBenchmark.p',ax155) ).
fof(ax141,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('theBenchmark.p',ax141) ).
fof(co1,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('theBenchmark.p',co1) ).
fof(co1_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(assume_negation,[status(cth)],[co1]) ).
cnf(c_41,plain,
( ssUserProfile(userProfileEntry(E,authObj(B,C,D)))
| ~ ssHolds(E,A)
| ~ ssSingleRole(singleRoleEntry(A,authObj(B,C,D))) ),
inference(clausify,[status(thm)],[ax141]) ).
fof(ax12,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
file('theBenchmark.p',ax12) ).
cnf(c_54,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
inference(clausify,[status(thm)],[ax12]) ).
fof(ax13,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
file('theBenchmark.p',ax13) ).
cnf(c_55,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
inference(clausify,[status(thm)],[ax13]) ).
fof(ax16,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
file('theBenchmark.p',ax16) ).
cnf(c_58,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(clausify,[status(thm)],[ax16]) ).
fof(ax17,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
file('theBenchmark.p',ax17) ).
cnf(c_59,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
inference(clausify,[status(thm)],[ax17]) ).
fof(ax18,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
file('theBenchmark.p',ax18) ).
cnf(c_60,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(clausify,[status(thm)],[ax18]) ).
fof(ax19,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
file('theBenchmark.p',ax19) ).
cnf(c_61,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
inference(clausify,[status(thm)],[ax19]) ).
fof(ax20,axiom,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
file('theBenchmark.p',ax20) ).
cnf(c_62,plain,
ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(clausify,[status(thm)],[ax20]) ).
fof(ax114,axiom,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
file('theBenchmark.p',ax114) ).
cnf(c_153,plain,
ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
inference(clausify,[status(thm)],[ax114]) ).
fof(ax118,axiom,
ssStandardPurchase(ssNB),
file('theBenchmark.p',ax118) ).
cnf(c_155,plain,
ssStandardPurchase(ssNB),
inference(clausify,[status(thm)],[ax118]) ).
cnf(c_172,plain,
( ssAccess(A,authObj(B,C,D))
| ~ ssUserProfile(userProfileEntry(A,authObj(B,C,D))) ),
inference(clausify,[status(thm)],[ax137]) ).
cnf(c_173,plain,
( ssAccess(A,authObj(B,C,D))
| ~ ssUserProfile(userProfileEntry(A,authObj(B,C,ssSTAR))) ),
inference(clausify,[status(thm)],[ax138]) ).
cnf(c_177,plain,
( ssAccess(A,ssME51N)
| ~ ssAccess(A,authObj(ssM_BANF_EKG,ssEKGRP,D))
| ~ ssAccess(A,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(A,authObj(ssM_BANF_BSA,ssBSART,C))
| ~ ssAccess(A,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(A,authObj(ssM_BANF_WRK,ssWERKS,B))
| ~ ssAccess(A,authObj(ssM_BANF_WRK,ssACTVT,np__1))
| ~ ssAccess(A,authObj(ssS_TCODE,ssTCD,ssME51N)) ),
inference(clausify,[status(thm)],[ax142]) ).
cnf(c_183,plain,
( ssRequisitionCreated(V9,A,B,C,D,E,F,V6,V7,V8)
| ~ ssAccess(V9,authObj(ssM_BANF_EKG,ssEKGRP,E))
| ~ ssAccess(V9,authObj(ssM_BANF_BSA,ssBSART,A))
| ~ ssAccess(V9,authObj(ssM_BANF_WRK,ssWERKS,D))
| ~ ssAccess(V9,ssME51N)
| ~ ssStandardPurchase(A)
| ~ ssRequisition(A,B,C,D,E,F,V6,V7,V8) ),
inference(clausify,[status(thm)],[ax149]) ).
cnf(c_200,plain,
ssRequisition(A,B,C,D,E,F,V6,V7,V8),
inference(clausify,[status(thm)],[ax155]) ).
cnf(c_204,negated_conjecture,
~ ssRequisitionCreated(ssMUELLER,A,B,C,ssINF,D,E,F,V6,V7),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_208,plain,
( ssRequisitionCreated(B,A,E,F,C,D,V6,V7,V8,V9)
| ~ ssAccess(B,authObj(ssM_BANF_EKG,ssEKGRP,D))
| ~ ssAccess(B,authObj(ssM_BANF_BSA,ssBSART,A))
| ~ ssAccess(B,authObj(ssM_BANF_WRK,ssWERKS,C))
| ~ ssAccess(B,ssME51N)
| ~ ssStandardPurchase(A) ),
inference(resolve,[status(thm)],[c_200,c_183]) ).
cnf(c_210,plain,
( ssUserProfile(userProfileEntry(ssMUELLER,authObj(A,B,C)))
| ~ ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(A,B,C))) ),
inference(resolve,[status(thm)],[c_153,c_41]) ).
cnf(c_212,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
inference(resolve,[status(thm)],[c_210,c_58]) ).
cnf(c_214,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))),
inference(resolve,[status(thm)],[c_54,c_210]) ).
cnf(c_215,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
inference(resolve,[status(thm)],[c_55,c_210]) ).
cnf(c_218,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
inference(resolve,[status(thm)],[c_59,c_210]) ).
cnf(c_219,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
inference(resolve,[status(thm)],[c_60,c_210]) ).
cnf(c_220,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
inference(resolve,[status(thm)],[c_61,c_210]) ).
cnf(c_221,plain,
ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
inference(resolve,[status(thm)],[c_62,c_210]) ).
cnf(c_223,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)),
inference(resolve,[status(thm)],[c_172,c_221]) ).
cnf(c_229,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)),
inference(resolve,[status(thm)],[c_172,c_215]) ).
cnf(c_230,plain,
ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)),
inference(resolve,[status(thm)],[c_172,c_214]) ).
cnf(c_231,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)),
inference(resolve,[status(thm)],[c_172,c_212]) ).
cnf(c_252,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,B))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,A))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)) ),
inference(resolve,[status(thm)],[c_223,c_177]) ).
cnf(c_253,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,B))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,A))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) ),
inference(resolve,[status(thm)],[c_230,c_252]) ).
cnf(c_233,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,B))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,A)) ),
inference(resolve,[status(thm)],[c_229,c_253]) ).
cnf(c_235,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,A)),
inference(resolve,[status(thm)],[c_173,c_220]) ).
cnf(c_236,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,A)),
inference(resolve,[status(thm)],[c_173,c_219]) ).
cnf(c_237,plain,
ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,A)),
inference(resolve,[status(thm)],[c_173,c_218]) ).
cnf(c_254,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,B))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,A)) ),
inference(resolve,[status(thm)],[c_237,c_233]) ).
cnf(c_255,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,A)) ),
inference(resolve,[status(thm)],[c_236,c_254]) ).
cnf(c_239,plain,
( ssAccess(ssMUELLER,ssME51N)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,A)) ),
inference(resolve,[status(thm)],[c_235,c_255]) ).
cnf(c_256,plain,
( ssRequisitionCreated(ssMUELLER,A,C,D,ssINF,B,E,F,V6,V7)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,B))
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,A))
| ~ ssAccess(ssMUELLER,ssME51N)
| ~ ssStandardPurchase(A) ),
inference(resolve,[status(thm)],[c_231,c_208]) ).
cnf(c_257,plain,
( ssRequisitionCreated(ssMUELLER,A,C,D,ssINF,B,E,F,V6,V7)
| ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,B))
| ~ ssAccess(ssMUELLER,ssME51N)
| ~ ssStandardPurchase(A) ),
inference(resolve,[status(thm)],[c_236,c_256]) ).
cnf(c_242,negated_conjecture,
( ~ ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,B))
| ~ ssAccess(ssMUELLER,ssME51N)
| ~ ssStandardPurchase(A) ),
inference(resolve,[status(thm)],[c_204,c_257]) ).
cnf(c_248,plain,
( ~ ssAccess(ssMUELLER,ssME51N)
| ~ ssStandardPurchase(A) ),
inference(resolve,[status(thm)],[c_242,c_223]) ).
cnf(c_249,plain,
ssAccess(ssMUELLER,ssME51N),
inference(resolve,[status(thm)],[c_239,c_231]) ).
cnf(c_250,plain,
~ ssStandardPurchase(A),
inference(resolve,[status(thm)],[c_249,c_248]) ).
cnf(c_251,plain,
$false,
inference(resolve,[status(thm)],[c_250,c_155]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT067+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n004.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sat Sep 26 00:11:36 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 312698 was started by sandbox2 on n004,
% 0.17/0.44 % Sat Sep 26 00:11:36 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.47
% 0.17/0.47 % From the command line: assign(max_seconds, 300).
% 0.17/0.47
% 0.17/0.47 % SInE: 147 to sos, 10 to usable, of 157 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.17/0.50
% 0.17/0.50 % SZS status Theorem for theBenchmark
% 0.17/0.50
% 0.17/0.50 % Proof 1 at 0.01 (+ 0.01) seconds.
% 0.17/0.50 % Length of proof is 46.
% 0.17/0.50 % Level of proof is 9.
% 0.17/0.50 % Maximum clause weight is 228.000.
% 0.17/0.50 % Given clauses 186.
% 0.17/0.50
% 0.17/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------