#include <stdio.h>
#include <stdlib.h>

/*  We are going to handle formulas of propositional
    logic, with

	False			(written "0")
	True			(written "1")
	Variables		(written "a".."z", "A".."Z")
	Negation 		(written "~e")
	Conjunction		(written "e & f")
	Disjunction		(written "e | f")
	Exclusive Or		(written "e ^ f")
	Implication		(written "e > f")
	Equivalence		(written "e = f")
	
    The first thing we have to do is decide how to represent these
    inside the computer.  I am going to use trees with labels on
    the nodes representing the operators, so
	p & (p > q) > q
    will be read as
	(> (& p (> p q)) q)
    and stored as a tree
		[> / \]
                  /   \
                 /     [Var q]
                [& / \]
                  /   \
           [Var p]     [> / \]
                         /   \
                  [Var p]     [Var q]

    We'll represent which variable is which by an integer 0..63;
    the surface syntax only allows 52 variables, but we'll allow
    64 in the internal representation.

    x ^ y is the same as x = ~y.
*/

enum Tag {
    False,
    True,
    Variable,
    Not,
    And,
    Or,
    Implies,
    Equiv
};    
typedef struct Node *formula;
struct Node {
    enum Tag tag;
    union {
        int     number;		/* variable number */
        formula operand[2];
    } u;
};

/*  Now we want to read and write these things.
    We rely on operator precedence:
	~ binds tightest,
	& next,
	| next,
	-> next,
	= weakest.
    We'll use parentheses whenever a low precedence operator
    governs an argument of a high precedence operator.

    &, |, and ^ are commutative and associative.
    It is customary to read p -> q -> r as p -> (q -> r).
    = is commutative, but not associative.
*/

static void
fwrite_formula_in_context(FILE *stream, formula f, enum Tag context) {
    switch (f->tag) {
	case False:
	    putc('0', stream);
	    break;
	case True:
	    putc('1', stream);
	    break;
	case Variable:
	    putc((f->u.number > 26 ? 'A'-27 : 'a'-1) + f->u.number, stream);
	    break;
	case Not:
	    putc('~', stream);
	    fwrite_formula_in_context(stream, f->u.operand[0], Not);
	    break;
	case And:
	    if (context < And) putc('(', stream);
	    fwrite_formula_in_context(stream, f->u.operand[0], And);
	    putc('&', stream);
	    fwrite_formula_in_context(stream, f->u.operand[1], And);
	    if (context < And) putc(')', stream);
	    break;
	case Or:
	    if (context < Or) putc('(', stream);
	    fwrite_formula_in_context(stream, f->u.operand[0], Or);
	    putc('|', stream);
	    fwrite_formula_in_context(stream, f->u.operand[1], Or);
	    if (context < Or) putc(')', stream);
	    break;
	case Implies:
	    if (context < Implies) putc('(', stream);
	    fwrite_formula_in_context(stream, f->u.operand[0], Or);
	    putc('>', stream);
	    fwrite_formula_in_context(stream, f->u.operand[1], Implies);
	    if (context < Implies) putc(')', stream);
	    break;
	case Equiv:
	    if (context < Equiv) putc('(', stream);
	    fwrite_formula_in_context(stream, f->u.operand[0], Implies);
	    putc('=', stream);
	    fwrite_formula_in_context(stream, f->u.operand[1], Implies);
	    if (context < Equiv) putc(')', stream);
	    break;
    }
}

static void
fwrite_formula(FILE *stream, formula f) {
    fwrite_formula_in_context(stream, f, Equiv);
    fprintf(stream, ";\n");
}

static void
write_formula(formula f) {
    fwrite_formula(stdout, f);
}

/*  Before we can read these things,
    we have to be able to create them.
    Later on, we are going to allocate lots and lots of them,
    and we'll want to do that fast.

    So we are going to keep a block of 1000 Nodes, dealing them
    out one at a time, and whenever we run out, we'll get another
    1000.
*/

