// I am converting propt.c to Java.
// It is a painful process, and I've not finished yet.

import java.lang.*;
import java.util.*;
import java.io.*;

public class Propt {

    static abstract class Formula {
	static final int Literal_Priority  = 0;
	static final int Variable_Priority = 0;
	static final int Not_Priority      = 1;
	static final int And_Priority      = 2;
	static final int Or_Priority       = 3;
	static final int Equiv_Priority    = 4;

	boolean is_literal()	     { return false; }
	boolean is_variable()	     { return false; }
	boolean is_not()             { return false; }

        static final False lfalse = new False();
        static final True  ltrue  = new True();

	static final Variable[] vars = {
	    null,
	    new Variable('a'),
	    new Variable('b'),
	    new Variable('c'),
	    new Variable('d'),
	    new Variable('e'),
	    new Variable('f'),
	    new Variable('g'),
	    new Variable('h'),
	    new Variable('i'),
	    new Variable('j'),
	    new Variable('k'),
	    new Variable('l'),
	    new Variable('m'),
	    new Variable('n'),
	    new Variable('o'),
	    new Variable('p'),
	    new Variable('q'),
	    new Variable('r'),
	    new Variable('s'),
	    new Variable('t'),
	    new Variable('u'),
	    new Variable('v'),
	    new Variable('w'),
	    new Variable('x'),
	    new Variable('y'),
	    new Variable('z'),
	    null, null, null, null, null,
	    null,
	    new Variable('A'),
	    new Variable('B'),
	    new Variable('C'),
	    new Variable('D'),
	    new Variable('E'),
	    new Variable('F'),
	    new Variable('G'),
	    new Variable('H'),
	    new Variable('I'),
	    new Variable('J'),
	    new Variable('K'),
	    new Variable('L'),
	    new Variable('M'),
	    new Variable('N'),
	    new Variable('O'),
	    new Variable('P'),
	    new Variable('Q'),
	    new Variable('R'),
	    new Variable('S'),
	    new Variable('T'),
	    new Variable('U'),
	    new Variable('V'),
	    new Variable('W'),
	    new Variable('X'),
	    new Variable('Y'),
	    new Variable('Z'),
	    null, null, null, null, null,
	};

        static Formula variable(char name) {
	    return vars[name <= 'Z' ? name-'A'+32 : name-'a'];
	}
	static Formula not(Formula x) {
	    return new Not(x);
	}
	static Formula and(Formula x, Formula y) {
	    return new And(x, y);
	}
	static Formula or(Formula x, Formula y) {
	    return new Or(x, y);
	}
	static Formula implies(Formula x, Formula y) {
	    return or(not(x), y);
	}
	static Formula equiv(Formula x, Formula y) {
	    return new Equiv(x, y);
	}
	static Formula xor(Formula x, Formula y) {
	    return equiv(x, not(y));
	}

	void printOn(OutputStream s, int priority) {}
	void printOn(OutputStream s) {
	    this.printOn(s, Equiv_Priority);
	}
	void print() {
	    this.printOut(System.output);
	}
    }

    static class False {
	False() { }

	boolean is_literal() { return true; }

	True opposite() { return Formula.ltrue; }

	void printOn(OutputStream s, int priority) {
	    s.write('0');
	}

	Simplification_Result simplify(Variable_Set pos, Variable_Set neg) {
	    return Simplification_Result(this,
		      Variable_Set.empty, Variable_Set.empty);
	}
    }

    static class True {
	True() { }

	boolean is_literal() { return true; }

	False opposite() { return Formula.lfalse; }

	void printOn(OutputStream s, int priority) {
	    s.write('1');
	}

	Simplification_Result simplify(Variable_Set pos, Variable_Set neg) {
	    return Simplification_Result(this,
		      Variable_Set.empty, Variable_Set.empty);
	}
    }

    static class Variable {
	int number;

	Variable(char n) {
	    number = n < 'Z' ? n - 'A' + 32 : n - 'a';
	}

	boolean is_variable() { return true; }

	void printOn(OutputStream s, int priority) {
	    s.write(number >= 32 ? number - 32 + 'A' : number + 'a');
	}

	Simplification_Result simplify(Variable_Set pos, Variable_Set neg) {
	    if (pos.contains(this)) {
		return new Simplification_Result(Formula.ltrue,
				Variable_Set.empty, Variable_Set.empty);
	    } else
	    if (neg.contains(this)) {
	        return new Simplication_Result(Formula.lfalse,
	                        Variable_Set.empty, Variable_Set.empty);
	    } else {
		return new Simplification_Result(this,
		                new Variable_Set(this), Variable_Set.empty);
	    }
	}
    }

