diff --git a/R.py b/R.py
index 1b0fa39..4ce4b04 100644
--- a/R.py
+++ b/R.py
@@ -12,8 +12,7 @@ from logic import (
 )
 from model import Model, ModelFunction, ModelValue, satisfiable
 from generate_model import generate_model
-from vsp import has_vsp
-from smt import smt_is_loaded
+# from vsp import has_vsp
 
 
 # ===================================================
@@ -57,17 +56,12 @@ disjunction_rules = {
     Rule({Conjunction(x, Disjunction(y, z)),}, Disjunction(Conjunction(x, y), Conjunction(x, z)))
 }
 
-falsification_rules = {
-    # At least one value is non-designated
-    Rule(set(), x)
-}
-
 
 logic_rules = implication_rules | negation_rules | conjunction_rules | disjunction_rules
 
 operations = {Negation, Conjunction, Disjunction, Implication}
 
-R_logic = Logic(operations, logic_rules, falsification_rules, "R")
+R_logic = Logic(operations, logic_rules, "R")
 
 # ===============================
 
@@ -75,36 +69,36 @@ R_logic = Logic(operations, logic_rules, falsification_rules, "R")
 Example 2-Element Model of R
 """
 
-a0 = ModelValue("0")
-a1 = ModelValue("1")
+a0 = ModelValue("a0")
+a1 = ModelValue("a1")
 
 carrier_set = {a0, a1}
 
 mnegation = ModelFunction(1, {
     a0: a1,
     a1: a0
-}, "¬")
+})
 
 mimplication = ModelFunction(2, {
     (a0, a0): a1,
     (a0, a1): a1,
     (a1, a0): a0,
     (a1, a1): a1
-}, "→")
+})
 
 mconjunction = ModelFunction(2, {
     (a0, a0): a0,
     (a0, a1): a0,
     (a1, a0): a0,
     (a1, a1): a1
-}, "∧")
+})
 
 mdisjunction = ModelFunction(2, {
     (a0, a0): a0,
     (a0, a1): a1,
     (a1, a0): a1,
     (a1, a1): a1
-}, "∨")
+})
 
 
 designated_values = {a1}
@@ -123,18 +117,11 @@ interpretation = {
 
 print(R_model_2)
 
-print(f"Does {R_model_2.name} satisfy the logic R?", satisfiable(R_logic, R_model_2, interpretation))
-
-if smt_is_loaded():
-    print(has_vsp(R_model_2, mimplication, True, True))
-else:
-    print("Z3 not setup, skipping VSP check...")
-
 
 # =================================
 
 """
-Generate models of R of a specified size using the slow approach
+Generate models of R of a specified size
 """
 
 print("*" * 30)
@@ -143,20 +130,14 @@ model_size = 2
 print("Generating models of Logic", R_logic.name, "of size", model_size)
 solutions = generate_model(R_logic, model_size, print_model=False)
 
-if smt_is_loaded():
-    num_satisfies_vsp = 0
-    for model, interpretation in solutions:
-        negation_defined = Negation in interpretation
-        conj_disj_defined = Conjunction in interpretation and Disjunction in interpretation
-        if has_vsp(model, interpretation[Implication], negation_defined, conj_disj_defined).has_vsp:
-            num_satisfies_vsp += 1
-
-    print(f"Found {len(solutions)} satisfiable models of size {model_size}, {num_satisfies_vsp} of which satisfy VSP")
+print(f"Found {len(solutions)} satisfiable models")
 
+# for model, interpretation in solutions:
+#     print(has_vsp(model, interpretation))
 
 print("*" * 30)
 
-# =================================
+######
 
 """
 Showing the smallest model for R that has the
