svg/plot/S5-bgraph_grayscale.svg

<svg xmlns="http://www.w3.org/2000/svg" width="1298" height="760" viewBox="150 127 1298 760">
<!-- Plot data obtained via command "pmGenerator -c -n -N -1 -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp <two hyphens>plot -s -x 150 -o data/s5-plot_data_x150.txt -d" ; repository at https://github.com/xamidi/pmGenerator -->
<style>
<![CDATA[text{filter:drop-shadow(0px -2px 6px #fff)}.B{font-family:Arial}.C{font-size:17px}.D{stroke-opacity:1}.G{text-anchor:middle}.H{text-anchor:end}.I{stroke-width:2}.J{stroke-dasharray:4 3}.K{font-style:italic}]]>
</style>
<defs>
<linearGradient id="A">
<stop offset="0%" stop-color="#e1e1e1"/><!-- relative luminance: 0.7529422168 (instead of #c0c0c0) -->
<stop offset="5%" stop-color="#e1e1e1"/>
<stop offset="28%" stop-color="#bcbcbc"/><!-- relative luminance: 0.502886458 (instead of #808080) -->
<stop offset="38%" stop-color="#bcbcbc"/>
<stop offset="61%" stop-color="#898989"/><!-- relative luminance: 0.2501582847 (instead of #404040) -->
<stop offset="71%" stop-color="#898989"/>
<stop offset="95%" stop-color="#000"/>
</linearGradient>
</defs>
<text x="296" y="161.45" font-weight="bold" class="B C">S5: Amount of minimal condensed detachment proofs w.r.t symbolic conclusion lengths</text>
<text x="1310" y="206.45" class="B C">proof length 21</text>
<circle cx="1287" cy="200.5" r="4.5" fill="#e1e1e1"/>
<text x="1310" y="234.45" class="B C">proof length 22</text>
<circle cx="1287" cy="228.5" r="4.5" fill="#bcbcbc"/>
<text x="1310" y="262.45" class="B C">proof length 23</text>
<circle cx="1287" cy="256.5" r="4.5" fill="#898989"/>
<text x="1310" y="290.45" class="B C">proof length 24</text>
<circle cx="1287" cy="284.5" r="4.5" fill="#000"/>
<text x="1310" y="318.45" class="B C">averages</text>
<path fill="none" stroke="url(#A)" d="M1270,312.5L1304,312.5001" class="D I"/>
<text x="1310" y="346.45" class="B C">medians</text>
<path fill="none" stroke="url(#A)" d="M1270,340.5L1304,340.5001" class="D I J"/>
<path fill="#ccc" d="M296 192h1v622h-1zm319 0h1v622h-1zm318 0h1v622h-1zm319 0h1v622h-1z"/>
<path fill="#ebebeb" d="M455 192h1v622h-1zm319 0h1v622h-1zm319 0h1v622h-1z"/>
<path fill="#ccc" d="M296 813h957v1H296zm0-124h957v1H296zm0-124h957v1H296zm0-125h957v1H296zm0-124h957v1H296zm0-124h957v1H296z"/>
<path fill="#ebebeb" d="M296 751h957v1H296zm0-124h957v1H296zm0-124h957v1H296zm0-125h957v1H296zm0-124h957v1H296z"/>
<g fill="#333">
<path d="M296 192h1v622h-1z"/>
<path d="M296 813h957v1H296z"/>
</g>
<g fill="none" class="I D">
<path stroke="#e1e1e1" d="M545.187 813.5v-621"/>
<path stroke="#bcbcbc" d="M555.831 813.5v-621"/>
<path stroke="#898989" d="M572.402 813.5v-621"/>
<path stroke="#000" d="M584.192 813.5v-621"/>
<g class="J">
<path stroke="#e1e1e1" d="M500.447 813.5v-621"/>
<path stroke="#bcbcbc" d="M506.82 813.5v-621"/>
<path stroke="#898989" d="M519.567 813.5v-621"/>
<path stroke="#000" d="M525.94 813.5v-621"/>
</g>
</g>
<g fill="#e1e1e1">
<circle cx="302.873" cy="813.5" r="4.5"/>
<circle cx="309.247" cy="813.5" r="4.5"/>
<circle cx="315.62" cy="813.5" r="4.5"/>
<circle cx="321.993" cy="813.5" r="4.5"/>
<circle cx="328.367" cy="813.5" r="4.5"/>
<circle cx="334.74" cy="813.499" r="4.5"/>
<circle cx="341.113" cy="813.497" r="4.5"/>
<circle cx="347.487" cy="813.497" r="4.5"/>
<circle cx="353.86" cy="813.493" r="4.5"/>
<circle cx="360.233" cy="813.467" r="4.5"/>
<circle cx="366.607" cy="813.462" r="4.5"/>
<circle cx="372.98" cy="813.421" r="4.5"/>
<circle cx="379.353" cy="813.299" r="4.5"/>
<circle cx="385.727" cy="812.981" r="4.5"/>
<circle cx="392.1" cy="812.346" r="4.5"/>
<circle cx="398.473" cy="812.231" r="4.5"/>
<circle cx="404.847" cy="811.836" r="4.5"/>
<circle cx="411.22" cy="808.61" r="4.5"/>
<circle cx="417.593" cy="802.641" r="4.5"/>
<circle cx="423.967" cy="802.295" r="4.5"/>
<circle cx="430.34" cy="804.272" r="4.5"/>
<circle cx="436.713" cy="800.502" r="4.5"/>
<circle cx="443.087" cy="777.057" r="4.5"/>
<circle cx="449.46" cy="752.852" r="4.5"/>
<circle cx="455.833" cy="763.935" r="4.5"/>
<circle cx="462.207" cy="794.324" r="4.5"/>
<circle cx="468.58" cy="784.009" r="4.5"/>
<circle cx="474.953" cy="756.059" r="4.5"/>
<circle cx="481.327" cy="732.068" r="4.5"/>
<circle cx="487.7" cy="754.092" r="4.5"/>
<circle cx="494.073" cy="775.908" r="4.5"/>
<circle cx="500.447" cy="764.355" r="4.5"/>
<circle cx="506.82" cy="755.275" r="4.5"/>
<circle cx="513.193" cy="788.382" r="4.5"/>
<circle cx="519.567" cy="790.322" r="4.5"/>
<circle cx="525.94" cy="790.56" r="4.5"/>
<circle cx="532.313" cy="783.455" r="4.5"/>
<circle cx="538.687" cy="796.057" r="4.5"/>
<circle cx="545.06" cy="797.271" r="4.5"/>
<circle cx="551.433" cy="802.61" r="4.5"/>
<circle cx="557.807" cy="799.308" r="4.5"/>
<circle cx="564.18" cy="805.07" r="4.5"/>
<circle cx="570.553" cy="802.418" r="4.5"/>
<circle cx="576.927" cy="803.322" r="4.5"/>
<circle cx="583.3" cy="799.786" r="4.5"/>
<circle cx="589.673" cy="804.744" r="4.5"/>
<circle cx="596.047" cy="801.981" r="4.5"/>
<circle cx="602.42" cy="805.872" r="4.5"/>
<circle cx="608.793" cy="801.79" r="4.5"/>
<circle cx="615.167" cy="805.243" r="4.5"/>
<circle cx="621.54" cy="803.011" r="4.5"/>
<circle cx="627.913" cy="807.325" r="4.5"/>
<circle cx="634.287" cy="804.693" r="4.5"/>
<circle cx="640.66" cy="807.289" r="4.5"/>
<circle cx="647.033" cy="804.209" r="4.5"/>
<circle cx="653.407" cy="807.322" r="4.5"/>
<circle cx="659.78" cy="804.476" r="4.5"/>
<circle cx="666.153" cy="807.653" r="4.5"/>
<circle cx="672.527" cy="804.353" r="4.5"/>
<circle cx="678.9" cy="809.201" r="4.5"/>
<circle cx="685.273" cy="807.174" r="4.5"/>
<circle cx="691.647" cy="809.4" r="4.5"/>
<circle cx="698.02" cy="806.934" r="4.5"/>
<circle cx="704.393" cy="809.7" r="4.5"/>
<circle cx="710.767" cy="807.288" r="4.5"/>
<circle cx="717.14" cy="810.073" r="4.5"/>
<circle cx="723.513" cy="808.278" r="4.5"/>
<circle cx="729.887" cy="810.335" r="4.5"/>
<circle cx="736.26" cy="809.038" r="4.5"/>
<circle cx="742.633" cy="810.976" r="4.5"/>
<circle cx="749.007" cy="809.104" r="4.5"/>
<circle cx="755.38" cy="811.281" r="4.5"/>
<circle cx="761.753" cy="810.121" r="4.5"/>
<circle cx="768.127" cy="811.187" r="4.5"/>
<circle cx="774.5" cy="810.134" r="4.5"/>
<circle cx="780.873" cy="811.774" r="4.5"/>
<circle cx="787.247" cy="810.624" r="4.5"/>
<circle cx="793.62" cy="811.923" r="4.5"/>
<circle cx="799.993" cy="811.202" r="4.5"/>
<circle cx="806.367" cy="811.913" r="4.5"/>
<circle cx="812.74" cy="811.343" r="4.5"/>
<circle cx="819.113" cy="812.192" r="4.5"/>
<circle cx="825.487" cy="810.896" r="4.5"/>
<circle cx="831.86" cy="812.543" r="4.5"/>
<circle cx="838.233" cy="812.08" r="4.5"/>
<circle cx="844.607" cy="812.309" r="4.5"/>
<circle cx="850.98" cy="812.085" r="4.5"/>
<circle cx="857.353" cy="812.693" r="4.5"/>
<circle cx="863.727" cy="811.925" r="4.5"/>
<circle cx="870.1" cy="812.703" r="4.5"/>
<circle cx="876.473" cy="812.291" r="4.5"/>
<circle cx="882.847" cy="812.516" r="4.5"/>
<circle cx="889.22" cy="812.426" r="4.5"/>
<circle cx="895.593" cy="812.829" r="4.5"/>
<circle cx="901.967" cy="812.057" r="4.5"/>
<circle cx="908.34" cy="812.993" r="4.5"/>
<circle cx="914.713" cy="812.65" r="4.5"/>
<circle cx="921.087" cy="812.79" r="4.5"/>
<circle cx="927.46" cy="812.508" r="4.5"/>
<circle cx="933.833" cy="812.98" r="4.5"/>
<circle cx="940.207" cy="812.546" r="4.5"/>
<circle cx="946.58" cy="812.968" r="4.5"/>
<circle cx="952.953" cy="812.74" r="4.5"/>
<circle cx="959.327" cy="812.949" r="4.5"/>
<circle cx="965.7" cy="812.873" r="4.5"/>
<circle cx="972.073" cy="813.173" r="4.5"/>
<circle cx="978.447" cy="812.591" r="4.5"/>
<circle cx="984.82" cy="813.155" r="4.5"/>
<circle cx="991.193" cy="813.047" r="4.5"/>
<circle cx="997.567" cy="813.09" r="4.5"/>
<circle cx="1003.94" cy="812.95" r="4.5"/>
<circle cx="1010.313" cy="813.181" r="4.5"/>
<circle cx="1016.687" cy="812.996" r="4.5"/>
<circle cx="1023.06" cy="813.202" r="4.5"/>
<circle cx="1029.433" cy="812.995" r="4.5"/>
<circle cx="1035.807" cy="813.208" r="4.5"/>
<circle cx="1042.18" cy="813.101" r="4.5"/>
<circle cx="1048.553" cy="813.189" r="4.5"/>
<circle cx="1054.927" cy="812.945" r="4.5"/>
<circle cx="1061.3" cy="813.301" r="4.5"/>
<circle cx="1067.673" cy="813.238" r="4.5"/>
<circle cx="1074.047" cy="813.138" r="4.5"/>
<circle cx="1080.42" cy="812.987" r="4.5"/>
<circle cx="1086.793" cy="813.314" r="4.5"/>
<circle cx="1093.167" cy="813.176" r="4.5"/>
<circle cx="1099.54" cy="813.317" r="4.5"/>
<circle cx="1105.913" cy="813.042" r="4.5"/>
<circle cx="1112.287" cy="813.316" r="4.5"/>
<circle cx="1118.66" cy="813.258" r="4.5"/>
<circle cx="1125.033" cy="813.371" r="4.5"/>
<circle cx="1131.407" cy="813.203" r="4.5"/>
<circle cx="1137.78" cy="813.32" r="4.5"/>
<circle cx="1144.153" cy="813.273" r="4.5"/>
<circle cx="1150.527" cy="813.326" r="4.5"/>
<circle cx="1156.9" cy="813.243" r="4.5"/>
<circle cx="1163.273" cy="813.414" r="4.5"/>
<circle cx="1169.647" cy="813.243" r="4.5"/>
<circle cx="1176.02" cy="813.355" r="4.5"/>
<circle cx="1182.393" cy="813.276" r="4.5"/>
<circle cx="1188.767" cy="813.357" r="4.5"/>
<circle cx="1195.14" cy="813.365" r="4.5"/>
<circle cx="1201.513" cy="813.327" r="4.5"/>
<circle cx="1207.887" cy="813.254" r="4.5"/>
<circle cx="1214.26" cy="813.409" r="4.5"/>
<circle cx="1220.633" cy="813.357" r="4.5"/>
<circle cx="1227.007" cy="813.417" r="4.5"/>
<circle cx="1233.38" cy="813.233" r="4.5"/>
<circle cx="1239.753" cy="813.44" r="4.5"/>
<circle cx="1246.127" cy="813.337" r="4.5"/>
<circle cx="1252.5" cy="813.436" r="4.5"/>
</g>
<g fill="#bcbcbc">
<circle cx="302.873" cy="813.5" r="4.5"/>
<circle cx="309.247" cy="813.5" r="4.5"/>
<circle cx="315.62" cy="813.5" r="4.5"/>
<circle cx="321.993" cy="813.5" r="4.5"/>
<circle cx="328.367" cy="813.5" r="4.5"/>
<circle cx="334.74" cy="813.5" r="4.5"/>
<circle cx="341.113" cy="813.498" r="4.5"/>
<circle cx="347.487" cy="813.495" r="4.5"/>
<circle cx="353.86" cy="813.496" r="4.5"/>
<circle cx="360.233" cy="813.482" r="4.5"/>
<circle cx="366.607" cy="813.43" r="4.5"/>
<circle cx="372.98" cy="813.414" r="4.5"/>
<circle cx="379.353" cy="813.357" r="4.5"/>
<circle cx="385.727" cy="813.094" r="4.5"/>
<circle cx="392.1" cy="812.372" r="4.5"/>
<circle cx="398.473" cy="811.191" r="4.5"/>
<circle cx="404.847" cy="810.958" r="4.5"/>
<circle cx="411.22" cy="810.113" r="4.5"/>
<circle cx="417.593" cy="803.566" r="4.5"/>
<circle cx="423.967" cy="792.554" r="4.5"/>
<circle cx="430.34" cy="791.846" r="4.5"/>
<circle cx="436.713" cy="795.796" r="4.5"/>
<circle cx="443.087" cy="787.129" r="4.5"/>
<circle cx="449.46" cy="743.573" r="4.5"/>
<circle cx="455.833" cy="701.119" r="4.5"/>
<circle cx="462.207" cy="723.351" r="4.5"/>
<circle cx="468.58" cy="775.231" r="4.5"/>
<circle cx="474.953" cy="754.989" r="4.5"/>
<circle cx="481.327" cy="701.62" r="4.5"/>
<circle cx="487.7" cy="662.777" r="4.5"/>
<circle cx="494.073" cy="703.733" r="4.5"/>
<circle cx="500.447" cy="741.181" r="4.5"/>
<circle cx="506.82" cy="718.197" r="4.5"/>
<circle cx="513.193" cy="705.699" r="4.5"/>
<circle cx="519.567" cy="762.253" r="4.5"/>
<circle cx="525.94" cy="768.918" r="4.5"/>
<circle cx="532.313" cy="766.54" r="4.5"/>
<circle cx="538.687" cy="756.011" r="4.5"/>
<circle cx="545.06" cy="777.411" r="4.5"/>
<circle cx="551.433" cy="783.742" r="4.5"/>
<circle cx="557.807" cy="788.647" r="4.5"/>
<circle cx="564.18" cy="787.209" r="4.5"/>
<circle cx="570.553" cy="793.955" r="4.5"/>
<circle cx="576.927" cy="793.558" r="4.5"/>
<circle cx="583.3" cy="791.298" r="4.5"/>
<circle cx="589.673" cy="789.618" r="4.5"/>
<circle cx="596.047" cy="794.042" r="4.5"/>
<circle cx="602.42" cy="794.494" r="4.5"/>
<circle cx="608.793" cy="794.377" r="4.5"/>
<circle cx="615.167" cy="794.334" r="4.5"/>
<circle cx="621.54" cy="792.701" r="4.5"/>
<circle cx="627.913" cy="796.457" r="4.5"/>
<circle cx="634.287" cy="797.319" r="4.5"/>
<circle cx="640.66" cy="799.232" r="4.5"/>
<circle cx="647.033" cy="798.375" r="4.5"/>
<circle cx="653.407" cy="798.589" r="4.5"/>
<circle cx="659.78" cy="797.828" r="4.5"/>
<circle cx="666.153" cy="799.905" r="4.5"/>
<circle cx="672.527" cy="796.481" r="4.5"/>
<circle cx="678.9" cy="799.913" r="4.5"/>
<circle cx="685.273" cy="799.615" r="4.5"/>
<circle cx="691.647" cy="803.792" r="4.5"/>
<circle cx="698.02" cy="801.92" r="4.5"/>
<circle cx="704.393" cy="803.19" r="4.5"/>
<circle cx="710.767" cy="802.793" r="4.5"/>
<circle cx="717.14" cy="804.257" r="4.5"/>
<circle cx="723.513" cy="802.952" r="4.5"/>
<circle cx="729.887" cy="804.949" r="4.5"/>
<circle cx="736.26" cy="804.217" r="4.5"/>
<circle cx="742.633" cy="806.45" r="4.5"/>
<circle cx="749.007" cy="805.289" r="4.5"/>
<circle cx="755.38" cy="806.693" r="4.5"/>
<circle cx="761.753" cy="807.173" r="4.5"/>
<circle cx="768.127" cy="807.621" r="4.5"/>
<circle cx="774.5" cy="807.188" r="4.5"/>
<circle cx="780.873" cy="808.245" r="4.5"/>
<circle cx="787.247" cy="807.502" r="4.5"/>
<circle cx="793.62" cy="809.054" r="4.5"/>
<circle cx="799.993" cy="808.809" r="4.5"/>
<circle cx="806.367" cy="809.186" r="4.5"/>
<circle cx="812.74" cy="809.815" r="4.5"/>
<circle cx="819.113" cy="809.83" r="4.5"/>
<circle cx="825.487" cy="808.95" r="4.5"/>
<circle cx="831.86" cy="809.687" r="4.5"/>
<circle cx="838.233" cy="810.648" r="4.5"/>
<circle cx="844.607" cy="809.924" r="4.5"/>
<circle cx="850.98" cy="810.802" r="4.5"/>
<circle cx="857.353" cy="811.137" r="4.5"/>
<circle cx="863.727" cy="810.661" r="4.5"/>
<circle cx="870.1" cy="811.094" r="4.5"/>
<circle cx="876.473" cy="811.279" r="4.5"/>
<circle cx="882.847" cy="811.046" r="4.5"/>
<circle cx="889.22" cy="811.371" r="4.5"/>
<circle cx="895.593" cy="811.651" r="4.5"/>
<circle cx="901.967" cy="811.064" r="4.5"/>
<circle cx="908.34" cy="811.382" r="4.5"/>
<circle cx="914.713" cy="812.151" r="4.5"/>
<circle cx="921.087" cy="811.483" r="4.5"/>
<circle cx="927.46" cy="811.895" r="4.5"/>
<circle cx="933.833" cy="811.908" r="4.5"/>
<circle cx="940.207" cy="811.722" r="4.5"/>
<circle cx="946.58" cy="811.969" r="4.5"/>
<circle cx="952.953" cy="812.167" r="4.5"/>
<circle cx="959.327" cy="811.902" r="4.5"/>
<circle cx="965.7" cy="812.293" r="4.5"/>
<circle cx="972.073" cy="812.41" r="4.5"/>
<circle cx="978.447" cy="812.077" r="4.5"/>
<circle cx="984.82" cy="812.221" r="4.5"/>
<circle cx="991.193" cy="812.604" r="4.5"/>
<circle cx="997.567" cy="812.372" r="4.5"/>
<circle cx="1003.94" cy="812.596" r="4.5"/>
<circle cx="1010.313" cy="812.455" r="4.5"/>
<circle cx="1016.687" cy="812.399" r="4.5"/>
<circle cx="1023.06" cy="812.724" r="4.5"/>
<circle cx="1029.433" cy="812.773" r="4.5"/>
<circle cx="1035.807" cy="812.539" r="4.5"/>
<circle cx="1042.18" cy="812.732" r="4.5"/>
<circle cx="1048.553" cy="812.832" r="4.5"/>
<circle cx="1054.927" cy="812.537" r="4.5"/>
<circle cx="1061.3" cy="812.682" r="4.5"/>
<circle cx="1067.673" cy="812.942" r="4.5"/>
<circle cx="1074.047" cy="812.821" r="4.5"/>
<circle cx="1080.42" cy="812.765" r="4.5"/>
<circle cx="1086.793" cy="812.623" r="4.5"/>
<circle cx="1093.167" cy="812.952" r="4.5"/>
<circle cx="1099.54" cy="813.015" r="4.5"/>
<circle cx="1105.913" cy="812.819" r="4.5"/>
<circle cx="1112.287" cy="812.786" r="4.5"/>
<circle cx="1118.66" cy="813.042" r="4.5"/>
<circle cx="1125.033" cy="813.119" r="4.5"/>
<circle cx="1131.407" cy="812.992" r="4.5"/>
<circle cx="1137.78" cy="812.775" r="4.5"/>
<circle cx="1144.153" cy="813.109" r="4.5"/>
<circle cx="1150.527" cy="813.046" r="4.5"/>
<circle cx="1156.9" cy="813.091" r="4.5"/>
<circle cx="1163.273" cy="813.094" r="4.5"/>
<circle cx="1169.647" cy="812.981" r="4.5"/>
<circle cx="1176.02" cy="813.124" r="4.5"/>
<circle cx="1182.393" cy="813.131" r="4.5"/>
<circle cx="1188.767" cy="813.094" r="4.5"/>
<circle cx="1195.14" cy="813.158" r="4.5"/>
<circle cx="1201.513" cy="813.195" r="4.5"/>
<circle cx="1207.887" cy="813.092" r="4.5"/>
<circle cx="1214.26" cy="813.132" r="4.5"/>
<circle cx="1220.633" cy="813.28" r="4.5"/>
<circle cx="1227.007" cy="813.209" r="4.5"/>
<circle cx="1233.38" cy="813.092" r="4.5"/>
<circle cx="1239.753" cy="813.144" r="4.5"/>
<circle cx="1246.127" cy="813.234" r="4.5"/>
<circle cx="1252.5" cy="813.266" r="4.5"/>
</g>
<g fill="#898989">
<circle cx="302.873" cy="813.5" r="4.5"/>
<circle cx="309.247" cy="813.5" r="4.5"/>
<circle cx="315.62" cy="813.5" r="4.5"/>
<circle cx="321.993" cy="813.5" r="4.5"/>
<circle cx="328.367" cy="813.5" r="4.5"/>
<circle cx="334.74" cy="813.499" r="4.5"/>
<circle cx="341.113" cy="813.499" r="4.5"/>
<circle cx="347.487" cy="813.496" r="4.5"/>
<circle cx="353.86" cy="813.487" r="4.5"/>
<circle cx="360.233" cy="813.483" r="4.5"/>
<circle cx="366.607" cy="813.448" r="4.5"/>
<circle cx="372.98" cy="813.321" r="4.5"/>
<circle cx="379.353" cy="813.245" r="4.5"/>
<circle cx="385.727" cy="813.076" r="4.5"/>
<circle cx="392.1" cy="812.459" r="4.5"/>
<circle cx="398.473" cy="810.934" r="4.5"/>
<circle cx="404.847" cy="808.564" r="4.5"/>
<circle cx="411.22" cy="808.09" r="4.5"/>
<circle cx="417.593" cy="805.806" r="4.5"/>
<circle cx="423.967" cy="793.005" r="4.5"/>
<circle cx="430.34" cy="772.266" r="4.5"/>
<circle cx="436.713" cy="770.952" r="4.5"/>
<circle cx="443.087" cy="777.552" r="4.5"/>
<circle cx="449.46" cy="759.467" r="4.5"/>
<circle cx="455.833" cy="677.696" r="4.5"/>
<circle cx="462.207" cy="604.717" r="4.5"/>
<circle cx="468.58" cy="646.513" r="4.5"/>
<circle cx="474.953" cy="736.627" r="4.5"/>
<circle cx="481.327" cy="695.183" r="4.5"/>
<circle cx="487.7" cy="596.085" r="4.5"/>
<circle cx="494.073" cy="530.39" r="4.5"/>
<circle cx="500.447" cy="609.602" r="4.5"/>
<circle cx="506.82" cy="670.148" r="4.5"/>
<circle cx="513.193" cy="628.964" r="4.5"/>
<circle cx="519.567" cy="608.046" r="4.5"/>
<circle cx="525.94" cy="709.59" r="4.5"/>
<circle cx="532.313" cy="722.399" r="4.5"/>
<circle cx="538.687" cy="719.184" r="4.5"/>
<circle cx="545.06" cy="697.535" r="4.5"/>
<circle cx="551.433" cy="742.079" r="4.5"/>
<circle cx="557.807" cy="751.53" r="4.5"/>
<circle cx="564.18" cy="764.047" r="4.5"/>
<circle cx="570.553" cy="755.383" r="4.5"/>
<circle cx="576.927" cy="775.731" r="4.5"/>
<circle cx="583.3" cy="767.758" r="4.5"/>
<circle cx="589.673" cy="772.186" r="4.5"/>
<circle cx="596.047" cy="762.218" r="4.5"/>
<circle cx="602.42" cy="778.179" r="4.5"/>
<circle cx="608.793" cy="770.992" r="4.5"/>
<circle cx="615.167" cy="780.872" r="4.5"/>
<circle cx="621.54" cy="767.124" r="4.5"/>
<circle cx="627.913" cy="778.241" r="4.5"/>
<circle cx="634.287" cy="770.388" r="4.5"/>
<circle cx="640.66" cy="786.252" r="4.5"/>
<circle cx="647.033" cy="776.97" r="4.5"/>
<circle cx="653.407" cy="787.457" r="4.5"/>
<circle cx="659.78" cy="777.879" r="4.5"/>
<circle cx="666.153" cy="788.058" r="4.5"/>
<circle cx="672.527" cy="777.888" r="4.5"/>
<circle cx="678.9" cy="786.941" r="4.5"/>
<circle cx="685.273" cy="775.881" r="4.5"/>
<circle cx="691.647" cy="791.911" r="4.5"/>
<circle cx="698.02" cy="783.088" r="4.5"/>
<circle cx="704.393" cy="794.92" r="4.5"/>
<circle cx="710.767" cy="785.377" r="4.5"/>
<circle cx="717.14" cy="796.407" r="4.5"/>
<circle cx="723.513" cy="788.14" r="4.5"/>
<circle cx="729.887" cy="796.645" r="4.5"/>
<circle cx="736.26" cy="788.943" r="4.5"/>
<circle cx="742.633" cy="798.721" r="4.5"/>
<circle cx="749.007" cy="790.598" r="4.5"/>
<circle cx="755.38" cy="800.344" r="4.5"/>
<circle cx="761.753" cy="794.569" r="4.5"/>
<circle cx="768.127" cy="801.339" r="4.5"/>
<circle cx="774.5" cy="797.519" r="4.5"/>
<circle cx="780.873" cy="803.183" r="4.5"/>
<circle cx="787.247" cy="797.207" r="4.5"/>
<circle cx="793.62" cy="804.112" r="4.5"/>
<circle cx="799.993" cy="799.283" r="4.5"/>
<circle cx="806.367" cy="804.866" r="4.5"/>
<circle cx="812.74" cy="801.628" r="4.5"/>
<circle cx="819.113" cy="806.855" r="4.5"/>
<circle cx="825.487" cy="802.533" r="4.5"/>
<circle cx="831.86" cy="806.149" r="4.5"/>
<circle cx="838.233" cy="803.164" r="4.5"/>
<circle cx="844.607" cy="806.616" r="4.5"/>
<circle cx="850.98" cy="804.568" r="4.5"/>
<circle cx="857.353" cy="808.604" r="4.5"/>
<circle cx="863.727" cy="804.369" r="4.5"/>
<circle cx="870.1" cy="808.902" r="4.5"/>
<circle cx="876.473" cy="806.806" r="4.5"/>
<circle cx="882.847" cy="808.097" r="4.5"/>
<circle cx="889.22" cy="807.14" r="4.5"/>
<circle cx="895.593" cy="809.588" r="4.5"/>
<circle cx="901.967" cy="807.095" r="4.5"/>
<circle cx="908.34" cy="809.493" r="4.5"/>
<circle cx="914.713" cy="807.923" r="4.5"/>
<circle cx="921.087" cy="809.394" r="4.5"/>
<circle cx="927.46" cy="808.718" r="4.5"/>
<circle cx="933.833" cy="810.62" r="4.5"/>
<circle cx="940.207" cy="807.834" r="4.5"/>
<circle cx="946.58" cy="810.566" r="4.5"/>
<circle cx="952.953" cy="809.346" r="4.5"/>
<circle cx="959.327" cy="810.171" r="4.5"/>
<circle cx="965.7" cy="809.541" r="4.5"/>
<circle cx="972.073" cy="811.266" r="4.5"/>
<circle cx="978.447" cy="809.413" r="4.5"/>
<circle cx="984.82" cy="811.215" r="4.5"/>
<circle cx="991.193" cy="810.122" r="4.5"/>
<circle cx="997.567" cy="811.131" r="4.5"/>
<circle cx="1003.94" cy="810.766" r="4.5"/>
<circle cx="1010.313" cy="811.396" r="4.5"/>
<circle cx="1016.687" cy="809.835" r="4.5"/>
<circle cx="1023.06" cy="811.668" r="4.5"/>
<circle cx="1029.433" cy="811.29" r="4.5"/>
<circle cx="1035.807" cy="811.475" r="4.5"/>
<circle cx="1042.18" cy="810.778" r="4.5"/>
<circle cx="1048.553" cy="812.108" r="4.5"/>
<circle cx="1054.927" cy="811.1" r="4.5"/>
<circle cx="1061.3" cy="811.925" r="4.5"/>
<circle cx="1067.673" cy="811.187" r="4.5"/>
<circle cx="1074.047" cy="811.993" r="4.5"/>
<circle cx="1080.42" cy="811.659" r="4.5"/>
<circle cx="1086.793" cy="812.045" r="4.5"/>
<circle cx="1093.167" cy="810.932" r="4.5"/>
<circle cx="1099.54" cy="812.466" r="4.5"/>
<circle cx="1105.913" cy="811.916" r="4.5"/>
<circle cx="1112.287" cy="812.139" r="4.5"/>
<circle cx="1118.66" cy="811.662" r="4.5"/>
<circle cx="1125.033" cy="812.643" r="4.5"/>
<circle cx="1131.407" cy="812.052" r="4.5"/>
<circle cx="1137.78" cy="812.211" r="4.5"/>
<circle cx="1144.153" cy="811.926" r="4.5"/>
<circle cx="1150.527" cy="812.501" r="4.5"/>
<circle cx="1156.9" cy="812.294" r="4.5"/>
<circle cx="1163.273" cy="812.713" r="4.5"/>
<circle cx="1169.647" cy="811.431" r="4.5"/>
<circle cx="1176.02" cy="812.69" r="4.5"/>
<circle cx="1182.393" cy="812.359" r="4.5"/>
<circle cx="1188.767" cy="812.69" r="4.5"/>
<circle cx="1195.14" cy="812.348" r="4.5"/>
<circle cx="1201.513" cy="812.558" r="4.5"/>
<circle cx="1207.887" cy="812.298" r="4.5"/>
<circle cx="1214.26" cy="812.765" r="4.5"/>
<circle cx="1220.633" cy="812.51" r="4.5"/>
<circle cx="1227.007" cy="812.964" r="4.5"/>
<circle cx="1233.38" cy="812.424" r="4.5"/>
<circle cx="1239.753" cy="812.867" r="4.5"/>
<circle cx="1246.127" cy="812.305" r="4.5"/>
<circle cx="1252.5" cy="813.077" r="4.5"/>
</g>
<g fill="#000">
<circle cx="302.873" cy="813.5" r="4.5"/>
<circle cx="309.247" cy="813.5" r="4.5"/>
<circle cx="315.62" cy="813.5" r="4.5"/>
<circle cx="321.993" cy="813.5" r="4.5"/>
<circle cx="328.367" cy="813.5" r="4.5"/>
<circle cx="334.74" cy="813.5" r="4.5"/>
<circle cx="341.113" cy="813.499" r="4.5"/>
<circle cx="347.487" cy="813.499" r="4.5"/>
<circle cx="353.86" cy="813.489" r="4.5"/>
<circle cx="360.233" cy="813.477" r="4.5"/>
<circle cx="366.607" cy="813.471" r="4.5"/>
<circle cx="372.98" cy="813.394" r="4.5"/>
<circle cx="379.353" cy="813.151" r="4.5"/>
<circle cx="385.727" cy="813.008" r="4.5"/>
<circle cx="392.1" cy="812.711" r="4.5"/>
<circle cx="398.473" cy="811.432" r="4.5"/>
<circle cx="404.847" cy="808.165" r="4.5"/>
<circle cx="411.22" cy="803.678" r="4.5"/>
<circle cx="417.593" cy="802.868" r="4.5"/>
<circle cx="423.967" cy="797.995" r="4.5"/>
<circle cx="430.34" cy="772.286" r="4.5"/>
<circle cx="436.713" cy="733.945" r="4.5"/>
<circle cx="443.087" cy="730.956" r="4.5"/>
<circle cx="449.46" cy="743.708" r="4.5"/>
<circle cx="455.833" cy="704.737" r="4.5"/>
<circle cx="462.207" cy="552.684" r="4.5"/>
<circle cx="468.58" cy="425.491" r="4.5"/>
<circle cx="474.953" cy="506.937" r="4.5"/>
<circle cx="481.327" cy="660.736" r="4.5"/>
<circle cx="487.7" cy="579.243" r="4.5"/>
<circle cx="494.073" cy="391.569" r="4.5"/>
<circle cx="500.447" cy="286.75" r="4.5"/>
<circle cx="506.82" cy="433.281" r="4.5"/>
<circle cx="513.193" cy="535.973" r="4.5"/>
<circle cx="519.567" cy="454.781" r="4.5"/>
<circle cx="525.94" cy="427.45" r="4.5"/>
<circle cx="532.313" cy="602.275" r="4.5"/>
<circle cx="538.687" cy="634.959" r="4.5"/>
<circle cx="545.06" cy="620.611" r="4.5"/>
<circle cx="551.433" cy="588.223" r="4.5"/>
<circle cx="557.807" cy="667.587" r="4.5"/>
<circle cx="564.18" cy="695.965" r="4.5"/>
<circle cx="570.553" cy="706.145" r="4.5"/>
<circle cx="576.927" cy="703.442" r="4.5"/>
<circle cx="583.3" cy="728.514" r="4.5"/>
<circle cx="589.673" cy="729.202" r="4.5"/>
<circle cx="596.047" cy="722.913" r="4.5"/>
<circle cx="602.42" cy="721.74" r="4.5"/>
<circle cx="608.793" cy="736.141" r="4.5"/>
<circle cx="615.167" cy="740.305" r="4.5"/>
<circle cx="621.54" cy="739.921" r="4.5"/>
<circle cx="627.913" cy="734.993" r="4.5"/>
<circle cx="634.287" cy="730.138" r="4.5"/>
<circle cx="640.66" cy="742.985" r="4.5"/>
<circle cx="647.033" cy="742.146" r="4.5"/>
<circle cx="653.407" cy="753.56" r="4.5"/>
<circle cx="659.78" cy="747.954" r="4.5"/>
<circle cx="666.153" cy="754.578" r="4.5"/>
<circle cx="672.527" cy="751.589" r="4.5"/>
<circle cx="678.9" cy="756.834" r="4.5"/>
<circle cx="685.273" cy="746.292" r="4.5"/>
<circle cx="691.647" cy="754.363" r="4.5"/>
<circle cx="698.02" cy="751.007" r="4.5"/>
<circle cx="704.393" cy="767.839" r="4.5"/>
<circle cx="710.767" cy="755.498" r="4.5"/>
<circle cx="717.14" cy="769.417" r="4.5"/>
<circle cx="723.513" cy="765.684" r="4.5"/>
<circle cx="729.887" cy="773.462" r="4.5"/>
<circle cx="736.26" cy="767.65" r="4.5"/>
<circle cx="742.633" cy="775.316" r="4.5"/>
<circle cx="749.007" cy="768.615" r="4.5"/>
<circle cx="755.38" cy="778.851" r="4.5"/>
<circle cx="761.753" cy="773.115" r="4.5"/>
<circle cx="768.127" cy="780.947" r="4.5"/>
<circle cx="774.5" cy="780.299" r="4.5"/>
<circle cx="780.873" cy="788.026" r="4.5"/>
<circle cx="787.247" cy="781.178" r="4.5"/>
<circle cx="793.62" cy="788.33" r="4.5"/>
<circle cx="799.993" cy="785.959" r="4.5"/>
<circle cx="806.367" cy="789.475" r="4.5"/>
<circle cx="812.74" cy="787.353" r="4.5"/>
<circle cx="819.113" cy="794.196" r="4.5"/>
<circle cx="825.487" cy="792.264" r="4.5"/>
<circle cx="831.86" cy="795.83" r="4.5"/>
<circle cx="838.233" cy="794.447" r="4.5"/>
<circle cx="844.607" cy="794.428" r="4.5"/>
<circle cx="850.98" cy="796.33" r="4.5"/>
<circle cx="857.353" cy="798.814" r="4.5"/>
<circle cx="863.727" cy="795.355" r="4.5"/>
<circle cx="870.1" cy="799.865" r="4.5"/>
<circle cx="876.473" cy="800.925" r="4.5"/>
<circle cx="882.847" cy="797.958" r="4.5"/>
<circle cx="889.22" cy="800.882" r="4.5"/>
<circle cx="895.593" cy="802.925" r="4.5"/>
<circle cx="901.967" cy="800.357" r="4.5"/>
<circle cx="908.34" cy="803.533" r="4.5"/>
<circle cx="914.713" cy="802.714" r="4.5"/>
<circle cx="921.087" cy="802.11" r="4.5"/>
<circle cx="927.46" cy="804.518" r="4.5"/>
<circle cx="933.833" cy="805.484" r="4.5"/>
<circle cx="940.207" cy="802.888" r="4.5"/>
<circle cx="946.58" cy="804.742" r="4.5"/>
<circle cx="952.953" cy="806.006" r="4.5"/>
<circle cx="959.327" cy="803.783" r="4.5"/>
<circle cx="965.7" cy="805.946" r="4.5"/>
<circle cx="972.073" cy="806.984" r="4.5"/>
<circle cx="978.447" cy="805.523" r="4.5"/>
<circle cx="984.82" cy="807.247" r="4.5"/>
<circle cx="991.193" cy="807.347" r="4.5"/>
<circle cx="997.567" cy="806.474" r="4.5"/>
<circle cx="1003.94" cy="808.253" r="4.5"/>
<circle cx="1010.313" cy="808.411" r="4.5"/>
<circle cx="1016.687" cy="806.823" r="4.5"/>
<circle cx="1023.06" cy="807.897" r="4.5"/>
<circle cx="1029.433" cy="808.913" r="4.5"/>
<circle cx="1035.807" cy="807.984" r="4.5"/>
<circle cx="1042.18" cy="808.247" r="4.5"/>
<circle cx="1048.553" cy="809.079" r="4.5"/>
<circle cx="1054.927" cy="808.484" r="4.5"/>
<circle cx="1061.3" cy="809.842" r="4.5"/>
<circle cx="1067.673" cy="809.387" r="4.5"/>
<circle cx="1074.047" cy="808.547" r="4.5"/>
<circle cx="1080.42" cy="809.944" r="4.5"/>
<circle cx="1086.793" cy="810.35" r="4.5"/>
<circle cx="1093.167" cy="809.034" r="4.5"/>
<circle cx="1099.54" cy="809.357" r="4.5"/>
<circle cx="1105.913" cy="810.615" r="4.5"/>
<circle cx="1112.287" cy="810.06" r="4.5"/>
<circle cx="1118.66" cy="810.23" r="4.5"/>
<circle cx="1125.033" cy="810.458" r="4.5"/>
<circle cx="1131.407" cy="810.628" r="4.5"/>
<circle cx="1137.78" cy="810.924" r="4.5"/>
<circle cx="1144.153" cy="810.556" r="4.5"/>
<circle cx="1150.527" cy="810.317" r="4.5"/>
<circle cx="1156.9" cy="811.255" r="4.5"/>
<circle cx="1163.273" cy="811.515" r="4.5"/>
<circle cx="1169.647" cy="810.047" r="4.5"/>
<circle cx="1176.02" cy="810.591" r="4.5"/>
<circle cx="1182.393" cy="811.364" r="4.5"/>
<circle cx="1188.767" cy="811.327" r="4.5"/>
<circle cx="1195.14" cy="811.393" r="4.5"/>
<circle cx="1201.513" cy="810.527" r="4.5"/>
<circle cx="1207.887" cy="811.081" r="4.5"/>
<circle cx="1214.26" cy="811.661" r="4.5"/>
<circle cx="1220.633" cy="811.679" r="4.5"/>
<circle cx="1227.007" cy="811.627" r="4.5"/>
<circle cx="1233.38" cy="811.4" r="4.5"/>
<circle cx="1239.753" cy="811.846" r="4.5"/>
<circle cx="1246.127" cy="811.318" r="4.5"/>
<circle cx="1252.5" cy="811.71" r="4.5"/>
</g>
<text x="296.5" y="839.45" class="B C G">0</text>
<text x="615.167" y="839.45" class="B C G">50</text>
<text x="933.833" y="839.45" class="B C G">100</text>
<text x="1252.5" y="839.45" class="B C G">150</text>
<text x="279" y="819.45" class="B C H">0</text>
<text x="279" y="695.25" class="B C H">200,000</text>
<text x="279" y="571.05" class="B C H">400,000</text>
<text x="279" y="446.85" class="B C H">600,000</text>
<text x="279" y="322.65" class="B C H">800,000</text>
<text x="279" y="198.45" class="B C H">1,000,000</text>
<text x="774.5" y="880.279" class="B C G K">symbolic length of conclusion</text>
<text x="-503" y="181.45" transform="rotate(270)" class="B C G K">amount of minimal proofs for conclusions of specific length</text>
</svg>