Index of /~mptp/1147/mptp/ilp1/reflexivity_r1_tarski
Name
Last modified
Size
Description
Parent Directory
-
zmodul01__1926_55.min1.thm1.tptp
2017-02-06 16:57
391
zmodul01__1925_76.min1.thm1.tptp
2017-02-06 16:57
373
zmodul01__988_56.min1.thm1.tptp
2017-02-06 16:57
391
zmodul01__987_76.min1.thm1.tptp
2017-02-06 16:57
372
zfrefle1__211_15.min1.thm1.tptp
2017-02-06 16:57
270
zfmisc_1__2026_16.min1.thm1.tptp
2017-02-06 16:57
327
zfmisc_1__901_28.min1.thm1.tptp
2017-02-06 16:57
350
zfmisc_1__879_16.min1.thm1.tptp
2017-02-06 16:57
292
zfmisc_1__670_67.min1.thm1.tptp
2017-02-06 16:57
454
zfmisc_1__661_39.min1.thm1.tptp
2017-02-06 16:57
327
zfmisc_1__491_41.min1.thm1.tptp
2017-02-06 16:57
381
zfmisc_1__167_25.min1.thm1.tptp
2017-02-06 16:57
273
zfmisc_1__67_16.min1.thm1.tptp
2017-02-06 16:57
305
zf_fund2__201_18.min1.thm1.tptp
2017-02-06 16:57
295
yellow_9__2751_59.min1.thm1.tptp
2017-02-06 16:57
298
yellow_9__2749_59.min1.thm1.tptp
2017-02-06 16:57
298
yellow_9__1801_57.min1.thm1.tptp
2017-02-06 16:57
295
yellow_9__1799_57.min1.thm1.tptp
2017-02-06 16:57
295
yellow_8__297_15.min1.thm1.tptp
2017-02-06 16:57
247
yellow_0__1659_11.min1.thm1.tptp
2017-02-06 16:57
321
xboole_1__961_56.min1.thm1.tptp
2017-02-06 16:57
338
wellord1__769_14.min1.thm1.tptp
2017-02-06 16:57
534
wellfnd1__400_39.min1.thm1.tptp
2017-02-06 16:57
295
waybel_4__2979_29.min1.thm1.tptp
2017-02-06 16:57
558
waybel_0__1225_55.min1.thm1.tptp
2017-02-06 16:57
299
waybel27__297_33.min1.thm1.tptp
2017-02-06 16:57
747
waybel23__540_55.min1.thm1.tptp
2017-02-06 16:57
299
waybel18__1301_19.min1.thm1.tptp
2017-02-06 16:57
275
waybel16__478_42.min1.thm1.tptp
2017-02-06 16:57
276
waybel14__130_15.min1.thm1.tptp
2017-02-06 16:57
228
waybel14__116_19.min1.thm1.tptp
2017-02-06 16:57
256
waybel11__2767_48.min1.thm1.tptp
2017-02-06 16:57
337
vectsp_9__1689_48.min1.thm1.tptp
2017-02-06 16:57
304
vectsp_9__191_46.min1.thm1.tptp
2017-02-06 16:57
294
vectsp_4__1751_53.min1.thm1.tptp
2017-02-06 16:57
295
urysohn3__1746_58.min1.thm1.tptp
2017-02-06 16:57
301
urysohn3__728_57.min1.thm1.tptp
2017-02-06 16:57
301
urysohn1__801_20.min1.thm1.tptp
2017-02-06 16:57
235
unialg_3__724_55.min1.thm1.tptp
2017-02-06 16:57
295
tops_2__1404_38.min1.thm1.tptp
2017-02-06 16:57
739
tops_2__1364_39.min1.thm1.tptp
2017-02-06 16:57
739
topgen_4__49_14.min1.thm1.tptp
2017-02-06 16:57
320
topalg_5__1431_20.min1.thm1.tptp
2017-02-06 16:57
259
topalg_2__538_33.min1.thm1.tptp
2017-02-06 16:57
225
tmap_1__2559_56.min1.thm1.tptp
2017-02-06 16:57
289
tex_4__1515_56.min1.thm1.tptp
2017-02-06 16:57
499
tex_3__531_59.min1.thm1.tptp
2017-02-06 16:57
290
tex_3__382_59.min1.thm1.tptp
2017-02-06 16:57
290
tex_3__204_59.min1.thm1.tptp
2017-02-06 16:57
290
tex_2__1542_58.min1.thm1.tptp
2017-02-06 16:57
288
tex_1__1332_36.min1.thm1.tptp
2017-02-06 16:57
262
tex_1__656_38.min1.thm1.tptp
2017-02-06 16:57
264
tex_1__192_57.min1.thm1.tptp
2017-02-06 16:57
291
tdlat_2__879_20.min1.thm1.tptp
2017-02-06 16:57
511
taxonom2__729_16.min1.thm1.tptp
2017-02-06 16:57
386
subset_1__177_18.min1.thm1.tptp
2017-02-06 16:57
296
subset_1__94_18.min1.thm1.tptp
2017-02-06 16:57
293
simplex1__656_22.min1.thm1.tptp
2017-02-06 16:57
335
sgraph1__827_11.min1.thm1.tptp
2017-02-06 16:57
342
setfam_1__1592_14.min1.thm1.tptp
2017-02-06 16:57
297
setfam_1__1499_18.min1.thm1.tptp
2017-02-06 16:57
247
scmyciel__1456_35.min1.thm1.tptp
2017-02-06 16:57
273
rusub_4__920_48.min1.thm1.tptp
2017-02-06 16:57
301
rusub_1__1857_53.min1.thm1.tptp
2017-02-06 16:57
375
rusub_1__1856_74.min1.thm1.tptp
2017-02-06 16:57
363
rusub_1__627_56.min1.thm1.tptp
2017-02-06 16:57
383
rusub_1__626_76.min1.thm1.tptp
2017-02-06 16:57
367
rmod_2__1490_53.min1.thm1.tptp
2017-02-06 16:57
289
rlvect_5__1731_48.min1.thm1.tptp
2017-02-06 16:57
304
rlvect_5__238_46.min1.thm1.tptp
2017-02-06 16:57
294
rlsub_1__1650_53.min1.thm1.tptp
2017-02-06 16:57
375
rlsub_1__1649_74.min1.thm1.tptp
2017-02-06 16:57
363
rlsub_1__597_56.min1.thm1.tptp
2017-02-06 16:57
383
rlsub_1__596_76.min1.thm1.tptp
2017-02-06 16:57
367
relset_1__381_48.min1.thm1.tptp
2017-02-06 16:57
327
relat_1__1092_21.min1.thm1.tptp
2017-02-06 16:57
327
relat_1__1071_21.min1.thm1.tptp
2017-02-06 16:57
325
rearran1__544_40.min1.thm1.tptp
2017-02-06 16:57
273
rearran1__326_22.min1.thm1.tptp
2017-02-06 16:57
343
rearran1__174_22.min1.thm1.tptp
2017-02-06 16:57
301
realset1__56_40.min1.thm1.tptp
2017-02-06 16:57
270
ramsey_1__1076_36.min1.thm1.tptp
2017-02-06 16:57
275
ramsey_1__259_15.min1.thm1.tptp
2017-02-06 16:57
221
prob_4__1629_24.min1.thm1.tptp
2017-02-06 16:57
403
pre_poly__2956_16.min1.thm1.tptp
2017-02-06 16:57
304
poset_1__874_51.min1.thm1.tptp
2017-02-06 16:57
341
pboole__2431_32.min1.thm1.tptp
2017-02-06 16:57
321
partit_2__690_16.min1.thm1.tptp
2017-02-06 16:57
331
osalg_2__563_28.min1.thm1.tptp
2017-02-06 16:57
553
osalg_2__559_25.min1.thm1.tptp
2017-02-06 16:57
553
ordinal6__1025_69.min1.thm1.tptp
2017-02-06 16:57
359
ordinal6__62_24.min1.thm1.tptp
2017-02-06 16:57
244
nfcont_1__1616_26.min1.thm1.tptp
2017-02-06 16:57
443
nfcont_1__1569_26.min1.thm1.tptp
2017-02-06 16:57
479
nfcont_1__1478_26.min1.thm1.tptp
2017-02-06 16:57
479
neckla_2__498_54.min1.thm1.tptp
2017-02-06 16:57
355
ncfcont1__4591_26.min1.thm1.tptp
2017-02-06 16:57
455
ncfcont1__4543_26.min1.thm1.tptp
2017-02-06 16:57
493
ncfcont1__4495_26.min1.thm1.tptp
2017-02-06 16:57
493
ncfcont1__4447_26.min1.thm1.tptp
2017-02-06 16:57
493
ncfcont1__4249_26.min1.thm1.tptp
2017-02-06 16:57
493
ncfcont1__4225_26.min1.thm1.tptp
2017-02-06 16:57
493
ncfcont1__4201_26.min1.thm1.tptp
2017-02-06 16:57
479
nat_4__2375_16.min1.thm1.tptp
2017-02-06 16:57
327
nagata_1__845_21.min1.thm1.tptp
2017-02-06 16:57
282
nagata_1__685_38.min1.thm1.tptp
2017-02-06 16:57
297
nagata_1__678_46.min1.thm1.tptp
2017-02-06 16:57
318
mycielsk__1669_48.min1.thm1.tptp
2017-02-06 16:57
331
monoid_0__1012_11.min1.thm1.tptp
2017-02-06 16:57
263
modelc_3__3208_32.min1.thm1.tptp
2017-02-06 16:57
700
modelc_3__188_23.min1.thm1.tptp
2017-02-06 16:57
301
measure8__481_23.min1.thm1.tptp
2017-02-06 16:57
261
measure4__159_29.min1.thm1.tptp
2017-02-06 16:57
404
measure3__1420_24.min1.thm1.tptp
2017-02-06 16:57
423
measure2__767_11.min1.thm1.tptp
2017-02-06 16:57
313
lpspace1__82_39.min1.thm1.tptp
2017-02-06 16:57
296
lattice8__3024_18.min1.thm1.tptp
2017-02-06 16:57
349
lattice8__2982_18.min1.thm1.tptp
2017-02-06 16:57
349
lattice8__1931_22.min1.thm1.tptp
2017-02-06 16:57
345
lattice8__1906_22.min1.thm1.tptp
2017-02-06 16:57
319
lattice8__1823_18.min1.thm1.tptp
2017-02-06 16:57
293
lattice8__1792_18.min1.thm1.tptp
2017-02-06 16:57
319
lattice6__569_54.min1.thm1.tptp
2017-02-06 16:57
292
lattice5__4281_18.min1.thm1.tptp
2017-02-06 16:57
349
lattice5__4241_18.min1.thm1.tptp
2017-02-06 16:57
349
lattice5__3231_22.min1.thm1.tptp
2017-02-06 16:57
345
lattice5__3206_22.min1.thm1.tptp
2017-02-06 16:57
319
lattice5__3130_18.min1.thm1.tptp
2017-02-06 16:57
293
lattice5__3099_18.min1.thm1.tptp
2017-02-06 16:57
319
lattice4__343_51.min1.thm1.tptp
2017-02-06 16:57
295
lang1__1071_48.min1.thm1.tptp
2017-02-06 16:57
316
kurato_2__868_37.min1.thm1.tptp
2017-02-06 16:57
313
knaster__774_55.min1.thm1.tptp
2017-02-06 16:57
296
knaster__234_41.min1.thm1.tptp
2017-02-06 16:57
265
knaster__191_16.min1.thm1.tptp
2017-02-06 16:57
351
jordan3__583_18.min1.thm1.tptp
2017-02-06 16:57
497
integra8__381_11.min1.thm1.tptp
2017-02-06 16:57
266
ideal_1__362_54.min1.thm1.tptp
2017-02-06 16:57
292
ideal_1__343_54.min1.thm1.tptp
2017-02-06 16:57
292
ideal_1__319_54.min1.thm1.tptp
2017-02-06 16:57
292
ideal_1__173_39.min1.thm1.tptp
2017-02-06 16:57
293
ideal_1__161_39.min1.thm1.tptp
2017-02-06 16:57
293
ideal_1__148_39.min1.thm1.tptp
2017-02-06 16:57
293
ideal_1__133_39.min1.thm1.tptp
2017-02-06 16:57
293
ideal_1__122_39.min1.thm1.tptp
2017-02-06 16:57
293
ideal_1__107_39.min1.thm1.tptp
2017-02-06 16:57
293
heyting3__1036_19.min1.thm1.tptp
2017-02-06 16:57
262
helly__2082_15.min1.thm1.tptp
2017-02-06 16:57
1.0K
hallmar1__949_16.min1.thm1.tptp
2017-02-06 16:57
469
group_6__1325_55.min1.thm1.tptp
2017-02-06 16:57
296
group_2__2801_53.min1.thm1.tptp
2017-02-06 16:57
295
group_2__2782_53.min1.thm1.tptp
2017-02-06 16:57
295
graph_4__2235_44.min1.thm1.tptp
2017-02-06 16:57
272
graph_4__2234_41.min1.thm1.tptp
2017-02-06 16:57
272
graph_4__2219_42.min1.thm1.tptp
2017-02-06 16:57
270
graph_4__2218_39.min1.thm1.tptp
2017-02-06 16:57
270
graph_2__4249_41.min1.thm1.tptp
2017-02-06 16:57
272
graph_2__4248_44.min1.thm1.tptp
2017-02-06 16:57
272
graph_2__4235_39.min1.thm1.tptp
2017-02-06 16:57
270
graph_2__4234_42.min1.thm1.tptp
2017-02-06 16:57
270
graph_2__1363_14.min1.thm1.tptp
2017-02-06 16:57
266
goedelcp__1827_18.min1.thm1.tptp
2017-02-06 16:57
383
glib_001__4107_47.min1.thm1.tptp
2017-02-06 16:57
345
glib_001__3945_57.min1.thm1.tptp
2017-02-06 16:57
334
glib_001__3934_59.min1.thm1.tptp
2017-02-06 16:57
338
glib_000__1101_25.min1.thm1.tptp
2017-02-06 16:57
330
funct_7__3420_12.min1.thm1.tptp
2017-02-06 16:57
242
fomodel4__958_2.min1.thm1.tptp
2017-02-06 16:57
301
fomodel4__816_59.min1.thm1.tptp
2017-02-06 16:57
547
fomodel3__975_39.min1.thm1.tptp
2017-02-06 16:57
331
fomodel2__1117_53.min1.thm1.tptp
2017-02-06 16:57
265
fomodel2__790_35.min1.thm1.tptp
2017-02-06 16:57
326
fomodel2__101_10.min1.thm1.tptp
2017-02-06 16:57
380
fomodel1__1047_45.min1.thm1.tptp
2017-02-06 16:57
340
flang_3__867_16.min1.thm1.tptp
2017-02-06 16:57
557
flang_2__1036_8.min1.thm1.tptp
2017-02-06 16:57
621
flang_2__788_30.min1.thm1.tptp
2017-02-06 16:57
321
fintopo5__1286_15.min1.thm1.tptp
2017-02-06 16:57
270
finseq_3__1653_19.min1.thm1.tptp
2017-02-06 16:57
404
euclid_9__1298_27.min1.thm1.tptp
2017-02-06 16:57
1.4K
eqrel_1__54_16.min1.thm1.tptp
2017-02-06 16:57
321
ens_1__1392_47.min1.thm1.tptp
2017-02-06 16:57
919
e_siec__112_43.min1.thm1.tptp
2017-02-06 16:57
370
dynkin__483_45.min1.thm1.tptp
2017-02-06 16:57
275
conlat_1__2816_71.min1.thm1.tptp
2017-02-06 16:57
295
conlat_1__2748_69.min1.thm1.tptp
2017-02-06 16:57
295
comput_1__4399_18.min1.thm1.tptp
2017-02-06 16:57
393
compts_1__1206_36.min1.thm1.tptp
2017-02-06 16:57
335
complsp1__47_56.min1.thm1.tptp
2017-02-06 16:57
294
cohsp_1__505_20.min1.thm1.tptp
2017-02-06 16:57
288
clvect_1__2031_53.min1.thm1.tptp
2017-02-06 16:57
391
clvect_1__2030_74.min1.thm1.tptp
2017-02-06 16:57
373
clvect_1__993_56.min1.thm1.tptp
2017-02-06 16:57
391
clvect_1__992_76.min1.thm1.tptp
2017-02-06 16:57
372
closure2__178_16.min1.thm1.tptp
2017-02-06 16:57
326
classes1__1688_17.min1.thm1.tptp
2017-02-06 16:57
377
chain_1__2299_16.min1.thm1.tptp
2017-02-06 16:57
354
chain_1__1759_50.min1.thm1.tptp
2017-02-06 16:57
298
cfcont_1__1844_26.min1.thm1.tptp
2017-02-06 16:57
371
card_3__2908_32.min1.thm1.tptp
2017-02-06 16:57
321
card_1__1946_26.min1.thm1.tptp
2017-02-06 16:57
395
borsuk_2__1527_64.min1.thm1.tptp
2017-02-06 16:57
287
bhsp_7__262_15.min1.thm1.tptp
2017-02-06 16:57
325
bhsp_7__230_26.min1.thm1.tptp
2017-02-06 16:57
347
bhsp_6__676_24.min1.thm1.tptp
2017-02-06 16:57
357
bciideal__1250_26.min1.thm1.tptp
2017-02-06 16:57
264
bciideal__1200_26.min1.thm1.tptp
2017-02-06 16:57
264
bciideal__361_26.min1.thm1.tptp
2017-02-06 16:57
264
arrow__141_48.min1.thm1.tptp
2017-02-06 16:57
311
arrow__117_27.min1.thm1.tptp
2017-02-06 16:57
334
altcat_2__1131_18.min1.thm1.tptp
2017-02-06 16:57
609
algstr_4__2202_40.min1.thm1.tptp
2017-02-06 16:57
304
algstr_4__1907_48.min1.thm1.tptp
2017-02-06 16:57
391
algstr_4__865_53.min1.thm1.tptp
2017-02-06 16:57
299
afproj__695_54.min1.thm1.tptp
2017-02-06 16:57
289
afproj__100_53.min1.thm1.tptp
2017-02-06 16:57
286
abcmiz_1__611_13.min1.thm1.tptp
2017-02-06 16:57
366
abcmiz_1__348_14.min1.thm1.tptp
2017-02-06 16:57
696
Apache/2.4.18 (Ubuntu) Server at grid01.ciirc.cvut.cz Port 80