body{margin:0}
/* Layout: one centred column. Tree panel (header, scrollable SVG tree, program strip), key,
   narration line, control bar, then the optional program editor. Same palette and type as
   the forward chaining demo so the two read as a pair. */
:root {
  --bg: #eef1f0;
  --panel: #fbfcfb;
  --ink: #1d2a2e;
  --muted: #5b6a6f;
  --line: #d2d9d7;
  --accent: #2c4f7c;
  --accent-ink: #ffffff;
  --band: #e4ecf5;
  --open: #eef3f9;
  --node: #e3e7e8;
  --node-stroke: #a7b1b4;
  --true: #2e9a5a;
  --true-line: #1d7442;
  --true-ink: #ffffff;
  --true-soft: #e1f2e7;
  --probe: #cf870b;
  --miss: #c2483a;
  --miss-soft: #f7e0dc;

  --font-display: "Newsreader", Georgia, "Times New Roman", serif;
  --font-body: "IBM Plex Sans", system-ui, -apple-system, "Segoe UI", sans-serif;
  --font-mono: "IBM Plex Mono", ui-monospace, Menlo, Consolas, monospace;
}
@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    --bg: #121618; --panel: #1a1f22; --ink: #e3e8e9; --muted: #9aa6aa; --line: #2d3539;
    --accent: #8fb3e6; --accent-ink: #0e1620; --band: #1f2a37; --open: #1d2631;
    --node: #262d31; --node-stroke: #4d585d;
    --true: #36a865; --true-line: #74d79b; --true-ink: #06150c; --true-soft: #18301f;
    --probe: #f0ad3a; --miss: #ec7766; --miss-soft: #3a2320;
    color-scheme: dark;
  }
}
:root[data-theme="dark"] {
  --bg: #121618; --panel: #1a1f22; --ink: #e3e8e9; --muted: #9aa6aa; --line: #2d3539;
  --accent: #8fb3e6; --accent-ink: #0e1620; --band: #1f2a37; --open: #1d2631;
  --node: #262d31; --node-stroke: #4d585d;
  --true: #36a865; --true-line: #74d79b; --true-ink: #06150c; --true-soft: #18301f;
  --probe: #f0ad3a; --miss: #ec7766; --miss-soft: #3a2320;
  color-scheme: dark;
}

* { box-sizing: border-box; }
[hidden] { display: none !important; }
body {
  background: var(--bg);
  color: var(--ink);
  font-family: var(--font-body);
  font-size: 15px;
  line-height: 1.55;
}
.wrap {
  max-width: 1040px;
  margin: 0 auto;
  padding-inline: 20px;
  padding-block: 28px 56px;
  display: grid;
  gap: 18px;
}

/* ---------- Intro ---------- */
.intro { display: grid; gap: 6px; }
.eyebrow {
  margin: 0;
  font-family: var(--font-mono);
  font-size: 12px;
  letter-spacing: 0.1em;
  text-transform: uppercase;
  color: var(--muted);
}
h1 {
  margin: 0;
  font-family: var(--font-display);
  font-weight: 600;
  font-size: clamp(30px, 4.4vw, 40px);
  line-height: 1.08;
  letter-spacing: -0.01em;
  text-wrap: balance;
}
.lede { margin: 0; max-width: 68ch; color: var(--muted); }

/* ---------- Tree panel ---------- */
.panel {
  min-width: 0;
  background: var(--panel);
  border: 1px solid var(--line);
  border-radius: 16px;
  overflow: hidden;
}
.panel-head {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 8px 14px;
  padding: 16px 20px 10px;
}
.panel-head h2 {
  margin: 0;
  font-family: var(--font-display);
  font-size: 23px;
  font-weight: 600;
  line-height: 1.2;
}
.spacer { flex: 1 1 auto; }
.badge {
  font-family: var(--font-mono);
  font-size: 11px;
  font-weight: 600;
  letter-spacing: 0.1em;
  text-transform: uppercase;
  padding: 4px 11px;
  border-radius: 999px;
  background: var(--band);
  color: var(--accent);
  white-space: nowrap;
}
.badge.ok { background: var(--true); color: var(--true-ink); }
.badge.bad { background: var(--miss-soft); color: var(--miss); }
.count { font-family: var(--font-mono); font-size: 13px; color: var(--muted); font-variant-numeric: tabular-nums; }

.seg { display: inline-flex; border: 1px solid var(--line); border-radius: 8px; overflow: hidden; }
.seg button {
  font: 500 12.5px/1 var(--font-body);
  padding: 7px 11px;
  border: 0;
  background: var(--bg);
  color: var(--muted);
  cursor: pointer;
}
.seg button + button { border-left: 1px solid var(--line); }
.seg button[aria-pressed="true"] { background: var(--band); color: var(--accent); }

