results/002bmc-apalache-nclauses.svg

<?xml version="1.0" encoding="utf-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
  "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<svg xmlns:xlink="http://www.w3.org/1999/xlink" width="460.8pt" height="345.6pt" viewBox="0 0 460.8 345.6" xmlns="http://www.w3.org/2000/svg" version="1.1">
 <metadata>
  <rdf:RDF 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#">
   <cc:Work>
    <dc:type rdf:resource="http://purl.org/dc/dcmitype/StillImage"/>
    <dc:date>2022-01-18T17:44:51.826996</dc:date>
    <dc:format>image/svg+xml</dc:format>
    <dc:creator>
     <cc:Agent>
      <dc:title>Matplotlib v3.5.0, https://matplotlib.org/</dc:title>
     </cc:Agent>
    </dc:creator>
   </cc:Work>
  </rdf:RDF>
 </metadata>
 <defs>
  <style type="text/css">*{stroke-linejoin: round; stroke-linecap: butt}</style>
 </defs>
 <g id="figure_1">
  <g id="patch_1">
   <path d="M 0 345.6 
L 460.8 345.6 
L 460.8 0 
L 0 0 
z
" style="fill: #ffffff"/>
  </g>
  <g id="axes_1">
   <g id="patch_2">
    <path d="M 57.6 307.584 
L 414.72 307.584 
L 414.72 41.472 
L 57.6 41.472 
z
" style="fill: #ffffff"/>
   </g>
   <g id="matplotlib.axis_1">
    <g id="xtick_1">
     <g id="line2d_1">
      <path d="M 95.476364 307.584 
L 95.476364 41.472 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_2">
      <defs>
       <path id="m572c3282c2" d="M 0 0 
L 0 3.5 
" style="stroke: #000000; stroke-width: 0.8"/>
      </defs>
      <g>
       <use xlink:href="#m572c3282c2" x="95.476364" y="307.584" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_1">
      <!-- 2 -->
      <g transform="translate(92.295114 322.182437)scale(0.1 -0.1)">
       <defs>
        <path id="DejaVuSans-32" d="M 1228 531 
L 3431 531 
L 3431 0 
L 469 0 
L 469 531 
Q 828 903 1448 1529 
Q 2069 2156 2228 2338 
Q 2531 2678 2651 2914 
Q 2772 3150 2772 3378 
Q 2772 3750 2511 3984 
Q 2250 4219 1831 4219 
Q 1534 4219 1204 4116 
Q 875 4013 500 3803 
L 500 4441 
Q 881 4594 1212 4672 
Q 1544 4750 1819 4750 
Q 2544 4750 2975 4387 
Q 3406 4025 3406 3419 
Q 3406 3131 3298 2873 
Q 3191 2616 2906 2266 
Q 2828 2175 2409 1742 
Q 1991 1309 1228 531 
z
" transform="scale(0.015625)"/>
       </defs>
       <use xlink:href="#DejaVuSans-32"/>
      </g>
     </g>
    </g>
    <g id="xtick_2">
     <g id="line2d_3">
      <path d="M 138.763636 307.584 
L 138.763636 41.472 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_4">
      <g>
       <use xlink:href="#m572c3282c2" x="138.763636" y="307.584" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_2">
      <!-- 4 -->
      <g transform="translate(135.582386 322.182437)scale(0.1 -0.1)">
       <defs>
        <path id="DejaVuSans-34" d="M 2419 4116 
L 825 1625 
L 2419 1625 
L 2419 4116 
z
M 2253 4666 
L 3047 4666 
L 3047 1625 
L 3713 1625 
L 3713 1100 
L 3047 1100 
L 3047 0 
L 2419 0 
L 2419 1100 
L 313 1100 
L 313 1709 
L 2253 4666 
z
" transform="scale(0.015625)"/>
       </defs>
       <use xlink:href="#DejaVuSans-34"/>
      </g>
     </g>
    </g>
    <g id="xtick_3">
     <g id="line2d_5">
      <path d="M 182.050909 307.584 
L 182.050909 41.472 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_6">
      <g>
       <use xlink:href="#m572c3282c2" x="182.050909" y="307.584" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_3">
      <!-- 6 -->
      <g transform="translate(178.869659 322.182437)scale(0.1 -0.1)">
       <defs>
        <path id="DejaVuSans-36" d="M 2113 2584 
Q 1688 2584 1439 2293 
Q 1191 2003 1191 1497 
Q 1191 994 1439 701 
Q 1688 409 2113 409 
Q 2538 409 2786 701 
Q 3034 994 3034 1497 
Q 3034 2003 2786 2293 
Q 2538 2584 2113 2584 
z
M 3366 4563 
L 3366 3988 
Q 3128 4100 2886 4159 
Q 2644 4219 2406 4219 
Q 1781 4219 1451 3797 
Q 1122 3375 1075 2522 
Q 1259 2794 1537 2939 
Q 1816 3084 2150 3084 
Q 2853 3084 3261 2657 
Q 3669 2231 3669 1497 
Q 3669 778 3244 343 
Q 2819 -91 2113 -91 
Q 1303 -91 875 529 
Q 447 1150 447 2328 
Q 447 3434 972 4092 
Q 1497 4750 2381 4750 
Q 2619 4750 2861 4703 
Q 3103 4656 3366 4563 
z
" transform="scale(0.015625)"/>
       </defs>
       <use xlink:href="#DejaVuSans-36"/>
      </g>
     </g>
    </g>
    <g id="xtick_4">
     <g id="line2d_7">
      <path d="M 225.338182 307.584 
L 225.338182 41.472 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_8">
      <g>
       <use xlink:href="#m572c3282c2" x="225.338182" y="307.584" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_4">
      <!-- 8 -->
      <g transform="translate(222.156932 322.182437)scale(0.1 -0.1)">
       <defs>
        <path id="DejaVuSans-38" d="M 2034 2216 
Q 1584 2216 1326 1975 
Q 1069 1734 1069 1313 
Q 1069 891 1326 650 
Q 1584 409 2034 409 
Q 2484 409 2743 651 
Q 3003 894 3003 1313 
Q 3003 1734 2745 1975 
Q 2488 2216 2034 2216 
z
M 1403 2484 
Q 997 2584 770 2862 
Q 544 3141 544 3541 
Q 544 4100 942 4425 
Q 1341 4750 2034 4750 
Q 2731 4750 3128 4425 
Q 3525 4100 3525 3541 
Q 3525 3141 3298 2862 
Q 3072 2584 2669 2484 
Q 3125 2378 3379 2068 
Q 3634 1759 3634 1313 
Q 3634 634 3220 271 
Q 2806 -91 2034 -91 
Q 1263 -91 848 271 
Q 434 634 434 1313 
Q 434 1759 690 2068 
Q 947 2378 1403 2484 
z
M 1172 3481 
Q 1172 3119 1398 2916 
Q 1625 2713 2034 2713 
Q 2441 2713 2670 2916 
Q 2900 3119 2900 3481 
Q 2900 3844 2670 4047 
Q 2441 4250 2034 4250 
Q 1625 4250 1398 4047 
Q 1172 3844 1172 3481 
z
" transform="scale(0.015625)"/>
       </defs>
       <use xlink:href="#DejaVuSans-38"/>
      </g>
     </g>
    </g>
    <g id="xtick_5">
     <g id="line2d_9">
      <path d="M 268.625455 307.584 
