%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR074+2 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n019.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 18.84s 19.01s % Output : Proof 18.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : CSR074+2 : TPTP v8.1.0. Released v3.4.0. % 0.00/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n019.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.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Thu Jun 9 22:37:55 EDT 2022 % 0.12/0.34 % CPUTime : % 18.84/19.01 (* PROOF-FOUND *) % 18.84/19.01 % SZS status Theorem % 18.84/19.01 (* BEGIN-PROOF *) % 18.84/19.01 % SZS output start Proof % 18.84/19.01 Theorem query124 : ((mtvisible (c_tptpgeo_member7_mt))->((inregion (c_geolocation_x53_y74) (c_georegion_l3_x17_y24))/\(geolevel_3 (c_georegion_l3_x17_y24)))). % 18.84/19.01 Proof. % 18.84/19.01 apply NNPP. intro zenon_G. % 18.84/19.01 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 ]. % 18.84/19.01 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 ]. % 18.84/19.01 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H455. zenon_intro zenon_H454. % 18.84/19.01 apply (zenon_notand_s _ _ zenon_H454); [ zenon_intro zenon_H457 | zenon_intro zenon_H456 ]. % 18.84/19.01 apply (zenon_imply_s _ _ ax1_82); [ zenon_intro zenon_H459 | zenon_intro zenon_H458 ]. % 18.84/19.01 exact (zenon_H459 zenon_H455). % 18.84/19.01 apply (zenon_imply_s _ _ ax1_472); [ zenon_intro zenon_H459 | zenon_intro zenon_H45a ]. % 18.84/19.01 exact (zenon_H459 zenon_H455). % 18.84/19.01 elim (classic (inregion (c_georegion_l4_x53_y74) (c_georegion_l3_x17_y24))); [ zenon_intro zenon_H45b | zenon_intro zenon_H45c ]. % 18.84/19.01 generalize (zenon_H450 (c_geolocation_x53_y74)). zenon_intro zenon_H45d. % 18.84/19.01 generalize (zenon_H45d (c_georegion_l4_x53_y74)). zenon_intro zenon_H45e. % 18.84/19.01 generalize (zenon_H45e (c_georegion_l3_x17_y24)). zenon_intro zenon_H45f. % 18.84/19.01 apply (zenon_imply_s _ _ zenon_H45f); [ zenon_intro zenon_H461 | zenon_intro zenon_H460 ]. % 18.84/19.01 exact (zenon_H461 zenon_H458). % 18.84/19.01 apply (zenon_imply_s _ _ zenon_H460); [ zenon_intro zenon_H45c | zenon_intro zenon_H462 ]. % 18.84/19.01 exact (zenon_H45c zenon_H45b). % 18.84/19.01 exact (zenon_H457 zenon_H462). % 18.84/19.01 generalize (ax1_128 (c_georegion_l3_x17_y24)). zenon_intro zenon_H463. % 18.84/19.01 generalize (zenon_H463 (c_georegion_l4_x53_y74)). zenon_intro zenon_H464. % 18.84/19.01 apply (zenon_imply_s _ _ zenon_H464); [ zenon_intro zenon_H465 | zenon_intro zenon_H45b ]. % 18.84/19.01 exact (zenon_H465 zenon_H45a). % 18.84/19.01 exact (zenon_H45c zenon_H45b). % 18.84/19.01 apply (zenon_imply_s _ _ ax1_478); [ zenon_intro zenon_H467 | zenon_intro zenon_H466 ]. % 18.84/19.01 generalize (ax1_1123 (c_tptpgeo_member7_mt)). zenon_intro zenon_H468. % 18.84/19.01 generalize (zenon_H468 (c_worldgeographymt)). zenon_intro zenon_H469. % 18.84/19.01 apply (zenon_imply_s _ _ zenon_H469); [ zenon_intro zenon_H46b | zenon_intro zenon_H46a ]. % 18.84/19.01 apply (zenon_notand_s _ _ zenon_H46b); [ zenon_intro zenon_H459 | zenon_intro zenon_H46c ]. % 18.84/19.01 exact (zenon_H459 zenon_H455). % 18.84/19.01 elim (classic ((~((c_tptpgeo_member7_mt) = (c_tptpgeo_spindleheadmt)))/\(~(genlmt (c_tptpgeo_member7_mt) (c_tptpgeo_spindleheadmt))))); [ zenon_intro zenon_H46d | zenon_intro zenon_H46e ]. % 18.84/19.01 apply (zenon_and_s _ _ zenon_H46d). zenon_intro zenon_H470. zenon_intro zenon_H46f. % 18.84/19.01 exact (zenon_H46f ax1_63). % 18.84/19.01 cut ((genlmt (c_tptpgeo_spindleheadmt) (c_worldgeographymt)) = (genlmt (c_tptpgeo_member7_mt) (c_worldgeographymt))). % 18.84/19.01 intro zenon_D_pnotp. % 18.84/19.01 apply zenon_H46c. % 18.84/19.01 rewrite <- zenon_D_pnotp. % 18.84/19.01 exact ax1_326. % 18.84/19.01 cut (((c_worldgeographymt) = (c_worldgeographymt))); [idtac | apply NNPP; zenon_intro zenon_H471]. % 18.84/19.01 cut (((c_tptpgeo_spindleheadmt) = (c_tptpgeo_member7_mt))); [idtac | apply NNPP; zenon_intro zenon_H472]. % 18.84/19.01 congruence. % 18.84/19.01 apply (zenon_notand_s _ _ zenon_H46e); [ zenon_intro zenon_H474 | zenon_intro zenon_H473 ]. % 18.84/19.01 apply zenon_H474. zenon_intro zenon_H475. % 18.84/19.01 elim (classic ((c_tptpgeo_member7_mt) = (c_tptpgeo_member7_mt))); [ zenon_intro zenon_H476 | zenon_intro zenon_H477 ]. % 18.84/19.01 cut (((c_tptpgeo_member7_mt) = (c_tptpgeo_member7_mt)) = ((c_tptpgeo_spindleheadmt) = (c_tptpgeo_member7_mt))). % 18.84/19.01 intro zenon_D_pnotp. % 18.84/19.01 apply zenon_H472. % 18.84/19.01 rewrite <- zenon_D_pnotp. % 18.84/19.01 exact zenon_H476. % 18.84/19.01 cut (((c_tptpgeo_member7_mt) = (c_tptpgeo_member7_mt))); [idtac | apply NNPP; zenon_intro zenon_H477]. % 18.84/19.01 cut (((c_tptpgeo_member7_mt) = (c_tptpgeo_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H470]. % 18.84/19.01 congruence. % 18.84/19.01 exact (zenon_H470 zenon_H475). % 18.84/19.01 apply zenon_H477. apply refl_equal. % 18.84/19.01 apply zenon_H477. apply refl_equal. % 18.84/19.01 apply zenon_H473. zenon_intro ax1_63. % 18.84/19.01 generalize (zenon_H452 (c_tptpgeo_member7_mt)). zenon_intro zenon_H478. % 18.84/19.01 generalize (zenon_H478 (c_tptpgeo_spindleheadmt)). zenon_intro zenon_H479. % 18.84/19.01 generalize (zenon_H479 (c_worldgeographymt)). zenon_intro zenon_H47a. % 18.84/19.04 apply (zenon_imply_s _ _ zenon_H47a); [ zenon_intro zenon_H46f | zenon_intro zenon_H47b ]. % 18.84/19.04 exact (zenon_H46f ax1_63). % 18.84/19.04 apply (zenon_imply_s _ _ zenon_H47b); [ zenon_intro zenon_H47d | zenon_intro zenon_H47c ]. % 18.84/19.04 exact (zenon_H47d ax1_326). % 18.84/19.04 exact (zenon_H46c zenon_H47c). % 18.84/19.04 apply zenon_H471. apply refl_equal. % 18.84/19.04 exact (zenon_H467 zenon_H46a). % 18.84/19.04 exact (zenon_H456 zenon_H466). % 18.84/19.04 apply zenon_H453. zenon_intro zenon_Tx_bsg. apply NNPP. zenon_intro zenon_H47f. % 18.84/19.04 apply zenon_H47f. zenon_intro zenon_Ty_bsi. apply NNPP. zenon_intro zenon_H481. % 18.84/19.04 apply zenon_H481. zenon_intro zenon_Tz_bsk. apply NNPP. zenon_intro zenon_H483. % 18.84/19.04 apply (zenon_notimply_s _ _ zenon_H483). zenon_intro zenon_H485. zenon_intro zenon_H484. % 18.84/19.04 apply (zenon_notimply_s _ _ zenon_H484). zenon_intro zenon_H487. zenon_intro zenon_H486. % 18.84/19.04 generalize (ax1_1128 zenon_Tx_bsg). zenon_intro zenon_H488. % 18.84/19.04 generalize (zenon_H488 zenon_Ty_bsi). zenon_intro zenon_H489. % 18.84/19.04 generalize (zenon_H489 zenon_Tz_bsk). zenon_intro zenon_H48a. % 18.84/19.04 apply (zenon_imply_s _ _ zenon_H48a); [ zenon_intro zenon_H48c | zenon_intro zenon_H48b ]. % 18.84/19.04 apply (zenon_notand_s _ _ zenon_H48c); [ zenon_intro zenon_H48e | zenon_intro zenon_H48d ]. % 18.84/19.04 exact (zenon_H48e zenon_H485). % 18.84/19.04 exact (zenon_H48d zenon_H487). % 18.84/19.04 exact (zenon_H486 zenon_H48b). % 18.84/19.04 apply zenon_H451. zenon_intro zenon_Tx_bsx. apply NNPP. zenon_intro zenon_H490. % 18.84/19.04 apply zenon_H490. zenon_intro zenon_Ty_bsz. apply NNPP. zenon_intro zenon_H492. % 18.84/19.04 apply zenon_H492. zenon_intro zenon_Tz_btb. apply NNPP. zenon_intro zenon_H494. % 18.84/19.04 apply (zenon_notimply_s _ _ zenon_H494). zenon_intro zenon_H496. zenon_intro zenon_H495. % 18.84/19.04 apply (zenon_notimply_s _ _ zenon_H495). zenon_intro zenon_H498. zenon_intro zenon_H497. % 18.84/19.04 generalize (ax1_933 zenon_Tx_bsx). zenon_intro zenon_H499. % 18.84/19.04 generalize (zenon_H499 zenon_Ty_bsz). zenon_intro zenon_H49a. % 18.84/19.04 generalize (zenon_H49a zenon_Tz_btb). zenon_intro zenon_H49b. % 18.84/19.04 apply (zenon_imply_s _ _ zenon_H49b); [ zenon_intro zenon_H49d | zenon_intro zenon_H49c ]. % 18.84/19.04 apply (zenon_notand_s _ _ zenon_H49d); [ zenon_intro zenon_H49f | zenon_intro zenon_H49e ]. % 18.84/19.04 exact (zenon_H49f zenon_H496). % 18.84/19.04 exact (zenon_H49e zenon_H498). % 18.84/19.04 exact (zenon_H497 zenon_H49c). % 18.84/19.04 Qed. % 18.84/19.04 % SZS output end Proof % 18.84/19.04 (* END-PROOF *) % 18.84/19.04 nodes searched: 680332 % 18.84/19.04 max branch formulas: 346667 % 18.84/19.04 proof nodes created: 351 % 18.84/19.04 formulas created: 5015634 % 18.84/19.04 %------------------------------------------------------------------------------