# Semi-Substitivity Example

Terminology note: Zeman's orignally coined term was "semisubstitutivity", which I find difficult to pronounce, and therefore to type. I personally prefer "semi-substitivity".

The best example of the use of semi-substitivity is the Rezus single axiom for BCIW logic. Since I used this as an example in a letter to the Association for Automated Reasoning (AAR) newsletter, I'm just going to repeat the original version of that letter here. (The editor found it too long, and an edited version was produced, referencing the text here for more detail.)

# Response to Dr. Larry Wos' president's column in the June 2010AARNewsletter

I was holed up on vacation in Hamilton, Montana having an uneventful time biking and hiking during the day, and working on J. J. Zeman's semisubstitutivity in the evenings. I had just gone on record telling a few people that, while it was a very interesting topic, semi-substitivity really didn't have any practical use in automated theorem proving.

Then, what to my wondering eyes should appear but the June AAR newsletter. And in it Larry Wos gave a challenge that proved me wrong. In the column, Larry posed a two part challenge, the one part being to generate a computer proof that the Rezus single axiom for BCIW logic was a theorem of BCIW. [The problem being that it is huge, and that causes problems for many automated theorem provers.] The other part of the challenge, in typical Larry Wos style, was to show a general method of proving such complex expressions from simple axioms.

I think that it should be noted that Dr. Bob Veroff, Dr. Larry Wos, and probably others have already published computer proofs that the Rezus axiom is a theorem of BCIW, so my just having such a proof is nothing particularly new or interesting. And, in fact, hand generated proofs existed long before the computer generated ones.

I have, however, enclosed with my proof a new technique for attacking large expressions of this sort. And I have enclosed both a "native" semi-substitivity proof that was generated using this technique, and that proof reduced to a more traditional Condensed Detachment proof. My technique is not the general method asked for, but it is a novel (and extremely effective in this case) technique for attacking large expressions. The new technique produces a semi-substitivity proof of the expression given, and that proof can be easily (mechanically) converted to a more traditional proof.

Just using semisubstitivity as the inference rule isn't actually particularly interesting. Semi-substitivity has MUCH worse fanout at any given step than a standard Condensed Detachment, or a typical Modus Ponens and Uniform Substitution proof. Without some trick to reduce the search space it would be a much worse approach than the traditional methods.

So, I hear you think, "What is the trick here?".

I'm afraid that the trick does depend on semi-substitivity, which is probably unfamiliar to most of the readers of the newsletter. I refer you to my web page on the topic for a quick introduction:

The short explaination is that if one had something of the form (p > q) and of the form (q > p) in most reasonable logics, one would have license to replace p by q, or q by p, anywhere in any theorem [Substitution of equivalents] without compromising validity. A subtly obvious question is whether having *JUST* the conditional (p > q), instead of the bi-conditional equivalence, buys you anything. The surprising answer is yes. For logics such as BCIW, with just implication and no other operators, it buys you something very clean. In BCIW, for example, if you have (p > q), there are positions in any expression where p (if it exists) can be replaced by q without compromising validity. This surprising fact is joined by the less obvious and more surprising fact that in all other positions in the expression q (if it exists) can be replaced by p. [Proofs on the web page.]

So semi-substitivity licenses you to do strategic surgery inside of theorems, which makes dealing with large expressions somewhat more tractable. But the problem of doing mechanical search with it is as bad, or worse, than with traditional methods.

OK, we now have enough tedious background to explain the actual trick.

Given a theorem of the form (p > q) and an alleged theorem that you are working on, semi-substitivity licenses either (depending on the position in the theorem) replacement of p by q, or of q by p, without compromising validity. (This assumes that all the operators that dominate the position obey semi-substivity, which is trivially true for BCIW since it has only one operator, and it obeys the rule.) But what can you say about replacements in the opposite direction than those licensed replacements, other than that they do NOT necessarily preserve validity? What CAN be said is that those replacements can be undone by a validity preserving licensed replacement. So, *** and here is the trick ***, any sequence of ONLY replacements in the opposite directon of the licensed directions, from an given expression to a *known valid* theorem (such as an axiom), can be run in the reverse (licensed) direction to produce a validity preserving proof from the axiom to the original starting point. And reduction of the given alleged theorem to an axiom can be very very simple and clean.

