%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT003+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % 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:24:16 AM UTC 2026 % Result : Theorem 0.38s 0.67s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT003+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.36 % Computer : n003.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 11:35:23 UTC 2026 % 0.09/0.36 % CPUTime : % 0.38/0.67 (* PROOF-FOUND *) % 0.38/0.67 % SZS status Theorem % 0.38/0.67 (* BEGIN-PROOF *) % 0.38/0.67 % SZS output start Proof % 0.38/0.67 Theorem t3_FOL : (forall X : zenon_U, (forall P1 : zenon_U, (forall P2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X T1)/\((organization X T2)/\((reorganization_free X T1 T2)/\((survival_chance X P1 T1)/\((survival_chance X P2 T2)/\(greater T2 T1))))))->(greater P2 P1))))))). % 0.38/0.67 Proof. % 0.38/0.67 apply NNPP. intro zenon_G. % 0.38/0.67 apply (zenon_notallex_s (fun X : zenon_U => (forall P1 : zenon_U, (forall P2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X T1)/\((organization X T2)/\((reorganization_free X T1 T2)/\((survival_chance X P1 T1)/\((survival_chance X P2 T2)/\(greater T2 T1))))))->(greater P2 P1))))))) zenon_G); [ zenon_intro zenon_H5; idtac ]. % 0.38/0.67 elim zenon_H5. zenon_intro zenon_TX_g. zenon_intro zenon_H7. % 0.38/0.67 apply (zenon_notallex_s (fun P1 : zenon_U => (forall P2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_g T1)/\((organization zenon_TX_g T2)/\((reorganization_free zenon_TX_g T1 T2)/\((survival_chance zenon_TX_g P1 T1)/\((survival_chance zenon_TX_g P2 T2)/\(greater T2 T1))))))->(greater P2 P1)))))) zenon_H7); [ zenon_intro zenon_H8; idtac ]. % 0.38/0.68 elim zenon_H8. zenon_intro zenon_TP1_j. zenon_intro zenon_Ha. % 0.38/0.68 apply (zenon_notallex_s (fun P2 : zenon_U => (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_g T1)/\((organization zenon_TX_g T2)/\((reorganization_free zenon_TX_g T1 T2)/\((survival_chance zenon_TX_g zenon_TP1_j T1)/\((survival_chance zenon_TX_g P2 T2)/\(greater T2 T1))))))->(greater P2 zenon_TP1_j))))) zenon_Ha); [ zenon_intro zenon_Hb; idtac ]. % 0.38/0.68 elim zenon_Hb. zenon_intro zenon_TP2_m. zenon_intro zenon_Hd. % 0.38/0.68 apply (zenon_notallex_s (fun T1 : zenon_U => (forall T2 : zenon_U, (((organization zenon_TX_g T1)/\((organization zenon_TX_g T2)/\((reorganization_free zenon_TX_g T1 T2)/\((survival_chance zenon_TX_g zenon_TP1_j T1)/\((survival_chance zenon_TX_g zenon_TP2_m T2)/\(greater T2 T1))))))->(greater zenon_TP2_m zenon_TP1_j)))) zenon_Hd); [ zenon_intro zenon_He; idtac ]. % 0.38/0.68 elim zenon_He. zenon_intro zenon_TT1_p. zenon_intro zenon_H10. % 0.38/0.68 apply (zenon_notallex_s (fun T2 : zenon_U => (((organization zenon_TX_g zenon_TT1_p)/\((organization zenon_TX_g T2)/\((reorganization_free zenon_TX_g zenon_TT1_p T2)/\((survival_chance zenon_TX_g zenon_TP1_j zenon_TT1_p)/\((survival_chance zenon_TX_g zenon_TP2_m T2)/\(greater T2 zenon_TT1_p))))))->(greater zenon_TP2_m zenon_TP1_j))) zenon_H10); [ zenon_intro zenon_H11; idtac ]. % 0.38/0.68 elim zenon_H11. zenon_intro zenon_TT2_s. zenon_intro zenon_H13. % 0.38/0.68 apply (zenon_notimply_s _ _ zenon_H13). zenon_intro zenon_H15. zenon_intro zenon_H14. % 0.38/0.68 apply (zenon_and_s _ _ zenon_H15). zenon_intro zenon_H17. zenon_intro zenon_H16. % 0.38/0.68 apply (zenon_and_s _ _ zenon_H16). zenon_intro zenon_H19. zenon_intro zenon_H18. % 0.38/0.68 apply (zenon_and_s _ _ zenon_H18). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 0.38/0.68 apply (zenon_and_s _ _ zenon_H1a). zenon_intro zenon_H1d. zenon_intro zenon_H1c. % 0.38/0.68 apply (zenon_and_s _ _ zenon_H1c). zenon_intro zenon_H1f. zenon_intro zenon_H1e. % 0.38/0.68 generalize (t1_FOL zenon_TX_g). zenon_intro zenon_H20. % 0.38/0.68 generalize (t2_FOL zenon_TX_g). zenon_intro zenon_H21. % 0.38/0.68 generalize (zenon_H20 zenon_TX_g). zenon_intro zenon_H22. % 0.38/0.68 generalize (zenon_H22 zenon_TT1_p). zenon_intro zenon_H23. % 0.38/0.68 generalize (zenon_H23 zenon_TT2_s). zenon_intro zenon_H24. % 0.38/0.68 generalize (mp5 zenon_TX_g). zenon_intro zenon_H25. % 0.38/0.68 generalize (zenon_H25 zenon_TT1_p). zenon_intro zenon_H26. % 0.38/0.68 apply (zenon_imply_s _ _ zenon_H26); [ zenon_intro zenon_H28 | zenon_intro zenon_H27 ]. % 0.38/0.68 exact (zenon_H28 zenon_H17). % 0.38/0.68 elim zenon_H27. zenon_intro zenon_TI_bp. zenon_intro zenon_H2a. % 0.38/0.68 generalize (zenon_H21 zenon_TI_bp). zenon_intro zenon_H2b. % 0.38/0.68 generalize (zenon_H24 zenon_TI_bp). zenon_intro zenon_H2c. % 0.38/0.68 generalize (zenon_H25 zenon_TT2_s). zenon_intro zenon_H2d. % 0.38/0.68 apply (zenon_imply_s _ _ zenon_H2d); [ zenon_intro zenon_H2f | zenon_intro zenon_H2e ]. % 0.38/0.68 exact (zenon_H2f zenon_H19). % 0.38/0.68 elim zenon_H2e. zenon_intro zenon_TI_bw. zenon_intro zenon_H31. % 0.38/0.68 generalize (zenon_H2c zenon_TI_bw). zenon_intro zenon_H32. % 0.38/0.68 generalize (zenon_H32 zenon_TP1_j). zenon_intro zenon_H33. % 0.38/0.68 generalize (zenon_H33 zenon_TP2_m). zenon_intro zenon_H34. % 0.38/0.68 apply (zenon_imply_s _ _ zenon_H34); [ zenon_intro zenon_H36 | zenon_intro zenon_H35 ]. % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H28 | zenon_intro zenon_H37 ]. % 0.38/0.68 exact (zenon_H28 zenon_H17). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H2f | zenon_intro zenon_H38 ]. % 0.38/0.68 exact (zenon_H2f zenon_H19). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H3a | zenon_intro zenon_H39 ]. % 0.38/0.68 generalize (mp4 zenon_TX_g). zenon_intro zenon_H3b. % 0.38/0.68 generalize (zenon_H3b zenon_TT1_p). zenon_intro zenon_H3c. % 0.38/0.68 generalize (zenon_H3c zenon_TT2_s). zenon_intro zenon_H3d. % 0.38/0.68 apply (zenon_imply_s _ _ zenon_H3d); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 0.38/0.68 exact (zenon_H3f zenon_H1b). % 0.38/0.68 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 0.38/0.68 exact (zenon_H3a zenon_H41). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H39); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 0.38/0.68 generalize (mp4 zenon_TX_g). zenon_intro zenon_H3b. % 0.38/0.68 generalize (zenon_H3b zenon_TT1_p). zenon_intro zenon_H3c. % 0.38/0.68 generalize (zenon_H3c zenon_TT2_s). zenon_intro zenon_H3d. % 0.38/0.68 apply (zenon_imply_s _ _ zenon_H3d); [ zenon_intro zenon_H3f | zenon_intro zenon_H3e ]. % 0.38/0.68 exact (zenon_H3f zenon_H1b). % 0.38/0.68 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 0.38/0.68 exact (zenon_H43 zenon_H40). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H42); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 0.38/0.68 exact (zenon_H45 zenon_H2a). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H44); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 0.38/0.68 exact (zenon_H47 zenon_H31). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H49 | zenon_intro zenon_H48 ]. % 0.38/0.68 exact (zenon_H49 zenon_H1d). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 0.38/0.68 exact (zenon_H4b zenon_H1f). % 0.38/0.68 generalize (zenon_H2b zenon_TI_bw). zenon_intro zenon_H4c. % 0.38/0.68 generalize (zenon_H4c zenon_TT1_p). zenon_intro zenon_H4d. % 0.38/0.68 generalize (zenon_H4d zenon_TT2_s). zenon_intro zenon_H4e. % 0.38/0.68 apply (zenon_imply_s _ _ zenon_H4e); [ zenon_intro zenon_H50 | zenon_intro zenon_H4f ]. % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H28 | zenon_intro zenon_H51 ]. % 0.38/0.68 exact (zenon_H28 zenon_H17). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H51); [ zenon_intro zenon_H2f | zenon_intro zenon_H52 ]. % 0.38/0.68 exact (zenon_H2f zenon_H19). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H3f | zenon_intro zenon_H53 ]. % 0.38/0.68 exact (zenon_H3f zenon_H1b). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H53); [ zenon_intro zenon_H45 | zenon_intro zenon_H54 ]. % 0.38/0.68 exact (zenon_H45 zenon_H2a). % 0.38/0.68 apply (zenon_notand_s _ _ zenon_H54); [ zenon_intro zenon_H47 | zenon_intro zenon_H55 ]. % 0.38/0.68 exact (zenon_H47 zenon_H31). % 0.38/0.68 exact (zenon_H55 zenon_H1e). % 0.38/0.68 exact (zenon_H4a zenon_H4f). % 0.38/0.68 exact (zenon_H14 zenon_H35). % 0.38/0.68 Qed. % 0.38/0.68 % SZS output end Proof % 0.38/0.68 (* END-PROOF *) % 0.38/0.68 nodes searched: 6657 % 0.38/0.68 max branch formulas: 2667 % 0.38/0.68 proof nodes created: 1092 % 0.38/0.68 formulas created: 52415 % 0.38/0.68 %------------------------------------------------------------------------------