%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LAT370+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n012.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:16 EDT 2022 % Result : Theorem 3.21s 3.44s % Output : Proof 3.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : LAT370+1 : TPTP v8.1.0. Released v3.4.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n012.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 : Wed Jun 29 02:33:33 EDT 2022 % 0.12/0.33 % CPUTime : % 3.21/3.44 Zenon warning: unused variable (B : zenon_U) in reflexivity_r1_tarski % 3.21/3.44 (* PROOF-FOUND *) % 3.21/3.44 % SZS status Theorem % 3.21/3.44 (* BEGIN-PROOF *) % 3.21/3.44 % SZS output start Proof % 3.21/3.44 Theorem t43_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)/\((v3_waybel_3 A)/\(l1_orders_2 A))))))))->(forall B : zenon_U, (((v1_funct_1 B)/\((v1_funct_2 B (u1_struct_0 A) (u1_struct_0 A))/\((v7_waybel_1 B A)/\(m2_relset_1 B (u1_struct_0 A) (u1_struct_0 A)))))->((v1_waybel34 (k2_waybel_1 A A B) A (k2_yellow_2 A A B))->(v4_waybel_0 (k2_yellow_2 A A B) A)))))). % 3.21/3.44 Proof. % 3.21/3.44 assert (zenon_L1_ : forall (zenon_TA_fn : zenon_U) (zenon_TB_fo : zenon_U), (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (~(m2_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn))) -> False). % 3.21/3.44 do 2 intro. intros zenon_H8d zenon_H8e. % 3.21/3.44 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TA_fn)). zenon_intro zenon_H91. % 3.21/3.44 generalize (zenon_H91 (u1_struct_0 zenon_TA_fn)). zenon_intro zenon_H92. % 3.21/3.44 generalize (zenon_H92 zenon_TB_fo). zenon_intro zenon_H93. % 3.21/3.44 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H8e; zenon_intro zenon_H95 | zenon_intro zenon_H94; zenon_intro zenon_H8d ]. % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 exact (zenon_H8e zenon_H94). % 3.21/3.44 (* end of lemma zenon_L1_ *) % 3.21/3.44 assert (zenon_L2_ : forall (zenon_TA_fn : zenon_U), (l1_orders_2 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (v3_struct_0 zenon_TA_fn) -> False). % 3.21/3.44 do 1 intro. intros zenon_H96 zenon_H97 zenon_H98. % 3.21/3.44 generalize (cc1_lattice3 zenon_TA_fn). zenon_intro zenon_H99. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H99); [ zenon_intro zenon_H9b | zenon_intro zenon_H9a ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H9d | zenon_intro zenon_H9c ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 exact (zenon_H9c zenon_H98). % 3.21/3.44 (* end of lemma zenon_L2_ *) % 3.21/3.44 assert (zenon_L3_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (~(v2_orders_2 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v7_waybel_1 zenon_TB_fo zenon_TA_fn) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_1 zenon_TB_fo) -> (v4_orders_2 zenon_TA_fn) -> (v3_orders_2 zenon_TA_fn) -> (v2_orders_2 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (l1_orders_2 zenon_TA_fn) -> False). % 3.21/3.44 do 2 intro. intros zenon_H9e zenon_H8d zenon_H9f zenon_Ha0 zenon_Ha1 zenon_Ha2 zenon_Ha3 zenon_Ha4 zenon_H97 zenon_H96. % 3.21/3.44 generalize (fc10_waybel10 zenon_TA_fn). zenon_intro zenon_Ha5. % 3.21/3.44 generalize (zenon_Ha5 zenon_TB_fo). zenon_intro zenon_Ha6. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Ha6); [ zenon_intro zenon_Ha8 | zenon_intro zenon_Ha7 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Ha8); [ zenon_intro zenon_Haa | zenon_intro zenon_Ha9 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Ha9); [ zenon_intro zenon_Hac | zenon_intro zenon_Hab ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hab); [ zenon_intro zenon_Hae | zenon_intro zenon_Had ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haf ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Haf); [ zenon_intro zenon_H9b | zenon_intro zenon_Hb1 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hb1); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb6 | zenon_intro zenon_H95 ]. % 3.21/3.44 exact (zenon_Hb6 zenon_H9f). % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_Ha7). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hb7). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Hbc. zenon_intro zenon_Hbb. % 3.21/3.44 exact (zenon_H9e zenon_Hbc). % 3.21/3.44 (* end of lemma zenon_L3_ *) % 3.21/3.44 assert (zenon_L4_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (l1_orders_2 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_1 zenon_TB_fo) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v7_waybel_1 zenon_TB_fo zenon_TA_fn) -> (~(v6_waybel_1 zenon_TB_fo zenon_TA_fn)) -> False). % 3.21/3.44 do 2 intro. intros zenon_H96 zenon_H97 zenon_H8d zenon_Ha1 zenon_Ha0 zenon_H9f zenon_Hbd. % 3.21/3.44 generalize (cc3_waybel_1 zenon_TA_fn). zenon_intro zenon_Hbe. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hbe); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Hbf ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hc0); [ zenon_intro zenon_Haa | zenon_intro zenon_H9b ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 generalize (zenon_Hbf zenon_TB_fo). zenon_intro zenon_Hc1. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hc1); [ zenon_intro zenon_H95 | zenon_intro zenon_Hc2 ]. % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc4 | zenon_intro zenon_Hc3 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hc4); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hc5 ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hc5); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb6 ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 exact (zenon_Hb6 zenon_H9f). % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hc3). zenon_intro zenon_Ha1. zenon_intro zenon_Hc6. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hc6). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_Ha0. zenon_intro zenon_Hc9. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_Hcb. zenon_intro zenon_Hca. % 3.21/3.44 exact (zenon_Hbd zenon_Hca). % 3.21/3.44 (* end of lemma zenon_L4_ *) % 3.21/3.44 assert (zenon_L5_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (~(v3_orders_2 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))) -> (v7_waybel_1 zenon_TB_fo zenon_TA_fn) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_1 zenon_TB_fo) -> (l1_orders_2 zenon_TA_fn) -> (v3_lattice3 zenon_TA_fn) -> (v2_lattice3 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (v4_orders_2 zenon_TA_fn) -> (v3_orders_2 zenon_TA_fn) -> (v2_orders_2 zenon_TA_fn) -> False). % 3.21/3.44 do 2 intro. intros zenon_Hcc zenon_H9f zenon_H8d zenon_Ha0 zenon_Ha1 zenon_H96 zenon_Hcd zenon_Hce zenon_H97 zenon_Ha2 zenon_Ha3 zenon_Ha4. % 3.21/3.44 generalize (fc10_waybel34 zenon_TA_fn). zenon_intro zenon_Hcf. % 3.21/3.44 generalize (zenon_Hcf zenon_TB_fo). zenon_intro zenon_Hd0. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hac | zenon_intro zenon_Hd3 ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_Hae | zenon_intro zenon_Hd4 ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd4); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hd5 ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd5); [ zenon_intro zenon_H9d | zenon_intro zenon_Hd6 ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 3.21/3.44 exact (zenon_Hd8 zenon_Hce). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd7); [ zenon_intro zenon_Hda | zenon_intro zenon_Hd9 ]. % 3.21/3.44 exact (zenon_Hda zenon_Hcd). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd9); [ zenon_intro zenon_H9b | zenon_intro zenon_Hdb ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdb); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hdc ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdc); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hdd ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_Hbd | zenon_intro zenon_H95 ]. % 3.21/3.44 apply (zenon_L4_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hd1). zenon_intro zenon_Hb8. zenon_intro zenon_Hde. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hde). zenon_intro zenon_Hba. zenon_intro zenon_Hdf. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_Hbc. zenon_intro zenon_He0. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He0). zenon_intro zenon_He2. zenon_intro zenon_He1. % 3.21/3.44 exact (zenon_Hcc zenon_He2). % 3.21/3.44 (* end of lemma zenon_L5_ *) % 3.21/3.44 assert (zenon_L6_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (~(v4_orders_2 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))) -> (v7_waybel_1 zenon_TB_fo zenon_TA_fn) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_1 zenon_TB_fo) -> (l1_orders_2 zenon_TA_fn) -> (v3_lattice3 zenon_TA_fn) -> (v2_lattice3 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (v4_orders_2 zenon_TA_fn) -> (v3_orders_2 zenon_TA_fn) -> (v2_orders_2 zenon_TA_fn) -> False). % 3.21/3.44 do 2 intro. intros zenon_He3 zenon_H9f zenon_H8d zenon_Ha0 zenon_Ha1 zenon_H96 zenon_Hcd zenon_Hce zenon_H97 zenon_Ha2 zenon_Ha3 zenon_Ha4. % 3.21/3.44 generalize (fc10_waybel34 zenon_TA_fn). zenon_intro zenon_Hcf. % 3.21/3.44 generalize (zenon_Hcf zenon_TB_fo). zenon_intro zenon_Hd0. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hac | zenon_intro zenon_Hd3 ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_Hae | zenon_intro zenon_Hd4 ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd4); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hd5 ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd5); [ zenon_intro zenon_H9d | zenon_intro zenon_Hd6 ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 3.21/3.44 exact (zenon_Hd8 zenon_Hce). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd7); [ zenon_intro zenon_Hda | zenon_intro zenon_Hd9 ]. % 3.21/3.44 exact (zenon_Hda zenon_Hcd). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd9); [ zenon_intro zenon_H9b | zenon_intro zenon_Hdb ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdb); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hdc ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdc); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hdd ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_Hbd | zenon_intro zenon_H95 ]. % 3.21/3.44 apply (zenon_L4_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hd1). zenon_intro zenon_Hb8. zenon_intro zenon_Hde. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hde). zenon_intro zenon_Hba. zenon_intro zenon_Hdf. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_Hbc. zenon_intro zenon_He0. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He0). zenon_intro zenon_He2. zenon_intro zenon_He1. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He1). zenon_intro zenon_He5. zenon_intro zenon_He4. % 3.21/3.44 exact (zenon_He3 zenon_He5). % 3.21/3.44 (* end of lemma zenon_L6_ *) % 3.21/3.44 assert (zenon_L7_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (~(v1_lattice3 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))) -> (v7_waybel_1 zenon_TB_fo zenon_TA_fn) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_1 zenon_TB_fo) -> (l1_orders_2 zenon_TA_fn) -> (v3_lattice3 zenon_TA_fn) -> (v2_lattice3 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (v4_orders_2 zenon_TA_fn) -> (v3_orders_2 zenon_TA_fn) -> (v2_orders_2 zenon_TA_fn) -> False). % 3.21/3.44 do 2 intro. intros zenon_He6 zenon_H9f zenon_H8d zenon_Ha0 zenon_Ha1 zenon_H96 zenon_Hcd zenon_Hce zenon_H97 zenon_Ha2 zenon_Ha3 zenon_Ha4. % 3.21/3.44 generalize (fc10_waybel34 zenon_TA_fn). zenon_intro zenon_Hcf. % 3.21/3.44 generalize (zenon_Hcf zenon_TB_fo). zenon_intro zenon_Hd0. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hac | zenon_intro zenon_Hd3 ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_Hae | zenon_intro zenon_Hd4 ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd4); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hd5 ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd5); [ zenon_intro zenon_H9d | zenon_intro zenon_Hd6 ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 3.21/3.44 exact (zenon_Hd8 zenon_Hce). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd7); [ zenon_intro zenon_Hda | zenon_intro zenon_Hd9 ]. % 3.21/3.44 exact (zenon_Hda zenon_Hcd). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd9); [ zenon_intro zenon_H9b | zenon_intro zenon_Hdb ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdb); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hdc ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdc); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hdd ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_Hbd | zenon_intro zenon_H95 ]. % 3.21/3.44 apply (zenon_L4_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hd1). zenon_intro zenon_Hb8. zenon_intro zenon_Hde. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hde). zenon_intro zenon_Hba. zenon_intro zenon_Hdf. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_Hbc. zenon_intro zenon_He0. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He0). zenon_intro zenon_He2. zenon_intro zenon_He1. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He1). zenon_intro zenon_He5. zenon_intro zenon_He4. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He4). zenon_intro zenon_He8. zenon_intro zenon_He7. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He7). zenon_intro zenon_Hea. zenon_intro zenon_He9. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He9). zenon_intro zenon_Hec. zenon_intro zenon_Heb. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Heb). zenon_intro zenon_Hee. zenon_intro zenon_Hed. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hed). zenon_intro zenon_Hf0. zenon_intro zenon_Hef. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hef). zenon_intro zenon_Hf2. zenon_intro zenon_Hf1. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hf1). zenon_intro zenon_Hf4. zenon_intro zenon_Hf3. % 3.21/3.44 exact (zenon_He6 zenon_Hf4). % 3.21/3.44 (* end of lemma zenon_L7_ *) % 3.21/3.44 assert (zenon_L8_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (~(v2_lattice3 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))) -> (v7_waybel_1 zenon_TB_fo zenon_TA_fn) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_1 zenon_TB_fo) -> (l1_orders_2 zenon_TA_fn) -> (v3_lattice3 zenon_TA_fn) -> (v2_lattice3 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (v4_orders_2 zenon_TA_fn) -> (v3_orders_2 zenon_TA_fn) -> (v2_orders_2 zenon_TA_fn) -> False). % 3.21/3.44 do 2 intro. intros zenon_Hf5 zenon_H9f zenon_H8d zenon_Ha0 zenon_Ha1 zenon_H96 zenon_Hcd zenon_Hce zenon_H97 zenon_Ha2 zenon_Ha3 zenon_Ha4. % 3.21/3.44 generalize (fc10_waybel34 zenon_TA_fn). zenon_intro zenon_Hcf. % 3.21/3.44 generalize (zenon_Hcf zenon_TB_fo). zenon_intro zenon_Hd0. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hac | zenon_intro zenon_Hd3 ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_Hae | zenon_intro zenon_Hd4 ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd4); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hd5 ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd5); [ zenon_intro zenon_H9d | zenon_intro zenon_Hd6 ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 3.21/3.44 exact (zenon_Hd8 zenon_Hce). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd7); [ zenon_intro zenon_Hda | zenon_intro zenon_Hd9 ]. % 3.21/3.44 exact (zenon_Hda zenon_Hcd). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd9); [ zenon_intro zenon_H9b | zenon_intro zenon_Hdb ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdb); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hdc ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdc); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hdd ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_Hbd | zenon_intro zenon_H95 ]. % 3.21/3.44 apply (zenon_L4_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hd1). zenon_intro zenon_Hb8. zenon_intro zenon_Hde. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hde). zenon_intro zenon_Hba. zenon_intro zenon_Hdf. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_Hbc. zenon_intro zenon_He0. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He0). zenon_intro zenon_He2. zenon_intro zenon_He1. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He1). zenon_intro zenon_He5. zenon_intro zenon_He4. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He4). zenon_intro zenon_He8. zenon_intro zenon_He7. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He7). zenon_intro zenon_Hea. zenon_intro zenon_He9. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He9). zenon_intro zenon_Hec. zenon_intro zenon_Heb. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Heb). zenon_intro zenon_Hee. zenon_intro zenon_Hed. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hed). zenon_intro zenon_Hf0. zenon_intro zenon_Hef. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hef). zenon_intro zenon_Hf2. zenon_intro zenon_Hf1. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hf1). zenon_intro zenon_Hf4. zenon_intro zenon_Hf3. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hf3). zenon_intro zenon_Hf7. zenon_intro zenon_Hf6. % 3.21/3.44 exact (zenon_Hf5 zenon_Hf7). % 3.21/3.44 (* end of lemma zenon_L8_ *) % 3.21/3.44 assert (zenon_L9_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (~(v3_lattice3 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))) -> (v7_waybel_1 zenon_TB_fo zenon_TA_fn) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_1 zenon_TB_fo) -> (l1_orders_2 zenon_TA_fn) -> (v3_lattice3 zenon_TA_fn) -> (v2_lattice3 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (v4_orders_2 zenon_TA_fn) -> (v3_orders_2 zenon_TA_fn) -> (v2_orders_2 zenon_TA_fn) -> False). % 3.21/3.44 do 2 intro. intros zenon_Hf8 zenon_H9f zenon_H8d zenon_Ha0 zenon_Ha1 zenon_H96 zenon_Hcd zenon_Hce zenon_H97 zenon_Ha2 zenon_Ha3 zenon_Ha4. % 3.21/3.44 generalize (fc10_waybel34 zenon_TA_fn). zenon_intro zenon_Hcf. % 3.21/3.44 generalize (zenon_Hcf zenon_TB_fo). zenon_intro zenon_Hd0. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hac | zenon_intro zenon_Hd3 ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_Hae | zenon_intro zenon_Hd4 ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd4); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hd5 ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd5); [ zenon_intro zenon_H9d | zenon_intro zenon_Hd6 ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd6); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 3.21/3.44 exact (zenon_Hd8 zenon_Hce). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd7); [ zenon_intro zenon_Hda | zenon_intro zenon_Hd9 ]. % 3.21/3.44 exact (zenon_Hda zenon_Hcd). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hd9); [ zenon_intro zenon_H9b | zenon_intro zenon_Hdb ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdb); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hdc ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdc); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hdd ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_Hbd | zenon_intro zenon_H95 ]. % 3.21/3.44 apply (zenon_L4_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hd1). zenon_intro zenon_Hb8. zenon_intro zenon_Hde. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hde). zenon_intro zenon_Hba. zenon_intro zenon_Hdf. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_Hbc. zenon_intro zenon_He0. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He0). zenon_intro zenon_He2. zenon_intro zenon_He1. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He1). zenon_intro zenon_He5. zenon_intro zenon_He4. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He4). zenon_intro zenon_He8. zenon_intro zenon_He7. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He7). zenon_intro zenon_Hea. zenon_intro zenon_He9. % 3.21/3.44 apply (zenon_and_s _ _ zenon_He9). zenon_intro zenon_Hec. zenon_intro zenon_Heb. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Heb). zenon_intro zenon_Hee. zenon_intro zenon_Hed. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hed). zenon_intro zenon_Hf0. zenon_intro zenon_Hef. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hef). zenon_intro zenon_Hf2. zenon_intro zenon_Hf1. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hf1). zenon_intro zenon_Hf4. zenon_intro zenon_Hf3. % 3.21/3.44 apply (zenon_and_s _ _ zenon_Hf3). zenon_intro zenon_Hf7. zenon_intro zenon_Hf6. % 3.21/3.44 exact (zenon_Hf8 zenon_Hf6). % 3.21/3.44 (* end of lemma zenon_L9_ *) % 3.21/3.44 assert (zenon_L10_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (l1_orders_2 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (v1_funct_1 zenon_TB_fo) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (~(l1_orders_2 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))) -> False). % 3.21/3.44 do 2 intro. intros zenon_H96 zenon_H97 zenon_Ha1 zenon_Ha0 zenon_H8d zenon_Hf9. % 3.21/3.44 generalize (dt_k2_yellow_2 zenon_TA_fn). zenon_intro zenon_Hfa. % 3.21/3.44 generalize (zenon_Hfa zenon_TA_fn). zenon_intro zenon_Hfb. % 3.21/3.44 generalize (dt_m1_yellow_0 zenon_TA_fn). zenon_intro zenon_Hfc. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hfc); [ zenon_intro zenon_H9b | zenon_intro zenon_Hfd ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 generalize (zenon_Hfd (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo)). zenon_intro zenon_Hfe. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_Hfe); [ zenon_intro zenon_H100 | zenon_intro zenon_Hff ]. % 3.21/3.44 generalize (zenon_Hfb zenon_TB_fo). zenon_intro zenon_H101. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H101); [ zenon_intro zenon_H103 | zenon_intro zenon_H102 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Haa | zenon_intro zenon_H104 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H104); [ zenon_intro zenon_H9b | zenon_intro zenon_H105 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_Haa | zenon_intro zenon_H106 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H106); [ zenon_intro zenon_H9b | zenon_intro zenon_H107 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H107); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H108 ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H95 ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_H102). zenon_intro zenon_Hba. zenon_intro zenon_H109. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H109). zenon_intro zenon_Hee. zenon_intro zenon_H10a. % 3.21/3.44 exact (zenon_H100 zenon_H10a). % 3.21/3.44 exact (zenon_Hf9 zenon_Hff). % 3.21/3.44 (* end of lemma zenon_L10_ *) % 3.21/3.44 assert (zenon_L11_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (l1_orders_2 zenon_TA_fn) -> (v1_lattice3 zenon_TA_fn) -> (v1_funct_1 zenon_TB_fo) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (~(v1_funct_2 (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo) (u1_struct_0 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo)) (u1_struct_0 zenon_TA_fn))) -> False). % 3.21/3.44 do 2 intro. intros zenon_H96 zenon_H97 zenon_Ha1 zenon_Ha0 zenon_H8d zenon_H10b. % 3.21/3.44 generalize (dt_k3_waybel_1 zenon_TA_fn). zenon_intro zenon_H10c. % 3.21/3.44 generalize (zenon_H10c zenon_TA_fn). zenon_intro zenon_H10d. % 3.21/3.44 generalize (zenon_H10d zenon_TB_fo). zenon_intro zenon_H10e. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H10e); [ zenon_intro zenon_H103 | zenon_intro zenon_H10f ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Haa | zenon_intro zenon_H104 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H104); [ zenon_intro zenon_H9b | zenon_intro zenon_H105 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_Haa | zenon_intro zenon_H106 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H106); [ zenon_intro zenon_H9b | zenon_intro zenon_H107 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H107); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H108 ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H95 ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_H10f). zenon_intro zenon_H111. zenon_intro zenon_H110. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H110). zenon_intro zenon_H113. zenon_intro zenon_H112. % 3.21/3.44 exact (zenon_H10b zenon_H113). % 3.21/3.44 (* end of lemma zenon_L11_ *) % 3.21/3.44 assert (zenon_L12_ : forall (zenon_TA_fn : zenon_U) (zenon_TB_fo : zenon_U), (m1_relset_1 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_2 zenon_TB_fo (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)) -> (v1_funct_1 zenon_TB_fo) -> (v1_lattice3 zenon_TA_fn) -> (l1_orders_2 zenon_TA_fn) -> (~(m2_relset_1 (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo) (u1_struct_0 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo)) (u1_struct_0 zenon_TA_fn))) -> False). % 3.21/3.44 do 2 intro. intros zenon_H8d zenon_Ha0 zenon_Ha1 zenon_H97 zenon_H96 zenon_H114. % 3.21/3.44 generalize (redefinition_m2_relset_1 (u1_struct_0 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))). zenon_intro zenon_H115. % 3.21/3.44 generalize (zenon_H115 (u1_struct_0 zenon_TA_fn)). zenon_intro zenon_H116. % 3.21/3.44 generalize (zenon_H116 (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo)). zenon_intro zenon_H117. % 3.21/3.44 apply (zenon_equiv_s _ _ zenon_H117); [ zenon_intro zenon_H114; zenon_intro zenon_H119 | zenon_intro zenon_H112; zenon_intro zenon_H118 ]. % 3.21/3.44 generalize (dt_k3_waybel_1 zenon_TA_fn). zenon_intro zenon_H10c. % 3.21/3.44 generalize (zenon_H10c zenon_TA_fn). zenon_intro zenon_H10d. % 3.21/3.44 generalize (zenon_H10d zenon_TB_fo). zenon_intro zenon_H10e. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H10e); [ zenon_intro zenon_H103 | zenon_intro zenon_H10f ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Haa | zenon_intro zenon_H104 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H104); [ zenon_intro zenon_H9b | zenon_intro zenon_H105 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_Haa | zenon_intro zenon_H106 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H106); [ zenon_intro zenon_H9b | zenon_intro zenon_H107 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H107); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H108 ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H95 ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_H10f). zenon_intro zenon_H111. zenon_intro zenon_H110. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H110). zenon_intro zenon_H113. zenon_intro zenon_H112. % 3.21/3.44 generalize (redefinition_m2_relset_1 (u1_struct_0 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))). zenon_intro zenon_H115. % 3.21/3.44 generalize (zenon_H115 (u1_struct_0 zenon_TA_fn)). zenon_intro zenon_H116. % 3.21/3.44 generalize (zenon_H116 (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo)). zenon_intro zenon_H117. % 3.21/3.44 apply (zenon_equiv_s _ _ zenon_H117); [ zenon_intro zenon_H114; zenon_intro zenon_H119 | zenon_intro zenon_H112; zenon_intro zenon_H118 ]. % 3.21/3.44 exact (zenon_H114 zenon_H112). % 3.21/3.44 exact (zenon_H119 zenon_H118). % 3.21/3.44 exact (zenon_H114 zenon_H112). % 3.21/3.44 (* end of lemma zenon_L12_ *) % 3.21/3.44 assert (zenon_L13_ : forall (zenon_TB_fo : zenon_U) (zenon_TA_fn : zenon_U), (~(v1_waybel34 (k1_waybel34 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo) zenon_TA_fn (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo)) zenon_TA_fn (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))) -> (v1_waybel34 (k2_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo) zenon_TA_fn (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo)) -> ((k1_waybel34 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo) zenon_TA_fn (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo)) = (k2_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo)) -> False). % 3.21/3.44 do 2 intro. intros zenon_H11a zenon_H11b zenon_H11c. % 3.21/3.44 cut ((v1_waybel34 (k2_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo) zenon_TA_fn (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo)) = (v1_waybel34 (k1_waybel34 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo) zenon_TA_fn (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo)) zenon_TA_fn (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))). % 3.21/3.44 intro zenon_D_pnotp. % 3.21/3.44 apply zenon_H11a. % 3.21/3.44 rewrite <- zenon_D_pnotp. % 3.21/3.44 exact zenon_H11b. % 3.21/3.44 cut (((k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo) = (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo))); [idtac | apply NNPP; zenon_intro zenon_H11d]. % 3.21/3.44 cut ((zenon_TA_fn = zenon_TA_fn)); [idtac | apply NNPP; zenon_intro zenon_H11e]. % 3.21/3.44 cut (((k2_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo) = (k1_waybel34 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo) zenon_TA_fn (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo)))); [idtac | apply NNPP; zenon_intro zenon_H11f]. % 3.21/3.44 congruence. % 3.21/3.44 apply zenon_H11f. apply sym_equal. exact zenon_H11c. % 3.21/3.44 apply zenon_H11e. apply refl_equal. % 3.21/3.44 apply zenon_H11d. apply refl_equal. % 3.21/3.44 (* end of lemma zenon_L13_ *) % 3.21/3.44 apply NNPP. intro zenon_G. % 3.21/3.44 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)/\((v3_waybel_3 A)/\(l1_orders_2 A))))))))->(forall B : zenon_U, (((v1_funct_1 B)/\((v1_funct_2 B (u1_struct_0 A) (u1_struct_0 A))/\((v7_waybel_1 B A)/\(m2_relset_1 B (u1_struct_0 A) (u1_struct_0 A)))))->((v1_waybel34 (k2_waybel_1 A A B) A (k2_yellow_2 A A B))->(v4_waybel_0 (k2_yellow_2 A A B) A)))))) zenon_G); [ zenon_intro zenon_H120; idtac ]. % 3.21/3.44 elim zenon_H120. zenon_intro zenon_TA_fn. zenon_intro zenon_H121. % 3.21/3.44 apply (zenon_notimply_s _ _ zenon_H121). zenon_intro zenon_H123. zenon_intro zenon_H122. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H123). zenon_intro zenon_Ha4. zenon_intro zenon_H124. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H124). zenon_intro zenon_Ha3. zenon_intro zenon_H125. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H125). zenon_intro zenon_Ha2. zenon_intro zenon_H126. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H126). zenon_intro zenon_H97. zenon_intro zenon_H127. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H127). zenon_intro zenon_Hce. zenon_intro zenon_H128. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H128). zenon_intro zenon_Hcd. zenon_intro zenon_H129. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H129). zenon_intro zenon_H12a. zenon_intro zenon_H96. % 3.21/3.44 apply (zenon_notallex_s (fun B : zenon_U => (((v1_funct_1 B)/\((v1_funct_2 B (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn))/\((v7_waybel_1 B zenon_TA_fn)/\(m2_relset_1 B (u1_struct_0 zenon_TA_fn) (u1_struct_0 zenon_TA_fn)))))->((v1_waybel34 (k2_waybel_1 zenon_TA_fn zenon_TA_fn B) zenon_TA_fn (k2_yellow_2 zenon_TA_fn zenon_TA_fn B))->(v4_waybel_0 (k2_yellow_2 zenon_TA_fn zenon_TA_fn B) zenon_TA_fn)))) zenon_H122); [ zenon_intro zenon_H12b; idtac ]. % 3.21/3.44 elim zenon_H12b. zenon_intro zenon_TB_fo. zenon_intro zenon_H12c. % 3.21/3.44 apply (zenon_notimply_s _ _ zenon_H12c). zenon_intro zenon_H12e. zenon_intro zenon_H12d. % 3.21/3.44 apply (zenon_notimply_s _ _ zenon_H12d). zenon_intro zenon_H11b. zenon_intro zenon_H12f. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H12e). zenon_intro zenon_Ha1. zenon_intro zenon_H130. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H130). zenon_intro zenon_Ha0. zenon_intro zenon_H131. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H131). zenon_intro zenon_H9f. zenon_intro zenon_H94. % 3.21/3.44 generalize (redefinition_m2_relset_1 (u1_struct_0 zenon_TA_fn)). zenon_intro zenon_H91. % 3.21/3.44 generalize (zenon_H91 (u1_struct_0 zenon_TA_fn)). zenon_intro zenon_H92. % 3.21/3.44 generalize (zenon_H92 zenon_TB_fo). zenon_intro zenon_H93. % 3.21/3.44 apply (zenon_equiv_s _ _ zenon_H93); [ zenon_intro zenon_H8e; zenon_intro zenon_H95 | zenon_intro zenon_H94; zenon_intro zenon_H8d ]. % 3.21/3.44 exact (zenon_H8e zenon_H94). % 3.21/3.44 generalize (t40_waybel34 zenon_TA_fn). zenon_intro zenon_H132. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H132); [ zenon_intro zenon_H134 | zenon_intro zenon_H133 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H134); [ zenon_intro zenon_Hac | zenon_intro zenon_H135 ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H135); [ zenon_intro zenon_Hae | zenon_intro zenon_H136 ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H136); [ zenon_intro zenon_Hb0 | zenon_intro zenon_H137 ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H137); [ zenon_intro zenon_H9d | zenon_intro zenon_H138 ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H138); [ zenon_intro zenon_Hd8 | zenon_intro zenon_H139 ]. % 3.21/3.44 exact (zenon_Hd8 zenon_Hce). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H139); [ zenon_intro zenon_Hda | zenon_intro zenon_H9b ]. % 3.21/3.44 exact (zenon_Hda zenon_Hcd). % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 generalize (zenon_H133 zenon_TB_fo). zenon_intro zenon_H13a. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H13a); [ zenon_intro zenon_H13c | zenon_intro zenon_H13b ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H13c); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H13d ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H13d); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H13e ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H13e); [ zenon_intro zenon_Hb6 | zenon_intro zenon_H8e ]. % 3.21/3.44 exact (zenon_Hb6 zenon_H9f). % 3.21/3.44 apply (zenon_L1_ zenon_TA_fn zenon_TB_fo); trivial. % 3.21/3.44 apply (zenon_equiv_s _ _ zenon_H13b); [ zenon_intro zenon_H12f; zenon_intro zenon_H141 | zenon_intro zenon_H140; zenon_intro zenon_H13f ]. % 3.21/3.44 generalize (t39_waybel34 zenon_TA_fn). zenon_intro zenon_H142. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H142); [ zenon_intro zenon_H134 | zenon_intro zenon_H143 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H134); [ zenon_intro zenon_Hac | zenon_intro zenon_H135 ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H135); [ zenon_intro zenon_Hae | zenon_intro zenon_H136 ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H136); [ zenon_intro zenon_Hb0 | zenon_intro zenon_H137 ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H137); [ zenon_intro zenon_H9d | zenon_intro zenon_H138 ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H138); [ zenon_intro zenon_Hd8 | zenon_intro zenon_H139 ]. % 3.21/3.44 exact (zenon_Hd8 zenon_Hce). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H139); [ zenon_intro zenon_Hda | zenon_intro zenon_H9b ]. % 3.21/3.44 exact (zenon_Hda zenon_Hcd). % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 generalize (zenon_H143 zenon_TB_fo). zenon_intro zenon_H144. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H144); [ zenon_intro zenon_H13c | zenon_intro zenon_H145 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H13c); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H13d ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H13d); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H13e ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H13e); [ zenon_intro zenon_Hb6 | zenon_intro zenon_H8e ]. % 3.21/3.44 exact (zenon_Hb6 zenon_H9f). % 3.21/3.44 apply (zenon_L1_ zenon_TA_fn zenon_TB_fo); trivial. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H145). zenon_intro zenon_H147. zenon_intro zenon_H146. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H146). zenon_intro zenon_H149. zenon_intro zenon_H148. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H148). zenon_intro zenon_H14a. zenon_intro zenon_H11c. % 3.21/3.44 generalize (t25_waybel34 (k2_yellow_2 zenon_TA_fn zenon_TA_fn zenon_TB_fo)). zenon_intro zenon_H14b. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H14b); [ zenon_intro zenon_H14d | zenon_intro zenon_H14c ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H14d); [ zenon_intro zenon_H9e | zenon_intro zenon_H14e ]. % 3.21/3.44 apply (zenon_L3_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H14e); [ zenon_intro zenon_Hcc | zenon_intro zenon_H14f ]. % 3.21/3.44 apply (zenon_L5_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H14f); [ zenon_intro zenon_He3 | zenon_intro zenon_H150 ]. % 3.21/3.44 apply (zenon_L6_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H150); [ zenon_intro zenon_He6 | zenon_intro zenon_H151 ]. % 3.21/3.44 apply (zenon_L7_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H151); [ zenon_intro zenon_Hf5 | zenon_intro zenon_H152 ]. % 3.21/3.44 apply (zenon_L8_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H152); [ zenon_intro zenon_Hf8 | zenon_intro zenon_Hf9 ]. % 3.21/3.44 apply (zenon_L9_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_L10_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 generalize (zenon_H14c zenon_TA_fn). zenon_intro zenon_H153. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H153); [ zenon_intro zenon_H155 | zenon_intro zenon_H154 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H155); [ zenon_intro zenon_Hac | zenon_intro zenon_H156 ]. % 3.21/3.44 exact (zenon_Hac zenon_Ha4). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H156); [ zenon_intro zenon_Hae | zenon_intro zenon_H157 ]. % 3.21/3.44 exact (zenon_Hae zenon_Ha3). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H157); [ zenon_intro zenon_Hb0 | zenon_intro zenon_H158 ]. % 3.21/3.44 exact (zenon_Hb0 zenon_Ha2). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H158); [ zenon_intro zenon_H9d | zenon_intro zenon_H159 ]. % 3.21/3.44 exact (zenon_H9d zenon_H97). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H159); [ zenon_intro zenon_Hd8 | zenon_intro zenon_H15a ]. % 3.21/3.44 exact (zenon_Hd8 zenon_Hce). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H15a); [ zenon_intro zenon_Hda | zenon_intro zenon_H15b ]. % 3.21/3.44 exact (zenon_Hda zenon_Hcd). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H15b); [ zenon_intro zenon_H15c | zenon_intro zenon_H9b ]. % 3.21/3.44 exact (zenon_H15c zenon_H12a). % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 generalize (zenon_H154 (k3_waybel_1 zenon_TA_fn zenon_TA_fn zenon_TB_fo)). zenon_intro zenon_H15d. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H15d); [ zenon_intro zenon_H15f | zenon_intro zenon_H15e ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H15f); [ zenon_intro zenon_H161 | zenon_intro zenon_H160 ]. % 3.21/3.44 generalize (fc7_waybel_1 zenon_TA_fn). zenon_intro zenon_H162. % 3.21/3.44 generalize (zenon_H162 zenon_TA_fn). zenon_intro zenon_H163. % 3.21/3.44 generalize (zenon_H163 zenon_TB_fo). zenon_intro zenon_H164. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H164); [ zenon_intro zenon_H103 | zenon_intro zenon_H165 ]. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_Haa | zenon_intro zenon_H104 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H104); [ zenon_intro zenon_H9b | zenon_intro zenon_H105 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_Haa | zenon_intro zenon_H106 ]. % 3.21/3.44 apply zenon_Haa. zenon_intro zenon_H98. % 3.21/3.44 apply (zenon_L2_ zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H106); [ zenon_intro zenon_H9b | zenon_intro zenon_H107 ]. % 3.21/3.44 exact (zenon_H9b zenon_H96). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H107); [ zenon_intro zenon_Hb3 | zenon_intro zenon_H108 ]. % 3.21/3.44 exact (zenon_Hb3 zenon_Ha1). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_Hb5 | zenon_intro zenon_H95 ]. % 3.21/3.44 exact (zenon_Hb5 zenon_Ha0). % 3.21/3.44 exact (zenon_H95 zenon_H8d). % 3.21/3.44 apply (zenon_and_s _ _ zenon_H165). zenon_intro zenon_H167. zenon_intro zenon_H166. % 3.21/3.44 apply (zenon_and_s _ _ zenon_H166). zenon_intro zenon_H111. zenon_intro zenon_H168. % 3.21/3.44 exact (zenon_H161 zenon_H111). % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H160); [ zenon_intro zenon_H10b | zenon_intro zenon_H169 ]. % 3.21/3.44 apply (zenon_L11_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 apply (zenon_notand_s _ _ zenon_H169); [ zenon_intro zenon_H16a | zenon_intro zenon_H114 ]. % 3.21/3.44 exact (zenon_H16a zenon_H149). % 3.21/3.44 apply (zenon_L12_ zenon_TA_fn zenon_TB_fo); trivial. % 3.21/3.44 apply (zenon_imply_s _ _ zenon_H15e); [ zenon_intro zenon_H11a | zenon_intro zenon_H13f ]. % 3.21/3.44 apply (zenon_L13_ zenon_TB_fo zenon_TA_fn); trivial. % 3.21/3.44 exact (zenon_H141 zenon_H13f). % 3.21/3.44 exact (zenon_H12f zenon_H140). % 3.21/3.44 Qed. % 3.21/3.44 % SZS output end Proof % 3.21/3.44 (* END-PROOF *) % 3.21/3.44 nodes searched: 142625 % 3.21/3.44 max branch formulas: 12980 % 3.21/3.44 proof nodes created: 3212 % 3.21/3.44 formulas created: 323793 % 3.21/3.44 %------------------------------------------------------------------------------