%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT002+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n009.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:15 AM UTC 2026 % Result : Theorem 0.57s 0.98s % Output : Proof 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT002+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.43 % Computer : n009.cluster.edu % 0.09/0.43 % Model : x86_64 x86_64 % 0.09/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.43 % Memory : 8046.5625MB % 0.09/0.43 % OS : Linux 6.8.0-71-generic % 0.09/0.43 % CPULimit : 300 % 0.09/0.43 % WCLimit : 300 % 0.09/0.43 % DateTime : Mon Sep 7 11:32:37 UTC 2026 % 0.09/0.43 % CPUTime : % 0.57/0.98 (* PROOF-FOUND *) % 0.57/0.98 % SZS status Theorem % 0.57/0.98 (* BEGIN-PROOF *) % 0.57/0.98 % SZS output start Proof % 0.57/0.98 Theorem t2_FOL : (forall X : zenon_U, (forall I1 : zenon_U, (forall I2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X T1)/\((organization X T2)/\((reorganization_free X T1 T2)/\((inertia X I1 T1)/\((inertia X I2 T2)/\(greater T2 T1))))))->(greater I2 I1))))))). % 0.57/0.98 Proof. % 0.57/0.98 assert (zenon_L1_ : forall (zenon_TT2_h : zenon_U) (zenon_TT1_i : zenon_U) (zenon_TX_j : zenon_U), (reorganization_free zenon_TX_j zenon_TT1_i zenon_TT2_h) -> (~(reorganization_free zenon_TX_j zenon_TT1_i zenon_TT1_i)) -> False). % 0.57/0.98 do 3 intro. intros zenon_H5 zenon_H6. % 0.57/0.98 generalize (mp4 zenon_TX_j). zenon_intro zenon_Ha. % 0.57/0.98 generalize (zenon_Ha zenon_TT1_i). zenon_intro zenon_Hb. % 0.57/0.98 generalize (zenon_Hb zenon_TT2_h). zenon_intro zenon_Hc. % 0.57/0.98 apply (zenon_imply_s _ _ zenon_Hc); [ zenon_intro zenon_He | zenon_intro zenon_Hd ]. % 0.57/0.98 exact (zenon_He zenon_H5). % 0.57/0.98 apply (zenon_and_s _ _ zenon_Hd). zenon_intro zenon_H10. zenon_intro zenon_Hf. % 0.57/0.98 exact (zenon_H6 zenon_H10). % 0.57/0.98 (* end of lemma zenon_L1_ *) % 0.57/0.98 assert (zenon_L2_ : forall (zenon_TT2_h : zenon_U) (zenon_TT1_i : zenon_U) (zenon_TX_j : zenon_U), (reorganization_free zenon_TX_j zenon_TT1_i zenon_TT2_h) -> (~(reorganization_free zenon_TX_j zenon_TT2_h zenon_TT2_h)) -> False). % 0.57/0.98 do 3 intro. intros zenon_H5 zenon_H11. % 0.57/0.98 generalize (mp4 zenon_TX_j). zenon_intro zenon_Ha. % 0.57/0.98 generalize (zenon_Ha zenon_TT1_i). zenon_intro zenon_Hb. % 0.57/0.98 generalize (zenon_Hb zenon_TT2_h). zenon_intro zenon_Hc. % 0.57/0.98 apply (zenon_imply_s _ _ zenon_Hc); [ zenon_intro zenon_He | zenon_intro zenon_Hd ]. % 0.57/0.98 exact (zenon_He zenon_H5). % 0.57/0.98 apply (zenon_and_s _ _ zenon_Hd). zenon_intro zenon_H10. zenon_intro zenon_Hf. % 0.57/0.98 exact (zenon_H11 zenon_Hf). % 0.57/0.98 (* end of lemma zenon_L2_ *) % 0.57/0.98 assert (zenon_L3_ : forall (zenon_TRp_z : zenon_U) (zenon_TT2_h : zenon_U) (zenon_TT1_i : zenon_U) (zenon_TRp_ba : zenon_U) (zenon_TX_j : zenon_U), (forall Rp2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_j T1)/\((organization zenon_TX_j T2)/\((reorganization_free zenon_TX_j T1 T2)/\((reproducibility zenon_TX_j zenon_TRp_ba T1)/\((reproducibility zenon_TX_j Rp2 T2)/\(greater T2 T1))))))->(greater Rp2 zenon_TRp_ba))))) -> (organization zenon_TX_j zenon_TT1_i) -> (organization zenon_TX_j zenon_TT2_h) -> (reorganization_free zenon_TX_j zenon_TT1_i zenon_TT2_h) -> (reproducibility zenon_TX_j zenon_TRp_ba zenon_TT1_i) -> (reproducibility zenon_TX_j zenon_TRp_z zenon_TT2_h) -> (greater zenon_TT2_h zenon_TT1_i) -> (~(greater zenon_TRp_z zenon_TRp_ba)) -> False). % 0.57/0.98 do 5 intro. intros zenon_H12 zenon_H13 zenon_H14 zenon_H5 zenon_H15 zenon_H16 zenon_H17 zenon_H18. % 0.57/0.98 generalize (zenon_H12 zenon_TRp_z). zenon_intro zenon_H1b. % 0.57/0.98 generalize (zenon_H1b zenon_TT1_i). zenon_intro zenon_H1c. % 0.57/0.98 generalize (zenon_H1c zenon_TT2_h). zenon_intro zenon_H1d. % 0.57/0.98 apply (zenon_imply_s _ _ zenon_H1d); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H1f); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 0.57/0.98 exact (zenon_H21 zenon_H13). % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H20); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 0.57/0.98 exact (zenon_H23 zenon_H14). % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H22); [ zenon_intro zenon_He | zenon_intro zenon_H24 ]. % 0.57/0.98 exact (zenon_He zenon_H5). % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_H26 | zenon_intro zenon_H25 ]. % 0.57/0.98 exact (zenon_H26 zenon_H15). % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H25); [ zenon_intro zenon_H28 | zenon_intro zenon_H27 ]. % 0.57/0.98 exact (zenon_H28 zenon_H16). % 0.57/0.98 exact (zenon_H27 zenon_H17). % 0.57/0.98 exact (zenon_H18 zenon_H1e). % 0.57/0.98 (* end of lemma zenon_L3_ *) % 0.57/0.98 apply NNPP. intro zenon_G. % 0.57/0.98 apply (zenon_notallex_s (fun X : zenon_U => (forall I1 : zenon_U, (forall I2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization X T1)/\((organization X T2)/\((reorganization_free X T1 T2)/\((inertia X I1 T1)/\((inertia X I2 T2)/\(greater T2 T1))))))->(greater I2 I1))))))) zenon_G); [ zenon_intro zenon_H29; idtac ]. % 0.57/0.98 elim zenon_H29. zenon_intro zenon_TX_j. zenon_intro zenon_H2a. % 0.57/0.98 apply (zenon_notallex_s (fun I1 : zenon_U => (forall I2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_j T1)/\((organization zenon_TX_j T2)/\((reorganization_free zenon_TX_j T1 T2)/\((inertia zenon_TX_j I1 T1)/\((inertia zenon_TX_j I2 T2)/\(greater T2 T1))))))->(greater I2 I1)))))) zenon_H2a); [ zenon_intro zenon_H2b; idtac ]. % 0.57/0.98 elim zenon_H2b. zenon_intro zenon_TI1_bs. zenon_intro zenon_H2d. % 0.57/0.98 apply (zenon_notallex_s (fun I2 : zenon_U => (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_j T1)/\((organization zenon_TX_j T2)/\((reorganization_free zenon_TX_j T1 T2)/\((inertia zenon_TX_j zenon_TI1_bs T1)/\((inertia zenon_TX_j I2 T2)/\(greater T2 T1))))))->(greater I2 zenon_TI1_bs))))) zenon_H2d); [ zenon_intro zenon_H2e; idtac ]. % 0.57/0.98 elim zenon_H2e. zenon_intro zenon_TI2_bv. zenon_intro zenon_H30. % 0.57/0.98 apply (zenon_notallex_s (fun T1 : zenon_U => (forall T2 : zenon_U, (((organization zenon_TX_j T1)/\((organization zenon_TX_j T2)/\((reorganization_free zenon_TX_j T1 T2)/\((inertia zenon_TX_j zenon_TI1_bs T1)/\((inertia zenon_TX_j zenon_TI2_bv T2)/\(greater T2 T1))))))->(greater zenon_TI2_bv zenon_TI1_bs)))) zenon_H30); [ zenon_intro zenon_H31; idtac ]. % 0.57/0.98 elim zenon_H31. zenon_intro zenon_TT1_i. zenon_intro zenon_H32. % 0.57/0.98 apply (zenon_notallex_s (fun T2 : zenon_U => (((organization zenon_TX_j zenon_TT1_i)/\((organization zenon_TX_j T2)/\((reorganization_free zenon_TX_j zenon_TT1_i T2)/\((inertia zenon_TX_j zenon_TI1_bs zenon_TT1_i)/\((inertia zenon_TX_j zenon_TI2_bv T2)/\(greater T2 zenon_TT1_i))))))->(greater zenon_TI2_bv zenon_TI1_bs))) zenon_H32); [ zenon_intro zenon_H33; idtac ]. % 0.57/0.98 elim zenon_H33. zenon_intro zenon_TT2_h. zenon_intro zenon_H34. % 0.57/0.98 apply (zenon_notimply_s _ _ zenon_H34). zenon_intro zenon_H36. zenon_intro zenon_H35. % 0.57/0.98 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H13. zenon_intro zenon_H37. % 0.57/0.98 apply (zenon_and_s _ _ zenon_H37). zenon_intro zenon_H14. zenon_intro zenon_H38. % 0.57/0.98 apply (zenon_and_s _ _ zenon_H38). zenon_intro zenon_H5. zenon_intro zenon_H39. % 0.57/0.98 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 0.57/0.98 apply (zenon_and_s _ _ zenon_H3a). zenon_intro zenon_H3c. zenon_intro zenon_H17. % 0.57/0.98 generalize (a4_FOL zenon_TX_j). zenon_intro zenon_H3d. % 0.57/0.98 generalize (a3_FOL zenon_TX_j). zenon_intro zenon_H3e. % 0.57/0.98 generalize (zenon_H3e zenon_TX_j). zenon_intro zenon_H3f. % 0.57/0.98 generalize (zenon_H3f zenon_TT1_i). zenon_intro zenon_H40. % 0.57/0.98 generalize (mp3 zenon_TX_j). zenon_intro zenon_H41. % 0.57/0.98 generalize (zenon_H41 zenon_TT2_h). zenon_intro zenon_H42. % 0.57/0.98 apply (zenon_imply_s _ _ zenon_H42); [ zenon_intro zenon_H23 | zenon_intro zenon_H43 ]. % 0.57/0.98 exact (zenon_H23 zenon_H14). % 0.57/0.98 elim zenon_H43. zenon_intro zenon_TRp_z. zenon_intro zenon_H16. % 0.57/0.98 generalize (zenon_H40 zenon_TT2_h). zenon_intro zenon_H44. % 0.57/0.98 generalize (zenon_H41 zenon_TT1_i). zenon_intro zenon_H45. % 0.57/0.98 apply (zenon_imply_s _ _ zenon_H45); [ zenon_intro zenon_H21 | zenon_intro zenon_H46 ]. % 0.57/0.98 exact (zenon_H21 zenon_H13). % 0.57/0.98 elim zenon_H46. zenon_intro zenon_TRp_ba. zenon_intro zenon_H15. % 0.57/0.98 generalize (zenon_H3d zenon_TRp_ba). zenon_intro zenon_H12. % 0.57/0.98 generalize (zenon_H44 zenon_TRp_ba). zenon_intro zenon_H47. % 0.57/0.98 generalize (zenon_H47 zenon_TRp_z). zenon_intro zenon_H48. % 0.57/0.98 generalize (zenon_H48 zenon_TI1_bs). zenon_intro zenon_H49. % 0.57/0.98 generalize (zenon_H49 zenon_TI2_bv). zenon_intro zenon_H4a. % 0.57/0.98 apply (zenon_imply_s _ _ zenon_H4a); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H4c); [ zenon_intro zenon_H21 | zenon_intro zenon_H4d ]. % 0.57/0.98 exact (zenon_H21 zenon_H13). % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H23 | zenon_intro zenon_H4e ]. % 0.57/0.98 exact (zenon_H23 zenon_H14). % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H6 | zenon_intro zenon_H4f ]. % 0.57/0.98 apply (zenon_L1_ zenon_TT2_h zenon_TT1_i zenon_TX_j); trivial. % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H11 | zenon_intro zenon_H50 ]. % 0.57/0.98 apply (zenon_L2_ zenon_TT2_h zenon_TT1_i zenon_TX_j); trivial. % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H26 | zenon_intro zenon_H51 ]. % 0.57/0.98 exact (zenon_H26 zenon_H15). % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H51); [ zenon_intro zenon_H28 | zenon_intro zenon_H52 ]. % 0.57/0.98 exact (zenon_H28 zenon_H16). % 0.57/0.98 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 0.57/0.99 exact (zenon_H54 zenon_H3b). % 0.57/0.99 exact (zenon_H53 zenon_H3c). % 0.57/0.99 apply (zenon_equiv_s _ _ zenon_H4b); [ zenon_intro zenon_H18; zenon_intro zenon_H35 | zenon_intro zenon_H1e; zenon_intro zenon_H55 ]. % 0.57/0.99 apply (zenon_L3_ zenon_TRp_z zenon_TT2_h zenon_TT1_i zenon_TRp_ba zenon_TX_j); trivial. % 0.57/0.99 exact (zenon_H35 zenon_H55). % 0.57/0.99 Qed. % 0.57/0.99 % SZS output end Proof % 0.57/0.99 (* END-PROOF *) % 0.57/0.99 nodes searched: 10357 % 0.57/0.99 max branch formulas: 4355 % 0.57/0.99 proof nodes created: 1558 % 0.57/0.99 formulas created: 111390 % 0.57/0.99 %------------------------------------------------------------------------------