Index of /~mptp/7.13.01_4.181.1147/mptp/ilp0/simplex0

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[ ]simplex0__61_45.min1.thm12017-02-06 12:46 370  
[ ]simplex0__61_45.min1.thm1.tptp2017-02-06 16:47 305  
[ ]simplex0__62_17.min1.thm12017-02-06 12:46 417  
[ ]simplex0__62_17.min1.thm1.tptp2017-02-06 16:47 364  
[ ]simplex0__65_14.min1.thm12017-02-06 12:46 451  
[ ]simplex0__72_16.min1.thm12017-02-06 12:46 351  
[ ]simplex0__72_16.min1.thm1.tptp2017-02-06 16:47 274  
[ ]simplex0__73_10.min1.thm12017-02-06 12:46 229  
[ ]simplex0__74_17.min1.thm12017-02-06 12:46 559  
[ ]simplex0__75_14.min1.thm12017-02-06 12:46 571  
[ ]simplex0__86_17.min1.thm12017-02-06 12:46 491  
[ ]simplex0__97_17.min1.thm12017-02-06 12:46 847  
[ ]simplex0__111_19.min1.thm12017-02-06 12:46 779  
[ ]simplex0__119_20.min1.thm12017-02-06 12:46 585  
[ ]simplex0__120_15.min1.thm12017-02-06 12:46 361  
[ ]simplex0__120_15.min1.thm1.tptp2017-02-06 16:47 280  
[ ]simplex0__121_17.min1.thm12017-02-06 12:46 901  
[ ]simplex0__133_21.min1.thm12017-02-06 12:46 463  
[ ]simplex0__133_21.min1.thm1.tptp2017-02-06 16:47 401  
[ ]simplex0__134_26.min1.thm12017-02-06 12:46 680  
[ ]simplex0__135_20.min1.thm12017-02-06 12:46 463  
[ ]simplex0__135_20.min1.thm1.tptp2017-02-06 16:47 401  
[ ]simplex0__144_11.min1.thm12017-02-06 12:46 509  
[ ]simplex0__145_20.min1.thm12017-02-06 12:46 523  
[ ]simplex0__146_11.min1.thm12017-02-06 12:46 416  
[ ]simplex0__146_11.min1.thm1.tptp2017-02-06 16:47 354  
[ ]simplex0__147_16.min1.thm12017-02-06 12:46 523  
[ ]simplex0__148_20.min1.thm12017-02-06 12:46 497  
[ ]simplex0__162_17.min1.thm12017-02-06 12:46 441  
[ ]simplex0__162_17.min1.thm1.tptp2017-02-06 16:47 386  
[ ]simplex0__165_13.min1.thm12017-02-06 12:46 475  
[ ]simplex0__165_13.min1.thm1.tptp2017-02-06 16:47 415  
[ ]simplex0__166_11.min1.thm12017-02-06 12:46 761  
[ ]simplex0__167_24.min1.thm12017-02-06 12:46 913  
[ ]simplex0__169_51.min1.thm12017-02-06 12:46 478  
[ ]simplex0__169_51.min1.thm1.tptp2017-02-06 16:47 425  
[ ]simplex0__171_16.min1.thm12017-02-06 12:46 271  
[ ]simplex0__176_25.min1.thm12017-02-06 12:46 621  
[ ]simplex0__177_18.min1.thm12017-02-06 12:46 945  
[ ]simplex0__185_16.min1.thm12017-02-06 12:46 498  
[ ]simplex0__186_46.min1.thm12017-02-06 12:46 468  
[ ]simplex0__186_46.min1.thm1.tptp2017-02-06 16:47 408  
[ ]simplex0__197_58.min1.thm12017-02-06 12:46 475  
[ ]simplex0__198_14.min1.thm12017-02-06 12:46 465  
[ ]simplex0__205_24.min1.thm12017-02-06 12:46 678  
[ ]simplex0__206_17.min1.thm12017-02-06 12:46 388  
[ ]simplex0__206_17.min1.thm1.tptp2017-02-06 16:47 318  
[ ]simplex0__216_65.min1.thm12017-02-06 12:46 471  
[ ]simplex0__217_37.min1.thm12017-02-06 12:46 551  
[ ]simplex0__221_17.min1.thm12017-02-06 12:46 587  
[ ]simplex0__223_30.min1.thm12017-02-06 12:46 475  
[ ]simplex0__223_30.min1.thm1.tptp2017-02-06 16:47 415  
[ ]simplex0__224_25.min1.thm12017-02-06 12:46 130  
[ ]simplex0__226_25.min1.thm12017-02-06 12:46 807  
[ ]simplex0__231_16.min1.thm12017-02-06 12:46 498  
[ ]simplex0__232_17.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__246_33.min1.thm12017-02-06 12:46 421  
[ ]simplex0__246_33.min1.thm1.tptp2017-02-06 16:47 357  
[ ]simplex0__247_16.min1.thm12017-02-06 12:46 711  
[ ]simplex0__248_15.min1.thm12017-02-06 12:46 615  
[ ]simplex0__250_14.min1.thm12017-02-06 12:46 600  
[ ]simplex0__260_41.min1.thm12017-02-06 12:46 331  
[ ]simplex0__260_41.min1.thm1.tptp2017-02-06 16:47 254  
[ ]simplex0__261_28.min1.thm12017-02-06 12:46 405  
[ ]simplex0__261_28.min1.thm1.tptp2017-02-06 16:47 341  
[ ]simplex0__268_19.min1.thm12017-02-06 12:46 312  
[ ]simplex0__268_19.min1.thm1.tptp2017-02-06 16:47 235  
[ ]simplex0__269_17.min1.thm12017-02-06 12:46 627  
[ ]simplex0__279_16.min1.thm12017-02-06 12:46 356  
[ ]simplex0__279_16.min1.thm1.tptp2017-02-06 16:47 285  
[ ]simplex0__280_36.min1.thm12017-02-06 12:46 456  
[ ]simplex0__281_17.min1.thm12017-02-06 12:46 449  
[ ]simplex0__294_16.min1.thm12017-02-06 12:46 413  
[ ]simplex0__294_16.min1.thm1.tptp2017-02-06 16:47 349  
[ ]simplex0__295_16.min1.thm12017-02-06 12:46 486  
[ ]simplex0__296_17.min1.thm12017-02-06 12:46 522  
[ ]simplex0__306_32.min1.thm12017-02-06 12:46 397  
[ ]simplex0__306_32.min1.thm1.tptp2017-02-06 16:47 333  
[ ]simplex0__307_17.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__314_17.min1.thm12017-02-06 12:46 270  
[ ]simplex0__319_19.min1.thm12017-02-06 12:46 427  
[ ]simplex0__319_19.min1.thm1.tptp2017-02-06 16:47 363  
[ ]simplex0__320_9.min1.thm12017-02-06 12:46 343  
[ ]simplex0__320_9.min1.thm1.tptp2017-02-06 16:47 278  
[ ]simplex0__321_23.min1.thm12017-02-06 12:46 670  
[ ]simplex0__325_17.min1.thm12017-02-06 12:46 733  
[ ]simplex0__339_20.min1.thm12017-02-06 12:46 463  
[ ]simplex0__339_20.min1.thm1.tptp2017-02-06 16:47 399  
[ ]simplex0__340_22.min1.thm12017-02-06 12:46 462  
[ ]simplex0__340_22.min1.thm1.tptp2017-02-06 16:47 400  
[ ]simplex0__341_29.min1.thm12017-02-06 12:46 569  
[ ]simplex0__342_23.min1.thm12017-02-06 12:46 514  
[ ]simplex0__342_23.min1.thm1.tptp2017-02-06 16:47 452  
[ ]simplex0__346_14.min1.thm12017-02-06 12:46 506  
[ ]simplex0__346_14.min1.thm1.tptp2017-02-06 16:47 444  
[ ]simplex0__350_17.min1.thm12017-02-06 12:46 405  
[ ]simplex0__350_17.min1.thm1.tptp2017-02-06 16:47 341  
[ ]simplex0__351_15.min1.thm12017-02-06 12:46 423  
[ ]simplex0__351_15.min1.thm1.tptp2017-02-06 16:47 361  
[ ]simplex0__352_18.min1.thm12017-02-06 12:46 526  
[ ]simplex0__357_17.min1.thm12017-02-06 12:46 405  
[ ]simplex0__357_17.min1.thm1.tptp2017-02-06 16:47 341  
[ ]simplex0__358_15.min1.thm12017-02-06 12:46 516  
[ ]simplex0__359_18.min1.thm12017-02-06 12:46 526  
[ ]simplex0__376_18.min1.thm12017-02-06 12:46 413  
[ ]simplex0__376_18.min1.thm1.tptp2017-02-06 16:47 349  
[ ]simplex0__379_17.min1.thm12017-02-06 12:46 500  
[ ]simplex0__380_12.min1.thm12017-02-06 12:46 457  
[ ]simplex0__381_19.min1.thm12017-02-06 12:46 476  
[ ]simplex0__387_17.min1.thm12017-02-06 12:46 440  
[ ]simplex0__388_32.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__389_14.min1.thm12017-02-06 12:46 292  
[ ]simplex0__401_33.min1.thm12017-02-06 12:46 405  
[ ]simplex0__401_33.min1.thm1.tptp2017-02-06 16:47 341  
[ ]simplex0__402_18.min1.thm12017-02-06 12:46 460  
[ ]simplex0__404_16.min1.thm12017-02-06 12:46 409  
[ ]simplex0__404_16.min1.thm1.tptp2017-02-06 16:47 355  
[ ]simplex0__414_16.min1.thm12017-02-06 12:46 417  
[ ]simplex0__414_16.min1.thm1.tptp2017-02-06 16:47 346  
[ ]simplex0__415_17.min1.thm12017-02-06 12:46 838  
[ ]simplex0__430_61.min1.thm12017-02-06 12:46 647  
[ ]simplex0__430_61.min1.thm1.tptp2017-02-06 16:47 593  
[ ]simplex0__431_15.min1.thm12017-02-06 12:46 640  
[ ]simplex0__433_42.min1.thm12017-02-06 12:46 559  
[ ]simplex0__437_61.min1.thm12017-02-06 12:46 825  
[ ]simplex0__438_33.min1.thm12017-02-06 12:46 452  
[ ]simplex0__441_14.min1.thm12017-02-06 12:46 777  
[ ]simplex0__453_35.min1.thm12017-02-06 12:46 793  
[ ]simplex0__454_18.min1.thm12017-02-06 12:46 885  
[ ]simplex0__458_34.min1.thm12017-02-06 12:46 783  
[ ]simplex0__459_17.min1.thm12017-02-06 12:46 871  
[ ]simplex0__470_16.min1.thm12017-02-06 12:46 312  
[ ]simplex0__470_16.min1.thm1.tptp2017-02-06 16:47 235  
[ ]simplex0__471_11.min1.thm12017-02-06 12:46 360  
[ ]simplex0__471_11.min1.thm1.tptp2017-02-06 16:47 282  
[ ]simplex0__472_53.min1.thm12017-02-06 12:46 598  
[ ]simplex0__474_19.min1.thm12017-02-06 12:46 469  
[ ]simplex0__475_17.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__487_25.min1.thm12017-02-06 12:46 969  
[ ]simplex0__488_14.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__503_11.min1.thm12017-02-06 12:46 787  
[ ]simplex0__504_20.min1.thm12017-02-06 12:46 534  
[ ]simplex0__505_38.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__506_29.min1.thm12017-02-06 12:46 745  
[ ]simplex0__507_10.min1.thm12017-02-06 12:46 818  
[ ]simplex0__508_17.min1.thm12017-02-06 12:46 953  
[ ]simplex0__519_14.min1.thm12017-02-06 12:46 227  
[ ]simplex0__520_29.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__521_52.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__522_14.min1.thm12017-02-06 12:46 657  
[ ]simplex0__534_16.min1.thm12017-02-06 12:46 460  
[ ]simplex0__534_16.min1.thm1.tptp2017-02-06 16:47 389  
[ ]simplex0__536_16.min1.thm12017-02-06 12:46 324  
[ ]simplex0__536_16.min1.thm1.tptp2017-02-06 16:47 247  
[ ]simplex0__537_12.min1.thm12017-02-06 12:46 850  
[ ]simplex0__538_22.min1.thm12017-02-06 12:46 860  
[ ]simplex0__539_20.min1.thm12017-02-06 12:46 487  
[ ]simplex0__540_29.min1.thm12017-02-06 12:46 513  
[ ]simplex0__541_11.min1.thm12017-02-06 12:46 368  
[ ]simplex0__541_11.min1.thm1.tptp2017-02-06 16:47 290  
[ ]simplex0__542_18.min1.thm12017-02-06 12:46 664  
[ ]simplex0__544_17.min1.thm12017-02-06 12:46 516  
[ ]simplex0__561_37.min1.thm12017-02-06 12:46 565  
[ ]simplex0__568_17.min1.thm12017-02-06 12:46 415  
[ ]simplex0__568_17.min1.thm1.tptp2017-02-06 16:47 360  
[ ]simplex0__569_11.min1.thm12017-02-06 12:46 352  
[ ]simplex0__569_11.min1.thm1.tptp2017-02-06 16:47 271  
[ ]simplex0__570_18.min1.thm12017-02-06 12:46 826  
[ ]simplex0__572_16.min1.thm12017-02-06 12:46 343  
[ ]simplex0__572_16.min1.thm1.tptp2017-02-06 16:47 265  
[ ]simplex0__573_17.min1.thm12017-02-06 12:46 515  
[ ]simplex0__596_40.min1.thm12017-02-06 12:46 511  
[ ]simplex0__597_46.min1.thm12017-02-06 12:46 766  
[ ]simplex0__598_15.min1.thm12017-02-06 12:46 633  
[ ]simplex0__600_19.min1.thm12017-02-06 12:46 870  
[ ]simplex0__603_26.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__604_25.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__605_32.min1.thm12017-02-06 12:46 546  
[ ]simplex0__606_21.min1.thm12017-02-06 12:46 337  
[ ]simplex0__607_28.min1.thm12017-02-06 12:46 566  
[ ]simplex0__608_46.min1.thm12017-02-06 12:46 541  
[ ]simplex0__612_28.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__613_20.min1.thm12017-02-06 12:46 647  
[ ]simplex0__616_24.min1.thm12017-02-06 12:46 546  
[ ]simplex0__617_24.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__618_23.min1.thm12017-02-06 12:46 777  
[ ]simplex0__619_30.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__620_29.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__621_26.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__622_34.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__623_18.min1.thm12017-02-06 12:46 512  
[ ]simplex0__624_28.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__625_19.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__634_16.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__635_15.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__638_18.min1.thm12017-02-06 12:46 2.2K 
[ ]simplex0__648_15.min1.thm12017-02-06 12:46 291  
[ ]simplex0__651_14.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__651_14.min1.thm1.tptp2017-02-06 16:47 1.0K 
[ ]simplex0__653_18.min1.thm12017-02-06 12:46 484  
[ ]simplex0__656_16.min1.thm12017-02-06 12:46 612  
[ ]simplex0__657_18.min1.thm12017-02-06 12:46 766  
[ ]simplex0__660_25.min1.thm12017-02-06 12:46 707  
[ ]simplex0__661_18.min1.thm12017-02-06 12:46 658  
[ ]simplex0__662_18.min1.thm12017-02-06 12:46 352  
[ ]simplex0__662_18.min1.thm1.tptp2017-02-06 16:47 278  
[ ]simplex0__665_25.min1.thm12017-02-06 12:46 707  
[ ]simplex0__666_18.min1.thm12017-02-06 12:46 658  
[ ]simplex0__667_18.min1.thm12017-02-06 12:46 352  
[ ]simplex0__667_18.min1.thm1.tptp2017-02-06 16:47 278  
[ ]simplex0__678_25.min1.thm12017-02-06 12:46 256  
[ ]simplex0__681_42.min1.thm12017-02-06 12:46 628  
[ ]simplex0__685_16.min1.thm12017-02-06 12:46 853  
[ ]simplex0__689_18.min1.thm12017-02-06 12:46 315  
[ ]simplex0__689_18.min1.thm1.tptp2017-02-06 16:47 232  
[ ]simplex0__692_17.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__693_13.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__694_24.min1.thm12017-02-06 12:46 566  
[ ]simplex0__704_29.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__706_30.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__707_42.min1.thm12017-02-06 12:46 811  
[ ]simplex0__708_55.min1.thm12017-02-06 12:46 753  
[ ]simplex0__708_55.min1.thm1.tptp2017-02-06 16:47 679  
[ ]simplex0__709_35.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__710_42.min1.thm12017-02-06 12:46 928  
[ ]simplex0__710_42.min1.thm1.tptp2017-02-06 16:47 854  
[ ]simplex0__711_12.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__712_18.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__714_20.min1.thm12017-02-06 12:46 488  
[ ]simplex0__717_43.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__718_29.min1.thm12017-02-06 12:46 474  
[ ]simplex0__719_33.min1.thm12017-02-06 12:46 588  
[ ]simplex0__720_24.min1.thm12017-02-06 12:46 587  
[ ]simplex0__721_39.min1.thm12017-02-06 12:46 653  
[ ]simplex0__726_26.min1.thm12017-02-06 12:46 490  
[ ]simplex0__727_15.min1.thm12017-02-06 12:46 601  
[ ]simplex0__728_22.min1.thm12017-02-06 12:46 763  
[ ]simplex0__729_22.min1.thm12017-02-06 12:46 824  
[ ]simplex0__730_17.min1.thm12017-02-06 12:46 826  
[ ]simplex0__731_22.min1.thm12017-02-06 12:46 563  
[ ]simplex0__734_13.min1.thm12017-02-06 12:46 541  
[ ]simplex0__734_13.min1.thm1.tptp2017-02-06 16:47 464  
[ ]simplex0__735_17.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__737_59.min1.thm12017-02-06 12:46 822  
[ ]simplex0__741_25.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__742_16.min1.thm12017-02-06 12:46 836  
[ ]simplex0__743_40.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__744_17.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__747_28.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__748_24.min1.thm12017-02-06 12:46 439  
[ ]simplex0__755_16.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__756_16.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__758_28.min1.thm12017-02-06 12:46 529  
[ ]simplex0__759_25.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__760_17.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__761_17.min1.thm12017-02-06 12:46 592  
[ ]simplex0__762_54.min1.thm12017-02-06 12:46 807  
[ ]simplex0__766_18.min1.thm12017-02-06 12:46 446  
[ ]simplex0__767_26.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__768_22.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__769_12.min1.thm12017-02-06 12:46 608  
[ ]simplex0__774_31.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__775_22.min1.thm12017-02-06 12:46 625  
[ ]simplex0__776_13.min1.thm12017-02-06 12:46 271  
[ ]simplex0__777_19.min1.thm12017-02-06 12:46 724  
[ ]simplex0__778_20.min1.thm12017-02-06 12:46 587  
[ ]simplex0__779_30.min1.thm12017-02-06 12:46 653  
[ ]simplex0__781_28.min1.thm12017-02-06 12:46 705  
[ ]simplex0__782_24.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__783_29.min1.thm12017-02-06 12:46 464  
[ ]simplex0__783_29.min1.thm1.tptp2017-02-06 16:47 386  
[ ]simplex0__784_17.min1.thm12017-02-06 12:46 593  
[ ]simplex0__785_29.min1.thm12017-02-06 12:46 889  
[ ]simplex0__787_25.min1.thm12017-02-06 12:46 945  
[ ]simplex0__788_23.min1.thm12017-02-06 12:46 575  
[ ]simplex0__789_19.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__790_25.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__791_13.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__815_53.min1.thm12017-02-06 12:46 750  
[ ]simplex0__816_16.min1.thm12017-02-06 12:46 353  
[ ]simplex0__818_45.min1.thm12017-02-06 12:46 676  
[ ]simplex0__820_17.min1.thm12017-02-06 12:46 913  
[ ]simplex0__823_38.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__825_50.min1.thm12017-02-06 12:46 934  
[ ]simplex0__826_24.min1.thm12017-02-06 12:46 394  
[ ]simplex0__829_14.min1.thm12017-02-06 12:46 890  
[ ]simplex0__830_18.min1.thm12017-02-06 12:46 364  
[ ]simplex0__830_18.min1.thm1.tptp2017-02-06 16:47 283  
[ ]simplex0__846_52.min1.thm12017-02-06 12:46 754  
[ ]simplex0__847_16.min1.thm12017-02-06 12:46 355  
[ ]simplex0__849_45.min1.thm12017-02-06 12:46 676  
[ ]simplex0__851_19.min1.thm12017-02-06 12:46 525  
[ ]simplex0__858_13.min1.thm12017-02-06 12:46 937  
[ ]simplex0__859_19.min1.thm12017-02-06 12:46 701  
[ ]simplex0__861_12.min1.thm12017-02-06 12:46 197  
[ ]simplex0__864_6.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__871_17.min1.thm12017-02-06 12:46 446  
[ ]simplex0__872_17.min1.thm12017-02-06 12:46 502  
[ ]simplex0__873_19.min1.thm12017-02-06 12:46 437  
[ ]simplex0__876_18.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__877_52.min1.thm12017-02-06 12:46 926  
[ ]simplex0__879_6.min1.thm12017-02-06 12:46 690  
[ ]simplex0__879_6.min1.thm1.tptp2017-02-06 16:47 637  
[ ]simplex0__886_17.min1.thm12017-02-06 12:46 446  
[ ]simplex0__887_17.min1.thm12017-02-06 12:46 503  
[ ]simplex0__888_19.min1.thm12017-02-06 12:46 439  
[ ]simplex0__901_18.min1.thm12017-02-06 12:46 771  
[ ]simplex0__901_18.min1.thm1.tptp2017-02-06 16:47 715  
[ ]simplex0__902_22.min1.thm12017-02-06 12:46 519  
[ ]simplex0__908_28.min1.thm12017-02-06 12:46 567  
[ ]simplex0__911_33.min1.thm12017-02-06 12:46 709  
[ ]simplex0__912_51.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__914_17.min1.thm12017-02-06 12:46 3.1K 
[ ]simplex0__923_24.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__925_52.min1.thm12017-02-06 12:46 672  
[ ]simplex0__931_24.min1.thm12017-02-06 12:46 607  
[ ]simplex0__931_24.min1.thm1.tptp2017-02-06 16:47 543  
[ ]simplex0__933_14.min1.thm12017-02-06 12:46 609  
[ ]simplex0__933_14.min1.thm1.tptp2017-02-06 16:47 545  
[ ]simplex0__934_28.min1.thm12017-02-06 12:46 769  
[ ]simplex0__935_23.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__936_29.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__937_18.min1.thm12017-02-06 12:46 855  
[ ]simplex0__937_18.min1.thm1.tptp2017-02-06 16:47 799  
[ ]simplex0__945_23.min1.thm12017-02-06 12:46 607  
[ ]simplex0__945_23.min1.thm1.tptp2017-02-06 16:47 543  
[ ]simplex0__952_25.min1.thm12017-02-06 12:46 557  
[ ]simplex0__952_25.min1.thm1.tptp2017-02-06 16:47 476  
[ ]simplex0__953_21.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__954_23.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__956_23.min1.thm12017-02-06 12:46 870  
[ ]simplex0__957_32.min1.thm12017-02-06 12:46 913  
[ ]simplex0__957_32.min1.thm1.tptp2017-02-06 16:47 857  
[ ]simplex0__958_18.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__959_15.min1.thm12017-02-06 12:46 947  
[ ]simplex0__963_17.min1.thm12017-02-06 12:46 854  
[ ]simplex0__976_21.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__977_24.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__978_22.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__979_24.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__980_13.min1.thm12017-02-06 12:46 772  
[ ]simplex0__980_13.min1.thm1.tptp2017-02-06 16:47 716  
[ ]simplex0__981_23.min1.thm12017-02-06 12:46 406  
[ ]simplex0__981_23.min1.thm1.tptp2017-02-06 16:47 332  
[ ]simplex0__982_18.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__983_19.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__987_19.min1.thm12017-02-06 12:46 511  
[ ]simplex0__988_21.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__991_29.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__992_10.min1.thm12017-02-06 12:46 584  
[ ]simplex0__993_18.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__1003_17.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1005_18.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__1013_24.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__1014_26.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__1015_20.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__1016_28.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__1017_12.min1.thm12017-02-06 12:46 265  
[ ]simplex0__1019_20.min1.thm12017-02-06 12:46 867  
[ ]simplex0__1020_26.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1022_20.min1.thm12017-02-06 12:46 382  
[ ]simplex0__1022_20.min1.thm1.tptp2017-02-06 16:47 315  
[ ]simplex0__1024_20.min1.thm12017-02-06 12:46 423  
[ ]simplex0__1024_20.min1.thm1.tptp2017-02-06 16:47 358  
[ ]simplex0__1025_30.min1.thm12017-02-06 12:46 2.5K 
[ ]simplex0__1026_18.min1.thm12017-02-06 12:46 845  
[ ]simplex0__1027_28.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__1028_18.min1.thm12017-02-06 12:46 743  
[ ]simplex0__1029_14.min1.thm12017-02-06 12:46 800  
[ ]simplex0__1030_19.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__1035_29.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__1036_25.min1.thm12017-02-06 12:46 2.5K 
[ ]simplex0__1038_18.min1.thm12017-02-06 12:46 845  
[ ]simplex0__1041_24.min1.thm12017-02-06 12:46 2.3K 
[ ]simplex0__1042_19.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__1043_25.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__1044_20.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__1045_20.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__1049_21.min1.thm12017-02-06 12:46 619  
[ ]simplex0__1050_23.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1053_31.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__1054_25.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1055_15.min1.thm12017-02-06 12:46 2.9K 
[ ]simplex0__1067_19.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1070_19.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1072_28.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__1073_19.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__1080_28.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__1081_24.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__1082_31.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__1083_28.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__1084_19.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__1091_28.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__1092_24.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__1093_31.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__1094_36.min1.thm12017-02-06 12:46 698  
[ ]simplex0__1095_15.min1.thm12017-02-06 12:46 876  
[ ]simplex0__1095_15.min1.thm1.tptp2017-02-06 16:47 811  
[ ]simplex0__1097_41.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__1098_42.min1.thm12017-02-06 12:46 684  
[ ]simplex0__1099_38.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__1100_19.min1.thm12017-02-06 12:46 723  
[ ]simplex0__1103_21.min1.thm12017-02-06 12:46 565  
[ ]simplex0__1103_21.min1.thm1.tptp2017-02-06 16:47 491  
[ ]simplex0__1104_28.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1105_19.min1.thm12017-02-06 12:46 644  
[ ]simplex0__1106_28.min1.thm12017-02-06 12:46 675  
[ ]simplex0__1107_18.min1.thm12017-02-06 12:46 860  
[ ]simplex0__1107_18.min1.thm1.tptp2017-02-06 16:47 804  
[ ]simplex0__1108_23.min1.thm12017-02-06 12:46 524  
[ ]simplex0__1108_23.min1.thm1.tptp2017-02-06 16:47 450  
[ ]simplex0__1109_42.min1.thm12017-02-06 12:46 757  
[ ]simplex0__1111_23.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1112_19.min1.thm12017-02-06 12:46 620  
[ ]simplex0__1115_21.min1.thm12017-02-06 12:46 565  
[ ]simplex0__1115_21.min1.thm1.tptp2017-02-06 16:47 491  
[ ]simplex0__1116_29.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1117_19.min1.thm12017-02-06 12:46 644  
[ ]simplex0__1118_28.min1.thm12017-02-06 12:46 675  
[ ]simplex0__1119_18.min1.thm12017-02-06 12:46 860  
[ ]simplex0__1119_18.min1.thm1.tptp2017-02-06 16:47 804  
[ ]simplex0__1120_23.min1.thm12017-02-06 12:46 524  
[ ]simplex0__1120_23.min1.thm1.tptp2017-02-06 16:47 450  
[ ]simplex0__1121_42.min1.thm12017-02-06 12:46 757  
[ ]simplex0__1123_23.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1124_19.min1.thm12017-02-06 12:46 620  
[ ]simplex0__1130_22.min1.thm12017-02-06 12:46 401  
[ ]simplex0__1130_22.min1.thm1.tptp2017-02-06 16:47 318  
[ ]simplex0__1133_19.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1135_26.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__1136_13.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__1143_21.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__1144_29.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__1145_19.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__1157_35.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__1158_19.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__1165_22.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__1167_32.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__1168_34.min1.thm12017-02-06 12:46 2.3K 
[ ]simplex0__1169_19.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__1176_22.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__1178_32.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__1179_34.min1.thm12017-02-06 12:46 2.3K 
[ ]simplex0__1180_35.min1.thm12017-02-06 12:46 704  
[ ]simplex0__1181_15.min1.thm12017-02-06 12:46 890  
[ ]simplex0__1181_15.min1.thm1.tptp2017-02-06 16:47 825  
[ ]simplex0__1183_23.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__1184_19.min1.thm12017-02-06 12:46 2.6K 
[ ]simplex0__1187_16.min1.thm12017-02-06 12:46 865  
[ ]simplex0__1187_16.min1.thm1.tptp2017-02-06 16:47 809  
[ ]simplex0__1188_21.min1.thm12017-02-06 12:46 530  
[ ]simplex0__1188_21.min1.thm1.tptp2017-02-06 16:47 456  
[ ]simplex0__1189_32.min1.thm12017-02-06 12:46 765  
[ ]simplex0__1191_14.min1.thm12017-02-06 12:46 573  
[ ]simplex0__1191_14.min1.thm1.tptp2017-02-06 16:47 499  
[ ]simplex0__1192_21.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1193_23.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1194_24.min1.thm12017-02-06 12:46 910  
[ ]simplex0__1198_16.min1.thm12017-02-06 12:46 864  
[ ]simplex0__1198_16.min1.thm1.tptp2017-02-06 16:47 808  
[ ]simplex0__1199_21.min1.thm12017-02-06 12:46 530  
[ ]simplex0__1199_21.min1.thm1.tptp2017-02-06 16:47 456  
[ ]simplex0__1200_32.min1.thm12017-02-06 12:46 765  
[ ]simplex0__1202_14.min1.thm12017-02-06 12:46 573  
[ ]simplex0__1202_14.min1.thm1.tptp2017-02-06 16:47 499  
[ ]simplex0__1203_21.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1204_23.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1205_24.min1.thm12017-02-06 12:46 911  
[ ]simplex0__1210_32.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__1211_17.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__1238_53.min1.thm12017-02-06 12:46 572  
[ ]simplex0__1239_17.min1.thm12017-02-06 12:46 951  
[ ]simplex0__1253_38.min1.thm12017-02-06 12:46 524  
[ ]simplex0__1254_24.min1.thm12017-02-06 12:46 954  
[ ]simplex0__1255_19.min1.thm12017-02-06 12:46 694  
[ ]simplex0__1261_17.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1284_24.min1.thm12017-02-06 12:46 586  
[ ]simplex0__1285_55.min1.thm12017-02-06 12:46 735  
[ ]simplex0__1286_18.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1288_34.min1.thm12017-02-06 12:46 639  
[ ]simplex0__1292_54.min1.thm12017-02-06 12:46 764  
[ ]simplex0__1293_25.min1.thm12017-02-06 12:46 327  
[ ]simplex0__1296_14.min1.thm12017-02-06 12:46 699  
[ ]simplex0__1305_38.min1.thm12017-02-06 12:46 518  
[ ]simplex0__1306_22.min1.thm12017-02-06 12:46 625  
[ ]simplex0__1307_19.min1.thm12017-02-06 12:46 625  
[ ]simplex0__1311_37.min1.thm12017-02-06 12:46 510  
[ ]simplex0__1312_21.min1.thm12017-02-06 12:46 607  
[ ]simplex0__1313_17.min1.thm12017-02-06 12:46 607  
[ ]simplex0__1355_16.min1.thm12017-02-06 12:46 577  
[ ]simplex0__1370_54.min1.thm12017-02-06 12:46 405  
[ ]simplex0__1372_33.min1.thm12017-02-06 12:46 379  
[ ]simplex0__1372_33.min1.thm1.tptp2017-02-06 16:47 308  
[ ]simplex0__1373_35.min1.thm12017-02-06 12:46 602  
[ ]simplex0__1374_24.min1.thm12017-02-06 12:46 528  
[ ]simplex0__1375_53.min1.thm12017-02-06 12:46 602  
[ ]simplex0__1376_23.min1.thm12017-02-06 12:46 676  
[ ]simplex0__1377_27.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__1383_25.min1.thm12017-02-06 12:46 331  
[ ]simplex0__1383_25.min1.thm1.tptp2017-02-06 16:47 254  
[ ]simplex0__1384_33.min1.thm12017-02-06 12:46 568  
[ ]simplex0__1385_21.min1.thm12017-02-06 12:46 835  
[ ]simplex0__1388_16.min1.thm12017-02-06 12:46 699  
[ ]simplex0__1389_27.min1.thm12017-02-06 12:46 591  
[ ]simplex0__1390_53.min1.thm12017-02-06 12:46 516  
[ ]simplex0__1399_35.min1.thm12017-02-06 12:46 482  
[ ]simplex0__1400_21.min1.thm12017-02-06 12:46 889  
[ ]simplex0__1401_17.min1.thm12017-02-06 12:46 811  
[ ]simplex0__1409_16.min1.thm12017-02-06 12:46 666  
[ ]simplex0__1416_36.min1.thm12017-02-06 12:46 576  
[ ]simplex0__1417_22.min1.thm12017-02-06 12:46 849  
[ ]simplex0__1420_17.min1.thm12017-02-06 12:46 711  
[ ]simplex0__1421_28.min1.thm12017-02-06 12:46 602  
[ ]simplex0__1422_40.min1.thm12017-02-06 12:46 931  
[ ]simplex0__1428_32.min1.thm12017-02-06 12:46 792  
[ ]simplex0__1429_32.min1.thm12017-02-06 12:46 594  
[ ]simplex0__1430_22.min1.thm12017-02-06 12:46 658  
[ ]simplex0__1431_17.min1.thm12017-02-06 12:46 759  
[ ]simplex0__1436_39.min1.thm12017-02-06 12:46 404  
[ ]simplex0__1436_39.min1.thm1.tptp2017-02-06 16:47 327  
[ ]simplex0__1437_49.min1.thm12017-02-06 12:46 823  
[ ]simplex0__1439_30.min1.thm12017-02-06 12:46 395  
[ ]simplex0__1440_17.min1.thm12017-02-06 12:46 724  
[ ]simplex0__1449_49.min1.thm12017-02-06 12:46 425  
[ ]simplex0__1450_17.min1.thm12017-02-06 12:46 502  
[ ]simplex0__1457_53.min1.thm12017-02-06 12:46 425  
[ ]simplex0__1458_17.min1.thm12017-02-06 12:46 502  
[ ]simplex0__1466_49.min1.thm12017-02-06 12:46 663  
[ ]simplex0__1467_17.min1.thm12017-02-06 12:46 425  
[ ]simplex0__1475_45.min1.thm12017-02-06 12:46 636  
[ ]simplex0__1476_17.min1.thm12017-02-06 12:46 896  
[ ]simplex0__1484_49.min1.thm12017-02-06 12:46 419  
[ ]simplex0__1490_16.min1.thm12017-02-06 12:46 615  
[ ]simplex0__1491_18.min1.thm12017-02-06 12:46 738  
[ ]simplex0__1493_24.min1.thm12017-02-06 12:46 420  
[ ]simplex0__1494_17.min1.thm12017-02-06 12:46 611  
[ ]simplex0__1502_56.min1.thm12017-02-06 12:46 628  
[ ]simplex0__1510_64.min1.thm12017-02-06 12:46 872  
[ ]simplex0__1511_19.min1.thm12017-02-06 12:46 647  
[ ]simplex0__1513_33.min1.thm12017-02-06 12:46 421  
[ ]simplex0__1514_18.min1.thm12017-02-06 12:46 702  
[ ]simplex0__1520_37.min1.thm12017-02-06 12:46 634  
[ ]simplex0__1521_23.min1.thm12017-02-06 12:46 818  
[ ]simplex0__1522_16.min1.thm12017-02-06 12:46 726  
[ ]simplex0__1523_15.min1.thm12017-02-06 12:46 700  
[ ]simplex0__1528_17.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1540_37.min1.thm12017-02-06 12:46 634  
[ ]simplex0__1541_24.min1.thm12017-02-06 12:46 608  
[ ]simplex0__1542_28.min1.thm12017-02-06 12:46 818  
[ ]simplex0__1543_12.min1.thm12017-02-06 12:46 209  
[ ]simplex0__1545_16.min1.thm12017-02-06 12:46 317  
[ ]simplex0__1545_16.min1.thm1.tptp2017-02-06 16:47 236  
[ ]simplex0__1549_19.min1.thm12017-02-06 12:46 423  
[ ]simplex0__1550_35.min1.thm12017-02-06 12:46 548  
[ ]simplex0__1551_23.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1552_39.min1.thm12017-02-06 12:46 903  
[ ]simplex0__1563_42.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1564_18.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1565_32.min1.thm12017-02-06 12:46 622  
[ ]simplex0__1566_19.min1.thm12017-02-06 12:46 594  
[ ]simplex0__1567_14.min1.thm12017-02-06 12:46 607  
[ ]simplex0__1568_18.min1.thm12017-02-06 12:46 934  
[ ]simplex0__1569_27.min1.thm12017-02-06 12:46 690  
[ ]simplex0__1570_39.min1.thm12017-02-06 12:46 746  
[ ]simplex0__1571_16.min1.thm12017-02-06 12:46 303  
[ ]simplex0__1572_24.min1.thm12017-02-06 12:46 507  
[ ]simplex0__1572_24.min1.thm1.tptp2017-02-06 16:47 445  
[ ]simplex0__1573_24.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1583_16.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1584_25.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1585_20.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1587_18.min1.thm12017-02-06 12:46 654  
[ ]simplex0__1588_28.min1.thm12017-02-06 12:46 753  
[ ]simplex0__1590_9.min1.thm12017-02-06 12:46 850  
[ ]simplex0__1593_16.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1594_24.min1.thm12017-02-06 12:46 905  
[ ]simplex0__1597_17.min1.thm12017-02-06 12:46 419  
[ ]simplex0__1606_37.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__1607_78.min1.thm12017-02-06 12:46 856  
[ ]simplex0__1610_13.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__1620_46.min1.thm12017-02-06 12:46 545  
[ ]simplex0__1621_26.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1622_70.min1.thm12017-02-06 12:46 717  
[ ]simplex0__1624_41.min1.thm12017-02-06 12:46 602  
[ ]simplex0__1625_38.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1626_17.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__1633_47.min1.thm12017-02-06 12:46 834  
[ ]simplex0__1635_70.min1.thm12017-02-06 12:46 784  
[ ]simplex0__1641_36.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1642_22.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1646_12.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1649_13.min1.thm12017-02-06 12:46 609  
[ ]simplex0__1650_37.min1.thm12017-02-06 12:46 758  
[ ]simplex0__1651_50.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1652_19.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1653_28.min1.thm12017-02-06 12:46 831  
[ ]simplex0__1666_13.min1.thm12017-02-06 12:46 581  
[ ]simplex0__1673_14.min1.thm12017-02-06 12:46 494  
[ ]simplex0__1683_35.min1.thm12017-02-06 12:46 668  
[ ]simplex0__1684_39.min1.thm12017-02-06 12:46 439  
[ ]simplex0__1684_39.min1.thm1.tptp2017-02-06 16:47 362  
[ ]simplex0__1685_49.min1.thm12017-02-06 12:46 862  
[ ]simplex0__1686_25.min1.thm12017-02-06 12:46 368  
[ ]simplex0__1686_25.min1.thm1.tptp2017-02-06 16:47 291  
[ ]simplex0__1687_17.min1.thm12017-02-06 12:46 824  
[ ]simplex0__1700_36.min1.thm12017-02-06 12:46 536  
[ ]simplex0__1701_22.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1702_36.min1.thm12017-02-06 12:46 645  
[ ]simplex0__1703_39.min1.thm12017-02-06 12:46 368  
[ ]simplex0__1703_39.min1.thm1.tptp2017-02-06 16:47 291  
[ ]simplex0__1704_17.min1.thm12017-02-06 12:46 775  
[ ]simplex0__1709_48.min1.thm12017-02-06 12:46 407  
[ ]simplex0__1709_48.min1.thm1.tptp2017-02-06 16:47 350  
[ ]simplex0__1712_41.min1.thm12017-02-06 12:46 322  
[ ]simplex0__1715_68.min1.thm12017-02-06 12:46 412  
[ ]simplex0__1718_61.min1.thm12017-02-06 12:46 296  
[ ]simplex0__1730_22.min1.thm12017-02-06 12:46 401  
[ ]simplex0__1731_34.min1.thm12017-02-06 12:46 404  
[ ]simplex0__1731_34.min1.thm1.tptp2017-02-06 16:47 327  
[ ]simplex0__1736_50.min1.thm12017-02-06 12:46 891  
[ ]simplex0__1737_15.min1.thm12017-02-06 12:46 326  
[ ]simplex0__1741_35.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__1742_17.min1.thm12017-02-06 12:46 835  
[ ]simplex0__1745_27.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__1746_27.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__1747_34.min1.thm12017-02-06 12:46 596  
[ ]simplex0__1753_18.min1.thm12017-02-06 12:46 808  
[ ]simplex0__1756_48.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__1757_17.min1.thm12017-02-06 12:46 403  
[ ]simplex0__1767_34.min1.thm12017-02-06 12:46 486  
[ ]simplex0__1768_48.min1.thm12017-02-06 12:46 401  
[ ]simplex0__1771_25.min1.thm12017-02-06 12:46 368  
[ ]simplex0__1771_25.min1.thm1.tptp2017-02-06 16:47 299  
[ ]simplex0__1772_25.min1.thm12017-02-06 12:46 370  
[ ]simplex0__1772_25.min1.thm1.tptp2017-02-06 16:47 292  
[ ]simplex0__1773_54.min1.thm12017-02-06 12:46 642  
[ ]simplex0__1774_34.min1.thm12017-02-06 12:46 385  
[ ]simplex0__1774_34.min1.thm1.tptp2017-02-06 16:47 302  
[ ]simplex0__1787_50.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__1788_17.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1800_17.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1818_17.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1829_48.min1.thm12017-02-06 12:46 700  
[ ]simplex0__1830_44.min1.thm12017-02-06 12:46 853  
[ ]simplex0__1832_31.min1.thm12017-02-06 12:46 729  
[ ]simplex0__1833_30.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__1834_17.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__1842_39.min1.thm12017-02-06 12:46 394  
[ ]simplex0__1864_44.min1.thm12017-02-06 12:46 374  
[ ]simplex0__1864_44.min1.thm1.tptp2017-02-06 16:47 295  
[ ]simplex0__1865_32.min1.thm12017-02-06 12:46 489  
[ ]simplex0__1866_17.min1.thm12017-02-06 12:46 648  
[ ]simplex0__1871_21.min1.thm12017-02-06 12:46 821  
[ ]simplex0__1872_14.min1.thm12017-02-06 12:46 805  
[ ]simplex0__1882_32.min1.thm12017-02-06 12:46 495  
[ ]simplex0__1883_33.min1.thm12017-02-06 12:46 887  
[ ]simplex0__1884_13.min1.thm12017-02-06 12:46 663  
[ ]simplex0__1885_14.min1.thm12017-02-06 12:46 479  
[ ]simplex0__1885_14.min1.thm1.tptp2017-02-06 16:47 398  
[ ]simplex0__1905_49.min1.thm12017-02-06 12:46 531  
[ ]simplex0__1906_29.min1.thm12017-02-06 12:46 710  
[ ]simplex0__1914_12.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1917_34.min1.thm12017-02-06 12:46 538  
[ ]simplex0__1918_41.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1919_28.min1.thm12017-02-06 12:46 789  
[ ]simplex0__1920_20.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__1930_24.min1.thm12017-02-06 12:46 3.1K 
[ ]simplex0__1951_21.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__1952_16.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__1953_17.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1957_13.min1.thm12017-02-06 12:46 577  
[ ]simplex0__1965_11.min1.thm12017-02-06 12:46 195  
[ ]simplex0__1967_26.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__1968_7.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1969_15.min1.thm12017-02-06 12:46 419  
[ ]simplex0__1974_28.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__1975_65.min1.thm12017-02-06 12:46 906  
[ ]simplex0__1977_19.min1.thm12017-02-06 12:46 676  
[ ]simplex0__1978_18.min1.thm12017-02-06 12:46 716  
[ ]simplex0__1984_28.min1.thm12017-02-06 12:46 847  
[ ]simplex0__1992_11.min1.thm12017-02-06 12:46 191  
[ ]simplex0__1994_18.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__1998_34.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2000_55.min1.thm12017-02-06 12:46 413  
[ ]simplex0__2002_34.min1.thm12017-02-06 12:46 387  
[ ]simplex0__2002_34.min1.thm1.tptp2017-02-06 16:47 316  
[ ]simplex0__2003_34.min1.thm12017-02-06 12:46 618  
[ ]simplex0__2004_28.min1.thm12017-02-06 12:46 712  
[ ]simplex0__2005_46.min1.thm12017-02-06 12:46 951  
[ ]simplex0__2007_17.min1.thm12017-02-06 12:46 2.2K 
[ ]simplex0__2013_28.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2014_32.min1.thm12017-02-06 12:46 614  
[ ]simplex0__2016_23.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2017_27.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2018_41.min1.thm12017-02-06 12:46 404  
[ ]simplex0__2026_11.min1.thm12017-02-06 12:46 299  
[ ]simplex0__2028_18.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2031_40.min1.thm12017-02-06 12:46 462  
[ ]simplex0__2032_21.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__2033_18.min1.thm12017-02-06 12:46 2.2K 
[ ]simplex0__2045_27.min1.thm12017-02-06 12:46 621  
[ ]simplex0__2046_27.min1.thm12017-02-06 12:46 488  
[ ]simplex0__2047_11.min1.thm12017-02-06 12:46 191  
[ ]simplex0__2052_26.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2053_28.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2054_18.min1.thm12017-02-06 12:46 847  
[ ]simplex0__2063_11.min1.thm12017-02-06 12:46 191  
[ ]simplex0__2067_34.min1.thm12017-02-06 12:46 663  
[ ]simplex0__2070_25.min1.thm12017-02-06 12:46 383  
[ ]simplex0__2071_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2075_31.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2076_16.min1.thm12017-02-06 12:46 371  
[ ]simplex0__2077_32.min1.thm12017-02-06 12:46 654  
[ ]simplex0__2078_53.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2079_30.min1.thm12017-02-06 12:46 628  
[ ]simplex0__2082_47.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2090_34.min1.thm12017-02-06 12:46 499  
[ ]simplex0__2091_33.min1.thm12017-02-06 12:46 610  
[ ]simplex0__2092_28.min1.thm12017-02-06 12:46 694  
[ ]simplex0__2093_45.min1.thm12017-02-06 12:46 845  
[ ]simplex0__2094_17.min1.thm12017-02-06 12:46 742  
[ ]simplex0__2096_63.min1.thm12017-02-06 12:46 609  
[ ]simplex0__2096_63.min1.thm1.tptp2017-02-06 16:47 553  
[ ]simplex0__2097_34.min1.thm12017-02-06 12:46 964  
[ ]simplex0__2098_40.min1.thm12017-02-06 12:46 430  
[ ]simplex0__2099_69.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2101_19.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2114_33.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2118_7.min1.thm12017-02-06 12:46 234  
[ ]simplex0__2119_48.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__2122_28.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__2135_40.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2136_74.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2139_16.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2152_22.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2153_67.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__2154_13.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2155_40.min1.thm12017-02-06 12:46 861  
[ ]simplex0__2156_52.min1.thm12017-02-06 12:46 2.7K 
[ ]simplex0__2158_13.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__2169_73.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2171_14.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2181_39.min1.thm12017-02-06 12:46 499  
[ ]simplex0__2183_33.min1.thm12017-02-06 12:46 593  
[ ]simplex0__2184_11.min1.thm12017-02-06 12:46 203  
[ ]simplex0__2186_45.min1.thm12017-02-06 12:46 473  
[ ]simplex0__2189_15.min1.thm12017-02-06 12:46 528  
[ ]simplex0__2192_29.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2193_58.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__2198_12.min1.thm12017-02-06 12:46 447  
[ ]simplex0__2199_44.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2201_17.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__2202_15.min1.thm12017-02-06 12:46 528  
[ ]simplex0__2205_12.min1.thm12017-02-06 12:46 641  
[ ]simplex0__2206_35.min1.thm12017-02-06 12:46 904  
[ ]simplex0__2207_35.min1.thm12017-02-06 12:46 767  
[ ]simplex0__2221_30.min1.thm12017-02-06 12:46 466  
[ ]simplex0__2222_44.min1.thm12017-02-06 12:46 811  
[ ]simplex0__2223_65.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2225_2.min1.thm12017-02-06 12:46 908  
[ ]simplex0__2226_17.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2238_75.min1.thm12017-02-06 12:46 735  
[ ]simplex0__2240_27.min1.thm12017-02-06 12:46 529  
[ ]simplex0__2244_36.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2245_17.min1.thm12017-02-06 12:46 811  
[ ]simplex0__2246_48.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2247_43.min1.thm12017-02-06 12:46 811  
[ ]simplex0__2248_28.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2249_17.min1.thm12017-02-06 12:46 866  
[ ]simplex0__2257_34.min1.thm12017-02-06 12:46 932  
[ ]simplex0__2258_27.min1.thm12017-02-06 12:46 468  
[ ]simplex0__2258_27.min1.thm1.tptp2017-02-06 16:47 397  
[ ]simplex0__2260_8.min1.thm12017-02-06 12:46 932  
[ ]simplex0__2261_49.min1.thm12017-02-06 12:46 468  
[ ]simplex0__2261_49.min1.thm1.tptp2017-02-06 16:47 397  
[ ]simplex0__2262_17.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2274_14.min1.thm12017-02-06 12:46 455  
[ ]simplex0__2289_39.min1.thm12017-02-06 12:46 461  
[ ]simplex0__2303_23.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2304_62.min1.thm12017-02-06 12:46 760  
[ ]simplex0__2313_38.min1.thm12017-02-06 12:46 915  
[ ]simplex0__2314_21.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2317_16.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2318_48.min1.thm12017-02-06 12:46 764  
[ ]simplex0__2319_32.min1.thm12017-02-06 12:46 937  
[ ]simplex0__2320_33.min1.thm12017-02-06 12:46 864  
[ ]simplex0__2321_35.min1.thm12017-02-06 12:46 693  
[ ]simplex0__2322_11.min1.thm12017-02-06 12:46 311  
[ ]simplex0__2322_11.min1.thm1.tptp2017-02-06 16:47 225  
[ ]simplex0__2323_36.min1.thm12017-02-06 12:46 484  
[ ]simplex0__2324_22.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2325_26.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2326_17.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2332_11.min1.thm12017-02-06 12:46 259  
[ ]simplex0__2337_29.min1.thm12017-02-06 12:46 734  
[ ]simplex0__2340_62.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2341_18.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2344_23.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2345_18.min1.thm12017-02-06 12:46 549  
[ ]simplex0__2348_26.min1.thm12017-02-06 12:46 567  
[ ]simplex0__2349_12.min1.thm12017-02-06 12:46 195  
[ ]simplex0__2351_28.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2352_19.min1.thm12017-02-06 12:46 864  
[ ]simplex0__2355_50.min1.thm12017-02-06 12:46 772  
[ ]simplex0__2358_30.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2359_34.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2360_35.min1.thm12017-02-06 12:46 904  
[ ]simplex0__2361_50.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__2362_25.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2365_30.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2366_19.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2386_30.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2387_29.min1.thm12017-02-06 12:46 889  
[ ]simplex0__2388_19.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2394_44.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2395_17.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__2406_33.min1.thm12017-02-06 12:46 617  
[ ]simplex0__2410_46.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__2420_51.min1.thm12017-02-06 12:46 607  
[ ]simplex0__2424_22.min1.thm12017-02-06 12:46 861  
[ ]simplex0__2426_36.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2428_28.min1.thm12017-02-06 12:46 949  
[ ]simplex0__2429_34.min1.thm12017-02-06 12:46 949  
[ ]simplex0__2430_29.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2432_51.min1.thm12017-02-06 12:46 898  
[ ]simplex0__2442_61.min1.thm12017-02-06 12:46 404  
[ ]simplex0__2443_44.min1.thm12017-02-06 12:46 764  
[ ]simplex0__2444_75.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2446_55.min1.thm12017-02-06 12:46 845  
[ ]simplex0__2447_60.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2448_17.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2458_30.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2459_15.min1.thm12017-02-06 12:46 827  
[ ]simplex0__2460_35.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2461_15.min1.thm12017-02-06 12:46 827  
[ ]simplex0__2462_35.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2463_26.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2464_29.min1.thm12017-02-06 12:46 846  
[ ]simplex0__2465_12.min1.thm12017-02-06 12:46 937  
[ ]simplex0__2466_17.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2478_35.min1.thm12017-02-06 12:46 465  
[ ]simplex0__2480_35.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__2483_21.min1.thm12017-02-06 12:46 933  
[ ]simplex0__2484_49.min1.thm12017-02-06 12:46 921  
[ ]simplex0__2485_14.min1.thm12017-02-06 12:46 490  
[ ]simplex0__2487_41.min1.thm12017-02-06 12:46 787  
[ ]simplex0__2491_13.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2507_17.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2517_20.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2518_63.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2519_46.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2521_17.min1.thm12017-02-06 12:46 940  
[ ]simplex0__2533_17.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2544_48.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2545_14.min1.thm12017-02-06 12:46 517  
[ ]simplex0__2547_40.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2549_12.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2550_17.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__2558_26.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2560_25.min1.thm12017-02-06 12:46 459  
[ ]simplex0__2561_69.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2563_30.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2572_34.min1.thm12017-02-06 12:46 769  
[ ]simplex0__2573_38.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2576_14.min1.thm12017-02-06 12:46 763  
[ ]simplex0__2590_14.min1.thm12017-02-06 12:46 465  
[ ]simplex0__2602_70.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2604_49.min1.thm12017-02-06 12:46 485  
[ ]simplex0__2604_49.min1.thm1.tptp2017-02-06 16:47 414  
[ ]simplex0__2608_24.min1.thm12017-02-06 12:46 887  
[ ]simplex0__2609_18.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2610_17.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2617_30.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2625_40.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__2626_27.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2627_27.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2641_69.min1.thm12017-02-06 12:46 895  
[ ]simplex0__2643_48.min1.thm12017-02-06 12:46 481  
[ ]simplex0__2643_48.min1.thm1.tptp2017-02-06 16:47 410  
[ ]simplex0__2644_45.min1.thm12017-02-06 12:46 472  
[ ]simplex0__2648_28.min1.thm12017-02-06 12:46 853  
[ ]simplex0__2649_20.min1.thm12017-02-06 12:46 448  
[ ]simplex0__2661_36.min1.thm12017-02-06 12:46 354  
[ ]simplex0__2661_36.min1.thm1.tptp2017-02-06 16:47 285  
[ ]simplex0__2663_68.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2675_11.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2678_54.min1.thm12017-02-06 12:46 2.2K 
[ ]simplex0__2684_32.min1.thm12017-02-06 12:46 722  
[ ]simplex0__2686_27.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__2687_31.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__2688_29.min1.thm12017-02-06 12:46 845  
[ ]simplex0__2689_18.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2692_57.min1.thm12017-02-06 12:46 699  
[ ]simplex0__2692_57.min1.thm1.tptp2017-02-06 16:47 621  
[ ]simplex0__2710_18.min1.thm12017-02-06 12:46 861  
[ ]simplex0__2712_35.min1.thm12017-02-06 12:46 471  
[ ]simplex0__2725_44.min1.thm12017-02-06 12:46 499  
[ ]simplex0__2728_54.min1.thm12017-02-06 12:46 506  
[ ]simplex0__2730_33.min1.thm12017-02-06 12:46 379  
[ ]simplex0__2730_33.min1.thm1.tptp2017-02-06 16:47 308  
[ ]simplex0__2732_16.min1.thm12017-02-06 12:46 312  
[ ]simplex0__2732_16.min1.thm1.tptp2017-02-06 16:47 235  
[ ]simplex0__2735_25.min1.thm12017-02-06 12:46 874  
[ ]simplex0__2736_23.min1.thm12017-02-06 12:46 523  
[ ]simplex0__2737_32.min1.thm12017-02-06 12:46 546  
[ ]simplex0__2738_11.min1.thm12017-02-06 12:46 351  
[ ]simplex0__2738_11.min1.thm1.tptp2017-02-06 16:47 273  
[ ]simplex0__2739_35.min1.thm12017-02-06 12:46 829  
[ ]simplex0__2740_70.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2743_56.min1.thm12017-02-06 12:46 850  
[ ]simplex0__2751_11.min1.thm12017-02-06 12:46 428  
[ ]simplex0__2753_51.min1.thm12017-02-06 12:46 901  
[ ]simplex0__2754_38.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2755_18.min1.thm12017-02-06 12:46 651  
[ ]simplex0__2758_41.min1.thm12017-02-06 12:46 650  
[ ]simplex0__2766_34.min1.thm12017-02-06 12:46 861  
[ ]simplex0__2767_42.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__2768_22.min1.thm12017-02-06 12:46 958  
[ ]simplex0__2769_30.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2770_41.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2771_23.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2780_29.min1.thm12017-02-06 12:46 492  
[ ]simplex0__2783_27.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2784_18.min1.thm12017-02-06 12:46 917  
[ ]simplex0__2795_45.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__2798_33.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2801_42.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2803_21.min1.thm12017-02-06 12:46 496  
[ ]simplex0__2803_21.min1.thm1.tptp2017-02-06 16:47 419  
[ ]simplex0__2804_23.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2813_11.min1.thm12017-02-06 12:46 194  
[ ]simplex0__2815_18.min1.thm12017-02-06 12:46 760  
[ ]simplex0__2819_46.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__2828_41.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2829_32.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__2830_22.min1.thm12017-02-06 12:46 473  
[ ]simplex0__2830_22.min1.thm1.tptp2017-02-06 16:47 396  
[ ]simplex0__2831_23.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2834_46.min1.thm12017-02-06 12:46 627  
[ ]simplex0__2835_32.min1.thm12017-02-06 12:46 508  
[ ]simplex0__2848_14.min1.thm12017-02-06 12:46 369  
[ ]simplex0__2849_26.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2850_57.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2851_49.min1.thm12017-02-06 12:46 838  
[ ]simplex0__2857_48.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2858_40.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2861_34.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2862_69.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2868_17.min1.thm12017-02-06 12:46 817  
[ ]simplex0__2870_38.min1.thm12017-02-06 12:46 499  
[ ]simplex0__2883_45.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__2884_11.min1.thm12017-02-06 12:46 194  
[ ]simplex0__2886_15.min1.thm12017-02-06 12:46 791  
[ ]simplex0__2888_50.min1.thm12017-02-06 12:46 490  
[ ]simplex0__2891_25.min1.thm12017-02-06 12:46 388  
[ ]simplex0__2891_25.min1.thm1.tptp2017-02-06 16:47 319  
[ ]simplex0__2892_23.min1.thm12017-02-06 12:46 2.2K 
[ ]simplex0__2895_21.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__2896_31.min1.thm12017-02-06 12:46 797  
[ ]simplex0__2897_46.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2899_26.min1.thm12017-02-06 12:46 899  
[ ]simplex0__2900_19.min1.thm12017-02-06 12:46 873  
[ ]simplex0__2905_18.min1.thm12017-02-06 12:46 744  
[ ]simplex0__2906_29.min1.thm12017-02-06 12:46 956  
[ ]simplex0__2907_28.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2910_22.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__2911_27.min1.thm12017-02-06 12:46 843  
[ ]simplex0__2912_36.min1.thm12017-02-06 12:46 798  
[ ]simplex0__2913_46.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2915_26.min1.thm12017-02-06 12:46 899  
[ ]simplex0__2916_19.min1.thm12017-02-06 12:46 873  
[ ]simplex0__2920_40.min1.thm12017-02-06 12:46 501  
[ ]simplex0__2923_29.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2924_42.min1.thm12017-02-06 12:46 947  
[ ]simplex0__2926_22.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2927_32.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__2930_21.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__2931_26.min1.thm12017-02-06 12:46 779  
[ ]simplex0__2932_35.min1.thm12017-02-06 12:46 771  
[ ]simplex0__2933_45.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2935_25.min1.thm12017-02-06 12:46 856  
[ ]simplex0__2936_18.min1.thm12017-02-06 12:46 857  
[ ]simplex0__2948_42.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2951_13.min1.thm12017-02-06 12:46 695  
[ ]simplex0__2952_18.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2958_17.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__2959_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2961_17.min1.thm12017-02-06 12:46 2.3K 
[ ]simplex0__2963_13.min1.thm12017-02-06 12:46 132  
[ ]simplex0__2972_17.min1.thm12017-02-06 12:46 427  
[ ]simplex0__2972_17.min1.thm1.tptp2017-02-06 16:47 345  
[ ]simplex0__2973_21.min1.thm12017-02-06 12:46 2.7K 
[ ]simplex0__2974_6.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__2975_14.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2984_23.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__2985_14.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__2986_14.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__2987_18.min1.thm12017-02-06 12:46 470  
[ ]simplex0__2988_14.min1.thm12017-02-06 12:46 452  
[ ]simplex0__2995_23.min1.thm12017-02-06 12:46 750  
[ ]simplex0__2997_32.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3013_67.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3015_29.min1.thm12017-02-06 12:46 841  
[ ]simplex0__3016_40.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3017_27.min1.thm12017-02-06 12:46 624  
[ ]simplex0__3018_14.min1.thm12017-02-06 12:46 486  
[ ]simplex0__3020_20.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3021_21.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3022_11.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3023_25.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__3024_17.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3028_26.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3029_12.min1.thm12017-02-06 12:46 236  
[ ]simplex0__3031_22.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__3035_22.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3040_12.min1.thm12017-02-06 12:46 360  
[ ]simplex0__3042_22.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__3046_22.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__3062_11.min1.thm12017-02-06 12:46 222  
[ ]simplex0__3066_7.min1.thm12017-02-06 12:46 2.1K 
[ ]simplex0__3068_17.min1.thm12017-02-06 12:46 860  
[ ]simplex0__3071_25.min1.thm12017-02-06 12:46 3.3K 
[ ]simplex0__3072_25.min1.thm12017-02-06 12:46 2.2K 
[ ]simplex0__3074_17.min1.thm12017-02-06 12:46 325  
[ ]simplex0__3074_17.min1.thm1.tptp2017-02-06 16:47 248  
[ ]simplex0__3075_38.min1.thm12017-02-06 12:46 563  
[ ]simplex0__3078_38.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3081_26.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3084_17.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3097_27.min1.thm12017-02-06 12:46 283  
[ ]simplex0__3097_27.min1.thm1.tptp2017-02-06 16:47 202  
[ ]simplex0__3099_29.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3100_19.min1.thm12017-02-06 12:46 2.6K 
[ ]simplex0__3102_35.min1.thm12017-02-06 12:46 324  
[ ]simplex0__3103_15.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3104_18.min1.thm12017-02-06 12:46 3.2K 
[ ]simplex0__3108_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3110_14.min1.thm12017-02-06 12:46 279  
[ ]simplex0__3111_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3112_21.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__3113_10.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3118_42.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3121_10.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3144_15.min1.thm12017-02-06 12:46 770  
[ ]simplex0__3146_43.min1.thm12017-02-06 12:46 595  
[ ]simplex0__3149_59.min1.thm12017-02-06 12:46 908  
[ ]simplex0__3151_17.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3154_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3156_13.min1.thm12017-02-06 12:46 649  
[ ]simplex0__3160_17.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3173_39.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3174_37.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3175_24.min1.thm12017-02-06 12:46 895  
[ ]simplex0__3177_2.min1.thm12017-02-06 12:46 904  
[ ]simplex0__3178_29.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3179_36.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3182_38.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3183_36.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3184_23.min1.thm12017-02-06 12:46 881  
[ ]simplex0__3185_78.min1.thm12017-02-06 12:46 892  
[ ]simplex0__3187_28.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3188_35.min1.thm12017-02-06 12:46 970  
[ ]simplex0__3202_11.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3204_34.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3205_47.min1.thm12017-02-06 12:46 693  
[ ]simplex0__3206_35.min1.thm12017-02-06 12:46 891  
[ ]simplex0__3214_23.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3224_16.min1.thm12017-02-06 12:46 435  
[ ]simplex0__3235_17.min1.thm12017-02-06 12:46 718  
[ ]simplex0__3237_19.min1.thm12017-02-06 12:46 556  
[ ]simplex0__3237_19.min1.thm1.tptp2017-02-06 16:47 479  
[ ]simplex0__3246_18.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__3250_18.min1.thm12017-02-06 12:46 547  
[ ]simplex0__3252_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3256_37.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3257_22.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3260_14.min1.thm12017-02-06 12:46 711  
[ ]simplex0__3273_54.min1.thm12017-02-06 12:46 923  
[ ]simplex0__3275_33.min1.thm12017-02-06 12:46 483  
[ ]simplex0__3275_33.min1.thm1.tptp2017-02-06 16:47 412  
[ ]simplex0__3276_36.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3280_28.min1.thm12017-02-06 12:46 934  
[ ]simplex0__3282_23.min1.thm12017-02-06 12:46 498  
[ ]simplex0__3282_23.min1.thm1.tptp2017-02-06 16:47 421  
[ ]simplex0__3283_15.min1.thm12017-02-06 12:46 886  
[ ]simplex0__3284_33.min1.thm12017-02-06 12:46 892  
[ ]simplex0__3285_22.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3286_33.min1.thm12017-02-06 12:46 758  
[ ]simplex0__3295_11.min1.thm12017-02-06 12:46 305  
[ ]simplex0__3297_46.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3298_15.min1.thm12017-02-06 12:46 2.5K 
[ ]simplex0__3302_46.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3303_18.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__3306_41.min1.thm12017-02-06 12:46 568  
[ ]simplex0__3307_30.min1.thm12017-02-06 12:46 714  
[ ]simplex0__3317_28.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__3318_31.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__3319_17.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3321_8.min1.thm12017-02-06 12:46 2.5K 
[ ]simplex0__3323_52.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3325_39.min1.thm12017-02-06 12:46 778  
[ ]simplex0__3327_13.min1.thm12017-02-06 12:46 212  
[ ]simplex0__3329_17.min1.thm12017-02-06 12:46 2.4K 
[ ]simplex0__3330_26.min1.thm12017-02-06 12:46 3.4K 
[ ]simplex0__3334_44.min1.thm12017-02-06 12:46 660  
[ ]simplex0__3334_44.min1.thm1.tptp2017-02-06 16:47 582  
[ ]simplex0__3335_22.min1.thm12017-02-06 12:46 834  
[ ]simplex0__3336_37.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3338_42.min1.thm12017-02-06 12:46 347  
[ ]simplex0__3338_42.min1.thm1.tptp2017-02-06 16:47 264  
[ ]simplex0__3339_41.min1.thm12017-02-06 12:46 881  
[ ]simplex0__3340_45.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__3341_20.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__3342_26.min1.thm12017-02-06 12:46 866  
[ ]simplex0__3343_25.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3344_24.min1.thm12017-02-06 12:46 951  
[ ]simplex0__3360_11.min1.thm12017-02-06 12:46 194  
[ ]simplex0__3365_29.min1.thm12017-02-06 12:46 492  
[ ]simplex0__3368_27.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3369_18.min1.thm12017-02-06 12:46 944  
[ ]simplex0__3372_41.min1.thm12017-02-06 12:46 533  
[ ]simplex0__3373_30.min1.thm12017-02-06 12:46 679  
[ ]simplex0__3382_13.min1.thm12017-02-06 12:46 384  
[ ]simplex0__3384_25.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3385_17.min1.thm12017-02-06 12:46 971  
[ ]simplex0__3388_51.min1.thm12017-02-06 12:46 882  
[ ]simplex0__3389_24.min1.thm12017-02-06 12:46 752  
[ ]simplex0__3390_40.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3391_33.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3392_36.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3393_42.min1.thm12017-02-06 12:46 760  
[ ]simplex0__3394_43.min1.thm12017-02-06 12:46 604  
[ ]simplex0__3395_50.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3396_22.min1.thm12017-02-06 12:46 625  
[ ]simplex0__3397_26.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__3398_31.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3399_44.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__3401_31.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__3403_20.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3431_52.min1.thm12017-02-06 12:46 675  
[ ]simplex0__3436_41.min1.thm12017-02-06 12:46 654  
[ ]simplex0__3437_41.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3442_36.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3443_23.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3452_37.min1.thm12017-02-06 12:46 696  
[ ]simplex0__3453_24.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3454_19.min1.thm12017-02-06 12:46 875  
[ ]simplex0__3456_21.min1.thm12017-02-06 12:46 518  
[ ]simplex0__3457_18.min1.thm12017-02-06 12:46 936  
[ ]simplex0__3468_36.min1.thm12017-02-06 12:46 1.9K 
[ ]simplex0__3469_37.min1.thm12017-02-06 12:46 2.3K 
[ ]simplex0__3471_17.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3489_28.min1.thm12017-02-06 12:46 737  
[ ]simplex0__3493_20.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3500_34.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3501_31.min1.thm12017-02-06 12:46 564  
[ ]simplex0__3502_20.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3508_36.min1.thm12017-02-06 12:46 604  
[ ]simplex0__3509_48.min1.thm12017-02-06 12:46 729  
[ ]simplex0__3514_28.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3515_19.min1.thm12017-02-06 12:46 561  
[ ]simplex0__3517_27.min1.thm12017-02-06 12:46 576  
[ ]simplex0__3519_31.min1.thm12017-02-06 12:46 831  
[ ]simplex0__3524_32.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3525_19.min1.thm12017-02-06 12:46 970  
[ ]simplex0__3527_65.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__3529_24.min1.thm12017-02-06 12:46 600  
[ ]simplex0__3531_15.min1.thm12017-02-06 12:46 737  
[ ]simplex0__3531_15.min1.thm1.tptp2017-02-06 16:47 660  
[ ]simplex0__3533_11.min1.thm12017-02-06 12:46 599  
[ ]simplex0__3535_24.min1.thm12017-02-06 12:46 820  
[ ]simplex0__3536_17.min1.thm12017-02-06 12:46 553  
[ ]simplex0__3537_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3540_54.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3541_16.min1.thm12017-02-06 12:46 574  
[ ]simplex0__3542_11.min1.thm12017-02-06 12:46 674  
[ ]simplex0__3543_15.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3544_15.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3545_41.min1.thm12017-02-06 12:46 574  
[ ]simplex0__3546_41.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__3548_17.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3549_18.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3552_31.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3556_40.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3560_42.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3565_18.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__3575_26.min1.thm12017-02-06 12:46 555  
[ ]simplex0__3577_16.min1.thm12017-02-06 12:46 351  
[ ]simplex0__3577_16.min1.thm1.tptp2017-02-06 16:47 277  
[ ]simplex0__3578_36.min1.thm12017-02-06 12:46 685  
[ ]simplex0__3579_19.min1.thm12017-02-06 12:46 669  
[ ]simplex0__3580_20.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3581_24.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3584_41.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3585_16.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3586_40.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3589_13.min1.thm12017-02-06 12:46 695  
[ ]simplex0__3592_45.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3593_29.min1.thm12017-02-06 12:46 716  
[ ]simplex0__3593_29.min1.thm1.tptp2017-02-06 16:47 645  
[ ]simplex0__3597_29.min1.thm12017-02-06 12:46 1.8K 
[ ]simplex0__3600_17.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3610_34.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3616_42.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3617_36.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3624_39.min1.thm12017-02-06 12:46 878  
[ ]simplex0__3625_13.min1.thm12017-02-06 12:46 870  
[ ]simplex0__3626_29.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3627_39.min1.thm12017-02-06 12:46 724  
[ ]simplex0__3628_17.min1.thm12017-02-06 12:46 881  
[ ]simplex0__3629_44.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3632_35.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3635_31.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3636_29.min1.thm12017-02-06 12:46 825  
[ ]simplex0__3639_18.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3641_32.min1.thm12017-02-06 12:46 640  
[ ]simplex0__3643_49.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3644_17.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__3654_20.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3655_24.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3658_41.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3661_20.min1.thm12017-02-06 12:46 736  
[ ]simplex0__3663_59.min1.thm12017-02-06 12:46 2.2K 
[ ]simplex0__3664_19.min1.thm12017-02-06 12:46 558  
[ ]simplex0__3665_37.min1.thm12017-02-06 12:46 874  
[ ]simplex0__3666_16.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3667_38.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3675_21.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3676_24.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3677_11.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3678_21.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3682_20.min1.thm12017-02-06 12:46 832  
[ ]simplex0__3684_17.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3691_45.min1.thm12017-02-06 12:46 699  
[ ]simplex0__3694_34.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3700_42.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3708_35.min1.thm12017-02-06 12:46 656  
[ ]simplex0__3709_24.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3710_19.min1.thm12017-02-06 12:46 807  
[ ]simplex0__3712_38.min1.thm12017-02-06 12:46 721  
[ ]simplex0__3714_20.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3718_44.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3719_17.min1.thm12017-02-06 12:46 2.2K 
[ ]simplex0__3727_22.min1.thm12017-02-06 12:46 774  
[ ]simplex0__3728_20.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3729_24.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3732_41.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__3733_16.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3737_26.min1.thm12017-02-06 12:46 512  
[ ]simplex0__3743_39.min1.thm12017-02-06 12:46 716  
[ ]simplex0__3744_23.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3745_38.min1.thm12017-02-06 12:46 965  
[ ]simplex0__3746_45.min1.thm12017-02-06 12:46 776  
[ ]simplex0__3747_18.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3750_17.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3759_73.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3765_42.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3768_23.min1.thm12017-02-06 12:46 820  
[ ]simplex0__3769_45.min1.thm12017-02-06 12:46 662  
[ ]simplex0__3770_20.min1.thm12017-02-06 12:46 716  
[ ]simplex0__3777_22.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3778_19.min1.thm12017-02-06 12:46 1.5K 
[ ]simplex0__3780_17.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3783_27.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3784_16.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3796_34.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3801_38.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3803_23.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3808_28.min1.thm12017-02-06 12:46 769  
[ ]simplex0__3811_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3817_38.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3819_23.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3824_28.min1.thm12017-02-06 12:46 769  
[ ]simplex0__3827_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3848_12.min1.thm12017-02-06 12:46 397  
[ ]simplex0__3853_20.min1.thm12017-02-06 12:46 434  
[ ]simplex0__3855_33.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3859_47.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3865_18.min1.thm12017-02-06 12:46 751  
[ ]simplex0__3865_18.min1.thm1.tptp2017-02-06 16:47 698  
[ ]simplex0__3879_35.min1.thm12017-02-06 12:46 744  
[ ]simplex0__3884_37.min1.thm12017-02-06 12:46 891  
[ ]simplex0__3887_50.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3903_54.min1.thm12017-02-06 12:46 961  
[ ]simplex0__3904_32.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3917_29.min1.thm12017-02-06 12:46 476  
[ ]simplex0__3918_12.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3921_18.min1.thm12017-02-06 12:46 810  
[ ]simplex0__3927_32.min1.thm12017-02-06 12:46 966  
[ ]simplex0__3927_32.min1.thm1.tptp2017-02-06 16:47 938  
[ ]simplex0__3928_63.min1.thm12017-02-06 12:46 914  
[ ]simplex0__3930_18.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3935_18.min1.thm12017-02-06 12:46 435  
[ ]simplex0__3936_21.min1.thm12017-02-06 12:46 856  
[ ]simplex0__3946_20.min1.thm12017-02-06 12:46 947  
[ ]simplex0__3947_63.min1.thm12017-02-06 12:46 890  
[ ]simplex0__3948_19.min1.thm12017-02-06 12:46 400  
[ ]simplex0__3949_10.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__3949_10.min1.thm1.tptp2017-02-06 16:47 1.2K 
[ ]simplex0__3952_20.min1.thm12017-02-06 12:46 867  
[ ]simplex0__3953_63.min1.thm12017-02-06 12:46 892  
[ ]simplex0__3954_37.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3955_12.min1.thm12017-02-06 12:46 1.1K 
[ ]simplex0__3957_50.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__3958_19.min1.thm12017-02-06 12:46 3.6K 
[ ]simplex0__3961_57.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3962_20.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__3963_53.min1.thm12017-02-06 12:46 2.3K 
[ ]simplex0__3967_11.min1.thm12017-02-06 12:46 1.0K 
[ ]simplex0__3970_17.min1.thm12017-02-06 12:46 1.4K 
[ ]simplex0__3976_36.min1.thm12017-02-06 12:46 940  
[ ]simplex0__3976_36.min1.thm1.tptp2017-02-06 16:47 912  
[ ]simplex0__3977_55.min1.thm12017-02-06 12:46 542  
[ ]simplex0__3979_17.min1.thm12017-02-06 12:46 859  
[ ]simplex0__3980_14.min1.thm12017-02-06 12:46 384  
[ ]simplex0__4006_20.min1.thm12017-02-06 12:46 484  
[ ]simplex0__4007_33.min1.thm12017-02-06 12:46 817  
[ ]simplex0__4008_18.min1.thm12017-02-06 12:46 1.6K 
[ ]simplex0__4010_22.min1.thm12017-02-06 12:46 594  
[ ]simplex0__4012_17.min1.thm12017-02-06 12:46 674  
[ ]simplex0__4022_14.min1.thm12017-02-06 12:46 649  
[ ]simplex0__4034_30.min1.thm12017-02-06 12:46 809  
[ ]simplex0__4035_17.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__4064_19.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__4082_19.min1.thm12017-02-06 12:46 1.2K 
[ ]simplex0__4084_18.min1.thm12017-02-06 12:46 1.3K 
[ ]simplex0__4086_22.min1.thm12017-02-06 12:46 608  
[ ]simplex0__4101_14.min1.thm12017-02-06 12:46 384  
[ ]simplex0__4102_73.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__4107_21.min1.thm12017-02-06 12:46 568  
[ ]simplex0__4109_14.min1.thm12017-02-06 12:46 486  
[ ]simplex0__4109_14.min1.thm1.tptp2017-02-06 16:47 409  
[ ]simplex0__4122_48.min1.thm12017-02-06 12:46 558  
[ ]simplex0__4123_18.min1.thm12017-02-06 12:46 384  
[ ]simplex0__4124_56.min1.thm12017-02-06 12:46 2.0K 
[ ]simplex0__4126_64.min1.thm12017-02-06 12:46 1.7K 
[ ]simplex0__4130_27.min1.thm12017-02-06 12:46 795  
[ ]simplex0__4131_18.min1.thm12017-02-06 12:46 861  
[ ]simplex0__4133_14.min1.thm12017-02-06 12:46 610  
[ ]simplex0__4133_14.min1.thm1.tptp2017-02-06 16:47 529  
Apache/2.4.18 (Ubuntu) Server at grid01.ciirc.cvut.cz Port 80