L 268.625455 41.472 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_10">
      <g>
       <use xlink:href="#m572c3282c2" x="268.625455" y="307.584" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_5">
      <!-- 10 -->
      <g transform="translate(262.262955 322.182437)scale(0.1 -0.1)">
       <defs>
        <path id="DejaVuSans-31" d="M 794 531 
L 1825 531 
L 1825 4091 
L 703 3866 
L 703 4441 
L 1819 4666 
L 2450 4666 
L 2450 531 
L 3481 531 
L 3481 0 
L 794 0 
L 794 531 
z
" transform="scale(0.015625)"/>
        <path id="DejaVuSans-30" d="M 2034 4250 
Q 1547 4250 1301 3770 
Q 1056 3291 1056 2328 
Q 1056 1369 1301 889 
Q 1547 409 2034 409 
Q 2525 409 2770 889 
Q 3016 1369 3016 2328 
Q 3016 3291 2770 3770 
Q 2525 4250 2034 4250 
z
M 2034 4750 
Q 2819 4750 3233 4129 
Q 3647 3509 3647 2328 
Q 3647 1150 3233 529 
Q 2819 -91 2034 -91 
Q 1250 -91 836 529 
Q 422 1150 422 2328 
Q 422 3509 836 4129 
Q 1250 4750 2034 4750 
z
" transform="scale(0.015625)"/>
       </defs>
       <use xlink:href="#DejaVuSans-31"/>
       <use xlink:href="#DejaVuSans-30" x="63.623047"/>
      </g>
     </g>
    </g>
    <g id="xtick_6">
     <g id="line2d_11">
      <path d="M 311.912727 307.584 
L 311.912727 41.472 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_12">
      <g>
       <use xlink:href="#m572c3282c2" x="311.912727" y="307.584" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_6">
      <!-- 12 -->
      <g transform="translate(305.550227 322.182437)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-31"/>
       <use xlink:href="#DejaVuSans-32" x="63.623047"/>
      </g>
     </g>
    </g>
    <g id="xtick_7">
     <g id="line2d_13">
      <path d="M 355.2 307.584 
L 355.2 41.472 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_14">
      <g>
       <use xlink:href="#m572c3282c2" x="355.2" y="307.584" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_7">
      <!-- 14 -->
      <g transform="translate(348.8375 322.182437)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-31"/>
       <use xlink:href="#DejaVuSans-34" x="63.623047"/>
      </g>
     </g>
    </g>
    <g id="xtick_8">
     <g id="line2d_15">
      <path d="M 398.487273 307.584 
L 398.487273 41.472 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_16">
      <g>
       <use xlink:href="#m572c3282c2" x="398.487273" y="307.584" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_8">
      <!-- 16 -->
      <g transform="translate(392.124773 322.182437)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-31"/>
       <use xlink:href="#DejaVuSans-36" x="63.623047"/>
      </g>
     </g>
    </g>
    <g id="text_9">
     <!-- benchmark -->
     <g transform="translate(207.937344 335.860562)scale(0.1 -0.1)">
      <defs>
       <path id="DejaVuSans-62" d="M 3116 1747 
Q 3116 2381 2855 2742 
Q 2594 3103 2138 3103 
Q 1681 3103 1420 2742 
Q 1159 2381 1159 1747 
Q 1159 1113 1420 752 
Q 1681 391 2138 391 
Q 2594 391 2855 752 
Q 3116 1113 3116 1747 
z
M 1159 2969 
Q 1341 3281 1617 3432 
Q 1894 3584 2278 3584 
Q 2916 3584 3314 3078 
Q 3713 2572 3713 1747 
Q 3713 922 3314 415 
Q 2916 -91 2278 -91 
Q 1894 -91 1617 61 
Q 1341 213 1159 525 
L 1159 0 
L 581 0 
L 581 4863 
L 1159 4863 
L 1159 2969 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-65" d="M 3597 1894 
L 3597 1613 
L 953 1613 
Q 991 1019 1311 708 
Q 1631 397 2203 397 
Q 2534 397 2845 478 
Q 3156 559 3463 722 
L 3463 178 
Q 3153 47 2828 -22 
Q 2503 -91 2169 -91 
Q 1331 -91 842 396 
Q 353 884 353 1716 
Q 353 2575 817 3079 
Q 1281 3584 2069 3584 
Q 2775 3584 3186 3129 
Q 3597 2675 3597 1894 
z
M 3022 2063 
Q 3016 2534 2758 2815 
Q 2500 3097 2075 3097 
Q 1594 3097 1305 2825 
Q 1016 2553 972 2059 
L 3022 2063 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-6e" d="M 3513 2113 
L 3513 0 
L 2938 0 
L 2938 2094 
Q 2938 2591 2744 2837 
Q 2550 3084 2163 3084 
Q 1697 3084 1428 2787 
Q 1159 2491 1159 1978 
L 1159 0 
L 581 0 
L 581 3500 
L 1159 3500 
L 1159 2956 
Q 1366 3272 1645 3428 
Q 1925 3584 2291 3584 
Q 2894 3584 3203 3211 
Q 3513 2838 3513 2113 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-63" d="M 3122 3366 
L 3122 2828 
Q 2878 2963 2633 3030 
Q 2388 3097 2138 3097 
Q 1578 3097 1268 2742 
Q 959 2388 959 1747 
Q 959 1106 1268 751 
Q 1578 397 2138 397 
Q 2388 397 2633 464 
Q 2878 531 3122 666 
L 3122 134 
Q 2881 22 2623 -34 
Q 2366 -91 2075 -91 
Q 1284 -91 818 406 
Q 353 903 353 1747 
Q 353 2603 823 3093 
Q 1294 3584 2113 3584 
Q 2378 3584 2631 3529 
Q 2884 3475 3122 3366 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-68" d="M 3513 2113 
L 3513 0 
L 2938 0 
L 2938 2094 
Q 2938 2591 2744 2837 
Q 2550 3084 2163 3084 
Q 1697 3084 1428 2787 
Q 1159 2491 1159 1978 
L 1159 0 
L 581 0 
L 581 4863 
L 1159 4863 
L 1159 2956 
Q 1366 3272 1645 3428 
Q 1925 3584 2291 3584 
Q 2894 3584 3203 3211 
Q 3513 2838 3513 2113 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-6d" d="M 3328 2828 
Q 3544 3216 3844 3400 
Q 4144 3584 4550 3584 
Q 5097 3584 5394 3201 
Q 5691 2819 5691 2113 
L 5691 0 
L 5113 0 
L 5113 2094 
Q 5113 2597 4934 2840 
Q 4756 3084 4391 3084 
Q 3944 3084 3684 2787 
Q 3425 2491 3425 1978 
L 3425 0 
L 2847 0 
L 2847 2094 
Q 2847 2600 2669 2842 
Q 2491 3084 2119 3084 
Q 1678 3084 1418 2786 
Q 1159 2488 1159 1978 
L 1159 0 
L 581 0 
L 581 3500 
L 1159 3500 
L 1159 2956 
Q 1356 3278 1631 3431 
Q 1906 3584 2284 3584 
Q 2666 3584 2933 3390 
Q 3200 3197 3328 2828 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-61" d="M 2194 1759 
Q 1497 1759 1228 1600 
Q 959 1441 959 1056 
Q 959 750 1161 570 
Q 1363 391 1709 391 
Q 2188 391 2477 730 
Q 2766 1069 2766 1631 
L 2766 1759 
L 2194 1759 
z
M 3341 1997 
L 3341 0 
L 2766 0 
L 2766 531 
Q 2569 213 2275 61 
Q 1981 -91 1556 -91 
Q 1019 -91 701 211 
Q 384 513 384 1019 
Q 384 1609 779 1909 
Q 1175 2209 1959 2209 
L 2766 2209 
L 2766 2266 
Q 2766 2663 2505 2880 
Q 2244 3097 1772 3097 
Q 1472 3097 1187 3025 
Q 903 2953 641 2809 
L 641 3341 
Q 956 3463 1253 3523 
Q 1550 3584 1831 3584 
Q 2591 3584 2966 3190 
Q 3341 2797 3341 1997 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-72" d="M 2631 2963 
Q 2534 3019 2420 3045 
Q 2306 3072 2169 3072 
Q 1681 3072 1420 2755 
Q 1159 2438 1159 1844 
L 1159 0 
L 581 0 
L 581 3500 
L 1159 3500 
L 1159 2956 
Q 1341 3275 1631 3429 
Q 1922 3584 2338 3584 
Q 2397 3584 2469 3576 
Q 2541 3569 2628 3553 
L 2631 2963 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-6b" d="M 581 4863 
L 1159 4863 
L 1159 1991 
L 2875 3500 
L 3609 3500 
L 1753 1863 
L 3688 0 
L 2938 0 
L 1159 1709 
L 1159 0 
L 581 0 
L 581 4863 
z
" transform="scale(0.015625)"/>
      </defs>
      <use xlink:href="#DejaVuSans-62"/>
      <use xlink:href="#DejaVuSans-65" x="63.476562"/>
      <use xlink:href="#DejaVuSans-6e" x="125"/>
      <use xlink:href="#DejaVuSans-63" x="188.378906"/>
      <use xlink:href="#DejaVuSans-68" x="243.359375"/>
      <use xlink:href="#DejaVuSans-6d" x="306.738281"/>
      <use xlink:href="#DejaVuSans-61" x="404.150391"/>
      <use xlink:href="#DejaVuSans-72" x="465.429688"/>
      <use xlink:href="#DejaVuSans-6b" x="506.542969"/>
     </g>
    </g>
   </g>
   <g id="matplotlib.axis_2">
    <g id="ytick_1">
     <g id="line2d_17">
      <path d="M 57.6 295.660974 
