%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM450+6 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.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:47 EDT 2022 % Result : Theorem 1.23s 1.46s % Output : Proof 1.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : NUM450+6 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jul 6 19:53:23 EDT 2022 % 0.13/0.34 % CPUTime : % 1.23/1.46 (* PROOF-FOUND *) % 1.23/1.46 % SZS status Theorem % 1.23/1.46 (* BEGIN-PROOF *) % 1.23/1.46 % SZS output start Proof % 1.23/1.46 Theorem m__ : (exists W0 : zenon_U, ((aInteger0 W0)/\((~(W0 = (sz00)))/\(((aSet0 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0))/\(forall W1 : zenon_U, (((aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0))->((aInteger0 W1)/\((exists W2 : zenon_U, ((aInteger0 W2)/\((sdtasdt0 W0 W2) = (sdtpldt0 W1 (smndt0 (sz10))))))/\((aDivisorOf0 W0 (sdtpldt0 W1 (smndt0 (sz10))))/\(sdteqdtlpzmzozddtrp0 W1 (sz10) W0)))))/\(((aInteger0 W1)/\((exists W2 : zenon_U, ((aInteger0 W2)/\((sdtasdt0 W0 W2) = (sdtpldt0 W1 (smndt0 (sz10))))))\/((aDivisorOf0 W0 (sdtpldt0 W1 (smndt0 (sz10))))\/(sdteqdtlpzmzozddtrp0 W1 (sz10) W0))))->(aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0))))))->(((aSet0 (sbsmnsldt0 (xS)))/\(forall W0 : zenon_U, ((aElementOf0 W0 (sbsmnsldt0 (xS)))<->((aInteger0 W0)/\(exists W1 : zenon_U, ((aElementOf0 W1 (xS))/\(aElementOf0 W0 W1)))))))->((forall W0 : zenon_U, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS))))<->((aInteger0 W0)/\(~(aElementOf0 W0 (sbsmnsldt0 (xS)))))))->((forall W1 : zenon_U, ((aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0))->(aElementOf0 W1 (stldt0 (sbsmnsldt0 (xS))))))\/(aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0) (stldt0 (sbsmnsldt0 (xS))))))))))). % 1.23/1.46 Proof. % 1.23/1.46 assert (zenon_L1_ : (~((sz10) = (sz10))) -> False). % 1.23/1.46 do 0 intro. intros zenon_H2e. % 1.23/1.46 apply zenon_H2e. apply refl_equal. % 1.23/1.46 (* end of lemma zenon_L1_ *) % 1.23/1.46 assert (zenon_L2_ : (exists W1 : zenon_U, ((aInteger0 W1)/\((~(W1 = (sz00)))/\((aSet0 (szAzrzSzezqlpdtcmdtrp0 (sz10) W1))/\((forall W2 : zenon_U, (((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (sz10) W1))->((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 (sz10))))))/\((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 (sz10))))/\(sdteqdtlpzmzozddtrp0 W2 (sz10) W1)))))/\(((aInteger0 W2)/\((exists W3 : zenon_U, ((aInteger0 W3)/\((sdtasdt0 W1 W3) = (sdtpldt0 W2 (smndt0 (sz10))))))\/((aDivisorOf0 W1 (sdtpldt0 W2 (smndt0 (sz10))))\/(sdteqdtlpzmzozddtrp0 W2 (sz10) W1))))->(aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (sz10) W1)))))/\((forall W2 : zenon_U, ((aElementOf0 W2 (szAzrzSzezqlpdtcmdtrp0 (sz10) W1))->(aElementOf0 W2 (stldt0 (sbsmnsldt0 (xS))))))/\(aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 (sz10) W1) (stldt0 (sbsmnsldt0 (xS)))))))))) -> (~(exists W0 : zenon_U, ((aInteger0 W0)/\((~(W0 = (sz00)))/\(((aSet0 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0))/\(forall W1 : zenon_U, (((aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0))->((aInteger0 W1)/\((exists W2 : zenon_U, ((aInteger0 W2)/\((sdtasdt0 W0 W2) = (sdtpldt0 W1 (smndt0 (sz10))))))/\((aDivisorOf0 W0 (sdtpldt0 W1 (smndt0 (sz10))))/\(sdteqdtlpzmzozddtrp0 W1 (sz10) W0)))))/\(((aInteger0 W1)/\((exists W2 : zenon_U, ((aInteger0 W2)/\((sdtasdt0 W0 W2) = (sdtpldt0 W1 (smndt0 (sz10))))))\/((aDivisorOf0 W0 (sdtpldt0 W1 (smndt0 (sz10))))\/(sdteqdtlpzmzozddtrp0 W1 (sz10) W0))))->(aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0))))))->(((aSet0 (sbsmnsldt0 (xS)))/\(forall W0 : zenon_U, ((aElementOf0 W0 (sbsmnsldt0 (xS)))<->((aInteger0 W0)/\(exists W1 : zenon_U, ((aElementOf0 W1 (xS))/\(aElementOf0 W0 W1)))))))->((forall W0 : zenon_U, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS))))<->((aInteger0 W0)/\(~(aElementOf0 W0 (sbsmnsldt0 (xS)))))))->((forall W1 : zenon_U, ((aElementOf0 W1 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0))->(aElementOf0 W1 (stldt0 (sbsmnsldt0 (xS))))))\/(aSubsetOf0 (szAzrzSzezqlpdtcmdtrp0 (sz10) W0) (stldt0 (sbsmnsldt0 (xS)))))))))))) -> False). % 1.23/1.46 do 0 intro. intros zenon_H2f zenon_G. % 1.23/1.46 elim zenon_H2f. zenon_intro zenon_TW1_bw. zenon_intro zenon_H31. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H31). zenon_intro zenon_H33. zenon_intro zenon_H32. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H38). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 1.23/1.46 apply zenon_G. exists zenon_TW1_bw. apply NNPP. zenon_intro zenon_H3c. % 1.23/1.46 apply (zenon_notand_s _ _ zenon_H3c); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 1.23/1.46 exact (zenon_H3e zenon_H33). % 1.23/1.46 apply (zenon_notand_s _ _ zenon_H3d); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 1.23/1.46 exact (zenon_H40 zenon_H35). % 1.23/1.46 apply (zenon_notimply_s _ _ zenon_H3f). zenon_intro zenon_H42. zenon_intro zenon_H41. % 1.23/1.46 apply (zenon_notimply_s _ _ zenon_H41). zenon_intro zenon_H44. zenon_intro zenon_H43. % 1.23/1.46 apply (zenon_notimply_s _ _ zenon_H43). zenon_intro zenon_H46. zenon_intro zenon_H45. % 1.23/1.46 apply (zenon_notor_s _ _ zenon_H45). zenon_intro zenon_H48. zenon_intro zenon_H47. % 1.23/1.46 exact (zenon_H48 zenon_H3b). % 1.23/1.46 (* end of lemma zenon_L2_ *) % 1.23/1.46 apply NNPP. intro zenon_G. % 1.23/1.46 apply (zenon_and_s _ _ m__2079). zenon_intro zenon_H4a. zenon_intro zenon_H49. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H49). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H4b). zenon_intro zenon_H4e. zenon_intro zenon_H4d. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H46. zenon_intro zenon_H4f. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H51. zenon_intro zenon_H50. % 1.23/1.46 apply (zenon_and_s _ _ m__2144). zenon_intro zenon_H4a. zenon_intro zenon_H52. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H52). zenon_intro zenon_H4c. zenon_intro zenon_H53. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H53). zenon_intro zenon_H46. zenon_intro zenon_H54. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H54). zenon_intro zenon_H56. zenon_intro zenon_H55. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H58. zenon_intro zenon_H57. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H57). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H4a. zenon_intro zenon_H5b. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H4c. zenon_intro zenon_H5c. % 1.23/1.46 apply (zenon_and_s _ _ zenon_H5c). zenon_intro zenon_H46. zenon_intro zenon_H56. % 1.23/1.46 generalize (zenon_H56 (sz10)). zenon_intro zenon_H5d. % 1.23/1.46 apply (zenon_imply_s _ _ zenon_H5d); [ zenon_intro zenon_H5e | zenon_intro zenon_H2f ]. % 1.23/1.46 generalize (zenon_H51 (sz10)). zenon_intro zenon_H5f. % 1.23/1.46 apply (zenon_equiv_s _ _ zenon_H5f); [ zenon_intro zenon_H5e; zenon_intro zenon_H62 | zenon_intro zenon_H61; zenon_intro zenon_H60 ]. % 1.23/1.46 apply (zenon_notor_s _ _ zenon_H62). zenon_intro zenon_H2e. zenon_intro zenon_H63. % 1.23/1.46 apply zenon_H2e. apply refl_equal. % 1.23/1.46 exact (zenon_H5e zenon_H61). % 1.23/1.46 apply (zenon_L2_); trivial. % 1.23/1.46 Qed. % 1.23/1.46 % SZS output end Proof % 1.23/1.46 (* END-PROOF *) % 1.23/1.46 nodes searched: 29222 % 1.23/1.46 max branch formulas: 2238 % 1.23/1.46 proof nodes created: 709 % 1.23/1.46 formulas created: 103232 % 1.23/1.46 %------------------------------------------------------------------------------