// Java dialect: Java 5.0
import java.util.*;
import java.io.*;

// Boolean Simplifier

// This program reads a stream of conditional (if) formulas expressed in parenthesized
// prefix syntax and outputs a corresponding stream of simplified formulas.
// All tautologies are simplied to "T" and all contradictions to "F".

interface IfForm {
  
  // An IfForm is either:
  
  // (i)   a variable consisting of alphanumeric characters  (class Variable) 
  // (ii)  a boolean constant true or false                  (class Constant)
  // (iii) a conditional expression (? f g h)                (class If)
  
  // where f,g,h are IfForms
  
  abstract public <T> T apply(IfFormVisitor<T> v);
  // IfForm visitor pattern hook
}

interface IfFormVisitor<T> {
  
  public T forConstant(Constant arg);
  public T forVariable(Variable arg);
  public T forIf(If arg);
}

abstract class Environment {
  public static final Environment empty = new Empty();
  
  public Environment bind(Variable s, IfForm v) {
    return new AddBinding(s,v,this);
  }
  abstract public IfForm lookup(Variable s);  // returns s for empty env
  
  private static class Empty extends Environment {
    // relying on default constructor
    public IfForm lookup(Variable s) {
      return s;
    }
  }
  
  private static class AddBinding extends Environment {
    Variable sym;
    IfForm value;
    Environment rest;
    
    AddBinding(Variable s, IfForm v, Environment r) {
      sym = s;
      value = v;
      rest = r;
    }
    
    public IfForm lookup(Variable s) {
      // Variables are hashed to guarantee uniqueness
      if (s == sym) return value;
      else return rest.lookup(s);
    }
  }
}

// The parse routine is a static method in FormStream called read(); it
// throws ParseException (an extension of IOException) if it encounters
// a syntax error.

class ParseException extends IOException {
  ParseException(String s) {
    super(s);
  }
}

class FormStream extends StreamTokenizer {
  
  // A FormStream is a file input stream of containing textual representations
  // of Form objects.
  
  // contains main method
  
  // short names for StreamTokenizer codes
  
  public static int WORD = StreamTokenizer.TT_WORD; 
  public static int EOF = StreamTokenizer.TT_EOF; 
  public static int EOL = StreamTokenizer.TT_EOL; 
  
  public static String simplify(String input) { return null; }
  
  /** Constructs a FormReader wrapping the String s */
  FormStream(String s) throws IOException {
    this(new BufferedReader(new StringReader(s)));
  }
  
  /** Constructs a FormReader wrapping the file f */
  FormStream(File f) throws IOException {
    this(new BufferedReader(new FileReader(f)));
  }
  /** Constructs a FormReader wrapping the Reader r */
  FormStream(Reader r) {
    super(r);
  
    
    // configure StreamTokenizer portion of this
    resetSyntax();
    wordChars('0','9');
    wordChars('a','z');
    wordChars('A','Z');
    whitespaceChars(0,' '); 
  }
  
  public void flush() throws IOException {
    eolIsSignificant(true);
    while (nextToken() != EOL) ; // eat tokens until EOL
    eolIsSignificant(false);
  }
  
  public IfForm read() throws IOException {
    
    int token = nextToken();
    
    if (token == WORD) { 
      if (sval.equals("T") || sval.equals("true")) return Constant.TRUE;
      else if (sval.equals("F") || sval.equals("false")) return Constant.FALSE;
      else return Variable.makeVariable(sval);
    }
    else if (token == '(') {
      token = nextToken();
      if (token == '?') {
        IfForm arg1 = read();
        IfForm arg2 = read();
        IfForm arg3 = read();
        token = nextToken(); // read trailing parenthesis
        if (token != ')') 
          throw new ParseException("wrong number of arguments to ?");
        return new If(arg1,arg2,arg3);
      }
      else throw new ParseException("operator " + toString() + 
                                    " not recognized");
    }
    else if (token == EOF) return null;
    else if (token == ')') throw new ParseException("unbalanced ')'");
    else throw new ParseException("operator " + toString() + 
                                  " not recognized");
  }
 
  
  public static void main(String[] args) throws IOException {
    // open file "data" as FormStream 
    FormStream in = new FormStream(new File("data"));
    
    IfForm g = in.read();
    
    int ct = 0;
    while (g != null) {
      ct++;
      IfForm h = g.apply(NormForm.ONLY);
      IfForm i = h.apply(EvalForm.ONLY);
      System.out.println("  " +g+ "\n= " + i + "\n\n");
      // System.out.println("Form " + ct + ": " + k + "\n\n");
      g = in.read();
    }
  }
}

