citations.svg

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- Created with Inkscape (http://www.inkscape.org/) -->

<svg
   xmlns:dc="http://purl.org/dc/elements/1.1/"
   xmlns:cc="http://creativecommons.org/ns#"
   xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
   xmlns:svg="http://www.w3.org/2000/svg"
   xmlns="http://www.w3.org/2000/svg"
   xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
   xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
   sodipodi:docname="citations.svg"
   viewBox="0 0 760.45215 311.58633"
   height="311.58633"
   width="760.45215"
   xml:space="preserve"
   id="svg2"
   version="1.1"
   inkscape:version="0.92.5 (2060ec1f9f, 2020-04-08)"><metadata
     id="metadata8"><rdf:RDF><cc:Work
         rdf:about=""><dc:format>image/svg+xml</dc:format><dc:type
           rdf:resource="http://purl.org/dc/dcmitype/StillImage" /><dc:title></dc:title></cc:Work></rdf:RDF></metadata><defs
     id="defs6"><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath20"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path18"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath28"><path
         d="M 40,752 H 187.5 V 733 H 40 Z"
         id="path26"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath40"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path38"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath46"><path
         d="M 40,737 H 156.5 V 718 H 40 Z"
         id="path44"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath58"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path56"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath64"><path
         d="M 40,722 H 156.5 V 703 H 40 Z"
         id="path62"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath76"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path74"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath82"><path
         d="M 40,707 H 156.5 V 688 H 40 Z"
         id="path80"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath94"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path92"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath100"><path
         d="m 40,692 h 92.5 V 673 H 40 Z"
         id="path98"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath112"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path110"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath118"><path
         d="M 40,677 H 144.5 V 658 H 40 Z"
         id="path116"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath130"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path128"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath136"><path
         d="M 40,662 H 193 V 643 H 40 Z"
         id="path134"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath148"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path146"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath154"><path
         d="M 40,647 H 162 V 628 H 40 Z"
         id="path152"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath166"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path164"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath172"><path
         d="M 40,632 H 162 V 613 H 40 Z"
         id="path170"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath184"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path182"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath190"><path
         d="M 40,617 H 92.5 V 598 H 40 Z"
         id="path188"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath202"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path200"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath208"><path
         d="m 40,602 h 96 V 583 H 40 Z"
         id="path206"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath220"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path218"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath226"><path
         d="m 40,587 h 96 V 568 H 40 Z"
         id="path224"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath238"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path236"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath244"><path
         d="M 40,572 H 210 V 553 H 40 Z"
         id="path242"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath256"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path254"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath262"><path
         d="M 40,557 H 146 V 538 H 40 Z"
         id="path260"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath274"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path272"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath280"><path
         d="M 40,542 H 155 V 523 H 40 Z"
         id="path278"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath292"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path290"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath298"><path
         d="M 40,527 H 167 V 508 H 40 Z"
         id="path296"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath310"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path308"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath316"><path
         d="M 40,512 H 167 V 493 H 40 Z"
         id="path314"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath328"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path326"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath334"><path
         d="M 40,497 H 167 V 478 H 40 Z"
         id="path332"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath346"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path344"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath352"><path
         d="M 40,482 H 189.5 V 463 H 40 Z"
         id="path350"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath364"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path362"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath370"><path
         d="M 40,467 H 167 V 448 H 40 Z"
         id="path368"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath382"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path380"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath388"><path
         d="M 40,452 H 146 V 433 H 40 Z"
         id="path386"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath400"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path398"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath406"><path
         d="m 40,437 h 99.5 V 418 H 40 Z"
         id="path404"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath418"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path416"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath424"><path
         d="M 40,422 H 191 V 403 H 40 Z"
         id="path422"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath436"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path434"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath442"><path
         d="M 40,407 H 186 V 388 H 40 Z"
         id="path440"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath454"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path452"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath460"><path
         d="M 40,392 H 201.5 V 373 H 40 Z"
         id="path458"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath472"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path470"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath478"><path
         d="M 40,377 H 210 V 358 H 40 Z"
         id="path476"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath490"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path488"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath496"><path
         d="M 40,362 H 170.5 V 343 H 40 Z"
         id="path494"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath508"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path506"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath514"><path
         d="M 40,347 H 215.5 V 328 H 40 Z"
         id="path512"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath526"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path524"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath532"><path
         d="M 40,332 H 243 V 313 H 40 Z"
         id="path530"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath544"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path542"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath550"><path
         d="M 40,317 H 267 V 298 H 40 Z"
         id="path548"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath562"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path560"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath568"><path
         d="M 40,302 H 141 V 283 H 40 Z"
         id="path566"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath580"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path578"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath586"><path
         d="M 40,287 H 156.5 V 268 H 40 Z"
         id="path584"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath598"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path596"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath604"><path
         d="M 40,272 H 167 V 253 H 40 Z"
         id="path602"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath616"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path614"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath622"><path
         d="m 40,257 h 96 V 238 H 40 Z"
         id="path620"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath634"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path632"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath640"><path
         d="M 40,242 H 286 V 223 H 40 Z"
         id="path638"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath652"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path650"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath658"><path
         d="M 40,227 H 224 V 208 H 40 Z"
         id="path656"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath670"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path668"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath676"><path
         d="M 40,212 H 160 V 193 H 40 Z"
         id="path674"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath688"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path686"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath694"><path
         d="M 40,197 H 186 V 178 H 40 Z"
         id="path692"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath706"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path704"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath712"><path
         d="m 40,182 h 89 V 163 H 40 Z"
         id="path710"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath724"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path722"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath730"><path
         d="M 40,167 H 288 V 148 H 40 Z"
         id="path728"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath742"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path740"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath748"><path
         d="M 40,152 H 253.5 V 133 H 40 Z"
         id="path746"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath760"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path758"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath766"><path
         d="M 40,137 H 141 V 118 H 40 Z"
         id="path764"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath778"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path776"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath784"><path
         d="M 40,122 H 144.5 V 103 H 40 Z"
         id="path782"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath796"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path794"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath802"><path
         d="M 40,77 H 153 V 58 H 40 Z"
         id="path800"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath814"><path
         d="M 36,756 H 576 V 36 H 36 Z"
         id="path812"
         inkscape:connector-curvature="0" /></clipPath><clipPath
       clipPathUnits="userSpaceOnUse"
       id="clipPath820"><path
         d="M 40,62 H 184 V 43 H 40 Z"
         id="path818"
         inkscape:connector-curvature="0" /></clipPath></defs><sodipodi:namedview
     pagecolor="#ffffff"
     bordercolor="#666666"
     borderopacity="1"
     objecttolerance="10"
     gridtolerance="10"
     guidetolerance="10"
     inkscape:pageopacity="0"
     inkscape:pageshadow="2"
     inkscape:window-width="2560"
     inkscape:window-height="1548"
     id="namedview4"
     showgrid="false"
     inkscape:zoom="1.2642212"
     inkscape:cx="252.64767"
     inkscape:cy="165.80973"
     inkscape:window-x="0"
     inkscape:window-y="0"
     inkscape:window-maximized="1"
     inkscape:current-layer="g10"
     fit-margin-top="0"
     fit-margin-left="0"
     fit-margin-right="0"
     fit-margin-bottom="0" /><g
     id="g10"
     inkscape:groupmode="layer"
     inkscape:label="citations"
     transform="matrix(1.3333333,0,0,-1.3333333,12.969662,801.33269)"><text
       id="text50"
       style="font-variant:normal;font-size:12.47999954px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.03999996"
       transform="scale(1,-1)"
       x="11.436768"
       y="-422.15735"><tspan
         id="tspan48"
         sodipodi:role="line"
         y="-422.15735"
         x="11.436768 16.828133 24.016611 31.205091 38.406052 45.594532 52.783012 59.971493 67.159981 72.551338 77.955177 85.143654 92.33213 99.520615 106.70909 113.89758 121.08607"
         style="stroke-width:1.03999996">jsCoq+Gallego2016</tspan></text>
<text
       id="text68"
       style="font-variant:normal;font-size:12.47999954px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.03999996"
       transform="scale(1,-1)"
       x="-6.8499227"
       y="-455.8443"><tspan
         id="tspan66"
         sodipodi:role="line"
         y="-455.8443"
         x="-6.8499227 0.33852345 7.527 14.715508 21.903984 29.092461 36.293419 43.481895 48.873253 54.26461 61.453087 68.641563 74.045403 81.233879 88.422386 95.610863 102.79934"
         style="stroke-width:1.03999996">CPDT+Chlipala2013</tspan></text>
<text
       id="text86"
       style="font-variant:normal;font-size:2.87999988px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.24000001"
       transform="scale(1,-1)"
       x="288.435"
       y="-467.93784"><tspan
         id="tspan84"
         sodipodi:role="line"
         y="-467.93784"
         x="288.435 290.0939 291.75278 293.41165 295.07053 296.7294 298.39117 300.05005 301.29419 302.53836 304.19724 305.85611 307.10315 308.76205 310.42093 312.0798 313.73868"
         style="stroke-width:0.24000001">FRAP+Chlipala2015</tspan></text>
<text
       id="text104"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="59.833984"
       y="-546.00696"><tspan
         id="tspan102"
         sodipodi:role="line"
         y="-546.00696"
         x="59.833984 65.363586 70.893181 76.422783 81.952385 86.109184 91.638786 97.168381 102.69798 108.22758 113.75718 119.28679 124.81639"
         style="stroke-width:0.80000001">SF+Pierce2018</tspan></text>
<text
       id="text122"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="434.58344"
       y="-451.66251"><tspan
         id="tspan120"
         sodipodi:role="line"
         y="-451.66251"
         x="434.58344 440.11304 444.26022 449.78983 455.32904 460.85864 466.38824 471.91782 477.44742 481.59464 487.12424 492.65384 498.18344 503.72269 509.25229"
         style="stroke-width:0.80000001">Flocq+Boldo2011</tspan></text>
<text
       id="text140"
       style="font-variant:normal;font-size:12.47999954px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.03999996"
       transform="scale(1,-1)"
       x="163.15106"
       y="-591.66449"><tspan
         id="tspan138"
         sodipodi:role="line"
         y="-591.66449"
         x="163.15106 172.13667 179.32515 186.51363 193.7021 200.89058 208.07907 217.06467 224.25314 231.44164 240.42723 247.61571 254.80418 261.99265 269.18112 276.38208 283.57059 288.96194 296.15042 303.3389 310.52737"
         style="stroke-width:1.03999996">MathComp+Mahboubi2018</tspan></text>
<text
       id="text158"
       style="font-variant:normal;font-size:7.67999983px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.63999999"
       transform="scale(1,-1)"
       x="153.0188"
       y="-514.42017"><tspan
         id="tspan156"
         sodipodi:role="line"
         y="-514.42017"
         x="153.0188 157.44247 161.86615 166.28983 170.71352 175.13719 179.56856 183.99223 188.41591 192.8396 197.26328 201.68695 206.11063 210.53432 214.95799 219.38167 223.80534"
         style="stroke-width:0.63999999">PeaCoq+Robert2018</tspan></text>
<text
       id="text176"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="266.71887"
       y="-516.65302"><tspan
         id="tspan174"
         sodipodi:role="line"
         y="-516.65302"
         x="266.71887 272.24847 277.77808 283.30768 288.83728 294.36688 299.90607 305.43567 310.96527 316.49487 322.02448 327.55408 333.08368 338.61328 344.14288 349.67249 355.20206"
         style="stroke-width:0.80000001">CoqArt+Bertot2004</tspan></text>
<text
       id="text248"
       style="font-variant:normal;font-size:7.67999983px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.63999999"
       transform="scale(1,-1)"
       x="302.20868"
       y="-442.87543"><tspan
         id="tspan246"
         sodipodi:role="line"
         y="-442.87543"
         x="302.20868 306.63235 311.05603 315.47974 319.90341 324.32709 328.75845 333.18213 337.6058 342.02948 346.45316 350.87683 354.19461 358.61829 363.04196 367.46564 371.897 375.21475 379.63843 384.06213 387.37988 390.70532 395.129 399.55267 403.97635"
         style="stroke-width:0.63999999">ProofGeneral+Aspinall2000</tspan></text>
<text
       id="text266"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="356.43533"
       y="-428.31226"><tspan
         id="tspan264"
         sodipodi:role="line"
         y="-428.31226"
         x="356.43533 361.96494 367.49454 373.02414 378.55374 384.08334 389.62253 395.15213 400.68173 404.82895 410.35855 415.88815 421.41772 426.94733 432.47693"
         style="stroke-width:0.80000001">Dafny+Leino2014</tspan></text>
<text
       id="text284"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="117.8613"
       y="-443.69781"><tspan
         id="tspan282"
         sodipodi:role="line"
         y="-443.69781"
         x="117.8613 123.3909 128.92046 134.45006 139.97966 145.50926 151.04846 156.57806 162.10767 167.63727 173.16687 178.69646 184.22606 189.75566 195.28526 200.81487"
         style="stroke-width:0.80000001">CoqPSV+Frank2020</tspan></text>
<text
       id="text302"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="463.21014"
       y="-534.69617"><tspan
         id="tspan300"
         sodipodi:role="line"
         y="-534.69617"
         x="463.21014 468.73975 472.88693 478.41653 483.95575 489.48535 495.01495 500.54456 506.07416 511.60373 517.13348 522.66309 528.19269 533.72229 539.25189 544.78143 550.32068 555.85028"
         style="stroke-width:0.80000001">Literate+Knuth1984</tspan></text>
<text
       id="text320"
       style="font-variant:normal;font-size:8.06400013px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.67199999"
       transform="scale(1,-1)"
       x="313.20627"
       y="-477.52988"><tspan
         id="tspan318"
         sodipodi:role="line"
         y="-477.52988"
         x="313.20627 317.85114 321.33478 325.97964 330.6326 335.27747 339.9223 344.56717 349.21204 353.8569 358.50174 363.14664 367.7915 372.43637 377.08121 381.72607 386.379 391.0239"
         style="stroke-width:0.67199999">Literate+Knuth1992</tspan></text>
<text
       id="text338"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="335.25363"
       y="-463.06711"><tspan
         id="tspan336"
         sodipodi:role="line"
         y="-463.06711"
         x="335.25363 340.7832 344.93042 350.46002 355.99921 361.52881 367.05841 372.58801 378.11761 383.64722 389.17682 396.08881 400.23602 405.76562 411.29523 416.82483 422.36401 427.89362"
         style="stroke-width:0.80000001">Literate+Smith1991</tspan></text>
<text
       id="text356"
       style="font-variant:normal;font-size:7.67999983px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.63999999"
       transform="scale(1,-1)"
       x="397.75552"
       y="-525.04016"><tspan
         id="tspan354"
         sodipodi:role="line"
         y="-525.04016"
         x="397.75552 402.1792 406.60287 411.02655 415.45023 419.8739 425.4035 429.82718 434.25089 438.68222 443.10593 447.5296 451.95328 456.37695 460.80063 464.11838 468.54208 472.96576 477.38943 481.8208 486.24448"
         style="stroke-width:0.63999999">ProofWeb+Hendriks2010</tspan></text>
<text
       id="text374"
       style="font-variant:normal;font-size:7.67999983px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.63999999"
       transform="scale(1,-1)"
       x="359.25076"
       y="-505.60562"><tspan
         id="tspan372"
         sodipodi:role="line"
         y="-505.60562"
         x="359.25076 363.67444 368.09811 372.52179 376.9455 381.36917 385.80054 390.22421 394.64789 399.07156 402.38931 406.81302 411.23669 415.66037 420.08405 424.50787 428.93921 433.36292"
         style="stroke-width:0.63999999">Czar+Corbineau2008</tspan></text>
<text
       id="text392"
       style="font-variant:normal;font-size:10.07999992px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.83999997"
       transform="scale(1,-1)"
       x="158.41331"
       y="-367.39041"><tspan
         id="tspan390"
         sodipodi:role="line"
         y="-367.39041"
         x="158.41331 162.76788 168.57396 174.38004 180.1962 186.00229 193.2498 199.06596 204.87204 210.67812 216.48421 220.83876 226.64484 232.45093 238.257"
         style="stroke-width:0.83999997">Isar+Wenzel1999</tspan></text>
<text
       id="text410"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="297.05688"
       y="-532.27478"><tspan
         id="tspan408"
         sodipodi:role="line"
         y="-532.27478"
         x="297.05688 301.2041 306.7337 312.26331 317.80249 323.33209 328.86169 334.3913 339.9209 345.4505 350.9801 356.5097 362.03928 367.56888"
         style="stroke-width:0.80000001">Isar+Bauer2001</tspan></text>
<text
       id="text428"
       style="font-variant:normal;font-size:14.39999962px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.20000005"
       transform="scale(1,-1)"
       x="324.41684"
       y="-576.91174"><tspan
         id="tspan426"
         sodipodi:role="line"
         y="-576.91174"
         x="324.41684 334.78485 341.00565 349.30005 357.59445 365.88885 374.18326 380.41846 388.71286 397.00726 405.30167 413.59607 423.96405 430.18484 438.47925 446.77365 453.00885 459.22964 467.52405 475.81845 484.11285 492.40726"
         style="stroke-width:1.20000005">MizarLight+Wiedijk2001</tspan></text>
<text
       id="text446"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="-10.495247"
       y="-513.0155"><tspan
         id="tspan444"
         sodipodi:role="line"
         y="-513.0155"
         x="-10.495247 -3.5832431 0.56395853 6.0935612 11.623161 17.152767 22.682354 28.221554 32.368755 37.898357 43.427959 48.957561 54.487164 60.016766 64.173561 69.703163 75.232765 80.762352 86.291954 91.821556 97.351143"
         style="stroke-width:0.80000001">MizarHol+Harrison1996</tspan></text>
<text
       id="text464"
       style="font-variant:normal;font-size:6.71999979px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.56"
       transform="scale(1,-1)"
       x="418.44861"
       y="-565.10156"><tspan
         id="tspan462"
         sodipodi:role="line"
         y="-565.10156"
         x="418.44861 422.31934 426.19006 430.06079 433.93149 437.80222 441.67966 445.55038 449.42111 453.29181 457.16254 461.03326 464.90399 467.80701 471.67773 475.54846 479.4259 483.29663 487.16733 491.03806 494.90878 498.77951 502.65021"
         style="stroke-width:0.56">StructuredCalc+Back1997</tspan></text>
<text
       id="text482"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="60.695805"
       y="-400.16879"><tspan
         id="tspan480"
         sodipodi:role="line"
         y="-400.16879"
         x="60.695805 66.22541 71.755005 77.284607 82.814209 88.343811 93.883011 99.412605 104.94221 110.47181 116.00142 121.53101 127.06061 132.59016 138.11977 143.64937 149.17897 154.70857 160.24777 165.77737 171.30698 176.83656 182.36617 187.89577"
         style="stroke-width:0.80000001">StructuredHOL+Grundy1997</tspan></text>
<text
       id="text500"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="255.34889"
       y="-565.85016"><tspan
         id="tspan498"
         sodipodi:role="line"
         y="-565.85016"
         x="255.34889 262.26089 266.40811 271.93771 277.46729 282.99689 288.52649 295.43851 300.96811 306.49771 312.0369 317.5665 323.0961 328.6257 334.1553 339.68491 345.21451 350.74411"
         style="stroke-width:0.80000001">MizarXML+Urban2005</tspan></text>
<text
       id="text518"
       style="font-variant:normal;font-size:6.71999979px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.56"
       transform="scale(1,-1)"
       x="193.90108"
       y="-456.01202"><tspan
         id="tspan516"
         sodipodi:role="line"
         y="-456.01202"
         x="193.90108 197.77179 201.64252 205.51323 209.38396 213.25467 217.13211 221.00284 223.90587 227.7766 231.64731 236.48572 239.38875 243.25948 247.13019 251.00092 254.87836 258.74908 262.61978 266.49051 270.36124 274.23196 278.10266 281.97339 285.84412"
         style="stroke-width:0.56">PresentingMizar+Urban2007</tspan></text>
<text
       id="text536"
       style="font-variant:normal;font-size:12.47999954px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.03999996"
       transform="scale(1,-1)"
       x="82.026314"
       y="-497.42477"><tspan
         id="tspan534"
         sodipodi:role="line"
         y="-497.42477"
         x="82.026314 89.21479 96.403275 103.59175 110.78024 116.18407 123.37255 130.561 137.7495 144.93797 152.12645 159.31493 164.70628 171.90726 179.09573 184.48709 191.67557 198.86404 206.05252 213.24101 218.64485 224.03621 231.2247 238.41316 245.60165 252.79013 259.97861 267.16708 274.35556 281.55652"
         style="stroke-width:1.03999996">PredicateCalculus+Dijkstra1990</tspan></text>
<text
       y="-411.77551"
       x="198.79524"
       id="text554"
       style="font-variant:normal;font-size:12.4800005px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.03999996"
       transform="scale(1,-1)"><tspan
         style="stroke-width:1.03999996"
         id="tspan552"
         sodipodi:role="line"
         y="-411.77551"
         x="198.79524 205.98372 213.1722 220.36069 227.54916 234.73764 241.9386 249.12708 256.31555 263.50406 270.69254 277.88098 286.86661 294.05508 301.24356 308.43204 315.62051 322.80899 329.99747 337.18594 344.37445 351.57541 358.76389 365.95236 373.14084 380.32932 387.51779 394.7063 401.89474 409.08322 416.27173 423.46021">ShapeOfArguments+VanGasteren1990</tspan></text>
<text
       id="text572"
       style="font-variant:normal;font-size:12.28800011px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.02399993"
       transform="scale(1,-1)"
       x="212.20595"
       y="-476.04688"><tspan
         id="tspan570"
         sodipodi:role="line"
         y="-476.04688"
         x="212.20595 219.28383 226.36174 233.43962 240.5175 247.5954 254.68556 261.76349 268.84137 275.91928 282.99716 290.07504 297.15292 304.2308"
         style="stroke-width:1.02399993">LCF+Gordon1979</tspan></text>
<text
       id="text590"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="454.88089"
       y="-476.42892"><tspan
         id="tspan588"
         sodipodi:role="line"
         y="-476.42892"
         x="454.88089 460.41049 465.94009 471.4697 476.99927 482.52887 488.06808 493.59769 500.50009 506.03928 511.56888 517.09863 522.62817 528.15778 533.68738 539.21698"
         style="stroke-width:0.80000001">Lean+deMoura2015</tspan></text>
<text
       id="text608"
       style="font-variant:normal;font-size:11.52000046px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.96000004"
       transform="scale(1,-1)"
       x="173.86351"
       y="-429.52725"><tspan
         id="tspan606"
         sodipodi:role="line"
         y="-429.52725"
         x="173.86351 182.15791 187.13457 193.77008 200.40561 207.04112 213.67665 220.32368 226.9592 233.5947 240.23022 246.86575 251.84241 258.47794 265.11343 271.74896 278.396 285.03152"
         style="stroke-width:0.96000004">Mizar+Trybulec1985</tspan></text>
<text
       id="text626"
       style="font-variant:normal;font-size:17.27999878px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.44000006"
       transform="scale(1,-1)"
       x="343.65607"
       y="-545.76526"><tspan
         id="tspan624"
         sodipodi:role="line"
         y="-545.76526"
         x="343.65607 356.09769 366.05096 376.00424 385.95749 395.91077 405.86407 415.81735 425.77063 435.72391 445.67719 455.63049 465.58377"
         style="stroke-width:1.44000006">Web+Knuth1984</tspan></text>
<text
       id="text644"
       style="font-variant:normal;font-size:11.52000046px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.96000004"
       transform="scale(1,-1)"
       x="22.791147"
       y="-528.38287"><tspan
         id="tspan642"
         sodipodi:role="line"
         y="-528.38287"
         x="22.791147 29.426664 36.062187 42.697704 49.333229 55.96875 62.615788 69.251297 75.886818 82.522339 89.15786 95.793365 102.4289 109.06441 115.69995 120.67657 127.3236 133.95912 138.93578 145.57129 152.20682 158.84233 165.47786 170.46602 175.44264 182.07817 188.71368 195.34921 200.32585 208.62025 215.25575 221.89128 228.53835 235.17384 241.80937 248.44489"
         style="stroke-width:0.96000004">ProofPresentationIsabelle+Simons1997</tspan></text>
<text
       id="text662"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="192.181"
       y="-545.1474"><tspan
         id="tspan660"
         sodipodi:role="line"
         y="-545.1474"
         x="192.181 197.7106 203.2402 208.76981 215.68179 221.2114 225.3586 230.8978 236.4274 241.957 247.4866 253.0162 258.54581 262.69299 268.2226 273.7522 279.29141 284.82101 291.72339 297.2626 302.79221 308.32181 313.85141 319.38101 324.91061 330.44022"
         style="stroke-width:0.80000001">ExampleCentric+Edwards2004</tspan></text>
<text
       id="text680"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="353.58429"
       y="-398.77966"><tspan
         id="tspan678"
         sodipodi:role="line"
         y="-398.77966"
         x="353.58429 359.11389 364.64349 370.1731 374.3299 379.8595 385.3891 390.9187 397.83069 403.36029 408.88989 414.41949 418.56668 424.09628 429.62589 435.15549 440.6947"
         style="stroke-width:0.80000001">Poplar+Morris1980</tspan></text>
<text
       id="text698"
       style="font-variant:normal;font-size:14.39999962px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.20000005"
       transform="scale(1,-1)"
       x="175.65727"
       y="-383.4769"><tspan
         id="tspan696"
         sodipodi:role="line"
         y="-383.4769"
         x="175.65727 183.95168 192.24608 200.54047 206.77567 215.07007 223.36447 231.65887 239.95328 246.17407 254.46849 262.76285 271.05725 279.36606 287.66046 295.95486 304.24927 312.54367 320.83807 329.13248 337.42685"
         style="stroke-width:1.20000005">Prolog+Eisenstadt1990</tspan></text>
<text
       id="text716"
       style="font-variant:normal;font-size:14.39999962px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.20000005"
       transform="scale(1,-1)"
       x="141.58409"
       y="-558.29095"><tspan
         id="tspan714"
         sodipodi:role="line"
         y="-558.29095"
         x="141.58409 149.87849 158.1729 166.4673 174.76169 183.05609 191.35049 199.6449 210.01289 218.3073 226.6017 234.8961"
         style="stroke-width:1.20000005">PVS+Crow1995</tspan></text>
<text
       id="text734"
       style="font-variant:normal;font-size:8.06400013px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.67199999"
       transform="scale(1,-1)"
       x="46.78775"
       y="-474.06839"><tspan
         id="tspan732"
         sodipodi:role="line"
         y="-474.06839"
         x="46.78775 51.432617 57.238689 61.883556 66.528419 71.173279 75.818146 80.463013 83.95472 88.599586 93.244461 97.88932 102.53417 107.17903 111.8239 116.46876 121.11362 125.75849 130.40335 135.05627 139.70114 144.34601 148.99088 153.63573 158.28061 162.92546 167.57031 173.3764 178.02126 182.66614 187.311 191.95586 196.60074 201.24559 205.89851"
         style="stroke-width:0.67199999">TwentyFirstCenturyProof+Lamport2012</tspan></text>
<text
       id="text752"
       style="font-variant:normal;font-size:12.47999954px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:1.03999996"
       transform="scale(1,-1)"
       x="331.96674"
       y="-489.87021"><tspan
         id="tspan750"
         sodipodi:role="line"
         y="-489.87021"
         x="331.96674 337.35809 344.54657 351.73505 358.93604 366.12451 373.31299 378.70435 385.89282 393.0813 400.26978 405.67361 412.86209 420.05057 427.23907 434.42755 443.41315 450.60162 457.7901 464.97858 472.16705 479.35553 484.75937 493.73251 500.92099 508.12195 515.31055 520.7019 527.89038 535.07886 542.26733"
         style="stroke-width:1.03999996">IntensionalSoftware+Simonyi2006</tspan></text>
<text
       id="text770"
       style="font-variant:normal;font-size:9.2159996px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.76800001"
       transform="scale(1,-1)"
       x="79.810379"
       y="-576.75476"><tspan
         id="tspan768"
         sodipodi:role="line"
         y="-576.75476"
         x="79.810379 85.118805 90.427216 95.735634 101.04406 106.35246 111.6701 116.97852 122.28694 127.59536 132.90373 138.21214 143.52055 148.82898"
         style="stroke-width:0.76800001">PnP+Sergey2014</tspan></text>
<text
       id="text788"
       style="font-variant:normal;font-size:9.60000038px;font-family:'Iosevka Sparkle';-inkscape-font-specification:Iosevka-Sparkle;writing-mode:lr-tb;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.80000001"
       transform="scale(1,-1)"
       x="464.08539"
       y="-510.60004"><tspan
         id="tspan786"
         sodipodi:role="line"
         y="-510.60004"
         x="464.08539 469.61499 475.14459 480.67419 486.2038 491.7334 497.27261 501.4198 506.9494 512.47913 516.62634 522.15594 527.68555 533.22473 538.75433"
         style="stroke-width:0.80000001">Brady+Idris2013</tspan></text>
</g></svg>