Here's my thirteen-step derivation of
CCCpqCCrpCrqCss /  {(pq)[(rp)(rq)]}(ss) from the axioms B, C, and I*:
 

 

                    1. CCpqCCrpCrq                   B       (pq)[(rp)(rq)]
                2. CCpCqrCqCpr                   C      
[p
(qr)][q(pr)]
               
   3. CCppCqq                             I*     (p
p)(qq)

D1.1     =   4. CCpCqrCpCCsqCsr                    [
p
(qr)]{p[(sq)(sr)]}
D1.2     =   5. CCpCqCrsCpCrCqs                   {
p
[q(rs)]}{p[r(qs)]}
D2.1     =   6. CCpqCCqrCpr                             (
p
q)[(qr)(pr)]
D1.3     =   7. CCpCqqCpCrr                              [
p
(qq)][p(rr)]
D5.5     =   8. CCpCqCrsCrCpCqs                   {
p
[q(rs)]}{r[p(qs)]}
D5.4     =   9. CCpCqrCCsqCpCsr                    [
p
(qr)]{(sq)[p(sr)]}
D5.7     = 10. CCpCqqCrCpr                              [
p
(qq)][r(pr)]
D1.7      = 11. CCpCqCrrCpCqCss                    {
p
[q(rr)]}{p[q(ss)]}
D6.8        =  12. CCCpCqCrstCCqCrCpst                     [{p
[q(rs)]}t][{q[r(ps)]}t]
D9.9     = 13. CCpCqrCCsCrtCpCsCqt           [p
(qr)][[s(rt)]{p[s(qt)]}]
D12.10 = 14. CCCpqCpCrqCsCrs                   {(p
q)[p(rq)]}[s(rs)]
D11.13 = 15. CCCpCqrCqsCCpCsrCtt           {[p
(qr)](qs)}{[p(sr)](tt)}
D15.14 = 16. CCCpqCCrpCrqCss              {(p
q)[(rp)(rq)]}(ss)
 


© Dolph Ulrich, 2007