%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LAT356+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n013.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:24:03 EDT 2022 % Result : Theorem 0.38s 0.59s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : LAT356+1 : TPTP v8.1.0. Released v3.4.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n013.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.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 30 09:29:29 EDT 2022 % 0.12/0.33 % CPUTime : % 0.38/0.59 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 0.38/0.59 (* PROOF-FOUND *) % 0.38/0.59 % SZS status Theorem % 0.38/0.59 (* BEGIN-PROOF *) % 0.38/0.59 % SZS output start Proof % 0.38/0.59 Theorem t7_waybel34 : (forall A : zenon_U, (((v2_orders_2 A)/\((v3_orders_2 A)/\((v4_orders_2 A)/\((v1_lattice3 A)/\((v2_lattice3 A)/\((v3_lattice3 A)/\(l1_orders_2 A)))))))->(((k1_waybel34 A A (k7_grcat_1 A)) = (k7_grcat_1 A))/\((k2_waybel34 A A (k7_grcat_1 A)) = (k7_grcat_1 A))))). % 0.38/0.59 Proof. % 0.38/0.59 assert (zenon_L1_ : forall (zenon_TA_er : zenon_U), (l1_orders_2 zenon_TA_er) -> (~(v1_funct_1 (k7_grcat_1 zenon_TA_er))) -> False). % 0.38/0.59 do 1 intro. intros zenon_H77 zenon_H78. % 0.38/0.59 generalize (fc2_waybel_1 zenon_TA_er). zenon_intro zenon_H7a. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_H7a); [ zenon_intro zenon_H7c | zenon_intro zenon_H7b ]. % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 apply (zenon_and_s _ _ zenon_H7b). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 0.38/0.59 apply (zenon_and_s _ _ zenon_H7d). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 0.38/0.59 exact (zenon_H78 zenon_H80). % 0.38/0.59 (* end of lemma zenon_L1_ *) % 0.38/0.59 assert (zenon_L2_ : forall (zenon_TA_er : zenon_U), (l1_orders_2 zenon_TA_er) -> (~(l1_struct_0 zenon_TA_er)) -> False). % 0.38/0.59 do 1 intro. intros zenon_H77 zenon_H81. % 0.38/0.59 generalize (dt_l1_orders_2 zenon_TA_er). zenon_intro zenon_H82. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H7c | zenon_intro zenon_H83 ]. % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 exact (zenon_H81 zenon_H83). % 0.38/0.59 (* end of lemma zenon_L2_ *) % 0.38/0.59 assert (zenon_L3_ : forall (zenon_TA_er : zenon_U), (l1_orders_2 zenon_TA_er) -> (~(v1_funct_2 (k7_grcat_1 zenon_TA_er) (u1_struct_0 zenon_TA_er) (u1_struct_0 zenon_TA_er))) -> False). % 0.38/0.59 do 1 intro. intros zenon_H77 zenon_H84. % 0.38/0.59 generalize (fc3_waybel10 zenon_TA_er). zenon_intro zenon_H85. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_H85); [ zenon_intro zenon_H81 | zenon_intro zenon_H86 ]. % 0.38/0.59 apply (zenon_L2_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H7e. zenon_intro zenon_H87. % 0.38/0.59 apply (zenon_and_s _ _ zenon_H87). zenon_intro zenon_H80. zenon_intro zenon_H88. % 0.38/0.59 apply (zenon_and_s _ _ zenon_H88). zenon_intro zenon_H8a. zenon_intro zenon_H89. % 0.38/0.59 exact (zenon_H84 zenon_H89). % 0.38/0.59 (* end of lemma zenon_L3_ *) % 0.38/0.59 assert (zenon_L4_ : forall (zenon_TA_er : zenon_U), (l1_orders_2 zenon_TA_er) -> (~(m2_relset_1 (k7_grcat_1 zenon_TA_er) (u1_struct_0 zenon_TA_er) (u1_struct_0 zenon_TA_er))) -> False). % 0.38/0.59 do 1 intro. intros zenon_H77 zenon_H8b. % 0.38/0.59 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TA_er)). zenon_intro zenon_H8c. % 0.38/0.59 generalize (zenon_H8c (u1_struct_0 zenon_TA_er)). zenon_intro zenon_H8d. % 0.38/0.59 generalize (zenon_H8d (k7_grcat_1 zenon_TA_er)). zenon_intro zenon_H8e. % 0.38/0.59 apply (zenon_equiv_s _ _ zenon_H8e); [ zenon_intro zenon_H8b; zenon_intro zenon_H91 | zenon_intro zenon_H90; zenon_intro zenon_H8f ]. % 0.38/0.59 generalize (dt_k7_grcat_1 zenon_TA_er). zenon_intro zenon_H92. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_H92); [ zenon_intro zenon_H81 | zenon_intro zenon_H93 ]. % 0.38/0.59 apply (zenon_L2_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_and_s _ _ zenon_H93). zenon_intro zenon_H80. zenon_intro zenon_H94. % 0.38/0.59 apply (zenon_and_s _ _ zenon_H94). zenon_intro zenon_H89. zenon_intro zenon_H90. % 0.38/0.59 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TA_er)). zenon_intro zenon_H8c. % 0.38/0.59 generalize (zenon_H8c (u1_struct_0 zenon_TA_er)). zenon_intro zenon_H8d. % 0.38/0.59 generalize (zenon_H8d (k7_grcat_1 zenon_TA_er)). zenon_intro zenon_H8e. % 0.38/0.59 apply (zenon_equiv_s _ _ zenon_H8e); [ zenon_intro zenon_H8b; zenon_intro zenon_H91 | zenon_intro zenon_H90; zenon_intro zenon_H8f ]. % 0.38/0.59 exact (zenon_H8b zenon_H90). % 0.38/0.59 exact (zenon_H91 zenon_H8f). % 0.38/0.59 exact (zenon_H8b zenon_H90). % 0.38/0.59 (* end of lemma zenon_L4_ *) % 0.38/0.59 assert (zenon_L5_ : forall (zenon_TA_er : zenon_U), (l1_orders_2 zenon_TA_er) -> (v1_lattice3 zenon_TA_er) -> (v3_struct_0 zenon_TA_er) -> False). % 0.38/0.59 do 1 intro. intros zenon_H77 zenon_H95 zenon_H96. % 0.38/0.59 generalize (cc1_lattice3 zenon_TA_er). zenon_intro zenon_H97. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_H97); [ zenon_intro zenon_H7c | zenon_intro zenon_H98 ]. % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 apply (zenon_imply_s _ _ zenon_H98); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 0.38/0.59 exact (zenon_H9a zenon_H95). % 0.38/0.59 exact (zenon_H99 zenon_H96). % 0.38/0.59 (* end of lemma zenon_L5_ *) % 0.38/0.59 apply NNPP. intro zenon_G. % 0.38/0.59 apply (zenon_notallex_s (fun A : zenon_U => (((v2_orders_2 A)/\((v3_orders_2 A)/\((v4_orders_2 A)/\((v1_lattice3 A)/\((v2_lattice3 A)/\((v3_lattice3 A)/\(l1_orders_2 A)))))))->(((k1_waybel34 A A (k7_grcat_1 A)) = (k7_grcat_1 A))/\((k2_waybel34 A A (k7_grcat_1 A)) = (k7_grcat_1 A))))) zenon_G); [ zenon_intro zenon_H9b; idtac ]. % 0.38/0.59 elim zenon_H9b. zenon_intro zenon_TA_er. zenon_intro zenon_H9c. % 0.38/0.59 apply (zenon_notimply_s _ _ zenon_H9c). zenon_intro zenon_H9e. zenon_intro zenon_H9d. % 0.38/0.59 apply (zenon_and_s _ _ zenon_H9e). zenon_intro zenon_Ha0. zenon_intro zenon_H9f. % 0.38/0.59 apply (zenon_and_s _ _ zenon_H9f). zenon_intro zenon_Ha2. zenon_intro zenon_Ha1. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Ha1). zenon_intro zenon_Ha4. zenon_intro zenon_Ha3. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Ha3). zenon_intro zenon_H95. zenon_intro zenon_Ha5. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Ha5). zenon_intro zenon_Ha7. zenon_intro zenon_Ha6. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Ha6). zenon_intro zenon_Ha8. zenon_intro zenon_H77. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_H9d); [ zenon_intro zenon_Haa | zenon_intro zenon_Ha9 ]. % 0.38/0.59 generalize (d1_waybel34 zenon_TA_er). zenon_intro zenon_Hab. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hab); [ zenon_intro zenon_Had | zenon_intro zenon_Hac ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.38/0.59 exact (zenon_Haf zenon_Ha0). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.38/0.59 exact (zenon_Hb1 zenon_Ha2). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.38/0.59 exact (zenon_Hb3 zenon_Ha4). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_H9a | zenon_intro zenon_Hb4 ]. % 0.38/0.59 exact (zenon_H9a zenon_H95). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H7c ]. % 0.38/0.59 exact (zenon_Hb5 zenon_Ha7). % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 generalize (zenon_Hac zenon_TA_er). zenon_intro zenon_Hb6. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hb6); [ zenon_intro zenon_Had | zenon_intro zenon_Hb7 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.38/0.59 exact (zenon_Haf zenon_Ha0). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.38/0.59 exact (zenon_Hb1 zenon_Ha2). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.38/0.59 exact (zenon_Hb3 zenon_Ha4). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_H9a | zenon_intro zenon_Hb4 ]. % 0.38/0.59 exact (zenon_H9a zenon_H95). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H7c ]. % 0.38/0.59 exact (zenon_Hb5 zenon_Ha7). % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 generalize (zenon_Hb7 (k7_grcat_1 zenon_TA_er)). zenon_intro zenon_Hb8. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hb8); [ zenon_intro zenon_Hba | zenon_intro zenon_Hb9 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_H78 | zenon_intro zenon_Hbb ]. % 0.38/0.59 apply (zenon_L1_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_H84 | zenon_intro zenon_H8b ]. % 0.38/0.59 apply (zenon_L3_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_L4_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hb9); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbc ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hbd); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbe ]. % 0.38/0.59 exact (zenon_Hbf zenon_Ha8). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hc0 ]. % 0.38/0.59 exact (zenon_Hbf zenon_Ha8). % 0.38/0.59 generalize (fc4_waybel10 zenon_TA_er). zenon_intro zenon_Hc1. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc2 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hc3); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 0.38/0.59 apply zenon_Hc5. zenon_intro zenon_H96. % 0.38/0.59 apply (zenon_L5_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hc4); [ zenon_intro zenon_Haf | zenon_intro zenon_H7c ]. % 0.38/0.59 exact (zenon_Haf zenon_Ha0). % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc2). zenon_intro zenon_H7e. zenon_intro zenon_Hc6. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc6). zenon_intro zenon_H80. zenon_intro zenon_Hc7. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_H8a. zenon_intro zenon_Hc8. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc8). zenon_intro zenon_Hca. zenon_intro zenon_Hc9. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_H89. zenon_intro zenon_Hcb. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hcb). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hcc). zenon_intro zenon_Hcf. zenon_intro zenon_Hce. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hce). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hd0). zenon_intro zenon_Hd3. zenon_intro zenon_Hd2. % 0.38/0.59 exact (zenon_Hc0 zenon_Hd3). % 0.38/0.59 generalize (t6_waybel34 zenon_TA_er). zenon_intro zenon_Hd4. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hd4); [ zenon_intro zenon_Hd6 | zenon_intro zenon_Hd5 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hd6); [ zenon_intro zenon_Hc5 | zenon_intro zenon_H7c ]. % 0.38/0.59 apply zenon_Hc5. zenon_intro zenon_H96. % 0.38/0.59 apply (zenon_L5_ zenon_TA_er); trivial. % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 generalize (zenon_Hbc (k7_grcat_1 zenon_TA_er)). zenon_intro zenon_Hd7. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hd7); [ zenon_intro zenon_Hba | zenon_intro zenon_Hd8 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_H78 | zenon_intro zenon_Hbb ]. % 0.38/0.59 apply (zenon_L1_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_H84 | zenon_intro zenon_H8b ]. % 0.38/0.59 apply (zenon_L3_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_L4_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_equiv_s _ _ zenon_Hd8); [ zenon_intro zenon_Hdb; zenon_intro zenon_Hda | zenon_intro zenon_Hd9; zenon_intro zenon_Hd5 ]. % 0.38/0.59 exact (zenon_Hda zenon_Hd5). % 0.38/0.59 apply zenon_Haa. apply sym_equal. exact zenon_Hd9. % 0.38/0.59 generalize (d2_waybel34 zenon_TA_er). zenon_intro zenon_Hdc. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hdc); [ zenon_intro zenon_Had | zenon_intro zenon_Hdd ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.38/0.59 exact (zenon_Haf zenon_Ha0). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.38/0.59 exact (zenon_Hb1 zenon_Ha2). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.38/0.59 exact (zenon_Hb3 zenon_Ha4). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_H9a | zenon_intro zenon_Hb4 ]. % 0.38/0.59 exact (zenon_H9a zenon_H95). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H7c ]. % 0.38/0.59 exact (zenon_Hb5 zenon_Ha7). % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 generalize (zenon_Hdd zenon_TA_er). zenon_intro zenon_Hde. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hde); [ zenon_intro zenon_Had | zenon_intro zenon_Hdf ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 0.38/0.59 exact (zenon_Haf zenon_Ha0). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 0.38/0.59 exact (zenon_Hb1 zenon_Ha2). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 0.38/0.59 exact (zenon_Hb3 zenon_Ha4). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_H9a | zenon_intro zenon_Hb4 ]. % 0.38/0.59 exact (zenon_H9a zenon_H95). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H7c ]. % 0.38/0.59 exact (zenon_Hb5 zenon_Ha7). % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 generalize (zenon_Hdf (k7_grcat_1 zenon_TA_er)). zenon_intro zenon_He0. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_He0); [ zenon_intro zenon_Hba | zenon_intro zenon_He1 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_H78 | zenon_intro zenon_Hbb ]. % 0.38/0.59 apply (zenon_L1_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_H84 | zenon_intro zenon_H8b ]. % 0.38/0.59 apply (zenon_L3_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_L4_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_He1); [ zenon_intro zenon_He3 | zenon_intro zenon_He2 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_He3); [ zenon_intro zenon_Hbf | zenon_intro zenon_He4 ]. % 0.38/0.59 exact (zenon_Hbf zenon_Ha8). % 0.38/0.59 apply (zenon_notand_s _ _ zenon_He4); [ zenon_intro zenon_Hbf | zenon_intro zenon_He5 ]. % 0.38/0.59 exact (zenon_Hbf zenon_Ha8). % 0.38/0.59 generalize (fc4_waybel10 zenon_TA_er). zenon_intro zenon_Hc1. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc2 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hc3); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 0.38/0.59 apply zenon_Hc5. zenon_intro zenon_H96. % 0.38/0.59 apply (zenon_L5_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hc4); [ zenon_intro zenon_Haf | zenon_intro zenon_H7c ]. % 0.38/0.59 exact (zenon_Haf zenon_Ha0). % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc2). zenon_intro zenon_H7e. zenon_intro zenon_Hc6. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc6). zenon_intro zenon_H80. zenon_intro zenon_Hc7. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_H8a. zenon_intro zenon_Hc8. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc8). zenon_intro zenon_Hca. zenon_intro zenon_Hc9. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_H89. zenon_intro zenon_Hcb. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hcb). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hcc). zenon_intro zenon_Hcf. zenon_intro zenon_Hce. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hce). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hd0). zenon_intro zenon_Hd3. zenon_intro zenon_Hd2. % 0.38/0.59 apply (zenon_and_s _ _ zenon_Hd2). zenon_intro zenon_He7. zenon_intro zenon_He6. % 0.38/0.59 exact (zenon_He5 zenon_He7). % 0.38/0.59 generalize (t6_waybel34 zenon_TA_er). zenon_intro zenon_Hd4. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_Hd4); [ zenon_intro zenon_Hd6 | zenon_intro zenon_Hd5 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hd6); [ zenon_intro zenon_Hc5 | zenon_intro zenon_H7c ]. % 0.38/0.59 apply zenon_Hc5. zenon_intro zenon_H96. % 0.38/0.59 apply (zenon_L5_ zenon_TA_er); trivial. % 0.38/0.59 exact (zenon_H7c zenon_H77). % 0.38/0.59 generalize (zenon_He2 (k7_grcat_1 zenon_TA_er)). zenon_intro zenon_He8. % 0.38/0.59 apply (zenon_imply_s _ _ zenon_He8); [ zenon_intro zenon_Hba | zenon_intro zenon_He9 ]. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_H78 | zenon_intro zenon_Hbb ]. % 0.38/0.59 apply (zenon_L1_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_H84 | zenon_intro zenon_H8b ]. % 0.38/0.59 apply (zenon_L3_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_L4_ zenon_TA_er); trivial. % 0.38/0.59 apply (zenon_equiv_s _ _ zenon_He9); [ zenon_intro zenon_Heb; zenon_intro zenon_Hda | zenon_intro zenon_Hea; zenon_intro zenon_Hd5 ]. % 0.38/0.59 exact (zenon_Hda zenon_Hd5). % 0.38/0.59 apply zenon_Ha9. apply sym_equal. exact zenon_Hea. % 0.38/0.59 Qed. % 0.38/0.59 % SZS output end Proof % 0.38/0.59 (* END-PROOF *) % 0.38/0.59 nodes searched: 3122 % 0.38/0.59 max branch formulas: 1317 % 0.38/0.59 proof nodes created: 375 % 0.38/0.59 formulas created: 15702 % 0.38/0.59 %------------------------------------------------------------------------------