%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEU219+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 16:00:20 EDT 2022 % Result : Theorem 0.20s 0.54s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU219+1 : TPTP v8.1.0. Released v3.3.0. % 0.12/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n011.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jun 19 17:04:54 EDT 2022 % 0.12/0.34 % CPUTime : % 0.20/0.54 (* PROOF-FOUND *) % 0.20/0.54 % SZS status Theorem % 0.20/0.54 (* BEGIN-PROOF *) % 0.20/0.54 % SZS output start Proof % 0.20/0.54 Theorem t55_funct_1 : (forall A : zenon_U, (((relation A)/\(function A))->((one_to_one A)->(((relation_rng A) = (relation_dom (function_inverse A)))/\((relation_dom A) = (relation_rng (function_inverse A))))))). % 0.20/0.54 Proof. % 0.20/0.54 assert (zenon_L1_ : forall (zenon_TA_m : zenon_U), (relation zenon_TA_m) -> (~(relation (relation_inverse zenon_TA_m))) -> False). % 0.20/0.54 do 1 intro. intros zenon_Ha zenon_Hb. % 0.20/0.54 generalize (dt_k4_relat_1 zenon_TA_m). zenon_intro zenon_Hd. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_Hd); [ zenon_intro zenon_Hf | zenon_intro zenon_He ]. % 0.20/0.54 exact (zenon_Hf zenon_Ha). % 0.20/0.54 exact (zenon_Hb zenon_He). % 0.20/0.54 (* end of lemma zenon_L1_ *) % 0.20/0.54 assert (zenon_L2_ : forall (zenon_TA_m : zenon_U), (~((relation_rng (relation_inverse (relation_inverse zenon_TA_m))) = (relation_rng zenon_TA_m))) -> ((relation_inverse (relation_inverse zenon_TA_m)) = zenon_TA_m) -> False). % 0.20/0.54 do 1 intro. intros zenon_H10 zenon_H11. % 0.20/0.54 cut (((relation_inverse (relation_inverse zenon_TA_m)) = zenon_TA_m)); [idtac | apply NNPP; zenon_intro zenon_H12]. % 0.20/0.54 congruence. % 0.20/0.54 exact (zenon_H12 zenon_H11). % 0.20/0.54 (* end of lemma zenon_L2_ *) % 0.20/0.54 assert (zenon_L3_ : forall (zenon_TA_m : zenon_U), (~((relation_dom (relation_inverse (relation_inverse zenon_TA_m))) = (relation_dom zenon_TA_m))) -> ((relation_inverse (relation_inverse zenon_TA_m)) = zenon_TA_m) -> False). % 0.20/0.54 do 1 intro. intros zenon_H13 zenon_H11. % 0.20/0.54 cut (((relation_inverse (relation_inverse zenon_TA_m)) = zenon_TA_m)); [idtac | apply NNPP; zenon_intro zenon_H12]. % 0.20/0.54 congruence. % 0.20/0.54 exact (zenon_H12 zenon_H11). % 0.20/0.54 (* end of lemma zenon_L3_ *) % 0.20/0.54 apply NNPP. intro zenon_G. % 0.20/0.54 apply (zenon_notallex_s (fun A : zenon_U => (((relation A)/\(function A))->((one_to_one A)->(((relation_rng A) = (relation_dom (function_inverse A)))/\((relation_dom A) = (relation_rng (function_inverse A))))))) zenon_G); [ zenon_intro zenon_H14; idtac ]. % 0.20/0.54 elim zenon_H14. zenon_intro zenon_TA_m. zenon_intro zenon_H15. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H15). zenon_intro zenon_H17. zenon_intro zenon_H16. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H16). zenon_intro zenon_H19. zenon_intro zenon_H18. % 0.20/0.54 apply (zenon_and_s _ _ zenon_H17). zenon_intro zenon_Ha. zenon_intro zenon_H1a. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H18); [ zenon_intro zenon_H1c | zenon_intro zenon_H1b ]. % 0.20/0.54 generalize (involutiveness_k4_relat_1 zenon_TA_m). zenon_intro zenon_H1d. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H1d); [ zenon_intro zenon_Hf | zenon_intro zenon_H11 ]. % 0.20/0.54 exact (zenon_Hf zenon_Ha). % 0.20/0.54 generalize (t37_relat_1 (relation_inverse zenon_TA_m)). zenon_intro zenon_H1e. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H1e); [ zenon_intro zenon_Hb | zenon_intro zenon_H1f ]. % 0.20/0.54 apply (zenon_L1_ zenon_TA_m); trivial. % 0.20/0.54 apply (zenon_and_s _ _ zenon_H1f). zenon_intro zenon_H21. zenon_intro zenon_H20. % 0.20/0.54 generalize (d9_funct_1 zenon_TA_m). zenon_intro zenon_H22. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H22); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_Hf | zenon_intro zenon_H25 ]. % 0.20/0.54 exact (zenon_Hf zenon_Ha). % 0.20/0.54 exact (zenon_H25 zenon_H1a). % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H23); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 0.20/0.54 exact (zenon_H27 zenon_H19). % 0.20/0.54 elim (classic ((relation_dom (function_inverse zenon_TA_m)) = (relation_dom (function_inverse zenon_TA_m)))); [ zenon_intro zenon_H28 | zenon_intro zenon_H29 ]. % 0.20/0.54 cut (((relation_dom (function_inverse zenon_TA_m)) = (relation_dom (function_inverse zenon_TA_m))) = ((relation_rng zenon_TA_m) = (relation_dom (function_inverse zenon_TA_m)))). % 0.20/0.54 intro zenon_D_pnotp. % 0.20/0.54 apply zenon_H1c. % 0.20/0.54 rewrite <- zenon_D_pnotp. % 0.20/0.54 exact zenon_H28. % 0.20/0.54 cut (((relation_dom (function_inverse zenon_TA_m)) = (relation_dom (function_inverse zenon_TA_m)))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 0.20/0.54 cut (((relation_dom (function_inverse zenon_TA_m)) = (relation_rng zenon_TA_m))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 0.20/0.54 congruence. % 0.20/0.54 cut (((relation_dom (relation_inverse zenon_TA_m)) = (relation_rng (relation_inverse (relation_inverse zenon_TA_m)))) = ((relation_dom (function_inverse zenon_TA_m)) = (relation_rng zenon_TA_m))). % 0.20/0.54 intro zenon_D_pnotp. % 0.20/0.54 apply zenon_H2a. % 0.20/0.54 rewrite <- zenon_D_pnotp. % 0.20/0.54 exact zenon_H20. % 0.20/0.54 cut (((relation_rng (relation_inverse (relation_inverse zenon_TA_m))) = (relation_rng zenon_TA_m))); [idtac | apply NNPP; zenon_intro zenon_H10]. % 0.20/0.54 cut (((relation_dom (relation_inverse zenon_TA_m)) = (relation_dom (function_inverse zenon_TA_m)))); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 0.20/0.54 congruence. % 0.20/0.54 elim (classic ((relation_dom (function_inverse zenon_TA_m)) = (relation_dom (function_inverse zenon_TA_m)))); [ zenon_intro zenon_H28 | zenon_intro zenon_H29 ]. % 0.20/0.54 cut (((relation_dom (function_inverse zenon_TA_m)) = (relation_dom (function_inverse zenon_TA_m))) = ((relation_dom (relation_inverse zenon_TA_m)) = (relation_dom (function_inverse zenon_TA_m)))). % 0.20/0.54 intro zenon_D_pnotp. % 0.20/0.54 apply zenon_H2b. % 0.20/0.54 rewrite <- zenon_D_pnotp. % 0.20/0.54 exact zenon_H28. % 0.20/0.54 cut (((relation_dom (function_inverse zenon_TA_m)) = (relation_dom (function_inverse zenon_TA_m)))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 0.20/0.54 cut (((relation_dom (function_inverse zenon_TA_m)) = (relation_dom (relation_inverse zenon_TA_m)))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 0.20/0.54 congruence. % 0.20/0.54 cut (((function_inverse zenon_TA_m) = (relation_inverse zenon_TA_m))); [idtac | apply NNPP; zenon_intro zenon_H2d]. % 0.20/0.54 congruence. % 0.20/0.54 exact (zenon_H2d zenon_H26). % 0.20/0.54 apply zenon_H29. apply refl_equal. % 0.20/0.54 apply zenon_H29. apply refl_equal. % 0.20/0.54 apply (zenon_L2_ zenon_TA_m); trivial. % 0.20/0.54 apply zenon_H29. apply refl_equal. % 0.20/0.54 apply zenon_H29. apply refl_equal. % 0.20/0.54 generalize (involutiveness_k4_relat_1 zenon_TA_m). zenon_intro zenon_H1d. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H1d); [ zenon_intro zenon_Hf | zenon_intro zenon_H11 ]. % 0.20/0.54 exact (zenon_Hf zenon_Ha). % 0.20/0.54 generalize (t37_relat_1 (relation_inverse zenon_TA_m)). zenon_intro zenon_H1e. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H1e); [ zenon_intro zenon_Hb | zenon_intro zenon_H1f ]. % 0.20/0.54 apply (zenon_L1_ zenon_TA_m); trivial. % 0.20/0.54 apply (zenon_and_s _ _ zenon_H1f). zenon_intro zenon_H21. zenon_intro zenon_H20. % 0.20/0.54 generalize (d9_funct_1 zenon_TA_m). zenon_intro zenon_H22. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H22); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H24); [ zenon_intro zenon_Hf | zenon_intro zenon_H25 ]. % 0.20/0.54 exact (zenon_Hf zenon_Ha). % 0.20/0.54 exact (zenon_H25 zenon_H1a). % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H23); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 0.20/0.54 exact (zenon_H27 zenon_H19). % 0.20/0.54 elim (classic ((relation_rng (function_inverse zenon_TA_m)) = (relation_rng (function_inverse zenon_TA_m)))); [ zenon_intro zenon_H2e | zenon_intro zenon_H2f ]. % 0.20/0.54 cut (((relation_rng (function_inverse zenon_TA_m)) = (relation_rng (function_inverse zenon_TA_m))) = ((relation_dom zenon_TA_m) = (relation_rng (function_inverse zenon_TA_m)))). % 0.20/0.54 intro zenon_D_pnotp. % 0.20/0.54 apply zenon_H1b. % 0.20/0.54 rewrite <- zenon_D_pnotp. % 0.20/0.54 exact zenon_H2e. % 0.20/0.54 cut (((relation_rng (function_inverse zenon_TA_m)) = (relation_rng (function_inverse zenon_TA_m)))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 0.20/0.54 cut (((relation_rng (function_inverse zenon_TA_m)) = (relation_dom zenon_TA_m))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 0.20/0.54 congruence. % 0.20/0.54 cut (((relation_rng (relation_inverse zenon_TA_m)) = (relation_dom (relation_inverse (relation_inverse zenon_TA_m)))) = ((relation_rng (function_inverse zenon_TA_m)) = (relation_dom zenon_TA_m))). % 0.20/0.54 intro zenon_D_pnotp. % 0.20/0.54 apply zenon_H30. % 0.20/0.54 rewrite <- zenon_D_pnotp. % 0.20/0.54 exact zenon_H21. % 0.20/0.54 cut (((relation_dom (relation_inverse (relation_inverse zenon_TA_m))) = (relation_dom zenon_TA_m))); [idtac | apply NNPP; zenon_intro zenon_H13]. % 0.20/0.54 cut (((relation_rng (relation_inverse zenon_TA_m)) = (relation_rng (function_inverse zenon_TA_m)))); [idtac | apply NNPP; zenon_intro zenon_H31]. % 0.20/0.54 congruence. % 0.20/0.54 elim (classic ((relation_rng (function_inverse zenon_TA_m)) = (relation_rng (function_inverse zenon_TA_m)))); [ zenon_intro zenon_H2e | zenon_intro zenon_H2f ]. % 0.20/0.54 cut (((relation_rng (function_inverse zenon_TA_m)) = (relation_rng (function_inverse zenon_TA_m))) = ((relation_rng (relation_inverse zenon_TA_m)) = (relation_rng (function_inverse zenon_TA_m)))). % 0.20/0.54 intro zenon_D_pnotp. % 0.20/0.54 apply zenon_H31. % 0.20/0.54 rewrite <- zenon_D_pnotp. % 0.20/0.54 exact zenon_H2e. % 0.20/0.54 cut (((relation_rng (function_inverse zenon_TA_m)) = (relation_rng (function_inverse zenon_TA_m)))); [idtac | apply NNPP; zenon_intro zenon_H2f]. % 0.20/0.54 cut (((relation_rng (function_inverse zenon_TA_m)) = (relation_rng (relation_inverse zenon_TA_m)))); [idtac | apply NNPP; zenon_intro zenon_H32]. % 0.20/0.54 congruence. % 0.20/0.54 cut (((function_inverse zenon_TA_m) = (relation_inverse zenon_TA_m))); [idtac | apply NNPP; zenon_intro zenon_H2d]. % 0.20/0.54 congruence. % 0.20/0.54 exact (zenon_H2d zenon_H26). % 0.20/0.54 apply zenon_H2f. apply refl_equal. % 0.20/0.54 apply zenon_H2f. apply refl_equal. % 0.20/0.54 apply (zenon_L3_ zenon_TA_m); trivial. % 0.20/0.54 apply zenon_H2f. apply refl_equal. % 0.20/0.54 apply zenon_H2f. apply refl_equal. % 0.20/0.54 Qed. % 0.20/0.54 % SZS output end Proof % 0.20/0.54 (* END-PROOF *) % 0.20/0.54 nodes searched: 432 % 0.20/0.54 max branch formulas: 142 % 0.20/0.54 proof nodes created: 76 % 0.20/0.54 formulas created: 1674 % 0.20/0.54 %------------------------------------------------------------------------------