L 414.72 295.660974 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_18">
      <defs>
       <path id="mc5bc4b2d30" d="M 0 0 
L -3.5 0 
" style="stroke: #000000; stroke-width: 0.8"/>
      </defs>
      <g>
       <use xlink:href="#mc5bc4b2d30" x="57.6" y="295.660974" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_10">
      <!-- 0 -->
      <g transform="translate(44.2375 299.460193)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-30"/>
      </g>
     </g>
    </g>
    <g id="ytick_2">
     <g id="line2d_19">
      <path d="M 57.6 257.560936 
L 414.72 257.560936 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_20">
      <g>
       <use xlink:href="#mc5bc4b2d30" x="57.6" y="257.560936" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_11">
      <!-- 100000 -->
      <g transform="translate(12.425 261.360155)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-31"/>
       <use xlink:href="#DejaVuSans-30" x="63.623047"/>
       <use xlink:href="#DejaVuSans-30" x="127.246094"/>
       <use xlink:href="#DejaVuSans-30" x="190.869141"/>
       <use xlink:href="#DejaVuSans-30" x="254.492188"/>
       <use xlink:href="#DejaVuSans-30" x="318.115234"/>
      </g>
     </g>
    </g>
    <g id="ytick_3">
     <g id="line2d_21">
      <path d="M 57.6 219.460899 
L 414.72 219.460899 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_22">
      <g>
       <use xlink:href="#mc5bc4b2d30" x="57.6" y="219.460899" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_12">
      <!-- 200000 -->
      <g transform="translate(12.425 223.260117)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-32"/>
       <use xlink:href="#DejaVuSans-30" x="63.623047"/>
       <use xlink:href="#DejaVuSans-30" x="127.246094"/>
       <use xlink:href="#DejaVuSans-30" x="190.869141"/>
       <use xlink:href="#DejaVuSans-30" x="254.492188"/>
       <use xlink:href="#DejaVuSans-30" x="318.115234"/>
      </g>
     </g>
    </g>
    <g id="ytick_4">
     <g id="line2d_23">
      <path d="M 57.6 181.360861 
L 414.72 181.360861 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_24">
      <g>
       <use xlink:href="#mc5bc4b2d30" x="57.6" y="181.360861" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_13">
      <!-- 300000 -->
      <g transform="translate(12.425 185.16008)scale(0.1 -0.1)">
       <defs>
        <path id="DejaVuSans-33" d="M 2597 2516 
Q 3050 2419 3304 2112 
Q 3559 1806 3559 1356 
Q 3559 666 3084 287 
Q 2609 -91 1734 -91 
Q 1441 -91 1130 -33 
Q 819 25 488 141 
L 488 750 
Q 750 597 1062 519 
Q 1375 441 1716 441 
Q 2309 441 2620 675 
Q 2931 909 2931 1356 
Q 2931 1769 2642 2001 
Q 2353 2234 1838 2234 
L 1294 2234 
L 1294 2753 
L 1863 2753 
Q 2328 2753 2575 2939 
Q 2822 3125 2822 3475 
Q 2822 3834 2567 4026 
Q 2313 4219 1838 4219 
Q 1578 4219 1281 4162 
Q 984 4106 628 3988 
L 628 4550 
Q 988 4650 1302 4700 
Q 1616 4750 1894 4750 
Q 2613 4750 3031 4423 
Q 3450 4097 3450 3541 
Q 3450 3153 3228 2886 
Q 3006 2619 2597 2516 
z
" transform="scale(0.015625)"/>
       </defs>
       <use xlink:href="#DejaVuSans-33"/>
       <use xlink:href="#DejaVuSans-30" x="63.623047"/>
       <use xlink:href="#DejaVuSans-30" x="127.246094"/>
       <use xlink:href="#DejaVuSans-30" x="190.869141"/>
       <use xlink:href="#DejaVuSans-30" x="254.492188"/>
       <use xlink:href="#DejaVuSans-30" x="318.115234"/>
      </g>
     </g>
    </g>
    <g id="ytick_5">
     <g id="line2d_25">
      <path d="M 57.6 143.260823 
L 414.72 143.260823 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_26">
      <g>
       <use xlink:href="#mc5bc4b2d30" x="57.6" y="143.260823" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_14">
      <!-- 400000 -->
      <g transform="translate(12.425 147.060042)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-34"/>
       <use xlink:href="#DejaVuSans-30" x="63.623047"/>
       <use xlink:href="#DejaVuSans-30" x="127.246094"/>
       <use xlink:href="#DejaVuSans-30" x="190.869141"/>
       <use xlink:href="#DejaVuSans-30" x="254.492188"/>
       <use xlink:href="#DejaVuSans-30" x="318.115234"/>
      </g>
     </g>
    </g>
    <g id="ytick_6">
     <g id="line2d_27">
      <path d="M 57.6 105.160785 
