%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEU375+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n006.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 16:01:37 EDT 2022 % Result : Theorem 0.73s 0.87s % Output : Proof 0.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SEU375+1 : TPTP v8.1.0. Released v3.3.0. % 0.10/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n006.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 Jun 20 11:56:10 EDT 2022 % 0.13/0.33 % CPUTime : % 0.73/0.87 (* PROOF-FOUND *) % 0.73/0.87 % SZS status Theorem % 0.73/0.87 (* BEGIN-PROOF *) % 0.73/0.87 % SZS output start Proof % 0.73/0.87 Theorem t21_yellow_6 : (forall A : zenon_U, ((one_sorted_str A)->(forall B : zenon_U, (((~(empty_carrier B))/\(net_str B A))->(forall C : zenon_U, (((~(empty_carrier C))/\((full_subnetstr C A B)/\(subnetstr C A B)))->(forall D : zenon_U, ((element D (the_carrier B))->(forall E : zenon_U, ((element E (the_carrier B))->(forall F : zenon_U, ((element F (the_carrier C))->(forall G : zenon_U, ((element G (the_carrier C))->(((D = F)/\((E = G)/\(related B D E)))->(related C F G)))))))))))))))). % 0.73/0.87 Proof. % 0.73/0.87 assert (zenon_L1_ : forall (zenon_TB_bn : zenon_U) (zenon_TA_bo : zenon_U), (one_sorted_str zenon_TA_bo) -> (net_str zenon_TB_bn zenon_TA_bo) -> (~(rel_str zenon_TB_bn)) -> False). % 0.73/0.87 do 2 intro. intros zenon_H24 zenon_H25 zenon_H26. % 0.73/0.87 generalize (dt_l1_waybel_0 zenon_TA_bo). zenon_intro zenon_H29. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H29); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 0.73/0.87 exact (zenon_H2b zenon_H24). % 0.73/0.87 generalize (zenon_H2a zenon_TB_bn). zenon_intro zenon_H2c. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H2c); [ zenon_intro zenon_H2e | zenon_intro zenon_H2d ]. % 0.73/0.87 exact (zenon_H2e zenon_H25). % 0.73/0.87 exact (zenon_H26 zenon_H2d). % 0.73/0.87 (* end of lemma zenon_L1_ *) % 0.73/0.87 assert (zenon_L2_ : forall (zenon_TB_bn : zenon_U) (zenon_TC_bx : zenon_U), ((full_subrelstr zenon_TC_bx zenon_TB_bn)/\(subrelstr zenon_TC_bx zenon_TB_bn)) -> (~(full_subrelstr zenon_TC_bx zenon_TB_bn)) -> False). % 0.73/0.87 do 2 intro. intros zenon_H2f zenon_H30. % 0.73/0.87 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H33. zenon_intro zenon_H32. % 0.73/0.87 exact (zenon_H30 zenon_H33). % 0.73/0.87 (* end of lemma zenon_L2_ *) % 0.73/0.87 assert (zenon_L3_ : forall (zenon_TB_bn : zenon_U) (zenon_TC_bx : zenon_U), ((full_subrelstr zenon_TC_bx zenon_TB_bn)/\(subrelstr zenon_TC_bx zenon_TB_bn)) -> (~(subrelstr zenon_TC_bx zenon_TB_bn)) -> False). % 0.73/0.87 do 2 intro. intros zenon_H2f zenon_H34. % 0.73/0.87 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H33. zenon_intro zenon_H32. % 0.73/0.87 exact (zenon_H34 zenon_H32). % 0.73/0.87 (* end of lemma zenon_L3_ *) % 0.73/0.87 assert (zenon_L4_ : forall (zenon_TC_bx : zenon_U) (zenon_TB_bn : zenon_U) (zenon_TA_bo : zenon_U), (one_sorted_str zenon_TA_bo) -> (forall B : zenon_U, (((one_sorted_str zenon_TA_bo)/\(net_str B zenon_TA_bo))->(forall C : zenon_U, ((subnetstr C zenon_TA_bo B)->(net_str C zenon_TA_bo))))) -> (net_str zenon_TB_bn zenon_TA_bo) -> (subnetstr zenon_TC_bx zenon_TA_bo zenon_TB_bn) -> (~(one_sorted_str zenon_TC_bx)) -> False). % 0.73/0.87 do 3 intro. intros zenon_H24 zenon_H35 zenon_H25 zenon_H36 zenon_H37. % 0.73/0.87 generalize (dt_l1_orders_2 zenon_TC_bx). zenon_intro zenon_H38. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H38); [ zenon_intro zenon_H3a | zenon_intro zenon_H39 ]. % 0.73/0.87 generalize (dt_l1_waybel_0 zenon_TA_bo). zenon_intro zenon_H29. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H29); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 0.73/0.87 exact (zenon_H2b zenon_H24). % 0.73/0.87 generalize (zenon_H2a zenon_TC_bx). zenon_intro zenon_H3b. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H3b); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 0.73/0.87 generalize (zenon_H35 zenon_TB_bn). zenon_intro zenon_H3e. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 0.73/0.87 apply (zenon_notand_s _ _ zenon_H40); [ zenon_intro zenon_H2b | zenon_intro zenon_H2e ]. % 0.73/0.87 exact (zenon_H2b zenon_H24). % 0.73/0.87 exact (zenon_H2e zenon_H25). % 0.73/0.87 generalize (zenon_H3f zenon_TC_bx). zenon_intro zenon_H41. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 0.73/0.87 exact (zenon_H43 zenon_H36). % 0.73/0.87 exact (zenon_H3d zenon_H42). % 0.73/0.87 exact (zenon_H3a zenon_H3c). % 0.73/0.87 exact (zenon_H37 zenon_H39). % 0.73/0.87 (* end of lemma zenon_L4_ *) % 0.73/0.87 assert (zenon_L5_ : forall (zenon_TC_bx : zenon_U) (zenon_TF_cu : zenon_U), (forall B : zenon_U, ((element zenon_TF_cu B)->((empty B)\/(in zenon_TF_cu B)))) -> (element zenon_TF_cu (the_carrier zenon_TC_bx)) -> (~(empty (the_carrier zenon_TC_bx))) -> (~(in zenon_TF_cu (the_carrier zenon_TC_bx))) -> False). % 0.73/0.87 do 2 intro. intros zenon_H44 zenon_H45 zenon_H46 zenon_H47. % 0.73/0.87 generalize (zenon_H44 (the_carrier zenon_TC_bx)). zenon_intro zenon_H49. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H49); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 0.73/0.87 exact (zenon_H4b zenon_H45). % 0.73/0.87 apply (zenon_or_s _ _ zenon_H4a); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 0.73/0.87 exact (zenon_H46 zenon_H4d). % 0.73/0.87 exact (zenon_H47 zenon_H4c). % 0.73/0.87 (* end of lemma zenon_L5_ *) % 0.73/0.87 assert (zenon_L6_ : forall (zenon_TB_bn : zenon_U) (zenon_TA_bo : zenon_U) (zenon_TC_bx : zenon_U) (zenon_TF_cu : zenon_U), (~(in zenon_TF_cu (the_carrier zenon_TC_bx))) -> (element zenon_TF_cu (the_carrier zenon_TC_bx)) -> (subnetstr zenon_TC_bx zenon_TA_bo zenon_TB_bn) -> (net_str zenon_TB_bn zenon_TA_bo) -> (forall B : zenon_U, (((one_sorted_str zenon_TA_bo)/\(net_str B zenon_TA_bo))->(forall C : zenon_U, ((subnetstr C zenon_TA_bo B)->(net_str C zenon_TA_bo))))) -> (one_sorted_str zenon_TA_bo) -> (~(empty_carrier zenon_TC_bx)) -> False). % 0.73/0.87 do 4 intro. intros zenon_H47 zenon_H45 zenon_H36 zenon_H25 zenon_H35 zenon_H24 zenon_H4e. % 0.73/0.87 generalize (t2_subset zenon_TF_cu). zenon_intro zenon_H44. % 0.73/0.87 generalize (fc1_struct_0 zenon_TC_bx). zenon_intro zenon_H4f. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H4f); [ zenon_intro zenon_H50 | zenon_intro zenon_H46 ]. % 0.73/0.87 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H51 | zenon_intro zenon_H37 ]. % 0.73/0.87 exact (zenon_H51 zenon_H4e). % 0.73/0.87 apply (zenon_L4_ zenon_TC_bx zenon_TB_bn zenon_TA_bo); trivial. % 0.73/0.87 apply (zenon_L5_ zenon_TC_bx zenon_TF_cu); trivial. % 0.73/0.87 (* end of lemma zenon_L6_ *) % 0.73/0.87 assert (zenon_L7_ : forall (zenon_TC_bx : zenon_U) (zenon_TG_dh : zenon_U), (forall B : zenon_U, ((element zenon_TG_dh B)->((empty B)\/(in zenon_TG_dh B)))) -> (element zenon_TG_dh (the_carrier zenon_TC_bx)) -> (~(empty (the_carrier zenon_TC_bx))) -> (~(in zenon_TG_dh (the_carrier zenon_TC_bx))) -> False). % 0.73/0.87 do 2 intro. intros zenon_H52 zenon_H53 zenon_H46 zenon_H54. % 0.73/0.87 generalize (zenon_H52 (the_carrier zenon_TC_bx)). zenon_intro zenon_H56. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H56); [ zenon_intro zenon_H58 | zenon_intro zenon_H57 ]. % 0.73/0.87 exact (zenon_H58 zenon_H53). % 0.73/0.87 apply (zenon_or_s _ _ zenon_H57); [ zenon_intro zenon_H4d | zenon_intro zenon_H59 ]. % 0.73/0.87 exact (zenon_H46 zenon_H4d). % 0.73/0.87 exact (zenon_H54 zenon_H59). % 0.73/0.87 (* end of lemma zenon_L7_ *) % 0.73/0.87 assert (zenon_L8_ : forall (zenon_TB_bn : zenon_U) (zenon_TA_bo : zenon_U) (zenon_TC_bx : zenon_U) (zenon_TG_dh : zenon_U), (~(in zenon_TG_dh (the_carrier zenon_TC_bx))) -> (element zenon_TG_dh (the_carrier zenon_TC_bx)) -> (subnetstr zenon_TC_bx zenon_TA_bo zenon_TB_bn) -> (net_str zenon_TB_bn zenon_TA_bo) -> (forall B : zenon_U, (((one_sorted_str zenon_TA_bo)/\(net_str B zenon_TA_bo))->(forall C : zenon_U, ((subnetstr C zenon_TA_bo B)->(net_str C zenon_TA_bo))))) -> (one_sorted_str zenon_TA_bo) -> (~(empty_carrier zenon_TC_bx)) -> False). % 0.73/0.87 do 4 intro. intros zenon_H54 zenon_H53 zenon_H36 zenon_H25 zenon_H35 zenon_H24 zenon_H4e. % 0.73/0.87 generalize (t2_subset zenon_TG_dh). zenon_intro zenon_H52. % 0.73/0.87 generalize (fc1_struct_0 zenon_TC_bx). zenon_intro zenon_H4f. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H4f); [ zenon_intro zenon_H50 | zenon_intro zenon_H46 ]. % 0.73/0.87 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H51 | zenon_intro zenon_H37 ]. % 0.73/0.87 exact (zenon_H51 zenon_H4e). % 0.73/0.87 apply (zenon_L4_ zenon_TC_bx zenon_TB_bn zenon_TA_bo); trivial. % 0.73/0.87 apply (zenon_L7_ zenon_TC_bx zenon_TG_dh); trivial. % 0.73/0.87 (* end of lemma zenon_L8_ *) % 0.73/0.87 apply NNPP. intro zenon_G. % 0.73/0.87 apply (zenon_notallex_s (fun A : zenon_U => ((one_sorted_str A)->(forall B : zenon_U, (((~(empty_carrier B))/\(net_str B A))->(forall C : zenon_U, (((~(empty_carrier C))/\((full_subnetstr C A B)/\(subnetstr C A B)))->(forall D : zenon_U, ((element D (the_carrier B))->(forall E : zenon_U, ((element E (the_carrier B))->(forall F : zenon_U, ((element F (the_carrier C))->(forall G : zenon_U, ((element G (the_carrier C))->(((D = F)/\((E = G)/\(related B D E)))->(related C F G)))))))))))))))) zenon_G); [ zenon_intro zenon_H5a; idtac ]. % 0.73/0.87 elim zenon_H5a. zenon_intro zenon_TA_bo. zenon_intro zenon_H5b. % 0.73/0.87 apply (zenon_notimply_s _ _ zenon_H5b). zenon_intro zenon_H24. zenon_intro zenon_H5c. % 0.73/0.87 apply (zenon_notallex_s (fun B : zenon_U => (((~(empty_carrier B))/\(net_str B zenon_TA_bo))->(forall C : zenon_U, (((~(empty_carrier C))/\((full_subnetstr C zenon_TA_bo B)/\(subnetstr C zenon_TA_bo B)))->(forall D : zenon_U, ((element D (the_carrier B))->(forall E : zenon_U, ((element E (the_carrier B))->(forall F : zenon_U, ((element F (the_carrier C))->(forall G : zenon_U, ((element G (the_carrier C))->(((D = F)/\((E = G)/\(related B D E)))->(related C F G)))))))))))))) zenon_H5c); [ zenon_intro zenon_H5d; idtac ]. % 0.73/0.87 elim zenon_H5d. zenon_intro zenon_TB_bn. zenon_intro zenon_H5e. % 0.73/0.87 apply (zenon_notimply_s _ _ zenon_H5e). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 0.73/0.87 apply (zenon_and_s _ _ zenon_H60). zenon_intro zenon_H61. zenon_intro zenon_H25. % 0.73/0.87 apply (zenon_notallex_s (fun C : zenon_U => (((~(empty_carrier C))/\((full_subnetstr C zenon_TA_bo zenon_TB_bn)/\(subnetstr C zenon_TA_bo zenon_TB_bn)))->(forall D : zenon_U, ((element D (the_carrier zenon_TB_bn))->(forall E : zenon_U, ((element E (the_carrier zenon_TB_bn))->(forall F : zenon_U, ((element F (the_carrier C))->(forall G : zenon_U, ((element G (the_carrier C))->(((D = F)/\((E = G)/\(related zenon_TB_bn D E)))->(related C F G)))))))))))) zenon_H5f); [ zenon_intro zenon_H62; idtac ]. % 0.73/0.87 elim zenon_H62. zenon_intro zenon_TC_bx. zenon_intro zenon_H63. % 0.73/0.87 apply (zenon_notimply_s _ _ zenon_H63). zenon_intro zenon_H65. zenon_intro zenon_H64. % 0.73/0.87 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H4e. zenon_intro zenon_H66. % 0.73/0.87 apply (zenon_and_s _ _ zenon_H66). zenon_intro zenon_H67. zenon_intro zenon_H36. % 0.73/0.87 apply (zenon_notallex_s (fun D : zenon_U => ((element D (the_carrier zenon_TB_bn))->(forall E : zenon_U, ((element E (the_carrier zenon_TB_bn))->(forall F : zenon_U, ((element F (the_carrier zenon_TC_bx))->(forall G : zenon_U, ((element G (the_carrier zenon_TC_bx))->(((D = F)/\((E = G)/\(related zenon_TB_bn D E)))->(related zenon_TC_bx F G)))))))))) zenon_H64); [ zenon_intro zenon_H68; idtac ]. % 0.73/0.87 elim zenon_H68. zenon_intro zenon_TD_eb. zenon_intro zenon_H6a. % 0.73/0.87 apply (zenon_notimply_s _ _ zenon_H6a). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.73/0.87 apply (zenon_notallex_s (fun E : zenon_U => ((element E (the_carrier zenon_TB_bn))->(forall F : zenon_U, ((element F (the_carrier zenon_TC_bx))->(forall G : zenon_U, ((element G (the_carrier zenon_TC_bx))->(((zenon_TD_eb = F)/\((E = G)/\(related zenon_TB_bn zenon_TD_eb E)))->(related zenon_TC_bx F G)))))))) zenon_H6b); [ zenon_intro zenon_H6d; idtac ]. % 0.73/0.87 elim zenon_H6d. zenon_intro zenon_TE_eg. zenon_intro zenon_H6f. % 0.73/0.87 apply (zenon_notimply_s _ _ zenon_H6f). zenon_intro zenon_H71. zenon_intro zenon_H70. % 0.73/0.87 apply (zenon_notallex_s (fun F : zenon_U => ((element F (the_carrier zenon_TC_bx))->(forall G : zenon_U, ((element G (the_carrier zenon_TC_bx))->(((zenon_TD_eb = F)/\((zenon_TE_eg = G)/\(related zenon_TB_bn zenon_TD_eb zenon_TE_eg)))->(related zenon_TC_bx F G)))))) zenon_H70); [ zenon_intro zenon_H72; idtac ]. % 0.73/0.87 elim zenon_H72. zenon_intro zenon_TF_cu. zenon_intro zenon_H73. % 0.73/0.87 apply (zenon_notimply_s _ _ zenon_H73). zenon_intro zenon_H45. zenon_intro zenon_H74. % 0.73/0.87 apply (zenon_notallex_s (fun G : zenon_U => ((element G (the_carrier zenon_TC_bx))->(((zenon_TD_eb = zenon_TF_cu)/\((zenon_TE_eg = G)/\(related zenon_TB_bn zenon_TD_eb zenon_TE_eg)))->(related zenon_TC_bx zenon_TF_cu G)))) zenon_H74); [ zenon_intro zenon_H75; idtac ]. % 0.73/0.87 elim zenon_H75. zenon_intro zenon_TG_dh. zenon_intro zenon_H76. % 0.73/0.87 apply (zenon_notimply_s _ _ zenon_H76). zenon_intro zenon_H53. zenon_intro zenon_H77. % 0.73/0.87 apply (zenon_notimply_s _ _ zenon_H77). zenon_intro zenon_H79. zenon_intro zenon_H78. % 0.73/0.87 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 0.73/0.87 apply (zenon_and_s _ _ zenon_H7a). zenon_intro zenon_H7d. zenon_intro zenon_H7c. % 0.73/0.87 generalize (dt_m1_yellow_6 zenon_TA_bo). zenon_intro zenon_H35. % 0.73/0.87 generalize (t61_yellow_0 zenon_TB_bn). zenon_intro zenon_H7e. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H26 | zenon_intro zenon_H7f ]. % 0.73/0.87 apply (zenon_L1_ zenon_TB_bn zenon_TA_bo); trivial. % 0.73/0.87 generalize (zenon_H7f zenon_TC_bx). zenon_intro zenon_H80. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H80); [ zenon_intro zenon_H82 | zenon_intro zenon_H81 ]. % 0.73/0.87 apply (zenon_notand_s _ _ zenon_H82); [ zenon_intro zenon_H30 | zenon_intro zenon_H34 ]. % 0.73/0.87 generalize (d9_yellow_6 zenon_TA_bo). zenon_intro zenon_H83. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H2b | zenon_intro zenon_H84 ]. % 0.73/0.87 exact (zenon_H2b zenon_H24). % 0.73/0.87 generalize (zenon_H84 zenon_TB_bn). zenon_intro zenon_H85. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H85); [ zenon_intro zenon_H2e | zenon_intro zenon_H86 ]. % 0.73/0.87 exact (zenon_H2e zenon_H25). % 0.73/0.87 generalize (zenon_H86 zenon_TC_bx). zenon_intro zenon_H87. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H43 | zenon_intro zenon_H88 ]. % 0.73/0.87 exact (zenon_H43 zenon_H36). % 0.73/0.87 apply (zenon_equiv_s _ _ zenon_H88); [ zenon_intro zenon_H89; zenon_intro zenon_H82 | zenon_intro zenon_H67; zenon_intro zenon_H2f ]. % 0.73/0.87 exact (zenon_H89 zenon_H67). % 0.73/0.87 apply (zenon_L2_ zenon_TB_bn zenon_TC_bx); trivial. % 0.73/0.87 generalize (d9_yellow_6 zenon_TA_bo). zenon_intro zenon_H83. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H2b | zenon_intro zenon_H84 ]. % 0.73/0.87 exact (zenon_H2b zenon_H24). % 0.73/0.87 generalize (zenon_H84 zenon_TB_bn). zenon_intro zenon_H85. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H85); [ zenon_intro zenon_H2e | zenon_intro zenon_H86 ]. % 0.73/0.87 exact (zenon_H2e zenon_H25). % 0.73/0.87 generalize (zenon_H86 zenon_TC_bx). zenon_intro zenon_H87. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H43 | zenon_intro zenon_H88 ]. % 0.73/0.87 exact (zenon_H43 zenon_H36). % 0.73/0.87 apply (zenon_equiv_s _ _ zenon_H88); [ zenon_intro zenon_H89; zenon_intro zenon_H82 | zenon_intro zenon_H67; zenon_intro zenon_H2f ]. % 0.73/0.87 exact (zenon_H89 zenon_H67). % 0.73/0.87 apply (zenon_L3_ zenon_TB_bn zenon_TC_bx); trivial. % 0.73/0.87 generalize (zenon_H81 zenon_TD_eb). zenon_intro zenon_H8a. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H8a); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 0.73/0.87 exact (zenon_H8c zenon_H6c). % 0.73/0.87 generalize (zenon_H8b zenon_TE_eg). zenon_intro zenon_H8d. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H8d); [ zenon_intro zenon_H8f | zenon_intro zenon_H8e ]. % 0.73/0.87 exact (zenon_H8f zenon_H71). % 0.73/0.87 generalize (zenon_H8e zenon_TF_cu). zenon_intro zenon_H90. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H90); [ zenon_intro zenon_H4b | zenon_intro zenon_H91 ]. % 0.73/0.87 exact (zenon_H4b zenon_H45). % 0.73/0.87 generalize (zenon_H91 zenon_TG_dh). zenon_intro zenon_H92. % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H92); [ zenon_intro zenon_H58 | zenon_intro zenon_H93 ]. % 0.73/0.87 exact (zenon_H58 zenon_H53). % 0.73/0.87 apply (zenon_imply_s _ _ zenon_H93); [ zenon_intro zenon_H95 | zenon_intro zenon_H94 ]. % 0.73/0.87 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 0.73/0.87 apply zenon_H97. apply sym_equal. exact zenon_H7b. % 0.73/0.87 apply (zenon_notand_s _ _ zenon_H96); [ zenon_intro zenon_H99 | zenon_intro zenon_H98 ]. % 0.73/0.87 apply zenon_H99. apply sym_equal. exact zenon_H7d. % 0.73/0.87 apply (zenon_notand_s _ _ zenon_H98); [ zenon_intro zenon_H9b | zenon_intro zenon_H9a ]. % 0.73/0.87 exact (zenon_H9b zenon_H7c). % 0.73/0.87 apply (zenon_notand_s _ _ zenon_H9a); [ zenon_intro zenon_H47 | zenon_intro zenon_H54 ]. % 0.73/0.87 apply (zenon_L6_ zenon_TB_bn zenon_TA_bo zenon_TC_bx zenon_TF_cu); trivial. % 0.73/0.87 apply (zenon_L8_ zenon_TB_bn zenon_TA_bo zenon_TC_bx zenon_TG_dh); trivial. % 0.73/0.87 exact (zenon_H78 zenon_H94). % 0.73/0.87 Qed. % 0.73/0.87 % SZS output end Proof % 0.73/0.87 (* END-PROOF *) % 0.73/0.87 nodes searched: 6751 % 0.73/0.87 max branch formulas: 1854 % 0.73/0.87 proof nodes created: 537 % 0.73/0.87 formulas created: 29407 % 0.73/0.87 %------------------------------------------------------------------------------