%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG106+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n024.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:28 EDT 2022 % Result : Theorem 0.40s 0.59s % Output : Proof 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG106+2 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon May 30 07:33:21 EDT 2022 % 0.12/0.34 % CPUTime : % 0.40/0.59 (* PROOF-FOUND *) % 0.40/0.59 % SZS status Theorem % 0.40/0.59 (* BEGIN-PROOF *) % 0.40/0.59 % SZS output start Proof % 0.40/0.59 Theorem m__ : ((forall W0 : zenon_U, (forall W1 : zenon_U, (forall W2 : zenon_U, ((((exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xc) W3) = W0)))\/(aElementOf0 W0 (slsdtgt0 (xc))))/\(((exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xc) W3) = W1)))\/(aElementOf0 W1 (slsdtgt0 (xc))))/\(aElement0 W2)))->(exists W3 : zenon_U, ((aElement0 W3)/\(((sdtasdt0 (xc) W3) = W0)/\(exists W4 : zenon_U, ((aElement0 W4)/\(((sdtasdt0 (xc) W4) = W1)/\(((sdtpldt0 W0 W1) = (sdtasdt0 (xc) (sdtpldt0 W3 W4)))/\(((sdtasdt0 W2 W0) = (sdtasdt0 (xc) (sdtasdt0 W3 W2)))/\((exists W5 : zenon_U, ((aElement0 W5)/\((sdtasdt0 (xc) W5) = (sdtpldt0 W0 W1))))/\((aElementOf0 (sdtpldt0 W0 W1) (slsdtgt0 (xc)))/\((exists W5 : zenon_U, ((aElement0 W5)/\((sdtasdt0 (xc) W5) = (sdtasdt0 W2 W0))))/\(aElementOf0 (sdtasdt0 W2 W0) (slsdtgt0 (xc))))))))))))))))))->(((aSet0 (slsdtgt0 (xc)))/\(forall W0 : zenon_U, ((aElementOf0 W0 (slsdtgt0 (xc)))<->(exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xc) W3) = W0))))))->((forall W0 : zenon_U, ((aElementOf0 W0 (slsdtgt0 (xc)))->((forall W1 : zenon_U, ((aElementOf0 W1 (slsdtgt0 (xc)))->(aElementOf0 (sdtpldt0 W0 W1) (slsdtgt0 (xc)))))/\(forall W1 : zenon_U, ((aElement0 W1)->(aElementOf0 (sdtasdt0 W1 W0) (slsdtgt0 (xc))))))))\/(aIdeal0 (slsdtgt0 (xc)))))). % 0.40/0.59 Proof. % 0.40/0.59 assert (zenon_L1_ : forall (zenon_TW0_bp : zenon_U), (~((exists W3 : zenon_U, ((aElement0 W3)/\((sdtasdt0 (xc) W3) = zenon_TW0_bp)))\/(aElementOf0 zenon_TW0_bp (slsdtgt0 (xc))))) -> (aElementOf0 zenon_TW0_bp (slsdtgt0 (xc))) -> False). % 0.40/0.59 do 1 intro. intros zenon_H27 zenon_H28. % 0.40/0.59 apply (zenon_notor_s _ _ zenon_H27). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 0.40/0.59 exact (zenon_H2a zenon_H28). % 0.40/0.59 (* end of lemma zenon_L1_ *) % 0.40/0.59 apply NNPP. intro zenon_G. % 0.40/0.59 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 0.40/0.59 apply (zenon_notimply_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 0.40/0.59 apply (zenon_notor_s _ _ zenon_H2e). zenon_intro zenon_H31. zenon_intro zenon_H30. % 0.40/0.59 apply (zenon_notallex_s (fun W0 : zenon_U => ((aElementOf0 W0 (slsdtgt0 (xc)))->((forall W1 : zenon_U, ((aElementOf0 W1 (slsdtgt0 (xc)))->(aElementOf0 (sdtpldt0 W0 W1) (slsdtgt0 (xc)))))/\(forall W1 : zenon_U, ((aElement0 W1)->(aElementOf0 (sdtasdt0 W1 W0) (slsdtgt0 (xc)))))))) zenon_H31); [ zenon_intro zenon_H32; idtac ]. % 0.40/0.59 elim zenon_H32. zenon_intro zenon_TW0_bp. zenon_intro zenon_H33. % 0.40/0.59 apply (zenon_notimply_s _ _ zenon_H33). zenon_intro zenon_H28. zenon_intro zenon_H34. % 0.40/0.59 apply (zenon_notand_s _ _ zenon_H34); [ zenon_intro zenon_H36 | zenon_intro zenon_H35 ]. % 0.40/0.59 apply (zenon_notallex_s (fun W1 : zenon_U => ((aElementOf0 W1 (slsdtgt0 (xc)))->(aElementOf0 (sdtpldt0 zenon_TW0_bp W1) (slsdtgt0 (xc))))) zenon_H36); [ zenon_intro zenon_H37; idtac ]. % 0.40/0.59 elim zenon_H37. zenon_intro zenon_TW1_ce. zenon_intro zenon_H39. % 0.40/0.59 apply (zenon_notimply_s _ _ zenon_H39). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 0.40/0.59 generalize (zenon_H2d zenon_TW0_bp). zenon_intro zenon_H3c. % 0.40/0.59 generalize (zenon_H3c zenon_TW1_ce). zenon_intro zenon_H3d. % 0.40/0.59 generalize (zenon_H3d (xc)). zenon_intro zenon_H3e. % 0.40/0.59 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 0.40/0.59 apply (zenon_notand_s _ _ zenon_H40); [ zenon_intro zenon_H27 | zenon_intro zenon_H41 ]. % 0.40/0.59 apply (zenon_L1_ zenon_TW0_bp); trivial. % 0.40/0.59 apply (zenon_notand_s _ _ zenon_H41); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 0.40/0.59 apply (zenon_notor_s _ _ zenon_H43). zenon_intro zenon_H45. zenon_intro zenon_H44. % 0.40/0.59 exact (zenon_H44 zenon_H3b). % 0.40/0.59 exact (zenon_H42 m__1905). % 0.40/0.59 elim zenon_H3f. zenon_intro zenon_TW3_cs. zenon_intro zenon_H47. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H47). zenon_intro zenon_H49. zenon_intro zenon_H48. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.40/0.59 elim zenon_H4a. zenon_intro zenon_TW4_cy. zenon_intro zenon_H4d. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H4e). zenon_intro zenon_H51. zenon_intro zenon_H50. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H50). zenon_intro zenon_H53. zenon_intro zenon_H52. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H52). zenon_intro zenon_H55. zenon_intro zenon_H54. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H54). zenon_intro zenon_H57. zenon_intro zenon_H56. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.40/0.59 exact (zenon_H3a zenon_H59). % 0.40/0.59 apply (zenon_notallex_s (fun W1 : zenon_U => ((aElement0 W1)->(aElementOf0 (sdtasdt0 W1 zenon_TW0_bp) (slsdtgt0 (xc))))) zenon_H35); [ zenon_intro zenon_H5a; idtac ]. % 0.40/0.59 elim zenon_H5a. zenon_intro zenon_TW1_dn. zenon_intro zenon_H5c. % 0.40/0.59 apply (zenon_notimply_s _ _ zenon_H5c). zenon_intro zenon_H5e. zenon_intro zenon_H5d. % 0.40/0.59 generalize (zenon_H2d zenon_TW0_bp). zenon_intro zenon_H3c. % 0.40/0.59 generalize (zenon_H3c zenon_TW0_bp). zenon_intro zenon_H5f. % 0.40/0.59 generalize (zenon_H5f zenon_TW1_dn). zenon_intro zenon_H60. % 0.40/0.59 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H62 | zenon_intro zenon_H61 ]. % 0.40/0.59 apply (zenon_notand_s _ _ zenon_H62); [ zenon_intro zenon_H27 | zenon_intro zenon_H63 ]. % 0.40/0.59 apply (zenon_L1_ zenon_TW0_bp); trivial. % 0.40/0.59 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H27 | zenon_intro zenon_H64 ]. % 0.40/0.59 apply (zenon_L1_ zenon_TW0_bp); trivial. % 0.40/0.59 exact (zenon_H64 zenon_H5e). % 0.40/0.59 elim zenon_H61. zenon_intro zenon_TW3_dx. zenon_intro zenon_H66. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H66). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 0.40/0.59 elim zenon_H69. zenon_intro zenon_TW4_ed. zenon_intro zenon_H6c. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H6c). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H72. zenon_intro zenon_H71. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H71). zenon_intro zenon_H74. zenon_intro zenon_H73. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H73). zenon_intro zenon_H76. zenon_intro zenon_H75. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.40/0.59 apply (zenon_and_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 0.40/0.59 exact (zenon_H5d zenon_H79). % 0.40/0.59 Qed. % 0.40/0.59 % SZS output end Proof % 0.40/0.59 (* END-PROOF *) % 0.40/0.59 nodes searched: 1085 % 0.40/0.59 max branch formulas: 664 % 0.40/0.59 proof nodes created: 67 % 0.40/0.59 formulas created: 13777 % 0.40/0.59 %------------------------------------------------------------------------------