Suppose we set up a correspondence between the definition of a well-formed formula in M and a meaningful expression in a system P in Polish notation such that each type of well-formed formula in M has a correspondent meaningful expression in P. The correspondence goes from M to P and from P to M.
The following will use a slightly different definition of a wff than many authors use. The definition will go as follows:
Any letter in nopqrstuvwxyz is a propositional wff.
Any letter in abcdefghijklm is a variable wff.
All variable wffs are wffs.
All propositional wffs are wffs.
If α is wff, then so is Nα.
If α is a wff, if β is a wff also, then Cαβ is a wff.
Variable wffs can get substituted by any meaningful expression (wff) in any formula (wff) in which the statement form (wff) appears. Propositional wffs can't get substituted by any meaningful expression.
Thus, we can address the above question by seeing if we can write a shorter than 30 line proof of p starting from the premiss NCpNq in a system P with the above definition of a wff with the following axiom schema:
We have a definition:
Def. Kab is defined as NCaNb
And the only rule of inference is C-detachment; from a wff of the form C$\alpha$$\beta$ and a wff of the form $\alpha$, we may infer a wff of the form $\beta$.
Premiss 1 Kpq
by 1 and the definition of Kab 2 NCpNq
Ax1 a/NCpNq, b/Na 3 CNCpNqCNaNCpNq
3 * C2-4 4 CNaNCpNq
Ax3 b/CpNq 5 CCNaNCpNqCCpNqa
5 * C4-6 6 CCpNqa
Ax1 a/CCpNqa, b/CNNqNp 7 CCCpNqaCCNNqNpCCpNqa
7 * C6-8 8 CCNNqNpCCpNqa
Ax2 a/CNNqNp, b/CpNq, c/a 9 CCCNNqNpCCpNqaCCCNNqNpCpNqCCNNqNpa
9 * C8-10 10 CCCNNqNpCpNqCCNNqNpa
Ax3 a/Nq, b/p 11 CCNNqNpCpNq
10 * C11-12 12 CCNNqNpa
Ax1 a/CCNqNpa, b/Np 13 CCCNNqNpaCNpCCNNqNpa
13 * C12-14 14 CNpCCNNqNpa
Ax2 a/Np, b/CNNqNp, c/a 15 CCNpCCNNqNpaCCNpCNNqNpCNpa
15 * C14-16 16 CCNpCNNqNpCNpa
Ax 1 a/Np, b/NNq 17 CNpCNNqNp
16 * C17-18 18 CNpa
18 a/NCNpa 19 CNpNCNpa
Ax 3 a/p, b/CNpa 20 CCNpNCNpaCCNpap
20 * C19-21 21 CCNpap
21 * C18-22 22 p
Twenty-two is less than thirty. So is twenty-one if we ignore the 1st step. Can step 20 get eliminated? Can there get written a twenty-one step proof?
For accepting this answer, the above system might differ substantially from Mendelson's and thus might not work.
I got an outline for constructing a previous proof (see earlier postings here) from this first-order hyper-resolution proof of OTTER written by the late William McCune at Argonne National Laboratory:
-----> EMPTY CLAUSE at 0.17 sec ----> 2433 [hyper,2,2424] $F.
Length of proof is 10. Level of proof is 10.
---------------- PROOF ----------------
1  -P(C(x,y))| -P(x)|P(y).
2  -P(p).
3  P(C(x,C(y,x))).
4  P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
5  P(C(C(N(x),N(y)),C(y,x))).
6  P(N(C(p,N(q)))).
8 [hyper,1,3,6] P(C(x,N(C(p,N(q))))).
12 [hyper,1,5,8] P(C(C(p,N(q)),x)).
13 [hyper,1,3,12] P(C(x,C(C(p,N(q)),y))).
24 [hyper,1,4,13] P(C(C(x,C(p,N(q))),C(x,y))).
76 [hyper,1,24,5] P(C(C(N(N(q)),N(p)),x)).
102 [hyper,1,3,76] P(C(x,C(C(N(N(q)),N(p)),y))).
116 [hyper,1,4,102] P(C(C(x,C(N(N(q)),N(p))),C(x,y))).
2404 [hyper,1,116,3] P(C(N(p),x)).
2419 [hyper,1,5,2404] P(C(x,p)).
2424 [hyper,1,2419,2419] P(p).
2433 [hyper,2,2424] $F.
------------ end of proof -------------