Ax1 CaCba
Ax2 CCaCbcCCabCac
Ax3 CCNbNaCba

premiss                      1 CpCqr
Ax2 a/p, b/q, c/r            2 CCpCqrCCpqCpr
2 * C1-3                     3 CCpqCpr
Ax1 a/CCpqCpr, b/q           4 CCCpqCprCqCCpqCpr
4 * C3-5                     5 CqCCpqCpr
Ax2 a/q, b/Cpq, c/Cpr        6 CCqCCpqCprCCqCpqCqCpr
6 * C5-7                     7 CCqCpqCqCpr
Ax1 a/q, b/p                 8 CqCpq
7 * C7-9                     9 CqCpr