%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG067+2 : 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:23 EDT 2022 % Result : Theorem 0.18s 0.57s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : RNG067+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n022.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 22:12:52 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.57 (* PROOF-FOUND *) % 0.18/0.57 % SZS status Theorem % 0.18/0.57 (* BEGIN-PROOF *) % 0.18/0.57 % SZS output start Proof % 0.18/0.57 Theorem m__ : (sdtlseqdt0 (sdtpldt0 (sdtpldt0 (sdtpldt0 (sdtasdt0 (xP) (xP)) (sdtasdt0 (xP) (xP))) (sdtasdt0 (xP) (xP))) (sdtasdt0 (xP) (xP))) (sdtpldt0 (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (sdtasdt0 (xS) (xS))) (xN)) (xN))). % 0.18/0.57 Proof. % 0.18/0.57 assert (zenon_L1_ : (~(aScalar0 (sdtasdt0 (xP) (xP)))) -> (aScalar0 (xP)) -> False). % 0.18/0.57 do 0 intro. intros zenon_H3b zenon_H3c. % 0.18/0.57 generalize (mMulSc (xP)). zenon_intro zenon_H3d. % 0.18/0.57 generalize (zenon_H3d (xP)). zenon_intro zenon_H3e. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H40); [ zenon_intro zenon_H41 | zenon_intro zenon_H41 ]. % 0.18/0.57 exact (zenon_H41 zenon_H3c). % 0.18/0.57 exact (zenon_H41 zenon_H3c). % 0.18/0.57 exact (zenon_H3b zenon_H3f). % 0.18/0.57 (* end of lemma zenon_L1_ *) % 0.18/0.57 assert (zenon_L2_ : (~(aScalar0 (sdtpldt0 (sdtasdt0 (xP) (xP)) (sdtasdt0 (xP) (xP))))) -> (aScalar0 (xP)) -> False). % 0.18/0.57 do 0 intro. intros zenon_H42 zenon_H3c. % 0.18/0.57 generalize (mSumSc (sdtasdt0 (xP) (xP))). zenon_intro zenon_H43. % 0.18/0.57 generalize (zenon_H43 (sdtasdt0 (xP) (xP))). zenon_intro zenon_H44. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H44); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H3b | zenon_intro zenon_H3b ]. % 0.18/0.57 apply (zenon_L1_); trivial. % 0.18/0.57 apply (zenon_L1_); trivial. % 0.18/0.57 exact (zenon_H42 zenon_H45). % 0.18/0.57 (* end of lemma zenon_L2_ *) % 0.18/0.57 assert (zenon_L3_ : (~(aScalar0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (sdtasdt0 (xS) (xS))))) -> (aScalar0 (xS)) -> (aScalar0 (xR)) -> False). % 0.18/0.57 do 0 intro. intros zenon_H47 zenon_H48 zenon_H49. % 0.18/0.57 generalize (mSumSc (sdtasdt0 (xR) (xR))). zenon_intro zenon_H4a. % 0.18/0.57 generalize (zenon_H4a (sdtasdt0 (xS) (xS))). zenon_intro zenon_H4b. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H4b); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 0.18/0.57 generalize (mMulSc (xR)). zenon_intro zenon_H50. % 0.18/0.57 generalize (zenon_H50 (xR)). zenon_intro zenon_H51. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H53); [ zenon_intro zenon_H54 | zenon_intro zenon_H54 ]. % 0.18/0.57 exact (zenon_H54 zenon_H49). % 0.18/0.57 exact (zenon_H54 zenon_H49). % 0.18/0.57 exact (zenon_H4f zenon_H52). % 0.18/0.57 generalize (mMulSc (xS)). zenon_intro zenon_H55. % 0.18/0.57 generalize (zenon_H55 (xS)). zenon_intro zenon_H56. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H56); [ zenon_intro zenon_H58 | zenon_intro zenon_H57 ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H58); [ zenon_intro zenon_H59 | zenon_intro zenon_H59 ]. % 0.18/0.57 exact (zenon_H59 zenon_H48). % 0.18/0.57 exact (zenon_H59 zenon_H48). % 0.18/0.57 exact (zenon_H4e zenon_H57). % 0.18/0.57 exact (zenon_H47 zenon_H4c). % 0.18/0.57 (* end of lemma zenon_L3_ *) % 0.18/0.57 apply NNPP. intro zenon_G. % 0.18/0.57 apply (zenon_and_s _ _ m__1892). zenon_intro zenon_H49. zenon_intro zenon_H5a. % 0.18/0.57 apply (zenon_and_s _ _ m__1911). zenon_intro zenon_H3c. zenon_intro zenon_H5b. % 0.18/0.57 apply (zenon_and_s _ _ m__1930). zenon_intro zenon_H48. zenon_intro zenon_H5c. % 0.18/0.57 apply (zenon_and_s _ _ m__1949). zenon_intro zenon_H5e. zenon_intro zenon_H5d. % 0.18/0.57 generalize (mLEMon (sdtpldt0 (sdtpldt0 (sdtasdt0 (xP) (xP)) (sdtasdt0 (xP) (xP))) (sdtasdt0 (xP) (xP)))). zenon_intro zenon_H5f. % 0.18/0.57 generalize (zenon_H5f (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (sdtasdt0 (xS) (xS))) (xN))). zenon_intro zenon_H60. % 0.18/0.57 generalize (zenon_H60 (sdtasdt0 (xP) (xP))). zenon_intro zenon_H61. % 0.18/0.57 generalize (zenon_H61 (xN)). zenon_intro zenon_H62. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H62); [ zenon_intro zenon_H64 | zenon_intro zenon_H63 ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H64); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 0.18/0.57 generalize (mSumSc (sdtpldt0 (sdtasdt0 (xP) (xP)) (sdtasdt0 (xP) (xP)))). zenon_intro zenon_H67. % 0.18/0.57 generalize (zenon_H67 (sdtasdt0 (xP) (xP))). zenon_intro zenon_H68. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H42 | zenon_intro zenon_H3b ]. % 0.18/0.57 apply (zenon_L2_); trivial. % 0.18/0.57 apply (zenon_L1_); trivial. % 0.18/0.57 exact (zenon_H66 zenon_H69). % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H65); [ zenon_intro zenon_H6c | zenon_intro zenon_H6b ]. % 0.18/0.57 generalize (mSumSc (sdtpldt0 (sdtasdt0 (xR) (xR)) (sdtasdt0 (xS) (xS)))). zenon_intro zenon_H6d. % 0.18/0.57 generalize (zenon_H6d (xN)). zenon_intro zenon_H6e. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H6e); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H47 | zenon_intro zenon_H71 ]. % 0.18/0.57 apply (zenon_L3_); trivial. % 0.18/0.57 exact (zenon_H71 zenon_H5e). % 0.18/0.57 exact (zenon_H6c zenon_H6f). % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H6b); [ zenon_intro zenon_H3b | zenon_intro zenon_H71 ]. % 0.18/0.57 apply (zenon_L1_); trivial. % 0.18/0.57 exact (zenon_H71 zenon_H5e). % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H63); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H73); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 0.18/0.57 generalize (mLEMon (sdtpldt0 (sdtasdt0 (xP) (xP)) (sdtasdt0 (xP) (xP)))). zenon_intro zenon_H76. % 0.18/0.57 generalize (zenon_H76 (sdtpldt0 (sdtasdt0 (xR) (xR)) (sdtasdt0 (xS) (xS)))). zenon_intro zenon_H77. % 0.18/0.57 generalize (zenon_H77 (sdtasdt0 (xP) (xP))). zenon_intro zenon_H78. % 0.18/0.57 generalize (zenon_H78 (xN)). zenon_intro zenon_H79. % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H79); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H7b); [ zenon_intro zenon_H42 | zenon_intro zenon_H7c ]. % 0.18/0.57 apply (zenon_L2_); trivial. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H7c); [ zenon_intro zenon_H47 | zenon_intro zenon_H6b ]. % 0.18/0.57 apply (zenon_L3_); trivial. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H6b); [ zenon_intro zenon_H3b | zenon_intro zenon_H71 ]. % 0.18/0.57 apply (zenon_L1_); trivial. % 0.18/0.57 exact (zenon_H71 zenon_H5e). % 0.18/0.57 apply (zenon_imply_s _ _ zenon_H7a); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 0.18/0.57 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H7f | zenon_intro zenon_H74 ]. % 0.18/0.57 exact (zenon_H7f m__2104). % 0.18/0.57 exact (zenon_H74 m__2004). % 0.18/0.57 exact (zenon_H75 zenon_H7d). % 0.18/0.57 exact (zenon_H74 m__2004). % 0.18/0.57 exact (zenon_G zenon_H72). % 0.18/0.57 Qed. % 0.18/0.57 % SZS output end Proof % 0.18/0.57 (* END-PROOF *) % 0.18/0.57 nodes searched: 1269 % 0.18/0.57 max branch formulas: 642 % 0.18/0.57 proof nodes created: 78 % 0.18/0.57 formulas created: 13280 % 0.18/0.57 %------------------------------------------------------------------------------