Alexander Bentkamp
email: a.bentkamp@vu.nl

Jasmin Blanchette
email: j.c.blanchette@vu.nl

Sophie Tourret
email: sophie.tourret@inria.fr

Petar Vukmirović
email: p.vukmirovic@vu.nl

Superposition for Full Higher-Order Logic

We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus's two predecessors, new challenges arise from the interplay between λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.

Introduction

Superposition is a leading calculus for first-order logic with equality. We have been wondering for some years whether it would be possible to gracefully generalize it to extensional higher-order logic and use it as the basis of a strong higher-order automatic theorem prover. Towards this goal, we have, together with colleagues, designed superposition-like calculi for three intermediate logics between first-order and higherorder logic. Now we are finally ready to assemble a superposition calculus for full higher-order logic. The filiation of our new calculus from Bachmair and Ganzinger's standard first-order superposition is as follows:

Standard superposition Bachmair and Ganzinger [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF] (Sup) Superposition with ← → and delayed CNF Ganzinger and Stuber [START_REF] Ganzinger | Superposition with equivalence reasoning and delayed clause normal form transformation[END_REF] (← →Sup)

Superposition with Booleans Nummelin et al. [START_REF] Nummelin | Superposition with first-class Booleans and inprocessing clausification[END_REF] (oSup)

Boolean-free λ-free superposition Bentkamp et al. [START_REF] Bentkamp | Superposition for lambda-free higher-order logic[END_REF] (λfSup)

Boolean-free λ-superposition Bentkamp et al. [START_REF] Bentkamp | Superposition with lambdas[END_REF] (λSup)

Boolean λ-superposition This paper (oλSup)

Our goal was to devise an efficient calculus for higher-order logic. To achieve it, we pursued two objectives. First, the calculus should be refutationally complete. Second, the calculus should coincide as much as possible with its predecessors oSup and λSup on the respective fragments of higher-order logic (which in turn essentially coincide with Sup on first-order logic). Achieving these objectives is the main contribution of this paper. We made an effort to keep the calculus simple, but often the refutational completeness proof forced our hand to add conditions or special cases.

Like oSup, our calculus oλSup operates on clauses that can contain Boolean subterms, and it interleaves clausification with other inferences. Like λSup, oλSup eagerly βη-normalizes terms, employs full higher-order unification, and relies on a fluid subterm superposition rule (FLUIDSUP) to simulate superposition inferences below applied variables-i.e., terms of the form y t 1 . . . t n for n ≥ 1.

Because oSup contains several superposition-like inference rules for Boolean subterms, our completeness proof requires dedicated fluid Boolean subterm hoisting rules (FLUIDBOOLHOIST, FLUIDLOOBHOIST), which simulate Boolean inferences below applied variables, in addition to FLUIDSUP, which simulates superposition inferences.

Due to restrictions related to the term order that parameterizes superposition, it is difficult to handle variables bound by unclausified quantifiers if these variables occur applied or in arguments of applied variables. We solve the issue by replacing such quantified terms ∀y. t by equivalent terms (λy.

t) ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ (λy.
) in a preprocessing step. We implemented our calculus in the Zipperposition prover and evaluated it on TPTP and Sledgehammer benchmarks. The new Zipperposition outperforms all other higherorder provers and is on a par with an ad hoc implementation of Booleans in the same prover by Vukmirović and Nummelin [START_REF] Vukmirović | Boolean reasoning in a higher-order superposition prover[END_REF]. We refer to the technical report [START_REF] Bentkamp | Superposition for full higherorder logic[END_REF] for the completeness proof and a more detailed account of the calculus and its evaluation.

Logic

Our logic is higher-order logic (simple type theory) with rank-1 polymorphism, Hilbert choice, and functional and Boolean extensionality. Its syntax mostly follows Gordon and Melham [START_REF]Introduction to HOL: A Theorem Proving Environment for Higher Order Logic[END_REF]. We use the notation ān or ā to stand for the tuple (a 1 , . . . , a n ) where n ≥ 0. Deviating from Gordon and Melham, type arguments are explicit, written as c τm for a symbol c : Π ᾱm . υ and types τm . In the type signature Σ ty , we require the presence of a nullary Boolean type constructor o and a binary function type constructor →. In the term signature Σ, we require the presence of the logical symbols ,

⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬, ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧, ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨, → → → → → → → → → → → → → → → → → → → → → → → → →, ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀, ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃, ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈, and ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈.
The logical symbols are shown in bold to distinguish them from the notation used for clauses below. Moreover, we require the presence of the Hilbert choice operator ε ∈ Σ. Although ε is interpreted in our semantics, we do not consider it a logical symbol. Our calculus will enforce the semantics of ε by an axiom, whereas the semantics of the logical symbols will be enforced by inference rules. We write V for the set of (term) variables. We use Henkin semantics, in the style of Fitting [START_REF] Fitting | Types, Tableaus, and Gödel's God[END_REF], with respect to which we can prove our calculus refutationally complete. In summary, our logic essentially coincides with the TPTP TH1 format [START_REF] Kaliszyk | TH1: The TPTP typed higher-order form with rank-1 polymorphism[END_REF].

We generally view terms modulo αβη-equivalence. When defining operations that need to analyze the structure of terms, however, we use a custom normal form as the default representative of a βη-equivalence class: The βηQ η -normal form t ↓ βηQ η of a term t is obtained by bringing the term into η-short β-normal form and finally applying the rewrite rule Q τ s -→ Q η Q τ (λx. s x) exhaustively whenever s is not a λexpression. Here and elsewhere, Q stands for either

∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ or ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃.
On top of the standard higher-order terms, we install a clausal structure that allows us to formulate calculus rules in the style of first-order superposition. A literal s ≈ t is an equation s ≈ t or disequation s ≈ t of terms s and t; both equations and disequations are unordered pairs. A clause L 1 ∨ • • • ∨ L n is a finite multiset of literals L j . The empty clause is written as ⊥. This clausal structure does not restrict the logic, because an arbitrary term t of Boolean type can be written as the clause t ≈ .

We considered excluding negative literals by encoding them as [START_REF] Ganzinger | Superposition with equivalence reasoning and delayed clause normal form transformation[END_REF]. However, this approach would make the conclusion of the equality factoring rule (EFACT) too large for our purposes. Regardless, the simplification machinery will allow us to reduce negative literals

(s ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ t) ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, fol- lowing ← →Sup
t ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ and t ≈ to t ≈ and t ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥
, respectively, thereby eliminating redundant representations of nonequational literals.

We let CSU(s, t) denote an arbitrary (preferably, minimal) complete set of unifiers for two terms s and t on the set of free variables of the clauses in which s and t occur. To compute such sets, Huet-style preunification [START_REF] Huet | A mechanization of type theory[END_REF] is not sufficient, and we must resort to a full unification procedure [START_REF] Jensen | Mechanizing ω-order type theory through unification[END_REF][START_REF] Vukmirović | Efficient full higher-order unification[END_REF]. To cope with the nontermination of such procedures, we use dovetailing as described by Vukmirović et al. [START_REF] Vukmirović | Making higher-order superposition work[END_REF]Sect. 5].

Some of the rules in our calculus introduce Skolem symbols, representing objects mandated by existential quantification. We assume that these symbols do not occur in the input problem. More formally, given a problem over a term signature Σ, our calculus operates on a Skolem-extended term signature Σ sk that, in addition to all symbols from Σ, inductively contains symbols sk Π ᾱ. ∀ x. ∃z. t z : Π ᾱ. τ → υ for all types υ, variables z : υ, and terms t : υ → o over Σ sk , where ᾱ are the free type variables occurring in t and x : τ are the free term variables occurring in t, both in order of first occurrence.

The Calculus

The oλSup calculus closely resembles λSup, augmented with rules for Boolean reasoning that are inspired by oSup. As in λSup, superposition-like inferences are restricted to certain first-order-like subterms, the green subterms, which we define inductively as follows: Every term t is a green subterm of t, and for all symbols

f ∈ Σ \ {∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀, ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃}, if t
is a green subterm of u i for some i, then t is a green subterm of f τ ū. For example, the green subterms of f (g

(¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ p)) (∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ τ (λx. q)) (y a) (λx. h b) are the term itself, g (¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ p), ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ p, p, ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ τ (λx. q),
y a, and λx. h b. We write s t to denote a term s with a green subterm t and call the first-order-like context s a green context. Following λSup, we call a term t fluid if (1) t ↓ βηQ η is of the form y ūn where n ≥ 1, or (2) t ↓ βηQ η is a λ-expression and there exists a substitution σ such that tσ↓ βηQ η is not a λ-expression (due to η-reduction). Intuitively, fluid terms are terms whose normal form can change radically as a result of instantiation.

We define deeply occurring variables as in λSup, but exclude λ-expressions directly below quantifiers: A variable occurs deeply in a clause C if it occurs inside an argument of an applied variable or inside a λ-expression that is not directly below a quantifier.

Preprocessing. Our completeness theorem requires that quantified variables do not appear in certain higher-order contexts. We use preprocessing to eliminate problematic occurrences of quantifiers. The rewrite rules

∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ≈ and ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ≈ , which we collectively denote by Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ , are defined as ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ τ -→ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ≈ λy. y ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ (λx. ) and ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ τ -→ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ≈ λy. y ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ (λx. ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥)
where the rewritten occurrence of Q τ is unapplied or has an argument of the form λx. v such that x occurs as a nongreen subterm of v. If either of these rewrite rules can be applied to a given term, the term is

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -reducible; otherwise, it is Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normal.
For example, the term λy.

∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ι → ι (λx. g x y (z y) (f x)) is Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normal. A term may be Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -reducible because a quantifier appears unapplied (e.g., g ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ι ); a quantified variable occurs applied (e.g., ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ι → ι (λx. x a)); a quantified variable occurs inside a nested λ- expression (e.g., ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ι (λx. f (λy. x)))
; or a quantified variable occurs in the argument of a variable, either a free variable (e.g.,

∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ι (λx. z x))
or a variable bound above the quantifier (e.g., λy.

∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ι (λx. y x)). A preprocessor Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normalizes the input problem. Although inferences may pro- duce Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -reducible clauses, we do not Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normalize during the derivation process it- self. Instead, Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -
reducible ground instances of clauses will be considered redundant by the redundancy criterion. Thus, clauses whose ground instances are all

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -reducible can be deleted. However, there are Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -reducible clauses, such as x ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ι ≈ a, that nev- ertheless have Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈
≈ ≈ ≈ ≈ ≈ -normal ground instances. Such clauses must be kept because the completeness proof relies on their

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normal ground instances.
In principle, we could omit the side condition of the

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -
rewrite rules and eliminate all quantifiers. However, the calculus (especially, the redundancy criterion) performs better with quantifiers than with λ-expressions, which is why we restrict

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -
normalization as much as the completeness proof allows. Extending the preprocessing to eliminate all Boolean terms as in Kotelnikov et al. [START_REF] Kotelnikov | A clausal normal form translation for FOOL[END_REF] does not work for higher-order logic because Boolean terms can contain variables bound by enclosing λ-expressions.

Term Order. The calculus is parameterized by a well-founded strict total order on ground terms satisfying these four criteria: (O1) compatibility with green contextsi.e., s s implies t s t s ; (O2) green subterm property-i.e. t s s where is the reflexive closure of ;

(O3) u ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ for all terms u / ∈ { , ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥}; (O4) Q τ t t
u for all types τ, terms t, and terms u such that Q τ t and u are

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -
normal and the only Boolean green subterms of u are and

⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥. The restriction of (O4) to Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈
≈ ≈ ≈ ≈ ≈ -normal terms ensures that term orders fulfilling the requirements exist, but it forces us to preprocess the input problem. We extend to literals and clauses via the multiset extensions in the standard way [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF]Sect. 2.4].

For nonground terms, is required to be a strict partial order such that t s implies tθ sθ for all grounding substitutions θ. As in λSup, we also introduce a nonstrict variant for which we require that tθ sθ for all grounding substitutions θ whenever t s, and similarly for literals and clauses.

To construct a concrete order fulfilling these requirements, we define an encoding into untyped first-order terms, and compare these using a variant of the Knuth-Bendix order. In a first step, denoted O, the encoding translates fluid terms t as fresh variables z t ; nonfluid λ-expressions λx : τ.

u as lam(O(τ),O(u)); applied quantifiers Q τ (λx : τ. u) as Q 1 (O(τ),O(u)); and other terms f τ ūk as f k (O(τ),O(ū k ))
. Bound variables are encoded as constants db i corresponding to De Bruijn indices. In a second step, denoted P , the encoding replaces Q 1 by Q 1 and variables z by z whenever they occur below lam. For example,

∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ι (λx. p y y (λu. f y y (∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ι (λv. u)))) is encoded as ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ 1 (ι, p 3 (y, y, lam(o, f 3 (y , y , ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ 1 (ι, db 1 ))))
). The first-order terms can then be compared using a transfinite Knuth-Bendix order kb [START_REF] Ludwig | An extension of the Knuth-Bendix ordering with LPO-like properties[END_REF]. Let the weight of

∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ 1 and ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ 1 be ω, the weight of 0 and ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 be 1,
and the weights of all other symbols be less than ω. Let the precedence > be total and

⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 , 0 be the symbols of lowest precedence, with ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 > 0 . Then let t s if O(P (t)) kb O(P (s)) and t s if O(P (t)) kb O(P (s)).
Selection Functions. The calculus is also parameterized by a literal selection function and a Boolean subterm selection function. We define an element x of a multiset M to be -maximal for some relation if for all y ∈ M with y x, we have y = x. It is strictly -maximal if it is -maximal and occurs only once in M.

The literal selection function HLitSel maps each clause to a subset of selected literals. A literal may not be selected if it is positive and neither side is

⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥.
Moreover, a literal L y may not be selected if y ūn , with n ≥ 1, is a -maximal term of the clause.

The Boolean subterm selection function HBoolSel maps each clause C to a subset of selected subterms in C. Selected subterms must be green subterms of Boolean type. Moreover, a subterm s must not be selected

if s = , if s = ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, if s is a variable-headed term, if
s is at the topmost position on either side of a positive literal, or if s contains a variable y as a green subterm, and y ūn , with n ≥ 1, is a -maximal term of the clause.

Eligibility. A literal L is (strictly) eligible w.r.t. a substitution σ in C if it is selected in C or there are no selected literals and no selected Boolean subterms in C and Lσ is (strictly) -maximal in Cσ.

The eligible subterms of a clause C w.r.t. a substitution σ are inductively defined as follows: Any selected subterm is eligible. If a literal L = s ≈ t with sσ tσ is either eligible and negative or strictly eligible and positive, then the subterm s is eligible. If a subterm t is eligible and the head of

t is not ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ or ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈, all direct green subterms of t are eligible. If a subterm t is eligible and t is of the form u ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ v or u ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ v, then u is eligible if uσ vσ and v is eligible if uσ vσ.
The Core Inference Rules. The calculus consists of the following core inference rules. The first five rules stem from λSup, with minor adaptions concerning Booleans: The following rules are concerned with Boolean reasoning and originate from oSup.

D D ∨ t ≈ t C u SUP (D ∨ C t )σ C C ∨ u ≈ u ERES C σ C C ∨ u ≈ v ∨ u ≈ v EFACT (C ∨ v ≈ v ∨ u ≈ v )σ D D ∨ t ≈ t C u FLUIDSUP (D ∨ C z t )σ C C ∨ s ≈ s ARGCONG C σ ∨ sσ xn ≈ s σ xn SUP 1. u is not fluid; 2. u is not a variable deeply occurring in C; 3. if u is a variable y,
σ = ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥,
They have been adapted to support polymorphism and applied variables.

C u BOOLHOIST (C ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ u ≈ )σ C u EQHOIST (C ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ x ≈ y)σ C u NEQHOIST (C ∨ x ≈ y)σ C u FORALLHOIST (C ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ y x ≈ )σ C u EXISTSHOIST (C ∨ y x ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥)σ C C ∨ s ≈ s FALSEELIM C σ C u BOOLRW C t σ C u FORALLRW C y (sk Π ᾱ. ∀ x. ∃z. ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬yσ z ᾱ x) σ C u EXISTSRW C y (sk Π ᾱ. ∀ x. ∃z. yσ z ᾱ x) σ BOOLHOIST 1.
σ is a type unifier of the type of u with the Boolean type o (i.e., the identity if u is Boolean or {α → o} if u is of type α for some type variable α); 2. the head of u is neither a variable nor a logical symbol; 3. u is eligible in C; 4. the occurrence of u is not at the top level of a positive literal. EQHOIST, NEQHOIST, FORALLHOIST, EXISTSHOIST 1.

σ ∈ CSU(u, x ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y), σ ∈ CSU(u, x ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y), σ ∈ CSU(u, ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ α y), or σ ∈ CSU(u, ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ α y), respectively; 2.
x, y, and α are fresh variables; 3. u is eligible in C w.r.t. σ; 4. if the head of u is a variable, it must be applied and the affected literal must be of the form u ≈ ,

u ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, or u ≈ v where v is a variable-headed term. FALSEELIM 1. σ ∈ CSU(s ≈ s , ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ ); 2. s ≈ s is strictly eligible in C w.r.t. σ.
BOOLRW 1. σ ∈ CSU(t, u) and (t, t ) is one of the following pairs, where y is a fresh variable:

(¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, ), (¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ , ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥), (⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥), ( ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥), (⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ , ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥), ( ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ , ), (⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥), ( ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, ), (⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ , ), ( ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ , ), (⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ → → → → → → → → → → → → → → → → → → → → → → → → → ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, ), ( → → → → → → → → → → → → → → → → → → → → → → → → → ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥), (⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ → → → → → → → → → → → → → → → → → → → → → → → → → , ), ( → → → → → → → → → → → → → → → → → → → → → → → → → , ), (y ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y, ), (y ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y, ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥); 2.
u is not a variable; 3. u is eligible in C w.r.t. σ; 4. if the head of u is a variable, it must be applied and the affected literal must be of the form

u ≈ , u ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, or u ≈ v where v is a variable-headed term. FORALLRW, EXISTSRW 1. σ ∈ CSU(∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ β y, u) and σ ∈ CSU(∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ β y, u)
, respectively, where β is a fresh type variable, y is a fresh term variable, ᾱ are the free type variables and x are the free term variables occurring in yσ in order of first occurrence; 2. u is not a variable; 3. u is eligible in C w.r.t. σ; 4. if the head of u is a variable, it must be applied and the affected literal must be of the form u

≈ , u ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, or u ≈ v
where v is a variable-headed term; 5. for FORALLRW, the indicated occurrence of u is not in a literal u ≈ , and for EXISTSRW, the indicated occurrence of u is not in a literal u

≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥.
Like SUP, also the Boolean rules must be simulated in fluid terms. The following rules are Boolean counterparts of FLUIDSUP:

C u FLUID- BOOLHOIST (C z ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ x ≈ )σ C u FLUID- LOOBHOIST (C z ∨ x ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥)σ
FLUIDBOOLHOIST 1. u is fluid; 2. z and x are fresh variables; 3. σ ∈ CSU(z x, u);

4. (z ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥)σ = (z x)σ; 5. xσ = and xσ = ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥; 6. u is eligible in C w.r.t. σ. FLUIDLOOBHOIST Like the above but with ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ replaced by in condition 4.
In addition to the inference rules, our calculus relies on two axioms, below. Axiom (EXT), from λSup, embodies functional extensionality; the expression diff α, β abbreviates sk Πα β. ∀z y. ∃x. z x ≈y x α, β . Axiom (CHOICE) characterizes the Hilbert choice operator ε.

