%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG118+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n018.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:30 EDT 2022 % Result : Theorem 10.53s 10.71s % Output : Proof 10.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : RNG118+4 : TPTP v8.1.0. Released v4.0.0. % 0.13/0.13 % Command : run_zenon %s %d % 0.14/0.36 % Computer : n018.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Mon May 30 18:05:42 EDT 2022 % 0.14/0.36 % CPUTime : % 10.53/10.71 (* PROOF-FOUND *) % 10.53/10.71 % SZS status Theorem % 10.53/10.71 (* BEGIN-PROOF *) % 10.53/10.71 % SZS output start Proof % 10.53/10.71 Theorem m__ : (exists W0 : zenon_U, (exists W1 : zenon_U, ((aElement0 W0)/\((aElement0 W1)/\(((xb) = (sdtpldt0 (sdtasdt0 W0 (xu)) W1))/\((W1 = (sz00))\/(iLess0 (sbrdtbr0 W1) (sbrdtbr0 (xu))))))))). % 10.53/10.71 Proof. % 10.53/10.71 assert (zenon_L1_ : (forall W1 : zenon_U, ((aElementOf0 W1 (xI))->(aElement0 W1))) -> (aElementOf0 (xu) (xI)) -> (~(aElement0 (xu))) -> False). % 10.53/10.71 do 0 intro. intros zenon_H32 zenon_H33 zenon_H34. % 10.53/10.71 generalize (zenon_H32 (xu)). zenon_intro zenon_H35. % 10.53/10.71 apply (zenon_imply_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 10.53/10.71 exact (zenon_H37 zenon_H33). % 10.53/10.71 exact (zenon_H34 zenon_H36). % 10.53/10.71 (* end of lemma zenon_L1_ *) % 10.53/10.71 assert (zenon_L2_ : (aSet0 (xI)) -> (aElementOf0 (xu) (xI)) -> (~(aElement0 (xu))) -> False). % 10.53/10.71 do 0 intro. intros zenon_H38 zenon_H33 zenon_H34. % 10.53/10.71 generalize (mEOfElem (xI)). zenon_intro zenon_H39. % 10.53/10.71 apply (zenon_imply_s _ _ zenon_H39); [ zenon_intro zenon_H3a | zenon_intro zenon_H32 ]. % 10.53/10.71 exact (zenon_H3a zenon_H38). % 10.53/10.71 apply (zenon_L1_); trivial. % 10.53/10.71 (* end of lemma zenon_L2_ *) % 10.53/10.71 assert (zenon_L3_ : forall (zenon_TW3_cj : zenon_U), (~((zenon_TW3_cj = (sz00))\/(iLess0 (sbrdtbr0 zenon_TW3_cj) (sbrdtbr0 (xu))))) -> (zenon_TW3_cj = (sz00)) -> False). % 10.53/10.71 do 1 intro. intros zenon_H3b zenon_H3c. % 10.53/10.71 apply (zenon_notor_s _ _ zenon_H3b). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 10.53/10.71 exact (zenon_H3f zenon_H3c). % 10.53/10.71 (* end of lemma zenon_L3_ *) % 10.53/10.71 assert (zenon_L4_ : forall (zenon_TW3_cj : zenon_U) (zenon_TW2_cq : zenon_U), (~(exists W1 : zenon_U, ((aElement0 zenon_TW2_cq)/\((aElement0 W1)/\(((xb) = (sdtpldt0 (sdtasdt0 zenon_TW2_cq (xu)) W1))/\((W1 = (sz00))\/(iLess0 (sbrdtbr0 W1) (sbrdtbr0 (xu))))))))) -> (aElement0 zenon_TW2_cq) -> (aElement0 zenon_TW3_cj) -> ((xb) = (sdtpldt0 (sdtasdt0 zenon_TW2_cq (xu)) zenon_TW3_cj)) -> (zenon_TW3_cj = (sz00)) -> False). % 10.53/10.71 do 2 intro. intros zenon_H40 zenon_H41 zenon_H42 zenon_H43 zenon_H3c. % 10.53/10.71 apply zenon_H40. exists zenon_TW3_cj. apply NNPP. zenon_intro zenon_H45. % 10.53/10.71 apply (zenon_notand_s _ _ zenon_H45); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 10.53/10.71 exact (zenon_H47 zenon_H41). % 10.53/10.71 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H49 | zenon_intro zenon_H48 ]. % 10.53/10.71 exact (zenon_H49 zenon_H42). % 10.53/10.71 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H4a | zenon_intro zenon_H3b ]. % 10.53/10.71 exact (zenon_H4a zenon_H43). % 10.53/10.71 apply (zenon_L3_ zenon_TW3_cj); trivial. % 10.53/10.71 (* end of lemma zenon_L4_ *) % 10.53/10.71 assert (zenon_L5_ : forall (zenon_TW3_cj : zenon_U), (~((zenon_TW3_cj = (sz00))\/(iLess0 (sbrdtbr0 zenon_TW3_cj) (sbrdtbr0 (xu))))) -> (iLess0 (sbrdtbr0 zenon_TW3_cj) (sbrdtbr0 (xu))) -> False). % 10.53/10.71 do 1 intro. intros zenon_H3b zenon_H4b. % 10.53/10.71 apply (zenon_notor_s _ _ zenon_H3b). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 10.53/10.71 exact (zenon_H3e zenon_H4b). % 10.53/10.71 (* end of lemma zenon_L5_ *) % 10.53/10.71 apply NNPP. intro zenon_G. % 10.53/10.71 apply (zenon_and_s _ _ m__2091). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 10.53/10.71 apply (zenon_and_s _ _ m__2174). zenon_intro zenon_H38. zenon_intro zenon_H4e. % 10.53/10.71 apply (zenon_and_s _ _ m__2273). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 10.53/10.71 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H33. zenon_intro zenon_H51. % 10.53/10.71 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H52. % 10.53/10.71 generalize (mDivision (xb)). zenon_intro zenon_H54. % 10.53/10.71 generalize (zenon_H54 (xu)). zenon_intro zenon_H55. % 10.53/10.71 apply (zenon_imply_s _ _ zenon_H55); [ zenon_intro zenon_H57 | zenon_intro zenon_H56 ]. % 10.53/10.71 apply (zenon_notand_s _ _ zenon_H57); [ zenon_intro zenon_H59 | zenon_intro zenon_H58 ]. % 10.53/10.71 exact (zenon_H59 zenon_H4c). % 10.53/10.71 apply (zenon_notand_s _ _ zenon_H58); [ zenon_intro zenon_H34 | zenon_intro zenon_H5a ]. % 10.53/10.71 apply (zenon_L2_); trivial. % 10.53/10.71 exact (zenon_H5a zenon_H53). % 10.53/10.71 elim zenon_H56. zenon_intro zenon_TW2_cq. zenon_intro zenon_H5b. % 10.53/10.71 elim zenon_H5b. zenon_intro zenon_TW3_cj. zenon_intro zenon_H5c. % 10.53/10.71 apply (zenon_and_s _ _ zenon_H5c). zenon_intro zenon_H41. zenon_intro zenon_H5d. % 10.53/10.71 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H42. zenon_intro zenon_H5e. % 10.53/10.71 apply (zenon_and_s _ _ zenon_H5e). zenon_intro zenon_H43. zenon_intro zenon_H5f. % 10.53/10.71 apply (zenon_imply_s _ _ zenon_H5f); [ zenon_intro zenon_H60 | zenon_intro zenon_H4b ]. % 10.53/10.72 apply zenon_H60. zenon_intro zenon_H3c. % 10.53/10.72 apply zenon_G. exists zenon_TW2_cq. apply NNPP. zenon_intro zenon_H40. % 10.53/10.72 apply (zenon_L4_ zenon_TW3_cj zenon_TW2_cq); trivial. % 10.53/10.72 apply zenon_G. exists zenon_TW2_cq. apply NNPP. zenon_intro zenon_H40. % 10.53/10.72 apply zenon_H40. exists zenon_TW3_cj. apply NNPP. zenon_intro zenon_H45. % 10.53/10.72 apply (zenon_notand_s _ _ zenon_H45); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 10.53/10.72 exact (zenon_H47 zenon_H41). % 10.53/10.72 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H49 | zenon_intro zenon_H48 ]. % 10.53/10.72 exact (zenon_H49 zenon_H42). % 10.53/10.72 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H4a | zenon_intro zenon_H3b ]. % 10.53/10.72 exact (zenon_H4a zenon_H43). % 10.53/10.72 apply (zenon_L5_ zenon_TW3_cj); trivial. % 10.53/10.72 Qed. % 10.53/10.72 % SZS output end Proof % 10.53/10.72 (* END-PROOF *) % 10.53/10.72 nodes searched: 49009 % 10.53/10.72 max branch formulas: 11973 % 10.53/10.72 proof nodes created: 1823 % 10.53/10.72 formulas created: 530066 % 10.53/10.72 %------------------------------------------------------------------------------