Pith. sign in

REVIEW 4 major objections 4 minor 1 cited by

Hereditary First-Order Logic: the tractable quantifier prefix classes

T0 review · 4 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Hereditary first-order model checking has a complete P/coNP-complete dichotomy by quantifier prefix.

desk verdict A real result with a complete non-monadic quantifier-prefix dichotomy for hereditary model checking, but one key hardness proof is left as an exercise and a few small statements need correction. read the letter →

arxiv 2411.10860 v2 pith:5F6Z722P submitted 2024-11-16 math.LO cs.CCcs.DMcs.LO

Manuel Bodirsky , Santiago Guzmán-Pro This is my paper · ORCID
classification math.LOcs.CCcs.DMcs.LO MSC 03C1303D1568Q17
keywords hereditaryfirst-orderlogicquantifierprefixmodelcheckingcomputationalcomplexitycoNP-completeconstraintsatisfactionproblemfinitetheorydichotomy
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper studies hereditary model checking: for a fixed first-order sentence $\phi$, decide whether a finite structure has the property that every one of its substructures satisfies $\phi$. It proves a complete complexity dichotomy by quantifier prefix—the leading string of $\forall$ and $\exists$ quantifiers when $\phi$ is written in prenex normal form. For every non-monadic relational signature, if the prefix is all-universal-then-existential ($\forall^{*}\exists^{*}$) or all-universal with a single existential between universal blocks ($\forall^{*}\exists\forall^{*}$), then the hereditary model checking problem for $\phi$ is in polynomial time for every sentence with that prefix. For every other prefix—one containing $\exists\exists\forall$ or $\exists\forall\exists$ somewhere in the quantifier string—there exists a sentence with that prefix whose hereditary model checking problem is coNP-complete. The paper also proves that, unless $\mathrm{P}=\mathrm{coNP}$, there is no algorithm that takes a first-order sentence and decides whether its hereditary model checking problem is solvable in polynomial time.

What carries the argument

The proof uses three mechanisms. For $\forall^{*}\exists^{*}$ sentences with $k$ universal quantifiers, Lemma 5.2 reduces hereditary satisfaction to checking all $k$-element substructures, which makes $\mathrm{Her}(\phi)$ a universal first-order property and therefore polynomial-time solvable. For $\forall^{*}\exists\forall^{*}$ sentences, the paper encodes $\mathrm{Her}(\phi)$ as an SNP sentence (a second-order sentence $\exists R_1,\ldots,R_k\forall x_1,\ldots,x_n\,\psi$ with quantifier-free $\psi$) that asks for an $(l+2)$-ary relation $L$ parameterizing a family of linear orders; Algorithm 1 either constructs such an $L$ for an input structure or returns a substructure violating $\phi$, in polynomial time. On the hardness side, the load-bearing object is a single digraph property—every directed cycle contains a symmetric edge—which is hereditarily definable by the $\exists\forall\exists$-sentence $\exists x,y\forall a\,(\neg E(x,a)\lor (E(x,y)\land E(y,x)))$ and is shown coNP-complete by a 3SAT reduction (Theorem 5.8). Extra quantifiers can then be added vacuously to produce hard formulas for every prefix that contains $\exists\exists\forall$ or $\exists\forall\exists$ as a subword.

What would settle it

Take the reduction from Theorem 5.8, run it on a few small 3SAT instances—for example the satisfiable formula $(x\lor y\lor z)\land(\neg x\lor\neg y\lor\neg z)$ and the unsatisfiable formula $(x\lor x\lor x)\land(\neg x\lor\neg x\lor\neg x)$—and enumerate all directed cycles of the constructed digraph. If a satisfiable instance yields a digraph in which every directed cycle has a symmetric edge, or an unsatisfiable instance yields a directed cycle without a symmetric edge, then the claimed coNP-completeness proof fails and with it the hardness half of the main dichotomy.

Watch

Extended reading notes

Core claim

