Metis Performance Benchmarks

performance

Metis Performance Benchmarks

CASC 23 (2011)

Metis 2.3 was entered in the competition with this System Description.

FOF	Attempted	Solved	Av. Time	Solutions
Vampire 0.6	300	269	12.95	269
Vampire 1.8	300	263	13.62	263
E-MaLeS 1.0	300	233	18.85	233
EP 1.4pre	300	232	22.55	232
iProver 0.9	300	192	9.22	0
leanCoP 2.2	300	136	46.80	136
iProver-Eq 0.7	300	135	8.68	0
E-KRHyper 1.2	300	109	8.93	0
E-Darwin 1.4	300	103	6.97	0
Metis 2.3	300	101	24.75	101
LEO-II 1.2.8	300	97	25.18	94
Otter 3.3	300	62	5.84	62
Muscadet 4.1	300	42	8.99	40

In the FOF division the time limit was 300 seconds, and Metis 2.3 solved 101 out of 300 problems with an average time of 24.75 seconds.

The competition website includes the division results, individual problem results and performance graphs.

CASC J5 (2010)

Metis 2.2 was entered in the competition with this System Description.

FOF	Attempted	Solved	Av. Time	Solutions
Vampire 0.6	200	178	14.16	178
E 1.2pre	200	143	10.20	0
EP 1.2pre	200	143	14.77	143
Vampire 11.0	200	125	44.92	125
iProver 0.8	200	117	25.55	0
Equinox 5.0	200	108	17.40	0
iProver-E 0.6	200	90	18.09	0
E-Darwin 1.3	200	81	25.29	0
leanCoP 2.2	200	54	42.61	54
Zenon 0.6.3	200	46	36.03	45
LEO-II 1.2	200	45	45.01	45
Geo 2010C	200	42	22.74	42
Metis 2.2	200	36	32.68	36
E-KRHyp 1.1.4	200	32	24.27	0
Otter 3.3	200	18	9.30	18
Muscadet 4.0	200	15	3.89	15
Ayane 2	200	0	-	0

In the FOF division the time limit was 240 seconds, and Metis 2.2 solved 36 out of 200 problems with an average time of 32.68 seconds.

The competition website includes the division results, individual problem results and performance graphs.

CASC 22 (2009)

Metis 2.2 was entered in the competition with this System Description.

FOF	Attempted	Solved	Av. Time	Solutions
Vampire 11.0	300	233	33.00	233
E 1.1pre	300	219	23.89	0
Vampire 10.0	300	219	35.06	219
EP 1.1pre	300	218	26.83	217
iProver 0.7	300	174	24.79	0
Equinox 4.1	300	119	24.08	0
leanCoP	300	113	37.02	113
iProver-Eq 0.5	300	88	26.58	0
Metis 2.2	300	84	24.73	84
E-KRHyper 1.1.3	300	81	21.96	0
Otter 3.3	300	58	12.90	58
OSHL-S 0.6	300	40	33.83	0
Infinox 1.0	300	0	-	0

In the FOF division the time limit was 300 seconds, and Metis 2.2 solved 84 out of 300 problems with an average time of 24.73 seconds.

The competition website includes the division results, individual problem results and performance graphs.

CASC J4 (2008)

Metis 2.1 was entered in the competition with this System Description.

FOF	Attempted	Solved	Av. Time	Solutions
Vampire 10.0	200	169	27.81	169
E 1.0pre	200	164	15.52	0
EP 1.0pre	200	164	20.97	161
Vampire 9.0	200	163	25.67	163
iProver 0.5c	200	139	10.29	0
randoCoP 1.1	200	95	21.51	95
Equinox 3.0	200	86	20.16	0
Metis 2.1	200	84	16.19	84
Otter 3.3	200	76	17.92	76
E-KRHyper 1.1	200	60	16.31	0
Zenon 0.5.0	200	51	4.33	51
Muscadet 3.0	200	38	8.77	31
OSHL-S 0.1	200	27	4.97	0