.tree-scroll {
  overflow: auto;
  max-height: min(74vh, 980px);
  border-block: 1px solid var(--line);
  background: var(--panel);
  overscroll-behavior: contain;
}
#tree { display: block; }

.program-wrap {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 8px 14px;
  padding: 12px 20px 14px;
}
.program-label {
  font-family: var(--font-mono);
  font-size: 11px;
  letter-spacing: 0.14em;
  text-transform: uppercase;
  color: var(--muted);
}
.program {
  display: flex;
  flex-wrap: wrap;
  gap: 6px;
  margin: 0;
  padding: 0;
  list-style: none;
  min-width: 0;
}
.program li {
  display: inline-flex;
  align-items: baseline;
  gap: 6px;
  padding: 3px 9px;
  border-radius: 6px;
  border: 1px solid var(--line);
  background: var(--bg);
  font-family: var(--font-mono);
  font-size: 13px;
  transition: background 0.2s, border-color 0.2s;
}
.program .cn { font-size: 11px; color: var(--muted); }
.program code { font-family: inherit; }
.program li.match { border-color: var(--probe); }
.program li.trying { border-color: var(--accent); background: var(--band); }
.program li.trying .cn { color: var(--accent); font-weight: 600; }

/* ---------- Legend ---------- */
.legend {
  display: flex;
  flex-wrap: wrap;
  gap: 6px 20px;
  margin: 0;
  padding: 0;
  list-style: none;
  font-size: 13px;
  color: var(--muted);
}
.legend li { display: inline-flex; align-items: center; gap: 7px; }
.sw {
  display: inline-block;
  width: 26px;
  height: 15px;
  border-radius: 5px;
  border: 1.5px solid var(--node-stroke);
  background: var(--panel);
}
.sw.focus { border: 2.5px solid var(--probe); background: transparent; }
.sw.pending { border-style: dashed; }
.sw.path { border: 2px solid var(--accent); background: var(--open); }
.sw.proof { background: var(--true); border-color: var(--true-line); }
.sw.fail { background: var(--miss-soft); border-color: var(--miss); }
.sw.cut { background: var(--node); border: 1.5px dashed var(--miss); }

/* ---------- Narration ---------- */
.status {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 6px 12px;
  margin: 0;
  min-height: 3.2em;
  font-size: 15.5px;
}
.chip {
  flex: none;
  font-family: var(--font-mono);
  font-size: 11.5px;
  font-weight: 600;
  letter-spacing: 0.08em;
  text-transform: uppercase;
  padding: 2px 9px;
  border-radius: 5px;
  background: var(--band);
  color: var(--accent);
  white-space: nowrap;
}
.msg { flex: 1 1 280px; min-width: 0; }
.atom { font-family: var(--font-mono); font-weight: 600; }
.atom.t { color: var(--true-line); }
.atom.f { color: var(--miss); }
.atom.c { color: var(--accent); }

/* ---------- Controls ---------- */
.controls {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 14px 26px;
  padding: 14px 16px;
  background: var(--panel);
  border: 1px solid var(--line);
  border-radius: 12px;
}
.btns, .selects { display: flex; flex-wrap: wrap; gap: 8px; }
.selects { gap: 8px 18px; }
.btn {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  gap: 7px;
  padding: 8px 15px;
  font: 500 14px/1.2 var(--font-body);
  color: var(--ink);
  background: var(--bg);
  border: 1px solid var(--line);
  border-radius: 8px;
  cursor: pointer;
}
.btn:hover:not(:disabled) { border-color: var(--muted); }
.btn.primary { min-width: 112px; color: var(--accent-ink); background: var(--accent); border-color: var(--accent); }
.btn.primary:hover:not(:disabled) { border-color: var(--accent); filter: brightness(1.08); }
.btn.next:not(:disabled) { color: var(--true-ink); background: var(--true); border-color: var(--true-line); }
.btn:disabled { opacity: 0.45; cursor: default; }
.icon { width: 14px; height: 14px; fill: currentColor; }

.field { display: inline-flex; align-items: center; gap: 8px; }
.field-label, .slider-label { font-size: 13.5px; color: var(--muted); white-space: nowrap; }
select {
  font: 500 14px var(--font-mono);
  padding: 6px 8px;
  color: var(--ink);
  background: var(--bg);
  border: 1px solid var(--line);
  border-radius: 7px;
}
.slider {
  flex: 1 1 230px;
  min-width: 0;
  display: grid;
  grid-template-columns: auto 1fr auto;
  align-items: center;
  gap: 10px;
}
input[type="range"] { width: 100%; min-width: 0; accent-color: var(--accent); }
output {
  min-width: 7ch;
  text-align: right;
  font-family: var(--font-mono);
  font-size: 13px;
  font-variant-numeric: tabular-nums;
}
.btn:focus-visible, input:focus-visible, select:focus-visible, textarea:focus-visible,
summary:focus-visible, .seg button:focus-visible {
  outline: 2px solid var(--accent);
  outline-offset: 2px;
}

