%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT047+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% 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 : Tue Sep 8 06:04:34 AM UTC 2026
% Result : Theorem 1.09s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT047+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 13:12:11 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.24/0.47 start to proof:theBenchmark.p
% 1.09/0.66 % Version : CSI_E---1.1
% 1.09/0.66 % Problem : theBenchmark.p
% 1.09/0.66 % Proof found!
% 1.09/0.66 % SZS status Theorem for theBenchmark.p
% 1.09/0.66 % SZS output start Proof
% 1.09/0.66 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)).
% 1.09/0.66 fof(definition_smaller, axiom, ![X1, X2]:((smaller(X1,X2)<=>greater(X2,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', definition_smaller)).
% 1.09/0.66 fof(meaning_postulate_greater_comparable, axiom, ![X1, X2]:((smaller(X1,X2)|X1=X2|greater(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_comparable)).
% 1.09/0.66 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)).
% 1.09/0.66 fof(definition_1, axiom, ![X1]:((has_endowment(X1)<=>![X4]:(((organization(X1)&(smaller_or_equal(age(X1,X4),eta)=>has_immunity(X1,X4)))&(greater(age(X1,X4),eta)=>~(has_immunity(X1,X4))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', definition_1)).
% 1.09/0.66 fof(theorem_2, conjecture, ![X1, X5, X6, X7, X8]:(((((((organization(X1)&has_endowment(X1))&smaller_or_equal(age(X1,X5),age(X1,X6)))&smaller_or_equal(age(X1,X6),eta))&greater(age(X1,X7),eta))&greater(age(X1,X8),age(X1,X7)))=>((greater(hazard_of_mortality(X1,X7),hazard_of_mortality(X1,X8))&greater(hazard_of_mortality(X1,X8),hazard_of_mortality(X1,X6)))&hazard_of_mortality(X1,X6)=hazard_of_mortality(X1,X5)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', theorem_2)).
% 1.09/0.66 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)).
% 1.09/0.66 fof(meaning_postulate_greater_transitive, axiom, ![X1, X2, X3]:(((greater(X1,X2)&greater(X2,X3))=>greater(X1,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_transitive)).
% 1.09/0.66 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)).
% 1.09/0.66 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)).
% 1.09/0.66 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)).
% 1.09/0.66 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)).
% 1.09/0.66 fof(assumption_2, axiom, ![X1, X5, X4]:((((organization(X1)&has_immunity(X1,X5))&has_immunity(X1,X4))=>hazard_of_mortality(X1,X5)=hazard_of_mortality(X1,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_2)).
% 1.09/0.66 fof(assumption_3, axiom, ![X1, X5, X4]:((((organization(X1)&has_immunity(X1,X5))&~(has_immunity(X1,X4)))=>greater(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_3)).
% 1.09/0.66 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)).
% 1.09/0.66 fof(meaning_postulate_greater_strict, axiom, ![X1, X2]:(~((greater(X1,X2)&greater(X2,X1)))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_strict)).
% 1.09/0.66 fof(c_0_16, 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)).
% 1.09/0.66 fof(c_0_17, 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)).
% 1.09/0.66 fof(c_0_18, 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_16])).
% 1.09/0.66 fof(c_0_19, axiom, ![X1, X5, X4]:((organization(X1)=>epred2_3(X5,X4,X1))), inference(apply_def,[status(thm)],[assumption_5, c_0_16])).
% 1.09/0.66 fof(c_0_20, plain, ![X13, X14]:(((~smaller(X13,X14)|greater(X14,X13))&(~greater(X14,X13)|smaller(X13,X14)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller])])])).
% 1.09/0.66 fof(c_0_21, plain, ![X20, X21]:((smaller(X20,X21)|X20=X21|greater(X20,X21))), inference(variable_rename,[status(thm)],[meaning_postulate_greater_comparable])).
% 1.09/0.66 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_17])).
% 1.09/0.66 fof(c_0_23, plain, ![X60, X61, X62]:((((~greater(stock_of_knowledge(X60,X61),stock_of_knowledge(X60,X62))|~smaller_or_equal(internal_friction(X60,X61),internal_friction(X60,X62))|greater(capability(X60,X61),capability(X60,X62))|~epred2_3(X62,X61,X60))&(~smaller_or_equal(stock_of_knowledge(X60,X61),stock_of_knowledge(X60,X62))|~greater(internal_friction(X60,X61),internal_friction(X60,X62))|smaller(capability(X60,X61),capability(X60,X62))|~epred2_3(X62,X61,X60)))&(stock_of_knowledge(X60,X61)!=stock_of_knowledge(X60,X62)|internal_friction(X60,X61)!=internal_friction(X60,X62)|capability(X60,X61)=capability(X60,X62)|~epred2_3(X62,X61,X60)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])])])).
% 1.09/0.66 fof(c_0_24, plain, ![X49, X50, X51]:((~organization(X49)|internal_friction(X49,X51)=internal_friction(X49,X50))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_9])])])).
% 1.09/0.66 fof(c_0_25, plain, ![X37, X38, X39]:((~organization(X37)|epred2_3(X38,X39,X37))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])).
% 1.09/0.66 fof(c_0_26, plain, ![X1]:((has_endowment(X1)<=>![X4]:(((organization(X1)&(smaller_or_equal(age(X1,X4),eta)=>has_immunity(X1,X4)))&(greater(age(X1,X4),eta)=>~has_immunity(X1,X4)))))), inference(fof_simplification,[status(thm)],[definition_1])).
% 1.09/0.66 fof(c_0_27, negated_conjecture, ~(![X1, X5, X6, X7, X8]:(((((((organization(X1)&has_endowment(X1))&smaller_or_equal(age(X1,X5),age(X1,X6)))&smaller_or_equal(age(X1,X6),eta))&greater(age(X1,X7),eta))&greater(age(X1,X8),age(X1,X7)))=>((greater(hazard_of_mortality(X1,X7),hazard_of_mortality(X1,X8))&greater(hazard_of_mortality(X1,X8),hazard_of_mortality(X1,X6)))&hazard_of_mortality(X1,X6)=hazard_of_mortality(X1,X5))))), inference(assume_negation,[status(cth)],[theorem_2])).
% 1.09/0.66 fof(c_0_28, plain, ![X9, X10]:(((~smaller_or_equal(X9,X10)|(smaller(X9,X10)|X9=X10))&((~smaller(X9,X10)|smaller_or_equal(X9,X10))&(X9!=X10|smaller_or_equal(X9,X10))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller_or_equal])])])])).
% 1.09/0.66 fof(c_0_29, plain, ![X17, X18, X19]:((~greater(X17,X18)|~greater(X18,X19)|greater(X17,X19))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[meaning_postulate_greater_transitive])])])).
% 1.09/0.66 cnf(c_0_30, plain, (greater(X2,X1)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 1.09/0.66 cnf(c_0_31, plain, (smaller(X1,X2)|X1=X2|greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.09/0.66 fof(c_0_32, plain, ![X57, X58, X59]:((((~greater(capability(X57,X58),capability(X57,X59))|~greater_or_equal(position(X57,X58),position(X57,X59))|smaller(hazard_of_mortality(X57,X58),hazard_of_mortality(X57,X59))|~epred1_3(X59,X58,X57))&(~greater_or_equal(capability(X57,X58),capability(X57,X59))|~greater(position(X57,X58),position(X57,X59))|smaller(hazard_of_mortality(X57,X58),hazard_of_mortality(X57,X59))|~epred1_3(X59,X58,X57)))&(capability(X57,X58)!=capability(X57,X59)|position(X57,X58)!=position(X57,X59)|hazard_of_mortality(X57,X58)=hazard_of_mortality(X57,X59)|~epred1_3(X59,X58,X57)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_22])])])])).
% 1.09/0.66 fof(c_0_33, plain, ![X11, X12]:(((~greater_or_equal(X11,X12)|(greater(X11,X12)|X11=X12))&((~greater(X11,X12)|greater_or_equal(X11,X12))&(X11!=X12|greater_or_equal(X11,X12))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_greater_or_equal])])])])).
% 1.09/0.66 fof(c_0_34, plain, ![X40, X41, X42]:(((~greater(external_ties(X40,X42),external_ties(X40,X41))|greater(position(X40,X42),position(X40,X41))|~organization(X40))&(external_ties(X40,X42)!=external_ties(X40,X41)|position(X40,X42)=position(X40,X41)|~organization(X40)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_6])])])])).
% 1.09/0.66 fof(c_0_35, plain, ![X46, X47, X48]:((~organization(X46)|~greater(age(X46,X48),age(X46,X47))|greater(external_ties(X46,X48),external_ties(X46,X47)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_8])])])).
% 1.09/0.66 cnf(c_0_36, 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_23])).
% 1.09/0.66 cnf(c_0_37, plain, (internal_friction(X1,X2)=internal_friction(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 1.09/0.66 cnf(c_0_38, plain, (epred2_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 1.09/0.66 fof(c_0_39, plain, ![X43, X44, X45]:((~organization(X43)|~greater(age(X43,X45),age(X43,X44))|greater(stock_of_knowledge(X43,X45),stock_of_knowledge(X43,X44)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_7])])])).
% 1.09/0.66 fof(c_0_40, plain, ![X22, X23, X24, X25]:(((((organization(X22)|~has_endowment(X22))&(~smaller_or_equal(age(X22,X23),eta)|has_immunity(X22,X23)|~has_endowment(X22)))&(~greater(age(X22,X24),eta)|~has_immunity(X22,X24)|~has_endowment(X22)))&(((greater(age(X25,esk2_1(X25)),eta)|(smaller_or_equal(age(X25,esk1_1(X25)),eta)|~organization(X25))|has_endowment(X25))&(has_immunity(X25,esk2_1(X25))|(smaller_or_equal(age(X25,esk1_1(X25)),eta)|~organization(X25))|has_endowment(X25)))&((greater(age(X25,esk2_1(X25)),eta)|(~has_immunity(X25,esk1_1(X25))|~organization(X25))|has_endowment(X25))&(has_immunity(X25,esk2_1(X25))|(~has_immunity(X25,esk1_1(X25))|~organization(X25))|has_endowment(X25)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_26])])])])])])])).
% 1.09/0.66 fof(c_0_41, negated_conjecture, ((((((organization(esk3_0)&has_endowment(esk3_0))&smaller_or_equal(age(esk3_0,esk4_0),age(esk3_0,esk5_0)))&smaller_or_equal(age(esk3_0,esk5_0),eta))&greater(age(esk3_0,esk6_0),eta))&greater(age(esk3_0,esk7_0),age(esk3_0,esk6_0)))&(~greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk7_0))|~greater(hazard_of_mortality(esk3_0,esk7_0),hazard_of_mortality(esk3_0,esk5_0))|hazard_of_mortality(esk3_0,esk5_0)!=hazard_of_mortality(esk3_0,esk4_0))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_27])])])])).
% 1.09/0.66 cnf(c_0_42, plain, (smaller_or_equal(X1,X2)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 1.09/0.66 cnf(c_0_43, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 1.09/0.66 cnf(c_0_44, plain, (X1=X2|greater(X1,X2)|greater(X2,X1)), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 1.09/0.66 cnf(c_0_45, 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_32])).
% 1.09/0.66 cnf(c_0_46, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_33])).
% 1.09/0.66 cnf(c_0_47, 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_34])).
% 1.09/0.66 cnf(c_0_48, 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_35])).
% 1.09/0.66 cnf(c_0_49, 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_36, c_0_37]), c_0_38])).
% 1.09/0.66 cnf(c_0_50, 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_39])).
% 1.09/0.66 fof(c_0_51, plain, ![X28, X29, X30]:((~organization(X28)|~has_immunity(X28,X29)|~has_immunity(X28,X30)|hazard_of_mortality(X28,X29)=hazard_of_mortality(X28,X30))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_2])])])).
% 1.09/0.66 cnf(c_0_52, plain, (has_immunity(X1,X2)|~smaller_or_equal(age(X1,X2),eta)|~has_endowment(X1)), inference(split_conjunct,[status(thm)],[c_0_40])).
% 1.09/0.66 cnf(c_0_53, negated_conjecture, (smaller_or_equal(age(esk3_0,esk5_0),eta)), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.09/0.66 cnf(c_0_54, negated_conjecture, (has_endowment(esk3_0)), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.09/0.66 cnf(c_0_55, plain, (X1=X2|greater(X1,X2)|smaller_or_equal(X1,X2)), inference(spm,[status(thm)],[c_0_42, c_0_31])).
% 1.09/0.66 cnf(c_0_56, plain, (smaller(X1,X2)|X1=X2|~smaller_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 1.09/0.66 cnf(c_0_57, negated_conjecture, (smaller_or_equal(age(esk3_0,esk4_0),age(esk3_0,esk5_0))), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.09/0.66 cnf(c_0_58, plain, (X1=X2|greater(X1,X2)|greater(X3,X1)|~greater(X3,X2)), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 1.09/0.66 fof(c_0_59, plain, ![X1, X5, X4]:((((organization(X1)&has_immunity(X1,X5))&~has_immunity(X1,X4))=>greater(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))), inference(fof_simplification,[status(thm)],[assumption_3])).
% 1.09/0.66 cnf(c_0_60, negated_conjecture, (greater(age(esk3_0,esk6_0),eta)), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.09/0.66 cnf(c_0_61, plain, (smaller(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~epred1_3(X3,X2,X1)|~greater(position(X1,X2),position(X1,X3))|~greater(capability(X1,X2),capability(X1,X3))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 1.09/0.66 cnf(c_0_62, plain, (greater(position(X1,X2),position(X1,X3))|~organization(X1)|~greater(age(X1,X2),age(X1,X3))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 1.09/0.66 cnf(c_0_63, plain, (greater(capability(X1,X2),capability(X1,X3))|~organization(X1)|~greater(age(X1,X2),age(X1,X3))|~smaller_or_equal(internal_friction(X1,X2),internal_friction(X1,X4))), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 1.09/0.66 cnf(c_0_64, negated_conjecture, (greater(age(esk3_0,esk7_0),age(esk3_0,esk6_0))), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.09/0.66 cnf(c_0_65, negated_conjecture, (organization(esk3_0)), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.09/0.66 cnf(c_0_66, plain, (smaller_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_28])).
% 1.09/0.66 fof(c_0_67, 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_17])).
% 1.09/0.66 cnf(c_0_68, plain, (hazard_of_mortality(X1,X2)=hazard_of_mortality(X1,X3)|~organization(X1)|~has_immunity(X1,X2)|~has_immunity(X1,X3)), inference(split_conjunct,[status(thm)],[c_0_51])).
% 1.09/0.66 cnf(c_0_69, negated_conjecture, (has_immunity(esk3_0,esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_53]), c_0_54])])).
% 1.09/0.66 cnf(c_0_70, plain, (age(X1,X2)=eta|has_immunity(X1,X2)|greater(age(X1,X2),eta)|~has_endowment(X1)), inference(spm,[status(thm)],[c_0_52, c_0_55])).
% 1.09/0.66 fof(c_0_71, plain, ![X15, X16]:((~greater(X15,X16)|~greater(X16,X15))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[meaning_postulate_greater_strict])])])).
% 1.09/0.66 cnf(c_0_72, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|smaller(age(esk3_0,esk4_0),age(esk3_0,esk5_0))), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 1.09/0.66 cnf(c_0_73, plain, (~greater(age(X1,X2),eta)|~has_immunity(X1,X2)|~has_endowment(X1)), inference(split_conjunct,[status(thm)],[c_0_40])).
% 1.09/0.66 cnf(c_0_74, plain, (X1=X2|X3=X2|greater(X2,X1)|greater(X1,X3)|greater(X3,X2)), inference(spm,[status(thm)],[c_0_58, c_0_44])).
% 1.09/0.66 fof(c_0_75, plain, ![X31, X32, X33]:((~organization(X31)|~has_immunity(X31,X32)|has_immunity(X31,X33)|greater(hazard_of_mortality(X31,X33),hazard_of_mortality(X31,X32)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_59])])])).
% 1.09/0.66 cnf(c_0_76, negated_conjecture, (greater(X1,eta)|~greater(X1,age(esk3_0,esk6_0))), inference(spm,[status(thm)],[c_0_43, c_0_60])).
% 1.09/0.66 cnf(c_0_77, plain, (smaller(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~epred1_3(X3,X2,X1)|~organization(X1)|~greater(capability(X1,X2),capability(X1,X3))|~greater(age(X1,X2),age(X1,X3))), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 1.09/0.66 cnf(c_0_78, negated_conjecture, (greater(capability(esk3_0,esk7_0),capability(esk3_0,esk6_0))|~smaller_or_equal(internal_friction(esk3_0,esk7_0),internal_friction(esk3_0,X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_65])])).
% 1.09/0.66 cnf(c_0_79, plain, (smaller_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_66])).
% 1.09/0.66 fof(c_0_80, plain, ![X34, X35, X36]:((~organization(X34)|has_immunity(X34,X35)|has_immunity(X34,X36)|epred1_3(X35,X36,X34))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_67])])])).
% 1.09/0.66 cnf(c_0_81, negated_conjecture, (hazard_of_mortality(esk3_0,X1)=hazard_of_mortality(esk3_0,esk5_0)|~has_immunity(esk3_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_69]), c_0_65])])).
% 1.09/0.66 cnf(c_0_82, negated_conjecture, (age(esk3_0,X1)=eta|has_immunity(esk3_0,X1)|greater(age(esk3_0,X1),eta)), inference(spm,[status(thm)],[c_0_70, c_0_54])).
% 1.09/0.66 cnf(c_0_83, plain, (~greater(X1,X2)|~greater(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_71])).
% 1.09/0.66 cnf(c_0_84, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|greater(age(esk3_0,esk5_0),age(esk3_0,esk4_0))), inference(spm,[status(thm)],[c_0_30, c_0_72])).
% 1.09/0.66 cnf(c_0_85, plain, (age(X1,X2)=X3|eta=X3|greater(X3,age(X1,X2))|greater(eta,X3)|~has_immunity(X1,X2)|~has_endowment(X1)), inference(spm,[status(thm)],[c_0_73, c_0_74])).
% 1.09/0.66 cnf(c_0_86, plain, (has_immunity(X1,X3)|greater(hazard_of_mortality(X1,X3),hazard_of_mortality(X1,X2))|~organization(X1)|~has_immunity(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_75])).
% 1.09/0.66 cnf(c_0_87, negated_conjecture, (greater(age(esk3_0,esk7_0),eta)), inference(spm,[status(thm)],[c_0_76, c_0_64])).
% 1.09/0.66 cnf(c_0_88, plain, (greater(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~epred1_3(X2,X3,X1)|~organization(X1)|~greater(capability(X1,X3),capability(X1,X2))|~greater(age(X1,X3),age(X1,X2))), inference(spm,[status(thm)],[c_0_30, c_0_77])).
% 1.09/0.66 cnf(c_0_89, negated_conjecture, (greater(capability(esk3_0,esk7_0),capability(esk3_0,esk6_0))), inference(spm,[status(thm)],[c_0_78, c_0_79])).
% 1.09/0.66 cnf(c_0_90, plain, (has_immunity(X1,X2)|has_immunity(X1,X3)|epred1_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_80])).
% 1.09/0.66 cnf(c_0_91, negated_conjecture, (hazard_of_mortality(esk3_0,X1)=hazard_of_mortality(esk3_0,esk5_0)|age(esk3_0,X1)=eta|greater(age(esk3_0,X1),eta)), inference(spm,[status(thm)],[c_0_81, c_0_82])).
% 1.09/0.66 cnf(c_0_92, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|~greater(age(esk3_0,esk4_0),age(esk3_0,esk5_0))), inference(spm,[status(thm)],[c_0_83, c_0_84])).
% 1.09/0.66 cnf(c_0_93, negated_conjecture, (age(esk3_0,esk5_0)=X1|eta=X1|greater(X1,age(esk3_0,esk5_0))|greater(eta,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_69]), c_0_54])])).
% 1.09/0.66 cnf(c_0_94, negated_conjecture, (~greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk7_0))|~greater(hazard_of_mortality(esk3_0,esk7_0),hazard_of_mortality(esk3_0,esk5_0))|hazard_of_mortality(esk3_0,esk5_0)!=hazard_of_mortality(esk3_0,esk4_0)), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.09/0.66 cnf(c_0_95, negated_conjecture, (has_immunity(esk3_0,X1)|greater(hazard_of_mortality(esk3_0,X1),hazard_of_mortality(esk3_0,esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_69]), c_0_65])])).
% 1.09/0.66 cnf(c_0_96, negated_conjecture, (~has_immunity(esk3_0,esk7_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_87]), c_0_54])])).
% 1.09/0.66 cnf(c_0_97, negated_conjecture, (greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk7_0))|~epred1_3(esk6_0,esk7_0,esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_89]), c_0_65]), c_0_64])])).
% 1.09/0.66 cnf(c_0_98, negated_conjecture, (epred1_3(X1,X2,esk3_0)|has_immunity(esk3_0,X1)|has_immunity(esk3_0,X2)), inference(spm,[status(thm)],[c_0_90, c_0_65])).
% 1.09/0.66 cnf(c_0_99, negated_conjecture, (~has_immunity(esk3_0,esk6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_60]), c_0_54])])).
% 1.09/0.66 cnf(c_0_100, plain, (smaller(X2,X1)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 1.09/0.66 cnf(c_0_101, negated_conjecture, (age(esk3_0,esk5_0)=eta|smaller(age(esk3_0,esk5_0),eta)), inference(spm,[status(thm)],[c_0_56, c_0_53])).
% 1.09/0.66 cnf(c_0_102, negated_conjecture, (hazard_of_mortality(esk3_0,X1)=hazard_of_mortality(esk3_0,esk5_0)|age(esk3_0,X1)=eta|~greater(eta,age(esk3_0,X1))), inference(spm,[status(thm)],[c_0_83, c_0_91])).
% 1.09/0.66 cnf(c_0_103, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|age(esk3_0,esk4_0)=eta|greater(eta,age(esk3_0,esk4_0))), inference(spm,[status(thm)],[c_0_92, c_0_93])).
% 1.09/0.66 cnf(c_0_104, negated_conjecture, (hazard_of_mortality(esk3_0,esk4_0)!=hazard_of_mortality(esk3_0,esk5_0)|~greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk7_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_95]), c_0_96])).
% 1.09/0.66 cnf(c_0_105, negated_conjecture, (greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk7_0))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_98]), c_0_99]), c_0_96])).
% 1.09/0.66 cnf(c_0_106, plain, (smaller_or_equal(X1,X2)|~greater(X2,X1)), inference(spm,[status(thm)],[c_0_42, c_0_100])).
% 1.09/0.66 cnf(c_0_107, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|greater(X1,age(esk3_0,esk4_0))|~greater(X1,age(esk3_0,esk5_0))), inference(spm,[status(thm)],[c_0_43, c_0_84])).
% 1.09/0.66 cnf(c_0_108, negated_conjecture, (age(esk3_0,esk5_0)=eta|greater(eta,age(esk3_0,esk5_0))), inference(spm,[status(thm)],[c_0_30, c_0_101])).
% 1.09/0.66 cnf(c_0_109, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|hazard_of_mortality(esk3_0,esk4_0)=hazard_of_mortality(esk3_0,esk5_0)|age(esk3_0,esk4_0)=eta), inference(spm,[status(thm)],[c_0_102, c_0_103])).
% 1.09/0.66 cnf(c_0_110, negated_conjecture, (hazard_of_mortality(esk3_0,esk4_0)!=hazard_of_mortality(esk3_0,esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_104, c_0_105])])).
% 1.09/0.66 cnf(c_0_111, plain, (has_immunity(X1,X2)|~has_endowment(X1)|~greater(eta,age(X1,X2))), inference(spm,[status(thm)],[c_0_52, c_0_106])).
% 1.09/0.66 cnf(c_0_112, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|age(esk3_0,esk5_0)=eta|greater(eta,age(esk3_0,esk4_0))), inference(spm,[status(thm)],[c_0_107, c_0_108])).
% 1.09/0.66 cnf(c_0_113, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|age(esk3_0,esk4_0)=eta), inference(sr,[status(thm)],[c_0_109, c_0_110])).
% 1.09/0.66 cnf(c_0_114, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|age(esk3_0,esk5_0)=eta|has_immunity(esk3_0,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_112]), c_0_54])])).
% 1.09/0.66 cnf(c_0_115, negated_conjecture, (age(esk3_0,esk4_0)=eta|age(esk3_0,esk5_0)!=eta), inference(ef,[status(thm)],[c_0_113])).
% 1.09/0.66 cnf(c_0_116, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|hazard_of_mortality(esk3_0,esk4_0)=hazard_of_mortality(esk3_0,esk5_0)|age(esk3_0,esk5_0)=eta), inference(spm,[status(thm)],[c_0_81, c_0_114])).
% 1.09/0.66 cnf(c_0_117, negated_conjecture, (has_immunity(esk3_0,esk4_0)|age(esk3_0,esk5_0)!=eta), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_115]), c_0_54]), c_0_79])])).
% 1.09/0.66 cnf(c_0_118, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)|age(esk3_0,esk5_0)=eta), inference(sr,[status(thm)],[c_0_116, c_0_110])).
% 1.09/0.66 cnf(c_0_119, negated_conjecture, (age(esk3_0,esk5_0)!=eta), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_117]), c_0_110])).
% 1.09/0.66 cnf(c_0_120, negated_conjecture, (age(esk3_0,esk4_0)=age(esk3_0,esk5_0)), inference(sr,[status(thm)],[c_0_118, c_0_119])).
% 1.09/0.66 cnf(c_0_121, negated_conjecture, (~greater(eta,age(esk3_0,esk5_0))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_120]), c_0_110]), c_0_119])).
% 1.09/0.66 cnf(c_0_122, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_108, c_0_119]), c_0_121]), ['proof']).
% 1.09/0.66 % SZS output end Proof
% 1.09/0.66 % User time : 0.099 s
% 1.09/0.66 % System time : 0.010 s
% 1.09/0.66 % Total time : 0.109 s
% 1.09/0.66 % User time : 0.593 s
% 1.09/0.66 % System time : 0.041 s
% 1.09/0.66 % Total time : 0.634 s
% 1.09/0.66
%------------------------------------------------------------------------------