%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : ALG138+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:30:13 EDT 2022 % Result : Unsatisfiable 0.92s 1.14s % Output : Proof 0.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : ALG138+1 : TPTP v8.1.0. Released v2.7.0. % 0.06/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 8 11:41:08 EDT 2022 % 0.13/0.34 % CPUTime : % 0.92/1.14 (* PROOF-FOUND *) % 0.92/1.14 % SZS status Unsatisfiable % 0.92/1.14 (* BEGIN-PROOF *) % 0.92/1.14 % SZS output start Proof % 0.92/1.14 Theorem zenon_thm : False. % 0.92/1.14 Proof. % 0.92/1.14 assert (zenon_L1_ : (~((e0) = (e0))) -> False). % 0.92/1.14 do 0 intro. intros zenon_H1d. % 0.92/1.14 apply zenon_H1d. apply refl_equal. % 0.92/1.14 (* end of lemma zenon_L1_ *) % 0.92/1.14 assert (zenon_L2_ : (~((e2) = (e2))) -> False). % 0.92/1.14 do 0 intro. intros zenon_H1e. % 0.92/1.14 apply zenon_H1e. apply refl_equal. % 0.92/1.14 (* end of lemma zenon_L2_ *) % 0.92/1.14 assert (zenon_L3_ : (~((e1) = (e1))) -> False). % 0.92/1.14 do 0 intro. intros zenon_H1f. % 0.92/1.14 apply zenon_H1f. apply refl_equal. % 0.92/1.14 (* end of lemma zenon_L3_ *) % 0.92/1.14 assert (zenon_L4_ : ((op (e0) (e2)) = (e1)) -> ((op (e3) (e2)) = (e0)) -> False). % 0.92/1.14 do 0 intro. intros zenon_H20 zenon_H21. % 0.92/1.14 apply (zenon_notand_s _ _ ax7); [ zenon_intro zenon_H23 | zenon_intro zenon_H22 ]. % 0.92/1.14 apply zenon_H23. apply sym_equal. exact zenon_H21. % 0.92/1.14 elim (classic ((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2)))); [ zenon_intro zenon_H24 | zenon_intro zenon_H25 ]. % 0.92/1.14 cut (((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2))) = ((e1) = (op (op (e3) (e2)) (e2)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H22. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H24. % 0.92/1.14 cut (((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 0.92/1.14 cut (((op (op (e3) (e2)) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H26]. % 0.92/1.14 congruence. % 0.92/1.14 cut (((op (e0) (e2)) = (e1)) = ((op (op (e3) (e2)) (e2)) = (e1))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H26. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H20. % 0.92/1.14 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H1f]. % 0.92/1.14 cut (((op (e0) (e2)) = (op (op (e3) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 0.92/1.14 congruence. % 0.92/1.14 elim (classic ((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2)))); [ zenon_intro zenon_H24 | zenon_intro zenon_H25 ]. % 0.92/1.14 cut (((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2))) = ((op (e0) (e2)) = (op (op (e3) (e2)) (e2)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H27. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H24. % 0.92/1.14 cut (((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 0.92/1.14 cut (((op (op (e3) (e2)) (e2)) = (op (e0) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H28]. % 0.92/1.14 congruence. % 0.92/1.14 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H1e]. % 0.92/1.14 cut (((op (e3) (e2)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 0.92/1.14 congruence. % 0.92/1.14 exact (zenon_H29 zenon_H21). % 0.92/1.14 apply zenon_H1e. apply refl_equal. % 0.92/1.14 apply zenon_H25. apply refl_equal. % 0.92/1.14 apply zenon_H25. apply refl_equal. % 0.92/1.14 apply zenon_H1f. apply refl_equal. % 0.92/1.14 apply zenon_H25. apply refl_equal. % 0.92/1.14 apply zenon_H25. apply refl_equal. % 0.92/1.14 (* end of lemma zenon_L4_ *) % 0.92/1.14 assert (zenon_L5_ : (~((op (e0) (e2)) = (op (e3) (e2)))) -> ((op (e0) (e2)) = (e1)) -> ((op (e3) (e2)) = (e1)) -> False). % 0.92/1.14 do 0 intro. intros zenon_H2a zenon_H20 zenon_H2b. % 0.92/1.14 cut (((op (e0) (e2)) = (e1)) = ((op (e0) (e2)) = (op (e3) (e2)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H2a. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H20. % 0.92/1.14 cut (((e1) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 0.92/1.14 cut (((op (e0) (e2)) = (op (e0) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H2d]. % 0.92/1.14 congruence. % 0.92/1.14 apply zenon_H2d. apply refl_equal. % 0.92/1.14 apply zenon_H2c. apply sym_equal. exact zenon_H2b. % 0.92/1.14 (* end of lemma zenon_L5_ *) % 0.92/1.14 assert (zenon_L6_ : (~((op (e2) (e2)) = (op (e3) (e2)))) -> ((op (e2) (e2)) = (e2)) -> ((op (e3) (e2)) = (e2)) -> False). % 0.92/1.14 do 0 intro. intros zenon_H2e zenon_H2f zenon_H30. % 0.92/1.14 cut (((op (e2) (e2)) = (e2)) = ((op (e2) (e2)) = (op (e3) (e2)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H2e. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H2f. % 0.92/1.14 cut (((e2) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H31]. % 0.92/1.14 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H32]. % 0.92/1.14 congruence. % 0.92/1.14 apply zenon_H32. apply refl_equal. % 0.92/1.14 apply zenon_H31. apply sym_equal. exact zenon_H30. % 0.92/1.14 (* end of lemma zenon_L6_ *) % 0.92/1.14 assert (zenon_L7_ : ((op (e3) (e3)) = (e3)) -> ((op (e3) (e2)) = (e3)) -> (~((op (e3) (e2)) = (op (e3) (e3)))) -> False). % 0.92/1.14 do 0 intro. intros zenon_H33 zenon_H34 zenon_H35. % 0.92/1.14 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H36 | zenon_intro zenon_H37 ]. % 0.92/1.14 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e3) (e2)) = (op (e3) (e3)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H35. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H36. % 0.92/1.14 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 0.92/1.14 cut (((op (e3) (e3)) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H38]. % 0.92/1.14 congruence. % 0.92/1.14 cut (((op (e3) (e3)) = (e3)) = ((op (e3) (e3)) = (op (e3) (e2)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H38. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H33. % 0.92/1.14 cut (((e3) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H39]. % 0.92/1.14 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 0.92/1.14 congruence. % 0.92/1.14 apply zenon_H37. apply refl_equal. % 0.92/1.14 apply zenon_H39. apply sym_equal. exact zenon_H34. % 0.92/1.14 apply zenon_H37. apply refl_equal. % 0.92/1.14 apply zenon_H37. apply refl_equal. % 0.92/1.14 (* end of lemma zenon_L7_ *) % 0.92/1.14 assert (zenon_L8_ : (~((e3) = (e3))) -> False). % 0.92/1.14 do 0 intro. intros zenon_H3a. % 0.92/1.14 apply zenon_H3a. apply refl_equal. % 0.92/1.14 (* end of lemma zenon_L8_ *) % 0.92/1.14 assert (zenon_L9_ : ((op (e0) (e3)) = (e1)) -> ((op (e2) (e3)) = (e0)) -> False). % 0.92/1.14 do 0 intro. intros zenon_H3b zenon_H3c. % 0.92/1.14 apply (zenon_notand_s _ _ ax6); [ zenon_intro zenon_H3e | zenon_intro zenon_H3d ]. % 0.92/1.14 apply zenon_H3e. apply sym_equal. exact zenon_H3c. % 0.92/1.14 elim (classic ((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3)))); [ zenon_intro zenon_H3f | zenon_intro zenon_H40 ]. % 0.92/1.14 cut (((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3))) = ((e1) = (op (op (e2) (e3)) (e3)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H3d. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H3f. % 0.92/1.14 cut (((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H40]. % 0.92/1.14 cut (((op (op (e2) (e3)) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 0.92/1.14 congruence. % 0.92/1.14 cut (((op (e0) (e3)) = (e1)) = ((op (op (e2) (e3)) (e3)) = (e1))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H41. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H3b. % 0.92/1.14 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H1f]. % 0.92/1.14 cut (((op (e0) (e3)) = (op (op (e2) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H42]. % 0.92/1.14 congruence. % 0.92/1.14 elim (classic ((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3)))); [ zenon_intro zenon_H3f | zenon_intro zenon_H40 ]. % 0.92/1.14 cut (((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3))) = ((op (e0) (e3)) = (op (op (e2) (e3)) (e3)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H42. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H3f. % 0.92/1.14 cut (((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H40]. % 0.92/1.14 cut (((op (op (e2) (e3)) (e3)) = (op (e0) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H43]. % 0.92/1.14 congruence. % 0.92/1.14 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H3a]. % 0.92/1.14 cut (((op (e2) (e3)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H44]. % 0.92/1.14 congruence. % 0.92/1.14 exact (zenon_H44 zenon_H3c). % 0.92/1.14 apply zenon_H3a. apply refl_equal. % 0.92/1.14 apply zenon_H40. apply refl_equal. % 0.92/1.14 apply zenon_H40. apply refl_equal. % 0.92/1.14 apply zenon_H1f. apply refl_equal. % 0.92/1.14 apply zenon_H40. apply refl_equal. % 0.92/1.14 apply zenon_H40. apply refl_equal. % 0.92/1.14 (* end of lemma zenon_L9_ *) % 0.92/1.14 assert (zenon_L10_ : (~((op (e0) (e3)) = (op (e2) (e3)))) -> ((op (e0) (e3)) = (e1)) -> ((op (e2) (e3)) = (e1)) -> False). % 0.92/1.14 do 0 intro. intros zenon_H45 zenon_H3b zenon_H46. % 0.92/1.14 cut (((op (e0) (e3)) = (e1)) = ((op (e0) (e3)) = (op (e2) (e3)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H45. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H3b. % 0.92/1.14 cut (((e1) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H47]. % 0.92/1.14 cut (((op (e0) (e3)) = (op (e0) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H48]. % 0.92/1.14 congruence. % 0.92/1.14 apply zenon_H48. apply refl_equal. % 0.92/1.14 apply zenon_H47. apply sym_equal. exact zenon_H46. % 0.92/1.14 (* end of lemma zenon_L10_ *) % 0.92/1.14 assert (zenon_L11_ : (~((op (e2) (e2)) = (op (e2) (e3)))) -> ((op (e2) (e2)) = (e2)) -> ((op (e2) (e3)) = (e2)) -> False). % 0.92/1.14 do 0 intro. intros zenon_H49 zenon_H2f zenon_H4a. % 0.92/1.14 cut (((op (e2) (e2)) = (e2)) = ((op (e2) (e2)) = (op (e2) (e3)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H49. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H2f. % 0.92/1.14 cut (((e2) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 0.92/1.14 cut (((op (e2) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H32]. % 0.92/1.14 congruence. % 0.92/1.14 apply zenon_H32. apply refl_equal. % 0.92/1.14 apply zenon_H4b. apply sym_equal. exact zenon_H4a. % 0.92/1.14 (* end of lemma zenon_L11_ *) % 0.92/1.14 assert (zenon_L12_ : ((op (e3) (e3)) = (e3)) -> ((op (e2) (e3)) = (e3)) -> (~((op (e2) (e3)) = (op (e3) (e3)))) -> False). % 0.92/1.14 do 0 intro. intros zenon_H33 zenon_H4c zenon_H4d. % 0.92/1.14 elim (classic ((op (e3) (e3)) = (op (e3) (e3)))); [ zenon_intro zenon_H36 | zenon_intro zenon_H37 ]. % 0.92/1.14 cut (((op (e3) (e3)) = (op (e3) (e3))) = ((op (e2) (e3)) = (op (e3) (e3)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H4d. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H36. % 0.92/1.14 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 0.92/1.14 cut (((op (e3) (e3)) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H4e]. % 0.92/1.14 congruence. % 0.92/1.14 cut (((op (e3) (e3)) = (e3)) = ((op (e3) (e3)) = (op (e2) (e3)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H4e. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_H33. % 0.92/1.14 cut (((e3) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H4f]. % 0.92/1.14 cut (((op (e3) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 0.92/1.14 congruence. % 0.92/1.14 apply zenon_H37. apply refl_equal. % 0.92/1.14 apply zenon_H4f. apply sym_equal. exact zenon_H4c. % 0.92/1.14 apply zenon_H37. apply refl_equal. % 0.92/1.14 apply zenon_H37. apply refl_equal. % 0.92/1.14 (* end of lemma zenon_L12_ *) % 0.92/1.14 apply (zenon_and_s _ _ ax1). zenon_intro zenon_H51. zenon_intro zenon_H50. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H50). zenon_intro zenon_H53. zenon_intro zenon_H52. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H52). zenon_intro zenon_H55. zenon_intro zenon_H54. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H54). zenon_intro zenon_H57. zenon_intro zenon_H56. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H58). zenon_intro zenon_H5b. zenon_intro zenon_H5a. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H5a). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H5c). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H5e). zenon_intro zenon_H61. zenon_intro zenon_H60. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H60). zenon_intro zenon_H63. zenon_intro zenon_H62. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H62). zenon_intro zenon_H65. zenon_intro zenon_H64. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H64). zenon_intro zenon_H67. zenon_intro zenon_H66. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H66). zenon_intro zenon_H69. zenon_intro zenon_H68. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H68). zenon_intro zenon_H6b. zenon_intro zenon_H6a. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H6a). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 0.92/1.14 apply (zenon_and_s _ _ ax2). zenon_intro zenon_H6f. zenon_intro zenon_H6e. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H71. zenon_intro zenon_H70. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H70). zenon_intro zenon_H73. zenon_intro zenon_H72. % 0.92/1.14 apply (zenon_and_s _ _ ax3). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H74). zenon_intro zenon_H77. zenon_intro zenon_H76. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H76). zenon_intro zenon_H79. zenon_intro zenon_H78. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H7a). zenon_intro zenon_H7d. zenon_intro zenon_H7c. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H7c). zenon_intro zenon_H7f. zenon_intro zenon_H7e. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H7e). zenon_intro zenon_H81. zenon_intro zenon_H80. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H82). zenon_intro zenon_H85. zenon_intro zenon_H84. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H84). zenon_intro zenon_H87. zenon_intro zenon_H86. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H89. zenon_intro zenon_H88. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H88). zenon_intro zenon_H8b. zenon_intro zenon_H8a. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H8a). zenon_intro zenon_H8d. zenon_intro zenon_H8c. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H8c). zenon_intro zenon_H8f. zenon_intro zenon_H8e. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H8e). zenon_intro zenon_H2a. zenon_intro zenon_H90. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H90). zenon_intro zenon_H92. zenon_intro zenon_H91. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H94. zenon_intro zenon_H93. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H93). zenon_intro zenon_H2e. zenon_intro zenon_H95. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H95). zenon_intro zenon_H97. zenon_intro zenon_H96. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H96). zenon_intro zenon_H45. zenon_intro zenon_H98. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H98). zenon_intro zenon_H9a. zenon_intro zenon_H99. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H99). zenon_intro zenon_H9c. zenon_intro zenon_H9b. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_H9e. zenon_intro zenon_H9d. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H9d). zenon_intro zenon_H4d. zenon_intro zenon_H9f. % 0.92/1.14 apply (zenon_and_s _ _ zenon_H9f). zenon_intro zenon_Ha1. zenon_intro zenon_Ha0. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Ha0). zenon_intro zenon_Ha3. zenon_intro zenon_Ha2. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Ha2). zenon_intro zenon_Ha5. zenon_intro zenon_Ha4. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Ha4). zenon_intro zenon_Ha7. zenon_intro zenon_Ha6. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Ha6). zenon_intro zenon_Ha9. zenon_intro zenon_Ha8. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Ha8). zenon_intro zenon_Hab. zenon_intro zenon_Haa. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Haa). zenon_intro zenon_Had. zenon_intro zenon_Hac. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hac). zenon_intro zenon_Haf. zenon_intro zenon_Hae. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hae). zenon_intro zenon_Hb1. zenon_intro zenon_Hb0. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hb0). zenon_intro zenon_Hb3. zenon_intro zenon_Hb2. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hb2). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hb4). zenon_intro zenon_Hb7. zenon_intro zenon_Hb6. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hb6). zenon_intro zenon_Hb9. zenon_intro zenon_Hb8. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hb8). zenon_intro zenon_Hbb. zenon_intro zenon_Hba. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hba). zenon_intro zenon_Hbd. zenon_intro zenon_Hbc. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hbc). zenon_intro zenon_Hbf. zenon_intro zenon_Hbe. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hbe). zenon_intro zenon_Hc1. zenon_intro zenon_Hc0. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hc0). zenon_intro zenon_H49. zenon_intro zenon_Hc2. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hc2). zenon_intro zenon_Hc4. zenon_intro zenon_Hc3. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hc3). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hc7). zenon_intro zenon_Hca. zenon_intro zenon_Hc9. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hc9). zenon_intro zenon_Hcb. zenon_intro zenon_H35. % 0.92/1.14 apply (zenon_and_s _ _ ax4). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 0.92/1.14 apply (zenon_and_s _ _ ax5). zenon_intro zenon_Hcf. zenon_intro zenon_Hce. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hce). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 0.92/1.14 apply (zenon_and_s _ _ zenon_Hd0). zenon_intro zenon_H2f. zenon_intro zenon_H33. % 0.92/1.14 apply (zenon_or_s _ _ zenon_H73); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hd2 ]. % 0.92/1.14 elim (classic ((e1) = (e1))); [ zenon_intro zenon_Hd4 | zenon_intro zenon_H1f ]. % 0.92/1.14 cut (((e1) = (e1)) = ((e0) = (e1))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_Hcd. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_Hd4. % 0.92/1.14 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H1f]. % 0.92/1.14 cut (((e1) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hd5]. % 0.92/1.14 congruence. % 0.92/1.14 cut (((op (e0) (e0)) = (e0)) = ((e1) = (e0))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_Hd5. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_Hcf. % 0.92/1.14 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H1d]. % 0.92/1.14 cut (((op (e0) (e0)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 0.92/1.14 congruence. % 0.92/1.14 exact (zenon_Hd6 zenon_Hd3). % 0.92/1.14 apply zenon_H1d. apply refl_equal. % 0.92/1.14 apply zenon_H1f. apply refl_equal. % 0.92/1.14 apply zenon_H1f. apply refl_equal. % 0.92/1.14 apply (zenon_or_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd8 | zenon_intro zenon_Hd7 ]. % 0.92/1.14 elim (classic ((op (e1) (e1)) = (op (e1) (e1)))); [ zenon_intro zenon_Hd9 | zenon_intro zenon_Hda ]. % 0.92/1.14 cut (((op (e1) (e1)) = (op (e1) (e1))) = ((op (e0) (e1)) = (op (e1) (e1)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_H81. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_Hd9. % 0.92/1.14 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hda]. % 0.92/1.14 cut (((op (e1) (e1)) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 0.92/1.14 congruence. % 0.92/1.14 cut (((op (e1) (e1)) = (e1)) = ((op (e1) (e1)) = (op (e0) (e1)))). % 0.92/1.14 intro zenon_D_pnotp. % 0.92/1.14 apply zenon_Hdb. % 0.92/1.14 rewrite <- zenon_D_pnotp. % 0.92/1.14 exact zenon_Hd1. % 0.92/1.14 cut (((e1) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hdc]. % 0.92/1.14 cut (((op (e1) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hda]. % 0.92/1.14 congruence. % 0.92/1.14 apply zenon_Hda. apply refl_equal. % 0.92/1.14 apply zenon_Hdc. apply sym_equal. exact zenon_Hd8. % 0.92/1.14 apply zenon_Hda. apply refl_equal. % 0.92/1.14 apply zenon_Hda. apply refl_equal. % 0.92/1.14 apply (zenon_or_s _ _ zenon_Hd7); [ zenon_intro zenon_H20 | zenon_intro zenon_H3b ]. % 0.92/1.14 apply (zenon_or_s _ _ zenon_H6d); [ zenon_intro zenon_H21 | zenon_intro zenon_Hdd ]. % 0.92/1.14 apply (zenon_L4_); trivial. % 0.92/1.14 apply (zenon_or_s _ _ zenon_Hdd); [ zenon_intro zenon_H2b | zenon_intro zenon_Hde ]. % 0.92/1.14 apply (zenon_L5_); trivial. % 0.92/1.14 apply (zenon_or_s _ _ zenon_Hde); [ zenon_intro zenon_H30 | zenon_intro zenon_H34 ]. % 0.92/1.14 apply (zenon_L6_); trivial. % 0.92/1.14 apply (zenon_L7_); trivial. % 0.92/1.14 apply (zenon_or_s _ _ zenon_H67); [ zenon_intro zenon_H3c | zenon_intro zenon_Hdf ]. % 0.92/1.14 apply (zenon_L9_); trivial. % 0.92/1.14 apply (zenon_or_s _ _ zenon_Hdf); [ zenon_intro zenon_H46 | zenon_intro zenon_He0 ]. % 0.92/1.14 apply (zenon_L10_); trivial. % 0.92/1.14 apply (zenon_or_s _ _ zenon_He0); [ zenon_intro zenon_H4a | zenon_intro zenon_H4c ]. % 0.92/1.14 apply (zenon_L11_); trivial. % 0.92/1.14 apply (zenon_L12_); trivial. % 0.92/1.14 Qed. % 0.92/1.14 % SZS output end Proof % 0.92/1.14 (* END-PROOF *) % 0.92/1.14 nodes searched: 18402 % 0.92/1.14 max branch formulas: 275 % 0.92/1.14 proof nodes created: 916 % 0.92/1.14 formulas created: 9399 % 0.92/1.14 %------------------------------------------------------------------------------