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/7a236bb9e1566b80fa7b593a7e973efa-SCPC-500-16.cnf "" CNF format instance c -------------------------------------------------- c [leader] preprocess(simplify) input data c After preprocess: vars: 500 -> 500 , clauses: 15610 -> 15610 , c [CE] almost one cons: 5979 c sz 2 c turns: 1 c After preprocess: vars: 500 -> 500 , clauses: 15610 -> 15610 , 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.500 c [worker] round 2, time: 0.500 c [worker] round 2, time: 0.500 c [worker] round 2, time: 0.502 c [worker] round 2, time: 0.504 c [worker] round 2, time: 0.504 c [worker] round 2, time: 0.520 c [worker] round 2, time: 0.526 c [worker] round 3, time: 1.1 c [worker] round 3, time: 1.2 c [worker] round 3, time: 1.5 c [worker] round 3, time: 1.15 c [worker] round 3, time: 1.7 c [worker] round 3, time: 1.25 c [worker] round 3, time: 1.20 c [worker] round 3, time: 1.42 c [worker] round 4, time: 1.505 c [worker] round 4, time: 1.509 c [worker] round 4, time: 1.515 c [worker] round 4, time: 1.509 c [worker] round 4, time: 1.523 c [worker] round 4, time: 1.521 c [worker] round 4, time: 1.541 c [worker] round 4, time: 1.544 c [worker] round 5, time: 2.10 c [worker] round 5, time: 2.15 c [worker] round 5, time: 2.20 c [worker] round 5, time: 2.24 c [worker] round 5, time: 2.23 c [worker] round 5, time: 2.44 c [worker] round 5, time: 2.40 c [worker] round 5, time: 2.52 c [worker] round 6, time: 2.514 c [worker] round 6, time: 2.523 c [worker] round 6, time: 2.523 c [worker] round 6, time: 2.527 c [worker] round 6, time: 2.526 c [worker] round 6, time: 2.545 c [worker] round 6, time: 2.552 c [worker] round 6, time: 2.553 c [worker] round 7, time: 3.16 c [worker] round 7, time: 3.23 c [worker] round 7, time: 3.31 c [worker] round 7, time: 3.35 c [worker] round 7, time: 3.33 c [worker] round 7, time: 3.53 c [worker] round 7, time: 3.62 c [worker] round 7, time: 3.62 c [worker] round 8, time: 3.527 c [worker] round 8, time: 3.532 c [worker] round 8, time: 3.528 c [worker] round 8, time: 3.534 c [worker] round 8, time: 3.556 c [worker] round 8, time: 3.562 c [worker] round 8, time: 3.577 c [worker] round 8, time: 3.570 c [worker] round 9, time: 4.29 c [worker] round 9, time: 4.38 c [worker] round 9, time: 4.41 c [worker] round 9, time: 4.38 c [worker] round 9, time: 4.62 c [worker] round 9, time: 4.65 c [worker] round 9, time: 4.71 c [worker] round 9, time: 4.81 c [worker] round 10, time: 4.533 c [worker] round 10, time: 4.544 c [worker] round 10, time: 4.548 c [worker] round 10, time: 4.544 c [worker] round 10, time: 4.563 c [worker] round 10, time: 4.567 c [worker] round 10, time: 4.584 c [worker] round 10, time: 4.584 c [worker] round 11, time: 5.47 c [worker] round 11, time: 5.52 c [worker] round 11, time: 5.57 c [worker] round 11, time: 5.69 c [worker] round 11, time: 5.73 c [worker] round 11, time: 5.84 c [worker] round 11, time: 5.85 c [worker] round 11, time: 5.93 c [worker] round 12, time: 5.548 c [worker] round 12, time: 5.556 c [worker] round 12, time: 5.563 c [worker] round 12, time: 5.574 c [worker] round 12, time: 5.578 c [worker] round 12, time: 5.597 c [worker] round 12, time: 5.589 c [worker] round 12, time: 5.597 c [worker] round 13, time: 6.48 c [worker] round 13, time: 6.59 c [worker] round 13, time: 6.71 c [worker] round 13, time: 6.80 c [worker] round 13, time: 6.80 c [worker] round 13, time: 6.92 c [worker] round 13, time: 6.105 c [worker] round 13, time: 6.110 c [worker] round 14, time: 6.551 c [worker] round 14, time: 6.561 c [worker] round 14, time: 6.584 c [worker] round 14, time: 6.582 c [worker] round 14, time: 6.588 c [worker] round 14, time: 6.597 c [worker] round 14, time: 6.623 c [worker] round 14, time: 6.631 c [worker] round 15, time: 7.55 c [worker] round 15, time: 7.68 c [worker] round 15, time: 7.86 c [worker] round 15, time: 7.92 c [worker] round 15, time: 7.94 c [worker] round 15, time: 7.112 c [worker] round 15, time: 7.131 c [worker] round 15, time: 7.141 c [worker] round 16, time: 7.563 c [worker] round 16, time: 7.570 c [worker] round 16, time: 7.590 c [worker] round 16, time: 7.597 c [worker] round 16, time: 7.604 c [worker] round 16, time: 7.643 c [worker] round 16, time: 7.650 c [worker] round 16, time: 7.645 c [worker] round 17, time: 8.68 c [worker] round 17, time: 8.84 c [worker] round 17, time: 8.96 c [worker] round 17, time: 8.105 c [worker] round 17, time: 8.116 c [worker] round 17, time: 8.144 c [worker] round 17, time: 8.151 c [worker] round 17, time: 8.201 c [worker] round 18, time: 8.572 c [worker] round 18, time: 8.594 c [worker] round 18, time: 8.604 c [worker] round 18, time: 8.612 c [worker] round 18, time: 8.616 c [worker] round 18, time: 8.650 c [worker] round 18, time: 8.653 c [worker] round 18, time: 8.705 c [worker] round 19, time: 9.81 c [worker] round 19, time: 9.104 c [worker] round 19, time: 9.116 c [worker] round 19, time: 9.119 c [worker] round 19, time: 9.128 c [worker] round 19, time: 9.151 c [worker] round 19, time: 9.164 c [worker] round 19, time: 9.208 c [worker] round 20, time: 9.587 c [worker] round 20, time: 9.629 c [worker] round 20, time: 9.634 c [worker] round 20, time: 9.633 c [worker] round 20, time: 9.640 c [worker] round 20, time: 9.659 c [worker] round 20, time: 9.672 c [worker] round 20, time: 9.722 c [worker] round 21, time: 10.93 c [worker] round 21, time: 10.130 c [worker] round 21, time: 10.144 c [worker] round 21, time: 10.152 c [worker] round 21, time: 10.160 c [worker] round 21, time: 10.167 c [worker] round 21, time: 10.188 c [worker] round 21, time: 10.231 c [worker] round 22, time: 10.597 c [worker] round 22, time: 10.640 c [worker] round 22, time: 10.656 c [worker] round 22, time: 10.671 c [worker] round 22, time: 10.676 c [worker] round 22, time: 10.680 c sharing nums: 22 c sharing time: 0.16 c [worker7] kissat exit with result: 20 c sharing nums: 22 c sharing time: 0.16 c [worker4] kissat exit with result: 0 c [worker] round 22, time: 10.693 c sharing nums: 22 c sharing time: 0.17 c [worker2] kissat exit with result: 0 c sharing nums: 22 c sharing time: 0.17 c [worker5] kissat exit with result: 0 c [worker] round 22, time: 10.779 c sharing nums: 22 c sharing time: 0.26 c [worker8] kissat exit with result: 20 c [worker] round 23, time: 11.105 c sharing nums: 23 c sharing time: 0.08 c [worker1] kissat exit with result: 20 c [worker] round 23, time: 11.159 c [worker] round 23, time: 11.163 c sharing nums: 23 c sharing time: 0.14 c [worker6] kissat exit with result: 20 c sharing nums: 23 c sharing time: 0.15 c [worker3] kissat exit with result: 0 s UNSATISFIABLE real 12.15 user 1230.22 sys 20.73 mem 193760