%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG092+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n022.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:26 EDT 2022 % Result : Theorem 0.43s 0.60s % Output : Proof 0.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG092+2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n022.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 : Mon May 30 20:16:37 EDT 2022 % 0.12/0.33 % CPUTime : % 0.43/0.60 (* PROOF-FOUND *) % 0.43/0.60 % SZS status Theorem % 0.43/0.60 (* BEGIN-PROOF *) % 0.43/0.60 % SZS output start Proof % 0.43/0.60 Theorem m__ : ((forall W0 : zenon_U, (forall W1 : zenon_U, (forall W2 : zenon_U, ((((exists W3 : zenon_U, (exists W4 : zenon_U, ((aElementOf0 W3 (xI))/\((aElementOf0 W4 (xJ))/\((sdtpldt0 W3 W4) = W0)))))\/(aElementOf0 W0 (sdtpldt1 (xI) (xJ))))/\(((exists W3 : zenon_U, (exists W4 : zenon_U, ((aElementOf0 W3 (xI))/\((aElementOf0 W4 (xJ))/\((sdtpldt0 W3 W4) = W1)))))\/(aElementOf0 W1 (sdtpldt1 (xI) (xJ))))/\(aElement0 W2)))->(exists W3 : zenon_U, (exists W4 : zenon_U, ((aElementOf0 W3 (xI))/\((aElementOf0 W4 (xJ))/\((W0 = (sdtpldt0 W3 W4))/\(exists W5 : zenon_U, (exists W6 : zenon_U, ((aElementOf0 W5 (xI))/\((aElementOf0 W6 (xJ))/\((W1 = (sdtpldt0 W5 W6))/\((aElementOf0 (sdtpldt0 W3 W5) (xI))/\((aElementOf0 (sdtpldt0 W4 W6) (xJ))/\((aElementOf0 (sdtasdt0 W2 W3) (xI))/\((aElementOf0 (sdtasdt0 W2 W4) (xJ))/\(((sdtpldt0 W0 W1) = (sdtpldt0 (sdtpldt0 W3 W5) (sdtpldt0 W4 W6)))/\((exists W7 : zenon_U, (exists W8 : zenon_U, ((aElementOf0 W7 (xI))/\((aElementOf0 W8 (xJ))/\((sdtpldt0 W7 W8) = (sdtpldt0 W0 W1))))))/\((aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ)))/\((exists W7 : zenon_U, (exists W8 : zenon_U, ((aElementOf0 W7 (xI))/\((aElementOf0 W8 (xJ))/\((sdtpldt0 W7 W8) = (sdtasdt0 W2 W0))))))/\(aElementOf0 (sdtasdt0 W2 W0) (sdtpldt1 (xI) (xJ)))))))))))))))))))))))))->(((aSet0 (sdtpldt1 (xI) (xJ)))/\(forall W0 : zenon_U, ((aElementOf0 W0 (sdtpldt1 (xI) (xJ)))<->(exists W3 : zenon_U, (exists W4 : zenon_U, ((aElementOf0 W3 (xI))/\((aElementOf0 W4 (xJ))/\((sdtpldt0 W3 W4) = W0))))))))->((forall W0 : zenon_U, ((aElementOf0 W0 (sdtpldt1 (xI) (xJ)))->((forall W1 : zenon_U, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ)))->(aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ)))))/\(forall W1 : zenon_U, ((aElement0 W1)->(aElementOf0 (sdtasdt0 W1 W0) (sdtpldt1 (xI) (xJ))))))))\/(aIdeal0 (sdtpldt1 (xI) (xJ)))))). % 0.43/0.60 Proof. % 0.43/0.60 assert (zenon_L1_ : forall (zenon_TW0_bc : zenon_U), (~((exists W3 : zenon_U, (exists W4 : zenon_U, ((aElementOf0 W3 (xI))/\((aElementOf0 W4 (xJ))/\((sdtpldt0 W3 W4) = zenon_TW0_bc)))))\/(aElementOf0 zenon_TW0_bc (sdtpldt1 (xI) (xJ))))) -> (aElementOf0 zenon_TW0_bc (sdtpldt1 (xI) (xJ))) -> False). % 0.43/0.60 do 1 intro. intros zenon_H1a zenon_H1b. % 0.43/0.60 apply (zenon_notor_s _ _ zenon_H1a). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 0.43/0.60 exact (zenon_H1d zenon_H1b). % 0.43/0.60 (* end of lemma zenon_L1_ *) % 0.43/0.60 apply NNPP. intro zenon_G. % 0.43/0.60 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H20. zenon_intro zenon_H1f. % 0.43/0.60 apply (zenon_notimply_s _ _ zenon_H1f). zenon_intro zenon_H22. zenon_intro zenon_H21. % 0.43/0.60 apply (zenon_notor_s _ _ zenon_H21). zenon_intro zenon_H24. zenon_intro zenon_H23. % 0.43/0.60 apply (zenon_notallex_s (fun W0 : zenon_U => ((aElementOf0 W0 (sdtpldt1 (xI) (xJ)))->((forall W1 : zenon_U, ((aElementOf0 W1 (sdtpldt1 (xI) (xJ)))->(aElementOf0 (sdtpldt0 W0 W1) (sdtpldt1 (xI) (xJ)))))/\(forall W1 : zenon_U, ((aElement0 W1)->(aElementOf0 (sdtasdt0 W1 W0) (sdtpldt1 (xI) (xJ)))))))) zenon_H24); [ zenon_intro zenon_H25; idtac ]. % 0.43/0.60 elim zenon_H25. zenon_intro zenon_TW0_bc. zenon_intro zenon_H26. % 0.43/0.60 apply (zenon_notimply_s _ _ zenon_H26). zenon_intro zenon_H1b. zenon_intro zenon_H27. % 0.43/0.60 apply (zenon_notand_s _ _ zenon_H27); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 0.43/0.60 apply (zenon_notallex_s (fun W1 : zenon_U => ((aElementOf0 W1 (sdtpldt1 (xI) (xJ)))->(aElementOf0 (sdtpldt0 zenon_TW0_bc W1) (sdtpldt1 (xI) (xJ))))) zenon_H29); [ zenon_intro zenon_H2a; idtac ]. % 0.43/0.60 elim zenon_H2a. zenon_intro zenon_TW1_br. zenon_intro zenon_H2c. % 0.43/0.60 apply (zenon_notimply_s _ _ zenon_H2c). zenon_intro zenon_H2e. zenon_intro zenon_H2d. % 0.43/0.60 generalize (zenon_H20 zenon_TW0_bc). zenon_intro zenon_H2f. % 0.43/0.60 generalize (zenon_H2f zenon_TW1_br). zenon_intro zenon_H30. % 0.43/0.60 generalize (zenon_H30 (sz10)). zenon_intro zenon_H31. % 0.43/0.60 apply (zenon_imply_s _ _ zenon_H31); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 0.43/0.60 apply (zenon_notand_s _ _ zenon_H33); [ zenon_intro zenon_H1a | zenon_intro zenon_H34 ]. % 0.43/0.60 apply (zenon_L1_ zenon_TW0_bc); trivial. % 0.43/0.60 apply (zenon_notand_s _ _ zenon_H34); [ zenon_intro zenon_H36 | zenon_intro zenon_H35 ]. % 0.43/0.60 apply (zenon_notor_s _ _ zenon_H36). zenon_intro zenon_H38. zenon_intro zenon_H37. % 0.43/0.60 exact (zenon_H37 zenon_H2e). % 0.43/0.60 exact (zenon_H35 mSortsC_01). % 0.43/0.60 elim zenon_H32. zenon_intro zenon_TW3_cf. zenon_intro zenon_H3a. % 0.43/0.60 elim zenon_H3a. zenon_intro zenon_TW4_ch. zenon_intro zenon_H3c. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H3d). zenon_intro zenon_H40. zenon_intro zenon_H3f. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H3f). zenon_intro zenon_H42. zenon_intro zenon_H41. % 0.43/0.60 elim zenon_H41. zenon_intro zenon_TW5_cp. zenon_intro zenon_H44. % 0.43/0.60 elim zenon_H44. zenon_intro zenon_TW6_cr. zenon_intro zenon_H46. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H46). zenon_intro zenon_H48. zenon_intro zenon_H47. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H47). zenon_intro zenon_H4a. zenon_intro zenon_H49. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H49). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H4b). zenon_intro zenon_H4e. zenon_intro zenon_H4d. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H52. zenon_intro zenon_H51. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H54. zenon_intro zenon_H53. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H53). zenon_intro zenon_H56. zenon_intro zenon_H55. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H58. zenon_intro zenon_H57. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H57). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 0.43/0.60 exact (zenon_H2d zenon_H5a). % 0.43/0.60 apply (zenon_notallex_s (fun W1 : zenon_U => ((aElement0 W1)->(aElementOf0 (sdtasdt0 W1 zenon_TW0_bc) (sdtpldt1 (xI) (xJ))))) zenon_H28); [ zenon_intro zenon_H5b; idtac ]. % 0.43/0.60 elim zenon_H5b. zenon_intro zenon_TW1_do. zenon_intro zenon_H5d. % 0.43/0.60 apply (zenon_notimply_s _ _ zenon_H5d). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 0.43/0.60 generalize (zenon_H20 zenon_TW0_bc). zenon_intro zenon_H2f. % 0.43/0.60 generalize (zenon_H2f zenon_TW0_bc). zenon_intro zenon_H60. % 0.43/0.60 generalize (zenon_H60 zenon_TW1_do). zenon_intro zenon_H61. % 0.43/0.60 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 0.43/0.60 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H1a | zenon_intro zenon_H64 ]. % 0.43/0.60 apply (zenon_L1_ zenon_TW0_bc); trivial. % 0.43/0.60 apply (zenon_notand_s _ _ zenon_H64); [ zenon_intro zenon_H1a | zenon_intro zenon_H65 ]. % 0.43/0.60 apply (zenon_L1_ zenon_TW0_bc); trivial. % 0.43/0.60 exact (zenon_H65 zenon_H5f). % 0.43/0.60 elim zenon_H62. zenon_intro zenon_TW3_dy. zenon_intro zenon_H67. % 0.43/0.60 elim zenon_H67. zenon_intro zenon_TW4_ea. zenon_intro zenon_H69. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H69). zenon_intro zenon_H6b. zenon_intro zenon_H6a. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H6a). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H6f. zenon_intro zenon_H6e. % 0.43/0.60 elim zenon_H6e. zenon_intro zenon_TW5_ei. zenon_intro zenon_H71. % 0.43/0.60 elim zenon_H71. zenon_intro zenon_TW6_ek. zenon_intro zenon_H73. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H73). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H74). zenon_intro zenon_H77. zenon_intro zenon_H76. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H76). zenon_intro zenon_H79. zenon_intro zenon_H78. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H7a). zenon_intro zenon_H7d. zenon_intro zenon_H7c. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H7c). zenon_intro zenon_H7f. zenon_intro zenon_H7e. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H7e). zenon_intro zenon_H81. zenon_intro zenon_H80. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H82). zenon_intro zenon_H85. zenon_intro zenon_H84. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H84). zenon_intro zenon_H87. zenon_intro zenon_H86. % 0.43/0.60 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H89. zenon_intro zenon_H88. % 0.43/0.60 exact (zenon_H5e zenon_H88). % 0.43/0.60 Qed. % 0.43/0.60 % SZS output end Proof % 0.43/0.60 (* END-PROOF *) % 0.43/0.60 nodes searched: 1515 % 0.43/0.60 max branch formulas: 626 % 0.43/0.60 proof nodes created: 94 % 0.43/0.60 formulas created: 16235 % 0.43/0.60 %------------------------------------------------------------------------------