%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT015+1 : TPTP v9.3.0. Released v2.0.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:17 AM UTC 2026 % Result : Theorem 206.24s 206.66s % Output : Proof 0.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT015+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.36 % Computer : n006.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:54:01 UTC 2026 % 0.09/0.36 % CPUTime : % 206.24/206.66 (* PROOF-FOUND *) % 206.24/206.66 % SZS status Theorem % 206.24/206.66 (* BEGIN-PROOF *) % 206.24/206.66 % SZS output start Proof % 206.24/206.66 Theorem t15_FOL : (forall X : zenon_U, (forall Y : zenon_U, (forall Re : zenon_U, (forall C : zenon_U, (forall C1 : zenon_U, (forall C2 : zenon_U, (forall Ta : zenon_U, (forall Tb : zenon_U, (forall Tc : zenon_U, (((organization X Ta)/\((organization Y Ta)/\((organization Y Tc)/\((class X C Ta)/\((class Y C Ta)/\((reorganization X Ta Tb)/\((reorganization Y Ta Tc)/\((reorganization_type X Re Ta)/\((reorganization_type Y Re Ta)/\((complexity X C1 Ta)/\((complexity Y C2 Ta)/\(greater C2 C1))))))))))))->(greater Tc Tb))))))))))). % 206.24/206.66 Proof. % 206.24/206.66 assert (zenon_L1_ : forall (zenon_TI_p : zenon_U) (zenon_TTa_q : zenon_U) (zenon_TI_r : zenon_U) (zenon_TC2_s : zenon_U) (zenon_TC1_t : zenon_U) (zenon_TC_u : zenon_U) (zenon_TY_v : zenon_U) (zenon_TX_w : zenon_U), (forall I2 : zenon_U, (forall T1 : zenon_U, (forall T2 : zenon_U, (((organization zenon_TX_w T1)/\((organization zenon_TY_v T2)/\((class zenon_TX_w zenon_TC_u T1)/\((class zenon_TY_v zenon_TC_u T2)/\((complexity zenon_TX_w zenon_TC1_t T1)/\((complexity zenon_TY_v zenon_TC2_s T2)/\((inertia zenon_TX_w zenon_TI_r T1)/\((inertia zenon_TY_v I2 T2)/\(greater zenon_TC2_s zenon_TC1_t)))))))))->(greater I2 zenon_TI_r))))) -> (organization zenon_TX_w zenon_TTa_q) -> (organization zenon_TY_v zenon_TTa_q) -> (class zenon_TX_w zenon_TC_u zenon_TTa_q) -> (class zenon_TY_v zenon_TC_u zenon_TTa_q) -> (complexity zenon_TX_w zenon_TC1_t zenon_TTa_q) -> (complexity zenon_TY_v zenon_TC2_s zenon_TTa_q) -> (inertia zenon_TX_w zenon_TI_r zenon_TTa_q) -> (inertia zenon_TY_v zenon_TI_p zenon_TTa_q) -> (greater zenon_TC2_s zenon_TC1_t) -> (~(greater zenon_TI_p zenon_TI_r)) -> False). % 206.24/206.66 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. % 206.24/206.66 generalize (zenon_H4 zenon_TI_p). zenon_intro zenon_H17. % 206.24/206.66 generalize (zenon_H17 zenon_TTa_q). zenon_intro zenon_H18. % 206.24/206.66 generalize (zenon_H18 zenon_TTa_q). zenon_intro zenon_H19. % 206.24/206.66 apply (zenon_imply_s _ _ zenon_H19); [ zenon_intro zenon_H1b | zenon_intro zenon_H1a ]. % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 206.24/206.66 exact (zenon_H1d zenon_H5). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H1c); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 206.24/206.66 exact (zenon_H1f zenon_H6). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H1e); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 206.24/206.66 exact (zenon_H21 zenon_H7). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H20); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 206.24/206.66 exact (zenon_H23 zenon_H8). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H22); [ zenon_intro zenon_H25 | zenon_intro zenon_H24 ]. % 206.24/206.66 exact (zenon_H25 zenon_H9). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 206.24/206.66 exact (zenon_H27 zenon_Ha). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 206.24/206.66 exact (zenon_H29 zenon_Hb). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H28); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 206.24/206.66 exact (zenon_H2b zenon_Hc). % 206.24/206.66 exact (zenon_H2a zenon_Hd). % 206.24/206.66 exact (zenon_He zenon_H1a). % 206.24/206.66 (* end of lemma zenon_L1_ *) % 206.24/206.66 apply NNPP. intro zenon_G. % 206.24/206.66 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (forall Re : zenon_U, (forall C : zenon_U, (forall C1 : zenon_U, (forall C2 : zenon_U, (forall Ta : zenon_U, (forall Tb : zenon_U, (forall Tc : zenon_U, (((organization X Ta)/\((organization Y Ta)/\((organization Y Tc)/\((class X C Ta)/\((class Y C Ta)/\((reorganization X Ta Tb)/\((reorganization Y Ta Tc)/\((reorganization_type X Re Ta)/\((reorganization_type Y Re Ta)/\((complexity X C1 Ta)/\((complexity Y C2 Ta)/\(greater C2 C1))))))))))))->(greater Tc Tb))))))))))) zenon_G); [ zenon_intro zenon_H2c; idtac ]. % 206.24/206.66 elim zenon_H2c. zenon_intro zenon_TX_w. zenon_intro zenon_H2d. % 206.24/206.66 apply (zenon_notallex_s (fun Y : zenon_U => (forall Re : zenon_U, (forall C : zenon_U, (forall C1 : zenon_U, (forall C2 : zenon_U, (forall Ta : zenon_U, (forall Tb : zenon_U, (forall Tc : zenon_U, (((organization zenon_TX_w Ta)/\((organization Y Ta)/\((organization Y Tc)/\((class zenon_TX_w C Ta)/\((class Y C Ta)/\((reorganization zenon_TX_w Ta Tb)/\((reorganization Y Ta Tc)/\((reorganization_type zenon_TX_w Re Ta)/\((reorganization_type Y Re Ta)/\((complexity zenon_TX_w C1 Ta)/\((complexity Y C2 Ta)/\(greater C2 C1))))))))))))->(greater Tc Tb)))))))))) zenon_H2d); [ zenon_intro zenon_H2e; idtac ]. % 206.24/206.66 elim zenon_H2e. zenon_intro zenon_TY_v. zenon_intro zenon_H2f. % 206.24/206.66 apply (zenon_notallex_s (fun Re : zenon_U => (forall C : zenon_U, (forall C1 : zenon_U, (forall C2 : zenon_U, (forall Ta : zenon_U, (forall Tb : zenon_U, (forall Tc : zenon_U, (((organization zenon_TX_w Ta)/\((organization zenon_TY_v Ta)/\((organization zenon_TY_v Tc)/\((class zenon_TX_w C Ta)/\((class zenon_TY_v C Ta)/\((reorganization zenon_TX_w Ta Tb)/\((reorganization zenon_TY_v Ta Tc)/\((reorganization_type zenon_TX_w Re Ta)/\((reorganization_type zenon_TY_v Re Ta)/\((complexity zenon_TX_w C1 Ta)/\((complexity zenon_TY_v C2 Ta)/\(greater C2 C1))))))))))))->(greater Tc Tb))))))))) zenon_H2f); [ zenon_intro zenon_H30; idtac ]. % 206.24/206.66 elim zenon_H30. zenon_intro zenon_TRe_bx. zenon_intro zenon_H32. % 206.24/206.66 apply (zenon_notallex_s (fun C : zenon_U => (forall C1 : zenon_U, (forall C2 : zenon_U, (forall Ta : zenon_U, (forall Tb : zenon_U, (forall Tc : zenon_U, (((organization zenon_TX_w Ta)/\((organization zenon_TY_v Ta)/\((organization zenon_TY_v Tc)/\((class zenon_TX_w C Ta)/\((class zenon_TY_v C Ta)/\((reorganization zenon_TX_w Ta Tb)/\((reorganization zenon_TY_v Ta Tc)/\((reorganization_type zenon_TX_w zenon_TRe_bx Ta)/\((reorganization_type zenon_TY_v zenon_TRe_bx Ta)/\((complexity zenon_TX_w C1 Ta)/\((complexity zenon_TY_v C2 Ta)/\(greater C2 C1))))))))))))->(greater Tc Tb)))))))) zenon_H32); [ zenon_intro zenon_H33; idtac ]. % 206.24/206.66 elim zenon_H33. zenon_intro zenon_TC_u. zenon_intro zenon_H34. % 206.24/206.66 apply (zenon_notallex_s (fun C1 : zenon_U => (forall C2 : zenon_U, (forall Ta : zenon_U, (forall Tb : zenon_U, (forall Tc : zenon_U, (((organization zenon_TX_w Ta)/\((organization zenon_TY_v Ta)/\((organization zenon_TY_v Tc)/\((class zenon_TX_w zenon_TC_u Ta)/\((class zenon_TY_v zenon_TC_u Ta)/\((reorganization zenon_TX_w Ta Tb)/\((reorganization zenon_TY_v Ta Tc)/\((reorganization_type zenon_TX_w zenon_TRe_bx Ta)/\((reorganization_type zenon_TY_v zenon_TRe_bx Ta)/\((complexity zenon_TX_w C1 Ta)/\((complexity zenon_TY_v C2 Ta)/\(greater C2 C1))))))))))))->(greater Tc Tb))))))) zenon_H34); [ zenon_intro zenon_H35; idtac ]. % 206.24/206.66 elim zenon_H35. zenon_intro zenon_TC1_t. zenon_intro zenon_H36. % 206.24/206.66 apply (zenon_notallex_s (fun C2 : zenon_U => (forall Ta : zenon_U, (forall Tb : zenon_U, (forall Tc : zenon_U, (((organization zenon_TX_w Ta)/\((organization zenon_TY_v Ta)/\((organization zenon_TY_v Tc)/\((class zenon_TX_w zenon_TC_u Ta)/\((class zenon_TY_v zenon_TC_u Ta)/\((reorganization zenon_TX_w Ta Tb)/\((reorganization zenon_TY_v Ta Tc)/\((reorganization_type zenon_TX_w zenon_TRe_bx Ta)/\((reorganization_type zenon_TY_v zenon_TRe_bx Ta)/\((complexity zenon_TX_w zenon_TC1_t Ta)/\((complexity zenon_TY_v C2 Ta)/\(greater C2 zenon_TC1_t))))))))))))->(greater Tc Tb)))))) zenon_H36); [ zenon_intro zenon_H37; idtac ]. % 206.24/206.66 elim zenon_H37. zenon_intro zenon_TC2_s. zenon_intro zenon_H38. % 206.24/206.66 apply (zenon_notallex_s (fun Ta : zenon_U => (forall Tb : zenon_U, (forall Tc : zenon_U, (((organization zenon_TX_w Ta)/\((organization zenon_TY_v Ta)/\((organization zenon_TY_v Tc)/\((class zenon_TX_w zenon_TC_u Ta)/\((class zenon_TY_v zenon_TC_u Ta)/\((reorganization zenon_TX_w Ta Tb)/\((reorganization zenon_TY_v Ta Tc)/\((reorganization_type zenon_TX_w zenon_TRe_bx Ta)/\((reorganization_type zenon_TY_v zenon_TRe_bx Ta)/\((complexity zenon_TX_w zenon_TC1_t Ta)/\((complexity zenon_TY_v zenon_TC2_s Ta)/\(greater zenon_TC2_s zenon_TC1_t))))))))))))->(greater Tc Tb))))) zenon_H38); [ zenon_intro zenon_H39; idtac ]. % 206.24/206.66 elim zenon_H39. zenon_intro zenon_TTa_q. zenon_intro zenon_H3a. % 206.24/206.66 apply (zenon_notallex_s (fun Tb : zenon_U => (forall Tc : zenon_U, (((organization zenon_TX_w zenon_TTa_q)/\((organization zenon_TY_v zenon_TTa_q)/\((organization zenon_TY_v Tc)/\((class zenon_TX_w zenon_TC_u zenon_TTa_q)/\((class zenon_TY_v zenon_TC_u zenon_TTa_q)/\((reorganization zenon_TX_w zenon_TTa_q Tb)/\((reorganization zenon_TY_v zenon_TTa_q Tc)/\((reorganization_type zenon_TX_w zenon_TRe_bx zenon_TTa_q)/\((reorganization_type zenon_TY_v zenon_TRe_bx zenon_TTa_q)/\((complexity zenon_TX_w zenon_TC1_t zenon_TTa_q)/\((complexity zenon_TY_v zenon_TC2_s zenon_TTa_q)/\(greater zenon_TC2_s zenon_TC1_t))))))))))))->(greater Tc Tb)))) zenon_H3a); [ zenon_intro zenon_H3b; idtac ]. % 206.24/206.66 elim zenon_H3b. zenon_intro zenon_TTb_ci. zenon_intro zenon_H3d. % 206.24/206.66 apply (zenon_notallex_s (fun Tc : zenon_U => (((organization zenon_TX_w zenon_TTa_q)/\((organization zenon_TY_v zenon_TTa_q)/\((organization zenon_TY_v Tc)/\((class zenon_TX_w zenon_TC_u zenon_TTa_q)/\((class zenon_TY_v zenon_TC_u zenon_TTa_q)/\((reorganization zenon_TX_w zenon_TTa_q zenon_TTb_ci)/\((reorganization zenon_TY_v zenon_TTa_q Tc)/\((reorganization_type zenon_TX_w zenon_TRe_bx zenon_TTa_q)/\((reorganization_type zenon_TY_v zenon_TRe_bx zenon_TTa_q)/\((complexity zenon_TX_w zenon_TC1_t zenon_TTa_q)/\((complexity zenon_TY_v zenon_TC2_s zenon_TTa_q)/\(greater zenon_TC2_s zenon_TC1_t))))))))))))->(greater Tc zenon_TTb_ci))) zenon_H3d); [ zenon_intro zenon_H3e; idtac ]. % 206.24/206.66 elim zenon_H3e. zenon_intro zenon_TTc_cl. zenon_intro zenon_H40. % 206.24/206.66 apply (zenon_notimply_s _ _ zenon_H40). zenon_intro zenon_H42. zenon_intro zenon_H41. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H42). zenon_intro zenon_H5. zenon_intro zenon_H43. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H43). zenon_intro zenon_H6. zenon_intro zenon_H44. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H44). zenon_intro zenon_H46. zenon_intro zenon_H45. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H45). zenon_intro zenon_H7. zenon_intro zenon_H47. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H47). zenon_intro zenon_H8. zenon_intro zenon_H48. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H4a. zenon_intro zenon_H49. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H49). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H4b). zenon_intro zenon_H4e. zenon_intro zenon_H4d. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H9. zenon_intro zenon_H51. % 206.24/206.66 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_Ha. zenon_intro zenon_Hd. % 206.24/206.66 generalize (a13_FOL zenon_TX_w). zenon_intro zenon_H52. % 206.24/206.66 generalize (a12_FOL zenon_TX_w). zenon_intro zenon_H53. % 206.24/206.66 generalize (zenon_H52 zenon_TY_v). zenon_intro zenon_H54. % 206.24/206.66 generalize (zenon_H53 zenon_TY_v). zenon_intro zenon_H55. % 206.24/206.66 generalize (zenon_H55 zenon_TC_u). zenon_intro zenon_H56. % 206.24/206.66 generalize (zenon_H56 zenon_TC1_t). zenon_intro zenon_H57. % 206.24/206.66 generalize (zenon_H57 zenon_TC2_s). zenon_intro zenon_H58. % 206.24/206.66 generalize (zenon_H54 zenon_TRe_bx). zenon_intro zenon_H59. % 206.24/206.66 generalize (zenon_H59 zenon_TC_u). zenon_intro zenon_H5a. % 206.24/206.66 generalize (mp5 zenon_TX_w). zenon_intro zenon_H5b. % 206.24/206.66 generalize (mp5 zenon_TY_v). zenon_intro zenon_H5c. % 206.24/206.66 generalize (zenon_H5b zenon_TTa_q). zenon_intro zenon_H5d. % 206.24/206.66 apply (zenon_imply_s _ _ zenon_H5d); [ zenon_intro zenon_H1d | zenon_intro zenon_H5e ]. % 206.24/206.66 exact (zenon_H1d zenon_H5). % 206.24/206.66 elim zenon_H5e. zenon_intro zenon_TI_r. zenon_intro zenon_Hb. % 206.24/206.66 generalize (zenon_H5c zenon_TTa_q). zenon_intro zenon_H5f. % 206.24/206.66 apply (zenon_imply_s _ _ zenon_H5f); [ zenon_intro zenon_H1f | zenon_intro zenon_H60 ]. % 206.24/206.66 exact (zenon_H1f zenon_H6). % 206.24/206.66 elim zenon_H60. zenon_intro zenon_TI_p. zenon_intro zenon_Hc. % 206.24/206.66 generalize (zenon_H5a zenon_TI_r). zenon_intro zenon_H61. % 206.24/206.66 generalize (zenon_H58 zenon_TI_r). zenon_intro zenon_H4. % 206.24/206.66 generalize (zenon_H61 zenon_TI_p). zenon_intro zenon_H62. % 206.24/206.66 generalize (zenon_H62 zenon_TTa_q). zenon_intro zenon_H63. % 206.24/206.66 generalize (zenon_H63 zenon_TTb_ci). zenon_intro zenon_H64. % 206.24/206.66 generalize (zenon_H64 zenon_TTc_cl). zenon_intro zenon_H65. % 206.24/206.66 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H1d | zenon_intro zenon_H68 ]. % 206.24/206.66 exact (zenon_H1d zenon_H5). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H1f | zenon_intro zenon_H69 ]. % 206.24/206.66 exact (zenon_H1f zenon_H6). % 206.24/206.66 apply (zenon_notand_s _ _ zenon_H69); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 206.24/206.66 exact (zenon_H6b zenon_H46). % 0.14/206.73 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H21 | zenon_intro zenon_H6c ]. % 0.14/206.73 exact (zenon_H21 zenon_H7). % 0.14/206.73 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H23 | zenon_intro zenon_H6d ]. % 0.14/206.73 exact (zenon_H23 zenon_H8). % 0.14/206.73 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.14/206.73 exact (zenon_H6f zenon_H4a). % 0.14/206.73 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 0.14/206.73 exact (zenon_H71 zenon_H4c). % 0.14/206.73 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.14/206.73 exact (zenon_H73 zenon_H4e). % 0.14/206.73 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 0.14/206.73 exact (zenon_H75 zenon_H50). % 0.14/206.73 apply (zenon_notand_s _ _ zenon_H74); [ zenon_intro zenon_H29 | zenon_intro zenon_H76 ]. % 0.14/206.73 exact (zenon_H29 zenon_Hb). % 0.14/206.73 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H2b | zenon_intro zenon_He ]. % 0.14/206.73 exact (zenon_H2b zenon_Hc). % 0.14/206.73 apply (zenon_L1_ zenon_TI_p zenon_TTa_q zenon_TI_r zenon_TC2_s zenon_TC1_t zenon_TC_u zenon_TY_v zenon_TX_w); trivial. % 0.14/206.73 exact (zenon_H41 zenon_H66). % 0.14/206.73 Qed. % 0.14/206.73 % SZS output end Proof % 0.14/206.73 (* END-PROOF *) % 0.14/206.73 nodes searched: 220764 % 0.14/206.73 max branch formulas: 55282 % 0.14/206.73 proof nodes created: 15169 % 0.14/206.73 formulas created: 2921592 % 0.14/206.73 %------------------------------------------------------------------------------