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