//
// Compare propagation of allDiff with clique of neq
// Note: problem is insoluble
//

import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.cp.solver.CPSolver;
import choco.kernel.model.Model;
import choco.kernel.solver.Solver;
import choco.kernel.model.variables.integer.IntegerVariable;
import choco.kernel.solver.ContradictionException;

import choco.kernel.model.constraints.Constraint;


public class Prop9 {

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

    Model m = new CPModel();

    IntegerVariable w = makeIntVar("W",1,6);
    IntegerVariable x = makeIntVar("X",1,6);
    IntegerVariable y = makeIntVar("Y",1,6);
    IntegerVariable z = makeIntVar("Z",1,6);

    m.addConstraint(gt(w,x));
    m.addConstraint(gt(x,y));
    m.addConstraint(gt(y,z));
    m.addConstraint(gt(z,w));

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

    Solver s = new CPSolver();
    s.read(m);
    s.propagate();

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

    System.out.println(s.solve());
    s.printRuntimeSatistics();
  }
}