/* Search explorer: replay of the recorded proof search */
.sx-pipeline { display: grid; grid-template-columns: repeat(5, minmax(0, 1fr)); gap: 0; margin: 8px 0 6px; border: 1px solid rgb(var(--c-line)); border-radius: var(--radius); overflow: hidden; background: rgb(var(--c-paper)); }
.sx-stage { position: relative; display: flex; flex-direction: column; gap: 4px; padding: 14px 16px 14px 18px; border: 0; border-right: 1px solid rgb(var(--c-line)); background: transparent; text-align: left; cursor: pointer; font-family: var(--font-sans); color: rgb(var(--c-ink-soft)); transition: background .2s, color .2s; }
.sx-stage:last-child { border-right: 0; }
.sx-stage:not(:last-child)::after { content: "→"; position: absolute; right: -8px; top: 50%; z-index: 1; transform: translateY(-50%); padding: 0 1px; background: rgb(var(--c-paper)); font-size: .8rem; color: rgb(var(--c-muted)); }
.sx-stage .sx-num { font-family: var(--font-mono); font-size: .7rem; letter-spacing: var(--track-mono); color: rgb(var(--c-muted)); }
.sx-stage strong { font-weight: 600; font-size: .92rem; color: rgb(var(--c-ink)); }
.sx-stage .sx-sub { font-size: .78rem; color: rgb(var(--c-muted)); }
.sx-stage:hover { background: rgb(var(--c-paper-2)); }
.sx-stage.is-active { background: rgb(var(--c-oxford) / .09); box-shadow: inset 0 -3px 0 rgb(var(--c-oxford)); }
.sx-stage[aria-pressed="true"] { background: rgb(var(--c-oxford) / .16); }
.sx-stage:focus-visible { outline: 2px solid rgb(var(--c-oxford)); outline-offset: -2px; }
[data-sx="sx-stage-text"] { min-height: 1.6em; margin: 6px 0 22px; font-family: var(--font-serif); font-size: 1rem; color: rgb(var(--c-ink-soft)); }

.sx-panel { border: 1px solid rgb(var(--c-line)); border-radius: var(--radius); background: rgb(var(--c-paper)); }
.sx-head { display: flex; flex-wrap: wrap; gap: 12px 24px; align-items: flex-end; justify-content: space-between; padding: 18px 20px 14px; border-bottom: 1px solid rgb(var(--c-line)); }
.sx-head h3 { margin: 2px 0 2px; font-family: var(--font-display); font-weight: 500; font-size: 1.35rem; color: rgb(var(--c-ink)); }
.sx-head p { margin: 0; font-family: var(--font-serif); color: rgb(var(--c-ink-soft)); }
.sx-head select { max-width: 100%; padding: 7px 10px; border: 1px solid rgb(var(--c-line-strong)); border-radius: var(--radius); background: rgb(var(--c-paper)); color: rgb(var(--c-ink)); font-family: var(--font-sans); font-size: .9rem; }
.sx-head label { display: flex; flex-direction: column; gap: 4px; min-width: 0; }
.sx-controls { display: flex; flex-wrap: wrap; align-items: center; gap: 8px 10px; padding: 12px 20px; border-bottom: 1px solid rgb(var(--c-line)); background: rgb(var(--c-paper-2) / .6); }
.sx-controls button { min-width: 38px; padding: 6px 12px; border: 1px solid rgb(var(--c-line-strong)); border-radius: var(--radius); background: rgb(var(--c-paper)); color: rgb(var(--c-ink)); font-family: var(--font-sans); font-size: .86rem; cursor: pointer; }
.sx-controls button[data-sx="sx-play"] { min-width: 74px; border-color: rgb(var(--c-ink)); background: rgb(var(--c-ink)); color: rgb(var(--c-paper)); }
.sx-controls button:disabled { opacity: .4; cursor: default; }
.sx-controls button:focus-visible, .sx-head select:focus-visible { outline: 2px solid rgb(var(--c-oxford)); outline-offset: 2px; }
[data-sx="sx-count"] { font-family: var(--font-mono); font-size: .74rem; letter-spacing: var(--track-mono); color: rgb(var(--c-muted)); }
.sx-toggle { display: inline-flex; align-items: center; gap: 6px; margin-left: auto; font-family: var(--font-sans); font-size: .86rem; color: rgb(var(--c-ink-soft)); }
.sx-legend { display: flex; flex-wrap: wrap; gap: 6px 16px; padding: 10px 20px; border-bottom: 1px solid rgb(var(--c-line)); font-family: var(--font-sans); font-size: .8rem; color: rgb(var(--c-ink-soft)); }
.sx-legend span { display: inline-flex; align-items: center; gap: 6px; }
.sx-legend i { display: inline-block; width: 22px; height: 12px; border-radius: 6px; border: 1.5px solid; }
.sx-legend .lg-model { border-color: rgb(var(--c-oxford)); background: rgb(var(--c-oxford) / .12); }
.sx-legend .lg-auto { border-color: rgb(var(--c-muted)); background: rgb(var(--c-paper-2)); }
.sx-legend .lg-hammer { border-color: rgb(var(--c-good)); background: rgb(var(--c-good) / .12); }
.sx-legend .lg-goal { border-radius: 2px; border-color: rgb(var(--c-line-strong)); }
.sx-legend .lg-proved { border-radius: 2px; border-color: rgb(var(--c-good)); background: rgb(var(--c-good) / .14); }
.sx-legend .lg-rej { width: 16px; height: 16px; border-radius: 50%; border-color: rgb(var(--c-bad)); }
.sx-legend .lg-proof { width: 22px; height: 0; border: 0; border-top: 3px solid rgb(var(--c-oxford)); border-radius: 0; }

