%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT042+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n011.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:33 AM UTC 2026
% Result : Theorem 5.14s 1.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT042+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 13:04:00 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark.p
% 5.14/1.22 % Version : CSI_E---1.1
% 5.14/1.22 % Problem : theBenchmark.p
% 5.14/1.22 % Proof found!
% 5.14/1.22 % SZS status Theorem for theBenchmark.p
% 5.14/1.22 % SZS output start Proof
% 5.14/1.22 fof(lemma_1, conjecture, ![X1, X4, X5]:((((organization(X1)&~(has_immunity(X1,X4)))&~(has_immunity(X1,X5)))=>((((greater(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&smaller_or_equal(internal_friction(X1,X5),internal_friction(X1,X4)))&greater_or_equal(external_ties(X1,X5),external_ties(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))&(((greater_or_equal(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&smaller_or_equal(internal_friction(X1,X5),internal_friction(X1,X4)))&greater(external_ties(X1,X5),external_ties(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma_1)).
% 5.14/1.22 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)).
% 5.14/1.22 fof(meaning_postulate_greater_transitive, axiom, ![X1, X2, X3]:(((greater(X1,X2)&greater(X2,X3))=>greater(X1,X3))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_transitive)).
% 5.14/1.22 fof(assumption_6, axiom, ![X1, X4, X5]:((organization(X1)=>((greater(external_ties(X1,X5),external_ties(X1,X4))=>greater(position(X1,X5),position(X1,X4)))&(external_ties(X1,X5)=external_ties(X1,X4)=>position(X1,X5)=position(X1,X4))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_6)).
% 5.14/1.22 fof(meaning_postulate_greater_strict, axiom, ![X1, X2]:(~((greater(X1,X2)&greater(X2,X1)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_strict)).
% 5.14/1.22 fof(definition_smaller, axiom, ![X1, X2]:((smaller(X1,X2)<=>greater(X2,X1))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', definition_smaller)).
% 5.14/1.22 fof(meaning_postulate_greater_comparable, axiom, ![X1, X2]:((smaller(X1,X2)|X1=X2|greater(X1,X2))), file('/export/starexec/sandbox/benchmark/Axioms/MGT001+0.ax', meaning_postulate_greater_comparable)).
% 5.14/1.22 fof(assumption_4, axiom, ![X1, X4, X5]:((((organization(X1)&~(has_immunity(X1,X4)))&~(has_immunity(X1,X5)))=>((((greater(capability(X1,X5),capability(X1,X4))&greater_or_equal(position(X1,X5),position(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))&((greater_or_equal(capability(X1,X5),capability(X1,X4))&greater(position(X1,X5),position(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4))))&((capability(X1,X5)=capability(X1,X4)&position(X1,X5)=position(X1,X4))=>hazard_of_mortality(X1,X5)=hazard_of_mortality(X1,X4))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_4)).
% 5.14/1.22 fof(assumption_5, axiom, ![X1, X4, X5]:((organization(X1)=>((((greater(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&smaller_or_equal(internal_friction(X1,X5),internal_friction(X1,X4)))=>greater(capability(X1,X5),capability(X1,X4)))&((smaller_or_equal(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&greater(internal_friction(X1,X5),internal_friction(X1,X4)))=>smaller(capability(X1,X5),capability(X1,X4))))&((stock_of_knowledge(X1,X5)=stock_of_knowledge(X1,X4)&internal_friction(X1,X5)=internal_friction(X1,X4))=>capability(X1,X5)=capability(X1,X4))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', assumption_5)).
% 5.14/1.22 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)).
% 5.14/1.22 fof(c_0_10, negated_conjecture, ~(![X1, X4, X5]:((((organization(X1)&~has_immunity(X1,X4))&~has_immunity(X1,X5))=>((((greater(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&smaller_or_equal(internal_friction(X1,X5),internal_friction(X1,X4)))&greater_or_equal(external_ties(X1,X5),external_ties(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))&(((greater_or_equal(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&smaller_or_equal(internal_friction(X1,X5),internal_friction(X1,X4)))&greater(external_ties(X1,X5),external_ties(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[lemma_1])])).
% 5.14/1.22 fof(c_0_11, negated_conjecture, (((organization(esk1_0)&~has_immunity(esk1_0,esk2_0))&~has_immunity(esk1_0,esk3_0))&(((((((greater_or_equal(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0)))&(smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))))&(greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))))&(~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))))&((((greater_or_equal(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))|smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0)))&(smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))|smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))))&(greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))|smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))))&(~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))|smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0)))))&((((greater_or_equal(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))|greater_or_equal(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0)))&(smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))|greater_or_equal(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))))&(greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))|greater_or_equal(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))))&(~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))|greater_or_equal(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0)))))&((((greater_or_equal(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))|~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0)))&(smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))|~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))))&(greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))|~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))))&(~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))|~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])])])).
% 5.14/1.22 fof(c_0_12, plain, ![X29, X30]:(((~greater_or_equal(X29,X30)|(greater(X29,X30)|X29=X30))&((~greater(X29,X30)|greater_or_equal(X29,X30))&(X29!=X30|greater_or_equal(X29,X30))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_greater_or_equal])])])])).
% 5.14/1.22 fof(c_0_13, plain, ![X18, X19, X20]:((~greater(X18,X19)|~greater(X19,X20)|greater(X18,X20))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[meaning_postulate_greater_transitive])])])).
% 5.14/1.22 fof(c_0_14, plain, ![X21, X22, X23]:(((~greater(external_ties(X21,X23),external_ties(X21,X22))|greater(position(X21,X23),position(X21,X22))|~organization(X21))&(external_ties(X21,X23)!=external_ties(X21,X22)|position(X21,X23)=position(X21,X22)|~organization(X21)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_6])])])])).
% 5.14/1.22 cnf(c_0_15, negated_conjecture, (greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))|greater_or_equal(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 5.14/1.22 cnf(c_0_16, plain, (greater_or_equal(X1,X2)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 5.14/1.22 cnf(c_0_17, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 5.14/1.22 cnf(c_0_18, 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_14])).
% 5.14/1.22 cnf(c_0_19, plain, (greater(X1,X2)|X1=X2|~greater_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 5.14/1.22 cnf(c_0_20, negated_conjecture, (greater_or_equal(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))), inference(csr,[status(thm)],[c_0_15, c_0_16])).
% 5.14/1.22 fof(c_0_21, plain, ![X1, X5, X4]:((epred1_3(X4,X5,X1)<=>((((greater(capability(X1,X5),capability(X1,X4))&greater_or_equal(position(X1,X5),position(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))&((greater_or_equal(capability(X1,X5),capability(X1,X4))&greater(position(X1,X5),position(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4))))&((capability(X1,X5)=capability(X1,X4)&position(X1,X5)=position(X1,X4))=>hazard_of_mortality(X1,X5)=hazard_of_mortality(X1,X4))))), introduced(definition)).
% 5.14/1.22 fof(c_0_22, plain, ![X16, X17]:((~greater(X16,X17)|~greater(X17,X16))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[meaning_postulate_greater_strict])])])).
% 5.14/1.22 cnf(c_0_23, plain, (greater(X1,position(X2,X3))|~organization(X2)|~greater(external_ties(X2,X4),external_ties(X2,X3))|~greater(X1,position(X2,X4))), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 5.14/1.22 cnf(c_0_24, negated_conjecture, (external_ties(esk1_0,esk2_0)=external_ties(esk1_0,esk3_0)|greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 5.14/1.22 cnf(c_0_25, negated_conjecture, (organization(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 5.14/1.22 fof(c_0_26, plain, ![X1, X5, X4]:((epred1_3(X4,X5,X1)=>((((greater(capability(X1,X5),capability(X1,X4))&greater_or_equal(position(X1,X5),position(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))&((greater_or_equal(capability(X1,X5),capability(X1,X4))&greater(position(X1,X5),position(X1,X4)))=>smaller(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4))))&((capability(X1,X5)=capability(X1,X4)&position(X1,X5)=position(X1,X4))=>hazard_of_mortality(X1,X5)=hazard_of_mortality(X1,X4))))), inference(split_equiv,[status(thm)],[c_0_21])).
% 5.14/1.22 cnf(c_0_27, plain, (~greater(X1,X2)|~greater(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 5.14/1.22 cnf(c_0_28, negated_conjecture, (external_ties(esk1_0,esk2_0)=external_ties(esk1_0,esk3_0)|greater(X1,position(esk1_0,esk2_0))|~greater(X1,position(esk1_0,esk3_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_25])])).
% 5.14/1.22 fof(c_0_29, plain, ![X9, X10]:(((~smaller(X9,X10)|greater(X10,X9))&(~greater(X10,X9)|smaller(X9,X10)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller])])])).
% 5.14/1.22 fof(c_0_30, plain, ![X11, X12]:((smaller(X11,X12)|X11=X12|greater(X11,X12))), inference(variable_rename,[status(thm)],[meaning_postulate_greater_comparable])).
% 5.14/1.22 fof(c_0_31, plain, ![X31, X32, X33]:((((~greater(capability(X31,X32),capability(X31,X33))|~greater_or_equal(position(X31,X32),position(X31,X33))|smaller(hazard_of_mortality(X31,X32),hazard_of_mortality(X31,X33))|~epred1_3(X33,X32,X31))&(~greater_or_equal(capability(X31,X32),capability(X31,X33))|~greater(position(X31,X32),position(X31,X33))|smaller(hazard_of_mortality(X31,X32),hazard_of_mortality(X31,X33))|~epred1_3(X33,X32,X31)))&(capability(X31,X32)!=capability(X31,X33)|position(X31,X32)!=position(X31,X33)|hazard_of_mortality(X31,X32)=hazard_of_mortality(X31,X33)|~epred1_3(X33,X32,X31)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_26])])])])).
% 5.14/1.22 cnf(c_0_32, negated_conjecture, (external_ties(esk1_0,esk2_0)=external_ties(esk1_0,esk3_0)|~greater(position(esk1_0,esk2_0),X1)|~greater(X1,position(esk1_0,esk3_0))), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 5.14/1.22 cnf(c_0_33, plain, (greater(X2,X1)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 5.14/1.22 cnf(c_0_34, plain, (smaller(X1,X2)|X1=X2|greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_30])).
% 5.14/1.22 cnf(c_0_35, plain, (position(X1,X2)=position(X1,X3)|external_ties(X1,X2)!=external_ties(X1,X3)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 5.14/1.22 fof(c_0_36, plain, ![X1, X5, X4]:((epred2_3(X4,X5,X1)<=>((((greater(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&smaller_or_equal(internal_friction(X1,X5),internal_friction(X1,X4)))=>greater(capability(X1,X5),capability(X1,X4)))&((smaller_or_equal(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&greater(internal_friction(X1,X5),internal_friction(X1,X4)))=>smaller(capability(X1,X5),capability(X1,X4))))&((stock_of_knowledge(X1,X5)=stock_of_knowledge(X1,X4)&internal_friction(X1,X5)=internal_friction(X1,X4))=>capability(X1,X5)=capability(X1,X4))))), introduced(definition)).
% 5.14/1.22 cnf(c_0_37, 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_31])).
% 5.14/1.22 cnf(c_0_38, negated_conjecture, (external_ties(esk1_0,esk2_0)=external_ties(esk1_0,esk3_0)|~greater(position(esk1_0,esk2_0),position(esk1_0,esk3_0))), inference(spm,[status(thm)],[c_0_32, c_0_28])).
% 5.14/1.22 cnf(c_0_39, plain, (X1=X2|greater(X1,X2)|greater(X2,X1)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 5.14/1.22 cnf(c_0_40, negated_conjecture, (position(esk1_0,X1)=position(esk1_0,X2)|external_ties(esk1_0,X1)!=external_ties(esk1_0,X2)), inference(spm,[status(thm)],[c_0_35, c_0_25])).
% 5.14/1.22 cnf(c_0_41, negated_conjecture, (~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))|~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 5.14/1.22 fof(c_0_42, plain, ![X1, X5, X4]:((epred2_3(X4,X5,X1)=>((((greater(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&smaller_or_equal(internal_friction(X1,X5),internal_friction(X1,X4)))=>greater(capability(X1,X5),capability(X1,X4)))&((smaller_or_equal(stock_of_knowledge(X1,X5),stock_of_knowledge(X1,X4))&greater(internal_friction(X1,X5),internal_friction(X1,X4)))=>smaller(capability(X1,X5),capability(X1,X4))))&((stock_of_knowledge(X1,X5)=stock_of_knowledge(X1,X4)&internal_friction(X1,X5)=internal_friction(X1,X4))=>capability(X1,X5)=capability(X1,X4))))), inference(split_equiv,[status(thm)],[c_0_36])).
% 5.14/1.22 cnf(c_0_43, 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_37, c_0_16])).
% 5.14/1.22 cnf(c_0_44, negated_conjecture, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|greater(position(esk1_0,esk3_0),position(esk1_0,esk2_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_40])).
% 5.14/1.22 cnf(c_0_45, negated_conjecture, (~smaller(hazard_of_mortality(esk1_0,esk3_0),hazard_of_mortality(esk1_0,esk2_0))), inference(cn,[status(thm)],[c_0_41])).
% 5.14/1.22 fof(c_0_46, plain, ![X34, X35, X36]:((((~greater(stock_of_knowledge(X34,X35),stock_of_knowledge(X34,X36))|~smaller_or_equal(internal_friction(X34,X35),internal_friction(X34,X36))|greater(capability(X34,X35),capability(X34,X36))|~epred2_3(X36,X35,X34))&(~smaller_or_equal(stock_of_knowledge(X34,X35),stock_of_knowledge(X34,X36))|~greater(internal_friction(X34,X35),internal_friction(X34,X36))|smaller(capability(X34,X35),capability(X34,X36))|~epred2_3(X36,X35,X34)))&(stock_of_knowledge(X34,X35)!=stock_of_knowledge(X34,X36)|internal_friction(X34,X35)!=internal_friction(X34,X36)|capability(X34,X35)=capability(X34,X36)|~epred2_3(X36,X35,X34)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_42])])])])).
% 5.14/1.22 cnf(c_0_47, negated_conjecture, (smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))|smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 5.14/1.22 cnf(c_0_48, negated_conjecture, (greater_or_equal(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 5.14/1.22 cnf(c_0_49, negated_conjecture, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|~epred1_3(esk2_0,esk3_0,esk1_0)|~greater(capability(esk1_0,esk3_0),capability(esk1_0,esk2_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_45])).
% 5.14/1.22 cnf(c_0_50, 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_46])).
% 5.14/1.22 cnf(c_0_51, negated_conjecture, (smaller_or_equal(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))), inference(cn,[status(thm)],[c_0_47])).
% 5.14/1.22 cnf(c_0_52, negated_conjecture, (greater_or_equal(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))), inference(csr,[status(thm)],[c_0_48, c_0_16])).
% 5.14/1.22 fof(c_0_53, plain, ![X1, X4, X5]:((((organization(X1)&~has_immunity(X1,X4))&~has_immunity(X1,X5))=>epred1_3(X4,X5,X1))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[assumption_4]), c_0_21])).
% 5.14/1.22 cnf(c_0_54, plain, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|~epred2_3(esk2_0,esk3_0,esk1_0)|~epred1_3(esk2_0,esk3_0,esk1_0)|~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_49, c_0_50]), c_0_51])])).
% 5.14/1.22 cnf(c_0_55, negated_conjecture, (stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_19, c_0_52])).
% 5.14/1.22 fof(c_0_56, plain, ![X13, X14, X15]:((~organization(X13)|has_immunity(X13,X14)|has_immunity(X13,X15)|epred1_3(X14,X15,X13))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_53])])])).
% 5.14/1.22 fof(c_0_57, axiom, ![X1, X4, X5]:((organization(X1)=>epred2_3(X4,X5,X1))), inference(apply_def,[status(thm)],[assumption_5, c_0_36])).
% 5.14/1.22 cnf(c_0_58, negated_conjecture, (stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)|position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|~epred2_3(esk2_0,esk3_0,esk1_0)|~epred1_3(esk2_0,esk3_0,esk1_0)), inference(spm,[status(thm)],[c_0_54, c_0_55])).
% 5.14/1.22 cnf(c_0_59, plain, (has_immunity(X1,X2)|has_immunity(X1,X3)|epred1_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_56])).
% 5.14/1.22 cnf(c_0_60, negated_conjecture, (~has_immunity(esk1_0,esk3_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 5.14/1.22 cnf(c_0_61, negated_conjecture, (~has_immunity(esk1_0,esk2_0)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 5.14/1.22 fof(c_0_62, plain, ![X26, X27, X28]:((~organization(X26)|epred2_3(X27,X28,X26))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_57])])])).
% 5.14/1.22 cnf(c_0_63, negated_conjecture, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)|~epred2_3(esk2_0,esk3_0,esk1_0)), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_25])]), c_0_60]), c_0_61])).
% 5.14/1.22 cnf(c_0_64, plain, (epred2_3(X2,X3,X1)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 5.14/1.22 cnf(c_0_65, 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])).
% 5.14/1.22 cnf(c_0_66, negated_conjecture, (stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)|position(esk1_0,esk2_0)=position(esk1_0,esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_25])])).
% 5.14/1.22 cnf(c_0_67, plain, (greater_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_12])).
% 5.14/1.22 cnf(c_0_68, plain, (stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)|smaller(hazard_of_mortality(esk1_0,X1),hazard_of_mortality(esk1_0,esk2_0))|~epred1_3(esk2_0,X1,esk1_0)|~greater(capability(esk1_0,X1),capability(esk1_0,esk2_0))|~greater_or_equal(position(esk1_0,X1),position(esk1_0,esk3_0))), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 5.14/1.22 cnf(c_0_69, plain, (greater_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_67])).
% 5.14/1.22 cnf(c_0_70, plain, (stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)|~epred1_3(esk2_0,esk3_0,esk1_0)|~greater(capability(esk1_0,esk3_0),capability(esk1_0,esk2_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_69]), c_0_45])).
% 5.14/1.22 cnf(c_0_71, 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_46])).
% 5.14/1.22 cnf(c_0_72, plain, (stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)|~epred2_3(esk2_0,esk3_0,esk1_0)|~epred1_3(esk2_0,esk3_0,esk1_0)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_50]), c_0_51])]), c_0_55])).
% 5.14/1.22 fof(c_0_73, plain, ![X24, X25]:(((~smaller_or_equal(X24,X25)|(smaller(X24,X25)|X24=X25))&((~smaller(X24,X25)|smaller_or_equal(X24,X25))&(X24!=X25|smaller_or_equal(X24,X25))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_smaller_or_equal])])])])).
% 5.14/1.22 cnf(c_0_74, plain, (greater(capability(X1,X2),capability(X1,X3))|~epred2_3(X2,X3,X1)|~greater(internal_friction(X1,X3),internal_friction(X1,X2))|~smaller_or_equal(stock_of_knowledge(X1,X3),stock_of_knowledge(X1,X2))), inference(spm,[status(thm)],[c_0_33, c_0_71])).
% 5.14/1.22 cnf(c_0_75, plain, (stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)|~epred2_3(esk2_0,esk3_0,esk1_0)), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_59]), c_0_25])]), c_0_60]), c_0_61])).
% 5.14/1.22 cnf(c_0_76, plain, (smaller_or_equal(X1,X2)|X1!=X2), inference(split_conjunct,[status(thm)],[c_0_73])).
% 5.14/1.22 cnf(c_0_77, plain, (smaller(X1,X2)|X1=X2|~smaller_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_73])).
% 5.14/1.22 cnf(c_0_78, plain, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|~epred2_3(esk3_0,esk2_0,esk1_0)|~epred1_3(esk2_0,esk3_0,esk1_0)|~greater(internal_friction(esk1_0,esk2_0),internal_friction(esk1_0,esk3_0))|~smaller_or_equal(stock_of_knowledge(esk1_0,esk2_0),stock_of_knowledge(esk1_0,esk3_0))), inference(spm,[status(thm)],[c_0_49, c_0_74])).
% 5.14/1.22 cnf(c_0_79, plain, (stock_of_knowledge(esk1_0,esk2_0)=stock_of_knowledge(esk1_0,esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_64]), c_0_25])])).
% 5.14/1.22 cnf(c_0_80, plain, (smaller_or_equal(X1,X1)), inference(er,[status(thm)],[c_0_76])).
% 5.14/1.22 cnf(c_0_81, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|smaller(internal_friction(esk1_0,esk3_0),internal_friction(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_77, c_0_51])).
% 5.14/1.22 cnf(c_0_82, plain, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|~epred2_3(esk3_0,esk2_0,esk1_0)|~epred1_3(esk2_0,esk3_0,esk1_0)|~greater(internal_friction(esk1_0,esk2_0),internal_friction(esk1_0,esk3_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_78, c_0_79]), c_0_80])])).
% 5.14/1.22 cnf(c_0_83, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|greater(internal_friction(esk1_0,esk2_0),internal_friction(esk1_0,esk3_0))), inference(spm,[status(thm)],[c_0_33, c_0_81])).
% 5.14/1.22 cnf(c_0_84, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|~epred2_3(esk3_0,esk2_0,esk1_0)|~epred1_3(esk2_0,esk3_0,esk1_0)), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 5.14/1.22 cnf(c_0_85, negated_conjecture, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|~epred2_3(esk3_0,esk2_0,esk1_0)), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_59]), c_0_25])]), c_0_60]), c_0_61])).
% 5.14/1.22 cnf(c_0_86, plain, (~organization(X1)|~greater(position(X1,X2),position(X1,X3))|~greater(external_ties(X1,X3),external_ties(X1,X2))), inference(spm,[status(thm)],[c_0_27, c_0_18])).
% 5.14/1.22 cnf(c_0_87, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|position(esk1_0,esk2_0)=position(esk1_0,esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_64]), c_0_25])])).
% 5.14/1.22 cnf(c_0_88, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|~greater(position(esk1_0,esk3_0),position(esk1_0,X1))|~greater(external_ties(esk1_0,X1),external_ties(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_87]), c_0_25])])).
% 5.14/1.22 cnf(c_0_89, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|greater(position(esk1_0,X1),position(esk1_0,esk3_0))|~greater(external_ties(esk1_0,X1),external_ties(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_87]), c_0_25])])).
% 5.14/1.22 cnf(c_0_90, negated_conjecture, (greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk2_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 5.14/1.22 cnf(c_0_91, plain, (capability(X1,X2)=capability(X1,X3)|stock_of_knowledge(X1,X2)!=stock_of_knowledge(X1,X3)|internal_friction(X1,X2)!=internal_friction(X1,X3)|~epred2_3(X3,X2,X1)), inference(split_conjunct,[status(thm)],[c_0_46])).
% 5.14/1.22 cnf(c_0_92, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|~greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_88, c_0_89])).
% 5.14/1.22 cnf(c_0_93, negated_conjecture, (greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk3_0))), inference(rw,[status(thm)],[c_0_90, c_0_79])).
% 5.14/1.22 cnf(c_0_94, plain, (capability(X1,X2)=capability(X1,X3)|stock_of_knowledge(X1,X2)!=stock_of_knowledge(X1,X3)|internal_friction(X1,X2)!=internal_friction(X1,X3)|~organization(X1)), inference(spm,[status(thm)],[c_0_91, c_0_64])).
% 5.14/1.22 cnf(c_0_95, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)|greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk3_0))), inference(spm,[status(thm)],[c_0_92, c_0_93])).
% 5.14/1.22 cnf(c_0_96, negated_conjecture, (capability(esk1_0,X1)=capability(esk1_0,X2)|stock_of_knowledge(esk1_0,X1)!=stock_of_knowledge(esk1_0,X2)|internal_friction(esk1_0,X1)!=internal_friction(esk1_0,X2)), inference(spm,[status(thm)],[c_0_94, c_0_25])).
% 5.14/1.22 cnf(c_0_97, negated_conjecture, (internal_friction(esk1_0,esk2_0)=internal_friction(esk1_0,esk3_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_95]), c_0_95])).
% 5.14/1.22 cnf(c_0_98, negated_conjecture, (capability(esk1_0,esk2_0)=capability(esk1_0,X1)|stock_of_knowledge(esk1_0,esk3_0)!=stock_of_knowledge(esk1_0,X1)|internal_friction(esk1_0,esk3_0)!=internal_friction(esk1_0,X1)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_97]), c_0_79])).
% 5.14/1.22 cnf(c_0_99, plain, (smaller(hazard_of_mortality(esk1_0,X1),hazard_of_mortality(esk1_0,X2))|stock_of_knowledge(esk1_0,esk3_0)!=stock_of_knowledge(esk1_0,X1)|internal_friction(esk1_0,esk3_0)!=internal_friction(esk1_0,X1)|~epred1_3(X2,X1,esk1_0)|~greater(position(esk1_0,X1),position(esk1_0,X2))|~greater_or_equal(capability(esk1_0,esk2_0),capability(esk1_0,X2))), inference(spm,[status(thm)],[c_0_37, c_0_98])).
% 5.14/1.22 cnf(c_0_100, plain, (smaller(hazard_of_mortality(esk1_0,X1),hazard_of_mortality(esk1_0,esk2_0))|stock_of_knowledge(esk1_0,esk3_0)!=stock_of_knowledge(esk1_0,X1)|internal_friction(esk1_0,esk3_0)!=internal_friction(esk1_0,X1)|~epred1_3(esk2_0,X1,esk1_0)|~greater(position(esk1_0,X1),position(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_99, c_0_69])).
% 5.14/1.22 cnf(c_0_101, negated_conjecture, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)|~epred1_3(esk2_0,esk3_0,esk1_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_44]), c_0_45])).
% 5.14/1.22 cnf(c_0_102, negated_conjecture, (position(esk1_0,esk2_0)=position(esk1_0,esk3_0)), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_59]), c_0_25])]), c_0_60]), c_0_61])).
% 5.14/1.22 cnf(c_0_103, negated_conjecture, (~greater(position(esk1_0,esk3_0),position(esk1_0,X1))|~greater(external_ties(esk1_0,X1),external_ties(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_102]), c_0_25])])).
% 5.14/1.22 cnf(c_0_104, negated_conjecture, (greater(position(esk1_0,X1),position(esk1_0,esk3_0))|~greater(external_ties(esk1_0,X1),external_ties(esk1_0,esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_102]), c_0_25])])).
% 5.14/1.22 cnf(c_0_105, negated_conjecture, (~greater(external_ties(esk1_0,esk3_0),external_ties(esk1_0,esk2_0))), inference(spm,[status(thm)],[c_0_103, c_0_104])).
% 5.14/1.22 cnf(c_0_106, negated_conjecture, (greater(stock_of_knowledge(esk1_0,esk3_0),stock_of_knowledge(esk1_0,esk3_0))), inference(sr,[status(thm)],[c_0_93, c_0_105])).
% 5.14/1.22 cnf(c_0_107, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_106]), c_0_106])]), ['proof']).
% 5.14/1.22 % SZS output end Proof
% 5.14/1.22 % User time : 0.697 s
% 5.14/1.22 % System time : 0.021 s
% 5.14/1.22 % Total time : 0.718 s
% 5.14/1.22 % User time : 0.699 s
% 5.14/1.22 % System time : 0.024 s
% 5.14/1.22 % Total time : 0.723 s
% 5.14/1.22
%------------------------------------------------------------------------------