%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR052+4 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n007.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:13 EDT 2022 % Result : Theorem 9.69s 9.89s % Output : Proof 9.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR052+4 : TPTP v8.1.0. Released v3.4.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.14/0.34 % Computer : n007.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sat Jun 11 00:31:07 EDT 2022 % 0.14/0.35 % CPUTime : % 9.69/9.89 (* PROOF-FOUND *) % 9.69/9.89 % SZS status Theorem % 9.69/9.89 (* BEGIN-PROOF *) % 9.69/9.89 % SZS output start Proof % 9.69/9.89 Theorem query202 : ((mtvisible (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn (s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml))) (c_translation_33)))->(genls (c_tptpcol_15_40430) (c_tptpcol_7_39939))). % 9.69/9.89 Proof. % 9.69/9.89 assert (zenon_L1_ : (~((c_tptpcol_11_40388) = (c_tptpcol_11_40388))) -> False). % 9.69/9.89 do 0 intro. intros zenon_Ha7e9. % 9.69/9.89 apply zenon_Ha7e9. apply refl_equal. % 9.69/9.89 (* end of lemma zenon_L1_ *) % 9.69/9.89 assert (zenon_L2_ : (~((c_tptpcol_10_40324) = (c_tptpcol_10_40324))) -> False). % 9.69/9.89 do 0 intro. intros zenon_Ha7ea. % 9.69/9.89 apply zenon_Ha7ea. apply refl_equal. % 9.69/9.89 (* end of lemma zenon_L2_ *) % 9.69/9.89 assert (zenon_L3_ : (~((c_tptpcol_9_40196) = (c_tptpcol_9_40196))) -> False). % 9.69/9.89 do 0 intro. intros zenon_Ha7eb. % 9.69/9.89 apply zenon_Ha7eb. apply refl_equal. % 9.69/9.89 (* end of lemma zenon_L3_ *) % 9.69/9.89 assert (zenon_L4_ : (~((c_tptpcol_8_39940) = (c_tptpcol_8_39940))) -> False). % 9.69/9.89 do 0 intro. intros zenon_Ha7ec. % 9.69/9.89 apply zenon_Ha7ec. apply refl_equal. % 9.69/9.89 (* end of lemma zenon_L4_ *) % 9.69/9.89 apply NNPP. intro zenon_G. % 9.69/9.89 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_Ha7ed | zenon_intro zenon_Ha7ee ]. % 9.69/9.89 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_Ha7f0. zenon_intro zenon_Ha7ef. % 9.69/9.89 elim (classic ((~((c_tptpcol_15_40430) = (c_tptpcol_8_39940)))/\(~(genls (c_tptpcol_15_40430) (c_tptpcol_8_39940))))); [ zenon_intro zenon_Ha7f1 | zenon_intro zenon_Ha7f2 ]. % 9.69/9.89 apply (zenon_and_s _ _ zenon_Ha7f1). zenon_intro zenon_Ha7f4. zenon_intro zenon_Ha7f3. % 9.69/9.89 elim (classic ((~((c_tptpcol_15_40430) = (c_tptpcol_9_40196)))/\(~(genls (c_tptpcol_15_40430) (c_tptpcol_9_40196))))); [ zenon_intro zenon_Ha7f5 | zenon_intro zenon_Ha7f6 ]. % 9.69/9.89 apply (zenon_and_s _ _ zenon_Ha7f5). zenon_intro zenon_Ha7f8. zenon_intro zenon_Ha7f7. % 9.69/9.89 elim (classic ((~((c_tptpcol_15_40430) = (c_tptpcol_10_40324)))/\(~(genls (c_tptpcol_15_40430) (c_tptpcol_10_40324))))); [ zenon_intro zenon_Ha7f9 | zenon_intro zenon_Ha7fa ]. % 9.69/9.89 apply (zenon_and_s _ _ zenon_Ha7f9). zenon_intro zenon_Ha7fc. zenon_intro zenon_Ha7fb. % 9.69/9.89 elim (classic ((~((c_tptpcol_15_40430) = (c_tptpcol_11_40388)))/\(~(genls (c_tptpcol_15_40430) (c_tptpcol_11_40388))))); [ zenon_intro zenon_Ha7fd | zenon_intro zenon_Ha7fe ]. % 9.69/9.89 apply (zenon_and_s _ _ zenon_Ha7fd). zenon_intro zenon_Ha800. zenon_intro zenon_Ha7ff. % 9.69/9.89 elim (classic ((~((c_tptpcol_15_40430) = (c_tptpcol_12_40420)))/\(~(genls (c_tptpcol_15_40430) (c_tptpcol_12_40420))))); [ zenon_intro zenon_Ha801 | zenon_intro zenon_Ha802 ]. % 9.69/9.89 apply (zenon_and_s _ _ zenon_Ha801). zenon_intro zenon_Ha804. zenon_intro zenon_Ha803. % 9.69/9.89 elim (classic ((~((c_tptpcol_15_40430) = (c_tptpcol_13_40421)))/\(~(genls (c_tptpcol_15_40430) (c_tptpcol_13_40421))))); [ zenon_intro zenon_Ha805 | zenon_intro zenon_Ha806 ]. % 9.69/9.89 apply (zenon_and_s _ _ zenon_Ha805). zenon_intro zenon_Ha808. zenon_intro zenon_Ha807. % 9.69/9.89 elim (classic ((~((c_tptpcol_15_40430) = (c_tptpcol_14_40429)))/\(~(genls (c_tptpcol_15_40430) (c_tptpcol_14_40429))))); [ zenon_intro zenon_Ha809 | zenon_intro zenon_Ha80a ]. % 9.69/9.89 apply (zenon_and_s _ _ zenon_Ha809). zenon_intro zenon_Ha80c. zenon_intro zenon_Ha80b. % 9.69/9.89 exact (zenon_Ha80b ax3_5727). % 9.69/9.89 cut ((genls (c_tptpcol_14_40429) (c_tptpcol_13_40421)) = (genls (c_tptpcol_15_40430) (c_tptpcol_13_40421))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha807. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact ax3_10200. % 9.69/9.89 cut (((c_tptpcol_13_40421) = (c_tptpcol_13_40421))); [idtac | apply NNPP; zenon_intro zenon_Ha80d]. % 9.69/9.89 cut (((c_tptpcol_14_40429) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha80e]. % 9.69/9.89 congruence. % 9.69/9.89 apply (zenon_notand_s _ _ zenon_Ha80a); [ zenon_intro zenon_Ha810 | zenon_intro zenon_Ha80f ]. % 9.69/9.89 apply zenon_Ha810. zenon_intro zenon_Ha811. % 9.69/9.89 elim (classic ((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [ zenon_intro zenon_Ha812 | zenon_intro zenon_Ha813 ]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430)) = ((c_tptpcol_14_40429) = (c_tptpcol_15_40430))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha80e. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact zenon_Ha812. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha813]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_14_40429))); [idtac | apply NNPP; zenon_intro zenon_Ha80c]. % 9.69/9.89 congruence. % 9.69/9.89 exact (zenon_Ha80c zenon_Ha811). % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha80f. zenon_intro ax3_5727. % 9.69/9.89 generalize (zenon_Ha7ed (c_tptpcol_15_40430)). zenon_intro zenon_Ha814. % 9.69/9.89 generalize (zenon_Ha814 (c_tptpcol_14_40429)). zenon_intro zenon_Ha815. % 9.69/9.89 generalize (zenon_Ha815 (c_tptpcol_13_40421)). zenon_intro zenon_Ha816. % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha816); [ zenon_intro zenon_Ha80b | zenon_intro zenon_Ha817 ]. % 9.69/9.89 exact (zenon_Ha80b ax3_5727). % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha817); [ zenon_intro zenon_Ha819 | zenon_intro zenon_Ha818 ]. % 9.69/9.89 exact (zenon_Ha819 ax3_10200). % 9.69/9.89 exact (zenon_Ha807 zenon_Ha818). % 9.69/9.89 apply zenon_Ha80d. apply refl_equal. % 9.69/9.89 cut ((genls (c_tptpcol_13_40421) (c_tptpcol_12_40420)) = (genls (c_tptpcol_15_40430) (c_tptpcol_12_40420))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha803. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact ax3_19340. % 9.69/9.89 cut (((c_tptpcol_12_40420) = (c_tptpcol_12_40420))); [idtac | apply NNPP; zenon_intro zenon_Ha81a]. % 9.69/9.89 cut (((c_tptpcol_13_40421) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha81b]. % 9.69/9.89 congruence. % 9.69/9.89 apply (zenon_notand_s _ _ zenon_Ha806); [ zenon_intro zenon_Ha81d | zenon_intro zenon_Ha81c ]. % 9.69/9.89 apply zenon_Ha81d. zenon_intro zenon_Ha81e. % 9.69/9.89 elim (classic ((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [ zenon_intro zenon_Ha812 | zenon_intro zenon_Ha813 ]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430)) = ((c_tptpcol_13_40421) = (c_tptpcol_15_40430))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha81b. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact zenon_Ha812. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha813]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_13_40421))); [idtac | apply NNPP; zenon_intro zenon_Ha808]. % 9.69/9.89 congruence. % 9.69/9.89 exact (zenon_Ha808 zenon_Ha81e). % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha81c. zenon_intro zenon_Ha818. % 9.69/9.89 generalize (zenon_Ha7ed (c_tptpcol_15_40430)). zenon_intro zenon_Ha814. % 9.69/9.89 generalize (zenon_Ha814 (c_tptpcol_13_40421)). zenon_intro zenon_Ha81f. % 9.69/9.89 generalize (zenon_Ha81f (c_tptpcol_12_40420)). zenon_intro zenon_Ha820. % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha820); [ zenon_intro zenon_Ha807 | zenon_intro zenon_Ha821 ]. % 9.69/9.89 exact (zenon_Ha807 zenon_Ha818). % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha821); [ zenon_intro zenon_Ha823 | zenon_intro zenon_Ha822 ]. % 9.69/9.89 exact (zenon_Ha823 ax3_19340). % 9.69/9.89 exact (zenon_Ha803 zenon_Ha822). % 9.69/9.89 apply zenon_Ha81a. apply refl_equal. % 9.69/9.89 cut ((genls (c_tptpcol_12_40420) (c_tptpcol_11_40388)) = (genls (c_tptpcol_15_40430) (c_tptpcol_11_40388))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha7ff. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact ax3_8138. % 9.69/9.89 cut (((c_tptpcol_11_40388) = (c_tptpcol_11_40388))); [idtac | apply NNPP; zenon_intro zenon_Ha7e9]. % 9.69/9.89 cut (((c_tptpcol_12_40420) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha824]. % 9.69/9.89 congruence. % 9.69/9.89 apply (zenon_notand_s _ _ zenon_Ha802); [ zenon_intro zenon_Ha826 | zenon_intro zenon_Ha825 ]. % 9.69/9.89 apply zenon_Ha826. zenon_intro zenon_Ha827. % 9.69/9.89 elim (classic ((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [ zenon_intro zenon_Ha812 | zenon_intro zenon_Ha813 ]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430)) = ((c_tptpcol_12_40420) = (c_tptpcol_15_40430))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha824. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact zenon_Ha812. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha813]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_12_40420))); [idtac | apply NNPP; zenon_intro zenon_Ha804]. % 9.69/9.89 congruence. % 9.69/9.89 exact (zenon_Ha804 zenon_Ha827). % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha825. zenon_intro zenon_Ha822. % 9.69/9.89 generalize (zenon_Ha7ed (c_tptpcol_15_40430)). zenon_intro zenon_Ha814. % 9.69/9.89 generalize (zenon_Ha814 (c_tptpcol_12_40420)). zenon_intro zenon_Ha828. % 9.69/9.89 generalize (zenon_Ha828 (c_tptpcol_11_40388)). zenon_intro zenon_Ha829. % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha829); [ zenon_intro zenon_Ha803 | zenon_intro zenon_Ha82a ]. % 9.69/9.89 exact (zenon_Ha803 zenon_Ha822). % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha82a); [ zenon_intro zenon_Ha82c | zenon_intro zenon_Ha82b ]. % 9.69/9.89 exact (zenon_Ha82c ax3_8138). % 9.69/9.89 exact (zenon_Ha7ff zenon_Ha82b). % 9.69/9.89 apply zenon_Ha7e9. apply refl_equal. % 9.69/9.89 cut ((genls (c_tptpcol_11_40388) (c_tptpcol_10_40324)) = (genls (c_tptpcol_15_40430) (c_tptpcol_10_40324))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha7fb. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact ax3_13323. % 9.69/9.89 cut (((c_tptpcol_10_40324) = (c_tptpcol_10_40324))); [idtac | apply NNPP; zenon_intro zenon_Ha7ea]. % 9.69/9.89 cut (((c_tptpcol_11_40388) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha82d]. % 9.69/9.89 congruence. % 9.69/9.89 apply (zenon_notand_s _ _ zenon_Ha7fe); [ zenon_intro zenon_Ha82f | zenon_intro zenon_Ha82e ]. % 9.69/9.89 apply zenon_Ha82f. zenon_intro zenon_Ha830. % 9.69/9.89 elim (classic ((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [ zenon_intro zenon_Ha812 | zenon_intro zenon_Ha813 ]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430)) = ((c_tptpcol_11_40388) = (c_tptpcol_15_40430))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha82d. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact zenon_Ha812. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha813]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_11_40388))); [idtac | apply NNPP; zenon_intro zenon_Ha800]. % 9.69/9.89 congruence. % 9.69/9.89 exact (zenon_Ha800 zenon_Ha830). % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha82e. zenon_intro zenon_Ha82b. % 9.69/9.89 generalize (zenon_Ha7ed (c_tptpcol_15_40430)). zenon_intro zenon_Ha814. % 9.69/9.89 generalize (zenon_Ha814 (c_tptpcol_11_40388)). zenon_intro zenon_Ha831. % 9.69/9.89 generalize (zenon_Ha831 (c_tptpcol_10_40324)). zenon_intro zenon_Ha832. % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha832); [ zenon_intro zenon_Ha7ff | zenon_intro zenon_Ha833 ]. % 9.69/9.89 exact (zenon_Ha7ff zenon_Ha82b). % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha833); [ zenon_intro zenon_Ha835 | zenon_intro zenon_Ha834 ]. % 9.69/9.89 exact (zenon_Ha835 ax3_13323). % 9.69/9.89 exact (zenon_Ha7fb zenon_Ha834). % 9.69/9.89 apply zenon_Ha7ea. apply refl_equal. % 9.69/9.89 cut ((genls (c_tptpcol_10_40324) (c_tptpcol_9_40196)) = (genls (c_tptpcol_15_40430) (c_tptpcol_9_40196))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha7f7. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact ax3_5606. % 9.69/9.89 cut (((c_tptpcol_9_40196) = (c_tptpcol_9_40196))); [idtac | apply NNPP; zenon_intro zenon_Ha7eb]. % 9.69/9.89 cut (((c_tptpcol_10_40324) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha836]. % 9.69/9.89 congruence. % 9.69/9.89 apply (zenon_notand_s _ _ zenon_Ha7fa); [ zenon_intro zenon_Ha838 | zenon_intro zenon_Ha837 ]. % 9.69/9.89 apply zenon_Ha838. zenon_intro zenon_Ha839. % 9.69/9.89 elim (classic ((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [ zenon_intro zenon_Ha812 | zenon_intro zenon_Ha813 ]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430)) = ((c_tptpcol_10_40324) = (c_tptpcol_15_40430))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha836. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact zenon_Ha812. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha813]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_10_40324))); [idtac | apply NNPP; zenon_intro zenon_Ha7fc]. % 9.69/9.89 congruence. % 9.69/9.89 exact (zenon_Ha7fc zenon_Ha839). % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha837. zenon_intro zenon_Ha834. % 9.69/9.89 generalize (zenon_Ha7ed (c_tptpcol_15_40430)). zenon_intro zenon_Ha814. % 9.69/9.89 generalize (zenon_Ha814 (c_tptpcol_10_40324)). zenon_intro zenon_Ha83a. % 9.69/9.89 generalize (zenon_Ha83a (c_tptpcol_9_40196)). zenon_intro zenon_Ha83b. % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha83b); [ zenon_intro zenon_Ha7fb | zenon_intro zenon_Ha83c ]. % 9.69/9.89 exact (zenon_Ha7fb zenon_Ha834). % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha83c); [ zenon_intro zenon_Ha83e | zenon_intro zenon_Ha83d ]. % 9.69/9.89 exact (zenon_Ha83e ax3_5606). % 9.69/9.89 exact (zenon_Ha7f7 zenon_Ha83d). % 9.69/9.89 apply zenon_Ha7eb. apply refl_equal. % 9.69/9.89 cut ((genls (c_tptpcol_9_40196) (c_tptpcol_8_39940)) = (genls (c_tptpcol_15_40430) (c_tptpcol_8_39940))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha7f3. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact ax3_6645. % 9.69/9.89 cut (((c_tptpcol_8_39940) = (c_tptpcol_8_39940))); [idtac | apply NNPP; zenon_intro zenon_Ha7ec]. % 9.69/9.89 cut (((c_tptpcol_9_40196) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha83f]. % 9.69/9.89 congruence. % 9.69/9.89 apply (zenon_notand_s _ _ zenon_Ha7f6); [ zenon_intro zenon_Ha841 | zenon_intro zenon_Ha840 ]. % 9.69/9.89 apply zenon_Ha841. zenon_intro zenon_Ha842. % 9.69/9.89 elim (classic ((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [ zenon_intro zenon_Ha812 | zenon_intro zenon_Ha813 ]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430)) = ((c_tptpcol_9_40196) = (c_tptpcol_15_40430))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha83f. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact zenon_Ha812. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha813]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_9_40196))); [idtac | apply NNPP; zenon_intro zenon_Ha7f8]. % 9.69/9.89 congruence. % 9.69/9.89 exact (zenon_Ha7f8 zenon_Ha842). % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha840. zenon_intro zenon_Ha83d. % 9.69/9.89 generalize (zenon_Ha7ed (c_tptpcol_15_40430)). zenon_intro zenon_Ha814. % 9.69/9.89 generalize (zenon_Ha814 (c_tptpcol_9_40196)). zenon_intro zenon_Ha843. % 9.69/9.89 generalize (zenon_Ha843 (c_tptpcol_8_39940)). zenon_intro zenon_Ha844. % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha844); [ zenon_intro zenon_Ha7f7 | zenon_intro zenon_Ha845 ]. % 9.69/9.89 exact (zenon_Ha7f7 zenon_Ha83d). % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha845); [ zenon_intro zenon_Ha847 | zenon_intro zenon_Ha846 ]. % 9.69/9.89 exact (zenon_Ha847 ax3_6645). % 9.69/9.89 exact (zenon_Ha7f3 zenon_Ha846). % 9.69/9.89 apply zenon_Ha7ec. apply refl_equal. % 9.69/9.89 cut ((genls (c_tptpcol_8_39940) (c_tptpcol_7_39939)) = (genls (c_tptpcol_15_40430) (c_tptpcol_7_39939))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha7ef. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact ax3_4357. % 9.69/9.89 cut (((c_tptpcol_7_39939) = (c_tptpcol_7_39939))); [idtac | apply NNPP; zenon_intro zenon_Ha848]. % 9.69/9.89 cut (((c_tptpcol_8_39940) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha849]. % 9.69/9.89 congruence. % 9.69/9.89 apply (zenon_notand_s _ _ zenon_Ha7f2); [ zenon_intro zenon_Ha84b | zenon_intro zenon_Ha84a ]. % 9.69/9.89 apply zenon_Ha84b. zenon_intro zenon_Ha84c. % 9.69/9.89 elim (classic ((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [ zenon_intro zenon_Ha812 | zenon_intro zenon_Ha813 ]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430)) = ((c_tptpcol_8_39940) = (c_tptpcol_15_40430))). % 9.69/9.89 intro zenon_D_pnotp. % 9.69/9.89 apply zenon_Ha849. % 9.69/9.89 rewrite <- zenon_D_pnotp. % 9.69/9.89 exact zenon_Ha812. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_15_40430))); [idtac | apply NNPP; zenon_intro zenon_Ha813]. % 9.69/9.89 cut (((c_tptpcol_15_40430) = (c_tptpcol_8_39940))); [idtac | apply NNPP; zenon_intro zenon_Ha7f4]. % 9.69/9.89 congruence. % 9.69/9.89 exact (zenon_Ha7f4 zenon_Ha84c). % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha813. apply refl_equal. % 9.69/9.89 apply zenon_Ha84a. zenon_intro zenon_Ha846. % 9.69/9.89 generalize (zenon_Ha7ed (c_tptpcol_15_40430)). zenon_intro zenon_Ha814. % 9.69/9.89 generalize (zenon_Ha814 (c_tptpcol_8_39940)). zenon_intro zenon_Ha84d. % 9.69/9.89 generalize (zenon_Ha84d (c_tptpcol_7_39939)). zenon_intro zenon_Ha84e. % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha84e); [ zenon_intro zenon_Ha7f3 | zenon_intro zenon_Ha84f ]. % 9.69/9.89 exact (zenon_Ha7f3 zenon_Ha846). % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha84f); [ zenon_intro zenon_Ha851 | zenon_intro zenon_Ha850 ]. % 9.69/9.89 exact (zenon_Ha851 ax3_4357). % 9.69/9.89 exact (zenon_Ha7ef zenon_Ha850). % 9.69/9.89 apply zenon_Ha848. apply refl_equal. % 9.69/9.89 apply zenon_Ha7ee. zenon_intro zenon_Tx_clti. apply NNPP. zenon_intro zenon_Ha853. % 9.69/9.89 apply zenon_Ha853. zenon_intro zenon_Ty_cltk. apply NNPP. zenon_intro zenon_Ha855. % 9.69/9.89 apply zenon_Ha855. zenon_intro zenon_Tz_cltm. apply NNPP. zenon_intro zenon_Ha857. % 9.69/9.89 apply (zenon_notimply_s _ _ zenon_Ha857). zenon_intro zenon_Ha859. zenon_intro zenon_Ha858. % 9.69/9.89 apply (zenon_notimply_s _ _ zenon_Ha858). zenon_intro zenon_Ha85b. zenon_intro zenon_Ha85a. % 9.69/9.89 generalize (ax3_44178 zenon_Tx_clti). zenon_intro zenon_Ha85c. % 9.69/9.89 generalize (zenon_Ha85c zenon_Ty_cltk). zenon_intro zenon_Ha85d. % 9.69/9.89 generalize (zenon_Ha85d zenon_Tz_cltm). zenon_intro zenon_Ha85e. % 9.69/9.89 apply (zenon_imply_s _ _ zenon_Ha85e); [ zenon_intro zenon_Ha860 | zenon_intro zenon_Ha85f ]. % 9.69/9.89 apply (zenon_notand_s _ _ zenon_Ha860); [ zenon_intro zenon_Ha862 | zenon_intro zenon_Ha861 ]. % 9.69/9.89 exact (zenon_Ha862 zenon_Ha859). % 9.69/9.89 exact (zenon_Ha861 zenon_Ha85b). % 9.69/9.89 exact (zenon_Ha85a zenon_Ha85f). % 9.69/9.89 Qed. % 9.69/9.89 % SZS output end Proof % 9.69/9.89 (* END-PROOF *) % 9.69/9.89 nodes searched: 133329 % 9.69/9.89 max branch formulas: 126961 % 9.69/9.89 proof nodes created: 167 % 9.69/9.89 formulas created: 1303171 % 9.69/9.89 %------------------------------------------------------------------------------