diff --git a/hw2/gameTree.png b/hw2/gameTree.png
new file mode 100644
index 0000000..82a0f81
Binary files /dev/null and b/hw2/gameTree.png differ
diff --git a/hw2/hw2.pdf b/hw2/hw2.pdf
new file mode 100644
index 0000000..c62b729
Binary files /dev/null and b/hw2/hw2.pdf differ
diff --git a/hw2/ints/__pycache__/grader_util.cpython-312.pyc b/hw2/ints/__pycache__/grader_util.cpython-312.pyc
new file mode 100644
index 0000000..ab49d9b
Binary files /dev/null and b/hw2/ints/__pycache__/grader_util.cpython-312.pyc differ
diff --git a/hw2/ints/__pycache__/logic.cpython-312.pyc b/hw2/ints/__pycache__/logic.cpython-312.pyc
new file mode 100644
index 0000000..babe26b
Binary files /dev/null and b/hw2/ints/__pycache__/logic.cpython-312.pyc differ
diff --git a/hw2/ints/__pycache__/submission.cpython-312.pyc b/hw2/ints/__pycache__/submission.cpython-312.pyc
new file mode 100644
index 0000000..edd0a6f
Binary files /dev/null and b/hw2/ints/__pycache__/submission.cpython-312.pyc differ
diff --git a/hw2/ints/examples.py b/hw2/ints/examples.py
new file mode 100644
index 0000000..889162e
--- /dev/null
+++ b/hw2/ints/examples.py
@@ -0,0 +1,26 @@
+from logic import *
+
+
+# Sentence: "If it's rains, it's wet".
+def rain_wet():
+    Rain = Atom('Rain')  # whether it's raining
+    Wet = Atom('Wet')  # whether it's wet
+    return Implies(Rain, Wet)
+
+
+# Sentence: "There is a light that shines."
+def light_shines():
+    def Light(x): return Atom('Light', x)  # whether x is lit
+
+    def Shines(x): return Atom('Shines', x)  # whether x is shining
+
+    return Exists('$x', And(Light('$x'), Shines('$x')))
+
+
+# Defining Parent in terms of Child.
+def parent_child():
+    def Parent(x, y): return Atom('Parent', x, y)  # whether x has a parent y
+
+    def Child(x, y): return Atom('Child', x, y)  # whether x has a child y
+
+    return Forall('$x', Forall('$y', Equiv(Parent('$x', '$y'), Child('$y', '$x'))))
diff --git a/hw2/ints/grader.py b/hw2/ints/grader.py
new file mode 100644
index 0000000..3f9542d
--- /dev/null
+++ b/hw2/ints/grader.py
@@ -0,0 +1,109 @@
+#!/usr/bin/env python3
+
+from logic import *
+
+import pickle, gzip, os, random
+import grader_util
+
+grader = grader_util.Grader()
+submission = grader.load('submission')
+
+# name: name of this formula (used to load the models)
+# predForm: the formula predicted in the submission
+# preconditionForm: only consider models such that preconditionForm is true
+def checkFormula(name, predForm, preconditionForm=None, handle_grader=True):
+    filename = os.path.join('models', name + '.pklz')
+    objects, targetModels = pickle.load(gzip.open(filename))
+    # If preconditionion exists, change the formula to
+    preconditionPredForm = And(preconditionForm, predForm) if preconditionForm else predForm
+    predModels = performModelChecking([preconditionPredForm], findAll=True, objects=objects)
+    ok = True
+    def hashkey(model): return tuple(sorted(str(atom) for atom in model))
+    targetModelSet = set(hashkey(model) for model in targetModels)
+    predModelSet = set(hashkey(model) for model in predModels)
+    for model in targetModels:
+        if hashkey(model) not in predModelSet:
+            if handle_grader:
+                grader.fail("Your formula (%s) says the following model is FALSE, but it should be TRUE:" % predForm)
+            ok = False
+            printModel(model)
+            return ok
+    for model in predModels:
+        if hashkey(model) not in targetModelSet:
+            if handle_grader:
+                grader.fail("Your formula (%s) says the following model is TRUE, but it should be FALSE:" % predForm)
+            ok = False
+            printModel(model)
+            return ok
+    if handle_grader:
+        grader.add_message('You matched the %d models' % len(targetModels))
+        grader.add_message('Example model: %s' % rstr(random.choice(targetModels)))
+        grader.assign_full_credit()
+    return ok
+
+# name: name of this formula set (used to load the models)
+# predForms: formulas predicted in the submission
+# predQuery: query formula predicted in the submission
+def addParts(name, numForms, predictionFunc):
+    # part is either an individual formula (0:numForms), all (combine everything)
+    def check(part):
+        predForms, predQuery = predictionFunc()
+        if len(predForms) < numForms:
+            grader.fail("Wanted %d formulas, but got %d formulas:" % (numForms, len(predForms)))
+            for form in predForms: print(('-', form))
+            return
+        if part == 'all':
+            checkFormula(name + '-all', AndList(predForms))
+        elif part == 'run':
+            # Actually run it on a knowledge base
+            kb = createModelCheckingKB()
+
+            # Need to tell the KB about the objects to do model checking
+            filename = os.path.join('models', name + '-all.pklz')
+            objects, targetModels = pickle.load(gzip.open(filename))
+            for obj in objects:
+                kb.tell(Atom('Object', obj))
+
+            # Add the formulas
+            for predForm in predForms:
+                response = kb.tell(predForm)
+                showKBResponse(response)
+                grader.require_is_true(response.status in [CONTINGENT, ENTAILMENT])
+            response = kb.ask(predQuery)
+            showKBResponse(response)
+
+        else:  # Check the part-th formula
+            checkFormula(name + '-' + str(part), predForms[part])
+
+    def createCheck(part): return lambda : check(part)  # To create closure
+
+    # run part-all once first for combined correctness, if true, trivially assign full score for all subparts
+    # this is to account for student adding formulas to the list in different orders but still get
+    # the combined preds correct.
+    all_is_correct = False
+    try:
+        predForms, predQuery = predictionFunc()
+        all_is_correct = checkFormula(name + '-all', AndList(predForms), handle_grader=False)
+    except BaseException:
+        pass
+
+    for part in list(range(numForms)) + ['all', 'run']:
+        if part == 'all':
+            description = 'test implementation of %s for %s' % (part, name)
+        elif part == 'run':
+            description = 'test implementation of %s for %s' % (part, name)
+        else:
+            description = 'test implementation of statement %s for %s' % (part, name)
+        if all_is_correct and not part in ['all', 'run']:
+            grader.add_basic_part(name + '-' + str(part), lambda : grader.assign_full_credit(), max_points=1, max_seconds=10000, description=description)
+        else:
+            grader.add_basic_part(name + '-' + str(part), createCheck(part), max_points=1, max_seconds=10000, description=description)
+
+############################################################
+# Problem 4: odd and even integers
+
+# Add 5a-[0-5], 5a-all, 5a-run
+addParts('4a', 6, submission.ints)
+
+
+grader.grade()
diff --git a/hw2/ints/grader_util.py b/hw2/ints/grader_util.py
new file mode 100644
index 0000000..c28691a
--- /dev/null
+++ b/hw2/ints/grader_util.py
@@ -0,0 +1,448 @@
+"""
+Library to do grading of Python programs.
+Usage (see grader.py):
+
+    # create a grader
+    grader = Grader("Name of assignment")
+
+    # add a basic test
+    grader.addBasicPart(number, grade_func, max_points, max_seconds, description="a basic test")
+
+    # add a hidden test
+    grader.addHiddenPart(number, grade_func, max_points, max_seconds, description="a hidden test")
+
+    # add a manual grading part
+    grader.addManualPart(number, grade_func, max_points, description="written problem")
+
+    # run grading
+    grader.grade()
+"""
+
+import argparse
+import datetime
+import gc
+import json
+import os
+import signal
+import sys
+import traceback
+
+default_max_seconds = 5  # 5 second
+TOLERANCE = 1e-4  # For measuring whether two floats are equal
+
+BASIC_MODE = 'basic'  # basic
+AUTO_MODE = 'auto'  # basic + hidden
+ALL_MODE = 'all'  # basic + hidden + manual
+
+
+# When reporting stack traces as feedback, ignore parts specific to the grading
+# system.
+def is_traceback_item_grader(item):
+    return item[0].endswith('graderUtil.py')
+
+
+def is_collection(x):
+    return isinstance(x, list) or isinstance(x, tuple)
+
+
+# Return whether two answers are equal.
+def is_equal(true_answer, pred_answer, tolerance=TOLERANCE):
+    # Handle floats specially
+    if isinstance(true_answer, float) or isinstance(pred_answer, float):
+        return abs(true_answer - pred_answer) < tolerance
+    # Recurse on collections to deal with floats inside them
+    if is_collection(true_answer) and is_collection(pred_answer) and len(true_answer) == len(pred_answer):
+        for a, b in zip(true_answer, pred_answer):
+            if not is_equal(a, b):
+                return False
+        return True
+    if isinstance(true_answer, dict) and isinstance(pred_answer, dict):
+        if len(true_answer) != len(pred_answer):
+            return False
+        for k, v in list(true_answer.items()):
+            if not is_equal(pred_answer.get(k), v):
+                return False
+        return True
+
+    # Numpy array comparison
+    if type(true_answer).__name__ == 'ndarray':
+        import numpy as np
+        if isinstance(true_answer, np.ndarray) and isinstance(pred_answer, np.ndarray):
+            if true_answer.shape != pred_answer.shape:
+                return False
+            for a, b in zip(true_answer, pred_answer):
+                if not is_equal(a, b):
+                    return False
+            return True
+
+    # Do normal comparison
+    return true_answer == pred_answer
+
+
+# Run a function, timing out after max_seconds.
+class TimeoutFunctionException(Exception):
+    pass
+
+
+class TimeoutFunction:
+    def __init__(self, function, max_seconds):
+        self.max_seconds = max_seconds
+        self.function = function
+
+    @staticmethod
+    def handle_max_seconds(signum, frame):
+        print('TIMEOUT!')
+        raise TimeoutFunctionException()
+
+    def __call__(self, *args):
+        if os.name == 'nt':
+            # Windows does not have signal.SIGALRM
+            # Will not stop after max_seconds second but can still throw an exception
+            time_start = datetime.datetime.now()
+            result = self.function(*args)
+            time_end = datetime.datetime.now()
+            if time_end - time_start > datetime.timedelta(seconds=self.max_seconds + 1):
+                raise TimeoutFunctionException()
+            return result
+            # End modification for Windows here
+        signal.signal(signal.SIGALRM, self.handle_max_seconds)
+        signal.alarm(self.max_seconds + 1)
+        result = self.function(*args)
+        signal.alarm(0)
+        return result
+
+
+class Part:
+    def __init__(self, number, grade_func, max_points, max_seconds, extra_credit, description, basic):
+        if not isinstance(number, str):
+            raise Exception("Invalid number: %s" % number)
+        if grade_func is not None and not callable(grade_func):
+            raise Exception("Invalid grade_func: %s" % grade_func)
+        if not isinstance(max_points, int) and not isinstance(max_points, float):
+            raise Exception("Invalid max_points: %s" % max_points)
+        if max_seconds is not None and not isinstance(max_seconds, int):
+            raise Exception("Invalid max_seconds: %s" % max_seconds)
+        if not description:
+            print('ERROR: description required for part {}'.format(number))
+        # Specification of part
+        self.number = number  # Unique identifier for this part.
+        self.description = description  # Description of this part
+        self.grade_func = grade_func  # Function to call to do grading
+        self.max_points = max_points  # Maximum number of points attainable on this part
+        self.max_seconds = max_seconds  # Maximum allowed time that the student's code can take (in seconds)
+        self.extra_credit = extra_credit  # Whether this is an extra credit problem
+        self.basic = basic
+        # Grading the part
+        self.points = 0
+        self.side = None  # Side information
+        self.seconds = 0
+        self.messages = []
+        self.failed = False
+
+    def fail(self):
+        self.failed = True
+
+    def is_basic(self):
+        return self.grade_func is not None and self.basic
+
+    def is_hidden(self):
+        return self.grade_func is not None and not self.basic
+
+    def is_auto(self):
+        return self.grade_func is not None
+
+    def is_manual(self):
+        return self.grade_func is None
+
+
+class Grader:
+    def __init__(self, args=None):
+        if args is None:
+            args = sys.argv
+        self.parts = []  # Parts (to be added)
+        self.useSolution = False  # Set to true if we are actually evaluating the hidden test cases
+
+        parser = argparse.ArgumentParser()
+        parser.add_argument('--js', action='store_true', help='Write JS file with information about this assignment')
+        parser.add_argument('--json', action='store_true',
+                            help='Write JSON file with information about this assignment')
+        parser.add_argument('--summary', action='store_true', help='Don\'t actually run code')
+        parser.add_argument('remainder', nargs=argparse.REMAINDER)
+        self.params = parser.parse_args(args[1:])
+
+        args = self.params.remainder
+        if len(args) < 1:
+            self.mode = AUTO_MODE
+            self.selectedPartName = None
+        else:
+            if args[0] in [BASIC_MODE, AUTO_MODE, ALL_MODE]:
+                self.mode = args[0]
+                self.selectedPartName = None
+            else:
+                self.mode = AUTO_MODE
+                self.selectedPartName = args[0]
+
+        self.messages = []  # General messages
+        self.currentPart = None  # Which part we're grading
+        self.fatalError = False  # Set this if we should just stop immediately
+
+    def add_basic_part(self, number, grade_func, max_points=1, max_seconds=default_max_seconds, extra_credit=False,
+                       description=""):
+        """Add a basic test case. The test will be visible to students."""
+        self.assert_new_number(number)
+        part = Part(number, grade_func, max_points, max_seconds, extra_credit, description, basic=True)
+        self.parts.append(part)
+
+    def add_hidden_part(self, number, grade_func, max_points=1, max_seconds=default_max_seconds, extra_credit=False,
+                        description=""):
+        """Add a hidden test case. The output should NOT be visible to students
+        and so should be inside a BEGIN_HIDE block."""
+        self.assert_new_number(number)
+        part = Part(number, grade_func, max_points, max_seconds, extra_credit, description, basic=False)
+        self.parts.append(part)
+
+    def add_manual_part(self, number, max_points, extra_credit=False, description=""):
+        """Add a manual part."""
+        self.assert_new_number(number)
+        part = Part(number, None, max_points, None, extra_credit, description, basic=False)
+        self.parts.append(part)
+
+    def assert_new_number(self, number):
+        if number in [part.number for part in self.parts]:
+            raise Exception("Part number %s already exists" % number)
+
+    # Try to load the module (submission from student).
+    def load(self, module_name):
+        try:
+            return __import__(module_name)
+        except Exception as e:
+            self.fail("Threw exception when importing '%s': %s" % (module_name, e))
+            self.fatalError = True
+            return None
+        except:
+            self.fail("Threw exception when importing '%s'" % module_name)
+            self.fatalError = True
+            return None
+
+    def grade_part(self, part):
+        print('----- START PART %s%s: %s' % (
+            part.number, ' (extra credit)' if part.extra_credit else '', part.description))
+        self.currentPart = part
+
+        start_time = datetime.datetime.now()
+        try:
+            TimeoutFunction(part.grade_func, part.max_seconds)()  # Call the part's function
+        except KeyboardInterrupt:
+            raise
+        except MemoryError:
+            signal.alarm(0)
+            gc.collect()
+            self.fail('Memory limit exceeded.')
+        except TimeoutFunctionException:
+            signal.alarm(0)
+            self.fail('Time limit (%s seconds) exceeded.' % part.max_seconds)
+        except Exception as e:
+            signal.alarm(0)
+            self.fail('Exception thrown: %s -- %s' % (str(type(e)), str(e)))
+            self.print_exception()
+        except SystemExit:
+            # Catch SystemExit raised by exit(), quit() or sys.exit()
+            # This class is not a subclass of Exception and we don't
+            # expect students to raise it.
+            self.fail('Unexpected exit.')
+            self.print_exception()
+        end_time = datetime.datetime.now()
+        part.seconds = (end_time - start_time).seconds
+        ###### quick fix to pacman problem 4 ######
+        if part.seconds > part.max_seconds:
+            signal.alarm(0)
+            self.fail('Time limit (%s seconds) exceeded.' % part.max_seconds)
+        ###### quick fix to pacman problem 4 ######
+        if part.is_hidden() and not self.useSolution:
+            display_points = '???/%s points (hidden test ungraded)' % part.max_points
+        else:
+            display_points = '%s/%s points' % (part.points, part.max_points)
+        print('----- END PART %s [%s]' % (
+            part.number, display_points))
+        print()
+
+    def get_selected_parts(self):
+        parts = []
+        for part in self.parts:
+            if self.selectedPartName is not None and self.selectedPartName != part.number:
+                continue
+            if self.mode == BASIC_MODE:
+                if part.is_basic():
+                    parts.append(part)
+            elif self.mode == AUTO_MODE:
+                if part.is_auto():
+                    parts.append(part)
+            elif self.mode == ALL_MODE:
+                parts.append(part)
+            else:
+                raise Exception("Invalid mode: {}".format(self.mode))
+        return parts
+
+    def grade(self):
+        parts = self.get_selected_parts()
+
+        result = {'mode': self.mode}
+
+        # Grade it!
+        if not self.params.summary and not self.fatalError:
+            print('========== START GRADING')
+            for part in parts:
+                self.grade_part(part)
+
+            # When students have it (not useSolution), only include basic tests.
+            active_parts = [part for part in parts if self.useSolution or part.basic]
+
+            total_points = sum(part.points for part in active_parts if not part.extra_credit)
+            extra_credit = sum(part.points for part in active_parts if part.extra_credit)
+            max_total_points = sum(part.max_points for part in active_parts if not part.extra_credit)
+            max_extra_credit = sum(part.max_points for part in active_parts if part.extra_credit)
+
+            print('========== END GRADING [%s/%s points + %s/%s extra credit]' %
+                  (total_points, max_total_points, extra_credit, max_extra_credit))
+
+        result_parts = []
+        leaderboard = []
+        for part in parts:
+            r = {'number': part.number, 'name': part.description}
+
+            if self.params.summary:
+                # Just print out specification of the part
+                r['description'] = part.description
+                r['max_seconds'] = part.max_seconds
+                r['max_points'] = part.max_points
+                r['extra_credit'] = part.extra_credit
+                r['basic'] = part.basic
+            else:
+                r['score'] = part.points
+                # Force max_score to be 0 for extra credits for displaying correct total points on Gradescope
+                r['max_score'] = 0 if (part.extra_credit and self.mode == AUTO_MODE) else part.max_points
+                r["visibility"] = "after_published" if part.is_hidden() else "visible"
+                r['seconds'] = part.seconds
+                if part.side is not None:
+                    r['side'] = part.side
+                r['output'] = "\n".join(part.messages)
+
+                if part.side is not None:
+                    for k in part.side:
+                        leaderboard.append({"name": k, "value": part.side[k]})
+            result_parts.append(r)
+        result['tests'] = result_parts
+        result['leaderboard'] = leaderboard
+
+        self.output(self.mode, result)
+
+        def display(name, select_extra_credit):
+            parts_to_display = [p for p in self.parts if p.extra_credit == select_extra_credit]
+            max_basic_points = sum(p.max_points for p in parts_to_display if p.is_basic())
+            max_hidden_points = sum(p.max_points for p in parts_to_display if p.is_hidden())
+            max_manual_points = sum(p.max_points for p in parts_to_display if p.is_manual())
+            max_total_points_found = max_basic_points + max_hidden_points + max_manual_points
+            print("Total %s (basic auto/coding + hidden auto/coding + manual/written): %d + %d + %d = %d" %
+                  (name, max_basic_points, max_hidden_points, max_manual_points, max_total_points_found))
+            if not select_extra_credit and max_total_points_found != 75:
+                print('WARNING: max_total_points = {} is not 75'.format(max_total_points_found))
+
+        if self.params.summary:
+            display('points', False)
+            display('extra credit', True)
+
+    def output(self, mode, result):
+        if self.params.json:
+            path = 'grader-{}.json'.format(mode)
+            with open(path, 'w') as out:
+                print(json.dumps(result), file=out)
+            print('Wrote to %s' % path)
+        if self.params.js:
+            path = 'grader-{}.js'.format(mode)
+            with open(path, 'w') as out:
+                print('var ' + mode + 'Result = ' + json.dumps(result) + ';', file=out)
+            print('Wrote to %s' % path)
+
+    # Called by the grader to modify state of the current part
+
+    def add_points(self, amt):
+        self.currentPart.points += amt
+
+    def assign_full_credit(self):
+        if not self.currentPart.failed:
+            self.currentPart.points = self.currentPart.max_points
+        return True
+
+    def assign_partial_credit(self, credit):
+        self.currentPart.points = credit
+        return True
+
+    def set_side(self, side):
+        self.currentPart.side = side
+
+    @staticmethod
+    def truncate_string(string, length=200):
+        if len(string) <= length:
+            return string
+        else:
+            return string[:length] + '...'
+
+    def require_is_numeric(self, answer):
+        if isinstance(answer, int) or isinstance(answer, float):
+            return self.assign_full_credit()
+        else:
+            return self.fail("Expected either int or float, but got '%s'" % self.truncate_string(answer))
+
+    def require_is_one_of(self, true_answers, pred_answer):
+        if pred_answer in true_answers:
+            return self.assign_full_credit()
+        else:
+            return self.fail("Expected one of %s, but got '%s'" % (
+                self.truncate_string(true_answers), self.truncate_string(pred_answer)))
+
+    def require_is_equal(self, true_answer, pred_answer, tolerance=TOLERANCE):
+        if is_equal(true_answer, pred_answer, tolerance):
+            return self.assign_full_credit()
+        else:
+            return self.fail("Expected '%s', but got '%s'" % (
+                self.truncate_string(str(true_answer)), self.truncate_string(str(pred_answer))))
+
+    def require_is_less_than(self, less_than_quantity, pred_answer):
+        if pred_answer < less_than_quantity:
+            return self.assign_full_credit()
+        else:
+            return self.fail("Expected to be < %f, but got %f" % (less_than_quantity, pred_answer))
+
+    def require_is_greater_than(self, greater_than_quantity, pred_answer):
+        if pred_answer > greater_than_quantity:
+            return self.assign_full_credit()
+        else:
+            return self.fail("Expected to be > %f, but got %f" %
+                             (greater_than_quantity, pred_answer))
+
+    def require_is_true(self, pred_answer):
+        if pred_answer:
+            return self.assign_full_credit()
+        else:
+            return self.fail("Expected to be true, but got false")
+
+    def fail(self, message):
+        print('FAIL:', message)
+        self.add_message(message)
+        if self.currentPart:
+            self.currentPart.points = 0
+            self.currentPart.fail()
+        return False
+
+    def print_exception(self):
+        tb = [item for item in traceback.extract_tb(sys.exc_info()[2]) if not is_traceback_item_grader(item)]
+        for item in traceback.format_list(tb):
+            self.fail('%s' % item)
+
+    def add_message(self, message):
+        if not self.useSolution:
+            print(message)
+        if self.currentPart:
+            self.currentPart.messages.append(message)
+        else:
+            self.messages.append(message)
diff --git a/hw2/ints/logic.py b/hw2/ints/logic.py
new file mode 100644
index 0000000..ed99c9d
--- /dev/null
+++ b/hw2/ints/logic.py
@@ -0,0 +1,1084 @@
+# Simple logical inference system: resolution and model checking for first-order logic.
+# @author Percy Liang
+
+import collections
+
+
+# Recursively apply str inside map
+def rstr(x):
+    if isinstance(x, tuple): return str(tuple(map(rstr, x)))
+    if isinstance(x, list): return str(list(map(rstr, x)))
+    if isinstance(x, set): return str(set(map(rstr, x)))
+    if isinstance(x, dict):
+        newx = {}
+        for k, v in list(x.items()):
+            newx[rstr(k)] = rstr(v)
+        return str(newx)
+    return str(x)
+
+
+class Expression:
+    # Helper functions used by subclasses.
+    def ensureType(self, arg, wantedType):
+        if not isinstance(arg, wantedType):
+            raise Exception('%s: wanted %s, but got %s' % (self.__class__.__name__, wantedType, arg))
+        return arg
+
+    def ensureFormula(self, arg):
+        return self.ensureType(arg, Formula)
+
+    def ensureFormulas(self, args):
+        for arg in args: self.ensureFormula(arg)
+        return args
+
+    def isa(self, wantedType):
+        return isinstance(self, wantedType)
+
+    def join(self, args):
+        return ','.join(str(arg) for arg in args)
+
+    def __eq__(self, other):
+        return str(self) == str(other)
+
+    def __hash__(self):
+        return hash(str(self))
+
+    # Cache the string to be more efficient
+    def __repr__(self):
+        if not self.strRepn: self.strRepn = self.computeStrRepn()
+        return self.strRepn
+
+
+# A Formula represents a truth value.
+class Formula(Expression): pass
+
+
+# A Term coresponds to an object.
+class Term(Expression): pass
+
+
+# Variable symbol (must start with '$')
+# Example: $x
+class Variable(Term):
+    def __init__(self, name):
+        if not name.startswith('$'): raise Exception('Variable must start with "$", but got %s' % name)
+        self.name = name
+        self.strRepn = None
+
+    def computeStrRepn(self): return self.name
+
+
+# Constant symbol (must be uncapitalized)
+# Example: john
+class Constant(Term):
+    def __init__(self, name):
+        if not name[0].islower(): raise Exception('Constants must start with a lowercase letter, but got %s' % name)
+        self.name = name
+        self.strRepn = None
+
+    def computeStrRepn(self): return self.name
+
+
+# Predicate symbol (must be capitalized) applied to arguments.
+# Example: LivesIn(john, palo_alto)
+class Atom(Formula):
+    def __init__(self, name, *args):
+        if not name[0].isupper(): raise Exception('Predicates must start with a uppercase letter, but got %s' % name)
+        self.name = name
+        self.args = list(map(toExpr, args))
+        self.strRepn = None
+
+    def computeStrRepn(self):
+        if len(self.args) == 0: return self.name
+        return self.name + '(' + self.join(self.args) + ')'
+
+
+def toExpr(x):
+    if isinstance(x, str):
+        if x.startswith('$'): return Variable(x)
+        return Constant(x)
+    return x
+
+
+AtomFalse = False
+AtomTrue = True
+
+
+# Example: Not(Rain)
+class Not(Formula):
+    def __init__(self, arg):
+        self.arg = self.ensureFormula(arg)
+        self.strRepn = None
+
+    def computeStrRepn(self): return 'Not(' + str(self.arg) + ')'
+
+
+# Example: And(Rain,Snow)
+class And(Formula):
+    def __init__(self, arg1, arg2):
+        self.arg1 = self.ensureFormula(arg1)
+        self.arg2 = self.ensureFormula(arg2)
+        self.strRepn = None
+
+    def computeStrRepn(self): return 'And(' + str(self.arg1) + ',' + str(self.arg2) + ')'
+
+
+# Example: Or(Rain,Snow)
+class Or(Formula):
+    def __init__(self, arg1, arg2):
+        self.arg1 = self.ensureFormula(arg1)
+        self.arg2 = self.ensureFormula(arg2)
+        self.strRepn = None
+
+    def computeStrRepn(self): return 'Or(' + str(self.arg1) + ',' + str(self.arg2) + ')'
+
+
+# Example: Implies(Rain,Wet)
+class Implies(Formula):
+    def __init__(self, arg1, arg2):
+        self.arg1 = self.ensureFormula(arg1)
+        self.arg2 = self.ensureFormula(arg2)
+        self.strRepn = None
+
+    def computeStrRepn(self): return 'Implies(' + str(self.arg1) + ',' + str(self.arg2) + ')'
+
+
+# Example: Exists($x,Lives(john, $x))
+class Exists(Formula):
+    def __init__(self, var, body):
+        self.var = self.ensureType(toExpr(var), Variable)
+        self.body = self.ensureFormula(body)
+        self.strRepn = None
+
+    def computeStrRepn(self): return 'Exists(' + str(self.var) + ',' + str(self.body) + ')'
+
+
+# Example: Forall($x,Implies(Human($x),Alive($x)))
+class Forall(Formula):
+    def __init__(self, var, body):
+        self.var = self.ensureType(toExpr(var), Variable)
+        self.body = self.ensureFormula(body)
+        self.strRepn = None
+
+    def computeStrRepn(self): return 'Forall(' + str(self.var) + ',' + str(self.body) + ')'
+
+
+# Take a list of conjuncts / disjuncts and return a formula
+def AndList(forms):
+    result = AtomTrue
+    for form in forms:
+        result = And(result, form) if result != AtomTrue else form
+    return result
+
+
+def OrList(forms):
+    result = AtomFalse
+    for form in forms:
+        result = Or(result, form) if result != AtomFalse else form
+    return result
+
+
+# Return list of conjuncts of |form|.
+# Example: And(And(A, Or(B, C)), Not(D)) => [A, Or(B, C), Not(D)]
+def flattenAnd(form):
+    if form.isa(And):
+        return flattenAnd(form.arg1) + flattenAnd(form.arg2)
+    else:
+        return [form]
+
+
+# Return list of disjuncts of |form|.
+# Example: Or(Or(A, And(B, C)), D) => [A, And(B, C), Not(D)]
+def flattenOr(form):
+    if form.isa(Or):
+        return flattenOr(form.arg1) + flattenOr(form.arg2)
+    else:
+        return [form]
+
+
+# Syntactic sugar
+def Equiv(a, b): return And(Implies(a, b), Implies(b, a))
+
+
+def Xor(a, b): return And(Or(a, b), Not(And(a, b)))
+
+
+# Special predicate which is used internally (e.g., in propositionalization).
+def Equals(x, y): return Atom('Equals', x, y)
+
+
+# Given a predicate name (e.g., Parent), return a formula that asserts that
+# that predicate is anti-reflexive
+# (e.g., Not(Parent(x,x))).
+def AntiReflexive(predicate):
+    # return Forall('$x', Not(Atom(predicate, '$x', '$x')))
+    # Force Equals() to be used and show up in the models.
+    return Forall('$x', Forall('$y', Implies(Atom(predicate, '$x', '$y'),
+                                             Not(Equals('$x', '$y')))))
+
+
+############################################################
+# Simple inference rules
+
+# A Rule takes a sequence of argument Formulas and produces a set of result
+# Formulas (possibly [] if the rule doesn't apply).
+class Rule:
+    pass
+
+
+class UnaryRule(Rule):
+    def applyRule(self, form): raise Exception('Override me')
+
+
+class BinaryRule(Rule):
+    def applyRule(self, form1, form2): raise Exception('Override me')
+
+    # Override if rule is symmetric to save a factor of 2.
+    def symmetric(self): return False
+
+
+############################################################
+# Unification
+
+# Mutate |subst| with variable => bindings
+# Return whether unification was successful
+# Assume forms are in CNF.
+# Note: we don't do occurs check because we don't have function symbols.
+def unify(form1, form2, subst):
+    if form1.isa(Variable): return unifyTerms(form1, form2, subst)
+    if form1.isa(Constant): return unifyTerms(form1, form2, subst)
+    if form1.isa(Atom):
+        return form2.isa(Atom) and form1.name == form2.name and len(form1.args) == len(form2.args) and \
+            all(unify(form1.args[i], form2.args[i], subst) for i in range(len(form1.args)))
+    if form1.isa(Not):
+        return form2.isa(Not) and unify(form1.arg, form2.arg, subst)
+    if form1.isa(And):
+        return form2.isa(And) and unify(form1.arg1, form2.arg1, subst) and unify(form1.arg2, form2.arg2, subst)
+    if form1.isa(Or):
+        return form2.isa(Or) and unify(form1.arg1, form2.arg1, subst) and unify(form1.arg2, form2.arg2, subst)
+    raise Exception('Unhandled: %s' % form1)
+
+
+# Follow multiple links to get to x
+def getSubst(subst, x):
+    while True:
+        y = subst.get(x)
+        if y == None: return x
+        x = y
+
+
+def unifyTerms(a, b, subst):
+    # print 'unifyTerms', a, b, rstr(subst)
+    a = getSubst(subst, a)
+    b = getSubst(subst, b)
+    if a == b: return True
+    if a.isa(Variable):
+        subst[a] = b
+    elif b.isa(Variable):
+        subst[b] = a
+    else:
+        return False
+    return True
+
+
+# Assume form in CNF.
+def applySubst(form, subst):
+    if len(subst) == 0: return form
+    if form.isa(Variable):
+        # print 'applySubst', rstr(form), rstr(subst), rstr(subst.get(form, form))
+        # return subst.get(form, form)
+        return getSubst(subst, form)
+    if form.isa(Constant): return form
+    if form.isa(Atom): return Atom(*[form.name] + [applySubst(arg, subst) for arg in form.args])
+    if form.isa(Not): return Not(applySubst(form.arg, subst))
+    if form.isa(And): return And(applySubst(form.arg1, subst), applySubst(form.arg2, subst))
+    if form.isa(Or): return Or(applySubst(form.arg1, subst), applySubst(form.arg2, subst))
+    raise Exception('Unhandled: %s' % form)
+
+
+############################################################
+# Convert to CNF, Resolution rules
+
+def withoutElementAt(items, i): return items[0:i] + items[i + 1:]
+
+
+def negateFormula(item):
+    return item.arg if item.isa(Not) else Not(item)
+
+
+# Given a list of Formulas, return a new list with:
+# - If A and Not(A) exists, return [AtomFalse] for conjunction, [AtomTrue] for disjunction
+# - Remove duplicates
+# - Sort the list
+def reduceFormulas(items, mode):
+    for i in range(len(items)):
+        for j in range(i + 1, len(items)):
+            if negateFormula(items[i]) == items[j]:
+                if mode == And:
+                    return [AtomFalse]
+                elif mode == Or:
+                    return [AtomTrue]
+                else:
+                    raise Exception("Invalid mode: %s" % mode)
+    items = sorted(set(items), key=str)
+    return items
+
+
+# Generate a list of all subexpressions of a formula (including terms).
+# Example:
+# - Input: And(Atom('A', Constant('a')), Atom('B'))
+# - Output: [And(Atom('A', Constant('a')), Atom('B')), Atom('A', Constant('a')), Constant('a'), Atom('B')]
+def allSubexpressions(form):
+    subforms = []
+
+    def recurse(form):
+        subforms.append(form)
+        if form.isa(Variable):
+            pass
+        elif form.isa(Constant):
+            pass
+        elif form.isa(Atom):
+            for arg in form.args: recurse(arg)
+        elif form.isa(Not):
+            recurse(form.arg)
+        elif form.isa(And):
+            recurse(form.arg1); recurse(form.arg2)
+        elif form.isa(Or):
+            recurse(form.arg1); recurse(form.arg2)
+        elif form.isa(Implies):
+            recurse(form.arg1); recurse(form.arg2)
+        elif form.isa(Exists):
+            recurse(form.body)
+        elif form.isa(Forall):
+            recurse(form.body)
+        else:
+            raise Exception("Unhandled: %s" % form)
+
+    recurse(form)
+    return subforms
+
+
+# Return a list of the free variables in |form|.
+def allFreeVars(form):
+    variables = []
+
+    def recurse(form, boundVars):
+        if form.isa(Variable):
+            if form not in boundVars: variables.append(form)
+        elif form.isa(Constant):
+            pass
+        elif form.isa(Atom):
+            for arg in form.args: recurse(arg, boundVars)
+        elif form.isa(Not):
+            recurse(form.arg, boundVars)
+        elif form.isa(And):
+            recurse(form.arg1, boundVars); recurse(form.arg2, boundVars)
+        elif form.isa(Or):
+            recurse(form.arg1, boundVars); recurse(form.arg2, boundVars)
+        elif form.isa(Implies):
+            recurse(form.arg1, boundVars); recurse(form.arg2, boundVars)
+        elif form.isa(Exists):
+            recurse(form.body, boundVars + [form.var])
+        elif form.isa(Forall):
+            recurse(form.body, boundVars + [form.var])
+        else:
+            raise Exception("Unhandled: %s" % form)
+
+    recurse(form, [])
+    return variables
+
+
+# Return |form| with all free occurrences of |var| replaced with |obj|.
+def substituteFreeVars(form, var, obj):
+    def recurse(form, boundVars):
+        if form.isa(Variable):
+            if form == var: return obj
+            return form
+        elif form.isa(Constant):
+            return form
+        elif form.isa(Atom):
+            return Atom(*[form.name] + [recurse(arg, boundVars) for arg in form.args])
+        elif form.isa(Not):
+            return Not(recurse(form.arg, boundVars))
+        elif form.isa(And):
+            return And(recurse(form.arg1, boundVars), recurse(form.arg2, boundVars))
+        elif form.isa(Or):
+            return Or(recurse(form.arg1, boundVars), recurse(form.arg2, boundVars))
+        elif form.isa(Implies):
+            return Implies(recurse(form.arg1, boundVars), recurse(form.arg2, boundVars))
+        elif form.isa(Exists):
+            if form.var == var: return form  # Don't substitute inside
+            return Exists(form.var, recurse(form.body, boundVars + [form.var]))
+        elif form.isa(Forall):
+            if form.var == var: return form  # Don't substitute inside
+            return Forall(form.var, recurse(form.body, boundVars + [form.var]))
+        else:
+            raise Exception("Unhandled: %s" % form)
+
+    return recurse(form, [])
+
+
+def allConstants(form):
+    return [x for x in allSubexpressions(form) if x.isa(Constant)]
+
+
+class ToCNFRule(UnaryRule):
+    def __init__(self):
+        # For standardizing variables.
+        # For each existing variable name, the number of times it has occurred
+        self.varCounts = collections.Counter()
+
+    def applyRule(self, form):
+        newForm = form
+
+        # Step 1: remove implications
+        def removeImplications(form):
+            if form.isa(Atom): return form
+            if form.isa(Not): return Not(removeImplications(form.arg))
+            if form.isa(And): return And(removeImplications(form.arg1), removeImplications(form.arg2))
+            if form.isa(Or): return Or(removeImplications(form.arg1), removeImplications(form.arg2))
+            if form.isa(Implies): return Or(Not(removeImplications(form.arg1)), removeImplications(form.arg2))
+            if form.isa(Exists): return Exists(form.var, removeImplications(form.body))
+            if form.isa(Forall): return Forall(form.var, removeImplications(form.body))
+            raise Exception("Unhandled: %s" % form)
+
+        newForm = removeImplications(newForm)
+
+        # Step 2: push negation inwards (de Morgan)
+        def pushNegationInwards(form):
+            if form.isa(Atom): return form
+            if form.isa(Not):
+                if form.arg.isa(Not):  # Double negation
+                    return pushNegationInwards(form.arg.arg)
+                if form.arg.isa(And):  # De Morgan
+                    return Or(pushNegationInwards(Not(form.arg.arg1)), pushNegationInwards(Not(form.arg.arg2)))
+                if form.arg.isa(Or):  # De Morgan
+                    return And(pushNegationInwards(Not(form.arg.arg1)), pushNegationInwards(Not(form.arg.arg2)))
+                if form.arg.isa(Exists):
+                    return Forall(form.arg.var, pushNegationInwards(Not(form.arg.body)))
+                if form.arg.isa(Forall):
+                    return Exists(form.arg.var, pushNegationInwards(Not(form.arg.body)))
+                return form
+            if form.isa(And): return And(pushNegationInwards(form.arg1), pushNegationInwards(form.arg2))
+            if form.isa(Or): return Or(pushNegationInwards(form.arg1), pushNegationInwards(form.arg2))
+            if form.isa(Implies): return Or(Not(pushNegationInwards(form.arg1)), pushNegationInwards(form.arg2))
+            if form.isa(Exists): return Exists(form.var, pushNegationInwards(form.body))
+            if form.isa(Forall): return Forall(form.var, pushNegationInwards(form.body))
+            raise Exception("Unhandled: %s" % form)
+
+        newForm = pushNegationInwards(newForm)
+
+        # Step 3: standardize variables: make sure all variables are different
+        # Don't modify subst; return a new version where var is mapped onto
+        # something that hasn't been seen before.
+        def updateSubst(subst, var):
+            self.varCounts[var.name] += 1
+            newVar = Variable(var.name + str(self.varCounts[var.name]))
+            return dict(list(subst.items()) + [(var, newVar)])
+
+        def standardizeVariables(form, subst):
+            if form.isa(Variable):
+                if form not in subst: raise Exception("Free variable found: %s" % form)
+                return subst[form]
+            if form.isa(Constant): return form
+            if form.isa(Atom): return Atom(*([form.name] + [standardizeVariables(arg, subst) for arg in form.args]))
+            if form.isa(Not): return Not(standardizeVariables(form.arg, subst))
+            if form.isa(And): return And(standardizeVariables(form.arg1, subst), standardizeVariables(form.arg2, subst))
+            if form.isa(Or): return Or(standardizeVariables(form.arg1, subst), standardizeVariables(form.arg2, subst))
+            if form.isa(Exists):
+                newSubst = updateSubst(subst, form.var)
+                return Exists(newSubst[form.var], standardizeVariables(form.body, newSubst))
+            if form.isa(Forall):
+                newSubst = updateSubst(subst, form.var)
+                return Forall(newSubst[form.var], standardizeVariables(form.body, newSubst))
+            raise Exception("Unhandled: %s" % form)
+
+        newForm = standardizeVariables(newForm, {})
+
+        # Step 4: replace existentially quantified variables with Skolem functions
+        def skolemize(form, subst, scope):
+            if form.isa(Variable): return subst.get(form, form)
+            if form.isa(Constant): return form
+            if form.isa(Atom): return Atom(*[form.name] + [skolemize(arg, subst, scope) for arg in form.args])
+            if form.isa(Not): return Not(skolemize(form.arg, subst, scope))
+            if form.isa(And): return And(skolemize(form.arg1, subst, scope), skolemize(form.arg2, subst, scope))
+            if form.isa(Or): return Or(skolemize(form.arg1, subst, scope), skolemize(form.arg2, subst, scope))
+            if form.isa(Exists):
+                # Create a Skolem function that depends on the variables in the scope (list of variables)
+                # Example:
+                # - Suppose scope = [$x, $y] and form = Exists($z,F($z)).
+                # - Normally, we would return F(Z($x,$y)), where Z is a brand new Skolem function.
+                # - But since we don't have function symbols, we replace with a Skolem predicate:
+                #   Forall($z,Implies(Z($z,$x,$y),F($z)))
+                #   Important: when doing resolution, need to catch Not(Z($z,*,*)) as a contradiction.
+                if len(scope) == 0:
+                    subst[form.var] = Constant('skolem' + form.var.name)
+                    return skolemize(form.body, subst, scope)
+                else:
+                    skolem = Atom(*['Skolem' + form.var.name, form.var] + scope)
+                    return Forall(form.var, Or(Not(skolem), skolemize(form.body, subst, scope)))
+            if form.isa(Forall):
+                return Forall(form.var, skolemize(form.body, subst, scope + [form.var]))
+            raise Exception("Unhandled: %s" % form)
+
+        newForm = skolemize(newForm, {}, [])
+
+        # Step 5: remove universal quantifiers [note: need to do this before distribute, unlike Russell/Norvig book]
+        def removeUniversalQuantifiers(form):
+            if form.isa(Atom): return form
+            if form.isa(Not): return Not(removeUniversalQuantifiers(form.arg))
+            if form.isa(And): return And(removeUniversalQuantifiers(form.arg1), removeUniversalQuantifiers(form.arg2))
+            if form.isa(Or): return Or(removeUniversalQuantifiers(form.arg1), removeUniversalQuantifiers(form.arg2))
+            if form.isa(Forall): return removeUniversalQuantifiers(form.body)
+            raise Exception("Unhandled: %s" % form)
+
+        newForm = removeUniversalQuantifiers(newForm)
+
+        # Step 6: distribute Or over And (want And on the outside): Or(And(A,B),C) becomes And(Or(A,C),Or(B,C))
+        def distribute(form):
+            if form.isa(Atom): return form
+            if form.isa(Not): return Not(distribute(form.arg))
+            if form.isa(And): return And(distribute(form.arg1), distribute(form.arg2))
+            if form.isa(Or):
+                # First need to distribute as much as possible
+                f1 = distribute(form.arg1)
+                f2 = distribute(form.arg2)
+                if f1.isa(And):
+                    return And(distribute(Or(f1.arg1, f2)), distribute(Or(f1.arg2, f2)))
+                if f2.isa(And):
+                    return And(distribute(Or(f1, f2.arg1)), distribute(Or(f1, f2.arg2)))
+                return Or(f1, f2)
+            if form.isa(Exists): return Exists(form.var, distribute(form.body))
+            if form.isa(Forall): return Forall(form.var, distribute(form.body))
+            raise Exception("Unhandled: %s" % form)
+
+        newForm = distribute(newForm)
+
+        # Post-processing: break up conjuncts into conjuncts and sort the disjuncts in each conjunct
+        # Remove instances of A and Not(A)
+        conjuncts = [OrList(reduceFormulas(flattenOr(f), Or)) for f in flattenAnd(newForm)]
+        # print rstr(form), rstr(conjuncts)
+        assert len(conjuncts) > 0
+        if any(x == AtomFalse for x in conjuncts): return [AtomFalse]
+        if all(x == AtomTrue for x in conjuncts): return [AtomTrue]
+        conjuncts = [x for x in conjuncts if x != AtomTrue]
+        results = reduceFormulas(conjuncts, And)
+        if len(results) == 0: results = [AtomFalse]
+        # print 'CNF', form, rstr(results)
+        return results
+
+
+class ResolutionRule(BinaryRule):
+    # Assume formulas are in CNF
+    # Assume A and Not(A) don't both exist in a form (taken care of by CNF conversion)
+    def applyRule(self, form1, form2):
+        items1 = flattenOr(form1)
+        items2 = flattenOr(form2)
+        results = []
+        # print 'RESOLVE', form1, form2
+        for i, item1 in enumerate(items1):
+            for j, item2 in enumerate(items2):
+                subst = {}
+                if unify(negateFormula(item1), item2, subst):
+                    newItems1 = withoutElementAt(items1, i)
+                    newItems2 = withoutElementAt(items2, j)
+                    newItems = [applySubst(item, subst) for item in newItems1 + newItems2]
+
+                    if len(newItems) == 0:  # Contradiction: False
+                        results = [AtomFalse]
+                        break
+
+                    # print 'STEP: %s %s => %s %s' % (form1, form2, rstr(newItems), rstr(subst))
+                    result = OrList(reduceFormulas(newItems, Or))
+
+                    # Not(Skolem$x($x,...)) is a contradiction
+                    if isinstance(result, Not) and result.arg.name.startswith('Skolem'):
+                        results = [AtomFalse]
+                        break
+
+                    # Don't add redundant stuff
+                    if result == AtomTrue: continue
+                    if result in results: continue
+
+                    results.append(result)
+            if results == [AtomFalse]: break
+
+        # print 'RESOLUTION: %s %s => %s' % (form1, form2, rstr(results))
+        return results
+
+    def symmetric(self):
+        return True
+
+
+############################################################
+# Model checking
+
+# Return the set of models
+def performModelChecking(allForms, findAll, objects=None, verbose=0):
+    if verbose >= 3:
+        print(('performModelChecking', rstr(allForms)))
+    # Propositionalize, convert to CNF, dedup
+    allForms = propositionalize(allForms, objects)
+    # Convert to CNF: actually makes things slower
+    # allForms = [f for form in allForms for f in ToCNFRule().applyRule(form)]
+    # if any(x == AtomFalse for x in allForms): return []
+    # if all(x == AtomTrue for x in allForms): return [set()]
+    # allForms = [x for x in allForms if x != AtomTrue]
+    # allForms = reduceFormulas(allForms, And)
+    allForms = [universalInterpret(form) for form in allForms]
+    allForms = list(set(allForms) - set([AtomTrue, AtomFalse]))
+    if verbose >= 3:
+        print(('All Forms:', rstr(allForms)))
+
+    if allForms == []: return [set()]  # One model
+    if allForms == [AtomFalse]: return []  # No models
+
+    # Atoms are the variables
+    atoms = set()
+    for form in allForms:
+        for f in allSubexpressions(form):
+            if f.isa(Atom): atoms.add(f)
+    atoms = list(atoms)
+
+    if verbose >= 3:
+        print(('Atoms:', rstr(atoms)))
+        print(('Constraints:', rstr(allForms)))
+
+    # For each atom, list the set of formulas
+    # atom index => list of formulas
+    atomForms = [
+        (atom, [form for form in allForms if atom in allSubexpressions(form)]) \
+        for atom in atoms \
+        ]
+    # Degree heuristic
+    atomForms.sort(key=lambda x: -len(x[1]))
+    atoms = [atom for atom, form in atomForms]
+
+    # Keep only the forms for an atom if it only uses atoms up until that point.
+    atomPrefixForms = []
+    for i, (atom, forms) in enumerate(atomForms):
+        prefixForms = []
+        for form in forms:
+            useAtoms = set(x for x in allSubexpressions(form) if x.isa(Atom))
+            if useAtoms <= set(atoms[0:i + 1]):
+                prefixForms.append(form)
+        atomPrefixForms.append((atom, prefixForms))
+
+    if verbose >= 3:
+        print('Plan:')
+        for atom, forms in atomForms:
+            print(("  %s: %s" % (rstr(atom), rstr(forms))))
+    assert sum(len(forms) for atom, forms in atomPrefixForms) == len(allForms)
+
+    # Build up an interpretation
+    N = len(atoms)
+    models = []  # List of models which are true
+    model = set()  # Set of true atoms, mutated over time
+
+    def recurse(i):  # i: atom index
+        if not findAll and len(models) > 0: return
+        if i == N:  # Found a model on which the formulas are true
+            models.append(set(model))
+            return
+        atom, forms = atomPrefixForms[i]
+        result = universalInterpretAtom(atom)
+        if result == None or result == False:
+            if interpretForms(forms, model): recurse(i + 1)
+        if result == None or result == True:
+            model.add(atom)
+            if interpretForms(forms, model): recurse(i + 1)
+            model.remove(atom)
+
+    recurse(0)
+
+    if verbose >= 5:
+        print('Models:')
+        for model in models:
+            print(("  %s" % rstr(model)))
+
+    return models
+
+
+# A model is a set of atoms.
+def printModel(model):
+    for x in sorted(map(str, model)):
+        print(('*', x, '=', 'True'))
+    print(('*', '(other atoms if any)', '=', 'False'))
+
+
+# Convert a first-order logic formula into a propositional formula, assuming
+# database semantics.
+# Example: Forall becomes And over all objects
+# - Input: form = Forall('$x', Atom('Alive', '$x')), objects = ['alice', 'bob']
+# - Output: And(Atom('Alive', 'alice'), Atom('Alive', 'bob'))
+# Example: Exists becomes Or over all objects
+# - Input: form = Exists('$x', Atom('Alive', '$x')), objects = ['alice', 'bob']
+# - Output: Or(Atom('Alive', 'alice'), Atom('Alive', 'bob'))
+def propositionalize(forms, objects=None):
+    # If not specified, set objects to all constants mentioned in in |form|.
+    if objects == None:
+        objects = set()
+        for form in forms:
+            objects |= set(allConstants(form))
+        objects = list(objects)
+    else:
+        # Make sure objects are expressions: Convert ['a', 'b'] to [Constant('a'), Constant('b')]
+        objects = [toExpr(obj) for obj in objects]
+
+    # Recursively convert |form|, which could contain Exists and Forall, to forms that don't contain these quantifiers.
+    # |subst| is a map from variables to constants.
+    def convert(form, subst):
+        if form.isa(Variable):
+            if form not in subst: raise Exception("Free variable found: %s" % form)
+            return subst[form]
+        if form.isa(Constant): return form
+        if form.isa(Atom):
+            return Atom(*[form.name] + [convert(arg, subst) for arg in form.args])
+        if form.isa(Not): return Not(convert(form.arg, subst))
+        if form.isa(And): return And(convert(form.arg1, subst), convert(form.arg2, subst))
+        if form.isa(Or): return Or(convert(form.arg1, subst), convert(form.arg2, subst))
+        if form.isa(Implies): return Implies(convert(form.arg1, subst), convert(form.arg2, subst))
+        if form.isa(Exists):
+            return OrList([convert(form.body, dict(list(subst.items()) + [(form.var, obj)])) for obj in objects])
+        if form.isa(Forall):
+            return AndList([convert(form.body, dict(list(subst.items()) + [(form.var, obj)])) for obj in objects])
+        raise Exception("Unhandled: %s" % form)
+
+    # Think of newForms as conjoined
+    newForms = []
+    # Convert all the forms
+    for form in forms:
+        newForm = convert(form, {})
+        if newForm == AtomFalse: return [AtomFalse]
+        if newForm == AtomTrue: continue
+        newForms.extend(flattenAnd(newForm))
+    return newForms
+
+
+# Some atoms have a fixed value, so we should just evaluate them.
+# Assumption: atom is propositional logic.
+def universalInterpretAtom(atom):
+    if atom.name == 'Equals':
+        return AtomTrue if atom.args[0] == atom.args[1] else AtomFalse
+    return None
+
+
+# Reduce the expression (e.g., Equals(a,a) => True)
+# Assumption: atom is propositional logic.
+def universalInterpret(form):
+    if form.isa(Variable): return form
+    if form.isa(Constant): return form
+    if form.isa(Atom):
+        result = universalInterpretAtom(form)
+        if result != None: return result
+        return Atom(*[form.name] + [universalInterpret(arg) for arg in form.args])
+    if form.isa(Not):
+        arg = universalInterpret(form.arg)
+        if arg == AtomTrue: return AtomFalse
+        if arg == AtomFalse: return AtomTrue
+        return Not(arg)
+    if form.isa(And):
+        arg1 = universalInterpret(form.arg1)
+        arg2 = universalInterpret(form.arg2)
+        if arg1 == AtomFalse: return AtomFalse
+        if arg2 == AtomFalse: return AtomFalse
+        if arg1 == AtomTrue: return arg2
+        if arg2 == AtomTrue: return arg1
+        return And(arg1, arg2)
+    if form.isa(Or):
+        arg1 = universalInterpret(form.arg1)
+        arg2 = universalInterpret(form.arg2)
+        if arg1 == AtomTrue: return AtomTrue
+        if arg2 == AtomTrue: return AtomTrue
+        if arg1 == AtomFalse: return arg2
+        if arg2 == AtomFalse: return arg1
+        return Or(arg1, arg2)
+    if form.isa(Implies):
+        arg1 = universalInterpret(form.arg1)
+        arg2 = universalInterpret(form.arg2)
+        if arg1 == AtomFalse: return AtomTrue
+        if arg2 == AtomTrue: return AtomTrue
+        if arg1 == AtomTrue: return arg2
+        if arg2 == AtomFalse: return Not(arg1)
+        return Implies(arg1, arg2)
+    raise Exception("Unhandled: %s" % form)
+
+
+def interpretForm(form, model):
+    if form.isa(Atom): return form in model
+    if form.isa(Not): return not interpretForm(form.arg, model)
+    if form.isa(And): return interpretForm(form.arg1, model) and interpretForm(form.arg2, model)
+    if form.isa(Or): return interpretForm(form.arg1, model) or interpretForm(form.arg2, model)
+    if form.isa(Implies): return not interpretForm(form.arg1, model) or interpretForm(form.arg2, model)
+    raise Exception("Unhandled: %s" % form)
+
+
+# Conjunction
+def interpretForms(forms, model):
+    return all(interpretForm(form, model) for form in forms)
+
+
+############################################################
+
+# A Derivation is a tree where each node corresponds to the application of a rule.
+# For any Formula, we can extract a set of categories.
+# Rule arguments are labeled with category.
+class Derivation:
+    def __init__(self, form, children, cost, derived):
+        self.form = form
+        self.children = children
+        self.cost = cost
+        self.permanent = False  # Marker for being able to extract.
+        self.derived = derived  # Whether this was derived (as opposed to added by the user).
+
+    def __repr__(self): return 'Derivation(%s, cost=%s, permanent=%s, derived=%s)' % (
+    self.form, self.cost, self.permanent, self.derived)
+
+
+# Possible responses to queries to the knowledge base
+ENTAILMENT = "ENTAILMENT"
+CONTINGENT = "CONTINGENT"
+CONTRADICTION = "CONTRADICTION"
+
+
+# A response to a KB query
+class KBResponse:
+    # query: what the query is (just a string description for printing)
+    # modify: whether we modified the knowledge base
+    # status: one of the ENTAILMENT, CONTINGENT, CONTRADICTION
+    # trueModel: if available, a model consistent with the KB for which the the query is true
+    # falseModel: if available, a model consistent with the KB for which the the query is false
+    def __init__(self, query, modify, status, trueModel, falseModel):
+        self.query = query
+        self.modify = modify
+        self.status = status
+        self.trueModel = trueModel
+        self.falseModel = falseModel
+
+    def show(self, verbose=1):
+        padding = '>>>>>'
+        print(padding + ' ' + self.responseStr())
+        if verbose >= 1:
+            print(('Query: %s[%s]' % ('TELL' if self.modify else 'ASK', self.query)))
+            if self.trueModel:
+                print('An example of a model where query is TRUE:')
+                printModel(self.trueModel)
+            if self.falseModel:
+                print('An example of a model where query is FALSE:')
+                printModel(self.falseModel)
+
+    def responseStr(self):
+        if self.status == ENTAILMENT:
+            if self.modify:
+                return 'I already knew that.'
+            else:
+                return 'Yes.'
+        elif self.status == CONTINGENT:
+            if self.modify:
+                return 'I learned something.'
+            else:
+                return 'I don\'t know.'
+        elif self.status == CONTRADICTION:
+            if self.modify:
+                return 'I don\'t buy that.'
+            else:
+                return 'No.'
+        else:
+            raise Exception("Invalid status: %s" % self.status)
+
+    def __repr__(self):
+        return self.responseStr()
+
+
+def showKBResponse(response, verbose=1):
+    if isinstance(response, KBResponse):
+        response.show(verbose)
+    else:
+        items = [(obj, r.status) for ((var, obj), r) in list(response.items())]
+        print(('Yes: %s' % rstr([obj for obj, status in items if status == ENTAILMENT])))
+        print(('Maybe: %s' % rstr([obj for obj, status in items if status == CONTINGENT])))
+        print(('No: %s' % rstr([obj for obj, status in items if status == CONTRADICTION])))
+
+
+# A KnowledgeBase is a set collection of Formulas.
+# Interact with it using
+# - addRule: add inference rules
+# - tell: modify the KB with a new formula.
+# - ask: query the KB about
+class KnowledgeBase:
+    def __init__(self, standardizationRule, rules, modelChecking, verbose=0):
+        # Rule to apply to each formula that's added to the KB (None is possible).
+        self.standardizationRule = standardizationRule
+
+        # Set of inference rules
+        self.rules = rules
+
+        # Use model checking as opposed to applying rules.
+        self.modelChecking = modelChecking
+
+        # For debugging
+        self.verbose = verbose
+
+        # Formulas that we believe are true (used when not doing model checking).
+        self.derivations = {}  # Map from Derivation key (logical form) to Derivation
+
+    # Add a formula |form| to the KB if it doesn't contradict.  Returns a KBResponse.
+    def tell(self, form):
+        return self.query(form, modify=True)
+
+    # Ask whether the logical formula |form| is True, False, or unknown based
+    # on the KB.  Returns a KBResponse.
+    def ask(self, form):
+        return self.query(form, modify=False)
+
+    def dump(self):
+        print(('==== Knowledge base [%d derivations] ===' % len(self.derivations)))
+        for deriv in list(self.derivations.values()):
+            print((('-' if deriv.derived else '*'), deriv if self.verbose >= 2 else deriv.form))
+
+    ####### Internal functions
+
+    # Returns a KBResponse or if there are free variables, a mapping from (var, obj) => query without that variable.
+    def query(self, form, modify):
+        # print 'QUERY', form
+        # Handle wh-queries: try all possible values of the free variable, and recurse on query().
+        freeVars = allFreeVars(form)
+        if len(freeVars) > 0:
+            if modify:
+                raise Exception("Can't modify database with a query with free variables: %s" % form)
+            var = freeVars[0]
+            allForms = AndList([deriv.form for deriv in list(self.derivations.values())])
+            if allForms == AtomTrue: return {}  # Weird corner case
+            objects = allConstants(allForms)
+            # Try binding |var| to |obj|
+            response = {}
+            for obj in objects:
+                response[(var, obj)] = self.query(substituteFreeVars(form, var, obj), modify)
+            return response
+
+        # Assume no free variables from here on...
+        formStr = '%s, standardized: %s' % (form, rstr(self.standardize(form)))
+
+        # Models to serve as supporting evidence
+        falseModel = None  # Makes the query false
+        trueModel = None  # Makes the query true
+
+        # Add Not(form)
+        if not self.addAxiom(Not(form)):
+            self.removeTemporary()
+            status = ENTAILMENT
+        else:
+            # Inconclusive...
+            falseModel = self.consistentModel
+            self.removeTemporary()
+
+            # Add form
+            if self.addAxiom(form):
+                if modify:
+                    self.makeTemporaryPermanent()
+                else:
+                    self.removeTemporary()
+                trueModel = self.consistentModel
+                status = CONTINGENT
+            else:
+                self.removeTemporary()
+                status = CONTRADICTION
+
+        return KBResponse(query=formStr, modify=modify, status=status, trueModel=trueModel, falseModel=falseModel)
+
+    # Apply the standardization rule to |form|.
+    def standardize(self, form):
+        if self.standardizationRule:
+            return self.standardizationRule.applyRule(form)
+        return [form]
+
+    # Return whether adding |form| is consistent with the current knowledge base.
+    # Add |form| to the knowledge base if we can.  Note: this is done temporarily!
+    # Just calls addDerivation.
+    def addAxiom(self, form):
+        self.consistentModel = None
+        for f in self.standardize(form):
+            if f == AtomFalse: return False
+            if f == AtomTrue: continue
+            deriv = Derivation(f, children=[], cost=0, derived=False)
+            if not self.addDerivation(deriv): return False
+        return True
+
+    # Return whether the Derivation is consistent with the KB.
+    def addDerivation(self, deriv):
+        # Derived a contradiction
+        if deriv.form == AtomFalse: return False
+
+        key = deriv.form
+        oldDeriv = self.derivations.get(key)
+        maxCost = 100
+        if oldDeriv == None and deriv.cost <= maxCost:
+            # if oldDeriv == None or (deriv.cost < oldDeriv.cost and (deriv.permanent >= oldDeriv.permanent)):
+            # print 'UPDATE %s %s' % (deriv, oldDeriv)
+            # self.dump()
+            # Something worth updating
+            self.derivations[key] = deriv
+            if self.verbose >= 3: print(('add %s [%s derivations]' % (deriv, len(self.derivations))))
+
+            if self.modelChecking:
+                allForms = [deriv.form for deriv in list(self.derivations.values())]
+                models = performModelChecking(allForms, findAll=False, verbose=self.verbose)
+                if len(models) == 0:
+                    return False
+                else:
+                    self.consistentModel = models[0]
+
+            # Apply rules forward
+            if not self.applyUnaryRules(deriv): return False
+            for key2, deriv2 in list(self.derivations.items()):
+                if not self.applyBinaryRules(deriv, deriv2): return False
+                if not self.applyBinaryRules(deriv2, deriv): return False
+
+        return True
+
+    # Raise an exception if |formulas| is not a list of Formulas.
+    def ensureFormulas(self, rule, formulas):
+        if isinstance(formulas, list) and all(formula == False or isinstance(formula, Formula) for formula in formulas):
+            return formulas
+        raise Exception('Expected list of Formulas, but %s returned %s' % (rule, formulas))
+
+    # Return whether everything is okay (no contradiction).
+    def applyUnaryRules(self, deriv):
+        for rule in self.rules:
+            if not isinstance(rule, UnaryRule): continue
+            for newForm in self.ensureFormulas(rule, rule.applyRule(deriv.form)):
+                if not self.addDerivation(Derivation(newForm, children=[deriv], cost=deriv.cost + 1, derived=True)):
+                    return False
+        return True
+
+    # Return whether everything is okay (no contradiction).
+    def applyBinaryRules(self, deriv1, deriv2):
+        for rule in self.rules:
+            if not isinstance(rule, BinaryRule): continue
+            if rule.symmetric() and str(deriv1.form) >= str(deriv2.form): continue  # Optimization
+            for newForm in self.ensureFormulas(rule, rule.applyRule(deriv1.form, deriv2.form)):
+                if not self.addDerivation(
+                        Derivation(newForm, children=[deriv1, deriv2], cost=deriv1.cost + deriv2.cost + 1,
+                                   derived=True)):
+                    return False
+        return True
+
+    # Remove all the temporary derivations from the KB.
+    def removeTemporary(self):
+        for key, value in list(self.derivations.items()):
+            if not value.permanent:
+                del self.derivations[key]
+
+    # Mark all the derivations marked temporary to permanent.
+    def makeTemporaryPermanent(self):
+        for deriv in list(self.derivations.values()):
+            deriv.permanent = True
+
+
+# Create an empty knowledge base equipped with the usual inference rules.
+def createResolutionKB():
+    return KnowledgeBase(standardizationRule=ToCNFRule(), rules=[ResolutionRule()], modelChecking=False)
+
+
+def createModelCheckingKB():
+    return KnowledgeBase(standardizationRule=None, rules=[], modelChecking=True)
diff --git a/hw2/ints/models/4a-0.pklz b/hw2/ints/models/4a-0.pklz
new file mode 100644
index 0000000..411c8fa
Binary files /dev/null and b/hw2/ints/models/4a-0.pklz differ
diff --git a/hw2/ints/models/4a-1.pklz b/hw2/ints/models/4a-1.pklz
new file mode 100644
index 0000000..b742254
Binary files /dev/null and b/hw2/ints/models/4a-1.pklz differ
diff --git a/hw2/ints/models/4a-2.pklz b/hw2/ints/models/4a-2.pklz
new file mode 100644
index 0000000..66a0b55
Binary files /dev/null and b/hw2/ints/models/4a-2.pklz differ
diff --git a/hw2/ints/models/4a-3.pklz b/hw2/ints/models/4a-3.pklz
new file mode 100644
index 0000000..b38bde7
Binary files /dev/null and b/hw2/ints/models/4a-3.pklz differ
diff --git a/hw2/ints/models/4a-4.pklz b/hw2/ints/models/4a-4.pklz
new file mode 100644
index 0000000..0d3d4ac
Binary files /dev/null and b/hw2/ints/models/4a-4.pklz differ
diff --git a/hw2/ints/models/4a-5.pklz b/hw2/ints/models/4a-5.pklz
new file mode 100644
index 0000000..b4899b2
Binary files /dev/null and b/hw2/ints/models/4a-5.pklz differ
diff --git a/hw2/ints/models/4a-all.pklz b/hw2/ints/models/4a-all.pklz
new file mode 100644
index 0000000..9ab0925
Binary files /dev/null and b/hw2/ints/models/4a-all.pklz differ
diff --git a/hw2/ints/submission.py b/hw2/ints/submission.py
new file mode 100644
index 0000000..99336ba
--- /dev/null
+++ b/hw2/ints/submission.py
@@ -0,0 +1,42 @@
+############################################################
+# Problem 4: Odd and even integers
+from typing import Tuple, List
+from logic import *
+
+
+# Return the following 6 laws. Be sure your formulas are exactly in the order specified.
+# 0. Each number $x$ has exactly one successor, which is not equal to $x$.
+# 1. Each number is either even or odd, but not both.
+# 2. The successor number of an even number is odd.
+# 3. The successor number of an odd number is even.
+# 4. For every number $x$, the successor of $x$ is larger than $x$.
+# 5. Larger is a transitive property: if $x$ is larger than $y$ and $y$ is
+#    larger than $z$, then $x$ is larger than $z$.
+# Query: For each number, there exists an even number larger than it.
+def ints() -> Tuple[List[Formula], Formula]:
+    def Even(x): return Atom('Even', x)  # whether x is even
+
+    def Odd(x): return Atom('Odd', x)  # whether x is odd
+
+    def Successor(x, y): return Atom('Successor', x, y)  # whether x's successor is y
+
+    def Larger(x, y): return Atom('Larger', x, y)  # whether x is larger than y
+
+    # Note: all objects are numbers, so we don't need to define Number as an
+    # explicit predicate.
+    #
+    # Note: pay attention to the order of arguments of Successor and Larger.
+    # Populate `formulas` with the 6 laws above.
+    #
+    # Hint: You might want to use the Equals predicate, defined in logic.py.  This
+    # predicate is used to assert that two objects are the same.
+    formulas = []
+    formulas.append(Forall('$x', Exists('$y', And(Successor('$x', '$y'), And(Not(Equals('$x', '$y')), Forall('$z', Implies(Not(Equals('$z', '$y')), Not(Successor('$x', '$z')))))))))
+    formulas.append(Forall('$x', Or(And(Even('$x'), Not(Odd('$x'))), And(Odd('$x'), Not(Even('$x'))))))
+    formulas.append(Forall('$x', Implies(Even('$x'), Exists('$y', Odd(Successor('$x', '$y'))))))
+    formulas.append(Forall('$x', Implies(Odd('$x'), Exists('$y', Even(Successor('$x', '$y'))))))
+    formulas.append(Forall('$x', Implies(Exists('$y', Successor('$x', '$y')), Larger('$y', '$x'))))
+    formulas.append(Forall('$x', Forall('$y', Forall('$z', Implies(And(Larger('$x', '$y'), Larger('$y', '$z')), Larger('$x', '$z'))))))
+
+    query = Forall('$x', Exists('$y', And(Even('$y'), Larger('$y', '$x'))))
+    return formulas, query
\ No newline at end of file
diff --git a/hw2/knights/__pycache__/logic.cpython-312.pyc b/hw2/knights/__pycache__/logic.cpython-312.pyc
new file mode 100644
index 0000000..fd441eb
Binary files /dev/null and b/hw2/knights/__pycache__/logic.cpython-312.pyc differ
diff --git a/hw2/knights/logic.py b/hw2/knights/logic.py
new file mode 100644
index 0000000..627bec3
--- /dev/null
+++ b/hw2/knights/logic.py
@@ -0,0 +1,260 @@
+class Sentence:
+
+    def evaluate(self, model):
+        """Evaluates the logical sentence."""
+        raise Exception("nothing to evaluate")
+
+    def formula(self):
+        """Returns string formula representing logical sentence."""
+        return ""
+
+    def symbols(self):
+        """Returns a set of all symbols in the logical sentence."""
+        return set()
+
+    @classmethod
+    def validate(cls, sentence):
+        if not isinstance(sentence, Sentence):
+            raise TypeError("must be a logical sentence")
+
+    @classmethod
+    def parenthesize(cls, s):
+        """Parenthesizes an expression if not already parenthesized."""
+        def balanced(s):
+            """Checks if a string has balanced parentheses."""
+            count = 0
+            for c in s:
+                if c == "(":
+                    count += 1
+                elif c == ")":
+                    if count <= 0:
+                        return False
+                    count -= 1
+            return count == 0
+        if not len(s) or s.isalpha() or (
+            s[0] == "(" and s[-1] == ")" and balanced(s[1:-1])
+        ):
+            return s
+        else:
+            return f"({s})"
+
+
+class Symbol(Sentence):
+
+    def __init__(self, name):
+        self.name = name
+
+    def __eq__(self, other):
+        return isinstance(other, Symbol) and self.name == other.name
+
+    def __hash__(self):
+        return hash(("symbol", self.name))
+
+    def __repr__(self):
+        return self.name
+
+    def evaluate(self, model):
+        try:
+            return bool(model[self.name])
+        except KeyError:
+            raise Exception(f"variable {self.name} not in model")
+
+    def formula(self):
+        return self.name
+
+    def symbols(self):
+        return {self.name}
+
+
+class Not(Sentence):
+    def __init__(self, operand):
+        Sentence.validate(operand)
+        self.operand = operand
+
+    def __eq__(self, other):
+        return isinstance(other, Not) and self.operand == other.operand
+
+    def __hash__(self):
+        return hash(("not", hash(self.operand)))
+
+    def __repr__(self):
+        return f"Not({self.operand})"
+
+    def evaluate(self, model):
+        return not self.operand.evaluate(model)
+
+    def formula(self):
+        return "¬" + Sentence.parenthesize(self.operand.formula())
+
+    def symbols(self):
+        return self.operand.symbols()
+
+
+class And(Sentence):
+    def __init__(self, *conjuncts):
+        for conjunct in conjuncts:
+            Sentence.validate(conjunct)
+        self.conjuncts = list(conjuncts)
+
+    def __eq__(self, other):
+        return isinstance(other, And) and self.conjuncts == other.conjuncts
+
+    def __hash__(self):
+        return hash(
+            ("and", tuple(hash(conjunct) for conjunct in self.conjuncts))
+        )
+
+    def __repr__(self):
+        conjunctions = ", ".join(
+            [str(conjunct) for conjunct in self.conjuncts]
+        )
+        return f"And({conjunctions})"
+
+    def add(self, conjunct):
+        Sentence.validate(conjunct)
+        self.conjuncts.append(conjunct)
+
+    def evaluate(self, model):
+        return all(conjunct.evaluate(model) for conjunct in self.conjuncts)
+
+    def formula(self):
+        if len(self.conjuncts) == 1:
+            return self.conjuncts[0].formula()
+        return " ∧ ".join([Sentence.parenthesize(conjunct.formula())
+                           for conjunct in self.conjuncts])
+
+    def symbols(self):
+        return set.union(*[conjunct.symbols() for conjunct in self.conjuncts])
+
+
+class Or(Sentence):
+    def __init__(self, *disjuncts):
+        for disjunct in disjuncts:
+            Sentence.validate(disjunct)
+        self.disjuncts = list(disjuncts)
+
+    def __eq__(self, other):
+        return isinstance(other, Or) and self.disjuncts == other.disjuncts
+
+    def __hash__(self):
+        return hash(
+            ("or", tuple(hash(disjunct) for disjunct in self.disjuncts))
+        )
+
+    def __repr__(self):
+        disjuncts = ", ".join([str(disjunct) for disjunct in self.disjuncts])
+        return f"Or({disjuncts})"
+
+    def evaluate(self, model):
+        return any(disjunct.evaluate(model) for disjunct in self.disjuncts)
+
+    def formula(self):
+        if len(self.disjuncts) == 1:
+            return self.disjuncts[0].formula()
+        return " ∨  ".join([Sentence.parenthesize(disjunct.formula())
+                            for disjunct in self.disjuncts])
+
+    def symbols(self):
+        return set.union(*[disjunct.symbols() for disjunct in self.disjuncts])
+
+
+class Implication(Sentence):
+    def __init__(self, antecedent, consequent):
+        Sentence.validate(antecedent)
+        Sentence.validate(consequent)
+        self.antecedent = antecedent
+        self.consequent = consequent
+
+    def __eq__(self, other):
+        return (isinstance(other, Implication)
+                and self.antecedent == other.antecedent
+                and self.consequent == other.consequent)
+
+    def __hash__(self):
+        return hash(("implies", hash(self.antecedent), hash(self.consequent)))
+
+    def __repr__(self):
+        return f"Implication({self.antecedent}, {self.consequent})"
+
+    def evaluate(self, model):
+        return ((not self.antecedent.evaluate(model))
+                or self.consequent.evaluate(model))
+
+    def formula(self):
+        antecedent = Sentence.parenthesize(self.antecedent.formula())
+        consequent = Sentence.parenthesize(self.consequent.formula())
+        return f"{antecedent} => {consequent}"
+
+    def symbols(self):
+        return set.union(self.antecedent.symbols(), self.consequent.symbols())
+
+
+class Biconditional(Sentence):
+    def __init__(self, left, right):
+        Sentence.validate(left)
+        Sentence.validate(right)
+        self.left = left
+        self.right = right
+
+    def __eq__(self, other):
+        return (isinstance(other, Biconditional)
+                and self.left == other.left
+                and self.right == other.right)
+
+    def __hash__(self):
+        return hash(("biconditional", hash(self.left), hash(self.right)))
+
+    def __repr__(self):
+        return f"Biconditional({self.left}, {self.right})"
+
+    def evaluate(self, model):
+        return ((self.left.evaluate(model)
+                 and self.right.evaluate(model))
+                or (not self.left.evaluate(model)
+                    and not self.right.evaluate(model)))
+
+    def formula(self):
+        left = Sentence.parenthesize(str(self.left))
+        right = Sentence.parenthesize(str(self.right))
+        return f"{left} <=> {right}"
+
+    def symbols(self):
+        return set.union(self.left.symbols(), self.right.symbols())
+
+
+def model_check(knowledge, query):
+    """Checks if knowledge base entails query."""
+
+    def check_all(knowledge, query, symbols, model):
+        """Checks if knowledge base entails query, given a particular model."""
+
+        # If model has an assignment for each symbol
+        if not symbols:
+
+            # If knowledge base is true in model, then query must also be true
+            if knowledge.evaluate(model):
+                return query.evaluate(model)
+            return True
+        else:
+
+            # Choose one of the remaining unused symbols
+            remaining = symbols.copy()
+            p = remaining.pop()
+
+            # Create a model where the symbol is true
+            model_true = model.copy()
+            model_true[p] = True
+
+            # Create a model where the symbol is false
+            model_false = model.copy()
+            model_false[p] = False
+
+            # Ensure entailment holds in both models
+            return (check_all(knowledge, query, remaining, model_true) and
+                    check_all(knowledge, query, remaining, model_false))
+
+    # Get all symbols in both knowledge and query
+    symbols = set.union(knowledge.symbols(), query.symbols())
+
+    # Check that knowledge entails query
+    return check_all(knowledge, query, symbols, dict())
\ No newline at end of file
diff --git a/hw2/knights/puzzle.py b/hw2/knights/puzzle.py
new file mode 100644
index 0000000..a72eced
--- /dev/null
+++ b/hw2/knights/puzzle.py
@@ -0,0 +1,82 @@
+from logic import *
+
+AKnight = Symbol("A is a Knight")
+AKnave = Symbol("A is a Knave")
+
+BKnight = Symbol("B is a Knight")
+BKnave = Symbol("B is a Knave")
+
+CKnight = Symbol("C is a Knight")
+CKnave = Symbol("C is a Knave")
+
+# Puzzle 0
+# A says "I am both a knight and a knave."
+knowledge0 = And(
+    Or(AKnight, AKnave),  # A is either a knight or a knave
+    Not(And(AKnight, AKnave)),  # A cannot be both a knight and a knave
+    Biconditional(AKnight, And(AKnight, AKnave))  # If A is a knight, then the statement is true; if A is a knave, the statement is false
+)
+
+# Puzzle 1
+# A says "We are both knaves."
+# B says nothing.
+knowledge1 = And(
+    Or(AKnight, AKnave),  # A is either a knight or a knave
+    Or(BKnight, BKnave),  # B is either a knight or a knave
+    Not(And(AKnight, AKnave)),  # A cannot be both a knight and a knave
+    Not(And(BKnight, BKnave)),  # B cannot be both a knight and a knave
+    Biconditional(AKnight, And(AKnave, BKnave)),  # If A is a knight, then the statement is true; if A is a knave, the statement is false
+    Biconditional(AKnave, Not(And(AKnave, BKnave)))  # If A is a knave, then the opposite of the statement is true
+)
+
+# Puzzle 2
+# A says "We are the same kind."
+# B says "We are of different kinds."
+knowledge2 = And(
+    Or(AKnight, AKnave),  # A is either a knight or a knave
+    Or(BKnight, BKnave),  # B is either a knight or a knave
+    Not(And(AKnight, AKnave)),  # A cannot be both a knight and a knave
+    Not(And(BKnight, BKnave)),  # B cannot be both a knight and a knave
+    Biconditional(AKnight, Or(And(AKnight, BKnight), And(AKnave, BKnave))),  # If A is a knight, then A's statement is true; if A is a knave, then A's statement is false
+    Biconditional(BKnight, Or(And(AKnight, BKnave), And(AKnave, BKnight)))  # If B is a knight, then B's statement is true; if B is a knave, then B's statement is false
+)
+
+# Puzzle 3
+# A says either "I am a knight." or "I am a knave.", but you don't know which.
+# B says "A said 'I am a knave'."
+# B says "C is a knave."
+# C says "A is a knight."
+knowledge3 = And(
+    Or(AKnight, AKnave),
+    Or(BKnight, BKnave),
+    Or(CKnight, CKnave),
+    Biconditional(AKnight, Not(AKnave)),
+    Biconditional(BKnight, Not(BKnave)),
+    Biconditional(CKnight, Not(CKnave)),
+    Implication(BKnight, Not(AKnave)),
+    Implication(BKnave, And(AKnight, CKnight)),
+    Implication(AKnight, CKnight),
+    Implication(AKnight, Not(BKnight))
+)
+
+
+def main():
+    symbols = [AKnight, AKnave, BKnight, BKnave, CKnight, CKnave]
+    puzzles = [
+        ("Puzzle 0", knowledge0),
+        ("Puzzle 1", knowledge1),
+        ("Puzzle 2", knowledge2),
+        ("Puzzle 3", knowledge3)
+    ]
+    for puzzle, knowledge in puzzles:
+        print(puzzle)
+        if len(knowledge.conjuncts) == 0:
+            print("    Not yet implemented.")
+        else:
+            for symbol in symbols:
+                if model_check(knowledge, symbol):
+                    print(f"    {symbol}")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/main.aux b/main.aux
index cacda7b..afe5557 100644
--- a/main.aux
+++ b/main.aux
@@ -10,4 +10,8 @@
 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Grid City}{7}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Six Degrees}{8}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Tic Tac Toe}{8}{}\protected@file@percent }
