Results for:
THF TFA FOF FNT EPR UEQ TNE TEQ TFI TFR TFE FNE FEQ FNN FNQ EPT EPS UEQ

Results for THF (Higher-order Theorems)

Higher-order Theorems Satallax_MaLeS
 1.3
Satallax
 2.7
Isabelle
 2013
LEO‑II
 1.6.2
agsyHOL
 1.0
HOLyHammer
 140616
cocATP
 0.2.0
SEU918^5 1.54 0.01 32.40 +50.03 0.03 TMO‑Non TMO‑Non
SYO113^5 36.37 0.64 2.18 +0.04 TMO‑Non 0.05 TMO‑Non
SYO464^4 1.52 0.01 17.86 +0.01 0.01 TMO‑Non TMO‑Non
LCL734^5 1.54 3.32 18.58 +0.01 0.01 GUP‑Non +0.02
SYN041^4 1.55 0.01 18.91 +0.01 1.52 GUP‑Non TMO‑Non
SEU967^5 1.60 0.01 2.25 +0.01 0.01 GUP‑Non TMO‑Non
SEU497^1 1.55 0.63 17.80 +0.01 TMO‑Non 192.19 TMO‑Non
SYO032^1 46.97 6.55 2.73 +0.01 0.01 GUP‑Non +0.02
SEU534^1 TMO‑Non 5.62 32.33 TMO‑Non 8.44 1.64 TMO‑Non
SYO307^5 1.79 0.01 56.14 +0.01 0.01 GUP‑Non UNK‑Non
SYO006^1 1.53 0.01 2.75 +0.01 0.01 GUP‑Non +0.02
SYO296^5 1.55 0.01 21.49 +0.01 0.01 GUP‑Non UNK‑Non
SYO457^3 1.49 0.01 2.59 +0.01 0.01 TMO‑Non TMO‑Non
SYO033^1 1.53 9.17 2.25 UNK‑Non 0.01 GUP‑Non +0.02
SYO417^1 1.55 0.01 18.29 +0.01 0.01 TMO‑Non TMO‑Non
SYO356^5 1.49 0.01 21.90 +0.01 0.01 GUP‑Non +0.02
SEU785^1 1.59 4.49 79.72 +16.14 TMO‑Non 1.41 TMO‑Non
SYO257^5 1.53 0.01 2.27 +0.01 0.01 GUP‑Non UNK‑Non
SEV002^5 1.65 UNK‑Non 66.27 +0.05 2.16 0.01 TMO‑Non
SYO292^5 1.53 0.01 5.35 +0.01 0.01 GUP‑Non UNK‑Non
AGT034^2 43.38 5.69 103.32 +0.01 1.25 TMO‑Non UNK‑Non
SYO286^5 1.49 0.01 2.25 +0.01 0.01 GUP‑Non +0.02
SYO060^4 1.60 0.01 17.80 +0.02 TMO‑Non 75.08 +0.02
SYO285^5 1.55 0.01 2.26 +0.01 0.01 GUP‑Non +0.02
SYO399^1 1.53 0.01 2.46 +0.01 0.01 TMO‑Non TMO‑Non
SEV055^5 3.48 3.84 93.39 +25.63 0.01 TMO‑Non TMO‑Non
AGT037^1 1.51 2.37 100.30 +0.01 0.01 TMO‑Non UNK‑Non
SYO293^5 1.53 0.01 2.18 +0.01 0.01 GUP‑Non UNK‑Non
SYO497^6 1.55 0.01 18.24 +0.01 3.53 TMO‑Non TMO‑Non
SYO170^5 14.87 49.18 63.99 +0.01 TMO‑Non 0.01 UNK‑Non
SEU657^2 1.53 9.30 2.34 +0.01 TMO‑Non 0.01 TMO‑Non
SYO299^5 1.52 0.01 2.75 +0.01 TMO‑Non 0.01 TMO‑Non
SEU752^2 1.54 2.79 78.12 +0.02 TMO‑Non 0.01 TMO‑Non
SYO255^5 1.53 0.01 2.26 +0.01 0.01 GUP‑Non +0.03
SEV285^5 1.53 0.01 2.16 +0.01 0.01 GUP‑Non +0.01
SEV257^5 126.66 37.50 18.76 +56.12 0.01 TMO‑Non UNK‑Non
SYO401^1 1.54 0.01 2.44 +0.01 0.01 TMO‑Non TMO‑Non
SYO373^5 1.55 0.01 14.53 +0.01 0.01 GUP‑Non TMO‑Non
SEU594^1 83.08 1.62 78.57 TMO‑Non 0.53 0.02 TMO‑Non
SEV406^5 1.49 0.01 44.54 +0.01 0.01 GUP‑Non UNK‑Non
SEU601^2 1.51 0.01 2.23 +47.55 0.01 GUP‑Non +0.03
SEV081^5 1.56 0.01 2.25 +1.82 0.01 GUP‑Non UNK‑Non
SEU483^1 82.37 8.73 208.42 TMO‑Non 0.01 200.23 UNK‑Non
SEV383^5 1.49 0.01 2.03 +0.01 0.01 GUP‑Non +0.02
SYO025^1 1.55 0.01 2.72 +0.01 0.02 UNK‑Non TMO‑Non
SYO259^5 1.49 0.02 48.67 +0.01 0.01 GUP‑Non UNK‑Non
SYO457^4 1.53 0.01 11.08 +0.01 0.01 TMO‑Non TMO‑Non
SYO009^1 1.54 0.02 2.26 +0.01 0.01 GUP‑Non UNK‑Non
SYO451^6 1.50 0.01 63.25 +0.01 0.01 TMO‑Non TMO‑Non
SYO277^5 1.82 0.01 97.78 +0.02 0.01 GUP‑Non +1.23
SYO459^6 1.55 0.01 17.83 +0.02 0.01 TMO‑Non TMO‑Non
SYO188^5 1.72 0.01 3.09 +0.01 0.01 GUP‑Non +0.02
SEU469^1 250.55 0.01 64.22 +0.01 TMO‑Non GUP‑Non TMO‑Non
SYO260^5 1.53 0.01 63.86 +0.01 0.01 GUP‑Non UNK‑Non
SEV239^5 1.53 0.02 2.24 +0.05 0.01 GUP‑Non TMO‑Non
SEV095^5 1.56 6.72 19.07 TMO‑Non 0.01 GUP‑Non TMO‑Non
SET926^7 116.20 7.73 116.08 +0.01 5.33 TMO‑Non UNK‑Non
SYN386^5 26.90 UNK‑Non 3.00 +0.01 1.74 0.01 TMO‑Non
SEU670^2 1.61 0.01 17.71 TMO‑Non 0.01 GUP‑Non +0.03
NUM762^1 TMO‑Non UNK‑Non 28.52 +0.01 7.43 25.03 UNK‑Non
SEV385^5 32.45 0.01 3.66 +9.92 0.01 GUP‑Non TMO‑Non
SYO193^5 1.55 0.01 2.73 +0.01 0.01 GUP‑Non UNK‑Non
NUM924^3 TMO‑Non 17.62 87.44 +25.61 TMO‑Non 6.40 UNK‑Non
SYO093^5 1.56 0.01 2.20 +0.01 TMO‑Non 0.02 UNK‑Non
SEU557^1 1.54 0.01 148.46 +138.04 0.02 1.53 TMO‑Non
SYO291^5 1.53 0.02 2.27 +0.01 0.01 GUP‑Non +0.33
PUZ081^1 1.51 3.31 18.15 +0.01 TMO‑Non 0.03 UNK‑Non
SYO327^5 27.48 6.60 2.26 TMO‑Non 0.01 GUP‑Non UNK‑Non
SYO049^1 1.51 0.01 2.63 +0.01 0.01 TMO‑Non TMO‑Non
SYO301^5 1.52 0.01 2.27 +0.01 0.01 GUP‑Non UNK‑Non
SEV057^5 1.52 0.01 2.27 TMO‑Non 0.01 TMO‑Non +3.94
SYO268^5 30.85 0.13 64.32 +0.01 0.01 GUP‑Non +3.35
SEU650^1 2.23 0.01 85.87 +22.74 1.94 2.32 TMO‑Non
SYO371^5 1.54 0.01 2.75 +0.01 0.01 GUP‑Non +0.01
SYO485^6 1.49 0.01 17.82 +0.01 0.01 TMO‑Non +1.34
SYO352^5 1.55 0.01 118.45 +0.01 0.01 GUP‑Non +0.01
SYO394^1 1.47 0.01 2.60 +0.01 0.01 TMO‑Non TMO‑Non
SYO183^6 1.53 0.01 3.08 +0.01 0.01 GUP‑Non +0.02
SYN999^1 1.55 0.01 153.26 +0.01 0.01 GUP‑Non +0.02
SYO196^5 1.52 0.01 2.72 +0.01 0.01 GUP‑Non +0.02
SYO406^1 1.52 0.01 2.60 +0.02 0.01 TMO‑Non TMO‑Non
SYO175^5 1.52 0.01 2.25 +0.01 TMO‑Non 0.01 TMO‑Non
SYO361^5 1.50 0.01 127.76 +0.01 0.01 GUP‑Non +1.13
SYN364^5 1.62 2.26 2.23 +0.01 TMO‑Non 0.01 TMO‑Non
SYO488^6 1.53 0.01 17.82 +0.01 0.01 TMO‑Non TMO‑Non
SEU927^5 1.53 0.01 2.11 TMO‑Non 0.01 GUP‑Non UNK‑Non
SYO460^6 1.59 0.01 17.81 +0.02 0.01 TMO‑Non TMO‑Non
SYO199^5 1.50 0.01 2.72 +0.01 0.01 GUP‑Non UNK‑Non
SEU625^2 1.62 5.97 78.16 +0.01 TMO‑Non 0.01 UNK‑Non
SYO028^1 1.53 0.01 3.04 +0.01 0.01 GUP‑Non +0.02
SEU745^1 4.60 1.49 86.80 +8.23 TMO‑Non 0.05 TMO‑Non
SYO114^5 1.89 0.01 2.26 +0.01 0.01 0.01 TMO‑Non
SYO052^2 29.14 108.41 3.01 +0.01 0.01 TMO‑Non UNK‑Non
SYO507^1 1.53 0.01 2.25 +0.01 0.01 GUP‑Non UNK‑Non
SEU810^1 19.08 UNK‑Non 87.33 +12.32 0.02 1.82 TMO‑Non
SYO105^5 39.03 UNK‑Non 2.32 +0.01 0.01 0.01 TMO‑Non
SYO450^3 1.54 0.01 2.79 +0.01 3.83 TMO‑Non TMO‑Non
SEV398^5 1.62 3.31 63.74 +0.01 0.01 TMO‑Non +3.04
SEU974^5 1.54 3.60 85.31 +4.80 0.01 0.01 TMO‑Non
LCL736^5 2.64 9.12 18.60 +0.01 0.01 GUP‑Non +0.03
SEU793^2 27.16 0.01 2.26 TMO‑Non 0.01 GUP‑Non +7.52
SYO034^1 1.53 0.01 2.73 +0.01 0.01 GUP‑Non +0.03
SYO035^1 1.53 0.01 2.28 +0.01 0.01 GUP‑Non TMO‑Non
SYO513^1 1.48 0.01 2.71 +0.01 0.01 GUP‑Non +0.02
SYO568^7 1.54 0.01 17.92 +0.02 0.01 TMO‑Non TMO‑Non
SYO258^5 1.56 0.02 17.83 +0.01 0.01 GUP‑Non UNK‑Non
SYO403^1 1.54 0.01 2.59 +0.01 0.01 TMO‑Non TMO‑Non
SYO267^5 1.54 0.01 33.79 +9.05 0.01 GUP‑Non UNK‑Non
SYO458^3 1.47 0.01 2.43 +0.02 0.01 TMO‑Non TMO‑Non
SYO270^5 1.55 0.01 2.26 +0.01 0.01 GUP‑Non UNK‑Non
SEV067^5 1.53 0.01 71.48 +0.01 TMO‑Non 0.01 TMO‑Non
SYO385^5 5.82 5.53 3.57 +0.01 TMO‑Non 52.92 UNK‑Non
SYO008^1 1.53 0.01 131.20 +0.01 0.01 GUP‑Non +0.33
SEV054^5 2.02 0.01 110.54 +25.63 0.01 TMO‑Non TMO‑Non
SYO547^1 1.52 0.01 48.59 +0.01 7.23 GUP‑Non +0.02
SYO315^5 25.11 0.05 2.25 +0.01 TMO‑Non 0.01 TMO‑Non
SEU630^2 1.53 0.01 24.18 TMO‑Non 13.05 GUP‑Non +2.25
SYO029^1 1.53 0.01 3.09 +0.01 0.01 GUP‑Non +0.02
SEV290^5 1.54 2.30 2.27 +25.05 0.01 TMO‑Non +0.02
SEV408^5 1.50 0.01 2.01 +0.01 0.01 GUP‑Non +0.02
SYO450^5 1.55 0.01 67.03 +0.01 9.24 TMO‑Non TMO‑Non
NUM824^5 69.62 0.01 2.43 +0.01 TMO‑Non GUP‑Non UNK‑Non
SWV061^7 1.56 3.32 79.12 TMO‑Non 0.01 138.23 TMO‑Non
SYN374^5 1.51 0.01 2.23 +0.01 0.01 GUP‑Non TMO‑Non
SYO228^5 44.92 0.02 2.26 +0.01 0.01 91.14 TMO‑Non
LCL738^5 1.54 3.33 4.78 +0.06 0.01 GUP‑Non +0.03
SEV116^5 1.51 0.01 2.25 +0.01 0.01 0.01 +0.43
SYO198^5 1.49 0.01 2.72 +0.01 0.01 GUP‑Non UNK‑Non
SYO230^5 1.54 0.01 2.25 +0.01 0.01 GUP‑Non +0.03
SEV162^5 1.53 0.01 2.26 +0.01 0.01 GUP‑Non UNK‑Non
AGT041^1 1.47 0.01 100.35 +0.01 0.01 TMO‑Non UNK‑Non
SYO266^5 1.54 0.01 2.27 +0.01 0.04 GUP‑Non +18.54
GEG015^1 1.53 0.01 TMO‑Non +9.63 0.34 69.66 UNK‑Non
SYO262^5 1.48 0.01 2.21 TMO‑Non 0.01 GUP‑Non UNK‑Non
AGT038^1 1.53 0.05 100.35 +0.01 0.01 TMO‑Non UNK‑Non
SYO314^5 98.38 2.17 2.46 +0.01 TMO‑Non 75.03 TMO‑Non
SEU581^1 1.55 4.11 21.57 TMO‑Non 0.01 25.11 TMO‑Non
CSR144^1 1.53 0.01 30.62 TMO‑Non 9.74 0.02 UNK‑Non
SYO241^5 1.49 0.01 24.04 +131.82 76.86 0.02 TMO‑Non
SYO200^5 1.55 0.01 2.72 +0.01 0.01 GUP‑Non UNK‑Non
SEU707^2 1.58 2.62 38.51 TMO‑Non 0.01 TMO‑Non +2.33
SEV254^5 1.54 0.01 3.14 TMO‑Non 19.24 75.08 TMO‑Non
SEU779^2 1.56 0.01 24.20 TMO‑Non 0.01 GUP‑Non +2.65
SYO370^5 1.51 0.01 2.25 +0.01 0.01 GUP‑Non UNK‑Non
SEU803^1 1.99 4.50 181.04 TMO‑Non 0.01 18.69 TMO‑Non
SEV409^5 1.55 0.01 3.09 +0.01 0.01 GUP‑Non UNK‑Non
SYO395^1 1.55 0.01 2.44 +0.01 0.01 TMO‑Non TMO‑Non
SYN381^5 1.52 0.01 2.25 +0.01 TMO‑Non 0.01 TMO‑Non
SYO552^1 1.49 0.01 2.25 +0.02 0.01 GUP‑Non +0.03
SYO303^5 1.54 0.01 2.26 +0.01 0.01 GUP‑Non +21.65
SYO195^5 1.56 0.01 2.74 +0.01 0.01 GUP‑Non UNK‑Non
SEV088^5 1.56 0.01 2.23 +0.01 0.01 GUP‑Non TMO‑Non
SYO062^4.002 164.13 2.80 65.10 +0.01 11.94 TMO‑Non TMO‑Non
SYO377^5 1.48 0.01 3.11 TMO‑Non TMO‑Non 0.01 TMO‑Non
ALG267^2 43.97 3.60 52.84 TMO‑Non 0.01 GUP‑Non +1.34
SEV048^5 1.54 0.01 2.25 +0.01 0.01 GUP‑Non UNK‑Non
SYO570^7 1.54 0.01 21.64 +0.01 0.01 TMO‑Non UNK‑Non
SYO298^5 1.57 0.01 4.86 +0.01 0.01 GUP‑Non UNK‑Non
SYO363^5 1.49 0.01 3.35 +0.01 0.01 GUP‑Non TMO‑Non
SEV056^5 97.26 0.04 2.25 +75.25 0.01 GUP‑Non UNK‑Non
SEU945^5 47.06 0.02 31.87 +0.01 0.01 GUP‑Non TMO‑Non
SYO300^5 1.54 0.01 2.79 TMO‑Non 0.01 GUP‑Non UNK‑Non
ALG260^1 5.68 9.37 78.74 +1.70 16.62 GUP‑Non +187.99
SEV256^5 1.62 0.01 18.60 +57.28 0.01 TMO‑Non UNK‑Non
SEV034^5 1.53 0.03 78.09 +0.01 3.22 0.03 TMO‑Non
CSR130^1 1.54 0.01 69.42 +0.01 TMO‑Non GUP‑Non UNK‑Non
SYO046^1 1.54 0.01 2.62 +0.01 0.01 TMO‑Non TMO‑Non
SEV246^5 TMO‑Non 37.52 63.44 TMO‑Non TMO‑Non 75.01 TMO‑Non
SYO194^5 1.50 0.01 18.08 +0.01 0.01 GUP‑Non +0.01
SYO180^5 3.48 0.01 2.77 +0.01 TMO‑Non 0.01 TMO‑Non
SEU602^2 1.54 0.01 8.25 TMO‑Non 0.01 GUP‑Non UNK‑Non
SEV086^5 1.48 0.01 176.83 +6.63 TMO‑Non GUP‑Non UNK‑Non
NUM926^1 TMO‑Non 14.75 66.26 TMO‑Non 12.83 35.98 TMO‑Non
SYO091^5 1.54 0.01 2.76 +0.01 TMO‑Non GUP‑Non TMO‑Non
SYO234^5 1.50 0.01 2.25 +0.01 0.01 GUP‑Non +0.02
CSR131^1 162.71 9.44 69.20 +76.35 TMO‑Non GUP‑Non UNK‑Non
SEU619^1 8.91 0.01 26.90 TMO‑Non 0.01 4.41 TMO‑Non
SYO018^1 1.52 0.01 3.62 +0.01 0.02 TMO‑Non UNK‑Non
LCL707^1 1.48 0.01 2.60 +0.01 TMO‑Non TMO‑Non TMO‑Non
SYO364^5 1.49 0.01 128.27 +0.01 75.26 GUP‑Non TMO‑Non
SEU517^2 1.53 0.01 78.12 TMO‑Non 0.01 GUP‑Non +0.03
SYO288^5 1.46 4.67 TMO‑Non TMO‑Non 0.01 GUP‑Non +0.02
SYO450^4 1.53 0.01 50.34 +0.04 8.63 TMO‑Non TMO‑Non
SYO263^5 1.56 0.01 48.68 +4.92 TMO‑Non GUP‑Non +1.38
SEU644^1 4.14 132.40 89.37 +2.54 TMO‑Non 0.04 TMO‑Non
SYN996^1 1.48 4.48 3.66 +0.01 0.01 GUP‑Non +0.02
SYO057^2 2.17 0.01 3.50 +0.01 0.01 TMO‑Non UNK‑Non
SYO559^1 1.48 0.01 2.76 +89.65 57.96 TMO‑Non UNK‑Non
SEV303^5 25.99 0.01 20.93 TMO‑Non 84.07 0.01 +21.05
SYO374^5 1.54 0.01 30.41 +0.01 0.02 GUP‑Non UNK‑Non
SEV191^5 12.25 0.02 2.42 +0.01 TMO‑Non 25.02 TMO‑Non
SEV218^5 1.55 2.68 2.27 +0.01 TMO‑Non 0.02 TMO‑Non
CSR123^2 TMO‑Non UNK‑Non 78.63 +0.01 0.01 0.03 TMO‑Non
SYO391^5 1.54 12.33 79.64 +1.44 TMO‑Non 75.09 TMO‑Non
SYO350^5 1.54 0.01 3.43 +0.01 0.01 GUP‑Non +0.03
SYO272^5 TMO‑Non UNK‑Non 2.26 TMO‑Non 0.01 TMO‑Non UNK‑Non
SEU613^2 6.77 0.01 2.31 TMO‑Non 0.01 GUP‑Non UNK‑Non
SEV082^5 TMO‑Non 0.03 18.21 +1.03 TMO‑Non TMO‑Non UNK‑Non
SEU792^2 1.55 80.38 18.08 +0.01 TMO‑Non 0.01 TMO‑Non
SYO169^5 12.92 50.48 63.69 +0.01 TMO‑Non 0.03 UNK‑Non
SYN357^7 1.51 0.01 17.86 +0.02 0.01 TMO‑Non +17.83
SYO387^5 1.60 6.57 77.55 +0.01 TMO‑Non 75.04 TMO‑Non
SET623^3 1.54 0.01 2.42 +0.01 TMO‑Non GUP‑Non TMO‑Non
SYO311^5 5.92 9.47 3.09 +0.01 TMO‑Non TMO‑Non UNK‑Non
SYO372^5 1.53 0.01 2.80 +0.01 0.01 GUP‑Non TMO‑Non
SEV083^5 TMO‑Non 0.01 4.83 +1.04 TMO‑Non TMO‑Non UNK‑Non
SEU673^2 1.47 0.01 17.71 TMO‑Non 0.01 GUP‑Non UNK‑Non
SYO527^1 1.54 0.01 3.68 +0.01 0.01 GUP‑Non +0.03
SYO460^1 1.49 0.01 2.61 +0.06 0.01 TMO‑Non TMO‑Non
SEV382^5 1.50 0.01 18.73 +0.01 TMO‑Non GUP‑Non UNK‑Non
SEU776^2 1.57 0.01 2.24 TMO‑Non 0.01 GUP‑Non +0.02
SEV164^5 1.54 0.01 2.24 +0.02 TMO‑Non GUP‑Non UNK‑Non
SYN393^4.002 1.60 0.01 17.82 +75.73 0.01 GUP‑Non UNK‑Non
SYO026^1 1.50 0.01 2.75 +0.02 TMO‑Non TMO‑Non UNK‑Non
LCL632^1 6.04 11.21 29.00 +66.89 0.01 TMO‑Non TMO‑Non
SYO388^5 1.53 6.59 76.81 +0.01 TMO‑Non 75.11 TMO‑Non
SYO397^1 1.53 0.01 2.41 +0.02 0.01 TMO‑Non TMO‑Non
SYO287^5 1.53 4.68 TMO‑Non TMO‑Non 0.01 GUP‑Non +0.03
SYN978^4 1.55 0.01 17.70 +0.01 0.01 GUP‑Non UNK‑Non
SYO324^5 1.53 0.01 20.30 +26.02 TMO‑Non 0.01 UNK‑Non
PHI003^2* 1.53 0.01 2.48 +0.01 0.01 UNK‑Non +0.03
SEV091^5 1.54 0.01 78.10 +0.01 TMO‑Non 0.01 TMO‑Non
PUZ140^1* 55.12 16.62 5.43 +0.01 0.01 GUP‑Non TMO‑Non
SYO317^5 TMO‑Non UNK‑Non 67.74 +0.01 0.01 GUP‑Non UNK‑Non
PHI002^2* 16.14 0.01 4.95 +0.01 0.02 TMO‑Non UNK‑Non
SEV148^5 2.39 0.01 71.80 TMO‑Non 145.50 TMO‑Non TMO‑Non
SEV222^5 1.54 6.98 19.12 +75.24 TMO‑Non GUP‑Non TMO‑Non
SYO332^5 TMO‑Non 16.62 TMO‑Non UNK‑Non 0.01 GUP‑Non TMO‑Non
SEV212^5 1.52 18.95 78.26 TMO‑Non 7.24 TMO‑Non TMO‑Non
SEV085^5 TMO‑Non UNK‑Non 162.71 TMO‑Non TMO‑Non GUP‑Non UNK‑Non
SYO443^1 1.53 0.01 18.05 +0.01 0.01 TMO‑Non TMO‑Non
SEV153^5 163.44 25.00 54.74 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SEU687^2 1.52 4.77 18.63 TMO‑Non TMO‑Non 0.01 TMO‑Non
GRA027^1 TMO‑Non 6.52 12.14 TMO‑Non TMO‑Non GUP‑Non TMO‑Non
NUM686^1 113.69 UNK‑Non 19.39 TMO‑Non 1.05 GUP‑Non TMO‑Non
SEV246^6 10.56 37.85 63.36 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
ALG017^7 9.85 3.32 63.81 TMO‑Non TMO‑Non 217.61 TMO‑Non
SYO173^5 1.55 UNK‑Non 20.42 +0.01 TMO‑Non 0.02 UNK‑Non
SEU653^2 1.54 UNK‑Non 78.13 +0.01 TMO‑Non 0.05 TMO‑Non
SEV400^5 1.53 6.68 TMO‑Non TMO‑Non TMO‑Non GUP‑Non UNK‑Non
SET598^5 3.02 3.52 TMO‑Non +0.01 0.01 GUP‑Non TMO‑Non
SYO376^5 1.48 0.01 2.74 +0.01 TMO‑Non GUP‑Non UNK‑Non
SEV261^5 2.29 15.65 2.25 +0.02 TMO‑Non TMO‑Non TMO‑Non
SEV243^5 17.93 11.06 63.36 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SEU603^1 1.58 1.02 153.84 TMO‑Non 0.01 GUP‑Non TMO‑Non
SEV156^5 1.87 0.01 78.59 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR139^2 72.56 UNK‑Non 19.79 +4.12 0.01 GUP‑Non TMO‑Non
SYO560^1 1.56 0.01 2.75 +100.03 TMO‑Non GUP‑Non UNK‑Non
SEV006^5 1.54 0.04 32.88 +0.01 TMO‑Non 10.84 TMO‑Non
SYO174^5 1.54 9.82 7.36 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GEG011^1 1.54 4.31 79.05 +0.02 TMO‑Non GUP‑Non TMO‑Non
SYO310^5 1.55 0.05 2.74 +0.01 TMO‑Non TMO‑Non UNK‑Non
ALG268^2 43.70 58.65 86.57 +1.34 TMO‑Non GUP‑Non TMO‑Non
SYO309^5 TMO‑Non UNK‑Non TMO‑Non +54.23 0.01 GUP‑Non +0.02
SEV129^5 1.56 38.65 79.21 +0.18 0.01 TMO‑Non TMO‑Non
SYN036^5 1.55 0.01 2.25 +0.01 TMO‑Non GUP‑Non TMO‑Non
SYO064^4.001 1.53 0.01 17.80 +0.01 TMO‑Non TMO‑Non UNK‑Non
SEV072^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non 0.02 GUP‑Non +1.44
CSR143^2 242.59 6.02 79.24 TMO‑Non TMO‑Non 8.59 TMO‑Non
SEV084^5 TMO‑Non 0.01 18.17 +2.86 TMO‑Non GUP‑Non UNK‑Non
SEU723^1 1.70 UNK‑Non 88.31 TMO‑Non 9.33 1.73 TMO‑Non
SEU960^5 1.53 0.02 TMO‑Non TMO‑Non 0.01 GUP‑Non +2.54
SYO067^4.001 20.88 3.63 100.04 +0.01 0.01 GUP‑Non UNK‑Non
SEV066^5 1.50 6.54 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
ALG294^5 1.53 0.01 149.07 TMO‑Non TMO‑Non 5.72 TMO‑Non
SEV155^5 1.55 0.01 78.22 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SEU696^2 1.54 0.01 2.30 TMO‑Non 1.44 GUP‑Non +8.65
SEV064^5 1.54 6.53 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GRP001^5 1.59 UNK‑Non 2.99 +0.01 TMO‑Non 0.01 TMO‑Non
SEV071^5 TMO‑Non UNK‑Non 3.11 TMO‑Non TMO‑Non GUP‑Non +1.53
SYO248^5 136.10 0.01 60.91 56.19 TMO‑Non 0.01 TMO‑Non
SEV312^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SET557^1 1.52 3.24 TMO‑Non +0.02 10.43 GUP‑Non TMO‑Non
SEV305^6 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEU735^1 28.12 1.48 86.63 +17.03 TMO‑Non 0.04 TMO‑Non
SEU939^5 1.64 UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEU621^1 22.25 UNK‑Non 88.65 TMO‑Non 83.97 18.09 TMO‑Non
SEV165^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
CSR119^2 TMO‑Non UNK‑Non 206.15 +0.01 TMO‑Non 0.02 TMO‑Non
SEV069^6 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR138^2 TMO‑Non UNK‑Non 82.39 +0.01 0.01 GUP‑Non TMO‑Non
SEV050^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non +0.03
ALG274^5 39.54 UNK‑Non 69.31 +0.01 TMO‑Non 283.86 TMO‑Non
SEV101^5 1.52 6.52 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEU675^2 1.53 0.01 2.03 TMO‑Non TMO‑Non GUP‑Non +0.02
SYO329^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEV432^1 172.39 0.01 3.65 +0.01 0.01 GUP‑Non +0.04
LCL729^5 TMO‑Non UNK‑Non TMO‑Non UNK‑Non 0.01 GUP‑Non TMO‑Non
SYO535^1 1.52 0.01 63.67 +0.01 0.01 GUP‑Non UNK‑Non
SYO548^1 1.53 0.01 TMO‑Non TMO‑Non TMO‑Non GUP‑Non +0.03
SEU807^2 1.98 UNK‑Non 18.32 +0.01 TMO‑Non 25.03 UNK‑Non
SEU940^5 TMO‑Non 18.14 TMO‑Non TMO‑Non TMO‑Non GUP‑Non UNK‑Non
SEU618^1 17.74 UNK‑Non 85.72 TMO‑Non 23.35 0.14 TMO‑Non
SYO533^1 TMO‑Non UNK‑Non TMO‑Non TMO‑Non 0.01 GUP‑Non UNK‑Non
SEU788^2 21.12 10.44 59.71 TMO‑Non TMO‑Non 36.12 TMO‑Non
MSC021^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non UNK‑Non
SEU794^2 TMO‑Non 11.01 18.35 TMO‑Non TMO‑Non 78.87 TMO‑Non
SEV068^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
ALG277^5 3.30 UNK‑Non 2.99 +0.01 TMO‑Non 25.03 TMO‑Non
SYO269^5 1.49 UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEU602^1 1.54 0.01 74.81 TMO‑Non 0.03 GUP‑Non TMO‑Non
SEU818^1 1.59 4.52 87.26 TMO‑Non TMO‑Non 3.70 TMO‑Non
CSR153^2 TMO‑Non UNK‑Non 254.05 +0.01 0.01 GUP‑Non TMO‑Non
NUM926^3 2.68 6.42 88.94 TMO‑Non TMO‑Non GUP‑Non UNK‑Non
LCL631^1 TMO‑Non UNK‑Non 23.94 +29.81 0.01 TMO‑Non TMO‑Non
ALG278^5 3.28 UNK‑Non 2.98 +0.01 TMO‑Non 25.03 TMO‑Non
SEV141^5 TMO‑Non 3.71 TMO‑Non UNK‑Non 12.24 TMO‑Non TMO‑Non
SEU753^2 4.63 2.81 18.32 TMO‑Non TMO‑Non 25.03 TMO‑Non
SEU591^1 1.55 0.01 88.12 TMO‑Non 0.01 GUP‑Non TMO‑Non
NUM651^1 2.01 UNK‑Non 18.23 +0.01 TMO‑Non 0.02 TMO‑Non
SET575^7 5.14 6.82 17.94 TMO‑Non 0.01 TMO‑Non TMO‑Non
SYO538^1 1.53 0.01 63.89 +0.01 0.01 TMO‑Non TMO‑Non
CSR141^2 TMO‑Non UNK‑Non 184.54 +0.02 TMO‑Non 0.02 TMO‑Non
ALG285^5 TMO‑Non UNK‑Non 34.32 +0.01 TMO‑Non 0.01 TMO‑Non
SCT171^2 12.79 0.01 23.76 TMO‑Non 0.01 GUP‑Non +7.53
PHI004^2* 1.65 0.01 29.79 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
PHI005^2* 1.64 3.31 33.17 +0.01 TMO‑Non UNK‑Non UNK‑Non
SEV158^5 1.51 0.20 176.72 +9.27 TMO‑Non GUP‑Non TMO‑Non
ALG273^5 TMO‑Non UNK‑Non 72.74 +0.01 TMO‑Non GUP‑Non TMO‑Non
SYO542^1 1.53 0.01 63.83 +2.14 TMO‑Non GUP‑Non TMO‑Non
SEU671^2 1.53 0.01 22.44 TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEU701^2 1.56 16.92 18.32 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM810^5 1.49 0.01 TMO‑Non TMO‑Non 0.01 GUP‑Non UNK‑Non
SWW473^3 TMO‑Non UNK‑Non 88.01 TMO‑Non TMO‑Non 6.59 TMO‑Non
ALG268^3 TMO‑Non TMO‑Non 165.78 +1.32 TMO‑Non GUP‑Non TMO‑Non
SEU998^5 83.23 UNK‑Non 3.74 +0.41 TMO‑Non 0.02 TMO‑Non
SYO249^5 TMO‑Non UNK‑Non 27.49 +0.02 TMO‑Non 25.32 TMO‑Non
SYO543^1 1.49 0.01 63.78 +0.61 TMO‑Non GUP‑Non TMO‑Non
LCL694^1 13.61 0.01 TMO‑Non +0.04 0.01 TMO‑Non UNK‑Non
SEU997^5 47.72 UNK‑Non 50.44 +0.01 TMO‑Non 17.42 TMO‑Non
SEU969^5 16.79 14.29 TMO‑Non TMO‑Non 0.01 TMO‑Non TMO‑Non
SWW478^2 1.62 0.01 20.24 +35.28 TMO‑Non UNK‑Non +2.75
SYO442^1 1.56 0.01 78.20 +0.01 245.53 TMO‑Non TMO‑Non
SWW473^2 44.58 UNK‑Non 83.79 UNK‑Non TMO‑Non 2.12 TMO‑Non
SEU764^1 TMO‑Non UNK‑Non 87.33 TMO‑Non TMO‑Non 72.94 TMO‑Non
SEU999^5 1.53 UNK‑Non 3.73 +0.01 TMO‑Non 0.01 TMO‑Non
SEU486^1 2.79 0.01 TMO‑Non TMO‑Non 0.01 27.92 TMO‑Non
SEV171^5 6.09 0.01 TMO‑Non TMO‑Non 0.01 GUP‑Non TMO‑Non
SYN741^7 1.61 0.01 65.47 +0.01 TMO‑Non GUP‑Non TMO‑Non
SYO066^4.002 2.88 1.22 116.36 +0.05 TMO‑Non GUP‑Non TMO‑Non
SYN397^7 4.04 0.01 78.38 +1.23 TMO‑Non TMO‑Non TMO‑Non
SEU968^5 TMO‑Non 0.01 TMO‑Non TMO‑Non 0.01 GUP‑Non +11.75
NUM808^5 1.51 0.01 TMO‑Non TMO‑Non 0.01 GUP‑Non UNK‑Non
SEV295^5 162.93 5.41 TMO‑Non TMO‑Non 0.01 TMO‑Non TMO‑Non
ALG276^5 TMO‑Non UNK‑Non 101.02 +0.01 TMO‑Non TMO‑Non TMO‑Non
SYO068^4.010 166.94 0.01 78.33 +0.01 TMO‑Non GUP‑Non UNK‑Non
PHI002^1* 1.56 0.01 TMO‑Non +0.01 0.01 TMO‑Non UNK‑Non
CSR150^3 177.67 UNK‑Non TMO‑Non 79.25 0.01 37.62 TMO‑Non
CSR132^1 219.27 81.73 TMO‑Non +4.21 TMO‑Non GUP‑Non TMO‑Non
SEV005^5 TMO‑Non UNK‑Non 50.95 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM021^1 TMO‑Non 199.55 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEV192^5 201.91 5.60 TMO‑Non TMO‑Non 11.46 TMO‑Non TMO‑Non
SEU869^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SEU867^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SYO516^1 86.03 UNK‑Non 48.95 +0.01 0.01 GUP‑Non TMO‑Non
PLA033^7 1.53 35.72 TMO‑Non +0.01 TMO‑Non TMO‑Non TMO‑Non
SWV431^2 1.52 0.03 TMO‑Non +0.01 0.01 TMO‑Non UNK‑Non
SEV041^5 TMO‑Non UNK‑Non 132.57 +8.01 TMO‑Non TMO‑Non TMO‑Non
NUM811^5 209.53 UNK‑Non TMO‑Non TMO‑Non 0.01 GUP‑Non UNK‑Non
CSR131^2 TMO‑Non UNK‑Non 78.46 +57.91 TMO‑Non GUP‑Non TMO‑Non
SEV249^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
AGT030^1 273.92 8.94 TMO‑Non +0.01 TMO‑Non GUP‑Non TMO‑Non
SWV441^1 3.42 1.04 TMO‑Non +0.01 1.22 GUP‑Non TMO‑Non
SWV426^2 1.55 0.01 TMO‑Non +0.02 20.03 TMO‑Non UNK‑Non
LCL874^1 3.12 UNK‑Non TMO‑Non +0.01 29.34 TMO‑Non TMO‑Non
SEU929^5 71.14 23.19 TMO‑Non TMO‑Non 0.01 GUP‑Non +6.85
AGT027^2 TMO‑Non UNK‑Non 42.91 +0.01 TMO‑Non TMO‑Non TMO‑Non
SYO532^1 TMO‑Non UNK‑Non TMO‑Non TMO‑Non 0.01 GUP‑Non UNK‑Non
COM024^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non 20.32 GUP‑Non TMO‑Non
SEV431^1 15.10 11.02 TMO‑Non TMO‑Non 0.01 GUP‑Non TMO‑Non
SYO213^5 TMO‑Non 9.45 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
CSR152^3 1.55 9.83 TMO‑Non 94.35 TMO‑Non 40.51 TMO‑Non
SEV087^5 TMO‑Non 0.01 TMO‑Non +73.75 TMO‑Non TMO‑Non TMO‑Non
CSR133^1 TMO‑Non 52.13 266.68 TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SYO208^5 1.58 3.23 TMO‑Non TMO‑Non 273.95 GUP‑Non TMO‑Non
SWV446^1 4.63 0.01 TMO‑Non +4.02 25.03 GUP‑Non UNK‑Non
GEG009^1 3.39 5.01 TMO‑Non +0.01 TMO‑Non TMO‑Non UNK‑Non
PHI003^1* 232.51 20.94 TMO‑Non +0.01 2.34 TMO‑Non UNK‑Non
PHI004^1* 175.94 11.08 TMO‑Non +30.50 TMO‑Non TMO‑Non TMO‑Non
SEU686^1 289.39 3.40 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SET914^7 TMO‑Non UNK‑Non TMO‑Non +0.01 TMO‑Non TMO‑Non TMO‑Non
CSR148^3 1.62 UNK‑Non TMO‑Non 89.15 TMO‑Non 34.38 TMO‑Non
SEU613^1 181.38 3.20 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
ALG269^1 TMO‑Non 1.62 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEV309^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SEU707^1 2.06 1.58 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
NUM800^1 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SYO239^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non 0.02 GUP‑Non +0.02
SEV010^5 TMO‑Non UNK‑Non TMO‑Non +0.01 TMO‑Non TMO‑Non TMO‑Non
SEU957^5 TMO‑Non UNK‑Non TMO‑Non +0.01 1.11 GUP‑Non TMO‑Non
SEU951^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non 7.43 GUP‑Non TMO‑Non
NUM925^4 TMO‑Non 55.72 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
SEU715^1 14.39 UNK‑Non TMO‑Non TMO‑Non TMO‑Non 35.50 TMO‑Non
SEU915^5 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SYO546^1 2.04 0.02 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
ALG269^2 43.94 0.01 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SYO066^4.003 TMO‑Non 99.32 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SYO544^1 1.58 10.26 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
SYO545^1 1.53 0.01 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
SYO063^4 22.74 2.21 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
Solved/400 333/400 324/400 316/400 269/400 236/400 96/400 74/400
Av. CPU Time 18.88 5.68 38.91 7.21 5.83 25.89 4.65
Solutions 0/400 0/400 0/400 265/400 0/400 0/400 74/400
μEfficiency 313 576 113 554 499 130 139
SOTAC 0.24 0.25 0.23 0.23 0.24 0.23 0.21
Core Usage 1.00 0.99 0.97 0.99 1.00 1.00 0.99
New Solved 8/8 8/8 5/8 7/8 5/8 0/8 1/8
* indicates a problem not previously seen by the systems. + indicates a solution was output by the system.


