%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS080+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n027.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:23 EDT 2022 % Result : Unsatisfiable 1.31s 1.48s % Output : Proof 1.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : KRS080+1 : TPTP v8.1.0. Released v3.1.0. % 0.00/0.11 % Command : run_zenon %s %d % 0.11/0.32 % Computer : n027.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Tue Jun 7 20:25:55 EDT 2022 % 0.11/0.32 % CPUTime : % 1.31/1.48 (* PROOF-FOUND *) % 1.31/1.48 % SZS status Unsatisfiable % 1.31/1.48 (* BEGIN-PROOF *) % 1.31/1.48 % SZS output start Proof % 1.31/1.48 Theorem zenon_thm : False. % 1.31/1.48 Proof. % 1.31/1.48 assert (zenon_L1_ : forall (zenon_TY_z : zenon_U) (zenon_TY_ba : zenon_U), (forall B : zenon_U, (((zenon_TY_ba = B)/\(cp3 zenon_TY_ba))->(cp3 B))) -> (zenon_TY_ba = zenon_TY_z) -> (cp3 zenon_TY_ba) -> (~(cp3 zenon_TY_z)) -> False). % 1.31/1.48 do 2 intro. intros zenon_H15 zenon_H16 zenon_H17 zenon_H18. % 1.31/1.48 generalize (zenon_H15 zenon_TY_z). zenon_intro zenon_H1b. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H1b); [ zenon_intro zenon_H1d | zenon_intro zenon_H1c ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H1d); [ zenon_intro zenon_H1f | zenon_intro zenon_H1e ]. % 1.31/1.48 exact (zenon_H1f zenon_H16). % 1.31/1.48 exact (zenon_H1e zenon_H17). % 1.31/1.48 exact (zenon_H18 zenon_H1c). % 1.31/1.48 (* end of lemma zenon_L1_ *) % 1.31/1.48 assert (zenon_L2_ : forall (zenon_TY_ba : zenon_U) (zenon_TY_z : zenon_U), (~(cp3 zenon_TY_z)) -> (cp3 zenon_TY_ba) -> (zenon_TY_ba = zenon_TY_z) -> False). % 1.31/1.48 do 2 intro. intros zenon_H18 zenon_H17 zenon_H16. % 1.31/1.48 generalize (cp3_substitution_1 zenon_TY_ba). zenon_intro zenon_H15. % 1.31/1.48 apply (zenon_L1_ zenon_TY_z zenon_TY_ba); trivial. % 1.31/1.48 (* end of lemma zenon_L2_ *) % 1.31/1.48 assert (zenon_L3_ : forall (zenon_TY_ba : zenon_U) (zenon_TY_bk : zenon_U), (forall B : zenon_U, (((zenon_TY_bk = B)/\(cp1 zenon_TY_bk))->(cp1 B))) -> (zenon_TY_ba = zenon_TY_bk) -> (cp1 zenon_TY_bk) -> (~(cp1 zenon_TY_ba)) -> False). % 1.31/1.48 do 2 intro. intros zenon_H20 zenon_H21 zenon_H22 zenon_H23. % 1.31/1.48 generalize (zenon_H20 zenon_TY_ba). zenon_intro zenon_H25. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H25); [ zenon_intro zenon_H27 | zenon_intro zenon_H26 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H27); [ zenon_intro zenon_H29 | zenon_intro zenon_H28 ]. % 1.31/1.48 apply zenon_H29. apply sym_equal. exact zenon_H21. % 1.31/1.48 exact (zenon_H28 zenon_H22). % 1.31/1.48 exact (zenon_H23 zenon_H26). % 1.31/1.48 (* end of lemma zenon_L3_ *) % 1.31/1.48 assert (zenon_L4_ : forall (zenon_TY_bt : zenon_U) (zenon_TY_z : zenon_U), (~(cp2 zenon_TY_z)) -> (cp2 zenon_TY_bt) -> (zenon_TY_z = zenon_TY_bt) -> False). % 1.31/1.48 do 2 intro. intros zenon_H2a zenon_H2b zenon_H2c. % 1.31/1.48 generalize (cp2_substitution_1 zenon_TY_bt). zenon_intro zenon_H2e. % 1.31/1.48 generalize (zenon_H2e zenon_TY_z). zenon_intro zenon_H2f. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H2f); [ zenon_intro zenon_H31 | zenon_intro zenon_H30 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H31); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 1.31/1.48 apply zenon_H33. apply sym_equal. exact zenon_H2c. % 1.31/1.48 exact (zenon_H32 zenon_H2b). % 1.31/1.48 exact (zenon_H2a zenon_H30). % 1.31/1.48 (* end of lemma zenon_L4_ *) % 1.31/1.48 assert (zenon_L5_ : forall (zenon_TY_z : zenon_U) (zenon_TY_bk : zenon_U), (forall B : zenon_U, (((zenon_TY_bk = B)/\(cp1 zenon_TY_bk))->(cp1 B))) -> (zenon_TY_z = zenon_TY_bk) -> (cp1 zenon_TY_bk) -> (~(cp1 zenon_TY_z)) -> False). % 1.31/1.48 do 2 intro. intros zenon_H20 zenon_H34 zenon_H22 zenon_H35. % 1.31/1.48 generalize (zenon_H20 zenon_TY_z). zenon_intro zenon_H36. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H36); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H39 | zenon_intro zenon_H28 ]. % 1.31/1.48 apply zenon_H39. apply sym_equal. exact zenon_H34. % 1.31/1.48 exact (zenon_H28 zenon_H22). % 1.31/1.48 exact (zenon_H35 zenon_H37). % 1.31/1.48 (* end of lemma zenon_L5_ *) % 1.31/1.48 assert (zenon_L6_ : forall (zenon_TY_ba : zenon_U) (zenon_TY_cj : zenon_U), (forall B : zenon_U, (((zenon_TY_cj = B)/\(cp1 zenon_TY_cj))->(cp1 B))) -> (zenon_TY_ba = zenon_TY_cj) -> (cp1 zenon_TY_cj) -> (~(cp1 zenon_TY_ba)) -> False). % 1.31/1.48 do 2 intro. intros zenon_H3a zenon_H3b zenon_H3c zenon_H23. % 1.31/1.48 generalize (zenon_H3a zenon_TY_ba). zenon_intro zenon_H3e. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H3f | zenon_intro zenon_H26 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 1.31/1.48 apply zenon_H41. apply sym_equal. exact zenon_H3b. % 1.31/1.48 exact (zenon_H40 zenon_H3c). % 1.31/1.48 exact (zenon_H23 zenon_H26). % 1.31/1.48 (* end of lemma zenon_L6_ *) % 1.31/1.48 assert (zenon_L7_ : forall (zenon_TY_z : zenon_U) (zenon_TY_cj : zenon_U), (forall B : zenon_U, (((zenon_TY_cj = B)/\(cp1 zenon_TY_cj))->(cp1 B))) -> (zenon_TY_z = zenon_TY_cj) -> (cp1 zenon_TY_cj) -> (~(cp1 zenon_TY_z)) -> False). % 1.31/1.48 do 2 intro. intros zenon_H3a zenon_H42 zenon_H3c zenon_H35. % 1.31/1.48 generalize (zenon_H3a zenon_TY_z). zenon_intro zenon_H43. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H43); [ zenon_intro zenon_H44 | zenon_intro zenon_H37 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H44); [ zenon_intro zenon_H45 | zenon_intro zenon_H40 ]. % 1.31/1.48 apply zenon_H45. apply sym_equal. exact zenon_H42. % 1.31/1.48 exact (zenon_H40 zenon_H3c). % 1.31/1.48 exact (zenon_H35 zenon_H37). % 1.31/1.48 (* end of lemma zenon_L7_ *) % 1.31/1.48 assert (zenon_L8_ : forall (zenon_TY_cj : zenon_U) (zenon_TY_z : zenon_U) (zenon_TY_ba : zenon_U) (zenon_TY_bk : zenon_U) (zenon_TY_bt : zenon_U), (zenon_TY_bt = zenon_TY_bk) -> (zenon_TY_ba = zenon_TY_bt) -> (~(cp1 zenon_TY_z)) -> (cp1 zenon_TY_bk) -> (forall B : zenon_U, (((zenon_TY_bk = B)/\(cp1 zenon_TY_bk))->(cp1 B))) -> (~(cp1 zenon_TY_ba)) -> (cp1 zenon_TY_cj) -> (forall B : zenon_U, (((zenon_TY_cj = B)/\(cp1 zenon_TY_cj))->(cp1 B))) -> (~(cp3 zenon_TY_z)) -> (cp3 zenon_TY_ba) -> (rr (i2003_11_14_17_19_21224) zenon_TY_bk) -> (rr (i2003_11_14_17_19_21224) zenon_TY_cj) -> (rr (i2003_11_14_17_19_21224) zenon_TY_z) -> (rr (i2003_11_14_17_19_21224) zenon_TY_ba) -> (forall Y3 : zenon_U, (((rr (i2003_11_14_17_19_21224) zenon_TY_ba)/\((rr (i2003_11_14_17_19_21224) zenon_TY_z)/\((rr (i2003_11_14_17_19_21224) zenon_TY_cj)/\(rr (i2003_11_14_17_19_21224) Y3))))->((zenon_TY_ba = zenon_TY_z)\/((zenon_TY_ba = zenon_TY_cj)\/((zenon_TY_ba = Y3)\/((zenon_TY_z = zenon_TY_cj)\/((zenon_TY_z = Y3)\/(zenon_TY_cj = Y3)))))))) -> False). % 1.31/1.48 do 5 intro. intros zenon_H46 zenon_H47 zenon_H35 zenon_H22 zenon_H20 zenon_H23 zenon_H3c zenon_H3a zenon_H18 zenon_H17 zenon_H48 zenon_H49 zenon_H4a zenon_H4b zenon_H4c. % 1.31/1.48 generalize (cp3_substitution_1 zenon_TY_ba). zenon_intro zenon_H15. % 1.31/1.48 generalize (zenon_H4c zenon_TY_bk). zenon_intro zenon_H4d. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H4d); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 1.31/1.48 exact (zenon_H51 zenon_H4b). % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H50); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 1.31/1.48 exact (zenon_H53 zenon_H4a). % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H55 | zenon_intro zenon_H54 ]. % 1.31/1.48 exact (zenon_H55 zenon_H49). % 1.31/1.48 exact (zenon_H54 zenon_H48). % 1.31/1.48 apply (zenon_or_s _ _ zenon_H4e); [ zenon_intro zenon_H16 | zenon_intro zenon_H56 ]. % 1.31/1.48 apply (zenon_L1_ zenon_TY_z zenon_TY_ba); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_H56); [ zenon_intro zenon_H3b | zenon_intro zenon_H57 ]. % 1.31/1.48 apply (zenon_L6_ zenon_TY_ba zenon_TY_cj); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_H57); [ zenon_intro zenon_H21 | zenon_intro zenon_H58 ]. % 1.31/1.48 apply (zenon_L3_ zenon_TY_ba zenon_TY_bk); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_H58); [ zenon_intro zenon_H42 | zenon_intro zenon_H59 ]. % 1.31/1.48 apply (zenon_L7_ zenon_TY_z zenon_TY_cj); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_H59); [ zenon_intro zenon_H34 | zenon_intro zenon_H5a ]. % 1.31/1.48 apply (zenon_L5_ zenon_TY_z zenon_TY_bk); trivial. % 1.31/1.48 generalize (zenon_H3a zenon_TY_ba). zenon_intro zenon_H3e. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H3e); [ zenon_intro zenon_H3f | zenon_intro zenon_H26 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 1.31/1.48 cut ((zenon_TY_cj = zenon_TY_bk) = (zenon_TY_cj = zenon_TY_ba)). % 1.31/1.48 intro zenon_D_pnotp. % 1.31/1.48 apply zenon_H41. % 1.31/1.48 rewrite <- zenon_D_pnotp. % 1.31/1.48 exact zenon_H5a. % 1.31/1.48 cut ((zenon_TY_bk = zenon_TY_ba)); [idtac | apply NNPP; zenon_intro zenon_H29]. % 1.31/1.48 cut ((zenon_TY_cj = zenon_TY_cj)); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 1.31/1.48 congruence. % 1.31/1.48 apply zenon_H5b. apply refl_equal. % 1.31/1.48 elim (classic (zenon_TY_ba = zenon_TY_ba)); [ zenon_intro zenon_H5c | zenon_intro zenon_H5d ]. % 1.31/1.48 cut ((zenon_TY_ba = zenon_TY_ba) = (zenon_TY_bk = zenon_TY_ba)). % 1.31/1.48 intro zenon_D_pnotp. % 1.31/1.48 apply zenon_H29. % 1.31/1.48 rewrite <- zenon_D_pnotp. % 1.31/1.48 exact zenon_H5c. % 1.31/1.48 cut ((zenon_TY_ba = zenon_TY_ba)); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 1.31/1.48 cut ((zenon_TY_ba = zenon_TY_bk)); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 1.31/1.48 congruence. % 1.31/1.48 cut ((zenon_TY_bt = zenon_TY_bk) = (zenon_TY_ba = zenon_TY_bk)). % 1.31/1.48 intro zenon_D_pnotp. % 1.31/1.48 apply zenon_H5e. % 1.31/1.48 rewrite <- zenon_D_pnotp. % 1.31/1.48 exact zenon_H46. % 1.31/1.48 cut ((zenon_TY_bk = zenon_TY_bk)); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 1.31/1.48 cut ((zenon_TY_bt = zenon_TY_ba)); [idtac | apply NNPP; zenon_intro zenon_H60]. % 1.31/1.48 congruence. % 1.31/1.48 elim (classic (zenon_TY_ba = zenon_TY_ba)); [ zenon_intro zenon_H5c | zenon_intro zenon_H5d ]. % 1.31/1.48 cut ((zenon_TY_ba = zenon_TY_ba) = (zenon_TY_bt = zenon_TY_ba)). % 1.31/1.48 intro zenon_D_pnotp. % 1.31/1.48 apply zenon_H60. % 1.31/1.48 rewrite <- zenon_D_pnotp. % 1.31/1.48 exact zenon_H5c. % 1.31/1.48 cut ((zenon_TY_ba = zenon_TY_ba)); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 1.31/1.48 cut ((zenon_TY_ba = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H61]. % 1.31/1.48 congruence. % 1.31/1.48 exact (zenon_H61 zenon_H47). % 1.31/1.48 apply zenon_H5d. apply refl_equal. % 1.31/1.48 apply zenon_H5d. apply refl_equal. % 1.31/1.48 apply zenon_H5f. apply refl_equal. % 1.31/1.48 apply zenon_H5d. apply refl_equal. % 1.31/1.48 apply zenon_H5d. apply refl_equal. % 1.31/1.48 exact (zenon_H40 zenon_H3c). % 1.31/1.48 exact (zenon_H23 zenon_H26). % 1.31/1.48 (* end of lemma zenon_L8_ *) % 1.31/1.48 assert (zenon_L9_ : forall (zenon_TY_z : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TY_bk : zenon_U), (forall B : zenon_U, (((zenon_TY_bk = B)/\(cp1 zenon_TY_bk))->(cp1 B))) -> (zenon_TY_bt = zenon_TY_bk) -> (zenon_TY_z = zenon_TY_bt) -> (cp1 zenon_TY_bk) -> (~(cp1 zenon_TY_z)) -> False). % 1.31/1.48 do 3 intro. intros zenon_H20 zenon_H46 zenon_H2c zenon_H22 zenon_H35. % 1.31/1.48 generalize (zenon_H20 zenon_TY_z). zenon_intro zenon_H36. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H36); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H39 | zenon_intro zenon_H28 ]. % 1.31/1.48 elim (classic (zenon_TY_z = zenon_TY_z)); [ zenon_intro zenon_H62 | zenon_intro zenon_H63 ]. % 1.31/1.48 cut ((zenon_TY_z = zenon_TY_z) = (zenon_TY_bk = zenon_TY_z)). % 1.31/1.48 intro zenon_D_pnotp. % 1.31/1.48 apply zenon_H39. % 1.31/1.48 rewrite <- zenon_D_pnotp. % 1.31/1.48 exact zenon_H62. % 1.31/1.48 cut ((zenon_TY_z = zenon_TY_z)); [idtac | apply NNPP; zenon_intro zenon_H63]. % 1.31/1.48 cut ((zenon_TY_z = zenon_TY_bk)); [idtac | apply NNPP; zenon_intro zenon_H64]. % 1.31/1.48 congruence. % 1.31/1.48 cut ((zenon_TY_bt = zenon_TY_bk) = (zenon_TY_z = zenon_TY_bk)). % 1.31/1.48 intro zenon_D_pnotp. % 1.31/1.48 apply zenon_H64. % 1.31/1.48 rewrite <- zenon_D_pnotp. % 1.31/1.48 exact zenon_H46. % 1.31/1.48 cut ((zenon_TY_bk = zenon_TY_bk)); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 1.31/1.48 cut ((zenon_TY_bt = zenon_TY_z)); [idtac | apply NNPP; zenon_intro zenon_H33]. % 1.31/1.48 congruence. % 1.31/1.48 elim (classic (zenon_TY_z = zenon_TY_z)); [ zenon_intro zenon_H62 | zenon_intro zenon_H63 ]. % 1.31/1.48 cut ((zenon_TY_z = zenon_TY_z) = (zenon_TY_bt = zenon_TY_z)). % 1.31/1.48 intro zenon_D_pnotp. % 1.31/1.48 apply zenon_H33. % 1.31/1.48 rewrite <- zenon_D_pnotp. % 1.31/1.48 exact zenon_H62. % 1.31/1.48 cut ((zenon_TY_z = zenon_TY_z)); [idtac | apply NNPP; zenon_intro zenon_H63]. % 1.31/1.48 cut ((zenon_TY_z = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H65]. % 1.31/1.48 congruence. % 1.31/1.48 exact (zenon_H65 zenon_H2c). % 1.31/1.48 apply zenon_H63. apply refl_equal. % 1.31/1.48 apply zenon_H63. apply refl_equal. % 1.31/1.48 apply zenon_H5f. apply refl_equal. % 1.31/1.48 apply zenon_H63. apply refl_equal. % 1.31/1.48 apply zenon_H63. apply refl_equal. % 1.31/1.48 exact (zenon_H28 zenon_H22). % 1.31/1.48 exact (zenon_H35 zenon_H37). % 1.31/1.48 (* end of lemma zenon_L9_ *) % 1.31/1.48 assert (zenon_L10_ : forall (zenon_TY_bk : zenon_U) (zenon_TY_cj : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TY_z : zenon_U) (zenon_TY_ba : zenon_U), (forall Y3 : zenon_U, (((rr (i2003_11_14_17_19_21224) zenon_TY_ba)/\((rr (i2003_11_14_17_19_21224) zenon_TY_z)/\((rr (i2003_11_14_17_19_21224) zenon_TY_bt)/\(rr (i2003_11_14_17_19_21224) Y3))))->((zenon_TY_ba = zenon_TY_z)\/((zenon_TY_ba = zenon_TY_bt)\/((zenon_TY_ba = Y3)\/((zenon_TY_z = zenon_TY_bt)\/((zenon_TY_z = Y3)\/(zenon_TY_bt = Y3)))))))) -> (rr (i2003_11_14_17_19_21224) zenon_TY_ba) -> (rr (i2003_11_14_17_19_21224) zenon_TY_z) -> (rr (i2003_11_14_17_19_21224) zenon_TY_bt) -> (rr (i2003_11_14_17_19_21224) zenon_TY_cj) -> (~(cp3 zenon_TY_z)) -> (cp3 zenon_TY_ba) -> (zenon_TY_bt = zenon_TY_bk) -> (~(cp1 zenon_TY_z)) -> (cp1 zenon_TY_bk) -> (forall B : zenon_U, (((zenon_TY_bk = B)/\(cp1 zenon_TY_bk))->(cp1 B))) -> (~(cp1 zenon_TY_ba)) -> (cp1 zenon_TY_cj) -> (forall B : zenon_U, (((zenon_TY_cj = B)/\(cp1 zenon_TY_cj))->(cp1 B))) -> (rr (i2003_11_14_17_19_21224) zenon_TY_bk) -> (forall Y3 : zenon_U, (((rr (i2003_11_14_17_19_21224) zenon_TY_ba)/\((rr (i2003_11_14_17_19_21224) zenon_TY_z)/\((rr (i2003_11_14_17_19_21224) zenon_TY_cj)/\(rr (i2003_11_14_17_19_21224) Y3))))->((zenon_TY_ba = zenon_TY_z)\/((zenon_TY_ba = zenon_TY_cj)\/((zenon_TY_ba = Y3)\/((zenon_TY_z = zenon_TY_cj)\/((zenon_TY_z = Y3)\/(zenon_TY_cj = Y3)))))))) -> (~(cp1 zenon_TY_bt)) -> False). % 1.31/1.48 do 5 intro. intros zenon_H66 zenon_H4b zenon_H4a zenon_H67 zenon_H49 zenon_H18 zenon_H17 zenon_H46 zenon_H35 zenon_H22 zenon_H20 zenon_H23 zenon_H3c zenon_H3a zenon_H48 zenon_H4c zenon_H68. % 1.31/1.48 generalize (zenon_H66 zenon_TY_cj). zenon_intro zenon_H69. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H69); [ zenon_intro zenon_H6b | zenon_intro zenon_H6a ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H6b); [ zenon_intro zenon_H51 | zenon_intro zenon_H6c ]. % 1.31/1.48 exact (zenon_H51 zenon_H4b). % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H6c); [ zenon_intro zenon_H53 | zenon_intro zenon_H6d ]. % 1.31/1.48 exact (zenon_H53 zenon_H4a). % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H6e | zenon_intro zenon_H55 ]. % 1.31/1.48 exact (zenon_H6e zenon_H67). % 1.31/1.48 exact (zenon_H55 zenon_H49). % 1.31/1.48 apply (zenon_or_s _ _ zenon_H6a); [ zenon_intro zenon_H16 | zenon_intro zenon_H6f ]. % 1.31/1.48 apply (zenon_L2_ zenon_TY_ba zenon_TY_z); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_H6f); [ zenon_intro zenon_H47 | zenon_intro zenon_H70 ]. % 1.31/1.48 apply (zenon_L8_ zenon_TY_cj zenon_TY_z zenon_TY_ba zenon_TY_bk zenon_TY_bt); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_H70); [ zenon_intro zenon_H3b | zenon_intro zenon_H71 ]. % 1.31/1.48 apply (zenon_L6_ zenon_TY_ba zenon_TY_cj); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_H71); [ zenon_intro zenon_H2c | zenon_intro zenon_H72 ]. % 1.31/1.48 apply (zenon_L9_ zenon_TY_z zenon_TY_bt zenon_TY_bk); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_H72); [ zenon_intro zenon_H42 | zenon_intro zenon_H73 ]. % 1.31/1.48 apply (zenon_L7_ zenon_TY_z zenon_TY_cj); trivial. % 1.31/1.48 generalize (zenon_H3a zenon_TY_bt). zenon_intro zenon_H74. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_H74); [ zenon_intro zenon_H76 | zenon_intro zenon_H75 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H77 | zenon_intro zenon_H40 ]. % 1.31/1.48 apply zenon_H77. apply sym_equal. exact zenon_H73. % 1.31/1.48 exact (zenon_H40 zenon_H3c). % 1.31/1.48 exact (zenon_H68 zenon_H75). % 1.31/1.48 (* end of lemma zenon_L10_ *) % 1.31/1.48 assert (zenon_L11_ : forall (zenon_TY_z : zenon_U), (~((cp4 zenon_TY_z)\/(cp5 zenon_TY_z))) -> (cp4 zenon_TY_z) -> False). % 1.31/1.48 do 1 intro. intros zenon_H78 zenon_H79. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 1.31/1.48 exact (zenon_H7b zenon_H79). % 1.31/1.48 (* end of lemma zenon_L11_ *) % 1.31/1.48 assert (zenon_L12_ : forall (zenon_TY_ba : zenon_U), (~((cp4 zenon_TY_ba)\/((cp5 zenon_TY_ba)\/(cp3 zenon_TY_ba)))) -> (cp3 zenon_TY_ba) -> False). % 1.31/1.48 do 1 intro. intros zenon_H7c zenon_H17. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H7c). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H7d). zenon_intro zenon_H7f. zenon_intro zenon_H1e. % 1.31/1.48 exact (zenon_H1e zenon_H17). % 1.31/1.48 (* end of lemma zenon_L12_ *) % 1.31/1.48 assert (zenon_L13_ : forall (zenon_TY_z : zenon_U), (~((cp4 zenon_TY_z)\/((cp5 zenon_TY_z)\/(cp3 zenon_TY_z)))) -> (cp4 zenon_TY_z) -> False). % 1.31/1.48 do 1 intro. intros zenon_H80 zenon_H79. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H80). zenon_intro zenon_H7b. zenon_intro zenon_H81. % 1.31/1.48 exact (zenon_H7b zenon_H79). % 1.31/1.48 (* end of lemma zenon_L13_ *) % 1.31/1.48 assert (zenon_L14_ : forall (zenon_TY_ba : zenon_U), (~((cp2 zenon_TY_ba)\/((cp4 zenon_TY_ba)\/((cp5 zenon_TY_ba)\/(cp3 zenon_TY_ba))))) -> (cp3 zenon_TY_ba) -> False). % 1.31/1.48 do 1 intro. intros zenon_H82 zenon_H17. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H82). zenon_intro zenon_H83. zenon_intro zenon_H7c. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H7c). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H7d). zenon_intro zenon_H7f. zenon_intro zenon_H1e. % 1.31/1.48 exact (zenon_H1e zenon_H17). % 1.31/1.48 (* end of lemma zenon_L14_ *) % 1.31/1.48 assert (zenon_L15_ : 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). % 1.31/1.48 do 1 intro. intros zenon_H84 zenon_H79. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H84). zenon_intro zenon_H2a. zenon_intro zenon_H80. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H80). zenon_intro zenon_H7b. zenon_intro zenon_H81. % 1.31/1.48 exact (zenon_H7b zenon_H79). % 1.31/1.48 (* end of lemma zenon_L15_ *) % 1.31/1.48 assert (zenon_L16_ : forall (zenon_TY_bt : zenon_U), (~((cp2 zenon_TY_bt)\/((cp4 zenon_TY_bt)\/((cp5 zenon_TY_bt)\/(cp3 zenon_TY_bt))))) -> (cp2 zenon_TY_bt) -> False). % 1.31/1.48 do 1 intro. intros zenon_H85 zenon_H2b. % 1.31/1.48 apply (zenon_notor_s _ _ zenon_H85). zenon_intro zenon_H32. zenon_intro zenon_H86. % 1.31/1.48 exact (zenon_H32 zenon_H2b). % 1.31/1.48 (* end of lemma zenon_L16_ *) % 1.31/1.48 generalize (axiom_2 (i2003_11_14_17_19_21224)). zenon_intro zenon_H87. % 1.31/1.48 apply (zenon_equiv_s _ _ zenon_H87); [ zenon_intro zenon_H8a; zenon_intro zenon_H89 | zenon_intro axiom_7; zenon_intro zenon_H88 ]. % 1.31/1.48 exact (zenon_H8a axiom_7). % 1.31/1.48 apply (zenon_and_s _ _ zenon_H88). zenon_intro zenon_H8c. zenon_intro zenon_H8b. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H8b). zenon_intro zenon_H8e. zenon_intro zenon_H8d. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H8d). zenon_intro zenon_H90. zenon_intro zenon_H8f. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H8f). zenon_intro zenon_H92. zenon_intro zenon_H91. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H91). zenon_intro zenon_H94. zenon_intro zenon_H93. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H93). zenon_intro zenon_H96. zenon_intro zenon_H95. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H95). zenon_intro zenon_H98. zenon_intro zenon_H97. % 1.31/1.48 elim zenon_H8c. zenon_intro zenon_TY_cj. zenon_intro zenon_H99. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H99). zenon_intro zenon_H49. zenon_intro zenon_H9a. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H9a). zenon_intro zenon_H9b. zenon_intro zenon_H3c. % 1.31/1.48 elim zenon_H8e. zenon_intro zenon_TY_bk. zenon_intro zenon_H9c. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H9c). zenon_intro zenon_H48. zenon_intro zenon_H22. % 1.31/1.48 elim zenon_H90. zenon_intro zenon_TY_z. zenon_intro zenon_H9d. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H9d). zenon_intro zenon_H4a. zenon_intro zenon_H79. % 1.31/1.48 elim zenon_H96. zenon_intro zenon_TY_ba. zenon_intro zenon_H9e. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H9e). zenon_intro zenon_H4b. zenon_intro zenon_H17. % 1.31/1.48 elim zenon_H97. zenon_intro zenon_TY_bt. zenon_intro zenon_H9f. % 1.31/1.48 apply (zenon_and_s _ _ zenon_H9f). zenon_intro zenon_H67. zenon_intro zenon_Ha0. % 1.31/1.48 apply (zenon_and_s _ _ zenon_Ha0). zenon_intro zenon_H2b. zenon_intro zenon_Ha1. % 1.31/1.48 generalize (axiom_3 zenon_TY_bt). zenon_intro zenon_Ha2. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_Ha2); [ zenon_intro zenon_H68 | zenon_intro zenon_H85 ]. % 1.31/1.48 generalize (axiom_3 zenon_TY_z). zenon_intro zenon_Ha3. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_Ha3); [ zenon_intro zenon_H35 | zenon_intro zenon_H84 ]. % 1.31/1.48 generalize (axiom_3 zenon_TY_ba). zenon_intro zenon_Ha4. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_Ha4); [ zenon_intro zenon_H23 | zenon_intro zenon_H82 ]. % 1.31/1.48 generalize (axiom_4 zenon_TY_z). zenon_intro zenon_Ha5. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_Ha5); [ zenon_intro zenon_H2a | zenon_intro zenon_H80 ]. % 1.31/1.48 generalize (axiom_4 zenon_TY_ba). zenon_intro zenon_Ha6. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_Ha6); [ zenon_intro zenon_H83 | zenon_intro zenon_H7c ]. % 1.31/1.48 generalize (axiom_5 zenon_TY_z). zenon_intro zenon_Ha7. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_Ha7); [ zenon_intro zenon_H18 | zenon_intro zenon_H78 ]. % 1.31/1.48 generalize (zenon_H92 zenon_TY_ba). zenon_intro zenon_Ha8. % 1.31/1.48 generalize (zenon_Ha8 zenon_TY_z). zenon_intro zenon_Ha9. % 1.31/1.48 generalize (zenon_Ha9 zenon_TY_bt). zenon_intro zenon_H66. % 1.31/1.48 generalize (cp1_substitution_1 zenon_TY_cj). zenon_intro zenon_H3a. % 1.31/1.48 generalize (zenon_Ha9 zenon_TY_cj). zenon_intro zenon_H4c. % 1.31/1.48 generalize (cp1_substitution_1 zenon_TY_bk). zenon_intro zenon_H20. % 1.31/1.48 generalize (zenon_H66 zenon_TY_bk). zenon_intro zenon_Haa. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_Haa); [ zenon_intro zenon_Hac | zenon_intro zenon_Hab ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_Hac); [ zenon_intro zenon_H51 | zenon_intro zenon_Had ]. % 1.31/1.48 exact (zenon_H51 zenon_H4b). % 1.31/1.48 apply (zenon_notand_s _ _ zenon_Had); [ zenon_intro zenon_H53 | zenon_intro zenon_Hae ]. % 1.31/1.48 exact (zenon_H53 zenon_H4a). % 1.31/1.48 apply (zenon_notand_s _ _ zenon_Hae); [ zenon_intro zenon_H6e | zenon_intro zenon_H54 ]. % 1.31/1.48 exact (zenon_H6e zenon_H67). % 1.31/1.48 exact (zenon_H54 zenon_H48). % 1.31/1.48 apply (zenon_or_s _ _ zenon_Hab); [ zenon_intro zenon_H16 | zenon_intro zenon_Haf ]. % 1.31/1.48 apply (zenon_L2_ zenon_TY_ba zenon_TY_z); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_Haf); [ zenon_intro zenon_H47 | zenon_intro zenon_Hb0 ]. % 1.31/1.48 generalize (cp2_substitution_1 zenon_TY_bt). zenon_intro zenon_H2e. % 1.31/1.48 generalize (zenon_H2e zenon_TY_ba). zenon_intro zenon_Hb1. % 1.31/1.48 apply (zenon_imply_s _ _ zenon_Hb1); [ zenon_intro zenon_Hb3 | zenon_intro zenon_Hb2 ]. % 1.31/1.48 apply (zenon_notand_s _ _ zenon_Hb3); [ zenon_intro zenon_H60 | zenon_intro zenon_H32 ]. % 1.31/1.48 apply zenon_H60. apply sym_equal. exact zenon_H47. % 1.31/1.48 exact (zenon_H32 zenon_H2b). % 1.31/1.48 exact (zenon_H83 zenon_Hb2). % 1.31/1.48 apply (zenon_or_s _ _ zenon_Hb0); [ zenon_intro zenon_H21 | zenon_intro zenon_Hb4 ]. % 1.31/1.48 apply (zenon_L3_ zenon_TY_ba zenon_TY_bk); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_Hb4); [ zenon_intro zenon_H2c | zenon_intro zenon_Hb5 ]. % 1.31/1.48 apply (zenon_L4_ zenon_TY_bt zenon_TY_z); trivial. % 1.31/1.48 apply (zenon_or_s _ _ zenon_Hb5); [ zenon_intro zenon_H34 | zenon_intro zenon_H46 ]. % 1.31/1.48 apply (zenon_L5_ zenon_TY_z zenon_TY_bk); trivial. % 1.31/1.48 apply (zenon_L10_ zenon_TY_bk zenon_TY_cj zenon_TY_bt zenon_TY_z zenon_TY_ba); trivial. % 1.31/1.48 apply (zenon_L11_ zenon_TY_z); trivial. % 1.31/1.48 apply (zenon_L12_ zenon_TY_ba); trivial. % 1.31/1.48 apply (zenon_L13_ zenon_TY_z); trivial. % 1.31/1.48 apply (zenon_L14_ zenon_TY_ba); trivial. % 1.31/1.48 apply (zenon_L15_ zenon_TY_z); trivial. % 1.31/1.48 apply (zenon_L16_ zenon_TY_bt); trivial. % 1.31/1.48 Qed. % 1.31/1.48 % SZS output end Proof % 1.31/1.48 (* END-PROOF *) % 1.31/1.48 nodes searched: 75950 % 1.31/1.48 max branch formulas: 5060 % 1.31/1.48 proof nodes created: 1101 % 1.31/1.48 formulas created: 181290 % 1.31/1.48 %------------------------------------------------------------------------------