%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NLP004+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n005.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 05:53:17 EDT 2022 % Result : Theorem 137.57s 137.81s % Output : Proof 137.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP004+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n005.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jul 1 01:00:07 EDT 2022 % 0.13/0.34 % CPUTime : % 137.57/137.81 (* PROOF-FOUND *) % 137.57/137.81 % SZS status Theorem % 137.57/137.81 (* BEGIN-PROOF *) % 137.57/137.81 % SZS output start Proof % 137.57/137.81 Theorem co1 : (((exists U : zenon_U, (exists V : zenon_U, (exists W : zenon_U, (exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, (exists X1 : zenon_U, (exists X2 : zenon_U, (exists X4 : zenon_U, (exists X5 : zenon_U, ((seat U)/\((furniture U)/\((front U)/\((seat V)/\((furniture V)/\((front V)/\((hollywood W)/\((city W)/\((event X)/\((street Y)/\((way Y)/\((lonely Y)/\((chevy Z)/\((car Z)/\((white Z)/\((dirty Z)/\((old Z)/\((barrel X Z)/\((down X Y)/\((in X W)/\((~(X1 = X2))/\((fellow X1)/\((man X1)/\((young X1)/\((fellow X2)/\((man X2)/\((young X2)/\((X1 = X4)/\((in X4 U)/\((X2 = X5)/\(in X5 V)))))))))))))))))))))))))))))))))))))))))->(exists X6 : zenon_U, (exists X7 : zenon_U, (exists X8 : zenon_U, (exists X9 : zenon_U, (exists X10 : zenon_U, (exists X11 : zenon_U, (exists X12 : zenon_U, (exists X13 : zenon_U, (exists X15 : zenon_U, (exists X16 : zenon_U, ((seat X6)/\((furniture X6)/\((front X6)/\((seat X7)/\((furniture X7)/\((front X7)/\((hollywood X8)/\((city X8)/\((event X9)/\((chevy X10)/\((car X10)/\((white X10)/\((dirty X10)/\((old X10)/\((street X11)/\((way X11)/\((lonely X11)/\((barrel X9 X10)/\((down X9 X11)/\((in X9 X8)/\((~(X12 = X13))/\((fellow X12)/\((man X12)/\((young X12)/\((fellow X13)/\((man X13)/\((young X13)/\((X12 = X15)/\((in X15 X6)/\((X13 = X16)/\(in X16 X7))))))))))))))))))))))))))))))))))))))))))/\((exists X6 : zenon_U, (exists X7 : zenon_U, (exists X8 : zenon_U, (exists X9 : zenon_U, (exists X10 : zenon_U, (exists X11 : zenon_U, (exists X12 : zenon_U, (exists X13 : zenon_U, (exists X15 : zenon_U, (exists X16 : zenon_U, ((seat X6)/\((furniture X6)/\((front X6)/\((seat X7)/\((furniture X7)/\((front X7)/\((hollywood X8)/\((city X8)/\((event X9)/\((chevy X10)/\((car X10)/\((white X10)/\((dirty X10)/\((old X10)/\((street X11)/\((way X11)/\((lonely X11)/\((barrel X9 X10)/\((down X9 X11)/\((in X9 X8)/\((~(X12 = X13))/\((fellow X12)/\((man X12)/\((young X12)/\((fellow X13)/\((man X13)/\((young X13)/\((X12 = X15)/\((in X15 X6)/\((X13 = X16)/\(in X16 X7)))))))))))))))))))))))))))))))))))))))))->(exists U : zenon_U, (exists V : zenon_U, (exists W : zenon_U, (exists X : zenon_U, (exists Y : zenon_U, (exists Z : zenon_U, (exists X1 : zenon_U, (exists X2 : zenon_U, (exists X4 : zenon_U, (exists X5 : zenon_U, ((seat U)/\((furniture U)/\((front U)/\((seat V)/\((furniture V)/\((front V)/\((hollywood W)/\((city W)/\((event X)/\((street Y)/\((way Y)/\((lonely Y)/\((chevy Z)/\((car Z)/\((white Z)/\((dirty Z)/\((old Z)/\((barrel X Z)/\((down X Y)/\((in X W)/\((~(X1 = X2))/\((fellow X1)/\((man X1)/\((young X1)/\((fellow X2)/\((man X2)/\((young X2)/\((X1 = X4)/\((in X4 U)/\((X2 = X5)/\(in X5 V))))))))))))))))))))))))))))))))))))))))))). % 137.57/137.81 Proof. % 137.57/137.81 assert (zenon_L1_ : forall (zenon_TX4_e : zenon_U) (zenon_TU_f : zenon_U) (zenon_TX1_g : zenon_U), (~(in zenon_TX1_g zenon_TU_f)) -> (in zenon_TX4_e zenon_TU_f) -> (zenon_TX1_g = zenon_TX4_e) -> False). % 137.57/137.81 do 3 intro. intros zenon_H1 zenon_H2 zenon_H3. % 137.57/137.81 cut ((in zenon_TX4_e zenon_TU_f) = (in zenon_TX1_g zenon_TU_f)). % 137.57/137.81 intro zenon_D_pnotp. % 137.57/137.81 apply zenon_H1. % 137.57/137.81 rewrite <- zenon_D_pnotp. % 137.57/137.81 exact zenon_H2. % 137.57/137.81 cut ((zenon_TU_f = zenon_TU_f)); [idtac | apply NNPP; zenon_intro zenon_H7]. % 137.57/137.81 cut ((zenon_TX4_e = zenon_TX1_g)); [idtac | apply NNPP; zenon_intro zenon_H8]. % 137.57/137.81 congruence. % 137.57/137.81 apply zenon_H8. apply sym_equal. exact zenon_H3. % 137.57/137.81 apply zenon_H7. apply refl_equal. % 137.57/137.81 (* end of lemma zenon_L1_ *) % 137.57/137.81 assert (zenon_L2_ : forall (zenon_TX15_m : zenon_U) (zenon_TX6_n : zenon_U) (zenon_TX12_o : zenon_U), (~(in zenon_TX12_o zenon_TX6_n)) -> (in zenon_TX15_m zenon_TX6_n) -> (zenon_TX12_o = zenon_TX15_m) -> False). % 137.57/137.81 do 3 intro. intros zenon_H9 zenon_Ha zenon_Hb. % 137.57/137.81 cut ((in zenon_TX15_m zenon_TX6_n) = (in zenon_TX12_o zenon_TX6_n)). % 137.57/137.81 intro zenon_D_pnotp. % 137.57/137.81 apply zenon_H9. % 137.57/137.81 rewrite <- zenon_D_pnotp. % 137.57/137.81 exact zenon_Ha. % 137.57/137.81 cut ((zenon_TX6_n = zenon_TX6_n)); [idtac | apply NNPP; zenon_intro zenon_Hf]. % 137.57/137.81 cut ((zenon_TX15_m = zenon_TX12_o)); [idtac | apply NNPP; zenon_intro zenon_H10]. % 137.57/137.81 congruence. % 137.57/137.81 apply zenon_H10. apply sym_equal. exact zenon_Hb. % 137.57/137.81 apply zenon_Hf. apply refl_equal. % 137.57/137.81 (* end of lemma zenon_L2_ *) % 137.57/137.81 apply NNPP. intro zenon_G. % 137.57/137.81 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H12 | zenon_intro zenon_H11 ]. % 137.57/137.81 apply (zenon_notimply_s _ _ zenon_H12). zenon_intro zenon_H14. zenon_intro zenon_H13. % 137.57/137.81 elim zenon_H14. zenon_intro zenon_TU_f. zenon_intro zenon_H15. % 137.57/137.81 elim zenon_H15. zenon_intro zenon_TV_w. zenon_intro zenon_H17. % 137.57/137.81 elim zenon_H17. zenon_intro zenon_TW_y. zenon_intro zenon_H19. % 137.57/137.81 elim zenon_H19. zenon_intro zenon_TX_ba. zenon_intro zenon_H1b. % 137.57/137.81 elim zenon_H1b. zenon_intro zenon_TY_bc. zenon_intro zenon_H1d. % 137.57/137.81 elim zenon_H1d. zenon_intro zenon_TZ_be. zenon_intro zenon_H1f. % 137.57/137.81 elim zenon_H1f. zenon_intro zenon_TX1_g. zenon_intro zenon_H20. % 137.57/137.81 elim zenon_H20. zenon_intro zenon_TX2_bh. zenon_intro zenon_H22. % 137.57/137.81 elim zenon_H22. zenon_intro zenon_TX4_e. zenon_intro zenon_H23. % 137.57/137.81 elim zenon_H23. zenon_intro zenon_TX5_bk. zenon_intro zenon_H25. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H25). zenon_intro zenon_H27. zenon_intro zenon_H26. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H2a). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H31. zenon_intro zenon_H30. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H38). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H42). zenon_intro zenon_H45. zenon_intro zenon_H44. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H46). zenon_intro zenon_H49. zenon_intro zenon_H48. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H4c). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H4e). zenon_intro zenon_H51. zenon_intro zenon_H50. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H50). zenon_intro zenon_H53. zenon_intro zenon_H52. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H52). zenon_intro zenon_H55. zenon_intro zenon_H54. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H54). zenon_intro zenon_H57. zenon_intro zenon_H56. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5b. zenon_intro zenon_H5a. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H5a). zenon_intro zenon_H3. zenon_intro zenon_H5c. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H5c). zenon_intro zenon_H2. zenon_intro zenon_H5d. % 137.57/137.81 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 137.57/137.81 apply zenon_H13. exists zenon_TV_w. apply NNPP. zenon_intro zenon_H60. % 137.57/137.81 apply zenon_H60. exists zenon_TU_f. apply NNPP. zenon_intro zenon_H61. % 137.57/137.81 apply zenon_H61. exists zenon_TW_y. apply NNPP. zenon_intro zenon_H62. % 137.57/137.81 apply zenon_H62. exists zenon_TX_ba. apply NNPP. zenon_intro zenon_H63. % 137.57/137.81 apply zenon_H63. exists zenon_TZ_be. apply NNPP. zenon_intro zenon_H64. % 137.57/137.81 apply zenon_H64. exists zenon_TY_bc. apply NNPP. zenon_intro zenon_H65. % 137.57/137.81 apply zenon_H65. exists zenon_TX2_bh. apply NNPP. zenon_intro zenon_H66. % 137.57/137.81 apply zenon_H66. exists zenon_TX1_g. apply NNPP. zenon_intro zenon_H67. % 137.57/137.81 apply zenon_H67. exists zenon_TX5_bk. apply NNPP. zenon_intro zenon_H68. % 137.57/137.81 apply zenon_H68. exists zenon_TX1_g. apply NNPP. zenon_intro zenon_H69. % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H69); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 137.57/137.81 exact (zenon_H6b zenon_H2d). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 137.57/137.81 exact (zenon_H6d zenon_H2f). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 137.57/137.81 exact (zenon_H6f zenon_H31). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 137.57/137.81 exact (zenon_H71 zenon_H27). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 137.57/137.81 exact (zenon_H73 zenon_H29). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 137.57/137.81 exact (zenon_H75 zenon_H2b). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H74); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 137.57/137.81 exact (zenon_H77 zenon_H33). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H79 | zenon_intro zenon_H78 ]. % 137.57/137.81 exact (zenon_H79 zenon_H35). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H78); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 137.57/137.81 exact (zenon_H7b zenon_H37). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H7d | zenon_intro zenon_H7c ]. % 137.57/137.81 exact (zenon_H7d zenon_H3f). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H7c); [ zenon_intro zenon_H7f | zenon_intro zenon_H7e ]. % 137.57/137.81 exact (zenon_H7f zenon_H41). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H81 | zenon_intro zenon_H80 ]. % 137.57/137.81 exact (zenon_H81 zenon_H43). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H80); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 137.57/137.81 exact (zenon_H83 zenon_H45). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H82); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 137.57/137.81 exact (zenon_H85 zenon_H47). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H87 | zenon_intro zenon_H86 ]. % 137.57/137.81 exact (zenon_H87 zenon_H39). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H86); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 137.57/137.81 exact (zenon_H89 zenon_H3b). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H88); [ zenon_intro zenon_H8b | zenon_intro zenon_H8a ]. % 137.57/137.81 exact (zenon_H8b zenon_H3d). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 137.57/137.81 exact (zenon_H8d zenon_H49). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H8c); [ zenon_intro zenon_H8f | zenon_intro zenon_H8e ]. % 137.57/137.81 exact (zenon_H8f zenon_H4b). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H8e); [ zenon_intro zenon_H91 | zenon_intro zenon_H90 ]. % 137.57/137.81 exact (zenon_H91 zenon_H4d). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H90); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 137.57/137.81 apply zenon_H93. zenon_intro zenon_H94. % 137.57/137.81 apply zenon_H4f. apply sym_equal. exact zenon_H94. % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H92); [ zenon_intro zenon_H96 | zenon_intro zenon_H95 ]. % 137.57/137.81 exact (zenon_H96 zenon_H57). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H98 | zenon_intro zenon_H97 ]. % 137.57/137.81 exact (zenon_H98 zenon_H59). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H97); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 137.57/137.81 exact (zenon_H9a zenon_H5b). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H99); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 137.57/137.81 exact (zenon_H9c zenon_H51). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H9e | zenon_intro zenon_H9d ]. % 137.57/137.81 exact (zenon_H9e zenon_H53). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H9d); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H9f ]. % 137.57/137.81 exact (zenon_Ha0 zenon_H55). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H9f); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1 ]. % 137.57/137.81 exact (zenon_Ha2 zenon_H5f). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha3 ]. % 137.57/137.81 exact (zenon_Ha4 zenon_H5e). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha5 | zenon_intro zenon_H1 ]. % 137.57/137.81 apply zenon_Ha5. apply refl_equal. % 137.57/137.81 apply (zenon_L1_ zenon_TX4_e zenon_TU_f zenon_TX1_g); trivial. % 137.57/137.81 apply (zenon_notimply_s _ _ zenon_H11). zenon_intro zenon_Ha7. zenon_intro zenon_Ha6. % 137.57/137.81 elim zenon_Ha7. zenon_intro zenon_TX6_n. zenon_intro zenon_Ha8. % 137.57/137.81 elim zenon_Ha8. zenon_intro zenon_TX7_gn. zenon_intro zenon_Haa. % 137.57/137.81 elim zenon_Haa. zenon_intro zenon_TX8_gp. zenon_intro zenon_Hac. % 137.57/137.81 elim zenon_Hac. zenon_intro zenon_TX9_gr. zenon_intro zenon_Hae. % 137.57/137.81 elim zenon_Hae. zenon_intro zenon_TX10_gt. zenon_intro zenon_Hb0. % 137.57/137.81 elim zenon_Hb0. zenon_intro zenon_TX11_gv. zenon_intro zenon_Hb2. % 137.57/137.81 elim zenon_Hb2. zenon_intro zenon_TX12_o. zenon_intro zenon_Hb3. % 137.57/137.81 elim zenon_Hb3. zenon_intro zenon_TX13_gy. zenon_intro zenon_Hb5. % 137.57/137.81 elim zenon_Hb5. zenon_intro zenon_TX15_m. zenon_intro zenon_Hb6. % 137.57/137.81 elim zenon_Hb6. zenon_intro zenon_TX16_hb. zenon_intro zenon_Hb8. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hb8). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Hbc. zenon_intro zenon_Hbb. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hbb). zenon_intro zenon_Hbe. zenon_intro zenon_Hbd. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hbd). zenon_intro zenon_Hc0. zenon_intro zenon_Hbf. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hbf). zenon_intro zenon_Hc2. zenon_intro zenon_Hc1. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hc1). zenon_intro zenon_Hc4. zenon_intro zenon_Hc3. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hc3). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_Hca. zenon_intro zenon_Hc9. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_Hcc. zenon_intro zenon_Hcb. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hcb). zenon_intro zenon_Hce. zenon_intro zenon_Hcd. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hcd). zenon_intro zenon_Hd0. zenon_intro zenon_Hcf. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_Hd2. zenon_intro zenon_Hd1. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hd1). zenon_intro zenon_Hd4. zenon_intro zenon_Hd3. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hd3). zenon_intro zenon_Hd6. zenon_intro zenon_Hd5. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hd5). zenon_intro zenon_Hd8. zenon_intro zenon_Hd7. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hd7). zenon_intro zenon_Hda. zenon_intro zenon_Hd9. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hd9). zenon_intro zenon_Hdc. zenon_intro zenon_Hdb. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hdb). zenon_intro zenon_Hde. zenon_intro zenon_Hdd. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hdd). zenon_intro zenon_He0. zenon_intro zenon_Hdf. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hdf). zenon_intro zenon_He2. zenon_intro zenon_He1. % 137.57/137.81 apply (zenon_and_s _ _ zenon_He1). zenon_intro zenon_He4. zenon_intro zenon_He3. % 137.57/137.81 apply (zenon_and_s _ _ zenon_He3). zenon_intro zenon_He6. zenon_intro zenon_He5. % 137.57/137.81 apply (zenon_and_s _ _ zenon_He5). zenon_intro zenon_He8. zenon_intro zenon_He7. % 137.57/137.81 apply (zenon_and_s _ _ zenon_He7). zenon_intro zenon_Hea. zenon_intro zenon_He9. % 137.57/137.81 apply (zenon_and_s _ _ zenon_He9). zenon_intro zenon_Hec. zenon_intro zenon_Heb. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Heb). zenon_intro zenon_Hee. zenon_intro zenon_Hed. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hed). zenon_intro zenon_Hb. zenon_intro zenon_Hef. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hef). zenon_intro zenon_Ha. zenon_intro zenon_Hf0. % 137.57/137.81 apply (zenon_and_s _ _ zenon_Hf0). zenon_intro zenon_Hf2. zenon_intro zenon_Hf1. % 137.57/137.81 apply zenon_Ha6. exists zenon_TX7_gn. apply NNPP. zenon_intro zenon_Hf3. % 137.57/137.81 apply zenon_Hf3. exists zenon_TX6_n. apply NNPP. zenon_intro zenon_Hf4. % 137.57/137.81 apply zenon_Hf4. exists zenon_TX8_gp. apply NNPP. zenon_intro zenon_Hf5. % 137.57/137.81 apply zenon_Hf5. exists zenon_TX9_gr. apply NNPP. zenon_intro zenon_Hf6. % 137.57/137.81 apply zenon_Hf6. exists zenon_TX11_gv. apply NNPP. zenon_intro zenon_Hf7. % 137.57/137.81 apply zenon_Hf7. exists zenon_TX10_gt. apply NNPP. zenon_intro zenon_Hf8. % 137.57/137.81 apply zenon_Hf8. exists zenon_TX13_gy. apply NNPP. zenon_intro zenon_Hf9. % 137.57/137.81 apply zenon_Hf9. exists zenon_TX12_o. apply NNPP. zenon_intro zenon_Hfa. % 137.57/137.81 apply zenon_Hfa. exists zenon_TX16_hb. apply NNPP. zenon_intro zenon_Hfb. % 137.57/137.81 apply zenon_Hfb. exists zenon_TX12_o. apply NNPP. zenon_intro zenon_Hfc. % 137.57/137.81 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hfe | zenon_intro zenon_Hfd ]. % 137.57/137.81 exact (zenon_Hfe zenon_Hc0). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_Hfd); [ zenon_intro zenon_H100 | zenon_intro zenon_Hff ]. % 137.57/137.81 exact (zenon_H100 zenon_Hc2). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_Hff); [ zenon_intro zenon_H102 | zenon_intro zenon_H101 ]. % 137.57/137.81 exact (zenon_H102 zenon_Hc4). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H101); [ zenon_intro zenon_H104 | zenon_intro zenon_H103 ]. % 137.57/137.81 exact (zenon_H104 zenon_Hba). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_H106 | zenon_intro zenon_H105 ]. % 137.57/137.81 exact (zenon_H106 zenon_Hbc). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_H108 | zenon_intro zenon_H107 ]. % 137.57/137.81 exact (zenon_H108 zenon_Hbe). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H107); [ zenon_intro zenon_H10a | zenon_intro zenon_H109 ]. % 137.57/137.81 exact (zenon_H10a zenon_Hc6). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H109); [ zenon_intro zenon_H10c | zenon_intro zenon_H10b ]. % 137.57/137.81 exact (zenon_H10c zenon_Hc8). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H10b); [ zenon_intro zenon_H10e | zenon_intro zenon_H10d ]. % 137.57/137.81 exact (zenon_H10e zenon_Hca). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H10d); [ zenon_intro zenon_H110 | zenon_intro zenon_H10f ]. % 137.57/137.81 exact (zenon_H110 zenon_Hd6). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H10f); [ zenon_intro zenon_H112 | zenon_intro zenon_H111 ]. % 137.57/137.81 exact (zenon_H112 zenon_Hd8). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H111); [ zenon_intro zenon_H114 | zenon_intro zenon_H113 ]. % 137.57/137.81 exact (zenon_H114 zenon_Hda). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H113); [ zenon_intro zenon_H116 | zenon_intro zenon_H115 ]. % 137.57/137.81 exact (zenon_H116 zenon_Hcc). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H115); [ zenon_intro zenon_H118 | zenon_intro zenon_H117 ]. % 137.57/137.81 exact (zenon_H118 zenon_Hce). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H117); [ zenon_intro zenon_H11a | zenon_intro zenon_H119 ]. % 137.57/137.81 exact (zenon_H11a zenon_Hd0). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H119); [ zenon_intro zenon_H11c | zenon_intro zenon_H11b ]. % 137.57/137.81 exact (zenon_H11c zenon_Hd2). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H11b); [ zenon_intro zenon_H11e | zenon_intro zenon_H11d ]. % 137.57/137.81 exact (zenon_H11e zenon_Hd4). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H11d); [ zenon_intro zenon_H120 | zenon_intro zenon_H11f ]. % 137.57/137.81 exact (zenon_H120 zenon_Hdc). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H11f); [ zenon_intro zenon_H122 | zenon_intro zenon_H121 ]. % 137.57/137.81 exact (zenon_H122 zenon_Hde). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H121); [ zenon_intro zenon_H124 | zenon_intro zenon_H123 ]. % 137.57/137.81 exact (zenon_H124 zenon_He0). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H123); [ zenon_intro zenon_H126 | zenon_intro zenon_H125 ]. % 137.57/137.81 apply zenon_H126. zenon_intro zenon_H127. % 137.57/137.81 apply zenon_He2. apply sym_equal. exact zenon_H127. % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H125); [ zenon_intro zenon_H129 | zenon_intro zenon_H128 ]. % 137.57/137.81 exact (zenon_H129 zenon_Hea). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H128); [ zenon_intro zenon_H12b | zenon_intro zenon_H12a ]. % 137.57/137.81 exact (zenon_H12b zenon_Hec). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H12a); [ zenon_intro zenon_H12d | zenon_intro zenon_H12c ]. % 137.57/137.81 exact (zenon_H12d zenon_Hee). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H12c); [ zenon_intro zenon_H12f | zenon_intro zenon_H12e ]. % 137.57/137.81 exact (zenon_H12f zenon_He4). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H12e); [ zenon_intro zenon_H131 | zenon_intro zenon_H130 ]. % 137.57/137.81 exact (zenon_H131 zenon_He6). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H130); [ zenon_intro zenon_H133 | zenon_intro zenon_H132 ]. % 137.57/137.81 exact (zenon_H133 zenon_He8). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H132); [ zenon_intro zenon_H135 | zenon_intro zenon_H134 ]. % 137.57/137.81 exact (zenon_H135 zenon_Hf2). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H134); [ zenon_intro zenon_H137 | zenon_intro zenon_H136 ]. % 137.57/137.81 exact (zenon_H137 zenon_Hf1). % 137.57/137.81 apply (zenon_notand_s _ _ zenon_H136); [ zenon_intro zenon_H138 | zenon_intro zenon_H9 ]. % 137.57/137.81 apply zenon_H138. apply refl_equal. % 137.57/137.81 apply (zenon_L2_ zenon_TX15_m zenon_TX6_n zenon_TX12_o); trivial. % 137.57/137.81 Qed. % 137.57/137.81 % SZS output end Proof % 137.57/137.81 (* END-PROOF *) % 137.57/137.81 nodes searched: 4143 % 137.57/137.81 max branch formulas: 916 % 137.57/137.81 proof nodes created: 665 % 137.57/137.81 formulas created: 60928 % 137.57/137.81 %------------------------------------------------------------------------------