%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEU080+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n007.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 15:59:17 EDT 2022 % Result : Theorem 0.19s 0.52s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SEU080+1 : TPTP v8.1.0. Released v3.2.0. % 0.12/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n007.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 20 01:42:30 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.52 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 0.19/0.52 (* PROOF-FOUND *) % 0.19/0.52 % SZS status Theorem % 0.19/0.52 (* BEGIN-PROOF *) % 0.19/0.52 % SZS output start Proof % 0.19/0.52 Theorem t161_funct_1 : (forall A : zenon_U, (forall B : zenon_U, (forall C : zenon_U, (((relation C)/\(function C))->((((relation_inverse_image C A) = (relation_inverse_image C B))/\((subset A (relation_rng C))/\(subset B (relation_rng C))))->(A = B)))))). % 0.19/0.52 Proof. % 0.19/0.52 assert (zenon_L1_ : forall (zenon_TA_bm : zenon_U) (zenon_TB_bn : zenon_U), (forall B : zenon_U, ((zenon_TB_bn = B)<->((subset zenon_TB_bn B)/\(subset B zenon_TB_bn)))) -> (subset zenon_TA_bm zenon_TB_bn) -> (subset zenon_TB_bn zenon_TA_bm) -> (~(zenon_TA_bm = zenon_TB_bn)) -> False). % 0.19/0.52 do 2 intro. intros zenon_H22 zenon_H23 zenon_H24 zenon_H25. % 0.19/0.52 generalize (zenon_H22 zenon_TA_bm). zenon_intro zenon_H28. % 0.19/0.52 apply (zenon_equiv_s _ _ zenon_H28); [ zenon_intro zenon_H2c; zenon_intro zenon_H2b | zenon_intro zenon_H2a; zenon_intro zenon_H29 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H2b); [ zenon_intro zenon_H2e | zenon_intro zenon_H2d ]. % 0.19/0.52 exact (zenon_H2e zenon_H24). % 0.19/0.52 exact (zenon_H2d zenon_H23). % 0.19/0.52 apply zenon_H25. apply sym_equal. exact zenon_H2a. % 0.19/0.52 (* end of lemma zenon_L1_ *) % 0.19/0.52 assert (zenon_L2_ : forall (zenon_TA_bm : zenon_U) (zenon_TC_cb : zenon_U) (zenon_TB_bn : zenon_U), (forall x : zenon_U, (subset x x)) -> (forall B : zenon_U, (forall C : zenon_U, (((relation C)/\(function C))->(((subset (relation_inverse_image C zenon_TB_bn) (relation_inverse_image C B))/\(subset zenon_TB_bn (relation_rng C)))->(subset zenon_TB_bn B))))) -> (relation zenon_TC_cb) -> (function zenon_TC_cb) -> ((relation_inverse_image zenon_TC_cb zenon_TA_bm) = (relation_inverse_image zenon_TC_cb zenon_TB_bn)) -> (subset zenon_TB_bn (relation_rng zenon_TC_cb)) -> (subset zenon_TA_bm zenon_TB_bn) -> (~(zenon_TA_bm = zenon_TB_bn)) -> False). % 0.19/0.52 do 3 intro. intros zenon_H2f zenon_H30 zenon_H31 zenon_H32 zenon_H33 zenon_H34 zenon_H23 zenon_H25. % 0.19/0.52 generalize (zenon_H30 zenon_TA_bm). zenon_intro zenon_H36. % 0.19/0.52 generalize (d10_xboole_0 zenon_TB_bn). zenon_intro zenon_H22. % 0.19/0.52 generalize (zenon_H36 zenon_TC_cb). zenon_intro zenon_H37. % 0.19/0.52 apply (zenon_imply_s _ _ zenon_H37); [ zenon_intro zenon_H39 | zenon_intro zenon_H38 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H39); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 0.19/0.52 exact (zenon_H3b zenon_H31). % 0.19/0.52 exact (zenon_H3a zenon_H32). % 0.19/0.52 apply (zenon_imply_s _ _ zenon_H38); [ zenon_intro zenon_H3c | zenon_intro zenon_H24 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 0.19/0.52 generalize (zenon_H2f (relation_inverse_image zenon_TC_cb zenon_TB_bn)). zenon_intro zenon_H3f. % 0.19/0.52 cut ((subset (relation_inverse_image zenon_TC_cb zenon_TB_bn) (relation_inverse_image zenon_TC_cb zenon_TB_bn)) = (subset (relation_inverse_image zenon_TC_cb zenon_TB_bn) (relation_inverse_image zenon_TC_cb zenon_TA_bm))). % 0.19/0.52 intro zenon_D_pnotp. % 0.19/0.52 apply zenon_H3e. % 0.19/0.52 rewrite <- zenon_D_pnotp. % 0.19/0.52 exact zenon_H3f. % 0.19/0.52 cut (((relation_inverse_image zenon_TC_cb zenon_TB_bn) = (relation_inverse_image zenon_TC_cb zenon_TA_bm))); [idtac | apply NNPP; zenon_intro zenon_H40]. % 0.19/0.52 cut (((relation_inverse_image zenon_TC_cb zenon_TB_bn) = (relation_inverse_image zenon_TC_cb zenon_TB_bn))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 0.19/0.52 congruence. % 0.19/0.52 apply zenon_H41. apply refl_equal. % 0.19/0.52 apply zenon_H40. apply sym_equal. exact zenon_H33. % 0.19/0.52 exact (zenon_H3d zenon_H34). % 0.19/0.52 apply (zenon_L1_ zenon_TA_bm zenon_TB_bn); trivial. % 0.19/0.52 (* end of lemma zenon_L2_ *) % 0.19/0.52 apply NNPP. intro zenon_G. % 0.19/0.52 elim (classic (forall x : zenon_U, (subset x x))); [ zenon_intro zenon_H2f | zenon_intro zenon_H42 ]. % 0.19/0.52 apply (zenon_notallex_s (fun A : zenon_U => (forall B : zenon_U, (forall C : zenon_U, (((relation C)/\(function C))->((((relation_inverse_image C A) = (relation_inverse_image C B))/\((subset A (relation_rng C))/\(subset B (relation_rng C))))->(A = B)))))) zenon_G); [ zenon_intro zenon_H43; idtac ]. % 0.19/0.52 elim zenon_H43. zenon_intro zenon_TA_bm. zenon_intro zenon_H44. % 0.19/0.52 apply (zenon_notallex_s (fun B : zenon_U => (forall C : zenon_U, (((relation C)/\(function C))->((((relation_inverse_image C zenon_TA_bm) = (relation_inverse_image C B))/\((subset zenon_TA_bm (relation_rng C))/\(subset B (relation_rng C))))->(zenon_TA_bm = B))))) zenon_H44); [ zenon_intro zenon_H45; idtac ]. % 0.19/0.52 elim zenon_H45. zenon_intro zenon_TB_bn. zenon_intro zenon_H46. % 0.19/0.52 apply (zenon_notallex_s (fun C : zenon_U => (((relation C)/\(function C))->((((relation_inverse_image C zenon_TA_bm) = (relation_inverse_image C zenon_TB_bn))/\((subset zenon_TA_bm (relation_rng C))/\(subset zenon_TB_bn (relation_rng C))))->(zenon_TA_bm = zenon_TB_bn)))) zenon_H46); [ zenon_intro zenon_H47; idtac ]. % 0.19/0.52 elim zenon_H47. zenon_intro zenon_TC_cb. zenon_intro zenon_H48. % 0.19/0.52 apply (zenon_notimply_s _ _ zenon_H48). zenon_intro zenon_H4a. zenon_intro zenon_H49. % 0.19/0.52 apply (zenon_notimply_s _ _ zenon_H49). zenon_intro zenon_H4b. zenon_intro zenon_H25. % 0.19/0.52 apply (zenon_and_s _ _ zenon_H4b). zenon_intro zenon_H33. zenon_intro zenon_H4c. % 0.19/0.52 apply (zenon_and_s _ _ zenon_H4c). zenon_intro zenon_H4d. zenon_intro zenon_H34. % 0.19/0.52 apply (zenon_and_s _ _ zenon_H4a). zenon_intro zenon_H31. zenon_intro zenon_H32. % 0.19/0.52 generalize (t158_funct_1 zenon_TB_bn). zenon_intro zenon_H30. % 0.19/0.52 generalize (t158_funct_1 zenon_TA_bm). zenon_intro zenon_H4e. % 0.19/0.52 generalize (zenon_H4e zenon_TB_bn). zenon_intro zenon_H4f. % 0.19/0.52 generalize (zenon_H4f zenon_TC_cb). zenon_intro zenon_H50. % 0.19/0.52 apply (zenon_imply_s _ _ zenon_H50); [ zenon_intro zenon_H39 | zenon_intro zenon_H51 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H39); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 0.19/0.52 exact (zenon_H3b zenon_H31). % 0.19/0.52 exact (zenon_H3a zenon_H32). % 0.19/0.52 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H52 | zenon_intro zenon_H23 ]. % 0.19/0.52 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 0.19/0.52 generalize (zenon_H2f (relation_inverse_image zenon_TC_cb zenon_TA_bm)). zenon_intro zenon_H55. % 0.19/0.52 cut ((subset (relation_inverse_image zenon_TC_cb zenon_TA_bm) (relation_inverse_image zenon_TC_cb zenon_TA_bm)) = (subset (relation_inverse_image zenon_TC_cb zenon_TA_bm) (relation_inverse_image zenon_TC_cb zenon_TB_bn))). % 0.19/0.52 intro zenon_D_pnotp. % 0.19/0.52 apply zenon_H54. % 0.19/0.52 rewrite <- zenon_D_pnotp. % 0.19/0.52 exact zenon_H55. % 0.19/0.52 cut (((relation_inverse_image zenon_TC_cb zenon_TA_bm) = (relation_inverse_image zenon_TC_cb zenon_TB_bn))); [idtac | apply NNPP; zenon_intro zenon_H56]. % 0.19/0.52 cut (((relation_inverse_image zenon_TC_cb zenon_TA_bm) = (relation_inverse_image zenon_TC_cb zenon_TA_bm))); [idtac | apply NNPP; zenon_intro zenon_H57]. % 0.19/0.52 congruence. % 0.19/0.52 apply zenon_H57. apply refl_equal. % 0.19/0.52 exact (zenon_H56 zenon_H33). % 0.19/0.52 exact (zenon_H53 zenon_H4d). % 0.19/0.52 apply (zenon_L2_ zenon_TA_bm zenon_TC_cb zenon_TB_bn); trivial. % 0.19/0.52 apply zenon_H42. zenon_intro zenon_Tx_dk. apply NNPP. zenon_intro zenon_H59. % 0.19/0.52 generalize (reflexivity_r1_tarski zenon_Tx_dk). zenon_intro zenon_H0. % 0.19/0.52 generalize (zenon_H0 zenon_E). zenon_intro zenon_H5a. % 0.19/0.52 exact (zenon_H59 zenon_H5a). % 0.19/0.52 Qed. % 0.19/0.52 % SZS output end Proof % 0.19/0.52 (* END-PROOF *) % 0.19/0.52 nodes searched: 408 % 0.19/0.52 max branch formulas: 251 % 0.19/0.52 proof nodes created: 45 % 0.19/0.52 formulas created: 2111 % 0.19/0.52 %------------------------------------------------------------------------------