API tools faq
paste
Advertisement
xamidi

pmproofs-summary.txt

xamidi
Mar 3rd, 2024 (edited)
68
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 18.27 KB | Science | 0 0
raw download clone embed print report
  1. % Full summary: pmGenerator --transform data/pmproofs-summary.txt -f -n -t . -j 1
  2. % - infix formulas: pmGenerator --transform data/pmproofs-summary.txt -f -n -t . -j 1 -u
  3. % - to file: pmGenerator --transform data/pmproofs-summary.txt -f -n -t . -j 1 -u -o data/tmp.txt
  4. % Current summary:
  5. % - step counting: pmGenerator --transform data/pmproofs-summary.txt -f -n -t . -j -1 -p -2 -d
  6. % - infix formulas: pmGenerator --transform data/pmproofs-summary.txt -f -n -t . -j -1 -u
  7.  
  8. % Steps to generate this file in Bash via pmGenerator 1.2 and its released (quick'n'dirty) helper tools:
  9. % 1. Write all D-proofs from 'data/pmproofs.txt' (version 17-Apr-2023) to 'data/tmp.txt', but without duplicates and trivial proofs (i.e. of length 1):
  10. % $ ./dProofsFromDB data/pmproofs.txt data/tmp.txt 1 1
  11. % 2. Combine proofs in 'data/tmp.txt' to an abstract proof summary (based on default axioms, which are CpCqp,CCpCqrCCpqCpr,CCNpNqCqp).
  12. % $ ./pmGenerator --parse data/tmp.txt -f -n -s -o data/pmproofs-summary.txt
  13. %
  14. % The below steps are optional, but used to reduce the abstract proof summary size from 14569 bytes to 12059 bytes,
  15. % while still containing all 154 (non-trivial) proof results from pmproofs.txt of its current 196 theorems.
  16. %
  17. % 3. Obtain conclusions for all proofs in 'data/tmp.txt' via 'pmGenerator --parse data/tmp.txt -f -n -b',
  18. % and reformat them to be in a single comma-separated line, e.g. via:
  19. % $ ./pmGenerator --parse data/tmp.txt -f -n -b | sed -E 's/[0-9]+\. /,/g' | sed -E 's/^[^,].+//g' | sed -E 's/,printProofs.+//g' | tr -d '\r' | tr -d '\n'
  20. % Output: ",<L>", for <L> being the list of all 154 proof results from pmproofs.txt in normal Polish notation
  21. % (Not to be confused with ' ./formulasFromProofs CpCqp,CCpCqrCCpqCpr,CCNpNqCqp data/tmp.txt <output file>', which would generate a line with all used formulas, not only final conclusions.)
  22. % 4. Find extra conclusions necessary to reach a compact abstract proof summary:
  23. % $ ./findCompactSummary data/pmproofs-summary.txt <L>
  24. % Output mentions "<E>" as 'bestDedicatedConclusions' in the final iteration after a few minutes.
  25. % 5. Transform abstract proof summary to compact variant.
  26. % $ ./pmGenerator --transform data/pmproofs-summary.txt -f -n -t <L> -j -1 -s <E> -d -o data/pmproofs-summary.txt
  27. % (total command length: 4153 bytes)
  28. %
  29. % NOTE: <L> = CCNppp,CCNpqCNqp,CCpCqrCqCpr,CCpqCCrpCrq,CCpNpNp,CCpNqCqNp,CCpqCCqrCpr,Cpp,CNNpp,CpNNp,CCpqCNqNp,CpCNpq,CNpCpq,CpCCpqq,CNNpCCpqq,CCpCNqrCpCNrq,CCpCNqrCNCpqr,CCNCpqrCpCNqr,CCpqCCNrpCNqr,CCpqCCNprCNrq,CCpqCCNprCNqr,CCpCpqCpq,CCNpCqpCqp,CCNNpCpqCpq,CNCpqp,CNCpqNq,CNCpqCNpr,CNCpqCrNq,CNCpqCqr,CNpCCNqpq,CCNpqCCpqq,CCpqCCNpqq,CCNpqCCNpNqp,CCpqCCpNqNp,CCCNpqrCpr,CCCpqrCNpr,CCCpqrCCrpp,CCpqCCNCNpqrCNqr,CCpqCCNCNqprCNqr,CCpqCCpCqrCpr,CCpqCCNNqrCpr,CCpCqrCCspCCsqCsr,CCNCpqrCCNCpNrsCNCpqs,CCpCqrCCpCrsCpCqs,CCCpqCrsCrCqs,CNCpqNCNNpq,CNCNNpqNCpq,CNNCpqCNNpq,CCNNpqNNCpq,CpCqNCpNq,CpCqNCqNp,CNCpNqNCqNp,NNCpNNp,CNCpNqq,CCNCpNqrCpCqr,CCpCqrCNCpNqr,CNCCpqNCqrCpr,CNCCpqNCrpCrq,CNCpNCpqq,CCNCpNqrCNCpNNrNq,CNCpNqCrq,CCpqCNCprq,CCpqCNCrNpq,CNCCpqNCprCpNCqNr,CNCCpqNCrqCCNprq,CCpqCNCprNCqr,CNCCpqNCrsCNCpNrNCqNs,CNCCpqNCrsCCNprCNqs,NCCCpqCNqNpNCCNrNsCsr,NCCNCCpqNCrsNCCNsNrNCNqNpNCNCCNtNuNCNvNwNCCwvNCut,NCCNCCpNqNCNrsNCCqNpNCNsrNCNCCtNuNCNvwNCCuNtNCNwv,NCCpNNpNCNNqq,NCCCNCpNqrCNCpNNrNqNCCNCsNNtuCNCsut,NCCCNCpNqrCNCqrNpNCCNCsNtNuCNCuNsNt,NCCppNCqq,NCCNCpNqNCqNpNCNCrNsNCsNr,CNCNCCpqNCrsNNCCqtNCurNCCptNCus,NCCpNCpNpNCNCqNrr,NCCpCqpNCCNrrr,NCCCNpqCNqpNCCNrsCNsr,NCCNCNCpNqrNCpNNCqrNCNCsNNCtuNCNCsNtu,NCCCNCpqrCpCNqrNCCsCNtuCNCstu,CNCCpqNCrsNCCNCptNCqtNCNCruNCsu,CNCCpqNCrsNCCCNptCNqtNCCNruCNsu,CNCNCCpqNCrsNNCCtuNCvwNCCNCpNtNCqNuNCNCrNvNCsNw,CNCNCCpqNCrsNNCCtuNCvwNCCCNptCNquNCCNrvCNsw,NCCNCpNCqrCNNCpqNCpNrNCCNNCstNCsNuNCsNCtu,NCCCpNCqNrNCCpqNCprNCNCCstNCsuCsNCtNu,NCCpCNNCpqNCpNqNCCNNCrsNCrtr,NCCpNCCNpqNCNprNCNCCNstNCNsNts,NCCpCNpqNCCNrNCrsr,NCCpNCpNCNpqNCNCrsr,NCCNCpqNCNNpqNCNCNNrsNCrs,NCCNNCpqCNNpqNCCNNrsNNCrs,NCCNCpNNqNCNNpqNCNCNNrsNCrNNs,NCCNNCpNNqCNNpqNCCNNrsNNCrNNs,NCCNNppNCqNNq,NCCNCpNNqNCpqNCNCrsNCrNNs,NCCNNCpNNqCpqNCCrsNNCrNNs,NCCCpqCNNpqNCCNNrsCrs,NCCNCpqNCpNNqNCNCrNNsNCrs,NCCCpqCpNCpNqNCCrNCsNtCrt,NCCCpqNCCpNCpNqNCNCrsrNCNCCtNCuNvwCtv,NCCCpqNCCrCsrNCCNpqqNCNCtNCCNuvwCuw,CpNCCqNCqNpNCNCrsr,CpNCCqCrqNCCpss,NCCNCCpqNCprCpNCqNrNCCsNCtNuNCCstNCsu,NCCNCCpqNCrqCCNprqNCCCNstuNCCsuNCtu,NCCCNCpqCprCpCNqrNCCsCNtuCNCvtCsu,NCCCNCpqCrqCNCpNrqNCCNCsNtuCNCsvCtu,NCCCpNpNpNCqCrq,NCCCNpppNCqCrq,NCCNCCpqNCpNqNpNCNrNCCrsNCrt,NCCNCCpqNCNpqqNCrNCCsrNCtr,CNCCpqNCrsNCCCstCrtNCCquCpu,CNCCpqNCrsNCCCtpCtqNCCurCus,CNCCpqNCrsNCCNCCstNCupNCCrtNCuqNCNCCqvNCwrNCCpvNCws,NCNCNCCCNCpNqrCpCqrNCCsCtuCNCsNtuNNCCCvCwxCwCvxNCCyCzaCzCyaNNCCCbCcdCNCbNcdNCCNCeNfgCeCfg,CNCpNqNCCrqNCsp,CNNCCpqNCrsNCCsNqNCNrp,NNCNCCpqNCqpNNCCpNqNCNqp,NCCNCCNpqNNNrNCrNCNqpNCNCsNCNtuNCCNutNNNs,NCCNCCpqNCqpNNCCpNqNCNqpNCNNCCrNsNCNtuNCCusNCtr,NNCCpNpNCNpp,CNCNpNNqNCCprNCqs,NCCNNCCpqNCrsCNNCpNNqNCrNNsNCCNNCtNNuNCvNNwNNCCtuNCvw,NCCNCCpqNCqpCNNCpNqNCNpNNqNCCNNCrNsNCNtNNuNCCtsNCur,NCCNCNNCpNqNCNpNNqCNNCpNNqNCqNNpNCCNNCrNsNCtNNuNCNNCusNCNrNNt,NCCCNpqCCpqqNCCCrstCNrt,NCCCNCpqrCNCpqNCpNrNCCsNCtNuCsu,CNCpNCqrCqNCrNp,NCCCpNCCqrNCstNCCNCpNqNCpNrNCNCpNsNCpNtNCNCCNCuNvNCwNxNCNCuNyNCzNaCuNCCvxNCya,NCCNCpNCqrNCpNCNCsNqrNCNCtNCNCtNuvNCtNCuv,CNCCpqNCprCpNCCsrNCtq,NCCNCpNNCCpqrNCqNNCCpqrNCNCsNNCtNCsuNCuNNCtNCsu,NCCCpCpqCpqNCrCsr,NCCCCpqCrsCrCqsNCCtCuvCCtuCtv,NCCCpCqrCpCqNCpNrNCCsCtNCuNvCsCtv,CCpqNCCCprCpNCqNrNCCsNCtNuCsu,CpNCCCpqqNCrCsr,CpNCCqNCCrqNCspNCNCCptut,NCCCCNCNpqrsNCNCCpsNCqsNCrsNCNCNCCtuNCvuNCwuCCNCNtvwu,CNNCCpqNCrNCrNsNCCNCtNuuNCsp,CNNCCCNpqpNCrCNrsNCCtqNCuCvu,NCCCNCpNqrCpCqrNCCsCtuCNCsNtu,NCCNCCNpqNNqNCpNNqNCNCrsNCCNrts,NCCCNNCpqrCNprNCCNstCNNCstt,NCCNCCCNpqCNrsNCCNtuCNvsCNsNCCprNCtvNCCNwNCCxyNCzaNCCCNxwCNywNCCNzwCNaw,CCpNqNCCNCCNrpNqNCrNqNCNCstNCCNsut,NCCCpNCCqrNCstNCCCpqCprNCCpsCptNCNCCCuvCwxNCCyzCwaCwNCCvxNCza,CNCCpqNNCCrCstNCCupvNCCNCrNstNCpNCvNq,CCCCCpqCNrNsrtCCtpCsp,CCCpqpp,NCCNCCNCCpqNCrstNCuNCCsvNCrpNCCsNCCqtNCuvNCNCCruNCtrpNCNCCwNCCxyNCzaNCNCCxzNCybcNCCNCCcxNCxwyNCzNCCwaNCbc
  30. % <E> = CCpqCpCrq,CCpCqCrsCpCCqrCqs,CCpCNqNrCpCrq,CCpCqCCrqsCpCqs,CNNpCqp,CCpCqrCpCCrsCqs,CCNNCpqpCNNCpqq,CpCCqNNrCqr,CCpqCpNNq,CCpCqCrsCpCrCqs,CCpqCNNpq,CCpCqrCpCqNNr,CCpCqCNrrCpCqr,CCpNCqNrCpr,CCNNpqCpq,CCpqCpNNNNq,CCpqCpCrNCqNr,CCpNCqrCpq,CCCNpqrCCNqpr,CCpCqrCpCCqsCqNCrNs,CNCCpqrCCspCsq,CpCqNCCrqNCsp,CCpCqrCpCNrNq,CNCpqNCpNNq,CCpCqrCpCCqNsCqNCrs,CNCCpqNCrsCNCCstNCupNCCrtNCuq,CNCCpqNCqpNNCCpNqNCNqp
  31.  
  32. CpCqp = 1
  33. CCpCqrCCpqCpr = 2
  34. CCNpNqCqp = 3
  35. [0] CCpqCpCrq = D2D11
  36. [1] CCpCqCrsCpCCqrCqs = D2D12
  37. [2] CCpCNqNrCpCrq = D2D13
  38. [3] Cpp = DD211
  39. [4] CCpCpqCpq = DD22D21
  40. [5] CCpqCCrpCrq = D[1]1
  41. [6] CNpCpq = D[2]1
  42. [7] CCpqCCpCqrCpr = DD2D1D221
  43. [8] CCpCqCCrqsCpCqs = D2D1DD22D11
  44. [9] CNNpCqp = D[2][6]
  45. [10] CpCCpqq = DD2D1D2[3]1
  46. [11] CCpqCCqrCpr = DD2D1D2[5]1
  47. [12] CpCNpq = DD2D1D2[6]1
  48. [13] CCpCqrCCspCCsqCsr = DD2D1[1][5]
  49. [14] CNNpp = DD2[9]1
  50. [15] CCpCqrCpCCrsCqs = D2D1[11]
  51. [16] CCNNCpqpCNNCpqq = D2[14]
  52. [17] CpNNp = D3[14]
  53. [18] CCpCqrCqCpr = D[8]D[0]2
  54. [19] CCCpqrCNpr = DD2D1DD22D1[6]1
  55. [20] CCNppp = DD2D[2]D2[6]1
  56. [21] CpCCqNNrCqr = D1D2D1[14]
  57. [22] CCpqCpNNq = D2D1[17]
  58. [23] CCpCqCrsCpCrCqs = D2D1[18]
  59. [24] CCpCqrCCpCrsCpCqs = D[1][15]
  60. [25] CNNpCCpqq = DD2D1D2[3][9]
  61. [26] CNCpqCqr = D[8]D[0][6]
  62. [27] CCpqCNNpq = DD2D1DD22D2[9]1
  63. [28] CCpCqrCpCqNNr = D2D1[22]
  64. [29] CCpCqCNrrCpCqr = D2D1D2D1[20]
  65. [30] CNCpNqq = D3D[22]1
  66. [31] CCCNpqrCpr = DD2D1DD22D1[12]1
  67. [32] CCNpqCNqp = D[2][22]
  68. [33] CCpNCqNrCpr = D2D1[30]
  69. [34] CpCqNCpNq = D[2]DD2D1[16]1
  70. [35] CNCpNqCrq = D[2][26]
  71. [36] CCpNqCqNp = D[2][27]
  72. [37] CCNNpqCpq = DD2D1DD22D1[17]1
  73. [38] CNCpqCNpr = DD2D1DD22D1[6]D[0][6]
  74. [39] CCpCNqrCpCNrq = D2D1[32]
  75. [40] CNCpqp = D3D[22][6]
  76. [41] NCCCpCpqCpqNCrCsr = DD3D[16]D1[4]1
  77. [42] CCpqCpNNNNq = D2D1D3DD2D[2]D[2][9]1
  78. [43] CCpqCpCrNCqNr = D2D1[34]
  79. [44] CNpCCNqpq = DD2D1D2D1DD23D11D[1]D[0][6]
  80. [45] NCCppNCqq = DD3D[16]D1[3][3]
  81. [46] CCpNCqrCpq = D2D1[40]
  82. [47] CCCpqCrsCrCqs = D[8]D[0]D[1]D[8]1
  83. [48] CNNCpqCNNpq = DD2D1DD22D2[9][9]
  84. [49] CNCpqNq = D3D[22][9]
  85. [50] CCNpqCCNpNqp = D[2]D2[34]
  86. [51] CpCqNCqNp = DD2D1D2[34]1
  87. [52] CCpqCNCrNpq = DD2[5]D1[30]
  88. [53] NNCpNNp = D[17][17]
  89. [54] CCCNpqrCCNqpr = DD2[5]D1[32]
  90. [55] CpNCCqCrqNCCpss = DD2D1D3D[16]D11[10]
  91. [56] CCNNpCpqCpq = DD2D1[4][37]
  92. [57] CNCpqCrNq = DD2D1D[2]DD2D1DD22D1[9]1[6]
  93. [58] CCpqCCNNqrCpr = D[15][22]
  94. [59] CCCpqpp = DD2D1[20][19]
  95. [60] CCpCqrCpCCqsCqNCrNs = D2D1D[1][43]
  96. [61] CCpqCCNrpCNqr = DD2D1[39][5]
  97. [62] CNCCpqrCCspCsq = DD2D1[5][40]
  98. [63] CCpqCNCprq = DD2[5]D1[40]
  99. [64] NCCpCqpNCCNrrr = DD3D[16]D11[20]
  100. [65] NCCCNpppNCqCrq = DD3D[16]D1[20]1
  101. [66] CCNpCqpCqp = D[29][18]
  102. [67] CCpNpNp = DD2D1[20][27]
  103. [68] CpCqNCCrqNCsp = DD2D1D2D[2]DD2D1[16]D[0]1D[0]1
  104. [69] CCpqCCNprCNrq = DD2D1[54][5]
  105. [70] CCNNpqNNCpq = D[22][37]
  106. [71] CpNCCCpqqNCrCsr = DD2D[43][10]D11
  107. [72] CCNCpNqrCpCqr = DD2D1D2D[15][34]1
  108. [73] CCpqCNqNp = DD2D1[36][22]
  109. [74] CCpqCNCprNCqr = D[39]DD2D1D2D[1][9]1
  110. [75] NCCpNNpNCNNqq = DD3D[16]D1[17][14]
  111. [76] NCCNNppNCqNNq = DD3D[16]D1[14][17]
  112. [77] CCpCqrCpCNrNq = D2D1[73]
  113. [78] CNCNNpqNCpq = D3D[22][48]
  114. [79] CNCpNCpqq = DD2[30][40]
  115. [80] NCCCCpqCrsCrCqsNCCtCuvCCtuCtv = DD3D[16]D1[47]2
  116. [81] CCCpqrCCrpp = DD2D1D[29][11][19]
  117. [82] CNCpNqNCqNp = D3D[22]D[2][48]
  118. [83] CNCpqNCpNNq = D3D[22]DD2[21][14]
  119. [84] CNCpqNCNNpq = D3D[22]DD2D[1][9]D1[17]
  120. [85] CCpqCCpNqNp = DD2D1[36]D2[34]
  121. [86] CCpCqrCpCCqNsCqNCrs = D2D1D[1]D2D1D[2]D[28]DD2D1[16]1
  122. [87] NCCCpNpNpNCqCrq = DD3D[16]D1[67]1
  123. [88] CCNpqCCpqq = DD2D1DD2D1D[29][11]3[22]
  124. [89] CCpqCCNprCNqr = D[15][73]
  125. [90] NCCpCNpqNCCNrNCrsr = DD3D[16]D1[12]DD2D[2]D2DD2D1D2[6]D[0][6]3
  126. [91] CCpqCCNpqq = D[29][69]
  127. [92] NCCCpqCNNpqNCCNNrsCrs = DD3D[16]D1[27][37]
  128. [93] CCpCqrCNCpNqr = DD2D[1][63]D1[30]
  129. [94] NCCCNpqCNqpNCCNrsCNsr = DD3D[16]D1[32][32]
  130. [95] NCCCpqCNqNpNCCNrNsCsr = DD3D[16]D1[73]3
  131. [96] NCCCpqCpNCpNqNCCrNCsNtCrt = DD3D[16]D1D2[34][33]
  132. [97] NCCpNCpNpNCNCqNrr = DD3D[16]D1DD2DD2D1D231DD2D1[16]1[30]
  133. [98] CCNCpqrCpCNqr = DD2D1[39]D[23][32]
  134. [99] CCpCNqrCNCpqr = D[39]D[23][39]
  135. [100] CCNCpqrCCNCpNrsCNCpqs = D[15]D2D[43][40]
  136. [101] CNCCpqNCqrCpr = D3D[22]DD2D1D2[74]1
  137. [102] CNCCpqNCrpCrq = D3D[22]DD2D1D2D[77][5]1
  138. [103] NCCCpCqrCpCqNCpNrNCCsCtNCuNvCsCtv = DD3D[16]D1D2DD2D1[5][34]D2D1[33]
  139. [104] CNCpNqNCCrqNCsp = DD2D[43][35]D[2][38]
  140. [105] NCCpNCpNCNpqNCNCrsr = DD3D[16]D1DD2[34][12][40]
  141. [106] CNCpNCqrCqNCrNp = DD2D1D2D[2]D[28]DD2D1[2]DD2D1DD2D1D2D[1][9]1DD2D1[16]11
  142. [107] CCpqNCCCprCpNCqNrNCCsNCtNuCsu = DD2D[43]D[1][43]D1[33]
  143. [108] CpNCCqNCqNpNCNCrsr = DD2D[43][51]D1[40]
  144. [109] CNCNpNNqNCCprNCqs = DD2D[43]DD2D[1]D[0][6]D1[12]D[2][35]
  145. [110] NCCNNCpNNqCpqNCCrsNNCrNNs = DD3D[16]D1DD2[21][14]D[22][22]
  146. [111] CNCCpqNCprCpNCqNr = DD2D[1]DD2D1[2]DD2D1D2D1[16]DD2D1[0][40][30]
  147. [112] NCCNNCpqCNNpqNCCNNrsNNCrs = DD3D[16]D1[48][70]
  148. [113] CCpqCCNCNqprCNqr = D[15]D[77]D[29][5]
  149. [114] CNCCpqNCrsNCCCtpCtqNCCurCus = DD2D[43][62]D[1][35]
  150. [115] NCCCNpqCCpqqNCCCrstCNrt = DD3D[16]D1[88][19]
  151. [116] NNCCpNpNCNpp = D[17]DD2D1DD2DD2D1D[2]D2DD2D1D2[6][14]11[67]
  152. [117] NCCCNCpqrCNCpqNCpNrNCCsNCtNuCsu = DD3D[16]D1D2D[43][40][33]
  153. [118] CpNCCqNCCrqNCspNCNCCptut = DD2D[43][68]DD2D1D2[40]1
  154. [119] CNCCpqNCrsNCCCstCrtNCCquCpu = DD2D[43]DD2D1D2[5][35]DD2D1D2[5]D[2][38]
  155. [120] CCCCCpqCNrNsrtCCtpCsp = DD2D1D2DD2D1DD2D1D2D3DD2[6]DD2D1D[0]1D3D[22]D[15]D[23]DD2D1D2[2]D[0][6]211
  156. [121] CCNCpNqrCNCpNNrNq = DD2D1D[2]D2DD2D1DD2D1D2D1D[22][22]D[15]D2[34][9]1
  157. [122] NCCNCpqNCNNpqNCNCNNrsNCrs = DD3D[16]D1[84][78]
  158. [123] CNCCpqNCprCpNCCsrNCtq = D3D[22]DD2D1D2D[77]D[1]D2D1[68]1
  159. [124] NCCpNCCNpqNCNprNCNCCNstNCNsNts = DD3D[16]D1DD2D[43][12][12]D3D[22]DD2D1D2D2[34]1
  160. [125] NCCNCpNqNCqNpNCNCrNsNCsNr = DD3D[16]D1[82][82]
  161. [126] CCpqCCNCNpqrCNqr = D[15]D[77][91]
  162. [127] NCCNCpNNqNCpqNCNCrsNCrNNs = DD3D[16]D1D3D[22]D[28][14][83]
  163. [128] NCCNCpqNCpNNqNCNCrNNsNCrs = DD3D[16]D1[83]D3D[22]D[28][14]
  164. [129] NCCpCNNCpqNCpNqNCCNNCrsNCrtr = DD3D[16]D1DD2D1[27]DD2D1D2D2[34]1D3DD2DD2D1DD2D1D2D[2]DD2D1D2D[2][14]11[6][6]
  165. [130] CNNCCCNpqpNCrCNrsNCCtqNCuCvu = DD2D[43]D3D[22]DD2D[43]DD2D1D2D[2]D2D1D[22]11D1[12]D11
  166. [131] NCCCNCpNqrCpCqrNCCsCtuCNCsNtu = DD3D[16]D1[72][93]
  167. [132] NCCCNNCpqrCNprNCCNstCNNCstt = DD3D[16]D1DD2[5]D1D[22][6]DD2D1DD2D1DD2D1D2DD2D1D[29][5][14]13[22]
  168. [133] NCCNNCpNNqCNNpqNCCNNrsNNCrNNs = DD3D[16]D1DD2D1DD2[21][27][14]D[22]D[2]D[2][42]
  169. [134] NCCNCCpqNCpNqNpNCNrNCCrsNCrt = DD3D[16]D1D3D[22]DD2D1D2DD2D1[27]D2[34]1DD2D[43][6][6]
  170. [135] CNCCpqNCrqCCNprq = DD2D[1]DD2D1[2]DD2D1D2D1D2[6]DD2D[1]D[0][62]DD2D1[2]DD2D1[28]D[1][35]D1D11
  171. [136] NCCCpqNCCrCsrNCCNpqqNCNCtNCCNuvwCuw = DD3D[16]D1DD2D1D3D[16]D11[91]DD2D1[31][30]
  172. [137] NCCCpqNCCpNCpNqNCNCrsrNCNCCtNCuNvwCtv = DD3D[16]D1DD2D1DD2[34]D1[40]D2[34]DD2D1[33][40]
  173. [138] CNCCpqNCrsCNCpNrNCqNs = DD2D[60]DD2D1[63][40]DD2D1[52][30]
  174. [139] NCCCNCpqrCpCNqrNCCsCNtuCNCstu = DD3D[16]D1[98][99]
  175. [140] NCCNCpNNqNCNNpqNCNCNNrsNCrNNs = DD3D[16]D1D3D[22]DD2D1D[2]D[2][42][14]D3D[22]DD2D1DD2[21][27][14]
  176. [141] CNCCpqNCrsCNCCstNCupNCCrtNCuq = DD2D[1]DD2D1D2D1[51]DD2D[1]D[0][62]D1[30]DD2D1D2[62][35]
  177. [142] CNNCCpqNCrNCrNsNCCNCtNuuNCsp = DD2D[43]D1[30]D3D[22]DD2D[43][26]DD2D1DD2D1D2[34][46]1
  178. [143] CNCCpqNCrsCCNprCNqs = DD2D1D2D[39]D[23]DD2D1[77]DD2D1DD2[5]D1[73]DD2D1[15][5]1
  179. [144] NCCNCCpqNCNpqqNCrNCCsrNCtr = DD3D[16]D1D3D[22]DD2D1D2D[77][91]1DD2D[2]DD2D1[16]D[0]11
  180. [145] CCpNqNCCNCCNrpNqNCrNqNCNCstNCCNsut = DD2D[43]DD2D[60]D[39]D[8]D[0]D[1][5]D1[30]D1D3D[22]DD2D[1][9]D1[12]
  181. [146] NCCNCCpqNCprCpNCqNrNCCsNCtNuNCCstNCsu = DD3D[16]D1[111]DD2D[43][46][33]
  182. [147] NCCCpNCqNrNCCpqNCprNCNCCstNCsuCsNCtNu = DD3D[16]D1DD2D[43][46][33][111]
  183. [148] NCCNCCNpqNNqNCpNNqNCNCrsNCCNrts = DD3D[16]D1D3D[22]DD2D1DD2D1DD2D1DD22D1[22]1[91][14]D3D[22]DD2D[1][9]D1[12]
  184. [149] CNNCCpqNCrsNCCsNqNCNrp = DD2D[43]DD2D1D2D[77][68]1DD2D1D2D[39]DD2D1DD2D1D2D[43][6]1[6]1
  185. [150] CNCCpqNCrsNCCNCptNCqtNCNCruNCsu = D3DDD22D2[9]D1D[22]DDDD2D[1]D[0]D[1]D[0][5]D1[11]D3DDD22D2[9]D1D[22][74][74]
  186. [151] CNCNCCpqNCrsNNCCqtNCurNCCptNCus = DD2D[43]DD2DD2D1[5]D3DD2D1D3D3D[42]1[6]D3DD2D1D[22][12][6]DD2DD2D1[5]D3DD2D1D[22][12]1D3DD2D1D3D3D[42]11
  187. [152] NCCCNCpNqrCNCqrNpNCCNCsNtNuCNCuNsNt = DD3D[16]D1D[77][72]D[77]D[23]DD2D1D2D1[36]3
  188. [153] NCCCNCpNqrCNCpNNrNqNCCNCsNNtuCNCsut = DD3D[16]D1[121]D[39]D[23][72]
  189. [154] NCCNCCpqNCrqCCNprqNCCCNstuNCCsuNCtu = DD3D[16]D1[135]DD2D[43][31]D[8]1
  190. [155] CNCCpqNCrsNCCCNptCNqtNCCNruCNsu = D3DDD22D2[9]D1D[22]DDDD2D[1]D[0]D[1]D[0][5]D1[11]D3DDD22D2[9]D1D[22][89][89]
  191. [156] CNCCpqNCqpNNCCpNqNCNqp = D[22]DD2D[86]DD2D1DD2D1D2D1[67][11][30]DD2D1[85][40]
  192. [157] NCCNCNCpNqrNCpNNCqrNCNCsNNCtuNCNCsNtu = DD3D[16]D1D3D[22]DD2D1DD2D1[93]D2D1[14][14]D3D[22]DD2D1D[28][72][14]
  193. [158] NCCCNCpqCprCpCNqrNCCsCNtuCNCvtCsu = DD3D[16]D1DD2D1[47]D[23]DD2D1DD2D1DD2D1[2]D[23]DD2D1D2D1D2DD2D1D2D2[34]1[18][39][18]DD2D1DD2[5]D1[57]2
  194. [159] NCCNCCNpqNNNrNCrNCNqpNCNCsNCNtuNCCNutNNNs = DD3D[16]D1D3D[22]DD2D1D[28]DD2D1[54][36][14]D3D[22]DD2D1DD2D1DD2D1[36][54]D2D1[14][14]
  195. [160] NNCNCCpqNCqpNNCCpNqNCNqp = D[17][156]
  196. [161] NCCCpNCCqrNCstNCCCpqCprNCCpsCptNCNCCCuvCwxNCCyzCwaCwNCCvxNCza = DD3D[16]D1DD2D[43]D[1][46]D[1][33]DD2D[60]DD2D1[47][40]DD2D1[47][30]
  197. [162] CNCCpqNNCCrCstNCCupvNCCNCrNstNCpNCvNq = DD2D[43]DD2D1DD2D1[93][40][30]DD2D[60]DD2D1DD2D1D[8]1[30][30][40]
  198. [163] NCCNCpNCqrCNNCpqNCpNrNCCNNCstNCsNuNCsNCtu = DD3D[16]D1DD2D1D2D[77]D[86][14]1D3DD2D1DD2D[43]D[22][46]D2D1[49][14]
  199. [164] NCCNNCCpqNCrsCNNCpNNqNCrNNsNCCNNCtNNuNCvNNwNNCCtuNCvw = DD3D[16]D1DD2D1DD2D1[27]DD2D1DD2D1DD22[21]1D2D1[83][14]D[22]DD2D1DD2D1D2D1D3D[22]D[28][14]DD2D1DD22D1[22]1[37]
  200. [165] NCCNCCpNqNCNrsNCCqNpNCNsrNCNCCtNuNCNvwNCCuNtNCNwv = DD3D[16]D1DD2D[43]DD2D1[36][40]D[39][30]DD2D[43]DD2D1[36][40]D[39][30]
  201. [166] NCCNCCpqNCrsNCCNsNrNCNqNpNCNCCNtNuNCNvNwNCCwvNCut = DD3D[16]D1DD2D[43]D[77][30]D[77][40]DD2D[43]D[2][30]D[2][40]
  202. [167] NCCNCpNNCCpqrNCqNNCCpqrNCNCsNNCtNCsuNCuNNCtNCsu = DD3D[16]D1DD2D[43]D3D[22]D[28]D[23]D[1]D[0][6][30]DD2D[43]D3D[22]DD2D1D2D1D[22]1DD2D1D2D[2]D[28]DD2D1[16]11[30]
  203. [168] NCCCNCpqCrqCNCpNrqNCCNCsNtuCNCsvCtu = DD3D[16]D1D[39]DD2D1[47]DD2D1[77]D[23]DD2D1DD2D1D2D1D[29]2D2D1D[2]DD2D1D2[6][0][18]DD2D1DD2D1DD2D1DD2[5]D1D[2][38][2]2[32]
  204. [169] NCCNCpNCqrNCpNCNCsNqrNCNCtNCNCtNuvNCtNCuv = DD3D[16]D1DD2D[43][40]DD2D1[52][30]DD2D[43][40]D3D[22]DD2D1D2D[77]D[15][34]1
  205. [170] NCNCNCCCNCpNqrCpCqrNCCsCtuCNCsNtuNNCCCvCwxCwCvxNCCyCzaCzCyaNNCCCbCcdCNCbNcdNCCNCeNfgCeCfg = DD3D[16]D1DD3D[16]D1[131]DD3D[16]D1[18][18]DD3D[16]D1[93][72]
  206. [171] CNCNCCpqNCrsNNCCtuNCvwNCCCNptCNquNCCNrvCNsw = DD2D[2]DD2D1[16]D[0]DD2D[1]D[0]DD2D1[5]D3DD2D1D3D3D[42]1[6]DD2D1D2[5]D[0]D[2]DD2D[1]D[0]D[28]D3DD2D1D[22][12][6]D1[14]DD2D[1]D[0]D[1]D[2]DD2D[1]D[0]D[2][35]D11DD2D1D2[5]D[0]D[2]DD2D[1]D[0]D[28]D3DD2D1D[22][12]1D1[14]
  207. [172] NCCNCCpqNCqpNNCCpNqNCNqpNCNNCCrNsNCNtuNCCusNCtr = DD3D[16]D1[156]DD2D1DD2D[43]D[8]D[0]D[2]D[8]1DD2D1D[2][19][46][14]
  208. [173] NCCNCCpqNCqpCNNCpNqNCNpNNqNCCNNCrNsNCNtNNuNCCtsNCur = DD3D[16]D1DD2D1[27]DD2D[60]DD2D1[85][40]DD2D1DD2D1D2D1[67][11][30]DD2D1DD2D[43]DD2D1D[2]D[8]1[46]DD2D1D[2][19][33][37]
  209. [174] CNCCpqNCrsNCCNCCstNCupNCCrtNCuqNCNCCqvNCwrNCCpvNCws = DD2D[43][141]DD2DD2D1DD2D1[77]DD2D1DD2[5]D1[73]DD2D1D2D[1]D[0][5]D[0][11]DD2D1D2[5]D[2][38]D[1][35]
  210. [175] CNCNCCpqNCrsNNCCtuNCvwNCCNCpNtNCqNuNCNCrNvNCsNw = DD2D[43]DD2D[60]DD2D1DD2D1[63][40][40]DD2D1DD2D1[52][40][30]DD2D[60]DD2D1DD2D1[63][30][40]DD2D1DD2D1[52][30][30]
  211. [176] NCCNCNNCpNqNCNpNNqCNNCpNNqNCqNNpNCCNNCrNsNCtNNuNCNNCusNCNrNNt = DD3D[16]D1DD2D1[27]DD2D1DD2D1DD22[21]1DD2D[60]DD2D1DD2D1D[29][11]3[30]DD2D1DD2D1DD2D1D2D1[67]D[1]D2D1[6][14][40]DD2D1DD2D[43]DD2D1DD2D1D[22]3[33]D[8]1DD2D1D2D1D3D[22]D[2][9][19][37]
  212. [177] NCCCpNCCqrNCstNCCNCpNqNCpNrNCNCpNsNCpNtNCNCCNCuNvNCwNxNCNCuNyNCzNaCuNCCvxNCya = DD3D[16]D1DD2D[43]D[77]D[1]D2D1D[77][40]D[77]D[1]D2D1D[77][30]DD2D[60]DD2D1[2]DD2D1[47]D[2][40]DD2D1[2]DD2D1[47]D[2][30]
  213. [178] NCCNCCCNpqCNrsNCCNtuCNvsCNsNCCprNCtvNCCNwNCCxyNCzaNCCCNxwCNywNCCNzwCNaw = DD3D[16]D1DD2D[60]DD2D1DD2D1DD2D1[47][39][54][40]DD2D1DD2D1DD2D1[47][39][54][30]DD2D[43]DD2D1DD2D1DD2D1[54][39]2[46]DD2D1DD2D1DD2D1[54][39]2[33]
  214. [179] NCCCCNCNpqrsNCNCCpsNCqsNCrsNCNCNCCtuNCvuNCwuCCNCNtvwu = DD3D[16]D1DD2D[43]DD2D[43]DD2[5]D1DD2D1D2[6]D[0][12]DD2D1DD22D1DD2D1D2[6]D[0]11D[8]1D[2]DD2D[86]DD2D1DD2D[86]D[77][40]D[77][30][40]D[77][30]
  215. [180] NCCNCCNCCpqNCrstNCuNCCsvNCrpNCCsNCCqtNCuvNCNCCruNCtrpNCNCCwNCCxyNCzaNCNCCxzNCybcNCCNCCcxNCxwyNCzNCCwaNCbc = DD3D[16]D1DD2D[43]DD2D[1]DD2D1[43]DD2D[1]D[0][62]D1[68]DD2D[1]D[0]D[1]DD2D1[46][30]D11DD2D1D2D1DD2DD2D1[88]DD2D1DD2D1D2D[39]DD2D1DD2D1D2D[43][6]1[6][73][30]DD2D[1]DD2D1[33][40]D1[3]DD2D[1]DD2D1[43]DD2D[1]D[0]D[1][35]D1[40]DD2D1D2D[1][35]D[2][38]DD2DD2D1[51]DD2D[1]DD2D1D2D1[51]DD2D[1]D[0]D[1][35]D1DD2D1D2DD2D1[51]1D[0]1DD2D[1]D[0]D[1]DD2D1[33][40]D11DD2D1D2D1DD2DD2D1[88]DD2D1DD2D1D2DD2D1D2D3D[22]DD2DD2D1[51][26]DD2D[1]D[0][6]D1[12]1[73][40]DD2D[1]DD2D1[46][30]D1[3][141]
  216.  
Tags: proof logic condensed detachment pmgenerator metamath Łukasiewicz pmproofs.txt
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!