diff --git a/frame/knowledge_base/demonstrations.py b/frame/knowledge_base/demonstrations.py
index 963879b..0b59bab 100644
--- a/frame/knowledge_base/demonstrations.py
+++ b/frame/knowledge_base/demonstrations.py
@@ -18,11 +18,8 @@
 """
 
 from frame.knowledge_base.entities import (
-    Var, Not, And, Or, Implies,
-    Forall, Exists, Set, SetDomain, In, Zero, Succ, Nat,
-    NatDomain, Lambda, Equals, SetCardinality, SetSum,
-    Fold, Concept, ExampleType, Conjecture, ConceptApplication,
-    ExampleStructure, ConceptType,
+    Zero, Succ, Nat, Concept, ExampleType, 
+    Conjecture, ExampleStructure, ConceptType,
 )
 
 # =============================================================================
diff --git a/frame/knowledge_base/entities.py b/frame/knowledge_base/entities.py
index 012d756..984ddb4 100644
--- a/frame/knowledge_base/entities.py
+++ b/frame/knowledge_base/entities.py
@@ -5,11 +5,8 @@
 
 Expression Framework:
 - Base Expression class and Context for variable tracking
-- Propositional logic (And, Or, Not, Implies)
-- First-order logic quantifiers (Forall, Exists)
 - Set theory operations and predicates
 - Natural number arithmetic
-- Lambda calculus and function application
 - Equality relations
 
 Entity Framework:
@@ -89,330 +86,6 @@ def to_z3(self) -> Z3Template:
         pass
 
 
-class Var(Expression):
-    """A variable."""
-
-    def __init__(self, name: str):
-        self.name = name
-
-    def to_lean4(self) -> str:
-        return self.name
-
-    def to_z3(self) -> Z3Template:
-        raise NotImplementedError("to_z3 is not yet implemented")
-
-
-class ConceptApplication(Expression):
-    """Represents application of a mathematical concept"""
-
-    def __init__(self, concept: "Entity", *args):
-        self.concept = concept
-        self.args = args
-
-    def _filter_example_type(self, arg: Any) -> Any:
-        """Filter out ExampleType values from arguments"""
-        if isinstance(arg, ExampleType):
-            return None  # Skip ExampleType values
-        return arg
-
-    def to_lean4(self) -> str:
-        raise NotImplementedError("to_lean4 is not yet implemented")
-
-    def to_z3(self) -> Z3Template:
-        raise NotImplementedError("to_z3 is not yet implemented")
-
-
-# =============================================================================
-# Propositional Logic Classes
-# =============================================================================
-
-
-class PropVar(Var):
-    """A propositional variable (atomic proposition)."""
-
-    def __init__(self, name: str):
-        super().__init__(name)
-
-    def to_lean4(self) -> str:
-        return self.name
-
-    def to_z3(self) -> Z3Template:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class Not(Expression):
-    def __init__(self, expr: Expression):
-        self.expr = expr
-
-    def to_lean4(self) -> str:
-        return f"(¬ {self.expr.to_lean4()})"
-
-    def to_z3(self) -> Z3Template:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class And(Expression):
-    def __init__(self, left: Expression, right: Expression):
-        self.left = left
-        self.right = right
-
-    def to_lean4(self) -> str:
-        left = self.left.to_lean4()
-        right = self.right.to_lean4()
-        return f"({left} ∧ {right})"
-
-    def to_z3(self) -> Z3Template:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class Or(Expression):
-    def __init__(self, left: Expression, right: Expression):
-        self.left = left
-        self.right = right
-
-    def to_lean4(self) -> str:
-        return f"({self.left.to_lean4()} ∨ {self.right.to_lean4()})"
-
-    def to_z3(self) -> Z3Template:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class Implies(Expression):
-    def __init__(self, antecedent: Expression, consequent: Expression):
-        self.antecedent = antecedent
-        self.consequent = consequent
-
-    def to_lean4(self) -> str:
-        return f"({self.antecedent.to_lean4()} → {self.consequent.to_lean4()})"
-
-    def to_z3(self) -> Z3Template:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-# =============================================================================
-# Quantifiers
-# =============================================================================
-
-
-class Forall(Expression):
-    def __init__(self, var: str, iterable: Expression, body: Expression):
-        """
-        var: variable name (as a string)
-        iterable: an expression denoting the iterable (domain, set, etc.) of the variable
-        body: the predicate in which var appears
-        """
-        self.var = var
-        self.iterable = iterable
-        self.body = body
-
-    def to_lean4(self) -> str:
-        iterable = self.iterable.to_lean4()
-        body = self.body.to_lean4()
-        return f"(∀ {self.var} : {iterable}, {body})"
-
-    def to_z3(self) -> Z3Template:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class Exists(Expression):
-    def __init__(self, var: str, domain: Expression, body: Expression):
-        self.var = var
-        self.domain = domain
-        self.body = body
-
-    def to_lean4(self) -> str:
-        domain = self.domain.to_lean4()
-        body = self.body.to_lean4()
-        return f"(∃ {self.var} : {domain}, {body})"
-
-    def to_z3(self) -> Z3Template:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-# =============================================================================
-# Set Theory Classes
-# =============================================================================
-
-
-class Set(Expression):
-    """
-    Represents a set with a specified element type.
-    Can be defined either by listing elements or by a predicate.
-    """
-
-    def __init__(
-        self,
-        domain: Expression,
-        elements: Optional[
-            List[Expression]
-        ] = None,  # TODO: Change to Set[Expression] but Set is defined twice (once here and once in typing)
-        predicate: Optional[Expression] = None,
-    ):
-        if elements is None and predicate is None:
-            raise ValueError("Must provide either elements or predicate")
-        if elements is not None and predicate is not None:
-            raise ValueError("Cannot provide both elements and predicate")
-        self.domain = domain
-        self.elements = elements
-        self.predicate = predicate
-
-    def to_lean4(self) -> str:
-        if self.elements is not None:
-            elems = ", ".join(e.to_lean4() for e in self.elements)
-            return f"{{" + elems + "}}"
-        else:
-            # Use Lean's set comprehension syntax
-            var = self.predicate.var_name
-            body = self.predicate.body.to_lean4()
-            return f"{{x : {self.domain.to_lean4()} | {body}}}"
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-    def evaluate(self) -> Optional[set]:
-        """
-        Attempts to evaluate the set to a concrete Python set.
-        Returns None if the set cannot be evaluated (e.g., symbolic variables).
-        """
-        if self.elements is not None:
-            try:
-                # If elements are already Python objects (like integers), return them directly
-                if all(not hasattr(e, "evaluate") for e in self.elements):
-                    return set(self.elements)
-                # Otherwise try to evaluate each element
-                return {e.evaluate() for e in self.elements}
-            except AttributeError:
-                return None
-        elif isinstance(self.domain, NatDomain):
-            # For natural numbers, we can try to evaluate up to some bound
-            raise NotImplementedError(
-                "Evaluation of predicate-defined sets requires a proper bounding strategy"
-            )
-        return None
-
-
-class SetDomain(Expression):
-    """Represents the domain/type of sets"""
-
-    def to_lean4(self) -> str:
-        return "Set"
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class TupleDomain(Expression):
-    """
-    Represents a product domain for a tuple of quantified variables.
-    For example, in Lean: D1 × D2 × ...
-    """
-
-    def __init__(self, domains: Tuple["Entity", ...]):
-        self.domains = domains
-
-    def to_lean4(self, ctx: Optional[Any] = None) -> str:
-        return " × ".join(d.to_lean4() for d in self.domains)
-
-    def to_z3(self, ctx: Optional[Any] = None) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class In(Expression):
-    """Represents set membership (x ∈ A)"""
-
-    def __init__(self, element: Expression, set_expr: Expression):
-        self.element = element
-        self.set_expr = set_expr
-
-    def to_lean4(self) -> str:
-        return f"({self.element.to_lean4()} ∈ {self.set_expr.to_lean4()})"
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class SetCardinality(Expression):
-    """Represents the cardinality of a set"""
-
-    def __init__(self, set_expr: Expression):
-        if not isinstance(set_expr, (Set, ConceptApplication)):
-            raise TypeError(
-                "SetCardinality can only be applied to set-valued expressions"
-            )
-        self.set = set_expr
-
-    def to_lean4(self) -> str:
-        set_str = self.set.to_lean4()
-        return f"(Finset.card {set_str})"
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-    def evaluate(self) -> Optional[int]:
-        """
-        Attempts to evaluate the cardinality for concrete cases.
-        Returns:
-        - The number of elements for concrete sets
-        - None if the cardinality cannot be determined (e.g., symbolic sets or concept applications)
-        """
-        if isinstance(self.set, Set) and self.set.elements is not None:
-            try:
-                return len(self.set.elements)
-            except AttributeError:
-                return None
-        elif isinstance(self.set, ConceptApplication):
-            try:
-                # Try to compute the concept and get the length of its result if possible
-                result = self.set.concept.compute(
-                    *[arg.evaluate() for arg in self.set.args]
-                )
-                if isinstance(result, set):
-                    return len(result)
-            except (AttributeError, TypeError):
-                pass
-        return None
-
-
-class SetSum(Expression):
-    """Represents the sum of elements in a set-valued expression"""
-
-    def __init__(self, set_expr: Expression):
-        if not isinstance(set_expr, (Set, ConceptApplication)):
-            raise TypeError("SetSum can only be applied to set-valued expressions")
-        self.set_expr = set_expr
-
-    def to_lean4(self) -> str:
-        set_str = self.set_expr.to_lean4()
-        return f"(Finset.sum {set_str} id)"
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-    def evaluate(self) -> Optional[int]:
-        """
-        Attempts to evaluate the sum for concrete cases.
-        Returns:
-        - The sum of elements for concrete sets
-        - None if the sum cannot be determined (e.g., symbolic sets or concept applications)
-        """
-        if isinstance(self.set_expr, Set) and self.set_expr.elements is not None:
-            try:
-                return sum(e.evaluate() for e in self.set_expr.elements)
-            except AttributeError:
-                return None
-        elif isinstance(self.set_expr, ConceptApplication):
-            try:
-                # Try to compute the concept and sum its result if possible
-                result = self.set_expr.concept.compute(
-                    *[arg.evaluate() for arg in self.set_expr.args]
-                )
-                if isinstance(result, set):
-                    return sum(result)
-            except (AttributeError, TypeError):
-                pass
-        return None
-
-
 # =============================================================================
 # Natural Numbers Classes
 # =============================================================================
@@ -560,181 +233,41 @@ def evaluate(self) -> int:
         return self.value
 
 
-
-class NatDomain(Expression):
-    """Represents the domain/type of natural numbers"""
-
-    def to_lean4(self) -> str:
-        return "ℕ"  # Unicode for natural numbers
-
-    def to_z3(self) -> str:
-        return "NatSet"  # Z3 doesn't have built-in naturals, we use integers
-
-
-class GroupDomain(Expression):
-    """Represents the domain/type of groups"""
-
-    def to_lean4(self) -> str:
-        return "Group"
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class GroupElementDomain(Expression):
-    """Represents the domain/type of group elements"""
-
-    def to_lean4(self) -> str:
-        return "G"  # In Lean, groups are typically defined over a type 'G'
-
-    def to_z3(self) -> str:
-        # In Z3, group elements can be modeled as an uninterpreted sort 'G'
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class TupleDomain(SetDomain):
-    """
-    Represents a product domain for a tuple of quantified variables.
-    For example, in Lean: D1 × D2 × ...
-    """
-
-    def __init__(self, domains: "Union[List[Entity], Tuple[Entity, ...]]"):
-        # Convert to tuple to communicate immutability
-        self.domains = tuple(domains)
-
-    def to_lean4(self) -> str:
-        return " × ".join(d.to_lean4() for d in self.domains)
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class TupleExpr(Expression):
-    """
-    Represents a tuple of expressions.
-    For example: (x₁, x₂, ..., xₙ)
-    """
-
-    def __init__(self, elements: "Union[List[Expression], Tuple[Expression, ...]]"):
-        # Convert to tuple to communicate immutability
-        self.elements = tuple(elements)
-
-    def to_lean4(self) -> str:
-        # In Lean4, tuples are represented using parentheses and commas
-        elements_str = ", ".join(e.to_lean4() for e in self.elements)
-        return f"({elements_str})"
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
 # =============================================================================
-# Function Classes
+# Group Classes
 # =============================================================================
 
+class SetExpr(Expression):
+    """A set expression that can be evaluated to a Python set."""
 
-class Lambda(Expression):
-    """Represents a lambda/anonymous function"""
-
-    def __init__(self, var_name: str, body: Expression):
-        self.var_name = var_name
-        self.body = body
-
-    def to_lean4(self) -> str:
-        body = self.body.to_lean4()
-        return f"(λ {self.var_name} => {body})"
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class Apply(Expression):
-    """Represents function application"""
-
-    def __init__(self, fn: Expression, arg: Expression):
-        self.fn = fn
-        self.arg = arg
+    def __init__(
+        self,
+        domain: Expression,
+        elements: Optional[List[Expression]] = None,
+        predicate: Optional[Expression] = None,
+    ):
+        self.domain = domain
+        self.elements = elements
+        self.predicate = predicate
 
     def to_lean4(self) -> str:
-        return f"({self.fn.to_lean4()} {self.arg.to_lean4()})"
+        return NotImplementedError("to_lean4 is not yet implemented")
 
     def to_z3(self) -> str:
         return NotImplementedError("to_z3 is not yet implemented")
 
-
-class Equals(Expression):
-    """Represents mathematical equality between two expressions"""
-
-    def __init__(self, left: Expression, right: Expression):
-        self.left = left
-        self.right = right
-
-    def to_lean4(self) -> str:
-        left = self.left.to_lean4()
-        right = self.right.to_lean4()
-        return f"({left} = {right})"
-
-    def to_z3(self) -> Z3Template:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-    def evaluate(self) -> Optional[bool]:
-        """
-        Attempts to evaluate equality for concrete cases.
-        Returns:
-        - True/False for concrete cases (Nat and explicit Sets)
-        - None if equality cannot be determined (e.g., symbolic expressions or predicate-defined sets)
-        """
-        try:
-            # Handle Nat equality
-            if isinstance(self.left, Nat) and isinstance(self.right, Nat):
-                return self.left.evaluate() == self.right.evaluate()
-
-            if isinstance(self.left, FiniteFieldElement) and isinstance(self.right, FiniteFieldElement):
-                return self.left.evaluate() == self.right.evaluate()
-
-            # Handle explicit Set equality
-            if (
-                isinstance(self.left, Set)
-                and isinstance(self.right, Set)
-                and self.left.elements is not None
-                and self.right.elements is not None
-            ):
-                left_vals = self.left.evaluate()
-                right_vals = self.right.evaluate()
-                if left_vals is not None and right_vals is not None:
-                    return left_vals == right_vals
-
-            return None  # Cannot evaluate equality
-        except AttributeError:
+    def evaluate(self) -> Optional[set]:
+        """Evaluate the set expression to a Python set."""
+        if self.elements is not None:
+            return {e.evaluate() for e in self.elements}
+        elif self.predicate is not None:
+            # For now, we can't evaluate predicate-based sets
+            return None
+        else:
+            # For now, we can't evaluate domain-based sets
             return None
 
 
-class Fold(Expression):
-    """
-    Represents folding/iteration over natural numbers.
-    fold(n, base, f) represents applying f n times starting with base.
-    For example:
-    - Addition(a,b) = fold(b, a, succ)  # Add b to a by applying succ b times
-    - Multiplication(a,b) = fold(b, 0, λx.add(a,x))  # Add a to itself b times
-    """
-
-    def __init__(self, count: Expression, base: Expression, step_fn: Expression):
-        self.count = count  # How many times to apply step_fn
-        self.base = base  # Starting value
-        self.step_fn = step_fn  # Function to apply at each step
-
-    def to_lean4(self) -> str:
-        return f"(fold {self.count.to_lean4()} {self.base.to_lean4()} {self.step_fn.to_lean4()})"
-
-    def to_z3(self) -> str:
-        # Z3 doesn't have direct fold, we'd need to use recursion/quantifiers
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-# =============================================================================
-# Group Classes
-# =============================================================================
-
 
 class GroupElement(Expression):
     """Represents a group element, wrapping any value and providing a consistent interface."""
@@ -772,52 +305,19 @@ def __hash__(self) -> int:
         """Hash based on the underlying value."""
         return hash(self.value)
 
-
 class GroupElementDomain(Expression):
     """Represents the domain/type of group elements"""
 
     def to_lean4(self) -> str:
-        return "G"  # In Lean4, group elements are of type G
-
-    def to_z3(self) -> str:
-        return NotImplementedError("to_z3 is not yet implemented")
-
-
-class SetExpr(Expression):
-    """A set expression that can be evaluated to a Python set."""
-
-    def __init__(
-        self,
-        domain: Expression,
-        elements: Optional[List[Expression]] = None,
-        predicate: Optional[Expression] = None,
-    ):
-        self.domain = domain
-        self.elements = elements
-        self.predicate = predicate
+        return "G"  # In Lean, groups are typically defined over a type 'G'
 
-    def to_lean4(self) -> str:
-        if self.elements is not None:
-            return f"{{{', '.join(e.to_lean4() for e in self.elements)}}}"
-        elif self.predicate is not None:
-            return f"{{x : {self.domain.to_lean4()} | {self.predicate.to_lean4()}}}"
-        else:
-            return f"{{x : {self.domain.to_lean4()}}}"
+    def to_prolog(self) -> str:
+        return "group_element"  # A clear Prolog atom for group elements
 
     def to_z3(self) -> str:
+        # In Z3, group elements can be modeled as an uninterpreted sort 'G'
         return NotImplementedError("to_z3 is not yet implemented")
 
-    def evaluate(self) -> Optional[set]:
-        """Evaluate the set expression to a Python set."""
-        if self.elements is not None:
-            return {e.evaluate() for e in self.elements}
-        elif self.predicate is not None:
-            # For now, we can't evaluate predicate-based sets
-            return None
-        else:
-            # For now, we can't evaluate domain-based sets
-            return None
-
 
 class Group(Expression):
     """
