#!/usr/bin/python

from random import choice
import sys
import string

vars = {}   # create empty hashtable of variables

class clause:
    def __init__(self, str):
        v = string.split(str)
        if(len(v) != 3):
            print "Invalid clause:", str
            sys.exit()
        self.compl = {}
        self.always_true = 0
        for x in v:
            if x[-1] == "'":
                name = x[:-1]
            else:
                name = x
            if not vars.has_key(name):
                vars[name] = choice([0, 1])
            if self.compl.has_key(name):
                if self.compl[name] == (x[-1] == "'"):
                    continue # variable is same sense, ignore
                else:
                    self.always_true = 1
            else:
                self.compl[name] = (x[-1] == "'")
                    
    def value(self):
        a = 0
        for v in self.compl.keys():
            a = a | (vars[v] ^ self.compl[v])
        return self.always_true or a

    def __str__(self):
        if self.always_true:
            return 'true'
        a, k = [], self.compl.keys()
        k.sort()
        for v in k:
            if self.compl[v]:
                a.append(v + "'")
            else:
                a.append(v)
        return '(' + string.join(a, ' | ') + ')'

clauses = []

#file = open(sys.argv[1])
#for l in file.readlines():
for l in sys.stdin.readlines():
    clauses.append(clause(l))

#clauses = map(clause, sys.stdin.readlines())

print 'Expression:', string.join(map(str, clauses), ' & ')
print len(vars), 'variables and', len(clauses), 'clauses'

def get_sat_count():
    s = len(filter(clause.value, clauses))
    print s, 'clauses satisfied'
    return s
def get_assignment(var):
    return var + ':' + str(vars[var])
def print_assignment():
    k = vars.keys()
    k.sort()
    print string.join(map(get_assignment, k))
def flip(var):
    vars[var] = not vars[var]
    print_assignment()

print 'Initial assignment:'
print_assignment()
sat_count = get_sat_count()
steps = 0

while sat_count < len(clauses):
    steps = steps + 1
    if steps > len(clauses):
        print 'Got bored and quit'
        sys.exit(0)
    old_sat_count = sat_count
    var = choice(vars.keys())
    print 'Flipping', var, '...'
    flip(var)
    sat_count = get_sat_count()
    if sat_count >= old_sat_count:
        pass
        #if sat_count > old_sat_count:
        #    print sat_count
    else:
        print 'Doh! Flipping', var, 'back now (' + str(old_sat_count), ' was better)'
        flip(var)
        sat_count = old_sat_count

print 'Expressions satisfied in', steps, 'iterations'