//
// csp6
// from AR33, figure 18, page 35
//

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

public class CSP6lite {

  
  public static void main(String[] args) throws ContradictionException {

     Problem pb = new Problem();

     IntDomainVar v1  = pb.makeEnumIntVar("v1",1,5);
     IntDomainVar v2  = pb.makeEnumIntVar("v2",1,5);
     IntDomainVar v3  = pb.makeEnumIntVar("v3",1,5);
     IntDomainVar v4  = pb.makeEnumIntVar("v4",1,5);
 
     pb.post(pb.lt(v1,v2));               // v1 < v2
     pb.post(pb.lt(v4,v3));               // v4 < v3
     pb.post(pb.eq(pb.plus(v4,v2),5));    // v4 + v2 = 5
     pb.post(pb.gt(pb.plus(v2,v3),6));    // v2 + v3 > 6
     pb.post(pb.leq(v1,pb.minus(v4,1)));  // v1 <= v4 - 1

     pb.propagate();

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