Results for: THF TFA FOF FNT EPR UEQ TNE TEQ TFI TFR TFE FNE FEQ FNN FNQ EPT EPS UEQ

Results for TFA (Typed First-order Theorems +*-/)

Typed First-order Theorems +*-/ CVC4
 1.4‑TFA
Princess
 140704
SPASS+T
 2.2.19
SPASS+T
 2.2.20
Beagle
 0.9
Zipperposition
 0.4‑TFF
ARI407=1 0.01 11.26 +1.09 +1.08 0.02 UNK‑Non
DAT071=1* 0.01 2.41 +1.17 +1.18 2.50 +7.95
ARI287=1 0.03 2.04 +1.05 +1.06 0.04 UNK‑Non
NUM912=1 0.01 2.14 +1.11 +1.10 1.26 UNK‑Non
DAT083=1* 0.01 2.13 +1.05 +1.11 1.88 +0.01
ARI309=1 0.01 1.64 +1.11 +1.08 0.99 UNK‑Non
NUM914=1 0.01 2.15 +1.11 +1.10 0.01 UNK‑Non
DAT082=1* 0.01 2.21 +1.07 +1.15 1.67 +0.01
ARI256=1 0.01 2.45 +1.08 +1.08 0.01 UNK‑Non
ARI426=1 0.01 1.97 +1.09 +1.09 0.01 UNK‑Non
DAT044=1 0.01 2.25 +1.11 +1.08 2.45 +0.01
ARI285=1 0.01 1.97 +1.11 +1.12 0.01 UNK‑Non
ARI489=1 0.01 2.50 +1.11 +1.10 0.01 UNK‑Non
ARI067=1 0.01 0.01 +1.11 +1.10 0.01 +0.01
ARI284=1 0.01 1.95 +1.09 +1.10 0.01 UNK‑Non
ARI402=1 0.01 1.95 +1.12 +1.09 0.01 UNK‑Non
ARI069=1 0.01 0.02 +1.11 +1.09 0.01 +0.01
ARI273=1 0.01 1.95 +1.07 +1.11 0.98 UNK‑Non
ARI406=1 0.01 11.74 +1.08 +1.11 0.01 UNK‑Non
ARI098=1 0.01 0.01 +1.10 +1.09 0.02 +0.01
ARI262=1 0.01 1.97 +1.08 +1.10 0.02 UNK‑Non
ARI447=1 0.01 2.50 +1.11 +1.10 1.00 UNK‑Non
GEG021=1 0.01 1.93 +1.09 +1.09 1.51 +0.01
NUM904=1 0.01 2.06 +1.11 +1.10 0.01 UNK‑Non
ARI420=1 0.02 11.81 +1.09 +1.08 0.01 UNK‑Non
ARI097=1 0.01 0.01 +1.08 +1.08 0.01 +0.01
ARI274=1 0.01 1.95 +1.09 +1.09 0.01 UNK‑Non
ARI462=1 0.01 1.68 +1.10 +1.10 0.01 UNK‑Non
ARI129=1 0.01 0.02 +1.09 +1.08 0.01 +0.01
ARI295=1 0.01 2.29 +1.08 +1.07 0.01 UNK‑Non
ARI445=1 0.01 2.57 +1.10 +1.10 0.01 UNK‑Non
SWW015=1 4.84 21.58 +11.51 +11.46 22.55 TMO‑Non
ARI312=1 0.01 1.67 +1.10 +1.11 0.02 UNK‑Non
ARI433=1 0.01 2.04 +1.10 +1.09 0.98 UNK‑Non
NUM891=1 0.01 0.01 +1.09 +1.11 0.98 +0.01
ARI289=1 0.01 1.94 +1.10 +1.09 0.01 UNK‑Non
NUM909=1 0.01 4.66 +1.09 +1.09 1.27 UNK‑Non
DAT021=1 0.01 2.18 +1.10 +1.10 1.87 +0.14
ARI247=1 0.01 1.90 +1.09 +1.10 0.01 UNK‑Non
ARI449=1 0.01 3.56 +1.09 +1.09 0.01 UNK‑Non
DAT058=1 0.02 3.85 +1.09 +1.10 2.02 +0.05
ARI249=1 0.01 1.92 +1.09 +1.06 0.01 UNK‑Non
ARI440=1 0.01 1.97 +1.10 +1.10 0.01 UNK‑Non
ARI066=1 0.01 0.02 +1.10 +1.09 0.98 +0.01
ARI277=1 0.01 1.91 +1.11 +1.10 0.01 UNK‑Non
ARI410=1 0.01 25.66 +1.11 +1.10 1.25 UNK‑Non
DAT045=1 0.01 2.26 +1.09 +1.10 2.36 +0.01
ARI252=1 0.01 1.92 +1.09 +1.09 0.01 UNK‑Non
ARI424=1 0.01 2.06 +1.10 +1.10 0.01 UNK‑Non
SWW049=1 8.03 44.34 +15.52 +15.43 21.49 TMO‑Non
ARI264=1 0.01 2.38 +1.10 +1.12 0.01 UNK‑Non
NUM913=1 0.01 2.32 +1.10 +1.09 1.38 UNK‑Non
DAT004=1 0.01 1.59 +1.10 +1.10 1.49 +0.05
ARI288=1 0.01 1.94 +1.09 +1.08 0.01 UNK‑Non
ARI448=1 0.01 3.13 +1.09 +1.10 1.26 UNK‑Non
SWW082=1 30.03 43.28 +19.71 +19.87 21.92 TMO‑Non
NUM901=1 0.01 3.95 +1.10 +1.10 0.02 UNK‑Non
ARI464=1 0.01 1.65 +1.10 +1.10 0.01 UNK‑Non
ARI542=1 0.01 0.01 +1.10 +1.10 0.01 +0.01
ARI286=1 0.01 1.97 +1.07 +1.09 0.01 UNK‑Non
ARI411=1 0.01 25.61 +1.08 +1.06 0.02 UNK‑Non
DAT060=1 0.01 1.79 +1.09 +1.08 1.65 +0.01
ARI296=1 0.01 2.49 +1.09 +1.07 0.01 UNK‑Non
ARI442=1 0.02 1.65 +1.09 +1.10 0.97 UNK‑Non
ARI133=1 0.01 0.01 +1.10 +1.06 0.01 +0.01
NUM907=1 0.01 11.22 +1.09 +1.09 1.70 UNK‑Non
ARI568=1 0.01 1.95 +1.10 +1.07 0.01 UNK‑Non
DAT084=1* 0.01 2.20 +1.08 +1.14 1.91 +0.01
ARI257=1 0.01 2.38 +1.09 +1.08 0.01 UNK‑Non
ARI421=1 0.01 12.01 +1.10 +1.10 0.01 UNK‑Non
DAT088=1* 0.01 5.46 +1.09 +1.18 4.22 +0.06
NUM906=1 0.01 2.28 +1.10 +1.10 1.27 UNK‑Non
ARI436=1 0.02 1.96 +1.09 +1.11 0.01 UNK‑Non
DAT099=1* 0.02 1.83 +1.11 +1.10 1.75 +0.04
ARI266=1 0.01 2.50 +1.08 +1.10 0.02 UNK‑Non
ARI565=1 0.02 2.24 +1.09 +1.11 0.01 UNK‑Non
DAT080=1* 0.01 2.31 +4.39 +4.37 10.14 +2.65
NUM903=1 0.01 2.17 +1.10 +1.09 0.01 UNK‑Non
ARI457=1 0.01 24.86 +1.09 +1.08 0.01 UNK‑Non
DAT098=1* 0.02 1.83 +1.09 +1.07 1.63 +0.01
ARI263=1 0.01 1.65 +1.08 +1.10 0.01 UNK‑Non
ARI458=1 0.01 24.88 +1.08 +1.09 0.01 UNK‑Non
SWW619=2* UNK‑Non 143.54 UNK‑Non UNK‑Non TMO‑Non +0.75
ARI241=1 0.01 2.03 +1.07 +1.10 0.01 UNK‑Non
ARI430=1 0.01 2.49 +1.10 +1.09 0.01 UNK‑Non
DAT087=1* 0.01 6.91 +1.12 +1.08 1.90 +0.04
ARI214=1 0.01 2.04 +1.09 +1.06 0.01 UNK‑Non
ARI414=1 0.01 1.96 +1.06 +1.08 0.01 UNK‑Non
DAT093=1* 0.01 3.47 +1.11 +1.08 2.27 +0.01
ARI558=1 0.01 2.81 +1.09 +1.09 0.01 UNK‑Non
ARI619=3 0.01 TMO‑Non +1.08 +1.05 3.24 UNK‑Non
DAT102=1* 0.01 8.43 +1.09 +1.09 1.61 +0.26
ARI208=1 0.01 2.05 +1.10 +1.09 0.01 UNK‑Non
ARI413=1 0.01 2.00 +1.10 +1.10 0.01 UNK‑Non
SWW046=1 30.02 42.18 +16.59 +16.66 22.59 TMO‑Non
ARI235=1 0.01 2.04 +1.10 +1.10 1.09 UNK‑Non
ARI566=1 0.01 27.63 +1.08 +1.11 1.11 UNK‑Non
SWW055=1 7.03 41.72 +23.20 +24.59 23.55 TMO‑Non
ARI342=1 0.01 9.00 +1.10 +1.10 0.02 UNK‑Non
ARI415=1 0.01 1.78 +1.03 +1.11 0.01 UNK‑Non
SWW061=1 30.02 43.11 +21.57 +22.86 23.32 TMO‑Non
ARI206=1 0.01 2.17 +1.08 +1.13 0.01 UNK‑Non
ARI459=1 0.01 1.67 +1.09 +1.11 0.01 UNK‑Non
SWW068=1 30.02 42.33 +25.54 +28.40 24.52 TMO‑Non
ARI216=1 0.01 2.17 +1.09 +1.08 0.01 UNK‑Non
ARI423=1 0.01 5.99 +1.10 +1.09 0.01 UNK‑Non
DAT007=1 0.01 2.44 +1.10 +1.08 1.52 +0.01
ARI202=1 0.01 2.18 +1.10 +1.11 0.01 UNK‑Non
ARI460=1 0.01 1.65 +1.11 +1.12 0.01 UNK‑Non
ARI093=1 0.01 0.02 +1.11 +1.10 0.96 +0.01
ARI242=1 0.01 2.16 +1.08 +1.09 0.01 UNK‑Non
ARI621=3 0.01 TMO‑Non +1.09 +1.10 4.66 UNK‑Non
DAT009=1 0.01 1.58 +1.09 +1.10 1.51 +0.05
NUM902=1 0.01 4.67 +1.10 +1.09 0.01 UNK‑Non
ARI452=1 0.01 1.99 +1.10 +1.09 0.01 UNK‑Non
SWW042=1 6.34 21.17 +32.32 +34.06 23.64 TMO‑Non
ARI268=1 0.01 11.82 +1.10 +1.09 0.01 UNK‑Non
ARI450=1 0.01 1.97 +1.10 +1.09 0.01 UNK‑Non
DAT006=1 0.01 2.43 +1.10 +1.10 1.50 +0.01
ARI269=1 0.01 11.62 +1.08 +1.10 0.01 UNK‑Non
ARI454=1 0.01 1.96 +1.09 +1.07 0.01 UNK‑Non
ARI061=1 0.01 0.01 +1.10 +1.08 0.01 +0.01
ARI272=1 0.01 2.04 +1.11 +1.09 0.01 UNK‑Non
ARI355=1 0.02 2.06 +1.10 +1.11 0.01 UNK‑Non
DAT039=1 0.01 8.03 +1.09 +1.08 11.43 TMO‑Non
ARI281=1 0.01 2.02 +1.10 +1.08 0.01 UNK‑Non
ARI349=1 0.01 2.34 +1.09 +1.08 0.03 UNK‑Non
SYO523=1 0.01 1.37 +1.11 +1.11 1.46 +0.01
ARI245=1 0.01 1.84 +1.10 +1.10 0.02 UNK‑Non
ARI383=1 0.01 2.22 +1.09 +1.09 0.01 UNK‑Non
SWW620=2* UNK‑Non 6.13 UNK‑Non UNK‑Non TMO‑Non +11.44
NUM905=1 0.01 2.17 +1.10 +1.10 1.26 UNK‑Non
ARI376=1 0.01 2.22 +1.09 +1.09 0.01 UNK‑Non
DAT085=1* 80.03 TMO‑Non +36.87 +36.75 13.89 +13.45
ARI195=1 0.02 2.05 +1.09 +1.10 0.02 UNK‑Non
ARI356=1 0.01 2.21 +1.10 +1.08 0.99 UNK‑Non
DAT100=1* 0.01 1.95 +1.11 +1.09 3.10 +0.06
ARI201=1 0.01 2.18 +1.10 +1.10 0.01 UNK‑Non
ARI350=1 0.01 2.04 +1.07 +1.08 0.01 UNK‑Non
DAT072=1* 0.01 TMO‑Non +7.96 +7.96 186.14 TMO‑Non
ARI341=1 0.01 3.66 +1.11 +1.10 0.01 UNK‑Non
ARI519=1 0.01 2.22 UNK‑Non UNK‑Non 0.97 UNK‑Non
DAT103=1* 0.01 1.69 +1.09 +1.08 1.74 +0.66
ARI619=2 0.01 TMO‑Non +1.11 +1.09 3.47 UNK‑Non
MSC023=2 0.01 TMO‑Non +1.09 +1.10 0.01 UNK‑Non
DAT076=1* 0.01 33.44 +1.10 +1.09 2.34 +0.01
ARI307=1 0.01 24.84 +1.09 +1.07 0.01 UNK‑Non
ARI536=1 UNK‑Non TMO‑Non UNK‑Non UNK‑Non 1.26 UNK‑Non
SWW666=2* 42.21 50.92 UNK‑Non UNK‑Non 28.06 +133.92
ARI337=1 0.01 9.00 +1.08 +1.10 0.01 UNK‑Non
DAT091=1* 80.02 TMO‑Non +1.16 +1.15 4.07 +0.03
DAT014=1 0.01 1.68 +1.10 +1.08 1.62 +0.01
DAT015=1 TMO‑Non 2.40 +1.08 +1.09 1.41 +0.01
NUM916=1 0.01 0.01 +1.09 +1.09 1.00 +0.01
DAT035=1 0.01 2.25 +1.12 +1.09 7.37 +0.25
DAT012=1 0.01 1.67 +1.08 +1.10 2.00 +0.34
DAT028=1 0.01 1.79 +1.16 +1.18 1.76 +0.01
ARI118=1 0.01 2.10 +1.09 +1.11 1.28 UNK‑Non
ARI056=1 0.01 0.01 +1.09 +1.09 0.01 +0.01
ARI163=1 0.01 1.08 +1.11 +1.09 0.01 +0.01
DAT024=1 0.01 1.79 +1.09 +1.10 1.52 +0.01
NUM917=1 0.01 0.01 +1.08 +1.09 0.01 +0.01
DAT027=1 0.01 1.90 +1.12 +1.10 1.87 +0.24
ARI603=1 TMO‑Non 1.60 +1.11 +1.05 TMO‑Non +0.01
DAT097=1* 0.01 29.77 +181.29 +195.73 48.94 +9.05
DAT106=1* 0.01 12.00 +15.55 +15.96 163.52 +0.04
DAT077=1* 0.01 2.35 +1.09 +1.08 2.23 +0.01
DAT105=1* TMO‑Non 9.03 +1.11 +1.08 1.73 +0.01
DAT095=1* 0.01 32.20 +1.19 +1.17 4.21 +0.04
GEG022=1 0.01 2.10 +1.11 +1.09 5.52 +0.06
SWW634=2* 3.62 91.14 UNK‑Non UNK‑Non TMO‑Non TMO‑Non
DAT074=1* TMO‑Non 102.76 +1.18 +1.16 2.76 +0.06
SWW598=2* 0.01 16.87 UNK‑Non UNK‑Non TMO‑Non TMO‑Non
DAT092=1* 109.95 27.37 +1.11 +1.10 1.89 +0.02
SWW622=2* 0.01 TMO‑Non UNK‑Non UNK‑Non TMO‑Non +12.17
DAT094=1* 81.03 TMO‑Non TMO‑Non TMO‑Non TMO‑Non +1.06
DAT101=1* 0.01 30.79 +1.09 +1.09 TMO‑Non +0.65
SWW621=2* UNK‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non +11.76
SWW628=2* 72.65 85.97 UNK‑Non UNK‑Non TMO‑Non +1.34
DAT089=1* 80.03 104.56 +1.17 +1.11 4.04 +0.05
SWW647=2* UNK‑Non 7.23 UNK‑Non UNK‑Non UNK‑Non +14.04
HWV047=1 3.83 TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
HWV044=1 4.03 TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
HWV051=1 1.94 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
HWV041=1 2.44 TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
NUM861=1 TMO‑Non 57.20 TMO‑Non TMO‑Non 7.67 +158.02
DAT104=1* TMO‑Non 18.61 +1.15 +1.09 TMO‑Non +0.06
SWW583=2* 0.01 TMO‑Non UNK‑Non UNK‑Non TMO‑Non +12.86
DAT075=1* 83.72 TMO‑Non TMO‑Non TMO‑Non 5.58 +11.86
DAT078=1* TMO‑Non 118.75 +1.19 +1.14 TMO‑Non +0.25
SWW648=2* UNK‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non +34.85
DAT073=1* TMO‑Non 36.14 +1.10 +1.09 161.17 +0.07
SWW630=2* UNK‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non +10.35
SWW606=2* UNK‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non +9.87
SWW607=2* UNK‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non +10.76
SWW596=2* UNK‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non +8.05
HWV093=1* 7.76 TMO‑Non +8.42 +8.73 UNK‑Non UNK‑Non
SWW601=2* UNK‑Non TMO‑Non UNK‑Non UNK‑Non UNK‑Non UNK‑Non
SWW589=2* UNK‑Non 193.18 UNK‑Non UNK‑Non TMO‑Non TMO‑Non
SWW656=2* UNK‑Non 39.81 UNK‑Non UNK‑Non TMO‑Non +45.84
Solved/200 179/200 176/200 173/200 173/200 173/200 80/200
Av. CPU Time 4.47 11.81 3.44 3.57 5.49 6.57
Solutions 0/200 0/200 173/200 173/200 0/200 80/200
μEfficiency 797 307 402 402 623 313
SOTAC 0.22 0.21 0.19 0.19 0.20 0.27
Core Usage 1.30 1.19 1.83 1.79 1.21 0.99
New Solved 33/50 35/50 30/50 30/50 28/50 44/50
* indicates a problem not previously seen by the systems. + indicates a solution was output by the system.


