%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:32:35 PM UTC 2026 % Result : Theorem 0.33s 0.63s % Output : Proof 0.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.09/0.35 % Computer : n008.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 5 20:00:23 UTC 2026 % 0.09/0.36 % CPUTime : % 0.33/0.63 (* PROOF-FOUND *) % 0.33/0.63 % SZS status Theorem % 0.33/0.63 (* BEGIN-PROOF *) % 0.33/0.63 % SZS output start Proof % 0.33/0.63 Theorem main : (~(exists X : zenon_U, (~((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((~(p8 X))/\((~(p6 X))/\((~(p4 X))/\(~(p2 X)))))))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p5 Y)))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((p4 X)/\((p3 X)/\((p2 X)/\(p1 X)))))))))))))))))). % 0.33/0.63 Proof. % 0.33/0.63 assert (zenon_L1_ : forall (zenon_TX_e : zenon_U), (~(~(p3 zenon_TX_e))) -> (p2 zenon_TX_e) -> (~((p3 zenon_TX_e)/\(p2 zenon_TX_e))) -> False). % 0.33/0.63 do 1 intro. intros zenon_H1 zenon_H2 zenon_H3. % 0.33/0.63 apply zenon_H1. zenon_intro zenon_H5. % 0.33/0.63 apply (zenon_notand_s _ _ zenon_H3); [ zenon_intro zenon_H7 | zenon_intro zenon_H6 ]. % 0.33/0.63 exact (zenon_H7 zenon_H5). % 0.33/0.63 exact (zenon_H6 zenon_H2). % 0.33/0.63 (* end of lemma zenon_L1_ *) % 0.33/0.63 assert (zenon_L2_ : forall (zenon_TX_e : zenon_U), (~(~(p1 zenon_TX_e))) -> (~(p1 zenon_TX_e)) -> False). % 0.33/0.63 do 1 intro. intros zenon_H8 zenon_H9. % 0.33/0.63 exact (zenon_H8 zenon_H9). % 0.33/0.63 (* end of lemma zenon_L2_ *) % 0.33/0.63 assert (zenon_L3_ : forall (zenon_TX_e : zenon_U), (~(((~(p3 zenon_TX_e))/\(~(p1 zenon_TX_e)))\/((p1 zenon_TX_e)/\(p3 zenon_TX_e)))) -> (p2 zenon_TX_e) -> (~((p3 zenon_TX_e)/\(p2 zenon_TX_e))) -> (~(p1 zenon_TX_e)) -> False). % 0.33/0.63 do 1 intro. intros zenon_Ha zenon_H2 zenon_H3 zenon_H9. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_Ha). zenon_intro zenon_Hc. zenon_intro zenon_Hb. % 0.33/0.63 apply (zenon_notand_s _ _ zenon_Hc); [ zenon_intro zenon_H1 | zenon_intro zenon_H8 ]. % 0.33/0.63 apply (zenon_L1_ zenon_TX_e); trivial. % 0.33/0.63 exact (zenon_H8 zenon_H9). % 0.33/0.63 (* end of lemma zenon_L3_ *) % 0.33/0.63 assert (zenon_L4_ : forall (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TY_p X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))) -> (r1 zenon_TY_p zenon_TX_e) -> (p2 zenon_TX_e) -> (~((p3 zenon_TX_e)/\(p2 zenon_TX_e))) -> (~(p1 zenon_TX_e)) -> False). % 0.33/0.63 do 2 intro. intros zenon_Hd zenon_He zenon_H2 zenon_H3 zenon_H9. % 0.33/0.63 generalize (zenon_Hd zenon_TX_e). zenon_intro zenon_H10. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H10); [ zenon_intro zenon_H11 | zenon_intro zenon_Ha ]. % 0.33/0.63 exact (zenon_H11 zenon_He). % 0.33/0.63 apply (zenon_L3_ zenon_TX_e); trivial. % 0.33/0.63 (* end of lemma zenon_L4_ *) % 0.33/0.63 assert (zenon_L5_ : forall (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U) (zenon_TX_u : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))) -> (r1 zenon_TX_u zenon_TY_p) -> (r1 zenon_TY_p zenon_TX_e) -> (p2 zenon_TX_e) -> (~((p3 zenon_TX_e)/\(p2 zenon_TX_e))) -> (~(p1 zenon_TX_e)) -> False). % 0.33/0.63 do 3 intro. intros zenon_H12 zenon_H13 zenon_He zenon_H2 zenon_H3 zenon_H9. % 0.33/0.63 generalize (zenon_H12 zenon_TY_p). zenon_intro zenon_H15. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H15); [ zenon_intro zenon_H16 | zenon_intro zenon_Hd ]. % 0.33/0.63 exact (zenon_H16 zenon_H13). % 0.33/0.63 apply (zenon_L4_ zenon_TX_e zenon_TY_p); trivial. % 0.33/0.63 (* end of lemma zenon_L5_ *) % 0.33/0.63 assert (zenon_L6_ : forall (zenon_TX_u : zenon_U) (zenon_TY_p : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TX_bc : zenon_U) (zenon_TX_e : zenon_U), (~(((~(p1 zenon_TX_e))/\(~(p2 zenon_TX_e)))\/((p2 zenon_TX_e)/\(p1 zenon_TX_e)))) -> (p2 zenon_TX_e) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (r1 zenon_TX_bc zenon_TY_bb) -> (~((p3 zenon_TX_e)/\(p2 zenon_TX_e))) -> (r1 zenon_TY_p zenon_TX_e) -> (r1 zenon_TX_u zenon_TY_p) -> (r1 zenon_TY_bb zenon_TX_u) -> False). % 0.33/0.63 do 5 intro. intros zenon_H17 zenon_H2 zenon_H18 zenon_H19 zenon_H3 zenon_He zenon_H13 zenon_H1a. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H17). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 0.33/0.63 apply (zenon_notand_s _ _ zenon_H1d); [ zenon_intro zenon_H6 | zenon_intro zenon_H9 ]. % 0.33/0.63 exact (zenon_H6 zenon_H2). % 0.33/0.63 generalize (zenon_H18 zenon_TY_bb). zenon_intro zenon_H1f. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H1f); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 0.33/0.63 exact (zenon_H21 zenon_H19). % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 0.33/0.63 apply zenon_H23. zenon_intro zenon_H24. % 0.33/0.63 generalize (zenon_H24 zenon_TX_u). zenon_intro zenon_H25. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H25); [ zenon_intro zenon_H26 | zenon_intro zenon_H12 ]. % 0.33/0.63 exact (zenon_H26 zenon_H1a). % 0.33/0.63 apply (zenon_L5_ zenon_TX_e zenon_TY_p zenon_TX_u); trivial. % 0.33/0.63 (* end of lemma zenon_L6_ *) % 0.33/0.63 assert (zenon_L7_ : forall (zenon_TX_bc : zenon_U) (zenon_TX_e : zenon_U) (zenon_TX_u : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TY_p : zenon_U), (~(~(forall X : zenon_U, ((~(r1 zenon_TY_p X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))) -> (r1 zenon_TY_bb zenon_TX_u) -> (r1 zenon_TX_u zenon_TY_p) -> (~((p3 zenon_TX_e)/\(p2 zenon_TX_e))) -> (r1 zenon_TX_bc zenon_TY_bb) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (p2 zenon_TX_e) -> (r1 zenon_TY_p zenon_TX_e) -> False). % 0.33/0.63 do 5 intro. intros zenon_H27 zenon_H1a zenon_H13 zenon_H3 zenon_H19 zenon_H18 zenon_H2 zenon_He. % 0.33/0.63 apply zenon_H27. zenon_intro zenon_H28. % 0.33/0.63 generalize (zenon_H28 zenon_TX_e). zenon_intro zenon_H29. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H29); [ zenon_intro zenon_H11 | zenon_intro zenon_H17 ]. % 0.33/0.63 exact (zenon_H11 zenon_He). % 0.33/0.63 apply (zenon_L6_ zenon_TX_u zenon_TY_p zenon_TY_bb zenon_TX_bc zenon_TX_e); trivial. % 0.33/0.63 (* end of lemma zenon_L7_ *) % 0.33/0.63 assert (zenon_L8_ : forall (zenon_TX_bc : zenon_U) (zenon_TX_e : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TY_p : zenon_U) (zenon_TX_u : zenon_U), (~((~(forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))) -> (r1 zenon_TX_u zenon_TY_p) -> (r1 zenon_TY_bb zenon_TX_u) -> (~((p3 zenon_TX_e)/\(p2 zenon_TX_e))) -> (r1 zenon_TX_bc zenon_TY_bb) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (p2 zenon_TX_e) -> (r1 zenon_TY_p zenon_TX_e) -> False). % 0.33/0.63 do 5 intro. intros zenon_H2a zenon_H13 zenon_H1a zenon_H3 zenon_H19 zenon_H18 zenon_H2 zenon_He. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H2a). zenon_intro zenon_H2c. zenon_intro zenon_H2b. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H2b). zenon_intro zenon_H2e. zenon_intro zenon_H2d. % 0.33/0.63 apply zenon_H2d. zenon_intro zenon_H2f. % 0.33/0.63 generalize (zenon_H2f zenon_TY_p). zenon_intro zenon_H30. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H30); [ zenon_intro zenon_H16 | zenon_intro zenon_H27 ]. % 0.33/0.63 exact (zenon_H16 zenon_H13). % 0.33/0.63 apply (zenon_L7_ zenon_TX_bc zenon_TX_e zenon_TX_u zenon_TY_bb zenon_TY_p); trivial. % 0.33/0.63 (* end of lemma zenon_L8_ *) % 0.33/0.63 assert (zenon_L9_ : forall (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U) (zenon_TX_u : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TX_bc : zenon_U), (r1 zenon_TX_bc zenon_TY_bb) -> (r1 zenon_TX_u zenon_TY_p) -> (~((p3 zenon_TX_e)/\(p2 zenon_TX_e))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (p2 zenon_TX_e) -> (r1 zenon_TY_p zenon_TX_e) -> (r1 zenon_TY_bb zenon_TX_u) -> False). % 0.33/0.63 do 5 intro. intros zenon_H19 zenon_H13 zenon_H3 zenon_H18 zenon_H2 zenon_He zenon_H1a. % 0.33/0.63 generalize (zenon_H18 zenon_TY_bb). zenon_intro zenon_H1f. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H1f); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 0.33/0.63 exact (zenon_H21 zenon_H19). % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H22). zenon_intro zenon_H32. zenon_intro zenon_H31. % 0.33/0.63 apply zenon_H31. zenon_intro zenon_H33. % 0.33/0.63 generalize (zenon_H33 zenon_TX_u). zenon_intro zenon_H34. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H34); [ zenon_intro zenon_H26 | zenon_intro zenon_H2a ]. % 0.33/0.63 exact (zenon_H26 zenon_H1a). % 0.33/0.63 apply (zenon_L8_ zenon_TX_bc zenon_TX_e zenon_TY_bb zenon_TY_p zenon_TX_u); trivial. % 0.33/0.63 (* end of lemma zenon_L9_ *) % 0.33/0.63 assert (zenon_L10_ : forall (zenon_TX_e : zenon_U), (~(~(p2 zenon_TX_e))) -> (~(p2 zenon_TX_e)) -> False). % 0.33/0.63 do 1 intro. intros zenon_H35 zenon_H6. % 0.33/0.63 exact (zenon_H35 zenon_H6). % 0.33/0.63 (* end of lemma zenon_L10_ *) % 0.33/0.63 assert (zenon_L11_ : forall (zenon_TX_e : zenon_U), (~(((~(p1 zenon_TX_e))/\(~(p2 zenon_TX_e)))\/((p2 zenon_TX_e)/\(p1 zenon_TX_e)))) -> (~(p1 zenon_TX_e)) -> (~(p2 zenon_TX_e)) -> False). % 0.33/0.63 do 1 intro. intros zenon_H17 zenon_H9 zenon_H6. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H17). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 0.33/0.63 apply (zenon_notand_s _ _ zenon_H1e); [ zenon_intro zenon_H8 | zenon_intro zenon_H35 ]. % 0.33/0.63 exact (zenon_H8 zenon_H9). % 0.33/0.63 exact (zenon_H35 zenon_H6). % 0.33/0.63 (* end of lemma zenon_L11_ *) % 0.33/0.63 assert (zenon_L12_ : forall (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U), (~(~(forall X : zenon_U, ((~(r1 zenon_TY_p X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))) -> (~(p2 zenon_TX_e)) -> (~(p1 zenon_TX_e)) -> (r1 zenon_TY_p zenon_TX_e) -> False). % 0.33/0.63 do 2 intro. intros zenon_H27 zenon_H6 zenon_H9 zenon_He. % 0.33/0.63 apply zenon_H27. zenon_intro zenon_H28. % 0.33/0.63 generalize (zenon_H28 zenon_TX_e). zenon_intro zenon_H29. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H29); [ zenon_intro zenon_H11 | zenon_intro zenon_H17 ]. % 0.33/0.63 exact (zenon_H11 zenon_He). % 0.33/0.63 apply (zenon_L11_ zenon_TX_e); trivial. % 0.33/0.63 (* end of lemma zenon_L12_ *) % 0.33/0.63 assert (zenon_L13_ : forall (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U) (zenon_TX_u : zenon_U), (~((~(forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))) -> (r1 zenon_TX_u zenon_TY_p) -> (~(p2 zenon_TX_e)) -> (~(p1 zenon_TX_e)) -> (r1 zenon_TY_p zenon_TX_e) -> False). % 0.33/0.63 do 3 intro. intros zenon_H2a zenon_H13 zenon_H6 zenon_H9 zenon_He. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H2a). zenon_intro zenon_H2c. zenon_intro zenon_H2b. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H2b). zenon_intro zenon_H2e. zenon_intro zenon_H2d. % 0.33/0.63 apply zenon_H2d. zenon_intro zenon_H2f. % 0.33/0.63 generalize (zenon_H2f zenon_TY_p). zenon_intro zenon_H30. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H30); [ zenon_intro zenon_H16 | zenon_intro zenon_H27 ]. % 0.33/0.63 exact (zenon_H16 zenon_H13). % 0.33/0.63 apply (zenon_L12_ zenon_TX_e zenon_TY_p); trivial. % 0.33/0.63 (* end of lemma zenon_L13_ *) % 0.33/0.63 assert (zenon_L14_ : forall (zenon_TY_p : zenon_U) (zenon_TX_u : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TX_bc : zenon_U) (zenon_TX_e : zenon_U), (~(((~(p3 zenon_TX_e))/\(~(p1 zenon_TX_e)))\/((p1 zenon_TX_e)/\(p3 zenon_TX_e)))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (r1 zenon_TX_bc zenon_TY_bb) -> (r1 zenon_TX_u zenon_TY_p) -> (~(p2 zenon_TX_e)) -> (r1 zenon_TY_p zenon_TX_e) -> (r1 zenon_TY_bb zenon_TX_u) -> (p3 zenon_TX_e) -> False). % 0.33/0.63 do 5 intro. intros zenon_Ha zenon_H18 zenon_H19 zenon_H13 zenon_H6 zenon_He zenon_H1a zenon_H5. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_Ha). zenon_intro zenon_Hc. zenon_intro zenon_Hb. % 0.33/0.63 apply (zenon_notand_s _ _ zenon_Hb); [ zenon_intro zenon_H9 | zenon_intro zenon_H7 ]. % 0.33/0.63 generalize (zenon_H18 zenon_TY_bb). zenon_intro zenon_H1f. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H1f); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 0.33/0.63 exact (zenon_H21 zenon_H19). % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H22). zenon_intro zenon_H32. zenon_intro zenon_H31. % 0.33/0.63 apply zenon_H31. zenon_intro zenon_H33. % 0.33/0.63 generalize (zenon_H33 zenon_TX_u). zenon_intro zenon_H34. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H34); [ zenon_intro zenon_H26 | zenon_intro zenon_H2a ]. % 0.33/0.63 exact (zenon_H26 zenon_H1a). % 0.33/0.63 apply (zenon_L13_ zenon_TX_e zenon_TY_p zenon_TX_u); trivial. % 0.33/0.63 exact (zenon_H7 zenon_H5). % 0.33/0.63 (* end of lemma zenon_L14_ *) % 0.33/0.63 assert (zenon_L15_ : forall (zenon_TX_u : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TX_bc : zenon_U) (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TY_p X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))) -> (r1 zenon_TY_p zenon_TX_e) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (r1 zenon_TX_bc zenon_TY_bb) -> (r1 zenon_TX_u zenon_TY_p) -> (~(p2 zenon_TX_e)) -> (r1 zenon_TY_bb zenon_TX_u) -> (p3 zenon_TX_e) -> False). % 0.33/0.63 do 5 intro. intros zenon_Hd zenon_He zenon_H18 zenon_H19 zenon_H13 zenon_H6 zenon_H1a zenon_H5. % 0.33/0.63 generalize (zenon_Hd zenon_TX_e). zenon_intro zenon_H10. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H10); [ zenon_intro zenon_H11 | zenon_intro zenon_Ha ]. % 0.33/0.63 exact (zenon_H11 zenon_He). % 0.33/0.63 apply (zenon_L14_ zenon_TY_p zenon_TX_u zenon_TY_bb zenon_TX_bc zenon_TX_e); trivial. % 0.33/0.63 (* end of lemma zenon_L15_ *) % 0.33/0.63 assert (zenon_L16_ : forall (zenon_TY_bb : zenon_U) (zenon_TX_bc : zenon_U) (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U) (zenon_TX_u : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))) -> (r1 zenon_TX_u zenon_TY_p) -> (r1 zenon_TY_p zenon_TX_e) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (r1 zenon_TX_bc zenon_TY_bb) -> (~(p2 zenon_TX_e)) -> (r1 zenon_TY_bb zenon_TX_u) -> (p3 zenon_TX_e) -> False). % 0.33/0.63 do 5 intro. intros zenon_H12 zenon_H13 zenon_He zenon_H18 zenon_H19 zenon_H6 zenon_H1a zenon_H5. % 0.33/0.63 generalize (zenon_H12 zenon_TY_p). zenon_intro zenon_H15. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H15); [ zenon_intro zenon_H16 | zenon_intro zenon_Hd ]. % 0.33/0.63 exact (zenon_H16 zenon_H13). % 0.33/0.63 apply (zenon_L15_ zenon_TX_u zenon_TY_bb zenon_TX_bc zenon_TX_e zenon_TY_p); trivial. % 0.33/0.63 (* end of lemma zenon_L16_ *) % 0.33/0.63 assert (zenon_L17_ : forall (zenon_TX_bc : zenon_U) (zenon_TY_p : zenon_U) (zenon_TX_u : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TX_e : zenon_U), (~(((~(p2 zenon_TX_e))/\(~(p3 zenon_TX_e)))\/((p3 zenon_TX_e)/\(p2 zenon_TX_e)))) -> (r1 zenon_TY_bb zenon_TX_u) -> (r1 zenon_TY_p zenon_TX_e) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (r1 zenon_TX_u zenon_TY_p) -> (r1 zenon_TX_bc zenon_TY_bb) -> False). % 0.33/0.63 do 5 intro. intros zenon_H36 zenon_H1a zenon_He zenon_H18 zenon_H13 zenon_H19. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H36). zenon_intro zenon_H37. zenon_intro zenon_H3. % 0.33/0.63 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H35 | zenon_intro zenon_H1 ]. % 0.33/0.63 apply zenon_H35. zenon_intro zenon_H2. % 0.33/0.63 apply (zenon_L9_ zenon_TX_e zenon_TY_p zenon_TX_u zenon_TY_bb zenon_TX_bc); trivial. % 0.33/0.63 apply zenon_H1. zenon_intro zenon_H5. % 0.33/0.63 apply (zenon_notand_s _ _ zenon_H3); [ zenon_intro zenon_H7 | zenon_intro zenon_H6 ]. % 0.33/0.63 exact (zenon_H7 zenon_H5). % 0.33/0.63 generalize (zenon_H18 zenon_TY_bb). zenon_intro zenon_H1f. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H1f); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 0.33/0.63 exact (zenon_H21 zenon_H19). % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 0.33/0.63 apply zenon_H23. zenon_intro zenon_H24. % 0.33/0.63 generalize (zenon_H24 zenon_TX_u). zenon_intro zenon_H25. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H25); [ zenon_intro zenon_H26 | zenon_intro zenon_H12 ]. % 0.33/0.63 exact (zenon_H26 zenon_H1a). % 0.33/0.63 apply (zenon_L16_ zenon_TY_bb zenon_TX_bc zenon_TX_e zenon_TY_p zenon_TX_u); trivial. % 0.33/0.63 (* end of lemma zenon_L17_ *) % 0.33/0.63 assert (zenon_L18_ : forall (zenon_TX_bc : zenon_U) (zenon_TX_u : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TY_p X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))) -> (r1 zenon_TY_p zenon_TX_e) -> (r1 zenon_TY_bb zenon_TX_u) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (r1 zenon_TX_u zenon_TY_p) -> (r1 zenon_TX_bc zenon_TY_bb) -> False). % 0.33/0.63 do 5 intro. intros zenon_H38 zenon_He zenon_H1a zenon_H18 zenon_H13 zenon_H19. % 0.33/0.63 generalize (zenon_H38 zenon_TX_e). zenon_intro zenon_H39. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H39); [ zenon_intro zenon_H11 | zenon_intro zenon_H36 ]. % 0.33/0.63 exact (zenon_H11 zenon_He). % 0.33/0.63 apply (zenon_L17_ zenon_TX_bc zenon_TY_p zenon_TX_u zenon_TY_bb zenon_TX_e); trivial. % 0.33/0.63 (* end of lemma zenon_L18_ *) % 0.33/0.63 assert (zenon_L19_ : forall (zenon_TX_bc : zenon_U) (zenon_TY_bb : zenon_U) (zenon_TX_e : zenon_U) (zenon_TY_p : zenon_U) (zenon_TX_u : zenon_U), (~((~(forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 zenon_TX_u Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))) -> (r1 zenon_TX_u zenon_TY_p) -> (r1 zenon_TY_p zenon_TX_e) -> (r1 zenon_TY_bb zenon_TX_u) -> (forall Y : zenon_U, ((~(r1 zenon_TX_bc Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p3 X))/\(~(p1 X)))\/((p1 X)/\(p3 X)))))))))))\/((forall X : zenon_U, ((~(r1 Y X))\/(p4 X)))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p2 X))/\(~(p3 X)))\/((p3 X)/\(p2 X)))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((~(p1 X))/\(~(p2 X)))\/((p2 X)/\(p1 X)))))))))))))))))))))) -> (r1 zenon_TX_bc zenon_TY_bb) -> False). % 0.33/0.63 do 5 intro. intros zenon_H2a zenon_H13 zenon_He zenon_H1a zenon_H18 zenon_H19. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H2a). zenon_intro zenon_H2c. zenon_intro zenon_H2b. % 0.33/0.63 apply zenon_H2c. zenon_intro zenon_H3a. % 0.33/0.63 generalize (zenon_H3a zenon_TY_p). zenon_intro zenon_H3b. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H3b); [ zenon_intro zenon_H16 | zenon_intro zenon_H38 ]. % 0.33/0.63 exact (zenon_H16 zenon_H13). % 0.33/0.63 apply (zenon_L18_ zenon_TX_bc zenon_TX_u zenon_TY_bb zenon_TX_e zenon_TY_p); trivial. % 0.33/0.63 (* end of lemma zenon_L19_ *) % 0.33/0.63 apply NNPP. intro zenon_G. % 0.33/0.63 apply zenon_G. zenon_intro zenon_H3c. % 0.33/0.63 elim zenon_H3c. zenon_intro zenon_TX_bc. zenon_intro zenon_H3d. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H3d). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 0.33/0.63 apply zenon_H43. zenon_intro zenon_H18. % 0.33/0.63 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_bc Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((~(p8 X))/\((~(p6 X))/\((~(p4 X))/\(~(p2 X))))))))))))) zenon_H3f); [ zenon_intro zenon_H44; idtac ]. % 0.33/0.63 elim zenon_H44. zenon_intro zenon_TY_bb. zenon_intro zenon_H45. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H45). zenon_intro zenon_H47. zenon_intro zenon_H46. % 0.33/0.63 apply zenon_H47. zenon_intro zenon_H19. % 0.33/0.63 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TY_bb X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((~(p8 X))/\((~(p6 X))/\((~(p4 X))/\(~(p2 X))))))))))) zenon_H46); [ zenon_intro zenon_H48; idtac ]. % 0.33/0.63 elim zenon_H48. zenon_intro zenon_TX_u. zenon_intro zenon_H49. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H49). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.33/0.63 apply zenon_H4b. zenon_intro zenon_H1a. % 0.33/0.63 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_u Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((~(p8 X))/\((~(p6 X))/\((~(p4 X))/\(~(p2 X))))))))) zenon_H4a); [ zenon_intro zenon_H4c; idtac ]. % 0.33/0.63 elim zenon_H4c. zenon_intro zenon_TY_p. zenon_intro zenon_H4d. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H4d). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 0.33/0.63 apply zenon_H4f. zenon_intro zenon_H13. % 0.33/0.63 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TY_p X))\/((~(p8 X))/\((~(p6 X))/\((~(p4 X))/\(~(p2 X))))))) zenon_H4e); [ zenon_intro zenon_H50; idtac ]. % 0.33/0.63 elim zenon_H50. zenon_intro zenon_TX_e. zenon_intro zenon_H51. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H52. % 0.33/0.63 apply zenon_H53. zenon_intro zenon_He. % 0.33/0.63 generalize (zenon_H18 zenon_TY_bb). zenon_intro zenon_H1f. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H1f); [ zenon_intro zenon_H21 | zenon_intro zenon_H20 ]. % 0.33/0.63 exact (zenon_H21 zenon_H19). % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 0.33/0.63 apply (zenon_notor_s _ _ zenon_H22). zenon_intro zenon_H32. zenon_intro zenon_H31. % 0.33/0.63 apply zenon_H31. zenon_intro zenon_H33. % 0.33/0.63 generalize (zenon_H33 zenon_TX_u). zenon_intro zenon_H34. % 0.33/0.63 apply (zenon_or_s _ _ zenon_H34); [ zenon_intro zenon_H26 | zenon_intro zenon_H2a ]. % 0.33/0.63 exact (zenon_H26 zenon_H1a). % 0.33/0.63 apply (zenon_L19_ zenon_TX_bc zenon_TY_bb zenon_TX_e zenon_TY_p zenon_TX_u); trivial. % 0.33/0.63 Qed. % 0.33/0.63 % SZS output end Proof % 0.33/0.63 (* END-PROOF *) % 0.33/0.63 nodes searched: 8005 % 0.33/0.63 max branch formulas: 760 % 0.33/0.63 proof nodes created: 769 % 0.33/0.63 formulas created: 19590 % 0.33/0.63 %------------------------------------------------------------------------------