Str	Args	Deps	Syms	Prems	Prover	Thm%	Uniq	ST⌀	STΣ	Thm	Maybe	Empty	Found
default	default	0	0	512	epar	22.439	1	0.020	8.00	403	1393	0	1796
seq	d2_div_s	0	10	128	epar	22.383	0	0.015	5.86	402	1393	1	1796
default	default	0	0	128	epar	22.327	0	0.014	5.79	401	1395	0	1796
seq	d2_div_s	0	20	128	epar	22.105	0	0.014	5.41	397	1394	5	1796
pgrank	u_div_s	0	10	128	epar	22.049	0	0.014	5.74	396	1339	61	1796
seq	d2_div_s	0	10	512	epar	22.049	0	0.017	6.58	396	1400	0	1796
maxcut	default	0	1	128	epar	21.993	0	0.015	5.82	395	1396	5	1796
pgrank	du_div_s	0	20	128	epar	21.882	0	0.015	6.04	393	1355	48	1796
seq	d_u_div_s2	0	10	128	epar	21.826	0	0.013	5.21	392	1396	8	1796
pgrank	du_div_s	0	10	128	epar	21.771	0	0.014	5.54	391	1386	19	1796
epcl	default	0	10	128	epar	21.715	0	0.014	5.43	390	1399	7	1796
seq	d2_div_s	0	20	512	epar	21.715	0	0.017	6.64	390	1404	2	1796
seq	d_u_div_exps	0	20	128	epar	21.659	1	0.016	6.35	389	1387	20	1796
seq	d_u_div_exps	0	10	128	epar	21.548	0	0.014	5.31	387	1401	8	1796
seq	d_u_div_s	0	10	128	epar	21.548	0	0.014	5.47	387	1403	6	1796
seq	d_u_div_exps	0	10	512	epar	21.437	0	0.014	5.36	385	1404	7	1796
seq	d_u_div_s2	0	20	128	epar	21.437	0	0.014	5.34	385	1396	15	1796
pgrank	u_div_s	0	20	128	epar	21.381	1	0.019	7.47	384	1307	105	1796
pgrank	u_div_s	0	10	512	epar	21.325	1	0.018	6.76	383	1355	58	1796
maxcut	default	0	5	512	epar	21.214	0	0.015	5.75	381	1391	24	1796
pgrank	du	0	10	128	epar	21.214	0	0.012	4.76	381	1409	6	1796
epcl	default	0	20	128	epar	21.158	0	0.013	4.85	380	1404	12	1796
maxcut	default	0	10	512	epar	21.102	1	0.018	6.99	379	1377	40	1796
seq	d_u_div_s	0	20	128	epar	21.047	0	0.014	5.22	378	1402	16	1796
pgrank	du_div_s	0	10	512	epar	20.935	0	0.016	5.89	376	1403	17	1796
pgrank	du_div_s	0	20	512	epar	20.935	1	0.020	7.57	376	1376	44	1796
maxcut	default	0	1	512	epar	22.368	0	0.014	5.42	374	1292	6	1672
pgrank	u	0	10	128	epar	20.824	0	0.012	4.57	374	1415	7	1796
epcl	default	0	10	512	epar	20.768	0	0.014	5.16	373	1415	8	1796
pgrank	du	0	10	512	epar	20.713	0	0.014	5.09	372	1419	5	1796
seq	d_u_div_exps	0	20	512	epar	20.713	1	0.016	6.05	372	1407	17	1796
seq	d_u_div_s2	0	10	512	epar	20.713	0	0.013	4.94	372	1417	7	1796
maxcut	default	0	5	128	epar	20.601	0	0.013	4.91	370	1392	34	1796
seq	d2_div_s	0	60	128	epar	20.601	0	0.013	4.64	370	1361	65	1796
seq	d_u_div_s	0	10	512	epar	20.601	0	0.014	5.04	370	1420	6	1796
pgrank	u	0	10	512	epar	20.490	0	0.015	5.51	368	1421	7	1796
pgrank	u_div_s	0	20	512	epar	20.490	0	0.017	6.24	368	1331	97	1796
pgrank	d_div_s	0	20	128	epar	20.434	0	0.017	6.24	367	1310	119	1796
pgrank	du	0	20	128	epar	20.379	0	0.012	4.52	366	1420	10	1796
pgrank	du	0	20	512	epar	20.379	1	0.018	6.47	366	1423	7	1796
seq	d_u_div_s2	0	20	512	epar	20.323	0	0.013	4.85	365	1418	13	1796
pgrank	d	0	10	128	epar	20.267	0	0.014	5.07	364	1369	63	1796
seq	d2_div_s	0	60	512	epar	20.267	0	0.016	5.64	364	1378	54	1796
seq	d_u_div_s	0	20	512	epar	20.267	0	0.014	5.09	364	1419	13	1796
pgrank	d_div_s	0	10	128	epar	20.156	0	0.014	4.95	362	1363	71	1796
pgrank	u	0	20	128	epar	20.156	2	0.018	6.44	362	1417	17	1796
seq	d_u_div_s2	0	60	128	epar	20.156	0	0.014	5.04	362	1321	113	1796
epcl	default	0	20	512	epar	20.100	0	0.013	4.83	361	1424	11	1796
pgrank	u	0	20	512	epar	20.100	1	0.018	6.44	361	1423	12	1796
maxcut	default	0	10	128	epar	19.933	0	0.014	5.01	358	1391	47	1796
seq	d_u_div_s2	0	60	512	epar	19.878	0	0.013	4.78	357	1348	91	1796
pgrank	d	0	20	128	epar	19.822	0	0.013	4.62	356	1354	86	1796
epcl	default	0	60	128	epar	19.543	0	0.014	4.96	351	1409	36	1796
pgrank	u	0	60	128	epar	19.543	1	0.016	5.59	351	1400	45	1796
seq	u2_div_s	0	10	128	epar	19.543	0	0.012	4.34	351	1422	23	1796
pgrank	du_div_s	0	60	128	epar	19.488	0	0.017	5.96	350	1299	147	1796
seq	d_u_div_exps	0	60	128	epar	19.376	0	0.015	5.15	348	1290	158	1796
seq	u2_div_s	0	20	128	epar	19.376	1	0.016	5.64	348	1409	39	1796
pgrank	du	0	60	128	epar	19.154	0	0.014	4.82	344	1416	36	1796
pgrank	d	0	60	128	epar	18.931	0	0.012	4.16	340	1343	113	1796
pgrank	u_div_s	0	60	128	epar	18.820	0	0.016	5.48	338	1257	201	1796
seq	u2_div_s	0	60	128	epar	18.597	0	0.012	4.13	334	1374	88	1796
seq	d_u_div_s	0	60	512	epar	18.541	0	0.014	4.59	333	1388	75	1796
pgrank	d_div_s	0	60	128	epar	18.374	0	0.016	5.44	330	1236	230	1796
seq	d_u_div_exps	0	60	512	epar	18.374	0	0.014	4.67	330	1325	141	1796
pgrank	du_div_s	0	60	512	epar	18.263	0	0.015	5.04	328	1335	133	1796
seq	d_u_div_s	0	60	128	epar	18.207	0	0.014	4.51	327	1373	96	1796
pgrank	du	0	60	512	epar	18.151	0	0.013	4.12	326	1437	33	1796
epcl	default	0	60	512	epar	18.040	0	0.013	4.10	324	1444	28	1796
pgrank	d	0	10	512	epar	17.762	0	0.013	4.22	319	1427	50	1796
pgrank	u_div_s	0	60	512	epar	17.762	0	0.016	5.04	319	1298	179	1796
pgrank	d_div_s	0	10	512	epar	17.650	0	0.014	4.36	317	1416	63	1796
pgrank	d_div_s	0	20	512	epar	16.370	0	0.017	4.97	294	1393	109	1796
seq	u2_div_s	0	10	512	epar	15.813	0	0.013	3.76	284	1495	17	1796
pgrank	d	0	20	512	epar	15.646	0	0.011	3.23	281	1435	80	1796
pgrank	u	0	60	512	epar	15.312	0	0.013	3.49	275	1493	28	1796
seq	d2_div_s	0	10	32	z3_4	15.145	0	0.011	3.12	272	0	1524	1796
default	default	0	0	32	z3_4	15.089	0	0.011	3.09	271	0	1525	1796
seq	d2_div_s	0	20	32	z3_4	15.089	0	0.014	3.67	271	0	1525	1796
pgrank	u	0	60	32	z3_4	14.978	4	0.038	10.31	269	0	1527	1796
epcl	default	0	10	32	z3_4	14.922	0	0.012	3.31	268	0	1528	1796
pgrank	d	0	60	512	epar	14.811	0	0.011	2.90	266	1442	88	1796
seq	d2_div_s	0	60	32	z3_4	14.755	6	0.037	9.85	265	0	1531	1796
seq	u2_div_s	0	20	512	epar	14.755	0	0.010	2.77	265	1498	33	1796
epcl	default	0	20	32	z3_4	14.644	0	0.013	3.45	263	0	1533	1796
pgrank	u_div_s	0	10	32	z3_4	14.703	0	0.013	3.44	262	0	1520	1782
seq	d_u_div_exps	0	10	32	z3_4	14.588	0	0.012	3.17	262	0	1534	1796
pgrank	u	0	10	32	z3_4	14.477	0	0.013	3.42	260	0	1536	1796
seq	u2_div_s	0	60	512	epar	14.477	0	0.011	2.93	260	1467	69	1796
maxcut	default	0	1	32	z3_4	14.421	0	0.011	2.89	259	0	1537	1796
seq	d_u_div_s	0	60	32	z3_4	14.421	4	0.042	11.00	259	0	1537	1796
pgrank	u_div_s	0	20	32	z3_4	14.430	0	0.016	4.24	258	0	1530	1788
seq	d_u_div_s	0	20	32	z3_4	14.310	1	0.020	5.08	257	0	1539	1796
seq	d_u_div_s2	0	10	32	z3_4	14.310	0	0.011	2.94	257	0	1539	1796
epcl	default	0	60	32	z3_4	14.254	0	0.019	4.86	256	0	1540	1796
seq	d_u_div_s	0	10	32	z3_4	14.198	0	0.012	3.15	255	0	1541	1796
maxcut	default	0	10	32	z3_4	14.143	0	0.012	3.07	254	0	1542	1796
pgrank	du_div_s	0	20	32	z3_4	14.143	0	0.012	3.10	254	0	1542	1796
pgrank	du_div_s	0	10	32	z3_4	14.087	0	0.011	2.73	253	0	1543	1796
seq	d_u_div_exps	0	20	32	z3_4	14.087	0	0.012	3.03	253	0	1543	1796
maxcut	default	0	5	32	z3_4	13.983	0	0.012	2.92	251	0	1544	1795
pgrank	du	0	10	32	z3_4	13.976	0	0.011	2.79	251	0	1545	1796
pgrank	du	0	60	32	z3_4	13.976	1	0.021	5.31	251	0	1545	1796
seq	u2_div_s	0	60	32	z3_4	13.808	5	0.041	10.22	248	0	1548	1796
all	default	0	all	128	epar	13.753	0	0.018	4.40	247	1274	275	1796
pgrank	u_div_s	0	60	32	z3_4	13.641	2	0.033	8.01	245	0	1551	1796
seq	u2_div_s	0	20	32	z3_4	13.586	0	0.020	4.85	244	0	1552	1796
pgrank	du	0	20	32	z3_4	13.530	0	0.010	2.44	243	0	1553	1796
seq	d2_div_s	0	10	92	vam	13.474	0	0.009	2.26	242	1553	1	1796
seq	d_u_div_s2	0	60	32	z3_4	13.474	3	0.029	7.09	242	0	1554	1796
pgrank	d_div_s	0	60	512	epar	13.419	1	0.020	4.79	241	1364	191	1796
pgrank	u_div_s	0	10	92	vam	13.419	0	0.011	2.66	241	1505	50	1796
seq	d_u_div_exps	0	60	32	z3_4	13.419	0	0.020	4.83	241	0	1555	1796
pgrank	u	0	20	32	z3_4	14.060	0	0.025	5.99	240	0	1467	1707
seq	d2_div_s	0	20	92	vam	13.363	0	0.009	2.24	240	1556	0	1796
default	default	0	0	92	vam	13.556	0	0.009	2.19	239	1524	0	1763
maxcut	default	0	1	92	vam	13.307	0	0.009	2.20	239	1552	5	1796
seq	d_u_div_exps	0	10	92	vam	13.252	0	0.009	2.21	238	1550	8	1796
seq	u2_div_s	0	10	32	z3_4	13.500	0	0.020	4.86	238	0	1525	1763
pgrank	du	0	10	92	vam	13.196	0	0.009	2.06	237	1554	5	1796
pgrank	d_div_s	0	20	32	z3_4	13.124	1	0.020	4.67	234	0	1549	1783
pgrank	du_div_s	0	10	92	vam	13.029	0	0.009	2.09	234	1547	15	1796
seq	d_u_div_exps	0	20	92	vam	13.029	0	0.010	2.23	234	1546	16	1796
epcl	default	0	20	92	vam	13.053	0	0.009	2.14	233	1537	15	1785
pgrank	d	0	20	32	z3_4	13.053	3	0.031	7.21	233	0	1552	1785
pgrank	d_div_s	0	10	32	z3_4	12.973	0	0.015	3.57	233	0	1563	1796
all	default	0	all	32	z3_4	12.918	26	0.161	37.31	232	0	1564	1796
epcl	default	0	10	92	vam	12.918	0	0.009	2.04	232	1561	3	1796
seq	d_u_div_s	0	10	92	vam	13.053	0	0.009	2.12	230	1526	6	1762
seq	d_u_div_s2	0	10	92	vam	12.806	0	0.009	2.00	230	1559	7	1796
pgrank	du	0	20	92	vam	12.751	0	0.010	2.18	229	1552	15	1796
pgrank	du_div_s	0	60	32	z3_4	12.695	0	0.015	3.53	228	0	1568	1796
seq	d2_div_s	0	60	92	vam	12.695	0	0.010	2.28	228	1535	33	1796
pgrank	du_div_s	0	20	92	vam	12.639	0	0.009	2.04	227	1522	47	1796
seq	d_u_div_s	0	20	92	vam	12.584	0	0.009	2.01	226	1559	11	1796
seq	d_u_div_s2	0	20	92	vam	12.834	0	0.009	2.00	226	1525	10	1761
seq	d_u_div_s2	0	20	32	z3_4	14.423	0	0.014	3.09	225	0	1335	1560
pgrank	d	0	60	32	z3_4	12.472	1	0.021	4.65	224	0	1572	1796
pgrank	d	0	10	32	z3_4	12.556	0	0.011	2.46	223	0	1553	1776
pgrank	u	0	10	92	vam	12.416	0	0.009	2.12	223	1565	8	1796
pgrank	d	0	10	92	vam	12.361	0	0.010	2.17	222	1529	45	1796
pgrank	u_div_s	0	20	92	vam	12.249	0	0.010	2.30	220	1492	84	1796
pgrank	u	0	60	92	vam	12.138	0	0.011	2.43	218	1554	24	1796
maxcut	default	0	5	92	vam	12.082	0	0.009	2.00	217	1528	51	1796
pgrank	d_div_s	0	10	92	vam	12.082	0	0.010	2.08	217	1518	61	1796
seq	d_u_div_s2	0	60	92	vam	11.971	0	0.009	1.98	215	1502	79	1796
epcl	default	0	60	92	vam	11.915	0	0.009	1.84	214	1548	34	1796
seq	d_u_div_exps	0	60	92	vam	11.860	0	0.013	2.79	213	1452	131	1796
pgrank	d_div_s	0	60	32	z3_4	11.748	1	0.019	4.10	211	0	1585	1796
pgrank	u	0	20	92	vam	11.693	0	0.009	1.92	210	1580	6	1796
pgrank	d	0	20	92	vam	11.581	0	0.009	1.90	208	1523	65	1796
pgrank	d_div_s	0	20	92	vam	11.581	0	0.009	1.90	208	1484	104	1796
pgrank	du	0	60	92	vam	11.526	0	0.010	2.07	207	1566	23	1796
seq	u2_div_s	0	10	92	vam	11.470	0	0.009	1.77	206	1573	17	1796
maxcut	default	0	10	92	vam	11.440	0	0.009	1.79	205	1522	65	1792
seq	u2_div_s	0	60	92	vam	11.303	0	0.010	1.94	203	1546	47	1796
pgrank	u_div_s	0	60	92	vam	11.192	0	0.011	2.28	201	1452	143	1796
seq	u2_div_s	0	20	92	vam	11.136	0	0.009	1.67	195	1532	24	1751
pgrank	du_div_s	0	60	92	vam	10.690	0	0.010	1.89	192	1482	122	1796
pgrank	d	0	60	92	vam	10.626	0	0.010	1.81	190	1502	96	1788
seq	d_u_div_s	0	60	92	vam	10.579	0	0.009	1.63	190	1522	84	1796
pgrank	d_div_s	0	60	92	vam	10.329	0	0.013	2.38	185	1429	177	1791
all	default	0	all	92	vam	9.020	0	0.016	2.52	162	1434	200	1796
all	default	0	all	512	epar	8.519	0	0.011	1.73	153	1489	154	1796
any						40.813				733			1796

