Higher-order Theorems Satallax
 3.0
Satallax
 2.8
LEO‑II
 1.7.0
Leo+III
 1.0
Leo‑III
 1.0
Isabelle
 2015
Solved/500 346/500 315/500 238/500 89/500 74/500 356/500
Av. CPU Time 22.10 19.45 20.93 48.37 42.79 81.08
Solutions 327/500 313/500 231/500 88/500 74/500 0/500
Typed First-order Theorems +*-/ Vampire
 4.1
VampireZ3
 1.0
CVC4
 TFF‑1.5.1
Beagle
 0.9.47
Princess
 160606
Solved/500 419/500 380/500 343/500 300/500 342/500
Av. CPU Time 13.39 9.15 5.72 18.76 17.59
Solutions 419/500 380/500 343/500 300/500 271/500
Typed First-order Non-theorems +*-/ Beagle
 SAT‑0.9.47
CVC4
 TFN‑1.5.1
Princess
 160606
CVC4
 TFN‑1.5
Solved/50 10/50 9/50 8/50 8/50
Av. CPU Time 3.11 0.02 1.44 22.90
First-order Theorems Vampire
 4.0
Vampire
 4.1
E
 2.0
CVC4
 FOF‑1.5.1
iProver
 2.5
leanCoP
 2.2
Prover9
 1109a
Geo‑III
 2016C
Solved/500 457/500 447/500 392/500 329/500 278/500 168/500 101/500 54/500
Av. CPU Time 15.39 14.14 30.87 35.04 30.82 77.94 29.99 41.73
Solutions 453/500 447/500 392/500 328/500 274/500 168/500 98/500 54/500
First-order Non-theorems Vampire
 SAT‑4.1
Vampire
 SAT‑4.0
iProver
 SAT‑2.5
Nitpick
 2015
CVC4
 FNT‑1.5.1
Geo‑III
 2016C
E
 FNT‑2.0
Refute
 2015
Solved/300 250/300 240/300 200/300 139/300 96/300 76/300 70/300 58/300
Av. CPU Time 40.11 36.45 30.28 37.86 22.43 13.69 16.31 69.09
Solutions 248/300 238/300 200/300 139/300 96/300 76/300 70/300 0/300
Effectively Propositional CNF iProver
 2.5
Vampire
 4.1
Vampire
 4.0
E
 2.0
Geo‑III
 2016C
Solved/300 229/300 222/300 222/300 101/300 10/300
Av. CPU Time 28.25 29.19 35.35 21.85 55.88
Large Theory Batch Problems Vampire
 LTB‑4.0
Vampire
 LLTB‑4.1
Vampire
 LTB‑4.1
E
 LTB‑2.0
iProver
 LTB‑2.5
Prover9Plus
 1.0
Solved/600 403/600 398/600 396/600 305/600 298/600 85/200
Av. WC Time 11.62 9.54 8.05 12.56 35.07 14.41
Solutions 403/600 398/600 396/600 305/600 298/600 85/200