Performance Comparison Details

[pqnelson]

Hello,

This isn't an "issue", per se, but I was wondering if there were any files where the "vanilla verifier" from Mizar outperforms mizar-rs? Or is the rust version better across the board?

Best, Alex

P.S. Will you continue and implement the parser, or is that "an exercise for the reader"?

[digama0]

That's a fair question, I haven't tried to measure that. Based on my experiences, the short articles are difficult to measure but rust will likely win out just because there is less file/process overhead (the rust verifier can chew through the first 20 articles in the time it takes for the vanilla verifier to do its usual progress reporting stuff for one), and there seem to be some patterns that take a lot longer in vanilla. When 5x is the baseline it seems difficult to imagine that there is an example where that goes to 1x.

Re: parser, I'm kind of hoping that this verifier gets some traction as an open source project within the Mizar community so that it's not just me doing the work. It's also the least important component re: proof export compared to accom + analyzer + checker, so it will likely be left for last if I'm the one doing it.

[digama0]

Okay, I had some time to sit down and do some per-file measurements for mizar-rs vs verifier.

                           

• The top graph is a log-log plot, the bottom is linear. Note that some outliers are off the top of the second chart and are only visible in the first.
• The blue line is the best linear fit, $y = 6.5697x$, while the orange line is $y=x$. So this is predicting an average speedup of $6.57\pm2.72$.
• The outliers are:
  • Worst for verifier:
  • LEIBNIZ1: 5.746s for mizar-rs, 637.738s for verifier, 110.9x speedup
  • Worst for mizar-rs:
  • AOFA_L00: 123.706s for mizar-rs, 451.123s for verifier, 3.65x speedup
  • Maximized verifier / mizar-rs:
  • SUBSET: 0.002s for mizar-rs, 1.499s for verifier, 749.5x speedup
  • TARSKI: 0.005s for mizar-rs, 0.574s for verifier, 114.8x speedup
  • LEIBNIZ1: 5.746s for mizar-rs, 637.738s for verifier, 110.9x speedup
  • Minimized verifier / mizar-rs:
  • BCIIDEAL: 1.951s for mizar-rs, 1.212s for verifier, 0.621x (slowdown)
  • LATSUM_1: 1.409s for mizar-rs, 1.103s for verifier 0.782x (slowdown)
  • TOPGEN_1: 1.340s for mizar-rs, 1.558s for verifier 1.162x speedup

BCIIDEAL and LATSUM_1 are the only two data points below the $y=x$ line, which you can see on the graph.

Ignoring SUBSET and TARSKI which have absurd speedup numbers because mizar-rs has lower fixed costs than verifier, LEIBNIZ1 stands out as hitting a particularly bad case in verifier resulting in a 10 minute runtime just for that one file. I have not investigated this in detail.

Data set

