%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL642+1.001 : 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:32 PM UTC 2026 % Result : Theorem 0.30s 0.61s % Output : Proof 0.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL642+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.08/0.35 % Computer : n026.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.36 % DateTime : Sat Sep 5 12:06:55 UTC 2026 % 0.13/0.36 % CPUTime : % 0.30/0.61 (* PROOF-FOUND *) % 0.30/0.61 % SZS status Theorem % 0.30/0.61 (* BEGIN-PROOF *) % 0.30/0.61 % SZS output start Proof % 0.30/0.61 Theorem main : (~(exists X : zenon_U, (~((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/((p3 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p3 Y)))\/(~(p3 X))))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p1 Y)))\/((~(forall Y : zenon_U, ((~(r1 X Y))\/((p1 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p1 Y)))\/(~(p1 X))))))))))\/(~(((((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))/\((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((((forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))/\((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))\/(~(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))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))/\((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))))\/(~(((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))/\((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y))))))))))))))))))/\(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))))))))))))))). % 0.30/0.61 Proof. % 0.30/0.61 assert (zenon_L1_ : forall (zenon_TY_f : zenon_U) (zenon_TX_g : zenon_U), (forall Y : zenon_U, ((~(r1 zenon_TX_g Y))\/(((forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))/\((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))) -> (r1 zenon_TX_g zenon_TY_f) -> (~(p2 zenon_TY_f)) -> (forall X : zenon_U, ((~(r1 zenon_TY_f X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))) -> False). % 0.30/0.61 do 2 intro. intros zenon_H1 zenon_H2 zenon_H3 zenon_H4. % 0.30/0.61 generalize (zenon_H1 zenon_TY_f). zenon_intro zenon_H7. % 0.30/0.61 apply (zenon_or_s _ _ zenon_H7); [ zenon_intro zenon_H9 | zenon_intro zenon_H8 ]. % 0.30/0.61 exact (zenon_H9 zenon_H2). % 0.30/0.61 apply (zenon_and_s _ _ zenon_H8). zenon_intro zenon_Hb. zenon_intro zenon_Ha. % 0.30/0.61 apply (zenon_or_s _ _ zenon_Ha); [ zenon_intro zenon_Hd | zenon_intro zenon_Hc ]. % 0.30/0.61 exact (zenon_H3 zenon_Hd). % 0.30/0.61 exact (zenon_Hc zenon_H4). % 0.30/0.61 (* end of lemma zenon_L1_ *) % 0.30/0.61 assert (zenon_L2_ : forall (zenon_TX_g : zenon_U), (~((forall Y : zenon_U, ((~(r1 zenon_TX_g Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))\/(~(forall Y : zenon_U, ((~(r1 zenon_TX_g Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))) -> (~(forall Y : zenon_U, ((~(r1 zenon_TX_g Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))) -> False). % 0.30/0.61 do 1 intro. intros zenon_He zenon_Hf. % 0.30/0.61 apply (zenon_notor_s _ _ zenon_He). zenon_intro zenon_H11. zenon_intro zenon_H10. % 0.30/0.61 exact (zenon_H10 zenon_Hf). % 0.30/0.61 (* end of lemma zenon_L2_ *) % 0.30/0.61 apply NNPP. intro zenon_G. % 0.30/0.61 apply zenon_G. zenon_intro zenon_H12. % 0.30/0.61 elim zenon_H12. zenon_intro zenon_TX_t. zenon_intro zenon_H14. % 0.30/0.61 apply (zenon_notor_s _ _ zenon_H14). zenon_intro zenon_H16. zenon_intro zenon_H15. % 0.30/0.61 apply (zenon_notor_s _ _ zenon_H15). zenon_intro zenon_H18. zenon_intro zenon_H17. % 0.30/0.61 apply (zenon_notor_s _ _ zenon_H17). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 0.30/0.61 apply (zenon_notor_s _ _ zenon_H19). zenon_intro zenon_H1c. zenon_intro zenon_H1b. % 0.30/0.61 apply (zenon_notor_s _ _ zenon_H1b). zenon_intro zenon_H1e. zenon_intro zenon_H1d. % 0.30/0.61 apply (zenon_notor_s _ _ zenon_H1d). zenon_intro zenon_H20. zenon_intro zenon_H1f. % 0.30/0.61 apply zenon_H1f. zenon_intro zenon_H21. % 0.30/0.61 apply (zenon_and_s _ _ zenon_H21). zenon_intro zenon_H23. zenon_intro zenon_H22. % 0.30/0.61 apply zenon_H1c. zenon_intro zenon_H24. % 0.30/0.61 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_t Y))\/(p2 Y))) zenon_H1a); [ zenon_intro zenon_H25; idtac ]. % 0.30/0.61 elim zenon_H25. zenon_intro zenon_TY_bm. zenon_intro zenon_H27. % 0.30/0.61 apply (zenon_notor_s _ _ zenon_H27). zenon_intro zenon_H29. zenon_intro zenon_H28. % 0.30/0.61 apply zenon_H29. zenon_intro zenon_H2a. % 0.30/0.61 apply (zenon_or_s _ _ zenon_H23); [ zenon_intro zenon_H2c | zenon_intro zenon_H2b ]. % 0.30/0.61 apply (zenon_and_s _ _ zenon_H2c). zenon_intro zenon_H2e. zenon_intro zenon_H2d. % 0.30/0.61 apply (zenon_or_s _ _ zenon_H2e); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 0.30/0.61 generalize (zenon_H22 zenon_TY_bm). zenon_intro zenon_H31. % 0.30/0.61 apply (zenon_or_s _ _ zenon_H31); [ zenon_intro zenon_H33 | zenon_intro zenon_H32 ]. % 0.30/0.61 exact (zenon_H33 zenon_H2a). % 0.30/0.61 apply (zenon_or_s _ _ zenon_H32); [ zenon_intro zenon_H35 | zenon_intro zenon_H34 ]. % 0.30/0.61 exact (zenon_H28 zenon_H35). % 0.30/0.61 generalize (zenon_H30 zenon_TY_bm). zenon_intro zenon_H36. % 0.30/0.61 apply (zenon_or_s _ _ zenon_H36); [ zenon_intro zenon_H33 | zenon_intro zenon_H37 ]. % 0.30/0.61 exact (zenon_H33 zenon_H2a). % 0.30/0.61 exact (zenon_H34 zenon_H37). % 0.30/0.61 exact (zenon_H2f zenon_H24). % 0.30/0.61 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_t Y))\/((((forall X : zenon_U, ((~(r1 Y X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))/\((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))\/(~(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))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))\/(~(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))/\((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))))\/(~(((forall Y : zenon_U, ((~(r1 X Y))\/(forall X : zenon_U, ((~(r1 Y X))\/((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X)))))))))))/\((p2 X)\/(~(forall Y : zenon_U, ((~(r1 X Y))\/((forall X : zenon_U, ((~(r1 Y X))\/(p2 X)))\/(~(p2 Y)))))))))))))))) zenon_H2b); [ zenon_intro zenon_H38; idtac ]. % 0.30/0.61 elim zenon_H38. zenon_intro zenon_TY_cf. zenon_intro zenon_H3a. % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H3a). zenon_intro zenon_H3c. zenon_intro zenon_H3b. % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H3b). zenon_intro zenon_H3e. zenon_intro zenon_H3d. % 0.30/0.62 apply zenon_H3d. zenon_intro zenon_H3f. % 0.30/0.62 apply zenon_H3c. zenon_intro zenon_H40. % 0.30/0.62 apply (zenon_notand_s _ _ zenon_H3e); [ zenon_intro zenon_H42 | zenon_intro zenon_H41 ]. % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H42). zenon_intro zenon_H44. zenon_intro zenon_H43. % 0.30/0.62 apply (zenon_notallex_s (fun X : zenon_U => ((~(r1 zenon_TY_cf X))\/(forall Y : zenon_U, ((~(r1 X Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))))) zenon_H44); [ zenon_intro zenon_H45; idtac ]. % 0.30/0.62 elim zenon_H45. zenon_intro zenon_TX_g. zenon_intro zenon_H46. % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H46). zenon_intro zenon_H47. zenon_intro zenon_Hf. % 0.30/0.62 apply zenon_H47. zenon_intro zenon_H48. % 0.30/0.62 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TX_g Y))\/((p2 Y)\/(~(forall X : zenon_U, ((~(r1 Y X))\/((forall Y : zenon_U, ((~(r1 X Y))\/(p2 Y)))\/(~(p2 X))))))))) zenon_Hf); [ zenon_intro zenon_H49; idtac ]. % 0.30/0.62 elim zenon_H49. zenon_intro zenon_TY_f. zenon_intro zenon_H4a. % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H4a). zenon_intro zenon_H4c. zenon_intro zenon_H4b. % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H4b). zenon_intro zenon_H3. zenon_intro zenon_H4d. % 0.30/0.62 apply zenon_H4d. zenon_intro zenon_H4. % 0.30/0.62 apply zenon_H4c. zenon_intro zenon_H2. % 0.30/0.62 apply zenon_H43. zenon_intro zenon_H4e. % 0.30/0.62 generalize (zenon_H4e zenon_TX_g). zenon_intro zenon_H4f. % 0.30/0.62 apply (zenon_or_s _ _ zenon_H4f); [ zenon_intro zenon_H51 | zenon_intro zenon_H50 ]. % 0.30/0.62 exact (zenon_H51 zenon_H48). % 0.30/0.62 apply (zenon_or_s _ _ zenon_H50); [ zenon_intro zenon_H53 | zenon_intro zenon_H52 ]. % 0.30/0.62 generalize (zenon_H3f zenon_TX_g). zenon_intro zenon_H54. % 0.30/0.62 apply (zenon_or_s _ _ zenon_H54); [ zenon_intro zenon_H51 | zenon_intro zenon_H55 ]. % 0.30/0.62 exact (zenon_H51 zenon_H48). % 0.30/0.62 apply (zenon_or_s _ _ zenon_H55); [ zenon_intro zenon_H1 | zenon_intro zenon_H56 ]. % 0.30/0.62 apply (zenon_L1_ zenon_TY_f zenon_TX_g); trivial. % 0.30/0.62 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_He | zenon_intro zenon_H57 ]. % 0.30/0.62 apply (zenon_L2_ zenon_TX_g); trivial. % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H57). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.30/0.62 exact (zenon_H59 zenon_H53). % 0.30/0.62 generalize (zenon_H3f zenon_TX_g). zenon_intro zenon_H54. % 0.30/0.62 apply (zenon_or_s _ _ zenon_H54); [ zenon_intro zenon_H51 | zenon_intro zenon_H55 ]. % 0.30/0.62 exact (zenon_H51 zenon_H48). % 0.30/0.62 apply (zenon_or_s _ _ zenon_H55); [ zenon_intro zenon_H1 | zenon_intro zenon_H56 ]. % 0.30/0.62 apply (zenon_L1_ zenon_TY_f zenon_TX_g); trivial. % 0.30/0.62 apply (zenon_notand_s _ _ zenon_H56); [ zenon_intro zenon_He | zenon_intro zenon_H57 ]. % 0.30/0.62 apply (zenon_L2_ zenon_TX_g); trivial. % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H57). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.30/0.62 exact (zenon_H58 zenon_H52). % 0.30/0.62 apply (zenon_notor_s _ _ zenon_H41). zenon_intro zenon_H5b. zenon_intro zenon_H5a. % 0.30/0.62 apply zenon_H5a. zenon_intro zenon_H5c. % 0.30/0.62 generalize (zenon_H24 zenon_TY_cf). zenon_intro zenon_H5d. % 0.30/0.62 apply (zenon_or_s _ _ zenon_H5d); [ zenon_intro zenon_H5f | zenon_intro zenon_H5e ]. % 0.30/0.62 exact (zenon_H5f zenon_H40). % 0.30/0.62 apply (zenon_or_s _ _ zenon_H5e); [ zenon_intro zenon_H61 | zenon_intro zenon_H60 ]. % 0.30/0.62 exact (zenon_H5b zenon_H61). % 0.30/0.62 exact (zenon_H60 zenon_H5c). % 0.30/0.62 Qed. % 0.30/0.62 % SZS output end Proof % 0.30/0.62 (* END-PROOF *) % 0.30/0.62 nodes searched: 3122 % 0.30/0.62 max branch formulas: 1340 % 0.30/0.62 proof nodes created: 505 % 0.30/0.62 formulas created: 20698 % 0.30/0.62 %------------------------------------------------------------------------------