%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG061+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n019.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 89.29s 89.49s % Output : Proof 89.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : RNG061+2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.14/0.35 % Computer : n019.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Mon May 30 16:38:40 EDT 2022 % 0.14/0.35 % CPUTime : % 89.29/89.49 (* PROOF-FOUND *) % 89.29/89.49 % SZS status Theorem % 89.29/89.49 (* BEGIN-PROOF *) % 89.29/89.49 % SZS output start Proof % 89.29/89.49 Theorem m__ : ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))). % 89.29/89.49 Proof. % 89.29/89.49 assert (zenon_L1_ : (((sdtpldt0 (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) (sz0z00)) = (sdtpldt0 (smndt0 (xN)) (sdtpldt0 (sdtasdt0 (xS) (xS)) (sz0z00))))/\(((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))/\(((sdtasdt0 (sdtasdt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) (sz0z00)) = (sdtasdt0 (smndt0 (xN)) (sdtasdt0 (sdtasdt0 (xS) (xS)) (sz0z00))))/\((sdtasdt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtasdt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))))) -> (~((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))) -> False). % 89.29/89.49 do 0 intro. intros zenon_H3c zenon_H3d. % 89.29/89.49 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 89.29/89.49 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 89.29/89.50 exact (zenon_H3d zenon_H41). % 89.29/89.50 (* end of lemma zenon_L1_ *) % 89.29/89.50 apply NNPP. intro zenon_G. % 89.29/89.50 apply (zenon_and_s _ _ m__1930). zenon_intro zenon_H43. zenon_intro zenon_H42. % 89.29/89.50 apply (zenon_and_s _ _ m__1949). zenon_intro zenon_H45. zenon_intro zenon_H44. % 89.29/89.50 cut (((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))))) = ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))))). % 89.29/89.50 intro zenon_D_pnotp. % 89.29/89.50 apply zenon_G. % 89.29/89.50 rewrite <- zenon_D_pnotp. % 89.29/89.50 exact m__2180. % 89.29/89.50 cut (((sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS)))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))))); [idtac | apply NNPP; zenon_intro zenon_H46]. % 89.29/89.50 cut (((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) = (sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))))); [idtac | apply NNPP; zenon_intro zenon_H47]. % 89.29/89.50 congruence. % 89.29/89.50 apply zenon_H47. apply refl_equal. % 89.29/89.50 cut (((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))); [idtac | apply NNPP; zenon_intro zenon_H3d]. % 89.29/89.50 cut (((sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) = (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))))); [idtac | apply NNPP; zenon_intro zenon_H48]. % 89.29/89.50 congruence. % 89.29/89.50 apply zenon_H48. apply refl_equal. % 89.29/89.50 generalize (mArith (smndt0 (xN))). zenon_intro zenon_H49. % 89.29/89.50 generalize (mNegSc (xN)). zenon_intro zenon_H4a. % 89.29/89.50 apply (zenon_imply_s _ _ zenon_H4a); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 89.29/89.50 exact (zenon_H4c zenon_H45). % 89.29/89.50 generalize (zenon_H49 (sdtasdt0 (xS) (xS))). zenon_intro zenon_H4d. % 89.29/89.50 generalize (zenon_H4d (sz0z00)). zenon_intro zenon_H4e. % 89.29/89.50 apply (zenon_imply_s _ _ zenon_H4e); [ zenon_intro zenon_H4f | zenon_intro zenon_H3c ]. % 89.29/89.50 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 89.29/89.50 exact (zenon_H51 zenon_H4b). % 89.29/89.50 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 89.29/89.50 generalize (mMulSc (xS)). zenon_intro zenon_H54. % 89.29/89.50 generalize (zenon_H54 (xS)). zenon_intro zenon_H55. % 89.29/89.50 apply (zenon_imply_s _ _ zenon_H55); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 89.29/89.50 apply (zenon_notand_s _ _ zenon_H57); [ zenon_intro zenon_H58 | zenon_intro zenon_H58 ]. % 89.29/89.50 exact (zenon_H58 zenon_H43). % 89.29/89.50 exact (zenon_H58 zenon_H43). % 89.29/89.50 exact (zenon_H53 zenon_H56). % 89.29/89.50 exact (zenon_H52 mSZeroSc). % 89.29/89.50 apply (zenon_L1_); trivial. % 89.29/89.50 Qed. % 89.29/89.50 % SZS output end Proof % 89.29/89.50 (* END-PROOF *) % 89.29/89.50 nodes searched: 139124 % 89.29/89.50 max branch formulas: 19977 % 89.29/89.50 proof nodes created: 2451 % 89.29/89.50 formulas created: 1551271 % 89.29/89.50 %------------------------------------------------------------------------------