Str	Args	Cheat	Add	Prems	Prover	Thm%	CoS%	Uniq	ST⌀	STΣ	Thm	CoS	Maybe	Empty	Found
default	default	nc	0	128	epar	51.041	0.000	1	0.024	25.39	1054	0	1011	0	2065
default	default	nc	0	512	epar	50.799	0.000	1	0.025	26.02	1049	0	1016	0	2065
seq	du_div_1.1exps	nc	1	512	epar	49.249	0.000	1	0.020	20.48	1017	0	1048	0	2065
seq	du_div_1.1exps	nc	1	128	epar	48.862	0.000	0	0.018	17.99	1009	0	1056	0	2065
seq	d_u_div_1.1exps	nc	1	128	epar	48.571	0.000	0	0.017	17.44	1003	0	1062	0	2065
seq	d_u_div_1.1exps	nc	1	512	epar	48.329	0.000	0	0.019	18.59	998	0	1067	0	2065
seq	du_div_s2	nc	1	128	epar	48.281	0.000	0	0.017	16.96	997	0	1068	0	2065
seq	d_u_div_s2	nc	1	128	epar	48.184	0.000	0	0.016	16.30	995	0	1070	0	2065
seq	du_div_s2	nc	1	512	epar	48.184	0.000	0	0.017	17.27	995	0	1070	0	2065
seq	d_u_div_s2	nc	1	512	epar	47.651	0.000	0	0.017	16.40	984	0	1081	0	2065
seq	du_div_1.1exps	nc	10	128	epar	47.554	0.000	0	0.016	15.73	982	0	1083	0	2065
seq	du_div_1.1exps	tnc	10	128	epar	47.458	0.000	0	0.016	15.30	980	0	1085	0	2065
seq	du_div_s	nc	1	128	epar	47.312	0.000	0	0.017	16.31	977	0	1088	0	2065
seq	du_div_s	nc	1	512	epar	47.022	0.000	0	0.016	15.96	971	0	1094	0	2065
seq	du_div_1.05exps	nc	10	128	epar	46.780	0.000	0	0.015	14.75	966	0	1099	0	2065
seq	d_u_div_s	nc	1	128	epar	46.731	0.000	0	0.016	15.49	965	0	1100	0	2065
seq	du_div_1.025exps	nc	10	128	epar	46.731	0.000	0	0.016	15.35	965	0	1100	0	2065
seq	d_u_div_s	nc	1	512	epar	46.441	0.000	0	0.016	15.45	959	0	1106	0	2065
seq	du_div_1.1exps	nc	10	512	epar	46.344	0.000	0	0.015	14.68	957	0	1108	0	2065
seq	du_div_1.1exps	tnc	10	512	epar	46.295	0.000	0	0.015	14.65	956	0	1109	0	2065
seq	du_div_1.025exps	nc	10	512	epar	46.053	0.000	0	0.016	14.78	951	0	1114	0	2065
seq	du_div_1.05exps	nc	10	512	epar	45.666	0.000	0	0.015	14.30	943	0	1122	0	2065
seq	du_div_s2	nc	10	128	epar	45.666	0.000	0	0.015	14.19	943	0	1122	0	2065
seq	d_u_div_s2	nc	10	128	epar	45.472	0.000	0	0.015	14.22	939	0	1126	0	2065
seq	du_div_s2	nc	10	512	epar	45.133	0.000	0	0.015	13.65	932	0	1133	0	2065
seq	du_div_s2	tnc	10	128	epar	45.085	0.000	0	0.014	13.33	931	0	1134	0	2065
seq	du_div_s2	tnc	10	512	epar	44.843	0.000	0	0.014	13.07	926	0	1139	0	2065
epcl	3	nc	10	128	epar	44.746	0.000	0	0.017	15.30	924	0	1141	0	2065
epcl	3	nc	10	512	epar	44.746	0.000	0	0.017	15.68	924	0	1141	0	2065
seq	du_div_s	tnc	10	128	epar	44.746	0.000	0	0.016	14.36	924	0	1141	0	2065
seq	d_u_div_s2	nc	10	512	epar	44.697	0.000	0	0.015	13.60	923	0	1142	0	2065
seq	du_div_s	nc	10	128	epar	44.600	0.000	0	0.015	13.62	921	0	1144	0	2065
seq	d_u_div_s	nc	10	128	epar	44.407	0.000	0	0.015	14.20	917	0	1148	0	2065
seq	du_div_s	tnc	10	512	epar	44.407	0.000	0	0.015	13.35	917	0	1148	0	2065
seq	du_div_s	nc	10	512	epar	44.310	0.000	0	0.015	13.36	915	0	1150	0	2065
epcl	1	tnc	10	128	epar	44.165	0.000	0	0.015	13.95	912	0	1153	0	2065
epcl	1	tnc	10	512	epar	43.971	0.000	0	0.015	14.03	908	0	1157	0	2065
seq	d_u_div_s	nc	10	512	epar	43.971	0.000	0	0.015	13.71	908	0	1157	0	2065
epcl	1	nc	10	128	epar	43.826	0.000	0	0.015	13.71	905	0	1160	0	2065
epcl	1	nc	10	512	epar	43.777	0.000	0	0.015	13.76	904	0	1161	0	2065
epcl	2	nc	10	512	epar	43.535	0.000	0	0.018	16.28	899	0	1166	0	2065
epcl	2	nc	10	128	epar	43.196	0.000	0	0.018	15.80	892	0	1173	0	2065
pgrank	u	nc	10	512	epar	43.148	0.000	1	0.019	16.62	891	0	1174	0	2065
seq	du_div_125exps	nc_opt	10	512	epar	43.002	0.000	0	0.016	14.13	888	0	1177	0	2065
seq	du_div_125exps	nc_opt	10	128	epar	42.954	0.000	0	0.015	13.55	887	0	1178	0	2065
seq	du_div_1.1exps	nc_opt	10	512	epar	42.857	0.000	0	0.017	15.05	885	0	1180	0	2065
seq	du_div_1.1exps	nc_opt	10	128	epar	42.712	0.000	0	0.016	14.25	882	0	1183	0	2065
pgrank	u	nc	10	128	epar	42.518	0.000	0	0.017	14.91	878	0	1187	0	2065
seq	du_div_s2	nc_opt	10	512	epar	42.179	0.000	0	0.015	13.17	871	0	1194	0	2065
pgrank	d_div_s	nc	10	512	epar	42.131	0.000	0	0.017	14.38	870	0	1195	0	2065
pgrank	d_div_s	nc	10	128	epar	42.034	0.000	0	0.016	13.76	868	0	1197	0	2065
seq	du_div_s2	nc_opt	10	128	epar	42.034	0.000	0	0.015	13.28	868	0	1197	0	2065
default	default	nc	0	32	epar	41.985	0.533	0	0.016	14.23	867	11	1187	0	2065
seq	d_u_div_1.1exps	nc	1	32	epar	41.695	0.339	0	0.016	13.61	861	7	1197	0	2065
pgrank	du	nc	10	512	epar	41.404	0.000	0	0.017	14.20	855	0	1210	0	2065
seq	du_div_s	nc_opt	10	512	epar	41.404	0.000	0	0.016	13.29	855	0	1210	0	2065
pgrank	du	nc	10	128	epar	41.356	0.000	0	0.017	14.18	854	0	1211	0	2065
seq	du_div_s	nc_opt	10	128	epar	41.356	0.000	0	0.016	13.78	854	0	1211	0	2065
seq	d_u_div_s2	nc	1	32	epar	41.162	0.581	0	0.016	13.66	850	12	1203	0	2065
seq	du_div_1.1exps	nc	1	32	epar	40.242	0.726	1	0.016	13.92	831	15	1219	0	2065
seq	d_u_div_s	nc	1	32	epar	39.952	0.775	0	0.015	12.54	825	16	1224	0	2065
seq	du_div_s2	nc	1	32	epar	39.661	0.581	0	0.014	12.03	819	12	1234	0	2065
seq	du_div_s	nc	1	32	epar	39.613	0.969	2	0.017	14.38	818	20	1227	0	2065
pgrank	d	nc	10	128	epar	38.692	0.000	0	0.015	12.14	799	0	1266	0	2065
pgrank	d	nc	10	512	epar	38.644	0.000	0	0.015	12.10	798	0	1267	0	2065
seq	du_div_1.1exps	tnc	10	32	epar	38.208	1.889	0	0.015	12.01	789	39	1237	0	2065
seq	du_div_1.1exps	nc	10	32	epar	37.918	1.985	0	0.014	11.81	783	41	1241	0	2065
seq	du_div_1.05exps	nc	10	32	epar	37.288	1.404	0	0.014	11.39	770	29	1266	0	2065
seq	d_u_div_s2	nc	10	32	epar	36.465	0.387	0	0.013	9.66	753	8	1304	0	2065
seq	du_div_1.025exps	nc	10	32	epar	36.416	2.228	0	0.012	9.85	752	46	1267	0	2065
seq	du_div_s2	tnc	10	32	epar	35.593	0.726	0	0.013	9.38	735	15	1315	0	2065
seq	du_div_s2	nc	10	32	epar	35.206	0.581	0	0.012	9.23	727	12	1326	0	2065
seq	d_u_div_s	nc	10	32	epar	34.237	1.453	0	0.012	9.03	707	30	1328	0	2065
seq	du_div_125exps	nc_opt	10	32	epar	34.140	1.356	0	0.013	9.40	705	28	1332	0	2065
epcl	3	nc	10	32	epar	33.995	3.293	1	0.014	10.46	702	68	1295	0	2065
seq	du_div_1.1exps	nc_opt	10	32	epar	33.608	1.598	0	0.013	9.61	694	33	1338	0	2065
seq	du_div_s	nc	10	32	epar	33.269	1.646	0	0.012	8.56	687	34	1344	0	2065
seq	du_div_s	tnc	10	32	epar	32.639	1.453	1	0.013	9.21	674	30	1361	0	2065
seq	du_div_s2	nc_opt	10	32	epar	32.107	1.211	0	0.013	8.97	663	25	1377	0	2065
epcl	2	nc	10	32	epar	31.574	5.811	0	0.011	8.22	652	120	1293	0	2065
seq	du_div_s	nc_opt	10	32	epar	31.574	0.920	1	0.015	9.92	652	19	1394	0	2065
epcl	1	nc	10	32	epar	31.186	4.649	1	0.012	9.10	644	96	1325	0	2065
epcl	1	tnc	10	32	epar	31.186	3.874	0	0.011	8.11	644	80	1341	0	2065
pgrank	d_div_s	nc	10	32	epar	30.896	0.581	0	0.014	9.08	638	12	1415	0	2065
pgrank	u	nc	10	32	epar	29.927	0.097	1	0.016	9.71	618	2	1445	0	2065
pgrank	du	nc	10	32	epar	29.588	0.097	0	0.014	8.30	611	2	1452	0	2065
pgrank	d	nc	10	32	epar	26.925	0.194	0	0.015	8.44	556	4	1505	0	2065
default	default	nc	0	8	epar	15.593	30.073	0	0.004	4.04	322	621	1122	0	2065
seq	d_u_div_1.1exps	nc	1	8	epar	15.545	39.031	0	0.004	4.54	321	806	938	0	2065
seq	d_u_div_s2	nc	1	8	epar	15.254	39.322	0	0.004	4.11	315	812	938	0	2065
seq	du_div_s	nc	10	8	epar	14.915	11.671	0	0.007	3.83	308	241	1516	0	2065
seq	du_div_1.1exps	nc	1	8	epar	14.722	41.695	0	0.003	3.96	304	861	900	0	2065
seq	d_u_div_s	nc	1	8	epar	14.673	39.903	2	0.005	5.60	303	824	938	0	2065
seq	d_u_div_s	nc	10	8	epar	14.576	12.930	0	0.006	3.54	301	267	1497	0	2065
seq	du_div_1.025exps	nc	10	8	epar	14.576	29.637	0	0.004	3.29	301	612	1152	0	2065
seq	du_div_s2	nc	1	8	epar	14.576	41.211	0	0.003	3.59	301	851	913	0	2065
seq	du_div_s	nc	1	8	epar	14.528	38.547	0	0.003	3.47	300	796	969	0	2065
pgrank	u	nc	10	8	epar	14.479	1.308	1	0.014	4.72	299	27	1739	0	2065
pgrank	du	nc	10	8	epar	14.334	3.148	0	0.013	4.55	296	65	1704	0	2065
seq	du_div_1.1exps	nc	10	8	epar	14.286	30.944	0	0.003	3.22	295	639	1131	0	2065
seq	du_div_1.1exps	tnc	10	8	epar	14.237	30.363	0	0.004	3.71	294	627	1144	0	2065
seq	d_u_div_s2	nc	10	8	epar	14.044	10.218	0	0.006	3.07	290	211	1564	0	2065
seq	du_div_1.05exps	nc	10	8	epar	14.044	30.847	0	0.003	3.09	290	637	1138	0	2065
epcl	2	nc	10	8	epar	13.753	38.305	0	0.003	3.19	284	791	990	0	2065
seq	du_div_s2	nc	10	8	epar	13.705	10.363	0	0.006	3.00	283	214	1568	0	2065
seq	du_div_s2	tnc	10	8	epar	13.608	10.993	0	0.006	2.96	281	227	1557	0	2065
seq	du_div_s	nc_opt	10	8	epar	13.462	6.489	0	0.009	3.65	278	134	1653	0	2065
seq	du_div_s	tnc	10	8	epar	13.414	13.075	0	0.006	3.09	277	270	1518	0	2065
epcl	3	nc	10	8	epar	13.366	39.080	0	0.003	3.22	276	807	982	0	2065
seq	du_div_s2	nc_opt	10	8	epar	13.220	9.298	0	0.007	3.23	273	192	1600	0	2065
seq	du_div_125exps	nc_opt	10	8	epar	13.075	15.496	0	0.006	3.44	270	320	1475	0	2065
seq	du_div_1.1exps	nc_opt	10	8	epar	12.833	16.804	0	0.005	3.05	265	347	1453	0	2065
epcl	1	nc	10	8	epar	12.639	39.274	0	0.003	2.88	261	811	993	0	2065
epcl	1	tnc	10	8	epar	12.349	40.678	0	0.003	2.82	255	840	970	0	2065
pgrank	d_div_s	nc	10	8	epar	11.768	6.295	0	0.009	3.24	243	130	1692	0	2065
pgrank	d	nc	10	8	epar	10.363	4.019	0	0.008	2.51	214	83	1768	0	2065
any						62.373	75.109				1288	1551			2065