diff --git a/frame/knowledge_base/initial_concepts.py b/frame/knowledge_base/initial_concepts.py
index c144706..be79e43 100644
--- a/frame/knowledge_base/initial_concepts.py
+++ b/frame/knowledge_base/initial_concepts.py
@@ -5,8 +5,7 @@
 
 from frame.knowledge_base.entities import (
     Concept, ExampleStructure, ExampleType, ConceptType,
-    Zero, Succ, Nat, Fold, Lambda, Var, Exists, NatDomain, Equals,
-    ConceptApplication, FiniteField, FiniteFieldElement, DEFAULT_FINITE_FIELD
+    Zero, Succ, Nat, FiniteField, FiniteFieldElement, DEFAULT_FINITE_FIELD
 )
 from frame.tools.z3_template import Z3Template
 
diff --git a/frame/productions/concepts/compose.py b/frame/productions/concepts/compose.py
index 60f0179..3701bba 100644
--- a/frame/productions/concepts/compose.py
+++ b/frame/productions/concepts/compose.py
@@ -35,7 +35,6 @@
 from typing import List, Optional, Tuple, Any, Dict, Type, Union
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    And,
     Entity,
     Concept,
     ExampleStructure,
diff --git a/frame/productions/concepts/constant.py b/frame/productions/concepts/constant.py
index a9302b2..ed87da2 100644
--- a/frame/productions/concepts/constant.py
+++ b/frame/productions/concepts/constant.py
@@ -14,7 +14,6 @@
     ExampleType,
     ExampleStructure,
     ConceptType,