class Variable implements IfForm { 
  static HashMap<String,Variable> symbolTable =
    new HashMap<String,Variable>();
  
  public static Variable makeVariable(String name) {
    Variable result = symbolTable.get(name);
    if (result == null) {
      result = new Variable(name);
      symbolTable.put(name,result);
    }
    return result;
  }
  
  public String name;
  
  private Variable(String name) { this.name = name; }
  
  public String getName() { return name; }
  public String toString() { return name; }
  
  // public boolean equals(Object o);
  // default equals on Object compares pointers which is correct
  
  public <T> T apply(IfFormVisitor<T> v) { return v.forVariable(this); }
}

class Constant implements IfForm {
  
  public static final Constant TRUE = new Constant(true);
  public static final Constant T = TRUE;
  public static final Constant FALSE = new Constant(false);
  public static final Constant F = FALSE;
  
  public boolean value;
  
  private Constant(boolean value) { this.value = value; }
  
  public String toString() { return value ? "T" : "F"; }
  
  public <T> T apply(IfFormVisitor<T> v) { return v.forConstant(this); }
  
  // public boolean equals(Object o);
  // default equals on Object compares pointers which is correct
}

class If implements IfForm {
  
  public IfForm test,conseq,alt;
  
  public If(IfForm test, IfForm conseq, IfForm alt) {
    this.test = test;
    this.conseq = conseq;
    this.alt = alt;
  }
  
  public boolean equals(Object o) {
    if (o == null || o.getClass() != this.getClass()) return false;
    If io = (If) o;
    return test.equals(io.test) && conseq.equals(io.conseq) && alt.equals(io.alt); 
  }
  
  public <T> T apply(IfFormVisitor<T> v) { return v.forIf(this); }
  
  public String toString() {
    return  "(? " + test.toString() + " " + conseq.toString() + " " + alt.toString() + ")";
  }
}


class NormForm implements IfFormVisitor<IfForm> {
  
  public static NormForm ONLY = new NormForm();
  
  private NormForm() { };
  
  private static class HeadNormForm implements IfFormVisitor<IfForm> {
    
    // test, conseq, alt are already normalized 
    
    IfForm conseq, alt;
    
    public HeadNormForm(IfForm conseq, IfForm alt) {
      this.conseq = conseq;
      this.alt = alt;
    }  
    
    public IfForm forVariable(Variable test) { return new If(test, conseq, alt); }
    
    public IfForm forConstant(Constant test) { return new If(test, conseq, alt); } 
    
    public IfForm forIf(If test) {
      return new If(test.test, test.conseq.apply(this), test.alt.apply(this));
    } 
  }
  
  public IfForm forVariable(Variable s) { return s; }     
  public IfForm forConstant(Constant c) { return c; } 
  
  public IfForm forIf(If i) {
    IfForm test = i.test.apply(this);
    IfForm conseq = i.conseq.apply(this);
    IfForm alt = i.alt.apply(this);
    return test.apply(new HeadNormForm(conseq,alt));
  }
}  

class EvalForm implements IfFormVisitor<IfForm> {
  public static EvalForm ONLY = new EvalForm(Environment.empty);
  
  Environment env;
  private EvalForm(Environment e) {
    env = e;
  }
  
  public IfForm forVariable(Variable s) { return env.lookup(s); }     
  public IfForm forConstant(Constant c) { return c; } 
  
  public IfForm forIf(If i) {
    IfForm test = i.test.apply(this);
    if (test instanceof Constant) {
      if (((Constant)test).value) return i.conseq.apply(this);
      else return i.alt.apply(this);
    }
    Variable symtest = (Variable) test;
    IfForm conseq = 
      i.conseq.apply(new EvalForm(env.bind(symtest,Constant.TRUE)));
    IfForm alt =
      i.alt.apply(new EvalForm(env.bind(symtest,Constant.FALSE)));
    if (conseq.equals(alt)) return conseq;
    if ((conseq.equals(Constant.TRUE)) && (alt.equals(Constant.FALSE)))
      
      return symtest;
    
    //if (i.test.equals(test) && i.conseq.equals(conseq) && i.alt.equals(alt)) 
    //  return i;
    return new If(test,conseq,alt);
  }
}