%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT067+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:53 PM UTC 2026
% Result : Theorem 0.09s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.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 : Mon Sep 21 01:25:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.41 % Refutation found
% 0.09/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.41 fof(f12,axiom,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f13,axiom,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f16,axiom,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f17,axiom,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f18,axiom,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f19,axiom,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f20,axiom,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f114,axiom,(
% 0.09/0.41 ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f118,axiom,(
% 0.09/0.41 ssStandardPurchase(ssNB) ),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f137,axiom,(
% 0.09/0.41 (! [U,V,W,X] :( ssUserProfile(userProfileEntry(U,authObj(V,W,X)))=> ssAccess(U,authObj(V,W,X)) ) )),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f138,axiom,(
% 0.09/0.41 (! [U,V,W,X] :( ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))=> ssAccess(U,authObj(V,W,X)) ) )),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f141,axiom,(
% 0.09/0.41 (! [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))) ) )),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f142,axiom,(
% 0.09/0.41 (! [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) ) )),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f149,axiom,(
% 0.09/0.41 (! [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) ) )),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f155,axiom,(
% 0.09/0.41 ~ (? [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) ) ) )),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f158,conjecture,(
% 0.09/0.41 (? [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) ) )),
% 0.09/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f159,negated_conjecture,(
% 0.09/0.41 ~((? [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) ) ))),
% 0.09/0.41 inference(negated_conjecture,[status(cth)],[f158])).
% 0.09/0.41 fof(f171,plain,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f12])).
% 0.09/0.41 fof(f172,plain,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f13])).
% 0.09/0.41 fof(f175,plain,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f16])).
% 0.09/0.41 fof(f176,plain,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f17])).
% 0.09/0.41 fof(f177,plain,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f18])).
% 0.09/0.41 fof(f178,plain,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f19])).
% 0.09/0.41 fof(f179,plain,(
% 0.09/0.41 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f20])).
% 0.09/0.41 fof(f273,plain,(
% 0.09/0.41 ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f114])).
% 0.09/0.41 fof(f277,plain,(
% 0.09/0.41 ssStandardPurchase(ssNB)),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f118])).
% 0.09/0.41 fof(f311,plain,(
% 0.09/0.41 ![U,V,W,X]: (~ssUserProfile(userProfileEntry(U,authObj(V,W,X)))|ssAccess(U,authObj(V,W,X)))),
% 0.09/0.41 inference(pre_NNF_transformation,[status(thm)],[f137])).
% 0.09/0.41 fof(f312,plain,(
% 0.09/0.41 ![X0,X1,X2,X3]: (~ssUserProfile(userProfileEntry(X0,authObj(X1,X2,X3)))|ssAccess(X0,authObj(X1,X2,X3)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f311])).
% 0.09/0.41 fof(f313,plain,(
% 0.09/0.41 ![U,V,W,X]: (~ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))|ssAccess(U,authObj(V,W,X)))),
% 0.09/0.41 inference(pre_NNF_transformation,[status(thm)],[f138])).
% 0.09/0.41 fof(f314,plain,(
% 0.09/0.41 ![U,V,W]: (~ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))|(![X]: ssAccess(U,authObj(V,W,X))))),
% 0.09/0.41 inference(miniscoping,[status(thm)],[f313])).
% 0.09/0.41 fof(f315,plain,(
% 0.09/0.41 ![X0,X1,X2,X3]: (~ssUserProfile(userProfileEntry(X0,authObj(X1,X2,ssSTAR)))|ssAccess(X0,authObj(X1,X2,X3)))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f314])).
% 0.09/0.41 fof(f321,plain,(
% 0.09/0.41 ![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))))),
% 0.09/0.41 inference(pre_NNF_transformation,[status(thm)],[f141])).
% 0.09/0.41 fof(f322,plain,(
% 0.09/0.41 ![U,Y,Z,X1]: ((((![V]: (~ssProfile(profileEntry(V,authObj(Y,Z,X1)))|~ssHolds(U,V)))&(![W]: (~ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1)))|~ssHolds(U,W))))&(![X]: ((![W]: (~ssCompositeRole(compositeRoleEntry(X,W))|~ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1)))))|~ssHolds(U,X))))|ssUserProfile(userProfileEntry(U,authObj(Y,Z,X1))))),
% 0.09/0.41 inference(miniscoping,[status(thm)],[f321])).
% 0.09/0.41 fof(f324,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4]: (~ssSingleRole(singleRoleEntry(X0,authObj(X1,X2,X3)))|~ssHolds(X4,X0)|ssUserProfile(userProfileEntry(X4,authObj(X1,X2,X3))))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f322])).
% 0.09/0.41 fof(f326,plain,(
% 0.09/0.41 ![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))),
% 0.09/0.41 inference(pre_NNF_transformation,[status(thm)],[f142])).
% 0.09/0.41 fof(f327,plain,(
% 0.09/0.41 ![U]: (((((((~ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__1)))|(![V]: ~ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V))))|~ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1)))|(![W]: ~ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W))))|~ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__1)))|(![X]: ~ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X))))|ssAccess(U,ssME51N))),
% 0.09/0.41 inference(miniscoping,[status(thm)],[f326])).
% 0.09/0.41 fof(f328,plain,(
% 0.09/0.41 ![X0,X1,X2,X3]: (~ssAccess(X0,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(X0,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(X0,authObj(ssM_BANF_WRK,ssWERKS,X1))|~ssAccess(X0,authObj(ssM_BANF_BSA,ssACTVT,np__1))|~ssAccess(X0,authObj(ssM_BANF_BSA,ssBSART,X2))|~ssAccess(X0,authObj(ssM_BANF_EKG,ssACTVT,np__1))|~ssAccess(X0,authObj(ssM_BANF_EKG,ssEKGRP,X3))|ssAccess(X0,ssME51N))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f327])).
% 0.09/0.41 fof(f347,plain,(
% 0.09/0.41 ![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))),
% 0.09/0.41 inference(pre_NNF_transformation,[status(thm)],[f149])).
% 0.09/0.41 fof(f348,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~ssRequisition(X0,X1,X2,X3,X4,X5,X6,X7,X8)|~ssStandardPurchase(X0)|~ssAccess(X9,ssME51N)|~ssAccess(X9,authObj(ssM_BANF_WRK,ssWERKS,X3))|~ssAccess(X9,authObj(ssM_BANF_BSA,ssBSART,X0))|~ssAccess(X9,authObj(ssM_BANF_EKG,ssEKGRP,X4))|ssRequisitionCreated(X9,X0,X1,X2,X3,X4,X5,X6,X7,X8))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f347])).
% 0.09/0.41 fof(f371,plain,(
% 0.09/0.41 (![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))))),
% 0.09/0.41 inference(pre_NNF_transformation,[status(thm)],[f155])).
% 0.09/0.41 fof(f372,plain,(
% 0.09/0.41 (![V,W,X,Y,Z,X1,X2,X3,X4]: ssRequisition(Z,X1,X2,V,W,X,Y,X3,X4))&(![U,V,W,X,Y,Z,X1,X2,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)))),
% 0.09/0.41 inference(miniscoping,[status(thm)],[f371])).
% 0.09/0.41 fof(f373,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (ssRequisition(X0,X1,X2,X3,X4,X5,X6,X7,X8))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f372])).
% 0.09/0.41 fof(f383,plain,(
% 0.09/0.41 (![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)))),
% 0.09/0.41 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 0.09/0.41 fof(f384,plain,(
% 0.09/0.41 (![U,W,X,Y,Z,X1,X2,X3]: ssRequisition(Y,Z,X1,U,ssINF,W,X,X2,X3))&(![V,W,X,Y,Z,X1,X2,X3]: ~ssRequisitionCreated(ssMUELLER,Y,Z,X1,ssINF,V,W,X,X2,X3))),
% 0.09/0.41 inference(miniscoping,[status(thm)],[f383])).
% 0.09/0.41 fof(f386,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ssRequisitionCreated(ssMUELLER,X0,X1,X2,ssINF,X3,X4,X5,X6,X7))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f384])).
% 0.09/0.41 fof(f396,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~ssStandardPurchase(X0)|~ssAccess(X1,ssME51N)|~ssAccess(X1,authObj(ssM_BANF_WRK,ssWERKS,X2))|~ssAccess(X1,authObj(ssM_BANF_BSA,ssBSART,X0))|~ssAccess(X1,authObj(ssM_BANF_EKG,ssEKGRP,X3))|ssRequisitionCreated(X1,X0,X4,X5,X2,X3,X6,X7,X8,X9))),
% 0.09/0.41 inference(backward_subsumption_resolution,[status(thm)],[f348,f373])).
% 0.09/0.41 fof(f400,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~ssAccess(X0,ssME51N)|~ssAccess(X0,authObj(ssM_BANF_WRK,ssWERKS,X1))|~ssAccess(X0,authObj(ssM_BANF_BSA,ssBSART,ssNB))|~ssAccess(X0,authObj(ssM_BANF_EKG,ssEKGRP,X2))|ssRequisitionCreated(X0,ssNB,X3,X4,X1,X2,X5,X6,X7,X8))),
% 0.09/0.41 inference(resolution,[status(thm)],[f277,f396])).
% 0.09/0.41 fof(f405,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4]: (~ssSingleRole(singleRoleEntry(X0,authObj(X1,X2,ssSTAR)))|~ssHolds(X3,X0)|ssAccess(X3,authObj(X1,X2,X4)))),
% 0.09/0.41 inference(resolution,[status(thm)],[f324,f315])).
% 0.09/0.41 fof(f406,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4]: (~ssSingleRole(singleRoleEntry(X0,authObj(X1,X2,X3)))|~ssHolds(X4,X0)|ssAccess(X4,authObj(X1,X2,X3)))),
% 0.09/0.41 inference(resolution,[status(thm)],[f324,f312])).
% 0.09/0.41 fof(f411,plain,(
% 0.09/0.41 ![X0,X1,X2]: (~ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(X0,X1,X2)))|ssAccess(ssMUELLER,authObj(X0,X1,X2)))),
% 0.09/0.41 inference(resolution,[status(thm)],[f406,f273])).
% 0.09/0.41 fof(f412,plain,(
% 0.09/0.41 ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
% 0.09/0.41 inference(resolution,[status(thm)],[f411,f179])).
% 0.09/0.41 fof(f416,plain,(
% 0.09/0.41 ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
% 0.09/0.41 inference(resolution,[status(thm)],[f411,f175])).
% 0.09/0.41 fof(f419,plain,(
% 0.09/0.41 ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
% 0.09/0.41 inference(resolution,[status(thm)],[f411,f172])).
% 0.09/0.41 fof(f420,plain,(
% 0.09/0.41 ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))),
% 0.09/0.41 inference(resolution,[status(thm)],[f411,f171])).
% 0.09/0.41 fof(f435,plain,(
% 0.09/0.41 ![X0,X1,X2]: (~ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(X0,X1,ssSTAR)))|ssAccess(ssMUELLER,authObj(X0,X1,X2)))),
% 0.09/0.41 inference(resolution,[status(thm)],[f405,f273])).
% 0.09/0.41 fof(f436,plain,(
% 0.09/0.41 ![X0]: (ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,X0)))),
% 0.09/0.41 inference(resolution,[status(thm)],[f435,f178])).
% 0.09/0.41 fof(f437,plain,(
% 0.09/0.41 ![X0]: (ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X0)))),
% 0.09/0.41 inference(resolution,[status(thm)],[f435,f177])).
% 0.09/0.41 fof(f438,plain,(
% 0.09/0.41 ![X0]: (ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,X0)))),
% 0.09/0.41 inference(resolution,[status(thm)],[f435,f176])).
% 0.09/0.41 fof(f442,plain,(
% 0.09/0.41 ![X0,X1,X2]: (~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X2))|ssAccess(ssMUELLER,ssME51N))),
% 0.09/0.41 inference(resolution,[status(thm)],[f436,f328])).
% 0.09/0.41 fof(f449,definition,(
% 0.09/0.41 ![X0]: (sQ2_spl <=> (~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0))))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f450,plain,(
% 0.09/0.41 ![X0]: (~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0))|~sQ2_spl)),
% 0.09/0.41 inference(component_clause,[status(thm)],[f449])).
% 0.09/0.41 fof(f458,definition,(
% 0.09/0.41 ![X1]: (sQ5_spl <=> (~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X1))))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f459,plain,(
% 0.09/0.41 ![X0]: (~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X0))|~sQ5_spl)),
% 0.09/0.41 inference(component_clause,[status(thm)],[f458])).
% 0.09/0.41 fof(f461,definition,(
% 0.09/0.41 ![X2]: (sQ6_spl <=> (~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X2))))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f462,plain,(
% 0.09/0.41 ![X0]: (~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X0))|~sQ6_spl)),
% 0.09/0.41 inference(component_clause,[status(thm)],[f461])).
% 0.09/0.41 fof(f494,definition,(
% 0.09/0.41 sQ16_spl <=> (ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f496,plain,(
% 0.09/0.41 ~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))|sQ16_spl),
% 0.09/0.41 inference(component_clause,[status(thm)],[f494])).
% 0.09/0.41 fof(f497,definition,(
% 0.09/0.41 sQ17_spl <=> (ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f499,plain,(
% 0.09/0.41 ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))|sQ17_spl),
% 0.09/0.41 inference(component_clause,[status(thm)],[f497])).
% 0.09/0.41 fof(f500,definition,(
% 0.09/0.41 sQ18_spl <=> (ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f502,plain,(
% 0.09/0.41 ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))|sQ18_spl),
% 0.09/0.41 inference(component_clause,[status(thm)],[f500])).
% 0.09/0.41 fof(f503,definition,(
% 0.09/0.41 sQ19_spl <=> (ssAccess(ssMUELLER,ssME51N))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f504,plain,(
% 0.09/0.41 ssAccess(ssMUELLER,ssME51N)|~sQ19_spl),
% 0.09/0.41 inference(component_clause,[status(thm)],[f503])).
% 0.09/0.41 fof(f506,plain,(
% 0.09/0.41 ~sQ16_spl|~sQ17_spl|sQ2_spl|~sQ18_spl|sQ5_spl|sQ6_spl|sQ19_spl),
% 0.09/0.41 inference(split_clause,[status(thm)],[f442,f494,f497,f449,f500,f458,f461,f503])).
% 0.09/0.41 fof(f507,plain,(
% 0.09/0.41 $false|~sQ6_spl),
% 0.09/0.41 inference(backward_subsumption_resolution,[status(thm)],[f412,f462])).
% 0.09/0.41 fof(f508,plain,(
% 0.09/0.41 ~sQ6_spl),
% 0.09/0.41 inference(contradiction_clause,[status(thm)],[f507])).
% 0.09/0.41 fof(f509,plain,(
% 0.09/0.41 $false|~sQ5_spl),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f459,f437])).
% 0.09/0.41 fof(f510,plain,(
% 0.09/0.41 ~sQ5_spl),
% 0.09/0.41 inference(contradiction_clause,[status(thm)],[f509])).
% 0.09/0.41 fof(f511,plain,(
% 0.09/0.41 $false|~sQ2_spl),
% 0.09/0.41 inference(backward_subsumption_resolution,[status(thm)],[f416,f450])).
% 0.09/0.41 fof(f512,plain,(
% 0.09/0.41 ~sQ2_spl),
% 0.09/0.41 inference(contradiction_clause,[status(thm)],[f511])).
% 0.09/0.41 fof(f519,plain,(
% 0.09/0.41 $false|sQ18_spl),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f502,f438])).
% 0.09/0.41 fof(f520,plain,(
% 0.09/0.41 sQ18_spl),
% 0.09/0.41 inference(contradiction_clause,[status(thm)],[f519])).
% 0.09/0.41 fof(f521,plain,(
% 0.09/0.41 $false|sQ17_spl),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f499,f419])).
% 0.09/0.41 fof(f522,plain,(
% 0.09/0.41 sQ17_spl),
% 0.09/0.41 inference(contradiction_clause,[status(thm)],[f521])).
% 0.09/0.41 fof(f523,plain,(
% 0.09/0.41 $false|sQ16_spl),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f496,f420])).
% 0.09/0.41 fof(f524,plain,(
% 0.09/0.41 sQ16_spl),
% 0.09/0.41 inference(contradiction_clause,[status(thm)],[f523])).
% 0.09/0.41 fof(f529,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB))|~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X1))|ssRequisitionCreated(ssMUELLER,ssNB,X2,X3,X0,X1,X4,X5,X6,X7)|~sQ19_spl)),
% 0.09/0.41 inference(resolution,[status(thm)],[f504,f400])).
% 0.09/0.41 fof(f530,definition,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7]: (sQ20_spl <=> (~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0))|~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X1))|ssRequisitionCreated(ssMUELLER,ssNB,X2,X3,X0,X1,X4,X5,X6,X7)))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f531,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0))|~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X1))|ssRequisitionCreated(ssMUELLER,ssNB,X2,X3,X0,X1,X4,X5,X6,X7)|~sQ20_spl)),
% 0.09/0.41 inference(component_clause,[status(thm)],[f530])).
% 0.09/0.41 fof(f533,definition,(
% 0.09/0.41 sQ21_spl <=> (ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB)))),
% 0.09/0.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.09/0.41 fof(f535,plain,(
% 0.09/0.41 ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssNB))|sQ21_spl),
% 0.09/0.41 inference(component_clause,[status(thm)],[f533])).
% 0.09/0.41 fof(f536,plain,(
% 0.09/0.41 sQ20_spl|~sQ21_spl|~sQ19_spl),
% 0.09/0.41 inference(split_clause,[status(thm)],[f529,f530,f533,f503])).
% 0.09/0.41 fof(f537,plain,(
% 0.09/0.41 $false|sQ21_spl),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f535,f437])).
% 0.09/0.41 fof(f538,plain,(
% 0.09/0.41 sQ21_spl),
% 0.09/0.41 inference(contradiction_clause,[status(thm)],[f537])).
% 0.09/0.41 fof(f677,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5,X6]: (~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X0))|ssRequisitionCreated(ssMUELLER,ssNB,X1,X2,X0,ssI26,X3,X4,X5,X6)|~sQ20_spl)),
% 0.09/0.41 inference(resolution,[status(thm)],[f531,f412])).
% 0.09/0.41 fof(f678,plain,(
% 0.09/0.41 ![X0,X1,X2,X3,X4,X5]: (ssRequisitionCreated(ssMUELLER,ssNB,X0,X1,ssINF,ssI26,X2,X3,X4,X5)|~sQ20_spl)),
% 0.09/0.41 inference(resolution,[status(thm)],[f677,f416])).
% 0.09/0.41 fof(f679,plain,(
% 0.09/0.41 $false|~sQ20_spl),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f678,f386])).
% 0.09/0.41 fof(f680,plain,(
% 0.09/0.41 ~sQ20_spl),
% 0.09/0.41 inference(contradiction_clause,[status(thm)],[f679])).
% 0.09/0.41 fof(f681,plain,(
% 0.09/0.41 $false),
% 0.09/0.41 inference(sat_refutation,[status(thm)],[f506,f508,f510,f512,f520,f522,f524,f536,f538,f680])).
% 0.09/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.44 % Elapsed time: 0.058947 seconds
% 0.09/0.44 % CPU time: 0.189064 seconds
% 0.09/0.44 % Total memory used: 31.371 MB
% 0.09/0.44 % Net memory used: 31.206 MB
%------------------------------------------------------------------------------