%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT008+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.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:16 AM UTC 2026 % Result : Theorem 4.78s 5.11s % Output : Proof 4.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT008+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.08/0.36 % Computer : n026.cluster.edu % 0.08/0.36 % Model : x86_64 x86_64 % 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.36 % Memory : 8046.5625MB % 0.08/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 11:47:27 UTC 2026 % 0.10/0.36 % CPUTime : % 4.78/5.11 (* PROOF-FOUND *) % 4.78/5.11 % SZS status Theorem % 4.78/5.11 (* BEGIN-PROOF *) % 4.78/5.11 % SZS output start Proof % 4.78/5.11 Theorem t8_FOL : (forall X : zenon_U, (forall Y : zenon_U, (forall C : zenon_U, (forall P1 : zenon_U, (forall P2 : zenon_U, (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X T1)/\((organization Y T2)/\((reorganization_free X T1 T1)/\((reorganization_free Y T2 T2)/\((class X C T1)/\((class Y C T2)/\((survival_chance X P1 T1)/\((survival_chance Y P2 T2)/\((size X S1 T1)/\((size Y S2 T2)/\(greater S2 S1)))))))))))->(greater P2 P1))))))))))). % 4.78/5.11 Proof. % 4.78/5.11 assert (zenon_L1_ : forall (zenon_TP2_p : zenon_U) (zenon_TP1_q : zenon_U) (zenon_TI_r : zenon_U) (zenon_TI_s : zenon_U) (zenon_TT2_t : zenon_U) (zenon_TY_u : zenon_U) (zenon_TT1_v : zenon_U) (zenon_TX_w : zenon_U), (forall I2 : zenon_U, (forall P1 : zenon_U, (forall P2 : zenon_U, (((organization zenon_TX_w zenon_TT1_v)/\((organization zenon_TY_u zenon_TT2_t)/\((reorganization_free zenon_TX_w zenon_TT1_v zenon_TT1_v)/\((reorganization_free zenon_TY_u zenon_TT2_t zenon_TT2_t)/\((inertia zenon_TX_w zenon_TI_s zenon_TT1_v)/\((inertia zenon_TY_u I2 zenon_TT2_t)/\((survival_chance zenon_TX_w P1 zenon_TT1_v)/\((survival_chance zenon_TY_u P2 zenon_TT2_t)/\(greater I2 zenon_TI_s)))))))))->(greater P2 P1))))) -> (organization zenon_TX_w zenon_TT1_v) -> (organization zenon_TY_u zenon_TT2_t) -> (reorganization_free zenon_TX_w zenon_TT1_v zenon_TT1_v) -> (reorganization_free zenon_TY_u zenon_TT2_t zenon_TT2_t) -> (inertia zenon_TX_w zenon_TI_s zenon_TT1_v) -> (inertia zenon_TY_u zenon_TI_r zenon_TT2_t) -> (survival_chance zenon_TX_w zenon_TP1_q zenon_TT1_v) -> (survival_chance zenon_TY_u zenon_TP2_p zenon_TT2_t) -> (greater zenon_TI_r zenon_TI_s) -> (~(greater zenon_TP2_p zenon_TP1_q)) -> False). % 4.78/5.11 do 8 intro. intros zenon_H4 zenon_H5 zenon_H6 zenon_H7 zenon_H8 zenon_H9 zenon_Ha zenon_Hb zenon_Hc zenon_Hd zenon_He. % 4.78/5.11 generalize (zenon_H4 zenon_TI_r). zenon_intro zenon_H17. % 4.78/5.11 generalize (zenon_H17 zenon_TP1_q). zenon_intro zenon_H18. % 4.78/5.11 generalize (zenon_H18 zenon_TP2_p). zenon_intro zenon_H19. % 4.78/5.11 apply (zenon_imply_s _ _ zenon_H19); [ zenon_intro zenon_H1b | zenon_intro zenon_H1a ]. % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 4.78/5.11 exact (zenon_H1d zenon_H5). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H1c); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 4.78/5.11 exact (zenon_H1f zenon_H6). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H1e); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 4.78/5.11 exact (zenon_H21 zenon_H7). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H20); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 4.78/5.11 exact (zenon_H23 zenon_H8). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H22); [ zenon_intro zenon_H25 | zenon_intro zenon_H24 ]. % 4.78/5.11 exact (zenon_H25 zenon_H9). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 4.78/5.11 exact (zenon_H27 zenon_Ha). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 4.78/5.11 exact (zenon_H29 zenon_Hb). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H28); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 4.78/5.11 exact (zenon_H2b zenon_Hc). % 4.78/5.11 exact (zenon_H2a zenon_Hd). % 4.78/5.11 exact (zenon_He zenon_H1a). % 4.78/5.11 (* end of lemma zenon_L1_ *) % 4.78/5.11 apply NNPP. intro zenon_G. % 4.78/5.11 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (forall C : zenon_U, (forall P1 : zenon_U, (forall P2 : zenon_U, (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X T1)/\((organization Y T2)/\((reorganization_free X T1 T1)/\((reorganization_free Y T2 T2)/\((class X C T1)/\((class Y C T2)/\((survival_chance X P1 T1)/\((survival_chance Y P2 T2)/\((size X S1 T1)/\((size Y S2 T2)/\(greater S2 S1)))))))))))->(greater P2 P1))))))))))) zenon_G); [ zenon_intro zenon_H2c; idtac ]. % 4.78/5.11 elim zenon_H2c. zenon_intro zenon_TX_w. zenon_intro zenon_H2d. % 4.78/5.11 apply (zenon_notallex_s (fun Y : zenon_U => (forall C : zenon_U, (forall P1 : zenon_U, (forall P2 : zenon_U, (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_w T1)/\((organization Y T2)/\((reorganization_free zenon_TX_w T1 T1)/\((reorganization_free Y T2 T2)/\((class zenon_TX_w C T1)/\((class Y C T2)/\((survival_chance zenon_TX_w P1 T1)/\((survival_chance Y P2 T2)/\((size zenon_TX_w S1 T1)/\((size Y S2 T2)/\(greater S2 S1)))))))))))->(greater P2 P1)))))))))) zenon_H2d); [ zenon_intro zenon_H2e; idtac ]. % 4.78/5.11 elim zenon_H2e. zenon_intro zenon_TY_u. zenon_intro zenon_H2f. % 4.78/5.11 apply (zenon_notallex_s (fun C : zenon_U => (forall P1 : zenon_U, (forall P2 : zenon_U, (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_w T1)/\((organization zenon_TY_u T2)/\((reorganization_free zenon_TX_w T1 T1)/\((reorganization_free zenon_TY_u T2 T2)/\((class zenon_TX_w C T1)/\((class zenon_TY_u C T2)/\((survival_chance zenon_TX_w P1 T1)/\((survival_chance zenon_TY_u P2 T2)/\((size zenon_TX_w S1 T1)/\((size zenon_TY_u S2 T2)/\(greater S2 S1)))))))))))->(greater P2 P1))))))))) zenon_H2f); [ zenon_intro zenon_H30; idtac ]. % 4.78/5.11 elim zenon_H30. zenon_intro zenon_TC_bx. zenon_intro zenon_H32. % 4.78/5.11 apply (zenon_notallex_s (fun P1 : zenon_U => (forall P2 : zenon_U, (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_w T1)/\((organization zenon_TY_u T2)/\((reorganization_free zenon_TX_w T1 T1)/\((reorganization_free zenon_TY_u T2 T2)/\((class zenon_TX_w zenon_TC_bx T1)/\((class zenon_TY_u zenon_TC_bx T2)/\((survival_chance zenon_TX_w P1 T1)/\((survival_chance zenon_TY_u P2 T2)/\((size zenon_TX_w S1 T1)/\((size zenon_TY_u S2 T2)/\(greater S2 S1)))))))))))->(greater P2 P1)))))))) zenon_H32); [ zenon_intro zenon_H33; idtac ]. % 4.78/5.11 elim zenon_H33. zenon_intro zenon_TP1_q. zenon_intro zenon_H34. % 4.78/5.11 apply (zenon_notallex_s (fun P2 : zenon_U => (forall S1 : zenon_U, (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_w T1)/\((organization zenon_TY_u T2)/\((reorganization_free zenon_TX_w T1 T1)/\((reorganization_free zenon_TY_u T2 T2)/\((class zenon_TX_w zenon_TC_bx T1)/\((class zenon_TY_u zenon_TC_bx T2)/\((survival_chance zenon_TX_w zenon_TP1_q T1)/\((survival_chance zenon_TY_u P2 T2)/\((size zenon_TX_w S1 T1)/\((size zenon_TY_u S2 T2)/\(greater S2 S1)))))))))))->(greater P2 zenon_TP1_q))))))) zenon_H34); [ zenon_intro zenon_H35; idtac ]. % 4.78/5.11 elim zenon_H35. zenon_intro zenon_TP2_p. zenon_intro zenon_H36. % 4.78/5.11 apply (zenon_notallex_s (fun S1 : zenon_U => (forall S2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_w T1)/\((organization zenon_TY_u T2)/\((reorganization_free zenon_TX_w T1 T1)/\((reorganization_free zenon_TY_u T2 T2)/\((class zenon_TX_w zenon_TC_bx T1)/\((class zenon_TY_u zenon_TC_bx T2)/\((survival_chance zenon_TX_w zenon_TP1_q T1)/\((survival_chance zenon_TY_u zenon_TP2_p T2)/\((size zenon_TX_w S1 T1)/\((size zenon_TY_u S2 T2)/\(greater S2 S1)))))))))))->(greater zenon_TP2_p zenon_TP1_q)))))) zenon_H36); [ zenon_intro zenon_H37; idtac ]. % 4.78/5.11 elim zenon_H37. zenon_intro zenon_TS1_ce. zenon_intro zenon_H39. % 4.78/5.11 apply (zenon_notallex_s (fun S2 : zenon_U => (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_w T1)/\((organization zenon_TY_u T2)/\((reorganization_free zenon_TX_w T1 T1)/\((reorganization_free zenon_TY_u T2 T2)/\((class zenon_TX_w zenon_TC_bx T1)/\((class zenon_TY_u zenon_TC_bx T2)/\((survival_chance zenon_TX_w zenon_TP1_q T1)/\((survival_chance zenon_TY_u zenon_TP2_p T2)/\((size zenon_TX_w zenon_TS1_ce T1)/\((size zenon_TY_u S2 T2)/\(greater S2 zenon_TS1_ce)))))))))))->(greater zenon_TP2_p zenon_TP1_q))))) zenon_H39); [ zenon_intro zenon_H3a; idtac ]. % 4.78/5.11 elim zenon_H3a. zenon_intro zenon_TS2_ch. zenon_intro zenon_H3c. % 4.78/5.11 apply (zenon_notallex_s (fun T1 : zenon_U => (forall T2 : zenon_U, (((organization zenon_TX_w T1)/\((organization zenon_TY_u T2)/\((reorganization_free zenon_TX_w T1 T1)/\((reorganization_free zenon_TY_u T2 T2)/\((class zenon_TX_w zenon_TC_bx T1)/\((class zenon_TY_u zenon_TC_bx T2)/\((survival_chance zenon_TX_w zenon_TP1_q T1)/\((survival_chance zenon_TY_u zenon_TP2_p T2)/\((size zenon_TX_w zenon_TS1_ce T1)/\((size zenon_TY_u zenon_TS2_ch T2)/\(greater zenon_TS2_ch zenon_TS1_ce)))))))))))->(greater zenon_TP2_p zenon_TP1_q)))) zenon_H3c); [ zenon_intro zenon_H3d; idtac ]. % 4.78/5.11 elim zenon_H3d. zenon_intro zenon_TT1_v. zenon_intro zenon_H3e. % 4.78/5.11 apply (zenon_notallex_s (fun T2 : zenon_U => (((organization zenon_TX_w zenon_TT1_v)/\((organization zenon_TY_u T2)/\((reorganization_free zenon_TX_w zenon_TT1_v zenon_TT1_v)/\((reorganization_free zenon_TY_u T2 T2)/\((class zenon_TX_w zenon_TC_bx zenon_TT1_v)/\((class zenon_TY_u zenon_TC_bx T2)/\((survival_chance zenon_TX_w zenon_TP1_q zenon_TT1_v)/\((survival_chance zenon_TY_u zenon_TP2_p T2)/\((size zenon_TX_w zenon_TS1_ce zenon_TT1_v)/\((size zenon_TY_u zenon_TS2_ch T2)/\(greater zenon_TS2_ch zenon_TS1_ce)))))))))))->(greater zenon_TP2_p zenon_TP1_q))) zenon_H3e); [ zenon_intro zenon_H3f; idtac ]. % 4.78/5.11 elim zenon_H3f. zenon_intro zenon_TT2_t. zenon_intro zenon_H40. % 4.78/5.11 apply (zenon_notimply_s _ _ zenon_H40). zenon_intro zenon_H41. zenon_intro zenon_He. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H41). zenon_intro zenon_H5. zenon_intro zenon_H42. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H42). zenon_intro zenon_H6. zenon_intro zenon_H43. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H43). zenon_intro zenon_H7. zenon_intro zenon_H44. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H44). zenon_intro zenon_H8. zenon_intro zenon_H45. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H45). zenon_intro zenon_H47. zenon_intro zenon_H46. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H46). zenon_intro zenon_H49. zenon_intro zenon_H48. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_Hb. zenon_intro zenon_H4a. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H4a). zenon_intro zenon_Hc. zenon_intro zenon_H4b. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H4b). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 4.78/5.11 apply (zenon_and_s _ _ zenon_H4c). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 4.78/5.11 generalize (a5_FOL zenon_TX_w). zenon_intro zenon_H50. % 4.78/5.11 generalize (t1_FOL zenon_TX_w). zenon_intro zenon_H51. % 4.78/5.11 generalize (zenon_H50 zenon_TY_u). zenon_intro zenon_H52. % 4.78/5.11 generalize (zenon_H51 zenon_TY_u). zenon_intro zenon_H53. % 4.78/5.11 generalize (zenon_H52 zenon_TC_bx). zenon_intro zenon_H54. % 4.78/5.11 generalize (zenon_H54 zenon_TS1_ce). zenon_intro zenon_H55. % 4.78/5.11 generalize (zenon_H55 zenon_TS2_ch). zenon_intro zenon_H56. % 4.78/5.11 generalize (zenon_H53 zenon_TT1_v). zenon_intro zenon_H57. % 4.78/5.11 generalize (zenon_H57 zenon_TT2_t). zenon_intro zenon_H58. % 4.78/5.11 generalize (mp5 zenon_TX_w). zenon_intro zenon_H59. % 4.78/5.11 generalize (mp5 zenon_TY_u). zenon_intro zenon_H5a. % 4.78/5.11 generalize (zenon_H59 zenon_TT1_v). zenon_intro zenon_H5b. % 4.78/5.11 apply (zenon_imply_s _ _ zenon_H5b); [ zenon_intro zenon_H1d | zenon_intro zenon_H5c ]. % 4.78/5.11 exact (zenon_H1d zenon_H5). % 4.78/5.11 elim zenon_H5c. zenon_intro zenon_TI_s. zenon_intro zenon_H9. % 4.78/5.11 generalize (zenon_H56 zenon_TI_s). zenon_intro zenon_H5d. % 4.78/5.11 generalize (zenon_H58 zenon_TI_s). zenon_intro zenon_H4. % 4.78/5.11 generalize (zenon_H5a zenon_TT2_t). zenon_intro zenon_H5e. % 4.78/5.11 apply (zenon_imply_s _ _ zenon_H5e); [ zenon_intro zenon_H1f | zenon_intro zenon_H5f ]. % 4.78/5.11 exact (zenon_H1f zenon_H6). % 4.78/5.11 elim zenon_H5f. zenon_intro zenon_TI_r. zenon_intro zenon_Ha. % 4.78/5.11 generalize (zenon_H5d zenon_TI_r). zenon_intro zenon_H60. % 4.78/5.11 generalize (zenon_H60 zenon_TT1_v). zenon_intro zenon_H61. % 4.78/5.11 generalize (zenon_H61 zenon_TT2_t). zenon_intro zenon_H62. % 4.78/5.11 apply (zenon_imply_s _ _ zenon_H62); [ zenon_intro zenon_H63 | zenon_intro zenon_Hd ]. % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H1d | zenon_intro zenon_H64 ]. % 4.78/5.11 exact (zenon_H1d zenon_H5). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H64); [ zenon_intro zenon_H1f | zenon_intro zenon_H65 ]. % 4.78/5.11 exact (zenon_H1f zenon_H6). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H65); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 4.78/5.11 exact (zenon_H67 zenon_H47). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H69 | zenon_intro zenon_H68 ]. % 4.78/5.11 exact (zenon_H69 zenon_H49). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 4.78/5.11 exact (zenon_H6b zenon_H4d). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 4.78/5.11 exact (zenon_H6d zenon_H4f). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H25 | zenon_intro zenon_H6e ]. % 4.78/5.11 exact (zenon_H25 zenon_H9). % 4.78/5.11 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H27 | zenon_intro zenon_H6f ]. % 4.78/5.12 exact (zenon_H27 zenon_Ha). % 4.78/5.12 exact (zenon_H6f zenon_H4e). % 4.78/5.12 apply (zenon_L1_ zenon_TP2_p zenon_TP1_q zenon_TI_r zenon_TI_s zenon_TT2_t zenon_TY_u zenon_TT1_v zenon_TX_w); trivial. % 4.78/5.12 Qed. % 4.78/5.12 % SZS output end Proof % 4.78/5.12 (* END-PROOF *) % 4.78/5.12 nodes searched: 3810 % 4.78/5.12 max branch formulas: 2219 % 4.78/5.12 proof nodes created: 814 % 4.78/5.12 formulas created: 45175 % 4.78/5.12 %------------------------------------------------------------------------------