L 414.72 105.160785 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_28">
      <g>
       <use xlink:href="#mc5bc4b2d30" x="57.6" y="105.160785" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_15">
      <!-- 500000 -->
      <g transform="translate(12.425 108.960004)scale(0.1 -0.1)">
       <defs>
        <path id="DejaVuSans-35" d="M 691 4666 
L 3169 4666 
L 3169 4134 
L 1269 4134 
L 1269 2991 
Q 1406 3038 1543 3061 
Q 1681 3084 1819 3084 
Q 2600 3084 3056 2656 
Q 3513 2228 3513 1497 
Q 3513 744 3044 326 
Q 2575 -91 1722 -91 
Q 1428 -91 1123 -41 
Q 819 9 494 109 
L 494 744 
Q 775 591 1075 516 
Q 1375 441 1709 441 
Q 2250 441 2565 725 
Q 2881 1009 2881 1497 
Q 2881 1984 2565 2268 
Q 2250 2553 1709 2553 
Q 1456 2553 1204 2497 
Q 953 2441 691 2322 
L 691 4666 
z
" transform="scale(0.015625)"/>
       </defs>
       <use xlink:href="#DejaVuSans-35"/>
       <use xlink:href="#DejaVuSans-30" x="63.623047"/>
       <use xlink:href="#DejaVuSans-30" x="127.246094"/>
       <use xlink:href="#DejaVuSans-30" x="190.869141"/>
       <use xlink:href="#DejaVuSans-30" x="254.492188"/>
       <use xlink:href="#DejaVuSans-30" x="318.115234"/>
      </g>
     </g>
    </g>
    <g id="ytick_7">
     <g id="line2d_29">
      <path d="M 57.6 67.060747 
L 414.72 67.060747 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #b0b0b0; stroke-opacity: 0.2; stroke-width: 0.8; stroke-linecap: square"/>
     </g>
     <g id="line2d_30">
      <g>
       <use xlink:href="#mc5bc4b2d30" x="57.6" y="67.060747" style="stroke: #000000; stroke-width: 0.8"/>
      </g>
     </g>
     <g id="text_16">
      <!-- 600000 -->
      <g transform="translate(12.425 70.859966)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-36"/>
       <use xlink:href="#DejaVuSans-30" x="63.623047"/>
       <use xlink:href="#DejaVuSans-30" x="127.246094"/>
       <use xlink:href="#DejaVuSans-30" x="190.869141"/>
       <use xlink:href="#DejaVuSans-30" x="254.492188"/>
       <use xlink:href="#DejaVuSans-30" x="318.115234"/>
      </g>
     </g>
    </g>
    <g id="text_17">
     <!-- number of SMT clauses -->
     <g transform="translate(6.345312 232.828)rotate(-90)scale(0.1 -0.1)">
      <defs>
       <path id="DejaVuSans-75" d="M 544 1381 
L 544 3500 
L 1119 3500 
L 1119 1403 
Q 1119 906 1312 657 
Q 1506 409 1894 409 
Q 2359 409 2629 706 
Q 2900 1003 2900 1516 
L 2900 3500 
L 3475 3500 
L 3475 0 
L 2900 0 
L 2900 538 
Q 2691 219 2414 64 
Q 2138 -91 1772 -91 
Q 1169 -91 856 284 
Q 544 659 544 1381 
z
M 1991 3584 
L 1991 3584 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-20" transform="scale(0.015625)"/>
       <path id="DejaVuSans-6f" d="M 1959 3097 
Q 1497 3097 1228 2736 
Q 959 2375 959 1747 
Q 959 1119 1226 758 
Q 1494 397 1959 397 
Q 2419 397 2687 759 
Q 2956 1122 2956 1747 
Q 2956 2369 2687 2733 
Q 2419 3097 1959 3097 
z
M 1959 3584 
Q 2709 3584 3137 3096 
Q 3566 2609 3566 1747 
Q 3566 888 3137 398 
Q 2709 -91 1959 -91 
Q 1206 -91 779 398 
Q 353 888 353 1747 
Q 353 2609 779 3096 
Q 1206 3584 1959 3584 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-66" d="M 2375 4863 
L 2375 4384 
L 1825 4384 
Q 1516 4384 1395 4259 
Q 1275 4134 1275 3809 
L 1275 3500 
L 2222 3500 
L 2222 3053 
L 1275 3053 
L 1275 0 
L 697 0 
L 697 3053 
L 147 3053 
L 147 3500 
L 697 3500 
L 697 3744 
Q 697 4328 969 4595 
Q 1241 4863 1831 4863 
L 2375 4863 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-53" d="M 3425 4513 
L 3425 3897 
Q 3066 4069 2747 4153 
Q 2428 4238 2131 4238 
Q 1616 4238 1336 4038 
Q 1056 3838 1056 3469 
Q 1056 3159 1242 3001 
Q 1428 2844 1947 2747 
L 2328 2669 
Q 3034 2534 3370 2195 
Q 3706 1856 3706 1288 
Q 3706 609 3251 259 
Q 2797 -91 1919 -91 
Q 1588 -91 1214 -16 
Q 841 59 441 206 
L 441 856 
Q 825 641 1194 531 
Q 1563 422 1919 422 
Q 2459 422 2753 634 
Q 3047 847 3047 1241 
Q 3047 1584 2836 1778 
Q 2625 1972 2144 2069 
L 1759 2144 
Q 1053 2284 737 2584 
Q 422 2884 422 3419 
Q 422 4038 858 4394 
Q 1294 4750 2059 4750 
Q 2388 4750 2728 4690 
Q 3069 4631 3425 4513 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-4d" d="M 628 4666 
L 1569 4666 
L 2759 1491 
L 3956 4666 
L 4897 4666 
L 4897 0 
L 4281 0 
L 4281 4097 
L 3078 897 
L 2444 897 
L 1241 4097 
L 1241 0 
L 628 0 
L 628 4666 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-54" d="M -19 4666 
L 3928 4666 
L 3928 4134 
L 2272 4134 
L 2272 0 
L 1638 0 
L 1638 4134 
L -19 4134 
L -19 4666 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-6c" d="M 603 4863 
L 1178 4863 
L 1178 0 
L 603 0 
L 603 4863 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-73" d="M 2834 3397 
L 2834 2853 
Q 2591 2978 2328 3040 
Q 2066 3103 1784 3103 
Q 1356 3103 1142 2972 
Q 928 2841 928 2578 
Q 928 2378 1081 2264 
Q 1234 2150 1697 2047 
L 1894 2003 
Q 2506 1872 2764 1633 
Q 3022 1394 3022 966 
Q 3022 478 2636 193 
Q 2250 -91 1575 -91 
Q 1294 -91 989 -36 
Q 684 19 347 128 
L 347 722 
Q 666 556 975 473 
Q 1284 391 1588 391 
Q 1994 391 2212 530 
Q 2431 669 2431 922 
Q 2431 1156 2273 1281 
Q 2116 1406 1581 1522 
L 1381 1569 
Q 847 1681 609 1914 
Q 372 2147 372 2553 
Q 372 3047 722 3315 
Q 1072 3584 1716 3584 
Q 2034 3584 2315 3537 
Q 2597 3491 2834 3397 
z
" transform="scale(0.015625)"/>
      </defs>
      <use xlink:href="#DejaVuSans-6e"/>
      <use xlink:href="#DejaVuSans-75" x="63.378906"/>
      <use xlink:href="#DejaVuSans-6d" x="126.757812"/>
      <use xlink:href="#DejaVuSans-62" x="224.169922"/>
      <use xlink:href="#DejaVuSans-65" x="287.646484"/>
      <use xlink:href="#DejaVuSans-72" x="349.169922"/>
      <use xlink:href="#DejaVuSans-20" x="390.283203"/>
      <use xlink:href="#DejaVuSans-6f" x="422.070312"/>
      <use xlink:href="#DejaVuSans-66" x="483.251953"/>
      <use xlink:href="#DejaVuSans-20" x="518.457031"/>
      <use xlink:href="#DejaVuSans-53" x="550.244141"/>
      <use xlink:href="#DejaVuSans-4d" x="613.720703"/>
      <use xlink:href="#DejaVuSans-54" x="700"/>
      <use xlink:href="#DejaVuSans-20" x="761.083984"/>
      <use xlink:href="#DejaVuSans-63" x="792.871094"/>
      <use xlink:href="#DejaVuSans-6c" x="847.851562"/>
      <use xlink:href="#DejaVuSans-61" x="875.634766"/>
      <use xlink:href="#DejaVuSans-75" x="936.914062"/>
      <use xlink:href="#DejaVuSans-73" x="1000.292969"/>
      <use xlink:href="#DejaVuSans-65" x="1052.392578"/>
      <use xlink:href="#DejaVuSans-73" x="1113.916016"/>
     </g>
    </g>
   </g>
   <g id="line2d_31">
    <path d="M 73.832727 295.280355 
