%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL682+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n005.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:48 PM UTC 2026 % Result : Theorem 22.93s 23.21s % Output : Proof 22.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL682+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.36 % Computer : n005.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 5 13:46:05 UTC 2026 % 0.13/0.36 % CPUTime : % 22.93/23.21 (* PROOF-FOUND *) % 22.93/23.21 % SZS status Theorem % 22.93/23.21 (* BEGIN-PROOF *) % 22.93/23.21 % SZS output start Proof % 22.93/23.21 Theorem main : (~(exists X : zenon_U, (~((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(p56 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(p52 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p56 Y)))/\(~(p46 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p56 Y)))/\(~(p44 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p56 Y)))/\(~(p42 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p54 Y)))/\(~(p46 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p54 Y)))/\(~(p44 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p54 Y)))/\(~(p42 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p52 Y)))/\(~(p46 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p52 Y)))/\(~(p44 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p52 Y)))/\(~(p42 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))\/(p46 X)))/\(~(p36 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))\/(p46 X)))/\(~(p32 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p55 Y)))/\(~(p45 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p53 Y)))/\(~(p45 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p51 Y)))/\(~(p45 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))\/(p44 X)))/\(~(p36 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))\/(p44 X)))/\(~(p32 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p55 Y)))/\(~(p43 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p53 Y)))/\(~(p43 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p51 Y)))/\(~(p43 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))\/(p42 X)))/\(~(p36 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))\/(p42 X)))/\(~(p32 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p55 Y)))/\(~(p41 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p54 Y)))/\(~(p41 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p53 Y)))/\(~(p41 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))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p51 Y)))/\(~(p41 X)))))))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p36 Y)))/\(~(p26 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p36 Y)))/\(~(p24 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p36 Y)))/\(~(p22 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))\/(p45 X)))/\(~(p35 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))\/(p43 X)))/\(~(p35 Y)))))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p34 Y)))/\(~(p26 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p34 Y)))/\(~(p24 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p34 Y)))/\(~(p22 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))\/(p41 X)))/\(~(p34 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))\/(p45 X)))/\(~(p33 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))\/(p43 X)))/\(~(p33 Y)))))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p32 Y)))/\(~(p26 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p32 Y)))/\(~(p24 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p32 Y)))/\(~(p22 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))\/(p45 X)))/\(~(p31 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))\/(p43 X)))/\(~(p31 Y)))))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p26 X)))/\(~(p16 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p26 X)))/\(~(p14 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p35 Y)))/\(~(p25 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p33 Y)))/\(~(p25 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p31 Y)))/\(~(p25 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p24 X)))/\(~(p16 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p24 X)))/\(~(p14 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p35 Y)))/\(~(p23 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p33 Y)))/\(~(p23 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p31 Y)))/\(~(p23 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p22 X)))/\(~(p16 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p22 X)))/\(~(p14 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p35 Y)))/\(~(p21 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p34 Y)))/\(~(p21 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p33 Y)))/\(~(p21 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p31 Y)))/\(~(p21 X)))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p25 X)))/\(~(p15 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p23 X)))/\(~(p15 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p25 X)))/\(~(p13 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p23 X)))/\(~(p13 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p21 X)))/\(~(p12 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p25 X)))/\(~(p11 Y)))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p23 X)))/\(~(p11 Y)))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(p15 X)))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(p13 X)))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(p12 X)))))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(p11 X)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 22.93/23.21 Proof. % 22.93/23.21 assert (zenon_L1_ : forall (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U), (r1 zenon_TX_j zenon_TY_i) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_h)) -> (r1 zenon_TY_i zenon_TX_h) -> False). % 22.93/23.21 do 3 intro. intros zenon_H3 zenon_H4 zenon_H5 zenon_H6. % 22.93/23.21 elim (classic ((~(zenon_TX_j = zenon_TY_i))/\(~(r1 zenon_TX_j zenon_TY_i)))); [ zenon_intro zenon_Ha | zenon_intro zenon_Hb ]. % 22.93/23.21 apply (zenon_and_s _ _ zenon_Ha). zenon_intro zenon_Hd. zenon_intro zenon_Hc. % 22.93/23.21 exact (zenon_Hc zenon_H3). % 22.93/23.21 cut ((r1 zenon_TY_i zenon_TX_h) = (r1 zenon_TX_j zenon_TX_h)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H5. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H6. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_He]. % 22.93/23.21 cut ((zenon_TY_i = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_Hf]. % 22.93/23.21 congruence. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_Hb); [ zenon_intro zenon_H11 | zenon_intro zenon_H10 ]. % 22.93/23.21 apply zenon_H11. zenon_intro zenon_H12. % 22.93/23.21 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 22.93/23.21 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TY_i = zenon_TX_j)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_Hf. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H13. % 22.93/23.21 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 22.93/23.21 cut ((zenon_TX_j = zenon_TY_i)); [idtac | apply NNPP; zenon_intro zenon_Hd]. % 22.93/23.21 congruence. % 22.93/23.21 exact (zenon_Hd zenon_H12). % 22.93/23.21 apply zenon_H14. apply refl_equal. % 22.93/23.21 apply zenon_H14. apply refl_equal. % 22.93/23.21 apply zenon_H10. zenon_intro zenon_H3. % 22.93/23.21 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 22.93/23.21 generalize (zenon_H15 zenon_TY_i). zenon_intro zenon_H16. % 22.93/23.21 generalize (zenon_H16 zenon_TX_h). zenon_intro zenon_H17. % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H17); [ zenon_intro zenon_Hc | zenon_intro zenon_H18 ]. % 22.93/23.21 exact (zenon_Hc zenon_H3). % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H18); [ zenon_intro zenon_H1a | zenon_intro zenon_H19 ]. % 22.93/23.21 exact (zenon_H1a zenon_H6). % 22.93/23.21 exact (zenon_H5 zenon_H19). % 22.93/23.21 apply zenon_He. apply refl_equal. % 22.93/23.21 (* end of lemma zenon_L1_ *) % 22.93/23.21 assert (zenon_L2_ : forall (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U), (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TX_bd)) -> (r1 zenon_TX_h zenon_TX_bd) -> False). % 22.93/23.21 do 4 intro. intros zenon_H3 zenon_H6 zenon_H4 zenon_H1b zenon_H1c. % 22.93/23.21 elim (classic ((~(zenon_TX_j = zenon_TX_h))/\(~(r1 zenon_TX_j zenon_TX_h)))); [ zenon_intro zenon_H1e | zenon_intro zenon_H1f ]. % 22.93/23.21 apply (zenon_and_s _ _ zenon_H1e). zenon_intro zenon_H20. zenon_intro zenon_H5. % 22.93/23.21 apply (zenon_L1_ zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 22.93/23.21 cut ((r1 zenon_TX_h zenon_TX_bd) = (r1 zenon_TX_j zenon_TX_bd)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H1b. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H1c. % 22.93/23.21 cut ((zenon_TX_bd = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H21]. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H22]. % 22.93/23.21 congruence. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_H1f); [ zenon_intro zenon_H24 | zenon_intro zenon_H23 ]. % 22.93/23.21 apply zenon_H24. zenon_intro zenon_H25. % 22.93/23.21 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 22.93/23.21 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_h = zenon_TX_j)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H22. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H13. % 22.93/23.21 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 22.93/23.21 cut ((zenon_TX_j = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_H20]. % 22.93/23.21 congruence. % 22.93/23.21 exact (zenon_H20 zenon_H25). % 22.93/23.21 apply zenon_H14. apply refl_equal. % 22.93/23.21 apply zenon_H14. apply refl_equal. % 22.93/23.21 apply zenon_H23. zenon_intro zenon_H19. % 22.93/23.21 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 22.93/23.21 generalize (zenon_H15 zenon_TX_h). zenon_intro zenon_H26. % 22.93/23.21 generalize (zenon_H26 zenon_TX_bd). zenon_intro zenon_H27. % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H27); [ zenon_intro zenon_H5 | zenon_intro zenon_H28 ]. % 22.93/23.21 exact (zenon_H5 zenon_H19). % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H28); [ zenon_intro zenon_H2a | zenon_intro zenon_H29 ]. % 22.93/23.21 exact (zenon_H2a zenon_H1c). % 22.93/23.21 exact (zenon_H1b zenon_H29). % 22.93/23.21 apply zenon_H21. apply refl_equal. % 22.93/23.21 (* end of lemma zenon_L2_ *) % 22.93/23.21 assert (zenon_L3_ : forall (zenon_TY_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U), (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TX_j zenon_TY_bt)) -> (r1 zenon_TX_bd zenon_TY_bt) -> False). % 22.93/23.21 do 5 intro. intros zenon_H6 zenon_H3 zenon_H1c zenon_H4 zenon_H2b zenon_H2c. % 22.93/23.21 elim (classic ((~(zenon_TX_j = zenon_TX_bd))/\(~(r1 zenon_TX_j zenon_TX_bd)))); [ zenon_intro zenon_H2e | zenon_intro zenon_H2f ]. % 22.93/23.21 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H30. zenon_intro zenon_H1b. % 22.93/23.21 apply (zenon_L2_ zenon_TX_bd zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 22.93/23.21 cut ((r1 zenon_TX_bd zenon_TY_bt) = (r1 zenon_TX_j zenon_TY_bt)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H2b. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H2c. % 22.93/23.21 cut ((zenon_TY_bt = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H31]. % 22.93/23.21 cut ((zenon_TX_bd = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H32]. % 22.93/23.21 congruence. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_H2f); [ zenon_intro zenon_H34 | zenon_intro zenon_H33 ]. % 22.93/23.21 apply zenon_H34. zenon_intro zenon_H35. % 22.93/23.21 elim (classic (zenon_TX_j = zenon_TX_j)); [ zenon_intro zenon_H13 | zenon_intro zenon_H14 ]. % 22.93/23.21 cut ((zenon_TX_j = zenon_TX_j) = (zenon_TX_bd = zenon_TX_j)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H32. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H13. % 22.93/23.21 cut ((zenon_TX_j = zenon_TX_j)); [idtac | apply NNPP; zenon_intro zenon_H14]. % 22.93/23.21 cut ((zenon_TX_j = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H30]. % 22.93/23.21 congruence. % 22.93/23.21 exact (zenon_H30 zenon_H35). % 22.93/23.21 apply zenon_H14. apply refl_equal. % 22.93/23.21 apply zenon_H14. apply refl_equal. % 22.93/23.21 apply zenon_H33. zenon_intro zenon_H29. % 22.93/23.21 generalize (zenon_H4 zenon_TX_j). zenon_intro zenon_H15. % 22.93/23.21 generalize (zenon_H15 zenon_TX_bd). zenon_intro zenon_H36. % 22.93/23.21 generalize (zenon_H36 zenon_TY_bt). zenon_intro zenon_H37. % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H37); [ zenon_intro zenon_H1b | zenon_intro zenon_H38 ]. % 22.93/23.21 exact (zenon_H1b zenon_H29). % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H38); [ zenon_intro zenon_H3a | zenon_intro zenon_H39 ]. % 22.93/23.21 exact (zenon_H3a zenon_H2c). % 22.93/23.21 exact (zenon_H2b zenon_H39). % 22.93/23.21 apply zenon_H31. apply refl_equal. % 22.93/23.21 (* end of lemma zenon_L3_ *) % 22.93/23.21 assert (zenon_L4_ : forall (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U), (r1 zenon_TY_i zenon_TX_h) -> (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(r1 zenon_TY_i zenon_TX_bd)) -> (r1 zenon_TX_h zenon_TX_bd) -> False). % 22.93/23.21 do 3 intro. intros zenon_H6 zenon_H4 zenon_H3b zenon_H1c. % 22.93/23.21 elim (classic ((~(zenon_TY_i = zenon_TX_h))/\(~(r1 zenon_TY_i zenon_TX_h)))); [ zenon_intro zenon_H3c | zenon_intro zenon_H3d ]. % 22.93/23.21 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3e. zenon_intro zenon_H1a. % 22.93/23.21 exact (zenon_H1a zenon_H6). % 22.93/23.21 cut ((r1 zenon_TX_h zenon_TX_bd) = (r1 zenon_TY_i zenon_TX_bd)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H3b. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H1c. % 22.93/23.21 cut ((zenon_TX_bd = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H21]. % 22.93/23.21 cut ((zenon_TX_h = zenon_TY_i)); [idtac | apply NNPP; zenon_intro zenon_H3f]. % 22.93/23.21 congruence. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_H3d); [ zenon_intro zenon_H41 | zenon_intro zenon_H40 ]. % 22.93/23.21 apply zenon_H41. zenon_intro zenon_H42. % 22.93/23.21 elim (classic (zenon_TY_i = zenon_TY_i)); [ zenon_intro zenon_H43 | zenon_intro zenon_H44 ]. % 22.93/23.21 cut ((zenon_TY_i = zenon_TY_i) = (zenon_TX_h = zenon_TY_i)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H3f. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H43. % 22.93/23.21 cut ((zenon_TY_i = zenon_TY_i)); [idtac | apply NNPP; zenon_intro zenon_H44]. % 22.93/23.21 cut ((zenon_TY_i = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 22.93/23.21 congruence. % 22.93/23.21 exact (zenon_H3e zenon_H42). % 22.93/23.21 apply zenon_H44. apply refl_equal. % 22.93/23.21 apply zenon_H44. apply refl_equal. % 22.93/23.21 apply zenon_H40. zenon_intro zenon_H6. % 22.93/23.21 generalize (zenon_H4 zenon_TY_i). zenon_intro zenon_H45. % 22.93/23.21 generalize (zenon_H45 zenon_TX_h). zenon_intro zenon_H46. % 22.93/23.21 generalize (zenon_H46 zenon_TX_bd). zenon_intro zenon_H47. % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H47); [ zenon_intro zenon_H1a | zenon_intro zenon_H48 ]. % 22.93/23.21 exact (zenon_H1a zenon_H6). % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H48); [ zenon_intro zenon_H2a | zenon_intro zenon_H49 ]. % 22.93/23.21 exact (zenon_H2a zenon_H1c). % 22.93/23.21 exact (zenon_H3b zenon_H49). % 22.93/23.21 apply zenon_H21. apply refl_equal. % 22.93/23.21 (* end of lemma zenon_L4_ *) % 22.93/23.21 assert (zenon_L5_ : forall (zenon_TX_bd : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_cz : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(forall Y : zenon_U, ((~(r1 zenon_TX_cz Y))\/(p54 Y)))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(p56 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(p52 X)))))))))) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_bt zenon_TX_cz) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_bd zenon_TY_bt) -> False). % 22.93/23.21 do 6 intro. intros zenon_H4 zenon_H4a zenon_H4b zenon_H6 zenon_H3 zenon_H4c zenon_H1c zenon_H2c. % 22.93/23.21 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_cz Y))\/(p54 Y))) zenon_H4a); [ zenon_intro zenon_H4e; idtac ]. % 22.93/23.21 elim zenon_H4e. zenon_intro zenon_TY_db. zenon_intro zenon_H50. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H50). zenon_intro zenon_H52. zenon_intro zenon_H51. % 22.93/23.21 apply zenon_H52. zenon_intro zenon_H53. % 22.93/23.21 generalize (zenon_H4b zenon_TX_h). zenon_intro zenon_H54. % 22.93/23.21 apply (zenon_or_s _ _ zenon_H54); [ zenon_intro zenon_H5 | zenon_intro zenon_H55 ]. % 22.93/23.21 apply (zenon_L1_ zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H55). zenon_intro zenon_H57. zenon_intro zenon_H56. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H58). zenon_intro zenon_H59. zenon_intro zenon_H5a. % 22.93/23.21 apply zenon_H59. zenon_intro zenon_H5b. % 22.93/23.21 generalize (zenon_H5b zenon_TY_db). zenon_intro zenon_H5c. % 22.93/23.21 apply (zenon_or_s _ _ zenon_H5c); [ zenon_intro zenon_H5e | zenon_intro zenon_H5d ]. % 22.93/23.21 elim (classic ((~(zenon_TX_h = zenon_TX_cz))/\(~(r1 zenon_TX_h zenon_TX_cz)))); [ zenon_intro zenon_H5f | zenon_intro zenon_H60 ]. % 22.93/23.21 apply (zenon_and_s _ _ zenon_H5f). zenon_intro zenon_H62. zenon_intro zenon_H61. % 22.93/23.21 elim (classic ((~(zenon_TX_h = zenon_TY_bt))/\(~(r1 zenon_TX_h zenon_TY_bt)))); [ zenon_intro zenon_H63 | zenon_intro zenon_H64 ]. % 22.93/23.21 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 22.93/23.21 elim (classic ((~(zenon_TX_h = zenon_TX_bd))/\(~(r1 zenon_TX_h zenon_TX_bd)))); [ zenon_intro zenon_H67 | zenon_intro zenon_H68 ]. % 22.93/23.21 apply (zenon_and_s _ _ zenon_H67). zenon_intro zenon_H69. zenon_intro zenon_H2a. % 22.93/23.21 exact (zenon_H2a zenon_H1c). % 22.93/23.21 cut ((r1 zenon_TX_bd zenon_TY_bt) = (r1 zenon_TX_h zenon_TY_bt)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H65. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H2c. % 22.93/23.21 cut ((zenon_TY_bt = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H31]. % 22.93/23.21 cut ((zenon_TX_bd = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_H6a]. % 22.93/23.21 congruence. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_H68); [ zenon_intro zenon_H6c | zenon_intro zenon_H6b ]. % 22.93/23.21 apply zenon_H6c. zenon_intro zenon_H6d. % 22.93/23.21 elim (classic (zenon_TX_h = zenon_TX_h)); [ zenon_intro zenon_H6e | zenon_intro zenon_He ]. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_h) = (zenon_TX_bd = zenon_TX_h)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H6a. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H6e. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_He]. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H69]. % 22.93/23.21 congruence. % 22.93/23.21 exact (zenon_H69 zenon_H6d). % 22.93/23.21 apply zenon_He. apply refl_equal. % 22.93/23.21 apply zenon_He. apply refl_equal. % 22.93/23.21 apply zenon_H6b. zenon_intro zenon_H1c. % 22.93/23.21 generalize (zenon_H4 zenon_TX_h). zenon_intro zenon_H6f. % 22.93/23.21 generalize (zenon_H6f zenon_TX_bd). zenon_intro zenon_H70. % 22.93/23.21 generalize (zenon_H70 zenon_TY_bt). zenon_intro zenon_H71. % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H71); [ zenon_intro zenon_H2a | zenon_intro zenon_H72 ]. % 22.93/23.21 exact (zenon_H2a zenon_H1c). % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H72); [ zenon_intro zenon_H3a | zenon_intro zenon_H73 ]. % 22.93/23.21 exact (zenon_H3a zenon_H2c). % 22.93/23.21 exact (zenon_H65 zenon_H73). % 22.93/23.21 apply zenon_H31. apply refl_equal. % 22.93/23.21 cut ((r1 zenon_TY_bt zenon_TX_cz) = (r1 zenon_TX_h zenon_TX_cz)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H61. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H4c. % 22.93/23.21 cut ((zenon_TX_cz = zenon_TX_cz)); [idtac | apply NNPP; zenon_intro zenon_H74]. % 22.93/23.21 cut ((zenon_TY_bt = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_H75]. % 22.93/23.21 congruence. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_H64); [ zenon_intro zenon_H77 | zenon_intro zenon_H76 ]. % 22.93/23.21 apply zenon_H77. zenon_intro zenon_H78. % 22.93/23.21 elim (classic (zenon_TX_h = zenon_TX_h)); [ zenon_intro zenon_H6e | zenon_intro zenon_He ]. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_h) = (zenon_TY_bt = zenon_TX_h)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H75. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H6e. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_He]. % 22.93/23.21 cut ((zenon_TX_h = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H66]. % 22.93/23.21 congruence. % 22.93/23.21 exact (zenon_H66 zenon_H78). % 22.93/23.21 apply zenon_He. apply refl_equal. % 22.93/23.21 apply zenon_He. apply refl_equal. % 22.93/23.21 apply zenon_H76. zenon_intro zenon_H73. % 22.93/23.21 generalize (zenon_H4 zenon_TX_h). zenon_intro zenon_H6f. % 22.93/23.21 generalize (zenon_H6f zenon_TY_bt). zenon_intro zenon_H79. % 22.93/23.21 generalize (zenon_H79 zenon_TX_cz). zenon_intro zenon_H7a. % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H7a); [ zenon_intro zenon_H65 | zenon_intro zenon_H7b ]. % 22.93/23.21 exact (zenon_H65 zenon_H73). % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H7d | zenon_intro zenon_H7c ]. % 22.93/23.21 exact (zenon_H7d zenon_H4c). % 22.93/23.21 exact (zenon_H61 zenon_H7c). % 22.93/23.21 apply zenon_H74. apply refl_equal. % 22.93/23.21 cut ((r1 zenon_TX_cz zenon_TY_db) = (r1 zenon_TX_h zenon_TY_db)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H5e. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H53. % 22.93/23.21 cut ((zenon_TY_db = zenon_TY_db)); [idtac | apply NNPP; zenon_intro zenon_H7e]. % 22.93/23.21 cut ((zenon_TX_cz = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_H7f]. % 22.93/23.21 congruence. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_H60); [ zenon_intro zenon_H81 | zenon_intro zenon_H80 ]. % 22.93/23.21 apply zenon_H81. zenon_intro zenon_H82. % 22.93/23.21 elim (classic (zenon_TX_h = zenon_TX_h)); [ zenon_intro zenon_H6e | zenon_intro zenon_He ]. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_h) = (zenon_TX_cz = zenon_TX_h)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H7f. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H6e. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_h)); [idtac | apply NNPP; zenon_intro zenon_He]. % 22.93/23.21 cut ((zenon_TX_h = zenon_TX_cz)); [idtac | apply NNPP; zenon_intro zenon_H62]. % 22.93/23.21 congruence. % 22.93/23.21 exact (zenon_H62 zenon_H82). % 22.93/23.21 apply zenon_He. apply refl_equal. % 22.93/23.21 apply zenon_He. apply refl_equal. % 22.93/23.21 apply zenon_H80. zenon_intro zenon_H7c. % 22.93/23.21 generalize (zenon_H4 zenon_TX_h). zenon_intro zenon_H6f. % 22.93/23.21 generalize (zenon_H6f zenon_TX_cz). zenon_intro zenon_H83. % 22.93/23.21 generalize (zenon_H83 zenon_TY_db). zenon_intro zenon_H84. % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H84); [ zenon_intro zenon_H61 | zenon_intro zenon_H85 ]. % 22.93/23.21 exact (zenon_H61 zenon_H7c). % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H85); [ zenon_intro zenon_H87 | zenon_intro zenon_H86 ]. % 22.93/23.21 exact (zenon_H87 zenon_H53). % 22.93/23.21 exact (zenon_H5e zenon_H86). % 22.93/23.21 apply zenon_H7e. apply refl_equal. % 22.93/23.21 exact (zenon_H51 zenon_H5d). % 22.93/23.21 (* end of lemma zenon_L5_ *) % 22.93/23.21 assert (zenon_L6_ : forall (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TX_h : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TX_bd : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (forall X : zenon_U, ((~(r1 zenon_TX_bd X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p54 Y)))/\(~(p41 X)))))) -> (r1 zenon_TY_bt zenon_TX_cz) -> (r1 zenon_TX_bd zenon_TY_bt) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TY_i zenon_TX_h) -> (forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(p56 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(p52 X)))))))))) -> (~(p41 zenon_TX_cz)) -> False). % 22.93/23.21 do 6 intro. intros zenon_H4 zenon_H88 zenon_H4c zenon_H2c zenon_H1c zenon_H3 zenon_H6 zenon_H4b zenon_H89. % 22.93/23.21 generalize (zenon_H88 zenon_TX_cz). zenon_intro zenon_H8a. % 22.93/23.21 apply (zenon_or_s _ _ zenon_H8a); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 22.93/23.21 elim (classic ((~(zenon_TX_bd = zenon_TY_bt))/\(~(r1 zenon_TX_bd zenon_TY_bt)))); [ zenon_intro zenon_H8d | zenon_intro zenon_H8e ]. % 22.93/23.21 apply (zenon_and_s _ _ zenon_H8d). zenon_intro zenon_H8f. zenon_intro zenon_H3a. % 22.93/23.21 exact (zenon_H3a zenon_H2c). % 22.93/23.21 cut ((r1 zenon_TY_bt zenon_TX_cz) = (r1 zenon_TX_bd zenon_TX_cz)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H8c. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H4c. % 22.93/23.21 cut ((zenon_TX_cz = zenon_TX_cz)); [idtac | apply NNPP; zenon_intro zenon_H74]. % 22.93/23.21 cut ((zenon_TY_bt = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H90]. % 22.93/23.21 congruence. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_H8e); [ zenon_intro zenon_H92 | zenon_intro zenon_H91 ]. % 22.93/23.21 apply zenon_H92. zenon_intro zenon_H93. % 22.93/23.21 elim (classic (zenon_TX_bd = zenon_TX_bd)); [ zenon_intro zenon_H94 | zenon_intro zenon_H21 ]. % 22.93/23.21 cut ((zenon_TX_bd = zenon_TX_bd) = (zenon_TY_bt = zenon_TX_bd)). % 22.93/23.21 intro zenon_D_pnotp. % 22.93/23.21 apply zenon_H90. % 22.93/23.21 rewrite <- zenon_D_pnotp. % 22.93/23.21 exact zenon_H94. % 22.93/23.21 cut ((zenon_TX_bd = zenon_TX_bd)); [idtac | apply NNPP; zenon_intro zenon_H21]. % 22.93/23.21 cut ((zenon_TX_bd = zenon_TY_bt)); [idtac | apply NNPP; zenon_intro zenon_H8f]. % 22.93/23.21 congruence. % 22.93/23.21 exact (zenon_H8f zenon_H93). % 22.93/23.21 apply zenon_H21. apply refl_equal. % 22.93/23.21 apply zenon_H21. apply refl_equal. % 22.93/23.21 apply zenon_H91. zenon_intro zenon_H2c. % 22.93/23.21 generalize (zenon_H4 zenon_TX_bd). zenon_intro zenon_H95. % 22.93/23.21 generalize (zenon_H95 zenon_TY_bt). zenon_intro zenon_H96. % 22.93/23.21 generalize (zenon_H96 zenon_TX_cz). zenon_intro zenon_H97. % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H97); [ zenon_intro zenon_H3a | zenon_intro zenon_H98 ]. % 22.93/23.21 exact (zenon_H3a zenon_H2c). % 22.93/23.21 apply (zenon_imply_s _ _ zenon_H98); [ zenon_intro zenon_H7d | zenon_intro zenon_H99 ]. % 22.93/23.21 exact (zenon_H7d zenon_H4c). % 22.93/23.21 exact (zenon_H8c zenon_H99). % 22.93/23.21 apply zenon_H74. apply refl_equal. % 22.93/23.21 apply (zenon_notand_s _ _ zenon_H8b); [ zenon_intro zenon_H4a | zenon_intro zenon_H9a ]. % 22.93/23.21 apply (zenon_L5_ zenon_TX_bd zenon_TY_bt zenon_TX_h zenon_TY_i zenon_TX_j zenon_TX_cz); trivial. % 22.93/23.21 exact (zenon_H9a zenon_H89). % 22.93/23.21 (* end of lemma zenon_L6_ *) % 22.93/23.21 assert (zenon_L7_ : forall (zenon_TX_j : zenon_U) (zenon_TX_cz : zenon_U) (zenon_TY_bt : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (forall Y : zenon_U, ((~(r1 zenon_TY_i Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p54 Y)))/\(~(p41 X)))))))) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TY_bt zenon_TX_cz) -> (r1 zenon_TX_bd zenon_TY_bt) -> (r1 zenon_TX_j zenon_TY_i) -> (forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(p56 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(p52 X)))))))))) -> (~(p41 zenon_TX_cz)) -> False). % 22.93/23.21 do 6 intro. intros zenon_H4 zenon_H9b zenon_H1c zenon_H6 zenon_H4c zenon_H2c zenon_H3 zenon_H4b zenon_H89. % 22.93/23.21 generalize (zenon_H9b zenon_TX_bd). zenon_intro zenon_H9c. % 22.93/23.21 apply (zenon_or_s _ _ zenon_H9c); [ zenon_intro zenon_H3b | zenon_intro zenon_H88 ]. % 22.93/23.21 apply (zenon_L4_ zenon_TX_bd zenon_TX_h zenon_TY_i); trivial. % 22.93/23.21 apply (zenon_L6_ zenon_TY_i zenon_TX_j zenon_TX_h zenon_TX_cz zenon_TY_bt zenon_TX_bd); trivial. % 22.93/23.21 (* end of lemma zenon_L7_ *) % 22.93/23.21 assert (zenon_L8_ : forall (zenon_TX_bd : zenon_U) (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_j : zenon_U) (zenon_TY_bt : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (~(forall X : zenon_U, ((~(r1 zenon_TY_bt X))\/(p41 X)))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p54 Y)))/\(~(p41 X)))))))))))) -> (r1 zenon_TX_j zenon_TY_i) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_bd zenon_TY_bt) -> (forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(p56 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(p52 X)))))))))) -> False). % 22.93/23.21 do 5 intro. intros zenon_H4 zenon_H9d zenon_H9e zenon_H3 zenon_H1c zenon_H6 zenon_H2c zenon_H4b. % 22.93/23.21 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TY_bt X))\/(p41 X))) zenon_H9d); [ zenon_intro zenon_H9f; idtac ]. % 22.93/23.21 elim zenon_H9f. zenon_intro zenon_TX_cz. zenon_intro zenon_Ha0. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Ha0). zenon_intro zenon_Ha1. zenon_intro zenon_H89. % 22.93/23.21 apply zenon_Ha1. zenon_intro zenon_H4c. % 22.93/23.21 generalize (zenon_H9e zenon_TY_i). zenon_intro zenon_Ha2. % 22.93/23.21 apply (zenon_or_s _ _ zenon_Ha2); [ zenon_intro zenon_Hc | zenon_intro zenon_Ha3 ]. % 22.93/23.21 exact (zenon_Hc zenon_H3). % 22.93/23.21 generalize (zenon_Ha3 zenon_TY_i). zenon_intro zenon_Ha4. % 22.93/23.21 apply (zenon_or_s _ _ zenon_Ha4); [ zenon_intro zenon_Ha5 | zenon_intro zenon_H9b ]. % 22.93/23.21 generalize (reflexivity zenon_TY_i). zenon_intro zenon_Ha6. % 22.93/23.21 exact (zenon_Ha5 zenon_Ha6). % 22.93/23.21 apply (zenon_L7_ zenon_TX_j zenon_TX_cz zenon_TY_bt zenon_TX_bd zenon_TX_h zenon_TY_i); trivial. % 22.93/23.21 (* end of lemma zenon_L8_ *) % 22.93/23.21 assert (zenon_L9_ : forall (zenon_TX_h : zenon_U) (zenon_TY_i : zenon_U) (zenon_TX_bd : zenon_U) (zenon_TX_j : zenon_U) (zenon_TY_bt : zenon_U), (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z)))))) -> (forall Y : zenon_U, ((~(r1 zenon_TY_bt Y))\/(~((forall X : zenon_U, ((~(r1 Y X))\/(p41 X)))/\(~(p34 Y)))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/(~((~(forall X : zenon_U, ((~(r1 Y X))\/(p56 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/((~(forall X : zenon_U, ((~(r1 Y X))\/(p54 X))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(p52 X)))))))))) -> (r1 zenon_TX_bd zenon_TY_bt) -> (r1 zenon_TY_i zenon_TX_h) -> (r1 zenon_TX_h zenon_TX_bd) -> (r1 zenon_TX_j zenon_TY_i) -> (forall Y : zenon_U, ((~(r1 zenon_TX_j Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(~((forall Y : zenon_U, ((~(r1 X Y))\/(p54 Y)))/\(~(p41 X)))))))))))) -> (~(p34 zenon_TY_bt)) -> False). % 22.93/23.21 do 5 intro. intros zenon_H4 zenon_Ha7 zenon_H4b zenon_H2c zenon_H6 zenon_H1c zenon_H3 zenon_H9e zenon_Ha8. % 22.93/23.21 generalize (zenon_Ha7 zenon_TY_bt). zenon_intro zenon_Ha9. % 22.93/23.21 apply (zenon_or_s _ _ zenon_Ha9); [ zenon_intro zenon_Hab | zenon_intro zenon_Haa ]. % 22.93/23.21 generalize (reflexivity zenon_TY_bt). zenon_intro zenon_Hac. % 22.93/23.21 exact (zenon_Hab zenon_Hac). % 22.93/23.21 apply (zenon_notand_s _ _ zenon_Haa); [ zenon_intro zenon_H9d | zenon_intro zenon_Had ]. % 22.93/23.21 apply (zenon_L8_ zenon_TX_bd zenon_TX_h zenon_TY_i zenon_TX_j zenon_TY_bt); trivial. % 22.93/23.21 exact (zenon_Had zenon_Ha8). % 22.93/23.21 (* end of lemma zenon_L9_ *) % 22.93/23.21 apply NNPP. intro zenon_G. % 22.93/23.21 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((r1 x y)->((r1 y z)->(r1 x z))))))); [ zenon_intro zenon_H4 | zenon_intro zenon_Hae ]. % 22.93/23.21 apply zenon_G. zenon_intro zenon_Haf. % 22.93/23.21 elim zenon_Haf. zenon_intro zenon_TX_j. zenon_intro zenon_Hb0. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hb0). zenon_intro zenon_Hb2. zenon_intro zenon_Hb1. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hb1). zenon_intro zenon_Hb4. zenon_intro zenon_Hb3. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hb3). zenon_intro zenon_Hb6. zenon_intro zenon_Hb5. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hb5). zenon_intro zenon_Hb8. zenon_intro zenon_Hb7. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hb7). zenon_intro zenon_Hba. zenon_intro zenon_Hb9. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hb9). zenon_intro zenon_Hbc. zenon_intro zenon_Hbb. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hbb). zenon_intro zenon_Hbe. zenon_intro zenon_Hbd. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hbd). zenon_intro zenon_Hc0. zenon_intro zenon_Hbf. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hbf). zenon_intro zenon_Hc2. zenon_intro zenon_Hc1. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hc1). zenon_intro zenon_Hc4. zenon_intro zenon_Hc3. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hc3). zenon_intro zenon_Hc6. zenon_intro zenon_Hc5. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hc5). zenon_intro zenon_Hc8. zenon_intro zenon_Hc7. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hc7). zenon_intro zenon_Hca. zenon_intro zenon_Hc9. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hc9). zenon_intro zenon_Hcc. zenon_intro zenon_Hcb. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hcb). zenon_intro zenon_Hce. zenon_intro zenon_Hcd. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hcd). zenon_intro zenon_Hd0. zenon_intro zenon_Hcf. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hcf). zenon_intro zenon_Hd2. zenon_intro zenon_Hd1. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hd1). zenon_intro zenon_Hd4. zenon_intro zenon_Hd3. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hd3). zenon_intro zenon_Hd6. zenon_intro zenon_Hd5. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hd5). zenon_intro zenon_Hd8. zenon_intro zenon_Hd7. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hd7). zenon_intro zenon_Hda. zenon_intro zenon_Hd9. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hd9). zenon_intro zenon_Hdc. zenon_intro zenon_Hdb. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hdb). zenon_intro zenon_Hde. zenon_intro zenon_Hdd. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hdd). zenon_intro zenon_He0. zenon_intro zenon_Hdf. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hdf). zenon_intro zenon_He2. zenon_intro zenon_He1. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_He1). zenon_intro zenon_He4. zenon_intro zenon_He3. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_He3). zenon_intro zenon_He6. zenon_intro zenon_He5. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_He5). zenon_intro zenon_He8. zenon_intro zenon_He7. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_He7). zenon_intro zenon_Hea. zenon_intro zenon_He9. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_He9). zenon_intro zenon_Hec. zenon_intro zenon_Heb. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Heb). zenon_intro zenon_Hee. zenon_intro zenon_Hed. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hed). zenon_intro zenon_Hf0. zenon_intro zenon_Hef. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hef). zenon_intro zenon_Hf2. zenon_intro zenon_Hf1. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hf1). zenon_intro zenon_Hf4. zenon_intro zenon_Hf3. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hf3). zenon_intro zenon_Hf6. zenon_intro zenon_Hf5. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hf5). zenon_intro zenon_Hf8. zenon_intro zenon_Hf7. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hf7). zenon_intro zenon_Hfa. zenon_intro zenon_Hf9. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hf9). zenon_intro zenon_Hfc. zenon_intro zenon_Hfb. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hfb). zenon_intro zenon_Hfe. zenon_intro zenon_Hfd. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hfd). zenon_intro zenon_H100. zenon_intro zenon_Hff. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_Hff). zenon_intro zenon_H102. zenon_intro zenon_H101. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H101). zenon_intro zenon_H104. zenon_intro zenon_H103. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H103). zenon_intro zenon_H106. zenon_intro zenon_H105. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H105). zenon_intro zenon_H108. zenon_intro zenon_H107. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H107). zenon_intro zenon_H10a. zenon_intro zenon_H109. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H109). zenon_intro zenon_H10c. zenon_intro zenon_H10b. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H10b). zenon_intro zenon_H10e. zenon_intro zenon_H10d. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H10d). zenon_intro zenon_H110. zenon_intro zenon_H10f. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H10f). zenon_intro zenon_H112. zenon_intro zenon_H111. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H111). zenon_intro zenon_H114. zenon_intro zenon_H113. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H113). zenon_intro zenon_H116. zenon_intro zenon_H115. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H115). zenon_intro zenon_H118. zenon_intro zenon_H117. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H117). zenon_intro zenon_H11a. zenon_intro zenon_H119. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H119). zenon_intro zenon_H11c. zenon_intro zenon_H11b. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H11b). zenon_intro zenon_H11e. zenon_intro zenon_H11d. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H11d). zenon_intro zenon_H120. zenon_intro zenon_H11f. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H11f). zenon_intro zenon_H122. zenon_intro zenon_H121. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H121). zenon_intro zenon_H124. zenon_intro zenon_H123. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H123). zenon_intro zenon_H126. zenon_intro zenon_H125. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H125). zenon_intro zenon_H128. zenon_intro zenon_H127. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H127). zenon_intro zenon_H12a. zenon_intro zenon_H129. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H129). zenon_intro zenon_H12c. zenon_intro zenon_H12b. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H12b). zenon_intro zenon_H12e. zenon_intro zenon_H12d. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H12d). zenon_intro zenon_H130. zenon_intro zenon_H12f. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H12f). zenon_intro zenon_H132. zenon_intro zenon_H131. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H131). zenon_intro zenon_H134. zenon_intro zenon_H133. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H133). zenon_intro zenon_H136. zenon_intro zenon_H135. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H135). zenon_intro zenon_H138. zenon_intro zenon_H137. % 22.93/23.21 apply zenon_H12e. zenon_intro zenon_H139. % 22.93/23.21 apply zenon_H120. zenon_intro zenon_H13a. % 22.93/23.21 apply zenon_Hf6. zenon_intro zenon_H13b. % 22.93/23.21 apply zenon_He0. zenon_intro zenon_H9e. % 22.93/23.21 apply zenon_Hb2. zenon_intro zenon_H4b. % 22.93/23.21 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_j Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(p12 X))))) zenon_H138); [ zenon_intro zenon_H13c; idtac ]. % 22.93/23.21 elim zenon_H13c. zenon_intro zenon_TY_i. zenon_intro zenon_H13d. % 22.93/23.21 apply (zenon_notor_s _ _ zenon_H13d). zenon_intro zenon_H10. zenon_intro zenon_H13e. % 22.93/23.26 apply zenon_H10. zenon_intro zenon_H3. % 22.93/23.26 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TY_i X))\/(p12 X))) zenon_H13e); [ zenon_intro zenon_H13f; idtac ]. % 22.93/23.26 elim zenon_H13f. zenon_intro zenon_TX_h. zenon_intro zenon_H140. % 22.93/23.26 apply (zenon_notor_s _ _ zenon_H140). zenon_intro zenon_H40. zenon_intro zenon_H141. % 22.93/23.26 apply zenon_H40. zenon_intro zenon_H6. % 22.93/23.26 generalize (zenon_H139 zenon_TX_h). zenon_intro zenon_H142. % 22.93/23.26 apply (zenon_or_s _ _ zenon_H142); [ zenon_intro zenon_H5 | zenon_intro zenon_H143 ]. % 22.93/23.26 apply (zenon_L1_ zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 22.93/23.26 apply (zenon_notand_s _ _ zenon_H143); [ zenon_intro zenon_H145 | zenon_intro zenon_H144 ]. % 22.93/23.26 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_h X))\/(p21 X))) zenon_H145); [ zenon_intro zenon_H146; idtac ]. % 22.93/23.26 elim zenon_H146. zenon_intro zenon_TX_bd. zenon_intro zenon_H147. % 22.93/23.26 apply (zenon_notor_s _ _ zenon_H147). zenon_intro zenon_H6b. zenon_intro zenon_H148. % 22.93/23.26 apply zenon_H6b. zenon_intro zenon_H1c. % 22.93/23.26 generalize (zenon_H13a zenon_TX_j). zenon_intro zenon_H149. % 22.93/23.26 apply (zenon_or_s _ _ zenon_H149); [ zenon_intro zenon_H14b | zenon_intro zenon_H14a ]. % 22.93/23.26 generalize (reflexivity zenon_TX_j). zenon_intro zenon_H14c. % 22.93/23.26 exact (zenon_H14b zenon_H14c). % 22.93/23.26 generalize (zenon_H14a zenon_TX_bd). zenon_intro zenon_H14d. % 22.93/23.26 apply (zenon_or_s _ _ zenon_H14d); [ zenon_intro zenon_H1b | zenon_intro zenon_H14e ]. % 22.93/23.26 apply (zenon_L2_ zenon_TX_bd zenon_TX_h zenon_TY_i zenon_TX_j); trivial. % 22.93/23.26 apply (zenon_notand_s _ _ zenon_H14e); [ zenon_intro zenon_H150 | zenon_intro zenon_H14f ]. % 22.93/23.26 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_bd Y))\/(p34 Y))) zenon_H150); [ zenon_intro zenon_H151; idtac ]. % 22.93/23.26 elim zenon_H151. zenon_intro zenon_TY_bt. zenon_intro zenon_H152. % 22.93/23.26 apply (zenon_notor_s _ _ zenon_H152). zenon_intro zenon_H91. zenon_intro zenon_Ha8. % 22.93/23.26 apply zenon_H91. zenon_intro zenon_H2c. % 22.93/23.26 generalize (zenon_H13b zenon_TY_bt). zenon_intro zenon_H153. % 22.93/23.26 apply (zenon_or_s _ _ zenon_H153); [ zenon_intro zenon_H2b | zenon_intro zenon_H154 ]. % 22.93/23.26 apply (zenon_L3_ zenon_TY_bt zenon_TX_bd zenon_TX_j zenon_TX_h zenon_TY_i); trivial. % 22.93/23.26 generalize (zenon_H154 zenon_TY_bt). zenon_intro zenon_H155. % 22.93/23.26 apply (zenon_or_s _ _ zenon_H155); [ zenon_intro zenon_Hab | zenon_intro zenon_Ha7 ]. % 22.93/23.26 generalize (reflexivity zenon_TY_bt). zenon_intro zenon_Hac. % 22.93/23.26 exact (zenon_Hab zenon_Hac). % 22.93/23.26 apply (zenon_L9_ zenon_TX_h zenon_TY_i zenon_TX_bd zenon_TX_j zenon_TY_bt); trivial. % 22.93/23.26 exact (zenon_H14f zenon_H148). % 22.93/23.26 exact (zenon_H144 zenon_H141). % 22.93/23.26 apply zenon_Hae. zenon_intro zenon_Tx_ne. apply NNPP. zenon_intro zenon_H157. % 22.93/23.26 apply zenon_H157. zenon_intro zenon_Ty_ng. apply NNPP. zenon_intro zenon_H159. % 22.93/23.26 apply zenon_H159. zenon_intro zenon_Tz_ni. apply NNPP. zenon_intro zenon_H15b. % 22.93/23.26 apply (zenon_notimply_s _ _ zenon_H15b). zenon_intro zenon_H15d. zenon_intro zenon_H15c. % 22.93/23.26 apply (zenon_notimply_s _ _ zenon_H15c). zenon_intro zenon_H15f. zenon_intro zenon_H15e. % 22.93/23.26 generalize (transitivity zenon_Tx_ne). zenon_intro zenon_H160. % 22.93/23.26 generalize (zenon_H160 zenon_Ty_ng). zenon_intro zenon_H161. % 22.93/23.26 generalize (zenon_H161 zenon_Tz_ni). zenon_intro zenon_H162. % 22.93/23.26 apply (zenon_imply_s _ _ zenon_H162); [ zenon_intro zenon_H164 | zenon_intro zenon_H163 ]. % 22.93/23.26 apply (zenon_notand_s _ _ zenon_H164); [ zenon_intro zenon_H166 | zenon_intro zenon_H165 ]. % 22.93/23.26 exact (zenon_H166 zenon_H15d). % 22.93/23.26 exact (zenon_H165 zenon_H15f). % 22.93/23.26 exact (zenon_H15e zenon_H163). % 22.93/23.26 Qed. % 22.93/23.26 % SZS output end Proof % 22.93/23.26 (* END-PROOF *) % 22.93/23.26 nodes searched: 143498 % 22.93/23.26 max branch formulas: 41109 % 22.93/23.26 proof nodes created: 3930 % 22.93/23.26 formulas created: 331478 % 22.93/23.26 %------------------------------------------------------------------------------