%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n026.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 0.64s 0.94s % Output : Proof 0.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.07/0.34 % Computer : n026.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Sat Sep 5 16:27:11 UTC 2026 % 0.07/0.34 % CPUTime : % 0.64/0.94 (* PROOF-FOUND *) % 0.64/0.94 % SZS status Theorem % 0.64/0.94 (* BEGIN-PROOF *) % 0.64/0.94 % SZS output start Proof % 0.64/0.94 Theorem main : (~(exists X : zenon_U, (~((forall Y : zenon_U, ((~(r1 X Y))\/((~(p30 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))\/False))\/(~(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))\/(p30 Y)))\/(forall Y : zenon_U, ((~(r1 X 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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 0.64/0.94 Proof. % 0.64/0.94 assert (zenon_L1_ : forall (zenon_TY_f : zenon_U), (~(~(p2 zenon_TY_f))) -> (~(p2 zenon_TY_f)) -> False). % 0.64/0.94 do 1 intro. intros zenon_H3 zenon_H4. % 0.64/0.94 exact (zenon_H3 zenon_H4). % 0.64/0.94 (* end of lemma zenon_L1_ *) % 0.64/0.94 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). % 0.64/0.94 do 2 intro. intros zenon_H6 zenon_H7 zenon_H8 zenon_H9 zenon_Ha. % 0.64/0.94 apply zenon_H6. zenon_intro zenon_Hc. % 0.64/0.94 apply (zenon_notand_s _ _ zenon_Ha); [ zenon_intro zenon_Hd | zenon_intro zenon_H4 ]. % 0.64/0.94 exact (zenon_Hd zenon_Hc). % 0.64/0.94 apply (zenon_notand_s _ _ zenon_H7); [ zenon_intro zenon_He | zenon_intro zenon_H3 ]. % 0.64/0.94 apply zenon_He. zenon_intro zenon_Hf. % 0.64/0.94 generalize (zenon_H8 zenon_TY_f). zenon_intro zenon_H10. % 0.64/0.94 apply (zenon_or_s _ _ zenon_H10); [ zenon_intro zenon_H12 | zenon_intro zenon_H11 ]. % 0.64/0.94 exact (zenon_H12 zenon_H9). % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H11). zenon_intro zenon_H14. zenon_intro zenon_H13. % 0.64/0.94 apply (zenon_notand_s _ _ zenon_H13); [ zenon_intro zenon_H3 | zenon_intro zenon_H15 ]. % 0.64/0.94 exact (zenon_H3 zenon_H4). % 0.64/0.94 exact (zenon_H15 zenon_Hf). % 0.64/0.94 exact (zenon_H3 zenon_H4). % 0.64/0.94 (* end of lemma zenon_L2_ *) % 0.64/0.94 apply NNPP. intro zenon_G. % 0.64/0.94 apply zenon_G. zenon_intro zenon_H16. % 0.64/0.94 elim zenon_H16. zenon_intro zenon_TX_x. zenon_intro zenon_H18. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H18). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 0.64/0.94 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))\/False))\/(~(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))\/(p30 Y)))\/(forall Y : zenon_U, ((~(r1 X 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 ]. % 0.64/0.94 elim zenon_H1b. zenon_intro zenon_TY_l. zenon_intro zenon_H1c. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H1c). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 0.64/0.94 apply zenon_H1d. zenon_intro zenon_H1f. % 0.64/0.94 generalize (zenon_H1f zenon_TY_l). zenon_intro zenon_H20. % 0.64/0.94 apply (zenon_or_s _ _ zenon_H20); [ zenon_intro zenon_H22 | zenon_intro zenon_H21 ]. % 0.64/0.94 generalize (reflexivity zenon_TY_l). zenon_intro zenon_H23. % 0.64/0.94 exact (zenon_H22 zenon_H23). % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H21). zenon_intro zenon_H25. zenon_intro zenon_H24. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H24). zenon_intro zenon_H27. zenon_intro zenon_H26. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 0.64/0.94 apply zenon_H27. zenon_intro zenon_H8. % 0.64/0.94 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TY_l 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 ]. % 0.64/0.94 elim zenon_H2a. zenon_intro zenon_TY_f. zenon_intro zenon_H2b. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H2b). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H2e). zenon_intro zenon_H31. zenon_intro zenon_H30. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H38). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H42). zenon_intro zenon_H45. zenon_intro zenon_H44. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H46). zenon_intro zenon_H49. zenon_intro zenon_H48. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H4c). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H4e). zenon_intro zenon_H51. zenon_intro zenon_H50. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H50). zenon_intro zenon_H53. zenon_intro zenon_H52. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H52). zenon_intro zenon_H55. zenon_intro zenon_H54. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H54). zenon_intro zenon_H57. zenon_intro zenon_H56. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H58). zenon_intro zenon_H5b. zenon_intro zenon_H5a. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H5a). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H5c). zenon_intro zenon_H5f. zenon_intro zenon_H5e. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H5e). zenon_intro zenon_H61. zenon_intro zenon_H60. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H60). zenon_intro zenon_H63. zenon_intro zenon_H62. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H62). zenon_intro zenon_H65. zenon_intro zenon_H64. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H64). zenon_intro zenon_H67. zenon_intro zenon_H66. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H66). zenon_intro zenon_H69. zenon_intro zenon_H68. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H68). zenon_intro zenon_H6b. zenon_intro zenon_H6a. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H6a). zenon_intro zenon_H6d. zenon_intro zenon_H6c. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H6c). zenon_intro zenon_H6f. zenon_intro zenon_H6e. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H6e). zenon_intro zenon_H71. zenon_intro zenon_H70. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H70). zenon_intro zenon_H73. zenon_intro zenon_H72. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H72). zenon_intro zenon_H75. zenon_intro zenon_H74. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H74). zenon_intro zenon_H77. zenon_intro zenon_H76. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H76). zenon_intro zenon_H79. zenon_intro zenon_H78. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H78). zenon_intro zenon_H7b. zenon_intro zenon_H7a. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H7a). zenon_intro zenon_H7d. zenon_intro zenon_H7c. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H7c). zenon_intro zenon_H7f. zenon_intro zenon_H7e. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H7e). zenon_intro zenon_H81. zenon_intro zenon_H80. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H82). zenon_intro zenon_H85. zenon_intro zenon_H84. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H84). zenon_intro zenon_H87. zenon_intro zenon_H86. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H86). zenon_intro zenon_H89. zenon_intro zenon_H88. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H88). zenon_intro zenon_H8b. zenon_intro zenon_H8a. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H8a). zenon_intro zenon_H8d. zenon_intro zenon_H8c. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H8c). zenon_intro zenon_H8f. zenon_intro zenon_H8e. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H8e). zenon_intro zenon_H91. zenon_intro zenon_H90. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H90). zenon_intro zenon_H93. zenon_intro zenon_H92. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H92). zenon_intro zenon_H95. zenon_intro zenon_H94. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H94). zenon_intro zenon_H97. zenon_intro zenon_H96. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H96). zenon_intro zenon_Ha. zenon_intro zenon_H98. % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H98). zenon_intro zenon_H7. zenon_intro zenon_H99. % 0.64/0.94 apply zenon_H2d. zenon_intro zenon_H9. % 0.64/0.94 apply (zenon_notand_s _ _ zenon_H97); [ zenon_intro zenon_H3 | zenon_intro zenon_H6 ]. % 0.64/0.94 apply zenon_H3. zenon_intro zenon_H9a. % 0.64/0.94 apply (zenon_notand_s _ _ zenon_H99); [ zenon_intro zenon_H4 | zenon_intro zenon_H15 ]. % 0.64/0.94 exact (zenon_H4 zenon_H9a). % 0.64/0.94 generalize (zenon_H8 zenon_TY_f). zenon_intro zenon_H10. % 0.64/0.94 apply (zenon_or_s _ _ zenon_H10); [ zenon_intro zenon_H12 | zenon_intro zenon_H11 ]. % 0.64/0.94 exact (zenon_H12 zenon_H9). % 0.64/0.94 apply (zenon_notor_s _ _ zenon_H11). zenon_intro zenon_H14. zenon_intro zenon_H13. % 0.64/0.94 apply (zenon_notand_s _ _ zenon_H14); [ zenon_intro zenon_H4 | zenon_intro zenon_He ]. % 0.64/0.94 exact (zenon_H4 zenon_H9a). % 0.64/0.94 exact (zenon_He zenon_H15). % 0.64/0.94 apply (zenon_L2_ zenon_TY_l zenon_TY_f); trivial. % 0.64/0.94 Qed. % 0.64/0.94 % SZS output end Proof % 0.64/0.94 (* END-PROOF *) % 0.64/0.94 nodes searched: 6609 % 0.64/0.94 max branch formulas: 2738 % 0.64/0.94 proof nodes created: 717 % 0.64/0.94 formulas created: 54429 % 0.64/0.94 %------------------------------------------------------------------------------