@@ -165,12 +146,12 @@ variable sharing property.
 This model has 6 elements.
 """
 
-a0 = ModelValue("0")
-a1 = ModelValue("1")
-a2 = ModelValue("2")
-a3 = ModelValue("3")
-a4 = ModelValue("4")
-a5 = ModelValue("5")
+a0 = ModelValue("a0")
+a1 = ModelValue("a1")
+a2 = ModelValue("a2")
+a3 = ModelValue("a3")
+a4 = ModelValue("a4")
+a5 = ModelValue("a5")
 
 carrier_set = { a0, a1, a2, a3, a4, a5 }
 designated_values = {a1, a2, a3, a4, a5 }
@@ -331,26 +312,4 @@ interpretation = {
 
 print(R_model_6)
 print(f"Model {R_model_6.name} satisfies logic {R_logic.name}?", satisfiable(R_logic, R_model_6, interpretation))
-if smt_is_loaded():
-    print(has_vsp(R_model_6, mimplication, True, True))
-else:
-    print("Z3 not loaded, skipping VSP check...")
-
-"""
-Generate models of R of a specified size using the SMT approach
-"""
-
-from vsp import logic_has_vsp
-
-size = 7
-print(f"Searching for a model of size {size} which witness VSP...")
-if smt_is_loaded():
-    solution = logic_has_vsp(R_logic, size)
-    if solution is None:
-        print(f"No models found of size {size} which witness VSP")
-    else:
-        model, vsp_result = solution
-        print(vsp_result)
-        print(model)
-else:
-    print("Z3 not setup, skipping...")
\ No newline at end of file
+# print(has_vsp(R_model_6, interpretation))
diff --git a/generate_model.py b/generate_model.py
index ceb9681..5a46efc 100644
--- a/generate_model.py
+++ b/generate_model.py
@@ -67,7 +67,7 @@ def only_rules_with(rules: Set[Rule], operation: Operation) -> List[Rule]:
 
 def possible_interpretations(
         logic: Logic, carrier_set: Set[ModelValue],
-        designated_values: Set[ModelValue], debug: bool):
+        designated_values: Set[ModelValue]):
     """
     Consider every possible interpretation of operations
     within the specified logic given the carrier set of
