[mizar] Fwd: [dev-forum] Re: Urelements?

[trybulec@math.uwb.edu.pl]

----- Przekazana wiadomość od arturk@math.uwb.edu.pl -----
   Data: Mon, 12 Mar 2012 11:41:44 +0100 (CET)
   Od: Artur Kornilowicz <arturk@math.uwb.edu.pl>
Odpowiedz-Do:developer-forum@mizar.uwb.edu.pl
Temat: [dev-forum] Re: Urelements?
     Do: Developer-Forum <developer-forum@mizar.uwb.edu.pl>

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 -----