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/3ff263696219ca9e301b0a1b345eb9aa-SCPC-500-4.cnf "" CNF format instance c -------------------------------------------------- c [leader] preprocess(simplify) input data c After preprocess: vars: 500 -> 500 , clauses: 15443 -> 15443 , c [CE] almost one cons: 5879 c sz 2 c turns: 1 c After preprocess: vars: 500 -> 500 , clauses: 15443 -> 15443 , 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.501 c [worker] round 2, time: 0.500 c [worker] round 2, time: 0.500 c [worker] round 2, time: 0.503 c [worker] round 2, time: 0.503 c [worker] round 2, time: 0.502 c [worker] round 3, time: 1.6 c [worker] round 3, time: 1.2 c [worker] round 3, time: 1.3 c [worker] round 3, time: 1.15 c [worker] round 3, time: 1.19 c [worker] round 3, time: 1.26 c [worker] round 3, time: 1.22 c [worker] round 3, time: 1.33 c [worker] round 4, time: 1.505 c [worker] round 4, time: 1.516 c [worker] round 4, time: 1.519 c [worker] round 4, time: 1.524 c [worker] round 4, time: 1.531 c [worker] round 4, time: 1.536 c [worker] round 4, time: 1.529 c [worker] round 4, time: 1.547 c [worker] round 5, time: 2.19 c [worker] round 5, time: 2.26 c [worker] round 5, time: 2.33 c [worker] round 5, time: 2.25 c [worker] round 5, time: 2.30 c [worker] round 5, time: 2.39 c [worker] round 5, time: 2.73 c [worker] round 5, time: 2.57 c [worker] round 6, time: 2.530 c [worker] round 6, time: 2.531 c [worker] round 6, time: 2.534 c [worker] round 6, time: 2.541 c [worker] round 6, time: 2.535 c [worker] round 6, time: 2.550 c [worker] round 6, time: 2.575 c [worker] round 6, time: 2.561 c [worker] round 7, time: 3.41 c [worker] round 7, time: 3.34 c [worker] round 7, time: 3.36 c [worker] round 7, time: 3.46 c [worker] round 7, time: 3.51 c [worker] round 7, time: 3.51 c [worker] round 7, time: 3.62 c [worker] round 7, time: 3.92 c [worker] round 8, time: 3.544 c [worker] round 8, time: 3.540 c [worker] round 8, time: 3.540 c [worker] round 8, time: 3.554 c [worker] round 8, time: 3.564 c [worker] round 8, time: 3.581 c [worker] round 8, time: 3.571 c [worker] round 8, time: 3.599 c [worker] round 9, time: 4.51 c [worker] round 9, time: 4.46 c [worker] round 9, time: 4.51 c [worker] round 9, time: 4.59 c [worker] round 9, time: 4.67 c [worker] round 9, time: 4.87 c [worker] round 9, time: 4.89 c [worker] round 9, time: 4.116 c [worker] round 10, time: 4.547 c [worker] round 10, time: 4.558 c [worker] round 10, time: 4.560 c [worker] round 10, time: 4.561 c [worker] round 10, time: 4.579 c [worker] round 10, time: 4.597 c [worker] round 10, time: 4.595 c [worker] round 10, time: 4.621 c [worker] round 11, time: 5.59 c [worker] round 11, time: 5.53 c [worker] round 11, time: 5.63 c [worker] round 11, time: 5.84 c [worker] round 11, time: 5.88 c [worker] round 11, time: 5.105 c [worker] round 11, time: 5.105 c [worker] round 11, time: 5.127 c [worker] round 12, time: 5.558 c [worker] round 12, time: 5.566 c [worker] round 12, time: 5.566 c [worker] round 12, time: 5.587 c [worker] round 12, time: 5.595 c [worker] round 12, time: 5.617 c [worker] round 12, time: 5.608 c [worker] round 12, time: 5.638 c [worker] round 13, time: 6.69 c [worker] round 13, time: 6.66 c [worker] round 13, time: 6.82 c [worker] round 13, time: 6.99 c [worker] round 13, time: 6.102 c [worker] round 13, time: 6.125 c [worker] round 13, time: 6.117 c [worker] round 13, time: 6.148 c [worker] round 14, time: 6.578 c [worker] round 14, time: 6.575 c [worker] round 14, time: 6.598 c [worker] round 14, time: 6.612 c [worker] round 14, time: 6.612 c [worker] round 14, time: 6.632 c [worker] round 14, time: 6.651 c [worker] round 14, time: 6.669 c [worker] round 15, time: 7.79 c [worker] round 15, time: 7.88 c [worker] round 15, time: 7.108 c sharing nums: 15 c sharing time: 0.09 c [worker1] kissat exit with result: 20 c sharing nums: 15 c sharing time: 0.10 c [worker6] kissat exit with result: 0 c [worker] round 15, time: 7.123 c [worker] round 15, time: 7.116 c sharing nums: 15 c sharing time: 0.10 c sharing nums: 15 c sharing time: 0.11 c [worker4] kissat exit with result: 0 c [worker7] kissat exit with result: 0 c [worker] round 15, time: 7.137 c sharing nums: 15 c sharing time: 0.12 c [worker3] kissat exit with result: 0 c [worker] round 15, time: 7.165 c sharing nums: 15 c sharing time: 0.15 c [worker5] kissat exit with result: 0 c [worker] round 15, time: 7.179 c sharing nums: 15 c sharing time: 0.17 c [worker8] kissat exit with result: 20 c [worker] round 16, time: 7.602 c sharing nums: 16 c sharing time: 0.09 c [worker2] kissat exit with result: 20 s UNSATISFIABLE real 8.58 user 835.17 sys 14.14 mem 180332