The central claim is a dichotomy for the hereditary model checking problem $\mathrm{Her}(\phi)$, parameterized by the quantifier prefix of $\phi$. Fix a relational signature $\tau$ with at least one relation of arity at least two. If the prefix is of the form $\forall^{*}\exists^{*}$ or $\forall^{*}\exists\forall^{*}$, then for every $\tau$-sentence $\phi$ with that prefix, deciding whether a finite $\tau$-structure $A$ has every substructure satisfying $\phi$ is in $\mathrm{P}$. If the prefix contains $\exists\exists\forall$ or $\exists\forall\exists$ as a subword, then there exists a $\tau$-sentence $\phi$ with that prefix for which $\mathrm{Her}(\phi)$ is coNP-complete. These two cases cover every word over $\{\exists,\forall\}$, so the classification is complete. When all relation symbols are monadic, every $\mathrm{Her}(\phi)$ is universally definable and hence in $\mathrm{P}$, which is why the dichotomy is stated for non-monadic signatures. The paper further shows that, assuming $\mathrm{P}\neq\mathrm{coNP}$, whether a given first-order sentence $\phi$ has $\mathrm{Her}(\phi)$ in $\mathrm{P}$ is undecidable, and this remains undecidable even when $\phi$'s prefix contains $\exists\forall\exists$ or $\exists^3\forall$.

Load-bearing premise

The hardness half of the main dichotomy rests on a 3SAT reduction whose correctness the paper states but leaves to the reader; if that reduction has a hidden flaw, the claimed coNP-complete examples for a single binary relation, and hence for all non-monadic signatures, would need a new proof.

Editorial extensions

If this is right

  • For every non-monadic signature, every sentence with prefix $\forall^{*}\exists^{*}$ or $\forall^{*}\exists\forall^{*}$ has a hereditary model checking problem in $\mathrm{P}$, so all hereditary classes definable by such sentences have polynomial-time recognition.
  • Every prefix outside these two shapes admits at least one sentence whose hereditary class is coNP-complete, so the P-versus-coNP-complete boundary for $\mathrm{Her}(\phi)$ is completely described by quantifier prefixes.
  • Since $\mathrm{Her}(\phi)$ is always in coNP, the dichotomy is a genuine P-versus-coNP split for the prefix-defined fragments, with no unclassified prefixes.
  • For monadic signatures, every $\mathrm{Her}(\phi)$ is in $\mathrm{P}$, so the non-monadic assumption in the main theorem is necessary.
  • Unless $\mathrm{P}=\mathrm{coNP}$, one cannot algorithmically decide from a first-order sentence whether its hereditary model checking problem is polynomial-time solvable, and the undecidability persists for prefixes containing $\exists\forall\exists$ or $\exists^3\forall$.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural reading of the tractable side is that hereditary satisfaction is certified either by bounded-size substructures or by a parameterized linear order; testing whether analogous certificate-based dichotomies hold for hereditary logics with equality or counting quantifiers is a direct next step.
  • Because Theorem 5.8 states its 3SAT reduction but leaves the soundness proof to the reader, a small computational check—enumerating directed cycles in the digraphs built from satisfiable and unsatisfiable 3SAT formulas—would directly test the load-bearing hardness step.
  • The paper's CSP examples suggest that the prefix boundary may also organize which infinite-domain constraint satisfaction problems admit hereditary first-order definitions; mapping the coNP-complete hereditary CSPs against known infinite-domain complexity classifications would extend the picture.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper studies hereditary model checking: for a fixed first-order sentence φ, Her(φ) is the class of finite structures all of whose substructures satisfy φ. The main contribution is a claimed quantifier-prefix dichotomy: for every prefix Q either every Her(φ) with prefix Q is in P (when Q has the form ∀*∃* or ∀*∃∀*), or some Her(φ) with prefix Q is coNP-complete (when Q contains ∃∃∀ or ∃∀∃), for every non-monadic relational signature. The paper also proves, under P≠coNP, undecidability of the problem of deciding whether Her(φ) is polynomial-time solvable. The tractable side is approached through universal definability and a certifying SNP algorithm; the hard side uses two 3SAT reductions, one of which (Theorem 5.8) is explicitly left unproved.