Obtain by running `cargo run --release` vs `env ORIG_MIZAR=1 cargo run --release` (in ORIG_MIZAR mode, the tool will just shell out to `verifier` but still parallelize and report per-file times in the same way). Tested on 12ef4516. ``` 0: tarski mizar-rs: 0.005 s, verifier: 0.574 s 1: xboole_0 mizar-rs: 0.013 s, verifier: 1.140 s 2: boole mizar-rs: 0.008 s, verifier: 0.746 s 3: xboole_1 mizar-rs: 0.076 s, verifier: 4.441 s 4: enumset1 mizar-rs: 0.146 s, verifier: 4.694 s 5: xtuple_0 mizar-rs: 0.046 s, verifier: 2.511 s 6: xfamily mizar-rs: 0.002 s, verifier: 0.023 s 7: xregular mizar-rs: 0.034 s, verifier: 1.457 s 8: zfmisc_1 mizar-rs: 0.201 s, verifier: 6.181 s 9: subset_1 mizar-rs: 0.084 s, verifier: 4.048 s 10: subset mizar-rs: 0.002 s, verifier: 1.499 s 11: setfam_1 mizar-rs: 0.095 s, verifier: 4.124 s 12: relat_1 mizar-rs: 0.333 s, verifier: 5.705 s 13: funct_1 mizar-rs: 0.381 s, verifier: 4.989 s 14: grfunc_1 mizar-rs: 0.082 s, verifier: 2.748 s 15: relat_2 mizar-rs: 0.065 s, verifier: 1.045 s 16: ordinal1 mizar-rs: 0.210 s, verifier: 1.123 s 17: wellord1 mizar-rs: 0.410 s, verifier: 2.086 s 18: relset_1 mizar-rs: 0.099 s, verifier: 0.839 s 19: partfun1 mizar-rs: 0.337 s, verifier: 2.499 s 20: mcart_1 mizar-rs: 0.234 s, verifier: 2.828 s 21: wellord2 mizar-rs: 0.147 s, verifier: 2.316 s 22: funct_2 mizar-rs: 0.698 s, verifier: 5.240 s 23: binop_1 mizar-rs: 0.083 s, verifier: 1.730 s 24: domain_1 mizar-rs: 0.082 s, verifier: 1.484 s 25: funct_3 mizar-rs: 0.285 s, verifier: 2.388 s 26: funcop_1 mizar-rs: 0.525 s, verifier: 2.781 s 27: realset1 mizar-rs: 0.035 s, verifier: 0.529 s 28: funct_4 mizar-rs: 1.172 s, verifier: 4.517 s 29: numerals mizar-rs: 0.002 s, verifier: 0.044 s 30: ordinal2 mizar-rs: 0.414 s, verifier: 1.889 s 31: ordinal3 mizar-rs: 0.234 s, verifier: 0.958 s 32: wellset1 mizar-rs: 0.197 s, verifier: 0.960 s 33: multop_1 mizar-rs: 0.031 s, verifier: 0.193 s 34: schems_1 mizar-rs: 0.003 s, verifier: 0.028 s 35: sysrel mizar-rs: 0.154 s, verifier: 0.614 s 36: finset_1 mizar-rs: 0.227 s, verifier: 1.154 s 37: card_1 mizar-rs: 0.390 s, verifier: 1.701 s 38: classes1 mizar-rs: 0.506 s, verifier: 2.116 s 39: pboole mizar-rs: 1.207 s, verifier: 5.327 s 40: gate_1 mizar-rs: 0.260 s, verifier: 1.032 s 41: gate_2 mizar-rs: 0.052 s, verifier: 0.269 s 42: gate_3 mizar-rs: 0.391 s, verifier: 1.262 s 43: gate_4 mizar-rs: 0.096 s, verifier: 0.568 s 44: gate_5 mizar-rs: 8.774 s, verifier: 38.920 s 45: finsub_1 mizar-rs: 0.029 s, verifier: 0.162 s 46: orders_1 mizar-rs: 0.514 s, verifier: 2.661 s 47: setwiseo mizar-rs: 0.373 s, verifier: 2.007 s 48: fraenkel mizar-rs: 0.104 s, verifier: 0.607 s 49: funct_5 mizar-rs: 0.490 s, verifier: 2.217 s 50: partfun2 mizar-rs: 0.176 s, verifier: 1.002 s 51: card_3 mizar-rs: 1.024 s, verifier: 5.011 s 52: funct_6 mizar-rs: 0.783 s, verifier: 3.518 s 53: arytm_3 mizar-rs: 0.271 s, verifier: 1.267 s 54: arytm_2 mizar-rs: 0.685 s, verifier: 2.816 s 55: arytm_1 mizar-rs: 0.030 s, verifier: 0.172 s 56: numbers mizar-rs: 0.533 s, verifier: 2.371 s 57: arytm_0 mizar-rs: 0.586 s, verifier: 2.553 s 58: xcmplx_0 mizar-rs: 0.124 s, verifier: 0.678 s 59: arithm mizar-rs: 0.011 s, verifier: 0.059 s 60: xxreal_0 mizar-rs: 0.080 s, verifier: 0.396 s 61: xreal_0 mizar-rs: 0.149 s, verifier: 0.648 s 62: real mizar-rs: 0.016 s, verifier: 0.109 s 63: xcmplx_1 mizar-rs: 0.158 s, verifier: 0.991 s 64: xreal_1 mizar-rs: 0.384 s, verifier: 2.148 s 65: axioms mizar-rs: 0.047 s, verifier: 0.275 s 66: real_1 mizar-rs: 0.008 s, verifier: 0.071 s 67: square_1 mizar-rs: 0.181 s, verifier: 1.181 s 68: nat_1 mizar-rs: 0.374 s, verifier: 1.764 s 69: int_1 mizar-rs: 0.309 s, verifier: 1.454 s 70: rat_1 mizar-rs: 0.393 s, verifier: 1.397 s 71: membered mizar-rs: 0.284 s, verifier: 0.991 s 72: valued_0 mizar-rs: 0.856 s, verifier: 3.324 s 73: complex1 mizar-rs: 1.094 s, verifier: 4.681 s 74: absvalue mizar-rs: 0.170 s, verifier: 0.750 s 75: int_2 mizar-rs: 0.154 s, verifier: 0.844 s 76: nat_d mizar-rs: 0.394 s, verifier: 1.942 s 77: binop_2 mizar-rs: 0.201 s, verifier: 1.078 s 78: xxreal_1 mizar-rs: 0.977 s, verifier: 3.848 s 79: card_2 mizar-rs: 1.480 s, verifier: 6.152 s 80: xxreal_2 mizar-rs: 0.321 s, verifier: 1.393 s 81: xxreal_3 mizar-rs: 0.791 s, verifier: 3.297 s 82: member_1 mizar-rs: 0.954 s, verifier: 3.987 s 83: supinf_1 mizar-rs: 0.038 s, verifier: 0.235 s 84: quin_1 mizar-rs: 0.489 s, verifier: 3.166 s 85: classes2 mizar-rs: 0.222 s, verifier: 1.219 s 86: ordinal4 mizar-rs: 0.420 s, verifier: 1.974 s 87: finseq_1 mizar-rs: 3.077 s, verifier: 13.784 s 88: recdef_1 mizar-rs: 0.603 s, verifier: 3.113 s 89: eqrel_1 mizar-rs: 0.994 s, verifier: 4.781 s 90: finseq_2 mizar-rs: 1.530 s, verifier: 7.008 s 91: finseqop mizar-rs: 1.281 s, verifier: 5.797 s 92: finseq_3 mizar-rs: 7.263 s, verifier: 29.363 s 93: valued_1 mizar-rs: 4.515 s, verifier: 21.874 s 94: seq_1 mizar-rs: 0.866 s, verifier: 4.402 s 95: comseq_1 mizar-rs: 0.760 s, verifier: 3.643 s 96: xboolean mizar-rs: 0.819 s, verifier: 5.478 s 97: comseq_2 mizar-rs: 0.786 s, verifier: 3.906 s 98: seq_2 mizar-rs: 1.221 s, verifier: 6.753 s 99: margrel1 mizar-rs: 0.465 s, verifier: 2.182 s 100: toler_1 mizar-rs: 0.127 s, verifier: 0.795 s 101: trees_1 mizar-rs: 1.052 s, verifier: 5.749 s 102: finseq_4 mizar-rs: 3.635 s, verifier: 16.445 s 103: finsop_1 mizar-rs: 0.846 s, verifier: 4.191 s 104: setwop_2 mizar-rs: 1.324 s, verifier: 6.002 s 105: rfunct_1 mizar-rs: 2.069 s, verifier: 10.725 s 106: rvsum_1 mizar-rs: 2.869 s, verifier: 14.678 s 107: newton mizar-rs: 2.135 s, verifier: 11.309 s 108: card_4 mizar-rs: 1.835 s, verifier: 9.591 s 109: card_5 mizar-rs: 0.741 s, verifier: 4.709 s 110: trees_2 mizar-rs: 2.609 s, verifier: 13.240 s 111: valued_2 mizar-rs: 4.070 s, verifier: 32.581 s 112: seqm_3 mizar-rs: 1.433 s, verifier: 14.157 s 113: rfinseq mizar-rs: 2.331 s, verifier: 18.347 s 114: seq_4 mizar-rs: 6.502 s, verifier: 50.584 s 115: rcomp_1 mizar-rs: 0.491 s, verifier: 8.880 s 116: rfunct_2 mizar-rs: 1.777 s, verifier: 14.888 s 117: cfunct_1 mizar-rs: 1.743 s, verifier: 13.977 s 118: fcont_1 mizar-rs: 2.589 s, verifier: 19.226 s 119: fcont_2 mizar-rs: 1.276 s, verifier: 8.907 s 120: fdiff_1 mizar-rs: 2.933 s, verifier: 19.241 s 121: rolle mizar-rs: 1.119 s, verifier: 7.489 s 122: prepower mizar-rs: 2.814 s, verifier: 18.488 s 123: finseq_5 mizar-rs: 1.029 s, verifier: 6.269 s 124: rewrite1 mizar-rs: 1.005 s, verifier: 5.611 s 125: funct_7 mizar-rs: 4.185 s, verifier: 24.147 s 126: scheme1 mizar-rs: 0.706 s, verifier: 3.508 s 127: abian mizar-rs: 0.990 s, verifier: 6.096 s 128: power mizar-rs: 0.674 s, verifier: 4.033 s 129: polyeq_1 mizar-rs: 0.817 s, verifier: 7.176 s 130: series_1 mizar-rs: 1.822 s, verifier: 11.996 s 131: comseq_3 mizar-rs: 1.996 s, verifier: 12.794 s 132: cfcont_1 mizar-rs: 1.545 s, verifier: 9.282 s 133: cfdiff_1 mizar-rs: 3.077 s, verifier: 20.257 s 134: rpr_1 mizar-rs: 0.325 s, verifier: 1.582 s 135: supinf_2 mizar-rs: 0.967 s, verifier: 5.595 s 136: trees_a mizar-rs: 0.353 s, verifier: 1.590 s 137: pre_ff mizar-rs: 0.369 s, verifier: 2.333 s 138: trees_3 mizar-rs: 4.435 s, verifier: 20.718 s 139: partit1 mizar-rs: 0.510 s, verifier: 2.702 s 140: trees_4 mizar-rs: 1.098 s, verifier: 5.739 s 141: card_fil mizar-rs: 0.538 s, verifier: 2.770 s 142: binarith mizar-rs: 2.600 s, verifier: 23.998 s 143: pre_circ mizar-rs: 1.437 s, verifier: 7.192 s 144: finseq_6 mizar-rs: 10.592 s, verifier: 57.252 s 145: mboolean mizar-rs: 0.154 s, verifier: 0.758 s 146: wsierp_1 mizar-rs: 1.510 s, verifier: 7.681 s 147: glib_000 mizar-rs: 2.376 s, verifier: 13.491 s 148: pzfmisc1 mizar-rs: 0.253 s, verifier: 1.380 s 149: genealg1 mizar-rs: 2.366 s, verifier: 11.385 s 150: binari_2 mizar-rs: 3.395 s, verifier: 33.361 s 151: trees_9 mizar-rs: 1.921 s, verifier: 10.165 s 152: mssubfam mizar-rs: 0.517 s, verifier: 3.080 s 153: relset_2 mizar-rs: 0.378 s, verifier: 2.043 s 154: recdef_2 mizar-rs: 0.254 s, verifier: 1.457 s 155: prob_1 mizar-rs: 0.411 s, verifier: 2.191 s 156: prob_2 mizar-rs: 0.549 s, verifier: 3.232 s 157: limfunc1 mizar-rs: 4.365 s, verifier: 28.518 s 158: limfunc2 mizar-rs: 3.757 s, verifier: 26.300 s 159: seqfunc mizar-rs: 0.987 s, verifier: 5.721 s 160: limfunc3 mizar-rs: 2.686 s, verifier: 18.432 s 161: fcont_3 mizar-rs: 2.483 s, verifier: 16.656 s 162: limfunc4 mizar-rs: 1.982 s, verifier: 12.681 s 163: l_hospit mizar-rs: 2.325 s, verifier: 15.078 s 164: fdiff_2 mizar-rs: 6.522 s, verifier: 42.981 s 165: fdiff_3 mizar-rs: 5.513 s, verifier: 34.903 s 166: measure1 mizar-rs: 0.592 s, verifier: 3.809 s 167: measure2 mizar-rs: 0.426 s, verifier: 2.572 s 168: measure3 mizar-rs: 1.107 s, verifier: 6.868 s 169: measure4 mizar-rs: 0.672 s, verifier: 4.106 s 170: rfunct_3 mizar-rs: 5.231 s, verifier: 29.326 s 171: measure5 mizar-rs: 0.146 s, verifier: 0.712 s 172: rearran1 mizar-rs: 5.003 s, verifier: 27.460 s 173: measure6 mizar-rs: 1.715 s, verifier: 10.673 s 174: extreal1 mizar-rs: 1.084 s, verifier: 6.344 s 175: measure7 mizar-rs: 1.284 s, verifier: 7.785 s 176: rfunct_4 mizar-rs: 1.549 s, verifier: 7.352 s 177: mesfunc1 mizar-rs: 1.224 s, verifier: 6.778 s 178: sin_cos mizar-rs: 5.106 s, verifier: 33.962 s 179: mesfunc2 mizar-rs: 1.475 s, verifier: 8.770 s 180: sin_cos2 mizar-rs: 1.180 s, verifier: 8.031 s 181: sin_cos3 mizar-rs: 0.821 s, verifier: 6.452 s 182: sin_cos4 mizar-rs: 0.371 s, verifier: 2.408 s 183: sin_cos5 mizar-rs: 0.572 s, verifier: 4.179 s 184: asympt_0 mizar-rs: 2.384 s, verifier: 15.374 s 185: comptrig mizar-rs: 1.336 s, verifier: 9.484 s 186: complex2 mizar-rs: 1.187 s, verifier: 8.343 s 187: polyeq_2 mizar-rs: 0.590 s, verifier: 5.073 s 188: polyeq_3 mizar-rs: 2.231 s, verifier: 19.046 s 189: polyeq_4 mizar-rs: 0.545 s, verifier: 3.758 s 190: polyeq_5 mizar-rs: 6.111 s, verifier: 87.589 s 191: sin_cos6 mizar-rs: 1.126 s, verifier: 6.905 s 192: euler_1 mizar-rs: 1.162 s, verifier: 5.524 s 193: euler_2 mizar-rs: 0.846 s, verifier: 4.919 s 194: asympt_1 mizar-rs: 6.648 s, verifier: 42.860 s 195: series_3 mizar-rs: 2.603 s, verifier: 15.660 s 196: series_4 mizar-rs: 1.137 s, verifier: 5.778 s 197: series_5 mizar-rs: 2.022 s, verifier: 11.897 s 198: quaterni mizar-rs: 10.226 s, verifier: 19.886 s 199: afinsq_1 mizar-rs: 4.001 s, verifier: 19.466 s 200: nat_2 mizar-rs: 0.278 s, verifier: 1.179 s 201: pepin mizar-rs: 1.147 s, verifier: 7.511 s 202: irrat_1 mizar-rs: 1.103 s, verifier: 6.354 s 203: taylor_1 mizar-rs: 2.532 s, verifier: 21.652 s 204: holder_1 mizar-rs: 1.159 s, verifier: 12.772 s 205: fdiff_4 mizar-rs: 1.563 s, verifier: 13.817 s 206: fdiff_5 mizar-rs: 1.150 s, verifier: 10.491 s 207: fdiff_6 mizar-rs: 2.350 s, verifier: 14.428 s 208: fdiff_7 mizar-rs: 1.229 s, verifier: 6.899 s 209: fdiff_8 mizar-rs: 1.536 s, verifier: 6.661 s 210: sin_cos7 mizar-rs: 1.828 s, verifier: 13.062 s 211: sin_cos8 mizar-rs: 0.899 s, verifier: 7.287 s 212: bvfunc_1 mizar-rs: 1.159 s, verifier: 6.647 s 213: bvfunc_2 mizar-rs: 0.420 s, verifier: 2.507 s 214: taylor_2 mizar-rs: 1.150 s, verifier: 7.511 s 215: catalan1 mizar-rs: 0.246 s, verifier: 1.420 s 216: pythtrip mizar-rs: 0.436 s, verifier: 2.533 s 217: series_2 mizar-rs: 2.719 s, verifier: 26.522 s 218: fib_num mizar-rs: 0.705 s, verifier: 6.668 s 219: partit_2 mizar-rs: 0.388 s, verifier: 2.020 s 220: bvfunc_3 mizar-rs: 0.470 s, verifier: 2.896 s 221: bvfunc_4 mizar-rs: 0.333 s, verifier: 2.925 s 222: bvfunc_5 mizar-rs: 0.268 s, verifier: 1.350 s 223: bvfunc_6 mizar-rs: 7.861 s, verifier: 61.873 s 224: bvfunc11 mizar-rs: 0.322 s, verifier: 1.841 s 225: bvfunc14 mizar-rs: 5.070 s, verifier: 18.521 s 226: bvfunc25 mizar-rs: 0.588 s, verifier: 3.303 s 227: finseq_7 mizar-rs: 1.065 s, verifier: 5.376 s 228: prgcor_1 mizar-rs: 1.520 s, verifier: 7.990 s 229: fdiff_9 mizar-rs: 1.527 s, verifier: 8.119 s 230: arrow mizar-rs: 0.296 s, verifier: 1.925 s 231: real_3 mizar-rs: 2.837 s, verifier: 17.545 s 232: fdiff_10 mizar-rs: 1.160 s, verifier: 6.124 s 233: hfdiff_1 mizar-rs: 3.684 s, verifier: 21.512 s 234: pre_poly mizar-rs: 13.091 s, verifier: 78.571 s 235: prgcor_2 mizar-rs: 0.693 s, verifier: 3.711 s 236: sin_cos9 mizar-rs: 3.550 s, verifier: 22.252 s 237: sincos10 mizar-rs: 2.475 s, verifier: 18.321 s 238: mesfunc3 mizar-rs: 4.922 s, verifier: 26.229 s 239: mesfunc4 mizar-rs: 4.241 s, verifier: 20.271 s 240: rvsum_2 mizar-rs: 0.950 s, verifier: 6.419 s 241: finseq_8 mizar-rs: 1.008 s, verifier: 8.430 s 242: pnproc_1 mizar-rs: 2.791 s, verifier: 18.305 s 243: integra1 mizar-rs: 8.936 s, verifier: 54.343 s 244: integra2 mizar-rs: 2.242 s, verifier: 15.775 s 245: rfinseq2 mizar-rs: 1.132 s, verifier: 9.778 s 246: integra3 mizar-rs: 13.200 s, verifier: 76.667 s 247: integra4 mizar-rs: 3.840 s, verifier: 28.139 s 248: integra5 mizar-rs: 2.692 s, verifier: 16.662 s 249: integr12 mizar-rs: 4.813 s, verifier: 26.533 s 250: integra8 mizar-rs: 1.827 s, verifier: 11.800 s 251: card_lar mizar-rs: 0.242 s, verifier: 1.324 s 252: fuzzy_1 mizar-rs: 0.744 s, verifier: 4.435 s 253: kurato_0 mizar-rs: 0.214 s, verifier: 1.289 s 254: partfun3 mizar-rs: 0.895 s, verifier: 4.582 s 255: fuzzy_2 mizar-rs: 1.003 s, verifier: 5.883 s 256: fuzzy_4 mizar-rs: 1.589 s, verifier: 7.668 s 257: setlim_1 mizar-rs: 0.488 s, verifier: 2.837 s 258: diff_1 mizar-rs: 1.878 s, verifier: 10.661 s 259: rinfsup1 mizar-rs: 1.522 s, verifier: 9.462 s 260: setlim_2 mizar-rs: 0.710 s, verifier: 3.917 s 261: prob_3 mizar-rs: 1.434 s, verifier: 7.972 s 262: dynkin mizar-rs: 0.289 s, verifier: 1.389 s 263: prob_4 mizar-rs: 1.904 s, verifier: 8.892 s 264: kolmog01 mizar-rs: 3.757 s, verifier: 24.319 s 265: mesfunc5 mizar-rs: 17.098 s, verifier: 112.005 s 266: diff_2 mizar-rs: 1.831 s, verifier: 15.580 s 267: int_6 mizar-rs: 2.513 s, verifier: 18.482 s 268: bor_cant mizar-rs: 5.202 s, verifier: 46.016 s 269: mesfunc6 mizar-rs: 2.463 s, verifier: 18.208 s 270: diff_3 mizar-rs: 4.032 s, verifier: 29.650 s 271: mesfunc7 mizar-rs: 1.791 s, verifier: 10.950 s 272: mesfun6c mizar-rs: 2.406 s, verifier: 17.241 s 273: diff_4 mizar-rs: 2.581 s, verifier: 20.741 s 274: rinfsup2 mizar-rs: 1.252 s, verifier: 13.540 s 275: mesfunc8 mizar-rs: 2.026 s, verifier: 26.667 s 276: mesfunc9 mizar-rs: 4.537 s, verifier: 32.129 s 277: mesfun10 mizar-rs: 2.131 s, verifier: 19.496 s 278: matrix_0 mizar-rs: 1.670 s, verifier: 14.515 s 279: afinsq_2 mizar-rs: 8.013 s, verifier: 49.167 s 280: gobrd10 mizar-rs: 0.665 s, verifier: 8.561 s 281: integr13 mizar-rs: 2.890 s, verifier: 16.890 s 282: integr14 mizar-rs: 1.418 s, verifier: 8.627 s 283: stirl2_1 mizar-rs: 11.238 s, verifier: 57.394 s 284: nat_3 mizar-rs: 3.768 s, verifier: 20.154 s 285: nat_4 mizar-rs: 21.554 s, verifier: 119.392 s 286: fib_num2 mizar-rs: 3.608 s, verifier: 23.096 s 287: fib_num3 mizar-rs: 1.153 s, verifier: 6.867 s 288: ordinal5 mizar-rs: 1.949 s, verifier: 9.340 s 289: ordinal6 mizar-rs: 3.153 s, verifier: 15.675 s 290: descip_1 mizar-rs: 102.513 s, verifier: 216.697 s 291: zf_lang mizar-rs: 1.800 s, verifier: 8.141 s 292: zf_model mizar-rs: 0.345 s, verifier: 1.340 s 293: zf_colla mizar-rs: 0.202 s, verifier: 1.014 s 294: zfmodel1 mizar-rs: 1.728 s, verifier: 17.452 s 295: zf_lang1 mizar-rs: 3.056 s, verifier: 28.397 s 296: zf_refle mizar-rs: 0.791 s, verifier: 20.564 s 297: zfrefle1 mizar-rs: 0.676 s, verifier: 12.945 s 298: qc_lang1 mizar-rs: 2.177 s, verifier: 18.209 s 299: qc_lang2 mizar-rs: 1.563 s, verifier: 12.248 s 300: qc_lang3 mizar-rs: 0.330 s, verifier: 5.296 s 301: cqc_lang mizar-rs: 0.476 s, verifier: 4.029 s 302: cqc_the1 mizar-rs: 1.249 s, verifier: 5.999 s 303: valuat_1 mizar-rs: 0.892 s, verifier: 5.071 s 304: zfmodel2 mizar-rs: 2.131 s, verifier: 10.247 s 305: lukasi_1 mizar-rs: 0.118 s, verifier: 0.608 s 306: procal_1 mizar-rs: 0.100 s, verifier: 0.571 s 307: zf_fund1 mizar-rs: 1.625 s, verifier: 7.246 s 308: intpro_1 mizar-rs: 0.694 s, verifier: 3.278 s 309: cqc_the2 mizar-rs: 0.435 s, verifier: 2.009 s 310: zf_fund2 mizar-rs: 0.934 s, verifier: 4.054 s 311: hilbert1 mizar-rs: 0.404 s, verifier: 1.665 s 312: cqc_sim1 mizar-rs: 2.540 s, verifier: 12.367 s 313: modal_1 mizar-rs: 8.037 s, verifier: 33.671 s 314: cqc_the3 mizar-rs: 0.391 s, verifier: 1.480 s 315: qc_lang4 mizar-rs: 0.813 s, verifier: 4.190 s 316: substut1 mizar-rs: 1.732 s, verifier: 9.230 s 317: sublemma mizar-rs: 5.413 s, verifier: 28.630 s 318: substut2 mizar-rs: 0.779 s, verifier: 3.270 s 319: calcul_1 mizar-rs: 4.052 s, verifier: 22.218 s 320: calcul_2 mizar-rs: 0.909 s, verifier: 7.169 s 321: henmodel mizar-rs: 2.085 s, verifier: 13.774 s 322: goedelcp mizar-rs: 1.739 s, verifier: 12.944 s 323: qc_trans mizar-rs: 2.649 s, verifier: 14.447 s 324: ntalgo_1 mizar-rs: 2.728 s, verifier: 135.319 s 325: struct_0 mizar-rs: 0.132 s, verifier: 1.389 s 326: algstr_0 mizar-rs: 0.125 s, verifier: 2.155 s 327: incsp_1 mizar-rs: 0.543 s, verifier: 2.779 s 328: pre_topc mizar-rs: 0.167 s, verifier: 1.500 s 329: orders_2 mizar-rs: 0.505 s, verifier: 2.597 s 330: graph_1 mizar-rs: 1.183 s, verifier: 8.880 s 331: cat_1 mizar-rs: 0.503 s, verifier: 5.227 s 332: petri mizar-rs: 0.162 s, verifier: 3.422 s 333: net_1 mizar-rs: 0.097 s, verifier: 3.251 s 334: lattices mizar-rs: 0.226 s, verifier: 1.279 s 335: tops_1 mizar-rs: 0.273 s, verifier: 1.726 s 336: connsp_1 mizar-rs: 0.454 s, verifier: 2.398 s 337: tops_2 mizar-rs: 0.484 s, verifier: 2.815 s 338: rlvect_1 mizar-rs: 1.296 s, verifier: 6.308 s 339: rlsub_1 mizar-rs: 1.001 s, verifier: 5.568 s 340: group_1 mizar-rs: 0.738 s, verifier: 3.768 s 341: vectsp_1 mizar-rs: 0.509 s, verifier: 2.866 s 342: algstr_1 mizar-rs: 0.346 s, verifier: 1.875 s 343: complfld mizar-rs: 0.536 s, verifier: 3.013 s 344: parsp_1 mizar-rs: 0.343 s, verifier: 2.010 s 345: symsp_1 mizar-rs: 0.376 s, verifier: 2.571 s 346: ortsp_1 mizar-rs: 0.482 s, verifier: 2.654 s 347: compts_1 mizar-rs: 0.344 s, verifier: 2.011 s 348: rlsub_2 mizar-rs: 1.354 s, verifier: 7.163 s 349: midsp_1 mizar-rs: 0.173 s, verifier: 0.829 s 350: funcsdom mizar-rs: 1.318 s, verifier: 8.680 s 351: vectsp_2 mizar-rs: 0.835 s, verifier: 4.053 s 352: filter_0 mizar-rs: 0.591 s, verifier: 3.340 s 353: lattice2 mizar-rs: 0.382 s, verifier: 2.145 s 354: robbins1 mizar-rs: 0.629 s, verifier: 8.184 s 355: qmax_1 mizar-rs: 0.319 s, verifier: 4.757 s 356: parsp_2 mizar-rs: 0.663 s, verifier: 5.818 s 357: rlvect_2 mizar-rs: 5.546 s, verifier: 33.890 s 358: analoaf mizar-rs: 0.378 s, verifier: 2.610 s 359: metric_1 mizar-rs: 0.806 s, verifier: 4.308 s 360: diraf mizar-rs: 0.285 s, verifier: 1.239 s 361: aff_1 mizar-rs: 0.102 s, verifier: 0.625 s 362: aff_2 mizar-rs: 0.235 s, verifier: 1.334 s 363: aff_3 mizar-rs: 0.312 s, verifier: 1.443 s 364: collsp mizar-rs: 0.095 s, verifier: 0.395 s 365: pasch mizar-rs: 0.246 s, verifier: 1.294 s 366: real_lat mizar-rs: 0.335 s, verifier: 1.567 s 367: tdgroup mizar-rs: 0.157 s, verifier: 0.715 s 368: transgeo mizar-rs: 0.705 s, verifier: 4.158 s 369: cat_2 mizar-rs: 1.281 s, verifier: 6.991 s 370: translac mizar-rs: 0.279 s, verifier: 1.553 s 371: anproj_1 mizar-rs: 6.476 s, verifier: 40.520 s 372: anproj_2 mizar-rs: 29.499 s, verifier: 120.589 s 373: rlvect_3 mizar-rs: 1.232 s, verifier: 6.605 s 374: group_2 mizar-rs: 1.822 s, verifier: 11.796 s 375: vectsp_4 mizar-rs: 0.938 s, verifier: 8.447 s 376: vectsp_5 mizar-rs: 1.319 s, verifier: 9.366 s 377: normsp_0 mizar-rs: 0.141 s, verifier: 0.349 s 378: normsp_1 mizar-rs: 0.733 s, verifier: 4.295 s 379: vfunct_1 mizar-rs: 1.618 s, verifier: 9.582 s 380: vectsp_6 mizar-rs: 2.341 s, verifier: 17.167 s 381: vectsp_7 mizar-rs: 0.834 s, verifier: 6.036 s 382: analmetr mizar-rs: 0.824 s, verifier: 13.588 s 383: group_3 mizar-rs: 1.542 s, verifier: 18.707 s 384: projdes1 mizar-rs: 0.092 s, verifier: 2.210 s 385: group_4 mizar-rs: 2.608 s, verifier: 24.923 s 386: gr_cy_1 mizar-rs: 1.774 s, verifier: 14.927 s 387: realset2 mizar-rs: 0.978 s, verifier: 7.273 s 388: connsp_2 mizar-rs: 0.214 s, verifier: 1.407 s 389: matrix_1 mizar-rs: 0.653 s, verifier: 4.602 s 390: fvsum_1 mizar-rs: 1.110 s, verifier: 7.961 s 391: matrix_3 mizar-rs: 2.279 s, verifier: 13.972 s 392: midsp_2 mizar-rs: 0.172 s, verifier: 0.945 s 393: grcat_1 mizar-rs: 0.795 s, verifier: 5.699 s 394: mod_2 mizar-rs: 0.804 s, verifier: 5.452 s 395: matrlin mizar-rs: 3.112 s, verifier: 21.964 s 396: polynom1 mizar-rs: 5.405 s, verifier: 36.495 s 397: algseq_1 mizar-rs: 0.166 s, verifier: 0.974 s 398: homothet mizar-rs: 0.240 s, verifier: 1.301 s 399: afvect0 mizar-rs: 0.497 s, verifier: 1.770 s 400: complsp1 mizar-rs: 0.096 s, verifier: 0.558 s 401: realset3 mizar-rs: 0.167 s, verifier: 1.087 s 402: algstr_2 mizar-rs: 0.281 s, verifier: 1.923 s 403: metric_2 mizar-rs: 0.171 s, verifier: 0.805 s 404: metric_3 mizar-rs: 0.996 s, verifier: 7.365 s 405: hessenbe mizar-rs: 0.124 s, verifier: 0.710 s 406: incproj mizar-rs: 0.243 s, verifier: 1.219 s 407: afvect01 mizar-rs: 0.095 s, verifier: 0.577 s 408: normform mizar-rs: 0.475 s, verifier: 3.065 s 409: o_ring_1 mizar-rs: 0.803 s, verifier: 5.283 s 410: algstr_3 mizar-rs: 0.089 s, verifier: 0.685 s 411: projred1 mizar-rs: 0.273 s, verifier: 2.069 s 412: rmod_2 mizar-rs: 0.827 s, verifier: 5.732 s 413: rmod_3 mizar-rs: 0.992 s, verifier: 5.730 s 414: rmod_4 mizar-rs: 2.646 s, verifier: 15.628 s 415: geomtrap mizar-rs: 1.570 s, verifier: 9.840 s 416: projred2 mizar-rs: 0.260 s, verifier: 2.278 s 417: conaffm mizar-rs: 0.317 s, verifier: 2.152 s 418: conmetr mizar-rs: 0.638 s, verifier: 3.374 s 419: papdesaf mizar-rs: 0.361 s, verifier: 1.543 s 420: pardepap mizar-rs: 0.030 s, verifier: 0.228 s 421: semi_af1 mizar-rs: 0.442 s, verifier: 2.228 s 422: aff_4 mizar-rs: 0.392 s, verifier: 2.292 s 423: afproj mizar-rs: 1.158 s, verifier: 6.999 s 424: heyting1 mizar-rs: 1.004 s, verifier: 6.251 s 425: prelamb mizar-rs: 1.972 s, verifier: 9.548 s 426: oppcat_1 mizar-rs: 1.739 s, verifier: 10.387 s 427: euclmetr mizar-rs: 0.329 s, verifier: 2.535 s 428: filter_1 mizar-rs: 3.361 s, verifier: 18.843 s 429: conmetr1 mizar-rs: 0.442 s, verifier: 6.872 s 430: nat_lat mizar-rs: 0.296 s, verifier: 5.162 s 431: group_5 mizar-rs: 1.516 s, verifier: 11.891 s 432: cat_3 mizar-rs: 0.865 s, verifier: 9.425 s 433: nattra_1 mizar-rs: 1.898 s, verifier: 11.761 s 434: pcomps_1 mizar-rs: 0.579 s, verifier: 7.089 s 435: ali2 mizar-rs: 0.211 s, verifier: 2.322 s 436: bhsp_1 mizar-rs: 0.565 s, verifier: 10.534 s 437: bhsp_2 mizar-rs: 0.430 s, verifier: 9.714 s 438: bhsp_3 mizar-rs: 0.546 s, verifier: 9.678 s 439: ens_1 mizar-rs: 2.709 s, verifier: 19.315 s 440: borsuk_1 mizar-rs: 1.966 s, verifier: 15.655 s 441: tbsp_1 mizar-rs: 0.653 s, verifier: 9.275 s 442: group_6 mizar-rs: 2.071 s, verifier: 17.204 s 443: monoid_0 mizar-rs: 1.926 s, verifier: 17.347 s 444: rusub_1 mizar-rs: 1.790 s, verifier: 15.267 s 445: rusub_2 mizar-rs: 1.603 s, verifier: 14.179 s 446: rlvect_4 mizar-rs: 1.576 s, verifier: 13.569 s 447: rusub_3 mizar-rs: 2.222 s, verifier: 20.198 s 448: rlvect_5 mizar-rs: 2.042 s, verifier: 18.183 s 449: rusub_4 mizar-rs: 1.279 s, verifier: 11.293 s 450: t_0topsp mizar-rs: 0.244 s, verifier: 4.359 s 451: cantor_1 mizar-rs: 0.198 s, verifier: 4.267 s 452: tsep_1 mizar-rs: 0.594 s, verifier: 7.215 s 453: tdlat_1 mizar-rs: 0.881 s, verifier: 7.591 s 454: lattice3 mizar-rs: 0.927 s, verifier: 8.066 s 455: tdlat_2 mizar-rs: 0.841 s, verifier: 5.691 s 456: tdlat_3 mizar-rs: 0.393 s, verifier: 2.978 s 457: tops_3 mizar-rs: 0.201 s, verifier: 1.243 s 458: urysohn1 mizar-rs: 0.812 s, verifier: 5.434 s 459: unialg_1 mizar-rs: 0.072 s, verifier: 0.372 s 460: unialg_2 mizar-rs: 1.704 s, verifier: 8.887 s 461: lang1 mizar-rs: 0.664 s, verifier: 3.775 s 462: dtconstr mizar-rs: 3.898 s, verifier: 22.888 s 463: pralg_1 mizar-rs: 1.708 s, verifier: 10.303 s 464: yellow_0 mizar-rs: 0.336 s, verifier: 2.030 s 465: cat_5 mizar-rs: 2.740 s, verifier: 15.773 s 466: altcat_1 mizar-rs: 0.614 s, verifier: 3.139 s 467: orders_3 mizar-rs: 0.269 s, verifier: 1.678 s 468: yellow_1 mizar-rs: 0.716 s, verifier: 4.126 s 469: waybel_0 mizar-rs: 0.562 s, verifier: 3.747 s 470: quantal1 mizar-rs: 0.676 s, verifier: 4.322 s 471: yellow_2 mizar-rs: 0.372 s, verifier: 2.611 s 472: waybel_1 mizar-rs: 1.459 s, verifier: 9.546 s 473: yellow_3 mizar-rs: 0.706 s, verifier: 4.926 s 474: yellow_4 mizar-rs: 0.292 s, verifier: 1.563 s 475: tmap_1 mizar-rs: 1.716 s, verifier: 11.051 s 476: tex_1 mizar-rs: 0.429 s, verifier: 2.393 s 477: waybel_2 mizar-rs: 1.270 s, verifier: 7.674 s 478: waybel_3 mizar-rs: 1.103 s, verifier: 7.386 s 479: tex_2 mizar-rs: 0.765 s, verifier: 5.335 s 480: tex_4 mizar-rs: 0.622 s, verifier: 3.897 s 481: tsp_1 mizar-rs: 0.320 s, verifier: 1.703 s 482: yellow_8 mizar-rs: 0.213 s, verifier: 1.087 s 483: topmetr mizar-rs: 0.653 s, verifier: 3.574 s 484: heine mizar-rs: 0.705 s, verifier: 5.174 s 485: treal_1 mizar-rs: 1.221 s, verifier: 7.198 s 486: borsuk_2 mizar-rs: 1.462 s, verifier: 9.967 s 487: yellow_6 mizar-rs: 2.286 s, verifier: 14.341 s 488: msualg_1 mizar-rs: 0.411 s, verifier: 2.132 s 489: pralg_2 mizar-rs: 0.704 s, verifier: 3.746 s 490: msualg_2 mizar-rs: 1.286 s, verifier: 7.147 s 491: msualg_3 mizar-rs: 1.193 s, verifier: 7.616 s 492: waybel_5 mizar-rs: 2.593 s, verifier: 16.139 s 493: yellow_5 mizar-rs: 0.127 s, verifier: 0.612 s 494: yellow_7 mizar-rs: 1.087 s, verifier: 6.263 s 495: alg_1 mizar-rs: 1.144 s, verifier: 6.360 s 496: waybel_4 mizar-rs: 1.413 s, verifier: 9.723 s 497: waybel_6 mizar-rs: 2.348 s, verifier: 15.238 s 498: waybel_7 mizar-rs: 1.016 s, verifier: 6.803 s 499: waybel_8 mizar-rs: 0.762 s, verifier: 4.809 s 500: waybel_9 mizar-rs: 1.358 s, verifier: 8.121 s 501: waybel11 mizar-rs: 2.029 s, verifier: 13.709 s 502: yellow_9 mizar-rs: 1.769 s, verifier: 11.087 s 503: topgrp_1 mizar-rs: 0.971 s, verifier: 5.432 s 504: rusub_5 mizar-rs: 0.498 s, verifier: 2.982 s 505: convex1 mizar-rs: 10.589 s, verifier: 61.946 s 506: msafree mizar-rs: 2.645 s, verifier: 15.895 s 507: msualg_4 mizar-rs: 1.144 s, verifier: 6.674 s 508: msafree1 mizar-rs: 0.467 s, verifier: 2.686 s 509: msafree2 mizar-rs: 1.115 s, verifier: 6.044 s 510: msualg_5 mizar-rs: 1.510 s, verifier: 9.483 s 511: hahnban mizar-rs: 1.713 s, verifier: 11.244 s 512: closure2 mizar-rs: 0.719 s, verifier: 3.857 s 513: lattice4 mizar-rs: 0.379 s, verifier: 2.030 s 514: waybel12 mizar-rs: 0.954 s, verifier: 5.975 s 515: waybel14 mizar-rs: 1.246 s, verifier: 7.969 s 516: yellow12 mizar-rs: 0.689 s, verifier: 4.238 s 517: lattice5 mizar-rs: 7.007 s, verifier: 44.612 s 518: yellow11 mizar-rs: 6.551 s, verifier: 27.152 s 519: yellow13 mizar-rs: 0.442 s, verifier: 2.607 s 520: rltopsp1 mizar-rs: 1.898 s, verifier: 12.148 s 521: rsspace mizar-rs: 0.917 s, verifier: 6.647 s 522: euclid mizar-rs: 0.969 s, verifier: 6.966 s 523: topmetr2 mizar-rs: 0.441 s, verifier: 2.909 s 524: topreal1 mizar-rs: 4.269 s, verifier: 30.629 s 525: topreal3 mizar-rs: 2.637 s, verifier: 17.067 s 526: topreal2 mizar-rs: 4.937 s, verifier: 32.256 s 527: topreal4 mizar-rs: 2.764 s, verifier: 17.225 s 528: goboard1 mizar-rs: 3.941 s, verifier: 22.868 s 529: goboard2 mizar-rs: 4.801 s, verifier: 28.973 s 530: sppol_1 mizar-rs: 3.561 s, verifier: 23.243 s 531: sppol_2 mizar-rs: 5.405 s, verifier: 29.460 s 532: jordan1 mizar-rs: 2.402 s, verifier: 15.865 s 533: goboard5 mizar-rs: 8.970 s, verifier: 48.892 s 534: goboard6 mizar-rs: 5.733 s, verifier: 36.282 s 535: goboard7 mizar-rs: 6.610 s, verifier: 38.296 s 536: pscomp_1 mizar-rs: 5.767 s, verifier: 37.447 s 537: rsspace2 mizar-rs: 2.241 s, verifier: 19.559 s 538: rsspace3 mizar-rs: 3.007 s, verifier: 20.169 s 539: lopban_1 mizar-rs: 5.801 s, verifier: 43.105 s 540: vectsp_9 mizar-rs: 2.320 s, verifier: 15.848 s 541: ranknull mizar-rs: 1.919 s, verifier: 10.410 s 542: mod_3 mizar-rs: 0.705 s, verifier: 2.556 s 543: analort mizar-rs: 0.629 s, verifier: 3.579 s 544: prvect_1 mizar-rs: 1.053 s, verifier: 6.864 s 545: vectsp_8 mizar-rs: 1.275 s, verifier: 8.667 s 546: msualg_7 mizar-rs: 1.869 s, verifier: 10.885 s 547: t_1topsp mizar-rs: 0.197 s, verifier: 1.285 s 548: borsuk_3 mizar-rs: 0.522 s, verifier: 3.540 s 549: toprns_1 mizar-rs: 0.883 s, verifier: 7.483 s 550: isocat_1 mizar-rs: 1.177 s, verifier: 7.775 s 551: ringcat1 mizar-rs: 0.571 s, verifier: 4.233 s 552: modcat_1 mizar-rs: 0.237 s, verifier: 2.025 s 553: metric_6 mizar-rs: 0.375 s, verifier: 2.814 s 554: ff_siec mizar-rs: 0.252 s, verifier: 1.741 s 555: e_siec mizar-rs: 0.238 s, verifier: 0.915 s 556: commacat mizar-rs: 0.660 s, verifier: 2.816 s 557: bhsp_4 mizar-rs: 1.577 s, verifier: 10.313 s 558: midsp_3 mizar-rs: 0.527 s, verifier: 2.406 s 559: gr_cy_2 mizar-rs: 0.759 s, verifier: 3.905 s 560: isocat_2 mizar-rs: 2.869 s, verifier: 18.089 s 561: lmod_6 mizar-rs: 0.107 s, verifier: 1.080 s 562: dirort mizar-rs: 0.238 s, verifier: 3.335 s 563: mod_4 mizar-rs: 1.363 s, verifier: 10.544 s 564: pcomps_2 mizar-rs: 0.680 s, verifier: 10.478 s 565: goboard3 mizar-rs: 6.392 s, verifier: 45.303 s 566: goboard4 mizar-rs: 3.275 s, verifier: 24.090 s 567: cat_4 mizar-rs: 1.509 s, verifier: 14.770 s 568: tsep_2 mizar-rs: 0.109 s, verifier: 5.129 s 569: fin_topo mizar-rs: 0.497 s, verifier: 5.316 s 570: coh_sp mizar-rs: 0.682 s, verifier: 4.559 s 571: monoid_1 mizar-rs: 4.428 s, verifier: 25.677 s 572: lmod_7 mizar-rs: 0.561 s, verifier: 3.675 s 573: hahnban1 mizar-rs: 1.429 s, verifier: 7.556 s 574: openlatt mizar-rs: 0.526 s, verifier: 2.664 s 575: lopclset mizar-rs: 1.094 s, verifier: 4.882 s 576: boolmark mizar-rs: 0.604 s, verifier: 6.432 s 577: freealg mizar-rs: 2.959 s, verifier: 19.362 s 578: tex_3 mizar-rs: 0.260 s, verifier: 5.104 s 579: bintree1 mizar-rs: 1.109 s, verifier: 9.559 s 580: boolealg mizar-rs: 0.227 s, verifier: 4.816 s 581: autgroup mizar-rs: 0.533 s, verifier: 6.114 s 582: tsp_2 mizar-rs: 0.322 s, verifier: 4.941 s 583: projpl_1 mizar-rs: 0.097 s, verifier: 1.070 s 584: sgraph1 mizar-rs: 0.522 s, verifier: 2.395 s 585: grsolv_1 mizar-rs: 0.867 s, verifier: 4.412 s 586: filter_2 mizar-rs: 1.919 s, verifier: 10.754 s 587: fsm_1 mizar-rs: 5.030 s, verifier: 29.415 s 588: msaterm mizar-rs: 1.427 s, verifier: 9.279 s 589: decomp_1 mizar-rs: 0.170 s, verifier: 1.241 s 590: msuhom_1 mizar-rs: 0.934 s, verifier: 5.793 s 591: autalg_1 mizar-rs: 0.663 s, verifier: 3.555 s 592: circuit1 mizar-rs: 2.381 s, verifier: 14.366 s 593: extens_1 mizar-rs: 0.501 s, verifier: 2.909 s 594: circuit2 mizar-rs: 2.703 s, verifier: 17.122 s 595: circcomb mizar-rs: 2.670 s, verifier: 15.199 s 596: graph_2 mizar-rs: 2.949 s, verifier: 16.126 s 597: latsubgr mizar-rs: 0.854 s, verifier: 5.156 s 598: unialg_3 mizar-rs: 0.535 s, verifier: 2.775 s 599: index_1 mizar-rs: 1.049 s, verifier: 5.874 s 600: weierstr mizar-rs: 0.690 s, verifier: 4.163 s 601: facirc_1 mizar-rs: 7.186 s, verifier: 46.635 s 602: cohsp_1 mizar-rs: 2.319 s, verifier: 14.606 s 603: pua2mss1 mizar-rs: 2.866 s, verifier: 18.763 s 604: endalg mizar-rs: 0.352 s, verifier: 2.338 s 605: goboard8 mizar-rs: 1.395 s, verifier: 8.272 s 606: triang_1 mizar-rs: 1.052 s, verifier: 6.495 s 607: goboard9 mizar-rs: 9.924 s, verifier: 50.499 s 608: altcat_2 mizar-rs: 0.518 s, verifier: 2.925 s 609: connsp_3 mizar-rs: 0.170 s, verifier: 0.865 s 610: closure1 mizar-rs: 1.139 s, verifier: 7.270 s 611: msualg_6 mizar-rs: 2.048 s, verifier: 13.880 s 612: msscyc_1 mizar-rs: 1.563 s, verifier: 9.865 s 613: msualg_8 mizar-rs: 0.852 s, verifier: 5.409 s 614: msscyc_2 mizar-rs: 0.975 s, verifier: 7.269 s 615: functor0 mizar-rs: 3.217 s, verifier: 19.383 s 616: functor1 mizar-rs: 0.621 s, verifier: 4.503 s 617: pralg_3 mizar-rs: 1.995 s, verifier: 12.437 s 618: msalimit mizar-rs: 1.169 s, verifier: 8.789 s 619: msualg_9 mizar-rs: 1.416 s, verifier: 7.841 s 620: msinst_1 mizar-rs: 1.256 s, verifier: 7.021 s 621: gobrd11 mizar-rs: 2.482 s, verifier: 19.534 s 622: gobrd12 mizar-rs: 3.325 s, verifier: 19.569 s 623: knaster mizar-rs: 0.673 s, verifier: 4.611 s 624: twoscomp mizar-rs: 0.834 s, verifier: 6.775 s 625: jordan3 mizar-rs: 4.909 s, verifier: 25.310 s 626: instalg1 mizar-rs: 2.034 s, verifier: 12.731 s 627: waybel10 mizar-rs: 1.340 s, verifier: 8.815 s 628: catalg_1 mizar-rs: 3.085 s, verifier: 16.148 s 629: altcat_3 mizar-rs: 0.211 s, verifier: 8.587 s 630: wellfnd1 mizar-rs: 0.485 s, verifier: 16.641 s 631: waybel13 mizar-rs: 1.177 s, verifier: 20.170 s 632: jordan4 mizar-rs: 4.426 s, verifier: 48.709 s 633: substlat mizar-rs: 0.290 s, verifier: 11.072 s 634: equation mizar-rs: 2.769 s, verifier: 33.271 s 635: msafree3 mizar-rs: 1.644 s, verifier: 18.237 s 636: functor2 mizar-rs: 0.507 s, verifier: 12.330 s 637: yoneda_1 mizar-rs: 1.155 s, verifier: 15.577 s 638: gcd_1 mizar-rs: 3.129 s, verifier: 30.366 s 639: birkhoff mizar-rs: 0.684 s, verifier: 14.559 s 640: closure3 mizar-rs: 0.546 s, verifier: 9.335 s 641: graph_3 mizar-rs: 16.281 s, verifier: 100.421 s 642: jordan5a mizar-rs: 3.111 s, verifier: 23.363 s 643: jordan5b mizar-rs: 4.507 s, verifier: 30.724 s 644: jordan5c mizar-rs: 2.933 s, verifier: 19.538 s 645: altcat_4 mizar-rs: 1.865 s, verifier: 9.648 s 646: waybel15 mizar-rs: 0.828 s, verifier: 5.199 s 647: jordan2b mizar-rs: 1.272 s, verifier: 8.322 s 648: topreal5 mizar-rs: 0.564 s, verifier: 3.645 s 649: uniform1 mizar-rs: 0.951 s, verifier: 6.629 s 650: sprect_1 mizar-rs: 7.960 s, verifier: 45.572 s 651: sprect_2 mizar-rs: 12.052 s, verifier: 77.640 s 652: jordan6 mizar-rs: 4.918 s, verifier: 32.851 s 653: functor3 mizar-rs: 1.625 s, verifier: 10.255 s 654: waybel16 mizar-rs: 0.557 s, verifier: 3.559 s 655: waybel17 mizar-rs: 1.672 s, verifier: 10.366 s 656: binari_3 mizar-rs: 0.865 s, verifier: 4.278 s 657: bintree2 mizar-rs: 1.092 s, verifier: 9.542 s 658: yellow10 mizar-rs: 1.024 s, verifier: 11.236 s 659: waybel18 mizar-rs: 2.754 s, verifier: 23.375 s 660: quofield mizar-rs: 3.444 s, verifier: 26.757 s 661: frechet mizar-rs: 1.527 s, verifier: 9.544 s 662: jordan5d mizar-rs: 3.260 s, verifier: 23.495 s 663: group_7 mizar-rs: 1.662 s, verifier: 11.077 s 664: jordan7 mizar-rs: 9.959 s, verifier: 52.709 s 665: waybel19 mizar-rs: 1.497 s, verifier: 9.199 s 666: waybel20 mizar-rs: 1.947 s, verifier: 11.656 s 667: waybel21 mizar-rs: 1.491 s, verifier: 12.405 s 668: waybel22 mizar-rs: 1.290 s, verifier: 16.320 s 669: graph_4 mizar-rs: 1.507 s, verifier: 15.405 s 670: jgraph_1 mizar-rs: 22.651 s, verifier: 123.931 s 671: idea_1 mizar-rs: 3.269 s, verifier: 22.423 s 672: mssublat mizar-rs: 2.985 s, verifier: 18.827 s 673: conlat_1 mizar-rs: 1.168 s, verifier: 7.058 s 674: taxonom1 mizar-rs: 0.534 s, verifier: 3.437 s 675: taxonom2 mizar-rs: 0.194 s, verifier: 1.348 s 676: sprect_3 mizar-rs: 5.770 s, verifier: 27.319 s 677: vectmetr mizar-rs: 2.454 s, verifier: 15.575 s 678: waybel23 mizar-rs: 1.005 s, verifier: 20.264 s 679: heyting2 mizar-rs: 0.828 s, verifier: 15.577 s 680: convex2 mizar-rs: 1.655 s, verifier: 18.122 s 681: yellow15 mizar-rs: 1.619 s, verifier: 17.320 s 682: graph_5 mizar-rs: 2.577 s, verifier: 28.520 s 683: convex3 mizar-rs: 1.090 s, verifier: 14.716 s 684: yellow18 mizar-rs: 2.766 s, verifier: 30.284 s 685: yellow20 mizar-rs: 2.631 s, verifier: 25.535 s 686: binom mizar-rs: 1.264 s, verifier: 17.529 s 687: card_fin mizar-rs: 7.737 s, verifier: 70.998 s 688: matrix_4 mizar-rs: 1.003 s, verifier: 16.190 s 689: matrix_5 mizar-rs: 0.482 s, verifier: 7.367 s 690: matrixr1 mizar-rs: 1.706 s, verifier: 13.510 s 691: complsp2 mizar-rs: 2.999 s, verifier: 35.885 s 692: matrixc1 mizar-rs: 2.615 s, verifier: 35.346 s 693: matrprob mizar-rs: 2.914 s, verifier: 33.981 s 694: rlaffin1 mizar-rs: 6.325 s, verifier: 49.469 s 695: pencil_1 mizar-rs: 1.459 s, verifier: 11.769 s 696: chain_1 mizar-rs: 5.043 s, verifier: 42.272 s 697: hallmar1 mizar-rs: 0.940 s, verifier: 10.355 s 698: revrot_1 mizar-rs: 4.656 s, verifier: 26.185 s 699: jgraph_2 mizar-rs: 7.264 s, verifier: 57.201 s 700: combgras mizar-rs: 4.152 s, verifier: 27.003 s 701: circcmb2 mizar-rs: 0.842 s, verifier: 6.917 s 702: circcmb3 mizar-rs: 4.648 s, verifier: 38.279 s 703: comput_1 mizar-rs: 12.197 s, verifier: 70.459 s 704: aofa_000 mizar-rs: 18.436 s, verifier: 115.374 s 705: matroid0 mizar-rs: 1.045 s, verifier: 6.905 s 706: dickson mizar-rs: 3.778 s, verifier: 26.270 s 707: polynom2 mizar-rs: 5.038 s, verifier: 33.732 s 708: polynom3 mizar-rs: 4.787 s, verifier: 31.274 s 709: bagorder mizar-rs: 5.237 s, verifier: 32.673 s 710: polynom4 mizar-rs: 1.516 s, verifier: 10.179 s 711: polynom5 mizar-rs: 5.288 s, verifier: 38.266 s 712: uproots mizar-rs: 8.555 s, verifier: 56.441 s 713: matrix_7 mizar-rs: 4.518 s, verifier: 26.244 s 714: group_9 mizar-rs: 20.828 s, verifier: 136.971 s 715: group_8 mizar-rs: 0.488 s, verifier: 2.857 s 716: uniroots mizar-rs: 9.607 s, verifier: 62.610 s 717: weddwitt mizar-rs: 4.085 s, verifier: 26.623 s 718: group_10 mizar-rs: 2.603 s, verifier: 16.308 s 719: hilbert2 mizar-rs: 1.263 s, verifier: 6.785 s 720: int_3 mizar-rs: 2.675 s, verifier: 12.095 s 721: moebius1 mizar-rs: 2.958 s, verifier: 16.429 s 722: int_4 mizar-rs: 3.189 s, verifier: 18.560 s 723: simplex0 mizar-rs: 2.800 s, verifier: 17.303 s 724: rlaffin2 mizar-rs: 4.967 s, verifier: 32.646 s 725: matrix_6 mizar-rs: 0.675 s, verifier: 3.807 s 726: matrix_9 mizar-rs: 3.710 s, verifier: 20.446 s 727: matrix11 mizar-rs: 13.917 s, verifier: 81.702 s 728: matrix10 mizar-rs: 1.143 s, verifier: 6.682 s 729: matrixr2 mizar-rs: 5.014 s, verifier: 27.886 s 730: hurwitz mizar-rs: 4.717 s, verifier: 30.991 s 731: laplace mizar-rs: 5.474 s, verifier: 32.587 s 732: vectsp10 mizar-rs: 2.403 s, verifier: 15.417 s 733: matrix13 mizar-rs: 19.295 s, verifier: 119.165 s 734: matrix15 mizar-rs: 24.216 s, verifier: 137.965 s 735: matrix_8 mizar-rs: 0.725 s, verifier: 3.690 s 736: matrixj1 mizar-rs: 9.947 s, verifier: 56.899 s 737: matrlin2 mizar-rs: 5.865 s, verifier: 36.182 s 738: topgen_2 mizar-rs: 0.515 s, verifier: 3.233 s 739: euclid_2 mizar-rs: 0.696 s, verifier: 3.565 s 740: matrix12 mizar-rs: 1.064 s, verifier: 5.697 s 741: matrix14 mizar-rs: 3.563 s, verifier: 20.166 s 742: jordan2c mizar-rs: 22.734 s, verifier: 148.807 s 743: sprect_4 mizar-rs: 3.489 s, verifier: 21.011 s 744: frechet2 mizar-rs: 1.188 s, verifier: 6.581 s 745: topreal6 mizar-rs: 4.833 s, verifier: 36.446 s 746: jgraph_3 mizar-rs: 17.896 s, verifier: 109.182 s 747: jgraph_4 mizar-rs: 12.725 s, verifier: 85.340 s 748: jgraph_5 mizar-rs: 15.318 s, verifier: 108.760 s 749: topmetr3 mizar-rs: 0.906 s, verifier: 6.073 s 750: topreal7 mizar-rs: 1.388 s, verifier: 7.962 s 751: fscirc_1 mizar-rs: 1.781 s, verifier: 10.688 s 752: urysohn2 mizar-rs: 1.012 s, verifier: 6.369 s 753: jct_misc mizar-rs: 1.316 s, verifier: 9.512 s 754: borsuk_4 mizar-rs: 2.154 s, verifier: 15.417 s 755: borsuk_5 mizar-rs: 1.030 s, verifier: 5.779 s 756: hilbert3 mizar-rs: 2.368 s, verifier: 13.486 s 757: jordan1k mizar-rs: 1.186 s, verifier: 8.153 s 758: hausdorf mizar-rs: 0.472 s, verifier: 3.136 s 759: jordan16 mizar-rs: 0.860 s, verifier: 5.671 s 760: jordan17 mizar-rs: 0.464 s, verifier: 2.357 s 761: jordan20 mizar-rs: 5.680 s, verifier: 32.435 s 762: jordan21 mizar-rs: 1.875 s, verifier: 12.196 s 763: jgraph_6 mizar-rs: 23.841 s, verifier: 188.195 s 764: jgraph_7 mizar-rs: 9.044 s, verifier: 43.150 s 765: borsuk_6 mizar-rs: 8.005 s, verifier: 63.157 s 766: urysohn3 mizar-rs: 1.294 s, verifier: 12.916 s 767: topalg_1 mizar-rs: 3.263 s, verifier: 22.632 s 768: topalg_2 mizar-rs: 1.208 s, verifier: 8.029 s 769: topalg_3 mizar-rs: 1.949 s, verifier: 13.141 s 770: topalg_4 mizar-rs: 1.446 s, verifier: 10.097 s 771: topreal9 mizar-rs: 3.098 s, verifier: 20.869 s 772: topreala mizar-rs: 1.356 s, verifier: 9.481 s 773: toprealb mizar-rs: 16.751 s, verifier: 114.644 s 774: rcomp_3 mizar-rs: 5.127 s, verifier: 31.885 s 775: topalg_5 mizar-rs: 14.701 s, verifier: 118.789 s 776: partfun4 mizar-rs: 0.374 s, verifier: 1.720 s 777: brouwer mizar-rs: 7.279 s, verifier: 58.987 s 778: tietze mizar-rs: 2.895 s, verifier: 20.859 s 779: jgraph_8 mizar-rs: 4.128 s, verifier: 27.425 s 780: jordan24 mizar-rs: 1.308 s, verifier: 8.707 s 781: jordan mizar-rs: 34.328 s, verifier: 258.982 s 782: jordan8 mizar-rs: 1.436 s, verifier: 8.994 s 783: gobrd13 mizar-rs: 5.572 s, verifier: 28.088 s 784: gobrd14 mizar-rs: 3.220 s, verifier: 21.308 s 785: lattice6 mizar-rs: 1.056 s, verifier: 6.312 s 786: waybel24 mizar-rs: 1.198 s, verifier: 7.964 s 787: yellow14 mizar-rs: 0.916 s, verifier: 5.705 s 788: topreal8 mizar-rs: 1.720 s, verifier: 11.068 s 789: jordan9 mizar-rs: 27.838 s, verifier: 166.321 s 790: jordan10 mizar-rs: 1.893 s, verifier: 11.508 s 791: waybel25 mizar-rs: 3.843 s, verifier: 33.098 s 792: conlat_2 mizar-rs: 1.786 s, verifier: 10.385 s 793: radix_1 mizar-rs: 1.067 s, verifier: 21.974 s 794: yellow16 mizar-rs: 1.174 s, verifier: 20.498 s 795: algspec1 mizar-rs: 4.405 s, verifier: 25.581 s 796: waybel26 mizar-rs: 3.947 s, verifier: 36.164 s 797: waybel27 mizar-rs: 3.509 s, verifier: 29.535 s 798: waybel28 mizar-rs: 0.409 s, verifier: 2.603 s 799: waybel29 mizar-rs: 5.721 s, verifier: 37.494 s 800: waybel30 mizar-rs: 1.930 s, verifier: 11.948 s 801: waybel31 mizar-rs: 0.854 s, verifier: 5.992 s 802: lattice7 mizar-rs: 0.423 s, verifier: 2.212 s 803: radix_2 mizar-rs: 1.349 s, verifier: 7.851 s 804: yellow17 mizar-rs: 0.298 s, verifier: 1.822 s 805: waybel32 mizar-rs: 0.675 s, verifier: 3.837 s 806: orders_4 mizar-rs: 0.554 s, verifier: 3.399 s 807: lattice8 mizar-rs: 3.991 s, verifier: 25.794 s 808: heyting3 mizar-rs: 1.183 s, verifier: 8.538 s 809: jordan1a mizar-rs: 3.249 s, verifier: 22.143 s 810: jordan1b mizar-rs: 1.320 s, verifier: 10.369 s 811: fintopo2 mizar-rs: 0.232 s, verifier: 2.521 s 812: jordan1c mizar-rs: 1.213 s, verifier: 9.245 s 813: sprect_5 mizar-rs: 0.799 s, verifier: 5.212 s 814: jordan1d mizar-rs: 2.103 s, verifier: 13.849 s 815: ideal_1 mizar-rs: 6.684 s, verifier: 44.031 s 816: hilbasis mizar-rs: 9.256 s, verifier: 82.083 s 817: polyalg1 mizar-rs: 1.073 s, verifier: 6.771 s 818: circtrm1 mizar-rs: 3.034 s, verifier: 17.300 s 819: turing_1 mizar-rs: 5.557 s, verifier: 31.990 s 820: yellow19 mizar-rs: 0.800 s, verifier: 5.205 s 821: waybel33 mizar-rs: 1.273 s, verifier: 7.847 s 822: yellow21 mizar-rs: 1.400 s, verifier: 12.383 s 823: waybel34 mizar-rs: 4.247 s, verifier: 34.012 s 824: jordan1e mizar-rs: 2.472 s, verifier: 20.113 s 825: polynom6 mizar-rs: 4.032 s, verifier: 30.050 s 826: pencil_2 mizar-rs: 1.376 s, verifier: 8.261 s 827: jordan1f mizar-rs: 1.738 s, verifier: 11.266 s 828: jordan1g mizar-rs: 15.977 s, verifier: 97.460 s 829: jordan1h mizar-rs: 33.532 s, verifier: 167.854 s 830: polynom7 mizar-rs: 2.212 s, verifier: 13.939 s 831: fsm_2 mizar-rs: 1.484 s, verifier: 8.603 s 832: jordan1i mizar-rs: 2.576 s, verifier: 15.735 s 833: facirc_2 mizar-rs: 4.807 s, verifier: 30.319 s 834: jordan1j mizar-rs: 11.569 s, verifier: 60.736 s 835: jordan11 mizar-rs: 2.903 s, verifier: 18.775 s 836: jordan12 mizar-rs: 12.103 s, verifier: 65.752 s 837: jordan13 mizar-rs: 11.150 s, verifier: 62.354 s 838: jordan14 mizar-rs: 4.851 s, verifier: 22.817 s 839: jordan15 mizar-rs: 20.768 s, verifier: 116.071 s 840: jordan18 mizar-rs: 0.954 s, verifier: 5.224 s 841: osalg_1 mizar-rs: 0.599 s, verifier: 3.374 s 842: osalg_2 mizar-rs: 1.257 s, verifier: 6.361 s 843: osalg_3 mizar-rs: 0.452 s, verifier: 2.133 s 844: osalg_4 mizar-rs: 3.568 s, verifier: 20.185 s 845: osafree mizar-rs: 7.621 s, verifier: 42.489 s 846: armstrng mizar-rs: 3.037 s, verifier: 18.277 s 847: bilinear mizar-rs: 2.055 s, verifier: 12.765 s 848: hermitan mizar-rs: 5.385 s, verifier: 37.122 s 849: necklace mizar-rs: 1.345 s, verifier: 7.732 s 850: termord mizar-rs: 1.528 s, verifier: 9.599 s 851: polyred mizar-rs: 6.473 s, verifier: 45.207 s 852: radix_3 mizar-rs: 0.858 s, verifier: 4.582 s 853: radix_4 mizar-rs: 0.908 s, verifier: 4.578 s 854: bhsp_5 mizar-rs: 0.531 s, verifier: 3.236 s 855: binari_4 mizar-rs: 1.305 s, verifier: 6.779 s 856: waybel35 mizar-rs: 0.652 s, verifier: 2.999 s 857: oposet_1 mizar-rs: 0.269 s, verifier: 1.276 s 858: bhsp_6 mizar-rs: 0.729 s, verifier: 4.117 s 859: fscirc_2 mizar-rs: 3.651 s, verifier: 23.279 s 860: graphsp mizar-rs: 3.823 s, verifier: 21.624 s 861: bhsp_7 mizar-rs: 0.437 s, verifier: 2.870 s 862: euclid_3 mizar-rs: 14.609 s, verifier: 91.443 s 863: neckla_2 mizar-rs: 0.844 s, verifier: 5.099 s 864: groeb_1 mizar-rs: 7.295 s, verifier: 52.328 s 865: groeb_2 mizar-rs: 4.644 s, verifier: 33.986 s 866: kurato_1 mizar-rs: 0.821 s, verifier: 4.669 s 867: robbins2 mizar-rs: 0.138 s, verifier: 1.266 s 868: convfun1 mizar-rs: 3.401 s, verifier: 20.068 s 869: abcmiz_0 mizar-rs: 3.543 s, verifier: 21.695 s 870: euclid_4 mizar-rs: 1.591 s, verifier: 10.736 s 871: euclid_5 mizar-rs: 0.766 s, verifier: 3.962 s 872: lfuzzy_0 mizar-rs: 0.930 s, verifier: 6.086 s 873: kurato_2 mizar-rs: 1.337 s, verifier: 9.522 s 874: jordan_a mizar-rs: 2.265 s, verifier: 15.661 s 875: jordan19 mizar-rs: 17.741 s, verifier: 145.272 s 876: radix_5 mizar-rs: 0.545 s, verifier: 2.700 s 877: radix_6 mizar-rs: 0.314 s, verifier: 1.686 s 878: lfuzzy_1 mizar-rs: 1.806 s, verifier: 12.298 s 879: roughs_1 mizar-rs: 1.286 s, verifier: 7.177 s 880: rsspace4 mizar-rs: 4.784 s, verifier: 36.731 s 881: clvect_1 mizar-rs: 2.089 s, verifier: 11.913 s 882: lopban_2 mizar-rs: 4.666 s, verifier: 28.405 s 883: cfuncdom mizar-rs: 0.663 s, verifier: 4.034 s 884: csspace mizar-rs: 2.445 s, verifier: 16.309 s 885: fintopo3 mizar-rs: 0.175 s, verifier: 0.978 s 886: lopban_3 mizar-rs: 2.705 s, verifier: 17.190 s 887: neckla_3 mizar-rs: 6.846 s, verifier: 51.293 s 888: clvect_2 mizar-rs: 0.928 s, verifier: 7.447 s 889: lopban_4 mizar-rs: 4.167 s, verifier: 13.710 s 890: csspace2 mizar-rs: 6.179 s, verifier: 32.719 s 891: csspace3 mizar-rs: 4.066 s, verifier: 21.077 s 892: clopban1 mizar-rs: 7.283 s, verifier: 48.214 s 893: csspace4 mizar-rs: 6.507 s, verifier: 41.387 s 894: clvect_3 mizar-rs: 3.641 s, verifier: 10.723 s 895: clopban2 mizar-rs: 5.303 s, verifier: 29.123 s 896: nfcont_1 mizar-rs: 3.184 s, verifier: 5.956 s 897: nfcont_2 mizar-rs: 2.725 s, verifier: 6.076 s 898: clopban3 mizar-rs: 4.323 s, verifier: 12.255 s 899: clopban4 mizar-rs: 3.578 s, verifier: 11.679 s 900: ndiff_1 mizar-rs: 5.426 s, verifier: 30.195 s 901: latsum_1 mizar-rs: 1.409 s, verifier: 1.103 s 902: nagata_1 mizar-rs: 3.528 s, verifier: 18.045 s 903: sheffer1 mizar-rs: 1.414 s, verifier: 2.544 s 904: sheffer2 mizar-rs: 0.925 s, verifier: 3.360 s 905: ndiff_2 mizar-rs: 1.880 s, verifier: 13.904 s 906: fintopo4 mizar-rs: 0.955 s, verifier: 3.360 s 907: nagata_2 mizar-rs: 6.582 s, verifier: 40.987 s 908: vfunct_2 mizar-rs: 2.389 s, verifier: 6.944 s 909: ncfcont1 mizar-rs: 4.018 s, verifier: 17.001 s 910: lp_space mizar-rs: 4.159 s, verifier: 22.079 s 911: jordan22 mizar-rs: 5.364 s, verifier: 29.496 s 912: ncfcont2 mizar-rs: 2.863 s, verifier: 11.775 s 913: pencil_3 mizar-rs: 3.120 s, verifier: 18.351 s 914: pencil_4 mizar-rs: 2.455 s, verifier: 6.473 s 915: topgen_1 mizar-rs: 1.340 s, verifier: 1.558 s 916: groeb_3 mizar-rs: 7.491 s, verifier: 38.525 s 917: topgen_3 mizar-rs: 3.495 s, verifier: 15.294 s 918: robbins3 mizar-rs: 1.569 s, verifier: 3.572 s 919: mathmorp mizar-rs: 1.027 s, verifier: 2.677 s 920: jordan23 mizar-rs: 6.745 s, verifier: 32.696 s 921: isomichi mizar-rs: 0.754 s, verifier: 2.646 s 922: euclidlp mizar-rs: 2.475 s, verifier: 12.363 s 923: fintopo5 mizar-rs: 0.967 s, verifier: 3.904 s 924: filerec1 mizar-rs: 0.998 s, verifier: 4.887 s 925: circled1 mizar-rs: 0.987 s, verifier: 5.733 s 926: topgen_4 mizar-rs: 0.577 s, verifier: 3.265 s 927: topgen_5 mizar-rs: 16.096 s, verifier: 100.783 s 928: gfacirc1 mizar-rs: 10.305 s, verifier: 57.641 s 929: ring_1 mizar-rs: 0.670 s, verifier: 5.057 s 930: real_ns1 mizar-rs: 2.576 s, verifier: 18.116 s 931: glib_001 mizar-rs: 9.561 s, verifier: 50.124 s 932: glib_002 mizar-rs: 2.427 s, verifier: 15.705 s 933: glib_003 mizar-rs: 6.407 s, verifier: 33.783 s 934: glib_004 mizar-rs: 8.417 s, verifier: 54.879 s 935: glib_005 mizar-rs: 9.951 s, verifier: 65.697 s 936: chord mizar-rs: 20.277 s, verifier: 130.984 s 937: fintopo6 mizar-rs: 1.967 s, verifier: 11.391 s 938: polynom8 mizar-rs: 1.719 s, verifier: 10.006 s 939: catalan2 mizar-rs: 10.887 s, verifier: 61.921 s 940: modelc_1 mizar-rs: 3.108 s, verifier: 16.489 s 941: lexbfs mizar-rs: 8.742 s, verifier: 53.545 s 942: integra6 mizar-rs: 3.660 s, verifier: 23.577 s 943: normsp_2 mizar-rs: 1.059 s, verifier: 6.512 s 944: bcialg_1 mizar-rs: 0.473 s, verifier: 2.873 s 945: flang_1 mizar-rs: 0.584 s, verifier: 3.446 s 946: flang_2 mizar-rs: 0.755 s, verifier: 3.990 s 947: integra7 mizar-rs: 2.151 s, verifier: 14.091 s 948: pdiff_1 mizar-rs: 5.026 s, verifier: 37.612 s 949: prvect_2 mizar-rs: 1.687 s, verifier: 11.367 s 950: entropy1 mizar-rs: 3.374 s, verifier: 19.133 s 951: rewrite2 mizar-rs: 0.526 s, verifier: 3.128 s 952: compact1 mizar-rs: 0.546 s, verifier: 3.399 s 953: bcialg_2 mizar-rs: 0.779 s, verifier: 4.267 s 954: pcs_0 mizar-rs: 2.599 s, verifier: 15.121 s 955: bcialg_3 mizar-rs: 0.204 s, verifier: 1.417 s 956: bspace mizar-rs: 1.746 s, verifier: 8.961 s 957: polyform mizar-rs: 7.561 s, verifier: 40.056 s 958: lopban_5 mizar-rs: 1.959 s, verifier: 16.205 s 959: int_5 mizar-rs: 8.993 s, verifier: 63.783 s 960: flang_3 mizar-rs: 0.490 s, verifier: 2.101 s 961: compl_sp mizar-rs: 4.116 s, verifier: 29.085 s 962: bcialg_4 mizar-rs: 0.662 s, verifier: 4.412 s 963: gfacirc2 mizar-rs: 3.593 s, verifier: 22.137 s 964: helly mizar-rs: 4.795 s, verifier: 27.045 s 965: euclid_6 mizar-rs: 6.897 s, verifier: 51.847 s 966: int_7 mizar-rs: 5.237 s, verifier: 35.321 s 967: bciideal mizar-rs: 1.951 s, verifier: 1.212 s 968: c0sp1 mizar-rs: 7.568 s, verifier: 36.654 s 969: convex4 mizar-rs: 5.966 s, verifier: 26.030 s 970: quatern2 mizar-rs: 35.796 s, verifier: 55.092 s 971: aofa_i00 mizar-rs: 15.993 s, verifier: 92.814 s 972: ramsey_1 mizar-rs: 3.033 s, verifier: 11.137 s 973: abcmiz_1 mizar-rs: 19.040 s, verifier: 104.711 s 974: modelc_2 mizar-rs: 7.597 s, verifier: 39.672 s 975: bcialg_5 mizar-rs: 0.570 s, verifier: 3.108 s 976: robbins4 mizar-rs: 1.654 s, verifier: 9.492 s 977: numeral1 mizar-rs: 3.420 s, verifier: 18.416 s 978: vectsp11 mizar-rs: 5.065 s, verifier: 32.442 s 979: matrixj2 mizar-rs: 12.328 s, verifier: 71.751 s 980: integr10 mizar-rs: 0.888 s, verifier: 5.640 s 981: pdiff_2 mizar-rs: 2.126 s, verifier: 13.974 s 982: modelc_3 mizar-rs: 8.472 s, verifier: 48.359 s 983: matrix16 mizar-rs: 1.978 s, verifier: 10.700 s 984: lpspace1 mizar-rs: 3.213 s, verifier: 18.342 s 985: bcialg_6 mizar-rs: 1.732 s, verifier: 11.068 s 986: ftacell1 mizar-rs: 23.182 s, verifier: 125.593 s 987: fdiff_11 mizar-rs: 2.387 s, verifier: 14.253 s 988: lopban_6 mizar-rs: 1.122 s, verifier: 7.144 s 989: euclid_7 mizar-rs: 11.841 s, verifier: 64.669 s 990: integra9 mizar-rs: 2.409 s, verifier: 14.078 s 991: integr11 mizar-rs: 3.708 s, verifier: 23.209 s 992: quatern3 mizar-rs: 19.570 s, verifier: 48.882 s 993: petri_2 mizar-rs: 0.717 s, verifier: 4.302 s 994: pdiff_3 mizar-rs: 1.273 s, verifier: 8.190 s 995: mesfun7c mizar-rs: 4.232 s, verifier: 27.011 s 996: nat_5 mizar-rs: 5.368 s, verifier: 29.735 s 997: random_1 mizar-rs: 3.481 s, verifier: 22.384 s 998: mesfun9c mizar-rs: 2.310 s, verifier: 14.321 s 999: metrizts mizar-rs: 3.163 s, verifier: 20.203 s 1000: gr_cy_3 mizar-rs: 0.863 s, verifier: 5.448 s 1001: cfdiff_2 mizar-rs: 4.684 s, verifier: 34.442 s 1002: measure8 mizar-rs: 3.125 s, verifier: 18.354 s 1003: rewrite3 mizar-rs: 1.150 s, verifier: 6.732 s 1004: dist_1 mizar-rs: 1.025 s, verifier: 5.202 s 1005: integr15 mizar-rs: 4.333 s, verifier: 28.998 s 1006: funct_8 mizar-rs: 2.458 s, verifier: 14.499 s 1007: fsm_3 mizar-rs: 1.175 s, verifier: 6.155 s 1008: topdim_1 mizar-rs: 2.043 s, verifier: 12.586 s 1009: group_11 mizar-rs: 0.284 s, verifier: 1.535 s 1010: topdim_2 mizar-rs: 4.610 s, verifier: 29.557 s 1011: dilworth mizar-rs: 3.509 s, verifier: 22.120 s 1012: integr1c mizar-rs: 5.905 s, verifier: 38.085 s 1013: interva1 mizar-rs: 0.741 s, verifier: 4.016 s 1014: funct_9 mizar-rs: 2.278 s, verifier: 14.107 s 1015: euclid_8 mizar-rs: 5.697 s, verifier: 31.652 s 1016: c0sp2 mizar-rs: 5.275 s, verifier: 40.842 s 1017: algstr_4 mizar-rs: 4.822 s, verifier: 25.848 s 1018: pdiff_4 mizar-rs: 4.834 s, verifier: 31.733 s 1019: poset_1 mizar-rs: 1.221 s, verifier: 5.219 s 1020: grnilp_1 mizar-rs: 1.985 s, verifier: 12.713 s 1021: abcmiz_a mizar-rs: 10.632 s, verifier: 49.805 s 1022: fib_num4 mizar-rs: 1.415 s, verifier: 13.847 s 1023: euclid_9 mizar-rs: 5.144 s, verifier: 23.671 s 1024: pdiff_5 mizar-rs: 6.509 s, verifier: 21.572 s 1025: lpspace2 mizar-rs: 16.726 s, verifier: 99.481 s 1026: tops_4 mizar-rs: 3.523 s, verifier: 5.716 s 1027: toprealc mizar-rs: 13.164 s, verifier: 75.355 s 1028: simplex1 mizar-rs: 10.703 s, verifier: 52.846 s 1029: cardfin2 mizar-rs: 3.156 s, verifier: 9.617 s 1030: integr16 mizar-rs: 3.012 s, verifier: 19.319 s 1031: pdiff_6 mizar-rs: 6.099 s, verifier: 36.654 s 1032: random_2 mizar-rs: 5.189 s, verifier: 30.401 s 1033: pdiff_7 mizar-rs: 20.384 s, verifier: 139.736 s 1034: groupp_1 mizar-rs: 0.967 s, verifier: 4.015 s 1035: integr18 mizar-rs: 1.200 s, verifier: 6.036 s 1036: group_12 mizar-rs: 1.085 s, verifier: 5.738 s 1037: mycielsk mizar-rs: 2.663 s, verifier: 14.358 s 1038: nfcont_3 mizar-rs: 1.417 s, verifier: 7.926 s 1039: prvect_3 mizar-rs: 8.599 s, verifier: 54.206 s 1040: rlvect_x mizar-rs: 1.380 s, verifier: 7.589 s 1041: pdiff_8 mizar-rs: 3.698 s, verifier: 22.865 s 1042: ndiff_3 mizar-rs: 2.948 s, verifier: 18.645 s 1043: cgames_1 mizar-rs: 0.749 s, verifier: 4.378 s 1044: exchsort mizar-rs: 6.553 s, verifier: 39.204 s 1045: matrtop1 mizar-rs: 18.598 s, verifier: 125.067 s 1046: matrtop2 mizar-rs: 13.581 s, verifier: 80.242 s 1047: ltlaxio1 mizar-rs: 2.753 s, verifier: 15.571 s 1048: cc0sp1 mizar-rs: 4.253 s, verifier: 32.130 s 1049: mazurulm mizar-rs: 1.863 s, verifier: 12.892 s 1050: ec_pf_1 mizar-rs: 9.995 s, verifier: 46.891 s 1051: rlaffin3 mizar-rs: 12.452 s, verifier: 77.013 s 1052: simplex2 mizar-rs: 9.699 s, verifier: 73.557 s 1053: brouwer2 mizar-rs: 8.522 s, verifier: 57.854 s 1054: fomodel0 mizar-rs: 54.087 s, verifier: 225.657 s 1055: fomodel1 mizar-rs: 7.017 s, verifier: 35.599 s 1056: fomodel2 mizar-rs: 22.380 s, verifier: 123.495 s 1057: fomodel3 mizar-rs: 48.384 s, verifier: 303.112 s 1058: fomodel4 mizar-rs: 32.011 s, verifier: 209.714 s 1059: cayley mizar-rs: 0.472 s, verifier: 2.301 s 1060: nfcont_4 mizar-rs: 2.106 s, verifier: 12.430 s 1061: stacks_1 mizar-rs: 3.338 s, verifier: 17.274 s 1062: finance1 mizar-rs: 0.849 s, verifier: 6.212 s 1063: fvaluat1 mizar-rs: 3.628 s, verifier: 23.933 s 1064: cc0sp2 mizar-rs: 5.131 s, verifier: 41.787 s 1065: matrtop3 mizar-rs: 18.067 s, verifier: 111.667 s 1066: ndiff_5 mizar-rs: 17.762 s, verifier: 146.060 s 1067: zmodul01 mizar-rs: 4.599 s, verifier: 29.436 s 1068: morph_01 mizar-rs: 0.376 s, verifier: 2.534 s 1069: ndiff_4 mizar-rs: 6.122 s, verifier: 43.971 s 1070: matrix17 mizar-rs: 0.895 s, verifier: 5.128 s 1071: integr19 mizar-rs: 6.187 s, verifier: 42.115 s 1072: ec_pf_2 mizar-rs: 6.869 s, verifier: 44.496 s 1073: pdiff_9 mizar-rs: 10.411 s, verifier: 77.476 s 1074: mmlquery mizar-rs: 1.056 s, verifier: 4.810 s 1075: menelaus mizar-rs: 2.656 s, verifier: 24.858 s 1076: scmyciel mizar-rs: 4.939 s, verifier: 25.724 s 1077: ratfunc1 mizar-rs: 3.455 s, verifier: 20.979 s 1078: goedcpuc mizar-rs: 0.973 s, verifier: 5.006 s 1079: zmodul02 mizar-rs: 1.850 s, verifier: 11.316 s 1080: ltlaxio2 mizar-rs: 3.705 s, verifier: 20.613 s 1081: ltlaxio3 mizar-rs: 2.852 s, verifier: 15.898 s 1082: ltlaxio4 mizar-rs: 4.156 s, verifier: 24.130 s 1083: friends1 mizar-rs: 2.756 s, verifier: 14.402 s 1084: msafree4 mizar-rs: 28.848 s, verifier: 183.242 s 1085: dist_2 mizar-rs: 3.479 s, verifier: 20.793 s 1086: int_8 mizar-rs: 4.048 s, verifier: 20.795 s 1087: lopban_7 mizar-rs: 1.365 s, verifier: 9.767 s 1088: zmodul03 mizar-rs: 7.601 s, verifier: 43.468 s 1089: cayldick mizar-rs: 13.960 s, verifier: 98.461 s 1090: ordeq_01 mizar-rs: 8.729 s, verifier: 85.674 s 1091: altcat_5 mizar-rs: 0.392 s, verifier: 1.908 s 1092: tietze_2 mizar-rs: 22.271 s, verifier: 144.898 s 1093: brouwer3 mizar-rs: 72.277 s, verifier: 622.924 s 1094: mfold_0 mizar-rs: 11.998 s, verifier: 75.245 s 1095: mfold_1 mizar-rs: 5.562 s, verifier: 38.699 s 1096: mfold_2 mizar-rs: 13.160 s, verifier: 70.306 s 1097: topalg_6 mizar-rs: 16.143 s, verifier: 127.205 s 1098: borsuk_7 mizar-rs: 10.804 s, verifier: 95.708 s 1099: aofa_a00 mizar-rs: 29.983 s, verifier: 180.700 s 1100: group_14 mizar-rs: 5.927 s, verifier: 34.905 s 1101: lpspacc1 mizar-rs: 4.718 s, verifier: 27.265 s 1102: aofa_a01 mizar-rs: 42.306 s, verifier: 328.748 s 1103: ckspace1 mizar-rs: 2.058 s, verifier: 13.161 s 1104: random_3 mizar-rs: 1.831 s, verifier: 10.540 s 1105: mmlquer2 mizar-rs: 1.736 s, verifier: 9.719 s 1106: hurwitz2 mizar-rs: 2.511 s, verifier: 17.044 s 1107: roughs_2 mizar-rs: 0.611 s, verifier: 3.696 s 1108: group_17 mizar-rs: 4.336 s, verifier: 29.705 s 1109: nbvectsp mizar-rs: 1.575 s, verifier: 9.626 s 1110: topgen_6 mizar-rs: 1.043 s, verifier: 9.909 s 1111: numeral2 mizar-rs: 3.259 s, verifier: 25.177 s 1112: ndiff_6 mizar-rs: 0.962 s, verifier: 7.576 s 1113: numpoly1 mizar-rs: 1.821 s, verifier: 16.919 s 1114: gaussint mizar-rs: 5.325 s, verifier: 38.901 s 1115: topalg_7 mizar-rs: 0.900 s, verifier: 6.687 s 1116: huffman1 mizar-rs: 4.295 s, verifier: 25.903 s 1117: integr20 mizar-rs: 4.520 s, verifier: 31.800 s 1118: moebius2 mizar-rs: 3.975 s, verifier: 29.244 s 1119: dblseq_1 mizar-rs: 2.218 s, verifier: 16.806 s 1120: aescip_1 mizar-rs: 3.886 s, verifier: 28.217 s 1121: integr21 mizar-rs: 3.436 s, verifier: 23.958 s 1122: cat_6 mizar-rs: 2.727 s, verifier: 18.352 s 1123: group_18 mizar-rs: 2.935 s, verifier: 23.244 s 1124: latticea mizar-rs: 0.631 s, verifier: 4.399 s 1125: prefer_1 mizar-rs: 1.288 s, verifier: 7.606 s 1126: compos_0 mizar-rs: 0.878 s, verifier: 7.512 s 1127: compos_1 mizar-rs: 4.545 s, verifier: 29.160 s 1128: scm_inst mizar-rs: 1.298 s, verifier: 5.369 s 1129: ami_2 mizar-rs: 0.615 s, verifier: 3.746 s 1130: memstr_0 mizar-rs: 1.284 s, verifier: 9.326 s 1131: extpro_1 mizar-rs: 0.805 s, verifier: 6.874 s 1132: ami_3 mizar-rs: 1.666 s, verifier: 10.502 s 1133: scmfsa_i mizar-rs: 0.348 s, verifier: 3.288 s 1134: scmringi mizar-rs: 0.866 s, verifier: 5.696 s 1135: scmfsa_1 mizar-rs: 0.820 s, verifier: 5.306 s 1136: scmpds_i mizar-rs: 0.686 s, verifier: 3.774 s 1137: scmpds_1 mizar-rs: 0.124 s, verifier: 0.910 s 1138: scmring1 mizar-rs: 0.397 s, verifier: 2.677 s 1139: amistd_1 mizar-rs: 2.514 s, verifier: 19.290 s 1140: amistd_2 mizar-rs: 0.588 s, verifier: 5.534 s 1141: amistd_4 mizar-rs: 0.224 s, verifier: 2.026 s 1142: compos_2 mizar-rs: 1.459 s, verifier: 8.917 s 1143: amistd_3 mizar-rs: 1.079 s, verifier: 7.110 s 1144: amistd_5 mizar-rs: 1.294 s, verifier: 9.019 s 1145: scm_1 mizar-rs: 0.967 s, verifier: 6.428 s 1146: fib_fusc mizar-rs: 1.225 s, verifier: 8.235 s 1147: scm_comp mizar-rs: 1.622 s, verifier: 11.582 s 1148: ami_4 mizar-rs: 1.285 s, verifier: 7.948 s 1149: ami_5 mizar-rs: 1.922 s, verifier: 11.500 s 1150: ami_6 mizar-rs: 3.100 s, verifier: 19.667 s 1151: reloc mizar-rs: 1.884 s, verifier: 12.431 s 1152: scmfsa_2 mizar-rs: 16.356 s, verifier: 47.260 s 1153: scmfsa_3 mizar-rs: 1.533 s, verifier: 8.909 s 1154: scmfsa10 mizar-rs: 4.813 s, verifier: 31.703 s 1155: scmfsa_4 mizar-rs: 0.808 s, verifier: 5.642 s 1156: scmfsa_5 mizar-rs: 1.794 s, verifier: 11.034 s 1157: scmfsa_7 mizar-rs: 2.703 s, verifier: 17.025 s 1158: scmfsa_m mizar-rs: 2.855 s, verifier: 16.001 s 1159: scmfsa6a mizar-rs: 1.574 s, verifier: 10.349 s 1160: sf_mastr mizar-rs: 4.045 s, verifier: 33.427 s 1161: scmfsa6b mizar-rs: 1.905 s, verifier: 12.622 s 1162: scmfsa6c mizar-rs: 2.099 s, verifier: 12.944 s 1163: scmfsa7b mizar-rs: 2.782 s, verifier: 19.642 s 1164: scmfsa8a mizar-rs: 2.877 s, verifier: 18.411 s 1165: scmfsa_x mizar-rs: 4.169 s, verifier: 26.961 s 1166: scmfsa8b mizar-rs: 5.091 s, verifier: 33.730 s 1167: scmfsa8c mizar-rs: 10.181 s, verifier: 64.239 s 1168: scmfsa_9 mizar-rs: 3.604 s, verifier: 25.940 s 1169: sfmastr1 mizar-rs: 1.795 s, verifier: 11.581 s 1170: scmfsa9a mizar-rs: 11.521 s, verifier: 68.810 s 1171: sfmastr2 mizar-rs: 1.531 s, verifier: 10.275 s 1172: sfmastr3 mizar-rs: 14.415 s, verifier: 89.275 s 1173: scm_halt mizar-rs: 5.869 s, verifier: 38.837 s 1174: scmbsort mizar-rs: 11.003 s, verifier: 75.864 s 1175: scmisort mizar-rs: 10.260 s, verifier: 70.726 s 1176: scmring2 mizar-rs: 0.933 s, verifier: 5.297 s 1177: scmring3 mizar-rs: 10.960 s, verifier: 69.794 s 1178: scmring4 mizar-rs: 2.170 s, verifier: 15.411 s 1179: scmpds_2 mizar-rs: 2.689 s, verifier: 19.437 s 1180: scmpds_3 mizar-rs: 1.095 s, verifier: 7.329 s 1181: scmpds_4 mizar-rs: 2.373 s, verifier: 16.273 s 1182: scmpds_5 mizar-rs: 2.377 s, verifier: 14.247 s 1183: scmpds_6 mizar-rs: 9.578 s, verifier: 59.445 s 1184: scmp_gcd mizar-rs: 2.896 s, verifier: 16.644 s 1185: scmpds_7 mizar-rs: 7.896 s, verifier: 53.469 s 1186: scmpds_8 mizar-rs: 4.125 s, verifier: 32.933 s 1187: scpisort mizar-rs: 6.350 s, verifier: 46.553 s 1188: scpqsort mizar-rs: 22.358 s, verifier: 166.543 s 1189: scpinvar mizar-rs: 5.425 s, verifier: 39.949 s 1190: ami_wstd mizar-rs: 1.803 s, verifier: 14.369 s 1191: scmpds_9 mizar-rs: 1.343 s, verifier: 8.406 s 1192: altcat_6 mizar-rs: 0.284 s, verifier: 2.013 s 1193: petri_3 mizar-rs: 1.207 s, verifier: 8.504 s 1194: ndiff_7 mizar-rs: 7.739 s, verifier: 82.064 s 1195: ordeq_02 mizar-rs: 5.899 s, verifier: 56.699 s 1196: zmodul04 mizar-rs: 13.138 s, verifier: 87.430 s 1197: poset_2 mizar-rs: 4.163 s, verifier: 29.754 s 1198: petri_df mizar-rs: 2.498 s, verifier: 15.232 s 1199: absred_0 mizar-rs: 1.380 s, verifier: 10.188 s 1200: dblseq_2 mizar-rs: 3.827 s, verifier: 29.098 s 1201: dualsp01 mizar-rs: 12.366 s, verifier: 106.662 s 1202: srings_1 mizar-rs: 4.350 s, verifier: 25.877 s 1203: srings_2 mizar-rs: 8.601 s, verifier: 34.079 s 1204: roughs_4 mizar-rs: 0.767 s, verifier: 4.639 s 1205: hilbert4 mizar-rs: 3.343 s, verifier: 13.957 s 1206: lagra4sq mizar-rs: 1.893 s, verifier: 13.626 s 1207: nat_6 mizar-rs: 1.491 s, verifier: 8.623 s 1208: ballot_1 mizar-rs: 12.566 s, verifier: 34.607 s 1209: msafree5 mizar-rs: 38.850 s, verifier: 290.298 s 1210: rvsum_3 mizar-rs: 1.954 s, verifier: 11.737 s 1211: gtarski1 mizar-rs: 0.406 s, verifier: 2.292 s 1212: graph_3a mizar-rs: 3.732 s, verifier: 16.962 s 1213: zmodul05 mizar-rs: 8.205 s, verifier: 53.178 s 1214: finance2 mizar-rs: 3.458 s, verifier: 24.909 s 1215: newton01 mizar-rs: 0.885 s, verifier: 5.177 s 1216: normsp_3 mizar-rs: 5.557 s, verifier: 43.118 s 1217: aofa_l00 mizar-rs: 123.706 s, verifier: 451.123 s 1218: lattad_1 mizar-rs: 0.853 s, verifier: 5.947 s 1219: vsdiff_1 mizar-rs: 1.291 s, verifier: 9.970 s 1220: zmodul06 mizar-rs: 17.676 s, verifier: 129.890 s 1221: ring_2 mizar-rs: 7.817 s, verifier: 59.859 s 1222: dualsp02 mizar-rs: 14.006 s, verifier: 106.575 s 1223: euclid10 mizar-rs: 1.523 s, verifier: 12.885 s 1224: fuznum_1 mizar-rs: 1.419 s, verifier: 9.925 s 1225: cat_7 mizar-rs: 3.815 s, verifier: 27.323 s 1226: group_19 mizar-rs: 2.536 s, verifier: 18.438 s 1227: zmatrlin mizar-rs: 18.401 s, verifier: 117.983 s 1228: srings_3 mizar-rs: 3.154 s, verifier: 20.428 s 1229: normsp_4 mizar-rs: 2.634 s, verifier: 18.263 s 1230: group_20 mizar-rs: 1.997 s, verifier: 14.289 s 1231: euclid11 mizar-rs: 0.716 s, verifier: 7.589 s 1232: flexary1 mizar-rs: 24.948 s, verifier: 169.127 s 1233: eulrpart mizar-rs: 16.698 s, verifier: 114.768 s 1234: diophan1 mizar-rs: 2.101 s, verifier: 15.310 s 1235: srings_4 mizar-rs: 2.794 s, verifier: 18.688 s 1236: nelson_1 mizar-rs: 0.668 s, verifier: 4.456 s 1237: group_1a mizar-rs: 7.778 s, verifier: 50.732 s 1238: polnot_1 mizar-rs: 2.605 s, verifier: 13.714 s 1239: grzlog_1 mizar-rs: 0.976 s, verifier: 5.633 s 1240: cardfil2 mizar-rs: 2.376 s, verifier: 15.297 s 1241: asympt_2 mizar-rs: 1.665 s, verifier: 10.847 s 1242: newton02 mizar-rs: 2.737 s, verifier: 17.281 s 1243: dualsp03 mizar-rs: 8.196 s, verifier: 79.422 s 1244: dualsp04 mizar-rs: 3.526 s, verifier: 30.832 s 1245: dblseq_3 mizar-rs: 5.352 s, verifier: 35.984 s 1246: cardfil3 mizar-rs: 1.378 s, verifier: 8.848 s 1247: fintopo7 mizar-rs: 0.971 s, verifier: 6.214 s 1248: zmodul07 mizar-rs: 9.797 s, verifier: 63.847 s 1249: measure9 mizar-rs: 12.621 s, verifier: 79.454 s 1250: peterson mizar-rs: 0.694 s, verifier: 3.444 s 1251: ring_3 mizar-rs: 31.939 s, verifier: 197.338 s 1252: cat_8 mizar-rs: 3.471 s, verifier: 24.130 s 1253: asympt_3 mizar-rs: 4.005 s, verifier: 31.126 s 1254: ltlaxio5 mizar-rs: 0.959 s, verifier: 7.519 s 1255: latstone mizar-rs: 0.886 s, verifier: 6.042 s 1256: finance3 mizar-rs: 3.601 s, verifier: 24.219 s 1257: euclid12 mizar-rs: 3.597 s, verifier: 22.437 s 1258: euclid13 mizar-rs: 3.874 s, verifier: 26.185 s 1259: zmodul08 mizar-rs: 7.980 s, verifier: 43.745 s 1260: zmodlat1 mizar-rs: 24.845 s, verifier: 168.249 s 1261: measur10 mizar-rs: 36.575 s, verifier: 228.470 s 1262: group_21 mizar-rs: 6.996 s, verifier: 45.877 s 1263: bagord_2 mizar-rs: 5.160 s, verifier: 36.222 s 1264: cousin mizar-rs: 6.832 s, verifier: 51.761 s 1265: srings_5 mizar-rs: 8.196 s, verifier: 54.052 s 1266: roughs_3 mizar-rs: 1.027 s, verifier: 5.545 s 1267: gtarski2 mizar-rs: 4.097 s, verifier: 26.492 s 1268: topmetr4 mizar-rs: 1.572 s, verifier: 8.226 s 1269: cardfil4 mizar-rs: 4.194 s, verifier: 26.195 s 1270: newton03 mizar-rs: 1.321 s, verifier: 7.737 s 1271: integr22 mizar-rs: 3.347 s, verifier: 23.023 s 1272: uniform2 mizar-rs: 0.958 s, verifier: 5.584 s 1273: uniform3 mizar-rs: 2.147 s, verifier: 14.469 s 1274: ring_4 mizar-rs: 22.860 s, verifier: 180.416 s 1275: anproj_8 mizar-rs: 12.386 s, verifier: 77.166 s 1276: integr23 mizar-rs: 15.708 s, verifier: 98.122 s 1277: newton04 mizar-rs: 6.911 s, verifier: 47.868 s 1278: leibniz1 mizar-rs: 5.746 s, verifier: 637.738 s 1279: pl_axiom mizar-rs: 2.573 s, verifier: 18.432 s 1280: algnum_1 mizar-rs: 9.586 s, verifier: 69.293 s 1281: niven mizar-rs: 3.840 s, verifier: 26.407 s 1282: measur11 mizar-rs: 19.297 s, verifier: 133.196 s 1283: polydiff mizar-rs: 3.078 s, verifier: 24.472 s 1284: liouvil1 mizar-rs: 2.808 s, verifier: 19.932 s 1285: liouvil2 mizar-rs: 3.192 s, verifier: 23.714 s 1286: anproj_9 mizar-rs: 14.220 s, verifier: 59.617 s 1287: realalg1 mizar-rs: 9.427 s, verifier: 61.085 s 1288: zmodlat2 mizar-rs: 41.387 s, verifier: 256.749 s 1289: polyvie1 mizar-rs: 2.637 s, verifier: 18.955 s 1290: fuznorm1 mizar-rs: 0.966 s, verifier: 5.753 s 1291: finance4 mizar-rs: 0.802 s, verifier: 4.823 s 1292: pascal mizar-rs: 10.639 s, verifier: 60.907 s 1293: orders_5 mizar-rs: 6.245 s, verifier: 42.739 s 1294: basel_1 mizar-rs: 2.661 s, verifier: 17.435 s 1295: basel_2 mizar-rs: 4.203 s, verifier: 31.321 s 1296: zmodlat3 mizar-rs: 39.323 s, verifier: 237.764 s 1297: vectsp12 mizar-rs: 5.804 s, verifier: 39.728 s 1298: dualsp05 mizar-rs: 21.310 s, verifier: 181.723 s 1299: ring_5 mizar-rs: 6.367 s, verifier: 47.316 s 1300: pells_eq mizar-rs: 1.830 s, verifier: 13.242 s 1301: nomin_1 mizar-rs: 1.008 s, verifier: 6.464 s 1302: cousin2 mizar-rs: 3.334 s, verifier: 22.458 s 1303: mesfun11 mizar-rs: 2.604 s, verifier: 16.714 s 1304: fuzimpl1 mizar-rs: 0.672 s, verifier: 8.028 s 1305: realalg2 mizar-rs: 4.737 s, verifier: 36.271 s 1306: finance5 mizar-rs: 2.249 s, verifier: 13.776 s 1307: ndiff_8 mizar-rs: 5.766 s, verifier: 48.436 s 1308: diophan2 mizar-rs: 2.730 s, verifier: 18.530 s 1309: gtarski3 mizar-rs: 4.066 s, verifier: 10.213 s 1310: hilb10_1 mizar-rs: 6.456 s, verifier: 38.939 s 1311: finance6 mizar-rs: 2.653 s, verifier: 18.868 s 1312: partpr_1 mizar-rs: 1.238 s, verifier: 7.193 s 1313: bkmodel1 mizar-rs: 82.488 s, verifier: 219.037 s 1314: bkmodel2 mizar-rs: 21.801 s, verifier: 146.810 s 1315: mesfun12 mizar-rs: 18.483 s, verifier: 126.260 s 1316: moebius3 mizar-rs: 3.629 s, verifier: 25.435 s 1317: hilb10_2 mizar-rs: 6.638 s, verifier: 39.238 s 1318: newton05 mizar-rs: 1.412 s, verifier: 7.826 s 1319: glib_006 mizar-rs: 5.467 s, verifier: 26.211 s 1320: glib_007 mizar-rs: 5.916 s, verifier: 33.435 s 1321: partpr_2 mizar-rs: 0.350 s, verifier: 2.118 s 1322: nomin_2 mizar-rs: 0.991 s, verifier: 6.518 s 1323: nomin_3 mizar-rs: 0.490 s, verifier: 2.887 s 1324: nomin_4 mizar-rs: 0.719 s, verifier: 3.885 s 1325: hilb10_3 mizar-rs: 12.078 s, verifier: 80.878 s 1326: roughs_5 mizar-rs: 0.533 s, verifier: 3.017 s 1327: robbins5 mizar-rs: 0.181 s, verifier: 1.171 s 1328: finseq_9 mizar-rs: 3.164 s, verifier: 20.074 s 1329: tops_5 mizar-rs: 3.492 s, verifier: 21.767 s 1330: binari_6 mizar-rs: 1.674 s, verifier: 9.823 s 1331: lopban_8 mizar-rs: 2.970 s, verifier: 23.527 s 1332: music_s1 mizar-rs: 2.797 s, verifier: 41.742 s 1333: fuzimpl2 mizar-rs: 0.948 s, verifier: 5.845 s 1334: topzari1 mizar-rs: 1.223 s, verifier: 7.884 s 1335: rvsum_4 mizar-rs: 10.044 s, verifier: 67.109 s 1336: lopban_9 mizar-rs: 14.559 s, verifier: 132.324 s 1337: pdiffeq1 mizar-rs: 2.129 s, verifier: 15.024 s 1338: lopban10 mizar-rs: 8.103 s, verifier: 60.520 s 1339: anproj10 mizar-rs: 3.505 s, verifier: 24.485 s 1340: lopban11 mizar-rs: 4.287 s, verifier: 40.081 s 1341: mesfun13 mizar-rs: 3.091 s, verifier: 18.057 s 1342: gtarski4 mizar-rs: 1.256 s, verifier: 3.830 s 1343: ntalgo_2 mizar-rs: 1.483 s, verifier: 10.117 s 1344: field_1 mizar-rs: 5.544 s, verifier: 37.985 s 1345: lopban12 mizar-rs: 4.336 s, verifier: 35.620 s 1346: lopban13 mizar-rs: 6.403 s, verifier: 52.500 s 1347: ndiff_9 mizar-rs: 9.580 s, verifier: 71.871 s 1348: field_2 mizar-rs: 4.943 s, verifier: 40.186 s 1349: ordinal7 mizar-rs: 7.618 s, verifier: 45.273 s 1350: glib_008 mizar-rs: 7.631 s, verifier: 47.985 s 1351: nomin_5 mizar-rs: 0.342 s, verifier: 2.109 s 1352: nomin_6 mizar-rs: 0.384 s, verifier: 2.312 s 1353: hilb10_4 mizar-rs: 10.818 s, verifier: 67.844 s 1354: hilb10_5 mizar-rs: 32.486 s, verifier: 198.619 s 1355: field_3 mizar-rs: 28.386 s, verifier: 177.520 s 1356: field_4 mizar-rs: 11.521 s, verifier: 74.317 s 1357: glib_009 mizar-rs: 5.272 s, verifier: 31.626 s 1358: glib_010 mizar-rs: 12.290 s, verifier: 79.018 s 1359: glib_011 mizar-rs: 3.021 s, verifier: 15.924 s 1360: ec_pf_3 mizar-rs: 7.131 s, verifier: 48.042 s 1361: aimloop mizar-rs: 3.987 s, verifier: 32.948 s 1362: roughif1 mizar-rs: 1.474 s, verifier: 9.228 s 1363: bkmodel3 mizar-rs: 2.618 s, verifier: 21.245 s 1364: bkmodel4 mizar-rs: 41.176 s, verifier: 131.903 s 1365: glibpre0 mizar-rs: 11.132 s, verifier: 53.565 s 1366: glib_012 mizar-rs: 11.061 s, verifier: 77.163 s 1367: wallace1 mizar-rs: 78.498 s, verifier: 442.306 s 1368: ringfrac mizar-rs: 3.583 s, verifier: 27.712 s 1369: prsubset mizar-rs: 0.645 s, verifier: 3.705 s 1370: measur12 mizar-rs: 11.740 s, verifier: 78.534 s 1371: roughif2 mizar-rs: 2.659 s, verifier: 16.809 s 1372: number01 mizar-rs: 1.100 s, verifier: 8.988 s 1373: fuzimpl3 mizar-rs: 1.631 s, verifier: 13.255 s 1374: field_5 mizar-rs: 29.239 s, verifier: 183.522 s 1375: glib_013 mizar-rs: 5.833 s, verifier: 37.539 s 1376: glib_014 mizar-rs: 2.724 s, verifier: 15.259 s 1377: glunir00 mizar-rs: 4.749 s, verifier: 30.504 s 1378: nomin_7 mizar-rs: 1.472 s, verifier: 8.954 s 1379: complex3 mizar-rs: 1.946 s, verifier: 13.503 s 1380: classes3 mizar-rs: 0.468 s, verifier: 2.788 s 1381: latquasi mizar-rs: 2.562 s, verifier: 17.713 s 1382: fintopo8 mizar-rs: 1.679 s, verifier: 11.866 s 1383: counters mizar-rs: 2.404 s, verifier: 16.518 s 1384: field_6 mizar-rs: 21.576 s, verifier: 164.665 s 1385: seqfunc2 mizar-rs: 0.606 s, verifier: 3.338 s 1386: nomin_8 mizar-rs: 1.109 s, verifier: 7.945 s 1387: nomin_9 mizar-rs: 3.485 s, verifier: 24.145 s 1388: ringder1 mizar-rs: 4.675 s, verifier: 34.873 s 1389: ndiff10 mizar-rs: 14.865 s, verifier: 67.882 s 1390: glibpre1 mizar-rs: 20.855 s, verifier: 124.468 s 1391: field_7 mizar-rs: 30.645 s, verifier: 220.829 s 1392: c0sp3 mizar-rs: 4.256 s, verifier: 31.200 s 1393: number02 mizar-rs: 11.121 s, verifier: 87.688 s 1394: pappus mizar-rs: 9.396 s, verifier: 52.158 s 1395: latwal_1 mizar-rs: 2.228 s, verifier: 16.596 s 1396: ascoli mizar-rs: 6.805 s, verifier: 47.555 s 1397: ideal_2 mizar-rs: 2.952 s, verifier: 34.560 s 1398: fuzzy_5 mizar-rs: 2.846 s, verifier: 19.727 s 1399: real_ns2 mizar-rs: 4.619 s, verifier: 32.880 s 1400: field_8 mizar-rs: 17.437 s, verifier: 135.568 s 1401: binpack1 mizar-rs: 6.138 s, verifier: 40.089 s 1402: lattba_1 mizar-rs: 3.568 s, verifier: 34.254 s 1403: anproj11 mizar-rs: 10.106 s, verifier: 73.040 s 1404: real_ns3 mizar-rs: 4.768 s, verifier: 36.179 s 1405: mesfun14 mizar-rs: 9.908 s, verifier: 65.556 s 1406: integr24 mizar-rs: 17.168 s, verifier: 112.458 s 1407: hilb10_6 mizar-rs: 8.766 s, verifier: 64.120 s 1408: field_9 mizar-rs: 28.644 s, verifier: 187.913 s 1409: prvect_4 mizar-rs: 2.298 s, verifier: 14.494 s 1410: glib_015 mizar-rs: 12.777 s, verifier: 66.163 s 1411: integr25 mizar-rs: 6.015 s, verifier: 41.840 s ```

I will link to this post from the README for people interested in a more detailed performance comparison.