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/0447371bb8a97e8fe5d3cee6de1db766-UTI-20-10p0-sc2009.cnf "" CNF format instance c -------------------------------------------------- c [leader] preprocess(simplify) input data c After preprocess: vars: 259616 -> 203039 , clauses: 1374599 -> 1058485 , c sz 2 c turns: 2 c After preprocess: vars: 203039 -> 196678 , clauses: 1058485 -> 1045763 , 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.501 c [worker] round 2, time: 0.505 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.6 c [worker] round 3, time: 1.35 c [worker] round 2, time: 0.503 c [worker] round 2, time: 0.502 c [worker] round 2, time: 0.504 c [worker] round 2, time: 0.507 c [worker] round 1, time: 0.0 c [worker] round 4, time: 1.508 c [worker] round 3, time: 1.7 c [worker] round 1, time: 0.0 c [worker] round 3, time: 1.7 c [worker] round 4, time: 1.808 c [worker] round 3, time: 1.16 c [worker] round 3, time: 1.13 c [worker] round 2, time: 0.503 c [worker] round 5, time: 2.42 c [worker] round 4, time: 1.508 c [worker] round 2, time: 0.502 c [worker] round 4, time: 1.573 c [worker] round 3, time: 1.12 c [worker] round 4, time: 1.569 c [worker] round 4, time: 1.652 c [worker] round 5, time: 2.488 c [worker] round 6, time: 2.565 c [worker] round 5, time: 2.15 c [worker] round 3, time: 1.15 c [worker] round 5, time: 2.155 c [worker] round 4, time: 1.579 c [worker] round 5, time: 2.155 c [worker] round 5, time: 2.148 c [worker] round 6, time: 2.996 c [worker] round 7, time: 3.71 c [worker] round 6, time: 2.528 c [worker] round 4, time: 1.531 c [worker] round 5, time: 2.81 c [worker] round 6, time: 2.664 c [worker] round 7, time: 3.500 c [worker] round 6, time: 2.655 c [worker] round 6, time: 2.853 c [worker] round 8, time: 3.573 c [worker] round 7, time: 3.31 c [worker] round 5, time: 2.143 c [worker] round 6, time: 2.583 c [worker] round 7, time: 3.167 c [worker] round 7, time: 3.156 c [worker] round 8, time: 4.8 c [worker] round 7, time: 3.359 c [worker] round 9, time: 4.80 c [worker] round 8, time: 3.543 c [worker] round 6, time: 2.680 c [worker] round 7, time: 3.91 c [worker] round 8, time: 3.672 c [worker] round 9, time: 4.517 c [worker] round 8, time: 3.867 c [worker] round 10, time: 4.586 c [worker] round 9, time: 4.51 c [worker] round 7, time: 3.182 c [worker] round 8, time: 3.596 c [worker] round 8, time: 4.143 c [worker] round 9, time: 4.176 c [worker] round 10, time: 5.22 c [worker] round 9, time: 4.372 c [worker] round 11, time: 5.92 c [worker] round 10, time: 4.555 c [worker] round 8, time: 3.685 c [worker] round 9, time: 4.98 c [worker] round 10, time: 4.679 c [worker] round 9, time: 4.651 c [worker] round 11, time: 5.527 c [worker] round 10, time: 4.875 c [worker] round 12, time: 5.601 c [worker] round 11, time: 5.59 c [worker] round 9, time: 4.188 c [worker] round 10, time: 4.604 c [worker] round 11, time: 5.182 c [worker] round 10, time: 5.157 c [worker] round 12, time: 6.32 c [worker] round 11, time: 5.379 c [worker] round 13, time: 6.106 c [worker] round 12, time: 5.567 c [worker] round 10, time: 4.691 c [worker] round 11, time: 5.108 c [worker] round 12, time: 5.684 c [worker] round 11, time: 5.661 c [worker] round 13, time: 6.536 c [worker] round 12, time: 5.884 c [worker] round 14, time: 6.613 c [worker] round 13, time: 6.71 c [worker] round 11, time: 5.196 c [worker] round 12, time: 5.612 c [worker] round 13, time: 6.187 c [worker] round 12, time: 6.166 c [worker] round 14, time: 7.44 c [worker] round 13, time: 6.389 c [worker] round 15, time: 7.119 c [worker] round 14, time: 6.575 c [worker] round 12, time: 5.700 c [worker] round 13, time: 6.116 c [worker] round 14, time: 6.688 c [worker] round 13, time: 6.675 c [worker] round 15, time: 7.552 c [worker] round 14, time: 6.895 c [worker] round 16, time: 7.625 c [worker] round 15, time: 7.79 c [worker] round 13, time: 6.202 c [worker] round 14, time: 6.617 c [worker] round 15, time: 7.192 c [worker] round 14, time: 7.183 c [worker] round 16, time: 8.56 c [worker] round 15, time: 7.399 c [worker] round 17, time: 8.133 c [worker] round 16, time: 7.582 c [worker] round 14, time: 6.708 c [worker] round 15, time: 7.120 c [worker] round 16, time: 7.694 c [worker] round 15, time: 7.691 c [worker] round 17, time: 8.559 c [worker] round 16, time: 7.903 c [worker] round 18, time: 8.637 c [worker] round 17, time: 8.85 c [worker] round 15, time: 7.210 c [worker] round 16, time: 7.621 c [worker] round 17, time: 8.196 c [worker] round 16, time: 8.199 c [worker] round 18, time: 9.64 c [worker] round 17, time: 8.407 c [worker] round 19, time: 9.141 c [worker] round 18, time: 8.587 c [worker] round 16, time: 7.711 c [worker] round 17, time: 8.122 c [worker] round 18, time: 8.700 c [worker] round 17, time: 8.703 c [worker] round 19, time: 9.567 c [worker] round 18, time: 8.910 c [worker] round 20, time: 9.645 c [worker] round 19, time: 9.109 c [worker] round 17, time: 8.213 c [worker] round 18, time: 8.623 c [worker] round 19, time: 9.202 c [worker] round 18, time: 9.206 c [worker] round 20, time: 10.70 c [worker] round 19, time: 9.415 c [worker] round 21, time: 10.149 c [worker] round 20, time: 9.611 c [worker] round 18, time: 8.716 c [worker] round 19, time: 9.128 c [worker] round 20, time: 9.703 c [worker] round 19, time: 9.711 c [worker] round 21, time: 10.573 c [worker] round 20, time: 9.918 c [worker] round 22, time: 10.653 c [worker] round 21, time: 10.115 c [worker] round 19, time: 9.220 c [worker] round 20, time: 9.632 c [worker] round 21, time: 10.208 c [worker] round 20, time: 10.214 c [worker] round 22, time: 11.82 c [worker] round 21, time: 10.423 c [worker] round 23, time: 11.157 c [worker] round 22, time: 10.618 c [worker] round 20, time: 9.724 c [worker] round 21, time: 10.132 c [worker] round 22, time: 10.712 c [worker] round 21, time: 10.717 c [worker] round 23, time: 11.585 c [worker] round 22, time: 10.926 c [worker] round 24, time: 11.661 c [worker] round 23, time: 11.123 c [worker] round 21, time: 10.225 c [worker] round 22, time: 10.636 c [worker] round 23, time: 11.214 c [worker] round 22, time: 11.223 c [worker] round 24, time: 12.88 c [worker] round 23, time: 11.431 c [worker] round 25, time: 12.165 c [worker] round 24, time: 11.627 c [worker] round 22, time: 10.728 c [worker] round 23, time: 11.140 c [worker] round 24, time: 11.716 c [worker] round 23, time: 11.726 c [worker] round 25, time: 12.591 c [worker] round 24, time: 11.933 c [worker] round 26, time: 12.669 c [worker] round 25, time: 12.129 c [worker] round 23, time: 11.232 c [worker] round 24, time: 11.640 c [worker] round 25, time: 12.217 c [worker] round 24, time: 12.228 c [worker] round 26, time: 13.93 c [worker] round 25, time: 12.435 c [worker] round 27, time: 13.173 c [worker] round 26, time: 12.631 c [worker] round 24, time: 11.733 c [worker] round 25, time: 12.144 c [worker] round 26, time: 12.718 c [worker] round 25, time: 12.730 c [worker] round 27, time: 13.595 c [worker] round 26, time: 12.939 c [worker] round 28, time: 13.677 c [worker] round 27, time: 13.135 c [worker] round 25, time: 12.234 c [worker] round 26, time: 12.648 c [worker] round 27, time: 13.219 c [worker] round 26, time: 13.235 c [worker] round 28, time: 14.96 c [worker] round 27, time: 13.441 c [worker] round 29, time: 14.179 c [worker] round 28, time: 13.637 c [worker] round 26, time: 12.735 c [worker] round 27, time: 13.148 c [worker] round 28, time: 13.720 c [worker] round 27, time: 13.739 c [worker] round 29, time: 14.600 c [worker] round 28, time: 13.942 c [worker] round 30, time: 14.681 c [worker] round 29, time: 14.139 c [worker] round 27, time: 13.235 c [worker] round 28, time: 13.649 c [worker] round 29, time: 14.221 c [worker] round 28, time: 14.243 c [worker] round 30, time: 15.102 c [worker] round 29, time: 14.443 c [worker] round 31, time: 15.183 c [worker] round 30, time: 14.643 c [worker] round 28, time: 13.736 c [worker] round 29, time: 14.149 c [worker] round 30, time: 14.724 c [worker] round 29, time: 14.747 c [worker] round 31, time: 15.604 c [worker] round 30, time: 14.947 c [worker] round 32, time: 15.685 c [worker] round 31, time: 15.145 c [worker] round 29, time: 14.237 c [worker] round 30, time: 14.650 c [worker] round 31, time: 15.225 c [worker] round 30, time: 15.249 c [worker] round 32, time: 16.108 c [worker] round 31, time: 15.451 c [worker] round 33, time: 16.189 c [worker] round 32, time: 15.646 c [worker] round 30, time: 14.738 c [worker] round 31, time: 15.150 c [worker] round 32, time: 15.728 c [worker] round 31, time: 15.750 c [worker] round 33, time: 16.612 c [worker] round 32, time: 15.955 c [worker] round 34, time: 16.691 c [worker] round 33, time: 16.188 c [worker] round 31, time: 15.240 c [worker] round 32, time: 15.651 c [worker] round 33, time: 16.230 c [worker] round 32, time: 16.252 c [worker] round 34, time: 17.114 c [worker] round 33, time: 16.459 c [worker] round 35, time: 17.193 c [worker] round 34, time: 16.691 c [worker] round 32, time: 15.744 c [worker] round 33, time: 16.152 c [worker] round 34, time: 16.731 c [worker] round 33, time: 16.754 c [worker] round 35, time: 17.615 c [worker] round 34, time: 16.961 c [worker] round 36, time: 17.695 c [worker] round 35, time: 17.193 c [worker] round 33, time: 16.245 c [worker] round 34, time: 16.653 c [worker] round 35, time: 17.232 c [worker] round 34, time: 17.259 c [worker] round 36, time: 18.120 c [worker] round 35, time: 17.463 c [worker] round 37, time: 18.197 c [worker] round 36, time: 17.700 c [worker] round 34, time: 16.748 c [worker] round 35, time: 17.156 c [worker] round 36, time: 17.736 c [worker] round 35, time: 17.763 c [worker] round 37, time: 18.623 c [worker] round 36, time: 17.967 c [worker] round 38, time: 18.701 c [worker] round 37, time: 18.202 c [worker] round 35, time: 17.249 c [worker] round 36, time: 17.660 c [worker] round 37, time: 18.238 c [worker] round 36, time: 18.267 c [worker] round 38, time: 19.128 c [worker] round 37, time: 18.471 c [worker] round 39, time: 19.204 c [worker] round 38, time: 18.704 c [worker] round 36, time: 17.751 c [worker] round 37, time: 18.161 c [worker] round 38, time: 18.740 c [worker] round 37, time: 18.771 c [worker] round 39, time: 19.631 c [worker] round 38, time: 18.974 c [worker] round 40, time: 19.709 c [worker] round 39, time: 19.207 c [worker] round 37, time: 18.256 c [worker] round 38, time: 18.662 c [worker] round 39, time: 19.242 c [worker] round 38, time: 19.275 c [worker] round 40, time: 20.136 c [worker] round 39, time: 19.479 c [worker] round 41, time: 20.212 c [worker] round 40, time: 19.710 c [worker] round 38, time: 18.760 c [worker] round 39, time: 19.163 c [worker] round 40, time: 19.743 c [worker] round 39, time: 19.779 c [worker] round 41, time: 20.639 c [worker] round 40, time: 19.982 c [worker] round 42, time: 20.717 c [worker] round 41, time: 20.212 c [worker] round 39, time: 19.261 c [worker] round 40, time: 19.664 c [worker] round 41, time: 20.248 c [worker] round 40, time: 20.282 c [worker] round 42, time: 21.143 c [worker] round 41, time: 20.487 c [worker] round 43, time: 21.220 c [worker] round 42, time: 20.715 c [worker] round 40, time: 19.763 c [worker] round 41, time: 20.168 c [worker] round 42, time: 20.752 c [worker] round 41, time: 20.786 c [worker] round 43, time: 21.646 c [worker] round 42, time: 20.990 c [worker] round 44, time: 21.724 c [worker] round 43, time: 21.218 c [worker] round 41, time: 20.268 c [worker] round 42, time: 20.672 c [worker] round 43, time: 21.254 c [worker] round 42, time: 21.291 c [worker] round 44, time: 22.152 c [worker] round 43, time: 21.495 c [worker] round 45, time: 22.229 c [worker] round 44, time: 21.721 c [worker] round 42, time: 20.769 c [worker] round 43, time: 21.173 c [worker] round 44, time: 21.755 c [worker] round 43, time: 21.794 c [worker] round 45, time: 22.655 c [worker] round 44, time: 21.998 c [worker] round 46, time: 22.732 c [worker] round 45, time: 22.223 c [worker] round 43, time: 21.271 c [worker] round 44, time: 21.676 c [worker] round 45, time: 22.261 c [worker] round 44, time: 22.297 c [worker] round 46, time: 23.160 c [worker] round 45, time: 22.500 c [worker] round 47, time: 23.236 c [worker] round 46, time: 22.725 c [worker] round 44, time: 21.776 c [worker] round 45, time: 22.177 c [worker] round 46, time: 22.762 c [worker] round 45, time: 22.801 c [worker] round 47, time: 23.663 c [worker] round 46, time: 23.3 c [worker] round 48, time: 23.738 c [worker] round 47, time: 23.232 c [worker] round 45, time: 22.280 c [worker] round 46, time: 22.680 c [worker] round 47, time: 23.264 c [worker] round 46, time: 23.304 c [worker] round 48, time: 24.168 c [worker] round 47, time: 23.514 c [worker] round 49, time: 24.242 c [worker] round 48, time: 23.734 c [worker] round 46, time: 22.784 c [worker] round 47, time: 23.181 c [worker] round 48, time: 23.765 c [worker] round 47, time: 23.807 c [worker] round 49, time: 24.671 c [worker] round 48, time: 24.19 c [worker] round 50, time: 24.747 c [worker] round 49, time: 24.240 c [worker] round 47, time: 23.286 c [worker] round 48, time: 23.682 c [worker] round 49, time: 24.267 c [worker] round 48, time: 24.311 c [worker] round 50, time: 25.174 c [worker] round 49, time: 24.522 c [worker] round 51, time: 25.253 c [worker] round 50, time: 24.742 c [worker] round 48, time: 23.787 c [worker] round 49, time: 24.183 c [worker] round 50, time: 24.768 c [worker] round 49, time: 24.814 c [worker] round 51, time: 25.676 c [worker] round 50, time: 25.24 c [worker] round 52, time: 25.756 c [worker] round 51, time: 25.244 c [worker] round 49, time: 24.292 c [worker] round 50, time: 24.688 c [worker] round 51, time: 25.272 c [worker] round 50, time: 25.319 c [worker] round 52, time: 26.179 c [worker] round 51, time: 25.527 c [worker] round 53, time: 26.260 c [worker] round 52, time: 25.746 c [worker] round 50, time: 24.796 c [worker] round 51, time: 25.192 c [worker] round 52, time: 25.774 c [worker] round 51, time: 25.822 c [worker] round 53, time: 26.684 c [worker] round 52, time: 26.30 c [worker] round 54, time: 26.762 c [worker] round 53, time: 26.252 c [worker] round 51, time: 25.297 c [worker] round 52, time: 25.696 c [worker] round 53, time: 26.276 c [worker] round 52, time: 26.327 c [worker] round 54, time: 27.188 c [worker] round 53, time: 26.535 c [worker] round 55, time: 27.269 c [worker] round 54, time: 26.753 c [worker] round 52, time: 25.799 c [worker] round 53, time: 26.196 c [worker] round 54, time: 26.778 c [worker] round 53, time: 26.830 c [worker] round 55, time: 27.692 c [worker] round 54, time: 27.40 c [worker] round 56, time: 27.772 c [worker] round 55, time: 27.255 c [worker] round 53, time: 26.300 c [worker] round 54, time: 26.697 c [worker] round 55, time: 27.279 c [worker] round 54, time: 27.333 c [worker] round 56, time: 28.196 c [worker] round 55, time: 27.541 c [worker] round 57, time: 28.277 c [worker] round 56, time: 27.757 c [worker] round 54, time: 26.802 c [worker] round 55, time: 27.198 c [worker] round 56, time: 27.780 c [worker] round 55, time: 27.839 c [worker] round 57, time: 28.699 c [worker] round 56, time: 28.44 c [worker] round 58, time: 28.780 c [worker] round 57, time: 28.260 c [worker] round 55, time: 27.303 c [worker] round 56, time: 27.699 c [worker] round 57, time: 28.281 c [worker] round 56, time: 28.343 c [worker] round 58, time: 29.204 c [worker] round 57, time: 28.547 c [worker] round 59, time: 29.282 c [worker] round 58, time: 28.763 c [worker] round 56, time: 27.808 c [worker] round 57, time: 28.199 c [worker] round 58, time: 28.784 c [worker] round 57, time: 28.845 c [worker] round 59, time: 29.708 c [worker] round 58, time: 29.49 c [worker] round 60, time: 29.785 c [worker] round 59, time: 29.265 c [worker] round 57, time: 28.309 c [worker] round 58, time: 28.700 c [worker] round 59, time: 29.286 c [worker] round 58, time: 29.351 c [worker] round 60, time: 30.211 c [worker] round 59, time: 29.551 c [worker] round 61, time: 30.289 c [worker] round 60, time: 29.767 c [worker] round 58, time: 28.810 c [worker] round 59, time: 29.201 c [worker] round 60, time: 29.788 c [worker] round 59, time: 29.855 c [worker] round 61, time: 30.716 c [worker] round 60, time: 30.53 c [worker] round 62, time: 30.792 c [worker] round 61, time: 30.268 c [worker] round 59, time: 29.312 c [worker] round 60, time: 29.702 c [worker] round 61, time: 30.292 c [worker] round 60, time: 30.357 c [worker] round 62, time: 31.218 c [worker] round 61, time: 30.555 c [worker] round 63, time: 31.297 c [worker] round 62, time: 30.770 c [worker] round 60, time: 29.813 c [worker] round 61, time: 30.204 c [worker] round 62, time: 30.796 c [worker] round 61, time: 30.861 c [worker] round 63, time: 31.721 c [worker] round 62, time: 31.59 c [worker] round 64, time: 31.801 c [worker] round 63, time: 31.275 c [worker] round 61, time: 30.316 c [worker] round 62, time: 30.708 c [worker] round 63, time: 31.300 c [worker] round 62, time: 31.364 c [worker] round 64, time: 32.223 c [worker] round 63, time: 31.562 c [worker] round 65, time: 32.304 c [worker] round 64, time: 31.784 c [worker] round 62, time: 30.818 c [worker] round 63, time: 31.212 c [worker] round 64, time: 31.802 c [worker] round 63, time: 31.871 c [worker] round 65, time: 32.725 c [worker] round 64, time: 32.68 c [worker] round 66, time: 32.807 c [worker] round 65, time: 32.286 c [worker] round 63, time: 31.319 c [worker] round 64, time: 31.713 c [worker] round 65, time: 32.303 c [worker] round 64, time: 32.375 c [worker] round 66, time: 33.228 c [worker] round 65, time: 32.570 c [worker] round 67, time: 33.309 c [worker] round 66, time: 32.788 c [worker] round 64, time: 31.821 c [worker] round 65, time: 32.216 c [worker] round 66, time: 32.804 c [worker] round 65, time: 32.879 c [worker] round 67, time: 33.732 c [worker] round 66, time: 33.75 c [worker] round 68, time: 33.812 c [worker] round 67, time: 33.290 c [worker] round 65, time: 32.323 c [worker] round 66, time: 32.717 c [worker] round 67, time: 33.306 c [worker] round 66, time: 33.382 c [worker] round 68, time: 34.235 c [worker] round 67, time: 33.578 c [worker] round 69, time: 34.317 c [worker] round 68, time: 33.792 c [worker] round 66, time: 32.828 c [worker] round 67, time: 33.220 c [worker] round 68, time: 33.808 c [worker] round 67, time: 33.885 c [worker] round 69, time: 34.738 c [worker] round 68, time: 34.83 c [worker] round 70, time: 34.822 c [worker] round 69, time: 34.295 c [worker] round 67, time: 33.330 c [worker] round 68, time: 33.720 c [worker] round 69, time: 34.312 c [worker] round 68, time: 34.388 c [worker] round 70, time: 35.241 c [worker] round 69, time: 34.587 c [worker] round 71, time: 35.325 c [worker] round 70, time: 34.799 c [worker] round 68, time: 33.831 c [worker] round 69, time: 34.221 c [worker] round 70, time: 34.816 c [worker] round 69, time: 34.891 c [worker] round 71, time: 35.744 c [worker] round 70, time: 35.91 c [worker] round 72, time: 35.828 c [worker] round 71, time: 35.303 c [worker] round 69, time: 34.336 c [worker] round 70, time: 34.723 c [worker] round 71, time: 35.318 c [worker] round 72, time: 36.247 c [worker] round 70, time: 35.399 c [worker] round 71, time: 35.593 c [worker] round 73, time: 36.332 c [worker] round 72, time: 35.806 c [worker] round 70, time: 34.838 c [worker] round 71, time: 35.228 c [worker] round 72, time: 35.820 c [worker] round 73, time: 36.750 c [worker] round 71, time: 35.903 c [worker] round 72, time: 36.100 c [worker] round 74, time: 36.837 c [worker] round 73, time: 36.312 c [worker] round 71, time: 35.340 c [worker] round 72, time: 35.729 c [worker] round 73, time: 36.322 c [worker] round 74, time: 37.254 c [worker] round 72, time: 36.411 c [worker] round 73, time: 36.602 c [worker] round 75, time: 37.340 c [worker] round 74, time: 36.815 c [worker] round 72, time: 35.843 c [worker] round 73, time: 36.232 c [worker] round 74, time: 36.824 c [worker] round 75, time: 37.757 c [worker] round 73, time: 36.914 c [worker] round 74, time: 37.107 c [worker] round 76, time: 37.843 c [worker] round 75, time: 37.320 c [worker] round 73, time: 36.345 c [worker] round 74, time: 36.736 c [worker] round 75, time: 37.325 c [worker] round 76, time: 38.260 c [worker] round 74, time: 37.419 c [worker] round 75, time: 37.611 c [worker] round 77, time: 38.349 c [worker] round 76, time: 37.822 c [worker] round 74, time: 36.846 c [worker] round 75, time: 37.240 c [worker] round 76, time: 37.828 c [worker] round 77, time: 38.763 c [worker] round 75, time: 37.922 c [worker] round 76, time: 38.115 c [worker] round 78, time: 38.853 c [worker] round 77, time: 38.324 c [worker] round 75, time: 37.348 c [worker] round 76, time: 37.744 c [worker] round 77, time: 38.331 c [worker] round 78, time: 39.266 c [worker] round 76, time: 38.426 c [worker] round 77, time: 38.619 c [worker] round 79, time: 39.356 c [worker] round 78, time: 38.826 c [worker] round 76, time: 37.852 c [worker] round 77, time: 38.245 c [worker] round 78, time: 38.832 c [worker] round 79, time: 39.770 c [worker] round 77, time: 38.931 c [worker] round 78, time: 39.122 c [worker] round 80, time: 39.860 c [worker] round 79, time: 39.328 c [worker] round 77, time: 38.353 c [worker] round 78, time: 38.746 c [worker] round 79, time: 39.336 c [worker] round 80, time: 40.276 c [worker] round 78, time: 39.434 c [worker] round 79, time: 39.627 c [worker] round 81, time: 40.363 c [worker] round 80, time: 39.831 c [worker] round 78, time: 38.855 c [worker] round 79, time: 39.247 c [worker] round 80, time: 39.840 c [worker] round 81, time: 40.779 c [worker] round 79, time: 39.937 c [worker] round 80, time: 40.131 c [worker] round 82, time: 40.866 c [worker] round 81, time: 40.333 c [worker] round 79, time: 39.357 c [worker] round 80, time: 39.748 c [worker] round 81, time: 40.342 c [worker] round 82, time: 41.282 c [worker] round 80, time: 40.443 c [worker] round 81, time: 40.635 c [worker] round 83, time: 41.373 c [worker] round 82, time: 40.835 c [worker] round 80, time: 39.859 c [worker] round 81, time: 40.252 c [worker] round 82, time: 40.843 c [worker] round 83, time: 41.788 c [worker] round 81, time: 40.947 c [worker] round 82, time: 41.138 c [worker] round 84, time: 41.876 c [worker] round 83, time: 41.339 c [worker] round 81, time: 40.364 c [worker] round 82, time: 40.788 c [worker] round 83, time: 41.348 c [worker] round 84, time: 42.291 c [worker] round 82, time: 41.450 c [worker] round 83, time: 41.643 c [worker] round 85, time: 42.379 c [worker] round 84, time: 41.843 c [worker] round 82, time: 40.865 c [worker] round 83, time: 41.292 c [worker] round 84, time: 41.850 c [worker] round 85, time: 42.796 c [worker] round 83, time: 41.953 c [worker] round 84, time: 42.147 c [worker] round 86, time: 42.885 c [worker] round 85, time: 42.347 c [worker] round 83, time: 41.367 c [worker] round 85, time: 42.351 c [worker] round 84, time: 41.796 c [worker] round 84, time: 42.459 c [worker] round 86, time: 43.300 c [worker] round 85, time: 42.651 c [worker] round 87, time: 43.389 c [worker] round 86, time: 42.850 c [worker] round 84, time: 41.872 c [worker] round 85, time: 42.296 c [worker] round 86, time: 42.852 c [worker] round 87, time: 43.802 c [worker] round 85, time: 42.962 c [worker] round 86, time: 43.154 c [worker] round 88, time: 43.892 c [worker] round 87, time: 43.355 c [worker] round 85, time: 42.373 c [worker] round 87, time: 43.356 c [worker] round 86, time: 42.800 c [worker] round 88, time: 44.308 c [worker] round 86, time: 43.467 c [worker] round 87, time: 43.660 c [worker] round 89, time: 44.395 c [worker] round 88, time: 43.858 c [worker] round 86, time: 42.875 c [worker] round 87, time: 43.304 c [worker] round 88, time: 43.860 c [worker] round 89, time: 44.812 c [worker] round 87, time: 43.970 c [worker] round 88, time: 44.162 c [worker] round 90, time: 44.899 c [worker] round 89, time: 44.360 c [worker] round 87, time: 43.377 c [worker] round 88, time: 43.805 c [worker] round 89, time: 44.362 c [worker] round 90, time: 45.316 c [worker] round 88, time: 44.475 c [worker] round 89, time: 44.667 c [worker] round 91, time: 45.402 c [worker] round 90, time: 44.863 c [worker] round 88, time: 43.879 c [worker] round 90, time: 44.863 c [worker] round 89, time: 44.308 c [worker] round 91, time: 45.819 c [worker] round 89, time: 44.979 c [worker] round 90, time: 45.170 c [worker] round 92, time: 45.906 c [worker] round 91, time: 45.368 c [worker] round 89, time: 44.384 c [worker] round 90, time: 44.809 c [worker] round 91, time: 45.365 c [worker] round 92, time: 46.322 c [worker] round 90, time: 45.487 c [worker] round 91, time: 45.676 c [worker] round 93, time: 46.409 c [worker] round 92, time: 45.870 c [worker] round 90, time: 44.888 c [worker] round 91, time: 45.310 c [worker] round 92, time: 45.868 c [worker] round 93, time: 46.825 c [worker] round 91, time: 45.991 c [worker] round 92, time: 46.178 c [worker] round 94, time: 46.913 c [worker] round 93, time: 46.372 c [worker] round 91, time: 45.390 c [worker] round 92, time: 45.811 c [worker] round 93, time: 46.370 c [worker] round 94, time: 47.328 c [worker] round 92, time: 46.495 c [worker] round 93, time: 46.683 c [worker] round 95, time: 47.417 c [worker] round 94, time: 46.875 c [worker] round 92, time: 45.896 c [worker] round 93, time: 46.312 c [worker] round 94, time: 46.871 c [worker] round 95, time: 47.833 c [worker] round 93, time: 47.3 c [worker] round 94, time: 47.188 c [worker] round 96, time: 47.921 c [worker] round 95, time: 47.378 c [worker] round 93, time: 46.400 c [worker] round 94, time: 46.813 c [worker] round 95, time: 47.373 c [worker] round 96, time: 48.336 c [worker] round 94, time: 47.507 c [worker] round 95, time: 47.691 c [worker] round 97, time: 48.433 c [worker] round 96, time: 47.898 c [worker] round 94, time: 46.904 c [worker] round 95, time: 47.314 c [worker] round 96, time: 47.875 c [worker] round 97, time: 48.840 c [worker] round 95, time: 48.15 c [worker] round 96, time: 48.195 c [worker] round 98, time: 48.937 c [worker] round 97, time: 48.401 c [worker] round 95, time: 47.408 c [worker] round 96, time: 47.820 c [worker] round 97, time: 48.380 c [worker] round 98, time: 49.352 c [worker] round 96, time: 48.519 c [worker] round 97, time: 48.703 c [worker] round 99, time: 49.446 c [worker] round 98, time: 48.904 c [worker] round 96, time: 47.912 c [worker] round 97, time: 48.321 c [worker] round 98, time: 48.884 c [worker] round 99, time: 49.860 c [worker] round 97, time: 49.24 c [worker] round 98, time: 49.207 c [worker] round 100, time: 49.953 c [worker] round 99, time: 49.412 c [worker] round 97, time: 48.415 c [worker] round 98, time: 48.824 c [worker] round 99, time: 49.389 c [worker] round 100, time: 50.368 c [worker] round 98, time: 49.531 c [worker] round 99, time: 49.712 c [worker] round 101, time: 50.458 c [worker] round 100, time: 49.920 c [worker] round 98, time: 48.919 c [worker] round 99, time: 49.328 c [worker] round 100, time: 49.904 c [worker] round 101, time: 50.873 c [worker] round 99, time: 50.37 c [worker] round 100, time: 50.219 c [worker] round 102, time: 50.964 c [worker] round 101, time: 50.424 c [worker] round 99, time: 49.424 c [worker] round 100, time: 49.832 c [worker] round 101, time: 50.408 c [worker] round 102, time: 51.379 c [worker] round 100, time: 50.547 c [worker] round 101, time: 50.727 c [worker] round 103, time: 51.477 c [worker] round 102, time: 50.932 c [worker] round 100, time: 49.928 c [worker] round 101, time: 50.336 c [worker] round 102, time: 50.912 c [worker] round 103, time: 51.890 c [worker] round 101, time: 51.59 c [worker] round 102, time: 51.235 c [worker] round 104, time: 51.985 c [worker] round 103, time: 51.439 c [worker] round 101, time: 50.432 c [worker] round 102, time: 50.840 c [worker] round 103, time: 51.416 c [worker] round 104, time: 52.408 c [worker] round 102, time: 51.567 c [worker] round 103, time: 51.744 c [worker] round 105, time: 52.492 c [worker] round 104, time: 51.946 c [worker] round 102, time: 50.951 c [worker] round 103, time: 51.344 c [worker] round 104, time: 51.920 c [worker] round 105, time: 52.916 c [worker] round 103, time: 52.75 c [worker] round 104, time: 52.251 c [worker] round 106, time: 53.3 c [worker] round 105, time: 52.451 c [worker] round 103, time: 51.460 c [worker] round 104, time: 51.848 c [worker] round 105, time: 52.424 c [worker] round 104, time: 52.583 c [worker] round 106, time: 53.424 c [worker] round 105, time: 52.759 c [worker] round 107, time: 53.511 c [worker] round 106, time: 52.959 c [worker] round 104, time: 51.963 c [worker] round 105, time: 52.352 c [worker] round 106, time: 52.927 c [worker] round 107, time: 53.935 c [worker] round 105, time: 53.90 c [worker] round 106, time: 53.266 c [worker] round 108, time: 54.25 c [worker] round 107, time: 53.465 c [worker] round 105, time: 52.467 c [worker] round 106, time: 52.854 c [worker] round 107, time: 53.431 c [worker] round 106, time: 53.598 c [worker] round 108, time: 54.452 c [worker] round 107, time: 53.775 c [worker] round 109, time: 54.549 c [worker] round 108, time: 53.970 c [worker] round 106, time: 52.971 c [worker] round 107, time: 53.355 c [worker] round 108, time: 53.937 c [worker] round 109, time: 54.959 c [worker] round 107, time: 54.119 c [worker] round 108, time: 54.283 c [worker] round 110, time: 55.57 c [worker] round 109, time: 54.475 c [worker] round 107, time: 53.476 c [worker] round 108, time: 53.858 c [worker] round 109, time: 54.440 c [worker] round 110, time: 55.468 c [worker] round 108, time: 54.629 c [worker] round 109, time: 54.790 c [worker] round 110, time: 54.983 c [worker] round 111, time: 55.585 c [worker] round 108, time: 53.984 c [worker] round 109, time: 54.360 c [worker] round 110, time: 54.945 c [worker] round 111, time: 55.977 c [worker] round 109, time: 55.139 c [worker] round 110, time: 55.299 c [worker] round 111, time: 55.492 c [worker] round 112, time: 56.92 c [worker] round 109, time: 54.488 c [worker] round 110, time: 54.864 c [worker] round 111, time: 55.448 c [worker] round 110, time: 55.647 c [worker] round 112, time: 56.500 c [worker] round 111, time: 55.807 c [worker] round 112, time: 55.999 c [worker] round 113, time: 56.603 c [worker] round 110, time: 54.996 c [worker] round 111, time: 55.366 c [worker] round 112, time: 55.952 c [worker] round 113, time: 57.8 c [worker] round 111, time: 56.168 c [worker] round 112, time: 56.313 c [worker] round 113, time: 56.505 c [worker] round 114, time: 57.113 c [worker] round 111, time: 55.504 c [worker] round 112, time: 55.872 c [worker] round 113, time: 56.457 c [worker] round 114, time: 57.515 c [worker] round 112, time: 56.697 c [worker] round 113, time: 56.824 c [worker] round 114, time: 57.11 c [worker] round 115, time: 57.621 c [worker] round 112, time: 56.12 c [worker] round 113, time: 56.374 c [worker] round 114, time: 56.960 c [worker] round 115, time: 58.24 c [worker] round 113, time: 57.207 c [worker] round 114, time: 57.331 c [worker] round 115, time: 57.517 c [worker] round 116, time: 58.134 c [worker] round 113, time: 56.516 c [worker] round 114, time: 56.880 c [worker] round 115, time: 57.464 c [worker] round 116, time: 58.546 c [worker] round 115, time: 57.837 c [worker] round 114, time: 57.727 c [worker] round 116, time: 58.23 c [worker] round 117, time: 58.650 c [worker] round 114, time: 57.24 c [worker] round 115, time: 57.382 c [worker] round 116, time: 57.968 c [worker] round 117, time: 59.62 c [worker] round 116, time: 58.343 c [worker] round 115, time: 58.235 c [worker] round 117, time: 58.531 c [worker] round 118, time: 59.171 c [worker] round 115, time: 57.532 c [worker] round 116, time: 57.884 c [worker] round 117, time: 58.472 c [worker] round 117, time: 58.850 c [worker] round 118, time: 59.580 c [worker] round 116, time: 58.743 c sharing nums: 116 c sharing time: 1.08 c [worker] round 118, time: 59.38 c [worker8] kissat exit with result: 20 c sharing nums: 118 c sharing time: 0.38 c [worker4] kissat exit with result: 0 c [worker] round 119, time: 59.681 c sharing nums: 119 c sharing time: 0.54 c [worker] round 116, time: 58.40 c [worker7] kissat exit with result: 0 c [worker] round 117, time: 58.388 c sharing nums: 117 c sharing time: 0.18 c sharing nums: 116 c sharing time: 0.41 c [worker] round 118, time: 58.976 c sharing nums: 118 c sharing time: 0.30 c [worker1] kissat exit with result: 0 c [worker3] kissat exit with result: 0 c [worker2] kissat exit with result: 0 c [worker] round 119, time: 60.87 c [worker] round 118, time: 59.359 c sharing nums: 119 c sharing time: 0.92 c sharing nums: 118 c sharing time: 0.66 c [worker6] kissat exit with result: 0 c [worker5] kissat exit with result: 0 s UNSATISFIABLE real 64.56 user 7691.84 sys 91.34 mem 2969092