%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG070+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n027.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:24 EDT 2022 % Result : Theorem 259.17s 259.43s % Output : Proof 259.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : RNG070+2 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.13 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n027.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon May 30 08:42:16 EDT 2022 % 0.12/0.34 % CPUTime : % 259.17/259.43 (* PROOF-FOUND *) % 259.17/259.43 % SZS status Theorem % 259.17/259.43 (* BEGIN-PROOF *) % 259.17/259.43 % SZS output start Proof % 259.17/259.43 Theorem m__ : (sdtlseqdt0 (sdtpldt0 (xR) (xS)) (sdtpldt0 (xP) (xP))). % 259.17/259.43 Proof. % 259.17/259.43 assert (zenon_L1_ : (~(aScalar0 (sdtasdt0 (xE) (xH)))) -> (aScalar0 (xH)) -> (aScalar0 (xE)) -> False). % 259.17/259.43 do 0 intro. intros zenon_H3d zenon_H3e zenon_H3f. % 259.17/259.43 generalize (mMulSc (xE)). zenon_intro zenon_H40. % 259.17/259.43 generalize (zenon_H40 (xH)). zenon_intro zenon_H41. % 259.17/259.43 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 259.17/259.43 apply (zenon_notand_s _ _ zenon_H43); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 259.17/259.43 exact (zenon_H45 zenon_H3f). % 259.17/259.43 exact (zenon_H44 zenon_H3e). % 259.17/259.43 exact (zenon_H3d zenon_H42). % 259.17/259.43 (* end of lemma zenon_L1_ *) % 259.17/259.43 assert (zenon_L2_ : (~((xP) = (xP))) -> False). % 259.17/259.43 do 0 intro. intros zenon_H46. % 259.17/259.43 apply zenon_H46. apply refl_equal. % 259.17/259.43 (* end of lemma zenon_L2_ *) % 259.17/259.43 assert (zenon_L3_ : (~((sdtpldt0 (sdtasdt0 (xE) (xH)) (xP)) = (sdtpldt0 (xP) (xP)))) -> ((xP) = (sdtasdt0 (xE) (xH))) -> False). % 259.17/259.43 do 0 intro. intros zenon_H47 zenon_H48. % 259.17/259.43 cut (((xP) = (xP))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 259.17/259.43 cut (((sdtasdt0 (xE) (xH)) = (xP))); [idtac | apply NNPP; zenon_intro zenon_H49]. % 259.17/259.43 congruence. % 259.17/259.43 apply zenon_H49. apply sym_equal. exact zenon_H48. % 259.17/259.43 apply zenon_H46. apply refl_equal. % 259.17/259.43 (* end of lemma zenon_L3_ *) % 259.17/259.43 assert (zenon_L4_ : (forall W1 : zenon_U, (((aScalar0 (sdtasdt0 (xE) (xH)))/\(aScalar0 W1))->(aScalar0 (sdtpldt0 (sdtasdt0 (xE) (xH)) W1)))) -> (aScalar0 (xH)) -> (aScalar0 (xE)) -> (aScalar0 (xP)) -> (~(aScalar0 (sdtpldt0 (xP) (xP)))) -> ((xP) = (sdtasdt0 (xE) (xH))) -> False). % 259.17/259.43 do 0 intro. intros zenon_H4a zenon_H3e zenon_H3f zenon_H4b zenon_H4c zenon_H48. % 259.17/259.43 generalize (zenon_H4a (xP)). zenon_intro zenon_H4d. % 259.17/259.43 apply (zenon_imply_s _ _ zenon_H4d); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 259.17/259.43 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H3d | zenon_intro zenon_H50 ]. % 259.17/259.43 apply (zenon_L1_); trivial. % 259.17/259.43 exact (zenon_H50 zenon_H4b). % 259.17/259.43 cut ((aScalar0 (sdtpldt0 (sdtasdt0 (xE) (xH)) (xP))) = (aScalar0 (sdtpldt0 (xP) (xP)))). % 259.17/259.43 intro zenon_D_pnotp. % 259.17/259.43 apply zenon_H4c. % 259.17/259.43 rewrite <- zenon_D_pnotp. % 259.17/259.43 exact zenon_H4e. % 259.17/259.43 cut (((sdtpldt0 (sdtasdt0 (xE) (xH)) (xP)) = (sdtpldt0 (xP) (xP)))); [idtac | apply NNPP; zenon_intro zenon_H47]. % 259.17/259.43 congruence. % 259.17/259.43 apply (zenon_L3_); trivial. % 259.17/259.43 (* end of lemma zenon_L4_ *) % 259.17/259.43 assert (zenon_L5_ : (~(aScalar0 (sdtasdt0 (xC) (xG)))) -> (aScalar0 (xG)) -> (aScalar0 (xC)) -> False). % 259.17/259.43 do 0 intro. intros zenon_H51 zenon_H52 zenon_H53. % 259.17/259.43 generalize (mMulSc (xC)). zenon_intro zenon_H54. % 259.17/259.43 generalize (zenon_H54 (xG)). zenon_intro zenon_H55. % 259.17/259.43 apply (zenon_imply_s _ _ zenon_H55); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 259.17/259.43 apply (zenon_notand_s _ _ zenon_H57); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 259.17/259.43 exact (zenon_H59 zenon_H53). % 259.17/259.43 exact (zenon_H58 zenon_H52). % 259.17/259.43 exact (zenon_H51 zenon_H56). % 259.17/259.43 (* end of lemma zenon_L5_ *) % 259.17/259.43 assert (zenon_L6_ : (~((xS) = (xS))) -> False). % 259.17/259.43 do 0 intro. intros zenon_H5a. % 259.17/259.43 apply zenon_H5a. apply refl_equal. % 259.17/259.43 (* end of lemma zenon_L6_ *) % 259.17/259.43 assert (zenon_L7_ : (~((sdtpldt0 (sdtasdt0 (xC) (xG)) (xS)) = (sdtpldt0 (xR) (xS)))) -> ((xR) = (sdtasdt0 (xC) (xG))) -> False). % 259.17/259.43 do 0 intro. intros zenon_H5b zenon_H5c. % 259.17/259.43 cut (((xS) = (xS))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 259.17/259.43 cut (((sdtasdt0 (xC) (xG)) = (xR))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 259.17/259.43 congruence. % 259.17/259.43 apply zenon_H5d. apply sym_equal. exact zenon_H5c. % 259.17/259.43 apply zenon_H5a. apply refl_equal. % 259.17/259.43 (* end of lemma zenon_L7_ *) % 259.17/259.43 assert (zenon_L8_ : (forall W1 : zenon_U, (((aScalar0 (sdtasdt0 (xC) (xG)))/\(aScalar0 W1))->(aScalar0 (sdtpldt0 (sdtasdt0 (xC) (xG)) W1)))) -> (aScalar0 (xG)) -> (aScalar0 (xC)) -> (aScalar0 (xS)) -> (~(aScalar0 (sdtpldt0 (xR) (xS)))) -> ((xR) = (sdtasdt0 (xC) (xG))) -> False). % 259.17/259.43 do 0 intro. intros zenon_H5e zenon_H52 zenon_H53 zenon_H5f zenon_H60 zenon_H5c. % 259.17/259.43 generalize (zenon_H5e (xS)). zenon_intro zenon_H61. % 259.17/259.43 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 259.17/259.43 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H51 | zenon_intro zenon_H64 ]. % 259.17/259.43 apply (zenon_L5_); trivial. % 259.17/259.43 exact (zenon_H64 zenon_H5f). % 259.17/259.43 cut ((aScalar0 (sdtpldt0 (sdtasdt0 (xC) (xG)) (xS))) = (aScalar0 (sdtpldt0 (xR) (xS)))). % 259.17/259.44 intro zenon_D_pnotp. % 259.17/259.44 apply zenon_H60. % 259.17/259.44 rewrite <- zenon_D_pnotp. % 259.17/259.44 exact zenon_H62. % 259.17/259.44 cut (((sdtpldt0 (sdtasdt0 (xC) (xG)) (xS)) = (sdtpldt0 (xR) (xS)))); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 259.17/259.44 congruence. % 259.17/259.44 apply (zenon_L7_); trivial. % 259.17/259.44 (* end of lemma zenon_L8_ *) % 259.17/259.44 apply NNPP. intro zenon_G. % 259.17/259.44 apply (zenon_and_s _ _ m__1783). zenon_intro zenon_H53. zenon_intro zenon_H65. % 259.17/259.44 apply (zenon_and_s _ _ m__1820). zenon_intro zenon_H3f. zenon_intro zenon_H66. % 259.17/259.44 apply (zenon_and_s _ _ m__1854). zenon_intro zenon_H52. zenon_intro zenon_H67. % 259.17/259.44 apply (zenon_and_s _ _ m__1873). zenon_intro zenon_H3e. zenon_intro zenon_H68. % 259.17/259.44 apply (zenon_and_s _ _ m__1892). zenon_intro zenon_H69. zenon_intro zenon_H5c. % 259.17/259.44 apply (zenon_and_s _ _ m__1911). zenon_intro zenon_H4b. zenon_intro zenon_H48. % 259.17/259.44 apply (zenon_and_s _ _ m__1930). zenon_intro zenon_H5f. zenon_intro zenon_H6a. % 259.17/259.44 generalize (mSumSc (sdtasdt0 (xE) (xH))). zenon_intro zenon_H4a. % 259.17/259.44 generalize (mSumSc (sdtasdt0 (xC) (xG))). zenon_intro zenon_H5e. % 259.17/259.44 generalize (mLETot (sdtpldt0 (xP) (xP))). zenon_intro zenon_H6b. % 259.17/259.44 generalize (zenon_H6b (sdtpldt0 (xR) (xS))). zenon_intro zenon_H6c. % 259.17/259.44 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 259.17/259.44 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H4c | zenon_intro zenon_H60 ]. % 259.17/259.44 apply (zenon_L4_); trivial. % 259.17/259.44 apply (zenon_L8_); trivial. % 259.17/259.44 apply (zenon_or_s _ _ zenon_H6d); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 259.17/259.44 exact (m__2590 zenon_H70). % 259.17/259.44 exact (zenon_G zenon_H6f). % 259.17/259.44 Qed. % 259.17/259.44 % SZS output end Proof % 259.17/259.44 (* END-PROOF *) % 259.17/259.44 nodes searched: 498945 % 259.17/259.44 max branch formulas: 20186 % 259.17/259.44 proof nodes created: 11508 % 259.17/259.44 formulas created: 3905867 % 259.17/259.44 %------------------------------------------------------------------------------