-\gdef \@abspage@last{9}
+\@writefile{toc}{\contentsline {section}{\numberline {2}Homework 2}{8}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Cake}{8}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Knights and Knaves}{10}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Odds and Evens}{10}{}\protected@file@percent }
+\gdef \@abspage@last{11}
diff --git a/main.fdb_latexmk b/main.fdb_latexmk
index 36f9914..2339b38 100644
--- a/main.fdb_latexmk
+++ b/main.fdb_latexmk
@@ -1,8 +1,8 @@
 # Fdb version 4
-["pdflatex"] 1709000449.89094 "c:/Users/uzair/OneDrive/Documents/CSC 665/main.tex" "main.pdf" "main" 1709000450.74539 0
-  "C:/Users/uzair/AppData/Local/MiKTeX/fonts/map/pdftex/pdftex.map" 1707457733 80909 eab91d9745dd2edfd62a31d53cd5fe15 ""
-  "C:/Users/uzair/AppData/Local/MiKTeX/fonts/pk/ljfour/jknappen/ec/dpi600/tcrm1000.pk" 1707288887 11548 1854d2b3451e3d517cccd4e0b4daead1 ""
-  "C:/Users/uzair/AppData/Local/MiKTeX/miktex/data/le/pdftex/pdflatex.fmt" 1707288883 24210786 eea8c83a2618bf979528f763e32e98c9 ""
+["pdflatex"] 1710976757.77869 "c:/Users/uzair/OneDrive/Documents/Programming/classes/spring-2024/CSC_665_Homework/main.tex" "main.pdf" "main" 1710976758.61168 0
+  "C:/Users/uzair/AppData/Local/MiKTeX/fonts/map/pdftex/pdftex.map" 1710451113 80909 eab91d9745dd2edfd62a31d53cd5fe15 ""
+  "C:/Users/uzair/AppData/Local/MiKTeX/fonts/pk/ljfour/jknappen/ec/dpi600/tcrm1000.pk" 1710450570 11548 75f9244b55c9330932ad6d45f833429f ""
+  "C:/Users/uzair/AppData/Local/MiKTeX/miktex/data/le/pdftex/pdflatex.fmt" 1710872278 24233103 0233cc216d9fba92d9492b92406b1361 ""
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/tfm/jknappen/ec/tcrm1000.tfm" 993062508 1436 c7f957a372ef2fbe93c0982f96625e12 ""
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1233951848 1004 54797486969f23fa377b128694d548df ""
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1233951854 916 f87d7c45f9c908e672703b83b72241a3 ""
@@ -49,15 +49,16 @@
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/tex/latex/graphics/graphicx.sty" 1665067579 8010 a8d949cbdbc5c983593827c9eec252e1 ""
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/tex/latex/graphics/keyval.sty" 1665067579 2671 7e67d78d9b88c845599a85b2d41f2e39 ""
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/tex/latex/graphics/trig.sty" 1665067579 4023 293ea1c16429fc0c4cf605f4da1791a9 ""
-  "C:/Users/uzair/AppData/Local/Programs/MiKTeX/tex/latex/l3backend/l3backend-pdftex.def" 1704400941 30006 57b07afb710ee2f649c65cfbafda39c1 ""
+  "C:/Users/uzair/AppData/Local/Programs/MiKTeX/tex/latex/l3backend/l3backend-pdftex.def" 1708427688 30006 3d512c0edd558928ddea1690180ef77e ""
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/tex/latex/mathtools/mathtools.sty" 1656514886 62269 5c1837a5bc5db4c0d255eedc225ca44b ""
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/tex/latex/mathtools/mhsetup.sty" 1656514886 5582 a43dedf8e5ec418356f1e9dfe5d29fc3 ""
   "C:/Users/uzair/AppData/Local/Programs/MiKTeX/tex/latex/tools/calc.sty" 1700599895 10214 547fd4d29642cb7c80bf54b49d447f01 ""