static struct Node initial_nodes[64] = {
    {False   , { 0}},
    {Variable, { 1}},
    {Variable, { 2}},
    {Variable, { 3}},
    {Variable, { 4}},
    {Variable, { 5}},
    {Variable, { 6}},
    {Variable, { 7}},
    {Variable, { 8}},
    {Variable, { 9}},
    {Variable, {10}},
    {Variable, {11}},
    {Variable, {12}},
    {Variable, {13}},
    {Variable, {14}},
    {Variable, {15}},
    {Variable, {16}},
    {Variable, {17}},
    {Variable, {18}},
    {Variable, {19}},
    {Variable, {20}},
    {Variable, {21}},
    {Variable, {22}},
    {Variable, {23}},
    {Variable, {24}},
    {Variable, {25}},
    {Variable, {26}},
    {False   , { 0}},	/* unused */
    {False   , { 0}},	/* unused */
    {False   , { 0}},	/* unused */
    {False   , { 0}},	/* unused */
    {False   , { 0}},	/* unused */

    {True    , { 1}},
    {Variable, {27}},
    {Variable, {28}},
    {Variable, {29}},
    {Variable, {30}},
    {Variable, {31}},
    {Variable, {32}},
    {Variable, {33}},
    {Variable, {34}},
    {Variable, {35}},
    {Variable, {36}},
    {Variable, {37}},
    {Variable, {38}},
    {Variable, {39}},
    {Variable, {40}},
    {Variable, {41}},
    {Variable, {42}},
    {Variable, {43}},
    {Variable, {44}},
    {Variable, {45}},
    {Variable, {46}},
    {Variable, {47}},
    {Variable, {48}},
    {Variable, {49}},
    {Variable, {50}},
    {Variable, {51}},
    {Variable, {52}},
    {True    , { 1}},	/* unused */
    {True    , { 1}},	/* unused */
    {True    , { 1}},	/* unused */
    {True    , { 1}},	/* unused */
    {True    , { 1}} 	/* unused */
};

#define ffalse &initial_nodes[0]
#define ftrue  &initial_nodes[32]

/*  We are going to keep a list of blocks of nodes.
    In fact, we'll keep two:
	inuse_list		blocks with allocations in them
	spare_list		blocks that are completely free
    Allocation will proceed from the block at the front as long
    as there are any nodes_left there; when that runs out we
    move the first block from spare_list to inuse_list, or if
    there aren't any, allocate a new one.
*/
struct Pool_Block {
    struct Pool_Block *next;
    struct Node        node[1000];
};
static struct Pool_Block *inuse_list = 0, *spare_list = 0;
static int          nodes_left = 0;

static formula
make_node(enum Tag tag, formula lhs, formula rhs) {
    formula r;
    register struct Pool_Block *list;

    if (nodes_left == 0) {
	list = spare_list;

	if (list == 0) {
	    list = malloc(sizeof *list);
	    if (list == 0) {
		perror("memory ran out");
		exit(EXIT_FAILURE);
	    }
	} else {
	    spare_list = list->next;
	}
	list->next = inuse_list;
	inuse_list = list;
	nodes_left = sizeof list->node/sizeof list->node[0];
    } else {
	list = inuse_list;
    }
    r = &list->node[--nodes_left];
    r->tag = tag, r->u.operand[0] = lhs, r->u.operand[1] = rhs;
    return r;
}

static void
free_all_nodes(void) {
    struct Pool_Block *p, *q;

    for (p = inuse_list; p != 0; p = q) {
	q = p->next;
	p->next = spare_list;
	spare_list = p;
    }
    inuse_list = 0;
    nodes_left = 0;
}


#define make_not(    e)    make_node(Not,     e, (formula)0)
#define make_and(    e, f) make_node(And,     e, f)
#define make_or(     e, f) make_node(Or,      e, f)
#define make_implies(e, f) make_node(Implies, e, f)
#define make_equiv(  e, f) make_node(Equiv,   e, f)
#define make_xor(    e, f) make_node(Equiv,   e, make_not(f))

/*  Now we can read.
    The only difference between propt.c and prop.c is
    that this file has an explicit tokeniser.  The tokeniser
    sets one global variable: tok_char.  Since our lexical
    structure is so simple, one character is enough to encode
    an entire token.

    This is not only clearer, it speeded up the program on a
    large test file from 11.78 seconds to 8.35 seconds, and
    that's with debugging code to print lots of solutions left in.
*/
static int tok_char;

