%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NLP079+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n011.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:54:03 EDT 2022 % Result : Theorem 1.73s 1.96s % Output : Proof 1.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP079+1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n011.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 09:31:18 EDT 2022 % 0.12/0.34 % CPUTime : % 1.73/1.96 (* PROOF-FOUND *) % 1.73/1.96 % SZS status Theorem % 1.73/1.96 (* BEGIN-PROOF *) % 1.73/1.96 % SZS output start Proof % 1.73/1.96 Theorem co1 : (~(~(((exists U : zenon_U, ((actual_world 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, ((male U V)/\((male U W)/\((man U W)/\((of U X W)/\((cannon U X)/\((forall X3 : zenon_U, ((member U X3 Y)->(exists X4 : zenon_U, ((event U X4)/\((agent U X4 W)/\((patient U X4 X3)/\((present U X4)/\((nonreflexive U X4)/\((fire U X4)/\(from_loc U X4 X))))))))))/\((six U Y)/\((group U Y)/\((forall X5 : zenon_U, ((member U X5 Y)->(shot U X5)))/\((revenge U Z)/\((cry U X1)/\((event U X2)/\((agent U X2 V)/\((patient U X2 X1)/\((present U X2)/\((nonreflexive U X2)/\((scream U X2)/\(of U X2 Z)))))))))))))))))))))))))))->(exists X6 : zenon_U, ((actual_world X6)/\(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, ((male X6 X7)/\((male X6 X8)/\((man X6 X8)/\((of X6 X9 X8)/\((cannon X6 X9)/\((forall X14 : zenon_U, ((member X6 X14 X10)->(exists X15 : zenon_U, ((event X6 X15)/\((agent X6 X15 X8)/\((patient X6 X15 X14)/\((present X6 X15)/\((nonreflexive X6 X15)/\((fire X6 X15)/\(from_loc X6 X15 X9))))))))))/\((six X6 X10)/\((group X6 X10)/\((forall X16 : zenon_U, ((member X6 X16 X10)->(shot X6 X16)))/\((cry X6 X11)/\((revenge X6 X12)/\((event X6 X13)/\((agent X6 X13 X7)/\((patient X6 X13 X11)/\((present X6 X13)/\((nonreflexive X6 X13)/\((scream X6 X13)/\(of X6 X13 X12))))))))))))))))))))))))))))/\((exists X6 : zenon_U, ((actual_world X6)/\(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, ((male X6 X7)/\((male X6 X8)/\((man X6 X8)/\((of X6 X9 X8)/\((cannon X6 X9)/\((forall X14 : zenon_U, ((member X6 X14 X10)->(exists X15 : zenon_U, ((event X6 X15)/\((agent X6 X15 X8)/\((patient X6 X15 X14)/\((present X6 X15)/\((nonreflexive X6 X15)/\((fire X6 X15)/\(from_loc X6 X15 X9))))))))))/\((six X6 X10)/\((group X6 X10)/\((forall X16 : zenon_U, ((member X6 X16 X10)->(shot X6 X16)))/\((cry X6 X11)/\((revenge X6 X12)/\((event X6 X13)/\((agent X6 X13 X7)/\((patient X6 X13 X11)/\((present X6 X13)/\((nonreflexive X6 X13)/\((scream X6 X13)/\(of X6 X13 X12)))))))))))))))))))))))))))->(exists U : zenon_U, ((actual_world 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, ((male U V)/\((male U W)/\((man U W)/\((of U X W)/\((cannon U X)/\((forall X3 : zenon_U, ((member U X3 Y)->(exists X4 : zenon_U, ((event U X4)/\((agent U X4 W)/\((patient U X4 X3)/\((present U X4)/\((nonreflexive U X4)/\((fire U X4)/\(from_loc U X4 X))))))))))/\((six U Y)/\((group U Y)/\((forall X5 : zenon_U, ((member U X5 Y)->(shot U X5)))/\((revenge U Z)/\((cry U X1)/\((event U X2)/\((agent U X2 V)/\((patient U X2 X1)/\((present U X2)/\((nonreflexive U X2)/\((scream U X2)/\(of U X2 Z))))))))))))))))))))))))))))))). % 1.73/1.96 Proof. % 1.73/1.96 apply NNPP. intro zenon_G. % 1.73/1.96 apply zenon_G. zenon_intro zenon_H1. % 1.73/1.96 apply (zenon_notand_s _ _ zenon_H1); [ zenon_intro zenon_H3 | zenon_intro zenon_H2 ]. % 1.73/1.96 apply (zenon_notimply_s _ _ zenon_H3). zenon_intro zenon_H5. zenon_intro zenon_H4. % 1.73/1.96 elim zenon_H5. zenon_intro zenon_TU_g. zenon_intro zenon_H7. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H7). zenon_intro zenon_H9. zenon_intro zenon_H8. % 1.73/1.96 elim zenon_H8. zenon_intro zenon_TV_k. zenon_intro zenon_Hb. % 1.73/1.96 elim zenon_Hb. zenon_intro zenon_TW_m. zenon_intro zenon_Hd. % 1.73/1.96 elim zenon_Hd. zenon_intro zenon_TX_o. zenon_intro zenon_Hf. % 1.73/1.96 elim zenon_Hf. zenon_intro zenon_TY_q. zenon_intro zenon_H11. % 1.73/1.96 elim zenon_H11. zenon_intro zenon_TZ_s. zenon_intro zenon_H13. % 1.73/1.96 elim zenon_H13. zenon_intro zenon_TX1_u. zenon_intro zenon_H15. % 1.73/1.96 elim zenon_H15. zenon_intro zenon_TX2_w. zenon_intro zenon_H17. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H17). zenon_intro zenon_H19. zenon_intro zenon_H18. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H18). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H1a). zenon_intro zenon_H1d. zenon_intro zenon_H1c. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H1c). zenon_intro zenon_H1f. zenon_intro zenon_H1e. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H1e). zenon_intro zenon_H21. zenon_intro zenon_H20. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H22). zenon_intro zenon_H25. zenon_intro zenon_H24. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H24). zenon_intro zenon_H27. zenon_intro zenon_H26. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H2a). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H31. zenon_intro zenon_H30. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 1.73/1.96 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 1.73/1.96 apply zenon_H4. exists zenon_TU_g. apply NNPP. zenon_intro zenon_H3a. % 1.73/1.96 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H3c | zenon_intro zenon_H3b ]. % 1.73/1.96 exact (zenon_H3c zenon_H9). % 1.73/1.96 apply zenon_H3b. exists zenon_TV_k. apply NNPP. zenon_intro zenon_H3d. % 1.73/1.96 apply zenon_H3d. exists zenon_TW_m. apply NNPP. zenon_intro zenon_H3e. % 1.73/1.96 apply zenon_H3e. exists zenon_TX_o. apply NNPP. zenon_intro zenon_H3f. % 1.73/1.96 apply zenon_H3f. exists zenon_TY_q. apply NNPP. zenon_intro zenon_H40. % 1.73/1.96 apply zenon_H40. exists zenon_TX1_u. apply NNPP. zenon_intro zenon_H41. % 1.73/1.96 apply zenon_H41. exists zenon_TZ_s. apply NNPP. zenon_intro zenon_H42. % 1.73/1.96 apply zenon_H42. exists zenon_TX2_w. apply NNPP. zenon_intro zenon_H43. % 1.73/1.96 apply (zenon_notand_s _ _ zenon_H43); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 1.73/1.96 exact (zenon_H45 zenon_H19). % 1.73/1.96 apply (zenon_notand_s _ _ zenon_H44); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 1.73/1.97 exact (zenon_H47 zenon_H1b). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H49 | zenon_intro zenon_H48 ]. % 1.73/1.97 exact (zenon_H49 zenon_H1d). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 1.73/1.97 exact (zenon_H4b zenon_H1f). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H4a); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 1.73/1.97 exact (zenon_H4d zenon_H21). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H4c); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 1.73/1.97 exact (zenon_H4f zenon_H23). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 1.73/1.97 exact (zenon_H51 zenon_H25). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 1.73/1.97 exact (zenon_H53 zenon_H27). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H55 | zenon_intro zenon_H54 ]. % 1.73/1.97 exact (zenon_H55 zenon_H29). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H54); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 1.73/1.97 exact (zenon_H57 zenon_H2d). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 1.73/1.97 exact (zenon_H59 zenon_H2b). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H58); [ zenon_intro zenon_H5b | zenon_intro zenon_H5a ]. % 1.73/1.97 exact (zenon_H5b zenon_H2f). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H5d | zenon_intro zenon_H5c ]. % 1.73/1.97 exact (zenon_H5d zenon_H31). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H5c); [ zenon_intro zenon_H5f | zenon_intro zenon_H5e ]. % 1.73/1.97 exact (zenon_H5f zenon_H33). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 1.73/1.97 exact (zenon_H61 zenon_H35). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H60); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 1.73/1.97 exact (zenon_H63 zenon_H37). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H62); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 1.73/1.97 exact (zenon_H65 zenon_H39). % 1.73/1.97 exact (zenon_H64 zenon_H38). % 1.73/1.97 apply (zenon_notimply_s _ _ zenon_H2). zenon_intro zenon_H67. zenon_intro zenon_H66. % 1.73/1.97 elim zenon_H67. zenon_intro zenon_TX6_ea. zenon_intro zenon_H69. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6b. zenon_intro zenon_H6a. % 1.73/1.97 elim zenon_H6a. zenon_intro zenon_TX7_ee. zenon_intro zenon_H6d. % 1.73/1.97 elim zenon_H6d. zenon_intro zenon_TX8_eg. zenon_intro zenon_H6f. % 1.73/1.97 elim zenon_H6f. zenon_intro zenon_TX9_ei. zenon_intro zenon_H71. % 1.73/1.97 elim zenon_H71. zenon_intro zenon_TX10_ek. zenon_intro zenon_H73. % 1.73/1.97 elim zenon_H73. zenon_intro zenon_TX11_em. zenon_intro zenon_H75. % 1.73/1.97 elim zenon_H75. zenon_intro zenon_TX12_eo. zenon_intro zenon_H77. % 1.73/1.97 elim zenon_H77. zenon_intro zenon_TX13_eq. zenon_intro zenon_H79. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H7a). zenon_intro zenon_H7d. zenon_intro zenon_H7c. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H7c). zenon_intro zenon_H7f. zenon_intro zenon_H7e. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H7e). zenon_intro zenon_H81. zenon_intro zenon_H80. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H82). zenon_intro zenon_H85. zenon_intro zenon_H84. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H84). zenon_intro zenon_H87. zenon_intro zenon_H86. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H89. zenon_intro zenon_H88. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H88). zenon_intro zenon_H8b. zenon_intro zenon_H8a. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H8a). zenon_intro zenon_H8d. zenon_intro zenon_H8c. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H8c). zenon_intro zenon_H8f. zenon_intro zenon_H8e. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H8e). zenon_intro zenon_H91. zenon_intro zenon_H90. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H90). zenon_intro zenon_H93. zenon_intro zenon_H92. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H92). zenon_intro zenon_H95. zenon_intro zenon_H94. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H94). zenon_intro zenon_H97. zenon_intro zenon_H96. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H96). zenon_intro zenon_H99. zenon_intro zenon_H98. % 1.73/1.97 apply (zenon_and_s _ _ zenon_H98). zenon_intro zenon_H9b. zenon_intro zenon_H9a. % 1.73/1.97 apply zenon_H66. exists zenon_TX6_ea. apply NNPP. zenon_intro zenon_H9c. % 1.73/1.97 apply (zenon_notand_s _ _ zenon_H9c); [ zenon_intro zenon_H9e | zenon_intro zenon_H9d ]. % 1.73/1.97 exact (zenon_H9e zenon_H6b). % 1.73/1.97 apply zenon_H9d. exists zenon_TX7_ee. apply NNPP. zenon_intro zenon_H9f. % 1.73/1.97 apply zenon_H9f. exists zenon_TX8_eg. apply NNPP. zenon_intro zenon_Ha0. % 1.73/1.97 apply zenon_Ha0. exists zenon_TX9_ei. apply NNPP. zenon_intro zenon_Ha1. % 1.73/1.97 apply zenon_Ha1. exists zenon_TX10_ek. apply NNPP. zenon_intro zenon_Ha2. % 1.73/1.97 apply zenon_Ha2. exists zenon_TX12_eo. apply NNPP. zenon_intro zenon_Ha3. % 1.73/1.97 apply zenon_Ha3. exists zenon_TX11_em. apply NNPP. zenon_intro zenon_Ha4. % 1.73/1.97 apply zenon_Ha4. exists zenon_TX13_eq. apply NNPP. zenon_intro zenon_Ha5. % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_Ha6 ]. % 1.73/1.97 exact (zenon_Ha7 zenon_H7b). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Ha6); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8 ]. % 1.73/1.97 exact (zenon_Ha9 zenon_H7d). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Ha8); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 1.73/1.97 exact (zenon_Hab zenon_H7f). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_Had | zenon_intro zenon_Hac ]. % 1.73/1.97 exact (zenon_Had zenon_H81). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hac); [ zenon_intro zenon_Haf | zenon_intro zenon_Hae ]. % 1.73/1.97 exact (zenon_Haf zenon_H83). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_Hb1 | zenon_intro zenon_Hb0 ]. % 1.73/1.97 exact (zenon_Hb1 zenon_H85). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hb0); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 1.73/1.97 exact (zenon_Hb3 zenon_H87). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hb2); [ zenon_intro zenon_Hb5 | zenon_intro zenon_Hb4 ]. % 1.73/1.97 exact (zenon_Hb5 zenon_H89). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hb4); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 1.73/1.97 exact (zenon_Hb7 zenon_H8b). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 1.73/1.97 exact (zenon_Hb9 zenon_H8f). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hb8); [ zenon_intro zenon_Hbb | zenon_intro zenon_Hba ]. % 1.73/1.97 exact (zenon_Hbb zenon_H8d). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hba); [ zenon_intro zenon_Hbd | zenon_intro zenon_Hbc ]. % 1.73/1.97 exact (zenon_Hbd zenon_H91). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hbc); [ zenon_intro zenon_Hbf | zenon_intro zenon_Hbe ]. % 1.73/1.97 exact (zenon_Hbf zenon_H93). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hbe); [ zenon_intro zenon_Hc1 | zenon_intro zenon_Hc0 ]. % 1.73/1.97 exact (zenon_Hc1 zenon_H95). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hc0); [ zenon_intro zenon_Hc3 | zenon_intro zenon_Hc2 ]. % 1.73/1.97 exact (zenon_Hc3 zenon_H97). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hc2); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 1.73/1.97 exact (zenon_Hc5 zenon_H99). % 1.73/1.97 apply (zenon_notand_s _ _ zenon_Hc4); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc6 ]. % 1.73/1.97 exact (zenon_Hc7 zenon_H9b). % 1.73/1.97 exact (zenon_Hc6 zenon_H9a). % 1.73/1.97 Qed. % 1.73/1.97 % SZS output end Proof % 1.73/1.97 (* END-PROOF *) % 1.73/1.97 nodes searched: 752 % 1.73/1.97 max branch formulas: 303 % 1.73/1.97 proof nodes created: 222 % 1.73/1.97 formulas created: 9287 % 1.73/1.97 %------------------------------------------------------------------------------