z (diff α, β z y) ≈ y (diff α, β z y) ∨ z ≈ y (EXT) y x ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ y (ε α y) ≈ (CHOICE)
Rationale for the Rules. Most of the calculus's rules are adapted from its precursors. SUP, ERES, and EFACT are already present in Sup, with slightly different side conditions. Notably, as in λfSup and λSup, SUP inferences are required only into green contexts. Other subterms are accessed indirectly via ARGCONG and (EXT). The rules BOOLHOIST, EQHOIST, NEQHOIST, FORALLHOIST, EXISTSHOIST, FALSEELIM, BOOLRW, FORALLRW, and EXISTSRW, concerned with Boolean reasoning, stem from oSup, which was inspired by ← →Sup. Except for BOOLHOIST and FALSEELIM, these rules have a condition stating that "if the head of u is a variable, it must be applied and the affected literal must be of the form u

≈ , u ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥, or u ≈ v
where v is a variable-headed term." The inferences at variable-headed terms permitted by this condition are our form of primitive substitution [START_REF] Andrews | On connections and higher-order logic[END_REF][START_REF] Huet | A mechanization of type theory[END_REF], a mechanism that blindly substitutes logical connectives and quantifiers for variables z with a Boolean result type.

Example 1. Our calculus can prove that Leibniz equality implies equality (i.e., if two values behave the same for all predicates, they are equal) as follows:

a ≈ b z a ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ z b ≈ EQHOIST (x a ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y a) ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ ∨ x b ≈ y b BOOLRW ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ ∨ w a b b ≈ w b a b FALSEELIM ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ ∨ w a b b ≈ w b a b FALSEELIM w a b b ≈ w b a b SUP a ≈ a ERES ⊥
The EQHOIST inference, applied on z b, illustrates how our calculus introduces logical symbols without a dedicated primitive substitution rule. Although ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ does not appear in the premise, we still need to apply EQHOIST on z b with CSU(z b,

x 0 ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y 0 ) = {{z → λv. x v ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y v, x 0 → x b, y 0 → y b}}.
Other calculi [START_REF] Andrews | On connections and higher-order logic[END_REF][START_REF] Benzmüller | LEO-II-A cooperative automatic theorem prover for higher-order logic[END_REF][START_REF] Huet | A mechanization of type theory[END_REF][START_REF] Steen | The higher-order prover Leo-III[END_REF] would apply an explicit primitive substitution rule instead, yielding essentially

(xa ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ya) ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ (xb ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ yb) ≈ .
However, in our approach this clause is subsumed and could be discarded immediately. By hoisting the equality to the clausal level, we bypass the redundancy criterion.

Next, BOOLRW can be applied to

x a ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y a with CSU(x a ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y a, y 0 ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y 0 ) = {{x → λv. w a v v, y → λv. w v a v, y 0 → w a a a}}. The two FALSEELIM steps remove the ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ literals.
Then SUP is applicable with the unifier {w → λx 1 x 2 x 3 . x 2 } ∈ CSU(b, w a b b), and ERES derives the contradiction.

Like in λSup, the FLUIDSUP rule is responsible for simulating superposition inferences below applied variables, other fluid terms, and deeply occurring variables. Complementarily, FLUIDBOOLHOIST and FLUIDLOOBHOIST simulate the various Boolean inference rules below fluid terms. Initially, we considered adding a fluid version of each rule that operates on Boolean subterms, but we discovered that FLUID-BOOLHOIST and FLUIDLOOBHOIST suffice to achieve refutational completeness.

Example 2. The clause set consisting of h (y b)

≈ h (g ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥) ∨ h (y a) ≈ h (g )
and a ≈ b highlights the need for FLUIDBOOLHOIST and its companion. The set is unsatisfiable because the instantiation {y → λx. g

(x ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ a)} produces the clause h (g (b ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ a)) ≈ h (g ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥) ∨ h (g (a ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ a)) ≈ h (g )
, which is unsatisfiable in conjunction with a ≈ b. The literal selection function can select either literal in the first clause. ERES is applicable in either case, but the unifiers {y → λx.

g ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥}
and {y → λx. g } do not lead to a contradiction. Instead, we need to apply FLUIDBOOLHOIST if the first literal is selected or FLUIDLOOBHOIST if the second literal is selected. In the first case, the derivation is as follows:

a ≈ b h (y b) ≈ h (g ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥) ∨ h (y a) ≈ h (g ) FLUIDBOOLHOIST h (z b ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥) ≈ h (g ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥) ∨ h (z a (x a)) ≈ h (g ) ∨ x b ≈ ERES h (g (x a)) ≈ h (g ) ∨ x b ≈ EQHOIST h (g (x a ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ x a)) ≈ h (g ) ∨ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ ∨ x b ≈ x b SUP h (g (a ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ x a)) ≈ h (g ) ∨ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ ∨ a ≈ x b BOOLRW h (g ) ≈ h (g ) ∨ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ ∨ a ≈ a ERES ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ ∨ a ≈ a ERES ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ≈ FALSEELIM ⊥
The FLUIDBOOLHOIST inference uses the unifier {y → λu. z u (x u), z → λu.z b u, x → x b} ∈ CSU(z x, y b). We apply ERES to the first literal of the resulting clause, with unifier {z → λuv.

g v} ∈ CSU(h (z b ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥), h (g ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥))
. Next, we apply EQHOIST with the unifier {x → λu. The two sides of the interpreted equality in the first literal can then be unified, allowing us to apply BOOLRW with the unifier {y → a, x → λu. a} ∈ CSU(y

x u ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ x u, w → x b, w → x b} ∈ CSU(x b, w ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ w )
≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ y, a ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ x b).
Finally, applying ERES twice and FALSEELIM once yields the empty clause.

Remarkably, none of the provers that participated in the CASC-J10 competition can solve this two-clause problem within a minute. Satallax finds a proof after 72 s and LEO-II after over 7 minutes. Our new Zipperposition implementation solves it in 3 s.

The Redundancy Criterion. In first-order superposition, a clause is considered redundant if all its ground instances are entailed by ≺-smaller ground instances of other clauses. In essence, this will also be our definition, but we will use a different notion of ground instances and a different notion of entailment.

Given a clause C, let its ground instances G(C) be the set of all clauses of the form Cθ for some substitution θ such that Cθ is ground and

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normal,
and for all variables x occurring in C, the only Boolean green subterms of xθ are and

⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥.
The rationale of this definition is to ensure that ground instances of the conclusion of FORALLHOIST, EX-ISTSHOIST, FORALLRW, and EXISTSRW inferences are smaller than the corresponding instances of their premise by property (O4).

The redundancy criterion's notion of entailment is defined via an encoding into a weaker logic, following λfSup and λSup. In this paper, the weaker logic is ground firstorder logic with interpreted Booleans-the ground fragment of the logic of oSup. Its signature (Σ ty , Σ GF ) is derived from our higher-order signature (Σ ty , Σ) as follows. The type constructors Σ ty are the same in both signatures, but → is an uninterpreted type constructor in first-order logic. For each ground instance f ῡ :

τ 1 → • • • → τ n → τ of a symbol f ∈ Σ,
we introduce a first-order symbol f ῡ j ∈ Σ GF with argument types τj and result type τ j+1 → • • • → τ n → τ, for each j. Moreover, for each ground term λx. t, we introduce a symbol lam λx. t ∈ Σ GF of the same type. The symbols

⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 , 0 , ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ 1 , ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ ∧ 2 , ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ 2 , → → → → → → → → → → → → → → → → → → → → → → → → → 2 , ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ τ 2 , and ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ τ
2 are identified with the corresponding first-order logical symbols.

We define an encoding

F of Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈
≈ ≈ ≈ ≈ ≈ -normal ground higher-order terms into this ground first-order logic recursively as follows:

F (∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ τ (λx. t)) = ∀x. F (t) and F (∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ τ (λx. t)) =
∃x. F (t) for applied quantifiers; F (λx. t) = lam λx. t for λ-expressions; and F (f ῡ sj ) = f ῡ j (F ( sj )) for other terms. For quantified variables, we define F (x) = x. Here,

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈
≈ ≈ ≈ ≈ ≈normality is crucial to ensure that bound variables do not occur applied or within λexpressions. The definition of green subterms is devised such that green subterms correspond to first-order subterms via the encoding F , with the exception of first-order subterms below quantifiers. The encoding F is extended to clauses by mapping each literal and each side of a literal individually. From the entailment relation |= for the ground first-order logic, we derive an entailment relation

