%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : PUZ031+2 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n021.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 : Mon Jul 18 18:33:38 EDT 2022 % Result : Theorem 2.71s 2.87s % Output : Proof 2.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PUZ031+2 : TPTP v8.1.0. Released v4.1.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n021.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 : Sat May 28 21:46:42 EDT 2022 % 0.12/0.34 % CPUTime : % 2.71/2.87 (* PROOF-FOUND *) % 2.71/2.87 % SZS status Theorem % 2.71/2.87 (* BEGIN-PROOF *) % 2.71/2.87 % SZS output start Proof % 2.71/2.87 Theorem pel47 : (exists X : zenon_U, (exists Y : zenon_U, ((animal X)/\((animal Y)/\(exists Z : zenon_U, ((grain Z)/\((eats Y Z)/\(eats X Y)))))))). % 2.71/2.87 Proof. % 2.71/2.87 assert (zenon_L1_ : forall (zenon_TA_ba : zenon_U), (bird zenon_TA_ba) -> (~(animal zenon_TA_ba)) -> False). % 2.71/2.87 do 1 intro. intros zenon_H18 zenon_H19. % 2.71/2.87 generalize (pel47_3_1 zenon_TA_ba). zenon_intro zenon_H1b. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 2.71/2.87 exact (zenon_H1d zenon_H18). % 2.71/2.87 exact (zenon_H19 zenon_H1c). % 2.71/2.87 (* end of lemma zenon_L1_ *) % 2.71/2.87 assert (zenon_L2_ : forall (zenon_TA_bg : zenon_U), (fox zenon_TA_bg) -> (~(animal zenon_TA_bg)) -> False). % 2.71/2.87 do 1 intro. intros zenon_H1e zenon_H1f. % 2.71/2.87 generalize (pel47_2_1 zenon_TA_bg). zenon_intro zenon_H21. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H21); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 2.71/2.87 exact (zenon_H23 zenon_H1e). % 2.71/2.87 exact (zenon_H1f zenon_H22). % 2.71/2.87 (* end of lemma zenon_L2_ *) % 2.71/2.87 assert (zenon_L3_ : forall (zenon_TA_bm : zenon_U), (wolf zenon_TA_bm) -> (~(animal zenon_TA_bm)) -> False). % 2.71/2.87 do 1 intro. intros zenon_H24 zenon_H25. % 2.71/2.87 generalize (pel47_1_1 zenon_TA_bm). zenon_intro zenon_H27. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H27); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 2.71/2.87 exact (zenon_H29 zenon_H24). % 2.71/2.87 exact (zenon_H25 zenon_H28). % 2.71/2.87 (* end of lemma zenon_L3_ *) % 2.71/2.87 assert (zenon_L4_ : forall (zenon_TA_bs : zenon_U) (zenon_TA_bm : zenon_U), (wolf zenon_TA_bm) -> (forall Y : zenon_U, ((plant Y)->(eats zenon_TA_bm Y))) -> (grain zenon_TA_bs) -> False). % 2.71/2.87 do 2 intro. intros zenon_H24 zenon_H2a zenon_H2b. % 2.71/2.87 generalize (pel47_11a zenon_TA_bm). zenon_intro zenon_H2d. % 2.71/2.87 generalize (pel47_6_2 zenon_TA_bs). zenon_intro zenon_H2e. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 2.71/2.87 exact (zenon_H30 zenon_H2b). % 2.71/2.87 generalize (zenon_H2a zenon_TA_bs). zenon_intro zenon_H31. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H31); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 2.71/2.87 exact (zenon_H33 zenon_H2f). % 2.71/2.87 generalize (zenon_H2d zenon_TA_bs). zenon_intro zenon_H34. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H34); [ zenon_intro zenon_H36 | zenon_intro zenon_H35 ]. % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H29 | zenon_intro zenon_H30 ]. % 2.71/2.87 exact (zenon_H29 zenon_H24). % 2.71/2.87 exact (zenon_H30 zenon_H2b). % 2.71/2.87 exact (zenon_H35 zenon_H32). % 2.71/2.87 (* end of lemma zenon_L4_ *) % 2.71/2.87 assert (zenon_L5_ : forall (zenon_TA_bg : zenon_U) (zenon_TA_bm : zenon_U), (forall Y : zenon_U, (((wolf zenon_TA_bm)/\(fox Y))->(~(eats zenon_TA_bm Y)))) -> (wolf zenon_TA_bm) -> (fox zenon_TA_bg) -> (eats zenon_TA_bm zenon_TA_bg) -> False). % 2.71/2.87 do 2 intro. intros zenon_H37 zenon_H24 zenon_H1e zenon_H38. % 2.71/2.87 generalize (zenon_H37 zenon_TA_bg). zenon_intro zenon_H39. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H39); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H3b); [ zenon_intro zenon_H29 | zenon_intro zenon_H23 ]. % 2.71/2.87 exact (zenon_H29 zenon_H24). % 2.71/2.87 exact (zenon_H23 zenon_H1e). % 2.71/2.87 exact (zenon_H3a zenon_H38). % 2.71/2.87 (* end of lemma zenon_L5_ *) % 2.71/2.87 assert (zenon_L6_ : forall (zenon_TA_bg : zenon_U) (zenon_TA_bs : zenon_U) (zenon_TA_bm : zenon_U), (wolf zenon_TA_bm) -> (grain zenon_TA_bs) -> (forall Y : zenon_U, ((plant Y)->(eats zenon_TA_bg Y))) -> (much_smaller zenon_TA_bg zenon_TA_bm) -> (fox zenon_TA_bg) -> False). % 2.71/2.87 do 3 intro. intros zenon_H24 zenon_H2b zenon_H3c zenon_H3d zenon_H1e. % 2.71/2.87 generalize (pel47_7 zenon_TA_bm). zenon_intro zenon_H3e. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H25 | zenon_intro zenon_H3f ]. % 2.71/2.87 apply (zenon_L3_ zenon_TA_bm); trivial. % 2.71/2.87 apply (zenon_or_s _ _ zenon_H3f); [ zenon_intro zenon_H2a | zenon_intro zenon_H40 ]. % 2.71/2.87 apply (zenon_L4_ zenon_TA_bs zenon_TA_bm); trivial. % 2.71/2.87 generalize (pel47_6_2 zenon_TA_bs). zenon_intro zenon_H2e. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 2.71/2.87 exact (zenon_H30 zenon_H2b). % 2.71/2.87 generalize (zenon_H3c zenon_TA_bs). zenon_intro zenon_H41. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H33 | zenon_intro zenon_H42 ]. % 2.71/2.87 exact (zenon_H33 zenon_H2f). % 2.71/2.87 generalize (pel47_11 zenon_TA_bm). zenon_intro zenon_H37. % 2.71/2.87 generalize (pel47_2_1 zenon_TA_bg). zenon_intro zenon_H21. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H21); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 2.71/2.87 exact (zenon_H23 zenon_H1e). % 2.71/2.87 generalize (zenon_H40 zenon_TA_bg). zenon_intro zenon_H43. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H43); [ zenon_intro zenon_H44 | zenon_intro zenon_H38 ]. % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H44); [ zenon_intro zenon_H1f | zenon_intro zenon_H45 ]. % 2.71/2.87 exact (zenon_H1f zenon_H22). % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H45); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 2.71/2.87 exact (zenon_H47 zenon_H3d). % 2.71/2.87 apply zenon_H46. exists zenon_TA_bs. apply NNPP. zenon_intro zenon_H48. % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H33 | zenon_intro zenon_H49 ]. % 2.71/2.87 exact (zenon_H33 zenon_H2f). % 2.71/2.87 exact (zenon_H49 zenon_H42). % 2.71/2.87 apply (zenon_L5_ zenon_TA_bg zenon_TA_bm); trivial. % 2.71/2.87 (* end of lemma zenon_L6_ *) % 2.71/2.87 assert (zenon_L7_ : forall (zenon_TA_bs : zenon_U), (grain zenon_TA_bs) -> (~(plant zenon_TA_bs)) -> False). % 2.71/2.87 do 1 intro. intros zenon_H2b zenon_H33. % 2.71/2.87 generalize (pel47_6_2 zenon_TA_bs). zenon_intro zenon_H2e. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 2.71/2.87 exact (zenon_H30 zenon_H2b). % 2.71/2.87 exact (zenon_H33 zenon_H2f). % 2.71/2.87 (* end of lemma zenon_L7_ *) % 2.71/2.87 assert (zenon_L8_ : forall (zenon_TA_bs : zenon_U) (zenon_TA_ba : zenon_U) (zenon_TA_bg : zenon_U), (~(exists Y : zenon_U, ((animal zenon_TA_bg)/\((animal Y)/\(exists Z : zenon_U, ((grain Z)/\((eats Y Z)/\(eats zenon_TA_bg Y)))))))) -> (fox zenon_TA_bg) -> (bird zenon_TA_ba) -> (grain zenon_TA_bs) -> (eats zenon_TA_ba zenon_TA_bs) -> (eats zenon_TA_bg zenon_TA_ba) -> False). % 2.71/2.87 do 3 intro. intros zenon_H4a zenon_H1e zenon_H18 zenon_H2b zenon_H4b zenon_H4c. % 2.71/2.87 apply zenon_H4a. exists zenon_TA_ba. apply NNPP. zenon_intro zenon_H4d. % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H1f | zenon_intro zenon_H4e ]. % 2.71/2.87 apply (zenon_L2_ zenon_TA_bg); trivial. % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H19 | zenon_intro zenon_H4f ]. % 2.71/2.87 apply (zenon_L1_ zenon_TA_ba); trivial. % 2.71/2.87 apply zenon_H4f. exists zenon_TA_bs. apply NNPP. zenon_intro zenon_H50. % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H30 | zenon_intro zenon_H51 ]. % 2.71/2.87 exact (zenon_H30 zenon_H2b). % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H51); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 2.71/2.87 exact (zenon_H53 zenon_H4b). % 2.71/2.87 exact (zenon_H52 zenon_H4c). % 2.71/2.87 (* end of lemma zenon_L8_ *) % 2.71/2.87 assert (zenon_L9_ : forall (zenon_TA_bs : zenon_U) (zenon_TA_ba : zenon_U) (zenon_TA_bg : zenon_U), (~(exists X : zenon_U, (exists Y : zenon_U, ((animal X)/\((animal Y)/\(exists Z : zenon_U, ((grain Z)/\((eats Y Z)/\(eats X Y))))))))) -> (eats zenon_TA_bg zenon_TA_ba) -> (eats zenon_TA_ba zenon_TA_bs) -> (grain zenon_TA_bs) -> (bird zenon_TA_ba) -> (fox zenon_TA_bg) -> False). % 2.71/2.87 do 3 intro. intros zenon_G zenon_H4c zenon_H4b zenon_H2b zenon_H18 zenon_H1e. % 2.71/2.87 apply zenon_G. exists zenon_TA_bg. apply NNPP. zenon_intro zenon_H4a. % 2.71/2.87 apply (zenon_L8_ zenon_TA_bs zenon_TA_ba zenon_TA_bg); trivial. % 2.71/2.87 (* end of lemma zenon_L9_ *) % 2.71/2.87 assert (zenon_L10_ : forall (zenon_TA_bs : zenon_U) (zenon_TY_dk : zenon_U) (zenon_TA_ba : zenon_U) (zenon_TA_bg : zenon_U), (forall Y1 : zenon_U, (((animal Y1)/\((much_smaller Y1 zenon_TA_bg)/\(exists Z : zenon_U, ((plant Z)/\(eats Y1 Z)))))->(eats zenon_TA_bg Y1))) -> (animal zenon_TA_ba) -> (much_smaller zenon_TA_ba zenon_TA_bg) -> (plant zenon_TY_dk) -> (eats zenon_TA_ba zenon_TY_dk) -> (~(exists X : zenon_U, (exists Y : zenon_U, ((animal X)/\((animal Y)/\(exists Z : zenon_U, ((grain Z)/\((eats Y Z)/\(eats X Y))))))))) -> (eats zenon_TA_ba zenon_TA_bs) -> (grain zenon_TA_bs) -> (bird zenon_TA_ba) -> (fox zenon_TA_bg) -> False). % 2.71/2.87 do 4 intro. intros zenon_H54 zenon_H1c zenon_H55 zenon_H56 zenon_H57 zenon_G zenon_H4b zenon_H2b zenon_H18 zenon_H1e. % 2.71/2.87 generalize (zenon_H54 zenon_TA_ba). zenon_intro zenon_H59. % 2.71/2.87 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H5a | zenon_intro zenon_H4c ]. % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H19 | zenon_intro zenon_H5b ]. % 2.71/2.87 exact (zenon_H19 zenon_H1c). % 2.71/2.87 apply (zenon_notand_s _ _ zenon_H5b); [ zenon_intro zenon_H5d | zenon_intro zenon_H5c ]. % 2.71/2.88 exact (zenon_H5d zenon_H55). % 2.71/2.88 apply zenon_H5c. exists zenon_TY_dk. apply NNPP. zenon_intro zenon_H5e. % 2.71/2.88 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H60 | zenon_intro zenon_H5f ]. % 2.71/2.88 exact (zenon_H60 zenon_H56). % 2.71/2.88 exact (zenon_H5f zenon_H57). % 2.71/2.88 apply (zenon_L9_ zenon_TA_bs zenon_TA_ba zenon_TA_bg); trivial. % 2.71/2.88 (* end of lemma zenon_L10_ *) % 2.71/2.88 assert (zenon_L11_ : forall (zenon_TA_dw : zenon_U) (zenon_TA_ba : zenon_U), (forall Y : zenon_U, (((bird zenon_TA_ba)/\(snail Y))->(~(eats zenon_TA_ba Y)))) -> (bird zenon_TA_ba) -> (snail zenon_TA_dw) -> (eats zenon_TA_ba zenon_TA_dw) -> False). % 2.71/2.88 do 2 intro. intros zenon_H61 zenon_H18 zenon_H62 zenon_H63. % 2.71/2.88 generalize (zenon_H61 zenon_TA_dw). zenon_intro zenon_H65. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 2.71/2.88 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H1d | zenon_intro zenon_H68 ]. % 2.71/2.88 exact (zenon_H1d zenon_H18). % 2.71/2.88 exact (zenon_H68 zenon_H62). % 2.71/2.88 exact (zenon_H66 zenon_H63). % 2.71/2.88 (* end of lemma zenon_L11_ *) % 2.71/2.88 assert (zenon_L12_ : forall (zenon_TA_dw : zenon_U) (zenon_TA_ba : zenon_U), (bird zenon_TA_ba) -> (forall X : zenon_U, (((bird zenon_TA_ba)/\(snail X))->(much_smaller X zenon_TA_ba))) -> (snail zenon_TA_dw) -> (forall Y1 : zenon_U, (((animal Y1)/\((much_smaller Y1 zenon_TA_ba)/\(exists Z : zenon_U, ((plant Z)/\(eats Y1 Z)))))->(eats zenon_TA_ba Y1))) -> False). % 2.71/2.88 do 2 intro. intros zenon_H18 zenon_H69 zenon_H62 zenon_H6a. % 2.71/2.88 generalize (pel47_13 zenon_TA_ba). zenon_intro zenon_H61. % 2.71/2.88 generalize (zenon_H6a zenon_TA_dw). zenon_intro zenon_H6b. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_H6c | zenon_intro zenon_H63 ]. % 2.71/2.88 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 2.71/2.88 generalize (pel47_4_2 zenon_TA_dw). zenon_intro zenon_H6f. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H6f); [ zenon_intro zenon_H68 | zenon_intro zenon_H70 ]. % 2.71/2.88 exact (zenon_H68 zenon_H62). % 2.71/2.88 exact (zenon_H6e zenon_H70). % 2.71/2.88 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H72 | zenon_intro zenon_H71 ]. % 2.71/2.88 generalize (zenon_H69 zenon_TA_dw). zenon_intro zenon_H73. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H73); [ zenon_intro zenon_H67 | zenon_intro zenon_H74 ]. % 2.71/2.88 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H1d | zenon_intro zenon_H68 ]. % 2.71/2.88 exact (zenon_H1d zenon_H18). % 2.71/2.88 exact (zenon_H68 zenon_H62). % 2.71/2.88 exact (zenon_H72 zenon_H74). % 2.71/2.88 generalize (pel47_14a zenon_TA_dw). zenon_intro zenon_H75. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H75); [ zenon_intro zenon_H68 | zenon_intro zenon_H76 ]. % 2.71/2.88 exact (zenon_H68 zenon_H62). % 2.71/2.88 exact (zenon_H71 zenon_H76). % 2.71/2.88 apply (zenon_L11_ zenon_TA_dw zenon_TA_ba); trivial. % 2.71/2.88 (* end of lemma zenon_L12_ *) % 2.71/2.88 apply NNPP. intro zenon_G. % 2.71/2.88 elim wolf_type. zenon_intro zenon_TA_bm. zenon_intro zenon_H24. % 2.71/2.88 elim fox_type. zenon_intro zenon_TA_bg. zenon_intro zenon_H1e. % 2.71/2.88 elim bird_type. zenon_intro zenon_TA_ba. zenon_intro zenon_H18. % 2.71/2.88 elim caterpillar_type. zenon_intro zenon_TA_ep. zenon_intro zenon_H78. % 2.71/2.88 elim snail_type. zenon_intro zenon_TA_dw. zenon_intro zenon_H62. % 2.71/2.88 elim grain_type. zenon_intro zenon_TA_bs. zenon_intro zenon_H2b. % 2.71/2.88 generalize (pel47_8 zenon_TA_ba). zenon_intro zenon_H69. % 2.71/2.88 generalize (pel47_9 zenon_TA_ba). zenon_intro zenon_H79. % 2.71/2.88 generalize (pel47_10 zenon_TA_bg). zenon_intro zenon_H7a. % 2.71/2.88 generalize (pel47_7 zenon_TA_ba). zenon_intro zenon_H7b. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H19 | zenon_intro zenon_H7c ]. % 2.71/2.88 apply (zenon_L1_ zenon_TA_ba); trivial. % 2.71/2.88 apply (zenon_or_s _ _ zenon_H7c); [ zenon_intro zenon_H7d | zenon_intro zenon_H6a ]. % 2.71/2.88 generalize (pel47_14 zenon_TA_ep). zenon_intro zenon_H7e. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H80 | zenon_intro zenon_H7f ]. % 2.71/2.88 exact (zenon_H80 zenon_H78). % 2.71/2.88 elim zenon_H7f. zenon_intro zenon_TY_dk. zenon_intro zenon_H81. % 2.71/2.88 apply (zenon_and_s _ _ zenon_H81). zenon_intro zenon_H56. zenon_intro zenon_H82. % 2.71/2.88 generalize (zenon_H7d zenon_TY_dk). zenon_intro zenon_H83. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H83); [ zenon_intro zenon_H60 | zenon_intro zenon_H57 ]. % 2.71/2.88 exact (zenon_H60 zenon_H56). % 2.71/2.88 generalize (zenon_H79 zenon_TA_bg). zenon_intro zenon_H84. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H84); [ zenon_intro zenon_H85 | zenon_intro zenon_H55 ]. % 2.71/2.88 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H1d | zenon_intro zenon_H23 ]. % 2.71/2.88 exact (zenon_H1d zenon_H18). % 2.71/2.88 exact (zenon_H23 zenon_H1e). % 2.71/2.88 generalize (zenon_H7a zenon_TA_bm). zenon_intro zenon_H86. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H86); [ zenon_intro zenon_H87 | zenon_intro zenon_H3d ]. % 2.71/2.88 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H23 | zenon_intro zenon_H29 ]. % 2.71/2.88 exact (zenon_H23 zenon_H1e). % 2.71/2.88 exact (zenon_H29 zenon_H24). % 2.71/2.88 generalize (pel47_7 zenon_TA_bg). zenon_intro zenon_H88. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H88); [ zenon_intro zenon_H1f | zenon_intro zenon_H89 ]. % 2.71/2.88 apply (zenon_L2_ zenon_TA_bg); trivial. % 2.71/2.88 apply (zenon_or_s _ _ zenon_H89); [ zenon_intro zenon_H3c | zenon_intro zenon_H54 ]. % 2.71/2.88 apply (zenon_L6_ zenon_TA_bg zenon_TA_bs zenon_TA_bm); trivial. % 2.71/2.88 generalize (zenon_H7d zenon_TA_bs). zenon_intro zenon_H8a. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H8a); [ zenon_intro zenon_H33 | zenon_intro zenon_H4b ]. % 2.71/2.88 apply (zenon_L7_ zenon_TA_bs); trivial. % 2.71/2.88 generalize (pel47_3_1 zenon_TA_ba). zenon_intro zenon_H1b. % 2.71/2.88 apply (zenon_imply_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 2.71/2.88 exact (zenon_H1d zenon_H18). % 2.71/2.88 apply (zenon_L10_ zenon_TA_bs zenon_TY_dk zenon_TA_ba zenon_TA_bg); trivial. % 2.71/2.88 apply (zenon_L12_ zenon_TA_dw zenon_TA_ba); trivial. % 2.71/2.88 Qed. % 2.71/2.88 % SZS output end Proof % 2.71/2.88 (* END-PROOF *) % 2.71/2.88 nodes searched: 208638 % 2.71/2.88 max branch formulas: 8411 % 2.71/2.88 proof nodes created: 3191 % 2.71/2.88 formulas created: 260545 % 2.71/2.88 %------------------------------------------------------------------------------