%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL686+1.020 : 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:49 PM UTC 2026 % Result : Theorem 1.88s 2.14s % Output : Proof 1.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.08/0.35 % Computer : n008.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sun Sep 6 00:32:53 UTC 2026 % 0.08/0.35 % CPUTime : % 1.88/2.14 (* PROOF-FOUND *) % 1.88/2.14 % SZS status Theorem % 1.88/2.14 (* BEGIN-PROOF *) % 1.88/2.14 % SZS output start Proof % 1.88/2.14 Theorem main : (~(exists X : zenon_U, (~((forall Y : zenon_U, ((~(r1 X Y))\/((~(p60 Y))\/(forall X : zenon_U, ((~(r1 Y 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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/False))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p59 X)/\(~(p58 X)))\/((~(p59 X))/\(p58 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p58 Y)/\(~(p57 Y)))\/((~(p58 Y))/\(p57 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p57 X)/\(~(p56 X)))\/((~(p57 X))/\(p56 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p56 Y)/\(~(p55 Y)))\/((~(p56 Y))/\(p55 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p55 X)/\(~(p54 X)))\/((~(p55 X))/\(p54 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p54 Y)/\(~(p53 Y)))\/((~(p54 Y))/\(p53 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p53 X)/\(~(p52 X)))\/((~(p53 X))/\(p52 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p52 Y)/\(~(p51 Y)))\/((~(p52 Y))/\(p51 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p51 X)/\(~(p50 X)))\/((~(p51 X))/\(p50 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p50 Y)/\(~(p49 Y)))\/((~(p50 Y))/\(p49 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p49 X)/\(~(p48 X)))\/((~(p49 X))/\(p48 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p48 Y)/\(~(p47 Y)))\/((~(p48 Y))/\(p47 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p47 X)/\(~(p46 X)))\/((~(p47 X))/\(p46 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p46 Y)/\(~(p45 Y)))\/((~(p46 Y))/\(p45 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p45 X)/\(~(p44 X)))\/((~(p45 X))/\(p44 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p44 Y)/\(~(p43 Y)))\/((~(p44 Y))/\(p43 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p43 X)/\(~(p42 X)))\/((~(p43 X))/\(p42 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p42 Y)/\(~(p41 Y)))\/((~(p42 Y))/\(p41 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p41 X)/\(~(p40 X)))\/((~(p41 X))/\(p40 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p40 Y)/\(~(p39 Y)))\/((~(p40 Y))/\(p39 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p39 X)/\(~(p38 X)))\/((~(p39 X))/\(p38 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p38 Y)/\(~(p37 Y)))\/((~(p38 Y))/\(p37 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p37 X)/\(~(p36 X)))\/((~(p37 X))/\(p36 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p36 Y)/\(~(p35 Y)))\/((~(p36 Y))/\(p35 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p35 X)/\(~(p34 X)))\/((~(p35 X))/\(p34 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p34 Y)/\(~(p33 Y)))\/((~(p34 Y))/\(p33 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p33 X)/\(~(p32 X)))\/((~(p33 X))/\(p32 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p32 Y)/\(~(p31 Y)))\/((~(p32 Y))/\(p31 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p31 X)/\(~(p30 X)))\/((~(p31 X))/\(p30 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p30 Y)/\(~(p29 Y)))\/((~(p30 Y))/\(p29 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p29 X)/\(~(p28 X)))\/((~(p29 X))/\(p28 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p28 Y)/\(~(p27 Y)))\/((~(p28 Y))/\(p27 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p27 X)/\(~(p26 X)))\/((~(p27 X))/\(p26 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p26 Y)/\(~(p25 Y)))\/((~(p26 Y))/\(p25 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p25 X)/\(~(p24 X)))\/((~(p25 X))/\(p24 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p24 Y)/\(~(p23 Y)))\/((~(p24 Y))/\(p23 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p23 X)/\(~(p22 X)))\/((~(p23 X))/\(p22 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p22 Y)/\(~(p21 Y)))\/((~(p22 Y))/\(p21 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p21 X)/\(~(p20 X)))\/((~(p21 X))/\(p20 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p20 Y)/\(~(p19 Y)))\/((~(p20 Y))/\(p19 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p19 X)/\(~(p18 X)))\/((~(p19 X))/\(p18 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p18 Y)/\(~(p17 Y)))\/((~(p18 Y))/\(p17 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p17 X)/\(~(p16 X)))\/((~(p17 X))/\(p16 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p16 Y)/\(~(p15 Y)))\/((~(p16 Y))/\(p15 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p15 X)/\(~(p14 X)))\/((~(p15 X))/\(p14 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p14 Y)/\(~(p13 Y)))\/((~(p14 Y))/\(p13 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p13 X)/\(~(p12 X)))\/((~(p13 X))/\(p12 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p12 Y)/\(~(p11 Y)))\/((~(p12 Y))/\(p11 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p11 X)/\(~(p10 X)))\/((~(p11 X))/\(p10 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p10 Y)/\(~(p9 Y)))\/((~(p10 Y))/\(p9 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p9 X)/\(~(p8 X)))\/((~(p9 X))/\(p8 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p8 Y)/\(~(p7 Y)))\/((~(p8 Y))/\(p7 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p7 X)/\(~(p6 X)))\/((~(p7 X))/\(p6 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p6 Y)/\(~(p5 Y)))\/((~(p6 Y))/\(p5 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p5 X)/\(~(p4 X)))\/((~(p5 X))/\(p4 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p4 Y)/\(~(p3 Y)))\/((~(p4 Y))/\(p3 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p3 X)/\(~(p2 X)))\/((~(p3 X))/\(p2 X))))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p2 Y)/\(~(p1 Y)))\/((~(p2 Y))/\(p1 Y)))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p60 Y)))\/(forall Y : zenon_U, ((~(r1 X Y))\/(((~(p58 Y))/\(~(p59 Y)))\/(((p59 Y)/\(p58 Y))\/(((~(p57 Y))/\(~(p58 Y)))\/(((p58 Y)/\(p57 Y))\/(((~(p56 Y))/\(~(p57 Y)))\/(((p57 Y)/\(p56 Y))\/(((~(p55 Y))/\(~(p56 Y)))\/(((p56 Y)/\(p55 Y))\/(((~(p54 Y))/\(~(p55 Y)))\/(((p55 Y)/\(p54 Y))\/(((~(p53 Y))/\(~(p54 Y)))\/(((p54 Y)/\(p53 Y))\/(((~(p52 Y))/\(~(p53 Y)))\/(((p53 Y)/\(p52 Y))\/(((~(p51 Y))/\(~(p52 Y)))\/(((p52 Y)/\(p51 Y))\/(((~(p50 Y))/\(~(p51 Y)))\/(((p51 Y)/\(p50 Y))\/(((~(p49 Y))/\(~(p50 Y)))\/(((p50 Y)/\(p49 Y))\/(((~(p48 Y))/\(~(p49 Y)))\/(((p49 Y)/\(p48 Y))\/(((~(p47 Y))/\(~(p48 Y)))\/(((p48 Y)/\(p47 Y))\/(((~(p46 Y))/\(~(p47 Y)))\/(((p47 Y)/\(p46 Y))\/(((~(p45 Y))/\(~(p46 Y)))\/(((p46 Y)/\(p45 Y))\/(((~(p44 Y))/\(~(p45 Y)))\/(((p45 Y)/\(p44 Y))\/(((~(p43 Y))/\(~(p44 Y)))\/(((p44 Y)/\(p43 Y))\/(((~(p42 Y))/\(~(p43 Y)))\/(((p43 Y)/\(p42 Y))\/(((~(p41 Y))/\(~(p42 Y)))\/(((p42 Y)/\(p41 Y))\/(((~(p40 Y))/\(~(p41 Y)))\/(((p41 Y)/\(p40 Y))\/(((~(p39 Y))/\(~(p40 Y)))\/(((p40 Y)/\(p39 Y))\/(((~(p38 Y))/\(~(p39 Y)))\/(((p39 Y)/\(p38 Y))\/(((~(p37 Y))/\(~(p38 Y)))\/(((p38 Y)/\(p37 Y))\/(((~(p36 Y))/\(~(p37 Y)))\/(((p37 Y)/\(p36 Y))\/(((~(p35 Y))/\(~(p36 Y)))\/(((p36 Y)/\(p35 Y))\/(((~(p34 Y))/\(~(p35 Y)))\/(((p35 Y)/\(p34 Y))\/(((~(p33 Y))/\(~(p34 Y)))\/(((p34 Y)/\(p33 Y))\/(((~(p32 Y))/\(~(p33 Y)))\/(((p33 Y)/\(p32 Y))\/(((~(p31 Y))/\(~(p32 Y)))\/(((p32 Y)/\(p31 Y))\/(((~(p30 Y))/\(~(p31 Y)))\/(((p31 Y)/\(p30 Y))\/(((~(p29 Y))/\(~(p30 Y)))\/(((p30 Y)/\(p29 Y))\/(((~(p28 Y))/\(~(p29 Y)))\/(((p29 Y)/\(p28 Y))\/(((~(p27 Y))/\(~(p28 Y)))\/(((p28 Y)/\(p27 Y))\/(((~(p26 Y))/\(~(p27 Y)))\/(((p27 Y)/\(p26 Y))\/(((~(p25 Y))/\(~(p26 Y)))\/(((p26 Y)/\(p25 Y))\/(((~(p24 Y))/\(~(p25 Y)))\/(((p25 Y)/\(p24 Y))\/(((~(p23 Y))/\(~(p24 Y)))\/(((p24 Y)/\(p23 Y))\/(((~(p22 Y))/\(~(p23 Y)))\/(((p23 Y)/\(p22 Y))\/(((~(p21 Y))/\(~(p22 Y)))\/(((p22 Y)/\(p21 Y))\/(((~(p20 Y))/\(~(p21 Y)))\/(((p21 Y)/\(p20 Y))\/(((~(p19 Y))/\(~(p20 Y)))\/(((p20 Y)/\(p19 Y))\/(((~(p18 Y))/\(~(p19 Y)))\/(((p19 Y)/\(p18 Y))\/(((~(p17 Y))/\(~(p18 Y)))\/(((p18 Y)/\(p17 Y))\/(((~(p16 Y))/\(~(p17 Y)))\/(((p17 Y)/\(p16 Y))\/(((~(p15 Y))/\(~(p16 Y)))\/(((p16 Y)/\(p15 Y))\/(((~(p14 Y))/\(~(p15 Y)))\/(((p15 Y)/\(p14 Y))\/(((~(p13 Y))/\(~(p14 Y)))\/(((p14 Y)/\(p13 Y))\/(((~(p12 Y))/\(~(p13 Y)))\/(((p13 Y)/\(p12 Y))\/(((~(p11 Y))/\(~(p12 Y)))\/(((p12 Y)/\(p11 Y))\/(((~(p10 Y))/\(~(p11 Y)))\/(((p11 Y)/\(p10 Y))\/(((~(p9 Y))/\(~(p10 Y)))\/(((p10 Y)/\(p9 Y))\/(((~(p8 Y))/\(~(p9 Y)))\/(((p9 Y)/\(p8 Y))\/(((~(p7 Y))/\(~(p8 Y)))\/(((p8 Y)/\(p7 Y))\/(((~(p6 Y))/\(~(p7 Y)))\/(((p7 Y)/\(p6 Y))\/(((~(p5 Y))/\(~(p6 Y)))\/(((p6 Y)/\(p5 Y))\/(((~(p4 Y))/\(~(p5 Y)))\/(((p5 Y)/\(p4 Y))\/(((~(p3 Y))/\(~(p4 Y)))\/(((p4 Y)/\(p3 Y))\/(((~(p2 Y))/\(~(p3 Y)))\/(((p3 Y)/\(p2 Y))\/(((~(p1 Y))/\(~(p2 Y)))\/((p2 Y)/\(p1 Y)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 1.88/2.14 Proof. % 1.88/2.14 assert (zenon_L1_ : forall (zenon_TY_f : zenon_U), (~(~(p2 zenon_TY_f))) -> (~(p2 zenon_TY_f)) -> False). % 1.88/2.14 do 1 intro. intros zenon_H3 zenon_H4. % 1.88/2.14 exact (zenon_H3 zenon_H4). % 1.88/2.14 (* end of lemma zenon_L1_ *) % 1.88/2.14 assert (zenon_L2_ : forall (zenon_TY_l : zenon_U) (zenon_TY_f : zenon_U), (~(~(p3 zenon_TY_f))) -> (~((~(p1 zenon_TY_f))/\(~(p2 zenon_TY_f)))) -> (forall Y : zenon_U, ((~(r1 zenon_TY_l Y))\/(~(((p2 Y)/\(~(p1 Y)))\/((~(p2 Y))/\(p1 Y)))))) -> (r1 zenon_TY_l zenon_TY_f) -> (~((p3 zenon_TY_f)/\(p2 zenon_TY_f))) -> False). % 1.88/2.14 do 2 intro. intros zenon_H6 zenon_H7 zenon_H8 zenon_H9 zenon_Ha. % 1.88/2.14 apply zenon_H6. zenon_intro zenon_Hc. % 1.88/2.14 apply (zenon_notand_s _ _ zenon_Ha); [ zenon_intro zenon_Hd | zenon_intro zenon_H4 ]. % 1.88/2.14 exact (zenon_Hd zenon_Hc). % 1.88/2.14 apply (zenon_notand_s _ _ zenon_H7); [ zenon_intro zenon_He | zenon_intro zenon_H3 ]. % 1.88/2.14 apply zenon_He. zenon_intro zenon_Hf. % 1.88/2.14 generalize (zenon_H8 zenon_TY_f). zenon_intro zenon_H10. % 1.88/2.14 apply (zenon_or_s _ _ zenon_H10); [ zenon_intro zenon_H12 | zenon_intro zenon_H11 ]. % 1.88/2.14 exact (zenon_H12 zenon_H9). % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H11). zenon_intro zenon_H14. zenon_intro zenon_H13. % 1.88/2.14 apply (zenon_notand_s _ _ zenon_H13); [ zenon_intro zenon_H3 | zenon_intro zenon_H15 ]. % 1.88/2.14 exact (zenon_H3 zenon_H4). % 1.88/2.14 exact (zenon_H15 zenon_Hf). % 1.88/2.14 exact (zenon_H3 zenon_H4). % 1.88/2.14 (* end of lemma zenon_L2_ *) % 1.88/2.14 apply NNPP. intro zenon_G. % 1.88/2.14 apply zenon_G. zenon_intro zenon_H16. % 1.88/2.14 elim zenon_H16. zenon_intro zenon_TX_x. zenon_intro zenon_H18. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H18). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 1.88/2.14 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((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))\/((forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/False))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p59 X)/\(~(p58 X)))\/((~(p59 X))/\(p58 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p58 Y)/\(~(p57 Y)))\/((~(p58 Y))/\(p57 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p57 X)/\(~(p56 X)))\/((~(p57 X))/\(p56 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p56 Y)/\(~(p55 Y)))\/((~(p56 Y))/\(p55 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p55 X)/\(~(p54 X)))\/((~(p55 X))/\(p54 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p54 Y)/\(~(p53 Y)))\/((~(p54 Y))/\(p53 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p53 X)/\(~(p52 X)))\/((~(p53 X))/\(p52 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p52 Y)/\(~(p51 Y)))\/((~(p52 Y))/\(p51 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p51 X)/\(~(p50 X)))\/((~(p51 X))/\(p50 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p50 Y)/\(~(p49 Y)))\/((~(p50 Y))/\(p49 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p49 X)/\(~(p48 X)))\/((~(p49 X))/\(p48 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p48 Y)/\(~(p47 Y)))\/((~(p48 Y))/\(p47 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p47 X)/\(~(p46 X)))\/((~(p47 X))/\(p46 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p46 Y)/\(~(p45 Y)))\/((~(p46 Y))/\(p45 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p45 X)/\(~(p44 X)))\/((~(p45 X))/\(p44 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p44 Y)/\(~(p43 Y)))\/((~(p44 Y))/\(p43 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p43 X)/\(~(p42 X)))\/((~(p43 X))/\(p42 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p42 Y)/\(~(p41 Y)))\/((~(p42 Y))/\(p41 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p41 X)/\(~(p40 X)))\/((~(p41 X))/\(p40 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p40 Y)/\(~(p39 Y)))\/((~(p40 Y))/\(p39 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p39 X)/\(~(p38 X)))\/((~(p39 X))/\(p38 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p38 Y)/\(~(p37 Y)))\/((~(p38 Y))/\(p37 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p37 X)/\(~(p36 X)))\/((~(p37 X))/\(p36 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p36 Y)/\(~(p35 Y)))\/((~(p36 Y))/\(p35 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p35 X)/\(~(p34 X)))\/((~(p35 X))/\(p34 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p34 Y)/\(~(p33 Y)))\/((~(p34 Y))/\(p33 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p33 X)/\(~(p32 X)))\/((~(p33 X))/\(p32 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p32 Y)/\(~(p31 Y)))\/((~(p32 Y))/\(p31 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p31 X)/\(~(p30 X)))\/((~(p31 X))/\(p30 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p30 Y)/\(~(p29 Y)))\/((~(p30 Y))/\(p29 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p29 X)/\(~(p28 X)))\/((~(p29 X))/\(p28 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p28 Y)/\(~(p27 Y)))\/((~(p28 Y))/\(p27 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p27 X)/\(~(p26 X)))\/((~(p27 X))/\(p26 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p26 Y)/\(~(p25 Y)))\/((~(p26 Y))/\(p25 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p25 X)/\(~(p24 X)))\/((~(p25 X))/\(p24 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p24 Y)/\(~(p23 Y)))\/((~(p24 Y))/\(p23 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p23 X)/\(~(p22 X)))\/((~(p23 X))/\(p22 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p22 Y)/\(~(p21 Y)))\/((~(p22 Y))/\(p21 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p21 X)/\(~(p20 X)))\/((~(p21 X))/\(p20 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p20 Y)/\(~(p19 Y)))\/((~(p20 Y))/\(p19 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p19 X)/\(~(p18 X)))\/((~(p19 X))/\(p18 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p18 Y)/\(~(p17 Y)))\/((~(p18 Y))/\(p17 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p17 X)/\(~(p16 X)))\/((~(p17 X))/\(p16 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p16 Y)/\(~(p15 Y)))\/((~(p16 Y))/\(p15 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p15 X)/\(~(p14 X)))\/((~(p15 X))/\(p14 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p14 Y)/\(~(p13 Y)))\/((~(p14 Y))/\(p13 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p13 X)/\(~(p12 X)))\/((~(p13 X))/\(p12 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p12 Y)/\(~(p11 Y)))\/((~(p12 Y))/\(p11 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p11 X)/\(~(p10 X)))\/((~(p11 X))/\(p10 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p10 Y)/\(~(p9 Y)))\/((~(p10 Y))/\(p9 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p9 X)/\(~(p8 X)))\/((~(p9 X))/\(p8 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p8 Y)/\(~(p7 Y)))\/((~(p8 Y))/\(p7 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p7 X)/\(~(p6 X)))\/((~(p7 X))/\(p6 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p6 Y)/\(~(p5 Y)))\/((~(p6 Y))/\(p5 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p5 X)/\(~(p4 X)))\/((~(p5 X))/\(p4 X))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p4 Y)/\(~(p3 Y)))\/((~(p4 Y))/\(p3 Y))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/(~(((p3 X)/\(~(p2 X)))\/((~(p3 X))/\(p2 X))))))))))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/(~(((p2 Y)/\(~(p1 Y)))\/((~(p2 Y))/\(p1 Y)))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p60 Y)))\/(forall Y : zenon_U, ((~(r1 X Y))\/(((~(p58 Y))/\(~(p59 Y)))\/(((p59 Y)/\(p58 Y))\/(((~(p57 Y))/\(~(p58 Y)))\/(((p58 Y)/\(p57 Y))\/(((~(p56 Y))/\(~(p57 Y)))\/(((p57 Y)/\(p56 Y))\/(((~(p55 Y))/\(~(p56 Y)))\/(((p56 Y)/\(p55 Y))\/(((~(p54 Y))/\(~(p55 Y)))\/(((p55 Y)/\(p54 Y))\/(((~(p53 Y))/\(~(p54 Y)))\/(((p54 Y)/\(p53 Y))\/(((~(p52 Y))/\(~(p53 Y)))\/(((p53 Y)/\(p52 Y))\/(((~(p51 Y))/\(~(p52 Y)))\/(((p52 Y)/\(p51 Y))\/(((~(p50 Y))/\(~(p51 Y)))\/(((p51 Y)/\(p50 Y))\/(((~(p49 Y))/\(~(p50 Y)))\/(((p50 Y)/\(p49 Y))\/(((~(p48 Y))/\(~(p49 Y)))\/(((p49 Y)/\(p48 Y))\/(((~(p47 Y))/\(~(p48 Y)))\/(((p48 Y)/\(p47 Y))\/(((~(p46 Y))/\(~(p47 Y)))\/(((p47 Y)/\(p46 Y))\/(((~(p45 Y))/\(~(p46 Y)))\/(((p46 Y)/\(p45 Y))\/(((~(p44 Y))/\(~(p45 Y)))\/(((p45 Y)/\(p44 Y))\/(((~(p43 Y))/\(~(p44 Y)))\/(((p44 Y)/\(p43 Y))\/(((~(p42 Y))/\(~(p43 Y)))\/(((p43 Y)/\(p42 Y))\/(((~(p41 Y))/\(~(p42 Y)))\/(((p42 Y)/\(p41 Y))\/(((~(p40 Y))/\(~(p41 Y)))\/(((p41 Y)/\(p40 Y))\/(((~(p39 Y))/\(~(p40 Y)))\/(((p40 Y)/\(p39 Y))\/(((~(p38 Y))/\(~(p39 Y)))\/(((p39 Y)/\(p38 Y))\/(((~(p37 Y))/\(~(p38 Y)))\/(((p38 Y)/\(p37 Y))\/(((~(p36 Y))/\(~(p37 Y)))\/(((p37 Y)/\(p36 Y))\/(((~(p35 Y))/\(~(p36 Y)))\/(((p36 Y)/\(p35 Y))\/(((~(p34 Y))/\(~(p35 Y)))\/(((p35 Y)/\(p34 Y))\/(((~(p33 Y))/\(~(p34 Y)))\/(((p34 Y)/\(p33 Y))\/(((~(p32 Y))/\(~(p33 Y)))\/(((p33 Y)/\(p32 Y))\/(((~(p31 Y))/\(~(p32 Y)))\/(((p32 Y)/\(p31 Y))\/(((~(p30 Y))/\(~(p31 Y)))\/(((p31 Y)/\(p30 Y))\/(((~(p29 Y))/\(~(p30 Y)))\/(((p30 Y)/\(p29 Y))\/(((~(p28 Y))/\(~(p29 Y)))\/(((p29 Y)/\(p28 Y))\/(((~(p27 Y))/\(~(p28 Y)))\/(((p28 Y)/\(p27 Y))\/(((~(p26 Y))/\(~(p27 Y)))\/(((p27 Y)/\(p26 Y))\/(((~(p25 Y))/\(~(p26 Y)))\/(((p26 Y)/\(p25 Y))\/(((~(p24 Y))/\(~(p25 Y)))\/(((p25 Y)/\(p24 Y))\/(((~(p23 Y))/\(~(p24 Y)))\/(((p24 Y)/\(p23 Y))\/(((~(p22 Y))/\(~(p23 Y)))\/(((p23 Y)/\(p22 Y))\/(((~(p21 Y))/\(~(p22 Y)))\/(((p22 Y)/\(p21 Y))\/(((~(p20 Y))/\(~(p21 Y)))\/(((p21 Y)/\(p20 Y))\/(((~(p19 Y))/\(~(p20 Y)))\/(((p20 Y)/\(p19 Y))\/(((~(p18 Y))/\(~(p19 Y)))\/(((p19 Y)/\(p18 Y))\/(((~(p17 Y))/\(~(p18 Y)))\/(((p18 Y)/\(p17 Y))\/(((~(p16 Y))/\(~(p17 Y)))\/(((p17 Y)/\(p16 Y))\/(((~(p15 Y))/\(~(p16 Y)))\/(((p16 Y)/\(p15 Y))\/(((~(p14 Y))/\(~(p15 Y)))\/(((p15 Y)/\(p14 Y))\/(((~(p13 Y))/\(~(p14 Y)))\/(((p14 Y)/\(p13 Y))\/(((~(p12 Y))/\(~(p13 Y)))\/(((p13 Y)/\(p12 Y))\/(((~(p11 Y))/\(~(p12 Y)))\/(((p12 Y)/\(p11 Y))\/(((~(p10 Y))/\(~(p11 Y)))\/(((p11 Y)/\(p10 Y))\/(((~(p9 Y))/\(~(p10 Y)))\/(((p10 Y)/\(p9 Y))\/(((~(p8 Y))/\(~(p9 Y)))\/(((p9 Y)/\(p8 Y))\/(((~(p7 Y))/\(~(p8 Y)))\/(((p8 Y)/\(p7 Y))\/(((~(p6 Y))/\(~(p7 Y)))\/(((p7 Y)/\(p6 Y))\/(((~(p5 Y))/\(~(p6 Y)))\/(((p6 Y)/\(p5 Y))\/(((~(p4 Y))/\(~(p5 Y)))\/(((p5 Y)/\(p4 Y))\/(((~(p3 Y))/\(~(p4 Y)))\/(((p4 Y)/\(p3 Y))\/(((~(p2 Y))/\(~(p3 Y)))\/(((p3 Y)/\(p2 Y))\/(((~(p1 Y))/\(~(p2 Y)))\/((p2 Y)/\(p1 Y)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zenon_H19); [ zenon_intro zenon_H1b; idtac ]. % 1.88/2.14 elim zenon_H1b. zenon_intro zenon_TY_l. zenon_intro zenon_H1c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H1c). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 1.88/2.14 apply zenon_H1d. zenon_intro zenon_H1f. % 1.88/2.14 generalize (zenon_H1f zenon_TY_l). zenon_intro zenon_H20. % 1.88/2.14 apply (zenon_or_s _ _ zenon_H20); [ zenon_intro zenon_H22 | zenon_intro zenon_H21 ]. % 1.88/2.14 generalize (reflexivity zenon_TY_l). zenon_intro zenon_H23. % 1.88/2.14 exact (zenon_H22 zenon_H23). % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H24). zenon_intro zenon_H27. zenon_intro zenon_H26. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 1.88/2.14 apply zenon_H27. zenon_intro zenon_H8. % 1.88/2.14 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TY_l Y))\/(((~(p58 Y))/\(~(p59 Y)))\/(((p59 Y)/\(p58 Y))\/(((~(p57 Y))/\(~(p58 Y)))\/(((p58 Y)/\(p57 Y))\/(((~(p56 Y))/\(~(p57 Y)))\/(((p57 Y)/\(p56 Y))\/(((~(p55 Y))/\(~(p56 Y)))\/(((p56 Y)/\(p55 Y))\/(((~(p54 Y))/\(~(p55 Y)))\/(((p55 Y)/\(p54 Y))\/(((~(p53 Y))/\(~(p54 Y)))\/(((p54 Y)/\(p53 Y))\/(((~(p52 Y))/\(~(p53 Y)))\/(((p53 Y)/\(p52 Y))\/(((~(p51 Y))/\(~(p52 Y)))\/(((p52 Y)/\(p51 Y))\/(((~(p50 Y))/\(~(p51 Y)))\/(((p51 Y)/\(p50 Y))\/(((~(p49 Y))/\(~(p50 Y)))\/(((p50 Y)/\(p49 Y))\/(((~(p48 Y))/\(~(p49 Y)))\/(((p49 Y)/\(p48 Y))\/(((~(p47 Y))/\(~(p48 Y)))\/(((p48 Y)/\(p47 Y))\/(((~(p46 Y))/\(~(p47 Y)))\/(((p47 Y)/\(p46 Y))\/(((~(p45 Y))/\(~(p46 Y)))\/(((p46 Y)/\(p45 Y))\/(((~(p44 Y))/\(~(p45 Y)))\/(((p45 Y)/\(p44 Y))\/(((~(p43 Y))/\(~(p44 Y)))\/(((p44 Y)/\(p43 Y))\/(((~(p42 Y))/\(~(p43 Y)))\/(((p43 Y)/\(p42 Y))\/(((~(p41 Y))/\(~(p42 Y)))\/(((p42 Y)/\(p41 Y))\/(((~(p40 Y))/\(~(p41 Y)))\/(((p41 Y)/\(p40 Y))\/(((~(p39 Y))/\(~(p40 Y)))\/(((p40 Y)/\(p39 Y))\/(((~(p38 Y))/\(~(p39 Y)))\/(((p39 Y)/\(p38 Y))\/(((~(p37 Y))/\(~(p38 Y)))\/(((p38 Y)/\(p37 Y))\/(((~(p36 Y))/\(~(p37 Y)))\/(((p37 Y)/\(p36 Y))\/(((~(p35 Y))/\(~(p36 Y)))\/(((p36 Y)/\(p35 Y))\/(((~(p34 Y))/\(~(p35 Y)))\/(((p35 Y)/\(p34 Y))\/(((~(p33 Y))/\(~(p34 Y)))\/(((p34 Y)/\(p33 Y))\/(((~(p32 Y))/\(~(p33 Y)))\/(((p33 Y)/\(p32 Y))\/(((~(p31 Y))/\(~(p32 Y)))\/(((p32 Y)/\(p31 Y))\/(((~(p30 Y))/\(~(p31 Y)))\/(((p31 Y)/\(p30 Y))\/(((~(p29 Y))/\(~(p30 Y)))\/(((p30 Y)/\(p29 Y))\/(((~(p28 Y))/\(~(p29 Y)))\/(((p29 Y)/\(p28 Y))\/(((~(p27 Y))/\(~(p28 Y)))\/(((p28 Y)/\(p27 Y))\/(((~(p26 Y))/\(~(p27 Y)))\/(((p27 Y)/\(p26 Y))\/(((~(p25 Y))/\(~(p26 Y)))\/(((p26 Y)/\(p25 Y))\/(((~(p24 Y))/\(~(p25 Y)))\/(((p25 Y)/\(p24 Y))\/(((~(p23 Y))/\(~(p24 Y)))\/(((p24 Y)/\(p23 Y))\/(((~(p22 Y))/\(~(p23 Y)))\/(((p23 Y)/\(p22 Y))\/(((~(p21 Y))/\(~(p22 Y)))\/(((p22 Y)/\(p21 Y))\/(((~(p20 Y))/\(~(p21 Y)))\/(((p21 Y)/\(p20 Y))\/(((~(p19 Y))/\(~(p20 Y)))\/(((p20 Y)/\(p19 Y))\/(((~(p18 Y))/\(~(p19 Y)))\/(((p19 Y)/\(p18 Y))\/(((~(p17 Y))/\(~(p18 Y)))\/(((p18 Y)/\(p17 Y))\/(((~(p16 Y))/\(~(p17 Y)))\/(((p17 Y)/\(p16 Y))\/(((~(p15 Y))/\(~(p16 Y)))\/(((p16 Y)/\(p15 Y))\/(((~(p14 Y))/\(~(p15 Y)))\/(((p15 Y)/\(p14 Y))\/(((~(p13 Y))/\(~(p14 Y)))\/(((p14 Y)/\(p13 Y))\/(((~(p12 Y))/\(~(p13 Y)))\/(((p13 Y)/\(p12 Y))\/(((~(p11 Y))/\(~(p12 Y)))\/(((p12 Y)/\(p11 Y))\/(((~(p10 Y))/\(~(p11 Y)))\/(((p11 Y)/\(p10 Y))\/(((~(p9 Y))/\(~(p10 Y)))\/(((p10 Y)/\(p9 Y))\/(((~(p8 Y))/\(~(p9 Y)))\/(((p9 Y)/\(p8 Y))\/(((~(p7 Y))/\(~(p8 Y)))\/(((p8 Y)/\(p7 Y))\/(((~(p6 Y))/\(~(p7 Y)))\/(((p7 Y)/\(p6 Y))\/(((~(p5 Y))/\(~(p6 Y)))\/(((p6 Y)/\(p5 Y))\/(((~(p4 Y))/\(~(p5 Y)))\/(((p5 Y)/\(p4 Y))\/(((~(p3 Y))/\(~(p4 Y)))\/(((p4 Y)/\(p3 Y))\/(((~(p2 Y))/\(~(p3 Y)))\/(((p3 Y)/\(p2 Y))\/(((~(p1 Y))/\(~(p2 Y)))\/((p2 Y)/\(p1 Y))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zenon_H28); [ zenon_intro zenon_H2a; idtac ]. % 1.88/2.14 elim zenon_H2a. zenon_intro zenon_TY_f. zenon_intro zenon_H2b. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H2b). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H2e). zenon_intro zenon_H31. zenon_intro zenon_H30. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H38). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H42). zenon_intro zenon_H45. zenon_intro zenon_H44. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H46). zenon_intro zenon_H49. zenon_intro zenon_H48. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H4c). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H4e). zenon_intro zenon_H51. zenon_intro zenon_H50. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H50). zenon_intro zenon_H53. zenon_intro zenon_H52. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H52). zenon_intro zenon_H55. zenon_intro zenon_H54. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H54). zenon_intro zenon_H57. zenon_intro zenon_H56. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H58). zenon_intro zenon_H5b. zenon_intro zenon_H5a. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H5a). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H5c). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H5e). zenon_intro zenon_H61. zenon_intro zenon_H60. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H60). zenon_intro zenon_H63. zenon_intro zenon_H62. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H62). zenon_intro zenon_H65. zenon_intro zenon_H64. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H64). zenon_intro zenon_H67. zenon_intro zenon_H66. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H66). zenon_intro zenon_H69. zenon_intro zenon_H68. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H68). zenon_intro zenon_H6b. zenon_intro zenon_H6a. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H6a). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H6c). zenon_intro zenon_H6f. zenon_intro zenon_H6e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H6e). zenon_intro zenon_H71. zenon_intro zenon_H70. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H70). zenon_intro zenon_H73. zenon_intro zenon_H72. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H72). zenon_intro zenon_H75. zenon_intro zenon_H74. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H74). zenon_intro zenon_H77. zenon_intro zenon_H76. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H76). zenon_intro zenon_H79. zenon_intro zenon_H78. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H7a). zenon_intro zenon_H7d. zenon_intro zenon_H7c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H7c). zenon_intro zenon_H7f. zenon_intro zenon_H7e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H7e). zenon_intro zenon_H81. zenon_intro zenon_H80. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H82). zenon_intro zenon_H85. zenon_intro zenon_H84. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H84). zenon_intro zenon_H87. zenon_intro zenon_H86. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H86). zenon_intro zenon_H89. zenon_intro zenon_H88. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H88). zenon_intro zenon_H8b. zenon_intro zenon_H8a. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H8a). zenon_intro zenon_H8d. zenon_intro zenon_H8c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H8c). zenon_intro zenon_H8f. zenon_intro zenon_H8e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H8e). zenon_intro zenon_H91. zenon_intro zenon_H90. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H90). zenon_intro zenon_H93. zenon_intro zenon_H92. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H92). zenon_intro zenon_H95. zenon_intro zenon_H94. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H94). zenon_intro zenon_H97. zenon_intro zenon_H96. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H96). zenon_intro zenon_H99. zenon_intro zenon_H98. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H98). zenon_intro zenon_H9b. zenon_intro zenon_H9a. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H9a). zenon_intro zenon_H9d. zenon_intro zenon_H9c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H9c). zenon_intro zenon_H9f. zenon_intro zenon_H9e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H9e). zenon_intro zenon_Ha1. zenon_intro zenon_Ha0. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Ha0). zenon_intro zenon_Ha3. zenon_intro zenon_Ha2. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Ha2). zenon_intro zenon_Ha5. zenon_intro zenon_Ha4. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Ha4). zenon_intro zenon_Ha7. zenon_intro zenon_Ha6. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Ha6). zenon_intro zenon_Ha9. zenon_intro zenon_Ha8. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Ha8). zenon_intro zenon_Hab. zenon_intro zenon_Haa. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Haa). zenon_intro zenon_Had. zenon_intro zenon_Hac. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hac). zenon_intro zenon_Haf. zenon_intro zenon_Hae. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hae). zenon_intro zenon_Hb1. zenon_intro zenon_Hb0. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hb0). zenon_intro zenon_Hb3. zenon_intro zenon_Hb2. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hb2). zenon_intro zenon_Hb5. zenon_intro zenon_Hb4. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hb4). zenon_intro zenon_Hb7. zenon_intro zenon_Hb6. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hb6). zenon_intro zenon_Hb9. zenon_intro zenon_Hb8. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hb8). zenon_intro zenon_Hbb. zenon_intro zenon_Hba. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hba). zenon_intro zenon_Hbd. zenon_intro zenon_Hbc. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hbc). zenon_intro zenon_Hbf. zenon_intro zenon_Hbe. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hbe). zenon_intro zenon_Hc1. zenon_intro zenon_Hc0. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hc0). zenon_intro zenon_Hc3. zenon_intro zenon_Hc2. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hc2). zenon_intro zenon_Hc5. zenon_intro zenon_Hc4. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hc4). zenon_intro zenon_Hc7. zenon_intro zenon_Hc6. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hc6). zenon_intro zenon_Hc9. zenon_intro zenon_Hc8. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hc8). zenon_intro zenon_Hcb. zenon_intro zenon_Hca. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hca). zenon_intro zenon_Hcd. zenon_intro zenon_Hcc. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hcc). zenon_intro zenon_Hcf. zenon_intro zenon_Hce. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hce). zenon_intro zenon_Hd1. zenon_intro zenon_Hd0. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hd0). zenon_intro zenon_Hd3. zenon_intro zenon_Hd2. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hd2). zenon_intro zenon_Hd5. zenon_intro zenon_Hd4. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hd4). zenon_intro zenon_Hd7. zenon_intro zenon_Hd6. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hd6). zenon_intro zenon_Hd9. zenon_intro zenon_Hd8. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hd8). zenon_intro zenon_Hdb. zenon_intro zenon_Hda. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hda). zenon_intro zenon_Hdd. zenon_intro zenon_Hdc. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hdc). zenon_intro zenon_Hdf. zenon_intro zenon_Hde. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hde). zenon_intro zenon_He1. zenon_intro zenon_He0. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_He0). zenon_intro zenon_He3. zenon_intro zenon_He2. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_He2). zenon_intro zenon_He5. zenon_intro zenon_He4. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_He4). zenon_intro zenon_He7. zenon_intro zenon_He6. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_He6). zenon_intro zenon_He9. zenon_intro zenon_He8. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_He8). zenon_intro zenon_Heb. zenon_intro zenon_Hea. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hea). zenon_intro zenon_Hed. zenon_intro zenon_Hec. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hec). zenon_intro zenon_Hef. zenon_intro zenon_Hee. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hee). zenon_intro zenon_Hf1. zenon_intro zenon_Hf0. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hf0). zenon_intro zenon_Hf3. zenon_intro zenon_Hf2. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hf2). zenon_intro zenon_Hf5. zenon_intro zenon_Hf4. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hf4). zenon_intro zenon_Hf7. zenon_intro zenon_Hf6. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hf6). zenon_intro zenon_Hf9. zenon_intro zenon_Hf8. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hf8). zenon_intro zenon_Hfb. zenon_intro zenon_Hfa. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hfa). zenon_intro zenon_Hfd. zenon_intro zenon_Hfc. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hfc). zenon_intro zenon_Hff. zenon_intro zenon_Hfe. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_Hfe). zenon_intro zenon_H101. zenon_intro zenon_H100. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H100). zenon_intro zenon_H103. zenon_intro zenon_H102. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H102). zenon_intro zenon_H105. zenon_intro zenon_H104. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H104). zenon_intro zenon_H107. zenon_intro zenon_H106. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H106). zenon_intro zenon_H109. zenon_intro zenon_H108. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H108). zenon_intro zenon_H10b. zenon_intro zenon_H10a. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H10a). zenon_intro zenon_H10d. zenon_intro zenon_H10c. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H10c). zenon_intro zenon_H10f. zenon_intro zenon_H10e. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H10e). zenon_intro zenon_Ha. zenon_intro zenon_H110. % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H110). zenon_intro zenon_H7. zenon_intro zenon_H111. % 1.88/2.14 apply zenon_H2d. zenon_intro zenon_H9. % 1.88/2.14 apply (zenon_notand_s _ _ zenon_H10f); [ zenon_intro zenon_H3 | zenon_intro zenon_H6 ]. % 1.88/2.14 apply zenon_H3. zenon_intro zenon_H112. % 1.88/2.14 apply (zenon_notand_s _ _ zenon_H111); [ zenon_intro zenon_H4 | zenon_intro zenon_H15 ]. % 1.88/2.14 exact (zenon_H4 zenon_H112). % 1.88/2.14 generalize (zenon_H8 zenon_TY_f). zenon_intro zenon_H10. % 1.88/2.14 apply (zenon_or_s _ _ zenon_H10); [ zenon_intro zenon_H12 | zenon_intro zenon_H11 ]. % 1.88/2.14 exact (zenon_H12 zenon_H9). % 1.88/2.14 apply (zenon_notor_s _ _ zenon_H11). zenon_intro zenon_H14. zenon_intro zenon_H13. % 1.88/2.14 apply (zenon_notand_s _ _ zenon_H14); [ zenon_intro zenon_H4 | zenon_intro zenon_He ]. % 1.88/2.15 exact (zenon_H4 zenon_H112). % 1.88/2.15 exact (zenon_He zenon_H15). % 1.88/2.15 apply (zenon_L2_ zenon_TY_l zenon_TY_f); trivial. % 1.88/2.15 Qed. % 1.88/2.15 % SZS output end Proof % 1.88/2.15 (* END-PROOF *) % 1.88/2.15 nodes searched: 19648 % 1.88/2.15 max branch formulas: 8895 % 1.88/2.15 proof nodes created: 1665 % 1.88/2.15 formulas created: 413960 % 1.88/2.15 %------------------------------------------------------------------------------