%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SET917+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n008.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 06:39:37 EDT 2022 % Result : Theorem 0.18s 0.50s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SET917+1 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.13/0.32 % Computer : n008.cluster.edu % 0.13/0.32 % Model : x86_64 x86_64 % 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.32 % Memory : 8042.1875MB % 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 600 % 0.13/0.32 % DateTime : Sun Jul 10 12:21:53 EDT 2022 % 0.13/0.32 % CPUTime : % 0.18/0.50 Zenon warning: unused variable (B : zenon_U) in idempotence_k3_xboole_0 % 0.18/0.50 (* PROOF-FOUND *) % 0.18/0.50 % SZS status Theorem % 0.18/0.50 (* BEGIN-PROOF *) % 0.18/0.50 % SZS output start Proof % 0.18/0.50 Theorem t58_zfmisc_1 : (forall A : zenon_U, (forall B : zenon_U, ((disjoint (singleton A) B)\/((set_intersection2 (singleton A) B) = (singleton A))))). % 0.18/0.50 Proof. % 0.18/0.50 apply NNPP. intro zenon_G. % 0.18/0.50 apply (zenon_notallex_s (fun A : zenon_U => (forall B : zenon_U, ((disjoint (singleton A) B)\/((set_intersection2 (singleton A) B) = (singleton A))))) zenon_G); [ zenon_intro zenon_H9; idtac ]. % 0.18/0.50 elim zenon_H9. zenon_intro zenon_TA_k. zenon_intro zenon_Hb. % 0.18/0.50 apply (zenon_notallex_s (fun B : zenon_U => ((disjoint (singleton zenon_TA_k) B)\/((set_intersection2 (singleton zenon_TA_k) B) = (singleton zenon_TA_k)))) zenon_Hb); [ zenon_intro zenon_Hc; idtac ]. % 0.18/0.50 elim zenon_Hc. zenon_intro zenon_TB_n. zenon_intro zenon_He. % 0.18/0.50 apply (zenon_notor_s _ _ zenon_He). zenon_intro zenon_H10. zenon_intro zenon_Hf. % 0.18/0.50 generalize (commutativity_k3_xboole_0 zenon_TB_n). zenon_intro zenon_H11. % 0.18/0.50 generalize (l32_zfmisc_1 zenon_TA_k). zenon_intro zenon_H12. % 0.18/0.50 generalize (zenon_H11 (singleton zenon_TA_k)). zenon_intro zenon_H13. % 0.18/0.50 generalize (l28_zfmisc_1 zenon_TA_k). zenon_intro zenon_H14. % 0.18/0.50 elim (classic ((singleton zenon_TA_k) = (singleton zenon_TA_k))); [ zenon_intro zenon_H15 | zenon_intro zenon_H16 ]. % 0.18/0.50 cut (((singleton zenon_TA_k) = (singleton zenon_TA_k)) = ((set_intersection2 (singleton zenon_TA_k) zenon_TB_n) = (singleton zenon_TA_k))). % 0.18/0.50 intro zenon_D_pnotp. % 0.18/0.50 apply zenon_Hf. % 0.18/0.50 rewrite <- zenon_D_pnotp. % 0.18/0.50 exact zenon_H15. % 0.18/0.50 cut (((singleton zenon_TA_k) = (singleton zenon_TA_k))); [idtac | apply NNPP; zenon_intro zenon_H16]. % 0.18/0.50 cut (((singleton zenon_TA_k) = (set_intersection2 (singleton zenon_TA_k) zenon_TB_n))); [idtac | apply NNPP; zenon_intro zenon_H17]. % 0.18/0.50 congruence. % 0.18/0.50 cut (((set_intersection2 zenon_TB_n (singleton zenon_TA_k)) = (set_intersection2 (singleton zenon_TA_k) zenon_TB_n)) = ((singleton zenon_TA_k) = (set_intersection2 (singleton zenon_TA_k) zenon_TB_n))). % 0.18/0.50 intro zenon_D_pnotp. % 0.18/0.50 apply zenon_H17. % 0.18/0.50 rewrite <- zenon_D_pnotp. % 0.18/0.50 exact zenon_H13. % 0.18/0.50 cut (((set_intersection2 (singleton zenon_TA_k) zenon_TB_n) = (set_intersection2 (singleton zenon_TA_k) zenon_TB_n))); [idtac | apply NNPP; zenon_intro zenon_H18]. % 0.18/0.50 cut (((set_intersection2 zenon_TB_n (singleton zenon_TA_k)) = (singleton zenon_TA_k))); [idtac | apply NNPP; zenon_intro zenon_H19]. % 0.18/0.50 congruence. % 0.18/0.50 elim (classic ((singleton zenon_TA_k) = (singleton zenon_TA_k))); [ zenon_intro zenon_H15 | zenon_intro zenon_H16 ]. % 0.18/0.50 cut (((singleton zenon_TA_k) = (singleton zenon_TA_k)) = ((set_intersection2 zenon_TB_n (singleton zenon_TA_k)) = (singleton zenon_TA_k))). % 0.18/0.50 intro zenon_D_pnotp. % 0.18/0.50 apply zenon_H19. % 0.18/0.50 rewrite <- zenon_D_pnotp. % 0.18/0.50 exact zenon_H15. % 0.18/0.50 cut (((singleton zenon_TA_k) = (singleton zenon_TA_k))); [idtac | apply NNPP; zenon_intro zenon_H16]. % 0.18/0.50 cut (((singleton zenon_TA_k) = (set_intersection2 zenon_TB_n (singleton zenon_TA_k)))); [idtac | apply NNPP; zenon_intro zenon_H1a]. % 0.18/0.50 congruence. % 0.18/0.50 generalize (zenon_H12 zenon_TB_n). zenon_intro zenon_H1b. % 0.18/0.50 apply (zenon_imply_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 0.18/0.50 generalize (zenon_H14 zenon_TB_n). zenon_intro zenon_H1e. % 0.18/0.50 apply (zenon_imply_s _ _ zenon_H1e); [ zenon_intro zenon_H20 | zenon_intro zenon_H1f ]. % 0.18/0.50 exact (zenon_H20 zenon_H1d). % 0.18/0.50 exact (zenon_H10 zenon_H1f). % 0.18/0.50 apply zenon_H1a. apply sym_equal. exact zenon_H1c. % 0.18/0.50 apply zenon_H16. apply refl_equal. % 0.18/0.50 apply zenon_H16. apply refl_equal. % 0.18/0.50 apply zenon_H18. apply refl_equal. % 0.18/0.50 apply zenon_H16. apply refl_equal. % 0.18/0.50 apply zenon_H16. apply refl_equal. % 0.18/0.50 Qed. % 0.18/0.50 % SZS output end Proof % 0.18/0.50 (* END-PROOF *) % 0.18/0.50 nodes searched: 1425 % 0.18/0.50 max branch formulas: 381 % 0.18/0.50 proof nodes created: 138 % 0.18/0.50 formulas created: 3984 % 0.18/0.50 %------------------------------------------------------------------------------