@@ -100,7 +100,7 @@ def possible_interpretations(
             passed_functions = candidate_functions
         if len(passed_functions) == 0:
             raise Exception("No interpretation satisfies the axioms for the operation " + str(operation))
-        elif debug:
+        else:
             print(
                   f"Operation {operation.symbol} has {len(passed_functions)} candidate functions"
             )
@@ -120,7 +120,7 @@ def possible_interpretations(
 
 def generate_model(
         logic: Logic, number_elements: int, num_solutions: int = -1,
-        print_model=False, debug=False) -> List[Tuple[Model, Interpretation]]:
+        print_model=False) -> List[Tuple[Model, Interpretation]]:
     """
     Generate the specified number of models that
     satisfy a logic of a certain size.
@@ -136,10 +136,9 @@ def generate_model(
 
     for designated_values in possible_designated_values:
         designated_values = set(designated_values)
-        if debug:
-            print("Considering models for designated values", set_to_str(designated_values))
+        print("Considering models for designated values", set_to_str(designated_values))
 
-        possible_interps = possible_interpretations(logic, carrier_set, designated_values, debug)
+        possible_interps = possible_interpretations(logic, carrier_set, designated_values)
         for interpretation in possible_interps:
             is_valid = True
             model = Model(carrier_set, set(interpretation.values()), designated_values)
diff --git a/logic.py b/logic.py
index 1cb383e..44c5c6b 100644
--- a/logic.py
+++ b/logic.py
@@ -85,7 +85,7 @@ class Logic:
             name: Optional[str] = None):
         self.operations = operations
         self.rules = rules
-        self.falsifies = falsifies if falsifies is not None else set()
+        self.falsifies = falsifies
         self.name = str(abs(hash((
             frozenset(operations),
             frozenset(rules)
diff --git a/model.py b/model.py
index 05a1a1d..807f1ec 100644
--- a/model.py
+++ b/model.py
@@ -5,7 +5,7 @@ a given logic.
 from common import set_to_str, immutable
 from logic import (
     get_propostional_variables, Logic,
-    Operation, PropositionalVariable, Rule, Term
+    Operation, PropositionalVariable, Term
 )
 from collections import defaultdict
 from functools import cached_property, lru_cache, reduce
@@ -13,7 +13,7 @@ from itertools import (
     chain, combinations_with_replacement,
     permutations, product
 )
-from typing import Any, Dict, Generator, List, Optional, Set, Tuple
+from typing import Dict, List, Optional, Set, Tuple
 
 
 __all__ = ['ModelValue', 'ModelFunction', 'Model', 'Interpretation']
@@ -129,12 +129,6 @@ class OrderTable:
 
         candidates = X.intersection(Y)
 
-        if not candidates:
-            return None
-
-        if len(candidates) == 1:
-            return next(iter(candidates))
-
         # Grab all elements greater than each of the candidates
         candidate_ge_maps = (self.ge_map[candidate] for candidate in candidates)
         common_ge_values = reduce(set.intersection, candidate_ge_maps)
@@ -153,12 +147,6 @@ class OrderTable:
 
         candidates = X.intersection(Y)
 
-        if not candidates:
-            return None
-
-        if len(candidates) == 1:
-            return next(iter(candidates))
-
         # Grab all elements smaller than each of the candidates
         candidate_le_maps = (self.le_map[candidate] for candidate in candidates)
         common_le_values = reduce(set.intersection, candidate_le_maps)
@@ -221,7 +209,7 @@ class Model:
 
     def __str__(self):
         result = ("=" * 25) + f"""
-Matrix Name: {self.name}
+Model Name: {self.name}
 Carrier Set: {set_to_str(self.carrier_set)}
 Designated Values: {set_to_str(self.designated_values)}
 """
@@ -255,7 +243,7 @@ def evaluate_term(
 
 def all_model_valuations(
         pvars: Tuple[PropositionalVariable],
-        mvalues: Tuple[ModelValue]) -> Generator[Dict[PropositionalVariable, ModelValue], Any, None]:
+        mvalues: Tuple[ModelValue]):
     """
     Given propositional variables and model values,
     produce every possible mapping between the two.
@@ -277,50 +265,67 @@ def all_model_valuations_cached(
     return list(all_model_valuations(pvars, mvalues))
 
 
-def rule_satisfied(
-        rule: Rule, valuations: List[Dict[PropositionalVariable, ModelValue]],
-        interpretation: Dict[Operation, ModelFunction], designated_values: Set[ModelValue]) -> bool:
-    """
-    Checks whether a rule holds under all valuations.
-
-    If there is a mapping where the premise holds but the consequent does
-    not then this returns False.
-    """
-    for valuation in valuations:
-        premise_met = True
-        for premise in rule.premises:
-            premise_t = evaluate_term(premise, valuation, interpretation)
-            if premise_t not in designated_values:
-                premise_met = False
-                break
-
-        # If any of the premises doesn't hold, then this won't serve as a counterexample
-        if not premise_met:
-            continue
-
-        consequent_t = evaluate_term(rule.conclusion, valuation, interpretation)
-        if consequent_t not in designated_values:
-            # Counterexample found, return False
-            return False
-
-    # No valuation found which contradicts our rule
-    return True
-
-
 def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool:
     """
     Determine whether a model satisfies a logic
     given an interpretation.
     """
     pvars = tuple(get_propostional_variables(tuple(logic.rules)))
-    valuations = all_model_valuations_cached(pvars, tuple(model.carrier_set))
+    mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set))
 
     for rule in logic.rules:
-        if not rule_satisfied(rule, valuations, interpretation, model.designated_values):
-            return False
+        # The rule most hold for all valuations
+        for mapping in mappings:
+            # The check only applies if the premises are designated
+            premise_met = True
+            premise_ts: Set[ModelValue] = set()
+
+            for premise in rule.premises:
+                premise_t = evaluate_term(premise, mapping, interpretation)
+                # As soon as one premise is not designated,
+                # move to the next rule.
+                if premise_t not in model.designated_values:
+                    premise_met = False
+                    break
+                # If designated, keep track of the evaluated term
+                premise_ts.add(premise_t)
+
+            if not premise_met:
+                continue
+
+            # With the premises designated, make sure the consequent is designated
+            consequent_t = evaluate_term(rule.conclusion, mapping, interpretation)
+            if consequent_t not in model.designated_values:
+                return False
 
     for rule in logic.falsifies:
-        if rule_satisfied(rule, valuations, interpretation, model.designated_values):
+        # We must find one mapping where this does not hold
+        counterexample_found = False
+        for mapping in mappings:
+            # The check only applies if the premises are designated
+            premise_met = True
+            premise_ts: Set[ModelValue] = set()
+
+            for premise in rule.premises:
+                premise_t = evaluate_term(premise, mapping, interpretation)
+                # As soon as one premise is not designated,
+                # move to the next rule.
+                if premise_t not in model.designated_values:
+                    premise_met = False
+                    break
+                # If designated, keep track of the evaluated term
+                premise_ts.add(premise_t)
+
+            if not premise_met:
+                continue
+
+            # With the premises designated, make sure the consequent is not designated
+            consequent_t = evaluate_term(rule.conclusion, mapping, interpretation)
+            if consequent_t not in model.designated_values:
+                counterexample_found = True
+                break
+
+        if not counterexample_found:
             return False
 
     return True
