Str	Args	Deps	Syms	Prems	Prover	Thm%	CoS%	Uniq	ST⌀	STΣ	Thm	CoS	Maybe	Empty	Err	Found
lsi	3200ti_8_80	a13	s0	0128	epar3	51.383	0.000	3	0.093	98.18	1059	0	1002	0	0	2061
comb	min_2k_20_20	a13	s0	0128	epar3	51.043	0.000	11	0.099	104.19	1052	0	1009	0	0	2061
comb	har_2k_k200_33_33	a13	s0e	0256	epar3	50.315	0.000	1	0.087	90.70	1037	0	1024	0	0	2061
comb	geo_2k_50_00	a13	s0e	0096	vam30	49.588	0.000	3	0.091	93.14	1022	0	1039	0	0	2061
lsi	3200ti_8_80	a13	s0	0128	vam30	49.005	0.000	2	0.091	92.35	1010	0	1051	0	0	2061
geo	r_90	a13	s0e	0256	epar3	48.860	0.000	5	0.089	89.91	1007	0	1054	0	0	2061
comb	qua_2k_k200_33_33	a13	s0e	0512	epar3	47.356	0.000	10	0.096	93.84	976	0	1085	0	0	2061
comb	geo_2k_50_50	a13	s0	0064	epar3	47.065	0.194	12	0.102	99.65	970	4	1087	0	0	2061
geo	r_90	a13	s0e	0256	vam30	46.822	0.000	6	0.090	86.37	965	0	1096	0	0	2061
nb	idf010	a13	s0e	0128	epar3	44.250	0.000	4	0.091	83.33	912	0	1149	0	0	2061
geo	r_99	a13	s0e	0064	vam30	43.231	0.000	8	0.096	85.96	891	0	1170	0	0	2061
comb	geo_2k_60_20	a13	s0	1024	vam30	42.989	0.000	6	0.091	80.39	886	0	1175	0	0	2061
knn	is_200	a13	sde	1024	vam30	41.533	0.000	2	0.084	71.68	856	0	1205	0	0	2061
knn	is_40	a13	s0e	0096	z3_40	41.242	0.000	38	0.132	112.27	850	0	0	1211	0	2061
knn	is_80	m13	sde	1024	vam30	41.242	0.000	3	0.087	73.61	850	0	1211	0	0	2061
comb	min_2k_20_20	a13	s0	0128	vam30	55.224	0.000	0	0.028	1.05	37	0	30	0	0	67
comb	har_2k_k200_33_33	a13	s0e	0256	vam30	53.731	0.000	0	0.029	1.04	36	0	31	0	0	67
comb	qua_2k_k200_33_33	a13	s0e	0512	vam30	53.731	0.000	0	0.034	1.24	36	0	31	0	0	67
comb	geo_2k_50_00	a13	s0e	0096	epar3	52.239	0.000	0	0.029	1.02	35	0	32	0	0	67
knn	is_200	a13	sde	0064	epar3	52.239	4.478	0	0.035	1.33	35	3	29	0	0	67
comb	geo_2k_33_33	a13	s0	0256	vam30	50.746	0.000	0	0.027	0.93	34	0	33	0	0	67
knn	is_40	a13	s0e	0096	epar3	50.746	0.000	0	0.025	0.83	34	0	33	0	0	67
knn	is_40	a13	s0e	0096	vam30	49.254	0.000	0	0.027	0.88	33	0	34	0	0	67
comb	geo_2k_33_33	a13	s0	0256	epar3	47.761	0.000	0	0.025	0.80	32	0	35	0	0	67
comb	geo_2k_50_00	a13	s0e	0096	z3_40	47.761	0.000	0	0.027	0.85	32	0	0	35	0	67
comb	min_2k_20_20	a13	s0	0128	z3_40	47.761	0.000	0	0.028	0.89	32	0	0	35	0	67
comb	min_2k_60_20	a13	s0	1024	vam30	47.761	0.000	0	0.034	1.09	32	0	35	0	0	67
knn	is_200	a13	sde	0064	z3_40	47.761	0.000	0	0.039	1.25	32	0	0	35	0	67
geo	r_99	a13	s0e	0064	epar3	46.269	0.000	0	0.036	1.12	31	0	36	0	0	67
nb	idf010	a13	s0e	0128	vam30	46.269	0.000	0	0.038	1.18	31	0	36	0	0	67
comb	geo_2k_60_20	a13	s0	1024	epar3	44.776	0.000	0	0.029	0.86	30	0	37	0	0	67
lsi	3200ti_8_80	a13	s0	0128	z3_40	44.776	0.000	0	0.032	0.95	30	0	0	37	0	67
comb	geo_2k_33_33	a13	s0	1536	vam30	43.284	0.000	0	0.039	1.12	29	0	38	0	0	67
comb	geo_2k_50_50	a13	s0	0064	vam30	43.284	0.000	0	0.028	0.81	29	0	38	0	0	67
comb	min_2k_60_20	a13	s0	1024	epar3	43.284	0.000	0	0.027	0.78	29	0	38	0	0	67
knn	is_200	a13	sde	1024	epar3	43.284	0.000	0	0.025	0.72	29	0	38	0	0	67
comb	geo_2k_50_50	a13	s0	0064	z3_40	41.791	0.000	0	0.027	0.76	28	0	0	39	0	67
comb	geo_2k_60_20	a13	s0	0032	epar3	41.791	1.493	0	0.043	1.24	28	1	38	0	0	67
knn	is_200	a13	sde	0064	vam30	41.791	1.493	0	0.028	0.83	28	1	38	0	0	67
comb	geo_2k_60_20	a13	s0	0032	vam30	38.806	0.000	0	0.028	0.74	26	0	41	0	0	67
geo	r_99	a13	s0e	0064	z3_40	38.806	0.000	0	0.022	0.58	26	0	0	41	0	67
knn	is_80	m13	sde	1024	epar3	38.806	0.000	0	0.022	0.58	26	0	41	0	0	67
nb	idf010	a13	s0e	0128	z3_40	38.806	0.000	0	0.027	0.70	26	0	0	41	0	67
comb	geo_2k_33_33	a13	s0	0256	z3_40	37.313	0.000	0	0.032	0.80	25	0	0	42	0	67
comb	geo_2k_33_33	a13	s0	1536	epar3	37.313	0.000	0	0.022	0.56	25	0	42	0	0	67
comb	har_2k_k200_33_33	a13	s0e	0256	z3_40	37.313	0.000	0	0.030	0.75	25	0	0	42	0	67
comb	geo_2k_60_20	a13	s0	0032	z3_40	35.821	0.000	0	0.029	0.68	24	0	0	43	0	67
geo	r_90	a13	s0e	0256	z3_40	35.821	0.000	0	0.027	0.65	24	0	0	43	0	67
nb	idf070	m13	sde	0256	vam30	52.174	0.000	0	0.036	0.86	24	0	22	0	0	46
nb	idf070	m13	sde	0256	epar3	45.652	0.000	0	0.023	0.48	21	0	25	0	0	46
knn	is_40	b13	s0e	0064	epar3	28.358	0.000	0	0.021	0.40	19	0	48	0	0	67
knn	is_40	b13	s0e	0064	vam30	28.358	0.000	0	0.021	0.40	19	0	48	0	0	67
comb	qua_2k_k200_33_33	a13	s0e	0512	z3_40	26.866	0.000	0	0.021	0.39	18	0	0	49	0	67
knn	is_40	b13	s0e	0064	z3_40	25.373	0.000	0	0.020	0.34	17	0	0	50	0	67
knn	is_200	a13	sde	1024	z3_40	23.881	0.000	0	0.022	0.35	16	0	0	51	0	67
nb	idf070	m13	sde	0256	z3_40	34.783	0.000	0	0.024	0.39	16	0	0	30	0	46
comb	geo_2k_60_20	a13	s0	1024	z3_40	22.388	0.000	0	0.022	0.33	15	0	0	52	0	67
knn	is_80	m13	sde	1024	z3_40	20.896	0.000	0	0.022	0.30	14	0	0	53	0	67
comb	geo_2k_33_33	a13	s0	1536	z3_40	19.403	0.000	0	0.022	0.28	13	0	0	54	0	67
comb	min_2k_60_20	a13	s0	1024	z3_40	19.403	0.000	0	0.022	0.28	13	0	0	54	0	67
any						67.443	0.388				1390	8				2061