    static class Not {
	Formula right;

	Not(Formula r) { right = r; }

	boolean is_not() { return true; }

	void printOn(OutputStream s, int priority) {
	    right.printOn(s, Not_Priority);
	}

	Simplification_Result simplify(Variable_Set pos, Variable_Set neg) {
	    Simplification_Result r = right.simplify(pos, neg);
	    Variable_Set rpos = r.pos, rneg = r.neg;
	    if (r.e.is_not()) {
		r.e = r.e.right;
	    } else
	    if (r.e.is_literal()) {
		r.e = r.e.opposite();
	    } else
	    if (r.e != right) {
		r.e = Formula.not(r.e);
	    }
	    r.pos = rneg;
	    r.neg = rpos;
	    return r;
	}
    }

    static class And {
	Formula left, right;

	And(Formula l, Formula r) { left = l; right = r; }

	void printOn(OutputStream s, int priority) {
	    if (priority < And_Priority) s.write('(');
	    left.printOn(s, And_Priority);
	    s.write('&');
	    right.printOn(s, And_Priority);
	    if (priority < And_Priority) s.write(')');
	}

	Simplification_Result simplify(Variable_Set pos, Variable_Set neg) {
	    Simplification_Result rx = left.simplify(pos, neg);
	    Simplification_Result ry = right.simplify(pos, neg);
	    Formula e;
	    Variable_Set p, n;

	    if (rx.e.is_literal()) {
		if (rx.e == Formula.lfalse) {
		    e = rx.e;
		    p = n = Variable_Set.empty;
		} else {
		    e = ry.e;
		    p = ry.pos;
		    n = ry.neg;
		}
	    } else
	    if (ry.e.is_literal()) {
		if (ry.e == Formula.lfalse) {
		    e = ry.e;
		    p = n = Variable_Set.empty;
		} else {
		    e = rx.e;
		    p = rx.pos;
		    n = rx.neg;
		}
	    } else
		CONVERSION ABANDONED HERE.
    }

    static class Or {
	Formula left, right;

	Or(Formula l, Formula r) { left = l; right = r; }

	void printOn(OutputStream s, int priority) {
	    if (priority < Or_Priority) s.write('(');
	    left.printOn(s, Or_Priority);
	    s.write('|');
	    right.printOn(s, Or_Priority);
	    if (priority < Or_Priority) s.write(')');
	}
    }

    static class Equiv {
	Formula left, right;

	Or(Formula l, Formula r) { left = l; right = r; }

	void printOn(OutputStream s, int priority) {
	    if (priority < Equiv_Priority) s.write('(');
	    left.printOn(s, Or_Priority);
	    s.write('=');
	    right.printOn(s, Or_Priority);
	    if (priority < Equiv_Priority) s.write(')');
	}
    }

    static int tok_char;

    static void read_next_token(InputStream s) {
	int c;
	
	do c = s.read(); while (c <= ' ' && c >= 0);
	tok_char = c;
	// There is un ungetc() or pushback() in InputStream
    }

    static void syntax_error(String msg) {
	System.err.println(msg);
	System.exit(1);
    }

    static Formula read_primary(InputStream s) {
	Formula r;
	int c = tok_char;

	if (c == '0') {
	    r = Formula.lfalse;
	} else
	if (c == '1') {
	    r = Formula.ltrue;
	} else
	if (c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z') {
	    r = Formula.variable(c);
	} else
	if (c == '(') {
	    read_next_token(s);
	    r = read_expr(s);
	    if (tok_char != ')') syntax_error("Missing )");
	} else
	if (c == '~') {
	    read_next_token(s);
	    return Formula.not(read_primary(s));
	} else {
	    syntax_error("A primary cannot start with '" + (char)c + "'");
	}
	read_next_token(s);
	return r;
    }

    static Formula read_conj(InputStream s) {
	Formula r;

	r = read_primary(s);
	while (tok_char == '&') {
	    read_next_token(s);
	    r = Formula.and(r, read_primary(s));
	}
	return r;
    }

    static Formula read_disj(InputStream s) {
	Formula r;

	r = read_conj(s);
	while (tok_char == '|') {
	    read_next_token(s);
	    r = Formula.or(r, read_conj(s));
	}
	return r;
    }

