%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT055+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n003.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:35 AM UTC 2026
% Result : Theorem 0.51s 0.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT055+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.05 % Command : java -jar mcs_scs.jar %d %s
% 0.17/0.42 % Computer : n003.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 7 13:27:54 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.26/0.59 start to proof:theBenchmark.p
% 0.51/0.77 % Version : CSI_E---1.1
% 0.51/0.77 % Problem : theBenchmark.p
% 0.51/0.77 % Proof found!
% 0.51/0.77 % SZS status Theorem for theBenchmark.p
% 0.51/0.77 % SZS output start Proof
% 0.51/0.77 fof(definition_2, axiom, ![X1, X5, X4]:((dissimilar(X1,X5,X4)<=>(organization(X1)&~((is_aligned(X1,X5)<=>is_aligned(X1,X4)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', definition_2)).
% 0.51/0.77 fof(assumption_15, axiom, ![X1, X5, X4]:(((organization(X1)&age(X1,X5)=zero)=>(greater(age(X1,X4),sigma)<=>dissimilar(X1,X5,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_15)).
% 0.51/0.77 fof(assumption_13, axiom, ![X1, X4]:(((organization(X1)&age(X1,X4)=zero)=>is_aligned(X1,X4))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_13)).
% 0.51/0.77 fof(lemma_8, conjecture, ![X1, X5, X6, X7, X8]:((((((((((organization(X1)&has_endowment(X1))&age(X1,X5)=zero)&smaller_or_equal(age(X1,X6),eta))&greater(age(X1,X7),eta))&smaller_or_equal(age(X1,X7),sigma))&greater(age(X1,X8),sigma))&greater(sigma,eta))&greater(eta,zero))=>((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', lemma_8)).
% 0.51/0.77 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.51/0.77 fof(definition_smaller, axiom, ![X1, X2]:((smaller(X1,X2)<=>greater(X2,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/MGT001+0.ax', definition_smaller)).
% 0.51/0.77 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)).
% 0.51/0.77 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.51/0.77 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.51/0.77 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.51/0.77 fof(assumption_16, axiom, ![X1, X5, X4]:(((((organization(X1)&~(has_immunity(X1,X5)))&~(has_immunity(X1,X4)))&greater(capability(X1,X4),capability(X1,X5)))=>greater(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_16)).
% 0.51/0.77 fof(assumption_14, axiom, ![X1, X5, X4]:((((organization(X1)&is_aligned(X1,X5))&~(is_aligned(X1,X4)))=>greater(capability(X1,X5),capability(X1,X4)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_14)).
% 0.51/0.77 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.51/0.77 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)).
% 0.51/0.77 fof(c_0_14, plain, ![X34, X35, X36]:((((organization(X34)|~dissimilar(X34,X35,X36))&((~is_aligned(X34,X35)|~is_aligned(X34,X36)|~dissimilar(X34,X35,X36))&(is_aligned(X34,X35)|is_aligned(X34,X36)|~dissimilar(X34,X35,X36))))&((~is_aligned(X34,X35)|is_aligned(X34,X36)|~organization(X34)|dissimilar(X34,X35,X36))&(~is_aligned(X34,X36)|is_aligned(X34,X35)|~organization(X34)|dissimilar(X34,X35,X36))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[definition_2])])])])).
% 0.51/0.77 fof(c_0_15, plain, ![X42, X43, X44]:(((~greater(age(X42,X44),sigma)|dissimilar(X42,X43,X44)|(~organization(X42)|age(X42,X43)!=zero))&(~dissimilar(X42,X43,X44)|greater(age(X42,X44),sigma)|(~organization(X42)|age(X42,X43)!=zero)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_15])])])])).
% 0.51/0.77 fof(c_0_16, plain, ![X37, X38]:((~organization(X37)|age(X37,X38)!=zero|is_aligned(X37,X38))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[assumption_13])])])).
% 0.51/0.77 fof(c_0_17, negated_conjecture, ~(![X1, X5, X6, X7, X8]:((((((((((organization(X1)&has_endowment(X1))&age(X1,X5)=zero)&smaller_or_equal(age(X1,X6),eta))&greater(age(X1,X7),eta))&smaller_or_equal(age(X1,X7),sigma))&greater(age(X1,X8),sigma))&greater(sigma,eta))&greater(eta,zero))=>((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)],[lemma_8])).
% 0.51/0.77 cnf(c_0_18, plain, (~is_aligned(X1,X2)|~is_aligned(X1,X3)|~dissimilar(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.51/0.77 cnf(c_0_19, plain, (dissimilar(X1,X3,X2)|~greater(age(X1,X2),sigma)|~organization(X1)|age(X1,X3)!=zero), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.51/0.77 cnf(c_0_20, plain, (is_aligned(X1,X2)|~organization(X1)|age(X1,X2)!=zero), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.51/0.77 fof(c_0_21, negated_conjecture, (((((((((organization(esk3_0)&has_endowment(esk3_0))&age(esk3_0,esk4_0)=zero)&smaller_or_equal(age(esk3_0,esk5_0),eta))&greater(age(esk3_0,esk6_0),eta))&smaller_or_equal(age(esk3_0,esk6_0),sigma))&greater(age(esk3_0,esk7_0),sigma))&greater(sigma,eta))&greater(eta,zero))&(~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_17])])])])).
% 0.51/0.77 cnf(c_0_22, plain, (age(X1,X2)!=zero|~is_aligned(X1,X3)|~organization(X1)|~greater(age(X1,X3),sigma)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_19]), c_0_20])).
% 0.51/0.77 cnf(c_0_23, negated_conjecture, (age(esk3_0,esk4_0)=zero), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 cnf(c_0_24, negated_conjecture, (organization(esk3_0)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 fof(c_0_25, 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.51/0.77 cnf(c_0_26, plain, (is_aligned(X1,X3)|dissimilar(X1,X3,X2)|~is_aligned(X1,X2)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.51/0.77 cnf(c_0_27, negated_conjecture, (~is_aligned(esk3_0,X1)|~greater(age(esk3_0,X1),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_23]), c_0_24])])).
% 0.51/0.77 fof(c_0_28, 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.51/0.77 fof(c_0_29, plain, ![X20, X21]:((smaller(X20,X21)|X20=X21|greater(X20,X21))), inference(variable_rename,[status(thm)],[meaning_postulate_greater_comparable])).
% 0.51/0.77 fof(c_0_30, 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_25])])])])])])])).
% 0.51/0.77 fof(c_0_31, 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.51/0.77 cnf(c_0_32, plain, (greater(age(X1,X3),sigma)|~dissimilar(X1,X2,X3)|~organization(X1)|age(X1,X2)!=zero), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.51/0.77 cnf(c_0_33, plain, (organization(X1)|~dissimilar(X1,X2,X3)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.51/0.77 cnf(c_0_34, plain, (is_aligned(X1,X2)|dissimilar(X1,X2,X3)|age(X1,X3)!=zero|~organization(X1)), inference(spm,[status(thm)],[c_0_26, c_0_20])).
% 0.51/0.77 cnf(c_0_35, negated_conjecture, (age(esk3_0,X1)!=zero|~greater(age(esk3_0,X1),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_20]), c_0_24])])).
% 0.51/0.77 cnf(c_0_36, plain, (greater(X2,X1)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.51/0.77 cnf(c_0_37, plain, (smaller(X1,X2)|X1=X2|greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.51/0.77 cnf(c_0_38, plain, (has_immunity(X1,X2)|~smaller_or_equal(age(X1,X2),eta)|~has_endowment(X1)), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.51/0.77 cnf(c_0_39, negated_conjecture, (has_endowment(esk3_0)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 cnf(c_0_40, plain, (smaller_or_equal(X1,X2)|~smaller(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.51/0.77 cnf(c_0_41, plain, (smaller(X2,X1)|~greater(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.51/0.77 fof(c_0_42, 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.51/0.77 cnf(c_0_43, plain, (greater(age(X1,X2),sigma)|age(X1,X3)!=zero|~dissimilar(X1,X3,X2)), inference(csr,[status(thm)],[c_0_32, c_0_33])).
% 0.51/0.77 cnf(c_0_44, negated_conjecture, (is_aligned(esk3_0,X1)|dissimilar(esk3_0,X1,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_23]), c_0_24])])).
% 0.51/0.77 cnf(c_0_45, negated_conjecture, (~greater(zero,sigma)), inference(spm,[status(thm)],[c_0_35, c_0_23])).
% 0.51/0.77 cnf(c_0_46, 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_21])).
% 0.51/0.77 cnf(c_0_47, plain, (X1=X2|greater(X1,X2)|greater(X2,X1)), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.51/0.77 fof(c_0_48, 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.51/0.77 cnf(c_0_49, negated_conjecture, (has_immunity(esk3_0,esk4_0)|~smaller_or_equal(zero,eta)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_23]), c_0_39])])).
% 0.51/0.77 cnf(c_0_50, plain, (smaller_or_equal(X1,X2)|~greater(X2,X1)), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 0.51/0.77 cnf(c_0_51, negated_conjecture, (greater(eta,zero)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 fof(c_0_52, 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_42])])])).
% 0.51/0.77 cnf(c_0_53, negated_conjecture, (smaller_or_equal(age(esk3_0,esk5_0),eta)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 cnf(c_0_54, plain, (is_aligned(X1,X3)|dissimilar(X1,X2,X3)|~is_aligned(X1,X2)|~organization(X1)), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.51/0.77 cnf(c_0_55, negated_conjecture, (is_aligned(esk3_0,X1)|age(esk3_0,X1)!=zero), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_23]), c_0_45])).
% 0.51/0.77 cnf(c_0_56, negated_conjecture, (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,esk7_0))|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,esk5_0))), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 0.51/0.77 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_48])).
% 0.51/0.77 cnf(c_0_58, negated_conjecture, (has_immunity(esk3_0,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_50]), c_0_51])])).
% 0.51/0.77 cnf(c_0_59, 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_52])).
% 0.51/0.77 cnf(c_0_60, negated_conjecture, (has_immunity(esk3_0,esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_53]), c_0_39])])).
% 0.51/0.77 cnf(c_0_61, plain, (~greater(age(X1,X2),eta)|~has_immunity(X1,X2)|~has_endowment(X1)), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.51/0.77 cnf(c_0_62, negated_conjecture, (greater(age(esk3_0,esk6_0),eta)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 fof(c_0_63, plain, ![X1, X5, X4]:(((((organization(X1)&~has_immunity(X1,X5))&~has_immunity(X1,X4))&greater(capability(X1,X4),capability(X1,X5)))=>greater(hazard_of_mortality(X1,X5),hazard_of_mortality(X1,X4)))), inference(fof_simplification,[status(thm)],[assumption_16])).
% 0.51/0.77 fof(c_0_64, plain, ![X1, X5, X4]:((((organization(X1)&is_aligned(X1,X5))&~is_aligned(X1,X4))=>greater(capability(X1,X5),capability(X1,X4)))), inference(fof_simplification,[status(thm)],[assumption_14])).
% 0.51/0.77 cnf(c_0_65, negated_conjecture, (is_aligned(esk3_0,X1)|dissimilar(esk3_0,X2,X1)|age(esk3_0,X2)!=zero), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_55]), c_0_24])])).
% 0.51/0.77 fof(c_0_66, 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.51/0.77 cnf(c_0_67, negated_conjecture, (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,esk7_0))|hazard_of_mortality(esk3_0,X1)!=hazard_of_mortality(esk3_0,esk5_0)|~has_immunity(esk3_0,X1)|~greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_57]), c_0_58]), c_0_24])])).
% 0.51/0.77 cnf(c_0_68, 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_59, c_0_60]), c_0_24])])).
% 0.51/0.77 cnf(c_0_69, negated_conjecture, (~has_immunity(esk3_0,esk6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_39])])).
% 0.51/0.77 fof(c_0_70, plain, ![X45, X46, X47]:((~organization(X45)|has_immunity(X45,X46)|has_immunity(X45,X47)|~greater(capability(X45,X47),capability(X45,X46))|greater(hazard_of_mortality(X45,X46),hazard_of_mortality(X45,X47)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_63])])])).
% 0.51/0.77 fof(c_0_71, plain, ![X39, X40, X41]:((~organization(X39)|~is_aligned(X39,X40)|is_aligned(X39,X41)|greater(capability(X39,X40),capability(X39,X41)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_64])])])).
% 0.51/0.77 cnf(c_0_72, negated_conjecture, (is_aligned(esk3_0,X1)|dissimilar(esk3_0,esk4_0,X1)), inference(spm,[status(thm)],[c_0_65, c_0_23])).
% 0.51/0.77 cnf(c_0_73, plain, (greater(X1,X3)|~greater(X1,X2)|~greater(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_66])).
% 0.51/0.77 cnf(c_0_74, negated_conjecture, (greater(sigma,eta)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 fof(c_0_75, 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])])])).
% 0.51/0.77 cnf(c_0_76, negated_conjecture, (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,esk7_0))|hazard_of_mortality(esk3_0,X1)!=hazard_of_mortality(esk3_0,esk5_0)|~has_immunity(esk3_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_68]), c_0_69])).
% 0.51/0.77 cnf(c_0_77, plain, (has_immunity(X1,X2)|has_immunity(X1,X3)|greater(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~organization(X1)|~greater(capability(X1,X3),capability(X1,X2))), inference(split_conjunct,[status(thm)],[c_0_70])).
% 0.51/0.77 cnf(c_0_78, plain, (is_aligned(X1,X3)|greater(capability(X1,X2),capability(X1,X3))|~organization(X1)|~is_aligned(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_71])).
% 0.51/0.77 cnf(c_0_79, negated_conjecture, (is_aligned(esk3_0,X1)|greater(age(esk3_0,X1),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_72]), c_0_23])])).
% 0.51/0.77 cnf(c_0_80, negated_conjecture, (greater(X1,eta)|~greater(X1,sigma)), inference(spm,[status(thm)],[c_0_73, c_0_74])).
% 0.51/0.77 cnf(c_0_81, negated_conjecture, (greater(age(esk3_0,esk7_0),sigma)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 cnf(c_0_82, plain, (~greater(X1,X2)|~greater(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_75])).
% 0.51/0.77 cnf(c_0_83, negated_conjecture, (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,esk7_0))), inference(spm,[status(thm)],[c_0_76, c_0_60])).
% 0.51/0.77 cnf(c_0_84, plain, (has_immunity(X1,X2)|greater(hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3))|~organization(X1)|~greater(capability(X1,X3),capability(X1,X2))), inference(csr,[status(thm)],[c_0_77, c_0_59])).
% 0.51/0.77 cnf(c_0_85, negated_conjecture, (is_aligned(esk3_0,X1)|greater(capability(esk3_0,X2),capability(esk3_0,X1))|greater(age(esk3_0,X2),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_78, c_0_79]), c_0_24])])).
% 0.51/0.77 cnf(c_0_86, negated_conjecture, (greater(age(esk3_0,esk7_0),eta)), inference(spm,[status(thm)],[c_0_80, c_0_81])).
% 0.51/0.77 cnf(c_0_87, negated_conjecture, (hazard_of_mortality(esk3_0,esk7_0)=hazard_of_mortality(esk3_0,esk6_0)|~greater(hazard_of_mortality(esk3_0,esk7_0),hazard_of_mortality(esk3_0,esk6_0))), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 0.51/0.77 cnf(c_0_88, negated_conjecture, (is_aligned(esk3_0,X1)|has_immunity(esk3_0,X1)|greater(hazard_of_mortality(esk3_0,X1),hazard_of_mortality(esk3_0,X2))|greater(age(esk3_0,X2),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_85]), c_0_24])])).
% 0.51/0.77 cnf(c_0_89, negated_conjecture, (~has_immunity(esk3_0,esk7_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_86]), c_0_39])])).
% 0.51/0.77 cnf(c_0_90, negated_conjecture, (hazard_of_mortality(esk3_0,esk7_0)=hazard_of_mortality(esk3_0,esk6_0)|is_aligned(esk3_0,esk7_0)|greater(age(esk3_0,esk6_0),sigma)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_88]), c_0_89])).
% 0.51/0.77 cnf(c_0_91, negated_conjecture, (hazard_of_mortality(esk3_0,esk7_0)=hazard_of_mortality(esk3_0,esk6_0)|greater(age(esk3_0,esk6_0),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_90]), c_0_81])])).
% 0.51/0.77 cnf(c_0_92, negated_conjecture, (greater(hazard_of_mortality(esk3_0,esk6_0),hazard_of_mortality(esk3_0,esk5_0))|greater(age(esk3_0,esk6_0),sigma)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_91]), c_0_89])).
% 0.51/0.77 cnf(c_0_93, plain, (smaller(X1,X2)|X1=X2|~smaller_or_equal(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.51/0.77 cnf(c_0_94, negated_conjecture, (smaller_or_equal(age(esk3_0,esk6_0),sigma)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.51/0.77 cnf(c_0_95, negated_conjecture, (is_aligned(esk3_0,esk7_0)|greater(age(esk3_0,esk6_0),sigma)|hazard_of_mortality(esk3_0,esk4_0)!=hazard_of_mortality(esk3_0,esk5_0)), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_88]), c_0_89]), c_0_92])).
% 0.51/0.77 cnf(c_0_96, negated_conjecture, (age(esk3_0,esk6_0)=sigma|smaller(age(esk3_0,esk6_0),sigma)), inference(spm,[status(thm)],[c_0_93, c_0_94])).
% 0.51/0.77 cnf(c_0_97, negated_conjecture, (is_aligned(esk3_0,esk7_0)|greater(age(esk3_0,esk6_0),sigma)|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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95, c_0_57]), c_0_58]), c_0_24])])).
% 0.51/0.77 cnf(c_0_98, negated_conjecture, (age(esk3_0,esk6_0)=sigma|greater(sigma,age(esk3_0,esk6_0))), inference(spm,[status(thm)],[c_0_36, c_0_96])).
% 0.51/0.77 cnf(c_0_99, negated_conjecture, (is_aligned(esk3_0,esk7_0)|greater(age(esk3_0,esk6_0),sigma)), inference(spm,[status(thm)],[c_0_97, c_0_60])).
% 0.51/0.77 cnf(c_0_100, negated_conjecture, (age(esk3_0,esk6_0)=sigma|~greater(age(esk3_0,esk6_0),sigma)), inference(spm,[status(thm)],[c_0_82, c_0_98])).
% 0.51/0.77 cnf(c_0_101, negated_conjecture, (greater(age(esk3_0,esk6_0),sigma)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_99]), c_0_81])])).
% 0.51/0.77 cnf(c_0_102, negated_conjecture, (age(esk3_0,esk6_0)=sigma), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_100, c_0_101])])).
% 0.51/0.77 cnf(c_0_103, negated_conjecture, (greater(sigma,sigma)), inference(rw,[status(thm)],[c_0_101, c_0_102])).
% 0.51/0.77 cnf(c_0_104, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_103]), c_0_103])]), ['proof']).
% 0.51/0.77 % SZS output end Proof
% 0.51/0.77 % User time : 0.120 s
% 0.51/0.77 % System time : 0.007 s
% 0.51/0.77 % Total time : 0.127 s
% 0.51/0.77 % User time : 0.469 s
% 0.51/0.77 % System time : 0.027 s
% 0.51/0.77 % Total time : 0.496 s
% 0.51/0.77
%------------------------------------------------------------------------------