%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT046+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n010.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:34 AM UTC 2026
% Result : Theorem 0.23s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT046+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.36 % Computer : n010.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 7 13:10:26 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.23/0.48 start to proof:theBenchmark.p
% 0.23/0.56 % Version : CSI_E---1.1
% 0.23/0.56 % Problem : theBenchmark.p
% 0.23/0.56 % Proof found!
% 0.23/0.56 % SZS status Theorem for theBenchmark.p
% 0.23/0.56 % SZS output start Proof
% 0.23/0.56 fof(assumption_4, axiom, ![X1, X5, X4]:((((organization(X1)&~(has_immunity(X1,X5)))&~(has_immunity(X1,X4)))=>((((greater(capability(X1,X4),capability(X1,X5))&greater_or_equal(position(X1,X4),position(X1,X5)))=>smaller(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))&((greater_or_equal(capability(X1,X4),capability(X1,X5))&greater(position(X1,X4),position(X1,X5)))=>smaller(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5))))&((capability(X1,X4)=capability(X1,X5)&position(X1,X4)=position(X1,X5))=>hazard_of_mortality(X1,X4)=hazard_of_mortality(X1,X5))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_4)).
% 0.23/0.56 fof(theorem_1, conjecture, ![X1, X5, X4]:((((organization(X1)&~(has_endowment(X1)))&greater(age(X1,X4),age(X1,X5)))=>smaller(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', theorem_1)).
% 0.56/0.56 fof(assumption_1, axiom, ![X1, X4]:(((organization(X1)&~(has_endowment(X1)))=>~(has_immunity(X1,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_1)).
% 0.56/0.56 fof(assumption_6, axiom, ![X1, X5, X4]:((organization(X1)=>((greater(external_ties(X1,X4),external_ties(X1,X5))=>greater(position(X1,X4),position(X1,X5)))&(external_ties(X1,X4)=external_ties(X1,X5)=>position(X1,X4)=position(X1,X5))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_6)).
% 0.56/0.56 fof(assumption_8, axiom, ![X1, X5, X4]:(((organization(X1)&greater(age(X1,X4),age(X1,X5)))=>greater(external_ties(X1,X4),external_ties(X1,X5)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_8)).
% 0.56/0.56 fof(assumption_5, axiom, ![X1, X5, X4]:((organization(X1)=>((((greater(stock_of_knowledge(X1,X4),stock_of_knowledge(X1,X5))&smaller_or_equal(internal_friction(X1,X4),internal_friction(X1,X5)))=>greater(capability(X1,X4),capability(X1,X5)))&((smaller_or_equal(stock_of_knowledge(X1,X4),stock_of_knowledge(X1,X5))&greater(internal_friction(X1,X4),internal_friction(X1,X5)))=>smaller(capability(X1,X4),capability(X1,X5))))&((stock_of_knowledge(X1,X4)=stock_of_knowledge(X1,X5)&internal_friction(X1,X4)=internal_friction(X1,X5))=>capability(X1,X4)=capability(X1,X5))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_5)).
% 0.56/0.56 fof(assumption_9, axiom, ![X1, X5, X4]:((organization(X1)=>internal_friction(X1,X4)=internal_friction(X1,X5))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_9)).
% 0.56/0.56 fof(assumption_7, axiom, ![X1, X5, X4]:(((organization(X1)&greater(age(X1,X4),age(X1,X5)))=>greater(stock_of_knowledge(X1,X4),stock_of_knowledge(X1,X5)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_7)).
% 0.56/0.56 fof(definition_greater_or_equal, axiom, ![X1, X2]:((greater_or_equal(X1,X2)<=>(greater(X1,X2)|X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', definition_greater_or_equal)).
% 0.56/0.56 fof(definition_smaller_or_equal, axiom, ![X1, X2]:((smaller_or_equal(X1,X2)<=>(smaller(X1,X2)|X1=X2))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', definition_smaller_or_equal)).
% 0.56/0.56 fof(c_0_10, plain, ![X1, X4, X5]:((epred1_3(X5,X4,X1)<=>((((greater(capability(X1,X4),capability(X1,X5))&greater_or_equal(position(X1,X4),position(X1,X5)))=>smaller(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))&((greater_or_equal(capability(X1,X4),capability(X1,X5))&greater(position(X1,X4),position(X1,X5)))=>smaller(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5))))&((capability(X1,X4)=capability(X1,X5)&position(X1,X4)=position(X1,X5))=>hazard_of_mortality(X1,X4)=hazard_of_mortality(X1,X5))))), introduced(definition)).
% 0.56/0.56 fof(c_0_11, plain, ![X1, X5, X4]:((((organization(X1)&~has_immunity(X1,X5))&~has_immunity(X1,X4))=>epred1_3(X5,X4,X1))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[assumption_4]), c_0_10])).
% 0.56/0.56 fof(c_0_12, negated_conjecture, ~(![X1, X5, X4]:((((organization(X1)&~has_endowment(X1))&greater(age(X1,X4),age(X1,X5)))=>smaller(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[theorem_1])])).
% 0.56/0.56 fof(c_0_13, plain, ![X1, X4]:(((organization(X1)&~has_endowment(X1))=>~has_immunity(X1,X4))), inference(fof_simplification,[status(thm)],[assumption_1])).
% 0.56/0.56 fof(c_0_14, plain, ![X21, X22, X23]:((~organization(X21)|has_immunity(X21,X22)|has_immunity(X21,X23)|epred1_3(X22,X23,X21))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])).
% 0.56/0.56 fof(c_0_15, negated_conjecture, (((organization(esk1_0)&~has_endowment(esk1_0))&greater(age(esk1_0,esk3_0),age(esk1_0,esk2_0)))&~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])])).
% 0.56/0.56 fof(c_0_16, plain, ![X19, X20]:((~organization(X19)|has_endowment(X19)|~has_immunity(X19,X20))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])])).
% 0.56/0.56 cnf(c_0_17, plain, (has_immunity(X1,X2)|has_immunity(X1,X3)|epred1_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.56/0.56 cnf(c_0_18, negated_conjecture, (organization(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.56/0.56 fof(c_0_19, plain, ![X27, X28, X29]:(((~greater(external_ties(X27,X29),external_ties(X27,X28))|greater(position(X27,X29),position(X27,X28))|~organization(X27))&(external_ties(X27,X29)!=external_ties(X27,X28)|position(X27,X29)=position(X27,X28)|~organization(X27)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_6])])])])).
% 0.56/0.56 fof(c_0_20, plain, ![X33, X34, X35]:((~organization(X33)|~greater(age(X33,X35),age(X33,X34))|greater(external_ties(X33,X35),external_ties(X33,X34)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_8])])])).
% 0.56/0.56 fof(c_0_21, plain, ![X1, X4, X5]:((epred2_3(X5,X4,X1)<=>((((greater(stock_of_knowledge(X1,X4),stock_of_knowledge(X1,X5))&smaller_or_equal(internal_friction(X1,X4),internal_friction(X1,X5)))=>greater(capability(X1,X4),capability(X1,X5)))&((smaller_or_equal(stock_of_knowledge(X1,X4),stock_of_knowledge(X1,X5))&greater(internal_friction(X1,X4),internal_friction(X1,X5)))=>smaller(capability(X1,X4),capability(X1,X5))))&((stock_of_knowledge(X1,X4)=stock_of_knowledge(X1,X5)&internal_friction(X1,X4)=internal_friction(X1,X5))=>capability(X1,X4)=capability(X1,X5))))), introduced(definition)).
% 0.56/0.56 fof(c_0_22, plain, ![X1, X4, X5]:((epred1_3(X5,X4,X1)=>((((greater(capability(X1,X4),capability(X1,X5))&greater_or_equal(position(X1,X4),position(X1,X5)))=>smaller(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))&((greater_or_equal(capability(X1,X4),capability(X1,X5))&greater(position(X1,X4),position(X1,X5)))=>smaller(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5))))&((capability(X1,X4)=capability(X1,X5)&position(X1,X4)=position(X1,X5))=>hazard_of_mortality(X1,X4)=hazard_of_mortality(X1,X5))))), inference(split_equiv,[status(thm)],[c_0_10])).
% 0.56/0.56 cnf(c_0_23, plain, (has_endowment(X1)|~organization(X1)|~has_immunity(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.56/0.56 cnf(c_0_24, negated_conjecture, (epred1_3(X1,X2,esk1_0)|has_immunity(esk1_0,X1)|has_immunity(esk1_0,X2)), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.56/0.56 cnf(c_0_25, negated_conjecture, (~has_endowment(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.56/0.56 cnf(c_0_26, plain, (greater(position(X1,X2),position(X1,X3))|~greater(external_ties(X1,X2),external_ties(X1,X3))|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.56/0.56 cnf(c_0_27, plain, (greater(external_ties(X1,X2),external_ties(X1,X3))|~organization(X1)|~greater(age(X1,X2),age(X1,X3))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.56/0.56 fof(c_0_28, plain, ![X1, X4, X5]:((epred2_3(X5,X4,X1)=>((((greater(stock_of_knowledge(X1,X4),stock_of_knowledge(X1,X5))&smaller_or_equal(internal_friction(X1,X4),internal_friction(X1,X5)))=>greater(capability(X1,X4),capability(X1,X5)))&((smaller_or_equal(stock_of_knowledge(X1,X4),stock_of_knowledge(X1,X5))&greater(internal_friction(X1,X4),internal_friction(X1,X5)))=>smaller(capability(X1,X4),capability(X1,X5))))&((stock_of_knowledge(X1,X4)=stock_of_knowledge(X1,X5)&internal_friction(X1,X4)=internal_friction(X1,X5))=>capability(X1,X4)=capability(X1,X5))))), inference(split_equiv,[status(thm)],[c_0_21])).
% 0.56/0.56 fof(c_0_29, axiom, ![X1, X5, X4]:((organization(X1)=>epred2_3(X5,X4,X1))), inference(apply_def,[status(thm)],[assumption_5, c_0_21])).
% 0.56/0.56 fof(c_0_30, plain, ![X42, X43, X44]:((((~greater(capability(X42,X43),capability(X42,X44))|~greater_or_equal(position(X42,X43),position(X42,X44))|smaller(hazard_of_mortality(X42,X43),hazard_of_mortality(X42,X44))|~epred1_3(X44,X43,X42))&(~greater_or_equal(capability(X42,X43),capability(X42,X44))|~greater(position(X42,X43),position(X42,X44))|smaller(hazard_of_mortality(X42,X43),hazard_of_mortality(X42,X44))|~epred1_3(X44,X43,X42)))&(capability(X42,X43)!=capability(X42,X44)|position(X42,X43)!=position(X42,X44)|hazard_of_mortality(X42,X43)=hazard_of_mortality(X42,X44)|~epred1_3(X44,X43,X42)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_22])])])])).
% 0.56/0.56 cnf(c_0_31, negated_conjecture, (epred1_3(X1,X2,esk1_0)|has_immunity(esk1_0,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_18])]), c_0_25])).
% 0.56/0.56 cnf(c_0_32, plain, (greater(position(X1,X2),position(X1,X3))|~organization(X1)|~greater(age(X1,X2),age(X1,X3))), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 0.56/0.56 cnf(c_0_33, negated_conjecture, (greater(age(esk1_0,esk3_0),age(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.56/0.56 fof(c_0_34, plain, ![X45, X46, X47]:((((~greater(stock_of_knowledge(X45,X46),stock_of_knowledge(X45,X47))|~smaller_or_equal(internal_friction(X45,X46),internal_friction(X45,X47))|greater(capability(X45,X46),capability(X45,X47))|~epred2_3(X47,X46,X45))&(~smaller_or_equal(stock_of_knowledge(X45,X46),stock_of_knowledge(X45,X47))|~greater(internal_friction(X45,X46),internal_friction(X45,X47))|smaller(capability(X45,X46),capability(X45,X47))|~epred2_3(X47,X46,X45)))&(stock_of_knowledge(X45,X46)!=stock_of_knowledge(X45,X47)|internal_friction(X45,X46)!=internal_friction(X45,X47)|capability(X45,X46)=capability(X45,X47)|~epred2_3(X47,X46,X45)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])])])])).
% 0.56/0.56 fof(c_0_35, plain, ![X36, X37, X38]:((~organization(X36)|internal_friction(X36,X38)=internal_friction(X36,X37))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_9])])])).
% 0.56/0.56 fof(c_0_36, plain, ![X24, X25, X26]:((~organization(X24)|epred2_3(X25,X26,X24))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_29])])])).
% 0.56/0.56 fof(c_0_37, plain, ![X30, X31, X32]:((~organization(X30)|~greater(age(X30,X32),age(X30,X31))|greater(stock_of_knowledge(X30,X32),stock_of_knowledge(X30,X31)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_7])])])).
% 0.56/0.56 cnf(c_0_38, negated_conjecture, (~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.56/0.56 cnf(c_0_39, plain, (smaller(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~greater_or_equal(capability(X1,X2),capability(X1,X3))|~greater(position(X1,X2),position(X1,X3))|~epred1_3(X3,X2,X1)), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.56/0.56 cnf(c_0_40, negated_conjecture, (epred1_3(X1,X2,esk1_0)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_31]), c_0_18])]), c_0_25])).
% 0.56/0.56 cnf(c_0_41, negated_conjecture, (greater(position(esk1_0,esk3_0),position(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_18])])).
% 0.56/0.56 fof(c_0_42, plain, ![X8, X9]:(((~greater_or_equal(X8,X9)|(greater(X8,X9)|X8=X9))&((~greater(X8,X9)|greater_or_equal(X8,X9))&(X8!=X9|greater_or_equal(X8,X9))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_greater_or_equal])])])])).
% 0.56/0.56 cnf(c_0_43, plain, (greater(capability(X1,X2),capability(X1,X3))|~greater(stock_of_knowledge(X1,X2),stock_of_knowledge(X1,X3))|~smaller_or_equal(internal_friction(X1,X2),internal_friction(X1,X3))|~epred2_3(X3,X2,X1)), inference(split_conjunct,[status(thm)],[c_0_34])).
% 0.56/0.56 cnf(c_0_44, plain, (internal_friction(X1,X2)=internal_friction(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.56/0.56 cnf(c_0_45, plain, (epred2_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_36])).
% 0.56/0.56 cnf(c_0_46, plain, (greater(stock_of_knowledge(X1,X2),stock_of_knowledge(X1,X3))|~organization(X1)|~greater(age(X1,X2),age(X1,X3))), inference(split_conjunct,[status(thm)],[c_0_37])).
% 0.56/0.56 cnf(c_0_47, negated_conjecture, (~greater_or_equal(capability(esk1_0,esk3_0),capability(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_40]), c_0_41])])).
% 0.56/0.56 cnf(c_0_48, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_42])).
% 0.56/0.56 fof(c_0_49, plain, ![X6, X7]:(((~smaller_or_equal(X6,X7)|(smaller(X6,X7)|X6=X7))&((~smaller(X6,X7)|smaller_or_equal(X6,X7))&(X6!=X7|smaller_or_equal(X6,X7))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller_or_equal])])])])).
% 0.56/0.56 cnf(c_0_50, plain, (greater(capability(X1,X2),capability(X1,X3))|~organization(X1)|~greater(stock_of_knowledge(X1,X2),stock_of_knowledge(X1,X3))|~smaller_or_equal(internal_friction(X1,X2),internal_friction(X1,X4))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_45])).
% 0.56/0.56 cnf(c_0_51, negated_conjecture, (greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_33]), c_0_18])])).
% 0.56/0.56 cnf(c_0_52, negated_conjecture, (~greater(capability(esk1_0,esk3_0),capability(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 0.56/0.56 cnf(c_0_53, plain, (smaller_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_49])).
% 0.56/0.56 cnf(c_0_54, negated_conjecture, (~smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,X1))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_18])]), c_0_52])).
% 0.56/0.56 cnf(c_0_55, plain, (smaller_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_53])).
% 0.56/0.56 cnf(c_0_56, negated_conjecture, ($false), inference(spm,[status(thm)],[c_0_54, c_0_55]), ['proof']).
% 0.56/0.56 % SZS output end Proof
% 0.56/0.56 % User time : 0.019 s
% 0.56/0.56 % System time : 0.004 s
% 0.56/0.56 % Total time : 0.023 s
% 0.56/0.56 % User time : 0.086 s
% 0.56/0.56 % System time : 0.008 s
% 0.56/0.56 % Total time : 0.094 s
% 0.56/0.56
%------------------------------------------------------------------------------