w3: reduced D-proofs for CCpCqrCCpqCpr,CCNpNqCqp,CCpqCCqrCpr,CCNppp

Proofs generated by reducing previous proofs based on data generated for
a848c40,
with additionally using '--extract -l 24' and '-g -1 -q 50 -l 24' to
generate proofs from w3 with up to 581 steps, then '--extract -l 22' and
'-g -1 -q 50 -l 22' for up to 1135 steps. (source: 'w3-topDB-shaky.txt')
+ comment superfluous debug line

Author: xamidi

data/w3.txt

@@ -7,94 +7,96 @@
 % Full summary: pmGenerator --transform data/w3.txt -f -n -t . -j 1
 % Step counting: pmGenerator --transform data/w3.txt -f -n -t . -p -2 -d
 %                pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
-% Compact (2135 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCpCqrsCCqrs,CCCpqrCqr,CCCNpqrCpr,CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp,CCNppCqp,CpCCpqCrq,CpCqCrp,CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy,CCCCCpqrCsrtCqt,CCCpCqrsCrs,CpCNNCqrCsCqr,CCNCCppNqrCqr,CCNNpqCpq,CpCqCrNNp,CCpqCNNpq,CCNpqCNCrpq,CCNpqCNCrCspq,CCCpqCNprCsCNpr,CCpNCNppCqNCNpp,CNCpqCrCsp,CCpCpqCpq,CCpqCNCprq,CCCpqrCNpr,CCpqCCNppq,CpCCpqq,CCpqCCNqpq,CCpCqrCqCpr
-% Concrete (20789800 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
+% Compact (2367 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCpCqrsCCqrs,CCCCCpqrCqrsCts,CCCpqrCqr,CCCNpqrCpr,CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp,CCCCNpqCrqpCsp,CpCCpqCrq,CpCqCrp,CCCCCCpqCrqsNttCut,CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy,CCCCCpqrCsrtCqt,CCCpCqrsCrs,CCpNCCqCrqpCsNCCqCrqp,CCNCCpCqpNrsCrs,CCCpqCNprCsCNpr,CpCCNCqrrCqr,CCpqCNNpq,CCNNpqCpq,CCNpqCNCrpq,CCNpqCNCrCspq,CCpNCNppCqNCNpp,CNCpqCrCsp,CCpCpqCpq,CCpqCNCprq,CCCpqrCNpr,CCpqCCNppq,CpCCpqq,CCpqCCNqpq,CCpCqrCqCpr
+% Concrete (5271958 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
 
     CpCCNqCCNrsCptCCtqCrq = 1
 [0] CCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqp = D11
 [1] CCNpCCNqrCCCNsCCNtuCCvCCNwCCNxyCvzCCzwCxwaCCasCtsbCCbpCqp = D1[0]
 [2] CCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqv = D[0]1
 [3] CCCpCCqrCsrtCCCqrCsrt = D[1]1
 [4] CCNpCCNqrCCCCsCCtuCvuwCCCtuCvuwxCCxpCqp = D1[3]
-[5] CCCpCCCqrCsrtuCCCCqrCsrtu = D[4]1
-[6] CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw = D[3][0]
-[7] CCCNpqCCCNrCCNstCCuCCNvCCNwxCuyCCyvCwvzCCzrCsrqCCqaCpa = D[3][1]
-[8] CCCNpCCNqCCNrsCNptCCtqCrqCCCrqpCqpCCCCCrqpCqpuCvu = D[2][6]
-[9] CCCCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqvwCxw = D[8][0]
-[10] CCCCCpCCqrCsrtCCCqrCsrtuCvu = D[8][1]
-[11] CCCpCqrsCCqrs = DD1[9]1
-[12] CCCCCpCCqrCsrtCCCqrCsrtCuCCCqrCsrtCCCuCCCqrCsrtvCwv = D[3]D[3][4]
-[13] CCCCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpwCxCCqwCpwCCCxCCqwCpwyCzy = D[3]D[3]D1[6]
-[14] CCCCCpqrCqrsCts = DD[11][0]1
-[15] CCCCCCpqCrqsCtsuCqu = DD[11]DD[3]111
-[16] CCpqCrCpq = D[11][9]
-[17] CCCpqrCqr = DDD[14]D[3][2]1[0]
-[18] CCCNpqrCpr = D[0]D[10][11]
-[19] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1D[5]D[3]DD[14]11
-[20] CCNppCqp = D[0]D[18][0]
+[5] CCCpCCCNqCCNrsCtuCCuqCrqvwCCCCNqCCNrsCtuCCuqCrqvw = DD1[2]1
+[6] CCCpCCCqrCsrtuCCCCqrCsrtu = D[4]1
+[7] CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw = D[3][0]
+[8] CCCNpqCCCNrCCNstCCuCCNvCCNwxCuyCCyvCwvzCCzrCsrqCCqaCpa = D[3][1]
+[9] CCCNpCCNqCCNrsCNptCCtqCrqCCCrqpCqpCCCCCrqpCqpuCvu = D[2][7]
+[10] CCCCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqvwCxw = D[9][0]
+[11] CCCCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqpyCCyzCaz = D[5][8]
+[12] CCCCCpCCqrCsrtCCCqrCsrtuCvu = D[9][1]
+[13] CCCpCqrsCCqrs = DD1[10]1
+[14] CCCCCpCCqrCsrtCCCqrCsrtCuCCCqrCsrtCCCuCCCqrCsrtvCwv = D[3]D[3][4]
+[15] CCCCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpwCxCCqwCpwCCCxCCqwCpwyCzy = D[3]D[3]D1[7]
+[16] CCCCCpqrCqrsCts = DD[13][0]1
+[17] CCCCCCpqCrqsCtsuCqu = DD[13]DD[3]111
+[18] CCCNpqCCCCrstCstqCCquCpu = D[3]DD[16]11
+[19] CCpqCrCpq = D[13][10]
+[20] CCpqCCCpqrCsr = D[13][11]
+[21] CCCpqrCqr = DDD[16]D[3][2]1[0]
+[22] CCCNpqrCpr = D[0]D[12][13]
+[23] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1D[6][18]
+[24] CCNppCqp = D[0]D[22][0]
+[25] CpCqCrq = DD[16][16]1
+[26] CCNpCCNqrCCsCtCutvCCvpCqp = D1[25]
 
 % Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 67 steps
-[21] CpCqp = DDD[14][14]11
+[27] CpCqp = D[25]1
 
-[22] CCNpCCNqrCCsCtsuCCupCqp = D1[21]
-[23] CCCCNpqCrqpCsp = D[0]D[15]DD[3][7][3]
-[24] CpCCpqCrq = DD[1]DDD[3]D[3]D1[7][3][11][0]
-[25] CCNpCCNqrCCCCNstCCuCvuwCCwxCsxyCCypCqp = D1D[11][22]
-[26] CpCqCrp = D[17][16]
-[27] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[11][25]
-[28] CCCCCpqrCsrtCqt = DD[11]DD[3]D[11]1[20]1
+[28] CCNpCCNqrCCsCtsuCCupCqp = D1[27]
+[29] CCCCNpqCrqpCsp = D[0]D[17]DD[3][8][3]
+[30] CCCNpqCCrCsCtsqCCquCpu = D[3][26]
+[31] CpCCpqCrq = DD[1]DDD[3]D[3]D1[8][3][13][0]
+[32] CpCqCrp = D[21][19]
+[33] CCCCCCpqCrqsNttCut = D[0]D[21]DDD1[6]1D[6][10]
+[34] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[13]D1D[13][28]
+[35] CCCCCpqrCsrtCqt = DD[13]DD[3]D[13]1[24]1
 
 % Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 127 steps
-[29] CpCNpq = D[18]D[6][20]
+[36] CpCNpq = D[22]D[7][24]
 
-[30] CCCpCqrsCrs = DD1[20]DD[13][5][11]
+[37] CCCpCqrsCrs = DD1[24]DD[15][6][13]
 
 % Identity principle (Cpp), i.e. 0→0 ; 135 steps
-[31] Cpp = DD[18]D[0][24]1
+[38] Cpp = DD[22]D[0][31]1
 
-[32] CCNpCCNqrCCsstCCtpCqp = D1[31]
-[33] CpCNNCqrCsCqr = D[23]DD[11]D[3][25]D[23]D[1]DD[0]D[10]D[0]DD[12]DD1[2]1[11]DD[0]DDD[3]D[3]D1D[5][3][11][11][10]
-[34] CCNCCppNqrCqr = D[27]D[32]D[33][33]
-[35] CCCppNqCqr = D[18][34]
-[36] CCNNpqCpq = D[27]D[19]D[17]DD[27]D[19]D[34][26][26]
-[37] CpCqCrNNp = D[36][26]
-[38] CpCqCrNNCNps = D[18][37]
-[39] CCpqCNNpq = D[27]D[19][37]
-[40] CCpqCNCNNprq = D[27]D[19][38]
-[41] CpCNNCNqqq = D[20]D[40][20]
-[42] CCNpqCNCrpq = D[27]D[19]D[39]D[17][37]
-[43] CCNpqCNCNprq = D[27]D[19]D[39][38]
-[44] CCNpqCNCrCspq = D[27]D[19]D[39]D[30][37]
-[45] CCNpCqpCrCqp = D[19]D[42][26]
-[46] CpCCNCqrrCqr = D[45][24]
-[47] CCpqCCCrrpq = D[32][46]
-[48] CCCpqCNprCsCNpr = D[19]D[43]D[28]D[24][35]
+[39] CCNpCCNqrCCsstCCtpCqp = D1[38]
+[40] CCpNCCqCrqpCsNCCqCrqp = D[28]DD[29]DD[6]D[3]D1[13]D[29]D[1]DD[0]D[12]D[0]DD[14][5][13]DD[0]DDD[3]D[3]D1D[6][3][13][13][12]1
+[41] CCNCCpCqpNrsCrs = D[18][40]
+[42] CpCqCrNCCsCtsNp = D[41][32]
+[43] CCCpqCNprCsCNpr = D[23]D[35]D[20]D[22]DD[13][26]D[22][40]
+[44] CpCCNCqrrCqr = DD[39]D[21]DDD[13]D1DDD[16]D[3]D[3]D1[11]1[0]1DD[3][11][41][29]
+[45] CCpqCCCrrpq = D[39][44]
+[46] CCpqCNNpq = DD[33]DD[30]D[39]D[22]D[13][42][31]1
+[47] CCNNpqCpq = D[34]D[23]D[35]D[20]DD[22]D[39]D[41][31]1
+[48] CpCqCrNNp = D[47][32]
+[49] CpCqCrNNCNps = D[22][48]
 
-% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 6541 steps
-[49] CCNppp = D[36]D[41][41]
+% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 2225 steps
+[50] CCNppp = D[47]DD[33]DD[30]D[39]D[22][42][24]1
 
-[50] CpCNCqrCNqs = D[48][48]
-[51] CCpNCNppCqNCNpp = D[19]D[39]D[28]D[24]D[47][49]
-[52] CNCpqCrCsp = DDD[47][36]DD[19]D[43][26]D[39][45]D[44]DD[48]DD[0]DD[12][5][11][10]D[50][50]
-[53] CCpCpqCrCpq = D[19][52]
-[54] CpCCqCqrCqr = D[53][53]
-[55] CCpCpqCpq = D[54][54]
-[56] CCpqCNCprq = D[27]D[19]DD[55][48]D[36]D[17]D[11][16]
-[57] CCCpqrCNpr = D[27]D[19]D[56][37]
-[58] CCpqCCNppq = DD[11]D1[1]D[19]DD[27]DD[27]D[19]D[39]DD[27][51][26]D[57][51][26]
-[59] CCNCpqrCCrqCpq = DD[58][30]D[44]1
-[60] CCpCqCprCqCpr = D[55]D[19]D[42][52]
-[61] CpCCpqq = DD[60]D[15][13]DD[22][46][55]
-[62] CCpqCCNqpq = D[19]DDD[11][19]D[58]D[28][55][58]
+[51] CCNpqCNCrpq = D[34]D[23]D[46]D[21][48]
+[52] CCNpqCNCrCspq = D[34]D[23]D[46]D[37][48]
+[53] CCpNCNppCqNCNpp = D[23]D[46]D[35]D[31]D[45][50]
+[54] CNCpqCrCsp = DDD[45][47]DD[23]DD[34]D[23]D[46][49][32]D[46]D[23]D[51][32]D[52]DD[43]DD[0]DD[14][6][13][12]1
+[55] CCpCpqCrCpq = D[23][54]
+[56] CpCCqCqrCqr = D[55][55]
+[57] CCpCpqCpq = D[56][56]
+[58] CCpqCNCprq = D[34]D[23]DD[57][43]D[47]D[21]D[13][19]
+[59] CCCpqrCNpr = D[34]D[23]D[58][48]
+[60] CCpqCCNppq = DD[13]D1[1]D[23]DD[34]DD[34]D[23]D[46]DD[34][53][32]D[59][53][32]
+[61] CCpCqCprCqCpr = D[57]D[23]D[51][54]
+[62] CCNCpqrCCrqCpq = DD[60][37]D[52]1
+[63] CpCCpqq = DD[61]D[17][15]DD[28][44][57]
+[64] CCpqCCNqpq = D[23]DDD[13][23]D[60]D[35][57][60]
 
-% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 1193987 steps
-[63] CCNpNqCqp = D[36]D[60]DD[62]D[17][35]D[42]D[55]D[40][44]
+% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 303787 steps
+[65] CCpqCCqrCpr = DDD1[58]D[27]D[60][63][62]
 
-% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 1196969 steps
-[64] CCpqCCqrCpr = DDD1[56]D[21]D[58][61][59]
+% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 306275 steps
+[66] CCNpNqCqp = D[47]D[61]DD[64]D[21]D[22][41]D[51]D[57]DD[34]D[23][49][52]
 
-[65] CCCCpqCrqsCCrps = D[64][64]
-[66] CCpCqrCqCpr = D[65]D[64][61]
+[67] CCCCpqCrqsCCrps = D[65][65]
+[68] CCpCqrCqCpr = D[67]D[65][63]
 
-% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 18391835 steps
-[67] CCpCqrCCpqCpr = D[66]D[65]D[59]DD[66]D[57][62]D[66]D[65][57]
+% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 4659203 steps
+[69] CCpCqrCCpqCpr = D[68]D[67]D[62]DD[68]D[59][64]D[68]D[67][59]

metamath/DRuleParser.cpp

@@ -964,8 +964,7 @@ vector<DProofInfo> DRuleParser::parseDProofs_raw(const vector<string>& dProofs,
 						// 2. Obtain substitutions via unification and partial cloning
 						map<string, shared_ptr<DlFormula>> substitutions;
 						if (!DlCore::tryUnifyTrees(antecedent, conditional_children[0], &substitutions)) {
-							if (debug)
-								cerr << formulas.size() << ". " << DlCore::formulaRepresentation_traverse(formulas.back()) << "\t\t" << dReasons.back() << endl;
+							//#cerr << formulas.size() << ". " << DlCore::formulaRepresentation_traverse(formulas.back()) << "\t\t" << dReasons.back() << endl;
 							if (exceptionOnUnificationFailure)
 								throw invalid_argument("DRuleParser::parseDProofs(): Failed to find unification for " + DlCore::formulaRepresentation_traverse(antecedent) + " and " + DlCore::formulaRepresentation_traverse(conditional_children[0]) + ".");
 							else