def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
        """Replace all instances of variable v with expression E in self,
        where v is free in self."""
        first = self.first
        second = self.second
        consequent = self.consequent

        # If variable is bound
        if variable in self.get_refs():
            if replace_bound:
                first  = first.replace(variable, expression, replace_bound, alpha_convert)
                second = second.replace(variable, expression, replace_bound, alpha_convert)
                if consequent:
                    consequent = consequent.replace(variable, expression, replace_bound, alpha_convert)
        else:
            if alpha_convert:
                # alpha convert every ref that is free in 'expression'
                for ref in (set(self.get_refs(True)) & expression.free()):
                    v = DrtVariableExpression(unique_variable(ref))
                    first  = first.replace(ref, v, True, alpha_convert)
                    second = second.replace(ref, v, True, alpha_convert)
                    if consequent:
                        consequent = consequent.replace(ref, v, True, alpha_convert)

            first  = first.replace(variable, expression, replace_bound, alpha_convert)
            second = second.replace(variable, expression, replace_bound, alpha_convert)
            if consequent:
                consequent = consequent.replace(variable, expression, replace_bound, alpha_convert)

        return self.__class__(first, second, consequent)

    def _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug):
        try:
            current._used_vars
        except AttributeError:
            current._used_vars = set()

        #if there are accessible_vars on the path
        if accessible_vars:
            # get the set of bound variables that have not be used by this AllExpression
            bv_available = accessible_vars - current._used_vars

            if bv_available:
                variable_to_use = list(bv_available)[0]
                debug.line('--> Using \'%s\'' % variable_to_use, 2)
                current._used_vars |= set([variable_to_use])
                agenda.put(current.term.replace(current.variable, variable_to_use), context)
                agenda[Categories.ALL].add((current,context))
                return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)

            else:
                #no more available variables to substitute
                debug.line('--> Variables Exhausted', 2)
                current._exhausted = True
                agenda[Categories.ALL].add((current,context))
                return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)

        else:
            new_unique_variable = VariableExpression(unique_variable())
            debug.line('--> Using \'%s\'' % new_unique_variable, 2)
            current._used_vars |= set([new_unique_variable])
            agenda.put(current.term.replace(current.variable, new_unique_variable), context)
            agenda[Categories.ALL].add((current,context))
            agenda.mark_alls_fresh()
            return self._attempt_proof(agenda, accessible_vars|set([new_unique_variable]), atoms, debug+1)

 def _make_unique_signature(self, predHolder):
     """
     This method figures out how many arguments the predicate takes and
     returns a tuple containing that number of unique variables.
     """
     return tuple([unique_variable()
                   for i in range(predHolder.signature_len)])

 def _attempt_proof_some(
     self, current, context, agenda, accessible_vars, atoms, debug
 ):
     new_unique_variable = VariableExpression(unique_variable())
     agenda.put(current.term.replace(current.variable, new_unique_variable), context)
     agenda.mark_alls_fresh()
     return self._attempt_proof(
         agenda, accessible_vars | set([new_unique_variable]), atoms, debug + 1
     )

def clausify(expression):
    """
    Skolemize, clausify, and standardize the variables apart.
    """
    clause_list = []
    for clause in _clausify(skolemize(expression)):
        for free in clause.free():
            if is_indvar(free.name):
                newvar = VariableExpression(unique_variable())
                clause = clause.replace(free, newvar)
        clause_list.append(clause)
    return clause_list

    def simplify(self):
        first = self.first.simplify()
        second = self.second.simplify()
        consequent = (self.consequent.simplify() if self.consequent else None)

        if isinstance(first, DRS) and isinstance(second, DRS):
            # For any ref that is in both 'first' and 'second'
            for ref in (set(first.get_refs(True)) & set(second.get_refs(True))):
                # alpha convert the ref in 'second' to prevent collision
                newvar = DrtVariableExpression(unique_variable(ref))
                second = second.replace(ref, newvar, True)

            return DRS(first.refs + second.refs, first.conds + second.conds, consequent)
        else:
            return self.__class__(first, second, consequent)

    def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
        """Replace all instances of variable v with expression E in self,
        where v is free in self."""
        if variable in self.refs:
            # if a bound variable is the thing being replaced
            if not replace_bound:
                return self
            else:
                i = self.refs.index(variable)
                if self.consequent:
                    consequent = self.consequent.replace(variable, expression, True, alpha_convert)
                else:
                    consequent = None
                return DRS(
                    self.refs[:i] + [expression.variable] + self.refs[i + 1 :],
                    [cond.replace(variable, expression, True, alpha_convert) for cond in self.conds],
                    consequent,
                )
        else:
            if alpha_convert:
                # any bound variable that appears in the expression must
                # be alpha converted to avoid a conflict
                for ref in set(self.refs) & expression.free():
                    newvar = unique_variable(ref)
                    newvarex = DrtVariableExpression(newvar)
                    i = self.refs.index(ref)
                    if self.consequent:
                        consequent = self.consequent.replace(ref, newvarex, True, alpha_convert)
                    else:
                        consequent = None
                    self = DRS(
                        self.refs[:i] + [newvar] + self.refs[i + 1 :],
                        [cond.replace(ref, newvarex, True, alpha_convert) for cond in self.conds],
                        consequent,
                    )

            # replace in the conditions
            if self.consequent:
                consequent = self.consequent.replace(variable, expression, replace_bound, alpha_convert)
            else:
                consequent = None
            return DRS(
                self.refs,
                [cond.replace(variable, expression, replace_bound, alpha_convert) for cond in self.conds],
                consequent,
            )

 def inst_vars(self, edge):
     return dict((var, logic.unique_variable())
                 for var in edge.lhs().variables()
                 if var.name.startswith('@'))