Significance. If the dichotomy is fully established, it is a valuable and natural counterpart to the known prefix classifications for existential second-order logic, and it gives a unified account of several hereditary graph classes (forests, chordal graphs, acyclic digraphs, poset cover relations) and of some CSPs. The paper also contains useful conceptual contributions: the connection between Her-FO and CSPs, the undecidability argument in Theorem 4.2, and the certifying polynomial-time algorithm for ∀*∃∀* formulas. The main obstacle is that the hardness side for binary signatures rests on a reduction whose correctness proof is omitted, and the monadic-case proposition is stated with a false bound. These are local but load-bearing gaps, so the paper is not yet in publishable form.

major comments (4)
  1. [§5, Theorem 5.8] The coNP-hardness proof of Theorem 5.8 is incomplete. The proof presents a 3SAT reduction and then says that one can verify soundness and correctness, explicitly leaving the details to the reader. Corollary 5.9 and the hardness half of Theorem 5.10 for binary signatures depend directly on this theorem. The reduction appears sound on inspection, but a published dichotomy requires the full correctness argument rather than a reference to similar arguments from Theorem 3.2.
  2. [§5, Proposition 5.1] Proposition 5.1 is false as stated. Let τ={U} and let φ be the sentence expressing 'there are at most two U-elements'. A structure with exactly three U-elements has every substructure of size at most 2^|τ|=2 satisfying φ, yet the structure itself does not satisfy φ and hence is not in Her(φ). The proof collapses all elements with the same monadic type to one element, losing the cardinality information that first-order sentences can express. The bound must depend on the quantifier rank of φ, and the universal definability claim needs a corrected proof. Although Theorem 5.10 excludes monadic signatures, the paper uses this proposition to dispose of the monadic case.
  3. [§5, Lemma 5.2 and Corollary 5.3] The proof of the tractable case ∀*∃* does not cover the prefix ∃*, i.e., the case k=0. Lemma 5.2 is vacuous for k=0, and Corollary 5.3 bounds the existential witnesses by the list x1,...,xk, which is empty when there are no universal quantifiers. Since Q=∃* is included in the form ∀*∃* in Theorem 5.10, a separate argument is needed, for example showing that Her(∃y1...∃yl ψ) is equivalent to the universal statement that every substructure of size at most l satisfies the existential sentence.
  4. [§5, Theorem 5.10 (arity at least three)] For signatures that contain no binary relation but only relations of arity at least three, the proof says only that 'we can use R to model a binary relation'. This is not immediate: the existential quantifier that supplies the parameter changes the behavior of Her(φ) on substructures that do not contain that parameter, and the quantifier prefix Q may place the parameter after universal quantifiers. A concrete encoding must be given and shown to preserve both the prefix and hereditary satisfaction; as written, the dichotomy is fully proven only for signatures containing a binary relation symbol.
minor comments (4)
  1. [Abstract] The abstract states the dichotomy without the non-monadic assumption; as written, the second bullet is false for monadic signatures, where all Her(φ) problems are in P. Please add the qualification 'for non-monadic signatures'.
  2. [§4, Corollary 4.3] The quantifier bookkeeping in Corollary 4.3 should be checked: the dual of ∃3∀ is ∀3∃, which is of the form ∀*∃* that the corollary itself lists as decidable; likewise the subword '∀∀∃' is of that same decidable form. The intended forbidden subword is likely ∀∃∀.
  3. [References] References [4] and [5] list the same book by the same author and publisher; this appears to be a duplicate entry.
  4. [Throughout] There are several typographical errors, e.g., 'Yanakkakis' for 'Yannakakis' in Section 1, and 'It it true' in Open Problem 5 of Section 6.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the tractability and hardness results are derived from independent complexity and model-theoretic ingredients; the Theorem 5.8 proof gap is a correctness risk, not a circularity.

full rationale

