mpicxx -std=c++17 -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g -c src/sharer.cpp -o build/./src/sharer.cpp.o -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ -pthread -lz -lm -lboost_thread -lboost_date_time -lboost_system -Wl,-Bdynamic -lmpi_cxx -lmpi mpicxx -std=c++17 -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g build/./src/utils/parse.cpp.o build/./src/utils/hashmap.cpp.o build/./src/paras.cpp.o build/./src/main.cpp.o build/./src/preprocess/card.cpp.o build/./src/preprocess/preprocess.cpp.o build/./src/preprocess/resolution.cpp.o build/./src/preprocess/propagation.cpp.o build/./src/preprocess/gauss.cpp.o build/./src/preprocess/binary.cpp.o build/./src/solve.cpp.o build/./src/solver_api/basekissat.cpp.o build/./src/solver_api/basesolver.cpp.o build/./src/light.cpp.o build/./src/sharer.cpp.o -o light -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ -pthread -lz -lm -lboost_thread -lboost_date_time -lboost_system -Wl,-Bdynamic -lmpi_cxx -lmpi 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 share_method int 1 1 0 for Circle Propagate/ 1 for Tree Broadcast c shuffle int 1 1 Use random shuffle c simplify int 1 1 Use Simplify (only preprocess) c threads int 16 32 Thread number c times double 10.000000 5000 Cutoff time c unique int 1 1 Whether perform unique checking when receiving clauses from other nodes c config string "" Config file c instance string ./data/hard1.cnf "" CNF format instance c -------------------------------------------------- c [leader] preprocess(simplify) input data c [GE] XORs: 2484 (time: 0.00) c [GE] VAR SCC: 459 c [GE] XOR SCCs: 23 (time: 0.00) c [GE] unary xor: 0, bin xor: 0, bin added c After preprocess: vars: 5034 -> 5031 , clauses: 21066 -> 21062 , c [CE] almost one cons: 2550 c len 0 c sz 2 c turns: 2 c After preprocess: vars: 5031 -> 5024 , clauses: 21062 -> 21048 , 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 index:-1 number:-1 seed:-1 c index:0 number:16 seed:7 c index:10 number:16 seed:3 c index:14 number:16 seed:3 c index:0 number:16 seed:8 c index:2 number:16 seed:7 c index:-1 number:-1 seed:-1 c index:1 number:16 seed:1 c index:0 number:16 seed:1 c index:1 number:16 seed:8 c index:5 number:16 seed:8 c index:2 number:16 seed:5 c index:7 number:16 seed:5 c index:0 number:16 seed:5 c index:6 number:16 seed:7 c index:9 number:16 seed:5 c index:12 number:16 seed:7 c index:8 number:16 seed:7 c index:11 number:16 seed:7 c index:13 number:16 seed:7 c index:9 number:16 seed:7 c index:3 number:16 seed:1 c index:15 number:16 seed:8 c index:9 number:16 seed:8 c index:6 number:16 seed:1 c index:7 number:16 seed:1 c index:4 number:16 seed:8 c index:13 number:16 seed:8 c index:8 number:16 seed:8 c index:1 number:16 seed:4 c index:14 number:16 seed:1 c index:10 number:16 seed:8 c index:6 number:16 seed:8 c index:2 number:16 seed:8 c index:-1 number:-1 seed:-1 c index:-1 number:-1 seed:-1 c index:13 number:16 seed:1 c index:4 number:16 seed:4 c index:6 number:16 seed:4 c index:9 number:16 seed:1 c index:7 number:16 seed:4 c index:3 number:16 seed:4 c index:11 number:16 seed:4 c index:10 number:16 seed:4 c index:2 number:16 seed:4 c index:15 number:16 seed:1 c index:11 number:16 seed:8 c index:3 number:16 seed:8 c index:0 number:16 seed:4 c index:1 number:16 seed:5 c index:3 number:16 seed:7 c index:-1 number:-1 seed:-1 c index:15 number:16 seed:4 c index:12 number:16 seed:4 c index:14 number:16 seed:4 c index:5 number:16 seed:5 c index:3 number:16 seed:5 c index:5 number:16 seed:1 c index:5 number:16 seed:7 c index:4 number:16 seed:7 c index:7 number:16 seed:7 c index:7 number:16 seed:8 c index:2 number:16 seed:1 c index:11 number:16 seed:1 c index:9 number:16 seed:6 c index:11 number:16 seed:5 c index:6 number:16 seed:6 c index:15 number:16 seed:6 c index:12 number:16 seed:6 c index:12 number:16 seed:8 c index:10 number:16 seed:1 c index:-1 number:-1 seed:-1 c index:14 number:16 seed:8 c index:1 number:16 seed:7 c index:12 number:16 seed:1 c index:6 number:16 seed:5 c index:3 number:16 seed:3 c index:0 number:16 seed:3 c index:5 number:16 seed:3 c index:15 number:16 seed:5 c index:1 number:16 seed:6 c index:3 number:16 seed:6 c index:7 number:16 seed:6 c index:8 number:16 seed:1 c index:10 number:16 seed:7 c index:7 number:16 seed:3 c index:-1 number:-1 seed:-1 c index:8 number:16 seed:4 c index:15 number:16 seed:7 c index:4 number:16 seed:1 c index:5 number:16 seed:4 c index:9 number:16 seed:4 c index:5 number:16 seed:6 c index:10 number:16 seed:6 c index:-1 number:-1 seed:-1 c index:-1 number:-1 seed:-1 c index:-1 number:-1 seed:-1 c index:8 number:16 seed:5 c index:13 number:16 seed:5 c index:0 number:16 seed:6 c index:4 number:16 seed:5 c index:2 number:16 seed:6 c index:-1 number:-1 seed:-1 c index:8 number:16 seed:6 c index:2 number:16 seed:3 c index:14 number:16 seed:7 c index:13 number:16 seed:4 c index:14 number:16 seed:5 c index:4 number:16 seed:3 c index:1 number:16 seed:3 c index:12 number:16 seed:3 c index:13 number:16 seed:3 c index:9 number:16 seed:3 c index:4 number:16 seed:6 c index:13 number:16 seed:6 ==============run1============ c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] c =========build tree========= c son[1][1][0]=-1 son[1][1][1]=-1 c son[2][2][0]=-1 son[2][2][1]=-1 c son[3][3][0]=6 son[3][3][1]=8 c son[3][6][0]=4 son[3][6][1]=5 c son[3][8][0]=7 son[3][8][1]=-1 c son[3][4][0]=-1 son[3][4][1]=-1 c son[3][5][0]=-1 son[3][5][1]=-1 c son[3][7][0]=-1 son[3][7][1]=-1 c son[4][4][0]=7 son[4][4][1]=3 c son[4][7][0]=8 son[4][7][1]=5 c son[4][3][0]=6 son[4][3][1]=-1 c son[4][8][0]=-1 son[4][8][1]=-1 c son[4][5][0]=-1 son[4][5][1]=-1 c son[4][6][0]=-1 son[4][6][1]=-1 c son[5][5][0]=4 son[5][5][1]=6 c son[5][4][0]=7 son[5][4][1]=8 c son[5][6][0]=3 son[5][6][1]=-1 c son[5][7][0]=-1 son[5][7][1]=-1 c son[5][8][0]=-1 son[5][8][1]=-1 c son[5][3][0]=-1 son[5][3][1]=-1 c son[6][6][0]=8 son[6][6][1]=7 c son[6][8][0]=5 son[6][8][1]=3 c son[6][7][0]=4 son[6][7][1]=-1 c son[6][5][0]=-1 son[6][5][1]=-1 c son[6][3][0]=-1 son[6][3][1]=-1 c son[6][4][0]=-1 son[6][4][1]=-1 c son[7][7][0]=8c index:-1 number:-1 seed:-1 son[7][7][1]=4 c son[7][8][0]=6 son[7][8][1]=3 c son[7][4][0]=5 son[7][4][1]=-1 c son[7][6][0]=-1 son[7][6][1]=-1 c son[7][3][0]=-1 son[7][3][1]=-1 c son[7][5][0]=-1c index:-1 number:-1 seed:-1 son[7][5][1]=-1 c son[8][8][0]=7 son[8][8][1]=4 c son[8][7][0]=6 son[8][7][1]=5 c son[8][4][0]=3 son[8][4][1]=-1 c son[8][6][0]=-1 son[8][6][1]=-1 c son[8][5][0]=-1 son[8][5][1]=-1 c son[8][3][0]=-1 son[8][3][1]=-1 ==============run2============ c index:6 number:16 seed:3 c index:8 number:16 seed:3 c index:15 number:16 seed:3 c index:11 number:16 seed:3 ==============run1============ c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] c =========build tree========= c son[1][1][0]=-1 son[1][1][1]=-1 c son[2][2][0]=-1 son[2][2][1]=-1 c son[3][3][0]=6 son[3][3][1]=8 c son[3][6][0]=4 son[3][6][1]=5 c son[3][8][0]=7 son[3][8][1]=-1 c son[3][4][0]=-1 son[3][4][1]=-1 c index:12 number:16 seed:5 c son[3][5][0]=-1 son[3][5][1]=-1 c son[3][7][0]=-1 son[3][7][1]=-1 c son[4][4][0]=7 son[4][4][1]=3 c son[4][7][0]=8 son[4][7][1]=5 c son[4][3][0]=6 son[4][3][1]=-1 c son[4][8][0]=-1 son[4][8][1]=-1 c son[4][5][0]=-1 son[4][5][1]=-1 c son[4][6][0]=-1 son[4][6][1]=-1 c son[5][5][0]=4 son[5][5][1]=6 c son[5][4][0]=7 son[5][4][1]=8 c son[5][6][0]=3 son[5][6][1]=-1 c son[5][7][0]=-1 son[5][7][1]=-1 c son[5][8][0]=-1 son[5][8][1]=-1 c son[5][3][0]=-1 son[5][3][1]=-1 c son[6][6][0]=8 son[6][6][1]=7 c son[6][8][0]=5 son[6][8][1]=3 c son[6][7][0]=4 son[6][7][1]=-1 c son[6][5][0]=-1 son[6][5][1]=-1 c son[6][3][0]=-1 son[6][3][1]=-1 c son[6][4][0]=-1 son[6][4][1]=-1 c son[7][7][0]=8 son[7][7][1]=4 c son[7][8][0]=6 son[7][8][1]=3 c son[7][4][0]=5 son[7][4][1]=-1 c son[7][6][0]=-1 son[7][6][1]=-1 c son[7][3][0]=-1 son[7][3][1]=-1 c son[7][5][0]=-1 son[7][5][1]=-1 c son[8][8][0]=7 son[8][8][1]=4 c son[8][7][0]=6 son[8][7][1]=5 c son[8][4][0]=3 son[8][4][1]=-1 c son[8][6][0]=-1 son[8][6][1]=-1 c son[8][5][0]=-1 son[8][5][1]=-1 c son[8][3][0]=-1 son[8][3][1]=-1 ==============run2============ ==============run1============ c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] c =========build tree========= c son[1][1][0]=-1 son[1][1][1]=-1 c son[2][2][0]=-1 son[2][2][1]=-1 c son[3][3][0]=6 son[3][3][1]=8 c son[3][6][0]=4 son[3][6][1]=5 c son[3][8][0]=7 son[3][8][1]=-1 c son[3][4][0]=-1 son[3][4][1]=-1 c son[3][5][0]=-1 son[3][5][1]=-1 c son[3][7][0]=-1 son[3][7][1]=-1 c son[4][4][0]=7 son[4][4][1]=3 c son[4][7][0]=8 son[4][7][1]=5 c son[4][3][0]=6 son[4][3][1]=-1 c son[4][8][0]=-1 son[4][8][1]=-1 c son[4][5][0]=-1 son[4][5][1]=-1 c son[4][6][0]=-1 son[4][6][1]=-1 c son[5][5][0]=4 son[5][5][1]=6 c son[5][4][0]=7 son[5][4][1]=8 c son[5][6][0]=3 son[5][6][1]=-1 c son[5][7][0]=-1 son[5][7][1]=-1 c son[5][8][0]=-1 son[5][8][1]=-1 c son[5][3][0]=-1 son[5][3][1]=-1 c son[6][6][0]=8 son[6][6][1]=7 c son[6][8][0]=5 son[6][8][1]=3 c son[6][7][0]=4 son[6][7][1]=-1 c son[6][5][0]=-1 son[6][5][1]=-1 c son[6][3][0]=-1 son[6][3][1]=-1 c son[6][4][0]=-1 son[6][4][1]=-1 c son[7][7][0]=8 son[7][7][1]=4 c son[7][8][0]=6 son[7][8][1]=3 c son[7][4][0]=5 son[7][4][1]=-1 c son[7][6][0]=-1 son[7][6][1]=-1 c son[7][3][0]=-1 son[7][3][1]=-1 c son[7][5][0]=-1 son[7][5][1]=-1 c son[8][8][0]=7 son[8][8][1]=4 c son[8][7][0]=6 son[8][7][1]=5 c son[8][4][0]=3 son[8][4][1]=-1 c son[8][6][0]=-1 son[8][6][1]=-1 c son[8][5][0]=-1 son[8][5][1]=-1 c son[8][3][0]=-1 son[8][3][1]=-1 ==============run2============ c index:10 number:16 seed:5 c index:11 number:16 seed:6 c index:14 number:16 seed:6 ==============run1============ c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] c =========build tree========= c son[1][1][0]=-1 son[1][1][1]=-1 c son[2][2][0]=-1 son[2][2][1]=-1 c son[3][3][0]=6 son[3][3][1]=8 c son[3][6][0]=4 son[3][6][1]=5 c son[3][8][0]=7 son[3][8][1]=-1 c son[3][4][0]=-1 son[3][4][1]=-1 c son[3][5][0]=-1 son[3][5][1]=-1 c son[3][7][0]=-1 son[3][7][1]=-1 c son[4][4][0]=7 son[4][4][1]=3 c son[4][7][0]=8 son[4][7][1]=5 c son[4][3][0]=6 son[4][3][1]=-1 c son[4][8][0]=-1 son[4][8][1]=-1 c son[4][5][0]=-1 son[4][5][1]=-1 c son[4][6][0]=-1 son[4][6][1]=-1 c son[5][5][0]=4 son[5][5][1]=6 c son[5][4][0]=7 son[5][4][1]=8 c son[5][6][0]=3 son[5][6][1]=-1 c son[5][7][0]=-1 son[5][7][1]=-1 c son[5][8][0]=-1 son[5][8][1]=-1 c son[5][3][0]=-1 son[5][3][1]=-1 c son[6][6][0]=8 son[6][6][1]=7 c son[6][8][0]=5 son[6][8][1]=3 c son[6][7][0]=4 son[6][7][1]=-1 c son[6][5][0]=-1 son[6][5][1]=-1 c son[6][3][0]=-1 son[6][3][1]=-1 c son[6][4][0]=-1 son[6][4][1]=-1 c son[7][7][0]=8 son[7][7][1]=4 c son[7][8][0]=6 son[7][8][1]=3 c son[7][4][0]=5 son[7][4][1]=-1 c son[7][6][0]=-1 son[7][6][1]=-1 c son[7][3][0]=-1 son[7][3][1]=-1 c son[7][5][0]=-1 son[7][5][1]=-1 c son[8][8][0]=7 son[8][8][1]=4 c son[8][7][0]=6 son[8][7][1]=5 c son[8][4][0]=3 son[8][4][1]=-1 c son[8][6][0]=-1 son[8][6][1]=-1 c son[8][5][0]=-1 son[8][5][1]=-1 c son[8][3][0]=-1 son[8][3][1]=-1 ==============run2============ c index:-1 number:-1 seed:-1 c index:-1 number:-1 seed:-1 c index:-1 number:-1 seed:-1 ==============run1============ c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] c =========build tree========= c son[1][1][0]=-1 son[1][1][1]=-1 c son[2][2][0]=-1 son[2][2][1]=-1 c son[3][3][0]=6 son[3][3][1]=8 c son[3][6][0]=4 son[3][6][1]=5 c son[3][8][0]=7 son[3][8][1]=-1 c son[3][4][0]=-1 son[3][4][1]=-1 c son[3][5][0]=-1 son[3][5][1]=-1 c son[3][7][0]=-1 son[3][7][1]=-1 c son[4][4][0]=7 son[4][4][1]=3 c son[4][7][0]=8 son[4][7][1]=5 c son[4][3][0]=6 son[4][3][1]=-1 c son[4][8][0]=-1 son[4][8][1]=-1 c son[4][5][0]=-1 son[4][5][1]=-1 c son[4][6][0]=-1 son[4][6][1]=-1 c son[5][5][0]=4 son[5][5][1]=6 c son[5][4][0]=7 son[5][4][1]=8 c son[5][6][0]=3 son[5][6][1]=-1 c son[5][7][0]=-1 son[5][7][1]=-1 c son[5][8][0]=-1 son[5][8][1]=-1 c son[5][3][0]=-1 son[5][3][1]=-1 c son[6][6][0]=8 son[6][6][1]=7 c son[6][8][0]=5 son[6][8][1]=3 c son[6][7][0]=4 son[6][7][1]=-1 c son[6][5][0]=-1 son[6][5][1]=-1 c son[6][3][0]=-1 son[6][3][1]=-1 c son[6][4][0]=-1 son[6][4][1]=-1 c son[7][7][0]=8 son[7][7][1]=4 c son[7][8][0]=6 son[7][8][1]=3 c son[7][4][0]=5 son[7][4][1]=-1 c son[7][6][0]=-1 son[7][6][1]=-1 c son[7][3][0]=-1 son[7][3][1]=-1 c son[7][5][0]=-1 son[7][5][1]=-1 c son[8][8][0]=7 son[8][8][1]=4 c son[8][7][0]=6 son[8][7][1]=5 c son[8][4][0]=3 son[8][4][1]=-1 c son[8][6][0]=-1 son[8][6][1]=-1 c son[8][5][0]=-1 son[8][5][1]=-1 c son[8][3][0]=-1 son[8][3][1]=-1 ==============run2============ ==============run1============ c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] c =========build tree========= c son[1][1][0]=-1 son[1][1][1]=-1 c son[2][2][0]=-1 son[2][2][1]=-1 c son[3][3][0]=6 son[3][3][1]=8 c son[3][6][0]=4 son[3][6][1]=5 c son[3][8][0]=7 son[3][8][1]=-1 c son[3][4][0]=-1 son[3][4][1]=-1 c son[3][5][0]=-1 son[3][5][1]=-1 c son[3][7][0]=-1 son[3][7][1]=-1 c son[4][4][0]=7 son[4][4][1]=3 c son[4][7][0]=8 son[4][7][1]=5 c son[4][3][0]=6 son[4][3][1]=-1 c son[4][8][0]=-1 son[4][8][1]=-1 c son[4][5][0]=-1 son[4][5][1]=-1 c son[4][6][0]=-1 son[4][6][1]=-1 c son[5][5][0]=4 son[5][5][1]=6 c son[5][4][0]=7 son[5][4][1]=8 c son[5][6][0]=3 son[5][6][1]=-1 c son[5][7][0]=-1 son[5][7][1]=-1 c son[5][8][0]=-1 son[5][8][1]=-1 c son[5][3][0]=-1 son[5][3][1]=-1 c son[6][6][0]=8 son[6][6][1]=7 c son[6][8][0]=5 son[6][8][1]=3 c son[6][7][0]=4 son[6][7][1]=-1 c son[6][5][0]=-1 son[6][5][1]=-1 c son[6][3][0]=-1 son[6][3][1]=-1 c son[6][4][0]=-1 son[6][4][1]=-1 c son[7][7][0]=8 son[7][7][1]=4 c son[7][8][0]=6 son[7][8][1]=3 c son[7][4][0]=5 son[7][4][1]=-1 c son[7][6][0]=-1 son[7][6][1]=-1 c son[7][3][0]=-1 son[7][3][1]=-1 c son[7][5][0]=-1 son[7][5][1]=-1 c son[8][8][0]=7 son[8][8][1]=4 c son[8][7][0]=6 son[8][7][1]=5 c son[8][4][0]=3 son[8][4][1]=-1 c son[8][6][0]=-1 son[8][6][1]=-1 c son[8][5][0]=-1 son[8][5][1]=-1 c son[8][3][0]=-1 son[8][3][1]=-1 ==============run2============ ==============run1============ c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] c =========build tree========= c son[1][1][0]=-1 son[1][1][1]=-1 c son[2][2][0]=-1 son[2][2][1]=-1 c son[3][3][0]=6 son[3][3][1]=8 c son[3][6][0]=4 son[3][6][1]=5 c son[3][8][0]=7 son[3][8][1]=-1 c son[3][4][0]=-1 son[3][4][1]=-1 c son[3][5][0]=-1 son[3][5][1]=-1 c son[3][7][0]=-1 son[3][7][1]=-1 c son[4][4][0]=7 son[4][4][1]=3 c son[4][7][0]=8 son[4][7][1]=5 c son[4][3][0]=6 son[4][3][1]=-1 c son[4][8][0]=-1 son[4][8][1]=-1 c son[4][5][0]=-1 son[4][5][1]=-1 c son[4][6][0]=-1 son[4][6][1]=-1 c son[5][5][0]=4 son[5][5][1]=6 c son[5][4][0]=7 son[5][4][1]=8 c son[5][6][0]=3 son[5][6][1]=-1 c son[5][7][0]=-1 son[5][7][1]=-1 c son[5][8][0]=-1 son[5][8][1]=-1 c son[5][3][0]=-1 son[5][3][1]=-1 c son[6][6][0]=8 son[6][6][1]=7 c son[6][8][0]=5 son[6][8][1]=3 c son[6][7][0]=4 son[6][7][1]=-1 c son[6][5][0]=-1 son[6][5][1]=-1 c son[6][3][0]=-1 son[6][3][1]=-1 c son[6][4][0]=-1 son[6][4][1]=-1 c son[7][7][0]=8 son[7][7][1]=4 c son[7][8][0]=6 son[7][8][1]=3 c son[7][4][0]=5 son[7][4][1]=-1 c son[7][6][0]=-1 son[7][6][1]=-1 c son[7][3][0]=-1 son[7][3][1]=-1 c son[7][5][0]=-1 son[7][5][1]=-1 c son[8][8][0]=7 son[8][8][1]=4 c son[8][7][0]=6 son[8][7][1]=5 c son[8][4][0]=3 son[8][4][1]=-1 c son[8][6][0]=-1 son[8][6][1]=-1 c son[8][5][0]=-1 son[8][5][1]=-1 c son[8][3][0]=-1 son[8][3][1]=-1 ==============run2============ ==============run1============ c sharing groups: [ 1 ] [ 2 ] [ 3 4 5 6 7 8 ] c =========build tree========= c son[1][1][0]=-1 son[1][1][1]=-1 c son[2][2][0]=-1 son[2][2][1]=-1 c son[3][3][0]=6 son[3][3][1]=8 c son[3][6][0]=4 son[3][6][1]=5 c son[3][8][0]=7 son[3][8][1]=-1 c son[3][4][0]=-1 son[3][4][1]=-1 c son[3][5][0]=-1 son[3][5][1]=-1 c son[3][7][0]=-1 son[3][7][1]=-1 c son[4][4][0]=7 son[4][4][1]=3 c son[4][7][0]=8 son[4][7][1]=5 c son[4][3][0]=6 son[4][3][1]=-1 c son[4][8][0]=-1 son[4][8][1]=-1 c son[4][5][0]=-1 son[4][5][1]=-1 c son[4][6][0]=-1 son[4][6][1]=-1 c son[5][5][0]=4 son[5][5][1]=6 c son[5][4][0]=7 son[5][4][1]=8 c son[5][6][0]=3 son[5][6][1]=-1 c son[5][7][0]=-1 son[5][7][1]=-1 c son[5][8][0]=-1 son[5][8][1]=-1 c son[5][3][0]=-1 son[5][3][1]=-1 c son[6][6][0]=8 son[6][6][1]=7 c son[6][8][0]=5 son[6][8][1]=3 c son[6][7][0]=4 son[6][7][1]=-1 c son[6][5][0]=-1 son[6][5][1]=-1 c son[6][3][0]=-1 son[6][3][1]=-1 c son[6][4][0]=-1 son[6][4][1]=-1 c son[7][7][0]=8 son[7][7][1]=4 c son[7][8][0]=6 son[7][8][1]=3 c son[7][4][0]=5 son[7][4][1]=-1 c son[7][6][0]=-1 son[7][6][1]=-1 c son[7][3][0]=-1 son[7][3][1]=-1 c son[7][5][0]=-1 son[7][5][1]=-1 c son[8][8][0]=7 son[8][8][1]=4 c son[8][7][0]=6 son[8][7][1]=5 c son[8][4][0]=3 son[8][4][1]=-1 c son[8][6][0]=-1 son[8][6][1]=-1 c son[8][5][0]=-1 son[8][5][1]=-1 c son[8][3][0]=-1 son[8][3][1]=-1 ==============run2============ c node8(2)round 1, time: 0.0 c node8(2) get 0 exported lits from network c node1(0)round 1, time: 0.0 c node1(0) get 0 exported lits from network c node7(2)round 1, time: 0.0 c node4(2)round 1, time: 0.0 c node5(2)round 1, time: 0.0 c node3(2)round 1, time: 0.0 c node2(1)round 1, time: 0.0 c node2(1) get 0 exported lits from network c node7(2) get 61475 exported lits from network c node3(2) get 57542 exported lits from network c node5(2) get 70894 exported lits from network c node6(2)round 1, time: 0.0 c node4(2) get 169407 exported lits from network c node6(2) get 146781 exported lits from network c node1(0)round 2, time: 0.505 c node1(0) get 0 exported lits from network c node8(2)round 2, time: 0.507 c node2(1)round 2, time: 0.508 c node2(1) get 0 exported lits from network c node7(2)round 2, time: 0.522 c node5(2)round 2, time: 0.520 c node5(2) get 96220 exported lits from network c node3(2)round 2, time: 0.539 c node8(2) get 158779 exported lits from network c node7(2) get 180201 exported lits from network c node4(2)round 2, time: 0.570 c node3(2) get 167960 exported lits from network c node6(2)round 2, time: 0.568 c node4(2) get 147417 exported lits from network c node6(2) get 169923 exported lits from network c node1(0)round 3, time: 1.10 c node1(0) get 0 exported lits from network c node2(1)round 3, time: 1.25 c node2(1) get 0 exported lits from network c node5(2)round 3, time: 1.58 c node8(2)round 3, time: 1.68 c node7(2)round 3, time: 1.90 c node5(2) get 151592 exported lits from network c node3(2)round 3, time: 1.96 c node8(2) get 160986 exported lits from network c node4(2)round 3, time: 1.123 c node7(2) get 132887 exported lits from network c node3(2) get 146068 exported lits from network c node6(2)round 3, time: 1.124 c node4(2) get 121030 exported lits from network c node6(2) get 121107 exported lits from network c node1(0)round 4, time: 1.516 c node1(0) get 0 exported lits from network c node2(1)round 4, time: 1.531 c node2(1) get 0 exported lits from network c node5(2)round 4, time: 1.600 c node8(2)round 4, time: 1.626 c node7(2)round 4, time: 1.632 c node5(2) get 96047 exported lits from network c node3(2)round 4, time: 1.640 c node7(2) get 92408 exported lits from network c node8(2) get 135708 exported lits from network c node3(2) get 113665 exported lits from network c node4(2)round 4, time: 1.694 c node4(2) get 75871 exported lits from network c node6(2)round 4, time: 1.696 c node6(2) get 78695 exported lits from network c node1(0)round 5, time: 2.19 c node1(0) get 0 exported lits from network c node2(1)round 5, time: 2.38 c node2(1) get 0 exported lits from network c node5(2)round 5, time: 2.133 c node5(2) get 63142 exported lits from network c node7(2)round 5, time: 2.168 c node7(2) get 51839 exported lits from network c node8(2)round 5, time: 2.178 c node3(2)round 5, time: 2.174 c node8(2) get 62574 exported lits from network c node3(2) get 61814 exported lits from network c node4(2)round 5, time: 2.217 c node4(2) get 63967 exported lits from network c node6(2)round 5, time: 2.223 c node6(2) get 65534 exported lits from network c node1(0)round 6, time: 2.523 c node1(0) get 0 exported lits from network c node2(1)round 6, time: 2.544 c node2(1) get 0 exported lits from network c node5(2)round 6, time: 2.647 c node5(2) get 65327 exported lits from network c node7(2)round 6, time: 2.679 c node7(2) get 61918 exported lits from network c node8(2)round 6, time: 2.710 c node3(2)round 6, time: 2.711 c node3(2) get 61493 exported lits from network c node8(2) get 68462 exported lits from network c node4(2)round 6, time: 2.736 c node4(2) get 65870 exported lits from network c node6(2)round 6, time: 2.738 c node6(2) get 67926 exported lits from network c node1(0)round 7, time: 3.26 c node1(0) get 0 exported lits from network c node2(1)round 7, time: 3.48 c node2(1) get 0 exported lits from network c node5(2)round 7, time: 3.174 c node5(2) get 60817 exported lits from network c node7(2)round 7, time: 3.201 c node7(2) get 67941 exported lits from network c node8(2)round 7, time: 3.241 c node3(2)round 7, time: 3.235 c node4(2)round 7, time: 3.254 c node3(2) get 52426 exported lits from network c node4(2) get 56851 exported lits from network c node8(2) get 102288 exported lits from network c node6(2)round 7, time: 3.272 c node6(2) get 72854 exported lits from network c node1(0)round 8, time: 3.528 c node1(0) get 0 exported lits from network c node2(1)round 8, time: 3.553 c node2(1) get 0 exported lits from network c node5(2)round 8, time: 3.707 c node7(2)round 8, time: 3.717 c node7(2) get 94910 exported lits from network c node5(2) get 103849 exported lits from network c node3(2)round 8, time: 3.760 c node3(2) get 53356 exported lits from network c node4(2)round 8, time: 3.786 c node8(2)round 8, time: 3.797 c node8(2) get 79186 exported lits from network c node4(2) get 90767 exported lits from network c node6(2)round 8, time: 3.800 c node6(2) get 80368 exported lits from network c node1(0)round 9, time: 4.31 c node1(0) get 0 exported lits from network c node2(1)round 9, time: 4.57 c node2(1) get 0 exported lits from network c node7(2)round 9, time: 4.254 c node5(2)round 9, time: 4.248 c node7(2) get 71819 exported lits from network c node5(2) get 77702 exported lits from network c node3(2)round 9, time: 4.302 c node8(2)round 9, time: 4.319 c node4(2)round 9, time: 4.326 c node8(2) get 51759 exported lits from network c node4(2) get 59968 exported lits from network c node6(2)round 9, time: 4.320 c node3(2) get 145316 exported lits from network c node6(2) get 75791 exported lits from network c node1(0)round 10, time: 4.533 c node1(0) get 0 exported lits from network c node2(1)round 10, time: 4.561 c node2(1) get 0 exported lits from network c node7(2)round 10, time: 4.775 c node5(2)round 10, time: 4.769 c node7(2) get 45341 exported lits from network c node5(2) get 64543 exported lits from network c node8(2)round 10, time: 4.842 c node4(2)round 10, time: 4.844 c node8(2) get 53761 exported lits from network c node4(2) get 55729 exported lits from network c node3(2)round 10, time: 4.862 c node6(2)round 10, time: 4.838 c node6(2) get 36639 exported lits from network c node3(2) get 63265 exported lits from network c node1(0)round 11, time: 5.36 c node1(0) get 0 exported lits from network c node2(1)round 11, time: 5.65 c node2(1) get 0 exported lits from network c node7(2)round 11, time: 5.287 c node5(2)round 11, time: 5.282 c node7(2) get 52782 exported lits from network c node5(2) get 46506 exported lits from network c node8(2)round 11, time: 5.353 c node4(2)round 11, time: 5.357 c node8(2) get 50676 exported lits from network c node4(2) get 31544 exported lits from network c node6(2)round 11, time: 5.345 c node6(2) get 42762 exported lits from network c node3(2)round 11, time: 5.387 c node3(2) get 40729 exported lits from network c node1(0)round 12, time: 5.540 c node1(0) get 0 exported lits from network c node2(1)round 12, time: 5.569 c node2(1) get 0 exported lits from network c node7(2)round 12, time: 5.798 c node5(2)round 12, time: 5.793 c node7(2) get 45529 exported lits from network c node5(2) get 44821 exported lits from network c node8(2)round 12, time: 5.866 c node4(2)round 12, time: 5.866 c node6(2)round 12, time: 5.855 c node3(2)round 12, time: 5.897 c node8(2) get 50559 exported lits from network c node3(2) get 28134 exported lits from network c node4(2) get 44377 exported lits from network c node6(2) get 49071 exported lits from network c node1(0)round 13, time: 6.42 c node1(0) get 0 exported lits from network c node2(1)round 13, time: 6.72 c node2(1) get 0 exported lits from network c node7(2)round 13, time: 6.308 c node5(2)round 13, time: 6.305 c node7(2) get 44523 exported lits from network c node5(2) get 50818 exported lits from network c node3(2)round 13, time: 6.418 c node4(2)round 13, time: 6.425 c node8(2)round 13, time: 6.433 c node3(2) get 14873 exported lits from network c node4(2) get 45590 exported lits from network c node8(2) get 55860 exported lits from network c node6(2)round 13, time: 6.423 c node6(2) get 46575 exported lits from network c node1(0)round 14, time: 6.545 c node1(0) get 0 exported lits from network c node2(1)round 14, time: 6.575 c node2(1) get 0 exported lits from network c node7(2)round 14, time: 6.833 c node7(2) get 58604 exported lits from network c node5(2)round 14, time: 6.877 c node5(2) get 49441 exported lits from network c node3(2)round 14, time: 6.924 c node4(2)round 14, time: 6.935 c node3(2) get 38068 exported lits from network c node8(2)round 14, time: 6.944 c node4(2) get 56345 exported lits from network c node8(2) get 60247 exported lits from network c node6(2)round 14, time: 6.934 c node6(2) get 60786 exported lits from network c node1(0)round 15, time: 7.47 c node1(0) get 0 exported lits from network c node2(1)round 15, time: 7.78 c node2(1) get 0 exported lits from network c node7(2)round 15, time: 7.352 c node7(2) get 66476 exported lits from network c node5(2)round 15, time: 7.389 c node5(2) get 61963 exported lits from network c node3(2)round 15, time: 7.433 c node3(2) get 58654 exported lits from network c node4(2)round 15, time: 7.448 c node8(2)round 15, time: 7.455 c node8(2) get 60684 exported lits from network c node4(2) get 77573 exported lits from network c node6(2)round 15, time: 7.446 c node6(2) get 62870 exported lits from network c node1(0)round 16, time: 7.549 c node1(0) get 0 exported lits from network c node2(1)round 16, time: 7.581 c node2(1) get 0 exported lits from network c node7(2)round 16, time: 7.862 c node7(2) get 63902 exported lits from network c node5(2)round 16, time: 7.915 c node5(2) get 62018 exported lits from network c node3(2)round 16, time: 7.944 c node3(2) get 75642 exported lits from network c node8(2)round 16, time: 7.968 c node8(2) get 46504 exported lits from network c node4(2)round 16, time: 7.978 c node4(2) get 58550 exported lits from network c node6(2)round 16, time: 7.959 c node6(2) get 65241 exported lits from network c node1(0)round 17, time: 8.51 c node1(0) get 0 exported lits from network c node2(1)round 17, time: 8.84 c node2(1) get 0 exported lits from network c node7(2)round 17, time: 8.377 c node7(2) get 57430 exported lits from network c node5(2)round 17, time: 8.429 c node5(2) get 58363 exported lits from network c node3(2)round 17, time: 8.456 c node3(2) get 60027 exported lits from network c node8(2)round 17, time: 8.480 c node8(2) get 59134 exported lits from network c node6(2)round 17, time: 8.472 c node4(2)round 17, time: 8.509 c node6(2) get 62654 exported lits from network c node4(2) get 70297 exported lits from network c node1(0)round 18, time: 8.553 c node1(0) get 0 exported lits from network c node2(1)round 18, time: 8.586 c node2(1) get 0 exported lits from network c node7(2)round 18, time: 8.888 c node7(2) get 55080 exported lits from network c node5(2)round 18, time: 8.942 c node5(2) get 60046 exported lits from network c node8(2)round 18, time: 8.991 c node3(2)round 18, time: 8.981 c node8(2) get 46316 exported lits from network c node3(2) get 82408 exported lits from network c node6(2)round 18, time: 8.985 c node6(2) get 56658 exported lits from network c node4(2)round 18, time: 9.40 c node4(2) get 54840 exported lits from network c node1(0)round 19, time: 9.55 c node1(0) get 0 exported lits from network c node2(1)round 19, time: 9.89 c node2(1) get 0 exported lits from network c node7(2)round 19, time: 9.400 c node7(2) get 40907 exported lits from network c [leader] solve time out c node7 sharing nums: 19 c sharing time: 0.40 c node7 sharing received_num_by_network: 194696 c node7 sharing skip_num_by_network: 5216 c node7 sharing unique reduce percentage: 2.68% c [worker7] kissat exit with result: 0 c node5(2)round 19, time: 9.454 c node5(2) get 55197 exported lits from network c node5 sharing nums: 19 c sharing time: 0.45 c node5 sharing received_num_by_network: 191266 c node5 sharing skip_num_by_network: 3130 c node5 sharing unique reduce percentage: 1.64% c [worker5] kissat exit with result: 0 c node8(2)round 19, time: 9.504 c node3(2)round 19, time: 9.498 c node8(2) get 48048 exported lits from network c node8 sharing nums: 19 c sharing time: 0.50 c node8 sharing received_num_by_network: 190352 c node8 sharing skip_num_by_network: 4089 c node8 sharing unique reduce percentage: 2.15% c [worker8] kissat exit with result: 0 c node3(2) get 46609 exported lits from network c node3 sharing nums: 19 c sharing time: 0.50 c node3 sharing received_num_by_network: 194710 c node3 sharing skip_num_by_network: 2648 c node3 sharing unique reduce percentage: 1.36% c [worker3] kissat exit with result: 0 c node6(2)round 19, time: 9.494 c node6(2) get 46507 exported lits from network c node6 sharing nums: 19 c sharing time: 0.49 c node6 sharing received_num_by_network: 202626 c node6 sharing skip_num_by_network: 3727 c node6 sharing unique reduce percentage: 1.84% c [worker6] kissat exit with result: 0 c node1(0)round 20, time: 9.556 c node1(0) get 0 exported lits from network c node4(2)round 19, time: 9.553 c node1 sharing nums: 20 c sharing time: 0.05 c node1 sharing received_num_by_network: 0 c node1 sharing skip_num_by_network: 0 c node1 sharing unique reduce percentage: -nan% c [worker1] kissat exit with result: 0 c node4(2) get 44810 exported lits from network c node4 sharing nums: 19 c sharing time: 0.55 c node4 sharing received_num_by_network: 203364 c node4 sharing skip_num_by_network: 6532 c node4 sharing unique reduce percentage: 3.21% c [worker4] kissat exit with result: 0 c node2(1)round 20, time: 9.592 c node2(1) get 0 exported lits from network c node2 sharing nums: 20 c sharing time: 0.08 c node2 sharing received_num_by_network: 0 c node2 sharing skip_num_by_network: 0 c node2 sharing unique reduce percentage: -nan% c [worker2] kissat exit with result: 0 s UNKNOWN