%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SYN551+2 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 13:54:17 EDT 2022 % Result : Theorem 2.23s 2.43s % Output : Proof 2.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYN551+2 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.12/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n017.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 : Mon Jul 11 12:44:33 EDT 2022 % 0.12/0.33 % CPUTime : % 2.23/2.43 (* PROOF-FOUND *) % 2.23/2.43 % SZS status Theorem % 2.23/2.43 (* BEGIN-PROOF *) % 2.23/2.43 % SZS output start Proof % 2.23/2.43 Theorem prove_this_cute_thing : ((exists X : zenon_U, (forall Y : zenon_U, ((Y = (f (g Y)))<->(X = Y))))<->(exists X : zenon_U, (forall Y : zenon_U, ((Y = (g (f Y)))<->(X = Y))))). % 2.23/2.43 Proof. % 2.23/2.43 assert (zenon_L1_ : forall (zenon_TX_d : zenon_U), (~((g (f (g (f zenon_TX_d)))) = (g (f (g (f (g (f zenon_TX_d)))))))) -> ((g (f zenon_TX_d)) = (g (f (g (f zenon_TX_d))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H1 zenon_H2. % 2.23/2.43 cut (((f (g (f zenon_TX_d))) = (f (g (f (g (f zenon_TX_d))))))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f zenon_TX_d)) = (g (f (g (f zenon_TX_d)))))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 2.23/2.43 congruence. % 2.23/2.43 exact (zenon_H5 zenon_H2). % 2.23/2.43 (* end of lemma zenon_L1_ *) % 2.23/2.43 assert (zenon_L2_ : forall (zenon_TX_d : zenon_U), (~((g (f (g (f (g (f zenon_TX_d)))))) = (g (f (g (f (g (f (g (f zenon_TX_d)))))))))) -> ((g (f (g (f zenon_TX_d)))) = (g (f (g (f (g (f zenon_TX_d))))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H6 zenon_H7. % 2.23/2.43 cut (((f (g (f (g (f zenon_TX_d))))) = (f (g (f (g (f (g (f zenon_TX_d))))))))); [idtac | apply NNPP; zenon_intro zenon_H8]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f zenon_TX_d)))) = (g (f (g (f (g (f zenon_TX_d)))))))); [idtac | apply NNPP; zenon_intro zenon_H1]. % 2.23/2.43 congruence. % 2.23/2.43 exact (zenon_H1 zenon_H7). % 2.23/2.43 (* end of lemma zenon_L2_ *) % 2.23/2.43 assert (zenon_L3_ : forall (zenon_TX_d : zenon_U), (~((g (f (g (f (g (f zenon_TX_d)))))) = (g (f zenon_TX_d)))) -> (zenon_TX_d = (g (f (g (f zenon_TX_d))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H9 zenon_Ha. % 2.23/2.43 cut (((f (g (f (g (f zenon_TX_d))))) = (f zenon_TX_d))); [idtac | apply NNPP; zenon_intro zenon_Hb]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f zenon_TX_d)))) = zenon_TX_d)); [idtac | apply NNPP; zenon_intro zenon_Hc]. % 2.23/2.43 congruence. % 2.23/2.43 apply zenon_Hc. apply sym_equal. exact zenon_Ha. % 2.23/2.43 (* end of lemma zenon_L3_ *) % 2.23/2.43 assert (zenon_L4_ : forall (zenon_TX_d : zenon_U), (~((g (f (g (f (g (f (g (f zenon_TX_d)))))))) = (g (f (g (f zenon_TX_d)))))) -> (zenon_TX_d = (g (f (g (f zenon_TX_d))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_Hd zenon_Ha. % 2.23/2.43 cut (((f (g (f (g (f (g (f zenon_TX_d))))))) = (f (g (f zenon_TX_d))))); [idtac | apply NNPP; zenon_intro zenon_He]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f zenon_TX_d)))))) = (g (f zenon_TX_d)))); [idtac | apply NNPP; zenon_intro zenon_H9]. % 2.23/2.43 congruence. % 2.23/2.43 apply (zenon_L3_ zenon_TX_d); trivial. % 2.23/2.43 (* end of lemma zenon_L4_ *) % 2.23/2.43 assert (zenon_L5_ : forall (zenon_TX_d : zenon_U), (~((g (f (g (f (g (f (g (f (g (f zenon_TX_d)))))))))) = (g (f (g (f (g (f zenon_TX_d)))))))) -> (zenon_TX_d = (g (f (g (f zenon_TX_d))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_Hf zenon_Ha. % 2.23/2.43 cut (((f (g (f (g (f (g (f (g (f zenon_TX_d))))))))) = (f (g (f (g (f zenon_TX_d))))))); [idtac | apply NNPP; zenon_intro zenon_H10]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f (g (f zenon_TX_d)))))))) = (g (f (g (f zenon_TX_d)))))); [idtac | apply NNPP; zenon_intro zenon_Hd]. % 2.23/2.43 congruence. % 2.23/2.43 apply (zenon_L4_ zenon_TX_d); trivial. % 2.23/2.43 (* end of lemma zenon_L5_ *) % 2.23/2.43 assert (zenon_L6_ : forall (zenon_TY_t : zenon_U), (~((g zenon_TY_t) = (g (f (g zenon_TY_t))))) -> (zenon_TY_t = (f (g zenon_TY_t))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H11 zenon_H12. % 2.23/2.43 cut ((zenon_TY_t = (f (g zenon_TY_t)))); [idtac | apply NNPP; zenon_intro zenon_H14]. % 2.23/2.43 congruence. % 2.23/2.43 exact (zenon_H14 zenon_H12). % 2.23/2.43 (* end of lemma zenon_L6_ *) % 2.23/2.43 assert (zenon_L7_ : forall (zenon_TX_d : zenon_U), (~((g (f (g (f (g (f (g (f (g (f (g (f zenon_TX_d)))))))))))) = (g (f (g (f (g (f zenon_TX_d)))))))) -> (zenon_TX_d = (g (f (g (f (g (f zenon_TX_d))))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H15 zenon_H16. % 2.23/2.43 cut (((f (g (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))) = (f (g (f (g (f zenon_TX_d))))))); [idtac | apply NNPP; zenon_intro zenon_H17]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f (g (f (g (f zenon_TX_d)))))))))) = (g (f (g (f zenon_TX_d)))))); [idtac | apply NNPP; zenon_intro zenon_H18]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g (f (g (f (g (f zenon_TX_d))))))))) = (f (g (f zenon_TX_d))))); [idtac | apply NNPP; zenon_intro zenon_H19]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f (g (f zenon_TX_d)))))))) = (g (f zenon_TX_d)))); [idtac | apply NNPP; zenon_intro zenon_H1a]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g (f (g (f zenon_TX_d))))))) = (f zenon_TX_d))); [idtac | apply NNPP; zenon_intro zenon_H1b]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f zenon_TX_d)))))) = zenon_TX_d)); [idtac | apply NNPP; zenon_intro zenon_H1c]. % 2.23/2.43 congruence. % 2.23/2.43 apply zenon_H1c. apply sym_equal. exact zenon_H16. % 2.23/2.43 (* end of lemma zenon_L7_ *) % 2.23/2.43 assert (zenon_L8_ : forall (zenon_TX_bf : zenon_U), (~((f (g (f (g zenon_TX_bf)))) = (f (g (f (g (f (g zenon_TX_bf)))))))) -> ((f (g zenon_TX_bf)) = (f (g (f (g zenon_TX_bf))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H1d zenon_H1e. % 2.23/2.43 cut (((g (f (g zenon_TX_bf))) = (g (f (g (f (g zenon_TX_bf))))))); [idtac | apply NNPP; zenon_intro zenon_H20]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g zenon_TX_bf)) = (f (g (f (g zenon_TX_bf)))))); [idtac | apply NNPP; zenon_intro zenon_H21]. % 2.23/2.43 congruence. % 2.23/2.43 exact (zenon_H21 zenon_H1e). % 2.23/2.43 (* end of lemma zenon_L8_ *) % 2.23/2.43 assert (zenon_L9_ : forall (zenon_TX_bf : zenon_U), (~((f (g (f (g (f (g zenon_TX_bf)))))) = (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))) -> ((f (g (f (g zenon_TX_bf)))) = (f (g (f (g (f (g zenon_TX_bf))))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H22 zenon_H23. % 2.23/2.43 cut (((g (f (g (f (g zenon_TX_bf))))) = (g (f (g (f (g (f (g zenon_TX_bf))))))))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g zenon_TX_bf)))) = (f (g (f (g (f (g zenon_TX_bf)))))))); [idtac | apply NNPP; zenon_intro zenon_H1d]. % 2.23/2.43 congruence. % 2.23/2.43 exact (zenon_H1d zenon_H23). % 2.23/2.43 (* end of lemma zenon_L9_ *) % 2.23/2.43 assert (zenon_L10_ : forall (zenon_TX_bf : zenon_U), (~((f (g (f (g (f (g zenon_TX_bf)))))) = (f (g zenon_TX_bf)))) -> (zenon_TX_bf = (f (g (f (g zenon_TX_bf))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H25 zenon_H26. % 2.23/2.43 cut (((g (f (g (f (g zenon_TX_bf))))) = (g zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_H27]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g zenon_TX_bf)))) = zenon_TX_bf)); [idtac | apply NNPP; zenon_intro zenon_H28]. % 2.23/2.43 congruence. % 2.23/2.43 apply zenon_H28. apply sym_equal. exact zenon_H26. % 2.23/2.43 (* end of lemma zenon_L10_ *) % 2.23/2.43 assert (zenon_L11_ : forall (zenon_TX_bf : zenon_U), (~((f (g (f (g (f (g (f (g zenon_TX_bf)))))))) = (f (g (f (g zenon_TX_bf)))))) -> (zenon_TX_bf = (f (g (f (g zenon_TX_bf))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H29 zenon_H26. % 2.23/2.43 cut (((g (f (g (f (g (f (g zenon_TX_bf))))))) = (g (f (g zenon_TX_bf))))); [idtac | apply NNPP; zenon_intro zenon_H2a]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g (f (g zenon_TX_bf)))))) = (f (g zenon_TX_bf)))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 2.23/2.43 congruence. % 2.23/2.43 apply (zenon_L10_ zenon_TX_bf); trivial. % 2.23/2.43 (* end of lemma zenon_L11_ *) % 2.23/2.43 assert (zenon_L12_ : forall (zenon_TX_bf : zenon_U), (~((f (g (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))) = (f (g (f (g (f (g zenon_TX_bf)))))))) -> (zenon_TX_bf = (f (g (f (g zenon_TX_bf))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H2b zenon_H26. % 2.23/2.43 cut (((g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))) = (g (f (g (f (g zenon_TX_bf))))))); [idtac | apply NNPP; zenon_intro zenon_H2c]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g (f (g (f (g zenon_TX_bf)))))))) = (f (g (f (g zenon_TX_bf)))))); [idtac | apply NNPP; zenon_intro zenon_H29]. % 2.23/2.43 congruence. % 2.23/2.43 apply (zenon_L11_ zenon_TX_bf); trivial. % 2.23/2.43 (* end of lemma zenon_L12_ *) % 2.23/2.43 assert (zenon_L13_ : forall (zenon_TY_bv : zenon_U), (~((f zenon_TY_bv) = (f (g (f zenon_TY_bv))))) -> (zenon_TY_bv = (g (f zenon_TY_bv))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H2d zenon_H2e. % 2.23/2.43 cut ((zenon_TY_bv = (g (f zenon_TY_bv)))); [idtac | apply NNPP; zenon_intro zenon_H30]. % 2.23/2.43 congruence. % 2.23/2.43 exact (zenon_H30 zenon_H2e). % 2.23/2.43 (* end of lemma zenon_L13_ *) % 2.23/2.43 assert (zenon_L14_ : forall (zenon_TX_bf : zenon_U), (~((f (g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))))) = (f (g (f (g (f (g zenon_TX_bf)))))))) -> (zenon_TX_bf = (f (g (f (g (f (g zenon_TX_bf))))))) -> False). % 2.23/2.43 do 1 intro. intros zenon_H31 zenon_H32. % 2.23/2.43 cut (((g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))) = (g (f (g (f (g zenon_TX_bf))))))); [idtac | apply NNPP; zenon_intro zenon_H33]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))) = (f (g (f (g zenon_TX_bf)))))); [idtac | apply NNPP; zenon_intro zenon_H34]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))) = (g (f (g zenon_TX_bf))))); [idtac | apply NNPP; zenon_intro zenon_H35]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g (f (g (f (g zenon_TX_bf)))))))) = (f (g zenon_TX_bf)))); [idtac | apply NNPP; zenon_intro zenon_H36]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f (g zenon_TX_bf))))))) = (g zenon_TX_bf))); [idtac | apply NNPP; zenon_intro zenon_H37]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g (f (g zenon_TX_bf)))))) = zenon_TX_bf)); [idtac | apply NNPP; zenon_intro zenon_H38]. % 2.23/2.43 congruence. % 2.23/2.43 apply zenon_H38. apply sym_equal. exact zenon_H32. % 2.23/2.43 (* end of lemma zenon_L14_ *) % 2.23/2.43 apply NNPP. intro zenon_G. % 2.23/2.43 apply (zenon_notequiv_s _ _ zenon_G); [ zenon_intro zenon_H3c; zenon_intro zenon_H3b | zenon_intro zenon_H3a; zenon_intro zenon_H39 ]. % 2.23/2.43 elim zenon_H3b. zenon_intro zenon_TX_d. zenon_intro zenon_H3d. % 2.23/2.43 generalize (zenon_H3d zenon_TX_d). zenon_intro zenon_H3e. % 2.23/2.43 apply (zenon_equiv_s _ _ zenon_H3e); [ zenon_intro zenon_H42; zenon_intro zenon_H41 | zenon_intro zenon_H40; zenon_intro zenon_H3f ]. % 2.23/2.43 apply zenon_H41. apply refl_equal. % 2.23/2.43 generalize (zenon_H3d (g (f zenon_TX_d))). zenon_intro zenon_H43. % 2.23/2.43 apply (zenon_equiv_s _ _ zenon_H43); [ zenon_intro zenon_H5; zenon_intro zenon_H42 | zenon_intro zenon_H2; zenon_intro zenon_H40 ]. % 2.23/2.43 exact (zenon_H42 zenon_H40). % 2.23/2.43 generalize (zenon_H3d (g (f (g (f zenon_TX_d))))). zenon_intro zenon_H44. % 2.23/2.43 apply (zenon_equiv_s _ _ zenon_H44); [ zenon_intro zenon_H1; zenon_intro zenon_H45 | zenon_intro zenon_H7; zenon_intro zenon_Ha ]. % 2.23/2.43 apply (zenon_L1_ zenon_TX_d); trivial. % 2.23/2.43 generalize (zenon_H3d (g (f (g (f (g (f zenon_TX_d))))))). zenon_intro zenon_H46. % 2.23/2.43 apply (zenon_equiv_s _ _ zenon_H46); [ zenon_intro zenon_H6; zenon_intro zenon_H48 | zenon_intro zenon_H47; zenon_intro zenon_H16 ]. % 2.23/2.43 apply (zenon_L2_ zenon_TX_d); trivial. % 2.23/2.43 generalize (zenon_H3d (g (f (g (f (g (f (g (f zenon_TX_d))))))))). zenon_intro zenon_H49. % 2.23/2.43 apply (zenon_equiv_s _ _ zenon_H49); [ zenon_intro zenon_H4d; zenon_intro zenon_H4c | zenon_intro zenon_H4b; zenon_intro zenon_H4a ]. % 2.23/2.43 cut (((f (g (f (g (f (g (f zenon_TX_d))))))) = (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))); [idtac | apply NNPP; zenon_intro zenon_H4e]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f zenon_TX_d)))))) = (g (f (g (f (g (f (g (f zenon_TX_d)))))))))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 2.23/2.43 congruence. % 2.23/2.43 exact (zenon_H6 zenon_H47). % 2.23/2.43 generalize (zenon_H3d (g (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))). zenon_intro zenon_H4f. % 2.23/2.43 apply (zenon_equiv_s _ _ zenon_H4f); [ zenon_intro zenon_H53; zenon_intro zenon_H52 | zenon_intro zenon_H51; zenon_intro zenon_H50 ]. % 2.23/2.43 cut (((f (g (f (g (f (g (f (g (f zenon_TX_d))))))))) = (f (g (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))))); [idtac | apply NNPP; zenon_intro zenon_H54]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((g (f (g (f (g (f (g (f zenon_TX_d)))))))) = (g (f (g (f (g (f (g (f (g (f zenon_TX_d)))))))))))); [idtac | apply NNPP; zenon_intro zenon_H4d]. % 2.23/2.43 congruence. % 2.23/2.43 exact (zenon_H4d zenon_H4b). % 2.23/2.43 apply zenon_H3c. exists (f (g (f (g (f (g (f zenon_TX_d))))))). apply NNPP. zenon_intro zenon_H55. % 2.23/2.43 apply (zenon_notallex_s (fun Y : zenon_U => ((Y = (f (g Y)))<->((f (g (f (g (f (g (f zenon_TX_d))))))) = Y))) zenon_H55); [ zenon_intro zenon_H56; idtac ]. % 2.23/2.43 elim zenon_H56. zenon_intro zenon_TY_t. zenon_intro zenon_H57. % 2.23/2.43 apply (zenon_notequiv_s _ _ zenon_H57); [ zenon_intro zenon_H14; zenon_intro zenon_H59 | zenon_intro zenon_H12; zenon_intro zenon_H58 ]. % 2.23/2.43 elim (classic ((f (g zenon_TY_t)) = (f (g zenon_TY_t)))); [ zenon_intro zenon_H5a | zenon_intro zenon_H5b ]. % 2.23/2.43 cut (((f (g zenon_TY_t)) = (f (g zenon_TY_t))) = (zenon_TY_t = (f (g zenon_TY_t)))). % 2.23/2.43 intro zenon_D_pnotp. % 2.23/2.43 apply zenon_H14. % 2.23/2.43 rewrite <- zenon_D_pnotp. % 2.23/2.43 exact zenon_H5a. % 2.23/2.43 cut (((f (g zenon_TY_t)) = (f (g zenon_TY_t)))); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 2.23/2.43 cut (((f (g zenon_TY_t)) = zenon_TY_t)); [idtac | apply NNPP; zenon_intro zenon_H5c]. % 2.23/2.43 congruence. % 2.23/2.43 cut (((f (g (f (g (f (g (f zenon_TX_d))))))) = zenon_TY_t) = ((f (g zenon_TY_t)) = zenon_TY_t)). % 2.23/2.43 intro zenon_D_pnotp. % 2.23/2.43 apply zenon_H5c. % 2.23/2.43 rewrite <- zenon_D_pnotp. % 2.23/2.43 exact zenon_H59. % 2.23/2.43 cut ((zenon_TY_t = zenon_TY_t)); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 2.23/2.43 cut (((f (g (f (g (f (g (f zenon_TX_d))))))) = (f (g zenon_TY_t)))); [idtac | apply NNPP; zenon_intro zenon_H5e]. % 2.23/2.44 congruence. % 2.23/2.44 elim (classic ((f (g zenon_TY_t)) = (f (g zenon_TY_t)))); [ zenon_intro zenon_H5a | zenon_intro zenon_H5b ]. % 2.23/2.44 cut (((f (g zenon_TY_t)) = (f (g zenon_TY_t))) = ((f (g (f (g (f (g (f zenon_TX_d))))))) = (f (g zenon_TY_t)))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H5e. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H5a. % 2.23/2.44 cut (((f (g zenon_TY_t)) = (f (g zenon_TY_t)))); [idtac | apply NNPP; zenon_intro zenon_H5b]. % 2.23/2.44 cut (((f (g zenon_TY_t)) = (f (g (f (g (f (g (f zenon_TX_d))))))))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((g zenon_TY_t) = (g (f (g (f (g (f zenon_TX_d)))))))); [idtac | apply NNPP; zenon_intro zenon_H60]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((g (f (g (f (g (f (g (f zenon_TX_d)))))))) = (g (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))) = ((g zenon_TY_t) = (g (f (g (f (g (f zenon_TX_d)))))))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H60. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H4b. % 2.23/2.44 cut (((g (f (g (f (g (f (g (f (g (f zenon_TX_d)))))))))) = (g (f (g (f (g (f zenon_TX_d)))))))); [idtac | apply NNPP; zenon_intro zenon_Hf]. % 2.23/2.44 cut (((g (f (g (f (g (f (g (f zenon_TX_d)))))))) = (g zenon_TY_t))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 2.23/2.44 congruence. % 2.23/2.44 elim (classic ((g zenon_TY_t) = (g zenon_TY_t))); [ zenon_intro zenon_H62 | zenon_intro zenon_H63 ]. % 2.23/2.44 cut (((g zenon_TY_t) = (g zenon_TY_t)) = ((g (f (g (f (g (f (g (f zenon_TX_d)))))))) = (g zenon_TY_t))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H61. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H62. % 2.23/2.44 cut (((g zenon_TY_t) = (g zenon_TY_t))); [idtac | apply NNPP; zenon_intro zenon_H63]. % 2.23/2.44 cut (((g zenon_TY_t) = (g (f (g (f (g (f (g (f zenon_TX_d)))))))))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 2.23/2.44 congruence. % 2.23/2.44 cut ((zenon_TY_t = (f (g (f (g (f (g (f zenon_TX_d))))))))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 2.23/2.44 congruence. % 2.23/2.44 apply zenon_H65. apply sym_equal. exact zenon_H59. % 2.23/2.44 apply zenon_H63. apply refl_equal. % 2.23/2.44 apply zenon_H63. apply refl_equal. % 2.23/2.44 apply (zenon_L5_ zenon_TX_d); trivial. % 2.23/2.44 apply zenon_H5b. apply refl_equal. % 2.23/2.44 apply zenon_H5b. apply refl_equal. % 2.23/2.44 apply zenon_H5d. apply refl_equal. % 2.23/2.44 apply zenon_H5b. apply refl_equal. % 2.23/2.44 apply zenon_H5b. apply refl_equal. % 2.23/2.44 generalize (zenon_H3d (g (f (g (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))))). zenon_intro zenon_H66. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H66); [ zenon_intro zenon_H6a; zenon_intro zenon_H69 | zenon_intro zenon_H68; zenon_intro zenon_H67 ]. % 2.23/2.44 cut (((f (g (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))))))); [idtac | apply NNPP; zenon_intro zenon_H6b]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((g (f (g (f (g (f (g (f (g (f zenon_TX_d)))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f zenon_TX_d)))))))))))))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 2.23/2.44 congruence. % 2.23/2.44 exact (zenon_H53 zenon_H51). % 2.23/2.44 elim (classic (zenon_TY_t = zenon_TY_t)); [ zenon_intro zenon_H6c | zenon_intro zenon_H5d ]. % 2.23/2.44 cut ((zenon_TY_t = zenon_TY_t) = ((f (g (f (g (f (g (f zenon_TX_d))))))) = zenon_TY_t)). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H58. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H6c. % 2.23/2.44 cut ((zenon_TY_t = zenon_TY_t)); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 2.23/2.44 cut ((zenon_TY_t = (f (g (f (g (f (g (f zenon_TX_d))))))))); [idtac | apply NNPP; zenon_intro zenon_H65]. % 2.23/2.44 congruence. % 2.23/2.44 cut ((zenon_TY_t = (f (g zenon_TY_t))) = (zenon_TY_t = (f (g (f (g (f (g (f zenon_TX_d))))))))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H65. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H12. % 2.23/2.44 cut (((f (g zenon_TY_t)) = (f (g (f (g (f (g (f zenon_TX_d))))))))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 2.23/2.44 cut ((zenon_TY_t = zenon_TY_t)); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 2.23/2.44 congruence. % 2.23/2.44 apply zenon_H5d. apply refl_equal. % 2.23/2.44 cut (((g zenon_TY_t) = (g (f (g (f (g (f zenon_TX_d)))))))); [idtac | apply NNPP; zenon_intro zenon_H60]. % 2.23/2.44 congruence. % 2.23/2.44 generalize (zenon_H3d (g zenon_TY_t)). zenon_intro zenon_H6d. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H6d); [ zenon_intro zenon_H11; zenon_intro zenon_H70 | zenon_intro zenon_H6f; zenon_intro zenon_H6e ]. % 2.23/2.44 apply (zenon_L6_ zenon_TY_t); trivial. % 2.23/2.44 cut ((zenon_TX_d = (g (f (g (f (g (f (g (f (g (f (g (f zenon_TX_d))))))))))))) = ((g zenon_TY_t) = (g (f (g (f (g (f zenon_TX_d)))))))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H60. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H67. % 2.23/2.44 cut (((g (f (g (f (g (f (g (f (g (f (g (f zenon_TX_d)))))))))))) = (g (f (g (f (g (f zenon_TX_d)))))))); [idtac | apply NNPP; zenon_intro zenon_H15]. % 2.23/2.44 cut ((zenon_TX_d = (g zenon_TY_t))); [idtac | apply NNPP; zenon_intro zenon_H70]. % 2.23/2.44 congruence. % 2.23/2.44 exact (zenon_H70 zenon_H6e). % 2.23/2.44 apply (zenon_L7_ zenon_TX_d); trivial. % 2.23/2.44 apply zenon_H5d. apply refl_equal. % 2.23/2.44 apply zenon_H5d. apply refl_equal. % 2.23/2.44 elim zenon_H3a. zenon_intro zenon_TX_bf. zenon_intro zenon_H71. % 2.23/2.44 generalize (zenon_H71 zenon_TX_bf). zenon_intro zenon_H72. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H72); [ zenon_intro zenon_H76; zenon_intro zenon_H75 | zenon_intro zenon_H74; zenon_intro zenon_H73 ]. % 2.23/2.44 apply zenon_H75. apply refl_equal. % 2.23/2.44 generalize (zenon_H71 (f (g zenon_TX_bf))). zenon_intro zenon_H77. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H77); [ zenon_intro zenon_H21; zenon_intro zenon_H76 | zenon_intro zenon_H1e; zenon_intro zenon_H74 ]. % 2.23/2.44 exact (zenon_H76 zenon_H74). % 2.23/2.44 generalize (zenon_H71 (f (g (f (g zenon_TX_bf))))). zenon_intro zenon_H78. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H78); [ zenon_intro zenon_H1d; zenon_intro zenon_H79 | zenon_intro zenon_H23; zenon_intro zenon_H26 ]. % 2.23/2.44 apply (zenon_L8_ zenon_TX_bf); trivial. % 2.23/2.44 generalize (zenon_H71 (f (g (f (g (f (g zenon_TX_bf))))))). zenon_intro zenon_H7a. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H7a); [ zenon_intro zenon_H22; zenon_intro zenon_H7c | zenon_intro zenon_H7b; zenon_intro zenon_H32 ]. % 2.23/2.44 apply (zenon_L9_ zenon_TX_bf); trivial. % 2.23/2.44 generalize (zenon_H71 (f (g (f (g (f (g (f (g zenon_TX_bf))))))))). zenon_intro zenon_H7d. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H7d); [ zenon_intro zenon_H81; zenon_intro zenon_H80 | zenon_intro zenon_H7f; zenon_intro zenon_H7e ]. % 2.23/2.44 cut (((g (f (g (f (g (f (g zenon_TX_bf))))))) = (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))); [idtac | apply NNPP; zenon_intro zenon_H82]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((f (g (f (g (f (g zenon_TX_bf)))))) = (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))); [idtac | apply NNPP; zenon_intro zenon_H22]. % 2.23/2.44 congruence. % 2.23/2.44 exact (zenon_H22 zenon_H7b). % 2.23/2.44 generalize (zenon_H71 (f (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))). zenon_intro zenon_H83. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H83); [ zenon_intro zenon_H87; zenon_intro zenon_H86 | zenon_intro zenon_H85; zenon_intro zenon_H84 ]. % 2.23/2.44 cut (((g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))) = (g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))))); [idtac | apply NNPP; zenon_intro zenon_H88]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((f (g (f (g (f (g (f (g zenon_TX_bf)))))))) = (f (g (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))))); [idtac | apply NNPP; zenon_intro zenon_H81]. % 2.23/2.44 congruence. % 2.23/2.44 exact (zenon_H81 zenon_H7f). % 2.23/2.44 apply zenon_H39. exists (g (f (g (f (g (f (g zenon_TX_bf))))))). apply NNPP. zenon_intro zenon_H89. % 2.23/2.44 apply (zenon_notallex_s (fun Y : zenon_U => ((Y = (g (f Y)))<->((g (f (g (f (g (f (g zenon_TX_bf))))))) = Y))) zenon_H89); [ zenon_intro zenon_H8a; idtac ]. % 2.23/2.44 elim zenon_H8a. zenon_intro zenon_TY_bv. zenon_intro zenon_H8b. % 2.23/2.44 apply (zenon_notequiv_s _ _ zenon_H8b); [ zenon_intro zenon_H30; zenon_intro zenon_H8d | zenon_intro zenon_H2e; zenon_intro zenon_H8c ]. % 2.23/2.44 elim (classic ((g (f zenon_TY_bv)) = (g (f zenon_TY_bv)))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 2.23/2.44 cut (((g (f zenon_TY_bv)) = (g (f zenon_TY_bv))) = (zenon_TY_bv = (g (f zenon_TY_bv)))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H30. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H8e. % 2.23/2.44 cut (((g (f zenon_TY_bv)) = (g (f zenon_TY_bv)))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 2.23/2.44 cut (((g (f zenon_TY_bv)) = zenon_TY_bv)); [idtac | apply NNPP; zenon_intro zenon_H90]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((g (f (g (f (g (f (g zenon_TX_bf))))))) = zenon_TY_bv) = ((g (f zenon_TY_bv)) = zenon_TY_bv)). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H90. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H8d. % 2.23/2.44 cut ((zenon_TY_bv = zenon_TY_bv)); [idtac | apply NNPP; zenon_intro zenon_H91]. % 2.23/2.44 cut (((g (f (g (f (g (f (g zenon_TX_bf))))))) = (g (f zenon_TY_bv)))); [idtac | apply NNPP; zenon_intro zenon_H92]. % 2.23/2.44 congruence. % 2.23/2.44 elim (classic ((g (f zenon_TY_bv)) = (g (f zenon_TY_bv)))); [ zenon_intro zenon_H8e | zenon_intro zenon_H8f ]. % 2.23/2.44 cut (((g (f zenon_TY_bv)) = (g (f zenon_TY_bv))) = ((g (f (g (f (g (f (g zenon_TX_bf))))))) = (g (f zenon_TY_bv)))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H92. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H8e. % 2.23/2.44 cut (((g (f zenon_TY_bv)) = (g (f zenon_TY_bv)))); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 2.23/2.44 cut (((g (f zenon_TY_bv)) = (g (f (g (f (g (f (g zenon_TX_bf))))))))); [idtac | apply NNPP; zenon_intro zenon_H93]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((f zenon_TY_bv) = (f (g (f (g (f (g zenon_TX_bf)))))))); [idtac | apply NNPP; zenon_intro zenon_H94]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((f (g (f (g (f (g (f (g zenon_TX_bf)))))))) = (f (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))) = ((f zenon_TY_bv) = (f (g (f (g (f (g zenon_TX_bf)))))))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H94. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H7f. % 2.23/2.44 cut (((f (g (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))) = (f (g (f (g (f (g zenon_TX_bf)))))))); [idtac | apply NNPP; zenon_intro zenon_H2b]. % 2.23/2.44 cut (((f (g (f (g (f (g (f (g zenon_TX_bf)))))))) = (f zenon_TY_bv))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 2.23/2.44 congruence. % 2.23/2.44 elim (classic ((f zenon_TY_bv) = (f zenon_TY_bv))); [ zenon_intro zenon_H96 | zenon_intro zenon_H97 ]. % 2.23/2.44 cut (((f zenon_TY_bv) = (f zenon_TY_bv)) = ((f (g (f (g (f (g (f (g zenon_TX_bf)))))))) = (f zenon_TY_bv))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H95. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H96. % 2.23/2.44 cut (((f zenon_TY_bv) = (f zenon_TY_bv))); [idtac | apply NNPP; zenon_intro zenon_H97]. % 2.23/2.44 cut (((f zenon_TY_bv) = (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))); [idtac | apply NNPP; zenon_intro zenon_H98]. % 2.23/2.44 congruence. % 2.23/2.44 cut ((zenon_TY_bv = (g (f (g (f (g (f (g zenon_TX_bf))))))))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 2.23/2.44 congruence. % 2.23/2.44 apply zenon_H99. apply sym_equal. exact zenon_H8d. % 2.23/2.44 apply zenon_H97. apply refl_equal. % 2.23/2.44 apply zenon_H97. apply refl_equal. % 2.23/2.44 apply (zenon_L12_ zenon_TX_bf); trivial. % 2.23/2.44 apply zenon_H8f. apply refl_equal. % 2.23/2.44 apply zenon_H8f. apply refl_equal. % 2.23/2.44 apply zenon_H91. apply refl_equal. % 2.23/2.44 apply zenon_H8f. apply refl_equal. % 2.23/2.44 apply zenon_H8f. apply refl_equal. % 2.23/2.44 generalize (zenon_H71 (f (g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))))). zenon_intro zenon_H9a. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_H9a); [ zenon_intro zenon_H9e; zenon_intro zenon_H9d | zenon_intro zenon_H9c; zenon_intro zenon_H9b ]. % 2.23/2.44 cut (((g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))) = (g (f (g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))))))); [idtac | apply NNPP; zenon_intro zenon_H9f]. % 2.23/2.44 congruence. % 2.23/2.44 cut (((f (g (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))) = (f (g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))))))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 2.23/2.44 congruence. % 2.23/2.44 exact (zenon_H87 zenon_H85). % 2.23/2.44 elim (classic (zenon_TY_bv = zenon_TY_bv)); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H91 ]. % 2.23/2.44 cut ((zenon_TY_bv = zenon_TY_bv) = ((g (f (g (f (g (f (g zenon_TX_bf))))))) = zenon_TY_bv)). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H8c. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_Ha0. % 2.23/2.44 cut ((zenon_TY_bv = zenon_TY_bv)); [idtac | apply NNPP; zenon_intro zenon_H91]. % 2.23/2.44 cut ((zenon_TY_bv = (g (f (g (f (g (f (g zenon_TX_bf))))))))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 2.23/2.44 congruence. % 2.23/2.44 cut ((zenon_TY_bv = (g (f zenon_TY_bv))) = (zenon_TY_bv = (g (f (g (f (g (f (g zenon_TX_bf))))))))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H99. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H2e. % 2.23/2.44 cut (((g (f zenon_TY_bv)) = (g (f (g (f (g (f (g zenon_TX_bf))))))))); [idtac | apply NNPP; zenon_intro zenon_H93]. % 2.23/2.44 cut ((zenon_TY_bv = zenon_TY_bv)); [idtac | apply NNPP; zenon_intro zenon_H91]. % 2.23/2.44 congruence. % 2.23/2.44 apply zenon_H91. apply refl_equal. % 2.23/2.44 cut (((f zenon_TY_bv) = (f (g (f (g (f (g zenon_TX_bf)))))))); [idtac | apply NNPP; zenon_intro zenon_H94]. % 2.23/2.44 congruence. % 2.23/2.44 generalize (zenon_H71 (f zenon_TY_bv)). zenon_intro zenon_Ha1. % 2.23/2.44 apply (zenon_equiv_s _ _ zenon_Ha1); [ zenon_intro zenon_H2d; zenon_intro zenon_Ha4 | zenon_intro zenon_Ha3; zenon_intro zenon_Ha2 ]. % 2.23/2.44 apply (zenon_L13_ zenon_TY_bv); trivial. % 2.23/2.44 cut ((zenon_TX_bf = (f (g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf))))))))))))) = ((f zenon_TY_bv) = (f (g (f (g (f (g zenon_TX_bf)))))))). % 2.23/2.44 intro zenon_D_pnotp. % 2.23/2.44 apply zenon_H94. % 2.23/2.44 rewrite <- zenon_D_pnotp. % 2.23/2.44 exact zenon_H9b. % 2.23/2.44 cut (((f (g (f (g (f (g (f (g (f (g (f (g zenon_TX_bf)))))))))))) = (f (g (f (g (f (g zenon_TX_bf)))))))); [idtac | apply NNPP; zenon_intro zenon_H31]. % 2.23/2.44 cut ((zenon_TX_bf = (f zenon_TY_bv))); [idtac | apply NNPP; zenon_intro zenon_Ha4]. % 2.23/2.44 congruence. % 2.23/2.44 exact (zenon_Ha4 zenon_Ha2). % 2.23/2.44 apply (zenon_L14_ zenon_TX_bf); trivial. % 2.23/2.44 apply zenon_H91. apply refl_equal. % 2.23/2.44 apply zenon_H91. apply refl_equal. % 2.23/2.44 Qed. % 2.23/2.44 % SZS output end Proof % 2.23/2.44 (* END-PROOF *) % 2.23/2.44 nodes searched: 50903 % 2.23/2.44 max branch formulas: 631 % 2.23/2.44 proof nodes created: 1149 % 2.23/2.44 formulas created: 56014 % 2.23/2.44 %------------------------------------------------------------------------------