static void read_next_token(register FILE *stream) {
    int c;

    do c = getc(stream); while (c <= ' ' && c >= '\0');
    tok_char = c;
    if (c == ';') {
	do c = getc(stream); while (c == ' ' || c == '\t');
	(void)ungetc(c, stream);
    }
}

/*  We are going to use this grammar:

    primary = '0' | '1' | /[a-zA-Z]/ | '(' expr ')' | '~' primary
    conj = primary {'&' primary}...
    disj = conj {'|' conj}...
    xor  = disj {'^' disj}...
    impl = xor ['->' impl]
    expr = impl ['=' impl]
    formula = expr ';'

    Each of these will correspond to a parsing function.
    On entry to each of the functions (except 'formula', which
    has to get things started), the next character in the input
    will not be white space.
    Unfortunately, C99 added a 'conj' function, so I renamed my
    conj() to conjf().  Unfortunately, C99 added that too!
    So all the xxx functions have been renamed to read_xxx.
*/

static formula read_expr(FILE *);

static formula
read_primary(FILE *stream) {
    formula r;
    int const c = tok_char;

    if (c == '0') {
	r = ffalse;
    } else
    if (c == '1') {
        r = ftrue;
    } else
    if (c >= 'a' && c <= 'z') {
        r = &initial_nodes[c-'a'+1];
    } else
    if (c >= 'A' && c <= 'Z') {
	r = &initial_nodes[c-'A'+33];
    } else
    if (c == '(') {
	read_next_token(stream);
	r = read_expr(stream);
	if (tok_char != ')') {
	    fprintf(stderr, "Missing )\n");
	    exit(EXIT_FAILURE);
	}
    } else
    if (c == '~') {
	read_next_token(stream);
	return make_not(read_primary(stream));
    } else {
	fprintf(stderr, "A primary cannot start with '%c'\n", c);
	exit(EXIT_FAILURE);
    }
    read_next_token(stream);
    return r;
}

static formula
read_conj(FILE *stream) {
    formula r;

    r = read_primary(stream);
    while (tok_char == '&') {
	read_next_token(stream);
        r = make_and(r, read_primary(stream));
    }
    return r;
}

static formula
read_disj(FILE *stream) {
    formula r;

    r = read_conj(stream);
    while (tok_char == '|') {
        read_next_token(stream);
	r = make_or(r, read_conj(stream));
    }
    return r;
}

static formula
read_xor(FILE *stream) {
    formula r;

    r = read_disj(stream);
    while (tok_char == '^') {
	read_next_token(stream);
	r = make_xor(r, read_disj(stream));
    }
    return r;
}

static formula
read_impl(FILE *stream) {
    formula r;

    r = read_xor(stream);
    if (tok_char == '>') {
	read_next_token(stream);
	r = make_implies(r, read_impl(stream));
    }
    return r;
}

static formula
read_expr(FILE *stream) {
    formula r;

    r = read_impl(stream);
    if (tok_char == '=') {
	read_next_token(stream);
	r = make_equiv(r, read_impl(stream));
    }
    return r;
}

/*  At end of file, fread_formula will return a null pointer,
    which is not a formula.
*/
static formula
fread_formula(FILE *stream) {
    formula r;

    read_next_token(stream);
    if (tok_char == EOF) return (formula)0;
    r = read_expr(stream);
    if (tok_char != ';') {
	fprintf(stderr,
	        "Expected ';' at end of formula but got %c'\n", tok_char);
	exit(EXIT_FAILURE);
    }
    return r;
}

static formula
read_formula(void) {
    return fread_formula(stdin);
}

