pith. sign in

arxiv: 2606.03883 · v1 · pith:CZPCDEZNnew · submitted 2026-06-02 · 💻 cs.AI · cs.LG

Reasoning Structure of Large Language Models

Fr\'ed\'eric Berdoz , Luca A. Lanzend\"orfer , Fabian Farestam , Roger Wattenhofer This is my paper

Pith reviewed 2026-06-28 10:04 UTC · model grok-4.3

classification 💻 cs.AI cs.LG
keywords large language modelsreasoning modelslogic puzzlesreasoning graphsefficiency metricstructural analysisfailure diagnosis
0
0 comments X

The pith

Reasoning traces from large language models can be turned into graphs of claims and dependencies whose structure distinguishes behaviors that accuracy and token counts cannot.

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

Large reasoning models are usually scored by final answer accuracy and the number of tokens they generate. These scores can be identical even when the models follow entirely different logical paths. The paper introduces a benchmark of logic puzzles together with a pipeline that extracts verifiable graphs of claims connected by dependencies from the models' traces. It defines a reasoning efficiency metric that measures how concentrated the logical flow is inside each graph. Tests on open-source models demonstrate that these graph-based quantities separate distinct reasoning behaviors and show how structure changes as puzzles grow harder.

Core claim

Reasoning in large language models can be represented as verifiable graphs of claims and dependencies extracted from unstructured traces by a scalable pipeline. These graphs turn reasoning into a measurable topological object that supports quantitative analysis. A reasoning efficiency metric derived from the graphs quantifies the concentration of logical flow. When applied to open-source models on logic puzzles, the structural measures distinguish model behaviors that final-answer accuracy and token count leave indistinguishable, supplying a tool for diagnosing failure modes and tracking how reasoning structure scales with puzzle difficulty.

What carries the argument

Reasoning graphs of claims and dependencies extracted from model traces, which serve as the structured object whose topology supports the reasoning efficiency metric.

If this is right

  • Structural measurements separate reasoning behaviors that token count and accuracy conflate.
  • The reasoning efficiency metric quantifies concentration of logical flow in model traces.
  • Graph analysis provides a practical way to diagnose specific failure modes in reasoning.
  • Reasoning structure can be compared across models as puzzle difficulty increases.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the graphs prove reliable, they could be used to select or train models toward more concentrated logical structures.
  • The same extraction method might be tested on mathematical proofs or code to see whether similar structural distinctions appear.
  • Differences in graph topology across model sizes could indicate whether scaling produces systematically more efficient reasoning flows.

Load-bearing premise

The pipeline that converts unstructured traces into verifiable reasoning graphs of claims and dependencies produces graphs that faithfully represent the model's reasoning without significant construction artifacts or loss of logical dependencies.

What would settle it

Human annotation of logical dependencies in a sample of model traces that shows systematic mismatches with the pipeline output would indicate the graphs do not faithfully capture reasoning.

Figures

Figures reproduced from arXiv: 2606.03883 by Fabian Farestam, Fr\'ed\'eric Berdoz, Luca A. Lanzend\"orfer, Roger Wattenhofer.

