%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL686+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n015.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.30s 0.57s % Output : Proof 0.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_zenon %s %d % 0.11/0.36 % Computer : n015.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Fri Sep 4 18:49:26 UTC 2026 % 0.11/0.37 % CPUTime : % 0.30/0.57 (* PROOF-FOUND *) % 0.30/0.57 % SZS status Theorem % 0.30/0.57 (* BEGIN-PROOF *) % 0.30/0.57 % SZS output start Proof % 0.30/0.57 Theorem main : (~(exists X : zenon_U, (~((forall Y : zenon_U, ((~(r1 X Y))\/((~(p15 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))\/False))\/(~(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))\/(p15 Y)))\/(forall Y : zenon_U, ((~(r1 X 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.30/0.57 Proof. % 0.30/0.57 assert (zenon_L1_ : forall (zenon_TY_h : zenon_U) (zenon_TY_i : zenon_U), (~(~(p2 zenon_TY_i))) -> (forall Y : zenon_U, ((~(r1 zenon_TY_h Y))\/(~(((p2 Y)/\(~(p1 Y)))\/((~(p2 Y))/\(p1 Y)))))) -> (r1 zenon_TY_h zenon_TY_i) -> (~((p2 zenon_TY_i)/\(p1 zenon_TY_i))) -> False). % 0.30/0.57 do 2 intro. intros zenon_H3 zenon_H4 zenon_H5 zenon_H6. % 0.30/0.57 apply zenon_H3. zenon_intro zenon_H9. % 0.30/0.57 apply (zenon_notand_s _ _ zenon_H6); [ zenon_intro zenon_Hb | zenon_intro zenon_Ha ]. % 0.30/0.57 exact (zenon_Hb zenon_H9). % 0.30/0.57 generalize (zenon_H4 zenon_TY_i). zenon_intro zenon_Hc. % 0.30/0.57 apply (zenon_or_s _ _ zenon_Hc); [ zenon_intro zenon_He | zenon_intro zenon_Hd ]. % 0.30/0.57 exact (zenon_He zenon_H5). % 0.30/0.57 apply (zenon_notor_s _ _ zenon_Hd). zenon_intro zenon_H10. zenon_intro zenon_Hf. % 0.30/0.57 apply (zenon_notand_s _ _ zenon_H10); [ zenon_intro zenon_Hb | zenon_intro zenon_H11 ]. % 0.30/0.57 exact (zenon_Hb zenon_H9). % 0.30/0.57 exact (zenon_H11 zenon_Ha). % 0.30/0.57 (* end of lemma zenon_L1_ *) % 0.30/0.57 apply NNPP. intro zenon_G. % 0.30/0.57 apply zenon_G. zenon_intro zenon_H12. % 0.30/0.57 elim zenon_H12. zenon_intro zenon_TX_t. zenon_intro zenon_H14. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H14). zenon_intro zenon_H16. zenon_intro zenon_H15. % 0.30/0.57 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))\/((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))\/False))\/(~(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))\/(p15 Y)))\/(forall Y : zenon_U, ((~(r1 X 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_H15); [ zenon_intro zenon_H17; idtac ]. % 0.30/0.57 elim zenon_H17. zenon_intro zenon_TY_h. zenon_intro zenon_H18. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H18). zenon_intro zenon_H1a. zenon_intro zenon_H19. % 0.30/0.57 apply zenon_H19. zenon_intro zenon_H1b. % 0.30/0.57 generalize (zenon_H1b zenon_TY_h). zenon_intro zenon_H1c. % 0.30/0.57 apply (zenon_or_s _ _ zenon_H1c); [ zenon_intro zenon_H1e | zenon_intro zenon_H1d ]. % 0.30/0.57 generalize (reflexivity zenon_TY_h). zenon_intro zenon_H1f. % 0.30/0.57 exact (zenon_H1e zenon_H1f). % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H1d). zenon_intro zenon_H21. zenon_intro zenon_H20. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H22). zenon_intro zenon_H25. zenon_intro zenon_H24. % 0.30/0.57 apply zenon_H23. zenon_intro zenon_H4. % 0.30/0.57 apply (zenon_notallex_s (fun Y : zenon_U => ((~(r1 zenon_TY_h 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_H24); [ zenon_intro zenon_H26; idtac ]. % 0.30/0.57 elim zenon_H26. zenon_intro zenon_TY_i. zenon_intro zenon_H27. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H27). zenon_intro zenon_H29. zenon_intro zenon_H28. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H2a). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H2e). zenon_intro zenon_H31. zenon_intro zenon_H30. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H36). zenon_intro zenon_H39. zenon_intro zenon_H38. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H38). zenon_intro zenon_H3b. zenon_intro zenon_H3a. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H3a). zenon_intro zenon_H3d. zenon_intro zenon_H3c. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H3c). zenon_intro zenon_H3f. zenon_intro zenon_H3e. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H3e). zenon_intro zenon_H41. zenon_intro zenon_H40. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H40). zenon_intro zenon_H43. zenon_intro zenon_H42. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H42). zenon_intro zenon_H45. zenon_intro zenon_H44. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H46). zenon_intro zenon_H49. zenon_intro zenon_H48. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H48). zenon_intro zenon_H4b. zenon_intro zenon_H4a. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H4a). zenon_intro zenon_H4d. zenon_intro zenon_H4c. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H4c). zenon_intro zenon_H4f. zenon_intro zenon_H4e. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H4e). zenon_intro zenon_H51. zenon_intro zenon_H50. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H50). zenon_intro zenon_H53. zenon_intro zenon_H52. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H52). zenon_intro zenon_H55. zenon_intro zenon_H54. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H54). zenon_intro zenon_H57. zenon_intro zenon_H56. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H56). zenon_intro zenon_H59. zenon_intro zenon_H58. % 0.30/0.57 apply (zenon_notor_s _ _ zenon_H58). zenon_intro zenon_H5a. zenon_intro zenon_H6. % 0.30/0.57 apply zenon_H29. zenon_intro zenon_H5. % 0.30/0.57 apply (zenon_notand_s _ _ zenon_H5a); [ zenon_intro zenon_H11 | zenon_intro zenon_H3 ]. % 0.30/0.57 apply zenon_H11. zenon_intro zenon_H5b. % 0.30/0.57 generalize (zenon_H4 zenon_TY_i). zenon_intro zenon_Hc. % 0.30/0.57 apply (zenon_or_s _ _ zenon_Hc); [ zenon_intro zenon_He | zenon_intro zenon_Hd ]. % 0.30/0.57 exact (zenon_He zenon_H5). % 0.30/0.57 apply (zenon_notor_s _ _ zenon_Hd). zenon_intro zenon_H10. zenon_intro zenon_Hf. % 0.30/0.57 apply (zenon_notand_s _ _ zenon_Hf); [ zenon_intro zenon_H3 | zenon_intro zenon_Ha ]. % 0.30/0.57 apply (zenon_L1_ zenon_TY_h zenon_TY_i); trivial. % 0.30/0.57 exact (zenon_Ha zenon_H5b). % 0.30/0.57 apply (zenon_L1_ zenon_TY_h zenon_TY_i); trivial. % 0.30/0.57 Qed. % 0.30/0.57 % SZS output end Proof % 0.30/0.57 (* END-PROOF *) % 0.30/0.57 nodes searched: 2570 % 0.30/0.57 max branch formulas: 980 % 0.30/0.57 proof nodes created: 355 % 0.30/0.57 formulas created: 13808 % 0.30/0.57 %------------------------------------------------------------------------------