%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n005.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:04:37 AM UTC 2026
% Result : Theorem 0.23s 0.55s
% 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.0. Released v5.5.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n005.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 13:51:05 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.23/0.46 start to proof:theBenchmark.p
% 0.23/0.55 % Version : CSI_E---1.1
% 0.23/0.55 % Problem : theBenchmark.p
% 0.23/0.55 % Proof found!
% 0.23/0.55 % SZS status Theorem for theBenchmark.p
% 0.23/0.55 % SZS output start Proof
% 0.23/0.55 fof(ax141, axiom, ![X1, X2, X3, X4, X5, X6, X7]:((((ssProfile(profileEntry(X2,authObj(X5,X6,X7)))&ssHolds(X1,X2))|(ssSingleRole(singleRoleEntry(X3,authObj(X5,X6,X7)))&ssHolds(X1,X3))|((ssCompositeRole(compositeRoleEntry(X4,X3))&ssSingleRole(singleRoleEntry(X3,authObj(X5,X6,X7))))&ssHolds(X1,X4)))=>ssUserProfile(userProfileEntry(X1,authObj(X5,X6,X7))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax141)).
% 0.23/0.55 fof(ax12, axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax12)).
% 0.23/0.55 fof(ax13, axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax13)).
% 0.23/0.55 fof(ax17, axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax17)).
% 0.23/0.55 fof(ax19, axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax19)).
% 0.23/0.55 fof(ax18, axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 0.23/0.55 fof(ax137, axiom, ![X1, X2, X3, X4]:((ssUserProfile(userProfileEntry(X1,authObj(X2,X3,X4)))=>ssAccess(X1,authObj(X2,X3,X4)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax137)).
% 0.23/0.55 fof(ax114, axiom, ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax114)).
% 0.23/0.55 fof(ax138, axiom, ![X1, X2, X3, X4]:((ssUserProfile(userProfileEntry(X1,authObj(X2,X3,ssSTAR)))=>ssAccess(X1,authObj(X2,X3,X4)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax138)).
% 0.23/0.55 fof(ax16, axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax16)).
% 0.23/0.55 fof(ax142, axiom, ![X1, X2, X3, X4]:((((((((ssAccess(X1,authObj(ssS_TCODE,ssTCD,ssME51N))&ssAccess(X1,authObj(ssM_BANF_WRK,ssACTVT,np__1)))&ssAccess(X1,authObj(ssM_BANF_WRK,ssWERKS,X2)))&ssAccess(X1,authObj(ssM_BANF_BSA,ssACTVT,np__1)))&ssAccess(X1,authObj(ssM_BANF_BSA,ssBSART,X3)))&ssAccess(X1,authObj(ssM_BANF_EKG,ssACTVT,np__1)))&ssAccess(X1,authObj(ssM_BANF_EKG,ssEKGRP,X4)))=>ssAccess(X1,ssME51N))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax142)).
% 0.23/0.55 fof(ax20, axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 0.23/0.55 fof(ax149, axiom, ![X1, X2, X3, X4, X5, X6, X7, X8, X9, X10]:(((((((ssRequisition(X3,X6,X7,X2,X4,X8,X5,X9,X10)&ssStandardPurchase(X3))&ssAccess(X1,ssME51N))&ssAccess(X1,authObj(ssM_BANF_WRK,ssWERKS,X2)))&ssAccess(X1,authObj(ssM_BANF_BSA,ssBSART,X3)))&ssAccess(X1,authObj(ssM_BANF_EKG,ssEKGRP,X4)))=>ssRequisitionCreated(X1,X3,X6,X7,X2,X4,X8,X5,X9,X10))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax149)).
% 0.23/0.55 fof(ax155, axiom, ~(?[X1, X2, X3, X4, X5, X6, X7, X8, X9, X10]:((ssRequisition(X6,X7,X8,X2,X3,X4,X5,X9,X10)=>((ssRequisitionCreated(X1,X6,X7,X8,X2,X3,X4,X5,X9,X10)&ssRequisitionReleased(X1,X6,X7,X8,X2,X3,X4,X5,X9,X10))&ssOrderCreated(X1,X6,X7,X8,X2,X3,X4,X5,X9,X10))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax155)).
% 0.23/0.55 fof(co1, conjecture, ?[X1, X2, X3, X4, X5, X6, X7, X8, X9]:((ssRequisition(X5,X6,X7,X1,ssINF,X3,X4,X8,X9)=>ssRequisitionCreated(ssMUELLER,X5,X6,X7,ssINF,X2,X3,X4,X8,X9))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.23/0.55 fof(ax118, axiom, ssStandardPurchase(ssNB), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax118)).
% 0.23/0.55 fof(c_0_16, plain, ![X186, X187, X188, X189, X190, X191, X192]:((((~ssProfile(profileEntry(X187,authObj(X190,X191,X192)))|~ssHolds(X186,X187)|ssUserProfile(userProfileEntry(X186,authObj(X190,X191,X192))))&(~ssSingleRole(singleRoleEntry(X188,authObj(X190,X191,X192)))|~ssHolds(X186,X188)|ssUserProfile(userProfileEntry(X186,authObj(X190,X191,X192)))))&(~ssCompositeRole(compositeRoleEntry(X189,X188))|~ssSingleRole(singleRoleEntry(X188,authObj(X190,X191,X192)))|~ssHolds(X186,X189)|ssUserProfile(userProfileEntry(X186,authObj(X190,X191,X192)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax141])])])])).
% 0.23/0.55 cnf(c_0_17, plain, (ssUserProfile(userProfileEntry(X5,authObj(X2,X3,X4)))|~ssSingleRole(singleRoleEntry(X1,authObj(X2,X3,X4)))|~ssHolds(X5,X1)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.23/0.55 cnf(c_0_18, plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N)))), inference(split_conjunct,[status(thm)],[ax12])).
% 0.23/0.55 cnf(c_0_19, plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1)))), inference(split_conjunct,[status(thm)],[ax13])).
% 0.23/0.55 cnf(c_0_20, plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))), inference(split_conjunct,[status(thm)],[ax17])).
% 0.23/0.55 cnf(c_0_21, plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))), inference(split_conjunct,[status(thm)],[ax19])).
% 0.23/0.55 cnf(c_0_22, plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))), inference(split_conjunct,[status(thm)],[ax18])).
% 0.23/0.55 fof(c_0_23, plain, ![X110, X111, X112, X113]:((~ssUserProfile(userProfileEntry(X110,authObj(X111,X112,X113)))|ssAccess(X110,authObj(X111,X112,X113)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax137])])])).
% 0.23/0.55 cnf(c_0_24, plain, (ssUserProfile(userProfileEntry(X1,authObj(ssS_TCODE,ssTCD,ssME51N)))|~ssHolds(X1,ssZBANF_WRK_INF_ED)), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.23/0.55 cnf(c_0_25, plain, (ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)), inference(split_conjunct,[status(thm)],[ax114])).
% 0.23/0.55 cnf(c_0_26, plain, (ssUserProfile(userProfileEntry(X1,authObj(ssM_BANF_WRK,ssACTVT,np__1)))|~ssHolds(X1,ssZBANF_WRK_INF_ED)), inference(spm,[status(thm)],[c_0_17, c_0_19])).
% 0.23/0.55 fof(c_0_27, plain, ![X114, X115, X116, X117]:((~ssUserProfile(userProfileEntry(X114,authObj(X115,X116,ssSTAR)))|ssAccess(X114,authObj(X115,X116,X117)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax138])])])).
% 0.23/0.55 cnf(c_0_28, plain, (ssUserProfile(userProfileEntry(X1,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))|~ssHolds(X1,ssZBANF_WRK_INF_ED)), inference(spm,[status(thm)],[c_0_17, c_0_20])).
% 0.23/0.55 cnf(c_0_29, plain, (ssUserProfile(userProfileEntry(X1,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))|~ssHolds(X1,ssZBANF_WRK_INF_ED)), inference(spm,[status(thm)],[c_0_17, c_0_21])).
% 0.23/0.55 cnf(c_0_30, plain, (ssUserProfile(userProfileEntry(X1,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))|~ssHolds(X1,ssZBANF_WRK_INF_ED)), inference(spm,[status(thm)],[c_0_17, c_0_22])).
% 0.23/0.55 cnf(c_0_31, plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))), inference(split_conjunct,[status(thm)],[ax16])).
% 0.23/0.55 fof(c_0_32, plain, ![X124, X125, X126, X127]:((~ssAccess(X124,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(X124,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(X124,authObj(ssM_BANF_WRK,ssWERKS,X125))|~ssAccess(X124,authObj(ssM_BANF_BSA,ssACTVT,np__1))|~ssAccess(X124,authObj(ssM_BANF_BSA,ssBSART,X126))|~ssAccess(X124,authObj(ssM_BANF_EKG,ssACTVT,np__1))|~ssAccess(X124,authObj(ssM_BANF_EKG,ssEKGRP,X127))|ssAccess(X124,ssME51N))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax142])])])).
% 0.23/0.55 cnf(c_0_33, plain, (ssAccess(X1,authObj(X2,X3,X4))|~ssUserProfile(userProfileEntry(X1,authObj(X2,X3,X4)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.23/0.55 cnf(c_0_34, plain, (ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)))), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.23/0.55 cnf(c_0_35, plain, (ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)))), inference(spm,[status(thm)],[c_0_26, c_0_25])).
% 0.23/0.55 cnf(c_0_36, plain, (ssAccess(X1,authObj(X2,X3,X4))|~ssUserProfile(userProfileEntry(X1,authObj(X2,X3,ssSTAR)))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.23/0.55 cnf(c_0_37, plain, (ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))), inference(spm,[status(thm)],[c_0_28, c_0_25])).
% 0.23/0.55 cnf(c_0_38, plain, (ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))), inference(spm,[status(thm)],[c_0_29, c_0_25])).
% 0.23/0.55 cnf(c_0_39, plain, (ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))), inference(spm,[status(thm)],[c_0_30, c_0_25])).
% 0.23/0.55 cnf(c_0_40, plain, (ssUserProfile(userProfileEntry(X1,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))|~ssHolds(X1,ssZBANF_WRK_INF_ED)), inference(spm,[status(thm)],[c_0_17, c_0_31])).
% 0.23/0.55 cnf(c_0_41, plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))), inference(split_conjunct,[status(thm)],[ax20])).
% 0.23/0.55 cnf(c_0_42, plain, (ssAccess(X1,ssME51N)|~ssAccess(X1,authObj(ssS_TCODE,ssTCD,ssME51N))|~ssAccess(X1,authObj(ssM_BANF_WRK,ssACTVT,np__1))|~ssAccess(X1,authObj(ssM_BANF_WRK,ssWERKS,X2))|~ssAccess(X1,authObj(ssM_BANF_BSA,ssACTVT,np__1))|~ssAccess(X1,authObj(ssM_BANF_BSA,ssBSART,X3))|~ssAccess(X1,authObj(ssM_BANF_EKG,ssACTVT,np__1))|~ssAccess(X1,authObj(ssM_BANF_EKG,ssEKGRP,X4))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 0.23/0.55 cnf(c_0_43, plain, (ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.23/0.55 cnf(c_0_44, plain, (ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))), inference(spm,[status(thm)],[c_0_33, c_0_35])).
% 0.23/0.55 cnf(c_0_45, plain, (ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,X1))), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.23/0.55 cnf(c_0_46, plain, (ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,X1))), inference(spm,[status(thm)],[c_0_36, c_0_38])).
% 0.23/0.55 cnf(c_0_47, plain, (ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X1))), inference(spm,[status(thm)],[c_0_36, c_0_39])).
% 0.23/0.55 cnf(c_0_48, plain, (ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))), inference(spm,[status(thm)],[c_0_40, c_0_25])).
% 0.23/0.55 cnf(c_0_49, plain, (ssUserProfile(userProfileEntry(X1,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))|~ssHolds(X1,ssZBANF_WRK_INF_ED)), inference(spm,[status(thm)],[c_0_17, c_0_41])).
% 0.23/0.55 fof(c_0_50, plain, ![X25, X26, X27, X28, X29, X30, X31, X32, X33, X34]:((~ssRequisition(X27,X30,X31,X26,X28,X32,X29,X33,X34)|~ssStandardPurchase(X27)|~ssAccess(X25,ssME51N)|~ssAccess(X25,authObj(ssM_BANF_WRK,ssWERKS,X26))|~ssAccess(X25,authObj(ssM_BANF_BSA,ssBSART,X27))|~ssAccess(X25,authObj(ssM_BANF_EKG,ssEKGRP,X28))|ssRequisitionCreated(X25,X27,X30,X31,X26,X28,X32,X29,X33,X34))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax149])])])).
% 0.23/0.55 fof(c_0_51, plain, ![X74, X75, X76, X77, X78, X79, X80, X81, X82, X83]:((ssRequisition(X79,X80,X81,X75,X76,X77,X78,X82,X83)&(~ssRequisitionCreated(X74,X79,X80,X81,X75,X76,X77,X78,X82,X83)|~ssRequisitionReleased(X74,X79,X80,X81,X75,X76,X77,X78,X82,X83)|~ssOrderCreated(X74,X79,X80,X81,X75,X76,X77,X78,X82,X83)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax155])])])).
% 0.23/0.55 cnf(c_0_52, plain, (ssAccess(ssMUELLER,ssME51N)|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X1))|~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_43]), c_0_44]), c_0_45]), c_0_46]), c_0_47])])).
% 0.23/0.55 cnf(c_0_53, plain, (ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))), inference(spm,[status(thm)],[c_0_33, c_0_48])).
% 0.23/0.55 cnf(c_0_54, plain, (ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))), inference(spm,[status(thm)],[c_0_49, c_0_25])).
% 0.23/0.55 cnf(c_0_55, plain, (ssRequisitionCreated(X10,X1,X2,X3,X4,X5,X6,X7,X8,X9)|~ssRequisition(X1,X2,X3,X4,X5,X6,X7,X8,X9)|~ssStandardPurchase(X1)|~ssAccess(X10,ssME51N)|~ssAccess(X10,authObj(ssM_BANF_WRK,ssWERKS,X4))|~ssAccess(X10,authObj(ssM_BANF_BSA,ssBSART,X1))|~ssAccess(X10,authObj(ssM_BANF_EKG,ssEKGRP,X5))), inference(split_conjunct,[status(thm)],[c_0_50])).
% 0.23/0.55 cnf(c_0_56, plain, (ssRequisition(X1,X2,X3,X4,X5,X6,X7,X8,X9)), inference(split_conjunct,[status(thm)],[c_0_51])).
% 0.23/0.55 cnf(c_0_57, plain, (ssAccess(ssMUELLER,ssME51N)|~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X1))), inference(spm,[status(thm)],[c_0_52, c_0_53])).
% 0.23/0.55 cnf(c_0_58, plain, (ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))), inference(spm,[status(thm)],[c_0_33, c_0_54])).
% 0.23/0.55 fof(c_0_59, negated_conjecture, ~(?[X1, X2, X3, X4, X5, X6, X7, X8, X9]:((ssRequisition(X5,X6,X7,X1,ssINF,X3,X4,X8,X9)=>ssRequisitionCreated(ssMUELLER,X5,X6,X7,ssINF,X2,X3,X4,X8,X9)))), inference(assume_negation,[status(cth)],[co1])).
% 0.23/0.55 cnf(c_0_60, plain, (ssRequisitionCreated(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)|~ssAccess(X1,authObj(ssM_BANF_WRK,ssWERKS,X5))|~ssAccess(X1,authObj(ssM_BANF_BSA,ssBSART,X2))|~ssAccess(X1,authObj(ssM_BANF_EKG,ssEKGRP,X6))|~ssAccess(X1,ssME51N)|~ssStandardPurchase(X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_56])])).
% 0.23/0.55 cnf(c_0_61, plain, (ssAccess(ssMUELLER,ssME51N)), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 0.23/0.55 fof(c_0_62, negated_conjecture, ![X16, X17, X18, X19, X20, X21, X22, X23, X24]:((ssRequisition(X20,X21,X22,X16,ssINF,X18,X19,X23,X24)&~ssRequisitionCreated(ssMUELLER,X20,X21,X22,ssINF,X17,X18,X19,X23,X24))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_59])])])).
% 0.23/0.55 cnf(c_0_63, plain, (ssRequisitionCreated(ssMUELLER,X1,X2,X3,X4,X5,X6,X7,X8,X9)|~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X4))|~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X5))|~ssStandardPurchase(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_47])])).
% 0.23/0.55 cnf(c_0_64, negated_conjecture, (~ssRequisitionCreated(ssMUELLER,X1,X2,X3,ssINF,X4,X5,X6,X7,X8)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 0.23/0.55 cnf(c_0_65, plain, (~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X1))|~ssStandardPurchase(X2)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_53]), c_0_64])).
% 0.23/0.55 cnf(c_0_66, plain, (ssStandardPurchase(ssNB)), inference(split_conjunct,[status(thm)],[ax118])).
% 0.23/0.55 cnf(c_0_67, plain, (~ssStandardPurchase(X1)), inference(spm,[status(thm)],[c_0_65, c_0_58])).
% 0.23/0.55 cnf(c_0_68, plain, ($false), inference(sr,[status(thm)],[c_0_66, c_0_67]), ['proof']).
% 0.23/0.55 % SZS output end Proof
% 0.23/0.55 % User time : 0.041 s
% 0.23/0.55 % System time : 0.008 s
% 0.23/0.55 % Total time : 0.049 s
% 0.23/0.55 % User time : 0.046 s
% 0.23/0.55 % System time : 0.011 s
% 0.23/0.55 % Total time : 0.057 s
% 0.23/0.55
%------------------------------------------------------------------------------