/*  The next step is simplification.
    We shall simplify a formula in a context, which is
	- a set of variables to be regarded as true (pos)
	- a set of variables to be regarded as false (neg).
    We shall return
	- a simplified formula 
	- the set of variables occurring positively in it
	- the set of variables occurring negatively in it.

    A variable x occurs positively in
	variable     v  iff v is x
	negation    ~e  iff x occurs negatively in e
	conjunction e&f iff x occurs positively in e or f
	disjunction e|f iff x occurs positively in e or f
	implication e>f iff x occurs positively in f or negatively in e
			because (e -> f) = (~e | f)
	equivalence e=f iff x occurs positively or negatively in e or f
			because (e = f) = (e & f | ~e & ~f).

    A variable x occurs negatively in
	negation    ~e  iff x occurs positively in e
	conjunction e&f iff x occurs negatively in e or f
	disjunction e|f iff x occurs negatively in e or f
	implication e>f iff x occurs negatively in f or positively in e
	equivalence e=f iff x occurs positively or negatively in e or f

    To make life simple for ourselves, we'll represent a set of variables
    by a bitmask, with m&(1<<i) set whenever variable i is in the set
    represented by m.  With unsigned long long, we can handle up to 64
    bits, hence the limit on the number of variables.  We could obviously
    handle a lot more by using an array of bitmasks, or some other set
    representation.
*/
typedef unsigned long long set;

#define empty 0ull
#define has(set, elt) (((set) & (1ull << (elt))) != empty)
#define with(set, elt) ((set) | (1ull << (elt)))
#define sunion(s1, s2) ((s1)  | (s2))	/* set union */
#define sinter(s1, s2) ((s1)  & (s2))	/* set intersection */
#define sdiff( s1, s2) ((s1)  &~(s2))	/* s1 \ s2 */