L 95.476364 293.123893 
L 117.12 277.266276 
L 138.763636 197.421551 
L 160.407273 53.568 
L 182.050909 291.95765 
L 203.694545 283.950928 
L 225.338182 282.995379 
L 246.981818 241.605784 
L 268.625455 212.994941 
L 290.269091 88.465349 
L 311.912727 291.674948 
L 333.556364 289.585923 
L 355.2 276.482558 
L 376.843636 265.527654 
L 398.487273 125.769477 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #ff0000; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
    <defs>
     <path id="m290c578787" d="M -3 3 
L 3 3 
L 3 -3 
L -3 -3 
z
" style="stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </defs>
    <g clip-path="url(#paae626c28e)">
     <use xlink:href="#m290c578787" x="73.832727" y="295.280355" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="95.476364" y="293.123893" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="117.12" y="277.266276" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="138.763636" y="197.421551" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="160.407273" y="53.568" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="182.050909" y="291.95765" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="203.694545" y="283.950928" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="225.338182" y="282.995379" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="246.981818" y="241.605784" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="268.625455" y="212.994941" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="290.269091" y="88.465349" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="311.912727" y="291.674948" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="333.556364" y="289.585923" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="355.2" y="276.482558" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="376.843636" y="265.527654" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m290c578787" x="398.487273" y="125.769477" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </g>
   </g>
   <g id="line2d_32">
    <path d="M 73.832727 295.265496 
L 95.476364 292.875099 
L 117.12 281.204296 
L 138.763636 202.967392 
L 160.407273 67.850942 
L 182.050909 293.395165 
L 203.694545 288.500453 
L 225.338182 287.266774 
L 246.981818 255.468101 
L 268.625455 234.028829 
L 290.269091 146.433794 
L 311.912727 291.587318 
L 333.556364 289.538298 
L 355.2 278.723983 
L 376.843636 268.372584 
L 398.487273 199.12386 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #0000ff; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
    <defs>
     <path id="mc912abb91b" d="M 0 3 
C 0.795609 3 1.55874 2.683901 2.12132 2.12132 
C 2.683901 1.55874 3 0.795609 3 0 
C 3 -0.795609 2.683901 -1.55874 2.12132 -2.12132 
C 1.55874 -2.683901 0.795609 -3 0 -3 
C -0.795609 -3 -1.55874 -2.683901 -2.12132 -2.12132 
C -2.683901 -1.55874 -3 -0.795609 -3 0 
C -3 0.795609 -2.683901 1.55874 -2.12132 2.12132 
C -1.55874 2.683901 -0.795609 3 0 3 
z
" style="stroke: #0000ff; stroke-opacity: 0.7"/>
    </defs>
    <g clip-path="url(#paae626c28e)">
     <use xlink:href="#mc912abb91b" x="73.832727" y="295.265496" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="95.476364" y="292.875099" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="117.12" y="281.204296" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="138.763636" y="202.967392" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="160.407273" y="67.850942" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="182.050909" y="293.395165" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="203.694545" y="288.500453" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="225.338182" y="287.266774" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="246.981818" y="255.468101" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="268.625455" y="234.028829" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="290.269091" y="146.433794" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="311.912727" y="291.587318" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="333.556364" y="289.538298" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="355.2" y="278.723983" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="376.843636" y="268.372584" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     <use xlink:href="#mc912abb91b" x="398.487273" y="199.12386" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
    </g>
   </g>
   <g id="line2d_33">
    <path d="M 73.832727 295.486476 
L 95.476364 294.682565 
L 117.12 288.5336 
L 138.763636 249.847965 
L 160.407273 182.852096 
L 182.050909 294.825821 
L 203.694545 293.57614 
L 225.338182 293.070934 
L 246.981818 286.725753 
L 268.625455 280.350855 
L 290.269091 267.471518 
L 311.912727 293.821123 
L 333.556364 292.957776 
L 355.2 285.956133 
L 376.843636 279.731348 
L 398.487273 233.521337 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #008000; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
    <defs>
     <path id="m174d52aab2" d="M 0 -3 
L -3 3 
L 3 3 
z
" style="stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </defs>
    <g clip-path="url(#paae626c28e)">
     <use xlink:href="#m174d52aab2" x="73.832727" y="295.486476" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="95.476364" y="294.682565" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="117.12" y="288.5336" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="138.763636" y="249.847965" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="160.407273" y="182.852096" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="182.050909" y="294.825821" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="203.694545" y="293.57614" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="225.338182" y="293.070934" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="246.981818" y="286.725753" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="268.625455" y="280.350855" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="290.269091" y="267.471518" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="311.912727" y="293.821123" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="333.556364" y="292.957776" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="355.2" y="285.956133" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="376.843636" y="279.731348" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m174d52aab2" x="398.487273" y="233.521337" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </g>
   </g>
   <g id="line2d_34">
    <path d="M 73.832727 295.488 
