%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : COM022+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n028.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 : Fri Jul 15 01:53:03 EDT 2022 % Result : Theorem 1.75s 1.96s % Output : Proof 1.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : COM022+4 : TPTP v8.1.0. Released v4.0.0. % 0.09/0.15 % Command : run_zenon %s %d % 0.15/0.36 % Computer : n028.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Thu Jun 16 20:11:57 EDT 2022 % 0.15/0.36 % CPUTime : % 1.75/1.96 (* PROOF-FOUND *) % 1.75/1.96 % SZS status Theorem % 1.75/1.96 (* BEGIN-PROOF *) % 1.75/1.96 % SZS output start Proof % 1.75/1.96 Theorem m__ : (((((aReductOfIn0 (xb) (xa) (xR))\/((exists W0 : zenon_U, ((aElement0 W0)/\((aReductOfIn0 W0 (xa) (xR))/\(sdtmndtplgtdt0 W0 (xR) (xb)))))\/(sdtmndtplgtdt0 (xa) (xR) (xb))))/\((aReductOfIn0 (xc) (xa) (xR))\/((exists W0 : zenon_U, ((aElement0 W0)/\((aReductOfIn0 W0 (xa) (xR))/\(sdtmndtplgtdt0 W0 (xR) (xc)))))\/(sdtmndtplgtdt0 (xa) (xR) (xc)))))->(exists W0 : zenon_U, ((aElement0 W0)/\((aReductOfIn0 W0 (xa) (xR))/\(((W0 = (xb))\/(((aReductOfIn0 (xb) W0 (xR))\/(exists W1 : zenon_U, ((aElement0 W1)/\((aReductOfIn0 W1 W0 (xR))/\(sdtmndtplgtdt0 W1 (xR) (xb))))))/\(sdtmndtplgtdt0 W0 (xR) (xb))))/\((sdtmndtasgtdt0 W0 (xR) (xb))/\(exists W1 : zenon_U, ((aElement0 W1)/\((aReductOfIn0 W1 (xa) (xR))/\(((W1 = (xc))\/(((aReductOfIn0 (xc) W1 (xR))\/(exists W2 : zenon_U, ((aElement0 W2)/\((aReductOfIn0 W2 W1 (xR))/\(sdtmndtplgtdt0 W2 (xR) (xc))))))/\(sdtmndtplgtdt0 W1 (xR) (xc))))/\((sdtmndtasgtdt0 W1 (xR) (xc))/\(exists W2 : zenon_U, ((aElement0 W2)/\(((W0 = W2)\/(((aReductOfIn0 W2 W0 (xR))\/(exists W3 : zenon_U, ((aElement0 W3)/\((aReductOfIn0 W3 W0 (xR))/\(sdtmndtplgtdt0 W3 (xR) W2)))))/\(sdtmndtplgtdt0 W0 (xR) W2)))/\((sdtmndtasgtdt0 W0 (xR) W2)/\(((W1 = W2)\/(((aReductOfIn0 W2 W1 (xR))\/(exists W3 : zenon_U, ((aElement0 W3)/\((aReductOfIn0 W3 W1 (xR))/\(sdtmndtplgtdt0 W3 (xR) W2)))))/\(sdtmndtplgtdt0 W1 (xR) W2)))/\((sdtmndtasgtdt0 W1 (xR) W2)/\(exists W3 : zenon_U, ((aElement0 W3)/\(((W2 = W3)\/(((aReductOfIn0 W3 W2 (xR))\/(exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 W2 (xR))/\(sdtmndtplgtdt0 W4 (xR) W3)))))/\(sdtmndtplgtdt0 W2 (xR) W3)))/\((sdtmndtasgtdt0 W2 (xR) W3)/\((~(exists W4 : zenon_U, (aReductOfIn0 W4 W3 (xR))))/\((aNormalFormOfIn0 W3 W2 (xR))/\((((xb) = W3)\/(((aReductOfIn0 W3 (xb) (xR))\/(exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xb) (xR))/\(sdtmndtplgtdt0 W4 (xR) W3)))))/\(sdtmndtplgtdt0 (xb) (xR) W3)))/\((sdtmndtasgtdt0 (xb) (xR) W3)/\((((xc) = W3)\/(((aReductOfIn0 W3 (xc) (xR))\/(exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xc) (xR))/\(sdtmndtplgtdt0 W4 (xR) W3)))))/\(sdtmndtplgtdt0 (xc) (xR) W3)))/\(sdtmndtasgtdt0 (xc) (xR) W3)))))))))))))))))))))))))))->(((((xa) = (xb))\/(((aReductOfIn0 (xb) (xa) (xR))\/(exists W0 : zenon_U, ((aElement0 W0)/\((aReductOfIn0 W0 (xa) (xR))/\(sdtmndtplgtdt0 W0 (xR) (xb))))))/\(sdtmndtplgtdt0 (xa) (xR) (xb))))/\((sdtmndtasgtdt0 (xa) (xR) (xb))/\((((xa) = (xc))\/(((aReductOfIn0 (xc) (xa) (xR))\/(exists W0 : zenon_U, ((aElement0 W0)/\((aReductOfIn0 W0 (xa) (xR))/\(sdtmndtplgtdt0 W0 (xR) (xc))))))/\(sdtmndtplgtdt0 (xa) (xR) (xc))))/\(sdtmndtasgtdt0 (xa) (xR) (xc)))))->(exists W0 : zenon_U, ((aElement0 W0)/\((((xb) = W0)\/((aReductOfIn0 W0 (xb) (xR))\/((exists W1 : zenon_U, ((aElement0 W1)/\((aReductOfIn0 W1 (xb) (xR))/\(sdtmndtplgtdt0 W1 (xR) W0))))\/((sdtmndtplgtdt0 (xb) (xR) W0)\/(sdtmndtasgtdt0 (xb) (xR) W0)))))/\(((xc) = W0)\/((aReductOfIn0 W0 (xc) (xR))\/((exists W1 : zenon_U, ((aElement0 W1)/\((aReductOfIn0 W1 (xc) (xR))/\(sdtmndtplgtdt0 W1 (xR) W0))))\/((sdtmndtplgtdt0 (xc) (xR) W0)\/(sdtmndtasgtdt0 (xc) (xR) W0)))))))))). % 1.75/1.96 Proof. % 1.75/1.96 assert (zenon_L1_ : (~((xc) = (xc))) -> False). % 1.75/1.96 do 0 intro. intros zenon_H13. % 1.75/1.96 apply zenon_H13. apply refl_equal. % 1.75/1.96 (* end of lemma zenon_L1_ *) % 1.75/1.96 assert (zenon_L2_ : (~(((xc) = (xc))\/((aReductOfIn0 (xc) (xc) (xR))\/((exists W1 : zenon_U, ((aElement0 W1)/\((aReductOfIn0 W1 (xc) (xR))/\(sdtmndtplgtdt0 W1 (xR) (xc)))))\/((sdtmndtplgtdt0 (xc) (xR) (xc))\/(sdtmndtasgtdt0 (xc) (xR) (xc))))))) -> False). % 1.75/1.96 do 0 intro. intros zenon_H14. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H14). zenon_intro zenon_H13. zenon_intro zenon_H15. % 1.75/1.96 apply zenon_H13. apply refl_equal. % 1.75/1.96 (* end of lemma zenon_L2_ *) % 1.75/1.96 assert (zenon_L3_ : (~((xb) = (xb))) -> False). % 1.75/1.96 do 0 intro. intros zenon_H16. % 1.75/1.96 apply zenon_H16. apply refl_equal. % 1.75/1.96 (* end of lemma zenon_L3_ *) % 1.75/1.96 assert (zenon_L4_ : (~(((xb) = (xb))\/((aReductOfIn0 (xb) (xb) (xR))\/((exists W1 : zenon_U, ((aElement0 W1)/\((aReductOfIn0 W1 (xb) (xR))/\(sdtmndtplgtdt0 W1 (xR) (xb)))))\/((sdtmndtplgtdt0 (xb) (xR) (xb))\/(sdtmndtasgtdt0 (xb) (xR) (xb))))))) -> False). % 1.75/1.96 do 0 intro. intros zenon_H17. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H17). zenon_intro zenon_H16. zenon_intro zenon_H18. % 1.75/1.96 apply zenon_H16. apply refl_equal. % 1.75/1.96 (* end of lemma zenon_L4_ *) % 1.75/1.96 assert (zenon_L5_ : (~(((xc) = (xa))\/(sdtmndtplgtdt0 (xc) (xR) (xa)))) -> ((xa) = (xc)) -> False). % 1.75/1.96 do 0 intro. intros zenon_H19 zenon_H1a. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H19). zenon_intro zenon_H1c. zenon_intro zenon_H1b. % 1.75/1.96 apply zenon_H1c. apply sym_equal. exact zenon_H1a. % 1.75/1.96 (* end of lemma zenon_L5_ *) % 1.75/1.96 assert (zenon_L6_ : (((aReductOfIn0 (xc) (xa) (xR))\/(exists W0 : zenon_U, ((aElement0 W0)/\((aReductOfIn0 W0 (xa) (xR))/\(sdtmndtplgtdt0 W0 (xR) (xc))))))/\(sdtmndtplgtdt0 (xa) (xR) (xc))) -> (~(sdtmndtplgtdt0 (xa) (xR) (xc))) -> False). % 1.75/1.96 do 0 intro. intros zenon_H1d zenon_H1e. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H1d). zenon_intro zenon_H20. zenon_intro zenon_H1f. % 1.75/1.96 exact (zenon_H1e zenon_H1f). % 1.75/1.96 (* end of lemma zenon_L6_ *) % 1.75/1.96 assert (zenon_L7_ : forall (zenon_TW3_bj : zenon_U), (~(((xb) = zenon_TW3_bj)\/((aReductOfIn0 zenon_TW3_bj (xb) (xR))\/((exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xb) (xR))/\(sdtmndtplgtdt0 W4 (xR) zenon_TW3_bj))))\/((sdtmndtplgtdt0 (xb) (xR) zenon_TW3_bj)\/(sdtmndtasgtdt0 (xb) (xR) zenon_TW3_bj)))))) -> ((xb) = zenon_TW3_bj) -> False). % 1.75/1.96 do 1 intro. intros zenon_H21 zenon_H22. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 1.75/1.96 exact (zenon_H25 zenon_H22). % 1.75/1.96 (* end of lemma zenon_L7_ *) % 1.75/1.96 assert (zenon_L8_ : forall (zenon_TW3_bj : zenon_U), (~(((xc) = zenon_TW3_bj)\/((aReductOfIn0 zenon_TW3_bj (xc) (xR))\/((exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xc) (xR))/\(sdtmndtplgtdt0 W4 (xR) zenon_TW3_bj))))\/((sdtmndtplgtdt0 (xc) (xR) zenon_TW3_bj)\/(sdtmndtasgtdt0 (xc) (xR) zenon_TW3_bj)))))) -> (aReductOfIn0 zenon_TW3_bj (xc) (xR)) -> False). % 1.75/1.96 do 1 intro. intros zenon_H26 zenon_H27. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 1.75/1.96 exact (zenon_H2b zenon_H27). % 1.75/1.96 (* end of lemma zenon_L8_ *) % 1.75/1.96 assert (zenon_L9_ : forall (zenon_TW3_bj : zenon_U), (~(((xc) = zenon_TW3_bj)\/((aReductOfIn0 zenon_TW3_bj (xc) (xR))\/((exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xc) (xR))/\(sdtmndtplgtdt0 W4 (xR) zenon_TW3_bj))))\/((sdtmndtplgtdt0 (xc) (xR) zenon_TW3_bj)\/(sdtmndtasgtdt0 (xc) (xR) zenon_TW3_bj)))))) -> (exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xc) (xR))/\(sdtmndtplgtdt0 W4 (xR) zenon_TW3_bj)))) -> False). % 1.75/1.96 do 1 intro. intros zenon_H26 zenon_H2c. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H2a). zenon_intro zenon_H2e. zenon_intro zenon_H2d. % 1.75/1.96 exact (zenon_H2e zenon_H2c). % 1.75/1.96 (* end of lemma zenon_L9_ *) % 1.75/1.96 assert (zenon_L10_ : forall (zenon_TW3_bj : zenon_U), (~(((xb) = zenon_TW3_bj)\/((aReductOfIn0 zenon_TW3_bj (xb) (xR))\/((exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xb) (xR))/\(sdtmndtplgtdt0 W4 (xR) zenon_TW3_bj))))\/((sdtmndtplgtdt0 (xb) (xR) zenon_TW3_bj)\/(sdtmndtasgtdt0 (xb) (xR) zenon_TW3_bj)))))) -> (aReductOfIn0 zenon_TW3_bj (xb) (xR)) -> False). % 1.75/1.96 do 1 intro. intros zenon_H21 zenon_H2f. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H24). zenon_intro zenon_H31. zenon_intro zenon_H30. % 1.75/1.96 exact (zenon_H31 zenon_H2f). % 1.75/1.96 (* end of lemma zenon_L10_ *) % 1.75/1.96 assert (zenon_L11_ : forall (zenon_TW3_bj : zenon_U), (~(((xc) = zenon_TW3_bj)\/((aReductOfIn0 zenon_TW3_bj (xc) (xR))\/((exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xc) (xR))/\(sdtmndtplgtdt0 W4 (xR) zenon_TW3_bj))))\/((sdtmndtplgtdt0 (xc) (xR) zenon_TW3_bj)\/(sdtmndtasgtdt0 (xc) (xR) zenon_TW3_bj)))))) -> ((xc) = zenon_TW3_bj) -> False). % 1.75/1.96 do 1 intro. intros zenon_H26 zenon_H32. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 1.75/1.96 exact (zenon_H29 zenon_H32). % 1.75/1.96 (* end of lemma zenon_L11_ *) % 1.75/1.96 assert (zenon_L12_ : forall (zenon_TW3_bj : zenon_U), (~(((xb) = zenon_TW3_bj)\/((aReductOfIn0 zenon_TW3_bj (xb) (xR))\/((exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xb) (xR))/\(sdtmndtplgtdt0 W4 (xR) zenon_TW3_bj))))\/((sdtmndtplgtdt0 (xb) (xR) zenon_TW3_bj)\/(sdtmndtasgtdt0 (xb) (xR) zenon_TW3_bj)))))) -> (exists W4 : zenon_U, ((aElement0 W4)/\((aReductOfIn0 W4 (xb) (xR))/\(sdtmndtplgtdt0 W4 (xR) zenon_TW3_bj)))) -> False). % 1.75/1.96 do 1 intro. intros zenon_H21 zenon_H33. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H24). zenon_intro zenon_H31. zenon_intro zenon_H30. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H30). zenon_intro zenon_H35. zenon_intro zenon_H34. % 1.75/1.96 exact (zenon_H35 zenon_H33). % 1.75/1.96 (* end of lemma zenon_L12_ *) % 1.75/1.96 apply NNPP. intro zenon_G. % 1.75/1.96 apply (zenon_and_s _ _ m__731). zenon_intro zenon_H37. zenon_intro zenon_H36. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 1.75/1.96 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 1.75/1.96 apply (zenon_notimply_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H3d). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 1.75/1.96 apply (zenon_imply_s _ _ zenon_H3b); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H45); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H47). zenon_intro zenon_H49. zenon_intro zenon_H48. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 1.75/1.96 apply (zenon_or_s _ _ zenon_H3f); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 1.75/1.96 apply zenon_H3c. exists (xc). apply NNPP. zenon_intro zenon_H4e. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H50 | zenon_intro zenon_H4f ]. % 1.75/1.96 exact (zenon_H50 zenon_H38). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H14 ]. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H52. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H52). zenon_intro zenon_H55. zenon_intro zenon_H54. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H54). zenon_intro zenon_H57. zenon_intro zenon_H56. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 1.75/1.96 generalize (mTCRDef (xb)). zenon_intro zenon_H5a. % 1.75/1.96 generalize (mTCRTrans (xb)). zenon_intro zenon_H5b. % 1.75/1.96 generalize (zenon_H5a (xR)). zenon_intro zenon_H5c. % 1.75/1.96 generalize (zenon_H5b (xR)). zenon_intro zenon_H5d. % 1.75/1.96 generalize (zenon_H5c (xa)). zenon_intro zenon_H5e. % 1.75/1.96 apply (zenon_imply_s _ _ zenon_H5e); [ zenon_intro zenon_H60 | zenon_intro zenon_H5f ]. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H60); [ zenon_intro zenon_H62 | zenon_intro zenon_H61 ]. % 1.75/1.96 exact (zenon_H62 zenon_H39). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H64 | zenon_intro zenon_H63 ]. % 1.75/1.96 exact (zenon_H64 m__656). % 1.75/1.96 exact (zenon_H63 zenon_H37). % 1.75/1.96 apply (zenon_equiv_s _ _ zenon_H5f); [ zenon_intro zenon_H68; zenon_intro zenon_H67 | zenon_intro zenon_H66; zenon_intro zenon_H65 ]. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 1.75/1.96 apply zenon_H6a. apply sym_equal. exact zenon_H4d. % 1.75/1.96 generalize (zenon_H5d (xa)). zenon_intro zenon_H6b. % 1.75/1.96 generalize (zenon_H6b (xc)). zenon_intro zenon_H6c. % 1.75/1.96 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6e | zenon_intro zenon_H6d ]. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_H62 | zenon_intro zenon_H6f ]. % 1.75/1.96 exact (zenon_H62 zenon_H39). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H6f); [ zenon_intro zenon_H64 | zenon_intro zenon_H70 ]. % 1.75/1.96 exact (zenon_H64 m__656). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H63 | zenon_intro zenon_H50 ]. % 1.75/1.96 exact (zenon_H63 zenon_H37). % 1.75/1.96 exact (zenon_H50 zenon_H38). % 1.75/1.96 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H72 | zenon_intro zenon_H71 ]. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H68 | zenon_intro zenon_H73 ]. % 1.75/1.96 exact (zenon_H68 zenon_H66). % 1.75/1.96 exact (zenon_H73 zenon_H42). % 1.75/1.96 exact (zenon_H58 zenon_H71). % 1.75/1.96 apply (zenon_L2_); trivial. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H4c). zenon_intro zenon_H75. zenon_intro zenon_H74. % 1.75/1.96 exact (zenon_H4a zenon_H74). % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H46). zenon_intro zenon_H77. zenon_intro zenon_H76. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H76). zenon_intro zenon_H78. zenon_intro zenon_H1e. % 1.75/1.96 apply (zenon_or_s _ _ zenon_H43); [ zenon_intro zenon_H1a | zenon_intro zenon_H1d ]. % 1.75/1.96 apply zenon_H3c. exists (xb). apply NNPP. zenon_intro zenon_H79. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H79); [ zenon_intro zenon_H62 | zenon_intro zenon_H7a ]. % 1.75/1.96 exact (zenon_H62 zenon_H39). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H17 | zenon_intro zenon_H7b ]. % 1.75/1.96 apply (zenon_L4_); trivial. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H7b). zenon_intro zenon_H7d. zenon_intro zenon_H7c. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H7c). zenon_intro zenon_H7f. zenon_intro zenon_H7e. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H7e). zenon_intro zenon_H81. zenon_intro zenon_H80. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 1.75/1.96 generalize (mTCRDef (xc)). zenon_intro zenon_H84. % 1.75/1.96 generalize (mTCRTrans (xc)). zenon_intro zenon_H85. % 1.75/1.96 generalize (zenon_H84 (xR)). zenon_intro zenon_H86. % 1.75/1.96 generalize (zenon_H85 (xR)). zenon_intro zenon_H87. % 1.75/1.96 generalize (zenon_H86 (xa)). zenon_intro zenon_H88. % 1.75/1.96 apply (zenon_imply_s _ _ zenon_H88); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H50 | zenon_intro zenon_H61 ]. % 1.75/1.96 exact (zenon_H50 zenon_H38). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H64 | zenon_intro zenon_H63 ]. % 1.75/1.96 exact (zenon_H64 m__656). % 1.75/1.96 exact (zenon_H63 zenon_H37). % 1.75/1.96 apply (zenon_equiv_s _ _ zenon_H89); [ zenon_intro zenon_H8d; zenon_intro zenon_H19 | zenon_intro zenon_H8c; zenon_intro zenon_H8b ]. % 1.75/1.96 apply (zenon_L5_); trivial. % 1.75/1.96 generalize (zenon_H87 (xa)). zenon_intro zenon_H8e. % 1.75/1.96 generalize (zenon_H8e (xb)). zenon_intro zenon_H8f. % 1.75/1.96 apply (zenon_imply_s _ _ zenon_H8f); [ zenon_intro zenon_H91 | zenon_intro zenon_H90 ]. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H91); [ zenon_intro zenon_H50 | zenon_intro zenon_H92 ]. % 1.75/1.96 exact (zenon_H50 zenon_H38). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H92); [ zenon_intro zenon_H64 | zenon_intro zenon_H93 ]. % 1.75/1.96 exact (zenon_H64 m__656). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 1.75/1.96 exact (zenon_H63 zenon_H37). % 1.75/1.96 exact (zenon_H62 zenon_H39). % 1.75/1.96 apply (zenon_imply_s _ _ zenon_H90); [ zenon_intro zenon_H95 | zenon_intro zenon_H94 ]. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H8d | zenon_intro zenon_H96 ]. % 1.75/1.96 exact (zenon_H8d zenon_H8c). % 1.75/1.96 exact (zenon_H96 zenon_H41). % 1.75/1.96 exact (zenon_H82 zenon_H94). % 1.75/1.96 apply (zenon_L6_); trivial. % 1.75/1.96 elim zenon_H44. zenon_intro zenon_TW0_fv. zenon_intro zenon_H98. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H98). zenon_intro zenon_H9a. zenon_intro zenon_H99. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H99). zenon_intro zenon_H9c. zenon_intro zenon_H9b. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_H9e. zenon_intro zenon_H9d. % 1.75/1.96 apply (zenon_and_s _ _ zenon_H9d). zenon_intro zenon_Ha0. zenon_intro zenon_H9f. % 1.75/1.96 elim zenon_H9f. zenon_intro zenon_TW1_gf. zenon_intro zenon_Ha2. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Ha4. zenon_intro zenon_Ha3. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Ha3). zenon_intro zenon_Ha6. zenon_intro zenon_Ha5. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Ha5). zenon_intro zenon_Ha8. zenon_intro zenon_Ha7. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Ha7). zenon_intro zenon_Haa. zenon_intro zenon_Ha9. % 1.75/1.96 elim zenon_Ha9. zenon_intro zenon_TW2_gp. zenon_intro zenon_Hac. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hac). zenon_intro zenon_Hae. zenon_intro zenon_Had. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Had). zenon_intro zenon_Hb0. zenon_intro zenon_Haf. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Haf). zenon_intro zenon_Hb2. zenon_intro zenon_Hb1. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hb1). zenon_intro zenon_Hb4. zenon_intro zenon_Hb3. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hb3). zenon_intro zenon_Hb6. zenon_intro zenon_Hb5. % 1.75/1.96 elim zenon_Hb5. zenon_intro zenon_TW3_bj. zenon_intro zenon_Hb7. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hb7). zenon_intro zenon_Hb9. zenon_intro zenon_Hb8. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hb8). zenon_intro zenon_Hbb. zenon_intro zenon_Hba. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_Hbd. zenon_intro zenon_Hbc. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hbc). zenon_intro zenon_Hbf. zenon_intro zenon_Hbe. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hbe). zenon_intro zenon_Hc1. zenon_intro zenon_Hc0. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hc0). zenon_intro zenon_Hc3. zenon_intro zenon_Hc2. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hc2). zenon_intro zenon_Hc5. zenon_intro zenon_Hc4. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hc4). zenon_intro zenon_Hc7. zenon_intro zenon_Hc6. % 1.75/1.96 apply (zenon_or_s _ _ zenon_Hc3); [ zenon_intro zenon_H22 | zenon_intro zenon_Hc8 ]. % 1.75/1.96 apply (zenon_or_s _ _ zenon_Hc7); [ zenon_intro zenon_H32 | zenon_intro zenon_Hc9 ]. % 1.75/1.96 apply zenon_H3c. exists (xc). apply NNPP. zenon_intro zenon_H4e. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H50 | zenon_intro zenon_H4f ]. % 1.75/1.96 exact (zenon_H50 zenon_H38). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H14 ]. % 1.75/1.96 apply (zenon_notor_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H52. % 1.75/1.96 cut (((xb) = zenon_TW3_bj) = ((xb) = (xc))). % 1.75/1.96 intro zenon_D_pnotp. % 1.75/1.96 apply zenon_H53. % 1.75/1.96 rewrite <- zenon_D_pnotp. % 1.75/1.96 exact zenon_H22. % 1.75/1.96 cut ((zenon_TW3_bj = (xc))); [idtac | apply NNPP; zenon_intro zenon_Hca]. % 1.75/1.96 cut (((xb) = (xb))); [idtac | apply NNPP; zenon_intro zenon_H16]. % 1.75/1.96 congruence. % 1.75/1.96 apply zenon_H16. apply refl_equal. % 1.75/1.96 apply zenon_Hca. apply sym_equal. exact zenon_H32. % 1.75/1.96 apply (zenon_L2_); trivial. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_Hcc. zenon_intro zenon_Hcb. % 1.75/1.96 apply (zenon_or_s _ _ zenon_Hcc); [ zenon_intro zenon_H27 | zenon_intro zenon_H2c ]. % 1.75/1.96 apply zenon_H3c. exists zenon_TW3_bj. apply NNPP. zenon_intro zenon_Hcd. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 1.75/1.96 exact (zenon_Hcf zenon_Hb9). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_H21 | zenon_intro zenon_H26 ]. % 1.75/1.96 apply (zenon_L7_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_L8_ zenon_TW3_bj); trivial. % 1.75/1.96 apply zenon_H3c. exists zenon_TW3_bj. apply NNPP. zenon_intro zenon_Hcd. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 1.75/1.96 exact (zenon_Hcf zenon_Hb9). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_H21 | zenon_intro zenon_H26 ]. % 1.75/1.96 apply (zenon_L7_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_L9_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hc8). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 1.75/1.96 apply (zenon_or_s _ _ zenon_Hd1); [ zenon_intro zenon_H2f | zenon_intro zenon_H33 ]. % 1.75/1.96 apply (zenon_or_s _ _ zenon_Hc7); [ zenon_intro zenon_H32 | zenon_intro zenon_Hc9 ]. % 1.75/1.96 apply zenon_H3c. exists zenon_TW3_bj. apply NNPP. zenon_intro zenon_Hcd. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 1.75/1.96 exact (zenon_Hcf zenon_Hb9). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_H21 | zenon_intro zenon_H26 ]. % 1.75/1.96 apply (zenon_L10_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_L11_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_Hcc. zenon_intro zenon_Hcb. % 1.75/1.96 apply (zenon_or_s _ _ zenon_Hcc); [ zenon_intro zenon_H27 | zenon_intro zenon_H2c ]. % 1.75/1.96 apply zenon_H3c. exists zenon_TW3_bj. apply NNPP. zenon_intro zenon_Hcd. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 1.75/1.96 exact (zenon_Hcf zenon_Hb9). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_H21 | zenon_intro zenon_H26 ]. % 1.75/1.96 apply (zenon_L10_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_L8_ zenon_TW3_bj); trivial. % 1.75/1.96 apply zenon_H3c. exists zenon_TW3_bj. apply NNPP. zenon_intro zenon_Hcd. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 1.75/1.96 exact (zenon_Hcf zenon_Hb9). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_H21 | zenon_intro zenon_H26 ]. % 1.75/1.96 apply (zenon_L10_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_L9_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_or_s _ _ zenon_Hc7); [ zenon_intro zenon_H32 | zenon_intro zenon_Hc9 ]. % 1.75/1.96 apply zenon_H3c. exists zenon_TW3_bj. apply NNPP. zenon_intro zenon_Hcd. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 1.75/1.96 exact (zenon_Hcf zenon_Hb9). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_H21 | zenon_intro zenon_H26 ]. % 1.75/1.96 apply (zenon_L12_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_L11_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_Hcc. zenon_intro zenon_Hcb. % 1.75/1.96 apply (zenon_or_s _ _ zenon_Hcc); [ zenon_intro zenon_H27 | zenon_intro zenon_H2c ]. % 1.75/1.96 apply zenon_H3c. exists zenon_TW3_bj. apply NNPP. zenon_intro zenon_Hcd. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 1.75/1.96 exact (zenon_Hcf zenon_Hb9). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_H21 | zenon_intro zenon_H26 ]. % 1.75/1.96 apply (zenon_L12_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_L8_ zenon_TW3_bj); trivial. % 1.75/1.96 apply zenon_H3c. exists zenon_TW3_bj. apply NNPP. zenon_intro zenon_Hcd. % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hcd); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 1.75/1.96 exact (zenon_Hcf zenon_Hb9). % 1.75/1.96 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_H21 | zenon_intro zenon_H26 ]. % 1.75/1.96 apply (zenon_L12_ zenon_TW3_bj); trivial. % 1.75/1.96 apply (zenon_L9_ zenon_TW3_bj); trivial. % 1.75/1.96 Qed. % 1.75/1.96 % SZS output end Proof % 1.75/1.96 (* END-PROOF *) % 1.75/1.96 nodes searched: 53822 % 1.75/1.96 max branch formulas: 4621 % 1.75/1.96 proof nodes created: 3069 % 1.75/1.96 formulas created: 159112 % 1.75/1.96 %------------------------------------------------------------------------------