-    ConceptApplication,
 )
 from frame.tools.z3_template import Z3Template
 
diff --git a/frame/productions/concepts/exists.py b/frame/productions/concepts/exists.py
index 5e201d9..0eb7faf 100644
--- a/frame/productions/concepts/exists.py
+++ b/frame/productions/concepts/exists.py
@@ -11,17 +11,11 @@
 
 from frame.knowledge_base.entities import (
     Expression,
-    Exists,
-    Var,
-    ConceptApplication,
-    NatDomain,
-    And,
     Entity,
     Concept,
     ExampleType,
     ExampleStructure,
     ConceptType,
-    Equals,
     DEFAULT_FINITE_FIELD,
     FiniteFieldElement,
 )
diff --git a/frame/productions/concepts/forall.py b/frame/productions/concepts/forall.py
index 9cad2a3..10d0b22 100644
--- a/frame/productions/concepts/forall.py
+++ b/frame/productions/concepts/forall.py
@@ -12,24 +12,12 @@
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
     Expression,
-    Var,
-    ConceptApplication,
-    Forall,
     Entity,
     Concept,
     Conjecture,
     ExampleType,
     ExampleStructure,
     ConceptType,
-    Implies,
-)
-
-# Import default domains for each type of concept.
-from frame.knowledge_base.entities import (
-    NatDomain,
-    GroupDomain,
-    SetDomain,
-    GroupElementDomain,
 )
 
 from frame.tools.z3_template import Z3Template, _format_args
