w2: found D-proof for CCNppp (781 steps)

Proof was generated by reducing a Prover9 proof (with a D-proof of
fundamental length 5488897783) based on data generated for
a848c40.
The corresponding Prover9 search was configured with all hints encoded
in w2's top1000SmallestConclusions_1to43Steps.txt.

Author: xamidi

data/w2.txt

@@ -6,20 +6,40 @@
 %
 % Full summary: pmGenerator --transform data/w2.txt -f -n -t . -j 1
 % Step counting: pmGenerator --transform data/w2.txt -f -n -t . -p -2 -d
-%                pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq -p -2 -d
-% Compact & concrete (213 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq -j -1
+%                pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -p -2 -d
+% Compact (638 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCqCrp
+% Concrete (1008 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1 -e
 
     CpCCqCprCCNrCCNstqCsr = 1
 [0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
-[1] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDD[0]1111
+[1] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = DD[0]11
+[2] CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp = D[1]1
+[3] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[2]1
+[4] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][3]
 
 % Identity principle (Cpp), i.e. 0→0 ; 35 steps
-[2] Cpp = DD[0]DD[0][0][1][1]
+[5] Cpp = DD[0][4][3]
+
+[6] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
+[7] CpCqCrCsCtq = DDDDD1DD[0][6][3]1[3]11
+[8] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[7]1
 
 % Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 53 steps
-[3] CpCqp = DDD1DDDDDD1DD[0]DD1[0]1[1]1[1]111[0]1
+[9] CpCqp = DD[8][0]1
 
-[4] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = DDD1[0]1[1]
+[10] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[6][3]
+[11] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][10]
+[12] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[10]D[11][3]
 
 % Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 57 steps
-[5] CpCNpq = DD[4]DD[0][4][1]1
+[13] CpCNpq = D[12]1
+
+[14] CCpCCqqrCCNrCCNstpCsr = D1[5]
+[15] CpCqCrp = DD[0][11][7]
+[16] CpCqCCCNCrCCsCrtCCNtCCNuvsCutwNqx = D[11]1
+[17] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[3]
+[18] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp = DD1DD[17][0]11
+[19] CpCCNqCCNrsCNqCCNCtpuNCvCCwCvxCCNxCCNyzwCyxCrq = D[2][3]
+
+% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 781 steps
+[20] CCNppp = DDDD[14]1DDD[0]DDD1[15][0][16]DDD1DDD[0]D1[18][3]DD[0][17][3]DDD1[8]1[3][19]1DDD[0][15]DDD1DD[0]D1[16]DD[0]DDD1DDD1[6]111[3]1DDD1DDD1D[18][3]1[3]1[3][19]1DDD1D[12]DD[0][1]DD[0]DDD1DDD1[4]111[3]1[14]D[4]DD1[9]1