%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : MGT106+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n004.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 : Tue Sep 8 06:24:29 AM UTC 2026 % Result : Unsatisfiable 0.21s 0.54s % Output : Proof 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT106+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.04 % Command : run_zenon %s %d % 0.12/0.37 % Computer : n004.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Mon Sep 7 14:41:45 UTC 2026 % 0.12/0.37 % CPUTime : % 0.21/0.54 (* PROOF-FOUND *) % 0.21/0.54 % SZS status Unsatisfiable % 0.21/0.54 (* BEGIN-PROOF *) % 0.21/0.54 % SZS output start Proof % 0.21/0.54 Theorem zenon_thm : False. % 0.21/0.54 Proof. % 0.21/0.54 assert (zenon_L1_ : (~((v800) = (v800))) -> False). % 0.21/0.54 do 0 intro. intros zenon_H24. % 0.21/0.54 apply zenon_H24. apply refl_equal. % 0.21/0.54 (* end of lemma zenon_L1_ *) % 0.21/0.54 assert (zenon_L2_ : (~((w) = (w))) -> False). % 0.21/0.54 do 0 intro. intros zenon_H25. % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 (* end of lemma zenon_L2_ *) % 0.21/0.54 assert (zenon_L3_ : (~((v600) = (v600))) -> False). % 0.21/0.54 do 0 intro. intros zenon_H26. % 0.21/0.54 apply zenon_H26. apply refl_equal. % 0.21/0.54 (* end of lemma zenon_L3_ *) % 0.21/0.54 assert (zenon_L4_ : (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z)))))) -> (~(less (w) (w))) -> (less (w) (v600)) -> ((v800) = (w)) -> False). % 0.21/0.54 do 0 intro. intros zenon_H27 zenon_H28 zenon_H29 zenon_H2a. % 0.21/0.54 elim (classic (less (v600) (w))); [ zenon_intro zenon_H2b | zenon_intro zenon_H2c ]. % 0.21/0.54 generalize (zenon_H27 (w)). zenon_intro zenon_H2d. % 0.21/0.54 generalize (zenon_H2d (v600)). zenon_intro zenon_H2e. % 0.21/0.54 generalize (zenon_H2e (w)). zenon_intro zenon_H2f. % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H2f); [ zenon_intro zenon_H31 | zenon_intro zenon_H30 ]. % 0.21/0.54 exact (zenon_H31 zenon_H29). % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H30); [ zenon_intro zenon_H2c | zenon_intro zenon_H32 ]. % 0.21/0.54 exact (zenon_H2c zenon_H2b). % 0.21/0.54 exact (zenon_H28 zenon_H32). % 0.21/0.54 cut ((less (v600) (v800)) = (less (v600) (w))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H2c. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact ord_v600_v800. % 0.21/0.54 cut (((v800) = (w))); [idtac | apply NNPP; zenon_intro zenon_H33]. % 0.21/0.54 cut (((v600) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H26]. % 0.21/0.54 congruence. % 0.21/0.54 apply zenon_H26. apply refl_equal. % 0.21/0.54 exact (zenon_H33 zenon_H2a). % 0.21/0.54 (* end of lemma zenon_L4_ *) % 0.21/0.54 elim (classic (forall x : zenon_U, (forall y : zenon_U, (forall z : zenon_U, ((less x y)->((less y z)->(less x z))))))); [ zenon_intro zenon_H27 | zenon_intro zenon_H34 ]. % 0.21/0.54 apply (zenon_and_s _ _ distinct). zenon_intro zenon_H36. zenon_intro zenon_H35. % 0.21/0.54 apply (zenon_and_s _ _ zenon_H35). zenon_intro zenon_H38. zenon_intro zenon_H37. % 0.21/0.54 generalize (in_lopen (w)). zenon_intro zenon_H39. % 0.21/0.54 generalize (zenon_H39 (v0)). zenon_intro zenon_H3a. % 0.21/0.54 generalize (zenon_H3a (v600)). zenon_intro zenon_H3b. % 0.21/0.54 apply (zenon_equiv_s _ _ zenon_H3b); [ zenon_intro zenon_H3e; zenon_intro zenon_H3d | zenon_intro wit_in_lopen; zenon_intro zenon_H3c ]. % 0.21/0.54 exact (zenon_H3e wit_in_lopen). % 0.21/0.54 apply (zenon_and_s _ _ zenon_H3c). zenon_intro zenon_H40. zenon_intro zenon_H3f. % 0.21/0.54 generalize (leq_def (w)). zenon_intro zenon_H41. % 0.21/0.54 generalize (zenon_H41 (v600)). zenon_intro zenon_H42. % 0.21/0.54 apply (zenon_equiv_s _ _ zenon_H42); [ zenon_intro zenon_H45; zenon_intro zenon_H44 | zenon_intro zenon_H3f; zenon_intro zenon_H43 ]. % 0.21/0.54 exact (zenon_H45 zenon_H3f). % 0.21/0.54 generalize (leq_def (v800)). zenon_intro zenon_H46. % 0.21/0.54 generalize (zenon_H46 (w)). zenon_intro zenon_H47. % 0.21/0.54 apply (zenon_equiv_s _ _ zenon_H47); [ zenon_intro zenon_H4a; zenon_intro zenon_H49 | zenon_intro wit_leq; zenon_intro zenon_H48 ]. % 0.21/0.54 exact (zenon_H4a wit_leq). % 0.21/0.54 apply (zenon_or_s _ _ zenon_H48); [ zenon_intro zenon_H4b | zenon_intro zenon_H2a ]. % 0.21/0.54 apply (zenon_or_s _ _ zenon_H43); [ zenon_intro zenon_H29 | zenon_intro zenon_H4c ]. % 0.21/0.54 generalize (irreflexive (w)). zenon_intro zenon_H28. % 0.21/0.54 elim (classic ((~((w) = (v800)))/\(~(less (w) (v800))))); [ zenon_intro zenon_H4d | zenon_intro zenon_H4e ]. % 0.21/0.54 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 0.21/0.54 elim (classic ((~((w) = (v600)))/\(~(less (w) (v600))))); [ zenon_intro zenon_H51 | zenon_intro zenon_H52 ]. % 0.21/0.54 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H31. % 0.21/0.54 exact (zenon_H31 zenon_H29). % 0.21/0.54 cut ((less (v600) (v800)) = (less (w) (v800))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H4f. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact ord_v600_v800. % 0.21/0.54 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 0.21/0.54 cut (((v600) = (w))); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.21/0.54 congruence. % 0.21/0.54 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.21/0.54 apply zenon_H56. zenon_intro zenon_H4c. % 0.21/0.54 elim (classic ((w) = (w))); [ zenon_intro zenon_H57 | zenon_intro zenon_H25 ]. % 0.21/0.54 cut (((w) = (w)) = ((v600) = (w))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H54. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact zenon_H57. % 0.21/0.54 cut (((w) = (w))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 0.21/0.54 cut (((w) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.21/0.54 congruence. % 0.21/0.54 exact (zenon_H53 zenon_H4c). % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply zenon_H55. zenon_intro zenon_H29. % 0.21/0.54 generalize (zenon_H27 (w)). zenon_intro zenon_H2d. % 0.21/0.54 generalize (zenon_H2d (v600)). zenon_intro zenon_H2e. % 0.21/0.54 generalize (zenon_H2e (v800)). zenon_intro zenon_H58. % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H58); [ zenon_intro zenon_H31 | zenon_intro zenon_H59 ]. % 0.21/0.54 exact (zenon_H31 zenon_H29). % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H5b | zenon_intro zenon_H5a ]. % 0.21/0.54 exact (zenon_H5b ord_v600_v800). % 0.21/0.54 exact (zenon_H4f zenon_H5a). % 0.21/0.54 apply zenon_H24. apply refl_equal. % 0.21/0.54 cut ((less (v800) (w)) = (less (w) (w))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H28. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact zenon_H4b. % 0.21/0.54 cut (((w) = (w))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 0.21/0.54 cut (((v800) = (w))); [idtac | apply NNPP; zenon_intro zenon_H33]. % 0.21/0.54 congruence. % 0.21/0.54 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H5d | zenon_intro zenon_H5c ]. % 0.21/0.54 apply zenon_H5d. zenon_intro zenon_H5e. % 0.21/0.54 elim (classic ((w) = (w))); [ zenon_intro zenon_H57 | zenon_intro zenon_H25 ]. % 0.21/0.54 cut (((w) = (w)) = ((v800) = (w))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H33. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact zenon_H57. % 0.21/0.54 cut (((w) = (w))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 0.21/0.54 cut (((w) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 0.21/0.54 congruence. % 0.21/0.54 exact (zenon_H50 zenon_H5e). % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply zenon_H5c. zenon_intro zenon_H5a. % 0.21/0.54 generalize (zenon_H27 (w)). zenon_intro zenon_H2d. % 0.21/0.54 generalize (zenon_H2d (v800)). zenon_intro zenon_H5f. % 0.21/0.54 generalize (zenon_H5f (w)). zenon_intro zenon_H60. % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H4f | zenon_intro zenon_H61 ]. % 0.21/0.54 exact (zenon_H4f zenon_H5a). % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H62 | zenon_intro zenon_H32 ]. % 0.21/0.54 exact (zenon_H62 zenon_H4b). % 0.21/0.54 exact (zenon_H28 zenon_H32). % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 generalize (irreflexive (w)). zenon_intro zenon_H28. % 0.21/0.54 elim (classic ((~((w) = (v800)))/\(~(less (w) (v800))))); [ zenon_intro zenon_H4d | zenon_intro zenon_H4e ]. % 0.21/0.54 apply (zenon_and_s _ _ zenon_H4d). zenon_intro zenon_H50. zenon_intro zenon_H4f. % 0.21/0.54 elim (classic ((~((w) = (v600)))/\(~(less (w) (v600))))); [ zenon_intro zenon_H51 | zenon_intro zenon_H52 ]. % 0.21/0.54 apply (zenon_and_s _ _ zenon_H51). zenon_intro zenon_H53. zenon_intro zenon_H31. % 0.21/0.54 exact (zenon_H53 zenon_H4c). % 0.21/0.54 cut ((less (v600) (v800)) = (less (w) (v800))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H4f. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact ord_v600_v800. % 0.21/0.54 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 0.21/0.54 cut (((v600) = (w))); [idtac | apply NNPP; zenon_intro zenon_H54]. % 0.21/0.54 congruence. % 0.21/0.54 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H56 | zenon_intro zenon_H55 ]. % 0.21/0.54 apply zenon_H56. zenon_intro zenon_H4c. % 0.21/0.54 elim (classic ((w) = (w))); [ zenon_intro zenon_H57 | zenon_intro zenon_H25 ]. % 0.21/0.54 cut (((w) = (w)) = ((v600) = (w))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H54. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact zenon_H57. % 0.21/0.54 cut (((w) = (w))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 0.21/0.54 cut (((w) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.21/0.54 congruence. % 0.21/0.54 exact (zenon_H53 zenon_H4c). % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply zenon_H55. zenon_intro zenon_H29. % 0.21/0.54 generalize (zenon_H27 (w)). zenon_intro zenon_H2d. % 0.21/0.54 generalize (zenon_H2d (v600)). zenon_intro zenon_H2e. % 0.21/0.54 generalize (zenon_H2e (v800)). zenon_intro zenon_H58. % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H58); [ zenon_intro zenon_H31 | zenon_intro zenon_H59 ]. % 0.21/0.54 exact (zenon_H31 zenon_H29). % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H59); [ zenon_intro zenon_H5b | zenon_intro zenon_H5a ]. % 0.21/0.54 exact (zenon_H5b ord_v600_v800). % 0.21/0.54 exact (zenon_H4f zenon_H5a). % 0.21/0.54 apply zenon_H24. apply refl_equal. % 0.21/0.54 cut ((less (v800) (w)) = (less (w) (w))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H28. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact zenon_H4b. % 0.21/0.54 cut (((w) = (w))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 0.21/0.54 cut (((v800) = (w))); [idtac | apply NNPP; zenon_intro zenon_H33]. % 0.21/0.54 congruence. % 0.21/0.54 apply (zenon_notand_s _ _ zenon_H4e); [ zenon_intro zenon_H5d | zenon_intro zenon_H5c ]. % 0.21/0.54 apply zenon_H5d. zenon_intro zenon_H5e. % 0.21/0.54 elim (classic ((w) = (w))); [ zenon_intro zenon_H57 | zenon_intro zenon_H25 ]. % 0.21/0.54 cut (((w) = (w)) = ((v800) = (w))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H33. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact zenon_H57. % 0.21/0.54 cut (((w) = (w))); [idtac | apply NNPP; zenon_intro zenon_H25]. % 0.21/0.54 cut (((w) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H50]. % 0.21/0.54 congruence. % 0.21/0.54 exact (zenon_H50 zenon_H5e). % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply zenon_H5c. zenon_intro zenon_H5a. % 0.21/0.54 generalize (zenon_H27 (w)). zenon_intro zenon_H2d. % 0.21/0.54 generalize (zenon_H2d (v800)). zenon_intro zenon_H5f. % 0.21/0.54 generalize (zenon_H5f (w)). zenon_intro zenon_H60. % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H60); [ zenon_intro zenon_H4f | zenon_intro zenon_H61 ]. % 0.21/0.54 exact (zenon_H4f zenon_H5a). % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H61); [ zenon_intro zenon_H62 | zenon_intro zenon_H32 ]. % 0.21/0.54 exact (zenon_H62 zenon_H4b). % 0.21/0.54 exact (zenon_H28 zenon_H32). % 0.21/0.54 apply zenon_H25. apply refl_equal. % 0.21/0.54 apply (zenon_or_s _ _ zenon_H43); [ zenon_intro zenon_H29 | zenon_intro zenon_H4c ]. % 0.21/0.54 generalize (irreflexive (w)). zenon_intro zenon_H28. % 0.21/0.54 apply (zenon_L4_); trivial. % 0.21/0.54 elim (classic ((v800) = (v800))); [ zenon_intro zenon_H63 | zenon_intro zenon_H24 ]. % 0.21/0.54 cut (((v800) = (v800)) = ((v600) = (v800))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H37. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact zenon_H63. % 0.21/0.54 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 0.21/0.54 cut (((v800) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 0.21/0.54 congruence. % 0.21/0.54 cut (((v800) = (w)) = ((v800) = (v600))). % 0.21/0.54 intro zenon_D_pnotp. % 0.21/0.54 apply zenon_H64. % 0.21/0.54 rewrite <- zenon_D_pnotp. % 0.21/0.54 exact zenon_H2a. % 0.21/0.54 cut (((w) = (v600))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 0.21/0.54 cut (((v800) = (v800))); [idtac | apply NNPP; zenon_intro zenon_H24]. % 0.21/0.54 congruence. % 0.21/0.54 apply zenon_H24. apply refl_equal. % 0.21/0.54 exact (zenon_H53 zenon_H4c). % 0.21/0.54 apply zenon_H24. apply refl_equal. % 0.21/0.54 apply zenon_H24. apply refl_equal. % 0.21/0.54 apply zenon_H34. zenon_intro zenon_Tx_dx. apply NNPP. zenon_intro zenon_H66. % 0.21/0.54 apply zenon_H66. zenon_intro zenon_Ty_dz. apply NNPP. zenon_intro zenon_H68. % 0.21/0.54 apply zenon_H68. zenon_intro zenon_Tz_eb. apply NNPP. zenon_intro zenon_H6a. % 0.21/0.54 apply (zenon_notimply_s _ _ zenon_H6a). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.21/0.54 apply (zenon_notimply_s _ _ zenon_H6b). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.21/0.54 generalize (transitive zenon_Tx_dx). zenon_intro zenon_H6f. % 0.21/0.54 generalize (zenon_H6f zenon_Ty_dz). zenon_intro zenon_H70. % 0.21/0.54 generalize (zenon_H70 zenon_Tz_eb). zenon_intro zenon_H71. % 0.21/0.54 apply (zenon_imply_s _ _ zenon_H71); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.21/0.54 apply (zenon_notand_s _ _ zenon_H73); [ zenon_intro zenon_H75 | zenon_intro zenon_H74 ]. % 0.21/0.54 exact (zenon_H75 zenon_H6c). % 0.21/0.54 exact (zenon_H74 zenon_H6e). % 0.21/0.54 exact (zenon_H6d zenon_H72). % 0.21/0.54 Qed. % 0.21/0.54 % SZS output end Proof % 0.21/0.54 (* END-PROOF *) % 0.21/0.54 nodes searched: 1862 % 0.21/0.54 max branch formulas: 283 % 0.21/0.54 proof nodes created: 32 % 0.21/0.54 formulas created: 4350 % 0.21/0.54 %------------------------------------------------------------------------------