%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SET765+4 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n028.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:25 EDT 2022 % Result : Theorem 0.69s 0.84s % Output : Proof 0.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET765+4 : TPTP v8.1.0. Released v2.2.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon Jul 11 01:05:28 EDT 2022 % 0.13/0.33 % CPUTime : % 0.69/0.84 (* PROOF-FOUND *) % 0.69/0.84 % SZS status Theorem % 0.69/0.84 (* BEGIN-PROOF *) % 0.69/0.84 % SZS output start Proof % 0.69/0.84 Theorem thIII01 : (forall E : zenon_U, (forall R : zenon_U, (forall X : zenon_U, (((equivalence R E)/\(subset X E))->(equivalence R X))))). % 0.69/0.84 Proof. % 0.69/0.84 assert (zenon_L1_ : forall (zenon_TX_u : zenon_U) (zenon_TE_v : zenon_U) (zenon_TX_w : zenon_U), (forall X : zenon_U, ((member X zenon_TX_w)->(member X zenon_TE_v))) -> (member zenon_TX_u zenon_TX_w) -> (~(member zenon_TX_u zenon_TE_v)) -> False). % 0.69/0.84 do 3 intro. intros zenon_H11 zenon_H12 zenon_H13. % 0.69/0.84 generalize (zenon_H11 zenon_TX_u). zenon_intro zenon_H17. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H17); [ zenon_intro zenon_H19 | zenon_intro zenon_H18 ]. % 0.69/0.84 exact (zenon_H19 zenon_H12). % 0.69/0.84 exact (zenon_H13 zenon_H18). % 0.69/0.84 (* end of lemma zenon_L1_ *) % 0.69/0.84 assert (zenon_L2_ : forall (zenon_TY_bc : zenon_U) (zenon_TE_v : zenon_U) (zenon_TX_w : zenon_U), (forall X : zenon_U, ((member X zenon_TX_w)->(member X zenon_TE_v))) -> (member zenon_TY_bc zenon_TX_w) -> (~(member zenon_TY_bc zenon_TE_v)) -> False). % 0.69/0.84 do 3 intro. intros zenon_H11 zenon_H1a zenon_H1b. % 0.69/0.84 generalize (zenon_H11 zenon_TY_bc). zenon_intro zenon_H1d. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H1d); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 0.69/0.84 exact (zenon_H1f zenon_H1a). % 0.69/0.84 exact (zenon_H1b zenon_H1e). % 0.69/0.84 (* end of lemma zenon_L2_ *) % 0.69/0.84 assert (zenon_L3_ : forall (zenon_TZ_bi : zenon_U) (zenon_TE_v : zenon_U) (zenon_TX_w : zenon_U), (forall X : zenon_U, ((member X zenon_TX_w)->(member X zenon_TE_v))) -> (member zenon_TZ_bi zenon_TX_w) -> (~(member zenon_TZ_bi zenon_TE_v)) -> False). % 0.69/0.84 do 3 intro. intros zenon_H11 zenon_H20 zenon_H21. % 0.69/0.84 generalize (zenon_H11 zenon_TZ_bi). zenon_intro zenon_H23. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H23); [ zenon_intro zenon_H25 | zenon_intro zenon_H24 ]. % 0.69/0.84 exact (zenon_H25 zenon_H20). % 0.69/0.84 exact (zenon_H21 zenon_H24). % 0.69/0.84 (* end of lemma zenon_L3_ *) % 0.69/0.84 assert (zenon_L4_ : forall (zenon_TY_bo : zenon_U) (zenon_TE_v : zenon_U) (zenon_TX_w : zenon_U), (forall X : zenon_U, ((member X zenon_TX_w)->(member X zenon_TE_v))) -> (member zenon_TY_bo zenon_TX_w) -> (~(member zenon_TY_bo zenon_TE_v)) -> False). % 0.69/0.84 do 3 intro. intros zenon_H11 zenon_H26 zenon_H27. % 0.69/0.84 generalize (zenon_H11 zenon_TY_bo). zenon_intro zenon_H29. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H29); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 0.69/0.84 exact (zenon_H2b zenon_H26). % 0.69/0.84 exact (zenon_H27 zenon_H2a). % 0.69/0.84 (* end of lemma zenon_L4_ *) % 0.69/0.84 assert (zenon_L5_ : forall (zenon_TR_by : zenon_U) (zenon_TZ_bi : zenon_U) (zenon_TX_bz : zenon_U) (zenon_TE_v : zenon_U) (zenon_TY_bo : zenon_U), (~(~(member zenon_TY_bo zenon_TE_v))) -> (member zenon_TX_bz zenon_TE_v) -> (member zenon_TZ_bi zenon_TE_v) -> (apply zenon_TR_by zenon_TX_bz zenon_TY_bo) -> (apply zenon_TR_by zenon_TY_bo zenon_TZ_bi) -> (~(apply zenon_TR_by zenon_TX_bz zenon_TZ_bi)) -> (forall Y : zenon_U, (forall Z : zenon_U, (((member zenon_TX_bz zenon_TE_v)/\((member Y zenon_TE_v)/\(member Z zenon_TE_v)))->(((apply zenon_TR_by zenon_TX_bz Y)/\(apply zenon_TR_by Y Z))->(apply zenon_TR_by zenon_TX_bz Z))))) -> False). % 0.69/0.84 do 5 intro. intros zenon_H2c zenon_H2d zenon_H24 zenon_H2e zenon_H2f zenon_H30 zenon_H31. % 0.69/0.84 apply zenon_H2c. zenon_intro zenon_H2a. % 0.69/0.84 generalize (zenon_H31 zenon_TY_bo). zenon_intro zenon_H34. % 0.69/0.84 generalize (zenon_H34 zenon_TZ_bi). zenon_intro zenon_H35. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 0.69/0.84 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H39 | zenon_intro zenon_H38 ]. % 0.69/0.84 exact (zenon_H39 zenon_H2d). % 0.69/0.84 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H27 | zenon_intro zenon_H21 ]. % 0.69/0.84 exact (zenon_H27 zenon_H2a). % 0.69/0.84 exact (zenon_H21 zenon_H24). % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H36); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 0.69/0.84 apply (zenon_notand_s _ _ zenon_H3b); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 0.69/0.84 exact (zenon_H3d zenon_H2e). % 0.69/0.84 exact (zenon_H3c zenon_H2f). % 0.69/0.84 exact (zenon_H30 zenon_H3a). % 0.69/0.84 (* end of lemma zenon_L5_ *) % 0.69/0.84 assert (zenon_L6_ : forall (zenon_TR_by : zenon_U) (zenon_TX_bz : zenon_U) (zenon_TX_w : zenon_U) (zenon_TY_bo : zenon_U) (zenon_TE_v : zenon_U) (zenon_TZ_bi : zenon_U), (~(~(member zenon_TZ_bi zenon_TE_v))) -> (forall A : zenon_U, (forall E : zenon_U, ((member zenon_TY_bo (difference E A))<->((member zenon_TY_bo E)/\(~(member zenon_TY_bo A)))))) -> (forall X : zenon_U, ((member X zenon_TX_w)->(member X zenon_TE_v))) -> (member zenon_TY_bo zenon_TX_w) -> (member zenon_TX_bz zenon_TE_v) -> (apply zenon_TR_by zenon_TX_bz zenon_TY_bo) -> (apply zenon_TR_by zenon_TY_bo zenon_TZ_bi) -> (~(apply zenon_TR_by zenon_TX_bz zenon_TZ_bi)) -> (forall X : zenon_U, (forall Y : zenon_U, (forall Z : zenon_U, (((member X zenon_TE_v)/\((member Y zenon_TE_v)/\(member Z zenon_TE_v)))->(((apply zenon_TR_by X Y)/\(apply zenon_TR_by Y Z))->(apply zenon_TR_by X Z)))))) -> False). % 0.69/0.84 do 6 intro. intros zenon_H3e zenon_H3f zenon_H11 zenon_H26 zenon_H2d zenon_H2e zenon_H2f zenon_H30 zenon_H40. % 0.69/0.84 apply zenon_H3e. zenon_intro zenon_H24. % 0.69/0.84 generalize (zenon_H40 zenon_TX_bz). zenon_intro zenon_H31. % 0.69/0.84 generalize (zenon_H3f zenon_TE_v). zenon_intro zenon_H41. % 0.69/0.84 generalize (zenon_H41 zenon_TE_v). zenon_intro zenon_H42. % 0.69/0.84 apply (zenon_equiv_s _ _ zenon_H42); [ zenon_intro zenon_H46; zenon_intro zenon_H45 | zenon_intro zenon_H44; zenon_intro zenon_H43 ]. % 0.69/0.84 apply (zenon_notand_s _ _ zenon_H45); [ zenon_intro zenon_H27 | zenon_intro zenon_H2c ]. % 0.69/0.84 apply (zenon_L4_ zenon_TY_bo zenon_TE_v zenon_TX_w); trivial. % 0.69/0.84 apply (zenon_L5_ zenon_TR_by zenon_TZ_bi zenon_TX_bz zenon_TE_v zenon_TY_bo); trivial. % 0.69/0.84 apply (zenon_and_s _ _ zenon_H43). zenon_intro zenon_H2a. zenon_intro zenon_H27. % 0.69/0.84 exact (zenon_H27 zenon_H2a). % 0.69/0.84 (* end of lemma zenon_L6_ *) % 0.69/0.84 assert (zenon_L7_ : forall (zenon_TX_w : zenon_U) (zenon_TY_bo : zenon_U) (zenon_TZ_bi : zenon_U) (zenon_TR_by : zenon_U) (zenon_TE_v : zenon_U) (zenon_TX_bz : zenon_U), (~(~(member zenon_TX_bz zenon_TE_v))) -> (forall X : zenon_U, (forall Y : zenon_U, (forall Z : zenon_U, (((member X zenon_TE_v)/\((member Y zenon_TE_v)/\(member Z zenon_TE_v)))->(((apply zenon_TR_by X Y)/\(apply zenon_TR_by Y Z))->(apply zenon_TR_by X Z)))))) -> (~(apply zenon_TR_by zenon_TX_bz zenon_TZ_bi)) -> (apply zenon_TR_by zenon_TY_bo zenon_TZ_bi) -> (apply zenon_TR_by zenon_TX_bz zenon_TY_bo) -> (member zenon_TY_bo zenon_TX_w) -> (forall A : zenon_U, (forall E : zenon_U, ((member zenon_TY_bo (difference E A))<->((member zenon_TY_bo E)/\(~(member zenon_TY_bo A)))))) -> (member zenon_TZ_bi zenon_TX_w) -> (forall X : zenon_U, ((member X zenon_TX_w)->(member X zenon_TE_v))) -> (forall A : zenon_U, (forall E : zenon_U, ((member zenon_TZ_bi (difference E A))<->((member zenon_TZ_bi E)/\(~(member zenon_TZ_bi A)))))) -> False). % 0.69/0.84 do 6 intro. intros zenon_H47 zenon_H40 zenon_H30 zenon_H2f zenon_H2e zenon_H26 zenon_H3f zenon_H20 zenon_H11 zenon_H48. % 0.69/0.84 apply zenon_H47. zenon_intro zenon_H2d. % 0.69/0.84 generalize (zenon_H48 zenon_TE_v). zenon_intro zenon_H49. % 0.69/0.84 generalize (zenon_H49 zenon_TE_v). zenon_intro zenon_H4a. % 0.69/0.84 apply (zenon_equiv_s _ _ zenon_H4a); [ zenon_intro zenon_H4e; zenon_intro zenon_H4d | zenon_intro zenon_H4c; zenon_intro zenon_H4b ]. % 0.69/0.84 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H21 | zenon_intro zenon_H3e ]. % 0.69/0.84 apply (zenon_L3_ zenon_TZ_bi zenon_TE_v zenon_TX_w); trivial. % 0.69/0.84 apply (zenon_L6_ zenon_TR_by zenon_TX_bz zenon_TX_w zenon_TY_bo zenon_TE_v zenon_TZ_bi); trivial. % 0.69/0.84 apply (zenon_and_s _ _ zenon_H4b). zenon_intro zenon_H24. zenon_intro zenon_H21. % 0.69/0.84 exact (zenon_H21 zenon_H24). % 0.69/0.84 (* end of lemma zenon_L7_ *) % 0.69/0.84 assert (zenon_L8_ : forall (zenon_TX_bz : zenon_U) (zenon_TE_v : zenon_U) (zenon_TX_w : zenon_U), (forall X : zenon_U, ((member X zenon_TX_w)->(member X zenon_TE_v))) -> (member zenon_TX_bz zenon_TX_w) -> (~(member zenon_TX_bz zenon_TE_v)) -> False). % 0.69/0.84 do 3 intro. intros zenon_H11 zenon_H4f zenon_H39. % 0.69/0.84 generalize (zenon_H11 zenon_TX_bz). zenon_intro zenon_H50. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H50); [ zenon_intro zenon_H51 | zenon_intro zenon_H2d ]. % 0.69/0.84 exact (zenon_H51 zenon_H4f). % 0.69/0.84 exact (zenon_H39 zenon_H2d). % 0.69/0.84 (* end of lemma zenon_L8_ *) % 0.69/0.84 apply NNPP. intro zenon_G. % 0.69/0.84 apply (zenon_notallex_s (fun E : zenon_U => (forall R : zenon_U, (forall X : zenon_U, (((equivalence R E)/\(subset X E))->(equivalence R X))))) zenon_G); [ zenon_intro zenon_H52; idtac ]. % 0.69/0.84 elim zenon_H52. zenon_intro zenon_TE_v. zenon_intro zenon_H53. % 0.69/0.84 apply (zenon_notallex_s (fun R : zenon_U => (forall X : zenon_U, (((equivalence R zenon_TE_v)/\(subset X zenon_TE_v))->(equivalence R X)))) zenon_H53); [ zenon_intro zenon_H54; idtac ]. % 0.69/0.84 elim zenon_H54. zenon_intro zenon_TR_by. zenon_intro zenon_H55. % 0.69/0.84 apply (zenon_notallex_s (fun X : zenon_U => (((equivalence zenon_TR_by zenon_TE_v)/\(subset X zenon_TE_v))->(equivalence zenon_TR_by X))) zenon_H55); [ zenon_intro zenon_H56; idtac ]. % 0.69/0.84 elim zenon_H56. zenon_intro zenon_TX_w. zenon_intro zenon_H57. % 0.69/0.84 apply (zenon_notimply_s _ _ zenon_H57). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.69/0.84 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5b. zenon_intro zenon_H5a. % 0.69/0.84 generalize (equivalence zenon_TE_v). zenon_intro zenon_H5c. % 0.69/0.84 generalize (zenon_H5c zenon_TR_by). zenon_intro zenon_H5d. % 0.69/0.84 apply (zenon_equiv_s _ _ zenon_H5d); [ zenon_intro zenon_H60; zenon_intro zenon_H5f | zenon_intro zenon_H5b; zenon_intro zenon_H5e ]. % 0.69/0.84 exact (zenon_H60 zenon_H5b). % 0.69/0.84 apply (zenon_and_s _ _ zenon_H5e). zenon_intro zenon_H62. zenon_intro zenon_H61. % 0.69/0.84 apply (zenon_and_s _ _ zenon_H61). zenon_intro zenon_H63. zenon_intro zenon_H40. % 0.69/0.84 generalize (subset zenon_TX_w). zenon_intro zenon_H64. % 0.69/0.84 generalize (zenon_H64 zenon_TE_v). zenon_intro zenon_H65. % 0.69/0.84 apply (zenon_equiv_s _ _ zenon_H65); [ zenon_intro zenon_H67; zenon_intro zenon_H66 | zenon_intro zenon_H5a; zenon_intro zenon_H11 ]. % 0.69/0.84 exact (zenon_H67 zenon_H5a). % 0.69/0.84 generalize (equivalence zenon_TX_w). zenon_intro zenon_H68. % 0.69/0.84 generalize (zenon_H68 zenon_TR_by). zenon_intro zenon_H69. % 0.69/0.84 apply (zenon_equiv_s _ _ zenon_H69); [ zenon_intro zenon_H58; zenon_intro zenon_H6c | zenon_intro zenon_H6b; zenon_intro zenon_H6a ]. % 0.69/0.84 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 0.69/0.84 apply (zenon_notallex_s (fun X : zenon_U => ((member X zenon_TX_w)->(apply zenon_TR_by X X))) zenon_H6e); [ zenon_intro zenon_H6f; idtac ]. % 0.69/0.84 elim zenon_H6f. zenon_intro zenon_TX_ei. zenon_intro zenon_H71. % 0.69/0.84 apply (zenon_notimply_s _ _ zenon_H71). zenon_intro zenon_H73. zenon_intro zenon_H72. % 0.69/0.84 generalize (zenon_H62 zenon_TX_ei). zenon_intro zenon_H74. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H74); [ zenon_intro zenon_H76 | zenon_intro zenon_H75 ]. % 0.69/0.84 generalize (zenon_H11 zenon_TX_ei). zenon_intro zenon_H77. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H77); [ zenon_intro zenon_H79 | zenon_intro zenon_H78 ]. % 0.69/0.84 exact (zenon_H79 zenon_H73). % 0.69/0.84 exact (zenon_H76 zenon_H78). % 0.69/0.84 exact (zenon_H72 zenon_H75). % 0.69/0.84 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 0.69/0.84 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (((member X zenon_TX_w)/\(member Y zenon_TX_w))->((apply zenon_TR_by X Y)->(apply zenon_TR_by Y X))))) zenon_H7b); [ zenon_intro zenon_H7c; idtac ]. % 0.69/0.84 elim zenon_H7c. zenon_intro zenon_TX_u. zenon_intro zenon_H7d. % 0.69/0.84 apply (zenon_notallex_s (fun Y : zenon_U => (((member zenon_TX_u zenon_TX_w)/\(member Y zenon_TX_w))->((apply zenon_TR_by zenon_TX_u Y)->(apply zenon_TR_by Y zenon_TX_u)))) zenon_H7d); [ zenon_intro zenon_H7e; idtac ]. % 0.69/0.84 elim zenon_H7e. zenon_intro zenon_TY_bc. zenon_intro zenon_H7f. % 0.69/0.84 apply (zenon_notimply_s _ _ zenon_H7f). zenon_intro zenon_H81. zenon_intro zenon_H80. % 0.69/0.84 apply (zenon_notimply_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 0.69/0.84 apply (zenon_and_s _ _ zenon_H81). zenon_intro zenon_H12. zenon_intro zenon_H1a. % 0.69/0.84 generalize (zenon_H63 zenon_TX_u). zenon_intro zenon_H84. % 0.69/0.84 generalize (zenon_H84 zenon_TY_bc). zenon_intro zenon_H85. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H85); [ zenon_intro zenon_H87 | zenon_intro zenon_H86 ]. % 0.69/0.84 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H13 | zenon_intro zenon_H1b ]. % 0.69/0.84 apply (zenon_L1_ zenon_TX_u zenon_TE_v zenon_TX_w); trivial. % 0.69/0.84 apply (zenon_L2_ zenon_TY_bc zenon_TE_v zenon_TX_w); trivial. % 0.69/0.84 apply (zenon_imply_s _ _ zenon_H86); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.69/0.84 exact (zenon_H89 zenon_H83). % 0.69/0.84 exact (zenon_H82 zenon_H88). % 0.69/0.84 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (forall Z : zenon_U, (((member X zenon_TX_w)/\((member Y zenon_TX_w)/\(member Z zenon_TX_w)))->(((apply zenon_TR_by X Y)/\(apply zenon_TR_by Y Z))->(apply zenon_TR_by X Z)))))) zenon_H7a); [ zenon_intro zenon_H8a; idtac ]. % 0.69/0.85 elim zenon_H8a. zenon_intro zenon_TX_bz. zenon_intro zenon_H8b. % 0.69/0.85 apply (zenon_notallex_s (fun Y : zenon_U => (forall Z : zenon_U, (((member zenon_TX_bz zenon_TX_w)/\((member Y zenon_TX_w)/\(member Z zenon_TX_w)))->(((apply zenon_TR_by zenon_TX_bz Y)/\(apply zenon_TR_by Y Z))->(apply zenon_TR_by zenon_TX_bz Z))))) zenon_H8b); [ zenon_intro zenon_H8c; idtac ]. % 0.69/0.85 elim zenon_H8c. zenon_intro zenon_TY_bo. zenon_intro zenon_H8d. % 0.69/0.85 apply (zenon_notallex_s (fun Z : zenon_U => (((member zenon_TX_bz zenon_TX_w)/\((member zenon_TY_bo zenon_TX_w)/\(member Z zenon_TX_w)))->(((apply zenon_TR_by zenon_TX_bz zenon_TY_bo)/\(apply zenon_TR_by zenon_TY_bo Z))->(apply zenon_TR_by zenon_TX_bz Z)))) zenon_H8d); [ zenon_intro zenon_H8e; idtac ]. % 0.69/0.85 elim zenon_H8e. zenon_intro zenon_TZ_bi. zenon_intro zenon_H8f. % 0.69/0.85 apply (zenon_notimply_s _ _ zenon_H8f). zenon_intro zenon_H91. zenon_intro zenon_H90. % 0.69/0.85 apply (zenon_notimply_s _ _ zenon_H90). zenon_intro zenon_H92. zenon_intro zenon_H30. % 0.69/0.85 apply (zenon_and_s _ _ zenon_H92). zenon_intro zenon_H2e. zenon_intro zenon_H2f. % 0.69/0.85 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H4f. zenon_intro zenon_H93. % 0.69/0.85 apply (zenon_and_s _ _ zenon_H93). zenon_intro zenon_H26. zenon_intro zenon_H20. % 0.69/0.85 generalize (difference zenon_TY_bo). zenon_intro zenon_H3f. % 0.69/0.85 generalize (difference zenon_TZ_bi). zenon_intro zenon_H48. % 0.69/0.85 generalize (difference zenon_TX_bz). zenon_intro zenon_H94. % 0.69/0.85 generalize (zenon_H94 zenon_TE_v). zenon_intro zenon_H95. % 0.69/0.85 generalize (zenon_H95 zenon_TX_w). zenon_intro zenon_H96. % 0.69/0.85 apply (zenon_equiv_s _ _ zenon_H96); [ zenon_intro zenon_H9a; zenon_intro zenon_H99 | zenon_intro zenon_H98; zenon_intro zenon_H97 ]. % 0.69/0.85 apply (zenon_notand_s _ _ zenon_H99); [ zenon_intro zenon_H51 | zenon_intro zenon_H47 ]. % 0.69/0.85 exact (zenon_H51 zenon_H4f). % 0.69/0.85 apply (zenon_L7_ zenon_TX_w zenon_TY_bo zenon_TZ_bi zenon_TR_by zenon_TE_v zenon_TX_bz); trivial. % 0.69/0.85 apply (zenon_and_s _ _ zenon_H97). zenon_intro zenon_H4f. zenon_intro zenon_H39. % 0.69/0.85 apply (zenon_L8_ zenon_TX_bz zenon_TE_v zenon_TX_w); trivial. % 0.69/0.85 exact (zenon_H58 zenon_H6b). % 0.69/0.85 Qed. % 0.69/0.85 % SZS output end Proof % 0.69/0.85 (* END-PROOF *) % 0.69/0.85 nodes searched: 16430 % 0.69/0.85 max branch formulas: 1795 % 0.69/0.85 proof nodes created: 715 % 0.69/0.85 formulas created: 80290 % 0.69/0.85 %------------------------------------------------------------------------------