@@ -592,9 +580,6 @@ def _apply_single_predicate(
             # Determine which indices to keep (not quantified)
             kept_indices = [i for i in range(concept_arity) if i not in indices_to_quantify]
 
-            # Infer domains
-            # domains = self._infer_domains(concept, indices_to_quantify)
-
             # Create a new concept with reduced arity
             concept_types = concept.get_component_types()
             new_types = tuple(concept_types[i] for i in kept_indices)
@@ -648,22 +633,11 @@ def _apply_single_predicate(
             return new_concept
         
         else: # quantifying over every arg, create a conjecture
-            # Infer domains
-            # domains = self._infer_domains(concept, indices_to_quantify)
-
             # Get verification capabilities from the rule
             can_add_examples, can_add_nonexamples = (
                 self.determine_verification_capabilities(concept)
             )
 
-            # Create variables for quantification
-            vars = [Var(f"x{i}") for i in range(concept_arity)]
-            
-            # Wrap with universal quantifiers
-            expr = ConceptApplication(concept, vars)
-            for i in reversed(range(concept_arity)):
-                expr = Forall(f"x{i}", NatDomain(), expr)
-                # expr = Forall(f"x{i}", domains, expr)
         
             quantified_types = concept.get_component_types()
             new_conjecture = Conjecture(
@@ -761,7 +735,6 @@ def _apply_two_predicates(
                 "origin": "primary_unique",
                 "primary_idx": i,
                 "role": None, # Determined later
-                "var_obj": Var(var_id)
             }
             distinct_logical_vars_ordered_ids.append(var_id)
             var_counter += 1
@@ -776,7 +749,6 @@ def _apply_two_predicates(
                 "origin": "secondary_unique",
                 "secondary_idx": i,
                 "role": None, # Determined later
-                "var_obj": Var(var_id)
             }
             distinct_logical_vars_ordered_ids.append(var_id)
             var_counter += 1
@@ -794,7 +766,6 @@ def _apply_two_predicates(
                 "primary_idx": i,
                 "secondary_idx": secondary_idx,
                 "role": None, # Determined later
-                "var_obj": Var(var_id)
             }
             distinct_logical_vars_ordered_ids.append(var_id)
             var_counter += 1
@@ -925,27 +896,6 @@ def _apply_two_predicates(
             )
 
         return new_entity
-
-    def _infer_domains(self, var_types: List[ExampleType]) -> List[Entity]:
-        """Infer domains for the given variable types."""
-        # map from component type to domain
-        component_to_domain_map = {
-            ExampleType.NUMERIC: NatDomain(),
-            ExampleType.GROUPELEMENT: GroupElementDomain(),
-            ExampleType.GROUP: GroupDomain(),
-            ExampleType.SET: SetDomain(),
-            ExampleType.FUNCTION: NotImplementedError(
-                "Function domains not handled yet"
-            ),
-        }
-        domains = []
-        # Infer domains for each type
-        for var_type in var_types:
-            domain = component_to_domain_map.get(var_type)
-            if domain is None:
-                 raise NotImplementedError(f"Domain inference not implemented for type {var_type}")
-            domains.append(domain)
-        return domains
     
     def _z3_translate_forall_two_predicates(
             self,
diff --git a/frame/productions/concepts/map_iterate.py b/frame/productions/concepts/map_iterate.py
index 11106c9..2442e37 100644
--- a/frame/productions/concepts/map_iterate.py
+++ b/frame/productions/concepts/map_iterate.py
@@ -10,10 +10,6 @@
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
     Expression,
-    Lambda,
-    Var,
-    ConceptApplication,
-    Fold,
     Entity,
     Concept,
     Example,
diff --git a/frame/productions/concepts/match.py b/frame/productions/concepts/match.py
index bee201e..37bb40c 100644
--- a/frame/productions/concepts/match.py
+++ b/frame/productions/concepts/match.py
@@ -10,7 +10,6 @@
 from itertools import combinations
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    ConceptApplication,
     Entity,
     Concept,
     ExampleStructure,
diff --git a/frame/productions/concepts/negate.py b/frame/productions/concepts/negate.py
index 20f81bd..522133f 100644
--- a/frame/productions/concepts/negate.py
+++ b/frame/productions/concepts/negate.py
@@ -5,8 +5,6 @@
 from typing import List, Optional, Tuple, Any, Dict, Type, Union
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    Not,
-    ConceptApplication,
     Entity,
     Concept,
     ConceptType,
diff --git a/frame/productions/concepts/size.py b/frame/productions/concepts/size.py
index 9985a77..eeeafc4 100644
--- a/frame/productions/concepts/size.py
+++ b/frame/productions/concepts/size.py
@@ -5,20 +5,11 @@
 from typing import Optional, Tuple, List, Set, Any, Dict, Type, Union
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    ConceptApplication,
-    GroupDomain,
-    NatDomain,
-    SetDomain,
-    GroupElementDomain,
     Entity,
     Concept,
     ExampleType,
     ExampleStructure,
     ConceptType,
-    Set,
-    SetCardinality,
-    Lambda,
-    TupleDomain,
 )
 from itertools import combinations
 
diff --git a/frame/productions/concepts/specialize.py b/frame/productions/concepts/specialize.py
index 781c972..6f5adc3 100644
--- a/frame/productions/concepts/specialize.py
+++ b/frame/productions/concepts/specialize.py
@@ -5,13 +5,10 @@
 from typing import List, Optional, Tuple, Any, Dict, Type, Union
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    ConceptApplication,
     Entity,
     Concept,
     ExampleStructure,
     ConceptType,
-    Equals,
-    Nat,
 )
 
 from frame.tools.z3_template import Z3Template, _format_args
diff --git a/frame/productions/conjectures/equivalence.py b/frame/productions/conjectures/equivalence.py
index cc63272..cf3d226 100644
--- a/frame/productions/conjectures/equivalence.py
+++ b/frame/productions/conjectures/equivalence.py
@@ -8,13 +8,10 @@
 
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    Expression, Var, ConceptApplication, Forall, NatDomain,
-    Entity, Concept, Conjecture, Example, ExampleType, ExampleStructure, ConceptType,
-    Equals, Implies, And, Exists, Nat, Fold, Lambda
+    Entity, Concept, Conjecture, Example, ExampleType, ExampleStructure, ConceptType, Nat
 )
 from frame.tools.z3_template import Z3Template, _format_args
 from frame.knowledge_base.demonstrations import addition, is_even, divides, multiplication
-from frame.knowledge_base.entities import Succ, Zero
 
 MAX_SEARCH_LIMIT = 100
 MAX_VALUE_PER_VAR = 5
@@ -246,34 +243,6 @@ def apply(self, *inputs: Entity) -> Entity:
         # Determine verification capabilities
         can_add_examples, can_add_nonexamples = self.determine_verification_capabilities(*inputs)
         
-        # Create variables for quantification
-        vars = [Var(f"x{i}") for i in range(arity)]
-        
-        # Build the equivalence expression
-        if is_predicate:
-            # For predicates: P ↔ Q is equivalent to (P → Q) ∧ (Q → P)
-            equiv_expr = And(
-                Implies(
-                    ConceptApplication(concept1, *vars),
-                    ConceptApplication(concept2, *vars)
-                ),
-                Implies(
-                    ConceptApplication(concept2, *vars),
-                    ConceptApplication(concept1, *vars)
-                )
-            )
-        else:
-            # For functions: direct equality
-            input_arity = concept1.examples.example_structure.input_arity
-            equiv_expr = Equals(
-                ConceptApplication(concept1, *vars[:input_arity]),  # Only use input variables
-                ConceptApplication(concept2, *vars[:input_arity])   # Only use input variables
-            )
-        
-        # Wrap with universal quantifiers
-        expr = equiv_expr
-        for i in reversed(range(arity)):
-            expr = Forall(f"x{i}", NatDomain(), expr)
         
         component_types = concept1.get_component_types()
         is_finite_field = any(typ == ExampleType.FINITEFIELD_ELEMENT for typ in component_types)
diff --git a/frame/productions/conjectures/exclusivity.py b/frame/productions/conjectures/exclusivity.py
index 20b6852..80ed1b5 100644
--- a/frame/productions/conjectures/exclusivity.py
+++ b/frame/productions/conjectures/exclusivity.py
@@ -14,10 +14,8 @@
 
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    Expression, Var, ConceptApplication, Forall, NatDomain,
-    Entity, Concept, Conjecture, Example, ExampleType, ExampleStructure, ConceptType,
-    Equals, Implies, Not, And, Exists, Nat, Fold, Lambda,
-    In, Set as SetExpr, TupleDomain, TupleExpr,
+    Entity, Concept, Conjecture, Example, 
+    ExampleType, ExampleStructure, ConceptType, Nat, SetExpr,
 )
 from frame.knowledge_base.demonstrations import (
     is_prime, is_even
@@ -188,9 +186,6 @@ def apply(self, *inputs: Entity, valid_set: Optional[Set] = None, target_value:
             *inputs, valid_set=valid_set, target_value=target_value
         )
         
-        # Create variables for quantification
-        vars = [Var(f"x{i}") for i in range(arity)]
-
         # Convert Python set of tuples to Expression Set
         # First create the domain for tuples of the right arity
         component_types = concept.get_component_types()
@@ -202,46 +197,6 @@ def _wrap_value(val, val_type):
                 return val # FiniteFieldElement is already an expression
             return val
 
-        tuple_domain = TupleDomain([NatDomain() for _ in range(arity)])
-        
-        # Convert each tuple in valid_set to a tuple of Nat expressions
-        valid_tuples = [TupleExpr([_wrap_value(x, component_types[i]) for i, x in enumerate(t)]) for t in valid_set]
-        valid_set_expr = SetExpr(tuple_domain, elements=valid_tuples)
-        
-        # Build the exclusivity expression
-        if concept.examples.example_structure.concept_type == ConceptType.PREDICATE:
-            # For predicates: P(x₁,...,xₙ) ↔ (x₁,...,xₙ) ∈ S
-            exclusivity_expr = And(
-                Implies( # (P → in_set)
-                    ConceptApplication(concept, *vars), 
-                    In(TupleExpr(vars), valid_set_expr),  # Use ExprTuple
-                ),
-                Implies( # (in_set → P)
-                    In(TupleExpr(vars), valid_set_expr),  # Use ExprTuple
-                    ConceptApplication(concept, *vars),
-                ),
-            )
-            name_suffix = ""
-        else:
-            # For functions: f(x₁,...,xₙ) = v ↔ (x₁,...,xₙ) ∈ S
-            exclusivity_expr = And(
-                Implies(
-                    Equals(ConceptApplication(concept, *vars), Nat(target_value)),
-                    In(TupleExpr(vars), valid_set_expr),  # Use ExprTuple
-                ),
-                Implies(
-                    In(TupleExpr(vars), valid_set_expr),  # Use ExprTuple
-                    Equals(ConceptApplication(concept, *vars), Nat(target_value)),
-                ),
-            )
-            name_suffix = f"_equals_{target_value}"
-
-        
-        # Note(George; 2/18): If we expand quantification to support many variables without nesting, modify here.
-        # Wrap with universal quantifiers
-        expr = exclusivity_expr
-        for i in reversed(range(arity)):
-            expr = Forall(f"x{i}", NatDomain(), expr)
         
         component_types = concept.get_component_types()
         is_finite_field = any(typ == ExampleType.FINITEFIELD_ELEMENT for typ in component_types)
@@ -288,6 +243,12 @@ def impl():
                 return True
             computational_impl = impl
 
+        # Build the exclusivity expression
+        if concept.examples.example_structure.concept_type == ConceptType.PREDICATE:
+            name_suffix = ""
+        else:
+            name_suffix = f"_equals_{target_value}"
+
         # Create the conjecture with the same example structure as the input concept
         conjecture = Conjecture(
             name=f"excl_({concept.name}{name_suffix}_{valid_set})",
diff --git a/frame/productions/conjectures/implication.py b/frame/productions/conjectures/implication.py
index 3ba8030..9f579f6 100644
--- a/frame/productions/conjectures/implication.py
+++ b/frame/productions/conjectures/implication.py
@@ -5,9 +5,7 @@
 from typing import List, Optional, Set, Tuple, Any, Dict, Type
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    Expression, Var, ConceptApplication, Forall, NatDomain,
     Entity, Concept, Conjecture, Example, ExampleType, ExampleStructure, ConceptType,
-    Equals, Implies, And, Exists, Nat, Fold, Lambda
 )
 import logging
 from frame.tools.z3_template import Z3Template, _format_args
@@ -211,20 +209,6 @@ def apply(self, *inputs: Entity) -> Entity:
         
         # Determine verification capabilities
         can_add_examples, can_add_nonexamples = self.determine_verification_capabilities(*inputs)
-        
-        # Create variables for quantification
-        vars = [Var(f"x{i}") for i in range(arity)]
-        
-        # Build the implication expression
-        impl_expr = Implies(
-            ConceptApplication(concept1, *vars),
-            ConceptApplication(concept2, *vars)
-        )
-        
-        # Wrap with universal quantifiers
-        expr = impl_expr
-        for i in reversed(range(arity)):
-            expr = Forall(f"x{i}", NatDomain(), expr)
 
         component_types = concept1.get_component_types()
         is_finite_field = any(typ == ExampleType.FINITEFIELD_ELEMENT for typ in component_types)
diff --git a/frame/productions/conjectures/nonexistence.py b/frame/productions/conjectures/nonexistence.py
index 086837d..c2edaef 100644
--- a/frame/productions/conjectures/nonexistence.py
+++ b/frame/productions/conjectures/nonexistence.py
@@ -13,9 +13,7 @@
 
 from frame.productions.base import ProductionRule
 from frame.knowledge_base.entities import (
-    Expression, Var, ConceptApplication, Forall, NatDomain,
     Entity, Concept, Conjecture, Example, ExampleType, ExampleStructure, ConceptType,
-    Equals, Not, And, Exists, Nat
 )
 from frame.knowledge_base.demonstrations import (
     is_perfect, is_odd, is_prime, multiplication, addition
@@ -252,23 +250,6 @@ def apply(self, *inputs: Entity) -> Entity:
         # Determine verification capabilities
         can_add_examples, can_add_nonexamples = self.determine_verification_capabilities(*inputs)
         
-        # Create variables for quantification
-        vars = [Var(f"x{i}") for i in range(arity)]
-        
-        # Build the nonexistence expression
-        if concept.examples.example_structure.concept_type == ConceptType.PREDICATE:
-            nonexist_expr = Not(ConceptApplication(concept, *vars))
-            name_suffix = ""
-        else:
-            nonexist_expr = Not(
-                Equals(ConceptApplication(concept, *vars), ConceptApplication(target_concept))
-            )
-            name_suffix = f"_equals_{target_concept.name}"
-        
-        # Wrap with universal quantifiers
-        expr = nonexist_expr
-        for i in reversed(range(arity)):
-            expr = Forall(f"x{i}", NatDomain(), expr)
         
         component_types = concept.get_component_types()
         is_finite_field = any(typ == ExampleType.FINITEFIELD_ELEMENT for typ in component_types)
@@ -308,6 +289,13 @@ def impl():
                 return True
             computational_impl = impl
 
+        # Build the nonexistence expression
+        if concept.examples.example_structure.concept_type == ConceptType.PREDICATE:
+            name_suffix = ""
+        else:
+            name_suffix = f"_equals_{target_concept.name}"
+
+
         # Create the conjecture with the same example structure as the input concept
         conjecture = Conjecture(
             name=f"no_({concept.name}{name_suffix})",
diff --git a/tests/productions/conftest.py b/tests/productions/conftest.py
index dc61c61..aae4e89 100644
--- a/tests/productions/conftest.py
+++ b/tests/productions/conftest.py
@@ -5,30 +5,20 @@
 from frame.productions.concepts.specialize import SpecializeRule
 from frame.productions.concepts.size import SizeRule
 from frame.knowledge_base.entities import (
-    ConceptApplication,
     Concept,
     ExampleType,
     ExampleStructure,
     ConceptType,
-    Set,
-    NatDomain,
-    Equals,
-    Exists,
-    And,
-    Lambda,
     Zero,
     Succ,
     Nat,
-    Var,
     GroupElement,
-    Not,
     DEFAULT_FINITE_FIELD,
     FiniteFieldElement,
 )
 from frame.knowledge_base.demonstrations import (
     multiplication,
     addition,
-    SetCardinality,
     proper_divisors,
     divides,
     less_than,
@@ -924,7 +914,7 @@ def divisor_mod_k_equals_r():
 @pytest.fixture
 def commutes():
     """Create a concept that tests if two elements commute under group operation."""
-    from frame.knowledge_base.entities import Equals, Apply, Z2, Z3, S3
+    from frame.knowledge_base.entities import Z2, Z3, S3
 
     concept = Concept(
         name="commutes",
diff --git a/tests/productions/test_match.py b/tests/productions/test_match.py
index 49d68b1..ca2169b 100644
--- a/tests/productions/test_match.py
+++ b/tests/productions/test_match.py
@@ -2,7 +2,6 @@
 
 from frame.productions.concepts.match import MatchRule
 from frame.knowledge_base.entities import (
-    ConceptApplication,
     Concept,
     ExampleType,
     ExampleStructure,
@@ -10,7 +9,7 @@
     Nat,
     FiniteFieldElement,
 )
-from frame.knowledge_base.demonstrations import multiplication, addition, SetCardinality
+from frame.knowledge_base.demonstrations import multiplication, addition
 from frame.tools.z3_template import Z3Template
 
 @pytest.fixture
diff --git a/tests/productions/test_negate.py b/tests/productions/test_negate.py
index 8f3da7c..1fe749c 100644
--- a/tests/productions/test_negate.py
+++ b/tests/productions/test_negate.py
@@ -1,7 +1,7 @@
 import pytest
 
 from frame.productions.concepts.negate import NegateRule
-from frame.knowledge_base.entities import Conjecture, ConceptType, Var, Nat
+from frame.knowledge_base.entities import Conjecture, ConceptType, Nat
 
 # ==============================
 # Fixtures
diff --git a/tests/productions/test_size.py b/tests/productions/test_size.py
index 65f3b23..d43ff40 100644
--- a/tests/productions/test_size.py
+++ b/tests/productions/test_size.py
@@ -8,12 +8,6 @@
     ExampleStructure,
 )
 
-from frame.knowledge_base.entities import (
-    ConceptApplication,
-    Nat,
-    Var,
-)
-
 from frame.knowledge_base.demonstrations import (
     addition,
 )
diff --git a/tests/productions/test_specialize.py b/tests/productions/test_specialize.py
index a1d5cf0..1358d6b 100644
--- a/tests/productions/test_specialize.py
+++ b/tests/productions/test_specialize.py
@@ -5,15 +5,6 @@
     ExampleType,
     ExampleStructure,
     Nat,
-    NatDomain,
-    Var,
-    Equals,
-    Exists,
-    ConceptApplication,
-    SetCardinality,
-    Set,
-    Lambda,
-    And,
     Zero,
     Succ,
     DEFAULT_FINITE_FIELD,
diff --git a/tests/test_knowledge_graph.py b/tests/test_knowledge_graph.py
index f065b7c..404d199 100644
--- a/tests/test_knowledge_graph.py
+++ b/tests/test_knowledge_graph.py
@@ -33,17 +33,9 @@
     ExampleStructure,
     ConceptType,
     Expression,
-    Var,
-    ConceptApplication,
     Succ,
     Zero,
     Nat,
-    Exists,
-    And,
-    Not,
-    Equals,
-    Lambda,
-    Fold,
     ExampleCollection,
 )
 from frame.interestingness.learning.dsl_primitives import get_entity_step_age
diff --git a/tests/test_math_env_nat.py b/tests/test_math_env_nat.py
index 20c0ebc..3655328 100644
--- a/tests/test_math_env_nat.py
+++ b/tests/test_math_env_nat.py
@@ -22,12 +22,8 @@
     ExampleType,
     ExampleStructure,
     ConceptType,
-    Expression,
-    Var,
-    ConceptApplication,
-    Succ,
     Nat,
-    Conjecture,
+    SetExpr
 )
 from frame.knowledge_base.demonstrations import is_prime
 from frame.productions.concepts.map_iterate import MapIterateRule