name
degree
#rule_before
#rule_after
s(H
2
)
#rule_after - e(R)
ASK93_1
0
2
2
0
2
ASK93_6
0
11
11
0
9
BD94_collapse
1
5
5
N/A
BD94_peano
1
4
4
N/A
BD94_sqrt
2
3
4
0
3
BGK94_D08
2
6
21
2
5
BGK94_D10
2
6
21
1
4
BGK94_D12
2
6
20
2
5
BGK94_D16
2
6
20
2
5
BH96_fac8_theory
1
6
6
N/A
Chr89_A2
2
5
18
0
4
Chr89_A3
2
7
16
0
6
KK99_linear_assoc
0
2
2
0
1
LS94_G0
2
8
13
1
4
Les83_fib
1
9
9
N/A
Les83_subset
1
12
12
N/A
OKW95_dt1_theory
1
11
11
N/A
SK90_3.01
2
4
11
0
3
SK90_3.02
0
3
3
1
2
SK90_3.03
2
5
11
0
3
SK90_3.04
1
4
8
N/A
SK90_3.05
1
4
13
N/A
SK90_3.06
1
5
12
N/A
SK90_3.07
1
5
15
N/A
SK90_3.08
2
5
4
0
2
SK90_3.10
2
4
8
0
3
SK90_3.11
0
4
3
0
3
SK90_3.12
2
4
9
0
2
SK90_3.13
0
6
6
0
3
SK90_3.14
0
7
8
1
5
SK90_3.15
2
8
7
1
4
SK90_3.16
1
4
4
N/A
SK90_3.17
1
3
5
N/A
SK90_3.18
0
5
6
2
4
SK90_3.19
0
9
7
1
4
SK90_3.20
1
10
11
N/A
SK90_3.21
1
9
4
N/A
SK90_3.23
0
4
8
1
4
SK90_3.24
0
3
2
0
2
SK90_3.25
0
1
2
0
1
SK90_3.27
0
8
3
0
3
SK90_3.28
0
9
18
0
6
SK90_3.29
0
7
8
2
7
SK90_3.30
1
3
3
N/A
SK90_3.31
1
3
3
N/A
SK90_3.32
1
3
2
N/A
SK90_3.33
0
3
3
0
2
TPTP-BOO027-1_theory
1
5
5
N/A
TPTP-COL053-1_theory
0
1
1
0
1
TPTP-COL056-1_theory
0
3
3
0
3
TPTP-COL060-1_theory
0
2
2
0
2
TPTP-COL085-1_theory
0
1
1
0
1
TPTP-GRP010-4_theory
2
4
11
1
3
TPTP-GRP011-4_theory
2
4
11
1
3
TPTP-GRP012-4_theory
2
4
10
0
2
slothrop_ackermann
1
3
3
N/A
slothrop_cge
2
6
20
0
4
slothrop_cge3
2
9
28
0
5
slothrop_endo
2
4
14
0
3
slothrop_equiv_proofs
1
12
23
N/A
slothrop_fgh
1
4
3
N/A
slothrop_groups
2
3
10
0
2
slothrop_groups_conj
2
5
10
0
2
slothrop_hard
0
2
2
1
2