Colour key: 1st place 2nd place 3rd place Demonstration Previous winner
Higher-order Theorems Vampire
5.0 		Vampire
5.0.1 		E
3.5.1 		Leo‑III
1.8.0 		LEO‑II
1.7.0 		Zipperpin
2.1.9999
Solved/400 354/400 352/400 324/400 160/400 67/400 347/400
Av. WC Time 6.82 6.49 10.70 14.44 10.98 16.66
Av. CPU Time 40.78 37.68 45.80 43.04 10.13 115.54
Solutions/400 344/400 340/400 323/400 137/400 67/400 0/400
μWCEfficiency 576 615 593 83 110 334
μEfficiency 441 485 548 47 116 261
SotAC - 0.32 0.29 0.07 0.01 0.31
Core Usage/> 1.0 4.16/238 3.89/212 4.18/129 2.51/160 0.00/0 5.66/268
Core U. ≤ 1.0 116 140 195 0 67 79
New Solved 31/31 31/31 28/31 7/31 0/31 29/31
Unique Solved 3/31 3/31 23/31 1/31 0/31 1/31
First-order Theorems Vampire
5.0.1 		Vampire
5.0 		E
3.5.1 		CSI_PP
1.0 		iProver
3.9.4 		Drodi
4.1.1 		Prover9
2026‑6A 		LisaST
0.9 		FindProof
0.1 		SUPr
1.0 		mrs
0.2.0 		VIP
1.718 		ConnectPP
0.7.2 		SATResetCoP
1.0 		SPASS‑SCL
0.1.1 		Zipperpin
2.1.9999 		Prover9
1109a
Solved/400 381/400 328/400 264/400 264/400 250/400 215/400 143/400 199/400 91/400 73/400 79/400 32/400 64/400 20/400 14/400 192/400 92/400
Av. WC Time 9.47 8.05 10.56 14.05 22.95 20.33 12.99 18.52 19.80 16.69 12.57 26.08 59.59 70.52 21.91 19.62 14.74
Av. CPU Time 45.05 49.78 63.38 59.31 109.63 140.66 89.15 73.36 139.74 77.57 87.59 25.80 59.25 70.21 21.60 127.31 13.24
Solutions/400 380/400 328/400 264/400 264/400 222/400 214/400 139/400 127/400 91/400 73/400 71/400 32/400 24/400 20/400 14/400 0/400 0/400
μWCEfficiency 309 538 419 408 176 312 208 74 46 92 106 34 22 3 12 196 134
μEfficiency 193 413 375 366 112 250 155 19 10 69 80 35 22 3 12 155 140
SotAC 0.55 0.43 0.29 0.29 0.27 0.22 0.12 0.20 0.06 0.05 0.05 0.01 0.04 0.01 0.01 0.18 -
Core Usage/> 1.0 3.54/346 3.94/236 4.89/142 4.56/139 4.00/231 6.00/126 5.28/98 5.14/192 6.42/91 3.96/54 5.05/59 0.00/0 0.00/0 0.00/0 0.00/0 4.92/143 0.00/0
Core U. ≤ 1.0 35 92 122 125 19 89 45 7 0 19 20 32 64 20 14 49 92
New Solved 71/79 70/79 55/79 55/79 54/79 40/79 25/79 52/79 18/79 21/79 18/79 8/79 13/79 9/79 0/79 47/79 22/79
Unique Solved 45/48 3/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48 0/48
First-order Non-theorems Vampire
5.0.1 		Vampire
4.8 		iProver
3.9.4 		FMB4J
0.1 		Mace4
2026‑6A 		E
3.5.1 		Drodi
4.1.1 		ConnectPP
0.7.2
Solved/150 143/150 131/150 71/150 51/150 45/150 42/150 41/150 11/150
Av. WC Time 11.68 17.37 25.49 9.34 8.99 9.43 6.08 0.36
Av. CPU Time 63.01 112.09 125.03 11.25 27.16 31.00 27.87 0.10
Solutions/150 143/150 127/150 71/150 51/150 44/150 42/150 41/150 0/150
μWCEfficiency 516 483 161 253 243 168 206 73
μEfficiency 434 411 176 241 229 151 175 73
SotAC 0.58 - 0.19 0.11 0.10 0.12 0.09 0.01
Core Usage/> 1.0 4.73/87 5.56/82 3.25/53 1.34/33 4.21/12 4.30/22 4.85/17 0.00/0
Core U. ≤ 1.0 56 49 18 18 33 20 24 11
New Solved 10/10 10/10 8/10 7/10 8/10 2/10 2/10 0/10
Unique Solved 14/16 2/16 0/16 0/16 0/16 0/16 0/16 0/16
Unit Equality CNF Vampire
5.0.1 		Vampire
5.0 		Twee
2.7 		CSI_PP
1.0 		E
3.5.1 		FindProof
0.1 		Prover9
2026‑6A 		iProver
3.9.4 		Drodi
4.1.1 		mrs
0.2.0
Solved/400 370/400 322/400 286/400 258/400 255/400 269/400 208/400 198/400 163/400 76/400
Av. WC Time 11.82 16.57 22.41 21.54 20.40 25.27 21.39 37.85 37.23 36.78
Av. CPU Time 52.79 108.33 164.31 125.14 132.78 166.72 159.98 214.51 273.66 229.35
Solutions/400 370/400 322/400 286/400 258/400 255/400 251/400 207/400 198/400 163/400 75/400
μWCEfficiency 222 295 225 261 244 118 202 73 127 33
μEfficiency 110 147 92 160 149 26 117 34 74 20
SotAC 0.40 - 0.24 0.19 0.19 0.21 0.15 0.12 0.09 0.02
Core Usage/> 1.0 4.09/351 5.22/310 6.40/273 5.02/223 5.27/226 6.50/269 6.23/179 5.05/189 6.65/143 5.75/71
Core U. ≤ 1.0 19 12 13 35 29 0 29 9 20 5
New Solved 12/21 13/21 7/21 9/21 8/21 4/21 10/21 7/21 3/21 2/21
Unique Solved 17/30 3/30 2/30 1/30 1/30 1/30 4/30 1/30 0/30 0/30
Proof Verification GAPT
2.20 		VaLeaDate
0.1 		Norgler
1.1 		ProofCheck
1.0 		ProofGuard
1.0 		mrs‑proover
0.2.0 		PyCheck
0.1 		GDV
2.0 		GDV‑LP
2.0 		CheckProof
0.1
Score/150 114/150 97/150 93/150 67/150 55/150 37/150 19/150 -1/150 -5/150 -110/150
Av. WC Time 3.95 1.79 2.06 0.79 1.83 0.75 1.78 0.01 0.01 0.43
Av. CPU Time 3.50 3.23 3.51 1.19 1.43 0.18 1.76 0.01 0.01 0.14
VSB/100 42/100 48/100 49/100 44/100 43/100 41/100 28/100 9/100 9/100 26/100
VSG/100 36/100 24/100 27/100 33/100 32/100 32/100 38/100 36/100 33/100 30/100
UNK/100 8/100 3/100 1/100 3/100 5/100 1/100 7/100 9/100 11/100 8/100
UNK/100 8/100 2/100 0/100 2/100 2/100 3/100 15/100 36/100 36/100 6/100
VSB/100 6/100 23/100 22/100 14/100 13/100 17/100 5/100 5/100 6/100 12/100
VSG/100 0/100 0/100 1/100 4/100 5/100 6/100 7/100 5/100 5/100 18/100
THF without Equality E
3.5.1 		Vampire
5.0 		Vampire
5.0.1 		Leo‑III
1.8.0 		LEO‑II
1.7.0 		Zipperpin
2.1.9999
Solved/100 73/100 70/100 67/100 38/100 26/100 67/100
Av. WC Time 13.27 2.73 5.00 5.03 5.54 14.55
Av. CPU Time 83.69 15.52 29.50 13.53 5.24 104.01
Solutions/100 73/100 66/100 61/100 38/100 26/100 0/100
μWCEfficiency 545 539 568 105 195 346
μEfficiency 496 465 511 64 197 301
SotAC 0.33 - 0.23 0.05 0.01 0.23
Core Usage/> 1.0 4.90/29 4.44/31 4.35/20 2.06/38 0.00/0 5.59/43
Core U. ≤ 1.0 44 39 47 0 26 24
New Solved 0/0 0/0 0/0 0/0 0/0 0/0
Unique Solved 19/20 1/20 0/20 0/20 0/20 0/20
THF with Equality Vampire
5.0.1 		Vampire
5.0 		E
3.5.1 		Leo‑III
1.8.0 		LEO‑II
1.7.0 		Zipperpin
2.1.9999
Solved/300 285/300 284/300 251/300 122/300 41/300 280/300
Av. WC Time 6.84 7.83 9.96 17.37 14.44 17.17
Av. CPU Time 39.60 47.01 34.78 52.23 13.24 118.29
Solutions/300 279/300 278/300 250/300 99/300 41/300 0/300
μWCEfficiency 631 588 609 75 82 330
μEfficiency 476 433 566 41 90 248
SotAC 0.34 - 0.27 0.08 0.01 0.33
Core Usage/> 1.0 3.84/192 4.12/207 3.98/100 2.65/122 0.00/0 5.67/225
Core U. ≤ 1.0 93 77 151 0 41 55
New Solved 31/31 31/31 28/31 7/31 0/31 29/31
Unique Solved 3/11 2/11 4/11 1/11 0/11 1/11
FOF Theorems without Equality Vampire
5.0.1 		Vampire
5.0 		CSI_PP
1.0 		E
3.5.1 		iProver
3.9.4 		Drodi
4.1.1 		Prover9
2026‑6A 		LisaST
0.9 		FindProof
0.1 		mrs
0.2.0 		SUPr
1.0 		SPASS‑SCL
0.1.1 		ConnectPP
0.7.2 		VIP
1.718 		SATResetCoP
1.0 		Zipperpin
2.1.9999 		Prover9
1109a
Solved/100 94/100 80/100 76/100 75/100 64/100 60/100 50/100 54/100 26/100 23/100 22/100 14/100 27/100 13/100 3/100 46/100 23/100
Av. WC Time 7.86 13.08 22.55 8.10 21.14 21.08 11.00 11.17 16.54 11.49 14.62 21.91 48.16 25.01 116.60 20.69 16.22
Av. CPU Time 34.67 84.59 69.64 46.12 108.73 161.31 78.42 47.67 123.99 85.97 34.65 21.60 47.84 24.73 116.32 131.60 15.93
Solutions/100 94/100 80/100 76/100 75/100 63/100 59/100 50/100 43/100 26/100 23/100 22/100 14/100 14/100 13/100 3/100 0/100 0/100
μWCEfficiency 307 520 426 460 192 318 309 83 52 149 75 46 43 64 0 184 127
μEfficiency 226 456 425 427 112 245 213 25 11 106 61 47 43 64 0 158 137
SotAC 0.49 0.36 0.33 0.32 0.25 0.21 0.18 0.19 0.06 0.05 0.05 0.04 0.06 0.02 0.00 0.14 -
Core Usage/> 1.0 3.58/82 4.55/46 4.88/34 5.04/39 3.96/61 6.21/39 4.96/36 4.91/51 6.57/26 4.71/17 2.96/18 0.00/0 0.00/0 0.00/0 0.00/0 4.40/34 0.00/0
Core U. ≤ 1.0 12 34 42 36 3 21 14 3 0 6 4 14 27 13 3 12 23
New Solved 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0
Unique Solved 10/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10 0/10
FOF Theorems with Equality Vampire
5.0.1 		Vampire
5.0 		E
3.5.1 		CSI_PP
1.0 		iProver
3.9.4 		Drodi
4.1.1 		Prover9
2026‑6A 		LisaST
0.9 		FindProof
0.1 		SUPr
1.0 		mrs
0.2.0 		VIP
1.718 		SATResetCoP
1.0 		ConnectPP
0.7.2 		Zipperpin
2.1.9999 		Prover9
1109a 		SPASS‑SCL
0.1.1
Solved/300 287/300 248/300 189/300 188/300 186/300 155/300 93/300 145/300 65/300 51/300 56/300 19/300 17/300 37/300 146/300 69/300 0/300
Av. WC Time 9.99 6.43 11.53 10.62 23.58 20.04 14.06 21.25 21.11 17.58 13.01 26.82 62.39 67.94 19.28 14.25 -
Av. CPU Time 48.45 38.55 70.24 55.13 109.94 132.67 94.92 82.93 146.03 96.08 88.26 26.53 62.07 67.59 125.96 12.34 -
Solutions/300 286/300 248/300 189/300 188/300 159/300 155/300 89/300 84/300 65/300 51/300 48/300 19/300 17/300 10/300 0/300 0/300 0/300
μWCEfficiency 310 544 405 402 171 311 174 71 44 97 92 24 3 15 201 136 -
μEfficiency 182 399 358 347 111 251 136 17 9 72 72 25 4 15 154 141 -
SotAC 0.57 0.45 0.28 0.28 0.28 0.22 0.10 0.20 0.07 0.05 0.05 0.01 0.01 0.03 0.20 - -
Core Usage/> 1.0 3.53/264 3.79/190 4.83/103 4.45/105 4.02/170 5.91/87 5.47/62 5.23/141 6.36/65 4.46/36 5.19/42 0.00/0 0.00/0 0.00/0 5.08/109 0.00/0 -
Core U. ≤ 1.0 23 58 86 83 16 68 31 4 0 15 14 19 17 37 37 69 0
New Solved 71/79 70/79 55/79 55/79 54/79 40/79 25/79 52/79 18/79 21/79 18/79 8/79 9/79 13/79 47/79 22/79 0/79
Unique Solved 35/38 3/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38 0/38
FOF Non-theorems without Equality Vampire
5.0.1 		Vampire
4.8 		E
3.5.1 		iProver
3.9.4 		FMB4J
0.1 		Mace4
2026‑6A 		Drodi
4.1.1 		ConnectPP
0.7.2
Solved/50 45/50 45/50 17/50 15/50 8/50 8/50 7/50 3/50
Av. WC Time 17.28 31.72 15.98 23.71 0.89 2.31 20.78 0.39
Av. CPU Time 89.24 219.20 54.36 60.02 1.10 9.36 66.25 0.13
Solutions/50 45/50 44/50 17/50 15/50 8/50 8/50 7/50 0/50
μWCEfficiency 348 327 111 97 140 141 84 60
μEfficiency 278 260 89 90 137 140 87 60
SotAC 0.62 - 0.18 0.12 0.05 0.05 0.04 0.01
Core Usage/> 1.0 4.73/35 6.04/36 5.10/12 2.73/12 1.25/7 4.69/1 4.49/2 0.00/0
Core U. ≤ 1.0 10 9 5 3 1 7 5 3
New Solved 0/0 0/0 0/0 0/0 0/0 0/0 0/0 0/0
Unique Solved 2/4 2/4 0/4 0/4 0/4 0/4 0/4 0/4
FOF Non-theorems with Equality Vampire
5.0.1 		Vampire
4.8 		iProver
3.9.4 		FMB4J
0.1 		Mace4
2026‑6A 		Drodi
4.1.1 		E
3.5.1 		ConnectPP
0.7.2
Solved/100 98/100 86/100 56/100 43/100 37/100 34/100 25/100 8/100
Av. WC Time 9.11 9.86 25.97 10.91 10.44 3.06 4.97 0.35
Av. CPU Time 50.97 56.05 142.45 13.14 31.01 19.96 15.11 0.09
Solutions/100 98/100 83/100 56/100 43/100 36/100 34/100 25/100 0/100
μWCEfficiency 600 560 194 310 294 267 197 80
μEfficiency 513 486 220 293 274 219 182 80
SotAC 0.56 - 0.22 0.14 0.12 0.11 0.09 0.02
Core Usage/> 1.0 4.74/52 5.18/46 3.41/41 1.36/26 4.17/11 4.90/15 3.33/10 0.00/0
Core U. ≤ 1.0 46 40 15 17 26 19 15 8
New Solved 10/10 10/10 8/10 7/10 8/10 2/10 2/10 0/10
Unique Solved 12/12 0/12 0/12 0/12 0/12 0/12 0/12 0/12
Unit Equality CNF Vampire
5.0.1 		Vampire
5.0 		Twee
2.7 		CSI_PP
1.0 		E
3.5.1 		FindProof
0.1 		Prover9
2026‑6A 		iProver
3.9.4 		Drodi
4.1.1 		mrs
0.2.0
Solved/400 370/400 322/400 286/400 258/400 255/400 269/400 208/400 198/400 163/400 76/400
Av. WC Time 11.82 16.57 22.41 21.54 20.40 25.27 21.39 37.85 37.23 36.78
Av. CPU Time 52.79 108.33 164.31 125.14 132.78 166.72 159.98 214.51 273.66 229.35
Solutions/400 370/400 322/400 286/400 258/400 255/400 251/400 207/400 198/400 163/400 75/400
μWCEfficiency 222 295 225 261 244 118 202 73 127 33
μEfficiency 110 147 92 160 149 26 117 34 74 20
SotAC 0.40 - 0.24 0.19 0.19 0.21 0.15 0.12 0.09 0.02
Core Usage/> 1.0 4.09/351 5.22/310 6.40/273 5.02/223 5.27/226 6.50/269 6.23/179 5.05/189 6.65/143 5.75/71
Core U. ≤ 1.0 19 12 13 35 29 0 29 9 20 5
New Solved 12/21 13/21 7/21 9/21 8/21 4/21 10/21 7/21 3/21 2/21
Unique Solved 17/30 3/30 2/30 1/30 1/30 1/30 4/30 1/30 0/30 0/30
Proof Verification GAPT
2.20 		VaLeaDate
0.1 		Norgler
1.1 		ProofCheck
1.0 		ProofGuard
1.0 		mrs‑proover
0.2.0 		PyCheck
0.1 		GDV
2.0 		GDV‑LP
2.0 		CheckProof
0.1
Score/150 114/150 97/150 93/150 67/150 55/150 37/150 19/150 -1/150 -5/150 -110/150
Av. WC Time 3.95 1.79 2.06 0.79 1.83 0.75 1.78 0.01 0.01 0.43
Av. CPU Time 3.50 3.23 3.51 1.19 1.43 0.18 1.76 0.01 0.01 0.14
VSB/100 42/100 48/100 49/100 44/100 43/100 41/100 28/100 9/100 9/100 26/100
VSG/100 36/100 24/100 27/100 33/100 32/100 32/100 38/100 36/100 33/100 30/100
UNK/100 8/100 3/100 1/100 3/100 5/100 1/100 7/100 9/100 11/100 8/100
UNK/100 8/100 2/100 0/100 2/100 2/100 3/100 15/100 36/100 36/100 6/100
VSB/100 6/100 23/100 22/100 14/100 13/100 17/100 5/100 5/100 6/100 12/100
VSG/100 0/100 0/100 1/100 4/100 5/100 6/100 7/100 5/100 5/100 18/100