The existence of EFX allocations is a central open problem in discrete fair division. An allocation is EFX (envy-free up to any good) if no agent envies another agent after the removal of any single good from the other agent's bundle. We resolve this longstanding question by providing the \textbf{first-ever counterexample} to the existence of EFX allocations for agents with monotone valuations, which in turn immediately implies a counterexample for submodular valuations. Specifically, we show that EFX allocations need not exist for instances with $n \ge 3$ agents and $m \ge n+5$ goods. In contrast, we prove that every instance with three agents and seven goods admits an EFX allocation. Both results are obtained via SAT solving. We encode the negation of EFX existence as a SAT instance: satisfiability yields a counterexample, while unsatisfiability establishes universal existence. The correctness of the encoding is formally verified in Lean. Finally, we establish positive guarantees for fair allocations with three agents and an arbitrary number of goods. Although EFX allocations may fail to exist, we prove that every instance with three agents and monotone valuations admits at least one of two natural relaxations of EFX: tEFX, or EF1 and EEFX.

翻译：EFX分配的存在性是离散公平分配领域的一个核心开放问题。当任意一个智能体在去除其他智能体任意一个物品后不再嫉妒对方时，该分配被称为EFX（直至任意物品的无妒忌分配）。我们通过提供首个针对具有单调估值智能体的EFX分配存在性的反例，解决了这一长期问题，并由此直接推导出针对子模估值函数的反例。具体而言，我们证明了当智能体数量$n \ge 3$且物品数量$m \ge n+5$时，EFX分配并非必然存在。相比之下，我们证明了每个包含三个智能体和七个物品的实例均存在EFX分配。这两个结果均通过SAT求解获得。我们将EFX不存在的否定编码为SAT实例：可满足性生成反例，而不可满足性则证明普遍存在性。该编码的正确性已在Lean中形式化验证。最后，我们建立了关于三个智能体及任意数量物品公平分配的正向保证。尽管EFX分配可能不存在，我们证明了每个包含三个智能体及单调估值函数的实例至少满足EFX的两种自然松弛形式之一：tEFX，或EF1与EEFX。