import java.util.*;

class Belegung {
  Hashtable table;  // Key=Variable, Value=Wahrheitswert der Variablen
  
  Belegung (Formel formel) {
    table = new Hashtable ();
    formel.init(this);
  }

  void addVariable (Var var) {    // Variable zur Belegung hinzufuegen
    table.put(var,Boolean.FALSE); // und mit FALSE initialisieren
  }

  boolean get (Var var) {  // Wahrheitswert einer Variable holen
    return ((Boolean)table.get (var)).booleanValue();
  }

  void put (Var var, boolean val) {  // Wahrheitswert setzen
    table.put(var, new Boolean(val));
  }

  boolean next () {  // Belegungen von 00...0 bis 11...1 durchzaehlen
    Iterator iterator = table.keySet ().iterator ();

    boolean carry = true;

    while (iterator.hasNext () && carry) {
      Var var = (Var) iterator.next ();
      carry = get (var);
      put (var, !carry);
    }
    return !carry;
  }

  public String toString () {
    return table.toString ();
  }
}
  
    
public abstract class Formel {

  abstract boolean wahrheitswert (Belegung belegung);

  abstract void init (Belegung belegung);

  public boolean erfuellbar () {  // testet Formel auf Erfuellbarkeit
    boolean erfuellbar = false;
    Belegung belegung = new Belegung(this);

    System.out.println ("Gueltige Belegungen:");

    do {
      if (wahrheitswert (belegung)) {
	System.out.println (belegung);  // Git alle Modelle aus
	erfuellbar = true;
      }
    }
    while (belegung.next ());

    System.out.println ("Fertig!");
    return(erfuellbar);
  } 

  public static void main (String args []) {

    // Erstes Beispiel

    Var x = new Var ("A");
    Var y = new Var ("B");
    Var z = new Var ("C");

    Formel formel1 = new Und (new Und (new Oder (x,
						 y),
				       z),
			      new Nicht (x)
			      );
    
    formel1.erfuellbar ();

    // Zweites Beispiel

    Var b = new Var ("Bier");
    Var f = new Var ("Fisch");
    Var e = new Var ("Eis");
    
    Formel formel2 = new Und(new Und(new Implikation(new Nicht(b), 
						     f),
				     new Implikation(new Und(b,f),
						     new Nicht(e))),
			     new Implikation(new Oder(e, new Nicht(b)),
					     new Nicht(f)));
    
    formel2.erfuellbar ();
  }
}


class Var extends Formel {
  String name;

  Var (String _name) {
    name = _name;
  }
  
  void init (Belegung belegung) {
    belegung.put (this, false);
  }

  boolean wahrheitswert (Belegung belegung) {
    return (belegung.get (this));
  }

  public String toString() {
    return(name);
  }
}

class Implikation extends Formel {
  Formel links, rechts;

  Implikation (Formel l, Formel r) {
    links=l;
    rechts=r;
  }

  void init (Belegung belegung) {
    links.init(belegung);
    rechts.init(belegung);
  }

  boolean wahrheitswert (Belegung belegung) {
    return (!links.wahrheitswert (belegung) || rechts.wahrheitswert (belegung));
  }
}


class Und extends Formel {
  Formel links, rechts;

  Und (Formel l, Formel r) {
    links=l;
    rechts=r;
  }

  void init (Belegung belegung) {
    links.init(belegung);
    rechts.init(belegung);
  }

  boolean wahrheitswert (Belegung belegung) {
    return links.wahrheitswert (belegung) && rechts.wahrheitswert (belegung);
  }
}


class Oder extends Formel {
  Formel links, rechts;

  Oder (Formel l, Formel r) {
    links=l;
    rechts=r;
  }

  void init (Belegung belegung) {
    links.init(belegung);
    rechts.init(belegung);
  }

  boolean wahrheitswert (Belegung belegung) {
    return links.wahrheitswert (belegung) || rechts.wahrheitswert (belegung);
  }
}
  

class Nicht extends Formel {
  Formel nachf;

  Nicht (Formel n) {
    nachf=n;
  }

  void init (Belegung belegung) {
    nachf.init(belegung);
  }

  boolean wahrheitswert (Belegung belegung) {
    return !nachf.wahrheitswert (belegung);
  }
}