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/c9886f58320a360adbc8db9470563bea-ctl_4291_567_12_unsat.cnf "" CNF format instance c -------------------------------------------------- c [leader] preprocess(simplify) input data c After preprocess: vars: 17850 -> 17850 , clauses: 156259 -> 156259 , c [CE] almost one cons: 29227 c sz 2 c turns: 1 c After preprocess: vars: 17850 -> 17850 , clauses: 156259 -> 156259 , 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 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 1, time: 0.0 c [worker] round 1, time: 0.0 c [worker] round 2, time: 0.501 c [worker] round 2, time: 0.501 c [worker] round 2, time: 0.502 c [worker] round 2, time: 0.502 c [worker] round 2, time: 0.502 c [worker] round 2, time: 0.501 c [worker] round 2, time: 0.502 c [worker] round 2, time: 0.503 c [worker] round 3, time: 1.6 c [worker] round 3, time: 1.6 c [worker] round 3, time: 1.7 c [worker] round 3, time: 1.3 c [worker] round 3, time: 1.33 c [worker] round 3, time: 1.4 c [worker] round 3, time: 1.6 c [worker] round 3, time: 1.6 c [worker] round 4, time: 1.509 c [worker] round 4, time: 1.509 c [worker] round 4, time: 1.509 c [worker] round 4, time: 1.507 c [worker] round 4, time: 1.536 c [worker] round 4, time: 1.506 c [worker] round 4, time: 1.507 c [worker] round 4, time: 1.510 c [worker] round 5, time: 2.15 c [worker] round 5, time: 2.11 c [worker] round 5, time: 2.12 c [worker] round 5, time: 2.11 c [worker] round 5, time: 2.40 c [worker] round 5, time: 2.7 c [worker] round 5, time: 2.8 c [worker] round 5, time: 2.16 c [worker] round 6, time: 2.518 c [worker] round 6, time: 2.513 c [worker] round 6, time: 2.514 c [worker] round 6, time: 2.515 c [worker] round 6, time: 2.544 c [worker] round 6, time: 2.509 c [worker] round 6, time: 2.510 c [worker] round 6, time: 2.518 c [worker] round 7, time: 3.20 c [worker] round 7, time: 3.15 c [worker] round 7, time: 3.16 c [worker] round 7, time: 3.19 c [worker] round 7, time: 3.47 c [worker] round 7, time: 3.10 c [worker] round 7, time: 3.11 c [worker] round 7, time: 3.21 c [worker] round 8, time: 3.523 c [worker] round 8, time: 3.517 c [worker] round 8, time: 3.518 c [worker] round 8, time: 3.522 c [worker] round 8, time: 3.550 c [worker] round 8, time: 3.516 c [worker] round 8, time: 3.512 c [worker] round 8, time: 3.523 c [worker] round 9, time: 4.25 c [worker] round 9, time: 4.18 c [worker] round 9, time: 4.20 c [worker] round 9, time: 4.25 c [worker] round 9, time: 4.52 c [worker] round 9, time: 4.17 c [worker] round 9, time: 4.13 c [worker] round 9, time: 4.25 c [worker] round 10, time: 4.527 c [worker] round 10, time: 4.520 c [worker] round 10, time: 4.521 c [worker] round 10, time: 4.528 c [worker] round 10, time: 4.554 c [worker] round 10, time: 4.519 c [worker] round 10, time: 4.513 c [worker] round 10, time: 4.527 c [worker] round 11, time: 5.29 c [worker] round 11, time: 5.21 c [worker] round 11, time: 5.23 c [worker] round 11, time: 5.30 c [worker] round 11, time: 5.56 c [worker] round 11, time: 5.20 c [worker] round 11, time: 5.14 c [worker] round 11, time: 5.29 c [worker] round 12, time: 5.531 c [worker] round 12, time: 5.523 c [worker] round 12, time: 5.524 c [worker] round 12, time: 5.532 c [worker] round 12, time: 5.558 c [worker] round 12, time: 5.521 c [worker] round 12, time: 5.515 c [worker] round 12, time: 5.531 c [worker] round 13, time: 6.33 c [worker] round 13, time: 6.24 c [worker] round 13, time: 6.26 c [worker] round 13, time: 6.34 c [worker] round 13, time: 6.60 c [worker] round 13, time: 6.23 c [worker] round 13, time: 6.16 c [worker] round 13, time: 6.33 c [worker] round 14, time: 6.535 c [worker] round 14, time: 6.525 c [worker] round 14, time: 6.527 c [worker] round 14, time: 6.536 c [worker] round 14, time: 6.562 c [worker] round 14, time: 6.524 c [worker] round 14, time: 6.517 c [worker] round 14, time: 6.534 c [worker] round 15, time: 7.37 c [worker] round 15, time: 7.27 c [worker] round 15, time: 7.29 c [worker] round 15, time: 7.38 c [worker] round 15, time: 7.64 c [worker] round 15, time: 7.25 c [worker] round 15, time: 7.18 c [worker] round 15, time: 7.37 c [worker] round 16, time: 7.539 c [worker] round 16, time: 7.528 c [worker] round 16, time: 7.531 c [worker] round 16, time: 7.540 c [worker] round 16, time: 7.566 c [worker] round 16, time: 7.527 c [worker] round 16, time: 7.519 c [worker] round 16, time: 7.539 c [worker] round 17, time: 8.41 c [worker] round 17, time: 8.30 c [worker] round 17, time: 8.32 c [worker] round 17, time: 8.43 c [worker] round 17, time: 8.69 c [worker] round 17, time: 8.28 c [worker] round 17, time: 8.20 c [worker] round 17, time: 8.41 c [worker] round 18, time: 8.543 c [worker] round 18, time: 8.531 c [worker] round 18, time: 8.549 c [worker] round 18, time: 8.545 c [worker] round 18, time: 8.571 c [worker] round 18, time: 8.529 c [worker] round 18, time: 8.520 c [worker] round 18, time: 8.543 c [worker] round 19, time: 9.44 c [worker] round 19, time: 9.32 c [worker] round 19, time: 9.50 c [worker] round 19, time: 9.48 c [worker] round 19, time: 9.72 c [worker] round 19, time: 9.30 c [worker] round 19, time: 9.21 c [worker] round 19, time: 9.45 c [worker] round 20, time: 9.546 c [worker] round 20, time: 9.533 c [worker] round 20, time: 9.552 c [worker] round 20, time: 9.549 c [worker] round 20, time: 9.574 c [worker] round 20, time: 9.532 c [worker] round 20, time: 9.522 c [worker] round 20, time: 9.547 c [worker] round 21, time: 10.48 c [worker] round 21, time: 10.35 c [worker] round 21, time: 10.53 c [worker] round 21, time: 10.51 c [worker] round 21, time: 10.76 c [worker] round 21, time: 10.36 c [worker] round 21, time: 10.23 c [worker] round 21, time: 10.49 c [worker] round 22, time: 10.549 c [worker] round 22, time: 10.536 c [worker] round 22, time: 10.555 c [worker] round 22, time: 10.553 c [worker] round 22, time: 10.578 c [worker] round 22, time: 10.537 c [worker] round 22, time: 10.524 c [worker] round 22, time: 10.550 c [worker] round 23, time: 11.51 c [worker] round 23, time: 11.37 c [worker] round 23, time: 11.56 c [worker] round 23, time: 11.56 c [worker] round 23, time: 11.80 c [worker] round 23, time: 11.39 c [worker] round 23, time: 11.25 c [worker] round 23, time: 11.52 c [worker] round 24, time: 11.539 c [worker] round 24, time: 11.553 c [worker] round 24, time: 11.558 c [worker] round 24, time: 11.558 c [worker] round 24, time: 11.582 c [worker] round 24, time: 11.540 c [worker] round 24, time: 11.526 c [worker] round 24, time: 11.554 c [worker] round 25, time: 12.40 c [worker] round 25, time: 12.55 c [worker] round 25, time: 12.59 c [worker] round 25, time: 12.60 c [worker] round 25, time: 12.84 c [worker] round 25, time: 12.41 c [worker] round 25, time: 12.27 c [worker] round 25, time: 12.56 c [worker] round 26, time: 12.541 c [worker] round 26, time: 12.557 c [worker] round 26, time: 12.561 c [worker] round 26, time: 12.562 c [worker] round 26, time: 12.586 c [worker] round 26, time: 12.542 c [worker] round 26, time: 12.528 c [worker] round 26, time: 12.558 c [worker] round 27, time: 13.43 c [worker] round 27, time: 13.58 c [worker] round 27, time: 13.63 c [worker] round 27, time: 13.64 c [worker] round 27, time: 13.88 c [worker] round 27, time: 13.43 c [worker] round 27, time: 13.28 c [worker] round 27, time: 13.60 c [worker] round 28, time: 13.544 c [worker] round 28, time: 13.560 c [worker] round 28, time: 13.564 c [worker] round 28, time: 13.566 c [worker] round 28, time: 13.590 c [worker] round 28, time: 13.545 c [worker] round 28, time: 13.529 c [worker] round 28, time: 13.562 c [worker] round 29, time: 14.45 c [worker] round 29, time: 14.62 c [worker] round 29, time: 14.66 c [worker] round 29, time: 14.68 c [worker] round 29, time: 14.92 c [worker] round 29, time: 14.46 c [worker] round 29, time: 14.30 c [worker] round 29, time: 14.63 c [worker] round 30, time: 14.547 c [worker] round 30, time: 14.564 c [worker] round 30, time: 14.567 c [worker] round 30, time: 14.570 c [worker] round 30, time: 14.594 c [worker] round 30, time: 14.547 c [worker] round 30, time: 14.531 c [worker] round 30, time: 14.565 c [worker] round 31, time: 15.48 c [worker] round 31, time: 15.65 c [worker] round 31, time: 15.68 c [worker] round 31, time: 15.72 c [worker] round 31, time: 15.96 c [worker] round 31, time: 15.49 c [worker] round 31, time: 15.32 c [worker] round 31, time: 15.67 c [worker] round 32, time: 15.549 c [worker] round 32, time: 15.567 c [worker] round 32, time: 15.570 c [worker] round 32, time: 15.574 c [worker] round 32, time: 15.599 c [worker] round 32, time: 15.550 c [worker] round 32, time: 15.533 c [worker] round 32, time: 15.568 c [worker] round 33, time: 16.51 c [worker] round 33, time: 16.69 c [worker] round 33, time: 16.71 c [worker] round 33, time: 16.76 c [worker] round 33, time: 16.100 c [worker] round 33, time: 16.51 c [worker] round 33, time: 16.34 c [worker] round 33, time: 16.70 c [worker] round 34, time: 16.552 c [worker] round 34, time: 16.571 c [worker] round 34, time: 16.573 c [worker] round 34, time: 16.578 c [worker] round 34, time: 16.602 c [worker] round 34, time: 16.552 c [worker] round 34, time: 16.534 c [worker] round 34, time: 16.572 c [worker] round 35, time: 17.53 c [worker] round 35, time: 17.72 c [worker] round 35, time: 17.74 c [worker] round 35, time: 17.80 c [worker] round 35, time: 17.104 c [worker] round 35, time: 17.54 c [worker] round 35, time: 17.35 c [worker] round 35, time: 17.74 c [worker] round 36, time: 17.555 c [worker] round 36, time: 17.574 c [worker] round 36, time: 17.576 c [worker] round 36, time: 17.583 c [worker] round 36, time: 17.606 c [worker] round 36, time: 17.555 c [worker] round 36, time: 17.536 c [worker] round 36, time: 17.576 c [worker] round 37, time: 18.56 c [worker] round 37, time: 18.76 c [worker] round 37, time: 18.77 c [worker] round 37, time: 18.85 c [worker] round 37, time: 18.56 c [worker] round 37, time: 18.108 c [worker] round 37, time: 18.37 c [worker] round 37, time: 18.77 c [worker] round 38, time: 18.557 c [worker] round 38, time: 18.577 c [worker] round 38, time: 18.579 c [worker] round 38, time: 18.589 c [worker] round 38, time: 18.557 c [worker] round 38, time: 18.610 c [worker] round 38, time: 18.538 c [worker] round 38, time: 18.579 c [worker] round 39, time: 19.58 c [worker] round 39, time: 19.79 c [worker] round 39, time: 19.80 c [worker] round 39, time: 19.91 c [worker] round 39, time: 19.58 c [worker] round 39, time: 19.112 c [worker] round 39, time: 19.39 c [worker] round 39, time: 19.81 c [worker] round 40, time: 19.560 c [worker] round 40, time: 19.581 c [worker] round 40, time: 19.582 c [worker] round 40, time: 19.593 c [worker] round 40, time: 19.560 c [worker] round 40, time: 19.614 c [worker] round 40, time: 19.540 c [worker] round 40, time: 19.583 c [worker] round 41, time: 20.61 c [worker] round 41, time: 20.83 c [worker] round 41, time: 20.83 c [worker] round 41, time: 20.95 c [worker] round 41, time: 20.61 c [worker] round 41, time: 20.116 c [worker] round 41, time: 20.40 c [worker] round 41, time: 20.85 c [worker] round 42, time: 20.562 c [worker] round 42, time: 20.587 c [worker] round 42, time: 20.584 c [worker] round 42, time: 20.597 c [worker] round 42, time: 20.562 c [worker] round 42, time: 20.618 c [worker] round 42, time: 20.541 c [worker] round 42, time: 20.587 c [worker] round 43, time: 21.64 c [worker] round 43, time: 21.89 c [worker] round 43, time: 21.86 c [worker] round 43, time: 21.64 c [worker] round 43, time: 21.105 c [worker] round 43, time: 21.120 c [worker] round 43, time: 21.42 c [worker] round 43, time: 21.89 c [worker] round 44, time: 21.565 c [worker] round 44, time: 21.590 c [worker] round 44, time: 21.587 c [worker] round 44, time: 21.565 c [worker] round 44, time: 21.607 c [worker] round 44, time: 21.622 c [worker] round 44, time: 21.543 c [worker] round 44, time: 21.591 c [worker] round 45, time: 22.66 c [worker] round 45, time: 22.92 c [worker] round 45, time: 22.89 c [worker] round 45, time: 22.67 c [worker] round 45, time: 22.109 c [worker] round 45, time: 22.123 c [worker] round 45, time: 22.44 c [worker] round 45, time: 22.93 c [worker] round 46, time: 22.568 c [worker] round 46, time: 22.594 c [worker] round 46, time: 22.590 c [worker] round 46, time: 22.568 c [worker] round 46, time: 22.612 c [worker] round 46, time: 22.625 c [worker] round 46, time: 22.545 c [worker] round 46, time: 22.594 c [worker] round 47, time: 23.69 c [worker] round 47, time: 23.95 c [worker] round 47, time: 23.91 c [worker] round 47, time: 23.69 c [worker] round 47, time: 23.127 c [worker] round 47, time: 23.115 c [worker] round 47, time: 23.45 c [worker] round 47, time: 23.96 c [worker] round 48, time: 23.570 c [worker] round 48, time: 23.597 c [worker] round 48, time: 23.593 c [worker] round 48, time: 23.570 c [worker] round 48, time: 23.615 c [worker] round 48, time: 23.629 c [worker] round 48, time: 23.546 c [worker] round 48, time: 23.598 c [worker] round 49, time: 24.71 c [worker] round 49, time: 24.99 c [worker] round 49, time: 24.94 c [worker] round 49, time: 24.71 c [worker] round 49, time: 24.117 c [worker] round 49, time: 24.131 c [worker] round 49, time: 24.47 c [worker] round 49, time: 24.100 c [worker] round 50, time: 24.573 c [worker] round 50, time: 24.601 c [worker] round 50, time: 24.596 c [worker] round 50, time: 24.573 c [worker] round 50, time: 24.619 c [worker] round 50, time: 24.633 c [worker] round 50, time: 24.548 c [worker] round 50, time: 24.602 c [worker] round 51, time: 25.74 c [worker] round 51, time: 25.103 c [worker] round 51, time: 25.97 c [worker] round 51, time: 25.74 c [worker] round 51, time: 25.134 c [worker] round 51, time: 25.122 c [worker] round 51, time: 25.49 c [worker] round 51, time: 25.103 c [worker] round 52, time: 25.575 c [worker] round 52, time: 25.604 c [worker] round 52, time: 25.599 c [worker] round 52, time: 25.575 c [worker] round 52, time: 25.636 c [worker] round 52, time: 25.625 c [worker] round 52, time: 25.550 c [worker] round 52, time: 25.605 c [worker] round 53, time: 26.76 c [worker] round 53, time: 26.106 c [worker] round 53, time: 26.100 c [worker] round 53, time: 26.76 c [worker] round 53, time: 26.138 c [worker] round 53, time: 26.129 c [worker] round 53, time: 26.50 c [worker] round 53, time: 26.107 c [worker] round 54, time: 26.590 c [worker] round 54, time: 26.607 c [worker] round 54, time: 26.609 c [worker] round 54, time: 26.577 c [worker] round 54, time: 26.641 c [worker] round 54, time: 26.631 c [worker] round 54, time: 26.551 c [worker] round 54, time: 26.609 c [worker] round 55, time: 27.91 c [worker] round 55, time: 27.109 c [worker] round 55, time: 27.111 c [worker] round 55, time: 27.79 c [worker] round 55, time: 27.143 c [worker] round 55, time: 27.133 c [worker] round 55, time: 27.52 c [worker] round 55, time: 27.111 c [worker] round 56, time: 27.592 c [worker] round 56, time: 27.611 c [worker] round 56, time: 27.612 c [worker] round 56, time: 27.580 c [worker] round 56, time: 27.645 c [worker] round 56, time: 27.636 c [worker] round 56, time: 27.553 c [worker] round 56, time: 27.613 c [worker] round 57, time: 28.94 c [worker] round 57, time: 28.113 c [worker] round 57, time: 28.120 c [worker] round 57, time: 28.81 c [worker] round 57, time: 28.147 c [worker] round 57, time: 28.138 c [worker] round 57, time: 28.54 c [worker] round 57, time: 28.114 c [worker] round 58, time: 28.595 c [worker] round 58, time: 28.614 c [worker] round 58, time: 28.624 c [worker] round 58, time: 28.582 c [worker] round 58, time: 28.649 c [worker] round 58, time: 28.640 c [worker] round 58, time: 28.555 c [worker] round 58, time: 28.616 c [worker] round 59, time: 29.96 c [worker] round 59, time: 29.116 c [worker] round 59, time: 29.125 c [worker] round 59, time: 29.83 c [worker] round 59, time: 29.151 c [worker] round 59, time: 29.142 c [worker] round 59, time: 29.55 c [worker] round 59, time: 29.118 c [worker] round 60, time: 29.598 c [worker] round 60, time: 29.618 c [worker] round 60, time: 29.627 c [worker] round 60, time: 29.585 c [worker] round 60, time: 29.653 c [worker] round 60, time: 29.644 c [worker] round 60, time: 29.556 c [worker] round 60, time: 29.620 c [worker] round 61, time: 30.99 c [worker] round 61, time: 30.120 c [worker] round 61, time: 30.128 c [worker] round 61, time: 30.86 c [worker] round 61, time: 30.155 c [worker] round 61, time: 30.146 c [worker] round 61, time: 30.57 c [worker] round 61, time: 30.122 c [worker] round 62, time: 30.600 c [worker] round 62, time: 30.622 c [worker] round 62, time: 30.630 c [worker] round 62, time: 30.587 c [worker] round 62, time: 30.657 c [worker] round 62, time: 30.649 c [worker] round 62, time: 30.558 c [worker] round 62, time: 30.623 c [worker] round 63, time: 31.101 c [worker] round 63, time: 31.124 c [worker] round 63, time: 31.131 c [worker] round 63, time: 31.88 c [worker] round 63, time: 31.159 c [worker] round 63, time: 31.151 c [worker] round 63, time: 31.59 c [worker] round 63, time: 31.125 c [worker] round 64, time: 31.603 c [worker] round 64, time: 31.625 c [worker] round 64, time: 31.633 c [worker] round 64, time: 31.590 c [worker] round 64, time: 31.662 c [worker] round 64, time: 31.653 c [worker] round 64, time: 31.560 c [worker] round 64, time: 31.627 c [worker] round 65, time: 32.104 c [worker] round 65, time: 32.127 c [worker] round 65, time: 32.134 c [worker] round 65, time: 32.91 c [worker] round 65, time: 32.164 c [worker] round 65, time: 32.155 c [worker] round 65, time: 32.61 c [worker] round 65, time: 32.129 c [worker] round 66, time: 32.605 c [worker] round 66, time: 32.629 c [worker] round 66, time: 32.636 c [worker] round 66, time: 32.592 c [worker] round 66, time: 32.666 c [worker] round 66, time: 32.657 c [worker] round 66, time: 32.562 c [worker] round 66, time: 32.631 c [worker] round 67, time: 33.106 c [worker] round 67, time: 33.131 c [worker] round 67, time: 33.137 c [worker] round 67, time: 33.94 c [worker] round 67, time: 33.168 c [worker] round 67, time: 33.159 c [worker] round 67, time: 33.63 c [worker] round 67, time: 33.133 c [worker] round 68, time: 33.608 c [worker] round 68, time: 33.633 c [worker] round 68, time: 33.639 c [worker] round 68, time: 33.595 c [worker] round 68, time: 33.670 c [worker] round 68, time: 33.661 c [worker] round 68, time: 33.564 c [worker] round 68, time: 33.635 c [worker] round 69, time: 34.109 c [worker] round 69, time: 34.134 c [worker] round 69, time: 34.140 c [worker] round 69, time: 34.96 c [worker] round 69, time: 34.172 c [worker] round 69, time: 34.163 c [worker] round 69, time: 34.64 c [worker] round 69, time: 34.137 c [worker] round 70, time: 34.611 c [worker] round 70, time: 34.636 c [worker] round 70, time: 34.641 c [worker] round 70, time: 34.597 c [worker] round 70, time: 34.674 c [worker] round 70, time: 34.666 c [worker] round 70, time: 34.565 c [worker] round 70, time: 34.639 c [worker] round 71, time: 35.112 c [worker] round 71, time: 35.138 c [worker] round 71, time: 35.144 c [worker] round 71, time: 35.99 c [worker] round 71, time: 35.177 c [worker] round 71, time: 35.169 c [worker] round 71, time: 35.67 c [worker] round 71, time: 35.141 c [worker] round 72, time: 35.614 c [worker] round 72, time: 35.640 c [worker] round 72, time: 35.645 c [worker] round 72, time: 35.600 c [worker] round 72, time: 35.679 c [worker] round 72, time: 35.671 c [worker] round 72, time: 35.567 c [worker] round 72, time: 35.643 c [worker] round 73, time: 36.115 c [worker] round 73, time: 36.142 c [worker] round 73, time: 36.147 c [worker] round 73, time: 36.101 c [worker] round 73, time: 36.181 c [worker] round 73, time: 36.173 c [worker] round 73, time: 36.68 c [worker] round 73, time: 36.145 c [worker] round 74, time: 36.616 c [worker] round 74, time: 36.658 c [worker] round 74, time: 36.648 c [worker] round 74, time: 36.603 c [worker] round 74, time: 36.683 c [worker] round 74, time: 36.676 c [worker] round 74, time: 36.569 c [worker] round 74, time: 36.647 c [worker] round 75, time: 37.118 c [worker] round 75, time: 37.161 c [worker] round 75, time: 37.150 c [worker] round 75, time: 37.104 c [worker] round 75, time: 37.185 c [worker] round 75, time: 37.70 c [worker] round 75, time: 37.178 c [worker] round 75, time: 37.150 c [worker] round 76, time: 37.619 c [worker] round 76, time: 37.663 c [worker] round 76, time: 37.652 c [worker] round 76, time: 37.606 c [worker] round 76, time: 37.687 c [worker] round 76, time: 37.571 c [worker] round 76, time: 37.681 c sharing nums: 76 c sharing time: 0.14 c [worker8] kissat exit with result: 20 c [worker] round 76, time: 37.652 c sharing nums: 76 c sharing time: 0.10 c [worker5] kissat exit with result: 0 c [worker] round 77, time: 38.121 c sharing nums: 77 c sharing time: 0.09 c [worker3] kissat exit with result: 0 c [worker] round 77, time: 38.165 c sharing nums: 77 c sharing time: 0.11 c [worker6] kissat exit with result: 0 c [worker] round 77, time: 38.154 c sharing nums: 77 c sharing time: 0.11 c [worker] round 77, time: 38.107 c [worker4] kissat exit with result: 0 c sharing nums: 77 c sharing time: 0.08 c [worker2] kissat exit with result: 0 c [worker] round 77, time: 38.190 c [worker] round 77, time: 38.72 c sharing nums: 77 c sharing time: 0.14 c [worker7] kissat exit with result: 20 c sharing nums: 77 c sharing time: 0.01 c [worker1] kissat exit with result: 20 s UNSATISFIABLE real 39.53 user 4912.37 sys 16.87 mem 915920