%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SET773+4 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 06:38:28 EDT 2022 % Result : Theorem 0.89s 1.07s % Output : Proof 0.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET773+4 : TPTP v8.1.0. Released v2.2.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n022.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 : Sun Jul 10 16:30:25 EDT 2022 % 0.12/0.34 % CPUTime : % 0.89/1.07 (* PROOF-FOUND *) % 0.89/1.07 % SZS status Theorem % 0.89/1.07 (* BEGIN-PROOF *) % 0.89/1.07 % SZS output start Proof % 0.89/1.07 Theorem thIII09 : (forall E : zenon_U, (forall R1 : zenon_U, (forall R2 : zenon_U, (forall R : zenon_U, (((equivalence R1 E)/\((equivalence R2 E)/\(forall A : zenon_U, (forall B : zenon_U, (((member A E)/\(member B E))->((apply R A B)<->((apply R1 A B)/\(apply R2 A B))))))))->(equivalence R E)))))). % 0.89/1.07 Proof. % 0.89/1.07 assert (zenon_L1_ : forall (zenon_TY_w : zenon_U) (zenon_TR2_x : zenon_U) (zenon_TR1_y : zenon_U) (zenon_TR_z : zenon_U) (zenon_TE_ba : zenon_U) (zenon_TX_bb : zenon_U), (forall B : zenon_U, (((member zenon_TX_bb zenon_TE_ba)/\(member B zenon_TE_ba))->((apply zenon_TR_z zenon_TX_bb B)<->((apply zenon_TR1_y zenon_TX_bb B)/\(apply zenon_TR2_x zenon_TX_bb B))))) -> (member zenon_TX_bb zenon_TE_ba) -> (member zenon_TY_w zenon_TE_ba) -> (~(apply zenon_TR1_y zenon_TX_bb zenon_TY_w)) -> (apply zenon_TR_z zenon_TX_bb zenon_TY_w) -> False). % 0.89/1.07 do 6 intro. intros zenon_H11 zenon_H12 zenon_H13 zenon_H14 zenon_H15. % 0.89/1.07 generalize (zenon_H11 zenon_TY_w). zenon_intro zenon_H1c. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H1c); [ zenon_intro zenon_H1e | zenon_intro zenon_H1d ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H1e); [ zenon_intro zenon_H20 | zenon_intro zenon_H1f ]. % 0.89/1.07 exact (zenon_H20 zenon_H12). % 0.89/1.07 exact (zenon_H1f zenon_H13). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H1d); [ zenon_intro zenon_H23; zenon_intro zenon_H22 | zenon_intro zenon_H15; zenon_intro zenon_H21 ]. % 0.89/1.07 exact (zenon_H23 zenon_H15). % 0.89/1.07 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 0.89/1.07 exact (zenon_H14 zenon_H25). % 0.89/1.07 (* end of lemma zenon_L1_ *) % 0.89/1.07 apply NNPP. intro zenon_G. % 0.89/1.07 apply (zenon_notallex_s (fun E : zenon_U => (forall R1 : zenon_U, (forall R2 : zenon_U, (forall R : zenon_U, (((equivalence R1 E)/\((equivalence R2 E)/\(forall A : zenon_U, (forall B : zenon_U, (((member A E)/\(member B E))->((apply R A B)<->((apply R1 A B)/\(apply R2 A B))))))))->(equivalence R E)))))) zenon_G); [ zenon_intro zenon_H26; idtac ]. % 0.89/1.07 elim zenon_H26. zenon_intro zenon_TE_ba. zenon_intro zenon_H27. % 0.89/1.07 apply (zenon_notallex_s (fun R1 : zenon_U => (forall R2 : zenon_U, (forall R : zenon_U, (((equivalence R1 zenon_TE_ba)/\((equivalence R2 zenon_TE_ba)/\(forall A : zenon_U, (forall B : zenon_U, (((member A zenon_TE_ba)/\(member B zenon_TE_ba))->((apply R A B)<->((apply R1 A B)/\(apply R2 A B))))))))->(equivalence R zenon_TE_ba))))) zenon_H27); [ zenon_intro zenon_H28; idtac ]. % 0.89/1.07 elim zenon_H28. zenon_intro zenon_TR1_y. zenon_intro zenon_H29. % 0.89/1.07 apply (zenon_notallex_s (fun R2 : zenon_U => (forall R : zenon_U, (((equivalence zenon_TR1_y zenon_TE_ba)/\((equivalence R2 zenon_TE_ba)/\(forall A : zenon_U, (forall B : zenon_U, (((member A zenon_TE_ba)/\(member B zenon_TE_ba))->((apply R A B)<->((apply zenon_TR1_y A B)/\(apply R2 A B))))))))->(equivalence R zenon_TE_ba)))) zenon_H29); [ zenon_intro zenon_H2a; idtac ]. % 0.89/1.07 elim zenon_H2a. zenon_intro zenon_TR2_x. zenon_intro zenon_H2b. % 0.89/1.07 apply (zenon_notallex_s (fun R : zenon_U => (((equivalence zenon_TR1_y zenon_TE_ba)/\((equivalence zenon_TR2_x zenon_TE_ba)/\(forall A : zenon_U, (forall B : zenon_U, (((member A zenon_TE_ba)/\(member B zenon_TE_ba))->((apply R A B)<->((apply zenon_TR1_y A B)/\(apply zenon_TR2_x A B))))))))->(equivalence R zenon_TE_ba))) zenon_H2b); [ zenon_intro zenon_H2c; idtac ]. % 0.89/1.07 elim zenon_H2c. zenon_intro zenon_TR_z. zenon_intro zenon_H2d. % 0.89/1.07 apply (zenon_notimply_s _ _ zenon_H2d). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 0.89/1.07 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H31. zenon_intro zenon_H30. % 0.89/1.07 apply (zenon_and_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 0.89/1.07 generalize (equivalence zenon_TE_ba). zenon_intro zenon_H34. % 0.89/1.07 generalize (zenon_H34 zenon_TR1_y). zenon_intro zenon_H35. % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H35); [ zenon_intro zenon_H38; zenon_intro zenon_H37 | zenon_intro zenon_H31; zenon_intro zenon_H36 ]. % 0.89/1.07 exact (zenon_H38 zenon_H31). % 0.89/1.07 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H3a. zenon_intro zenon_H39. % 0.89/1.07 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H3c. zenon_intro zenon_H3b. % 0.89/1.07 generalize (equivalence zenon_TE_ba). zenon_intro zenon_H34. % 0.89/1.07 generalize (zenon_H34 zenon_TR2_x). zenon_intro zenon_H3d. % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H3d); [ zenon_intro zenon_H40; zenon_intro zenon_H3f | zenon_intro zenon_H33; zenon_intro zenon_H3e ]. % 0.89/1.07 exact (zenon_H40 zenon_H33). % 0.89/1.07 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H42. zenon_intro zenon_H41. % 0.89/1.07 apply (zenon_and_s _ _ zenon_H41). zenon_intro zenon_H44. zenon_intro zenon_H43. % 0.89/1.07 generalize (equivalence zenon_TE_ba). zenon_intro zenon_H34. % 0.89/1.07 generalize (zenon_H34 zenon_TR_z). zenon_intro zenon_H45. % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H45); [ zenon_intro zenon_H2e; zenon_intro zenon_H48 | zenon_intro zenon_H47; zenon_intro zenon_H46 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H4a | zenon_intro zenon_H49 ]. % 0.89/1.07 apply (zenon_notallex_s (fun X : zenon_U => ((member X zenon_TE_ba)->(apply zenon_TR_z X X))) zenon_H4a); [ zenon_intro zenon_H4b; idtac ]. % 0.89/1.07 elim zenon_H4b. zenon_intro zenon_TX_cy. zenon_intro zenon_H4d. % 0.89/1.07 apply (zenon_notimply_s _ _ zenon_H4d). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 0.89/1.07 generalize (zenon_H32 zenon_TX_cy). zenon_intro zenon_H50. % 0.89/1.07 generalize (zenon_H42 zenon_TX_cy). zenon_intro zenon_H51. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 0.89/1.07 exact (zenon_H53 zenon_H4f). % 0.89/1.07 generalize (zenon_H50 zenon_TX_cy). zenon_intro zenon_H54. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H54); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_H53 | zenon_intro zenon_H53 ]. % 0.89/1.07 exact (zenon_H53 zenon_H4f). % 0.89/1.07 exact (zenon_H53 zenon_H4f). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H55); [ zenon_intro zenon_H4e; zenon_intro zenon_H59 | zenon_intro zenon_H58; zenon_intro zenon_H57 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H59); [ zenon_intro zenon_H5b | zenon_intro zenon_H5a ]. % 0.89/1.07 generalize (zenon_H3a zenon_TX_cy). zenon_intro zenon_H5c. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H5c); [ zenon_intro zenon_H53 | zenon_intro zenon_H5d ]. % 0.89/1.07 exact (zenon_H53 zenon_H4f). % 0.89/1.07 exact (zenon_H5b zenon_H5d). % 0.89/1.07 exact (zenon_H5a zenon_H52). % 0.89/1.07 exact (zenon_H4e zenon_H58). % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H5f | zenon_intro zenon_H5e ]. % 0.89/1.07 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (((member X zenon_TE_ba)/\(member Y zenon_TE_ba))->((apply zenon_TR_z X Y)->(apply zenon_TR_z Y X))))) zenon_H5f); [ zenon_intro zenon_H60; idtac ]. % 0.89/1.07 elim zenon_H60. zenon_intro zenon_TX_dt. zenon_intro zenon_H62. % 0.89/1.07 apply (zenon_notallex_s (fun Y : zenon_U => (((member zenon_TX_dt zenon_TE_ba)/\(member Y zenon_TE_ba))->((apply zenon_TR_z zenon_TX_dt Y)->(apply zenon_TR_z Y zenon_TX_dt)))) zenon_H62); [ zenon_intro zenon_H63; idtac ]. % 0.89/1.07 elim zenon_H63. zenon_intro zenon_TY_dw. zenon_intro zenon_H65. % 0.89/1.07 apply (zenon_notimply_s _ _ zenon_H65). zenon_intro zenon_H67. zenon_intro zenon_H66. % 0.89/1.07 apply (zenon_notimply_s _ _ zenon_H66). zenon_intro zenon_H69. zenon_intro zenon_H68. % 0.89/1.07 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6b. zenon_intro zenon_H6a. % 0.89/1.07 generalize (zenon_H32 zenon_TY_dw). zenon_intro zenon_H6c. % 0.89/1.07 generalize (zenon_H6c zenon_TX_dt). zenon_intro zenon_H6d. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H6f); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 0.89/1.07 exact (zenon_H71 zenon_H6a). % 0.89/1.07 exact (zenon_H70 zenon_H6b). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H6e); [ zenon_intro zenon_H68; zenon_intro zenon_H74 | zenon_intro zenon_H73; zenon_intro zenon_H72 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H74); [ zenon_intro zenon_H76 | zenon_intro zenon_H75 ]. % 0.89/1.07 generalize (zenon_H3c zenon_TX_dt). zenon_intro zenon_H77. % 0.89/1.07 generalize (zenon_H77 zenon_TY_dw). zenon_intro zenon_H78. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H78); [ zenon_intro zenon_H7a | zenon_intro zenon_H79 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H70 | zenon_intro zenon_H71 ]. % 0.89/1.07 exact (zenon_H70 zenon_H6b). % 0.89/1.07 exact (zenon_H71 zenon_H6a). % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H79); [ zenon_intro zenon_H7c | zenon_intro zenon_H7b ]. % 0.89/1.07 generalize (zenon_H32 zenon_TX_dt). zenon_intro zenon_H7d. % 0.89/1.07 generalize (zenon_H7d zenon_TY_dw). zenon_intro zenon_H7e. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H7a | zenon_intro zenon_H7f ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H70 | zenon_intro zenon_H71 ]. % 0.89/1.07 exact (zenon_H70 zenon_H6b). % 0.89/1.07 exact (zenon_H71 zenon_H6a). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H7f); [ zenon_intro zenon_H82; zenon_intro zenon_H81 | zenon_intro zenon_H69; zenon_intro zenon_H80 ]. % 0.89/1.07 exact (zenon_H82 zenon_H69). % 0.89/1.07 apply (zenon_and_s _ _ zenon_H80). zenon_intro zenon_H84. zenon_intro zenon_H83. % 0.89/1.07 exact (zenon_H7c zenon_H84). % 0.89/1.07 exact (zenon_H76 zenon_H7b). % 0.89/1.07 generalize (zenon_H44 zenon_TX_dt). zenon_intro zenon_H85. % 0.89/1.07 generalize (zenon_H85 zenon_TY_dw). zenon_intro zenon_H86. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H86); [ zenon_intro zenon_H7a | zenon_intro zenon_H87 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H70 | zenon_intro zenon_H71 ]. % 0.89/1.07 exact (zenon_H70 zenon_H6b). % 0.89/1.07 exact (zenon_H71 zenon_H6a). % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.89/1.07 generalize (zenon_H32 zenon_TX_dt). zenon_intro zenon_H7d. % 0.89/1.07 generalize (zenon_H7d zenon_TY_dw). zenon_intro zenon_H7e. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H7a | zenon_intro zenon_H7f ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H70 | zenon_intro zenon_H71 ]. % 0.89/1.07 exact (zenon_H70 zenon_H6b). % 0.89/1.07 exact (zenon_H71 zenon_H6a). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H7f); [ zenon_intro zenon_H82; zenon_intro zenon_H81 | zenon_intro zenon_H69; zenon_intro zenon_H80 ]. % 0.89/1.07 exact (zenon_H82 zenon_H69). % 0.89/1.07 apply (zenon_and_s _ _ zenon_H80). zenon_intro zenon_H84. zenon_intro zenon_H83. % 0.89/1.07 exact (zenon_H89 zenon_H83). % 0.89/1.07 exact (zenon_H75 zenon_H88). % 0.89/1.07 exact (zenon_H68 zenon_H73). % 0.89/1.07 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (forall Z : zenon_U, (((member X zenon_TE_ba)/\((member Y zenon_TE_ba)/\(member Z zenon_TE_ba)))->(((apply zenon_TR_z X Y)/\(apply zenon_TR_z Y Z))->(apply zenon_TR_z X Z)))))) zenon_H5e); [ zenon_intro zenon_H8a; idtac ]. % 0.89/1.07 elim zenon_H8a. zenon_intro zenon_TX_bb. zenon_intro zenon_H8b. % 0.89/1.07 apply (zenon_notallex_s (fun Y : zenon_U => (forall Z : zenon_U, (((member zenon_TX_bb zenon_TE_ba)/\((member Y zenon_TE_ba)/\(member Z zenon_TE_ba)))->(((apply zenon_TR_z zenon_TX_bb Y)/\(apply zenon_TR_z Y Z))->(apply zenon_TR_z zenon_TX_bb Z))))) zenon_H8b); [ zenon_intro zenon_H8c; idtac ]. % 0.89/1.07 elim zenon_H8c. zenon_intro zenon_TY_w. zenon_intro zenon_H8d. % 0.89/1.07 apply (zenon_notallex_s (fun Z : zenon_U => (((member zenon_TX_bb zenon_TE_ba)/\((member zenon_TY_w zenon_TE_ba)/\(member Z zenon_TE_ba)))->(((apply zenon_TR_z zenon_TX_bb zenon_TY_w)/\(apply zenon_TR_z zenon_TY_w Z))->(apply zenon_TR_z zenon_TX_bb Z)))) zenon_H8d); [ zenon_intro zenon_H8e; idtac ]. % 0.89/1.07 elim zenon_H8e. zenon_intro zenon_TZ_fn. zenon_intro zenon_H90. % 0.89/1.07 apply (zenon_notimply_s _ _ zenon_H90). zenon_intro zenon_H92. zenon_intro zenon_H91. % 0.89/1.07 apply (zenon_notimply_s _ _ zenon_H91). zenon_intro zenon_H94. zenon_intro zenon_H93. % 0.89/1.07 apply (zenon_and_s _ _ zenon_H94). zenon_intro zenon_H15. zenon_intro zenon_H95. % 0.89/1.07 apply (zenon_and_s _ _ zenon_H92). zenon_intro zenon_H12. zenon_intro zenon_H96. % 0.89/1.07 apply (zenon_and_s _ _ zenon_H96). zenon_intro zenon_H13. zenon_intro zenon_H97. % 0.89/1.07 generalize (zenon_H32 zenon_TX_bb). zenon_intro zenon_H11. % 0.89/1.07 generalize (zenon_H11 zenon_TZ_fn). zenon_intro zenon_H98. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H98); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H9a); [ zenon_intro zenon_H20 | zenon_intro zenon_H9b ]. % 0.89/1.07 exact (zenon_H20 zenon_H12). % 0.89/1.07 exact (zenon_H9b zenon_H97). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H99); [ zenon_intro zenon_H93; zenon_intro zenon_H9e | zenon_intro zenon_H9d; zenon_intro zenon_H9c ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H9e); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H9f ]. % 0.89/1.07 generalize (zenon_H3b zenon_TX_bb). zenon_intro zenon_Ha1. % 0.89/1.07 generalize (zenon_Ha1 zenon_TY_w). zenon_intro zenon_Ha2. % 0.89/1.07 generalize (zenon_Ha2 zenon_TZ_fn). zenon_intro zenon_Ha3. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_H20 | zenon_intro zenon_Ha6 ]. % 0.89/1.07 exact (zenon_H20 zenon_H12). % 0.89/1.07 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_H1f | zenon_intro zenon_H9b ]. % 0.89/1.07 exact (zenon_H1f zenon_H13). % 0.89/1.07 exact (zenon_H9b zenon_H97). % 0.89/1.07 apply (zenon_imply_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha8 | zenon_intro zenon_Ha7 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_Ha8); [ zenon_intro zenon_H14 | zenon_intro zenon_Ha9 ]. % 0.89/1.07 apply (zenon_L1_ zenon_TY_w zenon_TR2_x zenon_TR1_y zenon_TR_z zenon_TE_ba zenon_TX_bb); trivial. % 0.89/1.07 generalize (zenon_H32 zenon_TY_w). zenon_intro zenon_Haa. % 0.89/1.07 generalize (zenon_Haa zenon_TZ_fn). zenon_intro zenon_Hab. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_Hab); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Hac ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_H1f | zenon_intro zenon_H9b ]. % 0.89/1.07 exact (zenon_H1f zenon_H13). % 0.89/1.07 exact (zenon_H9b zenon_H97). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_Hac); [ zenon_intro zenon_Haf; zenon_intro zenon_Hae | zenon_intro zenon_H95; zenon_intro zenon_Had ]. % 0.89/1.07 exact (zenon_Haf zenon_H95). % 0.89/1.07 apply (zenon_and_s _ _ zenon_Had). zenon_intro zenon_Hb1. zenon_intro zenon_Hb0. % 0.89/1.07 exact (zenon_Ha9 zenon_Hb1). % 0.89/1.07 exact (zenon_Ha0 zenon_Ha7). % 0.89/1.07 generalize (zenon_H43 zenon_TX_bb). zenon_intro zenon_Hb2. % 0.89/1.07 generalize (zenon_Hb2 zenon_TY_w). zenon_intro zenon_Hb3. % 0.89/1.07 generalize (zenon_Hb3 zenon_TZ_fn). zenon_intro zenon_Hb4. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_Hb4); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Hb5 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_H20 | zenon_intro zenon_Ha6 ]. % 0.89/1.07 exact (zenon_H20 zenon_H12). % 0.89/1.07 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_H1f | zenon_intro zenon_H9b ]. % 0.89/1.07 exact (zenon_H1f zenon_H13). % 0.89/1.07 exact (zenon_H9b zenon_H97). % 0.89/1.07 apply (zenon_imply_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_Hb7); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 0.89/1.07 generalize (zenon_H11 zenon_TY_w). zenon_intro zenon_H1c. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_H1c); [ zenon_intro zenon_H1e | zenon_intro zenon_H1d ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_H1e); [ zenon_intro zenon_H20 | zenon_intro zenon_H1f ]. % 0.89/1.07 exact (zenon_H20 zenon_H12). % 0.89/1.07 exact (zenon_H1f zenon_H13). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_H1d); [ zenon_intro zenon_H23; zenon_intro zenon_H22 | zenon_intro zenon_H15; zenon_intro zenon_H21 ]. % 0.89/1.07 exact (zenon_H23 zenon_H15). % 0.89/1.07 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 0.89/1.07 exact (zenon_Hb9 zenon_H24). % 0.89/1.07 generalize (zenon_H32 zenon_TY_w). zenon_intro zenon_Haa. % 0.89/1.07 generalize (zenon_Haa zenon_TZ_fn). zenon_intro zenon_Hab. % 0.89/1.07 apply (zenon_imply_s _ _ zenon_Hab); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Hac ]. % 0.89/1.07 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_H1f | zenon_intro zenon_H9b ]. % 0.89/1.07 exact (zenon_H1f zenon_H13). % 0.89/1.07 exact (zenon_H9b zenon_H97). % 0.89/1.07 apply (zenon_equiv_s _ _ zenon_Hac); [ zenon_intro zenon_Haf; zenon_intro zenon_Hae | zenon_intro zenon_H95; zenon_intro zenon_Had ]. % 0.89/1.07 exact (zenon_Haf zenon_H95). % 0.89/1.07 apply (zenon_and_s _ _ zenon_Had). zenon_intro zenon_Hb1. zenon_intro zenon_Hb0. % 0.89/1.07 exact (zenon_Hb8 zenon_Hb0). % 0.89/1.07 exact (zenon_H9f zenon_Hb6). % 0.89/1.07 exact (zenon_H93 zenon_H9d). % 0.89/1.07 exact (zenon_H2e zenon_H47). % 0.89/1.07 Qed. % 0.89/1.07 % SZS output end Proof % 0.89/1.07 (* END-PROOF *) % 0.89/1.07 nodes searched: 15339 % 0.89/1.07 max branch formulas: 2144 % 0.89/1.07 proof nodes created: 982 % 0.89/1.07 formulas created: 68459 % 0.89/1.07 %------------------------------------------------------------------------------