The slickest example I'm aware of is the Rezus theorem that Larry offered: [I'm going to use polish notation here because infix notation of expressions of this large size is totally unreadable (at least to me).] The alleged theorem we want to prove is (in Polish Notation):

```
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCCv17v17CCv18v18CCv19v19CCv20v20Cv16v21v21v22v22
```

And to make the explanation readable, I'll first exhibit an annotated version of a graph of the expression. The annotation is:

```
Symbol #:  direction licensed, position, graphic
```

positions are given as strings of "A"'s (for Antecedent) and "C"'s (for Consequent). So, for example, "CCA" means the Consequent of the Consequent of the Antecedent.

```
># : sym   direction position  diagram.

1: C     +                  .- C
|
2: C     -             A       .- C
|  |
3: C     +            AA       |  .- C
|  |  |
4: x     -           AAA       |  |  .- x
|  |  |
5: C     +           CAA       |  |  .- C
|  |     |
6: C     -          ACAA       |  |     .- C
|  |     |  |
7: C     +         AACAA       |  |     |  .- C
|  |     |  |  |
8: y     -        AAACAA       |  |     |  |  .- y
|  |     |  |  |
9: y     +        CAACAA       |  |     |  |  .- y
|  |     |  |
10: C     -         CACAA       |  |     |  .- C
|  |     |     |
11: C     +        ACACAA       |  |     |     .- C
|  |     |     |  |
12: z     -       AACACAA       |  |     |     |  .- z
|  |     |     |  |
13: z     +       CACACAA       |  |     |     |  .- z
|  |     |     |
14: C     -        CCACAA       |  |     |     .- C
|  |     |        |
15: C     +       ACCACAA       |  |     |        .- C
|  |     |        |  |
16: u     -      AACCACAA       |  |     |        |  .- u
|  |     |        |  |
17: u     +      CACCACAA       |  |     |        |  .- u
|  |     |        |
18: C     -       CCCACAA       |  |     |        .- C
|  |     |           |
19: C     +      ACCCACAA       |  |     |           .- C
|  |     |           |  |
20: v     -     AACCCACAA       |  |     |           |  .- v
|  |     |           |  |
21: v     +     CACCCACAA       |  |     |           |  .- v
|  |     |           |
22: C     -      CCCCACAA       |  |     |           .- C
|  |     |              |
23: x     +     ACCCCACAA       |  |     |              .- x
|  |     |              |
24: w     -     CCCCCACAA       |  |     |              .- w
|  |     |
25: w     +          CCAA       |  |     .- w
|  |
26: C     -            CA       |  .- C
|     |
27: C     +           ACA       |     .- C
|     |  |
28: C     -          AACA       |     |  .- C
|     |  |  |
29: C     +         AAACA       |     |  |  .- C
|     |  |  |  |
30: C     -        AAAACA       |     |  |  |  .- C
|     |  |  |  |  |
31: v6    +       AAAAACA       |     |  |  |  |  .- v6
|     |  |  |  |  |
32: v7    -       CAAAACA       |     |  |  |  |  .- v7
|     |  |  |  |
33: C     +        CAAACA       |     |  |  |  .- C
|     |  |  |     |
34: C     -       ACAAACA       |     |  |  |     .- C
|     |  |  |     |  |
35: v7    +      AACAAACA       |     |  |  |     |  .- v7
|     |  |  |     |  |
36: v8    -      CACAAACA       |     |  |  |     |  .- v8
|     |  |  |     |
37: C     +       CCAAACA       |     |  |  |     .- C
|     |  |  |        |
38: v6    -      ACCAAACA       |     |  |  |        .- v6
|     |  |  |        |
39: v8    +      CCCAAACA       |     |  |  |        .- v8
|     |  |  |
40: C     -         CAACA       |     |  |  .- C
|     |  |     |
41: C     +        ACAACA       |     |  |     .- C
|     |  |     |  |
42: C     -       AACAACA       |     |  |     |  .- C
|     |  |     |  |  |
43: C     +      AAACAACA       |     |  |     |  |  .- C
|     |  |     |  |  |  |
44: C     -     AAAACAACA       |     |  |     |  |  |  .- C
|     |  |     |  |  |  |  |
45: v9    +    AAAAACAACA       |     |  |     |  |  |  |  .- v9
|     |  |     |  |  |  |  |
46: C     -    CAAAACAACA       |     |  |     |  |  |  |  .- C
|     |  |     |  |  |  |     |
47: v9    +   ACAAAACAACA       |     |  |     |  |  |  |     .- v9
|     |  |     |  |  |  |     |
48: v10   -   CCAAAACAACA       |     |  |     |  |  |  |     .- v10
|     |  |     |  |  |  |
49: C     +     CAAACAACA       |     |  |     |  |  |  .- C
|     |  |     |  |  |     |
50: v9    -    ACAAACAACA       |     |  |     |  |  |     .- v9
|     |  |     |  |  |     |
51: v10   +    CCAAACAACA       |     |  |     |  |  |     .- v10
|     |  |     |  |  |
52: C     -      CAACAACA       |     |  |     |  |  .- C
|     |  |     |  |     |
53: C     +     ACAACAACA       |     |  |     |  |     .- C
|     |  |     |  |     |  |
54: C     -    AACAACAACA       |     |  |     |  |     |  .- C
|     |  |     |  |     |  |  |
55: v11   +   AAACAACAACA       |     |  |     |  |     |  |  .- v11
|     |  |     |  |     |  |  |
56: v12   -   CAACAACAACA       |     |  |     |  |     |  |  .- v12
|     |  |     |  |     |  |
57: C     +    CACAACAACA       |     |  |     |  |     |  .- C
|     |  |     |  |     |     |
58: C     -   ACACAACAACA       |     |  |     |  |     |     .- C
|     |  |     |  |     |     |  |
59: v12   +  AACACAACAACA       |     |  |     |  |     |     |  .- v12
|     |  |     |  |     |     |  |
60: v13   -  CACACAACAACA       |     |  |     |  |     |     |  .- v13
|     |  |     |  |     |     |
61: C     +   CCACAACAACA       |     |  |     |  |     |     .- C
|     |  |     |  |     |        |
62: v11   -  ACCACAACAACA       |     |  |     |  |     |        .- v11
|     |  |     |  |     |        |
63: v13   +  CCCACAACAACA       |     |  |     |  |     |        .- v13
|     |  |     |  |     |
64: v14   -     CCAACAACA       |     |  |     |  |     .- v14
|     |  |     |  |
65: v14   +       CACAACA       |     |  |     |  .- v14
|     |  |     |
66: v15   -        CCAACA       |     |  |     .- v15
|     |  |
67: v15   +          CACA       |     |  .- v15
|     |
68: C     -           CCA       |     .- C
|        |
69: C     +          ACCA       |        .- C
|        |  |
70: v16   -         AACCA       |        |  .- v16
|        |  |
71: C     +         CACCA       |        |  .- C
|        |     |
72: C     -        ACACCA       |        |     .- C
|        |     |  |
73: C     +       AACACCA       |        |     |  .- C
|        |     |  |  |
74: v17   -      AAACACCA       |        |     |  |  .- v17
|        |     |  |  |
75: v17   +      CAACACCA       |        |     |  |  .- v17
|        |     |  |
76: C     -       CACACCA       |        |     |  .- C
|        |     |     |
77: C     +      ACACACCA       |        |     |     .- C
|        |     |     |  |
78: v18   -     AACACACCA       |        |     |     |  .- v18
|        |     |     |  |
79: v18   +     CACACACCA       |        |     |     |  .- v18
|        |     |     |
80: C     -      CCACACCA       |        |     |     .- C
|        |     |        |
81: C     +     ACCACACCA       |        |     |        .- C
|        |     |        |  |
82: v19   -    AACCACACCA       |        |     |        |  .- v19
|        |     |        |  |
83: v19   +    CACCACACCA       |        |     |        |  .- v19
|        |     |        |
84: C     -     CCCACACCA       |        |     |        .- C
|        |     |           |
85: C     +    ACCCACACCA       |        |     |           .- C
|        |     |           |  |
86: v20   -   AACCCACACCA       |        |     |           |  .- v20
|        |     |           |  |
87: v20   +   CACCCACACCA       |        |     |           |  .- v20
|        |     |           |
88: C     -    CCCCACACCA       |        |     |           .- C
|        |     |              |
89: v16   +   ACCCCACACCA       |        |     |              .- v16
|        |     |              |
90: v21   -   CCCCCACACCA       |        |     |              .- v21
|        |     |
91: v21   +        CCACCA       |        |     .- v21
|        |
92: v22   -          CCCA       |        .- v22
|
93: v22   +             C       .- v22
```

