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 12ef451.

   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.