EFX Allocations for Three Agents and Seven or Eight Chores

RESUMO

We prove that every nonnegative additive chore instance with three agents and either seven or eight indivisible chores admits a chores-EFX allocation, in the zero-tolerant sense that every owned chore, including one of zero cost, is quantified in the trim. Both proofs are computer-assisted, but their machine formulas differ. For seven chores, hand-checkable canonicalization reduces nonexistence to a quantifier-free linear real arithmetic (QF_LRA) formula over 21 variables with one failure clause per complete allocation. For eight chores, instances in which two agents share a weakly cheapest chore are lifted from the seven-chore theorem through the matching insertion lemma of Kobayashi, Mahara, and Sakamoto, and the remaining pairwise-disjoint-argmin class reduces to a residual QF_LRA formula over 24 variables. Z3 5.1.0 and cvc5 1.3.4 report both formulas unsatisfiable. With the known $m\leq 2n$ theorem, this settles every three-agent instance with at most eight chores; $m=9$ is the next open cardinality, and additive chores can fail to admit EFX for every $n\geq 4$.