The central claims (Theorem 5.10 dichotomy and Theorem 4.2 undecidability) are not obtained by fitting, renaming, or self-referential definition. The tractable side reduces Her(phi) to universal or SNP definability via Lemma 5.2 and Lemma 5.4, each proved directly from the syntax of phi with constructive arguments and Algorithm 1, and the hardness side builds explicit 3SAT reductions in Theorem 3.2 and Theorem 5.8. The paper's self-citations are to standard CSP facts (Observation 2.1 and the CSP representation in Observation 3.1, citing the authors' book) and to an MSO-to-omega-categorical CSP result; these are auxiliary background, are not used to define the target classes, and do not carry the dichotomy. The only load-bearing fragility is that Theorem 5.8 explicitly leaves the soundness and correctness proof of its 3SAT reduction 'to the reader'; that is a missing proof and hence a correctness risk for the binary-signature hardness half, not a circular step, since the reduction is a new combinatorial construction rather than an input to itself. No fitted parameter is renamed as a prediction, no uniqueness theorem is imported from the authors' prior work, and no known result is repackaged as a derivation. The derivation is therefore self-contained up to the stated external classical results (Trakhtenbrot's theorem, 3SAT, prefix-class decidability results), and no circularity score is warranted.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claims rest on standard theorems in finite model theory and complexity, plus the explicit P≠NP and P≠coNP assumptions in the undecidability theorems. There are no fitted constants and no newly postulated entities.

assumptions (4)
  • standard math The finite satisfiability problem for first-order logic is undecidable (Trakhtenbrot's theorem).
    Used in Theorem 4.2 as the base problem reduced to the HerFO tractability problem.
  • standard math Finite satisfiability is decidable for the Ackermann and Bernays-Schönfinkel prefix classes, and undecidable for prefixes containing ∃∀∃ or ∀∀∃.
    Used in Corollary 4.3 to transfer undecidability of tractability to specific quantifier prefixes.
  • standard math A class of finite τ-structures is a CSP of a countably infinite structure iff it is closed under inverse homomorphisms and disjoint unions.
    Observation 2.1 and the proof of Observation 3.1 rely on this external characterization, cited to the authors' book [4].
  • domain assumption The complexity separations P≠NP and P≠coNP.
    The undecidability theorems are conditional on these assumptions, stated explicitly in Theorem 4.2 and Corollary 4.3.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Hereditary First-Order Logic: the tractable quantifier prefix classes." pith.science (2026). https://pith.science/paper/5F6Z722P

@misc{pith2026241110860,
  author       = {Pith},
  title        = {Pith review of: Hereditary First-Order Logic: the tractable quantifier prefix classes},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5F6Z722P}},
  note         = {Machine review of arXiv:2411.10860}
}
abstract

Many computational problems can be modelled as the class of all finite structures $\mathbb A$ that satisfy a fixed first-order sentence $\phi$ hereditarily, i.e., we require that every (induced) substructure of $\mathbb A$ satisfies $\phi$. We call the corresponding computational problem the hereditary model checking problem for $\phi$, and denote it by Her$(\phi)$. We present a complete description of the quantifier prefixes for $\phi$ such that Her$(\phi)$ is in P; we show that for every other quantifier prefix there exists a formula $\phi$ with this prefix such that Her$(\phi)$ is coNP-complete. Specifically, we show that if $Q$ is of the form $\forall^\ast\exists\forall^\ast$ or of the form $\forall^\ast\exists^\ast$, then Her$(\phi)$ can be solved in polynomial time whenever the quantifier prefix of $\phi$ is $Q$. Otherwise, $Q$ contains $\exists \exists \forall$ or $\exists \forall \exists$ as a subword, and in this case, there is a first-order formula $\phi$ whose quantifier prefix is $Q$ and Her$(\phi)$ is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula $\phi$ whether Her$(\phi)$ is in P (unless P$=$NP).

Figures

Figures reproduced from arXiv: 2411.10860 by the authors.

