%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT051+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n004.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.73s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT051+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.33 % Computer : n004.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Mon Sep 7 13:19:00 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.13/0.45 start to proof:theBenchmark.p
% 0.73/0.57 % Version : CSI_E---1.1
% 0.73/0.57 % Problem : theBenchmark.p
% 0.73/0.57 % Proof found!
% 0.73/0.57 % SZS status Theorem for theBenchmark.p
% 0.73/0.57 % SZS output start Proof
% 0.73/0.57 fof(theorem_4, 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,X8),hazard_of_mortality(X1,X7))&greater(hazard_of_mortality(X1,X7),hazard_of_mortality(X1,X6)))&hazard_of_mortality(X1,X6)=hazard_of_mortality(X1,X5)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', theorem_4)).
% 0.73/0.57 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.73/0.57 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.73/0.57 fof(definition_smaller, axiom, ![X1, X2]:((smaller(X1,X2)<=>greater(X2,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', definition_smaller)).
% 0.73/0.57 fof(assumption_10, axiom, ![X1, X5, X4]:((organization(X1)=>stock_of_knowledge(X1,X4)=stock_of_knowledge(X1,X5))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_10)).
% 0.73/0.57 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)).
% 0.73/0.57 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)).
% 0.73/0.57 fof(assumption_12, axiom, ![X1, X5, X4]:(((organization(X1)&greater(age(X1,X4),age(X1,X5)))=>greater(internal_friction(X1,X4),internal_friction(X1,X5)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_12)).
% 0.73/0.57 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)).
% 0.73/0.57 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.73/0.57 fof(assumption_11, axiom, ![X1, X5, X4]:((organization(X1)=>external_ties(X1,X4)=external_ties(X1,X5))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_11)).
% 0.73/0.57 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.73/0.57 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.73/0.57 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)).
% 0.73/0.57 fof(c_0_14, 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,X8),hazard_of_mortality(X1,X7))&greater(hazard_of_mortality(X1,X7),hazard_of_mortality(X1,X6)))&hazard_of_mortality(X1,X6)=hazard_of_mortality(X1,X5))))), inference(assume_negation,[status(cth)],[theorem_4])).
% 0.73/0.57 fof(c_0_15, 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.73/0.57 fof(c_0_16, 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])])])])).
% 0.73/0.57 fof(c_0_17, 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,esk7_0),hazard_of_mortality(esk3_0,esk6_0))|~greater(hazard_of_mortality(esk3_0,esk6_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_14])])])])).
% 0.73/0.57 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_15])).
% 0.73/0.57 fof(c_0_19, axiom, ![X1, X5, X4]:((organization(X1)=>epred2_3(X5,X4,X1))), inference(apply_def,[status(thm)],[assumption_5, c_0_15])).
% 0.73/0.57 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])])])).
% 0.73/0.57 cnf(c_0_21, plain, (smaller(X1,X2)|X1=X2|~smaller_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.73/0.57 cnf(c_0_22, negated_conjecture, (smaller_or_equal(age(esk3_0,esk4_0),age(esk3_0,esk5_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.73/0.57 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])])])])).
% 0.73/0.57 fof(c_0_24, plain, ![X43, X44, X45]:((~organization(X43)|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_10])])])).
% 0.73/0.57 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])])])).
% 0.73/0.57 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])).
% 0.73/0.57 fof(c_0_27, 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])])])).
% 0.73/0.57 cnf(c_0_28, plain, (greater(X2,X1)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.73/0.57 cnf(c_0_29, 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_21, c_0_22])).
% 0.73/0.57 cnf(c_0_30, negated_conjecture, (smaller_or_equal(age(esk3_0,esk5_0),eta)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.73/0.57 cnf(c_0_31, plain, (smaller(capability(X1,X2),capability(X1,X3))|~smaller_or_equal(stock_of_knowledge(X1,X2),stock_of_knowledge(X1,X3))|~greater(internal_friction(X1,X2),internal_friction(X1,X3))|~epred2_3(X3,X2,X1)), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.73/0.57 cnf(c_0_32, plain, (stock_of_knowledge(X1,X2)=stock_of_knowledge(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.73/0.57 cnf(c_0_33, plain, (epred2_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.73/0.57 fof(c_0_34, plain, ![X49, X50, X51]:((~organization(X49)|~greater(age(X49,X51),age(X49,X50))|greater(internal_friction(X49,X51),internal_friction(X49,X50)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_12])])])).
% 0.73/0.57 fof(c_0_35, 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])])])])])])])).
% 0.73/0.57 cnf(c_0_36, plain, (smaller_or_equal(X1,X2)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.73/0.57 cnf(c_0_37, plain, (smaller(X2,X1)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.73/0.57 cnf(c_0_38, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.73/0.57 cnf(c_0_39, 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_28, c_0_29])).
% 0.73/0.57 cnf(c_0_40, negated_conjecture, (age(esk3_0,esk5_0)=eta|smaller(age(esk3_0,esk5_0),eta)), inference(spm,[status(thm)],[c_0_21, c_0_30])).
% 0.73/0.57 fof(c_0_41, 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.73/0.57 cnf(c_0_42, plain, (smaller(capability(X1,X2),capability(X1,X3))|~organization(X1)|~greater(internal_friction(X1,X2),internal_friction(X1,X3))|~smaller_or_equal(stock_of_knowledge(X1,X2),stock_of_knowledge(X1,X4))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_33])).
% 0.73/0.57 cnf(c_0_43, plain, (greater(internal_friction(X1,X2),internal_friction(X1,X3))|~organization(X1)|~greater(age(X1,X2),age(X1,X3))), inference(split_conjunct,[status(thm)],[c_0_34])).
% 0.73/0.57 fof(c_0_44, 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])])])).
% 0.73/0.57 cnf(c_0_45, plain, (has_immunity(X1,X2)|~smaller_or_equal(age(X1,X2),eta)|~has_endowment(X1)), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.73/0.57 cnf(c_0_46, negated_conjecture, (has_endowment(esk3_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.73/0.57 cnf(c_0_47, plain, (smaller_or_equal(X1,X2)|~greater(X2,X1)), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.73/0.57 cnf(c_0_48, 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_38, c_0_39])).
% 0.73/0.57 cnf(c_0_49, negated_conjecture, (age(esk3_0,esk5_0)=eta|greater(eta,age(esk3_0,esk5_0))), inference(spm,[status(thm)],[c_0_28, c_0_40])).
% 0.73/0.57 fof(c_0_50, 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_41])).
% 0.73/0.57 fof(c_0_51, 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])])])])).
% 0.73/0.57 fof(c_0_52, plain, ![X46, X47, X48]:((~organization(X46)|external_ties(X46,X48)=external_ties(X46,X47))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_11])])])).
% 0.73/0.57 cnf(c_0_53, plain, (smaller(capability(X1,X2),capability(X1,X3))|~organization(X1)|~greater(age(X1,X2),age(X1,X3))|~smaller_or_equal(stock_of_knowledge(X1,X2),stock_of_knowledge(X1,X4))), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 0.73/0.57 cnf(c_0_54, negated_conjecture, (greater(age(esk3_0,esk7_0),age(esk3_0,esk6_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.73/0.57 cnf(c_0_55, negated_conjecture, (organization(esk3_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.73/0.57 cnf(c_0_56, plain, (smaller_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.73/0.57 cnf(c_0_57, 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_44])).
% 0.73/0.57 cnf(c_0_58, negated_conjecture, (has_immunity(esk3_0,esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_30]), c_0_46])])).
% 0.73/0.57 cnf(c_0_59, plain, (has_immunity(X1,X2)|~has_endowment(X1)|~greater(eta,age(X1,X2))), inference(spm,[status(thm)],[c_0_45, c_0_47])).
% 0.73/0.57 cnf(c_0_60, 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_48, c_0_49])).
% 0.73/0.57 fof(c_0_61, 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_50])])])])).
% 0.73/0.57 cnf(c_0_62, plain, (position(X1,X2)=position(X1,X3)|external_ties(X1,X2)!=external_ties(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_51])).
% 0.73/0.57 cnf(c_0_63, plain, (external_ties(X1,X2)=external_ties(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_52])).
% 0.73/0.57 cnf(c_0_64, negated_conjecture, (smaller(capability(esk3_0,esk7_0),capability(esk3_0,esk6_0))|~smaller_or_equal(stock_of_knowledge(esk3_0,esk7_0),stock_of_knowledge(esk3_0,X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_54]), c_0_55])])).
% 0.73/0.57 cnf(c_0_65, plain, (smaller_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_56])).
% 0.73/0.57 cnf(c_0_66, 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_57, c_0_58]), c_0_55])])).
% 0.73/0.57 cnf(c_0_67, 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_59, c_0_60]), c_0_46])])).
% 0.73/0.57 cnf(c_0_68, plain, (smaller(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~greater(capability(X1,X2),capability(X1,X3))|~greater_or_equal(position(X1,X2),position(X1,X3))|~epred1_3(X3,X2,X1)), inference(split_conjunct,[status(thm)],[c_0_61])).
% 0.73/0.57 cnf(c_0_69, plain, (position(X1,X2)=position(X1,X3)|~organization(X1)), inference(csr,[status(thm)],[c_0_62, c_0_63])).
% 0.73/0.57 cnf(c_0_70, negated_conjecture, (smaller(capability(esk3_0,esk7_0),capability(esk3_0,esk6_0))), inference(spm,[status(thm)],[c_0_64, c_0_65])).
% 0.73/0.57 fof(c_0_71, 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])])])])).
% 0.73/0.57 cnf(c_0_72, 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_66, c_0_67])).
% 0.73/0.57 cnf(c_0_73, 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_or_equal(position(X1,X2),position(X1,X4))), inference(spm,[status(thm)],[c_0_68, c_0_69])).
% 0.73/0.57 cnf(c_0_74, negated_conjecture, (greater(capability(esk3_0,esk6_0),capability(esk3_0,esk7_0))), inference(spm,[status(thm)],[c_0_28, c_0_70])).
% 0.73/0.57 cnf(c_0_75, plain, (greater_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_71])).
% 0.73/0.57 fof(c_0_76, 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_41])).
% 0.73/0.57 cnf(c_0_77, negated_conjecture, (greater(age(esk3_0,esk6_0),eta)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.73/0.57 cnf(c_0_78, negated_conjecture, (hazard_of_mortality(esk3_0,esk4_0)=hazard_of_mortality(esk3_0,esk5_0)|age(esk3_0,esk5_0)=eta), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_72]), c_0_46]), c_0_30])]), c_0_66])).
% 0.73/0.57 cnf(c_0_79, plain, (smaller(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk7_0))|~epred1_3(esk7_0,esk6_0,esk3_0)|~greater_or_equal(position(esk3_0,esk6_0),position(esk3_0,X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_74]), c_0_55])])).
% 0.73/0.57 cnf(c_0_80, plain, (greater_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_75])).
% 0.73/0.57 fof(c_0_81, 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_76])])])).
% 0.73/0.57 cnf(c_0_82, negated_conjecture, (greater(X1,eta)|~greater(X1,age(esk3_0,esk6_0))), inference(spm,[status(thm)],[c_0_38, c_0_77])).
% 0.73/0.57 cnf(c_0_83, negated_conjecture, (hazard_of_mortality(esk3_0,esk4_0)=hazard_of_mortality(esk3_0,esk5_0)|smaller_or_equal(age(esk3_0,esk4_0),eta)), inference(spm,[status(thm)],[c_0_22, c_0_78])).
% 0.73/0.57 cnf(c_0_84, plain, (smaller(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk7_0))|~epred1_3(esk7_0,esk6_0,esk3_0)), inference(spm,[status(thm)],[c_0_79, c_0_80])).
% 0.73/0.57 cnf(c_0_85, plain, (has_immunity(X1,X2)|has_immunity(X1,X3)|epred1_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_81])).
% 0.73/0.57 cnf(c_0_86, plain, (~greater(age(X1,X2),eta)|~has_immunity(X1,X2)|~has_endowment(X1)), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.73/0.57 cnf(c_0_87, negated_conjecture, (greater(age(esk3_0,esk7_0),eta)), inference(spm,[status(thm)],[c_0_82, c_0_54])).
% 0.73/0.57 fof(c_0_88, 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])).
% 0.73/0.57 cnf(c_0_89, negated_conjecture, (~greater(hazard_of_mortality(esk3_0,esk7_0),hazard_of_mortality(esk3_0,esk6_0))|~greater(hazard_of_mortality(esk3_0,esk6_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_17])).
% 0.73/0.57 cnf(c_0_90, negated_conjecture, (hazard_of_mortality(esk3_0,esk4_0)=hazard_of_mortality(esk3_0,esk5_0)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_83]), c_0_46])]), c_0_66])).
% 0.73/0.57 cnf(c_0_91, plain, (greater(hazard_of_mortality(esk3_0,esk7_0),hazard_of_mortality(esk3_0,esk6_0))|~epred1_3(esk7_0,esk6_0,esk3_0)), inference(spm,[status(thm)],[c_0_28, c_0_84])).
% 0.73/0.57 cnf(c_0_92, negated_conjecture, (epred1_3(X1,X2,esk3_0)|has_immunity(esk3_0,X1)|has_immunity(esk3_0,X2)), inference(spm,[status(thm)],[c_0_85, c_0_55])).
% 0.73/0.57 cnf(c_0_93, negated_conjecture, (~has_immunity(esk3_0,esk7_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_87]), c_0_46])])).
% 0.73/0.57 cnf(c_0_94, negated_conjecture, (~has_immunity(esk3_0,esk6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_77]), c_0_46])])).
% 0.73/0.57 fof(c_0_95, 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_88])])])).
% 0.73/0.57 cnf(c_0_96, negated_conjecture, (~greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk5_0))|~greater(hazard_of_mortality(esk3_0,esk7_0),hazard_of_mortality(esk3_0,esk6_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_89, c_0_90])])).
% 0.73/0.57 cnf(c_0_97, negated_conjecture, (greater(hazard_of_mortality(esk3_0,esk7_0),hazard_of_mortality(esk3_0,esk6_0))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_92]), c_0_93]), c_0_94])).
% 0.73/0.57 cnf(c_0_98, 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_95])).
% 0.73/0.57 cnf(c_0_99, negated_conjecture, (~greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96, c_0_97])])).
% 0.73/0.57 cnf(c_0_100, 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_98, c_0_58]), c_0_55])])).
% 0.73/0.57 cnf(c_0_101, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_99, c_0_100]), c_0_94]), ['proof']).
% 0.73/0.57 % SZS output end Proof
% 0.73/0.57 % User time : 0.036 s
% 0.73/0.57 % System time : 0.008 s
% 0.73/0.57 % Total time : 0.044 s
% 0.73/0.57 % User time : 0.137 s
% 0.73/0.57 % System time : 0.032 s
% 0.73/0.57 % Total time : 0.169 s
% 0.73/0.57
%------------------------------------------------------------------------------