The axioms of the system are:

• B: CCpqCCrpCrq
• C: CCpCqrCqCpr
• I: Cpp
• W: CCpCpqCpq

Or in possibly more familiar notation:

• B: (p > q) > ((r > p) > (r > q))
• C: (p > (q > r)) > (q > (p > r))
• I: p > p
• W: ( p > (p > q) ) > (p > q)

In order to avoid making this a truly ugly example, I'll introduce some template lemmas1 to make this short and sweet. And I'll work from the right to the left so that any unprocessed part of the expression is still numbered as above, and I don't have to reconstruct the diagram above after each replacement.

The template lemmas are all of the form

```
(( {axiom or theorem} > s) > s)
```

Each is trivially (4 or less steps from the axioms) provable from the axioms:

```
B' simplify: CCCCpqCCqrCprss  # Note that this is not based on B, it is
# based on B'.
I  simplify: CCCppqq
W  simplify: CCCCpCpqCpqrr
MP simplify: CCCpCCpqqrr
```

Scanning from the right to the left in the expression, the first place we match a template is at symbol 84, where we match I simplify. In this position the reverse (q replaced by p) is licensed, so the unlicensed (p replaced by q) will be used: [*** Since, oddly enough, All replacements in this proof occur at negative positions, I'm not going to keep repeating this part]

```
84: CCCppqq, p/v20, q/Cv16v21, applied at CCCACACCA
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCCv17v17CCv18v18CCv19v19Cv16v21v21v22v22
```

Continuing our right to left scan, the next place we match a template is at symbol 80, where we match I simplify

```
80: CCCppqq, p/v19, q/Cv16v21, applied CCCACACCA
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCCv17v17CCv18v18Cv16v21v21v22v22
```

And then we match at symbol 76 with I simplify

```
76: CCCppqq, p/v18, q/Cv16v21, applied at CACACCA
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCCv17v17Cv16v21v21v22v22
```

At symbol 72 we match I simplify

```
72: CCCppqq, p/v17, q/Cv16v21, applied at ACACCA
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCv16v21v21v22v22
```

At symbol 68 we match W simplify

```
68: CCCCpCpqCpqrr, p/v16, q/v21, r/v22, applied at CCA
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15v22v22
```

At symbol 52 we match B' simplify

```
52: CCCCpqCCqrCprss, p/v11, q/v12, r/v13, s/v14
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10v14v14v15v15v22v22
```

At symbol 42 we match W simplify

```
42: CCCCpCpqCpqrr, p/v9, q/v10, r/v14, applied at AACAACA
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCv14v14v15v15v22v22
```

At symbol 40 we match I simplify

```
40: CCCppqq, p/v14, q/v15, applied at CAACA
CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8v15v15v22v22
```

At symbol 28 we match B' simplify

```
28: CCCCpqCCqrCprss, p/v6, q/v7, r/v8, s/v15, applied at AACA
CCCxCCCyyCCzzCCuuCCvvCxwwCCv15v15v22v22
```

At symbol 26 we match I simplify

```
26: CCCppqq, p/v15, q/v22, applied at CA
CCCxCCCyyCCzzCCuuCCvvCxwwv22v22
```

At symbol 18 we match I simplify

```
18: CCppqq, p/v q/Cxw, applied at CCCCACAA
CCCxCCCyyCCzzCCuuCxwwv22v22
```

At symbol 14 we match I simplify

```
14: CCCppqq, p/u, q/Cxw, applied at CCACAA
CCCxCCCyyCCzzCxwwv22v22
```

At symbol 10 we match I simplify

```
10: CCCppqq, p/z, q/Cxw, applied at CACAA
CCCxCCCyyCxwwv22v22
```

At symbol 6 we match I simplify

```
6: CCCppqq, p/y, q/Cxw, applied at ACAA
CCCxCCxwwv22v22
```

At symbol 3 we match MP simplify

```
3: CCCpCCpqqrr, p/x, q/w, r/v22, applied at AA
Cv22v22
```

And this is just the axiom I.

```
1: Cv22v22, v22/p
```

Since the reduction, in only the directions opposite to the licenced directions has produced an axiom, we can now read off the proper (licensed direction) semi-substitivity proof of the theorem from the I axiom. (Just do the steps in the reverse order, reversing the substitutions.)

The only obvious hand wave I've done here was in choosing to use template lemmas and in the choice of which ones. (I originally had one for each of B, B', C, I, MP, and W, but just omitted the one that didn't get used.) In general, finding the reductions is generally not as clean as it is in Rezus style single axioms for systems, but I think this does give the rough idea. A process that would have worked to find the templates, and works a little more generally, is to collect all theorems a short distance from the axioms, and note whether or not they reduce in either the forward or reverse direction. Then walk the expression looking for instances of those that reduce in each position.

ASIDE: Few semi-substitivity proofs are likely to be this clean, but I think this example does show that the technique has promise. In my playing with the technique, it seems to have many properties of rewriting systems, but with restrictions on where the rewrites can occur. I personally expect, but have not pursued, that there is an analog of the Knuth-Bendix algorithm that can be worked out for semi-substitivity. It might make an interesting project for someone looking for something fun to play with.

# Wrap up

For some odd reason :), theorem proving programs are usually not set up to handle semi-substitivity as a rule of inference. Fortunately these proof steps can be mechanically converted to a more traditional proof. The semi-substitivity transformations for a given position can be easily written (and the proof mechanically generated from the position, or one can allow a traditional theorem prover to prove them). The template lemmas are a trivial few steps away from the axioms, and substituting them into the semi-substitivity theorems is obviously trivial.

