changelog download home install notes 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.

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).


Metis the moon of Jupiter