%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR063+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n029.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 : Sat Jul 16 00:02:23 EDT 2022 % Result : Theorem 13.66s 13.87s % Output : Proof 13.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR063+1 : TPTP v8.1.0. Released v3.4.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n029.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 : Sat Jun 11 01:51:38 EDT 2022 % 0.13/0.34 % CPUTime : % 13.66/13.87 (* PROOF-FOUND *) % 13.66/13.87 % SZS status Theorem % 13.66/13.87 (* BEGIN-PROOF *) % 13.66/13.87 % SZS output start Proof % 13.66/13.87 Theorem query63 : (~(disjointwith (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949))). % 13.66/13.87 Proof. % 13.66/13.87 assert (zenon_L1_ : (~((c_mathematicalorcomputationalthing) = (c_mathematicalorcomputationalthing))) -> False). % 13.66/13.87 do 0 intro. intros zenon_H5e. % 13.66/13.87 apply zenon_H5e. apply refl_equal. % 13.66/13.87 (* end of lemma zenon_L1_ *) % 13.66/13.87 assert (zenon_L2_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_setorcollection) (c_mathematicalorcomputationalthing))) -> False). % 13.66/13.87 do 0 intro. intros zenon_H5f zenon_H60. % 13.66/13.87 elim (classic ((~((c_setorcollection) = (c_mathematicalthing)))/\(~(genls (c_setorcollection) (c_mathematicalthing))))); [ zenon_intro zenon_H61 | zenon_intro zenon_H62 ]. % 13.66/13.87 apply (zenon_and_s _ _ zenon_H61). zenon_intro zenon_H64. zenon_intro zenon_H63. % 13.66/13.87 exact (zenon_H63 just1). % 13.66/13.87 cut ((genls (c_mathematicalthing) (c_mathematicalorcomputationalthing)) = (genls (c_setorcollection) (c_mathematicalorcomputationalthing))). % 13.66/13.87 intro zenon_D_pnotp. % 13.66/13.87 apply zenon_H60. % 13.66/13.87 rewrite <- zenon_D_pnotp. % 13.66/13.87 exact just10. % 13.66/13.87 cut (((c_mathematicalorcomputationalthing) = (c_mathematicalorcomputationalthing))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 13.66/13.87 cut (((c_mathematicalthing) = (c_setorcollection))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 13.66/13.87 congruence. % 13.66/13.87 apply (zenon_notand_s _ _ zenon_H62); [ zenon_intro zenon_H67 | zenon_intro zenon_H66 ]. % 13.66/13.87 apply zenon_H67. zenon_intro zenon_H68. % 13.66/13.87 elim (classic ((c_setorcollection) = (c_setorcollection))); [ zenon_intro zenon_H69 | zenon_intro zenon_H6a ]. % 13.66/13.87 cut (((c_setorcollection) = (c_setorcollection)) = ((c_mathematicalthing) = (c_setorcollection))). % 13.66/13.87 intro zenon_D_pnotp. % 13.66/13.87 apply zenon_H65. % 13.66/13.87 rewrite <- zenon_D_pnotp. % 13.66/13.87 exact zenon_H69. % 13.66/13.87 cut (((c_setorcollection) = (c_setorcollection))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 13.66/13.87 cut (((c_setorcollection) = (c_mathematicalthing))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 13.66/13.87 congruence. % 13.66/13.87 exact (zenon_H64 zenon_H68). % 13.66/13.87 apply zenon_H6a. apply refl_equal. % 13.66/13.87 apply zenon_H6a. apply refl_equal. % 13.66/13.87 apply zenon_H66. zenon_intro just1. % 13.66/13.87 generalize (zenon_H5f (c_setorcollection)). zenon_intro zenon_H6b. % 13.66/13.87 generalize (zenon_H6b (c_mathematicalthing)). zenon_intro zenon_H6c. % 13.66/13.87 generalize (zenon_H6c (c_mathematicalorcomputationalthing)). zenon_intro zenon_H6d. % 13.66/13.87 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H63 | zenon_intro zenon_H6e ]. % 13.66/13.87 exact (zenon_H63 just1). % 13.66/13.87 apply (zenon_imply_s _ _ zenon_H6e); [ zenon_intro zenon_H70 | zenon_intro zenon_H6f ]. % 13.66/13.87 exact (zenon_H70 just10). % 13.66/13.87 exact (zenon_H60 zenon_H6f). % 13.66/13.87 apply zenon_H5e. apply refl_equal. % 13.66/13.87 (* end of lemma zenon_L2_ *) % 13.66/13.87 assert (zenon_L3_ : (~((c_intangible) = (c_intangible))) -> False). % 13.66/13.87 do 0 intro. intros zenon_H71. % 13.66/13.87 apply zenon_H71. apply refl_equal. % 13.66/13.87 (* end of lemma zenon_L3_ *) % 13.66/13.87 assert (zenon_L4_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_setorcollection) (c_intangible))) -> False). % 13.66/13.88 do 0 intro. intros zenon_H5f zenon_H72. % 13.66/13.88 elim (classic ((~((c_setorcollection) = (c_mathematicalorcomputationalthing)))/\(~(genls (c_setorcollection) (c_mathematicalorcomputationalthing))))); [ zenon_intro zenon_H73 | zenon_intro zenon_H74 ]. % 13.66/13.88 apply (zenon_and_s _ _ zenon_H73). zenon_intro zenon_H75. zenon_intro zenon_H60. % 13.66/13.88 apply (zenon_L2_); trivial. % 13.66/13.88 cut ((genls (c_mathematicalorcomputationalthing) (c_intangible)) = (genls (c_setorcollection) (c_intangible))). % 13.66/13.88 intro zenon_D_pnotp. % 13.66/13.88 apply zenon_H72. % 13.66/13.88 rewrite <- zenon_D_pnotp. % 13.66/13.88 exact just4. % 13.66/13.88 cut (((c_intangible) = (c_intangible))); [idtac | apply NNPP; zenon_intro zenon_H71]. % 13.66/13.88 cut (((c_mathematicalorcomputationalthing) = (c_setorcollection))); [idtac | apply NNPP; zenon_intro zenon_H76]. % 13.66/13.88 congruence. % 13.66/13.88 apply (zenon_notand_s _ _ zenon_H74); [ zenon_intro zenon_H78 | zenon_intro zenon_H77 ]. % 13.66/13.88 apply zenon_H78. zenon_intro zenon_H79. % 13.66/13.88 elim (classic ((c_setorcollection) = (c_setorcollection))); [ zenon_intro zenon_H69 | zenon_intro zenon_H6a ]. % 13.66/13.88 cut (((c_setorcollection) = (c_setorcollection)) = ((c_mathematicalorcomputationalthing) = (c_setorcollection))). % 13.66/13.88 intro zenon_D_pnotp. % 13.66/13.88 apply zenon_H76. % 13.66/13.88 rewrite <- zenon_D_pnotp. % 13.66/13.88 exact zenon_H69. % 13.66/13.88 cut (((c_setorcollection) = (c_setorcollection))); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 13.66/13.88 cut (((c_setorcollection) = (c_mathematicalorcomputationalthing))); [idtac | apply NNPP; zenon_intro zenon_H75]. % 13.66/13.88 congruence. % 13.66/13.88 exact (zenon_H75 zenon_H79). % 13.66/13.88 apply zenon_H6a. apply refl_equal. % 13.66/13.88 apply zenon_H6a. apply refl_equal. % 13.66/13.88 apply zenon_H77. zenon_intro zenon_H6f. % 13.66/13.88 generalize (zenon_H5f (c_setorcollection)). zenon_intro zenon_H6b. % 13.66/13.88 generalize (zenon_H6b (c_mathematicalorcomputationalthing)). zenon_intro zenon_H7a. % 13.66/13.88 generalize (zenon_H7a (c_intangible)). zenon_intro zenon_H7b. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H60 | zenon_intro zenon_H7c ]. % 13.66/13.88 exact (zenon_H60 zenon_H6f). % 13.66/13.88 apply (zenon_imply_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 13.66/13.88 exact (zenon_H7e just4). % 13.66/13.88 exact (zenon_H72 zenon_H7d). % 13.66/13.88 apply zenon_H71. apply refl_equal. % 13.66/13.88 (* end of lemma zenon_L4_ *) % 13.66/13.88 assert (zenon_L5_ : (~((c_inanimateobject_nonnatural) = (c_inanimateobject_nonnatural))) -> False). % 13.66/13.88 do 0 intro. intros zenon_H7f. % 13.66/13.88 apply zenon_H7f. apply refl_equal. % 13.66/13.88 (* end of lemma zenon_L5_ *) % 13.66/13.88 assert (zenon_L6_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_computerdataartifact) (c_inanimateobject_nonnatural))) -> False). % 13.66/13.88 do 0 intro. intros zenon_H5f zenon_H80. % 13.66/13.88 elim (classic ((~((c_computerdataartifact) = (c_artifact)))/\(~(genls (c_computerdataartifact) (c_artifact))))); [ zenon_intro zenon_H81 | zenon_intro zenon_H82 ]. % 13.66/13.88 apply (zenon_and_s _ _ zenon_H81). zenon_intro zenon_H84. zenon_intro zenon_H83. % 13.66/13.88 exact (zenon_H83 just8). % 13.66/13.88 cut ((genls (c_artifact) (c_inanimateobject_nonnatural)) = (genls (c_computerdataartifact) (c_inanimateobject_nonnatural))). % 13.66/13.88 intro zenon_D_pnotp. % 13.66/13.88 apply zenon_H80. % 13.66/13.88 rewrite <- zenon_D_pnotp. % 13.66/13.88 exact just13. % 13.66/13.88 cut (((c_inanimateobject_nonnatural) = (c_inanimateobject_nonnatural))); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 13.66/13.88 cut (((c_artifact) = (c_computerdataartifact))); [idtac | apply NNPP; zenon_intro zenon_H85]. % 13.66/13.88 congruence. % 13.66/13.88 apply (zenon_notand_s _ _ zenon_H82); [ zenon_intro zenon_H87 | zenon_intro zenon_H86 ]. % 13.66/13.88 apply zenon_H87. zenon_intro zenon_H88. % 13.66/13.88 elim (classic ((c_computerdataartifact) = (c_computerdataartifact))); [ zenon_intro zenon_H89 | zenon_intro zenon_H8a ]. % 13.66/13.88 cut (((c_computerdataartifact) = (c_computerdataartifact)) = ((c_artifact) = (c_computerdataartifact))). % 13.66/13.88 intro zenon_D_pnotp. % 13.66/13.88 apply zenon_H85. % 13.66/13.88 rewrite <- zenon_D_pnotp. % 13.66/13.88 exact zenon_H89. % 13.66/13.88 cut (((c_computerdataartifact) = (c_computerdataartifact))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 13.66/13.88 cut (((c_computerdataartifact) = (c_artifact))); [idtac | apply NNPP; zenon_intro zenon_H84]. % 13.66/13.88 congruence. % 13.66/13.88 exact (zenon_H84 zenon_H88). % 13.66/13.88 apply zenon_H8a. apply refl_equal. % 13.66/13.88 apply zenon_H8a. apply refl_equal. % 13.66/13.88 apply zenon_H86. zenon_intro just8. % 13.66/13.88 generalize (zenon_H5f (c_computerdataartifact)). zenon_intro zenon_H8b. % 13.66/13.88 generalize (zenon_H8b (c_artifact)). zenon_intro zenon_H8c. % 13.66/13.88 generalize (zenon_H8c (c_inanimateobject_nonnatural)). zenon_intro zenon_H8d. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_H8d); [ zenon_intro zenon_H83 | zenon_intro zenon_H8e ]. % 13.66/13.88 exact (zenon_H83 just8). % 13.66/13.88 apply (zenon_imply_s _ _ zenon_H8e); [ zenon_intro zenon_H90 | zenon_intro zenon_H8f ]. % 13.66/13.88 exact (zenon_H90 just13). % 13.66/13.88 exact (zenon_H80 zenon_H8f). % 13.66/13.88 apply zenon_H7f. apply refl_equal. % 13.66/13.88 (* end of lemma zenon_L6_ *) % 13.66/13.88 assert (zenon_L7_ : (~((c_inanimateobject) = (c_inanimateobject))) -> False). % 13.66/13.88 do 0 intro. intros zenon_H91. % 13.66/13.88 apply zenon_H91. apply refl_equal. % 13.66/13.88 (* end of lemma zenon_L7_ *) % 13.66/13.88 assert (zenon_L8_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_computerdataartifact) (c_inanimateobject))) -> False). % 13.66/13.88 do 0 intro. intros zenon_H5f zenon_H92. % 13.66/13.88 elim (classic ((~((c_computerdataartifact) = (c_inanimateobject_nonnatural)))/\(~(genls (c_computerdataartifact) (c_inanimateobject_nonnatural))))); [ zenon_intro zenon_H93 | zenon_intro zenon_H94 ]. % 13.66/13.88 apply (zenon_and_s _ _ zenon_H93). zenon_intro zenon_H95. zenon_intro zenon_H80. % 13.66/13.88 apply (zenon_L6_); trivial. % 13.66/13.88 cut ((genls (c_inanimateobject_nonnatural) (c_inanimateobject)) = (genls (c_computerdataartifact) (c_inanimateobject))). % 13.66/13.88 intro zenon_D_pnotp. % 13.66/13.88 apply zenon_H92. % 13.66/13.88 rewrite <- zenon_D_pnotp. % 13.66/13.88 exact just15. % 13.66/13.88 cut (((c_inanimateobject) = (c_inanimateobject))); [idtac | apply NNPP; zenon_intro zenon_H91]. % 13.66/13.88 cut (((c_inanimateobject_nonnatural) = (c_computerdataartifact))); [idtac | apply NNPP; zenon_intro zenon_H96]. % 13.66/13.88 congruence. % 13.66/13.88 apply (zenon_notand_s _ _ zenon_H94); [ zenon_intro zenon_H98 | zenon_intro zenon_H97 ]. % 13.66/13.88 apply zenon_H98. zenon_intro zenon_H99. % 13.66/13.88 elim (classic ((c_computerdataartifact) = (c_computerdataartifact))); [ zenon_intro zenon_H89 | zenon_intro zenon_H8a ]. % 13.66/13.88 cut (((c_computerdataartifact) = (c_computerdataartifact)) = ((c_inanimateobject_nonnatural) = (c_computerdataartifact))). % 13.66/13.88 intro zenon_D_pnotp. % 13.66/13.88 apply zenon_H96. % 13.66/13.88 rewrite <- zenon_D_pnotp. % 13.66/13.88 exact zenon_H89. % 13.66/13.88 cut (((c_computerdataartifact) = (c_computerdataartifact))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 13.66/13.88 cut (((c_computerdataartifact) = (c_inanimateobject_nonnatural))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 13.66/13.88 congruence. % 13.66/13.88 exact (zenon_H95 zenon_H99). % 13.66/13.88 apply zenon_H8a. apply refl_equal. % 13.66/13.88 apply zenon_H8a. apply refl_equal. % 13.66/13.88 apply zenon_H97. zenon_intro zenon_H8f. % 13.66/13.88 generalize (zenon_H5f (c_computerdataartifact)). zenon_intro zenon_H8b. % 13.66/13.88 generalize (zenon_H8b (c_inanimateobject_nonnatural)). zenon_intro zenon_H9a. % 13.66/13.88 generalize (zenon_H9a (c_inanimateobject)). zenon_intro zenon_H9b. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_H9b); [ zenon_intro zenon_H80 | zenon_intro zenon_H9c ]. % 13.66/13.88 exact (zenon_H80 zenon_H8f). % 13.66/13.88 apply (zenon_imply_s _ _ zenon_H9c); [ zenon_intro zenon_H9e | zenon_intro zenon_H9d ]. % 13.66/13.88 exact (zenon_H9e just15). % 13.66/13.88 exact (zenon_H92 zenon_H9d). % 13.66/13.88 apply zenon_H91. apply refl_equal. % 13.66/13.88 (* end of lemma zenon_L8_ *) % 13.66/13.88 assert (zenon_L9_ : (~((c_partiallytangible) = (c_partiallytangible))) -> False). % 13.66/13.88 do 0 intro. intros zenon_H9f. % 13.66/13.88 apply zenon_H9f. apply refl_equal. % 13.66/13.88 (* end of lemma zenon_L9_ *) % 13.66/13.88 assert (zenon_L10_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z)))))) -> (~(genls (c_computerdataartifact) (c_partiallytangible))) -> False). % 13.66/13.88 do 0 intro. intros zenon_H5f zenon_Ha0. % 13.66/13.88 elim (classic ((~((c_computerdataartifact) = (c_inanimateobject)))/\(~(genls (c_computerdataartifact) (c_inanimateobject))))); [ zenon_intro zenon_Ha1 | zenon_intro zenon_Ha2 ]. % 13.66/13.88 apply (zenon_and_s _ _ zenon_Ha1). zenon_intro zenon_Ha3. zenon_intro zenon_H92. % 13.66/13.88 apply (zenon_L8_); trivial. % 13.66/13.88 cut ((genls (c_inanimateobject) (c_partiallytangible)) = (genls (c_computerdataartifact) (c_partiallytangible))). % 13.66/13.88 intro zenon_D_pnotp. % 13.66/13.88 apply zenon_Ha0. % 13.66/13.88 rewrite <- zenon_D_pnotp. % 13.66/13.88 exact just17. % 13.66/13.88 cut (((c_partiallytangible) = (c_partiallytangible))); [idtac | apply NNPP; zenon_intro zenon_H9f]. % 13.66/13.88 cut (((c_inanimateobject) = (c_computerdataartifact))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 13.66/13.88 congruence. % 13.66/13.88 apply (zenon_notand_s _ _ zenon_Ha2); [ zenon_intro zenon_Ha6 | zenon_intro zenon_Ha5 ]. % 13.66/13.88 apply zenon_Ha6. zenon_intro zenon_Ha7. % 13.66/13.88 elim (classic ((c_computerdataartifact) = (c_computerdataartifact))); [ zenon_intro zenon_H89 | zenon_intro zenon_H8a ]. % 13.66/13.88 cut (((c_computerdataartifact) = (c_computerdataartifact)) = ((c_inanimateobject) = (c_computerdataartifact))). % 13.66/13.88 intro zenon_D_pnotp. % 13.66/13.88 apply zenon_Ha4. % 13.66/13.88 rewrite <- zenon_D_pnotp. % 13.66/13.88 exact zenon_H89. % 13.66/13.88 cut (((c_computerdataartifact) = (c_computerdataartifact))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 13.66/13.88 cut (((c_computerdataartifact) = (c_inanimateobject))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 13.66/13.88 congruence. % 13.66/13.88 exact (zenon_Ha3 zenon_Ha7). % 13.66/13.88 apply zenon_H8a. apply refl_equal. % 13.66/13.88 apply zenon_H8a. apply refl_equal. % 13.66/13.88 apply zenon_Ha5. zenon_intro zenon_H9d. % 13.66/13.88 generalize (zenon_H5f (c_computerdataartifact)). zenon_intro zenon_H8b. % 13.66/13.88 generalize (zenon_H8b (c_inanimateobject)). zenon_intro zenon_Ha8. % 13.66/13.88 generalize (zenon_Ha8 (c_partiallytangible)). zenon_intro zenon_Ha9. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Ha9); [ zenon_intro zenon_H92 | zenon_intro zenon_Haa ]. % 13.66/13.88 exact (zenon_H92 zenon_H9d). % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Haa); [ zenon_intro zenon_Hac | zenon_intro zenon_Hab ]. % 13.66/13.88 exact (zenon_Hac just17). % 13.66/13.88 exact (zenon_Ha0 zenon_Hab). % 13.66/13.88 apply zenon_H9f. apply refl_equal. % 13.66/13.88 (* end of lemma zenon_L10_ *) % 13.66/13.88 assert (zenon_L11_ : (~(isa (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_computerdataartifact))) -> False). % 13.66/13.88 do 0 intro. intros zenon_Had. % 13.66/13.88 generalize (just89 (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))). zenon_intro zenon_Hae. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Hae); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haf ]. % 13.66/13.88 exact (zenon_Hb0 just3). % 13.66/13.88 exact (zenon_Had zenon_Haf). % 13.66/13.88 (* end of lemma zenon_L11_ *) % 13.66/13.88 assert (zenon_L12_ : (few (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) (c_tptpcol_16_118949)) -> (disjointwith (c_setorcollection) (c_computerdataartifact)) -> False). % 13.66/13.88 do 0 intro. intros zenon_Hb1 zenon_Hb2. % 13.66/13.88 generalize (just19 (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))). zenon_intro zenon_Hb3. % 13.66/13.88 generalize (zenon_Hb3 (c_setorcollection)). zenon_intro zenon_Hb4. % 13.66/13.88 generalize (zenon_Hb4 (c_computerdataartifact)). zenon_intro zenon_Hb5. % 13.66/13.88 apply (zenon_notand_s _ _ zenon_Hb5); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 13.66/13.88 generalize (just105 (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))). zenon_intro zenon_Hb8. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Hb8); [ zenon_intro zenon_Hba | zenon_intro zenon_Hb9 ]. % 13.66/13.88 generalize (just38 (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))). zenon_intro zenon_Hbb. % 13.66/13.88 generalize (zenon_Hbb (c_tptpcol_16_118949)). zenon_intro zenon_Hbc. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Hbc); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hbd ]. % 13.66/13.88 exact (zenon_Hbe zenon_Hb1). % 13.66/13.88 exact (zenon_Hba zenon_Hbd). % 13.66/13.88 exact (zenon_Hb7 zenon_Hb9). % 13.66/13.88 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Had | zenon_intro zenon_Hbf ]. % 13.66/13.88 apply (zenon_L11_); trivial. % 13.66/13.88 exact (zenon_Hbf zenon_Hb2). % 13.66/13.88 (* end of lemma zenon_L12_ *) % 13.66/13.88 apply NNPP. intro zenon_G. % 13.66/13.88 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((genls x y)->((genls y z)->(genls x z))))))); [ zenon_intro zenon_H5f | zenon_intro zenon_Hc0 ]. % 13.66/13.88 apply zenon_G. zenon_intro zenon_Hc1. % 13.66/13.88 generalize (just22 (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))). zenon_intro zenon_Hc2. % 13.66/13.88 generalize (zenon_Hc2 (c_tptpcol_16_118949)). zenon_intro zenon_Hc3. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Hc3); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 13.66/13.88 exact (zenon_Hc5 zenon_Hc1). % 13.66/13.88 generalize (just25 (f_urlreferentfn (f_urlfn (s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))). zenon_intro zenon_Hc6. % 13.66/13.88 generalize (zenon_Hc6 (c_tptpcol_16_118949)). zenon_intro zenon_Hc7. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Hc7); [ zenon_intro zenon_Hc8 | zenon_intro zenon_Hb1 ]. % 13.66/13.88 exact (zenon_Hc8 zenon_Hc4). % 13.66/13.88 generalize (just83 (c_intangible)). zenon_intro zenon_Hc9. % 13.66/13.88 generalize (zenon_Hc9 (c_partiallytangible)). zenon_intro zenon_Hca. % 13.66/13.88 generalize (just82 (c_setorcollection)). zenon_intro zenon_Hcb. % 13.66/13.88 generalize (zenon_Hcb (c_partiallytangible)). zenon_intro zenon_Hcc. % 13.66/13.88 generalize (zenon_Hcc (c_computerdataartifact)). zenon_intro zenon_Hcd. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Hcd); [ zenon_intro zenon_Hce | zenon_intro zenon_Hb2 ]. % 13.66/13.88 apply (zenon_notand_s _ _ zenon_Hce); [ zenon_intro zenon_Hcf | zenon_intro zenon_Ha0 ]. % 13.66/13.88 generalize (zenon_Hca (c_setorcollection)). zenon_intro zenon_Hd0. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_Hd0); [ zenon_intro zenon_Hd2 | zenon_intro zenon_Hd1 ]. % 13.66/13.88 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hd3 | zenon_intro zenon_H72 ]. % 13.66/13.88 exact (zenon_Hd3 just6). % 13.66/13.88 apply (zenon_L4_); trivial. % 13.66/13.88 exact (zenon_Hcf zenon_Hd1). % 13.66/13.88 apply (zenon_L10_); trivial. % 13.66/13.88 apply (zenon_L12_); trivial. % 13.66/13.88 apply zenon_Hc0. zenon_intro zenon_Tx_ie. apply NNPP. zenon_intro zenon_Hd5. % 13.66/13.88 apply zenon_Hd5. zenon_intro zenon_Ty_ig. apply NNPP. zenon_intro zenon_Hd7. % 13.66/13.88 apply zenon_Hd7. zenon_intro zenon_Tz_ii. apply NNPP. zenon_intro zenon_Hd9. % 13.66/13.88 apply (zenon_notimply_s _ _ zenon_Hd9). zenon_intro zenon_Hdb. zenon_intro zenon_Hda. % 13.66/13.88 apply (zenon_notimply_s _ _ zenon_Hda). zenon_intro zenon_Hdd. zenon_intro zenon_Hdc. % 13.66/13.88 generalize (just110 zenon_Tx_ie). zenon_intro zenon_Hde. % 13.66/13.88 generalize (zenon_Hde zenon_Ty_ig). zenon_intro zenon_Hdf. % 13.66/13.88 generalize (zenon_Hdf zenon_Tz_ii). zenon_intro zenon_He0. % 13.66/13.88 apply (zenon_imply_s _ _ zenon_He0); [ zenon_intro zenon_He2 | zenon_intro zenon_He1 ]. % 13.66/13.88 apply (zenon_notand_s _ _ zenon_He2); [ zenon_intro zenon_He4 | zenon_intro zenon_He3 ]. % 13.66/13.88 exact (zenon_He4 zenon_Hdb). % 13.66/13.88 exact (zenon_He3 zenon_Hdd). % 13.66/13.88 exact (zenon_Hdc zenon_He1). % 13.66/13.88 Qed. % 13.66/13.88 % SZS output end Proof % 13.66/13.88 (* END-PROOF *) % 13.66/13.88 nodes searched: 1072860 % 13.66/13.88 max branch formulas: 22682 % 13.66/13.88 proof nodes created: 4553 % 13.66/13.88 formulas created: 1916325 % 13.66/13.88 %------------------------------------------------------------------------------