diff --git a/smt.py b/smt.py
index 9dbee99..0be7af6 100644
--- a/smt.py
+++ b/smt.py
@@ -1,122 +1,96 @@
-from functools import lru_cache
 from itertools import product
-from typing import Dict, Generator, Optional, Set, Tuple
+from typing import Dict, Generator, Optional, Tuple
 
 from logic import Logic, Operation, Rule, PropositionalVariable, Term, OpTerm, get_prop_vars_from_rule
 from model import Model, ModelValue, ModelFunction
 
-SMT_LOADED = True
-try:
-    from z3 import (
-        And, BoolSort, Context, EnumSort, Function, Implies, Or, sat, Solver, z3
-    )
-except ImportError:
-    SMT_LOADED = False
-
-def smt_is_loaded() -> bool:
-    global SMT_LOADED
-    return SMT_LOADED
+from z3 import (
+    And, BoolSort, Context, EnumSort, Function, Implies, Or, sat, Solver, z3
+)
 
 def term_to_smt(
     t: Term,
-    op_mapping: Dict[Operation, "z3.FuncDeclRef"],
-    var_mapping: Dict[PropositionalVariable, "z3.DatatypeRef"]
-) -> "z3.DatatypeRef":
+    op_mapping: Dict[Operation, z3.FuncDeclRef],
+    var_mapping: Dict[PropositionalVariable, z3.DatatypeRef]
+) -> z3.DatatypeRef:
     """Convert a logic term to its SMT representation."""
     if isinstance(t, PropositionalVariable):
         return var_mapping[t]
 
     assert isinstance(t, OpTerm)
 
-    # Recursively convert all arguments to SMT
     arguments = [term_to_smt(arg, op_mapping, var_mapping) for arg in t.arguments]
     fn = op_mapping[t.operation]
 
     return fn(*arguments)
 
-def all_smt_valuations(pvars: Tuple[PropositionalVariable], smtvalues):
-    """
-    Generator which maps all the propositional variable to
-    smt variables representing the carrier set.
-
-    Exhaust the generator to get all such mappings.
-    """
-    all_possible_values = product(smtvalues, repeat=len(pvars))
-    for valuation in all_possible_values:
-        mapping = dict()
-        assert len(pvars) == len(valuation)
-        for pvar, value in zip(pvars, valuation):
-            mapping[pvar] = value
-        yield mapping
-
-
-@lru_cache
-def all_smt_valuations_cached(pvars: Tuple[PropositionalVariable], smtvalues):
-    return list(all_smt_valuations(pvars, smtvalues))
-
 def logic_rule_to_smt_constraints(
     rule: Rule,
-    IsDesignated: "z3.FuncDeclRef",
+    IsDesignated: z3.FuncDeclRef,
     smt_carrier_set,
-    op_mapping: Dict[Operation, "z3.FuncDeclRef"]
-) -> Generator["z3.BoolRef", None, None]:
+    op_mapping: Dict[Operation, z3.FuncDeclRef]
+) -> Generator[z3.BoolRef, None, None]:
     """
     Encode a logic rule as SMT constraints.
 
     For all valuations: if premises are designated, then conclusion is designated.
     """
-    prop_vars = tuple(get_prop_vars_from_rule(rule))
-    valuations = all_smt_valuations_cached(prop_vars, tuple(smt_carrier_set))
+    prop_vars = get_prop_vars_from_rule(rule)
+
+    # Requires that the rule holds under all valuations
+    for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)):
+        assert len(prop_vars) == len(smt_vars)
+
+        var_mapping = {
+            prop_var: smt_var
+            for (prop_var, smt_var) in zip(prop_vars, smt_vars)
+        }
 
-    for valuation in valuations:
         premises = [
-            IsDesignated(term_to_smt(premise, op_mapping, valuation)) == True
+            IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True
             for premise in rule.premises
         ]
