Index of /~mptp/1147/mptp/ilp1/d2_tarski

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[ ]abcmiz_1__280_27.min1.thm1.tptp2017-02-06 16:57 419  
[ ]abcmiz_1__481_64.min1.thm1.tptp2017-02-06 16:57 562  
[ ]abcmiz_1__1713_24.min1.thm1.tptp2017-02-06 16:57 335  
[ ]abcmiz_1__4005_20.min1.thm1.tptp2017-02-06 16:57 346  
[ ]abcmiz_a__339_33.min1.thm1.tptp2017-02-06 16:57 333  
[ ]abcmiz_a__799_48.min1.thm1.tptp2017-02-06 16:57 395  
[ ]abcmiz_a__999_48.min1.thm1.tptp2017-02-06 16:57 395  
[ ]abcmiz_a__1142_28.min1.thm1.tptp2017-02-06 16:57 358  
[ ]abcmiz_a__1242_28.min1.thm1.tptp2017-02-06 16:57 358  
[ ]algstr_4__1777_23.min1.thm1.tptp2017-02-06 16:57 328  
[ ]ami_3__198_19.min1.thm1.tptp2017-02-06 16:57 311  
[ ]ami_4__694_17.min1.thm1.tptp2017-02-06 16:57 336  
[ ]ami_4__695_17.min1.thm1.tptp2017-02-06 16:57 341  
[ ]ami_4__906_19.min1.thm1.tptp2017-02-06 16:57 336  
[ ]ami_4__908_18.min1.thm1.tptp2017-02-06 16:57 341  
[ ]ami_6__656_32.min1.thm1.tptp2017-02-06 16:57 320  
[ ]ami_6__675_14.min1.thm1.tptp2017-02-06 16:57 349  
[ ]ami_6__785_32.min1.thm1.tptp2017-02-06 16:57 320  
[ ]ami_6__804_14.min1.thm1.tptp2017-02-06 16:57 349  
[ ]ami_6__918_23.min1.thm1.tptp2017-02-06 16:57 324  
[ ]ami_6__926_23.min1.thm1.tptp2017-02-06 16:57 337  
[ ]ami_6__934_23.min1.thm1.tptp2017-02-06 16:57 337  
[ ]ami_6__942_23.min1.thm1.tptp2017-02-06 16:57 337  
[ ]ami_6__950_23.min1.thm1.tptp2017-02-06 16:57 337  
[ ]ami_6__958_23.min1.thm1.tptp2017-02-06 16:57 337  
[ ]ami_6__995_16.min1.thm1.tptp2017-02-06 16:57 359  
[ ]ami_6__1185_41.min1.thm1.tptp2017-02-06 16:57 450  
[ ]ami_6__1186_41.min1.thm1.tptp2017-02-06 16:57 455  
[ ]ami_6__1204_46.min1.thm1.tptp2017-02-06 16:57 455  
[ ]ami_6__1209_41.min1.thm1.tptp2017-02-06 16:57 450  
[ ]ami_6__1225_46.min1.thm1.tptp2017-02-06 16:57 455  
[ ]ami_6__1230_41.min1.thm1.tptp2017-02-06 16:57 450  
[ ]ami_6__1247_46.min1.thm1.tptp2017-02-06 16:57 455  
[ ]ami_6__1252_41.min1.thm1.tptp2017-02-06 16:57 450  
[ ]ami_6__1269_46.min1.thm1.tptp2017-02-06 16:57 445  
[ ]ami_6__1275_41.min1.thm1.tptp2017-02-06 16:57 440  
[ ]ami_wstd__1559_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]amistd_1__951_35.min1.thm1.tptp2017-02-06 16:57 398  
[ ]amistd_1__958_16.min1.thm1.tptp2017-02-06 16:57 462  
[ ]aofa_000__2578_44.min1.thm1.tptp2017-02-06 16:57 518  
[ ]aofa_000__3382_18.min1.thm1.tptp2017-02-06 16:57 625  
[ ]aofa_000__3883_27.min1.thm1.tptp2017-02-06 16:57 527  
[ ]aofa_000__3945_23.min1.thm1.tptp2017-02-06 16:57 525  
[ ]arrow__88_17.min1.thm1.tptp2017-02-06 16:57 318  
[ ]arytm_0__718_20.min1.thm1.tptp2017-02-06 16:57 375  
[ ]arytm_0__721_17.min1.thm1.tptp2017-02-06 16:57 390  
[ ]arytm_0__739_17.min1.thm1.tptp2017-02-06 16:57 475  
[ ]arytm_0__757_30.min1.thm1.tptp2017-02-06 16:57 401  
[ ]arytm_0__770_28.min1.thm1.tptp2017-02-06 16:57 603  
[ ]arytm_0__793_19.min1.thm1.tptp2017-02-06 16:57 367  
[ ]arytm_0__803_19.min1.thm1.tptp2017-02-06 16:57 357  
[ ]bintree1__145_35.min1.thm1.tptp2017-02-06 16:57 543  
[ ]bintree1__386_42.min1.thm1.tptp2017-02-06 16:57 506  
[ ]bintree1__511_50.min1.thm1.tptp2017-02-06 16:57 588  
[ ]bintree1__517_54.min1.thm1.tptp2017-02-06 16:57 679  
[ ]bintree1__553_50.min1.thm1.tptp2017-02-06 16:57 588  
[ ]bintree1__559_54.min1.thm1.tptp2017-02-06 16:57 679  
[ ]bintree1__596_42.min1.thm1.tptp2017-02-06 16:57 520  
[ ]bintree1__600_35.min1.thm1.tptp2017-02-06 16:57 514  
[ ]bintree1__635_42.min1.thm1.tptp2017-02-06 16:57 520  
[ ]bintree1__639_35.min1.thm1.tptp2017-02-06 16:57 514  
[ ]bintree1__799_43.min1.thm1.tptp2017-02-06 16:57 597  
[ ]bintree1__835_32.min1.thm1.tptp2017-02-06 16:57 356  
[ ]brouwer__230_17.min1.thm1.tptp2017-02-06 16:57 339  
[ ]bvfunc11__90_26.min1.thm1.tptp2017-02-06 16:57 349  
[ ]bvfunc11__121_14.min1.thm1.tptp2017-02-06 16:57 307  
[ ]bvfunc11__143_29.min1.thm1.tptp2017-02-06 16:57 485  
[ ]bvfunc11__192_28.min1.thm1.tptp2017-02-06 16:57 367  
[ ]bvfunc14__177_19.min1.thm1.tptp2017-02-06 16:57 346  
[ ]bvfunc14__250_13.min1.thm1.tptp2017-02-06 16:57 308  
[ ]bvfunc14__715_23.min1.thm1.tptp2017-02-06 16:57 484  
[ ]bvfunc_1__2540_19.min1.thm1.tptp2017-02-06 16:57 358  
[ ]bvfunc_1__2739_21.min1.thm1.tptp2017-02-06 16:57 348  
[ ]card_2__1418_21.min1.thm1.tptp2017-02-06 16:57 314  
[ ]card_2__1431_21.min1.thm1.tptp2017-02-06 16:57 332  
[ ]card_3__551_23.min1.thm1.tptp2017-02-06 16:57 340  
[ ]card_3__558_17.min1.thm1.tptp2017-02-06 16:57 332  
[ ]card_3__559_23.min1.thm1.tptp2017-02-06 16:57 434  
[ ]card_3__1904_18.min1.thm1.tptp2017-02-06 16:57 478  
[ ]card_3__2389_23.min1.thm1.tptp2017-02-06 16:57 340  
[ ]card_3__2390_23.min1.thm1.tptp2017-02-06 16:57 340  
[ ]card_fil__1984_48.min1.thm1.tptp2017-02-06 16:57 323  
[ ]card_fin__1614_19.min1.thm1.tptp2017-02-06 16:57 394  
[ ]cat_3__115_20.min1.thm1.tptp2017-02-06 16:57 324  
[ ]cat_3__300_28.min1.thm1.tptp2017-02-06 16:57 331  
[ ]cat_3__366_28.min1.thm1.tptp2017-02-06 16:57 331  
[ ]cat_3__425_28.min1.thm1.tptp2017-02-06 16:57 331  
[ ]cat_3__442_28.min1.thm1.tptp2017-02-06 16:57 331  
[ ]cat_3__580_28.min1.thm1.tptp2017-02-06 16:57 331  
[ ]cat_3__1582_14.min1.thm1.tptp2017-02-06 16:57 330  
[ ]cat_3__1616_28.min1.thm1.tptp2017-02-06 16:57 333  
[ ]cat_3__1623_12.min1.thm1.tptp2017-02-06 16:57 328  
[ ]cat_3__1653_30.min1.thm1.tptp2017-02-06 16:57 341  
[ ]cat_3__1661_12.min1.thm1.tptp2017-02-06 16:57 329  
[ ]cat_3__1791_23.min1.thm1.tptp2017-02-06 16:57 313  
[ ]cat_3__1792_20.min1.thm1.tptp2017-02-06 16:57 313  
[ ]cat_3__2866_14.min1.thm1.tptp2017-02-06 16:57 330  
[ ]cat_3__2900_28.min1.thm1.tptp2017-02-06 16:57 333  
[ ]cat_3__2907_12.min1.thm1.tptp2017-02-06 16:57 328  
[ ]cat_3__2937_30.min1.thm1.tptp2017-02-06 16:57 341  
[ ]cat_3__2945_12.min1.thm1.tptp2017-02-06 16:57 329  
[ ]cat_3__3076_23.min1.thm1.tptp2017-02-06 16:57 318  
[ ]cat_3__3077_20.min1.thm1.tptp2017-02-06 16:57 318  
[ ]cat_4__86_17.min1.thm1.tptp2017-02-06 16:57 315  
[ ]cat_4__1156_17.min1.thm1.tptp2017-02-06 16:57 316  
[ ]catalg_1__783_26.min1.thm1.tptp2017-02-06 16:57 400  
[ ]catalg_1__1062_28.min1.thm1.tptp2017-02-06 16:57 418  
[ ]cfuncdom__557_12.min1.thm1.tptp2017-02-06 16:57 312  
[ ]cfuncdom__615_22.min1.thm1.tptp2017-02-06 16:57 357  
[ ]chain_1__121_17.min1.thm1.tptp2017-02-06 16:57 334  
[ ]circcmb3__1586_15.min1.thm1.tptp2017-02-06 16:57 340  
[ ]circcmb3__2669_33.min1.thm1.tptp2017-02-06 16:57 406  
[ ]circcmb3__2676_33.min1.thm1.tptp2017-02-06 16:57 406  
[ ]circcomb__1437_25.min1.thm1.tptp2017-02-06 16:57 409  
[ ]classes1__946_23.min1.thm1.tptp2017-02-06 16:57 378  
[ ]classes1__950_28.min1.thm1.tptp2017-02-06 16:57 368  
[ ]classes1__951_20.min1.thm1.tptp2017-02-06 16:57 600  
[ ]classes1__952_21.min1.thm1.tptp2017-02-06 16:57 615  
[ ]classes1__2456_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]classes2__102_26.min1.thm1.tptp2017-02-06 16:57 349  
[ ]closure2__531_30.min1.thm1.tptp2017-02-06 16:57 410  
[ ]closure2__609_29.min1.thm1.tptp2017-02-06 16:57 461  
[ ]coh_sp__488_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]coh_sp__489_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]cohsp_1__369_15.min1.thm1.tptp2017-02-06 16:57 336  
[ ]cohsp_1__752_21.min1.thm1.tptp2017-02-06 16:57 339  
[ ]cohsp_1__753_19.min1.thm1.tptp2017-02-06 16:57 339  
[ ]cohsp_1__804_13.min1.thm1.tptp2017-02-06 16:57 336  
[ ]cohsp_1__2602_60.min1.thm1.tptp2017-02-06 16:57 574  
[ ]cohsp_1__3588_18.min1.thm1.tptp2017-02-06 16:57 370  
[ ]cohsp_1__3641_17.min1.thm1.tptp2017-02-06 16:57 348  
[ ]combgras__2026_15.min1.thm1.tptp2017-02-06 16:57 314  
[ ]compos_2__765_31.min1.thm1.tptp2017-02-06 16:57 374  
[ ]comput_1__4291_43.min1.thm1.tptp2017-02-06 16:57 439  
[ ]comput_1__4418_38.min1.thm1.tptp2017-02-06 16:57 378  
[ ]comput_1__4626_16.min1.thm1.tptp2017-02-06 16:57 525  
[ ]comput_1__4744_16.min1.thm1.tptp2017-02-06 16:57 525  
[ ]comput_1__5427_22.min1.thm1.tptp2017-02-06 16:57 363  
[ ]dilworth__932_29.min1.thm1.tptp2017-02-06 16:57 584  
[ ]dilworth__944_32.min1.thm1.tptp2017-02-06 16:57 465  
[ ]dilworth__958_21.min1.thm1.tptp2017-02-06 16:57 578  
[ ]enumset1__34_19.min1.thm1.tptp2017-02-06 16:57 425  
[ ]enumset1__256_69.min1.thm1.tptp2017-02-06 16:57 742  
[ ]enumset1__992_21.min1.thm1.tptp2017-02-06 16:57 348  
[ ]equation__1050_16.min1.thm1.tptp2017-02-06 16:57 330  
[ ]euclid_6__3331_24.min1.thm1.tptp2017-02-06 16:57 352  
[ ]euclid_6__3384_29.min1.thm1.tptp2017-02-06 16:57 360  
[ ]euclid_6__3773_25.min1.thm1.tptp2017-02-06 16:57 364  
[ ]euclid_6__3804_25.min1.thm1.tptp2017-02-06 16:57 364  
[ ]facirc_1__184_26.min1.thm1.tptp2017-02-06 16:57 368  
[ ]facirc_1__1257_15.min1.thm1.tptp2017-02-06 16:57 340  
[ ]facirc_1__1355_15.min1.thm1.tptp2017-02-06 16:57 340  
[ ]facirc_1__1734_17.min1.thm1.tptp2017-02-06 16:57 341  
[ ]facirc_2__68_23.min1.thm1.tptp2017-02-06 16:57 391  
[ ]facirc_2__69_23.min1.thm1.tptp2017-02-06 16:57 391  
[ ]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__1189_23.min1.thm1.tptp2017-02-06 16:57 400  
[ ]facirc_2__1202_24.min1.thm1.tptp2017-02-06 16:57 402  
[ ]facirc_2__1211_24.min1.thm1.tptp2017-02-06 16:57 402  
[ ]fcont_1__2282_28.min1.thm1.tptp2017-02-06 16:57 968  
[ ]fcont_1__2572_28.min1.thm1.tptp2017-02-06 16:57 968  
[ ]fib_num2__329_21.min1.thm1.tptp2017-02-06 16:57 358  
[ ]finseq_1__122_26.min1.thm1.tptp2017-02-06 16:57 313  
[ ]finseq_3__913_25.min1.thm1.tptp2017-02-06 16:57 413  
[ ]finseq_3__914_26.min1.thm1.tptp2017-02-06 16:57 413  
[ ]finseq_3__2827_25.min1.thm1.tptp2017-02-06 16:57 500  
[ ]finseq_3__2927_17.min1.thm1.tptp2017-02-06 16:57 334  
[ ]finseq_3__2930_17.min1.thm1.tptp2017-02-06 16:57 334  
[ ]finseq_3__4097_30.min1.thm1.tptp2017-02-06 16:57 363  
[ ]finseq_3__4273_26.min1.thm1.tptp2017-02-06 16:57 323  
[ ]finseq_3__4282_26.min1.thm1.tptp2017-02-06 16:57 323  
[ ]finseq_3__4445_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]finseq_3__4447_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]finseq_3__4625_17.min1.thm1.tptp2017-02-06 16:57 349  
[ ]finseq_6__844_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]finseq_6__1154_20.min1.thm1.tptp2017-02-06 16:57 340  
[ ]finset_1__1513_24.min1.thm1.tptp2017-02-06 16:57 396  
[ ]fintopo6__2975_18.min1.thm1.tptp2017-02-06 16:57 434  
[ ]fomodel1__1485_26.min1.thm1.tptp2017-02-06 16:57 387  
[ ]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__993_23.min1.thm1.tptp2017-02-06 16:57 400  
[ ]fsm_2__902_48.min1.thm1.tptp2017-02-06 16:57 392  
[ ]funcsdom__711_12.min1.thm1.tptp2017-02-06 16:57 312  
[ ]funcsdom__768_22.min1.thm1.tptp2017-02-06 16:57 357  
[ ]funct_1__1651_21.min1.thm1.tptp2017-02-06 16:57 509  
[ ]funct_1__1656_17.min1.thm1.tptp2017-02-06 16:57 570  
[ ]funct_3__990_17.min1.thm1.tptp2017-02-06 16:57 315  
[ ]funct_4__1338_26.min1.thm1.tptp2017-02-06 16:57 339  
[ ]funct_5__1932_21.min1.thm1.tptp2017-02-06 16:57 359  
[ ]funct_5__1976_30.min1.thm1.tptp2017-02-06 16:57 369  
[ ]funct_5__1996_19.min1.thm1.tptp2017-02-06 16:57 341  
[ ]funct_5__2011_17.min1.thm1.tptp2017-02-06 16:57 338  
[ ]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  
[ ]goboard9__252_17.min1.thm1.tptp2017-02-06 16:57 314  
[ ]gobrd11__104_22.min1.thm1.tptp2017-02-06 16:57 340  
[ ]gobrd14__206_15.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]gobrd14__212_15.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]gobrd14__1202_18.min1.thm1.tptp2017-02-06 16:57 325  
[ ]graph_2__1228_23.min1.thm1.tptp2017-02-06 16:57 353  
[ ]graph_2__2029_24.min1.thm1.tptp2017-02-06 16:57 658  
[ ]graph_2__2041_32.min1.thm1.tptp2017-02-06 16:57 708  
[ ]graph_2__2043_28.min1.thm1.tptp2017-02-06 16:57 660  
[ ]graph_2__2048_36.min1.thm1.tptp2017-02-06 16:57 708  
[ ]grfunc_1__148_66.min1.thm1.tptp2017-02-06 16:57 574  
[ ]groeb_1__2411_26.min1.thm1.tptp2017-02-06 16:57 358  
[ ]groeb_3__501_20.min1.thm1.tptp2017-02-06 16:57 373  
[ ]group_5__1674_27.min1.thm1.tptp2017-02-06 16:57 381  
[ ]group_7__2123_18.min1.thm1.tptp2017-02-06 16:57 335  
[ ]group_7__2364_17.min1.thm1.tptp2017-02-06 16:57 309  
[ ]group_7__2486_16.min1.thm1.tptp2017-02-06 16:57 315  
[ ]group_7__2587_16.min1.thm1.tptp2017-02-06 16:57 315  
[ ]group_10__451_33.min1.thm1.tptp2017-02-06 16:57 458  
[ ]group_10__498_51.min1.thm1.tptp2017-02-06 16:57 345  
[ ]hallmar1__253_16.min1.thm1.tptp2017-02-06 16:57 779  
[ ]hallmar1__276_19.min1.thm1.tptp2017-02-06 16:57 346  
[ ]helly__1193_16.min1.thm1.tptp2017-02-06 16:57 433  
[ ]hilbert3__247_15.min1.thm1.tptp2017-02-06 16:57 340  
[ ]hilbert3__271_35.min1.thm1.tptp2017-02-06 16:57 458  
[ ]hurwitz__1227_26.min1.thm1.tptp2017-02-06 16:57 341  
[ ]hurwitz__1235_15.min1.thm1.tptp2017-02-06 16:57 881  
[ ]hurwitz__1258_26.min1.thm1.tptp2017-02-06 16:57 341  
[ ]hurwitz__1286_28.min1.thm1.tptp2017-02-06 16:57 361  
[ ]hurwitz__1381_26.min1.thm1.tptp2017-02-06 16:57 897  
[ ]ideal_1__3117_23.min1.thm1.tptp2017-02-06 16:57 313  
[ ]jgraph_5__3112_36.min1.thm1.tptp2017-02-06 16:57 383  
[ ]jgraph_5__3703_36.min1.thm1.tptp2017-02-06 16:57 383  
[ ]jgraph_5__4364_36.min1.thm1.tptp2017-02-06 16:57 382  
[ ]jgraph_5__4430_36.min1.thm1.tptp2017-02-06 16:57 382  
[ ]jgraph_5__4995_34.min1.thm1.tptp2017-02-06 16:57 408  
[ ]jgraph_5__5067_38.min1.thm1.tptp2017-02-06 16:57 408  
[ ]jgraph_5__5151_38.min1.thm1.tptp2017-02-06 16:57 408  
[ ]jgraph_5__5650_38.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jgraph_5__5732_38.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan1__2874_14.min1.thm1.tptp2017-02-06 16:57 308  
[ ]jordan1__2875_14.min1.thm1.tptp2017-02-06 16:57 308  
[ ]jordan1e__944_16.min1.thm1.tptp2017-02-06 16:57 604  
[ ]jordan1g__963_16.min1.thm1.tptp2017-02-06 16:57 604  
[ ]jordan1g__1898_14.min1.thm1.tptp2017-02-06 16:57 598  
[ ]jordan1g__2007_14.min1.thm1.tptp2017-02-06 16:57 598  
[ ]jordan1g__3953_36.min1.thm1.tptp2017-02-06 16:57 1.8K 
[ ]jordan1g__4228_28.min1.thm1.tptp2017-02-06 16:57 652  
[ ]jordan1g__4496_28.min1.thm1.tptp2017-02-06 16:57 650  
[ ]jordan1h__200_14.min1.thm1.tptp2017-02-06 16:57 699  
[ ]jordan1j__321_16.min1.thm1.tptp2017-02-06 16:57 591  
[ ]jordan1j__1996_24.min1.thm1.tptp2017-02-06 16:57 638  
[ ]jordan1j__2091_20.min1.thm1.tptp2017-02-06 16:57 627  
[ ]jordan1j__2290_24.min1.thm1.tptp2017-02-06 16:57 638  
[ ]jordan1j__2376_20.min1.thm1.tptp2017-02-06 16:57 627  
[ ]jordan1j__2857_14.min1.thm1.tptp2017-02-06 16:57 907  
[ ]jordan1j__3061_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan1j__3769_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan6__1795_19.min1.thm1.tptp2017-02-06 16:57 441  
[ ]jordan6__1886_12.min1.thm1.tptp2017-02-06 16:57 300  
[ ]jordan6__2357_24.min1.thm1.tptp2017-02-06 16:57 349  
[ ]jordan7__1031_20.min1.thm1.tptp2017-02-06 16:57 505  
[ ]jordan7__1099_20.min1.thm1.tptp2017-02-06 16:57 504  
[ ]jordan7__1420_38.min1.thm1.tptp2017-02-06 16:57 577  
[ ]jordan7__2138_42.min1.thm1.tptp2017-02-06 16:57 439  
[ ]jordan7__2447_44.min1.thm1.tptp2017-02-06 16:57 523  
[ ]jordan11__190_16.min1.thm1.tptp2017-02-06 16:57 408  
[ ]jordan12__2624_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]jordan15__2071_14.min1.thm1.tptp2017-02-06 16:57 907  
[ ]jordan15__2276_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan15__2298_26.min1.thm1.tptp2017-02-06 16:57 323  
[ ]jordan15__2987_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan15__3009_26.min1.thm1.tptp2017-02-06 16:57 323  
[ ]jordan15__3855_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan15__3877_26.min1.thm1.tptp2017-02-06 16:57 323  
[ ]jordan15__4564_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan15__4586_26.min1.thm1.tptp2017-02-06 16:57 323  
[ ]jordan15__5460_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan15__6243_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan15__7023_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan15__7803_32.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan16__278_39.min1.thm1.tptp2017-02-06 16:57 539  
[ ]jordan18__917_52.min1.thm1.tptp2017-02-06 16:57 464  
[ ]jordan19__1114_28.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan19__1807_28.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan19__2680_28.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan19__3427_28.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan19__4173_28.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan19__4919_28.min1.thm1.tptp2017-02-06 16:57 607  
[ ]jordan19__6816_36.min1.thm1.tptp2017-02-06 16:57 406  
[ ]jordan23__3183_37.min1.thm1.tptp2017-02-06 16:57 567  
[ ]jordan_a__865_45.min1.thm1.tptp2017-02-06 16:57 422  
[ ]jordan_a__943_45.min1.thm1.tptp2017-02-06 16:57 422  
[ ]kolmog01__147_27.min1.thm1.tptp2017-02-06 16:57 343  
[ ]kolmog01__149_19.min1.thm1.tptp2017-02-06 16:57 427  
[ ]kolmog01__152_47.min1.thm1.tptp2017-02-06 16:57 462  
[ ]kolmog01__161_27.min1.thm1.tptp2017-02-06 16:57 343  
[ ]kurato_1__196_29.min1.thm1.tptp2017-02-06 16:57 439  
[ ]l_hospit__1183_24.min1.thm1.tptp2017-02-06 16:57 409  
[ ]l_hospit__1226_24.min1.thm1.tptp2017-02-06 16:57 409  
[ ]l_hospit__1588_24.min1.thm1.tptp2017-02-06 16:57 409  
[ ]l_hospit__1632_24.min1.thm1.tptp2017-02-06 16:57 409  
[ ]lang1__431_50.min1.thm1.tptp2017-02-06 16:57 392  
[ ]lang1__442_50.min1.thm1.tptp2017-02-06 16:57 392  
[ ]lattice8__924_16.min1.thm1.tptp2017-02-06 16:57 530  
[ ]matrix11__1004_21.min1.thm1.tptp2017-02-06 16:57 355  
[ ]matrix11__1038_23.min1.thm1.tptp2017-02-06 16:57 393  
[ ]matrix11__1085_29.min1.thm1.tptp2017-02-06 16:57 378  
[ ]matrix11__1144_29.min1.thm1.tptp2017-02-06 16:57 378  
[ ]matrix13__4585_15.min1.thm1.tptp2017-02-06 16:57 321  
[ ]matrix13__4586_12.min1.thm1.tptp2017-02-06 16:57 321  
[ ]matrix13__4591_15.min1.thm1.tptp2017-02-06 16:57 324  
[ ]matrix13__4592_12.min1.thm1.tptp2017-02-06 16:57 324  
[ ]matrix_2__131_17.min1.thm1.tptp2017-02-06 16:57 323  
[ ]matrix_9__260_42.min1.thm1.tptp2017-02-06 16:57 396  
[ ]mcart_1__157_17.min1.thm1.tptp2017-02-06 16:57 562  
[ ]mcart_1__254_24.min1.thm1.tptp2017-02-06 16:57 595  
[ ]mcart_1__280_26.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]mcart_1__283_24.min1.thm1.tptp2017-02-06 16:57 595  
[ ]measure1__61_26.min1.thm1.tptp2017-02-06 16:57 349  
[ ]measure5__326_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]member_1__988_21.min1.thm1.tptp2017-02-06 16:57 358  
[ ]member_1__994_23.min1.thm1.tptp2017-02-06 16:57 396  
[ ]mesfunc4__461_25.min1.thm1.tptp2017-02-06 16:57 337  
[ ]mesfunc4__471_25.min1.thm1.tptp2017-02-06 16:57 338  
[ ]mesfunc4__546_25.min1.thm1.tptp2017-02-06 16:57 338  
[ ]mesfunc4__698_25.min1.thm1.tptp2017-02-06 16:57 338  
[ ]mesfunc4__701_25.min1.thm1.tptp2017-02-06 16:57 338  
[ ]mesfunc4__712_25.min1.thm1.tptp2017-02-06 16:57 338  
[ ]mesfunc5__4040_14.min1.thm1.tptp2017-02-06 16:57 424  
[ ]mmlquery__2325_37.min1.thm1.tptp2017-02-06 16:57 491  
[ ]mmlquery__2326_34.min1.thm1.tptp2017-02-06 16:57 497  
[ ]modal_1__554_25.min1.thm1.tptp2017-02-06 16:57 383  
[ ]modal_1__561_25.min1.thm1.tptp2017-02-06 16:57 384  
[ ]modelc_3__618_22.min1.thm1.tptp2017-02-06 16:57 460  
[ ]modelc_3__3524_22.min1.thm1.tptp2017-02-06 16:57 382  
[ ]modelc_3__3602_22.min1.thm1.tptp2017-02-06 16:57 382  
[ ]modelc_3__3714_31.min1.thm1.tptp2017-02-06 16:57 398  
[ ]modelc_3__3732_31.min1.thm1.tptp2017-02-06 16:57 398  
[ ]modelc_3__3806_31.min1.thm1.tptp2017-02-06 16:57 398  
[ ]mycielsk__2376_24.min1.thm1.tptp2017-02-06 16:57 363  
[ ]nagata_1__338_26.min1.thm1.tptp2017-02-06 16:57 364  
[ ]neckla_2__194_27.min1.thm1.tptp2017-02-06 16:57 397  
[ ]neckla_2__198_27.min1.thm1.tptp2017-02-06 16:57 397  
[ ]neckla_2__306_30.min1.thm1.tptp2017-02-06 16:57 481  
[ ]neckla_3__522_23.min1.thm1.tptp2017-02-06 16:57 361  
[ ]neckla_3__531_23.min1.thm1.tptp2017-02-06 16:57 361  
[ ]necklace__321_20.min1.thm1.tptp2017-02-06 16:57 384  
[ ]necklace__326_28.min1.thm1.tptp2017-02-06 16:57 348  
[ ]necklace__343_20.min1.thm1.tptp2017-02-06 16:57 384  
[ ]necklace__348_28.min1.thm1.tptp2017-02-06 16:57 348  
[ ]necklace__1503_24.min1.thm1.tptp2017-02-06 16:57 438  
[ ]necklace__1507_19.min1.thm1.tptp2017-02-06 16:57 438  
[ ]necklace__1651_22.min1.thm1.tptp2017-02-06 16:57 428  
[ ]necklace__1659_22.min1.thm1.tptp2017-02-06 16:57 418  
[ ]necklace__1676_22.min1.thm1.tptp2017-02-06 16:57 418  
[ ]numbers__138_34.min1.thm1.tptp2017-02-06 16:57 427  
[ ]numbers__943_31.min1.thm1.tptp2017-02-06 16:57 357  
[ ]orders_3__556_16.min1.thm1.tptp2017-02-06 16:57 360  
[ ]orders_3__570_17.min1.thm1.tptp2017-02-06 16:57 342  
[ ]orders_3__573_16.min1.thm1.tptp2017-02-06 16:57 412  
[ ]pcs_0__43_46.min1.thm1.tptp2017-02-06 16:57 357  
[ ]pcs_0__2362_26.min1.thm1.tptp2017-02-06 16:57 328  
[ ]pcs_0__2374_26.min1.thm1.tptp2017-02-06 16:57 328  
[ ]pcs_0__2434_26.min1.thm1.tptp2017-02-06 16:57 328  
[ ]pencil_1__345_26.min1.thm1.tptp2017-02-06 16:57 396  
[ ]pencil_1__352_30.min1.thm1.tptp2017-02-06 16:57 404  
[ ]pencil_1__366_26.min1.thm1.tptp2017-02-06 16:57 396  
[ ]pencil_1__420_24.min1.thm1.tptp2017-02-06 16:57 376  
[ ]pencil_1__462_22.min1.thm1.tptp2017-02-06 16:57 358  
[ ]pencil_1__563_26.min1.thm1.tptp2017-02-06 16:57 404  
[ ]pencil_1__570_16.min1.thm1.tptp2017-02-06 16:57 349  
[ ]pencil_1__586_26.min1.thm1.tptp2017-02-06 16:57 404  
[ ]pencil_1__593_16.min1.thm1.tptp2017-02-06 16:57 353  
[ ]pnproc_1__156_18.min1.thm1.tptp2017-02-06 16:57 331  
[ ]pre_topc__64_30.min1.thm1.tptp2017-02-06 16:57 385  
[ ]prelamb__270_16.min1.thm1.tptp2017-02-06 16:57 385  
[ ]prob_1__134_26.min1.thm1.tptp2017-02-06 16:57 331  
[ ]prob_1__230_40.min1.thm1.tptp2017-02-06 16:57 377  
[ ]qc_lang2__1433_19.min1.thm1.tptp2017-02-06 16:57 412  
[ ]qc_lang2__1439_36.min1.thm1.tptp2017-02-06 16:57 402  
[ ]qc_lang4__130_18.min1.thm1.tptp2017-02-06 16:57 315  
[ ]quaterni__119_18.min1.thm1.tptp2017-02-06 16:57 447  
[ ]quaterni__713_30.min1.thm1.tptp2017-02-06 16:57 406  
[ ]ramsey_1__1868_27.min1.thm1.tptp2017-02-06 16:57 440  
[ ]ramsey_1__1998_27.min1.thm1.tptp2017-02-06 16:57 440  
[ ]rcomp_3__363_24.min1.thm1.tptp2017-02-06 16:57 339  
[ ]rcomp_3__1430_30.min1.thm1.tptp2017-02-06 16:57 425  
[ ]relat_1__306_21.min1.thm1.tptp2017-02-06 16:57 359  
[ ]relat_1__310_26.min1.thm1.tptp2017-02-06 16:57 349  
[ ]relat_1__322_19.min1.thm1.tptp2017-02-06 16:57 349  
[ ]relat_1__326_24.min1.thm1.tptp2017-02-06 16:57 339  
[ ]rewrite1__1987_25.min1.thm1.tptp2017-02-06 16:57 356  
[ ]rewrite1__1990_25.min1.thm1.tptp2017-02-06 16:57 356  
[ ]rolle__102_25.min1.thm1.tptp2017-02-06 16:57 324  
[ ]scm_comp__342_17.min1.thm1.tptp2017-02-06 16:57 328  
[ ]scm_halt__113_18.min1.thm1.tptp2017-02-06 16:57 386  
[ ]scm_halt__1031_16.min1.thm1.tptp2017-02-06 16:57 394  
[ ]scm_halt__1182_18.min1.thm1.tptp2017-02-06 16:57 414  
[ ]scm_halt__3874_29.min1.thm1.tptp2017-02-06 16:57 409  
[ ]scmbsort__1552_25.min1.thm1.tptp2017-02-06 16:57 451  
[ ]scmbsort__1553_25.min1.thm1.tptp2017-02-06 16:57 446  
[ ]scmfsa6b__98_18.min1.thm1.tptp2017-02-06 16:57 398  
[ ]scmfsa6b__113_19.min1.thm1.tptp2017-02-06 16:57 394  
[ ]scmfsa6c__111_18.min1.thm1.tptp2017-02-06 16:57 386  
[ ]scmfsa8b__463_24.min1.thm1.tptp2017-02-06 16:57 479  
[ ]scmfsa8b__464_22.min1.thm1.tptp2017-02-06 16:57 484  
[ ]scmfsa8b__483_24.min1.thm1.tptp2017-02-06 16:57 480  
[ ]scmfsa8b__484_22.min1.thm1.tptp2017-02-06 16:57 485  
[ ]scmfsa8b__510_27.min1.thm1.tptp2017-02-06 16:57 484  
[ ]scmfsa8b__513_22.min1.thm1.tptp2017-02-06 16:57 479  
[ ]scmfsa8b__530_27.min1.thm1.tptp2017-02-06 16:57 484  
[ ]scmfsa8b__533_22.min1.thm1.tptp2017-02-06 16:57 480  
[ ]scmfsa8c__792_24.min1.thm1.tptp2017-02-06 16:57 479  
[ ]scmfsa8c__793_22.min1.thm1.tptp2017-02-06 16:57 484  
[ ]scmfsa8c__808_24.min1.thm1.tptp2017-02-06 16:57 480  
[ ]scmfsa8c__809_22.min1.thm1.tptp2017-02-06 16:57 485  
[ ]scmfsa8c__831_27.min1.thm1.tptp2017-02-06 16:57 484  
[ ]scmfsa8c__834_22.min1.thm1.tptp2017-02-06 16:57 479  
[ ]scmfsa8c__847_27.min1.thm1.tptp2017-02-06 16:57 484  
[ ]scmfsa8c__850_22.min1.thm1.tptp2017-02-06 16:57 480  
[ ]scmfsa10__870_33.min1.thm1.tptp2017-02-06 16:57 341  
[ ]scmfsa10__889_14.min1.thm1.tptp2017-02-06 16:57 376  
[ ]scmfsa10__998_33.min1.thm1.tptp2017-02-06 16:57 341  
[ ]scmfsa10__1016_14.min1.thm1.tptp2017-02-06 16:57 376  
[ ]scmfsa10__1214_23.min1.thm1.tptp2017-02-06 16:57 345  
[ ]scmfsa10__1222_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmfsa10__1230_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmfsa10__1238_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmfsa10__1246_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmfsa10__1254_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmfsa10__1294_23.min1.thm1.tptp2017-02-06 16:57 360  
[ ]scmfsa10__1302_23.min1.thm1.tptp2017-02-06 16:57 360  
[ ]scmfsa10__1310_23.min1.thm1.tptp2017-02-06 16:57 360  
[ ]scmfsa10__1318_23.min1.thm1.tptp2017-02-06 16:57 360  
[ ]scmfsa10__1323_16.min1.thm1.tptp2017-02-06 16:57 386  
[ ]scmfsa10__1528_53.min1.thm1.tptp2017-02-06 16:57 474  
[ ]scmfsa10__1529_53.min1.thm1.tptp2017-02-06 16:57 479  
[ ]scmfsa10__1550_58.min1.thm1.tptp2017-02-06 16:57 479  
[ ]scmfsa10__1557_53.min1.thm1.tptp2017-02-06 16:57 474  
[ ]scmfsa10__1573_58.min1.thm1.tptp2017-02-06 16:57 479  
[ ]scmfsa10__1580_53.min1.thm1.tptp2017-02-06 16:57 474  
[ ]scmfsa10__1598_58.min1.thm1.tptp2017-02-06 16:57 479  
[ ]scmfsa10__1605_53.min1.thm1.tptp2017-02-06 16:57 474  
[ ]scmfsa10__1623_58.min1.thm1.tptp2017-02-06 16:57 469  
[ ]scmfsa10__1631_53.min1.thm1.tptp2017-02-06 16:57 464  
[ ]scmfsa_2__296_23.min1.thm1.tptp2017-02-06 16:57 322  
[ ]scmfsa_2__308_22.min1.thm1.tptp2017-02-06 16:57 320  
[ ]scmfsa_2__334_22.min1.thm1.tptp2017-02-06 16:57 330  
[ ]scmfsa_2__343_19.min1.thm1.tptp2017-02-06 16:57 332  
[ ]scmfsa_2__465_19.min1.thm1.tptp2017-02-06 16:57 316  
[ ]scmfsa_2__490_20.min1.thm1.tptp2017-02-06 16:57 317  
[ ]scmfsa_2__707_23.min1.thm1.tptp2017-02-06 16:57 322  
[ ]scmfsa_2__735_23.min1.thm1.tptp2017-02-06 16:57 322  
[ ]scmfsa_9__258_44.min1.thm1.tptp2017-02-06 16:57 642  
[ ]scmfsa_9__277_44.min1.thm1.tptp2017-02-06 16:57 644  
[ ]scmfsa_9__302_24.min1.thm1.tptp2017-02-06 16:57 502  
[ ]scmfsa_9__303_24.min1.thm1.tptp2017-02-06 16:57 497  
[ ]scmfsa_9__337_25.min1.thm1.tptp2017-02-06 16:57 504  
[ ]scmfsa_9__338_25.min1.thm1.tptp2017-02-06 16:57 499  
[ ]scmfsa_i__231_25.min1.thm1.tptp2017-02-06 16:57 305  
[ ]scmfsa_i__247_26.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmfsa_i__541_17.min1.thm1.tptp2017-02-06 16:57 310  
[ ]scmfsa_i__577_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmisort__2065_25.min1.thm1.tptp2017-02-06 16:57 450  
[ ]scmisort__2066_25.min1.thm1.tptp2017-02-06 16:57 445  
[ ]scmpds_2__195_24.min1.thm1.tptp2017-02-06 16:57 308  
[ ]scmpds_2__269_17.min1.thm1.tptp2017-02-06 16:57 314  
[ ]scmpds_2__447_21.min1.thm1.tptp2017-02-06 16:57 308  
[ ]scmpds_2__541_17.min1.thm1.tptp2017-02-06 16:57 308  
[ ]scmpds_2__562_17.min1.thm1.tptp2017-02-06 16:57 308  
[ ]scmpds_4__529_25.min1.thm1.tptp2017-02-06 16:57 815  
[ ]scmpds_4__530_20.min1.thm1.tptp2017-02-06 16:57 802  
[ ]scmpds_7__3065_22.min1.thm1.tptp2017-02-06 16:57 386  
[ ]scmpds_7__3100_20.min1.thm1.tptp2017-02-06 16:57 442  
[ ]scmpds_7__3191_24.min1.thm1.tptp2017-02-06 16:57 385  
[ ]scmpds_7__3225_22.min1.thm1.tptp2017-02-06 16:57 433  
[ ]scmpds_9__372_30.min1.thm1.tptp2017-02-06 16:57 393  
[ ]scmpds_9__378_14.min1.thm1.tptp2017-02-06 16:57 457  
[ ]scmpds_9__461_30.min1.thm1.tptp2017-02-06 16:57 393  
[ ]scmpds_9__467_14.min1.thm1.tptp2017-02-06 16:57 457  
[ ]scmpds_9__549_30.min1.thm1.tptp2017-02-06 16:57 393  
[ ]scmpds_9__555_14.min1.thm1.tptp2017-02-06 16:57 457  
[ ]scmring3__865_19.min1.thm1.tptp2017-02-06 16:57 335  
[ ]scmring3__896_14.min1.thm1.tptp2017-02-06 16:57 379  
[ ]scmring3__1011_23.min1.thm1.tptp2017-02-06 16:57 345  
[ ]scmring3__1019_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmring3__1027_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmring3__1035_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmring3__1043_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmring3__1071_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]scmring3__1076_16.min1.thm1.tptp2017-02-06 16:57 386  
[ ]scmring3__1255_55.min1.thm1.tptp2017-02-06 16:57 682  
[ ]scmring3__1261_55.min1.thm1.tptp2017-02-06 16:57 687  
[ ]scmring3__1293_60.min1.thm1.tptp2017-02-06 16:57 687  
[ ]scmring3__1299_55.min1.thm1.tptp2017-02-06 16:57 682  
[ ]scmring3__1341_60.min1.thm1.tptp2017-02-06 16:57 687  
[ ]scmring3__1345_55.min1.thm1.tptp2017-02-06 16:57 682  
[ ]scmring3__1383_62.min1.thm1.tptp2017-02-06 16:57 703  
[ ]scmring3__1387_57.min1.thm1.tptp2017-02-06 16:57 698  
[ ]scmyciel__55_19.min1.thm1.tptp2017-02-06 16:57 336  
[ ]scmyciel__280_21.min1.thm1.tptp2017-02-06 16:57 357  
[ ]scmyciel__908_16.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmyciel__921_16.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmyciel__924_21.min1.thm1.tptp2017-02-06 16:57 331  
[ ]scmyciel__929_24.min1.thm1.tptp2017-02-06 16:57 339  
[ ]scmyciel__932_24.min1.thm1.tptp2017-02-06 16:57 354  
[ ]scmyciel__1316_27.min1.thm1.tptp2017-02-06 16:57 417  
[ ]scmyciel__1388_18.min1.thm1.tptp2017-02-06 16:57 372  
[ ]scmyciel__1395_28.min1.thm1.tptp2017-02-06 16:57 372  
[ ]scmyciel__1414_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]scmyciel__1753_18.min1.thm1.tptp2017-02-06 16:57 372  
[ ]scmyciel__1759_33.min1.thm1.tptp2017-02-06 16:57 372  
[ ]scmyciel__2034_54.min1.thm1.tptp2017-02-06 16:57 532  
[ ]scmyciel__3149_25.min1.thm1.tptp2017-02-06 16:57 814  
[ ]scmyciel__3192_32.min1.thm1.tptp2017-02-06 16:57 474  
[ ]setfam_1__219_49.min1.thm1.tptp2017-02-06 16:57 400  
[ ]setwiseo__841_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]setwop_2__165_24.min1.thm1.tptp2017-02-06 16:57 343  
[ ]simplex1__2671_23.min1.thm1.tptp2017-02-06 16:57 344  
[ ]simplex1__3356_16.min1.thm1.tptp2017-02-06 16:57 499  
[ ]simplex1__3690_15.min1.thm1.tptp2017-02-06 16:57 521  
[ ]simplex1__4154_27.min1.thm1.tptp2017-02-06 16:57 377  
[ ]sin_cos9__449_14.min1.thm1.tptp2017-02-06 16:57 686  
[ ]sincos10__870_14.min1.thm1.tptp2017-02-06 16:57 542  
[ ]sincos10__955_14.min1.thm1.tptp2017-02-06 16:57 706  
[ ]sincos10__996_14.min1.thm1.tptp2017-02-06 16:57 618  
[ ]sincos10__1828_14.min1.thm1.tptp2017-02-06 16:57 478  
[ ]sincos10__1930_14.min1.thm1.tptp2017-02-06 16:57 478  
[ ]sppol_2__2899_18.min1.thm1.tptp2017-02-06 16:57 366  
[ ]sppol_2__3145_21.min1.thm1.tptp2017-02-06 16:57 352  
[ ]sprect_1__83_17.min1.thm1.tptp2017-02-06 16:57 336  
[ ]sprect_1__173_48.min1.thm1.tptp2017-02-06 16:57 667  
[ ]sprect_1__845_15.min1.thm1.tptp2017-02-06 16:57 310  
[ ]sprect_3__1363_21.min1.thm1.tptp2017-02-06 16:57 514  
[ ]sprect_3__1368_21.min1.thm1.tptp2017-02-06 16:57 514  
[ ]sprect_3__1465_21.min1.thm1.tptp2017-02-06 16:57 518  
[ ]sprect_3__2303_22.min1.thm1.tptp2017-02-06 16:57 432  
[ ]sprect_3__2326_23.min1.thm1.tptp2017-02-06 16:57 433  
[ ]sprect_3__2357_20.min1.thm1.tptp2017-02-06 16:57 310  
[ ]sprect_3__2457_22.min1.thm1.tptp2017-02-06 16:57 428  
[ ]sprect_3__2467_23.min1.thm1.tptp2017-02-06 16:57 429  
[ ]sprect_3__2562_23.min1.thm1.tptp2017-02-06 16:57 428  
[ ]sprect_3__2584_24.min1.thm1.tptp2017-02-06 16:57 429  
[ ]struct_0__437_13.min1.thm1.tptp2017-02-06 16:57 273  
[ ]struct_0__541_22.min1.thm1.tptp2017-02-06 16:57 298  
[ ]tdlat_3__283_44.min1.thm1.tptp2017-02-06 16:57 378  
[ ]tdlat_3__528_19.min1.thm1.tptp2017-02-06 16:57 377  
[ ]tdlat_3__627_45.min1.thm1.tptp2017-02-06 16:57 397  
[ ]tex_1__920_40.min1.thm1.tptp2017-02-06 16:57 318  
[ ]tex_1__925_13.min1.thm1.tptp2017-02-06 16:57 317  
[ ]tex_1__1579_18.min1.thm1.tptp2017-02-06 16:57 317  
[ ]tex_1__1799_40.min1.thm1.tptp2017-02-06 16:57 318  
[ ]tex_1__1804_13.min1.thm1.tptp2017-02-06 16:57 317  
[ ]toler_1__462_21.min1.thm1.tptp2017-02-06 16:57 349  
[ ]toler_1__463_21.min1.thm1.tptp2017-02-06 16:57 349  
[ ]toler_1__657_21.min1.thm1.tptp2017-02-06 16:57 349  
[ ]toler_1__658_21.min1.thm1.tptp2017-02-06 16:57 349  
[ ]toler_1__667_15.min1.thm1.tptp2017-02-06 16:57 336  
[ ]topalg_4__43_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]topdim_2__1708_32.min1.thm1.tptp2017-02-06 16:57 518  
[ ]topmetr3__1429_48.min1.thm1.tptp2017-02-06 16:57 524  
[ ]topreal1__1395_19.min1.thm1.tptp2017-02-06 16:57 651  
[ ]topreal1__1519_19.min1.thm1.tptp2017-02-06 16:57 651  
[ ]topreal2__5061_21.min1.thm1.tptp2017-02-06 16:57 349  
[ ]topreal2__5069_21.min1.thm1.tptp2017-02-06 16:57 349  
[ ]topreal3__461_23.min1.thm1.tptp2017-02-06 16:57 477  
[ ]topreal6__275_17.min1.thm1.tptp2017-02-06 16:57 312  
[ ]topreal6__574_17.min1.thm1.tptp2017-02-06 16:57 487  
[ ]topreal6__1087_20.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]topreal6__1095_15.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]topreal6__2015_15.min1.thm1.tptp2017-02-06 16:57 483  
[ ]topreal9__1046_24.min1.thm1.tptp2017-02-06 16:57 334  
[ ]topreal9__1104_24.min1.thm1.tptp2017-02-06 16:57 348  
[ ]topreal9__1148_27.min1.thm1.tptp2017-02-06 16:57 344  
[ ]topreal9__1159_32.min1.thm1.tptp2017-02-06 16:57 390  
[ ]topreal9__1187_32.min1.thm1.tptp2017-02-06 16:57 384  
[ ]topreal9__1201_22.min1.thm1.tptp2017-02-06 16:57 368  
[ ]topreal9__1410_24.min1.thm1.tptp2017-02-06 16:57 386  
[ ]topreal9__1464_28.min1.thm1.tptp2017-02-06 16:57 350  
[ ]topreala__192_15.min1.thm1.tptp2017-02-06 16:57 445  
[ ]trees_1__1633_25.min1.thm1.tptp2017-02-06 16:57 339  
[ ]trees_1__1634_22.min1.thm1.tptp2017-02-06 16:57 339  
[ ]trees_3__452_17.min1.thm1.tptp2017-02-06 16:57 338  
[ ]trees_3__471_17.min1.thm1.tptp2017-02-06 16:57 338  
[ ]trees_3__490_17.min1.thm1.tptp2017-02-06 16:57 338  
[ ]trees_3__2858_20.min1.thm1.tptp2017-02-06 16:57 340  
[ ]twoscomp__1517_55.min1.thm1.tptp2017-02-06 16:57 732  
[ ]urysohn2__139_44.min1.thm1.tptp2017-02-06 16:57 415  
[ ]urysohn2__142_44.min1.thm1.tptp2017-02-06 16:57 415  
[ ]waybel18__1454_21.min1.thm1.tptp2017-02-06 16:57 328  
[ ]waybel18__1532_29.min1.thm1.tptp2017-02-06 16:57 452  
[ ]xboole_0__76_21.min1.thm1.tptp2017-02-06 16:57 423  
[ ]xreal_0__51_52.min1.thm1.tptp2017-02-06 16:57 439  
[ ]xtuple_0__46_21.min1.thm1.tptp2017-02-06 16:57 327  
[ ]xtuple_0__368_18.min1.thm1.tptp2017-02-06 16:57 362  
[ ]xtuple_0__379_20.min1.thm1.tptp2017-02-06 16:57 378  
[ ]xtuple_0__382_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]xxreal_1__2252_38.min1.thm1.tptp2017-02-06 16:57 525  
[ ]xxreal_1__2257_40.min1.thm1.tptp2017-02-06 16:57 521  
[ ]xxreal_2__504_15.min1.thm1.tptp2017-02-06 16:57 340  
[ ]xxreal_2__544_15.min1.thm1.tptp2017-02-06 16:57 340  
[ ]xxreal_2__2277_14.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_2__2308_14.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_2__2342_14.min1.thm1.tptp2017-02-06 16:57 523  
[ ]xxreal_2__2376_14.min1.thm1.tptp2017-02-06 16:57 523  
[ ]yellow_0__340_20.min1.thm1.tptp2017-02-06 16:57 487  
[ ]yellow_0__347_16.min1.thm1.tptp2017-02-06 16:57 473  
[ ]yellow_1__520_19.min1.thm1.tptp2017-02-06 16:57 350  
[ ]yellow_1__560_19.min1.thm1.tptp2017-02-06 16:57 350  
[ ]yellow_9__639_19.min1.thm1.tptp2017-02-06 16:57 358  
[ ]yellow_9__646_26.min1.thm1.tptp2017-02-06 16:57 358  
[ ]yellow_9__660_24.min1.thm1.tptp2017-02-06 16:57 350  
[ ]yellow_9__664_25.min1.thm1.tptp2017-02-06 16:57 340  
[ ]zf_fund1__1450_17.min1.thm1.tptp2017-02-06 16:57 347  
[ ]zf_fund1__1472_30.min1.thm1.tptp2017-02-06 16:57 518  
[ ]zf_fund1__1663_25.min1.thm1.tptp2017-02-06 16:57 352  
[ ]zf_fund2__99_23.min1.thm1.tptp2017-02-06 16:57 608  
[ ]zf_lang1__966_31.min1.thm1.tptp2017-02-06 16:57 414  
[ ]zf_lang1__980_30.min1.thm1.tptp2017-02-06 16:57 412  
[ ]zf_lang1__1933_24.min1.thm1.tptp2017-02-06 16:57 357  
[ ]zf_lang1__1962_24.min1.thm1.tptp2017-02-06 16:57 357  
[ ]zf_lang1__2714_23.min1.thm1.tptp2017-02-06 16:57 327  
[ ]zf_model__752_30.min1.thm1.tptp2017-02-06 16:57 403  
[ ]zfmisc_1__117_28.min1.thm1.tptp2017-02-06 16:57 385  
[ ]zfmisc_1__201_21.min1.thm1.tptp2017-02-06 16:57 334  
[ ]zfmisc_1__227_17.min1.thm1.tptp2017-02-06 16:57 312  
[ ]zfmisc_1__350_17.min1.thm1.tptp2017-02-06 16:57 342  
[ ]zfmisc_1__384_17.min1.thm1.tptp2017-02-06 16:57 356  
[ ]zfmisc_1__528_21.min1.thm1.tptp2017-02-06 16:57 422  
[ ]zfmisc_1__595_16.min1.thm1.tptp2017-02-06 16:57 342  
[ ]zfmisc_1__603_21.min1.thm1.tptp2017-02-06 16:57 368  
[ ]zfmisc_1__610_26.min1.thm1.tptp2017-02-06 16:57 417  
[ ]zfmisc_1__624_21.min1.thm1.tptp2017-02-06 16:57 368  
[ ]zfmisc_1__765_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]zfmisc_1__789_4.min1.thm1.tptp2017-02-06 16:57 735  
[ ]zfmisc_1__1773_19.min1.thm1.tptp2017-02-06 16:57 360  
[ ]zfmisc_1__2353_19.min1.thm1.tptp2017-02-06 16:57 366  
[ ]zfmisc_1__2356_19.min1.thm1.tptp2017-02-06 16:57 383  
[ ]zfmisc_1__2359_26.min1.thm1.tptp2017-02-06 16:57 421  
[ ]zfmodel1__925_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]zfmodel1__941_26.min1.thm1.tptp2017-02-06 16:57 358  
[ ]zfmodel1__1208_30.min1.thm1.tptp2017-02-06 16:57 395  
[ ]zfmodel1__1223_30.min1.thm1.tptp2017-02-06 16:57 395  
[ ]zfmodel1__1500_30.min1.thm1.tptp2017-02-06 16:57 376  
[ ]zfmodel1__1668_30.min1.thm1.tptp2017-02-06 16:57 376  
Apache/2.4.18 (Ubuntu) Server at grid01.ciirc.cvut.cz Port 80