%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM423+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n028.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:55:31 EDT 2022 % Result : Theorem 95.08s 95.30s % Output : Proof 95.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM423+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n028.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 : Tue Jul 5 12:01:36 EDT 2022 % 0.12/0.34 % CPUTime : % 95.08/95.30 (* PROOF-FOUND *) % 95.08/95.30 % SZS status Theorem % 95.08/95.30 (* BEGIN-PROOF *) % 95.08/95.30 % SZS output start Proof % 95.08/95.30 Theorem m__ : (sdteqdtlpzmzozddtrp0 (xa) (xa) (xq)). % 95.08/95.30 Proof. % 95.08/95.30 assert (zenon_L1_ : (~(aInteger0 (sdtpldt0 (xa) (smndt0 (xa))))) -> (aInteger0 (xa)) -> False). % 95.08/95.30 do 0 intro. intros zenon_H15 zenon_H16. % 95.08/95.30 generalize (mIntPlus (xa)). zenon_intro zenon_H17. % 95.08/95.30 generalize (zenon_H17 (smndt0 (xa))). zenon_intro zenon_H18. % 95.08/95.30 apply (zenon_imply_s _ _ zenon_H18); [ zenon_intro zenon_H1a | zenon_intro zenon_H19 ]. % 95.08/95.30 apply (zenon_notand_s _ _ zenon_H1a); [ zenon_intro zenon_H1c | zenon_intro zenon_H1b ]. % 95.08/95.30 exact (zenon_H1c zenon_H16). % 95.08/95.30 generalize (mIntNeg (xa)). zenon_intro zenon_H1d. % 95.08/95.30 apply (zenon_imply_s _ _ zenon_H1d); [ zenon_intro zenon_H1c | zenon_intro zenon_H1e ]. % 95.08/95.30 exact (zenon_H1c zenon_H16). % 95.08/95.30 exact (zenon_H1b zenon_H1e). % 95.08/95.30 exact (zenon_H15 zenon_H19). % 95.08/95.30 (* end of lemma zenon_L1_ *) % 95.08/95.30 assert (zenon_L2_ : (~((aInteger0 (sz00))/\((sdtasdt0 (xq) (sz00)) = (sdtpldt0 (xa) (smndt0 (xa)))))) -> ((sdtpldt0 (xa) (smndt0 (xa))) = (sz00)) -> (aInteger0 (xq)) -> False). % 95.08/95.30 do 0 intro. intros zenon_H1f zenon_H20 zenon_H21. % 95.08/95.30 apply (zenon_notand_s _ _ zenon_H1f); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 95.08/95.30 exact (zenon_H23 mIntZero). % 95.08/95.30 generalize (mMulZero (xq)). zenon_intro zenon_H24. % 95.08/95.30 apply (zenon_imply_s _ _ zenon_H24); [ zenon_intro zenon_H26 | zenon_intro zenon_H25 ]. % 95.08/95.30 exact (zenon_H26 zenon_H21). % 95.08/95.30 apply (zenon_and_s _ _ zenon_H25). zenon_intro zenon_H28. zenon_intro zenon_H27. % 95.08/95.30 elim (classic ((sdtpldt0 (xa) (smndt0 (xa))) = (sdtpldt0 (xa) (smndt0 (xa))))); [ zenon_intro zenon_H29 | zenon_intro zenon_H2a ]. % 95.08/95.30 cut (((sdtpldt0 (xa) (smndt0 (xa))) = (sdtpldt0 (xa) (smndt0 (xa)))) = ((sdtasdt0 (xq) (sz00)) = (sdtpldt0 (xa) (smndt0 (xa))))). % 95.08/95.30 intro zenon_D_pnotp. % 95.08/95.30 apply zenon_H22. % 95.08/95.30 rewrite <- zenon_D_pnotp. % 95.08/95.30 exact zenon_H29. % 95.08/95.30 cut (((sdtpldt0 (xa) (smndt0 (xa))) = (sdtpldt0 (xa) (smndt0 (xa))))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 95.08/95.30 cut (((sdtpldt0 (xa) (smndt0 (xa))) = (sdtasdt0 (xq) (sz00)))); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 95.08/95.30 congruence. % 95.08/95.30 cut (((sdtpldt0 (xa) (smndt0 (xa))) = (sz00)) = ((sdtpldt0 (xa) (smndt0 (xa))) = (sdtasdt0 (xq) (sz00)))). % 95.08/95.30 intro zenon_D_pnotp. % 95.08/95.30 apply zenon_H2b. % 95.08/95.30 rewrite <- zenon_D_pnotp. % 95.08/95.30 exact zenon_H20. % 95.08/95.30 cut (((sz00) = (sdtasdt0 (xq) (sz00)))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 95.08/95.30 cut (((sdtpldt0 (xa) (smndt0 (xa))) = (sdtpldt0 (xa) (smndt0 (xa))))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 95.08/95.30 congruence. % 95.08/95.30 apply zenon_H2a. apply refl_equal. % 95.08/95.30 apply zenon_H2c. apply sym_equal. exact zenon_H28. % 95.08/95.30 apply zenon_H2a. apply refl_equal. % 95.08/95.30 apply zenon_H2a. apply refl_equal. % 95.08/95.30 (* end of lemma zenon_L2_ *) % 95.08/95.30 assert (zenon_L3_ : (~(exists W2 : zenon_U, ((aInteger0 W2)/\((sdtasdt0 (xq) W2) = (sdtpldt0 (xa) (smndt0 (xa))))))) -> (aInteger0 (xq)) -> ((sdtpldt0 (xa) (smndt0 (xa))) = (sz00)) -> False). % 95.08/95.30 do 0 intro. intros zenon_H2d zenon_H21 zenon_H20. % 95.08/95.30 apply zenon_H2d. exists (sz00). apply NNPP. zenon_intro zenon_H1f. % 95.08/95.30 apply (zenon_L2_); trivial. % 95.08/95.30 (* end of lemma zenon_L3_ *) % 95.08/95.30 apply NNPP. intro zenon_G. % 95.08/95.30 apply (zenon_and_s _ _ m__671). zenon_intro zenon_H16. zenon_intro zenon_H2e. % 95.08/95.30 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H21. zenon_intro zenon_H2f. % 95.08/95.30 generalize (mEquMod (xa)). zenon_intro zenon_H30. % 95.08/95.30 generalize (zenon_H30 (xa)). zenon_intro zenon_H31. % 95.08/95.30 generalize (zenon_H31 (xq)). zenon_intro zenon_H32. % 95.08/95.30 apply (zenon_imply_s _ _ zenon_H32); [ zenon_intro zenon_H34 | zenon_intro zenon_H33 ]. % 95.08/95.30 apply (zenon_notand_s _ _ zenon_H34); [ zenon_intro zenon_H1c | zenon_intro zenon_H35 ]. % 95.08/95.30 exact (zenon_H1c zenon_H16). % 95.08/95.30 apply (zenon_notand_s _ _ zenon_H35); [ zenon_intro zenon_H1c | zenon_intro zenon_H36 ]. % 95.08/95.30 exact (zenon_H1c zenon_H16). % 95.08/95.30 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H26 | zenon_intro zenon_H37 ]. % 95.08/95.30 exact (zenon_H26 zenon_H21). % 95.08/95.30 exact (zenon_H37 zenon_H2f). % 95.08/95.30 apply (zenon_equiv_s _ _ zenon_H33); [ zenon_intro zenon_G; zenon_intro zenon_H3a | zenon_intro zenon_H39; zenon_intro zenon_H38 ]. % 95.08/95.30 generalize (mDivisor (sdtpldt0 (xa) (smndt0 (xa)))). zenon_intro zenon_H3b. % 95.08/95.30 apply (zenon_imply_s _ _ zenon_H3b); [ zenon_intro zenon_H15 | zenon_intro zenon_H3c ]. % 95.08/95.30 apply (zenon_L1_); trivial. % 95.12/95.33 generalize (zenon_H3c (xq)). zenon_intro zenon_H3d. % 95.12/95.33 apply (zenon_equiv_s _ _ zenon_H3d); [ zenon_intro zenon_H3a; zenon_intro zenon_H3f | zenon_intro zenon_H38; zenon_intro zenon_H3e ]. % 95.12/95.33 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H26 | zenon_intro zenon_H40 ]. % 95.12/95.33 exact (zenon_H26 zenon_H21). % 95.12/95.33 apply (zenon_notand_s _ _ zenon_H40); [ zenon_intro zenon_H37 | zenon_intro zenon_H2d ]. % 95.12/95.33 exact (zenon_H37 zenon_H2f). % 95.12/95.33 generalize (mAddNeg (xa)). zenon_intro zenon_H41. % 95.12/95.33 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H1c | zenon_intro zenon_H42 ]. % 95.12/95.33 exact (zenon_H1c zenon_H16). % 95.12/95.33 apply (zenon_and_s _ _ zenon_H42). zenon_intro zenon_H20. zenon_intro zenon_H43. % 95.12/95.33 apply (zenon_L3_); trivial. % 95.12/95.33 exact (zenon_H3a zenon_H38). % 95.12/95.33 exact (zenon_G zenon_H39). % 95.12/95.33 Qed. % 95.12/95.33 % SZS output end Proof % 95.12/95.33 (* END-PROOF *) % 95.12/95.33 nodes searched: 391453 % 95.12/95.33 max branch formulas: 15857 % 95.12/95.33 proof nodes created: 6612 % 95.12/95.33 formulas created: 2384374 % 95.12/95.33 %------------------------------------------------------------------------------