-        conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, valuation)) == True
+        conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == True
 
         if len(premises) == 0:
-            # If there are no premises, then the conclusion must always be designated
             yield conclusion
         else:
-            # Otherwise, combine all the premises with and
-            # and have that if the premises are designated
-            # then the conclusion is designated
             premise = premises[0]
             for p in premises[1:]:
                 premise = And(premise, p)
 
             yield Implies(premise, conclusion)
 
-
 def logic_falsification_rule_to_smt_constraints(
     rule: Rule,
-    IsDesignated: "z3.FuncDeclRef",
+    IsDesignated: z3.FuncDeclRef,
     smt_carrier_set,
-    op_mapping: Dict[Operation, "z3.FuncDeclRef"]
-) -> "z3.BoolRef":
+    op_mapping: Dict[Operation, z3.FuncDeclRef]
+) -> z3.BoolRef:
     """
     Encode a falsification rule as an SMT constraint.
 
     There exists at least one valuation where premises are designated
     but conclusion is not designated.
     """
-    prop_vars = tuple(get_prop_vars_from_rule(rule))
-    valuations = all_smt_valuations_cached(prop_vars, tuple(smt_carrier_set))
+    prop_vars = get_prop_vars_from_rule(rule)
 
     # Collect all possible counter-examples (valuations that falsify the rule)
     counter_examples = []
 
-    for valuation in valuations:
-        # The rule is falsified when all of our premises
-        # are designated but our conclusion is not designated
+    for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)):
+        assert len(prop_vars) == len(smt_vars)
+
+        var_mapping = {
+            prop_var: smt_var
+            for (prop_var, smt_var) in zip(prop_vars, smt_vars)
+        }
 
         premises = [
-            IsDesignated(term_to_smt(premise, op_mapping, valuation)) == True
+            IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True
             for premise in rule.premises
         ]
-
-        conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, valuation)) == False
+        conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == False
 
         if len(premises) == 0:
             counter_examples.append(conclusion)
@@ -158,7 +132,7 @@ class SMTLogicEncoder:
         self.carrier_sort, self.smt_carrier_set = EnumSort("C", element_names, ctx=self.ctx)
 
         # Create operation functions
-        self.operation_function_map: Dict[Operation, "z3.FuncDeclRef"] = {}
+        self.operation_function_map: Dict[Operation, z3.FuncDeclRef] = {}
         for operation in logic.operations:
             self.operation_function_map[operation] = self.create_function(operation.symbol, operation.arity)
 
@@ -169,10 +143,10 @@ class SMTLogicEncoder:
         self._add_logic_constraints()
         self._add_designation_symmetry_constraints()
 
-    def create_predicate(self, name: str, arity: int) -> "z3.FuncDeclRef":
+    def create_predicate(self, name: str, arity: int) -> z3.FuncDeclRef:
         return Function(name, *(self.carrier_sort for _ in range(arity)), BoolSort(ctx=self.ctx))
 
-    def create_function(self, name: str, arity: int) -> "z3.FuncDeclRef":
+    def create_function(self, name: str, arity: int) -> z3.FuncDeclRef:
         return Function(name, *(self.carrier_sort for _ in range(arity + 1)))
 
     def _add_logic_constraints(self):
@@ -197,9 +171,9 @@ class SMTLogicEncoder:
             )
             self.solver.add(constraint)
 
-    def extract_model(self, smt_model) -> Tuple[Model, Dict[Operation, ModelFunction]]:
+    def extract_model(self, smt_model) -> Model:
         """
-        Extract a Model object and interpretation from an SMT model.
+        Extract a Model object from an SMT model.
         """
         carrier_set = {ModelValue(f"{i}") for i in range(self.size)}
 
@@ -211,8 +185,7 @@ class SMTLogicEncoder:
         designated_values = {ModelValue(str(x)) for x in smt_designated}
 
         # Extract operation functions
-        model_functions: Set[ModelFunction] = set()
-        interpretation: Dict[Operation, ModelFunction] = dict()
+        model_functions = set()
         for (operation, smt_function) in self.operation_function_map.items():
             mapping: Dict[Tuple[ModelValue], ModelValue] = {}
             for smt_inputs in product(self.smt_carrier_set, repeat=operation.arity):
