#!/usr/bin/env python
# coding: utf-8

# In[1]:


from collections import defaultdict, deque


# ## algorithm

# In[2]:


def knowledge_base(formulas):
    rules, variable, dependency = [], defaultdict(bool), defaultdict(list)

    def _clause(formula):
        # A, B, C => P
        neg, pos = formula.replace(' ', '').split('=>')
        neg, pos = set(neg.split('&')) - {''}, pos or None

        # add rule
        rules.append((neg, pos))
        
        # set variable and track dependencies
        for i in neg:
            dependency[i].append((neg, pos))

    # parse formulas and build knowledge base
    deque((_clause(i) for i in formulas.split('\n') if i), 0)
    
    return rules, variable, dependency


# In[3]:


def resolution(rules, variable, dependency):
    # initial variables that have to be satisfied
    to_satisfy = [(neg, pos) for neg, pos in rules if not neg]

    while to_satisfy:
        neg, pos = to_satisfy.pop()

        # contradiction: true => false
        if not pos:
            return False

        # satisfy variable
        variable[pos] = True

        # update dependent rules
        for d_neg, d_pos in dependency[pos]:
            d_neg.remove(pos)
            
            # next variable to be satisfied
            if not d_neg and d_pos not in variable:
                to_satisfy.append((d_neg, d_pos))

    return True


# In[4]:


def hornsat(formulas):
    rules, variable, dependency = knowledge_base(formulas)
    satisfiable = resolution(rules, variable, dependency)

    print(['CONTRADICTION', 'SATISFIABLE'][satisfiable])
    print(', '.join('%s=%s' % i for i in variable.items()))


# ## run

# In[5]:


hornsat("""
X => Y
Y => Z
=> X
""")


# In[6]:


hornsat("""
X => Y
Y => X
=> X
Y =>
""")


# In[7]:


hornsat("""
P & Q & R & S => X
P & Q => R
R => S
X =>
=> P
=> R
""")


# In[8]:


hornsat("""
P & Q & R & S => X
P & Q => R
R => S
X =>
=> P
=> Q
""")


# In[ ]: