%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SCT105+1 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n023.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 : Mon Jul 18 22:25:44 EDT 2022 % Result : Theorem 42.13s 42.32s % Output : Proof 42.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SCT105+1 : TPTP v8.1.0. Released v5.2.0. % 0.10/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n023.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 Jul 2 02:40:58 EDT 2022 % 0.12/0.34 % CPUTime : % 42.13/42.32 (* PROOF-FOUND *) % 42.13/42.32 % SZS status Theorem % 42.13/42.32 (* BEGIN-PROOF *) % 42.13/42.32 % SZS output start Proof % 42.13/42.32 Theorem conj_0 : (((c_Relation_Otrans (tc_Arrow__Order__Mirabelle_Oalt) (v_L))/\((forall B_x : zenon_U, (~(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_x B_x) (v_L))))/\(forall B_x : zenon_U, (forall B_y : zenon_U, ((~(B_x = B_y))->((c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_y B_x) (v_L))\/(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_x B_y) (v_L))))))))<->((c_Relation_Otrans (tc_Arrow__Order__Mirabelle_Oalt) (v_L))/\((forall B_x : zenon_U, (~(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_x B_x) (v_L))))/\(forall B_x : zenon_U, (forall B_y : zenon_U, ((~(B_x = B_y))->((c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_x B_y) (v_L))\/(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_y B_x) (v_L))))))))). % 42.13/42.32 Proof. % 42.13/42.32 assert (zenon_L1_ : (forall B_x : zenon_U, (forall B_y : zenon_U, ((c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_x B_y) (v_L))->(forall B_z : zenon_U, ((c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_y B_z) (v_L))->(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_x B_z) (v_L))))))) -> (~(c_Relation_Otrans (tc_Arrow__Order__Mirabelle_Oalt) (v_L))) -> False). % 42.13/42.32 do 0 intro. intros zenon_H1f7 zenon_H1f8. % 42.13/42.32 generalize (fact_trans__def (v_L)). zenon_intro zenon_H1f9. % 42.13/42.32 generalize (zenon_H1f9 (tc_Arrow__Order__Mirabelle_Oalt)). zenon_intro zenon_H1fa. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H1fa); [ zenon_intro zenon_H1f8; zenon_intro zenon_H1fc | zenon_intro zenon_H1fb; zenon_intro zenon_H1f7 ]. % 42.13/42.32 exact (zenon_H1fc zenon_H1f7). % 42.13/42.32 exact (zenon_H1f8 zenon_H1fb). % 42.13/42.32 (* end of lemma zenon_L1_ *) % 42.13/42.32 assert (zenon_L2_ : forall (zenon_TB_y_tr : zenon_U) (zenon_TB_x_ts : zenon_U), (c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_x_ts zenon_TB_y_tr) (v_L)) -> (~(hBOOL (hAPP (v_L) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_x_ts zenon_TB_y_tr)))) -> False). % 42.13/42.32 do 2 intro. intros zenon_H1fd zenon_H1fe. % 42.13/42.32 generalize (fact_mem__def (v_L)). zenon_intro zenon_H201. % 42.13/42.32 generalize (zenon_H201 (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_x_ts zenon_TB_y_tr)). zenon_intro zenon_H202. % 42.13/42.32 generalize (zenon_H202 (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt))). zenon_intro zenon_H203. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H203); [ zenon_intro zenon_H205; zenon_intro zenon_H1fe | zenon_intro zenon_H1fd; zenon_intro zenon_H204 ]. % 42.13/42.32 exact (zenon_H205 zenon_H1fd). % 42.13/42.32 exact (zenon_H1fe zenon_H204). % 42.13/42.32 (* end of lemma zenon_L2_ *) % 42.13/42.32 apply NNPP. intro zenon_G. % 42.13/42.32 apply (zenon_notequiv_s _ _ zenon_G); [ zenon_intro zenon_H209; zenon_intro zenon_H208 | zenon_intro zenon_H207; zenon_intro zenon_H206 ]. % 42.13/42.32 apply (zenon_and_s _ _ zenon_H208). zenon_intro zenon_H1fb. zenon_intro zenon_H20a. % 42.13/42.32 apply (zenon_and_s _ _ zenon_H20a). zenon_intro zenon_H20c. zenon_intro zenon_H20b. % 42.13/42.32 generalize (fact_trans__def (v_L)). zenon_intro zenon_H1f9. % 42.13/42.32 generalize (zenon_H1f9 (tc_Arrow__Order__Mirabelle_Oalt)). zenon_intro zenon_H1fa. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H1fa); [ zenon_intro zenon_H1f8; zenon_intro zenon_H1fc | zenon_intro zenon_H1fb; zenon_intro zenon_H1f7 ]. % 42.13/42.32 exact (zenon_H1f8 zenon_H1fb). % 42.13/42.32 apply (zenon_notand_s _ _ zenon_H209); [ zenon_intro zenon_H1f8 | zenon_intro zenon_H20d ]. % 42.13/42.32 apply (zenon_L1_); trivial. % 42.13/42.32 apply (zenon_notand_s _ _ zenon_H20d); [ zenon_intro zenon_H20f | zenon_intro zenon_H20e ]. % 42.13/42.32 exact (zenon_H20f zenon_H20c). % 42.13/42.32 apply (zenon_notallex_s (fun B_x : zenon_U => (forall B_y : zenon_U, ((~(B_x = B_y))->((c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_y B_x) (v_L))\/(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_x B_y) (v_L)))))) zenon_H20e); [ zenon_intro zenon_H210; idtac ]. % 42.13/42.32 elim zenon_H210. zenon_intro zenon_TB_x_uj. zenon_intro zenon_H212. % 42.13/42.32 apply (zenon_notallex_s (fun B_y : zenon_U => ((~(zenon_TB_x_uj = B_y))->((c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_y zenon_TB_x_uj) (v_L))\/(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_x_uj B_y) (v_L))))) zenon_H212); [ zenon_intro zenon_H213; idtac ]. % 42.13/42.32 elim zenon_H213. zenon_intro zenon_TB_y_um. zenon_intro zenon_H215. % 42.13/42.32 apply (zenon_notimply_s _ _ zenon_H215). zenon_intro zenon_H217. zenon_intro zenon_H216. % 42.13/42.32 apply (zenon_notor_s _ _ zenon_H216). zenon_intro zenon_H219. zenon_intro zenon_H218. % 42.13/42.32 generalize (fact_mem__def (v_L)). zenon_intro zenon_H201. % 42.13/42.32 generalize (zenon_H201 (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_y_um zenon_TB_x_uj)). zenon_intro zenon_H21a. % 42.13/42.32 generalize (zenon_H21a (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt))). zenon_intro zenon_H21b. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H21b); [ zenon_intro zenon_H219; zenon_intro zenon_H21e | zenon_intro zenon_H21d; zenon_intro zenon_H21c ]. % 42.13/42.32 generalize (fact_mem__def (v_L)). zenon_intro zenon_H201. % 42.13/42.32 generalize (zenon_H201 (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_x_uj zenon_TB_y_um)). zenon_intro zenon_H21f. % 42.13/42.32 generalize (zenon_H21f (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt))). zenon_intro zenon_H220. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H220); [ zenon_intro zenon_H218; zenon_intro zenon_H223 | zenon_intro zenon_H222; zenon_intro zenon_H221 ]. % 42.13/42.32 generalize (zenon_H20b zenon_TB_x_uj). zenon_intro zenon_H224. % 42.13/42.32 generalize (zenon_H224 zenon_TB_y_um). zenon_intro zenon_H225. % 42.13/42.32 apply (zenon_imply_s _ _ zenon_H225); [ zenon_intro zenon_H227 | zenon_intro zenon_H226 ]. % 42.13/42.32 exact (zenon_H227 zenon_H217). % 42.13/42.32 apply (zenon_or_s _ _ zenon_H226); [ zenon_intro zenon_H222 | zenon_intro zenon_H21d ]. % 42.13/42.32 generalize (fact_mem__def (v_L)). zenon_intro zenon_H201. % 42.13/42.32 generalize (zenon_H201 (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_x_uj zenon_TB_y_um)). zenon_intro zenon_H21f. % 42.13/42.32 generalize (zenon_H21f (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt))). zenon_intro zenon_H220. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H220); [ zenon_intro zenon_H218; zenon_intro zenon_H223 | zenon_intro zenon_H222; zenon_intro zenon_H221 ]. % 42.13/42.32 exact (zenon_H218 zenon_H222). % 42.13/42.32 exact (zenon_H223 zenon_H221). % 42.13/42.32 generalize (fact_mem__def (v_L)). zenon_intro zenon_H201. % 42.13/42.32 generalize (zenon_H201 (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_y_um zenon_TB_x_uj)). zenon_intro zenon_H21a. % 42.13/42.32 generalize (zenon_H21a (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt))). zenon_intro zenon_H21b. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H21b); [ zenon_intro zenon_H219; zenon_intro zenon_H21e | zenon_intro zenon_H21d; zenon_intro zenon_H21c ]. % 42.13/42.32 exact (zenon_H219 zenon_H21d). % 42.13/42.32 exact (zenon_H21e zenon_H21c). % 42.13/42.32 exact (zenon_H218 zenon_H222). % 42.13/42.32 exact (zenon_H219 zenon_H21d). % 42.13/42.32 apply (zenon_and_s _ _ zenon_H207). zenon_intro zenon_H1fb. zenon_intro zenon_H228. % 42.13/42.32 apply (zenon_and_s _ _ zenon_H228). zenon_intro zenon_H20c. zenon_intro zenon_H229. % 42.13/42.32 generalize (fact_trans__def (v_L)). zenon_intro zenon_H1f9. % 42.13/42.32 generalize (zenon_H1f9 (tc_Arrow__Order__Mirabelle_Oalt)). zenon_intro zenon_H1fa. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H1fa); [ zenon_intro zenon_H1f8; zenon_intro zenon_H1fc | zenon_intro zenon_H1fb; zenon_intro zenon_H1f7 ]. % 42.13/42.32 exact (zenon_H1f8 zenon_H1fb). % 42.13/42.32 apply (zenon_notand_s _ _ zenon_H206); [ zenon_intro zenon_H1f8 | zenon_intro zenon_H22a ]. % 42.13/42.32 apply (zenon_L1_); trivial. % 42.13/42.32 apply (zenon_notand_s _ _ zenon_H22a); [ zenon_intro zenon_H20f | zenon_intro zenon_H22b ]. % 42.13/42.32 exact (zenon_H20f zenon_H20c). % 42.13/42.32 apply (zenon_notallex_s (fun B_x : zenon_U => (forall B_y : zenon_U, ((~(B_x = B_y))->((c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_x B_y) (v_L))\/(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_y B_x) (v_L)))))) zenon_H22b); [ zenon_intro zenon_H22c; idtac ]. % 42.13/42.32 elim zenon_H22c. zenon_intro zenon_TB_x_ts. zenon_intro zenon_H22d. % 42.13/42.32 apply (zenon_notallex_s (fun B_y : zenon_U => ((~(zenon_TB_x_ts = B_y))->((c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_x_ts B_y) (v_L))\/(c_member (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt)) (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) B_y zenon_TB_x_ts) (v_L))))) zenon_H22d); [ zenon_intro zenon_H22e; idtac ]. % 42.13/42.32 elim zenon_H22e. zenon_intro zenon_TB_y_tr. zenon_intro zenon_H22f. % 42.13/42.32 apply (zenon_notimply_s _ _ zenon_H22f). zenon_intro zenon_H231. zenon_intro zenon_H230. % 42.13/42.32 apply (zenon_notor_s _ _ zenon_H230). zenon_intro zenon_H205. zenon_intro zenon_H232. % 42.13/42.32 generalize (fact_mem__def (v_L)). zenon_intro zenon_H201. % 42.13/42.32 generalize (zenon_H201 (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_x_ts zenon_TB_y_tr)). zenon_intro zenon_H202. % 42.13/42.32 generalize (zenon_H202 (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt))). zenon_intro zenon_H203. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H203); [ zenon_intro zenon_H205; zenon_intro zenon_H1fe | zenon_intro zenon_H1fd; zenon_intro zenon_H204 ]. % 42.13/42.32 generalize (fact_mem__def (v_L)). zenon_intro zenon_H201. % 42.13/42.32 generalize (zenon_H201 (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_y_tr zenon_TB_x_ts)). zenon_intro zenon_H233. % 42.13/42.32 generalize (zenon_H233 (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt))). zenon_intro zenon_H234. % 42.13/42.32 apply (zenon_equiv_s _ _ zenon_H234); [ zenon_intro zenon_H232; zenon_intro zenon_H237 | zenon_intro zenon_H236; zenon_intro zenon_H235 ]. % 42.13/42.32 generalize (zenon_H229 zenon_TB_x_ts). zenon_intro zenon_H238. % 42.13/42.32 generalize (zenon_H238 zenon_TB_y_tr). zenon_intro zenon_H239. % 42.13/42.32 apply (zenon_imply_s _ _ zenon_H239); [ zenon_intro zenon_H23b | zenon_intro zenon_H23a ]. % 42.13/42.32 exact (zenon_H23b zenon_H231). % 42.13/42.32 apply (zenon_or_s _ _ zenon_H23a); [ zenon_intro zenon_H236 | zenon_intro zenon_H1fd ]. % 42.13/42.32 generalize (fact_mem__def (v_L)). zenon_intro zenon_H201. % 42.13/42.32 generalize (zenon_H201 (c_Product__Type_OPair (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt) zenon_TB_y_tr zenon_TB_x_ts)). zenon_intro zenon_H233. % 42.13/42.32 generalize (zenon_H233 (tc_prod (tc_Arrow__Order__Mirabelle_Oalt) (tc_Arrow__Order__Mirabelle_Oalt))). zenon_intro zenon_H234. % 42.16/42.34 apply (zenon_equiv_s _ _ zenon_H234); [ zenon_intro zenon_H232; zenon_intro zenon_H237 | zenon_intro zenon_H236; zenon_intro zenon_H235 ]. % 42.16/42.34 exact (zenon_H232 zenon_H236). % 42.16/42.34 exact (zenon_H237 zenon_H235). % 42.16/42.34 apply (zenon_L2_ zenon_TB_y_tr zenon_TB_x_ts); trivial. % 42.16/42.34 exact (zenon_H232 zenon_H236). % 42.16/42.34 exact (zenon_H205 zenon_H1fd). % 42.16/42.34 Qed. % 42.16/42.34 % SZS output end Proof % 42.16/42.34 (* END-PROOF *) % 42.16/42.34 nodes searched: 348964 % 42.16/42.34 max branch formulas: 194539 % 42.16/42.34 proof nodes created: 5569 % 42.16/42.34 formulas created: 2570126 % 42.16/42.34 %------------------------------------------------------------------------------