%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT046+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:22 AM UTC 2026 % Result : Theorem 13.54s 13.83s % Output : Proof 13.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT046+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.10/0.36 % Computer : n006.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 13:10:01 UTC 2026 % 0.10/0.36 % CPUTime : % 13.54/13.83 (* PROOF-FOUND *) % 13.54/13.83 % SZS status Theorem % 13.54/13.83 (* BEGIN-PROOF *) % 13.54/13.83 % SZS output start Proof % 13.54/13.83 Theorem theorem_1 : (forall X : zenon_U, (forall T0 : zenon_U, (forall T : zenon_U, (((organization X)/\((~(has_endowment X))/\(greater (age X T) (age X T0))))->(smaller (hazard_of_mortality X T) (hazard_of_mortality X T0)))))). % 13.54/13.83 Proof. % 13.54/13.83 assert (zenon_L1_ : forall (zenon_TT_u : zenon_U) (zenon_TT0_v : zenon_U) (zenon_TX_w : zenon_U), (forall T : zenon_U, (((organization zenon_TX_w)/\(greater (age zenon_TX_w T) (age zenon_TX_w zenon_TT0_v)))->(greater (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w zenon_TT0_v)))) -> (organization zenon_TX_w) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (~(greater (stock_of_knowledge zenon_TX_w zenon_TT_u) (stock_of_knowledge zenon_TX_w zenon_TT0_v))) -> False). % 13.54/13.83 do 3 intro. intros zenon_H10 zenon_H11 zenon_H12 zenon_H13. % 13.54/13.83 generalize (zenon_H10 zenon_TT_u). zenon_intro zenon_H17. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H17); [ zenon_intro zenon_H19 | zenon_intro zenon_H18 ]. % 13.54/13.83 apply (zenon_notand_s _ _ zenon_H19); [ zenon_intro zenon_H1b | zenon_intro zenon_H1a ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 exact (zenon_H1a zenon_H12). % 13.54/13.83 exact (zenon_H13 zenon_H18). % 13.54/13.83 (* end of lemma zenon_L1_ *) % 13.54/13.83 assert (zenon_L2_ : forall (zenon_TT0_v : zenon_U) (zenon_TT_u : zenon_U) (zenon_TX_w : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_w)/\(greater (age zenon_TX_w T) (age zenon_TX_w T0)))->(greater (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w T0))))) -> (~(greater (stock_of_knowledge zenon_TX_w zenon_TT_u) (stock_of_knowledge zenon_TX_w zenon_TT0_v))) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (organization zenon_TX_w) -> False). % 13.54/13.83 do 3 intro. intros zenon_H1c zenon_H13 zenon_H12 zenon_H11. % 13.54/13.83 generalize (zenon_H1c zenon_TT0_v). zenon_intro zenon_H10. % 13.54/13.83 apply (zenon_L1_ zenon_TT_u zenon_TT0_v zenon_TX_w); trivial. % 13.54/13.83 (* end of lemma zenon_L2_ *) % 13.54/13.83 assert (zenon_L3_ : forall (zenon_TT0_v : zenon_U) (zenon_TT_u : zenon_U) (zenon_TX_w : zenon_U), (~(greater (internal_friction zenon_TX_w zenon_TT_u) (internal_friction zenon_TX_w zenon_TT0_v))) -> (~((internal_friction zenon_TX_w zenon_TT_u) = (internal_friction zenon_TX_w zenon_TT0_v))) -> (~(greater (internal_friction zenon_TX_w zenon_TT0_v) (internal_friction zenon_TX_w zenon_TT_u))) -> False). % 13.54/13.83 do 3 intro. intros zenon_H1d zenon_H1e zenon_H1f. % 13.54/13.83 generalize (meaning_postulate_greater_comparable (internal_friction zenon_TX_w zenon_TT_u)). zenon_intro zenon_H20. % 13.54/13.83 generalize (zenon_H20 (internal_friction zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H21. % 13.54/13.83 apply (zenon_or_s _ _ zenon_H21); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 13.54/13.83 generalize (definition_smaller (internal_friction zenon_TX_w zenon_TT_u)). zenon_intro zenon_H24. % 13.54/13.83 generalize (zenon_H24 (internal_friction zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H25. % 13.54/13.83 apply (zenon_equiv_s _ _ zenon_H25); [ zenon_intro zenon_H27; zenon_intro zenon_H1f | zenon_intro zenon_H23; zenon_intro zenon_H26 ]. % 13.54/13.83 exact (zenon_H27 zenon_H23). % 13.54/13.83 exact (zenon_H1f zenon_H26). % 13.54/13.83 apply (zenon_or_s _ _ zenon_H22); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 13.54/13.83 exact (zenon_H1e zenon_H29). % 13.54/13.83 exact (zenon_H1d zenon_H28). % 13.54/13.83 (* end of lemma zenon_L3_ *) % 13.54/13.83 assert (zenon_L4_ : forall (zenon_TT_u : zenon_U) (zenon_TT0_v : zenon_U) (zenon_TX_w : zenon_U), (forall T : zenon_U, ((organization zenon_TX_w)->((((greater (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w zenon_TT0_v))/\(smaller_or_equal (internal_friction zenon_TX_w T) (internal_friction zenon_TX_w zenon_TT0_v)))->(greater (capability zenon_TX_w T) (capability zenon_TX_w zenon_TT0_v)))/\((((smaller_or_equal (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w zenon_TT0_v))/\(greater (internal_friction zenon_TX_w T) (internal_friction zenon_TX_w zenon_TT0_v)))->(smaller (capability zenon_TX_w T) (capability zenon_TX_w zenon_TT0_v)))/\((((stock_of_knowledge zenon_TX_w T) = (stock_of_knowledge zenon_TX_w zenon_TT0_v))/\((internal_friction zenon_TX_w T) = (internal_friction zenon_TX_w zenon_TT0_v)))->((capability zenon_TX_w T) = (capability zenon_TX_w zenon_TT0_v))))))) -> (organization zenon_TX_w) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_w)/\(greater (age zenon_TX_w T) (age zenon_TX_w T0)))->(greater (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w T0))))) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (~(greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v))) -> (forall T : zenon_U, ((organization zenon_TX_w)->((internal_friction zenon_TX_w T) = (internal_friction zenon_TX_w zenon_E)))) -> (~(greater (capability zenon_TX_w zenon_TT_u) (capability zenon_TX_w zenon_TT0_v))) -> False). % 13.54/13.83 do 3 intro. intros zenon_H2a zenon_H11 zenon_H1c zenon_H12 zenon_H2b zenon_H2c zenon_H2d. % 13.54/13.83 generalize (zenon_H2a zenon_TT_u). zenon_intro zenon_H2e. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H1b | zenon_intro zenon_H2f ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H31. zenon_intro zenon_H30. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H31); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 13.54/13.83 apply (zenon_notand_s _ _ zenon_H33); [ zenon_intro zenon_H13 | zenon_intro zenon_H34 ]. % 13.54/13.83 apply (zenon_L2_ zenon_TT0_v zenon_TT_u zenon_TX_w); trivial. % 13.54/13.83 generalize (definition_smaller_or_equal (internal_friction zenon_TX_w zenon_TT_u)). zenon_intro zenon_H35. % 13.54/13.83 generalize (zenon_H35 (internal_friction zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H36. % 13.54/13.83 apply (zenon_equiv_s _ _ zenon_H36); [ zenon_intro zenon_H34; zenon_intro zenon_H39 | zenon_intro zenon_H38; zenon_intro zenon_H37 ]. % 13.54/13.83 apply (zenon_notor_s _ _ zenon_H39). zenon_intro zenon_H27. zenon_intro zenon_H1e. % 13.54/13.83 generalize (definition_smaller (internal_friction zenon_TX_w zenon_TT_u)). zenon_intro zenon_H24. % 13.54/13.83 generalize (zenon_H24 (internal_friction zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H25. % 13.54/13.83 apply (zenon_equiv_s _ _ zenon_H25); [ zenon_intro zenon_H27; zenon_intro zenon_H1f | zenon_intro zenon_H23; zenon_intro zenon_H26 ]. % 13.54/13.83 generalize (zenon_H2c zenon_TT_u). zenon_intro zenon_H3a. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H3a); [ zenon_intro zenon_H1b | zenon_intro zenon_H3b ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 elim (classic ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_TT_u))); [ zenon_intro zenon_H3c | zenon_intro zenon_H3d ]. % 13.54/13.83 elim (classic (greater (internal_friction zenon_TX_w zenon_TT_u) (internal_friction zenon_TX_w zenon_TT0_v))); [ zenon_intro zenon_H28 | zenon_intro zenon_H1d ]. % 13.54/13.83 cut ((greater (internal_friction zenon_TX_w zenon_TT_u) (internal_friction zenon_TX_w zenon_TT0_v)) = (greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H2b. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H28. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_TT0_v))); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT_u) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 13.54/13.83 congruence. % 13.54/13.83 elim (classic ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [ zenon_intro zenon_H40 | zenon_intro zenon_H41 ]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E)) = ((internal_friction zenon_TX_w zenon_TT_u) = (internal_friction zenon_TX_w zenon_E))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H3f. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H40. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_TT_u))); [idtac | apply NNPP; zenon_intro zenon_H3d]. % 13.54/13.83 congruence. % 13.54/13.83 exact (zenon_H3d zenon_H3c). % 13.54/13.83 apply zenon_H41. apply refl_equal. % 13.54/13.83 apply zenon_H41. apply refl_equal. % 13.54/13.83 apply zenon_H3e. apply refl_equal. % 13.54/13.83 apply (zenon_L3_ zenon_TT0_v zenon_TT_u zenon_TX_w); trivial. % 13.54/13.83 elim (classic ((internal_friction zenon_TX_w zenon_TT_u) = (internal_friction zenon_TX_w zenon_TT_u))); [ zenon_intro zenon_H42 | zenon_intro zenon_H43 ]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT_u) = (internal_friction zenon_TX_w zenon_TT_u)) = ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_TT_u))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H3d. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H42. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT_u) = (internal_friction zenon_TX_w zenon_TT_u))); [idtac | apply NNPP; zenon_intro zenon_H43]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT_u) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 13.54/13.83 congruence. % 13.54/13.83 exact (zenon_H3f zenon_H3b). % 13.54/13.83 apply zenon_H43. apply refl_equal. % 13.54/13.83 apply zenon_H43. apply refl_equal. % 13.54/13.83 exact (zenon_H27 zenon_H23). % 13.54/13.83 exact (zenon_H34 zenon_H38). % 13.54/13.83 exact (zenon_H2d zenon_H32). % 13.54/13.83 (* end of lemma zenon_L4_ *) % 13.54/13.83 assert (zenon_L5_ : forall (zenon_TT_u : zenon_U) (zenon_TT0_v : zenon_U) (zenon_TX_w : zenon_U), ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E)) -> (~(greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v))) -> (forall T : zenon_U, ((organization zenon_TX_w)->((((greater (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w zenon_TT0_v))/\(smaller_or_equal (internal_friction zenon_TX_w T) (internal_friction zenon_TX_w zenon_TT0_v)))->(greater (capability zenon_TX_w T) (capability zenon_TX_w zenon_TT0_v)))/\((((smaller_or_equal (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w zenon_TT0_v))/\(greater (internal_friction zenon_TX_w T) (internal_friction zenon_TX_w zenon_TT0_v)))->(smaller (capability zenon_TX_w T) (capability zenon_TX_w zenon_TT0_v)))/\((((stock_of_knowledge zenon_TX_w T) = (stock_of_knowledge zenon_TX_w zenon_TT0_v))/\((internal_friction zenon_TX_w T) = (internal_friction zenon_TX_w zenon_TT0_v)))->((capability zenon_TX_w T) = (capability zenon_TX_w zenon_TT0_v))))))) -> (organization zenon_TX_w) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_w)/\(greater (age zenon_TX_w T) (age zenon_TX_w T0)))->(greater (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w T0))))) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (forall T : zenon_U, ((organization zenon_TX_w)->((internal_friction zenon_TX_w T) = (internal_friction zenon_TX_w zenon_E)))) -> (~(greater (capability zenon_TX_w zenon_TT_u) (capability zenon_TX_w zenon_TT0_v))) -> False). % 13.54/13.83 do 3 intro. intros zenon_H44 zenon_H45 zenon_H2a zenon_H11 zenon_H1c zenon_H12 zenon_H2c zenon_H2d. % 13.54/13.83 elim (classic (greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v))); [ zenon_intro zenon_H46 | zenon_intro zenon_H2b ]. % 13.54/13.83 cut ((greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v)) = (greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H45. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H46. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_TT0_v))); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H47]. % 13.54/13.83 congruence. % 13.54/13.83 elim (classic ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [ zenon_intro zenon_H48 | zenon_intro zenon_H49 ]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E)) = ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H47. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H48. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H49]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 13.54/13.83 congruence. % 13.54/13.83 exact (zenon_H4a zenon_H44). % 13.54/13.83 apply zenon_H49. apply refl_equal. % 13.54/13.83 apply zenon_H49. apply refl_equal. % 13.54/13.83 apply zenon_H3e. apply refl_equal. % 13.54/13.83 apply (zenon_L4_ zenon_TT_u zenon_TT0_v zenon_TX_w); trivial. % 13.54/13.83 (* end of lemma zenon_L5_ *) % 13.54/13.83 assert (zenon_L6_ : forall (zenon_TT0_v : zenon_U) (zenon_TX_w : zenon_U), (forall T : zenon_U, ((organization zenon_TX_w)->((internal_friction zenon_TX_w T) = (internal_friction zenon_TX_w zenon_E)))) -> (organization zenon_TX_w) -> (~((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_E))) -> False). % 13.54/13.83 do 2 intro. intros zenon_H2c zenon_H11 zenon_H4b. % 13.54/13.83 generalize (zenon_H2c zenon_TT0_v). zenon_intro zenon_H4c. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H4c); [ zenon_intro zenon_H1b | zenon_intro zenon_H4d ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 exact (zenon_H4b zenon_H4d). % 13.54/13.83 (* end of lemma zenon_L6_ *) % 13.54/13.83 assert (zenon_L7_ : forall (zenon_TT0_v : zenon_U) (zenon_TX_w : zenon_U), (greater (capability zenon_TX_w zenon_TT0_v) (capability zenon_TX_w zenon_TT0_v)) -> False). % 13.54/13.83 do 2 intro. intros zenon_H4e. % 13.54/13.83 generalize (meaning_postulate_greater_strict (capability zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H4f. % 13.54/13.83 generalize (zenon_H4f (capability zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H50. % 13.54/13.83 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H51 | zenon_intro zenon_H51 ]. % 13.54/13.83 exact (zenon_H51 zenon_H4e). % 13.54/13.83 exact (zenon_H51 zenon_H4e). % 13.54/13.83 (* end of lemma zenon_L7_ *) % 13.54/13.83 assert (zenon_L8_ : forall (zenon_TT0_v : zenon_U) (zenon_TX_w : zenon_U), (smaller (capability zenon_TX_w zenon_TT0_v) (capability zenon_TX_w zenon_TT0_v)) -> False). % 13.54/13.83 do 2 intro. intros zenon_H52. % 13.54/13.83 generalize (definition_smaller (capability zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H53. % 13.54/13.83 generalize (zenon_H53 (capability zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H54. % 13.54/13.83 apply (zenon_equiv_s _ _ zenon_H54); [ zenon_intro zenon_H55; zenon_intro zenon_H51 | zenon_intro zenon_H52; zenon_intro zenon_H4e ]. % 13.54/13.83 exact (zenon_H55 zenon_H52). % 13.54/13.83 apply (zenon_L7_ zenon_TT0_v zenon_TX_w); trivial. % 13.54/13.83 (* end of lemma zenon_L8_ *) % 13.54/13.83 assert (zenon_L9_ : forall (zenon_TT0_v : zenon_U) (zenon_TT_u : zenon_U) (zenon_TX_w : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, ((organization zenon_TX_w)->((((greater (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w T0))/\(smaller_or_equal (internal_friction zenon_TX_w T) (internal_friction zenon_TX_w T0)))->(greater (capability zenon_TX_w T) (capability zenon_TX_w T0)))/\((((smaller_or_equal (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w T0))/\(greater (internal_friction zenon_TX_w T) (internal_friction zenon_TX_w T0)))->(smaller (capability zenon_TX_w T) (capability zenon_TX_w T0)))/\((((stock_of_knowledge zenon_TX_w T) = (stock_of_knowledge zenon_TX_w T0))/\((internal_friction zenon_TX_w T) = (internal_friction zenon_TX_w T0)))->((capability zenon_TX_w T) = (capability zenon_TX_w T0)))))))) -> (forall T : zenon_U, ((organization zenon_TX_w)->((internal_friction zenon_TX_w T) = (internal_friction zenon_TX_w zenon_E)))) -> ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E)) -> (~(greater (capability zenon_TX_w zenon_TT_u) (capability zenon_TX_w zenon_TT0_v))) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (forall T0 : zenon_U, (forall T : zenon_U, (((organization zenon_TX_w)/\(greater (age zenon_TX_w T) (age zenon_TX_w T0)))->(greater (stock_of_knowledge zenon_TX_w T) (stock_of_knowledge zenon_TX_w T0))))) -> (organization zenon_TX_w) -> False). % 13.54/13.83 do 3 intro. intros zenon_H56 zenon_H2c zenon_H44 zenon_H2d zenon_H12 zenon_H1c zenon_H11. % 13.54/13.83 generalize (zenon_H56 zenon_TT0_v). zenon_intro zenon_H2a. % 13.54/13.83 generalize (zenon_H2a zenon_TT0_v). zenon_intro zenon_H57. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H57); [ zenon_intro zenon_H1b | zenon_intro zenon_H58 ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 13.54/13.83 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H5c); [ zenon_intro zenon_H5d | zenon_intro zenon_H52 ]. % 13.54/13.83 apply (zenon_notand_s _ _ zenon_H5d); [ zenon_intro zenon_H5f | zenon_intro zenon_H5e ]. % 13.54/13.83 generalize (definition_smaller_or_equal (stock_of_knowledge zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H60. % 13.54/13.83 generalize (zenon_H60 (stock_of_knowledge zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H61. % 13.54/13.83 apply (zenon_equiv_s _ _ zenon_H61); [ zenon_intro zenon_H5f; zenon_intro zenon_H64 | zenon_intro zenon_H63; zenon_intro zenon_H62 ]. % 13.54/13.83 apply (zenon_notor_s _ _ zenon_H64). zenon_intro zenon_H66. zenon_intro zenon_H65. % 13.54/13.83 apply zenon_H65. apply refl_equal. % 13.54/13.83 exact (zenon_H5f zenon_H63). % 13.54/13.83 elim (classic ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [ zenon_intro zenon_H67 | zenon_intro zenon_H47 ]. % 13.54/13.83 elim (classic (greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v))); [ zenon_intro zenon_H68 | zenon_intro zenon_H45 ]. % 13.54/13.83 elim (classic (greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v))); [ zenon_intro zenon_H46 | zenon_intro zenon_H2b ]. % 13.54/13.83 cut ((greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v)) = (greater (internal_friction zenon_TX_w zenon_TT0_v) (internal_friction zenon_TX_w zenon_TT0_v))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H5e. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H46. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_TT0_v))); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_TT0_v))); [idtac | apply NNPP; zenon_intro zenon_H69]. % 13.54/13.83 congruence. % 13.54/13.83 elim (classic ((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_TT0_v))); [ zenon_intro zenon_H6a | zenon_intro zenon_H3e ]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_TT0_v)) = ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_TT0_v))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H69. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H6a. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_TT0_v))); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 13.54/13.83 congruence. % 13.54/13.83 apply (zenon_L6_ zenon_TT0_v zenon_TX_w); trivial. % 13.54/13.83 apply zenon_H3e. apply refl_equal. % 13.54/13.83 apply zenon_H3e. apply refl_equal. % 13.54/13.83 apply zenon_H3e. apply refl_equal. % 13.54/13.83 cut ((greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v)) = (greater (internal_friction zenon_TX_w zenon_E) (internal_friction zenon_TX_w zenon_TT0_v))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H2b. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H68. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_TT0_v) = (internal_friction zenon_TX_w zenon_TT0_v))); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 13.54/13.83 congruence. % 13.54/13.83 elim (classic ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [ zenon_intro zenon_H40 | zenon_intro zenon_H41 ]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E)) = ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H4a. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H40. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H47]. % 13.54/13.83 congruence. % 13.54/13.83 exact (zenon_H47 zenon_H67). % 13.54/13.83 apply zenon_H41. apply refl_equal. % 13.54/13.83 apply zenon_H41. apply refl_equal. % 13.54/13.83 apply zenon_H3e. apply refl_equal. % 13.54/13.83 apply (zenon_L5_ zenon_TT_u zenon_TT0_v zenon_TX_w); trivial. % 13.54/13.83 elim (classic ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [ zenon_intro zenon_H48 | zenon_intro zenon_H49 ]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E)) = ((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))). % 13.54/13.83 intro zenon_D_pnotp. % 13.54/13.83 apply zenon_H47. % 13.54/13.83 rewrite <- zenon_D_pnotp. % 13.54/13.83 exact zenon_H48. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H49]. % 13.54/13.83 cut (((internal_friction zenon_TX_w zenon_E) = (internal_friction zenon_TX_w zenon_E))); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 13.54/13.83 congruence. % 13.54/13.83 exact (zenon_H4a zenon_H44). % 13.54/13.83 apply zenon_H49. apply refl_equal. % 13.54/13.83 apply zenon_H49. apply refl_equal. % 13.54/13.83 apply (zenon_L8_ zenon_TT0_v zenon_TX_w); trivial. % 13.54/13.83 (* end of lemma zenon_L9_ *) % 13.54/13.83 assert (zenon_L10_ : forall (zenon_TT_u : zenon_U) (zenon_TT0_v : zenon_U) (zenon_TX_w : zenon_U), (forall T : zenon_U, ((organization zenon_TX_w)->(((greater (external_ties zenon_TX_w T) (external_ties zenon_TX_w zenon_TT0_v))->(greater (position zenon_TX_w T) (position zenon_TX_w zenon_TT0_v)))/\(((external_ties zenon_TX_w T) = (external_ties zenon_TX_w zenon_TT0_v))->((position zenon_TX_w T) = (position zenon_TX_w zenon_TT0_v)))))) -> (organization zenon_TX_w) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (~(greater (position zenon_TX_w zenon_TT_u) (position zenon_TX_w zenon_TT0_v))) -> False). % 13.54/13.83 do 3 intro. intros zenon_H6b zenon_H11 zenon_H12 zenon_H6c. % 13.54/13.83 generalize (zenon_H6b zenon_TT_u). zenon_intro zenon_H6d. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H1b | zenon_intro zenon_H6e ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H72 | zenon_intro zenon_H71 ]. % 13.54/13.83 generalize (assumption_8 zenon_TX_w). zenon_intro zenon_H73. % 13.54/13.83 generalize (zenon_H73 zenon_TT0_v). zenon_intro zenon_H74. % 13.54/13.83 generalize (zenon_H74 zenon_TT_u). zenon_intro zenon_H75. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H75); [ zenon_intro zenon_H19 | zenon_intro zenon_H76 ]. % 13.54/13.83 apply (zenon_notand_s _ _ zenon_H19); [ zenon_intro zenon_H1b | zenon_intro zenon_H1a ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 exact (zenon_H1a zenon_H12). % 13.54/13.83 exact (zenon_H72 zenon_H76). % 13.54/13.83 exact (zenon_H6c zenon_H71). % 13.54/13.83 (* end of lemma zenon_L10_ *) % 13.54/13.83 assert (zenon_L11_ : forall (zenon_TT0_v : zenon_U) (zenon_TT_u : zenon_U) (zenon_TX_w : zenon_U), (forall T0 : zenon_U, (forall T : zenon_U, ((organization zenon_TX_w)->(((greater (external_ties zenon_TX_w T) (external_ties zenon_TX_w T0))->(greater (position zenon_TX_w T) (position zenon_TX_w T0)))/\(((external_ties zenon_TX_w T) = (external_ties zenon_TX_w T0))->((position zenon_TX_w T) = (position zenon_TX_w T0))))))) -> (~(greater (position zenon_TX_w zenon_TT_u) (position zenon_TX_w zenon_TT0_v))) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (organization zenon_TX_w) -> False). % 13.54/13.83 do 3 intro. intros zenon_H77 zenon_H6c zenon_H12 zenon_H11. % 13.54/13.83 generalize (zenon_H77 zenon_TT0_v). zenon_intro zenon_H6b. % 13.54/13.83 apply (zenon_L10_ zenon_TT_u zenon_TT0_v zenon_TX_w); trivial. % 13.54/13.83 (* end of lemma zenon_L11_ *) % 13.54/13.83 assert (zenon_L12_ : forall (zenon_TT0_v : zenon_U) (zenon_TT_u : zenon_U) (zenon_TX_w : zenon_U), (organization zenon_TX_w) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (~(greater (position zenon_TX_w zenon_TT_u) (position zenon_TX_w zenon_TT0_v))) -> False). % 13.54/13.83 do 3 intro. intros zenon_H11 zenon_H12 zenon_H6c. % 13.54/13.83 generalize (assumption_6 zenon_TX_w). zenon_intro zenon_H77. % 13.54/13.83 apply (zenon_L11_ zenon_TT0_v zenon_TT_u zenon_TX_w); trivial. % 13.54/13.83 (* end of lemma zenon_L12_ *) % 13.54/13.83 assert (zenon_L13_ : forall (zenon_TT0_v : zenon_U) (zenon_TT_u : zenon_U) (zenon_TX_w : zenon_U), (organization zenon_TX_w) -> (greater (age zenon_TX_w zenon_TT_u) (age zenon_TX_w zenon_TT0_v)) -> (~(greater_or_equal (position zenon_TX_w zenon_TT_u) (position zenon_TX_w zenon_TT0_v))) -> False). % 13.54/13.83 do 3 intro. intros zenon_H11 zenon_H12 zenon_H78. % 13.54/13.83 generalize (definition_greater_or_equal (position zenon_TX_w zenon_TT_u)). zenon_intro zenon_H79. % 13.54/13.83 generalize (zenon_H79 (position zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H7a. % 13.54/13.83 apply (zenon_equiv_s _ _ zenon_H7a); [ zenon_intro zenon_H78; zenon_intro zenon_H7d | zenon_intro zenon_H7c; zenon_intro zenon_H7b ]. % 13.54/13.83 apply (zenon_notor_s _ _ zenon_H7d). zenon_intro zenon_H6c. zenon_intro zenon_H7e. % 13.54/13.83 apply (zenon_L12_ zenon_TT0_v zenon_TT_u zenon_TX_w); trivial. % 13.54/13.83 exact (zenon_H78 zenon_H7c). % 13.54/13.83 (* end of lemma zenon_L13_ *) % 13.54/13.83 assert (zenon_L14_ : forall (zenon_TT0_v : zenon_U) (zenon_TT_u : zenon_U) (zenon_TX_w : zenon_U), (smaller (hazard_of_mortality zenon_TX_w zenon_TT_u) (hazard_of_mortality zenon_TX_w zenon_TT0_v)) -> (~(greater (hazard_of_mortality zenon_TX_w zenon_TT0_v) (hazard_of_mortality zenon_TX_w zenon_TT_u))) -> False). % 13.54/13.83 do 3 intro. intros zenon_H7f zenon_H80. % 13.54/13.83 generalize (definition_smaller (hazard_of_mortality zenon_TX_w zenon_TT_u)). zenon_intro zenon_H81. % 13.54/13.83 generalize (zenon_H81 (hazard_of_mortality zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H82. % 13.54/13.83 apply (zenon_equiv_s _ _ zenon_H82); [ zenon_intro zenon_H84; zenon_intro zenon_H80 | zenon_intro zenon_H7f; zenon_intro zenon_H83 ]. % 13.54/13.83 exact (zenon_H84 zenon_H7f). % 13.54/13.83 exact (zenon_H80 zenon_H83). % 13.54/13.83 (* end of lemma zenon_L14_ *) % 13.54/13.83 apply NNPP. intro zenon_G. % 13.54/13.83 apply (zenon_notallex_s (fun X : zenon_U => (forall T0 : zenon_U, (forall T : zenon_U, (((organization X)/\((~(has_endowment X))/\(greater (age X T) (age X T0))))->(smaller (hazard_of_mortality X T) (hazard_of_mortality X T0)))))) zenon_G); [ zenon_intro zenon_H85; idtac ]. % 13.54/13.83 elim zenon_H85. zenon_intro zenon_TX_w. zenon_intro zenon_H86. % 13.54/13.83 apply (zenon_notallex_s (fun T0 : zenon_U => (forall T : zenon_U, (((organization zenon_TX_w)/\((~(has_endowment zenon_TX_w))/\(greater (age zenon_TX_w T) (age zenon_TX_w T0))))->(smaller (hazard_of_mortality zenon_TX_w T) (hazard_of_mortality zenon_TX_w T0))))) zenon_H86); [ zenon_intro zenon_H87; idtac ]. % 13.54/13.83 elim zenon_H87. zenon_intro zenon_TT0_v. zenon_intro zenon_H88. % 13.54/13.83 apply (zenon_notallex_s (fun T : zenon_U => (((organization zenon_TX_w)/\((~(has_endowment zenon_TX_w))/\(greater (age zenon_TX_w T) (age zenon_TX_w zenon_TT0_v))))->(smaller (hazard_of_mortality zenon_TX_w T) (hazard_of_mortality zenon_TX_w zenon_TT0_v)))) zenon_H88); [ zenon_intro zenon_H89; idtac ]. % 13.54/13.83 elim zenon_H89. zenon_intro zenon_TT_u. zenon_intro zenon_H8a. % 13.54/13.83 apply (zenon_notimply_s _ _ zenon_H8a). zenon_intro zenon_H8b. zenon_intro zenon_H84. % 13.54/13.83 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H11. zenon_intro zenon_H8c. % 13.54/13.83 apply (zenon_and_s _ _ zenon_H8c). zenon_intro zenon_H8d. zenon_intro zenon_H12. % 13.54/13.83 generalize (definition_smaller (hazard_of_mortality zenon_TX_w zenon_TT_u)). zenon_intro zenon_H81. % 13.54/13.83 generalize (zenon_H81 (hazard_of_mortality zenon_TX_w zenon_TT0_v)). zenon_intro zenon_H82. % 13.54/13.83 apply (zenon_equiv_s _ _ zenon_H82); [ zenon_intro zenon_H84; zenon_intro zenon_H80 | zenon_intro zenon_H7f; zenon_intro zenon_H83 ]. % 13.54/13.83 generalize (assumption_4 zenon_TX_w). zenon_intro zenon_H8e. % 13.54/13.83 generalize (assumption_5 zenon_TX_w). zenon_intro zenon_H56. % 13.54/13.83 generalize (assumption_9 zenon_TX_w). zenon_intro zenon_H1. % 13.54/13.83 generalize (zenon_H1 zenon_E). zenon_intro zenon_H2c. % 13.54/13.83 generalize (zenon_H2c zenon_E). zenon_intro zenon_H8f. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H8f); [ zenon_intro zenon_H1b | zenon_intro zenon_H44 ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 generalize (assumption_7 zenon_TX_w). zenon_intro zenon_H1c. % 13.54/13.83 generalize (zenon_H8e zenon_TT0_v). zenon_intro zenon_H90. % 13.54/13.83 generalize (zenon_H90 zenon_TT_u). zenon_intro zenon_H91. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H91); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 13.54/13.83 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H1b | zenon_intro zenon_H94 ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 apply (zenon_notand_s _ _ zenon_H94); [ zenon_intro zenon_H96 | zenon_intro zenon_H95 ]. % 13.54/13.83 apply zenon_H96. zenon_intro zenon_H97. % 13.54/13.83 generalize (assumption_1 zenon_TX_w). zenon_intro zenon_H98. % 13.54/13.83 generalize (zenon_H98 zenon_TT0_v). zenon_intro zenon_H99. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H99); [ zenon_intro zenon_H9b | zenon_intro zenon_H9a ]. % 13.54/13.83 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H1b | zenon_intro zenon_H9c ]. % 13.54/13.83 exact (zenon_H1b zenon_H11). % 13.54/13.83 exact (zenon_H9c zenon_H8d). % 13.54/13.83 exact (zenon_H9a zenon_H97). % 13.54/13.83 apply zenon_H95. zenon_intro zenon_H9d. % 13.54/13.83 generalize (assumption_1 zenon_TX_w). zenon_intro zenon_H98. % 13.54/13.83 generalize (zenon_H98 zenon_TT_u). zenon_intro zenon_H9e. % 13.54/13.83 apply (zenon_imply_s _ _ zenon_H9e); [ zenon_intro zenon_H9b | zenon_intro zenon_H9f ]. % 13.54/13.85 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H1b | zenon_intro zenon_H9c ]. % 13.54/13.85 exact (zenon_H1b zenon_H11). % 13.54/13.85 exact (zenon_H9c zenon_H8d). % 13.54/13.85 exact (zenon_H9f zenon_H9d). % 13.54/13.85 apply (zenon_and_s _ _ zenon_H92). zenon_intro zenon_Ha1. zenon_intro zenon_Ha0. % 13.54/13.85 apply (zenon_imply_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha2 | zenon_intro zenon_H7f ]. % 13.54/13.85 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_H2d | zenon_intro zenon_H78 ]. % 13.54/13.85 apply (zenon_L9_ zenon_TT0_v zenon_TT_u zenon_TX_w); trivial. % 13.54/13.85 apply (zenon_L13_ zenon_TT0_v zenon_TT_u zenon_TX_w); trivial. % 13.54/13.85 apply (zenon_L14_ zenon_TT0_v zenon_TT_u zenon_TX_w); trivial. % 13.54/13.85 exact (zenon_H84 zenon_H7f). % 13.54/13.85 Qed. % 13.54/13.85 % SZS output end Proof % 13.54/13.85 (* END-PROOF *) % 13.54/13.85 nodes searched: 392338 % 13.54/13.85 max branch formulas: 4384 % 13.54/13.85 proof nodes created: 4781 % 13.54/13.85 formulas created: 132844 % 13.54/13.85 %------------------------------------------------------------------------------