ALG THM_RFO_NEQ_CNF_NHN         1
ALG THM_RFO_PEQ_CNF_NUE         2
ALG THM_RFO_PEQ_CNF_UEQ         3
ALG THM_RFO_SEQ_CNF_NHN         3
ANA THM_RFO_NEQ_CNF_HRN         3
ANA THM_RFO_NEQ_CNF_NHN        10
ANA THM_RFO_SEQ_CNF_HRN         3
ANA THM_RFO_SEQ_CNF_NHN         3
BOO SAT_RFO_EQU_CNF_NUE         1
BOO SAT_RFO_PEQ_CNF_UEQ         5
BOO THM_RFO_PEQ_CNF_NUE         2
BOO THM_RFO_PEQ_CNF_UEQ        42
BOO THM_RFO_SEQ_CNF_HRN        18
CAT SAT_RFO_EQU_CNF_NUE         6
CAT THM_RFO_NEQ_CNF_NHN         1
CAT THM_RFO_PEQ_CNF_NUE         5
CAT THM_RFO_SEQ_CNF_HRN        31
CAT THM_RFO_SEQ_CNF_NHN        15
COL SAT_RFO_PEQ_CNF_UEQ         5
COL THM_RFO_PEQ_CNF_NUE        17
COL THM_RFO_PEQ_CNF_UEQ       114
COL THM_RFO_SEQ_CNF_HRN        24
COM THM_EPR_FOF         3
COM THM_RFO_NEQ_CNF_HRN         2
COM THM_RFO_NEQ_CNF_NHN         3
COM THM_RFO_SEQ_CNF_HRN         1
FLD THM_RFO_NEQ_CNF_NHN       281
GEO THM_EPR_CNF         1
GEO THM_RFO_EQU_FOF        73
GEO THM_RFO_NEQ_CNF_HRN         2
GEO THM_RFO_SEQ_CNF_NHN       235
GRA THM_EPR_CNF         1
GRP SAT_EPR_CNF        50
GRP SAT_RFO_EQU_CNF_NUE         5
GRP SAT_RFO_PEQ_CNF_UEQ         2
GRP THM_EPR_CNF        51
GRP THM_RFO_EQU_FOF         1
GRP THM_RFO_NEQ_CNF_HRN        20
GRP THM_RFO_NEQ_CNF_NHN         4
GRP THM_RFO_PEQ_CNF_NUE        67
GRP THM_RFO_PEQ_CNF_UEQ       135
GRP THM_RFO_SEQ_CNF_HRN        27
GRP THM_RFO_SEQ_CNF_NHN        16
HEN THM_RFO_PEQ_CNF_NUE        11
HEN THM_RFO_SEQ_CNF_HRN        53
HWC THM_RFO_SEQ_CNF_HRN         4
HWV THM_RFO_NEQ_CNF_NHN        10
HWV THM_RFO_SEQ_CNF_HRN         4
KRS SAT_RFO_NEQ_CNF         8
KRS THM_EPR_CNF         1
KRS THM_RFO_NEQ_CNF_NHN         8
LAT SAT_RFO_PEQ_CNF_UEQ         3
LAT THM_EPR_CNF         2
LAT THM_RFO_PEQ_CNF_NUE         7
LAT THM_RFO_PEQ_CNF_UEQ        27
LAT THM_RFO_SEQ_CNF_HRN         6
LAT THM_RFO_SEQ_CNF_NHN         2
LCL SAT_EPR_FOF         1
LCL SAT_RFO_EQU_CNF_NUE        10
LCL SAT_RFO_NEQ_CNF         2
LCL SAT_RFO_PEQ_CNF_UEQ         3
LCL THM_EPR_CNF         2
LCL THM_EPR_FOF         2
LCL THM_RFO_NEQ_CNF_HRN       278
LCL THM_RFO_PEQ_CNF_NUE         1
LCL THM_RFO_PEQ_CNF_UEQ        29
LCL THM_RFO_SEQ_CNF_HRN       178
LCL THM_RFO_SEQ_CNF_NHN         1
LDA THM_RFO_PEQ_CNF_UEQ         3
LDA THM_RFO_SEQ_CNF_HRN         2
LDA THM_RFO_SEQ_CNF_NHN        18
MGT SAT_RFO_EQU_CNF_NUE        10
MGT SAT_RFO_FOF        10
MGT THM_EPR_CNF         5
MGT THM_EPR_FOF        22
MGT THM_RFO_EQU_FOF        37
MGT THM_RFO_NEQ_CNF_HRN        11
MGT THM_RFO_NEQ_CNF_NHN        10
MGT THM_RFO_NEQ_FOF         8
MGT THM_RFO_SEQ_CNF_HRN         2
MGT THM_RFO_SEQ_CNF_NHN        39
MSC SAT_EPR_CNF         1
MSC SAT_EPR_FOF         1
MSC SAT_RFO_NEQ_CNF         1
MSC THM_EPR_CNF         4
MSC THM_RFO_NEQ_CNF_HRN         1
MSC THM_RFO_NEQ_CNF_NHN         5
MSC THM_RFO_SEQ_CNF_NHN         1
NLP SAT_EPR_CNF        22
NLP SAT_EPR_FOF       226
NLP SAT_RFO_EQU_CNF_NUE       116
NLP SAT_RFO_NEQ_CNF        88
NLP THM_EPR_CNF         7
NLP THM_EPR_FOF        33
NLP THM_RFO_NEQ_CNF_NHN         4
NLP THM_RFO_SEQ_CNF_HRN         4
NLP THM_RFO_SEQ_CNF_NHN        17
NUM SAT_EPR_CNF         1
NUM SAT_RFO_EQU_CNF_NUE         1
NUM THM_RFO_NEQ_CNF_HRN        13
NUM THM_RFO_NEQ_CNF_NHN         8
NUM THM_RFO_SEQ_CNF_HRN         1
NUM THM_RFO_SEQ_CNF_NHN       285
PLA SAT_RFO_FOF         5
PLA THM_RFO_NEQ_CNF_HRN        28
PLA THM_RFO_NEQ_CNF_NHN         2
PUZ SAT_EPR_CNF         7
PUZ SAT_RFO_EQU_CNF_NUE         1
PUZ SAT_RFO_NEQ_CNF         1
PUZ THM_EPR_CNF        29
PUZ THM_EPR_FOF         2
PUZ THM_RFO_NEQ_CNF_HRN         7
PUZ THM_RFO_NEQ_CNF_NHN        15
PUZ THM_RFO_NEQ_FOF         1
PUZ THM_RFO_SEQ_CNF_HRN         1
PUZ THM_RFO_SEQ_CNF_NHN         4
RNG SAT_RFO_EQU_CNF_NUE         1
RNG SAT_RFO_PEQ_CNF_UEQ         2
RNG THM_RFO_NEQ_CNF_HRN         9
RNG THM_RFO_PEQ_CNF_NUE        11
RNG THM_RFO_PEQ_CNF_UEQ        56
RNG THM_RFO_SEQ_CNF_HRN        17
RNG THM_RFO_SEQ_CNF_NHN         3
ROB SAT_RFO_EQU_CNF_NUE         1
ROB THM_RFO_NEQ_CNF_HRN         1
ROB THM_RFO_PEQ_CNF_NUE         2
ROB THM_RFO_PEQ_CNF_UEQ        20
ROB THM_RFO_SEQ_CNF_HRN        12
SET SAT_RFO_EQU_CNF_NUE         4
SET THM_EPR_CNF         1
SET THM_EPR_FOF        17
SET THM_RFO_EQU_FOF       299
SET THM_RFO_NEQ_CNF_NHN        24
SET THM_RFO_NEQ_FOF         5
SET THM_RFO_SEQ_CNF_NHN       666
SWC SAT_RFO_EQU_CNF_NUE         1
SWC THM_RFO_EQU_FOF       422
SWC THM_RFO_SEQ_CNF_NHN       421
SWV SAT_RFO_FOF         7
SWV SAT_RFO_NEQ_CNF         7
SWV THM_EPR_CNF         1
SWV THM_RFO_NEQ_CNF_HRN         2
SWV THM_RFO_NEQ_CNF_NHN         1
SWV THM_RFO_NEQ_FOF         2
SWV THM_RFO_SEQ_CNF_NHN         8
SYN SAT_EPR_CNF        80
SYN SAT_EPR_FOF        82
SYN SAT_RFO_EQU_CNF_NUE         1
SYN SAT_RFO_NEQ_CNF        18
SYN SAT_RFO_PEQ_CNF_UEQ         2
SYN THM_EPR_CNF       308
SYN THM_EPR_FOF       190
SYN THM_RFO_EQU_FOF         7
SYN THM_RFO_NEQ_CNF_HRN        19
SYN THM_RFO_NEQ_CNF_NHN        42
SYN THM_RFO_NEQ_FOF         7
SYN THM_RFO_PEQ_CNF_UEQ         2
SYN THM_RFO_SEQ_CNF_NHN         8
TOP SAT_RFO_NEQ_CNF        15
TOP THM_RFO_NEQ_CNF_NHN         9