c ------------------- Paras list -------------------
c Name                	 Type      	 Now       	 Default   	 Comment
c DPS                 	 int       	 0         	 0         	 DPS/NPS
c DPS_period          	 int       	 10000     	 10000     	 DPS sharing period
c margin              	 int       	 0         	 0         	 DPS margin
c pakis               	 int       	 1         	 1         	 Use pakis diversity
c reset               	 int       	 0         	 0         	 Dynamically reseting
c reset_time          	 int       	 10        	 10        	 Reseting base interval (seconds)
c share               	 int       	 1         	 1         	 Sharing learnt clauses
c share_intv          	 int       	 500000    	 500000    	 Sharing interval (microseconds)
c share_lits          	 int       	 1500      	 1500      	 Sharing lits (per every #share_intv seconds)
c shuffle             	 int       	 1         	 1         	 Use random shuffle
c simplify            	 int       	 1         	 1         	 Use Simplify (only preprocess)
c threads             	 int       	 32        	 32        	 Thread number
c times               	 double    	 3600.000000	 5000      	 Cutoff time
c config              	 string		           	 ""        	 Config file
c instance            	 string		 /pub/data/chenzh/data/sat2022/436d00b6d41912e800e9855d08c75139-manol-pipe-f7nidw.cnf	 ""        	 CNF format instance
c --------------------------------------------------
c [leader] preprocess(simplify) input data
c After preprocess: vars: 310434 -> 310433 , clauses: 923497 -> 923494 ,
c After preprocess: vars: 310433 -> 310323 , clauses: 923494 -> 923274 ,
c sz 2
c turns: 1
c After preprocess: vars: 310323 -> 310323 , clauses: 923274 -> 923274 ,
c [leader] hand out length of cnf instance to all nodes
c [leader] hand out cnf instance to all nodes
c [leader] hand out done!
c [worker] round 1, time: 0.0
c [worker] round 1, time: 0.0
c [worker] round 2, time: 0.503
c [worker] round 2, time: 0.503
c [worker] round 1, time: 0.0
c [worker] round 1, time: 0.0
c [worker] round 1, time: 0.0
c [worker] round 1, time: 0.0
c [worker] round 3, time: 1.7
c [worker] round 3, time: 1.7
c [worker] round 2, time: 0.501
c [worker] round 1, time: 0.0
c [worker] round 2, time: 0.503
c [worker] round 2, time: 0.505
c [worker] round 1, time: 0.0
c [worker] round 2, time: 0.505
c [worker] round 4, time: 1.511
c [worker] round 4, time: 1.512
c [worker] round 3, time: 1.2
c [worker] round 2, time: 0.502
c [worker] round 3, time: 1.8
c [worker] round 3, time: 1.12
c [worker] round 2, time: 0.503
c [worker] round 3, time: 1.6
c [worker] round 5, time: 2.15
c [worker] round 5, time: 2.15
c [worker] round 4, time: 1.506
c [worker] round 3, time: 1.7
c [worker] round 4, time: 1.515
c [worker] round 4, time: 1.516
c [worker] round 3, time: 1.7
c [worker] round 4, time: 1.513
c [worker] round 6, time: 2.521
c [worker] round 6, time: 2.529
c [worker] round 5, time: 2.11
c [worker] round 4, time: 1.515
c [worker] round 5, time: 2.18
c [worker] round 5, time: 2.22
c [worker] round 4, time: 1.511
c [worker] round 5, time: 2.17
c [worker] round 7, time: 3.27
c [worker] round 7, time: 3.33
c [worker] round 6, time: 2.517
c [worker] round 5, time: 2.18
c [worker] round 6, time: 2.520
c [worker] round 6, time: 2.526
c [worker] round 5, time: 2.16
c [worker] round 6, time: 2.525
c [worker] round 8, time: 3.535
c [worker] round 8, time: 3.543
c [worker] round 7, time: 3.23
c [worker] round 6, time: 2.521
c [worker] round 7, time: 3.22
c [worker] round 7, time: 3.36
c [worker] round 6, time: 2.519
c [worker] round 7, time: 3.29
c [worker] round 9, time: 4.39
c [worker] round 9, time: 4.48
c [worker] round 8, time: 3.527
c [worker] round 7, time: 3.27
c [worker] round 8, time: 3.523
c [worker] round 7, time: 3.23
c [worker] round 8, time: 3.544
c [worker] round 8, time: 3.532
c [worker] round 10, time: 4.543
c [worker] round 9, time: 4.30
c [worker] round 10, time: 4.555
c [worker] round 8, time: 3.529
c [worker] round 9, time: 4.27
c [worker] round 8, time: 3.527
c [worker] round 9, time: 4.48
c [worker] round 9, time: 4.36
c [worker] round 11, time: 5.47
c [worker] round 10, time: 4.533
c [worker] round 11, time: 5.63
c [worker] round 9, time: 4.35
c [worker] round 10, time: 4.531
c [worker] round 9, time: 4.31
c [worker] round 10, time: 4.556
c [worker] round 10, time: 4.538
c [worker] round 12, time: 5.551
c [worker] round 11, time: 5.35
c [worker] round 12, time: 5.567
c [worker] round 10, time: 4.539
c [worker] round 11, time: 5.35
c [worker] round 10, time: 4.535
c [worker] round 11, time: 5.60
c [worker] round 11, time: 5.45
c [worker] round 13, time: 6.54
c [worker] round 12, time: 5.539
c [worker] round 13, time: 6.71
c [worker] round 11, time: 5.43
c [worker] round 12, time: 5.537
c [worker] round 11, time: 5.39
c [worker] round 12, time: 5.564
c [worker] round 12, time: 5.548
c [worker] round 14, time: 6.558
c [worker] round 13, time: 6.43
c [worker] round 14, time: 6.583
c [worker] round 12, time: 5.546
c [worker] round 13, time: 6.39
c [worker] round 12, time: 5.543
c [worker] round 13, time: 6.72
c [worker] round 13, time: 6.51
c [worker] round 15, time: 7.61
c [worker] round 14, time: 6.546
c [worker] round 15, time: 7.87
c [worker] round 13, time: 6.51
c [worker] round 14, time: 6.540
c [worker] round 13, time: 6.47
c [worker] round 14, time: 6.576
c [worker] round 14, time: 6.555
c [worker] round 16, time: 7.565
c [worker] round 15, time: 7.51
c [worker] round 16, time: 7.591
c [worker] round 14, time: 6.555
c [worker] round 15, time: 7.42
c [worker] round 14, time: 6.549
c [worker] round 15, time: 7.80
c [worker] round 15, time: 7.61
c [worker] round 17, time: 8.69
c [worker] round 16, time: 7.554
c [worker] round 17, time: 8.95
c [worker] round 15, time: 7.59
c [worker] round 16, time: 7.547
c [worker] round 15, time: 7.51
c [worker] round 16, time: 7.588
c [worker] round 16, time: 7.563
c [worker] round 18, time: 8.575
c [worker] round 17, time: 8.59
c [worker] round 18, time: 8.598
c [worker] round 16, time: 7.561
c [worker] round 17, time: 8.49
c [worker] round 16, time: 7.555
c [worker] round 17, time: 8.92
c [worker] round 17, time: 8.66
c [worker] round 19, time: 9.79
c [worker] round 18, time: 8.562
c [worker] round 19, time: 9.103
c [worker] round 17, time: 8.63
c [worker] round 18, time: 8.550
c [worker] round 17, time: 8.56
c [worker] round 18, time: 8.595
c [worker] round 18, time: 8.568
c [worker] round 20, time: 9.583
c [worker] round 19, time: 9.63
c [worker] round 20, time: 9.606
c [worker] round 18, time: 8.564
c [worker] round 19, time: 9.51
c [worker] round 18, time: 8.559
c [worker] round 19, time: 9.100
c [worker] round 19, time: 9.71
c [worker] round 21, time: 10.85
c [worker] round 20, time: 9.567
c [worker] round 21, time: 10.111
c [worker] round 19, time: 9.65
c [worker] round 20, time: 9.555
c [worker] round 19, time: 9.60
c [worker] round 20, time: 9.602
c [worker] round 20, time: 9.572
c [worker] round 22, time: 10.587
c [worker] round 21, time: 10.71
c [worker] round 22, time: 10.613
c [worker] round 20, time: 9.567
c [worker] round 21, time: 10.59
c [worker] round 20, time: 9.563
c [worker] round 21, time: 10.103
c [worker] round 21, time: 10.77
c [worker] round 23, time: 11.89
c [worker] round 22, time: 10.573
c [worker] round 23, time: 11.115
c [worker] round 21, time: 10.68
c [worker] round 22, time: 10.563
c [worker] round 21, time: 10.67
c [worker] round 22, time: 10.608
c [worker] round 22, time: 10.581
c [worker] round 24, time: 11.591
c [worker] round 23, time: 11.74
c [worker] round 24, time: 11.619
c [worker] round 22, time: 10.569
c [worker] round 23, time: 11.64
c [worker] round 22, time: 10.568
c [worker] round 23, time: 11.109
c [worker] round 23, time: 11.82
c [worker] round 25, time: 12.95
c [worker] round 24, time: 11.575
c [worker] round 25, time: 12.123
c [worker] round 23, time: 11.69
c [worker] round 24, time: 11.567
c [worker] round 23, time: 11.71
c [worker] round 24, time: 11.610
c [worker] round 24, time: 11.585
c [worker] round 26, time: 12.599
c [worker] round 25, time: 12.76
c [worker] round 26, time: 12.625
c [worker] round 24, time: 11.570
c [worker] round 25, time: 12.68
c [worker] round 24, time: 11.575
c [worker] round 25, time: 12.111
c [worker] round 25, time: 12.89
c [worker] round 27, time: 13.103
c [worker] round 26, time: 12.579
c [worker] round 27, time: 13.126
c [worker] round 25, time: 12.71
c [worker] round 26, time: 12.571
c [worker] round 25, time: 12.79
c [worker] round 26, time: 12.616
c [worker] round 26, time: 12.589
c [worker] round 28, time: 13.604
c [worker] round 27, time: 13.83
c [worker] round 28, time: 13.627
c [worker] round 26, time: 12.572
c [worker] round 27, time: 13.75
c [worker] round 26, time: 12.583
c [worker] round 27, time: 13.120
c [worker] round 27, time: 13.93
c [worker] round 29, time: 14.105
c [worker] round 28, time: 13.584
c [worker] round 29, time: 14.128
c [worker] round 27, time: 13.75
c [worker] round 28, time: 13.579
c [worker] round 27, time: 13.84
c [worker] round 28, time: 13.621
c [worker] round 28, time: 13.594
c [worker] round 30, time: 14.607
c [worker] round 29, time: 14.85
c [worker] round 30, time: 14.631
c [worker] round 28, time: 13.576
c [worker] round 29, time: 14.80
c [worker] round 28, time: 13.587
c [worker] round 29, time: 14.122
c [worker] round 29, time: 14.97
c [worker] round 31, time: 15.111
c [worker] round 30, time: 14.587
c [worker] round 31, time: 15.135
c [worker] round 29, time: 14.77
c [worker] round 30, time: 14.583
c [worker] round 29, time: 14.88
c [worker] round 30, time: 14.624
c [worker] round 30, time: 14.601
c [worker] round 32, time: 15.615
c [worker] round 31, time: 15.111
c [worker] round 32, time: 15.639
c [worker] round 30, time: 14.578
c [worker] round 31, time: 15.87
c [worker] round 30, time: 14.591
c [worker] round 31, time: 15.125
c [worker] round 31, time: 15.102
c [worker] round 33, time: 16.119
c [worker] round 32, time: 15.612
c [worker] round 33, time: 16.143
c [worker] round 31, time: 15.79
c [worker] round 32, time: 15.591
c [worker] round 31, time: 15.92
c [worker] round 32, time: 15.627
c [worker] round 32, time: 15.603
c [worker] round 34, time: 16.623
c [worker] round 33, time: 16.114
c [worker] round 34, time: 16.645
c [worker] round 32, time: 15.583
c [worker] round 33, time: 16.93
c [worker] round 32, time: 15.595
c [worker] round 33, time: 16.129
c [worker] round 33, time: 16.105
c [worker] round 35, time: 17.125
c [worker] round 34, time: 16.615
c [worker] round 35, time: 17.147
c [worker] round 33, time: 16.85
c [worker] round 34, time: 16.594
c [worker] round 33, time: 16.96
c [worker] round 34, time: 16.633
c [worker] round 34, time: 16.609
c [worker] round 36, time: 17.628
c [worker] round 35, time: 17.117
c [worker] round 36, time: 17.651
c [worker] round 34, time: 16.586
c [worker] round 35, time: 17.95
c [worker] round 34, time: 16.599
c [worker] round 35, time: 17.136
c [worker] round 35, time: 17.113
c [worker] round 37, time: 18.130
c [worker] round 36, time: 17.623
c [worker] round 37, time: 18.154
c [worker] round 35, time: 17.88
c [worker] round 36, time: 17.597
c [worker] round 35, time: 17.101
c [worker] round 36, time: 17.639
c [worker] round 36, time: 17.617
c [worker] round 38, time: 18.633
c [worker] round 37, time: 18.126
c [worker] round 38, time: 18.664
c [worker] round 36, time: 17.591
c [worker] round 37, time: 18.99
c [worker] round 36, time: 17.603
c [worker] round 37, time: 18.143
c [worker] round 37, time: 18.119
c [worker] round 39, time: 19.139
c [worker] round 38, time: 18.631
c [worker] round 39, time: 19.171
c [worker] round 37, time: 18.95
c [worker] round 38, time: 18.603
c [worker] round 37, time: 18.105
c [worker] round 38, time: 18.646
c [worker] round 38, time: 18.622
c [worker] round 40, time: 19.643
c [worker] round 39, time: 19.134
c [worker] round 40, time: 19.679
c [worker] round 38, time: 18.598
c [worker] round 39, time: 19.106
c [worker] round 38, time: 18.606
c [worker] round 39, time: 19.151
c [worker] round 39, time: 19.126
c [worker] round 41, time: 20.151
c [worker] round 40, time: 19.638
c [worker] round 41, time: 20.187
c [worker] round 39, time: 19.101
c [worker] round 40, time: 19.608
c [worker] round 39, time: 19.107
c [worker] round 40, time: 19.656
c [worker] round 40, time: 19.633
c [worker] round 42, time: 20.656
c [worker] round 41, time: 20.143
c [worker] round 42, time: 20.695
c [worker] round 40, time: 19.607
c [worker] round 41, time: 20.109
c [worker] round 40, time: 19.611
c [worker] round 41, time: 20.161
c [worker] round 41, time: 20.137
c [worker] round 43, time: 21.161
c [worker] round 42, time: 20.647
c [worker] round 43, time: 21.200
c [worker] round 41, time: 20.110
c [worker] round 42, time: 20.611
c [worker] round 41, time: 20.115
c [worker] round 42, time: 20.666
c [worker] round 42, time: 20.640
c [worker] round 44, time: 21.665
c [worker] round 43, time: 21.151
c [worker] round 44, time: 21.707
c [worker] round 42, time: 20.612
c [worker] round 43, time: 21.113
c [worker] round 42, time: 20.617
c [worker] round 43, time: 21.170
c [worker] round 43, time: 21.145
c [worker] round 45, time: 22.169
c [worker] round 44, time: 21.655
c [worker] round 45, time: 22.212
c [worker] round 43, time: 21.114
c [worker] round 44, time: 21.614
c [worker] round 43, time: 21.118
c [worker] round 44, time: 21.675
c [worker] round 44, time: 21.648
c [worker] round 46, time: 22.675
c [worker] round 45, time: 22.157
c [worker] round 46, time: 22.716
c [worker] round 44, time: 21.617
c [worker] round 45, time: 22.119
c [worker] round 44, time: 21.619
c [worker] round 45, time: 22.184
c [worker] round 45, time: 22.153
c [worker] round 47, time: 23.179
c [worker] round 46, time: 22.660
c [worker] round 47, time: 23.220
c [worker] round 45, time: 22.123
c [worker] round 46, time: 22.621
c [worker] round 45, time: 22.123
c [worker] round 46, time: 22.692
c [worker] round 46, time: 22.657
c [worker] round 48, time: 23.683
c [worker] round 47, time: 23.163
c [worker] round 48, time: 23.725
c [worker] round 46, time: 22.626
c [worker] round 47, time: 23.123
c [worker] round 46, time: 22.627
c [worker] round 47, time: 23.196
c [worker] round 47, time: 23.160
c [worker] round 49, time: 24.186
c [worker] round 48, time: 23.666
c [worker] round 49, time: 24.231
c [worker] round 47, time: 23.131
c [worker] round 48, time: 23.627
c [worker] round 47, time: 23.129
c [worker] round 48, time: 23.704
c [worker] round 48, time: 23.663
c [worker] round 50, time: 24.690
c [worker] round 49, time: 24.169
c [worker] round 50, time: 24.735
c [worker] round 48, time: 23.635
c [worker] round 49, time: 24.129
c [worker] round 48, time: 23.630
c [worker] round 49, time: 24.208
c [worker] round 49, time: 24.169
c [worker] round 51, time: 25.195
c [worker] round 50, time: 24.672
c [worker] round 51, time: 25.247
c [worker] round 49, time: 24.137
c [worker] round 50, time: 24.631
c [worker] round 49, time: 24.131
c [worker] round 50, time: 24.716
c [worker] round 50, time: 24.672
c [worker] round 52, time: 25.699
c [worker] round 51, time: 25.174
c [worker] round 52, time: 25.751
c [worker] round 50, time: 24.639
c [worker] round 51, time: 25.132
c [worker] round 50, time: 24.635
c [worker] round 51, time: 25.220
c [worker] round 51, time: 25.175
c [worker] round 53, time: 26.203
c [worker] round 52, time: 25.677
c [worker] round 53, time: 26.255
c [worker] round 51, time: 25.141
c [worker] round 52, time: 25.634
c [worker] round 51, time: 25.139
c [worker] round 52, time: 25.723
c [worker] round 52, time: 25.681
c [worker] round 54, time: 26.707
c [worker] round 53, time: 26.179
c [worker] round 54, time: 26.759
c [worker] round 52, time: 25.647
c [worker] round 53, time: 26.135
c [worker] round 52, time: 25.641
c [worker] round 53, time: 26.227
c [worker] round 53, time: 26.185
c [worker] round 55, time: 27.211
c [worker] round 54, time: 26.682
c [worker] round 55, time: 27.263
c [worker] round 53, time: 26.151
c [worker] round 54, time: 26.637
c [worker] round 53, time: 26.142
c [worker] round 54, time: 26.732
c [worker] round 54, time: 26.687
c [worker] round 56, time: 27.714
c [worker] round 55, time: 27.187
c [worker] round 56, time: 27.767
c [worker] round 54, time: 26.653
c [worker] round 55, time: 27.138
c [worker] round 54, time: 26.643
c [worker] round 55, time: 27.190
c [worker] round 55, time: 27.272
c [worker] round 57, time: 28.219
c [worker] round 56, time: 27.690
c [worker] round 57, time: 28.270
c [worker] round 55, time: 27.155
c [worker] round 56, time: 27.639
c [worker] round 55, time: 27.147
c [worker] round 56, time: 27.780
c [worker] round 56, time: 27.733
c [worker] round 58, time: 28.723
c [worker] round 57, time: 28.195
c [worker] round 58, time: 28.773
c [worker] round 56, time: 27.659
c [worker] round 57, time: 28.143
c [worker] round 56, time: 27.649
c [worker] round 57, time: 28.283
c [worker] round 57, time: 28.235
c [worker] round 59, time: 29.226
c [worker] round 58, time: 28.697
c [worker] round 59, time: 29.279
c [worker] round 57, time: 28.161
c [worker] round 58, time: 28.645
c [worker] round 57, time: 28.149
c [worker] round 58, time: 28.786
c [worker] round 58, time: 28.741
c [worker] round 60, time: 29.731
c [worker] round 59, time: 29.203
c [worker] round 60, time: 29.783
c [worker] round 58, time: 28.663
c [worker] round 59, time: 29.147
c [worker] round 58, time: 28.650
c [worker] round 59, time: 29.292
c [worker] round 59, time: 29.243
c [worker] round 61, time: 30.234
c [worker] round 60, time: 29.706
c [worker] round 61, time: 30.286
c [worker] round 59, time: 29.165
c [worker] round 60, time: 29.648
c [worker] round 59, time: 29.151
c [worker] round 60, time: 29.795
c [worker] round 60, time: 29.749
c [worker] round 62, time: 30.737
c [worker] round 61, time: 30.211
c [worker] round 62, time: 30.789
c [worker] round 60, time: 29.666
c [worker] round 61, time: 30.151
c [worker] round 60, time: 29.655
c [worker] round 61, time: 30.298
c [worker] round 61, time: 30.251
c [worker] round 63, time: 31.239
c [worker] round 62, time: 30.713
c [worker] round 63, time: 31.292
c [worker] round 61, time: 30.168
c [worker] round 62, time: 30.655
c [worker] round 61, time: 30.159
c [worker] round 62, time: 30.804
c [worker] round 62, time: 30.753
c [worker] round 64, time: 31.742
c [worker] round 63, time: 31.215
c [worker] round 64, time: 31.794
c [worker] round 62, time: 30.671
c [worker] round 63, time: 31.157
c [worker] round 62, time: 30.663
c [worker] round 63, time: 31.306
c [worker] round 63, time: 31.257
c [worker] round 65, time: 32.247
c [worker] round 64, time: 31.719
c [worker] round 65, time: 32.297
c [worker] round 63, time: 31.172
c [worker] round 64, time: 31.659
c [worker] round 63, time: 31.167
c [worker] round 64, time: 31.809
c [worker] round 64, time: 31.761
c [worker] round 66, time: 32.751
c [worker] round 65, time: 32.221
c [worker] round 66, time: 32.799
c [worker] round 64, time: 31.674
c [worker] round 65, time: 32.163
c [worker] round 64, time: 31.671
c [worker] round 65, time: 32.311
c [worker] round 65, time: 32.263
c [worker] round 67, time: 33.253
c [worker] round 66, time: 32.723
c [worker] round 67, time: 33.303
c [worker] round 65, time: 32.179
c [worker] round 66, time: 32.665
c [worker] round 65, time: 32.175
c [worker] round 66, time: 32.814
c [worker] round 66, time: 32.765
c [worker] round 68, time: 33.756
c [worker] round 67, time: 33.227
c [worker] round 68, time: 33.807
c [worker] round 66, time: 32.681
c [worker] round 67, time: 33.166
c [worker] round 66, time: 32.676
c [worker] round 67, time: 33.316
c [worker] round 67, time: 33.267
c [worker] round 69, time: 34.258
c [worker] round 68, time: 33.730
c [worker] round 69, time: 34.310
c [worker] round 67, time: 33.182
c [worker] round 68, time: 33.667
c [worker] round 67, time: 33.179
c [worker] round 68, time: 33.819
c [worker] round 68, time: 33.770
c [worker] round 70, time: 34.763
c [worker] round 69, time: 34.255
c [worker] round 70, time: 34.815
c [worker] round 68, time: 33.684
c [worker] round 69, time: 34.169
c [worker] round 68, time: 33.683
c [worker] round 69, time: 34.322
c [worker] round 69, time: 34.272
c [worker] round 71, time: 35.266
c [worker] round 70, time: 34.759
c [worker] round 71, time: 35.318
c [worker] round 69, time: 34.186
c [worker] round 70, time: 34.670
c [worker] round 69, time: 34.185
c [worker] round 70, time: 34.824
c [worker] round 70, time: 34.774
c [worker] round 72, time: 35.771
c [worker] round 71, time: 35.263
c [worker] round 72, time: 35.821
c [worker] round 70, time: 34.688
c [worker] round 71, time: 35.172
c [worker] round 70, time: 34.686
c [worker] round 71, time: 35.327
c [worker] round 71, time: 35.281
c [worker] round 73, time: 36.275
c [worker] round 72, time: 35.766
c [worker] round 73, time: 36.324
c [worker] round 71, time: 35.190
c [worker] round 72, time: 35.675
c [worker] round 71, time: 35.187
c [worker] round 72, time: 35.830
c [worker] round 72, time: 35.783
c [worker] round 74, time: 36.778
c [worker] round 73, time: 36.271
c [worker] round 74, time: 36.831
c [worker] round 72, time: 35.692
c [worker] round 73, time: 36.179
c [worker] round 72, time: 35.688
c [worker] round 73, time: 36.336
c [worker] round 73, time: 36.286
c [worker] round 75, time: 37.281
c [worker] round 74, time: 36.774
c [worker] round 75, time: 37.334
c [worker] round 73, time: 36.194
c [worker] round 74, time: 36.681
c [worker] round 73, time: 36.191
c [worker] round 74, time: 36.840
c [worker] round 74, time: 36.793
c [worker] round 76, time: 37.784
c [worker] round 75, time: 37.276
c [worker] round 76, time: 37.838
c [worker] round 74, time: 36.696
c [worker] round 75, time: 37.182
c [worker] round 74, time: 36.695
c [worker] round 75, time: 37.343
c [worker] round 75, time: 37.295
c [worker] round 77, time: 38.287
c [worker] round 76, time: 37.779
c [worker] round 77, time: 38.343
c [worker] round 75, time: 37.198
c [worker] round 76, time: 37.684
c [worker] round 75, time: 37.199
c [worker] round 76, time: 37.847
c [worker] round 76, time: 37.798
c [worker] round 78, time: 38.789
c [worker] round 77, time: 38.283
c [worker] round 78, time: 38.847
c [worker] round 76, time: 37.699
c [worker] round 77, time: 38.186
c [worker] round 76, time: 37.701
c [worker] round 77, time: 38.351
c [worker] round 77, time: 38.300
c [worker] round 79, time: 39.293
c [worker] round 78, time: 38.786
c [worker] round 79, time: 39.351
c [worker] round 77, time: 38.203
c [worker] round 78, time: 38.691
c [worker] round 77, time: 38.203
c [worker] round 78, time: 38.856
c [worker] round 78, time: 38.803
c [worker] round 80, time: 39.799
c [worker] round 79, time: 39.288
c [worker] round 80, time: 39.855
c [worker] round 78, time: 38.707
c [worker] round 79, time: 39.195
c [worker] round 78, time: 38.704
c [worker] round 79, time: 39.360
c [worker] round 79, time: 39.313
c [worker] round 81, time: 40.307
c [worker] round 80, time: 39.792
c [worker] round 81, time: 40.367
c [worker] round 79, time: 39.210
c [worker] round 80, time: 39.699
c [worker] round 79, time: 39.207
c [worker] round 80, time: 39.865
c [worker] round 80, time: 39.818
c [worker] round 82, time: 40.814
c [worker] round 81, time: 40.299
c [worker] round 82, time: 40.874
c [worker] round 80, time: 39.714
c [worker] round 81, time: 40.203
c [worker] round 80, time: 39.709
c [worker] round 81, time: 40.376
c [worker] round 81, time: 40.324
c [worker] round 83, time: 41.323
c [worker] round 82, time: 40.807
c [worker] round 83, time: 41.390
c [worker] round 81, time: 40.219
c [worker] round 82, time: 40.706
c [worker] round 81, time: 40.211
c [worker] round 82, time: 40.830
c [worker] round 82, time: 40.896
c sharing nums: 82
c sharing time: 0.29
c [worker8] kissat exit with result: 20
c [worker] round 84, time: 41.829
c sharing nums: 84
c sharing time: 0.21
c [worker6] kissat exit with result: 20
c [worker] round 83, time: 41.315
c sharing nums: 83
c sharing time: 0.19
c [worker] round 82, time: 40.723
c [worker] round 84, time: 41.905
c sharing nums: 82
c sharing time: 0.11
c sharing nums: 84
c sharing time: 0.28
c [worker7] kissat exit with result: 20
c [worker] round 83, time: 41.209
c sharing nums: 83
c sharing time: 0.09
c [worker4] kissat exit with result: 0
c [worker] round 82, time: 40.713
c sharing nums: 82
c sharing time: 0.04
c [worker1] kissat exit with result: 20
c [worker2] kissat exit with result: 20
c [worker3] kissat exit with result: 0
c [worker] round 83, time: 41.335
c sharing nums: 83
c sharing time: 0.23
c [worker5] kissat exit with result: 20
s UNSATISFIABLE

real	44.97
user	5376.78
sys	85.75
mem	3563812