Figure 1
Figure 1. Consider a first-order {E}-sentence ϕ that states that E is a symmetric relation, and that for every vertex x there is a vertex y not adjacent to x such that the neighbourhood of y induces a clique. Clearly, ϕ can be chosen to be an ∀∃∀∗ formula. On the top, we depict a graph G with two distinguished vertices a and b. At the bottom left, we depict the linear order ≤a (from left to right) of G obtained via Algorithm … view at source ↗
Figure 2
Figure 2. A partial depiction of the first three lines of [PITH_FULL_IMAGE:figures/full_fig_p022_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. The Network Satisfaction Problem for Relation Algebras with at most 4 Atoms

    math.RA 2025-07 conditional novelty 7.0 of 10

    Every finite relation algebra with at most four atoms has a network satisfaction problem that is either in P or NP-hard, with the paper determining which.

Reference graph

Works this paper leans on

35 extracted references · 34 canonical work pages · cited by 1 Pith paper

  1. [1]

    We conjecture that there are first-order sentences ϕ such that Her( ϕ) is coNP-intermediate (assuming P ̸= NP)

    work page

  2. [2]

    Is every finite-domain CSP which is in Her-FO also in P? Prove this without complexity- theoretic assumptions

    work page

  3. [3]

    Characterize the finite-domain CSPs in Her-FO

    work page

  4. [4]

    Is every CSP in Her-FO also of the form Her( ϕ) for some negative connected sentence ϕ?

    work page

  5. [5]

    7 References

    It it true that the tractability problem for Her-FO is undecidable even for first-order sentences with quantifier prefix ∃∃∀ (assuming P ̸= NP)? Compare to Corollary 4.3 and to the first item of Theorem 5.10. 7 References

    work page

  6. [6]

    Ackermann

    W. Ackermann. Beitr¨ age zum Entscheidungsproblem der mathematischen Logik. Mathema- tische Annalen, 112(1):419–432, 1936

    work page 1936

  7. [7]

    Bannach, F

    M. Bannach, F. Chudigiewitsch, and T. Tantau. On the Descriptive Complexity of Vertex Deletion Problems. In R. Kr´ aloviˇ c and A. Kuˇ cera, editors,49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024) , volume 306 of Leibniz In- ternational Proceedings in Informatics (LIPIcs) , pages 17:1–17:14, Dagstuhl, Germany, 2024...

    work page 2024

  8. [8]

    Bernays and M

    P. Bernays and M. Sch¨ onfinkel. Zum Entscheidungsproblem der mathematischen Logik.Math- ematische Annalen, 99:342–372, 1928

    work page 1928

