Index of /~mptp/7.13.01_4.181.1147/MPTP2/ilp1/d3_xboole_0

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[ ]abcmiz_a__604_45.min1.thm1.tptp2017-02-06 16:57 474  
[ ]abcmiz_a__2197_23.min1.thm1.tptp2017-02-06 16:57 518  
[ ]abcmiz_a__2202_18.min1.thm1.tptp2017-02-06 16:57 510  
[ ]abian__1113_18.min1.thm1.tptp2017-02-06 16:57 783  
[ ]abian__1154_27.min1.thm1.tptp2017-02-06 16:57 490  
[ ]afinsq_1__85_19.min1.thm1.tptp2017-02-06 16:57 431  
[ ]afinsq_2__1194_28.min1.thm1.tptp2017-02-06 16:57 434  
[ ]afinsq_2__1231_41.min1.thm1.tptp2017-02-06 16:57 463  
[ ]afinsq_2__1292_28.min1.thm1.tptp2017-02-06 16:57 454  
[ ]afinsq_2__2122_30.min1.thm1.tptp2017-02-06 16:57 499  
[ ]afinsq_2__3773_19.min1.thm1.tptp2017-02-06 16:57 677  
[ ]algspec1__63_38.min1.thm1.tptp2017-02-06 16:57 451  
[ ]aofa_000__105_38.min1.thm1.tptp2017-02-06 16:57 436  
[ ]aofa_000__396_26.min1.thm1.tptp2017-02-06 16:57 385  
[ ]aofa_000__1421_47.min1.thm1.tptp2017-02-06 16:57 740  
[ ]aofa_000__1691_8.min1.thm1.tptp2017-02-06 16:57 604  
[ ]armstrng__2973_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]armstrng__3064_18.min1.thm1.tptp2017-02-06 16:57 494  
[ ]armstrng__3299_22.min1.thm1.tptp2017-02-06 16:57 371  
[ ]arytm_0__52_43.min1.thm1.tptp2017-02-06 16:57 440  
[ ]arytm_0__204_44.min1.thm1.tptp2017-02-06 16:57 438  
[ ]arytm_0__209_39.min1.thm1.tptp2017-02-06 16:57 439  
[ ]arytm_0__369_16.min1.thm1.tptp2017-02-06 16:57 521  
[ ]arytm_0__384_45.min1.thm1.tptp2017-02-06 16:57 456  
[ ]arytm_0__543_18.min1.thm1.tptp2017-02-06 16:57 449  
[ ]arytm_0__575_48.min1.thm1.tptp2017-02-06 16:57 482  
[ ]arytm_0__605_20.min1.thm1.tptp2017-02-06 16:57 477  
[ ]arytm_0__694_16.min1.thm1.tptp2017-02-06 16:57 457  
[ ]bagorder__364_24.min1.thm1.tptp2017-02-06 16:57 492  
[ ]bagorder__396_24.min1.thm1.tptp2017-02-06 16:57 492  
[ ]bagorder__420_24.min1.thm1.tptp2017-02-06 16:57 492  
[ ]bagorder__490_24.min1.thm1.tptp2017-02-06 16:57 492  
[ ]bagorder__522_24.min1.thm1.tptp2017-02-06 16:57 492  
[ ]bagorder__546_24.min1.thm1.tptp2017-02-06 16:57 492  
[ ]binom__1778_18.min1.thm1.tptp2017-02-06 16:57 567  
[ ]bintree2__1142_21.min1.thm1.tptp2017-02-06 16:57 418  
[ ]boole__40_29.min1.thm1.tptp2017-02-06 16:57 364  
[ ]boole__45_17.min1.thm1.tptp2017-02-06 16:57 317  
[ ]borsuk_1__1435_20.min1.thm1.tptp2017-02-06 16:57 488  
[ ]borsuk_5__58_19.min1.thm1.tptp2017-02-06 16:57 563  
[ ]borsuk_5__62_52.min1.thm1.tptp2017-02-06 16:57 553  
[ ]calcul_2__137_41.min1.thm1.tptp2017-02-06 16:57 557  
[ ]card_1__855_29.min1.thm1.tptp2017-02-06 16:57 382  
[ ]card_1__904_21.min1.thm1.tptp2017-02-06 16:57 343  
[ ]card_2__778_21.min1.thm1.tptp2017-02-06 16:57 500  
[ ]card_2__784_40.min1.thm1.tptp2017-02-06 16:57 490  
[ ]card_2__1032_23.min1.thm1.tptp2017-02-06 16:57 382  
[ ]card_3__573_23.min1.thm1.tptp2017-02-06 16:57 382  
[ ]card_3__575_19.min1.thm1.tptp2017-02-06 16:57 482  
[ ]card_3__580_35.min1.thm1.tptp2017-02-06 16:57 472  
[ ]card_3__586_18.min1.thm1.tptp2017-02-06 16:57 339  
[ ]card_5__1333_22.min1.thm1.tptp2017-02-06 16:57 507  
[ ]card_fil__1479_32.min1.thm1.tptp2017-02-06 16:57 417  
[ ]card_fil__1485_25.min1.thm1.tptp2017-02-06 16:57 406  
[ ]card_fin__776_18.min1.thm1.tptp2017-02-06 16:57 371  
[ ]card_fin__823_19.min1.thm1.tptp2017-02-06 16:57 371  
[ ]card_fin__962_18.min1.thm1.tptp2017-02-06 16:57 371  
[ ]card_fin__967_19.min1.thm1.tptp2017-02-06 16:57 721  
[ ]catalg_1__236_18.min1.thm1.tptp2017-02-06 16:57 618  
[ ]catalg_1__300_18.min1.thm1.tptp2017-02-06 16:57 618  
[ ]catalg_1__450_65.min1.thm1.tptp2017-02-06 16:57 616  
[ ]catalg_1__478_65.min1.thm1.tptp2017-02-06 16:57 616  
[ ]catalg_1__908_51.min1.thm1.tptp2017-02-06 16:57 442  
[ ]cgames_1__1123_16.min1.thm1.tptp2017-02-06 16:57 629  
[ ]cgames_1__2010_22.min1.thm1.tptp2017-02-06 16:57 602  
[ ]circcomb__174_30.min1.thm1.tptp2017-02-06 16:57 420  
[ ]circtrm1__301_48.min1.thm1.tptp2017-02-06 16:57 448  
[ ]circtrm1__306_14.min1.thm1.tptp2017-02-06 16:57 440  
[ ]circtrm1__334_52.min1.thm1.tptp2017-02-06 16:57 516  
[ ]circtrm1__339_14.min1.thm1.tptp2017-02-06 16:57 508  
[ ]classes1__573_40.min1.thm1.tptp2017-02-06 16:57 441  
[ ]classes1__706_44.min1.thm1.tptp2017-02-06 16:57 457  
[ ]classes1__714_44.min1.thm1.tptp2017-02-06 16:57 483  
[ ]classes1__1533_25.min1.thm1.tptp2017-02-06 16:57 390  
[ ]coh_sp__407_24.min1.thm1.tptp2017-02-06 16:57 387  
[ ]cohsp_1__407_34.min1.thm1.tptp2017-02-06 16:57 441  
[ ]cohsp_1__3781_42.min1.thm1.tptp2017-02-06 16:57 510  
[ ]combgras__1502_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]combgras__1510_31.min1.thm1.tptp2017-02-06 16:57 468  
[ ]compact1__575_46.min1.thm1.tptp2017-02-06 16:57 478  
[ ]compact1__926_18.min1.thm1.tptp2017-02-06 16:57 481  
[ ]compos_1__1316_10.min1.thm1.tptp2017-02-06 16:57 576  
[ ]compos_1__1394_10.min1.thm1.tptp2017-02-06 16:57 624  
[ ]comput_1__3478_68.min1.thm1.tptp2017-02-06 16:57 2.0K 
[ ]cqc_lang__73_8.min1.thm1.tptp2017-02-06 16:57 535  
[ ]cqc_sim1__2433_55.min1.thm1.tptp2017-02-06 16:57 767  
[ ]cqc_the1__54_19.min1.thm1.tptp2017-02-06 16:57 477  
[ ]cqc_the1__60_38.min1.thm1.tptp2017-02-06 16:57 477  
[ ]dickson__2479_28.min1.thm1.tptp2017-02-06 16:57 575  
[ ]dickson__2483_16.min1.thm1.tptp2017-02-06 16:57 573  
[ ]dickson__2606_30.min1.thm1.tptp2017-02-06 16:57 655  
[ ]dickson__2610_18.min1.thm1.tptp2017-02-06 16:57 653  
[ ]dickson__3283_18.min1.thm1.tptp2017-02-06 16:57 428  
[ ]dickson__3376_20.min1.thm1.tptp2017-02-06 16:57 445  
[ ]dickson__3782_24.min1.thm1.tptp2017-02-06 16:57 465  
[ ]dilworth__103_24.min1.thm1.tptp2017-02-06 16:57 391  
[ ]dilworth__320_16.min1.thm1.tptp2017-02-06 16:57 424  
[ ]dilworth__333_16.min1.thm1.tptp2017-02-06 16:57 856  
[ ]dilworth__386_16.min1.thm1.tptp2017-02-06 16:57 424  
[ ]dilworth__399_16.min1.thm1.tptp2017-02-06 16:57 856  
[ ]dilworth__2233_25.min1.thm1.tptp2017-02-06 16:57 556  
[ ]dilworth__2690_21.min1.thm1.tptp2017-02-06 16:57 780  
[ ]dilworth__3178_24.min1.thm1.tptp2017-02-06 16:57 584  
[ ]dilworth__3434_18.min1.thm1.tptp2017-02-06 16:57 573  
[ ]dtconstr__381_38.min1.thm1.tptp2017-02-06 16:57 540  
[ ]dtconstr__527_38.min1.thm1.tptp2017-02-06 16:57 522  
[ ]dtconstr__867_10.min1.thm1.tptp2017-02-06 16:57 528  
[ ]dtconstr__903_38.min1.thm1.tptp2017-02-06 16:57 526  
[ ]dtconstr__1346_36.min1.thm1.tptp2017-02-06 16:57 564  
[ ]enumset1__224_53.min1.thm1.tptp2017-02-06 16:57 600  
[ ]enumset1__237_59.min1.thm1.tptp2017-02-06 16:57 668  
[ ]enumset1__258_65.min1.thm1.tptp2017-02-06 16:57 732  
[ ]enumset1__337_77.min1.thm1.tptp2017-02-06 16:57 868  
[ ]eqrel_1__1759_65.min1.thm1.tptp2017-02-06 16:57 655  
[ ]euclid_7__581_30.min1.thm1.tptp2017-02-06 16:57 410  
[ ]facirc_1__142_28.min1.thm1.tptp2017-02-06 16:57 401  
[ ]facirc_1__361_77.min1.thm1.tptp2017-02-06 16:57 594  
[ ]facirc_1__1293_17.min1.thm1.tptp2017-02-06 16:57 683  
[ ]fcont_3__1032_39.min1.thm1.tptp2017-02-06 16:57 663  
[ ]fcont_3__1394_39.min1.thm1.tptp2017-02-06 16:57 665  
[ ]filter_0__372_21.min1.thm1.tptp2017-02-06 16:57 461  
[ ]filter_0__382_29.min1.thm1.tptp2017-02-06 16:57 524  
[ ]filter_0__395_31.min1.thm1.tptp2017-02-06 16:57 534  
[ ]filter_0__402_31.min1.thm1.tptp2017-02-06 16:57 536  
[ ]filter_0__416_29.min1.thm1.tptp2017-02-06 16:57 524  
[ ]filter_0__427_29.min1.thm1.tptp2017-02-06 16:57 524  
[ ]filter_0__444_26.min1.thm1.tptp2017-02-06 16:57 414  
[ ]finseq_1__200_38.min1.thm1.tptp2017-02-06 16:57 480  
[ ]finseq_3__612_30.min1.thm1.tptp2017-02-06 16:57 381  
[ ]finseq_3__660_30.min1.thm1.tptp2017-02-06 16:57 381  
[ ]finseq_3__1112_18.min1.thm1.tptp2017-02-06 16:57 484  
[ ]finseq_3__1315_18.min1.thm1.tptp2017-02-06 16:57 556  
[ ]finseq_3__1826_22.min1.thm1.tptp2017-02-06 16:57 556  
[ ]finseq_3__1834_27.min1.thm1.tptp2017-02-06 16:57 477  
[ ]finseq_3__1838_27.min1.thm1.tptp2017-02-06 16:57 489  
[ ]finseq_3__1847_20.min1.thm1.tptp2017-02-06 16:57 550  
[ ]finseq_5__1444_27.min1.thm1.tptp2017-02-06 16:57 381  
[ ]finseq_6__2083_39.min1.thm1.tptp2017-02-06 16:57 532  
[ ]finset_1__992_29.min1.thm1.tptp2017-02-06 16:57 460  
[ ]finset_1__1012_34.min1.thm1.tptp2017-02-06 16:57 462  
[ ]finset_1__1050_29.min1.thm1.tptp2017-02-06 16:57 460  
[ ]finset_1__1070_34.min1.thm1.tptp2017-02-06 16:57 462  
[ ]finset_1__1611_26.min1.thm1.tptp2017-02-06 16:57 410  
[ ]fintopo5__1324_18.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]fintopo5__1354_69.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]fomodel0__1926_40.min1.thm1.tptp2017-02-06 16:57 654  
[ ]fomodel0__1927_55.min1.thm1.tptp2017-02-06 16:57 525  
[ ]fomodel1__871_55.min1.thm1.tptp2017-02-06 16:57 696  
[ ]fomodel1__1496_2.min1.thm1.tptp2017-02-06 16:57 569  
[ ]fomodel1__1583_24.min1.thm1.tptp2017-02-06 16:57 575  
[ ]fomodel2__3625_42.min1.thm1.tptp2017-02-06 16:57 497  
[ ]fomodel2__3909_57.min1.thm1.tptp2017-02-06 16:57 429  
[ ]fomodel3__106_32.min1.thm1.tptp2017-02-06 16:57 654  
[ ]fraenkel__696_35.min1.thm1.tptp2017-02-06 16:57 440  
[ ]frechet__733_26.min1.thm1.tptp2017-02-06 16:57 393  
[ ]frechet__796_21.min1.thm1.tptp2017-02-06 16:57 404  
[ ]frechet__805_34.min1.thm1.tptp2017-02-06 16:57 421  
[ ]frechet__851_25.min1.thm1.tptp2017-02-06 16:57 391  
[ ]frechet__853_43.min1.thm1.tptp2017-02-06 16:57 484  
[ ]frechet__872_39.min1.thm1.tptp2017-02-06 16:57 476  
[ ]frechet__1478_35.min1.thm1.tptp2017-02-06 16:57 372  
[ ]frechet__1564_36.min1.thm1.tptp2017-02-06 16:57 455  
[ ]frechet__1711_43.min1.thm1.tptp2017-02-06 16:57 417  
[ ]frechet__1800_36.min1.thm1.tptp2017-02-06 16:57 401  
[ ]frechet__1954_19.min1.thm1.tptp2017-02-06 16:57 445  
[ ]frechet__2009_39.min1.thm1.tptp2017-02-06 16:57 435  
[ ]frechet__2311_49.min1.thm1.tptp2017-02-06 16:57 673  
[ ]fsm_1__4383_35.min1.thm1.tptp2017-02-06 16:57 378  
[ ]fsm_1__4435_33.min1.thm1.tptp2017-02-06 16:57 394  
[ ]funct_4__275_31.min1.thm1.tptp2017-02-06 16:57 385  
[ ]funct_4__291_17.min1.thm1.tptp2017-02-06 16:57 607  
[ ]funct_4__297_43.min1.thm1.tptp2017-02-06 16:57 449  
[ ]funct_4__379_17.min1.thm1.tptp2017-02-06 16:57 437  
[ ]funct_4__582_17.min1.thm1.tptp2017-02-06 16:57 381  
[ ]funct_4__1471_33.min1.thm1.tptp2017-02-06 16:57 443  
[ ]funct_4__1526_44.min1.thm1.tptp2017-02-06 16:57 551  
[ ]funct_5__1557_34.min1.thm1.tptp2017-02-06 16:57 411  
[ ]funct_7__202_23.min1.thm1.tptp2017-02-06 16:57 482  
[ ]funct_7__280_37.min1.thm1.tptp2017-02-06 16:57 534  
[ ]funct_7__283_21.min1.thm1.tptp2017-02-06 16:57 561  
[ ]funct_7__288_37.min1.thm1.tptp2017-02-06 16:57 551  
[ ]funct_7__290_33.min1.thm1.tptp2017-02-06 16:57 524  
[ ]funct_7__299_42.min1.thm1.tptp2017-02-06 16:57 551  
[ ]funct_7__3310_19.min1.thm1.tptp2017-02-06 16:57 508  
[ ]funct_7__3330_33.min1.thm1.tptp2017-02-06 16:57 476  
[ ]fvsum_1__1055_25.min1.thm1.tptp2017-02-06 16:57 418  
[ ]gcd_1__880_18.min1.thm1.tptp2017-02-06 16:57 461  
[ ]glib_000__1843_22.min1.thm1.tptp2017-02-06 16:57 580  
[ ]glib_001__4735_52.min1.thm1.tptp2017-02-06 16:57 689  
[ ]glib_001__4740_52.min1.thm1.tptp2017-02-06 16:57 876  
[ ]glib_001__4748_30.min1.thm1.tptp2017-02-06 16:57 949  
[ ]glib_001__6574_33.min1.thm1.tptp2017-02-06 16:57 449  
[ ]glib_001__6583_37.min1.thm1.tptp2017-02-06 16:57 461  
[ ]glib_001__6699_18.min1.thm1.tptp2017-02-06 16:57 537  
[ ]glib_001__6736_47.min1.thm1.tptp2017-02-06 16:57 465  
[ ]glib_001__8627_18.min1.thm1.tptp2017-02-06 16:57 537  
[ ]glib_001__8632_32.min1.thm1.tptp2017-02-06 16:57 465  
[ ]glib_001__8719_32.min1.thm1.tptp2017-02-06 16:57 618  
[ ]glib_004__77_28.min1.thm1.tptp2017-02-06 16:57 384  
[ ]glib_004__106_19.min1.thm1.tptp2017-02-06 16:57 385  
[ ]glib_004__4350_42.min1.thm1.tptp2017-02-06 16:57 651  
[ ]glib_005__1703_36.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]glib_005__1825_36.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]graph_1__149_25.min1.thm1.tptp2017-02-06 16:57 410  
[ ]graph_1__180_18.min1.thm1.tptp2017-02-06 16:57 402  
[ ]graph_1__210_25.min1.thm1.tptp2017-02-06 16:57 410  
[ ]graph_1__242_18.min1.thm1.tptp2017-02-06 16:57 402  
[ ]graph_1__2224_37.min1.thm1.tptp2017-02-06 16:57 443  
[ ]graph_2__238_20.min1.thm1.tptp2017-02-06 16:57 518  
[ ]graph_2__869_32.min1.thm1.tptp2017-02-06 16:57 529  
[ ]graph_2__909_34.min1.thm1.tptp2017-02-06 16:57 543  
[ ]graph_2__915_31.min1.thm1.tptp2017-02-06 16:57 447  
[ ]graph_2__922_22.min1.thm1.tptp2017-02-06 16:57 438  
[ ]graph_2__926_23.min1.thm1.tptp2017-02-06 16:57 485  
[ ]graph_2__3221_30.min1.thm1.tptp2017-02-06 16:57 535  
[ ]graph_2__3533_30.min1.thm1.tptp2017-02-06 16:57 540  
[ ]graph_3__1923_45.min1.thm1.tptp2017-02-06 16:57 466  
[ ]graph_3__1927_45.min1.thm1.tptp2017-02-06 16:57 448  
[ ]graph_3__1932_16.min1.thm1.tptp2017-02-06 16:57 525  
[ ]graph_3__1986_44.min1.thm1.tptp2017-02-06 16:57 466  
[ ]graph_3__1990_44.min1.thm1.tptp2017-02-06 16:57 448  
[ ]graph_3__1995_16.min1.thm1.tptp2017-02-06 16:57 525  
[ ]graph_3__2457_45.min1.thm1.tptp2017-02-06 16:57 672  
[ ]graph_3__2491_45.min1.thm1.tptp2017-02-06 16:57 672  
[ ]graph_3__2536_41.min1.thm1.tptp2017-02-06 16:57 648  
[ ]graph_3__2551_20.min1.thm1.tptp2017-02-06 16:57 737  
[ ]graph_4__256_19.min1.thm1.tptp2017-02-06 16:57 471  
[ ]graph_4__1293_30.min1.thm1.tptp2017-02-06 16:57 535  
[ ]graph_4__1297_18.min1.thm1.tptp2017-02-06 16:57 533  
[ ]graph_4__1484_30.min1.thm1.tptp2017-02-06 16:57 540  
[ ]graph_4__1488_18.min1.thm1.tptp2017-02-06 16:57 538  
[ ]graph_5__1583_16.min1.thm1.tptp2017-02-06 16:57 583  
[ ]groeb_1__1492_28.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]groeb_1__1523_28.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]groeb_2__315_31.min1.thm1.tptp2017-02-06 16:57 405  
[ ]group_2__2896_29.min1.thm1.tptp2017-02-06 16:57 428  
[ ]group_2__2905_29.min1.thm1.tptp2017-02-06 16:57 428  
[ ]group_2__2916_24.min1.thm1.tptp2017-02-06 16:57 428  
[ ]group_2__2920_27.min1.thm1.tptp2017-02-06 16:57 453  
[ ]group_2__2942_24.min1.thm1.tptp2017-02-06 16:57 463  
[ ]group_2__2943_24.min1.thm1.tptp2017-02-06 16:57 429  
[ ]group_9__7495_16.min1.thm1.tptp2017-02-06 16:57 526  
[ ]group_9__8258_37.min1.thm1.tptp2017-02-06 16:57 563  
[ ]group_10__1955_30.min1.thm1.tptp2017-02-06 16:57 509  
[ ]group_10__1965_16.min1.thm1.tptp2017-02-06 16:57 594  
[ ]hallmar1__256_21.min1.thm1.tptp2017-02-06 16:57 545  
[ ]hallmar1__268_16.min1.thm1.tptp2017-02-06 16:57 514  
[ ]hallmar1__378_21.min1.thm1.tptp2017-02-06 16:57 537  
[ ]hallmar1__392_27.min1.thm1.tptp2017-02-06 16:57 420  
[ ]hallmar1__1381_27.min1.thm1.tptp2017-02-06 16:57 422  
[ ]hallmar1__1383_49.min1.thm1.tptp2017-02-06 16:57 590  
[ ]hallmar1__1384_75.min1.thm1.tptp2017-02-06 16:57 726  
[ ]hallmar1__1462_38.min1.thm1.tptp2017-02-06 16:57 485  
[ ]hallmar1__1464_42.min1.thm1.tptp2017-02-06 16:57 483  
[ ]heyting1__324_28.min1.thm1.tptp2017-02-06 16:57 400  
[ ]heyting1__343_25.min1.thm1.tptp2017-02-06 16:57 410  
[ ]heyting3__755_21.min1.thm1.tptp2017-02-06 16:57 550  
[ ]heyting3__760_21.min1.thm1.tptp2017-02-06 16:57 652  
[ ]heyting3__766_14.min1.thm1.tptp2017-02-06 16:57 712  
[ ]hilbasis__312_16.min1.thm1.tptp2017-02-06 16:57 441  
[ ]ideal_1__5926_34.min1.thm1.tptp2017-02-06 16:57 440  
[ ]int_7__129_20.min1.thm1.tptp2017-02-06 16:57 432  
[ ]int_7__153_29.min1.thm1.tptp2017-02-06 16:57 379  
[ ]jgraph_8__568_45.min1.thm1.tptp2017-02-06 16:57 541  
[ ]jordan1__423_60.min1.thm1.tptp2017-02-06 16:57 717  
[ ]jordan1__444_64.min1.thm1.tptp2017-02-06 16:57 717  
[ ]jordan1d__64_43.min1.thm1.tptp2017-02-06 16:57 539  
[ ]jordan1d__65_49.min1.thm1.tptp2017-02-06 16:57 583  
[ ]jordan1d__68_41.min1.thm1.tptp2017-02-06 16:57 579  
[ ]jordan21__62_31.min1.thm1.tptp2017-02-06 16:57 437  
[ ]jordan21__63_37.min1.thm1.tptp2017-02-06 16:57 479  
[ ]kolmog01__1443_66.min1.thm1.tptp2017-02-06 16:57 716  
[ ]kolmog01__1462_29.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]kolmog01__1479_64.min1.thm1.tptp2017-02-06 16:57 704  
[ ]l_hospit__1173_20.min1.thm1.tptp2017-02-06 16:57 549  
[ ]l_hospit__1216_20.min1.thm1.tptp2017-02-06 16:57 549  
[ ]l_hospit__1578_20.min1.thm1.tptp2017-02-06 16:57 549  
[ ]l_hospit__1622_20.min1.thm1.tptp2017-02-06 16:57 549  
[ ]lang1__106_51.min1.thm1.tptp2017-02-06 16:57 404  
[ ]lang1__117_17.min1.thm1.tptp2017-02-06 16:57 394  
[ ]laplace__401_16.min1.thm1.tptp2017-02-06 16:57 559  
[ ]laplace__460_21.min1.thm1.tptp2017-02-06 16:57 450  
[ ]laplace__468_21.min1.thm1.tptp2017-02-06 16:57 507  
[ ]laplace__624_38.min1.thm1.tptp2017-02-06 16:57 665  
[ ]latsum_1__137_58.min1.thm1.tptp2017-02-06 16:57 443  
[ ]latsum_1__164_50.min1.thm1.tptp2017-02-06 16:57 899  
[ ]latsum_1__211_50.min1.thm1.tptp2017-02-06 16:57 899  
[ ]latsum_1__252_69.min1.thm1.tptp2017-02-06 16:57 442  
[ ]latsum_1__255_48.min1.thm1.tptp2017-02-06 16:57 684  
[ ]latsum_1__262_46.min1.thm1.tptp2017-02-06 16:57 680  
[ ]latsum_1__276_17.min1.thm1.tptp2017-02-06 16:57 526  
[ ]latsum_1__333_55.min1.thm1.tptp2017-02-06 16:57 384  
[ ]latsum_1__423_57.min1.thm1.tptp2017-02-06 16:57 935  
[ ]latsum_1__453_47.min1.thm1.tptp2017-02-06 16:57 806  
[ ]latsum_1__515_50.min1.thm1.tptp2017-02-06 16:57 923  
[ ]latsum_1__518_14.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]latsum_1__629_50.min1.thm1.tptp2017-02-06 16:57 923  
[ ]latsum_1__632_14.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]latsum_1__730_16.min1.thm1.tptp2017-02-06 16:57 946  
[ ]latsum_1__813_59.min1.thm1.tptp2017-02-06 16:57 947  
[ ]latsum_1__815_20.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]latsum_1__829_58.min1.thm1.tptp2017-02-06 16:57 828  
[ ]latsum_1__843_60.min1.thm1.tptp2017-02-06 16:57 828  
[ ]latsum_1__893_59.min1.thm1.tptp2017-02-06 16:57 947  
[ ]latsum_1__895_20.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]latsum_1__902_60.min1.thm1.tptp2017-02-06 16:57 828  
[ ]latsum_1__922_60.min1.thm1.tptp2017-02-06 16:57 828  
[ ]lattice5__4080_42.min1.thm1.tptp2017-02-06 16:57 600  
[ ]lattice5__4116_41.min1.thm1.tptp2017-02-06 16:57 622  
[ ]lattice5__4123_43.min1.thm1.tptp2017-02-06 16:57 644  
[ ]lattice5__5465_43.min1.thm1.tptp2017-02-06 16:57 734  
[ ]lattice5__5480_45.min1.thm1.tptp2017-02-06 16:57 712  
[ ]lattice8__2818_33.min1.thm1.tptp2017-02-06 16:57 496  
[ ]lattice8__2860_32.min1.thm1.tptp2017-02-06 16:57 518  
[ ]lattice8__3995_35.min1.thm1.tptp2017-02-06 16:57 606  
[ ]lattice8__4010_37.min1.thm1.tptp2017-02-06 16:57 584  
[ ]lattice8__4138_35.min1.thm1.tptp2017-02-06 16:57 606  
[ ]lattice8__4153_37.min1.thm1.tptp2017-02-06 16:57 584  
[ ]lexbfs__109_42.min1.thm1.tptp2017-02-06 16:57 560  
[ ]lexbfs__114_42.min1.thm1.tptp2017-02-06 16:57 459  
[ ]lexbfs__119_18.min1.thm1.tptp2017-02-06 16:57 595  
[ ]lexbfs__2103_33.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]lexbfs__2133_33.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]lexbfs__2159_76.min1.thm1.tptp2017-02-06 16:57 1.9K 
[ ]lopclset__568_50.min1.thm1.tptp2017-02-06 16:57 564  
[ ]matrix11__968_25.min1.thm1.tptp2017-02-06 16:57 472  
[ ]matrix11__1474_17.min1.thm1.tptp2017-02-06 16:57 369  
[ ]matrix11__4392_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]matrix11__4432_15.min1.thm1.tptp2017-02-06 16:57 367  
[ ]matrix11__4446_15.min1.thm1.tptp2017-02-06 16:57 371  
[ ]matrix11__4596_16.min1.thm1.tptp2017-02-06 16:57 375  
[ ]matrix11__4904_32.min1.thm1.tptp2017-02-06 16:57 518  
[ ]matrix11__4919_19.min1.thm1.tptp2017-02-06 16:57 466  
[ ]matrix_7__1358_34.min1.thm1.tptp2017-02-06 16:57 419  
[ ]matrix_7__1374_42.min1.thm1.tptp2017-02-06 16:57 475  
[ ]matrix_7__1915_34.min1.thm1.tptp2017-02-06 16:57 419  
[ ]matrix_7__1931_42.min1.thm1.tptp2017-02-06 16:57 475  
[ ]matrix_7__2862_30.min1.thm1.tptp2017-02-06 16:57 458  
[ ]matrix_7__2870_29.min1.thm1.tptp2017-02-06 16:57 412  
[ ]matrix_7__2915_22.min1.thm1.tptp2017-02-06 16:57 458  
[ ]matrix_7__2926_23.min1.thm1.tptp2017-02-06 16:57 714  
[ ]matrix_9__711_14.min1.thm1.tptp2017-02-06 16:57 888  
[ ]matrix_9__716_24.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]matrlin__1028_22.min1.thm1.tptp2017-02-06 16:57 491  
[ ]matrlin__1059_20.min1.thm1.tptp2017-02-06 16:57 482  
[ ]matrtop3__210_17.min1.thm1.tptp2017-02-06 16:57 358  
[ ]matrtop3__3613_42.min1.thm1.tptp2017-02-06 16:57 500  
[ ]measure6__1037_24.min1.thm1.tptp2017-02-06 16:57 492  
[ ]measure6__1055_24.min1.thm1.tptp2017-02-06 16:57 492  
[ ]member_1__184_30.min1.thm1.tptp2017-02-06 16:57 433  
[ ]member_1__186_28.min1.thm1.tptp2017-02-06 16:57 446  
[ ]member_1__189_30.min1.thm1.tptp2017-02-06 16:57 442  
[ ]member_1__191_22.min1.thm1.tptp2017-02-06 16:57 429  
[ ]member_1__455_30.min1.thm1.tptp2017-02-06 16:57 430  
[ ]member_1__457_28.min1.thm1.tptp2017-02-06 16:57 446  
[ ]member_1__460_30.min1.thm1.tptp2017-02-06 16:57 442  
[ ]member_1__462_22.min1.thm1.tptp2017-02-06 16:57 426  
[ ]member_1__619_23.min1.thm1.tptp2017-02-06 16:57 400  
[ ]member_1__625_14.min1.thm1.tptp2017-02-06 16:57 444  
[ ]member_1__631_16.min1.thm1.tptp2017-02-06 16:57 361  
[ ]member_1__872_30.min1.thm1.tptp2017-02-06 16:57 430  
[ ]member_1__874_28.min1.thm1.tptp2017-02-06 16:57 446  
[ ]member_1__877_30.min1.thm1.tptp2017-02-06 16:57 442  
[ ]member_1__879_20.min1.thm1.tptp2017-02-06 16:57 426  
[ ]member_1__1089_25.min1.thm1.tptp2017-02-06 16:57 400  
[ ]member_1__1095_14.min1.thm1.tptp2017-02-06 16:57 508  
[ ]member_1__1101_17.min1.thm1.tptp2017-02-06 16:57 361  
[ ]member_1__1336_25.min1.thm1.tptp2017-02-06 16:57 400  
[ ]member_1__1342_14.min1.thm1.tptp2017-02-06 16:57 508  
[ ]member_1__1348_17.min1.thm1.tptp2017-02-06 16:57 361  
[ ]member_1__1900_25.min1.thm1.tptp2017-02-06 16:57 409  
[ ]member_1__1906_14.min1.thm1.tptp2017-02-06 16:57 525  
[ ]member_1__1912_17.min1.thm1.tptp2017-02-06 16:57 368  
[ ]member_1__2233_25.min1.thm1.tptp2017-02-06 16:57 409  
[ ]member_1__2239_14.min1.thm1.tptp2017-02-06 16:57 525  
[ ]member_1__2245_17.min1.thm1.tptp2017-02-06 16:57 368  
[ ]membered__821_28.min1.thm1.tptp2017-02-06 16:57 410  
[ ]membered__833_28.min1.thm1.tptp2017-02-06 16:57 410  
[ ]membered__845_28.min1.thm1.tptp2017-02-06 16:57 410  
[ ]membered__857_28.min1.thm1.tptp2017-02-06 16:57 410  
[ ]membered__869_28.min1.thm1.tptp2017-02-06 16:57 410  
[ ]membered__881_28.min1.thm1.tptp2017-02-06 16:57 410  
[ ]mesfunc4__310_29.min1.thm1.tptp2017-02-06 16:57 495  
[ ]mesfunc4__316_22.min1.thm1.tptp2017-02-06 16:57 581  
[ ]mfold_2__1506_18.min1.thm1.tptp2017-02-06 16:57 489  
[ ]modelc_3__50_57.min1.thm1.tptp2017-02-06 16:57 514  
[ ]modelc_3__51_17.min1.thm1.tptp2017-02-06 16:57 685  
[ ]modelc_3__529_43.min1.thm1.tptp2017-02-06 16:57 672  
[ ]modelc_3__542_31.min1.thm1.tptp2017-02-06 16:57 605  
[ ]modelc_3__688_32.min1.thm1.tptp2017-02-06 16:57 442  
[ ]modelc_3__709_56.min1.thm1.tptp2017-02-06 16:57 681  
[ ]modelc_3__3530_73.min1.thm1.tptp2017-02-06 16:57 849  
[ ]modelc_3__3552_10.min1.thm1.tptp2017-02-06 16:57 861  
[ ]modelc_3__3624_18.min1.thm1.tptp2017-02-06 16:57 873  
[ ]modelc_3__3634_18.min1.thm1.tptp2017-02-06 16:57 873  
[ ]modelc_3__5188_53.min1.thm1.tptp2017-02-06 16:57 916  
[ ]modelc_3__6071_46.min1.thm1.tptp2017-02-06 16:57 645  
[ ]moebius1__1601_16.min1.thm1.tptp2017-02-06 16:57 510  
[ ]msscyc_1__262_32.min1.thm1.tptp2017-02-06 16:57 436  
[ ]msscyc_1__265_37.min1.thm1.tptp2017-02-06 16:57 436  
[ ]msscyc_1__277_37.min1.thm1.tptp2017-02-06 16:57 436  
[ ]msscyc_1__292_37.min1.thm1.tptp2017-02-06 16:57 436  
[ ]msualg_6__1526_33.min1.thm1.tptp2017-02-06 16:57 526  
[ ]mycielsk__130_51.min1.thm1.tptp2017-02-06 16:57 639  
[ ]mycielsk__131_57.min1.thm1.tptp2017-02-06 16:57 673  
[ ]mycielsk__136_22.min1.thm1.tptp2017-02-06 16:57 346  
[ ]mycielsk__137_27.min1.thm1.tptp2017-02-06 16:57 402  
[ ]mycielsk__143_27.min1.thm1.tptp2017-02-06 16:57 402  
[ ]mycielsk__1452_29.min1.thm1.tptp2017-02-06 16:57 448  
[ ]mycielsk__2622_21.min1.thm1.tptp2017-02-06 16:57 630  
[ ]mycielsk__2685_36.min1.thm1.tptp2017-02-06 16:57 700  
[ ]mycielsk__2704_36.min1.thm1.tptp2017-02-06 16:57 726  
[ ]mycielsk__2710_33.min1.thm1.tptp2017-02-06 16:57 583  
[ ]mycielsk__2719_21.min1.thm1.tptp2017-02-06 16:57 632  
[ ]mycielsk__2938_20.min1.thm1.tptp2017-02-06 16:57 533  
[ ]nagata_2__1106_30.min1.thm1.tptp2017-02-06 16:57 372  
[ ]nagata_2__2042_35.min1.thm1.tptp2017-02-06 16:57 728  
[ ]nagata_2__2280_30.min1.thm1.tptp2017-02-06 16:57 956  
[ ]nagata_2__2704_39.min1.thm1.tptp2017-02-06 16:57 904  
[ ]nat_3__745_17.min1.thm1.tptp2017-02-06 16:57 419  
[ ]nat_3__857_17.min1.thm1.tptp2017-02-06 16:57 419  
[ ]nat_4__2644_26.min1.thm1.tptp2017-02-06 16:57 423  
[ ]nat_4__2975_24.min1.thm1.tptp2017-02-06 16:57 521  
[ ]nat_4__3009_32.min1.thm1.tptp2017-02-06 16:57 519  
[ ]nat_4__4425_28.min1.thm1.tptp2017-02-06 16:57 563  
[ ]nat_4__4518_26.min1.thm1.tptp2017-02-06 16:57 568  
[ ]nat_4__4915_20.min1.thm1.tptp2017-02-06 16:57 561  
[ ]nat_4__4944_30.min1.thm1.tptp2017-02-06 16:57 559  
[ ]nat_5__2205_57.min1.thm1.tptp2017-02-06 16:57 506  
[ ]nat_5__2212_57.min1.thm1.tptp2017-02-06 16:57 523  
[ ]nat_5__2217_20.min1.thm1.tptp2017-02-06 16:57 601  
[ ]neckla_2__948_31.min1.thm1.tptp2017-02-06 16:57 586  
[ ]neckla_2__1012_20.min1.thm1.tptp2017-02-06 16:57 578  
[ ]neckla_2__1456_20.min1.thm1.tptp2017-02-06 16:57 578  
[ ]neckla_3__818_56.min1.thm1.tptp2017-02-06 16:57 424  
[ ]neckla_3__860_56.min1.thm1.tptp2017-02-06 16:57 424  
[ ]neckla_3__923_18.min1.thm1.tptp2017-02-06 16:57 474  
[ ]neckla_3__962_18.min1.thm1.tptp2017-02-06 16:57 474  
[ ]neckla_3__1017_50.min1.thm1.tptp2017-02-06 16:57 864  
[ ]neckla_3__1018_18.min1.thm1.tptp2017-02-06 16:57 924  
[ ]neckla_3__1092_50.min1.thm1.tptp2017-02-06 16:57 864  
[ ]neckla_3__1093_18.min1.thm1.tptp2017-02-06 16:57 924  
[ ]neckla_3__1653_34.min1.thm1.tptp2017-02-06 16:57 438  
[ ]neckla_3__1654_45.min1.thm1.tptp2017-02-06 16:57 535  
[ ]neckla_3__2536_38.min1.thm1.tptp2017-02-06 16:57 629  
[ ]neckla_3__4111_30.min1.thm1.tptp2017-02-06 16:57 710  
[ ]neckla_3__4116_21.min1.thm1.tptp2017-02-06 16:57 494  
[ ]neckla_3__4124_16.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]neckla_3__4674_14.min1.thm1.tptp2017-02-06 16:57 705  
[ ]neckla_3__4871_68.min1.thm1.tptp2017-02-06 16:57 541  
[ ]neckla_3__5461_23.min1.thm1.tptp2017-02-06 16:57 372  
[ ]neckla_3__5471_16.min1.thm1.tptp2017-02-06 16:57 406  
[ ]neckla_3__5518_23.min1.thm1.tptp2017-02-06 16:57 467  
[ ]neckla_3__5525_23.min1.thm1.tptp2017-02-06 16:57 439  
[ ]neckla_3__5531_16.min1.thm1.tptp2017-02-06 16:57 514  
[ ]neckla_3__5553_23.min1.thm1.tptp2017-02-06 16:57 372  
[ ]neckla_3__5563_16.min1.thm1.tptp2017-02-06 16:57 406  
[ ]neckla_3__5811_65.min1.thm1.tptp2017-02-06 16:57 440  
[ ]neckla_3__5866_61.min1.thm1.tptp2017-02-06 16:57 413  
[ ]neckla_3__5929_20.min1.thm1.tptp2017-02-06 16:57 776  
[ ]neckla_3__5975_20.min1.thm1.tptp2017-02-06 16:57 776  
[ ]neckla_3__6296_20.min1.thm1.tptp2017-02-06 16:57 776  
[ ]neckla_3__6342_20.min1.thm1.tptp2017-02-06 16:57 776  
[ ]neckla_3__6560_55.min1.thm1.tptp2017-02-06 16:57 600  
[ ]neckla_3__6565_27.min1.thm1.tptp2017-02-06 16:57 481  
[ ]necklace__219_35.min1.thm1.tptp2017-02-06 16:57 400  
[ ]necklace__947_41.min1.thm1.tptp2017-02-06 16:57 458  
[ ]necklace__963_38.min1.thm1.tptp2017-02-06 16:57 405  
[ ]necklace__971_38.min1.thm1.tptp2017-02-06 16:57 405  
[ ]newton__85_73.min1.thm1.tptp2017-02-06 16:57 533  
[ ]newton__924_18.min1.thm1.tptp2017-02-06 16:57 578  
[ ]numbers__798_36.min1.thm1.tptp2017-02-06 16:57 328  
[ ]numbers__800_37.min1.thm1.tptp2017-02-06 16:57 363  
[ ]openlatt__463_46.min1.thm1.tptp2017-02-06 16:57 554  
[ ]orders_4__365_20.min1.thm1.tptp2017-02-06 16:57 488  
[ ]ordinal1__74_27.min1.thm1.tptp2017-02-06 16:57 403  
[ ]ordinal1__76_30.min1.thm1.tptp2017-02-06 16:57 403  
[ ]ordinal4__179_25.min1.thm1.tptp2017-02-06 16:57 388  
[ ]ordinal6__249_16.min1.thm1.tptp2017-02-06 16:57 448  
[ ]partfun1__82_31.min1.thm1.tptp2017-02-06 16:57 437  
[ ]partfun2__1179_16.min1.thm1.tptp2017-02-06 16:57 398  
[ ]partit1__2153_17.min1.thm1.tptp2017-02-06 16:57 473  
[ ]partit_2__840_56.min1.thm1.tptp2017-02-06 16:57 542  
[ ]pboole__344_27.min1.thm1.tptp2017-02-06 16:57 554  
[ ]pboole__500_27.min1.thm1.tptp2017-02-06 16:57 409  
[ ]pcs_0__2972_37.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]pencil_3__946_23.min1.thm1.tptp2017-02-06 16:57 427  
[ ]pencil_3__958_16.min1.thm1.tptp2017-02-06 16:57 460  
[ ]pencil_4__1402_18.min1.thm1.tptp2017-02-06 16:57 375  
[ ]pencil_4__1415_18.min1.thm1.tptp2017-02-06 16:57 373  
[ ]pnproc_1__2761_51.min1.thm1.tptp2017-02-06 16:57 577  
[ ]polynom2__186_55.min1.thm1.tptp2017-02-06 16:57 410  
[ ]polynom3__735_34.min1.thm1.tptp2017-02-06 16:57 480  
[ ]polynom3__738_34.min1.thm1.tptp2017-02-06 16:57 480  
[ ]polynom3__789_33.min1.thm1.tptp2017-02-06 16:57 490  
[ ]polynom6__83_18.min1.thm1.tptp2017-02-06 16:57 397  
[ ]polynom6__98_47.min1.thm1.tptp2017-02-06 16:57 429  
[ ]polynom6__120_25.min1.thm1.tptp2017-02-06 16:57 366  
[ ]polynom6__232_20.min1.thm1.tptp2017-02-06 16:57 511  
[ ]polyred__3402_20.min1.thm1.tptp2017-02-06 16:57 1.4K 
[ ]polyred__3485_20.min1.thm1.tptp2017-02-06 16:57 923  
[ ]polyred__4371_36.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]pre_poly__2529_23.min1.thm1.tptp2017-02-06 16:57 416  
[ ]pre_poly__2535_23.min1.thm1.tptp2017-02-06 16:57 416  
[ ]pre_poly__2574_48.min1.thm1.tptp2017-02-06 16:57 460  
[ ]pre_poly__2583_31.min1.thm1.tptp2017-02-06 16:57 399  
[ ]pre_poly__3483_36.min1.thm1.tptp2017-02-06 16:57 499  
[ ]pre_poly__4411_29.min1.thm1.tptp2017-02-06 16:57 398  
[ ]prob_4__66_19.min1.thm1.tptp2017-02-06 16:57 555  
[ ]prob_4__70_43.min1.thm1.tptp2017-02-06 16:57 545  
[ ]qc_lang2__1462_19.min1.thm1.tptp2017-02-06 16:57 542  
[ ]qc_lang2__1500_50.min1.thm1.tptp2017-02-06 16:57 524  
[ ]qc_lang2__1504_19.min1.thm1.tptp2017-02-06 16:57 692  
[ ]qc_lang2__1557_19.min1.thm1.tptp2017-02-06 16:57 574  
[ ]ramsey_1__1713_22.min1.thm1.tptp2017-02-06 16:57 788  
[ ]ramsey_1__1768_25.min1.thm1.tptp2017-02-06 16:57 649  
[ ]rat_1__275_37.min1.thm1.tptp2017-02-06 16:57 394  
[ ]recdef_2__237_36.min1.thm1.tptp2017-02-06 16:57 532  
[ ]recdef_2__339_47.min1.thm1.tptp2017-02-06 16:57 650  
[ ]relat_1__401_24.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]relat_1__1380_23.min1.thm1.tptp2017-02-06 16:57 385  
[ ]relat_1__1400_18.min1.thm1.tptp2017-02-06 16:57 346  
[ ]relat_1__1727_19.min1.thm1.tptp2017-02-06 16:57 664  
[ ]relat_1__1990_25.min1.thm1.tptp2017-02-06 16:57 400  
[ ]relat_1__1992_32.min1.thm1.tptp2017-02-06 16:57 512  
[ ]relat_1__1997_16.min1.thm1.tptp2017-02-06 16:57 504  
[ ]relat_1__2009_20.min1.thm1.tptp2017-02-06 16:57 361  
[ ]relat_1__2341_25.min1.thm1.tptp2017-02-06 16:57 400  
[ ]relat_1__2343_30.min1.thm1.tptp2017-02-06 16:57 512  
[ ]relat_1__2348_16.min1.thm1.tptp2017-02-06 16:57 504  
[ ]relat_1__2360_20.min1.thm1.tptp2017-02-06 16:57 361  
[ ]relat_2__451_30.min1.thm1.tptp2017-02-06 16:57 430  
[ ]relat_2__585_30.min1.thm1.tptp2017-02-06 16:57 430  
[ ]relat_2__962_4.min1.thm1.tptp2017-02-06 16:57 718  
[ ]relset_2__105_23.min1.thm1.tptp2017-02-06 16:57 391  
[ ]relset_2__117_16.min1.thm1.tptp2017-02-06 16:57 354  
[ ]relset_2__268_19.min1.thm1.tptp2017-02-06 16:57 512  
[ ]relset_2__273_14.min1.thm1.tptp2017-02-06 16:57 504  
[ ]rfunct_1__1767_22.min1.thm1.tptp2017-02-06 16:57 365  
[ ]rfunct_1__2561_18.min1.thm1.tptp2017-02-06 16:57 413  
[ ]rfunct_1__2610_18.min1.thm1.tptp2017-02-06 16:57 413  
[ ]rlaffin2__761_36.min1.thm1.tptp2017-02-06 16:57 478  
[ ]rlaffin2__776_43.min1.thm1.tptp2017-02-06 16:57 534  
[ ]rlvect_5__1652_32.min1.thm1.tptp2017-02-06 16:57 436  
[ ]rlvect_5__1660_32.min1.thm1.tptp2017-02-06 16:57 436  
[ ]rlvect_5__1692_26.min1.thm1.tptp2017-02-06 16:57 404  
[ ]rusub_4__842_32.min1.thm1.tptp2017-02-06 16:57 427  
[ ]rusub_4__850_32.min1.thm1.tptp2017-02-06 16:57 427  
[ ]rusub_4__880_26.min1.thm1.tptp2017-02-06 16:57 395  
[ ]scmbsort__244_39.min1.thm1.tptp2017-02-06 16:57 570  
[ ]scmfsa_2__321_14.min1.thm1.tptp2017-02-06 16:57 482  
[ ]scmfsa_2__984_13.min1.thm1.tptp2017-02-06 16:57 431  
[ ]scmfsa_i__90_14.min1.thm1.tptp2017-02-06 16:57 441  
[ ]scmfsa_i__93_14.min1.thm1.tptp2017-02-06 16:57 393  
[ ]scmfsa_i__402_18.min1.thm1.tptp2017-02-06 16:57 482  
[ ]scmfsa_m__345_38.min1.thm1.tptp2017-02-06 16:57 466  
[ ]scmfsa_m__1131_31.min1.thm1.tptp2017-02-06 16:57 361  
[ ]scmyciel__783_24.min1.thm1.tptp2017-02-06 16:57 410  
[ ]scmyciel__2779_29.min1.thm1.tptp2017-02-06 16:57 456  
[ ]scmyciel__3587_35.min1.thm1.tptp2017-02-06 16:57 477  
[ ]scmyciel__3669_30.min1.thm1.tptp2017-02-06 16:57 453  
[ ]scmyciel__3707_17.min1.thm1.tptp2017-02-06 16:57 741  
[ ]scmyciel__3761_34.min1.thm1.tptp2017-02-06 16:57 445  
[ ]scmyciel__3771_34.min1.thm1.tptp2017-02-06 16:57 497  
[ ]scmyciel__3802_36.min1.thm1.tptp2017-02-06 16:57 505  
[ ]scmyciel__3814_14.min1.thm1.tptp2017-02-06 16:57 713  
[ ]scmyciel__3957_42.min1.thm1.tptp2017-02-06 16:57 584  
[ ]scmyciel__4054_32.min1.thm1.tptp2017-02-06 16:57 410  
[ ]scmyciel__4073_14.min1.thm1.tptp2017-02-06 16:57 613  
[ ]scmyciel__4591_55.min1.thm1.tptp2017-02-06 16:57 739  
[ ]scmyciel__4619_30.min1.thm1.tptp2017-02-06 16:57 443  
[ ]scmyciel__4756_23.min1.thm1.tptp2017-02-06 16:57 603  
[ ]scmyciel__4758_27.min1.thm1.tptp2017-02-06 16:57 498  
[ ]scmyciel__4761_27.min1.thm1.tptp2017-02-06 16:57 531  
[ ]scmyciel__4766_21.min1.thm1.tptp2017-02-06 16:57 593  
[ ]scmyciel__4770_33.min1.thm1.tptp2017-02-06 16:57 486  
[ ]scmyciel__4800_34.min1.thm1.tptp2017-02-06 16:57 480  
[ ]scmyciel__4841_27.min1.thm1.tptp2017-02-06 16:57 482  
[ ]scmyciel__4848_27.min1.thm1.tptp2017-02-06 16:57 519  
[ ]scmyciel__4855_45.min1.thm1.tptp2017-02-06 16:57 583  
[ ]scmyciel__5037_18.min1.thm1.tptp2017-02-06 16:57 587  
[ ]scmyciel__5075_30.min1.thm1.tptp2017-02-06 16:57 419  
[ ]scmyciel__5077_35.min1.thm1.tptp2017-02-06 16:57 639  
[ ]scmyciel__5088_30.min1.thm1.tptp2017-02-06 16:57 639  
[ ]scmyciel__5092_35.min1.thm1.tptp2017-02-06 16:57 450  
[ ]scmyciel__5105_22.min1.thm1.tptp2017-02-06 16:57 735  
[ ]scmyciel__5119_29.min1.thm1.tptp2017-02-06 16:57 536  
[ ]scmyciel__5146_27.min1.thm1.tptp2017-02-06 16:57 536  
[ ]scmyciel__5157_16.min1.thm1.tptp2017-02-06 16:57 577  
[ ]scmyciel__5166_19.min1.thm1.tptp2017-02-06 16:57 607  
[ ]scmyciel__5237_18.min1.thm1.tptp2017-02-06 16:57 607  
[ ]scmyciel__5270_17.min1.thm1.tptp2017-02-06 16:57 577  
[ ]scmyciel__5369_17.min1.thm1.tptp2017-02-06 16:57 504  
[ ]setfam_1__186_30.min1.thm1.tptp2017-02-06 16:57 401  
[ ]setfam_1__626_30.min1.thm1.tptp2017-02-06 16:57 426  
[ ]setfam_1__647_17.min1.thm1.tptp2017-02-06 16:57 370  
[ ]setfam_1__648_24.min1.thm1.tptp2017-02-06 16:57 383  
[ ]setfam_1__833_37.min1.thm1.tptp2017-02-06 16:57 442  
[ ]setfam_1__1300_28.min1.thm1.tptp2017-02-06 16:57 392  
[ ]setlim_1__69_18.min1.thm1.tptp2017-02-06 16:57 615  
[ ]setwop_2__128_25.min1.thm1.tptp2017-02-06 16:57 373  
[ ]setwop_2__893_18.min1.thm1.tptp2017-02-06 16:57 454  
[ ]sgraph1__80_40.min1.thm1.tptp2017-02-06 16:57 401  
[ ]sgraph1__122_40.min1.thm1.tptp2017-02-06 16:57 401  
[ ]sgraph1__241_18.min1.thm1.tptp2017-02-06 16:57 417  
[ ]sgraph1__709_18.min1.thm1.tptp2017-02-06 16:57 477  
[ ]simplex0__133_21.min1.thm1.tptp2017-02-06 16:57 401  
[ ]simplex0__135_20.min1.thm1.tptp2017-02-06 16:57 401  
[ ]simplex0__340_22.min1.thm1.tptp2017-02-06 16:57 400  
[ ]simplex0__342_23.min1.thm1.tptp2017-02-06 16:57 452  
[ ]simplex0__346_14.min1.thm1.tptp2017-02-06 16:57 444  
[ ]simplex0__351_15.min1.thm1.tptp2017-02-06 16:57 361  
[ ]simplex0__651_14.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]simplex0__1572_24.min1.thm1.tptp2017-02-06 16:57 445  
[ ]simplex2__1105_20.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]sin_cos9__448_49.min1.thm1.tptp2017-02-06 16:57 680  
[ ]sincos10__869_39.min1.thm1.tptp2017-02-06 16:57 536  
[ ]sincos10__954_49.min1.thm1.tptp2017-02-06 16:57 700  
[ ]sincos10__1827_43.min1.thm1.tptp2017-02-06 16:57 472  
[ ]sincos10__1929_43.min1.thm1.tptp2017-02-06 16:57 472  
[ ]sppol_2__3235_44.min1.thm1.tptp2017-02-06 16:57 944  
[ ]sppol_2__3236_42.min1.thm1.tptp2017-02-06 16:57 873  
[ ]sppol_2__3241_37.min1.thm1.tptp2017-02-06 16:57 863  
[ ]sppol_2__3242_16.min1.thm1.tptp2017-02-06 16:57 930  
[ ]sprect_3__479_21.min1.thm1.tptp2017-02-06 16:57 598  
[ ]sprect_3__484_16.min1.thm1.tptp2017-02-06 16:57 590  
[ ]sprect_3__534_21.min1.thm1.tptp2017-02-06 16:57 630  
[ ]sprect_3__540_16.min1.thm1.tptp2017-02-06 16:57 622  
[ ]stirl2_1__2675_30.min1.thm1.tptp2017-02-06 16:57 530  
[ ]stirl2_1__3094_52.min1.thm1.tptp2017-02-06 16:57 482  
[ ]stirl2_1__3100_17.min1.thm1.tptp2017-02-06 16:57 367  
[ ]sysrel__363_25.min1.thm1.tptp2017-02-06 16:57 386  
[ ]sysrel__372_18.min1.thm1.tptp2017-02-06 16:57 382  
[ ]taxonom2__679_16.min1.thm1.tptp2017-02-06 16:57 424  
[ ]taxonom2__682_18.min1.thm1.tptp2017-02-06 16:57 428  
[ ]taxonom2__1350_18.min1.thm1.tptp2017-02-06 16:57 542  
[ ]taxonom2__1365_18.min1.thm1.tptp2017-02-06 16:57 542  
[ ]taxonom2__1368_20.min1.thm1.tptp2017-02-06 16:57 554  
[ ]taxonom2__1380_20.min1.thm1.tptp2017-02-06 16:57 554  
[ ]taxonom2__1406_14.min1.thm1.tptp2017-02-06 16:57 531  
[ ]taxonom2__1465_18.min1.thm1.tptp2017-02-06 16:57 426  
[ ]taxonom2__1481_18.min1.thm1.tptp2017-02-06 16:57 426  
[ ]taxonom2__1484_20.min1.thm1.tptp2017-02-06 16:57 438  
[ ]taxonom2__1497_20.min1.thm1.tptp2017-02-06 16:57 438  
[ ]taxonom2__1585_14.min1.thm1.tptp2017-02-06 16:57 415  
[ ]taxonom2__1771_25.min1.thm1.tptp2017-02-06 16:57 403  
[ ]taxonom2__1851_24.min1.thm1.tptp2017-02-06 16:57 592  
[ ]taxonom2__1863_22.min1.thm1.tptp2017-02-06 16:57 609  
[ ]taxonom2__1866_21.min1.thm1.tptp2017-02-06 16:57 413  
[ ]taxonom2__1943_24.min1.thm1.tptp2017-02-06 16:57 592  
[ ]taxonom2__1946_26.min1.thm1.tptp2017-02-06 16:57 596  
[ ]taxonom2__1965_26.min1.thm1.tptp2017-02-06 16:57 596  
[ ]taxonom2__2022_24.min1.thm1.tptp2017-02-06 16:57 694  
[ ]taxonom2__2051_24.min1.thm1.tptp2017-02-06 16:57 694  
[ ]taxonom2__2054_26.min1.thm1.tptp2017-02-06 16:57 698  
[ ]taxonom2__2073_26.min1.thm1.tptp2017-02-06 16:57 698  
[ ]tmap_1__2774_22.min1.thm1.tptp2017-02-06 16:57 493  
[ ]toler_1__399_27.min1.thm1.tptp2017-02-06 16:57 449  
[ ]toler_1__402_27.min1.thm1.tptp2017-02-06 16:57 449  
[ ]toler_1__611_28.min1.thm1.tptp2017-02-06 16:57 427  
[ ]toler_1__614_28.min1.thm1.tptp2017-02-06 16:57 427  
[ ]topalg_6__2400_37.min1.thm1.tptp2017-02-06 16:57 400  
[ ]topgen_3__2386_31.min1.thm1.tptp2017-02-06 16:57 438  
[ ]topgen_4__914_19.min1.thm1.tptp2017-02-06 16:57 386  
[ ]topgen_4__936_16.min1.thm1.tptp2017-02-06 16:57 446  
[ ]topgen_4__1023_27.min1.thm1.tptp2017-02-06 16:57 404  
[ ]topgen_5__81_36.min1.thm1.tptp2017-02-06 16:57 443  
[ ]topgen_5__87_19.min1.thm1.tptp2017-02-06 16:57 499  
[ ]topgen_5__3644_29.min1.thm1.tptp2017-02-06 16:57 366  
[ ]topgen_5__3645_47.min1.thm1.tptp2017-02-06 16:57 509  
[ ]topgen_5__3666_47.min1.thm1.tptp2017-02-06 16:57 509  
[ ]topgen_5__3675_16.min1.thm1.tptp2017-02-06 16:57 726  
[ ]topgen_5__3742_23.min1.thm1.tptp2017-02-06 16:57 342  
[ ]topgen_5__3744_27.min1.thm1.tptp2017-02-06 16:57 398  
[ ]topgen_5__3748_27.min1.thm1.tptp2017-02-06 16:57 398  
[ ]topgen_5__3779_31.min1.thm1.tptp2017-02-06 16:57 398  
[ ]topgen_5__3791_16.min1.thm1.tptp2017-02-06 16:57 502  
[ ]topmetr2__121_27.min1.thm1.tptp2017-02-06 16:57 377  
[ ]topmetr2__656_32.min1.thm1.tptp2017-02-06 16:57 398  
[ ]topmetr2__667_32.min1.thm1.tptp2017-02-06 16:57 398  
[ ]topreal1__68_23.min1.thm1.tptp2017-02-06 16:57 366  
[ ]topreal1__78_16.min1.thm1.tptp2017-02-06 16:57 403  
[ ]trees_1__549_31.min1.thm1.tptp2017-02-06 16:57 411  
[ ]trees_1__559_36.min1.thm1.tptp2017-02-06 16:57 605  
[ ]trees_1__561_19.min1.thm1.tptp2017-02-06 16:57 605  
[ ]trees_1__645_43.min1.thm1.tptp2017-02-06 16:57 467  
[ ]trees_1__659_43.min1.thm1.tptp2017-02-06 16:57 467  
[ ]trees_1__673_8.min1.thm1.tptp2017-02-06 16:57 667  
[ ]trees_1__689_21.min1.thm1.tptp2017-02-06 16:57 542  
[ ]trees_2__103_19.min1.thm1.tptp2017-02-06 16:57 428  
[ ]trees_2__107_45.min1.thm1.tptp2017-02-06 16:57 418  
[ ]trees_2__740_43.min1.thm1.tptp2017-02-06 16:57 473  
[ ]trees_2__1066_43.min1.thm1.tptp2017-02-06 16:57 455  
[ ]trees_3__208_28.min1.thm1.tptp2017-02-06 16:57 382  
[ ]trees_3__217_23.min1.thm1.tptp2017-02-06 16:57 339  
[ ]trees_3__270_28.min1.thm1.tptp2017-02-06 16:57 391  
[ ]trees_3__279_23.min1.thm1.tptp2017-02-06 16:57 346  
[ ]trees_3__332_28.min1.thm1.tptp2017-02-06 16:57 391  
[ ]trees_3__341_23.min1.thm1.tptp2017-02-06 16:57 346  
[ ]trees_3__1641_36.min1.thm1.tptp2017-02-06 16:57 524  
[ ]trees_3__1643_21.min1.thm1.tptp2017-02-06 16:57 516  
[ ]trees_3__1646_34.min1.thm1.tptp2017-02-06 16:57 512  
[ ]trees_3__1648_27.min1.thm1.tptp2017-02-06 16:57 520  
[ ]trees_3__1665_36.min1.thm1.tptp2017-02-06 16:57 538  
[ ]trees_3__1670_27.min1.thm1.tptp2017-02-06 16:57 443  
[ ]trees_3__2077_22.min1.thm1.tptp2017-02-06 16:57 516  
[ ]trees_3__2099_18.min1.thm1.tptp2017-02-06 16:57 424  
[ ]trees_3__2131_31.min1.thm1.tptp2017-02-06 16:57 502  
[ ]trees_3__2185_58.min1.thm1.tptp2017-02-06 16:57 516  
[ ]trees_9__1920_23.min1.thm1.tptp2017-02-06 16:57 397  
[ ]trees_9__1930_23.min1.thm1.tptp2017-02-06 16:57 407  
[ ]trees_9__2188_25.min1.thm1.tptp2017-02-06 16:57 407  
[ ]trees_9__2195_25.min1.thm1.tptp2017-02-06 16:57 419  
[ ]trees_9__2547_25.min1.thm1.tptp2017-02-06 16:57 401  
[ ]trees_a__594_21.min1.thm1.tptp2017-02-06 16:57 536  
[ ]trees_a__627_19.min1.thm1.tptp2017-02-06 16:57 526  
[ ]turing_1__2733_21.min1.thm1.tptp2017-02-06 16:57 836  
[ ]valued_1__2708_28.min1.thm1.tptp2017-02-06 16:57 625  
[ ]valued_1__2716_31.min1.thm1.tptp2017-02-06 16:57 461  
[ ]vectsp_9__1610_32.min1.thm1.tptp2017-02-06 16:57 436  
[ ]vectsp_9__1618_32.min1.thm1.tptp2017-02-06 16:57 436  
[ ]vectsp_9__1650_26.min1.thm1.tptp2017-02-06 16:57 404  
[ ]vfunct_1__1592_16.min1.thm1.tptp2017-02-06 16:57 394  
[ ]vfunct_2__1568_16.min1.thm1.tptp2017-02-06 16:57 394  
[ ]waybel19__1072_55.min1.thm1.tptp2017-02-06 16:57 442  
[ ]waybel30__351_60.min1.thm1.tptp2017-02-06 16:57 516  
[ ]waybel30__1324_18.min1.thm1.tptp2017-02-06 16:57 443  
[ ]waybel30__1377_18.min1.thm1.tptp2017-02-06 16:57 442  
[ ]waybel_3__851_25.min1.thm1.tptp2017-02-06 16:57 679  
[ ]waybel_4__2876_19.min1.thm1.tptp2017-02-06 16:57 545  
[ ]waybel_4__2882_30.min1.thm1.tptp2017-02-06 16:57 545  
[ ]waybel_6__1588_30.min1.thm1.tptp2017-02-06 16:57 432  
[ ]waybel_6__2374_21.min1.thm1.tptp2017-02-06 16:57 612  
[ ]waybel_6__2383_18.min1.thm1.tptp2017-02-06 16:57 612  
[ ]wellset1__65_21.min1.thm1.tptp2017-02-06 16:57 350  
[ ]xboole_0__188_46.min1.thm1.tptp2017-02-06 16:57 532  
[ ]xboole_0__244_18.min1.thm1.tptp2017-02-06 16:57 361  
[ ]xboole_0__296_4.min1.thm1.tptp2017-02-06 16:57 581  
[ ]xboole_1__63_33.min1.thm1.tptp2017-02-06 16:57 447  
[ ]xboole_1__64_38.min1.thm1.tptp2017-02-06 16:57 493  
[ ]xboole_1__65_33.min1.thm1.tptp2017-02-06 16:57 493  
[ ]xboole_1__66_19.min1.thm1.tptp2017-02-06 16:57 447  
[ ]xboole_1__70_31.min1.thm1.tptp2017-02-06 16:57 437  
[ ]xboole_1__71_36.min1.thm1.tptp2017-02-06 16:57 479  
[ ]xboole_1__72_31.min1.thm1.tptp2017-02-06 16:57 479  
[ ]xboole_1__107_26.min1.thm1.tptp2017-02-06 16:57 381  
[ ]xboole_1__118_26.min1.thm1.tptp2017-02-06 16:57 381  
[ ]xboole_1__120_17.min1.thm1.tptp2017-02-06 16:57 381  
[ ]xboole_1__146_28.min1.thm1.tptp2017-02-06 16:57 400  
[ ]xboole_1__150_16.min1.thm1.tptp2017-02-06 16:57 423  
[ ]xboole_1__162_26.min1.thm1.tptp2017-02-06 16:57 390  
[ ]xboole_1__164_17.min1.thm1.tptp2017-02-06 16:57 390  
[ ]xboole_1__258_21.min1.thm1.tptp2017-02-06 16:57 345  
[ ]xboole_1__269_33.min1.thm1.tptp2017-02-06 16:57 458  
[ ]xboole_1__286_23.min1.thm1.tptp2017-02-06 16:57 400  
[ ]xboole_1__289_19.min1.thm1.tptp2017-02-06 16:57 516  
[ ]xboole_1__293_36.min1.thm1.tptp2017-02-06 16:57 506  
[ ]xboole_1__296_21.min1.thm1.tptp2017-02-06 16:57 488  
[ ]xboole_1__307_33.min1.thm1.tptp2017-02-06 16:57 458  
[ ]xboole_1__309_37.min1.thm1.tptp2017-02-06 16:57 527  
[ ]xboole_1__317_23.min1.thm1.tptp2017-02-06 16:57 390  
[ ]xboole_1__319_26.min1.thm1.tptp2017-02-06 16:57 390  
[ ]xboole_1__321_17.min1.thm1.tptp2017-02-06 16:57 448  
[ ]xboole_1__402_28.min1.thm1.tptp2017-02-06 16:57 458  
[ ]xboole_1__405_20.min1.thm1.tptp2017-02-06 16:57 451  
[ ]xboole_1__414_23.min1.thm1.tptp2017-02-06 16:57 390  
[ ]xboole_1__426_42.min1.thm1.tptp2017-02-06 16:57 516  
[ ]xboole_1__428_24.min1.thm1.tptp2017-02-06 16:57 502  
[ ]xboole_1__508_19.min1.thm1.tptp2017-02-06 16:57 516  
[ ]xboole_1__555_32.min1.thm1.tptp2017-02-06 16:57 458  
[ ]xboole_1__557_19.min1.thm1.tptp2017-02-06 16:57 400  
[ ]xboole_1__561_39.min1.thm1.tptp2017-02-06 16:57 441  
[ ]xboole_1__563_17.min1.thm1.tptp2017-02-06 16:57 448  
[ ]xboole_1__575_23.min1.thm1.tptp2017-02-06 16:57 400  
[ ]xboole_1__585_20.min1.thm1.tptp2017-02-06 16:57 400  
[ ]xboole_1__614_17.min1.thm1.tptp2017-02-06 16:57 357  
[ ]xboole_1__633_19.min1.thm1.tptp2017-02-06 16:57 516  
[ ]xboole_1__637_38.min1.thm1.tptp2017-02-06 16:57 506  
[ ]xboole_1__640_23.min1.thm1.tptp2017-02-06 16:57 492  
[ ]xboole_1__668_17.min1.thm1.tptp2017-02-06 16:57 390  
[ ]xboole_1__679_41.min1.thm1.tptp2017-02-06 16:57 560  
[ ]xboole_1__757_39.min1.thm1.tptp2017-02-06 16:57 516  
[ ]xboole_1__764_17.min1.thm1.tptp2017-02-06 16:57 506  
[ ]xboole_1__777_19.min1.thm1.tptp2017-02-06 16:57 516  
[ ]xboole_1__782_39.min1.thm1.tptp2017-02-06 16:57 516  
[ ]xboole_1__826_30.min1.thm1.tptp2017-02-06 16:57 404  
[ ]xboole_1__828_21.min1.thm1.tptp2017-02-06 16:57 520  
[ ]xboole_1__831_40.min1.thm1.tptp2017-02-06 16:57 516  
[ ]xboole_1__971_41.min1.thm1.tptp2017-02-06 16:57 549  
[ ]xboole_1__989_18.min1.thm1.tptp2017-02-06 16:57 353  
[ ]xboole_1__1493_19.min1.thm1.tptp2017-02-06 16:57 589  
[ ]xregular__107_31.min1.thm1.tptp2017-02-06 16:57 402  
[ ]xregular__176_31.min1.thm1.tptp2017-02-06 16:57 402  
[ ]xregular__267_31.min1.thm1.tptp2017-02-06 16:57 402  
[ ]xregular__386_31.min1.thm1.tptp2017-02-06 16:57 402  
[ ]xtuple_0__680_18.min1.thm1.tptp2017-02-06 16:57 452  
[ ]xtuple_0__729_18.min1.thm1.tptp2017-02-06 16:57 456  
[ ]xxreal_0__228_42.min1.thm1.tptp2017-02-06 16:57 392  
[ ]xxreal_1__2253_19.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__2256_36.min1.thm1.tptp2017-02-06 16:57 515  
[ ]xxreal_1__2275_34.min1.thm1.tptp2017-02-06 16:57 481  
[ ]xxreal_1__2291_19.min1.thm1.tptp2017-02-06 16:57 485  
[ ]xxreal_1__2294_34.min1.thm1.tptp2017-02-06 16:57 481  
[ ]xxreal_1__2310_19.min1.thm1.tptp2017-02-06 16:57 485  
[ ]xxreal_1__2313_34.min1.thm1.tptp2017-02-06 16:57 481  
[ ]xxreal_1__2332_34.min1.thm1.tptp2017-02-06 16:57 481  
[ ]xxreal_1__3101_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3121_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3141_19.min1.thm1.tptp2017-02-06 16:57 527  
[ ]xxreal_1__3149_19.min1.thm1.tptp2017-02-06 16:57 527  
[ ]xxreal_1__3157_19.min1.thm1.tptp2017-02-06 16:57 527  
[ ]xxreal_1__3166_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3186_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3206_19.min1.thm1.tptp2017-02-06 16:57 527  
[ ]xxreal_1__3214_19.min1.thm1.tptp2017-02-06 16:57 527  
[ ]xxreal_1__3222_19.min1.thm1.tptp2017-02-06 16:57 527  
[ ]xxreal_1__3236_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3247_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3260_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3271_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3284_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3295_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3308_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3319_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3332_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3343_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3356_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3367_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3380_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3391_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3404_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3415_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3428_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3439_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3453_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3464_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3478_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3489_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3503_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3514_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3528_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3539_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__3553_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__3564_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4109_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__4112_38.min1.thm1.tptp2017-02-06 16:57 521  
[ ]xxreal_1__4149_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__4152_38.min1.thm1.tptp2017-02-06 16:57 521  
[ ]xxreal_1__4191_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__4194_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4221_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__4224_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4251_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__4254_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4281_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__4284_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4300_39.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4308_39.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4316_39.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4324_39.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__4512_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5228_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5231_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5260_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5263_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5292_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5295_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5324_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5327_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5356_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5359_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5388_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5391_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5420_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5423_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5452_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5455_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5484_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5487_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5516_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5519_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5548_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5551_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5580_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5583_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5612_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5615_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5644_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5647_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5676_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5679_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__5708_19.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__5711_38.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__6430_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__6441_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__6454_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__6465_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_1__6478_40.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_1__6489_17.min1.thm1.tptp2017-02-06 16:57 519  
[ ]xxreal_2__285_14.min1.thm1.tptp2017-02-06 16:57 392  
[ ]xxreal_2__309_14.min1.thm1.tptp2017-02-06 16:57 392  
[ ]xxreal_2__2276_33.min1.thm1.tptp2017-02-06 16:57 515  
[ ]xxreal_2__2307_33.min1.thm1.tptp2017-02-06 16:57 515  
[ ]xxreal_2__2341_33.min1.thm1.tptp2017-02-06 16:57 515  
[ ]xxreal_2__2375_33.min1.thm1.tptp2017-02-06 16:57 515  
[ ]xxreal_2__2428_21.min1.thm1.tptp2017-02-06 16:57 368  
[ ]xxreal_2__2437_23.min1.thm1.tptp2017-02-06 16:57 376  
[ ]xxreal_2__2452_23.min1.thm1.tptp2017-02-06 16:57 376  
[ ]xxreal_2__2490_21.min1.thm1.tptp2017-02-06 16:57 368  
[ ]xxreal_2__2499_23.min1.thm1.tptp2017-02-06 16:57 376  
[ ]xxreal_2__2552_21.min1.thm1.tptp2017-02-06 16:57 368  
[ ]xxreal_2__2561_23.min1.thm1.tptp2017-02-06 16:57 376  
[ ]xxreal_2__2576_23.min1.thm1.tptp2017-02-06 16:57 376  
[ ]yellow21__1197_16.min1.thm1.tptp2017-02-06 16:57 738  
[ ]yellow_2__103_16.min1.thm1.tptp2017-02-06 16:57 393  
[ ]yellow_2__153_16.min1.thm1.tptp2017-02-06 16:57 393  
[ ]yellow_8__764_27.min1.thm1.tptp2017-02-06 16:57 438  
[ ]yellow_9__944_21.min1.thm1.tptp2017-02-06 16:57 412  
[ ]yellow_9__952_21.min1.thm1.tptp2017-02-06 16:57 430  
[ ]yellow_9__958_14.min1.thm1.tptp2017-02-06 16:57 472  
[ ]yellow_9__2763_25.min1.thm1.tptp2017-02-06 16:57 377  
[ ]zf_lang1__1893_40.min1.thm1.tptp2017-02-06 16:57 449  
[ ]zf_lang1__1907_45.min1.thm1.tptp2017-02-06 16:57 455  
[ ]zf_lang1__2030_29.min1.thm1.tptp2017-02-06 16:57 459  
[ ]zf_lang1__2038_38.min1.thm1.tptp2017-02-06 16:57 447  
[ ]zf_lang1__2041_33.min1.thm1.tptp2017-02-06 16:57 462  
[ ]zf_lang__2108_21.min1.thm1.tptp2017-02-06 16:57 476  
[ ]zf_lang__2146_52.min1.thm1.tptp2017-02-06 16:57 460  
[ ]zf_lang__2150_21.min1.thm1.tptp2017-02-06 16:57 592  
[ ]zf_lang__2212_21.min1.thm1.tptp2017-02-06 16:57 508  
[ ]zfmisc_1__888_36.min1.thm1.tptp2017-02-06 16:57 442  
[ ]zfmisc_1__934_17.min1.thm1.tptp2017-02-06 16:57 514  
[ ]zfmisc_1__942_48.min1.thm1.tptp2017-02-06 16:57 558  
[ ]zfmisc_1__950_19.min1.thm1.tptp2017-02-06 16:57 516  
[ ]zfmisc_1__1003_23.min1.thm1.tptp2017-02-06 16:57 400  
[ ]zfmisc_1__1005_19.min1.thm1.tptp2017-02-06 16:57 444  
[ ]zfmisc_1__1337_31.min1.thm1.tptp2017-02-06 16:57 397  
[ ]zfmisc_1__1352_22.min1.thm1.tptp2017-02-06 16:57 358  
[ ]zfmisc_1__1417_25.min1.thm1.tptp2017-02-06 16:57 404  
[ ]zfmisc_1__1426_23.min1.thm1.tptp2017-02-06 16:57 502  
[ ]zfmisc_1__1432_44.min1.thm1.tptp2017-02-06 16:57 532  
[ ]zfmisc_1__1763_20.min1.thm1.tptp2017-02-06 16:57 370  
[ ]zfmisc_1__1798_33.min1.thm1.tptp2017-02-06 16:57 412  
[ ]zfmisc_1__1813_24.min1.thm1.tptp2017-02-06 16:57 373  
[ ]zfmodel2__88_66.min1.thm1.tptp2017-02-06 16:57 828  
[ ]zfmodel2__95_21.min1.thm1.tptp2017-02-06 16:57 661  
[ ]zfmodel2__120_21.min1.thm1.tptp2017-02-06 16:57 657  
[ ]zfmodel2__226_45.min1.thm1.tptp2017-02-06 16:57 563  
[ ]zfmodel2__233_23.min1.thm1.tptp2017-02-06 16:57 621  
[ ]zfmodel2__237_50.min1.thm1.tptp2017-02-06 16:57 611  
[ ]zfmodel2__244_35.min1.thm1.tptp2017-02-06 16:57 553  
[ ]zfmodel2__315_55.min1.thm1.tptp2017-02-06 16:57 621  
[ ]zfmodel2__338_54.min1.thm1.tptp2017-02-06 16:57 611  
[ ]zfrefle1__480_58.min1.thm1.tptp2017-02-06 16:57 813  
Apache/2.4.18 (Ubuntu) Server at grid01.ciirc.cvut.cz Port 80