%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : ALG043+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n023.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 : Thu Jul 14 18:29:04 EDT 2022 % Result : Theorem 0.43s 0.59s % Output : Proof 0.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG043+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n023.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 : Wed Jun 8 07:15:23 EDT 2022 % 0.12/0.33 % CPUTime : % 0.43/0.59 (* PROOF-FOUND *) % 0.43/0.59 % SZS status Theorem % 0.43/0.59 (* BEGIN-PROOF *) % 0.43/0.59 % SZS output start Proof % 0.43/0.59 Theorem co1 : (((((op (e0) (e0)) = (e0))/\(((op (e1) (e1)) = (e0))/\(((op (e2) (e2)) = (e0))/\((op (e3) (e3)) = (e0)))))\/((((op (e0) (e0)) = (e1))/\(((op (e1) (e1)) = (e1))/\(((op (e2) (e2)) = (e1))/\((op (e3) (e3)) = (e1)))))\/((((op (e0) (e0)) = (e2))/\(((op (e1) (e1)) = (e2))/\(((op (e2) (e2)) = (e2))/\((op (e3) (e3)) = (e2)))))\/(((op (e0) (e0)) = (e3))/\(((op (e1) (e1)) = (e3))/\(((op (e2) (e2)) = (e3))/\((op (e3) (e3)) = (e3))))))))/\((((op (e0) (e0)) = (e0))\/(((op (e0) (e0)) = (e1))\/(((op (e0) (e0)) = (e2))\/((op (e0) (e0)) = (e3)))))/\((((op (e0) (e1)) = (e0))\/(((op (e0) (e1)) = (e1))\/(((op (e0) (e1)) = (e2))\/((op (e0) (e1)) = (e3)))))/\((((op (e0) (e2)) = (e0))\/(((op (e0) (e2)) = (e1))\/(((op (e0) (e2)) = (e2))\/((op (e0) (e2)) = (e3)))))/\((((op (e0) (e3)) = (e0))\/(((op (e0) (e3)) = (e1))\/(((op (e0) (e3)) = (e2))\/((op (e0) (e3)) = (e3)))))/\((((op (e1) (e0)) = (e0))\/(((op (e1) (e0)) = (e1))\/(((op (e1) (e0)) = (e2))\/((op (e1) (e0)) = (e3)))))/\((((op (e1) (e1)) = (e0))\/(((op (e1) (e1)) = (e1))\/(((op (e1) (e1)) = (e2))\/((op (e1) (e1)) = (e3)))))/\((((op (e1) (e2)) = (e0))\/(((op (e1) (e2)) = (e1))\/(((op (e1) (e2)) = (e2))\/((op (e1) (e2)) = (e3)))))/\((((op (e1) (e3)) = (e0))\/(((op (e1) (e3)) = (e1))\/(((op (e1) (e3)) = (e2))\/((op (e1) (e3)) = (e3)))))/\((((op (e2) (e0)) = (e0))\/(((op (e2) (e0)) = (e1))\/(((op (e2) (e0)) = (e2))\/((op (e2) (e0)) = (e3)))))/\((((op (e2) (e1)) = (e0))\/(((op (e2) (e1)) = (e1))\/(((op (e2) (e1)) = (e2))\/((op (e2) (e1)) = (e3)))))/\((((op (e2) (e2)) = (e0))\/(((op (e2) (e2)) = (e1))\/(((op (e2) (e2)) = (e2))\/((op (e2) (e2)) = (e3)))))/\((((op (e2) (e3)) = (e0))\/(((op (e2) (e3)) = (e1))\/(((op (e2) (e3)) = (e2))\/((op (e2) (e3)) = (e3)))))/\((((op (e3) (e0)) = (e0))\/(((op (e3) (e0)) = (e1))\/(((op (e3) (e0)) = (e2))\/((op (e3) (e0)) = (e3)))))/\((((op (e3) (e1)) = (e0))\/(((op (e3) (e1)) = (e1))\/(((op (e3) (e1)) = (e2))\/((op (e3) (e1)) = (e3)))))/\((((op (e3) (e2)) = (e0))\/(((op (e3) (e2)) = (e1))\/(((op (e3) (e2)) = (e2))\/((op (e3) (e2)) = (e3)))))/\((((op (e3) (e3)) = (e0))\/(((op (e3) (e3)) = (e1))\/(((op (e3) (e3)) = (e2))\/((op (e3) (e3)) = (e3)))))/\(((op (unit) (e0)) = (e0))/\(((op (e0) (unit)) = (e0))/\(((op (unit) (e1)) = (e1))/\(((op (e1) (unit)) = (e1))/\(((op (unit) (e2)) = (e2))/\(((op (e2) (unit)) = (e2))/\(((op (unit) (e3)) = (e3))/\(((op (e3) (unit)) = (e3))/\((((unit) = (e0))\/(((unit) = (e1))\/(((unit) = (e2))\/((unit) = (e3)))))/\((((op (e0) (e0)) = (e0))\/(((op (e0) (e1)) = (e0))\/(((op (e0) (e2)) = (e0))\/((op (e0) (e3)) = (e0)))))/\((((op (e0) (e0)) = (e0))\/(((op (e1) (e0)) = (e0))\/(((op (e2) (e0)) = (e0))\/((op (e3) (e0)) = (e0)))))/\((((op (e0) (e0)) = (e1))\/(((op (e0) (e1)) = (e1))\/(((op (e0) (e2)) = (e1))\/((op (e0) (e3)) = (e1)))))/\((((op (e0) (e0)) = (e1))\/(((op (e1) (e0)) = (e1))\/(((op (e2) (e0)) = (e1))\/((op (e3) (e0)) = (e1)))))/\((((op (e0) (e0)) = (e2))\/(((op (e0) (e1)) = (e2))\/(((op (e0) (e2)) = (e2))\/((op (e0) (e3)) = (e2)))))/\((((op (e0) (e0)) = (e2))\/(((op (e1) (e0)) = (e2))\/(((op (e2) (e0)) = (e2))\/((op (e3) (e0)) = (e2)))))/\((((op (e0) (e0)) = (e3))\/(((op (e0) (e1)) = (e3))\/(((op (e0) (e2)) = (e3))\/((op (e0) (e3)) = (e3)))))/\((((op (e0) (e0)) = (e3))\/(((op (e1) (e0)) = (e3))\/(((op (e2) (e0)) = (e3))\/((op (e3) (e0)) = (e3)))))/\((((op (e1) (e0)) = (e0))\/(((op (e1) (e1)) = (e0))\/(((op (e1) (e2)) = (e0))\/((op (e1) (e3)) = (e0)))))/\((((op (e0) (e1)) = (e0))\/(((op (e1) (e1)) = (e0))\/(((op (e2) (e1)) = (e0))\/((op (e3) (e1)) = (e0)))))/\((((op (e1) (e0)) = (e1))\/(((op (e1) (e1)) = (e1))\/(((op (e1) (e2)) = (e1))\/((op (e1) (e3)) = (e1)))))/\((((op (e0) (e1)) = (e1))\/(((op (e1) (e1)) = (e1))\/(((op (e2) (e1)) = (e1))\/((op (e3) (e1)) = (e1)))))/\((((op (e1) (e0)) = (e2))\/(((op (e1) (e1)) = (e2))\/(((op (e1) (e2)) = (e2))\/((op (e1) (e3)) = (e2)))))/\((((op (e0) (e1)) = (e2))\/(((op (e1) (e1)) = (e2))\/(((op (e2) (e1)) = (e2))\/((op (e3) (e1)) = (e2)))))/\((((op (e1) (e0)) = (e3))\/(((op (e1) (e1)) = (e3))\/(((op (e1) (e2)) = (e3))\/((op (e1) (e3)) = (e3)))))/\((((op (e0) (e1)) = (e3))\/(((op (e1) (e1)) = (e3))\/(((op (e2) (e1)) = (e3))\/((op (e3) (e1)) = (e3)))))/\((((op (e2) (e0)) = (e0))\/(((op (e2) (e1)) = (e0))\/(((op (e2) (e2)) = (e0))\/((op (e2) (e3)) = (e0)))))/\((((op (e0) (e2)) = (e0))\/(((op (e1) (e2)) = (e0))\/(((op (e2) (e2)) = (e0))\/((op (e3) (e2)) = (e0)))))/\((((op (e2) (e0)) = (e1))\/(((op (e2) (e1)) = (e1))\/(((op (e2) (e2)) = (e1))\/((op (e2) (e3)) = (e1)))))/\((((op (e0) (e2)) = (e1))\/(((op (e1) (e2)) = (e1))\/(((op (e2) (e2)) = (e1))\/((op (e3) (e2)) = (e1)))))/\((((op (e2) (e0)) = (e2))\/(((op (e2) (e1)) = (e2))\/(((op (e2) (e2)) = (e2))\/((op (e2) (e3)) = (e2)))))/\((((op (e0) (e2)) = (e2))\/(((op (e1) (e2)) = (e2))\/(((op (e2) (e2)) = (e2))\/((op (e3) (e2)) = (e2)))))/\((((op (e2) (e0)) = (e3))\/(((op (e2) (e1)) = (e3))\/(((op (e2) (e2)) = (e3))\/((op (e2) (e3)) = (e3)))))/\((((op (e0) (e2)) = (e3))\/(((op (e1) (e2)) = (e3))\/(((op (e2) (e2)) = (e3))\/((op (e3) (e2)) = (e3)))))/\((((op (e3) (e0)) = (e0))\/(((op (e3) (e1)) = (e0))\/(((op (e3) (e2)) = (e0))\/((op (e3) (e3)) = (e0)))))/\((((op (e0) (e3)) = (e0))\/(((op (e1) (e3)) = (e0))\/(((op (e2) (e3)) = (e0))\/((op (e3) (e3)) = (e0)))))/\((((op (e3) (e0)) = (e1))\/(((op (e3) (e1)) = (e1))\/(((op (e3) (e2)) = (e1))\/((op (e3) (e3)) = (e1)))))/\((((op (e0) (e3)) = (e1))\/(((op (e1) (e3)) = (e1))\/(((op (e2) (e3)) = (e1))\/((op (e3) (e3)) = (e1)))))/\((((op (e3) (e0)) = (e2))\/(((op (e3) (e1)) = (e2))\/(((op (e3) (e2)) = (e2))\/((op (e3) (e3)) = (e2)))))/\((((op (e0) (e3)) = (e2))\/(((op (e1) (e3)) = (e2))\/(((op (e2) (e3)) = (e2))\/((op (e3) (e3)) = (e2)))))/\((((op (e3) (e0)) = (e3))\/(((op (e3) (e1)) = (e3))\/(((op (e3) (e2)) = (e3))\/((op (e3) (e3)) = (e3)))))/\(((op (e0) (e3)) = (e3))\/(((op (e1) (e3)) = (e3))\/(((op (e2) (e3)) = (e3))\/((op (e3) (e3)) = (e3)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 0.43/0.59 Proof. % 0.43/0.59 assert (zenon_L1_ : (~((unit) = (e0))) -> False). % 0.43/0.59 do 0 intro. intros zenon_H4. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 (* end of lemma zenon_L1_ *) % 0.43/0.59 assert (zenon_L2_ : (~((e0) = (e0))) -> False). % 0.43/0.59 do 0 intro. intros zenon_H5. % 0.43/0.59 apply zenon_H5. apply refl_equal. % 0.43/0.59 (* end of lemma zenon_L2_ *) % 0.43/0.59 assert (zenon_L3_ : (~((e1) = (e1))) -> False). % 0.43/0.59 do 0 intro. intros zenon_H6. % 0.43/0.59 apply zenon_H6. apply refl_equal. % 0.43/0.59 (* end of lemma zenon_L3_ *) % 0.43/0.59 assert (zenon_L4_ : (~((e2) = (e2))) -> False). % 0.43/0.59 do 0 intro. intros zenon_H7. % 0.43/0.59 apply zenon_H7. apply refl_equal. % 0.43/0.59 (* end of lemma zenon_L4_ *) % 0.43/0.59 assert (zenon_L5_ : (~((e3) = (e3))) -> False). % 0.43/0.59 do 0 intro. intros zenon_H8. % 0.43/0.59 apply zenon_H8. apply refl_equal. % 0.43/0.59 (* end of lemma zenon_L5_ *) % 0.43/0.59 apply NNPP. intro zenon_G. % 0.43/0.59 apply (zenon_and_s _ _ ax2). zenon_intro zenon_Ha. zenon_intro zenon_H9. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H9). zenon_intro zenon_Hc. zenon_intro zenon_Hb. % 0.43/0.59 apply (zenon_and_s _ _ zenon_Hb). zenon_intro zenon_He. zenon_intro zenon_Hd. % 0.43/0.59 apply (zenon_and_s _ _ zenon_Hd). zenon_intro zenon_H10. zenon_intro zenon_Hf. % 0.43/0.59 apply (zenon_and_s _ _ zenon_Hf). zenon_intro zenon_H12. zenon_intro zenon_H11. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H11). zenon_intro zenon_H14. zenon_intro zenon_H13. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H13). zenon_intro zenon_H16. zenon_intro zenon_H15. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H15). zenon_intro zenon_H18. zenon_intro zenon_H17. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H17). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H19). zenon_intro zenon_H1c. zenon_intro zenon_H1b. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H1b). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H1d). zenon_intro zenon_H20. zenon_intro zenon_H1f. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H1f). zenon_intro zenon_H22. zenon_intro zenon_H21. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H24. zenon_intro zenon_H23. % 0.43/0.59 apply (zenon_and_s _ _ zenon_H23). zenon_intro zenon_H26. zenon_intro zenon_H25. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H28 | zenon_intro zenon_H27 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H28). zenon_intro zenon_H2a. zenon_intro zenon_H29. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H2a); [ zenon_intro zenon_H2c | zenon_intro zenon_H2b ]. % 0.43/0.59 exact (zenon_H2c zenon_Ha). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H2b); [ zenon_intro zenon_H2e | zenon_intro zenon_H2d ]. % 0.43/0.59 exact (zenon_H2e zenon_H14). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H2d); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 0.43/0.59 exact (zenon_H30 zenon_H1e). % 0.43/0.59 exact (zenon_H2f zenon_H25). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H27); [ zenon_intro zenon_H32 | zenon_intro zenon_H31 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H32). zenon_intro zenon_H2c. zenon_intro zenon_H33. % 0.43/0.59 exact (zenon_H2c zenon_Ha). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H31); [ zenon_intro zenon_H35 | zenon_intro zenon_H34 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H35). zenon_intro zenon_H37. zenon_intro zenon_H36. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 0.43/0.59 exact (zenon_H39 zenon_Hc). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H34); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H3b). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 0.43/0.59 exact (zenon_H41 zenon_He). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H43). zenon_intro zenon_H45. zenon_intro zenon_H44. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H46). zenon_intro zenon_H49. zenon_intro zenon_H48. % 0.43/0.59 exact (zenon_H48 zenon_H10). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H42); [ zenon_intro zenon_H4b | zenon_intro zenon_H4a ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H4b). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H4c). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 0.43/0.59 exact (zenon_H4f zenon_H12). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H4a); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H51). zenon_intro zenon_H2e. zenon_intro zenon_H52. % 0.43/0.59 exact (zenon_H2e zenon_H14). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H54). zenon_intro zenon_H56. zenon_intro zenon_H55. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H55). zenon_intro zenon_H58. zenon_intro zenon_H57. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H57). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 0.43/0.59 exact (zenon_H59 zenon_H16). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H53); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H5c). zenon_intro zenon_H5e. zenon_intro zenon_H5d. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H5d). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H5f). zenon_intro zenon_H62. zenon_intro zenon_H61. % 0.43/0.59 exact (zenon_H62 zenon_H18). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H5b); [ zenon_intro zenon_H64 | zenon_intro zenon_H63 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H64). zenon_intro zenon_H66. zenon_intro zenon_H65. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 0.43/0.59 exact (zenon_H6a zenon_H1a). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H63); [ zenon_intro zenon_H6c | zenon_intro zenon_H6b ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H6c). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H6f). zenon_intro zenon_H72. zenon_intro zenon_H71. % 0.43/0.59 exact (zenon_H71 zenon_H1c). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H6b); [ zenon_intro zenon_H74 | zenon_intro zenon_H73 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H74). zenon_intro zenon_H30. zenon_intro zenon_H75. % 0.43/0.59 exact (zenon_H30 zenon_H1e). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H73); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H77). zenon_intro zenon_H79. zenon_intro zenon_H78. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 0.43/0.59 exact (zenon_H7b zenon_H20). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H7d | zenon_intro zenon_H7c ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H7d). zenon_intro zenon_H7f. zenon_intro zenon_H7e. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H7e). zenon_intro zenon_H81. zenon_intro zenon_H80. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 0.43/0.59 exact (zenon_H82 zenon_H22). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H7c); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H85). zenon_intro zenon_H87. zenon_intro zenon_H86. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H86). zenon_intro zenon_H89. zenon_intro zenon_H88. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H88). zenon_intro zenon_H8b. zenon_intro zenon_H8a. % 0.43/0.59 exact (zenon_H8b zenon_H24). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H8d). zenon_intro zenon_H8f. zenon_intro zenon_H8e. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H8e). zenon_intro zenon_H91. zenon_intro zenon_H90. % 0.43/0.59 exact (zenon_H91 zenon_H26). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H8c); [ zenon_intro zenon_H93 | zenon_intro zenon_H92 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H93). zenon_intro zenon_H2f. zenon_intro zenon_H94. % 0.43/0.59 exact (zenon_H2f zenon_H25). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H92); [ zenon_intro zenon_H96 | zenon_intro zenon_H95 ]. % 0.43/0.59 cut (((op (e0) (e0)) = (e0)) = ((op (unit) (e0)) = (e0))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_H96. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Ha. % 0.43/0.59 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 0.43/0.59 cut (((op (e0) (e0)) = (op (unit) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H97]. % 0.43/0.59 congruence. % 0.43/0.59 elim (classic ((op (unit) (e0)) = (op (unit) (e0)))); [ zenon_intro zenon_H98 | zenon_intro zenon_H99 ]. % 0.43/0.59 cut (((op (unit) (e0)) = (op (unit) (e0))) = ((op (e0) (e0)) = (op (unit) (e0)))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_H97. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_H98. % 0.43/0.59 cut (((op (unit) (e0)) = (op (unit) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 0.43/0.59 cut (((op (unit) (e0)) = (op (e0) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H9a]. % 0.43/0.59 congruence. % 0.43/0.59 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 0.43/0.59 cut (((unit) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 0.43/0.59 congruence. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply zenon_H5. apply refl_equal. % 0.43/0.59 apply zenon_H99. apply refl_equal. % 0.43/0.59 apply zenon_H99. apply refl_equal. % 0.43/0.59 apply zenon_H5. apply refl_equal. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H95); [ zenon_intro zenon_H9c | zenon_intro zenon_H9b ]. % 0.43/0.59 cut (((op (e0) (e0)) = (e0)) = ((op (e0) (unit)) = (e0))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_H9c. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Ha. % 0.43/0.59 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 0.43/0.59 cut (((op (e0) (e0)) = (op (e0) (unit)))); [idtac | apply NNPP; zenon_intro zenon_H9d]. % 0.43/0.59 congruence. % 0.43/0.59 elim (classic ((op (e0) (unit)) = (op (e0) (unit)))); [ zenon_intro zenon_H9e | zenon_intro zenon_H9f ]. % 0.43/0.59 cut (((op (e0) (unit)) = (op (e0) (unit))) = ((op (e0) (e0)) = (op (e0) (unit)))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_H9d. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_H9e. % 0.43/0.59 cut (((op (e0) (unit)) = (op (e0) (unit)))); [idtac | apply NNPP; zenon_intro zenon_H9f]. % 0.43/0.59 cut (((op (e0) (unit)) = (op (e0) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 0.43/0.59 congruence. % 0.43/0.59 cut (((unit) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 0.43/0.59 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 0.43/0.59 congruence. % 0.43/0.59 apply zenon_H5. apply refl_equal. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply zenon_H9f. apply refl_equal. % 0.43/0.59 apply zenon_H9f. apply refl_equal. % 0.43/0.59 apply zenon_H5. apply refl_equal. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1 ]. % 0.43/0.59 cut (((op (e0) (e1)) = (e1)) = ((op (unit) (e1)) = (e1))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Ha2. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Hc. % 0.43/0.59 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 0.43/0.59 cut (((op (e0) (e1)) = (op (unit) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 0.43/0.59 congruence. % 0.43/0.59 elim (classic ((op (unit) (e1)) = (op (unit) (e1)))); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha5 ]. % 0.43/0.59 cut (((op (unit) (e1)) = (op (unit) (e1))) = ((op (e0) (e1)) = (op (unit) (e1)))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Ha3. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Ha4. % 0.43/0.59 cut (((op (unit) (e1)) = (op (unit) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 0.43/0.59 cut (((op (unit) (e1)) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 0.43/0.59 congruence. % 0.43/0.59 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 0.43/0.59 cut (((unit) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 0.43/0.59 congruence. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply zenon_H6. apply refl_equal. % 0.43/0.59 apply zenon_Ha5. apply refl_equal. % 0.43/0.59 apply zenon_Ha5. apply refl_equal. % 0.43/0.59 apply zenon_H6. apply refl_equal. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha8 | zenon_intro zenon_Ha7 ]. % 0.43/0.59 cut (((op (e1) (e0)) = (e1)) = ((op (e1) (unit)) = (e1))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Ha8. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_H12. % 0.43/0.59 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 0.43/0.59 cut (((op (e1) (e0)) = (op (e1) (unit)))); [idtac | apply NNPP; zenon_intro zenon_Ha9]. % 0.43/0.59 congruence. % 0.43/0.59 elim (classic ((op (e1) (unit)) = (op (e1) (unit)))); [ zenon_intro zenon_Haa | zenon_intro zenon_Hab ]. % 0.43/0.59 cut (((op (e1) (unit)) = (op (e1) (unit))) = ((op (e1) (e0)) = (op (e1) (unit)))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Ha9. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Haa. % 0.43/0.59 cut (((op (e1) (unit)) = (op (e1) (unit)))); [idtac | apply NNPP; zenon_intro zenon_Hab]. % 0.43/0.59 cut (((op (e1) (unit)) = (op (e1) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 0.43/0.59 congruence. % 0.43/0.59 cut (((unit) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 0.43/0.59 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 0.43/0.59 congruence. % 0.43/0.59 apply zenon_H6. apply refl_equal. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply zenon_Hab. apply refl_equal. % 0.43/0.59 apply zenon_Hab. apply refl_equal. % 0.43/0.59 apply zenon_H6. apply refl_equal. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Ha7); [ zenon_intro zenon_Hae | zenon_intro zenon_Had ]. % 0.43/0.59 cut (((op (e0) (e2)) = (e2)) = ((op (unit) (e2)) = (e2))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Hae. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_He. % 0.43/0.59 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 0.43/0.59 cut (((op (e0) (e2)) = (op (unit) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Haf]. % 0.43/0.59 congruence. % 0.43/0.59 elim (classic ((op (unit) (e2)) = (op (unit) (e2)))); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Hb1 ]. % 0.43/0.59 cut (((op (unit) (e2)) = (op (unit) (e2))) = ((op (e0) (e2)) = (op (unit) (e2)))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Haf. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Hb0. % 0.43/0.59 cut (((op (unit) (e2)) = (op (unit) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 0.43/0.59 cut (((op (unit) (e2)) = (op (e0) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hb2]. % 0.43/0.59 congruence. % 0.43/0.59 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 0.43/0.59 cut (((unit) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 0.43/0.59 congruence. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply zenon_H7. apply refl_equal. % 0.43/0.59 apply zenon_Hb1. apply refl_equal. % 0.43/0.59 apply zenon_Hb1. apply refl_equal. % 0.43/0.59 apply zenon_H7. apply refl_equal. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_Hb4 | zenon_intro zenon_Hb3 ]. % 0.43/0.59 cut (((op (e2) (e0)) = (e2)) = ((op (e2) (unit)) = (e2))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Hb4. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_H1a. % 0.43/0.59 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 0.43/0.59 cut (((op (e2) (e0)) = (op (e2) (unit)))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 0.43/0.59 congruence. % 0.43/0.59 elim (classic ((op (e2) (unit)) = (op (e2) (unit)))); [ zenon_intro zenon_Hb6 | zenon_intro zenon_Hb7 ]. % 0.43/0.59 cut (((op (e2) (unit)) = (op (e2) (unit))) = ((op (e2) (e0)) = (op (e2) (unit)))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Hb5. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Hb6. % 0.43/0.59 cut (((op (e2) (unit)) = (op (e2) (unit)))); [idtac | apply NNPP; zenon_intro zenon_Hb7]. % 0.43/0.59 cut (((op (e2) (unit)) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Hb8]. % 0.43/0.59 congruence. % 0.43/0.59 cut (((unit) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 0.43/0.59 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 0.43/0.59 congruence. % 0.43/0.59 apply zenon_H7. apply refl_equal. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply zenon_Hb7. apply refl_equal. % 0.43/0.59 apply zenon_Hb7. apply refl_equal. % 0.43/0.59 apply zenon_H7. apply refl_equal. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hb3); [ zenon_intro zenon_Hba | zenon_intro zenon_Hb9 ]. % 0.43/0.59 cut (((op (e0) (e3)) = (e3)) = ((op (unit) (e3)) = (e3))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Hba. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_H10. % 0.43/0.59 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H8]. % 0.43/0.59 cut (((op (e0) (e3)) = (op (unit) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hbb]. % 0.43/0.59 congruence. % 0.43/0.59 elim (classic ((op (unit) (e3)) = (op (unit) (e3)))); [ zenon_intro zenon_Hbc | zenon_intro zenon_Hbd ]. % 0.43/0.59 cut (((op (unit) (e3)) = (op (unit) (e3))) = ((op (e0) (e3)) = (op (unit) (e3)))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Hbb. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Hbc. % 0.43/0.59 cut (((op (unit) (e3)) = (op (unit) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hbd]. % 0.43/0.59 cut (((op (unit) (e3)) = (op (e0) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hbe]. % 0.43/0.59 congruence. % 0.43/0.59 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H8]. % 0.43/0.59 cut (((unit) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 0.43/0.59 congruence. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply zenon_H8. apply refl_equal. % 0.43/0.59 apply zenon_Hbd. apply refl_equal. % 0.43/0.59 apply zenon_Hbd. apply refl_equal. % 0.43/0.59 apply zenon_H8. apply refl_equal. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hb9); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Hbf ]. % 0.43/0.59 cut (((op (e3) (e0)) = (e3)) = ((op (e3) (unit)) = (e3))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Hc0. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_H22. % 0.43/0.59 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H8]. % 0.43/0.59 cut (((op (e3) (e0)) = (op (e3) (unit)))); [idtac | apply NNPP; zenon_intro zenon_Hc1]. % 0.43/0.59 congruence. % 0.43/0.59 elim (classic ((op (e3) (unit)) = (op (e3) (unit)))); [ zenon_intro zenon_Hc2 | zenon_intro zenon_Hc3 ]. % 0.43/0.59 cut (((op (e3) (unit)) = (op (e3) (unit))) = ((op (e3) (e0)) = (op (e3) (unit)))). % 0.43/0.59 intro zenon_D_pnotp. % 0.43/0.59 apply zenon_Hc1. % 0.43/0.59 rewrite <- zenon_D_pnotp. % 0.43/0.59 exact zenon_Hc2. % 0.43/0.59 cut (((op (e3) (unit)) = (op (e3) (unit)))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 0.43/0.59 cut (((op (e3) (unit)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Hc4]. % 0.43/0.59 congruence. % 0.43/0.59 cut (((unit) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 0.43/0.59 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H8]. % 0.43/0.59 congruence. % 0.43/0.59 apply zenon_H8. apply refl_equal. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply zenon_Hc3. apply refl_equal. % 0.43/0.59 apply zenon_Hc3. apply refl_equal. % 0.43/0.59 apply zenon_H8. apply refl_equal. % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hbf); [ zenon_intro zenon_Hc6 | zenon_intro zenon_Hc5 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hc6). zenon_intro zenon_H4. zenon_intro zenon_Hc7. % 0.43/0.59 exact (zenon_H4 ax3). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hc5); [ zenon_intro zenon_Hc9 | zenon_intro zenon_Hc8 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hc9). zenon_intro zenon_H2c. zenon_intro zenon_Hca. % 0.43/0.59 exact (zenon_H2c zenon_Ha). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hc8); [ zenon_intro zenon_Hcc | zenon_intro zenon_Hcb ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hcc). zenon_intro zenon_H2c. zenon_intro zenon_Hcd. % 0.43/0.59 exact (zenon_H2c zenon_Ha). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hcb); [ zenon_intro zenon_Hcf | zenon_intro zenon_Hce ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hcf). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hd0). zenon_intro zenon_H39. zenon_intro zenon_Hd2. % 0.43/0.59 exact (zenon_H39 zenon_Hc). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_Hd4 | zenon_intro zenon_Hd3 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hd4). zenon_intro zenon_Hd1. zenon_intro zenon_Hd5. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hd5). zenon_intro zenon_H4f. zenon_intro zenon_Hd6. % 0.43/0.59 exact (zenon_H4f zenon_H12). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hd3); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hd8). zenon_intro zenon_Hda. zenon_intro zenon_Hd9. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hd9). zenon_intro zenon_Hdc. zenon_intro zenon_Hdb. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hdb). zenon_intro zenon_H41. zenon_intro zenon_H49. % 0.43/0.59 exact (zenon_H41 zenon_He). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hd7); [ zenon_intro zenon_Hde | zenon_intro zenon_Hdd ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hde). zenon_intro zenon_Hda. zenon_intro zenon_Hdf. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hdf). zenon_intro zenon_He1. zenon_intro zenon_He0. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_He0). zenon_intro zenon_H6a. zenon_intro zenon_H83. % 0.43/0.59 exact (zenon_H6a zenon_H1a). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hdd); [ zenon_intro zenon_He3 | zenon_intro zenon_He2 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_He3). zenon_intro zenon_He5. zenon_intro zenon_He4. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_He4). zenon_intro zenon_He7. zenon_intro zenon_He6. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_He6). zenon_intro zenon_H40. zenon_intro zenon_H48. % 0.43/0.59 exact (zenon_H48 zenon_H10). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_He2); [ zenon_intro zenon_He9 | zenon_intro zenon_He8 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_He9). zenon_intro zenon_He5. zenon_intro zenon_Hea. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hea). zenon_intro zenon_Hec. zenon_intro zenon_Heb. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Heb). zenon_intro zenon_H69. zenon_intro zenon_H82. % 0.43/0.59 exact (zenon_H82 zenon_H22). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_He8); [ zenon_intro zenon_Hee | zenon_intro zenon_Hed ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hee). zenon_intro zenon_H4d. zenon_intro zenon_Hef. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hef). zenon_intro zenon_H2e. zenon_intro zenon_Hf0. % 0.43/0.59 exact (zenon_H2e zenon_H14). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hed); [ zenon_intro zenon_Hf2 | zenon_intro zenon_Hf1 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hf2). zenon_intro zenon_H37. zenon_intro zenon_Hf3. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hf3). zenon_intro zenon_H2e. zenon_intro zenon_Hf4. % 0.43/0.59 exact (zenon_H2e zenon_H14). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hf1); [ zenon_intro zenon_Hf6 | zenon_intro zenon_Hf5 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hf6). zenon_intro zenon_H4f. zenon_intro zenon_Hf7. % 0.43/0.59 exact (zenon_H4f zenon_H12). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hf5); [ zenon_intro zenon_Hf9 | zenon_intro zenon_Hf8 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hf9). zenon_intro zenon_H39. zenon_intro zenon_Hfa. % 0.43/0.59 exact (zenon_H39 zenon_Hc). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hf8); [ zenon_intro zenon_Hfc | zenon_intro zenon_Hfb ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hfc). zenon_intro zenon_He1. zenon_intro zenon_Hfd. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hfd). zenon_intro zenon_Hff. zenon_intro zenon_Hfe. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_Hfe). zenon_intro zenon_H5a. zenon_intro zenon_H62. % 0.43/0.59 exact (zenon_H62 zenon_H18). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_Hfb); [ zenon_intro zenon_H101 | zenon_intro zenon_H100 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H101). zenon_intro zenon_Hdc. zenon_intro zenon_H102. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H102). zenon_intro zenon_Hff. zenon_intro zenon_H103. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H103). zenon_intro zenon_H72. zenon_intro zenon_H8b. % 0.43/0.59 exact (zenon_H8b zenon_H24). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H100); [ zenon_intro zenon_H105 | zenon_intro zenon_H104 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H105). zenon_intro zenon_Hec. zenon_intro zenon_H106. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H106). zenon_intro zenon_H108. zenon_intro zenon_H107. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H107). zenon_intro zenon_H59. zenon_intro zenon_H61. % 0.43/0.59 exact (zenon_H59 zenon_H16). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H104); [ zenon_intro zenon_H10a | zenon_intro zenon_H109 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H10a). zenon_intro zenon_He7. zenon_intro zenon_H10b. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H10b). zenon_intro zenon_H108. zenon_intro zenon_H10c. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H10c). zenon_intro zenon_H71. zenon_intro zenon_H8a. % 0.43/0.59 exact (zenon_H71 zenon_H1c). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H109); [ zenon_intro zenon_H10e | zenon_intro zenon_H10d ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H10e). zenon_intro zenon_H66. zenon_intro zenon_H10f. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H10f). zenon_intro zenon_H6e. zenon_intro zenon_H110. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H110). zenon_intro zenon_H30. zenon_intro zenon_H79. % 0.43/0.59 exact (zenon_H30 zenon_H1e). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H10d); [ zenon_intro zenon_H112 | zenon_intro zenon_H111 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H112). zenon_intro zenon_H3d. zenon_intro zenon_H113. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H113). zenon_intro zenon_H56. zenon_intro zenon_H114. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H114). zenon_intro zenon_H30. zenon_intro zenon_H8f. % 0.43/0.59 exact (zenon_H30 zenon_H1e). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H111); [ zenon_intro zenon_H116 | zenon_intro zenon_H115 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H116). zenon_intro zenon_H68. zenon_intro zenon_H117. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H117). zenon_intro zenon_H70. zenon_intro zenon_H118. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H118). zenon_intro zenon_H119. zenon_intro zenon_H7b. % 0.43/0.59 exact (zenon_H7b zenon_H20). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H115); [ zenon_intro zenon_H11b | zenon_intro zenon_H11a ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H11b). zenon_intro zenon_H3f. zenon_intro zenon_H11c. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H11c). zenon_intro zenon_H58. zenon_intro zenon_H11d. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H11d). zenon_intro zenon_H119. zenon_intro zenon_H91. % 0.43/0.59 exact (zenon_H91 zenon_H26). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H11a); [ zenon_intro zenon_H11f | zenon_intro zenon_H11e ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H11f). zenon_intro zenon_H6a. zenon_intro zenon_H120. % 0.43/0.59 exact (zenon_H6a zenon_H1a). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H11e); [ zenon_intro zenon_H122 | zenon_intro zenon_H121 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H122). zenon_intro zenon_H41. zenon_intro zenon_H123. % 0.43/0.59 exact (zenon_H41 zenon_He). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H121); [ zenon_intro zenon_H125 | zenon_intro zenon_H124 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H125). zenon_intro zenon_H69. zenon_intro zenon_H126. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H126). zenon_intro zenon_H71. zenon_intro zenon_H127. % 0.43/0.59 exact (zenon_H71 zenon_H1c). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H124); [ zenon_intro zenon_H129 | zenon_intro zenon_H128 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H129). zenon_intro zenon_H40. zenon_intro zenon_H12a. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H12a). zenon_intro zenon_H59. zenon_intro zenon_H12b. % 0.43/0.59 exact (zenon_H59 zenon_H16). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H128); [ zenon_intro zenon_H12d | zenon_intro zenon_H12c ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H12d). zenon_intro zenon_H7f. zenon_intro zenon_H12e. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H12e). zenon_intro zenon_H87. zenon_intro zenon_H12f. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H12f). zenon_intro zenon_H8f. zenon_intro zenon_H2f. % 0.43/0.59 exact (zenon_H2f zenon_H25). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H12c); [ zenon_intro zenon_H131 | zenon_intro zenon_H130 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H131). zenon_intro zenon_H45. zenon_intro zenon_H132. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H132). zenon_intro zenon_H5e. zenon_intro zenon_H133. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H133). zenon_intro zenon_H79. zenon_intro zenon_H2f. % 0.43/0.59 exact (zenon_H2f zenon_H25). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H130); [ zenon_intro zenon_H135 | zenon_intro zenon_H134 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H135). zenon_intro zenon_H81. zenon_intro zenon_H136. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H136). zenon_intro zenon_H89. zenon_intro zenon_H137. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H137). zenon_intro zenon_H91. zenon_intro zenon_H138. % 0.43/0.59 exact (zenon_H91 zenon_H26). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H134); [ zenon_intro zenon_H13a | zenon_intro zenon_H139 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H13a). zenon_intro zenon_H47. zenon_intro zenon_H13b. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H13b). zenon_intro zenon_H60. zenon_intro zenon_H13c. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H13c). zenon_intro zenon_H7b. zenon_intro zenon_H138. % 0.43/0.59 exact (zenon_H7b zenon_H20). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H139); [ zenon_intro zenon_H13e | zenon_intro zenon_H13d ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H13e). zenon_intro zenon_H83. zenon_intro zenon_H13f. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H13f). zenon_intro zenon_H8b. zenon_intro zenon_H140. % 0.43/0.59 exact (zenon_H8b zenon_H24). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H13d); [ zenon_intro zenon_H142 | zenon_intro zenon_H141 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H142). zenon_intro zenon_H49. zenon_intro zenon_H143. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H143). zenon_intro zenon_H62. zenon_intro zenon_H144. % 0.43/0.59 exact (zenon_H62 zenon_H18). % 0.43/0.59 apply (zenon_notand_s _ _ zenon_H141); [ zenon_intro zenon_H146 | zenon_intro zenon_H145 ]. % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H146). zenon_intro zenon_H82. zenon_intro zenon_H147. % 0.43/0.59 exact (zenon_H82 zenon_H22). % 0.43/0.59 apply (zenon_notor_s _ _ zenon_H145). zenon_intro zenon_H48. zenon_intro zenon_H148. % 0.43/0.59 exact (zenon_H48 zenon_H10). % 0.43/0.59 Qed. % 0.43/0.59 % SZS output end Proof % 0.43/0.59 (* END-PROOF *) % 0.43/0.59 nodes searched: 547 % 0.43/0.59 max branch formulas: 80 % 0.43/0.59 proof nodes created: 126 % 0.43/0.59 formulas created: 3630 % 0.43/0.59 %------------------------------------------------------------------------------