Show all 35 references
  1. [10]

    Bodirsky

    M. Bodirsky. Complexity of Infinite-Domain Constraint Satisfaction . Lecture Notes in Logic (52). Cambridge University Press, Cambridge, United Kingdom; New York, NY, 2021

    2021

  2. [11]

    Bodirsky and J

    M. Bodirsky and J. K´ ara. A fast algorithm and Datalog inexpressibility for temporal reasoning. ACM Transactions on Computational Logic , 11(3), 2010

    2010

  3. [12]

    Bodirsky, S

    M. Bodirsky, S. Kn¨ auer, and S. Rudolph. Datalog-expressibility for monadic and guarded second-order logic. In 48th International Colloquium on Automata, Languages, and Program- ming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference) , pages 120:1– 120:17, ...

    2021

  4. [13]

    J. A. Bondy and U. S. R. Murty. Graph Theory. Springer, Berlin, 2008

    2008

  5. [14]

    B¨ orger, E

    E. B¨ orger, E. Gr¨ adel, and Y. Gurevich. The Classical Decision Problem . Perspectives in Mathematical Logic. Springer, 1997

    1997

  6. [15]

    Ebbinghaus and J

    H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer, Berlin, Heidelberg, New York,

  7. [16]

    Eiter, G

    T. Eiter, G. Gottlob, and T. Schwentick. The Model Checking Problem for Prefix Classes of Second-Order Logic: A Survey, pages 227–250. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010

    2010

  8. [17]

    Feder and M

    T. Feder and M. Y. Vardi. The computational structure of monotone monadic SNP and con- straint satisfaction: a study through Datalog and group theory. SIAM Journal on Computing , 28(1):57–104, 1999

    1999

  9. [18]

    Feder and M

    T. Feder and M. Y. Vardi. Homomorphism closed vs. existential positive. In Proceedings of the Symposium on Logic in Computer Science (LICS) , pages 311–320, 2003

    2003

  10. [19]

    Fomin, P

    F. Fomin, P. Golovach, and D. Thilikos. On the parameterized complexity of graph modifica- tion to first-order logic properties. Theory of Computing Systems , 64:251–271, 2020

    2020

  11. [20]

    T. Fujito. A unified approximation algorithm for node-deletion problems. Discrete Applied Mathematics, 86(2):213–231, 1998

    1998

  12. [21]

    Gottlob, P

    G. Gottlob, P. G. Kolaitis, and T. Schwentick. Existential second-order logic over graphs: Charting the tractability frontier. Journal of the ACM , 51:312–362, 2004

    2004

  13. [22]

    W. Hodges. A shorter model theory . Cambridge University Press, Cambridge, 1997

    1997

  14. [23]

    M. S. Krishnamoorthy and N. Deo. Node-deletion np-complete problems. SIAM Journal on Computing, 8(4):619–625, 1979

    1979

  15. [24]

    J. M. Lewis and M. Yannakakis. The node-deletion problem for hereditary properties is np- complete. Journal of Computer and System Sciences , 20(2):219–230, 1980. 16

    1980

  16. [25]

    Raman, S

    V. Raman, S. Saurabh, and C. R. Subramanian. Faster fixed parameter tractable algorithms for finding feedback vertex sets. ACM Trans. Algorithms, 2(3):403–415, July 2006

    2006

  17. [26]

    B. Reed, K. Smith, and A. Vetta. Finding odd cycle transversals. Operations Research Letters, 32(4):299–301, 2004

    2004

  18. [27]

    D. J. Rose. Triangulated graphs and the elimination process. Journal of Mathematical Analysis and Applications, 32:597–609–2:58, 1970

    1970

  19. [28]

    D. J. Rose, R. E. Tarjan, and G. S. Lueker. Algorithmic aspects of vertex elimination on graphs. SIAM Journal on Computing , 5(2):266–283, 1976

    1976

  20. [29]

    Trakhtenbrot

    B. Trakhtenbrot. The impossibility of an algorithm for the decidability problem on finite classes. Proceedings of the USSR Academy of Sciences , 70(4):569–572, 1950. (in Russian). A Examples A.1 Polynomial-time solvable examples Example 3 shows that CSP( Q, <) is in Her-FO but...

    1950

  21. [30]

    , vn we find a substructure of D that models ϕ; namely, the substructure with vertex set {v1,

    In the former case, D clearly satisfies ϕ, and in the latter, by choosing the shortest such path v1, . . . , vn we find a substructure of D that models ϕ; namely, the substructure with vertex set {v1, . . . , vn}. Therefore, if D ̸→ ⃗P3, then D ̸∈ Her(¬ϕ). The following is an ...

  22. [31]

    s1, s2, s3 and t1, t2, t3 are directed cycles in T

  23. [32]

    t3, t, s1 is a directed cycle for every t ∈ T \ {s1, s2, t2, t3}

  24. [33]

    There is an edge E(t2, t) and E(s, s2) for every t ∈ T \ {t1, t2} and every s ∈ T \ {s2, s3}

  25. [34]

    Every edge ( s, t) ̸= (s1, t3) belongs to at most 2 directed 3-cycles

  26. [35]

    At most 2 edges of every directed 3-cycle belong to 2 different directed 3-cycles

  27. [36]

    x1 x2 x3 y1 y2 y3 z̸∈{x1,x2,y2,y3} Figure 2: A partial depiction of the first three lines of ϕ

    Every directed 3-cycle that does not contain the edge ( s1, t3) contains exactly 2 edges that belong to 2 different directed 3-cycles. x1 x2 x3 y1 y2 y3 z̸∈{x1,x2,y2,y3} Figure 2: A partial depiction of the first three lines of ϕ. Lemma A.2. If a tournament T belongs to the He...

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.