Results for: THF TFA FOF FNT EPR UEQ TNE TEQ TFI TFR TFE FNE FEQ FNN FNQ EPT EPS UEQ

Results for FOF (First-order Theorems)

First-order Theorems Vampire
 2.6
ET
 0.1
E
 1.9
VanHElsing
 1.0
CVC4
 1.4‑FOF
iProver
 1.4
leanCoP
 2.2
Prover9
 1109a
Zipperposition
 0.4‑FOF
Muscadet
 4.4
Princess
 140704
SET002+4 +4.34 +0.03 +0.01 +2.65 +0.01 +0.04 +0.03 TMO‑Non +6.10 +0.03 2.34
SYN549+1 +0.03 +0.02 +0.04 +2.64 +0.01 +0.02 +0.11 +0.08 +1.54 GUP‑Non TMO‑Non
CSR022+1 +0.02 +0.10 +0.05 +2.62 +0.03 +1.11 +245.91 +0.02 +0.14 +0.03 6.97
SWB009+3 +3.64 +0.02 +0.05 +2.63 +15.50 +10.43 +0.03 GUP‑Non +24.43 +10.33 14.56
NUM926+5 +0.02 +0.01 +0.01 +2.60 +0.01 +0.01 +1.10 +0.01 +0.42 TMO‑Non 33.54
KRS265+1 +0.01 +0.01 +0.01 +2.58 +68.24 +0.01 +0.01 +2.38 +2.06 TMO‑Non 82.20
SWV210+1 +0.01 +0.18 +0.01 +2.62 +0.01 +0.15 +0.01 +15.22 TMO‑Non +0.02 5.70
CSR035+3 +0.01 +12.17 +0.01 +2.75 +0.01 +1.23 +1.30 TMO‑Non TMO‑Non TMO‑Non 45.04
HAL003+3 +0.01 +6.10 +0.01 +2.61 +16.41 +0.02 +2.09 TMO‑Non TMO‑Non +0.01 4.55
CSR058+3 +0.01 +12.17 +0.01 +2.75 +0.01 +1.26 +1.29 TMO‑Non TMO‑Non UNK‑Non 44.69
SET776+4 +0.01 +0.01 +0.01 +7.48 +0.01 +0.02 TMO‑Non +25.80 TMO‑Non +0.01 10.82
SYN386+1 +0.01 +0.04 +0.01 +2.79 TMO‑Non +0.01 +0.01 +0.01 +0.01 TMO‑Non TMO‑Non
ALG167+1 +0.83 +1.94 +0.01 +3.68 +0.01 TMO‑Non TMO‑Non TMO‑Non +60.17 TMO‑Non 11.44
LCL638+1.005 +4.51 +1.21 +0.01 +9.73 TMO‑Non +40.83 +69.17 TMO‑Non +211.90 UNK‑Non 35.69
SYN551+2 +0.01 +0.01 +0.01 +2.60 +15.04 +3.82 +29.35 +221.69 +0.35 +0.42 26.86
KRS217+1 +0.01 +0.01 +46.64 +51.09 TMO‑Non +0.72 +109.74 +3.08 TMO‑Non TMO‑Non TMO‑Non
NUM327+1 +0.01 +0.01 +115.65 +105.30 +47.45 +85.77 +0.10 +6.89 TMO‑Non UNK‑Non TMO‑Non
SWV014+1 +0.01 +6.08 +0.01 +2.56 +0.01 +0.01 TMO‑Non GUP‑Non TMO‑Non TMO‑Non 145.01
ALG220+1 +0.02 +1.38 +0.01 +10.77 +0.01 +14.73 TMO‑Non +0.01 +147.75 TMO‑Non 8.68
CSR064+3 +0.02 +9.40 +2.00 +3.38 +3.54 +2.17 +1.42 TMO‑Non TMO‑Non +159.88 115.00
NUM924+6 +5.13 +1.88 +0.01 +2.79 +0.01 TMO‑Non +109.76 +4.73 TMO‑Non TMO‑Non 43.29
SWV437+1 +0.01 +0.01 +0.01 +2.62 TMO‑Non +0.03 +1.35 +0.02 +0.15 TMO‑Non TMO‑Non
LCL893+1 +0.01 +0.01 +0.01 +2.61 +45.04 +0.01 +25.95 UNK‑Non +0.06 +0.01 TMO‑Non
LCL658+1.001 +0.01 +4.21 +0.01 +8.31 TMO‑Non +4.93 TMO‑Non TMO‑Non +4.55 UNK‑Non 24.90
SWV377+1 +0.01 +6.06 +0.01 +2.64 +0.01 TMO‑Non +227.41 +0.01 +0.25 TMO‑Non 6.09
KRS260+1 +0.01 +0.01 +9.85 +12.43 TMO‑Non +0.01 +0.01 +0.01 TMO‑Non TMO‑Non 87.44
CSR017+1 +0.01 +0.01 +0.01 +2.63 +0.01 +0.02 TMO‑Non TMO‑Non +0.55 TMO‑Non 7.67
SYN548+1 +0.01 +154.19 +40.85 +3.00 +13.54 +1.14 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
MGT039+2 +6.05 +0.02 +0.01 +2.58 +0.01 +0.01 TMO‑Non +0.01 +0.05 +7.93 TMO‑Non
KRS202+1 +0.01 +0.03 +0.01 +2.62 TMO‑Non +0.01 +109.58 +0.01 TMO‑Non TMO‑Non 126.84
NUM924+1 +0.01 +0.01 +0.01 +2.61 +0.01 TMO‑Non TMO‑Non +0.01 +136.86 TMO‑Non 5.57
CSR113+6 +0.01 +0.74 +0.01 +3.79 +0.02 +1.06 +0.01 TMO‑Non TMO‑Non TMO‑Non 124.71
NUM924+2 +5.13 +1.59 +0.01 +2.65 +0.01 TMO‑Non +109.71 +3.36 TMO‑Non TMO‑Non 14.50
CSR054+3 +0.06 +11.83 +0.01 +2.76 +0.01 +1.25 +1.30 TMO‑Non TMO‑Non TMO‑Non 43.32
LCL529+1 +0.01 +0.01 +0.01 +2.62 +1.93 +10.10 +0.01 +0.01 +0.05 TMO‑Non 4.28
CSR032+3 +0.01 +10.67 +0.01 +2.99 +4.22 +1.27 +1.94 TMO‑Non TMO‑Non TMO‑Non 116.79
NUM925+2 +0.01 +1.79 +0.01 +2.66 +0.01 TMO‑Non +22.23 +1.26 +4.13 TMO‑Non 16.65
KRS215+1 +0.01 +0.01 +0.01 +2.63 TMO‑Non +0.01 +0.01 +0.01 TMO‑Non TMO‑Non TMO‑Non
SWB010+2 +0.01 +0.01 +0.01 +2.61 +153.93 +0.02 +0.01 +0.02 +0.03 TMO‑Non 126.52
CSR061+2 +1.40 +1.65 +0.01 +2.83 +6.54 +1.63 TMO‑Non TMO‑Non +107.95 TMO‑Non 182.47
AGT016+2 +0.01 +0.02 +0.01 +2.63 +47.43 +0.02 +0.01 +0.01 +0.34 TMO‑Non TMO‑Non
KRS262+1 +0.01 +0.01 +0.01 +2.65 TMO‑Non +0.01 +0.01 +0.01 TMO‑Non TMO‑Non 81.45
SET603+4 +0.01 +0.01 +0.01 +2.61 +0.01 +0.01 +0.17 TMO‑Non +9.86 +0.01 2.39
LCL652+1.001 +0.01 +2.41 +1.63 +3.29 TMO‑Non +2.52 TMO‑Non TMO‑Non +2.46 GUP‑Non 222.35
SET073+1 +0.01 +0.01 +0.01 +2.61 +0.01 +6.13 +20.53 +0.01 +0.01 +0.01 22.33
KRS266+1 +0.01 +0.01 +0.03 +2.62 TMO‑Non +0.01 +0.01 +0.01 TMO‑Non TMO‑Non 82.62
SWV221+1 +0.03 +0.01 +0.01 +2.61 +0.01 +0.01 +0.03 +30.31 +11.16 +0.01 5.67
CSR115+52 +0.08 +0.01 +0.01 +3.69 +0.01 +1.25 +0.01 GUP‑Non TMO‑Non TMO‑Non 123.27
SET108+1 +0.01 +0.01 +0.01 +2.58 TMO‑Non +0.02 +0.02 +0.03 TMO‑Non TMO‑Non 4.24
CSR063+3 +0.02 +8.69 +1.31 +2.98 +3.52 +1.55 +29.24 TMO‑Non TMO‑Non TMO‑Non 218.69
MGT042+1 +0.01 +0.07 +0.01 +2.61 +0.01 +0.01 TMO‑Non +0.01 UNK‑Non TMO‑Non 9.86
CSR051+3 +0.02 +10.10 +0.01 +2.78 +1.03 +0.01 +1.29 TMO‑Non TMO‑Non TMO‑Non 43.37
MGT063+1 +0.01 +0.01 +1.44 +4.99 TMO‑Non +1.61 TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non
CSR034+3 +0.02 +9.69 +0.09 +2.76 +4.44 +1.36 +1.78 TMO‑Non TMO‑Non TMO‑Non 115.59
NUM840+1 +0.01 +0.01 +0.01 +2.63 +0.01 +0.01 +0.01 UNK‑Non +7.34 TMO‑Non 3.21
CSR045+3 +0.10 +8.91 +7.73 +3.22 +189.17 +2.04 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV174+1 +0.01 +0.01 +64.64 +2.61 +0.01 +0.01 +0.13 +27.32 TMO‑Non TMO‑Non 6.46
CSR115+76 +0.01 +0.01 +0.01 +3.78 +0.01 +1.36 +109.99 TMO‑Non TMO‑Non TMO‑Non 124.08
SWV167+1 +0.01 +0.08 +0.01 +2.59 +0.01 +37.22 +30.86 TMO‑Non +12.17 TMO‑Non 21.48
CSR113+18 +0.01 +0.01 +0.01 +3.70 +0.01 +1.26 +0.01 TMO‑Non TMO‑Non TMO‑Non 122.73
LCL453+1 +0.01 +0.01 +0.01 +3.07 TMO‑Non +4.94 TMO‑Non +0.01 +0.64 GUP‑Non TMO‑Non
CSR057+2 +0.02 +1.68 +0.02 +2.72 TMO‑Non +0.01 +1.68 TMO‑Non +19.35 TMO‑Non TMO‑Non
PUZ001+2 +0.01 +0.01 +0.01 +2.62 +0.01 +0.01 +91.62 +0.01 +0.01 TMO‑Non TMO‑Non
CSR049+2 +1.43 +1.66 +0.01 +2.87 +273.09 +3.61 TMO‑Non TMO‑Non +94.58 TMO‑Non 183.59
ALG210+2 +0.01 +0.02 +0.01 +2.78 +0.01 TMO‑Non TMO‑Non +0.01 +68.19 TMO‑Non 3.76
CSR116+44 +0.01 +0.56 +0.01 +3.72 +0.01 +109.35 +110.05 TMO‑Non TMO‑Non TMO‑Non 122.90
GRP715+1 +15.69 +0.01 +0.01 +2.64 +0.01 TMO‑Non TMO‑Non +1.11 +64.53 GUP‑Non 32.89
KRS258+1 +0.01 +0.01 +0.01 +3.06 +50.54 +0.01 +0.25 +0.01 +62.36 TMO‑Non 89.16
NUM926+1 +0.03 +0.01 +0.01 +2.64 +0.01 +0.01 +0.01 GUP‑Non +0.45 164.57 TMO‑Non
CSR115+81 +0.01 +0.01 +0.02 +3.77 +0.01 +1.54 +0.01 GUP‑Non TMO‑Non TMO‑Non 123.18
SET083+1 +0.01 +0.01 +0.01 +2.58 +0.01 TMO‑Non TMO‑Non +0.01 +4.84 +0.01 25.09
KRS201+1 +0.01 +0.02 +0.01 +2.59 TMO‑Non +0.03 +1.54 +0.01 TMO‑Non TMO‑Non 106.55
GRP194+1 +0.01 +0.01 +0.01 +2.70 +14.93 TMO‑Non +185.50 +0.01 +0.01 +0.04 2.16
CSR071+3 +0.01 +11.54 +1.33 +3.45 +3.73 +24.75 +71.39 TMO‑Non TMO‑Non TMO‑Non 274.77
NUM925+3 +0.01 +10.37 +0.01 +3.39 +0.01 TMO‑Non +158.91 +14.29 TMO‑Non TMO‑Non 138.78
SWB029+3 +1.19 +0.01 +0.01 +2.71 +2.65 +54.02 +0.01 +4.16 +28.47 +9.04 44.68
SWW473+1 +0.01 +5.73 +0.01 +2.63 +0.01 +10.22 +0.01 +20.93 TMO‑Non TMO‑Non 16.02
CSR115+34 +0.01 +7.76 +0.01 +3.74 +85.80 +3.54 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SET601+3 +10.69 +147.33 +0.02 +3.62 +0.02 +36.35 +35.98 +0.01 TMO‑Non +37.56 31.45
CSR115+47 +0.02 +0.01 +0.01 +3.73 +1.45 +1.45 +110.04 TMO‑Non TMO‑Non TMO‑Non 135.22
SWW473+3 +0.01 +11.21 +0.01 +3.47 +1.05 +13.72 +4.00 TMO‑Non TMO‑Non UNK‑Non 157.36
CSR115+72 +0.01 +0.01 +0.02 +3.72 +86.25 +2.38 +224.05 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KLE148+2 +0.01 +0.02 +0.01 +2.62 TMO‑Non TMO‑Non TMO‑Non +0.02 TMO‑Non GUP‑Non 57.23
KRS259+1 +0.01 +0.03 +0.01 +2.64 +72.56 +0.02 +0.24 +0.01 +261.31 TMO‑Non 83.34
SET681+3 +0.01 +0.01 +0.01 +2.63 TMO‑Non +7.74 TMO‑Non GUP‑Non +0.35 TMO‑Non TMO‑Non
CSR115+73 +0.01 +0.01 +0.02 +3.80 +85.19 +2.26 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV384+1 +0.01 +6.08 +0.01 +2.62 +0.01 +0.02 +9.04 UNK‑Non TMO‑Non TMO‑Non 5.99
CSR040+3 +0.01 +13.83 +5.72 +8.35 TMO‑Non +1.95 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM422+1 +1.32 +4.96 +0.01 +3.22 +0.01 TMO‑Non TMO‑Non +0.01 TMO‑Non +0.02 57.68
CSR042+3 +0.01 +9.28 +0.01 +2.77 +44.17 +1.25 +1.41 TMO‑Non TMO‑Non TMO‑Non 154.19
GEO272+1 +0.01 +5.37 +0.02 +2.65 +0.01 +3.82 +111.08 GUP‑Non TMO‑Non +10.73 84.31
CSR115+87 +0.01 +0.55 +0.02 +3.67 +86.23 +1.84 +225.96 TMO‑Non TMO‑Non UNK‑Non TMO‑Non
SWV094+1 +0.01 +12.33 +35.91 +3.49 +0.01 +6.40 +71.96 TMO‑Non TMO‑Non TMO‑Non 6.45
CSR067+3 +0.01 +9.31 +0.02 +2.75 +44.05 +1.22 +1.38 TMO‑Non TMO‑Non TMO‑Non 117.96
GEO344+1 +0.01 +6.31 +0.01 +2.63 +0.01 +18.64 +117.85 UNK‑Non TMO‑Non +41.15 18.98
MGT067+1 +0.01 +0.01 +0.01 +2.69 TMO‑Non +0.01 +1.03 +0.02 +0.35 TMO‑Non TMO‑Non
SWV162+1 +0.01 +0.01 +0.02 +2.62 +0.01 TMO‑Non TMO‑Non +25.02 +11.57 TMO‑Non 6.21
KRS251+1 +0.01 +81.41 TMO‑Non TMO‑Non +15.45 +1.33 +27.77 TMO‑Non TMO‑Non TMO‑Non 61.72
GEO275+1 +0.38 +6.46 +2.43 +2.64 TMO‑Non +0.01 +27.88 UNK‑Non TMO‑Non TMO‑Non 86.08
CSR115+27 +0.01 +0.01 +0.01 +3.78 +85.25 +2.55 TMO‑Non GUP‑Non TMO‑Non TMO‑Non TMO‑Non
NUM855+2 +0.01 +0.98 +0.04 +2.63 +0.01 +2.15 +0.01 UNK‑Non TMO‑Non TMO‑Non 3.72
LCL642+1.010 +0.01 +78.04 +17.74 +106.29 TMO‑Non +0.02 TMO‑Non TMO‑Non +0.65 GUP‑Non TMO‑Non
LCL899+1 +1.20 +0.01 +0.01 +2.64 +108.94 +4.53 TMO‑Non UNK‑Non +2.75 GUP‑Non TMO‑Non
KRS263+1 +0.01 +0.09 +9.63 +12.23 TMO‑Non +0.01 +0.01 +0.01 TMO‑Non TMO‑Non 83.01
GEO278+1 +0.01 +6.58 +0.02 +3.31 TMO‑Non +36.43 +27.93 UNK‑Non TMO‑Non TMO‑Non 98.86
CSR114+4 +0.01 +0.02 +0.01 +3.77 +1.14 +1.34 +8.10 TMO‑Non TMO‑Non TMO‑Non 135.50
HAL002+1 +2.23 +0.02 +0.01 +2.60 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non +0.01 35.59
KRS267+1 +0.01 +0.02 +0.01 +2.63 TMO‑Non +0.01 +0.01 +0.02 TMO‑Non TMO‑Non 81.11
SWV455+1 +1.89 +6.49 +2.64 +2.61 +0.01 +5.23 +242.13 +0.33 +3.46 +0.01 17.93
CSR114+2 +0.02 +0.01 +0.01 +3.68 +1.72 +1.64 +16.11 TMO‑Non TMO‑Non TMO‑Non 135.81
LCL526+1 +12.09 +0.02 +0.01 +2.62 TMO‑Non +24.72 TMO‑Non +4.40 +0.46 TMO‑Non 78.36
CSR115+35 +0.01 +7.78 +0.01 +3.71 +85.34 +2.85 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV466+1 +0.06 +0.01 +2.54 +46.80 +0.22 +95.27 TMO‑Non +0.01 TMO‑Non TMO‑Non 30.59
LCL640+1.010 +0.01 +8.32 +1.13 +3.97 TMO‑Non +36.02 TMO‑Non TMO‑Non +9.25 GUP‑Non TMO‑Non
SCT147+1 +0.01 +3.21 +0.01 +2.66 +0.01 +3.03 +27.88 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR114+21 +0.08 +0.01 +0.01 +3.75 +1.16 +1.37 +7.95 TMO‑Non TMO‑Non TMO‑Non 134.98
SWW271+1 +0.01 +10.12 +178.63 +3.92 +0.02 +24.24 +75.42 +98.51 TMO‑Non TMO‑Non 106.97
CSR050+3 +0.01 +11.24 +1.43 +4.00 +4.63 +3.35 +111.40 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GRA007+1 +8.14 +6.09 +0.01 +2.61 +15.71 +6.93 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
LCL642+1.020 +1.03 +81.94 +26.19 +6.79 TMO‑Non +1.51 TMO‑Non UNK‑Non +9.74 GUP‑Non TMO‑Non
SWB017+1 +0.01 +0.01 +0.03 +2.81 +0.02 TMO‑Non TMO‑Non TMO‑Non +135.44 TMO‑Non 16.33
KRS216+1 +0.02 +0.01 +0.01 +2.65 TMO‑Non +4.74 +3.68 +26.20 TMO‑Non TMO‑Non 82.51
SCT149+1 +0.01 +18.71 TMO‑Non TMO‑Non +0.13 +0.01 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR114+5 +0.01 +0.01 +0.01 +3.75 +1.43 +1.35 +8.07 GUP‑Non TMO‑Non TMO‑Non 132.90
GRA006+1 +17.47 +6.10 +0.01 +2.62 +15.89 +2.15 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS261+1 +0.01 +0.01 +37.71 +42.60 TMO‑Non +0.01 +20.03 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR012+1 +7.66 +30.19 +0.01 +2.63 TMO‑Non +219.44 TMO‑Non +0.01 +0.95 TMO‑Non TMO‑Non
CSR052+3 +0.01 +9.09 +5.92 +5.33 +222.33 +19.76 +71.18 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV469+1 +0.01 +25.12 +6.61 +4.82 +0.03 +5.72 TMO‑Non +24.50 TMO‑Non TMO‑Non 20.27
CSR115+97 +0.01 +0.01 +0.01 +3.79 +85.93 +1.83 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB057+1 +0.06 +0.01 +0.01 +2.86 +0.01 +15.83 TMO‑Non GUP‑Non +6.04 TMO‑Non 22.11
CSR048+3 +0.01 +9.24 +0.01 +3.54 +1.04 +11.95 +1.65 TMO‑Non TMO‑Non TMO‑Non 117.80
GEO127+1 +2.49 +6.10 +0.01 +2.63 +50.24 +162.54 TMO‑Non +0.01 UNK‑Non TMO‑Non TMO‑Non
KRS234+1 +0.01 +0.02 +0.01 +2.71 +45.61 +0.01 +27.93 +0.01 TMO‑Non UNK‑Non 80.02
KLE132+1 +0.01 +0.01 +0.01 +2.63 TMO‑Non TMO‑Non TMO‑Non +0.01 TMO‑Non GUP‑Non TMO‑Non
CSR115+6 +0.01 +0.02 +0.01 +3.78 +87.66 +2.24 +209.61 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB021+2 +0.01 +0.01 +0.01 +2.62 +0.01 +78.44 TMO‑Non +4.69 +1.85 +0.01 TMO‑Non
CSR066+3 +10.26 +12.13 +1.33 +3.56 +222.15 +19.96 +112.95 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GRP776+1 +0.01 +0.02 +0.01 +2.62 +0.01 TMO‑Non TMO‑Non +8.80 +52.24 GUP‑Non 147.55
CSR057+3 +0.01 +8.36 +1.41 +3.49 TMO‑Non +23.35 +105.95 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV486+3 +0.01 +1.71 +0.01 +19.71 +184.20 TMO‑Non +38.02 TMO‑Non +0.34 +1.04 TMO‑Non
CSR115+68 +0.08 +7.78 +0.01 +3.69 +86.32 +1.96 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KLE039+1 +3.34 +0.01 +0.01 +2.62 +0.01 TMO‑Non TMO‑Non +1.31 +174.68 GUP‑Non 43.53
CSR115+9 +0.01 +7.70 +0.01 +3.71 +90.04 +1.95 +137.96 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB049+1 +0.01 +0.56 +0.01 +3.20 TMO‑Non +16.04 +66.58 TMO‑Non +5.16 TMO‑Non 91.95
LCL676+1.001 +0.01 TMO‑Non TMO‑Non TMO‑Non +92.18 +3.02 +66.88 TMO‑Non +3.55 GUP‑Non TMO‑Non
SWV486+2 +0.02 +1.82 +0.01 +15.28 +184.58 TMO‑Non +50.93 TMO‑Non +0.35 +1.03 TMO‑Non
CSR073+3 +0.01 +9.27 +5.62 +4.35 TMO‑Non +1.48 +70.04 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL902+1 +0.01 +0.03 +0.01 +2.62 +0.01 +16.13 TMO‑Non GUP‑Non +6.66 GUP‑Non TMO‑Non
CSR113+7 +0.01 +0.01 +0.10 +3.74 +1.44 +3.64 +8.28 TMO‑Non TMO‑Non TMO‑Non 136.71
SWV478+1 +2.30 +42.26 +0.01 +2.63 +1.12 +60.55 TMO‑Non +71.33 TMO‑Non TMO‑Non 181.41
CSR115+70 +0.01 +7.68 +0.01 +3.71 +85.82 +1.85 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GEO300+1 +2.00 +0.01 +0.02 +2.64 +0.01 +0.01 +110.30 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR033+3 +0.01 +9.04 +5.83 +5.00 +227.31 +35.37 +79.77 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV468+1 +0.01 +24.18 +151.83 +7.06 +0.02 +5.22 TMO‑Non +89.34 TMO‑Non TMO‑Non 22.26
SYN353+1 +0.01 +0.04 +0.01 +2.68 TMO‑Non +10.03 TMO‑Non +1.39 UNK‑Non TMO‑Non TMO‑Non
GRA007+2 +8.15 +6.08 +0.01 +2.64 +42.15 +7.73 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR115+42 +0.01 +7.78 +0.01 +3.74 +86.36 +1.94 +0.47 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM842+1 +4.33 +0.01 +0.03 +2.61 +0.01 +161.76 TMO‑Non UNK‑Non TMO‑Non +123.38 3.66
LCL688+1.001 +25.82 +157.59 +10.95 TMO‑Non TMO‑Non +1.63 +36.68 TMO‑Non +3.64 GUP‑Non TMO‑Non
SWB097+1 +0.01 +0.01 +1.73 +11.74 +0.01 TMO‑Non +28.22 TMO‑Non TMO‑Non TMO‑Non 53.38
CSR115+3 +0.01 +0.01 +0.10 +3.88 +85.54 +2.33 +199.55 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW474+3 +0.01 +8.92 +0.01 +268.74 +1.21 +1.06 +217.06 GUP‑Non TMO‑Non TMO‑Non 31.61
LCL676+1.015 +1.14 TMO‑Non TMO‑Non TMO‑Non TMO‑Non +4.34 TMO‑Non GUP‑Non +6.45 GUP‑Non TMO‑Non
SWW470+1 +16.39 +2.00 +0.22 +3.05 +0.02 TMO‑Non TMO‑Non +4.81 +13.64 TMO‑Non 8.25
LCL676+1.005 +72.83 TMO‑Non TMO‑Non TMO‑Non +99.01 +6.91 TMO‑Non TMO‑Non +5.24 GUP‑Non TMO‑Non
ALG072+1 +0.01 +64.43 +0.01 +3.06 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR115+100 +0.01 +0.56 +0.01 +3.79 +85.46 +2.27 +0.02 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
REL042+1 +144.52 +0.01 +1.53 +4.69 TMO‑Non TMO‑Non TMO‑Non +61.30 TMO‑Non GUP‑Non TMO‑Non
CSR115+53 +0.01 +7.79 +0.02 +3.69 +85.97 +1.94 +184.12 GUP‑Non TMO‑Non TMO‑Non TMO‑Non
PUZ133+1 +18.30 +14.81 +3.13 +5.97 +1.33 +5.93 TMO‑Non +0.01 TMO‑Non GUP‑Non 101.61
CSR115+8 +0.01 +0.01 +0.02 +3.94 +89.34 +1.42 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM926+7 +5.82 +16.53 +1.93 +3.11 +4.11 +225.09 TMO‑Non +29.73 +16.83 TMO‑Non TMO‑Non
CSR070+3 +0.01 +10.83 +5.45 +4.18 +184.01 +7.96 +70.22 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV235+1 +5.55 +6.08 +0.01 +2.62 +17.83 TMO‑Non +224.97 +12.61 TMO‑Non GUP‑Non TMO‑Non
CSR044+3 +11.16 +10.54 +1.42 +3.93 +220.26 +29.97 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB077+1 +0.02 +0.01 +154.81 +5.67 +177.97 +12.62 +61.04 TMO‑Non TMO‑Non TMO‑Non 88.09
CSR038+3 +10.16 +11.25 +1.42 +3.50 +216.20 +26.94 +1.64 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GEO342+1 +0.01 +6.33 +0.02 +2.65 +172.29 +0.01 +110.03 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR027+3 +10.54 +11.06 +1.40 +3.48 +222.69 +26.44 +70.78 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GEO284+1 +0.01 +0.01 +0.01 +2.64 +153.41 +0.01 TMO‑Non UNK‑Non TMO‑Non TMO‑Non 46.93
LCL660+1.005 +0.01 +261.14 +127.85 +131.68 TMO‑Non +5.45 TMO‑Non TMO‑Non +3.86 GUP‑Non TMO‑Non
SWB047+1 +0.01 +0.01 +163.70 +11.21 TMO‑Non +50.35 TMO‑Non TMO‑Non TMO‑Non TMO‑Non 93.65
CSR115+90 +0.02 +7.81 +0.01 +3.77 +86.65 +1.92 +0.49 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV473+1 +2.49 +93.43 +151.16 +50.56 +0.01 TMO‑Non TMO‑Non +72.53 TMO‑Non TMO‑Non 22.52
CSR056+3 +0.02 +13.62 +1.41 +2.76 +220.87 +23.97 +86.37 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV404+1 +48.44 +16.71 +7.84 +2.62 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 7.06
LCL676+1.010 +79.74 TMO‑Non TMO‑Non TMO‑Non +207.63 +1.62 TMO‑Non TMO‑Non +8.65 GUP‑Non TMO‑Non
CSR013+1 +7.74 +24.20 +1.15 +3.63 TMO‑Non TMO‑Non TMO‑Non +6.91 TMO‑Non TMO‑Non TMO‑Non
CSR115+99 +0.02 +7.78 +0.03 +3.68 +86.38 +1.96 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KLE170+1.004 +74.86 +1.97 +8.12 +4.57 +2.73 TMO‑Non TMO‑Non +1.57 TMO‑Non GUP‑Non 41.09
SWB014+3 +1.20 +0.14 +0.01 +2.64 +2.15 TMO‑Non +137.96 +30.11 TMO‑Non +10.95 TMO‑Non
NUM335+1 +1.83 +0.01 +148.56 +104.83 TMO‑Non TMO‑Non +0.01 +180.19 TMO‑Non TMO‑Non TMO‑Non
SWB012+3 +1.21 +0.01 +0.01 +2.61 +5.64 TMO‑Non +13.22 UNK‑Non TMO‑Non +11.64 53.41
ALG223+1 +1.22 +81.36 TMO‑Non TMO‑Non +16.81 +82.36 TMO‑Non TMO‑Non +5.15 TMO‑Non 24.44
CSR115+55 +0.01 +7.65 +0.01 +3.72 +85.84 +1.85 +137.88 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW470+2 +0.01 +13.50 +235.34 +2.89 +1.05 TMO‑Non TMO‑Non TMO‑Non +7.86 TMO‑Non 51.37
CSR115+5 +0.01 +0.02 +0.01 +3.80 +160.43 +2.27 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT123+1 +2.93 +17.24 TMO‑Non TMO‑Non +0.02 TMO‑Non TMO‑Non +33.97 TMO‑Non TMO‑Non 20.80
CSR113+1 +0.01 +0.01 +0.02 +3.69 +1.23 +1.35 +8.01 TMO‑Non TMO‑Non TMO‑Non 135.60
SWW300+1 +0.01 +0.01 +3.52 +4.29 +8.93 +1.89 +29.58 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR062+3 +0.01 +9.48 +1.53 +3.83 TMO‑Non +14.36 +111.41 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM924+4 +6.91 +32.70 +0.01 +5.59 +2.53 TMO‑Non TMO‑Non UNK‑Non TMO‑Non UNK‑Non TMO‑Non
CSR030+3 +0.01 +9.40 +1.32 +3.47 +220.62 +11.96 +70.13 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV036+1 +0.01 +190.15 TMO‑Non TMO‑Non +0.01 +9.14 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR060+3 +67.09 +12.12 +1.42 +3.91 +222.50 +27.15 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB056+1 +23.22 +1.18 +3.93 +6.68 +172.87 TMO‑Non +36.24 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL660+1.015 +1.04 TMO‑Non TMO‑Non TMO‑Non TMO‑Non +3.71 TMO‑Non UNK‑Non +4.45 GUP‑Non TMO‑Non
SWW302+1 +0.01 +0.01 +3.54 +3.34 +8.92 +1.90 +29.49 UNK‑Non TMO‑Non UNK‑Non TMO‑Non
CSR036+3 +8.43 GUP‑Non +161.36 +10.65 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GEO093+1 +8.11 +6.07 +5.81 +2.90 +0.06 +9.84 TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non
LCL652+1.005 +0.01 +148.41 +1.24 +130.93 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non GUP‑Non TMO‑Non
SWB009+1 +0.01 +0.01 +27.34 +30.04 TMO‑Non +16.32 +31.53 TMO‑Non TMO‑Non TMO‑Non 127.14
SYN986+1.004 +12.56 TMO‑Non +134.59 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
LCL496+1 +0.01 +9.02 +74.44 +14.00 +15.93 TMO‑Non TMO‑Non UNK‑Non TMO‑Non GUP‑Non 82.36
KRS264+1 +0.01 +0.01 TMO‑Non TMO‑Non TMO‑Non +1.53 +114.32 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GEO280+1 +1.64 +6.70 +0.51 +3.00 +4.04 +52.53 TMO‑Non UNK‑Non TMO‑Non TMO‑Non 51.50
CSR061+3 +8.43 +37.44 +132.13 +6.95 TMO‑Non +29.56 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
PUZ073+1 28.65 +232.41 +3.14 +26.49 +16.52 TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non 18.94
CSR049+3 +8.44 GUP‑Non +157.81 +11.56 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GEO283+1 +9.86 +6.47 +0.01 +2.64 +152.94 +18.43 +121.86 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR116+24 +0.01 +0.01 +0.01 +3.78 +161.13 +4.06 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV492+1 +0.01 +54.38 +5.82 +28.96 +212.82 TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LCL648+1.010 3.93 TMO‑Non TMO‑Non TMO‑Non +6.44 284.88 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWV467+1 +8.45 +164.74 +250.96 +86.91 +16.03 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 26.27
CSR116+36 +0.01 +0.02 +0.01 +3.81 +161.22 +2.66 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT163+1 +28.08 +2.37 +6.23 +14.20 TMO‑Non TMO‑Non TMO‑Non +4.26 TMO‑Non TMO‑Non TMO‑Non
LCL654+1.005 +10.28 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
NUM346+1 +1.82 +0.01 +149.53 +108.26 TMO‑Non TMO‑Non TMO‑Non +172.80 TMO‑Non TMO‑Non TMO‑Non
SYO525+1.021 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SCT168+1 +2.38 +5.81 +0.01 +2.65 TMO‑Non +61.95 TMO‑Non GUP‑Non TMO‑Non TMO‑Non TMO‑Non
CSR113+9 +0.01 +7.79 +0.02 +3.94 TMO‑Non +11.44 +178.63 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW473+7 +18.92 +22.72 +2.32 +4.21 +1.13 TMO‑Non +6.86 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LCL650+1.010 +56.90 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non GUP‑Non TMO‑Non
GEO285+1 +1.62 +6.57 +0.01 +2.64 +0.01 +47.14 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
BOO109+1 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
CSR055+4 +0.60 +11.27 +9.02 +5.96 +221.58 +17.81 +62.02 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
NLP560+1 +21.18 +38.17 +17.12 TMO‑Non +215.79 TMO‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
SCT115+1 +2.85 +10.93 TMO‑Non +162.16 +7.13 +159.26 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR113+31 +0.01 +7.76 +0.01 +3.89 TMO‑Non +11.25 +192.35 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM511+3 +31.02 +2.48 +1.23 +3.37 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 35.47
LAT258+1 +21.50 +228.66 +35.04 +38.84 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non +37.85 TMO‑Non
SWV234+2 +2.80 +6.06 +0.01 +2.59 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
LCL668+1.005 +56.64 TMO‑Non TMO‑Non TMO‑Non +0.01 +0.01 TMO‑Non UNK‑Non TMO‑Non GUP‑Non TMO‑Non
SWB032+1 +0.01 +0.01 +8.83 +5.28 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL658+1.020 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
GEO286+1 +9.74 +8.08 +1.13 +2.66 +152.98 +24.94 +134.05 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LCL672+1.015 +37.36 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW313+1 +0.01 +34.59 +3.32 +4.32 +8.44 +3.88 +30.70 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR113+22 +0.08 +7.47 +0.01 +3.92 TMO‑Non +11.64 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB025+1 +0.01 +1.38 +6.05 +8.77 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL652+1.020 +24.71 +157.43 +11.23 +248.72 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWW312+1 +1.14 +39.52 +9.02 +7.28 +2.16 +3.51 +2.63 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR114+28 +0.01 +2.80 +0.01 +3.86 TMO‑Non +13.85 +189.14 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT166+1 +3.65 +4.63 +0.01 +4.39 TMO‑Non TMO‑Non TMO‑Non +4.85 TMO‑Non TMO‑Non TMO‑Non
LCL672+1.020 +113.32 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non TMO‑Non TMO‑Non
SWB014+1 +1.82 +1.18 +4.92 +7.52 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NLP562+1 +21.28 +38.16 +15.33 TMO‑Non +236.01 TMO‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
SWB058+1 +1.82 +0.01 +233.88 +190.72 +173.49 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 155.05
LCL662+1.005 +49.42 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWB106+1 +2.84 +0.02 +162.51 +10.22 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL656+1.020 +59.05 +179.34 +33.34 +137.55 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWB043+1 +2.32 +0.01 +169.22 +20.96 +160.66 TMO‑Non +109.20 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NLP561+1 +21.29 +37.89 +17.42 TMO‑Non +235.97 TMO‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
SWV398+1 +24.32 +259.65 +5.14 +2.62 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 21.32
LCL668+1.015 +67.90 TMO‑Non TMO‑Non TMO‑Non TMO‑Non +10.93 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SCT158+1 +0.01 +10.89 TMO‑Non TMO‑Non +15.49 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 258.73
LCL670+1.005 +96.04 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWW470+3 +2.35 +19.35 +151.17 +246.51 +2.72 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 36.44
LCL656+1.015 +25.80 +152.01 +5.12 +6.39 TMO‑Non +1.93 TMO‑Non TMO‑Non +205.19 GUP‑Non TMO‑Non
SWV474+1 +3.63 +26.49 +153.04 +23.54 +1.13 +13.82 TMO‑Non TMO‑Non TMO‑Non TMO‑Non 20.52
LCL664+1.015 +31.23 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
REL029+4 +122.01 +264.16 +13.54 +15.99 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL668+1.020 +85.65 TMO‑Non TMO‑Non TMO‑Non TMO‑Non +25.23 TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
PUZ077+1 +0.14 +101.08 +13.16 +30.45 TMO‑Non +0.01 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LCL650+1.020 +61.47 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non GUP‑Non TMO‑Non
SWW257+1 +93.71 TMO‑Non +243.39 +16.10 +7.34 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 64.84
LCL664+1.020 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non UNK‑Non TMO‑Non
SWW322+1 +1.33 +120.04 +9.93 +5.30 +9.74 +3.79 +31.22 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL876+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWW298+1 +0.02 +26.67 +3.33 +6.43 +8.53 +3.57 +71.42 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LCL688+1.015 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
NUM925+4 +3.60 +45.37 +0.16 +7.03 +2.04 TMO‑Non TMO‑Non GUP‑Non TMO‑Non UNK‑Non TMO‑Non
LCL646+1.015 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
LAT363+1 +1.81 +18.18 +5.34 +11.90 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL680+1.010 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWB026+1 +0.01 +0.77 +2.23 +4.95 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL638+1.015 +19.79 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non +101.55 TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWB083+1 +0.02 +0.01 TMO‑Non TMO‑Non +178.32 TMO‑Non +64.90 TMO‑Non TMO‑Non TMO‑Non 88.01
LCL688+1.020 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWB080+1 +2.32 +0.78 +158.62 +10.46 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL684+1.010 5.12 TMO‑Non TMO‑Non TMO‑Non +146.05 18.02 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
SCT120+1 +55.95 +10.89 +93.14 +12.14 +0.01 TMO‑Non TMO‑Non +191.99 TMO‑Non TMO‑Non TMO‑Non
GEO167+1 +3.42 TMO‑Non TMO‑Non TMO‑Non +23.15 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW318+1 +1.45 +49.99 +5.10 +6.08 TMO‑Non TMO‑Non +31.30 +278.80 TMO‑Non TMO‑Non TMO‑Non
LCL650+1.015 +58.27 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non GUP‑Non TMO‑Non
CSR004+1 +7.75 +23.16 +1.05 +3.61 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL662+1.020 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT137+1 +30.95 +2.42 +224.53 +2.65 TMO‑Non TMO‑Non TMO‑Non +4.45 TMO‑Non TMO‑Non TMO‑Non
LCL638+1.020 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
HWV091+1* +5.22 +19.95 TMO‑Non TMO‑Non TMO‑Non +11.07 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW299+1 +1.34 +38.56 +8.53 +7.17 TMO‑Non +3.88 +87.59 +263.70 TMO‑Non TMO‑Non TMO‑Non
SWW387+1 +0.01 +47.56 +3.41 +6.44 +10.23 +4.28 +31.30 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB068+1 +0.95 +3.99 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWV471+1 +3.34 +93.39 TMO‑Non TMO‑Non +15.64 TMO‑Non +173.86 +33.09 TMO‑Non TMO‑Non 27.00
GEO292+1 +82.97 +58.37 +2.53 +2.63 TMO‑Non +56.75 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW294+1 +0.01 +43.01 +8.61 +9.49 +14.12 +3.70 +158.06 +276.87 +38.82 TMO‑Non TMO‑Non
SWW311+1 +0.01 +30.10 +4.53 +6.63 +8.63 +3.50 +35.12 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWB094+1 +2.85 +0.01 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB093+1 +2.88 +0.99 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT141+1 +31.76 +22.74 +151.14 +3.18 TMO‑Non TMO‑Non TMO‑Non +4.37 TMO‑Non TMO‑Non TMO‑Non
SWB082+1 +2.85 +1.38 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GRA011+1 +6.70 +25.16 +3.11 +5.83 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB064+1 +7.64 +0.01 +127.96 +138.13 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
AGT011+2 +17.28 +114.98 TMO‑Non TMO‑Non +32.23 TMO‑Non TMO‑Non GUP‑Non TMO‑Non TMO‑Non TMO‑Non
SCT138+1 +30.94 +2.66 +224.60 +2.67 TMO‑Non TMO‑Non TMO‑Non +4.46 TMO‑Non TMO‑Non TMO‑Non
SCT139+1 +32.15 +4.11 +152.12 +3.50 TMO‑Non TMO‑Non TMO‑Non +4.76 TMO‑Non TMO‑Non TMO‑Non
HWV090+1* +8.24 +13.20 TMO‑Non TMO‑Non TMO‑Non +17.53 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SET018+1 +72.09 +6.13 +0.02 +2.61 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non 3.83 28.12
SEU218+1 +3.62 TMO‑Non +109.04 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL896+1 +139.99 +12.72 +0.01 +53.09 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non GUP‑Non TMO‑Non
SWB095+1 +2.86 +0.99 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW321+1 +1.34 +127.75 +10.22 +5.40 +9.84 +4.79 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWB089+1 +4.53 +41.69 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW385+1 +0.02 +48.56 +3.23 +6.87 +10.12 +4.66 TMO‑Non +247.60 TMO‑Non TMO‑Non TMO‑Non
SWW293+1 +0.01 +57.25 +8.51 +9.12 TMO‑Non +3.99 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW358+1 +1.31 +35.69 +7.82 +8.11 +8.63 TMO‑Non +75.77 GUP‑Non TMO‑Non TMO‑Non TMO‑Non
LCL889+1 TMO‑Non +114.51 +17.45 +46.14 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non GUP‑Non TMO‑Non
GEO288+1 +1.73 +21.47 +3.12 +14.52 +188.62 TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non 263.46
SWW391+1 +1.41 +47.77 +9.03 +6.74 TMO‑Non +4.28 +30.14 GUP‑Non TMO‑Non TMO‑Non TMO‑Non
NUM924+8 +5.82 +147.28 +2.43 +5.27 +3.54 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT152+1 +4.53 +30.79 TMO‑Non TMO‑Non +17.43 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT151+1 +4.54 +30.77 TMO‑Non TMO‑Non +17.51 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
HWV094+1* +141.46 +25.21 TMO‑Non TMO‑Non TMO‑Non +171.42 TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
HWV096+1* +140.96 +21.02 TMO‑Non TMO‑Non TMO‑Non +166.78 TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
SWW396+1 +0.01 TMO‑Non +10.01 +6.87 TMO‑Non TMO‑Non TMO‑Non +294.48 TMO‑Non TMO‑Non TMO‑Non
SEU418+3 +27.61 +31.62 +4.71 +82.83 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SCT156+1 +0.01 +10.89 TMO‑Non TMO‑Non +15.51 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
GRP646+1 +20.99 +236.66 +159.46 +11.43 +7.13 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW304+1 +1.42 TMO‑Non +5.33 +6.91 TMO‑Non TMO‑Non TMO‑Non +276.36 TMO‑Non TMO‑Non TMO‑Non
SET723+4 +237.36 +0.01 TMO‑Non TMO‑Non +1.62 TMO‑Non TMO‑Non TMO‑Non TMO‑Non +0.01 199.00
CSR038+5 +10.53 +67.06 +11.51 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
SWW309+1 +1.23 +278.44 +10.62 +6.03 TMO‑Non TMO‑Non TMO‑Non +295.60 TMO‑Non TMO‑Non TMO‑Non
LCL890+1 TMO‑Non TMO‑Non +184.94 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non GUP‑Non TMO‑Non
SCT157+1 +0.01 +10.91 TMO‑Non TMO‑Non +15.53 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SEU406+3 +3.63 +27.53 +0.02 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SEU430+3 +3.64 +17.22 +1.02 +206.76 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non UNK‑Non TMO‑Non
LCL461+1 TMO‑Non +131.74 +138.65 +14.77 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non GUP‑Non TMO‑Non
PRO006+1 +29.93 +132.96 +43.72 +21.24 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
SWB066+1 +7.68 +0.77 +239.66 +24.10 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW352+1 +0.01 TMO‑Non +5.02 +6.90 TMO‑Non TMO‑Non TMO‑Non +255.31 TMO‑Non TMO‑Non TMO‑Non
AGT024+2 +5.71 +42.31 TMO‑Non +173.39 TMO‑Non TMO‑Non +182.38 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW367+1 +1.42 +52.84 +12.61 +13.75 +10.73 TMO‑Non +38.36 UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWB039+1 +24.78 +10.92 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
REL034+2 +14.26 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
HWV092+1* +29.59 +26.56 TMO‑Non TMO‑Non TMO‑Non +183.72 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW378+1 +1.22 TMO‑Non +9.50 +6.21 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW307+1 +1.23 +270.96 +10.31 +6.52 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW097+1 +11.98 +17.66 +1.53 +4.20 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW296+1 +1.34 +199.20 +9.42 +7.09 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LAT348+4 +5.54 +21.23 +154.48 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SEU449+3 +199.18 TMO‑Non +26.24 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR042+6 +91.99 +108.27 +79.70 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
GEO341+1 +2.91 TMO‑Non TMO‑Non +29.00 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW349+1 +1.15 +26.77 +6.13 +5.67 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW380+1 +0.22 TMO‑Non +8.23 +6.89 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW373+1 +1.21 TMO‑Non +10.12 +9.45 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW360+1 +1.33 +46.06 +11.80 +7.00 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
NUM926+8 +46.10 +278.51 +13.42 +14.30 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW329+1 +1.12 TMO‑Non +10.12 +7.44 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
SWW336+1 +1.42 +32.45 +10.23 +10.30 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW348+1 +1.14 +26.67 +6.52 +4.94 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
GEO319+1 +57.93 +131.73 +7.02 +9.72 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SEU418+4 +34.05 +38.74 +5.41 TMO‑Non TMO‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR047+6 +92.01 +106.60 +82.51 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SWW395+1 +0.01 +79.78 +4.72 +6.63 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
CSR052+5 TMO‑Non +34.38 +11.61 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
SWW330+1 +1.42 +291.12 +10.23 +7.37 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LCL467+1 +295.41 TMO‑Non TMO‑Non +123.18 TMO‑Non TMO‑Non TMO‑Non +151.43 TMO‑Non GUP‑Non TMO‑Non
LCL508+1 TMO‑Non +208.46 +38.22 +219.34 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non
HWV107+1* TMO‑Non GUP‑Non TMO‑Non TMO‑Non TMO‑Non +103.68 TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SCT154+1 +0.01 +10.96 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT150+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
CSR048+6 +91.07 +125.31 +80.45 TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LCL570+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT148+1 +56.43 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT145+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SEU168+2 TMO‑Non +70.80 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non
GEO316+1 TMO‑Non TMO‑Non +83.26 +60.46 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SCT133+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SWW098+1 TMO‑Non +229.84 +25.65 +28.27 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LAT291+2 +34.31 +110.90 TMO‑Non +287.82 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SEU018+1 +28.11 +18.14 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non
CSR060+5 TMO‑Non +157.68 GUP‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non UNK‑Non UNK‑Non TMO‑Non TMO‑Non
GEO323+1 +78.04 TMO‑Non +82.96 +86.00 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
SEU435+2 +197.93 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SCT142+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SEU389+1 +83.46 +24.26 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non GUP‑Non TMO‑Non TMO‑Non TMO‑Non
GEO324+1 +43.10 TMO‑Non +82.18 +98.83 TMO‑Non TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non TMO‑Non
LCL554+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
Solved/400 375/400 339/400 321/400 310/400 215/400 216/400 158/400 95/400 73/400 32/400 134/400
Av. CPU Time 13.19 29.31 22.88 17.29 46.03 18.11 55.15 41.45 28.81 19.74 69.31
Solutions 372/400 339/400 321/400 310/400 215/400 214/400 158/400 95/400 73/400 30/400 0/400
μEfficiency 571 361 466 168 228 216 129 119 75 47 17
SOTAC 0.22 0.18 0.17 0.17 0.15 0.16 0.14 0.14 0.13 0.12 0.13
Core Usage 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 0.99 1.22
New Solved 5/6 5/6 0/6 0/6 0/6 6/6 0/6 0/6 0/6 0/6 0/6
* indicates a problem not previously seen by the systems. + indicates a solution was output by the system.


