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

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[ ]abcmiz_1__348_14.min1.thm1.tptp2017-02-06 16:57 696  
[ ]abcmiz_1__368_51.min1.thm1.tptp2017-02-06 16:57 569  
[ ]abcmiz_1__1089_45.min1.thm1.tptp2017-02-06 16:57 370  
[ ]abcmiz_1__1099_45.min1.thm1.tptp2017-02-06 16:57 602  
[ ]abcmiz_1__2739_32.min1.thm1.tptp2017-02-06 16:57 1.7K 
[ ]abcmiz_1__3330_42.min1.thm1.tptp2017-02-06 16:57 357  
[ ]abcmiz_1__3355_42.min1.thm1.tptp2017-02-06 16:57 357  
[ ]abcmiz_1__4816_26.min1.thm1.tptp2017-02-06 16:57 654  
[ ]abcmiz_1__4832_26.min1.thm1.tptp2017-02-06 16:57 810  
[ ]abcmiz_a__726_38.min1.thm1.tptp2017-02-06 16:57 510  
[ ]abcmiz_a__762_38.min1.thm1.tptp2017-02-06 16:57 510  
[ ]abcmiz_a__789_38.min1.thm1.tptp2017-02-06 16:57 510  
[ ]abcmiz_a__884_59.min1.thm1.tptp2017-02-06 16:57 313  
[ ]abcmiz_a__945_64.min1.thm1.tptp2017-02-06 16:57 313  
[ ]abcmiz_a__988_38.min1.thm1.tptp2017-02-06 16:57 510  
[ ]abcmiz_a__1548_8.min1.thm1.tptp2017-02-06 16:57 313  
[ ]abcmiz_a__2098_8.min1.thm1.tptp2017-02-06 16:57 310  
[ ]abcmiz_a__2117_8.min1.thm1.tptp2017-02-06 16:57 310  
[ ]abcmiz_a__2151_8.min1.thm1.tptp2017-02-06 16:57 310  
[ ]afinsq_1__2347_61.min1.thm1.tptp2017-02-06 16:57 364  
[ ]afproj__886_36.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]afproj__1044_12.min1.thm1.tptp2017-02-06 16:57 296  
[ ]afproj__1076_10.min1.thm1.tptp2017-02-06 16:57 280  
[ ]afproj__2617_10.min1.thm1.tptp2017-02-06 16:57 286  
[ ]afproj__2945_14.min1.thm1.tptp2017-02-06 16:57 294  
[ ]afproj__3156_15.min1.thm1.tptp2017-02-06 16:57 296  
[ ]afproj__3162_15.min1.thm1.tptp2017-02-06 16:57 296  
[ ]afproj__3168_15.min1.thm1.tptp2017-02-06 16:57 296  
[ ]algstr_4__650_54.min1.thm1.tptp2017-02-06 16:57 594  
[ ]algstr_4__653_54.min1.thm1.tptp2017-02-06 16:57 594  
[ ]algstr_4__2345_17.min1.thm1.tptp2017-02-06 16:57 284  
[ ]algstr_4__2347_17.min1.thm1.tptp2017-02-06 16:57 296  
[ ]algstr_4__2400_26.min1.thm1.tptp2017-02-06 16:57 575  
[ ]algstr_4__2456_22.min1.thm1.tptp2017-02-06 16:57 338  
[ ]algstr_4__2457_47.min1.thm1.tptp2017-02-06 16:57 339  
[ ]algstr_4__2458_47.min1.thm1.tptp2017-02-06 16:57 341  
[ ]algstr_4__2459_30.min1.thm1.tptp2017-02-06 16:57 377  
[ ]algstr_4__2460_30.min1.thm1.tptp2017-02-06 16:57 378  
[ ]algstr_4__3034_23.min1.thm1.tptp2017-02-06 16:57 332  
[ ]altcat_1__147_21.min1.thm1.tptp2017-02-06 16:57 343  
[ ]altcat_2__432_18.min1.thm1.tptp2017-02-06 16:57 360  
[ ]armstrng__101_28.min1.thm1.tptp2017-02-06 16:57 289  
[ ]armstrng__2098_19.min1.thm1.tptp2017-02-06 16:57 401  
[ ]armstrng__2203_25.min1.thm1.tptp2017-02-06 16:57 367  
[ ]armstrng__2279_24.min1.thm1.tptp2017-02-06 16:57 364  
[ ]armstrng__3067_27.min1.thm1.tptp2017-02-06 16:57 371  
[ ]armstrng__3801_23.min1.thm1.tptp2017-02-06 16:57 370  
[ ]arytm_0__717_24.min1.thm1.tptp2017-02-06 16:57 347  
[ ]arytm_0__749_16.min1.thm1.tptp2017-02-06 16:57 497  
[ ]arytm_0__768_22.min1.thm1.tptp2017-02-06 16:57 449  
[ ]arytm_3__796_25.min1.thm1.tptp2017-02-06 16:57 295  
[ ]arytm_3__831_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]arytm_3__848_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]arytm_3__1005_40.min1.thm1.tptp2017-02-06 16:57 353  
[ ]bagorder__395_23.min1.thm1.tptp2017-02-06 16:57 616  
[ ]bagorder__419_23.min1.thm1.tptp2017-02-06 16:57 616  
[ ]bagorder__521_23.min1.thm1.tptp2017-02-06 16:57 616  
[ ]bagorder__545_23.min1.thm1.tptp2017-02-06 16:57 616  
[ ]bagorder__1379_24.min1.thm1.tptp2017-02-06 16:57 380  
[ ]bagorder__1382_20.min1.thm1.tptp2017-02-06 16:57 368  
[ ]bagorder__1971_22.min1.thm1.tptp2017-02-06 16:57 824  
[ ]bagorder__1998_52.min1.thm1.tptp2017-02-06 16:57 954  
[ ]bagorder__2022_18.min1.thm1.tptp2017-02-06 16:57 822  
[ ]bagorder__2034_24.min1.thm1.tptp2017-02-06 16:57 366  
[ ]bagorder__2047_24.min1.thm1.tptp2017-02-06 16:57 366  
[ ]bagorder__2064_44.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]bagorder__2510_18.min1.thm1.tptp2017-02-06 16:57 1.9K 
[ ]bagorder__2568_18.min1.thm1.tptp2017-02-06 16:57 1.9K 
[ ]bagorder__2584_29.min1.thm1.tptp2017-02-06 16:57 378  
[ ]bagorder__2590_25.min1.thm1.tptp2017-02-06 16:57 366  
[ ]bagorder__2604_25.min1.thm1.tptp2017-02-06 16:57 366  
[ ]bagorder__2712_25.min1.thm1.tptp2017-02-06 16:57 468  
[ ]bagorder__2732_29.min1.thm1.tptp2017-02-06 16:57 480  
[ ]bagorder__2735_25.min1.thm1.tptp2017-02-06 16:57 468  
[ ]bagorder__2756_31.min1.thm1.tptp2017-02-06 16:57 472  
[ ]bcialg_2__1314_54.min1.thm1.tptp2017-02-06 16:57 863  
[ ]bcialg_6__141_20.min1.thm1.tptp2017-02-06 16:57 612  
[ ]bcialg_6__147_10.min1.thm1.tptp2017-02-06 16:57 484  
[ ]bhsp_5__619_26.min1.thm1.tptp2017-02-06 16:57 512  
[ ]bhsp_5__647_49.min1.thm1.tptp2017-02-06 16:57 916  
[ ]bhsp_5__731_43.min1.thm1.tptp2017-02-06 16:57 822  
[ ]bhsp_5__813_16.min1.thm1.tptp2017-02-06 16:57 968  
[ ]bhsp_5__864_16.min1.thm1.tptp2017-02-06 16:57 754  
[ ]bhsp_5__913_16.min1.thm1.tptp2017-02-06 16:57 470  
[ ]bhsp_5__973_16.min1.thm1.tptp2017-02-06 16:57 464  
[ ]bhsp_5__989_16.min1.thm1.tptp2017-02-06 16:57 526  
[ ]bhsp_7__628_16.min1.thm1.tptp2017-02-06 16:57 792  
[ ]bintree2__414_16.min1.thm1.tptp2017-02-06 16:57 388  
[ ]bintree2__419_16.min1.thm1.tptp2017-02-06 16:57 393  
[ ]borsuk_3__373_16.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]borsuk_6__640_14.min1.thm1.tptp2017-02-06 16:57 480  
[ ]borsuk_6__2992_14.min1.thm1.tptp2017-02-06 16:57 300  
[ ]borsuk_6__3982_17.min1.thm1.tptp2017-02-06 16:57 304  
[ ]borsuk_6__4028_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]borsuk_6__4029_17.min1.thm1.tptp2017-02-06 16:57 299  
[ ]borsuk_6__4305_17.min1.thm1.tptp2017-02-06 16:57 304  
[ ]borsuk_6__4351_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]borsuk_6__4352_17.min1.thm1.tptp2017-02-06 16:57 299  
[ ]card_1__1664_12.min1.thm1.tptp2017-02-06 16:57 324  
[ ]card_1__1695_17.min1.thm1.tptp2017-02-06 16:57 322  
[ ]card_1__1974_17.min1.thm1.tptp2017-02-06 16:57 306  
[ ]card_2__175_10.min1.thm1.tptp2017-02-06 16:57 321  
[ ]card_2__212_28.min1.thm1.tptp2017-02-06 16:57 354  
[ ]card_2__224_21.min1.thm1.tptp2017-02-06 16:57 298  
[ ]card_2__230_21.min1.thm1.tptp2017-02-06 16:57 298  
[ ]card_2__460_17.min1.thm1.tptp2017-02-06 16:57 298  
[ ]card_2__1039_17.min1.thm1.tptp2017-02-06 16:57 297  
[ ]card_2__1048_17.min1.thm1.tptp2017-02-06 16:57 292  
[ ]card_2__1563_36.min1.thm1.tptp2017-02-06 16:57 282  
[ ]card_3__1176_17.min1.thm1.tptp2017-02-06 16:57 307  
[ ]card_3__1177_17.min1.thm1.tptp2017-02-06 16:57 307  
[ ]cat_1__386_7.min1.thm1.tptp2017-02-06 16:57 797  
[ ]catalg_1__924_21.min1.thm1.tptp2017-02-06 16:57 320  
[ ]catalg_1__935_21.min1.thm1.tptp2017-02-06 16:57 320  
[ ]catalg_1__957_14.min1.thm1.tptp2017-02-06 16:57 868  
[ ]cgames_1__1700_52.min1.thm1.tptp2017-02-06 16:57 795  
[ ]circcmb3__759_23.min1.thm1.tptp2017-02-06 16:57 383  
[ ]circcmb3__788_15.min1.thm1.tptp2017-02-06 16:57 322  
[ ]circcmb3__1279_15.min1.thm1.tptp2017-02-06 16:57 384  
[ ]circcmb3__2149_41.min1.thm1.tptp2017-02-06 16:57 529  
[ ]circcmb3__2177_51.min1.thm1.tptp2017-02-06 16:57 612  
[ ]circcmb3__2206_66.min1.thm1.tptp2017-02-06 16:57 703  
[ ]circcmb3__2238_76.min1.thm1.tptp2017-02-06 16:57 782  
[ ]circcmb3__2240_71.min1.thm1.tptp2017-02-06 16:57 769  
[ ]circcomb__1437_25.min1.thm1.tptp2017-02-06 16:57 409  
[ ]circcomb__1924_23.min1.thm1.tptp2017-02-06 16:57 368  
[ ]circcomb__1967_23.min1.thm1.tptp2017-02-06 16:57 368  
[ ]circtrm1__1243_46.min1.thm1.tptp2017-02-06 16:57 380  
[ ]coh_sp__734_22.min1.thm1.tptp2017-02-06 16:57 335  
[ ]coh_sp__750_44.min1.thm1.tptp2017-02-06 16:57 446  
[ ]coh_sp__775_25.min1.thm1.tptp2017-02-06 16:57 340  
[ ]coh_sp__1429_15.min1.thm1.tptp2017-02-06 16:57 306  
[ ]coh_sp__1462_27.min1.thm1.tptp2017-02-06 16:57 345  
[ ]coh_sp__1573_20.min1.thm1.tptp2017-02-06 16:57 335  
[ ]coh_sp__1590_44.min1.thm1.tptp2017-02-06 16:57 446  
[ ]coh_sp__1615_25.min1.thm1.tptp2017-02-06 16:57 340  
[ ]cohsp_1__1490_16.min1.thm1.tptp2017-02-06 16:57 408  
[ ]cohsp_1__1702_17.min1.thm1.tptp2017-02-06 16:57 304  
[ ]cohsp_1__1861_16.min1.thm1.tptp2017-02-06 16:57 523  
[ ]cohsp_1__2144_17.min1.thm1.tptp2017-02-06 16:57 304  
[ ]cohsp_1__2602_60.min1.thm1.tptp2017-02-06 16:57 574  
[ ]cohsp_1__2846_16.min1.thm1.tptp2017-02-06 16:57 369  
[ ]cohsp_1__4603_16.min1.thm1.tptp2017-02-06 16:57 551  
[ ]cohsp_1__4809_76.min1.thm1.tptp2017-02-06 16:57 680  
[ ]conlat_1__179_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__181_45.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__183_34.min1.thm1.tptp2017-02-06 16:57 388  
[ ]conlat_1__187_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__189_48.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__191_34.min1.thm1.tptp2017-02-06 16:57 388  
[ ]conlat_1__193_42.min1.thm1.tptp2017-02-06 16:57 356  
[ ]conlat_1__194_22.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__195_12.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__196_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__198_46.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__199_13.min1.thm1.tptp2017-02-06 16:57 356  
[ ]conlat_1__212_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__214_52.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__215_12.min1.thm1.tptp2017-02-06 16:57 356  
[ ]conlat_1__248_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__250_52.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__252_34.min1.thm1.tptp2017-02-06 16:57 388  
[ ]conlat_1__268_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__270_56.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__272_34.min1.thm1.tptp2017-02-06 16:57 388  
[ ]conlat_1__273_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__275_56.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__276_13.min1.thm1.tptp2017-02-06 16:57 356  
[ ]conlat_1__341_18.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__343_45.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__345_34.min1.thm1.tptp2017-02-06 16:57 388  
[ ]conlat_1__349_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__351_56.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__355_34.min1.thm1.tptp2017-02-06 16:57 388  
[ ]conlat_1__357_42.min1.thm1.tptp2017-02-06 16:57 356  
[ ]conlat_1__358_22.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__359_12.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__360_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__362_46.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__363_13.min1.thm1.tptp2017-02-06 16:57 356  
[ ]conlat_1__376_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__378_52.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__379_12.min1.thm1.tptp2017-02-06 16:57 356  
[ ]conlat_1__412_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__414_52.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__416_34.min1.thm1.tptp2017-02-06 16:57 388  
[ ]conlat_1__432_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__434_56.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__436_34.min1.thm1.tptp2017-02-06 16:57 388  
[ ]conlat_1__437_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_1__439_56.min1.thm1.tptp2017-02-06 16:57 502  
[ ]conlat_1__440_13.min1.thm1.tptp2017-02-06 16:57 356  
[ ]conlat_2__1910_22.min1.thm1.tptp2017-02-06 16:57 308  
[ ]conlat_2__1912_11.min1.thm1.tptp2017-02-06 16:57 308  
[ ]conlat_2__1980_10.min1.thm1.tptp2017-02-06 16:57 308  
[ ]conlat_2__1981_17.min1.thm1.tptp2017-02-06 16:57 308  
[ ]conlat_2__1984_22.min1.thm1.tptp2017-02-06 16:57 308  
[ ]conlat_2__1986_11.min1.thm1.tptp2017-02-06 16:57 308  
[ ]conlat_2__2329_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]conlat_2__2340_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]conlat_2__2802_69.min1.thm1.tptp2017-02-06 16:57 506  
[ ]conlat_2__2803_22.min1.thm1.tptp2017-02-06 16:57 700  
[ ]conlat_2__2804_12.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_2__2805_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_2__2806_61.min1.thm1.tptp2017-02-06 16:57 700  
[ ]conlat_2__2807_30.min1.thm1.tptp2017-02-06 16:57 506  
[ ]conlat_2__2808_24.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_2__2810_13.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_2__2851_18.min1.thm1.tptp2017-02-06 16:57 324  
[ ]conlat_2__2852_61.min1.thm1.tptp2017-02-06 16:57 705  
[ ]conlat_2__2853_32.min1.thm1.tptp2017-02-06 16:57 509  
[ ]conlat_2__2863_30.min1.thm1.tptp2017-02-06 16:57 512  
[ ]conlat_2__2867_34.min1.thm1.tptp2017-02-06 16:57 538  
[ ]conlat_2__2875_32.min1.thm1.tptp2017-02-06 16:57 541  
[ ]conlat_2__2910_19.min1.thm1.tptp2017-02-06 16:57 426  
[ ]conlat_2__2911_62.min1.thm1.tptp2017-02-06 16:57 803  
[ ]conlat_2__2912_30.min1.thm1.tptp2017-02-06 16:57 506  
[ ]conlat_2__2915_18.min1.thm1.tptp2017-02-06 16:57 375  
[ ]conlat_2__2917_34.min1.thm1.tptp2017-02-06 16:57 535  
[ ]dickson__215_17.min1.thm1.tptp2017-02-06 16:57 440  
[ ]dickson__264_17.min1.thm1.tptp2017-02-06 16:57 450  
[ ]dickson__282_61.min1.thm1.tptp2017-02-06 16:57 450  
[ ]dickson__926_39.min1.thm1.tptp2017-02-06 16:57 340  
[ ]dickson__936_16.min1.thm1.tptp2017-02-06 16:57 470  
[ ]dickson__1093_16.min1.thm1.tptp2017-02-06 16:57 470  
[ ]dickson__1140_18.min1.thm1.tptp2017-02-06 16:57 486  
[ ]dickson__1838_16.min1.thm1.tptp2017-02-06 16:57 470  
[ ]dickson__3656_22.min1.thm1.tptp2017-02-06 16:57 327  
[ ]dickson__3657_22.min1.thm1.tptp2017-02-06 16:57 327  
[ ]dickson__3688_24.min1.thm1.tptp2017-02-06 16:57 328  
[ ]dickson__3701_24.min1.thm1.tptp2017-02-06 16:57 329  
[ ]dickson__3872_22.min1.thm1.tptp2017-02-06 16:57 327  
[ ]dickson__3896_22.min1.thm1.tptp2017-02-06 16:57 327  
[ ]dickson__4372_28.min1.thm1.tptp2017-02-06 16:57 346  
[ ]dickson__4399_28.min1.thm1.tptp2017-02-06 16:57 346  
[ ]dickson__4402_24.min1.thm1.tptp2017-02-06 16:57 334  
[ ]ec_pf_1__1580_39.min1.thm1.tptp2017-02-06 16:57 361  
[ ]ec_pf_1__1647_40.min1.thm1.tptp2017-02-06 16:57 345  
[ ]eqrel_1__779_20.min1.thm1.tptp2017-02-06 16:57 710  
[ ]eqrel_1__937_18.min1.thm1.tptp2017-02-06 16:57 524  
[ ]eqrel_1__1289_71.min1.thm1.tptp2017-02-06 16:57 692  
[ ]exchsort__743_29.min1.thm1.tptp2017-02-06 16:57 411  
[ ]facirc_1__1111_29.min1.thm1.tptp2017-02-06 16:57 439  
[ ]facirc_1__1129_36.min1.thm1.tptp2017-02-06 16:57 427  
[ ]facirc_1__1157_34.min1.thm1.tptp2017-02-06 16:57 537  
[ ]facirc_1__1176_34.min1.thm1.tptp2017-02-06 16:57 537  
[ ]facirc_1__1310_15.min1.thm1.tptp2017-02-06 16:57 300  
[ ]facirc_1__1946_55.min1.thm1.tptp2017-02-06 16:57 744  
[ ]facirc_1__2157_55.min1.thm1.tptp2017-02-06 16:57 744  
[ ]facirc_2__960_53.min1.thm1.tptp2017-02-06 16:57 731  
[ ]facirc_2__961_14.min1.thm1.tptp2017-02-06 16:57 768  
[ ]facirc_2__978_21.min1.thm1.tptp2017-02-06 16:57 358  
[ ]facirc_2__979_21.min1.thm1.tptp2017-02-06 16:57 358  
[ ]facirc_2__991_22.min1.thm1.tptp2017-02-06 16:57 359  
[ ]facirc_2__1011_22.min1.thm1.tptp2017-02-06 16:57 359  
[ ]facirc_2__1025_22.min1.thm1.tptp2017-02-06 16:57 359  
[ ]facirc_2__1037_22.min1.thm1.tptp2017-02-06 16:57 359  
[ ]facirc_2__1119_46.min1.thm1.tptp2017-02-06 16:57 759  
[ ]facirc_2__1167_44.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]finseq_3__3930_10.min1.thm1.tptp2017-02-06 16:57 845  
[ ]finset_1__1238_12.min1.thm1.tptp2017-02-06 16:57 324  
[ ]finset_1__1304_12.min1.thm1.tptp2017-02-06 16:57 324  
[ ]fscirc_2__763_4.min1.thm1.tptp2017-02-06 16:57 731  
[ ]fscirc_2__764_14.min1.thm1.tptp2017-02-06 16:57 766  
[ ]fscirc_2__781_21.min1.thm1.tptp2017-02-06 16:57 358  
[ ]fscirc_2__782_21.min1.thm1.tptp2017-02-06 16:57 358  
[ ]fscirc_2__794_22.min1.thm1.tptp2017-02-06 16:57 359  
[ ]fscirc_2__814_22.min1.thm1.tptp2017-02-06 16:57 359  
[ ]fscirc_2__828_22.min1.thm1.tptp2017-02-06 16:57 359  
[ ]fscirc_2__840_22.min1.thm1.tptp2017-02-06 16:57 359  
[ ]fscirc_2__923_48.min1.thm1.tptp2017-02-06 16:57 759  
[ ]fscirc_2__971_44.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]fsm_1__961_63.min1.thm1.tptp2017-02-06 16:57 610  
[ ]fsm_1__4191_23.min1.thm1.tptp2017-02-06 16:57 505  
[ ]fsm_1__4260_21.min1.thm1.tptp2017-02-06 16:57 493  
[ ]funcop_1__66_21.min1.thm1.tptp2017-02-06 16:57 366  
[ ]funcop_1__76_51.min1.thm1.tptp2017-02-06 16:57 453  
[ ]funcop_1__98_21.min1.thm1.tptp2017-02-06 16:57 366  
[ ]funcop_1__130_21.min1.thm1.tptp2017-02-06 16:57 366  
[ ]funcop_1__163_21.min1.thm1.tptp2017-02-06 16:57 366  
[ ]funcop_1__215_23.min1.thm1.tptp2017-02-06 16:57 404  
[ ]funct_1__66_22.min1.thm1.tptp2017-02-06 16:57 377  
[ ]funct_1__97_18.min1.thm1.tptp2017-02-06 16:57 436  
[ ]funct_3__1235_16.min1.thm1.tptp2017-02-06 16:57 508  
[ ]funct_4__862_29.min1.thm1.tptp2017-02-06 16:57 346  
[ ]funct_4__985_16.min1.thm1.tptp2017-02-06 16:57 418  
[ ]funct_6__2033_34.min1.thm1.tptp2017-02-06 16:57 396  
[ ]funct_6__2039_34.min1.thm1.tptp2017-02-06 16:57 396  
[ ]funct_6__2069_33.min1.thm1.tptp2017-02-06 16:57 382  
[ ]funct_6__2074_33.min1.thm1.tptp2017-02-06 16:57 382  
[ ]funct_7__168_33.min1.thm1.tptp2017-02-06 16:57 434  
[ ]functor0__1002_13.min1.thm1.tptp2017-02-06 16:57 574  
[ ]functor0__1004_13.min1.thm1.tptp2017-02-06 16:57 574  
[ ]functor0__1058_13.min1.thm1.tptp2017-02-06 16:57 574  
[ ]functor0__1064_13.min1.thm1.tptp2017-02-06 16:57 574  
[ ]functor0__1165_9.min1.thm1.tptp2017-02-06 16:57 300  
[ ]functor0__1210_11.min1.thm1.tptp2017-02-06 16:57 558  
[ ]functor0__1212_11.min1.thm1.tptp2017-02-06 16:57 558  
[ ]functor0__1262_11.min1.thm1.tptp2017-02-06 16:57 558  
[ ]functor0__1267_11.min1.thm1.tptp2017-02-06 16:57 558  
[ ]functor0__1802_8.min1.thm1.tptp2017-02-06 16:57 300  
[ ]functor0__1917_8.min1.thm1.tptp2017-02-06 16:57 300  
[ ]functor0__2594_8.min1.thm1.tptp2017-02-06 16:57 304  
[ ]fuzzy_4__359_13.min1.thm1.tptp2017-02-06 16:57 408  
[ ]gfacirc1__340_32.min1.thm1.tptp2017-02-06 16:57 420  
[ ]gfacirc1__343_34.min1.thm1.tptp2017-02-06 16:57 421  
[ ]gfacirc1__372_32.min1.thm1.tptp2017-02-06 16:57 421  
[ ]gfacirc1__377_32.min1.thm1.tptp2017-02-06 16:57 421  
[ ]gfacirc1__380_32.min1.thm1.tptp2017-02-06 16:57 421  
[ ]gfacirc1__584_22.min1.thm1.tptp2017-02-06 16:57 731  
[ ]gfacirc1__585_14.min1.thm1.tptp2017-02-06 16:57 766  
[ ]gfacirc1__623_44.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]gfacirc1__663_24.min1.thm1.tptp2017-02-06 16:57 371  
[ ]gfacirc1__700_35.min1.thm1.tptp2017-02-06 16:57 759  
[ ]gfacirc1__760_22.min1.thm1.tptp2017-02-06 16:57 731  
[ ]gfacirc1__835_43.min1.thm1.tptp2017-02-06 16:57 872  
[ ]gfacirc1__876_22.min1.thm1.tptp2017-02-06 16:57 731  
[ ]gfacirc1__1640_22.min1.thm1.tptp2017-02-06 16:57 731  
[ ]gfacirc1__1641_14.min1.thm1.tptp2017-02-06 16:57 768  
[ ]gfacirc1__1679_44.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]gfacirc1__1719_14.min1.thm1.tptp2017-02-06 16:57 371  
[ ]gfacirc1__1756_35.min1.thm1.tptp2017-02-06 16:57 759  
[ ]gfacirc1__1816_22.min1.thm1.tptp2017-02-06 16:57 731  
[ ]gfacirc1__1891_43.min1.thm1.tptp2017-02-06 16:57 874  
[ ]gfacirc1__1932_22.min1.thm1.tptp2017-02-06 16:57 731  
[ ]gfacirc1__2717_22.min1.thm1.tptp2017-02-06 16:57 744  
[ ]gfacirc1__2718_14.min1.thm1.tptp2017-02-06 16:57 788  
[ ]gfacirc1__2756_44.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]gfacirc1__2797_14.min1.thm1.tptp2017-02-06 16:57 375  
[ ]gfacirc1__2834_35.min1.thm1.tptp2017-02-06 16:57 776  
[ ]gfacirc1__2894_22.min1.thm1.tptp2017-02-06 16:57 744  
[ ]gfacirc1__2969_43.min1.thm1.tptp2017-02-06 16:57 893  
[ ]gfacirc1__3010_22.min1.thm1.tptp2017-02-06 16:57 744  
[ ]gfacirc1__3777_22.min1.thm1.tptp2017-02-06 16:57 744  
[ ]gfacirc1__3778_14.min1.thm1.tptp2017-02-06 16:57 788  
[ ]gfacirc1__3816_44.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]gfacirc1__3857_14.min1.thm1.tptp2017-02-06 16:57 375  
[ ]gfacirc1__3894_35.min1.thm1.tptp2017-02-06 16:57 776  
[ ]gfacirc1__3954_22.min1.thm1.tptp2017-02-06 16:57 744  
[ ]gfacirc1__4029_43.min1.thm1.tptp2017-02-06 16:57 893  
[ ]gfacirc1__4070_22.min1.thm1.tptp2017-02-06 16:57 744  
[ ]goboard1__1262_30.min1.thm1.tptp2017-02-06 16:57 364  
[ ]goboard1__1274_30.min1.thm1.tptp2017-02-06 16:57 364  
[ ]goboard1__1515_51.min1.thm1.tptp2017-02-06 16:57 871  
[ ]graph_3__2703_37.min1.thm1.tptp2017-02-06 16:57 4.2K 
[ ]graph_3__2707_37.min1.thm1.tptp2017-02-06 16:57 4.2K 
[ ]graph_3__2785_57.min1.thm1.tptp2017-02-06 16:57 2.2K 
[ ]graph_3__2793_60.min1.thm1.tptp2017-02-06 16:57 2.2K 
[ ]graph_3__2811_53.min1.thm1.tptp2017-02-06 16:57 2.2K 
[ ]graph_3__2829_53.min1.thm1.tptp2017-02-06 16:57 2.2K 
[ ]graph_3__2859_46.min1.thm1.tptp2017-02-06 16:57 1.5K 
[ ]graph_3__2895_46.min1.thm1.tptp2017-02-06 16:57 1.5K 
[ ]grfunc_1__148_66.min1.thm1.tptp2017-02-06 16:57 574  
[ ]grfunc_1__160_18.min1.thm1.tptp2017-02-06 16:57 362  
[ ]grfunc_1__164_60.min1.thm1.tptp2017-02-06 16:57 804  
[ ]heyting1__568_43.min1.thm1.tptp2017-02-06 16:57 437  
[ ]heyting1__615_43.min1.thm1.tptp2017-02-06 16:57 437  
[ ]heyting1__658_43.min1.thm1.tptp2017-02-06 16:57 437  
[ ]heyting1__760_66.min1.thm1.tptp2017-02-06 16:57 412  
[ ]heyting1__1259_61.min1.thm1.tptp2017-02-06 16:57 414  
[ ]heyting3__169_16.min1.thm1.tptp2017-02-06 16:57 295  
[ ]index_1__1311_19.min1.thm1.tptp2017-02-06 16:57 626  
[ ]instalg1__1544_29.min1.thm1.tptp2017-02-06 16:57 339  
[ ]interva1__2440_43.min1.thm1.tptp2017-02-06 16:57 524  
[ ]jordan1f__1312_20.min1.thm1.tptp2017-02-06 16:57 634  
[ ]jordan1i__1125_32.min1.thm1.tptp2017-02-06 16:57 344  
[ ]jordan1i__1350_32.min1.thm1.tptp2017-02-06 16:57 344  
[ ]jordan1i__1755_74.min1.thm1.tptp2017-02-06 16:57 920  
[ ]jordan1i__1984_74.min1.thm1.tptp2017-02-06 16:57 920  
[ ]jordan9__265_16.min1.thm1.tptp2017-02-06 16:57 648  
[ ]jordan9__4054_24.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan9__4086_24.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan9__4117_24.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan9__4120_20.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan13__1921_24.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan13__1965_24.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan13__2008_24.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan13__2011_20.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]lang1__435_12.min1.thm1.tptp2017-02-06 16:57 728  
[ ]lang1__446_12.min1.thm1.tptp2017-02-06 16:57 828  
[ ]lattice5__4179_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]lattice5__4201_22.min1.thm1.tptp2017-02-06 16:57 442  
[ ]lattice5__4216_20.min1.thm1.tptp2017-02-06 16:57 360  
[ ]lattice5__4250_20.min1.thm1.tptp2017-02-06 16:57 322  
[ ]lattice5__4253_20.min1.thm1.tptp2017-02-06 16:57 322  
[ ]lattice5__4293_20.min1.thm1.tptp2017-02-06 16:57 322  
[ ]lattice5__4296_20.min1.thm1.tptp2017-02-06 16:57 323  
[ ]lattice5__4549_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]lattice5__4550_16.min1.thm1.tptp2017-02-06 16:57 306  
[ ]lattice5__4625_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]lattice5__4645_20.min1.thm1.tptp2017-02-06 16:57 315  
[ ]lattice5__4646_20.min1.thm1.tptp2017-02-06 16:57 315  
[ ]lattice5__4661_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]lattice5__4665_18.min1.thm1.tptp2017-02-06 16:57 307  
[ ]lattice5__4701_19.min1.thm1.tptp2017-02-06 16:57 307  
[ ]lattice5__4704_18.min1.thm1.tptp2017-02-06 16:57 307  
[ ]lattice5__4719_19.min1.thm1.tptp2017-02-06 16:57 310  
[ ]lattice5__4722_15.min1.thm1.tptp2017-02-06 16:57 310  
[ ]lattice5__4765_20.min1.thm1.tptp2017-02-06 16:57 311  
[ ]lattice5__4768_15.min1.thm1.tptp2017-02-06 16:57 311  
[ ]lattice5__4785_16.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice5__4788_15.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice5__4794_19.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice5__4805_19.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice5__4808_15.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice5__4909_18.min1.thm1.tptp2017-02-06 16:57 311  
[ ]lattice5__4911_18.min1.thm1.tptp2017-02-06 16:57 311  
[ ]lattice5__4956_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__4959_16.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__4963_22.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__4967_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__4981_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__4984_16.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__4988_22.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__4992_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__5258_13.min1.thm1.tptp2017-02-06 16:57 338  
[ ]lattice5__5508_15.min1.thm1.tptp2017-02-06 16:57 341  
[ ]lattice5__5516_15.min1.thm1.tptp2017-02-06 16:57 341  
[ ]lattice7__244_16.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]lattice7__683_16.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]lattice7__766_18.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]lattice8__2917_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]lattice8__2939_22.min1.thm1.tptp2017-02-06 16:57 442  
[ ]lattice8__2954_20.min1.thm1.tptp2017-02-06 16:57 360  
[ ]lattice8__2991_20.min1.thm1.tptp2017-02-06 16:57 322  
[ ]lattice8__3036_20.min1.thm1.tptp2017-02-06 16:57 322  
[ ]lattice8__3089_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]lattice8__3090_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]lattice8__3164_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]lattice8__3184_20.min1.thm1.tptp2017-02-06 16:57 315  
[ ]lattice8__3185_20.min1.thm1.tptp2017-02-06 16:57 315  
[ ]lattice8__3200_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]lattice8__3204_18.min1.thm1.tptp2017-02-06 16:57 307  
[ ]lattice8__3240_19.min1.thm1.tptp2017-02-06 16:57 307  
[ ]lattice8__3243_15.min1.thm1.tptp2017-02-06 16:57 307  
[ ]lattice8__3257_19.min1.thm1.tptp2017-02-06 16:57 310  
[ ]lattice8__3260_15.min1.thm1.tptp2017-02-06 16:57 310  
[ ]lattice8__3302_19.min1.thm1.tptp2017-02-06 16:57 311  
[ ]lattice8__3305_16.min1.thm1.tptp2017-02-06 16:57 311  
[ ]lattice8__3320_19.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice8__3323_16.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice8__3338_19.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice8__3341_16.min1.thm1.tptp2017-02-06 16:57 314  
[ ]lattice8__3439_15.min1.thm1.tptp2017-02-06 16:57 311  
[ ]lattice8__3443_18.min1.thm1.tptp2017-02-06 16:57 311  
[ ]lattice8__3485_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__3488_16.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__3492_22.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__3496_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__3510_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__3513_16.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__3517_22.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__3521_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__3791_13.min1.thm1.tptp2017-02-06 16:57 338  
[ ]lattice8__4049_15.min1.thm1.tptp2017-02-06 16:57 341  
[ ]lattice8__4057_15.min1.thm1.tptp2017-02-06 16:57 341  
[ ]matrix15__680_20.min1.thm1.tptp2017-02-06 16:57 2.3K 
[ ]matrix15__3311_27.min1.thm1.tptp2017-02-06 16:57 888  
[ ]matrix15__3627_25.min1.thm1.tptp2017-02-06 16:57 2.9K 
[ ]mcart_1__215_47.min1.thm1.tptp2017-02-06 16:57 748  
[ ]mcart_1__217_43.min1.thm1.tptp2017-02-06 16:57 659  
[ ]mcart_1__377_36.min1.thm1.tptp2017-02-06 16:57 640  
[ ]mcart_1__385_31.min1.thm1.tptp2017-02-06 16:57 488  
[ ]mcart_1__395_52.min1.thm1.tptp2017-02-06 16:57 689  
[ ]mcart_1__396_57.min1.thm1.tptp2017-02-06 16:57 737  
[ ]mcart_1__397_66.min1.thm1.tptp2017-02-06 16:57 898  
[ ]mcart_1__423_39.min1.thm1.tptp2017-02-06 16:57 670  
[ ]mcart_1__440_55.min1.thm1.tptp2017-02-06 16:57 719  
[ ]mcart_1__441_60.min1.thm1.tptp2017-02-06 16:57 767  
[ ]mcart_1__1037_51.min1.thm1.tptp2017-02-06 16:57 488  
[ ]mcart_1__1225_51.min1.thm1.tptp2017-02-06 16:57 488  
[ ]mcart_1__1451_14.min1.thm1.tptp2017-02-06 16:57 501  
[ ]mmlquery__98_30.min1.thm1.tptp2017-02-06 16:57 386  
[ ]modelc_1__5170_18.min1.thm1.tptp2017-02-06 16:57 594  
[ ]msafree2__912_24.min1.thm1.tptp2017-02-06 16:57 514  
[ ]msafree3__175_10.min1.thm1.tptp2017-02-06 16:57 298  
[ ]msafree3__440_49.min1.thm1.tptp2017-02-06 16:57 475  
[ ]msafree3__441_15.min1.thm1.tptp2017-02-06 16:57 298  
[ ]msafree3__445_15.min1.thm1.tptp2017-02-06 16:57 298  
[ ]msafree3__564_49.min1.thm1.tptp2017-02-06 16:57 475  
[ ]msafree3__1074_8.min1.thm1.tptp2017-02-06 16:57 300  
[ ]msafree__909_18.min1.thm1.tptp2017-02-06 16:57 450  
[ ]msaterm__1659_28.min1.thm1.tptp2017-02-06 16:57 331  
[ ]msaterm__1668_28.min1.thm1.tptp2017-02-06 16:57 331  
[ ]msaterm__1694_37.min1.thm1.tptp2017-02-06 16:57 412  
[ ]msaterm__1760_37.min1.thm1.tptp2017-02-06 16:57 412  
[ ]msinst_1__194_17.min1.thm1.tptp2017-02-06 16:57 594  
[ ]msinst_1__1339_17.min1.thm1.tptp2017-02-06 16:57 587  
[ ]msscyc_2__329_42.min1.thm1.tptp2017-02-06 16:57 388  
[ ]msscyc_2__382_16.min1.thm1.tptp2017-02-06 16:57 312  
[ ]msscyc_2__580_26.min1.thm1.tptp2017-02-06 16:57 393  
[ ]msualg_6__1700_15.min1.thm1.tptp2017-02-06 16:57 306  
[ ]msualg_6__1702_13.min1.thm1.tptp2017-02-06 16:57 306  
[ ]msualg_6__2484_26.min1.thm1.tptp2017-02-06 16:57 525  
[ ]msualg_9__393_11.min1.thm1.tptp2017-02-06 16:57 308  
[ ]msualg_9__404_11.min1.thm1.tptp2017-02-06 16:57 308  
[ ]msualg_9__830_10.min1.thm1.tptp2017-02-06 16:57 321  
[ ]msualg_9__871_10.min1.thm1.tptp2017-02-06 16:57 321  
[ ]mycielsk__2031_21.min1.thm1.tptp2017-02-06 16:57 348  
[ ]nattra_1__1569_13.min1.thm1.tptp2017-02-06 16:57 324  
[ ]nattra_1__1583_13.min1.thm1.tptp2017-02-06 16:57 324  
[ ]nattra_1__1645_22.min1.thm1.tptp2017-02-06 16:57 324  
[ ]nattra_1__1650_16.min1.thm1.tptp2017-02-06 16:57 324  
[ ]nattra_1__1686_27.min1.thm1.tptp2017-02-06 16:57 416  
[ ]nattra_1__1749_14.min1.thm1.tptp2017-02-06 16:57 415  
[ ]nattra_1__1782_22.min1.thm1.tptp2017-02-06 16:57 336  
[ ]nattra_1__1802_32.min1.thm1.tptp2017-02-06 16:57 374  
[ ]nattra_1__1804_14.min1.thm1.tptp2017-02-06 16:57 372  
[ ]nattra_1__1821_23.min1.thm1.tptp2017-02-06 16:57 328  
[ ]nattra_1__1838_31.min1.thm1.tptp2017-02-06 16:57 379  
[ ]nattra_1__1840_15.min1.thm1.tptp2017-02-06 16:57 376  
[ ]nattra_1__1841_29.min1.thm1.tptp2017-02-06 16:57 366  
[ ]nattra_1__1843_14.min1.thm1.tptp2017-02-06 16:57 364  
[ ]nattra_1__1859_47.min1.thm1.tptp2017-02-06 16:57 420  
[ ]nattra_1__1888_14.min1.thm1.tptp2017-02-06 16:57 375  
[ ]nattra_1__1907_47.min1.thm1.tptp2017-02-06 16:57 406  
[ ]nattra_1__2039_8.min1.thm1.tptp2017-02-06 16:57 300  
[ ]nattra_1__2042_9.min1.thm1.tptp2017-02-06 16:57 300  
[ ]nattra_1__2062_16.min1.thm1.tptp2017-02-06 16:57 350  
[ ]nattra_1__2088_11.min1.thm1.tptp2017-02-06 16:57 302  
[ ]neckla_2__304_16.min1.thm1.tptp2017-02-06 16:57 484  
[ ]neckla_3__140_15.min1.thm1.tptp2017-02-06 16:57 885  
[ ]neckla_3__146_15.min1.thm1.tptp2017-02-06 16:57 885  
[ ]neckla_3__153_38.min1.thm1.tptp2017-02-06 16:57 1.7K 
[ ]neckla_3__154_14.min1.thm1.tptp2017-02-06 16:57 1.8K 
[ ]neckla_3__237_14.min1.thm1.tptp2017-02-06 16:57 297  
[ ]neckla_3__1525_18.min1.thm1.tptp2017-02-06 16:57 406  
[ ]neckla_3__4445_14.min1.thm1.tptp2017-02-06 16:57 522  
[ ]neckla_3__5845_35.min1.thm1.tptp2017-02-06 16:57 492  
[ ]neckla_3__6212_35.min1.thm1.tptp2017-02-06 16:57 492  
[ ]necklace__70_26.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]necklace__72_21.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]necklace__74_14.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]necklace__76_10.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]necklace__78_14.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]necklace__80_21.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]necklace__84_16.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]necklace__86_10.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]necklace__957_16.min1.thm1.tptp2017-02-06 16:57 721  
[ ]normform__548_15.min1.thm1.tptp2017-02-06 16:57 298  
[ ]numbers__943_31.min1.thm1.tptp2017-02-06 16:57 357  
[ ]orders_2__424_16.min1.thm1.tptp2017-02-06 16:57 550  
[ ]orders_2__1525_20.min1.thm1.tptp2017-02-06 16:57 562  
[ ]orders_2__1528_16.min1.thm1.tptp2017-02-06 16:57 552  
[ ]orders_2__1768_16.min1.thm1.tptp2017-02-06 16:57 550  
[ ]orders_2__2025_16.min1.thm1.tptp2017-02-06 16:57 632  
[ ]orders_2__2250_18.min1.thm1.tptp2017-02-06 16:57 570  
[ ]osafree__1278_35.min1.thm1.tptp2017-02-06 16:57 402  
[ ]osafree__2409_29.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]osafree__2433_31.min1.thm1.tptp2017-02-06 16:57 954  
[ ]osalg_4__112_18.min1.thm1.tptp2017-02-06 16:57 512  
[ ]osalg_4__895_31.min1.thm1.tptp2017-02-06 16:57 638  
[ ]osalg_4__925_26.min1.thm1.tptp2017-02-06 16:57 638  
[ ]osalg_4__974_26.min1.thm1.tptp2017-02-06 16:57 639  
[ ]osalg_4__977_26.min1.thm1.tptp2017-02-06 16:57 640  
[ ]osalg_4__1014_24.min1.thm1.tptp2017-02-06 16:57 788  
[ ]osalg_4__1020_21.min1.thm1.tptp2017-02-06 16:57 638  
[ ]partfun1__85_16.min1.thm1.tptp2017-02-06 16:57 573  
[ ]partit1__1446_18.min1.thm1.tptp2017-02-06 16:57 528  
[ ]partit1__1843_16.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]pcomps_2__79_16.min1.thm1.tptp2017-02-06 16:57 740  
[ ]pcs_0__332_18.min1.thm1.tptp2017-02-06 16:57 499  
[ ]pcs_0__354_18.min1.thm1.tptp2017-02-06 16:57 499  
[ ]pcs_0__429_16.min1.thm1.tptp2017-02-06 16:57 459  
[ ]pnproc_1__153_55.min1.thm1.tptp2017-02-06 16:57 812  
[ ]pralg_2__363_19.min1.thm1.tptp2017-02-06 16:57 323  
[ ]pralg_2__396_19.min1.thm1.tptp2017-02-06 16:57 323  
[ ]pre_poly__1086_34.min1.thm1.tptp2017-02-06 16:57 490  
[ ]pua2mss1__2345_16.min1.thm1.tptp2017-02-06 16:57 307  
[ ]pua2mss1__2489_16.min1.thm1.tptp2017-02-06 16:57 305  
[ ]pua2mss1__2490_16.min1.thm1.tptp2017-02-06 16:57 306  
[ ]qc_lang1__853_12.min1.thm1.tptp2017-02-06 16:57 291  
[ ]qc_lang1__1347_8.min1.thm1.tptp2017-02-06 16:57 285  
[ ]quaterni__424_37.min1.thm1.tptp2017-02-06 16:57 676  
[ ]recdef_1__669_43.min1.thm1.tptp2017-02-06 16:57 520  
[ ]relat_1__80_18.min1.thm1.tptp2017-02-06 16:57 323  
[ ]relat_1__174_16.min1.thm1.tptp2017-02-06 16:57 298  
[ ]relat_1__182_16.min1.thm1.tptp2017-02-06 16:57 358  
[ ]relat_1__434_16.min1.thm1.tptp2017-02-06 16:57 482  
[ ]relat_1__756_26.min1.thm1.tptp2017-02-06 16:57 273  
[ ]relat_1__922_18.min1.thm1.tptp2017-02-06 16:57 501  
[ ]relat_1__931_35.min1.thm1.tptp2017-02-06 16:57 470  
[ ]relat_1__1132_42.min1.thm1.tptp2017-02-06 16:57 540  
[ ]relat_1__1523_42.min1.thm1.tptp2017-02-06 16:57 540  
[ ]relat_1__1727_19.min1.thm1.tptp2017-02-06 16:57 664  
[ ]relat_1__1737_62.min1.thm1.tptp2017-02-06 16:57 664  
[ ]relat_1__2688_34.min1.thm1.tptp2017-02-06 16:57 376  
[ ]relat_1__2690_46.min1.thm1.tptp2017-02-06 16:57 430  
[ ]relat_1__2696_34.min1.thm1.tptp2017-02-06 16:57 376  
[ ]relat_1__2698_46.min1.thm1.tptp2017-02-06 16:57 431  
[ ]rewrite1__1245_49.min1.thm1.tptp2017-02-06 16:57 448  
[ ]scm_comp__268_21.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]scm_comp__365_29.min1.thm1.tptp2017-02-06 16:57 328  
[ ]scm_comp__366_29.min1.thm1.tptp2017-02-06 16:57 338  
[ ]scm_comp__558_29.min1.thm1.tptp2017-02-06 16:57 328  
[ ]scm_comp__559_29.min1.thm1.tptp2017-02-06 16:57 338  
[ ]scmyciel__3634_31.min1.thm1.tptp2017-02-06 16:57 379  
[ ]scmyciel__3640_33.min1.thm1.tptp2017-02-06 16:57 380  
[ ]scmyciel__3759_13.min1.thm1.tptp2017-02-06 16:57 650  
[ ]scmyciel__3768_20.min1.thm1.tptp2017-02-06 16:57 420  
[ ]scmyciel__3800_18.min1.thm1.tptp2017-02-06 16:57 428  
[ ]scmyciel__4243_55.min1.thm1.tptp2017-02-06 16:57 553  
[ ]scmyciel__4248_18.min1.thm1.tptp2017-02-06 16:57 553  
[ ]scmyciel__4459_21.min1.thm1.tptp2017-02-06 16:57 539  
[ ]scmyciel__4465_21.min1.thm1.tptp2017-02-06 16:57 539  
[ ]scmyciel__4747_19.min1.thm1.tptp2017-02-06 16:57 436  
[ ]sgraph1__960_15.min1.thm1.tptp2017-02-06 16:57 340  
[ ]sgraph1__973_19.min1.thm1.tptp2017-02-06 16:57 366  
[ ]sgraph1__976_14.min1.thm1.tptp2017-02-06 16:57 314  
[ ]sgraph1__988_15.min1.thm1.tptp2017-02-06 16:57 346  
[ ]sprect_3__74_35.min1.thm1.tptp2017-02-06 16:57 515  
[ ]stacks_1__862_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]sysrel__345_26.min1.thm1.tptp2017-02-06 16:57 373  
[ ]sysrel__469_40.min1.thm1.tptp2017-02-06 16:57 502  
[ ]taxonom1__184_16.min1.thm1.tptp2017-02-06 16:57 342  
[ ]taxonom1__463_18.min1.thm1.tptp2017-02-06 16:57 678  
[ ]topalg_4__390_10.min1.thm1.tptp2017-02-06 16:57 308  
[ ]topalg_4__429_10.min1.thm1.tptp2017-02-06 16:57 308  
[ ]topdim_2__702_20.min1.thm1.tptp2017-02-06 16:57 330  
[ ]topdim_2__705_20.min1.thm1.tptp2017-02-06 16:57 331  
[ ]topgen_5__201_15.min1.thm1.tptp2017-02-06 16:57 294  
[ ]topgen_5__202_13.min1.thm1.tptp2017-02-06 16:57 294  
[ ]topreal8__315_32.min1.thm1.tptp2017-02-06 16:57 376  
[ ]topreal8__334_32.min1.thm1.tptp2017-02-06 16:57 378  
[ ]valued_1__3282_55.min1.thm1.tptp2017-02-06 16:57 354  
[ ]waybel26__1772_15.min1.thm1.tptp2017-02-06 16:57 306  
[ ]waybel26__1788_15.min1.thm1.tptp2017-02-06 16:57 306  
[ ]waybel26__1892_23.min1.thm1.tptp2017-02-06 16:57 330  
[ ]waybel26__1896_22.min1.thm1.tptp2017-02-06 16:57 330  
[ ]waybel26__1967_23.min1.thm1.tptp2017-02-06 16:57 330  
[ ]waybel26__1970_22.min1.thm1.tptp2017-02-06 16:57 331  
[ ]waybel27__421_13.min1.thm1.tptp2017-02-06 16:57 303  
[ ]waybel27__422_14.min1.thm1.tptp2017-02-06 16:57 305  
[ ]waybel27__466_14.min1.thm1.tptp2017-02-06 16:57 299  
[ ]waybel27__467_14.min1.thm1.tptp2017-02-06 16:57 299  
[ ]waybel28__747_16.min1.thm1.tptp2017-02-06 16:57 462  
[ ]waybel28__767_16.min1.thm1.tptp2017-02-06 16:57 462  
[ ]waybel35__904_18.min1.thm1.tptp2017-02-06 16:57 588  
[ ]waybel35__932_18.min1.thm1.tptp2017-02-06 16:57 588  
[ ]waybel_4__978_14.min1.thm1.tptp2017-02-06 16:57 498  
[ ]waybel_4__1004_14.min1.thm1.tptp2017-02-06 16:57 498  
[ ]waybel_4__3260_18.min1.thm1.tptp2017-02-06 16:57 575  
[ ]waybel_4__3266_14.min1.thm1.tptp2017-02-06 16:57 714  
[ ]wellord2__72_37.min1.thm1.tptp2017-02-06 16:57 467  
[ ]wellord2__1118_24.min1.thm1.tptp2017-02-06 16:57 331  
[ ]wellset1__698_12.min1.thm1.tptp2017-02-06 16:57 540  
[ ]wellset1__1235_16.min1.thm1.tptp2017-02-06 16:57 355  
[ ]wellset1__1270_16.min1.thm1.tptp2017-02-06 16:57 387  
[ ]wellset1__1400_16.min1.thm1.tptp2017-02-06 16:57 436  
[ ]xtuple_0__38_13.min1.thm1.tptp2017-02-06 16:57 298  
[ ]xtuple_0__368_18.min1.thm1.tptp2017-02-06 16:57 362  
[ ]xtuple_0__379_20.min1.thm1.tptp2017-02-06 16:57 378  
[ ]yellow10__805_17.min1.thm1.tptp2017-02-06 16:57 316  
[ ]yellow10__839_15.min1.thm1.tptp2017-02-06 16:57 308  
[ ]yellow10__889_17.min1.thm1.tptp2017-02-06 16:57 316  
[ ]yellow10__923_15.min1.thm1.tptp2017-02-06 16:57 308  
[ ]yellow18__459_15.min1.thm1.tptp2017-02-06 16:57 310  
[ ]yellow18__460_15.min1.thm1.tptp2017-02-06 16:57 310  
[ ]yellow18__820_12.min1.thm1.tptp2017-02-06 16:57 567  
[ ]yellow18__834_26.min1.thm1.tptp2017-02-06 16:57 506  
[ ]yellow18__835_19.min1.thm1.tptp2017-02-06 16:57 420  
[ ]yellow18__1054_12.min1.thm1.tptp2017-02-06 16:57 574  
[ ]yellow18__1068_26.min1.thm1.tptp2017-02-06 16:57 516  
[ ]yellow18__1069_19.min1.thm1.tptp2017-02-06 16:57 428  
[ ]yellow18__3767_21.min1.thm1.tptp2017-02-06 16:57 335  
[ ]yellow18__3768_26.min1.thm1.tptp2017-02-06 16:57 364  
[ ]yellow19__578_17.min1.thm1.tptp2017-02-06 16:57 322  
[ ]yellow19__742_17.min1.thm1.tptp2017-02-06 16:57 323  
[ ]yellow19__744_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]yellow19__751_17.min1.thm1.tptp2017-02-06 16:57 323  
[ ]yellow20__1191_41.min1.thm1.tptp2017-02-06 16:57 890  
[ ]yellow20__1293_39.min1.thm1.tptp2017-02-06 16:57 891  
[ ]yellow_3__412_42.min1.thm1.tptp2017-02-06 16:57 297  
[ ]yellow_3__423_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]yellow_3__425_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]yellow_3__430_17.min1.thm1.tptp2017-02-06 16:57 281  
[ ]yellow_6__2551_19.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]yellow_6__2663_14.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]yoneda_1__83_14.min1.thm1.tptp2017-02-06 16:57 772  
[ ]yoneda_1__305_25.min1.thm1.tptp2017-02-06 16:57 587  
[ ]yoneda_1__310_25.min1.thm1.tptp2017-02-06 16:57 587  
[ ]yoneda_1__326_25.min1.thm1.tptp2017-02-06 16:57 587  
[ ]yoneda_1__331_25.min1.thm1.tptp2017-02-06 16:57 587  
[ ]yoneda_1__566_26.min1.thm1.tptp2017-02-06 16:57 603  
[ ]yoneda_1__571_27.min1.thm1.tptp2017-02-06 16:57 603  
[ ]yoneda_1__587_27.min1.thm1.tptp2017-02-06 16:57 603  
[ ]yoneda_1__592_26.min1.thm1.tptp2017-02-06 16:57 603  
[ ]yoneda_1__1499_25.min1.thm1.tptp2017-02-06 16:57 568  
[ ]yoneda_1__1510_25.min1.thm1.tptp2017-02-06 16:57 568  
[ ]yoneda_1__1537_24.min1.thm1.tptp2017-02-06 16:57 568  
[ ]zf_fund1__101_25.min1.thm1.tptp2017-02-06 16:57 506  
[ ]zf_fund1__102_19.min1.thm1.tptp2017-02-06 16:57 408  
[ ]zf_fund1__1104_25.min1.thm1.tptp2017-02-06 16:57 394  
[ ]zf_fund1__1660_22.min1.thm1.tptp2017-02-06 16:57 566  
[ ]zf_fund2__786_14.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]zf_model__172_43.min1.thm1.tptp2017-02-06 16:57 464  
[ ]zf_model__299_43.min1.thm1.tptp2017-02-06 16:57 463  
[ ]zf_model__367_43.min1.thm1.tptp2017-02-06 16:57 463  
[ ]zfmisc_1__33_11.min1.thm1.tptp2017-02-06 16:57 278  
[ ]zfmisc_1__555_16.min1.thm1.tptp2017-02-06 16:57 539  
[ ]zfmisc_1__1173_41.min1.thm1.tptp2017-02-06 16:57 430  
[ ]zfmisc_1__1178_45.min1.thm1.tptp2017-02-06 16:57 496  
[ ]zfmisc_1__1305_34.min1.thm1.tptp2017-02-06 16:57 456  
[ ]zfmisc_1__1315_14.min1.thm1.tptp2017-02-06 16:57 348  
[ ]zfmisc_1__2128_43.min1.thm1.tptp2017-02-06 16:57 693  
[ ]zfmisc_1__2353_19.min1.thm1.tptp2017-02-06 16:57 366  
[ ]zfmisc_1__2356_19.min1.thm1.tptp2017-02-06 16:57 383  
Apache/2.4.18 (Ubuntu) Server at grid01.ciirc.cvut.cz Port 80