Index of /~mptp/7.13.01_4.181.1147/MPTP2/ilp0/lattice5

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[ ]lattice5__63_34.min1.thm12017-02-06 12:45 948  
[ ]lattice5__66_17.min1.thm12017-02-06 12:45 732  
[ ]lattice5__69_14.min1.thm12017-02-06 12:45 618  
[ ]lattice5__70_22.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__72_31.min1.thm12017-02-06 12:45 769  
[ ]lattice5__74_27.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__75_19.min1.thm12017-02-06 12:45 596  
[ ]lattice5__81_22.min1.thm12017-02-06 12:45 453  
[ ]lattice5__81_22.min1.thm1.tptp2017-02-06 16:47 398  
[ ]lattice5__84_22.min1.thm12017-02-06 12:45 774  
[ ]lattice5__85_18.min1.thm12017-02-06 12:45 528  
[ ]lattice5__87_20.min1.thm12017-02-06 12:45 598  
[ ]lattice5__89_12.min1.thm12017-02-06 12:45 486  
[ ]lattice5__89_12.min1.thm1.tptp2017-02-06 16:47 425  
[ ]lattice5__90_18.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__91_24.min1.thm12017-02-06 12:45 947  
[ ]lattice5__92_22.min1.thm12017-02-06 12:45 887  
[ ]lattice5__109_16.min1.thm12017-02-06 12:45 670  
[ ]lattice5__110_19.min1.thm12017-02-06 12:45 640  
[ ]lattice5__113_14.min1.thm12017-02-06 12:45 409  
[ ]lattice5__113_14.min1.thm1.tptp2017-02-06 16:47 354  
[ ]lattice5__114_19.min1.thm12017-02-06 12:45 640  
[ ]lattice5__117_14.min1.thm12017-02-06 12:45 409  
[ ]lattice5__117_14.min1.thm1.tptp2017-02-06 16:47 354  
[ ]lattice5__118_36.min1.thm12017-02-06 12:45 325  
[ ]lattice5__118_36.min1.thm1.tptp2017-02-06 16:47 247  
[ ]lattice5__119_36.min1.thm12017-02-06 12:45 326  
[ ]lattice5__119_36.min1.thm1.tptp2017-02-06 16:47 248  
[ ]lattice5__122_19.min1.thm12017-02-06 12:45 588  
[ ]lattice5__128_13.min1.thm12017-02-06 12:45 463  
[ ]lattice5__128_13.min1.thm1.tptp2017-02-06 16:47 408  
[ ]lattice5__136_32.min1.thm12017-02-06 12:45 859  
[ ]lattice5__155_13.min1.thm12017-02-06 12:45 441  
[ ]lattice5__155_13.min1.thm1.tptp2017-02-06 16:47 386  
[ ]lattice5__159_13.min1.thm12017-02-06 12:45 763  
[ ]lattice5__160_28.min1.thm12017-02-06 12:45 682  
[ ]lattice5__161_16.min1.thm12017-02-06 12:45 399  
[ ]lattice5__161_16.min1.thm1.tptp2017-02-06 16:47 325  
[ ]lattice5__164_18.min1.thm12017-02-06 12:45 795  
[ ]lattice5__165_27.min1.thm12017-02-06 12:45 484  
[ ]lattice5__165_27.min1.thm1.tptp2017-02-06 16:47 413  
[ ]lattice5__170_18.min1.thm12017-02-06 12:45 795  
[ ]lattice5__171_27.min1.thm12017-02-06 12:45 484  
[ ]lattice5__171_27.min1.thm1.tptp2017-02-06 16:47 413  
[ ]lattice5__179_56.min1.thm12017-02-06 12:45 647  
[ ]lattice5__180_16.min1.thm12017-02-06 12:45 703  
[ ]lattice5__182_28.min1.thm12017-02-06 12:45 423  
[ ]lattice5__182_28.min1.thm1.tptp2017-02-06 16:47 345  
[ ]lattice5__183_27.min1.thm12017-02-06 12:45 548  
[ ]lattice5__195_13.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__201_11.min1.thm12017-02-06 12:45 731  
[ ]lattice5__211_61.min1.thm12017-02-06 12:45 465  
[ ]lattice5__212_10.min1.thm12017-02-06 12:45 654  
[ ]lattice5__214_35.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__219_8.min1.thm12017-02-06 12:45 827  
[ ]lattice5__220_40.min1.thm12017-02-06 12:45 584  
[ ]lattice5__225_41.min1.thm12017-02-06 12:45 769  
[ ]lattice5__226_49.min1.thm12017-02-06 12:45 368  
[ ]lattice5__226_49.min1.thm1.tptp2017-02-06 16:47 290  
[ ]lattice5__228_33.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__229_14.min1.thm12017-02-06 12:45 498  
[ ]lattice5__236_58.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__253_19.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__255_19.min1.thm12017-02-06 12:45 807  
[ ]lattice5__261_22.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__262_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__275_10.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__277_10.min1.thm12017-02-06 12:45 555  
[ ]lattice5__280_10.min1.thm12017-02-06 12:45 555  
[ ]lattice5__285_10.min1.thm12017-02-06 12:45 565  
[ ]lattice5__301_53.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__302_53.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__306_54.min1.thm12017-02-06 12:45 394  
[ ]lattice5__306_54.min1.thm1.tptp2017-02-06 16:47 311  
[ ]lattice5__307_54.min1.thm12017-02-06 12:45 394  
[ ]lattice5__307_54.min1.thm1.tptp2017-02-06 16:47 311  
[ ]lattice5__310_25.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__311_30.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__312_16.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__322_10.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__334_15.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__336_13.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__337_15.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__338_18.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__355_54.min1.thm12017-02-06 12:45 394  
[ ]lattice5__355_54.min1.thm1.tptp2017-02-06 16:47 311  
[ ]lattice5__356_54.min1.thm12017-02-06 12:45 394  
[ ]lattice5__356_54.min1.thm1.tptp2017-02-06 16:47 311  
[ ]lattice5__359_25.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__360_30.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__380_64.min1.thm12017-02-06 12:45 848  
[ ]lattice5__392_64.min1.thm12017-02-06 12:45 879  
[ ]lattice5__393_25.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__395_23.min1.thm12017-02-06 12:45 786  
[ ]lattice5__399_17.min1.thm12017-02-06 12:45 908  
[ ]lattice5__400_21.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__411_60.min1.thm12017-02-06 12:45 693  
[ ]lattice5__412_18.min1.thm12017-02-06 12:45 738  
[ ]lattice5__416_62.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__427_62.min1.thm12017-02-06 12:45 701  
[ ]lattice5__428_23.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__430_21.min1.thm12017-02-06 12:45 678  
[ ]lattice5__434_15.min1.thm12017-02-06 12:45 726  
[ ]lattice5__435_19.min1.thm12017-02-06 12:45 968  
[ ]lattice5__451_18.min1.thm12017-02-06 12:45 721  
[ ]lattice5__453_49.min1.thm12017-02-06 12:45 803  
[ ]lattice5__455_20.min1.thm12017-02-06 12:45 821  
[ ]lattice5__466_23.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__468_25.min1.thm12017-02-06 12:45 596  
[ ]lattice5__473_33.min1.thm12017-02-06 12:45 349  
[ ]lattice5__474_30.min1.thm12017-02-06 12:45 694  
[ ]lattice5__494_25.min1.thm12017-02-06 12:45 684  
[ ]lattice5__511_23.min1.thm12017-02-06 12:45 971  
[ ]lattice5__513_25.min1.thm12017-02-06 12:45 647  
[ ]lattice5__517_53.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__519_45.min1.thm12017-02-06 12:45 802  
[ ]lattice5__524_52.min1.thm12017-02-06 12:45 669  
[ ]lattice5__524_52.min1.thm1.tptp2017-02-06 16:47 583  
[ ]lattice5__537_52.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__555_23.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__577_22.min1.thm12017-02-06 12:45 850  
[ ]lattice5__586_22.min1.thm12017-02-06 12:45 850  
[ ]lattice5__614_22.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__615_32.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__616_15.min1.thm12017-02-06 12:45 850  
[ ]lattice5__617_21.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__627_14.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__630_12.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__643_22.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__644_32.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__645_15.min1.thm12017-02-06 12:45 850  
[ ]lattice5__646_21.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__664_31.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__665_32.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__676_16.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__679_16.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__680_51.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__681_58.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__699_16.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__702_16.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__703_51.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__704_58.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__711_19.min1.thm12017-02-06 12:45 2.3K 
[ ]lattice5__741_21.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__743_14.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__753_32.min1.thm12017-02-06 12:45 3.6K 
[ ]lattice5__755_27.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__759_15.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__760_25.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__762_16.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__764_21.min1.thm12017-02-06 12:45 944  
[ ]lattice5__768_32.min1.thm12017-02-06 12:45 3.6K 
[ ]lattice5__770_27.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__774_15.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__775_25.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__777_16.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__779_21.min1.thm12017-02-06 12:45 944  
[ ]lattice5__781_19.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__783_20.min1.thm12017-02-06 12:45 954  
[ ]lattice5__791_62.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__809_20.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__810_14.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__813_21.min1.thm12017-02-06 12:45 867  
[ ]lattice5__814_22.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__815_42.min1.thm12017-02-06 12:45 938  
[ ]lattice5__816_45.min1.thm12017-02-06 12:45 924  
[ ]lattice5__818_12.min1.thm12017-02-06 12:45 879  
[ ]lattice5__820_17.min1.thm12017-02-06 12:45 860  
[ ]lattice5__825_33.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__828_22.min1.thm12017-02-06 12:45 888  
[ ]lattice5__831_17.min1.thm12017-02-06 12:45 888  
[ ]lattice5__832_24.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__834_15.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__837_15.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__839_27.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__849_41.min1.thm12017-02-06 12:45 3.6K 
[ ]lattice5__859_28.min1.thm12017-02-06 12:45 964  
[ ]lattice5__863_19.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__864_25.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__872_31.min1.thm12017-02-06 12:45 2.8K 
[ ]lattice5__874_41.min1.thm12017-02-06 12:45 3.1K 
[ ]lattice5__879_20.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__884_21.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__891_25.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__899_39.min1.thm12017-02-06 12:45 3.6K 
[ ]lattice5__909_26.min1.thm12017-02-06 12:45 960  
[ ]lattice5__913_17.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__914_23.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__922_29.min1.thm12017-02-06 12:45 2.8K 
[ ]lattice5__924_39.min1.thm12017-02-06 12:45 3.1K 
[ ]lattice5__929_18.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__934_19.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__941_23.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__947_19.min1.thm12017-02-06 12:45 722  
[ ]lattice5__976_19.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__976_19.min1.thm1.tptp2017-02-06 16:47 941  
[ ]lattice5__977_18.min1.thm12017-02-06 12:45 668  
[ ]lattice5__977_18.min1.thm1.tptp2017-02-06 16:47 606  
[ ]lattice5__978_21.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__979_25.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__983_27.min1.thm12017-02-06 12:45 744  
[ ]lattice5__988_31.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__992_27.min1.thm12017-02-06 12:45 925  
[ ]lattice5__997_18.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__999_16.min1.thm12017-02-06 12:45 389  
[ ]lattice5__1006_51.min1.thm12017-02-06 12:45 595  
[ ]lattice5__1017_32.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__1021_26.min1.thm12017-02-06 12:45 863  
[ ]lattice5__1025_28.min1.thm12017-02-06 12:45 912  
[ ]lattice5__1033_26.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__1034_19.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__1038_13.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__1062_20.min1.thm12017-02-06 12:45 692  
[ ]lattice5__1062_20.min1.thm1.tptp2017-02-06 16:47 630  
[ ]lattice5__1064_29.min1.thm12017-02-06 12:45 912  
[ ]lattice5__1065_20.min1.thm12017-02-06 12:45 692  
[ ]lattice5__1065_20.min1.thm1.tptp2017-02-06 16:47 630  
[ ]lattice5__1067_29.min1.thm12017-02-06 12:45 913  
[ ]lattice5__1074_19.min1.thm12017-02-06 12:45 693  
[ ]lattice5__1074_19.min1.thm1.tptp2017-02-06 16:47 631  
[ ]lattice5__1076_28.min1.thm12017-02-06 12:45 914  
[ ]lattice5__1077_19.min1.thm12017-02-06 12:45 693  
[ ]lattice5__1077_19.min1.thm1.tptp2017-02-06 16:47 631  
[ ]lattice5__1079_28.min1.thm12017-02-06 12:45 914  
[ ]lattice5__1082_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__1085_29.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__1087_26.min1.thm12017-02-06 12:45 2.6K 
[ ]lattice5__1092_29.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__1094_26.min1.thm12017-02-06 12:45 2.6K 
[ ]lattice5__1117_35.min1.thm12017-02-06 12:45 452  
[ ]lattice5__1118_17.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__1123_19.min1.thm12017-02-06 12:45 2.4K 
[ ]lattice5__1124_17.min1.thm12017-02-06 12:45 665  
[ ]lattice5__1124_17.min1.thm1.tptp2017-02-06 16:47 603  
[ ]lattice5__1126_27.min1.thm12017-02-06 12:45 878  
[ ]lattice5__1127_17.min1.thm12017-02-06 12:45 665  
[ ]lattice5__1127_17.min1.thm1.tptp2017-02-06 16:47 603  
[ ]lattice5__1129_27.min1.thm12017-02-06 12:45 878  
[ ]lattice5__1152_47.min1.thm12017-02-06 12:45 690  
[ ]lattice5__1153_24.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__1189_37.min1.thm12017-02-06 12:45 717  
[ ]lattice5__1208_23.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__1209_19.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__1245_44.min1.thm12017-02-06 12:45 354  
[ ]lattice5__1245_44.min1.thm1.tptp2017-02-06 16:47 276  
[ ]lattice5__1246_44.min1.thm12017-02-06 12:45 354  
[ ]lattice5__1246_44.min1.thm1.tptp2017-02-06 16:47 276  
[ ]lattice5__1257_46.min1.thm12017-02-06 12:45 354  
[ ]lattice5__1257_46.min1.thm1.tptp2017-02-06 16:47 276  
[ ]lattice5__1258_24.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__1259_30.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__1264_32.min1.thm12017-02-06 12:45 628  
[ ]lattice5__1272_60.min1.thm12017-02-06 12:45 570  
[ ]lattice5__1272_60.min1.thm1.tptp2017-02-06 16:47 492  
[ ]lattice5__1281_55.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__1283_47.min1.thm12017-02-06 12:45 816  
[ ]lattice5__1284_48.min1.thm12017-02-06 12:45 420  
[ ]lattice5__1284_48.min1.thm1.tptp2017-02-06 16:47 346  
[ ]lattice5__1299_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__1312_39.min1.thm12017-02-06 12:45 942  
[ ]lattice5__1318_23.min1.thm12017-02-06 12:45 708  
[ ]lattice5__1318_23.min1.thm1.tptp2017-02-06 16:47 646  
[ ]lattice5__1322_59.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__1328_23.min1.thm12017-02-06 12:45 708  
[ ]lattice5__1328_23.min1.thm1.tptp2017-02-06 16:47 646  
[ ]lattice5__1329_57.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__1346_37.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__1365_21.min1.thm12017-02-06 12:45 893  
[ ]lattice5__1367_26.min1.thm12017-02-06 12:45 894  
[ ]lattice5__1369_26.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__1373_27.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__1377_19.min1.thm12017-02-06 12:45 889  
[ ]lattice5__1380_23.min1.thm12017-02-06 12:45 890  
[ ]lattice5__1386_43.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__1387_18.min1.thm12017-02-06 12:45 801  
[ ]lattice5__1388_10.min1.thm12017-02-06 12:45 263  
[ ]lattice5__1390_29.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__1395_55.min1.thm12017-02-06 12:45 808  
[ ]lattice5__1401_19.min1.thm12017-02-06 12:45 666  
[ ]lattice5__1401_19.min1.thm1.tptp2017-02-06 16:47 604  
[ ]lattice5__1402_53.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__1408_22.min1.thm12017-02-06 12:45 3.7K 
[ ]lattice5__1411_21.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__1422_31.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__1434_39.min1.thm12017-02-06 12:45 426  
[ ]lattice5__1434_39.min1.thm1.tptp2017-02-06 16:47 348  
[ ]lattice5__1441_39.min1.thm12017-02-06 12:45 430  
[ ]lattice5__1441_39.min1.thm1.tptp2017-02-06 16:47 352  
[ ]lattice5__1449_25.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__1451_14.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__1453_25.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__1454_18.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__1466_13.min1.thm12017-02-06 12:45 131  
[ ]lattice5__1472_11.min1.thm12017-02-06 12:45 510  
[ ]lattice5__1497_51.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__1512_38.min1.thm12017-02-06 12:45 446  
[ ]lattice5__1514_25.min1.thm12017-02-06 12:45 709  
[ ]lattice5__1518_43.min1.thm12017-02-06 12:45 901  
[ ]lattice5__1519_43.min1.thm12017-02-06 12:45 901  
[ ]lattice5__1521_59.min1.thm12017-02-06 12:45 757  
[ ]lattice5__1522_21.min1.thm12017-02-06 12:45 371  
[ ]lattice5__1522_21.min1.thm1.tptp2017-02-06 16:47 312  
[ ]lattice5__1526_30.min1.thm12017-02-06 12:45 439  
[ ]lattice5__1526_30.min1.thm1.tptp2017-02-06 16:47 374  
[ ]lattice5__1531_27.min1.thm12017-02-06 12:45 322  
[ ]lattice5__1532_34.min1.thm12017-02-06 12:45 356  
[ ]lattice5__1539_28.min1.thm12017-02-06 12:45 417  
[ ]lattice5__1539_28.min1.thm1.tptp2017-02-06 16:47 352  
[ ]lattice5__1544_34.min1.thm12017-02-06 12:45 356  
[ ]lattice5__1548_18.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__1551_49.min1.thm12017-02-06 12:45 458  
[ ]lattice5__1551_49.min1.thm1.tptp2017-02-06 16:47 380  
[ ]lattice5__1553_22.min1.thm12017-02-06 12:45 7.0K 
[ ]lattice5__1558_22.min1.thm12017-02-06 12:45 5.0K 
[ ]lattice5__1563_22.min1.thm12017-02-06 12:45 5.0K 
[ ]lattice5__1568_22.min1.thm12017-02-06 12:45 5.5K 
[ ]lattice5__1573_22.min1.thm12017-02-06 12:45 5.2K 
[ ]lattice5__1577_46.min1.thm12017-02-06 12:45 405  
[ ]lattice5__1577_46.min1.thm1.tptp2017-02-06 16:47 329  
[ ]lattice5__1579_22.min1.thm12017-02-06 12:45 7.6K 
[ ]lattice5__1583_46.min1.thm12017-02-06 12:45 416  
[ ]lattice5__1583_46.min1.thm1.tptp2017-02-06 16:47 340  
[ ]lattice5__1585_22.min1.thm12017-02-06 12:45 8.1K 
[ ]lattice5__1589_46.min1.thm12017-02-06 12:45 427  
[ ]lattice5__1589_46.min1.thm1.tptp2017-02-06 16:47 351  
[ ]lattice5__1591_22.min1.thm12017-02-06 12:45 7.7K 
[ ]lattice5__1595_46.min1.thm12017-02-06 12:45 405  
[ ]lattice5__1595_46.min1.thm1.tptp2017-02-06 16:47 329  
[ ]lattice5__1597_22.min1.thm12017-02-06 12:45 7.6K 
[ ]lattice5__1601_46.min1.thm12017-02-06 12:45 418  
[ ]lattice5__1601_46.min1.thm1.tptp2017-02-06 16:47 342  
[ ]lattice5__1603_22.min1.thm12017-02-06 12:45 8.1K 
[ ]lattice5__1607_46.min1.thm12017-02-06 12:45 429  
[ ]lattice5__1607_46.min1.thm1.tptp2017-02-06 16:47 353  
[ ]lattice5__1609_22.min1.thm12017-02-06 12:45 7.7K 
[ ]lattice5__1616_40.min1.thm12017-02-06 12:45 457  
[ ]lattice5__1618_28.min1.thm12017-02-06 12:45 731  
[ ]lattice5__1619_45.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__1619_45.min1.thm1.tptp2017-02-06 16:47 893  
[ ]lattice5__1620_36.min1.thm12017-02-06 12:45 436  
[ ]lattice5__1622_24.min1.thm12017-02-06 12:45 689  
[ ]lattice5__1627_50.min1.thm12017-02-06 12:45 819  
[ ]lattice5__1630_36.min1.thm12017-02-06 12:45 966  
[ ]lattice5__1630_36.min1.thm1.tptp2017-02-06 16:47 893  
[ ]lattice5__1633_43.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__1633_43.min1.thm1.tptp2017-02-06 16:47 1.0K 
[ ]lattice5__1636_18.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__1636_18.min1.thm1.tptp2017-02-06 16:47 937  
[ ]lattice5__1642_58.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__1649_50.min1.thm12017-02-06 12:45 819  
[ ]lattice5__1652_36.min1.thm12017-02-06 12:45 966  
[ ]lattice5__1652_36.min1.thm1.tptp2017-02-06 16:47 893  
[ ]lattice5__1655_43.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__1655_43.min1.thm1.tptp2017-02-06 16:47 1.0K 
[ ]lattice5__1658_18.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__1658_18.min1.thm1.tptp2017-02-06 16:47 937  
[ ]lattice5__1695_43.min1.thm12017-02-06 12:45 901  
[ ]lattice5__1696_43.min1.thm12017-02-06 12:45 901  
[ ]lattice5__1697_18.min1.thm12017-02-06 12:45 2.7K 
[ ]lattice5__1705_46.min1.thm12017-02-06 12:45 405  
[ ]lattice5__1705_46.min1.thm1.tptp2017-02-06 16:47 329  
[ ]lattice5__1711_46.min1.thm12017-02-06 12:45 416  
[ ]lattice5__1711_46.min1.thm1.tptp2017-02-06 16:47 340  
[ ]lattice5__1717_46.min1.thm12017-02-06 12:45 427  
[ ]lattice5__1717_46.min1.thm1.tptp2017-02-06 16:47 351  
[ ]lattice5__1723_46.min1.thm12017-02-06 12:45 405  
[ ]lattice5__1723_46.min1.thm1.tptp2017-02-06 16:47 329  
[ ]lattice5__1741_46.min1.thm12017-02-06 12:45 416  
[ ]lattice5__1741_46.min1.thm1.tptp2017-02-06 16:47 340  
[ ]lattice5__1759_46.min1.thm12017-02-06 12:45 429  
[ ]lattice5__1759_46.min1.thm1.tptp2017-02-06 16:47 353  
[ ]lattice5__1792_41.min1.thm12017-02-06 12:45 881  
[ ]lattice5__1793_16.min1.thm12017-02-06 12:45 742  
[ ]lattice5__1793_16.min1.thm1.tptp2017-02-06 16:47 684  
[ ]lattice5__1796_44.min1.thm12017-02-06 12:45 338  
[ ]lattice5__1796_44.min1.thm1.tptp2017-02-06 16:47 260  
[ ]lattice5__1798_22.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__1819_41.min1.thm12017-02-06 12:45 875  
[ ]lattice5__1820_41.min1.thm12017-02-06 12:45 875  
[ ]lattice5__1821_14.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__1824_50.min1.thm12017-02-06 12:45 426  
[ ]lattice5__1824_50.min1.thm1.tptp2017-02-06 16:47 348  
[ ]lattice5__1831_42.min1.thm12017-02-06 12:45 378  
[ ]lattice5__1831_42.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__1837_42.min1.thm12017-02-06 12:45 389  
[ ]lattice5__1837_42.min1.thm1.tptp2017-02-06 16:47 313  
[ ]lattice5__1843_42.min1.thm12017-02-06 12:45 400  
[ ]lattice5__1843_42.min1.thm1.tptp2017-02-06 16:47 324  
[ ]lattice5__1849_42.min1.thm12017-02-06 12:45 378  
[ ]lattice5__1849_42.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__1855_16.min1.thm12017-02-06 12:45 747  
[ ]lattice5__1855_16.min1.thm1.tptp2017-02-06 16:47 670  
[ ]lattice5__1869_42.min1.thm12017-02-06 12:45 389  
[ ]lattice5__1869_42.min1.thm1.tptp2017-02-06 16:47 313  
[ ]lattice5__1880_16.min1.thm12017-02-06 12:45 771  
[ ]lattice5__1880_16.min1.thm1.tptp2017-02-06 16:47 694  
[ ]lattice5__1889_42.min1.thm12017-02-06 12:45 402  
[ ]lattice5__1889_42.min1.thm1.tptp2017-02-06 16:47 326  
[ ]lattice5__1905_16.min1.thm12017-02-06 12:45 793  
[ ]lattice5__1905_16.min1.thm1.tptp2017-02-06 16:47 716  
[ ]lattice5__1919_55.min1.thm12017-02-06 12:45 352  
[ ]lattice5__1922_48.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__1929_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__1932_52.min1.thm12017-02-06 12:45 481  
[ ]lattice5__1932_52.min1.thm1.tptp2017-02-06 16:47 405  
[ ]lattice5__1938_48.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__1948_52.min1.thm12017-02-06 12:45 492  
[ ]lattice5__1948_52.min1.thm1.tptp2017-02-06 16:47 416  
[ ]lattice5__1955_62.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__1968_52.min1.thm12017-02-06 12:45 503  
[ ]lattice5__1968_52.min1.thm1.tptp2017-02-06 16:47 427  
[ ]lattice5__1974_48.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__1992_40.min1.thm12017-02-06 12:45 330  
[ ]lattice5__1992_40.min1.thm1.tptp2017-02-06 16:47 252  
[ ]lattice5__1993_16.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__2008_38.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2009_20.min1.thm12017-02-06 12:45 826  
[ ]lattice5__2010_27.min1.thm12017-02-06 12:45 823  
[ ]lattice5__2011_27.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2034_26.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2045_38.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2046_20.min1.thm12017-02-06 12:45 826  
[ ]lattice5__2047_27.min1.thm12017-02-06 12:45 823  
[ ]lattice5__2048_27.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2068_38.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__2069_20.min1.thm12017-02-06 12:45 823  
[ ]lattice5__2070_27.min1.thm12017-02-06 12:45 826  
[ ]lattice5__2071_27.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2106_48.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__2124_48.min1.thm12017-02-06 12:45 426  
[ ]lattice5__2124_48.min1.thm1.tptp2017-02-06 16:47 348  
[ ]lattice5__2125_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__2171_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__2174_52.min1.thm12017-02-06 12:45 481  
[ ]lattice5__2174_52.min1.thm1.tptp2017-02-06 16:47 405  
[ ]lattice5__2184_52.min1.thm12017-02-06 12:45 492  
[ ]lattice5__2184_52.min1.thm1.tptp2017-02-06 16:47 416  
[ ]lattice5__2198_52.min1.thm12017-02-06 12:45 503  
[ ]lattice5__2198_52.min1.thm1.tptp2017-02-06 16:47 427  
[ ]lattice5__2213_16.min1.thm12017-02-06 12:45 5.3K 
[ ]lattice5__2223_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2230_20.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2242_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2262_27.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__2263_20.min1.thm12017-02-06 12:45 823  
[ ]lattice5__2270_20.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2278_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2293_27.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__2294_20.min1.thm12017-02-06 12:45 827  
[ ]lattice5__2301_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2313_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2322_27.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__2323_20.min1.thm12017-02-06 12:45 824  
[ ]lattice5__2335_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2343_20.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2353_27.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__2354_20.min1.thm12017-02-06 12:45 827  
[ ]lattice5__2372_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2385_20.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2392_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2409_40.min1.thm12017-02-06 12:45 330  
[ ]lattice5__2409_40.min1.thm1.tptp2017-02-06 16:47 252  
[ ]lattice5__2410_16.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__2495_40.min1.thm12017-02-06 12:45 330  
[ ]lattice5__2495_40.min1.thm1.tptp2017-02-06 16:47 252  
[ ]lattice5__2496_16.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__2524_34.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2525_41.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__2537_26.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2561_34.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2562_41.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__2583_34.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__2585_41.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__2601_34.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__2611_17.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2615_48.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__2632_58.min1.thm12017-02-06 12:45 522  
[ ]lattice5__2632_58.min1.thm1.tptp2017-02-06 16:47 444  
[ ]lattice5__2640_16.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__2643_21.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__2647_21.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__2651_21.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__2655_21.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__2659_21.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__2663_21.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__2667_21.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__2671_21.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__2684_21.min1.thm12017-02-06 12:45 408  
[ ]lattice5__2684_21.min1.thm1.tptp2017-02-06 16:47 331  
[ ]lattice5__2691_16.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__2693_23.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__2695_19.min1.thm12017-02-06 12:45 722  
[ ]lattice5__2698_24.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__2715_18.min1.thm12017-02-06 12:45 619  
[ ]lattice5__2724_19.min1.thm12017-02-06 12:45 593  
[ ]lattice5__2736_33.min1.thm12017-02-06 12:45 357  
[ ]lattice5__2738_25.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__2739_32.min1.thm12017-02-06 12:45 770  
[ ]lattice5__2741_17.min1.thm12017-02-06 12:45 888  
[ ]lattice5__2796_14.min1.thm12017-02-06 12:45 607  
[ ]lattice5__2829_65.min1.thm12017-02-06 12:45 704  
[ ]lattice5__2830_18.min1.thm12017-02-06 12:45 716  
[ ]lattice5__2841_17.min1.thm12017-02-06 12:45 428  
[ ]lattice5__2845_37.min1.thm12017-02-06 12:45 829  
[ ]lattice5__2846_15.min1.thm12017-02-06 12:45 345  
[ ]lattice5__2846_15.min1.thm1.tptp2017-02-06 16:47 266  
[ ]lattice5__2848_20.min1.thm12017-02-06 12:45 942  
[ ]lattice5__2850_39.min1.thm12017-02-06 12:45 537  
[ ]lattice5__2851_18.min1.thm12017-02-06 12:45 708  
[ ]lattice5__2853_12.min1.thm12017-02-06 12:45 341  
[ ]lattice5__2853_12.min1.thm1.tptp2017-02-06 16:47 259  
[ ]lattice5__2855_16.min1.thm12017-02-06 12:45 363  
[ ]lattice5__2855_16.min1.thm1.tptp2017-02-06 16:47 280  
[ ]lattice5__2866_63.min1.thm12017-02-06 12:45 684  
[ ]lattice5__2868_56.min1.thm12017-02-06 12:45 627  
[ ]lattice5__2870_19.min1.thm12017-02-06 12:45 577  
[ ]lattice5__2881_15.min1.thm12017-02-06 12:45 404  
[ ]lattice5__2885_35.min1.thm12017-02-06 12:45 785  
[ ]lattice5__2886_13.min1.thm12017-02-06 12:45 341  
[ ]lattice5__2886_13.min1.thm1.tptp2017-02-06 16:47 262  
[ ]lattice5__2888_18.min1.thm12017-02-06 12:45 882  
[ ]lattice5__2890_19.min1.thm12017-02-06 12:45 509  
[ ]lattice5__2892_12.min1.thm12017-02-06 12:45 416  
[ ]lattice5__2894_14.min1.thm12017-02-06 12:45 377  
[ ]lattice5__2894_14.min1.thm1.tptp2017-02-06 16:47 296  
[ ]lattice5__2910_30.min1.thm12017-02-06 12:45 619  
[ ]lattice5__2914_16.min1.thm12017-02-06 12:45 801  
[ ]lattice5__2915_33.min1.thm12017-02-06 12:45 691  
[ ]lattice5__2923_18.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__2926_67.min1.thm12017-02-06 12:45 803  
[ ]lattice5__2929_29.min1.thm12017-02-06 12:45 537  
[ ]lattice5__2930_27.min1.thm12017-02-06 12:45 389  
[ ]lattice5__2931_18.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__2948_19.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__2954_34.min1.thm12017-02-06 12:45 457  
[ ]lattice5__2954_34.min1.thm1.tptp2017-02-06 16:47 369  
[ ]lattice5__2955_19.min1.thm12017-02-06 12:45 565  
[ ]lattice5__2956_31.min1.thm12017-02-06 12:45 448  
[ ]lattice5__2957_60.min1.thm12017-02-06 12:45 737  
[ ]lattice5__2959_60.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__2960_14.min1.thm12017-02-06 12:45 2.7K 
[ ]lattice5__2961_16.min1.thm12017-02-06 12:45 682  
[ ]lattice5__2961_16.min1.thm1.tptp2017-02-06 16:47 596  
[ ]lattice5__2971_37.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__2972_40.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__2973_20.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__2977_71.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__2978_42.min1.thm12017-02-06 12:45 2.3K 
[ ]lattice5__2979_42.min1.thm12017-02-06 12:45 961  
[ ]lattice5__2981_12.min1.thm12017-02-06 12:45 805  
[ ]lattice5__2982_43.min1.thm12017-02-06 12:45 529  
[ ]lattice5__2984_17.min1.thm12017-02-06 12:45 561  
[ ]lattice5__2995_14.min1.thm12017-02-06 12:45 684  
[ ]lattice5__3059_14.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3059_14.min1.thm1.tptp2017-02-06 16:47 1.0K 
[ ]lattice5__3096_13.min1.thm12017-02-06 12:45 229  
[ ]lattice5__3099_18.min1.thm12017-02-06 12:45 399  
[ ]lattice5__3099_18.min1.thm1.tptp2017-02-06 16:47 319  
[ ]lattice5__3103_27.min1.thm12017-02-06 12:45 848  
[ ]lattice5__3105_22.min1.thm12017-02-06 12:45 746  
[ ]lattice5__3106_61.min1.thm12017-02-06 12:45 476  
[ ]lattice5__3106_61.min1.thm1.tptp2017-02-06 16:47 399  
[ ]lattice5__3107_66.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__3109_21.min1.thm12017-02-06 12:45 839  
[ ]lattice5__3127_13.min1.thm12017-02-06 12:45 203  
[ ]lattice5__3130_18.min1.thm12017-02-06 12:45 373  
[ ]lattice5__3130_18.min1.thm1.tptp2017-02-06 16:47 293  
[ ]lattice5__3135_17.min1.thm12017-02-06 12:45 691  
[ ]lattice5__3136_22.min1.thm12017-02-06 12:45 602  
[ ]lattice5__3138_22.min1.thm12017-02-06 12:45 831  
[ ]lattice5__3139_36.min1.thm12017-02-06 12:45 859  
[ ]lattice5__3140_21.min1.thm12017-02-06 12:45 705  
[ ]lattice5__3143_10.min1.thm12017-02-06 12:45 924  
[ ]lattice5__3145_14.min1.thm12017-02-06 12:45 518  
[ ]lattice5__3145_14.min1.thm1.tptp2017-02-06 16:47 441  
[ ]lattice5__3162_9.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3163_63.min1.thm12017-02-06 12:45 684  
[ ]lattice5__3165_43.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__3166_38.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__3201_41.min1.thm12017-02-06 12:45 723  
[ ]lattice5__3203_17.min1.thm12017-02-06 12:45 223  
[ ]lattice5__3206_22.min1.thm12017-02-06 12:45 399  
[ ]lattice5__3206_22.min1.thm1.tptp2017-02-06 16:47 319  
[ ]lattice5__3211_20.min1.thm12017-02-06 12:45 743  
[ ]lattice5__3213_20.min1.thm12017-02-06 12:45 642  
[ ]lattice5__3214_46.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__3215_22.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3216_32.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__3217_25.min1.thm12017-02-06 12:45 614  
[ ]lattice5__3228_17.min1.thm12017-02-06 12:45 249  
[ ]lattice5__3231_22.min1.thm12017-02-06 12:45 425  
[ ]lattice5__3231_22.min1.thm1.tptp2017-02-06 16:47 345  
[ ]lattice5__3235_30.min1.thm12017-02-06 12:45 900  
[ ]lattice5__3237_25.min1.thm12017-02-06 12:45 786  
[ ]lattice5__3238_26.min1.thm12017-02-06 12:45 266  
[ ]lattice5__3239_30.min1.thm12017-02-06 12:45 887  
[ ]lattice5__3241_35.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__3242_53.min1.thm12017-02-06 12:45 884  
[ ]lattice5__3244_29.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__3245_45.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__3247_37.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3251_11.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3262_18.min1.thm12017-02-06 12:45 651  
[ ]lattice5__3265_18.min1.thm12017-02-06 12:45 651  
[ ]lattice5__3266_49.min1.thm12017-02-06 12:45 821  
[ ]lattice5__3267_30.min1.thm12017-02-06 12:45 514  
[ ]lattice5__3268_30.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3269_21.min1.thm12017-02-06 12:45 423  
[ ]lattice5__3269_21.min1.thm1.tptp2017-02-06 16:47 349  
[ ]lattice5__3272_27.min1.thm12017-02-06 12:45 458  
[ ]lattice5__3272_27.min1.thm1.tptp2017-02-06 16:47 405  
[ ]lattice5__3281_17.min1.thm12017-02-06 12:45 651  
[ ]lattice5__3282_32.min1.thm12017-02-06 12:45 687  
[ ]lattice5__3283_37.min1.thm12017-02-06 12:45 787  
[ ]lattice5__3285_56.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__3286_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__3288_52.min1.thm12017-02-06 12:45 2.6K 
[ ]lattice5__3292_28.min1.thm12017-02-06 12:45 888  
[ ]lattice5__3295_46.min1.thm12017-02-06 12:45 396  
[ ]lattice5__3307_38.min1.thm12017-02-06 12:45 687  
[ ]lattice5__3308_37.min1.thm12017-02-06 12:45 787  
[ ]lattice5__3311_58.min1.thm12017-02-06 12:45 421  
[ ]lattice5__3311_58.min1.thm1.tptp2017-02-06 16:47 333  
[ ]lattice5__3320_26.min1.thm12017-02-06 12:45 823  
[ ]lattice5__3321_23.min1.thm12017-02-06 12:45 647  
[ ]lattice5__3322_50.min1.thm12017-02-06 12:45 771  
[ ]lattice5__3323_41.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3325_61.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__3326_21.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__3327_61.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3333_53.min1.thm12017-02-06 12:45 798  
[ ]lattice5__3334_37.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3335_73.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__3336_21.min1.thm12017-02-06 12:45 889  
[ ]lattice5__3338_26.min1.thm12017-02-06 12:45 565  
[ ]lattice5__3339_19.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__3341_21.min1.thm12017-02-06 12:45 953  
[ ]lattice5__3343_15.min1.thm12017-02-06 12:45 405  
[ ]lattice5__3344_52.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3345_31.min1.thm12017-02-06 12:45 555  
[ ]lattice5__3346_34.min1.thm12017-02-06 12:45 843  
[ ]lattice5__3355_55.min1.thm12017-02-06 12:45 806  
[ ]lattice5__3356_37.min1.thm12017-02-06 12:45 913  
[ ]lattice5__3359_26.min1.thm12017-02-06 12:45 499  
[ ]lattice5__3359_26.min1.thm1.tptp2017-02-06 16:47 417  
[ ]lattice5__3360_20.min1.thm12017-02-06 12:45 915  
[ ]lattice5__3366_14.min1.thm12017-02-06 12:45 679  
[ ]lattice5__3370_37.min1.thm12017-02-06 12:45 687  
[ ]lattice5__3371_33.min1.thm12017-02-06 12:45 768  
[ ]lattice5__3382_18.min1.thm12017-02-06 12:45 728  
[ ]lattice5__3385_18.min1.thm12017-02-06 12:45 728  
[ ]lattice5__3386_49.min1.thm12017-02-06 12:45 821  
[ ]lattice5__3387_39.min1.thm12017-02-06 12:45 691  
[ ]lattice5__3388_30.min1.thm12017-02-06 12:45 514  
[ ]lattice5__3389_39.min1.thm12017-02-06 12:45 691  
[ ]lattice5__3390_30.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3391_21.min1.thm12017-02-06 12:45 423  
[ ]lattice5__3391_21.min1.thm1.tptp2017-02-06 16:47 349  
[ ]lattice5__3394_24.min1.thm12017-02-06 12:45 421  
[ ]lattice5__3394_24.min1.thm1.tptp2017-02-06 16:47 368  
[ ]lattice5__3398_17.min1.thm12017-02-06 12:45 969  
[ ]lattice5__3401_29.min1.thm12017-02-06 12:45 337  
[ ]lattice5__3401_29.min1.thm1.tptp2017-02-06 16:47 258  
[ ]lattice5__3403_13.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__3405_14.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3405_14.min1.thm1.tptp2017-02-06 16:47 1.3K 
[ ]lattice5__3433_15.min1.thm12017-02-06 12:45 404  
[ ]lattice5__3437_37.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3438_13.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__3440_18.min1.thm12017-02-06 12:45 931  
[ ]lattice5__3455_12.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__3457_14.min1.thm12017-02-06 12:45 627  
[ ]lattice5__3457_14.min1.thm1.tptp2017-02-06 16:47 546  
[ ]lattice5__3483_13.min1.thm12017-02-06 12:45 203  
[ ]lattice5__3491_17.min1.thm12017-02-06 12:45 691  
[ ]lattice5__3492_22.min1.thm12017-02-06 12:45 602  
[ ]lattice5__3494_22.min1.thm12017-02-06 12:45 880  
[ ]lattice5__3495_38.min1.thm12017-02-06 12:45 957  
[ ]lattice5__3506_13.min1.thm12017-02-06 12:45 229  
[ ]lattice5__3513_27.min1.thm12017-02-06 12:45 848  
[ ]lattice5__3515_22.min1.thm12017-02-06 12:45 746  
[ ]lattice5__3525_14.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3525_14.min1.thm1.tptp2017-02-06 16:47 905  
[ ]lattice5__3544_67.min1.thm12017-02-06 12:45 784  
[ ]lattice5__3577_20.min1.thm12017-02-06 12:45 939  
[ ]lattice5__3580_17.min1.thm12017-02-06 12:45 651  
[ ]lattice5__3581_32.min1.thm12017-02-06 12:45 687  
[ ]lattice5__3582_37.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3584_60.min1.thm12017-02-06 12:45 946  
[ ]lattice5__3585_60.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3589_42.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3590_53.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3593_40.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3596_33.min1.thm12017-02-06 12:45 866  
[ ]lattice5__3599_22.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__3606_40.min1.thm12017-02-06 12:45 439  
[ ]lattice5__3608_20.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__3611_14.min1.thm12017-02-06 12:45 556  
[ ]lattice5__3611_14.min1.thm1.tptp2017-02-06 16:47 475  
[ ]lattice5__3630_71.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3663_21.min1.thm12017-02-06 12:45 939  
[ ]lattice5__3666_19.min1.thm12017-02-06 12:45 651  
[ ]lattice5__3669_21.min1.thm12017-02-06 12:45 939  
[ ]lattice5__3672_19.min1.thm12017-02-06 12:45 652  
[ ]lattice5__3673_36.min1.thm12017-02-06 12:45 823  
[ ]lattice5__3674_34.min1.thm12017-02-06 12:45 866  
[ ]lattice5__3675_39.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3680_46.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3681_55.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3683_24.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3685_63.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3686_34.min1.thm12017-02-06 12:45 868  
[ ]lattice5__3687_39.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3692_46.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3693_55.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3695_24.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__3697_63.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3698_15.min1.thm12017-02-06 12:45 515  
[ ]lattice5__3702_55.min1.thm12017-02-06 12:45 727  
[ ]lattice5__3705_43.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3708_67.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__3718_55.min1.thm12017-02-06 12:45 727  
[ ]lattice5__3721_43.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3724_67.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__3737_48.min1.thm12017-02-06 12:45 598  
[ ]lattice5__3743_14.min1.thm12017-02-06 12:45 556  
[ ]lattice5__3743_14.min1.thm1.tptp2017-02-06 16:47 475  
[ ]lattice5__3763_24.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3765_18.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__3766_25.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__3771_42.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3773_10.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__3777_53.min1.thm12017-02-06 12:45 2.7K 
[ ]lattice5__3824_20.min1.thm12017-02-06 12:45 940  
[ ]lattice5__3827_18.min1.thm12017-02-06 12:45 651  
[ ]lattice5__3830_20.min1.thm12017-02-06 12:45 940  
[ ]lattice5__3833_18.min1.thm12017-02-06 12:45 652  
[ ]lattice5__3836_20.min1.thm12017-02-06 12:45 941  
[ ]lattice5__3839_18.min1.thm12017-02-06 12:45 653  
[ ]lattice5__3840_39.min1.thm12017-02-06 12:45 958  
[ ]lattice5__3841_34.min1.thm12017-02-06 12:45 871  
[ ]lattice5__3842_39.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3847_28.min1.thm12017-02-06 12:45 2.7K 
[ ]lattice5__3849_43.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__3850_38.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__3853_63.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3854_34.min1.thm12017-02-06 12:45 874  
[ ]lattice5__3855_39.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3860_28.min1.thm12017-02-06 12:45 2.7K 
[ ]lattice5__3862_43.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__3863_38.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__3866_63.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3867_39.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__3872_28.min1.thm12017-02-06 12:45 2.7K 
[ ]lattice5__3874_43.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__3875_38.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__3878_63.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__3879_34.min1.thm12017-02-06 12:45 873  
[ ]lattice5__3880_15.min1.thm12017-02-06 12:45 523  
[ ]lattice5__3884_55.min1.thm12017-02-06 12:45 735  
[ ]lattice5__3887_19.min1.thm12017-02-06 12:45 529  
[ ]lattice5__3890_67.min1.thm12017-02-06 12:45 963  
[ ]lattice5__3892_67.min1.thm12017-02-06 12:45 701  
[ ]lattice5__3893_47.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3896_59.min1.thm12017-02-06 12:45 747  
[ ]lattice5__3897_72.min1.thm12017-02-06 12:45 707  
[ ]lattice5__3910_67.min1.thm12017-02-06 12:45 962  
[ ]lattice5__3912_47.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3915_59.min1.thm12017-02-06 12:45 747  
[ ]lattice5__3916_72.min1.thm12017-02-06 12:45 707  
[ ]lattice5__3920_59.min1.thm12017-02-06 12:45 741  
[ ]lattice5__3922_59.min1.thm12017-02-06 12:45 668  
[ ]lattice5__3923_72.min1.thm12017-02-06 12:45 709  
[ ]lattice5__3936_55.min1.thm12017-02-06 12:45 735  
[ ]lattice5__3939_19.min1.thm12017-02-06 12:45 529  
[ ]lattice5__3942_67.min1.thm12017-02-06 12:45 962  
[ ]lattice5__3944_47.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3947_59.min1.thm12017-02-06 12:45 747  
[ ]lattice5__3948_72.min1.thm12017-02-06 12:45 707  
[ ]lattice5__3952_59.min1.thm12017-02-06 12:45 741  
[ ]lattice5__3954_59.min1.thm12017-02-06 12:45 668  
[ ]lattice5__3955_72.min1.thm12017-02-06 12:45 709  
[ ]lattice5__3965_67.min1.thm12017-02-06 12:45 960  
[ ]lattice5__3967_67.min1.thm12017-02-06 12:45 701  
[ ]lattice5__3968_47.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__3971_59.min1.thm12017-02-06 12:45 747  
[ ]lattice5__3972_72.min1.thm12017-02-06 12:45 707  
[ ]lattice5__3992_56.min1.thm12017-02-06 12:45 757  
[ ]lattice5__3999_14.min1.thm12017-02-06 12:45 729  
[ ]lattice5__3999_14.min1.thm1.tptp2017-02-06 16:47 652  
[ ]lattice5__4012_13.min1.thm12017-02-06 12:45 131  
[ ]lattice5__4019_11.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__4028_13.min1.thm12017-02-06 12:45 131  
[ ]lattice5__4059_24.min1.thm12017-02-06 12:45 2.9K 
[ ]lattice5__4066_28.min1.thm12017-02-06 12:45 2.7K 
[ ]lattice5__4070_28.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__4071_23.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__4077_53.min1.thm12017-02-06 12:45 438  
[ ]lattice5__4078_34.min1.thm12017-02-06 12:45 436  
[ ]lattice5__4080_42.min1.thm12017-02-06 12:45 662  
[ ]lattice5__4080_42.min1.thm1.tptp2017-02-06 16:47 600  
[ ]lattice5__4084_20.min1.thm12017-02-06 12:45 538  
[ ]lattice5__4085_39.min1.thm12017-02-06 12:45 447  
[ ]lattice5__4087_26.min1.thm12017-02-06 12:45 709  
[ ]lattice5__4088_11.min1.thm12017-02-06 12:45 519  
[ ]lattice5__4089_51.min1.thm12017-02-06 12:45 628  
[ ]lattice5__4090_22.min1.thm12017-02-06 12:45 411  
[ ]lattice5__4090_22.min1.thm1.tptp2017-02-06 16:47 334  
[ ]lattice5__4091_19.min1.thm12017-02-06 12:45 550  
[ ]lattice5__4092_61.min1.thm12017-02-06 12:45 829  
[ ]lattice5__4094_41.min1.thm12017-02-06 12:45 458  
[ ]lattice5__4096_28.min1.thm12017-02-06 12:45 731  
[ ]lattice5__4097_21.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__4099_29.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__4102_41.min1.thm12017-02-06 12:45 750  
[ ]lattice5__4105_48.min1.thm12017-02-06 12:45 2.6K 
[ ]lattice5__4109_26.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__4111_42.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4114_24.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4115_11.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4116_41.min1.thm12017-02-06 12:45 684  
[ ]lattice5__4116_41.min1.thm1.tptp2017-02-06 16:47 622  
[ ]lattice5__4117_49.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__4120_40.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__4123_43.min1.thm12017-02-06 12:45 706  
[ ]lattice5__4123_43.min1.thm1.tptp2017-02-06 16:47 644  
[ ]lattice5__4127_24.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4128_11.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4178_23.min1.thm12017-02-06 12:45 252  
[ ]lattice5__4179_23.min1.thm12017-02-06 12:45 434  
[ ]lattice5__4179_23.min1.thm1.tptp2017-02-06 16:47 358  
[ ]lattice5__4201_22.min1.thm12017-02-06 12:45 518  
[ ]lattice5__4201_22.min1.thm1.tptp2017-02-06 16:47 442  
[ ]lattice5__4213_23.min1.thm12017-02-06 12:45 3.6K 
[ ]lattice5__4216_20.min1.thm12017-02-06 12:45 436  
[ ]lattice5__4216_20.min1.thm1.tptp2017-02-06 16:47 360  
[ ]lattice5__4241_18.min1.thm12017-02-06 12:45 429  
[ ]lattice5__4241_18.min1.thm1.tptp2017-02-06 16:47 349  
[ ]lattice5__4250_20.min1.thm12017-02-06 12:45 392  
[ ]lattice5__4250_20.min1.thm1.tptp2017-02-06 16:47 322  
[ ]lattice5__4252_51.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__4253_20.min1.thm12017-02-06 12:45 392  
[ ]lattice5__4253_20.min1.thm1.tptp2017-02-06 16:47 322  
[ ]lattice5__4255_14.min1.thm12017-02-06 12:45 3.2K 
[ ]lattice5__4256_59.min1.thm12017-02-06 12:45 2.6K 
[ ]lattice5__4257_21.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__4260_13.min1.thm12017-02-06 12:45 741  
[ ]lattice5__4281_18.min1.thm12017-02-06 12:45 429  
[ ]lattice5__4281_18.min1.thm1.tptp2017-02-06 16:47 349  
[ ]lattice5__4292_26.min1.thm12017-02-06 12:45 3.2K 
[ ]lattice5__4293_20.min1.thm12017-02-06 12:45 392  
[ ]lattice5__4293_20.min1.thm1.tptp2017-02-06 16:47 322  
[ ]lattice5__4296_20.min1.thm12017-02-06 12:45 393  
[ ]lattice5__4296_20.min1.thm1.tptp2017-02-06 16:47 323  
[ ]lattice5__4301_14.min1.thm12017-02-06 12:45 741  
[ ]lattice5__4319_15.min1.thm12017-02-06 12:45 227  
[ ]lattice5__4323_22.min1.thm12017-02-06 12:45 480  
[ ]lattice5__4328_22.min1.thm12017-02-06 12:45 573  
[ ]lattice5__4335_37.min1.thm12017-02-06 12:45 821  
[ ]lattice5__4339_20.min1.thm12017-02-06 12:45 867  
[ ]lattice5__4344_55.min1.thm12017-02-06 12:45 643  
[ ]lattice5__4345_15.min1.thm12017-02-06 12:45 227  
[ ]lattice5__4349_23.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4355_19.min1.thm12017-02-06 12:45 233  
[ ]lattice5__4358_39.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__4361_54.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__4368_23.min1.thm12017-02-06 12:45 239  
[ ]lattice5__4371_45.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__4372_64.min1.thm12017-02-06 12:45 2.3K 
[ ]lattice5__4378_72.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4383_68.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__4397_47.min1.thm12017-02-06 12:45 471  
[ ]lattice5__4397_47.min1.thm1.tptp2017-02-06 16:47 383  
[ ]lattice5__4398_15.min1.thm12017-02-06 12:45 227  
[ ]lattice5__4401_20.min1.thm12017-02-06 12:45 464  
[ ]lattice5__4409_52.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__4411_18.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4428_15.min1.thm12017-02-06 12:45 227  
[ ]lattice5__4432_24.min1.thm12017-02-06 12:45 880  
[ ]lattice5__4433_24.min1.thm12017-02-06 12:45 880  
[ ]lattice5__4444_53.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__4445_18.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__4459_42.min1.thm12017-02-06 12:45 356  
[ ]lattice5__4459_42.min1.thm1.tptp2017-02-06 16:47 278  
[ ]lattice5__4460_41.min1.thm12017-02-06 12:45 356  
[ ]lattice5__4460_41.min1.thm1.tptp2017-02-06 16:47 278  
[ ]lattice5__4461_13.min1.thm12017-02-06 12:45 229  
[ ]lattice5__4466_34.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__4473_15.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__4485_12.min1.thm12017-02-06 12:45 966  
[ ]lattice5__4486_16.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4487_51.min1.thm12017-02-06 12:45 779  
[ ]lattice5__4488_43.min1.thm12017-02-06 12:45 699  
[ ]lattice5__4495_16.min1.thm12017-02-06 12:45 845  
[ ]lattice5__4496_60.min1.thm12017-02-06 12:45 820  
[ ]lattice5__4497_52.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4503_53.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__4504_53.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__4505_33.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__4518_32.min1.thm12017-02-06 12:45 223  
[ ]lattice5__4530_20.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4532_34.min1.thm12017-02-06 12:45 405  
[ ]lattice5__4532_34.min1.thm1.tptp2017-02-06 16:47 331  
[ ]lattice5__4535_75.min1.thm12017-02-06 12:45 502  
[ ]lattice5__4535_75.min1.thm1.tptp2017-02-06 16:47 449  
[ ]lattice5__4549_19.min1.thm12017-02-06 12:45 376  
[ ]lattice5__4549_19.min1.thm1.tptp2017-02-06 16:47 306  
[ ]lattice5__4550_16.min1.thm12017-02-06 12:45 376  
[ ]lattice5__4550_16.min1.thm1.tptp2017-02-06 16:47 306  
[ ]lattice5__4552_8.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4553_41.min1.thm12017-02-06 12:45 2.4K 
[ ]lattice5__4556_13.min1.thm12017-02-06 12:45 613  
[ ]lattice5__4559_35.min1.thm12017-02-06 12:45 805  
[ ]lattice5__4561_71.min1.thm12017-02-06 12:45 759  
[ ]lattice5__4561_71.min1.thm1.tptp2017-02-06 16:47 711  
[ ]lattice5__4563_68.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__4566_15.min1.thm12017-02-06 12:45 471  
[ ]lattice5__4579_12.min1.thm12017-02-06 12:45 664  
[ ]lattice5__4587_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__4588_19.min1.thm12017-02-06 12:45 825  
[ ]lattice5__4590_30.min1.thm12017-02-06 12:45 536  
[ ]lattice5__4591_57.min1.thm12017-02-06 12:45 216  
[ ]lattice5__4603_16.min1.thm12017-02-06 12:45 612  
[ ]lattice5__4604_39.min1.thm12017-02-06 12:45 422  
[ ]lattice5__4605_20.min1.thm12017-02-06 12:45 867  
[ ]lattice5__4606_18.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__4612_14.min1.thm12017-02-06 12:45 771  
[ ]lattice5__4613_19.min1.thm12017-02-06 12:45 967  
[ ]lattice5__4619_46.min1.thm12017-02-06 12:45 414  
[ ]lattice5__4625_18.min1.thm12017-02-06 12:45 376  
[ ]lattice5__4625_18.min1.thm1.tptp2017-02-06 16:47 306  
[ ]lattice5__4626_19.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__4628_49.min1.thm12017-02-06 12:45 377  
[ ]lattice5__4628_49.min1.thm1.tptp2017-02-06 16:47 289  
[ ]lattice5__4637_23.min1.thm12017-02-06 12:45 808  
[ ]lattice5__4638_19.min1.thm12017-02-06 12:45 559  
[ ]lattice5__4639_39.min1.thm12017-02-06 12:45 766  
[ ]lattice5__4645_20.min1.thm12017-02-06 12:45 385  
[ ]lattice5__4645_20.min1.thm1.tptp2017-02-06 16:47 315  
[ ]lattice5__4646_20.min1.thm12017-02-06 12:45 385  
[ ]lattice5__4646_20.min1.thm1.tptp2017-02-06 16:47 315  
[ ]lattice5__4647_22.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__4648_20.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__4649_33.min1.thm12017-02-06 12:45 2.4K 
[ ]lattice5__4661_19.min1.thm12017-02-06 12:45 376  
[ ]lattice5__4661_19.min1.thm1.tptp2017-02-06 16:47 306  
[ ]lattice5__4662_12.min1.thm12017-02-06 12:45 491  
[ ]lattice5__4664_23.min1.thm12017-02-06 12:45 680  
[ ]lattice5__4665_18.min1.thm12017-02-06 12:45 377  
[ ]lattice5__4665_18.min1.thm1.tptp2017-02-06 16:47 307  
[ ]lattice5__4666_22.min1.thm12017-02-06 12:45 2.0K 
[ ]lattice5__4667_21.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__4668_22.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4669_19.min1.thm12017-02-06 12:45 860  
[ ]lattice5__4680_20.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4682_34.min1.thm12017-02-06 12:45 405  
[ ]lattice5__4682_34.min1.thm1.tptp2017-02-06 16:47 331  
[ ]lattice5__4684_24.min1.thm12017-02-06 12:45 408  
[ ]lattice5__4684_24.min1.thm1.tptp2017-02-06 16:47 355  
[ ]lattice5__4685_38.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4686_16.min1.thm12017-02-06 12:45 951  
[ ]lattice5__4693_15.min1.thm12017-02-06 12:45 849  
[ ]lattice5__4701_19.min1.thm12017-02-06 12:45 377  
[ ]lattice5__4701_19.min1.thm1.tptp2017-02-06 16:47 307  
[ ]lattice5__4703_15.min1.thm12017-02-06 12:45 707  
[ ]lattice5__4704_18.min1.thm12017-02-06 12:45 377  
[ ]lattice5__4704_18.min1.thm1.tptp2017-02-06 16:47 307  
[ ]lattice5__4706_8.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4711_15.min1.thm12017-02-06 12:45 850  
[ ]lattice5__4719_19.min1.thm12017-02-06 12:45 380  
[ ]lattice5__4719_19.min1.thm1.tptp2017-02-06 16:47 310  
[ ]lattice5__4721_15.min1.thm12017-02-06 12:45 718  
[ ]lattice5__4722_15.min1.thm12017-02-06 12:45 380  
[ ]lattice5__4722_15.min1.thm1.tptp2017-02-06 16:47 310  
[ ]lattice5__4724_15.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4727_13.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4732_19.min1.thm12017-02-06 12:45 773  
[ ]lattice5__4733_27.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4743_51.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__4744_27.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__4757_15.min1.thm12017-02-06 12:45 853  
[ ]lattice5__4765_20.min1.thm12017-02-06 12:45 381  
[ ]lattice5__4765_20.min1.thm1.tptp2017-02-06 16:47 311  
[ ]lattice5__4767_15.min1.thm12017-02-06 12:45 724  
[ ]lattice5__4768_15.min1.thm12017-02-06 12:45 381  
[ ]lattice5__4768_15.min1.thm1.tptp2017-02-06 16:47 311  
[ ]lattice5__4770_5.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4773_26.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4774_20.min1.thm12017-02-06 12:45 554  
[ ]lattice5__4777_15.min1.thm12017-02-06 12:45 854  
[ ]lattice5__4785_16.min1.thm12017-02-06 12:45 384  
[ ]lattice5__4785_16.min1.thm1.tptp2017-02-06 16:47 314  
[ ]lattice5__4787_15.min1.thm12017-02-06 12:45 737  
[ ]lattice5__4788_15.min1.thm12017-02-06 12:45 384  
[ ]lattice5__4788_15.min1.thm1.tptp2017-02-06 16:47 314  
[ ]lattice5__4790_5.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__4793_26.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4794_19.min1.thm12017-02-06 12:45 384  
[ ]lattice5__4794_19.min1.thm1.tptp2017-02-06 16:47 314  
[ ]lattice5__4797_15.min1.thm12017-02-06 12:45 854  
[ ]lattice5__4805_19.min1.thm12017-02-06 12:45 384  
[ ]lattice5__4805_19.min1.thm1.tptp2017-02-06 16:47 314  
[ ]lattice5__4807_15.min1.thm12017-02-06 12:45 737  
[ ]lattice5__4808_15.min1.thm12017-02-06 12:45 384  
[ ]lattice5__4808_15.min1.thm1.tptp2017-02-06 16:47 314  
[ ]lattice5__4810_5.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__4813_26.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4814_13.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4821_17.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4827_20.min1.thm12017-02-06 12:45 476  
[ ]lattice5__4828_60.min1.thm12017-02-06 12:45 818  
[ ]lattice5__4829_47.min1.thm12017-02-06 12:45 353  
[ ]lattice5__4829_47.min1.thm1.tptp2017-02-06 16:47 275  
[ ]lattice5__4842_47.min1.thm12017-02-06 12:45 353  
[ ]lattice5__4842_47.min1.thm1.tptp2017-02-06 16:47 275  
[ ]lattice5__4843_47.min1.thm12017-02-06 12:45 574  
[ ]lattice5__4844_47.min1.thm12017-02-06 12:45 582  
[ ]lattice5__4861_17.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__4867_17.min1.thm12017-02-06 12:45 476  
[ ]lattice5__4868_47.min1.thm12017-02-06 12:45 580  
[ ]lattice5__4869_47.min1.thm12017-02-06 12:45 826  
[ ]lattice5__4870_47.min1.thm12017-02-06 12:45 582  
[ ]lattice5__4884_14.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__4901_14.min1.thm12017-02-06 12:45 853  
[ ]lattice5__4909_18.min1.thm12017-02-06 12:45 381  
[ ]lattice5__4909_18.min1.thm1.tptp2017-02-06 16:47 311  
[ ]lattice5__4910_46.min1.thm12017-02-06 12:45 804  
[ ]lattice5__4911_18.min1.thm12017-02-06 12:45 381  
[ ]lattice5__4911_18.min1.thm1.tptp2017-02-06 16:47 311  
[ ]lattice5__4913_5.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4916_25.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4919_19.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4921_17.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__4942_68.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__4945_15.min1.thm12017-02-06 12:45 471  
[ ]lattice5__4948_14.min1.thm12017-02-06 12:45 773  
[ ]lattice5__4956_19.min1.thm12017-02-06 12:45 372  
[ ]lattice5__4956_19.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__4958_15.min1.thm12017-02-06 12:45 685  
[ ]lattice5__4959_16.min1.thm12017-02-06 12:45 372  
[ ]lattice5__4959_16.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__4960_71.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4963_22.min1.thm12017-02-06 12:45 372  
[ ]lattice5__4963_22.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__4966_17.min1.thm12017-02-06 12:45 476  
[ ]lattice5__4967_19.min1.thm12017-02-06 12:45 372  
[ ]lattice5__4967_19.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__4973_15.min1.thm12017-02-06 12:45 774  
[ ]lattice5__4981_19.min1.thm12017-02-06 12:45 372  
[ ]lattice5__4981_19.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__4983_15.min1.thm12017-02-06 12:45 686  
[ ]lattice5__4984_16.min1.thm12017-02-06 12:45 372  
[ ]lattice5__4984_16.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__4985_71.min1.thm12017-02-06 12:45 1.3K 
[ ]lattice5__4988_22.min1.thm12017-02-06 12:45 372  
[ ]lattice5__4988_22.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__4991_17.min1.thm12017-02-06 12:45 476  
[ ]lattice5__4992_19.min1.thm12017-02-06 12:45 372  
[ ]lattice5__4992_19.min1.thm1.tptp2017-02-06 16:47 302  
[ ]lattice5__4996_11.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5001_49.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5002_24.min1.thm12017-02-06 12:45 571  
[ ]lattice5__5004_58.min1.thm12017-02-06 12:45 656  
[ ]lattice5__5005_25.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5013_14.min1.thm12017-02-06 12:45 432  
[ ]lattice5__5014_25.min1.thm12017-02-06 12:45 572  
[ ]lattice5__5015_68.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5017_29.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5030_49.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5031_24.min1.thm12017-02-06 12:45 571  
[ ]lattice5__5033_58.min1.thm12017-02-06 12:45 656  
[ ]lattice5__5034_25.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5042_14.min1.thm12017-02-06 12:45 432  
[ ]lattice5__5043_25.min1.thm12017-02-06 12:45 572  
[ ]lattice5__5044_68.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5046_29.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5085_14.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5086_28.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5088_14.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5089_30.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__5091_37.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__5098_35.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5099_32.min1.thm12017-02-06 12:45 436  
[ ]lattice5__5099_32.min1.thm1.tptp2017-02-06 16:47 348  
[ ]lattice5__5112_15.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5129_16.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__5162_22.min1.thm12017-02-06 12:45 956  
[ ]lattice5__5163_17.min1.thm12017-02-06 12:45 852  
[ ]lattice5__5164_15.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5165_15.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5172_15.min1.thm12017-02-06 12:45 769  
[ ]lattice5__5173_16.min1.thm12017-02-06 12:45 1.9K 
[ ]lattice5__5176_21.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5177_21.min1.thm12017-02-06 12:45 624  
[ ]lattice5__5181_22.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5182_21.min1.thm12017-02-06 12:45 624  
[ ]lattice5__5186_22.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5187_21.min1.thm12017-02-06 12:45 624  
[ ]lattice5__5191_22.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5192_21.min1.thm12017-02-06 12:45 624  
[ ]lattice5__5196_21.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5197_21.min1.thm12017-02-06 12:45 624  
[ ]lattice5__5200_43.min1.thm12017-02-06 12:45 635  
[ ]lattice5__5201_48.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__5202_15.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5209_16.min1.thm12017-02-06 12:45 848  
[ ]lattice5__5212_22.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5218_23.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5221_18.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5226_23.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5229_16.min1.thm12017-02-06 12:45 950  
[ ]lattice5__5234_22.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5237_16.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5244_11.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5258_13.min1.thm12017-02-06 12:45 408  
[ ]lattice5__5258_13.min1.thm1.tptp2017-02-06 16:47 338  
[ ]lattice5__5259_17.min1.thm12017-02-06 12:45 928  
[ ]lattice5__5260_37.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5268_38.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5279_21.min1.thm12017-02-06 12:45 544  
[ ]lattice5__5279_21.min1.thm1.tptp2017-02-06 16:47 474  
[ ]lattice5__5285_56.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5292_21.min1.thm12017-02-06 12:45 544  
[ ]lattice5__5292_21.min1.thm1.tptp2017-02-06 16:47 474  
[ ]lattice5__5296_16.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5299_54.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5306_16.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5315_20.min1.thm12017-02-06 12:45 1.7K 
[ ]lattice5__5348_29.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5349_18.min1.thm12017-02-06 12:45 878  
[ ]lattice5__5350_16.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5351_16.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5352_16.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5354_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5355_16.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5362_20.min1.thm12017-02-06 12:45 756  
[ ]lattice5__5367_33.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__5374_33.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__5381_33.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__5388_33.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__5392_16.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5393_23.min1.thm12017-02-06 12:45 943  
[ ]lattice5__5398_21.min1.thm12017-02-06 12:45 544  
[ ]lattice5__5398_21.min1.thm1.tptp2017-02-06 16:47 474  
[ ]lattice5__5404_56.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5412_24.min1.thm12017-02-06 12:45 2.1K 
[ ]lattice5__5415_24.min1.thm12017-02-06 12:45 3.7K 
[ ]lattice5__5418_23.min1.thm12017-02-06 12:45 1.4K 
[ ]lattice5__5421_67.min1.thm12017-02-06 12:45 2.8K 
[ ]lattice5__5422_32.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__5423_33.min1.thm12017-02-06 12:45 1.8K 
[ ]lattice5__5430_24.min1.thm12017-02-06 12:45 439  
[ ]lattice5__5430_24.min1.thm1.tptp2017-02-06 16:47 374  
[ ]lattice5__5442_31.min1.thm12017-02-06 12:45 944  
[ ]lattice5__5463_39.min1.thm12017-02-06 12:45 497  
[ ]lattice5__5465_43.min1.thm12017-02-06 12:45 796  
[ ]lattice5__5465_43.min1.thm1.tptp2017-02-06 16:47 734  
[ ]lattice5__5468_40.min1.thm12017-02-06 12:45 2.2K 
[ ]lattice5__5470_31.min1.thm12017-02-06 12:45 590  
[ ]lattice5__5473_47.min1.thm12017-02-06 12:45 1.1K 
[ ]lattice5__5474_37.min1.thm12017-02-06 12:45 1.5K 
[ ]lattice5__5477_23.min1.thm12017-02-06 12:45 783  
[ ]lattice5__5478_26.min1.thm12017-02-06 12:45 785  
[ ]lattice5__5479_37.min1.thm12017-02-06 12:45 486  
[ ]lattice5__5480_45.min1.thm12017-02-06 12:45 774  
[ ]lattice5__5480_45.min1.thm1.tptp2017-02-06 16:47 712  
[ ]lattice5__5481_58.min1.thm12017-02-06 12:45 1.2K 
[ ]lattice5__5491_46.min1.thm12017-02-06 12:45 1.6K 
[ ]lattice5__5494_13.min1.thm12017-02-06 12:45 2.5K 
[ ]lattice5__5499_14.min1.thm12017-02-06 12:45 654  
[ ]lattice5__5499_14.min1.thm1.tptp2017-02-06 16:47 577  
[ ]lattice5__5508_15.min1.thm12017-02-06 12:45 411  
[ ]lattice5__5508_15.min1.thm1.tptp2017-02-06 16:47 341  
[ ]lattice5__5516_15.min1.thm12017-02-06 12:45 411  
[ ]lattice5__5516_15.min1.thm1.tptp2017-02-06 16:47 341  
[ ]lattice5__5517_19.min1.thm12017-02-06 12:45 1.0K 
[ ]lattice5__5518_32.min1.thm12017-02-06 12:45 487  
[ ]lattice5__5518_32.min1.thm1.tptp2017-02-06 16:47 419  
[ ]lattice5__5524_20.min1.thm12017-02-06 12:45 1.2K 
Apache/2.4.18 (Ubuntu) Server at grid01.ciirc.cvut.cz Port 80