%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : PUZ031+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n024.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:37 EDT 2022 % Result : Theorem 1.30s 1.47s % Output : Proof 1.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : PUZ031+1 : TPTP v8.1.0. Released v2.0.0. % 0.04/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n024.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 : Sat May 28 23:14:06 EDT 2022 % 0.12/0.33 % CPUTime : % 1.30/1.47 (* PROOF-FOUND *) % 1.30/1.47 % SZS status Theorem % 1.30/1.47 (* BEGIN-PROOF *) % 1.30/1.47 % SZS output start Proof % 1.30/1.47 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)))))))). % 1.30/1.47 Proof. % 1.30/1.47 assert (zenon_L1_ : forall (zenon_TX1_x : zenon_U), (~((snail zenon_TX1_x)\/(caterpillar zenon_TX1_x))) -> (snail zenon_TX1_x) -> False). % 1.30/1.47 do 1 intro. intros zenon_H15 zenon_H16. % 1.30/1.47 apply (zenon_notor_s _ _ zenon_H15). zenon_intro zenon_H19. zenon_intro zenon_H18. % 1.30/1.47 exact (zenon_H19 zenon_H16). % 1.30/1.47 (* end of lemma zenon_L1_ *) % 1.30/1.47 assert (zenon_L2_ : forall (zenon_TX1_bc : zenon_U), (bird zenon_TX1_bc) -> (~(animal zenon_TX1_bc)) -> False). % 1.30/1.47 do 1 intro. intros zenon_H1a zenon_H1b. % 1.30/1.47 generalize (pel47_3_1 zenon_TX1_bc). zenon_intro zenon_H1d. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H1d); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 1.30/1.47 exact (zenon_H1f zenon_H1a). % 1.30/1.47 exact (zenon_H1b zenon_H1e). % 1.30/1.47 (* end of lemma zenon_L2_ *) % 1.30/1.47 assert (zenon_L3_ : forall (zenon_TX1_bi : zenon_U), (fox zenon_TX1_bi) -> (~(animal zenon_TX1_bi)) -> False). % 1.30/1.47 do 1 intro. intros zenon_H20 zenon_H21. % 1.30/1.47 generalize (pel47_2_1 zenon_TX1_bi). zenon_intro zenon_H23. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H23); [ zenon_intro zenon_H25 | zenon_intro zenon_H24 ]. % 1.30/1.47 exact (zenon_H25 zenon_H20). % 1.30/1.47 exact (zenon_H21 zenon_H24). % 1.30/1.47 (* end of lemma zenon_L3_ *) % 1.30/1.47 assert (zenon_L4_ : forall (zenon_TX1_bo : zenon_U), (wolf zenon_TX1_bo) -> (~(animal zenon_TX1_bo)) -> False). % 1.30/1.47 do 1 intro. intros zenon_H26 zenon_H27. % 1.30/1.47 generalize (pel47_1_1 zenon_TX1_bo). zenon_intro zenon_H29. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H29); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 1.30/1.47 exact (zenon_H2b zenon_H26). % 1.30/1.47 exact (zenon_H27 zenon_H2a). % 1.30/1.47 (* end of lemma zenon_L4_ *) % 1.30/1.47 assert (zenon_L5_ : forall (zenon_TX_bu : zenon_U) (zenon_TX1_bo : zenon_U), (wolf zenon_TX1_bo) -> (forall Y : zenon_U, ((plant Y)->(eats zenon_TX1_bo Y))) -> (grain zenon_TX_bu) -> False). % 1.30/1.47 do 2 intro. intros zenon_H26 zenon_H2c zenon_H2d. % 1.30/1.47 generalize (pel47_11 zenon_TX1_bo). zenon_intro zenon_H2f. % 1.30/1.47 generalize (pel47_6_2 zenon_TX_bu). zenon_intro zenon_H30. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H30); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 1.30/1.47 exact (zenon_H32 zenon_H2d). % 1.30/1.47 generalize (zenon_H2c zenon_TX_bu). zenon_intro zenon_H33. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H33); [ zenon_intro zenon_H35 | zenon_intro zenon_H34 ]. % 1.30/1.47 exact (zenon_H35 zenon_H31). % 1.30/1.47 generalize (zenon_H2f zenon_TX_bu). zenon_intro zenon_H36. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H36); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H2b | zenon_intro zenon_H39 ]. % 1.30/1.47 exact (zenon_H2b zenon_H26). % 1.30/1.47 apply (zenon_notor_s _ _ zenon_H39). zenon_intro zenon_H3a. zenon_intro zenon_H32. % 1.30/1.47 exact (zenon_H32 zenon_H2d). % 1.30/1.47 exact (zenon_H37 zenon_H34). % 1.30/1.47 (* end of lemma zenon_L5_ *) % 1.30/1.47 assert (zenon_L6_ : forall (zenon_TX1_bi : zenon_U) (zenon_TX1_bo : zenon_U), (forall Y : zenon_U, (((wolf zenon_TX1_bo)/\((fox Y)\/(grain Y)))->(~(eats zenon_TX1_bo Y)))) -> (wolf zenon_TX1_bo) -> (fox zenon_TX1_bi) -> (eats zenon_TX1_bo zenon_TX1_bi) -> False). % 1.30/1.47 do 2 intro. intros zenon_H2f zenon_H26 zenon_H20 zenon_H3b. % 1.30/1.47 generalize (zenon_H2f zenon_TX1_bi). zenon_intro zenon_H3c. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H2b | zenon_intro zenon_H3f ]. % 1.30/1.47 exact (zenon_H2b zenon_H26). % 1.30/1.47 apply (zenon_notor_s _ _ zenon_H3f). zenon_intro zenon_H25. zenon_intro zenon_H40. % 1.30/1.47 exact (zenon_H25 zenon_H20). % 1.30/1.47 exact (zenon_H3d zenon_H3b). % 1.30/1.47 (* end of lemma zenon_L6_ *) % 1.30/1.47 assert (zenon_L7_ : forall (zenon_TX_bu : zenon_U) (zenon_TX1_bi : zenon_U) (zenon_TX1_bc : zenon_U), (~(exists Z : zenon_U, ((grain Z)/\((eats zenon_TX1_bc Z)/\(eats zenon_TX1_bi zenon_TX1_bc))))) -> (grain zenon_TX_bu) -> (eats zenon_TX1_bc zenon_TX_bu) -> (eats zenon_TX1_bi zenon_TX1_bc) -> False). % 1.30/1.47 do 3 intro. intros zenon_H41 zenon_H2d zenon_H42 zenon_H43. % 1.30/1.47 apply zenon_H41. exists zenon_TX_bu. apply NNPP. zenon_intro zenon_H44. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H44); [ zenon_intro zenon_H32 | zenon_intro zenon_H45 ]. % 1.30/1.47 exact (zenon_H32 zenon_H2d). % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H45); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 1.30/1.47 exact (zenon_H47 zenon_H42). % 1.30/1.47 exact (zenon_H46 zenon_H43). % 1.30/1.47 (* end of lemma zenon_L7_ *) % 1.30/1.47 assert (zenon_L8_ : forall (zenon_TX_bu : zenon_U) (zenon_TX1_bc : zenon_U) (zenon_TX1_bi : zenon_U), (~(exists Y : zenon_U, ((animal zenon_TX1_bi)/\((animal Y)/\(exists Z : zenon_U, ((grain Z)/\((eats Y Z)/\(eats zenon_TX1_bi Y)))))))) -> (fox zenon_TX1_bi) -> (bird zenon_TX1_bc) -> (grain zenon_TX_bu) -> (eats zenon_TX1_bc zenon_TX_bu) -> (eats zenon_TX1_bi zenon_TX1_bc) -> False). % 1.30/1.47 do 3 intro. intros zenon_H48 zenon_H20 zenon_H1a zenon_H2d zenon_H42 zenon_H43. % 1.30/1.47 apply zenon_H48. exists zenon_TX1_bc. apply NNPP. zenon_intro zenon_H49. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H21 | zenon_intro zenon_H4a ]. % 1.30/1.47 apply (zenon_L3_ zenon_TX1_bi); trivial. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H4a); [ zenon_intro zenon_H1b | zenon_intro zenon_H41 ]. % 1.30/1.47 apply (zenon_L2_ zenon_TX1_bc); trivial. % 1.30/1.47 apply (zenon_L7_ zenon_TX_bu zenon_TX1_bi zenon_TX1_bc); trivial. % 1.30/1.47 (* end of lemma zenon_L8_ *) % 1.30/1.47 assert (zenon_L9_ : forall (zenon_TX1_bi : zenon_U) (zenon_TX1_bc : zenon_U) (zenon_TX_bu : zenon_U), (grain zenon_TX_bu) -> (forall Y : zenon_U, ((plant Y)->(eats zenon_TX1_bc Y))) -> (~(exists X : zenon_U, (exists Y : zenon_U, ((animal X)/\((animal Y)/\(exists Z : zenon_U, ((grain Z)/\((eats Y Z)/\(eats X Y))))))))) -> (fox zenon_TX1_bi) -> (much_smaller zenon_TX1_bc zenon_TX1_bi) -> (bird zenon_TX1_bc) -> (forall Y1 : zenon_U, (((animal Y1)/\((much_smaller Y1 zenon_TX1_bi)/\(exists Z : zenon_U, ((plant Z)/\(eats Y1 Z)))))->(eats zenon_TX1_bi Y1))) -> False). % 1.30/1.47 do 3 intro. intros zenon_H2d zenon_H4b zenon_G zenon_H20 zenon_H4c zenon_H1a zenon_H4d. % 1.30/1.47 generalize (pel47_6_2 zenon_TX_bu). zenon_intro zenon_H30. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H30); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 1.30/1.47 exact (zenon_H32 zenon_H2d). % 1.30/1.47 generalize (zenon_H4b zenon_TX_bu). zenon_intro zenon_H4e. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H4e); [ zenon_intro zenon_H35 | zenon_intro zenon_H42 ]. % 1.30/1.47 exact (zenon_H35 zenon_H31). % 1.30/1.47 apply zenon_G. exists zenon_TX1_bi. apply NNPP. zenon_intro zenon_H48. % 1.30/1.47 generalize (zenon_H4d zenon_TX1_bc). zenon_intro zenon_H4f. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H4f); [ zenon_intro zenon_H50 | zenon_intro zenon_H43 ]. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H1b | zenon_intro zenon_H51 ]. % 1.30/1.47 apply (zenon_L2_ zenon_TX1_bc); trivial. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H51); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 1.30/1.47 exact (zenon_H53 zenon_H4c). % 1.30/1.47 apply zenon_H52. exists zenon_TX_bu. apply NNPP. zenon_intro zenon_H54. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H54); [ zenon_intro zenon_H35 | zenon_intro zenon_H47 ]. % 1.30/1.47 exact (zenon_H35 zenon_H31). % 1.30/1.47 exact (zenon_H47 zenon_H42). % 1.30/1.47 apply (zenon_L8_ zenon_TX_bu zenon_TX1_bc zenon_TX1_bi); trivial. % 1.30/1.47 (* end of lemma zenon_L9_ *) % 1.30/1.47 assert (zenon_L10_ : forall (zenon_TX1_x : zenon_U) (zenon_TX1_bc : zenon_U), (forall Y : zenon_U, (((bird zenon_TX1_bc)/\(snail Y))->(~(eats zenon_TX1_bc Y)))) -> (bird zenon_TX1_bc) -> (snail zenon_TX1_x) -> (eats zenon_TX1_bc zenon_TX1_x) -> False). % 1.30/1.47 do 2 intro. intros zenon_H55 zenon_H1a zenon_H16 zenon_H56. % 1.30/1.47 generalize (zenon_H55 zenon_TX1_x). zenon_intro zenon_H57. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H57); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H59); [ zenon_intro zenon_H1f | zenon_intro zenon_H19 ]. % 1.30/1.47 exact (zenon_H1f zenon_H1a). % 1.30/1.47 exact (zenon_H19 zenon_H16). % 1.30/1.47 exact (zenon_H58 zenon_H56). % 1.30/1.47 (* end of lemma zenon_L10_ *) % 1.30/1.47 assert (zenon_L11_ : forall (zenon_TX1_x : zenon_U) (zenon_TX1_bc : zenon_U), (forall Y1 : zenon_U, (((animal Y1)/\((much_smaller Y1 zenon_TX1_bc)/\(exists Z : zenon_U, ((plant Z)/\(eats Y1 Z)))))->(eats zenon_TX1_bc Y1))) -> (animal zenon_TX1_x) -> (much_smaller zenon_TX1_x zenon_TX1_bc) -> (snail zenon_TX1_x) -> (forall Y : zenon_U, (((bird zenon_TX1_bc)/\(snail Y))->(~(eats zenon_TX1_bc Y)))) -> (bird zenon_TX1_bc) -> False). % 1.30/1.47 do 2 intro. intros zenon_H5a zenon_H5b zenon_H5c zenon_H16 zenon_H55 zenon_H1a. % 1.30/1.47 generalize (zenon_H5a zenon_TX1_x). zenon_intro zenon_H5d. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H5d); [ zenon_intro zenon_H5e | zenon_intro zenon_H56 ]. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H60 | zenon_intro zenon_H5f ]. % 1.30/1.47 exact (zenon_H60 zenon_H5b). % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H5f); [ zenon_intro zenon_H62 | zenon_intro zenon_H61 ]. % 1.30/1.47 exact (zenon_H62 zenon_H5c). % 1.30/1.47 generalize (pel47_14 zenon_TX1_x). zenon_intro zenon_H63. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 1.30/1.47 apply (zenon_notor_s _ _ zenon_H65). zenon_intro zenon_H18. zenon_intro zenon_H19. % 1.30/1.47 exact (zenon_H19 zenon_H16). % 1.30/1.47 exact (zenon_H61 zenon_H64). % 1.30/1.47 apply (zenon_L10_ zenon_TX1_x zenon_TX1_bc); trivial. % 1.30/1.47 (* end of lemma zenon_L11_ *) % 1.30/1.47 assert (zenon_L12_ : forall (zenon_TX1_x : zenon_U) (zenon_TX1_bc : zenon_U), (bird zenon_TX1_bc) -> (much_smaller zenon_TX1_x zenon_TX1_bc) -> (forall Y1 : zenon_U, (((animal Y1)/\((much_smaller Y1 zenon_TX1_bc)/\(exists Z : zenon_U, ((plant Z)/\(eats Y1 Z)))))->(eats zenon_TX1_bc Y1))) -> (snail zenon_TX1_x) -> False). % 1.30/1.47 do 2 intro. intros zenon_H1a zenon_H5c zenon_H5a zenon_H16. % 1.30/1.47 generalize (pel47_13 zenon_TX1_bc). zenon_intro zenon_H55. % 1.30/1.47 generalize (pel47_5_1 zenon_TX1_x). zenon_intro zenon_H66. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H66); [ zenon_intro zenon_H19 | zenon_intro zenon_H5b ]. % 1.30/1.47 exact (zenon_H19 zenon_H16). % 1.30/1.47 apply (zenon_L11_ zenon_TX1_x zenon_TX1_bc); trivial. % 1.30/1.47 (* end of lemma zenon_L12_ *) % 1.30/1.47 apply NNPP. intro zenon_G. % 1.30/1.47 elim pel47_1_2. zenon_intro zenon_TX1_bo. zenon_intro zenon_H26. % 1.30/1.47 elim pel47_2_2. zenon_intro zenon_TX1_bi. zenon_intro zenon_H20. % 1.30/1.47 elim pel47_3_2. zenon_intro zenon_TX1_bc. zenon_intro zenon_H1a. % 1.30/1.47 elim pel47_4_2. zenon_intro zenon_TX1_dz. zenon_intro zenon_H68. % 1.30/1.47 elim pel47_5_2. zenon_intro zenon_TX1_x. zenon_intro zenon_H16. % 1.30/1.47 elim pel47_6_1. zenon_intro zenon_TX_bu. zenon_intro zenon_H2d. % 1.30/1.47 generalize (pel47_8 zenon_TX1_x). zenon_intro zenon_H69. % 1.30/1.47 generalize (pel47_9 zenon_TX1_bc). zenon_intro zenon_H6a. % 1.30/1.47 generalize (pel47_10 zenon_TX1_bi). zenon_intro zenon_H6b. % 1.30/1.47 generalize (pel47_14 zenon_TX1_dz). zenon_intro zenon_H6c. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 1.30/1.47 apply (zenon_notor_s _ _ zenon_H6e). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 1.30/1.47 exact (zenon_H70 zenon_H68). % 1.30/1.47 elim zenon_H6d. zenon_intro zenon_TY_ej. zenon_intro zenon_H72. % 1.30/1.47 apply (zenon_and_s _ _ zenon_H72). zenon_intro zenon_H74. zenon_intro zenon_H73. % 1.30/1.47 generalize (zenon_H69 zenon_TX1_bc). zenon_intro zenon_H75. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H75); [ zenon_intro zenon_H76 | zenon_intro zenon_H5c ]. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H1f | zenon_intro zenon_H15 ]. % 1.30/1.47 exact (zenon_H1f zenon_H1a). % 1.30/1.47 apply (zenon_L1_ zenon_TX1_x); trivial. % 1.30/1.47 generalize (pel47_7 zenon_TX1_bc). zenon_intro zenon_H77. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H77); [ zenon_intro zenon_H1b | zenon_intro zenon_H78 ]. % 1.30/1.47 apply (zenon_L2_ zenon_TX1_bc); trivial. % 1.30/1.47 apply (zenon_or_s _ _ zenon_H78); [ zenon_intro zenon_H4b | zenon_intro zenon_H5a ]. % 1.30/1.47 generalize (zenon_H6a zenon_TX1_bi). zenon_intro zenon_H79. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H79); [ zenon_intro zenon_H7a | zenon_intro zenon_H4c ]. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H1f | zenon_intro zenon_H25 ]. % 1.30/1.47 exact (zenon_H1f zenon_H1a). % 1.30/1.47 exact (zenon_H25 zenon_H20). % 1.30/1.47 generalize (zenon_H6b zenon_TX1_bo). zenon_intro zenon_H7b. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H7d | zenon_intro zenon_H7c ]. % 1.30/1.47 apply (zenon_notand_s _ _ zenon_H7d); [ zenon_intro zenon_H25 | zenon_intro zenon_H2b ]. % 1.30/1.47 exact (zenon_H25 zenon_H20). % 1.30/1.47 exact (zenon_H2b zenon_H26). % 1.30/1.47 generalize (pel47_7 zenon_TX1_bi). zenon_intro zenon_H7e. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H21 | zenon_intro zenon_H7f ]. % 1.30/1.47 apply (zenon_L3_ zenon_TX1_bi); trivial. % 1.30/1.47 apply (zenon_or_s _ _ zenon_H7f); [ zenon_intro zenon_H80 | zenon_intro zenon_H4d ]. % 1.30/1.47 generalize (zenon_H80 zenon_TY_ej). zenon_intro zenon_H81. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H81); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 1.30/1.47 exact (zenon_H83 zenon_H74). % 1.30/1.47 generalize (pel47_7 zenon_TX1_bo). zenon_intro zenon_H84. % 1.30/1.47 apply (zenon_imply_s _ _ zenon_H84); [ zenon_intro zenon_H27 | zenon_intro zenon_H85 ]. % 1.30/1.48 apply (zenon_L4_ zenon_TX1_bo); trivial. % 1.30/1.48 apply (zenon_or_s _ _ zenon_H85); [ zenon_intro zenon_H2c | zenon_intro zenon_H86 ]. % 1.30/1.48 apply (zenon_L5_ zenon_TX_bu zenon_TX1_bo); trivial. % 1.30/1.48 generalize (pel47_11 zenon_TX1_bo). zenon_intro zenon_H2f. % 1.30/1.48 generalize (pel47_2_1 zenon_TX1_bi). zenon_intro zenon_H23. % 1.30/1.48 apply (zenon_imply_s _ _ zenon_H23); [ zenon_intro zenon_H25 | zenon_intro zenon_H24 ]. % 1.30/1.48 exact (zenon_H25 zenon_H20). % 1.30/1.48 generalize (zenon_H86 zenon_TX1_bi). zenon_intro zenon_H87. % 1.30/1.48 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H88 | zenon_intro zenon_H3b ]. % 1.30/1.48 apply (zenon_notand_s _ _ zenon_H88); [ zenon_intro zenon_H21 | zenon_intro zenon_H89 ]. % 1.30/1.48 exact (zenon_H21 zenon_H24). % 1.30/1.48 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H8b | zenon_intro zenon_H8a ]. % 1.30/1.48 exact (zenon_H8b zenon_H7c). % 1.30/1.48 apply zenon_H8a. exists zenon_TY_ej. apply NNPP. zenon_intro zenon_H8c. % 1.30/1.48 apply (zenon_notand_s _ _ zenon_H8c); [ zenon_intro zenon_H83 | zenon_intro zenon_H8d ]. % 1.30/1.48 exact (zenon_H83 zenon_H74). % 1.30/1.48 exact (zenon_H8d zenon_H82). % 1.30/1.48 apply (zenon_L6_ zenon_TX1_bi zenon_TX1_bo); trivial. % 1.30/1.48 apply (zenon_L9_ zenon_TX1_bi zenon_TX1_bc zenon_TX_bu); trivial. % 1.30/1.48 apply (zenon_L12_ zenon_TX1_x zenon_TX1_bc); trivial. % 1.30/1.48 Qed. % 1.30/1.48 % SZS output end Proof % 1.30/1.48 (* END-PROOF *) % 1.30/1.48 nodes searched: 63933 % 1.30/1.48 max branch formulas: 7552 % 1.30/1.48 proof nodes created: 2186 % 1.30/1.48 formulas created: 141319 % 1.30/1.48 %------------------------------------------------------------------------------