def is_var(t):
    return isinstance(t, str) and t[0].islower()        # variables: lowercase; constants: Capitalised

def substitute(t, theta):
    if is_var(t):
        return substitute(theta[t], theta) if t in theta else t
    if isinstance(t, tuple):
        return tuple(substitute(a, theta) for a in t)
    return t

def occurs(var, t, theta):
    t = substitute(t, theta)
    return t == var or (isinstance(t, tuple) and any(occurs(var, a, theta) for a in t))

def unify(x, y, theta):
    if theta is None:
        return None
    x, y = substitute(x, theta), substitute(y, theta)
    if x == y:
        return theta
    if is_var(x):
        return None if occurs(x, y, theta) else {**theta, x: y}      # occurs check
    if is_var(y):
        return unify(y, x, theta)
    if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y):
        for a, b in zip(x, y):
            theta = unify(a, b, theta)
        return theta
    return None

def show(theta):
    return theta if theta is None else {v: substitute(v, theta) for v in theta}

q = ("Knows", "John", "x")
print(show(unify(q, ("Knows", "John", "Jane"), {})))               # {'x': 'Jane'}
print(show(unify(q, ("Knows", "y", "Bill"), {})))                  # {'y': 'John', 'x': 'Bill'}
print(show(unify(q, ("Knows", "y", ("Mother", "y")), {})))         # {'y': 'John', 'x': ('Mother', 'John')}
print(show(unify(q, ("Knows", "x", "Elizabeth"), {})))             # None ← x can't be John and Elizabeth
print(show(unify(q, ("Knows", "x2", "Elizabeth"), {})))            # {'x2': 'John', 'x': 'Elizabeth'} ← fixed by standardising apart

FACTS = {("American", "West"), ("Missile", "M1"), ("Owns", "Nono", "M1"), ("Enemy", "Nono", "America")}
RULES = [
    ([("American", "x"), ("Weapon", "y"), ("Sells", "x", "y", "z"), ("Hostile", "z")], ("Criminal", "x")),
    ([("Missile", "x"), ("Owns", "Nono", "x")], ("Sells", "West", "x", "Nono")),
    ([("Missile", "x")], ("Weapon", "x")),
    ([("Enemy", "x", "America")], ("Hostile", "x")),
]

def match(pattern, fact, theta):                   # one-way unification: variables only in the pattern
    if len(pattern) != len(fact) or pattern[0] != fact[0]:
        return None
    theta = dict(theta)
    for p, f in zip(pattern[1:], fact[1:]):
        if p[0].islower():
            if theta.setdefault(p, f) != f:
                return None
        elif p != f:
            return None
    return theta

def solutions(premises, facts, theta):
    if not premises:
        yield theta
        return
    for fact in sorted(facts):
        t = match(premises[0], fact, theta)
        if t is not None:
            yield from solutions(premises[1:], facts, t)

def forward_chain(facts, rules):
    facts, rounds = set(facts), []
    while True:
        new = {tuple(theta.get(a, a) for a in concl)
               for prem, concl in rules for theta in solutions(prem, facts, {})} - facts
        if not new:
            return facts, rounds
        rounds.append(sorted(new))
        facts |= new

facts, rounds = forward_chain(FACTS, RULES)
print(rounds[0])                                   # [('Hostile', 'Nono'), ('Sells', 'West', 'M1', 'Nono'), ('Weapon', 'M1')]
print(rounds[1])                                   # [('Criminal', 'West')]
print(("Criminal", "West") in facts)               # True