%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n018.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:21 EDT 2022 % Result : Theorem 11.82s 12.00s % Output : Proof 11.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n018.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 : Fri Jul 1 00:43:47 EDT 2022 % 0.12/0.34 % CPUTime : % 11.82/12.00 (* PROOF-FOUND *) % 11.82/12.00 % SZS status Theorem % 11.82/12.00 (* BEGIN-PROOF *) % 11.82/12.00 % SZS output start Proof % 11.82/12.00 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, ((hollywood U)/\((city U)/\((event V)/\((street W)/\((way W)/\((lonely W)/\((chevy X)/\((car X)/\((white X)/\((dirty X)/\((old X)/\((barrel V X)/\((down V W)/\((in V U)/\((seat X1)/\((furniture X1)/\((front X1)/\((~(Y = Z))/\((fellow Y)/\((man Y)/\((young Y)/\((fellow Z)/\((man Z)/\((young Z)/\((Y = X2)/\((in X2 X1)/\((Z = X3)/\(in X3 X1)))))))))))))))))))))))))))))))))))))->(exists X4 : zenon_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, ((hollywood X4)/\((city X4)/\((event X5)/\((chevy X6)/\((car X6)/\((white X6)/\((dirty X6)/\((old X6)/\((street X7)/\((way X7)/\((lonely X7)/\((barrel X5 X6)/\((down X5 X7)/\((in X5 X4)/\((seat X10)/\((furniture X10)/\((front X10)/\((~(X8 = X9))/\((fellow X8)/\((man X8)/\((young X8)/\((fellow X9)/\((man X9)/\((young X9)/\((X8 = X11)/\((in X11 X10)/\((X9 = X12)/\(in X12 X10))))))))))))))))))))))))))))))))))))))/\((exists X4 : zenon_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, ((hollywood X4)/\((city X4)/\((event X5)/\((chevy X6)/\((car X6)/\((white X6)/\((dirty X6)/\((old X6)/\((street X7)/\((way X7)/\((lonely X7)/\((barrel X5 X6)/\((down X5 X7)/\((in X5 X4)/\((seat X10)/\((furniture X10)/\((front X10)/\((~(X8 = X9))/\((fellow X8)/\((man X8)/\((young X8)/\((fellow X9)/\((man X9)/\((young X9)/\((X8 = X11)/\((in X11 X10)/\((X9 = X12)/\(in X12 X10)))))))))))))))))))))))))))))))))))))->(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, ((hollywood U)/\((city U)/\((event V)/\((street W)/\((way W)/\((lonely W)/\((chevy X)/\((car X)/\((white X)/\((dirty X)/\((old X)/\((barrel V X)/\((down V W)/\((in V U)/\((seat X1)/\((furniture X1)/\((front X1)/\((~(Y = Z))/\((fellow Y)/\((man Y)/\((young Y)/\((fellow Z)/\((man Z)/\((young Z)/\((Y = X2)/\((in X2 X1)/\((Z = X3)/\(in X3 X1))))))))))))))))))))))))))))))))))))))). % 11.82/12.00 Proof. % 11.82/12.00 apply NNPP. intro zenon_G. % 11.82/12.00 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H2 | zenon_intro zenon_H1 ]. % 11.82/12.00 apply (zenon_notimply_s _ _ zenon_H2). zenon_intro zenon_H4. zenon_intro zenon_H3. % 11.82/12.00 elim zenon_H4. zenon_intro zenon_TU_f. zenon_intro zenon_H6. % 11.82/12.00 elim zenon_H6. zenon_intro zenon_TV_h. zenon_intro zenon_H8. % 11.82/12.00 elim zenon_H8. zenon_intro zenon_TW_j. zenon_intro zenon_Ha. % 11.82/12.00 elim zenon_Ha. zenon_intro zenon_TX_l. zenon_intro zenon_Hc. % 11.82/12.00 elim zenon_Hc. zenon_intro zenon_TY_n. zenon_intro zenon_He. % 11.82/12.00 elim zenon_He. zenon_intro zenon_TZ_p. zenon_intro zenon_H10. % 11.82/12.00 elim zenon_H10. zenon_intro zenon_TX1_r. zenon_intro zenon_H12. % 11.82/12.00 elim zenon_H12. zenon_intro zenon_TX2_t. zenon_intro zenon_H14. % 11.82/12.00 elim zenon_H14. zenon_intro zenon_TX3_v. zenon_intro zenon_H16. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H16). zenon_intro zenon_H18. zenon_intro zenon_H17. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H17). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H19). zenon_intro zenon_H1c. zenon_intro zenon_H1b. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H1b). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H1d). zenon_intro zenon_H20. zenon_intro zenon_H1f. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H1f). zenon_intro zenon_H22. zenon_intro zenon_H21. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H24. zenon_intro zenon_H23. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H23). zenon_intro zenon_H26. zenon_intro zenon_H25. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H25). zenon_intro zenon_H28. zenon_intro zenon_H27. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H27). zenon_intro zenon_H2a. zenon_intro zenon_H29. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H29). zenon_intro zenon_H2c. zenon_intro zenon_H2b. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H2b). zenon_intro zenon_H2e. zenon_intro zenon_H2d. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H2d). zenon_intro zenon_H30. zenon_intro zenon_H2f. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H2f). zenon_intro zenon_H32. zenon_intro zenon_H31. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H31). zenon_intro zenon_H34. zenon_intro zenon_H33. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H33). zenon_intro zenon_H36. zenon_intro zenon_H35. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H35). zenon_intro zenon_H38. zenon_intro zenon_H37. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H37). zenon_intro zenon_H3a. zenon_intro zenon_H39. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H3c. zenon_intro zenon_H3b. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H3b). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H3d). zenon_intro zenon_H40. zenon_intro zenon_H3f. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H3f). zenon_intro zenon_H42. zenon_intro zenon_H41. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H41). zenon_intro zenon_H44. zenon_intro zenon_H43. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H43). zenon_intro zenon_H46. zenon_intro zenon_H45. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H45). zenon_intro zenon_H48. zenon_intro zenon_H47. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H47). zenon_intro zenon_H4a. zenon_intro zenon_H49. % 11.82/12.00 apply (zenon_and_s _ _ zenon_H49). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 11.82/12.00 apply zenon_H3. exists zenon_TU_f. apply NNPP. zenon_intro zenon_H4d. % 11.82/12.00 apply zenon_H4d. exists zenon_TV_h. apply NNPP. zenon_intro zenon_H4e. % 11.82/12.00 apply zenon_H4e. exists zenon_TX_l. apply NNPP. zenon_intro zenon_H4f. % 11.82/12.00 apply zenon_H4f. exists zenon_TW_j. apply NNPP. zenon_intro zenon_H50. % 11.82/12.00 apply zenon_H50. exists zenon_TZ_p. apply NNPP. zenon_intro zenon_H51. % 11.82/12.00 apply zenon_H51. exists zenon_TY_n. apply NNPP. zenon_intro zenon_H52. % 11.82/12.00 apply zenon_H52. exists zenon_TX1_r. apply NNPP. zenon_intro zenon_H53. % 11.82/12.00 apply zenon_H53. exists zenon_TX3_v. apply NNPP. zenon_intro zenon_H54. % 11.82/12.00 apply zenon_H54. exists zenon_TX2_t. apply NNPP. zenon_intro zenon_H55. % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H55); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 11.82/12.00 exact (zenon_H57 zenon_H18). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 11.82/12.00 exact (zenon_H59 zenon_H1a). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H58); [ zenon_intro zenon_H5b | zenon_intro zenon_H5a ]. % 11.82/12.00 exact (zenon_H5b zenon_H1c). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H5d | zenon_intro zenon_H5c ]. % 11.82/12.00 exact (zenon_H5d zenon_H24). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H5c); [ zenon_intro zenon_H5f | zenon_intro zenon_H5e ]. % 11.82/12.00 exact (zenon_H5f zenon_H26). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 11.82/12.00 exact (zenon_H61 zenon_H28). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H60); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 11.82/12.00 exact (zenon_H63 zenon_H2a). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H62); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 11.82/12.00 exact (zenon_H65 zenon_H2c). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H64); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 11.82/12.00 exact (zenon_H67 zenon_H1e). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H69 | zenon_intro zenon_H68 ]. % 11.82/12.00 exact (zenon_H69 zenon_H20). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 11.82/12.00 exact (zenon_H6b zenon_H22). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 11.82/12.00 exact (zenon_H6d zenon_H2e). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 11.82/12.00 exact (zenon_H6f zenon_H30). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 11.82/12.00 exact (zenon_H71 zenon_H32). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 11.82/12.00 exact (zenon_H73 zenon_H34). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 11.82/12.00 exact (zenon_H75 zenon_H36). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H74); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 11.82/12.00 exact (zenon_H77 zenon_H38). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H79 | zenon_intro zenon_H78 ]. % 11.82/12.00 apply zenon_H79. zenon_intro zenon_H7a. % 11.82/12.00 apply zenon_H3a. apply sym_equal. exact zenon_H7a. % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H78); [ zenon_intro zenon_H7c | zenon_intro zenon_H7b ]. % 11.82/12.00 exact (zenon_H7c zenon_H42). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H7b); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 11.82/12.00 exact (zenon_H7e zenon_H44). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H7d); [ zenon_intro zenon_H80 | zenon_intro zenon_H7f ]. % 11.82/12.00 exact (zenon_H80 zenon_H46). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H7f); [ zenon_intro zenon_H82 | zenon_intro zenon_H81 ]. % 11.82/12.00 exact (zenon_H82 zenon_H3c). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H81); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 11.82/12.00 exact (zenon_H84 zenon_H3e). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H83); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 11.82/12.00 exact (zenon_H86 zenon_H40). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 11.82/12.00 exact (zenon_H88 zenon_H4c). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 11.82/12.00 exact (zenon_H8a zenon_H4b). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 11.82/12.00 exact (zenon_H8c zenon_H48). % 11.82/12.00 exact (zenon_H8b zenon_H4a). % 11.82/12.00 apply (zenon_notimply_s _ _ zenon_H1). zenon_intro zenon_H8e. zenon_intro zenon_H8d. % 11.82/12.00 elim zenon_H8e. zenon_intro zenon_TX4_fn. zenon_intro zenon_H90. % 11.82/12.00 elim zenon_H90. zenon_intro zenon_TX5_fp. zenon_intro zenon_H92. % 11.82/12.00 elim zenon_H92. zenon_intro zenon_TX6_fr. zenon_intro zenon_H94. % 11.82/12.00 elim zenon_H94. zenon_intro zenon_TX7_ft. zenon_intro zenon_H96. % 11.82/12.00 elim zenon_H96. zenon_intro zenon_TX8_fv. zenon_intro zenon_H98. % 11.82/12.00 elim zenon_H98. zenon_intro zenon_TX9_fx. zenon_intro zenon_H9a. % 11.82/12.00 elim zenon_H9a. zenon_intro zenon_TX10_fz. zenon_intro zenon_H9c. % 11.82/12.00 elim zenon_H9c. zenon_intro zenon_TX11_gb. zenon_intro zenon_H9e. % 11.82/12.00 elim zenon_H9e. zenon_intro zenon_TX12_gd. zenon_intro zenon_Ha0. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Ha0). zenon_intro zenon_Ha2. zenon_intro zenon_Ha1. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Ha1). zenon_intro zenon_Ha4. zenon_intro zenon_Ha3. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Ha3). zenon_intro zenon_Ha6. zenon_intro zenon_Ha5. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Ha5). zenon_intro zenon_Ha8. zenon_intro zenon_Ha7. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Ha7). zenon_intro zenon_Haa. zenon_intro zenon_Ha9. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Ha9). zenon_intro zenon_Hac. zenon_intro zenon_Hab. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hab). zenon_intro zenon_Hae. zenon_intro zenon_Had. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Had). zenon_intro zenon_Hb0. zenon_intro zenon_Haf. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Haf). zenon_intro zenon_Hb2. zenon_intro zenon_Hb1. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hb1). zenon_intro zenon_Hb4. zenon_intro zenon_Hb3. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hb3). zenon_intro zenon_Hb6. zenon_intro zenon_Hb5. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hb5). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hb7). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hb9). zenon_intro zenon_Hbc. zenon_intro zenon_Hbb. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hbb). zenon_intro zenon_Hbe. zenon_intro zenon_Hbd. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hbd). zenon_intro zenon_Hc0. zenon_intro zenon_Hbf. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hbf). zenon_intro zenon_Hc2. zenon_intro zenon_Hc1. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hc1). zenon_intro zenon_Hc4. zenon_intro zenon_Hc3. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hc3). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_Hca. zenon_intro zenon_Hc9. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_Hcc. zenon_intro zenon_Hcb. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hcb). zenon_intro zenon_Hce. zenon_intro zenon_Hcd. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hcd). zenon_intro zenon_Hd0. zenon_intro zenon_Hcf. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hcf). zenon_intro zenon_Hd2. zenon_intro zenon_Hd1. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hd1). zenon_intro zenon_Hd4. zenon_intro zenon_Hd3. % 11.82/12.00 apply (zenon_and_s _ _ zenon_Hd3). zenon_intro zenon_Hd6. zenon_intro zenon_Hd5. % 11.82/12.00 apply zenon_H8d. exists zenon_TX4_fn. apply NNPP. zenon_intro zenon_Hd7. % 11.82/12.00 apply zenon_Hd7. exists zenon_TX5_fp. apply NNPP. zenon_intro zenon_Hd8. % 11.82/12.00 apply zenon_Hd8. exists zenon_TX7_ft. apply NNPP. zenon_intro zenon_Hd9. % 11.82/12.00 apply zenon_Hd9. exists zenon_TX6_fr. apply NNPP. zenon_intro zenon_Hda. % 11.82/12.00 apply zenon_Hda. exists zenon_TX9_fx. apply NNPP. zenon_intro zenon_Hdb. % 11.82/12.00 apply zenon_Hdb. exists zenon_TX8_fv. apply NNPP. zenon_intro zenon_Hdc. % 11.82/12.00 apply zenon_Hdc. exists zenon_TX10_fz. apply NNPP. zenon_intro zenon_Hdd. % 11.82/12.00 apply zenon_Hdd. exists zenon_TX12_gd. apply NNPP. zenon_intro zenon_Hde. % 11.82/12.00 apply zenon_Hde. exists zenon_TX11_gb. apply NNPP. zenon_intro zenon_Hdf. % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hdf); [ zenon_intro zenon_He1 | zenon_intro zenon_He0 ]. % 11.82/12.00 exact (zenon_He1 zenon_Ha2). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_He0); [ zenon_intro zenon_He3 | zenon_intro zenon_He2 ]. % 11.82/12.00 exact (zenon_He3 zenon_Ha4). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_He2); [ zenon_intro zenon_He5 | zenon_intro zenon_He4 ]. % 11.82/12.00 exact (zenon_He5 zenon_Ha6). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_He4); [ zenon_intro zenon_He7 | zenon_intro zenon_He6 ]. % 11.82/12.00 exact (zenon_He7 zenon_Hb2). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_He6); [ zenon_intro zenon_He9 | zenon_intro zenon_He8 ]. % 11.82/12.00 exact (zenon_He9 zenon_Hb4). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_He8); [ zenon_intro zenon_Heb | zenon_intro zenon_Hea ]. % 11.82/12.00 exact (zenon_Heb zenon_Hb6). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hea); [ zenon_intro zenon_Hed | zenon_intro zenon_Hec ]. % 11.82/12.00 exact (zenon_Hed zenon_Ha8). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hec); [ zenon_intro zenon_Hef | zenon_intro zenon_Hee ]. % 11.82/12.00 exact (zenon_Hef zenon_Haa). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hee); [ zenon_intro zenon_Hf1 | zenon_intro zenon_Hf0 ]. % 11.82/12.00 exact (zenon_Hf1 zenon_Hac). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hf0); [ zenon_intro zenon_Hf3 | zenon_intro zenon_Hf2 ]. % 11.82/12.00 exact (zenon_Hf3 zenon_Hae). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hf2); [ zenon_intro zenon_Hf5 | zenon_intro zenon_Hf4 ]. % 11.82/12.00 exact (zenon_Hf5 zenon_Hb0). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hf4); [ zenon_intro zenon_Hf7 | zenon_intro zenon_Hf6 ]. % 11.82/12.00 exact (zenon_Hf7 zenon_Hb8). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hf6); [ zenon_intro zenon_Hf9 | zenon_intro zenon_Hf8 ]. % 11.82/12.00 exact (zenon_Hf9 zenon_Hba). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hf8); [ zenon_intro zenon_Hfb | zenon_intro zenon_Hfa ]. % 11.82/12.00 exact (zenon_Hfb zenon_Hbc). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hfa); [ zenon_intro zenon_Hfd | zenon_intro zenon_Hfc ]. % 11.82/12.00 exact (zenon_Hfd zenon_Hbe). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_Hff | zenon_intro zenon_Hfe ]. % 11.82/12.00 exact (zenon_Hff zenon_Hc0). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_Hfe); [ zenon_intro zenon_H101 | zenon_intro zenon_H100 ]. % 11.82/12.00 exact (zenon_H101 zenon_Hc2). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H100); [ zenon_intro zenon_H103 | zenon_intro zenon_H102 ]. % 11.82/12.00 apply zenon_H103. zenon_intro zenon_H104. % 11.82/12.00 apply zenon_Hc4. apply sym_equal. exact zenon_H104. % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H102); [ zenon_intro zenon_H106 | zenon_intro zenon_H105 ]. % 11.82/12.00 exact (zenon_H106 zenon_Hcc). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H105); [ zenon_intro zenon_H108 | zenon_intro zenon_H107 ]. % 11.82/12.00 exact (zenon_H108 zenon_Hce). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H107); [ zenon_intro zenon_H10a | zenon_intro zenon_H109 ]. % 11.82/12.00 exact (zenon_H10a zenon_Hd0). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H109); [ zenon_intro zenon_H10c | zenon_intro zenon_H10b ]. % 11.82/12.00 exact (zenon_H10c zenon_Hc6). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H10b); [ zenon_intro zenon_H10e | zenon_intro zenon_H10d ]. % 11.82/12.00 exact (zenon_H10e zenon_Hc8). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H10d); [ zenon_intro zenon_H110 | zenon_intro zenon_H10f ]. % 11.82/12.00 exact (zenon_H110 zenon_Hca). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H10f); [ zenon_intro zenon_H112 | zenon_intro zenon_H111 ]. % 11.82/12.00 exact (zenon_H112 zenon_Hd6). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H111); [ zenon_intro zenon_H114 | zenon_intro zenon_H113 ]. % 11.82/12.00 exact (zenon_H114 zenon_Hd5). % 11.82/12.00 apply (zenon_notand_s _ _ zenon_H113); [ zenon_intro zenon_H116 | zenon_intro zenon_H115 ]. % 11.82/12.00 exact (zenon_H116 zenon_Hd2). % 11.82/12.00 exact (zenon_H115 zenon_Hd4). % 11.82/12.00 Qed. % 11.82/12.00 % SZS output end Proof % 11.82/12.00 (* END-PROOF *) % 11.82/12.00 nodes searched: 1407 % 11.82/12.00 max branch formulas: 476 % 11.82/12.00 proof nodes created: 303 % 11.82/12.00 formulas created: 21981 % 11.82/12.00 %------------------------------------------------------------------------------