diff --git a/run.sh b/run.sh
index 7d5068b..e402289 100755
--- a/run.sh
+++ b/run.sh
@@ -14,13 +14,10 @@
 # - 0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf
 
 
+
 # 这个存在问题
 DIR=/pub/data/chenzh/data/sat2022
-INSTANCE=51e4929accfa3a0e68bff09974c7f0f4-SAT_MS_sat_nurikabe_p16.pddl_166.cnf
-
-
-
-
+INSTANCE=0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf
 
 
 # make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=1 --threads=16 --times=3600 --share_method=1
diff --git a/src/leader.hpp b/src/leader.hpp
index 8d4f70c..ea74a72 100644
--- a/src/leader.hpp
+++ b/src/leader.hpp
@@ -49,10 +49,12 @@ void leader_main(light* S, int num_procs, int rank) {
     const auto& str_ref = ss.str();
     char* cstr = const_cast<char *>(str_ref.c_str());
 
-    printf("c [leader] hand out length of cnf instance to all nodes\n");
-
     int cnf_length = str_ref.size() + 1;
 
+    printf("c [leader] length of cnf (bytes): %lld\n", cnf_length);
+
+    printf("c [leader] hand out length of cnf instance to all nodes\n");
+
     MPI_Barrier(MPI_COMM_WORLD);
 
     MPI_Bcast(&cnf_length, 1, MPI_INT, 0, MPI_COMM_WORLD);
diff --git a/src/preprocess/preprocess.cpp b/src/preprocess/preprocess.cpp
index 2fd3c07..55fe87a 100644
--- a/src/preprocess/preprocess.cpp
+++ b/src/preprocess/preprocess.cpp
@@ -172,13 +172,15 @@ int preprocess::do_preprocess(char* filename) {
     oriclauses = clauses; 
     preprocess_init();
     int res = 1;
-    
-    res = preprocess_gauss();
-    if (!res) {
-        printf("c solved by gauss elimination\n");
-        release();
-        return 0;
-    }
+
+    // if (vars <= 1e5 && clauses <= 1e6) {    
+    //     res = preprocess_gauss();
+    //     if (!res) {
+    //         printf("c solved by gauss elimination\n");
+    //         release();
+    //         return 0;
+    //     }
+    // }
 
     res = preprocess_up();
     if (!res) {
@@ -214,17 +216,18 @@ int preprocess::do_preprocess(char* filename) {
         return 0;
     }
 
-
-    res = preprocess_binary();
-    if (!res) {
-        release();
-        delete []mapto;
-        delete []mapval;
-        clause.clear(true);
-        res_clause.clear(true);
-        resolution.clear(true);
-        return 0;
-    }
+    // if (clauses <= 1e7) {  
+    //     res = preprocess_binary();
+    //     if (!res) {
+    //         release();
+    //         delete []mapto;
+    //         delete []mapval;
+    //         clause.clear(true);
+    //         res_clause.clear(true);
+    //         resolution.clear(true);
+    //         return 0;
+    //     }
+    // }
     
     release();
     return 1;
diff --git a/src/solve.cpp b/src/solve.cpp
index ca07c33..87bf28b 100644
--- a/src/solve.cpp
+++ b/src/solve.cpp
@@ -258,19 +258,19 @@ void light::seperate_groups() {
     int worker_procs = num_procs - 1;
 
     if(worker_procs >= 8) {
-        int sat_procs = 0;
-        int unsat_procs = 2;
+        int sat_procs = worker_procs / 8;
+        int unsat_procs = worker_procs / 4;
         int default_procs = worker_procs - sat_procs - unsat_procs;
 
         std::vector<int> tmp;
         // [1, sat_procs] for sat
-        // if(rank >= 1 && rank <= sat_procs) {
-        //     worker_type = light::SAT;
-        // }
-        // for(int i=1; i<=sat_procs; i++) {
-        //     tmp.push_back(i);
-        // }
-        // sharing_groups.push_back(tmp);
+        if(rank >= 1 && rank <= sat_procs) {
+            worker_type = light::SAT;
+        }
+        for(int i=1; i<=sat_procs; i++) {
+            tmp.push_back(i);
+        }
+        sharing_groups.push_back(tmp);
         
         // [sat_procs+1, sat_procs+unsat_procs] for unsat
         if(rank >= sat_procs+1 && rank <= sat_procs+unsat_procs) {
diff --git a/src/worker.hpp b/src/worker.hpp
index d842c69..e159b6f 100644
--- a/src/worker.hpp
+++ b/src/worker.hpp
@@ -3,6 +3,7 @@
 #include <fstream>
 #include <ctime>
 #include <mpi.h>
+#include <cmath>
 
 #include "light.hpp"
 #include "utils/cmdline.h"
@@ -41,6 +42,26 @@ void worker_main(light* S, int num_procs, int rank) {
 
     MPI_Barrier(MPI_COMM_WORLD);
 
+    // mem_usage per thread per G input file (GB)
+    double mem_ptpg = 20.4;
+
+    // mem_usage per thread (GB)
+    double mem_pt = (double)cnf_length / 1073741824 * mem_ptpg;
+
+    //printf("mem_pt: %lf\n", mem_pt);
+
+    // max thread with 64G mem machine
+    double threads = 64.0 / mem_pt;
+    // printf("threads: %lf\n", threads);
+
+    if(threads > 16) {
+        printf("c [worker%d] threads per worker were set %d by default : %d\n", rank, OPT(threads));
+    } else {
+        OPT(threads) = floor(threads);
+        printf("c [worker%d] too big instance %lld\n", rank, cnf_length);
+        printf("c [worker%d] threads per worker were set %d by memcheck %d\n", rank, OPT(threads));
+    }
+
     int res = S->run();
 
     printf("c [worker%d] kissat exit with result: %d\n", rank, res);
diff --git a/test.log b/test.log
index ccdf39d..7cf7409 100644
--- a/test.log
+++ b/test.log
@@ -10,536 +10,13 @@ c reset_time          	 int       	 10        	 10        	 Reseting base interv
 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 share_method        	 int       	 0         	 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    	 3600.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		 /pub/data/chenzh/data/sat2022/d87714e099c66f0034fb95727fa47ccc-Wallace_Bits_Fast_2.cnf.cnf	 ""        	 CNF format instance
+c instance            	 string		 /pub/data/chenzh/data/sat2022/51e4929accfa3a0e68bff09974c7f0f4-SAT_MS_sat_nurikabe_p16.pddl_166.cnf	 ""        	 CNF format instance
 c --------------------------------------------------
 c [leader] preprocess(simplify) input data
-c [GE] XORs: 2879 (time: 0.00)
-c [GE] VAR SCC: 1009
-c [GE] XOR SCCs: 66 (time: 0.00)
-c [GE] unary xor: 0, bin xor: 0, bin added
-c After preprocess: vars: 5892 -> 5825 , clauses: 23367 -> 23165 ,
-c [CE] almost one cons: 133
-c len 0
-c sz 2
-c turns: 4
-c After preprocess: vars: 5825 -> 5675 , clauses: 23165 -> 22697 ,
-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:5 number:16 seed:8
-c index:4 number:16 seed:8
-c index:0 number:16 seed:8
-c index:3 number:16 seed:8
-c index:1 number:16 seed:8
-c index:2 number:16 seed:8
-c index:10 number:16 seed:8
-c index:6 number:16 seed:8
-c index:15 number:16 seed:8
-c index:8 number:16 seed:8
-c index:15 number:16 seed:3
-c index:1 number:16 seed:3
-c index:7 number:16 seed:8
-c index:0 number:16 seed:3
-c index:2 number:16 seed:7
-c index:9 number:16 seed:3
-c index:5 number:16 seed:3
-c index:2 number:16 seed:5
-c index:7 number:16 seed:5
-c index:13 number:16 seed:5
-c index:4 number:16 seed:3
-c index:7 number:16 seed:3
-c index:0 number:16 seed:5
-c index:6 number:16 seed:5
-c index:3 number:16 seed:5
-c index:11 number:16 seed:5
-c index:14 number:16 seed:8
-c index:12 number:16 seed:8
-c index:9 number:16 seed:8
-c index:13 number:16 seed:8
-c index:11 number:16 seed:8
-c index:0 number:16 seed:4
-c index:10 number:16 seed:5
-c index:10 number:16 seed:6
-c index:0 number:16 seed:6
-c index:4 number:16 seed:5
-c index:12 number:16 seed:5
-c index:15 number:16 seed:5
-c index:1 number:16 seed:5
-c index:8 number:16 seed:5
-c index:9 number:16 seed:5
-c index:5 number:16 seed:5
-c index:14 number:16 seed:5
-c index:5 number:16 seed:4
-c index:7 number:16 seed:6
-c index:5 number:16 seed:6
-c index:1 number:16 seed:6
-c index:3 number:16 seed:6
-c index:3 number:16 seed:4
-c index:13 number:16 seed:4
-c index:14 number:16 seed:4
-c index:8 number:16 seed:4
-c index:10 number:16 seed:4
-c index:2 number:16 seed:4
-c index:14 number:16 seed:6
-c index:6 number:16 seed:6
-c index:13 number:16 seed:6
-c index:15 number:16 seed:6
-c index:9 number:16 seed:6
-c index:2 number:16 seed:6
-c index:3 number:16 seed:3
-c index:14 number:16 seed:3
-c index:2 number:16 seed:3
-c index:11 number:16 seed:4
-c index:12 number:16 seed:3
-c index:13 number:16 seed:3
-c index:12 number:16 seed:4
-c index:8 number:16 seed:3
-c index:1 number:16 seed:1
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-c index:0 number:16 seed:1
-c index:12 number:16 seed:1
-c index:5 number:16 seed:1
-c index:12 number:16 seed:6
-c index:6 number:16 seed:4
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-c index:13 number:16 seed:1
-c index:7 number:16 seed:4
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-c index:15 number:16 seed:4
-c index:9 number:16 seed:4
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-c index:7 number:16 seed:1
-c index:-1 number:-1 seed:-1
-c index:4 number:16 seed:4
-c index:-1 number:-1 seed:-1
-c index:1 number:16 seed:4
-c index:10 number:16 seed:1
-c index:15 number:16 seed:1
-c index:9 number:16 seed:1
-c index:-1 number:-1 seed:-1
-c index:-1 number:-1 seed:-1
-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 index:11 number:16 seed:6
-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
-c index:4 number:16 seed:6
-c index:0 number:16 seed:7
-c index:1 number:16 seed:7
-c index:10 number:16 seed:3
-c index:4 number:16 seed:1
-c index:6 number:16 seed:1
-c index:3 number:16 seed:1
-c index:8 number:16 seed:1
-c index:14 number:16 seed:1
-c index:11 number:16 seed:1
-c index:6 number:16 seed:3
-c index:13 number:16 seed:7
-c index:15 number:16 seed:7
-c index:7 number:16 seed:7
-c index:5 number:16 seed:7
-c index:14 number:16 seed:7
-c index:8 number:16 seed:7
-c index:2 number:16 seed:1
-c index:8 number:16 seed:6
-c index:9 number:16 seed:7
-c index:3 number:16 seed:7
-c index:12 number:16 seed:7
-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
-c index:10 number:16 seed:7
-c index:6 number:16 seed:7
-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
-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
-c index:11 number:16 seed:3
-c index:4 number:16 seed:7
-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
-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
-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
-c index:11 number:16 seed:7
-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
-c node4(2)round 1, time: 0.0
-c node4(2) get 6835 exported lits from network
-c node4 sharing nums: 1
-c sharing time: 0.00
-c node4 sharing received_num_by_network: 1997
-c node4 sharing skip_num_by_network: 0
-c node4 sharing unique reduce percentage: 0.00%
-c [worker4] kissat exit with result: 0
-c node2(1)round 1, time: 0.0
-c node2(1) get 0 exported lits from network
-c node2 sharing nums: 1
-c sharing time: 0.00
-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: 10
-c [worker2] getting terminate signal
-c node1(0)round 1, time: 0.0
-c node1(0) get 0 exported lits from network
-c node1 sharing nums: 1
-c sharing time: 0.00
-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: 10
-c [worker1] getting terminate signal
-c node3(2)round 1, time: 0.0
-c node3(2) get 20985 exported lits from network
-c node3 sharing nums: 1
-c sharing time: 0.00
-c node3 sharing received_num_by_network: 5906
-c node3 sharing skip_num_by_network: 0
-c node3 sharing unique reduce percentage: 0.00%
-c [worker3] kissat exit with result: 10
-c [worker3] getting terminate signal
-c node7(2)round 1, time: 0.0
-c node7(2) get 34928 exported lits from network
-c node7 sharing nums: 1
-c sharing time: 0.01
-c node7 sharing received_num_by_network: 10690
-c node7 sharing skip_num_by_network: 1147
-c node7 sharing unique reduce percentage: 10.73%
-c [worker7] kissat exit with result: 10
-c [worker7] getting terminate signal
-c node8(2)round 1, time: 0.0
-c node8(2) get 0 exported lits from network
-c node8 sharing nums: 1
-c sharing time: 0.00
-c node8 sharing received_num_by_network: 0
-c node8 sharing skip_num_by_network: 0
-c node8 sharing unique reduce percentage: -nan%
-c [worker8] kissat exit with result: 10
-c [worker8] getting send model signal
-c node6(2)round 1, time: 0.0
-c node6(2) get 0 exported lits from network
-c node6 sharing nums: 1
-c sharing time: 0.00
-c node6 sharing received_num_by_network: 0
-c node6 sharing skip_num_by_network: 0
-c node6 sharing unique reduce percentage: -nan%
-c [worker6] kissat exit with result: 0
-c [leader] received model size: 5675