%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LAT346+1 : TPTP v8.1.0. Released v3.4.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 : Sun Jul 17 07:23:52 EDT 2022 % Result : Theorem 9.26s 9.45s % Output : Proof 9.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : LAT346+1 : TPTP v8.1.0. Released v3.4.0. % 0.12/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n007.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 : Thu Jun 30 10:08:38 EDT 2022 % 0.12/0.34 % CPUTime : % 9.26/9.45 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 9.26/9.45 (* PROOF-FOUND *) % 9.26/9.45 % SZS status Theorem % 9.26/9.45 (* BEGIN-PROOF *) % 9.26/9.45 % SZS output start Proof % 9.26/9.45 Theorem t22_conlat_2 : (forall A : zenon_U, (((~(v3_conlat_1 A))/\(l2_conlat_1 A))->(r1_filter_1 (k11_conlat_1 (k7_conlat_2 A)) (k1_lattice2 (k11_conlat_1 A))))). % 9.26/9.45 Proof. % 9.26/9.45 assert (zenon_L1_ : forall (zenon_TA_ds : zenon_U), (~(v3_conlat_1 zenon_TA_ds)) -> (l2_conlat_1 zenon_TA_ds) -> (~(l3_lattices (k11_conlat_1 zenon_TA_ds))) -> False). % 9.26/9.45 do 1 intro. intros zenon_H5d zenon_H5e zenon_H5f. % 9.26/9.45 generalize (dt_k11_conlat_1 zenon_TA_ds). zenon_intro zenon_H61. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 9.26/9.45 exact (zenon_H65 zenon_H5d). % 9.26/9.45 exact (zenon_H64 zenon_H5e). % 9.26/9.45 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H67. zenon_intro zenon_H66. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H66). zenon_intro zenon_H69. zenon_intro zenon_H68. % 9.26/9.45 exact (zenon_H5f zenon_H68). % 9.26/9.45 (* end of lemma zenon_L1_ *) % 9.26/9.45 assert (zenon_L2_ : forall (zenon_TA_ds : zenon_U), (~(v3_conlat_1 zenon_TA_ds)) -> (l2_conlat_1 zenon_TA_ds) -> (~(l3_lattices (k1_lattice2 (k11_conlat_1 zenon_TA_ds)))) -> False). % 9.26/9.45 do 1 intro. intros zenon_H5d zenon_H5e zenon_H6a. % 9.26/9.45 generalize (dt_k1_lattice2 (k11_conlat_1 zenon_TA_ds)). zenon_intro zenon_H6b. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_H5f | zenon_intro zenon_H6c ]. % 9.26/9.45 apply (zenon_L1_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 9.26/9.45 exact (zenon_H6a zenon_H6d). % 9.26/9.45 (* end of lemma zenon_L2_ *) % 9.26/9.45 assert (zenon_L3_ : forall (zenon_TA_ds : zenon_U), (~(v3_conlat_1 zenon_TA_ds)) -> (l2_conlat_1 zenon_TA_ds) -> (v3_conlat_1 (k7_conlat_2 zenon_TA_ds)) -> False). % 9.26/9.45 do 1 intro. intros zenon_H5d zenon_H5e zenon_H6f. % 9.26/9.45 generalize (dt_k7_conlat_2 zenon_TA_ds). zenon_intro zenon_H70. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H63 | zenon_intro zenon_H71 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 9.26/9.45 exact (zenon_H65 zenon_H5d). % 9.26/9.45 exact (zenon_H64 zenon_H5e). % 9.26/9.45 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H73. zenon_intro zenon_H72. % 9.26/9.45 exact (zenon_H73 zenon_H6f). % 9.26/9.45 (* end of lemma zenon_L3_ *) % 9.26/9.45 assert (zenon_L4_ : forall (zenon_TA_ds : zenon_U), (~(v3_conlat_1 zenon_TA_ds)) -> (l2_conlat_1 zenon_TA_ds) -> (~(l2_conlat_1 (k7_conlat_2 zenon_TA_ds))) -> False). % 9.26/9.45 do 1 intro. intros zenon_H5d zenon_H5e zenon_H74. % 9.26/9.45 generalize (dt_k7_conlat_2 zenon_TA_ds). zenon_intro zenon_H70. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H63 | zenon_intro zenon_H71 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 9.26/9.45 exact (zenon_H65 zenon_H5d). % 9.26/9.45 exact (zenon_H64 zenon_H5e). % 9.26/9.45 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H73. zenon_intro zenon_H72. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H72). zenon_intro zenon_H76. zenon_intro zenon_H75. % 9.26/9.45 exact (zenon_H74 zenon_H75). % 9.26/9.45 (* end of lemma zenon_L4_ *) % 9.26/9.45 apply NNPP. intro zenon_G. % 9.26/9.45 apply (zenon_notallex_s (fun A : zenon_U => (((~(v3_conlat_1 A))/\(l2_conlat_1 A))->(r1_filter_1 (k11_conlat_1 (k7_conlat_2 A)) (k1_lattice2 (k11_conlat_1 A))))) zenon_G); [ zenon_intro zenon_H77; idtac ]. % 9.26/9.45 elim zenon_H77. zenon_intro zenon_TA_ds. zenon_intro zenon_H78. % 9.26/9.45 apply (zenon_notimply_s _ _ zenon_H78). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H7a). zenon_intro zenon_H5d. zenon_intro zenon_H5e. % 9.26/9.45 generalize (fc2_conlat_2 (k11_conlat_1 zenon_TA_ds)). zenon_intro zenon_H7b. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H7d | zenon_intro zenon_H7c ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H7d); [ zenon_intro zenon_H7f | zenon_intro zenon_H7e ]. % 9.26/9.45 apply zenon_H7f. zenon_intro zenon_H80. % 9.26/9.45 generalize (dt_k11_conlat_1 zenon_TA_ds). zenon_intro zenon_H61. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 9.26/9.45 exact (zenon_H65 zenon_H5d). % 9.26/9.45 exact (zenon_H64 zenon_H5e). % 9.26/9.45 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H67. zenon_intro zenon_H66. % 9.26/9.45 exact (zenon_H67 zenon_H80). % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H82 | zenon_intro zenon_H81 ]. % 9.26/9.45 generalize (fc1_conlat_2 zenon_TA_ds). zenon_intro zenon_H83. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H63 | zenon_intro zenon_H84 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 9.26/9.45 exact (zenon_H65 zenon_H5d). % 9.26/9.45 exact (zenon_H64 zenon_H5e). % 9.26/9.45 apply (zenon_and_s _ _ zenon_H84). zenon_intro zenon_H67. zenon_intro zenon_H85. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H85). zenon_intro zenon_H69. zenon_intro zenon_H86. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H88. zenon_intro zenon_H87. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H87). zenon_intro zenon_H8a. zenon_intro zenon_H89. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H89). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H8e. zenon_intro zenon_H8d. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H8d). zenon_intro zenon_H90. zenon_intro zenon_H8f. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H8f). zenon_intro zenon_H92. zenon_intro zenon_H91. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H94. zenon_intro zenon_H93. % 9.26/9.45 exact (zenon_H82 zenon_H94). % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H81); [ zenon_intro zenon_H95 | zenon_intro zenon_H5f ]. % 9.26/9.45 generalize (fc1_conlat_2 zenon_TA_ds). zenon_intro zenon_H83. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H63 | zenon_intro zenon_H84 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 9.26/9.45 exact (zenon_H65 zenon_H5d). % 9.26/9.45 exact (zenon_H64 zenon_H5e). % 9.26/9.45 apply (zenon_and_s _ _ zenon_H84). zenon_intro zenon_H67. zenon_intro zenon_H85. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H85). zenon_intro zenon_H69. zenon_intro zenon_H86. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H88. zenon_intro zenon_H87. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H87). zenon_intro zenon_H8a. zenon_intro zenon_H89. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H89). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H8e. zenon_intro zenon_H8d. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H8d). zenon_intro zenon_H90. zenon_intro zenon_H8f. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H8f). zenon_intro zenon_H92. zenon_intro zenon_H91. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H94. zenon_intro zenon_H93. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H93). zenon_intro zenon_H97. zenon_intro zenon_H96. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H96). zenon_intro zenon_H99. zenon_intro zenon_H98. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H98). zenon_intro zenon_H9b. zenon_intro zenon_H9a. % 9.26/9.45 exact (zenon_H95 zenon_H9a). % 9.26/9.45 apply (zenon_L1_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H7c). zenon_intro zenon_H9d. zenon_intro zenon_H9c. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H9c). zenon_intro zenon_H6e. zenon_intro zenon_H9e. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H9e). zenon_intro zenon_Ha0. zenon_intro zenon_H9f. % 9.26/9.45 apply (zenon_and_s _ _ zenon_H9f). zenon_intro zenon_Ha2. zenon_intro zenon_Ha1. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Ha1). zenon_intro zenon_Ha4. zenon_intro zenon_Ha3. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Ha3). zenon_intro zenon_Ha6. zenon_intro zenon_Ha5. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Ha5). zenon_intro zenon_Ha8. zenon_intro zenon_Ha7. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Ha7). zenon_intro zenon_Haa. zenon_intro zenon_Ha9. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Ha9). zenon_intro zenon_Hac. zenon_intro zenon_Hab. % 9.26/9.45 generalize (symmetry_r1_filter_1 (k1_lattice2 (k11_conlat_1 zenon_TA_ds))). zenon_intro zenon_Had. % 9.26/9.45 generalize (zenon_Had (k11_conlat_1 (k7_conlat_2 zenon_TA_ds))). zenon_intro zenon_Hae. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Hae); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haf ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb1 ]. % 9.26/9.45 exact (zenon_Hb2 zenon_H9d). % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hb1); [ zenon_intro zenon_Hb4 | zenon_intro zenon_Hb3 ]. % 9.26/9.45 exact (zenon_Hb4 zenon_Hac). % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hb3); [ zenon_intro zenon_H6a | zenon_intro zenon_Hb5 ]. % 9.26/9.45 apply (zenon_L2_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 9.26/9.45 apply zenon_Hb7. zenon_intro zenon_Hb8. % 9.26/9.45 generalize (dt_k11_conlat_1 (k7_conlat_2 zenon_TA_ds)). zenon_intro zenon_Hb9. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_Hbc | zenon_intro zenon_H74 ]. % 9.26/9.45 apply zenon_Hbc. zenon_intro zenon_H6f. % 9.26/9.45 apply (zenon_L3_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_L4_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_Hbe. zenon_intro zenon_Hbd. % 9.26/9.45 exact (zenon_Hbe zenon_Hb8). % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Hbf ]. % 9.26/9.45 generalize (fc1_conlat_2 (k7_conlat_2 zenon_TA_ds)). zenon_intro zenon_Hc1. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hc2 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_Hbc | zenon_intro zenon_H74 ]. % 9.26/9.45 apply zenon_Hbc. zenon_intro zenon_H6f. % 9.26/9.45 apply (zenon_L3_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_L4_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc2). zenon_intro zenon_Hbe. zenon_intro zenon_Hc3. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc3). zenon_intro zenon_Hc5. zenon_intro zenon_Hc4. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc4). zenon_intro zenon_Hc7. zenon_intro zenon_Hc6. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc6). zenon_intro zenon_Hc9. zenon_intro zenon_Hc8. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc8). zenon_intro zenon_Hcb. zenon_intro zenon_Hca. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hca). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hcc). zenon_intro zenon_Hcf. zenon_intro zenon_Hce. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hce). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hd0). zenon_intro zenon_Hd3. zenon_intro zenon_Hd2. % 9.26/9.45 exact (zenon_Hc0 zenon_Hd3). % 9.26/9.45 generalize (dt_k11_conlat_1 (k7_conlat_2 zenon_TA_ds)). zenon_intro zenon_Hb9. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_Hbc | zenon_intro zenon_H74 ]. % 9.26/9.45 apply zenon_Hbc. zenon_intro zenon_H6f. % 9.26/9.45 apply (zenon_L3_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_L4_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_Hbe. zenon_intro zenon_Hbd. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hbd). zenon_intro zenon_Hc5. zenon_intro zenon_Hd4. % 9.26/9.45 exact (zenon_Hbf zenon_Hd4). % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Haf); [ zenon_intro zenon_Hd6 | zenon_intro zenon_Hd5 ]. % 9.26/9.45 generalize (dt_k11_conlat_1 (k7_conlat_2 zenon_TA_ds)). zenon_intro zenon_Hb9. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_Hbc | zenon_intro zenon_H74 ]. % 9.26/9.45 apply zenon_Hbc. zenon_intro zenon_H6f. % 9.26/9.45 apply (zenon_L3_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_L4_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_Hbe. zenon_intro zenon_Hbd. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hbd). zenon_intro zenon_Hc5. zenon_intro zenon_Hd4. % 9.26/9.45 generalize (fc1_conlat_2 (k7_conlat_2 zenon_TA_ds)). zenon_intro zenon_Hc1. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hc2 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_Hbc | zenon_intro zenon_H74 ]. % 9.26/9.45 apply zenon_Hbc. zenon_intro zenon_H6f. % 9.26/9.45 apply (zenon_L3_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_L4_ zenon_TA_ds); trivial. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc2). zenon_intro zenon_Hbe. zenon_intro zenon_Hc3. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc3). zenon_intro zenon_Hc5. zenon_intro zenon_Hc4. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc4). zenon_intro zenon_Hc7. zenon_intro zenon_Hc6. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc6). zenon_intro zenon_Hc9. zenon_intro zenon_Hc8. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hc8). zenon_intro zenon_Hcb. zenon_intro zenon_Hca. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hca). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hcc). zenon_intro zenon_Hcf. zenon_intro zenon_Hce. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hce). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 9.26/9.45 apply (zenon_and_s _ _ zenon_Hd0). zenon_intro zenon_Hd3. zenon_intro zenon_Hd2. % 9.26/9.45 generalize (d5_lattice4 (k1_lattice2 (k11_conlat_1 zenon_TA_ds))). zenon_intro zenon_Hd7. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Hd7); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hd8 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hd9); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hda ]. % 9.26/9.45 exact (zenon_Hb2 zenon_H9d). % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hda); [ zenon_intro zenon_Hb4 | zenon_intro zenon_H6a ]. % 9.26/9.45 exact (zenon_Hb4 zenon_Hac). % 9.26/9.45 apply (zenon_L2_ zenon_TA_ds); trivial. % 9.26/9.45 generalize (zenon_Hd8 (k11_conlat_1 (k7_conlat_2 zenon_TA_ds))). zenon_intro zenon_Hdb. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_Hdb); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hdc ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 9.26/9.45 exact (zenon_Hb7 zenon_Hbe). % 9.26/9.45 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Hbf ]. % 9.26/9.45 exact (zenon_Hc0 zenon_Hd3). % 9.26/9.45 exact (zenon_Hbf zenon_Hd4). % 9.26/9.45 apply (zenon_equiv_s _ _ zenon_Hdc); [ zenon_intro zenon_Hd6; zenon_intro zenon_Hdf | zenon_intro zenon_Hde; zenon_intro zenon_Hdd ]. % 9.26/9.45 generalize (t21_conlat_2 zenon_TA_ds). zenon_intro zenon_He0. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_He0); [ zenon_intro zenon_H63 | zenon_intro zenon_He1 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 9.26/9.45 exact (zenon_H65 zenon_H5d). % 9.26/9.45 exact (zenon_H64 zenon_H5e). % 9.26/9.45 apply zenon_Hdf. exists (k10_conlat_2 zenon_TA_ds). apply NNPP. zenon_intro zenon_He2. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_He2); [ zenon_intro zenon_He4 | zenon_intro zenon_He3 ]. % 9.26/9.45 generalize (dt_k10_conlat_2 zenon_TA_ds). zenon_intro zenon_He5. % 9.26/9.45 apply (zenon_imply_s _ _ zenon_He5); [ zenon_intro zenon_H63 | zenon_intro zenon_He6 ]. % 9.26/9.45 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 9.26/9.45 exact (zenon_H65 zenon_H5d). % 9.26/9.45 exact (zenon_H64 zenon_H5e). % 9.26/9.45 exact (zenon_He4 zenon_He6). % 9.26/9.45 exact (zenon_He3 zenon_He1). % 9.26/9.45 exact (zenon_Hd6 zenon_Hde). % 9.26/9.45 exact (zenon_H79 zenon_Hd5). % 9.26/9.45 Qed. % 9.26/9.45 % SZS output end Proof % 9.26/9.45 (* END-PROOF *) % 9.26/9.45 nodes searched: 44712 % 9.26/9.45 max branch formulas: 6203 % 9.26/9.45 proof nodes created: 545 % 9.26/9.45 formulas created: 556933 % 9.26/9.45 %------------------------------------------------------------------------------