%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n025.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 : Sun Jul 17 03:39:24 EDT 2022 % Result : Unsatisfiable 12.56s 12.81s % Output : Proof 12.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n025.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 : Tue Jun 7 11:53:04 EDT 2022 % 0.12/0.33 % CPUTime : % 12.56/12.81 (* PROOF-FOUND *) % 12.56/12.81 % SZS status Unsatisfiable % 12.56/12.81 (* BEGIN-PROOF *) % 12.56/12.81 % SZS output start Proof % 12.56/12.81 Theorem zenon_thm : False. % 12.56/12.81 Proof. % 12.56/12.81 assert (zenon_L1_ : forall (zenon_TY_y : zenon_U) (zenon_TY_z : zenon_U), (~(cp2 zenon_TY_z)) -> (cp2 zenon_TY_y) -> (zenon_TY_z = zenon_TY_y) -> False). % 12.56/12.81 do 2 intro. intros zenon_H15 zenon_H16 zenon_H17. % 12.56/12.81 cut ((cp2 zenon_TY_y) = (cp2 zenon_TY_z)). % 12.56/12.81 intro zenon_D_pnotp. % 12.56/12.81 apply zenon_H15. % 12.56/12.81 rewrite <- zenon_D_pnotp. % 12.56/12.81 exact zenon_H16. % 12.56/12.81 cut ((zenon_TY_y = zenon_TY_z)); [idtac | apply NNPP; zenon_intro zenon_H1a]. % 12.56/12.81 congruence. % 12.56/12.81 apply zenon_H1a. apply sym_equal. exact zenon_H17. % 12.56/12.81 (* end of lemma zenon_L1_ *) % 12.56/12.81 assert (zenon_L2_ : forall (zenon_TY_bd : zenon_U), (~((cp4 zenon_TY_bd)\/(cp5 zenon_TY_bd))) -> (cp5 zenon_TY_bd) -> False). % 12.56/12.81 do 1 intro. intros zenon_H1b zenon_H1c. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H1b). zenon_intro zenon_H1f. zenon_intro zenon_H1e. % 12.56/12.81 exact (zenon_H1e zenon_H1c). % 12.56/12.81 (* end of lemma zenon_L2_ *) % 12.56/12.81 assert (zenon_L3_ : forall (zenon_TY_z : zenon_U), (~((cp4 zenon_TY_z)\/(cp5 zenon_TY_z))) -> (cp4 zenon_TY_z) -> False). % 12.56/12.81 do 1 intro. intros zenon_H20 zenon_H21. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 12.56/12.81 exact (zenon_H23 zenon_H21). % 12.56/12.81 (* end of lemma zenon_L3_ *) % 12.56/12.81 assert (zenon_L4_ : forall (zenon_TY_bm : zenon_U), (~((cp4 zenon_TY_bm)\/((cp5 zenon_TY_bm)\/(cp3 zenon_TY_bm)))) -> (cp3 zenon_TY_bm) -> False). % 12.56/12.81 do 1 intro. intros zenon_H24 zenon_H25. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H24). zenon_intro zenon_H28. zenon_intro zenon_H27. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H27). zenon_intro zenon_H2a. zenon_intro zenon_H29. % 12.56/12.81 exact (zenon_H29 zenon_H25). % 12.56/12.81 (* end of lemma zenon_L4_ *) % 12.56/12.81 assert (zenon_L5_ : forall (zenon_TY_bd : zenon_U), (~((cp4 zenon_TY_bd)\/((cp5 zenon_TY_bd)\/(cp3 zenon_TY_bd)))) -> (cp5 zenon_TY_bd) -> False). % 12.56/12.81 do 1 intro. intros zenon_H2b zenon_H1c. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H2b). zenon_intro zenon_H1f. zenon_intro zenon_H2c. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H2c). zenon_intro zenon_H1e. zenon_intro zenon_H2d. % 12.56/12.81 exact (zenon_H1e zenon_H1c). % 12.56/12.81 (* end of lemma zenon_L5_ *) % 12.56/12.81 assert (zenon_L6_ : forall (zenon_TY_z : zenon_U), (~((cp4 zenon_TY_z)\/((cp5 zenon_TY_z)\/(cp3 zenon_TY_z)))) -> (cp4 zenon_TY_z) -> False). % 12.56/12.81 do 1 intro. intros zenon_H2e zenon_H21. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H2e). zenon_intro zenon_H23. zenon_intro zenon_H2f. % 12.56/12.81 exact (zenon_H23 zenon_H21). % 12.56/12.81 (* end of lemma zenon_L6_ *) % 12.56/12.81 assert (zenon_L7_ : forall (zenon_TY_bd : zenon_U), (~((cp2 zenon_TY_bd)\/((cp4 zenon_TY_bd)\/((cp5 zenon_TY_bd)\/(cp3 zenon_TY_bd))))) -> (cp5 zenon_TY_bd) -> False). % 12.56/12.81 do 1 intro. intros zenon_H30 zenon_H1c. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H30). zenon_intro zenon_H31. zenon_intro zenon_H2b. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H2b). zenon_intro zenon_H1f. zenon_intro zenon_H2c. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H2c). zenon_intro zenon_H1e. zenon_intro zenon_H2d. % 12.56/12.81 exact (zenon_H1e zenon_H1c). % 12.56/12.81 (* end of lemma zenon_L7_ *) % 12.56/12.81 assert (zenon_L8_ : forall (zenon_TY_bm : zenon_U), (~((cp2 zenon_TY_bm)\/((cp4 zenon_TY_bm)\/((cp5 zenon_TY_bm)\/(cp3 zenon_TY_bm))))) -> (cp3 zenon_TY_bm) -> False). % 12.56/12.81 do 1 intro. intros zenon_H32 zenon_H25. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H32). zenon_intro zenon_H33. zenon_intro zenon_H24. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H24). zenon_intro zenon_H28. zenon_intro zenon_H27. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H27). zenon_intro zenon_H2a. zenon_intro zenon_H29. % 12.56/12.81 exact (zenon_H29 zenon_H25). % 12.56/12.81 (* end of lemma zenon_L8_ *) % 12.56/12.81 assert (zenon_L9_ : forall (zenon_TY_z : zenon_U), (~((cp2 zenon_TY_z)\/((cp4 zenon_TY_z)\/((cp5 zenon_TY_z)\/(cp3 zenon_TY_z))))) -> (cp4 zenon_TY_z) -> False). % 12.56/12.81 do 1 intro. intros zenon_H34 zenon_H21. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H34). zenon_intro zenon_H15. zenon_intro zenon_H2e. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H2e). zenon_intro zenon_H23. zenon_intro zenon_H2f. % 12.56/12.81 exact (zenon_H23 zenon_H21). % 12.56/12.81 (* end of lemma zenon_L9_ *) % 12.56/12.81 assert (zenon_L10_ : forall (zenon_TY_y : zenon_U), (~((cp2 zenon_TY_y)\/((cp4 zenon_TY_y)\/((cp5 zenon_TY_y)\/(cp3 zenon_TY_y))))) -> (cp2 zenon_TY_y) -> False). % 12.56/12.81 do 1 intro. intros zenon_H35 zenon_H16. % 12.56/12.81 apply (zenon_notor_s _ _ zenon_H35). zenon_intro zenon_H37. zenon_intro zenon_H36. % 12.64/12.81 exact (zenon_H37 zenon_H16). % 12.64/12.81 (* end of lemma zenon_L10_ *) % 12.64/12.81 generalize (axiom_2 (i2003_11_14_17_19_24236)). zenon_intro zenon_H38. % 12.64/12.81 apply (zenon_equiv_s _ _ zenon_H38); [ zenon_intro zenon_H3b; zenon_intro zenon_H3a | zenon_intro axiom_7; zenon_intro zenon_H39 ]. % 12.64/12.81 exact (zenon_H3b axiom_7). % 12.64/12.81 apply (zenon_and_s _ _ zenon_H39). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H42). zenon_intro zenon_H45. zenon_intro zenon_H44. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H46). zenon_intro zenon_H49. zenon_intro zenon_H48. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 12.64/12.81 elim zenon_H3f. zenon_intro zenon_TY_z. zenon_intro zenon_H4c. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H4c). zenon_intro zenon_H4e. zenon_intro zenon_H4d. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H21. zenon_intro zenon_H4f. % 12.64/12.81 elim zenon_H43. zenon_intro zenon_TY_y. zenon_intro zenon_H50. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H50). zenon_intro zenon_H52. zenon_intro zenon_H51. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H16. zenon_intro zenon_H53. % 12.64/12.81 elim zenon_H45. zenon_intro zenon_TY_bd. zenon_intro zenon_H54. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H54). zenon_intro zenon_H55. zenon_intro zenon_H1c. % 12.64/12.81 elim zenon_H47. zenon_intro zenon_TY_bm. zenon_intro zenon_H56. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_H58. zenon_intro zenon_H57. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H57). zenon_intro zenon_H59. zenon_intro zenon_H25. % 12.64/12.81 elim zenon_H49. zenon_intro zenon_TY_dm. zenon_intro zenon_H5b. % 12.64/12.81 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 12.64/12.81 generalize (axiom_3 zenon_TY_y). zenon_intro zenon_H5e. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H5e); [ zenon_intro zenon_H5f | zenon_intro zenon_H35 ]. % 12.64/12.81 generalize (axiom_3 zenon_TY_z). zenon_intro zenon_H60. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H61 | zenon_intro zenon_H34 ]. % 12.64/12.81 generalize (axiom_3 zenon_TY_bm). zenon_intro zenon_H62. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H62); [ zenon_intro zenon_H63 | zenon_intro zenon_H32 ]. % 12.64/12.81 generalize (axiom_3 zenon_TY_bd). zenon_intro zenon_H64. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H65 | zenon_intro zenon_H30 ]. % 12.64/12.81 generalize (axiom_4 zenon_TY_z). zenon_intro zenon_H66. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H66); [ zenon_intro zenon_H15 | zenon_intro zenon_H2e ]. % 12.64/12.81 generalize (axiom_4 zenon_TY_bd). zenon_intro zenon_H67. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H67); [ zenon_intro zenon_H31 | zenon_intro zenon_H2b ]. % 12.64/12.81 generalize (axiom_4 zenon_TY_bm). zenon_intro zenon_H68. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H68); [ zenon_intro zenon_H33 | zenon_intro zenon_H24 ]. % 12.64/12.81 generalize (axiom_5 zenon_TY_z). zenon_intro zenon_H69. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H69); [ zenon_intro zenon_H6a | zenon_intro zenon_H20 ]. % 12.64/12.81 generalize (axiom_5 zenon_TY_bd). zenon_intro zenon_H6b. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_H2d | zenon_intro zenon_H1b ]. % 12.64/12.81 generalize (zenon_H4b zenon_TY_bd). zenon_intro zenon_H6c. % 12.64/12.81 generalize (zenon_H6c zenon_TY_bm). zenon_intro zenon_H6d. % 12.64/12.81 generalize (axiom_6 zenon_TY_bd). zenon_intro zenon_H6e. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H6e); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 12.64/12.81 generalize (zenon_H6d zenon_TY_dm). zenon_intro zenon_H6f. % 12.64/12.81 generalize (cp3_substitution_1 zenon_TY_bm). zenon_intro zenon_H70. % 12.64/12.81 generalize (cp2_substitution_1 zenon_TY_y). zenon_intro zenon_H71. % 12.64/12.81 generalize (zenon_H6f zenon_TY_z). zenon_intro zenon_H72. % 12.64/12.81 generalize (zenon_H70 zenon_TY_bd). zenon_intro zenon_H73. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H73); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H75); [ zenon_intro zenon_H76 | zenon_intro zenon_H29 ]. % 12.64/12.81 generalize (cp4_substitution_1 zenon_TY_z). zenon_intro zenon_H77. % 12.64/12.81 generalize (zenon_H71 zenon_TY_bm). zenon_intro zenon_H78. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H78); [ zenon_intro zenon_H7a | zenon_intro zenon_H79 ]. % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H7a); [ zenon_intro zenon_H7b | zenon_intro zenon_H37 ]. % 12.64/12.81 generalize (zenon_H71 zenon_TY_bd). zenon_intro zenon_H7c. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H7f | zenon_intro zenon_H37 ]. % 12.64/12.81 cut ((cp1 zenon_TY_dm) = (cp1 zenon_TY_y)). % 12.64/12.81 intro zenon_D_pnotp. % 12.64/12.81 apply zenon_H5f. % 12.64/12.81 rewrite <- zenon_D_pnotp. % 12.64/12.81 exact zenon_H5c. % 12.64/12.81 cut ((zenon_TY_dm = zenon_TY_y)); [idtac | apply NNPP; zenon_intro zenon_H80]. % 12.64/12.81 congruence. % 12.64/12.81 generalize (zenon_H70 zenon_TY_z). zenon_intro zenon_H81. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H81); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H83); [ zenon_intro zenon_H84 | zenon_intro zenon_H29 ]. % 12.64/12.81 cut ((cp1 zenon_TY_dm) = (cp1 zenon_TY_z)). % 12.64/12.81 intro zenon_D_pnotp. % 12.64/12.81 apply zenon_H61. % 12.64/12.81 rewrite <- zenon_D_pnotp. % 12.64/12.81 exact zenon_H5c. % 12.64/12.81 cut ((zenon_TY_dm = zenon_TY_z)); [idtac | apply NNPP; zenon_intro zenon_H85]. % 12.64/12.81 congruence. % 12.64/12.81 cut ((cp1 zenon_TY_dm) = (cp1 zenon_TY_bm)). % 12.64/12.81 intro zenon_D_pnotp. % 12.64/12.81 apply zenon_H63. % 12.64/12.81 rewrite <- zenon_D_pnotp. % 12.64/12.81 exact zenon_H5c. % 12.64/12.81 cut ((zenon_TY_dm = zenon_TY_bm)); [idtac | apply NNPP; zenon_intro zenon_H86]. % 12.64/12.81 congruence. % 12.64/12.81 cut ((cp1 zenon_TY_dm) = (cp1 zenon_TY_bd)). % 12.64/12.81 intro zenon_D_pnotp. % 12.64/12.81 apply zenon_H65. % 12.64/12.81 rewrite <- zenon_D_pnotp. % 12.64/12.81 exact zenon_H5c. % 12.64/12.81 cut ((zenon_TY_dm = zenon_TY_bd)); [idtac | apply NNPP; zenon_intro zenon_H87]. % 12.64/12.81 congruence. % 12.64/12.81 generalize (zenon_H72 zenon_TY_y). zenon_intro zenon_H88. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H88); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 12.64/12.81 exact (zenon_H8c zenon_H55). % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_H8e | zenon_intro zenon_H8d ]. % 12.64/12.81 exact (zenon_H8e zenon_H58). % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H8d); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 12.64/12.81 exact (zenon_H90 zenon_H5d). % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H8f); [ zenon_intro zenon_H92 | zenon_intro zenon_H91 ]. % 12.64/12.81 exact (zenon_H92 zenon_H4e). % 12.64/12.81 exact (zenon_H91 zenon_H52). % 12.64/12.81 apply (zenon_or_s _ _ zenon_H89); [ zenon_intro zenon_H94 | zenon_intro zenon_H93 ]. % 12.64/12.81 apply zenon_H76. apply sym_equal. exact zenon_H94. % 12.64/12.81 apply (zenon_or_s _ _ zenon_H93); [ zenon_intro zenon_H96 | zenon_intro zenon_H95 ]. % 12.64/12.81 apply zenon_H87. apply sym_equal. exact zenon_H96. % 12.64/12.81 apply (zenon_or_s _ _ zenon_H95); [ zenon_intro zenon_H98 | zenon_intro zenon_H97 ]. % 12.64/12.81 generalize (zenon_H77 zenon_TY_bd). zenon_intro zenon_H99. % 12.64/12.81 apply (zenon_imply_s _ _ zenon_H99); [ zenon_intro zenon_H9b | zenon_intro zenon_H9a ]. % 12.64/12.81 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H9c | zenon_intro zenon_H23 ]. % 12.64/12.81 apply zenon_H9c. apply sym_equal. exact zenon_H98. % 12.64/12.81 exact (zenon_H23 zenon_H21). % 12.64/12.81 exact (zenon_H1f zenon_H9a). % 12.64/12.81 apply (zenon_or_s _ _ zenon_H97); [ zenon_intro zenon_H9e | zenon_intro zenon_H9d ]. % 12.64/12.81 apply zenon_H7f. apply sym_equal. exact zenon_H9e. % 12.64/12.81 apply (zenon_or_s _ _ zenon_H9d); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H9f ]. % 12.64/12.81 apply zenon_H86. apply sym_equal. exact zenon_Ha0. % 12.64/12.81 apply (zenon_or_s _ _ zenon_H9f); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1 ]. % 12.64/12.81 exact (zenon_H84 zenon_Ha2). % 12.64/12.81 apply (zenon_or_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha3 ]. % 12.64/12.81 apply zenon_H7b. apply sym_equal. exact zenon_Ha4. % 12.64/12.81 apply (zenon_or_s _ _ zenon_Ha3); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha5 ]. % 12.64/12.81 exact (zenon_H85 zenon_Ha6). % 12.64/12.81 apply (zenon_or_s _ _ zenon_Ha5); [ zenon_intro zenon_Ha7 | zenon_intro zenon_H17 ]. % 12.64/12.81 exact (zenon_H80 zenon_Ha7). % 12.64/12.81 apply (zenon_L1_ zenon_TY_y zenon_TY_z); trivial. % 12.64/12.81 exact (zenon_H29 zenon_H25). % 12.64/12.81 exact (zenon_H6a zenon_H82). % 12.64/12.81 exact (zenon_H37 zenon_H16). % 12.64/12.81 exact (zenon_H31 zenon_H7d). % 12.64/12.81 exact (zenon_H37 zenon_H16). % 12.64/12.81 exact (zenon_H33 zenon_H79). % 12.64/12.81 exact (zenon_H29 zenon_H25). % 12.64/12.81 exact (zenon_H2d zenon_H74). % 12.64/12.81 exact (zenon_H1e zenon_H1c). % 12.64/12.81 apply (zenon_L2_ zenon_TY_bd); trivial. % 12.64/12.81 apply (zenon_L3_ zenon_TY_z); trivial. % 12.64/12.81 apply (zenon_L4_ zenon_TY_bm); trivial. % 12.64/12.81 apply (zenon_L5_ zenon_TY_bd); trivial. % 12.64/12.81 apply (zenon_L6_ zenon_TY_z); trivial. % 12.64/12.81 apply (zenon_L7_ zenon_TY_bd); trivial. % 12.64/12.81 apply (zenon_L8_ zenon_TY_bm); trivial. % 12.64/12.81 apply (zenon_L9_ zenon_TY_z); trivial. % 12.64/12.81 apply (zenon_L10_ zenon_TY_y); trivial. % 12.64/12.81 Qed. % 12.64/12.81 % SZS output end Proof % 12.64/12.81 (* END-PROOF *) % 12.64/12.81 nodes searched: 156518 % 12.64/12.81 max branch formulas: 34459 % 12.64/12.81 proof nodes created: 402 % 12.64/12.81 formulas created: 924815 % 12.64/12.81 %------------------------------------------------------------------------------