Results for: THF TFA FOF FNT EPR UEQ TNE TEQ TFI TFR TFE FNE FEQ FNN FNQ EPT EPS UEQ

Results for FNT (First-order Non-theorems)

First-order Non-theorems iProver
 1.0‑SAT
iProver
 1.4‑SAT
Crossbow
 0.1
CVC4
 1.4‑FNT
E
 1.9‑FNT
NLP199+1 +0.51 +0.03 +10.42 +76.61 +0.41
NLP211+1 +62.40 +66.00 TMO‑Non +0.03 +1.22
NLP237+1 +0.01 +0.02 +1.03 +15.11 +0.01
NLP217+1 +62.10 +66.34 TMO‑Non +0.01 +1.42
NLP165+1 +2.63 +0.01 +20.72 +5.64 +1.04
PRO013+2 +66.93 +64.33 +5.03 +3.34 TMO‑Non
GEO224+1 +60.40 +60.65 +5.02 +0.01 TMO‑Non
NLP049+1 +30.73 TMO‑Non TMO‑Non +0.01 +0.01
NLP195+1 +3.63 +0.01 +9.83 +18.34 +0.01
NLP090+1 +31.12 TMO‑Non TMO‑Non +0.01 +0.01
GEO211+3 +60.23 +60.25 +5.02 +0.01 TMO‑Non
RNG110+1 +65.33 +69.83 +5.02 +0.02 TMO‑Non
NLP230+1 +7.32 +0.01 +1.14 +18.54 +0.01
NLP218+1 +62.05 +66.33 TMO‑Non +0.01 +0.01
NLP169+1 +5.13 +0.01 +5.71 +15.94 +0.02
LAT384+1 +61.33 +61.23 +5.01 +0.01 TMO‑Non
GEO259+3 +60.23 +60.54 +5.02 +0.01 TMO‑Non
COM014+4 +62.93 +62.63 +5.04 +0.01 TMO‑Non
LCL679+1.010 +0.02 +1.04 +7.51 +0.01 TMO‑Non
NLP216+1 +62.14 +66.33 TMO‑Non +0.01 +1.34
NLP192+1 +3.60 +0.01 +9.93 +21.23 +0.43
NLP215+1 +62.02 +66.44 TMO‑Non +0.01 +0.01
NLP232+1 +0.01 +0.02 +1.01 +214.28 +0.01
NLP213+1 +62.14 +66.44 TMO‑Non +0.01 +1.05
NLP163+1 +2.62 +0.01 +28.72 +5.03 +1.12
NLP088+1 +31.13 TMO‑Non TMO‑Non +0.01 +0.01
PLA027+1 +0.01 +0.01 +5.02 +0.01 TMO‑Non
NLP256+1 +0.01 +0.02 TMO‑Non +1.03 +0.01
PLA026+1 +1.84 +0.01 +5.01 +0.01 TMO‑Non
PRO013+4 +64.55 +65.23 +5.02 +1.54 TMO‑Non
SYN330+1 +0.01 +0.01 +0.01 TMO‑Non +0.01
NUM440+1 +63.51 +64.54 +5.04 +0.01 TMO‑Non
LCL641+1.005 +0.01 +0.01 +5.01 +136.86 +0.05
NUM446+1 +0.01 +0.01 +5.01 +0.01 TMO‑Non
NLP222+1 +0.01 +0.01 +0.01 +0.01 +0.01
NLP070+1 +30.13 TMO‑Non +259.70 +0.02 +0.01
NLP193+1 +8.53 +0.02 +12.55 TMO‑Non +0.01
NLP255+1 +0.01 +0.01 TMO‑Non +1.05 +0.01
GEO254+3 +60.35 +60.34 +5.02 +0.02 TMO‑Non
NLP212+1 +62.24 +66.04 TMO‑Non +0.01 +1.23
GEO229+3 +60.13 +60.13 +5.00 +0.02 TMO‑Non
COM014+1 +61.24 +61.43 +5.02 +0.02 TMO‑Non
GEO224+2 +60.34 +60.45 +5.02 +0.01 TMO‑Non
NLP253+1 +0.72 +0.01 TMO‑Non +2.92 +0.01
NLP162+1 +2.52 +0.02 +5.50 +2.83 +0.02
NLP093+1 +31.13 TMO‑Non TMO‑Non +0.01 +151.02
GEO215+3 +60.23 +60.24 +5.01 +0.01 TMO‑Non
LAT386+1 +61.44 +61.41 +5.01 +0.01 TMO‑Non
GEO213+3 +60.25 +60.34 +5.02 +0.01 TMO‑Non
NUM445+5 +62.41 +63.03 +5.02 +0.01 TMO‑Non
PLA024+1 +0.01 +0.01 +5.02 +0.03 TMO‑Non
NLP076+1 +30.13 TMO‑Non +259.21 +0.01 +0.01
NLP236+1 +0.02 +0.02 +0.02 +13.53 +0.02
LAT383+1 +61.43 +61.04 +5.01 +0.03 TMO‑Non
LCL659+1.010 +0.01 +0.01 +5.22 +2.03 TMO‑Non
NUM447+1 +30.25 +4.22 +5.03 +0.01 TMO‑Non
NLP234+1 +1.02 +0.01 +1.01 +22.05 +0.01
NLP219+1 +62.15 +66.43 TMO‑Non +0.01 +0.01
NLP233+1 +1.03 +0.01 +0.01 +62.22 +0.01
NLP092+1 +31.23 TMO‑Non TMO‑Non +0.01 +151.02
NLP160+1 +2.53 +0.01 +5.51 +2.92 +0.01
LAT387+1 +61.66 +61.66 +5.02 +0.01 TMO‑Non
GEO212+3 +60.13 +60.25 +5.01 +0.02 TMO‑Non
PRO013+1 +68.04 +72.35 +5.03 +26.53 TMO‑Non
NLP032+1 +0.01 +0.01 +5.53 +128.61 +1.04
LAT385+1 +61.44 +61.24 +5.02 +0.01 TMO‑Non
GEO230+3 +60.14 +60.25 +5.03 +0.01 TMO‑Non
HWV111+1* +57.56 +65.66 +5.59 +128.12 TMO‑Non
LCL679+1.005 +0.01 +0.01 +6.54 +0.01 TMO‑Non
HWV117+1* TMO‑Non TMO‑Non +9.23 TMO‑Non TMO‑Non
GEO228+3 +60.14 +60.23 +5.02 +0.05 TMO‑Non
HWV114+1* +75.10 +81.49 +6.39 +184.08 TMO‑Non
GEO214+3 +60.24 +60.25 +5.02 +0.01 TMO‑Non
KRS034+1 +62.93 +61.13 +5.03 +0.01 +0.02
GRA025+1 +5.75 +31.44 +31.40 +8.34 TMO‑Non
NLP181+1 +61.24 +66.93 TMO‑Non +0.01 +0.02
GRA026+1 +6.72 +55.65 +242.11 +107.86 TMO‑Non
NLP084+1 +31.03 TMO‑Non TMO‑Non +0.01 +0.01
GRA018+1 +60.93 +60.66 +5.22 +65.54 TMO‑Non
NLP087+1 +31.03 TMO‑Non TMO‑Non +0.01 +0.01
LCL653+1.005 +64.02 +63.73 +5.02 +202.51 TMO‑Non
NUM439+1 +68.03 +66.54 +5.02 +0.01 TMO‑Non
SWB012+4 +0.35 +0.02 +5.01 +0.01 +0.01
NLP187+1 +61.33 +66.73 TMO‑Non +0.01 +0.01
LCL673+1.005 +67.95 +82.94 +5.10 +3.83 TMO‑Non
NLP180+1 +61.55 +66.94 TMO‑Non +0.02 +0.01
SWV440+1 +0.01 +0.01 +5.00 +0.01 +0.01
NLP186+1 +61.53 +66.53 TMO‑Non +0.01 +0.01
LCL677+1.015 +60.55 +60.93 +5.29 +0.01 TMO‑Non
NLP082+1 +31.14 TMO‑Non TMO‑Non +0.01 +0.01
NLP161+1 +2.53 +0.01 +5.52 +6.05 +0.01
NLP182+1 +61.55 +67.15 TMO‑Non +0.92 +0.12
GEO260+3 +60.36 +60.24 +4.99 +0.01 TMO‑Non
RNG110+4 +69.05 +70.03 +5.02 +0.01 TMO‑Non
LCL665+1.020 +0.02 +0.01 +5.52 +4.63 TMO‑Non
NLP083+1 +31.12 TMO‑Non TMO‑Non +0.01 +0.01
LCL687+1.005 +0.01 +0.01 +5.03 +0.01 TMO‑Non
NLP184+1 +61.13 +67.15 TMO‑Non +0.01 +0.15
MSC014+1 +0.01 +0.01 +17.79 +0.01 +0.01
NLP188+1 +61.24 +66.15 TMO‑Non +0.01 +0.01
MSC013+1 +0.01 +0.01 TMO‑Non +9.13 +0.01
LCL577+1 +62.43 +63.65 +5.12 +13.04 TMO‑Non
LCL639+1.015 +109.25 +188.16 +52.61 +79.32 TMO‑Non
NLP085+1 +31.03 TMO‑Non TMO‑Non +0.01 +0.01
SWB011+3 TMO‑Non TMO‑Non +13.61 TMO‑Non +3.52
SWV484+2 TMO‑Non TMO‑Non UNK‑Non TMO‑Non +0.01
SWB034+1 TMO‑Non TMO‑Non +15.79 TMO‑Non +3.72
SWV483+2 TMO‑Non TMO‑Non UNK‑Non TMO‑Non +1.13
LCL671+1.020 +62.14 +63.14 +6.21 TMO‑Non TMO‑Non
LCL887+1 +61.25 +62.44 +5.02 +0.02 TMO‑Non
SWB005+3 TMO‑Non TMO‑Non +13.91 TMO‑Non +4.51
PRO007+2 +150.67 TMO‑Non +5.01 TMO‑Non TMO‑Non
LCL653+1.010 +68.25 +72.34 +5.11 TMO‑Non TMO‑Non
KLE136+1 +84.56 +231.28 +5.09 +5.56 TMO‑Non
SWB017+3 TMO‑Non TMO‑Non +14.32 TMO‑Non +4.12
PRO008+2 +198.86 TMO‑Non +5.01 TMO‑Non TMO‑Non
LCL689+1.015 +67.75 +69.00 +5.22 +226.82 TMO‑Non
KLE172+1 +87.52 +210.61 +4.99 +12.83 TMO‑Non
LCL671+1.015 +61.44 +62.25 +5.79 TMO‑Non TMO‑Non
PRO007+1 +134.45 TMO‑Non +5.08 TMO‑Non TMO‑Non
SWB028+3 TMO‑Non TMO‑Non +15.22 TMO‑Non +2.03
SWW103+1 +65.96 +65.85 +5.04 +0.01 TMO‑Non
SWB019+3 TMO‑Non TMO‑Non +14.83 TMO‑Non +4.53
GEG001+1 TMO‑Non TMO‑Non +11.11 TMO‑Non +0.01
SWB030+3 TMO‑Non TMO‑Non +14.63 TMO‑Non +3.14
KRS051+1 +83.34 +87.95 +5.23 +12.63 TMO‑Non
SWB004+3 TMO‑Non TMO‑Non +14.03 TMO‑Non +3.94
LCL883+1 +66.35 +68.86 +5.01 +0.01 TMO‑Non
LCL651+1.010 +62.45 +63.34 +5.12 +91.75 TMO‑Non
HWV048+1 +115.68 +161.66 TMO‑Non TMO‑Non TMO‑Non
SWB015+3 TMO‑Non TMO‑Non +14.01 TMO‑Non +4.34
SYO593+1 TMO‑Non TMO‑Non UNK‑Non TMO‑Non +9.84
LCL669+1.020 +9.43 +13.25 +5.62 TMO‑Non TMO‑Non
HWV053+1 TMO‑Non TMO‑Non UNK‑Non TMO‑Non +177.23
KRS222+1 +97.97 +141.95 TMO‑Non TMO‑Non TMO‑Non
HAL003+2 +88.96 +61.73 +5.02 TMO‑Non TMO‑Non
LCL669+1.010 +9.22 +10.83 +5.12 +92.63 TMO‑Non
HAL005+1 TMO‑Non +63.62 +5.01 TMO‑Non TMO‑Non
LCL651+1.015 +66.34 +70.45 +5.21 +226.43 TMO‑Non
SWV482+1 TMO‑Non TMO‑Non UNK‑Non TMO‑Non +0.01
SWB007+3 TMO‑Non TMO‑Non +13.91 TMO‑Non +4.22
HAL003+1 +98.36 +63.55 +5.02 TMO‑Non TMO‑Non
SWB032+3 TMO‑Non TMO‑Non +14.29 TMO‑Non +3.52
HWV112+1* TMO‑Non TMO‑Non +5.63 +130.63 TMO‑Non
SWB027+3 TMO‑Non TMO‑Non +194.75 TMO‑Non +3.31
HWV113+1* TMO‑Non TMO‑Non +5.79 +133.17 TMO‑Non
SWB016+3 TMO‑Non TMO‑Non +15.43 TMO‑Non +4.42
HWV087+1* +64.45 +65.34 +5.42 +97.52 TMO‑Non
KRS177+1 +79.64 +103.53 TMO‑Non TMO‑Non TMO‑Non
HWV115+1* TMO‑Non TMO‑Non +6.42 +184.91 TMO‑Non
KRS253+1 +90.01 +101.41 TMO‑Non TMO‑Non TMO‑Non
HWV118+1* TMO‑Non TMO‑Non +8.91 TMO‑Non TMO‑Non
KRS197+1 +97.45 +200.24 TMO‑Non TMO‑Non TMO‑Non
HWV049+1 +162.15 +181.25 TMO‑Non TMO‑Non TMO‑Non
KRS212+1 +78.25 +135.74 TMO‑Non TMO‑Non TMO‑Non
HWV042+1 +111.45 +128.16 TMO‑Non TMO‑Non TMO‑Non
LCL647+1.010 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
HWV048+2 +241.86 +286.25 TMO‑Non TMO‑Non TMO‑Non
KRS232+1 +66.04 +98.95 TMO‑Non TMO‑Non TMO‑Non
SWV238+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non +0.01
KRS246+1 +115.26 +125.65 TMO‑Non TMO‑Non TMO‑Non
LCL565+1 +243.46 +163.16 +5.11 TMO‑Non TMO‑Non
KRS270+1 +102.27 +110.07 TMO‑Non TMO‑Non TMO‑Non
LCL571+1 +232.67 +187.83 +5.14 TMO‑Non TMO‑Non
SWB010+3 TMO‑Non TMO‑Non +285.98 TMO‑Non +3.42
HWV080+1 TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non
SWB023+3 TMO‑Non TMO‑Non +177.64 TMO‑Non +4.72
SYO586+1 TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non
SWB021+3 TMO‑Non TMO‑Non +182.63 TMO‑Non +20.94
HWV082+1 TMO‑Non TMO‑Non UNK‑Non TMO‑Non TMO‑Non
LCL657+1.015 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
LCL567+1 TMO‑Non TMO‑Non +5.11 TMO‑Non TMO‑Non
KRS244+1 +114.26 +105.42 TMO‑Non TMO‑Non TMO‑Non
SWV483+1 TMO‑Non TMO‑Non UNK‑Non TMO‑Non +1.82
SWB025+3 TMO‑Non TMO‑Non +226.50 TMO‑Non +5.13
SWV485+1 TMO‑Non TMO‑Non UNK‑Non TMO‑Non +3.52
KRS241+1 +89.24 +102.24 TMO‑Non TMO‑Non TMO‑Non
BIO001+1* +63.33 +80.67 UNK‑Non TMO‑Non TMO‑Non
KRS240+1 +82.34 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
SET781+3 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS271+1 +138.04 +107.04 TMO‑Non TMO‑Non TMO‑Non
NUM374+2 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS230+1 +246.15 +187.54 TMO‑Non TMO‑Non TMO‑Non
GEO121+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS247+1 +90.44 +201.72 TMO‑Non TMO‑Non TMO‑Non
NUM444+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS250+1 +84.03 +206.94 TMO‑Non TMO‑Non TMO‑Non
RNG107+4 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS249+1 +110.73 TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM352+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS206+1 +65.84 +94.04 TMO‑Non TMO‑Non TMO‑Non
ALG230+4 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS225+1 +233.46 +102.53 TMO‑Non TMO‑Non TMO‑Non
CAT024+2 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS218+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
NUM365+1 TMO‑Non TMO‑Non TMO‑Non TMO‑Non TMO‑Non
KRS227+1 +150.22 +138.33 TMO‑Non TMO‑Non TMO‑Non
HWV120+1* TMO‑Non TMO‑Non +12.12 TMO‑Non TMO‑Non
SWB024+3 TMO‑Non TMO‑Non +15.61 TMO‑Non +2.63
PUZ133+3 +223.45 TMO‑Non +5.03 +1.23 TMO‑Non
Solved/200 150/200 133/200 124/200 116/200 82/200
Av. CPU Time 59.12 63.37 21.66 24.38 7.23
Solutions 150/200 133/200 124/200 116/200 82/200
μEfficiency 146 186 107 374 292
SOTAC 0.30 0.29 0.32 0.25 0.38
Core Usage 1.00 1.00 1.00 1.00 0.99
New Solved 4/10 4/10 9/10 6/10 0/10
* indicates a problem not previously seen by the systems. + indicates a solution was output by the system.


