%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : KRS138+1 : TPTP v8.1.0. Released v3.1.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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 03:39:34 EDT 2022 % Result : Theorem 0.94s 1.10s % Output : Proof 0.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : KRS138+1 : TPTP v8.1.0. Released v3.1.0. % 0.07/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jun 7 10:50:46 EDT 2022 % 0.12/0.33 % CPUTime : % 0.94/1.10 (* PROOF-FOUND *) % 0.94/1.10 % SZS status Theorem % 0.94/1.10 (* BEGIN-PROOF *) % 0.94/1.10 % SZS output start Proof % 0.94/1.10 Theorem the_axiom : ((forall X : zenon_U, ((cowlThing X)/\(~(cowlNothing X))))/\((forall X : zenon_U, ((xsd_string X)<->(~(xsd_integer X))))/\((forall X : zenon_U, (forall Y : zenon_U, ((requalityOnA X Y)->((X = (ia))\/((X = (ib))\/(X = (ic)))))))/\((forall X : zenon_U, (forall Y : zenon_U, ((requalityOnA X Y)->(requalityOnA Y X))))/\((cowlThing (ia))/\((requalityOnA (ia) (ia))/\((cowlThing (ib))/\(cowlThing (ic))))))))). % 0.94/1.10 Proof. % 0.94/1.10 assert (zenon_L1_ : forall (zenon_TY_v : zenon_U), (forall C : zenon_U, ((((ib) = zenon_TY_v)/\(requalityOnA C (ib)))->(requalityOnA C zenon_TY_v))) -> (zenon_TY_v = (ib)) -> (~(requalityOnA (ib) zenon_TY_v)) -> False). % 0.94/1.10 do 1 intro. intros zenon_H12 zenon_H13 zenon_H14. % 0.94/1.10 generalize (zenon_H12 (ib)). zenon_intro zenon_H16. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H16); [ zenon_intro zenon_H18 | zenon_intro zenon_H17 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H18); [ zenon_intro zenon_H1a | zenon_intro zenon_H19 ]. % 0.94/1.10 apply zenon_H1a. apply sym_equal. exact zenon_H13. % 0.94/1.10 exact (zenon_H19 axiom_8). % 0.94/1.10 exact (zenon_H14 zenon_H17). % 0.94/1.10 (* end of lemma zenon_L1_ *) % 0.94/1.10 assert (zenon_L2_ : forall (zenon_TY_v : zenon_U) (zenon_TX_be : zenon_U), (forall Z : zenon_U, (((requalityOnA zenon_TX_be zenon_TY_v)/\(requalityOnA Z zenon_TY_v))->(zenon_TX_be = Z))) -> (requalityOnA zenon_TX_be zenon_TY_v) -> (forall C : zenon_U, ((((ib) = zenon_TY_v)/\(requalityOnA C (ib)))->(requalityOnA C zenon_TY_v))) -> (zenon_TY_v = (ib)) -> (~(zenon_TX_be = (ib))) -> False). % 0.94/1.10 do 2 intro. intros zenon_H1b zenon_H1c zenon_H12 zenon_H13 zenon_H1d. % 0.94/1.10 generalize (zenon_H1b (ib)). zenon_intro zenon_H1f. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H1f); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H21); [ zenon_intro zenon_H22 | zenon_intro zenon_H14 ]. % 0.94/1.10 exact (zenon_H22 zenon_H1c). % 0.94/1.10 apply (zenon_L1_ zenon_TY_v); trivial. % 0.94/1.10 exact (zenon_H1d zenon_H20). % 0.94/1.10 (* end of lemma zenon_L2_ *) % 0.94/1.10 assert (zenon_L3_ : forall (zenon_TX_be : zenon_U) (zenon_TY_v : zenon_U), (cA zenon_TY_v) -> (~((ia) = zenon_TY_v)) -> (~(zenon_TX_be = (ib))) -> (forall C : zenon_U, ((((ib) = zenon_TY_v)/\(requalityOnA C (ib)))->(requalityOnA C zenon_TY_v))) -> (requalityOnA zenon_TX_be zenon_TY_v) -> (forall Z : zenon_U, (((requalityOnA zenon_TX_be zenon_TY_v)/\(requalityOnA Z zenon_TY_v))->(zenon_TX_be = Z))) -> False). % 0.94/1.10 do 2 intro. intros zenon_H23 zenon_H24 zenon_H1d zenon_H12 zenon_H1c zenon_H1b. % 0.94/1.10 generalize (axiom_2 zenon_TY_v). zenon_intro zenon_H25. % 0.94/1.10 apply (zenon_equiv_s _ _ zenon_H25); [ zenon_intro zenon_H28; zenon_intro zenon_H27 | zenon_intro zenon_H23; zenon_intro zenon_H26 ]. % 0.94/1.10 exact (zenon_H28 zenon_H23). % 0.94/1.10 apply (zenon_or_s _ _ zenon_H26); [ zenon_intro zenon_H13 | zenon_intro zenon_H29 ]. % 0.94/1.10 apply (zenon_L2_ zenon_TY_v zenon_TX_be); trivial. % 0.94/1.10 apply zenon_H24. apply sym_equal. exact zenon_H29. % 0.94/1.10 (* end of lemma zenon_L3_ *) % 0.94/1.10 assert (zenon_L4_ : forall (zenon_TX_be : zenon_U) (zenon_TY_v : zenon_U), (~((ia) = zenon_TY_v)) -> (~(zenon_TX_be = (ib))) -> (forall C : zenon_U, ((((ib) = zenon_TY_v)/\(requalityOnA C (ib)))->(requalityOnA C zenon_TY_v))) -> (forall Z : zenon_U, (((requalityOnA zenon_TX_be zenon_TY_v)/\(requalityOnA Z zenon_TY_v))->(zenon_TX_be = Z))) -> (requalityOnA zenon_TX_be zenon_TY_v) -> False). % 0.94/1.10 do 2 intro. intros zenon_H24 zenon_H1d zenon_H12 zenon_H1b zenon_H1c. % 0.94/1.10 generalize (axiom_4 zenon_TX_be). zenon_intro zenon_H2a. % 0.94/1.10 generalize (zenon_H2a zenon_TY_v). zenon_intro zenon_H2b. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H2b); [ zenon_intro zenon_H22 | zenon_intro zenon_H23 ]. % 0.94/1.10 exact (zenon_H22 zenon_H1c). % 0.94/1.10 apply (zenon_L3_ zenon_TX_be zenon_TY_v); trivial. % 0.94/1.10 (* end of lemma zenon_L4_ *) % 0.94/1.10 assert (zenon_L5_ : forall (zenon_TX_be : zenon_U) (zenon_TY_v : zenon_U), (forall C : zenon_U, ((((ia) = zenon_TY_v)/\(requalityOnA C (ia)))->(requalityOnA C zenon_TY_v))) -> (~(zenon_TX_be = (ib))) -> (forall C : zenon_U, ((((ib) = zenon_TY_v)/\(requalityOnA C (ib)))->(requalityOnA C zenon_TY_v))) -> (forall Z : zenon_U, (((requalityOnA zenon_TX_be zenon_TY_v)/\(requalityOnA Z zenon_TY_v))->(zenon_TX_be = Z))) -> (requalityOnA zenon_TX_be zenon_TY_v) -> (~(requalityOnA (ia) zenon_TY_v)) -> False). % 0.94/1.10 do 2 intro. intros zenon_H2c zenon_H1d zenon_H12 zenon_H1b zenon_H1c zenon_H2d. % 0.94/1.10 generalize (zenon_H2c (ia)). zenon_intro zenon_H2e. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H2e); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H30); [ zenon_intro zenon_H24 | zenon_intro zenon_H31 ]. % 0.94/1.10 apply (zenon_L4_ zenon_TX_be zenon_TY_v); trivial. % 0.94/1.10 exact (zenon_H31 axiom_6). % 0.94/1.10 exact (zenon_H2d zenon_H2f). % 0.94/1.10 (* end of lemma zenon_L5_ *) % 0.94/1.10 assert (zenon_L6_ : forall (zenon_TY_cb : zenon_U), (cA zenon_TY_cb) -> (~((ia) = zenon_TY_cb)) -> (~((ib) = zenon_TY_cb)) -> False). % 0.94/1.10 do 1 intro. intros zenon_H32 zenon_H33 zenon_H34. % 0.94/1.10 generalize (axiom_2 zenon_TY_cb). zenon_intro zenon_H36. % 0.94/1.10 apply (zenon_equiv_s _ _ zenon_H36); [ zenon_intro zenon_H39; zenon_intro zenon_H38 | zenon_intro zenon_H32; zenon_intro zenon_H37 ]. % 0.94/1.10 exact (zenon_H39 zenon_H32). % 0.94/1.10 apply (zenon_or_s _ _ zenon_H37); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 0.94/1.10 apply zenon_H34. apply sym_equal. exact zenon_H3b. % 0.94/1.10 apply zenon_H33. apply sym_equal. exact zenon_H3a. % 0.94/1.10 (* end of lemma zenon_L6_ *) % 0.94/1.10 assert (zenon_L7_ : forall (zenon_TX_cm : zenon_U) (zenon_TY_cb : zenon_U), (forall Z : zenon_U, (((requalityOnA zenon_TY_cb (ia))/\(requalityOnA Z (ia)))->(zenon_TY_cb = Z))) -> (requalityOnA zenon_TY_cb (ia)) -> (requalityOnA zenon_TX_cm (ia)) -> (~(zenon_TY_cb = zenon_TX_cm)) -> False). % 0.94/1.10 do 2 intro. intros zenon_H3c zenon_H3d zenon_H3e zenon_H3f. % 0.94/1.10 generalize (zenon_H3c zenon_TX_cm). zenon_intro zenon_H41. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H41); [ zenon_intro zenon_H43 | zenon_intro zenon_H42 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H43); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 0.94/1.10 exact (zenon_H45 zenon_H3d). % 0.94/1.10 exact (zenon_H44 zenon_H3e). % 0.94/1.10 exact (zenon_H3f zenon_H42). % 0.94/1.10 (* end of lemma zenon_L7_ *) % 0.94/1.10 assert (zenon_L8_ : forall (zenon_TY_cb : zenon_U) (zenon_TX_cm : zenon_U), (forall B : zenon_U, (forall C : zenon_U, (((zenon_TX_cm = B)/\(requalityOnA zenon_TX_cm C))->(requalityOnA B C)))) -> (requalityOnA zenon_TY_cb (ia)) -> (requalityOnA zenon_TX_cm zenon_TY_cb) -> (~(zenon_TY_cb = zenon_TX_cm)) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_cb = B)/\(requalityOnA C zenon_TY_cb))->(requalityOnA C B)))) -> False). % 0.94/1.10 do 2 intro. intros zenon_H46 zenon_H3d zenon_H47 zenon_H3f zenon_H48. % 0.94/1.10 generalize (zenon_H46 zenon_TX_cm). zenon_intro zenon_H49. % 0.94/1.10 generalize (axiom_3 (ia)). zenon_intro zenon_H4a. % 0.94/1.10 generalize (zenon_H4a zenon_TY_cb). zenon_intro zenon_H3c. % 0.94/1.10 generalize (zenon_H48 (ia)). zenon_intro zenon_H4b. % 0.94/1.10 generalize (zenon_H3c (ia)). zenon_intro zenon_H4c. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H4c); [ zenon_intro zenon_H4d | zenon_intro zenon_H3a ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H45 | zenon_intro zenon_H31 ]. % 0.94/1.10 exact (zenon_H45 zenon_H3d). % 0.94/1.10 exact (zenon_H31 axiom_6). % 0.94/1.10 generalize (zenon_H49 (ia)). zenon_intro zenon_H4e. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H4e); [ zenon_intro zenon_H4f | zenon_intro zenon_H3e ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H50 | zenon_intro zenon_H44 ]. % 0.94/1.10 apply zenon_H50. apply refl_equal. % 0.94/1.10 generalize (zenon_H4b zenon_TX_cm). zenon_intro zenon_H51. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H51); [ zenon_intro zenon_H52 | zenon_intro zenon_H3e ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 0.94/1.10 exact (zenon_H54 zenon_H3a). % 0.94/1.10 exact (zenon_H53 zenon_H47). % 0.94/1.10 exact (zenon_H44 zenon_H3e). % 0.94/1.10 apply (zenon_L7_ zenon_TX_cm zenon_TY_cb); trivial. % 0.94/1.10 (* end of lemma zenon_L8_ *) % 0.94/1.10 assert (zenon_L9_ : forall (zenon_TX_cm : zenon_U) (zenon_TY_cb : zenon_U), (forall B : zenon_U, (forall C : zenon_U, (((zenon_TY_cb = B)/\(requalityOnA C zenon_TY_cb))->(requalityOnA C B)))) -> (~(zenon_TY_cb = zenon_TX_cm)) -> (requalityOnA zenon_TX_cm zenon_TY_cb) -> (requalityOnA zenon_TY_cb (ia)) -> False). % 0.94/1.10 do 2 intro. intros zenon_H48 zenon_H3f zenon_H47 zenon_H3d. % 0.94/1.10 generalize (requalityOnA_substitution_1 zenon_TX_cm). zenon_intro zenon_H46. % 0.94/1.10 apply (zenon_L8_ zenon_TY_cb zenon_TX_cm); trivial. % 0.94/1.10 (* end of lemma zenon_L9_ *) % 0.94/1.10 assert (zenon_L10_ : forall (zenon_TX_cm : zenon_U) (zenon_TY_cb : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, (((requalityOnA Y (ib))/\(requalityOnA Z (ib)))->(Y = Z)))) -> (forall C : zenon_U, (((zenon_TY_cb = (ib))/\(requalityOnA C zenon_TY_cb))->(requalityOnA C (ib)))) -> (requalityOnA zenon_TX_cm zenon_TY_cb) -> (~(zenon_TY_cb = zenon_TX_cm)) -> (forall B : zenon_U, (forall C : zenon_U, (((zenon_TX_cm = B)/\(requalityOnA zenon_TX_cm C))->(requalityOnA B C)))) -> (requalityOnA zenon_TY_cb (ib)) -> False). % 0.94/1.10 do 2 intro. intros zenon_H55 zenon_H56 zenon_H47 zenon_H3f zenon_H46 zenon_H57. % 0.94/1.10 generalize (zenon_H55 zenon_TY_cb). zenon_intro zenon_H58. % 0.94/1.10 generalize (zenon_H58 (ib)). zenon_intro zenon_H59. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H5a | zenon_intro zenon_H3b ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H5b | zenon_intro zenon_H19 ]. % 0.94/1.10 exact (zenon_H5b zenon_H57). % 0.94/1.10 exact (zenon_H19 axiom_8). % 0.94/1.10 generalize (zenon_H46 zenon_TX_cm). zenon_intro zenon_H49. % 0.94/1.10 generalize (zenon_H49 (ib)). zenon_intro zenon_H5c. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H5c); [ zenon_intro zenon_H5e | zenon_intro zenon_H5d ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H5e); [ zenon_intro zenon_H50 | zenon_intro zenon_H5f ]. % 0.94/1.10 apply zenon_H50. apply refl_equal. % 0.94/1.10 generalize (zenon_H56 zenon_TX_cm). zenon_intro zenon_H60. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H61 | zenon_intro zenon_H5d ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H61); [ zenon_intro zenon_H62 | zenon_intro zenon_H53 ]. % 0.94/1.10 exact (zenon_H62 zenon_H3b). % 0.94/1.10 exact (zenon_H53 zenon_H47). % 0.94/1.10 exact (zenon_H5f zenon_H5d). % 0.94/1.10 generalize (zenon_H58 zenon_TX_cm). zenon_intro zenon_H63. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H63); [ zenon_intro zenon_H64 | zenon_intro zenon_H42 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H64); [ zenon_intro zenon_H5b | zenon_intro zenon_H5f ]. % 0.94/1.10 exact (zenon_H5b zenon_H57). % 0.94/1.10 exact (zenon_H5f zenon_H5d). % 0.94/1.10 exact (zenon_H3f zenon_H42). % 0.94/1.10 (* end of lemma zenon_L10_ *) % 0.94/1.10 assert (zenon_L11_ : forall (zenon_TY_cb : zenon_U), (zenon_TY_cb = (ib)) -> (requalityOnA zenon_TY_cb (ib)) -> (~(requalityOnA zenon_TY_cb zenon_TY_cb)) -> False). % 0.94/1.10 do 1 intro. intros zenon_H3b zenon_H57 zenon_H65. % 0.94/1.10 generalize (requalityOnA_substitution_2 (ib)). zenon_intro zenon_H66. % 0.94/1.10 generalize (zenon_H66 zenon_TY_cb). zenon_intro zenon_H67. % 0.94/1.10 generalize (zenon_H67 zenon_TY_cb). zenon_intro zenon_H68. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H68); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H34 | zenon_intro zenon_H5b ]. % 0.94/1.10 apply zenon_H34. apply sym_equal. exact zenon_H3b. % 0.94/1.10 exact (zenon_H5b zenon_H57). % 0.94/1.10 exact (zenon_H65 zenon_H69). % 0.94/1.10 (* end of lemma zenon_L11_ *) % 0.94/1.10 assert (zenon_L12_ : forall (zenon_TY_cb : zenon_U), (cA zenon_TY_cb) -> (~((ia) = zenon_TY_cb)) -> (~(requalityOnA zenon_TY_cb zenon_TY_cb)) -> (forall C : zenon_U, ((((ib) = zenon_TY_cb)/\(requalityOnA (ib) C))->(requalityOnA zenon_TY_cb C))) -> False). % 0.94/1.10 do 1 intro. intros zenon_H32 zenon_H33 zenon_H65 zenon_H6b. % 0.94/1.10 generalize (axiom_2 zenon_TY_cb). zenon_intro zenon_H36. % 0.94/1.10 apply (zenon_equiv_s _ _ zenon_H36); [ zenon_intro zenon_H39; zenon_intro zenon_H38 | zenon_intro zenon_H32; zenon_intro zenon_H37 ]. % 0.94/1.10 exact (zenon_H39 zenon_H32). % 0.94/1.10 apply (zenon_or_s _ _ zenon_H37); [ zenon_intro zenon_H3b | zenon_intro zenon_H3a ]. % 0.94/1.10 generalize (zenon_H6b (ib)). zenon_intro zenon_H6c. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6d | zenon_intro zenon_H57 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H34 | zenon_intro zenon_H19 ]. % 0.94/1.10 apply zenon_H34. apply sym_equal. exact zenon_H3b. % 0.94/1.10 exact (zenon_H19 axiom_8). % 0.94/1.10 apply (zenon_L11_ zenon_TY_cb); trivial. % 0.94/1.10 apply zenon_H33. apply sym_equal. exact zenon_H3a. % 0.94/1.10 (* end of lemma zenon_L12_ *) % 0.94/1.10 assert (zenon_L13_ : forall (zenon_TY_cb : zenon_U), (forall Y : zenon_U, (forall Z : zenon_U, (((requalityOnA Y (ia))/\(requalityOnA Z (ia)))->(Y = Z)))) -> (~(requalityOnA zenon_TY_cb zenon_TY_cb)) -> (requalityOnA zenon_TY_cb (ia)) -> False). % 0.94/1.10 do 1 intro. intros zenon_H4a zenon_H65 zenon_H3d. % 0.94/1.10 generalize (zenon_H4a zenon_TY_cb). zenon_intro zenon_H3c. % 0.94/1.10 generalize (zenon_H3c (ia)). zenon_intro zenon_H4c. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H4c); [ zenon_intro zenon_H4d | zenon_intro zenon_H3a ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H45 | zenon_intro zenon_H31 ]. % 0.94/1.10 exact (zenon_H45 zenon_H3d). % 0.94/1.10 exact (zenon_H31 axiom_6). % 0.94/1.10 generalize (requalityOnA_substitution_2 (ia)). zenon_intro zenon_H6e. % 0.94/1.10 generalize (zenon_H6e zenon_TY_cb). zenon_intro zenon_H6f. % 0.94/1.10 generalize (zenon_H6f zenon_TY_cb). zenon_intro zenon_H70. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H70); [ zenon_intro zenon_H71 | zenon_intro zenon_H69 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H71); [ zenon_intro zenon_H33 | zenon_intro zenon_H45 ]. % 0.94/1.10 apply zenon_H33. apply sym_equal. exact zenon_H3a. % 0.94/1.10 exact (zenon_H45 zenon_H3d). % 0.94/1.10 exact (zenon_H65 zenon_H69). % 0.94/1.10 (* end of lemma zenon_L13_ *) % 0.94/1.10 assert (zenon_L14_ : forall (zenon_TY_cb : zenon_U), (requalityOnA zenon_TY_cb (ia)) -> (~(requalityOnA zenon_TY_cb zenon_TY_cb)) -> False). % 0.94/1.10 do 1 intro. intros zenon_H3d zenon_H65. % 0.94/1.10 generalize (axiom_3 (ia)). zenon_intro zenon_H4a. % 0.94/1.10 apply (zenon_L13_ zenon_TY_cb); trivial. % 0.94/1.10 (* end of lemma zenon_L14_ *) % 0.94/1.10 apply NNPP. intro zenon_G. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.94/1.10 exact (zenon_H73 axiom_0). % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H72); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 0.94/1.10 exact (zenon_H75 axiom_1). % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H74); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 0.94/1.10 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, ((requalityOnA X Y)->((X = (ia))\/((X = (ib))\/(X = (ic))))))) zenon_H77); [ zenon_intro zenon_H78; idtac ]. % 0.94/1.10 elim zenon_H78. zenon_intro zenon_TX_be. zenon_intro zenon_H79. % 0.94/1.10 apply (zenon_notallex_s (fun Y : zenon_U => ((requalityOnA zenon_TX_be Y)->((zenon_TX_be = (ia))\/((zenon_TX_be = (ib))\/(zenon_TX_be = (ic)))))) zenon_H79); [ zenon_intro zenon_H7a; idtac ]. % 0.94/1.10 elim zenon_H7a. zenon_intro zenon_TY_v. zenon_intro zenon_H7b. % 0.94/1.10 apply (zenon_notimply_s _ _ zenon_H7b). zenon_intro zenon_H1c. zenon_intro zenon_H7c. % 0.94/1.10 apply (zenon_notor_s _ _ zenon_H7c). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 0.94/1.10 apply (zenon_notor_s _ _ zenon_H7d). zenon_intro zenon_H1d. zenon_intro zenon_H7f. % 0.94/1.10 generalize (axiom_3 zenon_TY_v). zenon_intro zenon_H80. % 0.94/1.10 generalize (zenon_H80 zenon_TX_be). zenon_intro zenon_H1b. % 0.94/1.10 generalize (requalityOnA_substitution_2 (ib)). zenon_intro zenon_H66. % 0.94/1.10 generalize (zenon_H66 zenon_TY_v). zenon_intro zenon_H12. % 0.94/1.10 generalize (requalityOnA_substitution_2 (ia)). zenon_intro zenon_H6e. % 0.94/1.10 generalize (zenon_H6e zenon_TY_v). zenon_intro zenon_H2c. % 0.94/1.10 generalize (zenon_H1b (ia)). zenon_intro zenon_H81. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H81); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H83); [ zenon_intro zenon_H22 | zenon_intro zenon_H2d ]. % 0.94/1.10 exact (zenon_H22 zenon_H1c). % 0.94/1.10 apply (zenon_L5_ zenon_TX_be zenon_TY_v); trivial. % 0.94/1.10 exact (zenon_H7e zenon_H82). % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H76); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 0.94/1.10 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, ((requalityOnA X Y)->(requalityOnA Y X)))) zenon_H85); [ zenon_intro zenon_H86; idtac ]. % 0.94/1.10 elim zenon_H86. zenon_intro zenon_TX_cm. zenon_intro zenon_H87. % 0.94/1.10 apply (zenon_notallex_s (fun Y : zenon_U => ((requalityOnA zenon_TX_cm Y)->(requalityOnA Y zenon_TX_cm))) zenon_H87); [ zenon_intro zenon_H88; idtac ]. % 0.94/1.10 elim zenon_H88. zenon_intro zenon_TY_cb. zenon_intro zenon_H89. % 0.94/1.10 apply (zenon_notimply_s _ _ zenon_H89). zenon_intro zenon_H47. zenon_intro zenon_H8a. % 0.94/1.10 generalize (requalityOnA_substitution_2 zenon_TY_cb). zenon_intro zenon_H48. % 0.94/1.10 generalize (zenon_H48 zenon_TX_cm). zenon_intro zenon_H8b. % 0.94/1.10 generalize (zenon_H8b zenon_TY_cb). zenon_intro zenon_H8c. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H8c); [ zenon_intro zenon_H8e | zenon_intro zenon_H8d ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H8e); [ zenon_intro zenon_H3f | zenon_intro zenon_H65 ]. % 0.94/1.10 generalize (zenon_H48 (ib)). zenon_intro zenon_H56. % 0.94/1.10 generalize (requalityOnA_substitution_1 (ib)). zenon_intro zenon_H8f. % 0.94/1.10 generalize (requalityOnA_substitution_1 (ia)). zenon_intro zenon_H90. % 0.94/1.10 generalize (requalityOnA_substitution_1 zenon_TX_cm). zenon_intro zenon_H46. % 0.94/1.10 generalize (zenon_H90 zenon_TY_cb). zenon_intro zenon_H91. % 0.94/1.10 generalize (zenon_H8f zenon_TY_cb). zenon_intro zenon_H6b. % 0.94/1.10 generalize (axiom_3 (ib)). zenon_intro zenon_H55. % 0.94/1.10 generalize (zenon_H6b (ib)). zenon_intro zenon_H6c. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6d | zenon_intro zenon_H57 ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H34 | zenon_intro zenon_H19 ]. % 0.94/1.10 generalize (zenon_H91 (ia)). zenon_intro zenon_H92. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H92); [ zenon_intro zenon_H93 | zenon_intro zenon_H3d ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H33 | zenon_intro zenon_H31 ]. % 0.94/1.10 generalize (axiom_4 zenon_TX_cm). zenon_intro zenon_H94. % 0.94/1.10 generalize (zenon_H94 zenon_TY_cb). zenon_intro zenon_H95. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H95); [ zenon_intro zenon_H53 | zenon_intro zenon_H32 ]. % 0.94/1.10 exact (zenon_H53 zenon_H47). % 0.94/1.10 apply (zenon_L6_ zenon_TY_cb); trivial. % 0.94/1.10 exact (zenon_H31 axiom_6). % 0.94/1.10 apply (zenon_L9_ zenon_TX_cm zenon_TY_cb); trivial. % 0.94/1.10 exact (zenon_H19 axiom_8). % 0.94/1.10 apply (zenon_L10_ zenon_TX_cm zenon_TY_cb); trivial. % 0.94/1.10 generalize (requalityOnA_substitution_1 (ia)). zenon_intro zenon_H90. % 0.94/1.10 generalize (requalityOnA_substitution_1 (ib)). zenon_intro zenon_H8f. % 0.94/1.10 generalize (zenon_H90 zenon_TY_cb). zenon_intro zenon_H91. % 0.94/1.10 generalize (zenon_H91 (ia)). zenon_intro zenon_H92. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H92); [ zenon_intro zenon_H93 | zenon_intro zenon_H3d ]. % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H33 | zenon_intro zenon_H31 ]. % 0.94/1.10 generalize (zenon_H8f zenon_TY_cb). zenon_intro zenon_H6b. % 0.94/1.10 generalize (axiom_4 zenon_TX_cm). zenon_intro zenon_H94. % 0.94/1.10 generalize (zenon_H94 zenon_TY_cb). zenon_intro zenon_H95. % 0.94/1.10 apply (zenon_imply_s _ _ zenon_H95); [ zenon_intro zenon_H53 | zenon_intro zenon_H32 ]. % 0.94/1.10 exact (zenon_H53 zenon_H47). % 0.94/1.10 apply (zenon_L12_ zenon_TY_cb); trivial. % 0.94/1.10 exact (zenon_H31 axiom_6). % 0.94/1.10 apply (zenon_L14_ zenon_TY_cb); trivial. % 0.94/1.10 exact (zenon_H8a zenon_H8d). % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H97 | zenon_intro zenon_H96 ]. % 0.94/1.10 exact (zenon_H97 axiom_5). % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H96); [ zenon_intro zenon_H31 | zenon_intro zenon_H98 ]. % 0.94/1.10 exact (zenon_H31 axiom_6). % 0.94/1.10 apply (zenon_notand_s _ _ zenon_H98); [ zenon_intro zenon_H9a | zenon_intro zenon_H99 ]. % 0.94/1.10 exact (zenon_H9a axiom_7). % 0.94/1.10 exact (zenon_H99 axiom_9). % 0.94/1.10 Qed. % 0.94/1.10 % SZS output end Proof % 0.94/1.10 (* END-PROOF *) % 0.94/1.10 nodes searched: 31845 % 0.94/1.10 max branch formulas: 989 % 0.94/1.10 proof nodes created: 2209 % 0.94/1.10 formulas created: 68872 % 0.94/1.10 %------------------------------------------------------------------------------