diff --git a/forseti/exceptions.py b/forseti/exceptions.py
new file mode 100644
index 0000000..7a95456
--- /dev/null
+++ b/forseti/exceptions.py
@@ -0,0 +1,2 @@
+class TimeoutException(Exception):
+    pass
diff --git a/forseti/prover.py b/forseti/prover.py
index 626948e..e3b0feb 100644
--- a/forseti/prover.py
+++ b/forseti/prover.py
@@ -3,9 +3,12 @@
 """
 # pylint: disable=fixme
 from copy import deepcopy
+import time
+
 from forseti.formula import Formula, Not, And, Or, Skolem, Herbrand, Predicate
 from forseti import converter, parser
 import forseti.util as util
+from forseti import exceptions
 
 
 class Prover(object):
@@ -13,13 +16,15 @@ class Prover(object):
     Prover class
     """
 
-    def __init__(self):
+    def __init__(self, timeout=30):
         self._cnf_list = []
         self.parents = []
         self.formulas = []
         self.goals = []
         self._goals = []
         self.proof_found = False
+        self.proof_time = 0
+        self.proof_timeout = timeout
 
     def add_formula(self, statement):
         """
@@ -80,7 +85,7 @@ def run_prover(self):
             self._cnf_list[i] = sorted(self._cnf_list[i])
         for i in range(len(self._cnf_list)):
             self.parents.append([])
-        self.proof_found = self._resolve()
+        self.proof_found, self.proof_time = self._resolve()
         return self.proof_found
 
     @staticmethod
@@ -133,9 +138,12 @@ def _resolve(self):
 
         :return:
         """
+        start_time = time.time()
         i = 0
         checked = list()
         while i < len(self._cnf_list):
+            if (time.time() - start_time) > self.proof_timeout:
+                raise exceptions.TimeoutException('Proof timeout reached')
             j = i + 1
             while j < len(self._cnf_list):
                 if [i, j] in checked:
@@ -165,7 +173,7 @@ def _resolve(self):
                         if len(new_cnf) == 0:
                             self._cnf_list.append([])
                             self.parents.append([i, j])
-                            return True
+                            return True, time.time() - start_time
                         if not util.is_tautology(new_cnf) and \
                            new_cnf not in self._cnf_list:
                             have_resolve = True
@@ -180,7 +188,7 @@ def _resolve(self):
                     break
                 j += 1
             i += 1