|= F on Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normal ground higher-order clauses by defining M |= F N if F (M) |= F (N).
This relation is weaker than standard higher-order entailment; for example, {f ≈ g} |= F {f a ≈ g a} (because of the subscripts added by F ) and {p (λx. For first-order superposition, an inference is considered redundant if for each of its ground instances, a premise is redundant or the conclusion is entailed by clauses smaller than the main premise. For most inference rules, our definition follows this idea, using |= F for entailment; other rules need nonstandard notions of ground instances and redundancy. The definition of inference redundancy presented below is simpler than the more sophisticated notion in our technical report. Nonetheless, the redundant inferences below are a strict subset of the redundant inferences of our report and thus completeness also holds using the notion below. For the few prover optimizations based on inference redundancy that we know about (e.g., simultaneous superposition [START_REF] Benanav | Simultaneous paramodulation[END_REF]), the following criterion suffices.

)} |= F {p (λx. ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥)} (
For SUP, ERES, EFACT, BOOLHOIST, FALSEELIM, EQHOIST, NEQHOIST, and BOOLRW, we define ground instances as usual: Ground instances are all inferences obtained by applying a grounding substitution to premises and conclusion such that the result adheres to the conditions of the given rule w.r.t. selection functions that select literals and subterms as in the original premise. For FLUIDSUP and FLUIDBOOLHOIST, we define ground instances in the same way except that we require that ground instances adhere to the conditions of SUP or BOOLHOIST, respectively. For FORALLRW, EXISTSRW, FORALLHOIST, EXISTSHOIST, which do not have ground instances in the sense above, we define a ground instance as any inference that is obtained by applying the unifier σ to the premise and then applying a grounding substitution to premise and conclusion, regardless of whether the resulting inference is an inference of our calculus.

For all rules except FLUIDLOOBHOIST and ARGCONG, we define an inference to be redundant w.r.t. a clause set N if for each ground instance ι, a premise of ι is redundant w.r.t. G(N) or the conclusion of ι is entailed w.r.t. |= F by clauses from G(N) that are smaller than the main (i.e., rightmost) premise of ι. For the rules FLUIDLOOB-HOIST and ARGCONG, as well as axioms (EXT) and (CHOICE)-viewed as premiseless inferences-we define an inference to be redundant w.r.t. a clause set N if all ground instances of its conclusion are contained in G(N) or redundant w.r.t. G(N).

We denote the set of redundant inferences w.r.t. N by Red I (N).

Simplification Rules. Our redundancy criterion is strong enough to support counterparts of most simplification rules implemented in Schulz's first-order E [25, Sect. 2.3.1 and 2.3.2]. Deletion of duplicated literals, deletion of resolved literals, syntactic tautology deletion, negative simplify-reflect, and clause subsumption adhere to our redundancy criterion. Positive simplify-reflect, equality subsumption, and rewriting (demodulation) of positive and negative literals are supported if they are applied on green subterms or on other subterms that are encoded into first-order subterms by G and F . Semantic tautology deletion can be applied as well, using |= F ; moreover, for positive literals, the rewriting clause must be smaller than the rewritten clause.

Under some circumstances, inference rules can be applied as simplifications. The FALSEELIM and BOOLRW rules can be applied as a simplification if σ is the identity.

If the head of u is ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀ ∀,
FORALLHOIST and FORALLRW can both be applied and, together, serve as one simplification rule. The same holds for EXISTSHOIST and EXISTSRW if the head of

u is ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃ ∃.
For all of these rules, the eligibility conditions can be ignored.

Clausification. Like oSup, our calculus does not require the input problem to be clausified during the preprocessing, and it supports higher-order analogues of the three inprocessing clausification methods introduced by Nummelin et al. Inner delayed clausification relies on our core calculus rules to destruct logical symbols. Outer delayed clausification adds the following clausification rules to the calculus:

s ≈ ∨ C POSOUTERCLAUS oc(s,C) s ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ C NEGOUTERCLAUS oc(¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬s,C) s ≈ t ∨ C EQOUTERCLAUS s ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ t ≈ ∨ C s ≈ ∨ t ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ C s ≈ t ∨ C NEQOUTERCLAUS s ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ t ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ C s ≈ ∨ t ≈ ∨ C
The double bars identify simplification rules (i.e., the conclusions make the premise redundant and can replace it). The first two rules require that s has a logical symbol as its head, whereas the last two require that s and t are Boolean terms other than and

⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥.
The function oc distributes the logical symbols over the clause C-e.g., oc(s

→ → → → → → → → → → → → → → → → → → → → → → → → → t, C) = {s ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ t ≈ ∨ C}, and oc(¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬ ¬(s ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ t), C) = {s ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ C, t ≈ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ∨ C}.
It is easy to check that our redundancy criterion allows us to replace the premise of the OUTERCLAUS rules with their conclusion. Nonetheless, we apply EQOUTERCLAUS and NEQOUTERCLAUS as inferences because the premises might be useful in their original form.

Besides the two delayed clausification methods, a third inprocessing clausification method is immediate clausification. This clausifies the input problem's outer Boolean structure in one swoop, resulting in a set of higher-order clauses. If unclausified Boolean terms rise to the top during saturation, the same algorithm is run to clausify them.

Unlike delayed clausification, immediate clausification is a black box and is unaware of the proof state other than the Boolean term it is applied to. Delayed clausification, on the other hand, clausifies the term step by step, allowing us to interleave clausification with the strong simplification machinery of superposition provers. It is especially powerful in higher-order contexts: Examples such as y p q ≈ (p

∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ ∨ q
) can be refuted directly by equality resolution, rather than via more explosive rules on the clausified form.

Refutational Completeness

Our calculus is dynamically refutationally complete for problems in

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normal form.
The full proof can be found in our technical report [START_REF] Bentkamp | Superposition for full higherorder logic[END_REF].

Theorem 3 (Dynamic refutational completeness). Let (N i ) i be a derivation-i.e.,

N i \ N i+1 ⊆ Red C (N i+1 ) for all i. Let N 0 be Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈
≈ ≈ ≈ ≈ ≈ -normal and such that N 0 |= ⊥. Moreover, assume that (N i ) i is fair-i.e., all inferences from clauses in the limit inferior i j≥i N j are contained in i Red I (N i ). Then we have ⊥ ∈ N i for some i.

Following the completeness proof of λSup, our proof is structured in three levels of logics. For each, we define a calculus and show that it is refutationally complete: ground monomorphic first-order logic with an interpreted Boolean type (GF); the

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈
≈ ≈ ≈ ≈ ≈ -normal ground fragment of higher-order logic (GH); and higher-order logic (H).

The logic of the GF level is the ground fragment of oSup's logic. The GF calculus is a ground version of oSup, which Nummelin et al. showed refutationally complete. It consists of ground first-order equivalents of our rules, excluding ARGCONG, FLUID-BOOLHOIST, and FLUIDLOOBHOIST, which are specific to higher-order logic. The counterparts to FORALLHOIST and EXISTSHOIST enumerate ground terms instead of producing free variables, to stay within the ground fragment. For compatibility with the nonground level, the conclusions of FORALLRW and EXISTSRW cannot contain concrete Skolem functions. Instead, the GF calculus is parameterized by a witness function that can assign an arbitrary term to each occurrence of a quantifier in a clause. This witness function is used to retrieve the Skolem terms in the GF equivalents of FORALLRW and EXISTSRW.

On the next level, the GH calculus includes inference rules isomorphic to the GF rules, transferred to higher-order logic via F -1 . Moreover, it contains an ARGCONG variant that enumerates ground terms instead of introducing fresh variables, as well as rules enumerating ground instances of axioms (EXT) and (CHOICE). We prove refutational completeness of the GH calculus by constructing a higher-order interpretation based on the model constructed for the completeness proof of the GF level. This proof step is analogous to the corresponding step in λSup's proof, but we must also consider

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈
≈ ≈ ≈ ≈ ≈ -normality and the logical symbols.

To lift completeness to the H level, we use the saturation framework of Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]. The main proof obligation it leaves us to show is that nonredundant GH inferences can be lifted to corresponding nonground H inferences. For this lifting, we must choose a suitable GH witness function and appropriate GH selection functions for literals and Boolean subterms, given a saturated clause set at the H level and the H selection functions. Then the saturation framework guarantees static refutational completeness w.r.t. Herbrand entailment, which is the entailment relation induced by the grounding function G. We then show that this implies dynamic refutational completeness w.r.t.

|= for Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normal initial clause sets.

Implementation

We implemented our calculus in the Zipperposition prover [START_REF] Cruanes | Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond[END_REF], whose OCaml source code makes it convenient to prototype calculus extensions. Except for the presence of axioms (EXT) and (CHOICE), the new code gracefully extends Zipperposition's implementation of oSup in the sense that oλSup coincides with oSup on first-order problems. The same cannot be said w.r.t. λSup on Boolean-free problems because of the FLUIDBOOLHOIST and FLUIDLOOBHOIST rules, which are triggered by any applied variable. From the implementation of λSup, we inherit the given clause procedure, which supports infinitely branching inferences, as well as calculus extensions and heuristics [START_REF] Vukmirović | Making higher-order superposition work[END_REF]. From the implementation of oSup, we inherit the simplification rule BOOLSIMP, a mainstay of our Boolean simplification machinery.

As in the implementation of λSup, we approximate fluid terms as terms that are either nonground λ-expressions or terms of the form x sn with n > 0. Two slight, accidental discrepancies are that we also count variable occurrences below quantifiers as deep and perform EFACT inferences even if the maximal literal is selected. Since we expect FLUIDBOOLHOIST and FLUIDLOOBHOIST to be highly explosive, we penalize them and all of their offspring. In addition to various λSup extensions [6, Sect. 5], we also use all the rules for Boolean reasoning described by Vukmirović and Nummelin [START_REF] Vukmirović | Boolean reasoning in a higher-order superposition prover[END_REF] except for the BOOLEF rules.

Evaluation

We evaluate the calculus implementation in Zipperposition and compare it with other higher-order provers. Our experiments were performed on StarExec Miami servers equipped with Intel Xeon E5-2620 v4 CPUs clocked at 2.10 GHz. We used all 2606 TH0 theorems from the TPTP 7.3.0 library [START_REF] Sutcliffe | The TPTP problem library and associated infrastructure-from CNF to TH0, TPTP v6.4.0[END_REF] and 1253 "Judgment Day" problems [START_REF] Böhme | Sledgehammer: Judgement Day[END_REF] generated using Sledgehammer (SH) [START_REF] Paulson | Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers[END_REF] as our benchmark set. An archive containing the benchmarks and the raw evaluation results is publicly available [START_REF] Bentkamp | Superposition for full higherorder logic[END_REF].

Calculus Evaluation. In this first part, we evaluate selected parameters of Zipperposition by varying only the studied parameter in a fixed well-performing configuration. This base configuration disables axioms (CHOICE) and (EXT) and the FLUID-rules. It uses the unification procedure of Vukmirović et al. [START_REF] Vukmirović | Efficient full higher-order unification[END_REF] in its complete variant-i.e., the variant that produces a complete set of unifiers. It uses none of the early Boolean rules described by Vukmirović and Nummelin [START_REF] Vukmirović | Boolean reasoning in a higher-order superposition prover[END_REF]. The preprocessor

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ is disabled as well.
All of the completeness-preserving simplification rules listed in Sect. 3 are enabled. The configuration uses immediate clausification. We set the CPU time limit to 30 s in all three experiments.

