Index of /~mptp/7.13.01_4.181.1147/mptp/ilp1/d1_tarski

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[ ]abcmiz_1__1629_49.min1.thm1.tptp2017-02-06 16:57 285  
[ ]abcmiz_1__1742_56.min1.thm1.tptp2017-02-06 16:57 537  
[ ]abcmiz_1__2558_38.min1.thm1.tptp2017-02-06 16:57 341  
[ ]abcmiz_1__4879_23.min1.thm1.tptp2017-02-06 16:57 332  
[ ]abcmiz_1__4954_16.min1.thm1.tptp2017-02-06 16:57 368  
[ ]abcmiz_1__4976_15.min1.thm1.tptp2017-02-06 16:57 348  
[ ]abcmiz_1__5147_15.min1.thm1.tptp2017-02-06 16:57 324  
[ ]abcmiz_1__5150_21.min1.thm1.tptp2017-02-06 16:57 325  
[ ]abcmiz_1__5208_28.min1.thm1.tptp2017-02-06 16:57 310  
[ ]abcmiz_1__5435_27.min1.thm1.tptp2017-02-06 16:57 310  
[ ]abcmiz_1__5703_28.min1.thm1.tptp2017-02-06 16:57 311  
[ ]abcmiz_a__1055_28.min1.thm1.tptp2017-02-06 16:57 469  
[ ]afinsq_1__718_16.min1.thm1.tptp2017-02-06 16:57 288  
[ ]afinsq_1__816_17.min1.thm1.tptp2017-02-06 16:57 316  
[ ]afinsq_1__878_18.min1.thm1.tptp2017-02-06 16:57 358  
[ ]afinsq_1__887_15.min1.thm1.tptp2017-02-06 16:57 268  
[ ]afinsq_1__941_13.min1.thm1.tptp2017-02-06 16:57 268  
[ ]afinsq_1__1038_16.min1.thm1.tptp2017-02-06 16:57 340  
[ ]afinsq_1__2359_36.min1.thm1.tptp2017-02-06 16:57 349  
[ ]afinsq_2__3780_10.min1.thm1.tptp2017-02-06 16:57 284  
[ ]afinsq_2__3781_17.min1.thm1.tptp2017-02-06 16:57 336  
[ ]afinsq_2__3802_18.min1.thm1.tptp2017-02-06 16:57 342  
[ ]algseq_1__392_21.min1.thm1.tptp2017-02-06 16:57 312  
[ ]algstr_1__87_14.min1.thm1.tptp2017-02-06 16:57 292  
[ ]algstr_4__1427_20.min1.thm1.tptp2017-02-06 16:57 326  
[ ]algstr_4__2107_12.min1.thm1.tptp2017-02-06 16:57 298  
[ ]algstr_4__3055_23.min1.thm1.tptp2017-02-06 16:57 322  
[ ]algstr_4__3141_17.min1.thm1.tptp2017-02-06 16:57 481  
[ ]algstr_4__3195_48.min1.thm1.tptp2017-02-06 16:57 356  
[ ]algstr_4__3392_15.min1.thm1.tptp2017-02-06 16:57 506  
[ ]altcat_1__551_15.min1.thm1.tptp2017-02-06 16:57 302  
[ ]altcat_1__555_19.min1.thm1.tptp2017-02-06 16:57 304  
[ ]altcat_1__1163_32.min1.thm1.tptp2017-02-06 16:57 602  
[ ]altcat_1__1458_20.min1.thm1.tptp2017-02-06 16:57 342  
[ ]altcat_1__1476_18.min1.thm1.tptp2017-02-06 16:57 331  
[ ]altcat_3__1231_72.min1.thm1.tptp2017-02-06 16:57 482  
[ ]altcat_3__1320_72.min1.thm1.tptp2017-02-06 16:57 482  
[ ]ami_2__77_39.min1.thm1.tptp2017-02-06 16:57 312  
[ ]ami_4__723_23.min1.thm1.tptp2017-02-06 16:57 350  
[ ]ami_5__490_27.min1.thm1.tptp2017-02-06 16:57 273  
[ ]ami_5__572_40.min1.thm1.tptp2017-02-06 16:57 386  
[ ]ami_5__585_33.min1.thm1.tptp2017-02-06 16:57 362  
[ ]ami_5__655_40.min1.thm1.tptp2017-02-06 16:57 386  
[ ]ami_5__669_33.min1.thm1.tptp2017-02-06 16:57 372  
[ ]ami_6__82_11.min1.thm1.tptp2017-02-06 16:57 244  
[ ]ami_6__101_22.min1.thm1.tptp2017-02-06 16:57 254  
[ ]ami_6__106_17.min1.thm1.tptp2017-02-06 16:57 246  
[ ]ami_6__127_22.min1.thm1.tptp2017-02-06 16:57 254  
[ ]ami_6__132_17.min1.thm1.tptp2017-02-06 16:57 246  
[ ]ami_6__153_22.min1.thm1.tptp2017-02-06 16:57 254  
[ ]ami_6__158_17.min1.thm1.tptp2017-02-06 16:57 246  
[ ]ami_6__179_22.min1.thm1.tptp2017-02-06 16:57 254  
[ ]ami_6__184_17.min1.thm1.tptp2017-02-06 16:57 246  
[ ]ami_6__205_22.min1.thm1.tptp2017-02-06 16:57 254  
[ ]ami_6__210_17.min1.thm1.tptp2017-02-06 16:57 246  
[ ]ami_6__332_54.min1.thm1.tptp2017-02-06 16:57 448  
[ ]ami_6__369_57.min1.thm1.tptp2017-02-06 16:57 474  
[ ]ami_6__406_57.min1.thm1.tptp2017-02-06 16:57 474  
[ ]ami_6__615_12.min1.thm1.tptp2017-02-06 16:57 260  
[ ]ami_6__691_26.min1.thm1.tptp2017-02-06 16:57 331  
[ ]ami_6__713_26.min1.thm1.tptp2017-02-06 16:57 321  
[ ]ami_6__752_12.min1.thm1.tptp2017-02-06 16:57 260  
[ ]ami_6__820_26.min1.thm1.tptp2017-02-06 16:57 321  
[ ]ami_6__841_26.min1.thm1.tptp2017-02-06 16:57 331  
[ ]ami_6__880_12.min1.thm1.tptp2017-02-06 16:57 260  
[ ]ami_6__1002_18.min1.thm1.tptp2017-02-06 16:57 268  
[ ]ami_6__1012_23.min1.thm1.tptp2017-02-06 16:57 294  
[ ]ami_wstd__548_23.min1.thm1.tptp2017-02-06 16:57 396  
[ ]amistd_2__141_14.min1.thm1.tptp2017-02-06 16:57 272  
[ ]amistd_2__165_19.min1.thm1.tptp2017-02-06 16:57 264  
[ ]amistd_2__190_14.min1.thm1.tptp2017-02-06 16:57 272  
[ ]amistd_2__206_19.min1.thm1.tptp2017-02-06 16:57 264  
[ ]amistd_3__530_25.min1.thm1.tptp2017-02-06 16:57 404  
[ ]amistd_3__594_30.min1.thm1.tptp2017-02-06 16:57 428  
[ ]amistd_3__660_20.min1.thm1.tptp2017-02-06 16:57 386  
[ ]amistd_4__724_17.min1.thm1.tptp2017-02-06 16:57 296  
[ ]amistd_5__542_51.min1.thm1.tptp2017-02-06 16:57 716  
[ ]amistd_5__614_60.min1.thm1.tptp2017-02-06 16:57 828  
[ ]amistd_5__726_6.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]aofa_000__2731_23.min1.thm1.tptp2017-02-06 16:57 388  
[ ]aofa_000__2746_34.min1.thm1.tptp2017-02-06 16:57 293  
[ ]aofa_000__3797_51.min1.thm1.tptp2017-02-06 16:57 526  
[ ]aofa_000__6988_26.min1.thm1.tptp2017-02-06 16:57 312  
[ ]aofa_000__7150_26.min1.thm1.tptp2017-02-06 16:57 312  
[ ]aofa_000__7359_26.min1.thm1.tptp2017-02-06 16:57 312  
[ ]armstrng__485_13.min1.thm1.tptp2017-02-06 16:57 289  
[ ]armstrng__2203_25.min1.thm1.tptp2017-02-06 16:57 367  
[ ]armstrng__2279_24.min1.thm1.tptp2017-02-06 16:57 364  
[ ]armstrng__2934_14.min1.thm1.tptp2017-02-06 16:57 344  
[ ]armstrng__2935_14.min1.thm1.tptp2017-02-06 16:57 344  
[ ]armstrng__2941_19.min1.thm1.tptp2017-02-06 16:57 366  
[ ]armstrng__2947_19.min1.thm1.tptp2017-02-06 16:57 366  
[ ]armstrng__3011_27.min1.thm1.tptp2017-02-06 16:57 314  
[ ]armstrng__3067_27.min1.thm1.tptp2017-02-06 16:57 371  
[ ]armstrng__3071_16.min1.thm1.tptp2017-02-06 16:57 290  
[ ]armstrng__3095_22.min1.thm1.tptp2017-02-06 16:57 286  
[ ]armstrng__3301_13.min1.thm1.tptp2017-02-06 16:57 274  
[ ]armstrng__3800_12.min1.thm1.tptp2017-02-06 16:57 284  
[ ]armstrng__3801_23.min1.thm1.tptp2017-02-06 16:57 370  
[ ]arrow__66_17.min1.thm1.tptp2017-02-06 16:57 250  
[ ]arytm_0__47_28.min1.thm1.tptp2017-02-06 16:57 350  
[ ]arytm_0__62_24.min1.thm1.tptp2017-02-06 16:57 300  
[ ]arytm_0__95_12.min1.thm1.tptp2017-02-06 16:57 254  
[ ]arytm_0__558_21.min1.thm1.tptp2017-02-06 16:57 323  
[ ]arytm_0__570_32.min1.thm1.tptp2017-02-06 16:57 388  
[ ]arytm_0__720_14.min1.thm1.tptp2017-02-06 16:57 286  
[ ]arytm_0__722_19.min1.thm1.tptp2017-02-06 16:57 316  
[ ]arytm_0__752_30.min1.thm1.tptp2017-02-06 16:57 358  
[ ]arytm_0__778_20.min1.thm1.tptp2017-02-06 16:57 332  
[ ]arytm_0__780_25.min1.thm1.tptp2017-02-06 16:57 342  
[ ]arytm_2__378_17.min1.thm1.tptp2017-02-06 16:57 473  
[ ]arytm_2__2283_27.min1.thm1.tptp2017-02-06 16:57 277  
[ ]arytm_3__1890_20.min1.thm1.tptp2017-02-06 16:57 274  
[ ]arytm_3__1901_18.min1.thm1.tptp2017-02-06 16:57 342  
[ ]arytm_3__1903_20.min1.thm1.tptp2017-02-06 16:57 306  
[ ]arytm_3__1906_15.min1.thm1.tptp2017-02-06 16:57 284  
[ ]bagorder__402_22.min1.thm1.tptp2017-02-06 16:57 338  
[ ]bagorder__528_22.min1.thm1.tptp2017-02-06 16:57 338  
[ ]bcialg_1__1166_18.min1.thm1.tptp2017-02-06 16:57 304  
[ ]bcialg_1__1176_31.min1.thm1.tptp2017-02-06 16:57 520  
[ ]bcialg_1__1178_19.min1.thm1.tptp2017-02-06 16:57 304  
[ ]bcialg_1__1193_17.min1.thm1.tptp2017-02-06 16:57 354  
[ ]bcialg_5__953_57.min1.thm1.tptp2017-02-06 16:57 454  
[ ]bcialg_5__981_54.min1.thm1.tptp2017-02-06 16:57 342  
[ ]bcialg_5__989_15.min1.thm1.tptp2017-02-06 16:57 298  
[ ]bciideal__177_41.min1.thm1.tptp2017-02-06 16:57 527  
[ ]bciideal__189_21.min1.thm1.tptp2017-02-06 16:57 308  
[ ]bciideal__202_19.min1.thm1.tptp2017-02-06 16:57 304  
[ ]bciideal__255_18.min1.thm1.tptp2017-02-06 16:57 492  
[ ]bciideal__275_21.min1.thm1.tptp2017-02-06 16:57 312  
[ ]bciideal__280_13.min1.thm1.tptp2017-02-06 16:57 304  
[ ]bciideal__685_18.min1.thm1.tptp2017-02-06 16:57 304  
[ ]bciideal__693_31.min1.thm1.tptp2017-02-06 16:57 520  
[ ]bciideal__695_19.min1.thm1.tptp2017-02-06 16:57 304  
[ ]bciideal__919_19.min1.thm1.tptp2017-02-06 16:57 312  
[ ]bciideal__948_26.min1.thm1.tptp2017-02-06 16:57 410  
[ ]binom__1508_17.min1.thm1.tptp2017-02-06 16:57 380  
[ ]binom__1641_20.min1.thm1.tptp2017-02-06 16:57 340  
[ ]binom__1750_16.min1.thm1.tptp2017-02-06 16:57 258  
[ ]boolmark__420_17.min1.thm1.tptp2017-02-06 16:57 613  
[ ]borsuk_1__2017_30.min1.thm1.tptp2017-02-06 16:57 365  
[ ]borsuk_3__606_23.min1.thm1.tptp2017-02-06 16:57 314  
[ ]borsuk_3__1212_23.min1.thm1.tptp2017-02-06 16:57 314  
[ ]borsuk_6__1758_16.min1.thm1.tptp2017-02-06 16:57 310  
[ ]borsuk_6__1910_16.min1.thm1.tptp2017-02-06 16:57 310  
[ ]borsuk_6__3131_15.min1.thm1.tptp2017-02-06 16:57 295  
[ ]borsuk_6__3592_15.min1.thm1.tptp2017-02-06 16:57 298  
[ ]borsuk_7__513_19.min1.thm1.tptp2017-02-06 16:57 273  
[ ]borsuk_7__516_19.min1.thm1.tptp2017-02-06 16:57 273  
[ ]brouwer__143_12.min1.thm1.tptp2017-02-06 16:57 258  
[ ]bvfunc11__120_21.min1.thm1.tptp2017-02-06 16:57 269  
[ ]bvfunc14__197_21.min1.thm1.tptp2017-02-06 16:57 269  
[ ]bvfunc14__550_21.min1.thm1.tptp2017-02-06 16:57 439  
[ ]bvfunc14__554_21.min1.thm1.tptp2017-02-06 16:57 270  
[ ]bvfunc14__662_22.min1.thm1.tptp2017-02-06 16:57 285  
[ ]bvfunc14__1055_22.min1.thm1.tptp2017-02-06 16:57 473  
[ ]bvfunc14__1059_22.min1.thm1.tptp2017-02-06 16:57 290  
[ ]bvfunc14__2102_22.min1.thm1.tptp2017-02-06 16:57 290  
[ ]bvfunc14__2142_24.min1.thm1.tptp2017-02-06 16:57 473  
[ ]bvfunc14__3205_27.min1.thm1.tptp2017-02-06 16:57 449  
[ ]bvfunc14__3215_22.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bvfunc14__3874_21.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bvfunc14__3941_27.min1.thm1.tptp2017-02-06 16:57 449  
[ ]bvfunc14__4708_21.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bvfunc14__4803_27.min1.thm1.tptp2017-02-06 16:57 449  
[ ]bvfunc14__5711_27.min1.thm1.tptp2017-02-06 16:57 449  
[ ]bvfunc14__5722_21.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bvfunc_1__2235_27.min1.thm1.tptp2017-02-06 16:57 390  
[ ]bvfunc_1__2267_25.min1.thm1.tptp2017-02-06 16:57 386  
[ ]bvfunc_1__2578_20.min1.thm1.tptp2017-02-06 16:57 289  
[ ]calcul_1__1698_15.min1.thm1.tptp2017-02-06 16:57 299  
[ ]calcul_1__1779_15.min1.thm1.tptp2017-02-06 16:57 299  
[ ]calcul_1__1901_15.min1.thm1.tptp2017-02-06 16:57 299  
[ ]calcul_1__2022_15.min1.thm1.tptp2017-02-06 16:57 299  
[ ]calcul_1__2139_15.min1.thm1.tptp2017-02-06 16:57 299  
[ ]calcul_1__2214_15.min1.thm1.tptp2017-02-06 16:57 299  
[ ]calcul_1__2289_15.min1.thm1.tptp2017-02-06 16:57 299  
[ ]calcul_1__2365_15.min1.thm1.tptp2017-02-06 16:57 299  
[ ]calcul_1__3133_17.min1.thm1.tptp2017-02-06 16:57 300  
[ ]calcul_2__169_16.min1.thm1.tptp2017-02-06 16:57 316  
[ ]calcul_2__177_14.min1.thm1.tptp2017-02-06 16:57 284  
[ ]calcul_2__992_20.min1.thm1.tptp2017-02-06 16:57 278  
[ ]calcul_2__999_12.min1.thm1.tptp2017-02-06 16:57 270  
[ ]card_1__399_26.min1.thm1.tptp2017-02-06 16:57 466  
[ ]card_1__804_12.min1.thm1.tptp2017-02-06 16:57 258  
[ ]card_1__972_20.min1.thm1.tptp2017-02-06 16:57 305  
[ ]card_1__974_23.min1.thm1.tptp2017-02-06 16:57 273  
[ ]card_1__990_14.min1.thm1.tptp2017-02-06 16:57 263  
[ ]card_1__993_26.min1.thm1.tptp2017-02-06 16:57 265  
[ ]card_1__1193_16.min1.thm1.tptp2017-02-06 16:57 286  
[ ]card_1__1906_13.min1.thm1.tptp2017-02-06 16:57 264  
[ ]card_1__1996_13.min1.thm1.tptp2017-02-06 16:57 272  
[ ]card_2__286_15.min1.thm1.tptp2017-02-06 16:57 268  
[ ]card_2__482_13.min1.thm1.tptp2017-02-06 16:57 260  
[ ]card_2__691_15.min1.thm1.tptp2017-02-06 16:57 292  
[ ]card_2__702_16.min1.thm1.tptp2017-02-06 16:57 292  
[ ]card_2__1422_26.min1.thm1.tptp2017-02-06 16:57 277  
[ ]card_2__1424_19.min1.thm1.tptp2017-02-06 16:57 274  
[ ]card_2__1432_17.min1.thm1.tptp2017-02-06 16:57 335  
[ ]card_2__1656_25.min1.thm1.tptp2017-02-06 16:57 337  
[ ]card_2__1661_19.min1.thm1.tptp2017-02-06 16:57 329  
[ ]card_3__306_12.min1.thm1.tptp2017-02-06 16:57 369  
[ ]card_3__362_19.min1.thm1.tptp2017-02-06 16:57 262  
[ ]card_3__367_13.min1.thm1.tptp2017-02-06 16:57 254  
[ ]card_3__530_12.min1.thm1.tptp2017-02-06 16:57 266  
[ ]card_3__537_12.min1.thm1.tptp2017-02-06 16:57 310  
[ ]card_3__2186_16.min1.thm1.tptp2017-02-06 16:57 254  
[ ]card_3__2332_17.min1.thm1.tptp2017-02-06 16:57 369  
[ ]card_3__2608_15.min1.thm1.tptp2017-02-06 16:57 274  
[ ]card_3__2609_17.min1.thm1.tptp2017-02-06 16:57 347  
[ ]card_3__2636_29.min1.thm1.tptp2017-02-06 16:57 292  
[ ]card_3__2666_21.min1.thm1.tptp2017-02-06 16:57 278  
[ ]card_fil__71_15.min1.thm1.tptp2017-02-06 16:57 272  
[ ]card_fil__80_26.min1.thm1.tptp2017-02-06 16:57 356  
[ ]card_fil__86_19.min1.thm1.tptp2017-02-06 16:57 320  
[ ]card_fil__88_19.min1.thm1.tptp2017-02-06 16:57 268  
[ ]card_fil__1481_24.min1.thm1.tptp2017-02-06 16:57 317  
[ ]card_fil__1698_19.min1.thm1.tptp2017-02-06 16:57 424  
[ ]card_fil__1713_19.min1.thm1.tptp2017-02-06 16:57 390  
[ ]card_fil__1850_18.min1.thm1.tptp2017-02-06 16:57 275  
[ ]card_fil__2054_19.min1.thm1.tptp2017-02-06 16:57 278  
[ ]card_fin__393_23.min1.thm1.tptp2017-02-06 16:57 290  
[ ]card_fin__491_21.min1.thm1.tptp2017-02-06 16:57 274  
[ ]card_fin__728_21.min1.thm1.tptp2017-02-06 16:57 394  
[ ]card_fin__1104_12.min1.thm1.tptp2017-02-06 16:57 334  
[ ]card_fin__1196_13.min1.thm1.tptp2017-02-06 16:57 334  
[ ]card_fin__1221_13.min1.thm1.tptp2017-02-06 16:57 326  
[ ]card_fin__1239_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]card_fin__1242_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]card_fin__1263_13.min1.thm1.tptp2017-02-06 16:57 326  
[ ]card_fin__1289_20.min1.thm1.tptp2017-02-06 16:57 342  
[ ]card_fin__1326_15.min1.thm1.tptp2017-02-06 16:57 328  
[ ]card_fin__1377_20.min1.thm1.tptp2017-02-06 16:57 342  
[ ]card_fin__1382_22.min1.thm1.tptp2017-02-06 16:57 398  
[ ]card_fin__1402_18.min1.thm1.tptp2017-02-06 16:57 334  
[ ]card_fin__1428_20.min1.thm1.tptp2017-02-06 16:57 342  
[ ]card_fin__1443_18.min1.thm1.tptp2017-02-06 16:57 334  
[ ]card_fin__1468_13.min1.thm1.tptp2017-02-06 16:57 326  
[ ]card_fin__1503_20.min1.thm1.tptp2017-02-06 16:57 294  
[ ]card_fin__1528_22.min1.thm1.tptp2017-02-06 16:57 342  
[ ]card_fin__1533_17.min1.thm1.tptp2017-02-06 16:57 342  
[ ]card_fin__1547_22.min1.thm1.tptp2017-02-06 16:57 342  
[ ]card_fin__1552_17.min1.thm1.tptp2017-02-06 16:57 342  
[ ]card_fin__1580_16.min1.thm1.tptp2017-02-06 16:57 348  
[ ]card_fin__1689_16.min1.thm1.tptp2017-02-06 16:57 326  
[ ]card_fin__1833_26.min1.thm1.tptp2017-02-06 16:57 378  
[ ]card_fin__1842_21.min1.thm1.tptp2017-02-06 16:57 378  
[ ]card_fin__2674_21.min1.thm1.tptp2017-02-06 16:57 298  
[ ]card_fin__2781_21.min1.thm1.tptp2017-02-06 16:57 298  
[ ]cardfin2__351_13.min1.thm1.tptp2017-02-06 16:57 262  
[ ]cat_1__156_17.min1.thm1.tptp2017-02-06 16:57 252  
[ ]cat_1__195_25.min1.thm1.tptp2017-02-06 16:57 374  
[ ]cat_4__153_21.min1.thm1.tptp2017-02-06 16:57 304  
[ ]cat_4__163_25.min1.thm1.tptp2017-02-06 16:57 307  
[ ]cat_4__189_21.min1.thm1.tptp2017-02-06 16:57 304  
[ ]cat_4__198_25.min1.thm1.tptp2017-02-06 16:57 307  
[ ]cat_4__312_19.min1.thm1.tptp2017-02-06 16:57 300  
[ ]cat_4__321_23.min1.thm1.tptp2017-02-06 16:57 303  
[ ]cat_4__1223_21.min1.thm1.tptp2017-02-06 16:57 310  
[ ]cat_4__1233_25.min1.thm1.tptp2017-02-06 16:57 313  
[ ]cat_4__1259_21.min1.thm1.tptp2017-02-06 16:57 310  
[ ]cat_4__1268_25.min1.thm1.tptp2017-02-06 16:57 313  
[ ]cat_4__1381_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]cat_4__1390_23.min1.thm1.tptp2017-02-06 16:57 309  
[ ]catalg_1__252_23.min1.thm1.tptp2017-02-06 16:57 310  
[ ]catalg_1__283_23.min1.thm1.tptp2017-02-06 16:57 310  
[ ]catalg_1__320_23.min1.thm1.tptp2017-02-06 16:57 310  
[ ]catalg_1__345_23.min1.thm1.tptp2017-02-06 16:57 310  
[ ]catalg_1__455_73.min1.thm1.tptp2017-02-06 16:57 758  
[ ]catalg_1__484_8.min1.thm1.tptp2017-02-06 16:57 758  
[ ]catalg_1__1913_19.min1.thm1.tptp2017-02-06 16:57 310  
[ ]cfcont_1__1467_11.min1.thm1.tptp2017-02-06 16:57 273  
[ ]cfcont_1__1649_33.min1.thm1.tptp2017-02-06 16:57 466  
[ ]cfcont_1__1681_26.min1.thm1.tptp2017-02-06 16:57 350  
[ ]cfdiff_1__1216_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]cfdiff_1__1384_18.min1.thm1.tptp2017-02-06 16:57 321  
[ ]cfdiff_1__2207_23.min1.thm1.tptp2017-02-06 16:57 294  
[ ]cfdiff_1__2212_15.min1.thm1.tptp2017-02-06 16:57 286  
[ ]cfunct_1__226_31.min1.thm1.tptp2017-02-06 16:57 489  
[ ]cfunct_1__230_33.min1.thm1.tptp2017-02-06 16:57 353  
[ ]cfunct_1__238_32.min1.thm1.tptp2017-02-06 16:57 355  
[ ]cfunct_1__258_22.min1.thm1.tptp2017-02-06 16:57 353  
[ ]cfunct_1__267_26.min1.thm1.tptp2017-02-06 16:57 355  
[ ]cfunct_1__270_37.min1.thm1.tptp2017-02-06 16:57 491  
[ ]cfunct_1__332_27.min1.thm1.tptp2017-02-06 16:57 410  
[ ]cfunct_1__338_28.min1.thm1.tptp2017-02-06 16:57 355  
[ ]cfunct_1__350_23.min1.thm1.tptp2017-02-06 16:57 406  
[ ]cfunct_1__364_26.min1.thm1.tptp2017-02-06 16:57 436  
[ ]cfunct_1__375_19.min1.thm1.tptp2017-02-06 16:57 350  
[ ]cfunct_1__411_29.min1.thm1.tptp2017-02-06 16:57 468  
[ ]cfunct_1__415_23.min1.thm1.tptp2017-02-06 16:57 354  
[ ]cfunct_1__422_23.min1.thm1.tptp2017-02-06 16:57 350  
[ ]cfunct_1__429_25.min1.thm1.tptp2017-02-06 16:57 464  
[ ]cgames_1__287_33.min1.thm1.tptp2017-02-06 16:57 280  
[ ]cgames_1__459_17.min1.thm1.tptp2017-02-06 16:57 318  
[ ]cgames_1__2456_28.min1.thm1.tptp2017-02-06 16:57 310  
[ ]chain_1__251_15.min1.thm1.tptp2017-02-06 16:57 304  
[ ]chain_1__1820_22.min1.thm1.tptp2017-02-06 16:57 382  
[ ]chain_1__1916_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]chain_1__3353_24.min1.thm1.tptp2017-02-06 16:57 460  
[ ]chord__2009_15.min1.thm1.tptp2017-02-06 16:57 268  
[ ]chord__2026_13.min1.thm1.tptp2017-02-06 16:57 260  
[ ]circcmb2__578_68.min1.thm1.tptp2017-02-06 16:57 436  
[ ]circcmb3__759_23.min1.thm1.tptp2017-02-06 16:57 383  
[ ]circcmb3__1110_32.min1.thm1.tptp2017-02-06 16:57 380  
[ ]circcmb3__1125_25.min1.thm1.tptp2017-02-06 16:57 369  
[ ]circcmb3__1279_15.min1.thm1.tptp2017-02-06 16:57 384  
[ ]circcomb__1891_19.min1.thm1.tptp2017-02-06 16:57 294  
[ ]circcomb__1924_23.min1.thm1.tptp2017-02-06 16:57 368  
[ ]circcomb__1967_23.min1.thm1.tptp2017-02-06 16:57 368  
[ ]circtrm1__770_29.min1.thm1.tptp2017-02-06 16:57 322  
[ ]circuit2__1320_30.min1.thm1.tptp2017-02-06 16:57 470  
[ ]classes1__363_16.min1.thm1.tptp2017-02-06 16:57 294  
[ ]classes1__766_21.min1.thm1.tptp2017-02-06 16:57 273  
[ ]classes1__2207_19.min1.thm1.tptp2017-02-06 16:57 408  
[ ]classes1__2239_23.min1.thm1.tptp2017-02-06 16:57 472  
[ ]classes1__2240_19.min1.thm1.tptp2017-02-06 16:57 472  
[ ]classes1__2256_27.min1.thm1.tptp2017-02-06 16:57 470  
[ ]classes1__2281_21.min1.thm1.tptp2017-02-06 16:57 342  
[ ]classes1__2287_20.min1.thm1.tptp2017-02-06 16:57 344  
[ ]classes1__2295_20.min1.thm1.tptp2017-02-06 16:57 334  
[ ]classes1__2300_19.min1.thm1.tptp2017-02-06 16:57 335  
[ ]classes1__2390_15.min1.thm1.tptp2017-02-06 16:57 350  
[ ]classes2__1746_33.min1.thm1.tptp2017-02-06 16:57 320  
[ ]classes2__1753_14.min1.thm1.tptp2017-02-06 16:57 278  
[ ]closure2__371_21.min1.thm1.tptp2017-02-06 16:57 286  
[ ]closure2__377_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]closure2__500_16.min1.thm1.tptp2017-02-06 16:57 304  
[ ]closure2__562_17.min1.thm1.tptp2017-02-06 16:57 328  
[ ]closure3__282_17.min1.thm1.tptp2017-02-06 16:57 398  
[ ]closure3__311_21.min1.thm1.tptp2017-02-06 16:57 289  
[ ]closure3__337_21.min1.thm1.tptp2017-02-06 16:57 289  
[ ]closure3__365_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]closure3__383_21.min1.thm1.tptp2017-02-06 16:57 289  
[ ]cohsp_1__126_25.min1.thm1.tptp2017-02-06 16:57 286  
[ ]cohsp_1__873_23.min1.thm1.tptp2017-02-06 16:57 290  
[ ]cohsp_1__2353_21.min1.thm1.tptp2017-02-06 16:57 280  
[ ]cohsp_1__3179_21.min1.thm1.tptp2017-02-06 16:57 287  
[ ]cohsp_1__3199_11.min1.thm1.tptp2017-02-06 16:57 276  
[ ]collsp__46_17.min1.thm1.tptp2017-02-06 16:57 309  
[ ]collsp__91_23.min1.thm1.tptp2017-02-06 16:57 362  
[ ]collsp__530_18.min1.thm1.tptp2017-02-06 16:57 320  
[ ]combgras__268_17.min1.thm1.tptp2017-02-06 16:57 288  
[ ]combgras__320_36.min1.thm1.tptp2017-02-06 16:57 454  
[ ]combgras__609_21.min1.thm1.tptp2017-02-06 16:57 311  
[ ]combgras__1947_15.min1.thm1.tptp2017-02-06 16:57 278  
[ ]combgras__2487_23.min1.thm1.tptp2017-02-06 16:57 305  
[ ]combgras__2520_23.min1.thm1.tptp2017-02-06 16:57 305  
[ ]combgras__2550_23.min1.thm1.tptp2017-02-06 16:57 305  
[ ]combgras__3963_23.min1.thm1.tptp2017-02-06 16:57 295  
[ ]compl_sp__2216_16.min1.thm1.tptp2017-02-06 16:57 404  
[ ]compl_sp__3215_17.min1.thm1.tptp2017-02-06 16:57 334  
[ ]compos_1__400_13.min1.thm1.tptp2017-02-06 16:57 294  
[ ]compos_1__419_11.min1.thm1.tptp2017-02-06 16:57 270  
[ ]comput_1__231_13.min1.thm1.tptp2017-02-06 16:57 266  
[ ]comput_1__347_13.min1.thm1.tptp2017-02-06 16:57 286  
[ ]comput_1__460_15.min1.thm1.tptp2017-02-06 16:57 286  
[ ]comput_1__812_21.min1.thm1.tptp2017-02-06 16:57 288  
[ ]comput_1__1818_24.min1.thm1.tptp2017-02-06 16:57 324  
[ ]comput_1__2248_32.min1.thm1.tptp2017-02-06 16:57 440  
[ ]comput_1__2353_24.min1.thm1.tptp2017-02-06 16:57 768  
[ ]comput_1__2477_24.min1.thm1.tptp2017-02-06 16:57 768  
[ ]comput_1__2776_17.min1.thm1.tptp2017-02-06 16:57 630  
[ ]comput_1__2882_13.min1.thm1.tptp2017-02-06 16:57 270  
[ ]comput_1__3095_37.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]comput_1__3891_25.min1.thm1.tptp2017-02-06 16:57 366  
[ ]comput_1__4017_24.min1.thm1.tptp2017-02-06 16:57 344  
[ ]comput_1__5003_21.min1.thm1.tptp2017-02-06 16:57 328  
[ ]comput_1__5484_22.min1.thm1.tptp2017-02-06 16:57 322  
[ ]comput_1__5690_24.min1.thm1.tptp2017-02-06 16:57 300  
[ ]comseq_1__181_15.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_1__483_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_1__533_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_1__1709_19.min1.thm1.tptp2017-02-06 16:57 326  
[ ]convex3__900_24.min1.thm1.tptp2017-02-06 16:57 340  
[ ]convex3__929_28.min1.thm1.tptp2017-02-06 16:57 361  
[ ]convex3__939_28.min1.thm1.tptp2017-02-06 16:57 362  
[ ]convex3__985_28.min1.thm1.tptp2017-02-06 16:57 362  
[ ]convex4__459_23.min1.thm1.tptp2017-02-06 16:57 526  
[ ]convfun1__1561_19.min1.thm1.tptp2017-02-06 16:57 302  
[ ]cqc_lang__50_13.min1.thm1.tptp2017-02-06 16:57 246  
[ ]cqc_lang__57_11.min1.thm1.tptp2017-02-06 16:57 248  
[ ]cqc_lang__227_24.min1.thm1.tptp2017-02-06 16:57 322  
[ ]cqc_lang__232_26.min1.thm1.tptp2017-02-06 16:57 321  
[ ]cqc_sim1__102_23.min1.thm1.tptp2017-02-06 16:57 276  
[ ]cqc_sim1__172_19.min1.thm1.tptp2017-02-06 16:57 277  
[ ]cqc_sim1__189_20.min1.thm1.tptp2017-02-06 16:57 268  
[ ]cqc_the1__94_16.min1.thm1.tptp2017-02-06 16:57 272  
[ ]cqc_the3__1148_21.min1.thm1.tptp2017-02-06 16:57 278  
[ ]descip_1__1315_19.min1.thm1.tptp2017-02-06 16:57 468  
[ ]dickson__62_14.min1.thm1.tptp2017-02-06 16:57 270  
[ ]dickson__72_12.min1.thm1.tptp2017-02-06 16:57 266  
[ ]dickson__3074_24.min1.thm1.tptp2017-02-06 16:57 314  
[ ]dickson__3394_18.min1.thm1.tptp2017-02-06 16:57 304  
[ ]dickson__3457_23.min1.thm1.tptp2017-02-06 16:57 304  
[ ]dickson__3581_22.min1.thm1.tptp2017-02-06 16:57 316  
[ ]dickson__3618_20.min1.thm1.tptp2017-02-06 16:57 312  
[ ]dickson__3732_24.min1.thm1.tptp2017-02-06 16:57 324  
[ ]dickson__3758_24.min1.thm1.tptp2017-02-06 16:57 324  
[ ]dickson__3808_22.min1.thm1.tptp2017-02-06 16:57 320  
[ ]dickson__3836_25.min1.thm1.tptp2017-02-06 16:57 308  
[ ]dilworth__325_19.min1.thm1.tptp2017-02-06 16:57 286  
[ ]dilworth__340_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]dilworth__354_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]dilworth__366_27.min1.thm1.tptp2017-02-06 16:57 382  
[ ]dilworth__391_19.min1.thm1.tptp2017-02-06 16:57 286  
[ ]dilworth__406_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]dilworth__421_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]dilworth__434_27.min1.thm1.tptp2017-02-06 16:57 382  
[ ]dilworth__1131_21.min1.thm1.tptp2017-02-06 16:57 347  
[ ]dilworth__1136_21.min1.thm1.tptp2017-02-06 16:57 347  
[ ]dilworth__1141_29.min1.thm1.tptp2017-02-06 16:57 402  
[ ]dilworth__3073_34.min1.thm1.tptp2017-02-06 16:57 386  
[ ]dilworth__3238_28.min1.thm1.tptp2017-02-06 16:57 377  
[ ]dilworth__3249_32.min1.thm1.tptp2017-02-06 16:57 377  
[ ]dilworth__3352_23.min1.thm1.tptp2017-02-06 16:57 306  
[ ]dilworth__3357_24.min1.thm1.tptp2017-02-06 16:57 306  
[ ]enumset1__223_57.min1.thm1.tptp2017-02-06 16:57 534  
[ ]enumset1__518_43.min1.thm1.tptp2017-02-06 16:57 430  
[ ]eqrel_1__650_17.min1.thm1.tptp2017-02-06 16:57 429  
[ ]equation__771_27.min1.thm1.tptp2017-02-06 16:57 482  
[ ]equation__1169_26.min1.thm1.tptp2017-02-06 16:57 436  
[ ]equation__1178_26.min1.thm1.tptp2017-02-06 16:57 388  
[ ]equation__1502_24.min1.thm1.tptp2017-02-06 16:57 372  
[ ]euclid_6__2952_21.min1.thm1.tptp2017-02-06 16:57 286  
[ ]euclid_6__2957_21.min1.thm1.tptp2017-02-06 16:57 286  
[ ]euclid_6__3374_25.min1.thm1.tptp2017-02-06 16:57 390  
[ ]euclid_9__173_18.min1.thm1.tptp2017-02-06 16:57 441  
[ ]euclid_9__271_29.min1.thm1.tptp2017-02-06 16:57 630  
[ ]euler_1__104_13.min1.thm1.tptp2017-02-06 16:57 255  
[ ]exchsort__1881_28.min1.thm1.tptp2017-02-06 16:57 378  
[ ]facirc_1__175_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]facirc_2__56_19.min1.thm1.tptp2017-02-06 16:57 275  
[ ]fcont_3__1042_24.min1.thm1.tptp2017-02-06 16:57 699  
[ ]fcont_3__1203_24.min1.thm1.tptp2017-02-06 16:57 699  
[ ]fcont_3__1404_24.min1.thm1.tptp2017-02-06 16:57 701  
[ ]fcont_3__1565_24.min1.thm1.tptp2017-02-06 16:57 701  
[ ]fdiff_1__703_21.min1.thm1.tptp2017-02-06 16:57 322  
[ ]fdiff_1__798_18.min1.thm1.tptp2017-02-06 16:57 315  
[ ]fdiff_1__1598_23.min1.thm1.tptp2017-02-06 16:57 288  
[ ]fdiff_1__1603_13.min1.thm1.tptp2017-02-06 16:57 280  
[ ]fdiff_2__172_16.min1.thm1.tptp2017-02-06 16:57 306  
[ ]fdiff_2__399_21.min1.thm1.tptp2017-02-06 16:57 274  
[ ]fdiff_2__403_17.min1.thm1.tptp2017-02-06 16:57 268  
[ ]fdiff_2__434_15.min1.thm1.tptp2017-02-06 16:57 260  
[ ]fdiff_2__650_21.min1.thm1.tptp2017-02-06 16:57 322  
[ ]fdiff_2__843_15.min1.thm1.tptp2017-02-06 16:57 280  
[ ]fdiff_2__966_23.min1.thm1.tptp2017-02-06 16:57 338  
[ ]fdiff_2__972_18.min1.thm1.tptp2017-02-06 16:57 330  
[ ]fdiff_2__1381_28.min1.thm1.tptp2017-02-06 16:57 317  
[ ]fdiff_2__1551_17.min1.thm1.tptp2017-02-06 16:57 254  
[ ]fdiff_2__1782_28.min1.thm1.tptp2017-02-06 16:57 440  
[ ]fdiff_2__1786_18.min1.thm1.tptp2017-02-06 16:57 314  
[ ]fdiff_2__1796_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]fdiff_2__1800_26.min1.thm1.tptp2017-02-06 16:57 430  
[ ]fdiff_2__1826_21.min1.thm1.tptp2017-02-06 16:57 314  
[ ]fdiff_2__1867_37.min1.thm1.tptp2017-02-06 16:57 443  
[ ]fdiff_2__1945_20.min1.thm1.tptp2017-02-06 16:57 314  
[ ]fdiff_2__1963_35.min1.thm1.tptp2017-02-06 16:57 441  
[ ]fdiff_2__3144_25.min1.thm1.tptp2017-02-06 16:57 420  
[ ]fdiff_2__3148_27.min1.thm1.tptp2017-02-06 16:57 412  
[ ]fdiff_2__3377_25.min1.thm1.tptp2017-02-06 16:57 544  
[ ]fdiff_2__3381_28.min1.thm1.tptp2017-02-06 16:57 536  
[ ]fdiff_2__3616_25.min1.thm1.tptp2017-02-06 16:57 546  
[ ]fdiff_2__3620_28.min1.thm1.tptp2017-02-06 16:57 538  
[ ]fdiff_2__3864_25.min1.thm1.tptp2017-02-06 16:57 574  
[ ]fdiff_2__3868_28.min1.thm1.tptp2017-02-06 16:57 566  
[ ]fdiff_3__87_21.min1.thm1.tptp2017-02-06 16:57 274  
[ ]fdiff_3__91_18.min1.thm1.tptp2017-02-06 16:57 268  
[ ]fdiff_3__159_21.min1.thm1.tptp2017-02-06 16:57 274  
[ ]fdiff_3__163_18.min1.thm1.tptp2017-02-06 16:57 268  
[ ]fdiff_3__576_23.min1.thm1.tptp2017-02-06 16:57 282  
[ ]fdiff_3__581_15.min1.thm1.tptp2017-02-06 16:57 274  
[ ]fdiff_3__859_23.min1.thm1.tptp2017-02-06 16:57 282  
[ ]fdiff_3__864_15.min1.thm1.tptp2017-02-06 16:57 274  
[ ]fdiff_3__1112_15.min1.thm1.tptp2017-02-06 16:57 288  
[ ]fdiff_3__1163_15.min1.thm1.tptp2017-02-06 16:57 288  
[ ]fdiff_3__1726_19.min1.thm1.tptp2017-02-06 16:57 326  
[ ]fdiff_3__2037_18.min1.thm1.tptp2017-02-06 16:57 326  
[ ]fdiff_3__2747_19.min1.thm1.tptp2017-02-06 16:57 326  
[ ]fdiff_3__3061_18.min1.thm1.tptp2017-02-06 16:57 326  
[ ]fdiff_3__3331_19.min1.thm1.tptp2017-02-06 16:57 304  
[ ]fdiff_3__3378_23.min1.thm1.tptp2017-02-06 16:57 328  
[ ]finseq_1__104_17.min1.thm1.tptp2017-02-06 16:57 254  
[ ]finseq_1__230_16.min1.thm1.tptp2017-02-06 16:57 310  
[ ]finseq_1__353_14.min1.thm1.tptp2017-02-06 16:57 290  
[ ]finseq_1__361_16.min1.thm1.tptp2017-02-06 16:57 322  
[ ]finseq_1__1208_16.min1.thm1.tptp2017-02-06 16:57 278  
[ ]finseq_1__1302_17.min1.thm1.tptp2017-02-06 16:57 306  
[ ]finseq_1__1375_15.min1.thm1.tptp2017-02-06 16:57 258  
[ ]finseq_1__1385_18.min1.thm1.tptp2017-02-06 16:57 348  
[ ]finseq_1__1444_13.min1.thm1.tptp2017-02-06 16:57 258  
[ ]finseq_1__1497_16.min1.thm1.tptp2017-02-06 16:57 372  
[ ]finseq_1__1513_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]finseq_1__1754_30.min1.thm1.tptp2017-02-06 16:57 307  
[ ]finseq_1__1775_30.min1.thm1.tptp2017-02-06 16:57 307  
[ ]finseq_1__1847_28.min1.thm1.tptp2017-02-06 16:57 303  
[ ]finseq_1__1974_21.min1.thm1.tptp2017-02-06 16:57 274  
[ ]finseq_1__2152_19.min1.thm1.tptp2017-02-06 16:57 357  
[ ]finseq_1__2351_14.min1.thm1.tptp2017-02-06 16:57 282  
[ ]finseq_1__3435_14.min1.thm1.tptp2017-02-06 16:57 267  
[ ]finseq_2__2376_28.min1.thm1.tptp2017-02-06 16:57 302  
[ ]finseq_2__2440_24.min1.thm1.tptp2017-02-06 16:57 296  
[ ]finseq_3__184_16.min1.thm1.tptp2017-02-06 16:57 302  
[ ]finseq_3__986_38.min1.thm1.tptp2017-02-06 16:57 489  
[ ]finseq_3__1016_22.min1.thm1.tptp2017-02-06 16:57 330  
[ ]finseq_3__1124_20.min1.thm1.tptp2017-02-06 16:57 322  
[ ]finseq_3__1133_32.min1.thm1.tptp2017-02-06 16:57 443  
[ ]finseq_3__1242_12.min1.thm1.tptp2017-02-06 16:57 258  
[ ]finseq_3__1856_26.min1.thm1.tptp2017-02-06 16:57 356  
[ ]finseq_3__1914_24.min1.thm1.tptp2017-02-06 16:57 404  
[ ]finseq_3__1938_22.min1.thm1.tptp2017-02-06 16:57 344  
[ ]finseq_3__2032_26.min1.thm1.tptp2017-02-06 16:57 368  
[ ]finseq_3__2365_29.min1.thm1.tptp2017-02-06 16:57 329  
[ ]finseq_3__2756_13.min1.thm1.tptp2017-02-06 16:57 250  
[ ]finseq_3__2881_21.min1.thm1.tptp2017-02-06 16:57 318  
[ ]finseq_3__2885_19.min1.thm1.tptp2017-02-06 16:57 420  
[ ]finseq_3__3103_56.min1.thm1.tptp2017-02-06 16:57 376  
[ ]finseq_3__3111_48.min1.thm1.tptp2017-02-06 16:57 369  
[ ]finseq_3__3227_24.min1.thm1.tptp2017-02-06 16:57 331  
[ ]finseq_3__3277_25.min1.thm1.tptp2017-02-06 16:57 323  
[ ]finseq_3__3318_20.min1.thm1.tptp2017-02-06 16:57 344  
[ ]finseq_3__3344_35.min1.thm1.tptp2017-02-06 16:57 361  
[ ]finseq_3__3374_24.min1.thm1.tptp2017-02-06 16:57 356  
[ ]finseq_3__3835_25.min1.thm1.tptp2017-02-06 16:57 326  
[ ]finseq_3__4065_17.min1.thm1.tptp2017-02-06 16:57 299  
[ ]finseq_3__4240_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]finseq_3__4249_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]finseq_3__4399_17.min1.thm1.tptp2017-02-06 16:57 299  
[ ]finseq_4__56_24.min1.thm1.tptp2017-02-06 16:57 372  
[ ]finseq_4__112_18.min1.thm1.tptp2017-02-06 16:57 384  
[ ]finseq_4__163_15.min1.thm1.tptp2017-02-06 16:57 264  
[ ]finseq_4__182_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]finseq_4__205_18.min1.thm1.tptp2017-02-06 16:57 326  
[ ]finseq_4__216_17.min1.thm1.tptp2017-02-06 16:57 328  
[ ]finseq_4__234_15.min1.thm1.tptp2017-02-06 16:57 280  
[ ]finseq_4__235_19.min1.thm1.tptp2017-02-06 16:57 322  
[ ]finseq_4__243_16.min1.thm1.tptp2017-02-06 16:57 326  
[ ]finseq_4__246_19.min1.thm1.tptp2017-02-06 16:57 272  
[ ]finseq_4__302_15.min1.thm1.tptp2017-02-06 16:57 270  
[ ]finseq_4__356_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]finseq_4__488_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]finseq_4__528_22.min1.thm1.tptp2017-02-06 16:57 384  
[ ]finseq_4__613_17.min1.thm1.tptp2017-02-06 16:57 334  
[ ]finseq_4__631_20.min1.thm1.tptp2017-02-06 16:57 336  
[ ]finseq_4__641_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]finseq_4__644_17.min1.thm1.tptp2017-02-06 16:57 329  
[ ]finseq_4__696_26.min1.thm1.tptp2017-02-06 16:57 333  
[ ]finseq_4__715_16.min1.thm1.tptp2017-02-06 16:57 342  
[ ]finseq_4__722_16.min1.thm1.tptp2017-02-06 16:57 336  
[ ]finseq_4__725_23.min1.thm1.tptp2017-02-06 16:57 388  
[ ]finseq_4__874_54.min1.thm1.tptp2017-02-06 16:57 401  
[ ]finseq_4__1111_55.min1.thm1.tptp2017-02-06 16:57 401  
[ ]finseq_4__1202_16.min1.thm1.tptp2017-02-06 16:57 282  
[ ]finseq_4__1565_18.min1.thm1.tptp2017-02-06 16:57 282  
[ ]finseq_4__1579_18.min1.thm1.tptp2017-02-06 16:57 282  
[ ]finseq_4__1591_19.min1.thm1.tptp2017-02-06 16:57 282  
[ ]finseq_4__1750_30.min1.thm1.tptp2017-02-06 16:57 484  
[ ]finseq_4__1757_25.min1.thm1.tptp2017-02-06 16:57 395  
[ ]finseq_4__2289_13.min1.thm1.tptp2017-02-06 16:57 258  
[ ]finseq_4__2378_13.min1.thm1.tptp2017-02-06 16:57 258  
[ ]finseq_5__76_17.min1.thm1.tptp2017-02-06 16:57 340  
[ ]finseq_5__80_17.min1.thm1.tptp2017-02-06 16:57 318  
[ ]finseq_5__766_20.min1.thm1.tptp2017-02-06 16:57 416  
[ ]finseq_6__1060_15.min1.thm1.tptp2017-02-06 16:57 298  
[ ]finseq_6__1339_20.min1.thm1.tptp2017-02-06 16:57 358  
[ ]finseq_6__1586_28.min1.thm1.tptp2017-02-06 16:57 281  
[ ]finseq_6__1641_19.min1.thm1.tptp2017-02-06 16:57 340  
[ ]finseq_6__2220_20.min1.thm1.tptp2017-02-06 16:57 356  
[ ]finseq_6__2439_28.min1.thm1.tptp2017-02-06 16:57 308  
[ ]finseq_6__2454_22.min1.thm1.tptp2017-02-06 16:57 361  
[ ]finseq_6__2512_27.min1.thm1.tptp2017-02-06 16:57 372  
[ ]finset_1__64_14.min1.thm1.tptp2017-02-06 16:57 276  
[ ]finset_1__72_19.min1.thm1.tptp2017-02-06 16:57 272  
[ ]finset_1__417_18.min1.thm1.tptp2017-02-06 16:57 369  
[ ]finset_1__698_17.min1.thm1.tptp2017-02-06 16:57 322  
[ ]finset_1__1579_16.min1.thm1.tptp2017-02-06 16:57 312  
[ ]finset_1__1634_21.min1.thm1.tptp2017-02-06 16:57 300  
[ ]finsop_1__757_24.min1.thm1.tptp2017-02-06 16:57 343  
[ ]finsop_1__796_23.min1.thm1.tptp2017-02-06 16:57 306  
[ ]finsop_1__836_30.min1.thm1.tptp2017-02-06 16:57 347  
[ ]finsop_1__853_30.min1.thm1.tptp2017-02-06 16:57 347  
[ ]finsub_1__68_15.min1.thm1.tptp2017-02-06 16:57 282  
[ ]finsub_1__77_15.min1.thm1.tptp2017-02-06 16:57 282  
[ ]finsub_1__86_15.min1.thm1.tptp2017-02-06 16:57 282  
[ ]fintopo5__1194_19.min1.thm1.tptp2017-02-06 16:57 330  
[ ]fintopo5__1331_17.min1.thm1.tptp2017-02-06 16:57 306  
[ ]fintopo5__1345_17.min1.thm1.tptp2017-02-06 16:57 306  
[ ]flang_2__238_18.min1.thm1.tptp2017-02-06 16:57 348  
[ ]flang_2__239_18.min1.thm1.tptp2017-02-06 16:57 348  
[ ]flang_2__1135_23.min1.thm1.tptp2017-02-06 16:57 382  
[ ]fomodel0__582_16.min1.thm1.tptp2017-02-06 16:57 289  
[ ]fomodel0__2002_15.min1.thm1.tptp2017-02-06 16:57 394  
[ ]fomodel0__3161_12.min1.thm1.tptp2017-02-06 16:57 403  
[ ]fomodel0__3175_37.min1.thm1.tptp2017-02-06 16:57 286  
[ ]fomodel2__3645_37.min1.thm1.tptp2017-02-06 16:57 286  
[ ]fomodel3__3935_14.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]fomodel4__680_49.min1.thm1.tptp2017-02-06 16:57 286  
[ ]frechet__920_18.min1.thm1.tptp2017-02-06 16:57 454  
[ ]frechet__942_19.min1.thm1.tptp2017-02-06 16:57 276  
[ ]frechet__1644_24.min1.thm1.tptp2017-02-06 16:57 302  
[ ]frechet__1700_26.min1.thm1.tptp2017-02-06 16:57 284  
[ ]frechet__1797_24.min1.thm1.tptp2017-02-06 16:57 276  
[ ]frechet__1991_24.min1.thm1.tptp2017-02-06 16:57 267  
[ ]frechet__2010_14.min1.thm1.tptp2017-02-06 16:57 522  
[ ]frechet__2061_26.min1.thm1.tptp2017-02-06 16:57 348  
[ ]frechet__2264_26.min1.thm1.tptp2017-02-06 16:57 352  
[ ]freealg__267_23.min1.thm1.tptp2017-02-06 16:57 433  
[ ]fsm_1__1831_12.min1.thm1.tptp2017-02-06 16:57 286  
[ ]fsm_1__4173_17.min1.thm1.tptp2017-02-06 16:57 294  
[ ]fsm_1__4242_16.min1.thm1.tptp2017-02-06 16:57 276  
[ ]funcop_1__291_15.min1.thm1.tptp2017-02-06 16:57 288  
[ ]funcop_1__365_23.min1.thm1.tptp2017-02-06 16:57 306  
[ ]funcop_1__371_25.min1.thm1.tptp2017-02-06 16:57 302  
[ ]funct_1__248_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]funct_1__249_17.min1.thm1.tptp2017-02-06 16:57 292  
[ ]funct_1__332_17.min1.thm1.tptp2017-02-06 16:57 317  
[ ]funct_1__1627_14.min1.thm1.tptp2017-02-06 16:57 280  
[ ]funct_1__1632_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]funct_1__1928_10.min1.thm1.tptp2017-02-06 16:57 264  
[ ]funct_1__1963_14.min1.thm1.tptp2017-02-06 16:57 278  
[ ]funct_1__1983_16.min1.thm1.tptp2017-02-06 16:57 330  
[ ]funct_1__1990_17.min1.thm1.tptp2017-02-06 16:57 365  
[ ]funct_1__2268_20.min1.thm1.tptp2017-02-06 16:57 350  
[ ]funct_1__2370_19.min1.thm1.tptp2017-02-06 16:57 278  
[ ]funct_1__2601_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]funct_1__2614_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]funct_1__2664_23.min1.thm1.tptp2017-02-06 16:57 382  
[ ]funct_1__3006_18.min1.thm1.tptp2017-02-06 16:57 378  
[ ]funct_2__848_17.min1.thm1.tptp2017-02-06 16:57 406  
[ ]funct_2__1463_17.min1.thm1.tptp2017-02-06 16:57 397  
[ ]funct_2__2311_24.min1.thm1.tptp2017-02-06 16:57 361  
[ ]funct_2__2621_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]funct_3__1006_21.min1.thm1.tptp2017-02-06 16:57 312  
[ ]funct_4__1999_17.min1.thm1.tptp2017-02-06 16:57 272  
[ ]funct_5__120_19.min1.thm1.tptp2017-02-06 16:57 272  
[ ]funct_5__126_17.min1.thm1.tptp2017-02-06 16:57 272  
[ ]funct_5__138_19.min1.thm1.tptp2017-02-06 16:57 272  
[ ]funct_5__144_17.min1.thm1.tptp2017-02-06 16:57 272  
[ ]funct_5__1320_19.min1.thm1.tptp2017-02-06 16:57 266  
[ ]funct_5__1326_13.min1.thm1.tptp2017-02-06 16:57 258  
[ ]funct_5__1859_22.min1.thm1.tptp2017-02-06 16:57 357  
[ ]funct_5__1863_22.min1.thm1.tptp2017-02-06 16:57 357  
[ ]funct_5__1875_26.min1.thm1.tptp2017-02-06 16:57 354  
[ ]funct_5__1915_18.min1.thm1.tptp2017-02-06 16:57 346  
[ ]funct_5__1923_24.min1.thm1.tptp2017-02-06 16:57 338  
[ ]funct_6__1265_25.min1.thm1.tptp2017-02-06 16:57 312  
[ ]funct_6__1462_13.min1.thm1.tptp2017-02-06 16:57 266  
[ ]funct_6__2002_36.min1.thm1.tptp2017-02-06 16:57 486  
[ ]funct_7__368_22.min1.thm1.tptp2017-02-06 16:57 267  
[ ]funct_7__423_14.min1.thm1.tptp2017-02-06 16:57 238  
[ ]funct_7__449_13.min1.thm1.tptp2017-02-06 16:57 258  
[ ]funct_8__2722_28.min1.thm1.tptp2017-02-06 16:57 315  
[ ]funct_8__2780_28.min1.thm1.tptp2017-02-06 16:57 319  
[ ]funct_9__759_21.min1.thm1.tptp2017-02-06 16:57 315  
[ ]funct_9__761_38.min1.thm1.tptp2017-02-06 16:57 439  
[ ]funct_9__790_21.min1.thm1.tptp2017-02-06 16:57 315  
[ ]funct_9__792_38.min1.thm1.tptp2017-02-06 16:57 439  
[ ]funct_9__842_34.min1.thm1.tptp2017-02-06 16:57 734  
[ ]funct_9__844_47.min1.thm1.tptp2017-02-06 16:57 625  
[ ]funct_9__913_34.min1.thm1.tptp2017-02-06 16:57 734  
[ ]funct_9__915_47.min1.thm1.tptp2017-02-06 16:57 625  
[ ]funct_9__971_15.min1.thm1.tptp2017-02-06 16:57 315  
[ ]funct_9__1010_15.min1.thm1.tptp2017-02-06 16:57 315  
[ ]funct_9__1071_48.min1.thm1.tptp2017-02-06 16:57 834  
[ ]funct_9__1154_48.min1.thm1.tptp2017-02-06 16:57 834  
[ ]fvaluat1__1434_19.min1.thm1.tptp2017-02-06 16:57 540  
[ ]fvaluat1__2384_19.min1.thm1.tptp2017-02-06 16:57 550  
[ ]gcd_1__818_25.min1.thm1.tptp2017-02-06 16:57 312  
[ ]gcd_1__894_27.min1.thm1.tptp2017-02-06 16:57 375  
[ ]gcd_1__938_29.min1.thm1.tptp2017-02-06 16:57 376  
[ ]gcd_1__946_29.min1.thm1.tptp2017-02-06 16:57 376  
[ ]glib_000__417_24.min1.thm1.tptp2017-02-06 16:57 368  
[ ]glib_000__429_26.min1.thm1.tptp2017-02-06 16:57 364  
[ ]glib_000__1322_35.min1.thm1.tptp2017-02-06 16:57 449  
[ ]glib_000__1325_29.min1.thm1.tptp2017-02-06 16:57 449  
[ ]glib_000__1534_18.min1.thm1.tptp2017-02-06 16:57 352  
[ ]glib_000__1538_19.min1.thm1.tptp2017-02-06 16:57 321  
[ ]glib_000__1572_18.min1.thm1.tptp2017-02-06 16:57 352  
[ ]glib_000__1576_19.min1.thm1.tptp2017-02-06 16:57 321  
[ ]glib_000__2597_64.min1.thm1.tptp2017-02-06 16:57 344  
[ ]glib_000__2868_65.min1.thm1.tptp2017-02-06 16:57 470  
[ ]glib_000__2873_61.min1.thm1.tptp2017-02-06 16:57 470  
[ ]glib_000__2881_66.min1.thm1.tptp2017-02-06 16:57 470  
[ ]glib_000__2887_60.min1.thm1.tptp2017-02-06 16:57 470  
[ ]glib_001__6587_30.min1.thm1.tptp2017-02-06 16:57 312  
[ ]glib_001__6606_21.min1.thm1.tptp2017-02-06 16:57 296  
[ ]glib_001__6952_24.min1.thm1.tptp2017-02-06 16:57 466  
[ ]glib_002__973_41.min1.thm1.tptp2017-02-06 16:57 316  
[ ]glib_002__977_30.min1.thm1.tptp2017-02-06 16:57 312  
[ ]glib_002__984_47.min1.thm1.tptp2017-02-06 16:57 322  
[ ]glib_002__1185_26.min1.thm1.tptp2017-02-06 16:57 296  
[ ]glib_002__2332_18.min1.thm1.tptp2017-02-06 16:57 352  
[ ]glib_002__2336_19.min1.thm1.tptp2017-02-06 16:57 321  
[ ]glib_002__3137_26.min1.thm1.tptp2017-02-06 16:57 348  
[ ]glib_003__224_20.min1.thm1.tptp2017-02-06 16:57 402  
[ ]glib_003__285_26.min1.thm1.tptp2017-02-06 16:57 303  
[ ]glib_003__323_16.min1.thm1.tptp2017-02-06 16:57 292  
[ ]glib_003__365_21.min1.thm1.tptp2017-02-06 16:57 292  
[ ]glib_003__3133_18.min1.thm1.tptp2017-02-06 16:57 356  
[ ]glib_003__3137_19.min1.thm1.tptp2017-02-06 16:57 326  
[ ]glib_003__3779_23.min1.thm1.tptp2017-02-06 16:57 285  
[ ]glib_003__3902_23.min1.thm1.tptp2017-02-06 16:57 285  
[ ]glib_003__3973_18.min1.thm1.tptp2017-02-06 16:57 276  
[ ]glib_003__4050_18.min1.thm1.tptp2017-02-06 16:57 276  
[ ]glib_004__64_17.min1.thm1.tptp2017-02-06 16:57 264  
[ ]glib_004__99_20.min1.thm1.tptp2017-02-06 16:57 272  
[ ]glib_004__283_17.min1.thm1.tptp2017-02-06 16:57 320  
[ ]glib_004__889_16.min1.thm1.tptp2017-02-06 16:57 290  
[ ]glib_004__1806_22.min1.thm1.tptp2017-02-06 16:57 550  
[ ]glib_004__1807_53.min1.thm1.tptp2017-02-06 16:57 634  
[ ]glib_004__1975_27.min1.thm1.tptp2017-02-06 16:57 915  
[ ]glib_004__1993_40.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]glib_004__2232_27.min1.thm1.tptp2017-02-06 16:57 646  
[ ]glib_004__2264_25.min1.thm1.tptp2017-02-06 16:57 638  
[ ]glib_004__2562_21.min1.thm1.tptp2017-02-06 16:57 390  
[ ]glib_004__2581_21.min1.thm1.tptp2017-02-06 16:57 390  
[ ]glib_004__2834_26.min1.thm1.tptp2017-02-06 16:57 558  
[ ]glib_004__2835_54.min1.thm1.tptp2017-02-06 16:57 642  
[ ]glib_004__2874_26.min1.thm1.tptp2017-02-06 16:57 558  
[ ]glib_004__2875_54.min1.thm1.tptp2017-02-06 16:57 642  
[ ]glib_004__3147_29.min1.thm1.tptp2017-02-06 16:57 618  
[ ]glib_004__3177_28.min1.thm1.tptp2017-02-06 16:57 618  
[ ]glib_004__4089_15.min1.thm1.tptp2017-02-06 16:57 502  
[ ]glib_004__4347_26.min1.thm1.tptp2017-02-06 16:57 522  
[ ]glib_004__4369_22.min1.thm1.tptp2017-02-06 16:57 304  
[ ]glib_004__4404_15.min1.thm1.tptp2017-02-06 16:57 502  
[ ]glib_005__435_26.min1.thm1.tptp2017-02-06 16:57 512  
[ ]glib_005__442_23.min1.thm1.tptp2017-02-06 16:57 428  
[ ]glib_005__459_23.min1.thm1.tptp2017-02-06 16:57 428  
[ ]glib_005__476_26.min1.thm1.tptp2017-02-06 16:57 512  
[ ]glib_005__901_42.min1.thm1.tptp2017-02-06 16:57 764  
[ ]glib_005__1030_42.min1.thm1.tptp2017-02-06 16:57 764  
[ ]glib_005__1232_42.min1.thm1.tptp2017-02-06 16:57 764  
[ ]glib_005__1400_42.min1.thm1.tptp2017-02-06 16:57 764  
[ ]glib_005__1640_25.min1.thm1.tptp2017-02-06 16:57 756  
[ ]glib_005__1762_25.min1.thm1.tptp2017-02-06 16:57 756  
[ ]glib_005__2582_18.min1.thm1.tptp2017-02-06 16:57 541  
[ ]glib_005__2583_29.min1.thm1.tptp2017-02-06 16:57 541  
[ ]glib_005__4430_44.min1.thm1.tptp2017-02-06 16:57 454  
[ ]glib_005__4451_37.min1.thm1.tptp2017-02-06 16:57 386  
[ ]glib_005__4456_29.min1.thm1.tptp2017-02-06 16:57 402  
[ ]glib_005__4501_28.min1.thm1.tptp2017-02-06 16:57 405  
[ ]glib_005__4523_37.min1.thm1.tptp2017-02-06 16:57 386  
[ ]glib_005__4578_44.min1.thm1.tptp2017-02-06 16:57 454  
[ ]glib_005__4599_37.min1.thm1.tptp2017-02-06 16:57 386  
[ ]glib_005__4604_29.min1.thm1.tptp2017-02-06 16:57 402  
[ ]glib_005__4648_28.min1.thm1.tptp2017-02-06 16:57 405  
[ ]glib_005__4670_37.min1.thm1.tptp2017-02-06 16:57 386  
[ ]goboard1__267_14.min1.thm1.tptp2017-02-06 16:57 270  
[ ]goboard1__285_14.min1.thm1.tptp2017-02-06 16:57 270  
[ ]goboard1__304_14.min1.thm1.tptp2017-02-06 16:57 270  
[ ]goboard1__321_13.min1.thm1.tptp2017-02-06 16:57 264  
[ ]goboard3__970_35.min1.thm1.tptp2017-02-06 16:57 672  
[ ]goboard3__2039_35.min1.thm1.tptp2017-02-06 16:57 672  
[ ]goboard3__3136_35.min1.thm1.tptp2017-02-06 16:57 672  
[ ]goboard3__4209_35.min1.thm1.tptp2017-02-06 16:57 672  
[ ]goboard6__1576_47.min1.thm1.tptp2017-02-06 16:57 822  
[ ]goboard6__1679_51.min1.thm1.tptp2017-02-06 16:57 886  
[ ]goboard6__1786_51.min1.thm1.tptp2017-02-06 16:57 886  
[ ]goboard6__1891_47.min1.thm1.tptp2017-02-06 16:57 822  
[ ]goboard6__1995_47.min1.thm1.tptp2017-02-06 16:57 782  
[ ]goboard6__2085_55.min1.thm1.tptp2017-02-06 16:57 874  
[ ]goboard6__2172_47.min1.thm1.tptp2017-02-06 16:57 782  
[ ]goboard6__2262_59.min1.thm1.tptp2017-02-06 16:57 874  
[ ]goboard6__2348_41.min1.thm1.tptp2017-02-06 16:57 534  
[ ]goboard6__2431_43.min1.thm1.tptp2017-02-06 16:57 566  
[ ]goboard6__2516_45.min1.thm1.tptp2017-02-06 16:57 580  
[ ]goboard6__2601_47.min1.thm1.tptp2017-02-06 16:57 612  
[ ]goboard6__2683_41.min1.thm1.tptp2017-02-06 16:57 534  
[ ]goboard6__2766_43.min1.thm1.tptp2017-02-06 16:57 566  
[ ]goboard6__2852_47.min1.thm1.tptp2017-02-06 16:57 580  
[ ]goboard6__2937_49.min1.thm1.tptp2017-02-06 16:57 612  
[ ]goboard6__3017_41.min1.thm1.tptp2017-02-06 16:57 514  
[ ]goboard6__3069_45.min1.thm1.tptp2017-02-06 16:57 560  
[ ]goboard6__3131_47.min1.thm1.tptp2017-02-06 16:57 560  
[ ]goboard6__3192_51.min1.thm1.tptp2017-02-06 16:57 606  
[ ]goboard6__3254_41.min1.thm1.tptp2017-02-06 16:57 514  
[ ]goboard6__3306_45.min1.thm1.tptp2017-02-06 16:57 560  
[ ]goboard6__3367_47.min1.thm1.tptp2017-02-06 16:57 560  
[ ]goboard6__3426_51.min1.thm1.tptp2017-02-06 16:57 606  
[ ]goedelcp__1360_22.min1.thm1.tptp2017-02-06 16:57 566  
[ ]graph_1__416_35.min1.thm1.tptp2017-02-06 16:57 390  
[ ]graph_1__419_32.min1.thm1.tptp2017-02-06 16:57 392  
[ ]graph_2__251_22.min1.thm1.tptp2017-02-06 16:57 374  
[ ]graph_2__277_19.min1.thm1.tptp2017-02-06 16:57 352  
[ ]graph_2__2069_17.min1.thm1.tptp2017-02-06 16:57 319  
[ ]graph_3__1711_21.min1.thm1.tptp2017-02-06 16:57 305  
[ ]graph_3__1752_17.min1.thm1.tptp2017-02-06 16:57 294  
[ ]graph_3__1761_17.min1.thm1.tptp2017-02-06 16:57 294  
[ ]graph_3__1954_13.min1.thm1.tptp2017-02-06 16:57 293  
[ ]graph_3__2017_13.min1.thm1.tptp2017-02-06 16:57 293  
[ ]graph_3__2362_16.min1.thm1.tptp2017-02-06 16:57 270  
[ ]graph_3__2368_16.min1.thm1.tptp2017-02-06 16:57 282  
[ ]graph_3__2572_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]graph_3__2637_18.min1.thm1.tptp2017-02-06 16:57 296  
[ ]graph_3__4004_12.min1.thm1.tptp2017-02-06 16:57 298  
[ ]graph_5__152_25.min1.thm1.tptp2017-02-06 16:57 270  
[ ]graph_5__1575_27.min1.thm1.tptp2017-02-06 16:57 422  
[ ]graph_5__1600_22.min1.thm1.tptp2017-02-06 16:57 394  
[ ]graph_5__1704_19.min1.thm1.tptp2017-02-06 16:57 267  
[ ]graphsp__493_23.min1.thm1.tptp2017-02-06 16:57 281  
[ ]graphsp__3064_22.min1.thm1.tptp2017-02-06 16:57 271  
[ ]grcat_1__766_64.min1.thm1.tptp2017-02-06 16:57 377  
[ ]grfunc_1__128_14.min1.thm1.tptp2017-02-06 16:57 276  
[ ]grfunc_1__137_17.min1.thm1.tptp2017-02-06 16:57 292  
[ ]groeb_1__59_19.min1.thm1.tptp2017-02-06 16:57 282  
[ ]groeb_1__398_72.min1.thm1.tptp2017-02-06 16:57 564  
[ ]groeb_1__2310_23.min1.thm1.tptp2017-02-06 16:57 279  
[ ]groeb_1__2323_20.min1.thm1.tptp2017-02-06 16:57 272  
[ ]groeb_1__2440_24.min1.thm1.tptp2017-02-06 16:57 292  
[ ]groeb_1__2459_32.min1.thm1.tptp2017-02-06 16:57 314  
[ ]groeb_1__3099_23.min1.thm1.tptp2017-02-06 16:57 367  
[ ]groeb_1__3115_23.min1.thm1.tptp2017-02-06 16:57 366  
[ ]groeb_1__3166_23.min1.thm1.tptp2017-02-06 16:57 517  
[ ]groeb_1__3191_23.min1.thm1.tptp2017-02-06 16:57 373  
[ ]groeb_1__3308_33.min1.thm1.tptp2017-02-06 16:57 366  
[ ]groeb_2__735_26.min1.thm1.tptp2017-02-06 16:57 380  
[ ]groeb_3__201_30.min1.thm1.tptp2017-02-06 16:57 450  
[ ]groeb_3__753_23.min1.thm1.tptp2017-02-06 16:57 320  
[ ]groeb_3__815_23.min1.thm1.tptp2017-02-06 16:57 332  
[ ]groeb_3__1570_19.min1.thm1.tptp2017-02-06 16:57 522  
[ ]groeb_3__2038_18.min1.thm1.tptp2017-02-06 16:57 676  
[ ]groeb_3__2074_23.min1.thm1.tptp2017-02-06 16:57 545  
[ ]groeb_3__2115_32.min1.thm1.tptp2017-02-06 16:57 468  
[ ]groeb_3__2173_32.min1.thm1.tptp2017-02-06 16:57 468  
[ ]groeb_3__2672_68.min1.thm1.tptp2017-02-06 16:57 559  
[ ]groeb_3__2863_71.min1.thm1.tptp2017-02-06 16:57 536  
[ ]groeb_3__3046_29.min1.thm1.tptp2017-02-06 16:57 502  
[ ]groeb_3__3075_24.min1.thm1.tptp2017-02-06 16:57 691  
[ ]groeb_3__3117_27.min1.thm1.tptp2017-02-06 16:57 415  
[ ]groeb_3__3199_58.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]groeb_3__3231_32.min1.thm1.tptp2017-02-06 16:57 670  
[ ]groeb_3__3245_33.min1.thm1.tptp2017-02-06 16:57 850  
[ ]group_2__2781_40.min1.thm1.tptp2017-02-06 16:57 354  
[ ]group_2__2800_41.min1.thm1.tptp2017-02-06 16:57 354  
[ ]group_3__2221_21.min1.thm1.tptp2017-02-06 16:57 286  
[ ]group_6__336_36.min1.thm1.tptp2017-02-06 16:57 357  
[ ]group_6__1796_14.min1.thm1.tptp2017-02-06 16:57 296  
[ ]group_7__1967_14.min1.thm1.tptp2017-02-06 16:57 270  
[ ]group_7__2465_12.min1.thm1.tptp2017-02-06 16:57 254  
[ ]group_7__2566_12.min1.thm1.tptp2017-02-06 16:57 254  
[ ]group_9__460_15.min1.thm1.tptp2017-02-06 16:57 293  
[ ]group_9__737_18.min1.thm1.tptp2017-02-06 16:57 320  
[ ]group_9__5067_26.min1.thm1.tptp2017-02-06 16:57 296  
[ ]group_9__5750_28.min1.thm1.tptp2017-02-06 16:57 398  
[ ]group_9__5754_21.min1.thm1.tptp2017-02-06 16:57 454  
[ ]group_9__7419_21.min1.thm1.tptp2017-02-06 16:57 287  
[ ]group_9__7986_22.min1.thm1.tptp2017-02-06 16:57 275  
[ ]group_9__8050_14.min1.thm1.tptp2017-02-06 16:57 302  
[ ]group_9__8052_21.min1.thm1.tptp2017-02-06 16:57 334  
[ ]group_9__8275_21.min1.thm1.tptp2017-02-06 16:57 338  
[ ]group_9__9067_22.min1.thm1.tptp2017-02-06 16:57 305  
[ ]group_9__9070_25.min1.thm1.tptp2017-02-06 16:57 361  
[ ]group_9__9083_24.min1.thm1.tptp2017-02-06 16:57 361  
[ ]group_10__456_24.min1.thm1.tptp2017-02-06 16:57 424  
[ ]group_10__468_24.min1.thm1.tptp2017-02-06 16:57 424  
[ ]group_10__527_29.min1.thm1.tptp2017-02-06 16:57 484  
[ ]group_10__536_16.min1.thm1.tptp2017-02-06 16:57 294  
[ ]hallmar1__227_19.min1.thm1.tptp2017-02-06 16:57 420  
[ ]hallmar1__323_26.min1.thm1.tptp2017-02-06 16:57 289  
[ ]hallmar1__429_19.min1.thm1.tptp2017-02-06 16:57 275  
[ ]hallmar1__440_19.min1.thm1.tptp2017-02-06 16:57 276  
[ ]hallmar1__553_18.min1.thm1.tptp2017-02-06 16:57 281  
[ ]hallmar1__569_18.min1.thm1.tptp2017-02-06 16:57 281  
[ ]hallmar1__825_25.min1.thm1.tptp2017-02-06 16:57 362  
[ ]hallmar1__829_23.min1.thm1.tptp2017-02-06 16:57 354  
[ ]hallmar1__851_25.min1.thm1.tptp2017-02-06 16:57 362  
[ ]hallmar1__855_23.min1.thm1.tptp2017-02-06 16:57 354  
[ ]heine__351_30.min1.thm1.tptp2017-02-06 16:57 424  
[ ]helly__689_34.min1.thm1.tptp2017-02-06 16:57 360  
[ ]helly__696_34.min1.thm1.tptp2017-02-06 16:57 360  
[ ]helly__1667_13.min1.thm1.tptp2017-02-06 16:57 260  
[ ]helly__2277_32.min1.thm1.tptp2017-02-06 16:57 936  
[ ]hermitan__704_17.min1.thm1.tptp2017-02-06 16:57 542  
[ ]hermitan__2417_15.min1.thm1.tptp2017-02-06 16:57 616  
[ ]heyting2__84_12.min1.thm1.tptp2017-02-06 16:57 272  
[ ]heyting2__481_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]heyting2__1008_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]heyting2__1154_17.min1.thm1.tptp2017-02-06 16:57 614  
[ ]heyting2__1166_11.min1.thm1.tptp2017-02-06 16:57 270  
[ ]heyting2__1193_17.min1.thm1.tptp2017-02-06 16:57 590  
[ ]heyting3__1391_21.min1.thm1.tptp2017-02-06 16:57 278  
[ ]hfdiff_1__101_27.min1.thm1.tptp2017-02-06 16:57 348  
[ ]hfdiff_1__111_12.min1.thm1.tptp2017-02-06 16:57 264  
[ ]hfdiff_1__2401_15.min1.thm1.tptp2017-02-06 16:57 323  
[ ]hfdiff_1__2416_35.min1.thm1.tptp2017-02-06 16:57 572  
[ ]hfdiff_1__2422_17.min1.thm1.tptp2017-02-06 16:57 447  
[ ]hfdiff_1__2433_14.min1.thm1.tptp2017-02-06 16:57 312  
[ ]hfdiff_1__2441_36.min1.thm1.tptp2017-02-06 16:57 564  
[ ]hilbasis__251_21.min1.thm1.tptp2017-02-06 16:57 292  
[ ]hilbasis__284_21.min1.thm1.tptp2017-02-06 16:57 296  
[ ]hilbasis__1331_27.min1.thm1.tptp2017-02-06 16:57 414  
[ ]hilbasis__1380_24.min1.thm1.tptp2017-02-06 16:57 285  
[ ]hilbert2__885_18.min1.thm1.tptp2017-02-06 16:57 286  
[ ]hilbert2__899_47.min1.thm1.tptp2017-02-06 16:57 510  
[ ]hilbert2__1354_36.min1.thm1.tptp2017-02-06 16:57 485  
[ ]hilbert2__1374_41.min1.thm1.tptp2017-02-06 16:57 429  
[ ]hilbert2__1396_35.min1.thm1.tptp2017-02-06 16:57 490  
[ ]hilbert2__1405_39.min1.thm1.tptp2017-02-06 16:57 493  
[ ]hilbert2__1439_39.min1.thm1.tptp2017-02-06 16:57 493  
[ ]hilbert2__1447_43.min1.thm1.tptp2017-02-06 16:57 493  
[ ]hilbert2__1454_38.min1.thm1.tptp2017-02-06 16:57 369  
[ ]hilbert2__1481_36.min1.thm1.tptp2017-02-06 16:57 485  
[ ]hilbert2__1501_40.min1.thm1.tptp2017-02-06 16:57 429  
[ ]hilbert2__1523_33.min1.thm1.tptp2017-02-06 16:57 490  
[ ]hilbert2__1532_37.min1.thm1.tptp2017-02-06 16:57 493  
[ ]hilbert2__1566_37.min1.thm1.tptp2017-02-06 16:57 493  
[ ]hilbert2__1574_43.min1.thm1.tptp2017-02-06 16:57 493  
[ ]hilbert2__1581_37.min1.thm1.tptp2017-02-06 16:57 369  
[ ]hilbert3__409_19.min1.thm1.tptp2017-02-06 16:57 271  
[ ]hurwitz__112_35.min1.thm1.tptp2017-02-06 16:57 502  
[ ]hurwitz__717_30.min1.thm1.tptp2017-02-06 16:57 478  
[ ]hurwitz__2321_26.min1.thm1.tptp2017-02-06 16:57 332  
[ ]ideal_1__3116_17.min1.thm1.tptp2017-02-06 16:57 272  
[ ]instalg1__1414_26.min1.thm1.tptp2017-02-06 16:57 299  
[ ]int_4__251_13.min1.thm1.tptp2017-02-06 16:57 246  
[ ]int_5__320_21.min1.thm1.tptp2017-02-06 16:57 302  
[ ]int_7__759_21.min1.thm1.tptp2017-02-06 16:57 280  
[ ]int_7__1156_18.min1.thm1.tptp2017-02-06 16:57 263  
[ ]int_7__1183_10.min1.thm1.tptp2017-02-06 16:57 260  
[ ]int_7__1258_24.min1.thm1.tptp2017-02-06 16:57 302  
[ ]int_7__1302_24.min1.thm1.tptp2017-02-06 16:57 302  
[ ]integr1c__677_35.min1.thm1.tptp2017-02-06 16:57 783  
[ ]integr1c__824_35.min1.thm1.tptp2017-02-06 16:57 783  
[ ]integr1c__1057_35.min1.thm1.tptp2017-02-06 16:57 783  
[ ]integr1c__1206_35.min1.thm1.tptp2017-02-06 16:57 783  
[ ]integr19__235_20.min1.thm1.tptp2017-02-06 16:57 330  
[ ]integr19__1181_15.min1.thm1.tptp2017-02-06 16:57 332  
[ ]integr19__1673_18.min1.thm1.tptp2017-02-06 16:57 282  
[ ]integra1__160_17.min1.thm1.tptp2017-02-06 16:57 301  
[ ]interva1__157_21.min1.thm1.tptp2017-02-06 16:57 272  
[ ]interva1__161_12.min1.thm1.tptp2017-02-06 16:57 264  
[ ]interva1__816_29.min1.thm1.tptp2017-02-06 16:57 340  
[ ]jgraph_1__1162_26.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jgraph_5__2452_18.min1.thm1.tptp2017-02-06 16:57 326  
[ ]jgraph_5__2543_17.min1.thm1.tptp2017-02-06 16:57 304  
[ ]jgraph_6__1391_22.min1.thm1.tptp2017-02-06 16:57 366  
[ ]jgraph_6__4283_21.min1.thm1.tptp2017-02-06 16:57 436  
[ ]jgraph_6__4288_24.min1.thm1.tptp2017-02-06 16:57 426  
[ ]jgraph_6__4301_33.min1.thm1.tptp2017-02-06 16:57 946  
[ ]jgraph_6__4307_62.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]jgraph_6__4335_21.min1.thm1.tptp2017-02-06 16:57 436  
[ ]jgraph_6__4340_24.min1.thm1.tptp2017-02-06 16:57 426  
[ ]jgraph_6__4353_34.min1.thm1.tptp2017-02-06 16:57 946  
[ ]jgraph_6__4359_62.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]jgraph_6__4422_21.min1.thm1.tptp2017-02-06 16:57 436  
[ ]jgraph_6__4427_24.min1.thm1.tptp2017-02-06 16:57 426  
[ ]jgraph_6__4440_33.min1.thm1.tptp2017-02-06 16:57 946  
[ ]jgraph_6__4446_62.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]jgraph_6__4474_21.min1.thm1.tptp2017-02-06 16:57 436  
[ ]jgraph_6__4479_24.min1.thm1.tptp2017-02-06 16:57 426  
[ ]jgraph_6__4492_34.min1.thm1.tptp2017-02-06 16:57 946  
[ ]jgraph_6__4498_62.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]jgraph_8__522_18.min1.thm1.tptp2017-02-06 16:57 284  
[ ]jgraph_8__529_18.min1.thm1.tptp2017-02-06 16:57 284  
[ ]jordan1d__989_49.min1.thm1.tptp2017-02-06 16:57 538  
[ ]jordan1d__1104_48.min1.thm1.tptp2017-02-06 16:57 538  
[ ]jordan1d__1220_48.min1.thm1.tptp2017-02-06 16:57 538  
[ ]jordan1d__1336_49.min1.thm1.tptp2017-02-06 16:57 538  
[ ]jordan1d__1436_49.min1.thm1.tptp2017-02-06 16:57 538  
[ ]jordan1d__1536_48.min1.thm1.tptp2017-02-06 16:57 538  
[ ]jordan1d__1636_48.min1.thm1.tptp2017-02-06 16:57 538  
[ ]jordan1e__894_29.min1.thm1.tptp2017-02-06 16:57 702  
[ ]jordan1e__913_31.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]jordan1e__1092_45.min1.thm1.tptp2017-02-06 16:57 666  
[ ]jordan1e__1204_45.min1.thm1.tptp2017-02-06 16:57 666  
[ ]jordan1e__1319_45.min1.thm1.tptp2017-02-06 16:57 666  
[ ]jordan1g__927_29.min1.thm1.tptp2017-02-06 16:57 460  
[ ]jordan1g__946_31.min1.thm1.tptp2017-02-06 16:57 704  
[ ]jordan1g__2442_42.min1.thm1.tptp2017-02-06 16:57 595  
[ ]jordan1g__3485_33.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan1g__3658_34.min1.thm1.tptp2017-02-06 16:57 1.5K 
[ ]jordan1g__3868_32.min1.thm1.tptp2017-02-06 16:57 909  
[ ]jordan1g__3933_74.min1.thm1.tptp2017-02-06 16:57 2.5K 
[ ]jordan1i__1198_26.min1.thm1.tptp2017-02-06 16:57 562  
[ ]jordan1i__1282_26.min1.thm1.tptp2017-02-06 16:57 562  
[ ]jordan1i__1423_26.min1.thm1.tptp2017-02-06 16:57 562  
[ ]jordan1i__1507_26.min1.thm1.tptp2017-02-06 16:57 562  
[ ]jordan1i__1647_28.min1.thm1.tptp2017-02-06 16:57 566  
[ ]jordan1i__1731_28.min1.thm1.tptp2017-02-06 16:57 566  
[ ]jordan1i__1876_28.min1.thm1.tptp2017-02-06 16:57 566  
[ ]jordan1i__1960_28.min1.thm1.tptp2017-02-06 16:57 566  
[ ]jordan1j__265_33.min1.thm1.tptp2017-02-06 16:57 464  
[ ]jordan1j__279_28.min1.thm1.tptp2017-02-06 16:57 482  
[ ]jordan1j__303_31.min1.thm1.tptp2017-02-06 16:57 688  
[ ]jordan1j__1689_61.min1.thm1.tptp2017-02-06 16:57 938  
[ ]jordan1j__2998_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan1j__3016_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan1j__3034_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan1j__3129_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan1j__3163_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan1j__3182_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan1j__3213_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]jordan1j__3537_22.min1.thm1.tptp2017-02-06 16:57 468  
[ ]jordan1j__3706_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan1j__3724_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan1j__3742_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan1j__3837_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan1j__3871_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan1j__3890_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan1j__3921_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]jordan1j__4245_22.min1.thm1.tptp2017-02-06 16:57 468  
[ ]jordan2b__726_10.min1.thm1.tptp2017-02-06 16:57 278  
[ ]jordan3__376_16.min1.thm1.tptp2017-02-06 16:57 390  
[ ]jordan3__447_33.min1.thm1.tptp2017-02-06 16:57 472  
[ ]jordan4__3462_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]jordan4__3625_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]jordan4__3984_15.min1.thm1.tptp2017-02-06 16:57 326  
[ ]jordan4__3998_15.min1.thm1.tptp2017-02-06 16:57 330  
[ ]jordan5b__1312_29.min1.thm1.tptp2017-02-06 16:57 510  
[ ]jordan5b__1834_27.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan5c__243_21.min1.thm1.tptp2017-02-06 16:57 404  
[ ]jordan5c__486_21.min1.thm1.tptp2017-02-06 16:57 404  
[ ]jordan6__1018_11.min1.thm1.tptp2017-02-06 16:57 264  
[ ]jordan6__1065_11.min1.thm1.tptp2017-02-06 16:57 264  
[ ]jordan7__474_19.min1.thm1.tptp2017-02-06 16:57 413  
[ ]jordan7__478_14.min1.thm1.tptp2017-02-06 16:57 264  
[ ]jordan7__514_21.min1.thm1.tptp2017-02-06 16:57 280  
[ ]jordan7__524_11.min1.thm1.tptp2017-02-06 16:57 264  
[ ]jordan7__569_19.min1.thm1.tptp2017-02-06 16:57 472  
[ ]jordan7__574_18.min1.thm1.tptp2017-02-06 16:57 292  
[ ]jordan11__435_23.min1.thm1.tptp2017-02-06 16:57 646  
[ ]jordan11__439_54.min1.thm1.tptp2017-02-06 16:57 638  
[ ]jordan11__492_23.min1.thm1.tptp2017-02-06 16:57 650  
[ ]jordan11__496_54.min1.thm1.tptp2017-02-06 16:57 642  
[ ]jordan12__1270_38.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan12__1332_30.min1.thm1.tptp2017-02-06 16:57 522  
[ ]jordan12__2358_13.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan15__2213_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan15__2231_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__2249_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__2345_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__2379_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__2398_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__2429_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]jordan15__2754_22.min1.thm1.tptp2017-02-06 16:57 468  
[ ]jordan15__2924_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan15__2942_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__2960_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__3056_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__3090_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__3109_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__3140_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]jordan15__3465_22.min1.thm1.tptp2017-02-06 16:57 468  
[ ]jordan15__3792_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan15__3810_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__3828_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__3924_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__3958_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__3977_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__4008_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]jordan15__4332_22.min1.thm1.tptp2017-02-06 16:57 468  
[ ]jordan15__4501_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan15__4519_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__4537_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__4633_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__4667_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__4686_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__4717_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]jordan15__5041_22.min1.thm1.tptp2017-02-06 16:57 468  
[ ]jordan15__5388_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__5425_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__5477_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__5522_23.min1.thm1.tptp2017-02-06 16:57 420  
[ ]jordan15__5539_31.min1.thm1.tptp2017-02-06 16:57 480  
[ ]jordan15__5577_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan15__5618_18.min1.thm1.tptp2017-02-06 16:57 518  
[ ]jordan15__5957_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]jordan15__6169_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__6206_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__6260_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__6305_23.min1.thm1.tptp2017-02-06 16:57 420  
[ ]jordan15__6322_31.min1.thm1.tptp2017-02-06 16:57 480  
[ ]jordan15__6360_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan15__6401_18.min1.thm1.tptp2017-02-06 16:57 518  
[ ]jordan15__6739_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]jordan15__6951_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__6986_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__7040_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__7085_23.min1.thm1.tptp2017-02-06 16:57 420  
[ ]jordan15__7100_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan15__7123_31.min1.thm1.tptp2017-02-06 16:57 480  
[ ]jordan15__7161_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan15__7519_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]jordan15__7731_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__7766_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan15__7820_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan15__7865_23.min1.thm1.tptp2017-02-06 16:57 420  
[ ]jordan15__7880_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan15__7903_31.min1.thm1.tptp2017-02-06 16:57 480  
[ ]jordan15__7941_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan15__8299_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]jordan15__8537_68.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan15__8558_70.min1.thm1.tptp2017-02-06 16:57 1.4K 
[ ]jordan15__8586_32.min1.thm1.tptp2017-02-06 16:57 590  
[ ]jordan15__8613_33.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan15__8661_32.min1.thm1.tptp2017-02-06 16:57 590  
[ ]jordan15__8688_33.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan15__8870_68.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan15__8891_70.min1.thm1.tptp2017-02-06 16:57 1.4K 
[ ]jordan15__8919_32.min1.thm1.tptp2017-02-06 16:57 590  
[ ]jordan15__8946_33.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan15__8994_32.min1.thm1.tptp2017-02-06 16:57 590  
[ ]jordan15__9021_33.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan19__298_43.min1.thm1.tptp2017-02-06 16:57 683  
[ ]jordan19__1057_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan19__1075_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__1094_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan19__1192_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__1226_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__1244_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan19__1275_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]jordan19__1578_22.min1.thm1.tptp2017-02-06 16:57 468  
[ ]jordan19__1750_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan19__1768_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__1787_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan19__1885_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__1919_16.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__1937_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan19__1968_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]jordan19__2271_22.min1.thm1.tptp2017-02-06 16:57 468  
[ ]jordan19__2619_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan19__2639_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__2660_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan19__2775_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan19__2808_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan19__2827_23.min1.thm1.tptp2017-02-06 16:57 420  
[ ]jordan19__2857_31.min1.thm1.tptp2017-02-06 16:57 484  
[ ]jordan19__3165_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]jordan19__3366_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan19__3386_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__3407_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan19__3522_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan19__3555_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan19__3574_23.min1.thm1.tptp2017-02-06 16:57 420  
[ ]jordan19__3604_31.min1.thm1.tptp2017-02-06 16:57 484  
[ ]jordan19__3912_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]jordan19__4112_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan19__4132_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__4153_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan19__4268_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan19__4301_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan19__4320_23.min1.thm1.tptp2017-02-06 16:57 420  
[ ]jordan19__4350_31.min1.thm1.tptp2017-02-06 16:57 484  
[ ]jordan19__4658_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]jordan19__4858_15.min1.thm1.tptp2017-02-06 16:57 486  
[ ]jordan19__4878_15.min1.thm1.tptp2017-02-06 16:57 490  
[ ]jordan19__4899_17.min1.thm1.tptp2017-02-06 16:57 384  
[ ]jordan19__5014_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan19__5047_18.min1.thm1.tptp2017-02-06 16:57 514  
[ ]jordan19__5066_23.min1.thm1.tptp2017-02-06 16:57 420  
[ ]jordan19__5096_31.min1.thm1.tptp2017-02-06 16:57 484  
[ ]jordan19__5404_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]jordan19__5640_27.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan19__5653_12.min1.thm1.tptp2017-02-06 16:57 1.4K 
[ ]jordan19__5684_27.min1.thm1.tptp2017-02-06 16:57 590  
[ ]jordan19__5712_28.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan19__5759_27.min1.thm1.tptp2017-02-06 16:57 590  
[ ]jordan19__5788_28.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan19__5971_27.min1.thm1.tptp2017-02-06 16:57 1.3K 
[ ]jordan19__5984_12.min1.thm1.tptp2017-02-06 16:57 1.4K 
[ ]jordan19__6015_27.min1.thm1.tptp2017-02-06 16:57 590  
[ ]jordan19__6043_28.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan19__6090_27.min1.thm1.tptp2017-02-06 16:57 590  
[ ]jordan19__6119_28.min1.thm1.tptp2017-02-06 16:57 578  
[ ]jordan20__64_10.min1.thm1.tptp2017-02-06 16:57 272  
[ ]jordan20__1706_22.min1.thm1.tptp2017-02-06 16:57 283  
[ ]jordan20__1748_15.min1.thm1.tptp2017-02-06 16:57 281  
[ ]jordan20__1828_22.min1.thm1.tptp2017-02-06 16:57 283  
[ ]jordan20__2023_11.min1.thm1.tptp2017-02-06 16:57 278  
[ ]jordan20__2054_19.min1.thm1.tptp2017-02-06 16:57 278  
[ ]jordan20__2133_24.min1.thm1.tptp2017-02-06 16:57 288  
[ ]jordan20__2134_25.min1.thm1.tptp2017-02-06 16:57 281  
[ ]jordan20__2161_30.min1.thm1.tptp2017-02-06 16:57 291  
[ ]jordan20__2189_30.min1.thm1.tptp2017-02-06 16:57 337  
[ ]jordan20__2269_30.min1.thm1.tptp2017-02-06 16:57 337  
[ ]jordan20__2341_26.min1.thm1.tptp2017-02-06 16:57 313  
[ ]jordan20__2390_25.min1.thm1.tptp2017-02-06 16:57 281  
[ ]jordan20__2417_30.min1.thm1.tptp2017-02-06 16:57 291  
[ ]jordan20__2445_30.min1.thm1.tptp2017-02-06 16:57 337  
[ ]jordan20__2528_30.min1.thm1.tptp2017-02-06 16:57 337  
[ ]jordan20__2601_26.min1.thm1.tptp2017-02-06 16:57 313  
[ ]jordan23__3147_21.min1.thm1.tptp2017-02-06 16:57 440  
[ ]jordan23__3152_29.min1.thm1.tptp2017-02-06 16:57 432  
[ ]kolmog01__796_13.min1.thm1.tptp2017-02-06 16:57 286  
[ ]kolmog01__843_27.min1.thm1.tptp2017-02-06 16:57 522  
[ ]kolmog01__1957_37.min1.thm1.tptp2017-02-06 16:57 324  
[ ]kolmog01__1964_25.min1.thm1.tptp2017-02-06 16:57 514  
[ ]l_hospit__249_24.min1.thm1.tptp2017-02-06 16:57 318  
[ ]l_hospit__260_29.min1.thm1.tptp2017-02-06 16:57 372  
[ ]l_hospit__466_24.min1.thm1.tptp2017-02-06 16:57 318  
[ ]l_hospit__477_29.min1.thm1.tptp2017-02-06 16:57 372  
[ ]l_hospit__706_24.min1.thm1.tptp2017-02-06 16:57 318  
[ ]l_hospit__717_29.min1.thm1.tptp2017-02-06 16:57 372  
[ ]l_hospit__929_24.min1.thm1.tptp2017-02-06 16:57 318  
[ ]l_hospit__940_29.min1.thm1.tptp2017-02-06 16:57 372  
[ ]l_hospit__1299_24.min1.thm1.tptp2017-02-06 16:57 318  
[ ]l_hospit__1323_39.min1.thm1.tptp2017-02-06 16:57 478  
[ ]l_hospit__1698_24.min1.thm1.tptp2017-02-06 16:57 318  
[ ]l_hospit__1722_39.min1.thm1.tptp2017-02-06 16:57 478  
[ ]l_hospit__1966_24.min1.thm1.tptp2017-02-06 16:57 318  
[ ]l_hospit__1977_29.min1.thm1.tptp2017-02-06 16:57 372  
[ ]l_hospit__2198_24.min1.thm1.tptp2017-02-06 16:57 318  
[ ]l_hospit__2209_29.min1.thm1.tptp2017-02-06 16:57 372  
[ ]l_hospit__2453_24.min1.thm1.tptp2017-02-06 16:57 324  
[ ]l_hospit__2464_29.min1.thm1.tptp2017-02-06 16:57 380  
[ ]l_hospit__2692_24.min1.thm1.tptp2017-02-06 16:57 324  
[ ]l_hospit__2703_29.min1.thm1.tptp2017-02-06 16:57 380  
[ ]lang1__410_41.min1.thm1.tptp2017-02-06 16:57 288  
[ ]lang1__548_19.min1.thm1.tptp2017-02-06 16:57 258  
[ ]lang1__553_13.min1.thm1.tptp2017-02-06 16:57 250  
[ ]lang1__594_19.min1.thm1.tptp2017-02-06 16:57 260  
[ ]lang1__598_15.min1.thm1.tptp2017-02-06 16:57 253  
[ ]lang1__662_19.min1.thm1.tptp2017-02-06 16:57 288  
[ ]lang1__667_17.min1.thm1.tptp2017-02-06 16:57 280  
[ ]lang1__692_19.min1.thm1.tptp2017-02-06 16:57 260  
[ ]lang1__697_12.min1.thm1.tptp2017-02-06 16:57 252  
[ ]lang1__822_24.min1.thm1.tptp2017-02-06 16:57 264  
[ ]laplace__434_13.min1.thm1.tptp2017-02-06 16:57 275  
[ ]laplace__454_12.min1.thm1.tptp2017-02-06 16:57 275  
[ ]laplace__660_21.min1.thm1.tptp2017-02-06 16:57 275  
[ ]latsubgr__933_17.min1.thm1.tptp2017-02-06 16:57 310  
[ ]latsubgr__938_20.min1.thm1.tptp2017-02-06 16:57 319  
[ ]lattice3__2110_19.min1.thm1.tptp2017-02-06 16:57 351  
[ ]lattice3__2114_17.min1.thm1.tptp2017-02-06 16:57 276  
[ ]lattice5__1522_21.min1.thm1.tptp2017-02-06 16:57 312  
[ ]lattice5__1526_30.min1.thm1.tptp2017-02-06 16:57 374  
[ ]lattice5__1539_28.min1.thm1.tptp2017-02-06 16:57 352  
[ ]lattice5__5430_24.min1.thm1.tptp2017-02-06 16:57 374  
[ ]lattice6__260_26.min1.thm1.tptp2017-02-06 16:57 304  
[ ]lattice6__1854_24.min1.thm1.tptp2017-02-06 16:57 304  
[ ]lattice6__1890_21.min1.thm1.tptp2017-02-06 16:57 304  
[ ]lattice8__732_21.min1.thm1.tptp2017-02-06 16:57 312  
[ ]lattice8__736_26.min1.thm1.tptp2017-02-06 16:57 330  
[ ]lattice8__3956_24.min1.thm1.tptp2017-02-06 16:57 374  
[ ]lattice8__4099_24.min1.thm1.tptp2017-02-06 16:57 374  
[ ]lexbfs__1261_30.min1.thm1.tptp2017-02-06 16:57 289  
[ ]limfunc1__511_21.min1.thm1.tptp2017-02-06 16:57 272  
[ ]limfunc1__515_10.min1.thm1.tptp2017-02-06 16:57 268  
[ ]limfunc1__572_21.min1.thm1.tptp2017-02-06 16:57 272  
[ ]limfunc1__576_10.min1.thm1.tptp2017-02-06 16:57 268  
[ ]limfunc1__4666_22.min1.thm1.tptp2017-02-06 16:57 329  
[ ]limfunc1__4730_22.min1.thm1.tptp2017-02-06 16:57 329  
[ ]limfunc1__4794_22.min1.thm1.tptp2017-02-06 16:57 329  
[ ]limfunc1__4858_22.min1.thm1.tptp2017-02-06 16:57 329  
[ ]limfunc1__4933_31.min1.thm1.tptp2017-02-06 16:57 355  
[ ]limfunc1__4950_31.min1.thm1.tptp2017-02-06 16:57 355  
[ ]limfunc1__5025_31.min1.thm1.tptp2017-02-06 16:57 355  
[ ]limfunc1__5042_31.min1.thm1.tptp2017-02-06 16:57 355  
[ ]limfunc1__5117_31.min1.thm1.tptp2017-02-06 16:57 355  
[ ]limfunc1__5134_31.min1.thm1.tptp2017-02-06 16:57 355  
[ ]limfunc1__5209_31.min1.thm1.tptp2017-02-06 16:57 355  
[ ]limfunc1__5226_31.min1.thm1.tptp2017-02-06 16:57 355  
[ ]limfunc2__4390_31.min1.thm1.tptp2017-02-06 16:57 349  
[ ]limfunc2__4408_31.min1.thm1.tptp2017-02-06 16:57 349  
[ ]limfunc2__4615_31.min1.thm1.tptp2017-02-06 16:57 349  
[ ]limfunc2__4634_31.min1.thm1.tptp2017-02-06 16:57 349  
[ ]limfunc2__4830_22.min1.thm1.tptp2017-02-06 16:57 323  
[ ]limfunc2__4914_22.min1.thm1.tptp2017-02-06 16:57 323  
[ ]limfunc2__4998_22.min1.thm1.tptp2017-02-06 16:57 323  
[ ]limfunc2__5082_22.min1.thm1.tptp2017-02-06 16:57 323  
[ ]limfunc3__772_29.min1.thm1.tptp2017-02-06 16:57 393  
[ ]limfunc3__899_29.min1.thm1.tptp2017-02-06 16:57 393  
[ ]limfunc3__1093_24.min1.thm1.tptp2017-02-06 16:57 397  
[ ]limfunc3__1251_29.min1.thm1.tptp2017-02-06 16:57 393  
[ ]limfunc3__1375_29.min1.thm1.tptp2017-02-06 16:57 393  
[ ]limfunc3__1569_24.min1.thm1.tptp2017-02-06 16:57 397  
[ ]limfunc3__2644_29.min1.thm1.tptp2017-02-06 16:57 393  
[ ]limfunc3__2768_29.min1.thm1.tptp2017-02-06 16:57 393  
[ ]limfunc3__2968_24.min1.thm1.tptp2017-02-06 16:57 397  
[ ]limfunc3__3989_22.min1.thm1.tptp2017-02-06 16:57 325  
[ ]limfunc3__3994_22.min1.thm1.tptp2017-02-06 16:57 325  
[ ]limfunc3__4088_22.min1.thm1.tptp2017-02-06 16:57 325  
[ ]limfunc3__4093_22.min1.thm1.tptp2017-02-06 16:57 325  
[ ]limfunc4__1656_41.min1.thm1.tptp2017-02-06 16:57 561  
[ ]limfunc4__1723_41.min1.thm1.tptp2017-02-06 16:57 561  
[ ]limfunc4__1923_47.min1.thm1.tptp2017-02-06 16:57 561  
[ ]limfunc4__1985_47.min1.thm1.tptp2017-02-06 16:57 561  
[ ]limfunc4__2039_46.min1.thm1.tptp2017-02-06 16:57 529  
[ ]limfunc4__2098_46.min1.thm1.tptp2017-02-06 16:57 529  
[ ]limfunc4__2157_46.min1.thm1.tptp2017-02-06 16:57 529  
[ ]limfunc4__2216_46.min1.thm1.tptp2017-02-06 16:57 529  
[ ]limfunc4__2421_46.min1.thm1.tptp2017-02-06 16:57 561  
[ ]limfunc4__2483_46.min1.thm1.tptp2017-02-06 16:57 561  
[ ]limfunc4__3386_46.min1.thm1.tptp2017-02-06 16:57 529  
[ ]limfunc4__3451_46.min1.thm1.tptp2017-02-06 16:57 529  
[ ]limfunc4__3587_46.min1.thm1.tptp2017-02-06 16:57 561  
[ ]limfunc4__3730_47.min1.thm1.tptp2017-02-06 16:57 561  
[ ]limfunc4__3803_41.min1.thm1.tptp2017-02-06 16:57 561  
[ ]ltlaxio1__2216_15.min1.thm1.tptp2017-02-06 16:57 298  
[ ]margrel1__104_45.min1.thm1.tptp2017-02-06 16:57 379  
[ ]margrel1__390_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]margrel1__1181_19.min1.thm1.tptp2017-02-06 16:57 274  
[ ]margrel1__1248_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]matrix11__320_17.min1.thm1.tptp2017-02-06 16:57 300  
[ ]matrix11__478_17.min1.thm1.tptp2017-02-06 16:57 306  
[ ]matrix11__809_17.min1.thm1.tptp2017-02-06 16:57 306  
[ ]matrix11__1412_11.min1.thm1.tptp2017-02-06 16:57 278  
[ ]matrix11__1829_26.min1.thm1.tptp2017-02-06 16:57 396  
[ ]matrix11__2827_17.min1.thm1.tptp2017-02-06 16:57 306  
[ ]matrix11__3355_15.min1.thm1.tptp2017-02-06 16:57 298  
[ ]matrix11__3745_17.min1.thm1.tptp2017-02-06 16:57 306  
[ ]matrix11__4588_13.min1.thm1.tptp2017-02-06 16:57 291  
[ ]matrix11__4609_17.min1.thm1.tptp2017-02-06 16:57 288  
[ ]matrix11__5136_18.min1.thm1.tptp2017-02-06 16:57 282  
[ ]matrix13__1778_13.min1.thm1.tptp2017-02-06 16:57 332  
[ ]matrix13__1817_16.min1.thm1.tptp2017-02-06 16:57 347  
[ ]matrix13__1912_56.min1.thm1.tptp2017-02-06 16:57 848  
[ ]matrix13__1933_18.min1.thm1.tptp2017-02-06 16:57 291  
[ ]matrix13__1940_12.min1.thm1.tptp2017-02-06 16:57 286  
[ ]matrix14__4222_19.min1.thm1.tptp2017-02-06 16:57 290  
[ ]matrix14__4246_19.min1.thm1.tptp2017-02-06 16:57 290  
[ ]matrix14__4541_27.min1.thm1.tptp2017-02-06 16:57 338  
[ ]matrix14__4578_27.min1.thm1.tptp2017-02-06 16:57 338  
[ ]matrix_1__332_19.min1.thm1.tptp2017-02-06 16:57 304  
[ ]matrix_2__949_22.min1.thm1.tptp2017-02-06 16:57 284  
[ ]matrix_7__645_22.min1.thm1.tptp2017-02-06 16:57 438  
[ ]matrix_7__1360_24.min1.thm1.tptp2017-02-06 16:57 319  
[ ]matrix_7__1376_22.min1.thm1.tptp2017-02-06 16:57 440  
[ ]matrix_7__1410_30.min1.thm1.tptp2017-02-06 16:57 316  
[ ]matrix_7__1419_34.min1.thm1.tptp2017-02-06 16:57 319  
[ ]matrix_7__1917_24.min1.thm1.tptp2017-02-06 16:57 319  
[ ]matrix_7__1933_22.min1.thm1.tptp2017-02-06 16:57 440  
[ ]matrix_7__1967_30.min1.thm1.tptp2017-02-06 16:57 316  
[ ]matrix_7__1976_34.min1.thm1.tptp2017-02-06 16:57 319  
[ ]matrix_7__2864_22.min1.thm1.tptp2017-02-06 16:57 416  
[ ]matrix_7__2875_24.min1.thm1.tptp2017-02-06 16:57 305  
[ ]matrix_7__2922_23.min1.thm1.tptp2017-02-06 16:57 314  
[ ]matrlin__1459_16.min1.thm1.tptp2017-02-06 16:57 270  
[ ]matroid0__472_27.min1.thm1.tptp2017-02-06 16:57 431  
[ ]matroid0__621_21.min1.thm1.tptp2017-02-06 16:57 290  
[ ]matrprob__1115_16.min1.thm1.tptp2017-02-06 16:57 274  
[ ]matrtop2__577_17.min1.thm1.tptp2017-02-06 16:57 400  
[ ]matrtop2__632_18.min1.thm1.tptp2017-02-06 16:57 302  
[ ]matrtop2__791_24.min1.thm1.tptp2017-02-06 16:57 413  
[ ]matrtop2__1140_33.min1.thm1.tptp2017-02-06 16:57 780  
[ ]mcart_1__114_17.min1.thm1.tptp2017-02-06 16:57 404  
[ ]mcart_1__1424_14.min1.thm1.tptp2017-02-06 16:57 272  
[ ]measure6__1032_24.min1.thm1.tptp2017-02-06 16:57 333  
[ ]measure8__314_20.min1.thm1.tptp2017-02-06 16:57 388  
[ ]measure8__1196_22.min1.thm1.tptp2017-02-06 16:57 290  
[ ]member_1__262_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]member_1__267_13.min1.thm1.tptp2017-02-06 16:57 296  
[ ]member_1__533_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]member_1__538_13.min1.thm1.tptp2017-02-06 16:57 294  
[ ]member_1__691_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]member_1__696_13.min1.thm1.tptp2017-02-06 16:57 296  
[ ]member_1__969_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]member_1__974_13.min1.thm1.tptp2017-02-06 16:57 294  
[ ]member_1__1140_22.min1.thm1.tptp2017-02-06 16:57 374  
[ ]member_1__1146_14.min1.thm1.tptp2017-02-06 16:57 328  
[ ]member_1__1415_22.min1.thm1.tptp2017-02-06 16:57 374  
[ ]member_1__1421_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]member_1__2009_22.min1.thm1.tptp2017-02-06 16:57 384  
[ ]member_1__2015_14.min1.thm1.tptp2017-02-06 16:57 336  
[ ]member_1__2366_22.min1.thm1.tptp2017-02-06 16:57 384  
[ ]member_1__2372_14.min1.thm1.tptp2017-02-06 16:57 334  
[ ]member_1__2732_13.min1.thm1.tptp2017-02-06 16:57 284  
[ ]member_1__2890_13.min1.thm1.tptp2017-02-06 16:57 284  
[ ]member_1__2993_13.min1.thm1.tptp2017-02-06 16:57 272  
[ ]member_1__3205_13.min1.thm1.tptp2017-02-06 16:57 284  
[ ]member_1__3440_13.min1.thm1.tptp2017-02-06 16:57 284  
[ ]member_1__3588_13.min1.thm1.tptp2017-02-06 16:57 284  
[ ]member_1__3732_13.min1.thm1.tptp2017-02-06 16:57 284  
[ ]member_1__3906_11.min1.thm1.tptp2017-02-06 16:57 264  
[ ]member_1__3941_13.min1.thm1.tptp2017-02-06 16:57 262  
[ ]membered__580_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]membered__590_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]membered__600_18.min1.thm1.tptp2017-02-06 16:57 310  
[ ]membered__610_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]membered__620_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]membered__630_18.min1.thm1.tptp2017-02-06 16:57 312  
[ ]mesfunc1__1050_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]mesfunc1__1055_20.min1.thm1.tptp2017-02-06 16:57 354  
[ ]mesfunc1__1069_23.min1.thm1.tptp2017-02-06 16:57 358  
[ ]mesfunc1__1074_17.min1.thm1.tptp2017-02-06 16:57 354  
[ ]mesfunc2__374_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]mesfunc2__377_28.min1.thm1.tptp2017-02-06 16:57 380  
[ ]mesfunc2__389_20.min1.thm1.tptp2017-02-06 16:57 380  
[ ]mesfunc2__404_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]mesfunc2__406_28.min1.thm1.tptp2017-02-06 16:57 380  
[ ]mesfunc2__418_20.min1.thm1.tptp2017-02-06 16:57 380  
[ ]mesfunc2__422_25.min1.thm1.tptp2017-02-06 16:57 324  
[ ]mesfunc2__729_26.min1.thm1.tptp2017-02-06 16:57 388  
[ ]mesfunc2__730_23.min1.thm1.tptp2017-02-06 16:57 388  
[ ]mesfunc2__741_28.min1.thm1.tptp2017-02-06 16:57 388  
[ ]mesfunc2__753_28.min1.thm1.tptp2017-02-06 16:57 388  
[ ]mesfunc2__764_28.min1.thm1.tptp2017-02-06 16:57 388  
[ ]mesfunc3__1487_31.min1.thm1.tptp2017-02-06 16:57 341  
[ ]mesfunc3__1519_33.min1.thm1.tptp2017-02-06 16:57 314  
[ ]mesfunc5__1470_14.min1.thm1.tptp2017-02-06 16:57 338  
[ ]mesfunc5__1482_17.min1.thm1.tptp2017-02-06 16:57 338  
[ ]mesfunc5__2423_28.min1.thm1.tptp2017-02-06 16:57 333  
[ ]mesfunc5__2427_28.min1.thm1.tptp2017-02-06 16:57 333  
[ ]mesfunc5__2815_24.min1.thm1.tptp2017-02-06 16:57 330  
[ ]mesfunc5__2828_23.min1.thm1.tptp2017-02-06 16:57 330  
[ ]mesfunc5__2844_24.min1.thm1.tptp2017-02-06 16:57 330  
[ ]mesfunc5__2857_23.min1.thm1.tptp2017-02-06 16:57 330  
[ ]mesfunc5__2882_23.min1.thm1.tptp2017-02-06 16:57 330  
[ ]mesfunc5__2895_24.min1.thm1.tptp2017-02-06 16:57 330  
[ ]mesfunc5__2909_23.min1.thm1.tptp2017-02-06 16:57 330  
[ ]mesfunc5__2922_24.min1.thm1.tptp2017-02-06 16:57 330  
[ ]mesfunc5__2998_43.min1.thm1.tptp2017-02-06 16:57 583  
[ ]mesfunc5__3001_48.min1.thm1.tptp2017-02-06 16:57 584  
[ ]mesfunc5__3024_43.min1.thm1.tptp2017-02-06 16:57 584  
[ ]mesfunc5__3027_48.min1.thm1.tptp2017-02-06 16:57 584  
[ ]mesfunc5__3063_39.min1.thm1.tptp2017-02-06 16:57 568  
[ ]mesfunc5__3069_39.min1.thm1.tptp2017-02-06 16:57 568  
[ ]mesfunc5__3139_29.min1.thm1.tptp2017-02-06 16:57 338  
[ ]mesfunc5__6889_14.min1.thm1.tptp2017-02-06 16:57 274  
[ ]mesfunc5__6901_19.min1.thm1.tptp2017-02-06 16:57 274  
[ ]mesfunc5__6913_14.min1.thm1.tptp2017-02-06 16:57 274  
[ ]mesfunc5__7407_19.min1.thm1.tptp2017-02-06 16:57 318  
[ ]mesfunc5__7475_27.min1.thm1.tptp2017-02-06 16:57 415  
[ ]mesfunc5__11330_23.min1.thm1.tptp2017-02-06 16:57 352  
[ ]mesfunc7__999_24.min1.thm1.tptp2017-02-06 16:57 314  
[ ]mesfunc7__1003_25.min1.thm1.tptp2017-02-06 16:57 315  
[ ]mesfunc8__1748_13.min1.thm1.tptp2017-02-06 16:57 279  
[ ]mesfunc9__1465_41.min1.thm1.tptp2017-02-06 16:57 485  
[ ]mesfunc9__1536_41.min1.thm1.tptp2017-02-06 16:57 485  
[ ]mesfunc9__1592_29.min1.thm1.tptp2017-02-06 16:57 498  
[ ]mesfunc9__1599_27.min1.thm1.tptp2017-02-06 16:57 474  
[ ]mesfunc9__1613_29.min1.thm1.tptp2017-02-06 16:57 498  
[ ]mesfunc9__1620_28.min1.thm1.tptp2017-02-06 16:57 474  
[ ]mesfunc9__1715_24.min1.thm1.tptp2017-02-06 16:57 438  
[ ]metrizts__1360_23.min1.thm1.tptp2017-02-06 16:57 315  
[ ]metrizts__2157_23.min1.thm1.tptp2017-02-06 16:57 302  
[ ]mfold_1__60_19.min1.thm1.tptp2017-02-06 16:57 332  
[ ]mfold_1__60_41.min1.thm1.tptp2017-02-06 16:57 332  
[ ]mfold_2__1290_21.min1.thm1.tptp2017-02-06 16:57 254  
[ ]mfold_2__1520_20.min1.thm1.tptp2017-02-06 16:57 326  
[ ]mfold_2__1896_21.min1.thm1.tptp2017-02-06 16:57 459  
[ ]mfold_2__2360_24.min1.thm1.tptp2017-02-06 16:57 715  
[ ]midsp_3__144_16.min1.thm1.tptp2017-02-06 16:57 261  
[ ]mmlquery__835_17.min1.thm1.tptp2017-02-06 16:57 389  
[ ]mmlquery__1152_14.min1.thm1.tptp2017-02-06 16:57 430  
[ ]modal_1__524_25.min1.thm1.tptp2017-02-06 16:57 342  
[ ]modal_1__2054_20.min1.thm1.tptp2017-02-06 16:57 418  
[ ]modelc_1__439_26.min1.thm1.tptp2017-02-06 16:57 289  
[ ]modelc_1__501_27.min1.thm1.tptp2017-02-06 16:57 307  
[ ]modelc_1__4464_28.min1.thm1.tptp2017-02-06 16:57 645  
[ ]modelc_1__4526_27.min1.thm1.tptp2017-02-06 16:57 601  
[ ]modelc_2__412_26.min1.thm1.tptp2017-02-06 16:57 289  
[ ]modelc_2__483_27.min1.thm1.tptp2017-02-06 16:57 307  
[ ]modelc_3__658_48.min1.thm1.tptp2017-02-06 16:57 362  
[ ]modelc_3__699_30.min1.thm1.tptp2017-02-06 16:57 310  
[ ]modelc_3__707_34.min1.thm1.tptp2017-02-06 16:57 313  
[ ]modelc_3__882_28.min1.thm1.tptp2017-02-06 16:57 302  
[ ]modelc_3__888_32.min1.thm1.tptp2017-02-06 16:57 305  
[ ]modelc_3__990_22.min1.thm1.tptp2017-02-06 16:57 470  
[ ]modelc_3__1085_28.min1.thm1.tptp2017-02-06 16:57 302  
[ ]modelc_3__1091_32.min1.thm1.tptp2017-02-06 16:57 305  
[ ]modelc_3__1202_22.min1.thm1.tptp2017-02-06 16:57 470  
[ ]modelc_3__1297_28.min1.thm1.tptp2017-02-06 16:57 302  
[ ]modelc_3__1303_32.min1.thm1.tptp2017-02-06 16:57 305  
[ ]modelc_3__1389_26.min1.thm1.tptp2017-02-06 16:57 298  
[ ]modelc_3__1444_26.min1.thm1.tptp2017-02-06 16:57 298  
[ ]modelc_3__1487_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]modelc_3__1855_25.min1.thm1.tptp2017-02-06 16:57 349  
[ ]modelc_3__2069_13.min1.thm1.tptp2017-02-06 16:57 270  
[ ]modelc_3__3539_22.min1.thm1.tptp2017-02-06 16:57 326  
[ ]modelc_3__3566_24.min1.thm1.tptp2017-02-06 16:57 298  
[ ]modelc_3__3605_22.min1.thm1.tptp2017-02-06 16:57 326  
[ ]modelc_3__3778_31.min1.thm1.tptp2017-02-06 16:57 342  
[ ]modelc_3__3848_31.min1.thm1.tptp2017-02-06 16:57 342  
[ ]modelc_3__3876_31.min1.thm1.tptp2017-02-06 16:57 342  
[ ]modelc_3__3905_25.min1.thm1.tptp2017-02-06 16:57 334  
[ ]modelc_3__3989_32.min1.thm1.tptp2017-02-06 16:57 371  
[ ]modelc_3__4000_27.min1.thm1.tptp2017-02-06 16:57 421  
[ ]modelc_3__4024_32.min1.thm1.tptp2017-02-06 16:57 371  
[ ]modelc_3__5190_37.min1.thm1.tptp2017-02-06 16:57 554  
[ ]modelc_3__5700_19.min1.thm1.tptp2017-02-06 16:57 308  
[ ]modelc_3__6003_34.min1.thm1.tptp2017-02-06 16:57 332  
[ ]modelc_3__6623_14.min1.thm1.tptp2017-02-06 16:57 430  
[ ]modelc_3__6855_34.min1.thm1.tptp2017-02-06 16:57 423  
[ ]monoid_0__204_39.min1.thm1.tptp2017-02-06 16:57 293  
[ ]msafree2__750_34.min1.thm1.tptp2017-02-06 16:57 516  
[ ]msafree2__806_32.min1.thm1.tptp2017-02-06 16:57 653  
[ ]msafree3__133_37.min1.thm1.tptp2017-02-06 16:57 293  
[ ]msafree3__820_39.min1.thm1.tptp2017-02-06 16:57 303  
[ ]msafree3__1350_39.min1.thm1.tptp2017-02-06 16:57 315  
[ ]msafree3__1369_27.min1.thm1.tptp2017-02-06 16:57 312  
[ ]msafree3__1590_37.min1.thm1.tptp2017-02-06 16:57 301  
[ ]msafree__274_17.min1.thm1.tptp2017-02-06 16:57 302  
[ ]msalimit__1048_21.min1.thm1.tptp2017-02-06 16:57 446  
[ ]msaterm__1110_18.min1.thm1.tptp2017-02-06 16:57 343  
[ ]msscyc_1__1041_39.min1.thm1.tptp2017-02-06 16:57 277  
[ ]msscyc_1__1513_36.min1.thm1.tptp2017-02-06 16:57 462  
[ ]mssublat__113_37.min1.thm1.tptp2017-02-06 16:57 279  
[ ]mssublat__510_21.min1.thm1.tptp2017-02-06 16:57 300  
[ ]mssublat__587_18.min1.thm1.tptp2017-02-06 16:57 290  
[ ]mssublat__1374_19.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_1__299_37.min1.thm1.tptp2017-02-06 16:57 280  
[ ]msualg_2__326_23.min1.thm1.tptp2017-02-06 16:57 370  
[ ]msualg_6__886_17.min1.thm1.tptp2017-02-06 16:57 258  
[ ]msualg_6__1093_19.min1.thm1.tptp2017-02-06 16:57 306  
[ ]msualg_7__1035_29.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_9__210_12.min1.thm1.tptp2017-02-06 16:57 270  
[ ]msualg_9__786_15.min1.thm1.tptp2017-02-06 16:57 430  
[ ]msualg_9__787_25.min1.thm1.tptp2017-02-06 16:57 430  
[ ]msuhom_1__347_19.min1.thm1.tptp2017-02-06 16:57 284  
[ ]msuhom_1__477_26.min1.thm1.tptp2017-02-06 16:57 285  
[ ]msuhom_1__765_17.min1.thm1.tptp2017-02-06 16:57 268  
[ ]msuhom_1__775_17.min1.thm1.tptp2017-02-06 16:57 268  
[ ]mycielsk__1439_38.min1.thm1.tptp2017-02-06 16:57 377  
[ ]mycielsk__1449_29.min1.thm1.tptp2017-02-06 16:57 313  
[ ]mycielsk__1526_28.min1.thm1.tptp2017-02-06 16:57 386  
[ ]mycielsk__1533_28.min1.thm1.tptp2017-02-06 16:57 386  
[ ]mycielsk__1882_22.min1.thm1.tptp2017-02-06 16:57 348  
[ ]mycielsk__1897_22.min1.thm1.tptp2017-02-06 16:57 348  
[ ]mycielsk__2055_18.min1.thm1.tptp2017-02-06 16:57 324  
[ ]mycielsk__2066_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]mycielsk__2145_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]mycielsk__2218_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]mycielsk__2429_46.min1.thm1.tptp2017-02-06 16:57 549  
[ ]mycielsk__2649_28.min1.thm1.tptp2017-02-06 16:57 354  
[ ]mycielsk__2708_36.min1.thm1.tptp2017-02-06 16:57 348  
[ ]mycielsk__2781_26.min1.thm1.tptp2017-02-06 16:57 354  
[ ]mycielsk__2801_25.min1.thm1.tptp2017-02-06 16:57 354  
[ ]mycielsk__2821_40.min1.thm1.tptp2017-02-06 16:57 514  
[ ]mycielsk__2923_33.min1.thm1.tptp2017-02-06 16:57 354  
[ ]mycielsk__2937_30.min1.thm1.tptp2017-02-06 16:57 450  
[ ]nat_1__1700_26.min1.thm1.tptp2017-02-06 16:57 306  
[ ]nat_3__212_19.min1.thm1.tptp2017-02-06 16:57 272  
[ ]nat_3__1761_15.min1.thm1.tptp2017-02-06 16:57 252  
[ ]nat_4__2416_16.min1.thm1.tptp2017-02-06 16:57 287  
[ ]nat_4__2437_18.min1.thm1.tptp2017-02-06 16:57 303  
[ ]nat_4__2441_17.min1.thm1.tptp2017-02-06 16:57 300  
[ ]nat_4__2552_19.min1.thm1.tptp2017-02-06 16:57 284  
[ ]nat_4__2621_20.min1.thm1.tptp2017-02-06 16:57 402  
[ ]nat_4__2625_22.min1.thm1.tptp2017-02-06 16:57 291  
[ ]nat_4__2631_26.min1.thm1.tptp2017-02-06 16:57 288  
[ ]nat_4__2643_15.min1.thm1.tptp2017-02-06 16:57 283  
[ ]nat_4__4543_67.min1.thm1.tptp2017-02-06 16:57 498  
[ ]nat_5__1762_13.min1.thm1.tptp2017-02-06 16:57 252  
[ ]nat_5__1882_19.min1.thm1.tptp2017-02-06 16:57 304  
[ ]nat_5__1964_18.min1.thm1.tptp2017-02-06 16:57 304  
[ ]nattra_1__281_34.min1.thm1.tptp2017-02-06 16:57 696  
[ ]ncfcont1__3033_11.min1.thm1.tptp2017-02-06 16:57 273  
[ ]ncfcont1__3088_11.min1.thm1.tptp2017-02-06 16:57 273  
[ ]ncfcont1__3143_11.min1.thm1.tptp2017-02-06 16:57 273  
[ ]ndiff_1__271_19.min1.thm1.tptp2017-02-06 16:57 347  
[ ]ndiff_1__281_26.min1.thm1.tptp2017-02-06 16:57 295  
[ ]ndiff_1__1907_22.min1.thm1.tptp2017-02-06 16:57 384  
[ ]ndiff_1__2836_23.min1.thm1.tptp2017-02-06 16:57 288  
[ ]ndiff_1__2841_13.min1.thm1.tptp2017-02-06 16:57 280  
[ ]ndiff_2__485_18.min1.thm1.tptp2017-02-06 16:57 274  
[ ]ndiff_2__496_24.min1.thm1.tptp2017-02-06 16:57 274  
[ ]ndiff_3__655_22.min1.thm1.tptp2017-02-06 16:57 384  
[ ]ndiff_3__745_20.min1.thm1.tptp2017-02-06 16:57 315  
[ ]ndiff_3__1370_28.min1.thm1.tptp2017-02-06 16:57 288  
[ ]ndiff_3__1374_15.min1.thm1.tptp2017-02-06 16:57 280  
[ ]neckla_2__551_35.min1.thm1.tptp2017-02-06 16:57 356  
[ ]neckla_3__1711_30.min1.thm1.tptp2017-02-06 16:57 314  
[ ]neckla_3__2582_14.min1.thm1.tptp2017-02-06 16:57 332  
[ ]neckla_3__2585_19.min1.thm1.tptp2017-02-06 16:57 342  
[ ]neckla_3__4377_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]neckla_3__4384_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]neckla_3__4400_13.min1.thm1.tptp2017-02-06 16:57 275  
[ ]neckla_3__4434_13.min1.thm1.tptp2017-02-06 16:57 275  
[ ]necklace__272_17.min1.thm1.tptp2017-02-06 16:57 276  
[ ]necklace__274_15.min1.thm1.tptp2017-02-06 16:57 278  
[ ]necklace__285_16.min1.thm1.tptp2017-02-06 16:57 272  
[ ]necklace__287_13.min1.thm1.tptp2017-02-06 16:57 274  
[ ]net_1__399_52.min1.thm1.tptp2017-02-06 16:57 318  
[ ]net_1__451_52.min1.thm1.tptp2017-02-06 16:57 318  
[ ]newton__698_20.min1.thm1.tptp2017-02-06 16:57 340  
[ ]newton__705_30.min1.thm1.tptp2017-02-06 16:57 341  
[ ]newton__809_16.min1.thm1.tptp2017-02-06 16:57 262  
[ ]newton__891_20.min1.thm1.tptp2017-02-06 16:57 346  
[ ]newton__1836_17.min1.thm1.tptp2017-02-06 16:57 266  
[ ]newton__1899_26.min1.thm1.tptp2017-02-06 16:57 310  
[ ]nfcont_1__1113_11.min1.thm1.tptp2017-02-06 16:57 273  
[ ]nfcont_3__562_22.min1.thm1.tptp2017-02-06 16:57 398  
[ ]nfcont_3__939_13.min1.thm1.tptp2017-02-06 16:57 316  
[ ]numbers__108_14.min1.thm1.tptp2017-02-06 16:57 280  
[ ]numbers__110_19.min1.thm1.tptp2017-02-06 16:57 308  
[ ]numbers__133_34.min1.thm1.tptp2017-02-06 16:57 384  
[ ]numbers__796_25.min1.thm1.tptp2017-02-06 16:57 261  
[ ]orders_1__107_15.min1.thm1.tptp2017-02-06 16:57 302  
[ ]orders_1__1576_20.min1.thm1.tptp2017-02-06 16:57 273  
[ ]orders_1__1660_29.min1.thm1.tptp2017-02-06 16:57 377  
[ ]orders_1__1696_29.min1.thm1.tptp2017-02-06 16:57 377  
[ ]orders_1__2914_16.min1.thm1.tptp2017-02-06 16:57 522  
[ ]orders_3__289_56.min1.thm1.tptp2017-02-06 16:57 488  
[ ]orders_3__532_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]orders_3__540_32.min1.thm1.tptp2017-02-06 16:57 304  
[ ]orders_4__726_16.min1.thm1.tptp2017-02-06 16:57 306  
[ ]ordinal1__87_19.min1.thm1.tptp2017-02-06 16:57 373  
[ ]ordinal1__90_30.min1.thm1.tptp2017-02-06 16:57 360  
[ ]ordinal1__478_37.min1.thm1.tptp2017-02-06 16:57 316  
[ ]ordinal1__759_44.min1.thm1.tptp2017-02-06 16:57 324  
[ ]ordinal1__1512_19.min1.thm1.tptp2017-02-06 16:57 273  
[ ]ordinal2__403_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]ordinal2__2169_21.min1.thm1.tptp2017-02-06 16:57 266  
[ ]ordinal5__236_12.min1.thm1.tptp2017-02-06 16:57 286  
[ ]ordinal5__535_27.min1.thm1.tptp2017-02-06 16:57 266  
[ ]ordinal5__1078_25.min1.thm1.tptp2017-02-06 16:57 308  
[ ]ordinal6__1951_20.min1.thm1.tptp2017-02-06 16:57 386  
[ ]ordinal6__2687_21.min1.thm1.tptp2017-02-06 16:57 284  
[ ]osafree__1403_26.min1.thm1.tptp2017-02-06 16:57 293  
[ ]osalg_4__804_17.min1.thm1.tptp2017-02-06 16:57 289  
[ ]partfun1__448_17.min1.thm1.tptp2017-02-06 16:57 476  
[ ]partfun1__1046_17.min1.thm1.tptp2017-02-06 16:57 337  
[ ]partfun1__1063_17.min1.thm1.tptp2017-02-06 16:57 337  
[ ]partfun1__1478_19.min1.thm1.tptp2017-02-06 16:57 389  
[ ]partfun1__1481_25.min1.thm1.tptp2017-02-06 16:57 360  
[ ]partfun2__1042_21.min1.thm1.tptp2017-02-06 16:57 290  
[ ]partfun2__1054_15.min1.thm1.tptp2017-02-06 16:57 292  
[ ]partfun2__1066_17.min1.thm1.tptp2017-02-06 16:57 448  
[ ]partfun3__95_19.min1.thm1.tptp2017-02-06 16:57 326  
[ ]partit1__230_15.min1.thm1.tptp2017-02-06 16:57 272  
[ ]partit1__248_9.min1.thm1.tptp2017-02-06 16:57 272  
[ ]partit1__649_19.min1.thm1.tptp2017-02-06 16:57 320  
[ ]partit1__798_23.min1.thm1.tptp2017-02-06 16:57 271  
[ ]partit1__826_23.min1.thm1.tptp2017-02-06 16:57 271  
[ ]partit1__1980_17.min1.thm1.tptp2017-02-06 16:57 288  
[ ]partit_2__69_14.min1.thm1.tptp2017-02-06 16:57 276  
[ ]partit_2__80_20.min1.thm1.tptp2017-02-06 16:57 272  
[ ]partit_2__711_23.min1.thm1.tptp2017-02-06 16:57 290  
[ ]pboole__53_28.min1.thm1.tptp2017-02-06 16:57 274  
[ ]pboole__59_15.min1.thm1.tptp2017-02-06 16:57 266  
[ ]pcomps_2__1458_54.min1.thm1.tptp2017-02-06 16:57 432  
[ ]pcs_0__2990_19.min1.thm1.tptp2017-02-06 16:57 282  
[ ]pcs_0__3060_19.min1.thm1.tptp2017-02-06 16:57 282  
[ ]pencil_1__146_11.min1.thm1.tptp2017-02-06 16:57 299  
[ ]pencil_1__2390_27.min1.thm1.tptp2017-02-06 16:57 418  
[ ]pencil_3__256_28.min1.thm1.tptp2017-02-06 16:57 408  
[ ]pencil_3__326_29.min1.thm1.tptp2017-02-06 16:57 408  
[ ]pencil_3__363_34.min1.thm1.tptp2017-02-06 16:57 476  
[ ]pencil_3__689_23.min1.thm1.tptp2017-02-06 16:57 394  
[ ]pencil_3__773_23.min1.thm1.tptp2017-02-06 16:57 580  
[ ]pencil_3__1420_39.min1.thm1.tptp2017-02-06 16:57 554  
[ ]pencil_3__1584_23.min1.thm1.tptp2017-02-06 16:57 438  
[ ]pencil_3__1595_19.min1.thm1.tptp2017-02-06 16:57 406  
[ ]pencil_3__2151_30.min1.thm1.tptp2017-02-06 16:57 438  
[ ]pencil_3__2223_30.min1.thm1.tptp2017-02-06 16:57 438  
[ ]pencil_3__2386_34.min1.thm1.tptp2017-02-06 16:57 564  
[ ]pencil_3__2399_20.min1.thm1.tptp2017-02-06 16:57 480  
[ ]pencil_3__2423_27.min1.thm1.tptp2017-02-06 16:57 402  
[ ]pencil_4__1255_17.min1.thm1.tptp2017-02-06 16:57 279  
[ ]pnproc_1__141_15.min1.thm1.tptp2017-02-06 16:57 292  
[ ]pnproc_1__948_18.min1.thm1.tptp2017-02-06 16:57 337  
[ ]pnproc_1__1551_20.min1.thm1.tptp2017-02-06 16:57 396  
[ ]pnproc_1__1552_20.min1.thm1.tptp2017-02-06 16:57 396  
[ ]polyalg1__63_39.min1.thm1.tptp2017-02-06 16:57 286  
[ ]polyalg1__87_39.min1.thm1.tptp2017-02-06 16:57 286  
[ ]polyalg1__889_39.min1.thm1.tptp2017-02-06 16:57 287  
[ ]polyform__2318_13.min1.thm1.tptp2017-02-06 16:57 270  
[ ]polyform__2584_22.min1.thm1.tptp2017-02-06 16:57 704  
[ ]polynom1__112_12.min1.thm1.tptp2017-02-06 16:57 254  
[ ]polynom1__288_12.min1.thm1.tptp2017-02-06 16:57 258  
[ ]polynom1__308_12.min1.thm1.tptp2017-02-06 16:57 258  
[ ]polynom2__749_34.min1.thm1.tptp2017-02-06 16:57 494  
[ ]polynom2__839_29.min1.thm1.tptp2017-02-06 16:57 437  
[ ]polynom2__946_29.min1.thm1.tptp2017-02-06 16:57 495  
[ ]polynom2__1156_30.min1.thm1.tptp2017-02-06 16:57 499  
[ ]polynom2__1538_21.min1.thm1.tptp2017-02-06 16:57 328  
[ ]polynom2__1548_18.min1.thm1.tptp2017-02-06 16:57 415  
[ ]polynom2__1601_55.min1.thm1.tptp2017-02-06 16:57 436  
[ ]polynom2__1936_26.min1.thm1.tptp2017-02-06 16:57 306  
[ ]polynom2__2057_22.min1.thm1.tptp2017-02-06 16:57 333  
[ ]polynom2__2074_22.min1.thm1.tptp2017-02-06 16:57 332  
[ ]polynom2__2135_25.min1.thm1.tptp2017-02-06 16:57 766  
[ ]polynom2__2140_29.min1.thm1.tptp2017-02-06 16:57 769  
[ ]polynom2__2163_29.min1.thm1.tptp2017-02-06 16:57 769  
[ ]polynom2__2191_29.min1.thm1.tptp2017-02-06 16:57 765  
[ ]polynom2__2196_21.min1.thm1.tptp2017-02-06 16:57 758  
[ ]polynom2__2208_20.min1.thm1.tptp2017-02-06 16:57 758  
[ ]polynom2__2225_20.min1.thm1.tptp2017-02-06 16:57 766  
[ ]polynom2__2237_24.min1.thm1.tptp2017-02-06 16:57 769  
[ ]polynom2__2465_18.min1.thm1.tptp2017-02-06 16:57 444  
[ ]polynom2__2498_55.min1.thm1.tptp2017-02-06 16:57 465  
[ ]polynom2__2573_21.min1.thm1.tptp2017-02-06 16:57 306  
[ ]polynom2__2597_29.min1.thm1.tptp2017-02-06 16:57 472  
[ ]polynom2__2636_29.min1.thm1.tptp2017-02-06 16:57 482  
[ ]polynom2__2648_57.min1.thm1.tptp2017-02-06 16:57 465  
[ ]polynom2__3004_19.min1.thm1.tptp2017-02-06 16:57 388  
[ ]polynom2__3051_30.min1.thm1.tptp2017-02-06 16:57 334  
[ ]polynom2__3328_25.min1.thm1.tptp2017-02-06 16:57 294  
[ ]polynom2__3334_27.min1.thm1.tptp2017-02-06 16:57 293  
[ ]polynom2__3353_25.min1.thm1.tptp2017-02-06 16:57 298  
[ ]polynom2__3358_29.min1.thm1.tptp2017-02-06 16:57 301  
[ ]polynom2__3382_29.min1.thm1.tptp2017-02-06 16:57 309  
[ ]polynom2__3411_29.min1.thm1.tptp2017-02-06 16:57 297  
[ ]polynom2__3427_20.min1.thm1.tptp2017-02-06 16:57 290  
[ ]polynom2__3447_20.min1.thm1.tptp2017-02-06 16:57 298  
[ ]polynom2__3459_24.min1.thm1.tptp2017-02-06 16:57 301  
[ ]polynom2__3681_73.min1.thm1.tptp2017-02-06 16:57 654  
[ ]polynom2__3744_25.min1.thm1.tptp2017-02-06 16:57 294  
[ ]polynom2__3750_27.min1.thm1.tptp2017-02-06 16:57 293  
[ ]polynom2__3769_25.min1.thm1.tptp2017-02-06 16:57 298  
[ ]polynom2__3774_29.min1.thm1.tptp2017-02-06 16:57 301  
[ ]polynom2__3798_29.min1.thm1.tptp2017-02-06 16:57 309  
[ ]polynom2__3827_29.min1.thm1.tptp2017-02-06 16:57 297  
[ ]polynom2__3843_20.min1.thm1.tptp2017-02-06 16:57 290  
[ ]polynom2__3863_20.min1.thm1.tptp2017-02-06 16:57 298  
[ ]polynom2__3875_24.min1.thm1.tptp2017-02-06 16:57 301  
[ ]polynom2__3969_25.min1.thm1.tptp2017-02-06 16:57 294  
[ ]polynom2__3975_27.min1.thm1.tptp2017-02-06 16:57 293  
[ ]polynom2__3994_25.min1.thm1.tptp2017-02-06 16:57 298  
[ ]polynom2__3999_29.min1.thm1.tptp2017-02-06 16:57 301  
[ ]polynom2__4023_29.min1.thm1.tptp2017-02-06 16:57 309  
[ ]polynom2__4052_29.min1.thm1.tptp2017-02-06 16:57 297  
[ ]polynom2__4068_20.min1.thm1.tptp2017-02-06 16:57 290  
[ ]polynom2__4088_20.min1.thm1.tptp2017-02-06 16:57 298  
[ ]polynom2__4100_24.min1.thm1.tptp2017-02-06 16:57 301  
[ ]polynom3__143_27.min1.thm1.tptp2017-02-06 16:57 342  
[ ]polynom3__701_16.min1.thm1.tptp2017-02-06 16:57 326  
[ ]polynom3__791_20.min1.thm1.tptp2017-02-06 16:57 446  
[ ]polynom3__893_16.min1.thm1.tptp2017-02-06 16:57 326  
[ ]polynom7__432_21.min1.thm1.tptp2017-02-06 16:57 444  
[ ]polynom7__760_16.min1.thm1.tptp2017-02-06 16:57 318  
[ ]polynom7__807_23.min1.thm1.tptp2017-02-06 16:57 314  
[ ]polynom7__896_69.min1.thm1.tptp2017-02-06 16:57 458  
[ ]polynom7__1172_22.min1.thm1.tptp2017-02-06 16:57 404  
[ ]polynom7__1201_14.min1.thm1.tptp2017-02-06 16:57 302  
[ ]polynom7__1275_21.min1.thm1.tptp2017-02-06 16:57 302  
[ ]polynom7__1284_20.min1.thm1.tptp2017-02-06 16:57 468  
[ ]polyred__204_23.min1.thm1.tptp2017-02-06 16:57 302  
[ ]polyred__290_14.min1.thm1.tptp2017-02-06 16:57 270  
[ ]polyred__2223_70.min1.thm1.tptp2017-02-06 16:57 554  
[ ]polyred__2232_70.min1.thm1.tptp2017-02-06 16:57 554  
[ ]polyred__2449_31.min1.thm1.tptp2017-02-06 16:57 516  
[ ]polyred__3034_16.min1.thm1.tptp2017-02-06 16:57 582  
[ ]polyred__3038_35.min1.thm1.tptp2017-02-06 16:57 429  
[ ]polyred__3147_29.min1.thm1.tptp2017-02-06 16:57 351  
[ ]polyred__3184_29.min1.thm1.tptp2017-02-06 16:57 355  
[ ]polyred__3200_29.min1.thm1.tptp2017-02-06 16:57 355  
[ ]polyred__3308_29.min1.thm1.tptp2017-02-06 16:57 349  
[ ]polyred__3453_29.min1.thm1.tptp2017-02-06 16:57 357  
[ ]polyred__3506_29.min1.thm1.tptp2017-02-06 16:57 351  
[ ]polyred__3795_31.min1.thm1.tptp2017-02-06 16:57 365  
[ ]polyred__3895_28.min1.thm1.tptp2017-02-06 16:57 399  
[ ]polyred__4439_33.min1.thm1.tptp2017-02-06 16:57 371  
[ ]polyred__4461_28.min1.thm1.tptp2017-02-06 16:57 371  
[ ]pralg_1__794_45.min1.thm1.tptp2017-02-06 16:57 290  
[ ]pralg_1__852_40.min1.thm1.tptp2017-02-06 16:57 368  
[ ]pralg_1__857_24.min1.thm1.tptp2017-02-06 16:57 322  
[ ]pralg_2__160_21.min1.thm1.tptp2017-02-06 16:57 270  
[ ]pralg_2__165_13.min1.thm1.tptp2017-02-06 16:57 262  
[ ]pralg_2__166_18.min1.thm1.tptp2017-02-06 16:57 282  
[ ]pralg_2__174_18.min1.thm1.tptp2017-02-06 16:57 262  
[ ]pralg_3__215_29.min1.thm1.tptp2017-02-06 16:57 472  
[ ]pralg_3__278_33.min1.thm1.tptp2017-02-06 16:57 594  
[ ]pre_circ__216_21.min1.thm1.tptp2017-02-06 16:57 286  
[ ]pre_circ__416_24.min1.thm1.tptp2017-02-06 16:57 358  
[ ]pre_circ__428_37.min1.thm1.tptp2017-02-06 16:57 526  
[ ]pre_poly__744_21.min1.thm1.tptp2017-02-06 16:57 309  
[ ]pre_poly__2522_24.min1.thm1.tptp2017-02-06 16:57 360  
[ ]pre_poly__2967_20.min1.thm1.tptp2017-02-06 16:57 278  
[ ]prelamb__579_21.min1.thm1.tptp2017-02-06 16:57 282  
[ ]prelamb__584_21.min1.thm1.tptp2017-02-06 16:57 482  
[ ]pua2mss1__811_19.min1.thm1.tptp2017-02-06 16:57 278  
[ ]pythtrip__582_26.min1.thm1.tptp2017-02-06 16:57 373  
[ ]pzfmisc1__232_23.min1.thm1.tptp2017-02-06 16:57 409  
[ ]pzfmisc1__331_22.min1.thm1.tptp2017-02-06 16:57 394  
[ ]qc_lang1__247_25.min1.thm1.tptp2017-02-06 16:57 360  
[ ]qc_lang1__258_17.min1.thm1.tptp2017-02-06 16:57 352  
[ ]qc_lang1__298_25.min1.thm1.tptp2017-02-06 16:57 360  
[ ]qc_lang1__309_17.min1.thm1.tptp2017-02-06 16:57 352  
[ ]qc_lang2__1401_22.min1.thm1.tptp2017-02-06 16:57 298  
[ ]qc_lang2__1420_17.min1.thm1.tptp2017-02-06 16:57 362  
[ ]qc_lang2__1479_23.min1.thm1.tptp2017-02-06 16:57 334  
[ ]qc_lang2__1510_23.min1.thm1.tptp2017-02-06 16:57 366  
[ ]qc_lang2__1574_24.min1.thm1.tptp2017-02-06 16:57 366  
[ ]qc_lang3__960_13.min1.thm1.tptp2017-02-06 16:57 250  
[ ]qc_lang3__961_11.min1.thm1.tptp2017-02-06 16:57 251  
[ ]qc_lang3__979_13.min1.thm1.tptp2017-02-06 16:57 250  
[ ]qc_lang3__980_11.min1.thm1.tptp2017-02-06 16:57 251  
[ ]qc_lang3__998_13.min1.thm1.tptp2017-02-06 16:57 250  
[ ]qc_lang3__999_11.min1.thm1.tptp2017-02-06 16:57 251  
[ ]quaterni__441_14.min1.thm1.tptp2017-02-06 16:57 292  
[ ]quaterni__442_14.min1.thm1.tptp2017-02-06 16:57 324  
[ ]quaterni__709_30.min1.thm1.tptp2017-02-06 16:57 362  
[ ]radix_1__204_15.min1.thm1.tptp2017-02-06 16:57 289  
[ ]radix_2__135_17.min1.thm1.tptp2017-02-06 16:57 296  
[ ]radix_2__493_18.min1.thm1.tptp2017-02-06 16:57 299  
[ ]radix_2__919_17.min1.thm1.tptp2017-02-06 16:57 300  
[ ]radix_2__1343_18.min1.thm1.tptp2017-02-06 16:57 300  
[ ]radix_2__1595_18.min1.thm1.tptp2017-02-06 16:57 299  
[ ]ramsey_1__1096_12.min1.thm1.tptp2017-02-06 16:57 276  
[ ]ramsey_1__1564_45.min1.thm1.tptp2017-02-06 16:57 368  
[ ]ramsey_1__1642_45.min1.thm1.tptp2017-02-06 16:57 368  
[ ]ramsey_1__1723_22.min1.thm1.tptp2017-02-06 16:57 330  
[ ]ramsey_1__1741_22.min1.thm1.tptp2017-02-06 16:57 330  
[ ]ramsey_1__1755_21.min1.thm1.tptp2017-02-06 16:57 317  
[ ]random_1__602_29.min1.thm1.tptp2017-02-06 16:57 480  
[ ]random_1__774_29.min1.thm1.tptp2017-02-06 16:57 486  
[ ]random_1__993_19.min1.thm1.tptp2017-02-06 16:57 530  
[ ]random_1__1006_19.min1.thm1.tptp2017-02-06 16:57 530  
[ ]random_1__1040_18.min1.thm1.tptp2017-02-06 16:57 394  
[ ]random_1__1075_18.min1.thm1.tptp2017-02-06 16:57 394  
[ ]random_2__929_21.min1.thm1.tptp2017-02-06 16:57 320  
[ ]random_2__2073_50.min1.thm1.tptp2017-02-06 16:57 436  
[ ]random_2__2189_53.min1.thm1.tptp2017-02-06 16:57 357  
[ ]rat_1__229_13.min1.thm1.tptp2017-02-06 16:57 261  
[ ]ratfunc1__1805_28.min1.thm1.tptp2017-02-06 16:57 492  
[ ]ratfunc1__2677_20.min1.thm1.tptp2017-02-06 16:57 286  
[ ]ratfunc1__2700_20.min1.thm1.tptp2017-02-06 16:57 286  
[ ]rcomp_3__924_15.min1.thm1.tptp2017-02-06 16:57 304  
[ ]rcomp_3__2106_18.min1.thm1.tptp2017-02-06 16:57 330  
[ ]realset1__125_19.min1.thm1.tptp2017-02-06 16:57 279  
[ ]rearran1__1319_40.min1.thm1.tptp2017-02-06 16:57 418  
[ ]rearran1__1380_25.min1.thm1.tptp2017-02-06 16:57 390  
[ ]rearran1__1561_25.min1.thm1.tptp2017-02-06 16:57 390  
[ ]rearran1__2082_40.min1.thm1.tptp2017-02-06 16:57 420  
[ ]rearran1__2143_25.min1.thm1.tptp2017-02-06 16:57 392  
[ ]rearran1__2324_25.min1.thm1.tptp2017-02-06 16:57 392  
[ ]rearran1__2649_19.min1.thm1.tptp2017-02-06 16:57 338  
[ ]rearran1__2909_19.min1.thm1.tptp2017-02-06 16:57 396  
[ ]relat_1__264_21.min1.thm1.tptp2017-02-06 16:57 276  
[ ]relat_1__267_15.min1.thm1.tptp2017-02-06 16:57 272  
[ ]relat_1__281_21.min1.thm1.tptp2017-02-06 16:57 276  
[ ]relat_1__284_17.min1.thm1.tptp2017-02-06 16:57 272  
[ ]relat_1__2521_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]relset_1__779_12.min1.thm1.tptp2017-02-06 16:57 290  
[ ]relset_2__491_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]relset_2__713_21.min1.thm1.tptp2017-02-06 16:57 314  
[ ]relset_2__1228_21.min1.thm1.tptp2017-02-06 16:57 294  
[ ]relset_2__1473_12.min1.thm1.tptp2017-02-06 16:57 282  
[ ]rewrite1__2417_14.min1.thm1.tptp2017-02-06 16:57 308  
[ ]rewrite1__2426_19.min1.thm1.tptp2017-02-06 16:57 308  
[ ]rfinseq__214_23.min1.thm1.tptp2017-02-06 16:57 328  
[ ]rfinseq__228_23.min1.thm1.tptp2017-02-06 16:57 282  
[ ]rfinseq__244_26.min1.thm1.tptp2017-02-06 16:57 532  
[ ]rfinseq__246_23.min1.thm1.tptp2017-02-06 16:57 352  
[ ]rfinseq__255_26.min1.thm1.tptp2017-02-06 16:57 528  
[ ]rfinseq__257_23.min1.thm1.tptp2017-02-06 16:57 398  
[ ]rfinseq__1721_21.min1.thm1.tptp2017-02-06 16:57 376  
[ ]rfinseq__1725_21.min1.thm1.tptp2017-02-06 16:57 378  
[ ]rfinseq__1735_21.min1.thm1.tptp2017-02-06 16:57 370  
[ ]rfinseq__1739_19.min1.thm1.tptp2017-02-06 16:57 369  
[ ]rfinseq__1758_24.min1.thm1.tptp2017-02-06 16:57 354  
[ ]rfunct_1__233_28.min1.thm1.tptp2017-02-06 16:57 387  
[ ]rfunct_1__237_27.min1.thm1.tptp2017-02-06 16:57 327  
[ ]rfunct_1__247_27.min1.thm1.tptp2017-02-06 16:57 329  
[ ]rfunct_1__264_16.min1.thm1.tptp2017-02-06 16:57 327  
[ ]rfunct_1__268_21.min1.thm1.tptp2017-02-06 16:57 327  
[ ]rfunct_1__271_34.min1.thm1.tptp2017-02-06 16:57 389  
[ ]rfunct_1__317_20.min1.thm1.tptp2017-02-06 16:57 374  
[ ]rfunct_1__332_28.min1.thm1.tptp2017-02-06 16:57 356  
[ ]rfunct_1__336_19.min1.thm1.tptp2017-02-06 16:57 328  
[ ]rfunct_1__344_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]rfunct_1__348_24.min1.thm1.tptp2017-02-06 16:57 352  
[ ]rfunct_1__361_24.min1.thm1.tptp2017-02-06 16:57 356  
[ ]rfunct_1__372_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]rfunct_1__407_27.min1.thm1.tptp2017-02-06 16:57 388  
[ ]rfunct_1__411_19.min1.thm1.tptp2017-02-06 16:57 328  
[ ]rfunct_1__418_19.min1.thm1.tptp2017-02-06 16:57 324  
[ ]rfunct_1__425_23.min1.thm1.tptp2017-02-06 16:57 384  
[ ]rfunct_2__1669_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]rfunct_2__1687_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]rfunct_2__1705_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]rfunct_2__1723_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]rfunct_3__202_21.min1.thm1.tptp2017-02-06 16:57 380  
[ ]rfunct_3__205_28.min1.thm1.tptp2017-02-06 16:57 432  
[ ]rfunct_3__214_23.min1.thm1.tptp2017-02-06 16:57 424  
[ ]rfunct_3__218_19.min1.thm1.tptp2017-02-06 16:57 373  
[ ]rfunct_3__243_26.min1.thm1.tptp2017-02-06 16:57 416  
[ ]rfunct_3__264_20.min1.thm1.tptp2017-02-06 16:57 358  
[ ]rfunct_3__296_30.min1.thm1.tptp2017-02-06 16:57 416  
[ ]rfunct_3__303_30.min1.thm1.tptp2017-02-06 16:57 416  
[ ]rfunct_3__323_24.min1.thm1.tptp2017-02-06 16:57 348  
[ ]rfunct_3__326_17.min1.thm1.tptp2017-02-06 16:57 320  
[ ]rfunct_3__335_17.min1.thm1.tptp2017-02-06 16:57 312  
[ ]rfunct_3__339_22.min1.thm1.tptp2017-02-06 16:57 394  
[ ]rfunct_3__357_22.min1.thm1.tptp2017-02-06 16:57 350  
[ ]rfunct_3__1496_14.min1.thm1.tptp2017-02-06 16:57 330  
[ ]rfunct_3__1500_30.min1.thm1.tptp2017-02-06 16:57 390  
[ ]rfunct_3__1509_21.min1.thm1.tptp2017-02-06 16:57 382  
[ ]rfunct_3__1514_20.min1.thm1.tptp2017-02-06 16:57 324  
[ ]rfunct_3__1548_21.min1.thm1.tptp2017-02-06 16:57 372  
[ ]rfunct_3__1592_15.min1.thm1.tptp2017-02-06 16:57 352  
[ ]rfunct_3__1596_30.min1.thm1.tptp2017-02-06 16:57 390  
[ ]rfunct_3__1605_21.min1.thm1.tptp2017-02-06 16:57 382  
[ ]rfunct_3__1644_21.min1.thm1.tptp2017-02-06 16:57 372  
[ ]rfunct_3__1995_21.min1.thm1.tptp2017-02-06 16:57 384  
[ ]rfunct_3__1999_21.min1.thm1.tptp2017-02-06 16:57 444  
[ ]rfunct_3__2011_21.min1.thm1.tptp2017-02-06 16:57 436  
[ ]rfunct_3__2655_23.min1.thm1.tptp2017-02-06 16:57 322  
[ ]rfunct_3__2669_23.min1.thm1.tptp2017-02-06 16:57 298  
[ ]rfunct_3__2685_26.min1.thm1.tptp2017-02-06 16:57 612  
[ ]rfunct_3__2687_23.min1.thm1.tptp2017-02-06 16:57 422  
[ ]rfunct_3__2696_26.min1.thm1.tptp2017-02-06 16:57 648  
[ ]rfunct_3__2698_23.min1.thm1.tptp2017-02-06 16:57 446  
[ ]rfunct_3__2822_21.min1.thm1.tptp2017-02-06 16:57 338  
[ ]rfunct_3__2825_22.min1.thm1.tptp2017-02-06 16:57 464  
[ ]rfunct_3__2827_17.min1.thm1.tptp2017-02-06 16:57 330  
[ ]rfunct_3__2979_17.min1.thm1.tptp2017-02-06 16:57 292  
[ ]rinfsup2__56_20.min1.thm1.tptp2017-02-06 16:57 261  
[ ]rinfsup2__82_20.min1.thm1.tptp2017-02-06 16:57 261  
[ ]rinfsup2__1594_17.min1.thm1.tptp2017-02-06 16:57 286  
[ ]rinfsup2__1619_28.min1.thm1.tptp2017-02-06 16:57 286  
[ ]rinfsup2__1638_29.min1.thm1.tptp2017-02-06 16:57 398  
[ ]rinfsup2__1684_19.min1.thm1.tptp2017-02-06 16:57 286  
[ ]rinfsup2__1709_28.min1.thm1.tptp2017-02-06 16:57 286  
[ ]rinfsup2__1728_29.min1.thm1.tptp2017-02-06 16:57 398  
[ ]ring_1__353_30.min1.thm1.tptp2017-02-06 16:57 286  
[ ]ringcat1__686_63.min1.thm1.tptp2017-02-06 16:57 389  
[ ]rlaffin2__296_17.min1.thm1.tptp2017-02-06 16:57 292  
[ ]rlaffin2__1146_14.min1.thm1.tptp2017-02-06 16:57 270  
[ ]rltopsp1__2553_17.min1.thm1.tptp2017-02-06 16:57 298  
[ ]rlvect_1__1204_19.min1.thm1.tptp2017-02-06 16:57 266  
[ ]rlvect_1__1535_21.min1.thm1.tptp2017-02-06 16:57 294  
[ ]rlvect_1__1888_20.min1.thm1.tptp2017-02-06 16:57 276  
[ ]rlvect_2__550_21.min1.thm1.tptp2017-02-06 16:57 288  
[ ]rlvect_2__1289_25.min1.thm1.tptp2017-02-06 16:57 538  
[ ]rlvect_5__1539_13.min1.thm1.tptp2017-02-06 16:57 282  
[ ]rmod_4__691_25.min1.thm1.tptp2017-02-06 16:57 436  
[ ]roughs_1__117_28.min1.thm1.tptp2017-02-06 16:57 306  
[ ]rusub_4__722_13.min1.thm1.tptp2017-02-06 16:57 276  
[ ]scm_halt__235_31.min1.thm1.tptp2017-02-06 16:57 333  
[ ]scm_halt__1626_33.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scm_halt__1714_34.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]scm_halt__3250_27.min1.thm1.tptp2017-02-06 16:57 368  
[ ]scm_inst__539_22.min1.thm1.tptp2017-02-06 16:57 271  
[ ]scm_inst__545_14.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa6b__94_30.min1.thm1.tptp2017-02-06 16:57 376  
[ ]scmfsa6b__269_36.min1.thm1.tptp2017-02-06 16:57 334  
[ ]scmfsa6b__1174_28.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmfsa6b__1423_52.min1.thm1.tptp2017-02-06 16:57 449  
[ ]scmfsa6b__1431_61.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]scmfsa6b__1597_33.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmfsa6c__185_28.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__217_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__250_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__282_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__314_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__347_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__381_30.min1.thm1.tptp2017-02-06 16:57 378  
[ ]scmfsa6c__410_30.min1.thm1.tptp2017-02-06 16:57 378  
[ ]scmfsa6c__460_28.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__494_30.min1.thm1.tptp2017-02-06 16:57 378  
[ ]scmfsa6c__523_30.min1.thm1.tptp2017-02-06 16:57 378  
[ ]scmfsa6c__573_28.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__617_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__662_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__707_29.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__756_28.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__804_28.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa6c__852_28.min1.thm1.tptp2017-02-06 16:57 374  
[ ]scmfsa8c__226_33.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmfsa9a__242_18.min1.thm1.tptp2017-02-06 16:57 303  
[ ]scmfsa9a__1397_18.min1.thm1.tptp2017-02-06 16:57 303  
[ ]scmfsa10__209_12.min1.thm1.tptp2017-02-06 16:57 260  
[ ]scmfsa10__228_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__233_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__254_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__259_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__280_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__285_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__306_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__311_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__332_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__337_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__466_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__471_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__492_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__497_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__518_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__523_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__544_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa10__549_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa10__561_50.min1.thm1.tptp2017-02-06 16:57 480  
[ ]scmfsa10__596_57.min1.thm1.tptp2017-02-06 16:57 512  
[ ]scmfsa10__631_57.min1.thm1.tptp2017-02-06 16:57 512  
[ ]scmfsa10__682_17.min1.thm1.tptp2017-02-06 16:57 297  
[ ]scmfsa10__829_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmfsa10__905_26.min1.thm1.tptp2017-02-06 16:57 353  
[ ]scmfsa10__926_26.min1.thm1.tptp2017-02-06 16:57 343  
[ ]scmfsa10__965_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmfsa10__1032_26.min1.thm1.tptp2017-02-06 16:57 343  
[ ]scmfsa10__1053_26.min1.thm1.tptp2017-02-06 16:57 353  
[ ]scmfsa10__1092_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmfsa10__1330_18.min1.thm1.tptp2017-02-06 16:57 286  
[ ]scmfsa10__1340_23.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmfsa10__1665_27.min1.thm1.tptp2017-02-06 16:57 370  
[ ]scmfsa_1__165_12.min1.thm1.tptp2017-02-06 16:57 276  
[ ]scmfsa_1__316_15.min1.thm1.tptp2017-02-06 16:57 276  
[ ]scmfsa_1__365_16.min1.thm1.tptp2017-02-06 16:57 276  
[ ]scmfsa_2__1056_28.min1.thm1.tptp2017-02-06 16:57 304  
[ ]scmfsa_3__58_31.min1.thm1.tptp2017-02-06 16:57 287  
[ ]scmfsa_3__75_31.min1.thm1.tptp2017-02-06 16:57 287  
[ ]scmfsa_3__211_49.min1.thm1.tptp2017-02-06 16:57 414  
[ ]scmfsa_3__226_37.min1.thm1.tptp2017-02-06 16:57 396  
[ ]scmfsa_3__254_49.min1.thm1.tptp2017-02-06 16:57 414  
[ ]scmfsa_3__270_26.min1.thm1.tptp2017-02-06 16:57 386  
[ ]scmfsa_3__323_49.min1.thm1.tptp2017-02-06 16:57 414  
[ ]scmfsa_3__343_35.min1.thm1.tptp2017-02-06 16:57 396  
[ ]scmfsa_3__425_49.min1.thm1.tptp2017-02-06 16:57 414  
[ ]scmfsa_3__440_26.min1.thm1.tptp2017-02-06 16:57 386  
[ ]scmfsa_i__536_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa_i__545_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmfsa_i__573_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmfsa_i__581_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmisort__108_26.min1.thm1.tptp2017-02-06 16:57 283  
[ ]scmisort__231_26.min1.thm1.tptp2017-02-06 16:57 283  
[ ]scmpds_2__880_27.min1.thm1.tptp2017-02-06 16:57 304  
[ ]scmpds_3__109_31.min1.thm1.tptp2017-02-06 16:57 287  
[ ]scmpds_3__166_46.min1.thm1.tptp2017-02-06 16:57 398  
[ ]scmpds_4__142_22.min1.thm1.tptp2017-02-06 16:57 300  
[ ]scmpds_4__207_30.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmpds_4__495_18.min1.thm1.tptp2017-02-06 16:57 354  
[ ]scmpds_5__621_18.min1.thm1.tptp2017-02-06 16:57 284  
[ ]scmpds_5__1796_32.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmpds_7__1189_32.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmpds_7__2853_21.min1.thm1.tptp2017-02-06 16:57 288  
[ ]scmpds_7__2858_41.min1.thm1.tptp2017-02-06 16:57 359  
[ ]scmpds_7__2889_38.min1.thm1.tptp2017-02-06 16:57 367  
[ ]scmpds_7__2915_23.min1.thm1.tptp2017-02-06 16:57 288  
[ ]scmpds_9__126_26.min1.thm1.tptp2017-02-06 16:57 298  
[ ]scmpds_9__135_17.min1.thm1.tptp2017-02-06 16:57 290  
[ ]scmpds_9__181_21.min1.thm1.tptp2017-02-06 16:57 348  
[ ]scmring3__90_29.min1.thm1.tptp2017-02-06 16:57 319  
[ ]scmring3__334_12.min1.thm1.tptp2017-02-06 16:57 260  
[ ]scmring3__353_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmring3__358_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmring3__379_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmring3__384_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmring3__405_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmring3__410_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmring3__431_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmring3__436_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmring3__457_22.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmring3__462_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]scmring3__546_53.min1.thm1.tptp2017-02-06 16:57 578  
[ ]scmring3__581_57.min1.thm1.tptp2017-02-06 16:57 610  
[ ]scmring3__797_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmring3__973_13.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmring3__1083_18.min1.thm1.tptp2017-02-06 16:57 286  
[ ]scmring3__1093_23.min1.thm1.tptp2017-02-06 16:57 312  
[ ]scmyciel__135_18.min1.thm1.tptp2017-02-06 16:57 286  
[ ]scmyciel__632_21.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmyciel__636_18.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmyciel__747_20.min1.thm1.tptp2017-02-06 16:57 270  
[ ]scmyciel__993_23.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmyciel__1000_16.min1.thm1.tptp2017-02-06 16:57 298  
[ ]scmyciel__1022_16.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmyciel__1102_21.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmyciel__1104_25.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmyciel__1115_26.min1.thm1.tptp2017-02-06 16:57 286  
[ ]scmyciel__1128_22.min1.thm1.tptp2017-02-06 16:57 278  
[ ]scmyciel__1308_18.min1.thm1.tptp2017-02-06 16:57 310  
[ ]scmyciel__2595_24.min1.thm1.tptp2017-02-06 16:57 282  
[ ]scmyciel__2766_38.min1.thm1.tptp2017-02-06 16:57 385  
[ ]scmyciel__2776_29.min1.thm1.tptp2017-02-06 16:57 319  
[ ]scmyciel__2853_28.min1.thm1.tptp2017-02-06 16:57 394  
[ ]scmyciel__2860_28.min1.thm1.tptp2017-02-06 16:57 394  
[ ]scmyciel__3559_21.min1.thm1.tptp2017-02-06 16:57 298  
[ ]scmyciel__3606_31.min1.thm1.tptp2017-02-06 16:57 416  
[ ]scmyciel__3619_21.min1.thm1.tptp2017-02-06 16:57 298  
[ ]scmyciel__3659_19.min1.thm1.tptp2017-02-06 16:57 274  
[ ]scmyciel__3716_18.min1.thm1.tptp2017-02-06 16:57 338  
[ ]scmyciel__3776_16.min1.thm1.tptp2017-02-06 16:57 306  
[ ]scmyciel__3806_17.min1.thm1.tptp2017-02-06 16:57 314  
[ ]scmyciel__3823_16.min1.thm1.tptp2017-02-06 16:57 322  
[ ]scmyciel__3827_18.min1.thm1.tptp2017-02-06 16:57 314  
[ ]scmyciel__3890_28.min1.thm1.tptp2017-02-06 16:57 336  
[ ]scmyciel__3953_15.min1.thm1.tptp2017-02-06 16:57 306  
[ ]scmyciel__3961_14.min1.thm1.tptp2017-02-06 16:57 306  
[ ]scmyciel__4484_20.min1.thm1.tptp2017-02-06 16:57 282  
[ ]scmyciel__4491_16.min1.thm1.tptp2017-02-06 16:57 304  
[ ]scmyciel__4568_21.min1.thm1.tptp2017-02-06 16:57 298  
[ ]scmyciel__4584_19.min1.thm1.tptp2017-02-06 16:57 282  
[ ]scmyciel__4768_21.min1.thm1.tptp2017-02-06 16:57 340  
[ ]scmyciel__4804_36.min1.thm1.tptp2017-02-06 16:57 476  
[ ]scmyciel__4809_21.min1.thm1.tptp2017-02-06 16:57 453  
[ ]scmyciel__4817_21.min1.thm1.tptp2017-02-06 16:57 453  
[ ]scmyciel__4840_28.min1.thm1.tptp2017-02-06 16:57 332  
[ ]scmyciel__5058_24.min1.thm1.tptp2017-02-06 16:57 344  
[ ]scmyciel__5114_23.min1.thm1.tptp2017-02-06 16:57 346  
[ ]scmyciel__5144_30.min1.thm1.tptp2017-02-06 16:57 330  
[ ]scmyciel__5209_29.min1.thm1.tptp2017-02-06 16:57 360  
[ ]scmyciel__5232_25.min1.thm1.tptp2017-02-06 16:57 336  
[ ]scmyciel__5291_28.min1.thm1.tptp2017-02-06 16:57 336  
[ ]scmyciel__5354_25.min1.thm1.tptp2017-02-06 16:57 340  
[ ]scmyciel__5368_24.min1.thm1.tptp2017-02-06 16:57 428  
[ ]scpisort__1566_42.min1.thm1.tptp2017-02-06 16:57 625  
[ ]scpqsort__290_44.min1.thm1.tptp2017-02-06 16:57 651  
[ ]scpqsort__327_9.min1.thm1.tptp2017-02-06 16:57 423  
[ ]scpqsort__329_16.min1.thm1.tptp2017-02-06 16:57 333  
[ ]seq_4__3208_15.min1.thm1.tptp2017-02-06 16:57 282  
[ ]setfam_1__203_42.min1.thm1.tptp2017-02-06 16:57 314  
[ ]setfam_1__334_17.min1.thm1.tptp2017-02-06 16:57 311  
[ ]setfam_1__677_13.min1.thm1.tptp2017-02-06 16:57 279  
[ ]setfam_1__766_13.min1.thm1.tptp2017-02-06 16:57 279  
[ ]setlim_1__83_23.min1.thm1.tptp2017-02-06 16:57 390  
[ ]setwiseo__498_24.min1.thm1.tptp2017-02-06 16:57 322  
[ ]setwiseo__1058_19.min1.thm1.tptp2017-02-06 16:57 398  
[ ]setwiseo__1135_25.min1.thm1.tptp2017-02-06 16:57 562  
[ ]setwiseo__1789_17.min1.thm1.tptp2017-02-06 16:57 482  
[ ]setwop_2__76_32.min1.thm1.tptp2017-02-06 16:57 321  
[ ]setwop_2__79_27.min1.thm1.tptp2017-02-06 16:57 395  
[ ]setwop_2__885_27.min1.thm1.tptp2017-02-06 16:57 294  
[ ]setwop_2__907_16.min1.thm1.tptp2017-02-06 16:57 290  
[ ]sf_mastr__2251_16.min1.thm1.tptp2017-02-06 16:57 317  
[ ]sf_mastr__2291_16.min1.thm1.tptp2017-02-06 16:57 318  
[ ]sf_mastr__2311_16.min1.thm1.tptp2017-02-06 16:57 316  
[ ]sfmastr1__977_31.min1.thm1.tptp2017-02-06 16:57 304  
[ ]sgraph1__73_26.min1.thm1.tptp2017-02-06 16:57 288  
[ ]sgraph1__115_26.min1.thm1.tptp2017-02-06 16:57 288  
[ ]sgraph1__401_11.min1.thm1.tptp2017-02-06 16:57 267  
[ ]sgraph1__418_12.min1.thm1.tptp2017-02-06 16:57 274  
[ ]sgraph1__419_13.min1.thm1.tptp2017-02-06 16:57 274  
[ ]sgraph1__717_20.min1.thm1.tptp2017-02-06 16:57 340  
[ ]sgraph1__1159_52.min1.thm1.tptp2017-02-06 16:57 312  
[ ]sgraph1__1166_23.min1.thm1.tptp2017-02-06 16:57 273  
[ ]simplex0__320_9.min1.thm1.tptp2017-02-06 16:57 278  
[ ]simplex0__1024_20.min1.thm1.tptp2017-02-06 16:57 358  
[ ]simplex1__2815_18.min1.thm1.tptp2017-02-06 16:57 290  
[ ]simplex1__3537_15.min1.thm1.tptp2017-02-06 16:57 440  
[ ]simplex1__4138_22.min1.thm1.tptp2017-02-06 16:57 324  
[ ]simplex1__4172_12.min1.thm1.tptp2017-02-06 16:57 332  
[ ]simplex1__4192_22.min1.thm1.tptp2017-02-06 16:57 418  
[ ]simplex1__4224_26.min1.thm1.tptp2017-02-06 16:57 400  
[ ]simplex1__4226_26.min1.thm1.tptp2017-02-06 16:57 400  
[ ]simplex1__4361_21.min1.thm1.tptp2017-02-06 16:57 334  
[ ]simplex2__836_8.min1.thm1.tptp2017-02-06 16:57 270  
[ ]sppol_2__1753_39.min1.thm1.tptp2017-02-06 16:57 544  
[ ]sppol_2__1845_35.min1.thm1.tptp2017-02-06 16:57 528  
[ ]sppol_2__2561_27.min1.thm1.tptp2017-02-06 16:57 400  
[ ]sppol_2__2837_18.min1.thm1.tptp2017-02-06 16:57 707  
[ ]sppol_2__2855_14.min1.thm1.tptp2017-02-06 16:57 707  
[ ]sppol_2__2950_32.min1.thm1.tptp2017-02-06 16:57 458  
[ ]sprect_2__2438_43.min1.thm1.tptp2017-02-06 16:57 765  
[ ]sprect_3__496_27.min1.thm1.tptp2017-02-06 16:57 356  
[ ]sprect_3__555_27.min1.thm1.tptp2017-02-06 16:57 388  
[ ]sprect_3__694_24.min1.thm1.tptp2017-02-06 16:57 406  
[ ]sprect_3__728_28.min1.thm1.tptp2017-02-06 16:57 438  
[ ]sprect_4__239_28.min1.thm1.tptp2017-02-06 16:57 430  
[ ]sprect_4__274_24.min1.thm1.tptp2017-02-06 16:57 398  
[ ]sprect_4__726_17.min1.thm1.tptp2017-02-06 16:57 342  
[ ]sprect_4__805_34.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]sprect_4__919_17.min1.thm1.tptp2017-02-06 16:57 342  
[ ]sprect_4__996_27.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]sprect_4__1543_64.min1.thm1.tptp2017-02-06 16:57 734  
[ ]sprect_4__1583_59.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]stirl2_1__845_13.min1.thm1.tptp2017-02-06 16:57 310  
[ ]stirl2_1__1235_18.min1.thm1.tptp2017-02-06 16:57 531  
[ ]stirl2_1__1567_25.min1.thm1.tptp2017-02-06 16:57 514  
[ ]stirl2_1__2986_26.min1.thm1.tptp2017-02-06 16:57 337  
[ ]stirl2_1__3143_17.min1.thm1.tptp2017-02-06 16:57 298  
[ ]stirl2_1__3194_20.min1.thm1.tptp2017-02-06 16:57 348  
[ ]stirl2_1__3537_24.min1.thm1.tptp2017-02-06 16:57 382  
[ ]stirl2_1__3547_17.min1.thm1.tptp2017-02-06 16:57 390  
[ ]stirl2_1__4276_18.min1.thm1.tptp2017-02-06 16:57 498  
[ ]subset_1__79_18.min1.thm1.tptp2017-02-06 16:57 327  
[ ]subset_1__1163_11.min1.thm1.tptp2017-02-06 16:57 270  
[ ]substlat__95_13.min1.thm1.tptp2017-02-06 16:57 266  
[ ]substlat__294_14.min1.thm1.tptp2017-02-06 16:57 270  
[ ]substlat__307_18.min1.thm1.tptp2017-02-06 16:57 273  
[ ]symsp_1__63_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]t_0topsp__625_14.min1.thm1.tptp2017-02-06 16:57 450  
[ ]t_0topsp__670_19.min1.thm1.tptp2017-02-06 16:57 708  
[ ]t_0topsp__730_19.min1.thm1.tptp2017-02-06 16:57 762  
[ ]taxonom1__318_12.min1.thm1.tptp2017-02-06 16:57 292  
[ ]taxonom1__760_14.min1.thm1.tptp2017-02-06 16:57 286  
[ ]taxonom1__773_23.min1.thm1.tptp2017-02-06 16:57 286  
[ ]taxonom2__350_11.min1.thm1.tptp2017-02-06 16:57 262  
[ ]taxonom2__380_11.min1.thm1.tptp2017-02-06 16:57 262  
[ ]taxonom2__393_20.min1.thm1.tptp2017-02-06 16:57 286  
[ ]taxonom2__423_10.min1.thm1.tptp2017-02-06 16:57 270  
[ ]taxonom2__488_25.min1.thm1.tptp2017-02-06 16:57 314  
[ ]taxonom2__495_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]taxonom2__689_23.min1.thm1.tptp2017-02-06 16:57 294  
[ ]taxonom2__696_16.min1.thm1.tptp2017-02-06 16:57 286  
[ ]taxonom2__706_18.min1.thm1.tptp2017-02-06 16:57 278  
[ ]taxonom2__991_25.min1.thm1.tptp2017-02-06 16:57 286  
[ ]taxonom2__1135_25.min1.thm1.tptp2017-02-06 16:57 286  
[ ]taxonom2__1323_27.min1.thm1.tptp2017-02-06 16:57 289  
[ ]taxonom2__1336_15.min1.thm1.tptp2017-02-06 16:57 281  
[ ]taxonom2__1432_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]taxonom2__1491_23.min1.thm1.tptp2017-02-06 16:57 302  
[ ]taxonom2__1500_18.min1.thm1.tptp2017-02-06 16:57 294  
[ ]taxonom2__1505_23.min1.thm1.tptp2017-02-06 16:57 302  
[ ]taxonom2__1593_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]taxonom2__1624_18.min1.thm1.tptp2017-02-06 16:57 278  
[ ]taxonom2__1632_14.min1.thm1.tptp2017-02-06 16:57 278  
[ ]taxonom2__1642_33.min1.thm1.tptp2017-02-06 16:57 314  
[ ]taxonom2__1957_32.min1.thm1.tptp2017-02-06 16:57 450  
[ ]taxonom2__1964_25.min1.thm1.tptp2017-02-06 16:57 442  
[ ]taxonom2__1982_27.min1.thm1.tptp2017-02-06 16:57 434  
[ ]taxonom2__2065_32.min1.thm1.tptp2017-02-06 16:57 552  
[ ]taxonom2__2072_25.min1.thm1.tptp2017-02-06 16:57 544  
[ ]taxonom2__2090_27.min1.thm1.tptp2017-02-06 16:57 536  
[ ]taylor_1__220_14.min1.thm1.tptp2017-02-06 16:57 264  
[ ]tbsp_1__1257_13.min1.thm1.tptp2017-02-06 16:57 258  
[ ]tdlat_3__816_20.min1.thm1.tptp2017-02-06 16:57 311  
[ ]termord__246_30.min1.thm1.tptp2017-02-06 16:57 424  
[ ]termord__260_30.min1.thm1.tptp2017-02-06 16:57 424  
[ ]termord__1186_27.min1.thm1.tptp2017-02-06 16:57 356  
[ ]termord__1254_48.min1.thm1.tptp2017-02-06 16:57 427  
[ ]termord__1283_48.min1.thm1.tptp2017-02-06 16:57 427  
[ ]termord__1320_17.min1.thm1.tptp2017-02-06 16:57 324  
[ ]termord__1453_45.min1.thm1.tptp2017-02-06 16:57 696  
[ ]termord__1517_21.min1.thm1.tptp2017-02-06 16:57 394  
[ ]termord__1565_29.min1.thm1.tptp2017-02-06 16:57 295  
[ ]termord__1623_22.min1.thm1.tptp2017-02-06 16:57 398  
[ ]termord__2300_28.min1.thm1.tptp2017-02-06 16:57 381  
[ ]tietze__1486_28.min1.thm1.tptp2017-02-06 16:57 344  
[ ]tietze__1500_14.min1.thm1.tptp2017-02-06 16:57 258  
[ ]tietze__1513_14.min1.thm1.tptp2017-02-06 16:57 268  
[ ]toler_1__401_24.min1.thm1.tptp2017-02-06 16:57 402  
[ ]toler_1__404_24.min1.thm1.tptp2017-02-06 16:57 402  
[ ]toler_1__613_25.min1.thm1.tptp2017-02-06 16:57 378  
[ ]toler_1__616_25.min1.thm1.tptp2017-02-06 16:57 378  
[ ]topalg_1__2344_32.min1.thm1.tptp2017-02-06 16:57 644  
[ ]topalg_1__2349_21.min1.thm1.tptp2017-02-06 16:57 636  
[ ]topalg_2__337_32.min1.thm1.tptp2017-02-06 16:57 572  
[ ]topalg_2__342_21.min1.thm1.tptp2017-02-06 16:57 564  
[ ]topalg_2__866_32.min1.thm1.tptp2017-02-06 16:57 572  
[ ]topalg_2__871_21.min1.thm1.tptp2017-02-06 16:57 564  
[ ]topalg_3__407_32.min1.thm1.tptp2017-02-06 16:57 304  
[ ]topalg_3__430_21.min1.thm1.tptp2017-02-06 16:57 320  
[ ]topalg_3__830_23.min1.thm1.tptp2017-02-06 16:57 342  
[ ]topalg_3__876_23.min1.thm1.tptp2017-02-06 16:57 342  
[ ]topalg_5__2056_21.min1.thm1.tptp2017-02-06 16:57 334  
[ ]topalg_5__2442_21.min1.thm1.tptp2017-02-06 16:57 334  
[ ]topalg_6__81_19.min1.thm1.tptp2017-02-06 16:57 386  
[ ]topalg_6__238_20.min1.thm1.tptp2017-02-06 16:57 459  
[ ]topalg_6__339_21.min1.thm1.tptp2017-02-06 16:57 564  
[ ]topalg_6__639_17.min1.thm1.tptp2017-02-06 16:57 492  
[ ]topalg_6__641_19.min1.thm1.tptp2017-02-06 16:57 415  
[ ]topalg_6__979_38.min1.thm1.tptp2017-02-06 16:57 669  
[ ]topalg_6__984_25.min1.thm1.tptp2017-02-06 16:57 660  
[ ]topdim_1__1764_13.min1.thm1.tptp2017-02-06 16:57 286  
[ ]topgen_2__1117_18.min1.thm1.tptp2017-02-06 16:57 273  
[ ]topgen_2__1136_12.min1.thm1.tptp2017-02-06 16:57 270  
[ ]topgen_2__1429_16.min1.thm1.tptp2017-02-06 16:57 303  
[ ]topgen_3__1990_17.min1.thm1.tptp2017-02-06 16:57 305  
[ ]topgen_3__2205_19.min1.thm1.tptp2017-02-06 16:57 274  
[ ]topgen_3__2224_14.min1.thm1.tptp2017-02-06 16:57 273  
[ ]topgen_3__2239_20.min1.thm1.tptp2017-02-06 16:57 274  
[ ]topmetr2__186_16.min1.thm1.tptp2017-02-06 16:57 378  
[ ]topmetr2__655_18.min1.thm1.tptp2017-02-06 16:57 306  
[ ]topmetr__910_25.min1.thm1.tptp2017-02-06 16:57 304  
[ ]topreal1__507_16.min1.thm1.tptp2017-02-06 16:57 276  
[ ]topreal2__1028_24.min1.thm1.tptp2017-02-06 16:57 290  
[ ]topreal2__1056_24.min1.thm1.tptp2017-02-06 16:57 290  
[ ]topreal3__331_24.min1.thm1.tptp2017-02-06 16:57 334  
[ ]topreal3__357_24.min1.thm1.tptp2017-02-06 16:57 334  
[ ]topreal3__980_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]topreal3__1057_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]topreal3__1102_11.min1.thm1.tptp2017-02-06 16:57 374  
[ ]topreal3__1144_11.min1.thm1.tptp2017-02-06 16:57 374  
[ ]topreal3__1217_19.min1.thm1.tptp2017-02-06 16:57 496  
[ ]topreal3__1222_12.min1.thm1.tptp2017-02-06 16:57 488  
[ ]topreal3__1294_19.min1.thm1.tptp2017-02-06 16:57 496  
[ ]topreal3__1299_12.min1.thm1.tptp2017-02-06 16:57 488  
[ ]topreal3__1895_25.min1.thm1.tptp2017-02-06 16:57 576  
[ ]topreal4__498_33.min1.thm1.tptp2017-02-06 16:57 562  
[ ]topreal4__554_33.min1.thm1.tptp2017-02-06 16:57 562  
[ ]topreal4__1572_23.min1.thm1.tptp2017-02-06 16:57 564  
[ ]topreal4__1584_45.min1.thm1.tptp2017-02-06 16:57 624  
[ ]topreal4__1772_22.min1.thm1.tptp2017-02-06 16:57 438  
[ ]topreal4__1889_22.min1.thm1.tptp2017-02-06 16:57 438  
[ ]topreal6__1564_12.min1.thm1.tptp2017-02-06 16:57 270  
[ ]topreal6__1599_12.min1.thm1.tptp2017-02-06 16:57 270  
[ ]topreal8__164_14.min1.thm1.tptp2017-02-06 16:57 326  
[ ]topreal8__939_30.min1.thm1.tptp2017-02-06 16:57 339  
[ ]topreal8__952_21.min1.thm1.tptp2017-02-06 16:57 328  
[ ]topreal8__962_19.min1.thm1.tptp2017-02-06 16:57 272  
[ ]topreal9__806_21.min1.thm1.tptp2017-02-06 16:57 278  
[ ]topreal9__810_15.min1.thm1.tptp2017-02-06 16:57 270  
[ ]topreal9__964_23.min1.thm1.tptp2017-02-06 16:57 286  
[ ]topreal9__970_15.min1.thm1.tptp2017-02-06 16:57 270  
[ ]topreal9__1290_18.min1.thm1.tptp2017-02-06 16:57 280  
[ ]topreal9__1463_21.min1.thm1.tptp2017-02-06 16:57 304  
[ ]toprns_1__82_19.min1.thm1.tptp2017-02-06 16:57 379  
[ ]toprns_1__95_30.min1.thm1.tptp2017-02-06 16:57 325  
[ ]trees_1__359_18.min1.thm1.tptp2017-02-06 16:57 258  
[ ]trees_1__436_20.min1.thm1.tptp2017-02-06 16:57 282  
[ ]trees_1__443_20.min1.thm1.tptp2017-02-06 16:57 282  
[ ]trees_1__1614_52.min1.thm1.tptp2017-02-06 16:57 379  
[ ]trees_1__1619_10.min1.thm1.tptp2017-02-06 16:57 264  
[ ]trees_1__2195_18.min1.thm1.tptp2017-02-06 16:57 278  
[ ]trees_1__2237_18.min1.thm1.tptp2017-02-06 16:57 278  
[ ]trees_2__874_14.min1.thm1.tptp2017-02-06 16:57 281  
[ ]trees_2__3095_14.min1.thm1.tptp2017-02-06 16:57 350  
[ ]trees_2__3106_19.min1.thm1.tptp2017-02-06 16:57 342  
[ ]trees_3__409_16.min1.thm1.tptp2017-02-06 16:57 357  
[ ]trees_3__425_16.min1.thm1.tptp2017-02-06 16:57 417  
[ ]trees_3__441_16.min1.thm1.tptp2017-02-06 16:57 409  
[ ]trees_3__1734_27.min1.thm1.tptp2017-02-06 16:57 312  
[ ]trees_4__1226_44.min1.thm1.tptp2017-02-06 16:57 290  
[ ]trees_4__1227_40.min1.thm1.tptp2017-02-06 16:57 290  
[ ]trees_9__252_16.min1.thm1.tptp2017-02-06 16:57 288  
[ ]trees_9__1895_23.min1.thm1.tptp2017-02-06 16:57 288  
[ ]trees_9__1919_24.min1.thm1.tptp2017-02-06 16:57 284  
[ ]trees_9__2001_21.min1.thm1.tptp2017-02-06 16:57 284  
[ ]trees_9__2019_24.min1.thm1.tptp2017-02-06 16:57 284  
[ ]trees_9__2187_26.min1.thm1.tptp2017-02-06 16:57 292  
[ ]trees_9__2230_13.min1.thm1.tptp2017-02-06 16:57 266  
[ ]trees_9__2551_27.min1.thm1.tptp2017-02-06 16:57 292  
[ ]valuat_1__1237_22.min1.thm1.tptp2017-02-06 16:57 298  
[ ]valuat_1__1705_32.min1.thm1.tptp2017-02-06 16:57 350  
[ ]valued_2__164_18.min1.thm1.tptp2017-02-06 16:57 444  
[ ]valued_2__196_75.min1.thm1.tptp2017-02-06 16:57 384  
[ ]vectsp_6__452_25.min1.thm1.tptp2017-02-06 16:57 456  
[ ]vectsp_9__1497_13.min1.thm1.tptp2017-02-06 16:57 282  
[ ]vfunct_1__253_32.min1.thm1.tptp2017-02-06 16:57 529  
[ ]vfunct_1__257_34.min1.thm1.tptp2017-02-06 16:57 413  
[ ]vfunct_1__265_28.min1.thm1.tptp2017-02-06 16:57 319  
[ ]vfunct_1__285_23.min1.thm1.tptp2017-02-06 16:57 413  
[ ]vfunct_1__294_22.min1.thm1.tptp2017-02-06 16:57 319  
[ ]vfunct_1__297_38.min1.thm1.tptp2017-02-06 16:57 531  
[ ]vfunct_1__315_29.min1.thm1.tptp2017-02-06 16:57 414  
[ ]vfunct_1__319_22.min1.thm1.tptp2017-02-06 16:57 424  
[ ]vfunct_1__329_22.min1.thm1.tptp2017-02-06 16:57 420  
[ ]vfunct_1__332_30.min1.thm1.tptp2017-02-06 16:57 410  
[ ]vfunct_1__345_27.min1.thm1.tptp2017-02-06 16:57 514  
[ ]vfunct_1__350_22.min1.thm1.tptp2017-02-06 16:57 424  
[ ]vfunct_1__360_22.min1.thm1.tptp2017-02-06 16:57 420  
[ ]vfunct_1__363_28.min1.thm1.tptp2017-02-06 16:57 510  
[ ]vfunct_1__383_30.min1.thm1.tptp2017-02-06 16:57 546  
[ ]vfunct_1__388_22.min1.thm1.tptp2017-02-06 16:57 424  
[ ]vfunct_1__398_26.min1.thm1.tptp2017-02-06 16:57 510  
[ ]vfunct_1__401_31.min1.thm1.tptp2017-02-06 16:57 542  
[ ]vfunct_2__131_32.min1.thm1.tptp2017-02-06 16:57 529  
[ ]vfunct_2__138_33.min1.thm1.tptp2017-02-06 16:57 415  
[ ]vfunct_2__164_22.min1.thm1.tptp2017-02-06 16:57 321  
[ ]vfunct_2__175_27.min1.thm1.tptp2017-02-06 16:57 415  
[ ]vfunct_2__178_38.min1.thm1.tptp2017-02-06 16:57 531  
[ ]vfunct_2__196_29.min1.thm1.tptp2017-02-06 16:57 408  
[ ]vfunct_2__200_22.min1.thm1.tptp2017-02-06 16:57 414  
[ ]vfunct_2__210_22.min1.thm1.tptp2017-02-06 16:57 410  
[ ]vfunct_2__213_30.min1.thm1.tptp2017-02-06 16:57 404  
[ ]vfunct_2__226_27.min1.thm1.tptp2017-02-06 16:57 500  
[ ]vfunct_2__231_22.min1.thm1.tptp2017-02-06 16:57 414  
[ ]vfunct_2__241_22.min1.thm1.tptp2017-02-06 16:57 410  
[ ]vfunct_2__244_28.min1.thm1.tptp2017-02-06 16:57 496  
[ ]vfunct_2__264_30.min1.thm1.tptp2017-02-06 16:57 530  
[ ]vfunct_2__269_22.min1.thm1.tptp2017-02-06 16:57 414  
[ ]vfunct_2__279_26.min1.thm1.tptp2017-02-06 16:57 496  
[ ]vfunct_2__282_31.min1.thm1.tptp2017-02-06 16:57 526  
[ ]waybel16__498_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel16__575_19.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel16__641_19.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel18__129_27.min1.thm1.tptp2017-02-06 16:57 277  
[ ]waybel18__1562_25.min1.thm1.tptp2017-02-06 16:57 362  
[ ]waybel18__1571_28.min1.thm1.tptp2017-02-06 16:57 362  
[ ]waybel18__2104_23.min1.thm1.tptp2017-02-06 16:57 552  
[ ]waybel18__2111_28.min1.thm1.tptp2017-02-06 16:57 338  
[ ]waybel22__1264_18.min1.thm1.tptp2017-02-06 16:57 338  
[ ]waybel22__1417_18.min1.thm1.tptp2017-02-06 16:57 298  
[ ]waybel25__74_21.min1.thm1.tptp2017-02-06 16:57 262  
[ ]waybel25__79_12.min1.thm1.tptp2017-02-06 16:57 254  
[ ]waybel25__107_21.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel25__112_12.min1.thm1.tptp2017-02-06 16:57 264  
[ ]waybel26__2142_14.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel27__566_14.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel27__688_28.min1.thm1.tptp2017-02-06 16:57 378  
[ ]waybel27__696_24.min1.thm1.tptp2017-02-06 16:57 370  
[ ]waybel27__718_24.min1.thm1.tptp2017-02-06 16:57 380  
[ ]waybel27__991_21.min1.thm1.tptp2017-02-06 16:57 279  
[ ]waybel29__778_15.min1.thm1.tptp2017-02-06 16:57 297  
[ ]waybel29__2567_33.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]waybel29__2581_28.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]waybel30__1341_16.min1.thm1.tptp2017-02-06 16:57 298  
[ ]waybel30__1388_16.min1.thm1.tptp2017-02-06 16:57 298  
[ ]waybel35__44_17.min1.thm1.tptp2017-02-06 16:57 359  
[ ]waybel_8__1695_23.min1.thm1.tptp2017-02-06 16:57 314  
[ ]waybel_8__1700_48.min1.thm1.tptp2017-02-06 16:57 340  
[ ]weddwitt__327_18.min1.thm1.tptp2017-02-06 16:57 354  
[ ]weddwitt__904_24.min1.thm1.tptp2017-02-06 16:57 396  
[ ]weddwitt__940_27.min1.thm1.tptp2017-02-06 16:57 548  
[ ]weddwitt__963_22.min1.thm1.tptp2017-02-06 16:57 392  
[ ]weddwitt__999_25.min1.thm1.tptp2017-02-06 16:57 542  
[ ]weddwitt__1020_26.min1.thm1.tptp2017-02-06 16:57 542  
[ ]weddwitt__1084_28.min1.thm1.tptp2017-02-06 16:57 551  
[ ]weddwitt__1287_27.min1.thm1.tptp2017-02-06 16:57 514  
[ ]weddwitt__1320_27.min1.thm1.tptp2017-02-06 16:57 410  
[ ]weddwitt__1992_22.min1.thm1.tptp2017-02-06 16:57 340  
[ ]weddwitt__2002_21.min1.thm1.tptp2017-02-06 16:57 312  
[ ]weddwitt__2016_25.min1.thm1.tptp2017-02-06 16:57 312  
[ ]weddwitt__2020_29.min1.thm1.tptp2017-02-06 16:57 315  
[ ]weddwitt__2411_26.min1.thm1.tptp2017-02-06 16:57 320  
[ ]weddwitt__2415_30.min1.thm1.tptp2017-02-06 16:57 323  
[ ]weddwitt__2437_16.min1.thm1.tptp2017-02-06 16:57 312  
[ ]weddwitt__3062_19.min1.thm1.tptp2017-02-06 16:57 258  
[ ]wellfnd1__187_17.min1.thm1.tptp2017-02-06 16:57 307  
[ ]wellord2__1049_13.min1.thm1.tptp2017-02-06 16:57 272  
[ ]wellord2__1113_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]wellord2__1115_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]wellset1__768_21.min1.thm1.tptp2017-02-06 16:57 491  
[ ]wellset1__1205_14.min1.thm1.tptp2017-02-06 16:57 298  
[ ]wellset1__1210_37.min1.thm1.tptp2017-02-06 16:57 322  
[ ]xtuple_0__47_17.min1.thm1.tptp2017-02-06 16:57 264  
[ ]xtuple_0__75_21.min1.thm1.tptp2017-02-06 16:57 294  
[ ]xtuple_0__77_14.min1.thm1.tptp2017-02-06 16:57 272  
[ ]xxreal_0__176_16.min1.thm1.tptp2017-02-06 16:57 296  
[ ]xxreal_0__185_16.min1.thm1.tptp2017-02-06 16:57 297  
[ ]xxreal_1__417_19.min1.thm1.tptp2017-02-06 16:57 274  
[ ]xxreal_1__421_12.min1.thm1.tptp2017-02-06 16:57 270  
[ ]xxreal_1__1386_19.min1.thm1.tptp2017-02-06 16:57 278  
[ ]xxreal_1__1396_17.min1.thm1.tptp2017-02-06 16:57 270  
[ ]xxreal_1__2271_36.min1.thm1.tptp2017-02-06 16:57 434  
[ ]xxreal_1__2276_31.min1.thm1.tptp2017-02-06 16:57 430  
[ ]xxreal_1__2290_36.min1.thm1.tptp2017-02-06 16:57 434  
[ ]xxreal_1__2295_31.min1.thm1.tptp2017-02-06 16:57 430  
[ ]xxreal_1__2309_36.min1.thm1.tptp2017-02-06 16:57 434  
[ ]xxreal_1__2314_31.min1.thm1.tptp2017-02-06 16:57 430  
[ ]xxreal_1__2328_36.min1.thm1.tptp2017-02-06 16:57 434  
[ ]xxreal_1__2333_31.min1.thm1.tptp2017-02-06 16:57 430  
[ ]xxreal_1__2413_17.min1.thm1.tptp2017-02-06 16:57 636  
[ ]xxreal_1__4188_18.min1.thm1.tptp2017-02-06 16:57 283  
[ ]xxreal_1__4218_18.min1.thm1.tptp2017-02-06 16:57 283  
[ ]xxreal_1__4248_18.min1.thm1.tptp2017-02-06 16:57 283  
[ ]xxreal_1__4278_18.min1.thm1.tptp2017-02-06 16:57 283  
[ ]xxreal_1__6519_17.min1.thm1.tptp2017-02-06 16:57 636  
[ ]xxreal_1__6547_17.min1.thm1.tptp2017-02-06 16:57 636  
[ ]xxreal_2__402_23.min1.thm1.tptp2017-02-06 16:57 354  
[ ]xxreal_2__404_28.min1.thm1.tptp2017-02-06 16:57 354  
[ ]xxreal_2__1367_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]xxreal_2__1379_17.min1.thm1.tptp2017-02-06 16:57 262  
[ ]yellow13__227_19.min1.thm1.tptp2017-02-06 16:57 297  
[ ]yellow13__469_27.min1.thm1.tptp2017-02-06 16:57 304  
[ ]yellow13__826_27.min1.thm1.tptp2017-02-06 16:57 304  
[ ]yellow13__1089_22.min1.thm1.tptp2017-02-06 16:57 472  
[ ]yellow14__603_11.min1.thm1.tptp2017-02-06 16:57 270  
[ ]yellow15__796_17.min1.thm1.tptp2017-02-06 16:57 278  
[ ]yellow17__47_23.min1.thm1.tptp2017-02-06 16:57 494  
[ ]yellow17__171_31.min1.thm1.tptp2017-02-06 16:57 402  
[ ]yellow_0__317_20.min1.thm1.tptp2017-02-06 16:57 382  
[ ]yellow_0__324_16.min1.thm1.tptp2017-02-06 16:57 368  
[ ]yellow_0__1541_23.min1.thm1.tptp2017-02-06 16:57 305  
[ ]yellow_0__1553_21.min1.thm1.tptp2017-02-06 16:57 304  
[ ]yellow_0__1619_23.min1.thm1.tptp2017-02-06 16:57 305  
[ ]yellow_0__1631_21.min1.thm1.tptp2017-02-06 16:57 304  
[ ]yellow_1__1125_13.min1.thm1.tptp2017-02-06 16:57 270  
[ ]yellow_8__727_27.min1.thm1.tptp2017-02-06 16:57 326  
[ ]yellow_8__731_22.min1.thm1.tptp2017-02-06 16:57 326  
[ ]yellow_8__756_19.min1.thm1.tptp2017-02-06 16:57 277  
[ ]yellow_9__696_27.min1.thm1.tptp2017-02-06 16:57 436  
[ ]yellow_9__834_13.min1.thm1.tptp2017-02-06 16:57 262  
[ ]yellow_9__851_21.min1.thm1.tptp2017-02-06 16:57 278  
[ ]yellow_9__856_12.min1.thm1.tptp2017-02-06 16:57 270  
[ ]yellow_9__943_22.min1.thm1.tptp2017-02-06 16:57 286  
[ ]yellow_9__961_12.min1.thm1.tptp2017-02-06 16:57 278  
[ ]zf_fund1__741_19.min1.thm1.tptp2017-02-06 16:57 399  
[ ]zf_fund1__803_23.min1.thm1.tptp2017-02-06 16:57 340  
[ ]zf_fund1__820_14.min1.thm1.tptp2017-02-06 16:57 307  
[ ]zf_fund1__1393_19.min1.thm1.tptp2017-02-06 16:57 416  
[ ]zf_fund1__1420_16.min1.thm1.tptp2017-02-06 16:57 404  
[ ]zf_fund2__387_29.min1.thm1.tptp2017-02-06 16:57 299  
[ ]zf_fund2__405_23.min1.thm1.tptp2017-02-06 16:57 291  
[ ]zf_fund2__591_26.min1.thm1.tptp2017-02-06 16:57 351  
[ ]zf_lang1__1927_24.min1.thm1.tptp2017-02-06 16:57 275  
[ ]zf_lang1__1956_24.min1.thm1.tptp2017-02-06 16:57 265  
[ ]zf_lang1__1980_24.min1.thm1.tptp2017-02-06 16:57 265  
[ ]zf_lang1__2004_24.min1.thm1.tptp2017-02-06 16:57 265  
[ ]zf_lang1__2027_24.min1.thm1.tptp2017-02-06 16:57 265  
[ ]zf_lang1__2589_14.min1.thm1.tptp2017-02-06 16:57 266  
[ ]zf_lang1__2635_16.min1.thm1.tptp2017-02-06 16:57 270  
[ ]zf_lang__482_31.min1.thm1.tptp2017-02-06 16:57 343  
[ ]zf_lang__487_27.min1.thm1.tptp2017-02-06 16:57 333  
[ ]zf_lang__492_28.min1.thm1.tptp2017-02-06 16:57 333  
[ ]zf_lang__2053_18.min1.thm1.tptp2017-02-06 16:57 326  
[ ]zf_lang__2076_19.min1.thm1.tptp2017-02-06 16:57 334  
[ ]zf_lang__2091_20.min1.thm1.tptp2017-02-06 16:57 306  
[ ]zf_lang__2155_20.min1.thm1.tptp2017-02-06 16:57 338  
[ ]zf_lang__2195_21.min1.thm1.tptp2017-02-06 16:57 338  
[ ]zf_model__784_16.min1.thm1.tptp2017-02-06 16:57 308  
[ ]zfmisc_1__43_16.min1.thm1.tptp2017-02-06 16:57 324  
[ ]zfmisc_1__202_17.min1.thm1.tptp2017-02-06 16:57 270  
[ ]zfmisc_1__226_13.min1.thm1.tptp2017-02-06 16:57 270  
[ ]zfmisc_1__245_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]zfmisc_1__267_17.min1.thm1.tptp2017-02-06 16:57 273  
[ ]zfmisc_1__288_22.min1.thm1.tptp2017-02-06 16:57 273  
[ ]zfmisc_1__295_23.min1.thm1.tptp2017-02-06 16:57 350  
[ ]zfmisc_1__304_17.min1.thm1.tptp2017-02-06 16:57 326  
[ ]zfmisc_1__322_17.min1.thm1.tptp2017-02-06 16:57 473  
[ ]zfmisc_1__332_17.min1.thm1.tptp2017-02-06 16:57 270  
[ ]zfmisc_1__348_26.min1.thm1.tptp2017-02-06 16:57 386  
[ ]zfmisc_1__353_19.min1.thm1.tptp2017-02-06 16:57 274  
[ ]zfmisc_1__362_17.min1.thm1.tptp2017-02-06 16:57 407  
[ ]zfmisc_1__370_19.min1.thm1.tptp2017-02-06 16:57 273  
[ ]zfmisc_1__393_17.min1.thm1.tptp2017-02-06 16:57 270  
[ ]zfmisc_1__513_19.min1.thm1.tptp2017-02-06 16:57 319  
[ ]zfmisc_1__578_20.min1.thm1.tptp2017-02-06 16:57 386  
[ ]zfmisc_1__604_13.min1.thm1.tptp2017-02-06 16:57 286  
[ ]zfmisc_1__610_26.min1.thm1.tptp2017-02-06 16:57 417  
[ ]zfmisc_1__625_13.min1.thm1.tptp2017-02-06 16:57 286  
[ ]zfmisc_1__768_17.min1.thm1.tptp2017-02-06 16:57 270  
[ ]zfmisc_1__781_17.min1.thm1.tptp2017-02-06 16:57 407  
[ ]zfmisc_1__801_17.min1.thm1.tptp2017-02-06 16:57 545  
[ ]zfmisc_1__2170_11.min1.thm1.tptp2017-02-06 16:57 292  
[ ]zfmisc_1__2193_16.min1.thm1.tptp2017-02-06 16:57 336  
[ ]zfmisc_1__2321_17.min1.thm1.tptp2017-02-06 16:57 301  
[ ]zfmisc_1__2359_26.min1.thm1.tptp2017-02-06 16:57 421  
[ ]zfmisc_1__2380_17.min1.thm1.tptp2017-02-06 16:57 558  
[ ]zfmodel1__1301_34.min1.thm1.tptp2017-02-06 16:57 327  
[ ]zfmodel2__274_23.min1.thm1.tptp2017-02-06 16:57 291  
[ ]zfmodel2__696_14.min1.thm1.tptp2017-02-06 16:57 281  
[ ]zfmodel2__1012_27.min1.thm1.tptp2017-02-06 16:57 344  
[ ]zfmodel2__1056_25.min1.thm1.tptp2017-02-06 16:57 319  
[ ]zfmodel2__1061_26.min1.thm1.tptp2017-02-06 16:57 329  
[ ]zfmodel2__1070_25.min1.thm1.tptp2017-02-06 16:57 329  
[ ]zfmodel2__1088_30.min1.thm1.tptp2017-02-06 16:57 319  
[ ]zfrefle1__306_13.min1.thm1.tptp2017-02-06 16:57 275  
[ ]zfrefle1__314_11.min1.thm1.tptp2017-02-06 16:57 274  
Apache/2.4.18 (Ubuntu) Server at grid01.ciirc.cvut.cz Port 80