%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n027.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:37 PM UTC 2026 % Result : Theorem 159.03s 159.36s % Output : Proof 159.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.10/0.35 % Computer : n027.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Sat Sep 5 17:28:28 UTC 2026 % 0.10/0.35 % CPUTime : % 159.03/159.36 (* PROOF-FOUND *) % 159.03/159.36 % SZS status Theorem % 159.03/159.36 (* BEGIN-PROOF *) % 159.03/159.36 % SZS output start Proof % 159.03/159.36 Theorem main : (~(exists X : zenon_U, (~((~(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 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))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y)))))))))))))))))))))))))))))/\((~(p101 X))/\(p100 X)))))))). % 159.03/159.36 Proof. % 159.03/159.36 assert (zenon_L1_ : forall (zenon_TX_e : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_e Y))\/(p3 Y))) -> (~(p3 zenon_TX_e)) -> False). % 159.03/159.36 do 1 intro. intros zenon_H2 zenon_H3. % 159.03/159.36 generalize (zenon_H2 zenon_TX_e). zenon_intro zenon_H5. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H5); [ zenon_intro zenon_H7 | zenon_intro zenon_H6 ]. % 159.03/159.36 generalize (reflexivity zenon_TX_e). zenon_intro zenon_H8. % 159.03/159.36 exact (zenon_H7 zenon_H8). % 159.03/159.36 exact (zenon_H3 zenon_H6). % 159.03/159.36 (* end of lemma zenon_L1_ *) % 159.03/159.36 assert (zenon_L2_ : forall (zenon_TX_e : zenon_U) (zenon_TX_l : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))) -> (r1 zenon_TX_l zenon_TX_e) -> (~(p3 zenon_TX_e)) -> False). % 159.03/159.36 do 2 intro. intros zenon_H9 zenon_Ha zenon_H3. % 159.03/159.36 generalize (zenon_H9 zenon_TX_e). zenon_intro zenon_Hc. % 159.03/159.36 apply (zenon_or_s _ _ zenon_Hc); [ zenon_intro zenon_Hd | zenon_intro zenon_H2 ]. % 159.03/159.36 exact (zenon_Hd zenon_Ha). % 159.03/159.36 apply (zenon_L1_ zenon_TX_e); trivial. % 159.03/159.36 (* end of lemma zenon_L2_ *) % 159.03/159.36 assert (zenon_L3_ : forall (zenon_TX_e : zenon_U) (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_q Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (r1 zenon_TX_l zenon_TX_e) -> (~(p3 zenon_TX_e)) -> False). % 159.03/159.36 do 3 intro. intros zenon_He zenon_Hf zenon_Ha zenon_H3. % 159.03/159.36 generalize (zenon_He zenon_TX_l). zenon_intro zenon_H11. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H11); [ zenon_intro zenon_H12 | zenon_intro zenon_H9 ]. % 159.03/159.36 exact (zenon_H12 zenon_Hf). % 159.03/159.36 apply (zenon_L2_ zenon_TX_e zenon_TX_l); trivial. % 159.03/159.36 (* end of lemma zenon_L3_ *) % 159.03/159.36 assert (zenon_L4_ : forall (zenon_TX_q : zenon_U) (zenon_TX_l : zenon_U), ((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 zenon_TX_l))/\(p104 zenon_TX_l))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 zenon_TX_l))/\(p103 zenon_TX_l))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 zenon_TX_l))/\(p102 zenon_TX_l))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 zenon_TX_l))/\(p101 zenon_TX_l))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_l X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 zenon_TX_l))/\(p100 zenon_TX_l))))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 zenon_TX_l))))\/(~(p105 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 zenon_TX_l))))\/(~(p104 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 zenon_TX_l))))\/(~(p103 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 zenon_TX_l))))\/(~(p102 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 zenon_TX_l))))\/(~(p101 zenon_TX_l)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 zenon_TX_l))/\((forall X : zenon_U, ((~(r1 zenon_TX_l X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 zenon_TX_l))))\/(~(p100 zenon_TX_l)))/\(((p105 zenon_TX_l)\/(~(p106 zenon_TX_l)))/\(((p104 zenon_TX_l)\/(~(p105 zenon_TX_l)))/\(((p103 zenon_TX_l)\/(~(p104 zenon_TX_l)))/\(((p102 zenon_TX_l)\/(~(p103 zenon_TX_l)))/\(((p101 zenon_TX_l)\/(~(p102 zenon_TX_l)))/\((p100 zenon_TX_l)\/(~(p101 zenon_TX_l))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(p3 Y))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (~(p102 zenon_TX_l)) -> (p101 zenon_TX_l) -> False). % 159.03/159.36 do 2 intro. intros zenon_H13 zenon_H14 zenon_Hf zenon_H15 zenon_H16. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H13). zenon_intro zenon_H18. zenon_intro zenon_H17. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H17). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H19). zenon_intro zenon_H1c. zenon_intro zenon_H1b. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H1b). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H1e); [ zenon_intro zenon_H20 | zenon_intro zenon_H1f ]. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H20). zenon_intro zenon_H22. zenon_intro zenon_H21. % 159.03/159.36 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_l X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))) zenon_H22); [ zenon_intro zenon_H23; idtac ]. % 159.03/159.36 elim zenon_H23. zenon_intro zenon_TX_e. zenon_intro zenon_H24. % 159.03/159.36 apply (zenon_notor_s _ _ zenon_H24). zenon_intro zenon_H26. zenon_intro zenon_H25. % 159.03/159.36 apply zenon_H25. zenon_intro zenon_H27. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H27). zenon_intro zenon_H3. zenon_intro zenon_H28. % 159.03/159.36 apply zenon_H26. zenon_intro zenon_Ha. % 159.03/159.36 generalize (zenon_H14 zenon_TX_q). zenon_intro zenon_H29. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H29); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 generalize (zenon_H2a zenon_TX_q). zenon_intro zenon_H2d. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H2d); [ zenon_intro zenon_H2b | zenon_intro zenon_He ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 apply (zenon_L3_ zenon_TX_e zenon_TX_l zenon_TX_q); trivial. % 159.03/159.36 apply (zenon_notand_s _ _ zenon_H1f); [ zenon_intro zenon_H2f | zenon_intro zenon_H2e ]. % 159.03/159.36 exact (zenon_H2f zenon_H15). % 159.03/159.36 exact (zenon_H2e zenon_H16). % 159.03/159.36 (* end of lemma zenon_L4_ *) % 159.03/159.36 assert (zenon_L5_ : forall (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_q Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(p3 Y))))))))))) -> (~(p102 zenon_TX_l)) -> (p101 zenon_TX_l) -> False). % 159.03/159.36 do 2 intro. intros zenon_H30 zenon_Hf zenon_H14 zenon_H15 zenon_H16. % 159.03/159.36 generalize (zenon_H30 zenon_TX_l). zenon_intro zenon_H31. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H31); [ zenon_intro zenon_H12 | zenon_intro zenon_H13 ]. % 159.03/159.36 exact (zenon_H12 zenon_Hf). % 159.03/159.36 apply (zenon_L4_ zenon_TX_q zenon_TX_l); trivial. % 159.03/159.36 (* end of lemma zenon_L5_ *) % 159.03/159.36 assert (zenon_L6_ : forall (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(p3 Y))))))))))) -> (~(p102 zenon_TX_l)) -> (p101 zenon_TX_l) -> False). % 159.03/159.36 do 2 intro. intros zenon_H32 zenon_Hf zenon_H14 zenon_H15 zenon_H16. % 159.03/159.36 generalize (zenon_H32 zenon_TX_q). zenon_intro zenon_H33. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H33); [ zenon_intro zenon_H2b | zenon_intro zenon_H30 ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 apply (zenon_L5_ zenon_TX_l zenon_TX_q); trivial. % 159.03/159.36 (* end of lemma zenon_L6_ *) % 159.03/159.36 assert (zenon_L7_ : forall (zenon_TX_l : zenon_U) (zenon_TX_q : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_q Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))) -> (r1 zenon_TX_q zenon_TX_l) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(p3 Y))))))))))) -> (~(p102 zenon_TX_l)) -> (p101 zenon_TX_l) -> False). % 159.03/159.36 do 2 intro. intros zenon_H34 zenon_Hf zenon_H14 zenon_H15 zenon_H16. % 159.03/159.36 generalize (zenon_H34 zenon_TX_q). zenon_intro zenon_H35. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H35); [ zenon_intro zenon_H2b | zenon_intro zenon_H32 ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 apply (zenon_L6_ zenon_TX_l zenon_TX_q); trivial. % 159.03/159.36 (* end of lemma zenon_L7_ *) % 159.03/159.36 assert (zenon_L8_ : forall (zenon_TX_q : zenon_U), ((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 zenon_TX_q))/\(p104 zenon_TX_q))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 zenon_TX_q))/\(p103 zenon_TX_q))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 zenon_TX_q))/\(p102 zenon_TX_q))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 zenon_TX_q))/\(p101 zenon_TX_q))))/\((((~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 zenon_TX_q))/\(p100 zenon_TX_q))))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 zenon_TX_q))))\/(~(p105 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 zenon_TX_q))))\/(~(p104 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 zenon_TX_q))))\/(~(p103 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 zenon_TX_q))))\/(~(p102 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 zenon_TX_q))))\/(~(p101 zenon_TX_q)))/\(((((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 zenon_TX_q))/\((forall X : zenon_U, ((~(r1 zenon_TX_q X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 zenon_TX_q))))\/(~(p100 zenon_TX_q)))/\(((p105 zenon_TX_q)\/(~(p106 zenon_TX_q)))/\(((p104 zenon_TX_q)\/(~(p105 zenon_TX_q)))/\(((p103 zenon_TX_q)\/(~(p104 zenon_TX_q)))/\(((p102 zenon_TX_q)\/(~(p103 zenon_TX_q)))/\(((p101 zenon_TX_q)\/(~(p102 zenon_TX_q)))/\((p100 zenon_TX_q)\/(~(p101 zenon_TX_q))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(p3 Y))))))))))) -> (~(p101 zenon_TX_q)) -> (p100 zenon_TX_q) -> False). % 159.03/159.36 do 1 intro. intros zenon_H36 zenon_H37 zenon_H14 zenon_H38 zenon_H39. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H36). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H43); [ zenon_intro zenon_H45 | zenon_intro zenon_H44 ]. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H45). zenon_intro zenon_H47. zenon_intro zenon_H46. % 159.03/159.36 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TX_q X))\/(~((p2 X)/\((~(p102 X))/\(p101 X)))))) zenon_H46); [ zenon_intro zenon_H48; idtac ]. % 159.03/159.36 elim zenon_H48. zenon_intro zenon_TX_l. zenon_intro zenon_H49. % 159.03/159.36 apply (zenon_notor_s _ _ zenon_H49). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 159.03/159.36 apply zenon_H4a. zenon_intro zenon_H4c. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H4c). zenon_intro zenon_H4e. zenon_intro zenon_H4d. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H15. zenon_intro zenon_H16. % 159.03/159.36 apply zenon_H4b. zenon_intro zenon_Hf. % 159.03/159.36 generalize (zenon_H37 zenon_TX_q). zenon_intro zenon_H4f. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H4f); [ zenon_intro zenon_H2b | zenon_intro zenon_H50 ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 generalize (zenon_H50 zenon_TX_q). zenon_intro zenon_H51. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H51); [ zenon_intro zenon_H2b | zenon_intro zenon_H34 ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 apply (zenon_L7_ zenon_TX_l zenon_TX_q); trivial. % 159.03/159.36 apply (zenon_notand_s _ _ zenon_H44); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 159.03/159.36 exact (zenon_H53 zenon_H38). % 159.03/159.36 exact (zenon_H52 zenon_H39). % 159.03/159.36 (* end of lemma zenon_L8_ *) % 159.03/159.36 assert (zenon_L9_ : forall (zenon_TX_q : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_q Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(p3 Y))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (~(p101 zenon_TX_q)) -> (p100 zenon_TX_q) -> False). % 159.03/159.36 do 1 intro. intros zenon_H30 zenon_H14 zenon_H37 zenon_H38 zenon_H39. % 159.03/159.36 generalize (zenon_H30 zenon_TX_q). zenon_intro zenon_H54. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H54); [ zenon_intro zenon_H2b | zenon_intro zenon_H36 ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 apply (zenon_L8_ zenon_TX_q); trivial. % 159.03/159.36 (* end of lemma zenon_L9_ *) % 159.03/159.36 assert (zenon_L10_ : forall (zenon_TX_q : zenon_U), (forall X : zenon_U, ((~(r1 zenon_TX_q X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(p3 Y))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (~(p101 zenon_TX_q)) -> (p100 zenon_TX_q) -> False). % 159.03/159.36 do 1 intro. intros zenon_H32 zenon_H14 zenon_H37 zenon_H38 zenon_H39. % 159.03/159.36 generalize (zenon_H32 zenon_TX_q). zenon_intro zenon_H33. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H33); [ zenon_intro zenon_H2b | zenon_intro zenon_H30 ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 apply (zenon_L9_ zenon_TX_q); trivial. % 159.03/159.36 (* end of lemma zenon_L10_ *) % 159.03/159.36 assert (zenon_L11_ : forall (zenon_TX_q : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_q Y))\/(forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(p3 Y))))))))))) -> (forall Y : zenon_U, ((~(r1 zenon_TX_q 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))\/(~((~(p6 X))/\((~(p106 X))/\(p105 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p6 X)/\((~(p106 X))/\(p105 X))))))))\/(~((~(p105 Y))/\(p104 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p5 X))/\((~(p105 X))/\(p104 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p5 X)/\((~(p105 X))/\(p104 X))))))))\/(~((~(p104 Y))/\(p103 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p4 X))/\((~(p104 X))/\(p103 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p4 X)/\((~(p104 X))/\(p103 X))))))))\/(~((~(p103 Y))/\(p102 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p3 X))/\((~(p103 X))/\(p102 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p3 X)/\((~(p103 X))/\(p102 X))))))))\/(~((~(p102 Y))/\(p101 Y))))/\((((~(forall X : zenon_U, ((~(r1 Y X))\/(~((~(p2 X))/\((~(p102 X))/\(p101 X)))))))/\(~(forall X : zenon_U, ((~(r1 Y X))\/(~((p2 X)/\((~(p102 X))/\(p101 X))))))))\/(~((~(p101 Y))/\(p100 Y))))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p6 X))\/(~(p105 X)))))\/(p6 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p6 X)\/(~(p105 X)))))\/(~(p6 Y))))\/(~(p105 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p5 X))\/(~(p104 X)))))\/(p5 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p5 X)\/(~(p104 X)))))\/(~(p5 Y))))\/(~(p104 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p4 X))\/(~(p103 X)))))\/(p4 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p4 X)\/(~(p103 X)))))\/(~(p4 Y))))\/(~(p103 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p3 X))\/(~(p102 X)))))\/(p3 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p3 X)\/(~(p102 X)))))\/(~(p3 Y))))\/(~(p102 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p2 X))\/(~(p101 X)))))\/(p2 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(p101 X)))))\/(~(p2 Y))))\/(~(p101 Y)))/\(((((forall X : zenon_U, ((~(r1 Y X))\/((~(p1 X))\/(~(p100 X)))))\/(p1 Y))/\((forall X : zenon_U, ((~(r1 Y X))\/((p1 X)\/(~(p100 X)))))\/(~(p1 Y))))\/(~(p100 Y)))/\(((p105 Y)\/(~(p106 Y)))/\(((p104 Y)\/(~(p105 Y)))/\(((p103 Y)\/(~(p104 Y)))/\(((p102 Y)\/(~(p103 Y)))/\(((p101 Y)\/(~(p102 Y)))/\((p100 Y)\/(~(p101 Y))))))))))))))))))))))))))))) -> (~(p101 zenon_TX_q)) -> (p100 zenon_TX_q) -> False). % 159.03/159.36 do 1 intro. intros zenon_H34 zenon_H14 zenon_H37 zenon_H38 zenon_H39. % 159.03/159.36 generalize (zenon_H34 zenon_TX_q). zenon_intro zenon_H35. % 159.03/159.36 apply (zenon_or_s _ _ zenon_H35); [ zenon_intro zenon_H2b | zenon_intro zenon_H32 ]. % 159.03/159.36 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.36 exact (zenon_H2b zenon_H2c). % 159.03/159.36 apply (zenon_L10_ zenon_TX_q); trivial. % 159.03/159.36 (* end of lemma zenon_L11_ *) % 159.03/159.36 apply NNPP. intro zenon_G. % 159.03/159.36 apply zenon_G. zenon_intro zenon_H55. % 159.03/159.36 elim zenon_H55. zenon_intro zenon_TX_q. zenon_intro zenon_H56. % 159.03/159.36 apply (zenon_notor_s _ _ zenon_H56). zenon_intro zenon_H58. zenon_intro zenon_H57. % 159.03/159.36 apply zenon_H57. zenon_intro zenon_H59. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H37. zenon_intro zenon_H5a. % 159.03/159.36 apply (zenon_and_s _ _ zenon_H5a). zenon_intro zenon_H38. zenon_intro zenon_H39. % 159.03/159.36 apply zenon_H58. zenon_intro zenon_H14. % 159.03/159.36 generalize (zenon_H37 zenon_TX_q). zenon_intro zenon_H4f. % 159.03/159.38 apply (zenon_or_s _ _ zenon_H4f); [ zenon_intro zenon_H2b | zenon_intro zenon_H50 ]. % 159.03/159.38 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.38 exact (zenon_H2b zenon_H2c). % 159.03/159.38 generalize (zenon_H50 zenon_TX_q). zenon_intro zenon_H51. % 159.03/159.38 apply (zenon_or_s _ _ zenon_H51); [ zenon_intro zenon_H2b | zenon_intro zenon_H34 ]. % 159.03/159.38 generalize (reflexivity zenon_TX_q). zenon_intro zenon_H2c. % 159.03/159.38 exact (zenon_H2b zenon_H2c). % 159.03/159.38 apply (zenon_L11_ zenon_TX_q); trivial. % 159.03/159.38 Qed. % 159.03/159.38 % SZS output end Proof % 159.03/159.38 (* END-PROOF *) % 159.03/159.38 nodes searched: 3272255 % 159.03/159.38 max branch formulas: 49405 % 159.03/159.38 proof nodes created: 348659 % 159.03/159.38 formulas created: 5140825 % 159.03/159.38 %------------------------------------------------------------------------------