import choco.Problem;
import choco.ContradictionException;
import choco.integer.*;
import choco.Constraint;

public class Test2 {

  
  public static void main(String[] args) {
     Problem pb = new Problem();

     IntDomainVar x = pb.makeEnumIntVar("x",0,2);
     IntDomainVar y = pb.makeEnumIntVar("y",0,2);
     IntDomainVar z = pb.makeEnumIntVar("z",0,2);
     IntDomainVar d = pb.makeEnumIntVar("d",0,1);
     
     Constraint Cxy  = pb.eq(x,y);
     Constraint NCxy = pb.neq(x,y);
     Constraint Cxz  = pb.eq(x,z);
     Constraint NCxz = pb.neq(x,z);
     Constraint Cyz  = pb.lt(y,z);
     Constraint NCyz = pb.geq(y,z);

     Constraint C1  = pb.and(Cxy,pb.and(Cxz,Cyz));
     Constraint C2  = pb.eq(d,0);
     Constraint NC1 = pb.or(NCxy,pb.or(NCxz,NCyz));
     Constraint NC2 = pb.eq(d,1);
     Constraint C3  = pb.or(pb.and(C1,C2),pb.and(NC1,NC2));

     pb.post(C3);

     pb.solve(false);

     System.out.println(pb.pretty());

  }
}