@charset "UTF-8";
/* ECS651U Week 5 Logic Lab. No external fonts or assets: system UI + Georgia for formulas. */
:root {
  --ink: #13231f; --green: #1b4a40; --green-2: #2a6152; --muted: #4a5a53; --paper: #f4f3ec;
  --line: #d2d9cd; --wash: #ecf1e7; --mint: #dceacf; --coral: #a8371f; --coral-wash: #fbe4d8;
  --gold: #7a5200; --gold-wash: #fbf0d6; --focus: #1f56b8; --white: #fffef9; --edge: #5f7168;
  --mono: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace;
  --math: Georgia, 'Times New Roman', serif;
  --sans: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, 'Helvetica Neue', Arial, sans-serif;
}
* { box-sizing: border-box; }
html { -webkit-text-size-adjust: 100%; }
body { margin: 0; background: var(--paper); color: var(--ink); font: 16px/1.5 var(--sans); }
button, select, textarea, input { font: inherit; color: inherit; }
button { cursor: pointer; border: 1px solid #b9c4b9; background: var(--white); border-radius: 6px; padding: 8px 14px; font-weight: 600; line-height: 1.3; font-size: 14px; }
button:hover:not(:disabled) { border-color: var(--green); background: #edf3e8; }
button:disabled { opacity: .45; cursor: default; }
:focus-visible { outline: 3px solid var(--focus); outline-offset: 2px; }
.primary { background: var(--green); color: #fff; border-color: var(--green); }
.primary:hover:not(:disabled) { background: var(--green-2); color: #fff; }
.quiet { background: transparent; }
.text-button { border: 0; background: transparent; padding: 10px 0; color: var(--green); text-align: left; font-size: 14px; }
.text-button:hover:not(:disabled) { background: transparent; text-decoration: underline; }
.link-button { border: 0; background: transparent; padding: 2px 0; color: var(--green); font-weight: 600; font-family: var(--math); font-size: 17px; text-align: left; text-decoration: underline; text-underline-offset: 3px; }
.link-button.on { color: var(--coral); }
.link-button:hover:not(:disabled) { background: transparent; }
.skip { position: absolute; top: -80px; left: 20px; z-index: 9; padding: 12px; background: #fff; }
.skip:focus { top: 12px; }
code { font-family: var(--mono); font-size: .9em; }
.sr-only { position: absolute; width: 1px; height: 1px; padding: 0; margin: -1px; overflow: hidden; clip: rect(0, 0, 0, 0); white-space: nowrap; border: 0; }
.math { font-family: var(--math); font-size: 21px; line-height: 1.35; letter-spacing: .1px; }
.math.big { display: block; font-size: 30px; margin: 10px 0 16px; }
.math.faint { color: #8a978f; }
.subtle { color: var(--muted); font-size: 14px; }
.pad { padding: 0 28px; }
.pass { color: #1f6a35; font-weight: 600; }
.fail { color: var(--coral); font-weight: 600; }

/* ---- top bar and intro ---- */
.topbar { min-height: 70px; border-bottom: 1px solid var(--line); display: flex; align-items: center; gap: 28px; padding: 0 4vw; }
.brand { font-size: 18px; letter-spacing: 1.6px; font-weight: 800; white-space: nowrap; display: inline-flex; align-items: center; }
.brand > span:last-child { font-weight: 400; margin-left: 6px; }
.brand-icon { display: inline-flex; width: 32px; height: 32px; background: var(--green); color: #fff; margin-right: 10px; align-items: center; justify-content: center; border-radius: 50%; font: 22px var(--math); }
.course { font-size: 11px; letter-spacing: 1.1px; font-weight: 700; flex: 1; text-transform: uppercase; color: var(--muted); }
.course span, .eyebrow span { color: #8b9a8e; margin: 0 8px; }
#lecture { font-size: 13px; }
#lecture[aria-pressed="true"] { background: var(--green); color: #fff; border-color: var(--green); }
main { max-width: 1680px; margin: auto; padding: 0 4vw; }
.intro { display: flex; justify-content: space-between; align-items: center; padding: 30px 0 24px; }
.eyebrow { font-size: 11px; letter-spacing: 1.4px; font-weight: 750; margin: 0 0 10px; text-transform: uppercase; color: #3f5a4d; }
h1 { font-size: clamp(30px, 3vw, 44px); font-weight: 500; letter-spacing: -1.4px; line-height: 1.15; margin: 0 0 10px; }
h1 em { font-family: var(--math); font-weight: 400; color: var(--green); }
.intro p:last-child { margin: 0; color: var(--muted); font-size: 15px; }
.intro-mark { font: italic 28px/1.5 var(--math); transform: rotate(-6deg); padding: 0 32px; color: var(--green); }
.intro-mark span { color: #6e8275; }

/* ---- workspace tabs ---- */
.workspaces { display: flex; align-items: stretch; border-bottom: 1px solid var(--line); gap: 8px; }
.workspace-tab { border: 0; border-radius: 8px 8px 0 0; background: transparent; padding: 14px 22px; font-size: 17px; }
.workspace-tab.active { background: var(--green); color: #fff; }
.workspace-tab.active:hover { background: var(--green); }
.workspace-tab > span { font: 12px var(--mono); margin-right: 10px; opacity: .75; }
.workspace-tab small { font-size: 12px; font-weight: 400; margin-left: 14px; opacity: .85; }
.guide-link { margin-left: auto; border: 0; background: transparent; font-size: 13px; font-weight: 500; }
.guide-link span { display: inline-block; background: #e1e7dc; border-radius: 50%; width: 22px; height: 22px; line-height: 22px; margin-left: 6px; text-align: center; }

/* ---- layout ---- */
.app-layout { display: grid; grid-template-columns: 300px minmax(0, 1fr); border: 1px solid var(--line); border-top: 0; border-radius: 0 0 8px 8px; background: var(--white); min-height: 640px; }
.formula-panel { padding: 22px 20px; border-right: 1px solid var(--line); min-width: 0; }
.panel-heading { display: flex; align-items: center; justify-content: space-between; gap: 8px; margin-bottom: 16px; }
.panel-heading .eyebrow { margin: 0; }
.pill { font: 11px var(--mono); border: 1px solid #b4c6b6; background: #edf3e8; border-radius: 20px; padding: 3px 9px; white-space: nowrap; }
label { display: block; font-size: 13px; font-weight: 650; margin-bottom: 6px; }
select, textarea, input[type=text] { width: 100%; background: #fff; border: 1px solid #a9b7ab; border-radius: 6px; padding: 8px 9px; font-size: 14px; }
textarea, input[type=text] { font-family: var(--mono); }
textarea { resize: vertical; line-height: 1.55; }
.caption { font-size: 13px; color: var(--muted); line-height: 1.5; margin: 8px 0 14px; }
#clause-list { display: grid; gap: 6px; }
.clause { display: flex; gap: 12px; align-items: flex-start; border: 1px solid transparent; border-radius: 6px; background: #f3f4ec; padding: 7px 10px; width: 100%; text-align: left; font-weight: 400; }
.clause .number { color: var(--muted); font: 12px var(--mono); flex: 0 0 24px; padding-top: 6px; }
.clause-body { display: flex; flex-direction: column; min-width: 0; }
.clause-arrows { font: 15px var(--math); color: var(--green); display: flex; flex-wrap: wrap; gap: 0 14px; }
.clause-arrows > span { white-space: nowrap; }
.clause.pending { opacity: .6; background: transparent; border: 1px dashed #b9c4b9; }
.clause.linked, .clause.hover { border-color: var(--green); background: var(--mint); box-shadow: inset 4px 0 var(--green); }
.clause.wide .math { color: var(--gold); }
.formula-meta { font: 12px var(--mono); color: var(--muted); margin: 10px 0 6px; }
.notes { margin: 0 0 10px; padding-left: 18px; font-size: 13px; color: var(--gold); }
.notes:empty { display: none; }
details { font-size: 14px; }
summary { cursor: pointer; font-weight: 650; padding: 6px 0; }
#editor { border-top: 1px solid var(--line); border-bottom: 1px solid var(--line); padding: 4px 0 8px; margin: 8px 0 16px; }
#editor label { margin-top: 10px; }
#editor button { width: 100%; }
.error { color: var(--coral); font-size: 14px; }
.error:empty { display: none; }
.principle { border-left: 3px solid #b6c9ab; padding-left: 12px; font-size: 13px; color: var(--muted); margin-top: 18px; display: flex; flex-direction: column; gap: 6px; }
.principle .eyebrow { margin: 0; }
.principle .math { font-size: 20px; color: var(--ink); }
.rule-mini { display: inline-flex; flex-direction: column; align-items: center; align-self: flex-start; padding: 2px 6px; }
.rule-mini .premises { border-bottom: 1.5px solid var(--ink); padding: 0 6px 4px; display: flex; gap: 22px; }
.work-area { min-width: 0; }

/* ---- stage navigation and headings ---- */
.stage-nav { display: flex; flex-wrap: wrap; gap: 4px; padding: 14px 22px; border-bottom: 1px solid var(--line); background: #f8f9f2; border-top-right-radius: 8px; }
.stage-nav button { background: transparent; border: 1px solid transparent; color: var(--muted); font-size: 14px; padding: 7px 12px; }
.stage-nav button.active { background: var(--mint); color: var(--green); border-color: #b6cfa9; }
.stage-nav button span { font: 12px var(--mono); margin-right: 8px; display: inline-block; width: 20px; height: 20px; line-height: 19px; border-radius: 50%; border: 1px solid currentColor; text-align: center; }
.canvas-heading { padding: 20px 28px 0; display: flex; align-items: flex-start; justify-content: space-between; gap: 12px; }
.canvas-heading h2, .resolution-head h2, .notice h2 { font-size: 24px; letter-spacing: -.5px; margin: 0 0 4px; font-weight: 600; }
.canvas-heading p, .resolution-head p { font-size: 15px; color: var(--muted); margin: 0; }
.tag { font: 12px var(--mono); white-space: nowrap; padding: 5px 10px; background: #eaefe5; border-radius: 4px; }
.tag.good { background: var(--mint); color: var(--green); font-weight: 700; }

/* ---- graph ---- */
.graph-wrap { padding: 0 12px; }
.graph { width: 100%; height: 320px; display: block; overflow: visible; }
.empty-graph { margin: 26px 28px; padding: 40px 20px; border: 1px dashed var(--line); border-radius: 8px; text-align: center; color: var(--muted); }
.edge { fill: none; stroke: var(--edge); stroke-width: 2.2; }
.edge-hit { fill: none; stroke: transparent; stroke-width: 16; pointer-events: stroke; cursor: pointer; }
.edge.linked, .edge-g.hover .edge { stroke: var(--green); stroke-width: 3.8; }
.edge.trace { stroke: var(--coral); stroke-width: 3.6; }
.edge.trace.current { stroke-width: 5.5; }
.edge.path { stroke: var(--coral); stroke-width: 4.6; }
.ah-plain { fill: var(--edge); } .ah-linked { fill: var(--green); } .ah-trace, .ah-path { fill: var(--coral); }
.edge-label { fill: var(--muted); font: 600 15px var(--mono); paint-order: stroke; stroke: var(--white); stroke-width: 6px; stroke-linejoin: round; pointer-events: none; }
.edge-label.linked, .edge-label.hover { fill: var(--green); font-weight: 800; }
.edge-label.trace, .edge-label.path { fill: var(--coral); font-weight: 800; }
.node { cursor: pointer; }
.node:focus { outline: none; }
.node circle { stroke: var(--green); stroke-width: 2.2; fill: #fff; }
.node text { font: 25px var(--math); fill: var(--ink); pointer-events: none; }
.node:hover circle { fill: #eef4ea; }
.node:focus-visible circle { stroke: var(--focus); stroke-width: 5; }
.node.visited circle { fill: var(--coral-wash); stroke: var(--coral); stroke-width: 3; }
.node.start circle { fill: var(--green); stroke: var(--green); }
.node.start text { fill: #fff; }
.node.conflict circle { stroke: var(--coral); stroke-width: 5; stroke-dasharray: 7 3; fill: #f6c9b6; }
.node.scc circle { stroke-width: 3.2; }
.node.scc-0 circle, .comp.scc-0.multi { fill: #dbe7fb; stroke: #2a5aa8; background: #dbe7fb; border-color: #2a5aa8; }
.node.scc-1 circle, .comp.scc-1.multi { fill: #fde2c6; stroke: #9a5410; background: #fde2c6; border-color: #9a5410; }
.node.scc-2 circle, .comp.scc-2.multi { fill: #e0efd3; stroke: #3a7428; background: #e0efd3; border-color: #3a7428; }
.node.scc-3 circle, .comp.scc-3.multi { fill: #efdcf4; stroke: #773b8b; background: #efdcf4; border-color: #773b8b; }
.node.scc-4 circle, .comp.scc-4.multi { fill: #d6efee; stroke: #1d6f6b; background: #d6efee; border-color: #1d6f6b; }
.node.scc-5 circle, .comp.scc-5.multi { fill: #f8dbe0; stroke: #9c374c; background: #f8dbe0; border-color: #9c374c; }
.node.scc-6 circle, .comp.scc-6.multi { fill: #ebe5cf; stroke: #665622; background: #ebe5cf; border-color: #665622; }
.node.scc-7 circle, .comp.scc-7.multi { fill: #e0e0f5; stroke: #474796; background: #e0e0f5; border-color: #474796; }
.node.scc-bad circle { stroke: var(--coral); stroke-width: 5; stroke-dasharray: 7 3; }
.badge rect { fill: #fff; stroke: #7e8f84; stroke-width: 1.2; }
.badge text { font: 700 12px var(--mono); fill: var(--ink); }
.graph-legend { display: flex; flex-wrap: wrap; justify-content: center; gap: 6px 20px; font-size: 13px; color: var(--muted); margin: 0 20px 14px; }
.graph-legend > span { display: inline-flex; align-items: center; gap: 6px; }
.legend-line { display: inline-block; width: 26px; height: 0; border-top: 2.5px solid var(--edge); }
.legend-line.linked { border-top: 4px solid var(--green); }
.legend-line.path { border-top: 4px solid var(--coral); }
.legend-dot { display: inline-block; width: 13px; height: 13px; border: 2px solid var(--green); border-radius: 50%; background: #fff; }
.legend-dot.start { background: var(--green); }
.legend-dot.visited { background: var(--coral-wash); border-color: var(--coral); }
.legend-dot.conflict { background: #f6c9b6; border: 2px dashed var(--coral); }
.legend-dot.scc { background: #dbe7fb; border-color: #2a5aa8; }

/* ---- stage panels ---- */
.stage-panel { padding-bottom: 20px; }
.control-strip { display: flex; align-items: center; justify-content: space-between; flex-wrap: wrap; gap: 10px; border-top: 1px solid var(--line); padding: 14px 28px; }
.control-strip > div { display: flex; flex-wrap: wrap; gap: 6px; align-items: center; }
.step-count { font: 13px var(--mono); color: var(--muted); }
.check { display: inline-flex; align-items: center; gap: 8px; font-weight: 500; font-size: 14px; margin: 0; cursor: pointer; }
.check input { width: 18px; height: 18px; margin: 0; }
.explanation { background: var(--wash); padding: 16px 22px; margin: 0 28px 16px; border-radius: 8px; font-size: 16px; }
.explanation .eyebrow { margin-bottom: 6px; }
.explanation p { margin: 4px 0; }
.explanation .math { font-size: 24px; }
.two-arrows { display: flex; gap: 34px; flex-wrap: wrap; margin-top: 6px; }
.two-arrows .subtle { margin: 0; }
.next-row { display: flex; align-items: center; justify-content: space-between; gap: 12px; flex-wrap: wrap; margin: 0 28px; color: var(--muted); }
.trace-controls { padding: 16px 28px 4px; display: flex; gap: 12px; align-items: center; flex-wrap: wrap; border-top: 1px solid var(--line); }
.trace-controls label { margin: 0; white-space: nowrap; font-size: 15px; }
.trace-controls select { max-width: 200px; font: 20px var(--math); padding: 4px 8px; }
.prediction { display: flex; gap: 8px; align-items: center; margin: 12px 28px; flex-wrap: wrap; font-size: 15px; }
.prediction > span { margin-right: 6px; font-weight: 600; }
.prediction button { min-width: 78px; }
.prediction .chosen { border-color: var(--green); background: var(--mint); box-shadow: inset 0 0 0 1px var(--green); }
.consequences { margin: 4px 28px 14px; padding-left: 26px; font-size: 15px; }
.consequences li { padding: 3px 0; }
.consequences .math { font-size: 20px; }
.consequences li.hit { color: var(--coral); font-weight: 600; }
.cref { font: 15px var(--math); color: var(--muted); }
.callout { background: var(--wash); padding: 14px 18px; border-radius: 8px; font-size: 15px; margin: 0 28px 12px; border-left: 4px solid var(--green); }
.callout.warn { background: var(--gold-wash); border-left-color: var(--gold); }
.callout p { margin: 4px 0 8px; }
.decision { padding: 4px 28px 22px; }
.decision > p { font-size: 16px; }
.stage-panel.decision .prediction { margin-left: 0; margin-right: 0; }
.result-header { display: flex; align-items: center; gap: 14px; margin: 14px 0; }
.result-badge { font: 700 22px var(--mono); background: var(--green); color: #fff; padding: 8px 16px; border-radius: 6px; letter-spacing: 1px; }
.result-badge.unsat { background: var(--coral); }
.result-header p { margin: 0; font-size: 15px; }
.assignment { display: flex; gap: 10px; margin: 14px 0; flex-wrap: wrap; }
.assignment span { font: 24px var(--math); padding: 8px 16px; border: 1px solid #a9c0a4; border-radius: 6px; background: #eef5e8; }
.path-card { padding: 12px 16px; border: 1px solid var(--line); border-left: 4px solid var(--coral); border-radius: 6px; margin: 12px 0; background: #fff; }
.path-card p { margin: 2px 0 6px; font-size: 16px; }
.path-steps { margin: 4px 0 10px; padding-left: 24px; }
.path-steps li { padding: 2px 0; }
.path-steps .math { font-size: 20px; }
.path-card button { font-size: 13px; }
button.next { margin-top: 8px; color: var(--green); }
.table-wrap { overflow-x: auto; }
table { border-collapse: collapse; width: 100%; font-size: 15px; }
th { text-align: left; color: var(--muted); font-size: 13px; letter-spacing: .3px; font-weight: 650; }
td, th { padding: 9px 12px; border-bottom: 1px solid var(--line); vertical-align: middle; }
.check-table .math, .reach-table .math { font-size: 19px; }
.reach-table { margin: 0 28px; width: calc(100% - 56px); }
.reach-table tr.bad td { background: #fdf0ea; }
.stage-panel > .table-wrap { margin: 0; }
.stage-panel > p.pass, .stage-panel > p.fail { margin: 12px 28px; }
.cost { margin: 12px 28px; font-size: 15px; }
.cost p { margin: 4px 0; }
.scc-box { margin: 16px 28px 10px; padding: 16px 20px; border: 1px solid var(--line); border-radius: 8px; background: #fafbf6; }
.scc-box p { margin: 4px 0 10px; font-size: 15px; }
.scc-box .eyebrow { margin: 0 0 6px; }
.component-list { display: flex; flex-wrap: wrap; gap: 8px; margin: 12px 28px; }
.comp { font: 18px var(--math); border: 1px solid #c3ccc2; border-left-width: 5px; padding: 5px 12px; border-radius: 4px; background: #f3f4ee; }
.comp.bad { outline: 2.5px dashed var(--coral); outline-offset: 2px; }
.stage-panel > p { margin-left: 28px; margin-right: 28px; }
.stage-panel > details.more { margin: 10px 28px; }
.compact { margin: 6px 0; padding-left: 20px; }
.notice { padding: 32px 34px; max-width: 760px; }
.notice p { font-size: 16px; }

/* ---- resolution ---- */
.resolution-head { display: flex; align-items: flex-start; justify-content: space-between; padding: 22px 28px 12px; gap: 12px; }
.proof-table { padding: 0 28px; max-height: 420px; overflow: auto; }
.proof-table table { min-width: 420px; }
.proof-table th:first-child { width: 54px; }
.proof-table td { padding: 5px 11px; }
.proof-table td .math { font-size: 22px; white-space: nowrap; }
.composer.done p { margin: 0; color: var(--muted); }
.proof-table .origin { font-size: 14px; color: var(--muted); }
.proof-table tr.parent td { background: var(--mint); }
.proof-table tr.hinted td { background: var(--gold-wash); }
.proof-table tr.parent.hinted td { background: var(--mint); }
.proof-table tr.latest td { border-bottom-color: #87a17c; }
.proof-table tr.last-input td { border-bottom: 2px solid #9aab9a; }
.proof-table tr.empty td { background: #e2efd9; font-weight: 700; }
.line-button { padding: 3px 9px; border: 1px solid #c3ccc2; font: 13px var(--mono); min-width: 36px; }
.line-button[aria-pressed="true"] { background: var(--green); color: #fff; border-color: var(--green); }
.proof-status { margin: 14px 28px; border: 1px solid #c4ccbb; padding: 11px 16px; border-radius: 6px; font-size: 15px; background: #fafbf6; }
.proof-status.refuted { background: #e4efdb; border-color: #8aa47a; }
.composer { margin: 14px 28px; padding: 16px 20px; background: var(--wash); border-radius: 8px; }
.composer .eyebrow { margin-bottom: 10px; }
.parent-selects { display: grid; grid-template-columns: 1fr 1fr 120px; gap: 12px; }
.parent-selects select { font: 17px var(--math); }
.rule-display { text-align: center; margin: 16px 0 12px; overflow-wrap: anywhere; }
.rule-display .premises { border-bottom: 1.5px solid #6f8370; display: inline-flex; flex-wrap: wrap; justify-content: center; gap: 8px 36px; padding: 0 14px 8px; font-size: 14px; color: var(--muted); }
.rule-display .premises .math { font-size: 22px; color: var(--ink); }
.rule-display .conclusion { padding-top: 6px; }
.rule-display .conclusion .math { font-size: 24px; }
.propose-row { display: flex; gap: 8px; }
.propose-row input { flex: 1; min-width: 0; font: 18px var(--math); }
.feedback { list-style: none; margin: 10px 0 0; padding: 0; font-size: 15px; }
.feedback li { padding: 5px 0 5px 26px; position: relative; }
.feedback li::before { position: absolute; left: 4px; font-weight: 800; }
.feedback li.error { color: #94301a; } .feedback li.error::before { content: '✗'; }
.feedback li.warn { color: var(--gold); } .feedback li.warn::before { content: '!'; left: 8px; }
.feedback li.ok { color: #1f6a35; } .feedback li.ok::before { content: '✓'; }
.composer-actions { display: flex; justify-content: space-between; gap: 12px; margin-top: 12px; flex-wrap: wrap; }
.proof-toolbar { display: flex; gap: 8px; flex-wrap: wrap; align-items: center; padding: 2px 28px 10px; }
.plan-pick { display: inline-flex; align-items: center; gap: 6px; margin: 0 0 0 auto; font-weight: 500; font-size: 13px; }
.plan-pick select { width: auto; font-size: 13px; padding: 5px; }
.hint-card { margin: 0 28px 12px; padding: 12px 16px; border-radius: 8px; background: var(--gold-wash); border-left: 4px solid var(--gold); font-size: 15px; }
.hint-card p { margin: 4px 0 8px; }
.hint-card .math { font-size: 20px; }
.bridge-card { margin: 8px 28px 14px; padding: 12px 16px; border: 1px solid var(--line); border-radius: 8px; font-size: 15px; background: #fafbf6; }
.bridge-card p { margin: 2px 0 8px; }
details.more { margin: 10px 28px; border-top: 1px solid var(--line); padding-top: 4px; font-size: 15px; }
details.more > summary { font-size: 15px; padding: 10px 0; color: var(--green); }
.more-body { padding: 0 0 8px; }
.more-body p { margin: 6px 0 10px; }
.facts { display: grid; grid-template-columns: 200px 1fr; gap: 10px 16px; margin: 6px 0; }
.facts dt { font-weight: 700; }
.facts dd { margin: 0; }
.search-controls { display: flex; gap: 8px; flex-wrap: wrap; align-items: center; margin: 10px 0; }
.search-controls label { margin: 0; }
.search-controls select { width: auto; }
.search-status { padding: 10px 14px; border-radius: 6px; background: #f2f3ec; }
.search-status.unsat, .search-status.sat { background: #e4efdb; }
.search-status.unknown { background: var(--gold-wash); }
.search-list { max-height: 220px; overflow: auto; border: 1px solid var(--line); border-radius: 6px; padding: 6px 10px 6px 0; margin-bottom: 10px; background: #fff; }
.search-list ol { margin: 0; padding-left: 52px; }
.search-list .math { font-size: 18px; }
.certificate-tools { display: flex; gap: 8px; margin: 12px 0; flex-wrap: wrap; align-items: center; }
.file-label { display: inline-block; border: 1px solid #b9c4b9; border-radius: 6px; padding: 8px 14px; font-size: 14px; cursor: pointer; background: var(--white); margin: 0; font-weight: 600; }
.file-label input { position: absolute; opacity: 0; width: 1px; height: 1px; }
.file-label:focus-within { outline: 3px solid var(--focus); outline-offset: 2px; }
#cert-text { font-size: 12px; margin-bottom: 8px; }
.io-message { padding: 9px 12px; border-radius: 6px; }
.io-message.ok { background: #e4efdb; }
.io-message.error { background: var(--coral-wash); color: #8a2c17; }
pre { background: #f2f3ec; padding: 10px 12px; border-radius: 6px; overflow-x: auto; font-size: 13px; }

/* ---- footer and dialog ---- */
footer { display: flex; justify-content: space-between; padding: 18px 0 28px; font-size: 12px; color: var(--muted); gap: 12px; flex-wrap: wrap; }
footer .dot { margin: 0 6px; color: #8b9b8c; }
dialog { border: 1px solid var(--line); border-radius: 12px; max-width: 620px; width: calc(100% - 30px); padding: 30px; color: var(--ink); background: var(--white); box-shadow: 0 20px 60px #152f2c33; }
dialog::backdrop { background: #152f2c66; }
dialog h2 { font-size: 26px; font-weight: 500; letter-spacing: -.5px; margin: 0 0 14px; }
dialog p { font-size: 14px; }
.dialog-close { float: right; border: 0; font-size: 28px; padding: 0 8px; background: transparent; line-height: 1; }
dl { display: grid; grid-template-columns: 110px 1fr; gap: 10px; font-size: 15px; }
dt { font-weight: 650; }
dd { margin: 0; }
.callout:not(.warn) strong { color: var(--green); }

/* ---- lecture mode: projection ---- */
.lecture .intro, .lecture footer { display: none; }
.lecture .topbar { min-height: 56px; }
.lecture .workspaces { margin-top: 12px; }
.lecture body, body.lecture { font-size: 18px; }
.lecture .app-layout { grid-template-columns: 330px minmax(0, 1fr); }
.lecture .math { font-size: 26px; }
.lecture .clause .math { font-size: 25px; }
.lecture .clause-arrows { font-size: 18px; }
.lecture .graph { height: 430px; }
.lecture .edge-label { font-size: 17px; }
.lecture .canvas-heading h2, .lecture .resolution-head h2 { font-size: 30px; }
.lecture .canvas-heading p, .lecture .resolution-head p, .lecture .explanation, .lecture .callout, .lecture .consequences, .lecture .decision > p, .lecture .proof-status, .lecture .hint-card, .lecture .feedback { font-size: 19px; }
.lecture .explanation .math { font-size: 30px; }
.lecture .proof-table td .math { font-size: 27px; }
.lecture .proof-table { max-height: 520px; }
.lecture button { font-size: 16px; }
.lecture .stage-nav button { font-size: 16px; }
.lecture .assignment span { font-size: 30px; }

/* ---- responsive ---- */
@media (min-width: 1500px) { .graph { height: 380px; } }
@media (max-width: 1100px) {
  main, .topbar { padding-left: 22px; padding-right: 22px; }
  .app-layout, .lecture .app-layout { grid-template-columns: 250px minmax(0, 1fr); }
  .workspace-tab small { display: none; }
  .formula-panel { padding: 18px 14px; }
  .canvas-heading, .resolution-head { padding-left: 20px; padding-right: 20px; }
  .control-strip, .trace-controls { padding-left: 20px; padding-right: 20px; }
  .explanation, .callout, .composer, .proof-status, .hint-card, .bridge-card, details.more, .stage-panel > details.more, .cost, .scc-box, .component-list, .next-row, .prediction, .consequences { margin-left: 20px; margin-right: 20px; }
  .proof-table, .proof-toolbar, .pad { padding-left: 20px; padding-right: 20px; }
  .decision { padding-left: 20px; padding-right: 20px; }
  .reach-table { margin: 0 20px; width: calc(100% - 40px); }
  .stage-panel > p { margin-left: 20px; margin-right: 20px; }
  .graph { height: 300px; }
  .intro-mark { display: none; }
  .facts { grid-template-columns: 1fr; gap: 2px; }
  .facts dd { margin-bottom: 8px; }
}
@media (max-width: 820px) {
  body { font-size: 15px; }
  .topbar { min-height: 58px; padding: 0 16px; gap: 14px; }
  .course { display: none; }
  #lecture { margin-left: auto; }
  main { padding: 0 12px; }
  .intro { padding: 20px 4px 16px; }
  h1 { font-size: 30px; letter-spacing: -1px; }
  .workspace-tab { padding: 12px 14px; font-size: 16px; }
  .guide-link { font-size: 0; padding: 10px; }
  .guide-link span { font-size: 14px; }
  .app-layout, .lecture .app-layout { grid-template-columns: 1fr; }
  .formula-panel { border-right: 0; border-bottom: 1px solid var(--line); padding: 16px; }
  #clause-list { grid-template-columns: repeat(auto-fill, minmax(150px, 1fr)); }
  .principle { display: none; }
  .canvas-heading { flex-direction: column; }
  .graph, .lecture .graph { height: 270px; }
  .graph-wrap { padding: 0 4px; }
  .parent-selects { grid-template-columns: 1fr 1fr; }
  .parent-selects > div:last-child { grid-column: 1 / -1; max-width: 200px; }
  .propose-row { flex-wrap: wrap; }
  .propose-row input { flex-basis: 100%; }
  .explanation, .callout, .composer, .proof-status, .hint-card, .bridge-card, details.more, .stage-panel > details.more, .cost, .scc-box, .component-list, .next-row, .prediction, .consequences { margin-left: 14px; margin-right: 14px; }
  .control-strip, .trace-controls, .canvas-heading, .resolution-head, .proof-table, .proof-toolbar, .decision, .pad { padding-left: 14px; padding-right: 14px; }
  .reach-table { margin: 0 14px; width: calc(100% - 28px); }
  .stage-panel > p { margin-left: 14px; margin-right: 14px; }
  .plan-pick { margin-left: 0; }
  footer { flex-direction: column; }
}
@media (prefers-reduced-motion: reduce) {
  *, *::before, *::after { animation: none !important; transition: none !important; scroll-behavior: auto !important; }
}
@media print {
  .topbar, .intro, .workspaces, #editor, button, .composer, .proof-toolbar, footer, .stage-nav, .control-strip, details.more { display: none !important; }
  .app-layout { display: block; border: 0; }
  .formula-panel { border: 0; }
  .proof-table { max-height: none; overflow: visible; }
  body { background: #fff; }
}
.stage-panel.decision > p, .stage-panel.decision > details.more, .stage-panel.decision > .table-wrap { margin-left: 0; margin-right: 0; }
@media (max-width: 600px) {
  .graph-wrap { overflow-x: auto; }
  .graph, .lecture .graph { min-width: calc(var(--cols, 2) * 120px); height: 250px; }
  .proof-table table { min-width: 360px; }
}