forked from xamidi/pmGenerator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
dProofs43-unfiltered39+_64cpu.log
146 lines (145 loc) · 21 KB
/
dProofs43-unfiltered39+_64cpu.log
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
( This log file was generated by 'pmGenerator 1.2' (master branch), compiled by 'Intel(R) oneAPI DPC++/C++ Compiler 2022.1.0 (2022.1.0.20220316)'.
The run was executed on a CLAIX-2018-OPTANE MPI node
— 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) —
running Linux, Rocky 8.8.
Wall-clock time: 29.3969444… h
CPU utilization: 1881.40444… core-h )
Wed Nov 1 01:58:44 2023: Process started. [pid: 70409, tid:23428951545728]
Tasks:
1. resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true)
2. generateDProofRepresentativeFiles(43, false, true)
[Main] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff]
(1) C0CC1C0.2CCN2CCN3.4.1C3.2 - CpCCqCprCCNrCCNstqCsr - 0\imply((1\imply(0\imply2))\imply((\not2\imply((\not3\imply4)\imply1))\imply(3\imply2)))
[Main] Calling generateDProofRepresentativeFiles(43, false, true).
Wed Nov 1 01:58:44 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 43, unfiltered]
0.03 ms taken to load initial representatives.
25.51 ms taken to read 1 condensed detachment proof and conclusion from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs3.txt. [tid:23428891297536]
9.22 ms taken to read 2 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs5.txt. [tid:23428889196288]
21.13 ms taken to read 5 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs7.txt. [tid:23428887095040]
11.36 ms taken to read 10 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs9.txt. [tid:23428884993792]
18.36 ms taken to read 24 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs11.txt. [tid:23428882892544]
22.46 ms taken to read 57 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs13.txt. [tid:23428880791296]
33.92 ms taken to read 137 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs15.txt. [tid:23428878690048]
26.86 ms taken to read 339 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs17.txt. [tid:23428876588800]
46.76 ms taken to read 854 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs19.txt. [tid:23428874487552]
67.66 ms taken to read 2171 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs21.txt. [tid:23428872386304]
148.14 ms taken to read 5583 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs23.txt. [tid:23428870285056]
278.36 ms taken to read 14478 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs25.txt. [tid:23428868183808]
2184.93 ms (2 s 184.93 ms) taken to read 37874 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs27.txt. [tid:23428866082560]
1250.58 ms (1 s 250.58 ms) taken to read 99756 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs29.txt. [tid:23428863981312]
2141.18 ms (2 s 141.18 ms) taken to read 264466 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs31.txt. [tid:23428861880064]
3152.65 ms (3 s 152.65 ms) taken to read 705026 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs33.txt. [tid:23428859778816]
6727.16 ms (6 s 727.16 ms) taken to read 1888450 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs35.txt. [tid:23428857677568]
12155.98 ms (12 s 155.98 ms) taken to read 5081180 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs37.txt. [tid:23428855576320]
12199.07 ms (12 s 199.07 ms) total read duration.
Loaded 19 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 5
9 : 10
11 : 24
13 : 57
15 : 137
17 : 339
19 : 854
21 : 2171
23 : 5583
25 : 14478
27 : 37874
29 : 99756
31 : 264466
33 : 705026
35 : 1888450
37 : 5081180
8100414 representatives in total.
49601.08 ms (49 s 601.08 ms) taken to read 13863883 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs39-unfiltered39+.txt. [tid:23428855576320]
102932.21 ms (1 min 42 s 932.21 ms) taken to read 37699564 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs41-unfiltered39+.txt. [tid:23428857677568]
102949.56 ms (1 min 42 s 949.56 ms) additional read duration.
Loaded 2 more representative collections of sizes:
39 : 13863883
41 : 37699564
59663861 representatives in total.
Wed Nov 1 02:00:53 2023: Inserted ≈ 5% of D-proof conclusions. [ 2983193 of 59663861] (ETC: Wed Nov 1 02:05:08 2023 ; 4 min 15 s 409.06 ms remaining ; 4 min 28 s 851.64 ms total)
Wed Nov 1 02:01:14 2023: Inserted ≈10% of D-proof conclusions. [ 5966386 of 59663861] (ETC: Wed Nov 1 02:06:24 2023 ; 5 min 9 s 885.54 ms remaining ; 5 min 44 s 317.26 ms total)
Wed Nov 1 02:01:34 2023: Inserted ≈15% of D-proof conclusions. [ 8949579 of 59663861] (ETC: Wed Nov 1 02:06:46 2023 ; 5 min 12 s 37.91 ms remaining ; 6 min 7 s 103.43 ms total)
Wed Nov 1 02:01:53 2023: Inserted ≈20% of D-proof conclusions. [11932772 of 59663861] (ETC: Wed Nov 1 02:06:47 2023 ; 4 min 54 s 275.22 ms remaining ; 6 min 7 s 844.03 ms total)
Wed Nov 1 02:02:15 2023: Inserted ≈25% of D-proof conclusions. [14915965 of 59663861] (ETC: Wed Nov 1 02:07:02 2023 ; 4 min 47 s 231.93 ms remaining ; 6 min 22 s 975.90 ms total)
Wed Nov 1 02:02:37 2023: Inserted ≈30% of D-proof conclusions. [17899158 of 59663861] (ETC: Wed Nov 1 02:07:11 2023 ; 4 min 34 s 409.22 ms remaining ; 6 min 32 s 13.17 ms total)
Wed Nov 1 02:02:58 2023: Inserted ≈35% of D-proof conclusions. [20882351 of 59663861] (ETC: Wed Nov 1 02:07:15 2023 ; 4 min 17 s 129.25 ms remaining ; 6 min 35 s 583.46 ms total)
Wed Nov 1 02:03:16 2023: Inserted ≈40% of D-proof conclusions. [23865544 of 59663861] (ETC: Wed Nov 1 02:07:11 2023 ; 3 min 54 s 821.22 ms remaining ; 6 min 31 s 368.69 ms total)
Wed Nov 1 02:03:34 2023: Inserted ≈45% of D-proof conclusions. [26848737 of 59663861] (ETC: Wed Nov 1 02:07:07 2023 ; 3 min 33 s 184.88 ms remaining ; 6 min 27 s 608.86 ms total)
Wed Nov 1 02:03:52 2023: Inserted ≈50% of D-proof conclusions. [29831930 of 59663861] (ETC: Wed Nov 1 02:07:05 2023 ; 3 min 13 s 124.56 ms remaining ; 6 min 26 s 249.10 ms total)
Wed Nov 1 02:04:10 2023: Inserted ≈55% of D-proof conclusions. [32815123 of 59663861] (ETC: Wed Nov 1 02:07:03 2023 ; 2 min 52 s 613.90 ms remaining ; 6 min 23 s 586.44 ms total)
Wed Nov 1 02:04:29 2023: Inserted ≈60% of D-proof conclusions. [35798316 of 59663861] (ETC: Wed Nov 1 02:07:02 2023 ; 2 min 33 s 189.71 ms remaining ; 6 min 22 s 974.27 ms total)
Wed Nov 1 02:04:49 2023: Inserted ≈65% of D-proof conclusions. [38781509 of 59663861] (ETC: Wed Nov 1 02:07:03 2023 ; 2 min 14 s 231.60 ms remaining ; 6 min 23 s 518.84 ms total)
Wed Nov 1 02:05:08 2023: Inserted ≈70% of D-proof conclusions. [41764702 of 59663861] (ETC: Wed Nov 1 02:07:04 2023 ; 1 min 55 s 368.74 ms remaining ; 6 min 24 s 562.45 ms total)
Wed Nov 1 02:05:29 2023: Inserted ≈75% of D-proof conclusions. [44747895 of 59663861] (ETC: Wed Nov 1 02:07:06 2023 ; 1 min 36 s 609.87 ms remaining ; 6 min 26 s 439.45 ms total)
Wed Nov 1 02:05:48 2023: Inserted ≈80% of D-proof conclusions. [47731088 of 59663861] (ETC: Wed Nov 1 02:07:05 2023 ; 1 min 17 s 114.35 ms remaining ; 6 min 25 s 571.75 ms total)
Wed Nov 1 02:06:07 2023: Inserted ≈85% of D-proof conclusions. [50714281 of 59663861] (ETC: Wed Nov 1 02:07:05 2023 ; 57 s 838.21 ms remaining ; 6 min 25 s 588.05 ms total)
Wed Nov 1 02:06:27 2023: Inserted ≈90% of D-proof conclusions. [53697474 of 59663861] (ETC: Wed Nov 1 02:07:05 2023 ; 38 s 595.16 ms remaining ; 6 min 25 s 951.57 ms total)
Wed Nov 1 02:06:46 2023: Inserted ≈95% of D-proof conclusions. [56680667 of 59663861] (ETC: Wed Nov 1 02:07:05 2023 ; 19 s 304.11 ms remaining ; 6 min 26 s 82.11 ms total)
Wed Nov 1 02:07:08 2023: Inserted 100% of D-proof conclusions. [59663861 of 59663861] (ETC: Wed Nov 1 02:07:08 2023 ; 0.00 ms remaining ; 6 min 29 s 251.13 ms total)
389251.33 ms (6 min 29 s 251.33 ms) total insertion duration.
Known iteration count loaded from 43:214945751.
Wed Nov 1 02:07:08 2023: Starting to generate D-proof representatives of length 43.
Wed Nov 1 02:30:33 2023: Iterated ≈ 2% of D-proof candidates. [ 4298915 of 214945751] (ETC: Wed Nov 1 21:37:40 2023 ; 19 h 7 min 7 s 308.88 ms remaining ; 19 h 30 min 31 s 947.83 ms total)
Wed Nov 1 03:00:55 2023: Iterated ≈ 4% of D-proof candidates. [ 8597830 of 214945751] (ETC: Thu Nov 2 00:31:33 2023 ; 21 h 30 min 37 s 645.91 ms remaining ; 22 h 24 min 24 s 214.47 ms total)
Wed Nov 1 03:40:23 2023: Iterated ≈ 6% of D-proof candidates. [ 12896745 of 214945751] (ETC: Thu Nov 2 04:01:17 2023 ; 1 d 20 min 53 s 167.76 ms remaining ; 1 d 1 h 54 min 8 s 50.78 ms total)
Wed Nov 1 04:19:15 2023: Iterated ≈ 8% of D-proof candidates. [ 17195660 of 214945751] (ETC: Thu Nov 2 05:38:30 2023 ; 1 d 1 h 19 min 14 s 938.34 ms remaining ; 1 d 3 h 31 min 21 s 454.67 ms total)
Wed Nov 1 04:55:26 2023: Iterated ≈10% of D-proof candidates. [ 21494575 of 214945751] (ETC: Thu Nov 2 06:10:06 2023 ; 1 d 1 h 14 min 39 s 793.72 ms remaining ; 1 d 4 h 2 min 57 s 548.53 ms total)
Wed Nov 1 05:32:12 2023: Iterated ≈12% of D-proof candidates. [ 25793490 of 214945751] (ETC: Thu Nov 2 06:35:56 2023 ; 1 d 1 h 3 min 44 s 189.03 ms remaining ; 1 d 4 h 28 min 47 s 487.47 ms total)
Wed Nov 1 06:14:10 2023: Iterated ≈14% of D-proof candidates. [ 30092405 of 214945751] (ETC: Thu Nov 2 07:31:35 2023 ; 1 d 1 h 17 min 25 s 470.23 ms remaining ; 1 d 5 h 24 min 26 s 825.77 ms total)
Wed Nov 1 07:06:09 2023: Iterated ≈16% of D-proof candidates. [ 34391320 of 214945751] (ETC: Thu Nov 2 09:15:57 2023 ; 1 d 2 h 9 min 48 s 6.56 ms remaining ; 1 d 7 h 8 min 48 s 579.14 ms total)
Wed Nov 1 07:47:50 2023: Iterated ≈18% of D-proof candidates. [ 38690235 of 214945751] (ETC: Thu Nov 2 09:39:51 2023 ; 1 d 1 h 52 min 958.89 ms remaining ; 1 d 7 h 32 min 42 s 144.87 ms total)
Wed Nov 1 08:46:51 2023: Iterated ≈20% of D-proof candidates. [ 42989150 of 214945751] (ETC: Thu Nov 2 11:25:41 2023 ; 1 d 2 h 38 min 50 s 370.95 ms remaining ; 1 d 9 h 18 min 32 s 963.55 ms total)
Wed Nov 1 09:45:27 2023: Iterated ≈22% of D-proof candidates. [ 47288065 of 214945751] (ETC: Thu Nov 2 12:50:20 2023 ; 1 d 3 h 4 min 53 s 241.46 ms remaining ; 1 d 10 h 43 min 11 s 335.04 ms total)
Wed Nov 1 10:50:23 2023: Iterated ≈24% of D-proof candidates. [ 51586980 of 214945751] (ETC: Thu Nov 2 14:27:19 2023 ; 1 d 3 h 36 min 55 s 982.24 ms remaining ; 1 d 12 h 20 min 10 s 502.75 ms total)
Wed Nov 1 11:35:48 2023: Iterated ≈26% of D-proof candidates. [ 55885895 of 214945751] (ETC: Thu Nov 2 14:34:15 2023 ; 1 d 2 h 58 min 27 s 856.53 ms remaining ; 1 d 12 h 27 min 6 s 832.94 ms total)
Wed Nov 1 12:16:54 2023: Iterated ≈28% of D-proof candidates. [ 60184810 of 214945751] (ETC: Thu Nov 2 14:24:49 2023 ; 1 d 2 h 7 min 55 s 689.71 ms remaining ; 1 d 12 h 17 min 40 s 679.91 ms total)
Wed Nov 1 13:00:36 2023: Iterated ≈30% of D-proof candidates. [ 64483725 of 214945751] (ETC: Thu Nov 2 14:25:20 2023 ; 1 d 1 h 24 min 44 s 77.48 ms remaining ; 1 d 12 h 18 min 11 s 539.00 ms total)
Wed Nov 1 13:53:52 2023: Iterated ≈32% of D-proof candidates. [ 68782640 of 214945751] (ETC: Thu Nov 2 14:55:39 2023 ; 1 d 1 h 1 min 46 s 875.71 ms remaining ; 1 d 12 h 48 min 30 s 111.05 ms total)
Wed Nov 1 14:46:45 2023: Iterated ≈34% of D-proof candidates. [ 73081555 of 214945751] (ETC: Thu Nov 2 15:21:16 2023 ; 1 d 34 min 31 s 563.65 ms remaining ; 1 d 13 h 14 min 7 s 823.38 ms total)
Wed Nov 1 15:37:00 2023: Iterated ≈36% of D-proof candidates. [ 77380470 of 214945751] (ETC: Thu Nov 2 15:36:44 2023 ; 23 h 59 min 44 s 360.51 ms remaining ; 1 d 13 h 29 min 35 s 562.95 ms total)
Wed Nov 1 16:33:00 2023: Iterated ≈38% of D-proof candidates. [ 81679385 of 214945751] (ETC: Thu Nov 2 16:05:42 2023 ; 23 h 32 min 42 s 223.15 ms remaining ; 1 d 13 h 58 min 33 s 262.76 ms total)
Wed Nov 1 17:21:16 2023: Iterated ≈40% of D-proof candidates. [ 85978300 of 214945751] (ETC: Thu Nov 2 16:12:26 2023 ; 22 h 51 min 10 s 516.51 ms remaining ; 1 d 14 h 5 min 17 s 527.10 ms total)
Wed Nov 1 18:05:22 2023: Iterated ≈42% of D-proof candidates. [ 90277215 of 214945751] (ETC: Thu Nov 2 16:08:38 2023 ; 22 h 3 min 16 s 93.45 ms remaining ; 1 d 14 h 1 min 29 s 815.84 ms total)
Wed Nov 1 18:44:45 2023: Iterated ≈44% of D-proof candidates. [ 94576130 of 214945751] (ETC: Thu Nov 2 15:54:25 2023 ; 21 h 9 min 40 s 435.82 ms remaining ; 1 d 13 h 47 min 16 s 492.04 ms total)
Wed Nov 1 19:23:00 2023: Iterated ≈46% of D-proof candidates. [ 98875045 of 214945751] (ETC: Thu Nov 2 15:39:01 2023 ; 20 h 16 min 750.32 ms remaining ; 1 d 13 h 31 min 52 s 500.06 ms total)
Wed Nov 1 20:00:53 2023: Iterated ≈48% of D-proof candidates. [103173960 of 214945751] (ETC: Thu Nov 2 15:24:07 2023 ; 19 h 23 min 13 s 642.73 ms remaining ; 1 d 13 h 16 min 58 s 543.14 ms total)
Wed Nov 1 20:37:37 2023: Iterated ≈50% of D-proof candidates. [107472875 of 214945751] (ETC: Thu Nov 2 15:08:05 2023 ; 18 h 30 min 28 s 86.52 ms remaining ; 1 d 13 h 56 s 172.42 ms total)
Wed Nov 1 21:13:48 2023: Iterated ≈52% of D-proof candidates. [111771790 of 214945751] (ETC: Thu Nov 2 14:52:16 2023 ; 17 h 38 min 27 s 442.38 ms remaining ; 1 d 12 h 45 min 7 s 170.96 ms total)
Wed Nov 1 21:50:08 2023: Iterated ≈54% of D-proof candidates. [116070705 of 214945751] (ETC: Thu Nov 2 14:37:52 2023 ; 16 h 47 min 43 s 861.43 ms remaining ; 1 d 12 h 30 min 43 s 176.30 ms total)
Wed Nov 1 22:24:58 2023: Iterated ≈56% of D-proof candidates. [120369620 of 214945751] (ETC: Thu Nov 2 14:21:50 2023 ; 15 h 56 min 51 s 911.37 ms remaining ; 1 d 12 h 14 min 41 s 615.98 ms total)
Wed Nov 1 22:57:12 2023: Iterated ≈58% of D-proof candidates. [124668535 of 214945751] (ETC: Thu Nov 2 14:02:25 2023 ; 15 h 5 min 12 s 937.51 ms remaining ; 1 d 11 h 55 min 16 s 517.04 ms total)
Wed Nov 1 23:28:14 2023: Iterated ≈60% of D-proof candidates. [128967450 of 214945751] (ETC: Thu Nov 2 13:42:18 2023 ; 14 h 14 min 3 s 842.95 ms remaining ; 1 d 11 h 35 min 9 s 606.47 ms total)
Wed Nov 1 23:59:02 2023: Iterated ≈62% of D-proof candidates. [133266365 of 214945751] (ETC: Thu Nov 2 13:23:05 2023 ; 13 h 24 min 3 s 580.07 ms remaining ; 1 d 11 h 15 min 56 s 788.69 ms total)
Thu Nov 2 00:30:57 2023: Iterated ≈64% of D-proof candidates. [137565280 of 214945751] (ETC: Thu Nov 2 13:06:51 2023 ; 12 h 35 min 53 s 777.28 ms remaining ; 1 d 10 h 59 min 42 s 713.62 ms total)
Thu Nov 2 01:02:12 2023: Iterated ≈66% of D-proof candidates. [141864195 of 214945751] (ETC: Thu Nov 2 12:50:33 2023 ; 11 h 48 min 21 s 592.57 ms remaining ; 1 d 10 h 43 min 24 s 682.90 ms total)
Thu Nov 2 01:31:24 2023: Iterated ≈68% of D-proof candidates. [146163110 of 214945751] (ETC: Thu Nov 2 12:32:13 2023 ; 11 h 49 s 454.38 ms remaining ; 1 d 10 h 25 min 4 s 543.70 ms total)
Thu Nov 2 01:58:19 2023: Iterated ≈70% of D-proof candidates. [150462025 of 214945751] (ETC: Thu Nov 2 12:11:41 2023 ; 10 h 13 min 21 s 689.95 ms remaining ; 1 d 10 h 4 min 32 s 298.50 ms total)
Thu Nov 2 02:22:48 2023: Iterated ≈72% of D-proof candidates. [154760940 of 214945751] (ETC: Thu Nov 2 11:48:53 2023 ; 9 h 26 min 5 s 308.60 ms remaining ; 1 d 9 h 41 min 44 s 672.11 ms total)
Thu Nov 2 02:45:55 2023: Iterated ≈74% of D-proof candidates. [159059855 of 214945751] (ETC: Thu Nov 2 11:25:30 2023 ; 8 h 39 min 34 s 304.47 ms remaining ; 1 d 9 h 18 min 21 s 169.46 ms total)
Thu Nov 2 03:08:34 2023: Iterated ≈76% of D-proof candidates. [163358770 of 214945751] (ETC: Thu Nov 2 11:02:41 2023 ; 7 h 54 min 7 s 908.48 ms remaining ; 1 d 8 h 55 min 32 s 950.26 ms total)
Thu Nov 2 03:29:50 2023: Iterated ≈78% of D-proof candidates. [167657685 of 214945751] (ETC: Thu Nov 2 10:39:19 2023 ; 7 h 9 min 28 s 684.21 ms remaining ; 1 d 8 h 32 min 10 s 380.82 ms total)
Thu Nov 2 03:50:30 2023: Iterated ≈80% of D-proof candidates. [171956600 of 214945751] (ETC: Thu Nov 2 10:16:20 2023 ; 6 h 25 min 50 s 307.94 ms remaining ; 1 d 8 h 9 min 11 s 537.52 ms total)
Thu Nov 2 04:10:27 2023: Iterated ≈82% of D-proof candidates. [176255515 of 214945751] (ETC: Thu Nov 2 09:53:36 2023 ; 5 h 43 min 9 s 797.43 ms remaining ; 1 d 7 h 46 min 27 s 761.09 ms total)
Thu Nov 2 04:29:04 2023: Iterated ≈84% of D-proof candidates. [180554430 of 214945751] (ETC: Thu Nov 2 09:30:24 2023 ; 5 h 1 min 19 s 235.81 ms remaining ; 1 d 7 h 23 min 15 s 221.05 ms total)
Thu Nov 2 04:46:43 2023: Iterated ≈86% of D-proof candidates. [184853345 of 214945751] (ETC: Thu Nov 2 09:07:06 2023 ; 4 h 20 min 23 s 699.54 ms remaining ; 1 d 6 h 59 min 57 s 850.66 ms total)
Thu Nov 2 05:03:28 2023: Iterated ≈88% of D-proof candidates. [189152260 of 214945751] (ETC: Thu Nov 2 08:43:53 2023 ; 3 h 40 min 24 s 485.64 ms remaining ; 1 d 6 h 36 min 44 s 43.22 ms total)
Thu Nov 2 05:19:28 2023: Iterated ≈90% of D-proof candidates. [193451175 of 214945751] (ETC: Thu Nov 2 08:20:51 2023 ; 3 h 1 min 22 s 206.86 ms remaining ; 1 d 6 h 13 min 42 s 64.06 ms total)
Thu Nov 2 05:34:43 2023: Iterated ≈92% of D-proof candidates. [197750090 of 214945751] (ETC: Thu Nov 2 07:57:59 2023 ; 2 h 23 min 16 s 24.51 ms remaining ; 1 d 5 h 50 min 50 s 300.62 ms total)
Thu Nov 2 05:49:41 2023: Iterated ≈94% of D-proof candidates. [202049005 of 214945751] (ETC: Thu Nov 2 07:35:48 2023 ; 1 h 46 min 7 s 189.47 ms remaining ; 1 d 5 h 28 min 39 s 816.86 ms total)
Thu Nov 2 06:04:19 2023: Iterated ≈96% of D-proof candidates. [206347920 of 214945751] (ETC: Thu Nov 2 07:14:12 2023 ; 1 h 9 min 52 s 942.34 ms remaining ; 1 d 5 h 7 min 3 s 546.82 ms total)
Thu Nov 2 06:18:34 2023: Iterated ≈98% of D-proof candidates. [210646835 of 214945751] (ETC: Thu Nov 2 06:53:05 2023 ; 34 min 31 s 134.69 ms remaining ; 1 d 4 h 45 min 56 s 710.70 ms total)
Thu Nov 2 06:32:27 2023: Iterated 100% of D-proof candidates. [214945751 of 214945751] (ETC: Thu Nov 2 06:32:27 2023 ; 0.00 ms remaining ; 1 d 4 h 25 min 18 s 271.80 ms total)
102319358.87 ms (1 d 4 h 25 min 19 s 358.87 ms) taken to collect 102797921 D-proofs of length 43. [iterated 214945751 condensed detachment proof strings]
[Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 5 }, { 9, 14 }, { 11, 34 }, { 13, 88 }, { 15, 227 }, { 17, 584 }, { 19, 1520 }, { 21, 3984 }, { 23, 10492 }, { 25, 27790 }, { 27, 73951 }, { 29, 197716 }, { 31, 530829 }, { 33, 1430830 }, { 35, 3870703 }, { 37, 10505128 }, { 39, 28598584 }, { 41, 78349744 }, { 43, 214945751 } }
1324435.80 ms (22 min 4 s 435.80 ms) taken to filter and order new representative proofs.
Found 102797921 representative, 1888638 redundant, and 110259192 invalid condensed detachment proof strings.
lengths up to 43 ; amounts per length: {(1,1), (3,1), (5,2), (7,5), (9,10), (11,24), (13,57), (15,137), (17,339), (19,854), (21,2171), (23,5583), (25,14478), (27,37874), (29,99756), (31,264466), (33,705026), (35,1888450), (37,5081180), (39,13863883), (41,37699564), (43,102797921)} ; 102797921 new representative proofs (1888638 redundant, 110259192 invalid)
Thu Nov 2 07:00:56 2023: Starting to write 102797921 entries to data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs43-unfiltered39+.txt.
732753.60 ms (12 min 12 s 753.60 ms) taken to print and save 257774107632 bytes of representative condensed detachment proof strings to data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs43-unfiltered39+.txt.
Thu Nov 2 07:15:47 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 43, unfiltered]
Thu Nov 2 07:22:33 2023: Process terminated. [pid: 70409, tid:23428951545728]