Results of the CM Prover on the CASC-25 FEQ Problems

Problem Vampire 2 Vampire 4 E ET CVC4 iProver Prover9 ePrincess leanCoP CM-ALL CM-E1 CM-E2 CM-E3 CM-E4 iProverM Geo-III Muscadet
GRP194+1 0.01 0.01 0.01 0.01 0.01 73.41 0.01 2.11 186.73 57.96 57.96 0.01 0.01
REL009+2 209.71 14.21 1.95 0.01 1.54 0.01 4.03
GRP777+1 39.29 4.42 0.01 147.24 0.02
NUM925+5 0.01 1.61 0.01 0.10 0.01 59.58 0.14 8.52 0.01 9.49 13.06 9.49
SET027+1 0.01 0.02 0.01 0.01 0.01 0.02 0.02 15.65 0.66 0.44 0.74 0.44 0.54 0.44 0.01 0.02
NUM341+1 0.01 0.01 0.01 0.02 15.52 0.01 0.01 0.03 0.26 0.47 0.26 0.26 0.45 0.02
SWV157+1 0.01 0.01 0.04 0.02 0.03 0.01 6.01 9.16 8.42 11.17 11.17 220.58
SET008+3 0.01 0.01 0.01 0.01 0.01 0.01 0.01 19.38 0.01 0.03 0.04 0.03 0.03 0.04 0.01 31.58 0.01
GEO112+1 0.01 0.01 0.01 0.03 0.01 0.01 0.01 2.85 0.09 0.13 0.36 0.34 1.23 0.13
PUZ001+2 0.01 0.01 0.01 0.01 0.01 0.01 0.01 11.98 91.82 143.02 143.02 0.01
SWB013+2 1.21 11.83 0.01 0.01 0.01 37.55 131.55 4.29 173.62 0.01
KLE004+1 0.01 0.01 0.01 0.01 15.05 4.52 0.01 0.01 0.06 17.45 7.04 5.33 0.06 0.01
REL023+1 0.01 0.01 0.01 6.08 286.56 0.01
GEO146+1 0.01 0.01 0.01 0.01 0.01 0.01 2.88 21.72 0.02 0.14 0.20 0.17 0.14 0.20 0.02
NUM925+6 0.01 0.01 0.01 1.43 0.01 12.74 54.36 0.38 2.06 39.38 85.27 7.13 2.06 243.84
MGT054+1 0.01 0.01 0.01 1.09 0.03 0.01 0.01 21.11 0.01
SWV167+1 0.01 0.01 0.01 0.01 0.01 86.12 24.82 30.88
LCL454+1 0.01 0.01 0.02 13.54 0.01 0.01 21.98 0.01 0.03 0.03 0.03 0.03 0.03 0.02
HWV051+1 11.96 227.88 143.30 53.50
HWV051+2 11.96 228.37 148.76 68.77
GEO148+1 0.01 0.01 0.01 0.02 0.01 0.01 0.01 17.06 27.78 0.15 0.20 0.19 0.15 0.20 0.01
HWV041+1 12.74 228.61 144.30 68.56
AGT003+2 0.01 0.01 0.02 0.01 0.01 0.13 3.04 227.87 0.01 0.89 0.92 0.90 0.89 0.89 0.02 85.05
HWV047+2 14.69 232.39 145.71 136.79
LCL536+1 0.01 0.01 0.01 15.35 10.04 0.01 5.11 0.15 0.08 0.10 0.08 0.08 0.10 1.60
HWV047+1 15.01 231.53 145.44 93.54
HWV050+2 12.47 228.92 144.18 71.24
HWV043+1 13.48 230.44 154.89 83.28
NUM924+1 1.42 0.01 0.01 0.01 0.01 0.02 6.32
SWV409+1 0.01 0.03 0.01 0.01 0.01 0.01 0.01 7.80 0.10 0.02
HWV089+1 0.01 0.01 6.64 4.54 86.61 5.89 5.03
MGT065+1 0.01 0.01 0.03 0.07 0.01 0.54 0.01 29.77 182.29
NUM924+2 1.62 5.15 0.01 0.01 0.34 3.24 18.95 110.37 1.45 1.99 1.64 1.51 1.45
SWB006+1 1.40 0.01 0.01 0.02 0.01 13.25 3.93 4.12 4.97 3.93
LAT356+1 0.01 0.01 0.01 0.01 15.47 1.84 68.98
GEO084+1 0.01 0.03 0.01 58.25 0.01 0.05 0.02 12.27 0.26 1.18 1.35 1.18 23.13
GEO118+1 0.01 1.92 0.01 6.09 30.91 0.01 0.03 3.54 0.12 0.13 0.17 0.16 0.13 0.17 0.06 207.84 0.02
NUM853+2 0.01 0.01 0.01 0.01 1.15 19.56 0.01 0.03 0.04 0.03 0.03 0.05
NUM925+3 0.01 0.01 0.01 8.00 0.01 14.52 159.78 9.84 29.61 85.13 9.84
ALG041+1 0.02 0.01 0.01 0.01 0.01 0.01 2.38 0.01
LCL538+1 0.01 0.01 0.01 59.74 0.02 2.40 11.89 229.37 0.63 22.54 0.63 2.79
SWW473+5 0.01 1.62 0.03 5.20 0.01 21.34 44.84 130.15 0.01 0.19 0.26 0.20 0.19 0.27 13.19
ALG210+2 0.01 0.01 0.01 0.01 0.01 0.01 11.45 0.02
NUM924+3 5.18 4.54 0.02 7.85 0.01 10.00
SWV463+1 0.02 0.01 5.01 0.01 0.01 5.60 0.14 14.86 33.30 90.87 90.87 57.67
SEU192+1 0.02 2.81 0.01 12.07 0.01 23.59 2.84 0.01
SWV203+1 0.01 0.01 14.73 0.01 1.05 0.01 34.38 21.98
SET889+1 0.01 2.71 0.01 0.01 0.01 6.73 45.06 0.01 0.10 0.77 0.10 10.63 0.25 0.01 0.01
SWV486+1 2.62 3.60 0.01 0.01 0.02 35.15 39.73 0.92
LCL499+1 0.01 0.01 0.01 1.63 10.65 0.01 17.78 0.04 0.12 0.04 0.06 0.04
NUM299+1 0.01 0.01 1.14 0.01 35.06 6.45 0.12 0.26 0.56 0.26 0.26 0.45 9.63
NUM534+2 0.01 3.81 0.01 5.07 0.01 7.54 200.28
TOP023+1 0.01 2.51 35.34 0.01 0.01 15.75 1.28 4.59 0.02
SCT131+1 2.93 0.01 0.01 5.68 0.01 4.93 1.68 1.75 1.97 4.70 1.75 1.82 166.64
GEO272+1 0.01 0.01 0.01 30.03 0.01 38.83 111.59 1.73 10.55
KLE079+1 1.30 3.90 0.01 0.01 15.78 0.01 71.91 181.60
SWV030+1 0.01 0.01 0.01 0.70 0.01 0.01 23.61 0.02 214.86
SWB049+1 1.42 0.01 0.01 0.01 14.15 220.90 68.13 8.15 11.50 8.15 10.92
SWV461+1 0.01 0.05 3.44 18.17 0.01 52.88 14.16 0.88 169.91
SWV450+1 0.01 0.01 0.01 6.51 0.01 0.01 78.08
SWW474+1 0.01 0.01 0.02 0.01 0.01 22.63 20.94 24.44 213.68 3.58
NUM329+1 0.01 0.01 0.02 15.54 103.93 19.40 0.01 0.26 0.78 0.26 0.28 0.47 0.02 55.83
SWV416+1 0.04 0.01 0.01 0.02 0.01 0.01 4.36 0.01 0.10 0.14 0.11 0.10 0.14 0.01
PRO003+4 0.02 2.51 0.02 0.01 0.02 4.10 23.86 0.01
SCT126+1 2.93 0.01 0.01 10.59 0.01 5.64 31.20 0.02 1.70 1.87 1.80 1.70 1.82
LCL526+1 1.32 12.08 0.01 61.95 4.52 22.75
LCL902+1 0.01 0.04 0.01 0.01 0.01 14.25 85.41 149.82 85.41 11.14
SWW473+2 0.01 0.01 0.02 6.61 0.01 147.40 37.64 1.44 2.71 2.89 14.57 2.71 8.30 26.38
SWW470+1 1.43 16.44 0.01 1.98 0.01 4.90 9.16
CSR024+1.009 0.01 0.06 0.01 0.01 0.01
PRO014+3 0.01 4.36 0.01 0.01 0.01 1.94 2.84 48.76 12.93
SWW186+1 0.02 6.16 0.02 6.77 0.01 33.87
GEO331+1 0.01 0.01 0.02 33.95 0.02 17.82
PUZ133+1 17.23 18.29 3.13 15.00 0.01 0.01 63.67
HAL002+1 1.21 2.25 0.01 0.01 0.01 7.69 0.01 0.01
ALG127+1 0.01 0.70 68.51 0.01 8.57
SET056+1 0.01 0.02 0.03 0.01 0.02 0.77 0.11 0.22 0.11 0.12 47.62 0.04
CSR008+1 3.84 7.66 0.03 30.52 19.81 0.02
SWC279+1 0.01 0.01 0.01 0.01 0.01 10.18 76.84
SWV453+1 0.14 0.85 48.85 25.38 0.23 79.10
SWV481+1 2.26 0.90 1.83 100.92 0.01 60.52
KLE170+1.002 6.11 2.83 0.01 0.01 0.01 0.01 41.35 192.10
NUM926+6 0.01 0.01 0.01 5.66 1.11 5.13 122.92
SET699+4 0.04 117.47 0.01 6.07 0.01 3.37 0.01 0.01 0.01
SWV456+1 0.01 2.51 10.24 36.49 15.11 16.31 83.94
GRA007+2 11.86 8.15 0.02 6.05 0.02 3.65 1.03
SET703+4 0.01 0.02 10.12 0.01 3.90 8.98 0.78 2.92 0.78 4.59 0.02 0.02
GEO088+1 5.89 44.91 84.52 12.11 0.02 35.45 92.11 39.29
SWV374+1 0.01 0.01 0.01 0.01 0.01 8.06
SWB040+1 1.05 0.04 100.83 0.02 218.64 1.42 214.41
LCL894+1 34.20 43.88 0.01 108.10 15.36 63.78
NUM926+3 2.95 23.18 151.76 63.09 0.01 57.80 21.70
SEU210+1 6.77 3.53 0.01 7.33 0.01 252.66 252.66 185.99
GEO127+1 0.01 2.51 0.01 6.06 0.01
ALG128+1 0.01 0.01 8.94 0.01 9.90
SWV468+1 0.01 0.01 151.89 18.69 0.01 39.12 104.35 71.16
SWV109+1 0.01 0.01 18.06 0.01 0.01 29.61 0.14
SCT164+1 2.91 3.63 0.01 0.99 64.70 4.65 148.74
HAL001+2 100.57 63.36 7.05 2.56 64.93 89.21 1.05
SWW314+1 0.02 0.01 4.22 7.90 2.24 3.34 2.65 10.85 15.58 11.07 10.85 15.29
CSR048+4 4.45 1.06 4.24 6.57 10.73 6.01 105.57 140.39
SWW302+1 0.01 0.01 3.72 0.01 11.64 1.60 29.61 10.66 15.42 10.88 10.66 15.04
GRA009+1 122.74 6.72 3.92 18.69 58.19 0.01
KLE044+1 59.24 3.44 0.02 1.28 1.14 10.61 54.29
SWV491+3 0.01 0.01 3.43 43.23 0.01 22.71 110.23 0.01
GEO169+2 3.42 33.05 19.15 54.54 15.09 8.33
SWW315+1 0.01 0.01 3.63 7.81 2.26 3.32 2.67 10.83 15.63 11.05 10.83 15.28
SWW313+1 0.01 0.22 3.56 7.77 11.00 3.59 30.76 10.94 16.00 13.14 10.94 15.56
SWW470+3 32.17 2.35 151.17 14.12 0.02 36.87
SWC061+1 1.41 0.01 0.02 6.10 288.33
NUM860+1 0.01 0.02 2.33 142.23 6.95
SCT149+1 0.04 0.01 15.69 0.01 0.01 107.07 0.02 0.03
GEO282+1 2.35 1.62 0.01 0.01 50.91 16.30
SWB024+1 3.72 0.01 3.92 0.01 240.31 28.35
SWW312+1 0.02 1.22 9.72 7.79 2.44 2.72 10.55 15.16 10.79 10.55 14.83
SCT167+1 2.33 3.62 0.02 2.93 58.68 5.57
SWB084+1 3.37 1.81 24.33 0.37 40.94 217.86 54.24 54.24 56.24
NUM516+3 145.35 130.79 225.83 65.29 69.71 30.18 29.37 1.26 1.26
SWV462+1 0.01 0.01 168.13 11.95 0.01 1.82 247.92
SCT166+1 2.93 3.61 0.02 1.19 51.27 4.95
SWV233+1 1.65 0.02 0.01 6.08
SWB086+1 3.31 2.85 162.12 0.02 111.12
SWW386+1 0.01 1.25 4.34 9.14 87.34 4.51 273.47 31.46 10.61 15.25 12.93 10.61 17.92
CSR005+1 3.82 7.79 0.01 28.86 19.84
GEO283+1 4.53 9.87 0.02 45.07 16.46 123.28
SWW344+1 0.01 0.01 2.83 9.25 3.20 30.44 10.37 14.89 10.58 10.37 14.53
SWW353+1 0.02 0.01 11.44 10.93 87.56 275.26 32.45 10.65 15.21 10.90 10.65 15.33
SWW298+1 0.01 0.01 3.82 6.99 121.50 11.81 72.19 14.94 56.24 15.15 14.94
SWB029+1 3.73 1.83 3.83 0.01 117.96
NUM862+1 0.02 0.01 151.15 150.44 45.17 157.29
SWB106+1 3.34 2.84 165.03 0.01
GEO306+1 7.24 3.71 0.01 45.05 58.29
NUM320+1 0.01 0.01 1.51 12.21 1.51 15.71 1.94
SWW387+1 0.01 0.01 3.54 9.13 87.26 4.40 31.35 10.64 15.10 12.94 10.64 17.56
CSR025+5 9.14 9.97 10.83 32.71 30.49
SET010+3 2.03 46.03 35.74 0.95 7.25 0.01 0.01
SWW474+6 0.02 18.02 56.34
SEU352+1 11.25 39.21 0.01 8.00
SWB032+1 2.21 0.02 8.94 0.01 36.89
LCL523+1 1.91 0.02 63.54
SWW318+1 0.02 1.44 6.14 10.50 31.54 10.48 15.17 10.67 10.48 14.78
SCT121+1 0.01 2.93 12.50 277.64 15.50
SWW362+1 0.18 1.33 15.04 22.34 14.43 38.39 162.73 162.73
NUM925+8 18.81 3.37 9.53 124.65 3.64 10.97 27.89 27.89
GRP654+1
CSR070+4 4.44 7.44 21.62 6.50 6.48 201.22
CSR026+4 10.23 0.60 13.49 14.70 12.71 7.21 139.77
SWB080+1 3.34 2.84 160.47 0.02
SCT117+1 0.02 2.83 14.18 0.01 51.80
GEO308+1 4.25 2.91 270.05 99.40 173.81
SWW321+1 0.02 1.31 11.54 20.88 80.50 14.10 36.04 14.10
SCT162+1 2.16 26.84 5.73 1.18 4.24
SCT163+1 2.82 28.14 6.65 1.01 4.29
AGT018+2 0.01 1.33 27.40 163.38 174.52
SWB063+1 3.73 6.17 167.69 0.02 114.70
NUM331+1 27.67 4.48 243.47 199.80 130.01 391.42 130.01
SWW358+1 0.02 1.34 7.93 8.63 12.05 76.10
GRP780+1 142.85 56.22 0.01 147.29 1.09
SWB071+1 3.34 0.03 3.61 0.01 15.84 15.84
SCT143+1 4.53 31.78 151.17 1.99 5.25
SCT141+1 4.45 31.96 151.13 21.36 4.47
SWW226+1 5.69 31.15 193.74 252.19
SCT153+1 17.75 55.25 15.48 1.15
SWW326+1 0.02 0.01 12.33 7.87 2.45
SCT135+1 0.01 0.01 10.38 0.01
GRA002+1 8.75 6.12 13.35 44.27 56.09 0.01
GRP779+1 6.96 1.24 35.34 7.00
SCT138+1 4.44 31.29 224.57 1.11 4.55
SWW368+1 3.24 1.43 12.71 22.13 14.73 38.49 160.47 160.47
SCT136+1 4.53 31.90 151.16 1.80 5.07
SWW337+1 0.01 0.01 8.94 7.12 11.64 208.44 30.92
SEU211+2 18.79 0.02 0.02 89.37
SCT128+1 24.04 0.41 13.28 0.01 72.65
SWW371+1 53.41 0.01 9.62 243.22 279.00
SWW310+1 0.01 1.24 10.48 38.07 282.96
SWB093+1 3.38 2.87 0.01
SWB064+1 3.75 7.68 185.43 0.36
GEO287+1 0.01 52.95 2.52 7.33
SCT139+1 4.56 32.48 152.18 2.21 4.75
SWB050+1 3.75 24.44 5.52 0.01
CSR038+4 17.51 1.60 162.30 6.61
SYN076+1 11.77 17.85 2.64 0.01
SWB082+1 3.35 2.85 0.99
SWV037+1 0.01 3.73 25.21 0.05
SWW382+1 0.01 0.01 12.04 9.01 118.01
SWW359+1 0.02 1.34 10.38
SWW470+7 0.05 3.55 12.68
LAT286+2 0.01 3.04 11.33 21.68
NUM926+4 3.35 3.99 4.74
SWW396+1 62.57 0.01 11.41
CSR055+5 9.44 191.15 11.43 32.36
SWB013+1 3.37 1.83 35.65
SWW339+1 0.01 1.62 10.03 7.81 11.85
CSR059+5 11.83 10.93 12.22 32.37
SWW356+1 62.45 1.23 10.43 35.98
SWV234+1 0.02 10.06 254.89
LAT287+2 0.01 3.05 0.01 29.40
SWW340+1 63.44 1.23 9.63 264.74
LCL551+1 22.01 1.63
LCL555+1 21.00 292.22 2.04
SWW305+1 63.66 1.32 18.51 118.33
SWW470+6 0.01 53.25 14.44 4.69
SET069+1 0.01 27.54 39.74 151.09 0.01
SWW366+1 21.94 1.44 10.82
SWW389+1 0.02 0.01 10.53 22.25
SWW335+1 51.32 1.29 6.31
SWW306+1 0.17 1.23 8.93 19.44
SWB105+1 3.62 7.14 3.40
SWW348+1 0.02 1.13 7.23 6.86
SWB010+1 3.34 2.34 0.40
SWW384+1 46.35 0.22 12.84 272.88
SWB095+1 3.37 2.84 0.01
SWW320+1 63.53 1.33 11.35 40.92
SWW350+1 0.02 1.15 5.24 6.82
SWW325+1 62.82 0.01 10.93 293.79
SEU214+2 13.18 49.65
CSR039+4 10.21 107.45
CSR064+6 95.94 97.00 94.53 110.68 200.90
GEO279+1 26.00 45.57 10.44
LCL890+1 41.44 189.69
SWW327+1 62.71 0.01 16.45
SWW100+1 3.43 1.74 31.98
CSR048+6 83.61
LAT297+3 4.54 3.37 0.02 26.90
SWW329+1 63.08 1.13 11.34
SWB069+1 54.25 1.83 10.36 116.08
SWW346+1 58.66 0.01 11.34
SEU063+1 1.23 6.03 30.16
LCL892+1 41.41
HWV107+1 8.44 64.65
SCT102+1 54.76 20.89
GEO293+1 30.67 76.86
GEO322+1 30.84 90.45
SWB101+1 3.75 2.89
GEO316+1 83.05
LAT348+3 0.49 3.55 9.33
KLE042+1 53.91 110.55
SCT170+2 57.68 112.96
GEO309+1 100.32
LAT359+3 159.54
GEO337+1 5.08 0.02 55.80
SWB038+1 3.73 23.22 2.21
GRP628+4 161.54 4.84 59.74
SCT148+1 18.82 56.70
GEO334+1 71.66
CSR058+6 98.63 97.01 205.95
GEO338+1 66.12
GEO329+1
GEO312+1 21.88 144.85
LAT377+3 52.27 201.60
Solved 241 227 194 184 146 97 82 78 74 57 48 45 44 42 36 22 19
Vampire 2 Vampire 4 E ET CVC4 iProver Prover9 ePrincess leanCoP CM-ALL CM-E1 CM-E2 CM-E3 CM-E4 iProverM Geo-III Muscadet