L 95.476364 294.682565 
L 117.12 288.549221 
L 138.763636 250.723885 
L 160.407273 183.789738 
L 182.050909 294.843347 
L 203.694545 293.608525 
L 225.338182 293.071315 
L 246.981818 286.726134 
L 268.625455 280.368762 
L 290.269091 267.490568 
L 311.912727 293.902657 
L 333.556364 292.973017 
L 355.2 288.004772 
L 376.843636 283.081485 
L 398.487273 253.073514 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #bf00bf; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
    <defs>
     <path id="m03e963d4b3" d="M -0 3 
L 3 -3 
L -3 -3 
z
" style="stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </defs>
    <g clip-path="url(#paae626c28e)">
     <use xlink:href="#m03e963d4b3" x="73.832727" y="295.488" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="95.476364" y="294.682565" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="117.12" y="288.549221" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="138.763636" y="250.723885" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="160.407273" y="183.789738" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="182.050909" y="294.843347" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="203.694545" y="293.608525" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="225.338182" y="293.071315" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="246.981818" y="286.726134" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="268.625455" y="280.368762" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="290.269091" y="267.490568" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="311.912727" y="293.902657" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="333.556364" y="292.973017" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="355.2" y="288.004772" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="376.843636" y="283.081485" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m03e963d4b3" x="398.487273" y="253.073514" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </g>
   </g>
   <g id="line2d_35">
    <path d="M 73.832727 295.265496 
L 95.476364 292.875099 
L 117.12 281.204296 
L 138.763636 237.673098 
L 160.407273 153.552786 
L 182.050909 293.395165 
L 203.694545 288.500453 
L 225.338182 287.266774 
L 246.981818 255.468101 
L 268.625455 234.028829 
L 290.269091 146.433794 
L 311.912727 291.587318 
L 333.556364 289.538298 
L 355.2 278.713315 
L 376.843636 268.372584 
L 398.487273 199.12386 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #000000; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
    <defs>
     <path id="maea95cfc86" d="M -0 4.242641 
L 4.242641 0 
L 0 -4.242641 
L -4.242641 -0 
z
" style="stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </defs>
    <g clip-path="url(#paae626c28e)">
     <use xlink:href="#maea95cfc86" x="73.832727" y="295.265496" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="95.476364" y="292.875099" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="117.12" y="281.204296" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="138.763636" y="237.673098" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="160.407273" y="153.552786" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="182.050909" y="293.395165" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="203.694545" y="288.500453" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="225.338182" y="287.266774" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="246.981818" y="255.468101" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="268.625455" y="234.028829" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="290.269091" y="146.433794" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="311.912727" y="291.587318" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="333.556364" y="289.538298" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="355.2" y="278.713315" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="376.843636" y="268.372584" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#maea95cfc86" x="398.487273" y="199.12386" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </g>
   </g>
   <g id="line2d_36">
    <path d="M 73.832727 295.477332 
