diff --git a/light b/light
index ba291ee..681b026 100755
Binary files a/light and b/light differ
diff --git a/light-v2 b/light-v2
new file mode 100755
index 0000000..ba291ee
Binary files /dev/null and b/light-v2 differ
diff --git a/preprocess.cpp b/preprocess.cpp
index d5bdf53..cadbf88 100644
--- a/preprocess.cpp
+++ b/preprocess.cpp
@@ -110,14 +110,15 @@ bool preprocess::preprocess_resolution() {
     for (int i = 1; i <= vars; i++) {
         occurn[i].clear();
         occurp[i].clear();
-        resseen[i] = resseen[i + vars] = clean[i] = seen[i] = 0;
+        resseen[i - 1] = resseen[i + vars - 1] = clean[i] = seen[i] = 0;
     }
     for (int i = 1; i <= clauses; i++) {
         int l = clause[i].size();
         clause_delete[i] = 0;
-        for (int j = 0; j < l; j++)
+        for (int j = 0; j < l; j++) {
             if (clause[i][j] > 0) occurp[abs(clause[i][j])].push(i);
             else occurn[abs(clause[i][j])].push(i);
+        }
     }
     for (int i = 1; i <= vars; i++)
         if (occurn[i].size() == 0 && occurp[i].size() == 0) clean[i] = 1;  
@@ -204,12 +205,13 @@ bool preprocess::preprocess_resolution() {
     }
     return true;
 }
-
+int count = 0;
 void preprocess::update_var_clause_label() {
+    ++count;
     int remain_var = 0;
     for (int i = 1; i <= vars; i++) color[i] = 0;
     for (int i = 1; i <= clauses; i++) {
-        if (clause_delete[i]) continue;
+        if (clause_delete[i]) {continue;}
         int l = clause[i].size();
         for (int j = 0; j < l; j++) {
             if (color[abs(clause[i][j])] == 0) color[abs(clause[i][j])] = ++remain_var;       
@@ -243,48 +245,49 @@ bool preprocess::preprocess_binary() {
     C = new HashMap();
     for (int i = 1; i <= clauses; i++) {
         int l = clause[i].size();
-        for (int j = 0; j < l; j++)
+        for (int j = 0; j < l; j++) {
             clause[i][j] = tolit(clause[i][j]);
+        }
     }
     nlit = (vars << 1) + 2;
     for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, color[i] = 0;
     for (int i = 1; i <= clauses; i++) clause_delete[i] = 0;
-    int len = 0;
-    for (int i = 1; i <= clauses; i++) {
-        if (clause[i].size() != 2) continue;
-        nxtc[++len] = i;
-        ll id1 = mapv(clause[i][0], clause[i][1]),
-           id2 = mapv(clause[i][1], clause[i][0]);
-        C->insert(id1, i);
-        C->insert(id2, i);
-    }
+    // int len = 0;
+    // for (int i = 1; i <= clauses; i++) {
+    //     if (clause[i].size() != 2) continue;
+    //     nxtc[++len] = i;
+    //     ll id1 = mapv(clause[i][0], clause[i][1]),
+    //        id2 = mapv(clause[i][1], clause[i][0]);
+    //     C->insert(id1, i);
+    //     C->insert(id2, i);
+    // }
            
-    for (int k = 1; k <= len; k++) {
-        int i = nxtc[k];
-        if (clause[i].size() != 2 || clause_delete[i]) continue;
-        int r = C->get(mapv(negative(clause[i][0]), negative(clause[i][1])), 0);
-        if (r) {
-            clause_delete[r] = clause_delete[i] = 1;
-            int u = toiidx(clause[i][0]), v = toiidx(clause[i][1]);
-            int fa = find(u), fb = find(v);
-            int sig = sign(clause[i][0]) * sign(clause[i][1]) * (-1);
-            //sig == 1 : a = b   -1 : a = -b
-            if (fa != fb) {
-                if (fa < fb) {
-                    f[fa] = fb;
-                    val[fa] = sig / (val[u] * val[v]);
-                }
-                else if (fa > fb) {
-                    f[fb] = fa;
-                    val[fb] = sig / (val[u] * val[v]);
-                }
-            }
-            else if (sig != val[u] * val[v])
-                return false;
-        }
-    }
+    // for (int k = 1; k <= len; k++) {
+    //     int i = nxtc[k];
+    //     if (clause[i].size() != 2 || clause_delete[i]) continue;
+    //     int r = C->get(mapv(negative(clause[i][0]), negative(clause[i][1])), 0);
+    //     if (r) {
+    //         clause_delete[r] = clause_delete[i] = 1;
+    //         int u = toiidx(clause[i][0]), v = toiidx(clause[i][1]);
+    //         int fa = find(u), fb = find(v);
+    //         int sig = sign(clause[i][0]) * sign(clause[i][1]) * (-1);
+    //         //sig == 1 : a = b   -1 : a = -b
+    //         if (fa != fb) {
+    //             if (fa < fb) {
+    //                 f[fa] = fb;
+    //                 val[fa] = sig / (val[u] * val[v]);
+    //             }
+    //             else if (fa > fb) {
+    //                 f[fb] = fa;
+    //                 val[fb] = sig / (val[u] * val[v]);
+    //             }
+    //         }
+    //         else if (sig != val[u] * val[v])
+    //             return false;
+    //     }
+    // }
     
-    for (int i = 1; i <= vars; i++) find(i);
+    // for (int i = 1; i <= vars; i++) find(i);
 
     for (int i = 1; i <= clauses; i++) {
         if (clause_delete[i]) continue;
@@ -319,12 +322,12 @@ bool preprocess::preprocess_binary() {
     }
 
     update_var_clause_label();
-    for (int i = 1; i <= orivars; i++) {
-        if (mapval[i]) continue;
-        int v = mapto[i], fa = find(v);
-        if (color[fa]) mapto[i] = color[fa] * val[v];
-        else {puts("why happened"); mapval[i] = val[v], mapto[i] = 0;}
-    }
+    // for (int i = 1; i <= orivars; i++) {
+    //     if (mapval[i]) continue;
+    //     int v = mapto[i], fa = find(v);
+    //     if (color[fa]) mapto[i] = color[fa] * val[v];
+    //     else {puts("why happened"); mapval[i] = val[v], mapto[i] = 0;}
+    // }
     
     return true;
 }
diff --git a/preprocess.o b/preprocess.o
index b37f4ac..bbf9a6d 100644
Binary files a/preprocess.o and b/preprocess.o differ