-        return False
+        return False, time.time() - start_time
 
     def _tautology_elimination(self):
         """
@@ -308,4 +316,4 @@ def get_proof(self):
     prover.add_formula("exists(x,forall(y,A(x,y)))")
     prover.add_goal("exists(x,A(x,a))")
     print(prover.run_prover())
-    print("\n".join(prover.get_proof()))
\ No newline at end of file
+    print("\n".join(prover.get_proof()))
diff --git a/setup.py b/setup.py
index e1d2fc7..638ace8 100644
--- a/setup.py
+++ b/setup.py
@@ -11,6 +11,7 @@ def read(*paths):
     with open(os.path.join(*paths), 'r') as open_file:
         return open_file.read()
 
+
 setup(
     # Metadata
     name='forseti',
diff --git a/tests/bram_testcases/README.md b/tests/bram_testcases/README.md
index 18ba486..2b68872 100644
--- a/tests/bram_testcases/README.md
+++ b/tests/bram_testcases/README.md
@@ -13,4 +13,4 @@ The handouts, in order of difficulty in given arguments and for ATP testing:
 * [Propositional Logic Arguments](handouts/PropLogicArguments.pdf)
 * [Propositional Logic Arguments II](handouts/PropLogicArgumentsII.pdf)
 * [Predicate Logic Arguments](handouts/PredicateLogicArguments.pdf)
-* [First Order Logic Proofs](handouts/FOLProofs.pdf)
+* [First Order Logic Proofs](handouts/FOLProofsII.pdf)
diff --git a/tests/bram_testcases/handouts/FOLProofs.pdf b/tests/bram_testcases/handouts/FOLProofsII.pdf
similarity index 100%
rename from tests/bram_testcases/handouts/FOLProofs.pdf
rename to tests/bram_testcases/handouts/FOLProofsII.pdf
diff --git a/tests/bram_testcases/test_fol_proofs_i.py b/tests/bram_testcases/test_fol_proofs_i.py
new file mode 100644
index 0000000..ed27a7c
--- /dev/null
+++ b/tests/bram_testcases/test_fol_proofs_i.py
@@ -0,0 +1,149 @@
+import unittest
+from forseti.prover import Prover
+from forseti.formula import Predicate, Skolem, Herbrand
+
+
+class TestFOLProofsI(unittest.TestCase):
+    def setUp(self):
+        Predicate.reset()
+        Skolem.reset()
+        Herbrand.reset()
+
+    def test_problem_01(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(A(x),B(x)))")
+        prover.add_formula("forall(x,if(B(x),C(x)))")
+        prover.add_goal("forall(x,if(A(x),C(x)))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_02(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(A(x),and(B(x),C(x))))")
+        prover.add_formula("forall(x,if(A(x),not(C(x))))")
+        prover.add_goal("not(A(a))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_03(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(A(x),B(x)))")
+        prover.add_formula("forall(x,if(not(A(x)),C(x)))")
+        prover.add_goal("forall(x,if(not(B(x)),not(C(x))))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_04(self):
+        prover = Prover()
+        prover.add_formula("exists(x,and(A(x),not(B(x))))")
+        prover.add_formula("exists(x,and(A(x),not(C(x))))")
+        prover.add_formula("exists(x,and(not(B(x)),D(x)))")
+        prover.add_goal("exists(x,and(and(A(x),not(B(x))),D(x)))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_05(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(A(x),F(x)))")
+        prover.add_formula("if(exists(x,F(x)),not(exists(y,G(y))))")
+        prover.add_goal("forall(x,if(exists(y,A(y)),not(G(x))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_06(self):
+        prover = Prover()
+        prover.add_formula("exists(x,or(A(x),not(B(x))))")
+        prover.add_formula("forall(x,if(and(A(x),not(B(x))),C(x)))")
+        prover.add_goal("exists(x,C(x))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_07(self):
+        prover = Prover()
+        prover.add_formula("forall(x,not(F(x,x)))")
+        prover.add_formula("if(not(forall(x,G(x))),exists(y,F(y,a)))")
+        prover.add_goal("exists(z,and(G(z),F(z,z)))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_08(self):
+        prover = Prover()
+        prover.add_formula("forall(x,exists(y,and(F(x),G(x,y))))")
+        prover.add_goal("exists(y,forall(x,and(F(x),G(x,y))))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_09(self):
+        prover = Prover()
+        prover.add_formula("exists(x,and(F(x),forall(y,if(G(y),L(x,y)))))")
+        prover.add_formula("forall(x,if(F(x),forall(y,if(M(y),not(L(x,y))))))")
+        prover.add_goal("forall(x,if(G(x),not(M(x))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_10(self):
+        prover = Prover()
+        prover.add_formula("or(F(a),exists(y,G(y,a)))")
+        prover.add_formula("or(F(b),exists(y,not(G(y,a))))")
+        prover.add_goal("exists(y,G(y,a))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_11(self):
+        prover = Prover()
+        prover.add_formula("forall(x,not(J(x)))")
+        prover.add_formula("if(exists(y,or(H(b,y),R(y,y))),exists(x,J(x)))")
+        prover.add_goal("forall(y,not(or(H(b,y),R(y,y))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_12(self):
+        prover = Prover()
+        prover.add_formula("forall(z,iff(L(z),H(z)))")
+        prover.add_formula("forall(x,not(or(H(x),not(B(x)))))")
+        prover.add_goal("not(L(b))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_13(self):
+        prover = Prover()
+        prover.add_formula("or(not(forall(x,K(x,x))),forall(y,H(y,y)))")
+        prover.add_goal("exists(z,if(not(H(z,z)),not(K(z,z))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_14(self):
+        prover = Prover()
+        prover.add_formula("forall(x,forall(y,or(F(x),G(x,y))))")
+        prover.add_formula("exists(x,F(x))")
+        prover.add_goal("exists(x,exists(y,G(x,y)))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_15(self):
+        prover = Prover()
+        prover.add_formula("forall(x,forall(y,forall(z,if(and(L(x,y),L(y,z)),"
+                           "L(x,z)))))")
+        prover.add_formula("forall(x,forall(y,if(L(x,y),L(y,x))))")
+        prover.add_goal("forall(x,L(x,x))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_16(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(S(x),exists(y,and(S(y),forall(z,"
+                           "iff(B(z,y),and(B(z,x),B(z,z))))))))")
+        prover.add_formula("forall(x,not(B(x,x)))")
+        prover.add_formula("exists(x,S(x))")
+        prover.add_goal("exists(x,and(S(x),forall(y,not(B(y,x)))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_17(self):
+        prover = Prover()
+        prover.add_formula("forall(x,forall(y,if(and(A(x),B(y)),C(x,y))))")
+        prover.add_formula("exists(y,and(F(y),forall(z,if(H(z),C(y,z)))))")
+        prover.add_formula("forall(x,forall(y,forall(z,if(and(L(x,y),L(y,z)),"
+                           "L(x,z)))))")
+        prover.add_formula("forall(x,if(F(x),B(x)))")
+        prover.add_goal("forall(z,forall(y,if(and(A(z),H(y)),C(z,y))))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_18(self):
+        self.skipTest('Should work')
+        prover = Prover()
+        prover.add_formula("forall(x,if(exists(y,and(A(y),B(x,y))),C(x)))")
+        prover.add_formula("exists(y,and(D(y),exists(x,and(F(x),and(G(x),B(y,x))))))")
+        prover.add_formula("forall(x,if(F(x),A(x)))")
+        prover.add_formula(
+            "if(exists(x,and(C(x),D(x))),if(exists(y,and(D(y),exists(z,B(y,z)))),forall(x,F(x))))")
+        prover.add_goal("forall(x,A(x))")
+        self.assertTrue(prover.run_prover())
+
+
+if __name__ == '__main__':
+    unittest.main()
\ No newline at end of file
diff --git a/tests/bram_testcases/test_fol_proofs_ii.py b/tests/bram_testcases/test_fol_proofs_ii.py
new file mode 100644
index 0000000..1da6309
--- /dev/null
+++ b/tests/bram_testcases/test_fol_proofs_ii.py
@@ -0,0 +1,10 @@
+import unittest
+from forseti.prover import Prover
+
+
+class TestFOLProofsII(unittest.TestCase):
+    pass
+
+
+if __name__ == '__main__':
+    unittest.main()
\ No newline at end of file
diff --git a/tests/bram_testcases/test_prop_logic_arguments_i.py b/tests/bram_testcases/test_prop_logic_arguments_i.py
new file mode 100644
index 0000000..0743559
--- /dev/null
+++ b/tests/bram_testcases/test_prop_logic_arguments_i.py
@@ -0,0 +1,150 @@
+import unittest
+from forseti.prover import Prover
+
+
+class TestPropLogicArgumentsI(unittest.TestCase):
+    def test_problem_01(self):
+        prover = Prover()
+        prover.add_formula('if(A, and(B, C))')
+        prover.add_formula('iff(C, B)')
+        prover.add_formula('not(C)')
+        prover.add_goal('not(A)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_02(self):
+        prover = Prover()
+        prover.add_formula('if(K, H)')
+        prover.add_formula('if(H, L)')
+        prover.add_formula('if(L, M)')
+        prover.add_goal('if(K, M)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_03(self):
+        prover = Prover()
+        prover.add_formula('not(iff(A, B))')
+        prover.add_formula('not(A)')
+        prover.add_formula('not(B)')
+        prover.add_goal('and(C, not(C))')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_04(self):
+        prover = Prover()
+        prover.add_formula('and(A, or(B, C))')
+        prover.add_formula('if(or(not(C), H), if(H, not(H)))')
+        prover.add_goal('and(A, B)')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_05(self):
+        prover = Prover()
+        prover.add_formula('if(R, Q)')
+        prover.add_formula('not(and(T, not(S)))')
+        prover.add_formula('or(not(Q), not(S))')
+        prover.add_goal('or(not(R), not(T))')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_06(self):
+        prover = Prover()
+        prover.add_formula('and(A, if(B, C))')
+        prover.add_goal('or(and(A, B), and(A, C))')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_07(self):
+        prover = Prover()
+        prover.add_formula('if(and(or(C, D), H), A)')
+        prover.add_formula('D')
+        prover.add_goal('if(H, A)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_08(self):
+        prover = Prover()
+        prover.add_formula('if(or(J, M), not(and(J, M)))')
+        prover.add_formula('iff(M, if(M, J))')
+        prover.add_goal('if(M, J)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_09(self):
+        prover = Prover()
+        prover.add_formula('not(iff(A, B))')
+        prover.add_goal('iff(not(A), not(B))')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_10(self):
+        prover = Prover()
+        prover.add_goal('iff(if(not(P), P), P)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_11(self):
+        prover = Prover()
+        prover.add_formula('if(M, if(K, B))')
+        prover.add_formula('if(not(K), not(M))')
+        prover.add_formula('and(L, M)')
+        prover.add_goal('B')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_12(self):
+        prover = Prover()
+        prover.add_formula('if(or(not(J), K), and(L, M))')
+        prover.add_formula('not(or(not(J), K))')
+        prover.add_goal('not(and(L, M))')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_13(self):
+        prover = Prover()
+        prover.add_formula('not(and(not(A), not(B)))')
+        prover.add_goal('and(A, B)')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_14(self):
+        prover = Prover()
+        prover.add_formula('or(iff(M, K), not(and(K, D)))')
+        prover.add_formula('if(not(M), not(K))')
+        prover.add_formula('if(not(D), not(and(K, D)))')
+        prover.add_goal('M')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_15(self):
+        prover = Prover()
+        prover.add_formula('and(B, or(H, Z))')
+        prover.add_formula('not(if(Z, K))')
+        prover.add_formula('if(iff(B, Z), not(Z))')
+        prover.add_formula('not(K)')
+        prover.add_goal('and(M, N)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_16(self):
+        prover = Prover()
+        prover.add_formula('and(iff(D, not(G)), G)')
+        prover.add_formula('if(or(G, and(if(A, D), A)), not(D))')
+        prover.add_goal('if(G, not(D))')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_17(self):
+        prover = Prover()
+        prover.add_formula('if(J, if(T, J))')
+        prover.add_formula('if(T, if(J, T))')
+        prover.add_goal('and(not(J), not(T))')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_18(self):
+        prover = Prover()
+        prover.add_formula('and(A, if(B, C))')
+        prover.add_goal('or(and(A, C), and(A, not(B)))')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_19(self):
+        prover = Prover()
+        prover.add_formula('or(A, not(and(B, C)))')
+        prover.add_formula('not(B)')
+        prover.add_formula('not(or(A, C))')
+        prover.add_goal('A')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_20(self):
+        prover = Prover()
+        prover.add_formula('or(iff(G, H), iff(not(G), H))')
+        prover.add_goal('or(iff(not(G), not(H)), not(iff(G, H)))')
+        self.assertTrue(prover.run_prover())
+
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/tests/bram_testcases/test_prop_logic_arguments_ii.py b/tests/bram_testcases/test_prop_logic_arguments_ii.py
new file mode 100644
index 0000000..d788a89
--- /dev/null
+++ b/tests/bram_testcases/test_prop_logic_arguments_ii.py
@@ -0,0 +1,154 @@
+import unittest
+from forseti.prover import Prover
+
+
+class TestPropLogicArgumentsII(unittest.TestCase):
+    def test_problem_01(self):
+        prover = Prover()
+        prover.add_formula('if(K, not(K))')
+        prover.add_goal('not(K)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_02(self):
+        prover = Prover()
+        prover.add_formula('if(R, R)')
+        prover.add_goal('R')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_03(self):
+        prover = Prover()
+        prover.add_formula('iff(P, not(N))')
+        prover.add_goal('or(N, P)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_04(self):
+        prover = Prover()
+        prover.add_formula('not(and(G, M))')
+        prover.add_formula('or(M, not(G))')
+        prover.add_goal('not(G)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_05(self):
+        prover = Prover()
+        prover.add_formula('iff(K, not(L))')
+        prover.add_formula('not(and(L, not(K)))')
+        prover.add_goal('if(K, L)')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_06(self):
+        prover = Prover()
+        prover.add_formula('Z')
+        prover.add_goal('if(E, if(Z, E))')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_07(self):
+        prover = Prover()
+        prover.add_formula('not(and(W, not(X)))')
+        prover.add_formula('not(and(X, not(W)))')
+        prover.add_goal('or(X, W)')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_08(self):
+        prover = Prover()
+        prover.add_formula('iff(C, D)')
+        prover.add_formula('or(E, not(D))')
+        prover.add_goal('if(E, C)')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_09(self):
+        prover = Prover()
+        prover.add_formula('iff(A, and(B, C))')
+        prover.add_formula('or(not(C), B)')
+        prover.add_goal('if(A, B)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_10(self):
+        prover = Prover()
+        prover.add_formula('if(J, if(K, L))')
+        prover.add_formula('if(K, if(J, L))')
+        prover.add_goal('if(or(J, K), L)')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_11(self):
+        prover = Prover()
+        prover.add_formula('not(iff(K, S))')
+        prover.add_formula('if(S, not(or(R, K)))')
+        prover.add_goal('or(R, not(S))')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_12(self):
+        prover = Prover()
+        prover.add_formula('if(E, and(F, G))')
+        prover.add_formula('if(F, if(G, H))')
+        prover.add_goal('if(E, H)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_13(self):
+        prover = Prover()
+        prover.add_formula('if(A, or(N, Q))')
+        prover.add_formula('not(or(N, not(A)))')
+        prover.add_goal('if(A, Q)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_14(self):
+        prover = Prover()
+        prover.add_formula('if(G, H)')
+        prover.add_formula('iff(R, G)')
+        prover.add_formula('or(not(H), G)')
+        prover.add_goal('iff(R, H)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_15(self):
+        prover = Prover()
+        prover.add_formula('if(L, M)')
+        prover.add_formula('if(M, N)')
+        prover.add_formula('if(N, L)')
+        prover.add_goal('or(L, N)')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_16(self):
+        prover = Prover()
+        prover.add_formula('if(S, T)')
+        prover.add_formula('if(S, not(T))')
+        prover.add_formula('if(not(T), S)')
+        prover.add_goal('or(S, not(T))')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_17(self):
+        prover = Prover()
+        prover.add_formula('if(W, X)')
+        prover.add_formula('if(X, W)')
+        prover.add_formula('if(X, Y)')
+        prover.add_formula('if(Y, X)')
+        prover.add_goal('iff(W, Y)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_18(self):
+        prover = Prover()
+        prover.add_formula('iff(K, or(L, M))')
+        prover.add_formula('if(L, M)')
+        prover.add_formula('if(M, K)')
+        prover.add_formula('or(K, L)')
+        prover.add_goal('if(K, L)')
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_19(self):
+        prover = Prover()
+        prover.add_formula('if(A, B)')
+        prover.add_formula('if(and(A, B), C)')
+        prover.add_formula('if(A, if(C, D))')
+        prover.add_goal('if(A, D)')
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_20(self):
+        prover = Prover()
+        prover.add_formula('or(not(A), R)')
+        prover.add_formula('not(and(N, not(C)))')
+        prover.add_formula('if(R, C)')
+        prover.add_formula('if(C, not(N))')
+        prover.add_goal('or(A, C)')
+        self.assertFalse(prover.run_prover())
+
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/tests/bram_testcases/prop_logic_proofs_tester.py b/tests/bram_testcases/test_prop_logic_proofs_i.py
similarity index 93%
rename from tests/bram_testcases/prop_logic_proofs_tester.py
rename to tests/bram_testcases/test_prop_logic_proofs_i.py
index b6817fe..486297a 100644
--- a/tests/bram_testcases/prop_logic_proofs_tester.py
+++ b/tests/bram_testcases/test_prop_logic_proofs_i.py
@@ -6,22 +6,22 @@
 from forseti.prover import Prover
 
 
-class PropLogicProofsTester(unittest.TestCase):
-    def test_problem_1(self):
+class TestPropLogicProofsI(unittest.TestCase):
+    def test_problem_01(self):
         prover = Prover()
         prover.add_formula("and(R, and(C, not(F)))")
         prover.add_formula("if(or(R, S), not(W))")
         prover.add_goal("not(W)")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_2(self):
+    def test_problem_02(self):
         prover = Prover()
         prover.add_formula("if(A, and(B, C))")
         prover.add_formula("not(C)")
         prover.add_goal("not(and(A, D))")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_3(self):
+    def test_problem_03(self):
         prover = Prover()
         prover.add_formula("not(iff(A, B))")
         prover.add_formula("not(A)")
@@ -29,14 +29,14 @@ def test_problem_3(self):
         prover.add_goal("and(C, not(C))")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_4(self):
+    def test_problem_04(self):
         prover = Prover()
         prover.add_formula("iff(F, G)")
         prover.add_formula("or(F, G)")
         prover.add_goal("and(F, G)")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_5(self):
+    def test_problem_05(self):
         prover = Prover()
         prover.add_formula("iff(not(B), Z)")
         prover.add_formula("if(N, B)")
@@ -44,14 +44,14 @@ def test_problem_5(self):
         prover.add_goal("not(H)")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_6(self):
+    def test_problem_06(self):
         prover = Prover()
         prover.add_formula("iff(A, B)")
         prover.add_formula("iff(B, not(C))")
         prover.add_goal("not(iff(A, C))")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_7(self):
+    def test_problem_07(self):
         prover = Prover()
         prover.add_formula("if(M, I)")
         prover.add_formula("and(not(I), L)")
@@ -59,7 +59,7 @@ def test_problem_7(self):
         prover.add_goal("B")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_8(self):
+    def test_problem_08(self):
         prover = Prover()
         prover.add_formula("or(Q, iff(J, D))")
         prover.add_formula("not(D)")
@@ -67,7 +67,7 @@ def test_problem_8(self):
         prover.add_goal("Q")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_9(self):
+    def test_problem_09(self):
         prover = Prover()
         prover.add_formula("or(A, B)")
         prover.add_formula("or(not(B), C)")
diff --git a/tests/bram_testcases/prop_logic_proofs_ii_tester.py b/tests/bram_testcases/test_prop_logic_proofs_ii.py
similarity index 91%
rename from tests/bram_testcases/prop_logic_proofs_ii_tester.py
rename to tests/bram_testcases/test_prop_logic_proofs_ii.py
index c1e0cef..b61d2ba 100644
--- a/tests/bram_testcases/prop_logic_proofs_ii_tester.py
+++ b/tests/bram_testcases/test_prop_logic_proofs_ii.py
@@ -5,40 +5,40 @@
 from forseti.prover import Prover
 
 
-class PropLogicProofsIITester(unittest.TestCase):
-    def test_problem_1(self):
+class TestPropLogicProofsII(unittest.TestCase):
+    def test_problem_01(self):
         prover = Prover()
         prover.add_formula("not(A)")
         prover.add_goal("if(A, B)")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_2(self):
+    def test_problem_02(self):
         prover = Prover()
         prover.add_formula("A")
         prover.add_goal("if(B, A)")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_3(self):
+    def test_problem_03(self):
         prover = Prover()
         prover.add_formula("if(A, if(B, C))")
         prover.add_goal("if(B, if(A, C))")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_4(self):
+    def test_problem_04(self):
         prover = Prover()
         prover.add_formula("if(A, B)")
         prover.add_formula("if(A, C)")
         prover.add_goal("if(A, and(B, C))")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_5(self):
+    def test_problem_05(self):
         prover = Prover()
         prover.add_formula("if(A, C)")
         prover.add_formula("if(B, C)")
         prover.add_goal("if(or(A, B), C)")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_6(self):
+    def test_problem_06(self):
         prover = Prover()
         prover.add_formula("or(A, and(B, C))")
         prover.add_formula("if(A, D)")
@@ -46,7 +46,7 @@ def test_problem_6(self):
         prover.add_goal("C")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_7(self):
+    def test_problem_07(self):
         prover = Prover()
         prover.add_formula("A")
         prover.add_formula("iff(A, B)")
@@ -54,14 +54,14 @@ def test_problem_7(self):
         prover.add_goal("not(C)")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_8(self):
+    def test_problem_08(self):
         prover = Prover()
         prover.add_formula("if(or(A, B), if(C, D))")
         prover.add_formula("if(or(not(D), E), and(A, C))")
         prover.add_goal("D")
         self.assertTrue(prover.run_prover())
 
-    def test_problem_9(self):
+    def test_problem_09(self):
         prover = Prover()
         prover.add_formula("if(A, B)")
         prover.add_formula("if(A, not(B))")
@@ -146,12 +146,15 @@ def test_problem_19(self):
         self.assertTrue(prover.run_prover())
 
     def test_problem_20(self):
+        """
+        While the PDF claims all arguments are "valid", this one is not
+        """
         prover = Prover()
         prover.add_formula("if(or(not(A), B), not(and(C, D)))")
         prover.add_formula("if(and(A, C), E)")
         prover.add_formula("and(A, not(E))")
         prover.add_goal("not(or(D, E))")
-        self.assertTrue(prover.run_prover())
+        self.assertFalse(prover.run_prover())
 
 
 if __name__ == "__main__":
diff --git a/tests/parsers/functional_tester.py b/tests/parsers/test_functional.py
similarity index 100%
rename from tests/parsers/functional_tester.py
rename to tests/parsers/test_functional.py
diff --git a/tests/parsers/prefix_tester.py b/tests/parsers/test_prefix.py
similarity index 100%
rename from tests/parsers/prefix_tester.py
rename to tests/parsers/test_prefix.py
diff --git a/tests/converter_tester.py b/tests/test_converter.py
similarity index 98%
rename from tests/converter_tester.py
rename to tests/test_converter.py
index f5d1274..b0b2250 100644
--- a/tests/converter_tester.py
+++ b/tests/test_converter.py
@@ -5,7 +5,7 @@
 from forseti import converter, parser
 
 
-class ConverterTester(unittest.TestCase):
+class TestConverter(unittest.TestCase):
     def test_cnf_converter_symbol(self):
         statement = Symbol("a")
         statement = converter.convert_formula(statement)
diff --git a/tests/formula_tester.py b/tests/test_formula.py
similarity index 99%
rename from tests/formula_tester.py
rename to tests/test_formula.py
index 602b787..7e19af6 100644
--- a/tests/formula_tester.py
+++ b/tests/test_formula.py
@@ -7,7 +7,7 @@
 from forseti.formula import Formula, Symbol, LogicalOperator, Not, And, Or, If, Iff
 
 
-class FormulaTester(unittest.TestCase):
+class TestFormula(unittest.TestCase):
     def test_formula_str(self):
         with self.assertRaises(NotImplementedError):
             str(Formula())
diff --git a/tests/prover_tester.py b/tests/test_prover.py
similarity index 96%
rename from tests/prover_tester.py
rename to tests/test_prover.py
index b7bb08e..8b93fea 100644
--- a/tests/prover_tester.py
+++ b/tests/test_prover.py
@@ -4,7 +4,7 @@
 from forseti.prover import Prover
 
 
-class ProverTester(unittest.TestCase):
+class TestProver(unittest.TestCase):
     def test_get_proof(self):
         prover = Prover()
         prover.add_formula("and(a,b)")
diff --git a/tests/util_tester.py b/tests/test_util.py
similarity index 98%
rename from tests/util_tester.py
rename to tests/test_util.py
index e1aa363..65302f7 100644
--- a/tests/util_tester.py
+++ b/tests/test_util.py
@@ -6,7 +6,7 @@
 import forseti.util as util
 
 
-class UtilTester(unittest.TestCase):
+class TestUtil(unittest.TestCase):
     def test_print_cnf_list(self):
         cnf = list()
         a_symbol = Symbol("a")