%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR037+3 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n028.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:58 EDT 2022 % Result : Theorem 1.19s 1.38s % Output : Proof 1.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : CSR037+3 : TPTP v8.1.0. Released v3.4.0. % 0.04/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jun 10 15:04:04 EDT 2022 % 0.13/0.35 % CPUTime : % 1.19/1.38 (* PROOF-FOUND *) % 1.19/1.38 % SZS status Theorem % 1.19/1.38 (* BEGIN-PROOF *) % 1.19/1.38 % SZS output start Proof % 1.19/1.38 Theorem query137 : ((mtvisible (c_tptpgeo_member7_mt))->(geographicalsubregions (c_georegion_l2_x5_y8) (c_georegion_l4_x45_y72))). % 1.19/1.38 Proof. % 1.19/1.38 assert (zenon_L1_ : (~((c_georegion_l4_x45_y72) = (c_georegion_l4_x45_y72))) -> False). % 1.19/1.38 do 0 intro. intros zenon_H1ce5. % 1.19/1.38 apply zenon_H1ce5. apply refl_equal. % 1.19/1.38 (* end of lemma zenon_L1_ *) % 1.19/1.38 apply NNPP. intro zenon_G. % 1.19/1.38 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((geographicalsubregions x y)->((geographicalsubregions y z)->(geographicalsubregions x z))))))); [ zenon_intro zenon_H1ce6 | zenon_intro zenon_H1ce7 ]. % 1.19/1.38 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H1ce9. zenon_intro zenon_H1ce8. % 1.19/1.38 apply (zenon_imply_s _ _ ax2_902); [ zenon_intro zenon_H1ceb | zenon_intro zenon_H1cea ]. % 1.19/1.38 exact (zenon_H1ceb zenon_H1ce9). % 1.19/1.38 apply (zenon_imply_s _ _ ax2_1656); [ zenon_intro zenon_H1ceb | zenon_intro zenon_H1cec ]. % 1.19/1.38 exact (zenon_H1ceb zenon_H1ce9). % 1.19/1.38 elim (classic ((~((c_georegion_l2_x5_y8) = (c_georegion_l3_x15_y24)))/\(~(geographicalsubregions (c_georegion_l2_x5_y8) (c_georegion_l3_x15_y24))))); [ zenon_intro zenon_H1ced | zenon_intro zenon_H1cee ]. % 1.19/1.38 apply (zenon_and_s _ _ zenon_H1ced). zenon_intro zenon_H1cf0. zenon_intro zenon_H1cef. % 1.19/1.38 exact (zenon_H1cef zenon_H1cea). % 1.19/1.38 cut ((geographicalsubregions (c_georegion_l3_x15_y24) (c_georegion_l4_x45_y72)) = (geographicalsubregions (c_georegion_l2_x5_y8) (c_georegion_l4_x45_y72))). % 1.19/1.38 intro zenon_D_pnotp. % 1.19/1.38 apply zenon_H1ce8. % 1.19/1.38 rewrite <- zenon_D_pnotp. % 1.19/1.38 exact zenon_H1cec. % 1.19/1.38 cut (((c_georegion_l4_x45_y72) = (c_georegion_l4_x45_y72))); [idtac | apply NNPP; zenon_intro zenon_H1ce5]. % 1.19/1.38 cut (((c_georegion_l3_x15_y24) = (c_georegion_l2_x5_y8))); [idtac | apply NNPP; zenon_intro zenon_H1cf1]. % 1.19/1.38 congruence. % 1.19/1.38 apply (zenon_notand_s _ _ zenon_H1cee); [ zenon_intro zenon_H1cf3 | zenon_intro zenon_H1cf2 ]. % 1.19/1.38 apply zenon_H1cf3. zenon_intro zenon_H1cf4. % 1.19/1.38 elim (classic ((c_georegion_l2_x5_y8) = (c_georegion_l2_x5_y8))); [ zenon_intro zenon_H1cf5 | zenon_intro zenon_H1cf6 ]. % 1.19/1.38 cut (((c_georegion_l2_x5_y8) = (c_georegion_l2_x5_y8)) = ((c_georegion_l3_x15_y24) = (c_georegion_l2_x5_y8))). % 1.19/1.38 intro zenon_D_pnotp. % 1.19/1.38 apply zenon_H1cf1. % 1.19/1.38 rewrite <- zenon_D_pnotp. % 1.19/1.38 exact zenon_H1cf5. % 1.19/1.38 cut (((c_georegion_l2_x5_y8) = (c_georegion_l2_x5_y8))); [idtac | apply NNPP; zenon_intro zenon_H1cf6]. % 1.19/1.38 cut (((c_georegion_l2_x5_y8) = (c_georegion_l3_x15_y24))); [idtac | apply NNPP; zenon_intro zenon_H1cf0]. % 1.19/1.38 congruence. % 1.19/1.38 exact (zenon_H1cf0 zenon_H1cf4). % 1.19/1.38 apply zenon_H1cf6. apply refl_equal. % 1.19/1.38 apply zenon_H1cf6. apply refl_equal. % 1.19/1.38 apply zenon_H1cf2. zenon_intro zenon_H1cea. % 1.19/1.38 generalize (zenon_H1ce6 (c_georegion_l2_x5_y8)). zenon_intro zenon_H1cf7. % 1.19/1.38 generalize (zenon_H1cf7 (c_georegion_l3_x15_y24)). zenon_intro zenon_H1cf8. % 1.19/1.38 generalize (zenon_H1cf8 (c_georegion_l4_x45_y72)). zenon_intro zenon_H1cf9. % 1.19/1.38 apply (zenon_imply_s _ _ zenon_H1cf9); [ zenon_intro zenon_H1cef | zenon_intro zenon_H1cfa ]. % 1.19/1.38 exact (zenon_H1cef zenon_H1cea). % 1.19/1.38 apply (zenon_imply_s _ _ zenon_H1cfa); [ zenon_intro zenon_H1cfc | zenon_intro zenon_H1cfb ]. % 1.19/1.38 exact (zenon_H1cfc zenon_H1cec). % 1.19/1.38 exact (zenon_H1ce8 zenon_H1cfb). % 1.19/1.38 apply zenon_H1ce5. apply refl_equal. % 1.19/1.38 apply zenon_H1ce7. zenon_intro zenon_Tx_kzl. apply NNPP. zenon_intro zenon_H1cfe. % 1.19/1.38 apply zenon_H1cfe. zenon_intro zenon_Ty_kzn. apply NNPP. zenon_intro zenon_H1d00. % 1.19/1.38 apply zenon_H1d00. zenon_intro zenon_Tz_kzp. apply NNPP. zenon_intro zenon_H1d02. % 1.19/1.38 apply (zenon_notimply_s _ _ zenon_H1d02). zenon_intro zenon_H1d04. zenon_intro zenon_H1d03. % 1.19/1.38 apply (zenon_notimply_s _ _ zenon_H1d03). zenon_intro zenon_H1d06. zenon_intro zenon_H1d05. % 1.19/1.38 generalize (ax2_7881 zenon_Tx_kzl). zenon_intro zenon_H1d07. % 1.19/1.38 generalize (zenon_H1d07 zenon_Ty_kzn). zenon_intro zenon_H1d08. % 1.19/1.38 generalize (zenon_H1d08 zenon_Tz_kzp). zenon_intro zenon_H1d09. % 1.19/1.38 apply (zenon_imply_s _ _ zenon_H1d09); [ zenon_intro zenon_H1d0b | zenon_intro zenon_H1d0a ]. % 1.19/1.38 apply (zenon_notand_s _ _ zenon_H1d0b); [ zenon_intro zenon_H1d0d | zenon_intro zenon_H1d0c ]. % 1.19/1.38 exact (zenon_H1d0d zenon_H1d04). % 1.19/1.38 exact (zenon_H1d0c zenon_H1d06). % 1.19/1.38 exact (zenon_H1d05 zenon_H1d0a). % 1.19/1.38 Qed. % 1.19/1.38 % SZS output end Proof % 1.19/1.38 (* END-PROOF *) % 1.19/1.38 nodes searched: 20877 % 1.19/1.38 max branch formulas: 23621 % 1.19/1.38 proof nodes created: 115 % 1.19/1.38 formulas created: 202090 % 1.19/1.38 %------------------------------------------------------------------------------