.sx-body { display: grid; grid-template-columns: minmax(0, 1fr) 340px; min-height: 460px; }
[data-sx="sx-scroll"] { overflow: auto; max-height: 560px; padding: 18px 12px 12px 16px; border-right: 1px solid rgb(var(--c-line)); cursor: grab; }
[data-sx="sx-scroll"]:focus-visible { outline: 2px solid rgb(var(--c-oxford)); outline-offset: -2px; }
[data-sx="sx-svg"] { display: block; font-family: var(--font-mono); }
.sx-wire { fill: none; stroke: rgb(var(--c-line-strong)); stroke-width: 1.3; }
.sx-wire.is-shared { stroke-dasharray: 3 4; }
.sx-wire.is-proof { stroke: rgb(var(--c-oxford)); stroke-width: 3; }
.sx-goal rect { fill: rgb(var(--c-paper)); stroke: rgb(var(--c-line-strong)); stroke-width: 1.3; }
.sx-goal text { font-size: 11px; fill: rgb(var(--c-ink)); pointer-events: none; }
.sx-goal.is-root rect { stroke: rgb(var(--c-ink)); stroke-width: 1.8; }
.sx-goal.is-proved rect { fill: rgb(var(--c-good) / .13); stroke: rgb(var(--c-good)); }
.sx-move rect { stroke-width: 1.5; }
.sx-move text { font-size: 10.5px; pointer-events: none; }
.sx-move.who-model rect { fill: rgb(var(--c-oxford) / .1); stroke: rgb(var(--c-oxford)); }
.sx-move.who-model text { fill: rgb(var(--c-oxford)); }
.sx-move.who-auto rect { fill: rgb(var(--c-paper-2)); stroke: rgb(var(--c-muted)); }
.sx-move.who-auto text { fill: rgb(var(--c-ink-soft)); }
.sx-move.who-hammer rect { fill: rgb(var(--c-good) / .12); stroke: rgb(var(--c-good)); }
.sx-move.who-hammer text { fill: rgb(var(--c-good)); }
.sx-move.is-proof rect { stroke-width: 2.6; }
.sx-goal, .sx-move { cursor: pointer; outline: none; }
.sx-goal:focus-visible rect, .sx-move:focus-visible rect, .is-selected rect { stroke: rgb(var(--c-ink)) !important; stroke-width: 2.6 !important; }
.sx-goal.is-current rect, .sx-move.is-current rect { stroke: rgb(var(--c-warn)) !important; stroke-width: 3 !important; }
.sx-move.is-current { animation: sx-pop .5s ease-out; }
.is-lit rect { filter: drop-shadow(0 0 5px rgb(var(--c-oxford) / .65)); }
.sx-rej circle { fill: rgb(var(--c-paper)); stroke: rgb(var(--c-bad)); stroke-width: 1.4; }
.sx-rej text { font-size: 9px; fill: rgb(var(--c-bad)); }
.sx-rej.is-current circle { fill: rgb(var(--c-bad) / .2); stroke-width: 2.4; }
@keyframes sx-pop { from { opacity: .2; } to { opacity: 1; } }
@media (prefers-reduced-motion: reduce) { .sx-move.is-current { animation: none; } }

