%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR029+2 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n015.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:01:50 EDT 2022 % Result : Theorem 30.02s 30.21s % Output : Proof 30.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : CSR029+2 : TPTP v8.1.0. Released v3.4.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n015.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sat Jun 11 09:55:05 EDT 2022 % 0.13/0.33 % CPUTime : % 30.02/30.21 (* PROOF-FOUND *) % 30.02/30.21 % SZS status Theorem % 30.02/30.21 (* BEGIN-PROOF *) % 30.02/30.21 % SZS output start Proof % 30.02/30.21 Theorem query79 : ((mtvisible (c_tptpgeo_member3_mt))->((inregion (c_geolocation_x14_y39) (c_georegion_l3_x4_y13))/\(geolevel_3 (c_georegion_l3_x4_y13)))). % 30.02/30.21 Proof. % 30.02/30.21 apply NNPP. intro zenon_G. % 30.02/30.21 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_H450 | zenon_intro zenon_H451 ]. % 30.02/30.21 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_H452 | zenon_intro zenon_H453 ]. % 30.02/30.21 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H455. zenon_intro zenon_H454. % 30.02/30.21 apply (zenon_notand_s _ _ zenon_H454); [ zenon_intro zenon_H457 | zenon_intro zenon_H456 ]. % 30.02/30.21 apply (zenon_imply_s _ _ ax1_282); [ zenon_intro zenon_H459 | zenon_intro zenon_H458 ]. % 30.02/30.21 exact (zenon_H459 zenon_H455). % 30.02/30.21 apply (zenon_imply_s _ _ ax1_337); [ zenon_intro zenon_H459 | zenon_intro zenon_H45a ]. % 30.02/30.21 exact (zenon_H459 zenon_H455). % 30.02/30.21 elim (classic (inregion (c_georegion_l4_x14_y39) (c_georegion_l3_x4_y13))); [ zenon_intro zenon_H45b | zenon_intro zenon_H45c ]. % 30.02/30.21 generalize (zenon_H450 (c_geolocation_x14_y39)). zenon_intro zenon_H45d. % 30.02/30.21 generalize (zenon_H45d (c_georegion_l4_x14_y39)). zenon_intro zenon_H45e. % 30.02/30.21 generalize (zenon_H45e (c_georegion_l3_x4_y13)). zenon_intro zenon_H45f. % 30.02/30.21 apply (zenon_imply_s _ _ zenon_H45f); [ zenon_intro zenon_H461 | zenon_intro zenon_H460 ]. % 30.02/30.21 exact (zenon_H461 zenon_H458). % 30.02/30.21 apply (zenon_imply_s _ _ zenon_H460); [ zenon_intro zenon_H45c | zenon_intro zenon_H462 ]. % 30.02/30.21 exact (zenon_H45c zenon_H45b). % 30.02/30.21 exact (zenon_H457 zenon_H462). % 30.02/30.21 generalize (ax1_128 (c_georegion_l3_x4_y13)). zenon_intro zenon_H463. % 30.02/30.21 generalize (zenon_H463 (c_georegion_l4_x14_y39)). zenon_intro zenon_H464. % 30.02/30.21 apply (zenon_imply_s _ _ zenon_H464); [ zenon_intro zenon_H465 | zenon_intro zenon_H45b ]. % 30.02/30.21 exact (zenon_H465 zenon_H45a). % 30.02/30.21 exact (zenon_H45c zenon_H45b). % 30.02/30.21 apply (zenon_imply_s _ _ ax1_121); [ zenon_intro zenon_H467 | zenon_intro zenon_H466 ]. % 30.02/30.21 generalize (ax1_1123 (c_tptpgeo_member3_mt)). zenon_intro zenon_H468. % 30.02/30.21 generalize (zenon_H468 (c_worldgeographymt)). zenon_intro zenon_H469. % 30.02/30.21 apply (zenon_imply_s _ _ zenon_H469); [ zenon_intro zenon_H46b | zenon_intro zenon_H46a ]. % 30.02/30.21 apply (zenon_notand_s _ _ zenon_H46b); [ zenon_intro zenon_H459 | zenon_intro zenon_H46c ]. % 30.02/30.21 exact (zenon_H459 zenon_H455). % 30.02/30.21 elim (classic ((~((c_tptpgeo_member3_mt) = (c_tptpgeo_spindleheadmt)))/\(~(genlmt (c_tptpgeo_member3_mt) (c_tptpgeo_spindleheadmt))))); [ zenon_intro zenon_H46d | zenon_intro zenon_H46e ]. % 30.02/30.21 apply (zenon_and_s _ _ zenon_H46d). zenon_intro zenon_H470. zenon_intro zenon_H46f. % 30.02/30.21 exact (zenon_H46f ax1_212). % 30.02/30.21 cut ((genlmt (c_tptpgeo_spindleheadmt) (c_worldgeographymt)) = (genlmt (c_tptpgeo_member3_mt) (c_worldgeographymt))). % 30.02/30.21 intro zenon_D_pnotp. % 30.02/30.21 apply zenon_H46c. % 30.02/30.21 rewrite <- zenon_D_pnotp. % 30.02/30.21 exact ax1_326. % 30.02/30.21 cut (((c_worldgeographymt) = (c_worldgeographymt))); [idtac | apply NNPP; zenon_intro zenon_H471]. % 30.02/30.21 cut (((c_tptpgeo_spindleheadmt) = (c_tptpgeo_member3_mt))); [idtac | apply NNPP; zenon_intro zenon_H472]. % 30.02/30.21 congruence. % 30.02/30.21 apply (zenon_notand_s _ _ zenon_H46e); [ zenon_intro zenon_H474 | zenon_intro zenon_H473 ]. % 30.02/30.21 apply zenon_H474. zenon_intro zenon_H475. % 30.02/30.21 elim (classic ((c_tptpgeo_member3_mt) = (c_tptpgeo_member3_mt))); [ zenon_intro zenon_H476 | zenon_intro zenon_H477 ]. % 30.02/30.21 cut (((c_tptpgeo_member3_mt) = (c_tptpgeo_member3_mt)) = ((c_tptpgeo_spindleheadmt) = (c_tptpgeo_member3_mt))). % 30.02/30.21 intro zenon_D_pnotp. % 30.02/30.21 apply zenon_H472. % 30.02/30.21 rewrite <- zenon_D_pnotp. % 30.02/30.21 exact zenon_H476. % 30.02/30.21 cut (((c_tptpgeo_member3_mt) = (c_tptpgeo_member3_mt))); [idtac | apply NNPP; zenon_intro zenon_H477]. % 30.02/30.21 cut (((c_tptpgeo_member3_mt) = (c_tptpgeo_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H470]. % 30.02/30.21 congruence. % 30.02/30.21 exact (zenon_H470 zenon_H475). % 30.02/30.21 apply zenon_H477. apply refl_equal. % 30.02/30.21 apply zenon_H477. apply refl_equal. % 30.02/30.21 apply zenon_H473. zenon_intro ax1_212. % 30.02/30.21 generalize (zenon_H452 (c_tptpgeo_member3_mt)). zenon_intro zenon_H478. % 30.02/30.21 generalize (zenon_H478 (c_tptpgeo_spindleheadmt)). zenon_intro zenon_H479. % 30.02/30.21 generalize (zenon_H479 (c_worldgeographymt)). zenon_intro zenon_H47a. % 30.02/30.24 apply (zenon_imply_s _ _ zenon_H47a); [ zenon_intro zenon_H46f | zenon_intro zenon_H47b ]. % 30.02/30.24 exact (zenon_H46f ax1_212). % 30.02/30.24 apply (zenon_imply_s _ _ zenon_H47b); [ zenon_intro zenon_H47d | zenon_intro zenon_H47c ]. % 30.02/30.24 exact (zenon_H47d ax1_326). % 30.02/30.24 exact (zenon_H46c zenon_H47c). % 30.02/30.24 apply zenon_H471. apply refl_equal. % 30.02/30.24 exact (zenon_H467 zenon_H46a). % 30.02/30.24 exact (zenon_H456 zenon_H466). % 30.02/30.24 apply zenon_H453. zenon_intro zenon_Tx_bsg. apply NNPP. zenon_intro zenon_H47f. % 30.02/30.24 apply zenon_H47f. zenon_intro zenon_Ty_bsi. apply NNPP. zenon_intro zenon_H481. % 30.02/30.24 apply zenon_H481. zenon_intro zenon_Tz_bsk. apply NNPP. zenon_intro zenon_H483. % 30.02/30.24 apply (zenon_notimply_s _ _ zenon_H483). zenon_intro zenon_H485. zenon_intro zenon_H484. % 30.02/30.24 apply (zenon_notimply_s _ _ zenon_H484). zenon_intro zenon_H487. zenon_intro zenon_H486. % 30.02/30.24 generalize (ax1_1128 zenon_Tx_bsg). zenon_intro zenon_H488. % 30.02/30.24 generalize (zenon_H488 zenon_Ty_bsi). zenon_intro zenon_H489. % 30.02/30.24 generalize (zenon_H489 zenon_Tz_bsk). zenon_intro zenon_H48a. % 30.02/30.24 apply (zenon_imply_s _ _ zenon_H48a); [ zenon_intro zenon_H48c | zenon_intro zenon_H48b ]. % 30.02/30.24 apply (zenon_notand_s _ _ zenon_H48c); [ zenon_intro zenon_H48e | zenon_intro zenon_H48d ]. % 30.02/30.24 exact (zenon_H48e zenon_H485). % 30.02/30.24 exact (zenon_H48d zenon_H487). % 30.02/30.24 exact (zenon_H486 zenon_H48b). % 30.02/30.24 apply zenon_H451. zenon_intro zenon_Tx_bsx. apply NNPP. zenon_intro zenon_H490. % 30.02/30.24 apply zenon_H490. zenon_intro zenon_Ty_bsz. apply NNPP. zenon_intro zenon_H492. % 30.02/30.24 apply zenon_H492. zenon_intro zenon_Tz_btb. apply NNPP. zenon_intro zenon_H494. % 30.02/30.24 apply (zenon_notimply_s _ _ zenon_H494). zenon_intro zenon_H496. zenon_intro zenon_H495. % 30.02/30.24 apply (zenon_notimply_s _ _ zenon_H495). zenon_intro zenon_H498. zenon_intro zenon_H497. % 30.02/30.24 generalize (ax1_933 zenon_Tx_bsx). zenon_intro zenon_H499. % 30.02/30.24 generalize (zenon_H499 zenon_Ty_bsz). zenon_intro zenon_H49a. % 30.02/30.24 generalize (zenon_H49a zenon_Tz_btb). zenon_intro zenon_H49b. % 30.02/30.24 apply (zenon_imply_s _ _ zenon_H49b); [ zenon_intro zenon_H49d | zenon_intro zenon_H49c ]. % 30.02/30.24 apply (zenon_notand_s _ _ zenon_H49d); [ zenon_intro zenon_H49f | zenon_intro zenon_H49e ]. % 30.02/30.24 exact (zenon_H49f zenon_H496). % 30.02/30.24 exact (zenon_H49e zenon_H498). % 30.02/30.24 exact (zenon_H497 zenon_H49c). % 30.02/30.24 Qed. % 30.02/30.24 % SZS output end Proof % 30.02/30.24 (* END-PROOF *) % 30.02/30.24 nodes searched: 995568 % 30.02/30.24 max branch formulas: 501097 % 30.02/30.24 proof nodes created: 426 % 30.02/30.24 formulas created: 7304341 % 30.02/30.24 %------------------------------------------------------------------------------