-  "c:/Users/uzair/OneDrive/Documents/CSC 665/main.tex" 1709000447 12730 ae20bfc5e0f04caa86c900106aea97ed ""
-  "main.aux" 1709000450 1087 ba931f15dd3503a818797c381a180181 "pdflatex"
-  "main.tex" 1709000447 12730 ae20bfc5e0f04caa86c900106aea97ed ""
-  "titlePage.aux" 1709000450 456 c979711f53deacf2b09031977e556db8 "pdflatex"
-  "titlePage.tex" 1707288498 394 ccdbd50244b3194dbad72dd1c7995bf0 ""
+  "c:/Users/uzair/OneDrive/Documents/Programming/classes/spring-2024/CSC_665_Homework/main.tex" 1710976753 15294 eefeb5115f03a7d6344da121e4de1ec8 ""
+  "hw2/gameTree.png" 1710872445 51736 b13904e696801b947e455a901505f683 ""
+  "main.aux" 1710976758 1503 e54afcc87f6e15c8bb521b6c8a85270b "pdflatex"
+  "main.tex" 1710976753 15294 eefeb5115f03a7d6344da121e4de1ec8 ""
+  "titlePage.aux" 1710976758 456 c979711f53deacf2b09031977e556db8 "pdflatex"
+  "titlePage.tex" 1710042044 407 ccdbd50244b3194dbad72dd1c7995bf0 ""
   (generated)
   "main.aux"
   "main.log"