Results for: THF TFA FOF FNT EPR UEQ TNE TEQ TFI TFR TFE FNE FEQ FNN FNQ EPT EPS UEQ

Results for EPR (Effectively Propositional CNF)

Effectively Propositional CNF iProver
 0.9
iProver
 1.4
E
 1.9
SYN829‑1 +3.60 +8.61 +3.19
SYN862‑1 13.13 +4.52 +1.23
SYN822‑1 30.53 +4.53 +60.41
SWV422‑1.065 5.04 +2.64 +138.15
SYN449‑1 +0.06 +0.01 +44.24
SYN486‑1 0.03 +0.01 +41.56
SYN902‑1 +6.84 +0.01 +0.05
PUZ017‑1 0.04 +0.01 +0.01
SYN826‑1 +2.52 +6.51 +2.50
SYN451‑1 0.01 +0.01 +27.44
SYN456‑1 +0.06 +0.01 TMO‑Non
SYN459‑1 0.01 +0.14 +26.71
SYN864‑1 13.33 +3.62 +1.22
SYN471‑1 0.01 +0.01 +3.53
GRP123‑7.005 +0.01 +0.01 TMO‑Non
SYN444‑1 0.01 +0.01 +43.83
SYN839‑1 +4.02 +10.12 +3.99
SYN467‑1 0.01 +0.01 +31.14
SYN811‑1 +1.73 +0.01 +0.01
SWV423‑1.010 1.73 +2.53 TMO‑Non
SYN888‑1 +0.01 +0.02 +0.01
SYN443‑1 0.01 +0.01 +5.44
SYN420‑1 +0.01 +0.01 +0.01
SYN461‑1 0.01 +0.01 +48.54
SYN520‑1 +1.04 +0.01 TMO‑Non
SYN501‑1 0.01 +0.01 +7.64
SYN463‑1 +0.01 +0.01 +4.85
SYN477‑1 0.01 +0.01 +13.43
SYN855‑1 +9.70 +11.00 +4.28
SYN445‑1 0.01 +0.01 +1.74
SYN841‑1 +4.44 +10.21 +3.88
SYN507‑1 0.01 +0.01 +20.34
SYN815‑1 +3.13 +3.53 +1.11
SYN498‑1 0.01 +0.01 +24.13
SYN435‑1 +0.01 +0.01 TMO‑Non
SYN861‑1 12.73 +3.72 +1.21
SYN824‑1 +0.01 +1.93 +0.01
SYN512‑1 0.01 +0.01 +14.53
GRP124‑7.005 +0.01 +0.01 TMO‑Non
SYN452‑1 0.01 +0.14 +42.64
SYN545‑1 +0.01 +0.01 +224.67
SYN483‑1 0.01 +0.02 +9.24
SYN851‑1 +6.24 +3.33 +1.13
SYN489‑1 0.01 +0.01 +31.65
SYN424‑1 +0.01 +0.01 TMO‑Non
SWV421‑1.065 5.85 +1.94 +131.65
SYN519‑1 +2.16 +5.14 TMO‑Non
PLA031‑1.004 30.95 +52.77 +2.16
SYN854‑1 16.02 +13.40 +4.41
SYN503‑1 0.01 +0.01 +12.15
SYN818‑1 +11.51 +11.31 +4.01
SYN499‑1 0.01 +0.01 +11.72
SYN542‑1 +0.01 +0.01 TMO‑Non
SWV424‑1.050 0.01 +0.01 TMO‑Non
SYN547‑1 +0.01 +0.15 +249.48
SYN475‑1 0.01 +0.01 +20.72
SYN514‑1 +0.01 +0.01 TMO‑Non
SYN448‑1 0.01 +0.01 +6.74
SYN428‑1 +0.01 +0.02 TMO‑Non
SYN470‑1 0.01 +0.01 +22.04
SYN546‑1 +0.01 +0.01 +7.11
SYN488‑1 0.01 +0.01 +22.34
SYN831‑1 +3.91 +8.83 +3.31
SYN482‑1 0.01 +0.01 +15.45
SYN464‑1 +0.01 +0.01 TMO‑Non
SYN500‑1 0.01 +0.01 +26.76
SYN429‑1 +0.01 +0.01 TMO‑Non
SYN473‑1 0.01 +0.03 +22.43
SYN441‑1 +0.01 +0.01 TMO‑Non
HWV069‑1 6.44 +19.64 +18.12
SYN872‑1 +0.01 +0.01 +0.01
GRP128‑2.006 0.01 +0.01 +55.87
GRP124‑9.005 +0.01 +0.01 TMO‑Non
SYN865‑1 12.72 +3.73 +1.22
SYN426‑1 +0.01 +1.05 TMO‑Non
SYN850‑1 2.43 +3.53 +1.22
SYN434‑1 +0.01 +0.01 TMO‑Non
SYN442‑1 0.01 +0.01 +21.44
SYN832‑1 +4.13 +7.73 +2.90
SYN509‑1 0.01 +0.01 +18.43
SYN437‑1 +0.04 +0.01 TMO‑Non
SYN469‑1 0.01 +0.01 +9.43
SYN427‑1 +0.01 +0.01 TMO‑Non
SYN478‑1 0.01 +0.01 +3.81
SYN423‑1 +0.01 +0.32 +5.13
SWV423‑1.020 13.05 +19.65 TMO‑Non
SYN852‑1 +50.03 +11.31 +4.41
SYN506‑1 0.01 +0.04 +5.14
GRP124‑8.005 +0.01 +0.01 TMO‑Non
SYN462‑1 0.01 +0.05 +2.94
SYN513‑1 +0.01 +0.01 +1.91
SYN481‑1 0.01 +0.01 +10.64
SYN816‑1 +4.03 +3.52 +1.14
SWV418‑1.100 2.15 +3.63 +54.12
SYN518‑1 +0.01 +0.01 TMO‑Non
HWV091‑1* 2.52 7.62 +2.70
SYN853‑1 15.69 +11.22 +4.48
HWV094‑1* 7.68 23.98 +8.86
GRP129‑3.005 +0.01 +0.01 TMO‑Non
HWV090‑1* 3.11 9.42 +3.48
SYN840‑1 +7.81 +9.99 +3.79
SYN439‑1 0.01 +0.01 TMO‑Non
SYN453‑1 +0.01 +0.01 TMO‑Non
SWV422‑1.105 12.34 +11.33 +175.24
HWV079‑1 +35.17 +132.49 TMO‑Non
SWV421‑1.100 12.23 +8.34 +163.36
PLA043‑1 +61.76 TMO‑Non TMO‑Non
SYO594‑1 TMO‑Non TMO‑Non +157.75
HWV048‑1 +53.15 +82.54 TMO‑Non
HWV058‑1 54.43 +16.53 +16.73
HWV042‑1 +25.74 +80.55 TMO‑Non
HWV092‑1* 16.43 55.22 +17.80
HWV076‑1 +53.43 +50.22 TMO‑Non
HWV096‑1* 7.58 24.10 +8.67
SYN821‑1 12.74 +4.22 +39.83
HWV059‑1 76.17 +16.22 +12.52
HWV066‑1 +33.14 +28.44 TMO‑Non
SWV421‑1.105 19.76 +13.02 TMO‑Non
HWV062‑1 +8.52 +54.04 TMO‑Non
HWV051‑1 32.15 +61.84 TMO‑Non
HWV071‑1 +202.71 TMO‑Non TMO‑Non
SWV422‑1.100 11.84 +6.83 TMO‑Non
HWV053‑1 TMO‑Non TMO‑Non GUP‑Non
SWV421‑1.205 29.24 +18.83 TMO‑Non
HWV049‑2 +29.25 +109.55 TMO‑Non
SYO591‑1 TMO‑Non TMO‑Non +96.53
SYO595‑1 +184.89 TMO‑Non TMO‑Non
SWV424‑1.100 0.01 +0.01 TMO‑Non
HWV049‑1 +33.05 +92.54 TMO‑Non
HWV050‑1 30.63 +64.15 TMO‑Non
HWV042‑2 +32.94 +77.17 TMO‑Non
SWV418‑1.500 13.15 +17.54 TMO‑Non
SYO593‑1 TMO‑Non TMO‑Non +190.38
HWV040‑1 23.95 +81.04 TMO‑Non
HWV082‑1 TMO‑Non TMO‑Non TMO‑Non
HWV045‑2 37.54 +61.85 TMO‑Non
PLA040‑1 TMO‑Non TMO‑Non TMO‑Non
SWV420‑1.010 2.33 +2.83 TMO‑Non
HWV085‑1 TMO‑Non TMO‑Non TMO‑Non
HWV043‑1 21.93 +70.53 TMO‑Non
HWV048‑2 +31.96 +83.35 TMO‑Non
HWV039‑2 28.34 +62.66 TMO‑Non
HWV074‑1 TMO‑Non TMO‑Non TMO‑Non
HWV041‑2 30.55 +83.16 TMO‑Non
PLA038‑1 +117.69 +157.16 TMO‑Non
SWV422‑1.200 24.84 +23.23 TMO‑Non
PLA045‑1 TMO‑Non +289.03 TMO‑Non
SWV424‑1.450 11.64 +11.72 TMO‑Non
HWV063‑1 TMO‑Non +154.43 TMO‑Non
PUZ056‑2.010 9.33 +15.24 +158.04
SWV418‑1.300 14.95 +20.32 TMO‑Non
HWV047‑2 61.65 +71.25 TMO‑Non
HWV046‑1 26.95 +69.97 TMO‑Non
SWV424‑1.500 15.25 +15.23 TMO‑Non
SWV419‑1.010 1.24 +0.01 TMO‑Non
HWV051‑2 32.45 +77.86 TMO‑Non
SWV421‑1.300 35.44 +17.43 TMO‑Non
SWV424‑1.350 3.62 +8.33 TMO‑Non
HWV044‑1 23.14 +69.95 TMO‑Non
SWV423‑1.050 67.95 +30.74 TMO‑Non
HWV047‑1 67.46 +73.06 TMO‑Non
HWV050‑2 32.45 +60.94 TMO‑Non
SWV424‑1.300 3.73 +11.44 TMO‑Non
HWV087‑1* 6.14 +43.77 TMO‑Non
SWV421‑1.365 42.94 +16.33 TMO‑Non
HWV064‑1 TMO‑Non TMO‑Non TMO‑Non
PLA031‑1.006 219.23 TMO‑Non TMO‑Non
SWV422‑1.360 44.47 +16.62 TMO‑Non
SWV421‑1.405 54.44 +17.34 TMO‑Non
PLA031‑1.007 TMO‑Non TMO‑Non TMO‑Non
SWV422‑1.365 64.98 +16.44 TMO‑Non
SWV422‑1.465 197.91 +20.33 TMO‑Non
SWV418‑1.700 16.95 +25.84 TMO‑Non
SWV420‑1.020 16.14 +19.85 TMO‑Non
SWV418‑1.580 15.55 +22.32 TMO‑Non
SWV419‑1.030 47.54 +5.44 TMO‑Non
SWV421‑1.500 86.97 +22.56 TMO‑Non
SWV421‑1.465 76.47 +21.05 TMO‑Non
SWV422‑1.405 55.64 +17.35 TMO‑Non
SWV422‑1.400 40.55 +17.84 TMO‑Non
SWV418‑1.900 24.54 +32.95 TMO‑Non
SWV419‑1.020 5.54 +1.93 TMO‑Non
SWV421‑1.360 37.85 +16.64 TMO‑Non
HWV103‑1* 138.91 TMO‑Non TMO‑Non
HWV111‑1* 28.06 +77.47 GUP‑Non
HWV114‑1* 65.46 +77.64 TMO‑Non
HWV107‑1* 24.23 +88.73 TMO‑Non
PLA031‑1.008 TMO‑Non TMO‑Non TMO‑Non
SWV419‑1.040 41.86 +21.15 TMO‑Non
PUZ056‑2.025 TMO‑Non TMO‑Non TMO‑Non
PUZ056‑2.030 TMO‑Non TMO‑Non TMO‑Non
SWV419‑1.050 58.55 +25.75 TMO‑Non
HWV078‑1 108.67 +60.85 TMO‑Non
HWV060‑1 94.15 +62.84 TMO‑Non
SWV419‑1.045 56.17 +26.13 TMO‑Non
HWV065‑1 69.05 +42.34 TMO‑Non
PUZ056‑2.027 TMO‑Non TMO‑Non TMO‑Non
SYO589‑1 TMO‑Non TMO‑Non TMO‑Non
MSC024‑1 275.85 298.08 TMO‑Non
SWV420‑1.040 55.64 +31.73 TMO‑Non
Solved/200 183/200 180/200 88/200
Av. CPU Time 22.96 22.80 31.02
Solutions 62/200 174/200 88/200
μEfficiency 400 405 98
SOTAC 0.44 0.43 0.36
Core Usage 1.00 1.00 1.00
New Solved 10/10 9/10 5/10
* indicates a problem not previously seen by the systems. + indicates a solution was output by the system.


Results for: THF TFA FOF FNT EPR UEQ TNE TEQ TFI TFR TFE FNE FEQ FNN FNQ EPT EPS UEQ

Results for UEQ (Unsatisfiable Unit Equality CNF)

Unsatisfiable Unit Equality CNF Waldmeister
 710
E
 1.9
GRP139‑1 +0.03 +0.05
BOO071‑1 +0.01 +0.01
COL063‑5 +0.02 +0.01
REL023‑1 +0.01 +0.05
GRP429‑1 +0.01 +0.01
GRP565‑1 +0.01 +0.01
COL003‑13 +0.01 +0.01
ALG236‑1 +0.01 +0.02
REL007‑1 +0.01 +0.01
GRP559‑1 +0.01 +0.01
ROB005‑1 +0.01 +0.01
COL009‑1 +0.01 +0.01