L 95.476364 294.679136 
L 117.12 288.532838 
L 138.763636 250.236966 
L 160.407273 183.789738 
L 182.050909 294.846776 
L 203.694545 293.622622 
L 225.338182 293.112463 
L 246.981818 286.767282 
L 268.625455 281.359363 
L 290.269091 269.592166 
L 311.912727 293.946853 
L 333.556364 293.027881 
L 355.2 287.815033 
L 376.843636 283.267413 
L 398.487273 233.533529 
" clip-path="url(#paae626c28e)" style="fill: none; stroke: #00bfbf; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
    <defs>
     <path id="m45fc077255" d="M -3 -0 
L 3 3 
L 3 -3 
z
" style="stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </defs>
    <g clip-path="url(#paae626c28e)">
     <use xlink:href="#m45fc077255" x="73.832727" y="295.477332" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="95.476364" y="294.679136" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="117.12" y="288.532838" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="138.763636" y="250.236966" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="160.407273" y="183.789738" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="182.050909" y="294.846776" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="203.694545" y="293.622622" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="225.338182" y="293.112463" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="246.981818" y="286.767282" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="268.625455" y="281.359363" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="290.269091" y="269.592166" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="311.912727" y="293.946853" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="333.556364" y="293.027881" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="355.2" y="287.815033" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="376.843636" y="283.267413" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     <use xlink:href="#m45fc077255" x="398.487273" y="233.533529" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
    </g>
   </g>
   <g id="patch_3">
    <path d="M 57.6 307.584 
L 57.6 41.472 
" style="fill: none; stroke: #000000; stroke-width: 0.8; stroke-linejoin: miter; stroke-linecap: square"/>
   </g>
   <g id="patch_4">
    <path d="M 414.72 307.584 
L 414.72 41.472 
" style="fill: none; stroke: #000000; stroke-width: 0.8; stroke-linejoin: miter; stroke-linecap: square"/>
   </g>
   <g id="patch_5">
    <path d="M 57.6 307.584 
L 414.72 307.584 
" style="fill: none; stroke: #000000; stroke-width: 0.8; stroke-linejoin: miter; stroke-linecap: square"/>
   </g>
   <g id="patch_6">
    <path d="M 57.6 41.472 
L 414.72 41.472 
" style="fill: none; stroke: #000000; stroke-width: 0.8; stroke-linejoin: miter; stroke-linecap: square"/>
   </g>
   <g id="legend_1">
    <g id="patch_7">
     <path d="M 250.523125 137.54075 
L 407.72 137.54075 
Q 409.72 137.54075 409.72 135.54075 
L 409.72 48.472 
Q 409.72 46.472 407.72 46.472 
L 250.523125 46.472 
Q 248.523125 46.472 248.523125 48.472 
L 248.523125 135.54075 
Q 248.523125 137.54075 250.523125 137.54075 
z
" style="fill: #ffffff; opacity: 0.8; stroke: #cccccc; stroke-linejoin: miter"/>
    </g>
    <g id="line2d_37">
     <path d="M 252.523125 54.570438 
L 262.523125 54.570438 
L 272.523125 54.570438 
" style="fill: none; stroke: #ff0000; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
     <g>
      <use xlink:href="#m290c578787" x="262.523125" y="54.570438" style="fill: #ff0000; fill-opacity: 0.7; stroke: #ff0000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     </g>
    </g>
    <g id="text_18">
     <!-- 002bmc-apalache-0.5.2 -->
     <g transform="translate(280.523125 58.070438)scale(0.1 -0.1)">
      <defs>
       <path id="DejaVuSans-2d" d="M 313 2009 
L 1997 2009 
L 1997 1497 
L 313 1497 
L 313 2009 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-70" d="M 1159 525 
L 1159 -1331 
L 581 -1331 
L 581 3500 
L 1159 3500 
L 1159 2969 
Q 1341 3281 1617 3432 
Q 1894 3584 2278 3584 
Q 2916 3584 3314 3078 
Q 3713 2572 3713 1747 
Q 3713 922 3314 415 
Q 2916 -91 2278 -91 
Q 1894 -91 1617 61 
Q 1341 213 1159 525 
z
M 3116 1747 
Q 3116 2381 2855 2742 
Q 2594 3103 2138 3103 
Q 1681 3103 1420 2742 
Q 1159 2381 1159 1747 
Q 1159 1113 1420 752 
Q 1681 391 2138 391 
Q 2594 391 2855 752 
Q 3116 1113 3116 1747 
z
" transform="scale(0.015625)"/>
       <path id="DejaVuSans-2e" d="M 684 794 
L 1344 794 
L 1344 0 
L 684 0 
L 684 794 
z
" transform="scale(0.015625)"/>
      </defs>
      <use xlink:href="#DejaVuSans-30"/>
      <use xlink:href="#DejaVuSans-30" x="63.623047"/>
      <use xlink:href="#DejaVuSans-32" x="127.246094"/>
      <use xlink:href="#DejaVuSans-62" x="190.869141"/>
      <use xlink:href="#DejaVuSans-6d" x="254.345703"/>
      <use xlink:href="#DejaVuSans-63" x="351.757812"/>
      <use xlink:href="#DejaVuSans-2d" x="406.738281"/>
      <use xlink:href="#DejaVuSans-61" x="442.822266"/>
      <use xlink:href="#DejaVuSans-70" x="504.101562"/>
      <use xlink:href="#DejaVuSans-61" x="567.578125"/>
      <use xlink:href="#DejaVuSans-6c" x="628.857422"/>
      <use xlink:href="#DejaVuSans-61" x="656.640625"/>
      <use xlink:href="#DejaVuSans-63" x="717.919922"/>
      <use xlink:href="#DejaVuSans-68" x="772.900391"/>
      <use xlink:href="#DejaVuSans-65" x="836.279297"/>
      <use xlink:href="#DejaVuSans-2d" x="897.802734"/>
      <use xlink:href="#DejaVuSans-30" x="933.886719"/>
      <use xlink:href="#DejaVuSans-2e" x="997.509766"/>
      <use xlink:href="#DejaVuSans-35" x="1029.296875"/>
      <use xlink:href="#DejaVuSans-2e" x="1092.919922"/>
      <use xlink:href="#DejaVuSans-32" x="1124.707031"/>
     </g>
    </g>
    <g id="line2d_38">
     <path d="M 252.523125 69.248563 
L 262.523125 69.248563 
L 272.523125 69.248563 
" style="fill: none; stroke: #0000ff; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
     <g>
      <use xlink:href="#mc912abb91b" x="262.523125" y="69.248563" style="fill: #0000ff; fill-opacity: 0.7; stroke: #0000ff; stroke-opacity: 0.7"/>
     </g>
    </g>
    <g id="text_19">
     <!-- 002bmc-apalache-0.7.0 -->
     <g transform="translate(280.523125 72.748563)scale(0.1 -0.1)">
      <defs>
       <path id="DejaVuSans-37" d="M 525 4666 
L 3525 4666 
L 3525 4397 
L 1831 0 
L 1172 0 
L 2766 4134 
L 525 4134 
L 525 4666 
z
" transform="scale(0.015625)"/>
      </defs>
      <use xlink:href="#DejaVuSans-30"/>
      <use xlink:href="#DejaVuSans-30" x="63.623047"/>
      <use xlink:href="#DejaVuSans-32" x="127.246094"/>
      <use xlink:href="#DejaVuSans-62" x="190.869141"/>
      <use xlink:href="#DejaVuSans-6d" x="254.345703"/>
      <use xlink:href="#DejaVuSans-63" x="351.757812"/>
      <use xlink:href="#DejaVuSans-2d" x="406.738281"/>
      <use xlink:href="#DejaVuSans-61" x="442.822266"/>
      <use xlink:href="#DejaVuSans-70" x="504.101562"/>
      <use xlink:href="#DejaVuSans-61" x="567.578125"/>
      <use xlink:href="#DejaVuSans-6c" x="628.857422"/>
      <use xlink:href="#DejaVuSans-61" x="656.640625"/>
      <use xlink:href="#DejaVuSans-63" x="717.919922"/>
      <use xlink:href="#DejaVuSans-68" x="772.900391"/>
      <use xlink:href="#DejaVuSans-65" x="836.279297"/>
      <use xlink:href="#DejaVuSans-2d" x="897.802734"/>
      <use xlink:href="#DejaVuSans-30" x="933.886719"/>
      <use xlink:href="#DejaVuSans-2e" x="997.509766"/>
      <use xlink:href="#DejaVuSans-37" x="1029.296875"/>
      <use xlink:href="#DejaVuSans-2e" x="1092.919922"/>
      <use xlink:href="#DejaVuSans-30" x="1124.707031"/>
     </g>
    </g>
    <g id="line2d_39">
     <path d="M 252.523125 83.926688 
L 262.523125 83.926688 
L 272.523125 83.926688 
" style="fill: none; stroke: #008000; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
     <g>
      <use xlink:href="#m174d52aab2" x="262.523125" y="83.926688" style="fill: #008000; fill-opacity: 0.7; stroke: #008000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     </g>
    </g>
    <g id="text_20">
     <!-- 002bmc-apalache-0.16.0 -->
     <g transform="translate(280.523125 87.426688)scale(0.1 -0.1)">
      <use xlink:href="#DejaVuSans-30"/>
      <use xlink:href="#DejaVuSans-30" x="63.623047"/>
      <use xlink:href="#DejaVuSans-32" x="127.246094"/>
      <use xlink:href="#DejaVuSans-62" x="190.869141"/>
      <use xlink:href="#DejaVuSans-6d" x="254.345703"/>
      <use xlink:href="#DejaVuSans-63" x="351.757812"/>
      <use xlink:href="#DejaVuSans-2d" x="406.738281"/>
      <use xlink:href="#DejaVuSans-61" x="442.822266"/>
      <use xlink:href="#DejaVuSans-70" x="504.101562"/>
      <use xlink:href="#DejaVuSans-61" x="567.578125"/>
      <use xlink:href="#DejaVuSans-6c" x="628.857422"/>
      <use xlink:href="#DejaVuSans-61" x="656.640625"/>
      <use xlink:href="#DejaVuSans-63" x="717.919922"/>
      <use xlink:href="#DejaVuSans-68" x="772.900391"/>
      <use xlink:href="#DejaVuSans-65" x="836.279297"/>
      <use xlink:href="#DejaVuSans-2d" x="897.802734"/>
      <use xlink:href="#DejaVuSans-30" x="933.886719"/>
      <use xlink:href="#DejaVuSans-2e" x="997.509766"/>
      <use xlink:href="#DejaVuSans-31" x="1029.296875"/>
      <use xlink:href="#DejaVuSans-36" x="1092.919922"/>
      <use xlink:href="#DejaVuSans-2e" x="1156.542969"/>
      <use xlink:href="#DejaVuSans-30" x="1188.330078"/>
     </g>
    </g>
    <g id="line2d_40">
     <path d="M 252.523125 98.604813 
L 262.523125 98.604813 
L 272.523125 98.604813 
" style="fill: none; stroke: #bf00bf; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
     <g>
      <use xlink:href="#m03e963d4b3" x="262.523125" y="98.604813" style="fill: #bf00bf; fill-opacity: 0.7; stroke: #bf00bf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     </g>
    </g>
    <g id="text_21">
     <!-- 002bmc-apalache-0.9.0 -->
     <g transform="translate(280.523125 102.104813)scale(0.1 -0.1)">
      <defs>
       <path id="DejaVuSans-39" d="M 703 97 
L 703 672 
Q 941 559 1184 500 
Q 1428 441 1663 441 
Q 2288 441 2617 861 
Q 2947 1281 2994 2138 
Q 2813 1869 2534 1725 
Q 2256 1581 1919 1581 
Q 1219 1581 811 2004 
Q 403 2428 403 3163 
Q 403 3881 828 4315 
Q 1253 4750 1959 4750 
Q 2769 4750 3195 4129 
Q 3622 3509 3622 2328 
Q 3622 1225 3098 567 
Q 2575 -91 1691 -91 
Q 1453 -91 1209 -44 
Q 966 3 703 97 
z
M 1959 2075 
Q 2384 2075 2632 2365 
Q 2881 2656 2881 3163 
Q 2881 3666 2632 3958 
Q 2384 4250 1959 4250 
Q 1534 4250 1286 3958 
Q 1038 3666 1038 3163 
Q 1038 2656 1286 2365 
Q 1534 2075 1959 2075 
z
" transform="scale(0.015625)"/>
      </defs>
      <use xlink:href="#DejaVuSans-30"/>
      <use xlink:href="#DejaVuSans-30" x="63.623047"/>
      <use xlink:href="#DejaVuSans-32" x="127.246094"/>
      <use xlink:href="#DejaVuSans-62" x="190.869141"/>
      <use xlink:href="#DejaVuSans-6d" x="254.345703"/>
      <use xlink:href="#DejaVuSans-63" x="351.757812"/>
      <use xlink:href="#DejaVuSans-2d" x="406.738281"/>
      <use xlink:href="#DejaVuSans-61" x="442.822266"/>
      <use xlink:href="#DejaVuSans-70" x="504.101562"/>
      <use xlink:href="#DejaVuSans-61" x="567.578125"/>
      <use xlink:href="#DejaVuSans-6c" x="628.857422"/>
      <use xlink:href="#DejaVuSans-61" x="656.640625"/>
      <use xlink:href="#DejaVuSans-63" x="717.919922"/>
      <use xlink:href="#DejaVuSans-68" x="772.900391"/>
      <use xlink:href="#DejaVuSans-65" x="836.279297"/>
      <use xlink:href="#DejaVuSans-2d" x="897.802734"/>
      <use xlink:href="#DejaVuSans-30" x="933.886719"/>
      <use xlink:href="#DejaVuSans-2e" x="997.509766"/>
      <use xlink:href="#DejaVuSans-39" x="1029.296875"/>
      <use xlink:href="#DejaVuSans-2e" x="1092.919922"/>
      <use xlink:href="#DejaVuSans-30" x="1124.707031"/>
     </g>
    </g>
    <g id="line2d_41">
     <path d="M 252.523125 113.282938 
L 262.523125 113.282938 
L 272.523125 113.282938 
" style="fill: none; stroke: #000000; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
     <g>
      <use xlink:href="#maea95cfc86" x="262.523125" y="113.282938" style="fill-opacity: 0.7; stroke: #000000; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     </g>
    </g>
    <g id="text_22">
     <!-- 002bmc-apalache-0.6.0 -->
     <g transform="translate(280.523125 116.782938)scale(0.1 -0.1)">
      <use xlink:href="#DejaVuSans-30"/>
      <use xlink:href="#DejaVuSans-30" x="63.623047"/>
      <use xlink:href="#DejaVuSans-32" x="127.246094"/>
      <use xlink:href="#DejaVuSans-62" x="190.869141"/>
      <use xlink:href="#DejaVuSans-6d" x="254.345703"/>
      <use xlink:href="#DejaVuSans-63" x="351.757812"/>
      <use xlink:href="#DejaVuSans-2d" x="406.738281"/>
      <use xlink:href="#DejaVuSans-61" x="442.822266"/>
      <use xlink:href="#DejaVuSans-70" x="504.101562"/>
      <use xlink:href="#DejaVuSans-61" x="567.578125"/>
      <use xlink:href="#DejaVuSans-6c" x="628.857422"/>
      <use xlink:href="#DejaVuSans-61" x="656.640625"/>
      <use xlink:href="#DejaVuSans-63" x="717.919922"/>
      <use xlink:href="#DejaVuSans-68" x="772.900391"/>
      <use xlink:href="#DejaVuSans-65" x="836.279297"/>
      <use xlink:href="#DejaVuSans-2d" x="897.802734"/>
      <use xlink:href="#DejaVuSans-30" x="933.886719"/>
      <use xlink:href="#DejaVuSans-2e" x="997.509766"/>
      <use xlink:href="#DejaVuSans-36" x="1029.296875"/>
      <use xlink:href="#DejaVuSans-2e" x="1092.919922"/>
      <use xlink:href="#DejaVuSans-30" x="1124.707031"/>
     </g>
    </g>
    <g id="line2d_42">
     <path d="M 252.523125 127.961063 
L 262.523125 127.961063 
L 272.523125 127.961063 
" style="fill: none; stroke: #00bfbf; stroke-opacity: 0.7; stroke-width: 1.5; stroke-linecap: square"/>
     <g>
      <use xlink:href="#m45fc077255" x="262.523125" y="127.961063" style="fill: #00bfbf; fill-opacity: 0.7; stroke: #00bfbf; stroke-opacity: 0.7; stroke-linejoin: miter"/>
     </g>
    </g>
    <g id="text_23">
     <!-- 002bmc-apalache-0.19.2 -->
     <g transform="translate(280.523125 131.461063)scale(0.1 -0.1)">
      <use xlink:href="#DejaVuSans-30"/>
      <use xlink:href="#DejaVuSans-30" x="63.623047"/>
      <use xlink:href="#DejaVuSans-32" x="127.246094"/>
      <use xlink:href="#DejaVuSans-62" x="190.869141"/>
      <use xlink:href="#DejaVuSans-6d" x="254.345703"/>
      <use xlink:href="#DejaVuSans-63" x="351.757812"/>
      <use xlink:href="#DejaVuSans-2d" x="406.738281"/>
      <use xlink:href="#DejaVuSans-61" x="442.822266"/>
      <use xlink:href="#DejaVuSans-70" x="504.101562"/>
      <use xlink:href="#DejaVuSans-61" x="567.578125"/>
      <use xlink:href="#DejaVuSans-6c" x="628.857422"/>
      <use xlink:href="#DejaVuSans-61" x="656.640625"/>
      <use xlink:href="#DejaVuSans-63" x="717.919922"/>
      <use xlink:href="#DejaVuSans-68" x="772.900391"/>
      <use xlink:href="#DejaVuSans-65" x="836.279297"/>
      <use xlink:href="#DejaVuSans-2d" x="897.802734"/>
      <use xlink:href="#DejaVuSans-30" x="933.886719"/>
      <use xlink:href="#DejaVuSans-2e" x="997.509766"/>
      <use xlink:href="#DejaVuSans-31" x="1029.296875"/>
      <use xlink:href="#DejaVuSans-39" x="1092.919922"/>
      <use xlink:href="#DejaVuSans-2e" x="1156.542969"/>
      <use xlink:href="#DejaVuSans-32" x="1188.330078"/>
     </g>
    </g>
   </g>
  </g>
 </g>
 <defs>
  <clipPath id="paae626c28e">
   <rect x="57.6" y="41.472" width="357.12" height="266.112"/>
  </clipPath>
 </defs>
</svg>