%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR026+3 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.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:48 EDT 2022 % Result : Theorem 80.69s 80.90s % Output : Proof 80.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : CSR026+3 : TPTP v8.1.0. Released v3.4.0. % 0.04/0.14 % Command : run_zenon %s %d % 0.14/0.36 % Computer : n026.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Sat Jun 11 17:22:49 EDT 2022 % 0.14/0.36 % CPUTime : % 80.69/80.90 (* PROOF-FOUND *) % 80.69/80.90 % SZS status Theorem % 80.69/80.90 (* BEGIN-PROOF *) % 80.69/80.90 % SZS output start Proof % 80.69/80.90 Theorem query126 : ((mtvisible (c_tptp_spindlecollectormt))->(tptpofobject (c_tptprunningshorts) (f_tptpquantityfn_2 (n_756)))). % 80.69/80.90 Proof. % 80.69/80.90 assert (zenon_L1_ : (~((c_tptp_spindleheadmt) = (c_tptp_spindleheadmt))) -> False). % 80.69/80.90 do 0 intro. intros zenon_H1ce5. % 80.69/80.90 apply zenon_H1ce5. apply refl_equal. % 80.69/80.90 (* end of lemma zenon_L1_ *) % 80.69/80.90 apply NNPP. intro zenon_G. % 80.69/80.90 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 ]. % 80.69/80.90 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H1ce9. zenon_intro zenon_H1ce8. % 80.69/80.90 apply (zenon_imply_s _ _ ax2_1317); [ zenon_intro zenon_H1ceb | zenon_intro zenon_H1cea ]. % 80.69/80.90 generalize (ax2_7997 (c_tptp_spindlecollectormt)). zenon_intro zenon_H1cec. % 80.69/80.90 generalize (zenon_H1cec (c_cyclistsmt)). zenon_intro zenon_H1ced. % 80.69/80.90 apply (zenon_imply_s _ _ zenon_H1ced); [ zenon_intro zenon_H1cef | zenon_intro zenon_H1cee ]. % 80.69/80.90 apply (zenon_notand_s _ _ zenon_H1cef); [ zenon_intro zenon_H1cf1 | zenon_intro zenon_H1cf0 ]. % 80.69/80.90 exact (zenon_H1cf1 zenon_H1ce9). % 80.69/80.90 elim (classic ((~((c_tptp_spindlecollectormt) = (c_tptp_spindleheadmt)))/\(~(genlmt (c_tptp_spindlecollectormt) (c_tptp_spindleheadmt))))); [ zenon_intro zenon_H1cf2 | zenon_intro zenon_H1cf3 ]. % 80.69/80.90 apply (zenon_and_s _ _ zenon_H1cf2). zenon_intro zenon_H1cf5. zenon_intro zenon_H1cf4. % 80.69/80.90 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 ]. % 80.69/80.90 apply (zenon_and_s _ _ zenon_H1cf6). zenon_intro zenon_H1cf9. zenon_intro zenon_H1cf8. % 80.69/80.90 exact (zenon_H1cf8 ax2_923). % 80.69/80.90 cut ((genlmt (c_tptp_member3993_mt) (c_tptp_spindleheadmt)) = (genlmt (c_tptp_spindlecollectormt) (c_tptp_spindleheadmt))). % 80.69/80.90 intro zenon_D_pnotp. % 80.69/80.90 apply zenon_H1cf4. % 80.69/80.90 rewrite <- zenon_D_pnotp. % 80.69/80.90 exact ax2_723. % 80.69/80.90 cut (((c_tptp_spindleheadmt) = (c_tptp_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H1ce5]. % 80.69/80.90 cut (((c_tptp_member3993_mt) = (c_tptp_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H1cfa]. % 80.69/80.90 congruence. % 80.69/80.90 apply (zenon_notand_s _ _ zenon_H1cf7); [ zenon_intro zenon_H1cfc | zenon_intro zenon_H1cfb ]. % 80.69/80.90 apply zenon_H1cfc. zenon_intro zenon_H1cfd. % 80.69/80.90 elim (classic ((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt))); [ zenon_intro zenon_H1cfe | zenon_intro zenon_H1cff ]. % 80.69/80.90 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt)) = ((c_tptp_member3993_mt) = (c_tptp_spindlecollectormt))). % 80.69/80.90 intro zenon_D_pnotp. % 80.69/80.90 apply zenon_H1cfa. % 80.69/80.90 rewrite <- zenon_D_pnotp. % 80.69/80.90 exact zenon_H1cfe. % 80.69/80.90 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H1cff]. % 80.69/80.90 cut (((c_tptp_spindlecollectormt) = (c_tptp_member3993_mt))); [idtac | apply NNPP; zenon_intro zenon_H1cf9]. % 80.69/80.90 congruence. % 80.69/80.90 exact (zenon_H1cf9 zenon_H1cfd). % 80.69/80.90 apply zenon_H1cff. apply refl_equal. % 80.69/80.90 apply zenon_H1cff. apply refl_equal. % 80.69/80.90 apply zenon_H1cfb. zenon_intro ax2_923. % 80.69/80.90 generalize (zenon_H1ce6 (c_tptp_spindlecollectormt)). zenon_intro zenon_H1d00. % 80.69/80.90 generalize (zenon_H1d00 (c_tptp_member3993_mt)). zenon_intro zenon_H1d01. % 80.69/80.90 generalize (zenon_H1d01 (c_tptp_spindleheadmt)). zenon_intro zenon_H1d02. % 80.69/80.90 apply (zenon_imply_s _ _ zenon_H1d02); [ zenon_intro zenon_H1cf8 | zenon_intro zenon_H1d03 ]. % 80.69/80.90 exact (zenon_H1cf8 ax2_923). % 80.69/80.90 apply (zenon_imply_s _ _ zenon_H1d03); [ zenon_intro zenon_H1d05 | zenon_intro zenon_H1d04 ]. % 80.69/80.90 exact (zenon_H1d05 ax2_723). % 80.69/80.90 exact (zenon_H1cf4 zenon_H1d04). % 80.69/80.90 apply zenon_H1ce5. apply refl_equal. % 80.69/80.90 cut ((genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) = (genlmt (c_tptp_spindlecollectormt) (c_cyclistsmt))). % 80.69/80.90 intro zenon_D_pnotp. % 80.69/80.90 apply zenon_H1cf0. % 80.69/80.90 rewrite <- zenon_D_pnotp. % 80.69/80.90 exact ax2_4288. % 80.69/80.90 cut (((c_cyclistsmt) = (c_cyclistsmt))); [idtac | apply NNPP; zenon_intro zenon_H1d06]. % 80.69/80.90 cut (((c_tptp_spindleheadmt) = (c_tptp_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H1d07]. % 80.69/80.90 congruence. % 80.69/80.90 apply (zenon_notand_s _ _ zenon_H1cf3); [ zenon_intro zenon_H1d09 | zenon_intro zenon_H1d08 ]. % 80.69/80.90 apply zenon_H1d09. zenon_intro zenon_H1d0a. % 80.82/80.98 elim (classic ((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt))); [ zenon_intro zenon_H1cfe | zenon_intro zenon_H1cff ]. % 80.82/80.98 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt)) = ((c_tptp_spindleheadmt) = (c_tptp_spindlecollectormt))). % 80.82/80.98 intro zenon_D_pnotp. % 80.82/80.98 apply zenon_H1d07. % 80.82/80.98 rewrite <- zenon_D_pnotp. % 80.82/80.98 exact zenon_H1cfe. % 80.82/80.98 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindlecollectormt))); [idtac | apply NNPP; zenon_intro zenon_H1cff]. % 80.82/80.98 cut (((c_tptp_spindlecollectormt) = (c_tptp_spindleheadmt))); [idtac | apply NNPP; zenon_intro zenon_H1cf5]. % 80.82/80.98 congruence. % 80.82/80.98 exact (zenon_H1cf5 zenon_H1d0a). % 80.82/80.98 apply zenon_H1cff. apply refl_equal. % 80.82/80.98 apply zenon_H1cff. apply refl_equal. % 80.82/80.98 apply zenon_H1d08. zenon_intro zenon_H1d04. % 80.82/80.98 generalize (zenon_H1ce6 (c_tptp_spindlecollectormt)). zenon_intro zenon_H1d00. % 80.82/80.98 generalize (zenon_H1d00 (c_tptp_spindleheadmt)). zenon_intro zenon_H1d0b. % 80.82/80.98 generalize (zenon_H1d0b (c_cyclistsmt)). zenon_intro zenon_H1d0c. % 80.82/80.98 apply (zenon_imply_s _ _ zenon_H1d0c); [ zenon_intro zenon_H1cf4 | zenon_intro zenon_H1d0d ]. % 80.82/80.98 exact (zenon_H1cf4 zenon_H1d04). % 80.82/80.98 apply (zenon_imply_s _ _ zenon_H1d0d); [ zenon_intro zenon_H1d0f | zenon_intro zenon_H1d0e ]. % 80.82/80.98 exact (zenon_H1d0f ax2_4288). % 80.82/80.98 exact (zenon_H1cf0 zenon_H1d0e). % 80.82/80.98 apply zenon_H1d06. apply refl_equal. % 80.82/80.98 exact (zenon_H1ceb zenon_H1cee). % 80.82/80.98 generalize (ax2_1907 (c_tptprunningshorts)). zenon_intro zenon_H1d10. % 80.82/80.98 apply (zenon_imply_s _ _ zenon_H1d10); [ zenon_intro zenon_H1d12 | zenon_intro zenon_H1d11 ]. % 80.82/80.98 apply (zenon_notand_s _ _ zenon_H1d12); [ zenon_intro zenon_H1d14 | zenon_intro zenon_H1d13 ]. % 80.82/80.98 generalize (ax2_7997 (c_tptp_spindlecollectormt)). zenon_intro zenon_H1cec. % 80.82/80.98 generalize (zenon_H1cec (c_tptp_member2701_mt)). zenon_intro zenon_H1d15. % 80.82/80.98 apply (zenon_imply_s _ _ zenon_H1d15); [ zenon_intro zenon_H1d17 | zenon_intro zenon_H1d16 ]. % 80.82/80.98 apply (zenon_notand_s _ _ zenon_H1d17); [ zenon_intro zenon_H1cf1 | zenon_intro zenon_H1d18 ]. % 80.82/80.98 exact (zenon_H1cf1 zenon_H1ce9). % 80.82/80.98 exact (zenon_H1d18 ax2_1645). % 80.82/80.98 exact (zenon_H1d14 zenon_H1d16). % 80.82/80.98 exact (zenon_H1d13 zenon_H1cea). % 80.82/80.98 exact (zenon_H1ce8 zenon_H1d11). % 80.82/80.98 apply zenon_H1ce7. zenon_intro zenon_Tx_lan. apply NNPP. zenon_intro zenon_H1d1a. % 80.82/80.98 apply zenon_H1d1a. zenon_intro zenon_Ty_lap. apply NNPP. zenon_intro zenon_H1d1c. % 80.82/80.98 apply zenon_H1d1c. zenon_intro zenon_Tz_lar. apply NNPP. zenon_intro zenon_H1d1e. % 80.82/80.98 apply (zenon_notimply_s _ _ zenon_H1d1e). zenon_intro zenon_H1d20. zenon_intro zenon_H1d1f. % 80.82/80.98 apply (zenon_notimply_s _ _ zenon_H1d1f). zenon_intro zenon_H1d22. zenon_intro zenon_H1d21. % 80.82/80.98 generalize (ax2_8002 zenon_Tx_lan). zenon_intro zenon_H1d23. % 80.82/80.98 generalize (zenon_H1d23 zenon_Ty_lap). zenon_intro zenon_H1d24. % 80.82/80.98 generalize (zenon_H1d24 zenon_Tz_lar). zenon_intro zenon_H1d25. % 80.82/80.98 apply (zenon_imply_s _ _ zenon_H1d25); [ zenon_intro zenon_H1d27 | zenon_intro zenon_H1d26 ]. % 80.82/80.98 apply (zenon_notand_s _ _ zenon_H1d27); [ zenon_intro zenon_H1d29 | zenon_intro zenon_H1d28 ]. % 80.82/80.98 exact (zenon_H1d29 zenon_H1d20). % 80.82/80.98 exact (zenon_H1d28 zenon_H1d22). % 80.82/80.98 exact (zenon_H1d21 zenon_H1d26). % 80.82/80.98 Qed. % 80.82/80.98 % SZS output end Proof % 80.82/80.98 (* END-PROOF *) % 80.82/80.98 nodes searched: 83752 % 80.82/80.98 max branch formulas: 60583 % 80.82/80.98 proof nodes created: 337 % 80.82/80.98 formulas created: 881668 % 80.82/80.98 %------------------------------------------------------------------------------