%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM505+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n013.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 15:56:18 EDT 2022 % Result : Theorem 261.86s 262.06s % Output : Proof 261.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : NUM505+1 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.14 % Command : run_zenon %s %d % 0.15/0.36 % Computer : n013.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Tue Jul 5 12:21:29 EDT 2022 % 0.15/0.36 % CPUTime : % 261.86/262.06 (* PROOF-FOUND *) % 261.86/262.06 % SZS status Theorem % 261.86/262.06 (* BEGIN-PROOF *) % 261.86/262.06 % SZS output start Proof % 261.86/262.06 Theorem m__ : ((~(sdtlseqdt0 (xp) (xk)))->((~((xk) = (xp)))/\(sdtlseqdt0 (xk) (xp)))). % 261.86/262.06 Proof. % 261.86/262.06 assert (zenon_L1_ : (aNaturalNumber0 (xp)) -> ((xp) = (sz00)) -> (isPrime0 (xp)) -> False). % 261.86/262.06 do 0 intro. intros zenon_H32 zenon_H33 zenon_H34. % 261.86/262.06 generalize (mDefPrime (xp)). zenon_intro zenon_H35. % 261.86/262.06 apply (zenon_imply_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 261.86/262.06 exact (zenon_H37 zenon_H32). % 261.86/262.06 apply (zenon_equiv_s _ _ zenon_H36); [ zenon_intro zenon_H3a; zenon_intro zenon_H39 | zenon_intro zenon_H34; zenon_intro zenon_H38 ]. % 261.86/262.06 exact (zenon_H3a zenon_H34). % 261.86/262.06 apply (zenon_and_s _ _ zenon_H38). zenon_intro zenon_H3c. zenon_intro zenon_H3b. % 261.86/262.06 exact (zenon_H3c zenon_H33). % 261.86/262.06 (* end of lemma zenon_L1_ *) % 261.86/262.06 assert (zenon_L2_ : (forall W1 : zenon_U, (((aNaturalNumber0 (xp))/\(aNaturalNumber0 W1))->(((~((xp) = (sz00)))/\(doDivides0 (xp) W1))->(forall W2 : zenon_U, ((W2 = (sdtsldt0 W1 (xp)))<->((aNaturalNumber0 W2)/\(W1 = (sdtasdt0 (xp) W2)))))))) -> (aNaturalNumber0 (xp)) -> (aNaturalNumber0 (xm)) -> (aNaturalNumber0 (xn)) -> (isPrime0 (xp)) -> (doDivides0 (xp) (sdtasdt0 (xn) (xm))) -> (~(aNaturalNumber0 (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)))) -> False). % 261.86/262.06 do 0 intro. intros zenon_H3d zenon_H32 zenon_H3e zenon_H3f zenon_H34 zenon_H40 zenon_H41. % 261.86/262.06 generalize (zenon_H3d (sdtasdt0 (xn) (xm))). zenon_intro zenon_H42. % 261.86/262.06 apply (zenon_imply_s _ _ zenon_H42); [ zenon_intro zenon_H44 | zenon_intro zenon_H43 ]. % 261.86/262.06 apply (zenon_notand_s _ _ zenon_H44); [ zenon_intro zenon_H37 | zenon_intro zenon_H45 ]. % 261.86/262.06 exact (zenon_H37 zenon_H32). % 261.86/262.06 generalize (mSortsB_02 (xn)). zenon_intro zenon_H46. % 261.86/262.06 generalize (zenon_H46 (xm)). zenon_intro zenon_H47. % 261.86/262.06 apply (zenon_imply_s _ _ zenon_H47); [ zenon_intro zenon_H49 | zenon_intro zenon_H48 ]. % 261.86/262.06 apply (zenon_notand_s _ _ zenon_H49); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 261.86/262.06 exact (zenon_H4b zenon_H3f). % 261.86/262.06 exact (zenon_H4a zenon_H3e). % 261.86/262.06 exact (zenon_H45 zenon_H48). % 261.86/262.06 apply (zenon_imply_s _ _ zenon_H43); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 261.86/262.06 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 261.86/262.06 apply zenon_H4f. zenon_intro zenon_H33. % 261.86/262.06 apply (zenon_L1_); trivial. % 261.86/262.06 exact (zenon_H4e zenon_H40). % 261.86/262.06 generalize (zenon_H4c (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp))). zenon_intro zenon_H50. % 261.86/262.06 apply (zenon_equiv_s _ _ zenon_H50); [ zenon_intro zenon_H54; zenon_intro zenon_H53 | zenon_intro zenon_H52; zenon_intro zenon_H51 ]. % 261.86/262.06 apply zenon_H54. apply refl_equal. % 261.86/262.06 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H56. zenon_intro zenon_H55. % 261.86/262.06 exact (zenon_H41 zenon_H56). % 261.86/262.06 (* end of lemma zenon_L2_ *) % 261.86/262.06 assert (zenon_L3_ : (~(aNaturalNumber0 (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)))) -> (doDivides0 (xp) (sdtasdt0 (xn) (xm))) -> (isPrime0 (xp)) -> (aNaturalNumber0 (xn)) -> (aNaturalNumber0 (xm)) -> (aNaturalNumber0 (xp)) -> False). % 261.86/262.06 do 0 intro. intros zenon_H41 zenon_H40 zenon_H34 zenon_H3f zenon_H3e zenon_H32. % 261.86/262.06 generalize (mDefQuot (xp)). zenon_intro zenon_H3d. % 261.86/262.06 apply (zenon_L2_); trivial. % 261.86/262.06 (* end of lemma zenon_L3_ *) % 261.86/262.06 assert (zenon_L4_ : (~((sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) = (xk))) -> False). % 261.86/262.06 do 0 intro. intros zenon_H57. % 261.86/262.06 apply (zenon_congruence_lr_s _ (fun zenon_Vi : _ => (~((sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) = zenon_Vi))) _ _ zenon_H57 m__2306). zenon_intro zenon_H54. % 261.86/262.06 apply zenon_H54. apply refl_equal. % 261.86/262.06 (* end of lemma zenon_L4_ *) % 261.86/262.06 assert (zenon_L5_ : ((~((sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) = (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp))))/\(sdtlseqdt0 (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)))) -> False). % 261.86/262.06 do 0 intro. intros zenon_H58. % 261.86/262.06 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H54. zenon_intro zenon_H59. % 261.86/262.06 apply zenon_H54. apply refl_equal. % 261.86/262.06 (* end of lemma zenon_L5_ *) % 261.86/262.06 assert (zenon_L6_ : (~((xp) = (xp))) -> False). % 261.86/262.06 do 0 intro. intros zenon_H5a. % 261.86/262.06 apply zenon_H5a. apply refl_equal. % 261.86/262.06 (* end of lemma zenon_L6_ *) % 261.86/262.06 apply NNPP. intro zenon_G. % 261.86/262.06 apply (zenon_and_s _ _ m__1837). zenon_intro zenon_H3f. zenon_intro zenon_H5b. % 261.86/262.06 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H3e. zenon_intro zenon_H32. % 261.86/262.06 apply (zenon_and_s _ _ m__1860). zenon_intro zenon_H34. zenon_intro zenon_H40. % 261.94/262.10 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 261.94/262.10 apply (zenon_notand_s _ _ zenon_H5c); [ zenon_intro zenon_H5f | zenon_intro zenon_H5e ]. % 261.94/262.10 apply zenon_H5f. zenon_intro zenon_H60. % 261.94/262.10 apply (zenon_congruence_lr_s _ (fun zenon_Vg : _ => (zenon_Vg = (xp))) _ _ zenon_H60 m__2306). zenon_intro zenon_H61. % 261.94/262.10 generalize (mLETotal (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp))). zenon_intro zenon_H62. % 261.94/262.10 generalize (zenon_H62 (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp))). zenon_intro zenon_H63. % 261.94/262.10 apply (zenon_imply_s _ _ zenon_H63); [ zenon_intro zenon_H65 | zenon_intro zenon_H64 ]. % 261.94/262.10 apply (zenon_notand_s _ _ zenon_H65); [ zenon_intro zenon_H41 | zenon_intro zenon_H41 ]. % 261.94/262.10 apply (zenon_L3_); trivial. % 261.94/262.10 apply (zenon_L3_); trivial. % 261.94/262.10 apply (zenon_or_s _ _ zenon_H64); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 261.94/262.10 cut ((sdtlseqdt0 (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp))) = (sdtlseqdt0 (xp) (xk))). % 261.94/262.10 intro zenon_D_pnotp. % 261.94/262.10 apply zenon_H5d. % 261.94/262.10 rewrite <- zenon_D_pnotp. % 261.94/262.10 exact zenon_H59. % 261.94/262.10 cut (((sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) = (xk))); [idtac | apply NNPP; zenon_intro zenon_H57]. % 261.94/262.10 cut (((sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) = (xp))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 261.94/262.10 congruence. % 261.94/262.10 exact (zenon_H66 zenon_H61). % 261.94/262.10 apply (zenon_L4_); trivial. % 261.94/262.10 apply (zenon_L5_); trivial. % 261.94/262.10 generalize (mLETotal (xp)). zenon_intro zenon_H67. % 261.94/262.10 generalize (zenon_H67 (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp))). zenon_intro zenon_H68. % 261.94/262.10 apply (zenon_imply_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 261.94/262.10 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H37 | zenon_intro zenon_H41 ]. % 261.94/262.10 exact (zenon_H37 zenon_H32). % 261.94/262.10 apply (zenon_L3_); trivial. % 261.94/262.10 apply (zenon_or_s _ _ zenon_H69); [ zenon_intro zenon_H6c | zenon_intro zenon_H6b ]. % 261.94/262.10 cut ((sdtlseqdt0 (xp) (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp))) = (sdtlseqdt0 (xp) (xk))). % 261.94/262.10 intro zenon_D_pnotp. % 261.94/262.10 apply zenon_H5d. % 261.94/262.10 rewrite <- zenon_D_pnotp. % 261.94/262.10 exact zenon_H6c. % 261.94/262.10 cut (((sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) = (xk))); [idtac | apply NNPP; zenon_intro zenon_H57]. % 261.94/262.10 cut (((xp) = (xp))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 261.94/262.10 congruence. % 261.94/262.10 apply zenon_H5a. apply refl_equal. % 261.94/262.10 apply (zenon_L4_); trivial. % 261.94/262.10 apply (zenon_and_s _ _ zenon_H6b). zenon_intro zenon_H66. zenon_intro zenon_H6d. % 261.94/262.10 cut ((sdtlseqdt0 (sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) (xp)) = (sdtlseqdt0 (xk) (xp))). % 261.94/262.10 intro zenon_D_pnotp. % 261.94/262.10 apply zenon_H5e. % 261.94/262.10 rewrite <- zenon_D_pnotp. % 261.94/262.10 exact zenon_H6d. % 261.94/262.10 cut (((xp) = (xp))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 261.94/262.10 cut (((sdtsldt0 (sdtasdt0 (xn) (xm)) (xp)) = (xk))); [idtac | apply NNPP; zenon_intro zenon_H57]. % 261.94/262.10 congruence. % 261.94/262.10 apply (zenon_L4_); trivial. % 261.94/262.10 apply zenon_H5a. apply refl_equal. % 261.94/262.10 Qed. % 261.94/262.10 % SZS output end Proof % 261.94/262.10 (* END-PROOF *) % 261.94/262.10 nodes searched: 1507066 % 261.94/262.10 max branch formulas: 41974 % 261.94/262.10 proof nodes created: 52223 % 261.94/262.10 formulas created: 7215103 % 261.94/262.10 %------------------------------------------------------------------------------