In the first experiment, we assess the overhead incurred by the FLUID-rules. These rules unify with a term whose head is a fresh variable. Thus, we expected that they needed to be tightly controlled to achieve good performance. To test our hypothesis, we simultaneously modified the parameters of these three rules. In Figure 1, the off mode simply disables the rules, the pragmatic mode uses a terminating incomplete unification algorithm (the pragmatic variant of Vukmirović et al. [START_REF] Vukmirović | Efficient full higher-order unification[END_REF]), and the complete mode uses a complete unification algorithm. The results show that disabling FLUIDrules altogether achieves the best performance. However, on TPTP problems, complete finds 35 proofs not found by off, and pragmatic finds 22 proofs not found by off. On Sledgehammer benchmarks, this effect is much weaker, likely because the Sledgehammer benchmarks require less higher-order reasoning: complete finds only one new proof over off, and pragmatic finds only four.

In the second experiment, we explore the clausification methods introduced at the end of Sect. 3: inner delayed clausification, outer delayed clausification, and immediate clausification. The modes inner and outer employ oSup's RENAME rule, which renames Boolean terms headed by logical symbols using a Tseitin-like transformation if they occur at least four times in the proof state. Vukmirović and Nummelin [START_REF] Vukmirović | Boolean reasoning in a higher-order superposition prover[END_REF] observed that outer clausification can greatly help prove higher-order problems, and we expected it to perform well for our calculus, too. The results are shown in Figure 2. The results confirm our hypothesis: The outer mode outperforms immediate on both TPTP and Sledgehammer benchmarks. The inner mode performs worst, but on Sledgehammer benchmarks, it proves 17 problems beyond the reach of the other two. Interestingly, several of these problems contain axioms of the form φ → → → → → → → → → → → → → → → → → → → → → → → → → ψ, and applying superposition and demodulation to these axioms is preferable to clausifying them.

In the third experiment, we investigate the effect of axiom (CHOICE), which is necessary to achieve refutational completeness. To evaluate (CHOICE), we either disabled it in a configuration labeled off or set the axiom's penalty p to different values. In Zipperposition, penalties are propagated through inference and simplification rules and are used to increase the heuristic weight of clauses, postponing the selection of penalized clauses. The results are shown in Figure 3. As expected, disabling (CHOICE), or at least penalizing it heavily, improves performance. Yet enabling (CHOICE) can be crucial: For 19 TPTP problems, the proofs are found when (CHOICE) is enabled and p = 4, but not when the rule is disabled. On Sledgehammer problems, this effect is weaker, with only two new problems proved for p = 4.

Prover Comparison. In this second part, we compare Zipperposition's performance with other higher-order provers. Like at CASC-J10, the wall-clock time limit was 120 s, the CPU time limit was 960 s, and the provers were run on StarExec Miami. We used the following versions of all systems that took part in the THF division: CVC4 1.8 [START_REF] Barrett | CVC4[END_REF], Leo-III 1.5.2 [START_REF] Steen | The higher-order prover Leo-III[END_REF], Satallax 3.5 [START_REF] Brown | Satallax: An automatic higher-order prover[END_REF], and Vampire 4.5 [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF]. The developers of Vampire have informed us that its higher-order schedule is optimized for running on a single core. As a result, the prover suffers some degradation of performance when running on multiple cores. We evaluate both the version of Zipperposition that took part in CASC-J10 (Zip) and the updated version of Zipperposition that supports our new calculus (New Zip). Zip's portfolio of prover configurations is based on λSup and techniques described by Vukmirović and Nummelin [START_REF] Vukmirović | Boolean reasoning in a higher-order superposition prover[END_REF]. New Zip's portfolio is specially designed for our new calculus and optimized for TPTP problems. To assess the performance of Boolean reasoning, we used Sledgehammer benchmarks generated both with native Booleans (SH) and with an encoding into Boolean-free higher-order logic (ofSH). For technical reasons, the encoding also performs λ-lifting, but this minor transformation should have little impact on results [START_REF] Bentkamp | Superposition with lambdas[END_REF]Sect. 7].

The results are shown in Figure 4. The two versions of Zipperposition are ahead of all other provers on both benchmark sets. This shows that, with thorough parameter tuning, higher-order superposition outperforms tableaux, which had been the state of the art in higher-order reasoning for a decade. The updated version of New Zip beats Zip on TPTP problems but lags behind Zip on Sledgehammer benchmarks as we have yet to further explore more general heuristics that work well with our new calculus. The Sledgehammer benchmarks fail to demonstrate the superiority of native Booleans reasoning compared with an encoding, and in fact CVC4 and Leo-III perform dramatically better on the encoded Boolean problems, suggesting that there is room for tuning.

Conclusion

We have created a superposition calculus for higher-order logic that is refutationally complete. Most of the key ideas have been developed in previous work by us and colleagues, but combining them in the right way has been challenging. A key idea was to

Q ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ ≈ -normalize away inconvenient terms.
Unlike earlier refutationally complete calculi for full higher-order logic based on resolution or paramodulation, our calculus employs a term order, which restricts the proof search, and a redundancy criterion, which can be used to add various simplification rules while keeping refutational completeness. These two mechanisms are undoubtedly major factors in the success of first-order superposition, and it is very fortunate that we could incorporate both in a higher-order calculus. An alternative calculus with the same two mechanisms could be achieved by combining oSup with Bhayat and Reger's combinatory superposition [START_REF] Bhayat | Set of support for higher-order reasoning[END_REF]. The article on λSup [6, Sect. 8] discusses related work in more detail.

The evaluation results show that our calculus is an excellent basis for higher-order theorem proving. In future work, we want to experiment further with the different parameters of the calculus (for example, with Boolean subterm selection heuristics) and implement it in a state-of-the-art prover such as E.

  to the literal created by FLUIDBOOLHOIST, effectively performing a primitive substitution. The resulting clause can superpose into a ≈ b with the unifier {x → λu. u} ∈ CSU(x b, b).

  because of the lam symbols used by F ).Using |= F , we define a clause C to be redundant w.r.t. a clause set N if for everyD ∈ G(C), we have {E ∈ G(N) | E ≺ D} |= F D or there exists a clause C ∈ N such that C C and D ∈ G(C ).The tiebreaker can be an arbitrary well-founded partial order on clauses; in practice, we use a well-founded restriction of the ill-founded strict subsumption relation[START_REF] Bentkamp | Superposition with lambdas[END_REF] Sect. 3.4]. We denote the set of redundant clauses w.r.t. a clause set N by Red C (N). Note that |= F is weak enough to ensure that the ARGCONG inference rule and axiom (EXT) are not immediately redundant and can fulfill their purpose.

  the subterm u is at the top level of a positive literal.ERES 1. σ ∈ CSU(u, u ); 2. u ≈ u is eligible in C w.r.t. σ. EFACT 1. σ ∈ CSU(u, u ); 2. uσ vσ; 3. (u ≈ v)σ is -maximal in Cσ; 4. uσ vσ;5. nothing is selected in C. FLUIDSUP 1. u is a variable deeply occurring in C or u is fluid; 2. z is a fresh variable;3. σ ∈ CSU(z t, u); 4. (z t )σ = (z t)σ; 5.-10. as for SUP. ARGCONG 1. n > 0; 2. σ is the most general type substitution that ensures welltypedness of the conclusion for a given n; 3. xn is a tuple of distinct fresh variables; 4. the literal s ≈ s is strictly eligible in C w.r.t. σ.

Acknowledgment. Uwe Waldmann provided advice and carefully checked the completeness proof. Visa Nummelin led the design of the oSup calculus. Simon Cruanes helped us with the implementation. Martin Desharnais generated the Sledgehammer benchmarks. Christoph Benzmüller, Ahmed Bhayat, Mathias Fleury, Herman Geuvers, Giles Reger, Alexander Steen, Mark Summerfield, Geoff Sutcliffe, and the anonymous reviewers helped us in various ways. We thank them all. Bentkamp, Blanchette, and Vukmirović's research has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Blanchette's research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).


Séverin Yvoz

Stéphane Cordeau

Camille Zuccolo

Sandrine Petit
email: sandrine.petit-michaut@inrae.fr

Crop type and within-field

Keywords: phenology, field edge, farming management, flowering success, pollination, pest control

Introduction

There is growing evidence that arable weeds provide habitat and resources that are of key value for the maintenance of biodiversity and the delivery of ecosystem services in agroecosystems [START_REF] Blaix | Quantification of regulating ecosystem services provided by weeds in annual cropping systems using a systematic map approach[END_REF]. Weeds are an important source of floral and seed resources for various insects, birds and mammals [START_REF] Wilson | A review of the abundance and diversity of invertebrate and plant foods of granivorous birds in northern Europe in relation to agricultural change[END_REF][START_REF] Petit | Weeds in agricultural landscapes : a review[END_REF]. Their role as providers of a continuous supply of pollen and nectar is of key importance for the maintenance of pollinators and the provision of the pollination service [START_REF] Requier | Honey bee diet in intensive farmland habitats reveals an unexpectedly high flower richness and a major role of weeds[END_REF][START_REF] Bretagnolle | Weeds for bees? A review[END_REF].

Weeds also supply trophic resources for many natural enemies (parasitoids, predators) and are thus contributing to the provision of pest control services [START_REF] Tylianakis | Improved fitness of aphid parasitoids receiving resource subsidies[END_REF][START_REF] Ditommaso | Integrating insect resistance and floral resource management in weed control decision-making[END_REF]. Some authors suggest that the decline of many insects and farmland birds is associated with changes in farming practices that adversely affect weeds [START_REF] Marshall | The role of weeds in supporting biological diversity within crop fields[END_REF].