In the FOF division the time limit was 300 seconds, and Metis 2.1 solved 84 out of 200 problems with an average time of 16.19 seconds.

The competition website includes the division results, individual problem results and performance graphs.

CASC 21 (2007)

Metis 2.0 was entered in the competition with this System Description.

FOF	Attempted	Solved	Av. Time	Solutions
Vampire 9.0	300	270	20.84	270
Vampire 8.1	300	266	16.37	266
Fampire 1.3	300	262	12.19	0
E 0.999	300	248	13.36	0
EP 0.999	300	225	13.10	221
iProver 0.2	300	201	9.57	0
Equinox 1.2	300	173	14.92	0
leanCoP 2.0	300	160	39.50	0
Otter 3.3	300	138	25.04	138
Metis 2.0	300	117	16.06	89
Geo 2007f	300	104	29.42	104
ileanCoP 1.2	300	103	44.23	0
Muscadet 2.7	300	37	0.76	0

In the FOF division the time limit was 360 seconds, and Metis 2.0 solved 117 out of 300 problems with an average time of 16.06 seconds. The number of solutions is only 89 because the other 28 problems were solved by the FOF → CNF normalization.

The competition website includes the division results, individual problem results and performance graphs.

Here is the paragraph on Metis 2.0 contributed to the CASC 21 report.

CASC 19 (2003)

Metis 1.5 was not entered in the official competition, but was run afterwards on the problems used in the competition.

MIX	Attempted	Solved	Av. Time	Solutions
Vampire 6.0	140	120	65.64	120
E-SETHEO csp03	140	119	34.65	0
E 0.8	140	113	20.91	0
Vampire 5.0	140	113	23.08	113
EP 0.8	140	113	25.35	110
Gandalf c-2.6	140	102	67.75	0
Gandalf c-2.6-PRF	140	79	30.94	79
DCTP 10.2p	140	72	43.28	0
Metis 1.5	140	71	81.07	71
DCTP 1.3	140	55	18.15	0
THEO J2003	140	49	45.59	47
Otter 3.2	140	34	99.12	34
CARINE 0.72	140	7	104.86	7

In the MIX division the time limit was 600 seconds, and Metis 1.5 solved 71 out of 140 problems with an average time of 81.07 seconds.

In the UEQ division the time limit was 600 seconds, and Metis 1.5 solved 21 out of 70 problems with an average time of 68.68 seconds.

In the FOF division the time limit was 600 seconds, and Metis 1.5 solved 32 out of 70 problems with an average time of 49.87 seconds.

Metis is running on a RedHat 7.1 GNU/Linux box with a Pentium III 600Mhz processor and 512Mb of main memory; the other provers are running on Dell Precision 330 workstations (GNU/Linux boxes with Pentium III 1Ghz processors and 512Mb of main memory).

CASC 18 (2002)

Metis 1.5 was not entered in the official competition, but was run afterwards on the problems used in the competition.

MIX	Attempted	Solved	Av. Time	Solutions
Vampire 5.0	175	158	25.25	158
Vampire 5.0-CASC	175	157	27.28	157
Vampire 2.0-CASC	175	152	57.33	152
E-SETHEO csp02	175	145	57.60	0
E 0.7	175	131	21.35	0
EP 0.7	175	129	25.58	129
Gandalf c-2.5	175	129	82.92	0
Gandalf c-2.5-PROOF	175	125	77.47	125
Metis 1.5	175	97	77.42	97
Bliksem 1.12a	175	88	43.99	88
DCTP 10.1p	175	76	41.18	0
SCOTT 6.1	175	63	74.48	63
Otter 3.2	175	60	56.34	60
DCTP 1.2	175	56	45.03	0

In the MIX division the time limit was 600 seconds, and Metis 1.5 solved 97 out of 175 problems with an average time of 77.42 seconds.

In the UEQ division the time limit was 300 seconds, and Metis 1.5 solved 7 out of 70 problems with an average time of 50.45 seconds.

In the FOF division the time limit was 300 seconds, and Metis 1.5 solved 35 out of 70 problems with an average time of 32.09 seconds.