Pairwise Logical Selection of Enthymeme Completions under Semantic-Link Uncertainty

# Pairwise Logical Selection of Enthymeme Completions under Semantic-Link Uncertainty
Source: [https://arxiv.org/html/2608.18820](https://arxiv.org/html/2608.18820)
###### Abstract

Arguments often omit premises or claims, forming enthymemes\. We study pairwise logical selection between two candidates for the omitted component\. Natural language processing methods can identify or generate candidates but often do not expose how the selected candidate completes the inference\. Logic\-based approaches make this inference explicit but usually assume that the required formulae and background knowledge are available\. A prior neuro\-symbolic pipeline translated the stated text and two generated missing\-premise candidates into propositional formulae and tested each candidate independently with a SAT solver; candidates with the same entailment status remained tied even when the task required a single selection\. We extend the pipeline to missing\-claim selection and replace binary entailment outcomes with logical\-resistance scores for pairwise comparison\. We defineTop\-Link, which uses weighted Partial MaxSAT to compute logical resistance under a single configuration of highest\-confidence semantic links\. We then introduce*Possible\-World Atom\-Link Formalization*\(PWAL\), which keeps translated formulae fixed and marginalizes logical resistance over alternative cross\-formula semantic\-link configurations\. We evaluate five tasks: ARCT and a CDED\-derived task for missing\-premise selection; iDebate\- and AAE2\-derived tasks for missing\-claim selection; andα\\alphaNLI for abductive hypothesis selection\. Relative toTop\-Link, PWAL raises strict accuracy by2\.952\.95–30\.8630\.86percentage points and reduces tie rates by4\.574\.57–58\.0058\.00percentage points on all five tasks\. When ties receive half credit, accuracy still increases by0\.450\.45–6\.046\.04percentage points\. For each comparison, PWAL records the translated formulae, sampled link configurations, and resistance components, providing a transparent trace of how the scores are computed\.

## Introduction

An enthymeme leaves a premise or claim unstated\. For example, the premise*the weather report predicts rain*does not entail the claim*you should take an umbrella*without an implicit premise connecting rain to the need for an umbrella\. Recovering the omitted component makes the inference explicit and permits logical evaluation\. We study pairwise logical selection between two supplied candidate completions, where the omitted component is either a premise or a claim\.

Natural language processing methods identify, retrieve, generate, or select omitted argument components, especially premises\([Habernal et al\. 2018](https://arxiv.org/html/2608.18820#bib.bib11);[Singh et al\. 2022](https://arxiv.org/html/2608.18820#bib.bib32);[Sviridova, Cabrio, and Villata 2026](https://arxiv.org/html/2608.18820#bib.bib34)\), but generally do not expose the logical inference completed by a selected or generated component\. Symbolic approaches make this inference explicit through abduction and other formal reasoning methods\([Hunter 2007](https://arxiv.org/html/2608.18820#bib.bib14);[de Saint\-Cyr 2011](https://arxiv.org/html/2608.18820#bib.bib8);[Black and Hunter 2012](https://arxiv.org/html/2608.18820#bib.bib5);[Hosseini, Modgil, and Rodrigues 2014](https://arxiv.org/html/2608.18820#bib.bib13);[Xydis et al\. 2020](https://arxiv.org/html/2608.18820#bib.bib37);[Panisson, McBurney, and Bordini 2022](https://arxiv.org/html/2608.18820#bib.bib28);[Hunter 2022](https://arxiv.org/html/2608.18820#bib.bib15);[Leiva, Gottifredi, and García 2023](https://arxiv.org/html/2608.18820#bib.bib23);[Leiva, García, and Gottifredi 2025](https://arxiv.org/html/2608.18820#bib.bib22);[Ben\-Naim, David, and Hunter 2025](https://arxiv.org/html/2608.18820#bib.bib3);[David and Hunter 2025](https://arxiv.org/html/2608.18820#bib.bib7)\), but generally assume that the formulae, candidate completions, or background knowledge are available\.

A prior neuro\-symbolic pipeline combined candidate generation with logical verification\([Feng and Hunter 2026](https://arxiv.org/html/2608.18820#bib.bib9)\)\. It generated two missing\-premise candidates, translated the stated and generated text into propositional formulae, and tested each candidate independently with a SAT solver\. Because each candidate received only an entailment or non\-entailment result, equal outcomes left the pair unresolved\.

We instead assign each candidate a logical\-resistance score and compare the two scores\. Each candidateccdefines a source statement collectionScS\_\{c\}evaluated against a target statement collectionTcT\_\{c\}\. Missing\-premise tasks varyScS\_\{c\}while holdingTcT\_\{c\}fixed; missing\-claim tasks holdScS\_\{c\}fixed while varyingTcT\_\{c\}\. Because the source and target are translated separately, semantically corresponding or conflicting propositions remain distinct Boolean atoms\. We represent these cross\-formula semantic relations as*atom links*encoding exact correspondence, entailment, or contradiction\. This creates*semantic\-link uncertainty*: a target atom without an exact correspondence may have several possible entailment or contradiction links, as well as the option of remaining unlinked, and committing to one configuration can change the candidate score\.

We instantiate the pairwise logical\-resistance score in two ways\.Top\-Linkserves as a single\-configuration reference: for each such target atom, it selects the highest\-confidence entailment or contradiction link when one is available and evaluates the resulting configuration with weighted Partial MaxSAT\.*Possible\-World Atom\-Link Formalization*\(PWAL\) instead keeps the translated statement formulae and exact atom correspondences fixed, assigns a uniform distribution over each target atom’s available entailment or contradiction links and the option of leaving it unlinked, and treats these local choices as independent\. PWAL selects the candidate with lower expected logical resistance\. A candidate’s logical\-resistance score is lower when requiring the target to hold creates less conflict and when more target content is already supported without that requirement\. The resulting trace records the translated formulae, evaluated link configurations, and resistance components used in each comparison\.

We evaluateTop\-Linkand PWAL on five pairwise tasks\. The Argument Reasoning Comprehension Task \(ARCT\)\([Habernal et al\. 2018](https://arxiv.org/html/2608.18820#bib.bib11)\)and a task derived from Context\-Dependent Evidence Detection \(CDED\)\([Rinott et al\. 2015](https://arxiv.org/html/2608.18820#bib.bib31)\)evaluate missing\-premise selection\. Tasks derived from iDebate\([Wang and Ling 2016](https://arxiv.org/html/2608.18820#bib.bib35)\)and Argument Annotated Essays v2 \(AAE2\)\([Stab and Gurevych 2017](https://arxiv.org/html/2608.18820#bib.bib33)\)evaluate missing\-claim selection\. We also evaluate Abductive Natural Language Inference \(α\\alphaNLI\)\([Bhagavatula et al\. 2020](https://arxiv.org/html/2608.18820#bib.bib4)\)as a pairwise task for abductive hypothesis selection\. The four argumentation tasks cover both premise\- and claim\-side completion, whileα\\alphaNLI evaluates the same pairwise selection framework in an abductive setting\.

## Background and Related Work

##### Related Work

Neuro\-symbolic reasoning systems translate natural\-language problems into formal representations and invoke symbolic solvers\([Pan et al\. 2023](https://arxiv.org/html/2608.18820#bib.bib27);[Olausson et al\. 2023](https://arxiv.org/html/2608.18820#bib.bib25);[Ye et al\. 2023](https://arxiv.org/html/2608.18820#bib.bib38);[Kirtania, Gupta, and Radhakrishna 2024](https://arxiv.org/html/2608.18820#bib.bib18)\)\. Some refine a generated formalization using solver feedback or aggregate predictions across several generated formalizations\([Pan et al\. 2023](https://arxiv.org/html/2608.18820#bib.bib27);[Olausson et al\. 2023](https://arxiv.org/html/2608.18820#bib.bib25)\)\. Recent enthymeme methods compare supplied premise candidates through natural\-language multi\-agent debate\([Ku et al\. 2025](https://arxiv.org/html/2608.18820#bib.bib19)\), optimize logical formalizations over argument maps\([David and Hunter 2025](https://arxiv.org/html/2608.18820#bib.bib7)\), or axiomatize the evaluation of alternative formalizations\([Ben\-Naim, David, and Hunter 2025](https://arxiv.org/html/2608.18820#bib.bib3)\)\. PWAL instead keeps each statement formula fixed and marginalizes over alternative cross\-formula atom\-link configurations during pairwise selection\.

Weighted and probabilistic logic frameworks attach weights to formulae or rules\([Richardson and Domingos 2006](https://arxiv.org/html/2608.18820#bib.bib29);[Bach et al\. 2017](https://arxiv.org/html/2608.18820#bib.bib1);[Riegel et al\. 2020](https://arxiv.org/html/2608.18820#bib.bib30)\)\. PWAL uses soft\-clause weights for within\-world violation costs and world probabilities for uncertainty over which links are active\.

##### Translation of AMR into Logic

Abstract Meaning Representation \(AMR\) represents the semantic structure of a sentence as a rooted, labeled, directed graph\([Banarescu et al\. 2013](https://arxiv.org/html/2608.18820#bib.bib2)\)\. Nodes denote concepts or PropBank frames\. In a frame label such aschase\-01,chaseis the predicate lemma and01is its PropBank sense identifier\. Labeled edges encode PropBank\-derived core roles such as:ARG0and:ARG1\([Kingsbury and Palmer 2002](https://arxiv.org/html/2608.18820#bib.bib17)\), alongside general AMR relations such as:locationand:time\([Banarescu et al\. 2013](https://arxiv.org/html/2608.18820#bib.bib2)\)\. AMR also represents coordination, conditions, polarity, and reentrancy\.

Motivated by compositional AMR semantics\([Bos 2016](https://arxiv.org/html/2608.18820#bib.bib6)\), we use a fixed rule\-based compiler that maps an AMR graph to structured semantic atoms and a propositional formula\. Coordination, conditions, and formula\-level polarity introduce conjunction or disjunction, implication, and negation, respectively, before truth\-preserving Boolean simplification\.

###### Definition 1\(Statement\-Level Propositional Representation\)\.

For a finite semantic\-atom set𝒜\\mathcal\{A\}, letℒ⁡\(𝒜\)\\mathcal\{L\}\(\\mathcal\{A\}\)be the smallest formula language containing everya∈𝒜a\\in\\mathcal\{A\}and closed under¬\\neg,∧\\land,∨\\lor, and→\\to\.

For each successfully translated statementxx, the solver\-facing representation is𝖱𝖾𝗉⁡\(x\)=⟨𝒜x,Φx,𝒱x⟩\\mathsf\{Rep\}\(x\)=\\langle\\mathcal\{A\}\_\{x\},\\Phi\_\{x\},\\mathcal\{V\}\_\{x\}\\rangle, where:

- •𝒜x\\mathcal\{A\}\_\{x\}is the finite, nonempty set of active semantic atoms;
- •Φx∈ℒ⁡\(𝒜x\)\\Phi\_\{x\}\\in\\mathcal\{L\}\(\\mathcal\{A\}\_\{x\}\)is the propositional formula compiled from the AMR structure; and
- •𝒱x\\mathcal\{V\}\_\{x\}maps each atom in𝒜x\\mathcal\{A\}\_\{x\}to a deterministic, nonempty surface verbalization ending in a full stop\. Formula\-level polarity is represented inΦx\\Phi\_\{x\}rather than in𝒱x\\mathcal\{V\}\_\{x\}\.

LetAtoms⁡\(Φx\)\\operatorname\{Atoms\}\(\\Phi\_\{x\}\)denote the atoms occurring inΦx\\Phi\_\{x\}\. The translator satisfiesAtoms⁡\(Φx\)=𝒜x\\operatorname\{Atoms\}\(\\Phi\_\{x\}\)=\\mathcal\{A\}\_\{x\}, so the atom inventory is exactly the set of propositional variables occurring in the formula\.

The main atom forms areUni⁡\(u\)\\operatorname\{Uni\}\(u\),Dyaκ⁡\(u,v\)\\operatorname\{Dya\}\_\{\\kappa\}\(u,v\), andTriκa,κb⁡\(u,e,v\)\\operatorname\{Tri\}\_\{\\kappa\_\{a\},\\kappa\_\{b\}\}\(u,e,v\)\. Hereu,v,eu,v,eare AMR terms, witheedenoting the predicate occurrence shared by the two roles in a triple, andκ,κa,κb\\kappa,\\kappa\_\{a\},\\kappa\_\{b\}denoting AMR roles\. A unary atom retains a concept that would otherwise have no active proposition or serves as a carrier for local negation\. A dyadic atom represents one role\-labeled semantic relation\. A triple combines two roles licensed by the same predicate occurrence\. Additional atom types, scope rules, and fallback cases are specified in the supplementary material\.

###### Example 1\(AMR\-to\-Logic Translation\)\.

Considerx\+x^\{\+\},*A cute dog chases a cat*, and the corresponding negative statementx−x^\{\-\},*No cute dog chases a cat*\. After omitting token alignments and renaming variables, their parsed AMRs differ only in the root polarity attribute:

Positive AMR \(c / chase\-01 :ARG0 \(d / dog :mod \(u / cute\)\) :ARG1 \(a / cat\)\)

Negative AMR \(c / chase\-01 :polarity \- :ARG0 \(d / dog :mod \(u / cute\)\) :ARG1 \(a / cat\)\)

Using the same names for corresponding atoms, the modifier producesa1=Dyamod⁡\(dog,cute\)a\_\{1\}=\\operatorname\{Dya\}\_\{\\mathrm\{mod\}\}\(\\textit\{dog\},\\textit\{cute\}\), while the shared:ARG0and:ARG1roles producea2=TriARG0,ARG1⁡\(dog,chase\-01,cat\)a\_\{2\}=\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG1\}\}\(\\textit\{dog\},\\textit\{chase\-01\},\\textit\{cat\}\)\. Both translations have𝒜x\+=𝒜x−=\{a1,a2\}\\mathcal\{A\}\_\{x^\{\+\}\}=\\mathcal\{A\}\_\{x^\{\-\}\}=\\\{a\_\{1\},a\_\{2\}\\\}and the same surface verbalizations,“cute dog\.”and“dog chase cat\.”The sense identifier remains part of the structured atom identity but is omitted from its surface verbalization\. Polarity changes the propositional formula:Φx\+=a2∧a1\\Phi\_\{x^\{\+\}\}=a\_\{2\}\\land a\_\{1\}, whereasΦx−=¬\(a2∧a1\)\\Phi\_\{x^\{\-\}\}=\\neg\(a\_\{2\}\\land a\_\{1\}\)\.

## Pipeline

A pairwise instance contains two candidate\-specific source–target pairs,\(SA,TA\)\(S\_\{A\},T\_\{A\}\)and\(SB,TB\)\(S\_\{B\},T\_\{B\}\)\. Forc∈\{A,B\}c\\in\\\{A,B\\\}, letSc=\(sc,1,…,sc,nc\)S\_\{c\}=\(s\_\{c,1\},\\ldots,s\_\{c,n\_\{c\}\}\)andTc=\(tc,1,…,tc,mc\)T\_\{c\}=\(t\_\{c,1\},\\ldots,t\_\{c,m\_\{c\}\}\)denote the source and target statement collections for candidatecc\. Statements within each collection are conjoined\. Common\-source tasks satisfySA=SBS\_\{A\}=S\_\{B\}, while common\-target tasks satisfyTA=TBT\_\{A\}=T\_\{B\}\.

The pipeline translates and assembles each candidate\-specific source–target pair, constructs cross\-formula atom links, and computes candidate\-level logical resistance using eitherTop\-Linkor PWAL; it selects the lower\-scoring candidate or returns a tie\.

For each resistance\-based scoring method, letσc\\sigma\_\{c\}denote the score assigned to candidatecc\. Lower logical scores are preferred\. The pipeline returnsTiewhenσA=σB\\sigma\_\{A\}=\\sigma\_\{B\}; otherwise, it selects the candidate with the lower score\. This compares the two candidate\-specific evaluations rather than assigning either candidate an absolute validity label\.

### Candidate Source and Target Assembly

Each statement inScS\_\{c\}andTcT\_\{c\}is translated independently\. Before assembly, statement\-local atoms are renamed so that atom namespaces are disjoint across all statement occurrences inScS\_\{c\}andTcT\_\{c\}\. The same renaming is applied to each statement’s formula and verbalization map\. Below,𝒜xi\\mathcal\{A\}\_\{x\_\{i\}\},Φxi\\Phi\_\{x\_\{i\}\}, and𝒱xi\\mathcal\{V\}\_\{x\_\{i\}\}denote these renamed representations\.

###### Definition 2\(Candidate Source and Target Representation\)\.

For each nonempty collectionX∈\{Sc,Tc\}X\\in\\\{S\_\{c\},T\_\{c\}\\\}, writeX=\(x1,…,x\|X\|\)X=\(x\_\{1\},\\ldots,x\_\{\|X\|\}\), and define𝒜X=⨄i=1\|X\|𝒜xi\\mathcal\{A\}\_\{X\}=\\biguplus\_\{i=1\}^\{\|X\|\}\\mathcal\{A\}\_\{x\_\{i\}\}andΦX=⋀i=1\|X\|Φxi\\Phi\_\{X\}=\\bigwedge\_\{i=1\}^\{\|X\|\}\\Phi\_\{x\_\{i\}\}, where⨄\\biguplusdenotes disjoint union\. For eacha∈𝒜Xa\\in\\mathcal\{A\}\_\{X\}, letxix\_\{i\}be its unique originating statement and set𝒱X​\(a\)=𝒱xi​\(a\)\\mathcal\{V\}\_\{X\}\(a\)=\\mathcal\{V\}\_\{x\_\{i\}\}\(a\)\. The source and target namespaces satisfy𝒜Sc∩𝒜Tc=∅\\mathcal\{A\}\_\{S\_\{c\}\}\\cap\\mathcal\{A\}\_\{T\_\{c\}\}=\\varnothing\.

LetCNF⁡\(Φ\)\\operatorname\{CNF\}\(\\Phi\)denote the clause collection in conjunctive normal form \(CNF\) produced by the fixed SymPy\-based conversion used by the solver\([Meurer et al\. 2017](https://arxiv.org/html/2608.18820#bib.bib24)\)\. ForX∈\{Sc,Tc\}X\\in\\\{S\_\{c\},T\_\{c\}\\\}, defineΓX=⨄i=1\|X\|CNF⁡\(Φxi\)\\Gamma\_\{X\}=\\biguplus\_\{i=1\}^\{\|X\|\}\\operatorname\{CNF\}\(\\Phi\_\{x\_\{i\}\}\)\. For clauses,⨄\\bigupluspreserves statement\-indexed clause occurrences\. A literal is an atom or its negation; a clause is a disjunction of literals, written\[ℓ1∨⋯∨ℓm\]\[\\ell\_\{1\}\\lor\\cdots\\lor\\ell\_\{m\}\]\. ThenΦX≡⋀q∈ΓXq\\Phi\_\{X\}\\equiv\\bigwedge\_\{q\\in\\Gamma\_\{X\}\}q\.

The fixed CNF conversion introduces no auxiliary Boolean atoms\.

###### Example 2\(Source and Target Assembly\)\.

Suppose that, after renaming,Φsc,1=a0\\Phi\_\{s\_\{c,1\}\}=a\_\{0\},Φsc,2=a1\\Phi\_\{s\_\{c,2\}\}=a\_\{1\},Φsc,3=¬\(a2∧a3\)\\Phi\_\{s\_\{c,3\}\}=\\neg\(a\_\{2\}\\land a\_\{3\}\), andΦtc,1=b1→b2\\Phi\_\{t\_\{c,1\}\}=b\_\{1\}\\to b\_\{2\}\. ThenΦSc=a0∧a1∧¬\(a2∧a3\)\\Phi\_\{S\_\{c\}\}=a\_\{0\}\\land a\_\{1\}\\land\\neg\(a\_\{2\}\\land a\_\{3\}\)andΦTc=b1→b2\\Phi\_\{T\_\{c\}\}=b\_\{1\}\\to b\_\{2\}, withΓSc=\{\[a0\],\[a1\],\[¬a2∨¬a3\]\}\\Gamma\_\{S\_\{c\}\}=\\\{\[a\_\{0\}\],\[a\_\{1\}\],\[\\neg a\_\{2\}\\lor\\neg a\_\{3\}\]\\\}andΓTc=\{\[¬b1∨b2\]\}\\Gamma\_\{T\_\{c\}\}=\\\{\[\\neg b\_\{1\}\\lor b\_\{2\}\]\\\}\.

### Candidate Atom Links

Because source and target atoms are distinct Boolean variables, their semantic relations must be represented explicitly\. An*atom link*connects a source atom to a target atom\.

###### Definition 3\(Natural Language Inference\)\.

Let𝒴=\{Ent,Con,Neu\}\\mathcal\{Y\}=\\\{\\texttt\{Ent\},\\texttt\{Con\},\\texttt\{Neu\}\\\}denote the entailment, contradiction, and neutral labels\. For nonempty verbalization stringsuuandvv, let𝖭⁡\(u,v\)=\(y,p\)∈𝒴×\[0,1\]\\mathsf\{N\}\(u,v\)=\(y,p\)\\in\\mathcal\{Y\}\\times\[0,1\], whereuuis the NLI premise,vvis the hypothesis,yyis the predicted label, andppis the confidence assigned toyy, rounded to three decimal places\.

###### Definition 4\(Exact and NLI\-Derived Atom Links\)\.

Letcf⁡\(u\)\\operatorname\{cf\}\(u\)denote the case\-folded form of stringuu\. Define

ℳcex\\displaystyle\\mathcal\{M\}\_\{c\}^\{\\mathrm\{ex\}\}=\{\(a,b\)∈𝒜Sc×𝒜Tc∣cf⁡\(𝒱Sc​\(a\)\)=cf⁡\(𝒱Tc​\(b\)\)\},\\displaystyle=\\\{\(a,b\)\\in\\mathcal\{A\}\_\{S\_\{c\}\}\\times\\mathcal\{A\}\_\{T\_\{c\}\}\\mid\\operatorname\{cf\}\(\\mathcal\{V\}\_\{S\_\{c\}\}\(a\)\)=\\operatorname\{cf\}\(\\mathcal\{V\}\_\{T\_\{c\}\}\(b\)\)\\\},𝒰c\\displaystyle\\mathcal\{U\}\_\{c\}=\{b∈𝒜Tc∣∄a∈𝒜Sc:\(a,b\)∈ℳcex\}\.\\displaystyle=\\\{b\\in\\mathcal\{A\}\_\{T\_\{c\}\}\\mid\\nexists a\\in\\mathcal\{A\}\_\{S\_\{c\}\}:\(a,b\)\\in\\mathcal\{M\}\_\{c\}^\{\\mathrm\{ex\}\}\\\}\.Every matching source–target pair is retained, so a target atom may have several exact links\. If a target atom has an exact link, it is not passed to NLI\.

For eacha∈𝒜Sca\\in\\mathcal\{A\}\_\{S\_\{c\}\}andb∈𝒰cb\\in\\mathcal\{U\}\_\{c\}, let\(ya,b,pa,b\)=𝖭⁡\(𝒱Sc​\(a\),𝒱Tc​\(b\)\)\(y\_\{a,b\},p\_\{a,b\}\)=\\mathsf\{N\}\(\\mathcal\{V\}\_\{S\_\{c\}\}\(a\),\\mathcal\{V\}\_\{T\_\{c\}\}\(b\)\)\. The retained non\-neutral alternatives areℛc\(b\)=\{\(a,b,ya,b,pa,b\)∣a∈𝒜Sc,ya,b∈\{Ent,Con\}\}\\mathcal\{R\}\_\{c\}\(b\)=\\\{\(a,b,y\_\{a,b\},p\_\{a,b\}\)\\mid a\\in\\mathcal\{A\}\_\{S\_\{c\}\},\\ y\_\{a,b\}\\in\\\{\\texttt\{Ent\},\\texttt\{Con\}\\\}\\\}\. Neutral outputs generate no link\.ℛc​\(b\)\\mathcal\{R\}\_\{c\}\(b\)contains the alternative non\-exact links for the unmatched target atombb\.

###### Example 3\(Exact and NLI\-Derived Links\)\.

Suppose𝒱Sc​\(a1\)=𝒱Sc​\(a2\)=𝒱Tc​\(b1\)=“dog bark\.”\\mathcal\{V\}\_\{S\_\{c\}\}\(a\_\{1\}\)=\\mathcal\{V\}\_\{S\_\{c\}\}\(a\_\{2\}\)=\\mathcal\{V\}\_\{T\_\{c\}\}\(b\_\{1\}\)=\\textit\{\`\`dog bark\.''\}, and these are the only exact matches\. Thenℳcex=\{\(a1,b1\),\(a2,b1\)\}\\mathcal\{M\}\_\{c\}^\{\\mathrm\{ex\}\}=\\\{\(a\_\{1\},b\_\{1\}\),\(a\_\{2\},b\_\{1\}\)\\\}\.

Letb2b\_\{2\}have verbalization“animal move\.”and no exact match\. If the NLI outputs for the pairs\(a3,b2\)\(a\_\{3\},b\_\{2\}\)and\(a4,b2\)\(a\_\{4\},b\_\{2\}\)are\(Ent,0\.88\)\(\\texttt\{Ent\},0\.88\)and\(Con,0\.83\)\(\\texttt\{Con\},0\.83\), respectively, and all other comparisons withb2b\_\{2\}are neutral, thenℛc​\(b2\)=\{\(a3,b2,Ent,0\.88\),\(a4,b2,Con,0\.83\)\}\\mathcal\{R\}\_\{c\}\(b\_\{2\}\)=\\\{\(a\_\{3\},b\_\{2\},\\texttt\{Ent\},0\.88\),\(a\_\{4\},b\_\{2\},\\texttt\{Con\},0\.83\)\\\}\.

### Weighted Atom\-Link Clauses

Atom links are encoded as weighted clauses\. We write\(q,∞\)\(q,\\infty\)for a hard clause and\(q,w\)\(q,w\), withw∈ℕ\>0w\\in\\mathbb\{N\}\_\{\>0\}, for a soft clause\. Every hard clause must be satisfied, whilewwis the penalty incurred when the soft clauseqqis violated\.

###### Definition 5\(Weighted Atom\-Link Clauses\)\.

LetWmax∈ℕ\>0W\_\{\\max\}\\in\\mathbb\{N\}\_\{\>0\}be the maximum finite link weight and definew⁡\(p\)=max⁡\{1,⌊Wmax​p⌋\}w\(p\)=\\max\\\{1,\\lfloor W\_\{\\max\}p\\rfloor\\\}forp∈\[0,1\]p\\in\[0,1\], where⌊x⌋\\lfloor x\\rflooris the greatest integer not exceedingxx\. Thus,w⁡\(p\)∈\{1,…,Wmax\}w\(p\)\\in\\\{1,\\ldots,W\_\{\\max\}\\\}, with the outer maximum ensuring a positive weight\.

Each exact link\(a,b\)∈ℳcex\(a,b\)\\in\\mathcal\{M\}\_\{c\}^\{\\mathrm\{ex\}\}contributes\(\[¬a∨b\],Wmax\)\(\[\\neg a\\lor b\],W\_\{\\max\}\)and\(\[a∨¬b\],Wmax\)\(\[a\\lor\\neg b\],W\_\{\\max\}\), encodinga→ba\\rightarrow bandb→ab\\rightarrow a, respectively\. Together they form a soft equivalence\. DefineΩcex=⋃\(a,b\)∈ℳcex\{\(\[¬a∨b\],Wmax\),\(\[a∨¬b\],Wmax\)\}\\Omega\_\{c\}^\{\\mathrm\{ex\}\}=\\bigcup\_\{\(a,b\)\\in\\mathcal\{M\}\_\{c\}^\{\\mathrm\{ex\}\}\}\\\{\(\[\\neg a\\lor b\],W\_\{\\max\}\),\(\[a\\lor\\neg b\],W\_\{\\max\}\)\\\}\.

For a non\-exact linkr=\(a,b,y,p\)r=\(a,b,y,p\), letcl⁡\(r\)=\(\[¬a∨b\],w⁡\(p\)\)\\operatorname\{cl\}\(r\)=\(\[\\neg a\\lor b\],w\(p\)\)ify=Enty=\\texttt\{Ent\}, andcl⁡\(r\)=\(\[¬a∨¬b\],w⁡\(p\)\)\\operatorname\{cl\}\(r\)=\(\[\\neg a\\lor\\neg b\],w\(p\)\)ify=Cony=\\texttt\{Con\}\.

An active non\-exact link setLc⊆⋃b∈𝒰cℛc​\(b\)L\_\{c\}\\subseteq\\bigcup\_\{b\\in\\mathcal\{U\}\_\{c\}\}\\mathcal\{R\}\_\{c\}\(b\)is admissible if\|Lc∩ℛc​\(b\)\|≤1\|L\_\{c\}\\cap\\mathcal\{R\}\_\{c\}\(b\)\|\\leq 1for everyb∈𝒰cb\\in\\mathcal\{U\}\_\{c\}\. Thus, each unmatched target atom has at most one active non\-exact link\. The atom\-link clause collection induced byLcL\_\{c\}isΩcsem​\(Lc\)=Ωcex∪\{cl⁡\(r\)∣r∈Lc\}\\Omega\_\{c\}^\{\\mathrm\{sem\}\}\(L\_\{c\}\)=\\Omega\_\{c\}^\{\\mathrm\{ex\}\}\\cup\\\{\\operatorname\{cl\}\(r\)\\mid r\\in L\_\{c\}\\\}\.

Exact\-link clauses occur inΩcsem​\(Lc\)\\Omega\_\{c\}^\{\\mathrm\{sem\}\}\(L\_\{c\}\)for every admissibleLcL\_\{c\}\.

###### Example 4\(Weighted Atom\-Link Clauses\)\.

Continuing Example[3](https://arxiv.org/html/2608.18820#Thmexample3), letWmax=100W\_\{\\max\}=100\. For eachi∈\{1,2\}i\\in\\\{1,2\\\}, the exact link\(ai,b1\)\(a\_\{i\},b\_\{1\}\)contributes\(\[¬ai∨b1\],100\)\(\[\\neg a\_\{i\}\\lor b\_\{1\}\],100\)and\(\[ai∨¬b1\],100\)\(\[a\_\{i\}\\lor\\neg b\_\{1\}\],100\)\. The two non\-exact alternatives map to\(\[¬a3∨b2\],88\)\(\[\\neg a\_\{3\}\\lor b\_\{2\}\],88\)and\(\[¬a4∨¬b2\],83\)\(\[\\neg a\_\{4\}\\lor\\neg b\_\{2\}\],83\)\. An admissible configuration may activate either non\-exact link forb2b\_\{2\}, or neither, but not both\.

### Partial MaxSAT Evaluation

For a fixed active non\-exact link setLcL\_\{c\}, the evaluator compares a base instance with a forced instance that additionally requires the target clauses\. All hard clauses must be satisfied, and the solver minimizes the total weight of violated soft clauses\.

###### Definition 6\(Base and Forced MaxSAT Instances\)\.

The hard source clauses areΩchard=\{\(q,∞\)∣q∈ΓSc\}\\Omega\_\{c\}^\{\\mathrm\{hard\}\}=\\\{\(q,\\infty\)\\mid q\\in\\Gamma\_\{S\_\{c\}\}\\\}, and the target\-inertia clauses areΩcinertia=\{\(\[¬b\],ϵ\)∣b∈𝒜Tc\}\\Omega\_\{c\}^\{\\mathrm\{inertia\}\}=\\\{\(\[\\neg b\],\\epsilon\)\\mid b\\in\\mathcal\{A\}\_\{T\_\{c\}\}\\\}, whereϵ∈ℕ\>0\\epsilon\\in\\mathbb\{N\}\_\{\>0\}\. Inertia prefers false target atoms but does not require them\. Define the base and forced instances by

ℐcbase​\(Lc\)\\displaystyle\\mathcal\{I\}\_\{c\}^\{\\mathrm\{base\}\}\(L\_\{c\}\)=Ωchard∪Ωcsem​\(Lc\)∪Ωcinertia,\\displaystyle=\\Omega\_\{c\}^\{\\mathrm\{hard\}\}\\cup\\Omega\_\{c\}^\{\\mathrm\{sem\}\}\(L\_\{c\}\)\\cup\\Omega\_\{c\}^\{\\mathrm\{inertia\}\},ℐcforced​\(Lc\)\\displaystyle\\mathcal\{I\}\_\{c\}^\{\\mathrm\{forced\}\}\(L\_\{c\}\)=ℐcbase​\(Lc\)∪\{\(q,∞\)∣q∈ΓTc\}\.\\displaystyle=\\mathcal\{I\}\_\{c\}^\{\\mathrm\{base\}\}\(L\_\{c\}\)\\cup\\\{\(q,\\infty\)\\mid q\\in\\Gamma\_\{T\_\{c\}\}\\\}\.
LetMcbase​\(Lc\)M\_\{c\}^\{\\mathrm\{base\}\}\(L\_\{c\}\)andMcforced​\(Lc\)M\_\{c\}^\{\\mathrm\{forced\}\}\(L\_\{c\}\)be the assignments returned by solvingℐcbase​\(Lc\)\\mathcal\{I\}\_\{c\}^\{\\mathrm\{base\}\}\(L\_\{c\}\)andℐcforced​\(Lc\)\\mathcal\{I\}\_\{c\}^\{\\mathrm\{forced\}\}\(L\_\{c\}\), respectively\. Each assignment satisfies all hard clauses and minimizes the total weight of violated soft clauses\. When either instance has multiple optimal assignments, the correspondingMcbaseM\_\{c\}^\{\\mathrm\{base\}\}orMcforcedM\_\{c\}^\{\\mathrm\{forced\}\}is the assignment returned by the solver; no secondary optimization criterion is applied\. For any assignmentMM, define

SemCostc⁡\(M,Lc\)=∑\(q,w\)∈Ωcsem​\(Lc\)M⊧̸qw\.\\operatorname\{SemCost\}\_\{c\}\(M,L\_\{c\}\)=\\sum\_\{\\begin\{subarray\}\{c\}\(q,w\)\\in\\Omega\_\{c\}^\{\\mathrm\{sem\}\}\(L\_\{c\}\)\\\\ M\\not\\models q\\end\{subarray\}\}w\.Both assignments minimize atom\-link and inertia costs jointly\. Inertia provides a conservative default for otherwise unconstrained target atoms; as an optimization regularizer rather than atom\-link evidence, it is excluded fromSemCostc\\operatorname\{SemCost\}\_\{c\}\.

The*semantic tension*is the signed change

Δ​Tc​\(Lc\)\\displaystyle\\Delta T\_\{c\}\(L\_\{c\}\)=SemCostc⁡\(Mcforced​\(Lc\),Lc\)\\displaystyle=\\operatorname\{SemCost\}\_\{c\}\(M\_\{c\}^\{\\mathrm\{forced\}\}\(L\_\{c\}\),L\_\{c\}\)−SemCostc⁡\(Mcbase​\(Lc\),Lc\)\.\\displaystyle\-\\operatorname\{SemCost\}\_\{c\}\(M\_\{c\}^\{\\mathrm\{base\}\}\(L\_\{c\}\),L\_\{c\}\)\.

A positiveΔ​Tc​\(Lc\)\\Delta T\_\{c\}\(L\_\{c\}\)means that enforcing the target increases conflict with the active atom links; a negative value means that it reduces this conflict\.

Semantic tension does not indicate which target clauses already hold in the base optimum\. We therefore define a target\-clause witness ratioRsat,c​\(Lc\)R\_\{\\mathrm\{sat\},c\}\(L\_\{c\}\)\. The conditionNegSupc,Lc⁡\(b\)\\operatorname\{NegSup\}\_\{c,L\_\{c\}\}\(b\)prevents target inertia alone from witnessing a negative target literal\. Logical resistance combines normalized semantic tension with this ratio\. A lower value reflects lower normalized semantic tension, stronger target support, or both; a higher value reflects greater tension, weaker support, or both\.

###### Definition 7\(Target Witness and Logical Resistance\)\.

WriteMc0=Mcbase​\(Lc\)M\_\{c\}^\{0\}=M\_\{c\}^\{\\mathrm\{base\}\}\(L\_\{c\}\)\. For a target atombb, defineNegSupc,Lc⁡\(b\)\\operatorname\{NegSup\}\_\{c,L\_\{c\}\}\(b\)to hold if either there existsa∈𝒜Sca\\in\\mathcal\{A\}\_\{S\_\{c\}\}such that\(a,b\)∈ℳcex\(a,b\)\\in\\mathcal\{M\}\_\{c\}^\{\\mathrm\{ex\}\}andMc0⊧¬aM\_\{c\}^\{0\}\\models\\neg a, or there exists\(a,b,Con,p\)∈Lc\(a,b,\\texttt\{Con\},p\)\\in L\_\{c\}such thatMc0⊧aM\_\{c\}^\{0\}\\models a\. We refer to this requirement as the*polarity\-aware negative guard*\.

For a target literalℓ\\ellover atombb, letWitc,Lc⁡\(ℓ\)=1\\operatorname\{Wit\}\_\{c,L\_\{c\}\}\(\\ell\)=1if eitherℓ=b\\ell=bandMc0⊧bM\_\{c\}^\{0\}\\models b, orℓ=¬b\\ell=\\neg b,Mc0⊧¬bM\_\{c\}^\{0\}\\models\\neg b, andNegSupc,Lc⁡\(b\)\\operatorname\{NegSup\}\_\{c,L\_\{c\}\}\(b\); otherwise it is00\. Forq∈ΓTcq\\in\\Gamma\_\{T\_\{c\}\}, letWitc,Lc⁡\(q\)=maxℓ∈q⁡Witc,Lc⁡\(ℓ\)\\operatorname\{Wit\}\_\{c,L\_\{c\}\}\(q\)=\\max\_\{\\ell\\in q\}\\operatorname\{Wit\}\_\{c,L\_\{c\}\}\(\\ell\)\. ForΓTc≠∅\\Gamma\_\{T\_\{c\}\}\\neq\\varnothing, the target\-clause witness ratio is

Rsat,c​\(Lc\)=\|ΓTc\|−1​∑q∈ΓTcWitc,Lc⁡\(q\)\.R\_\{\\mathrm\{sat\},c\}\(L\_\{c\}\)=\|\\Gamma\_\{T\_\{c\}\}\|^\{\-1\}\\sum\_\{q\\in\\Gamma\_\{T\_\{c\}\}\}\\operatorname\{Wit\}\_\{c,L\_\{c\}\}\(q\)\.Because the witness ratio is clause\-based, the fixed CNF conversion keeps clause granularity consistent across scoring methods\.

The total included link weight is

Wc​\(Lc\)=Wmax​\|ℳcex\|\+∑\(a,b,y,p\)∈Lcw⁡\(p\)\.W\_\{c\}\(L\_\{c\}\)=W\_\{\\max\}\|\\mathcal\{M\}\_\{c\}^\{\\mathrm\{ex\}\}\|\+\\sum\_\{\(a,b,y,p\)\\in L\_\{c\}\}w\(p\)\.Each exact link contributesWmaxW\_\{\\max\}, because an assignment can violate at most one of its two equivalence clauses\. Let

Cmax,c​\(Lc\)=\{Wc​\(Lc\),Wc​\(Lc\)\>0,\|𝒜Tc\|​Wmax,otherwise\.C\_\{\\max,c\}\(L\_\{c\}\)=\\begin\{cases\}W\_\{c\}\(L\_\{c\}\),&W\_\{c\}\(L\_\{c\}\)\>0,\\\\ \|\\mathcal\{A\}\_\{T\_\{c\}\}\|W\_\{\\max\},&\\text\{otherwise\}\.\\end\{cases\}We useCmax,c​\(Lc\)C\_\{\\max,c\}\(L\_\{c\}\)as the normalization capacity; it is an upper bound on the active atom\-link cost but need not be attainable\. WhenWc​\(Lc\)=0W\_\{c\}\(L\_\{c\}\)=0, no atom\-link clause is active andΔ​Tc​\(Lc\)=0\\Delta T\_\{c\}\(L\_\{c\}\)=0, so the fallback denominator only prevents division by zero\. The logical resistance is

ρc​\(Lc\)=Δ​Tc​\(Lc\)Cmax,c​\(Lc\)−Rsat,c​\(Lc\)\.\\rho\_\{c\}\(L\_\{c\}\)=\\frac\{\\Delta T\_\{c\}\(L\_\{c\}\)\}\{C\_\{\\max,c\}\(L\_\{c\}\)\}\-R\_\{\\mathrm\{sat\},c\}\(L\_\{c\}\)\.

Both resistance components are computed from solver\-returned optima\. In particular, the witness ratio is not logical entailment over all assignments satisfying the source clauses\.

###### Example 5\(Logical Resistance\)\.

LetΓSc=\{\[a\]\}\\Gamma\_\{S\_\{c\}\}=\\\{\[a\]\\\},ΓTc=\{\[b\]\}\\Gamma\_\{T\_\{c\}\}=\\\{\[b\]\\\},Wmax=100W\_\{\\max\}=100, andϵ=1\\epsilon=1, with no exact links\. ForrE=\(a,b,Ent,0\.80\)r\_\{E\}=\(a,b,\\texttt\{Ent\},0\.80\)andLc=\{rE\}L\_\{c\}=\\\{r\_\{E\}\\\}, the hard source clause forcesaatrue\. The base optimum setsbbtrue because violating inertia costs11, whereas violating the entailment link costs8080; the forced optimum also setsbbtrue\. Both atom\-link costs are00, soΔ​Tc​\(Lc\)=0\\Delta T\_\{c\}\(L\_\{c\}\)=0,Rsat,c​\(Lc\)=1R\_\{\\mathrm\{sat\},c\}\(L\_\{c\}\)=1,Cmax,c​\(Lc\)=80C\_\{\\max,c\}\(L\_\{c\}\)=80, andρc​\(Lc\)=−1\\rho\_\{c\}\(L\_\{c\}\)=\-1\.

ForrC=\(a,b,Con,0\.70\)r\_\{C\}=\(a,b,\\texttt\{Con\},0\.70\)andLc=\{rC\}L\_\{c\}=\\\{r\_\{C\}\\\}, the base optimum setsbbfalse, while the forced optimum setsbbtrue and violates the weight\-7070contradiction link\. Although the forced optimum also violates inertia, inertia is excluded fromSemCostc\\operatorname\{SemCost\}\_\{c\}\. ThusΔ​Tc​\(Lc\)=70\\Delta T\_\{c\}\(L\_\{c\}\)=70,Rsat,c​\(Lc\)=0R\_\{\\mathrm\{sat\},c\}\(L\_\{c\}\)=0,Cmax,c​\(Lc\)=70C\_\{\\max,c\}\(L\_\{c\}\)=70, andρc​\(Lc\)=1\\rho\_\{c\}\(L\_\{c\}\)=1\.

If the target instead contains¬b\\neg bwithout an exact or contradiction link supporting that polarity, inertia may setbbfalse, but¬b\\neg bis not witnessed\.

Figure 1:Constructed common\-target trace\. Atom identifiers precede their italic sans\-serif verbalizations\. Arrows show confidence and clause weight \(blue: entailment; dashed red: contradiction; thick:Top\-Link\)\. PWAL treats non\-neutral links and no\-link as local alternatives; dotted neutral is discarded\.
### Top\-Linkand PWAL

The two scoring methods use the same source and target formulae, exact links, non\-exact link inventory, clause\-construction rule, and MaxSAT evaluator\.Top\-Linkevaluates one admissible non\-exact link configuration, whereas PWAL averages logical resistance over a distribution of such configurations\.

###### Definition 8\(Top\-Link\)\.

For eachb∈𝒰cb\\in\\mathcal\{U\}\_\{c\}withℛc​\(b\)≠∅\\mathcal\{R\}\_\{c\}\(b\)\\neq\\varnothing, definerc⋆​\(b\)∈arg⁡max\(a,b,y,p\)∈ℛc​\(b\)⁡pr\_\{c\}^\{\\star\}\(b\)\\in\\arg\\max\_\{\(a,b,y,p\)\\in\\mathcal\{R\}\_\{c\}\(b\)\}pas a maximum\-confidence link, breaking confidence ties by a fixed total order on𝒜Sc\\mathcal\{A\}\_\{S\_\{c\}\}induced by source\-statement order and the translator’s atom order\. SetLctop=\{rc⋆\(b\)∣b∈𝒰c,ℛc\(b\)≠∅\}L\_\{c\}^\{\\mathrm\{top\}\}=\\\{r\_\{c\}^\{\\star\}\(b\)\\mid b\\in\\mathcal\{U\}\_\{c\},\\,\\mathcal\{R\}\_\{c\}\(b\)\\neq\\varnothing\\\}andσctop=ρc​\(Lctop\)\\sigma\_\{c\}^\{\\mathrm\{top\}\}=\\rho\_\{c\}\(L\_\{c\}^\{\\mathrm\{top\}\}\)\. Ifℛc​\(b\)=∅\\mathcal\{R\}\_\{c\}\(b\)=\\varnothing, no non\-exact link is selected forbb\.

PWAL treats every non\-neutral link and the no\-link outcome as local alternatives for each unmatched target atom\.

###### Definition 9\(PWAL\)\.

For eachb∈𝒰cb\\in\\mathcal\{U\}\_\{c\}, define𝒵c,b=\{∅\}∪ℛc​\(b\)\\mathcal\{Z\}\_\{c,b\}=\\\{\\varnothing\\\}\\cup\\mathcal\{R\}\_\{c\}\(b\), where∅\\varnothingdenotes no active non\-exact link\. PWAL assigns every local outcome equal probability:πc,b​\(z\)=1/\(\|ℛc​\(b\)\|\+1\)\\pi\_\{c,b\}\(z\)=1/\(\|\\mathcal\{R\}\_\{c\}\(b\)\|\+1\)forz∈𝒵c,bz\\in\\mathcal\{Z\}\_\{c,b\}\. Ifℛc​\(b\)=∅\\mathcal\{R\}\_\{c\}\(b\)=\\varnothing, thenπc,b​\(∅\)=1\\pi\_\{c,b\}\(\\varnothing\)=1\.

Let𝒲c=∏b∈𝒰c𝒵c,b\\mathcal\{W\}\_\{c\}=\\prod\_\{b\\in\\mathcal\{U\}\_\{c\}\}\\mathcal\{Z\}\_\{c,b\}\. Eachωc=\(zb\)b∈𝒰c∈𝒲c\\omega\_\{c\}=\(z\_\{b\}\)\_\{b\\in\\mathcal\{U\}\_\{c\}\}\\in\\mathcal\{W\}\_\{c\}activatesLcωc=\{zb∣zb≠∅\}L\_\{c\}^\{\\omega\_\{c\}\}=\\\{z\_\{b\}\\mid z\_\{b\}\\neq\\varnothing\\\}\. Assuming target\-wise independent local link choices,πc​\(ωc\)=∏b∈𝒰cπc,b​\(zb\)=1/Ncworld\\pi\_\{c\}\(\\omega\_\{c\}\)=\\prod\_\{b\\in\\mathcal\{U\}\_\{c\}\}\\pi\_\{c,b\}\(z\_\{b\}\)=1/N\_\{c\}^\{\\mathrm\{world\}\}, whereNcworld=\|𝒲c\|=∏b∈𝒰c\(\|ℛc​\(b\)\|\+1\)N\_\{c\}^\{\\mathrm\{world\}\}=\|\\mathcal\{W\}\_\{c\}\|=\\prod\_\{b\\in\\mathcal\{U\}\_\{c\}\}\(\|\\mathcal\{R\}\_\{c\}\(b\)\|\+1\)\. Logical dependencies among target atoms remain encoded inΦTc\\Phi\_\{T\_\{c\}\}and the MaxSAT instances\. Exact\-link clauses are included in every world and add no local choices\.

When all worlds are enumerated, the candidate score is

σcPWAL=μc=∑ωc∈𝒲cπc​\(ωc\)​ρc​\(Lcωc\)\.\\sigma\_\{c\}^\{\\mathrm\{PWAL\}\}=\\mu\_\{c\}=\\sum\_\{\\omega\_\{c\}\\in\\mathcal\{W\}\_\{c\}\}\\pi\_\{c\}\(\\omega\_\{c\}\)\\rho\_\{c\}\(L\_\{c\}^\{\\omega\_\{c\}\}\)\.ForK∈ℕ\>0K\\in\\mathbb\{N\}\_\{\>0\}i\.i\.d\. sampled worldsωc\(1\),…,ωc\(K\)∼πc\\omega\_\{c\}^\{\(1\)\},\\ldots,\\omega\_\{c\}^\{\(K\)\}\\sim\\pi\_\{c\}, it is estimated by

σ^cPWAL=μ^c=K−1​∑k=1Kρc​\(Lcωc\(k\)\)\.\\widehat\{\\sigma\}\_\{c\}^\{\\mathrm\{PWAL\}\}=\\widehat\{\\mu\}\_\{c\}=K^\{\-1\}\\sum\_\{k=1\}^\{K\}\\rho\_\{c\}\(L\_\{c\}^\{\\omega\_\{c\}^\{\(k\)\}\}\)\.Thus,μ^c\\widehat\{\\mu\}\_\{c\}is a finite\-KKMonte Carlo estimator ofμc\\mu\_\{c\}, the expected logical resistance\.

NLI confidence determines the within\-world clause weightw⁡\(p\)w\(p\), not the world probability\. A world specifies one alternative cross\-formula atom\-link configuration: the statement formulae and exact\-link clauses remain fixed, while the active non\-exact links vary\. PWAL compares expected resistance rather than the number of worlds won by each candidate\.

Figure[1](https://arxiv.org/html/2608.18820#Sx3.F1)gives a trace\-level illustration of this mechanism\.

Table 1:Pairwise test results \(%\)\. PWAL variants report ten\-seed means±\\pmsample SD \(K=100K=100\); other methods are deterministic\. FailedFH\-HardSATevaluations count as errors; bold marks the best Acc among non\-ablated logical methods\.

## Experimental Setup

##### Tasks and pair construction\.

Each instance contains two candidate\-specific source–target pairs,\(SA,TA\)\(S\_\{A\},T\_\{A\}\)and\(SB,TB\)\(S\_\{B\},T\_\{B\}\), with one designated gold candidate\. We use ARCT\([Habernal et al\. 2018](https://arxiv.org/html/2608.18820#bib.bib11)\)andα\\alphaNLI\([Bhagavatula et al\. 2020](https://arxiv.org/html/2608.18820#bib.bib4)\)in their original pairwise form, and derive pairwise tasks from CDED\([Rinott et al\. 2015](https://arxiv.org/html/2608.18820#bib.bib31)\), iDebate\([Wang and Ling 2016](https://arxiv.org/html/2608.18820#bib.bib35)\), and AAE2\([Stab and Gurevych 2017](https://arxiv.org/html/2608.18820#bib.bib33)\)\.

ARCT usesSc=\(reason,warrantc\)S\_\{c\}=\(\\text\{reason\},\\text\{warrant\}\_\{c\}\)andTc=\(claim\)T\_\{c\}=\(\\text\{claim\}\)\.α\\alphaNLI usesSc=\(O1,hypothesisc\)S\_\{c\}=\(O\_\{1\},\\text\{hypothesis\}\_\{c\}\)andTc=\(O2\)T\_\{c\}=\(O\_\{2\}\)\.

For the derived tasks, superscripts\+\+and−\-denote the gold and distractor items, not candidate positions or stance labels\. In CDED,TA=TB=\(Ci\)T\_\{A\}=T\_\{B\}=\(C\_\{i\}\)and\{SA,SB\}=\{\(Hi\+\),\(Hi−\)\}\\\{S\_\{A\},S\_\{B\}\\\}=\\\{\(H\_\{i\}^\{\+\}\),\(H\_\{i\}^\{\-\}\)\\\}, whereHi\+H\_\{i\}^\{\+\}is annotated as evidence forCiC\_\{i\}, andHi−H\_\{i\}^\{\-\}is a same\-topic passage annotated as evidence for another claim but not annotated as evidence forCiC\_\{i\}\.

For the two derived missing\-claim tasks, letPi=\(pi,1,…,pi,ni\)P\_\{i\}=\(p\_\{i,1\},\\ldots,p\_\{i,n\_\{i\}\}\)denote the source statement collection paired with gold claimCi\+C\_\{i\}^\{\+\}\. We setSA=SB=PiS\_\{A\}=S\_\{B\}=P\_\{i\}and\{TA,TB\}=\{\(Ci\+\),\(Ci−\)\}\\\{T\_\{A\},T\_\{B\}\\\}=\\\{\(C\_\{i\}^\{\+\}\),\(C\_\{i\}^\{\-\}\)\\\}\. In iDebate,PiP\_\{i\}is the argumentative statement collection associated with central claimCi\+C\_\{i\}^\{\+\}, andCi−C\_\{i\}^\{\-\}is a different central claim from the same debate\. In AAE2,PiP\_\{i\}contains all premise components directly annotated as supportingCi\+C\_\{i\}^\{\+\}, andCi−C\_\{i\}^\{\-\}is an opposite\-stance claim from the same essay such that no premise inPiP\_\{i\}has an annotated relation path to it\. Because stance is defined relative to the essay’s major claim,Ci−C\_\{i\}^\{\-\}is not assumed to be the logical negation ofCi\+C\_\{i\}^\{\+\}\.

We evaluate the full444444\-example ARCT test set, a fixed400400\-instance sample from the officialα\\alphaNLI test split, fixed400400\-instance samples from the derived CDED and iDebate pools, and a fixed350350\-instance AAE2 test set\. Construction metadata are excluded from method inputs; development and test groups are disjoint \(see supplementary material\)\.

##### Compared methods\.

The controlled comparison is between PWAL andTop\-Link\. Both use the same source and target formulae, exact links, NLI\-derived alternatives, clause weights, and Partial MaxSAT evaluator\. We additionally reportFH\-HardSAT, the prior neuro\-symbolic method\([Feng and Hunter 2026](https://arxiv.org/html/2608.18820#bib.bib9)\), andDirect NLI\.

FH\-HardSATevaluates the candidates independently and selects a candidate only when exactly one is entailed\. Equal valid outcomes produce a tie\. Its similarity and contradiction thresholds are selected separately for each dataset using held\-out development data\.

Direct NLIusesuc=cat⁡\(Sc\)u\_\{c\}=\\operatorname\{cat\}\(S\_\{c\}\)andvc=cat⁡\(Tc\)v\_\{c\}=\\operatorname\{cat\}\(T\_\{c\}\), wherecat⁡\(X\)\\operatorname\{cat\}\(X\)concatenates the statements inXXin their listed order, separated by a single space\. It applies the NLI model used for atom\-link construction\. Letpℓ​\(u,v\)p\_\{\\ell\}\(u,v\)denote the probability assigned by this model to labelℓ∈𝒴\\ell\\in\\mathcal\{Y\}\. It scores candidateccbyscNLI=pEnt​\(uc,vc\)−pCon​\(uc,vc\)s\_\{c\}^\{\\mathrm\{NLI\}\}=p\_\{\\mathrm\{Ent\}\}\(u\_\{c\},v\_\{c\}\)\-p\_\{\\mathrm\{Con\}\}\(u\_\{c\},v\_\{c\}\)\. It selects the candidate with the higher score; score differences within the numerical tolerance specified below are treated as ties\. No such ties occur in the reported test sets\. It uses no AMR translation, atom links, or MaxSAT inference\.

##### Implementation\.

Top\-Link, PWAL, and the component ablations use the logical\-resistance score defined above, without reweighting its two components\. We setWmax=100W\_\{\\max\}=100, the target\-inertia weight toϵ=1\\epsilon=1, and the main PWAL sampling budget toK=100K=100\. Sampled PWAL results, including ablations and each sampling budget, use seeds 2026–2035 and are reported as means±\\pmsample standard deviations\. Dataset\-level metrics are computed separately for each seed before aggregation\.Top\-Link,FH\-HardSAT,Direct NLI, and the fixed exact/10510^\{5\}\-capped references are reported as single values\.

We use Structured\-BART for AMR parsing\([Zhou et al\. 2021](https://arxiv.org/html/2608.18820#bib.bib39);[Lee et al\. 2022](https://arxiv.org/html/2608.18820#bib.bib21)\), the frozen rule\-based AMR\-to\-logic compiler specified in the supplementary material, mDeBERTa\-v3 for NLI\-based atom\-link construction\([He, Gao, and Chen 2023](https://arxiv.org/html/2608.18820#bib.bib12);[Laurer 2024](https://arxiv.org/html/2608.18820#bib.bib20)\), and RC2 in PySAT for Partial MaxSAT inference\([Ignatiev, Morgado, and Marques\-Silva 2018](https://arxiv.org/html/2608.18820#bib.bib16)\)\. In implementation,\|σA−σB\|≤τtie\\lvert\\sigma\_\{A\}\-\\sigma\_\{B\}\\rvert\\leq\\tau\_\{\\mathrm\{tie\}\}is treated as a tie, withτtie=10−12\\tau\_\{\\mathrm\{tie\}\}=10^\{\-12\}\.

##### Metrics\.

LetNwin,Nerr,NtieN\_\{\\mathrm\{win\}\},N\_\{\\mathrm\{err\}\},N\_\{\\mathrm\{tie\}\}denote correct unique selections, errors, and valid ties, respectively, withN=Nwin\+Nerr\+NtieN=N\_\{\\mathrm\{win\}\}\+N\_\{\\mathrm\{err\}\}\+N\_\{\\mathrm\{tie\}\}\. A valid tie is a successful evaluation returned asTieby this decision rule\. Errors include incorrect unique selections and failed evaluations\. We reportAccuracy=Nwin/N\\operatorname\{Accuracy\}=N\_\{\\mathrm\{win\}\}/N,TieRate=Ntie/N\\operatorname\{TieRate\}=N\_\{\\mathrm\{tie\}\}/N, andEAcc=\(Nwin\+12​Ntie\)/N\\operatorname\{EAcc\}=\(N\_\{\\mathrm\{win\}\}\+\\tfrac\{1\}\{2\}N\_\{\\mathrm\{tie\}\}\)/N\. Accuracy is the primary metric\. EAcc gives valid ties half credit and errors none, corresponding to uniform random tie\-breaking for evaluation only\. We use pointwise 95% paired two\-way bootstrap intervals over dataset\-specific source clusters and seed runs \(10,000 replicates\)\.

Table 2:Sampling and exact/10510^\{5\}\-capped reference results \(%\)\. Ref\. denotes the exact/10510^\{5\}\-capped reference\.

## Results

##### Main Results

Table[1](https://arxiv.org/html/2608.18820#Sx3.T1)reports the test results\. All differences discussed below are computed from unrounded values\.

FH\-HardSATreturns valid ties on49\.7549\.75–86\.71%86\.71\\%of examples and has lower Acc and EAcc thanTop\-Linkand PWAL on every task\. Relative toTop\-Link, PWAL raises mean Acc by2\.952\.95–30\.8630\.86percentage points, lowers mean Tie by4\.574\.57–58\.0058\.00percentage points, and raises mean EAcc by0\.450\.45–6\.046\.04percentage points across the five tasks\. OnTop\-Linkties, PWAL’s mean EAcc is49\.36%49\.36\\%–57\.13%57\.13\\%, versus50%50\\%under uniform tie\-breaking\. AmongTop\-Link’s unique decisions, mean wrong\-to\-correct repairs exceed correct\-to\-wrong damages on all five tasks\. Full transition matrices are reported in the supplementary material\. Paired bootstrap analysis supports the Acc gains onα\\alphaNLI, ARCT, and CDED, while the smaller Acc gains on iDebate and AAE2 remain uncertain\.

Direct NLIhas the highest EAcc on every task, exceeding PWAL by5\.215\.21–15\.7115\.71percentage points\. It is a predictive reference rather than a controlled logical comparator; PWAL andTop\-Linkshare the formalization and scoring pipeline except for the treatment of non\-exact link configurations\.

Removing the no\-link outcome lowers mean Acc and raises mean Tie on all five tasks; the corresponding Full\-minus\-ablation Acc intervals exclude zero onα\\alphaNLI, ARCT, and CDED\. Removing the negative guard lowers mean Acc on every task, with intervals excluding zero on ARCT and CDED\. EAcc may increase when an ablation produces additional ties because each valid tie receives half credit\.

##### Sampling Approximation and Exact/Capped Reference

We evaluateK∈\{10,20,50,100,200\}K\\in\\\{10,20,50,100,200\\\}over ten seeds\. Within each seed, the smaller budgets are prefixes of the sameK=200K=200world stream\. For the reference, a candidate is fully enumerated when its world count is at most10510^\{5\}; otherwise,10510^\{5\}worlds are sampled uniformly without replacement using seed 2026\. A pair is fully exact only when both candidate scores are enumerated\. The resulting fully exact pair counts are357/400357/400,443/444443/444,216/400216/400,146/400146/400, and93/35093/350forα\\alphaNLI, ARCT, CDED, iDebate, and AAE2, respectively\. Every other pair contains at least one capped candidate\. Table[2](https://arxiv.org/html/2608.18820#Sx4.T2)reportsK∈\{100,200\}K\\in\\\{100,200\\\}and the exact/10510^\{5\}\-capped reference; the full budget grid, timing protocol, and runtime distributions are reported in the supplementary material\.

AtK=100K=100, the across\-seed standard deviation is at most1\.121\.12points for Acc,0\.500\.50for Tie, and1\.071\.07for EAcc\. IncreasingKKfrom100100to200200changes mean Acc by at most1\.101\.10points and mean Tie by at most0\.680\.68points\. Mean EAcc changes by at most0\.200\.20points on four tasks and by1\.021\.02points on ARCT\. TheK=100K=100mean EAcc is within1\.071\.07points of the exact/10510^\{5\}\-capped reference on every task, supportingK=100K=100as a practical cost–stability setting\.

ARCT has the largest sampled–reference difference\. The reference raises Tie from6\.87%6\.87\\%to14\.41%14\.41\\%, lowers Acc from50\.90%50\.90\\%to48\.20%48\.20\\%, and raises EAcc from54\.34%54\.34\\%to55\.41%55\.41\\%\. All6464reference\-tied ARCT pairs are fully exact, with absolute expected\-resistance margins of at most10−1210^\{\-12\}\. Finite\-KKMonte Carlo estimates can break these ties, helping explain why sampled strict Acc is higher while sampled EAcc is lower\. On the other four tasks, reference EAcc differs from theK=100K=100mean by at most0\.750\.75points\.

Restricting the analysis to fully exact pairs,K=100K=100agrees with exact marginalization on83\.02%83\.02\\%–98\.39%98\.39\\%of decisions across the five tasks, averaged over ten seeds\. AmongK=100K=100’s incorrect unique decisions on these pairs,78\.72%78\.72\\%–98\.90%98\.90\\%remain incorrect under exact marginalization\. Thus, most of these errors are not removed by eliminating finite\-KKapproximation\. Dataset\-level analyses of score error, margin error, decision transitions, and exact/capped strata are reported in the supplementary material\.

On the controlled fully enumerable runtime subset,Top\-Linktakes1\.101\.10–1\.681\.68ms/example\. Relative toTop\-Link, the mean task\-level runtime multipliers are approximately84×84\\times,172×172\\times, and5\.8×1035\.8\\times 10^\{3\}forK=100K=100,K=200K=200, and exact enumeration, respectively\.

## Conclusion

We introduced PWAL, a pairwise logical method that averages logical resistance over alternative cross\-formula atom\-link configurations, rather than committing to a single highest\-confidence configuration\.

Across five tasks spanning missing\-premise, missing\-claim, and abductive selection, PWAL achieves higher mean strict accuracy and lower mean tie rates thanTop\-Link\. PWAL also achieves higher mean EAcc on all five tasks\.Direct NLIremains the stronger predictive reference, whereas PWAL exposes the formulae, link configurations, and resistance components underlying each decision\.

The framework is limited to two candidates, one fixed AMR\-derived propositional representation per statement, and independent uniform distributions over local link choices\. It also inherits errors from AMR parsing, AMR\-to\-logic compilation, and NLI\-based atom\-link construction, while its Monte Carlo estimates vary with the sampling budget and seed\. Future work will study alternative structured representations and joint uncertainty over representations and links, dependent or learned link distributions, more efficient exact inference and adaptive sampling, absolute verification of individual candidates, and selection among more than two candidates\.

## References

- Bach et al\. \(2017\)Bach, S\. H\.; Broecheler, M\.; Huang, B\.; and Getoor, L\. 2017\.Hinge\-Loss Markov Random Fields and Probabilistic Soft Logic\.*Journal of Machine Learning Research*, 18\(109\): 1–67\.
- Banarescu et al\. \(2013\)Banarescu, L\.; Bonial, C\.; Cai, S\.; Georgescu, M\.; Griffitt, K\.; Hermjakob, U\.; Knight, K\.; Koehn, P\.; Palmer, M\.; and Schneider, N\. 2013\.Abstract Meaning Representation for Sembanking\.In*Proceedings of the 7th Linguistic Annotation Workshop and Interoperability with Discourse*, 178–186\. Association for Computational Linguistics\.
- Ben\-Naim, David, and Hunter \(2025\)Ben\-Naim, J\.; David, V\.; and Hunter, A\. 2025\.An Axiomatic Study of a Modular Evaluation of Enthymeme Decoding in Weighted Structured Argumentation\.In*Proceedings of KR’25*, 110–120\.
- Bhagavatula et al\. \(2020\)Bhagavatula, C\.; Le Bras, R\.; Malaviya, C\.; Sakaguchi, K\.; Holtzman, A\.; Rashkin, H\.; Downey, D\.; Yih, S\. W\.; and Choi, Y\. 2020\.Abductive Commonsense Reasoning\.In*International Conference on Learning Representations*\.
- Black and Hunter \(2012\)Black, E\.; and Hunter, A\. 2012\.A Relevance\-theoretic Framework for Constructing and Deconstructing Enthymemes\.*Journal of Logic and Computation*, 22\(1\): 55–78\.
- Bos \(2016\)Bos, J\. 2016\.Squib: Expressive Power of Abstract Meaning Representations\.*Computational Linguistics*, 42\(3\): 527–535\.
- David and Hunter \(2025\)David, V\.; and Hunter, A\. 2025\.A Logic\-based Framework for Decoding Enthymemes in Argument Maps Involving Implicitness in Premises and Claims\.In*Proceedings of IJCAI’25*, 4445–4453\. IJCAI Organization\.
- de Saint\-Cyr \(2011\)de Saint\-Cyr, F\. D\. 2011\.Handling Enthymemes in Time\-Limited Persuasion Dialogs\.In*Proceedings of SUM’11*, volume 6929 of*LNCS*, 149–162\. Springer\.ISBN 978\-3\-642\-23963\-2\.
- Feng and Hunter \(2026\)Feng, X\.; and Hunter, A\. 2026\.Making Implicit Premises Explicit in Logical Understanding of Enthymemes\.*arXiv*, 2603\.06114\.
- Goodman \(2020\)Goodman, M\. W\. 2020\.Penman: An Open\-Source Library and Tool for AMR Graphs\.In Celikyilmaz, A\.; and Wen, T\.\-H\., eds\.,*Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics: System Demonstrations*, 312–319\. Online: Association for Computational Linguistics\.
- Habernal et al\. \(2018\)Habernal, I\.; Wachsmuth, H\.; Gurevych, I\.; and Stein, B\. 2018\.The Argument Reasoning Comprehension Task: Identification and Reconstruction of Implicit Warrants\.In*Proceedings of NAACL’18*, 1930–1940\. Association for Computational Linguistics\.
- He, Gao, and Chen \(2023\)He, P\.; Gao, J\.; and Chen, W\. 2023\.DeBERTaV3: Improving DeBERTa Using ELECTRA\-Style Pre\-Training with Gradient\-Disentangled Embedding Sharing\.In*The Eleventh International Conference on Learning Representations*\.
- Hosseini, Modgil, and Rodrigues \(2014\)Hosseini, S\.; Modgil, S\.; and Rodrigues, O\. 2014\.Enthymeme construction in dialogues using shared knowledge\.In*Proceedings of COMMA’14*, volume 266 of*FAIA*, 325–332\. IOS Press\.
- Hunter \(2007\)Hunter, A\. 2007\.Real arguments are approximate arguments\.In*Proceedings of AAAI’07*, 66–71\. AAAI Press\.ISBN 9781577353232\.
- Hunter \(2022\)Hunter, A\. 2022\.Understanding Enthymemes in Deductive Argumentation Using Semantic Distance Measures\.In*Proceedings of AAAI’22*, 5729–5736\. AAAI Press\.
- Ignatiev, Morgado, and Marques\-Silva \(2018\)Ignatiev, A\.; Morgado, A\.; and Marques\-Silva, J\. 2018\.PySAT: A Python Toolkit for Prototyping with SAT Oracles\.In*Proc\. SAT’18*, volume 10929 of*LNCS*, 428–437\. Springer\.
- Kingsbury and Palmer \(2002\)Kingsbury, P\.; and Palmer, M\. 2002\.From TreeBank to PropBank\.In*Proceedings of LREC’02*\. European Language Resources Association \(ELRA\)\.
- Kirtania, Gupta, and Radhakrishna \(2024\)Kirtania, S\.; Gupta, P\.; and Radhakrishna, A\. 2024\.LOGIC\-LM\+\+: Multi\-Step Refinement for Symbolic Formulations\.In*Proceedings of the 2nd Workshop on Natural Language Reasoning and Structured Explanations \(@ACL 2024\)*, 56–63\. Bangkok, Thailand: Association for Computational Linguistics\.
- Ku et al\. \(2025\)Ku, H\. B\.; Shin, J\.; Lee, H\. J\.; Na, S\.; and Jeon, I\. 2025\.Multi\-Agent LLM Debate Unveils the Premise Left Unsaid\.In*Proceedings of the 12th Argument Mining Workshop*, 58–73\. Vienna, Austria: Association for Computational Linguistics\.
- Laurer \(2024\)Laurer, M\. 2024\.mDeBERTa\-v3\-base\-xnli\-multilingual\-nli\-2mil7\.Hugging Face model card, revision b5113eb38ab63efdd7f280f8c144ea8b13f978ce\.
- Lee et al\. \(2022\)Lee, Y\.\-S\.; Astudillo, R\.; Thanh Lam, H\.; Naseem, T\.; Florian, R\.; and Roukos, S\. 2022\.Maximum Bayes Smatch Ensemble Distillation for AMR Parsing\.In*Proceedings of the 2022 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies*, 5379–5392\. Association for Computational Linguistics\.
- Leiva, García, and Gottifredi \(2025\)Leiva, D\. S\. O\.; García, A\. J\.; and Gottifredi, S\. 2025\.Principles for Assumptions Generation in Enthymeme\-Based Dialogue\.*Journal of Artificial Intelligence Research*, 83\.
- Leiva, Gottifredi, and García \(2023\)Leiva, D\. S\. O\.; Gottifredi, S\.; and García, A\. J\. 2023\.Automatic knowledge generation for a persuasion dialogue system with enthymemes\.*International Journal of Approximate Reasoning*, 160: 108963\.
- Meurer et al\. \(2017\)Meurer, A\.; Smith, C\. P\.; Paprocki, M\.; Čertík, O\.; Kirpichev, S\. B\.; Rocklin, M\.; Kumar, A\.; Ivanov, S\.; Moore, J\. K\.; Singh, S\.; Rathnayake, T\.; Vig, S\.; Granger, B\. E\.; Muller, R\. P\.; Bonazzi, F\.; Gupta, H\.; Vats, S\.; Johansson, F\.; Pedregosa, F\.; Curry, M\. J\.; Terrel, A\. R\.; Roučka, Š\.; Saboo, A\.; Fernando, I\.; Kulal, S\.; Cimrman, R\.; and Scopatz, A\. 2017\.SymPy: symbolic computing in Python\.*PeerJ Computer Science*, 3: e103\.
- Olausson et al\. \(2023\)Olausson, T\. X\.; Gu, A\.; Lipkin, B\.; Zhang, C\. E\.; Solar\-Lezama, A\.; Tenenbaum, J\. B\.; and Levy, R\. P\. 2023\.LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First\-Order Logic Provers\.In*Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing*, 5153–5176\. Singapore: Association for Computational Linguistics\.
- OpenAI \(2026\)OpenAI\. 2026\.GPT\-5\.6: Frontier Intelligence That Scales with Your Ambition\.Available athttps://openai\.com/index/gpt\-5\-6/\. Accessed 2026\-08\-02\.
- Pan et al\. \(2023\)Pan, L\.; Albalak, A\.; Wang, X\.; and Wang, W\. Y\. 2023\.Logic\-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning\.In*Findings of the Association for Computational Linguistics: EMNLP 2023*, 3806–3824\. Singapore: Association for Computational Linguistics\.
- Panisson, McBurney, and Bordini \(2022\)Panisson, A\. R\.; McBurney, P\.; and Bordini, R\. H\. 2022\.Towards an Enthymeme\-Based Communication Framework in Multi\-Agent Systems\.In*Proceedings of KR’22*, 267–277\.
- Richardson and Domingos \(2006\)Richardson, M\.; and Domingos, P\. 2006\.Markov Logic Networks\.*Machine Learning*, 62\(1–2\): 107–136\.
- Riegel et al\. \(2020\)Riegel, R\.; Gray, A\.; Luus, F\.; Khan, N\.; Makondo, N\.; Akhalwaya, I\. Y\.; Qian, H\.; Fagin, R\.; Barahona, F\.; Sharma, U\.; Ikbal, S\.; Karanam, H\.; Neelam, S\.; Likhyani, A\.; and Srivastava, S\. 2020\.Logical Neural Networks\.arXiv:2006\.13155\.
- Rinott et al\. \(2015\)Rinott, R\.; Dankin, L\.; Alzate Perez, C\.; Khapra, M\. M\.; Aharoni, E\.; and Slonim, N\. 2015\.Show Me Your Evidence—An Automatic Method for Context Dependent Evidence Detection\.In*Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing*, 440–450\. Lisbon, Portugal: Association for Computational Linguistics\.
- Singh et al\. \(2022\)Singh, K\.; Inoue, N\.; Mim, F\. S\.; Naito, S\.; and Inui, K\. 2022\.IRAC: A Domain\-Specific Annotated Corpus of Implicit Reasoning in Arguments\.In*Proceedings of LREC’22*, 4674–4683\. European Language Resources Association\.
- Stab and Gurevych \(2017\)Stab, C\.; and Gurevych, I\. 2017\.Parsing Argumentation Structures in Persuasive Essays\.*Computational Linguistics*, 43\(3\): 619–659\.
- Sviridova, Cabrio, and Villata \(2026\)Sviridova, E\.; Cabrio, E\.; and Villata, S\. 2026\.Mining Implicit Arguments for Reasoning: A Survey\.*Argument & Computation*, 17\(1\): 3–27\.First published online 30 June 2025\.
- Wang and Ling \(2016\)Wang, L\.; and Ling, W\. 2016\.Neural Network\-Based Abstract Generation for Opinions and Arguments\.In Knight, K\.; Nenkova, A\.; and Rambow, O\., eds\.,*Proceedings of the 2016 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies*, 47–57\. San Diego, California: Association for Computational Linguistics\.
- Xiao et al\. \(2024\)Xiao, S\.; Liu, Z\.; Zhang, P\.; Muennighoff, N\.; Lian, D\.; and Nie, J\.\-Y\. 2024\.C\-Pack: Packed Resources For General Chinese Embeddings\.In*Proceedings of SIGIR’24*, 641–649\. Association for Computing Machinery\.ISBN 9798400704314\.
- Xydis et al\. \(2020\)Xydis, A\.; Hampson, C\.; Modgil, S\.; and Black, E\. 2020\.Enthymemes in dialogues\.In*Proceedings of COMMA’20*, volume 326 of*FAIA*, 395–402\. IOS Press\.
- Ye et al\. \(2023\)Ye, X\.; Chen, Q\.; Dillig, I\.; and Durrett, G\. 2023\.SatLM: Satisfiability\-Aided Language Models Using Declarative Prompting\.In*Advances in Neural Information Processing Systems*, volume 36\.
- Zhou et al\. \(2021\)Zhou, J\.; Naseem, T\.; Fernandez Astudillo, R\.; Lee, Y\.\-S\.; Florian, R\.; and Roukos, S\. 2021\.Structure\-aware Fine\-tuning of Sequence\-to\-sequence Transformers for Transition\-based AMR Parsing\.In*Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing*, 6279–6290\. Association for Computational Linguistics\.

## Appendix ADataset Construction and Validity

Every evaluation instance contains two candidate\-specific source–target pairs,\(SA,TA\)\(S\_\{A\},T\_\{A\}\)and\(SB,TB\)\(S\_\{B\},T\_\{B\}\), and a gold candidatey∈\{A,B\}y\\in\\\{A,B\\\}\. Table[A\.1](https://arxiv.org/html/2608.18820#A1.T1)summarizes the mapping from each released dataset to this interface, the candidate\-construction rule, the development and test sizes, and the cluster unit\. Topic, debate, prompt, stance, and essay identifiers are used only to construct examples, prevent split leakage, and define bootstrap clusters\. They are not included inScS\_\{c\},TcT\_\{c\},Direct NLIinput, or symbolic solver input\.

### A\.1Pair Mappings and Dataset Splits

We retain each complete CDED evidence passage as one source text unit because CDED supervision is passage\-level; sentence\-level segmentation would introduce an additional unannotated aggregation choice\.

Forα\\alphaNLI, NumPy seed 1129 selects 400 examples from the official development pool and 400 from the official test pool after exact duplicate removal\. ARCT development combines 205 deduplicated official\-development rows with 195 deduplicated official\-training rows under the same seed; test retains all 444 official\-test rows in official order\. Both tasks retain the released candidate order and have no complete\-example or candidate\-pair overlap between development and test\.

The three derived tasks use deterministic distractor rules\. CDED first prefers the same released evidence type and then minimizes token\-length difference, subject to token Jaccard similarity below0\.900\.90; its token units are lower\-cased ASCII alphanumeric substrings\. For iDebate, seed 2026 selects 400 eligible test claims and assigns same\-debate distractors injectively by minimizing total and then maximum token\-length difference; its token units are case\-folded Unicode word tokens with optional internal apostrophes\. AAE2 minimizes claim\-length difference subject to nonidentity, token Jaccard below0\.900\.90, no graph reachability, and no support\-evidence overlap; indirect ancestors and attack neighbors are excluded from its source\. Its tokenizer additionally applies Unicode NFKC normalization before case folding\. Residual distractor\-assignment ties are resolved deterministically; candidate order is fixed so that gold positions are balanced 1:1 for all three derived tasks\.

CDED development and test use 19 and 39 disjoint topics, respectively\. iDebate development combines 166 eligible official\-development claims with 234 official\-training claims; test contains 400 of the 417 eligible non\-singleton official\-test claims\. AAE2 development contains 200 examples from 78 official\-training essays; its 350\-example test set uses 127 disjoint essays and comprises 103 official\-test and 247 official\-training targets\. Topic, debate, and essay identifiers are disjoint across the corresponding development and test splits, and the task\-specific overlap checks find no cross\-split leakage\.

##### iDebate qualification\.

The same\-debate distractor is topic\-controlled but lacks an iDebate annotation establishing that it is unsupported by the source statement collection\. It may therefore receive partial support\. This ambiguity is not used for filtering or scoring, and debate\-clustered intervals account for repeated examples from one debate\.

Table A\.1:Source–target mappings, split sizes, and cluster units\. Dataset subsampling is without replacement\. Candidate positions are balanced for the three derived tasks \(CDED, iDebate, and AAE2\);α\\alphaNLI and ARCT retain their released candidate order\. Parentheses denote ordered statement collections, including singleton targets\.

### A\.2AAE2 Graph Extraction

AAE2 requires an explicit distinction between the released essay graph and the text passed to the decoder\. For a gold ClaimC\+C^\{\+\}, we retain only Premises whose outgoing relation is a direct support edge toC\+C^\{\+\}\. Premises that support one of those Premises, components that attackC\+C^\{\+\}, and the support subtree of the opposite\-stance ClaimC−C^\{\-\}remain outside the source\. Because stance is defined relative to the essay’s major claim,C−C^\{\-\}is not assumed to be the logical negation ofC\+C^\{\+\}\. Figure[A\.1](https://arxiv.org/html/2608.18820#A1.F1)shows this extraction\.

Figure A\.1:AAE2 extraction\. The source contains every Premise with a direct support edge to the gold Claim and no other argument component\. The opposite\-stance distractor is selected from the same essay but has a graph\-disjoint support subtree\.The resulting AAE2 sources contain 2\.59 Premises on average in development and 2\.57 in test; both medians are 2 and both maxima are 7\. Development and test use disjoint essays\. To comply with the source archive’s redistribution terms, we do not redistribute the full derived text\.

### A\.3Automatic Construction Audit

For the automatic checks reported in Table[A\.2](https://arxiv.org/html/2608.18820#A1.T2), each string is normalized with Unicode NFKC and case folding; Unicode alphanumeric runs excluding underscores are then joined with single spaces, so punctuation is discarded\.

Table A\.2:Automatic audit of the three derived pairwise tasks\. “Clust\.” is the number of test clusters; “Split ov\.” counts development–test cluster overlap; “Dup\.” counts duplicate complete examples; “Ident\.” counts within\-example identical candidates; and “Verb\.” counts examples in which the normalized gold\-candidate text occurs as a substring of the normalized source\. A complete example includes its source–target context and both ordered candidates\.The audit finds no duplicate complete examples, identical within\-example candidates, or development–test cluster overlap\. For AAE2, revalidation of all 550 development and test examples against the released relation graphs additionally finds no path from a selected source Premise to its distractor and no overlap with the distractor’s support subtree\.

One iDebate test example contains the normalized gold\-claim string as a substring of the normalized source\. We retain the test set rather than replacing the item after observing results\. Excluding it changes each reported test accuracy, including PWAL’s ten\-seed mean accuracy, by at most0\.170\.17percentage points and does not alter any comparison\.

### A\.4AI\-Assisted Validity Audit with Author Verification

We additionally audited a fixed sample of 50 CDED, 50 iDebate, and 100 AAE2 test examples\. Within each dataset, seed 2026 fixes stratum quotas proportional to their frequencies in the fixed test set and a deterministic within\-stratum order, with distinct topic, debate, or essay clusters preferred before repeats\. CDED strata combine evidence type and gold position; iDebate strata use gold position; and AAE2 strata combine stance, gold position, and whether the distractor has an incoming support subtree\. OpenAI GPT\-5\.6\-SOL with maximum reasoning effort\([OpenAI 2026](https://arxiv.org/html/2608.18820#bib.bib26)\)produced a first\-pass semantic assessment from the displayed source or context and the two candidates\. One author then reviewed all 200 items and confirmed the first\-pass labels\. This is an author verification of an AI\-assisted audit, not an independent multi\-annotator study, so we do not report inter\-annotator agreement\. The first pass was strictly blinded for 197 items; the gold/distractor role was inadvertently exposed for one item per dataset\. Restricting the summary to the 197 strictly blinded items gives gold\-or\-both counts of47/4947/49,49/4949/49, and93/9993/99, respectively\. Table[A\.3](https://arxiv.org/html/2608.18820#A1.T3)reports the author\-confirmed outcomes for the complete 200\-item sample\.

##### Audit instruction\.

The complete task\-aware instruction used for the first pass was:

> You are conducting a validity audit of derived pairwise examples\. For each item, use only the displayed task context or source and Candidates A and B\. Do not consult gold labels, adjudication keys, model predictions, or solver outputs, and do not replace examples after review\. For CDED, determine whether each candidate provides evidence supporting the displayed claim\. For iDebate and AAE2, determine whether the displayed source supports each candidate claim\. Assignsupported\_candidateas exactly one of: A— only Candidate A is supported; B— only Candidate B is supported; both— both are plausibly supported; neither— neither is supported; unclear— the displayed text does not permit a clear judgment\. Also assign confidence ashigh,medium, orlow, and give one concise sentence explaining the judgment\. For AAE2 only, assignopposite\_stance\_contrastas exactly one of: meaningful\_contrast; topic\_related\_not\_contrast; unrelated; unclear\.

Table A\.3:Author\-confirmed outcomes of the AI\-assisted validity audit\. “Gold or both” counts examples for which the gold candidate alone or both candidates were plausible\. No item was unclear\.For the AAE2 contrast check, 92 of 100 distractors were judged meaningful opposite\-stance contrasts; the other 8 were topic\-related but did not form a meaningful contrast\. These audit labels were not used to modify the test sets or select any method setting\.

## Appendix BEvaluation Protocol and Development Decisions

### B\.1Evaluation Settings and Compute Environment

Experiments were run on 64\-bit Windows with an Intel Core i5\-13600KF CPU, 32 GB RAM, and an NVIDIA GeForce RTX 4090 GPU with 24 GB memory, using Python 3\.8\.18, PyTorch 1\.13\.1 with CUDA 11\.7, Transformers 4\.34\.0, Sentence\-Transformers 2\.2\.2, and PySAT 0\.1\.8\.dev9\. The common pipeline uses Structured\-BART for AMR parsing\([Zhou et al\. 2021](https://arxiv.org/html/2608.18820#bib.bib39);[Lee et al\. 2022](https://arxiv.org/html/2608.18820#bib.bib21)\), mDeBERTa\-v3 for NLI\-based atom links\([He, Gao, and Chen 2023](https://arxiv.org/html/2608.18820#bib.bib12);[Laurer 2024](https://arxiv.org/html/2608.18820#bib.bib20)\), and RC2 in PySAT for Partial MaxSAT inference\([Ignatiev, Morgado, and Marques\-Silva 2018](https://arxiv.org/html/2608.18820#bib.bib16)\)\.FH\-HardSATadditionally usesBAAI/bge\-small\-en\-v1\.5for cosine similarity\([Xiao et al\. 2024](https://arxiv.org/html/2608.18820#bib.bib36)\)\. For method selection, development labels are used only forFH\-HardSATthreshold selection\. Separately, development labels are used to evaluate the diagnostic resistance\-component sweep in Section[C\.3](https://arxiv.org/html/2608.18820#A3.SS3)\. No test label is used to choose the scoring rule, sampling budget, seed set, ablation, or reference policy\.

For an evaluation set ofNNexamples, letNwin,Nerr,NtieN\_\{\\mathrm\{win\}\},N\_\{\\mathrm\{err\}\},N\_\{\\mathrm\{tie\}\}denote correct unique decisions, errors, and valid score ties, withN=Nwin\+Nerr\+NtieN=N\_\{\\mathrm\{win\}\}\+N\_\{\\mathrm\{err\}\}\+N\_\{\\mathrm\{tie\}\}\. The reported metrics are

Accuracy\\displaystyle\\operatorname\{Accuracy\}=NwinN,\\displaystyle=\\frac\{N\_\{\\mathrm\{win\}\}\}\{N\},TieRate\\displaystyle\\operatorname\{TieRate\}=NtieN,\\displaystyle=\\frac\{N\_\{\\mathrm\{tie\}\}\}\{N\},EAcc\\displaystyle\\operatorname\{EAcc\}=Nwin\+12​NtieN\.\\displaystyle=\\frac\{N\_\{\\mathrm\{win\}\}\+\\tfrac\{1\}\{2\}N\_\{\\mathrm\{tie\}\}\}\{N\}\.Any absolute difference of at mostτtie=10−12\\tau\_\{\\mathrm\{tie\}\}=10^\{\-12\}between the two candidate scores is treated as a valid tie\. Invalid outputs are a diagnostic subset ofNerrN\_\{\\mathrm\{err\}\}: they receive zero credit and are never relabeled as ties\.

### B\.2FH\-HardSATThreshold Selection

FH\-HardSATsearches its threshold grid on the corresponding development split and applies the selected pair once to the test split\. Table[B\.1](https://arxiv.org/html/2608.18820#A2.T1)reports the selected thresholds and held\-out test counts without repeating the main\-paper metrics\.

Table B\.1:FH\-HardSATdevelopment selection and held\-out test counts\.τm\\tau\_\{m\}is the BGE cosine\-similarity threshold andτc\\tau\_\{c\}the NLI contradiction\-confidence threshold \(in percent\)\. TestW/L/TW/L/Tgives correct unique decisions, errors, and valid ties, respectively;LLincludes unsuccessful evaluations\. The corresponding metrics appear in the main results\.

## Appendix CDecision Diagnostics and Components

### C\.1Top\-Link\-to\-PWAL Transitions

We classify each output as a correct unique decision, an incorrect unique decision, or a valid tie\.Top\-Linkis deterministic, whereas PWAL transitions are computed separately for each of the tenK=100K=100seeds before aggregation\. Table[C\.1](https://arxiv.org/html/2608.18820#A3.T1)reports PWAL EAcc over theTop\-Linkties and full\-test unique\-to\-unique repairs and damages\. A tied\-subset EAcc of50%50\\%is the uniform tie\-breaking reference, not a significance threshold\.

Table C\.1:Top\-Link\-to\-PWAL transition summary\. Tied\-subset EAcc is PWAL EAcc on the deterministicTop\-Linkties\. Repairs and damages are full\-test mean counts of unique\-to\-unique transitions from incorrect to correct and correct to incorrect, respectively\. Entries are ten\-seed means±\\pmsample standard deviations\.CDED has the highest tied\-subset EAcc \(57\.13%57\.13\\%\)\. Repairs exceed damages on every dataset, although the net difference is small onα\\alphaNLI, iDebate, and AAE2\.

### C\.2Score\-Component Error Signatures

For each incorrect unique PWAL decision, we identify which score components favor the selected candidate\. The tension component favors it when the gold candidate has higher normalized semantic tension; the witness component favors it when the selected candidate has a higher target\-clause witness ratio\. For this diagnostic component attribution only, component differences within10−910^\{\-9\}are treated as zero\. This diagnostic tolerance does not alter the candidate\-score tie ruleτtie=10−12\\tau\_\{\\mathrm\{tie\}\}=10^\{\-12\}\.

Table[C\.2](https://arxiv.org/html/2608.18820#A3.T2)reports the resulting score\-component categories for all five datasets\.

Table C\.2:Score\-component attribution of PWAL’s incorrect unique decisions atK=100K=100\. Wrong is the mean count of incorrect unique decisions; the remaining columns are mean percentages\. Entries are means±\\pmsample standard deviations over seeds 2026–2035\.These categories describe score\-component signatures, not linguistic causes\. Both components favor the incorrect selection in a majority of errors onα\\alphaNLI, CDED, iDebate, and AAE2; witness\-only attribution is the largest category on ARCT\.

### C\.3Resistance\-Component Sensitivity

To diagnose the relative contribution of the two terms in the fixed logical\-resistance score, we evaluate a coefficient sweep on development data only\. The reported score remains

ρ=Δ​TCmax−Rsat,\\rho=\\frac\{\\Delta T\}\{C\_\{\\max\}\}\-R\_\{\\mathrm\{sat\}\},whereΔ​T/Cmax\\Delta T/C\_\{\\max\}is normalized semantic tension andRsatR\_\{\\mathrm\{sat\}\}is the target\-clause witness ratio\. The diagnostic sweep defines

ρα=α​Δ​TCmax−Rsat\\rho\_\{\\alpha\}=\\alpha\\frac\{\\Delta T\}\{C\_\{\\max\}\}\-R\_\{\\mathrm\{sat\}\}and evaluates everyα∈\{0,0\.05,…,5\}\\alpha\\in\\\{0,0\.05,\\ldots,5\\\}\. This development\-only sweep does not tune the test score:ρα=ρ\\rho\_\{\\alpha\}=\\rhoatα=1\\alpha=1, and all reported test results useρ\\rho\. All other settings remain fixed:Top\-Linkuses its single highest\-confidence link configuration, while PWAL usesK=100K=100and seeds 2026–2035\.

Figure C\.1:Development\-only diagnostic of the logical\-resistance components underρα=α​Δ​T/Cmax−Rsat\\rho\_\{\\alpha\}=\\alpha\\Delta T/C\_\{\\max\}\-R\_\{\\mathrm\{sat\}\}\. Curves contain every point in the fixed gridα=0,0\.05,…,5\\alpha=0,0\.05,\\ldots,5\. PWAL curves are ten\-seed means and shaded bands show one sample standard deviation;Top\-Linkis deterministic\. Filled markers identify the reported scoreρα=ρ\\rho\_\{\\alpha\}=\\rhoatα=1\\alpha=1\.Figure[C\.1](https://arxiv.org/html/2608.18820#A3.F1)shows that, across the ten dataset–method curves, the development accuracy obtained withρ\\rhois0\.250\.25–4\.504\.50percentage points below the maximum observed on the grid\.

### C\.4Component Contrasts

The no\-link state permits an unmatched target atom to remain unlinked in a sampled world\. The negative guard allows a negative target literal to count as witnessed only when its polarity is supported by an exact link whose source atom is false or by an active contradiction link whose source atom is true; target inertia alone is insufficient\. Each ablation changes only the named component and keeps the scoring ruleρ\\rho,K=100K=100, seeds 2026–2035, formulae, atom inventories, exact links, NLI alternatives, and clause weights fixed\. The negative\-guard ablation reuses Full PWAL’s sampled worlds for every example–seed pair and recomputes only witness and resistance terms\. Removing no\-link changes the local outcome distribution, so it uses the same seed IDs but resamples under the modified distribution\. The main paper reports the point estimates; Table[E\.1](https://arxiv.org/html/2608.18820#A5.T1)gives paired cluster\-aware intervals\.

##### AAE2 stance diagnostic\.

For AAE2, PWAL EAcc is56\.41%56\.41\\%forForclaims and54\.29%54\.29\\%forAgainstclaims, averaged over seeds 2026–2035\. This diagnostic was not used to select any method setting\.

## Appendix DSampling, Exact/10510^\{5\}\-Capped Reference, and Runtime

### D\.1Sampling Stability

For eachK∈\{10,20,50,100,200\}K\\in\\\{10,20,50,100,200\\\}, PWAL is evaluated with seeds 2026–2035\. Within each seed, the smaller budgets are prefixes of the sameK=200K=200world stream\. Table[D\.1](https://arxiv.org/html/2608.18820#A4.T1)reports the corresponding accuracy, tie\-rate, and EAcc summaries together with the fixed exact/10510^\{5\}\-capped reference\.

Table D\.1:PWAL stability and exact/10510^\{5\}\-capped reference results\. Finite\-KKcells are ten\-seed mean percentages±\\pmsample standard deviations in percentage points; Ref\. is a fixed percentage\.AtK=100K=100, the across\-seed accuracy standard deviation is at most1\.121\.12percentage points\. IncreasingKKfrom 100 to 200 changes mean accuracy and mean tie rate by at most1\.101\.10and0\.680\.68percentage points, respectively\.

### D\.2Reference Coverage and Approximation

For candidateccwith world set𝒲c\\mathcal\{W\}\_\{c\}, letNcworld=\|𝒲c\|N\_\{c\}^\{\\mathrm\{world\}\}=\|\\mathcal\{W\}\_\{c\}\|\. The reference enumerates all worlds whenNcworld≤105N\_\{c\}^\{\\mathrm\{world\}\}\\leq 10^\{5\}and otherwise draws10510^\{5\}worlds uniformly without replacement using seed 2026\. A pair is fully exact only when both candidates are enumerated\. Table[D\.2](https://arxiv.org/html/2608.18820#A4.T2)reports the world\-space quantities that determine exact coverage; the corresponding reference outcomes are included in Table[D\.1](https://arxiv.org/html/2608.18820#A4.T1)\.

Table D\.2:Exact/10510^\{5\}\-capped reference coverage and world\-space scale\. World\-count summaries are over candidate sides before capping; reference outcomes are included in Table[D\.1](https://arxiv.org/html/2608.18820#A4.T1)and summarized in the main paper\. A capped pair has at least one candidate withNcworld\>105N\_\{c\}^\{\\mathrm\{world\}\}\>10^\{5\}; P95 denotes the 95th percentile\.For a dataset ofNNexamples, let𝒮=\{2026,…,2035\}\\mathcal\{S\}=\\\{2026,\\ldots,2035\\\}and let

μ¯i,c\(100\)=1\|𝒮\|​∑s∈𝒮μ^i,c\(100,s\)\\overline\{\\mu\}^\{\(100\)\}\_\{i,c\}=\\frac\{1\}\{\|\\mathcal\{S\}\|\}\\sum\_\{s\\in\\mathcal\{S\}\}\\widehat\{\\mu\}^\{\(100,s\)\}\_\{i,c\}be the ten\-seed meanK=100K=100score for exampleiiand candidatec∈\{A,B\}c\\in\\\{A,B\\\}; letμi,cref\\mu^\{\\mathrm\{ref\}\}\_\{i,c\}be its reference score\. Define the corresponding candidate\-score margins as

mi\(100\)=μ¯i,B\(100\)−μ¯i,A\(100\),miref=μi,Bref−μi,Aref\.m\_\{i\}^\{\(100\)\}=\\overline\{\\mu\}^\{\(100\)\}\_\{i,B\}\-\\overline\{\\mu\}^\{\(100\)\}\_\{i,A\},\\qquad m\_\{i\}^\{\\mathrm\{ref\}\}=\\mu^\{\\mathrm\{ref\}\}\_\{i,B\}\-\\mu^\{\\mathrm\{ref\}\}\_\{i,A\}\.The candidate\-score and margin mean absolute errors \(MAEs\) are

MAEscore\\displaystyle\\operatorname\{MAE\}\_\{\\mathrm\{score\}\}=12​N​∑i=1N∑c∈\{A,B\}\|μ¯i,c\(100\)−μi,cref\|,\\displaystyle=\\frac\{1\}\{2N\}\\sum\_\{i=1\}^\{N\}\\sum\_\{c\\in\\\{A,B\\\}\}\\left\|\\overline\{\\mu\}^\{\(100\)\}\_\{i,c\}\-\\mu^\{\\mathrm\{ref\}\}\_\{i,c\}\\right\|,MAEmargin\\displaystyle\\operatorname\{MAE\}\_\{\\mathrm\{margin\}\}=1N​∑i=1N\|mi\(100\)−miref\|\.\\displaystyle=\\frac\{1\}\{N\}\\sum\_\{i=1\}^\{N\}\\left\|m\_\{i\}^\{\(100\)\}\-m\_\{i\}^\{\\mathrm\{ref\}\}\\right\|\.Decision agreement is the percentage of examples for which the mean\-score and reference evaluations return the sameA/B/TieA/B/\\texttt\{Tie\}decision\. Tie\-status agreement is the percentage for which both evaluations are either tied or unique, irrespective of which candidate wins when both are unique\. Table[D\.3](https://arxiv.org/html/2608.18820#A4.T3)reports these two agreements together with the two errors and the per\-seed attribution of sampled incorrect unique decisions\.

Table D\.3:Reference diagnostics\. The first block compares decisions formed from ten\-seedK=100K=100mean scores with the exact/10510^\{5\}\-capped reference\. In panel \(a\), MAEs are in resistance\-score units and the agreement columns are percentages\. The second block compares everyK=100K=100seed separately with exact marginalization on fully exact pairs; entries are mean percentages±\\pmsample standard deviations over seeds 2026–2035\. Its final three columns partition sampled incorrect unique decisions into those that become correct, become a tie, or remain wrong\.Candidate\-score MAE is0\.00660\.0066–0\.00890\.0089, margin MAE is0\.00940\.0094–0\.01220\.0122, and mean\-score decision agreement is88\.51%88\.51\\%–99\.71%99\.71\\%\.

Within the fully exact subsets,78\.72%78\.72\\%–98\.90%98\.90\\%of sampled incorrect unique decisions remain wrong under exact marginalization;1\.10%1\.10\\%–10\.95%10\.95\\%become correct, and the remainder become exact ties\. For capped candidates, the reference remains a deterministic uniform10510^\{5\}\-world estimate rather than an exact expectation\.

### D\.3Runtime

Runtime isolates logical scoring on the same fixed set of 20 fully enumerable test pairs per dataset for every configuration\. The pairs are selected once by a fixed label\-independent ranking of sample IDs\. Each per\-example value is the median of three timed runs after one warm\-up; finite\-KKconfigurations use seed 2026\. Timing begins from prepared logical states and excludes parsing, translation, NLI, and cache construction\.

Table D\.4:Controlled logical\-scoring runtime on 20 fully enumerable pairs per dataset \(ms/example\)\. P95 denotes the 95th percentile\.Table[D\.4](https://arxiv.org/html/2608.18820#A4.T4)shows that meanK=100K=100runtime is94\.0494\.04–142\.47142\.47ms per example, compared with1\.101\.10–1\.681\.68ms forTop\-Link\.K=200K=200approximately doubles theK=100K=100runtime, while exact enumeration requires526\.31526\.31–14,764\.9114\{,\}764\.91ms on the same pairs\.

## Appendix EPaired and Clustered Statistical Inference

Table E\.1:Paired two\-way bootstrap contrasts in percentage points\. Brackets are pointwise two\-sided 95% bootstrap percentile intervals;†\\daggermarks an interval that excludes zero\.The contrasts in Table[E\.1](https://arxiv.org/html/2608.18820#A5.T1)use the following bootstrap protocol\. Each reported point estimate averages per\-example utility over the ten completeK=100K=100seed runs\. Each of 10,000 bootstrap replicates resamples complete task\-specific clusters and whole seed runs with replacement while preserving method pairing\. Cluster units are example forα\\alphaNLI and ARCT, topic for CDED, debate for iDebate, and essay for AAE2\. Reported intervals are pointwise two\-sided 95% bootstrap percentile intervals; the ten seeds are not treated as ten independent test sets, and an interval containing zero is treated as statistically inconclusive\.

Strict\-accuracy utility is one only for a correct unique decision; EAcc utility is one for a correct unique decision and one half for a valid score tie; tie utility is one only for a valid score tie\. For accuracy and EAcc, a positive main\-method contrast favors PWAL and a positive component contrast favors Full\. Tie reduction reverses the subtraction order, so a positive value means fewer ties for PWAL or Full\.

PWAL’s strict\-accuracy interval relative toTop\-Linkexcludes zero onα\\alphaNLI, ARCT, and CDED but includes zero on iDebate and AAE2\. For component contrasts, the no\-link accuracy interval excludes zero onα\\alphaNLI, ARCT, and CDED, while the negative\-guard interval excludes zero on ARCT and CDED\.

## Appendix FTranslator Specification

### F\.1AMR\-to\-Logic Translation

This section specifies the deterministic AMR\-to\-logic translation shared by every evaluated symbolic decoder\. We use AMR\([Banarescu et al\. 2013](https://arxiv.org/html/2608.18820#bib.bib2)\), PropBank for numbered semantic roles\([Kingsbury and Palmer 2002](https://arxiv.org/html/2608.18820#bib.bib17)\), and the open\-source Penman library for PENMAN decoding\([Goodman 2020](https://arxiv.org/html/2608.18820#bib.bib10)\)\. Given one statementxx, the fixed parser–translator pipeline either returns a Boolean formula, its active atoms, and their base verbalizations, or fails without emitting a translator frame\. A statement is one translator input unit and may contain multiple orthographic sentences; parsermulti\-sentencebranches are compiled conjunctively\.

###### Definition F\.1\(AMR Translator Output\)\.

Fix an AMR parser configurationϑ\\vartheta, and let𝒯AMRϑ\\mathcal\{T\}\_\{\\mathrm\{AMR\}\}^\{\\vartheta\}be the resulting partial translator\. The parser and decoder first convertxxinto a normalized AMR graph, with supported inverse roles mapped to their base\-role directions\. For every successfully translated statement, let\(ax,1,…,ax,nx\)\(a\_\{x,1\},\\ldots,a\_\{x,n\_\{x\}\}\)be the deterministic active\-atom order\. The translator returns

𝔉x=⟨Φx,\(⟨id⁡\(ax,i\),θx​\(ax,i\),vx​\(ax,i\)⟩\)i=1nx⟩\.\\mathfrak\{F\}\_\{x\}=\\left\\langle\\Phi\_\{x\},\\left\(\\left\\langle\\operatorname\{id\}\(a\_\{x,i\}\),\\theta\_\{x\}\(a\_\{x,i\}\),v\_\{x\}\(a\_\{x,i\}\)\\right\\rangle\\right\)\_\{i=1\}^\{n\_\{x\}\}\\right\\rangle\.Let

𝒜x=\{ax,1,…,ax,nx\}\\mathcal\{A\}\_\{x\}=\\\{a\_\{x,1\},\\ldots,a\_\{x,n\_\{x\}\}\\\}denote the corresponding active atom set\. HereΦx\\Phi\_\{x\}is the emitted formula abstract syntax tree \(AST\),θx​\(a\)\\theta\_\{x\}\(a\)is the structured atom expression, andvx​\(a\)v\_\{x\}\(a\)is its nonempty unsigned base verbalization\. The translator does not add a terminal sentence delimiter, and negation is represented inΦx\\Phi\_\{x\}, not inserted intovx​\(a\)v\_\{x\}\(a\)\. The downstream surface adapter strips surrounding whitespace fromvx​\(a\)v\_\{x\}\(a\)and appends the string\., yielding the main\-paper surface𝒱x​\(a\)\\mathcal\{V\}\_\{x\}\(a\)\. This formatting step is outside𝒯AMRϑ\\mathcal\{T\}\_\{\\mathrm\{AMR\}\}^\{\\vartheta\}\. The solver\-facing representation used in the main paper is therefore

𝖱𝖾𝗉⁡\(x\)=⟨𝒜x,Φx,𝒱x⟩\.\\mathsf\{Rep\}\(x\)=\\langle\\mathcal\{A\}\_\{x\},\\Phi\_\{x\},\\mathcal\{V\}\_\{x\}\\rangle\.If parsing, AMR decoding, compilation, or output validation fails,𝒯AMRϑ​\(x\)\\mathcal\{T\}\_\{\\mathrm\{AMR\}\}^\{\\vartheta\}\(x\)is undefined; no fallback output is substituted\.

###### Example F\.1\(Running translator input\)\.

Forx=A careful student reads a bookx=\\textit\{A careful student reads a book\}, suppose the fixed parser returns

```
(r / read-01
   :ARG0 (s / student
      :mod (c / careful))
   :ARG1 (b / book))
```

The graph determines the record partition, atom inventory, and Boolean formula\. Numbered\-role verbalizations additionally use the pinned PropBank role index\. The symbolsaia\_\{i\}used below are expository labels and need not match emittedxiiidentifiers or their order\.

### F\.2Records, Atoms, and Verbalizations

###### Definition F\.2\(Normalized AMR Records and Endpoint Descriptors\)\.

Write the normalized graph for statementxxas

Gx=\(𝒩x,ℰxN,ℰxL,cx,tx\),G\_\{x\}=\(\\mathcal\{N\}\_\{x\},\\mathcal\{E\}\_\{x\}^\{\\mathrm\{N\}\},\\mathcal\{E\}\_\{x\}^\{\\mathrm\{L\}\},c\_\{x\},t\_\{x\}\),where𝒩x\\mathcal\{N\}\_\{x\}is the node set,ℰxN\\mathcal\{E\}\_\{x\}^\{\\mathrm\{N\}\}contains node\-valued role records,ℰxL\\mathcal\{E\}\_\{x\}^\{\\mathrm\{L\}\}contains literal\-valued attribute records,cxc\_\{x\}maps nodes to concepts, andtxt\_\{x\}is the parser top\. Every role or attribute occurrence receives a deterministic within\-graph record identifier; the compiler does not reconstruct occurrences from surface text\. Letℰx=ℰxN​⨄ℰxL\\mathcal\{E\}\_\{x\}=\\mathcal\{E\}\_\{x\}^\{\\mathrm\{N\}\}\\biguplus\\mathcal\{E\}\_\{x\}^\{\\mathrm\{L\}\}, where⨄\\biguplusdenotes disjoint union\. Normalization deterministically partitions the records as

ℰx=ℰxsem​⨄ℰxstr​⨄ℰxmeta\.\\mathcal\{E\}\_\{x\}=\\mathcal\{E\}\_\{x\}^\{\\mathrm\{sem\}\}\\biguplus\\mathcal\{E\}\_\{x\}^\{\\mathrm\{str\}\}\\biguplus\\mathcal\{E\}\_\{x\}^\{\\mathrm\{meta\}\}\.Semantic records can produce dyadic records or contribute to triples\. Structural records determine Boolean structure\. Metadata records may refine endpoint identity or lexical realization; metadata used by neither remains construction\-only\. Table[F\.1](https://arxiv.org/html/2608.18820#A6.T1)gives the principal cases\. List indices and descriptor subtrees are metadata under the same partition\. The only metadata role that may emit an active atom is the special active:modecase; a mode attached to a structural connective remains construction metadata\. Metadata may affect a descriptor, but it does not itself create a separate proposition\.

Endpoint identity includes its concept, normalized name, and descriptor metadata\. Define

δx​\(u\)=\{δxN​\(u\),u∈𝒩x,δxL​\(u\),u​is a literal,\\delta\_\{x\}\(u\)=\\begin\{cases\}\\delta\_\{x\}^\{\\mathrm\{N\}\}\(u\),&u\\in\\mathcal\{N\}\_\{x\},\\\\ \\delta\_\{x\}^\{\\mathrm\{L\}\}\(u\),&u\\text\{ is a literal\},\\end\{cases\}where

δxN​\(u\)\\displaystyle\\delta\_\{x\}^\{\\mathrm\{N\}\}\(u\)=NodeDesc⁡\(cx​\(u\),Namex⁡\(u\),mx​\(u\)\),\\displaystyle=\\operatorname\{NodeDesc\}\\\!\\left\(c\_\{x\}\(u\),\\operatorname\{Name\}\_\{x\}\(u\),m\_\{x\}\(u\)\\right\),δxL​\(u\)\\displaystyle\\delta\_\{x\}^\{\\mathrm\{L\}\}\(u\)=LitDesc⁡\(raw⁡\(u\),val⁡\(u\),type⁡\(u\)\)\.\\displaystyle=\\operatorname\{LitDesc\}\\\!\\left\(\\operatorname\{raw\}\(u\),\\operatorname\{val\}\(u\),\\operatorname\{type\}\(u\)\\right\)\.HereNamex⁡\(u\)\\operatorname\{Name\}\_\{x\}\(u\)is the normalized name, if present\. In the descriptor foruu, the direct metadata listmx​\(u\)m\_\{x\}\(u\)excludes:name,name\-part, and:wikirecords; node\-valued metadata targets are serialized recursively\. The normalized name is already represented byNamex⁡\(u\)\\operatorname\{Name\}\_\{x\}\(u\), while direct:wikimetadata is retained only for construction\. For literals, the raw PENMAN token, its evaluated value, and its recovered type are retained\. Parser node and record identifiers are source\-record identifiers and are not inserted intoδx\\delta\_\{x\}\.

Table F\.1:Principal structural and metadata cases\. Records not assigned to a structural or metadata category are semantic records\.###### Example F\.2\(Record partition and endpoint identity\)\.

In Example[F\.1](https://arxiv.org/html/2608.18820#Thmexample1a), the role occurrences:ARG0\(r,s\),:ARG1\(r,b\), and:mod\(s,c\)belong toℰxsem\\mathcal\{E\}\_\{x\}^\{\\mathrm\{sem\}\}\. There is no connective or scope record, soℰxstr=∅\\mathcal\{E\}\_\{x\}^\{\\mathrm\{str\}\}=\\varnothing\. If the book node additionally contained:quant 1, that occurrence would belong toℰxmeta\\mathcal\{E\}\_\{x\}^\{\\mathrm\{meta\}\}: it would refineδx​\(b\)\\delta\_\{x\}\(b\)without becoming an independent proposition\.

#### Active Atoms

The concrete AMR role labelsr,ra,rbr,r\_\{a\},r\_\{b\}below instantiate the main\-paper role parametersκ,κa,κb\\kappa,\\kappa\_\{a\},\\kappa\_\{b\}, respectively; the predicate occurrenceppcorresponds toeein the main paper’s compact atom notation\.

###### Definition F\.3\(Role\-Aware Dyads and Same\-Event Triples\)\.

For a semantic record\(p,:r,u\)\(p,\\texttt\{:\}r,u\), whereuumay be a node or literal, the compiler first creates the role\-aware dyadic record

Dyar⁡\(δx​\(p\),δx​\(u\)\)\.\\operatorname\{Dya\}\_\{r\}\\bigl\(\\delta\_\{x\}\(p\),\\delta\_\{x\}\(u\)\\bigr\)\.Its payload records the role, both typed descriptors, and whether the endpoints are the same node, distinct nodes, or a node and a literal\. The originating record identifier is stored separately as provenance\.

Two node\-valued role records can be compressed into one triple only when they share the same predicate occurrencepp\. Let

𝒞comp=\{\\displaystyle\\mathcal\{C\}\_\{\\mathrm\{comp\}\}=\\\{ARG0,…,ARG4,\\displaystyle\\texttt\{ARG0\},\\ldots,\\texttt\{ARG4\},accompanier,beneficiary,cause,\\displaystyle\\texttt\{accompanier\},\\texttt\{beneficiary\},\\texttt\{cause\},destination,direction,duration,\\displaystyle\\texttt\{destination\},\\texttt\{direction\},\\texttt\{duration\},extent,instrument,location,\\displaystyle\\texttt\{extent\},\\texttt\{instrument\},\\texttt\{location\},manner,medium,path,\\displaystyle\\texttt\{manner\},\\texttt\{medium\},\\texttt\{path\},purpose,source,time,topic\}\.\\displaystyle\\texttt\{purpose\},\\texttt\{source\},\\texttt\{time\},\\texttt\{topic\}\\\}\.Among the core roles present onpp, the compiler chooses the first available anchor in the fixed orderARG0,…,ARG4\\texttt\{ARG0\},\\ldots,\\texttt\{ARG4\}\. If\(p,:ra,u\)\(p,\\texttt\{:\}r\_\{a\},u\)is the anchor edge and\(p,:rb,v\)\(p,\\texttt\{:\}r\_\{b\},v\)is another edge withrb∈𝒞compr\_\{b\}\\in\\mathcal\{C\}\_\{\\mathrm\{comp\}\}, they produce

Trira,rb⁡\(δx​\(u\),δx​\(p\),δx​\(v\)\)\.\\operatorname\{Tri\}\_\{r\_\{a\},r\_\{b\}\}\\bigl\(\\delta\_\{x\}\(u\),\\delta\_\{x\}\(p\),\\delta\_\{x\}\(v\)\\bigr\)\.This triple records that, in one occurrence of predicatepp, endpointsuuandvvfill rolesrar\_\{a\}andrbr\_\{b\}\. WhenARG0is absent, a later core role can anchor the event; in particular,ARG1\+ARG2is legal\. Cross\-event paths are never merged\.

For each non\-anchor rolerb∈𝒞compr\_\{b\}\\in\\mathcal\{C\}\_\{\\mathrm\{comp\}\}, the compiler forms a separate triple with the selected anchor role\. An event withARG0,ARG1, andARG2yieldsTriARG0,ARG1\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG1\}\}andTriARG0,ARG2\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG2\}\}; whenARG0is available, the compiler does not additionally form anARG1\+ARG2triple\. Component dyads remain in the internal record inventory, but once absorbed they are not active formula atoms\. If exactly one endpoint of a candidate triple is a structural connective, the compiler recursively projects that endpoint to its leaf branches, creates one triple per leaf, and preserves the nested connective topology in the formula\. If the two endpoints are independently coordinated, the compiler forms no Cartesian product; the corresponding relations remain projected dyads\.

Each distinct unconsumed semantic record whose source is not a structural connective and whose target is not a structural connective produces one active dyad\. If its target is a structural connective, the relation is projected to one dyad per leaf branch and the formula preserves the connective topology\. Duplicate semantic occurrences are represented once, with their record identifiers retained together as internal provenance\. A relation whose source is a connective is represented by one opaque atom rather than being distributed over its branches\. A unary carrier is retained only when a concept would otherwise have no active proposition or a negative node requires a nonempty local scope\.

Let𝒟xrec\\mathcal\{D\}\_\{x\}^\{\\mathrm\{rec\}\}be the dyadic\-record inventory, let𝒞x⊆𝒟xrec\\mathcal\{C\}\_\{x\}\\subseteq\\mathcal\{D\}\_\{x\}^\{\\mathrm\{rec\}\}contain the component dyads consumed by successful same\-event composition, and letatomD⁡\(d\)\\operatorname\{atom\}\_\{\\mathrm\{D\}\}\(d\)denote the dyadic proposition represented by recorddd\. The provisional active inventory is

𝒜~x=𝒜~xU​⨄𝒜~xD​⨄𝒜~xT​⨄𝒜~xO,\\widetilde\{\\mathcal\{A\}\}\_\{x\}=\\widetilde\{\\mathcal\{A\}\}\_\{x\}^\{\\mathrm\{U\}\}\\biguplus\\widetilde\{\\mathcal\{A\}\}\_\{x\}^\{\\mathrm\{D\}\}\\biguplus\\widetilde\{\\mathcal\{A\}\}\_\{x\}^\{\\mathrm\{T\}\}\\biguplus\\widetilde\{\\mathcal\{A\}\}\_\{x\}^\{\\mathrm\{O\}\},where the four components contain unary carriers, active unconsumed dyads, same\-event triples, and opaque atoms\. The active dyads may also include the special:modecase described above\. Consumed dyads satisfy

\{atomD⁡\(d\):d∈𝒞x\}∩𝒜~x=∅\.\\\{\\operatorname\{atom\}\_\{\\mathrm\{D\}\}\(d\):d\\in\\mathcal\{C\}\_\{x\}\\\}\\cap\\widetilde\{\\mathcal\{A\}\}\_\{x\}=\\varnothing\.They remain internal provenance records but cannot also be scored as active atoms\.

###### Example F\.3\(Triple composition and a residual dyad\)\.

For the graph in Example[F\.1](https://arxiv.org/html/2608.18820#Thmexample1a), the same\-event records:ARG0\(r,s\)and:ARG1\(r,b\)compose into

a1=TriARG0,ARG1⁡\(student,read\-01,book\)\.a\_\{1\}=\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG1\}\}\(\\textit\{student\},\\textit\{read\-01\},\\textit\{book\}\)\.For readability, examples abbreviate typed endpoint descriptors by their lexical heads; the compiler retains the fullδx\\delta\_\{x\}values\. The modifier is not part of the event\-role pair and remains

a2=Dyamod⁡\(student,careful\)\.a\_\{2\}=\\operatorname\{Dya\}\_\{\\mathrm\{mod\}\}\(\\textit\{student\},\\textit\{careful\}\)\.Thus𝒜~x=\{a1,a2\}\\widetilde\{\\mathcal\{A\}\}\_\{x\}=\\\{a\_\{1\},a\_\{2\}\\\}\. TheARG0andARG1dyads remain provenance records but are not additional active atoms\.

#### Atom Identity, Provenance, and Verbalization

###### Definition F\.4\(Atom Identity, Provenance, and Verbalization\)\.

For every provisional atomaa,θx​\(a\)\\theta\_\{x\}\(a\)is its structured representation: atom kind, role or role pair, ordered endpoint descriptors, and, where applicable, a coreference flag\. Its canonical key is

keyx⁡\(a\)=Canon⁡\(θx​\(a\)\),\\operatorname\{key\}\_\{x\}\(a\)=\\operatorname\{Canon\}\\\!\\left\(\\theta\_\{x\}\(a\)\\right\),whereCanon\\operatorname\{Canon\}is a deterministic serialization independent of parser variable names\. In contrast,provx⁡\(a\)⊆ℰx\\operatorname\{prov\}\_\{x\}\(a\)\\subseteq\\mathcal\{E\}\_\{x\}records the graph records used to constructaa, andownerx⁡\(a\)∈𝒩x\\operatorname\{owner\}\_\{x\}\(a\)\\in\\mathcal\{N\}\_\{x\}is the graph node whose local formula body contains the leaf foraa\. Metadata may affectθx​\(a\)\\theta\_\{x\}\(a\)orvx​\(a\)v\_\{x\}\(a\)without appearing inprovx⁡\(a\)\\operatorname\{prov\}\_\{x\}\(a\); unary carriers may have empty provenance\. These fields are compiler\-internal and are distinct from the emitted verbalizationvx​\(a\)v\_\{x\}\(a\)\.

For a dyadDyar⁡\(c,d\)\\operatorname\{Dya\}\_\{r\}\(c,d\)and a tripleTrira,rb⁡\(c,p,d\)\\operatorname\{Tri\}\_\{r\_\{a\},r\_\{b\}\}\(c,p,d\), letC=ℓ⁡\(c\)C=\\ell\(c\),P=ℓ⁡\(p\)P=\\ell\(p\), andD=ℓ⁡\(d\)D=\\ell\(d\)\. The deterministic unsigned lexical formℓ\\ellremoves a predicate\-sense suffix and realizes names, quantities, and descriptor metadata from the AMR payload; it never consults the original sentence\. For an endpoint descriptorzzand numbered rolerr, the resolverχ⁡\(z,r\)\\chi\(z,r\)consults the predicate\-sense entry stored inzzand returns a semantic relation class from the pinned PropBank roleset, or⊥\\botwhen the roleset or role is unavailable or unresolved\. Non\-numbered roles are realized directly from their AMR role labels\. WritevDrv\_\{\\mathrm\{D\}\}^\{r\}andvTra,rbv\_\{\\mathrm\{T\}\}^\{r\_\{a\},r\_\{b\}\}for the base verbalizations of the corresponding dyad and triple\. SubscriptsD\\mathrm\{D\}andT\\mathrm\{T\}denote dyadic and triple forms, respectively\. Let𝖫𝖾𝗑D\\mathsf\{Lex\}^\{\\mathrm\{D\}\}and𝖫𝖾𝗑T\\mathsf\{Lex\}^\{\\mathrm\{T\}\}denote the fixed dyadic and triple realization maps specified below\. Then

relD\\displaystyle\\operatorname\{rel\}\_\{\\mathrm\{D\}\}=χ⁡\(c,r\),\\displaystyle=\\chi\(c,r\),relT\\displaystyle\\operatorname\{rel\}\_\{\\mathrm\{T\}\}=χ⁡\(p,rb\),\\displaystyle=\\chi\(p,r\_\{b\}\),sigD\\displaystyle\\operatorname\{sig\}\_\{\\mathrm\{D\}\}=\(r,relD\),\\displaystyle=\(r,\\operatorname\{rel\}\_\{\\mathrm\{D\}\}\),sigT\\displaystyle\\operatorname\{sig\}\_\{\\mathrm\{T\}\}=\(ra,rb,relT\),\\displaystyle=\(r\_\{a\},r\_\{b\},\\operatorname\{rel\}\_\{\\mathrm\{T\}\}\),fDr​\(c,d\)\\displaystyle f\_\{\\mathrm\{D\}\}^\{r\}\(c,d\)=\{norm⁡\(D​C\),r=ARG0,norm⁡\(C​D\),otherwise,\\displaystyle=\\begin\{cases\}\\operatorname\{norm\}\(D\\ C\),&r=\\texttt\{ARG0\},\\\\ \\operatorname\{norm\}\(C\\ D\),&\\text\{otherwise\},\\end\{cases\}fT​\(c,p,d\)\\displaystyle f\_\{\\mathrm\{T\}\}\(c,p,d\)=norm⁡\(C​P​D\),\\displaystyle=\\operatorname\{norm\}\(C\\ P\\ D\),vDr​\(c,d\)\\displaystyle v\_\{\\mathrm\{D\}\}^\{r\}\(c,d\)=𝖫𝖾𝗑sigDD​\(C,D\),\\displaystyle=\\mathsf\{Lex\}^\{\\mathrm\{D\}\}\_\{\\operatorname\{sig\}\_\{\\mathrm\{D\}\}\}\(C,D\),vTra,rb​\(c,p,d\)\\displaystyle v\_\{\\mathrm\{T\}\}^\{r\_\{a\},r\_\{b\}\}\(c,p,d\)=𝖫𝖾𝗑sigTT​\(C,P,D\)\.\\displaystyle=\\mathsf\{Lex\}^\{\\mathrm\{T\}\}\_\{\\operatorname\{sig\}\_\{\\mathrm\{T\}\}\}\(C,P,D\)\.Herenorm\\operatorname\{norm\}joins nonempty lexical fields with single spaces\. If the relevant resolver output is⊥\\bot, or a supported join has no resolved relation template,𝖫𝖾𝗑D\\mathsf\{Lex\}^\{\\mathrm\{D\}\}returns the ordered fallbackfDrf\_\{\\mathrm\{D\}\}^\{r\}, and𝖫𝖾𝗑T\\mathsf\{Lex\}^\{\\mathrm\{T\}\}returnsfTf\_\{\\mathrm\{T\}\}\. An opaque atom uses the dyadic template for its retained role\. For a unary carrier with conceptcc, lexical formC=ℓ⁡\(c\)C=\\ell\(c\), and optional quantityν\\nu, define

𝖫𝖾𝗑U​\(C,c,ν\)=\{C​occurs,c​is sense\-tagged,C​exist,ν​is present and​ν≠1,C​exists,otherwise\.\\mathsf\{Lex\}^\{\\mathrm\{U\}\}\(C;c,\\nu\)=\\begin\{cases\}C\\ \\textit\{occurs\},&c\\text\{ is sense\-tagged\},\\\\ C\\ \\textit\{exist\},&\\nu\\text\{ is present and \}\\nu\\neq 1,\\\\ C\\ \\textit\{exists\},&\\text\{otherwise\}\.\\end\{cases\}
The selected template depends only on the active atom kind, ordered terms, role or role pair, and, for numbered roles, the specific predicate\-sense entry in PropBank\. Tables[F\.2](https://arxiv.org/html/2608.18820#A6.T2),[F\.3](https://arxiv.org/html/2608.18820#A6.T3), and[F\.4](https://arxiv.org/html/2608.18820#A6.T4)summarize the surface templates applied after role resolution\. The fixed renderer additionally applies the specified PropBank\-description refinements, property\-predicate cases, and rule\-based inflections\. These affect onlyvxv\_\{x\}, not structured atom identity or the Boolean formula\. A listed metadata or connective role does not itself activate a proposition; activation is fixed by the record partition and atom construction above\. In the tables,pp⁡\(⋅\)\\operatorname\{pp\}\(\\cdot\)is the fixed rule\-based past\-participle inflector\.

Surface realization leavesθx\\theta\_\{x\},keyx\\operatorname\{key\}\_\{x\},ownerx\\operatorname\{owner\}\_\{x\},provx\\operatorname\{prov\}\_\{x\}, and the formula abstract syntax tree unchanged\. Negation is carried byΦx\\Phi\_\{x\}and is never inserted into the verbalization\.

###### Example F\.4\(Atom identity and verbalization\)\.

For the atoms in Example[F\.3](https://arxiv.org/html/2608.18820#Thmexample3a), the structured representation ofa1a\_\{1\}retains the predicate sense, role pair, and endpoint descriptors, while its verbalization omits the sense suffix:

θx​\(a1\)\\displaystyle\\theta\_\{x\}\(a\_\{1\}\)=TriARG0,ARG1⁡\(student,read\-01,book\),\\displaystyle=\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG1\}\}\(\\textit\{student\},\\textit\{read\-01\},\\textit\{book\}\),keyx⁡\(a1\)\\displaystyle\\operatorname\{key\}\_\{x\}\(a\_\{1\}\)=Canon⁡\(θx​\(a1\)\),\\displaystyle=\\operatorname\{Canon\}\\\!\\left\(\\theta\_\{x\}\(a\_\{1\}\)\\right\),vx​\(a1\)\\displaystyle v\_\{x\}\(a\_\{1\}\)=“student read book”,\\displaystyle=\\textit\{\`\`student read book''\},vx​\(a2\)\\displaystyle v\_\{x\}\(a\_\{2\}\)=“careful student”\.\\displaystyle=\\textit\{\`\`careful student''\}\.Thus the structured expression preservesread\-01, whereas the verbalization usesread\. Formula construction yieldsΦx=a1∧a2\\Phi\_\{x\}=a\_\{1\}\\land a\_\{2\}\.

\(a\) PropBank function\-tag resolutionPropBank tagResolved relation classPAG,CAU,SRC,EXT,PRP,TMPagent, cause, source, extent, purpose, and time, respectivelyPPTrefine to agent, property, instrument, accompaniment, path, source, location, topic, extent, attribute, active theme, or state; otherwise patientGOLrefine to beneficiary, result, location, or instrument; otherwise goalLOCdistinguish path, source, and goal; otherwise locationDIRdistinguish patient, source, goal, path, location, and beneficiary; otherwise directionMNRrefine to instrument or accompaniment; otherwise mannerCOMdistinguish opponent and companionPRDpatient forARG1; result otherwiseunavailable, missing,VSP, or unrecognizedreturn⊥\\botand use the ordered fallback\(b\) Numbered\-role surface templatesResolved relation classv⁡\(Dyar⁡\(c,d\)\)v\(\\operatorname\{Dya\}\_\{r\}\(c,d\)\)agent; active themeD​CD\\ CpatientD​is​pp⁡\(C\)D\\ \\textit\{is\}\\ \\operatorname\{pp\}\(C\)goalC​is directed to​DC\\ \\textit\{is directed to\}\\ DlocationC​occurs at​DC\\ \\textit\{occurs at\}\\ DpathC​occurs along​DC\\ \\textit\{occurs along\}\\ DdirectionC​proceeds toward​DC\\ \\textit\{proceeds toward\}\\ DsourceC​originates from​DC\\ \\textit\{originates from\}\\ DinstrumentC​uses​DC\\ \\textit\{uses\}\\ DmannerC​occurs by​DC\\ \\textit\{occurs by\}\\ Dcompanion; accompanimentC​occurs with​DC\\ \\textit\{occurs with\}\\ DopponentC​occurs against​DC\\ \\textit\{occurs against\}\\ Dbeneficiary; purposeC​is for​DC\\ \\textit\{is for\}\\ DresultC​results in​DC\\ \\textit\{results in\}\\ DextentC​has extent​DC\\ \\textit\{has extent\}\\ DcauseC​is caused by​DC\\ \\textit\{is caused by\}\\ DtopicC​is about​DC\\ \\textit\{is about\}\\ DtimeC​occurs during​DC\\ \\textit\{occurs during\}\\ DpropertyD​is​CD\\ \\textit\{is\}\\ CstateD​is in state​CD\\ \\textit\{is in state\}\\ CattributeC​has attribute​DC\\ \\textit\{has attribute\}\\ DunresolvedfDrf\_\{\\mathrm\{D\}\}^\{r\}Table F\.2:PropBank\-numbered dyadic verbalization\. Panel \(a\) resolves PropBank function tags to relation classes; panel \(b\) maps those classes to surface templates\. HereCCis the predicate surface andDDis the argument surface\. Relation classes that share a row use the same template\.Table F\.3:Surface templates for non\-numbered dyads and unary carriers\. For:prep\-qq,qqis the role suffix with hyphens replaced by spaces\.Table F\.4:Surface templates for same\-event triple atoms\. Monospaced entries are AMR roles or joins; roman entries are PropBank\-resolved classes or fallbacks\. HereCC,PP, andDDare the anchor, predicate, and non\-anchor surfaces\. Explicit adjunct roles precede PropBank classes\. Slash\-separated prepositions map in order to the listed classes; no slash is emitted\.

### F\.3Formula Construction, Polarity, and Validation

###### Definition F\.5\(Recursive Formula Construction\)\.

For specification, let

𝖳𝗋𝖺𝗏x=\(ownerx,Chx,Opx,Condx,𝒬x0\)\\mathsf\{Trav\}\_\{x\}=\(\\operatorname\{owner\}\_\{x\},\\operatorname\{Ch\}\_\{x\},\\operatorname\{Op\}\_\{x\},\\operatorname\{Cond\}\_\{x\},\\mathcal\{Q\}\_\{x\}^\{0\}\)summarize the compiler’s formula traversal\. Hereownerx\\operatorname\{owner\}\_\{x\}assigns every provisional atom to one formula owner;Chx⁡\(v\)\\operatorname\{Ch\}\_\{x\}\(v\)is the ordered list of semantic children reached fromvvthrough normalized forward or inverse\-tree records;Opx⁡\(v\)\\operatorname\{Op\}\_\{x\}\(v\)contains ordered connective branches; andCondx⁡\(v\)\\operatorname\{Cond\}\_\{x\}\(v\)contains condition targets\. Condition and connective records are handled separately and are excluded from ordinary child traversal\. Metadata and other structural records are excluded from ordinary child traversal\. A semantic back\-edge to an already open node is also not traversed, because the corresponding relation is already represented by a dyad or triple\.

The primary roots𝒬x0\\mathcal\{Q\}\_\{x\}^\{0\}contain the parser top and any incoming\-free roots of disconnected graph components\. After compiling them, if a provisional atom is absent from the formula, its owner is added as an additional coverage root in𝒬xcov\\mathcal\{Q\}\_\{x\}^\{\\mathrm\{cov\}\}\. Coverage continues until every provisional atom is represented; failure to add a new leaf is an invalid translation\. Let

𝒬x=𝒬x0​⨄𝒬xcov\.\\mathcal\{Q\}\_\{x\}=\\mathcal\{Q\}\_\{x\}^\{0\}\\biguplus\\mathcal\{Q\}\_\{x\}^\{\\mathrm\{cov\}\}\.For a provisional atomaa, letid⁡\(a\)\\operatorname\{id\}\(a\)be its assigned identifier\. For a formulaφ\\varphi, letLeafIds⁡\(φ\)\\operatorname\{LeafIds\}\(\\varphi\)be the set of identifiers on its atom leaves\.

For nodevv, letLocalx⁡\(v\)\\operatorname\{Local\}\_\{x\}\(v\)be the conjunction of provisional atoms owned byvv, and define

H⁡\(v\)=⋀u∈Chx⁡\(v\)F⁡\(u\),B0​\(v\)=Localx⁡\(v\)∧H⁡\(v\)\.H\(v\)=\\bigwedge\_\{u\\in\\operatorname\{Ch\}\_\{x\}\(v\)\}F\(u\),\\qquad B\_\{0\}\(v\)=\\operatorname\{Local\}\_\{x\}\(v\)\\land H\(v\)\.We take⋀∅=⊤\\bigwedge\\varnothing=\\topand⋁∅=⊥\\bigvee\\varnothing=\\bot\. Let𝒞∧=\{and,multi\-sentence\}\\mathcal\{C\}\_\{\\land\}=\\\{\\texttt\{and\},\\texttt\{multi\-sentence\}\\\}\. For a connective node with ordered branch rootsuiu\_\{i\}, define

Connx⁡\(v\)=\{⋀iF⁡\(ui\),cx​\(v\)∈𝒞∧,⋁iF⁡\(ui\),cx​\(v\)=or\.\\operatorname\{Conn\}\_\{x\}\(v\)=\\begin\{cases\}\\bigwedge\_\{i\}F\(u\_\{i\}\),&c\_\{x\}\(v\)\\in\\mathcal\{C\}\_\{\\land\},\\\\ \\bigvee\_\{i\}F\(u\_\{i\}\),&c\_\{x\}\(v\)=\\texttt\{or\}\.\\end\{cases\}The targetsuiu\_\{i\}arise from:opii,:sntii, or a multi\-sentence:reledge\. The local body is

B⁡\(v\)=\{B0​\(v\)∧Connx⁡\(v\),Connx⁡\(v\)​is defined,B0​\(v\),otherwise\.B\(v\)=\\begin\{cases\}B\_\{0\}\(v\)\\land\\operatorname\{Conn\}\_\{x\}\(v\),&\\operatorname\{Conn\}\_\{x\}\(v\)\\text\{ is defined\},\\\\ B\_\{0\}\(v\),&\\text\{otherwise\}\.\\end\{cases\}Node polarity is applied first:

N\(v\)=\{¬B⁡\(v\),vhas:polarity \-,B⁡\(v\),otherwise,N\(v\)=\\begin\{cases\}\\lnot B\(v\),&v\\text\{ has \}\\texttt\{:polarity \-\},\\\\ B\(v\),&\\text\{otherwise\},\\end\{cases\}Conditions are then applied to the resulting local body\. IfCondx⁡\(v\)=\{q1,…,qk\}\\operatorname\{Cond\}\_\{x\}\(v\)=\\\{q\_\{1\},\\ldots,q\_\{k\}\\\}, define

F⁡\(v\)=\{\(⋀jF⁡\(qj\)\)→N⁡\(v\),Condx⁡\(v\)≠∅,N⁡\(v\),otherwise\.F\(v\)=\\begin\{cases\}\\left\(\\bigwedge\_\{j\}F\(q\_\{j\}\)\\right\)\\to N\(v\),&\\operatorname\{Cond\}\_\{x\}\(v\)\\neq\\varnothing,\\\\ N\(v\),&\\text\{otherwise\}\.\\end\{cases\}Thus polarity on a conditioned node negates its consequent, not the whole implication\. AMR reentrancy is not expanded a second time when it points to an already open node; the corresponding relation is already present in a dyad or triple\. If a condition target is a proper ancestor already open on the current traversal path, the compiler uses the conjunction of that target node’s locally owned atoms as a finite antecedent\. A self\-condition or an empty local antecedent is invalid\. A cycle formed entirely by structural connective or multi\-sentence branch edges is also invalid rather than repaired; a branch already open only through ordinary semantic reentrancy is not expanded again\.

The formula before participant\-local polarity projection is

Φx0=⋀q∈𝒬xF⁡\(q\)\.\\Phi\_\{x\}^\{0\}=\\bigwedge\_\{q\\in\\mathcal\{Q\}\_\{x\}\}F\(q\)\.Coverage\-root construction guarantees

LeafIds⁡\(Φx0\)=\{id⁡\(a\):a∈𝒜~x\}\.\\operatorname\{LeafIds\}\(\\Phi\_\{x\}^\{0\}\)=\\\{\\operatorname\{id\}\(a\):a\\in\\widetilde\{\\mathcal\{A\}\}\_\{x\}\\\}\.

###### Example F\.5\(Coordination and condition\)\.

Suppose the parser representsThe committee chooses tea, or both coffee and cakewith an outerorbranch whose second child is anand\. Letat,ac,aka\_\{t\},a\_\{c\},a\_\{k\}denote the three same\-event choice atoms\. Then Definition[F\.5](https://arxiv.org/html/2608.18820#Thmdefinition5a)gives

Φx=at∨\(ac∧ak\)\.\\Phi\_\{x\}=a\_\{t\}\\lor\(a\_\{c\}\\land a\_\{k\}\)\.Forgo\-01 :ARG0 child :condition rain\-01, letaga\_\{g\}be theARG0dyad for the going event andara\_\{r\}the unary carrier for the otherwise atomless condition node\. Since the condition forms the antecedent and the local body forms the consequent, the result isΦx=ar→ag\\Phi\_\{x\}=a\_\{r\}\\to a\_\{g\}\.

#### Polarity, Branch Isolation, and Validation

###### Definition F\.6\(Participant\-Local Polarity\)\.

Node polarity on an event or proposition is handled byN⁡\(v\)N\(v\)above\. An explicit negative participant requires a narrower operation: only relation atoms containing that participant are negated\. Here a participant endpoint is a triple subject or object, or the node\-valued target of a dyad; unary and opaque atoms are not projected by this rule\. Let

𝒫x=\{id⁡\(a\)\|a∈𝒜~xD∪𝒜~xT,a​contains an explicitly negativeparticipant endpoint\}\.\\mathcal\{P\}\_\{x\}=\\left\\\{\\operatorname\{id\}\(a\)\\ \\middle\|\\ \\begin\{array\}\[\]\{l\}a\\in\\widetilde\{\\mathcal\{A\}\}\_\{x\}^\{\\mathrm\{D\}\}\\cup\\widetilde\{\\mathcal\{A\}\}\_\{x\}^\{\\mathrm\{T\}\},\\\\ a\\text\{ contains an explicitly negative\}\\\\ \\text\{participant endpoint\}\\end\{array\}\\right\\\}\.For parity bitb∈\{0,1\}b\\in\\\{0,1\\\}, defineΠ𝒫x\\Pi\_\{\\mathcal\{P\}\_\{x\}\}recursively by

Π𝒫x​\(a,b\)\\displaystyle\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\(a;b\)=\{¬a,id⁡\(a\)∈𝒫x​and​b=0,a,otherwise,\\displaystyle=\\begin\{cases\}\\lnot a,&\\operatorname\{id\}\(a\)\\in\\mathcal\{P\}\_\{x\}\\text\{ and \}b=0,\\\\ a,&\\text\{otherwise\},\\end\{cases\}Π𝒫x​\(¬φ,b\)\\displaystyle\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\(\\lnot\\varphi;b\)=¬Π𝒫x​\(φ,1−b\),\\displaystyle=\\lnot\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\(\\varphi;1\-b\),Π𝒫x\(○i=1kφi;b\)\\displaystyle\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\\left\(\\bigcirc\_\{i=1\}^\{k\}\\varphi\_\{i\};b\\right\)=○i=1kΠ𝒫x\(φi;b\),○∈\{∧,∨\},\\displaystyle=\\bigcirc\_\{i=1\}^\{k\}\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\(\\varphi\_\{i\};b\),\\qquad\\bigcirc\\in\\\{\\land,\\lor\\\},Π𝒫x\(φ→ψ;b\)\\displaystyle\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\(\\varphi\\to\\psi;b\)=Π𝒫x​\(φ,b\)→Π𝒫x​\(ψ,b\)\.\\displaystyle=\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\(\\varphi;b\)\\to\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\(\\psi;b\)\.Constants are unchanged\. Let

Φ~x=Π𝒫x​\(Φx0,0\)\\widetilde\{\\Phi\}\_\{x\}=\\Pi\_\{\\mathcal\{P\}\_\{x\}\}\(\\Phi\_\{x\}^\{0\};0\)be the formula before release finalization\. The emitted formula and atom inventory are

Φx\\displaystyle\\Phi\_\{x\}=ConstNorm⁡\(Φ~x\),\\displaystyle=\\operatorname\{ConstNorm\}\(\\widetilde\{\\Phi\}\_\{x\}\),𝒜x\\displaystyle\\mathcal\{A\}\_\{x\}=\{a∈𝒜~x:id⁡\(a\)∈LeafIds⁡\(Φx\)\}\.\\displaystyle=\\left\\\{a\\in\\widetilde\{\\mathcal\{A\}\}\_\{x\}:\\operatorname\{id\}\(a\)\\in\\operatorname\{LeafIds\}\(\\Phi\_\{x\}\)\\right\\\}\.HereConstNorm\\operatorname\{ConstNorm\}applies the usual truth\-preserving identities for⊤\\top,⊥\\bot, negation, conjunction, disjunction, and implication\. Removed atoms are not emitted\. The parity guard prevents a second negation when the same leaf occurrence is already under logical negation\. Projection preserves every Boolean operator, branch, atom owner, and provenance record; it neither applies De Morgan’s law nor moves participant polarity to the predicate\.

###### Example F\.6\(Event and participant polarity\)\.

ForThe teacher did not give the student a book, the event hasARG0,ARG1,ARG2, and:polarity \-\. Its two active atoms are

g1\\displaystyle g\_\{1\}=TriARG0,ARG1⁡\(teacher,give\-01,book\),\\displaystyle=\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG1\}\}\(\\textit\{teacher\},\\textit\{give\-01\},\\textit\{book\}\),g2\\displaystyle g\_\{2\}=TriARG0,ARG2⁡\(teacher,give\-01,student\)\.\\displaystyle=\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG2\}\}\(\\textit\{teacher\},\\textit\{give\-01\},\\textit\{student\}\)\.Event polarity preserves their shared parser scope:

Φx=¬\(g1∧g2\),\\Phi\_\{x\}=\\lnot\(g\_\{1\}\\land g\_\{2\}\),not\(¬g1\)∧\(¬g2\)\(\\lnot g\_\{1\}\)\\land\(\\lnot g\_\{2\}\)\. By contrast, polarity on an explicit participant is projected locally to each relation atom containing that participant\. For an AMR containingplay\-01 :ARG0 \(child :polarity \-\) :location statue, the output is the single atomp1p\_\{1\}, withvx​\(p1\)=“child play at statue”v\_\{x\}\(p\_\{1\}\)=\\textit\{\`\`child play at statue''\}, under formula¬p1\\lnot p\_\{1\}\. This participant\-only projection does not change the atom owner, negate the predicate, apply De Morgan’s law, or alter the surroundingand/orbranch\.

###### Definition F\.7\(Branch Isolation\)\.

When compiling one explicitand/orbranch, the compiler excludes atoms anchored only to sibling events and blocks inverse traversal into sibling roots\. If a shared owner has several event anchors, the anchor reachable only through the active branch is used in that branch’s formula view\. A participant descriptor may be shared across branches, but each event atom remains in the branch containing its event occurrence\.

###### Definition F\.8\(Translator Validity\)\.

The emitted frame contains only a formula AST and active atom records\. Each active atom has a unique nonempty identifier, a valid structured expression, and a nonempty unsigned verbalization\. The formula AST may use onlyatom,not,and,or, andimplies\. Anotnode has one argument, anandorornode has at least two arguments, and animpliesnode has an antecedent and a consequent\. The formula must satisfy

LeafIds⁡\(Φx\)=\{id⁡\(a\):a∈𝒜x\}\.\\operatorname\{LeafIds\}\(\\Phi\_\{x\}\)=\\\{\\operatorname\{id\}\(a\):a\\in\\mathcal\{A\}\_\{x\}\\\}\.No Boolean constant remains in the emitted formula\.

Any parsing, AMR decoding, compilation, or output\-validation failure yields an invalid translation, including an empty active inventory or a formula–atom closure mismatch\. No fallback translator or semantic\-repair rule is applied\.

##### Semantic boundary\.

The translator preserves explicit AMR coordination, conditions, and polarity, but does not infer modal, factive, or discourse\-level semantics\.

###### Example F\.7\(Isolating reentrant connective branches\)\.

Suppose the parser representsThe student reads a book and writes an essaywith a sharedstudentnode reentered by both event branches\. Branch\-local ownership then yields

TriARG0,ARG1⁡\(student,read\-01,book\)\\displaystyle\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG1\}\}\(\\textit\{student\},\\textit\{read\-01\},\\textit\{book\}\)∧TriARG0,ARG1⁡\(student,write\-01,essay\)\.\\displaystyle\\land\\operatorname\{Tri\}\_\{\\mathrm\{ARG0\},\\mathrm\{ARG1\}\}\(\\textit\{student\},\\textit\{write\-01\},\\textit\{essay\}\)\.

## Appendix GDetailed Calculation for the Constructed Example

Throughout Sections[G](https://arxiv.org/html/2608.18820#A7)–[I](https://arxiv.org/html/2608.18820#A9), candidate and active\-link\-set subscripts are suppressed when unambiguous\. We use the fixed main\-paper settingsWmax=100W\_\{\\max\}=100andϵ=1\\epsilon=1\. HereMbaseM^\{\\mathrm\{base\}\}andMforcedM^\{\\mathrm\{forced\}\}are the assignments returned by solving the base and target\-forced MaxSAT instances, andSemCost\\operatorname\{SemCost\}sums the weights of violated atom\-link clauses inΩsem\\Omega^\{\\mathrm\{sem\}\}\.

This section expands the constructed common\-target example from the main paper\. It shows how each local link outcome induces a MaxSAT calculation and how the resulting resistances are aggregated byTop\-Linkand PWAL\.

##### \(a\) Fixed translations and atom meanings\.

ΦP\\displaystyle\\Phi\_\{P\}=g,\\displaystyle=g,ΦA\\displaystyle\\Phi\_\{A\}=a1∧a2,\\displaystyle=a\_\{1\}\\land a\_\{2\},ΦSA\\displaystyle\\Phi\_\{S\_\{A\}\}=g∧a1∧a2,\\displaystyle=g\\land a\_\{1\}\\land a\_\{2\},ΦTA\\displaystyle\\Phi\_\{T\_\{A\}\}=ΦTB=b,\\displaystyle=\\Phi\_\{T\_\{B\}\}=b,ΦB\\displaystyle\\Phi\_\{B\}=d1∧d2,\\displaystyle=d\_\{1\}\\land d\_\{2\},ΦSB\\displaystyle\\Phi\_\{S\_\{B\}\}=g∧d1∧d2\.\\displaystyle=g\\land d\_\{1\}\\land d\_\{2\}\.gg: door is unlocked;a1,d1a\_\{1\},d\_\{1\}: Maya enter office;a2a\_\{2\}: Maya remain at office;d2d\_\{2\}: Maya leave office;bb: Maya present at office\.

##### \(b\) NLI outputs and induced semantic clauses\.

The retained alternatives are

A:\\displaystyle A:a1→b⁡\(Ent,p=0\.989,w=98\),\\displaystyle a\_\{1\}\\\!\\to b\\;\(\\texttt\{Ent\},p=0\.989,w=98\),a2→b⁡\(Ent,p=0\.995,w=99\);\\displaystyle a\_\{2\}\\\!\\to b\\;\(\\texttt\{Ent\},p=0\.995,w=99\);B:\\displaystyle B:d1→b⁡\(Ent,p=0\.989,w=98\),\\displaystyle d\_\{1\}\\\!\\to b\\;\(\\texttt\{Ent\},p=0\.989,w=98\),d2→b⁡\(Con,p=0\.668,w=66\)\.\\displaystyle d\_\{2\}\\\!\\to b\\;\(\\texttt\{Con\},p=0\.668,w=66\)\.They induce the weighted clauses

\[¬a1∨b\]98,\[¬a2∨b\]99,\[¬d1∨b\]98,\[¬d2∨¬b\]66\.\\begin\{gathered\}\\bigl\[\\neg a\_\{1\}\\lor b\\bigr\]\_\{98\},\\quad\\bigl\[\\neg a\_\{2\}\\lor b\\bigr\]\_\{99\},\\\\ \\bigl\[\\neg d\_\{1\}\\lor b\\bigr\]\_\{98\},\\quad\\bigl\[\\neg d\_\{2\}\\lor\\neg b\\bigr\]\_\{66\}\.\\end\{gathered\}The shared comparisong→bg\\\!\\to bis neutral with confidence0\.9820\.982and is discarded\. Each candidate has one unmatched target atom and two non\-neutral alternatives\. PWAL therefore assigns probability1/31/3to no\-link and to each listed candidate\-specific link\. Confidence determinesw⁡\(p\)w\(p\), not the local\-outcome probability\.

##### \(c\) MaxSAT calculation by local outcome\.

In this constructed example, each active\-link source is forced true by its candidate’s hard source formula\. With target\-inertia weightϵ=1\\epsilon=1, all displayed semantic\-link weights exceed the inertia weight\. The resistance score is

Δ​T\\displaystyle\\Delta T=SemCost⁡\(Mforced\)\\displaystyle=\\operatorname\{SemCost\}\(M^\{\\mathrm\{forced\}\}\)−SemCost⁡\(Mbase\),\\displaystyle\-\\operatorname\{SemCost\}\(M^\{\\mathrm\{base\}\}\),ρ\\displaystyle\\rho=Δ​TCmax−Rsat\.\\displaystyle=\\frac\{\\Delta T\}\{C\_\{\\max\}\}\-R\_\{\\mathrm\{sat\}\}\.In the no\-link case, the base and forced values ofbbare false and true, and both semantic costs are zero\. Under entailment they are both true and both costs are zero\. Under a contradiction of weightww, they are false and true, so the costs are00andww\. Consequently,

OutcomeΔ​T/CmaxRsatρNo\-link000Entailment01−1Contradiction101\\begin\{array\}\[\]\{lccc\}\\hline\\cr\\hline\\cr\\text\{Outcome\}&\\Delta T/C\_\{\\max\}&R\_\{\\mathrm\{sat\}\}&\\rho\\\\ \\hline\\cr\\text\{No\-link\}&0&0&0\\\\ \\text\{Entailment\}&0&1&\-1\\\\ \\text\{Contradiction\}&1&0&1\\\\ \\hline\\cr\\hline\\cr\\end\{array\}In the no\-link row,Cmax=\|𝒜T\|​Wmax=100C\_\{\\max\}=\|\\mathcal\{A\}\_\{T\}\|W\_\{\\max\}=100is the zero\-link fallback\. Inertia affects the two optima but is excluded fromSemCost\\operatorname\{SemCost\}\.

##### \(d\) Instantiated worlds and pairwise decision\.

For each worldω\\omega, report the score tuple𝐬⁡\(ω\)=\(Δ​T,Cmax,Rsat,ρ\)\\mathbf\{s\}\(\\omega\)=\(\\Delta T,C\_\{\\max\},R\_\{\\mathrm\{sat\}\},\\rho\)\. The complete world spaces, with probability1/31/3per world, are

A:\\displaystyle A:𝐬⁡\(ωA​0\)=\(0,100,0,0\),\\displaystyle\\mathbf\{s\}\(\\omega\_\{A0\}\)=\(0,100,0,0\),𝐬\(ωA​1\)=\(0,98,1,−1\),𝐬\(ωA​2\)=\(0,99,1,−1\);\\displaystyle\\mathbf\{s\}\(\\omega\_\{A1\}\)=\(0,98,1,\-1\),\\quad\\mathbf\{s\}\(\\omega\_\{A2\}\)=\(0,99,1,\-1\);B:\\displaystyle B:𝐬⁡\(ωB​0\)=\(0,100,0,0\),\\displaystyle\\mathbf\{s\}\(\\omega\_\{B0\}\)=\(0,100,0,0\),𝐬\(ωB​1\)=\(0,98,1,−1\),𝐬\(ωB​2\)=\(66,66,0,1\)\.\\displaystyle\\mathbf\{s\}\(\\omega\_\{B1\}\)=\(0,98,1,\-1\),\\quad\\mathbf\{s\}\(\\omega\_\{B2\}\)=\(66,66,0,1\)\.TheωA​1,ωA​2,ωB​1,ωB​2\\omega\_\{A1\},\\omega\_\{A2\},\\omega\_\{B1\},\\omega\_\{B2\}worlds activatea1→ba\_\{1\}\\\!\\to b,a2→ba\_\{2\}\\\!\\to b,d1→bd\_\{1\}\\\!\\to b, andd2→bd\_\{2\}\\\!\\to b, respectively\. Aggregation gives

Top\-Link:\\displaystyle\\textsc\{Top\-Link\}:LAtop=\{a2→b\},\\displaystyle L\_\{A\}^\{\\mathrm\{top\}\}=\\\{a\_\{2\}\\\!\\to b\\\},LBtop=\{d1→b\},\\displaystyle L\_\{B\}^\{\\mathrm\{top\}\}=\\\{d\_\{1\}\\\!\\to b\\\},σAtop=σBtop=−1⟹Tie;\\displaystyle\\sigma\_\{A\}^\{\\mathrm\{top\}\}=\\sigma\_\{B\}^\{\\mathrm\{top\}\}=\-1\\Longrightarrow\\textbf\{Tie\};PWAL:\\displaystyle\\text\{PWAL\}:μA=13​\(0−1−1\)=−23,\\displaystyle\\mu\_\{A\}=\\tfrac\{1\}\{3\}\(0\-1\-1\)=\-\\tfrac\{2\}\{3\},μB=13​\(0−1\+1\)=0,\\displaystyle\\mu\_\{B\}=\\tfrac\{1\}\{3\}\(0\-1\+1\)=0,μA<μB⟹Candidate A\.\\displaystyle\\mu\_\{A\}<\\mu\_\{B\}\\Longrightarrow\\textbf\{Candidate A\}\.

## Appendix HDetailed ARCT Success Trace

In this fully enumerable ARCT instance,Top\-Linkties, whereas PWAL selects the correct candidate for every seed 2026–2035 and under exact marginalization\. It is illustrative only and was not used for method or setting selection\. Tables[H\.1](https://arxiv.org/html/2608.18820#A8.T1)–[H\.4](https://arxiv.org/html/2608.18820#A8.T4)report the input, retained links, and complete world aggregation\.

##### \(a\) Input, fixed translations, and atom meanings\.

PremisePeople learn a lot from comment sections\.Candidate Atoo much learning hurtsCandidate Blearning never hurtsClaimComment sections have not failedTable H\.1:ARCT success trace\. Candidate B is gold\.The compiler produces

ΦSA\\displaystyle\\Phi\_\{S\_\{A\}\}=a1∧a2∧a3∧a4∧a5∧a6,\\displaystyle=a\_\{1\}\\land a\_\{2\}\\land a\_\{3\}\\land a\_\{4\}\\land a\_\{5\}\\land a\_\{6\},ΦSB\\displaystyle\\Phi\_\{S\_\{B\}\}=b1∧b2∧b3∧¬b4,\\displaystyle=b\_\{1\}\\land b\_\{2\}\\land b\_\{3\}\\land\\neg b\_\{4\},ΦT\\displaystyle\\Phi\_\{T\}=¬f∨¬c\.\\displaystyle=\\neg f\\lor\\neg c\.The atom surfaces below are reproduced verbatim from the translator output and were not manually edited\. The atom inventory is

a1,b1\\displaystyle a\_\{1\},b\_\{1\}:comment section,\\displaystyle:\\ \\text\{comment section\},a2,b2\\displaystyle a\_\{2\},b\_\{2\}:person learn lot,\\displaystyle:\\ \\text\{person learn lot\},a3,b3\\displaystyle a\_\{3\},b\_\{3\}:person learn toward section,\\displaystyle:\\ \\text\{person learn toward section\},a4\\displaystyle a\_\{4\}:learn hurt,a5:hurt much,a6:hurt too,\\displaystyle:\\ \\text\{learn hurt\},\\quad a\_\{5\}:\\ \\text\{hurt much\},\\quad a\_\{6\}:\\ \\text\{hurt too\},b4\\displaystyle b\_\{4\}:learn hurt during ever,\\displaystyle:\\ \\text\{learn hurt during ever\},f\\displaystyle f:section fail,c:comment section\.\\displaystyle:\\ \\text\{section fail\},\\quad c:\\ \\text\{comment section\}\.The negative literal¬b4\\neg b\_\{4\}is the compiled meaning of “learning never hurts\.” Exact surface matching supplies the deterministic semantic linksa1↔ca\_\{1\}\\leftrightarrow candb1↔cb\_\{1\}\\leftrightarrow c, each with fixed exact\-link weight 100\. Consequently only the unmatched target atomffis sampled\.

##### \(b\) NLI outputs, clause weights, and local outcomes\.

For an NLI confidencepp, the solver usesw⁡\(p\)=max⁡\{1,⌊100​p⌋\}w\(p\)=\\max\\\{1,\\lfloor 100p\\rfloor\\\}\. Entailment induces\[¬s∨f\]w⁡\(p\)\[\\neg s\\lor f\]\_\{w\(p\)\}, whereas contradiction induces\[¬s∨¬f\]w⁡\(p\)\[\\neg s\\lor\\neg f\]\_\{w\(p\)\}\.

Table H\.2:All retained candidate\-specific NLI links\. Each candidate’s five local outcomes—the four displayed links and no\-link—have probability1/51/5\.Notice that the final B\-link is built on the unsigned base atomb4b\_\{4\}, while the source formula hard\-enforces¬b4\\neg b\_\{4\}\. Its implication is therefore satisfied through¬b4\\neg b\_\{4\}and changes neither the target\-clause witness ratio nor semantic tension in the corresponding world\. This is why it is not equivalent to A’s positive “hurt much” entailment link\.

##### \(c\) MaxSAT calculation and all enumerated worlds\.

The source formula is hard in both MaxSAT instances;ΦT\\Phi\_\{T\}is hard only in the forced instance\. Unit target inertia participates in optimization but is excluded from semantic cost\. For each world,

Δ​T\\displaystyle\\Delta T=SemCost⁡\(Mforced\)\\displaystyle=\\operatorname\{SemCost\}\(M^\{\\mathrm\{forced\}\}\)−SemCost⁡\(Mbase\),\\displaystyle\-\\operatorname\{SemCost\}\(M^\{\\mathrm\{base\}\}\),ρ\\displaystyle\\rho=Δ​TCmax−Rsat\.\\displaystyle=\\frac\{\\Delta T\}\{C\_\{\\max\}\}\-R\_\{\\mathrm\{sat\}\}\.The exact match contributes 100 toCmaxC\_\{\\max\}; an active NLI link contributes its weight\. With no active NLI link,Cmax=100C\_\{\\max\}=100\. The exact link makescctrue in the base optimum\. An active contradiction link also supports¬f\\neg f, thereby witnessing the sole target clause¬f∨¬c\\neg f\\lor\\neg cand givingRsat=1R\_\{\\mathrm\{sat\}\}=1\. Tables[H\.3](https://arxiv.org/html/2608.18820#A8.T3)and[H\.4](https://arxiv.org/html/2608.18820#A8.T4)list the two complete five\-world spaces\. Every world has probability1/51/5;n2026n\_\{2026\}is its number of occurrences in the fixed seed\-2026 sample of 100 worlds for that candidate\.

Table H\.3:Candidate\-A worlds and seed\-2026 counts\. Link labels and weights are given in Table[H\.2](https://arxiv.org/html/2608.18820#A8.T2)\.Table H\.4:Candidate\-B worlds and seed\-2026 counts\. Link labels and weights are given in Table[H\.2](https://arxiv.org/html/2608.18820#A8.T2)\.For example, in A4 the hard source formula forcesa5a\_\{5\}true\. In the lower\-cost forced optimum, the weight\-100100exact link is preserved, makingcctrue; the hard target then requires¬f\\neg f, so the active entailment clause\[¬a5∨f\]42\[\\neg a\_\{5\}\\lor f\]\_\{42\}is violated\. HenceρA​4=42/142−0=0\.295775\\rho\_\{A4\}=42/142\-0=0\.295775\. By contrast, A2 supports¬f\\neg fwith no semantic penalty, soρA​2=0/198−1=−1\\rho\_\{A2\}=0/198\-1=\-1\.

##### \(d\) Aggregation and pairwise decision\.

Top\-Linkselects the highest\-confidence link forff, namelya2→fa\_\{2\}\\\!\\to fandb2→fb\_\{2\}\\\!\\to f, in both cases contradiction withp=0\.982p=0\.982\. The selected Candidate\-A and Candidate\-B configurations both have resistance−1\-1, soTop\-Linkties\. Exact marginalization instead gives

μA\\displaystyle\\mu\_\{A\}=15​\(0−1−1−1\+0\.295775\)=−0\.540845,\\displaystyle=\\tfrac\{1\}\{5\}\(0\-1\-1\-1\+0\.295775\)=\-0\.540845,μB\\displaystyle\\mu\_\{B\}=15​\(0−1−1−1\+0\)=−0\.600000,\\displaystyle=\\tfrac\{1\}\{5\}\(0\-1\-1\-1\+0\)=\-0\.600000,and therefore selects B because lower resistance is preferred\. The seed\-2026 Monte Carlo estimate uses the counts in Tables[H\.3](https://arxiv.org/html/2608.18820#A8.T3)and[H\.4](https://arxiv.org/html/2608.18820#A8.T4):

μ^A\\displaystyle\\widehat\{\\mu\}\_\{A\}=17​\(−1\)\+17​\(−1\)\+17​\(−1\)100\\displaystyle=\\frac\{17\(\-1\)\+17\(\-1\)\+17\(\-1\)\}\{100\}\+27​\(0\.295775\)\+22​\(0\)100=−0\.430141,\\displaystyle\+\\frac\{27\(0\.295775\)\+22\(0\)\}\{100\}=\-0\.430141,μ^B\\displaystyle\\widehat\{\\mu\}\_\{B\}=29​\(−1\)\+18​\(−1\)\+16​\(−1\)100\\displaystyle=\\frac\{29\(\-1\)\+18\(\-1\)\+16\(\-1\)\}\{100\}\+13​\(0\)\+24​\(0\)100=−0\.630000\.\\displaystyle\+\\frac\{13\(0\)\+24\(0\)\}\{100\}=\-0\.630000\.Thus sampled PWAL, exact PWAL, and all ten evaluation seeds select the gold Candidate B, whileTop\-Linkties\.

## Appendix IDetailed Stableα\\alphaNLI Failure Trace

In this fully enumerableα\\alphaNLI instance,Top\-Linkselects the correct candidate, whereas PWAL selects the wrong candidate for every seed 2026–2035 and under exact marginalization\. Candidate A is gold\. It is illustrative only and was not used for method or setting selection\. Tables[I\.1](https://arxiv.org/html/2608.18820#A9.T1)–[I\.5](https://arxiv.org/html/2608.18820#A9.T5)report the input, atoms, links, categorical choices, and representative worlds\.

##### \(a\) Input, fixed translations, and atom meanings\.

PremiseBill was poor\.Candidate AHis business went bankrupt and he had to take a new job\.Candidate BHis business is worth millions\.OutcomeBill made less money as a computer scientist than he did before\.Table I\.1:Stableα\\alphaNLI failure trace\. Candidate A is gold\.The source and target formulae are conjunctions:

ΦSA=⋀i=16ai,ΦSB=⋀i=14bi,ΦT=⋀j=17hj\.\\Phi\_\{S\_\{A\}\}=\\bigwedge\_\{i=1\}^\{6\}a\_\{i\},\\qquad\\Phi\_\{S\_\{B\}\}=\\bigwedge\_\{i=1\}^\{4\}b\_\{i\},\\qquad\\Phi\_\{T\}=\\bigwedge\_\{j=1\}^\{7\}h\_\{j\}\.
The atom surfaces in Table[I\.2](https://arxiv.org/html/2608.18820#A9.T2)are reproduced verbatim from the translator output and were not manually edited\.

Table I\.2:Complete atom inventory\.h2h\_\{2\}andh3h\_\{3\}are distinct compiled role occurrences even though their verbalizations coincide\.Unlike the ARCT trace, this instance has no exact surface links: all semantic links below are uncertain atom\-level NLI links\.

##### \(b\) Complete NLI link inventory\.

As before,w⁡\(p\)=max⁡\{1,⌊100​p⌋\}w\(p\)=\\max\\\{1,\\lfloor 100p\\rfloor\\\}\. A retained entailments→hs\\\!\\to hcontributes\[¬s∨h\]w⁡\(p\)\[\\neg s\\lor h\]\_\{w\(p\)\}, and a retained contradiction contributes\[¬s∨¬h\]w⁡\(p\)\[\\neg s\\lor\\neg h\]\_\{w\(p\)\}\. Becauseh2h\_\{2\}andh3h\_\{3\}have identical candidate sets, a row markedh2,h3h\_\{2\},h\_\{3\}represents two separate links, one to each target occurrence\.

Cand\.TargetSourceSource surfaceLabelppw⁡\(p\)w\(p\)Ah2,h3h\_\{2\},h\_\{3\}a1a\_\{1\}Bill is poorCon0\.98998Ah2,h3h\_\{2\},h\_\{3\}a2a\_\{2\}business is bankruptedCon0\.97397Ah2,h3h\_\{2\},h\_\{3\}a4a\_\{4\}he’s businessEnt0\.67067Ah2,h3h\_\{2\},h\_\{3\}a6a\_\{6\}he obligate takeEnt0\.58758Ah5h\_\{5\}a3a\_\{3\}job is newCon0\.98398Ah6h\_\{6\}a1a\_\{1\}Bill is poorEnt0\.57957Ah6h\_\{6\}a2a\_\{2\}business is bankruptedEnt0\.42342Ah7h\_\{7\}a1a\_\{1\}Bill is poorCon0\.91891Ah7h\_\{7\}a2a\_\{2\}business is bankruptedCon0\.88688Bh2,h3h\_\{2\},h\_\{3\}b1b\_\{1\}Bill is poorCon0\.98998Bh2,h3h\_\{2\},h\_\{3\}b2b\_\{2\}multiple 1000000 dollarsEnt0\.68568Bh2,h3h\_\{2\},h\_\{3\}b3b\_\{3\}he’s businessEnt0\.67067Bh2,h3h\_\{2\},h\_\{3\}b4b\_\{4\}business worth multipleEnt0\.94094Bh6h\_\{6\}b1b\_\{1\}Bill is poorEnt0\.57957Bh6h\_\{6\}b2b\_\{2\}multiple 1000000 dollarsCon0\.55155Bh6h\_\{6\}b4b\_\{4\}business worth multipleCon0\.76176Bh7h\_\{7\}b1b\_\{1\}Bill is poorCon0\.91891Bh7h\_\{7\}b2b\_\{2\}multiple 1000000 dollarsEnt0\.90190Bh7h\_\{7\}b4b\_\{4\}business worth multipleEnt0\.77477Table I\.3:All 27 retained NLI links, grouped only when two target occurrences have identical source, label, and confidence\.The nine grouped A rows contain 13 links because the first four rows each occur for bothh2h\_\{2\}andh3h\_\{3\}\. The ten grouped B rows similarly contain 14 links\. Neutral source–target pairs are absent from the retained inventory and never enter a world\.

##### \(c\) Categorical world construction\.

For each target atom, PWAL samples uniformly from its retained non\-neutral links plus an explicit no\-link outcome\. Target atoms are sampled independently\. The complete per\-target distributions are therefore:

Table I\.4:Per\-target categorical choices\. Every listed choice within a cell has the displayed common probability\.Thus the candidate\-specific world counts are

NA\\displaystyle N\_\{A\}=1⋅5⋅5⋅1⋅2⋅3⋅3=450,\\displaystyle=1\\cdot 5\\cdot 5\\cdot 1\\cdot 2\\cdot 3\\cdot 3=450,NB\\displaystyle N\_\{B\}=1⋅5⋅5⋅1⋅1⋅4⋅4=400\.\\displaystyle=1\\cdot 5\\cdot 5\\cdot 1\\cdot 1\\cdot 4\\cdot 4=400\.All A worlds have probability1/4501/450, and all B worlds have probability1/4001/400\. The displayed sampled run draws 100 worlds per candidate with seed 2026 rather than enumerating these world spaces\.

##### \(d\) DeterministicTop\-Linkcalculation\.

Top\-Linkactivates the highest\-confidence non\-neutral link for every target that has one\. Its active sets are

LAtop=\\displaystyle L\_\{A\}^\{\\mathrm\{top\}\}=\{\}\{a1→h2\(Con\),a1→h3\(Con\),\\displaystyle\\\{a\_\{1\}\\\!\\to h\_\{2\}\\;\(\\texttt\{Con\}\),a\_\{1\}\\\!\\to h\_\{3\}\\;\(\\texttt\{Con\}\),a3→h5\(Con\),a1→h6\(Ent\),\\displaystyle a\_\{3\}\\\!\\to h\_\{5\}\\;\(\\texttt\{Con\}\),a\_\{1\}\\\!\\to h\_\{6\}\\;\(\\texttt\{Ent\}\),a1→h7\(Con\)\},\\displaystyle a\_\{1\}\\\!\\to h\_\{7\}\\;\(\\texttt\{Con\}\)\\\},LBtop=\\displaystyle L\_\{B\}^\{\\mathrm\{top\}\}=\{\}\{b1→h2\(Con\),b1→h3\(Con\),\\displaystyle\\\{b\_\{1\}\\\!\\to h\_\{2\}\\;\(\\texttt\{Con\}\),b\_\{1\}\\\!\\to h\_\{3\}\\;\(\\texttt\{Con\}\),b4→h6\(Con\),b1→h7\(Con\)\}\.\\displaystyle b\_\{4\}\\\!\\to h\_\{6\}\\;\(\\texttt\{Con\}\),b\_\{1\}\\\!\\to h\_\{7\}\\;\(\\texttt\{Con\}\)\\\}\.For A, the active capacity isCmax=98\+98\+98\+57\+91=442C\_\{\\max\}=98\+98\+98\+57\+91=442\. Forcing the positive target conjunction violates the four contradiction clauses \(cost98\+98\+98\+91=38598\+98\+98\+91=385\), while the entailment witnesses one of seven target clauses\. Hence

ρAtop=385/442−1/7=0\.728184\.\\rho\_\{A\}^\{\\mathrm\{top\}\}=385/442\-1/7=0\.728184\.For B, all four selected links are contradictions, soΔ​T=Cmax=98\+98\+76\+91=363\\Delta T=C\_\{\\max\}=98\+98\+76\+91=363and no positive target clause is witnessed:

ρBtop=363/363−0=1\.\\rho\_\{B\}^\{\\mathrm\{top\}\}=363/363\-0=1\.Lower resistance is preferred;Top\-Linktherefore selects the gold Candidate A\.

##### \(e\) PWAL MaxSAT worlds and representative arithmetic\.

Every sampled or enumerated world uses the same base/forced MaxSAT definition as Section[G](https://arxiv.org/html/2608.18820#A7):

ρ=Δ​TCmax−Rsat\.\\rho=\\frac\{\\Delta T\}\{C\_\{\\max\}\}\-R\_\{\\mathrm\{sat\}\}\.Candidate A and Candidate B have 450 and 400 worlds, respectively\. The two candidate\-specific spaces are marginalized separately rather than crossed into450×400450\\times 400joint worlds\. Table[I\.4](https://arxiv.org/html/2608.18820#A9.T4)defines both complete world spaces; Table[I\.5](https://arxiv.org/html/2608.18820#A9.T5)gives four seed\-2026 draws that illustrate the most tense A world, the worlds closest to the two sampled means, and the B world with the largest target\-clause witness ratio\. Part \(f\) aggregates all 100 worlds sampled separately for each candidate\.

Table I\.5:Representative seed\-2026 candidate\-specific worlds for the stableα\\alphaNLI failure trace\.ConandEntrefer to Table[I\.3](https://arxiv.org/html/2608.18820#A9.T3)\. Draw is the index within the fixed seed\-2026 candidate\-specific sample\.For example, draw A76 has three contradiction clauses whose weights sum to98\+98\+91=28798\+98\+91=287; those clauses are violated when the positive target is forced\. Its two entailment links witnessh3h\_\{3\}andh6h\_\{6\}, giving

ρA​76=287/387−2/7=0\.455888\.\\rho\_\{A76\}=287/387\-2/7=0\.455888\.In B20 all four active links entail distinct positive target occurrences, so there is no semantic penalty and four of seven clauses are witnessed:ρB​20=0/322−4/7=−0\.571429\\rho\_\{B20\}=0/322\-4/7=\-0\.571429\. These rows illustrate why many B worlds receive lower resistance than A worlds\.

##### \(f\) Monte Carlo aggregation, exact check, and decision\.

For theK=100K=100seed\-2026 worlds sampled separately for each candidate, let

T¯=1K​∑k=1KΔ​TkCmax,k,R¯=1K​∑k=1KRsat,k\.\\overline\{T\}=\\frac\{1\}\{K\}\\sum\_\{k=1\}^\{K\}\\frac\{\\Delta T\_\{k\}\}\{C\_\{\\max,k\}\},\\qquad\\overline\{R\}=\\frac\{1\}\{K\}\\sum\_\{k=1\}^\{K\}R\_\{\\mathrm\{sat\},k\}\.Thenμ^=T¯−R¯\\widehat\{\\mu\}=\\overline\{T\}\-\\overline\{R\}, and the seed\-2026 sample averages are

T¯R¯μ^=T¯−R¯A0\.6672640\.2042860\.462978B0\.3737970\.2842860\.089512\\begin\{array\}\[\]\{c@\{\\qquad\}ccc\}&\\overline\{T\}&\\overline\{R\}&\\widehat\{\\mu\}=\\overline\{T\}\-\\overline\{R\}\\\\ A&0\.667264&0\.204286&0\.462978\\\\ B&0\.373797&0\.284286&0\.089512\\end\{array\}PWAL therefore selects B, the distractor\. Exact marginalization over all 450 Candidate\-A worlds and 400 Candidate\-B worlds gives

μA\\displaystyle\\mu\_\{A\}=0\.449152,\\displaystyle=0\.449152,μB\\displaystyle\\mu\_\{B\}=0\.098678,\\displaystyle=0\.098678,μB−μA\\displaystyle\\mu\_\{B\}\-\\mu\_\{A\}=−0\.350474\.\\displaystyle=\-0\.350474\.Exact marginalization therefore confirms the same wrong decision\. The absolute exact margin is0\.3504740\.350474; all seeds 2026–2035 choose B, and the smallest sampled absolute margin is0\.29170\.2917\. Thus the observed failure is separated from the tie threshold and persists across all ten evaluation seeds as well as under exact marginalization\.

The arithmetic also localizes the failure mechanism at the score level\. In the seed\-2026 sample the distractor has both lower normalized semantic tension \(0\.3738 versus 0\.6673\) and a larger target\-clause witness ratio \(0\.2843 versus 0\.2043\)\. This trace does not, by itself, assign the upstream cause to AMR parsing, formula compilation, atom\-level NLI, or the resistance function\.