%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n004.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 : Sat Jul 16 12:36:43 EDT 2022 % Result : Theorem 0.18s 0.52s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n004.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 : Tue Jun 14 12:02:39 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.52 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 0.18/0.52 (* PROOF-FOUND *) % 0.18/0.52 % SZS status Theorem % 0.18/0.52 (* BEGIN-PROOF *) % 0.18/0.52 % SZS output start Proof % 0.18/0.52 Theorem t38_latsubgr : (forall A : zenon_U, (((~(v3_struct_0 A))/\((v3_group_1 A)/\((v4_group_1 A)/\(l1_group_1 A))))->(forall B : zenon_U, (((~(v3_struct_0 B))/\((v3_group_1 B)/\((v4_group_1 B)/\(l1_group_1 B))))->(forall C : zenon_U, (((v1_funct_1 C)/\((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B))/\((v1_group_6 C A B)/\(m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))->((v2_funct_1 C)->(m1_lattice4 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))). % 0.18/0.52 Proof. % 0.18/0.52 assert (zenon_L1_ : forall (zenon_TB_ck : zenon_U) (zenon_TA_cl : zenon_U) (zenon_TC_cm : zenon_U), (m1_relset_1 zenon_TC_cm (u1_struct_0 zenon_TA_cl) (u1_struct_0 zenon_TB_ck)) -> (~(m2_relset_1 zenon_TC_cm (u1_struct_0 zenon_TA_cl) (u1_struct_0 zenon_TB_ck))) -> False). % 0.18/0.52 do 3 intro. intros zenon_H3c zenon_H3d. % 0.18/0.52 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TA_cl)). zenon_intro zenon_H41. % 0.18/0.52 generalize (zenon_H41 (u1_struct_0 zenon_TB_ck)). zenon_intro zenon_H42. % 0.18/0.52 generalize (zenon_H42 zenon_TC_cm). zenon_intro zenon_H43. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_H43); [ zenon_intro zenon_H3d; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H3c ]. % 0.18/0.52 exact (zenon_H45 zenon_H3c). % 0.18/0.52 exact (zenon_H3d zenon_H44). % 0.18/0.52 (* end of lemma zenon_L1_ *) % 0.18/0.52 apply NNPP. intro zenon_G. % 0.18/0.52 apply (zenon_notallex_s (fun A : zenon_U => (((~(v3_struct_0 A))/\((v3_group_1 A)/\((v4_group_1 A)/\(l1_group_1 A))))->(forall B : zenon_U, (((~(v3_struct_0 B))/\((v3_group_1 B)/\((v4_group_1 B)/\(l1_group_1 B))))->(forall C : zenon_U, (((v1_funct_1 C)/\((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B))/\((v1_group_6 C A B)/\(m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))->((v2_funct_1 C)->(m1_lattice4 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) zenon_G); [ zenon_intro zenon_H46; idtac ]. % 0.18/0.52 elim zenon_H46. zenon_intro zenon_TA_cl. zenon_intro zenon_H47. % 0.18/0.52 apply (zenon_notimply_s _ _ zenon_H47). zenon_intro zenon_H49. zenon_intro zenon_H48. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H49). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H4c). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 0.18/0.52 apply (zenon_notallex_s (fun B : zenon_U => (((~(v3_struct_0 B))/\((v3_group_1 B)/\((v4_group_1 B)/\(l1_group_1 B))))->(forall C : zenon_U, (((v1_funct_1 C)/\((v1_funct_2 C (u1_struct_0 zenon_TA_cl) (u1_struct_0 B))/\((v1_group_6 C zenon_TA_cl B)/\(m2_relset_1 C (u1_struct_0 zenon_TA_cl) (u1_struct_0 B)))))->((v2_funct_1 C)->(m1_lattice4 (k3_latsubgr zenon_TA_cl B C) (k11_group_4 zenon_TA_cl) (k11_group_4 B))))))) zenon_H48); [ zenon_intro zenon_H50; idtac ]. % 0.18/0.52 elim zenon_H50. zenon_intro zenon_TB_ck. zenon_intro zenon_H51. % 0.18/0.52 apply (zenon_notimply_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H52. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H53). zenon_intro zenon_H55. zenon_intro zenon_H54. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H54). zenon_intro zenon_H57. zenon_intro zenon_H56. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.18/0.52 apply (zenon_notallex_s (fun C : zenon_U => (((v1_funct_1 C)/\((v1_funct_2 C (u1_struct_0 zenon_TA_cl) (u1_struct_0 zenon_TB_ck))/\((v1_group_6 C zenon_TA_cl zenon_TB_ck)/\(m2_relset_1 C (u1_struct_0 zenon_TA_cl) (u1_struct_0 zenon_TB_ck)))))->((v2_funct_1 C)->(m1_lattice4 (k3_latsubgr zenon_TA_cl zenon_TB_ck C) (k11_group_4 zenon_TA_cl) (k11_group_4 zenon_TB_ck))))) zenon_H52); [ zenon_intro zenon_H5a; idtac ]. % 0.18/0.52 elim zenon_H5a. zenon_intro zenon_TC_cm. zenon_intro zenon_H5b. % 0.18/0.52 apply (zenon_notimply_s _ _ zenon_H5b). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 0.18/0.52 apply (zenon_notimply_s _ _ zenon_H5c). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H61. zenon_intro zenon_H60. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H60). zenon_intro zenon_H63. zenon_intro zenon_H62. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H64. zenon_intro zenon_H44. % 0.18/0.52 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TA_cl)). zenon_intro zenon_H41. % 0.18/0.52 generalize (zenon_H41 (u1_struct_0 zenon_TB_ck)). zenon_intro zenon_H42. % 0.18/0.52 generalize (zenon_H42 zenon_TC_cm). zenon_intro zenon_H43. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_H43); [ zenon_intro zenon_H3d; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H3c ]. % 0.18/0.52 exact (zenon_H3d zenon_H44). % 0.18/0.52 generalize (t11_vectsp_8 (k11_group_4 zenon_TA_cl)). zenon_intro zenon_H65. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H69 | zenon_intro zenon_H68 ]. % 0.18/0.52 apply zenon_H69. zenon_intro zenon_H6a. % 0.18/0.52 generalize (dt_k11_group_4 zenon_TA_cl). zenon_intro zenon_H6b. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.18/0.52 exact (zenon_H6f zenon_H4b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 0.18/0.52 exact (zenon_H71 zenon_H4d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.18/0.52 exact (zenon_H73 zenon_H4f). % 0.18/0.52 exact (zenon_H72 zenon_H4e). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.18/0.52 exact (zenon_H75 zenon_H6a). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 0.18/0.52 generalize (dt_k11_group_4 zenon_TA_cl). zenon_intro zenon_H6b. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.18/0.52 exact (zenon_H6f zenon_H4b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 0.18/0.52 exact (zenon_H71 zenon_H4d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.18/0.52 exact (zenon_H73 zenon_H4f). % 0.18/0.52 exact (zenon_H72 zenon_H4e). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H74). zenon_intro zenon_H79. zenon_intro zenon_H78. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 0.18/0.52 exact (zenon_H77 zenon_H7b). % 0.18/0.52 generalize (dt_k11_group_4 zenon_TA_cl). zenon_intro zenon_H6b. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.18/0.52 exact (zenon_H6f zenon_H4b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 0.18/0.52 exact (zenon_H71 zenon_H4d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.18/0.52 exact (zenon_H73 zenon_H4f). % 0.18/0.52 exact (zenon_H72 zenon_H4e). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H74). zenon_intro zenon_H79. zenon_intro zenon_H78. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 0.18/0.52 exact (zenon_H76 zenon_H7a). % 0.18/0.52 generalize (zenon_H66 (k11_group_4 zenon_TB_ck)). zenon_intro zenon_H7c. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H80 | zenon_intro zenon_H7f ]. % 0.18/0.52 apply zenon_H80. zenon_intro zenon_H81. % 0.18/0.52 generalize (dt_k11_group_4 zenon_TB_ck). zenon_intro zenon_H82. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 0.18/0.52 exact (zenon_H86 zenon_H55). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.18/0.52 exact (zenon_H88 zenon_H57). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 0.18/0.52 exact (zenon_H8a zenon_H59). % 0.18/0.52 exact (zenon_H89 zenon_H58). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H83). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 0.18/0.52 exact (zenon_H8c zenon_H81). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H7f); [ zenon_intro zenon_H8e | zenon_intro zenon_H8d ]. % 0.18/0.52 generalize (dt_k11_group_4 zenon_TB_ck). zenon_intro zenon_H82. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 0.18/0.52 exact (zenon_H86 zenon_H55). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.18/0.52 exact (zenon_H88 zenon_H57). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 0.18/0.52 exact (zenon_H8a zenon_H59). % 0.18/0.52 exact (zenon_H89 zenon_H58). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H83). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H90. zenon_intro zenon_H8f. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H8f). zenon_intro zenon_H92. zenon_intro zenon_H91. % 0.18/0.52 exact (zenon_H8e zenon_H92). % 0.18/0.52 generalize (dt_k11_group_4 zenon_TB_ck). zenon_intro zenon_H82. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 0.18/0.52 exact (zenon_H86 zenon_H55). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.18/0.52 exact (zenon_H88 zenon_H57). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 0.18/0.52 exact (zenon_H8a zenon_H59). % 0.18/0.52 exact (zenon_H89 zenon_H58). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H83). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H90. zenon_intro zenon_H8f. % 0.18/0.52 apply (zenon_and_s _ _ zenon_H8f). zenon_intro zenon_H92. zenon_intro zenon_H91. % 0.18/0.52 exact (zenon_H8d zenon_H91). % 0.18/0.52 generalize (zenon_H7d (k3_latsubgr zenon_TA_cl zenon_TB_ck zenon_TC_cm)). zenon_intro zenon_H93. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H93); [ zenon_intro zenon_H95 | zenon_intro zenon_H94 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 0.18/0.52 generalize (dt_k3_latsubgr zenon_TA_cl). zenon_intro zenon_H98. % 0.18/0.52 generalize (zenon_H98 zenon_TB_ck). zenon_intro zenon_H99. % 0.18/0.52 generalize (zenon_H99 zenon_TC_cm). zenon_intro zenon_H9a. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9c); [ zenon_intro zenon_H6f | zenon_intro zenon_H9d ]. % 0.18/0.52 exact (zenon_H6f zenon_H4b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9d); [ zenon_intro zenon_H71 | zenon_intro zenon_H9e ]. % 0.18/0.52 exact (zenon_H71 zenon_H4d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9e); [ zenon_intro zenon_H73 | zenon_intro zenon_H9f ]. % 0.18/0.52 exact (zenon_H73 zenon_H4f). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_H72 | zenon_intro zenon_Ha0 ]. % 0.18/0.52 exact (zenon_H72 zenon_H4e). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha0); [ zenon_intro zenon_H86 | zenon_intro zenon_Ha1 ]. % 0.18/0.52 exact (zenon_H86 zenon_H55). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha1); [ zenon_intro zenon_H88 | zenon_intro zenon_Ha2 ]. % 0.18/0.52 exact (zenon_H88 zenon_H57). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_H8a | zenon_intro zenon_Ha3 ]. % 0.18/0.52 exact (zenon_H8a zenon_H59). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_H89 | zenon_intro zenon_Ha4 ]. % 0.18/0.52 exact (zenon_H89 zenon_H58). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha5 ]. % 0.18/0.52 exact (zenon_Ha6 zenon_H61). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_H45 ]. % 0.18/0.52 exact (zenon_Ha7 zenon_H63). % 0.18/0.52 exact (zenon_H45 zenon_H3c). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_Ha9. zenon_intro zenon_Ha8. % 0.18/0.52 exact (zenon_H97 zenon_Ha9). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H96); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.18/0.52 generalize (dt_k3_latsubgr zenon_TA_cl). zenon_intro zenon_H98. % 0.18/0.52 generalize (zenon_H98 zenon_TB_ck). zenon_intro zenon_H99. % 0.18/0.52 generalize (zenon_H99 zenon_TC_cm). zenon_intro zenon_H9a. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9c); [ zenon_intro zenon_H6f | zenon_intro zenon_H9d ]. % 0.18/0.52 exact (zenon_H6f zenon_H4b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9d); [ zenon_intro zenon_H71 | zenon_intro zenon_H9e ]. % 0.18/0.52 exact (zenon_H71 zenon_H4d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9e); [ zenon_intro zenon_H73 | zenon_intro zenon_H9f ]. % 0.18/0.52 exact (zenon_H73 zenon_H4f). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_H72 | zenon_intro zenon_Ha0 ]. % 0.18/0.52 exact (zenon_H72 zenon_H4e). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha0); [ zenon_intro zenon_H86 | zenon_intro zenon_Ha1 ]. % 0.18/0.52 exact (zenon_H86 zenon_H55). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha1); [ zenon_intro zenon_H88 | zenon_intro zenon_Ha2 ]. % 0.18/0.52 exact (zenon_H88 zenon_H57). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_H8a | zenon_intro zenon_Ha3 ]. % 0.18/0.52 exact (zenon_H8a zenon_H59). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_H89 | zenon_intro zenon_Ha4 ]. % 0.18/0.52 exact (zenon_H89 zenon_H58). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha5 ]. % 0.18/0.52 exact (zenon_Ha6 zenon_H61). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_H45 ]. % 0.18/0.52 exact (zenon_Ha7 zenon_H63). % 0.18/0.52 exact (zenon_H45 zenon_H3c). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_Ha9. zenon_intro zenon_Ha8. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Ha8). zenon_intro zenon_Had. zenon_intro zenon_Hac. % 0.18/0.52 exact (zenon_Hab zenon_Had). % 0.18/0.52 generalize (redefinition_m2_relset_1 (u1_struct_0 (k11_group_4 zenon_TA_cl))). zenon_intro zenon_Hae. % 0.18/0.52 generalize (zenon_Hae (u1_struct_0 (k11_group_4 zenon_TB_ck))). zenon_intro zenon_Haf. % 0.18/0.52 generalize (zenon_Haf (k3_latsubgr zenon_TA_cl zenon_TB_ck zenon_TC_cm)). zenon_intro zenon_Hb0. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hb0); [ zenon_intro zenon_Haa; zenon_intro zenon_Hb2 | zenon_intro zenon_Hac; zenon_intro zenon_Hb1 ]. % 0.18/0.52 generalize (dt_k3_latsubgr zenon_TA_cl). zenon_intro zenon_H98. % 0.18/0.52 generalize (zenon_H98 zenon_TB_ck). zenon_intro zenon_H99. % 0.18/0.52 generalize (zenon_H99 zenon_TC_cm). zenon_intro zenon_H9a. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9c); [ zenon_intro zenon_H6f | zenon_intro zenon_H9d ]. % 0.18/0.52 exact (zenon_H6f zenon_H4b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9d); [ zenon_intro zenon_H71 | zenon_intro zenon_H9e ]. % 0.18/0.52 exact (zenon_H71 zenon_H4d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9e); [ zenon_intro zenon_H73 | zenon_intro zenon_H9f ]. % 0.18/0.52 exact (zenon_H73 zenon_H4f). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_H72 | zenon_intro zenon_Ha0 ]. % 0.18/0.52 exact (zenon_H72 zenon_H4e). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha0); [ zenon_intro zenon_H86 | zenon_intro zenon_Ha1 ]. % 0.18/0.52 exact (zenon_H86 zenon_H55). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha1); [ zenon_intro zenon_H88 | zenon_intro zenon_Ha2 ]. % 0.18/0.52 exact (zenon_H88 zenon_H57). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_H8a | zenon_intro zenon_Ha3 ]. % 0.18/0.52 exact (zenon_H8a zenon_H59). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_H89 | zenon_intro zenon_Ha4 ]. % 0.18/0.52 exact (zenon_H89 zenon_H58). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha5 ]. % 0.18/0.52 exact (zenon_Ha6 zenon_H61). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_H45 ]. % 0.18/0.52 exact (zenon_Ha7 zenon_H63). % 0.18/0.52 exact (zenon_H45 zenon_H3c). % 0.18/0.52 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_Ha9. zenon_intro zenon_Ha8. % 0.18/0.52 apply (zenon_and_s _ _ zenon_Ha8). zenon_intro zenon_Had. zenon_intro zenon_Hac. % 0.18/0.52 generalize (redefinition_m2_relset_1 (u1_struct_0 (k11_group_4 zenon_TA_cl))). zenon_intro zenon_Hae. % 0.18/0.52 generalize (zenon_Hae (u1_struct_0 (k11_group_4 zenon_TB_ck))). zenon_intro zenon_Haf. % 0.18/0.52 generalize (zenon_Haf (k3_latsubgr zenon_TA_cl zenon_TB_ck zenon_TC_cm)). zenon_intro zenon_Hb0. % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_Hb0); [ zenon_intro zenon_Haa; zenon_intro zenon_Hb2 | zenon_intro zenon_Hac; zenon_intro zenon_Hb1 ]. % 0.18/0.52 exact (zenon_Haa zenon_Hac). % 0.18/0.52 exact (zenon_Hb2 zenon_Hb1). % 0.18/0.52 exact (zenon_Haa zenon_Hac). % 0.18/0.52 apply (zenon_equiv_s _ _ zenon_H94); [ zenon_intro zenon_H5e; zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4; zenon_intro zenon_Hb3 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 0.18/0.52 generalize (t37_latsubgr zenon_TA_cl). zenon_intro zenon_Hb8. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_Hb8); [ zenon_intro zenon_H6d | zenon_intro zenon_Hb9 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.18/0.52 exact (zenon_H6f zenon_H4b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 0.18/0.52 exact (zenon_H71 zenon_H4d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.18/0.52 exact (zenon_H73 zenon_H4f). % 0.18/0.52 exact (zenon_H72 zenon_H4e). % 0.18/0.52 generalize (zenon_Hb9 zenon_TB_ck). zenon_intro zenon_Hba. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_Hba); [ zenon_intro zenon_H84 | zenon_intro zenon_Hbb ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 0.18/0.52 exact (zenon_H86 zenon_H55). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.18/0.52 exact (zenon_H88 zenon_H57). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 0.18/0.52 exact (zenon_H8a zenon_H59). % 0.18/0.52 exact (zenon_H89 zenon_H58). % 0.18/0.52 generalize (zenon_Hbb zenon_TC_cm). zenon_intro zenon_Hbc. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_Hbc); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hbd ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Hbf ]. % 0.18/0.52 exact (zenon_Ha6 zenon_H61). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hbf); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hc0 ]. % 0.18/0.52 exact (zenon_Ha7 zenon_H63). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hc0); [ zenon_intro zenon_Hc1 | zenon_intro zenon_H3d ]. % 0.18/0.52 exact (zenon_Hc1 zenon_H64). % 0.18/0.52 apply (zenon_L1_ zenon_TB_ck zenon_TA_cl zenon_TC_cm); trivial. % 0.18/0.52 exact (zenon_Hb7 zenon_Hbd). % 0.18/0.52 generalize (t36_latsubgr zenon_TA_cl). zenon_intro zenon_Hc2. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_Hc2); [ zenon_intro zenon_H6d | zenon_intro zenon_Hc3 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.18/0.52 exact (zenon_H6f zenon_H4b). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 0.18/0.52 exact (zenon_H71 zenon_H4d). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.18/0.52 exact (zenon_H73 zenon_H4f). % 0.18/0.52 exact (zenon_H72 zenon_H4e). % 0.18/0.52 generalize (zenon_Hc3 zenon_TB_ck). zenon_intro zenon_Hc4. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_Hc4); [ zenon_intro zenon_H84 | zenon_intro zenon_Hc5 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 0.18/0.52 exact (zenon_H86 zenon_H55). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.18/0.52 exact (zenon_H88 zenon_H57). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 0.18/0.52 exact (zenon_H8a zenon_H59). % 0.18/0.52 exact (zenon_H89 zenon_H58). % 0.18/0.52 generalize (zenon_Hc5 zenon_TC_cm). zenon_intro zenon_Hc6. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_Hc6); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hc7 ]. % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Hbf ]. % 0.18/0.52 exact (zenon_Ha6 zenon_H61). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hbf); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Hc0 ]. % 0.18/0.52 exact (zenon_Ha7 zenon_H63). % 0.18/0.52 apply (zenon_notand_s _ _ zenon_Hc0); [ zenon_intro zenon_Hc1 | zenon_intro zenon_H3d ]. % 0.18/0.52 exact (zenon_Hc1 zenon_H64). % 0.18/0.52 apply (zenon_L1_ zenon_TB_ck zenon_TA_cl zenon_TC_cm); trivial. % 0.18/0.52 apply (zenon_imply_s _ _ zenon_Hc7); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hc8 ]. % 0.18/0.52 exact (zenon_Hc9 zenon_H5f). % 0.18/0.52 exact (zenon_Hb6 zenon_Hc8). % 0.18/0.52 exact (zenon_H5e zenon_Hb4). % 0.18/0.52 Qed. % 0.18/0.52 % SZS output end Proof % 0.18/0.52 (* END-PROOF *) % 0.18/0.52 nodes searched: 622 % 0.18/0.52 max branch formulas: 454 % 0.18/0.52 proof nodes created: 179 % 0.18/0.52 formulas created: 4430 % 0.18/0.52 %------------------------------------------------------------------------------