%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM436+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n023.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:39 EDT 2022 % Result : Theorem 2.22s 2.40s % Output : Proof 2.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : NUM436+3 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : run_zenon %s %d % 0.12/0.31 % Computer : n023.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.31 % CPULimit : 300 % 0.16/0.31 % WCLimit : 600 % 0.16/0.31 % DateTime : Tue Jul 5 09:26:57 EDT 2022 % 0.16/0.31 % CPUTime : % 2.22/2.40 (* PROOF-FOUND *) % 2.22/2.40 % SZS status Theorem % 2.22/2.40 (* BEGIN-PROOF *) % 2.22/2.40 % SZS output start Proof % 2.22/2.40 Theorem m__ : (((exists W0 : zenon_U, ((aInteger0 W0)/\((sdtasdt0 (xp) W0) = (sdtpldt0 (xa) (smndt0 (xb))))))\/((aDivisorOf0 (xp) (sdtpldt0 (xa) (smndt0 (xb))))\/(sdteqdtlpzmzozddtrp0 (xa) (xb) (xp))))/\((exists W0 : zenon_U, ((aInteger0 W0)/\((sdtasdt0 (xq) W0) = (sdtpldt0 (xa) (smndt0 (xb))))))\/((aDivisorOf0 (xq) (sdtpldt0 (xa) (smndt0 (xb))))\/(sdteqdtlpzmzozddtrp0 (xa) (xb) (xq))))). % 2.22/2.40 Proof. % 2.22/2.40 apply NNPP. intro zenon_G. % 2.22/2.40 apply (zenon_and_s _ _ m__979). zenon_intro zenon_H1c. zenon_intro zenon_H1b. % 2.22/2.40 apply (zenon_and_s _ _ zenon_H1b). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 2.22/2.40 apply (zenon_and_s _ _ zenon_H1d). zenon_intro zenon_H20. zenon_intro zenon_H1f. % 2.22/2.40 apply (zenon_and_s _ _ zenon_H1f). zenon_intro zenon_H22. zenon_intro zenon_H21. % 2.22/2.40 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H24. zenon_intro zenon_H23. % 2.22/2.40 apply (zenon_and_s _ _ m__1032). zenon_intro zenon_H26. zenon_intro zenon_H25. % 2.22/2.40 apply (zenon_and_s _ _ m__1071). zenon_intro zenon_H28. zenon_intro zenon_H27. % 2.22/2.40 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H2a | zenon_intro zenon_H29 ]. % 2.22/2.40 apply (zenon_notor_s _ _ zenon_H2a). zenon_intro zenon_H2c. zenon_intro zenon_H2b. % 2.22/2.40 apply zenon_H2c. exists (sdtasdt0 (xq) (xm)). apply NNPP. zenon_intro zenon_H2d. % 2.22/2.40 apply (zenon_notand_s _ _ zenon_H2d); [ zenon_intro zenon_H2f | zenon_intro zenon_H2e ]. % 2.22/2.40 generalize (mIntMult (xq)). zenon_intro zenon_H30. % 2.22/2.40 generalize (zenon_H30 (xm)). zenon_intro zenon_H31. % 2.22/2.40 apply (zenon_imply_s _ _ zenon_H31); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 2.22/2.40 apply (zenon_notand_s _ _ zenon_H33); [ zenon_intro zenon_H35 | zenon_intro zenon_H34 ]. % 2.22/2.40 exact (zenon_H35 zenon_H24). % 2.22/2.40 exact (zenon_H34 zenon_H26). % 2.22/2.40 exact (zenon_H2f zenon_H32). % 2.22/2.40 exact (zenon_H2e zenon_H28). % 2.22/2.40 apply (zenon_notor_s _ _ zenon_H29). zenon_intro zenon_H37. zenon_intro zenon_H36. % 2.22/2.40 apply zenon_H37. exists (sdtasdt0 (xp) (xm)). apply NNPP. zenon_intro zenon_H38. % 2.22/2.40 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H3a | zenon_intro zenon_H39 ]. % 2.22/2.40 generalize (mIntMult (xp)). zenon_intro zenon_H3b. % 2.22/2.40 generalize (zenon_H3b (xm)). zenon_intro zenon_H3c. % 2.22/2.40 apply (zenon_imply_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 2.22/2.40 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H3f | zenon_intro zenon_H34 ]. % 2.22/2.40 exact (zenon_H3f zenon_H20). % 2.22/2.40 exact (zenon_H34 zenon_H26). % 2.22/2.40 exact (zenon_H3a zenon_H3d). % 2.22/2.40 apply zenon_H39. apply sym_equal. exact zenon_H27. % 2.22/2.40 Qed. % 2.22/2.40 % SZS output end Proof % 2.22/2.40 (* END-PROOF *) % 2.22/2.40 nodes searched: 20082 % 2.22/2.40 max branch formulas: 3775 % 2.22/2.40 proof nodes created: 956 % 2.22/2.40 formulas created: 136854 % 2.22/2.40 %------------------------------------------------------------------------------