%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR065+3 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n013.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:26 EDT 2022 % Result : Theorem 63.17s 63.44s % Output : Proof 63.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR065+3 : TPTP v8.1.0. Released v3.4.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n013.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 : Sat Jun 11 02:03:28 EDT 2022 % 0.12/0.33 % CPUTime : % 63.17/63.44 (* PROOF-FOUND *) % 63.17/63.44 % SZS status Theorem % 63.17/63.44 (* BEGIN-PROOF *) % 63.17/63.44 % SZS output start Proof % 63.17/63.44 Theorem query165 : ((mtvisible (c_tptp_spindlecollectormt))->(tptpofobject (c_tptpridgeline_topographical) (f_tptpquantityfn_13 (n_468)))). % 63.17/63.44 Proof. % 63.17/63.44 assert (zenon_L1_ : (~((c_tptp_spindleheadmt) = (c_tptp_spindleheadmt))) -> False). % 63.17/63.44 do 0 intro. intros zenon_H1ce5. % 63.17/63.44 apply zenon_H1ce5. apply refl_equal. % 63.17/63.44 (* end of lemma zenon_L1_ *) % 63.17/63.44 apply NNPP. intro zenon_G. % 63.17/63.44 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_H1ce6 | zenon_intro zenon_H1ce7 ]. % 63.17/63.44 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H1ce9. zenon_intro zenon_H1ce8. % 63.17/63.44 apply (zenon_imply_s _ _ ax2_737); [ zenon_intro zenon_H1ceb | zenon_intro zenon_H1cea ]. % 63.17/63.44 generalize (ax2_7997 (c_tptp_spindlecollectormt)). zenon_intro zenon_H1cec. % 63.17/63.44 generalize (zenon_H1cec (c_cyclistsmt)). zenon_intro zenon_H1ced. % 63.17/63.44 apply (zenon_imply_s _ _ zenon_H1ced); [ zenon_intro zenon_H1cef | zenon_intro zenon_H1cee ]. % 63.17/63.44 apply (zenon_notand_s _ _ zenon_H1cef); [ zenon_intro zenon_H1cf1 | zenon_intro zenon_H1cf0 ]. % 63.17/63.44 exact (zenon_H1cf1 zenon_H1ce9). % 63.17/63.44 elim (classic ((~((c_tptp_spindlecollectormt) = (c_tptp_spindleheadmt)))/\(~(genlmt (c_tptp_spindlecollectormt) (c_tptp_spindleheadmt))))); [ zenon_intro zenon_H1cf2 | zenon_intro zenon_H1cf3 ]. % 63.17/63.44 apply (zenon_and_s _ _ zenon_H1cf2). zenon_intro zenon_H1cf5. zenon_intro zenon_H1cf4. % 63.17/63.44 elim (classic ((~((c_tptp_spindlecollectormt) = (c_tptp_member3993_mt)))/\(~(genlmt (c_tptp_spindlecollectormt) (c_tptp_member3993_mt))))); [ zenon_intro zenon_H1cf6 | zenon_intro zenon_H1cf7 ]. % 63.17/63.44 apply (zenon_and_s _ _ zenon_H1cf6). zenon_intro zenon_H1cf9. zenon_intro zenon_H1cf8. % 63.17/63.44 exact (zenon_H1cf8 ax2_923). % 63.17/63.44 cut ((genlmt (c_tptp_member3993_mt) (c_tptp_spindleheadmt)) = (genlmt (c_tptp_spindlecollectormt) (c_tptp_spindleheadmt))). % 63.17/63.44 intro zenon_D_pnotp. % 63.17/63.44 apply zenon_H1cf4. % 63.17/63.44 rewrite <- zenon_D_pnotp. % 63.17/63.44 exact ax2_723. % 63.17/63.44 cut (((c_tptp_spindleheadmt) = (c_tptp_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H1ce5]. % 63.17/63.44 cut (((c_tptp_member3993_mt) = (c_tptp_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H1cfa]. % 63.17/63.44 congruence. % 63.17/63.44 apply (zenon_notand_s _ _ zenon_H1cf7); [ zenon_intro zenon_H1cfc | zenon_intro zenon_H1cfb ]. % 63.17/63.44 apply zenon_H1cfc. zenon_intro zenon_H1cfd. % 63.17/63.44 elim (classic ((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt))); [ zenon_intro zenon_H1cfe | zenon_intro zenon_H1cff ]. % 63.17/63.44 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt)) = ((c_tptp_member3993_mt) = (c_tptp_spindlecollectormt))). % 63.17/63.44 intro zenon_D_pnotp. % 63.17/63.44 apply zenon_H1cfa. % 63.17/63.44 rewrite <- zenon_D_pnotp. % 63.17/63.44 exact zenon_H1cfe. % 63.17/63.44 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H1cff]. % 63.17/63.44 cut (((c_tptp_spindlecollectormt) = (c_tptp_member3993_mt))); [idtac | apply NNPP; zenon_intro zenon_H1cf9]. % 63.17/63.44 congruence. % 63.17/63.44 exact (zenon_H1cf9 zenon_H1cfd). % 63.17/63.44 apply zenon_H1cff. apply refl_equal. % 63.17/63.44 apply zenon_H1cff. apply refl_equal. % 63.17/63.44 apply zenon_H1cfb. zenon_intro ax2_923. % 63.17/63.44 generalize (zenon_H1ce6 (c_tptp_spindlecollectormt)). zenon_intro zenon_H1d00. % 63.17/63.44 generalize (zenon_H1d00 (c_tptp_member3993_mt)). zenon_intro zenon_H1d01. % 63.17/63.44 generalize (zenon_H1d01 (c_tptp_spindleheadmt)). zenon_intro zenon_H1d02. % 63.17/63.44 apply (zenon_imply_s _ _ zenon_H1d02); [ zenon_intro zenon_H1cf8 | zenon_intro zenon_H1d03 ]. % 63.17/63.44 exact (zenon_H1cf8 ax2_923). % 63.17/63.44 apply (zenon_imply_s _ _ zenon_H1d03); [ zenon_intro zenon_H1d05 | zenon_intro zenon_H1d04 ]. % 63.17/63.44 exact (zenon_H1d05 ax2_723). % 63.17/63.44 exact (zenon_H1cf4 zenon_H1d04). % 63.17/63.44 apply zenon_H1ce5. apply refl_equal. % 63.17/63.44 cut ((genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) = (genlmt (c_tptp_spindlecollectormt) (c_cyclistsmt))). % 63.17/63.44 intro zenon_D_pnotp. % 63.17/63.44 apply zenon_H1cf0. % 63.17/63.44 rewrite <- zenon_D_pnotp. % 63.17/63.44 exact ax2_4288. % 63.17/63.44 cut (((c_cyclistsmt) = (c_cyclistsmt))); [idtac | apply NNPP; zenon_intro zenon_H1d06]. % 63.17/63.44 cut (((c_tptp_spindleheadmt) = (c_tptp_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H1d07]. % 63.17/63.44 congruence. % 63.17/63.44 apply (zenon_notand_s _ _ zenon_H1cf3); [ zenon_intro zenon_H1d09 | zenon_intro zenon_H1d08 ]. % 63.17/63.44 apply zenon_H1d09. zenon_intro zenon_H1d0a. % 63.36/63.52 elim (classic ((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt))); [ zenon_intro zenon_H1cfe | zenon_intro zenon_H1cff ]. % 63.36/63.52 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt)) = ((c_tptp_spindleheadmt) = (c_tptp_spindlecollectormt))). % 63.36/63.52 intro zenon_D_pnotp. % 63.36/63.52 apply zenon_H1d07. % 63.36/63.52 rewrite <- zenon_D_pnotp. % 63.36/63.52 exact zenon_H1cfe. % 63.36/63.52 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H1cff]. % 63.36/63.52 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H1cf5]. % 63.36/63.52 congruence. % 63.36/63.52 exact (zenon_H1cf5 zenon_H1d0a). % 63.36/63.52 apply zenon_H1cff. apply refl_equal. % 63.36/63.52 apply zenon_H1cff. apply refl_equal. % 63.36/63.52 apply zenon_H1d08. zenon_intro zenon_H1d04. % 63.36/63.52 generalize (zenon_H1ce6 (c_tptp_spindlecollectormt)). zenon_intro zenon_H1d00. % 63.36/63.52 generalize (zenon_H1d00 (c_tptp_spindleheadmt)). zenon_intro zenon_H1d0b. % 63.36/63.52 generalize (zenon_H1d0b (c_cyclistsmt)). zenon_intro zenon_H1d0c. % 63.36/63.52 apply (zenon_imply_s _ _ zenon_H1d0c); [ zenon_intro zenon_H1cf4 | zenon_intro zenon_H1d0d ]. % 63.36/63.52 exact (zenon_H1cf4 zenon_H1d04). % 63.36/63.52 apply (zenon_imply_s _ _ zenon_H1d0d); [ zenon_intro zenon_H1d0f | zenon_intro zenon_H1d0e ]. % 63.36/63.52 exact (zenon_H1d0f ax2_4288). % 63.36/63.52 exact (zenon_H1cf0 zenon_H1d0e). % 63.36/63.52 apply zenon_H1d06. apply refl_equal. % 63.36/63.52 exact (zenon_H1ceb zenon_H1cee). % 63.36/63.52 generalize (ax2_2569 (c_tptpridgeline_topographical)). zenon_intro zenon_H1d10. % 63.36/63.52 apply (zenon_imply_s _ _ zenon_H1d10); [ zenon_intro zenon_H1d12 | zenon_intro zenon_H1d11 ]. % 63.36/63.52 apply (zenon_notand_s _ _ zenon_H1d12); [ zenon_intro zenon_H1d14 | zenon_intro zenon_H1d13 ]. % 63.36/63.52 generalize (ax2_7997 (c_tptp_spindlecollectormt)). zenon_intro zenon_H1cec. % 63.36/63.52 generalize (zenon_H1cec (c_tptp_member235_mt)). zenon_intro zenon_H1d15. % 63.36/63.52 apply (zenon_imply_s _ _ zenon_H1d15); [ zenon_intro zenon_H1d17 | zenon_intro zenon_H1d16 ]. % 63.36/63.52 apply (zenon_notand_s _ _ zenon_H1d17); [ zenon_intro zenon_H1cf1 | zenon_intro zenon_H1d18 ]. % 63.36/63.52 exact (zenon_H1cf1 zenon_H1ce9). % 63.36/63.52 exact (zenon_H1d18 ax2_279). % 63.36/63.52 exact (zenon_H1d14 zenon_H1d16). % 63.36/63.52 exact (zenon_H1d13 zenon_H1cea). % 63.36/63.52 exact (zenon_H1ce8 zenon_H1d11). % 63.36/63.52 apply zenon_H1ce7. zenon_intro zenon_Tx_lan. apply NNPP. zenon_intro zenon_H1d1a. % 63.36/63.52 apply zenon_H1d1a. zenon_intro zenon_Ty_lap. apply NNPP. zenon_intro zenon_H1d1c. % 63.36/63.52 apply zenon_H1d1c. zenon_intro zenon_Tz_lar. apply NNPP. zenon_intro zenon_H1d1e. % 63.36/63.52 apply (zenon_notimply_s _ _ zenon_H1d1e). zenon_intro zenon_H1d20. zenon_intro zenon_H1d1f. % 63.36/63.52 apply (zenon_notimply_s _ _ zenon_H1d1f). zenon_intro zenon_H1d22. zenon_intro zenon_H1d21. % 63.36/63.52 generalize (ax2_8002 zenon_Tx_lan). zenon_intro zenon_H1d23. % 63.36/63.52 generalize (zenon_H1d23 zenon_Ty_lap). zenon_intro zenon_H1d24. % 63.36/63.52 generalize (zenon_H1d24 zenon_Tz_lar). zenon_intro zenon_H1d25. % 63.36/63.52 apply (zenon_imply_s _ _ zenon_H1d25); [ zenon_intro zenon_H1d27 | zenon_intro zenon_H1d26 ]. % 63.36/63.52 apply (zenon_notand_s _ _ zenon_H1d27); [ zenon_intro zenon_H1d29 | zenon_intro zenon_H1d28 ]. % 63.36/63.52 exact (zenon_H1d29 zenon_H1d20). % 63.36/63.52 exact (zenon_H1d28 zenon_H1d22). % 63.36/63.52 exact (zenon_H1d21 zenon_H1d26). % 63.36/63.52 Qed. % 63.36/63.52 % SZS output end Proof % 63.36/63.52 (* END-PROOF *) % 63.36/63.52 nodes searched: 83826 % 63.36/63.52 max branch formulas: 60564 % 63.36/63.52 proof nodes created: 332 % 63.36/63.52 formulas created: 881928 % 63.36/63.52 %------------------------------------------------------------------------------