%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT041+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n005.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 0.03s 0.44s % Output : Proof 0.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT041+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.10/0.35 % Computer : n005.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.03/0.35 % CPULimit : 300 % 0.03/0.35 % WCLimit : 300 % 0.03/0.35 % DateTime : Mon Sep 7 13:02:20 UTC 2026 % 0.03/0.36 % CPUTime : % 0.03/0.44 (* PROOF-FOUND *) % 0.03/0.44 % SZS status Theorem % 0.03/0.44 (* BEGIN-PROOF *) % 0.03/0.44 % SZS output start Proof % 0.03/0.44 Theorem prove_t10 : (exists X : zenon_U, (exists T : zenon_U, ((organisation_at_time X T)/\((~(first_mover X))/\(~(efficient_producer X)))))). % 0.03/0.44 Proof. % 0.03/0.44 assert (zenon_L1_ : forall (zenon_TT_j : zenon_U) (zenon_TX_k : zenon_U), (~(has_elaborated_routines zenon_TX_k zenon_TT_j)) -> (founding_time zenon_TX_k zenon_TT_j) -> (efficient_producer zenon_TX_k) -> (organisation_at_time zenon_TX_k zenon_TT_j) -> False). % 0.03/0.44 do 2 intro. intros zenon_H5 zenon_H6 zenon_H7 zenon_H8. % 0.03/0.44 generalize (a14 zenon_TX_k). zenon_intro zenon_Hb. % 0.03/0.44 generalize (zenon_Hb zenon_TT_j). zenon_intro zenon_Hc. % 0.03/0.44 apply (zenon_imply_s _ _ zenon_Hc); [ zenon_intro zenon_He | zenon_intro zenon_Hd ]. % 0.03/0.44 apply (zenon_notand_s _ _ zenon_He); [ zenon_intro zenon_H10 | zenon_intro zenon_Hf ]. % 0.03/0.44 exact (zenon_H10 zenon_H8). % 0.03/0.44 apply (zenon_notand_s _ _ zenon_Hf); [ zenon_intro zenon_H12 | zenon_intro zenon_H11 ]. % 0.03/0.44 exact (zenon_H12 zenon_H7). % 0.03/0.44 exact (zenon_H11 zenon_H6). % 0.03/0.44 exact (zenon_H5 zenon_Hd). % 0.03/0.44 (* end of lemma zenon_L1_ *) % 0.03/0.44 apply NNPP. intro zenon_G. % 0.03/0.44 elim a16. zenon_intro zenon_TX_k. zenon_intro zenon_H13. % 0.03/0.44 elim zenon_H13. zenon_intro zenon_TT_j. zenon_intro zenon_H14. % 0.03/0.44 apply (zenon_and_s _ _ zenon_H14). zenon_intro zenon_H8. zenon_intro zenon_H15. % 0.03/0.44 apply (zenon_and_s _ _ zenon_H15). zenon_intro zenon_H6. zenon_intro zenon_H16. % 0.03/0.44 apply (zenon_and_s _ _ zenon_H16). zenon_intro zenon_H17. zenon_intro zenon_H5. % 0.03/0.44 apply zenon_G. exists zenon_TX_k. apply NNPP. zenon_intro zenon_H18. % 0.03/0.44 apply zenon_H18. exists zenon_TT_j. apply NNPP. zenon_intro zenon_H19. % 0.03/0.44 apply (zenon_notand_s _ _ zenon_H19); [ zenon_intro zenon_H10 | zenon_intro zenon_H1a ]. % 0.03/0.44 exact (zenon_H10 zenon_H8). % 0.03/0.44 apply (zenon_notand_s _ _ zenon_H1a); [ zenon_intro zenon_H1c | zenon_intro zenon_H1b ]. % 0.03/0.44 apply zenon_H1c. zenon_intro zenon_H1d. % 0.03/0.44 generalize (mp_not_high_and_low zenon_TX_k). zenon_intro zenon_H1e. % 0.03/0.44 generalize (zenon_H1e zenon_TT_j). zenon_intro zenon_H1f. % 0.03/0.44 apply (zenon_notand_s _ _ zenon_H1f); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 0.03/0.44 generalize (a15 zenon_TX_k). zenon_intro zenon_H22. % 0.03/0.44 generalize (zenon_H22 zenon_TT_j). zenon_intro zenon_H23. % 0.03/0.44 apply (zenon_imply_s _ _ zenon_H23); [ zenon_intro zenon_H25 | zenon_intro zenon_H24 ]. % 0.03/0.44 apply (zenon_notand_s _ _ zenon_H25); [ zenon_intro zenon_H10 | zenon_intro zenon_H26 ]. % 0.03/0.44 exact (zenon_H10 zenon_H8). % 0.03/0.44 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H27 | zenon_intro zenon_H11 ]. % 0.03/0.44 exact (zenon_H27 zenon_H1d). % 0.03/0.44 exact (zenon_H11 zenon_H6). % 0.03/0.44 exact (zenon_H21 zenon_H24). % 0.03/0.44 exact (zenon_H20 zenon_H17). % 0.03/0.44 apply zenon_H1b. zenon_intro zenon_H7. % 0.03/0.44 apply (zenon_L1_ zenon_TT_j zenon_TX_k); trivial. % 0.03/0.44 Qed. % 0.03/0.44 % SZS output end Proof % 0.03/0.44 (* END-PROOF *) % 0.03/0.44 nodes searched: 70 % 0.03/0.44 max branch formulas: 54 % 0.03/0.44 proof nodes created: 32 % 0.03/0.44 formulas created: 417 % 0.03/0.44 %------------------------------------------------------------------------------