Can the Negation of a Conditional Implying the First Atomic Proposition Get Proven in Around 50 Steps?

Question

The following uses Polish notation with the following definition for meaningful expressions.

1. All lower case letters are meaningful expressions.
2. If $\alpha$ is a meaningful expression, then so is N$\alpha$.
3. If $\alpha$ is a meaningful expression, if $\beta$ is a meaningful expression also, then C$\alpha$$\beta$ is a meaningful expression.

The axioms are

Ax1 CxCyx

Ax2 CCxCyzCCxyCxz

Ax3 CCNxNyCyx

The rules of inference are uniform substitution for any thesis of the system and C-detachment, from $\vdash$C$\alpha$$\beta$, from $\vdash$$\alpha$ also, we may infer $\vdash$$\beta$.

Can CNCxyx get proven in around 50 steps?

Answer 1

Counting the axioms as steps in the proof, the following consists of a less than 50 step which indicates an answer of yes.

                                                     Expansion Number

                       1 CxCyx   

                       2 CCxCyzCCxyCxz 

                       3 CCNxNyCyx 

1/CxCyx, y/z           4 CCxCyxCzCxCyx

4 * C1-5               5 CzCxCyx                            2 

1 x/CCNxNyCyx, y/z     6 CCCNxNyCyxCzCCNxNyCyx

6 * C3-7               7 CzCCNxNyCyx                        2

2 x/z, y/x, z/Cyx      8 CCzCxCyxCCzxCzCyx

8 * C5-9               9 CCzxCzCyx                          2

2 x/z, y/CNxNy, z/Cyx  10 CCzCCNxNyCyxCCzCNxNyCzCyx          

10 * C7-11             11 CCzCNxNyCzCyx                      2

11 z/Ny                12 CCNyCNxNyCNyCyx                    

1 x/Ny, y/Nx           13 CNyCNxNy

12 * C13-14            14 CNyCyx                             3

9 z/Ny, x/Cyx, y/z     15 CCNyCyxCNyCzCyx

15 * C14-16            16 CNyCzCyx                           2

2 x/Ny, z/x            17 CCNyCyxCCNyyCNyx

17 * C14-18            18 CCNyyCNyx                          2

11 z/CNyy, x/y, y/x    19 CCCNyyCNyNxCCNyyCxy

18 x/Nx                20 CCNyyCNyNx 

19 * C20-21            21 CCNyyCxy                           3

1 x/CCNyyCNyx, y/z     22 CCCNyyCNyxCzCCNyyCNyx

22 * C18-23            23 CzCCNyyCNyx                        2

2 x/CNyy, y/x, z/y     24 CCCNyyCxyCCCNyyxCCNyyy

24 * C21               25 CCCNyyxCCNyyy                      2

2 x/z, y/CNyy, z/CNyx  26 CCzCCNyyCNyxCCzCNyyCzCNyx

26 * 23-27             27 CCzCNyyCzCNyx                      2

25 x/Cxy               28 CCCNyyCxyCCNyyy

28 * C21-29            29 CCNyyy                             2

27 z/Ny, y/Cyx, x/z    30 CCNyCNCyxCyxCNyCNCyxz

16 z/NCyx              31 CNyCNCyxCyx

30 * C31-32            32 CNyCNCyxz                          3

1 x/CCNyyy, y/x        33 CCCNyyyCxCCNyyy

33 * C29-34            34 CxCCNyyy                           2

2 x/Ny, y/NCyx         35 CCNyCNCyxzCCNyNCyxCNyz

35 * C32-36            36 CCNyNCyxCNyz                       2

2 y/CNyy, z/y          37 CCxCCNyyyCCxCNyyCxy

37 * C34-38            38 CCxCNyyCxy                         2

9 z/CxCNyy, x/Cxy, y/z 39 CCCxCNyyCxyCCxCNyyCzCxy

39 * C38-40            40 CCxCNyyCzCxy                       2

40 x/CNyNCyx           41 CCCNyNCyxCNyyCzCCNyNCyxy 

36 z/y                 42 CCNyNCyxCNyy

41 * C42-43            43 CzCCNyNCyxy                        3

2 x/z, y/CNyNCyx, z/y  44 CCzCCNyNCyxyCCzCNyNCyxCzy

44 * C43-45            45 CCzCNyNCyxCzy                      2

45 z/NCxy, y/x, x/y    46 CCNCxyCNxNCxyCNCxyx

1 x/NCxy, y/NCxy       47 CNCxyCNxNCxy

46 * C47-48            48 CNCxyx                             3

I constructed the above proof with the help of this first-order, hyperresolution proof I found with OTTER as my assistant.

1 [] -P(C(x,y))| -P(x)|P(y).

2 [] -P(C(N(C(p,N(q))),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 [hyper,1,3,3] P(C(x,C(y,C(z,y)))).

8 [hyper,1,3,5] P(C(x,C(C(N(y),N(z)),C(z,y)))).

9 [hyper,1,4,6] P(C(C(x,y),C(x,C(z,y)))).

15 [hyper,1,4,8] P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).

30 [hyper,1,15,3] P(C(N(x),C(x,y))).

67 [hyper,1,9,30] P(C(N(x),C(y,C(x,z)))).

68 [hyper,1,4,30] P(C(C(N(x),x),C(N(x),y))).

136 [hyper,1,15,68] P(C(C(N(x),x),C(y,x))).

138 [hyper,1,3,68] P(C(x,C(C(N(y),y),C(N(y),z)))).

220 [hyper,1,4,136] P(C(C(C(N(x),x),y),C(C(N(x),x),x))).

240 [hyper,1,4,138] P(C(C(x,C(N(y),y)),C(x,C(N(y),z)))).

326 [hyper,1,220,136] P(C(C(N(x),x),x)).

353 [hyper,1,240,67] P(C(N(x),C(N(C(x,y)),z))).

459 [hyper,1,3,326] P(C(x,C(C(N(y),y),y))).

503 [hyper,1,4,353] P(C(C(N(x),N(C(x,y))),C(N(x),z))).

659 [hyper,1,4,459] P(C(C(x,C(N(y),y)),C(x,y))).

902 [hyper,1,9,659] P(C(C(x,C(N(y),y)),C(z,C(x,y)))).

1343 [hyper,1,902,503] P(C(x,C(C(N(y),N(C(y,z))),y))).

1859 [hyper,1,4,1343] P(C(C(x,C(N(y),N(C(y,z)))),C(x,y))).

2803 [hyper,1,1859,3] P(C(N(C(x,y)),x)).

4153 [hyper,2,2803] $F.