diff --git a/main.fls b/main.fls
index dac3f66..6ae3368 100644
--- a/main.fls
+++ b/main.fls
@@ -1,6 +1,6 @@
-PWD c:\Users\uzair\OneDrive\Documents\CSC 665
+PWD c:\Users\uzair\OneDrive\Documents\Programming\classes\spring-2024\CSC_665_Homework
 INPUT C:\Users\uzair\AppData\Local\MiKTeX\miktex\data\le\pdftex\pdflatex.fmt
-INPUT c:\Users\uzair\OneDrive\Documents\CSC 665\main.tex
+INPUT c:\Users\uzair\OneDrive\Documents\Programming\classes\spring-2024\CSC_665_Homework\main.tex
 OUTPUT main.log
 INPUT C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex\latex\base\article.cls
 INPUT C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex\latex\base\article.cls
@@ -91,6 +91,13 @@ INPUT C:\Users\uzair\AppData\Local\Programs\MiKTeX\fonts\tfm\public\cm\cmti10.tf
 INPUT C:\Users\uzair\AppData\Local\Programs\MiKTeX\fonts\tfm\public\cm\cmbx12.tfm
 INPUT C:\Users\uzair\AppData\Local\Programs\MiKTeX\fonts\tfm\jknappen\ec\tcrm1000.tfm
 INPUT C:\Users\uzair\AppData\Local\Programs\MiKTeX\fonts\tfm\public\cm\cmbx10.tfm