[data-sx="sx-detail"] { padding: 18px 20px; overflow-y: auto; max-height: 560px; font-family: var(--font-sans); font-size: .9rem; color: rgb(var(--c-ink-soft)); }
[data-sx="sx-detail"] h4 { margin: 4px 0 8px; font-family: var(--font-serif); font-weight: 600; font-size: 1.08rem; color: rgb(var(--c-ink)); }
[data-sx="sx-detail"] p { margin: 0 0 10px; line-height: 1.5; }
.sx-code { margin: 0 0 12px; padding: 10px 12px; max-height: 220px; overflow: auto; border-left: 2px solid rgb(var(--c-oxford)); background: rgb(var(--c-paper-2)); font-family: var(--font-mono); font-size: .76rem; line-height: 1.55; color: rgb(var(--c-ink)); white-space: pre-wrap; overflow-wrap: anywhere; }
.sx-note { padding: 8px 10px; border: 1px solid rgb(var(--c-line)); border-radius: var(--radius); font-family: var(--font-serif); color: rgb(var(--c-ink)); }
.sx-err { font-family: var(--font-mono); font-size: .76rem; color: rgb(var(--c-bad)); overflow-wrap: anywhere; }
.sx-proofmark { font-weight: 600; color: rgb(var(--c-oxford)); }
.sx-tries { list-style: none; margin: 6px 0 0; padding: 0; }
.sx-tries li { border-bottom: 1px solid rgb(var(--c-line)); }
.sx-try { display: grid; grid-template-columns: auto minmax(0, 1fr) auto; gap: 8px; align-items: baseline; width: 100%; padding: 7px 0; border: 0; background: none; text-align: left; cursor: pointer; color: inherit; font: inherit; }
.sx-try:hover code { text-decoration: underline; }
.sx-try code { font-family: var(--font-mono); font-size: .74rem; overflow-wrap: anywhere; color: rgb(var(--c-ink)); }
.sx-badge { font-family: var(--font-mono); font-size: .64rem; letter-spacing: var(--track-mono); text-transform: uppercase; }
.who-model .sx-badge { color: rgb(var(--c-oxford)); } .who-auto .sx-badge { color: rgb(var(--c-muted)); } .who-hammer .sx-badge { color: rgb(var(--c-good)); }
.sx-res { font-size: .76rem; white-space: nowrap; color: rgb(var(--c-muted)); }
.sx-foot { display: flex; flex-wrap: wrap; gap: 8px 20px; justify-content: space-between; align-items: center; padding: 12px 20px; border-top: 1px solid rgb(var(--c-line)); }
[data-sx="sx-verdict"] { margin: 0; font-family: var(--font-serif); font-size: .98rem; color: rgb(var(--c-ink)); }
.sx-caveat { margin: 12px 0 0; font-family: var(--font-sans); font-size: .82rem; color: rgb(var(--c-muted)); }

@media (max-width: 900px) {
  .sx-pipeline { grid-template-columns: 1fr; }
  .sx-stage { border-right: 0; border-bottom: 1px solid rgb(var(--c-line)); padding: 10px 14px; }
  .sx-stage:last-child { border-bottom: 0; }
  .sx-stage:not(:last-child)::after { content: "↓"; right: 14px; top: auto; bottom: -10px; transform: none; }
  .sx-body { grid-template-columns: 1fr; }
  [data-sx="sx-scroll"] { max-height: 420px; border-right: 0; border-bottom: 1px solid rgb(var(--c-line)); }
  [data-sx="sx-detail"] { max-height: none; }
  .sx-toggle { margin-left: 0; }
}
.sx-zoom { display: inline-flex; align-items: center; gap: 6px; }
.sx-zoom .apparatus { min-width: 38px; text-align: center; }
.sx-subs { margin: 4px 0 12px; padding-left: 20px; } .sx-subs li { margin: 0 0 6px; } .sx-subs code { font-family: var(--font-mono); font-size: .74rem; overflow-wrap: anywhere; color: rgb(var(--c-ink)); }