%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NLP122+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:54:27 EDT 2022 % Result : Theorem 0.36s 0.53s % Output : Proof 0.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP122+1 : TPTP v8.1.0. Released v2.4.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n005.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 : Fri Jul 1 04:52:37 EDT 2022 % 0.12/0.33 % CPUTime : % 0.36/0.53 (* PROOF-FOUND *) % 0.36/0.53 % SZS status Theorem % 0.36/0.53 (* BEGIN-PROOF *) % 0.36/0.53 % SZS output start Proof % 0.36/0.53 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, ((of U V W)/\((city U W)/\((hollywood_placename U V)/\((placename U V)/\((chevy U W)/\((white U W)/\((dirty U W)/\((old U W)/\((street U X)/\((lonely U X)/\((event U Y)/\((agent U Y W)/\((present U Y)/\((barrel U Y)/\((down U Y X)/\(in U Y W))))))))))))))))))))))->(exists Z : zenon_U, ((actual_world Z)/\(exists X1 : zenon_U, (exists X2 : zenon_U, (exists X3 : zenon_U, (exists X4 : zenon_U, ((street Z X1)/\((lonely Z X1)/\((of Z X2 X3)/\((city Z X3)/\((hollywood_placename Z X2)/\((placename Z X2)/\((chevy Z X3)/\((white Z X3)/\((dirty Z X3)/\((old Z X3)/\((event Z X4)/\((agent Z X4 X3)/\((present Z X4)/\((barrel Z X4)/\((down Z X4 X1)/\(in Z X4 X3)))))))))))))))))))))))/\((exists Z : zenon_U, ((actual_world Z)/\(exists X1 : zenon_U, (exists X2 : zenon_U, (exists X3 : zenon_U, (exists X4 : zenon_U, ((street Z X1)/\((lonely Z X1)/\((of Z X2 X3)/\((city Z X3)/\((hollywood_placename Z X2)/\((placename Z X2)/\((chevy Z X3)/\((white Z X3)/\((dirty Z X3)/\((old Z X3)/\((event Z X4)/\((agent Z X4 X3)/\((present Z X4)/\((barrel Z X4)/\((down Z X4 X1)/\(in Z X4 X3))))))))))))))))))))))->(exists U : zenon_U, ((actual_world U)/\(exists V : zenon_U, (exists W : zenon_U, (exists X : zenon_U, (exists Y : zenon_U, ((of U V W)/\((city U W)/\((hollywood_placename U V)/\((placename U V)/\((chevy U W)/\((white U W)/\((dirty U W)/\((old U W)/\((street U X)/\((lonely U X)/\((event U Y)/\((agent U Y W)/\((present U Y)/\((barrel U Y)/\((down U Y X)/\(in U Y W)))))))))))))))))))))))))). % 0.36/0.53 Proof. % 0.36/0.53 apply NNPP. intro zenon_G. % 0.36/0.53 apply zenon_G. zenon_intro zenon_H1. % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H1); [ zenon_intro zenon_H3 | zenon_intro zenon_H2 ]. % 0.36/0.53 apply (zenon_notimply_s _ _ zenon_H3). zenon_intro zenon_H5. zenon_intro zenon_H4. % 0.36/0.53 elim zenon_H5. zenon_intro zenon_TU_g. zenon_intro zenon_H7. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H7). zenon_intro zenon_H9. zenon_intro zenon_H8. % 0.36/0.53 elim zenon_H8. zenon_intro zenon_TV_k. zenon_intro zenon_Hb. % 0.36/0.53 elim zenon_Hb. zenon_intro zenon_TW_m. zenon_intro zenon_Hd. % 0.36/0.53 elim zenon_Hd. zenon_intro zenon_TX_o. zenon_intro zenon_Hf. % 0.36/0.53 elim zenon_Hf. zenon_intro zenon_TY_q. zenon_intro zenon_H11. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H11). zenon_intro zenon_H13. zenon_intro zenon_H12. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H12). zenon_intro zenon_H15. zenon_intro zenon_H14. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H14). zenon_intro zenon_H17. zenon_intro zenon_H16. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H16). zenon_intro zenon_H19. zenon_intro zenon_H18. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H18). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H1a). zenon_intro zenon_H1d. zenon_intro zenon_H1c. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H1c). zenon_intro zenon_H1f. zenon_intro zenon_H1e. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H1e). zenon_intro zenon_H21. zenon_intro zenon_H20. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H22). zenon_intro zenon_H25. zenon_intro zenon_H24. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H24). zenon_intro zenon_H27. zenon_intro zenon_H26. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H2a). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 0.36/0.53 apply zenon_H4. exists zenon_TU_g. apply NNPP. zenon_intro zenon_H30. % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H30); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 0.36/0.53 exact (zenon_H32 zenon_H9). % 0.36/0.53 apply zenon_H31. exists zenon_TX_o. apply NNPP. zenon_intro zenon_H33. % 0.36/0.53 apply zenon_H33. exists zenon_TV_k. apply NNPP. zenon_intro zenon_H34. % 0.36/0.53 apply zenon_H34. exists zenon_TW_m. apply NNPP. zenon_intro zenon_H35. % 0.36/0.53 apply zenon_H35. exists zenon_TY_q. apply NNPP. zenon_intro zenon_H36. % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 0.36/0.53 exact (zenon_H38 zenon_H23). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H3a | zenon_intro zenon_H39 ]. % 0.36/0.53 exact (zenon_H3a zenon_H25). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H39); [ zenon_intro zenon_H3c | zenon_intro zenon_H3b ]. % 0.36/0.53 exact (zenon_H3c zenon_H13). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H3b); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 0.36/0.53 exact (zenon_H3e zenon_H15). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H3d); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 0.36/0.53 exact (zenon_H40 zenon_H17). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 0.36/0.53 exact (zenon_H42 zenon_H19). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H41); [ zenon_intro zenon_H44 | zenon_intro zenon_H43 ]. % 0.36/0.53 exact (zenon_H44 zenon_H1b). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H43); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 0.36/0.53 exact (zenon_H46 zenon_H1d). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H45); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 0.36/0.53 exact (zenon_H48 zenon_H1f). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H47); [ zenon_intro zenon_H4a | zenon_intro zenon_H49 ]. % 0.36/0.53 exact (zenon_H4a zenon_H21). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 0.36/0.53 exact (zenon_H4c zenon_H27). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H4b); [ zenon_intro zenon_H4e | zenon_intro zenon_H4d ]. % 0.36/0.53 exact (zenon_H4e zenon_H29). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H50 | zenon_intro zenon_H4f ]. % 0.36/0.53 exact (zenon_H50 zenon_H2b). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H52 | zenon_intro zenon_H51 ]. % 0.36/0.53 exact (zenon_H52 zenon_H2d). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H51); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 0.36/0.53 exact (zenon_H54 zenon_H2f). % 0.36/0.53 exact (zenon_H53 zenon_H2e). % 0.36/0.53 apply (zenon_notimply_s _ _ zenon_H2). zenon_intro zenon_H56. zenon_intro zenon_H55. % 0.36/0.53 elim zenon_H56. zenon_intro zenon_TZ_dj. zenon_intro zenon_H58. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 0.36/0.53 elim zenon_H59. zenon_intro zenon_TX1_dn. zenon_intro zenon_H5c. % 0.36/0.53 elim zenon_H5c. zenon_intro zenon_TX2_dp. zenon_intro zenon_H5e. % 0.36/0.53 elim zenon_H5e. zenon_intro zenon_TX3_dr. zenon_intro zenon_H60. % 0.36/0.53 elim zenon_H60. zenon_intro zenon_TX4_dt. zenon_intro zenon_H62. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H64. zenon_intro zenon_H63. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H72. zenon_intro zenon_H71. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H74. zenon_intro zenon_H73. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H73). zenon_intro zenon_H76. zenon_intro zenon_H75. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H79). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H7b). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 0.36/0.53 apply (zenon_and_s _ _ zenon_H7d). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 0.36/0.53 apply zenon_H55. exists zenon_TZ_dj. apply NNPP. zenon_intro zenon_H81. % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H81); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 0.36/0.53 exact (zenon_H83 zenon_H5a). % 0.36/0.53 apply zenon_H82. exists zenon_TX2_dp. apply NNPP. zenon_intro zenon_H84. % 0.36/0.53 apply zenon_H84. exists zenon_TX3_dr. apply NNPP. zenon_intro zenon_H85. % 0.36/0.53 apply zenon_H85. exists zenon_TX1_dn. apply NNPP. zenon_intro zenon_H86. % 0.36/0.53 apply zenon_H86. exists zenon_TX4_dt. apply NNPP. zenon_intro zenon_H87. % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.36/0.53 exact (zenon_H89 zenon_H68). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H88); [ zenon_intro zenon_H8b | zenon_intro zenon_H8a ]. % 0.36/0.53 exact (zenon_H8b zenon_H6a). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 0.36/0.53 exact (zenon_H8d zenon_H6c). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H8c); [ zenon_intro zenon_H8f | zenon_intro zenon_H8e ]. % 0.36/0.53 exact (zenon_H8f zenon_H6e). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H8e); [ zenon_intro zenon_H91 | zenon_intro zenon_H90 ]. % 0.36/0.53 exact (zenon_H91 zenon_H70). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H90); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 0.36/0.53 exact (zenon_H93 zenon_H72). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H92); [ zenon_intro zenon_H95 | zenon_intro zenon_H94 ]. % 0.36/0.53 exact (zenon_H95 zenon_H74). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H94); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 0.36/0.53 exact (zenon_H97 zenon_H76). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H96); [ zenon_intro zenon_H99 | zenon_intro zenon_H98 ]. % 0.36/0.53 exact (zenon_H99 zenon_H64). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H98); [ zenon_intro zenon_H9b | zenon_intro zenon_H9a ]. % 0.36/0.53 exact (zenon_H9b zenon_H66). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H9a); [ zenon_intro zenon_H9d | zenon_intro zenon_H9c ]. % 0.36/0.53 exact (zenon_H9d zenon_H78). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H9c); [ zenon_intro zenon_H9f | zenon_intro zenon_H9e ]. % 0.36/0.53 exact (zenon_H9f zenon_H7a). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_H9e); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha0 ]. % 0.36/0.53 exact (zenon_Ha1 zenon_H7c). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_Ha0); [ zenon_intro zenon_Ha3 | zenon_intro zenon_Ha2 ]. % 0.36/0.53 exact (zenon_Ha3 zenon_H7e). % 0.36/0.53 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_Ha5 | zenon_intro zenon_Ha4 ]. % 0.36/0.53 exact (zenon_Ha5 zenon_H80). % 0.36/0.53 exact (zenon_Ha4 zenon_H7f). % 0.36/0.53 Qed. % 0.36/0.53 % SZS output end Proof % 0.36/0.53 (* END-PROOF *) % 0.36/0.53 nodes searched: 170 % 0.36/0.53 max branch formulas: 79 % 0.36/0.53 proof nodes created: 84 % 0.36/0.53 formulas created: 2112 % 0.36/0.53 %------------------------------------------------------------------------------