diff --git a/.gitignore b/.gitignore
index 87620ac..10f39cf 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,5 @@
 .ipynb_checkpoints/
+*.cnf
+*.sat
+*.unsat
+*.out
diff --git a/README.md b/README.md
index 3730bd5..017e413 100644
--- a/README.md
+++ b/README.md
@@ -4,6 +4,13 @@
 
 - [fire](https://github.com/google/python-fire) python library
   - Either manually install it or use [pipenv](https://pypi.org/project/pipenv/)
-- [kissat](https://github.com/arminbiere/kissat) in `$PATH`
+- [kissat](https://github.com/arminbiere/kissat) installed and located in `$PATH`
 
 ## Usage
+
+```
+python main.py n a b N
+```
+checks if `N` points with no `n`-gon, `a`-cap and `b`-cup exists. The SAT
+instance is produced as `cnf` file, and either the solution or unsatisfiabilty
+proof is generated as `.sat` or `.unsat` file respectively.
diff --git a/lib/sat.py b/lib/sat.py
index 6e8b5d1..2e684cf 100644
--- a/lib/sat.py
+++ b/lib/sat.py
@@ -89,9 +89,11 @@ def load(self, filename):
 
     def solve(self, filename="tmp"):
         self.write(f"{filename}.cnf")
-        out_code = os.system(f"kissat {filename}.cnf > {filename}.sol")
+        out_code = os.system(f"kissat {filename}.cnf {filename}.unsat > {filename}.out")
         if out_code != 2560:
             return False
-
-        self.load(f"{filename}.sol")
-        return True
+        else:
+            os.system(f"rm {filename}.unsat")
+            os.system(f"mv {filename}.out {filename}.sat")
+            self.load(f"{filename}.sat")
+            return True
diff --git a/main.py b/main.py
index 46af64a..eca93a9 100644
--- a/main.py
+++ b/main.py
@@ -1 +1,15 @@
 # TODO: copy the jupyter notebook codes to here, make it reproducable
+
+import os
+import fire
+import lib.erdos as erdos
+from lib.util import binom
+
+def main(n, a, b, N, filename=None, signotope=False):
+    inst = erdos.etv(n, a, b, N)
+    if not filename:
+        filename = f"etv_{n}_{a}_{b}_{N}"
+    inst.solve(filename)
+
+if __name__ == '__main__':
+    fire.Fire(main)