/* ---------- Editor ---------- */
.editor { background: var(--panel); border: 1px solid var(--line); border-radius: 12px; padding: 12px 16px; }
.editor summary { cursor: pointer; font-weight: 500; }
.hint { margin: 10px 0; max-width: 68ch; font-size: 14px; color: var(--muted); }
.hint code {
  font-family: var(--font-mono);
  font-size: 13px;
  padding: 1px 5px;
  border-radius: 4px;
  background: var(--band);
  color: var(--ink);
}
textarea {
  display: block;
  width: 100%;
  padding: 10px 12px;
  font-family: var(--font-mono);
  font-size: 14px;
  line-height: 1.55;
  color: var(--ink);
  background: var(--bg);
  border: 1px solid var(--line);
  border-radius: 8px;
  resize: vertical;
}
.editor-actions { display: flex; flex-wrap: wrap; align-items: center; gap: 8px 10px; margin-top: 10px; }
.error { flex: 1 1 200px; margin: 0; font-size: 13.5px; color: var(--miss); }

/* ---------- SVG tree ---------- */
.ruler { stroke: var(--line); stroke-width: 1; stroke-dasharray: 2 5; }
.ruler.max { stroke: var(--miss); stroke-opacity: 0.55; stroke-dasharray: 6 5; }
.ruler-head { font-family: var(--font-mono); font-size: 10.5px; letter-spacing: 0.14em; fill: var(--muted); }
.ruler-label { font-family: var(--font-mono); font-size: 12px; fill: var(--muted); dominant-baseline: central; font-variant-numeric: tabular-nums; }
.ruler-label.max { fill: var(--miss); }

.edge line { stroke: var(--node-stroke); stroke-width: 1.5; transition: stroke 0.3s; }
.edge.pending line { stroke-dasharray: 4 4; }
.edge.done line { stroke-opacity: 0.55; }
.edge.path line { stroke: var(--accent); stroke-width: 2.5; stroke-opacity: 1; }
.edge.proof line { stroke: var(--true); stroke-width: 2.5; stroke-opacity: 1; }
.edge-label rect { fill: var(--panel); stroke: var(--line); }
.edge-label text {
  font-family: var(--font-mono);
  font-size: 11px;
  font-weight: 600;
  fill: var(--muted);
  text-anchor: middle;
  dominant-baseline: central;
}
.edge.pending .edge-label { opacity: 0.7; }
.edge.path .edge-label rect { stroke: var(--accent); }
.edge.path .edge-label text { fill: var(--accent); }
.edge.proof .edge-label rect { stroke: var(--true); }
.edge.proof .edge-label text { fill: var(--true-line); }

.node .body { fill: var(--panel); stroke: var(--node-stroke); stroke-width: 1.5; transition: fill 0.3s, stroke 0.3s; }
.node text {
  font-family: var(--font-mono);
  font-size: 14px;
  font-weight: 500;
  fill: var(--ink);
  text-anchor: middle;
  dominant-baseline: central;
  transition: fill 0.3s;
}
.node .pfx { fill: var(--muted); }
.node.pending { opacity: 0.8; }
.node.pending .body { stroke-dasharray: 4 3; }
.node.pending text { fill: var(--muted); }
.node.open .body { fill: var(--open); }
.node.path .body { stroke: var(--accent); stroke-width: 2; }
.node.done { opacity: 0.6; }
.node.done .body { fill: var(--node); }
.node.selecting .sel { fill: var(--accent); font-weight: 600; text-decoration: underline; }
.node.proof { opacity: 1; }
.node.proof .body { fill: var(--true-soft); stroke: var(--true); stroke-width: 2; }
.node.success .body { fill: var(--true); stroke: var(--true-line); }
.empty-box { fill: none; stroke: var(--muted); stroke-width: 1.6; }
.node.success .empty-box { stroke: var(--true-ink); }
.node.fail .body { fill: var(--miss-soft); stroke: var(--miss); }
.node.fail { opacity: 1; }
.node.cut .body { fill: var(--node); stroke: var(--miss); stroke-dasharray: 3 3; }
.node.cut { opacity: 1; }

.caption { font-family: var(--font-mono); font-size: 11px; fill: var(--muted); text-anchor: middle; }
.caption.ok { fill: var(--true-line); font-weight: 600; }
.caption.bad { fill: var(--miss); }

.focus { fill: none; stroke: var(--probe); stroke-width: 2.5; }

@media (prefers-reduced-motion: reduce) {
  .edge line, .node .body, .node text, .program li { transition: none; }
}