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

Problem Vampire 4 Vampire 2 iProver E ET CVC4 CM-ALL CM-n1 CM-n2 CM-n3 CM-n4 iProverM CM-n5 leanCoP CM-n6 CM-n7 CM-n8 ePrincess Prover9 Muscadet Geo-III
SWB009+3 3.73 2.12 10.34 0.05 0.01 45.43 0.53 0.57 0.61 0.53 0.61 150.85 0.77 0.01 0.76 0.75 1.08 31.82 10.44 10.40
CSR032+3 0.01 0.01 1.15 0.01 5.21 3.14 21.83 22.49 22.45 21.83 22.41 3.38 24.24 2.01 24.13 24.48 23.99
SYN386+1 0.01 0.01 0.01 0.01 0.01 0.01 0.01 0.01 0.01 0.01 0.01 0.01 0.08 0.01 0.01 0.01 0.01 0.01
KRS263+1 0.01 0.01 0.01 9.74 0.01 30.66 0.09 0.09 0.11 0.15 0.11 0.01 0.14 0.01 0.14 0.13 0.15 0.88
CSR047+3 0.02 0.02 0.04 0.01 4.21 0.03 21.91 22.96 22.43 21.91 22.52 1.22 24.35 1.39 24.21 24.29 24.06 41.57
CSR029+3 0.02 1.44 1.13 6.23 4.37 3.53 22.02 23.63 22.71 22.02 22.56 13.47 2.90
CSR037+3 0.01 1.73 1.06 1.72 4.13 0.01 21.82 22.56 22.37 21.82 22.52 1.23 24.24 29.45 24.11 24.38 24.26 261.44
KRS234+1 0.01 0.01 0.01 0.01 0.01 15.03 0.12 0.12 0.13 0.13 0.12 0.01 2.18 28.05 2.22 0.18 0.95 0.01
CSR115+36 0.01 0.01 1.64 0.01 0.01 1.01 3.21 3.34 3.33 3.21 3.33 42.99 47.83 0.01 47.74 48.68 48.31 27.50
CSR115+34 0.03 1.04 10.77 0.01 7.70 4.61 3.24 3.44 3.38 3.24 3.39 20.15 48.08 48.23 49.20 53.68
KRS261+1 0.01 0.01 0.01 39.41 0.01 30.07 0.18 3.88 6.24 179.89 0.01 0.18 20.06 0.18 2.44
KRS259+1 0.01 0.14 0.02 0.01 0.01 30.07 0.08 0.09 0.10 0.08 0.10 0.01 0.14 0.24 0.14 0.14 0.14 0.01
KRS194+1 0.01 1.73 0.01 0.01 0.01 0.01 0.08 0.09 0.09 0.08 0.10 0.01 0.15 3.71 0.15 0.14 0.14 12.67 0.01 0.01
CSR115+92 0.02 0.02 12.67 0.01 0.01 6.62 3.21 3.35 3.37 3.21 3.40 13.47 47.98 0.51 47.83 48.24 47.70
CSR114+6 0.07 0.02 1.07 0.05 0.02 0.74 3.48 3.60 3.65 3.48 3.64 5.25 48.44 0.01 48.28 49.48 48.09 26.33 271.99
KRS186+1 0.01 1.81 0.01 37.16 0.01 0.01 0.08 0.09 0.10 0.08 0.10 0.02 0.19 3.71 0.19 0.14 0.24 12.75 25.88 0.01
CSR041+3 0.10 0.01 1.46 1.33 6.03 3.51 21.66 22.55 22.46 21.66 22.44 7.81 24.35 1.64 24.24 24.22 24.04
SYN548+1 0.01 0.01 1.62 40.59 154.40 0.01 0.03 0.07 0.03 0.03 82.45 0.20 0.20 0.36 47.99 0.01
CSR045+3 0.01 0.01 41.92 8.04 5.81 130.61 25.00 307.64 25.00 153.51 60.79
CSR116+31 0.01 0.01 2.17 0.02 0.01 0.01 3.22 3.35 3.35 3.22 3.37 94.48 48.34 110.74 47.74 50.55 48.37 27.52
KRS188+1 0.01 1.77 0.01 38.13 0.01 0.01 0.08 0.10 0.10 0.08 0.10 0.01 0.15 4.03 0.15 0.14 0.26 13.09 25.51 0.01
LCL640+1.010 0.01 0.01 35.55 1.12 9.02
CSR115+20 0.01 0.01 18.88 0.01 0.01 7.12 3.22 3.38 3.41 3.22 3.36 16.62 48.79 48.95 49.23 48.76
CSR115+24 0.02 0.01 1.45 0.02 0.01 0.94 3.23 3.39 3.38 3.23 3.38 9.64 48.05 0.40 48.59 48.66 49.49 27.52
KRS189+1 0.01 1.73 0.01 41.71 0.02 0.01 0.08 0.09 0.10 0.08 0.10 0.01 0.19 3.98 0.19 0.14 0.25 12.65 26.44 0.01
LCL642+1.005 0.01 0.01 0.02 1.01 77.63 111.02 224.28 2.15
CSR114+26 0.02 0.02 1.54 0.10 0.02 1.53 3.22 3.35 3.33 3.22 3.33 42.37 48.44 8.13 48.01 48.67 48.82 42.61
LCL638+1.005 4.51 0.02 40.97 0.14 1.21 114.43 69.67 7.89
CSR026+3 0.01 1.22 1.14 1.43 8.68 3.99 24.75 59.88 39.52 33.29 24.75 3.28 26.46 112.12 26.63 28.31
SWB029+3 1.21 2.30 55.55 0.01 0.01 45.84 0.12 236.96 4.19 9.13
SYN549+1 0.01 0.01 0.01 0.01 0.01 0.01 0.03 0.12 0.10 0.10 0.01 0.03 0.01 0.03 6.04 0.37 84.31 0.01 0.01
KRS190+1 0.01 1.74 0.03 1.84 0.01 0.01 0.08 0.09 0.09 0.08 0.09 0.01 0.15 3.73 0.15 0.13 0.14 12.62 0.02 0.01
KRS195+1 0.01 1.72 0.01 0.01 0.01 0.01 0.08 0.09 0.09 0.08 0.10 0.01 0.15 3.70 0.15 0.13 0.14 12.59 0.02 0.01
CSR059+3 1.50 1.14 1.15 1.33 4.20 1.23 21.89 22.68 22.57 21.89 22.68 3.95 26.61 2.80 26.57 24.37 24.27
CSR065+3 0.01 1.33 1.17 1.41 8.53 3.63 24.96 59.49 39.33 33.35 24.96 3.72 26.37 112.52 26.43 28.20
CSR115+27 0.02 0.03 11.85 0.02 0.01 6.59 3.24 10.47 3.39 3.24 3.40 48.60 48.84 50.42 48.42
SWV014+1 0.01 0.01 0.02 0.01 6.08 0.02 2.40 150.23 2.40 42.35
CSR055+3 0.01 0.10 1.77 1.31 4.53 2.92 21.77 22.63 22.38 21.77 22.45 1.22 24.14 29.43 24.14 24.12 24.03
CSR034+3 0.01 0.01 1.14 0.01 4.92 3.94 21.80 22.63 22.64 21.80 22.40 3.39 24.16 1.83 24.10 24.20 24.26
LCL674+1.015 3.02 3.93 2.25 11.84 7.92 216.14 216.14 0.01 0.01 31.04
CSR068+3 0.02 1.14 1.08 1.40 6.33 1.23 21.87 22.67 22.42 21.87 22.40 1.26 24.60 1.76 24.72 25.37 24.45 253.96
CSR071+3 0.10 1.15 1.36 1.43 6.14 5.51 28.00 57.16 33.28 28.00 3.41 71.74
CSR040+3 0.01 0.01 4.05 9.94 8.96 271.60 28.89 28.89 117.40
KRS193+1 0.01 1.80 0.01 0.01 0.01 0.01 0.08 0.09 0.10 0.08 0.09 0.02 0.15 3.69 0.15 0.13 0.14 12.65 0.01 0.01
KRS233+1 0.01 1.73 0.01 6.44 0.01 0.01 0.11 0.11 0.11 0.12 0.12 0.01 27.72 11.69 0.17 1.28 12.69 2.79 36.65
CSR115+15 0.01 0.01 6.55 0.01 2.70 6.87 3.20 3.36 3.36 3.20 3.37 15.91 48.14 185.06 47.83 48.17 47.65
CSR113+2 0.09 0.08 52.82 0.02 0.02 47.51 3.20 3.34 3.34 3.20 3.37 50.02 8.15 48.31 49.99 48.10 42.84
KRS187+1 0.01 1.74 0.01 2.04 0.01 0.01 0.08 0.09 0.09 0.08 0.09 0.02 0.15 3.75 0.15 0.13 0.14 12.78 0.18 0.01
CSR115+48 0.01 0.09 1.77 0.01 0.01 1.54 3.23 3.40 3.43 3.23 3.41 57.98 47.58 110.62 47.90 49.02 48.70 40.92
SWB020+2 11.74 3.92 35.76 0.01 0.01 2.15 4.21
LCL642+1.015 0.02 1.81 0.01 27.33 80.24 111.18 3.34
KRS192+1 0.01 1.76 0.01 42.21 0.01 0.01 0.08 0.10 0.10 0.08 0.10 0.04 0.15 4.25 0.15 0.14 0.27 13.21 25.70 0.01
KRS267+1 0.01 0.01 0.01 0.01 0.01 30.07 0.08 0.09 0.09 0.08 0.09 0.02 0.14 0.01 0.14 0.13 0.14 0.02
CSR114+12 0.01 0.02 1.96 0.01 0.01 1.42 3.21 3.40 3.32 3.21 3.37 43.98 48.75 8.05 47.81 50.20 47.86 44.40
CSR115+35 0.01 0.02 10.17 0.01 7.60 6.74 3.25 3.39 3.35 3.25 3.39 21.64 50.08 47.96 48.27 48.10
CSR114+16 0.01 0.09 1.59 0.02 0.01 0.02 3.21 3.35 3.38 3.21 3.35 15.07 47.78 0.42 47.45 48.22 50.26 27.00
SYN938+1 0.01 0.01 0.01 0.01 0.01 33.07 3.14 28.96
KRS191+1 0.01 1.73 0.01 1.94 0.02 0.01 0.08 0.09 0.09 0.08 0.09 0.01 0.15 3.72 0.15 0.13 0.14 12.69 0.01 0.01
CSR115+32 0.01 0.01 6.56 0.01 2.71 6.65 3.20 3.34 3.34 3.20 3.34 100.83 49.35 0.53 47.78 48.18 49.38
KRS196+1 0.01 1.73 0.01 0.01 0.01 0.01 0.08 0.09 0.09 0.08 0.10 0.01 0.15 3.72 0.15 0.13 0.14 12.68 0.01 0.01
SYO525+1.015 4.14 13.21 8.92 49.84 270.11 0.47 1.43 1.40 0.47 1.28 1.27 1.28 1.27 0.48 5.59
SWB014+3 1.20 4.35 58.78 0.01 0.01 33.94 94.04 139.22 94.04 31.33 11.14
KRS216+1 0.01 1.74 1.63 0.01 0.02 190.88 0.08 0.09 0.10 0.08 0.10 0.01 0.27 3.71 0.27 0.13 0.23 27.80
CSR035+3 0.01 0.01 1.04 0.02 6.74 1.04 21.81 22.45 22.35 21.81 22.44 1.34 24.17 1.40 24.08 24.41 24.00 30.82
CSR115+53 0.01 0.01 10.22 0.08 8.60 7.13 3.21 3.39 3.38 3.21 3.39 13.95 48.55 185.41 47.90 48.07 48.69
CSR115+89 0.01 0.01 6.06 0.01 0.03 7.14 3.27 3.35 3.38 3.27 3.42 20.57 48.82 49.20 48.48 48.33
CSR115+42 0.02 0.02 17.83 0.01 7.60 6.82 3.19 3.34 3.40 3.19 3.36 15.57 48.37 0.01 47.86 49.52 47.98
MGT067+1 0.01 0.01 0.01 0.01 0.01 0.29 0.31 0.32 0.29 0.33 0.02 0.34 1.05 0.33 0.32 0.32 0.02
CSR048+3 0.01 1.14 1.17 0.01 4.25 1.29 21.77 22.51 22.42 21.77 22.40 2.81 24.22 1.65 24.15 24.12 24.05
LCL672+1.005 24.73 1.81 14.15 58.74 107.82 113.22 53.15
CSR115+14 0.01 0.09 12.55 0.01 7.71 6.94 3.23 3.36 3.38 3.23 3.35 16.62 48.60 0.01 48.00 47.93 48.23
CSR115+61 0.01 1.53 10.36 0.09 7.70 7.14 3.21 3.33 3.39 3.21 3.39 15.17 48.42 0.01 47.86 48.17 48.10
CSR115+46 0.01 0.01 12.96 0.01 7.60 7.14 3.21 3.35 3.34 3.21 3.37 16.95 48.36 0.02 49.17 48.17 48.27
CSR027+3 10.58 44.20 4.66 1.51 5.71 132.46 64.28 106.56 64.28 58.93
CSR066+3 10.24 44.24 3.85 1.52 5.83 21.92 22.49 22.48 21.92 22.52 5.01 24.09 113.52 24.11 24.29 24.82
CSR115+71 0.05 0.02 12.75 0.02 8.62 6.64 3.22 3.32 3.35 3.22 3.35 13.82 48.66 0.53 47.79 48.53 48.00
COM008+1 72.92 6.15 96.94 0.01 1.53 18.47 0.02 0.15
CSR044+3 11.15 44.23 4.47 1.49 4.62 131.12 7.24
CSR051+3 0.02 0.02 0.01 0.01 4.98 1.14 21.94 22.67 22.38 21.94 22.27 1.23 24.57 1.31 24.43 24.16 24.20 29.88
CSR050+3 0.01 10.78 1.30 1.57 5.07 2.61 21.97 22.78 22.68 21.97 22.64 3.30 112.03
CSR064+3 0.02 0.01 21.47 2.03 6.08 3.02 21.89 22.48 22.79 21.89 22.52 1.25 24.08 1.48 24.12 24.23 24.00
CSR115+3 0.01 1.02 6.31 0.01 0.02 6.72 3.22 3.34 3.37 3.22 3.38 17.29 48.71 200.46 48.13 48.13 47.76
LCL660+1.005 0.01 0.01 2.35 123.60 261.05 110.78 194.52
CSR058+3 0.02 0.01 1.16 0.01 5.73 1.17 21.88 22.53 22.34 21.88 22.38 1.26 24.25 1.37 24.16 24.29 24.21 31.47
CSR114+11 0.02 0.02 4.02 0.02 20.94 4.54 3.22 3.41 3.38 3.22 3.38 48.41 200.81 50.62 48.59 73.75
CSR115+13 0.01 0.02 12.76 0.11 2.68 6.73 3.22 3.35 3.39 3.22 3.38 67.74 48.40 174.72 48.68 48.84 48.55
CSR115+59 0.02 0.01 3.95 0.01 0.01 4.86 3.22 5.42 3.36 3.22 3.40 48.20 48.70 49.42 49.20
CSR054+3 0.01 1.14 1.07 0.01 6.51 1.00 22.05 22.58 22.36 22.05 22.53 1.23 24.24 1.39 24.19 24.24 23.93 31.43
CSR067+3 0.01 0.01 1.15 0.01 4.30 3.62 21.76 22.53 22.37 21.76 22.55 1.26 24.18 1.48 24.20 24.25 24.20
CSR115+45 0.01 0.11 11.97 0.01 8.69 4.46 3.22 3.43 3.37 3.22 3.34 18.67 48.48 28.42 49.72 48.51 49.27
CSR070+3 0.01 1.24 1.15 8.16 4.76 132.50 109.56 109.56 11.20 70.72
CSR063+3 0.01 0.01 2.34 1.43 4.63 2.94 21.81 22.66 22.28 21.81 22.40 1.29 24.12 29.25 24.25 24.15 23.83
LCL670+1.001 0.01 0.02 43.98 0.02 1.16 328.72 328.72 171.85 0.01
CSR116+47 0.01 2.26 14.45 0.10 0.01 4.73 3.54 7.98 3.81 3.54 3.86 49.30 49.16
CSR116+15 0.01 4.72 13.14 0.01 0.02 5.81 4.56 153.35 5.14 4.56 5.17 48.27 48.25
CSR116+20 0.01 0.01 12.85 0.02 0.01 5.83 3.43 6.59 3.61 3.43 3.64 48.40 48.54
SWB012+3 1.19 4.73 0.01 0.01 45.66 13.42 237.59 11.74
CSR030+3 0.01 1.03 1.06 1.33 4.55 226.58 21.91 22.69 22.51 21.91 22.53 2.63 70.57 27.04 26.23
CSR060+3 67.36 44.29 3.87 1.43 5.86 271.20 4.79
CSR116+26 0.01 3.23 29.17 0.01 0.01 4.44 31.15 53.52 31.15 48.43 47.89
LCL660+1.001 0.01 0.01 3.64 124.32 258.01 111.04 1.33
CSR057+3 0.02 1.24 3.77 1.41 4.33 22.57 25.22 22.99 22.57 23.00 127.81 29.03 106.56
CSR073+3 0.01 0.01 0.01 5.63 4.94 21.84 22.55 22.39 21.84 22.55 3.40 70.33 24.48 24.04
CSR116+30 0.01 0.03 47.80 0.02 0.01 5.44 3.23 39.47 3.42 3.23 3.44 48.72 0.01 47.94 49.62
SYN353+1 0.75 0.01 9.98 0.01 0.02 0.01 1.40
KRS251+1 0.02 1.73 0.02 20.05 0.01 0.09 0.11 0.10 0.09 0.11 0.02 0.35 27.97 0.35 0.17 21.11
CSR062+3 0.01 1.25 1.17 1.52 4.50 286.39 23.18 36.75 24.65 23.18 24.57 3.40 112.17
LCL640+1.020 25.45 0.02 44.70 1.19 9.32
CSR116+38 0.01 0.01 25.57 0.10 0.40 3.29 8.01 3.52 3.29 3.51 48.63 48.04
CSR061+3 8.44 30.05 154.79 34.06 10.17
PRD001+1 56.47 181.78 3.64 103.07 9.37 392.03 9.37 34.64 118.95
SYO525+1.018 66.55 42.41 193.62 3.65 10.49 10.60 3.65 14.28 13.92 10.39 13.86 3.71
LCL652+1.010 0.03 0.01 3.28 150.27
KRS264+1 0.01 1.82 4.32 0.02 36.95 124.52 36.74 114.57 124.52
CSR113+20 0.01 0.01 120.96 0.01 0.01 3.22 3.39 3.38 3.22 3.36 48.04 221.43 49.05 48.38 49.92
LCL676+1.015 1.12 1.83 17.85 92.76 2.90
LCL660+1.015 1.03 0.02 7.43 111.24 15.32
CSR113+29 0.01 0.01 33.27 0.02 8.72 3.24 3.33 3.38 3.24 3.36 48.51 217.59 48.81 48.09 48.69
CSR113+12 0.11 0.01 33.00 0.01 7.70 3.26 3.39 3.38 3.26 3.39 49.25 190.20 49.81 48.47 48.57
LCL676+1.010 80.42 1.81 10.62 1.73 0.02
CSR039+3 8.45 30.06 157.89
LCL676+1.020 1.22 4.82 10.64 112.15 3.49
LAT258+1 22.17 35.75 234.46 38.16
CSR049+3 8.44 29.99 158.20 11.65
LCL668+1.005 56.71 19.82 0.01 15.03 62.42 67.64 66.23 62.42
GEO168+1 3.54 11.07 30.05 104.67
LCL638+1.010 9.79 7.53 59.45 198.13 75.33
NLP560+1 21.50 42.12 18.34 34.23 270.05 70.20 73.05 71.07 70.20 71.72
LCL658+1.010 0.01 40.86
SYO525+1.021 153.52 25.67 25.67 26.56
LCL648+1.010 4.14 160.87 44.39 12.15
SYN986+1.004 12.59 0.01 91.90 91.90
LCL658+1.015 0.02 1.80
NLP562+1 21.37 42.20 15.34 34.46 68.99 72.37 70.72 68.99 70.91
LCL668+1.010 59.92 29.22 2.43 17.22 44.07 46.48 44.07
LCL668+1.015 68.02 57.09 6.56 23.53 282.19 282.19
NLP561+1 21.44 41.96 19.24 35.32 70.34 72.64 71.99 70.34 70.89
GEO167+1 3.54 88.03
LCL682+1.015 34.01 13.18
BOO109+1 0.01
LCL646+1.010 53.55
LCL672+1.020
LCL684+1.010 5.15 65.39 11.74 112.78
LCL666+1.010 3.92 68.62 35.17 11.95 131.69
LCL876+1
LCL662+1.015
LCL668+1.020 86.37 14.86
LCL646+1.015
LCL680+1.005 65.42 193.10 1.90
LCL662+1.010
Solved 144 139 125 122 119 111 107 95 94 94 93 91 85 85 83 82 77 35 29 18 15
Vampire 4 Vampire 2 iProver E ET CVC4 CM-ALL CM-n1 CM-n2 CM-n3 CM-n4 iProverM CM-n5 leanCoP CM-n6 CM-n7 CM-n8 ePrincess Prover9 Muscadet Geo-III