%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:32:45 PM UTC 2026 % Result : Theorem 0.38s 0.63s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.09/0.36 % Computer : n026.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 5 21:14:26 UTC 2026 % 0.09/0.36 % CPUTime : % 0.38/0.63 (* PROOF-FOUND *) % 0.38/0.63 % SZS status Theorem % 0.38/0.63 (* BEGIN-PROOF *) % 0.38/0.63 % SZS output start Proof % 0.38/0.63 Theorem main : (~(exists X : zenon_U, (~((~(forall Y : zenon_U, ((~(r1 X Y))\/(p5 Y))))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p11 X))/\((~(p111 X))/\(p110 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p11 X)/\((~(p111 X))/\(p110 X))))))))\/(~((~(p110 Y))/\(p109 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p10 X))/\((~(p110 X))/\(p109 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p10 X)/\((~(p110 X))/\(p109 X))))))))\/(~((~(p109 Y))/\(p108 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p9 X))/\((~(p109 X))/\(p108 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p9 X)/\((~(p109 X))/\(p108 X))))))))\/(~((~(p108 Y))/\(p107 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p8 X))/\((~(p108 X))/\(p107 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p8 X)/\((~(p108 X))/\(p107 X))))))))\/(~((~(p107 Y))/\(p106 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p7 X))/\((~(p107 X))/\(p106 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p7 X)/\((~(p107 X))/\(p106 X))))))))\/(~((~(p106 Y))/\(p105 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p11 X))\/(~(p110 X)))))\/(p11 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p11 X)\/(~(p110 X)))))\/(~(p11 Y))))\/(~(p110 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p10 X))\/(~(p109 X)))))\/(p10 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p10 X)\/(~(p109 X)))))\/(~(p10 Y))))\/(~(p109 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p9 X))\/(~(p108 X)))))\/(p9 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p9 X)\/(~(p108 X)))))\/(~(p9 Y))))\/(~(p108 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p8 X))\/(~(p107 X)))))\/(p8 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p8 X)\/(~(p107 X)))))\/(~(p8 Y))))\/(~(p107 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p7 X))\/(~(p106 X)))))\/(p7 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p7 X)\/(~(p106 X)))))\/(~(p7 Y))))\/(~(p106 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p110 Y)\/(~(p111 Y)))/\(((p109 Y)\/(~(p110 Y)))/\(((p108 Y)\/(~(p109 Y)))/\(((p107 Y)\/(~(p108 Y)))/\(((p106 Y)\/(~(p107 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))))))))))/\((~(p101 X))/\(p100 X)))))))). % 0.38/0.63 Proof. % 0.38/0.63 assert (zenon_L1_ : forall (zenon_TX_h : zenon_U) (zenon_TX_i : zenon_U) (zenon_TX_j : zenon_U), (r1 zenon_TX_j zenon_TX_i) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_h)) -> (r1 zenon_TX_i zenon_TX_h) -> False). % 0.38/0.63 do 3 intro. intros zenon_H3 zenon_H4 zenon_H5 zenon_H6. % 0.38/0.63 elim (classic ((~(zenon_TX_j = zenon_TX_i))/\(~(r1 zenon_TX_j zenon_TX_i)))); [ zenon_intro zenon_Ha | zenon_intro zenon_Hb ]. % 0.38/0.63 apply (zenon_and_s _ _ zenon_Ha). zenon_intro zenon_Hd. zenon_intro zenon_Hc. % 0.38/0.63 exact (zenon_Hc zenon_H3). % 0.38/0.63 cut ((r1 zenon_TX_i zenon_TX_h) = (r1 zenon_TX_j zenon_TX_h)). % 0.38/0.63 intro zenon_D_pnotp. % 0.38/0.63 apply zenon_H5. % 0.38/0.63 rewrite <- zenon_D_pnotp. % 0.38/0.63 exact zenon_H6. % 0.38/0.63 cut ((zenon_TX_h = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_He]. % 0.38/0.63 cut ((zenon_TX_i = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Hf]. % 0.38/0.63 congruence. % 0.38/0.63 apply (zenon_notand_s _ _ zenon_Hb); [ zenon_intro zenon_H11 | zenon_intro zenon_H10 ]. % 0.38/0.63 apply zenon_H11. zenon_intro zenon_H12. % 0.38/0.63 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_i = zenon_TX_j)). % 0.38/0.63 intro zenon_D_pnotp. % 0.38/0.63 apply zenon_Hf. % 0.38/0.63 rewrite <- zenon_D_pnotp. % 0.38/0.63 exact zenon_H13. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_i)); [idtac | apply NNPP; zenon_intro zenon_Hd]. % 0.38/0.63 congruence. % 0.38/0.63 exact (zenon_Hd zenon_H12). % 0.38/0.63 apply zenon_H14. apply refl_equal. % 0.38/0.63 apply zenon_H14. apply refl_equal. % 0.38/0.63 apply zenon_H10. zenon_intro zenon_H3. % 0.38/0.63 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 0.38/0.63 generalize (zenon_H15 zenon_TX_i). zenon_intro zenon_H16. % 0.38/0.63 generalize (zenon_H16 zenon_TX_h). zenon_intro zenon_H17. % 0.38/0.63 apply (zenon_imply_s _ _ zenon_H17); [ zenon_intro zenon_Hc | zenon_intro zenon_H18 ]. % 0.38/0.63 exact (zenon_Hc zenon_H3). % 0.38/0.63 apply (zenon_imply_s _ _ zenon_H18); [ zenon_intro zenon_H1a | zenon_intro zenon_H19 ]. % 0.38/0.63 exact (zenon_H1a zenon_H6). % 0.38/0.63 exact (zenon_H5 zenon_H19). % 0.38/0.63 apply zenon_He. apply refl_equal. % 0.38/0.63 (* end of lemma zenon_L1_ *) % 0.38/0.63 assert (zenon_L2_ : forall (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TX_i : zenon_U) (zenon_TX_j : zenon_U), (r1 zenon_TX_j zenon_TX_i) -> (r1 zenon_TX_i zenon_TX_h) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_bd)) -> (r1 zenon_TX_h zenon_TX_bd) -> False). % 0.38/0.63 do 4 intro. intros zenon_H3 zenon_H6 zenon_H4 zenon_H1b zenon_H1c. % 0.38/0.63 elim (classic ((~(zenon_TX_j = zenon_TX_h))/\(~(r1 zenon_TX_j zenon_TX_h)))); [ zenon_intro zenon_H1e | zenon_intro zenon_H1f ]. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H1e). zenon_intro zenon_H20. zenon_intro zenon_H5. % 0.38/0.63 apply (zenon_L1_ zenon_TX_h zenon_TX_i zenon_TX_j); trivial. % 0.38/0.63 cut ((r1 zenon_TX_h zenon_TX_bd) = (r1 zenon_TX_j zenon_TX_bd)). % 0.38/0.63 intro zenon_D_pnotp. % 0.38/0.63 apply zenon_H1b. % 0.38/0.63 rewrite <- zenon_D_pnotp. % 0.38/0.63 exact zenon_H1c. % 0.38/0.63 cut ((zenon_TX_bd = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H21]. % 0.38/0.63 cut ((zenon_TX_h = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H22]. % 0.38/0.63 congruence. % 0.38/0.63 apply (zenon_notand_s _ _ zenon_H1f); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 0.38/0.63 apply zenon_H24. zenon_intro zenon_H25. % 0.38/0.63 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_h = zenon_TX_j)). % 0.38/0.63 intro zenon_D_pnotp. % 0.38/0.63 apply zenon_H22. % 0.38/0.63 rewrite <- zenon_D_pnotp. % 0.38/0.63 exact zenon_H13. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_H20]. % 0.38/0.63 congruence. % 0.38/0.63 exact (zenon_H20 zenon_H25). % 0.38/0.63 apply zenon_H14. apply refl_equal. % 0.38/0.63 apply zenon_H14. apply refl_equal. % 0.38/0.63 apply zenon_H23. zenon_intro zenon_H19. % 0.38/0.63 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 0.38/0.63 generalize (zenon_H15 zenon_TX_h). zenon_intro zenon_H26. % 0.38/0.63 generalize (zenon_H26 zenon_TX_bd). zenon_intro zenon_H27. % 0.38/0.63 apply (zenon_imply_s _ _ zenon_H27); [ zenon_intro zenon_H5 | zenon_intro zenon_H28 ]. % 0.38/0.63 exact (zenon_H5 zenon_H19). % 0.38/0.63 apply (zenon_imply_s _ _ zenon_H28); [ zenon_intro zenon_H2a | zenon_intro zenon_H29 ]. % 0.38/0.63 exact (zenon_H2a zenon_H1c). % 0.38/0.63 exact (zenon_H1b zenon_H29). % 0.38/0.63 apply zenon_H21. apply refl_equal. % 0.38/0.63 (* end of lemma zenon_L2_ *) % 0.38/0.63 apply NNPP. intro zenon_G. % 0.38/0.63 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z))))))); [ zenon_intro zenon_H4 | zenon_intro zenon_H2b ]. % 0.38/0.63 apply zenon_G. zenon_intro zenon_H2c. % 0.38/0.63 elim zenon_H2c. zenon_intro zenon_TX_j. zenon_intro zenon_H2d. % 0.38/0.63 apply (zenon_notor_s _ _ zenon_H2d). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 0.38/0.63 apply zenon_H2e. zenon_intro zenon_H30. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H30). zenon_intro zenon_H32. zenon_intro zenon_H31. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H31). zenon_intro zenon_H34. zenon_intro zenon_H33. % 0.38/0.63 apply zenon_H2f. zenon_intro zenon_H35. % 0.38/0.63 generalize (zenon_H32 zenon_TX_j). zenon_intro zenon_H36. % 0.38/0.63 apply (zenon_or_s _ _ zenon_H36); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 0.38/0.63 generalize (reflexivity zenon_TX_j). zenon_intro zenon_H39. % 0.38/0.63 exact (zenon_H38 zenon_H39). % 0.38/0.63 apply (zenon_and_s _ _ zenon_H37). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H42). zenon_intro zenon_H45. zenon_intro zenon_H44. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H46). zenon_intro zenon_H49. zenon_intro zenon_H48. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 0.38/0.63 apply (zenon_or_s _ _ zenon_H4d); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H4f). zenon_intro zenon_H51. zenon_intro zenon_H50. % 0.38/0.63 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_j X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))) zenon_H51); [ zenon_intro zenon_H52; idtac ]. % 0.38/0.63 elim zenon_H52. zenon_intro zenon_TX_i. zenon_intro zenon_H53. % 0.38/0.63 apply (zenon_notor_s _ _ zenon_H53). zenon_intro zenon_H10. zenon_intro zenon_H54. % 0.38/0.63 apply zenon_H54. zenon_intro zenon_H55. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H57. zenon_intro zenon_H56. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.38/0.63 apply zenon_H10. zenon_intro zenon_H3. % 0.38/0.63 generalize (zenon_H32 zenon_TX_i). zenon_intro zenon_H5a. % 0.38/0.63 apply (zenon_or_s _ _ zenon_H5a); [ zenon_intro zenon_Hc | zenon_intro zenon_H5b ]. % 0.38/0.63 exact (zenon_Hc zenon_H3). % 0.38/0.63 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H5c). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H5e). zenon_intro zenon_H61. zenon_intro zenon_H60. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H60). zenon_intro zenon_H63. zenon_intro zenon_H62. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H65. zenon_intro zenon_H64. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H64). zenon_intro zenon_H67. zenon_intro zenon_H66. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H66). zenon_intro zenon_H69. zenon_intro zenon_H68. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H68). zenon_intro zenon_H6b. zenon_intro zenon_H6a. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H6a). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 0.38/0.63 apply (zenon_or_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H6f). zenon_intro zenon_H71. zenon_intro zenon_H70. % 0.38/0.63 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_i X))\/(~((p3 X)/\((~(p103 X))/\(p102 X)))))) zenon_H70); [ zenon_intro zenon_H72; idtac ]. % 0.38/0.63 elim zenon_H72. zenon_intro zenon_TX_h. zenon_intro zenon_H73. % 0.38/0.63 apply (zenon_notor_s _ _ zenon_H73). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.38/0.63 apply zenon_H74. zenon_intro zenon_H76. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H76). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H77). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 0.38/0.63 apply zenon_H75. zenon_intro zenon_H6. % 0.38/0.63 generalize (zenon_H32 zenon_TX_h). zenon_intro zenon_H7b. % 0.38/0.63 apply (zenon_or_s _ _ zenon_H7b); [ zenon_intro zenon_H5 | zenon_intro zenon_H7c ]. % 0.38/0.63 apply (zenon_L1_ zenon_TX_h zenon_TX_i zenon_TX_j); trivial. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H7c). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H7d). zenon_intro zenon_H80. zenon_intro zenon_H7f. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H7f). zenon_intro zenon_H82. zenon_intro zenon_H81. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H81). zenon_intro zenon_H84. zenon_intro zenon_H83. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H83). zenon_intro zenon_H86. zenon_intro zenon_H85. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H85). zenon_intro zenon_H88. zenon_intro zenon_H87. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H87). zenon_intro zenon_H8a. zenon_intro zenon_H89. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H89). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 0.38/0.63 apply (zenon_or_s _ _ zenon_H8c); [ zenon_intro zenon_H8e | zenon_intro zenon_H8d ]. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H8e). zenon_intro zenon_H90. zenon_intro zenon_H8f. % 0.38/0.63 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_h X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))) zenon_H90); [ zenon_intro zenon_H91; idtac ]. % 0.38/0.63 elim zenon_H91. zenon_intro zenon_TX_bd. zenon_intro zenon_H92. % 0.38/0.63 apply (zenon_notor_s _ _ zenon_H92). zenon_intro zenon_H94. zenon_intro zenon_H93. % 0.38/0.63 apply zenon_H93. zenon_intro zenon_H95. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H95). zenon_intro zenon_H97. zenon_intro zenon_H96. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H96). zenon_intro zenon_H99. zenon_intro zenon_H98. % 0.38/0.63 apply zenon_H94. zenon_intro zenon_H1c. % 0.38/0.63 generalize (zenon_H32 zenon_TX_bd). zenon_intro zenon_H9a. % 0.38/0.63 apply (zenon_or_s _ _ zenon_H9a); [ zenon_intro zenon_H1b | zenon_intro zenon_H9b ]. % 0.38/0.63 apply (zenon_L2_ zenon_TX_bd zenon_TX_h zenon_TX_i zenon_TX_j); trivial. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_H9d. zenon_intro zenon_H9c. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H9c). zenon_intro zenon_H9f. zenon_intro zenon_H9e. % 0.38/0.63 apply (zenon_and_s _ _ zenon_H9e). zenon_intro zenon_Ha1. zenon_intro zenon_Ha0. % 0.38/0.63 apply (zenon_and_s _ _ zenon_Ha0). zenon_intro zenon_Ha3. zenon_intro zenon_Ha2. % 0.38/0.63 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Ha5. zenon_intro zenon_Ha4. % 0.38/0.63 apply (zenon_and_s _ _ zenon_Ha4). zenon_intro zenon_Ha7. zenon_intro zenon_Ha6. % 0.38/0.63 apply (zenon_and_s _ _ zenon_Ha6). zenon_intro zenon_Ha9. zenon_intro zenon_Ha8. % 0.38/0.63 apply (zenon_or_s _ _ zenon_Ha9); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 0.38/0.63 apply (zenon_and_s _ _ zenon_Hab). zenon_intro zenon_Had. zenon_intro zenon_Hac. % 0.38/0.63 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_bd X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))) zenon_Had); [ zenon_intro zenon_Hae; idtac ]. % 0.38/0.63 elim zenon_Hae. zenon_intro zenon_TX_gt. zenon_intro zenon_Hb0. % 0.38/0.63 apply (zenon_notor_s _ _ zenon_Hb0). zenon_intro zenon_Hb2. zenon_intro zenon_Hb1. % 0.38/0.63 apply zenon_Hb1. zenon_intro zenon_Hb3. % 0.38/0.63 apply (zenon_and_s _ _ zenon_Hb3). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 0.38/0.63 apply zenon_Hb2. zenon_intro zenon_Hb6. % 0.38/0.63 generalize (zenon_H35 zenon_TX_gt). zenon_intro zenon_Hb7. % 0.38/0.63 apply (zenon_or_s _ _ zenon_Hb7); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hb8 ]. % 0.38/0.63 elim (classic ((~(zenon_TX_j = zenon_TX_bd))/\(~(r1 zenon_TX_j zenon_TX_bd)))); [ zenon_intro zenon_Hba | zenon_intro zenon_Hbb ]. % 0.38/0.63 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_Hbc. zenon_intro zenon_H1b. % 0.38/0.63 apply (zenon_L2_ zenon_TX_bd zenon_TX_h zenon_TX_i zenon_TX_j); trivial. % 0.38/0.63 cut ((r1 zenon_TX_bd zenon_TX_gt) = (r1 zenon_TX_j zenon_TX_gt)). % 0.38/0.63 intro zenon_D_pnotp. % 0.38/0.63 apply zenon_Hb9. % 0.38/0.63 rewrite <- zenon_D_pnotp. % 0.38/0.63 exact zenon_Hb6. % 0.38/0.63 cut ((zenon_TX_gt = zenon_TX_gt)); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 0.38/0.63 cut ((zenon_TX_bd = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 0.38/0.63 congruence. % 0.38/0.63 apply (zenon_notand_s _ _ zenon_Hbb); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Hbf ]. % 0.38/0.63 apply zenon_Hc0. zenon_intro zenon_Hc1. % 0.38/0.63 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_bd = zenon_TX_j)). % 0.38/0.63 intro zenon_D_pnotp. % 0.38/0.63 apply zenon_Hbe. % 0.38/0.63 rewrite <- zenon_D_pnotp. % 0.38/0.63 exact zenon_H13. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 0.38/0.63 cut ((zenon_TX_j = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 0.38/0.63 congruence. % 0.38/0.63 exact (zenon_Hbc zenon_Hc1). % 0.38/0.63 apply zenon_H14. apply refl_equal. % 0.38/0.63 apply zenon_H14. apply refl_equal. % 0.38/0.63 apply zenon_Hbf. zenon_intro zenon_H29. % 0.38/0.63 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 0.38/0.63 generalize (zenon_H15 zenon_TX_bd). zenon_intro zenon_Hc2. % 0.38/0.63 generalize (zenon_Hc2 zenon_TX_gt). zenon_intro zenon_Hc3. % 0.38/0.63 apply (zenon_imply_s _ _ zenon_Hc3); [ zenon_intro zenon_H1b | zenon_intro zenon_Hc4 ]. % 0.38/0.63 exact (zenon_H1b zenon_H29). % 0.38/0.63 apply (zenon_imply_s _ _ zenon_Hc4); [ zenon_intro zenon_Hc6 | zenon_intro zenon_Hc5 ]. % 0.38/0.63 exact (zenon_Hc6 zenon_Hb6). % 0.38/0.63 exact (zenon_Hb9 zenon_Hc5). % 0.38/0.63 apply zenon_Hbd. apply refl_equal. % 0.38/0.63 exact (zenon_Hb5 zenon_Hb8). % 0.38/0.63 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_Hc8 | zenon_intro zenon_Hc7 ]. % 0.38/0.63 exact (zenon_Hc8 zenon_H99). % 0.38/0.63 exact (zenon_Hc7 zenon_H98). % 0.38/0.63 apply (zenon_notand_s _ _ zenon_H8d); [ zenon_intro zenon_Hca | zenon_intro zenon_Hc9 ]. % 0.38/0.63 exact (zenon_Hca zenon_H7a). % 0.38/0.63 exact (zenon_Hc9 zenon_H79). % 0.38/0.63 apply (zenon_notand_s _ _ zenon_H6e); [ zenon_intro zenon_Hcc | zenon_intro zenon_Hcb ]. % 0.38/0.63 exact (zenon_Hcc zenon_H59). % 0.38/0.63 exact (zenon_Hcb zenon_H58). % 0.38/0.63 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_Hce | zenon_intro zenon_Hcd ]. % 0.38/0.63 exact (zenon_Hce zenon_H34). % 0.38/0.63 exact (zenon_Hcd zenon_H33). % 0.38/0.63 apply zenon_H2b. zenon_intro zenon_Tx_hz. apply NNPP. zenon_intro zenon_Hd0. % 0.38/0.63 apply zenon_Hd0. zenon_intro zenon_Ty_ib. apply NNPP. zenon_intro zenon_Hd2. % 0.38/0.63 apply zenon_Hd2. zenon_intro zenon_Tz_id. apply NNPP. zenon_intro zenon_Hd4. % 0.38/0.63 apply (zenon_notimply_s _ _ zenon_Hd4). zenon_intro zenon_Hd6. zenon_intro zenon_Hd5. % 0.38/0.63 apply (zenon_notimply_s _ _ zenon_Hd5). zenon_intro zenon_Hd8. zenon_intro zenon_Hd7. % 0.38/0.63 generalize (transitivity zenon_Tx_hz). zenon_intro zenon_Hd9. % 0.38/0.63 generalize (zenon_Hd9 zenon_Ty_ib). zenon_intro zenon_Hda. % 0.38/0.63 generalize (zenon_Hda zenon_Tz_id). zenon_intro zenon_Hdb. % 0.38/0.63 apply (zenon_imply_s _ _ zenon_Hdb); [ zenon_intro zenon_Hdd | zenon_intro zenon_Hdc ]. % 0.38/0.63 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_Hdf | zenon_intro zenon_Hde ]. % 0.38/0.63 exact (zenon_Hdf zenon_Hd6). % 0.38/0.63 exact (zenon_Hde zenon_Hd8). % 0.38/0.63 exact (zenon_Hd7 zenon_Hdc). % 0.38/0.63 Qed. % 0.38/0.63 % SZS output end Proof % 0.38/0.63 (* END-PROOF *) % 0.38/0.63 nodes searched: 4862 % 0.38/0.63 max branch formulas: 2450 % 0.38/0.63 proof nodes created: 546 % 0.38/0.63 formulas created: 21836 % 0.38/0.63 %------------------------------------------------------------------------------