%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG105+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n022.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 20:48:28 EDT 2022 % Result : Theorem 1.89s 2.05s % Output : Proof 1.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG105+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n022.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon May 30 15:08:52 EDT 2022 % 0.13/0.33 % CPUTime : % 1.89/2.05 (* PROOF-FOUND *) % 1.89/2.05 % SZS status Theorem % 1.89/2.05 (* BEGIN-PROOF *) % 1.89/2.05 % SZS output start Proof % 1.89/2.05 Theorem m__ : ((aElementOf0 (sdtpldt0 (xx) (xy)) (slsdtgt0 (xc)))/\(aElementOf0 (sdtasdt0 (xz) (xx)) (slsdtgt0 (xc)))). % 1.89/2.05 Proof. % 1.89/2.05 assert (zenon_L1_ : (~(exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xc) W3) = (sdtpldt0 (xx) (xy)))))) -> (aElement0 (xv)) -> (aElement0 (xu)) -> False). % 1.89/2.05 do 0 intro. intros zenon_H2c zenon_H2d zenon_H2e. % 1.89/2.05 apply zenon_H2c. exists (sdtpldt0 (xu) (xv)). apply NNPP. zenon_intro zenon_H2f. % 1.89/2.05 apply (zenon_notand_s _ _ zenon_H2f); [ zenon_intro zenon_H31 | zenon_intro zenon_H30 ]. % 1.89/2.05 generalize (mSortsB (xu)). zenon_intro zenon_H32. % 1.89/2.05 generalize (zenon_H32 (xv)). zenon_intro zenon_H33. % 1.89/2.05 apply (zenon_imply_s _ _ zenon_H33); [ zenon_intro zenon_H35 | zenon_intro zenon_H34 ]. % 1.89/2.05 apply (zenon_notand_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 1.89/2.05 exact (zenon_H37 zenon_H2e). % 1.89/2.05 exact (zenon_H36 zenon_H2d). % 1.89/2.05 exact (zenon_H31 zenon_H34). % 1.89/2.05 apply zenon_H30. apply sym_equal. exact m__2010. % 1.89/2.05 (* end of lemma zenon_L1_ *) % 1.89/2.05 assert (zenon_L2_ : (~(aElement0 (sdtasdt0 (xu) (xz)))) -> (aElement0 (xz)) -> (aElement0 (xu)) -> False). % 1.89/2.05 do 0 intro. intros zenon_H38 zenon_H39 zenon_H2e. % 1.89/2.05 generalize (mSortsB_02 (xu)). zenon_intro zenon_H3a. % 1.89/2.05 generalize (zenon_H3a (xz)). zenon_intro zenon_H3b. % 1.89/2.05 apply (zenon_imply_s _ _ zenon_H3b); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 1.89/2.05 apply (zenon_notand_s _ _ zenon_H3d); [ zenon_intro zenon_H37 | zenon_intro zenon_H3e ]. % 1.89/2.05 exact (zenon_H37 zenon_H2e). % 1.89/2.05 exact (zenon_H3e zenon_H39). % 1.89/2.05 exact (zenon_H38 zenon_H3c). % 1.89/2.05 (* end of lemma zenon_L2_ *) % 1.89/2.05 apply NNPP. intro zenon_G. % 1.89/2.05 apply (zenon_and_s _ _ m__1933). zenon_intro zenon_H40. zenon_intro zenon_H3f. % 1.89/2.05 apply (zenon_and_s _ _ zenon_H3f). zenon_intro zenon_H41. zenon_intro zenon_H39. % 1.89/2.05 apply (zenon_and_s _ _ m__1956). zenon_intro zenon_H2e. zenon_intro zenon_H42. % 1.89/2.05 apply (zenon_and_s _ _ m__1979). zenon_intro zenon_H2d. zenon_intro zenon_H43. % 1.89/2.05 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 1.89/2.05 generalize (mDefPrIdeal (xc)). zenon_intro zenon_H46. % 1.89/2.05 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 1.89/2.05 exact (zenon_H48 m__1905). % 1.89/2.05 generalize (zenon_H47 (slsdtgt0 (xc))). zenon_intro zenon_H49. % 1.89/2.05 apply (zenon_equiv_s _ _ zenon_H49); [ zenon_intro zenon_H4d; zenon_intro zenon_H4c | zenon_intro zenon_H4b; zenon_intro zenon_H4a ]. % 1.89/2.05 apply zenon_H4d. apply refl_equal. % 1.89/2.05 apply (zenon_and_s _ _ zenon_H4a). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 1.89/2.05 generalize (zenon_H4e (sdtpldt0 (xx) (xy))). zenon_intro zenon_H50. % 1.89/2.05 apply (zenon_equiv_s _ _ zenon_H50); [ zenon_intro zenon_H45; zenon_intro zenon_H2c | zenon_intro zenon_H52; zenon_intro zenon_H51 ]. % 1.89/2.05 apply (zenon_L1_); trivial. % 1.89/2.05 exact (zenon_H45 zenon_H52). % 1.89/2.05 generalize (mDefPrIdeal (xc)). zenon_intro zenon_H46. % 1.89/2.05 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 1.89/2.05 exact (zenon_H48 m__1905). % 1.89/2.05 generalize (zenon_H47 (slsdtgt0 (xc))). zenon_intro zenon_H49. % 1.89/2.05 apply (zenon_equiv_s _ _ zenon_H49); [ zenon_intro zenon_H4d; zenon_intro zenon_H4c | zenon_intro zenon_H4b; zenon_intro zenon_H4a ]. % 1.89/2.05 apply zenon_H4d. apply refl_equal. % 1.89/2.05 apply (zenon_and_s _ _ zenon_H4a). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 1.89/2.05 generalize (zenon_H4e (sdtasdt0 (xz) (xx))). zenon_intro zenon_H53. % 1.89/2.05 apply (zenon_equiv_s _ _ zenon_H53); [ zenon_intro zenon_H44; zenon_intro zenon_H56 | zenon_intro zenon_H55; zenon_intro zenon_H54 ]. % 1.89/2.05 apply zenon_H56. exists (sdtasdt0 (xu) (xz)). apply NNPP. zenon_intro zenon_H57. % 1.89/2.05 apply (zenon_notand_s _ _ zenon_H57); [ zenon_intro zenon_H38 | zenon_intro zenon_H58 ]. % 1.89/2.05 apply (zenon_L2_); trivial. % 1.89/2.05 apply zenon_H58. apply sym_equal. exact m__2043. % 1.89/2.05 exact (zenon_H44 zenon_H55). % 1.89/2.05 Qed. % 1.89/2.05 % SZS output end Proof % 1.89/2.05 (* END-PROOF *) % 1.89/2.05 nodes searched: 17040 % 1.89/2.05 max branch formulas: 3978 % 1.89/2.05 proof nodes created: 682 % 1.89/2.05 formulas created: 151925 % 1.89/2.05 %------------------------------------------------------------------------------