+INPUT .\hw2\gameTree.png
+INPUT .\hw2\gameTree.png
+INPUT .\hw2\gameTree.png
+INPUT .\hw2\gameTree.png
+INPUT .\hw2\gameTree.png
+INPUT .\hw2\gameTree.png
+INPUT .\hw2\gameTree.png
 INPUT main.aux
 INPUT .\titlePage.aux
 INPUT .\titlePage.aux
diff --git a/main.log b/main.log
index e6b2777..ac32880 100644
--- a/main.log
+++ b/main.log
@@ -1,25 +1,25 @@
-This is pdfTeX, Version 3.141592653-2.6-1.40.25 (MiKTeX 24.1) (preloaded format=pdflatex 2024.2.6)  26 FEB 2024 18:20
+This is pdfTeX, Version 3.141592653-2.6-1.40.26 (MiKTeX 24.3) (preloaded format=pdflatex 2024.3.19)  20 MAR 2024 16:19
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
  %&-line parsing enabled.
-**"c:/Users/uzair/OneDrive/Documents/CSC 665/main.tex"
-(c:/Users/uzair/OneDrive/Documents/CSC 665/main.tex
+**c:/Users/uzair/OneDrive/Documents/Programming/classes/spring-2024/CSC_665_Homework/main.tex
+(c:/Users/uzair/OneDrive/Documents/Programming/classes/spring-2024/CSC_665_Homework/main.tex
 LaTeX2e <2023-11-01> patch level 1
-L3 programming layer <2024-01-22>
+L3 programming layer <2024-02-20>
 (C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex/latex/base\article.cls
 Document Class: article 2023/05/17 v1.4n Standard LaTeX document class
 (C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex/latex/base\size10.clo
 File: size10.clo 2023/05/17 v1.4n Standard LaTeX file (size option)
 )
-\c@part=\count187
-\c@section=\count188
-\c@subsection=\count189
-\c@subsubsection=\count190
-\c@paragraph=\count191
-\c@subparagraph=\count192
-\c@figure=\count193
-\c@table=\count194
+\c@part=\count188
+\c@section=\count189
+\c@subsection=\count190
+\c@subsubsection=\count191
+\c@paragraph=\count192
+\c@subparagraph=\count193
+\c@figure=\count194
+\c@table=\count195
 \abovecaptionskip=\skip48
 \belowcaptionskip=\skip49
 \bibindent=\dimen140
@@ -40,14 +40,14 @@ Package: amsbsy 1999/11/29 v1.2d Bold Symbols
 ) (C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex/latex/amsmath\amsopn.sty
 Package: amsopn 2022/04/08 v2.04 operator names
 )
-\inf@bad=\count195
+\inf@bad=\count196
 LaTeX Info: Redefining \frac on input line 234.
-\uproot@=\count196
-\leftroot@=\count197
+\uproot@=\count197
+\leftroot@=\count198
 LaTeX Info: Redefining \overline on input line 399.
 LaTeX Info: Redefining \colon on input line 410.
-\classnum@=\count198
-\DOTSCASE@=\count199
+\classnum@=\count199
+\DOTSCASE@=\count266
 LaTeX Info: Redefining \ldots on input line 496.
 LaTeX Info: Redefining \dots on input line 499.
 LaTeX Info: Redefining \cdots on input line 620.
@@ -60,20 +60,20 @@ LaTeX Info: Redefining \Bigg on input line 725.
 \big@size=\dimen143
 LaTeX Font Info:    Redeclaring font encoding OML on input line 743.
 LaTeX Font Info:    Redeclaring font encoding OMS on input line 744.
-\macc@depth=\count266
+\macc@depth=\count267
 LaTeX Info: Redefining \bmod on input line 905.
 LaTeX Info: Redefining \pmod on input line 910.
 LaTeX Info: Redefining \smash on input line 940.
 LaTeX Info: Redefining \relbar on input line 970.
 LaTeX Info: Redefining \Relbar on input line 971.
-\c@MaxMatrixCols=\count267
+\c@MaxMatrixCols=\count268
 \dotsspace@=\muskip16
-\c@parentequation=\count268
-\dspbrk@lvl=\count269
+\c@parentequation=\count269
+\dspbrk@lvl=\count270
 \tag@help=\toks18
-\row@=\count270
-\column@=\count271
-\maxfields@=\count272
+\row@=\count271
+\column@=\count272
+\maxfields@=\count273
 \andhelp@=\toks19
 \eqnshift@=\dimen144
 \alignsep@=\dimen145
@@ -94,20 +94,20 @@ Package: keyval 2022/05/29 v1.15 key=value parser (DPC)
 \KV@toks@=\toks22
 ) (C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex/latex/tools\calc.sty
 Package: calc 2023/07/08 v4.3 Infix arithmetic (KKT,FJ)
-\calc@Acount=\count273
-\calc@Bcount=\count274
+\calc@Acount=\count274
+\calc@Bcount=\count275
 \calc@Adimen=\dimen150
 \calc@Bdimen=\dimen151
 \calc@Askip=\skip53
 \calc@Bskip=\skip54
 LaTeX Info: Redefining \setlength on input line 80.
 LaTeX Info: Redefining \addtolength on input line 81.
-\calc@Ccount=\count275
+\calc@Ccount=\count276
 \calc@Cskip=\skip55
 ) (C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex/latex/mathtools\mhsetup.sty
 Package: mhsetup 2021/03/18 v1.4 programming setup (MH)
 )
-\g_MT_multlinerow_int=\count276
+\g_MT_multlinerow_int=\count277
 \l_MT_multwidth_dim=\dimen152
 \origjot=\skip56
 \l_MT_shortvdotswithinadjustabove_dim=\dimen153
@@ -130,8 +130,8 @@ LaTeX Font Info:    Redeclaring math symbol \hbar on input line 98.
 LaTeX Font Info:    Overwriting math alphabet `\mathfrak' in version `bold'
 (Font)                  U/euf/m/n --> U/euf/b/n on input line 106.
 )) (C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex/latex/l3backend\l3backend-pdftex.def
-File: l3backend-pdftex.def 2024-01-04 L3 backend support: PDF output (pdfTeX)
-\l__color_backend_stack_int=\count277
+File: l3backend-pdftex.def 2024-02-20 L3 backend support: PDF output (pdfTeX)
+\l__color_backend_stack_int=\count278
 \l__pdf_internal_box=\box54
 ) (main.aux (titlePage.aux))
 \openout1 = `main.aux'.
@@ -164,16 +164,16 @@ Package graphics Info: Driver file: pdftex.def on input line 107.
 File: pdftex.def 2022/09/22 v1.2b Graphics/color driver for pdftex
  (C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex/context/base/mkii\supp-pdf.mkii
 [Loading MPS to PDF converter (version 2006.09.02).]
-\scratchcounter=\count278
+\scratchcounter=\count279
 \scratchdimen=\dimen160
 \scratchbox=\box55
-\nofMPsegments=\count279
-\nofMParguments=\count280
+\nofMPsegments=\count280
+\nofMParguments=\count281
 \everyMPshowfont=\toks23
-\MPscratchCnt=\count281
+\MPscratchCnt=\count282
 \MPscratchDim=\dimen161
-\MPnumerator=\count282
-\makeMPintoPDFobject=\count283
+\MPnumerator=\count283
+\makeMPintoPDFobject=\count284
 \everyMPtoPDFconversion=\toks24
 ))) (C:\Users\uzair\AppData\Local\Programs\MiKTeX\tex/latex/epstopdf-pkg\epstopdf-base.sty
 Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
@@ -215,24 +215,30 @@ Underfull \hbox (badness 10000) in paragraph at lines 108--111
 
  []
 
-[4] [5] [6] [7] [8] (main.aux (titlePage.aux))
+[4] [5] [6] [7]
+<hw2/gameTree.png, id=40, 511.9125pt x 429.10312pt>
+File: hw2/gameTree.png Graphic file (type png)
+<use hw2/gameTree.png>
+Package pdftex.def Info: hw2/gameTree.png  used on input line 271.
+(pdftex.def)             Requested size: 153.57494pt x 128.73192pt.
+ [8] [9 <./hw2/gameTree.png>] [10] (main.aux (titlePage.aux))
  ***********
 LaTeX2e <2023-11-01> patch level 1
-L3 programming layer <2024-01-22>
+L3 programming layer <2024-02-20>
  ***********
  ) 
 Here is how much of TeX's memory you used:
- 3224 strings out of 474542
- 50311 string characters out of 5744447
- 1935978 words of memory out of 5000000
- 25436 multiletter control sequences out of 15000+600000
+ 3231 strings out of 474436
+ 50875 string characters out of 5741954
+ 1938190 words of memory out of 5000000
+ 25549 multiletter control sequences out of 15000+600000
  562573 words of font info for 53 fonts, out of 8000000 for 9000
  1141 hyphenation exceptions out of 8191
- 65i,19n,72p,466b,279s stack positions out of 10000i,1000n,20000p,200000b,200000s
+ 65i,19n,72p,505b,279s stack positions out of 10000i,1000n,20000p,200000b,200000s
  <C:\Users\uzair\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600\tcrm1000.pk><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmbx10.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmbx12.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmex10.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmmi10.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmmi7.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmr10.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmr12.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmr7.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmsy10.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmsy7.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmti10.pfb><C:/Users/uzair/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/latxfont/line10.pfb>
-Output written on main.pdf (9 pages, 163153 bytes).
+Output written on main.pdf (11 pages, 219801 bytes).
 PDF statistics:
- 97 PDF objects out of 1000 (max. 8388607)
+ 106 PDF objects out of 1000 (max. 8388607)
  0 named destinations out of 1000 (max. 500000)
- 1 words of extra memory for PDF output out of 10000 (max. 10000000)
+ 6 words of extra memory for PDF output out of 10000 (max. 10000000)
 
diff --git a/main.pdf b/main.pdf
index b9dbeb4..b3f875e 100644
Binary files a/main.pdf and b/main.pdf differ
diff --git a/main.synctex.gz b/main.synctex.gz
index 4a42788..164b79d 100644
Binary files a/main.synctex.gz and b/main.synctex.gz differ
diff --git a/main.tex b/main.tex
index d0ba7f7..dc8188d 100644
--- a/main.tex
+++ b/main.tex
@@ -261,4 +261,64 @@ Now consider UCS running on an arbitrary graph.
 
 \end{itemize}
 
+\section{Homework 2}
+
+    \subsection{Cake}
+
+    Alice and Bob are sharing a cake....
+
+    \begin{center}
+        \includegraphics[scale=0.3]{hw2/gameTree.png}
+    \end{center}
+
+    
+    Write down the utility Alice should expect to receive in each of the game states given the following knowlege of player strategies:
+
+    \begin{itemize}
+        \item [a.] Alice and Bob playing adversarially, each trying to maximize the cake they receive.
+            \begin{enumerate}
+                \item 1/2
+                \item 1/2
+                \item 1/2
+            \end{enumerate}
+        \item [b. ] Alice still trying to maximize, Bob now playing collaboratively and helping Alice.
+            \begin{enumerate}
+                \item 2/3
+                \item 1/2
+                \item 2/3
+            \end{enumerate}
+        \item [c. ] Random play.
+            \begin{enumerate}
+                \item Node 2 or 3
+                \item Doesn't matter because of constant utility
+                \item Node 3
+            \end{enumerate}
+        \item [d. ] Alpha Beta pruning
+            \begin{enumerate}
+                \item Leaf notes with utility 1/3, 1/3, 1/3, 1/3 on left, and right leaf node with utility 1/6
+            \end{enumerate}
+        \item [e. ] Alpha Beta pruning with tree elements swapped.
+            \begin{enumerate}
+                \item No nodes are pruned
+            \end{enumerate}
+    \end{itemize}
+
+    \begin{itemize}
+        \item [2. ] Logical Formulas
+        \begin{itemize}
+            \item [a. ] $(P \land \neg Q) \lor (\neg P \land Q)$
+            \item [b. ] $(\exists x \text{Course}(x) \land \text{Enrolled}(A, x) \land \text{Enrolled}(B,x))$
+            \item [c. ] $(\forall x \text{Course}(x) \land \text{Enrolled}(A, x) \rightarrow \text{Enrolled}(B,x))$
+            \item [d. ] $\forall x \forall y (\text{Enrolled}(x,y) \land \text{Course}(y) \rightarrow \text{Student}(x))$
+            \item [e. ] $\forall x (\text{Course}(x) \rightarrow \exists y (\text{Student}(y) \land \text{Enrolled}(y,x)))$
+        \end{itemize}
+    \end{itemize}
+
+    \subsection{Knights and Knaves}
+        See attached puzzle.py file
+
+    \subsection{Odds and Evens}
+        See attached submission.py file
+    
+
 \end{document}
\ No newline at end of file