Greedy sequence

Prover	Sum%	Sum	G+2	G1+2	G-1+2	G+2M	Alt
default-default-0-0-512-epar	22.439	403
all-default-0-all-32-z3_4	27.004	485
pgrank-du_div_s-0-20-128-epar	30.290	544
seq-d_u_div_s-0-60-32-z3_4	32.183	578
seq-d2_div_s-0-10-128-epar	33.296	598
seq-u2_div_s-0-60-32-z3_4	34.131	613
pgrank-du_div_s-0-20-512-epar	34.800	625
pgrank-u_div_s-0-60-32-z3_4	35.412	636
pgrank-u_div_s-0-60-512-epar	35.857	644					= pgrank-d_div_s-0-60-512-epar
pgrank-d-0-20-32-z3_4	36.247	651					= epcl-default-0-60-32-z3_4
seq-d2_div_s-0-60-32-z3_4	36.581	657					= pgrank-d-0-10-92-vam = seq-d_u_div_exps-0-60-92-vam = seq-d_u_div_exps-0-20-128-epar = ... (9)
pgrank-d-0-10-92-vam	36.915	663					= seq-d_u_div_exps-0-60-92-vam = seq-d_u_div_exps-0-20-128-epar = pgrank-d_div_s-0-60-512-epar = ... (8)
pgrank-d_div_s-0-60-512-epar	37.249	669					= epcl-default-0-60-32-z3_4 = seq-d_u_div_s-0-20-32-z3_4
epcl-default-0-60-32-z3_4	37.584	675					= seq-d_u_div_s-0-20-32-z3_4
pgrank-u-0-60-32-z3_4	37.862	680
pgrank-u-0-60-128-epar	38.085	684					= pgrank-d-0-10-128-epar = seq-d_u_div_s-0-20-128-epar = seq-d_u_div_exps-0-20-128-epar = ... (6)
pgrank-d-0-10-128-epar	38.307	688					= pgrank-du_div_s-0-60-128-epar
pgrank-d_div_s-0-20-32-z3_4	38.474	691					= pgrank-u_div_s-0-20-128-epar = seq-d2_div_s-0-20-32-z3_4 = pgrank-du-0-60-32-z3_4 = ... (5)
pgrank-u_div_s-0-20-128-epar	38.641	694					= seq-d2_div_s-0-20-32-z3_4 = seq-d_u_div_s2-0-60-32-z3_4 = seq-d_u_div_s-0-20-32-z3_4
seq-d2_div_s-0-20-32-z3_4	38.808	697					= seq-d_u_div_s2-0-60-32-z3_4 = seq-d_u_div_s-0-20-32-z3_4
seq-d_u_div_s2-0-60-32-z3_4	38.976	700
pgrank-du-0-60-128-epar	39.087	702					= pgrank-du-0-60-92-vam = seq-u2_div_s-0-20-128-epar = pgrank-u-0-20-512-epar = ... (18)
seq-u2_div_s-0-20-128-epar	39.198	704					= pgrank-u-0-20-512-epar = seq-d_u_div_exps-0-20-128-epar = epcl-default-0-20-32-z3_4 = ... (14)
pgrank-u-0-20-512-epar	39.310	706					= seq-d_u_div_exps-0-20-128-epar = epcl-default-0-20-32-z3_4 = all-default-0-all-92-vam = ... (13)
seq-d_u_div_exps-0-20-128-epar	39.421	708					= epcl-default-0-20-32-z3_4 = all-default-0-all-92-vam = pgrank-du_div_s-0-60-32-z3_4 = ... (12)
epcl-default-0-20-32-z3_4	39.532	710					= all-default-0-all-92-vam = pgrank-du_div_s-0-60-32-z3_4 = all-default-0-all-128-epar = ... (8)
all-default-0-all-92-vam	39.644	712					= pgrank-du_div_s-0-60-32-z3_4 = all-default-0-all-128-epar = seq-d_u_div_exps-0-60-32-z3_4 = ... (7)
pgrank-du_div_s-0-60-32-z3_4	39.755	714					= seq-d_u_div_exps-0-60-32-z3_4 = pgrank-du-0-20-512-epar = pgrank-du_div_s-0-60-128-epar = ... (5)
pgrank-du-0-20-512-epar	39.866	716					= pgrank-d_div_s-0-20-128-epar = pgrank-u-0-20-128-epar
pgrank-d_div_s-0-20-128-epar	39.978	718					= pgrank-u-0-20-128-epar
pgrank-u-0-20-128-epar	40.089	720
pgrank-d_div_s-0-60-32-z3_4	40.145	721					= pgrank-u_div_s-0-10-512-epar = seq-d_u_div_exps-0-20-32-z3_4 = seq-d_u_div_s-0-20-128-epar = ... (21)
pgrank-u_div_s-0-10-512-epar	40.200	722					= seq-d_u_div_exps-0-20-32-z3_4 = seq-d_u_div_s-0-20-128-epar = seq-u2_div_s-0-10-32-z3_4 = ... (20)
seq-d_u_div_exps-0-20-32-z3_4	40.256	723					= seq-d_u_div_s-0-20-128-epar = seq-u2_div_s-0-10-32-z3_4 = seq-d_u_div_s-0-10-128-epar = ... (19)
seq-d_u_div_s-0-20-128-epar	40.312	724					= seq-u2_div_s-0-10-32-z3_4 = seq-d_u_div_s-0-10-128-epar = pgrank-du_div_s-0-10-128-epar = ... (17)
seq-u2_div_s-0-10-32-z3_4	40.367	725					= seq-d_u_div_s-0-10-128-epar = pgrank-du_div_s-0-10-128-epar = seq-d_u_div_exps-0-20-512-epar = ... (15)
seq-d_u_div_s-0-10-128-epar	40.423	726					= pgrank-du_div_s-0-10-128-epar = seq-d_u_div_exps-0-20-512-epar = pgrank-d-0-60-32-z3_4 = ... (13)
seq-d_u_div_exps-0-20-512-epar	40.479	727					= pgrank-d-0-60-32-z3_4 = seq-d_u_div_s2-0-60-128-epar = pgrank-du_div_s-0-60-128-epar = ... (11)
pgrank-d-0-60-32-z3_4	40.535	728					= seq-d_u_div_s2-0-60-128-epar = pgrank-du_div_s-0-60-128-epar = seq-d_u_div_s2-0-10-32-z3_4 = ... (10)
seq-d_u_div_s2-0-60-128-epar	40.590	729					= pgrank-du_div_s-0-60-128-epar = seq-d_u_div_s2-0-10-32-z3_4 = pgrank-du-0-60-32-z3_4 = ... (9)
pgrank-du-0-60-32-z3_4	40.646	730					= pgrank-u-0-20-32-z3_4 = seq-d_u_div_s-0-20-32-z3_4 = maxcut-default-0-10-512-epar = ... (4)
pgrank-u-0-20-32-z3_4	40.702	731					= seq-d_u_div_s-0-20-32-z3_4 = maxcut-default-0-10-512-epar = pgrank-u-0-10-32-z3_4
seq-d_u_div_s-0-20-32-z3_4	40.757	732					= maxcut-default-0-10-512-epar
maxcut-default-0-10-512-epar	40.813	733