    static Formula read_xor(InputStream s) {
	Formula r;

	r = read_disj(s);
	while (tok_char == '^') {
	    read_next_token(s);
	    r = Formula.xor(r, read_disj(s));
	}
	return r;
    }

    static Formula read_impl(InputStream s) {
	Formula r;

	r = read_xor(s);
	if (tok_char == '>') {
	    read_next_token(s);
	    r = Formula.implies(r, read_impl(s));
	}
	return r;
    }

    static Formula read_expr(InputStream s) {
	Formula r;

	r = read_impl(s);
	if (tok_char == '=') {
	    read_next_token(s);
	    r = Formula.equiv(r, read_impl(s));
	}
	return r;
    }

    static Formula read_formula(InputStream s) {
	Formula r;

	read_next_token(s);
	if (tok_char < 0) return null;
	r = read_expr(s);
	if (tok_char != ';')
	    syntax_error("Expected ';' at end of formula but got '"
			 +(char)tok_char+"'");
	return r;
    }

    static Formula read_formula() {
	return read_formula(System.in);
    }

    static class Variable_Set {
	long bits;

	Variable_Set() {
	    bits = 0;
	}

	Variable_Set(Variable v) {
	    bits = 1 << v.number;
	}

	static final Variable_Set empty = new Variable_Set();

	Variable_Set union(Variable_Set other) {
	    return new Variable_Set(bits | other.bits);
	}

	Variable_Set intersection(Variable_Set other) {
	    return new Variable_Set(bits & other.bits);
	}

	Variable_Set difference(Variable_Set other) {
	    return new Variable_Set(bits &~ other.bits);
	}

	Variable_Set choice() {
	    // Return a subset containing any one element only.
	    return Variable_Set(bits &~ (bits - 1));
	}

	boolean is_empty() {
	    return bits == 0;
	}

	boolean contains(int i) {
	    return ((bits >> i) & 1) != 0;
	}
	
	boolean contains(Variable v) {
	    return this.contains(v.number);
	}

	void printOn(OutputStream s) {
	    char c = '{';
	    for (int i = 1; i <= 52; i++) {
	        if (this.contains(i)) {
	            s.write(c);
	            c = i < 32 ? 'a' + i : 'A' - 32 + i;
	            s.write(c);
	            c = ',';
		}
	    }
	    if (c == '{') s.write(c);
	    s.write('}');
	}

	void printNlOn(OutputStream s) {
	    this.printOn(s);
	    s.write('\n');
	}
    }

    static class Simplification_Result {
	Formula e;
	Variable_Set pos;	
	Variable_Set neg;

	Simplification_Result(Formula e, Variable_Set pos, Variable_Set neg) {
	    this.e = e;
	    this.pos = pos;
	    this.neg = neg;
	}
    }


    static Simplification_Result simplify(
	Formula e, Variable_Set pos, Variable_Set neg
    ) {
	Formula x, y;
	Variable_Set px, nx, py, ny;
	Simplification_Result rx, ry;

	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;
    }
}

    abstract static class Result_Handler {
	abstract boolean handle(Simplification_Result r);
    }

    static class Print_First_Solution_Handler extends Result_Handler {
	boolean handle(Simplification_Result r) {
	    System.out.print("p = ");
	    r.pos.printOn(System.out);
	    System.out.print(", n = ");
	    r.neg.printOn(System.out);
	    System.out.print(".\n");
	    return true;
	}
    }

    static boolean solve(
	Formula e,
	Variable_Set pos,
	Variable_Set neg,
	Result_Handler handler
    ) {
	Simplification_Result r = e.simplify(pos, neg);
	Variable_Set occ_both = r.pos.intersection(r.neg);
	if (occ_both.is_empty()) {
	    r = r.e.simplify(pos.union(r.pos), neg.union(r.neg));
	    assert r.pos.union(r.neg).is_empty();
	    if (r.e == Formula.ltrue) return handler.handle(r);
	    return false;
	} else {
	    pos = pos.union(r.pos.difference(occ_both);
	    neg = neg.union(r.neg.difference(occ_both);
	    occ_both = occ_both.choice();
	    return solve(r.e, pos.union(occ_both), neg, handler)
                || solve(r.e, pos, neg.union(occ_both), handler);
	}
    }

    static void main(String[] args) {
	Formula r;

	while ((r = read_formula(System.in)) != null) {
	    r.printOn(System.out);
	    if (!solve(r, Variable_Set.empty, Variable_Set.empty,
		       new Print_First_Solution_Handler())) {
		System.out.println("No solutions.");
	    }
	    System.out.println("");
	}
    }
}