Weed richness and abundance in arable farming has indeed drastically declined over the last decades as documented in Europe [START_REF] Andreasen | Decline of the flora in Danish arable fields[END_REF][START_REF] Baessler | Effects of changes in agricultural land-use on landscape structure and arable weed vegetation over the last 50 years[END_REF]. In Northern France, [START_REF] Fried | Arable weed decline in Northern France: Crop edges as refugia for weed conservation?[END_REF] estimated that weed richness and abundance within arable fields decreased respectively by 44 and 66% over the last 30 years. These authors also showed that this decline was dependent on the within-field location of weeds, with a much less pronounced decline in crop edges, i.e. the area between the field margin and first row of crop, because this habitat can act as refugia for many weed species [START_REF] Solé-Senan | Plant diversity in Mediterranean cereal fields: Unraveling the effect of landscape complexity on rare arable plants[END_REF].

Evaluating the capacity of agroecosystems to provide key resources and how this capacity is affected by farming management is of prime importance to enhance the ecological functioning of agricultural systems. Yet, there are few examples of such assessment at large spatial scales. [START_REF] Evans | Seeds in farmland food-webs: Resource importance, distribution and the impacts of farm management[END_REF] evaluated the biomass and energy provided by berries and seeds at a farm scale in relation to the trophic value of such resources for farmland birds. Similarly, [START_REF] Vialatte | Landscape potential for pollen provisioning for beneficial insects favours biological control in crop fields[END_REF] estimated the pollen resource provision within an agricultural landscape for hoverflies through the aggregation of mean provision values estimated by plant surveys in different types of semi-natural and cultivated habitats. Many studies have documented weed communities in different agricultural or landscape settings, yet, to our knowledge, no assessment of weed floral and seed resources within an agricultural landscape is yet available.