Figure 1
Figure 1. Figure 1: Qualitative reasoning graphs. Shown are two extracted claim graphs from two independent samples of the same model (Qwen3 235B) on the same Tents puzzle instance: a diffuse trace (left) and a focused trace (right). Both traces solve the instance. Nodes are atomic claims and edges indicate deductive dependen￾cies. Node color encodes claim validity: green = verified correct, red = verified wrong, grey = unver… view at source ↗
Figure 2
Figure 2. Figure 2: Reasoning graph extraction. Example of a 4×4 Tents instance (left), an excerpt of a human-generated reasoning trace (middle), and the corresponding verifiable claim graph extracted using our pipeline described in Section 3 (right). This illustrates how our pipeline turns free-form traces into structured objects that can be analyzed beyond accuracy and token count. free-form textual traces into verifiable r… view at source ↗
Figure 3
Figure 3. Figure 3: Puzzle suite overview. We evaluate models on 21 grid puzzles spanning diverse constraint types (e.g., placement, connectivity, counting, and Latin-square-style constraints), each with four difficulty levels (Trivial, Human easy, Human normal, Human hard).. Detailed rules, state representations, and difficulty-to-size mappings for each puzzle are provided in Section E.5. The puzzle images are taken from Tat… view at source ↗
Figure 4
Figure 4. Figure 4: Graph extraction overview. Chunk-level extraction uses deterministic extraction with LLM augmentation and from￾scratch LLM extraction. Outputs are merged and screened in batches. The final claim set is then processed to extract the edges that representing the canonical reasoning steps. LLM-based steps are visualized in green, pre-processing steps are shown in blue. jump representations that quantify explor… view at source ↗
Figure 5
Figure 5. Figure 5: Efficiency correlations. Each panel plots a graph-level metric against efficiency η or token count. Points are colored by model; dashed lines show linear fits. Statistical significance is reported above each plot. (a) Efficiency is not significantly correlated with verbosity. (b,c) Efficiency tracks claim composition: negatively with stated fraction and positively with restated fraction. This suggests that… view at source ↗
Figure 6
Figure 6. Figure 6: Reasoning-flow efficiency vs. puzzle size under perfect accuracy. Mean reasoning-flow efficiency η as a function of puzzle size for settings where all puzzle sizes are solved. We observe that even when correctness is saturated, η exposes differences in reasoning structure and scaling behavior, demonstrating that accuracy alone hides substantial variation in how solutions are produced. 5. Discussion Difficu… view at source ↗
Figure 7
Figure 7. Figure 7: Prompt for solving the instance described in the puzzle state. Puzzle descriptions are detailed in Section E.5. references. The second prompt pair ( [PITH_FULL_IMAGE:figures/full_fig_p017_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: System (top) and user (bottom) prompts for determining whether the reasoning trace relies on 0-based or 1-based indexing. E.3. Rule Extraction Prompts The rule extraction prompt ( [PITH_FULL_IMAGE:figures/full_fig_p017_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: System (top) and user (bottom) prompts for extracting the claims from the reasoning trace. 19 [PITH_FULL_IMAGE:figures/full_fig_p019_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: System (top) and user (bottom) prompts for complementing claims extracted with a rule-based method. You are a strict validator for extracted claims from a reasoning trace solving a {PUZZLE} instance. TASK You will be given: - the reasoning trace (sentences labeled S1, S2, ...), - a combined list of candidate claims (JSON) Your job: SCREEN AND FILTER. SEMANTICS (CRITICAL) - A claim is VALID if at least one… view at source ↗
Figure 11
Figure 11. Figure 11: System (top) and user (bottom) prompts for filtering and cleaning claims. 20 [PITH_FULL_IMAGE:figures/full_fig_p020_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: System (top) and user (bottom) prompts for extracting deduction rules (i.e., edges). 21 [PITH_FULL_IMAGE:figures/full_fig_p021_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Possible claims for Tents. 22 [PITH_FULL_IMAGE:figures/full_fig_p022_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Possible rules for Tents. 23 [PITH_FULL_IMAGE:figures/full_fig_p023_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Possible claims for Sudoku [PITH_FULL_IMAGE:figures/full_fig_p024_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Possible rules for Sudoku. 25 [PITH_FULL_IMAGE:figures/full_fig_p025_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Puzzle description for Dominosa. You have a grid of squares, some of which contain digits, and the rest of which are empty. Your job is to fill in digits in the empty squares, in such a way that each connected region of squares all containing the same digit has an area equal to that digit. (‘Connected region’, for the purposes of this game, does not count diagonally separated squares as adjacent.) For exa… view at source ↗
Figure 20
Figure 20. Figure 20: Puzzle description for Keen. You have a grid of squares. Some are filled in black; some of the black squares are numbered. Your aim is to ‘light up’ all the empty squares by placing light bulbs in some of them. Each light bulb illuminates the square it is on, plus all squares in line with it horizontally or vertically unless a black square is blocking the way. To win the game, you must satisfy the followi… view at source ↗
Figure 21
Figure 21. Figure 21: Puzzle description for Lightup. A rectangular grid has been filled with a mixture of magnets (that is, dominoes with one positive end and one negative end) and blank dominoes (that is, dominoes with two neutral poles). These dominoes are initially only seen in silhouette. Around the grid are placed a number of clues indicating the number of positive and negative poles contained in certain columns and rows… view at source ↗
Figure 22
Figure 22. Figure 22: Puzzle description for Magnets. You are given a grid of squares, which you must colour either black or white. Some squares contain clue numbers. Each clue tells you the number of black squares in the 3×3 region surrounding the clue { including the clue square itself. You have to return a filled grid with all of the squares coloured. Black is represented by 1, white by 2 [PITH_FULL_IMAGE:figures/full_fig_… view at source ↗
Figure 24
Figure 24. Figure 24: Puzzle description for Net. You have a grid of squares, which must all be filled in either black or white. Beside each row of the grid are listed, in order, the lengths of the runs of black squares on that row; above each column are listed, in order, the lengths of the runs of black squares in that column. Your aim is to fill in the entire grid black or white. You have to return the entire grid filled out… view at source ↗
Figure 26
Figure 26. Figure 26: Puzzle description for Pearl. You have a grid of squares; some squares contain numbers. Your job is to colour some of the squares black, such that several criteria are satisfied: no square with a number is coloured black. no two black squares are adjacent (horizontally or vertically). for any two white squares, there is a path between them using only white squares. for each square with a number, that numb… view at source ↗
Figure 27
Figure 27. Figure 27: Puzzle description for Range. You have a grid of squares, with numbers written in some (but not all) of the squares. Your task is to subdivide the grid into rectangles of various sizes, such that (a) every rectangle contains exactly one numbered square, and (b) the area of each rectangle is equal to the number written in its numbered square. Return the entire grid filled out with each grid having a unique… view at source ↗
Figure 29
Figure 29. Figure 29: Puzzle description for Signpost. You have a grid of white squares, all of which contain numbers. Your task is to colour some of the squares black (removing the number) so as to satisfy all of the following conditions: No number occurs more than once in any row or column. No black square is horizontally or vertically adjacent to any other black square. The remaining white squares must all form one contiguo… view at source ↗
Figure 31
Figure 31. Figure 31: Puzzle description for Solo (also known as Sudoku). You have a grid of squares, some of which contain trees. Your aim is to place tents in some of the remaining squares, in such a way that the following conditions are met: There are exactly as many tents as trees. The tents and trees can be matched up in such a way that each tent is directly adjacent (horizontally or vertically, but not diagonally) to its… view at source ↗
Figure 33
Figure 33. Figure 33: Puzzle description for Towers. You are given a grid of squares, some of which are filled with train tracks. You need to complete the track from A to B so that the rows and columns contain the same number of track segments as are indicated in the clues to the top and right of the grid. There are only straight and 90 degree curved rails, and the track may not cross itself. Tracks was contributed to this col… view at source ↗
Figure 34
Figure 34. Figure 34: Puzzle description for Tracks. You are given a grid of squares, some of which contain diagonal mirrors. Your goal is to fill them with the given amount of each type monster. Every square which is not a mirror must be filled with one of three types of undead monster: a ghost, a vampire, or a zombie. Vampires can be seen directly, but are invisible when reflected in mirrors. Ghosts are the opposite way roun… view at source ↗
Figure 35
Figure 35. Figure 35: Puzzle description for Undead. You have a square grid; each square may contain a digit from 1 to the size of the grid, and some squares have clue signs between them. Your aim is to fully populate the grid with numbers such that: Each row contains only one occurrence of each digit Each column contains only one occurrence of each digit All the clue signs are satisfied. Make sure to return the whole grid wit… view at source ↗
read the original abstract

Large reasoning models (LRMs) are often evaluated using metrics such as final-answer accuracy or token count. However, identical scores on these metrics can hide fundamentally different reasoning structures. To address this limitation, we introduce a scalable LRM benchmark of logic puzzles and a pipeline that converts unstructured traces into verifiable reasoning graphs of claims and dependencies. This turns reasoning into a structured, measurable object whose topology can be quantitatively analyzed. Building on this, we define a reasoning efficiency metric that quantifies how concentrated the model's logical flow is. Our analysis on open-source reasoning models shows that structural measurements separate behaviors that token count and accuracy conflate, providing a practical tool for diagnosing failure modes and comparing how reasoning scales with puzzle difficulty.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces a benchmark of logic puzzles for large reasoning models (LRMs) along with a pipeline that converts unstructured reasoning traces into graphs of claims and dependencies. It defines a reasoning efficiency metric based on graph topology and claims that structural measurements distinguish reasoning behaviors that token count and accuracy metrics conflate, as demonstrated through analysis of open-source models.

Significance. If the trace-to-graph pipeline is shown to be reliable, the approach would supply a practical new lens for diagnosing LRM failure modes and comparing reasoning structure across puzzle difficulties, extending beyond conventional scalar metrics.

major comments (2)
  1. [Pipeline description (likely §3 or §4)] Pipeline description (likely §3 or §4): No validation of the automated extraction method is reported, including error rates for claim/dependency identification, comparison to human-annotated traces, or specification of whether the converter is LLM-based, rule-based, or hybrid. This is load-bearing for the central claim, as any systematic merging of claims or invention of dependencies would make the reported topology and efficiency metrics reflect pipeline artifacts rather than model reasoning.
  2. [Results and evaluation sections] Results and evaluation sections: The abstract and provided description contain no quantitative results, tables, error analysis, or ablation studies demonstrating that the structural metrics separate behaviors more effectively than baselines; without such data the separation claim cannot be assessed.
minor comments (1)
  1. [Abstract] Abstract: The phrase 'verifiable reasoning graphs' is used without defining the verification procedure or criteria for logical soundness of the extracted dependencies.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. We address each major comment below with clarifications from the full manuscript and proposed revisions where appropriate.

read point-by-point responses

  1. Referee: Pipeline description (likely §3 or §4): No validation of the automated extraction method is reported, including error rates for claim/dependency identification, comparison to human-annotated traces, or specification of whether the converter is LLM-based, rule-based, or hybrid. This is load-bearing for the central claim, as any systematic merging of claims or invention of dependencies would make the reported topology and efficiency metrics reflect pipeline artifacts rather than model reasoning.

    Authors: Section 3 describes the converter as a hybrid system: an LLM prompt for claim extraction followed by deterministic rule-based parsing for dependency edges, with explicit prompts and rules provided in the appendix. We agree that a quantitative validation study against human annotations is missing from the current version and is necessary to support the central claims. We will add a dedicated validation subsection reporting precision/recall on a sample of 200 manually annotated traces along with inter-annotator agreement. revision: yes

  2. Referee: Results and evaluation sections: The abstract and provided description contain no quantitative results, tables, error analysis, or ablation studies demonstrating that the structural metrics separate behaviors more effectively than baselines; without such data the separation claim cannot be assessed.

    Authors: Sections 5 and 6 of the full manuscript contain the requested quantitative results: tables comparing reasoning efficiency, graph density, and path concentration across five open-source LRMs on puzzles of increasing difficulty, together with direct comparisons showing that these structural metrics differentiate model behaviors where accuracy and token count do not. We will revise the abstract to include the key numerical findings and will add an explicit ablation on the efficiency metric if it is not already present in sufficient detail. revision: partial

Circularity Check

0 steps flagged

No significant circularity; empirical analysis on constructed graphs

full rationale

The paper introduces a pipeline converting traces to claim-dependency graphs and defines a reasoning efficiency metric quantifying concentration of logical flow. The central claim is an empirical finding that structural measurements distinguish behaviors conflated by token count and accuracy. No equations, self-citations, or derivations are shown that reduce any prediction or result to its inputs by construction. The pipeline and metric are presented as new tools for analysis rather than self-referential fits, and the abstract provides no load-bearing self-citation chains or ansatzes smuggled via prior work. This is a standard non-circular empirical study.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract provides no explicit details on free parameters, axioms, or invented entities; the pipeline and metric are introduced without specifying any fitted values or background assumptions.

pith-pipeline@v0.9.1-grok · 5654 in / 951 out tokens · 26163 ms · 2026-06-28T10:04:08.994351+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

20 extracted references · 3 canonical work pages · 2 internal anchors

  1. [1]

    Concrete Problems in AI Safety

    arXiv:1606.06565. Berdoz, F., Lanzend¨orfer, L., Tuninga, N., and Wattenhofer, R. Text-to-Scene with Large Reasoning Models. InAAAI Conference on Artificial Intelligence (AAAI), 2026. Besta, M., Blach, N., Kubicek, A., Gerstenberger, R., Pod- stawski, M., Gianinazzi, L., et al. Graph of Thoughts: Solving Elaborate Problems with Large Language Mod- 9 Reaso...

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  2. [2]

    Kimi K2: Open Agentic Intelligence

    URL https://www.chiark.greenend. org.uk/˜sgtatham/puzzles/. Accessed January 28, 2026. Team, K. et al. Kimi K2: Open Agentic Intelligence, 2025. arXiv:2507.20534. Ueda, N. and Nagao, T. NP-completeness Results for NONOGRAM via Parsimonious Reductions. Technical report TR96-0008, Tokyo Institute of Technology, 1996. Wang, Y ., Liu, Q., Xu, J., Liang, T., C...

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  3. [3]

    0-based" or

    arXiv:2504.10885. 11 Reasoning Structure of Large Language Models Zhou, Z., Zhu, Z., Li, X., Galkin, M., Feng, X., Koyejo, S., et al. Landscape of Thoughts: Visualizing the Reasoning Process of Large Language Models. InInternational Conference on Learning Representations (ICLR), 2026. 12 Reasoning Structure of Large Language Models Appendix overview.This ...

    work page arXiv 2026

  4. [4]

    R_COUNT_REMAINING (output: Remaining)Essence:- The reasoning trace explicitly computes an EXACT remaining count for a row/col by counting placed tents and subtracting from quota.Use only if:- \remaining/left/still to place" language + explicit counting/arithmetic.Minimal inputs:- the relevant Quota(...)- the Tent claims explicitly counted, if they exist; ...

  5. [5]

    R_LINE_BLOCK (output: NotTent)Essence:- The reasoning trace concludes this cell is NotTent BECAUSE the line has no capacity left (full / 0 remaining / quota 0).Minimal inputs:- Remaining(...,0) or Quota(...,0) when available; otherwise C_MISSING if fullness is explicitly asserted.Never use for:- no-touch or needs-tree reasoning

  6. [6]

    R_NO_TOUCH (output: NotTent)Essence:- The reasoning trace concludes this cell is NotTent because it would touch a specific tent (\tents can't touch").Minimal inputs:- the causing Tent(...) if available; otherwise C_MISSING if the reasoning trace relies on it.Never use for:- needs-tree or fullness reasoning

  7. [7]

    , \place/put/set

    R_ONLY_CAND (output: TreeCandidate OR Tent)Essence:- Tree-anchored candidate restriction (\for the tree at ... only possible cells are ...") and optionally tree-forced placement.Use only if:- reasoning is explicitly anchored to a specific tree.Minimal inputs:- Tree(...) for that tree.- include elimination reasons ONLY if explicitly cited; otherwise omit; ...

  8. [8]

    facts but the needed candidate claim is missing.Tent output allowed only if:- reasoning trace explicitly concludes/places (\must be

    R_LINE_CAND (output: LineCandidates OR Tent)Essence:- Line-anchored candidate restriction (\in row/col ... only possible cells are ...") and optionally placement from line uniqueness/intersection.Use only if:- reasoning is explicitly anchored to a row/col (or intersection of row/col candidates).Minimal inputs:- For LineCandidates output: Quota(...) or Rem...

  9. [9]

    R_CELL_NEEDS_TREE (output: NotTent)Essence:- The reasoning trace concludes this cell is NotTent because a tent must be adjacent to a tree, and this cell has no adjacent tree (as argued).Minimal inputs:- referenced Tree(...) claims if cited; otherwise omit; use C_MISSING if adjacency-to-tree reasoning is cited but missing in claims.Never use for:- no-touch...

  10. [10]

    R_CONTRADICTION_CAUSE (output: Contradiction)Essence:- The reasoning trace explicitly declares a contradiction in a BRANCH and cites (at least implicitly) the statements that cannot all hold.Use only if:- the reasoning trace says \contradiction/contradicts/inconsistent/impossible" (or equivalent) and concludes a Contradiction claim.Minimal inputs:- Includ...

  11. [11]

    tentative

    R_TENTATIVE_DISCHARGE (output: Tent or NotTent in MAIN)Essence:- Proof-by-contradiction discharge: after Contradiction(branch=k) in BRANCH#k, the reasoning trace concludes the negation of the tentative assumption in MAIN.- OR, confirmation of the tentative assumption if no contradiction arose.Inputs MUST include:- Exactly one tentative assumption in BRANC...

    2003

  12. [12]

    , \column has

    R_UNIT_HAS_STATED (output: UnitHas)Essence:- The trace explicitly states a unit contains a digit (inventory or justification).Minimal inputs: []Use when:- \digits present are ...", \column has ...", OR \because digit d is in its row/col/box"

  13. [13]

    R_UNIT_MISSING_STATED (output: UnitMissing)Essence:- The trace explicitly states the exact missing digits of a unit.Minimal inputs: []Never use for:- inferred updates after a placement unless the updated set is explicitly stated

  14. [14]

    OUT")Essence:- The trace eliminates digits for a cell explicitly because those digits already appear in the cell's row/col/box (\cannot be ... because ... already appears in

    R_ELIM_BY_UNIT_PRESENCE (output: Cand with polarity="OUT")Essence:- The trace eliminates digits for a cell explicitly because those digits already appear in the cell's row/col/box (\cannot be ... because ... already appears in ...").Minimal inputs:- The relevant UnitHas(...) claim(s) if present; otherwise C_MISSING.Notes:- The output Cand(OUT).d must matc...

  15. [15]

    OUT")Essence:- The trace eliminates digits for a cell due to an explicit constraint that is NOT phrased as direct unit presence (e.g., \by column constraints

    R_ELIM_BY_CONSTRAINT (output: Cand with polarity="OUT")Essence:- The trace eliminates digits for a cell due to an explicit constraint that is NOT phrased as direct unit presence (e.g., \by column constraints" without naming digits present, or other explicitly cited constraint reasoning).Minimal inputs:- Any explicitly referenced premise claims if they exi...

  16. [16]

    / \only remaining digit for the cell

    R_ONLY_REMAINING_IN_CELL (output: Assign)Essence:- The trace concludes the digit for a cell because all other options are eliminated (\cannot be ... so it must be ..." / \only remaining digit for the cell").Minimal inputs:- A Cand(OUT) elimination for that cell if present; otherwise C_MISSING.- A UnitMissing for the relevant unit if explicitly used/stated...

  17. [17]

    R_ONLY_MISSING_DIGIT_IN_UNIT (output: Assign)Essence:- The trace places a digit because it is the only missing digit left in a unit and the trace specifies the target cell (\only remaining digit for row/col/box is d, placed at ...").Minimal inputs:- The corresponding UnitMissing(unit,index,[d]) if explicitly stated; otherwise C_MISSING.Important:- Do NOT ...

  18. [18]

    R_PATTERN_EXPERT (output: Cand(OUT) or Assign or UnitPlaces)Essence:- A named or template-identifiable advanced Sudoku technique (X-Wing, XY-Wing, Swordfish, Skyscraper, AIC/nice loop, Unique Rectangle, ALS, etc.) is explicitly used.Minimal inputs:- Any claims explicitly referenced by the trace; otherwise C_MISSING.Use only if:- The technique name (or una...

  19. [19]

    R_CONTRADICTION_CAUSE (output: Contradiction)Essence:- The trace explicitly declares a contradiction in a branch and cites statements that cannot all hold.Minimal inputs:- Conflicting claims if referenced; otherwise C_MISSING

  20. [20]

    L" to represent the left half of a domino and

    R_CONTRADICTION_DISCHARGE (output: Cand(OUT) or Assign in MAIN)Essence:- After Contradiction in BRANCH#k, the trace concludes the negation/forced conclusion in MAIN.Inputs MUST include:- Exactly one tentative assumption in BRANCH#k.- Exactly one Contradiction(branch=k, ...) in BRANCH#k. Figure 16.Possible rules forSudoku. 25 Reasoning Structure of Large L...