Greedy sequence

Prover	Sum%	Sum	G+2	G1+2	G-1+2	G+2M	Alt
lsi-3200ti_8_80-a13-s0-0128-epar3	51.383	1059
knn-is_40-a13-s0e-0096-z3_40	57.011	1175
comb-geo_2k_60_20-a13-s0-1024-vam30	60.019	1237
geo-r_99-a13-s0e-0064-vam30	61.912	1276					= comb-geo_2k_50_50-a13-s0-0064-epar3
comb-geo_2k_50_50-a13-s0-0064-epar3	63.270	1304
comb-qua_2k_k200_33_33-a13-s0e-0512-epar3	64.435	1328
comb-min_2k_20_20-a13-s0-0128-epar3	65.211	1344
geo-r_90-a13-s0e-0256-vam30	65.842	1357
knn-is_200-a13-sde-1024-vam30	66.279	1366
comb-geo_2k_50_00-a13-s0e-0096-vam30	66.570	1372					= nb-idf010-a13-s0e-0128-epar3 = geo-r_90-a13-s0e-0256-epar3
nb-idf010-a13-s0e-0128-epar3	66.861	1378					= geo-r_90-a13-s0e-0256-epar3
geo-r_90-a13-s0e-0256-epar3	67.103	1383
knn-is_80-m13-sde-1024-vam30	67.249	1386
lsi-3200ti_8_80-a13-s0-0128-vam30	67.346	1388
comb-geo_2k_33_33-a13-s0-0256-epar3	67.394	1389					= lsi-3200ti_8_80-a13-s0-0128-z3_40 = comb-geo_2k_33_33-a13-s0-0256-z3_40 = geo-r_90-a13-s0e-0256-z3_40 = ... (15)
comb-har_2k_k200_33_33-a13-s0e-0256-epar3	67.443	1390