@@ -220,12 +193,9 @@ class SMTLogicEncoder:
                 smt_output = smt_model.evaluate(smt_function(*smt_inputs))
                 model_output = ModelValue(str(smt_output))
                 mapping[model_inputs] = model_output
-            model_function = ModelFunction(operation.arity, mapping, operation.symbol)
-            model_functions.add(model_function)
-            interpretation[operation] = model_function
+            model_functions.add(ModelFunction(operation.arity, mapping, operation.symbol))
 
-
-        return Model(carrier_set, model_functions, designated_values), interpretation
+        return Model(carrier_set, model_functions, designated_values)
 
 
     def _add_designation_symmetry_constraints(self):
@@ -248,7 +218,7 @@ class SMTLogicEncoder:
                 )
             )
 
-    def create_exclusion_constraint(self, model: Model) -> "z3.BoolRef":
+    def create_exclusion_constraint(self, model: Model) -> z3.BoolRef:
         """
         Create a constraint that excludes the given model from future solutions.
         """
@@ -260,7 +230,7 @@ class SMTLogicEncoder:
             for smt_elem in self.smt_carrier_set
         }
 
-        # Iterate over all logical operations
+        # Exclude operation function mappings
         for model_func in model.logical_operations:
             operation = Operation(model_func.operation_name, model_func.arity)
             smt_func = self.operation_function_map[operation]
@@ -269,9 +239,10 @@ class SMTLogicEncoder:
                 smt_inputs = tuple(model_value_to_smt[inp] for inp in inputs)
                 smt_output = model_value_to_smt[output]
 
-                # It may be the case that the output of f(input) differs
+                # For future models the input->output mapping may differ
                 constraints.append(smt_func(*smt_inputs) != smt_output)
 
+        # Exclude designated value set
         for smt_elem in self.smt_carrier_set:
             model_val = ModelValue(str(smt_elem))
             is_designated_in_model = model_val in model.designated_values
@@ -284,7 +255,7 @@ class SMTLogicEncoder:
 
         return Or(constraints)
 
-    def find_model(self) -> Optional[Tuple[Model, Dict[Operation, ModelFunction]]]:
+    def find_model(self) -> Optional[Model]:
         """
         Find a single model satisfying the logic constraints.
 
@@ -304,12 +275,12 @@ class SMTLogicEncoder:
             pass
 
 
-def find_model(logic: Logic, size: int) -> Optional[Tuple[Model, Dict[Operation, ModelFunction]]]:
+def find_model(logic: Logic, size: int) -> Optional[Model]:
     """Find a single model for the given logic and size."""
     encoder = SMTLogicEncoder(logic, size)
     return encoder.find_model()
 
-def find_all_models(logic: Logic, size: int) -> Generator[Tuple[Model, Dict[Operation, ModelFunction]], None, None]:
+def find_all_models(logic: Logic, size: int) -> Generator[Model, None, None]:
     """
     Find all models for the given logic and size.
 
