AGT_PlanT
ALG_FTA
ALG_Meier
ANA_KaliszykHOL
ANA_Paulson
ARI_FloorCeiling
ARI_NoVars
ARI_Vars
COL_MengIsabelle
COL_Paulson
COL_StrongFixedPoint
COMLATRNGNUM_SAD
COM_QuantifierElim
CSR_2Trolleys
CSR_AdimenSUMO
CSR_Cyc1
CSR_Cyc2
CSR_Cyc3
CSR_Cyc4
CSR_Cyc5
CSR_Cyc6
CSR_KitchenSink
CSR_LogAnswer
CSR_SUMO1
CSR_SUMO2
CSR_SUMO3
CSR_SUMO4
CSR_SUMO5
CSR_SUMO6
DAT_KaliszykHOL
DAT_WaldmannCollections
FLD_Draeger
GEO_HalesUrban
GEO_ILTP
GEO_ILTP_Affine
GEO_KulikCurves
GEO_Quaife
GRA_PathTriangles
GRA_Ramsey
GRP_FromHR
GRP_Quasi
GRP_StanovskyCNF
GRP_StanovskyFOF
HWV_Safelogic
HWV_Safelogic2
HWV_ZurabCNF
HWV_ZurabFOF
HWV_ZurabTFA
HWV_ZurabTFF
KLE_Hoefner
KRS_OWL
KRS_SZSOntology
LAT_McCuneSet1
LAT_McCuneSet2
LAT_McCuneSet3
LAT_McCuneSet4
LAT_Paulson
LCL_CondensedDetachment
LCL_KaminskiModal
LCL_PCBases
LCL_PCModal
LCL_Paulson
LCL_PrincipiaMathematica
LCL_S10Modal
LCL_StrongNormalization
MGT_KampsCNF
MGT_KampsFOF
NLP_DorisCNF
NLP_DorisFOF
NUM_CimattiEUF
NUM_Landau
NUM_Naproche
NUM_RDNArithmetic
NUM_RobinsonAEq
NUM_RobinsonAId
NUM_SumOfTwoSquares
PLA_BlocksWorld
PRO_Halcomb
QBF_SeidlEPR
QBF_SeidlFOF
QML_GoedelTranslation
REL_HoefnerCNF
REL_HoefnerFOF
SCT_ArrowCNF
SCT_ArrowTF1
SET_ILF
SET_Pastre
SET_QuaifeCNF
SET_QuaifeFOF
SEU_BinaryRelations
SEU_BushyMizar
SEU_ChainyMizar
SEU_RootMizarBushy
SEU_RootMizarChainyLarge
SEU_RootMizarChainySmall
SEU_RootMizarNormal
SEU_ZFCGlobal
SEU_ZFCLocal
SEV_KaliszykHOL
SWC_SWReuseCNF
SWC_SWReuseFOF
SWV_Armando
SWV_EPRMutex
SWV_FFTCNF
SWV_FFTTF1
SWV_FTATF1
SWV_HoareCNF
SWV_HoareTF1
SWV_HuffmanTF1
SWV_JinjaCNF
SWV_JinjaTF1
SWV_NASASimplified
SWV_NASAUnsimplified
SWV_NSSharedCNF
SWV_NSSharedTF1
SWV_Paulson
SWV_Piskac
SWW_FTAFOF
SWW_Filliatre1
SWW_Filliatre2
SWW_FixPointTFA
SWW_KumarCakeML
SWW_PaskevichTF1
SWW_SeparationLogic
SWW_SpecSharp
SYN_ALCCNF
SYN_ALCFOF
SYN_Church
SYN_Harrison
SYN_KalishMontague
SYN_PeterAndrews
SYN_SchmidtPSAT
SYN_SchmidtQBF
SYO_SiderModal