Greedy sequence

Prover	Sum%	Sum	G+2	G1+2	G-1+2	G+2M	Alt
default-default-nc-0-128-epar	51.041	1054
epcl-2-nc-10-512-epar	54.286	1121
seq-d_u_div_1.1exps-nc-1-32-epar	56.174	1160
seq-du_div_125exps-nc_opt-10-512-epar	57.433	1186
seq-du_div_1.1exps-nc-1-512-epar	58.015	1198					= seq-d_u_div_s-nc-10-128-epar = seq-du_div_s-nc_opt-10-128-epar
seq-du_div_1.1exps-tnc-10-32-epar	58.499	1208					= seq-du_div_1.1exps-nc-10-32-epar = seq-du_div_s-nc_opt-10-128-epar = pgrank-d-nc-10-512-epar = ... (6)
seq-du_div_s-nc_opt-10-128-epar	58.983	1218					= pgrank-d-nc-10-512-epar = pgrank-d_div_s-nc-10-512-epar
pgrank-d_div_s-nc-10-128-epar	59.370	1226					= seq-d_u_div_1.1exps-nc-1-8-epar = seq-du_div_125exps-nc_opt-10-8-epar = seq-d_u_div_s-nc-1-8-epar = ... (4)
seq-d_u_div_1.1exps-nc-1-8-epar	59.758	1234					= seq-du_div_125exps-nc_opt-10-8-epar = seq-d_u_div_s-nc-1-8-epar
pgrank-u-nc-10-512-epar	60.048	1240
seq-du_div_s2-nc-10-128-epar	60.242	1244					= seq-du_div_s-nc-1-32-epar = seq-d_u_div_s-nc-1-128-epar = seq-d_u_div_s2-nc-10-128-epar = ... (10)
seq-du_div_s-nc-1-32-epar	60.436	1248					= seq-du_div_s-nc-1-128-epar = default-default-nc-0-512-epar = seq-du_div_125exps-nc_opt-10-8-epar = ... (6)
default-default-nc-0-512-epar	60.630	1252					= seq-du_div_125exps-nc_opt-10-8-epar = seq-d_u_div_s-nc-1-8-epar = seq-du_div_s-nc-1-512-epar
seq-du_div_125exps-nc_opt-10-8-epar	60.823	1256					= seq-d_u_div_s-nc-1-8-epar
pgrank-du-nc-10-512-epar	60.969	1259					= pgrank-du-nc-10-128-epar = seq-du_div_s-nc-1-128-epar
seq-du_div_s-nc-1-128-epar	61.114	1262
seq-du_div_1.025exps-nc-10-512-epar	61.211	1264					= seq-du_div_1.1exps-nc-10-128-epar = seq-du_div_1.1exps-nc_opt-10-32-epar = pgrank-du-nc-10-32-epar = ... (12)
seq-du_div_1.1exps-nc-10-128-epar	61.308	1266					= seq-du_div_1.1exps-nc_opt-10-32-epar = pgrank-du-nc-10-32-epar = seq-du_div_s-nc_opt-10-8-epar = ... (9)
seq-du_div_1.1exps-nc_opt-10-32-epar	61.404	1268					= pgrank-du-nc-10-32-epar = seq-du_div_s-nc_opt-10-8-epar = seq-du_div_s-nc-10-8-epar = ... (8)
pgrank-du-nc-10-32-epar	61.501	1270					= seq-du_div_s-nc_opt-10-8-epar = seq-du_div_s-nc-10-8-epar = seq-du_div_1.1exps-nc_opt-10-128-epar = ... (7)
seq-du_div_1.1exps-nc_opt-10-128-epar	61.598	1272					= seq-du_div_1.1exps-nc_opt-10-512-epar = seq-d_u_div_s-nc-1-8-epar = seq-du_div_s-nc_opt-10-32-epar
seq-d_u_div_s-nc-1-8-epar	61.695	1274					= seq-du_div_s-nc_opt-10-32-epar
seq-du_div_s-nc_opt-10-32-epar	61.792	1276
epcl-3-nc-10-8-epar	61.840	1277					= epcl-1-nc-10-32-epar = seq-du_div_s-nc_opt-10-8-epar = seq-du_div_s-nc-10-8-epar = ... (22)
epcl-1-nc-10-32-epar	61.889	1278					= pgrank-u-nc-10-8-epar = seq-d_u_div_s-nc-10-128-epar = pgrank-u-nc-10-32-epar = ... (19)
pgrank-u-nc-10-8-epar	61.937	1279					= seq-d_u_div_s-nc-10-128-epar = pgrank-u-nc-10-32-epar = epcl-1-nc-10-512-epar = ... (18)
seq-d_u_div_s-nc-10-128-epar	61.985	1280					= pgrank-u-nc-10-32-epar = epcl-1-nc-10-512-epar = epcl-1-nc-10-128-epar = ... (17)
pgrank-u-nc-10-32-epar	62.034	1281					= epcl-1-nc-10-512-epar = epcl-1-nc-10-128-epar = epcl-1-tnc-10-512-epar = ... (15)
epcl-1-nc-10-512-epar	62.082	1282					= epcl-1-nc-10-128-epar = epcl-1-tnc-10-512-epar = epcl-3-nc-10-32-epar = ... (14)
epcl-3-nc-10-32-epar	62.131	1283					= seq-du_div_1.05exps-nc-10-512-epar = seq-du_div_1.1exps-nc-10-512-epar = pgrank-d_div_s-nc-10-32-epar = ... (10)
seq-du_div_1.05exps-nc-10-512-epar	62.179	1284					= seq-du_div_1.1exps-nc-10-512-epar = pgrank-d_div_s-nc-10-32-epar = seq-du_div_s2-nc_opt-10-512-epar = ... (9)
pgrank-d_div_s-nc-10-32-epar	62.228	1285					= seq-du_div_s2-nc_opt-10-512-epar = seq-du_div_1.1exps-nc-1-32-epar = seq-du_div_s2-nc_opt-10-128-epar = ... (5)
seq-du_div_s2-nc_opt-10-512-epar	62.276	1286					= seq-du_div_1.1exps-nc-1-32-epar = seq-du_div_s2-nc_opt-10-128-epar = seq-du_div_s-tnc-10-32-epar
seq-du_div_1.1exps-nc-1-32-epar	62.324	1287					= seq-du_div_s-tnc-10-32-epar
seq-du_div_s-tnc-10-32-epar	62.373	1288