@@ -324,14 +295,13 @@ def find_all_models(logic: Logic, size: int) -> Generator[Tuple[Model, Dict[Oper
 
     while True:
         # Try to find a model
-        solution = encoder.find_model()
-        if solution is None:
+        model = encoder.find_model()
+        if model is None:
             break
 
-        yield solution
+        yield model
 
         # Add constraint to exclude this model from future solutions
-        model, _ = solution
         exclusion_constraint = encoder.create_exclusion_constraint(model)
         encoder.solver.add(exclusion_constraint)
 
@@ -377,13 +347,13 @@ class SMTModelEncoder:
             is_designated = model_value in model.designated_values
             self.solver.add(self.is_designated(self.model_value_to_smt[model_value]) == is_designated)
 
-    def create_predicate(self, name: str, arity: int) -> "z3.FuncDeclRef":
+    def create_predicate(self, name: str, arity: int) -> z3.FuncDeclRef:
         return Function(name, *(self.carrier_sort for _ in range(arity)), BoolSort(ctx=self.ctx))
 
-    def create_function(self, name: str, arity: int) -> "z3.FuncDeclRef":
+    def create_function(self, name: str, arity: int) -> z3.FuncDeclRef:
         return Function(name, *(self.carrier_sort for _ in range(arity + 1)))
 
-    def add_function_constraints_from_table(self, smt_fn: "z3.FuncDeclRef", model_fn: ModelFunction):
+    def add_function_constraints_from_table(self, smt_fn: z3.FuncDeclRef, model_fn: ModelFunction):
         for inputs, output in model_fn.mapping.items():
             smt_inputs = tuple(self.model_value_to_smt[inp] for inp in inputs)
             smt_output = self.model_value_to_smt[output]
diff --git a/utils/compare_vsp_results.py b/utils/compare_vsp_results.py
index aa16aa5..82c587d 100644
--- a/utils/compare_vsp_results.py
+++ b/utils/compare_vsp_results.py
@@ -56,9 +56,9 @@ if __name__ == "__main__":
     extra_models1 = 0
     extra_models2 = 0
 
-    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions1:
+    for model, impfunction, negation_defined in solutions1:
         total_models1 += 1
-        vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
+        vsp_result = has_vsp(model, impfunction, negation_defined)
 
         if vsp_result.has_vsp:
             good_models1 += 1
@@ -83,9 +83,9 @@ if __name__ == "__main__":
 
 
     # Check through the remaining models in the second set
-    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions2:
+    for model, impfunction, negation_defined in solutions2:
         total_models2 += 1
-        vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
+        vsp_result = has_vsp(model, impfunction, negation_defined)
 
         if not vsp_result.has_vsp:
             bad_models2 += 1
diff --git a/vsp.py b/vsp.py
index c4fd398..ee87657 100644
--- a/vsp.py
+++ b/vsp.py
@@ -10,12 +10,12 @@ from model import (
     Model, model_closure, ModelFunction, ModelValue
 )
 
-from smt import SMTModelEncoder, SMTLogicEncoder, smt_is_loaded
-
+SMT_LOADED = True
 try:
     from z3 import And, Or, Implies, sat
+    from smt import SMTModelEncoder, SMTLogicEncoder
 except ImportError:
-    pass
+    SMT_LOADED = False
 
 class VSP_Result:
     def __init__(
@@ -29,14 +29,14 @@ class VSP_Result:
 
     def __str__(self):
         if not self.has_vsp:
-            return f"Matrix {self.model_name} does not have the variable sharing property."
-        return f"""Matrix {self.model_name} has the variable sharing property.
+            return f"Model {self.model_name} does not have the variable sharing property."
+        return f"""Model {self.model_name} has the variable sharing property.
 Subalgebra 1: {set_to_str(self.subalgebra1)}
 Subalgebra 2: {set_to_str(self.subalgebra2)}
 """
 
 def has_vsp_magical(model: Model, impfunction: ModelFunction,
-            negation_defined: bool, conjunction_disjunction_defined: bool) -> VSP_Result:
+            negation_defined: bool) -> VSP_Result:
     """
     Checks whether a MaGIC model has the variable
     sharing property.
@@ -46,10 +46,6 @@ def has_vsp_magical(model: Model, impfunction: ModelFunction,
     if len(model.designated_values) == 1:
         return VSP_Result(False, model.name)
 
-    if len(model.carrier_set) in [2,3,4,5,7] \
-        and conjunction_disjunction_defined and negation_defined:
-        return VSP_Result(False, model.name)
-
     assert model.ordering is not None, "Expected ordering table in model"
 
     top = model.ordering.top()
@@ -139,7 +135,7 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
     Checks whether a given model satisfies the variable
     sharing property via SMT
     """
-    if not smt_is_loaded():
+    if not SMT_LOADED:
         raise Exception("Z3 is not property installed, cannot check via SMT")
 
     encoder = SMTModelEncoder(model)
@@ -168,7 +164,7 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
                 )
             )
 
-    # x -> y is non-designated for any x in K1 and y in K2
+    # x -> y is non-designated
     smt_imp = encoder.model_function_map[impfn]
     for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set):
         encoder.solver.add(
@@ -194,11 +190,11 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
 
 
 def has_vsp(model: Model, impfunction: ModelFunction,
-            negation_defined: bool, conjunction_disjunction_defined: bool) -> VSP_Result:
+            negation_defined: bool) -> VSP_Result:
     if model.is_magical:
-        return has_vsp_magical(model, impfunction, negation_defined, conjunction_disjunction_defined)
+        return has_vsp_magical(model, impfunction, negation_defined)
 
-    return has_vsp_smt(model, impfunction)
+    return has_vsp_smt(model)
 
 
 def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]]:
@@ -244,7 +240,7 @@ def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]]
                 )
             )
 
-    # x -> y is non-designated for any x in k1 and y in k2
+    # x -> y is non-designated
     Impfn = encoder.operation_function_map[Implication]
     for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set):
         encoder.solver.add(
@@ -254,15 +250,15 @@ def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]]
             )
         )
 
-    solution = encoder.find_model()
+    model = encoder.find_model()
 
     # We failed to find a VSP witness
-    if solution is None:
+    if model is None:
         return None
 
     # Otherwise, a matrix model and correspoding
     # subalgebras exist.
-    model, _ = solution
+
     smt_model = encoder.solver.model()
     K1_smt = [x for x in encoder.smt_carrier_set if smt_model.evaluate(IsInK1(x))]
     K1 = {ModelValue(str(x)) for x in K1_smt}
diff --git a/vspursuer.py b/vspursuer.py
index 67e73fa..d9d9e53 100755
--- a/vspursuer.py
+++ b/vspursuer.py
@@ -6,7 +6,7 @@ from queue import Empty as QueueEmpty
 import argparse
 import multiprocessing as mp
 
-from logic import Conjunction, Disjunction, Implication, Negation, Operation
+from logic import Negation, Implication, Operation
 from model import Model, ModelFunction
 from parse_magic import SourceFile, parse_matrices
 from vsp import has_vsp, VSP_Result
@@ -36,14 +36,13 @@ def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, Model
         # NOTE: Implication must be defined, the rest may not
         impfunction = interpretation[Implication]
         negation_defined = Negation in interpretation
-        conjunction_disjunction_defined = (Conjunction in interpretation) and (Disjunction in interpretation)
-        yield (model, impfunction, negation_defined, conjunction_disjunction_defined)
+        yield (model, impfunction, negation_defined)
 
-def has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined) -> Tuple[Optional[Model], VSP_Result]:
+def has_vsp_plus_model(model, impfunction, negation_defined) -> Tuple[Optional[Model], VSP_Result]:
     """
     Wrapper which also stores the models along with its vsp result
     """
-    vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
+    vsp_result = has_vsp(model, impfunction, negation_defined)
     # NOTE: Memory optimization - Don't return model if it doesn't have VSP
     model = model if vsp_result.has_vsp else None
     return (model, vsp_result)
@@ -62,8 +61,8 @@ def worker_vsp(task_queue: mp.Queue, result_queue: mp.Queue):
             # If sentinal value, break
             if task is None:
                 break
-            (model, impfunction, negation_defined, conjunction_disjunction_defined) = task
-            result = has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined)
+            (model, impfunction, negation_defined) = task
+            result = has_vsp_plus_model(model, impfunction, negation_defined)
             result_queue.put(result)
     finally:
         # Either an exception occured or the worker finished
@@ -169,7 +168,7 @@ def multi_process_runner(num_cpu: int, data_file_path: str, skip_to: Optional[st
         if vsp_result.has_vsp:
             num_has_vsp += 1
 
-    print_with_timestamp(f"Tested {num_tested} matrices, {num_has_vsp} of which satisfy VSP")
+    print_with_timestamp(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP")
 
 def single_process_runner(data_file_path: str, skip_to: Optional[str]):
     num_tested = 0
@@ -179,8 +178,8 @@ def single_process_runner(data_file_path: str, skip_to: Optional[str]):
     solutions = parse_matrices(SourceFile(data_file))
     solutions = restructure_solutions(solutions, skip_to)
 
-    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions:
-        model, vsp_result = has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined)
+    for model, impfunction, negation_defined in solutions:
+        model, vsp_result = has_vsp_plus_model(model, impfunction, negation_defined)
         print_with_timestamp(vsp_result)
         num_tested += 1
 
@@ -190,7 +189,7 @@ def single_process_runner(data_file_path: str, skip_to: Optional[str]):
         if vsp_result.has_vsp:
             num_has_vsp += 1
 
-    print_with_timestamp(f"Tested {num_tested} matrices, {num_has_vsp} of which satisfy VSP")
+    print_with_timestamp(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP")
 
 
 if __name__ == "__main__":