One reason is that most arable weed surveys conducted at large scale are designed to assess the effect farming management or environmental conditions on weed communities (for a review, see Hanzlik and Gerowitt, 2016). The timing of the weed sampling is therefore often driven by agronomic considerations such as the completion of weed management measures (e.g. Hawes et al., 2010) or crop phenology (e.g. [START_REF] Andreasen | Increasing weed flora in Danish arable fields and its importance for biodiversity[END_REF]. Weeds are often described once in the season, at an earlier or unspecified phenological stage (Hanzlik and Gerowitt, 2016). Such methodology is thus not tailored to assess the production of weed resources within an agricultural landscape. Between earlier phenological stages and the flowering and fruiting stages that are key in the provision of resources to other taxa, weed plant survival and development is likely to be impacted by the environment where it grows. The competition for resources (nutrients, water, light) exerted by the crop on weeds can significantly affect weed survival and growth [START_REF] Kaur | Understanding crop-weed-fertilizer-water interactions and their implications for weed management in agricultural systems[END_REF], with an effect often considered as weaker in field edges than in field cores [START_REF] Cordeau | The impact of sown grass strips on the spatial distribution of weed species in adjacent boundaries and arable fields[END_REF][START_REF] Perronne | The interspecific and intraspecific variation of functional traits in weeds: diversified ecological strategies within arable fields[END_REF] and variable according to the type of crop grown. In addition, even after the completion of weed management operations, farming practices such as nitrogen fertilization can affect weed development [START_REF] Bàrberi | Weed communities of winter wheat as influenced by input level and rotation[END_REF][START_REF] Kleijn | Conservation headlands for rare arable weeds: the effects of fertilizer application and light penetration on plant growth[END_REF]. The timing, frequency and intensity of these farming practices vary across farming systems and crop types and their adverse effect on weed development likely to be less intense in the edges of the field [START_REF] Marshall | Field margins in northern Europe: their functions and interactions with agriculture[END_REF].

One can thus expect that the chance for a weed plant to reach the next phenological stages will vary much within the same agricultural landscape, depending on the local plant growing conditions. Assessing this intraspecific variability in weed phenology thus appears a necessary step for assessing the production of weed resources within an agricultural landscape.

In this paper, we assessed the intraspecific phenological variability of 30 weeds species commonly found in arable farming in response to their location in the field (hereafter 'withinfield location', i.e. field core vs. field edge) and to the crop grown. We monitored the phenology of 685 weed seedling patches across 64 commercial fields and 6 crop types over 6 months. We developed survival curves and estimated indicators of floral resources production (flowering success, starting date and duration of flowering and dry biomass at flowering as a proxy for the amount of flowers) and seed resource production (fruiting success, starting date of fruiting).

We tested for the effect of within-field location, crop type and their interaction on the phenological indicators. We expected higher success and higher resource production in the field edge as this within-field location is less affected by farming practices and by crop competition.

We also expected weed phenology to respond to the crop grown as the crop tested differed in terms of competitive ability, morphological traits and response to farming management.

Materials and methods

Study area

The study was conducted in the monitoring study area of Fénay, a 1000 ha arable farming area located in a plain 10km south of Dijon in eastern France (47°13'N, 5°03'E). Climatic conditions are continental (mean annual temperature 10.7°C and precipitation 744 mm) and land use is dominated by arable cropping, i.e. mostly rapeseed/cereals-based rotations. Climatic and soil conditions are quite homogeneous across the area, and such a low variability in pedoclimatic conditions across sampled fields was deemed advantageous to conduct intraspecific comparisons in weed phenology. Weed communities and farming practices are monitored in the study area since 2008, in between 70 and 140 fields, depending on the year. Field size average 9.8 ha and range from 0.5ha to 43ha. Field management in the area is conventional although the farmers differ in their farming strategies, and notably in terms of the diversity of crop rotations and their reliance on tillage and herbicides (for a full description of farming strategies in the area, see [START_REF] Yvoz | A framework to type farming strategies within a production situation to improve the comprehension of weed communities[END_REF]. The standard annual weed monitoring includes weed recording at seedling stage in the field core within a 2000 m² zone (50 m x 40 m) located 20 m away from the field margin and in the field edge (i.e. the area between the field margin and the first row of crop) facing the field core zone along a 50 m long line. The annual survey spans from March (winter crops) to June (summer crops). The management by farmers ensure that the weed flora is kept under control in the area [START_REF] Quinio | Separating the confounding effects of farming practices on weeds and winter wheat production using path modelling[END_REF] and over the years, 147 weed species have been recorded, among which 46 were solely observed in the field edge.

From the existing weed records, we identified the top 30 weed species (in terms of occurrence and abundance over the period 2008-2018) that occurred both in the core of fields and in field edges (Supp. Mat. Table S1). This list included 2 monocotyledon (Alopecurus myosuroides and Bromus sterilis) and 28 dicotyledon species. The flowers of some species are known to be of particularly high value for pollinators such as bees, bumblebees and hoverflies, e.g. the poppy Papaver rhoeas, the cornflower Cyanus segetum, the field bindweed Convolvus arvensis or the common knotgrass Polygonum aviculare ), whereas other species produce floral resources of limited use (e.g. for pollinators, see [START_REF] Marshall | The role of weeds in supporting biological diversity within crop fields[END_REF][START_REF] Ricou | A vegetation-based indicator to assess the pollination value of field margin flora[END_REF]. Seeds produced by the 30 species can be used by invertebrate and vertebrate seed-eaters, and some species are known to be much consumed by generalist invertebrate predators such as carabid beetles e.g. the field pansy Viola sp, the dandelion Taraxacum officinale or the creeping thistle Cirsium arvense [START_REF] Petit | Weed seed choice by carabid beetles (Coleoptera: Carabidae): Linking field measurements with laboratory diet assessments[END_REF].

Weed phenological survey

In spring 2019, we surveyed the distribution of the 30 targeted weed species, first at seedling stage, across the Fénay area during the standard annual weed monitoring of 76 fields (called early weed survey, Figure 1). This allowed selecting a subset of 64 fields that were grown with 6 different crop types, i.e. two winter cereals (wheat, barley), two winter Brassicacae (oilseed rape, mustard), one spring crop (spring barley) and one summer crop (soya bean). The number of field sampled per crop type is provided in Supp. Mat. Table S2. The light condition prevailing in the field core and in the field edge of each of the 64 fields was quantified by conducting five measures of the photosynthetically active radiation (PAR) on top of the canopy and on the ground using a Sunscan PAR sensor (AT Delta-T Devices Cambridge England). PAR was measured once, at the flowering of the crop, as the rationale was to gather comparative information on light conditions in different within-field locations and crop types.

Within the 64 fields, we georeferenced a total of 685 weed patches (Figure 1) distributed per within-field location and crop type as described in Supp. Mat. Table S2. In the weed patch selection process, we maximised the co-occurrence of a targeted weed species in field core patches and field edge patches of the same field. The phenological survey was based on a simplified BBCH scale [START_REF] Hess | Use of the extended BBCH scale -general for the descriptions of the growth stages of mono-and dicotyledonous weed species[END_REF] with 10 stages from the cotyledon stage until the senescence (Supp. Mat. Table S3). We added a stage "DEATH" to account for record units dying before reaching the flowering stage. Within a weed patch, we recorded individually the phenological stage of the targeted weed species present. Obviously, not all the 30 species were present in all patches. When plants germinated after the early weed survey, we included them in the following surveys. When very different phenological stages (different by more than 2 stages on the scale) of the same weed species co-occurred in the same patch, they were considered as different record units. As a consequence, we monitored a total of 3770 records (called record units hereafter) distributed across within-field locations and crop types as described in Supp. Mat. Table S2.

The record units were monitored during six or seven (for winter wheat) successive surveys, spanning from 5 th April till 21 th September 2019 (Supp. Mat. Table S4). The first survey S1 was the early weed survey described above, implemented after all weeding operations. Field cores of oilseed rape and mustards could not be surveyed at S5 (end of the crop flowering) because it was too difficult to enter in the field. The last survey S6 (or S7 for winter wheat) occurred just after crop harvest and before any tillage (Figure 2). When a record unit reached stage D2 or more (flowering), we sampled between one and three individual plants to quantify their dry biomass. To avoid any impact of plant removal on the following surveys, we collected plants in the surrounding, within a radius of 10 meters centred on the patch, when less than three individuals were present in the patch. Individual plants were dried (48 hours at 80°C) and weighted. For a subset of collected plants, we counted the number of flowers produced. The linear relationship between dry biomass at flowering and the number of flowers produced and the adjusted R-square of linear models for the 30 weed species is presented in Supp. Mat. Figure S1.

Estimation of resource production

The production of floral and fruit resources was estimated for each record unit by using a set of six indicators. The six indicators were applied to the 30 weed species surveyed.

The flowering success (FLS) was calculated as the proportion of patches within which the record unit reached any of the flowering stages D1 to E2. The starting date of flowering or flowering onset (FLOn) was estimated per record unit as the date where stage D1 was reached and was expressed in growing degree days since January 1 st (base temperature = 0°C). The duration of the flowering period (FLD) was calculated per record unit as the difference between the end of the flowering (stage E1 reached) and FLOn and was also expressed in growing degree days. Similarly, the production of seed resources was estimated by the fruiting success (FRS) calculated as the proportion of patches within which the record unit reached stage D3 or later stages and the fruiting onset (FROn) estimated per record unit as the date where stage D3 was reached and was also expressed in growing degree days. We did not consider a fruiting duration in this study as we considered that after seed shed, seeds on the soil surface were available to seed consumers for duration that could be highly variable, depending on seed characteristics and notably seed size [START_REF] Westerman | Burial rates of surrogate seeds in arable fields[END_REF]. The sixth indicator was the dry biomass of record units at flowering. Dry biomass at flowering is a measure indicative of the number of flowers produced in the 30 species (see Supp. Mat. Figure S1). It is also strongly related to the amount of seed produced, as documented for many weed species [START_REF] Senseman | Flowering patterns, seed production and somatic polymorphism of three weed species[END_REF][START_REF] Wilson | Predicting the competitive effects of weed and crop density on weed biomass, weed seed production and crop yield in wheat[END_REF][START_REF] Lutman | Estimation of seed production by Stellaria media, Sinapis arvensis and Tripleurospermum inodorum in arable crops[END_REF][START_REF] Grundy | Seed production of Chenopodium album in competition with field vegetables[END_REF][START_REF] Lutman | Seed production and subsequent seed germination of Senecio vulgaris (groundsel) grown alone or in autumn-sown crops[END_REF][START_REF] Lutman | Estimation of seed production by Myosotis arvensis, Veronica hederifolia, Veronica persica and Viola arvensis under different competitive conditions[END_REF].

Data analysis

Data analysis were done with the R software (R Core Team, 2019). Differences in light reaching the soil between field edges and field cores and between crop types were tested with a mixed linear model (package lme4) including Field as a random factor to account for differences in soil properties and farming management between fields. Significance was tested using the package [car] and pair-wise comparisons were conducted with the packages [emmeans] and

[multcomp].
Models were fit for each species and phenological stages to test for the effect of Within-field location and Crop type on weed phenological development. We hypothesised that some species will respond to interactive effects, i.e. that the response to Within-field location will depend on Crop type. This assumption is built on the fact that the ecological properties of a field edge (width, light availability, etc.) can depend on the identity of the adjacent crop and associated farming practices (de Snoo, 1997). Interaction could not be tested for success indicators (FLS and FRS) as models failed to converge. In all models, Field was included as a random factor.

We first conducted a time-to-event analysis using survival curves comparison. For each species, the survival curve represents the proportion of individuals having already reached a particular stage over time [START_REF] Mcnair | How to analyse seed germination data using statistical time-to-event analysis: non-parametric and semi-parametric methods[END_REF]. Cox proportional hazards models linking the characteristics of the species survival curve to Within-field location and Crop type were then developed with the coxme function from the [coxme] package. The effects of Within-field location, Crop type and their interaction were tested by a type II ANOVA using the function Anova from the [car] package.

The effect of Within-field location and Crop type (and when possible their interaction) was then assessed for the six phenological indicators for each species with logistic (FLS, FRS) or linear regression models (glmer and lmer functions of the [lme4] package). The effects were tested by a type II ANOVA using the function Anova from the [car] package. Comparisons between Within-field location (two-level factor) and between crop types were tested using the function emmeans from the [emmeans] package (computes the estimates) and the function cld from the [multcomp] package (implements the multiple comparison needed for the effect of crop type (multiple levels).Because of variations in the occurrence of weed species across within-field locations and among crop types, data were lacking for some situations and not all full models could be run for the 30 weed species.

Results

The proportion of light reaching the soil surface was significantly higher in field edges than in field cores for all crop types but mustard and oilseed rape. It did not differ between crop types, whether in crop edges or in field cores (Supp. Mat. Figure S2).

Overall differences in weed species phenology

The time to event analysis revealed that overall, the phenological development of all targeted weed species except AMASS was affected either by Within-field location, Crop type or both (see survival curves of the 30 species per within-field location and crop type and tests associated Cox proportional hazards models in Supp. Mat. Appendix 1). Across species, the proportion of plants that died before reaching the flowering stage (stage DEATH) was lower in field edges (mean±s.d., 0.21±0.19) than in field cores (0.39±0.23). The probability of new emergence (stage A) after the first survey (S1) was similar in field edges (0.17±0.22) and in field cores (0.15±0.14). For most species, earlier phenological stages (from A to C1) were affected by Crop type, according to the timing of crop sowing (i.e. stages were reached earlier in early sown crops, see Supp. Mat. Table S2) whereas latter stages (from E1 to E2) were mostly impacted by Within-field location, species shedding seeds (stages E2) earlier in field edges compared to field cores.

Production of resources by weeds

Flowering success, date and duration

The flowering success (FLS) across species was on average 0.70±0.22 in the field edge and 0.51±0.25 in the field core and was highly variable among species (Table 1). For one species (AMASS) we could only test the effect of Within-field location. FLS of 16 species appeared unaffected by Within-field location and Crop type (p-values in Table 2). Six species responded solely to Within-field location (Table 2), with higher FLS in field edges (Table 1). Three species responded solely to Crop type, with lower FLS in cereal crops than in other crop types (Table 2, Supp. Mat. Table S5). Five species responded both to Within-field location and Crop type, with lower FLS in field cores than field edges and in cereal crops than in other crop types (Figure 3).

The flowering onset (FLOn) across species occurred on average 113 degree days earlier in the field edge (1547±663) than in the field core (1660±682). Full models (i.e. Within-field location, Crop type and their interaction) were run for 22 species and partial models for seven species.

Ten species appeared unaffected by Within-field location and Crop type (Table 2). FLOn of eight species differed solely by Crop type following the gradient of crop sowing date, as previously described (Table 2, Supp. Mat. Table S5). We detected a sole effect of Within-field location for one species (BROST) and additive (4 species) or interactive (6 species) effects of Within-field location and Crop type. When interactive effects were detected, they indicated earlier flowering only in the field edges of some of the crops (Table 1; Supp. Mat. Figure S3).

The flowering duration (FLD) across species was on average 63 degree days shorter in the field edge (807±244) than in the field core (870±320). Full models were run for 17 species and partial models for 11 species. Eleven species did not respond to Within-field location or Crop type.

Within-field location (3 species) or its interaction with Crop type (5 species) affected FLD. For these species, except for EPHHE, FLD was longer in field edge than in field core (+60 degree days in average). Crop type affected FLD for 10 species (Table 2). Record units in cereal crops had a shorter FLD than those located in other crop types (341 degree days less on average, Supp. Mat. Table S5). Interactive effects indicated longer FLD in the field edges of cereal crops but shorter FLD in the field edges of winter mustard and oilseed rape compared to field cores (Supp. Mat. Figure S4).

Fruiting success and date

The fruiting success (FRS) across species was higher in the field edge (0.59±0.30) than in the field core (0.43±0.25) and was below 0.36 in cereal crops against above 0.74 in the other crop types (Supp. Mat. Table S5). Additive models were applied for 27 species and only the Withinfield location was tested for the 3 others. Crop type and Within-field location did not appear to affect FRS of 17 species. For the other species, Within-field location (eleven species) and Crop type (six species) affected FRS (Table 2). Except for SONAS, FRS was always higher (+29 %) in the field edge than in the field core (Table 1). Crop type effects opposed cereal crops (low FRS) to the other crop types (Supp. Mat. Figure S5).

The Fruiting onset (FROn) across species occurred on average 166 degree days earlier in the field edge (2125±778) than in the field core (2291±741). Full models could be run for 18 species and partial models for nine other species. Ten of them responded neither to Within-field location nor to Crop type (Table 2). Within-field location had a significant impact on FROn, as the sole impacting factor for two species, in addition to Crop type for two species and in interaction with Crop type for six species (Table 2). With the exception of ANGAR, FROn occurred later (337 degree days) in field cores than in field edges although this trend could be restricted to some specific crop types (Table 1). In addition to the interactive effect, Crop type impacted 9 species with later FROn in mustard, oilseed rape or in soya compared to other crop types (Supp. Mat. Figure S6).

Dry biomass

Dry biomass at flowering did not differ strongly between field cores and field edges but tended to be lower in cereal crops than in the other crop types (Supp. Mat. Table S5). Full models could be run for 21 weed species and partial models for 8 species. Among them, the dry biomass of 13 species were affected nor by Within-field location neither by Crop type. Within-field location effects and interactive effects with Crop type were detected for respectively four and six weed species, with higher biomasses in field edge or in field core, depending on the species and the crop type (Table 1; Table 2). The biomass of six species was solely affected by Crop type, with higher biomass in mustard and oilseed rape compared to other crop types (Supp. Mat. Figure S7).

Discussion

A first rationale for this phenological survey was to assess the proportion of plants recorded at seedling stage, and after the completion of weed management operations, that would reach a stage where they provide floral and seed resources. Our results indicate that on average, only 60% of plants flowered and 50% fruited; this was mostly due to weed mortality which highly varied among the 30 species. We also expected resource production of individual weed species to be modulated by their location in the field and by the crop type where they stand. Our results support this hypothesis. Although weed responses were quite specific, we show that for a given weed species, the probability of reaching flowering and fruiting stages, as well as the timing, duration and amount of resources produced, estimated here by the dry biomass at flowering, vary according to their location in the field and to the crop type.

Intraspecific weed responses to field location and crop type

Our results demonstrate that in field cores, mortality before reaching the flowering stage was higher than in field edges. In addition, most weed species flowered and fruited more and earlier in field edges than in field cores. This observed higher mortality and delays in phenological development could be related to differences in the intensity of competition for resources. In field cores, competition for light is higher than in the field edge and decreases in light quality and quantity can delay weed flowering and seed production onsets [START_REF] Mclachlan | Light limitation of reproduction and variation in the allometric relationship between reproductive and vegetative biomass in Amaranthus retroflexus (redroot pigweed)[END_REF][START_REF] Yasin | The importance of reduced light intensity on the growth and development of six weed species[END_REF]. It is also possible that in some fields, herbicides that were applied prior to our first survey were still acting, causing mortality or slowing the development of weeds, with possibly a more marked effect in field cores than in field edges, although this could highly depend on the way the farmer conducted the spraying. We also often observed a longer flowering period in the field edge than in field core which could also be explained by higher amount of light [START_REF] Benvenuti | Effects of shade on reproduction and some morphological characteristics on Abutilon theophrasti Medicos, Datura stramonium L. and Sorghum halepense L[END_REF]. Some studies have established that weed dry biomass can also decrease as competition for light increases [START_REF] Mclachlan | Effect of corn-induced shading and temperature on rate of leaf appearance in redroot pigweed (Amaranthus retroflexus L.)[END_REF]. We detected no such effect here, i.e. our estimates of dry biomass at flowering for a given weed species were comparable in the two within-field locations. This result could be related to (i) a possibly higher plant density in field edges which restrained each individual to a limited biomass [START_REF] Wilson | Predicting the competitive effects of weed and crop density on weed biomass, weed seed production and crop yield in wheat[END_REF], (ii) competition for soil resources with the plants growing in the adjacent grass boundaries [START_REF] De Cauwer | Effect of margin strips on soil mineral nitrogen and plant biodiversity[END_REF][START_REF] Cordeau | Relative importance of farming practices and landscape context on the weed flora of sown grass strips[END_REF], and/or (iii) a lower amount of nitrogen sprayed by famers in field edges than in field cores. Competition for soil resources could also explain some of the observed differences in weed mortality and phenology detected here. In field cores, N supply is higher than in field edges so that crops produce high aboveground biomass and thus outcompete weeds for water and nutrients [START_REF] Moreau | The ecophysiological determinants of nitrophily in annual weed species[END_REF]. This could explain the higher weed mortality observed in field cores, but also the fact that surviving weeds may have had access to important resources [START_REF] Bischoff | The effects of nitrogen and diaspore availability on the regeneration of weed communities following extensification[END_REF], so that their biomass was not inferior to that of plants growing in field edges.

We also detected that crop type modulated weed development, especially at earlier phenological stages. This is congruent with results indicating that the period of tillage and crop sowing affects the timing of weed germination but also the post-germination life history characters of weeds [START_REF] Zhou | Phenotypic plasticity of life-history characters in response to different germination timing in two annual weeds[END_REF], and particularly their flowering date [START_REF] Gunton | Functional traits relating arable weed communities to crop characteristics[END_REF]. Weed phenological responses to crop type may also be partly explained by differences in light interception. Crop types exert different levels of light competition on weeds, in relation to their sowing density, row spacing and morphological characteristics [START_REF] Swanton | Experimental Methods for Crop-Weed Competition Studies[END_REF]. Cereals crops are generally highly competitive because of small row spacing and of their tillering ability, a key characteristic to outcompete weeds [START_REF] Jha | Weed management using crop competition in the United States: A review[END_REF]. Our findings indeed suggest that weed plants in the field core of cereal crops suffered high mortality before reaching the flowering stage and, if they survived, exhibited an earlier and shorter flowering and fruiting period and a lower dry biomass. The earlier and shorter weed flowering period observed in cereal crops could also be a direct consequence of the low Red:Far Red ratio of light typically found in cereals [START_REF] Franklin | Phytochromes and Shade-avoidance Responses in Plants[END_REF]. The effect of Brassicaceae crops on weed phenology was quite different from that of cereals crops in our study. A major characteristic of oilseed rape and mustard crops is their high nitrogen demand and their subsequent high aboveground biomass [START_REF] Blackshaw | Differential response of weed species to added nitrogen[END_REF]. Weed mortality in Brassicaceae crops could thus be explained by a combination of competition for soil resources and light. The later flowering onset detected in some species could reflect that in conditions of limited light and high nitrogen availability, some nitrophilous weed species, such as Chenopodium album, increase allocation of resources to leaves rather than investing in flowering [START_REF] Moreau | The ecophysiological determinants of nitrophily in annual weed species[END_REF]. Besides, an opening of the canopy during oilseed rape and mustard senescence leads to a reduction of competition for light. Thus, weed plants with delayed flowering have higher flowering and fruiting success.

Implications for resource provision by weeds within a landscape

It is well established that the composition of weed communities results from the combination of environmental, farming management and landscape factors [START_REF] Fried | Environmental and management factors determining weed species composition and diversity in France[END_REF][START_REF] Petit | Landscape scale management affects weed richness but not weed abundance in winter wheat fields[END_REF]. These factors thus drive the probability of occurrence and the spatial distribution of a particular weed species within a landscape [START_REF] Alignier | Identifying the relevant spatial and temporal scales in plant species occurrence models: The case of arable weeds in landscape mosaic of crops[END_REF], with important consequences on the provision of weed resources at that level. Our findings highlight an additional factor affecting the production of weed resources. We provide evidence that a weed plant will deliver different amounts of floral and fruit resources, and at different times, depending on the habitat (within-field location and crop type) it occupies within the agricultural landscape. Our quantification of this phenological variability gives some insights into the relative contribution of the field cores and field edges of different crops to the provision of flowers and seeds. It also enables to explore to what extent the complementarity between these habitats could be used to enhance the provision of weed resources over time in a given landscape.

For 28 out of the 30 weed species, the overall duration of flower production by a given weed species at a field scale (core + edge of the field) is longer than the duration that results from the contribution of only one of the field locations. In half of these cases, the production of flowers in field edges started earlier and ended later than in the core of the fields, and hence the presence of individuals in field edges significantly increased the duration of the provision of flower resources at the field scale. For six weed species, the core field supplied flower resources for a longer period, with individuals starting earlier and ending flowering later than in the edge. For five species, field edges and cores were truly complementary, with flowering first occurring in the edge and ending in the core, with an intermediate period during which both field locations provided floral resources. Similarly, the co-occurrence of different crop types in the landscape could buffer variations in the amount and the temporal provision of weed resources. For example, our findings show a relatively low production of resources by weed plants located in cereal crops, compared to other crop types. This result suggests that it is of particular importance to maintain the extent of field edges in cereal crops but also that the presence of other crop types in the vicinity could also be used to counteract the low amount of weed resources provided by cereal core fields, with potentially positive effects on the biodiversity of many taxa [START_REF] Sirami | Increasing crop heterogeneity enhances multitrophic diversity across agricultural regions[END_REF]. The impact of changes in the composition and configuration of agricultural landscapes on weed services could be further investigated through landscape scale modelling predicting the impact of landscape change scenario on weed distribution [START_REF] Ricci | How much can a large landscape-scale planning reduce local weed infestations? A landscape-scale modelling approach[END_REF].

Conclusion

This study provides field-based evidence that the production of trophic resources by 30 individual weed species that are commonly found in arable farming is not a constant. Rather, we evidenced important intraspecific variability in the success of reaching phenological stages that are key to resource provision as well as in the timing of the production of resources in response to within-field location and crop type. It is important to account for this intraspecific variability when evaluating the contribution of weed communities to ecosystem services. It also suggests that at a landscape scale, the amount, timing and duration of provision of services by weeds can be enhanced by maintaining sufficient lengths of crop edges and by growing a diversity of crop types.

Table 1: Indicators of resource provision (mean, [min-max] and (number of observed record units) of the 30 weed species named according to their EPPO codes 5 (see Supp. Mat. Table S1, https://gd.eppo.int/) and per Within-field location (FE: Field edge; FC: Field core). FLS: flowering success (rate); FLOn: flowering 6 onset (growing degree day (GDD) since Jan 1 st , base temperature = 0°C); FLD: duration of the flowering period (GDD); FRS: fruiting success (rate); FROn:

Table 2: Effects of Crop type, Within-field location and their interaction on the six indicators of resource provision of the 30 weed species named according to their EPPO codes (see Supp. Mat.Table S1, https://gd.eppo.int/). FLS: flowering success (rate); FLOn: flowering onset (growing degree day (GDD) since Jan 1st, base temperature = 0°C); FLD: duration of the flowering period (GDD); FRS: fruiting success (rate); FROn: fruiting onset (GDD); Dry biomass at flowering (g of dry matter). Results are presented as the p-value of the regression model (ns = p > 0.1; -means the effect cannot be tested due to insufficient data).

Species

Acknowledgements

We want to thank the two reviewers who provided many constructive comments on a previous version the manuscript. We thank the staff of UMR Agroécologie who have contributed to the long-term weed monitoring in the Fenay study area (Emilie Cadet, Bruno Chauvel, Emeline Felten, Eric Vieren). We are also grateful to the farmers for granting us access to their fields. This work was funded by the European Union's Horizon 2020 research and innovation program under grant agreement No 727321 (IWM PRAISE) and by the INRAE metaprogram Ecoserv on "ecosystem services".

Declaration of interest

None fruiting onset (GDD); Dry biomass at flowering (g of dry matter). FE/FC represents the difference in the mean value of the indicator between the field edge and the 8 field core, estimated as (mean FEmean FC) for FLS and FRS and as (100 (mean FEmean FC / mean FC)) for the other four indicators, in bold when FE/FC > 9 0 (value of indicator is higher in the field edge). n/a indicates that no data could be collected to estimate the indicator.