Fwd: [dev-forum] Re: Urelements?
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
----- Przekazana wiadomość od [email protected] ----- Data: Mon, 12 Mar 2012 11:41:44 +0100 (CET) Od: Artur Kornilowicz <[email protected]> Odpowiedz-Do:[email protected] Temat: [dev-forum] Re: Urelements? Do: Developer-Forum <[email protected]> Just to present some results. The columns are: article time_without_expansions time_with_exp difference_in_seconds They are sorted wrt 4th column. nat_4 1:18 27:17 1559 menelaus 0:36 10:48 612 sf_mastr 0:49 8:44 475 abcmiz_1 1:47 7:20 333 jordan9 1:07 6:29 322 jordan13 1:05 6:15 310 euclid_6 0:56 6:01 305 enumset1 0:01 4:39 278 euclid_3 0:14 4:45 271 fomodel3 2:31 6:42 251 convex4 0:28 4:38 250 jordan 3:29 7:32 243 matrix_9 1:28 5:26 238 nat_1 0:02 3:54 232 topgen_5 1:11 4:17 186 scpqsort 3:59 7:05 186 borsuk_5 0:05 3:09 184 scmbsort 1:50 4:50 180 borsuk_7 1:37 4:30 173 aofa_i00 1:36 4:28 172 circuit1 0:35 3:19 164 jordan1h 0:56 3:22 146 fomodel2 1:25 3:38 133 matrix15 1:23 3:30 127 fomodel0 0:35 2:42 127 cqc_the1 0:05 2:01 116 gfacirc1 1:08 3:03 115 abcmiz_a 0:29 2:22 113 jgraph_1 0:60 2:50 110 calcul_1 0:22 2:04 102 matrix13 1:47 3:15 88 scmfsa_i 0:02 1:29 87 goboard9 0:52 2:16 84 scmpds_4 0:13 1:34 81 uniroots 1:26 2:46 80 jgraph_5 1:10 2:29 79 anproj_2 0:06 1:25 79 graph_2 1:22 2:36 74 jgraph_6 2:09 3:22 73 jgraph_3 1:18 2:31 73 group_10 0:27 1:39 72 chord 1:19 2:31 72 matrtop1 1:02 2:12 70 zfmodel2 0:11 1:19 68 scmfsa6a 0:12 1:20 68 convex1 0:09 1:13 64 scmring3 0:19 1:21 62 jordan12 0:19 1:20 61 pre_poly 0:35 1:33 58 facirc_1 0:50 1:45 55 fomodel4 3:01 3:54 53 facirc_2 0:40 1:32 52 goboard5 0:15 1:06 51 jordan2c 2:17 3:07 50 sin_cos 0:49 1:37 48 amistd_5 0:28 1:16 48 pdiff_7 1:25 2:11 46 neckla_3 0:35 1:21 46 scmfsa_2 1:27 2:12 45 toprealb 1:15 1:59 44 toprealc 0:59 1:42 43 matrix11 1:41 2:24 43 hermitan 0:25 1:08 43 modal_1 0:22 1:03 41 matrixj2 1:50 2:30 40 exchsort 0:24 1:04 40 cohsp_1 0:35 1:15 40 topalg_5 1:09 1:48 39 scm_inst 0:05 0:44 39 sprect_1 0:40 1:18 38 seq_4 0:47 1:25 38 scm_comp 0:10 0:48 38 euclid_7 2:04 2:42 38 scm_halt 0:57 1:34 37 lpspace2 1:14 1:51 37 jordan19 1:38 2:15 37 fscirc_2 0:30 1:07 37 topalg_6 1:22 1:58 36 sprect_2 1:07 1:43 36 rlvect_2 0:22 0:57 35 necklace 0:08 0:43 35 moebius1 0:31 1:04 33 jordan7 0:38 1:11 33 int_4 0:35 1:08 33 group_9 4:28 5:01 33 matrtop2 0:54 1:26 32 jordan1g 1:15 1:47 32 diff_4 0:43 1:15 32 rlaffin3 0:58 1:29 31 msualg_9 0:26 0:57 31 jordan15 1:36 2:07 31 descip_1 6:23 6:54 31 mesfunc5 1:16 1:46 30 funct_7 0:16 0:46 30 catalan2 0:53 1:23 30 graph_3 1:50 2:18 28 revrot_1 0:20 0:47 27 holder_1 0:17 0:44 27 memstr_0 0:23 0:49 26 isocat_2 0:21 0:47 26 circuit2 0:38 1:04 26 stacks_1 0:14 0:39 25 finseq_3 0:19 0:44 25 numeral1 0:41 1:05 24 modelc_3 1:13 1:37 24 comput_1 1:13 1:37 24 compos_1 0:40 1:04 24 yellow11 0:10 0:33 23 sprect_3 0:42 1:05 23 gobrd11 0:33 0:56 23 fsm_1 0:50 1:13 23 circcmb3 0:32 0:55 23 cfdiff_1 0:18 0:41 23 brouwer 0:44 1:07 23 yellow18 0:15 0:37 22 jordan1j 0:58 1:20 22 card_fin 0:33 0:55 22 ami_6 0:16 0:38 22 integr11 0:34 0:55 21 amistd_1 0:28 0:49 21 afinsq_1 0:54 1:15 21 polynom3 0:36 0:56 20 pnproc_1 0:24 0:44 20 lattice5 0:32 0:52 20 goboard6 0:43 1:03 20 rlaffin1 0:33 0:52 19 quaterni 1:07 1:26 19 polyform 0:27 0:46 19 integra1 0:58 1:17 19 integr12 0:50 1:09 19 endalg 0:04 0:23 19 stirl2_1 0:47 1:05 18 rlaffin2 0:56 1:14 18 polynom5 0:49 1:07 18 mesfun7c 0:22 0:40 18 matrix14 0:19 0:37 18 goboard2 0:38 0:56 18 sin_cos2 0:22 0:39 17 pua2mss1 0:23 0:40 17 borsuk_6 0:42 0:59 17 uproots 1:02 1:18 16 mfold_2 0:48 1:04 16 jordan5b 0:25 0:41 16 afinsq_2 0:32 0:48 16 simplex1 0:43 0:58 15 rmod_4 0:08 0:23 15 limfunc1 0:25 0:40 15 jgraph_2 0:41 0:56 15 fdiff_3 0:45 0:60 15 algspec1 0:07 0:22 15 topalg_1 0:21 0:35 14 pscomp_1 0:45 0:59 14 polynom1 0:23 0:37 14 msualg_6 0:20 0:34 14 jordan23 0:21 0:35 14 fdiff_2 0:38 0:52 14 altcat_4 0:10 0:24 14 zf_lang1 0:12 0:25 13 waybel34 0:19 0:32 13 waybel29 0:27 0:40 13 waybel26 0:25 0:38 13 vectsp_6 0:08 0:21 13 trees_3 0:09 0:22 13 sin_cos3 0:09 0:22 13 scmfsa_4 0:13 0:26 13 dtconstr 0:19 0:32 13 bcialg_6 0:17 0:30 13 yellow20 0:09 0:21 12 vectsp10 0:12 0:24 12 topreal6 0:37 0:49 12 topreal1 0:21 0:33 12 robbins4 0:15 0:27 12 polyeq_5 2:37 2:49 12 oppcat_1 0:09 0:21 12 matrixj1 0:51 1:03 12 goboard1 0:28 0:40 12 finseq_4 0:09 0:21 12 complex2 0:19 0:31 12 circcomb 0:18 0:30 12 scmfsa_m 0:23 0:34 11 scmfsa10 0:22 0:33 11 rfunct_3 0:22 0:33 11 rcomp_3 0:28 0:39 11 pdiff_9 1:05 1:16 11 osafree 0:40 0:51 11 fib_num2 0:19 0:30 11 waybel27 0:21 0:31 10 topreal4 0:12 0:22 10 sppol_2 0:28 0:38 10 rvsum_2 0:08 0:18 10 rearran1 0:23 0:33 10 qc_lang2 0:03 0:13 10 prelamb 0:12 0:22 10 polynom6 0:16 0:26 10 ndiff_1 0:22 0:32 10 hurwitz 0:42 0:52 10 hilbert3 0:10 0:20 10 helly 0:19 0:29 10 fcont_1 0:22 0:32 10 csspace4 0:30 0:40 10 card_4 0:06 0:16 10 vectmetr 0:20 0:29 9 topreal9 0:21 0:30 9 topdim_2 0:28 0:37 9 tmap_1 0:10 0:19 9 scmyciel 0:20 0:29 9 rsspace4 0:24 0:33 9 pdiff_4 0:28 0:37 9 pcs_0 0:08 0:17 9 nat_3 0:22 0:31 9 mesfunc4 0:18 0:27 9 matrtop3 1:47 1:56 9 lattice8 0:15 0:24 9 kolmog01 0:19 0:28 9 integr16 0:12 0:21 9 ideal_1 0:40 0:49 9 hfdiff_1 0:26 0:35 9 gcd_1 0:08 0:17 9 finseq_1 0:12 0:21 9 cqc_sim1 0:22 0:31 9 compos_0 0:14 0:23 9 catalg_1 0:17 0:26 9 zmodul01 0:18 0:26 8 weierstr 0:07 0:15 8 topreal3 0:15 0:23 8 sin_cos6 0:25 0:33 8 pralg_3 0:11 0:19 8 pencil_3 0:13 0:21 8 pdiff_5 0:21 0:29 8 nagata_2 0:37 0:45 8 monoid_1 0:15 0:23 8 matrlin2 0:27 0:35 8 lopban_6 0:09 0:17 8 index_1 0:10 0:18 8 gobrd12 0:47 0:55 8 goboard3 0:20 0:28 8 fvaluat1 0:15 0:23 8 fomodel1 0:29 0:37 8 fdiff_11 0:31 0:39 8 fdiff_1 0:21 0:29 8 circtrm1 0:17 0:25 8 cfdiff_2 0:32 0:40 8 cat_5 0:12 0:20 8 card_2 0:06 0:14 8 sin_cos4 0:04 0:11 7 rfinseq 0:11 0:18 7 random_1 0:24 0:31 7 ordinal6 0:10 0:17 7 msalimit 0:09 0:16 7 mesfunc3 0:26 0:33 7 mazurulm 0:13 0:20 7 jordan_a 0:19 0:26 7 jordan6 0:22 0:29 7 jordan1a 0:25 0:32 7 isocat_1 0:05 0:12 7 integr13 0:17 0:24 7 group_7 0:11 0:18 7 glib_005 1:09 1:16 7 funct_9 0:12 0:19 7 extpro_1 0:08 0:15 7 euclid_9 0:21 0:28 7 dilworth 0:17 0:24 7 closure1 0:06 0:13 7 bilinear 0:13 0:20 7 altcat_2 0:10 0:17 7 abcmiz_0 0:15 0:22 7 zfmodel1 0:09 0:15 6 waybel18 0:12 0:18 6 valued_2 0:35 0:41 6 sublemma 0:44 0:50 6 scmpds_7 1:16 1:22 6 scmfsa7b 0:31 0:37 6 rlvect_4 0:03 0:09 6 quofield 0:10 0:16 6 pralg_1 0:09 0:15 6 ntalgo_1 4:26 4:32 6 ndiff_3 0:15 0:21 6 nattra_1 0:08 0:14 6 mssublat 0:11 0:17 6 matrix10 0:14 0:20 6 jordan5a 0:21 0:27 6 jgraph_8 0:24 0:30 6 integr15 0:25 0:31 6 hahnban 0:11 0:17 6 gobrd14 0:18 0:24 6 filter_1 0:17 0:23 6 euler_1 0:06 0:12 6 equation 0:15 0:21 6 combgras 0:22 0:28 6 cc0sp2 0:39 0:45 6 amistd_2 0:15 0:21 6 waybel25 0:20 0:25 5 trees_2 0:10 0:15 5 topreal2 0:35 0:40 5 topgen_3 0:11 0:16 5 tietze 0:20 0:25 5 series_2 0:33 0:38 5 rusub_3 0:11 0:16 5 rfunct_1 0:09 0:14 5 qc_lang1 0:08 0:13 5 osalg_4 0:14 0:19 5 newton 0:12 0:17 5 msinst_1 0:12 0:17 5 msafree3 0:14 0:19 5 monoid_0 0:13 0:18 5 modelc_2 0:44 0:49 5 measure7 0:10 0:15 5 matrix_7 1:09 1:14 5 lfuzzy_1 0:09 0:14 5 jordan5c 0:14 0:19 5 jordan21 0:16 0:21 5 jordan11 0:21 0:26 5 integr19 0:55 1:00 5 group_4 0:10 0:15 5 groeb_1 1:01 1:06 5 glib_003 0:38 0:43 5 functor0 0:33 0:38 5 extens_1 0:06 0:11 5 dist_1 0:06 0:11 5 clvect_1 0:09 0:14 5 chain_1 0:34 0:39 5 cc0sp1 0:33 0:38 5 cardfin2 0:13 0:18 5 bvfunc_1 0:30 0:35 5 bspace 0:06 0:11 5 borsuk_2 0:11 0:16 5 zf_fund1 0:06 0:10 4 yellow_9 0:09 0:13 4 yellow16 0:07 0:11 4 yellow15 0:07 0:11 4 waybel_6 0:11 0:15 4 triang_1 0:13 0:17 4 trees_9 0:10 0:14 4 topalg_4 0:11 0:15 4 topalg_3 0:11 0:15 4 seq_2 0:10 0:14 4 scmpds_9 0:08 0:12 4 reloc 0:17 0:21 4 ranknull 0:09 0:13 4 prob_3 0:11 0:15 4 pre_circ 0:08 0:12 4 pdiff_8 0:28 0:32 4 msualg_7 0:10 0:14 4 msscyc_1 0:14 0:18 4 msaterm 0:15 0:19 4 metrizts 0:17 0:21 4 mesfunc6 0:12 0:16 4 mesfunc2 0:14 0:18 4 matrixr2 0:42 0:46 4 lopban_1 0:49 0:53 4 jordan5d 0:26 0:30 4 jordan24 0:08 0:12 4 jordan1e 0:14 0:18 4 integra2 0:18 0:22 4 integr10 0:07 0:11 4 int_5 1:14 1:18 4 gobrd13 0:26 0:30 4 glib_004 0:49 0:53 4 functor1 0:05 0:09 4 freealg 0:14 0:18 4 finseq_6 0:10 0:14 4 finseq_5 0:05 0:09 4 fib_num4 0:13 0:17 4 euclid_4 0:10 0:14 4 clopban1 0:49 0:53 4 card_3 0:04 0:08 4 bcialg_5 0:04 0:08 4 amistd_3 0:07 0:11 4 altcat_1 0:04 0:08 4 zf_refle 0:04 0:07 3 zf_lang 0:05 0:08 3 yellow_7 0:07 0:10 3 yellow21 0:06 0:09 3 yellow10 0:07 0:10 3 wellfnd1 0:02 0:05 3 waybel_3 0:06 0:09 3 waybel_2 0:08 0:11 3 waybel21 0:09 0:12 3 waybel17 0:09 0:12 3 vfunct_1 0:08 0:11 3 vectsp_5 0:06 0:09 3 valued_1 0:14 0:17 3 unialg_2 0:05 0:08 3 tsep_1 0:03 0:06 3 trees_1 0:06 0:09 3 topreal7 0:09 0:12 3 topgrp_1 0:05 0:08 3 topdim_1 0:12 0:15 3 sfmastr3 1:08 1:11 3 scmring2 0:05 0:08 3 rusub_2 0:07 0:10 3 rusub_1 0:08 0:11 3 rlvect_3 0:04 0:07 3 rlsub_2 0:06 0:09 3 rfunct_2 0:09 0:12 3 pencil_4 0:05 0:08 3 pencil_1 0:06 0:09 3 pdiff_6 0:40 0:43 3 pboole 0:02 0:05 3 ordinal5 0:06 0:09 3 mycielsk 0:11 0:14 3 msualg_2 0:07 0:10 3 msafree 0:14 0:17 3 mfold_1 0:35 0:38 3 mesfun6c 0:15 0:18 3 limfunc3 0:20 0:23 3 lexbfs 1:10 1:13 3 latsubgr 0:07 0:10 3 jordan8 0:09 0:12 3 jordan1d 0:15 0:18 3 jordan10 0:10 0:13 3 jordan1 0:16 0:19 3 integr14 0:09 0:12 3 hahnban1 0:10 0:13 3 group_6 0:08 0:11 3 group_2 0:08 0:11 3 funct_2 0:02 0:05 3 ftacell1 4:08 4:11 3 fsm_2 0:05 0:08 3 fintopo6 0:10 0:13 3 finsop_1 0:04 0:07 3 filter_2 0:20 0:23 3 fdiff_5 0:16 0:19 3 ens_1 0:15 0:18 3 complfld 0:02 0:05 3 coh_sp 0:05 0:08 3 catalan1 0:02 0:05 3 c0sp2 0:40 0:43 3 borsuk_1 0:08 0:11 3 ami_wstd 0:14 0:17 3 zfrefle1 0:02 0:04 2 yellow12 0:04 0:06 2 waybel_9 0:08 0:10 2 waybel_1 0:07 0:09 2 waybel30 0:09 0:11 2 waybel24 0:07 0:09 2 waybel19 0:08 0:10 2 waybel11 0:13 0:15 2 waybel10 0:12 0:14 2 vfunct_2 0:05 0:07 2 vectsp_8 0:10 0:12 2 vectsp_4 0:04 0:06 2 urysohn1 0:03 0:05 2 topreala 0:08 0:10 2 topalg_2 0:07 0:09 2 taylor_2 0:15 0:17 2 substut1 0:17 0:19 2 simplex2 1:25 1:27 2 sfmastr1 0:29 0:31 2 setwop_2 0:04 0:06 2 seqfunc 0:08 0:10 2 scmring4 0:26 0:28 2 scmfsa8c 1:27 1:29 2 scheme1 0:03 0:05 2 rvsum_1 0:24 0:26 2 rusub_4 0:05 0:07 2 rsspace 0:07 0:09 2 roughs_1 0:07 0:09 2 rmod_3 0:04 0:06 2 rltopsp1 0:07 0:09 2 rlsub_1 0:04 0:06 2 rinfsup1 0:12 0:14 2 quatern3 1:34 1:36 2 quatern2 1:36 1:38 2 partit_2 0:02 0:04 2 numbers 0:02 0:04 2 ndiff_5 2:48 2:50 2 ndiff_4 0:49 0:51 2 ncfcont1 0:20 0:22 2 msualg_4 0:05 0:07 2 msualg_3 0:06 0:08 2 modelc_1 0:16 0:18 2 member_1 0:04 0:06 2 measure6 0:13 0:15 2 measure3 0:06 0:08 2 mcart_1 0:01 0:03 2 lopclset 0:04 0:06 2 lopban_5 0:17 0:19 2 lattice3 0:03 0:05 2 lang1 0:04 0:06 2 knaster 0:06 0:08 2 jordan1k 0:08 0:10 2 jordan18 0:04 0:06 2 jgraph_4 1:35 1:37 2 jct_misc 0:10 0:12 2 int_6 0:15 0:17 2 instalg1 0:13 0:15 2 group_5 0:06 0:08 2 group_3 0:05 0:07 2 graphsp 0:20 0:22 2 goedelcp 0:08 0:10 2 glib_000 0:12 0:14 2 funct_8 0:13 0:15 2 funct_6 0:04 0:06 2 funct_4 0:02 0:04 2 finseq_7 0:05 0:07 2 finseq_2 0:10 0:12 2 fcont_3 0:19 0:21 2 conlat_2 0:09 0:11 2 comseq_1 0:05 0:07 2 complex1 0:05 0:07 2 commacat 0:03 0:05 2 circled1 0:05 0:07 2 cfunct_1 0:09 0:11 2 cfcont_1 0:10 0:12 2 c0sp1 0:36 0:38 2 boolmark 0:03 0:05 2 birkhoff 0:05 0:07 2 bintree2 0:04 0:06 2 binarith 0:29 0:31 2 autalg_1 0:05 0:07 2 alg_1 0:06 0:08 2 zf_fund2 0:03 0:04 1 yellow_3 0:04 0:05 1 yellow_1 0:04 0:05 1 yellow19 0:04 0:05 1 yellow17 0:01 0:02 1 yellow14 0:04 0:05 1 xxreal_1 0:03 0:04 1 xxreal_0 0:00 0:01 1 wsierp_1 0:12 0:13 1 wellord1 0:01 0:02 1 waybel_7 0:05 0:06 1 waybel_4 0:08 0:09 1 waybel35 0:02 0:03 1 waybel33 0:07 0:08 1 waybel32 0:03 0:04 1 waybel28 0:02 0:03 1 waybel23 0:06 0:07 1 waybel20 0:13 0:14 1 waybel14 0:07 0:08 1 waybel12 0:06 0:07 1 vectsp_7 0:02 0:03 1 vectsp_2 0:03 0:04 1 valued_0 0:04 0:05 1 urysohn2 0:06 0:07 1 turing_1 0:23 0:24 1 tsep_2 0:00 0:01 1 trees_a 0:01 0:02 1 trees_4 0:06 0:07 1 tex_2 0:04 0:05 1 tdlat_3 0:01 0:02 1 tdlat_1 0:04 0:05 1 tbsp_1 0:04 0:05 1 t_0topsp 0:01 0:02 1 supinf_2 0:07 0:08 1 substlat 0:01 0:02 1 subset_1 0:00 0:01 1 square_1 0:01 0:02 1 sprect_5 0:04 0:05 1 sincos10 0:19 0:20 1 sin_cos7 0:26 0:27 1 series_1 0:15 0:16 1 seqm_3 0:12 0:13 1 seq_1 0:05 0:06 1 scmpds_i 0:05 0:06 1 scmpds_6 0:47 0:48 1 scmpds_5 0:18 0:19 1 scmp_gcd 0:12 0:13 1 scmfsa_7 0:14 0:15 1 scm_1 0:06 0:07 1 rusub_5 0:03 0:04 1 rpr_1 0:02 0:03 1 rmod_2 0:04 0:05 1 ring_1 0:03 0:04 1 rfinseq2 0:07 0:08 1 rewrite1 0:05 0:06 1 relat_1 0:01 0:02 1 realset2 0:04 0:05 1 real_3 0:28 0:29 1 rat_1 0:02 0:03 1 random_2 0:33 0:34 1 quantal1 0:04 0:05 1 qc_lang4 0:05 0:06 1 prvect_1 0:05 0:06 1 projpl_1 0:01 0:02 1 prob_4 0:12 0:13 1 pralg_2 0:04 0:05 1 polyalg1 0:07 0:08 1 pencil_2 0:07 0:08 1 pdiff_3 0:11 0:12 1 pcomps_2 0:04 0:05 1 partfun1 0:01 0:02 1 ordinal4 0:01 0:02 1 ordinal2 0:01 0:02 1 orders_3 0:01 0:02 1 orders_2 0:02 0:03 1 orders_1 0:03 0:04 1 openlatt 0:02 0:03 1 normform 0:03 0:04 1 nfcont_4 0:12 0:13 1 nfcont_3 0:09 0:10 1 nfcont_1 0:05 0:06 1 msualg_1 0:02 0:03 1 mssubfam 0:02 0:03 1 msafree2 0:07 0:08 1 mod_3 0:03 0:04 1 mmlquery 0:05 0:06 1 metric_6 0:02 0:03 1 metric_1 0:03 0:04 1 mesfunc9 0:29 0:30 1 mesfunc8 0:15 0:16 1 mesfunc7 0:09 0:10 1 mesfun9c 0:16 0:17 1 measure1 0:04 0:05 1 matroid0 0:07 0:08 1 matrix_8 0:03 0:04 1 matrix_4 0:05 0:06 1 matrix_1 0:07 0:08 1 mathmorp 0:03 0:04 1 margrel1 0:03 0:04 1 ltlaxio1 0:14 0:15 1 lmod_7 0:04 0:05 1 limfunc2 0:27 0:28 1 lfuzzy_0 0:06 0:07 1 lattice4 0:02 0:03 1 kurato_2 0:09 0:10 1 jordan1c 0:09 0:10 1 jordan16 0:05 0:06 1 interva1 0:03 0:04 1 integra3 1:26 1:27 1 integr1c 0:41 0:42 1 integr18 0:03 0:04 1 int_7 0:46 0:47 1 int_1 0:01 0:02 1 incsp_1 0:02 0:03 1 hilbert2 0:10 0:11 1 heyting1 0:04 0:05 1 henmodel 0:09 0:10 1 hausdorf 0:03 0:04 1 hallmar1 0:04 0:05 1 grsolv_1 0:06 0:07 1 group_8 0:05 0:06 1 grnilp_1 0:12 0:13 1 grfunc_1 0:00 0:01 1 graph_5 0:20 0:21 1 graph_4 0:08 0:09 1 goboard4 0:25 0:26 1 glib_002 0:13 0:14 1 glib_001 0:54 0:55 1 fuzzy_4 0:07 0:08 1 functor3 0:09 0:10 1 funct_5 0:02 0:03 1 funct_1 0:01 0:02 1 funcop_1 0:02 0:03 1 frechet 0:08 0:09 1 flang_2 0:03 0:04 1 finseq_8 0:04 0:05 1 filter_0 0:03 0:04 1 fib_num 0:07 0:08 1 fdiff_9 0:12 0:13 1 euclid_8 0:38 0:39 1 euclid 0:11 0:12 1 eqrel_1 0:05 0:06 1 entropy1 0:25 0:26 1 ec_pf_1 1:13 1:14 1 csspace2 0:19 0:20 1 convex3 0:06 0:07 1 closure2 0:03 0:04 1 clopban2 0:31 0:32 1 cayley 0:02 0:03 1 cat_4 0:07 0:08 1 card_fil 0:02 0:03 1 card_5 0:03 0:04 1 card_1 0:01 0:02 1 calcul_2 0:05 0:06 1 bvfunc_9 0:06 0:07 1 bvfunc_8 0:01 0:02 1 bvfunc_2 0:03 0:04 1 bvfunc26 0:02 0:03 1 bvfunc11 0:01 0:02 1 brouwer2 0:58 0:59 1 borsuk_4 0:15 0:16 1 bor_cant 0:52 0:53 1 bcialg_2 0:03 0:04 1 bcialg_1 0:03 0:04 1 bagorder 0:43 0:44 1 autgroup 0:04 0:05 1 arytm_2 0:02 0:03 1 anproj_1 0:02 0:03 1 analmetr 0:04 0:05 1 amistd_4 0:01 0:02 1 ami_5 0:13 0:14 1 ali2 0:01 0:02 1 algstr_3 0:00 0:01 1 afvect01 0:00 0:01 1 afproj 0:05 0:06 1 abian 0:05 0:06 1 zfmisc_1 0:01 0:01 0 zf_model 0:02 0:02 0 zf_colla 0:01 0:01 0 yellow_8 0:01 0:01 0 yellow_6 0:14 0:14 0 yellow_5 0:01 0:01 0 yellow_4 0:01 0:01 0 yellow_2 0:02 0:02 0 yellow_0 0:02 0:02 0 yellow13 0:03 0:03 0 xxreal_3 0:03 0:03 0 xxreal_2 0:02 0:02 0 xtuple_0 0:00 0:00 0 xregular 0:00 0:00 0 xreal_1 0:02 0:02 0 xreal_0 0:01 0:01 0 xcmplx_1 0:01 0:01 0 xcmplx_0 0:01 0:01 0 xboolean 0:07 0:07 0 xboole_1 0:00 0:00 0 xboole_0 0:00 0:00 0 wellset1 0:01 0:01 0 wellord2 0:01 0:01 0 waybel_8 0:05 0:05 0 waybel_5 0:20 0:20 0 waybel_0 0:03 0:03 0 waybel31 0:05 0:05 0 waybel22 0:08 0:08 0 waybel16 0:03 0:03 0 waybel15 0:06 0:06 0 waybel13 0:09 0:09 0 vectsp_9 0:13 0:13 0 vectsp_1 0:03 0:03 0 valuat_1 0:07 0:07 0 urysohn3 0:08 0:08 0 uniform1 0:07 0:07 0 unialg_3 0:07 0:07 0 unialg_1 0:01 0:01 0 twoscomp 0:11 0:11 0 tsp_2 0:03 0:03 0 tsp_1 0:01 0:01 0 treal_1 0:07 0:07 0 transgeo 0:03 0:03 0 tops_4 0:06 0:06 0 tops_3 0:01 0:01 0 tops_2 0:03 0:03 0 tops_1 0:01 0:01 0 topreal8 0:09 0:09 0 topreal5 0:04 0:04 0 topmetr3 0:07 0:07 0 topmetr2 0:03 0:03 0 topmetr 0:03 0:03 0 topgen_4 0:03 0:03 0 topgen_2 0:03 0:03 0 topgen_1 0:01 0:01 0 toler_1 0:01 0:01 0 tex_4 0:03 0:03 0 tex_3 0:02 0:02 0 tex_1 0:02 0:02 0 termord 0:10 0:10 0 tdlat_2 0:05 0:05 0 tdgroup 0:01 0:01 0 taxonom2 0:01 0:01 0 taxonom1 0:02 0:02 0 t_1topsp 0:01 0:01 0 sysrel 0:01 0:01 0 symsp_1 0:02 0:02 0 supinf_1 0:00 0:00 0 substut2 0:04 0:04 0 subset 0:00 0:00 0 struct_0 0:00 0:00 0 sppol_1 0:26 0:26 0 sin_cos9 0:22 0:22 0 sin_cos5 0:08 0:08 0 sheffer2 0:01 0:01 0 sheffer1 0:01 0:01 0 sgraph1 0:03 0:03 0 sfmastr2 0:24 0:24 0 setwiseo 0:02 0:02 0 setlim_2 0:03 0:03 0 setlim_1 0:03 0:03 0 setfam_1 0:00 0:00 0 semi_af1 0:02 0:02 0 scpisort 0:36 0:36 0 scmringi 0:06 0:06 0 scmring1 0:03 0:03 0 scmpds_8 0:38 0:38 0 scmpds_3 0:05 0:05 0 scmpds_1 0:01 0:01 0 scmisort 2:10 2:10 0 scmfsa_9 1:04 1:04 0 scmfsa_5 0:08 0:08 0 scmfsa_3 0:08 0:08 0 scmfsa_1 0:05 0:05 0 scmfsa9a 1:01 1:01 0 scmfsa8b 0:44 0:44 0 scmfsa8a 0:29 0:29 0 scmfsa6c 0:19 0:19 0 scmfsa6b 0:20 0:20 0 schems_1 0:00 0:00 0 rsspace3 0:12 0:12 0 rsspace2 0:10 0:10 0 rolle 0:08 0:08 0 robbins3 0:03 0:03 0 robbins2 0:01 0:01 0 robbins1 0:04 0:04 0 rlvect_x 0:07 0:07 0 rlvect_5 0:14 0:14 0 rlvect_1 0:08 0:08 0 ringcat1 0:03 0:03 0 rinfsup2 0:08 0:08 0 rfunct_4 0:12 0:12 0 rewrite3 0:09 0:09 0 rewrite2 0:03 0:03 0 relset_2 0:02 0:02 0 relset_1 0:00 0:00 0 relat_2 0:00 0:00 0 recdef_2 0:02 0:02 0 recdef_1 0:06 0:06 0 realset3 0:01 0:01 0 realset1 0:00 0:00 0 real_ns1 0:19 0:19 0 real_lat 0:02 0:02 0 real_1 0:00 0:00 0 real 0:00 0:00 0 rcomp_1 0:04 0:04 0 ramsey_1 0:12 0:12 0 radix_6 0:02 0:02 0 radix_5 0:03 0:03 0 radix_4 0:05 0:05 0 radix_3 0:05 0:05 0 radix_2 0:09 0:09 0 radix_1 0:06 0:06 0 quin_1 0:04 0:04 0 qmax_1 0:03 0:03 0 qc_lang3 0:02 0:02 0 pzfmisc1 0:01 0:01 0 pythtrip 0:04 0:04 0 prvect_3 0:52 0:52 0 prvect_2 0:16 0:16 0 projred2 0:01 0:01 0 projred1 0:01 0:01 0 projdes1 0:00 0:00 0 procal_1 0:00 0:00 0 prob_2 0:05 0:05 0 prob_1 0:03 0:03 0 prgcor_2 0:05 0:05 0 prepower 0:23 0:23 0 pre_topc 0:01 0:01 0 pre_ff 0:03 0:03 0 power 0:05 0:05 0 poset_1 0:06 0:06 0 polynom8 0:10 0:10 0 polynom4 0:10 0:10 0 polyeq_1 0:08 0:08 0 petri_2 0:05 0:05 0 petri 0:01 0:01 0 pdiff_2 0:27 0:27 0 pdiff_1 0:35 0:35 0 pcomps_1 0:03 0:03 0 pasch 0:01 0:01 0 partit1 0:02 0:02 0 partfun4 0:02 0:02 0 partfun3 0:05 0:05 0 partfun2 0:01 0:01 0 parsp_2 0:03 0:03 0 parsp_1 0:01 0:01 0 pardepap 0:00 0:00 0 papdesaf 0:01 0:01 0 osalg_3 0:02 0:02 0 osalg_2 0:06 0:06 0 osalg_1 0:03 0:03 0 ortsp_1 0:02 0:02 0 ordinal3 0:01 0:01 0 ordinal1 0:01 0:01 0 orders_4 0:03 0:03 0 oposet_1 0:01 0:01 0 o_ring_1 0:04 0:04 0 numerals 0:00 0:00 0 normsp_2 0:06 0:06 0 normsp_1 0:04 0:04 0 normsp_0 0:00 0:00 0 nfcont_2 0:07 0:07 0 net_1 0:00 0:00 0 neckla_2 0:04 0:04 0 ndiff_2 0:13 0:13 0 ncfcont2 0:13 0:13 0 nat_lat 0:02 0:02 0 nat_d 0:02 0:02 0 nat_2 0:05 0:05 0 multop_1 0:00 0:00 0 msafree1 0:03 0:03 0 morph_01 0:02 0:02 0 modcat_1 0:02 0:02 0 mod_4 0:10 0:10 0 mod_2 0:05 0:05 0 midsp_3 0:02 0:02 0 midsp_2 0:01 0:01 0 midsp_1 0:01 0:01 0 metric_3 0:07 0:07 0 metric_2 0:01 0:01 0 mesfunc1 0:08 0:08 0 mesfun10 0:14 0:14 0 membered 0:00 0:00 0 measure5 0:01 0:01 0 measure4 0:05 0:05 0 measure2 0:03 0:03 0 mboolean 0:01 0:01 0 matrprob 0:18 0:18 0 matrlin 0:21 0:21 0 matrixr1 0:09 0:09 0 matrixc1 0:15 0:15 0 matrix_5 0:02 0:02 0 matrix_3 0:14 0:14 0 matrix_2 0:04 0:04 0 matrix17 0:06 0:06 0 matrix16 0:16 0:16 0 matrix12 0:05 0:05 0 lukasi_1 0:01 0:01 0 lp_space 0:16 0:16 0 lopban_4 0:15 0:15 0 lopban_3 0:19 0:19 0 lopban_2 0:27 0:27 0 lmod_6 0:01 0:01 0 lmod_5 0:02 0:02 0 limfunc4 0:14 0:14 0 lattices 0:01 0:01 0 lattice7 0:02 0:02 0 lattice6 0:06 0:06 0 lattice2 0:02 0:02 0 latsum_1 0:01 0:01 0 laplace 0:43 0:43 0 l_hospit 0:16 0:16 0 kurato_1 0:04 0:04 0 kurato_0 0:02 0:02 0 jordan2b 0:08 0:08 0 jordan22 0:32 0:32 0 jordan20 0:39 0:39 0 jordan1i 0:18 0:18 0 jordan1f 0:11 0:11 0 jordan1b 0:10 0:10 0 jordan17 0:03 0:03 0 jordan14 0:25 0:25 0 jgraph_7 0:47 0:47 0 isomichi 0:03 0:03 0 irrat_1 0:12 0:12 0 intpro_1 0:03 0:03 0 integra8 0:15 0:15 0 integra7 0:14 0:14 0 integra6 0:29 0:29 0 int_2 0:01 0:01 0 incproj 0:01 0:01 0 idea_1 0:22 0:22 0 homothet 0:01 0:01 0 hilbert1 0:01 0:01 0 hilbasis 1:28 1:28 0 heyting3 0:10 0:10 0 heyting2 0:04 0:04 0 hessenbe 0:00 0:00 0 heine 0:06 0:06 0 groupp_1 0:05 0:05 0 group_12 0:06 0:06 0 group_11 0:01 0:01 0 group_1 0:04 0:04 0 groeb_3 0:41 0:41 0 groeb_2 0:35 0:35 0 grcat_1 0:06 0:06 0 graph_1 0:07 0:07 0 gr_cy_2 0:04 0:04 0 gr_cy_1 0:13 0:13 0 goboard8 0:12 0:12 0 goboard7 0:44 0:44 0 gfacirc2 0:25 0:25 0 geomtrap 0:09 0:09 0 genealg1 0:11 0:11 0 gate_5 1:39 1:39 0 gate_4 0:01 0:01 0 gate_3 0:02 0:02 0 gate_2 0:00 0:00 0 gate_1 0:01 0:01 0 fvsum_1 0:07 0:07 0 fuzzy_2 0:06 0:06 0 fuzzy_1 0:05 0:05 0 functor2 0:04 0:04 0 funct_3 0:02 0:02 0 funcsdom 0:04 0:04 0 fsm_3 0:08 0:08 0 frechet2 0:08 0:08 0 fraenkel 0:01 0:01 0 flang_3 0:02 0:02 0 flang_1 0:03 0:03 0 fintopo5 0:03 0:03 0 fintopo4 0:02 0:02 0 fintopo3 0:01 0:01 0 fintopo2 0:01 0:01 0 finsub_1 0:00 0:00 0 finset_1 0:01 0:01 0 finseqop 0:07 0:07 0 finance1 0:06 0:06 0 fin_topo 0:02 0:02 0 filerec1 0:05 0:05 0 fib_num3 0:06 0:06 0 fib_fusc 0:05 0:05 0 ff_siec 0:01 0:01 0 fdiff_8 0:12 0:12 0 fdiff_10 0:09 0:09 0 fcont_2 0:11 0:11 0 extreal2 0:01 0:01 0 euclmetr 0:02 0:02 0 euclidlp 0:13 0:13 0 euclid_5 0:04 0:04 0 euclid_2 0:05 0:05 0 ec_pf_2 0:30 0:30 0 e_siec 0:01 0:01 0 dynkin 0:01 0:01 0 domain_1 0:01 0:01 0 dirort 0:01 0:01 0 diraf 0:01 0:01 0 diff_3 0:36 0:36 0 diff_2 0:17 0:17 0 diff_1 0:18 0:18 0 csspace3 0:14 0:14 0 csspace 0:17 0:17 0 cqc_the3 0:02 0:02 0 cqc_the2 0:02 0:02 0 cqc_lang 0:03 0:03 0 convfun1 0:21 0:21 0 convex2 0:12 0:12 0 connsp_2 0:01 0:01 0 connsp_1 0:02 0:02 0 conmetr1 0:02 0:02 0 conmetr 0:02 0:02 0 conaffm 0:01 0:01 0 comseq_3 0:16 0:16 0 comseq_2 0:06 0:06 0 compts_1 0:02 0:02 0 compos_2 0:08 0:08 0 complsp2 0:24 0:24 0 complsp1 0:02 0:02 0 compact1 0:03 0:03 0 collsp 0:00 0:00 0 clvect_3 0:12 0:12 0 clvect_2 0:08 0:08 0 closure3 0:03 0:03 0 clopban4 0:17 0:17 0 clopban3 0:18 0:18 0 classes2 0:01 0:01 0 classes1 0:02 0:02 0 circcmb2 0:05 0:05 0 cgames_1 0:05 0:05 0 cfuncdom 0:02 0:02 0 cat_3 0:04 0:04 0 cat_2 0:07 0:07 0 cat_1 0:03 0:03 0 card_lar 0:01 0:01 0 cantor_1 0:01 0:01 0 bvfunc_7 0:02 0:02 0 bvfunc_4 0:03 0:03 0 bvfunc_3 0:02 0:02 0 bvfunc25 0:01 0:01 0 borsuk_3 0:03 0:03 0 boolealg 0:01 0:01 0 boole 0:00 0:00 0 bintree1 0:07 0:07 0 binop_2 0:01 0:01 0 binop_1 0:01 0:01 0 binom 0:08 0:08 0 binari_4 0:10 0:10 0 binari_3 0:04 0:04 0 binari_2 0:36 0:36 0 bhsp_7 0:02 0:02 0 bhsp_6 0:05 0:05 0 bhsp_5 0:04 0:04 0 bhsp_4 0:12 0:12 0 bhsp_3 0:04 0:04 0 bhsp_2 0:03 0:03 0 bhsp_1 0:05 0:05 0 bciideal 0:01 0:01 0 bcialg_4 0:03 0:03 0 bcialg_3 0:01 0:01 0 axioms 0:00 0:00 0 arytm_3 0:01 0:01 0 arytm_1 0:00 0:00 0 arytm_0 0:02 0:02 0 arrow 0:02 0:02 0 armstrng 0:29 0:29 0 arithm 0:00 0:00 0 aofa_000 2:13 -133 analort 0:03 0:03 0 analoaf 0:03 0:03 0 ami_4 0:07 0:07 0 ami_3 0:10 0:10 0 ami_2 0:04 0:04 0 algstr_4 0:25 0:25 0 algstr_2 0:02 0:02 0 algstr_1 0:02 0:02 0 algstr_0 0:00 0:00 0 algseq_1 0:00 0:00 0 afvect0 0:02 0:02 0 aff_4 0:01 0:01 0 aff_3 0:01 0:01 0 aff_2 0:01 0:01 0 aff_1 0:00 0:00 0 absvalue 0:01 0:01 0 vectsp11 0:57 0:56 -1 translac 0:02 0:01 -1 toprns_1 0:09 0:08 -1 sprect_4 0:22 0:21 -1 series_4 0:14 0:13 -1 scpinvar 1:06 1:05 -1 scmpds_2 0:28 0:27 -1 ratfunc1 0:29 0:28 -1 polyred 0:49 0:48 -1 polynom7 0:13 0:12 -1 polynom2 0:40 0:39 -1 nagata_1 0:17 0:16 -1 msualg_5 0:11 0:10 -1 msscyc_2 0:17 0:16 -1 measure8 0:21 0:20 -1 matrix_6 0:05 0:04 -1 integra5 0:21 0:20 -1 integra4 0:35 0:34 -1 gr_cy_3 0:07 0:06 -1 fscirc_1 0:12 0:11 -1 extreal1 0:11 0:10 -1 dickson 0:32 0:31 -1 connsp_3 0:02 0:01 -1 conlat_1 0:07 0:06 -1 compl_sp 0:24 0:23 -1 bvfunc_5 0:02 0:01 -1 bvfunc14 0:24 0:23 -1 asympt_1 1:31 1:30 -1 altcat_3 0:02 0:01 -1 polyeq_4 0:08 0:06 -2 decomp_1 0:05 0:03 -2 yoneda_1 0:17 0:14 -3 prgcor_1 0:12 0:09 -3 nat_5 0:46 0:43 -3 bvfunc_6 0:27 0:24 -3 bvfunc10 0:22 0:18 -4 msuhom_1 0:14 0:09 -5 sin_cos8 0:21 0:15 -6 polyeq_3 0:46 0:40 -6 integra9 0:30 0:24 -6 pepin 0:20 0:13 -7 jordan4 0:50 0:43 -7 jordan3 0:57 0:50 -7 asympt_0 0:43 0:35 -8 taylor_1 0:44 0:35 -9 msualg_8 0:24 0:14 -10 euler_2 0:35 0:25 -10 gobrd10 0:19 0:07 -12 polyeq_2 0:23 0:08 -15 int_3 0:37 0:22 -15 fdiff_4 0:39 0:24 -15 series_3 0:51 0:35 -16 fdiff_7 0:31 0:13 -18 comptrig 0:54 0:35 -19 weddwitt 1:07 0:47 -20 lpspace1 0:52 0:30 -22 simplex0 0:52 0:27 -25 fdiff_6 1:02 0:29 -33 series_5 1:02 0:26 -36 ----- Koniec przekazanej wiadomości -----