Doing the above in my theorem prover (shotgun) yields the traditional proof that follows: (The variable names are different, since my program canonicalizes variables in theorems in a slightly different manner than Larry's does... But the results are the same theorem...) Shotgun has done some optimizations on the proof in places where it saw a shortening of the direct translation of the above.

```
# ----------------- Proof: --------------------
# Produced Tue Jul 13 02:37:52 2010
# by the "shotgun" program, version 2010-01-07 0.01.007

#    --  Rules --

#  Condensed detachment for ">"
#      From |- p and |- Cpq,  produce the most general possible |- q.
#

#          --- Wish List ---

=wishlist "CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1CCw1w1CCx1x1CCy1y1Cu1z1z1p2p2" "BCIW REZUS"

#          --- Axioms ---
1:
=axiom "CCpqCCrpCrq" "B"
2:
=axiom "CCpCqrCqCpr" "C"
3:
# Rezus 3
=axiom "Cpp" "I"
4:
=axiom "CCpCpqCpq" "W"

#          --- Theorems ---

# Modus Ponens
5: CpCCpqq                                 # Condensed detachment, inference line 2 with line 3

# Rezus 6
6: CCCpCCpqqrr                             # Condensed detachment, inference line 5 with line 5

# I simplify
7: CCCppqq                                 # Condensed detachment, inference line 5 with line 3

# B'
8: CCpqCCqrCpr                             # Condensed detachment, inference line 2 with line 1

9: CCCCpqCprsCCqrs                         # Condensed detachment, inference line 8 with line 1

# Semi - CA
10: CCpqCCCrqsCCrps                         # Condensed detachment, inference line 9 with line 8

11: CCCCpqCrqsCCrps                         # Condensed detachment, inference line 8 with line 8

# Semi - ACA
12: CCpqCCCrCpstCCrCqst                     # Condensed detachment, inference line 11 with line 10

13: CCpCqrCpCCrsCqs                         # Condensed detachment, inference line 1 with line 8
14: CCpqCCCCrCqstuCCCrCpstu                 # Condensed detachment, inference line 13 with line 12
15: CCCCpCqrstCCCpCCCuuqrst                 # Condensed detachment, inference line 14 with line 7

# Rezus 10
16: CCCpCCCqqCprrss                         # Condensed detachment, inference line 15 with line 6

# Rezus 14
17: CCCpCCCqqCCrrCpsstt                     # Condensed detachment, inference line 15 with line 16

# Rezus 18
18: CCCpCCCqqCCrrCCssCpttuu                 # Condensed detachment, inference line 15 with line 17

# Rezus 26
19: CCCpCCCqqCCrrCCssCCttCpuuvv             # Condensed detachment, inference line 15 with line 18

20: CCCpqrCCpCCssqr                         # Condensed detachment, inference line 10 with line 7

# Rezus 28
21: CCCpCCCqqCCrrCCssCCttCpuuCCvvww         # Condensed detachment, inference line 20 with line 19

# B' Simplify
22: CCCCpqCCqrCprss                         # Condensed detachment, inference line 5 with line 8
23: CCpqCCCrCCqstuCCrCCpstu                 # Condensed detachment, inference line 11 with line 12
24: CCCpCCqrstCCpCCCCCuvCCvwCuwqrst         # Condensed detachment, inference line 23 with line 22

# Rezus 40
25: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxyyzz
# Condensed detachment, inference line 24 with line 21

26: CCCpCCCqrstuCCpCCCqCCvvrstu             # Condensed detachment, inference line 12 with line 20

# Rezus 42
27: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCyyzzp1p1
# Condensed detachment, inference line 26 with line 25

28: CCCCpCpqCpqrr                           # Condensed detachment, inference line 5 with line 4
29: CCpqCCCrCCCsqtuvCCrCCCsptuv             # Condensed detachment, inference line 9 with line 23
30: CCpqCCCrCCCsCptuvwCCrCCCsCqtuvw         # Condensed detachment, inference line 11 with line 29
31: CCpqCCCrCCCsCCqtuvwxCCrCCCsCCptuvwx     # Condensed detachment, inference line 11 with line 30
32: CCCpCCCqCCrstuvwCCpCCCqCCCCCxCxyCxyrstuvw
# Condensed detachment, inference line 31 with line 28
# Rezus 52
33: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzp1p1q1q1r1r1
# Condensed detachment, inference line 32 with line 27

34: CCpqCCCrCCCsCCCtquvwxyCCrCCCsCCCtpuvwxy # Condensed detachment, inference line 9 with line 31
35: CCCpCCCqCCCrstuvwxCCpCCCqCCCrCCCyzCCzp1Cyp1stuvwx
# Condensed detachment, inference line 34 with line 22

# Rezus 68
36: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1u1u1
# Condensed detachment, inference line 35 with line 33

37: CCpqCCCrCsqtCCrCspt                     # Condensed detachment, inference line 9 with line 10
38: CCCpCqrsCCpCqCCtCCtuurs                 # Condensed detachment, inference line 37 with line 6

# Rezus 72
39: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCu1v1v1w1w1
# Condensed detachment, inference line 38 with line 36

40: CCpqCCCrCsCptuCCrCsCqtu                 # Condensed detachment, inference line 11 with line 37
41: CCpqCCCrCsCCtpuvCCrCsCCtquv             # Condensed detachment, inference line 9 with line 40
42: CCpqCCCrCsCCtCquvwCCrCsCCtCpuvw         # Condensed detachment, inference line 11 with line 41
43: CCCpCqCCrCstuvCCpCqCCrCCCwwstuv         # Condensed detachment, inference line 42 with line 7

# Rezus 76
44: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1Cu1w1w1x1x1
# Condensed detachment, inference line 43 with line 39

# Rezus 80
45: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1CCw1w1Cu1x1x1y1y1
# Condensed detachment, inference line 43 with line 44

# Rezus 84
46: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1CCw1w1CCx1x1Cu1y1y1z1z1
# Condensed detachment, inference line 43 with line 45
# Wish list theorem: BCIW REZUS
47: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1CCw1w1CCx1x1CCy1y1Cu1z1z1p2p2
# Condensed detachment, inference line 43 with line 46

# Final proof had 47 lines (43 steps)
# ------------------ End proof --------------
```

# Footnotes:

1: The question has been asked, "How did you choose those helper theorems? I went out a few inference steps and checked how many times they each appeared in parts of the Rezus formula, and tried the most popular. Looking at the result, I added MP by hand, and ran it and it worked.