%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR074+1 : TPTP v8.1.0. Released v3.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 : Sat Jul 16 00:02:34 EDT 2022 % Result : Theorem 0.20s 0.53s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : CSR074+1 : TPTP v8.1.0. Released v3.4.0. % 0.03/0.13 % Command : run_zenon %s %d % 0.13/0.35 % Computer : n018.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Fri Jun 10 23:33:39 EDT 2022 % 0.13/0.35 % CPUTime : % 0.20/0.53 (* PROOF-FOUND *) % 0.20/0.53 % SZS status Theorem % 0.20/0.53 (* BEGIN-PROOF *) % 0.20/0.53 % SZS output start Proof % 0.20/0.53 Theorem query74 : ((mtvisible (c_tptpgeo_member7_mt))->((inregion (c_geolocation_x53_y74) (c_georegion_l3_x17_y24))/\(geolevel_3 (c_georegion_l3_x17_y24)))). % 0.20/0.53 Proof. % 0.20/0.53 apply NNPP. intro zenon_G. % 0.20/0.53 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((inregion x y)->((inregion y z)->(inregion x z))))))); [ zenon_intro zenon_H32 | zenon_intro zenon_H33 ]. % 0.20/0.53 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genlmt x y)->((genlmt y z)->(genlmt x z))))))); [ zenon_intro zenon_H34 | zenon_intro zenon_H35 ]. % 0.20/0.53 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H37. zenon_intro zenon_H36. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H39 | zenon_intro zenon_H38 ]. % 0.20/0.53 apply (zenon_imply_s _ _ just11); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 0.20/0.53 exact (zenon_H3b zenon_H37). % 0.20/0.53 apply (zenon_imply_s _ _ just12); [ zenon_intro zenon_H3b | zenon_intro zenon_H3c ]. % 0.20/0.53 exact (zenon_H3b zenon_H37). % 0.20/0.53 elim (classic (inregion (c_georegion_l4_x53_y74) (c_georegion_l3_x17_y24))); [ zenon_intro zenon_H3d | zenon_intro zenon_H3e ]. % 0.20/0.53 generalize (zenon_H32 (c_geolocation_x53_y74)). zenon_intro zenon_H3f. % 0.20/0.53 generalize (zenon_H3f (c_georegion_l4_x53_y74)). zenon_intro zenon_H40. % 0.20/0.53 generalize (zenon_H40 (c_georegion_l3_x17_y24)). zenon_intro zenon_H41. % 0.20/0.53 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 0.20/0.53 exact (zenon_H43 zenon_H3c). % 0.20/0.53 apply (zenon_imply_s _ _ zenon_H42); [ zenon_intro zenon_H3e | zenon_intro zenon_H44 ]. % 0.20/0.53 exact (zenon_H3e zenon_H3d). % 0.20/0.53 exact (zenon_H39 zenon_H44). % 0.20/0.53 generalize (just5 (c_georegion_l3_x17_y24)). zenon_intro zenon_H45. % 0.20/0.53 generalize (zenon_H45 (c_georegion_l4_x53_y74)). zenon_intro zenon_H46. % 0.20/0.53 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H47 | zenon_intro zenon_H3d ]. % 0.20/0.53 exact (zenon_H47 zenon_H3a). % 0.20/0.53 exact (zenon_H3e zenon_H3d). % 0.20/0.53 apply (zenon_imply_s _ _ just10); [ zenon_intro zenon_H49 | zenon_intro zenon_H48 ]. % 0.20/0.53 generalize (just49 (c_tptpgeo_member7_mt)). zenon_intro zenon_H4a. % 0.20/0.53 generalize (zenon_H4a (c_worldgeographymt)). zenon_intro zenon_H4b. % 0.20/0.53 apply (zenon_imply_s _ _ zenon_H4b); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H3b | zenon_intro zenon_H4e ]. % 0.20/0.53 exact (zenon_H3b zenon_H37). % 0.20/0.53 elim (classic ((~((c_tptpgeo_member7_mt) = (c_tptpgeo_spindleheadmt)))/\(~(genlmt (c_tptpgeo_member7_mt) (c_tptpgeo_spindleheadmt))))); [ zenon_intro zenon_H4f | zenon_intro zenon_H50 ]. % 0.20/0.53 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H52. zenon_intro zenon_H51. % 0.20/0.53 exact (zenon_H51 just9). % 0.20/0.53 cut ((genlmt (c_tptpgeo_spindleheadmt) (c_worldgeographymt)) = (genlmt (c_tptpgeo_member7_mt) (c_worldgeographymt))). % 0.20/0.53 intro zenon_D_pnotp. % 0.20/0.53 apply zenon_H4e. % 0.20/0.53 rewrite <- zenon_D_pnotp. % 0.20/0.53 exact just8. % 0.20/0.53 cut (((c_worldgeographymt) = (c_worldgeographymt))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.20/0.53 cut (((c_tptpgeo_spindleheadmt) = (c_tptpgeo_member7_mt))); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.20/0.53 congruence. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.20/0.53 apply zenon_H56. zenon_intro zenon_H57. % 0.20/0.53 elim (classic ((c_tptpgeo_member7_mt) = (c_tptpgeo_member7_mt))); [ zenon_intro zenon_H58 | zenon_intro zenon_H59 ]. % 0.20/0.53 cut (((c_tptpgeo_member7_mt) = (c_tptpgeo_member7_mt)) = ((c_tptpgeo_spindleheadmt) = (c_tptpgeo_member7_mt))). % 0.20/0.53 intro zenon_D_pnotp. % 0.20/0.53 apply zenon_H54. % 0.20/0.53 rewrite <- zenon_D_pnotp. % 0.20/0.53 exact zenon_H58. % 0.20/0.53 cut (((c_tptpgeo_member7_mt) = (c_tptpgeo_member7_mt))); [idtac | apply NNPP; zenon_intro zenon_H59]. % 0.20/0.53 cut (((c_tptpgeo_member7_mt) = (c_tptpgeo_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 0.20/0.53 congruence. % 0.20/0.53 exact (zenon_H52 zenon_H57). % 0.20/0.53 apply zenon_H59. apply refl_equal. % 0.20/0.53 apply zenon_H59. apply refl_equal. % 0.20/0.53 apply zenon_H55. zenon_intro just9. % 0.20/0.53 generalize (zenon_H34 (c_tptpgeo_member7_mt)). zenon_intro zenon_H5a. % 0.20/0.53 generalize (zenon_H5a (c_tptpgeo_spindleheadmt)). zenon_intro zenon_H5b. % 0.20/0.53 generalize (zenon_H5b (c_worldgeographymt)). zenon_intro zenon_H5c. % 0.20/0.53 apply (zenon_imply_s _ _ zenon_H5c); [ zenon_intro zenon_H51 | zenon_intro zenon_H5d ]. % 0.20/0.53 exact (zenon_H51 just9). % 0.20/0.53 apply (zenon_imply_s _ _ zenon_H5d); [ zenon_intro zenon_H5f | zenon_intro zenon_H5e ]. % 0.20/0.53 exact (zenon_H5f just8). % 0.20/0.53 exact (zenon_H4e zenon_H5e). % 0.20/0.53 apply zenon_H53. apply refl_equal. % 0.20/0.53 exact (zenon_H49 zenon_H4c). % 0.20/0.53 exact (zenon_H38 zenon_H48). % 0.20/0.53 apply zenon_H35. zenon_intro zenon_Tx_ds. apply NNPP. zenon_intro zenon_H61. % 0.20/0.53 apply zenon_H61. zenon_intro zenon_Ty_du. apply NNPP. zenon_intro zenon_H63. % 0.20/0.53 apply zenon_H63. zenon_intro zenon_Tz_dw. apply NNPP. zenon_intro zenon_H65. % 0.20/0.53 apply (zenon_notimply_s _ _ zenon_H65). zenon_intro zenon_H67. zenon_intro zenon_H66. % 0.20/0.53 apply (zenon_notimply_s _ _ zenon_H66). zenon_intro zenon_H69. zenon_intro zenon_H68. % 0.20/0.53 generalize (just54 zenon_Tx_ds). zenon_intro zenon_H6a. % 0.20/0.53 generalize (zenon_H6a zenon_Ty_du). zenon_intro zenon_H6b. % 0.20/0.53 generalize (zenon_H6b zenon_Tz_dw). zenon_intro zenon_H6c. % 0.20/0.53 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 0.20/0.53 exact (zenon_H70 zenon_H67). % 0.20/0.53 exact (zenon_H6f zenon_H69). % 0.20/0.53 exact (zenon_H68 zenon_H6d). % 0.20/0.53 apply zenon_H33. zenon_intro zenon_Tx_ej. apply NNPP. zenon_intro zenon_H72. % 0.20/0.53 apply zenon_H72. zenon_intro zenon_Ty_el. apply NNPP. zenon_intro zenon_H74. % 0.20/0.53 apply zenon_H74. zenon_intro zenon_Tz_en. apply NNPP. zenon_intro zenon_H76. % 0.20/0.53 apply (zenon_notimply_s _ _ zenon_H76). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.20/0.53 apply (zenon_notimply_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 0.20/0.53 generalize (just41 zenon_Tx_ej). zenon_intro zenon_H7b. % 0.20/0.53 generalize (zenon_H7b zenon_Ty_el). zenon_intro zenon_H7c. % 0.20/0.53 generalize (zenon_H7c zenon_Tz_en). zenon_intro zenon_H7d. % 0.20/0.53 apply (zenon_imply_s _ _ zenon_H7d); [ zenon_intro zenon_H7f | zenon_intro zenon_H7e ]. % 0.20/0.53 apply (zenon_notand_s _ _ zenon_H7f); [ zenon_intro zenon_H81 | zenon_intro zenon_H80 ]. % 0.20/0.53 exact (zenon_H81 zenon_H78). % 0.20/0.53 exact (zenon_H80 zenon_H7a). % 0.20/0.53 exact (zenon_H79 zenon_H7e). % 0.20/0.53 Qed. % 0.20/0.53 % SZS output end Proof % 0.20/0.53 (* END-PROOF *) % 0.20/0.53 nodes searched: 298 % 0.20/0.53 max branch formulas: 195 % 0.20/0.53 proof nodes created: 31 % 0.20/0.53 formulas created: 1513 % 0.20/0.53 %------------------------------------------------------------------------------