%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT060+1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n006.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:24:24 AM UTC 2026 % Result : Theorem 0.45s 0.73s % Output : Proof 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT060+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.35 % Computer : n006.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 13:33:31 UTC 2026 % 0.09/0.35 % CPUTime : % 0.45/0.73 (* PROOF-FOUND *) % 0.45/0.73 % SZS status Theorem % 0.45/0.73 (* BEGIN-PROOF *) % 0.45/0.73 % SZS output start Proof % 0.45/0.73 Theorem assumption_3 : (forall X : zenon_U, (forall T0 : zenon_U, (forall T : zenon_U, (((organization X)/\((has_immunity X T0)/\(~(has_immunity X T))))->(greater (hazard_of_mortality X T) (hazard_of_mortality X T0)))))). % 0.45/0.73 Proof. % 0.45/0.73 assert (zenon_L1_ : forall (zenon_TT_r : zenon_U) (zenon_TX_s : zenon_U), (((~(is_aligned zenon_TX_s zenon_TT_r))/\(~(positional_advantage zenon_TX_s zenon_TT_r)))->((hazard_of_mortality zenon_TX_s zenon_TT_r) = (high))) -> (~(positional_advantage zenon_TX_s zenon_TT_r)) -> (~(is_aligned zenon_TX_s zenon_TT_r)) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (high))) -> False). % 0.45/0.73 do 2 intro. intros zenon_Hd zenon_He zenon_Hf zenon_H10. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_Hd); [ zenon_intro zenon_H14 | zenon_intro zenon_H13 ]. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H14); [ zenon_intro zenon_H16 | zenon_intro zenon_H15 ]. % 0.45/0.73 exact (zenon_H16 zenon_Hf). % 0.45/0.73 exact (zenon_H15 zenon_He). % 0.45/0.73 exact (zenon_H10 zenon_H13). % 0.45/0.73 (* end of lemma zenon_L1_ *) % 0.45/0.73 assert (zenon_L2_ : forall (zenon_TT_r : zenon_U) (zenon_TX_s : zenon_U), (forall T : zenon_U, ((organization zenon_TX_s)->(((has_immunity zenon_TX_s T)->((hazard_of_mortality zenon_TX_s T) = (very_low)))/\((~(has_immunity zenon_TX_s T))->((((is_aligned zenon_TX_s T)/\(positional_advantage zenon_TX_s T))->((hazard_of_mortality zenon_TX_s T) = (low)))/\((((~(is_aligned zenon_TX_s T))/\(positional_advantage zenon_TX_s T))->((hazard_of_mortality zenon_TX_s T) = (mod1)))/\((((is_aligned zenon_TX_s T)/\(~(positional_advantage zenon_TX_s T)))->((hazard_of_mortality zenon_TX_s T) = (mod2)))/\(((~(is_aligned zenon_TX_s T))/\(~(positional_advantage zenon_TX_s T)))->((hazard_of_mortality zenon_TX_s T) = (high)))))))))) -> (organization zenon_TX_s) -> (~(has_immunity zenon_TX_s zenon_TT_r)) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod1))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (high))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod2))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (low))) -> False). % 0.45/0.73 do 2 intro. intros zenon_H17 zenon_H18 zenon_H19 zenon_H1a zenon_H10 zenon_H1b zenon_H1c. % 0.45/0.73 generalize (zenon_H17 zenon_TT_r). zenon_intro zenon_H1d. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H1d); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 0.45/0.73 exact (zenon_H1f zenon_H18). % 0.45/0.73 apply (zenon_and_s _ _ zenon_H1e). zenon_intro zenon_H21. zenon_intro zenon_H20. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H20); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 0.45/0.73 exact (zenon_H23 zenon_H19). % 0.45/0.73 apply (zenon_and_s _ _ zenon_H22). zenon_intro zenon_H25. zenon_intro zenon_H24. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H24). zenon_intro zenon_H27. zenon_intro zenon_H26. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H26). zenon_intro zenon_H28. zenon_intro zenon_Hd. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H25); [ zenon_intro zenon_H2a | zenon_intro zenon_H29 ]. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H2a); [ zenon_intro zenon_Hf | zenon_intro zenon_He ]. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H27); [ zenon_intro zenon_H2c | zenon_intro zenon_H2b ]. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H2c); [ zenon_intro zenon_H16 | zenon_intro zenon_He ]. % 0.45/0.73 exact (zenon_H16 zenon_Hf). % 0.45/0.73 apply (zenon_L1_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 exact (zenon_H1a zenon_H2b). % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H28); [ zenon_intro zenon_H2e | zenon_intro zenon_H2d ]. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H2e); [ zenon_intro zenon_Hf | zenon_intro zenon_H15 ]. % 0.45/0.73 apply (zenon_L1_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 exact (zenon_H15 zenon_He). % 0.45/0.73 exact (zenon_H1b zenon_H2d). % 0.45/0.73 exact (zenon_H1c zenon_H29). % 0.45/0.73 (* end of lemma zenon_L2_ *) % 0.45/0.73 assert (zenon_L3_ : forall (zenon_TT_r : zenon_U) (zenon_TX_s : zenon_U), (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (low))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod2))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (high))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod1))) -> (~(has_immunity zenon_TX_s zenon_TT_r)) -> (organization zenon_TX_s) -> False). % 0.45/0.73 do 2 intro. intros zenon_H1c zenon_H1b zenon_H10 zenon_H1a zenon_H19 zenon_H18. % 0.45/0.73 generalize (assumption_17 zenon_TX_s). zenon_intro zenon_H17. % 0.45/0.73 apply (zenon_L2_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 (* end of lemma zenon_L3_ *) % 0.45/0.73 assert (zenon_L4_ : (~((low) = (low))) -> False). % 0.45/0.73 do 0 intro. intros zenon_H2f. % 0.45/0.73 apply zenon_H2f. apply refl_equal. % 0.45/0.73 (* end of lemma zenon_L4_ *) % 0.45/0.73 assert (zenon_L5_ : forall (zenon_TT_r : zenon_U) (zenon_TX_s : zenon_U), (organization zenon_TX_s) -> (~(has_immunity zenon_TX_s zenon_TT_r)) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (high))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod2))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (low))) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (low))) -> False). % 0.45/0.73 do 2 intro. intros zenon_H18 zenon_H19 zenon_H10 zenon_H1b zenon_H1c zenon_H30 zenon_H31. % 0.45/0.73 elim (classic ((~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod1)))/\(~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (mod1))))); [ zenon_intro zenon_H32 | zenon_intro zenon_H33 ]. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H32). zenon_intro zenon_H1a. zenon_intro zenon_H34. % 0.45/0.73 apply (zenon_L3_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 cut ((greater (mod1) (low)) = (greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (low))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H31. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact assumption_18b. % 0.45/0.73 cut (((low) = (low))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 0.45/0.73 cut (((mod1) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 0.45/0.73 congruence. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H33); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 0.45/0.73 apply zenon_H37. zenon_intro zenon_H2b. % 0.45/0.73 elim (classic ((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r)) = ((mod1) = (hazard_of_mortality zenon_TX_s zenon_TT_r))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H35. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact zenon_H38. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod1))); [idtac | apply NNPP; zenon_intro zenon_H1a]. % 0.45/0.73 congruence. % 0.45/0.73 exact (zenon_H1a zenon_H2b). % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H36. zenon_intro zenon_H3a. % 0.45/0.73 generalize (zenon_H30 (hazard_of_mortality zenon_TX_s zenon_TT_r)). zenon_intro zenon_H3b. % 0.45/0.73 generalize (zenon_H3b (mod1)). zenon_intro zenon_H3c. % 0.45/0.73 generalize (zenon_H3c (low)). zenon_intro zenon_H3d. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H3d); [ zenon_intro zenon_H34 | zenon_intro zenon_H3e ]. % 0.45/0.73 exact (zenon_H34 zenon_H3a). % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 0.45/0.73 exact (zenon_H40 assumption_18b). % 0.45/0.73 exact (zenon_H31 zenon_H3f). % 0.45/0.73 apply zenon_H2f. apply refl_equal. % 0.45/0.73 (* end of lemma zenon_L5_ *) % 0.45/0.73 assert (zenon_L6_ : forall (zenon_TT_r : zenon_U) (zenon_TX_s : zenon_U), (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (low))) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (high))) -> (~(has_immunity zenon_TX_s zenon_TT_r)) -> (organization zenon_TX_s) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (low))) -> False). % 0.45/0.73 do 2 intro. intros zenon_H1c zenon_H10 zenon_H19 zenon_H18 zenon_H30 zenon_H31. % 0.45/0.73 elim (classic ((~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod2)))/\(~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (mod2))))); [ zenon_intro zenon_H41 | zenon_intro zenon_H42 ]. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H41). zenon_intro zenon_H1b. zenon_intro zenon_H43. % 0.45/0.73 apply (zenon_L5_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 cut ((greater (mod2) (low)) = (greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (low))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H31. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact assumption_18e. % 0.45/0.73 cut (((low) = (low))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 0.45/0.73 cut (((mod2) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H44]. % 0.45/0.73 congruence. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H42); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 0.45/0.73 apply zenon_H46. zenon_intro zenon_H2d. % 0.45/0.73 elim (classic ((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r)) = ((mod2) = (hazard_of_mortality zenon_TX_s zenon_TT_r))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H44. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact zenon_H38. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_H1b]. % 0.45/0.73 congruence. % 0.45/0.73 exact (zenon_H1b zenon_H2d). % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H45. zenon_intro zenon_H47. % 0.45/0.73 generalize (zenon_H30 (hazard_of_mortality zenon_TX_s zenon_TT_r)). zenon_intro zenon_H3b. % 0.45/0.73 generalize (zenon_H3b (mod2)). zenon_intro zenon_H48. % 0.45/0.73 generalize (zenon_H48 (low)). zenon_intro zenon_H49. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H49); [ zenon_intro zenon_H43 | zenon_intro zenon_H4a ]. % 0.45/0.73 exact (zenon_H43 zenon_H47). % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H4a); [ zenon_intro zenon_H4b | zenon_intro zenon_H3f ]. % 0.45/0.73 exact (zenon_H4b assumption_18e). % 0.45/0.73 exact (zenon_H31 zenon_H3f). % 0.45/0.73 apply zenon_H2f. apply refl_equal. % 0.45/0.73 (* end of lemma zenon_L6_ *) % 0.45/0.73 assert (zenon_L7_ : (~((mod2) = (mod2))) -> False). % 0.45/0.73 do 0 intro. intros zenon_H4c. % 0.45/0.73 apply zenon_H4c. apply refl_equal. % 0.45/0.73 (* end of lemma zenon_L7_ *) % 0.45/0.73 assert (zenon_L8_ : forall (zenon_TT_r : zenon_U) (zenon_TX_s : zenon_U), (~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (low))) -> (organization zenon_TX_s) -> (~(has_immunity zenon_TX_s zenon_TT_r)) -> (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (low))) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (mod2))) -> False). % 0.45/0.73 do 2 intro. intros zenon_H31 zenon_H18 zenon_H19 zenon_H1c zenon_H30 zenon_H43. % 0.45/0.73 elim (classic ((~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (high)))/\(~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (high))))); [ zenon_intro zenon_H4d | zenon_intro zenon_H4e ]. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H10. zenon_intro zenon_H4f. % 0.45/0.73 apply (zenon_L6_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 cut ((greater (high) (mod2)) = (greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (mod2))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H43. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact assumption_18d. % 0.45/0.73 cut (((mod2) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 0.45/0.73 cut (((high) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 0.45/0.73 congruence. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H52 | zenon_intro zenon_H51 ]. % 0.45/0.73 apply zenon_H52. zenon_intro zenon_H13. % 0.45/0.73 elim (classic ((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r)) = ((high) = (hazard_of_mortality zenon_TX_s zenon_TT_r))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H50. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact zenon_H38. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (high))); [idtac | apply NNPP; zenon_intro zenon_H10]. % 0.45/0.73 congruence. % 0.45/0.73 exact (zenon_H10 zenon_H13). % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H51. zenon_intro zenon_H53. % 0.45/0.73 generalize (zenon_H30 (hazard_of_mortality zenon_TX_s zenon_TT_r)). zenon_intro zenon_H3b. % 0.45/0.73 generalize (zenon_H3b (high)). zenon_intro zenon_H54. % 0.45/0.73 generalize (zenon_H54 (mod2)). zenon_intro zenon_H55. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H55); [ zenon_intro zenon_H4f | zenon_intro zenon_H56 ]. % 0.45/0.73 exact (zenon_H4f zenon_H53). % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H56); [ zenon_intro zenon_H57 | zenon_intro zenon_H47 ]. % 0.45/0.73 exact (zenon_H57 assumption_18d). % 0.45/0.73 exact (zenon_H43 zenon_H47). % 0.45/0.73 apply zenon_H4c. apply refl_equal. % 0.45/0.73 (* end of lemma zenon_L8_ *) % 0.45/0.73 assert (zenon_L9_ : forall (zenon_TT_r : zenon_U) (zenon_TX_s : zenon_U), (~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (low))) -> (~(has_immunity zenon_TX_s zenon_TT_r)) -> (organization zenon_TX_s) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (low))) -> False). % 0.45/0.73 do 2 intro. intros zenon_H1c zenon_H19 zenon_H18 zenon_H30 zenon_H31. % 0.45/0.73 elim (classic ((~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod2)))/\(~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (mod2))))); [ zenon_intro zenon_H41 | zenon_intro zenon_H42 ]. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H41). zenon_intro zenon_H1b. zenon_intro zenon_H43. % 0.45/0.73 apply (zenon_L8_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 cut ((greater (mod2) (low)) = (greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (low))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H31. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact assumption_18e. % 0.45/0.73 cut (((low) = (low))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 0.45/0.73 cut (((mod2) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H44]. % 0.45/0.73 congruence. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H42); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 0.45/0.73 apply zenon_H46. zenon_intro zenon_H2d. % 0.45/0.73 elim (classic ((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r)) = ((mod2) = (hazard_of_mortality zenon_TX_s zenon_TT_r))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H44. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact zenon_H38. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (mod2))); [idtac | apply NNPP; zenon_intro zenon_H1b]. % 0.45/0.73 congruence. % 0.45/0.73 exact (zenon_H1b zenon_H2d). % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H45. zenon_intro zenon_H47. % 0.45/0.73 generalize (zenon_H30 (hazard_of_mortality zenon_TX_s zenon_TT_r)). zenon_intro zenon_H3b. % 0.45/0.73 generalize (zenon_H3b (mod2)). zenon_intro zenon_H48. % 0.45/0.73 generalize (zenon_H48 (low)). zenon_intro zenon_H49. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H49); [ zenon_intro zenon_H43 | zenon_intro zenon_H4a ]. % 0.45/0.73 exact (zenon_H43 zenon_H47). % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H4a); [ zenon_intro zenon_H4b | zenon_intro zenon_H3f ]. % 0.45/0.73 exact (zenon_H4b assumption_18e). % 0.45/0.73 exact (zenon_H31 zenon_H3f). % 0.45/0.73 apply zenon_H2f. apply refl_equal. % 0.45/0.73 (* end of lemma zenon_L9_ *) % 0.45/0.73 assert (zenon_L10_ : (~((very_low) = (very_low))) -> False). % 0.45/0.73 do 0 intro. intros zenon_H58. % 0.45/0.73 apply zenon_H58. apply refl_equal. % 0.45/0.73 (* end of lemma zenon_L10_ *) % 0.45/0.73 assert (zenon_L11_ : forall (zenon_TT_r : zenon_U) (zenon_TX_s : zenon_U), (organization zenon_TX_s) -> (~(has_immunity zenon_TX_s zenon_TT_r)) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z)))))) -> (~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (very_low))) -> False). % 0.45/0.73 do 2 intro. intros zenon_H18 zenon_H19 zenon_H30 zenon_H59. % 0.45/0.73 elim (classic ((~((hazard_of_mortality zenon_TX_s zenon_TT_r) = (low)))/\(~(greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (low))))); [ zenon_intro zenon_H5a | zenon_intro zenon_H5b ]. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H5a). zenon_intro zenon_H1c. zenon_intro zenon_H31. % 0.45/0.73 apply (zenon_L9_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 cut ((greater (low) (very_low)) = (greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (very_low))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H59. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact assumption_18c. % 0.45/0.73 cut (((very_low) = (very_low))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 0.45/0.73 cut (((low) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 0.45/0.73 congruence. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H5b); [ zenon_intro zenon_H5e | zenon_intro zenon_H5d ]. % 0.45/0.73 apply zenon_H5e. zenon_intro zenon_H29. % 0.45/0.73 elim (classic ((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [ zenon_intro zenon_H38 | zenon_intro zenon_H39 ]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r)) = ((low) = (hazard_of_mortality zenon_TX_s zenon_TT_r))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H5c. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact zenon_H38. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (low))); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 0.45/0.73 congruence. % 0.45/0.73 exact (zenon_H1c zenon_H29). % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 apply zenon_H5d. zenon_intro zenon_H3f. % 0.45/0.73 generalize (zenon_H30 (hazard_of_mortality zenon_TX_s zenon_TT_r)). zenon_intro zenon_H3b. % 0.45/0.73 generalize (zenon_H3b (low)). zenon_intro zenon_H5f. % 0.45/0.73 generalize (zenon_H5f (very_low)). zenon_intro zenon_H60. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H31 | zenon_intro zenon_H61 ]. % 0.45/0.73 exact (zenon_H31 zenon_H3f). % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 0.45/0.73 exact (zenon_H63 assumption_18c). % 0.45/0.73 exact (zenon_H59 zenon_H62). % 0.45/0.73 apply zenon_H58. apply refl_equal. % 0.45/0.73 (* end of lemma zenon_L11_ *) % 0.45/0.73 apply NNPP. intro zenon_G. % 0.45/0.73 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((greater x y)->((greater y z)->(greater x z))))))); [ zenon_intro zenon_H30 | zenon_intro zenon_H64 ]. % 0.45/0.73 apply (zenon_notallex_s (fun X : zenon_U => (forall T0 : zenon_U, (forall T : zenon_U, (((organization X)/\((has_immunity X T0)/\(~(has_immunity X T))))->(greater (hazard_of_mortality X T) (hazard_of_mortality X T0)))))) zenon_G); [ zenon_intro zenon_H65; idtac ]. % 0.45/0.73 elim zenon_H65. zenon_intro zenon_TX_s. zenon_intro zenon_H66. % 0.45/0.73 apply (zenon_notallex_s (fun T0 : zenon_U => (forall T : zenon_U, (((organization zenon_TX_s)/\((has_immunity zenon_TX_s T0)/\(~(has_immunity zenon_TX_s T))))->(greater (hazard_of_mortality zenon_TX_s T) (hazard_of_mortality zenon_TX_s T0))))) zenon_H66); [ zenon_intro zenon_H67; idtac ]. % 0.45/0.73 elim zenon_H67. zenon_intro zenon_TT0_ea. zenon_intro zenon_H69. % 0.45/0.73 apply (zenon_notallex_s (fun T : zenon_U => (((organization zenon_TX_s)/\((has_immunity zenon_TX_s zenon_TT0_ea)/\(~(has_immunity zenon_TX_s T))))->(greater (hazard_of_mortality zenon_TX_s T) (hazard_of_mortality zenon_TX_s zenon_TT0_ea)))) zenon_H69); [ zenon_intro zenon_H6a; idtac ]. % 0.45/0.73 elim zenon_H6a. zenon_intro zenon_TT_r. zenon_intro zenon_H6b. % 0.45/0.73 apply (zenon_notimply_s _ _ zenon_H6b). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H18. zenon_intro zenon_H6e. % 0.45/0.73 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H6f. zenon_intro zenon_H19. % 0.45/0.73 generalize (assumption_17 zenon_TX_s). zenon_intro zenon_H17. % 0.45/0.73 generalize (zenon_H17 zenon_TT0_ea). zenon_intro zenon_H70. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H1f | zenon_intro zenon_H71 ]. % 0.45/0.73 exact (zenon_H1f zenon_H18). % 0.45/0.73 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H73. zenon_intro zenon_H72. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H73); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 0.45/0.73 exact (zenon_H75 zenon_H6f). % 0.45/0.73 elim (classic ((very_low) = (hazard_of_mortality zenon_TX_s zenon_TT0_ea))); [ zenon_intro zenon_H76 | zenon_intro zenon_H77 ]. % 0.45/0.73 elim (classic (greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (very_low))); [ zenon_intro zenon_H62 | zenon_intro zenon_H59 ]. % 0.45/0.73 cut ((greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (very_low)) = (greater (hazard_of_mortality zenon_TX_s zenon_TT_r) (hazard_of_mortality zenon_TX_s zenon_TT0_ea))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H6c. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact zenon_H62. % 0.45/0.73 cut (((very_low) = (hazard_of_mortality zenon_TX_s zenon_TT0_ea))); [idtac | apply NNPP; zenon_intro zenon_H77]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT_r) = (hazard_of_mortality zenon_TX_s zenon_TT_r))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.45/0.73 congruence. % 0.45/0.73 apply zenon_H39. apply refl_equal. % 0.45/0.73 exact (zenon_H77 zenon_H76). % 0.45/0.73 apply (zenon_L11_ zenon_TT_r zenon_TX_s); trivial. % 0.45/0.73 elim (classic ((hazard_of_mortality zenon_TX_s zenon_TT0_ea) = (hazard_of_mortality zenon_TX_s zenon_TT0_ea))); [ zenon_intro zenon_H78 | zenon_intro zenon_H79 ]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT0_ea) = (hazard_of_mortality zenon_TX_s zenon_TT0_ea)) = ((very_low) = (hazard_of_mortality zenon_TX_s zenon_TT0_ea))). % 0.45/0.73 intro zenon_D_pnotp. % 0.45/0.73 apply zenon_H77. % 0.45/0.73 rewrite <- zenon_D_pnotp. % 0.45/0.73 exact zenon_H78. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT0_ea) = (hazard_of_mortality zenon_TX_s zenon_TT0_ea))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 0.45/0.73 cut (((hazard_of_mortality zenon_TX_s zenon_TT0_ea) = (very_low))); [idtac | apply NNPP; zenon_intro zenon_H7a]. % 0.45/0.73 congruence. % 0.45/0.73 exact (zenon_H7a zenon_H74). % 0.45/0.73 apply zenon_H79. apply refl_equal. % 0.45/0.73 apply zenon_H79. apply refl_equal. % 0.45/0.73 apply zenon_H64. zenon_intro zenon_Tx_et. apply NNPP. zenon_intro zenon_H7c. % 0.45/0.73 apply zenon_H7c. zenon_intro zenon_Ty_ev. apply NNPP. zenon_intro zenon_H7e. % 0.45/0.73 apply zenon_H7e. zenon_intro zenon_Tz_ex. apply NNPP. zenon_intro zenon_H80. % 0.45/0.73 apply (zenon_notimply_s _ _ zenon_H80). zenon_intro zenon_H82. zenon_intro zenon_H81. % 0.45/0.73 apply (zenon_notimply_s _ _ zenon_H81). zenon_intro zenon_H84. zenon_intro zenon_H83. % 0.45/0.73 generalize (meaning_postulate_greater_transitive zenon_Tx_et). zenon_intro zenon_H85. % 0.45/0.73 generalize (zenon_H85 zenon_Ty_ev). zenon_intro zenon_H86. % 0.45/0.73 generalize (zenon_H86 zenon_Tz_ex). zenon_intro zenon_H87. % 0.45/0.73 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.45/0.73 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H8b | zenon_intro zenon_H8a ]. % 0.45/0.73 exact (zenon_H8b zenon_H82). % 0.45/0.73 exact (zenon_H8a zenon_H84). % 0.45/0.73 exact (zenon_H83 zenon_H88). % 0.45/0.73 Qed. % 0.45/0.73 % SZS output end Proof % 0.45/0.73 (* END-PROOF *) % 0.45/0.73 nodes searched: 6304 % 0.45/0.73 max branch formulas: 213 % 0.45/0.73 proof nodes created: 609 % 0.45/0.73 formulas created: 4412 % 0.45/0.73 %------------------------------------------------------------------------------