static void
simplify(
    formula e,		/* formula to simplify */
    set pos,		/* treat these as true */
    set neg,		/* treat these as false */
    formula *s,		/* simplified version of e */
    set     *occ_pos,	/* these occur positively in s */
    set     *occ_neg	/* these occur negatively in s */
) {
    formula x, y;
    set     px, nx, py, ny;

    switch (e->tag) {
	case False:
	case True:
	    *s = e;
	    *occ_pos = *occ_neg = empty;
	    return;
	case Variable:
	    if (has(pos, e->u.number)) {
		*s = ftrue;
		*occ_pos = *occ_neg = empty;
	    } else
	    if (has(neg, e->u.number)) {
		*s = ffalse;
		*occ_pos = *occ_neg = empty;
	    } else {
		*s = e;
		*occ_neg = empty;
		*occ_pos = with(empty, e->u.number);
	    }
	    return;
	case Not:
	    simplify(e->u.operand[0], pos, neg, &x, &px, &nx);
	    if (x->tag == Not) {
		*s = x->u.operand[0];	/* ~~x = x */
	    } else
	    if (x->tag == False) {	/* ~0 = 1 */
		*s = ftrue;		/* px, nx are already {} */
	    } else
	    if (x->tag == True) {	/* ~1 = 0 */
		*s = ffalse;		/* px, nx are already {} */
	    } else
	    if (x == e->u.operand[0]) {
		*s = e;		/* no change */
	    } else {
		*s = make_not(x);
	    }
	    *occ_pos = nx;	/* note the swap! */
	    *occ_neg = px;	/* note the swap! */
	    return;
	case And:
	    simplify(e->u.operand[0], pos, neg, &x, &px, &nx);
	    simplify(e->u.operand[1], pos, neg, &y, &py, &ny);
	    if (x->tag == False) {		/* 0&y = 0 */
		*s = x;
		*occ_pos = *occ_neg = empty;
	    } else
	    if (x->tag == True) {		/* 1&y = y */
		*s = y;
		*occ_pos = py, *occ_neg = ny;
	    } else
	    if (y->tag == False) {		/* x&0 = 0 */
		*s = y;
	        *occ_pos = *occ_neg = empty;
	    } else
	    if (y->tag == True) {		/* x&1 = x */
	        *s = x;
		*occ_pos = px, *occ_neg = nx;
	    } else
	    if (x == y) {			/* x&x = x */
	        *s = x;
	        *occ_pos = px, *occ_neg = nx;
	    } else
	    if (x->tag == Not && x->u.operand[0] == y
	     || y->tag == Not && y->u.operand[0] == x
	    ) {					/* x & ~x = ~x & x = 0 */
		*s = ffalse;
		*occ_pos = *occ_neg = empty;
	    } else {
		if (x == e->u.operand[0] && y == e->u.operand[1]) {
		    *s = e;			/* no change */
		} else {
		    *s = make_and(x, y);	/* x is simpler or y is */
		}
		*occ_pos = sunion(px, py);
		*occ_neg = sunion(nx, ny);
	    }
	    return;
	case Or:
	    simplify(e->u.operand[0], pos, neg, &x, &px, &nx);
	    simplify(e->u.operand[1], pos, neg, &y, &py, &ny);
	    if (x->tag == True) {		/* 1|y = 1 */
		*s = x;
		*occ_pos = *occ_neg = empty;
	    } else
	    if (x->tag == False) {		/* 0|y = y */
		*s = y;
		*occ_pos = py, *occ_neg = ny;
	    } else
	    if (y->tag == True) {		/* x|1 = 1 */
		*s = y;
	        *occ_pos = *occ_neg = empty;
	    } else
	    if (y->tag == False) {		/* x|0 = x */
	        *s = x;
		*occ_pos = px, *occ_neg = nx;
	    } else
	    if (x == y) {			/* x|x = x */
	        *s = x;
	        *occ_pos = px, *occ_neg = nx;
	    } else
	    if (x->tag == Not && x->u.operand[0] == y
	     || y->tag == Not && y->u.operand[1] == x
	    ) {					/* x | ~x = ~x | x = 1 */
	        *s = ftrue;
	        *occ_pos = *occ_neg = empty;
	    } else {
		if (x->tag == Not) {		/* (~z)|y = z>y */
		    *s = make_implies(x->u.operand[0], y);
		} else
		if (x == e->u.operand[0] && y == e->u.operand[1]) {
		    *s = e;			/* no change */
		} else {
		    *s = make_or(x, y);		/* x is simpler, or y is */
		}
		*occ_pos = sunion(px, py);
		*occ_neg = sunion(nx, ny);
	    }
	    return;
	case Implies:
	    simplify(e->u.operand[0], pos, neg, &x, &px, &nx);
	    simplify(e->u.operand[1], pos, neg, &y, &py, &ny);
	    if (x->tag == True) {		/* 1>y = y */
		*s = y;
		*occ_pos = py, *occ_neg = ny;
	    } else
	    if (x->tag == False) {		/* 0>y = 1 */
		*s = ftrue;
		*occ_pos = *occ_neg = empty;
	    } else
	    if (y->tag == True) {		/* x>1 = 1 */
		*s = y;
	        *occ_pos = *occ_neg = empty;
	    } else
	    if (y->tag == False) {		/* x>0 = ~x */
		if (x->tag == Not) {		/* (~z)>0 = z */
		    *s = x->u.operand[0];
		} else {
		    *s = make_not(x);
		}
		*occ_pos = nx, *occ_neg = px;
	    } else
	    if (x == y) {			/* x>x = 1 */
	        *s = ftrue;
	        *occ_pos = *occ_neg = empty;
	    } else {
		if (x->tag == Not) {		/* (~z)>y z|y */
		    *s = make_or(x->u.operand[0], y);
		} else
		if (x == e->u.operand[0] && y == e->u.operand[1]) {
		    *s = e;			/* no change */
		} else {
		    *s = make_implies(x, y);	/* x is simpler, or y is */
		}
		*occ_pos = sunion(nx, py);
		*occ_neg = sunion(px, ny);
	    }
	    return;
	case Equiv:
	    simplify(e->u.operand[0], pos, neg, &x, &px, &nx);
	    simplify(e->u.operand[1], pos, neg, &y, &py, &ny);
	    if (x->tag == True) {		/* (1=y) = y */
		*s = y;
		*occ_pos = py, *occ_neg = ny;
	    } else
	    if (x->tag == False) {		/* (0=y) = ~y */
		if (y->tag == Not) {
		    *s = y->u.operand[0];
		} else {
		    *s = make_not(y);
		}
		*occ_pos = ny, *occ_neg = py;
	    } else
	    if (y->tag == True) {		/* (x=1) = x */
		*s = x;
		*occ_pos = px, *occ_neg = nx;
	    } else
	    if (y->tag == False) {		/* (x=0) = ~x */
		if (x->tag == Not) {
		    *s = x->u.operand[0];
		} else {
		    *s = make_not(x);
		}
		*occ_pos = nx, *occ_neg = px;
	    } else
	    if (x == y) {			/* (x=x) = x */
	        *s = ftrue;
	        *occ_pos = *occ_neg = empty;
	    } else {
		if (x == e->u.operand[0] && y == e->u.operand[1]) {
		    *s = e;			/* no change */
		} else {
		    *s = make_equiv(x, y);	/* x is simpler, or y is */
		}
		px = sunion(px, nx);
		py = sunion(py, ny);
		*occ_pos = *occ_neg = sunion(px, py);
	    }
	    return;
    }
}

