%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG108+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n029.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 9.93s 10.13s % Output : Proof 9.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : RNG108+1 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n029.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 : Mon May 30 19:41:44 EDT 2022 % 0.12/0.33 % CPUTime : % 9.93/10.13 (* PROOF-FOUND *) % 9.93/10.13 % SZS status Theorem % 9.93/10.13 (* BEGIN-PROOF *) % 9.93/10.13 % SZS output start Proof % 9.93/10.13 Theorem m__ : ((aElementOf0 (sz00) (slsdtgt0 (xa)))/\((aElementOf0 (xa) (slsdtgt0 (xa)))/\((aElementOf0 (sz00) (slsdtgt0 (xb)))/\(aElementOf0 (xb) (slsdtgt0 (xb)))))). % 9.93/10.13 Proof. % 9.93/10.13 assert (zenon_L1_ : (~(exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xa) W3) = (sz00))))) -> (aElement0 (xa)) -> False). % 9.93/10.13 do 0 intro. intros zenon_H2b zenon_H2c. % 9.93/10.13 apply zenon_H2b. exists (sz00). apply NNPP. zenon_intro zenon_H2d. % 9.93/10.13 apply (zenon_notand_s _ _ zenon_H2d); [ zenon_intro zenon_H2f | zenon_intro zenon_H2e ]. % 9.93/10.13 exact (zenon_H2f mSortsC). % 9.93/10.13 generalize (mMulZero (xa)). zenon_intro zenon_H30. % 9.93/10.13 apply (zenon_imply_s _ _ zenon_H30); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 9.93/10.13 exact (zenon_H32 zenon_H2c). % 9.93/10.13 apply (zenon_and_s _ _ zenon_H31). zenon_intro zenon_H34. zenon_intro zenon_H33. % 9.93/10.13 exact (zenon_H2e zenon_H34). % 9.93/10.13 (* end of lemma zenon_L1_ *) % 9.93/10.13 assert (zenon_L2_ : (aElement0 (xa)) -> (~(exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xa) W3) = (xa))))) -> False). % 9.93/10.13 do 0 intro. intros zenon_H2c zenon_H35. % 9.93/10.13 generalize (mMulUnit (xa)). zenon_intro zenon_H36. % 9.93/10.13 apply (zenon_imply_s _ _ zenon_H36); [ zenon_intro zenon_H32 | zenon_intro zenon_H37 ]. % 9.93/10.13 exact (zenon_H32 zenon_H2c). % 9.93/10.13 apply (zenon_and_s _ _ zenon_H37). zenon_intro zenon_H39. zenon_intro zenon_H38. % 9.93/10.13 apply zenon_H35. exists (sz10). apply NNPP. zenon_intro zenon_H3a. % 9.93/10.13 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H3c | zenon_intro zenon_H3b ]. % 9.93/10.13 exact (zenon_H3c mSortsC_01). % 9.93/10.13 exact (zenon_H3b zenon_H39). % 9.93/10.13 (* end of lemma zenon_L2_ *) % 9.93/10.13 assert (zenon_L3_ : (~(exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xb) W3) = (sz00))))) -> (aElement0 (xb)) -> False). % 9.93/10.13 do 0 intro. intros zenon_H3d zenon_H3e. % 9.93/10.13 apply zenon_H3d. exists (sz00). apply NNPP. zenon_intro zenon_H3f. % 9.93/10.13 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H2f | zenon_intro zenon_H40 ]. % 9.93/10.13 exact (zenon_H2f mSortsC). % 9.93/10.13 generalize (mMulZero (xb)). zenon_intro zenon_H41. % 9.93/10.13 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 9.93/10.14 exact (zenon_H43 zenon_H3e). % 9.93/10.14 apply (zenon_and_s _ _ zenon_H42). zenon_intro zenon_H45. zenon_intro zenon_H44. % 9.93/10.14 exact (zenon_H40 zenon_H45). % 9.93/10.14 (* end of lemma zenon_L3_ *) % 9.93/10.14 assert (zenon_L4_ : (aElement0 (xb)) -> (~(exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xb) W3) = (xb))))) -> False). % 9.93/10.14 do 0 intro. intros zenon_H3e zenon_H46. % 9.93/10.14 generalize (mMulUnit (xb)). zenon_intro zenon_H47. % 9.93/10.14 apply (zenon_imply_s _ _ zenon_H47); [ zenon_intro zenon_H43 | zenon_intro zenon_H48 ]. % 9.93/10.14 exact (zenon_H43 zenon_H3e). % 9.93/10.14 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H4a. zenon_intro zenon_H49. % 9.93/10.14 apply zenon_H46. exists (sz10). apply NNPP. zenon_intro zenon_H4b. % 9.93/10.14 apply (zenon_notand_s _ _ zenon_H4b); [ zenon_intro zenon_H3c | zenon_intro zenon_H4c ]. % 9.93/10.14 exact (zenon_H3c mSortsC_01). % 9.93/10.14 exact (zenon_H4c zenon_H4a). % 9.93/10.14 (* end of lemma zenon_L4_ *) % 9.93/10.14 apply NNPP. intro zenon_G. % 9.93/10.14 apply (zenon_and_s _ _ m__2091). zenon_intro zenon_H2c. zenon_intro zenon_H3e. % 9.93/10.14 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H4e | zenon_intro zenon_H4d ]. % 9.93/10.14 generalize (mDefPrIdeal (xa)). zenon_intro zenon_H4f. % 9.93/10.14 apply (zenon_imply_s _ _ zenon_H4f); [ zenon_intro zenon_H32 | zenon_intro zenon_H50 ]. % 9.93/10.14 exact (zenon_H32 zenon_H2c). % 9.93/10.14 generalize (zenon_H50 (slsdtgt0 (xa))). zenon_intro zenon_H51. % 9.93/10.14 apply (zenon_equiv_s _ _ zenon_H51); [ zenon_intro zenon_H55; zenon_intro zenon_H54 | zenon_intro zenon_H53; zenon_intro zenon_H52 ]. % 9.93/10.14 apply zenon_H55. apply refl_equal. % 9.93/10.14 apply (zenon_and_s _ _ zenon_H52). zenon_intro zenon_H57. zenon_intro zenon_H56. % 9.93/10.14 generalize (zenon_H56 (sz00)). zenon_intro zenon_H58. % 9.93/10.14 apply (zenon_equiv_s _ _ zenon_H58); [ zenon_intro zenon_H4e; zenon_intro zenon_H2b | zenon_intro zenon_H5a; zenon_intro zenon_H59 ]. % 9.93/10.14 apply (zenon_L1_); trivial. % 9.93/10.14 exact (zenon_H4e zenon_H5a). % 9.93/10.14 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 9.93/10.14 generalize (mDefPrIdeal (xa)). zenon_intro zenon_H4f. % 9.93/10.14 apply (zenon_imply_s _ _ zenon_H4f); [ zenon_intro zenon_H32 | zenon_intro zenon_H50 ]. % 9.93/10.14 exact (zenon_H32 zenon_H2c). % 9.93/10.14 generalize (zenon_H50 (slsdtgt0 (xa))). zenon_intro zenon_H51. % 9.93/10.14 apply (zenon_equiv_s _ _ zenon_H51); [ zenon_intro zenon_H55; zenon_intro zenon_H54 | zenon_intro zenon_H53; zenon_intro zenon_H52 ]. % 9.93/10.14 apply zenon_H55. apply refl_equal. % 9.93/10.14 apply (zenon_and_s _ _ zenon_H52). zenon_intro zenon_H57. zenon_intro zenon_H56. % 9.93/10.14 generalize (zenon_H56 (xa)). zenon_intro zenon_H5d. % 9.93/10.14 apply (zenon_equiv_s _ _ zenon_H5d); [ zenon_intro zenon_H5c; zenon_intro zenon_H35 | zenon_intro zenon_H5f; zenon_intro zenon_H5e ]. % 9.93/10.14 apply (zenon_L2_); trivial. % 9.93/10.14 exact (zenon_H5c zenon_H5f). % 9.93/10.14 apply (zenon_notand_s _ _ zenon_H5b); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 9.93/10.14 generalize (mDefPrIdeal (xb)). zenon_intro zenon_H62. % 9.93/10.14 apply (zenon_imply_s _ _ zenon_H62); [ zenon_intro zenon_H43 | zenon_intro zenon_H63 ]. % 9.93/10.14 exact (zenon_H43 zenon_H3e). % 9.93/10.14 generalize (zenon_H63 (slsdtgt0 (xb))). zenon_intro zenon_H64. % 9.93/10.14 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H68; zenon_intro zenon_H67 | zenon_intro zenon_H66; zenon_intro zenon_H65 ]. % 9.93/10.14 apply zenon_H68. apply refl_equal. % 9.93/10.14 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 9.93/10.14 generalize (zenon_H69 (sz00)). zenon_intro zenon_H6b. % 9.93/10.14 apply (zenon_equiv_s _ _ zenon_H6b); [ zenon_intro zenon_H61; zenon_intro zenon_H3d | zenon_intro zenon_H6d; zenon_intro zenon_H6c ]. % 9.93/10.14 apply (zenon_L3_); trivial. % 9.93/10.14 exact (zenon_H61 zenon_H6d). % 9.93/10.14 generalize (mDefPrIdeal (xb)). zenon_intro zenon_H62. % 9.93/10.14 apply (zenon_imply_s _ _ zenon_H62); [ zenon_intro zenon_H43 | zenon_intro zenon_H63 ]. % 9.93/10.14 exact (zenon_H43 zenon_H3e). % 9.93/10.14 generalize (zenon_H63 (slsdtgt0 (xb))). zenon_intro zenon_H64. % 9.93/10.14 apply (zenon_equiv_s _ _ zenon_H64); [ zenon_intro zenon_H68; zenon_intro zenon_H67 | zenon_intro zenon_H66; zenon_intro zenon_H65 ]. % 9.93/10.14 apply zenon_H68. apply refl_equal. % 9.93/10.14 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 9.93/10.14 generalize (zenon_H69 (xb)). zenon_intro zenon_H6e. % 9.93/10.14 apply (zenon_equiv_s _ _ zenon_H6e); [ zenon_intro zenon_H60; zenon_intro zenon_H46 | zenon_intro zenon_H70; zenon_intro zenon_H6f ]. % 9.93/10.14 apply (zenon_L4_); trivial. % 9.93/10.14 exact (zenon_H60 zenon_H70). % 9.93/10.14 Qed. % 9.93/10.14 % SZS output end Proof % 9.93/10.14 (* END-PROOF *) % 9.93/10.14 nodes searched: 244356 % 9.93/10.14 max branch formulas: 5154 % 9.93/10.14 proof nodes created: 9051 % 9.93/10.14 formulas created: 767149 % 9.93/10.14 %------------------------------------------------------------------------------