%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEU326+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n021.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:01:14 EDT 2022 % Result : Theorem 0.77s 0.97s % Output : Proof 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEU326+1 : TPTP v8.1.0. Released v3.3.0. % 0.11/0.13 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % 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 19:04:18 EDT 2022 % 0.12/0.34 % CPUTime : % 0.77/0.97 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 0.77/0.97 (* PROOF-FOUND *) % 0.77/0.97 % SZS status Theorem % 0.77/0.97 (* BEGIN-PROOF *) % 0.77/0.97 % SZS output start Proof % 0.77/0.97 Theorem t10_tops_2 : (forall A : zenon_U, (forall B : zenon_U, ((element B (powerset (powerset A)))->((~((~(B = (empty_set)))/\((complements_of_subsets A B) = (empty_set))))/\(~((~((complements_of_subsets A B) = (empty_set)))/\(B = (empty_set)))))))). % 0.77/0.97 Proof. % 0.77/0.97 assert (zenon_L1_ : forall (zenon_TB_bn : zenon_U) (zenon_TA_bo : zenon_U), (forall B : zenon_U, ((element B (powerset (powerset zenon_TA_bo)))->(element (complements_of_subsets zenon_TA_bo B) (powerset (powerset zenon_TA_bo))))) -> (element zenon_TB_bn (powerset (powerset zenon_TA_bo))) -> (~(element (complements_of_subsets zenon_TA_bo zenon_TB_bn) (powerset (powerset zenon_TA_bo)))) -> False). % 0.77/0.97 do 2 intro. intros zenon_H24 zenon_H25 zenon_H26. % 0.77/0.97 generalize (zenon_H24 zenon_TB_bn). zenon_intro zenon_H29. % 0.77/0.97 apply (zenon_imply_s _ _ zenon_H29); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 0.77/0.97 exact (zenon_H2b zenon_H25). % 0.77/0.97 exact (zenon_H26 zenon_H2a). % 0.77/0.97 (* end of lemma zenon_L1_ *) % 0.77/0.97 assert (zenon_L2_ : forall (zenon_TA_bo : zenon_U) (zenon_TB_bn : zenon_U), (zenon_TB_bn = (empty_set)) -> ((complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)) = zenon_TB_bn) -> (~((empty_set) = (complements_of_subsets zenon_TA_bo zenon_TB_bn))) -> (element zenon_TB_bn (powerset (powerset zenon_TA_bo))) -> (forall B : zenon_U, ((element B (powerset (powerset zenon_TA_bo)))->(element (complements_of_subsets zenon_TA_bo B) (powerset (powerset zenon_TA_bo))))) -> False). % 0.77/0.97 do 2 intro. intros zenon_H2c zenon_H2d zenon_H2e zenon_H25 zenon_H24. % 0.77/0.97 generalize (t46_setfam_1 zenon_TA_bo). zenon_intro zenon_H2f. % 0.77/0.97 generalize (zenon_H2f (complements_of_subsets zenon_TA_bo zenon_TB_bn)). zenon_intro zenon_H30. % 0.77/0.97 apply (zenon_imply_s _ _ zenon_H30); [ zenon_intro zenon_H26 | zenon_intro zenon_H31 ]. % 0.77/0.97 apply (zenon_L1_ zenon_TB_bn zenon_TA_bo); trivial. % 0.77/0.97 apply (zenon_notand_s _ _ zenon_H31); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 0.77/0.97 apply zenon_H33. zenon_intro zenon_H34. % 0.77/0.97 apply zenon_H2e. apply sym_equal. exact zenon_H34. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)) = zenon_TB_bn) = ((complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)) = (empty_set))). % 0.77/0.97 intro zenon_D_pnotp. % 0.77/0.97 apply zenon_H32. % 0.77/0.97 rewrite <- zenon_D_pnotp. % 0.77/0.97 exact zenon_H2d. % 0.77/0.97 cut ((zenon_TB_bn = (empty_set))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)) = (complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)))); [idtac | apply NNPP; zenon_intro zenon_H36]. % 0.77/0.97 congruence. % 0.77/0.97 apply zenon_H36. apply refl_equal. % 0.77/0.97 exact (zenon_H35 zenon_H2c). % 0.77/0.97 (* end of lemma zenon_L2_ *) % 0.77/0.97 assert (zenon_L3_ : (~((empty_set) = (empty_set))) -> False). % 0.77/0.97 do 0 intro. intros zenon_H37. % 0.77/0.97 apply zenon_H37. apply refl_equal. % 0.77/0.97 (* end of lemma zenon_L3_ *) % 0.77/0.97 apply NNPP. intro zenon_G. % 0.77/0.97 apply (zenon_notallex_s (fun A : zenon_U => (forall B : zenon_U, ((element B (powerset (powerset A)))->((~((~(B = (empty_set)))/\((complements_of_subsets A B) = (empty_set))))/\(~((~((complements_of_subsets A B) = (empty_set)))/\(B = (empty_set)))))))) zenon_G); [ zenon_intro zenon_H38; idtac ]. % 0.77/0.97 elim zenon_H38. zenon_intro zenon_TA_bo. zenon_intro zenon_H39. % 0.77/0.97 apply (zenon_notallex_s (fun B : zenon_U => ((element B (powerset (powerset zenon_TA_bo)))->((~((~(B = (empty_set)))/\((complements_of_subsets zenon_TA_bo B) = (empty_set))))/\(~((~((complements_of_subsets zenon_TA_bo B) = (empty_set)))/\(B = (empty_set))))))) zenon_H39); [ zenon_intro zenon_H3a; idtac ]. % 0.77/0.97 elim zenon_H3a. zenon_intro zenon_TB_ch. zenon_intro zenon_H3c. % 0.77/0.97 apply (zenon_notimply_s _ _ zenon_H3c). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 0.77/0.97 apply (zenon_notand_s _ _ zenon_H3d); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 0.77/0.97 apply zenon_H40. zenon_intro zenon_H41. % 0.77/0.97 apply (zenon_and_s _ _ zenon_H41). zenon_intro zenon_H43. zenon_intro zenon_H42. % 0.77/0.97 generalize (t46_setfam_1 zenon_TA_bo). zenon_intro zenon_H2f. % 0.77/0.97 generalize (zenon_H2f zenon_TB_ch). zenon_intro zenon_H44. % 0.77/0.97 apply (zenon_imply_s _ _ zenon_H44); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 0.77/0.97 exact (zenon_H46 zenon_H3e). % 0.77/0.97 apply (zenon_notand_s _ _ zenon_H45); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 0.77/0.97 exact (zenon_H48 zenon_H43). % 0.77/0.97 exact (zenon_H47 zenon_H42). % 0.77/0.97 apply zenon_H3f. zenon_intro zenon_H49. % 0.77/0.97 apply (zenon_and_s _ _ zenon_H49). zenon_intro zenon_H47. zenon_intro zenon_H4a. % 0.77/0.97 generalize (involutiveness_k7_setfam_1 zenon_TA_bo). zenon_intro zenon_H4b. % 0.77/0.97 generalize (dt_k7_setfam_1 zenon_TA_bo). zenon_intro zenon_H24. % 0.77/0.97 generalize (rc2_subset_1 (powerset zenon_TA_bo)). zenon_intro zenon_H4c. % 0.77/0.97 elim zenon_H4c. zenon_intro zenon_TB_bn. zenon_intro zenon_H4d. % 0.77/0.97 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H25. zenon_intro zenon_H4e. % 0.77/0.97 generalize (t6_boole zenon_TB_bn). zenon_intro zenon_H4f. % 0.77/0.97 apply (zenon_imply_s _ _ zenon_H4f); [ zenon_intro zenon_H50 | zenon_intro zenon_H2c ]. % 0.77/0.97 exact (zenon_H50 zenon_H4e). % 0.77/0.97 cut ((zenon_TB_bn = (empty_set)) = ((complements_of_subsets zenon_TA_bo zenon_TB_ch) = (empty_set))). % 0.77/0.97 intro zenon_D_pnotp. % 0.77/0.97 apply zenon_H47. % 0.77/0.97 rewrite <- zenon_D_pnotp. % 0.77/0.97 exact zenon_H2c. % 0.77/0.97 cut (((empty_set) = (empty_set))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 0.77/0.97 cut ((zenon_TB_bn = (complements_of_subsets zenon_TA_bo zenon_TB_ch))); [idtac | apply NNPP; zenon_intro zenon_H51]. % 0.77/0.97 congruence. % 0.77/0.97 elim (classic ((complements_of_subsets zenon_TA_bo zenon_TB_ch) = (complements_of_subsets zenon_TA_bo zenon_TB_ch))); [ zenon_intro zenon_H52 | zenon_intro zenon_H53 ]. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo zenon_TB_ch) = (complements_of_subsets zenon_TA_bo zenon_TB_ch)) = (zenon_TB_bn = (complements_of_subsets zenon_TA_bo zenon_TB_ch))). % 0.77/0.97 intro zenon_D_pnotp. % 0.77/0.97 apply zenon_H51. % 0.77/0.97 rewrite <- zenon_D_pnotp. % 0.77/0.97 exact zenon_H52. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo zenon_TB_ch) = (complements_of_subsets zenon_TA_bo zenon_TB_ch))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo zenon_TB_ch) = zenon_TB_bn)); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.77/0.97 congruence. % 0.77/0.97 generalize (zenon_H4b zenon_TB_bn). zenon_intro zenon_H55. % 0.77/0.97 apply (zenon_imply_s _ _ zenon_H55); [ zenon_intro zenon_H2b | zenon_intro zenon_H2d ]. % 0.77/0.97 exact (zenon_H2b zenon_H25). % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)) = zenon_TB_bn) = ((complements_of_subsets zenon_TA_bo zenon_TB_ch) = zenon_TB_bn)). % 0.77/0.97 intro zenon_D_pnotp. % 0.77/0.97 apply zenon_H54. % 0.77/0.97 rewrite <- zenon_D_pnotp. % 0.77/0.97 exact zenon_H2d. % 0.77/0.97 cut ((zenon_TB_bn = zenon_TB_bn)); [idtac | apply NNPP; zenon_intro zenon_H56]. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)) = (complements_of_subsets zenon_TA_bo zenon_TB_ch))); [idtac | apply NNPP; zenon_intro zenon_H57]. % 0.77/0.97 congruence. % 0.77/0.97 elim (classic ((complements_of_subsets zenon_TA_bo zenon_TB_ch) = (complements_of_subsets zenon_TA_bo zenon_TB_ch))); [ zenon_intro zenon_H52 | zenon_intro zenon_H53 ]. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo zenon_TB_ch) = (complements_of_subsets zenon_TA_bo zenon_TB_ch)) = ((complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)) = (complements_of_subsets zenon_TA_bo zenon_TB_ch))). % 0.77/0.97 intro zenon_D_pnotp. % 0.77/0.97 apply zenon_H57. % 0.77/0.97 rewrite <- zenon_D_pnotp. % 0.77/0.97 exact zenon_H52. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo zenon_TB_ch) = (complements_of_subsets zenon_TA_bo zenon_TB_ch))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.77/0.97 cut (((complements_of_subsets zenon_TA_bo zenon_TB_ch) = (complements_of_subsets zenon_TA_bo (complements_of_subsets zenon_TA_bo zenon_TB_bn)))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 0.77/0.97 congruence. % 0.77/0.97 cut ((zenon_TB_ch = (complements_of_subsets zenon_TA_bo zenon_TB_bn))); [idtac | apply NNPP; zenon_intro zenon_H59]. % 0.77/0.97 cut ((zenon_TA_bo = zenon_TA_bo)); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 0.77/0.97 congruence. % 0.77/0.97 apply zenon_H5a. apply refl_equal. % 0.77/0.97 cut ((zenon_TB_ch = (empty_set)) = (zenon_TB_ch = (complements_of_subsets zenon_TA_bo zenon_TB_bn))). % 0.77/0.97 intro zenon_D_pnotp. % 0.77/0.97 apply zenon_H59. % 0.77/0.97 rewrite <- zenon_D_pnotp. % 0.77/0.97 exact zenon_H4a. % 0.77/0.97 cut (((empty_set) = (complements_of_subsets zenon_TA_bo zenon_TB_bn))); [idtac | apply NNPP; zenon_intro zenon_H2e]. % 0.77/0.97 cut ((zenon_TB_ch = zenon_TB_ch)); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 0.77/0.97 congruence. % 0.77/0.97 apply zenon_H5b. apply refl_equal. % 0.77/0.97 apply (zenon_L2_ zenon_TA_bo zenon_TB_bn); trivial. % 0.77/0.97 apply zenon_H53. apply refl_equal. % 0.77/0.97 apply zenon_H53. apply refl_equal. % 0.77/0.97 apply zenon_H56. apply refl_equal. % 0.77/0.97 apply zenon_H53. apply refl_equal. % 0.77/0.97 apply zenon_H53. apply refl_equal. % 0.77/0.97 apply zenon_H37. apply refl_equal. % 0.77/0.97 Qed. % 0.77/0.97 % SZS output end Proof % 0.77/0.97 (* END-PROOF *) % 0.77/0.97 nodes searched: 18291 % 0.77/0.97 max branch formulas: 2181 % 0.77/0.97 proof nodes created: 1250 % 0.77/0.97 formulas created: 33003 % 0.77/0.97 %------------------------------------------------------------------------------