Paper deep dive
Pairwise Logical Selection of Enthymeme Completions under Semantic-Link Uncertainty
Xuyao Feng, Antonis Bikakis
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 8/20/2026, 5:11:00 AM
Summary
The paper introduces Possible-World Atom-Link Formalization (PWAL), a neuro-symbolic method for pairwise logical selection of enthymeme completions (missing premises or claims). PWAL addresses semantic-link uncertainty by marginalizing logical resistance over alternative cross-formula semantic-link configurations, unlike the prior Top-Link method which uses a single highest-confidence configuration. Evaluated on five tasks (ARCT, CDED, iDebate, AAE2, alphaNLI), PWAL significantly improves strict accuracy and reduces tie rates compared to Top-Link.
Entities (11)
Relation Signals (7)
PWAL → improves → Strict Accuracy
confidence 95% · Relative to Top-Link, PWAL raises strict accuracy by 2.95-30.86 percentage points... on all five tasks.
PWAL → reduces → tie rates
confidence 95% · PWAL... reduces tie rates by 4.57-58.00 percentage points on all five tasks.
ARCT → evaluates → missing-premise selection
confidence 90% · The Argument Reasoning Comprehension Task (ARCT)... evaluate missing-premise selection.
iDebate → evaluates → missing-claim selection
confidence 90% · Tasks derived from iDebate... evaluate missing-claim selection.
PWAL → marginalizes → logical resistance
confidence 90% · PWAL... marginalizes logical resistance over alternative cross-formula semantic-link configurations.
Top-Link → uses → Partial MaxSAT
confidence 90% · Top-Link uses weighted Partial MaxSAT under a single configuration of highest-confidence semantic links.
AMR → isusedfortranslation → PWAL
confidence 85% · Translation of AMR into Logic... we use a fixed rule-based compiler that maps an AMR graph to structured semantic atoms and a propositional formula.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Arguments often omit premises or claims, forming enthymemes. We study pairwise logical selection between two candidates for the omitted component. Existing natural language methods can identify or generate candidates but often do not expose how the selected candidate completes the inference, while logic-based approaches usually assume that the required formulae and background knowledge are available. We extend a prior neuro-symbolic pipeline from missing-premise to missing-claim selection and replace binary entailment outcomes with logical-resistance scores. Top-Link uses weighted Partial MaxSAT 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 PWAL on 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 to Top-Link, PWAL raises strict accuracy by 2.95-30.86 percentage points and reduces tie rates by 4.57-58.00 percentage points on all five tasks. When ties receive half credit, accuracy still increases by 0.45-6.04 percentage points. PWAL also records the translated formulae, sampled link configurations, and resistance components for every comparison, providing a transparent trace of each score.
Tags
Links
- Source: https://arxiv.org/abs/2608.18820v1
- Canonical: https://arxiv.org/abs/2608.18820v1
Trouble viewing inline? Open PDF directly →
Full Text
142,141 characters extracted from source content.
Expand or collapse full text
Pairwise Logical Selection of Enthymeme Completions under Semantic-Link Uncertainty Xuyao Feng Antonis Bikakis 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 define Top-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 α for abductive hypothesis selection. Relative to Top-Link, PWAL raises strict accuracy by 2.952.95–30.8630.86 percentage points and reduces tie rates by 4.574.57–58.0058.00 percentage points on all five tasks. When ties receive half credit, accuracy still increases by 0.450.45–6.046.04 percentage 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; Singh et al. 2022; Sviridova, Cabrio, and Villata 2026), 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; de Saint-Cyr 2011; Black and Hunter 2012; Hosseini, Modgil, and Rodrigues 2014; Xydis et al. 2020; Panisson, McBurney, and Bordini 2022; Hunter 2022; Leiva, Gottifredi, and García 2023; Leiva, García, and Gottifredi 2025; Ben-Naim, David, and Hunter 2025; David and Hunter 2025), 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). 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 candidate c defines a source statement collection ScS_c evaluated against a target statement collection TcT_c. Missing-premise tasks vary ScS_c while holding TcT_c fixed; missing-claim tasks hold ScS_c fixed while varying TcT_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-Link serves 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 evaluate Top-Link and PWAL on five pairwise tasks. The Argument Reasoning Comprehension Task (ARCT) (Habernal et al. 2018) and a task derived from Context-Dependent Evidence Detection (CDED) (Rinott et al. 2015) evaluate missing-premise selection. Tasks derived from iDebate (Wang and Ling 2016) and Argument Annotated Essays v2 (AAE2) (Stab and Gurevych 2017) evaluate missing-claim selection. We also evaluate Abductive Natural Language Inference (α ) (Bhagavatula et al. 2020) as a pairwise task for abductive hypothesis selection. The four argumentation tasks cover both premise- and claim-side completion, while α 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; Olausson et al. 2023; Ye et al. 2023; Kirtania, Gupta, and Radhakrishna 2024). Some refine a generated formalization using solver feedback or aggregate predictions across several generated formalizations (Pan et al. 2023; Olausson et al. 2023). Recent enthymeme methods compare supplied premise candidates through natural-language multi-agent debate (Ku et al. 2025), optimize logical formalizations over argument maps (David and Hunter 2025), or axiomatize the evaluation of alternative formalizations (Ben-Naim, David, and Hunter 2025). 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; Bach et al. 2017; Riegel et al. 2020). 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). Nodes denote concepts or PropBank frames. In a frame label such as chase-01, chase is the predicate lemma and 01 is its PropBank sense identifier. Labeled edges encode PropBank-derived core roles such as :ARG0 and :ARG1 (Kingsbury and Palmer 2002), alongside general AMR relations such as :location and :time (Banarescu et al. 2013). AMR also represents coordination, conditions, polarity, and reentrancy. Motivated by compositional AMR semantics (Bos 2016), 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 A, let ℒ()L(A) be the smallest formula language containing every a∈a and closed under ¬ , ∧ , ∨ , and →. For each successfully translated statement x, the solver-facing representation is (x)=⟨x,Φx,x⟩ Rep(x)= _x, _x,V_x , where: • xA_x is the finite, nonempty set of active semantic atoms; • Φx∈ℒ(x) _x (A_x) is the propositional formula compiled from the AMR structure; and • xV_x maps each atom in xA_x to a deterministic, nonempty surface verbalization ending in a full stop. Formula-level polarity is represented in Φx _x rather than in xV_x. Let Atoms(Φx)Atoms( _x) denote the atoms occurring in Φx _x. The translator satisfies Atoms(Φx)=xAtoms( _x)=A_x, so the atom inventory is exactly the set of propositional variables occurring in the formula. The main atom forms are Uni(u)Uni(u), Dyaκ(u,v)Dya_κ(u,v), and Triκa,κb(u,e,v)Tri_ _a, _b(u,e,v). Here u,v,eu,v,e are AMR terms, with e denoting the predicate occurrence shared by the two roles in a triple, and κ,κa,κbκ, _a, _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). Consider x+x^+, A cute dog chases a cat, and the corresponding negative statement x−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 produces a1=Dyamod(dog,cute)a_1=Dya_mod(dog,cute), while the shared :ARG0 and :ARG1 roles produce a2=TriARG0,ARG1(dog,chase-01,cat)a_2=Tri_ARG0,ARG1(dog,chase-01,cat). Both translations have x+=x−=a1,a2A_x^+=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 _x^+=a_2 a_1, whereas Φx−=¬(a2∧a1) _x^-= (a_2 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). For c∈A,Bc∈\A,B\, let Sc=(sc,1,…,sc,nc)S_c=(s_c,1,…,s_c,n_c) and Tc=(tc,1,…,tc,mc)T_c=(t_c,1,…,t_c,m_c) denote the source and target statement collections for candidate c. Statements within each collection are conjoined. Common-source tasks satisfy SA=SBS_A=S_B, while common-target tasks satisfy TA=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 either Top-Link or PWAL; it selects the lower-scoring candidate or returns a tie. For each resistance-based scoring method, let σc _c denote the score assigned to candidate c. Lower logical scores are preferred. The pipeline returns Tie when σA=σB _A= _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 in ScS_c and TcT_c is translated independently. Before assembly, statement-local atoms are renamed so that atom namespaces are disjoint across all statement occurrences in ScS_c and TcT_c. The same renaming is applied to each statement’s formula and verbalization map. Below, xiA_x_i, Φxi _x_i, and xiV_x_i denote these renamed representations. Definition 2 (Candidate Source and Target Representation). For each nonempty collection X∈Sc,TcX∈\S_c,T_c\, write X=(x1,…,x|X|)X=(x_1,…,x_|X|), and define X=⨄i=1|X|xiA_X= _i=1^|X|A_x_i and ΦX=⋀i=1|X|Φxi _X= _i=1^|X| _x_i, where ⨄ denotes disjoint union. For each a∈Xa _X, let xix_i be its unique originating statement and set X(a)=xi(a)V_X(a)=V_x_i(a). The source and target namespaces satisfy Sc∩Tc=∅A_S_c _T_c= . Let CNF(Φ)CNF( ) denote the clause collection in conjunctive normal form (CNF) produced by the fixed SymPy-based conversion used by the solver (Meurer et al. 2017). For X∈Sc,TcX∈\S_c,T_c\, define ΓX=⨄i=1|X|CNF(Φxi) _X= _i=1^|X|CNF( _x_i). For clauses, ⨄ preserves statement-indexed clause occurrences. A literal is an atom or its negation; a clause is a disjunction of literals, written [ℓ1∨⋯∨ℓm][ _1 ·s _m]. Then ΦX≡⋀q∈ΓXq _X≡ _q∈ _Xq. The fixed CNF conversion introduces no auxiliary Boolean atoms. Example 2 (Source and Target Assembly). Suppose that, after renaming, Φsc,1=a0 _s_c,1=a_0, Φsc,2=a1 _s_c,2=a_1, Φsc,3=¬(a2∧a3) _s_c,3= (a_2 a_3), and Φtc,1=b1→b2 _t_c,1=b_1→ b_2. Then ΦSc=a0∧a1∧¬(a2∧a3) _S_c=a_0 a_1 (a_2 a_3) and ΦTc=b1→b2 _T_c=b_1→ b_2, with ΓSc=[a0],[a1],[¬a2∨¬a3] _S_c=\[a_0],[a_1],[ a_2 a_3]\ and ΓTc=[¬b1∨b2] _T_c=\[ b_1 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,NeuY=\ Ent, Con, Neu\ denote the entailment, contradiction, and neutral labels. For nonempty verbalization strings u and v, let (u,v)=(y,p)∈×[0,1] N(u,v)=(y,p) ×[0,1], where u is the NLI premise, v is the hypothesis, y is the predicted label, and p is the confidence assigned to y, rounded to three decimal places. Definition 4 (Exact and NLI-Derived Atom Links). Let cf(u)cf(u) denote the case-folded form of string u. Define ℳcex _c^ex =(a,b)∈Sc×Tc∣cf(Sc(a))=cf(Tc(b)), =\(a,b) _S_c×A_T_c (V_S_c(a))=cf(V_T_c(b))\, c _c =b∈Tc∣∄a∈Sc:(a,b)∈ℳcex. =\b _T_c a _S_c:(a,b) _c^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 each a∈Sca _S_c and b∈cb _c, let (ya,b,pa,b)=(Sc(a),Tc(b))(y_a,b,p_a,b)= N(V_S_c(a),V_T_c(b)). The retained non-neutral alternatives are ℛc(b)=(a,b,ya,b,pa,b)∣a∈Sc,ya,b∈Ent,ConR_c(b)=\(a,b,y_a,b,p_a,b) a _S_c,\ y_a,b∈\ Ent, Con\\. Neutral outputs generate no link. ℛc(b)R_c(b) contains the alternative non-exact links for the unmatched target atom b. Example 3 (Exact and NLI-Derived Links). Suppose Sc(a1)=Sc(a2)=Tc(b1)=“dog bark.”V_S_c(a_1)=V_S_c(a_2)=V_T_c(b_1)=``dog bark.′, and these are the only exact matches. Then ℳcex=(a1,b1),(a2,b1)M_c^ex=\(a_1,b_1),(a_2,b_1)\. Let b2b_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)( Ent,0.88) and (Con,0.83)( Con,0.83), respectively, and all other comparisons with b2b_2 are neutral, then ℛc(b2)=(a3,b2,Ent,0.88),(a4,b2,Con,0.83)R_c(b_2)=\(a_3,b_2, Ent,0.88),(a_4,b_2, Con,0.83)\. Weighted Atom-Link Clauses Atom links are encoded as weighted clauses. We write (q,∞)(q,∞) for a hard clause and (q,w)(q,w), with w∈ℕ>0w _>0, for a soft clause. Every hard clause must be satisfied, while w is the penalty incurred when the soft clause q is violated. Definition 5 (Weighted Atom-Link Clauses). Let Wmax∈ℕ>0W_ _>0 be the maximum finite link weight and define w(p)=max1,⌊Wmaxp⌋w(p)= \1, W_ p \ for p∈[0,1]p∈[0,1], where ⌊x⌋ x is the greatest integer not exceeding x. Thus, w(p)∈1,…,Wmaxw(p)∈\1,…,W_ \, with the outer maximum ensuring a positive weight. Each exact link (a,b)∈ℳcex(a,b) _c^ex contributes ([¬a∨b],Wmax)([ a b],W_ ) and ([a∨¬b],Wmax)([a b],W_ ), encoding a→ba→ b and b→ab→ a, respectively. Together they form a soft equivalence. Define Ωcex=⋃(a,b)∈ℳcex([¬a∨b],Wmax),([a∨¬b],Wmax) _c^ex= _(a,b) _c^ex\([ a b],W_ ),([a b],W_ )\. For a non-exact link r=(a,b,y,p)r=(a,b,y,p), let cl(r)=([¬a∨b],w(p))cl(r)=([ a b],w(p)) if y=Enty= Ent, and cl(r)=([¬a∨¬b],w(p))cl(r)=([ a b],w(p)) if y=Cony= Con. An active non-exact link set Lc⊆⋃b∈cℛc(b)L_c _b _cR_c(b) is admissible if |Lc∩ℛc(b)|≤1|L_c _c(b)|≤ 1 for every b∈cb _c. Thus, each unmatched target atom has at most one active non-exact link. The atom-link clause collection induced by LcL_c is Ωcsem(Lc)=Ωcex∪cl(r)∣r∈Lc _c^sem(L_c)= _c^ex∪\cl(r) r∈ L_c\. Exact-link clauses occur in Ωcsem(Lc) _c^sem(L_c) for every admissible LcL_c. Example 4 (Weighted Atom-Link Clauses). Continuing Example 3, let Wmax=100W_ =100. For each i∈1,2i∈\1,2\, the exact link (ai,b1)(a_i,b_1) contributes ([¬ai∨b1],100)([ a_i b_1],100) and ([ai∨¬b1],100)([a_i b_1],100). The two non-exact alternatives map to ([¬a3∨b2],88)([ a_3 b_2],88) and ([¬a4∨¬b2],83)([ a_4 b_2],83). An admissible configuration may activate either non-exact link for b2b_2, or neither, but not both. Partial MaxSAT Evaluation For a fixed active non-exact link set LcL_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 _c^hard=\(q,∞) q∈ _S_c\, and the target-inertia clauses are Ωcinertia=([¬b],ϵ)∣b∈Tc _c^inertia=\([ b],ε) b _T_c\, where ϵ∈ℕ>0ε _>0. Inertia prefers false target atoms but does not require them. Define the base and forced instances by ℐcbase(Lc) _c^base(L_c) =Ωchard∪Ωcsem(Lc)∪Ωcinertia, = _c^hard∪ _c^sem(L_c)∪ _c^inertia, ℐcforced(Lc) _c^forced(L_c) =ℐcbase(Lc)∪(q,∞)∣q∈ΓTc. =I_c^base(L_c)∪\(q,∞) q∈ _T_c\. Let Mcbase(Lc)M_c^base(L_c) and Mcforced(Lc)M_c^forced(L_c) be the assignments returned by solving ℐcbase(Lc)I_c^base(L_c) and ℐcforced(Lc)I_c^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 corresponding McbaseM_c^base or McforcedM_c^forced is the assignment returned by the solver; no secondary optimization criterion is applied. For any assignment M, define SemCostc(M,Lc)=∑(q,w)∈Ωcsem(Lc)M⊧̸qw.SemCost_c(M,L_c)= _ subarrayc(q,w)∈ _c^sem(L_c)\\ M q subarrayw. 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 from SemCostcSemCost_c. The semantic tension is the signed change ΔTc(Lc) T_c(L_c) =SemCostc(Mcforced(Lc),Lc) =SemCost_c(M_c^forced(L_c),L_c) −SemCostc(Mcbase(Lc),Lc). -SemCost_c(M_c^base(L_c),L_c). A positive ΔTc(Lc) 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 ratio Rsat,c(Lc)R_sat,c(L_c). The condition NegSupc,Lc(b)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). Write Mc0=Mcbase(Lc)M_c^0=M_c^base(L_c). For a target atom b, define NegSupc,Lc(b)NegSup_c,L_c(b) to hold if either there exists a∈Sca _S_c such that (a,b)∈ℳcex(a,b) _c^ex and Mc0⊧¬aM_c^0 a, or there exists (a,b,Con,p)∈Lc(a,b, Con,p)∈ L_c such that Mc0⊧aM_c^0 a. We refer to this requirement as the polarity-aware negative guard. For a target literal ℓ over atom b, let Witc,Lc(ℓ)=1Wit_c,L_c( )=1 if either ℓ=b =b and Mc0⊧bM_c^0 b, or ℓ=¬b = b, Mc0⊧¬bM_c^0 b, and NegSupc,Lc(b)NegSup_c,L_c(b); otherwise it is 00. For q∈ΓTcq∈ _T_c, let Witc,Lc(q)=maxℓ∈qWitc,Lc(ℓ)Wit_c,L_c(q)= _ ∈ qWit_c,L_c( ). For ΓTc≠∅ _T_c≠ , the target-clause witness ratio is Rsat,c(Lc)=|ΓTc|−1∑q∈ΓTcWitc,Lc(q).R_sat,c(L_c)=| _T_c|^-1 _q∈ _T_cWit_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_ |M_c^ex|+ _(a,b,y,p)∈ L_cw(p). Each exact link contributes WmaxW_ , 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_ ,c(L_c)= casesW_c(L_c),&W_c(L_c)>0,\\ |A_T_c|W_ ,&otherwise. cases We use Cmax,c(Lc)C_ ,c(L_c) as the normalization capacity; it is an upper bound on the active atom-link cost but need not be attainable. When Wc(Lc)=0W_c(L_c)=0, no atom-link clause is active and ΔTc(Lc)=0 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). _c(L_c)= T_c(L_c)C_ ,c(L_c)-R_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] _S_c=\[a]\, ΓTc=[b] _T_c=\[b]\, Wmax=100W_ =100, and ϵ=1ε=1, with no exact links. For rE=(a,b,Ent,0.80)r_E=(a,b, Ent,0.80) and Lc=rEL_c=\r_E\, the hard source clause forces a true. The base optimum sets b true because violating inertia costs 11, whereas violating the entailment link costs 8080; the forced optimum also sets b true. Both atom-link costs are 00, so ΔTc(Lc)=0 T_c(L_c)=0, Rsat,c(Lc)=1R_sat,c(L_c)=1, Cmax,c(Lc)=80C_ ,c(L_c)=80, and ρc(Lc)=−1 _c(L_c)=-1. For rC=(a,b,Con,0.70)r_C=(a,b, Con,0.70) and Lc=rCL_c=\r_C\, the base optimum sets b false, while the forced optimum sets b true and violates the weight-7070 contradiction link. Although the forced optimum also violates inertia, inertia is excluded from SemCostcSemCost_c. Thus ΔTc(Lc)=70 T_c(L_c)=70, Rsat,c(Lc)=0R_sat,c(L_c)=0, Cmax,c(Lc)=70C_ ,c(L_c)=70, and ρc(Lc)=1 _c(L_c)=1. If the target instead contains ¬b b without an exact or contradiction link supporting that polarity, inertia may set b false, but ¬b b is 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-Link and 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-Link evaluates one admissible non-exact link configuration, whereas PWAL averages logical resistance over a distribution of such configurations. Definition 8 (Top-Link). For each b∈cb _c with ℛc(b)≠∅R_c(b)≠ , define rc⋆(b)∈argmax(a,b,y,p)∈ℛc(b)pr_c (b)∈ _(a,b,y,p) _c(b)p as a maximum-confidence link, breaking confidence ties by a fixed total order on ScA_S_c induced by source-statement order and the translator’s atom order. Set Lctop=rc⋆(b)∣b∈c,ℛc(b)≠∅L_c^top=\r_c (b) b _c,\,R_c(b)≠ \ and σctop=ρc(Lctop) _c^top= _c(L_c^top). If ℛc(b)=∅R_c(b)= , no non-exact link is selected for b. PWAL treats every non-neutral link and the no-link outcome as local alternatives for each unmatched target atom. Definition 9 (PWAL). For each b∈cb _c, define c,b=∅∪ℛc(b)Z_c,b=\ \ _c(b), where ∅ denotes no active non-exact link. PWAL assigns every local outcome equal probability: πc,b(z)=1/(|ℛc(b)|+1) _c,b(z)=1/(|R_c(b)|+1) for z∈c,bz _c,b. If ℛc(b)=∅R_c(b)= , then πc,b(∅)=1 _c,b( )=1. Let c=∏b∈c,bW_c= _b _cZ_c,b. Each ωc=(zb)b∈c∈c _c=(z_b)_b _c _c activates Lcωc=zb∣zb≠∅L_c _c=\z_b z_b≠ \. Assuming target-wise independent local link choices, πc(ωc)=∏b∈cπc,b(zb)=1/Ncworld _c( _c)= _b _c _c,b(z_b)=1/N_c^world, where Ncworld=|c|=∏b∈c(|ℛc(b)|+1)N_c^world=|W_c|= _b _c(|R_c(b)|+1). Logical dependencies among target atoms remain encoded in ΦTc _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). _c^PWAL= _c= _ _c _c _c( _c) _c(L_c _c). For K∈ℕ>0K _>0 i.i.d. sampled worlds ωc(1),…,ωc(K)∼πc _c^(1),…, _c^(K) _c, it is estimated by σ^cPWAL=μ^c=K−1∑k=1Kρc(Lcωc(k)). σ_c^PWAL= μ_c=K^-1 _k=1^K _c(L_c _c^(k)). Thus, μ^c μ_c is a finite-K Monte Carlo estimator of μc _c, the expected logical resistance. NLI confidence determines the within-world clause weight w(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 gives a trace-level illustration of this mechanism. Dataset (N) Metric FH-HardSAT Top-Link PWAL PWAL w/o no-link PWAL w/o neg. guard Direct NLI α (400) Acc 11.00 36.50 49.55±0.9649.55± 0.96 46.15±0.4146.15± 0.41 49.48±0.8949.48± 0.89 57.75 Tie 55.75 27.25 2.15±0.502.15± 0.50 11.98±0.1411.98± 0.14 4.63±0.384.63± 0.38 0.00 EAcc 38.88 50.13 50.63±0.9850.63± 0.98 52.14±0.4152.14± 0.41 51.79±0.9351.79± 0.93 57.75 ARCT (444) Acc 7.43 20.05 50.90±1.1250.90± 1.12 47.77±1.2347.77± 1.23 40.59±1.1240.59± 1.12 70.05 Tie 86.71 64.86 6.87±0.416.87± 0.41 17.32±0.2017.32± 0.20 31.89±0.2831.89± 0.28 0.00 EAcc 50.79 52.48 54.34±1.0754.34± 1.07 56.43±1.1756.43± 1.17 56.53±1.1056.53± 1.10 70.05 CDED (400) Acc 34.50 62.00 73.50±0.7973.50± 0.79 71.50±0.5071.50± 0.50 69.60±0.5369.60± 0.53 80.00 Tie 49.75 13.50 2.58±0.292.58± 0.29 5.58±0.215.58± 0.21 8.23±0.258.23± 0.25 0.00 EAcc 59.38 68.75 74.79±0.7374.79± 0.73 74.29±0.5374.29± 0.53 73.71±0.5173.71± 0.51 80.00 iDebate (400) Acc 33.00 60.75 63.70±0.6563.70± 0.65 63.48±0.5663.48± 0.56 63.63±0.5363.63± 0.53 72.50 Tie 55.00 5.00 0.00±0.000.00± 0.00 0.03±0.080.03± 0.08 0.33±0.120.33± 0.12 0.00 EAcc 60.50 63.25 63.70±0.6563.70± 0.65 63.49±0.5663.49± 0.56 63.79±0.5663.79± 0.56 72.50 AAE2 (350) Acc 18.86 51.14 54.43±0.5654.43± 0.56 53.89±0.4553.89± 0.45 54.17±0.7254.17± 0.72 70.57 Tie 62.00 7.43 2.86±0.002.86± 0.00 3.74±0.093.74± 0.09 2.37±0.142.37± 0.14 0.00 EAcc 49.86 54.86 55.86±0.5655.86± 0.56 55.76±0.4455.76± 0.44 55.36±0.6955.36± 0.69 70.57 Table 1: Pairwise test results (%). PWAL variants report ten-seed means ± sample SD (K=100K=100); other methods are deterministic. Failed FH-HardSAT evaluations 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) and α (Bhagavatula et al. 2020) in their original pairwise form, and derive pairwise tasks from CDED (Rinott et al. 2015), iDebate (Wang and Ling 2016), and AAE2 (Stab and Gurevych 2017). ARCT uses Sc=(reason,warrantc)S_c=(reason,warrant_c) and Tc=(claim)T_c=(claim). α uses Sc=(O1,hypothesisc)S_c=(O_1,hypothesis_c) and Tc=(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^-)\, where Hi+H_i^+ is annotated as evidence for CiC_i, and Hi−H_i^- is a same-topic passage annotated as evidence for another claim but not annotated as evidence for CiC_i. For the two derived missing-claim tasks, let Pi=(pi,1,…,pi,ni)P_i=(p_i,1,…,p_i,n_i) denote the source statement collection paired with gold claim Ci+C_i^+. We set SA=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 claim Ci+C_i^+, and Ci−C_i^- is a different central claim from the same debate. In AAE2, PiP_i contains all premise components directly annotated as supporting Ci+C_i^+, and Ci−C_i^- is an opposite-stance claim from the same essay such that no premise in PiP_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 of Ci+C_i^+. We evaluate the full 444444-example ARCT test set, a fixed 400400-instance sample from the official α test split, fixed 400400-instance samples from the derived CDED and iDebate pools, and a fixed 350350-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 and Top-Link. Both use the same source and target formulae, exact links, NLI-derived alternatives, clause weights, and Partial MaxSAT evaluator. We additionally report FH-HardSAT, the prior neuro-symbolic method (Feng and Hunter 2026), and Direct NLI. FH-HardSAT evaluates 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 NLI uses uc=cat(Sc)u_c=cat(S_c) and vc=cat(Tc)v_c=cat(T_c), where cat(X)cat(X) concatenates the statements in X in their listed order, separated by a single space. It applies the NLI model used for atom-link construction. Let pℓ(u,v)p_ (u,v) denote the probability assigned by this model to label ℓ∈ . It scores candidate c by scNLI=pEnt(uc,vc)−pCon(uc,vc)s_c^NLI=p_Ent(u_c,v_c)-p_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 set Wmax=100W_ =100, the target-inertia weight to ϵ=1ε=1, and the main PWAL sampling budget to K=100K=100. Sampled PWAL results, including ablations and each sampling budget, use seeds 2026–2035 and are reported as means ± sample 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; Lee et al. 2022), 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; Laurer 2024), and RC2 in PySAT for Partial MaxSAT inference (Ignatiev, Morgado, and Marques-Silva 2018). In implementation, |σA−σB|≤τtie _A- _B ≤ _tie is treated as a tie, with τtie=10−12 _tie=10^-12. Metrics. Let Nwin,Nerr,NtieN_win,N_err,N_tie denote correct unique selections, errors, and valid ties, respectively, with N=Nwin+Nerr+NtieN=N_win+N_err+N_tie. A valid tie is a successful evaluation returned as Tie by this decision rule. Errors include incorrect unique selections and failed evaluations. We report Accuracy=Nwin/NAccuracy=N_win/N, TieRate=Ntie/NTieRate=N_tie/N, and EAcc=(Nwin+12Ntie)/NEAcc=(N_win+ 12N_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). Dataset Metric K=100K=100 K=200K=200 Ref. α Acc 49.55±0.9649.55± 0.96 49.92±1.1649.92± 1.16 49.7549.75 Tie 2.15±0.502.15± 0.50 1.48±0.251.48± 0.25 3.253.25 EAcc 50.63±0.9850.63± 0.98 50.66±1.1750.66± 1.17 51.3851.38 ARCT Acc 50.90±1.1250.90± 1.12 52.00±1.5952.00± 1.59 48.2048.20 Tie 6.87±0.416.87± 0.41 6.71±0.516.71± 0.51 14.4114.41 EAcc 54.34±1.0754.34± 1.07 55.36±1.4755.36± 1.47 55.4155.41 CDED Acc 73.50±0.7973.50± 0.79 73.55±0.4573.55± 0.45 74.2574.25 Tie 2.58±0.292.58± 0.29 2.28±0.302.28± 0.30 1.501.50 EAcc 74.79±0.7374.79± 0.73 74.69±0.4774.69± 0.47 75.0075.00 iDebate Acc 63.70±0.6563.70± 0.65 63.50±0.3163.50± 0.31 63.2563.25 Tie 0.00±0.000.00± 0.00 0.00±0.000.00± 0.00 0.000.00 EAcc 63.70±0.6563.70± 0.65 63.50±0.3163.50± 0.31 63.2563.25 AAE2 Acc 54.43±0.5654.43± 0.56 54.43±0.4954.43± 0.49 54.2954.29 Tie 2.86±0.002.86± 0.00 2.89±0.092.89± 0.09 2.862.86 EAcc 55.86±0.5655.86± 0.56 55.87±0.4955.87± 0.49 55.7155.71 Table 2: Sampling and exact/10510^5-capped reference results (%). Ref. denotes the exact/10510^5-capped reference. Results Main Results Table 1 reports the test results. All differences discussed below are computed from unrounded values. FH-HardSAT returns valid ties on 49.7549.75–86.71%86.71\% of examples and has lower Acc and EAcc than Top-Link and PWAL on every task. Relative to Top-Link, PWAL raises mean Acc by 2.952.95–30.8630.86 percentage points, lowers mean Tie by 4.574.57–58.0058.00 percentage points, and raises mean EAcc by 0.450.45–6.046.04 percentage points across the five tasks. On Top-Link ties, PWAL’s mean EAcc is 49.36%49.36\%–57.13%57.13\%, versus 50%50\% under uniform tie-breaking. Among Top-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 α , ARCT, and CDED, while the smaller Acc gains on iDebate and AAE2 remain uncertain. Direct NLI has the highest EAcc on every task, exceeding PWAL by 5.215.21–15.7115.71 percentage points. It is a predictive reference rather than a controlled logical comparator; PWAL and Top-Link share 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 α , 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 evaluate K∈10,20,50,100,200K∈\10,20,50,100,200\ over ten seeds. Within each seed, the smaller budgets are prefixes of the same K=200K=200 world stream. For the reference, a candidate is fully enumerated when its world count is at most 10510^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 are 357/400357/400, 443/444443/444, 216/400216/400, 146/400146/400, and 93/35093/350 for α , ARCT, CDED, iDebate, and AAE2, respectively. Every other pair contains at least one capped candidate. Table 2 reports K∈100,200K∈\100,200\ and the exact/10510^5-capped reference; the full budget grid, timing protocol, and runtime distributions are reported in the supplementary material. At K=100K=100, the across-seed standard deviation is at most 1.121.12 points for Acc, 0.500.50 for Tie, and 1.071.07 for EAcc. Increasing K from 100100 to 200200 changes mean Acc by at most 1.101.10 points and mean Tie by at most 0.680.68 points. Mean EAcc changes by at most 0.200.20 points on four tasks and by 1.021.02 points on ARCT. The K=100K=100 mean EAcc is within 1.071.07 points of the exact/10510^5-capped reference on every task, supporting K=100K=100 as a practical cost–stability setting. ARCT has the largest sampled–reference difference. The reference raises Tie from 6.87%6.87\% to 14.41%14.41\%, lowers Acc from 50.90%50.90\% to 48.20%48.20\%, and raises EAcc from 54.34%54.34\% to 55.41%55.41\%. All 6464 reference-tied ARCT pairs are fully exact, with absolute expected-resistance margins of at most 10−1210^-12. Finite-K Monte 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 the K=100K=100 mean by at most 0.750.75 points. Restricting the analysis to fully exact pairs, K=100K=100 agrees with exact marginalization on 83.02%83.02\%–98.39%98.39\% of decisions across the five tasks, averaged over ten seeds. Among K=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-K approximation. 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-Link takes 1.101.10–1.681.68 ms/example. Relative to Top-Link, the mean task-level runtime multipliers are approximately 84×84×, 172×172×, and 5.8×1035.8× 10^3 for K=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 than Top-Link. PWAL also achieves higher mean EAcc on all five tasks. Direct NLI remains 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 at https://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 A Dataset 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 candidate y∈A,By∈\A,B\. Table A.1 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 in ScS_c, TcT_c, Direct NLI input, or symbolic solver input. A.1 Pair 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 α , 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 below 0.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 below 0.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. Dataset Candidate pair (Sc,Tc)(S_c,T_c) Candidate construction Dev/Test; cluster α (Bhagavatula et al. 2020) Sc=(O1,Hc)S_c=(O_1,H_c), Tc=(O2)T_c=(O_2) The two released hypotheses are retained in their released order. 400/400; example ARCT (Habernal et al. 2018) Sc=(R,Wc)S_c=(R,W_c), Tc=(C)T_c=(C) The two released warrants are retained. 400/444; example CDED (Rinott et al. 2015) Sc=(Hc)S_c=(H_c), Tc=(C)T_c=(C) Same-topic evidence annotated as evidence for another claim but not annotated as evidence for C. 200/400; topic iDebate (Wang and Ling 2016) Sc=(P1,…,Pm)S_c=(P_1,…,P_m), Tc=(Cc)T_c=(C_c) A different central claim from the same debate. 400/400; debate AAE2 (Stab and Gurevych 2017) Sc=(P1,…,Pm)S_c=(P_1,…,P_m), Tc=(Cc)T_c=(C_c) An opposite-stance Claim from the same essay with a graph-disjoint support subtree. 200/350; essay 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); α and ARCT retain their released candidate order. Parentheses denote ordered statement collections, including singleton targets. A.2 AAE2 Graph Extraction AAE2 requires an explicit distinction between the released essay graph and the text passed to the decoder. For a gold Claim C+C^+, we retain only Premises whose outgoing relation is a direct support edge to C+C^+. Premises that support one of those Premises, components that attack C+C^+, and the support subtree of the opposite-stance Claim C−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 of C+C^+. Figure A.1 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.3 Automatic Construction Audit For the automatic checks reported in Table A.2, 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. Dataset N Clust. Split ov. Dup. Ident. Verb. CDED 400 39 0 0 0 0 iDebate 400 128 0 0 0 1 AAE2 350 127 0 0 0 0 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 most 0.170.17 percentage points and does not alter any comparison. A.4 AI-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) 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 of 47/4947/49, 49/4949/49, and 93/9993/99, respectively. Table A.3 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. Assign supported_candidate as 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 as high, medium, or low, and give one concise sentence explaining the judgment. For AAE2 only, assign opposite_stance_contrast as exactly one of: meaningful_contrast; topic_related_not_contrast; unrelated; unclear. Dataset N Only gold Both Only distractor Neither Gold or both CDED 50 39 9 0 2 48 (96%) iDebate 50 37 13 0 0 50 (100%) AAE2 100 91 3 4 2 94 (94%) 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 B Evaluation Protocol and Development Decisions B.1 Evaluation 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; Lee et al. 2022), mDeBERTa-v3 for NLI-based atom links (He, Gao, and Chen 2023; Laurer 2024), and RC2 in PySAT for Partial MaxSAT inference (Ignatiev, Morgado, and Marques-Silva 2018). FH-HardSAT additionally uses BAAI/bge-small-en-v1.5 for cosine similarity (Xiao et al. 2024). For method selection, development labels are used only for FH-HardSAT threshold selection. Separately, development labels are used to evaluate the diagnostic resistance-component sweep in Section C.3. No test label is used to choose the scoring rule, sampling budget, seed set, ablation, or reference policy. For an evaluation set of N examples, let Nwin,Nerr,NtieN_win,N_err,N_tie denote correct unique decisions, errors, and valid score ties, with N=Nwin+Nerr+NtieN=N_win+N_err+N_tie. The reported metrics are Accuracy =NwinN, = N_winN, TieRate =NtieN, = N_tieN, EAcc =Nwin+12NtieN. = N_win+ 12N_tieN. Any absolute difference of at most τtie=10−12 _tie=10^-12 between the two candidate scores is treated as a valid tie. Invalid outputs are a diagnostic subset of NerrN_err: they receive zero credit and are never relabeled as ties. B.2 FH-HardSAT Threshold Selection FH-HardSAT searches its threshold grid on the corresponding development split and applies the selected pair once to the test split. Table B.1 reports the selected thresholds and held-out test counts without repeating the main-paper metrics. Dataset τc _c τm _m Dev Acc. (%) Test W/L/TW/L/T α 90 0.55 11.50 44/133/223 ARCT 100 0.60 5.25 33/26/385 CDED 100 0.60 35.50 138/63/199 iDebate 100 0.70 29.25 132/48/220 AAE2 100 0.60 17.50 66/67/217 Table B.1: FH-HardSAT development selection and held-out test counts. τm _m is the BGE cosine-similarity threshold and τc _c the NLI contradiction-confidence threshold (in percent). Test W/L/TW/L/T gives correct unique decisions, errors, and valid ties, respectively; L includes unsuccessful evaluations. The corresponding metrics appear in the main results. Appendix C Decision Diagnostics and Components C.1 Top-Link-to-PWAL Transitions We classify each output as a correct unique decision, an incorrect unique decision, or a valid tie. Top-Link is deterministic, whereas PWAL transitions are computed separately for each of the ten K=100K=100 seeds before aggregation. Table C.1 reports PWAL EAcc over the Top-Link ties and full-test unique-to-unique repairs and damages. A tied-subset EAcc of 50%50\% is the uniform tie-breaking reference, not a significance threshold. Dataset TL ties (N)(N) PWAL EAcc on TL ties (%)(\%) Repairs (N)(N) Damages (N)(N) α 109 49.36±1.9749.36± 1.97 32.1±2.1332.1± 2.13 29.4±1.8429.4± 1.84 ARCT 288 51.82±1.4951.82± 1.49 11.7±1.1611.7± 1.16 8.7±1.778.7± 1.77 CDED 54 57.13±3.5557.13± 3.55 39.0±2.4039.0± 2.40 18.7±0.8218.7± 0.82 iDebate 20 52.50±2.6452.50± 2.64 33.9±1.9733.9± 1.97 32.6±1.3532.6± 1.35 AAE2 26 51.15±3.1751.15± 3.17 26.6±1.0726.6± 1.07 23.4±1.1723.4± 1.17 Table C.1: Top-Link-to-PWAL transition summary. Tied-subset EAcc is PWAL EAcc on the deterministic Top-Link ties. 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 ± sample 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 α , iDebate, and AAE2. C.2 Score-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 within 10−910^-9 are treated as zero. This diagnostic tolerance does not alter the candidate-score tie rule τtie=10−12 _tie=10^-12. Table C.2 reports the resulting score-component categories for all five datasets. Dataset Wrong Tension Witness Both α 193.20±4.26193.20± 4.26 31.73±1.7231.73± 1.72 15.42±2.0015.42± 2.00 52.86±2.4752.86± 2.47 ARCT 187.50±4.72187.50± 4.72 33.07±2.1733.07± 2.17 47.36±2.3347.36± 2.33 19.57±2.4519.57± 2.45 CDED 95.70±2.7595.70± 2.75 16.71±2.0716.71± 2.07 27.60±2.5327.60± 2.53 55.69±2.9055.69± 2.90 iDebate 145.20±2.62145.20± 2.62 8.73±1.238.73± 1.23 9.91±1.459.91± 1.45 81.35±1.5481.35± 1.54 AAE2 149.50±1.96149.50± 1.96 11.24±1.3111.24± 1.31 8.15±1.068.15± 1.06 80.61±1.5780.61± 1.57 Table C.2: Score-component attribution of PWAL’s incorrect unique decisions at K=100K=100. Wrong is the mean count of incorrect unique decisions; the remaining columns are mean percentages. Entries are means ± sample 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 α , CDED, iDebate, and AAE2; witness-only attribution is the largest category on ARCT. C.3 Resistance-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,ρ= TC_ -R_sat, where ΔT/Cmax T/C_ is normalized semantic tension and RsatR_sat is the target-clause witness ratio. The diagnostic sweep defines ρα=αΔTCmax−Rsat _α=α TC_ -R_sat and evaluates every α∈0,0.05,…,5α∈\0,0.05,…,5\. This development-only sweep does not tune the test score: ρα=ρ _α=ρ at α=1α=1, and all reported test results use ρ. All other settings remain fixed: Top-Link uses its single highest-confidence link configuration, while PWAL uses K=100K=100 and seeds 2026–2035. Figure C.1: Development-only diagnostic of the logical-resistance components under ρα=αΔT/Cmax−Rsat _α=α T/C_ -R_sat. Curves contain every point in the fixed grid α=0,0.05,…,5α=0,0.05,…,5. PWAL curves are ten-seed means and shaded bands show one sample standard deviation; Top-Link is deterministic. Filled markers identify the reported score ρα=ρ _α=ρ at α=1α=1. Figure C.1 shows that, across the ten dataset–method curves, the development accuracy obtained with ρ is 0.250.25–4.504.50 percentage points below the maximum observed on the grid. C.4 Component 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 ρ, 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 gives paired cluster-aware intervals. AAE2 stance diagnostic. For AAE2, PWAL EAcc is 56.41%56.41\% for For claims and 54.29%54.29\% for Against claims, averaged over seeds 2026–2035. This diagnostic was not used to select any method setting. Appendix D Sampling, Exact/10510^5-Capped Reference, and Runtime D.1 Sampling Stability For each K∈10,20,50,100,200K∈\10,20,50,100,200\, PWAL is evaluated with seeds 2026–2035. Within each seed, the smaller budgets are prefixes of the same K=200K=200 world stream. Table D.1 reports the corresponding accuracy, tie-rate, and EAcc summaries together with the fixed exact/10510^5-capped reference. Dataset K Accuracy Tie EAcc α 10 47.83 ± 1.62 5.63 ± 0.48 50.64 ± 1.68 20 49.08 ± 1.83 4.28 ± 0.59 51.21 ± 1.80 50 49.30 ± 0.86 3.18 ± 0.51 50.89 ± 0.76 100 49.55 ± 0.96 2.15 ± 0.50 50.63 ± 0.98 200 49.92 ± 1.16 1.48 ± 0.25 50.66 ± 1.17 Ref. 49.75 3.25 51.38 ARCT 10 47.52 ± 1.42 12.21 ± 0.91 53.63 ± 1.39 20 48.51 ± 1.86 9.19 ± 0.52 53.11 ± 1.79 50 49.66 ± 2.27 7.59 ± 0.51 53.46 ± 2.15 100 50.90 ± 1.12 6.87 ± 0.41 54.34 ± 1.07 200 52.00 ± 1.59 6.71 ± 0.51 55.36 ± 1.47 Ref. 48.20 14.41 55.41 CDED 10 71.53 ± 1.23 4.73 ± 0.49 73.89 ± 1.17 20 71.93 ± 1.23 4.18 ± 0.54 74.01 ± 1.31 50 72.68 ± 1.03 3.33 ± 0.37 74.34 ± 0.95 100 73.50 ± 0.79 2.58 ± 0.29 74.79 ± 0.73 200 73.55 ± 0.45 2.28 ± 0.30 74.69 ± 0.47 Ref. 74.25 1.50 75.00 iDebate 10 63.23 ± 0.58 0.15 ± 0.13 63.30 ± 0.64 20 63.73 ± 0.99 0.08 ± 0.12 63.76 ± 0.99 50 63.65 ± 1.06 0.08 ± 0.12 63.69 ± 1.04 100 63.70 ± 0.65 0.00 ± 0.00 63.70 ± 0.65 200 63.50 ± 0.31 0.00 ± 0.00 63.50 ± 0.31 Ref. 63.25 0.00 63.25 AAE2 10 53.94 ± 0.81 3.09 ± 0.23 55.49 ± 0.83 20 54.14 ± 0.93 2.97 ± 0.20 55.63 ± 0.92 50 54.51 ± 0.92 2.86 ± 0.00 55.94 ± 0.92 100 54.43 ± 0.56 2.86 ± 0.00 55.86 ± 0.56 200 54.43 ± 0.49 2.89 ± 0.09 55.87 ± 0.49 Ref. 54.29 2.86 55.71 Table D.1: PWAL stability and exact/10510^5-capped reference results. Finite-K cells are ten-seed mean percentages ± sample standard deviations in percentage points; Ref. is a fixed percentage. At K=100K=100, the across-seed accuracy standard deviation is at most 1.121.12 percentage points. Increasing K from 100 to 200 changes mean accuracy and mean tie rate by at most 1.101.10 and 0.680.68 percentage points, respectively. D.2 Reference Coverage and Approximation For candidate c with world set cW_c, let Ncworld=|c|N_c^world=|W_c|. The reference enumerates all worlds when Ncworld≤105N_c^world≤ 10^5 and otherwise draws 10510^5 worlds uniformly without replacement using seed 2026. A pair is fully exact only when both candidates are enumerated. Table D.2 reports the world-space quantities that determine exact coverage; the corresponding reference outcomes are included in Table D.1. Dataset Exact pairs Capped pairs Median P95 α 357 43 294 205,920 ARCT 443 1 42 1,848 CDED 216 184 6,210 7.47×10107.47× 10^10 iDebate 146 254 37,440 5.00×10115.00× 10^11 AAE2 93 257 170,586 5.40×10135.40× 10^13 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 and summarized in the main paper. A capped pair has at least one candidate with Ncworld>105N_c^world>10^5; P95 denotes the 95th percentile. For a dataset of N examples, let =2026,…,2035S=\2026,…,2035\ and let μ¯i,c(100)=1||∑s∈μ^i,c(100,s) μ^(100)_i,c= 1|S| _s μ^(100,s)_i,c be the ten-seed mean K=100K=100 score for example i and candidate c∈A,Bc∈\A,B\; let μi,crefμ^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)= μ^(100)_i,B- μ^(100)_i,A, m_i^ref=μ^ref_i,B-μ^ref_i,A. The candidate-score and margin mean absolute errors (MAEs) are MAEscore _score =12N∑i=1N∑c∈A,B|μ¯i,c(100)−μi,cref|, = 12N _i=1^N _c∈\A,B\ | μ^(100)_i,c-μ^ref_i,c |, MAEmargin _margin =1N∑i=1N|mi(100)−miref|. = 1N _i=1^N |m_i^(100)-m_i^ref |. Decision agreement is the percentage of examples for which the mean-score and reference evaluations return the same A/B/TieA/B/ 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 reports these two agreements together with the two errors and the per-seed attribution of sampled incorrect unique decisions. (a) Ten-seed mean-score approximation Dataset Score MAE Margin MAE Decision agr. Tie-status agr. α 0.0080 0.0117 95.25 97.25 ARCT 0.0078 0.0111 88.51 91.67 CDED 0.0069 0.0105 98.75 99.25 iDebate 0.0089 0.0122 99.00 100.00 AAE2 0.0066 0.0094 99.71 100.00 (b) Per-seed exact attribution Dataset Sample–exact decision agr. Wrong→ correct Wrong→ tie Wrong→ wrong α 89.47±1.5589.47± 1.55 6.95±2.116.95± 2.11 3.04±0.613.04± 0.61 90.02±2.3490.02± 2.34 ARCT 83.02±1.3483.02± 1.34 10.95±1.4910.95± 1.49 10.33±1.7710.33± 1.77 78.72±2.3578.72± 2.35 CDED 96.34±0.9996.34± 0.99 5.36±2.435.36± 2.43 0.56±0.900.56± 0.90 94.08±2.7694.08± 2.76 iDebate 97.67±1.2297.67± 1.22 2.78±1.982.78± 1.98 0.00±0.000.00± 0.00 97.22±1.9897.22± 1.98 AAE2 98.39±1.5498.39± 1.54 1.10±1.431.10± 1.43 0.00±0.000.00± 0.00 98.90±1.4398.90± 1.43 Table D.3: Reference diagnostics. The first block compares decisions formed from ten-seed K=100K=100 mean 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 every K=100K=100 seed separately with exact marginalization on fully exact pairs; entries are mean percentages ± sample 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 is 0.00660.0066–0.00890.0089, margin MAE is 0.00940.0094–0.01220.0122, and mean-score decision agreement is 88.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 uniform 10510^5-world estimate rather than an exact expectation. D.3 Runtime 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-K configurations use seed 2026. Timing begins from prepared logical states and excludes parsing, translation, NLI, and cache construction. Dataset Configuration Mean Median P95 α Top-Link 1.66 1.67 2.16 PWAL K=10K=10 14.58 14.37 21.71 PWAL K=20K=20 27.31 26.19 41.30 PWAL K=50K=50 68.19 66.75 101.80 PWAL K=100K=100 135.59 133.95 203.65 PWAL K=200K=200 280.89 283.08 411.32 Exact enumeration 7,608.02 354.35 33,502.77 ARCT Top-Link 1.41 1.55 1.84 PWAL K=10K=10 12.08 11.88 17.47 PWAL K=20K=20 25.92 24.83 34.25 PWAL K=50K=50 61.86 63.11 85.55 PWAL K=100K=100 120.22 119.82 170.60 PWAL K=200K=200 250.90 260.40 333.48 Exact enumeration 526.31 53.88 1,694.38 CDED Top-Link 1.68 1.66 2.28 PWAL K=10K=10 14.63 15.35 20.15 PWAL K=20K=20 25.43 25.16 36.28 PWAL K=50K=50 62.11 61.03 89.96 PWAL K=100K=100 126.53 126.21 175.92 PWAL K=200K=200 262.79 267.03 379.23 Exact enumeration 12,873.73 1,792.32 61,171.62 iDebate Top-Link 1.57 1.48 2.22 PWAL K=10K=10 15.38 13.99 23.13 PWAL K=20K=20 30.79 28.66 46.39 PWAL K=50K=50 72.23 67.55 101.76 PWAL K=100K=100 142.47 141.32 203.66 PWAL K=200K=200 289.34 278.08 386.68 Exact enumeration 14,764.91 5,567.09 78,545.72 AAE2 Top-Link 1.10 1.06 1.56 PWAL K=10K=10 9.51 8.53 13.45 PWAL K=20K=20 19.60 17.38 33.37 PWAL K=50K=50 48.49 42.07 81.37 PWAL K=100K=100 94.04 85.63 145.66 PWAL K=200K=200 188.33 165.96 283.57 Exact enumeration 7,886.06 1,823.10 24,037.05 Table D.4: Controlled logical-scoring runtime on 20 fully enumerable pairs per dataset (ms/example). P95 denotes the 95th percentile. Table D.4 shows that mean K=100K=100 runtime is 94.0494.04–142.47142.47 ms per example, compared with 1.101.10–1.681.68 ms for Top-Link. K=200K=200 approximately doubles the K=100K=100 runtime, while exact enumeration requires 526.31526.31–14,764.9114,764.91 ms on the same pairs. Appendix E Paired and Clustered Statistical Inference (a) Main-method contrasts Dataset Contrast Δ [95% CI] Δ [95% CI] Tie reduction [95% CI] α PWAL −- Direct NLI -8.20 [-14.52, -1.60]† -7.12 [-13.46, -0.57]† -2.15 [-3.38, -1.10]† α PWAL −- Top-Link +13.05 [+8.45, +17.68]† +0.50 [-3.70, +4.69] +25.10 [+21.00, +29.38]† α PWAL −- FH-HardSAT +38.55 [+33.27, +43.85]† +11.75 [+6.41, +17.14]† +53.60 [+48.62, +58.67]† ARCT PWAL −- Direct NLI -19.14 [-25.18, -13.11]† -15.71 [-21.69, -9.90]† -6.87 [-9.14, -4.73]† ARCT PWAL −- Top-Link +30.86 [+26.80, +34.91]† +1.86 [-1.58, +5.24] +58.00 [+53.33, +62.50]† ARCT PWAL −- FH-HardSAT +43.47 [+38.81, +48.18]† +3.55 [-0.72, +7.92] +79.84 [+75.90, +83.58]† CDED PWAL −- Direct NLI -6.50 [-11.35, -1.78]† -5.21 [-9.99, -0.51]† -2.57 [-4.12, -1.21]† CDED PWAL −- Top-Link +11.50 [+7.70, +15.45]† +6.04 [+2.28, +9.94]† +10.93 [+7.45, +14.67]† CDED PWAL −- FH-HardSAT +39.00 [+32.45, +45.01]† +15.41 [+9.99, +20.58]† +47.17 [+42.48, +51.99]† iDebate PWAL −- Direct NLI -8.80 [-13.76, -3.95]† -8.80 [-13.76, -3.95]† +0.00 [+0.00, +0.00] iDebate PWAL −- Top-Link +2.95 [-1.15, +6.94] +0.45 [-3.55, +4.32] +5.00 [+2.77, +7.48]† iDebate PWAL −- FH-HardSAT +30.70 [+25.64, +35.66]† +3.20 [-1.17, +7.40] +55.00 [+49.88, +59.90]† AAE2 PWAL −- Direct NLI -16.14 [-22.96, -9.40]† -14.71 [-21.36, -8.16]† -2.86 [-4.58, -1.22]† AAE2 PWAL −- Top-Link +3.29 [-0.38, +6.99] +1.00 [-2.54, +4.54] +4.57 [+2.51, +6.92]† AAE2 PWAL −- FH-HardSAT +35.57 [+29.70, +41.43]† +6.00 [+0.64, +11.22]† +59.14 [+53.42, +64.86]† (b) Component contrasts Dataset Contrast Δ [95% CI] Δ [95% CI] Tie reduction [95% CI] α Full −- w/o no-link +3.40 [+0.85, +6.02]† -1.51 [-3.91, +0.85] +9.83 [+7.07, +12.70]† α Full −- w/o negative guard +0.07 [-1.03, +1.20] -1.16 [-2.26, -0.15]† +2.48 [+1.15, +4.08]† ARCT Full −- w/o no-link +3.13 [+0.99, +5.36]† -2.09 [-3.95, -0.24]† +10.45 [+7.79, +13.33]† ARCT Full −- w/o negative guard +10.32 [+6.98, +13.67]† -2.20 [-4.97, +0.54] +25.02 [+21.15, +29.05]† CDED Full −- w/o no-link +2.00 [+0.08, +4.00]† +0.50 [-1.15, +2.14] +3.00 [+1.46, +4.84]† CDED Full −- w/o negative guard +3.90 [+1.73, +6.17]† +1.07 [-0.23, +2.25] +5.65 [+2.98, +8.64]† iDebate Full −- w/o no-link +0.22 [-0.75, +1.21] +0.21 [-0.77, +1.19] +0.03 [+0.00, +0.15] iDebate Full −- w/o negative guard +0.07 [-0.78, +0.95] -0.09 [-1.01, +0.81] +0.33 [+0.00, +0.97] AAE2 Full −- w/o no-link +0.54 [-1.26, +2.38] +0.10 [-1.59, +1.79] +0.89 [+0.00, +1.97] AAE2 Full −- w/o negative guard +0.26 [-1.37, +2.08] +0.50 [-0.91, +2.05] -0.49 [-2.17, +1.18] Table E.1: Paired two-way bootstrap contrasts in percentage points. Brackets are pointwise two-sided 95% bootstrap percentile intervals; † marks an interval that excludes zero. The contrasts in Table E.1 use the following bootstrap protocol. Each reported point estimate averages per-example utility over the ten complete K=100K=100 seed 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 α 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 to Top-Link excludes zero on α , ARCT, and CDED but includes zero on iDebate and AAE2. For component contrasts, the no-link accuracy interval excludes zero on α , ARCT, and CDED, while the negative-guard interval excludes zero on ARCT and CDED. Appendix F Translator Specification F.1 AMR-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), PropBank for numbered semantic roles (Kingsbury and Palmer 2002), and the open-source Penman library for PENMAN decoding (Goodman 2020). Given one statement x, 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; parser multi-sentence branches are compiled conjunctively. Definition F.1 (AMR Translator Output). Fix an AMR parser configuration ϑ , and let AMRϑT_AMR be the resulting partial translator. The parser and decoder first convert x into 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,…,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⟩. F_x= _x, ( (a_x,i), _x(a_x,i),v_x(a_x,i) )_i=1^n_x . Let x=ax,1,…,ax,nxA_x=\a_x,1,…,a_x,n_x\ denote the corresponding active atom set. Here Φx _x is the emitted formula abstract syntax tree (AST), θx(a) _x(a) is the structured atom expression, and vx(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 _x, not inserted into vx(a)v_x(a). The downstream surface adapter strips surrounding whitespace from vx(a)v_x(a) and appends the string ., yielding the main-paper surface x(a)V_x(a). This formatting step is outside AMRϑT_AMR . The solver-facing representation used in the main paper is therefore (x)=⟨x,Φx,x⟩. Rep(x)= _x, _x,V_x . If parsing, AMR decoding, compilation, or output validation fails, AMRϑ(x)T_AMR (x) is undefined; no fallback output is substituted. Example F.1 (Running translator input). For x=A careful student reads a bookx=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 symbols aia_i used below are expository labels and need not match emitted xii identifiers or their order. F.2 Records, Atoms, and Verbalizations Definition F.2 (Normalized AMR Records and Endpoint Descriptors). Write the normalized graph for statement x as Gx=(x,ℰxN,ℰxL,cx,tx),G_x=(N_x,E_x^N,E_x^L,c_x,t_x), where xN_x is the node set, ℰxNE_x^N contains node-valued role records, ℰxLE_x^L contains literal-valued attribute records, cxc_x maps nodes to concepts, and txt_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⨄ℰxLE_x=E_x^N _x^L, where ⨄ denotes disjoint union. Normalization deterministically partitions the records as ℰx=ℰxsem⨄ℰxstr⨄ℰxmeta.E_x=E_x^sem _x^str _x^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 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 :mode case; 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, _x(u)= cases _x^N(u),&u _x,\\ _x^L(u),&u is a literal, cases where δxN(u) _x^N(u) =NodeDesc(cx(u),Namex(u),mx(u)), =NodeDesc\! (c_x(u),Name_x(u),m_x(u) ), δxL(u) _x^L(u) =LitDesc(raw(u),val(u),type(u)). =LitDesc\! (raw(u),val(u),type(u) ). Here Namex(u)Name_x(u) is the normalized name, if present. In the descriptor for u, the direct metadata list mx(u)m_x(u) excludes :name, name-part, and :wiki records; node-valued metadata targets are serialized recursively. The normalized name is already represented by Namex(u)Name_x(u), while direct :wiki metadata 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 _x. AMR record Compiler action Formula effect and/or with :opii ordered branch traversal ∧ / ∨ multi-sentence with :sntii or :rel ordered sentence traversal ∧ :polarity - local scope marker ¬ :condition antecedent edge → :name, :quant, :unit, and date/value fields endpoint identity or lexical realization no separate atom :wiki construction-only metadata no separate atom 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, the role occurrences :ARG0(r,s), :ARG1(r,b), and :mod(s,c) belong to ℰxsemE_x^sem. There is no connective or scope record, so ℰxstr=∅E_x^str= . If the book node additionally contained :quant 1, that occurrence would belong to ℰxmetaE_x^meta: it would refine δx(b) _x(b) without becoming an independent proposition. Active Atoms The concrete AMR role labels r,ra,rbr,r_a,r_b below instantiate the main-paper role parameters κ,κa,κbκ, _a, _b, respectively; the predicate occurrence p corresponds to e in 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, :r,u), where u may be a node or literal, the compiler first creates the role-aware dyadic record Dyar(δx(p),δx(u)).Dya_r ( _x(p), _x(u) ). 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 occurrence p. Let comp= _comp=\ ARG0,…,ARG4, ARG0,…, ARG4, accompanier,beneficiary,cause, accompanier, beneficiary, cause, destination,direction,duration, destination, direction, duration, extent,instrument,location, extent, instrument, location, manner,medium,path, manner, medium, path, purpose,source,time,topic. purpose, source, time, topic\. Among the core roles present on p, the compiler chooses the first available anchor in the fixed order ARG0,…,ARG4 ARG0,…, ARG4. If (p,:ra,u)(p, :r_a,u) is the anchor edge and (p,:rb,v)(p, :r_b,v) is another edge with rb∈compr_b _comp, they produce Trira,rb(δx(u),δx(p),δx(v)).Tri_r_a,r_b ( _x(u), _x(p), _x(v) ). This triple records that, in one occurrence of predicate p, endpoints u and v fill roles rar_a and rbr_b. When ARG0 is absent, a later core role can anchor the event; in particular, ARG1+ARG2 is legal. Cross-event paths are never merged. For each non-anchor role rb∈compr_b _comp, the compiler forms a separate triple with the selected anchor role. An event with ARG0, ARG1, and ARG2 yields TriARG0,ARG1Tri_ARG0,ARG1 and TriARG0,ARG2Tri_ARG0,ARG2; when ARG0 is available, the compiler does not additionally form an ARG1+ARG2 triple. 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 xrecD_x^rec be the dyadic-record inventory, let x⊆xrecC_x _x^rec contain the component dyads consumed by successful same-event composition, and let atomD(d)atom_D(d) denote the dyadic proposition represented by record d. The provisional active inventory is ~x=~xU⨄~xD⨄~xT⨄~xO, A_x= A_x^U A_x^D A_x^T A_x^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 :mode case described above. Consumed dyads satisfy atomD(d):d∈x∩~x=∅.\atom_D(d):d _x\∩ A_x= . 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, the same-event records :ARG0(r,s) and :ARG1(r,b) compose into a1=TriARG0,ARG1(student,read-01,book).a_1=Tri_ARG0,ARG1(student,read-01,book). For readability, examples abbreviate typed endpoint descriptors by their lexical heads; the compiler retains the full δx _x values. The modifier is not part of the event-role pair and remains a2=Dyamod(student,careful).a_2=Dya_mod(student,careful). Thus ~x=a1,a2 A_x=\a_1,a_2\. The ARG0 and ARG1 dyads 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 atom a, θx(a) _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)),key_x(a)=Canon\! ( _x(a) ), where CanonCanon is a deterministic serialization independent of parser variable names. In contrast, provx(a)⊆ℰxprov_x(a) _x records the graph records used to construct a, and ownerx(a)∈xowner_x(a) _x is the graph node whose local formula body contains the leaf for a. Metadata may affect θx(a) _x(a) or vx(a)v_x(a) without appearing in provx(a)prov_x(a); unary carriers may have empty provenance. These fields are compiler-internal and are distinct from the emitted verbalization vx(a)v_x(a). For a dyad Dyar(c,d)Dya_r(c,d) and a triple Trira,rb(c,p,d)Tri_r_a,r_b(c,p,d), let C=ℓ(c)C= (c), P=ℓ(p)P= (p), and D=ℓ(d)D= (d). The deterministic unsigned lexical form ℓ removes a predicate-sense suffix and realizes names, quantities, and descriptor metadata from the AMR payload; it never consults the original sentence. For an endpoint descriptor z and numbered role r, the resolver χ(z,r)χ(z,r) consults the predicate-sense entry stored in z and returns a semantic relation class from the pinned PropBank roleset, or ⊥ when the roleset or role is unavailable or unresolved. Non-numbered roles are realized directly from their AMR role labels. Write vDrv_D^r and vTra,rbv_T^r_a,r_b for the base verbalizations of the corresponding dyad and triple. Subscripts DD and TT denote dyadic and triple forms, respectively. Let D Lex^D and T Lex^T denote the fixed dyadic and triple realization maps specified below. Then relD _D =χ(c,r), =χ(c,r), relT _T =χ(p,rb), =χ(p,r_b), sigD _D =(r,relD), =(r,rel_D), sigT _T =(ra,rb,relT), =(r_a,r_b,rel_T), fDr(c,d) f_D^r(c,d) =norm(DC),r=ARG0,norm(CD),otherwise, = casesnorm(D\ C),&r= ARG0,\\ norm(C\ D),&otherwise, cases fT(c,p,d) f_T(c,p,d) =norm(CPD), =norm(C\ P\ D), vDr(c,d) v_D^r(c,d) =sigDD(C,D), = Lex^D_sig_D(C,D), vTra,rb(c,p,d) v_T^r_a,r_b(c,p,d) =sigTT(C,P,D). = Lex^T_sig_T(C,P,D). Here normnorm joins nonempty lexical fields with single spaces. If the relevant resolver output is ⊥ , or a supported join has no resolved relation template, D Lex^D returns the ordered fallback fDrf_D^r, and T Lex^T returns fTf_T. An opaque atom uses the dyadic template for its retained role. For a unary carrier with concept c, lexical form C=ℓ(c)C= (c), and optional quantity ν, define U(C,c,ν)=Coccurs,c is sense-tagged,Cexist,ν is present and ν≠1,Cexists,otherwise. Lex^U(C;c,ν)= casesC\ occurs,&c is sense-tagged,\\ C\ exist,&ν is present and ν≠ 1,\\ C\ exists,&otherwise. 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, F.3, and F.4 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 only vxv_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, p(⋅)p(·) is the fixed rule-based past-participle inflector. Surface realization leaves θx _x, keyxkey_x, ownerxowner_x, provxprov_x, and the formula abstract syntax tree unchanged. Negation is carried by Φx _x and is never inserted into the verbalization. Example F.4 (Atom identity and verbalization). For the atoms in Example F.3, the structured representation of a1a_1 retains the predicate sense, role pair, and endpoint descriptors, while its verbalization omits the sense suffix: θx(a1) _x(a_1) =TriARG0,ARG1(student,read-01,book), =Tri_ARG0,ARG1(student,read-01,book), keyx(a1) _x(a_1) =Canon(θx(a1)), =Canon\! ( _x(a_1) ), vx(a1) v_x(a_1) =“student read book”, =``student read book′, vx(a2) v_x(a_2) =“careful student”. =``careful student′. Thus the structured expression preserves read-01, whereas the verbalization uses read. Formula construction yields Φx=a1∧a2 _x=a_1 a_2. (a) PropBank function-tag resolution PropBank tag Resolved relation class PAG, CAU, SRC, EXT, PRP, TMP agent, cause, source, extent, purpose, and time, respectively PPT refine to agent, property, instrument, accompaniment, path, source, location, topic, extent, attribute, active theme, or state; otherwise patient GOL refine to beneficiary, result, location, or instrument; otherwise goal LOC distinguish path, source, and goal; otherwise location DIR distinguish patient, source, goal, path, location, and beneficiary; otherwise direction MNR refine to instrument or accompaniment; otherwise manner COM distinguish opponent and companion PRD patient for ARG1; result otherwise unavailable, missing, VSP, or unrecognized return ⊥ and use the ordered fallback (b) Numbered-role surface templates Resolved relation class v(Dyar(c,d))v(Dya_r(c,d)) agent; active theme DCD\ C patient Disp(C)D\ is\ p(C) goal Cis directed toDC\ is directed to\ D location Coccurs atDC\ occurs at\ D path Coccurs alongDC\ occurs along\ D direction Cproceeds towardDC\ proceeds toward\ D source Coriginates fromDC\ originates from\ D instrument CusesDC\ uses\ D manner Coccurs byDC\ occurs by\ D companion; accompaniment Coccurs withDC\ occurs with\ D opponent Coccurs againstDC\ occurs against\ D beneficiary; purpose Cis forDC\ is for\ D result Cresults inDC\ results in\ D extent Chas extentDC\ has extent\ D cause Cis caused byDC\ is caused by\ D topic Cis aboutDC\ is about\ D time Coccurs duringDC\ occurs during\ D property DisCD\ is\ C state Dis in stateCD\ is in state\ C attribute Chas attributeDC\ has attribute\ D unresolved fDrf_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. Here C is the predicate surface and D is the argument surface. Relation classes that share a row use the same template. AMR role or atom kind Verbalization template purpose, beneficiary Cis forDC\ is for\ D time, location Coccurs atDC\ occurs at\ D direction Cproceeds towardDC\ proceeds toward\ D domain DisCD\ is\ C mod DCD\ C manner Coccurs in mannerDC\ occurs in manner\ D poss D’sCD's\ C poss-of C’sDC's\ D topic Cis aboutDC\ is about\ D part, subevent-of Dis part ofCD\ is part of\ C part-of, subevent Cis part ofDC\ is part of\ D consist Dconsists ofCD\ consists of\ C consist-of Cconsists ofDC\ consists of\ D location-of Doccurs atCD\ occurs at\ C dayperiod Coccurs duringDC\ occurs during\ D destination Cproceeds toDC\ proceeds to\ D source Coriginates fromDC\ originates from\ D instrument CusesDC\ uses\ D accompanier Coccurs withDC\ occurs with\ D path Cproceeds alongDC\ proceeds along\ D medium Coccurs viaDC\ occurs via\ D cause Cis caused byDC\ is caused by\ D concession Coccurs despiteDC\ occurs despite\ D duration Clasts forDC\ lasts for\ D degree, age Chas degreeDC\ has degree\ D; Chas ageDC\ has age\ D frequency Chas frequencyDC\ has frequency\ D extent, example Chas extentDC\ has extent\ D; Chas exampleDC\ has example\ D :prep-q CqDC\ q\ D :opii CDC\ D special mode ChasDmodeC\ has\ D\ mode other non-numbered role fDrf_D^r unary predicate / entity CoccursC\ occurs / CexistsC\ exists (exist when ν≠1ν≠ 1) Table F.3: Surface templates for non-numbered dyads and unary carriers. For :prep-q, q is the role suffix with hyphens replaced by spaces. Join or resolved relation class v(Trira,rb(c,p,d))v(Tri_r_a,r_b(c,p,d)) ARG0+ARG1 CPDC\ P\ D accompanier; beneficiary/purpose CPwithDC\ P\ with\ D; CPforDC\ P\ for\ D cause; destination; direction CPbecause ofDC\ P\ because of\ D; CPtoDC\ P\ to\ D; CPtowardDC\ P\ toward\ D duration; extent CPforDC\ P\ for\ D; CPbyDC\ P\ by\ D instrument; location; manner CPusingDC\ P\ using\ D; CPatDC\ P\ at\ D; CPbyDC\ P\ by\ D medium; path; source CPviaDC\ P\ via\ D; CPalongDC\ P\ along\ D; CPfromDC\ P\ from\ D time; topic CPduringDC\ P\ during\ D; CPaboutDC\ P\ about\ D goal; location; path; direction; source CPto/at/along/toward/fromDC\ P\ to/at/along/toward/from\ D instrument; manner CPusing/byDC\ P\ using/by\ D companion or accompaniment; opponent CPwith/againstDC\ P\ with/against\ D beneficiary or purpose; result CPforDC\ P\ for\ D; CPDC\ P\ D extent; cause; topic; time CPby/because of/about/duringDC\ P\ by/because of/about/during\ D property, state, or attribute CPasDC\ P\ as\ D agent, patient, or active theme as a secondary role fTf_T unresolved numbered role or unsupported join fTf_T 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. Here C, P, and D are 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.3 Formula Construction, Polarity, and Validation Definition F.5 (Recursive Formula Construction). For specification, let x=(ownerx,Chx,Opx,Condx,x0) Trav_x=(owner_x,Ch_x,Op_x,Cond_x,Q_x^0) summarize the compiler’s formula traversal. Here ownerxowner_x assigns every provisional atom to one formula owner; Chx(v)Ch_x(v) is the ordered list of semantic children reached from v through normalized forward or inverse-tree records; Opx(v)Op_x(v) contains ordered connective branches; and Condx(v)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 x0Q_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 xcovQ_x^cov. Coverage continues until every provisional atom is represented; failure to add a new leaf is an invalid translation. Let x=x0⨄xcov.Q_x=Q_x^0 _x^cov. For a provisional atom a, let id(a)id(a) be its assigned identifier. For a formula φ , let LeafIds(φ)LeafIds( ) be the set of identifiers on its atom leaves. For node v, let Localx(v)Local_x(v) be the conjunction of provisional atoms owned by v, and define H(v)=⋀u∈Chx(v)F(u),B0(v)=Localx(v)∧H(v).H(v)= _u _x(v)F(u), B_0(v)=Local_x(v) H(v). We take ⋀∅=⊤ = and ⋁∅=⊥ = . Let ∧=and,multi-sentenceC_ =\ and, multi-sentence\. For a connective node with ordered branch roots uiu_i, define Connx(v)=⋀iF(ui),cx(v)∈∧,⋁iF(ui),cx(v)=or.Conn_x(v)= cases _iF(u_i),&c_x(v) _ ,\\ _iF(u_i),&c_x(v)= or. cases The targets uiu_i arise from :opii, :sntii, or a multi-sentence :rel edge. The local body is B(v)=B0(v)∧Connx(v),Connx(v) is defined,B0(v),otherwise.B(v)= casesB_0(v) _x(v),&Conn_x(v) is defined,\\ B_0(v),&otherwise. cases Node polarity is applied first: N(v)=¬B(v),v has :polarity -,B(v),otherwise,N(v)= cases B(v),&v has :polarity -,\\ B(v),&otherwise, cases Conditions are then applied to the resulting local body. If Condx(v)=q1,…,qkCond_x(v)=\q_1,…,q_k\, define F(v)=(⋀jF(qj))→N(v),Condx(v)≠∅,N(v),otherwise.F(v)= cases ( _jF(q_j) )→ N(v),&Cond_x(v)≠ ,\\ N(v),&otherwise. 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). _x^0= _q _xF(q). Coverage-root construction guarantees LeafIds(Φx0)=id(a):a∈~x.LeafIds( _x^0)=\id(a):a∈ A_x\. Example F.5 (Coordination and condition). Suppose the parser represents The committee chooses tea, or both coffee and cake with an outer or branch whose second child is an and. Let at,ac,aka_t,a_c,a_k denote the three same-event choice atoms. Then Definition F.5 gives Φx=at∨(ac∧ak). _x=a_t (a_c a_k). For go-01 :ARG0 child :condition rain-01, let aga_g be the ARG0 dyad for the going event and ara_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 _x=a_r→ a_g. Polarity, Branch Isolation, and Validation Definition F.6 (Participant-Local Polarity). Node polarity on an event or proposition is handled by N(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.P_x= \id(a)\ |\ array[]la∈ A_x^D∪ A_x^T,\\ a contains an explicitly negative\\ participant endpoint array \. For parity bit b∈0,1b∈\0,1\, define Πx _P_x recursively by Πx(a,b) _P_x(a;b) =¬a,id(a)∈x and b=0,a,otherwise, = cases a,&id(a) _x and b=0,\\ a,&otherwise, cases Πx(¬φ,b) _P_x( ;b) =¬Πx(φ,1−b), = _P_x( ;1-b), Πx(○i=1kφi;b) _P_x ( _i=1^k _i;b ) =○i=1kΠx(φi;b),○∈∧,∨, = _i=1^k _P_x( _i;b), ∈\ , \, Πx(φ→ψ;b) _P_x( →ψ;b) =Πx(φ,b)→Πx(ψ,b). = _P_x( ;b)→ _P_x(ψ;b). Constants are unchanged. Let Φ~x=Πx(Φx0,0) _x= _P_x( _x^0;0) be the formula before release finalization. The emitted formula and atom inventory are Φx _x =ConstNorm(Φ~x), =ConstNorm( _x), x _x =a∈~x:id(a)∈LeafIds(Φx). = \a∈ A_x:id(a) ( _x) \. Here ConstNormConstNorm applies the usual truth-preserving identities for ⊤ , ⊥ , 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). For The teacher did not give the student a book, the event has ARG0, ARG1, ARG2, and :polarity -. Its two active atoms are g1 g_1 =TriARG0,ARG1(teacher,give-01,book), =Tri_ARG0,ARG1(teacher,give-01,book), g2 g_2 =TriARG0,ARG2(teacher,give-01,student). =Tri_ARG0,ARG2(teacher,give-01,student). Event polarity preserves their shared parser scope: Φx=¬(g1∧g2), _x= (g_1 g_2), not (¬g1)∧(¬g2)( g_1) ( g_2). By contrast, polarity on an explicit participant is projected locally to each relation atom containing that participant. For an AMR containing play-01 :ARG0 (child :polarity -) :location statue, the output is the single atom p1p_1, with vx(p1)=“child play at statue”v_x(p_1)=``child play at statue′, under formula ¬p1 p_1. This participant-only projection does not change the atom owner, negate the predicate, apply De Morgan’s law, or alter the surrounding and/or branch. Definition F.7 (Branch Isolation). When compiling one explicit and/or branch, 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 only atom, not, and, or, and implies. A not node has one argument, an and or or node has at least two arguments, and an implies node has an antecedent and a consequent. The formula must satisfy LeafIds(Φx)=id(a):a∈x.LeafIds( _x)=\id(a):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 represents The student reads a book and writes an essay with a shared student node reentered by both event branches. Branch-local ownership then yields TriARG0,ARG1(student,read-01,book) _ARG0,ARG1(student,read-01,book) ∧TriARG0,ARG1(student,write-01,essay). _ARG0,ARG1(student,write-01,essay). Appendix G Detailed Calculation for the Constructed Example Throughout Sections G–I, candidate and active-link-set subscripts are suppressed when unambiguous. We use the fixed main-paper settings Wmax=100W_ =100 and ϵ=1ε=1. Here MbaseM^base and MforcedM^forced are the assignments returned by solving the base and target-forced MaxSAT instances, and SemCostSemCost sums the weights of violated atom-link clauses in Ωsem ^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 by Top-Link and PWAL. (a) Fixed translations and atom meanings. ΦP _P =g, =g, ΦA _A =a1∧a2, =a_1 a_2, ΦSA _S_A =g∧a1∧a2, =g a_1 a_2, ΦTA _T_A =ΦTB=b, = _T_B=b, ΦB _B =d1∧d2, =d_1 d_2, ΦSB _S_B =g∧d1∧d2. =g d_1 d_2. g: door is unlocked; a1,d1a_1,d_1: Maya enter office; a2a_2: Maya remain at office; d2d_2: Maya leave office; b: Maya present at office. (b) NLI outputs and induced semantic clauses. The retained alternatives are A: A: a1→b(Ent,p=0.989,w=98), a_1\!→ b\;( Ent,p=0.989,w=98), a2→b(Ent,p=0.995,w=99); a_2\!→ b\;( Ent,p=0.995,w=99); B: B: d1→b(Ent,p=0.989,w=98), d_1\!→ b\;( Ent,p=0.989,w=98), d2→b(Con,p=0.668,w=66). d_2\!→ b\;( Con,p=0.668,w=66). They induce the weighted clauses [¬a1∨b]98,[¬a2∨b]99,[¬d1∨b]98,[¬d2∨¬b]66. gathered [ a_1 b ]_98, [ a_2 b ]_99,\\ [ d_1 b ]_98, [ d_2 b ]_66. gathered The shared comparison g→bg\!→ b is neutral with confidence 0.9820.982 and is discarded. Each candidate has one unmatched target atom and two non-neutral alternatives. PWAL therefore assigns probability 1/31/3 to no-link and to each listed candidate-specific link. Confidence determines w(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ε=1, all displayed semantic-link weights exceed the inertia weight. The resistance score is ΔT T =SemCost(Mforced) =SemCost(M^forced) −SemCost(Mbase), -SemCost(M^base), ρ ρ =ΔTCmax−Rsat. = TC_ -R_sat. In the no-link case, the base and forced values of b are false and true, and both semantic costs are zero. Under entailment they are both true and both costs are zero. Under a contradiction of weight w, they are false and true, so the costs are 00 and w. Consequently, OutcomeΔT/CmaxRsatρNo-link000Entailment01−1Contradiction101 array[]lccc & T/C_ &R_sat&ρ\\ -link&0&0&0\\ Entailment&0&1&-1\\ Contradiction&1&0&1\\ array In the no-link row, Cmax=|T|Wmax=100C_ =|A_T|W_ =100 is the zero-link fallback. Inertia affects the two optima but is excluded from SemCostSemCost. (d) Instantiated worlds and pairwise decision. For each world ω, report the score tuple (ω)=(ΔT,Cmax,Rsat,ρ)s(ω)=( T,C_ ,R_sat,ρ). The complete world spaces, with probability 1/31/3 per world, are A: A: (ωA0)=(0,100,0,0), ( _A0)=(0,100,0,0), (ωA1)=(0,98,1,−1),(ωA2)=(0,99,1,−1); ( _A1)=(0,98,1,-1), ( _A2)=(0,99,1,-1); B: B: (ωB0)=(0,100,0,0), ( _B0)=(0,100,0,0), (ωB1)=(0,98,1,−1),(ωB2)=(66,66,0,1). ( _B1)=(0,98,1,-1), ( _B2)=(66,66,0,1). The ωA1,ωA2,ωB1,ωB2 _A1, _A2, _B1, _B2 worlds activate a1→ba_1\!→ b, a2→ba_2\!→ b, d1→bd_1\!→ b, and d2→bd_2\!→ b, respectively. Aggregation gives Top-Link: Top-Link: LAtop=a2→b, L_A^top=\a_2\!→ b\, LBtop=d1→b, L_B^top=\d_1\!→ b\, σAtop=σBtop=−1⟹Tie; _A^top= _B^top=-1 ; PWAL: : μA=13(0−1−1)=−23, _A= 13(0-1-1)=- 23, μB=13(0−1+1)=0, _B= 13(0-1+1)=0, μA<μB⟹Candidate A. _A< _B A. Appendix H Detailed ARCT Success Trace In this fully enumerable ARCT instance, Top-Link ties, 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–H.4 report the input, retained links, and complete world aggregation. (a) Input, fixed translations, and atom meanings. Premise People learn a lot from comment sections. Candidate A too much learning hurts Candidate B learning never hurts Claim Comment sections have not failed Table H.1: ARCT success trace. Candidate B is gold. The compiler produces ΦSA _S_A =a1∧a2∧a3∧a4∧a5∧a6, =a_1 a_2 a_3 a_4 a_5 a_6, ΦSB _S_B =b1∧b2∧b3∧¬b4, =b_1 b_2 b_3 b_4, ΦT _T =¬f∨¬c. = f c. The atom surfaces below are reproduced verbatim from the translator output and were not manually edited. The atom inventory is a1,b1 a_1,b_1 :comment section, :\ comment section, a2,b2 a_2,b_2 :person learn lot, :\ person learn lot, a3,b3 a_3,b_3 :person learn toward section, :\ person learn toward section, a4 a_4 :learn hurt,a5:hurt much,a6:hurt too, :\ learn hurt, a_5:\ hurt much, a_6:\ hurt too, b4 b_4 :learn hurt during ever, :\ learn hurt during ever, f f :section fail,c:comment section. :\ section fail, c:\ comment section. The negative literal ¬b4 b_4 is the compiled meaning of “learning never hurts.” Exact surface matching supplies the deterministic semantic links a1↔ca_1 c and b1↔cb_1 c, each with fixed exact-link weight 100. Consequently only the unmatched target atom f is sampled. (b) NLI outputs, clause weights, and local outcomes. For an NLI confidence p, the solver uses w(p)=max1,⌊100p⌋w(p)= \1, 100p \. Entailment induces [¬s∨f]w(p)[ s f]_w(p), whereas contradiction induces [¬s∨¬f]w(p)[ s f]_w(p). Candidate Link Source surface Label p w(p)w(p) Soft clause A a1→fa_1\!→ f comment section Con 0.848 84 [¬a1∨¬f]84[ a_1 f]_84 A a2→fa_2\!→ f person learn lot Con 0.982 98 [¬a2∨¬f]98[ a_2 f]_98 A a3→fa_3\!→ f person learn toward section Con 0.971 97 [¬a3∨¬f]97[ a_3 f]_97 A a5→fa_5\!→ f hurt much Ent 0.421 42 [¬a5∨f]42[ a_5 f]_42 B b1→fb_1\!→ f comment section Con 0.848 84 [¬b1∨¬f]84[ b_1 f]_84 B b2→fb_2\!→ f person learn lot Con 0.982 98 [¬b2∨¬f]98[ b_2 f]_98 B b3→fb_3\!→ f person learn toward section Con 0.971 97 [¬b3∨¬f]97[ b_3 f]_97 B b4→fb_4\!→ f learn hurt during ever Ent 0.587 58 [¬b4∨f]58[ b_4 f]_58 Table H.2: All retained candidate-specific NLI links. Each candidate’s five local outcomes—the four displayed links and no-link—have probability 1/51/5. Notice that the final B-link is built on the unsigned base atom b4b_4, while the source formula hard-enforces ¬b4 b_4. Its implication is therefore satisfied through ¬b4 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 _T is hard only in the forced instance. Unit target inertia participates in optimization but is excluded from semantic cost. For each world, ΔT T =SemCost(Mforced) =SemCost(M^forced) −SemCost(Mbase), -SemCost(M^base), ρ ρ =ΔTCmax−Rsat. = TC_ -R_sat. The exact match contributes 100 to CmaxC_ ; an active NLI link contributes its weight. With no active NLI link, Cmax=100C_ =100. The exact link makes c true in the base optimum. An active contradiction link also supports ¬f f, thereby witnessing the sole target clause ¬f∨¬c f c and giving Rsat=1R_sat=1. Tables H.3 and H.4 list the two complete five-world spaces. Every world has probability 1/51/5; n2026n_2026 is its number of occurrences in the fixed seed-2026 sample of 100 worlds for that candidate. World Link n2026n_2026 (ΔT,Cmax)( T,C_ ) (Rsat,ρ)(R_sat,ρ) A0 no-link 22 (0,100)(0,100) (0,0)(0,0) A1 a1→fa_1\!→ f 17 (0,184)(0,184) (1,−1)(1,-1) A2 a2→fa_2\!→ f 17 (0,198)(0,198) (1,−1)(1,-1) A3 a3→fa_3\!→ f 17 (0,197)(0,197) (1,−1)(1,-1) A4 a5→fa_5\!→ f 27 (42,142)(42,142) (0,0.295775)(0,0.295775) Table H.3: Candidate-A worlds and seed-2026 counts. Link labels and weights are given in Table H.2. World Link n2026n_2026 (ΔT,Cmax)( T,C_ ) (Rsat,ρ)(R_sat,ρ) B0 no-link 24 (0,100)(0,100) (0,0)(0,0) B1 b1→fb_1\!→ f 29 (0,184)(0,184) (1,−1)(1,-1) B2 b2→fb_2\!→ f 18 (0,198)(0,198) (1,−1)(1,-1) B3 b3→fb_3\!→ f 16 (0,197)(0,197) (1,−1)(1,-1) B4 b4→fb_4\!→ f 13 (0,158)(0,158) (0,0)(0,0) Table H.4: Candidate-B worlds and seed-2026 counts. Link labels and weights are given in Table H.2. For example, in A4 the hard source formula forces a5a_5 true. In the lower-cost forced optimum, the weight-100100 exact link is preserved, making c true; the hard target then requires ¬f f, so the active entailment clause [¬a5∨f]42[ a_5 f]_42 is violated. Hence ρA4=42/142−0=0.295775 _A4=42/142-0=0.295775. By contrast, A2 supports ¬f f with no semantic penalty, so ρA2=0/198−1=−1 _A2=0/198-1=-1. (d) Aggregation and pairwise decision. Top-Link selects the highest-confidence link for f, namely a2→fa_2\!→ f and b2→fb_2\!→ f, in both cases contradiction with p=0.982p=0.982. The selected Candidate-A and Candidate-B configurations both have resistance −1-1, so Top-Link ties. Exact marginalization instead gives μA _A =15(0−1−1−1+0.295775)=−0.540845, = 15(0-1-1-1+0.295775)=-0.540845, μB _B =15(0−1−1−1+0)=−0.600000, = 15(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 and H.4: μ^A μ_A =17(−1)+17(−1)+17(−1)100 = 17(-1)+17(-1)+17(-1)100 +27(0.295775)+22(0)100=−0.430141, + 27(0.295775)+22(0)100=-0.430141, μ^B μ_B =29(−1)+18(−1)+16(−1)100 = 29(-1)+18(-1)+16(-1)100 +13(0)+24(0)100=−0.630000. + 13(0)+24(0)100=-0.630000. Thus sampled PWAL, exact PWAL, and all ten evaluation seeds select the gold Candidate B, while Top-Link ties. Appendix I Detailed Stable α Failure Trace In this fully enumerable α instance, Top-Link selects 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–I.5 report the input, atoms, links, categorical choices, and representative worlds. (a) Input, fixed translations, and atom meanings. Premise Bill was poor. Candidate A His business went bankrupt and he had to take a new job. Candidate B His business is worth millions. Outcome Bill made less money as a computer scientist than he did before. Table I.1: Stable α failure trace. Candidate A is gold. The source and target formulae are conjunctions: ΦSA=⋀i=16ai,ΦSB=⋀i=14bi,ΦT=⋀j=17hj. _S_A= _i=1^6a_i, _S_B= _i=1^4b_i, _T= _j=1^7h_j. The atom surfaces in Table I.2 are reproduced verbatim from the translator output and were not manually edited. Candidate A source Candidate B source Target a1a_1 Bill is poor b1b_1 Bill is poor h1h_1 computer scientist a2a_2 business is bankrupted b2b_2 multiple 1000000 dollars h2h_2 Bill make money a3a_3 job is new b3b_3 he’s business h3h_3 Bill make money a4a_4 he’s business b4b_4 business worth multiple h4h_4 Bill make toward scientist a5a_5 he take job h5h_5 Bill make during before a6a_6 he obligate take h6h_6 money have quant by less h7h_7 money have quant money Table I.2: Complete atom inventory. h2h_2 and h3h_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)=max1,⌊100p⌋w(p)= \1, 100p \. A retained entailment s→hs\!→ h contributes [¬s∨h]w(p)[ s h]_w(p), and a retained contradiction contributes [¬s∨¬h]w(p)[ s h]_w(p). Because h2h_2 and h3h_3 have identical candidate sets, a row marked h2,h3h_2,h_3 represents two separate links, one to each target occurrence. Cand. Target Source Source surface Label p w(p)w(p) A h2,h3h_2,h_3 a1a_1 Bill is poor Con 0.989 98 A h2,h3h_2,h_3 a2a_2 business is bankrupted Con 0.973 97 A h2,h3h_2,h_3 a4a_4 he’s business Ent 0.670 67 A h2,h3h_2,h_3 a6a_6 he obligate take Ent 0.587 58 A h5h_5 a3a_3 job is new Con 0.983 98 A h6h_6 a1a_1 Bill is poor Ent 0.579 57 A h6h_6 a2a_2 business is bankrupted Ent 0.423 42 A h7h_7 a1a_1 Bill is poor Con 0.918 91 A h7h_7 a2a_2 business is bankrupted Con 0.886 88 B h2,h3h_2,h_3 b1b_1 Bill is poor Con 0.989 98 B h2,h3h_2,h_3 b2b_2 multiple 1000000 dollars Ent 0.685 68 B h2,h3h_2,h_3 b3b_3 he’s business Ent 0.670 67 B h2,h3h_2,h_3 b4b_4 business worth multiple Ent 0.940 94 B h6h_6 b1b_1 Bill is poor Ent 0.579 57 B h6h_6 b2b_2 multiple 1000000 dollars Con 0.551 55 B h6h_6 b4b_4 business worth multiple Con 0.761 76 B h7h_7 b1b_1 Bill is poor Con 0.918 91 B h7h_7 b2b_2 multiple 1000000 dollars Ent 0.901 90 B h7h_7 b4b_4 business worth multiple Ent 0.774 77 Table 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 both h2h_2 and h3h_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: Target Candidate A choices Candidate B choices h1h_1 no-link (probability 1) no-link (probability 1) h2h_2 no-link, a1a_1 Con, a2a_2 Con, a4a_4 Ent, a6a_6 Ent (each 1/51/5) no-link, b1b_1 Con, b2b_2 Ent, b3b_3 Ent, b4b_4 Ent (each 1/51/5) h3h_3 same five A choices as h2h_2 (each 1/51/5) same five B choices as h2h_2 (each 1/51/5) h4h_4 no-link (probability 1) no-link (probability 1) h5h_5 no-link, a3a_3 Con (each 1/21/2) no-link (probability 1) h6h_6 no-link, a1a_1 Ent, a2a_2 Ent (each 1/31/3) no-link, b1b_1 Ent, b2b_2 Con, b4b_4 Con (each 1/41/4) h7h_7 no-link, a1a_1 Con, a2a_2 Con (each 1/31/3) no-link, b1b_1 Con, b2b_2 Ent, b4b_4 Ent (each 1/41/4) 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 N_A =1⋅5⋅5⋅1⋅2⋅3⋅3=450, =1· 5· 5· 1· 2· 3· 3=450, NB N_B =1⋅5⋅5⋅1⋅1⋅4⋅4=400. =1· 5· 5· 1· 1· 4· 4=400. All A worlds have probability 1/4501/450, and all B worlds have probability 1/4001/400. The displayed sampled run draws 100 worlds per candidate with seed 2026 rather than enumerating these world spaces. (d) Deterministic Top-Link calculation. Top-Link activates the highest-confidence non-neutral link for every target that has one. Its active sets are LAtop= L_A^top= a1→h2(Con),a1→h3(Con), \a_1\!→ h_2\;( Con),a_1\!→ h_3\;( Con), a3→h5(Con),a1→h6(Ent), a_3\!→ h_5\;( Con),a_1\!→ h_6\;( Ent), a1→h7(Con), a_1\!→ h_7\;( Con)\, LBtop= L_B^top= b1→h2(Con),b1→h3(Con), \b_1\!→ h_2\;( Con),b_1\!→ h_3\;( Con), b4→h6(Con),b1→h7(Con). b_4\!→ h_6\;( Con),b_1\!→ h_7\;( Con)\. For A, the active capacity is Cmax=98+98+98+57+91=442C_ =98+98+98+57+91=442. Forcing the positive target conjunction violates the four contradiction clauses (cost 98+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. _A^top=385/442-1/7=0.728184. For B, all four selected links are contradictions, so ΔT=Cmax=98+98+76+91=363 T=C_ =98+98+76+91=363 and no positive target clause is witnessed: ρBtop=363/363−0=1. _B^top=363/363-0=1. Lower resistance is preferred; Top-Link therefore 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: ρ=ΔTCmax−Rsat.ρ= TC_ -R_sat. Candidate A and Candidate B have 450 and 400 worlds, respectively. The two candidate-specific spaces are marginalized separately rather than crossed into 450×400450× 400 joint worlds. Table I.4 defines both complete world spaces; Table I.5 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. Cand. Draw Active links ΔT T CmaxC_ RsatR_sat ρ A 86 a2→h3a_2\!→ h_3 Con 97 97 0 1.000000 A 76 a1→h2a_1\!→ h_2 Con; a6→h3a_6\!→ h_3 Ent; a3→h5a_3\!→ h_5 Con; a2→h6a_2\!→ h_6 Ent; a1→h7a_1\!→ h_7 Con 287 387 2/72/7 0.455888 B 12 b4→h2b_4\!→ h_2 Ent; b3→h3b_3\!→ h_3 Ent; b1→h7b_1\!→ h_7 Con 91 252 2/72/7 0.075397 B 20 b4→h2b_4\!→ h_2 Ent; b4→h3b_4\!→ h_3 Ent; b1→h6b_1\!→ h_6 Ent; b4→h7b_4\!→ h_7 Ent 0 322 4/74/7 -0.571429 Table I.5: Representative seed-2026 candidate-specific worlds for the stable α failure trace. Con and Ent refer to Table I.3. Draw is the index within the fixed seed-2026 candidate-specific sample. For example, draw A76 has three contradiction clauses whose weights sum to 98+98+91=28798+98+91=287; those clauses are violated when the positive target is forced. Its two entailment links witness h3h_3 and h6h_6, giving ρA76=287/387−2/7=0.455888. _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: ρB20=0/322−4/7=−0.571429 _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 the K=100K=100 seed-2026 worlds sampled separately for each candidate, let T¯=1K∑k=1KΔTkCmax,k,R¯=1K∑k=1KRsat,k. T= 1K _k=1^K T_kC_ ,k, R= 1K _k=1^KR_sat,k. Then μ^=T¯−R¯ μ= T- R, and the seed-2026 sample averages are T¯R¯μ^=T¯−R¯A0.6672640.2042860.462978B0.3737970.2842860.089512 array[]c@ c& T& R& μ= T- R\\ A&0.667264&0.204286&0.462978\\ B&0.373797&0.284286&0.089512 array PWAL therefore selects B, the distractor. Exact marginalization over all 450 Candidate-A worlds and 400 Candidate-B worlds gives μA _A =0.449152, =0.449152, μB _B =0.098678, =0.098678, μB−μA _B- _A =−0.350474. =-0.350474. Exact marginalization therefore confirms the same wrong decision. The absolute exact margin is 0.3504740.350474; all seeds 2026–2035 choose B, and the smallest sampled absolute margin is 0.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.