%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT050+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n020.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.25s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT050+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n020.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 13:18:13 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark.p
% 0.25/0.55 % Version : CSI_E---1.1
% 0.25/0.55 % Problem : theBenchmark.p
% 0.25/0.55 % Proof found!
% 0.25/0.55 % SZS status Theorem for theBenchmark.p
% 0.25/0.55 % SZS output start Proof
% 0.25/0.55 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/sandbox/benchmark/theBenchmark.p', assumption_4)).
% 0.25/0.55 fof(theorem_3, conjecture, ![X1, X5, X4]:((((organization(X1)&~(has_endowment(X1)))&greater(age(X1,X4),age(X1,X5)))=>greater(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_3)).
% 0.25/0.55 fof(assumption_1, axiom, ![X1, X4]:(((organization(X1)&~(has_endowment(X1)))=>~(has_immunity(X1,X4)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_1)).
% 0.25/0.55 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/sandbox/benchmark/theBenchmark.p', assumption_5)).
% 0.25/0.55 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/sandbox/benchmark/theBenchmark.p', assumption_6)).
% 0.25/0.55 fof(assumption_11, axiom, ![X1, X5, X4]:((organization(X1)=>external_ties(X1,X4)=external_ties(X1,X5))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_11)).
% 0.25/0.55 fof(assumption_10, axiom, ![X1, X5, X4]:((organization(X1)=>stock_of_knowledge(X1,X4)=stock_of_knowledge(X1,X5))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_10)).
% 0.25/0.55 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/sandbox/benchmark/theBenchmark.p', assumption_12)).
% 0.25/0.55 fof(definition_smaller, axiom, ![X1, X2]:((smaller(X1,X2)<=>greater(X2,X1))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_smaller)).
% 0.25/0.55 fof(definition_smaller_or_equal, axiom, ![X1, X2]:((smaller_or_equal(X1,X2)<=>(smaller(X1,X2)|X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_smaller_or_equal)).
% 0.25/0.55 fof(definition_greater_or_equal, axiom, ![X1, X2]:((greater_or_equal(X1,X2)<=>(greater(X1,X2)|X1=X2))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_greater_or_equal)).
% 0.25/0.55 fof(c_0_11, 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.25/0.55 fof(c_0_12, 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_11])).
% 0.25/0.55 fof(c_0_13, negated_conjecture, ~(![X1, X5, X4]:((((organization(X1)&~has_endowment(X1))&greater(age(X1,X4),age(X1,X5)))=>greater(hazard_of_mortality(X1,X4),hazard_of_mortality(X1,X5))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[theorem_3])])).
% 0.25/0.55 fof(c_0_14, 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.25/0.55 fof(c_0_15, plain, ![X1, X4]:(((organization(X1)&~has_endowment(X1))=>~has_immunity(X1,X4))), inference(fof_simplification,[status(thm)],[assumption_1])).
% 0.25/0.55 fof(c_0_16, plain, ![X14, X15, X16]:((~organization(X14)|has_immunity(X14,X15)|has_immunity(X14,X16)|epred1_3(X15,X16,X14))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])).
% 0.25/0.55 fof(c_0_17, negated_conjecture, (((organization(esk1_0)&~has_endowment(esk1_0))&greater(age(esk1_0,esk3_0),age(esk1_0,esk2_0)))&~greater(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_13])])])])).
% 0.25/0.55 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_14])).
% 0.25/0.55 fof(c_0_19, axiom, ![X1, X5, X4]:((organization(X1)=>epred2_3(X5,X4,X1))), inference(apply_def,[status(thm)],[assumption_5, c_0_14])).
% 0.25/0.55 fof(c_0_20, 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_11])).
% 0.25/0.55 fof(c_0_21, plain, ![X22, X23, X24]:(((~greater(external_ties(X22,X24),external_ties(X22,X23))|greater(position(X22,X24),position(X22,X23))|~organization(X22))&(external_ties(X22,X24)!=external_ties(X22,X23)|position(X22,X24)=position(X22,X23)|~organization(X22)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_6])])])])).
% 0.25/0.55 fof(c_0_22, plain, ![X34, X35, X36]:((~organization(X34)|external_ties(X34,X36)=external_ties(X34,X35))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_11])])])).
% 0.25/0.55 fof(c_0_23, plain, ![X20, X21]:((~organization(X20)|has_endowment(X20)|~has_immunity(X20,X21))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_15])])])).
% 0.25/0.55 cnf(c_0_24, plain, (has_immunity(X1,X2)|has_immunity(X1,X3)|epred1_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.25/0.55 cnf(c_0_25, negated_conjecture, (organization(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.25/0.55 fof(c_0_26, 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_18])])])])).
% 0.25/0.55 fof(c_0_27, plain, ![X37, X38, X39]:((~organization(X37)|stock_of_knowledge(X37,X39)=stock_of_knowledge(X37,X38))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_10])])])).
% 0.25/0.55 fof(c_0_28, plain, ![X25, X26, X27]:((~organization(X25)|epred2_3(X26,X27,X25))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])).
% 0.25/0.55 fof(c_0_29, plain, ![X17, X18, X19]:((~organization(X17)|~greater(age(X17,X19),age(X17,X18))|greater(internal_friction(X17,X19),internal_friction(X17,X18)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_12])])])).
% 0.25/0.55 fof(c_0_30, plain, ![X28, X29]:(((~smaller(X28,X29)|greater(X29,X28))&(~greater(X29,X28)|smaller(X28,X29)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller])])])).
% 0.25/0.55 fof(c_0_31, 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_20])])])])).
% 0.25/0.55 cnf(c_0_32, plain, (position(X1,X2)=position(X1,X3)|external_ties(X1,X2)!=external_ties(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.25/0.55 cnf(c_0_33, plain, (external_ties(X1,X2)=external_ties(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.25/0.55 cnf(c_0_34, plain, (has_endowment(X1)|~organization(X1)|~has_immunity(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.25/0.55 cnf(c_0_35, negated_conjecture, (epred1_3(X1,X2,esk1_0)|has_immunity(esk1_0,X1)|has_immunity(esk1_0,X2)), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.25/0.55 cnf(c_0_36, negated_conjecture, (~has_endowment(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.25/0.55 cnf(c_0_37, 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_26])).
% 0.25/0.55 cnf(c_0_38, plain, (stock_of_knowledge(X1,X2)=stock_of_knowledge(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.25/0.55 cnf(c_0_39, plain, (epred2_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.25/0.55 cnf(c_0_40, 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_29])).
% 0.25/0.55 cnf(c_0_41, negated_conjecture, (greater(age(esk1_0,esk3_0),age(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.25/0.55 fof(c_0_42, plain, ![X40, X41]:(((~smaller_or_equal(X40,X41)|(smaller(X40,X41)|X40=X41))&((~smaller(X40,X41)|smaller_or_equal(X40,X41))&(X40!=X41|smaller_or_equal(X40,X41))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller_or_equal])])])])).
% 0.25/0.55 cnf(c_0_43, plain, (greater(X2,X1)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.25/0.55 cnf(c_0_44, 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_31])).
% 0.25/0.55 cnf(c_0_45, plain, (position(X1,X2)=position(X1,X3)|~organization(X1)), inference(csr,[status(thm)],[c_0_32, c_0_33])).
% 0.25/0.55 cnf(c_0_46, 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_34, c_0_35]), c_0_25])]), c_0_36])).
% 0.25/0.55 fof(c_0_47, plain, ![X32, X33]:(((~greater_or_equal(X32,X33)|(greater(X32,X33)|X32=X33))&((~greater(X32,X33)|greater_or_equal(X32,X33))&(X32!=X33|greater_or_equal(X32,X33))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_greater_or_equal])])])])).
% 0.25/0.55 cnf(c_0_48, 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_37, c_0_38]), c_0_39])).
% 0.25/0.55 cnf(c_0_49, negated_conjecture, (greater(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_25])])).
% 0.25/0.55 cnf(c_0_50, plain, (smaller_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_42])).
% 0.25/0.55 cnf(c_0_51, plain, (greater(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~epred1_3(X2,X3,X1)|~greater(capability(X1,X3),capability(X1,X2))|~greater_or_equal(position(X1,X3),position(X1,X2))), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 0.25/0.55 cnf(c_0_52, negated_conjecture, (position(esk1_0,X1)=position(esk1_0,X2)), inference(spm,[status(thm)],[c_0_45, c_0_25])).
% 0.25/0.55 cnf(c_0_53, 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_34, c_0_46]), c_0_25])]), c_0_36])).
% 0.25/0.55 cnf(c_0_54, plain, (greater_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_47])).
% 0.25/0.55 cnf(c_0_55, negated_conjecture, (smaller(capability(esk1_0,esk3_0),capability(esk1_0,esk2_0))|~smaller_or_equal(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_49]), c_0_25])])).
% 0.25/0.55 cnf(c_0_56, plain, (smaller_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_50])).
% 0.25/0.55 cnf(c_0_57, negated_conjecture, (greater(hazard_of_mortality(esk1_0,X1),hazard_of_mortality(esk1_0,X2))|~greater(capability(esk1_0,X2),capability(esk1_0,X1))|~greater_or_equal(position(esk1_0,X2),position(esk1_0,X3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_53])])).
% 0.25/0.55 cnf(c_0_58, plain, (greater_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_54])).
% 0.25/0.55 cnf(c_0_59, negated_conjecture, (smaller(capability(esk1_0,esk3_0),capability(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_55, c_0_56])).
% 0.25/0.55 cnf(c_0_60, negated_conjecture, (~greater(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.25/0.55 cnf(c_0_61, negated_conjecture, (greater(hazard_of_mortality(esk1_0,X1),hazard_of_mortality(esk1_0,X2))|~greater(capability(esk1_0,X2),capability(esk1_0,X1))), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 0.25/0.55 cnf(c_0_62, negated_conjecture, (greater(capability(esk1_0,esk2_0),capability(esk1_0,esk3_0))), inference(spm,[status(thm)],[c_0_43, c_0_59])).
% 0.25/0.55 cnf(c_0_63, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_62])]), ['proof']).
% 0.25/0.55 % SZS output end Proof
% 0.25/0.55 % User time : 0.020 s
% 0.25/0.55 % System time : 0.001 s
% 0.25/0.55 % Total time : 0.021 s
% 0.25/0.55 % User time : 0.021 s
% 0.25/0.55 % System time : 0.005 s
% 0.25/0.55 % Total time : 0.026 s
% 0.25/0.55
%------------------------------------------------------------------------------