// Description:  7 queen problem
// Author:  CLab# Crew
// Date:  2006-01-25

type
  Queen [1 .. 7];

variable
  Queen q1;
  Queen q2;
  Queen q3;
  Queen q4;
  Queen q5;
  Queen q6;
  Queen q7;

rule
  (((q1 != q2) & (q1 != (q2 - 1))) & (q1 != (q2 + 1)));
  (((q1 != q3) & (q1 != (q3 - 2))) & (q1 != (q3 + 2)));
  (((q1 != q4) & (q1 != (q4 - 3))) & (q1 != (q4 + 3)));
  (((q1 != q5) & (q1 != (q5 - 4))) & (q1 != (q5 + 4)));
  (((q1 != q6) & (q1 != (q6 - 5))) & (q1 != (q6 + 5)));
  (((q1 != q7) & (q1 != (q7 - 6))) & (q1 != (q7 + 6)));
  (((q2 != q3) & (q2 != (q3 - 1))) & (q2 != (q3 + 1)));
  (((q2 != q4) & (q2 != (q4 - 2))) & (q2 != (q4 + 2)));
  (((q2 != q5) & (q2 != (q5 - 3))) & (q2 != (q5 + 3)));
  (((q2 != q6) & (q2 != (q6 - 4))) & (q2 != (q6 + 4)));
  (((q2 != q7) & (q2 != (q7 - 5))) & (q2 != (q7 + 5)));
  (((q3 != q4) & (q3 != (q4 - 1))) & (q3 != (q4 + 1)));
  (((q3 != q5) & (q3 != (q5 - 2))) & (q3 != (q5 + 2)));
  (((q3 != q6) & (q3 != (q6 - 3))) & (q3 != (q6 + 3)));
  (((q3 != q7) & (q3 != (q7 - 4))) & (q3 != (q7 + 4)));
  (((q4 != q5) & (q4 != (q5 - 1))) & (q4 != (q5 + 1)));
  (((q4 != q6) & (q4 != (q6 - 2))) & (q4 != (q6 + 2)));
  (((q4 != q7) & (q4 != (q7 - 3))) & (q4 != (q7 + 3)));
  (((q5 != q6) & (q5 != (q6 - 1))) & (q5 != (q6 + 1)));
  (((q5 != q7) & (q5 != (q7 - 2))) & (q5 != (q7 + 2)));
  (((q6 != q7) & (q6 != (q7 - 1))) & (q6 != (q7 + 1)));