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

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[ ]abcmiz_0__781_36.min1.thm1.tptp2017-02-06 16:57 270  
[ ]abcmiz_1__385_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]abcmiz_1__1544_56.min1.thm1.tptp2017-02-06 16:57 448  
[ ]abcmiz_1__1629_49.min1.thm1.tptp2017-02-06 16:57 285  
[ ]abcmiz_1__1796_6.min1.thm1.tptp2017-02-06 16:57 524  
[ ]abcmiz_1__1813_48.min1.thm1.tptp2017-02-06 16:57 262  
[ ]abcmiz_1__1826_48.min1.thm1.tptp2017-02-06 16:57 262  
[ ]abcmiz_1__2226_45.min1.thm1.tptp2017-02-06 16:57 278  
[ ]abcmiz_1__2356_45.min1.thm1.tptp2017-02-06 16:57 278  
[ ]abcmiz_1__3766_51.min1.thm1.tptp2017-02-06 16:57 416  
[ ]abcmiz_1__3893_56.min1.thm1.tptp2017-02-06 16:57 344  
[ ]abcmiz_1__4096_40.min1.thm1.tptp2017-02-06 16:57 444  
[ ]abcmiz_1__4884_38.min1.thm1.tptp2017-02-06 16:57 284  
[ ]abcmiz_1__5434_38.min1.thm1.tptp2017-02-06 16:57 284  
[ ]abcmiz_1__5684_38.min1.thm1.tptp2017-02-06 16:57 284  
[ ]abcmiz_1__6701_44.min1.thm1.tptp2017-02-06 16:57 428  
[ ]abcmiz_1__6724_44.min1.thm1.tptp2017-02-06 16:57 428  
[ ]abcmiz_a__600_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]abcmiz_a__621_37.min1.thm1.tptp2017-02-06 16:57 294  
[ ]abcmiz_a__664_39.min1.thm1.tptp2017-02-06 16:57 290  
[ ]abcmiz_a__673_38.min1.thm1.tptp2017-02-06 16:57 454  
[ ]abcmiz_a__1054_38.min1.thm1.tptp2017-02-06 16:57 454  
[ ]abcmiz_a__1139_49.min1.thm1.tptp2017-02-06 16:57 352  
[ ]abcmiz_a__1239_49.min1.thm1.tptp2017-02-06 16:57 352  
[ ]abcmiz_a__1760_35.min1.thm1.tptp2017-02-06 16:57 294  
[ ]abcmiz_a__1934_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]afinsq_2__3199_44.min1.thm1.tptp2017-02-06 16:57 352  
[ ]afinsq_2__3222_43.min1.thm1.tptp2017-02-06 16:57 352  
[ ]afinsq_2__3245_43.min1.thm1.tptp2017-02-06 16:57 352  
[ ]afinsq_2__4095_31.min1.thm1.tptp2017-02-06 16:57 257  
[ ]afinsq_2__4096_44.min1.thm1.tptp2017-02-06 16:57 257  
[ ]afinsq_2__4129_31.min1.thm1.tptp2017-02-06 16:57 257  
[ ]afinsq_2__4130_44.min1.thm1.tptp2017-02-06 16:57 257  
[ ]afproj__679_36.min1.thm1.tptp2017-02-06 16:57 258  
[ ]afvect0__1261_40.min1.thm1.tptp2017-02-06 16:57 272  
[ ]alg_1__992_34.min1.thm1.tptp2017-02-06 16:57 252  
[ ]alg_1__1017_45.min1.thm1.tptp2017-02-06 16:57 276  
[ ]alg_1__1029_57.min1.thm1.tptp2017-02-06 16:57 512  
[ ]alg_1__1039_49.min1.thm1.tptp2017-02-06 16:57 394  
[ ]alg_1__1147_38.min1.thm1.tptp2017-02-06 16:57 276  
[ ]alg_1__1272_36.min1.thm1.tptp2017-02-06 16:57 260  
[ ]alg_1__1276_36.min1.thm1.tptp2017-02-06 16:57 262  
[ ]algseq_1__243_41.min1.thm1.tptp2017-02-06 16:57 242  
[ ]algseq_1__266_35.min1.thm1.tptp2017-02-06 16:57 270  
[ ]algspec1__930_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]algspec1__1895_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]algspec1__1913_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]algstr_1__87_14.min1.thm1.tptp2017-02-06 16:57 292  
[ ]algstr_4__307_39.min1.thm1.tptp2017-02-06 16:57 440  
[ ]algstr_4__311_39.min1.thm1.tptp2017-02-06 16:57 440  
[ ]algstr_4__350_45.min1.thm1.tptp2017-02-06 16:57 358  
[ ]algstr_4__352_45.min1.thm1.tptp2017-02-06 16:57 358  
[ ]algstr_4__403_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]algstr_4__474_37.min1.thm1.tptp2017-02-06 16:57 428  
[ ]algstr_4__731_37.min1.thm1.tptp2017-02-06 16:57 469  
[ ]algstr_4__880_41.min1.thm1.tptp2017-02-06 16:57 400  
[ ]algstr_4__2803_60.min1.thm1.tptp2017-02-06 16:57 526  
[ ]altcat_1__196_57.min1.thm1.tptp2017-02-06 16:57 483  
[ ]altcat_1__972_50.min1.thm1.tptp2017-02-06 16:57 398  
[ ]altcat_1__973_50.min1.thm1.tptp2017-02-06 16:57 398  
[ ]altcat_1__1232_44.min1.thm1.tptp2017-02-06 16:57 476  
[ ]altcat_2__588_44.min1.thm1.tptp2017-02-06 16:57 436  
[ ]altcat_2__807_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]altcat_2__1201_40.min1.thm1.tptp2017-02-06 16:57 507  
[ ]altcat_3__1247_46.min1.thm1.tptp2017-02-06 16:57 342  
[ ]altcat_3__1336_46.min1.thm1.tptp2017-02-06 16:57 342  
[ ]altcat_4__297_39.min1.thm1.tptp2017-02-06 16:57 334  
[ ]altcat_4__406_38.min1.thm1.tptp2017-02-06 16:57 389  
[ ]altcat_4__442_38.min1.thm1.tptp2017-02-06 16:57 388  
[ ]altcat_4__1098_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__1133_45.min1.thm1.tptp2017-02-06 16:57 554  
[ ]altcat_4__1342_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__1404_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__1439_45.min1.thm1.tptp2017-02-06 16:57 554  
[ ]altcat_4__1648_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__1709_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__1744_45.min1.thm1.tptp2017-02-06 16:57 554  
[ ]altcat_4__1964_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__2029_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__2065_45.min1.thm1.tptp2017-02-06 16:57 554  
[ ]altcat_4__2285_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__2351_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__2386_45.min1.thm1.tptp2017-02-06 16:57 554  
[ ]altcat_4__2605_41.min1.thm1.tptp2017-02-06 16:57 424  
[ ]altcat_4__2859_39.min1.thm1.tptp2017-02-06 16:57 400  
[ ]altcat_4__2891_39.min1.thm1.tptp2017-02-06 16:57 400  
[ ]altcat_4__2924_39.min1.thm1.tptp2017-02-06 16:57 400  
[ ]altcat_4__2957_39.min1.thm1.tptp2017-02-06 16:57 400  
[ ]altcat_4__2990_39.min1.thm1.tptp2017-02-06 16:57 400  
[ ]ami_2__473_39.min1.thm1.tptp2017-02-06 16:57 222  
[ ]ami_5__50_39.min1.thm1.tptp2017-02-06 16:57 218  
[ ]ami_6__352_37.min1.thm1.tptp2017-02-06 16:57 222  
[ ]ami_6__389_37.min1.thm1.tptp2017-02-06 16:57 222  
[ ]ami_6__426_37.min1.thm1.tptp2017-02-06 16:57 222  
[ ]amistd_4__322_42.min1.thm1.tptp2017-02-06 16:57 346  
[ ]aofa_000__1846_39.min1.thm1.tptp2017-02-06 16:57 272  
[ ]aofa_000__3724_35.min1.thm1.tptp2017-02-06 16:57 258  
[ ]aofa_000__6073_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]aofa_000__6376_35.min1.thm1.tptp2017-02-06 16:57 258  
[ ]aofa_000__6549_35.min1.thm1.tptp2017-02-06 16:57 258  
[ ]aofa_000__6692_35.min1.thm1.tptp2017-02-06 16:57 284  
[ ]aofa_000__6693_35.min1.thm1.tptp2017-02-06 16:57 258  
[ ]aofa_i00__635_39.min1.thm1.tptp2017-02-06 16:57 268  
[ ]aofa_i00__896_33.min1.thm1.tptp2017-02-06 16:57 244  
[ ]armstrng__312_37.min1.thm1.tptp2017-02-06 16:57 252  
[ ]armstrng__2575_40.min1.thm1.tptp2017-02-06 16:57 244  
[ ]armstrng__3580_40.min1.thm1.tptp2017-02-06 16:57 276  
[ ]arytm_0__166_52.min1.thm1.tptp2017-02-06 16:57 316  
[ ]arytm_0__175_46.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_0__181_42.min1.thm1.tptp2017-02-06 16:57 250  
[ ]arytm_0__188_46.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_0__194_42.min1.thm1.tptp2017-02-06 16:57 250  
[ ]arytm_0__214_40.min1.thm1.tptp2017-02-06 16:57 244  
[ ]arytm_0__215_40.min1.thm1.tptp2017-02-06 16:57 244  
[ ]arytm_0__262_52.min1.thm1.tptp2017-02-06 16:57 316  
[ ]arytm_0__270_46.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_0__276_42.min1.thm1.tptp2017-02-06 16:57 250  
[ ]arytm_0__288_46.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_0__294_42.min1.thm1.tptp2017-02-06 16:57 250  
[ ]arytm_0__310_42.min1.thm1.tptp2017-02-06 16:57 250  
[ ]arytm_0__316_42.min1.thm1.tptp2017-02-06 16:57 252  
[ ]arytm_0__387_46.min1.thm1.tptp2017-02-06 16:57 246  
[ ]arytm_0__546_50.min1.thm1.tptp2017-02-06 16:57 250  
[ ]arytm_0__563_44.min1.thm1.tptp2017-02-06 16:57 270  
[ ]arytm_0__959_46.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_0__972_45.min1.thm1.tptp2017-02-06 16:57 246  
[ ]arytm_1__30_42.min1.thm1.tptp2017-02-06 16:57 256  
[ ]arytm_1__36_41.min1.thm1.tptp2017-02-06 16:57 253  
[ ]arytm_1__162_18.min1.thm1.tptp2017-02-06 16:57 338  
[ ]arytm_2__200_46.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__540_55.min1.thm1.tptp2017-02-06 16:57 338  
[ ]arytm_2__752_53.min1.thm1.tptp2017-02-06 16:57 318  
[ ]arytm_2__1186_53.min1.thm1.tptp2017-02-06 16:57 318  
[ ]arytm_2__1198_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1218_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1301_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1302_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1303_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1312_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1313_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1328_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1329_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1343_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1362_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1363_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1384_43.min1.thm1.tptp2017-02-06 16:57 239  
[ ]arytm_2__1406_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]arytm_2__1475_46.min1.thm1.tptp2017-02-06 16:57 254  
[ ]arytm_2__1484_44.min1.thm1.tptp2017-02-06 16:57 248  
[ ]arytm_2__1537_50.min1.thm1.tptp2017-02-06 16:57 250  
[ ]arytm_2__1588_45.min1.thm1.tptp2017-02-06 16:57 256  
[ ]arytm_2__1613_46.min1.thm1.tptp2017-02-06 16:57 254  
[ ]arytm_2__1622_44.min1.thm1.tptp2017-02-06 16:57 248  
[ ]arytm_2__2532_43.min1.thm1.tptp2017-02-06 16:57 234  
[ ]arytm_2__2541_43.min1.thm1.tptp2017-02-06 16:57 234  
[ ]arytm_2__2602_52.min1.thm1.tptp2017-02-06 16:57 314  
[ ]arytm_2__2651_43.min1.thm1.tptp2017-02-06 16:57 232  
[ ]arytm_2__2676_41.min1.thm1.tptp2017-02-06 16:57 232  
[ ]arytm_2__2724_43.min1.thm1.tptp2017-02-06 16:57 234  
[ ]arytm_2__2733_43.min1.thm1.tptp2017-02-06 16:57 234  
[ ]autgroup__532_9.min1.thm1.tptp2017-02-06 16:57 301  
[ ]axioms__162_44.min1.thm1.tptp2017-02-06 16:57 264  
[ ]axioms__190_44.min1.thm1.tptp2017-02-06 16:57 264  
[ ]axioms__227_44.min1.thm1.tptp2017-02-06 16:57 266  
[ ]axioms__248_48.min1.thm1.tptp2017-02-06 16:57 286  
[ ]axioms__263_44.min1.thm1.tptp2017-02-06 16:57 262  
[ ]axioms__311_54.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bagorder__3452_43.min1.thm1.tptp2017-02-06 16:57 304  
[ ]bagorder__3497_43.min1.thm1.tptp2017-02-06 16:57 304  
[ ]bagorder__3689_43.min1.thm1.tptp2017-02-06 16:57 305  
[ ]bcialg_2__1332_41.min1.thm1.tptp2017-02-06 16:57 302  
[ ]bcialg_2__1375_41.min1.thm1.tptp2017-02-06 16:57 436  
[ ]bcialg_2__1644_37.min1.thm1.tptp2017-02-06 16:57 400  
[ ]bcialg_2__1665_37.min1.thm1.tptp2017-02-06 16:57 400  
[ ]bcialg_2__1851_37.min1.thm1.tptp2017-02-06 16:57 400  
[ ]bcialg_2__1872_37.min1.thm1.tptp2017-02-06 16:57 400  
[ ]bcialg_2__1894_37.min1.thm1.tptp2017-02-06 16:57 400  
[ ]bcialg_2__1915_37.min1.thm1.tptp2017-02-06 16:57 400  
[ ]bcialg_2__2151_36.min1.thm1.tptp2017-02-06 16:57 278  
[ ]bcialg_2__2180_36.min1.thm1.tptp2017-02-06 16:57 278  
[ ]bcialg_4__749_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]bcialg_6__72_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]bcialg_6__1837_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]bcialg_6__1865_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]bcialg_6__2024_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]bcialg_6__2441_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]bciideal__725_8.min1.thm1.tptp2017-02-06 16:57 293  
[ ]bhsp_5__1023_40.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bhsp_5__1027_41.min1.thm1.tptp2017-02-06 16:57 274  
[ ]binom__174_48.min1.thm1.tptp2017-02-06 16:57 250  
[ ]binom__297_35.min1.thm1.tptp2017-02-06 16:57 236  
[ ]binom__298_37.min1.thm1.tptp2017-02-06 16:57 234  
[ ]binom__457_48.min1.thm1.tptp2017-02-06 16:57 250  
[ ]binom__580_35.min1.thm1.tptp2017-02-06 16:57 236  
[ ]binom__581_37.min1.thm1.tptp2017-02-06 16:57 234  
[ ]binom__1146_37.min1.thm1.tptp2017-02-06 16:57 276  
[ ]binom__1147_39.min1.thm1.tptp2017-02-06 16:57 246  
[ ]binom__1207_37.min1.thm1.tptp2017-02-06 16:57 276  
[ ]binom__1208_39.min1.thm1.tptp2017-02-06 16:57 246  
[ ]binop_1__82_69.min1.thm1.tptp2017-02-06 16:57 463  
[ ]binop_1__182_38.min1.thm1.tptp2017-02-06 16:57 248  
[ ]binop_1__183_38.min1.thm1.tptp2017-02-06 16:57 248  
[ ]binop_1__739_66.min1.thm1.tptp2017-02-06 16:57 478  
[ ]bintree1__1234_48.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bintree1__1260_46.min1.thm1.tptp2017-02-06 16:57 266  
[ ]bintree1__1286_48.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bintree1__1312_46.min1.thm1.tptp2017-02-06 16:57 266  
[ ]birkhoff__75_42.min1.thm1.tptp2017-02-06 16:57 264  
[ ]birkhoff__131_46.min1.thm1.tptp2017-02-06 16:57 280  
[ ]birkhoff__261_46.min1.thm1.tptp2017-02-06 16:57 284  
[ ]birkhoff__763_46.min1.thm1.tptp2017-02-06 16:57 280  
[ ]birkhoff__971_46.min1.thm1.tptp2017-02-06 16:57 286  
[ ]birkhoff__1072_9.min1.thm1.tptp2017-02-06 16:57 309  
[ ]borsuk_1__1233_31.min1.thm1.tptp2017-02-06 16:57 270  
[ ]borsuk_1__1607_37.min1.thm1.tptp2017-02-06 16:57 270  
[ ]borsuk_1__1665_37.min1.thm1.tptp2017-02-06 16:57 270  
[ ]borsuk_1__1935_46.min1.thm1.tptp2017-02-06 16:57 306  
[ ]borsuk_2__861_43.min1.thm1.tptp2017-02-06 16:57 268  
[ ]borsuk_2__965_46.min1.thm1.tptp2017-02-06 16:57 284  
[ ]borsuk_6__56_61.min1.thm1.tptp2017-02-06 16:57 389  
[ ]borsuk_6__58_48.min1.thm1.tptp2017-02-06 16:57 540  
[ ]borsuk_6__431_63.min1.thm1.tptp2017-02-06 16:57 306  
[ ]borsuk_6__1544_40.min1.thm1.tptp2017-02-06 16:57 380  
[ ]borsuk_6__1685_41.min1.thm1.tptp2017-02-06 16:57 284  
[ ]borsuk_6__1837_41.min1.thm1.tptp2017-02-06 16:57 284  
[ ]borsuk_6__2001_41.min1.thm1.tptp2017-02-06 16:57 284  
[ ]borsuk_7__1025_35.min1.thm1.tptp2017-02-06 16:57 242  
[ ]borsuk_7__2494_36.min1.thm1.tptp2017-02-06 16:57 272  
[ ]bspace__321_40.min1.thm1.tptp2017-02-06 16:57 404  
[ ]bspace__352_36.min1.thm1.tptp2017-02-06 16:57 282  
[ ]bspace__353_36.min1.thm1.tptp2017-02-06 16:57 282  
[ ]bspace__446_36.min1.thm1.tptp2017-02-06 16:57 282  
[ ]bspace__447_39.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bspace__480_36.min1.thm1.tptp2017-02-06 16:57 282  
[ ]bspace__481_39.min1.thm1.tptp2017-02-06 16:57 274  
[ ]bvfunc_1__2538_39.min1.thm1.tptp2017-02-06 16:57 268  
[ ]bvfunc_2__206_39.min1.thm1.tptp2017-02-06 16:57 262  
[ ]bvfunc_2__429_41.min1.thm1.tptp2017-02-06 16:57 270  
[ ]c0sp1__576_29.min1.thm1.tptp2017-02-06 16:57 246  
[ ]c0sp2__1110_59.min1.thm1.tptp2017-02-06 16:57 327  
[ ]card_3__2794_35.min1.thm1.tptp2017-02-06 16:57 238  
[ ]card_4__361_43.min1.thm1.tptp2017-02-06 16:57 234  
[ ]card_4__453_43.min1.thm1.tptp2017-02-06 16:57 234  
[ ]card_5__1320_37.min1.thm1.tptp2017-02-06 16:57 240  
[ ]card_5__1774_44.min1.thm1.tptp2017-02-06 16:57 248  
[ ]card_fil__1434_43.min1.thm1.tptp2017-02-06 16:57 260  
[ ]card_fil__1984_48.min1.thm1.tptp2017-02-06 16:57 323  
[ ]card_fil__2036_43.min1.thm1.tptp2017-02-06 16:57 260  
[ ]card_lar__301_16.min1.thm1.tptp2017-02-06 16:57 480  
[ ]card_lar__568_38.min1.thm1.tptp2017-02-06 16:57 244  
[ ]card_lar__614_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]card_lar__804_42.min1.thm1.tptp2017-02-06 16:57 252  
[ ]cat_2__253_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]cat_2__1549_43.min1.thm1.tptp2017-02-06 16:57 268  
[ ]cat_2__1550_43.min1.thm1.tptp2017-02-06 16:57 269  
[ ]cat_5__656_44.min1.thm1.tptp2017-02-06 16:57 266  
[ ]cat_5__667_44.min1.thm1.tptp2017-02-06 16:57 266  
[ ]cat_5__1096_49.min1.thm1.tptp2017-02-06 16:57 284  
[ ]cat_5__1117_49.min1.thm1.tptp2017-02-06 16:57 278  
[ ]cat_5__1412_46.min1.thm1.tptp2017-02-06 16:57 296  
[ ]cat_5__1588_40.min1.thm1.tptp2017-02-06 16:57 260  
[ ]cat_5__1649_18.min1.thm1.tptp2017-02-06 16:57 625  
[ ]cat_5__1863_44.min1.thm1.tptp2017-02-06 16:57 260  
[ ]cat_5__1874_44.min1.thm1.tptp2017-02-06 16:57 260  
[ ]cat_5__1992_40.min1.thm1.tptp2017-02-06 16:57 260  
[ ]cat_5__2154_37.min1.thm1.tptp2017-02-06 16:57 234  
[ ]cat_5__2185_46.min1.thm1.tptp2017-02-06 16:57 264  
[ ]cat_5__2273_45.min1.thm1.tptp2017-02-06 16:57 268  
[ ]cat_5__2283_43.min1.thm1.tptp2017-02-06 16:57 260  
[ ]cat_5__2418_38.min1.thm1.tptp2017-02-06 16:57 260  
[ ]catalan2__3448_31.min1.thm1.tptp2017-02-06 16:57 242  
[ ]catalg_1__1301_33.min1.thm1.tptp2017-02-06 16:57 244  
[ ]catalg_1__1322_37.min1.thm1.tptp2017-02-06 16:57 428  
[ ]catalg_1__1382_41.min1.thm1.tptp2017-02-06 16:57 425  
[ ]catalg_1__1452_40.min1.thm1.tptp2017-02-06 16:57 310  
[ ]catalg_1__1480_46.min1.thm1.tptp2017-02-06 16:57 586  
[ ]catalg_1__1612_44.min1.thm1.tptp2017-02-06 16:57 322  
[ ]catalg_1__1786_41.min1.thm1.tptp2017-02-06 16:57 310  
[ ]catalg_1__1897_69.min1.thm1.tptp2017-02-06 16:57 346  
[ ]catalg_1__2112_43.min1.thm1.tptp2017-02-06 16:57 324  
[ ]cayley__441_37.min1.thm1.tptp2017-02-06 16:57 280  
[ ]cc0sp2__1601_59.min1.thm1.tptp2017-02-06 16:57 335  
[ ]cfdiff_1__268_50.min1.thm1.tptp2017-02-06 16:57 572  
[ ]chord__2012_41.min1.thm1.tptp2017-02-06 16:57 256  
[ ]chord__2029_39.min1.thm1.tptp2017-02-06 16:57 252  
[ ]chord__3486_40.min1.thm1.tptp2017-02-06 16:57 234  
[ ]circcmb2__81_40.min1.thm1.tptp2017-02-06 16:57 328  
[ ]circcmb2__1560_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]circcmb2__1622_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]circcmb2__1660_43.min1.thm1.tptp2017-02-06 16:57 286  
[ ]circcmb2__1679_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]circcomb__890_39.min1.thm1.tptp2017-02-06 16:57 328  
[ ]circcomb__1063_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]circcomb__1093_40.min1.thm1.tptp2017-02-06 16:57 274  
[ ]circcomb__1549_38.min1.thm1.tptp2017-02-06 16:57 284  
[ ]circcomb__1777_32.min1.thm1.tptp2017-02-06 16:57 328  
[ ]circcomb__1792_40.min1.thm1.tptp2017-02-06 16:57 274  
[ ]circcomb__1819_30.min1.thm1.tptp2017-02-06 16:57 328  
[ ]circcomb__1836_40.min1.thm1.tptp2017-02-06 16:57 274  
[ ]circcomb__2192_11.min1.thm1.tptp2017-02-06 16:57 428  
[ ]circtrm1__565_39.min1.thm1.tptp2017-02-06 16:57 258  
[ ]circtrm1__617_53.min1.thm1.tptp2017-02-06 16:57 384  
[ ]circtrm1__641_47.min1.thm1.tptp2017-02-06 16:57 376  
[ ]circtrm1__717_51.min1.thm1.tptp2017-02-06 16:57 384  
[ ]circtrm1__730_51.min1.thm1.tptp2017-02-06 16:57 384  
[ ]circtrm1__768_40.min1.thm1.tptp2017-02-06 16:57 296  
[ ]circtrm1__845_45.min1.thm1.tptp2017-02-06 16:57 360  
[ ]circtrm1__1563_14.min1.thm1.tptp2017-02-06 16:57 891  
[ ]circtrm1__1582_14.min1.thm1.tptp2017-02-06 16:57 819  
[ ]circuit2__244_44.min1.thm1.tptp2017-02-06 16:57 288  
[ ]circuit2__328_44.min1.thm1.tptp2017-02-06 16:57 288  
[ ]circuit2__447_44.min1.thm1.tptp2017-02-06 16:57 288  
[ ]circuit2__1816_43.min1.thm1.tptp2017-02-06 16:57 278  
[ ]circuit2__1845_43.min1.thm1.tptp2017-02-06 16:57 278  
[ ]clopban3__1278_44.min1.thm1.tptp2017-02-06 16:57 358  
[ ]clvect_1__1103_48.min1.thm1.tptp2017-02-06 16:57 242  
[ ]coh_sp__995_59.min1.thm1.tptp2017-02-06 16:57 396  
[ ]coh_sp__1007_59.min1.thm1.tptp2017-02-06 16:57 396  
[ ]coh_sp__1825_59.min1.thm1.tptp2017-02-06 16:57 400  
[ ]coh_sp__1837_59.min1.thm1.tptp2017-02-06 16:57 400  
[ ]cohsp_1__1918_36.min1.thm1.tptp2017-02-06 16:57 294  
[ ]cohsp_1__2890_46.min1.thm1.tptp2017-02-06 16:57 298  
[ ]cohsp_1__4003_36.min1.thm1.tptp2017-02-06 16:57 260  
[ ]cohsp_1__4014_36.min1.thm1.tptp2017-02-06 16:57 260  
[ ]cohsp_1__4090_36.min1.thm1.tptp2017-02-06 16:57 260  
[ ]cohsp_1__4101_36.min1.thm1.tptp2017-02-06 16:57 260  
[ ]collsp__408_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]combgras__786_38.min1.thm1.tptp2017-02-06 16:57 330  
[ ]combgras__1356_21.min1.thm1.tptp2017-02-06 16:57 475  
[ ]combgras__1371_21.min1.thm1.tptp2017-02-06 16:57 479  
[ ]combgras__1501_20.min1.thm1.tptp2017-02-06 16:57 459  
[ ]combgras__1573_20.min1.thm1.tptp2017-02-06 16:57 453  
[ ]combgras__1642_20.min1.thm1.tptp2017-02-06 16:57 463  
[ ]combgras__1662_18.min1.thm1.tptp2017-02-06 16:57 435  
[ ]combgras__1749_18.min1.thm1.tptp2017-02-06 16:57 433  
[ ]combgras__1839_11.min1.thm1.tptp2017-02-06 16:57 361  
[ ]combgras__1898_11.min1.thm1.tptp2017-02-06 16:57 357  
[ ]combgras__1918_17.min1.thm1.tptp2017-02-06 16:57 443  
[ ]combgras__1974_17.min1.thm1.tptp2017-02-06 16:57 443  
[ ]combgras__1988_19.min1.thm1.tptp2017-02-06 16:57 443  
[ ]combgras__2030_11.min1.thm1.tptp2017-02-06 16:57 351  
[ ]combgras__2035_11.min1.thm1.tptp2017-02-06 16:57 351  
[ ]combgras__2114_24.min1.thm1.tptp2017-02-06 16:57 497  
[ ]combgras__2125_17.min1.thm1.tptp2017-02-06 16:57 417  
[ ]combgras__2132_17.min1.thm1.tptp2017-02-06 16:57 417  
[ ]combgras__2631_9.min1.thm1.tptp2017-02-06 16:57 299  
[ ]combgras__2643_9.min1.thm1.tptp2017-02-06 16:57 299  
[ ]combgras__2790_10.min1.thm1.tptp2017-02-06 16:57 299  
[ ]combgras__3029_16.min1.thm1.tptp2017-02-06 16:57 453  
[ ]combgras__3039_16.min1.thm1.tptp2017-02-06 16:57 453  
[ ]combgras__3042_11.min1.thm1.tptp2017-02-06 16:57 359  
[ ]combgras__3045_16.min1.thm1.tptp2017-02-06 16:57 453  
[ ]combgras__3186_11.min1.thm1.tptp2017-02-06 16:57 357  
[ ]combgras__3214_17.min1.thm1.tptp2017-02-06 16:57 453  
[ ]combgras__3220_17.min1.thm1.tptp2017-02-06 16:57 453  
[ ]combgras__3288_17.min1.thm1.tptp2017-02-06 16:57 453  
[ ]combgras__3522_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]combgras__3746_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]combgras__4343_12.min1.thm1.tptp2017-02-06 16:57 391  
[ ]combgras__4356_24.min1.thm1.tptp2017-02-06 16:57 515  
[ ]combgras__4530_12.min1.thm1.tptp2017-02-06 16:57 413  
[ ]combgras__4556_12.min1.thm1.tptp2017-02-06 16:57 413  
[ ]compl_sp__73_33.min1.thm1.tptp2017-02-06 16:57 280  
[ ]compl_sp__445_33.min1.thm1.tptp2017-02-06 16:57 286  
[ ]compl_sp__476_33.min1.thm1.tptp2017-02-06 16:57 286  
[ ]compl_sp__2826_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]compl_sp__3118_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]comput_1__488_37.min1.thm1.tptp2017-02-06 16:57 260  
[ ]comput_1__548_37.min1.thm1.tptp2017-02-06 16:57 260  
[ ]comput_1__1497_44.min1.thm1.tptp2017-02-06 16:57 242  
[ ]conlat_1__1225_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_1__1241_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_1__1552_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_1__1582_36.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_2__1142_39.min1.thm1.tptp2017-02-06 16:57 294  
[ ]conlat_2__1210_55.min1.thm1.tptp2017-02-06 16:57 294  
[ ]conlat_2__1918_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_2__2072_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]conlat_2__2890_57.min1.thm1.tptp2017-02-06 16:57 348  
[ ]conlat_2__3075_55.min1.thm1.tptp2017-02-06 16:57 332  
[ ]connsp_3__166_42.min1.thm1.tptp2017-02-06 16:57 276  
[ ]connsp_3__499_38.min1.thm1.tptp2017-02-06 16:57 278  
[ ]convex4__201_43.min1.thm1.tptp2017-02-06 16:57 282  
[ ]convfun1__142_37.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__143_37.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__187_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__188_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__233_37.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__234_37.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__239_37.min1.thm1.tptp2017-02-06 16:57 289  
[ ]convfun1__240_37.min1.thm1.tptp2017-02-06 16:57 289  
[ ]convfun1__261_37.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__266_37.min1.thm1.tptp2017-02-06 16:57 289  
[ ]convfun1__267_37.min1.thm1.tptp2017-02-06 16:57 289  
[ ]convfun1__268_37.min1.thm1.tptp2017-02-06 16:57 289  
[ ]convfun1__273_37.min1.thm1.tptp2017-02-06 16:57 292  
[ ]convfun1__274_37.min1.thm1.tptp2017-02-06 16:57 292  
[ ]convfun1__300_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__301_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__320_34.min1.thm1.tptp2017-02-06 16:57 280  
[ ]convfun1__323_34.min1.thm1.tptp2017-02-06 16:57 280  
[ ]convfun1__351_37.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__356_37.min1.thm1.tptp2017-02-06 16:57 289  
[ ]convfun1__357_37.min1.thm1.tptp2017-02-06 16:57 289  
[ ]convfun1__358_37.min1.thm1.tptp2017-02-06 16:57 289  
[ ]convfun1__378_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__379_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__397_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__398_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__414_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__415_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]convfun1__1091_37.min1.thm1.tptp2017-02-06 16:57 382  
[ ]convfun1__1092_35.min1.thm1.tptp2017-02-06 16:57 382  
[ ]convfun1__1115_39.min1.thm1.tptp2017-02-06 16:57 376  
[ ]convfun1__1127_39.min1.thm1.tptp2017-02-06 16:57 376  
[ ]cqc_sim1__489_53.min1.thm1.tptp2017-02-06 16:57 284  
[ ]cqc_the3__1101_61.min1.thm1.tptp2017-02-06 16:57 312  
[ ]cqc_the3__1134_75.min1.thm1.tptp2017-02-06 16:57 484  
[ ]descip_1__735_16.min1.thm1.tptp2017-02-06 16:57 290  
[ ]descip_1__2059_49.min1.thm1.tptp2017-02-06 16:57 267  
[ ]dickson__500_39.min1.thm1.tptp2017-02-06 16:57 272  
[ ]dickson__1599_35.min1.thm1.tptp2017-02-06 16:57 254  
[ ]dickson__1687_37.min1.thm1.tptp2017-02-06 16:57 246  
[ ]dickson__1875_46.min1.thm1.tptp2017-02-06 16:57 254  
[ ]dickson__2430_45.min1.thm1.tptp2017-02-06 16:57 246  
[ ]dickson__3949_46.min1.thm1.tptp2017-02-06 16:57 286  
[ ]dickson__3963_46.min1.thm1.tptp2017-02-06 16:57 298  
[ ]dickson__4067_42.min1.thm1.tptp2017-02-06 16:57 230  
[ ]dilworth__1113_38.min1.thm1.tptp2017-02-06 16:57 278  
[ ]dilworth__1802_43.min1.thm1.tptp2017-02-06 16:57 278  
[ ]dilworth__1860_43.min1.thm1.tptp2017-02-06 16:57 278  
[ ]dist_1__80_9.min1.thm1.tptp2017-02-06 16:57 299  
[ ]domain_1__48_35.min1.thm1.tptp2017-02-06 16:57 238  
[ ]domain_1__49_35.min1.thm1.tptp2017-02-06 16:57 238  
[ ]domain_1__90_37.min1.thm1.tptp2017-02-06 16:57 246  
[ ]domain_1__95_37.min1.thm1.tptp2017-02-06 16:57 248  
[ ]domain_1__96_37.min1.thm1.tptp2017-02-06 16:57 247  
[ ]domain_1__128_37.min1.thm1.tptp2017-02-06 16:57 246  
[ ]domain_1__133_37.min1.thm1.tptp2017-02-06 16:57 248  
[ ]domain_1__134_37.min1.thm1.tptp2017-02-06 16:57 247  
[ ]domain_1__217_37.min1.thm1.tptp2017-02-06 16:57 252  
[ ]domain_1__252_37.min1.thm1.tptp2017-02-06 16:57 252  
[ ]dtconstr__420_18.min1.thm1.tptp2017-02-06 16:57 440  
[ ]dtconstr__2357_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]ec_pf_1__314_42.min1.thm1.tptp2017-02-06 16:57 266  
[ ]ens_1__584_58.min1.thm1.tptp2017-02-06 16:57 382  
[ ]ens_1__596_58.min1.thm1.tptp2017-02-06 16:57 382  
[ ]ens_1__978_40.min1.thm1.tptp2017-02-06 16:57 224  
[ ]ens_1__1029_37.min1.thm1.tptp2017-02-06 16:57 242  
[ ]ens_1__1715_44.min1.thm1.tptp2017-02-06 16:57 276  
[ ]ens_1__1751_44.min1.thm1.tptp2017-02-06 16:57 276  
[ ]eqrel_1__1300_33.min1.thm1.tptp2017-02-06 16:57 238  
[ ]eqrel_1__1665_46.min1.thm1.tptp2017-02-06 16:57 278  
[ ]equation__1341_43.min1.thm1.tptp2017-02-06 16:57 278  
[ ]equation__1497_45.min1.thm1.tptp2017-02-06 16:57 260  
[ ]equation__1583_47.min1.thm1.tptp2017-02-06 16:57 270  
[ ]equation__1632_43.min1.thm1.tptp2017-02-06 16:57 274  
[ ]euclid_3__1141_49.min1.thm1.tptp2017-02-06 16:57 298  
[ ]euclid_3__1149_13.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]euclid_3__1186_49.min1.thm1.tptp2017-02-06 16:57 298  
[ ]euclid_3__1194_13.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]euclid_3__1231_49.min1.thm1.tptp2017-02-06 16:57 298  
[ ]euclid_3__1239_13.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]euclid_6__2148_47.min1.thm1.tptp2017-02-06 16:57 302  
[ ]euclid_7__4795_38.min1.thm1.tptp2017-02-06 16:57 310  
[ ]exchsort__2783_44.min1.thm1.tptp2017-02-06 16:57 244  
[ ]extens_1__258_45.min1.thm1.tptp2017-02-06 16:57 280  
[ ]extens_1__1056_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]extens_1__1078_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]facirc_1__1365_51.min1.thm1.tptp2017-02-06 16:57 645  
[ ]facirc_1__1442_54.min1.thm1.tptp2017-02-06 16:57 799  
[ ]facirc_1__1663_46.min1.thm1.tptp2017-02-06 16:57 644  
[ ]facirc_1__1731_46.min1.thm1.tptp2017-02-06 16:57 645  
[ ]facirc_1__1784_40.min1.thm1.tptp2017-02-06 16:57 400  
[ ]facirc_1__1971_46.min1.thm1.tptp2017-02-06 16:57 643  
[ ]facirc_1__1998_46.min1.thm1.tptp2017-02-06 16:57 643  
[ ]facirc_1__2029_46.min1.thm1.tptp2017-02-06 16:57 643  
[ ]facirc_1__2235_53.min1.thm1.tptp2017-02-06 16:57 447  
[ ]facirc_1__2247_53.min1.thm1.tptp2017-02-06 16:57 447  
[ ]facirc_1__2259_53.min1.thm1.tptp2017-02-06 16:57 447  
[ ]facirc_1__2293_53.min1.thm1.tptp2017-02-06 16:57 667  
[ ]facirc_1__2320_53.min1.thm1.tptp2017-02-06 16:57 447  
[ ]facirc_1__2332_53.min1.thm1.tptp2017-02-06 16:57 447  
[ ]facirc_1__2344_53.min1.thm1.tptp2017-02-06 16:57 447  
[ ]facirc_1__2362_53.min1.thm1.tptp2017-02-06 16:57 667  
[ ]facirc_1__2394_40.min1.thm1.tptp2017-02-06 16:57 380  
[ ]facirc_2__1629_53.min1.thm1.tptp2017-02-06 16:57 654  
[ ]facirc_2__1662_53.min1.thm1.tptp2017-02-06 16:57 654  
[ ]facirc_2__1689_40.min1.thm1.tptp2017-02-06 16:57 370  
[ ]facirc_2__1924_43.min1.thm1.tptp2017-02-06 16:57 242  
[ ]fcont_1__3033_42.min1.thm1.tptp2017-02-06 16:57 230  
[ ]fdiff_1__171_47.min1.thm1.tptp2017-02-06 16:57 556  
[ ]filter_0__338_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]filter_0__1761_39.min1.thm1.tptp2017-02-06 16:57 270  
[ ]filter_0__1773_46.min1.thm1.tptp2017-02-06 16:57 388  
[ ]filter_0__1787_53.min1.thm1.tptp2017-02-06 16:57 506  
[ ]filter_1__1396_43.min1.thm1.tptp2017-02-06 16:57 282  
[ ]filter_1__1415_43.min1.thm1.tptp2017-02-06 16:57 282  
[ ]fin_topo__166_37.min1.thm1.tptp2017-02-06 16:57 246  
[ ]fin_topo__171_37.min1.thm1.tptp2017-02-06 16:57 247  
[ ]fin_topo__410_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]fin_topo__441_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]finance1__515_42.min1.thm1.tptp2017-02-06 16:57 327  
[ ]finance1__1010_43.min1.thm1.tptp2017-02-06 16:57 276  
[ ]finseq_2__2376_28.min1.thm1.tptp2017-02-06 16:57 302  
[ ]finseq_2__2440_24.min1.thm1.tptp2017-02-06 16:57 296  
[ ]finsub_1__229_44.min1.thm1.tptp2017-02-06 16:57 400  
[ ]fintopo5__291_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]fintopo5__745_46.min1.thm1.tptp2017-02-06 16:57 300  
[ ]flang_1__1753_16.min1.thm1.tptp2017-02-06 16:57 458  
[ ]flang_1__1821_47.min1.thm1.tptp2017-02-06 16:57 272  
[ ]fomodel0__761_38.min1.thm1.tptp2017-02-06 16:57 261  
[ ]fomodel0__763_38.min1.thm1.tptp2017-02-06 16:57 262  
[ ]fomodel0__794_38.min1.thm1.tptp2017-02-06 16:57 261  
[ ]fomodel0__796_38.min1.thm1.tptp2017-02-06 16:57 262  
[ ]fomodel0__3062_59.min1.thm1.tptp2017-02-06 16:57 324  
[ ]fomodel0__3175_37.min1.thm1.tptp2017-02-06 16:57 286  
[ ]fomodel2__3645_37.min1.thm1.tptp2017-02-06 16:57 286  
[ ]fomodel3__798_34.min1.thm1.tptp2017-02-06 16:57 311  
[ ]fomodel3__960_34.min1.thm1.tptp2017-02-06 16:57 376  
[ ]fomodel3__1433_47.min1.thm1.tptp2017-02-06 16:57 286  
[ ]fomodel3__1989_34.min1.thm1.tptp2017-02-06 16:57 264  
[ ]fomodel3__2478_60.min1.thm1.tptp2017-02-06 16:57 282  
[ ]fomodel3__3466_36.min1.thm1.tptp2017-02-06 16:57 358  
[ ]fomodel4__1439_64.min1.thm1.tptp2017-02-06 16:57 342  
[ ]fraenkel__839_47.min1.thm1.tptp2017-02-06 16:57 298  
[ ]fraenkel__964_74.min1.thm1.tptp2017-02-06 16:57 623  
[ ]freealg__65_39.min1.thm1.tptp2017-02-06 16:57 250  
[ ]fscirc_1__153_46.min1.thm1.tptp2017-02-06 16:57 629  
[ ]fscirc_1__181_46.min1.thm1.tptp2017-02-06 16:57 629  
[ ]fscirc_1__211_46.min1.thm1.tptp2017-02-06 16:57 636  
[ ]fscirc_1__413_51.min1.thm1.tptp2017-02-06 16:57 437  
[ ]fscirc_1__425_51.min1.thm1.tptp2017-02-06 16:57 437  
[ ]fscirc_1__437_51.min1.thm1.tptp2017-02-06 16:57 437  
[ ]fscirc_1__473_53.min1.thm1.tptp2017-02-06 16:57 647  
[ ]fscirc_1__502_51.min1.thm1.tptp2017-02-06 16:57 437  
[ ]fscirc_1__514_51.min1.thm1.tptp2017-02-06 16:57 437  
[ ]fscirc_1__526_51.min1.thm1.tptp2017-02-06 16:57 437  
[ ]fscirc_1__544_53.min1.thm1.tptp2017-02-06 16:57 647  
[ ]fscirc_1__576_40.min1.thm1.tptp2017-02-06 16:57 368  
[ ]fscirc_2__1394_53.min1.thm1.tptp2017-02-06 16:57 647  
[ ]fscirc_2__1427_53.min1.thm1.tptp2017-02-06 16:57 647  
[ ]fscirc_2__1454_40.min1.thm1.tptp2017-02-06 16:57 368  
[ ]fscirc_2__1653_43.min1.thm1.tptp2017-02-06 16:57 242  
[ ]fsm_1__1558_42.min1.thm1.tptp2017-02-06 16:57 406  
[ ]fsm_1__1567_42.min1.thm1.tptp2017-02-06 16:57 406  
[ ]fsm_1__1622_33.min1.thm1.tptp2017-02-06 16:57 256  
[ ]fsm_1__1663_40.min1.thm1.tptp2017-02-06 16:57 276  
[ ]fsm_1__1709_38.min1.thm1.tptp2017-02-06 16:57 268  
[ ]fsm_1__1800_42.min1.thm1.tptp2017-02-06 16:57 260  
[ ]fsm_1__1825_37.min1.thm1.tptp2017-02-06 16:57 268  
[ ]fsm_1__1898_37.min1.thm1.tptp2017-02-06 16:57 268  
[ ]fsm_1__1899_37.min1.thm1.tptp2017-02-06 16:57 268  
[ ]fsm_1__1910_35.min1.thm1.tptp2017-02-06 16:57 260  
[ ]fsm_1__1911_35.min1.thm1.tptp2017-02-06 16:57 260  
[ ]fsm_1__2891_38.min1.thm1.tptp2017-02-06 16:57 370  
[ ]fsm_1__3904_43.min1.thm1.tptp2017-02-06 16:57 270  
[ ]fsm_1__4025_43.min1.thm1.tptp2017-02-06 16:57 270  
[ ]fsm_1__4388_41.min1.thm1.tptp2017-02-06 16:57 450  
[ ]fsm_1__4440_40.min1.thm1.tptp2017-02-06 16:57 468  
[ ]fsm_2__902_48.min1.thm1.tptp2017-02-06 16:57 392  
[ ]fsm_3__307_40.min1.thm1.tptp2017-02-06 16:57 302  
[ ]fsm_3__313_40.min1.thm1.tptp2017-02-06 16:57 304  
[ ]fsm_3__328_40.min1.thm1.tptp2017-02-06 16:57 302  
[ ]fsm_3__334_40.min1.thm1.tptp2017-02-06 16:57 304  
[ ]fsm_3__365_40.min1.thm1.tptp2017-02-06 16:57 349  
[ ]ftacell1__361_14.min1.thm1.tptp2017-02-06 16:57 1.5K 
[ ]ftacell1__1125_14.min1.thm1.tptp2017-02-06 16:57 1.5K 
[ ]ftacell1__1895_14.min1.thm1.tptp2017-02-06 16:57 1.5K 
[ ]ftacell1__2670_14.min1.thm1.tptp2017-02-06 16:57 1.5K 
[ ]funcop_1__1689_35.min1.thm1.tptp2017-02-06 16:57 266  
[ ]funct_2__1166_40.min1.thm1.tptp2017-02-06 16:57 370  
[ ]funct_2__1196_37.min1.thm1.tptp2017-02-06 16:57 238  
[ ]funct_2__1655_70.min1.thm1.tptp2017-02-06 16:57 360  
[ ]funct_2__1767_51.min1.thm1.tptp2017-02-06 16:57 386  
[ ]funct_2__2348_33.min1.thm1.tptp2017-02-06 16:57 244  
[ ]funct_7__526_45.min1.thm1.tptp2017-02-06 16:57 254  
[ ]funct_7__955_16.min1.thm1.tptp2017-02-06 16:57 240  
[ ]functor0__515_33.min1.thm1.tptp2017-02-06 16:57 245  
[ ]functor0__766_43.min1.thm1.tptp2017-02-06 16:57 252  
[ ]functor1__577_40.min1.thm1.tptp2017-02-06 16:57 400  
[ ]functor1__617_38.min1.thm1.tptp2017-02-06 16:57 388  
[ ]functor1__876_39.min1.thm1.tptp2017-02-06 16:57 400  
[ ]functor2__113_18.min1.thm1.tptp2017-02-06 16:57 674  
[ ]functor2__146_42.min1.thm1.tptp2017-02-06 16:57 288  
[ ]functor2__210_42.min1.thm1.tptp2017-02-06 16:57 288  
[ ]functor2__236_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]functor2__713_53.min1.thm1.tptp2017-02-06 16:57 436  
[ ]functor2__818_44.min1.thm1.tptp2017-02-06 16:57 310  
[ ]functor3__601_42.min1.thm1.tptp2017-02-06 16:57 294  
[ ]functor3__665_42.min1.thm1.tptp2017-02-06 16:57 294  
[ ]functor3__862_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]functor3__879_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]functor3__1233_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]fuzzy_4__134_45.min1.thm1.tptp2017-02-06 16:57 294  
[ ]fvaluat1__61_46.min1.thm1.tptp2017-02-06 16:57 238  
[ ]fvaluat1__113_36.min1.thm1.tptp2017-02-06 16:57 238  
[ ]fvaluat1__136_36.min1.thm1.tptp2017-02-06 16:57 238  
[ ]fvaluat1__158_36.min1.thm1.tptp2017-02-06 16:57 238  
[ ]fvaluat1__178_44.min1.thm1.tptp2017-02-06 16:57 318  
[ ]fvaluat1__283_44.min1.thm1.tptp2017-02-06 16:57 324  
[ ]fvaluat1__2356_50.min1.thm1.tptp2017-02-06 16:57 344  
[ ]gfacirc1__467_46.min1.thm1.tptp2017-02-06 16:57 645  
[ ]gfacirc1__979_53.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]gfacirc1__1009_53.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]gfacirc1__1042_40.min1.thm1.tptp2017-02-06 16:57 368  
[ ]gfacirc1__2035_53.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]gfacirc1__2066_53.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]gfacirc1__2099_40.min1.thm1.tptp2017-02-06 16:57 370  
[ ]gfacirc1__3114_53.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]gfacirc1__3145_53.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]gfacirc1__3178_40.min1.thm1.tptp2017-02-06 16:57 380  
[ ]gfacirc1__4175_53.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]gfacirc1__4206_53.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]gfacirc1__4239_40.min1.thm1.tptp2017-02-06 16:57 380  
[ ]glib_002__1172_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]glib_002__2838_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]gobrd11__173_46.min1.thm1.tptp2017-02-06 16:57 274  
[ ]gobrd14__1315_44.min1.thm1.tptp2017-02-06 16:57 282  
[ ]gobrd14__1361_44.min1.thm1.tptp2017-02-06 16:57 282  
[ ]gr_cy_1__1279_42.min1.thm1.tptp2017-02-06 16:57 280  
[ ]gr_cy_2__423_48.min1.thm1.tptp2017-02-06 16:57 312  
[ ]gr_cy_2__515_48.min1.thm1.tptp2017-02-06 16:57 312  
[ ]gr_cy_2__712_42.min1.thm1.tptp2017-02-06 16:57 280  
[ ]gr_cy_2__773_42.min1.thm1.tptp2017-02-06 16:57 280  
[ ]gr_cy_3__1316_37.min1.thm1.tptp2017-02-06 16:57 238  
[ ]graph_2__2307_33.min1.thm1.tptp2017-02-06 16:57 264  
[ ]graph_2__2308_33.min1.thm1.tptp2017-02-06 16:57 265  
[ ]graph_3__2423_47.min1.thm1.tptp2017-02-06 16:57 316  
[ ]graph_3__3435_56.min1.thm1.tptp2017-02-06 16:57 808  
[ ]graph_5__177_33.min1.thm1.tptp2017-02-06 16:57 232  
[ ]grnilp_1__1037_35.min1.thm1.tptp2017-02-06 16:57 286  
[ ]groeb_1__4093_44.min1.thm1.tptp2017-02-06 16:57 256  
[ ]groeb_1__4174_37.min1.thm1.tptp2017-02-06 16:57 404  
[ ]group_1__533_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]group_2__158_39.min1.thm1.tptp2017-02-06 16:57 258  
[ ]group_2__483_41.min1.thm1.tptp2017-02-06 16:57 272  
[ ]group_2__492_39.min1.thm1.tptp2017-02-06 16:57 264  
[ ]group_2__1207_42.min1.thm1.tptp2017-02-06 16:57 272  
[ ]group_2__2599_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]group_2__2613_39.min1.thm1.tptp2017-02-06 16:57 270  
[ ]group_2__2681_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]group_2__2715_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]group_4__2683_61.min1.thm1.tptp2017-02-06 16:57 410  
[ ]group_4__2727_61.min1.thm1.tptp2017-02-06 16:57 410  
[ ]group_6__490_57.min1.thm1.tptp2017-02-06 16:57 474  
[ ]group_6__1117_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]group_6__1380_35.min1.thm1.tptp2017-02-06 16:57 272  
[ ]group_6__1413_35.min1.thm1.tptp2017-02-06 16:57 272  
[ ]group_7__335_42.min1.thm1.tptp2017-02-06 16:57 254  
[ ]group_7__356_42.min1.thm1.tptp2017-02-06 16:57 254  
[ ]group_7__376_42.min1.thm1.tptp2017-02-06 16:57 254  
[ ]group_9__1312_43.min1.thm1.tptp2017-02-06 16:57 272  
[ ]group_9__1357_45.min1.thm1.tptp2017-02-06 16:57 274  
[ ]group_9__1360_55.min1.thm1.tptp2017-02-06 16:57 366  
[ ]group_9__2018_41.min1.thm1.tptp2017-02-06 16:57 262  
[ ]group_9__2820_42.min1.thm1.tptp2017-02-06 16:57 272  
[ ]group_9__3029_41.min1.thm1.tptp2017-02-06 16:57 272  
[ ]group_10__161_43.min1.thm1.tptp2017-02-06 16:57 284  
[ ]group_10__308_44.min1.thm1.tptp2017-02-06 16:57 296  
[ ]group_10__498_51.min1.thm1.tptp2017-02-06 16:57 345  
[ ]group_10__626_46.min1.thm1.tptp2017-02-06 16:57 330  
[ ]group_10__758_44.min1.thm1.tptp2017-02-06 16:57 334  
[ ]group_10__852_39.min1.thm1.tptp2017-02-06 16:57 276  
[ ]group_10__853_40.min1.thm1.tptp2017-02-06 16:57 302  
[ ]group_10__1010_44.min1.thm1.tptp2017-02-06 16:57 360  
[ ]group_10__1233_56.min1.thm1.tptp2017-02-06 16:57 334  
[ ]group_10__1756_44.min1.thm1.tptp2017-02-06 16:57 272  
[ ]group_10__2330_39.min1.thm1.tptp2017-02-06 16:57 268  
[ ]group_10__2331_40.min1.thm1.tptp2017-02-06 16:57 294  
[ ]group_10__2340_42.min1.thm1.tptp2017-02-06 16:57 302  
[ ]group_10__2390_40.min1.thm1.tptp2017-02-06 16:57 310  
[ ]group_10__2404_42.min1.thm1.tptp2017-02-06 16:57 302  
[ ]group_12__364_68.min1.thm1.tptp2017-02-06 16:57 672  
[ ]grsolv_1__617_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]grsolv_1__656_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]grsolv_1__707_36.min1.thm1.tptp2017-02-06 16:57 279  
[ ]grsolv_1__712_36.min1.thm1.tptp2017-02-06 16:57 280  
[ ]grsolv_1__726_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]grsolv_1__996_41.min1.thm1.tptp2017-02-06 16:57 302  
[ ]grsolv_1__1020_41.min1.thm1.tptp2017-02-06 16:57 302  
[ ]hahnban__1323_34.min1.thm1.tptp2017-02-06 16:57 272  
[ ]henmodel__1678_57.min1.thm1.tptp2017-02-06 16:57 294  
[ ]hermitan__2506_35.min1.thm1.tptp2017-02-06 16:57 488  
[ ]hermitan__2509_35.min1.thm1.tptp2017-02-06 16:57 583  
[ ]hermitan__2529_35.min1.thm1.tptp2017-02-06 16:57 488  
[ ]hermitan__2532_35.min1.thm1.tptp2017-02-06 16:57 583  
[ ]heyting2__970_55.min1.thm1.tptp2017-02-06 16:57 326  
[ ]hilbasis__525_42.min1.thm1.tptp2017-02-06 16:57 242  
[ ]hilbasis__968_36.min1.thm1.tptp2017-02-06 16:57 278  
[ ]hilbasis__988_36.min1.thm1.tptp2017-02-06 16:57 278  
[ ]hilbasis__1163_36.min1.thm1.tptp2017-02-06 16:57 278  
[ ]hilbasis__1169_36.min1.thm1.tptp2017-02-06 16:57 279  
[ ]hilbasis__1319_37.min1.thm1.tptp2017-02-06 16:57 286  
[ ]hilbasis__2272_50.min1.thm1.tptp2017-02-06 16:57 266  
[ ]hilbasis__2507_47.min1.thm1.tptp2017-02-06 16:57 386  
[ ]hilbasis__2513_46.min1.thm1.tptp2017-02-06 16:57 266  
[ ]hilbasis__2579_46.min1.thm1.tptp2017-02-06 16:57 370  
[ ]hilbasis__3236_36.min1.thm1.tptp2017-02-06 16:57 238  
[ ]hilbert2__1745_55.min1.thm1.tptp2017-02-06 16:57 396  
[ ]hilbert3__734_57.min1.thm1.tptp2017-02-06 16:57 396  
[ ]hilbert3__943_20.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]holder_1__233_49.min1.thm1.tptp2017-02-06 16:57 363  
[ ]hurwitz__1301_46.min1.thm1.tptp2017-02-06 16:57 254  
[ ]hurwitz__1567_46.min1.thm1.tptp2017-02-06 16:57 254  
[ ]hurwitz__2330_50.min1.thm1.tptp2017-02-06 16:57 278  
[ ]hurwitz__2861_46.min1.thm1.tptp2017-02-06 16:57 254  
[ ]ideal_1__809_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]ideal_1__843_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]ideal_1__888_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]ideal_1__2184_40.min1.thm1.tptp2017-02-06 16:57 272  
[ ]ideal_1__2201_40.min1.thm1.tptp2017-02-06 16:57 272  
[ ]ideal_1__2218_40.min1.thm1.tptp2017-02-06 16:57 272  
[ ]ideal_1__5336_35.min1.thm1.tptp2017-02-06 16:57 286  
[ ]ideal_1__5778_41.min1.thm1.tptp2017-02-06 16:57 242  
[ ]incsp_1__391_6.min1.thm1.tptp2017-02-06 16:57 580  
[ ]incsp_1__481_19.min1.thm1.tptp2017-02-06 16:57 467  
[ ]incsp_1__495_19.min1.thm1.tptp2017-02-06 16:57 463  
[ ]incsp_1__596_21.min1.thm1.tptp2017-02-06 16:57 517  
[ ]incsp_1__657_21.min1.thm1.tptp2017-02-06 16:57 521  
[ ]incsp_1__677_21.min1.thm1.tptp2017-02-06 16:57 509  
[ ]incsp_1__894_55.min1.thm1.tptp2017-02-06 16:57 387  
[ ]index_1__91_40.min1.thm1.tptp2017-02-06 16:57 266  
[ ]index_1__530_44.min1.thm1.tptp2017-02-06 16:57 262  
[ ]index_1__978_40.min1.thm1.tptp2017-02-06 16:57 272  
[ ]index_1__1001_42.min1.thm1.tptp2017-02-06 16:57 272  
[ ]index_1__1011_40.min1.thm1.tptp2017-02-06 16:57 272  
[ ]index_1__1363_42.min1.thm1.tptp2017-02-06 16:57 272  
[ ]index_1__1392_42.min1.thm1.tptp2017-02-06 16:57 272  
[ ]instalg1__612_41.min1.thm1.tptp2017-02-06 16:57 294  
[ ]instalg1__823_43.min1.thm1.tptp2017-02-06 16:57 272  
[ ]instalg1__867_45.min1.thm1.tptp2017-02-06 16:57 278  
[ ]instalg1__1162_46.min1.thm1.tptp2017-02-06 16:57 284  
[ ]instalg1__1174_41.min1.thm1.tptp2017-02-06 16:57 330  
[ ]instalg1__1314_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]instalg1__1323_45.min1.thm1.tptp2017-02-06 16:57 400  
[ ]instalg1__1413_37.min1.thm1.tptp2017-02-06 16:57 271  
[ ]instalg1__1487_40.min1.thm1.tptp2017-02-06 16:57 280  
[ ]instalg1__1597_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]instalg1__1662_45.min1.thm1.tptp2017-02-06 16:57 278  
[ ]int_7__2695_37.min1.thm1.tptp2017-02-06 16:57 230  
[ ]integr1c__117_54.min1.thm1.tptp2017-02-06 16:57 424  
[ ]isocat_1__255_40.min1.thm1.tptp2017-02-06 16:57 286  
[ ]isocat_1__460_35.min1.thm1.tptp2017-02-06 16:57 271  
[ ]isocat_1__461_35.min1.thm1.tptp2017-02-06 16:57 271  
[ ]isocat_1__540_35.min1.thm1.tptp2017-02-06 16:57 271  
[ ]isocat_1__545_36.min1.thm1.tptp2017-02-06 16:57 274  
[ ]isocat_1__546_36.min1.thm1.tptp2017-02-06 16:57 274  
[ ]isocat_2__307_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]isocat_2__804_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]isocat_2__1049_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]isocat_2__1673_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]isocat_2__2089_64.min1.thm1.tptp2017-02-06 16:57 406  
[ ]jgraph_2__5008_49.min1.thm1.tptp2017-02-06 16:57 298  
[ ]jgraph_2__5020_71.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]jgraph_2__5026_48.min1.thm1.tptp2017-02-06 16:57 298  
[ ]jgraph_3__300_48.min1.thm1.tptp2017-02-06 16:57 294  
[ ]jgraph_3__3089_47.min1.thm1.tptp2017-02-06 16:57 282  
[ ]jgraph_3__3106_46.min1.thm1.tptp2017-02-06 16:57 282  
[ ]jgraph_3__3619_47.min1.thm1.tptp2017-02-06 16:57 282  
[ ]jgraph_3__5087_49.min1.thm1.tptp2017-02-06 16:57 290  
[ ]jgraph_4__3507_49.min1.thm1.tptp2017-02-06 16:57 290  
[ ]jgraph_4__6490_49.min1.thm1.tptp2017-02-06 16:57 290  
[ ]jgraph_4__9411_49.min1.thm1.tptp2017-02-06 16:57 294  
[ ]jgraph_4__12325_49.min1.thm1.tptp2017-02-06 16:57 294  
[ ]jordan1h__259_38.min1.thm1.tptp2017-02-06 16:57 230  
[ ]jordan1h__269_38.min1.thm1.tptp2017-02-06 16:57 310  
[ ]jordan1h__279_40.min1.thm1.tptp2017-02-06 16:57 398  
[ ]jordan1h__289_40.min1.thm1.tptp2017-02-06 16:57 316  
[ ]jordan1h__311_42.min1.thm1.tptp2017-02-06 16:57 258  
[ ]jordan1h__558_42.min1.thm1.tptp2017-02-06 16:57 283  
[ ]jordan1h__626_42.min1.thm1.tptp2017-02-06 16:57 283  
[ ]jordan1k__68_14.min1.thm1.tptp2017-02-06 16:57 338  
[ ]jordan1k__84_35.min1.thm1.tptp2017-02-06 16:57 238  
[ ]jordan1k__717_47.min1.thm1.tptp2017-02-06 16:57 274  
[ ]jordan2b__997_31.min1.thm1.tptp2017-02-06 16:57 242  
[ ]jordan2c__787_40.min1.thm1.tptp2017-02-06 16:57 360  
[ ]jordan2c__4235_47.min1.thm1.tptp2017-02-06 16:57 302  
[ ]jordan18__83_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]jordan18__98_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]jordan18__113_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]jordan18__128_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]jordan18__156_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]jordan18__186_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]jordan18__216_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]jordan18__246_42.min1.thm1.tptp2017-02-06 16:57 282  
[ ]jordan18__723_40.min1.thm1.tptp2017-02-06 16:57 276  
[ ]jordan18__748_40.min1.thm1.tptp2017-02-06 16:57 276  
[ ]jordan21__56_14.min1.thm1.tptp2017-02-06 16:57 422  
[ ]kurato_2__115_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]lang1__114_38.min1.thm1.tptp2017-02-06 16:57 246  
[ ]lang1__410_41.min1.thm1.tptp2017-02-06 16:57 288  
[ ]lang1__431_50.min1.thm1.tptp2017-02-06 16:57 392  
[ ]lang1__442_50.min1.thm1.tptp2017-02-06 16:57 392  
[ ]lang1__827_35.min1.thm1.tptp2017-02-06 16:57 226  
[ ]lattice3__255_39.min1.thm1.tptp2017-02-06 16:57 294  
[ ]lattice5__118_36.min1.thm1.tptp2017-02-06 16:57 247  
[ ]lattice5__119_36.min1.thm1.tptp2017-02-06 16:57 248  
[ ]lattice5__226_49.min1.thm1.tptp2017-02-06 16:57 290  
[ ]lattice5__1245_44.min1.thm1.tptp2017-02-06 16:57 276  
[ ]lattice5__1246_44.min1.thm1.tptp2017-02-06 16:57 276  
[ ]lattice5__1257_46.min1.thm1.tptp2017-02-06 16:57 276  
[ ]lattice5__1272_60.min1.thm1.tptp2017-02-06 16:57 492  
[ ]lattice5__1434_39.min1.thm1.tptp2017-02-06 16:57 348  
[ ]lattice5__1441_39.min1.thm1.tptp2017-02-06 16:57 352  
[ ]lattice5__1551_49.min1.thm1.tptp2017-02-06 16:57 380  
[ ]lattice5__1577_46.min1.thm1.tptp2017-02-06 16:57 329  
[ ]lattice5__1583_46.min1.thm1.tptp2017-02-06 16:57 340  
[ ]lattice5__1589_46.min1.thm1.tptp2017-02-06 16:57 351  
[ ]lattice5__1595_46.min1.thm1.tptp2017-02-06 16:57 329  
[ ]lattice5__1601_46.min1.thm1.tptp2017-02-06 16:57 342  
[ ]lattice5__1607_46.min1.thm1.tptp2017-02-06 16:57 353  
[ ]lattice5__1705_46.min1.thm1.tptp2017-02-06 16:57 329  
[ ]lattice5__1711_46.min1.thm1.tptp2017-02-06 16:57 340  
[ ]lattice5__1717_46.min1.thm1.tptp2017-02-06 16:57 351  
[ ]lattice5__1723_46.min1.thm1.tptp2017-02-06 16:57 329  
[ ]lattice5__1741_46.min1.thm1.tptp2017-02-06 16:57 340  
[ ]lattice5__1759_46.min1.thm1.tptp2017-02-06 16:57 353  
[ ]lattice5__1796_44.min1.thm1.tptp2017-02-06 16:57 260  
[ ]lattice5__1824_50.min1.thm1.tptp2017-02-06 16:57 348  
[ ]lattice5__1831_42.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__1837_42.min1.thm1.tptp2017-02-06 16:57 313  
[ ]lattice5__1843_42.min1.thm1.tptp2017-02-06 16:57 324  
[ ]lattice5__1849_42.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice5__1869_42.min1.thm1.tptp2017-02-06 16:57 313  
[ ]lattice5__1889_42.min1.thm1.tptp2017-02-06 16:57 326  
[ ]lattice5__1932_52.min1.thm1.tptp2017-02-06 16:57 405  
[ ]lattice5__1948_52.min1.thm1.tptp2017-02-06 16:57 416  
[ ]lattice5__1968_52.min1.thm1.tptp2017-02-06 16:57 427  
[ ]lattice5__1992_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]lattice5__2124_48.min1.thm1.tptp2017-02-06 16:57 348  
[ ]lattice5__2174_52.min1.thm1.tptp2017-02-06 16:57 405  
[ ]lattice5__2184_52.min1.thm1.tptp2017-02-06 16:57 416  
[ ]lattice5__2198_52.min1.thm1.tptp2017-02-06 16:57 427  
[ ]lattice5__2409_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]lattice5__2495_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]lattice5__2632_58.min1.thm1.tptp2017-02-06 16:57 444  
[ ]lattice5__4459_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]lattice5__4460_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]lattice5__4829_47.min1.thm1.tptp2017-02-06 16:57 275  
[ ]lattice5__4842_47.min1.thm1.tptp2017-02-06 16:57 275  
[ ]lattice8__748_49.min1.thm1.tptp2017-02-06 16:57 380  
[ ]lattice8__764_46.min1.thm1.tptp2017-02-06 16:57 329  
[ ]lattice8__770_46.min1.thm1.tptp2017-02-06 16:57 340  
[ ]lattice8__776_46.min1.thm1.tptp2017-02-06 16:57 329  
[ ]lattice8__782_46.min1.thm1.tptp2017-02-06 16:57 340  
[ ]lattice8__865_46.min1.thm1.tptp2017-02-06 16:57 329  
[ ]lattice8__871_46.min1.thm1.tptp2017-02-06 16:57 340  
[ ]lattice8__877_46.min1.thm1.tptp2017-02-06 16:57 329  
[ ]lattice8__891_46.min1.thm1.tptp2017-02-06 16:57 340  
[ ]lattice8__927_44.min1.thm1.tptp2017-02-06 16:57 260  
[ ]lattice8__957_50.min1.thm1.tptp2017-02-06 16:57 348  
[ ]lattice8__964_42.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__970_42.min1.thm1.tptp2017-02-06 16:57 313  
[ ]lattice8__976_42.min1.thm1.tptp2017-02-06 16:57 302  
[ ]lattice8__991_42.min1.thm1.tptp2017-02-06 16:57 313  
[ ]lattice8__1033_52.min1.thm1.tptp2017-02-06 16:57 405  
[ ]lattice8__1043_52.min1.thm1.tptp2017-02-06 16:57 416  
[ ]lattice8__1069_44.min1.thm1.tptp2017-02-06 16:57 369  
[ ]lattice8__1099_44.min1.thm1.tptp2017-02-06 16:57 369  
[ ]lattice8__1149_44.min1.thm1.tptp2017-02-06 16:57 369  
[ ]lattice8__1167_44.min1.thm1.tptp2017-02-06 16:57 369  
[ ]lattice8__1262_44.min1.thm1.tptp2017-02-06 16:57 369  
[ ]lattice8__1290_44.min1.thm1.tptp2017-02-06 16:57 369  
[ ]lattice8__1331_48.min1.thm1.tptp2017-02-06 16:57 348  
[ ]lattice8__1365_52.min1.thm1.tptp2017-02-06 16:57 405  
[ ]lattice8__1381_52.min1.thm1.tptp2017-02-06 16:57 416  
[ ]lattice8__1401_58.min1.thm1.tptp2017-02-06 16:57 444  
[ ]lexbfs__3447_50.min1.thm1.tptp2017-02-06 16:57 274  
[ ]lfuzzy_0__112_48.min1.thm1.tptp2017-02-06 16:57 418  
[ ]lfuzzy_0__341_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]lfuzzy_0__357_39.min1.thm1.tptp2017-02-06 16:57 270  
[ ]lfuzzy_0__370_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]lfuzzy_0__386_39.min1.thm1.tptp2017-02-06 16:57 270  
[ ]lfuzzy_0__669_39.min1.thm1.tptp2017-02-06 16:57 310  
[ ]lfuzzy_0__1762_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]lfuzzy_0__1763_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]lmod_5__565_42.min1.thm1.tptp2017-02-06 16:57 274  
[ ]lmod_5__603_42.min1.thm1.tptp2017-02-06 16:57 274  
[ ]lmod_7__695_18.min1.thm1.tptp2017-02-06 16:57 248  
[ ]lopban_3__1336_44.min1.thm1.tptp2017-02-06 16:57 358  
[ ]lopban_5__328_40.min1.thm1.tptp2017-02-06 16:57 288  
[ ]lopban_6__319_34.min1.thm1.tptp2017-02-06 16:57 272  
[ ]lopban_6__608_38.min1.thm1.tptp2017-02-06 16:57 278  
[ ]lopban_6__614_38.min1.thm1.tptp2017-02-06 16:57 280  
[ ]lopban_6__752_37.min1.thm1.tptp2017-02-06 16:57 288  
[ ]lopban_6__785_39.min1.thm1.tptp2017-02-06 16:57 304  
[ ]lopban_6__1090_40.min1.thm1.tptp2017-02-06 16:57 286  
[ ]lopban_6__1096_36.min1.thm1.tptp2017-02-06 16:57 286  
[ ]lopclset__458_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]lpspace1__109_29.min1.thm1.tptp2017-02-06 16:57 254  
[ ]ltlaxio1__281_43.min1.thm1.tptp2017-02-06 16:57 282  
[ ]ltlaxio1__347_43.min1.thm1.tptp2017-02-06 16:57 282  
[ ]ltlaxio1__412_46.min1.thm1.tptp2017-02-06 16:57 260  
[ ]ltlaxio1__612_40.min1.thm1.tptp2017-02-06 16:57 266  
[ ]ltlaxio1__615_45.min1.thm1.tptp2017-02-06 16:57 268  
[ ]ltlaxio1__1494_46.min1.thm1.tptp2017-02-06 16:57 260  
[ ]ltlaxio1__1630_46.min1.thm1.tptp2017-02-06 16:57 244  
[ ]mathmorp__291_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]matrix13__592_41.min1.thm1.tptp2017-02-06 16:57 358  
[ ]matrix13__5414_39.min1.thm1.tptp2017-02-06 16:57 344  
[ ]matrlin2__179_46.min1.thm1.tptp2017-02-06 16:57 396  
[ ]matrlin2__192_46.min1.thm1.tptp2017-02-06 16:57 396  
[ ]matrlin2__331_38.min1.thm1.tptp2017-02-06 16:57 388  
[ ]matrlin2__1814_41.min1.thm1.tptp2017-02-06 16:57 294  
[ ]matrlin2__2210_38.min1.thm1.tptp2017-02-06 16:57 278  
[ ]matrlin2__2286_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]matrlin2__2354_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]matrtop2__445_35.min1.thm1.tptp2017-02-06 16:57 302  
[ ]mcart_1__1090_50.min1.thm1.tptp2017-02-06 16:57 324  
[ ]mcart_1__1279_53.min1.thm1.tptp2017-02-06 16:57 354  
[ ]measure5__266_33.min1.thm1.tptp2017-02-06 16:57 274  
[ ]measure5__276_33.min1.thm1.tptp2017-02-06 16:57 274  
[ ]measure7__253_41.min1.thm1.tptp2017-02-06 16:57 270  
[ ]membered__180_15.min1.thm1.tptp2017-02-06 16:57 291  
[ ]membered__192_15.min1.thm1.tptp2017-02-06 16:57 288  
[ ]membered__204_15.min1.thm1.tptp2017-02-06 16:57 282  
[ ]mesfun7c__647_18.min1.thm1.tptp2017-02-06 16:57 449  
[ ]mesfunc1__927_25.min1.thm1.tptp2017-02-06 16:57 234  
[ ]mesfunc1__946_25.min1.thm1.tptp2017-02-06 16:57 234  
[ ]mesfunc2__1271_41.min1.thm1.tptp2017-02-06 16:57 284  
[ ]mesfunc5__4249_48.min1.thm1.tptp2017-02-06 16:57 306  
[ ]mesfunc5__4313_50.min1.thm1.tptp2017-02-06 16:57 312  
[ ]mesfunc5__4486_42.min1.thm1.tptp2017-02-06 16:57 282  
[ ]mesfunc5__4487_48.min1.thm1.tptp2017-02-06 16:57 310  
[ ]mesfunc9__726_34.min1.thm1.tptp2017-02-06 16:57 242  
[ ]mesfunc9__741_39.min1.thm1.tptp2017-02-06 16:57 306  
[ ]mesfunc9__792_36.min1.thm1.tptp2017-02-06 16:57 254  
[ ]mesfunc9__3035_44.min1.thm1.tptp2017-02-06 16:57 268  
[ ]mesfunc9__3079_44.min1.thm1.tptp2017-02-06 16:57 268  
[ ]metrizts__479_18.min1.thm1.tptp2017-02-06 16:57 558  
[ ]metrizts__891_47.min1.thm1.tptp2017-02-06 16:57 290  
[ ]metrizts__1456_43.min1.thm1.tptp2017-02-06 16:57 258  
[ ]metrizts__1635_43.min1.thm1.tptp2017-02-06 16:57 258  
[ ]metrizts__1911_42.min1.thm1.tptp2017-02-06 16:57 302  
[ ]mfold_2__926_49.min1.thm1.tptp2017-02-06 16:57 312  
[ ]mfold_2__995_50.min1.thm1.tptp2017-02-06 16:57 328  
[ ]mmlquery__1160_37.min1.thm1.tptp2017-02-06 16:57 356  
[ ]mod_2__610_43.min1.thm1.tptp2017-02-06 16:57 351  
[ ]mod_2__617_43.min1.thm1.tptp2017-02-06 16:57 346  
[ ]mod_2__624_43.min1.thm1.tptp2017-02-06 16:57 346  
[ ]mod_2__721_14.min1.thm1.tptp2017-02-06 16:57 348  
[ ]mod_2__724_14.min1.thm1.tptp2017-02-06 16:57 353  
[ ]mod_2__1112_49.min1.thm1.tptp2017-02-06 16:57 354  
[ ]mod_2__1119_49.min1.thm1.tptp2017-02-06 16:57 354  
[ ]mod_3__392_42.min1.thm1.tptp2017-02-06 16:57 268  
[ ]mod_3__405_42.min1.thm1.tptp2017-02-06 16:57 268  
[ ]mod_4__167_43.min1.thm1.tptp2017-02-06 16:57 268  
[ ]modal_1__2780_47.min1.thm1.tptp2017-02-06 16:57 246  
[ ]modelc_1__61_13.min1.thm1.tptp2017-02-06 16:57 388  
[ ]modelc_1__1778_37.min1.thm1.tptp2017-02-06 16:57 242  
[ ]modelc_1__2237_39.min1.thm1.tptp2017-02-06 16:57 266  
[ ]modelc_1__3847_37.min1.thm1.tptp2017-02-06 16:57 258  
[ ]modelc_1__4186_43.min1.thm1.tptp2017-02-06 16:57 270  
[ ]modelc_1__4224_41.min1.thm1.tptp2017-02-06 16:57 262  
[ ]modelc_1__4258_41.min1.thm1.tptp2017-02-06 16:57 262  
[ ]modelc_1__4638_38.min1.thm1.tptp2017-02-06 16:57 300  
[ ]modelc_1__5050_38.min1.thm1.tptp2017-02-06 16:57 300  
[ ]modelc_2__3443_39.min1.thm1.tptp2017-02-06 16:57 246  
[ ]modelc_2__3495_18.min1.thm1.tptp2017-02-06 16:57 888  
[ ]modelc_2__3566_18.min1.thm1.tptp2017-02-06 16:57 874  
[ ]modelc_2__3627_18.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]modelc_2__3716_18.min1.thm1.tptp2017-02-06 16:57 1.0K 
[ ]modelc_3__4244_14.min1.thm1.tptp2017-02-06 16:57 306  
[ ]modelc_3__4252_14.min1.thm1.tptp2017-02-06 16:57 278  
[ ]monoid_0__204_39.min1.thm1.tptp2017-02-06 16:57 293  
[ ]monoid_0__1349_57.min1.thm1.tptp2017-02-06 16:57 378  
[ ]monoid_1__1268_41.min1.thm1.tptp2017-02-06 16:57 252  
[ ]morph_01__75_43.min1.thm1.tptp2017-02-06 16:57 272  
[ ]morph_01__116_43.min1.thm1.tptp2017-02-06 16:57 272  
[ ]morph_01__137_43.min1.thm1.tptp2017-02-06 16:57 272  
[ ]morph_01__371_38.min1.thm1.tptp2017-02-06 16:57 395  
[ ]morph_01__413_45.min1.thm1.tptp2017-02-06 16:57 395  
[ ]morph_01__414_43.min1.thm1.tptp2017-02-06 16:57 395  
[ ]msafree2__331_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msafree2__970_50.min1.thm1.tptp2017-02-06 16:57 360  
[ ]msafree3__272_38.min1.thm1.tptp2017-02-06 16:57 280  
[ ]msafree3__652_47.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msafree3__676_47.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msafree3__728_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msafree3__1052_43.min1.thm1.tptp2017-02-06 16:57 270  
[ ]msafree3__1213_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msafree3__1368_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msafree3__1403_48.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msafree__292_43.min1.thm1.tptp2017-02-06 16:57 256  
[ ]msafree__1020_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__1036_44.min1.thm1.tptp2017-02-06 16:57 280  
[ ]msafree__1526_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__1548_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__1570_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__1733_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__1961_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__1977_42.min1.thm1.tptp2017-02-06 16:57 264  
[ ]msafree__2115_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__2138_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__2157_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msafree__2447_44.min1.thm1.tptp2017-02-06 16:57 272  
[ ]msafree__2549_44.min1.thm1.tptp2017-02-06 16:57 272  
[ ]msafree__2625_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]msalimit__500_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msalimit__947_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msalimit__988_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msinst_1__482_61.min1.thm1.tptp2017-02-06 16:57 366  
[ ]msinst_1__527_65.min1.thm1.tptp2017-02-06 16:57 390  
[ ]msinst_1__646_57.min1.thm1.tptp2017-02-06 16:57 330  
[ ]msinst_1__689_61.min1.thm1.tptp2017-02-06 16:57 354  
[ ]msinst_1__1115_63.min1.thm1.tptp2017-02-06 16:57 370  
[ ]msinst_1__1139_63.min1.thm1.tptp2017-02-06 16:57 370  
[ ]msinst_1__1218_44.min1.thm1.tptp2017-02-06 16:57 650  
[ ]msinst_1__1328_52.min1.thm1.tptp2017-02-06 16:57 500  
[ ]msscyc_1__1041_39.min1.thm1.tptp2017-02-06 16:57 277  
[ ]msscyc_1__1107_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msscyc_1__1214_42.min1.thm1.tptp2017-02-06 16:57 271  
[ ]msscyc_1__1227_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msscyc_1__1290_33.min1.thm1.tptp2017-02-06 16:57 271  
[ ]msscyc_1__1417_45.min1.thm1.tptp2017-02-06 16:57 266  
[ ]msscyc_2__476_38.min1.thm1.tptp2017-02-06 16:57 268  
[ ]msscyc_2__477_36.min1.thm1.tptp2017-02-06 16:57 268  
[ ]msscyc_2__521_40.min1.thm1.tptp2017-02-06 16:57 274  
[ ]msscyc_2__522_38.min1.thm1.tptp2017-02-06 16:57 273  
[ ]msscyc_2__702_41.min1.thm1.tptp2017-02-06 16:57 292  
[ ]msscyc_2__1100_36.min1.thm1.tptp2017-02-06 16:57 265  
[ ]msscyc_2__1111_33.min1.thm1.tptp2017-02-06 16:57 408  
[ ]mssublat__113_37.min1.thm1.tptp2017-02-06 16:57 279  
[ ]mssublat__338_52.min1.thm1.tptp2017-02-06 16:57 304  
[ ]mssublat__943_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]mssublat__980_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]mssublat__1070_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_1__299_37.min1.thm1.tptp2017-02-06 16:57 280  
[ ]msualg_1__408_42.min1.thm1.tptp2017-02-06 16:57 276  
[ ]msualg_1__571_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__275_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msualg_2__293_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]msualg_2__359_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_2__495_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_2__518_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_2__538_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_2__595_45.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__622_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_2__647_60.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_2__707_45.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__765_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__807_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__861_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__899_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__993_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__1304_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_2__1326_42.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_2__1340_42.min1.thm1.tptp2017-02-06 16:57 270  
[ ]msualg_2__1366_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__1397_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_2__1631_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_2__1681_48.min1.thm1.tptp2017-02-06 16:57 302  
[ ]msualg_3__1367_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_3__1485_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_4__296_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__299_59.min1.thm1.tptp2017-02-06 16:57 394  
[ ]msualg_4__318_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__460_44.min1.thm1.tptp2017-02-06 16:57 440  
[ ]msualg_4__496_48.min1.thm1.tptp2017-02-06 16:57 440  
[ ]msualg_4__585_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__607_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__627_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__645_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__667_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__687_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__918_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__940_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__960_47.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__1062_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__1081_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__1158_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_4__1255_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__1268_41.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__1335_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__1372_40.min1.thm1.tptp2017-02-06 16:57 382  
[ ]msualg_4__1409_40.min1.thm1.tptp2017-02-06 16:57 382  
[ ]msualg_4__1448_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__1468_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_4__1553_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_4__1572_41.min1.thm1.tptp2017-02-06 16:57 380  
[ ]msualg_4__1576_41.min1.thm1.tptp2017-02-06 16:57 379  
[ ]msualg_4__1604_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_5__117_44.min1.thm1.tptp2017-02-06 16:57 271  
[ ]msualg_5__147_39.min1.thm1.tptp2017-02-06 16:57 366  
[ ]msualg_5__170_48.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_5__437_44.min1.thm1.tptp2017-02-06 16:57 262  
[ ]msualg_5__450_42.min1.thm1.tptp2017-02-06 16:57 262  
[ ]msualg_5__466_44.min1.thm1.tptp2017-02-06 16:57 262  
[ ]msualg_5__507_44.min1.thm1.tptp2017-02-06 16:57 262  
[ ]msualg_5__530_42.min1.thm1.tptp2017-02-06 16:57 252  
[ ]msualg_5__550_42.min1.thm1.tptp2017-02-06 16:57 252  
[ ]msualg_5__764_46.min1.thm1.tptp2017-02-06 16:57 276  
[ ]msualg_5__777_44.min1.thm1.tptp2017-02-06 16:57 276  
[ ]msualg_5__2172_46.min1.thm1.tptp2017-02-06 16:57 302  
[ ]msualg_5__2208_46.min1.thm1.tptp2017-02-06 16:57 302  
[ ]msualg_5__2244_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_5__2279_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_6__1243_42.min1.thm1.tptp2017-02-06 16:57 337  
[ ]msualg_6__1456_48.min1.thm1.tptp2017-02-06 16:57 358  
[ ]msualg_6__1769_40.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_6__1821_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_6__1883_46.min1.thm1.tptp2017-02-06 16:57 284  
[ ]msualg_6__1904_44.min1.thm1.tptp2017-02-06 16:57 276  
[ ]msualg_6__2246_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_6__2259_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_6__2272_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_6__2545_42.min1.thm1.tptp2017-02-06 16:57 270  
[ ]msualg_6__2559_42.min1.thm1.tptp2017-02-06 16:57 270  
[ ]msualg_6__2735_39.min1.thm1.tptp2017-02-06 16:57 244  
[ ]msualg_6__2834_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_6__2853_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]msualg_6__2896_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_7__118_46.min1.thm1.tptp2017-02-06 16:57 270  
[ ]msualg_7__149_46.min1.thm1.tptp2017-02-06 16:57 270  
[ ]msualg_7__179_44.min1.thm1.tptp2017-02-06 16:57 254  
[ ]msualg_7__209_44.min1.thm1.tptp2017-02-06 16:57 254  
[ ]msualg_7__240_44.min1.thm1.tptp2017-02-06 16:57 254  
[ ]msualg_7__338_40.min1.thm1.tptp2017-02-06 16:57 246  
[ ]msualg_8__956_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]msualg_9__373_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_9__554_58.min1.thm1.tptp2017-02-06 16:57 544  
[ ]msualg_9__1111_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_9__1132_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_9__1166_50.min1.thm1.tptp2017-02-06 16:57 358  
[ ]msualg_9__1243_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_9__1253_52.min1.thm1.tptp2017-02-06 16:57 371  
[ ]msualg_9__1278_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_9__1345_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msualg_9__1390_44.min1.thm1.tptp2017-02-06 16:57 278  
[ ]msuhom_1__477_26.min1.thm1.tptp2017-02-06 16:57 285  
[ ]msuhom_1__598_46.min1.thm1.tptp2017-02-06 16:57 298  
[ ]multop_1__125_38.min1.thm1.tptp2017-02-06 16:57 254  
[ ]multop_1__126_38.min1.thm1.tptp2017-02-06 16:57 254  
[ ]multop_1__127_38.min1.thm1.tptp2017-02-06 16:57 254  
[ ]multop_1__295_38.min1.thm1.tptp2017-02-06 16:57 258  
[ ]multop_1__296_38.min1.thm1.tptp2017-02-06 16:57 258  
[ ]multop_1__297_38.min1.thm1.tptp2017-02-06 16:57 258  
[ ]multop_1__298_38.min1.thm1.tptp2017-02-06 16:57 259  
[ ]mycielsk__1435_47.min1.thm1.tptp2017-02-06 16:57 302  
[ ]nagata_1__830_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]nagata_1__1810_37.min1.thm1.tptp2017-02-06 16:57 400  
[ ]nagata_1__2253_39.min1.thm1.tptp2017-02-06 16:57 268  
[ ]nagata_1__2274_41.min1.thm1.tptp2017-02-06 16:57 268  
[ ]nagata_2__450_41.min1.thm1.tptp2017-02-06 16:57 416  
[ ]nagata_2__526_37.min1.thm1.tptp2017-02-06 16:57 338  
[ ]nagata_2__1261_35.min1.thm1.tptp2017-02-06 16:57 400  
[ ]nagata_2__1506_35.min1.thm1.tptp2017-02-06 16:57 400  
[ ]nagata_2__1848_39.min1.thm1.tptp2017-02-06 16:57 424  
[ ]nagata_2__1869_39.min1.thm1.tptp2017-02-06 16:57 424  
[ ]nagata_2__1961_39.min1.thm1.tptp2017-02-06 16:57 430  
[ ]nat_3__1088_43.min1.thm1.tptp2017-02-06 16:57 250  
[ ]ndiff_4__1696_43.min1.thm1.tptp2017-02-06 16:57 238  
[ ]ndiff_4__2461_42.min1.thm1.tptp2017-02-06 16:57 238  
[ ]neckla_2__796_60.min1.thm1.tptp2017-02-06 16:57 323  
[ ]neckla_3__3512_39.min1.thm1.tptp2017-02-06 16:57 440  
[ ]neckla_3__3749_35.min1.thm1.tptp2017-02-06 16:57 388  
[ ]neckla_3__3818_39.min1.thm1.tptp2017-02-06 16:57 400  
[ ]neckla_3__4069_39.min1.thm1.tptp2017-02-06 16:57 402  
[ ]neckla_3__4874_38.min1.thm1.tptp2017-02-06 16:57 588  
[ ]neckla_3__4891_38.min1.thm1.tptp2017-02-06 16:57 588  
[ ]neckla_3__5808_49.min1.thm1.tptp2017-02-06 16:57 636  
[ ]neckla_3__5822_51.min1.thm1.tptp2017-02-06 16:57 488  
[ ]neckla_3__6179_49.min1.thm1.tptp2017-02-06 16:57 636  
[ ]neckla_3__6185_51.min1.thm1.tptp2017-02-06 16:57 488  
[ ]neckla_3__6526_37.min1.thm1.tptp2017-02-06 16:57 298  
[ ]openlatt__364_41.min1.thm1.tptp2017-02-06 16:57 294  
[ ]orders_1__1848_43.min1.thm1.tptp2017-02-06 16:57 260  
[ ]orders_1__2289_44.min1.thm1.tptp2017-02-06 16:57 258  
[ ]orders_1__2304_44.min1.thm1.tptp2017-02-06 16:57 258  
[ ]orders_1__2413_44.min1.thm1.tptp2017-02-06 16:57 258  
[ ]orders_1__2428_44.min1.thm1.tptp2017-02-06 16:57 258  
[ ]orders_2__555_39.min1.thm1.tptp2017-02-06 16:57 270  
[ ]orders_2__579_39.min1.thm1.tptp2017-02-06 16:57 270  
[ ]ordinal1__1461_43.min1.thm1.tptp2017-02-06 16:57 258  
[ ]ordinal5__883_45.min1.thm1.tptp2017-02-06 16:57 287  
[ ]ordinal5__1057_40.min1.thm1.tptp2017-02-06 16:57 268  
[ ]ordinal5__1097_40.min1.thm1.tptp2017-02-06 16:57 268  
[ ]ordinal5__1227_38.min1.thm1.tptp2017-02-06 16:57 252  
[ ]ordinal6__1285_40.min1.thm1.tptp2017-02-06 16:57 268  
[ ]ordinal6__1325_40.min1.thm1.tptp2017-02-06 16:57 268  
[ ]ordinal6__1485_38.min1.thm1.tptp2017-02-06 16:57 252  
[ ]osafree__743_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__758_41.min1.thm1.tptp2017-02-06 16:57 280  
[ ]osafree__1159_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__1181_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__1203_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__1400_37.min1.thm1.tptp2017-02-06 16:57 265  
[ ]osafree__1808_41.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__1990_41.min1.thm1.tptp2017-02-06 16:57 284  
[ ]osafree__2182_52.min1.thm1.tptp2017-02-06 16:57 391  
[ ]osafree__2387_52.min1.thm1.tptp2017-02-06 16:57 391  
[ ]osafree__2596_52.min1.thm1.tptp2017-02-06 16:57 390  
[ ]osafree__2831_41.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__2892_41.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__3185_57.min1.thm1.tptp2017-02-06 16:57 412  
[ ]osafree__3186_58.min1.thm1.tptp2017-02-06 16:57 416  
[ ]osafree__3206_55.min1.thm1.tptp2017-02-06 16:57 406  
[ ]osafree__3237_56.min1.thm1.tptp2017-02-06 16:57 408  
[ ]osafree__3286_43.min1.thm1.tptp2017-02-06 16:57 280  
[ ]osafree__3659_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__3677_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__3692_39.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osafree__3846_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__4087_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__4102_39.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osafree__4520_41.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osafree__4641_41.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osafree__4776_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__4799_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__4820_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osafree__5451_52.min1.thm1.tptp2017-02-06 16:57 391  
[ ]osafree__5543_37.min1.thm1.tptp2017-02-06 16:57 266  
[ ]osalg_1__1165_44.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_1__1201_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_1__1320_43.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osalg_2__356_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_2__371_43.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osalg_2__388_41.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osalg_2__434_48.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_2__472_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_2__485_43.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osalg_2__502_41.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osalg_2__530_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osalg_2__576_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osalg_2__957_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_2__991_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_2__1022_43.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osalg_2__1048_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osalg_2__1080_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osalg_2__1229_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_2__1281_47.min1.thm1.tptp2017-02-06 16:57 280  
[ ]osalg_2__1323_46.min1.thm1.tptp2017-02-06 16:57 280  
[ ]osalg_2__1342_43.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osalg_4__788_38.min1.thm1.tptp2017-02-06 16:57 264  
[ ]osalg_4__918_54.min1.thm1.tptp2017-02-06 16:57 418  
[ ]osalg_4__940_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]osalg_4__1230_45.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1249_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1444_44.min1.thm1.tptp2017-02-06 16:57 428  
[ ]osalg_4__1480_48.min1.thm1.tptp2017-02-06 16:57 428  
[ ]osalg_4__1571_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1593_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1613_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1631_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1653_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1673_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1895_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1917_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1937_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__1988_62.min1.thm1.tptp2017-02-06 16:57 372  
[ ]osalg_4__2027_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__2046_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__2128_41.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osalg_4__2141_46.min1.thm1.tptp2017-02-06 16:57 368  
[ ]osalg_4__2187_67.min1.thm1.tptp2017-02-06 16:57 566  
[ ]osalg_4__2242_40.min1.thm1.tptp2017-02-06 16:57 372  
[ ]osalg_4__2278_45.min1.thm1.tptp2017-02-06 16:57 372  
[ ]osalg_4__2321_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__2341_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__2426_44.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osalg_4__2440_41.min1.thm1.tptp2017-02-06 16:57 368  
[ ]osalg_4__2447_41.min1.thm1.tptp2017-02-06 16:57 370  
[ ]osalg_4__2479_44.min1.thm1.tptp2017-02-06 16:57 361  
[ ]osalg_4__2510_44.min1.thm1.tptp2017-02-06 16:57 272  
[ ]osalg_4__2881_40.min1.thm1.tptp2017-02-06 16:57 372  
[ ]osalg_4__2918_45.min1.thm1.tptp2017-02-06 16:57 372  
[ ]osalg_4__2961_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__2981_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]osalg_4__3083_44.min1.thm1.tptp2017-02-06 16:57 361  
[ ]partfun1__391_14.min1.thm1.tptp2017-02-06 16:57 468  
[ ]partit1__1416_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]pboole__2330_59.min1.thm1.tptp2017-02-06 16:57 305  
[ ]pboole__2492_50.min1.thm1.tptp2017-02-06 16:57 378  
[ ]pcomps_2__239_36.min1.thm1.tptp2017-02-06 16:57 272  
[ ]pcs_0__43_46.min1.thm1.tptp2017-02-06 16:57 357  
[ ]pcs_0__167_39.min1.thm1.tptp2017-02-06 16:57 244  
[ ]pcs_0__573_39.min1.thm1.tptp2017-02-06 16:57 250  
[ ]pcs_0__1089_39.min1.thm1.tptp2017-02-06 16:57 250  
[ ]pdiff_1__112_43.min1.thm1.tptp2017-02-06 16:57 234  
[ ]pdiff_1__133_45.min1.thm1.tptp2017-02-06 16:57 234  
[ ]pdiff_1__282_44.min1.thm1.tptp2017-02-06 16:57 254  
[ ]pdiff_1__1080_41.min1.thm1.tptp2017-02-06 16:57 238  
[ ]pdiff_2__59_45.min1.thm1.tptp2017-02-06 16:57 234  
[ ]pdiff_2__84_45.min1.thm1.tptp2017-02-06 16:57 234  
[ ]pdiff_4__60_47.min1.thm1.tptp2017-02-06 16:57 234  
[ ]pdiff_4__84_47.min1.thm1.tptp2017-02-06 16:57 234  
[ ]pdiff_4__108_47.min1.thm1.tptp2017-02-06 16:57 234  
[ ]pencil_1__426_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]pencil_1__859_34.min1.thm1.tptp2017-02-06 16:57 294  
[ ]pencil_1__966_37.min1.thm1.tptp2017-02-06 16:57 252  
[ ]pencil_1__988_39.min1.thm1.tptp2017-02-06 16:57 252  
[ ]pencil_1__1038_39.min1.thm1.tptp2017-02-06 16:57 410  
[ ]pencil_1__1061_41.min1.thm1.tptp2017-02-06 16:57 268  
[ ]pencil_1__1658_35.min1.thm1.tptp2017-02-06 16:57 256  
[ ]pencil_1__1884_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]pencil_1__2467_45.min1.thm1.tptp2017-02-06 16:57 276  
[ ]pencil_1__2495_43.min1.thm1.tptp2017-02-06 16:57 268  
[ ]pencil_1__2884_44.min1.thm1.tptp2017-02-06 16:57 276  
[ ]pencil_2__546_39.min1.thm1.tptp2017-02-06 16:57 246  
[ ]pencil_3__96_33.min1.thm1.tptp2017-02-06 16:57 272  
[ ]pencil_3__345_40.min1.thm1.tptp2017-02-06 16:57 246  
[ ]pencil_3__518_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]pencil_3__1104_44.min1.thm1.tptp2017-02-06 16:57 440  
[ ]pencil_3__2301_41.min1.thm1.tptp2017-02-06 16:57 268  
[ ]pencil_3__2593_43.min1.thm1.tptp2017-02-06 16:57 276  
[ ]pencil_3__2619_46.min1.thm1.tptp2017-02-06 16:57 652  
[ ]pencil_3__2632_43.min1.thm1.tptp2017-02-06 16:57 276  
[ ]pencil_3__3142_39.min1.thm1.tptp2017-02-06 16:57 427  
[ ]pencil_3__3241_46.min1.thm1.tptp2017-02-06 16:57 284  
[ ]pencil_3__3274_44.min1.thm1.tptp2017-02-06 16:57 276  
[ ]pencil_3__3445_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]pencil_4__679_36.min1.thm1.tptp2017-02-06 16:57 294  
[ ]pencil_4__1045_36.min1.thm1.tptp2017-02-06 16:57 294  
[ ]polyalg1__63_39.min1.thm1.tptp2017-02-06 16:57 286  
[ ]polyalg1__87_39.min1.thm1.tptp2017-02-06 16:57 286  
[ ]polyalg1__194_44.min1.thm1.tptp2017-02-06 16:57 368  
[ ]polyalg1__215_45.min1.thm1.tptp2017-02-06 16:57 370  
[ ]polyalg1__232_46.min1.thm1.tptp2017-02-06 16:57 368  
[ ]polyalg1__889_39.min1.thm1.tptp2017-02-06 16:57 287  
[ ]polyalg1__1043_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]polyform__1619_14.min1.thm1.tptp2017-02-06 16:57 554  
[ ]polyform__2442_48.min1.thm1.tptp2017-02-06 16:57 300  
[ ]polynom3__2978_44.min1.thm1.tptp2017-02-06 16:57 378  
[ ]polynom3__2999_45.min1.thm1.tptp2017-02-06 16:57 380  
[ ]polynom5__2587_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]polynom6__489_43.min1.thm1.tptp2017-02-06 16:57 268  
[ ]polynom7__608_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]polynom8__1767_46.min1.thm1.tptp2017-02-06 16:57 258  
[ ]polynom8__2002_46.min1.thm1.tptp2017-02-06 16:57 258  
[ ]poset_1__822_39.min1.thm1.tptp2017-02-06 16:57 272  
[ ]poset_1__1086_39.min1.thm1.tptp2017-02-06 16:57 288  
[ ]poset_1__1110_46.min1.thm1.tptp2017-02-06 16:57 296  
[ ]poset_1__1446_51.min1.thm1.tptp2017-02-06 16:57 342  
[ ]poset_1__1472_55.min1.thm1.tptp2017-02-06 16:57 342  
[ ]pralg_1__437_45.min1.thm1.tptp2017-02-06 16:57 286  
[ ]pralg_1__794_45.min1.thm1.tptp2017-02-06 16:57 290  
[ ]pralg_1__1919_44.min1.thm1.tptp2017-02-06 16:57 262  
[ ]pralg_1__2009_44.min1.thm1.tptp2017-02-06 16:57 262  
[ ]pralg_2__744_45.min1.thm1.tptp2017-02-06 16:57 270  
[ ]pralg_2__801_47.min1.thm1.tptp2017-02-06 16:57 288  
[ ]pralg_2__817_44.min1.thm1.tptp2017-02-06 16:57 280  
[ ]pralg_2__877_45.min1.thm1.tptp2017-02-06 16:57 270  
[ ]pralg_2__1210_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]pralg_2__1247_48.min1.thm1.tptp2017-02-06 16:57 296  
[ ]pralg_2__1588_61.min1.thm1.tptp2017-02-06 16:57 296  
[ ]pralg_3__435_42.min1.thm1.tptp2017-02-06 16:57 246  
[ ]pralg_3__831_44.min1.thm1.tptp2017-02-06 16:57 290  
[ ]pralg_3__869_46.min1.thm1.tptp2017-02-06 16:57 288  
[ ]pralg_3__1174_47.min1.thm1.tptp2017-02-06 16:57 272  
[ ]pralg_3__1243_49.min1.thm1.tptp2017-02-06 16:57 278  
[ ]pralg_3__1295_49.min1.thm1.tptp2017-02-06 16:57 278  
[ ]pralg_3__1376_48.min1.thm1.tptp2017-02-06 16:57 280  
[ ]pralg_3__1569_47.min1.thm1.tptp2017-02-06 16:57 270  
[ ]pralg_3__1596_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]pralg_3__1905_43.min1.thm1.tptp2017-02-06 16:57 272  
[ ]prgcor_2__85_36.min1.thm1.tptp2017-02-06 16:57 238  
[ ]prob_1__564_34.min1.thm1.tptp2017-02-06 16:57 531  
[ ]projred1__980_37.min1.thm1.tptp2017-02-06 16:57 292  
[ ]prvect_1__442_38.min1.thm1.tptp2017-02-06 16:57 294  
[ ]prvect_3__537_39.min1.thm1.tptp2017-02-06 16:57 357  
[ ]prvect_3__1426_34.min1.thm1.tptp2017-02-06 16:57 358  
[ ]prvect_3__1427_37.min1.thm1.tptp2017-02-06 16:57 358  
[ ]prvect_3__2368_35.min1.thm1.tptp2017-02-06 16:57 338  
[ ]prvect_3__2556_35.min1.thm1.tptp2017-02-06 16:57 338  
[ ]pscomp_1__656_35.min1.thm1.tptp2017-02-06 16:57 282  
[ ]pua2mss1__1260_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]pua2mss1__1414_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]pua2mss1__2359_43.min1.thm1.tptp2017-02-06 16:57 338  
[ ]pua2mss1__2397_44.min1.thm1.tptp2017-02-06 16:57 338  
[ ]pua2mss1__2636_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]pua2mss1__2725_45.min1.thm1.tptp2017-02-06 16:57 278  
[ ]pythtrip__561_50.min1.thm1.tptp2017-02-06 16:57 382  
[ ]qc_lang1__1622_53.min1.thm1.tptp2017-02-06 16:57 284  
[ ]qc_lang1__2072_20.min1.thm1.tptp2017-02-06 16:57 370  
[ ]qc_lang1__2240_14.min1.thm1.tptp2017-02-06 16:57 277  
[ ]qc_lang3__918_35.min1.thm1.tptp2017-02-06 16:57 270  
[ ]qc_lang3__941_39.min1.thm1.tptp2017-02-06 16:57 234  
[ ]qmax_1__684_42.min1.thm1.tptp2017-02-06 16:57 255  
[ ]quofield__2736_38.min1.thm1.tptp2017-02-06 16:57 302  
[ ]quofield__2743_38.min1.thm1.tptp2017-02-06 16:57 303  
[ ]quofield__2834_39.min1.thm1.tptp2017-02-06 16:57 294  
[ ]quofield__2875_39.min1.thm1.tptp2017-02-06 16:57 294  
[ ]quofield__3318_66.min1.thm1.tptp2017-02-06 16:57 326  
[ ]ramsey_1__115_67.min1.thm1.tptp2017-02-06 16:57 318  
[ ]ramsey_1__411_50.min1.thm1.tptp2017-02-06 16:57 288  
[ ]ramsey_1__426_49.min1.thm1.tptp2017-02-06 16:57 294  
[ ]ramsey_1__842_48.min1.thm1.tptp2017-02-06 16:57 262  
[ ]rat_1__209_40.min1.thm1.tptp2017-02-06 16:57 226  
[ ]rat_1__221_39.min1.thm1.tptp2017-02-06 16:57 234  
[ ]rcomp_3__891_27.min1.thm1.tptp2017-02-06 16:57 230  
[ ]rcomp_3__2993_51.min1.thm1.tptp2017-02-06 16:57 426  
[ ]rearran1__771_39.min1.thm1.tptp2017-02-06 16:57 244  
[ ]rearran1__1763_39.min1.thm1.tptp2017-02-06 16:57 244  
[ ]recdef_1__993_31.min1.thm1.tptp2017-02-06 16:57 246  
[ ]recdef_1__1082_31.min1.thm1.tptp2017-02-06 16:57 246  
[ ]recdef_1__1733_31.min1.thm1.tptp2017-02-06 16:57 250  
[ ]rewrite2__850_44.min1.thm1.tptp2017-02-06 16:57 400  
[ ]rewrite2__922_46.min1.thm1.tptp2017-02-06 16:57 412  
[ ]rewrite2__935_46.min1.thm1.tptp2017-02-06 16:57 412  
[ ]rewrite2__957_44.min1.thm1.tptp2017-02-06 16:57 400  
[ ]rewrite2__975_44.min1.thm1.tptp2017-02-06 16:57 400  
[ ]rewrite2__999_44.min1.thm1.tptp2017-02-06 16:57 400  
[ ]rewrite2__1053_44.min1.thm1.tptp2017-02-06 16:57 400  
[ ]rewrite2__1086_44.min1.thm1.tptp2017-02-06 16:57 400  
[ ]rewrite3__678_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]rewrite3__679_38.min1.thm1.tptp2017-02-06 16:57 294  
[ ]rewrite3__684_43.min1.thm1.tptp2017-02-06 16:57 295  
[ ]rewrite3__685_38.min1.thm1.tptp2017-02-06 16:57 295  
[ ]rfunct_1__1703_41.min1.thm1.tptp2017-02-06 16:57 580  
[ ]rinfsup2__741_37.min1.thm1.tptp2017-02-06 16:57 260  
[ ]ring_1__204_37.min1.thm1.tptp2017-02-06 16:57 266  
[ ]ring_1__321_35.min1.thm1.tptp2017-02-06 16:57 258  
[ ]ring_1__338_35.min1.thm1.tptp2017-02-06 16:57 266  
[ ]ring_1__344_39.min1.thm1.tptp2017-02-06 16:57 274  
[ ]ring_1__396_35.min1.thm1.tptp2017-02-06 16:57 266  
[ ]ring_1__579_14.min1.thm1.tptp2017-02-06 16:57 514  
[ ]rlaffin3__1421_38.min1.thm1.tptp2017-02-06 16:57 223  
[ ]rlsub_1__707_34.min1.thm1.tptp2017-02-06 16:57 238  
[ ]rlsub_2__208_40.min1.thm1.tptp2017-02-06 16:57 258  
[ ]rlsub_2__677_37.min1.thm1.tptp2017-02-06 16:57 272  
[ ]rlsub_2__685_37.min1.thm1.tptp2017-02-06 16:57 274  
[ ]rlsub_2__1807_61.min1.thm1.tptp2017-02-06 16:57 410  
[ ]rlsub_2__1848_61.min1.thm1.tptp2017-02-06 16:57 410  
[ ]rltopsp1__1346_50.min1.thm1.tptp2017-02-06 16:57 400  
[ ]rltopsp1__1884_50.min1.thm1.tptp2017-02-06 16:57 400  
[ ]rlvect_2__1050_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]rlvect_3__1239_42.min1.thm1.tptp2017-02-06 16:57 286  
[ ]rlvect_3__1270_42.min1.thm1.tptp2017-02-06 16:57 286  
[ ]rlvect_5__284_40.min1.thm1.tptp2017-02-06 16:57 272  
[ ]rlvect_5__299_50.min1.thm1.tptp2017-02-06 16:57 1.1K 
[ ]rlvect_5__589_36.min1.thm1.tptp2017-02-06 16:57 278  
[ ]rlvect_x__178_36.min1.thm1.tptp2017-02-06 16:57 366  
[ ]rlvect_x__195_36.min1.thm1.tptp2017-02-06 16:57 366  
[ ]rlvect_x__211_38.min1.thm1.tptp2017-02-06 16:57 336  
[ ]rlvect_x__307_36.min1.thm1.tptp2017-02-06 16:57 344  
[ ]rlvect_x__362_39.min1.thm1.tptp2017-02-06 16:57 358  
[ ]rlvect_x__400_39.min1.thm1.tptp2017-02-06 16:57 359  
[ ]rlvect_x__547_39.min1.thm1.tptp2017-02-06 16:57 344  
[ ]rlvect_x__662_39.min1.thm1.tptp2017-02-06 16:57 386  
[ ]rlvect_x__835_39.min1.thm1.tptp2017-02-06 16:57 386  
[ ]rmod_3__200_40.min1.thm1.tptp2017-02-06 16:57 252  
[ ]rmod_3__792_37.min1.thm1.tptp2017-02-06 16:57 266  
[ ]rmod_3__800_37.min1.thm1.tptp2017-02-06 16:57 268  
[ ]rmod_3__1141_40.min1.thm1.tptp2017-02-06 16:57 266  
[ ]rmod_4__405_43.min1.thm1.tptp2017-02-06 16:57 282  
[ ]rmod_4__2500_42.min1.thm1.tptp2017-02-06 16:57 274  
[ ]rmod_4__2532_42.min1.thm1.tptp2017-02-06 16:57 274  
[ ]robbins3__418_52.min1.thm1.tptp2017-02-06 16:57 424  
[ ]robbins3__428_60.min1.thm1.tptp2017-02-06 16:57 554  
[ ]robbins3__438_39.min1.thm1.tptp2017-02-06 16:57 294  
[ ]robbins4__1657_44.min1.thm1.tptp2017-02-06 16:57 352  
[ ]rsspace__109_14.min1.thm1.tptp2017-02-06 16:57 228  
[ ]rsspace__506_29.min1.thm1.tptp2017-02-06 16:57 254  
[ ]rusub_1__750_34.min1.thm1.tptp2017-02-06 16:57 238  
[ ]rusub_2__213_40.min1.thm1.tptp2017-02-06 16:57 258  
[ ]rusub_2__777_37.min1.thm1.tptp2017-02-06 16:57 272  
[ ]rusub_2__785_37.min1.thm1.tptp2017-02-06 16:57 274  
[ ]rusub_2__1936_61.min1.thm1.tptp2017-02-06 16:57 410  
[ ]rusub_2__1983_61.min1.thm1.tptp2017-02-06 16:57 410  
[ ]rusub_3__369_42.min1.thm1.tptp2017-02-06 16:57 280  
[ ]rusub_3__400_42.min1.thm1.tptp2017-02-06 16:57 280  
[ ]rusub_3__1339_36.min1.thm1.tptp2017-02-06 16:57 272  
[ ]scheme1__994_44.min1.thm1.tptp2017-02-06 16:57 252  
[ ]scheme1__1687_38.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__1688_38.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__1726_37.min1.thm1.tptp2017-02-06 16:57 255  
[ ]scheme1__1727_37.min1.thm1.tptp2017-02-06 16:57 255  
[ ]scheme1__1801_38.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__1802_38.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__1852_37.min1.thm1.tptp2017-02-06 16:57 255  
[ ]scheme1__1853_37.min1.thm1.tptp2017-02-06 16:57 255  
[ ]scheme1__2160_44.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__2196_44.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__2230_37.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__2231_37.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__2271_37.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scheme1__2272_37.min1.thm1.tptp2017-02-06 16:57 254  
[ ]scmfsa_1__537_54.min1.thm1.tptp2017-02-06 16:57 226  
[ ]scmfsa_i__508_53.min1.thm1.tptp2017-02-06 16:57 237  
[ ]scmfsa_i__610_51.min1.thm1.tptp2017-02-06 16:57 286  
[ ]scmpds_9__1484_37.min1.thm1.tptp2017-02-06 16:57 234  
[ ]scmring3__566_37.min1.thm1.tptp2017-02-06 16:57 234  
[ ]scmring3__601_37.min1.thm1.tptp2017-02-06 16:57 234  
[ ]scmyciel__2762_47.min1.thm1.tptp2017-02-06 16:57 304  
[ ]setfam_1__1454_16.min1.thm1.tptp2017-02-06 16:57 293  
[ ]setfam_1__1608_32.min1.thm1.tptp2017-02-06 16:57 311  
[ ]setlim_1__168_37.min1.thm1.tptp2017-02-06 16:57 238  
[ ]setlim_1__200_40.min1.thm1.tptp2017-02-06 16:57 246  
[ ]setlim_1__487_41.min1.thm1.tptp2017-02-06 16:57 258  
[ ]setlim_1__528_41.min1.thm1.tptp2017-02-06 16:57 258  
[ ]sf_mastr__270_16.min1.thm1.tptp2017-02-06 16:57 798  
[ ]sf_mastr__967_16.min1.thm1.tptp2017-02-06 16:57 556  
[ ]sgraph1__295_14.min1.thm1.tptp2017-02-06 16:57 482  
[ ]sgraph1__490_18.min1.thm1.tptp2017-02-06 16:57 352  
[ ]stacks_1__197_40.min1.thm1.tptp2017-02-06 16:57 256  
[ ]stacks_1__942_43.min1.thm1.tptp2017-02-06 16:57 308  
[ ]stacks_1__1256_36.min1.thm1.tptp2017-02-06 16:57 294  
[ ]stacks_1__2093_16.min1.thm1.tptp2017-02-06 16:57 516  
[ ]stacks_1__2126_33.min1.thm1.tptp2017-02-06 16:57 406  
[ ]stirl2_1__608_20.min1.thm1.tptp2017-02-06 16:57 381  
[ ]struct_0__285_20.min1.thm1.tptp2017-02-06 16:57 491  
[ ]sublemma__803_49.min1.thm1.tptp2017-02-06 16:57 270  
[ ]sublemma__804_46.min1.thm1.tptp2017-02-06 16:57 270  
[ ]subset__34_57.min1.thm1.tptp2017-02-06 16:57 363  
[ ]substut1__531_45.min1.thm1.tptp2017-02-06 16:57 294  
[ ]substut1__593_45.min1.thm1.tptp2017-02-06 16:57 294  
[ ]substut1__1185_43.min1.thm1.tptp2017-02-06 16:57 270  
[ ]substut1__1186_45.min1.thm1.tptp2017-02-06 16:57 271  
[ ]substut1__2287_57.min1.thm1.tptp2017-02-06 16:57 286  
[ ]supinf_2__365_39.min1.thm1.tptp2017-02-06 16:57 268  
[ ]supinf_2__385_37.min1.thm1.tptp2017-02-06 16:57 252  
[ ]supinf_2__456_39.min1.thm1.tptp2017-02-06 16:57 268  
[ ]supinf_2__482_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]supinf_2__499_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]symsp_1__63_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]t_0topsp__106_58.min1.thm1.tptp2017-02-06 16:57 540  
[ ]taxonom1__234_20.min1.thm1.tptp2017-02-06 16:57 357  
[ ]taxonom1__500_42.min1.thm1.tptp2017-02-06 16:57 252  
[ ]taxonom1__516_48.min1.thm1.tptp2017-02-06 16:57 348  
[ ]taxonom1__553_48.min1.thm1.tptp2017-02-06 16:57 348  
[ ]taxonom1__607_48.min1.thm1.tptp2017-02-06 16:57 348  
[ ]taxonom1__1036_48.min1.thm1.tptp2017-02-06 16:57 400  
[ ]taxonom1__1050_48.min1.thm1.tptp2017-02-06 16:57 400  
[ ]taxonom1__1189_44.min1.thm1.tptp2017-02-06 16:57 400  
[ ]taxonom2__917_44.min1.thm1.tptp2017-02-06 16:57 270  
[ ]taxonom2__1068_44.min1.thm1.tptp2017-02-06 16:57 270  
[ ]taylor_1__998_47.min1.thm1.tptp2017-02-06 16:57 381  
[ ]taylor_1__1049_47.min1.thm1.tptp2017-02-06 16:57 382  
[ ]taylor_2__478_41.min1.thm1.tptp2017-02-06 16:57 242  
[ ]termord__131_48.min1.thm1.tptp2017-02-06 16:57 288  
[ ]tex_1__920_40.min1.thm1.tptp2017-02-06 16:57 318  
[ ]tex_1__1799_40.min1.thm1.tptp2017-02-06 16:57 318  
[ ]tex_2__1409_31.min1.thm1.tptp2017-02-06 16:57 252  
[ ]tex_4__638_31.min1.thm1.tptp2017-02-06 16:57 252  
[ ]tex_4__2670_33.min1.thm1.tptp2017-02-06 16:57 274  
[ ]tietze__1181_44.min1.thm1.tptp2017-02-06 16:57 258  
[ ]tietze__1230_41.min1.thm1.tptp2017-02-06 16:57 456  
[ ]topalg_5__122_41.min1.thm1.tptp2017-02-06 16:57 410  
[ ]topalg_5__194_41.min1.thm1.tptp2017-02-06 16:57 410  
[ ]topalg_5__236_35.min1.thm1.tptp2017-02-06 16:57 326  
[ ]topalg_6__202_33.min1.thm1.tptp2017-02-06 16:57 288  
[ ]topdim_1__1639_36.min1.thm1.tptp2017-02-06 16:57 286  
[ ]topdim_1__1788_41.min1.thm1.tptp2017-02-06 16:57 242  
[ ]topgen_2__789_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]topgen_2__817_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]topgen_3__887_47.min1.thm1.tptp2017-02-06 16:57 258  
[ ]topgen_3__1352_44.min1.thm1.tptp2017-02-06 16:57 242  
[ ]topgen_5__632_31.min1.thm1.tptp2017-02-06 16:57 234  
[ ]topgen_5__709_31.min1.thm1.tptp2017-02-06 16:57 234  
[ ]topgen_5__1781_49.min1.thm1.tptp2017-02-06 16:57 270  
[ ]topgrp_1__169_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]topgrp_1__226_39.min1.thm1.tptp2017-02-06 16:57 270  
[ ]topgrp_1__309_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]topgrp_1__335_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]topgrp_1__367_42.min1.thm1.tptp2017-02-06 16:57 286  
[ ]topgrp_1__396_42.min1.thm1.tptp2017-02-06 16:57 286  
[ ]topgrp_1__457_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]topgrp_1__485_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]topmetr3__551_37.min1.thm1.tptp2017-02-06 16:57 306  
[ ]topmetr3__878_37.min1.thm1.tptp2017-02-06 16:57 306  
[ ]topmetr__722_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]topreal6__1192_42.min1.thm1.tptp2017-02-06 16:57 282  
[ ]topreal6__1250_42.min1.thm1.tptp2017-02-06 16:57 282  
[ ]topreal6__1982_43.min1.thm1.tptp2017-02-06 16:57 316  
[ ]topreal6__2267_40.min1.thm1.tptp2017-02-06 16:57 274  
[ ]topreal6__2319_40.min1.thm1.tptp2017-02-06 16:57 274  
[ ]topreal7__894_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]topreal7__895_36.min1.thm1.tptp2017-02-06 16:57 288  
[ ]topreal7__1150_40.min1.thm1.tptp2017-02-06 16:57 314  
[ ]topreal7__1151_40.min1.thm1.tptp2017-02-06 16:57 314  
[ ]toprealc__577_44.min1.thm1.tptp2017-02-06 16:57 310  
[ ]toprealc__700_39.min1.thm1.tptp2017-02-06 16:57 276  
[ ]toprealc__708_37.min1.thm1.tptp2017-02-06 16:57 268  
[ ]toprealc__738_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]toprealc__751_35.min1.thm1.tptp2017-02-06 16:57 260  
[ ]toprealc__776_40.min1.thm1.tptp2017-02-06 16:57 286  
[ ]toprealc__1034_42.min1.thm1.tptp2017-02-06 16:57 310  
[ ]toprealc__1208_39.min1.thm1.tptp2017-02-06 16:57 302  
[ ]toprealc__2446_39.min1.thm1.tptp2017-02-06 16:57 504  
[ ]toprealc__2467_42.min1.thm1.tptp2017-02-06 16:57 300  
[ ]toprealc__2497_44.min1.thm1.tptp2017-02-06 16:57 378  
[ ]trees_4__1226_44.min1.thm1.tptp2017-02-06 16:57 290  
[ ]trees_4__1227_40.min1.thm1.tptp2017-02-06 16:57 290  
[ ]trees_9__1211_35.min1.thm1.tptp2017-02-06 16:57 238  
[ ]trees_9__1968_22.min1.thm1.tptp2017-02-06 16:57 438  
[ ]trees_9__2737_45.min1.thm1.tptp2017-02-06 16:57 254  
[ ]triang_1__661_45.min1.thm1.tptp2017-02-06 16:57 258  
[ ]triang_1__900_45.min1.thm1.tptp2017-02-06 16:57 258  
[ ]triang_1__923_43.min1.thm1.tptp2017-02-06 16:57 258  
[ ]triang_1__931_43.min1.thm1.tptp2017-02-06 16:57 336  
[ ]triang_1__950_55.min1.thm1.tptp2017-02-06 16:57 418  
[ ]tsp_2__311_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]tsp_2__445_31.min1.thm1.tptp2017-02-06 16:57 246  
[ ]tsp_2__534_41.min1.thm1.tptp2017-02-06 16:57 276  
[ ]tsp_2__1567_41.min1.thm1.tptp2017-02-06 16:57 276  
[ ]tsp_2__1751_37.min1.thm1.tptp2017-02-06 16:57 284  
[ ]turing_1__465_38.min1.thm1.tptp2017-02-06 16:57 248  
[ ]turing_1__963_42.min1.thm1.tptp2017-02-06 16:57 296  
[ ]turing_1__987_42.min1.thm1.tptp2017-02-06 16:57 292  
[ ]turing_1__1465_43.min1.thm1.tptp2017-02-06 16:57 296  
[ ]turing_1__1487_43.min1.thm1.tptp2017-02-06 16:57 292  
[ ]turing_1__1884_43.min1.thm1.tptp2017-02-06 16:57 296  
[ ]turing_1__1899_43.min1.thm1.tptp2017-02-06 16:57 292  
[ ]turing_1__2274_44.min1.thm1.tptp2017-02-06 16:57 296  
[ ]uniform1__493_42.min1.thm1.tptp2017-02-06 16:57 280  
[ ]uproots__2848_44.min1.thm1.tptp2017-02-06 16:57 288  
[ ]uproots__2869_42.min1.thm1.tptp2017-02-06 16:57 272  
[ ]uproots__2989_41.min1.thm1.tptp2017-02-06 16:57 272  
[ ]urysohn2__110_35.min1.thm1.tptp2017-02-06 16:57 246  
[ ]urysohn2__191_39.min1.thm1.tptp2017-02-06 16:57 285  
[ ]urysohn2__247_46.min1.thm1.tptp2017-02-06 16:57 334  
[ ]urysohn2__304_39.min1.thm1.tptp2017-02-06 16:57 285  
[ ]urysohn2__376_39.min1.thm1.tptp2017-02-06 16:57 285  
[ ]urysohn2__429_46.min1.thm1.tptp2017-02-06 16:57 334  
[ ]urysohn2__489_39.min1.thm1.tptp2017-02-06 16:57 285  
[ ]urysohn2__639_39.min1.thm1.tptp2017-02-06 16:57 293  
[ ]urysohn2__640_37.min1.thm1.tptp2017-02-06 16:57 293  
[ ]urysohn2__744_11.min1.thm1.tptp2017-02-06 16:57 304  
[ ]urysohn2__749_14.min1.thm1.tptp2017-02-06 16:57 304  
[ ]urysohn2__821_11.min1.thm1.tptp2017-02-06 16:57 296  
[ ]urysohn2__913_11.min1.thm1.tptp2017-02-06 16:57 304  
[ ]urysohn2__918_14.min1.thm1.tptp2017-02-06 16:57 304  
[ ]urysohn2__990_11.min1.thm1.tptp2017-02-06 16:57 296  
[ ]urysohn2__1070_11.min1.thm1.tptp2017-02-06 16:57 301  
[ ]urysohn2__1128_35.min1.thm1.tptp2017-02-06 16:57 286  
[ ]urysohn2__1133_14.min1.thm1.tptp2017-02-06 16:57 309  
[ ]urysohn2__1230_11.min1.thm1.tptp2017-02-06 16:57 301  
[ ]urysohn2__1291_42.min1.thm1.tptp2017-02-06 16:57 328  
[ ]urysohn2__1891_41.min1.thm1.tptp2017-02-06 16:57 326  
[ ]urysohn2__1962_41.min1.thm1.tptp2017-02-06 16:57 326  
[ ]urysohn3__1078_37.min1.thm1.tptp2017-02-06 16:57 294  
[ ]vectmetr__94_42.min1.thm1.tptp2017-02-06 16:57 390  
[ ]vectmetr__148_50.min1.thm1.tptp2017-02-06 16:57 414  
[ ]vectmetr__188_50.min1.thm1.tptp2017-02-06 16:57 416  
[ ]vectmetr__487_44.min1.thm1.tptp2017-02-06 16:57 432  
[ ]vectmetr__1596_53.min1.thm1.tptp2017-02-06 16:57 320  
[ ]vectmetr__1615_59.min1.thm1.tptp2017-02-06 16:57 476  
[ ]vectmetr__1619_42.min1.thm1.tptp2017-02-06 16:57 294  
[ ]vectmetr__1643_67.min1.thm1.tptp2017-02-06 16:57 632  
[ ]vectmetr__1647_42.min1.thm1.tptp2017-02-06 16:57 294  
[ ]vectmetr__1656_42.min1.thm1.tptp2017-02-06 16:57 298  
[ ]vectsp10__1739_42.min1.thm1.tptp2017-02-06 16:57 302  
[ ]vectsp11__1054_48.min1.thm1.tptp2017-02-06 16:57 490  
[ ]vectsp11__2103_40.min1.thm1.tptp2017-02-06 16:57 278  
[ ]vectsp_1__645_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]vectsp_5__205_40.min1.thm1.tptp2017-02-06 16:57 264  
[ ]vectsp_5__816_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]vectsp_5__824_37.min1.thm1.tptp2017-02-06 16:57 280  
[ ]vectsp_5__1601_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]vectsp_6__157_43.min1.thm1.tptp2017-02-06 16:57 288  
[ ]vectsp_7__586_42.min1.thm1.tptp2017-02-06 16:57 286  
[ ]vectsp_7__627_42.min1.thm1.tptp2017-02-06 16:57 286  
[ ]vectsp_9__235_40.min1.thm1.tptp2017-02-06 16:57 272  
[ ]vectsp_9__251_50.min1.thm1.tptp2017-02-06 16:57 1.2K 
[ ]vectsp_9__540_36.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel10__81_44.min1.thm1.tptp2017-02-06 16:57 288  
[ ]waybel10__88_42.min1.thm1.tptp2017-02-06 16:57 280  
[ ]waybel10__551_46.min1.thm1.tptp2017-02-06 16:57 310  
[ ]waybel10__560_44.min1.thm1.tptp2017-02-06 16:57 302  
[ ]waybel10__1201_37.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel10__1218_60.min1.thm1.tptp2017-02-06 16:57 434  
[ ]waybel10__1230_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel10__1321_58.min1.thm1.tptp2017-02-06 16:57 388  
[ ]waybel10__1511_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel11__2808_44.min1.thm1.tptp2017-02-06 16:57 264  
[ ]waybel11__2929_48.min1.thm1.tptp2017-02-06 16:57 310  
[ ]waybel14__330_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel14__347_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel15__530_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel17__127_46.min1.thm1.tptp2017-02-06 16:57 254  
[ ]waybel17__504_46.min1.thm1.tptp2017-02-06 16:57 310  
[ ]waybel17__512_44.min1.thm1.tptp2017-02-06 16:57 302  
[ ]waybel17__1283_35.min1.thm1.tptp2017-02-06 16:57 280  
[ ]waybel18__580_39.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel18__627_42.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel18__1866_44.min1.thm1.tptp2017-02-06 16:57 269  
[ ]waybel18__2334_46.min1.thm1.tptp2017-02-06 16:57 268  
[ ]waybel18__2464_46.min1.thm1.tptp2017-02-06 16:57 268  
[ ]waybel19__663_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel19__839_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel19__840_35.min1.thm1.tptp2017-02-06 16:57 279  
[ ]waybel20__81_42.min1.thm1.tptp2017-02-06 16:57 246  
[ ]waybel20__95_48.min1.thm1.tptp2017-02-06 16:57 338  
[ ]waybel20__1090_42.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel20__1386_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel20__1537_42.min1.thm1.tptp2017-02-06 16:57 412  
[ ]waybel20__1610_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel20__1652_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel20__1715_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel20__1722_35.min1.thm1.tptp2017-02-06 16:57 280  
[ ]waybel20__1781_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel20__1836_42.min1.thm1.tptp2017-02-06 16:57 412  
[ ]waybel20__1990_44.min1.thm1.tptp2017-02-06 16:57 452  
[ ]waybel20__2002_42.min1.thm1.tptp2017-02-06 16:57 440  
[ ]waybel20__2030_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel20__2071_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel21__895_33.min1.thm1.tptp2017-02-06 16:57 270  
[ ]waybel21__1472_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel21__1680_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel21__1695_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel21__1934_39.min1.thm1.tptp2017-02-06 16:57 297  
[ ]waybel22__458_44.min1.thm1.tptp2017-02-06 16:57 260  
[ ]waybel22__868_41.min1.thm1.tptp2017-02-06 16:57 284  
[ ]waybel22__1013_48.min1.thm1.tptp2017-02-06 16:57 396  
[ ]waybel23__262_49.min1.thm1.tptp2017-02-06 16:57 296  
[ ]waybel23__1930_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel23__2268_64.min1.thm1.tptp2017-02-06 16:57 422  
[ ]waybel23__2476_42.min1.thm1.tptp2017-02-06 16:57 284  
[ ]waybel24__950_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel25__636_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel25__842_45.min1.thm1.tptp2017-02-06 16:57 312  
[ ]waybel25__1039_45.min1.thm1.tptp2017-02-06 16:57 268  
[ ]waybel25__2120_33.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel26__430_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel26__495_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel26__1273_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel26__1414_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel26__1561_45.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel26__1598_43.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel26__2229_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel27__1085_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel27__1086_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel27__1593_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel27__2042_43.min1.thm1.tptp2017-02-06 16:57 260  
[ ]waybel27__2376_43.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel28__157_40.min1.thm1.tptp2017-02-06 16:57 288  
[ ]waybel28__399_42.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel28__532_48.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel29__1689_56.min1.thm1.tptp2017-02-06 16:57 410  
[ ]waybel29__2595_64.min1.thm1.tptp2017-02-06 16:57 388  
[ ]waybel29__2618_38.min1.thm1.tptp2017-02-06 16:57 287  
[ ]waybel29__2619_38.min1.thm1.tptp2017-02-06 16:57 287  
[ ]waybel29__2638_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel29__2639_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel29__2662_76.min1.thm1.tptp2017-02-06 16:57 388  
[ ]waybel29__2684_38.min1.thm1.tptp2017-02-06 16:57 287  
[ ]waybel29__2685_38.min1.thm1.tptp2017-02-06 16:57 287  
[ ]waybel29__2704_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel29__2705_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel32__1232_39.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel33__363_34.min1.thm1.tptp2017-02-06 16:57 270  
[ ]waybel34__447_44.min1.thm1.tptp2017-02-06 16:57 372  
[ ]waybel34__550_44.min1.thm1.tptp2017-02-06 16:57 372  
[ ]waybel34__612_44.min1.thm1.tptp2017-02-06 16:57 364  
[ ]waybel34__640_44.min1.thm1.tptp2017-02-06 16:57 364  
[ ]waybel34__1012_37.min1.thm1.tptp2017-02-06 16:57 290  
[ ]waybel34__1046_37.min1.thm1.tptp2017-02-06 16:57 292  
[ ]waybel34__1121_35.min1.thm1.tptp2017-02-06 16:57 312  
[ ]waybel34__1176_33.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel34__2159_38.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel34__2170_36.min1.thm1.tptp2017-02-06 16:57 304  
[ ]waybel34__2691_46.min1.thm1.tptp2017-02-06 16:57 312  
[ ]waybel34__2988_37.min1.thm1.tptp2017-02-06 16:57 292  
[ ]waybel35__161_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel_1__682_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel_1__776_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel_1__1045_33.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel_1__1159_33.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel_1__1529_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel_1__2440_37.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel_1__2562_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel_3__1302_41.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel_3__1375_41.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel_4__947_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel_4__1210_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel_4__1215_42.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel_4__1273_46.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel_4__1372_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]waybel_4__1528_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel_4__1559_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel_4__1651_40.min1.thm1.tptp2017-02-06 16:57 270  
[ ]waybel_4__1708_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel_4__1858_49.min1.thm1.tptp2017-02-06 16:57 312  
[ ]waybel_4__2072_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel_4__2230_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel_4__2274_44.min1.thm1.tptp2017-02-06 16:57 294  
[ ]waybel_5__862_45.min1.thm1.tptp2017-02-06 16:57 268  
[ ]waybel_5__987_43.min1.thm1.tptp2017-02-06 16:57 264  
[ ]waybel_5__1012_39.min1.thm1.tptp2017-02-06 16:57 264  
[ ]waybel_5__1100_45.min1.thm1.tptp2017-02-06 16:57 276  
[ ]waybel_5__1263_48.min1.thm1.tptp2017-02-06 16:57 336  
[ ]waybel_5__1398_46.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel_5__1423_48.min1.thm1.tptp2017-02-06 16:57 288  
[ ]waybel_5__1444_40.min1.thm1.tptp2017-02-06 16:57 280  
[ ]waybel_5__1945_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel_5__2084_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel_5__2468_44.min1.thm1.tptp2017-02-06 16:57 260  
[ ]waybel_5__2558_43.min1.thm1.tptp2017-02-06 16:57 264  
[ ]waybel_5__2762_41.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel_5__2787_41.min1.thm1.tptp2017-02-06 16:57 252  
[ ]waybel_5__2848_45.min1.thm1.tptp2017-02-06 16:57 272  
[ ]waybel_6__66_44.min1.thm1.tptp2017-02-06 16:57 254  
[ ]waybel_6__443_44.min1.thm1.tptp2017-02-06 16:57 260  
[ ]waybel_6__1241_44.min1.thm1.tptp2017-02-06 16:57 286  
[ ]waybel_6__1983_48.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel_6__1994_46.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel_6__2296_42.min1.thm1.tptp2017-02-06 16:57 500  
[ ]waybel_6__2316_42.min1.thm1.tptp2017-02-06 16:57 500  
[ ]waybel_6__2576_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]waybel_6__2689_44.min1.thm1.tptp2017-02-06 16:57 260  
[ ]waybel_7__901_37.min1.thm1.tptp2017-02-06 16:57 280  
[ ]waybel_9__1548_39.min1.thm1.tptp2017-02-06 16:57 266  
[ ]weddwitt__833_39.min1.thm1.tptp2017-02-06 16:57 332  
[ ]weddwitt__993_39.min1.thm1.tptp2017-02-06 16:57 278  
[ ]weddwitt__1168_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]weddwitt__1319_21.min1.thm1.tptp2017-02-06 16:57 383  
[ ]weddwitt__1627_40.min1.thm1.tptp2017-02-06 16:57 286  
[ ]weddwitt__1707_45.min1.thm1.tptp2017-02-06 16:57 308  
[ ]weddwitt__1795_45.min1.thm1.tptp2017-02-06 16:57 308  
[ ]weddwitt__1985_60.min1.thm1.tptp2017-02-06 16:57 340  
[ ]weddwitt__2012_48.min1.thm1.tptp2017-02-06 16:57 304  
[ ]weddwitt__2125_40.min1.thm1.tptp2017-02-06 16:57 288  
[ ]weddwitt__2129_40.min1.thm1.tptp2017-02-06 16:57 288  
[ ]weddwitt__2225_45.min1.thm1.tptp2017-02-06 16:57 310  
[ ]weddwitt__2283_45.min1.thm1.tptp2017-02-06 16:57 310  
[ ]weddwitt__2504_38.min1.thm1.tptp2017-02-06 16:57 294  
[ ]wellfnd1__514_35.min1.thm1.tptp2017-02-06 16:57 278  
[ ]xxreal_0__114_46.min1.thm1.tptp2017-02-06 16:57 254  
[ ]xxreal_0__126_42.min1.thm1.tptp2017-02-06 16:57 262  
[ ]xxreal_0__159_58.min1.thm1.tptp2017-02-06 16:57 346  
[ ]xxreal_3__221_31.min1.thm1.tptp2017-02-06 16:57 287  
[ ]yellow10__86_33.min1.thm1.tptp2017-02-06 16:57 264  
[ ]yellow10__87_33.min1.thm1.tptp2017-02-06 16:57 264  
[ ]yellow10__114_33.min1.thm1.tptp2017-02-06 16:57 264  
[ ]yellow10__115_33.min1.thm1.tptp2017-02-06 16:57 264  
[ ]yellow10__145_35.min1.thm1.tptp2017-02-06 16:57 272  
[ ]yellow10__146_35.min1.thm1.tptp2017-02-06 16:57 272  
[ ]yellow10__170_35.min1.thm1.tptp2017-02-06 16:57 272  
[ ]yellow10__171_35.min1.thm1.tptp2017-02-06 16:57 272  
[ ]yellow11__5065_39.min1.thm1.tptp2017-02-06 16:57 302  
[ ]yellow12__619_40.min1.thm1.tptp2017-02-06 16:57 412  
[ ]yellow12__679_40.min1.thm1.tptp2017-02-06 16:57 412  
[ ]yellow14__860_37.min1.thm1.tptp2017-02-06 16:57 262  
[ ]yellow14__1158_35.min1.thm1.tptp2017-02-06 16:57 254  
[ ]yellow14__1198_41.min1.thm1.tptp2017-02-06 16:57 268  
[ ]yellow15__1241_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]yellow16__1171_41.min1.thm1.tptp2017-02-06 16:57 252  
[ ]yellow16__1728_43.min1.thm1.tptp2017-02-06 16:57 286  
[ ]yellow16__1832_41.min1.thm1.tptp2017-02-06 16:57 278  
[ ]yellow17__237_38.min1.thm1.tptp2017-02-06 16:57 294  
[ ]yellow17__280_42.min1.thm1.tptp2017-02-06 16:57 254  
[ ]yellow17__491_33.min1.thm1.tptp2017-02-06 16:57 244  
[ ]yellow17__685_44.min1.thm1.tptp2017-02-06 16:57 368  
[ ]yellow18__253_43.min1.thm1.tptp2017-02-06 16:57 340  
[ ]yellow18__410_43.min1.thm1.tptp2017-02-06 16:57 368  
[ ]yellow18__411_43.min1.thm1.tptp2017-02-06 16:57 368  
[ ]yellow18__954_46.min1.thm1.tptp2017-02-06 16:57 358  
[ ]yellow18__1202_46.min1.thm1.tptp2017-02-06 16:57 358  
[ ]yellow18__1328_57.min1.thm1.tptp2017-02-06 16:57 370  
[ ]yellow18__1483_57.min1.thm1.tptp2017-02-06 16:57 370  
[ ]yellow18__3029_60.min1.thm1.tptp2017-02-06 16:57 418  
[ ]yellow18__3164_40.min1.thm1.tptp2017-02-06 16:57 290  
[ ]yellow18__3551_56.min1.thm1.tptp2017-02-06 16:57 358  
[ ]yellow18__3842_34.min1.thm1.tptp2017-02-06 16:57 278  
[ ]yellow19__244_37.min1.thm1.tptp2017-02-06 16:57 358  
[ ]yellow19__641_39.min1.thm1.tptp2017-02-06 16:57 372  
[ ]yellow19__670_45.min1.thm1.tptp2017-02-06 16:57 384  
[ ]yellow19__671_45.min1.thm1.tptp2017-02-06 16:57 384  
[ ]yellow19__675_45.min1.thm1.tptp2017-02-06 16:57 385  
[ ]yellow19__690_47.min1.thm1.tptp2017-02-06 16:57 384  
[ ]yellow20__379_39.min1.thm1.tptp2017-02-06 16:57 338  
[ ]yellow20__380_39.min1.thm1.tptp2017-02-06 16:57 338  
[ ]yellow20__886_45.min1.thm1.tptp2017-02-06 16:57 292  
[ ]yellow20__895_43.min1.thm1.tptp2017-02-06 16:57 284  
[ ]yellow20__953_39.min1.thm1.tptp2017-02-06 16:57 400  
[ ]yellow20__1247_35.min1.thm1.tptp2017-02-06 16:57 394  
[ ]yellow20__1349_35.min1.thm1.tptp2017-02-06 16:57 394  
[ ]yellow20__1657_53.min1.thm1.tptp2017-02-06 16:57 508  
[ ]yellow21__581_48.min1.thm1.tptp2017-02-06 16:57 386  
[ ]yellow21__869_49.min1.thm1.tptp2017-02-06 16:57 408  
[ ]yellow21__931_49.min1.thm1.tptp2017-02-06 16:57 408  
[ ]yellow21__1717_47.min1.thm1.tptp2017-02-06 16:57 296  
[ ]yellow21__1776_44.min1.thm1.tptp2017-02-06 16:57 364  
[ ]yellow_0__61_37.min1.thm1.tptp2017-02-06 16:57 280  
[ ]yellow_0__82_39.min1.thm1.tptp2017-02-06 16:57 524  
[ ]yellow_0__100_37.min1.thm1.tptp2017-02-06 16:57 402  
[ ]yellow_0__1990_45.min1.thm1.tptp2017-02-06 16:57 328  
[ ]yellow_0__2044_45.min1.thm1.tptp2017-02-06 16:57 328  
[ ]yellow_1__455_50.min1.thm1.tptp2017-02-06 16:57 400  
[ ]yellow_1__474_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]yellow_1__486_42.min1.thm1.tptp2017-02-06 16:57 278  
[ ]yellow_1__1243_43.min1.thm1.tptp2017-02-06 16:57 308  
[ ]yellow_1__1411_41.min1.thm1.tptp2017-02-06 16:57 276  
[ ]yellow_1__1453_43.min1.thm1.tptp2017-02-06 16:57 284  
[ ]yellow_1__1480_41.min1.thm1.tptp2017-02-06 16:57 276  
[ ]yellow_1__1534_41.min1.thm1.tptp2017-02-06 16:57 276  
[ ]yellow_1__1577_43.min1.thm1.tptp2017-02-06 16:57 284  
[ ]yellow_1__1606_41.min1.thm1.tptp2017-02-06 16:57 276  
[ ]yellow_2__349_35.min1.thm1.tptp2017-02-06 16:57 270  
[ ]yellow_3__625_25.min1.thm1.tptp2017-02-06 16:57 535  
[ ]yellow_3__2210_35.min1.thm1.tptp2017-02-06 16:57 270  
[ ]yellow_3__2211_35.min1.thm1.tptp2017-02-06 16:57 270  
[ ]yellow_3__2241_35.min1.thm1.tptp2017-02-06 16:57 270  
[ ]yellow_3__2242_35.min1.thm1.tptp2017-02-06 16:57 270  
[ ]yellow_6__1252_45.min1.thm1.tptp2017-02-06 16:57 302  
[ ]yellow_6__1265_45.min1.thm1.tptp2017-02-06 16:57 302  
[ ]yellow_6__1289_43.min1.thm1.tptp2017-02-06 16:57 294  
[ ]yellow_6__2946_44.min1.thm1.tptp2017-02-06 16:57 306  
[ ]yellow_7__1357_47.min1.thm1.tptp2017-02-06 16:57 280  
[ ]yellow_7__1446_45.min1.thm1.tptp2017-02-06 16:57 268  
[ ]yellow_9__1741_37.min1.thm1.tptp2017-02-06 16:57 294  
[ ]yellow_9__1742_37.min1.thm1.tptp2017-02-06 16:57 294  
[ ]zf_colla__356_41.min1.thm1.tptp2017-02-06 16:57 246  
[ ]zf_colla__851_38.min1.thm1.tptp2017-02-06 16:57 246  
[ ]zf_fund2__190_43.min1.thm1.tptp2017-02-06 16:57 336  
[ ]zf_fund2__226_38.min1.thm1.tptp2017-02-06 16:57 258  
[ ]zf_fund2__241_44.min1.thm1.tptp2017-02-06 16:57 258  
[ ]zf_fund2__319_42.min1.thm1.tptp2017-02-06 16:57 246  
[ ]zf_lang1__1128_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]zf_lang1__1158_41.min1.thm1.tptp2017-02-06 16:57 252  
[ ]zf_refle__67_43.min1.thm1.tptp2017-02-06 16:57 232  
[ ]zfmodel1__550_39.min1.thm1.tptp2017-02-06 16:57 240  
[ ]zfmodel1__1063_44.min1.thm1.tptp2017-02-06 16:57 268  
[ ]zfmodel1__1853_41.min1.thm1.tptp2017-02-06 16:57 252  
[ ]zfmodel2__1562_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]zfmodel2__1894_42.min1.thm1.tptp2017-02-06 16:57 252  
[ ]zfmodel2__1972_35.min1.thm1.tptp2017-02-06 16:57 252  
[ ]zmodul01__2163_40.min1.thm1.tptp2017-02-06 16:57 276  
[ ]zmodul01__2608_39.min1.thm1.tptp2017-02-06 16:57 284  
[ ]zmodul01__2616_39.min1.thm1.tptp2017-02-06 16:57 286  
[ ]zmodul01__3323_62.min1.thm1.tptp2017-02-06 16:57 434  
[ ]zmodul01__3363_62.min1.thm1.tptp2017-02-06 16:57 434  
[ ]zmodul01__3611_39.min1.thm1.tptp2017-02-06 16:57 328  
[ ]zmodul01__3612_41.min1.thm1.tptp2017-02-06 16:57 347  
Apache/2.4.18 (Ubuntu) Server at grid01.ciirc.cvut.cz Port 80