%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG109+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n017.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:29 EDT 2022 % Result : Theorem 20.39s 20.59s % Output : Proof 20.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG109+4 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n017.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 16:44:25 EDT 2022 % 0.12/0.33 % CPUTime : % 20.39/20.59 (* PROOF-FOUND *) % 20.39/20.59 % SZS status Theorem % 20.39/20.59 (* BEGIN-PROOF *) % 20.39/20.59 % SZS output start Proof % 20.39/20.59 Theorem m__ : (exists W0 : zenon_U, (((forall W0 : zenon_U, ((aElementOf0 W0 (slsdtgt0 (xa)))<->(exists W1 : zenon_U, ((aElement0 W1)/\((sdtasdt0 (xa) W1) = W0)))))->((forall W0 : zenon_U, ((aElementOf0 W0 (slsdtgt0 (xb)))<->(exists W1 : zenon_U, ((aElement0 W1)/\((sdtasdt0 (xb) W1) = W0)))))->((exists W1 : zenon_U, (exists W2 : zenon_U, ((aElementOf0 W1 (slsdtgt0 (xa)))/\((aElementOf0 W2 (slsdtgt0 (xb)))/\((sdtpldt0 W1 W2) = W0)))))\/(aElementOf0 W0 (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))/\(~(W0 = (sz00))))). % 20.39/20.59 Proof. % 20.39/20.59 assert (zenon_L1_ : (~((xa) = (xa))) -> False). % 20.39/20.59 do 0 intro. intros zenon_H2c. % 20.39/20.59 apply zenon_H2c. apply refl_equal. % 20.39/20.59 (* end of lemma zenon_L1_ *) % 20.39/20.59 assert (zenon_L2_ : (~((xb) = (xb))) -> False). % 20.39/20.59 do 0 intro. intros zenon_H2d. % 20.39/20.59 apply zenon_H2d. apply refl_equal. % 20.39/20.59 (* end of lemma zenon_L2_ *) % 20.39/20.59 assert (zenon_L3_ : (((sdtpldt0 (xb) (sz00)) = (xb))/\((xb) = (sdtpldt0 (sz00) (xb)))) -> (~(exists W0 : zenon_U, (((forall W0 : zenon_U, ((aElementOf0 W0 (slsdtgt0 (xa)))<->(exists W1 : zenon_U, ((aElement0 W1)/\((sdtasdt0 (xa) W1) = W0)))))->((forall W0 : zenon_U, ((aElementOf0 W0 (slsdtgt0 (xb)))<->(exists W1 : zenon_U, ((aElement0 W1)/\((sdtasdt0 (xb) W1) = W0)))))->((exists W1 : zenon_U, (exists W2 : zenon_U, ((aElementOf0 W1 (slsdtgt0 (xa)))/\((aElementOf0 W2 (slsdtgt0 (xb)))/\((sdtpldt0 W1 W2) = W0)))))\/(aElementOf0 W0 (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))/\(~(W0 = (sz00)))))) -> (aElementOf0 (sz00) (slsdtgt0 (xa))) -> (aElementOf0 (xb) (slsdtgt0 (xb))) -> (~((xb) = (sz00))) -> False). % 20.39/20.59 do 0 intro. intros zenon_H2e zenon_G zenon_H2f zenon_H30 zenon_H31. % 20.39/20.59 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H33. zenon_intro zenon_H32. % 20.39/20.59 cut (((xb) = (sdtpldt0 (sz00) (xb))) = ((xb) = (sz00))). % 20.39/20.59 intro zenon_D_pnotp. % 20.39/20.59 apply zenon_H31. % 20.39/20.59 rewrite <- zenon_D_pnotp. % 20.39/20.59 exact zenon_H32. % 20.39/20.59 cut (((sdtpldt0 (sz00) (xb)) = (sz00))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 20.39/20.59 cut (((xb) = (xb))); [idtac | apply NNPP; zenon_intro zenon_H2d]. % 20.39/20.59 congruence. % 20.39/20.59 apply zenon_H2d. apply refl_equal. % 20.39/20.59 apply zenon_G. exists (sdtpldt0 (sz00) (xb)). apply NNPP. zenon_intro zenon_H35. % 20.39/20.59 apply (zenon_notand_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 20.39/20.59 apply (zenon_notimply_s _ _ zenon_H37). zenon_intro zenon_H39. zenon_intro zenon_H38. % 20.39/20.59 apply (zenon_notimply_s _ _ zenon_H38). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 20.39/20.59 apply (zenon_notor_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 20.39/20.59 apply zenon_H3d. exists (sz00). apply NNPP. zenon_intro zenon_H3e. % 20.39/20.59 apply zenon_H3e. exists (xb). apply NNPP. zenon_intro zenon_H3f. % 20.39/20.59 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 20.39/20.59 exact (zenon_H41 zenon_H2f). % 20.39/20.59 apply (zenon_notand_s _ _ zenon_H40); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 20.39/20.59 exact (zenon_H43 zenon_H30). % 20.39/20.59 apply zenon_H42. apply refl_equal. % 20.39/20.59 exact (zenon_H36 zenon_H34). % 20.39/20.59 (* end of lemma zenon_L3_ *) % 20.39/20.59 assert (zenon_L4_ : (aElement0 (xb)) -> (~(exists W0 : zenon_U, (((forall W0 : zenon_U, ((aElementOf0 W0 (slsdtgt0 (xa)))<->(exists W1 : zenon_U, ((aElement0 W1)/\((sdtasdt0 (xa) W1) = W0)))))->((forall W0 : zenon_U, ((aElementOf0 W0 (slsdtgt0 (xb)))<->(exists W1 : zenon_U, ((aElement0 W1)/\((sdtasdt0 (xb) W1) = W0)))))->((exists W1 : zenon_U, (exists W2 : zenon_U, ((aElementOf0 W1 (slsdtgt0 (xa)))/\((aElementOf0 W2 (slsdtgt0 (xb)))/\((sdtpldt0 W1 W2) = W0)))))\/(aElementOf0 W0 (sdtpldt1 (slsdtgt0 (xa)) (slsdtgt0 (xb)))))))/\(~(W0 = (sz00)))))) -> (aElementOf0 (sz00) (slsdtgt0 (xa))) -> (aElementOf0 (xb) (slsdtgt0 (xb))) -> (~((xb) = (sz00))) -> False). % 20.39/20.59 do 0 intro. intros zenon_H44 zenon_G zenon_H2f zenon_H30 zenon_H31. % 20.39/20.59 generalize (mAddZero (xb)). zenon_intro zenon_H45. % 20.39/20.59 apply (zenon_imply_s _ _ zenon_H45); [ zenon_intro zenon_H46 | zenon_intro zenon_H2e ]. % 20.39/20.59 exact (zenon_H46 zenon_H44). % 20.39/20.59 apply (zenon_L3_); trivial. % 20.39/20.59 (* end of lemma zenon_L4_ *) % 20.39/20.59 apply NNPP. intro zenon_G. % 20.39/20.59 apply (zenon_and_s _ _ m__2091). zenon_intro zenon_H47. zenon_intro zenon_H44. % 20.39/20.59 apply (zenon_and_s _ _ m__2203). zenon_intro zenon_H49. zenon_intro zenon_H48. % 20.39/20.59 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H2f. zenon_intro zenon_H4a. % 20.39/20.59 apply (zenon_and_s _ _ zenon_H4a). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 20.39/20.59 apply (zenon_and_s _ _ zenon_H4b). zenon_intro zenon_H4e. zenon_intro zenon_H4d. % 20.39/20.59 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 20.39/20.59 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H52. zenon_intro zenon_H51. % 20.39/20.59 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H30. % 20.39/20.59 apply (zenon_or_s _ _ m__2110); [ zenon_intro zenon_H54 | zenon_intro zenon_H31 ]. % 20.39/20.59 generalize (mAddZero (xa)). zenon_intro zenon_H55. % 20.39/20.59 apply (zenon_imply_s _ _ zenon_H55); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 20.39/20.59 exact (zenon_H57 zenon_H47). % 20.39/20.59 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 20.39/20.59 elim (classic ((sz00) = (sz00))); [ zenon_intro zenon_H5a | zenon_intro zenon_H5b ]. % 20.39/20.59 cut (((sz00) = (sz00)) = ((xa) = (sz00))). % 20.39/20.59 intro zenon_D_pnotp. % 20.39/20.59 apply zenon_H54. % 20.39/20.59 rewrite <- zenon_D_pnotp. % 20.39/20.59 exact zenon_H5a. % 20.39/20.59 cut (((sz00) = (sz00))); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 20.39/20.59 cut (((sz00) = (xa))); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 20.39/20.59 congruence. % 20.39/20.59 cut (((sdtpldt0 (xa) (sz00)) = (xa)) = ((sz00) = (xa))). % 20.39/20.59 intro zenon_D_pnotp. % 20.39/20.59 apply zenon_H5c. % 20.39/20.59 rewrite <- zenon_D_pnotp. % 20.39/20.59 exact zenon_H59. % 20.39/20.59 cut (((xa) = (xa))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 20.39/20.59 cut (((sdtpldt0 (xa) (sz00)) = (sz00))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 20.39/20.59 congruence. % 20.39/20.59 elim (classic ((sz00) = (sz00))); [ zenon_intro zenon_H5a | zenon_intro zenon_H5b ]. % 20.39/20.59 cut (((sz00) = (sz00)) = ((sdtpldt0 (xa) (sz00)) = (sz00))). % 20.39/20.59 intro zenon_D_pnotp. % 20.39/20.59 apply zenon_H5d. % 20.39/20.59 rewrite <- zenon_D_pnotp. % 20.39/20.59 exact zenon_H5a. % 20.39/20.59 cut (((sz00) = (sz00))); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 20.39/20.59 cut (((sz00) = (sdtpldt0 (xa) (sz00)))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 20.39/20.59 congruence. % 20.39/20.59 apply zenon_G. exists (sdtpldt0 (xa) (sz00)). apply NNPP. zenon_intro zenon_H5f. % 20.39/20.59 apply (zenon_notand_s _ _ zenon_H5f); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 20.39/20.59 apply (zenon_notimply_s _ _ zenon_H61). zenon_intro zenon_H39. zenon_intro zenon_H62. % 20.39/20.59 apply (zenon_notimply_s _ _ zenon_H62). zenon_intro zenon_H3b. zenon_intro zenon_H63. % 20.39/20.59 apply (zenon_notor_s _ _ zenon_H63). zenon_intro zenon_H65. zenon_intro zenon_H64. % 20.39/20.59 apply zenon_H65. exists (xa). apply NNPP. zenon_intro zenon_H66. % 20.39/20.59 apply zenon_H66. exists (sz00). apply NNPP. zenon_intro zenon_H67. % 20.39/20.59 apply (zenon_notand_s _ _ zenon_H67); [ zenon_intro zenon_H69 | zenon_intro zenon_H68 ]. % 20.39/20.59 exact (zenon_H69 zenon_H4e). % 20.39/20.59 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 20.39/20.59 exact (zenon_H6b zenon_H52). % 20.39/20.59 apply zenon_H6a. apply refl_equal. % 20.39/20.59 apply zenon_H60. zenon_intro zenon_H6c. % 20.39/20.59 apply zenon_H5e. apply sym_equal. exact zenon_H6c. % 20.39/20.59 apply zenon_H5b. apply refl_equal. % 20.39/20.59 apply zenon_H5b. apply refl_equal. % 20.39/20.59 apply zenon_H2c. apply refl_equal. % 20.39/20.59 apply zenon_H5b. apply refl_equal. % 20.39/20.59 apply zenon_H5b. apply refl_equal. % 20.39/20.59 apply (zenon_L4_); trivial. % 20.39/20.59 Qed. % 20.39/20.59 % SZS output end Proof % 20.39/20.59 (* END-PROOF *) % 20.39/20.59 nodes searched: 543509 % 20.39/20.59 max branch formulas: 7437 % 20.39/20.59 proof nodes created: 15950 % 20.39/20.59 formulas created: 1327258 % 20.39/20.59 %------------------------------------------------------------------------------