def skolemize(expression, univ_scope=None, used_variables=None):
    """
    Skolemize the expression and convert to conjunctive normal form (CNF)
    """
    if univ_scope is None:
        univ_scope = set()
    if used_variables is None:
        used_variables = set()

    if isinstance(expression, AllExpression):
        term = skolemize(expression.term, univ_scope|set([expression.variable]), used_variables|set([expression.variable]))
        return term.replace(expression.variable, VariableExpression(unique_variable(ignore=used_variables)))
    elif isinstance(expression, AndExpression):
        return skolemize(expression.first, univ_scope, used_variables) &\
               skolemize(expression.second, univ_scope, used_variables)
    elif isinstance(expression, OrExpression):
        return to_cnf(skolemize(expression.first, univ_scope, used_variables),
                      skolemize(expression.second, univ_scope, used_variables))
    elif isinstance(expression, ImpExpression):
        return to_cnf(skolemize(-expression.first, univ_scope, used_variables),
                      skolemize(expression.second, univ_scope, used_variables))
    elif isinstance(expression, IffExpression):
        return to_cnf(skolemize(-expression.first, univ_scope, used_variables),
                      skolemize(expression.second, univ_scope, used_variables)) &\
               to_cnf(skolemize(expression.first, univ_scope, used_variables),
                      skolemize(-expression.second, univ_scope, used_variables))
    elif isinstance(expression, EqualityExpression):
        return expression
    elif isinstance(expression, NegatedExpression):
        negated = expression.term
        if isinstance(negated, AllExpression):
            term = skolemize(-negated.term, univ_scope, used_variables|set([negated.variable]))
            if univ_scope:
                return term.replace(negated.variable, skolem_function(univ_scope))
            else:
                skolem_constant = VariableExpression(unique_variable(ignore=used_variables))
                return term.replace(negated.variable, skolem_constant)
        elif isinstance(negated, AndExpression):
            return to_cnf(skolemize(-negated.first, univ_scope, used_variables),
                          skolemize(-negated.second, univ_scope, used_variables))
        elif isinstance(negated, OrExpression):
            return skolemize(-negated.first, univ_scope, used_variables) &\
                   skolemize(-negated.second, univ_scope, used_variables)
        elif isinstance(negated, ImpExpression):
            return skolemize(negated.first, univ_scope, used_variables) &\
                   skolemize(-negated.second, univ_scope, used_variables)
        elif isinstance(negated, IffExpression):
            return to_cnf(skolemize(-negated.first, univ_scope, used_variables),
                          skolemize(-negated.second, univ_scope, used_variables)) &\
                   to_cnf(skolemize(negated.first, univ_scope, used_variables),
                          skolemize(negated.second, univ_scope, used_variables))
        elif isinstance(negated, EqualityExpression):
            return expression
        elif isinstance(negated, NegatedExpression):
            return skolemize(negated.term, univ_scope, used_variables)
        elif isinstance(negated, ExistsExpression):
            term = skolemize(-negated.term, univ_scope|set([negated.variable]), used_variables|set([negated.variable]))
            return term.replace(negated.variable, VariableExpression(unique_variable(ignore=used_variables)))
        elif isinstance(negated, ApplicationExpression):
            return expression
        else:
            raise Exception('\'%s\' cannot be skolemized' % expression)
    elif isinstance(expression, ExistsExpression):
        term = skolemize(expression.term, univ_scope, used_variables|set([expression.variable]))
        if univ_scope:
            return term.replace(expression.variable, skolem_function(univ_scope))
        else:
            skolem_constant = VariableExpression(unique_variable(ignore=used_variables))
            return term.replace(expression.variable, skolem_constant)
    elif isinstance(expression, ApplicationExpression):
        return expression
    else:
        raise Exception('\'%s\' cannot be skolemized' % expression)

 def inst_vars(self, edge):
     return dict((var, unique_variable(self.counter).variable)
                 for var in edge.lhs().variables()
                 if var.name.startswith('@'))