%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : RNG099+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n020.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:27 EDT 2022 % Result : Theorem 5.99s 6.19s % Output : Proof 5.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG099+2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n020.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon May 30 18:21:09 EDT 2022 % 0.13/0.33 % CPUTime : % 5.99/6.19 (* PROOF-FOUND *) % 5.99/6.19 % SZS status Theorem % 5.99/6.19 (* BEGIN-PROOF *) % 5.99/6.19 % SZS output start Proof % 5.99/6.19 Theorem m__ : (exists W0 : zenon_U, ((aElement0 W0)/\(((aElementOf0 (sdtpldt0 W0 (smndt0 (xx))) (xI))\/(sdteqdtlpzmzozddtrp0 W0 (xx) (xI)))/\((aElementOf0 (sdtpldt0 W0 (smndt0 (xy))) (xJ))\/(sdteqdtlpzmzozddtrp0 W0 (xy) (xJ)))))). % 5.99/6.19 Proof. % 5.99/6.19 assert (zenon_L1_ : (~((xw) = (sdtpldt0 (sdtasdt0 (xy) (xa)) (sdtasdt0 (xx) (xb))))) -> False). % 5.99/6.19 do 0 intro. intros zenon_H23. % 5.99/6.19 exact (zenon_H23 m__1319). % 5.99/6.19 (* end of lemma zenon_L1_ *) % 5.99/6.19 assert (zenon_L2_ : (~((xI) = (xI))) -> False). % 5.99/6.19 do 0 intro. intros zenon_H24. % 5.99/6.19 apply zenon_H24. apply refl_equal. % 5.99/6.19 (* end of lemma zenon_L2_ *) % 5.99/6.19 assert (zenon_L3_ : (~((xJ) = (xJ))) -> False). % 5.99/6.19 do 0 intro. intros zenon_H25. % 5.99/6.19 apply zenon_H25. apply refl_equal. % 5.99/6.19 (* end of lemma zenon_L3_ *) % 5.99/6.19 apply NNPP. intro zenon_G. % 5.99/6.19 apply (zenon_and_s _ _ m__1205). zenon_intro zenon_H27. zenon_intro zenon_H26. % 5.99/6.19 apply (zenon_and_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 5.99/6.19 apply (zenon_and_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 5.99/6.19 apply (zenon_and_s _ _ zenon_H2a). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 5.99/6.19 apply (zenon_and_s _ _ m__1217). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 5.99/6.19 apply (zenon_and_s _ _ m__1294). zenon_intro zenon_H31. zenon_intro zenon_H30. % 5.99/6.19 apply (zenon_and_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 5.99/6.19 generalize (mEOfElem (xJ)). zenon_intro zenon_H34. % 5.99/6.19 apply (zenon_imply_s _ _ zenon_H34); [ zenon_intro zenon_H36 | zenon_intro zenon_H35 ]. % 5.99/6.19 exact (zenon_H36 zenon_H2d). % 5.99/6.19 generalize (mEOfElem (xI)). zenon_intro zenon_H37. % 5.99/6.19 apply (zenon_imply_s _ _ zenon_H37); [ zenon_intro zenon_H39 | zenon_intro zenon_H38 ]. % 5.99/6.19 exact (zenon_H39 zenon_H27). % 5.99/6.19 apply zenon_G. exists (sdtpldt0 (sdtasdt0 (xy) (xa)) (sdtasdt0 (xx) (xb))). apply NNPP. zenon_intro zenon_H3a. % 5.99/6.19 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H3c | zenon_intro zenon_H3b ]. % 5.99/6.19 generalize (mSortsB (sdtasdt0 (xy) (xa))). zenon_intro zenon_H3d. % 5.99/6.19 generalize (zenon_H3d (sdtasdt0 (xx) (xb))). zenon_intro zenon_H3e. % 5.99/6.19 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 5.99/6.19 apply (zenon_notand_s _ _ zenon_H40); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 5.99/6.19 generalize (mSortsB_02 (xy)). zenon_intro zenon_H43. % 5.99/6.19 generalize (zenon_H43 (xa)). zenon_intro zenon_H44. % 5.99/6.19 apply (zenon_imply_s _ _ zenon_H44); [ zenon_intro zenon_H46 | zenon_intro zenon_H45 ]. % 5.99/6.19 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 5.99/6.19 exact (zenon_H48 zenon_H2e). % 5.99/6.19 generalize (zenon_H38 (xa)). zenon_intro zenon_H49. % 5.99/6.19 apply (zenon_imply_s _ _ zenon_H49); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 5.99/6.19 exact (zenon_H4b zenon_H31). % 5.99/6.19 exact (zenon_H47 zenon_H4a). % 5.99/6.19 exact (zenon_H42 zenon_H45). % 5.99/6.19 generalize (mSortsB_02 (xx)). zenon_intro zenon_H4c. % 5.99/6.19 generalize (zenon_H4c (xb)). zenon_intro zenon_H4d. % 5.99/6.19 apply (zenon_imply_s _ _ zenon_H4d); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 5.99/6.19 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 5.99/6.19 exact (zenon_H51 zenon_H2f). % 5.99/6.19 generalize (zenon_H35 (xb)). zenon_intro zenon_H52. % 5.99/6.19 apply (zenon_imply_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 5.99/6.19 exact (zenon_H54 zenon_H33). % 5.99/6.19 exact (zenon_H50 zenon_H53). % 5.99/6.19 exact (zenon_H41 zenon_H4e). % 5.99/6.19 exact (zenon_H3c zenon_H3f). % 5.99/6.19 apply (zenon_notand_s _ _ zenon_H3b); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 5.99/6.19 apply (zenon_notor_s _ _ zenon_H56). zenon_intro zenon_H58. zenon_intro zenon_H57. % 5.99/6.19 cut ((aElementOf0 (sdtpldt0 (xw) (smndt0 (xx))) (xI)) = (aElementOf0 (sdtpldt0 (sdtpldt0 (sdtasdt0 (xy) (xa)) (sdtasdt0 (xx) (xb))) (smndt0 (xx))) (xI))). % 5.99/6.19 intro zenon_D_pnotp. % 5.99/6.19 apply zenon_H58. % 5.99/6.19 rewrite <- zenon_D_pnotp. % 5.99/6.19 exact m__1332. % 5.99/6.19 cut (((xI) = (xI))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 5.99/6.19 cut (((sdtpldt0 (xw) (smndt0 (xx))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xy) (xa)) (sdtasdt0 (xx) (xb))) (smndt0 (xx))))); [idtac | apply NNPP; zenon_intro zenon_H59]. % 5.99/6.19 congruence. % 5.99/6.19 cut (((smndt0 (xx)) = (smndt0 (xx)))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 5.99/6.19 cut (((xw) = (sdtpldt0 (sdtasdt0 (xy) (xa)) (sdtasdt0 (xx) (xb))))); [idtac | apply NNPP; zenon_intro zenon_H23]. % 5.99/6.19 congruence. % 5.99/6.19 exact (zenon_H23 m__1319). % 5.99/6.19 apply zenon_H5a. apply refl_equal. % 5.99/6.19 apply zenon_H24. apply refl_equal. % 5.99/6.19 apply (zenon_notor_s _ _ zenon_H55). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 5.99/6.19 cut ((aElementOf0 (sdtpldt0 (xw) (smndt0 (xy))) (xJ)) = (aElementOf0 (sdtpldt0 (sdtpldt0 (sdtasdt0 (xy) (xa)) (sdtasdt0 (xx) (xb))) (smndt0 (xy))) (xJ))). % 5.99/6.19 intro zenon_D_pnotp. % 5.99/6.19 apply zenon_H5c. % 5.99/6.19 rewrite <- zenon_D_pnotp. % 5.99/6.19 exact m__1409. % 5.99/6.19 cut (((xJ) = (xJ))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 5.99/6.19 cut (((sdtpldt0 (xw) (smndt0 (xy))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xy) (xa)) (sdtasdt0 (xx) (xb))) (smndt0 (xy))))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 5.99/6.19 congruence. % 5.99/6.19 cut (((smndt0 (xy)) = (smndt0 (xy)))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 5.99/6.19 cut (((xw) = (sdtpldt0 (sdtasdt0 (xy) (xa)) (sdtasdt0 (xx) (xb))))); [idtac | apply NNPP; zenon_intro zenon_H23]. % 5.99/6.19 congruence. % 5.99/6.19 exact (zenon_H23 m__1319). % 5.99/6.19 apply zenon_H5e. apply refl_equal. % 5.99/6.19 apply zenon_H25. apply refl_equal. % 5.99/6.19 Qed. % 5.99/6.19 % SZS output end Proof % 5.99/6.19 (* END-PROOF *) % 5.99/6.19 nodes searched: 68424 % 5.99/6.19 max branch formulas: 8530 % 5.99/6.19 proof nodes created: 1453 % 5.99/6.19 formulas created: 311264 % 5.99/6.19 %------------------------------------------------------------------------------