%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:18:49 AM UTC 2026
% Result : Theorem 3.17s 3.42s
% Output : CNFRefutation 3.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n028.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 13:53:17 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.41 (re.compile("\."), Token.FullStop),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.41 (re.compile("\("), Token.OpenPar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.41 (re.compile("\)"), Token.ClosePar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.41 (re.compile("\["), Token.OpenSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("~\|"), Token.Nor),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("\|"), Token.Or),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.41 (re.compile("\?"), Token.Existential),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.22/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.32/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.57 """
% 3.17/3.42 % Version: 1.5
% 3.17/3.42 % SZS status Theorem
% 3.17/3.42 % SZS output start CNFRefutation
% 3.17/3.42 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('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 3.17/3.42 fof(c0,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])).
% 3.17/3.42 fof(c1,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(fof_nnf,[status(thm)],[c0])).
% 3.17/3.42 fof(c2,negated_conjecture,((![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)))))))))),inference(shift_quantors,[status(thm)],[c1])).
% 3.17/3.42 fof(c4,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(ssRequisition(X5,X6,X7,X2,ssINF,X3,X4,X8,X9)&~ssRequisitionCreated(ssMUELLER,X13,X14,X15,ssINF,X10,X11,X12,X16,X17)))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,((![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:ssRequisition(X5,X6,X7,X2,ssINF,X3,X4,X8,X9)))))))))&(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:~ssRequisitionCreated(ssMUELLER,X13,X14,X15,ssINF,X10,X11,X12,X16,X17)))))))))),inference(variable_rename,[status(thm)],[c2])).])).
% 3.17/3.42 cnf(c6,negated_conjecture,~ssRequisitionCreated(ssMUELLER,X208,X211,X214,ssINF,X210,X213,X215,X212,X209),inference(split_conjunct,[status(thm)],[c4])).
% 3.17/3.42 fof(ax118,axiom,ssStandardPurchase(ssNB),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax118)).
% 3.17/3.42 cnf(c170,plain,ssStandardPurchase(ssNB),inference(split_conjunct,[status(thm)],[ax118])).
% 3.17/3.42 fof(ax137,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)).
% 3.17/3.42 fof(c111,plain,(![U]:(![V]:(![W]:(![X]:(~ssUserProfile(userProfileEntry(U,authObj(V,W,X)))|ssAccess(U,authObj(V,W,X))))))),inference(fof_nnf,[status(thm)],[ax137])).
% 3.17/3.42 fof(c112,plain,(![X178]:(![X179]:(![X180]:(![X181]:(~ssUserProfile(userProfileEntry(X178,authObj(X179,X180,X181)))|ssAccess(X178,authObj(X179,X180,X181))))))),inference(variable_rename,[status(thm)],[c111])).
% 3.17/3.42 cnf(c113,plain,~ssUserProfile(userProfileEntry(X473,authObj(X471,X472,X474)))|ssAccess(X473,authObj(X471,X472,X474)),inference(split_conjunct,[status(thm)],[c112])).
% 3.17/3.42 fof(ax114,axiom,ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax114)).
% 3.17/3.42 cnf(c174,plain,ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),inference(split_conjunct,[status(thm)],[ax114])).
% 3.17/3.42 fof(ax16,axiom,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 3.17/3.42 cnf(c272,plain,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),inference(split_conjunct,[status(thm)],[ax16])).
% 3.17/3.42 fof(ax141,axiom,(![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/sandbox2/benchmark/theBenchmark.p', ax141)).
% 3.17/3.42 fof(c92,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))))))))))),inference(fof_nnf,[status(thm)],[ax141])).
% 3.17/3.42 fof(c93,plain,(![X161]:(![X162]:(![X163]:(![X164]:(![X165]:(![X166]:(![X167]:((((~ssProfile(profileEntry(X162,authObj(X165,X166,X167)))|~ssHolds(X161,X162))&(~ssSingleRole(singleRoleEntry(X163,authObj(X165,X166,X167)))|~ssHolds(X161,X163)))&((~ssCompositeRole(compositeRoleEntry(X164,X163))|~ssSingleRole(singleRoleEntry(X163,authObj(X165,X166,X167))))|~ssHolds(X161,X164)))|ssUserProfile(userProfileEntry(X161,authObj(X165,X166,X167))))))))))),inference(variable_rename,[status(thm)],[c92])).
% 3.17/3.42 fof(c94,plain,(![X161]:(![X162]:(![X163]:(![X164]:(![X165]:(![X166]:(![X167]:((((~ssProfile(profileEntry(X162,authObj(X165,X166,X167)))|~ssHolds(X161,X162))|ssUserProfile(userProfileEntry(X161,authObj(X165,X166,X167))))&((~ssSingleRole(singleRoleEntry(X163,authObj(X165,X166,X167)))|~ssHolds(X161,X163))|ssUserProfile(userProfileEntry(X161,authObj(X165,X166,X167)))))&(((~ssCompositeRole(compositeRoleEntry(X164,X163))|~ssSingleRole(singleRoleEntry(X163,authObj(X165,X166,X167))))|~ssHolds(X161,X164))|ssUserProfile(userProfileEntry(X161,authObj(X165,X166,X167)))))))))))),inference(distribute,[status(thm)],[c93])).
% 3.17/3.42 cnf(c96,plain,~ssSingleRole(singleRoleEntry(X500,authObj(X501,X499,X498)))|~ssHolds(X497,X500)|ssUserProfile(userProfileEntry(X497,authObj(X501,X499,X498))),inference(split_conjunct,[status(thm)],[c94])).
% 3.17/3.42 cnf(c375,plain,~ssHolds(X650,ssZBANF_WRK_INF_ED)|ssUserProfile(userProfileEntry(X650,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),inference(resolution,[status(thm)],[c96, c272])).
% 3.17/3.42 cnf(c525,plain,ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),inference(resolution,[status(thm)],[c375, c174])).
% 3.17/3.42 cnf(c526,plain,ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)),inference(resolution,[status(thm)],[c525, c113])).
% 3.17/3.42 fof(ax138,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)).
% 3.17/3.42 fof(c106,plain,(![U]:(![V]:(![W]:(![X]:(~ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))|ssAccess(U,authObj(V,W,X))))))),inference(fof_nnf,[status(thm)],[ax138])).
% 3.17/3.42 fof(c107,plain,(![U]:(![V]:(![W]:(~ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR)))|(![X]:ssAccess(U,authObj(V,W,X))))))),inference(shift_quantors,[status(thm)],[c106])).
% 3.17/3.42 fof(c109,plain,(![X174]:(![X175]:(![X176]:(![X177]:(~ssUserProfile(userProfileEntry(X174,authObj(X175,X176,ssSTAR)))|ssAccess(X174,authObj(X175,X176,X177))))))),inference(shift_quantors,[status(thm)],[fof(c108,plain,(![X174]:(![X175]:(![X176]:(~ssUserProfile(userProfileEntry(X174,authObj(X175,X176,ssSTAR)))|(![X177]:ssAccess(X174,authObj(X175,X176,X177))))))),inference(variable_rename,[status(thm)],[c107])).])).
% 3.17/3.42 cnf(c110,plain,~ssUserProfile(userProfileEntry(X475,authObj(X477,X476,ssSTAR)))|ssAccess(X475,authObj(X477,X476,X478)),inference(split_conjunct,[status(thm)],[c109])).
% 3.17/3.42 fof(ax18,axiom,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 3.17/3.42 cnf(c270,plain,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),inference(split_conjunct,[status(thm)],[ax18])).
% 3.17/3.42 cnf(c385,plain,~ssHolds(X660,ssZBANF_WRK_INF_ED)|ssUserProfile(userProfileEntry(X660,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),inference(resolution,[status(thm)],[c96, c270])).
% 3.17/3.42 cnf(c527,plain,ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),inference(resolution,[status(thm)],[c385, c174])).
% 3.17/3.42 cnf(c529,plain,ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X661)),inference(resolution,[status(thm)],[c527, c110])).
% 3.17/3.42 fof(ax20,axiom,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 3.17/3.42 cnf(c268,plain,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),inference(split_conjunct,[status(thm)],[ax20])).
% 3.17/3.42 cnf(c333,plain,~ssHolds(X572,ssZBANF_WRK_INF_ED)|ssUserProfile(userProfileEntry(X572,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),inference(resolution,[status(thm)],[c96, c268])).
% 3.17/3.42 cnf(c506,plain,ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),inference(resolution,[status(thm)],[c333, c174])).
% 3.17/3.42 cnf(c507,plain,ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)),inference(resolution,[status(thm)],[c506, c113])).
% 3.17/3.42 fof(ax155,axiom,(~(?[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/sandbox2/benchmark/theBenchmark.p', ax155)).
% 3.17/3.42 fof(c17,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))))))))))))),inference(fof_nnf,[status(thm)],[ax155])).
% 3.17/3.42 fof(c18,plain,((![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))))))))))))),inference(shift_quantors,[status(thm)],[c17])).
% 3.17/3.42 fof(c20,plain,(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(![X56]:(ssRequisition(X42,X43,X44,X38,X39,X40,X41,X45,X46)&((~ssRequisitionCreated(X47,X52,X53,X54,X48,X49,X50,X51,X55,X56)|~ssRequisitionReleased(X47,X52,X53,X54,X48,X49,X50,X51,X55,X56))|~ssOrderCreated(X47,X52,X53,X54,X48,X49,X50,X51,X55,X56)))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c19,plain,((![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:ssRequisition(X42,X43,X44,X38,X39,X40,X41,X45,X46))))))))))&(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(![X56]:((~ssRequisitionCreated(X47,X52,X53,X54,X48,X49,X50,X51,X55,X56)|~ssRequisitionReleased(X47,X52,X53,X54,X48,X49,X50,X51,X55,X56))|~ssOrderCreated(X47,X52,X53,X54,X48,X49,X50,X51,X55,X56))))))))))))),inference(variable_rename,[status(thm)],[c18])).])).
% 3.17/3.42 cnf(c21,plain,ssRequisition(X241,X236,X240,X242,X239,X234,X235,X238,X237),inference(split_conjunct,[status(thm)],[c20])).
% 3.17/3.42 fof(ax149,axiom,(![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/sandbox2/benchmark/theBenchmark.p', ax149)).
% 3.17/3.42 fof(c54,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)))))))))))),inference(fof_nnf,[status(thm)],[ax149])).
% 3.17/3.42 fof(c55,plain,(![X118]:(![X119]:(![X120]:(![X121]:(![X122]:(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:((((((~ssRequisition(X120,X123,X124,X119,X121,X125,X122,X126,X127)|~ssStandardPurchase(X120))|~ssAccess(X118,ssME51N))|~ssAccess(X118,authObj(ssM_BANF_WRK,ssWERKS,X119)))|~ssAccess(X118,authObj(ssM_BANF_BSA,ssBSART,X120)))|~ssAccess(X118,authObj(ssM_BANF_EKG,ssEKGRP,X121)))|ssRequisitionCreated(X118,X120,X123,X124,X119,X121,X125,X122,X126,X127)))))))))))),inference(variable_rename,[status(thm)],[c54])).
% 3.17/3.42 cnf(c56,plain,~ssRequisition(X446,X444,X448,X440,X441,X443,X449,X442,X445)|~ssStandardPurchase(X446)|~ssAccess(X447,ssME51N)|~ssAccess(X447,authObj(ssM_BANF_WRK,ssWERKS,X440))|~ssAccess(X447,authObj(ssM_BANF_BSA,ssBSART,X446))|~ssAccess(X447,authObj(ssM_BANF_EKG,ssEKGRP,X441))|ssRequisitionCreated(X447,X446,X444,X448,X440,X441,X443,X449,X442,X445),inference(split_conjunct,[status(thm)],[c55])).
% 3.17/3.42 cnf(c290,plain,~ssStandardPurchase(X632)|~ssAccess(X627,ssME51N)|~ssAccess(X627,authObj(ssM_BANF_WRK,ssWERKS,X628))|~ssAccess(X627,authObj(ssM_BANF_BSA,ssBSART,X632))|~ssAccess(X627,authObj(ssM_BANF_EKG,ssEKGRP,X631))|ssRequisitionCreated(X627,X632,X626,X634,X628,X631,X633,X635,X629,X630),inference(resolution,[status(thm)],[c56, c21])).
% 3.17/3.42 cnf(c524,plain,~ssStandardPurchase(X984)|~ssAccess(ssMUELLER,ssME51N)|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X978))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X984))|ssRequisitionCreated(ssMUELLER,X984,X980,X979,X978,ssI26,X977,X983,X981,X982),inference(resolution,[status(thm)],[c290, c507])).
% 3.17/3.42 cnf(c840,plain,~ssStandardPurchase(X991)|~ssAccess(ssMUELLER,ssME51N)|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X987))|ssRequisitionCreated(ssMUELLER,X991,X989,X986,X987,ssI26,X990,X988,X992,X985),inference(resolution,[status(thm)],[c524, c529])).
% 3.17/3.42 cnf(c841,plain,~ssStandardPurchase(X994)|~ssAccess(ssMUELLER,ssME51N)|ssRequisitionCreated(ssMUELLER,X994,X993,X999,ssINF,ssI26,X995,X996,X997,X998),inference(resolution,[status(thm)],[c840, c526])).
% 3.17/3.42 fof(ax12,axiom,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 3.17/3.42 cnf(c276,plain,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),inference(split_conjunct,[status(thm)],[ax12])).
% 3.17/3.42 cnf(c344,plain,~ssHolds(X589,ssZBANF_WRK_INF_ED)|ssUserProfile(userProfileEntry(X589,authObj(ssS_TCODE,ssTCD,ssME51N))),inference(resolution,[status(thm)],[c96, c276])).
% 3.17/3.42 cnf(c513,plain,ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))),inference(resolution,[status(thm)],[c344, c174])).
% 3.17/3.42 cnf(c514,plain,ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)),inference(resolution,[status(thm)],[c513, c113])).
% 3.17/3.42 fof(ax13,axiom,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 3.17/3.42 cnf(c275,plain,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),inference(split_conjunct,[status(thm)],[ax13])).
% 3.17/3.42 cnf(c387,plain,~ssHolds(X663,ssZBANF_WRK_INF_ED)|ssUserProfile(userProfileEntry(X663,authObj(ssM_BANF_WRK,ssACTVT,np__1))),inference(resolution,[status(thm)],[c96, c275])).
% 3.17/3.42 cnf(c530,plain,ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))),inference(resolution,[status(thm)],[c387, c174])).
% 3.17/3.42 cnf(c531,plain,ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)),inference(resolution,[status(thm)],[c530, c113])).
% 3.17/3.42 fof(ax17,axiom,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 3.17/3.42 cnf(c271,plain,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),inference(split_conjunct,[status(thm)],[ax17])).
% 3.17/3.42 cnf(c350,plain,~ssHolds(X602,ssZBANF_WRK_INF_ED)|ssUserProfile(userProfileEntry(X602,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),inference(resolution,[status(thm)],[c96, c271])).
% 3.17/3.42 cnf(c521,plain,ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),inference(resolution,[status(thm)],[c350, c174])).
% 3.17/3.42 cnf(c523,plain,ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,X603)),inference(resolution,[status(thm)],[c521, c110])).
% 3.17/3.42 fof(ax19,axiom,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 3.17/3.42 cnf(c269,plain,ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),inference(split_conjunct,[status(thm)],[ax19])).
% 3.17/3.42 cnf(c349,plain,~ssHolds(X598,ssZBANF_WRK_INF_ED)|ssUserProfile(userProfileEntry(X598,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),inference(resolution,[status(thm)],[c96, c269])).
% 3.17/3.42 cnf(c517,plain,ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),inference(resolution,[status(thm)],[c349, c174])).
% 3.17/3.42 cnf(c519,plain,ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,X599)),inference(resolution,[status(thm)],[c517, c110])).
% 3.17/3.42 fof(ax142,axiom,(![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/sandbox2/benchmark/theBenchmark.p', ax142)).
% 3.17/3.42 fof(c87,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)))))),inference(fof_nnf,[status(thm)],[ax142])).
% 3.17/3.42 fof(c88,plain,(![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))),inference(shift_quantors,[status(thm)],[c87])).
% 3.17/3.42 fof(c90,plain,(![X157]:(![X158]:(![X159]:(![X160]:(((((((~ssAccess(X157,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(X157,authObj(ssM_BANF_WRK,ssACTVT,np__1)))|~ssAccess(X157,authObj(ssM_BANF_WRK,ssWERKS,X158)))|~ssAccess(X157,authObj(ssM_BANF_BSA,ssACTVT,np__1)))|~ssAccess(X157,authObj(ssM_BANF_BSA,ssBSART,X159)))|~ssAccess(X157,authObj(ssM_BANF_EKG,ssACTVT,np__1)))|~ssAccess(X157,authObj(ssM_BANF_EKG,ssEKGRP,X160)))|ssAccess(X157,ssME51N)))))),inference(shift_quantors,[status(thm)],[fof(c89,plain,(![X157]:(((((((~ssAccess(X157,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(X157,authObj(ssM_BANF_WRK,ssACTVT,np__1)))|(![X158]:~ssAccess(X157,authObj(ssM_BANF_WRK,ssWERKS,X158))))|~ssAccess(X157,authObj(ssM_BANF_BSA,ssACTVT,np__1)))|(![X159]:~ssAccess(X157,authObj(ssM_BANF_BSA,ssBSART,X159))))|~ssAccess(X157,authObj(ssM_BANF_EKG,ssACTVT,np__1)))|(![X160]:~ssAccess(X157,authObj(ssM_BANF_EKG,ssEKGRP,X160))))|ssAccess(X157,ssME51N))),inference(variable_rename,[status(thm)],[c88])).])).
% 3.17/3.42 cnf(c91,plain,~ssAccess(X514,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(X514,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(X514,authObj(ssM_BANF_WRK,ssWERKS,X515))|~ssAccess(X514,authObj(ssM_BANF_BSA,ssACTVT,np__1))|~ssAccess(X514,authObj(ssM_BANF_BSA,ssBSART,X513))|~ssAccess(X514,authObj(ssM_BANF_EKG,ssACTVT,np__1))|~ssAccess(X514,authObj(ssM_BANF_EKG,ssEKGRP,X512))|ssAccess(X514,ssME51N),inference(split_conjunct,[status(thm)],[c90])).
% 3.17/3.42 cnf(c510,plain,~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X1045))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X1044))|~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1))|ssAccess(ssMUELLER,ssME51N),inference(resolution,[status(thm)],[c507, c91])).
% 3.17/3.42 cnf(c847,plain,~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X1046))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X1047))|ssAccess(ssMUELLER,ssME51N),inference(resolution,[status(thm)],[c510, c519])).
% 3.17/3.42 cnf(c848,plain,~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X1048))|~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1))|ssAccess(ssMUELLER,ssME51N),inference(resolution,[status(thm)],[c847, c529])).
% 3.17/3.42 cnf(c849,plain,~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X1049))|ssAccess(ssMUELLER,ssME51N),inference(resolution,[status(thm)],[c848, c523])).
% 3.17/3.42 cnf(c850,plain,~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))|ssAccess(ssMUELLER,ssME51N),inference(resolution,[status(thm)],[c849, c526])).
% 3.17/3.42 cnf(c851,plain,~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))|ssAccess(ssMUELLER,ssME51N),inference(resolution,[status(thm)],[c850, c531])).
% 3.17/3.42 cnf(c852,plain,ssAccess(ssMUELLER,ssME51N),inference(resolution,[status(thm)],[c851, c514])).
% 3.17/3.42 cnf(c854,plain,~ssStandardPurchase(X1059)|ssRequisitionCreated(ssMUELLER,X1059,X1057,X1055,ssINF,ssI26,X1056,X1060,X1061,X1058),inference(resolution,[status(thm)],[c852, c841])).
% 3.17/3.42 cnf(c855,plain,ssRequisitionCreated(ssMUELLER,ssNB,X1067,X1065,ssINF,ssI26,X1064,X1066,X1062,X1063),inference(resolution,[status(thm)],[c854, c170])).
% 3.17/3.42 cnf(c858,plain,$false,inference(resolution,[status(thm)],[c855, c6])).
% 3.17/3.42 % SZS output end CNFRefutation
% 3.17/3.42
% 3.17/3.42 % Initial clauses : 180
% 3.17/3.42 % Processed clauses : 715
% 3.17/3.42 % Factors computed : 0
% 3.17/3.42 % Resolvents computed: 580
% 3.17/3.42 % Tautologies deleted: 0
% 3.17/3.42 % Forward subsumed : 14
% 3.17/3.42 % Backward subsumed : 11
% 3.17/3.42 % -------- CPU Time ---------
% 3.17/3.42 % User time : 3.036 s
% 3.17/3.42 % System time : 0.031 s
% 3.17/3.42 % Total time : 3.067 s
%------------------------------------------------------------------------------