The formula CCCCppqrCCsCrtCqCs is easily provable in BCI*:
			1. CCpqCCrpCrq                                                           [B]                  2. CCpCqrCqCpr                                                          [C]                  3. CCppCqq                                                                      [I*] D1.1  =   4. CCpCqrCpCCsqCsr D2.1  =   5. CCpqCCqrCpr D2.3 =   6. CpCCqqp D4.2 =   7. CCpCqrCCsqCsCpr D5.6 =   8. CCCCppqrCqr D7.7  =   9. CCpCqrCpCCsCrtCqCst D9.8 = 10. CCCCppqrCCsCrtCqCst                                     [The axiom]
		It, in turn, delivers B, C, and I*.  My original derivation of the latter three from it runs 34 lines long (though I note that Larry Wos has since used OTTER to find a shorter (29-line) proof).
			D1.1 D2.1 D2.3 D1.4 D5.3 D6.1 D2.7 D1.8 D2.9 D9.10 D11.11 D8.11 D12.12 D13.14 D1.14 D14.15 D16.13 D1.18 D19.17 D2.20 D21.21 D13.22 D23.23 D23.1 D1.24 D25.24 D26.27 D25.28 D14.29 D30.25 D31.31 D15.32 D14.33	= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =	1. CCCCppqrCCsCrtCqCst                              [The axiom]    2. CCpCCCqCrsCCttCqsuCrCpu    3. CpCCCCqqrCssCrCCtCpuCtu    4. CpCqCCpCrrCCsCqtCst    5. CCpCCqCCCCrrsCttCCuCqvCuvwCsCpw    6. CCCCppqCrrCsCqCCtCsuCtu    7. CpCCqqCCrCpsCrs    8. CCppCqCCrCqsCrs    9. CCpCCqCCrCqsCrstCCuuCpt  10. CCppCCqCCrCCsCrtCstuCqu  11. CCppCCqqCCrCstCsCrt  12. CCppCCqCrsCrCqs  13. CpCCqCprCqr  14. CCpCqrCqCpr                                                     [Com]  15. CCpCCCqCrsCrCqstCpt  16. CCpCCqCCrrstCCqsCpt  17. CpCCpCCCqCrsCrCqstt  18. CCpqCCrrCpq  19. CCpCCCqqCCrrstCsCpt  20. CpCCqqp  21. CCppCqq                                                                 [I*]  22. Cpp  23. CCpCCqqrCpr  24. CCCppCCqqrr  25. CCCCppqrCqCCrss  26. CCpCqrCCCssqCpr  27. CCCppqCCqrr  28. CCCppCqrCCCssqr  29. CCpqCCCCCrrpqss  30. CCCCCppqrsCCqrs  31. CCpqCpCCqrr  32. CCpqCCCpCCqrrss  33. CCpqCCqrCpr  34. CCpqCCrpCrq                                                     [B]
		© Dolph Ulrich, 2007