static void
fwrite_set(FILE *stream, set s) {
    int i;
    char c, x;

    c = '{';
    for (i = 1; i <= 52; i++) {
	if (has(s, i)) {
	    putc(c, stream);
	    x = (i <= 26 ? 'a'-1 : 'A'-27) + i;
	    putc(x, stream);
	    c = ',';
	}
    }
    if (c == '{') putc(c, stream);
    putc('}', stream);
}

static void
write_set(set s) {
    fwrite_set(stdout, s);
}

/*  Finally, our method of solving a propositional
    formula (finding an interpretation under which it
    is true) is this:

    to solve e given pos and neg
	simplify e given pos and neg producing e', occ-pos, occ-neg
	if occ-pos .intersection. occ-neg is empty then
	   if occ-pos U occ-neg is empty
	       e' must be True or False.
	       if e' is True,
		  pos U occ-pos, neg U occ-neg  is a solution.
	   else
	      solve e' given pos U occ-pos and neg U occ-neg
	otherwise
	   let x be any element of occ-pos .intersection. occ-neg
	   solve e' given pos U (occ-pos \ occ-neg) U {x}
		      and neg U (occ-neg \ occ-pos).
	   solve e' given pos U (occ-pos \ occ-neg)
		      and neg U (occ-neg \ occ-pos) U {x}.

    Given that there may be many solutions, how do we report them?
    Answer: accept a function that says what to do with a solution.
    We'll hack this slightly so that the function returns a result
    saying whether to stop.
*/
static int
solve(
    formula e,
    set     pos,
    set     neg,
    int   (*handler)(set, set)
) {
    set occ_pos, occ_neg, occ_both;
    
    simplify(e, pos, neg, &e, &occ_pos, &occ_neg);
    occ_both = sinter(occ_pos, occ_neg);
    if (occ_both == empty) {
	pos = sunion(pos, occ_pos);
	neg = sunion(neg, occ_neg);
	simplify(e, pos, neg, &e, &occ_pos, &occ_neg);
	if (sunion(occ_pos, occ_neg) != empty) abort();
	if (e->tag == True) {
	    return handler(pos, neg);
	} else {
	    return 0;
	}
    } else {
	pos = sunion(pos, sdiff(occ_pos, occ_both));
	neg = sunion(neg, sdiff(occ_neg, occ_both));
	occ_both &=~ (occ_both-1);
	return solve(e, sunion(pos, occ_both), neg, handler)
	    || solve(e, pos, sunion(neg, occ_both), handler);
    }
}

/*  To find and print single solution, we need a handler
    that prints its arguments and returns 1.
*/
static int
print_first_solution_handler(set pos, set neg) {
    printf("p = ");   write_set(pos);
    printf(", n = "); write_set(neg);
    printf(".\n");
    return 1;
}

static void
print_first_solution(formula e) {
    if (!solve(e, empty, empty, print_first_solution_handler))
	printf("No solutions.\n");
}

/*  For testing purposes, we are going to use the simple
    blind backtracking-over-all-variables approach.
*/
static void
print_all_solutions(formula e, set pos, set neg) {
    set p, n;

    simplify(e, pos, neg, &e, &p, &n);
    p = sunion(p, n);
    if (p == empty) {
	/* The only way you can get a simplified formula with */
	/* no variables is if it is True or False. */
	if (e->tag == True) (void)print_first_solution_handler(pos, neg);
    } else {
	p = p&~ (p-1);
	print_all_solutions(e, sunion(pos, p), neg);
	print_all_solutions(e, pos, sunion(neg, p));
    }
}

int main(void) {
    formula r;

    while ((r = read_formula()) != 0) {
	write_formula(r);
	print_first_solution(r);
	print_all_solutions(r, empty, empty);
	printf("\n");
	free_all_nodes();
    }
    return 0;
}