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

type
  Queen [1 .. 15];

variable
  Queen q1;
  Queen q2;
  Queen q3;
  Queen q4;
  Queen q5;
  Queen q6;
  Queen q7;
  Queen q8;
  Queen q9;
  Queen q10;
  Queen q11;
  Queen q12;
  Queen q13;
  Queen q14;
  Queen q15;


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)));
  (((q1 != q8) & (q1 != (q8 - 7))) & (q1 != (q8 + 7)));
  (((q1 != q9) & (q1 != (q9 - 8))) & (q1 != (q9 + 8)));
  (((q1 != q10) & (q1 != (q10 - 9))) & (q1 != (q10 + 9)));
  (((q1 != q11) & (q1 != (q11 - 10))) & (q1 != (q11 + 10)));
  (((q1 != q12) & (q1 != (q12 - 11))) & (q1 != (q12 + 11)));
  (((q1 != q13) & (q1 != (q13 - 12))) & (q1 != (q13 + 12)));
  (((q1 != q14) & (q1 != (q14 - 13))) & (q1 != (q14 + 13)));
  (((q1 != q15) & (q1 != (q15 - 14))) & (q1 != (q15 + 14)));
 
  (((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)));
  (((q2 != q8) & (q2 != (q8 - 6))) & (q2 != (q8 + 6)));
  (((q2 != q9) & (q2 != (q9 - 7))) & (q2 != (q9 + 7)));
  (((q2 != q10) & (q2 != (q10 - 8))) & (q2 != (q10 + 8)));
  (((q2 != q11) & (q2 != (q11 - 9))) & (q2 != (q11 + 9)));
  (((q2 != q12) & (q2 != (q12 - 10))) & (q2 != (q12 + 10)));
  (((q2 != q13) & (q2 != (q13 - 11))) & (q2 != (q13 + 11)));
  (((q2 != q14) & (q2 != (q14 - 12))) & (q2 != (q14 + 12)));
  (((q2 != q15) & (q2 != (q15 - 13))) & (q2 != (q15 + 13)));
 
  (((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)));
  (((q3 != q8) & (q3 != (q8 - 5))) & (q3 != (q8 + 5)));
  (((q3 != q9) & (q3 != (q9 - 6))) & (q3 != (q9 + 6)));
  (((q3 != q10) & (q3 != (q10 - 7))) & (q3 != (q10 + 7)));
  (((q3 != q11) & (q3 != (q11 - 8))) & (q3 != (q11 + 8)));
  (((q3 != q12) & (q3 != (q12 - 9))) & (q3 != (q12 + 9)));
  (((q3 != q13) & (q3 != (q13 - 10))) & (q3 != (q13 + 10)));
  (((q3 != q14) & (q3 != (q14 - 11))) & (q3 != (q14 + 11)));
  (((q3 != q15) & (q3 != (q15 - 12))) & (q3 != (q15 + 12)));
  
  (((q4 != q5) & (q4 != (q5 - 1))) & (q4 != (q5 + 1)));
  (((q4 != q6) & (q4 != (q6 - 2))) & (q4 != (q6 + 2)));
  (((q4 != q7) & (q4 != (q7 - 3))) & (q4 != (q7 + 3)));
  (((q4 != q8) & (q4 != (q8 - 4))) & (q4 != (q8 + 4)));
  (((q4 != q9) & (q4 != (q9 - 5))) & (q4 != (q9 + 5)));
  (((q4 != q10) & (q4 != (q10 - 6))) & (q4 != (q10 + 6)));
  (((q4 != q11) & (q4 != (q11 - 7))) & (q4 != (q11 + 7)));
  (((q4 != q12) & (q4 != (q12 - 8))) & (q4 != (q12 + 8)));
  (((q4 != q13) & (q4 != (q13 - 9))) & (q4 != (q13 + 9)));
  (((q4 != q14) & (q4 != (q14 - 10))) & (q4 != (q14 + 10)));
  (((q4 != q15) & (q4 != (q15 - 11))) & (q4 != (q15 + 11)));
  
  (((q5 != q6) & (q5 != (q6 - 1))) & (q5 != (q6 + 1)));
  (((q5 != q7) & (q5 != (q7 - 2))) & (q5 != (q7 + 2)));
  (((q5 != q8) & (q5 != (q8 - 3))) & (q5 != (q8 + 3)));
  (((q5 != q9) & (q5 != (q9 - 4))) & (q5 != (q9 + 4)));
  (((q5 != q10) & (q5 != (q10 - 5))) & (q5 != (q10 + 5)));
  (((q5 != q11) & (q5 != (q11 - 6))) & (q5 != (q11 + 6)));
  (((q5 != q12) & (q5 != (q12 - 7))) & (q5 != (q12 + 7)));
  (((q5 != q13) & (q5 != (q13 - 8))) & (q5 != (q13 + 8)));
  (((q5 != q14) & (q5 != (q14 - 9))) & (q5 != (q14 + 9)));
  (((q5 != q15) & (q5 != (q15 - 10))) & (q5 != (q15 + 10)));
  
  (((q6 != q7) & (q6 != (q7 - 1))) & (q6 != (q7 + 1)));
  (((q6 != q8) & (q6 != (q8 - 2))) & (q6 != (q8 + 2)));
  (((q6 != q9) & (q6 != (q9 - 3))) & (q6 != (q9 + 3)));
  (((q6 != q10) & (q6 != (q10 - 4))) & (q6 != (q10 + 4)));
  (((q6 != q11) & (q6 != (q11 - 5))) & (q6 != (q11 + 5)));
  (((q6 != q12) & (q6 != (q12 - 6))) & (q6 != (q12 + 6)));
  (((q6 != q13) & (q6 != (q13 - 7))) & (q6 != (q13 + 7)));
  (((q6 != q14) & (q6 != (q14 - 8))) & (q6 != (q14 + 8)));
  (((q6 != q15) & (q6 != (q15 - 9))) & (q6 != (q15 + 9)));
  
  (((q7 != q8) & (q7 != (q8 - 1))) & (q7 != (q8 + 1)));
  (((q7 != q9) & (q7 != (q9 - 2))) & (q7 != (q9 + 2)));
  (((q7 != q10) & (q7 != (q10 - 3))) & (q7 != (q10 + 3)));
  (((q7 != q11) & (q7 != (q11 - 4))) & (q7 != (q11 + 4)));
  (((q7 != q12) & (q7 != (q12 - 5))) & (q7 != (q12 + 5)));
  (((q7 != q13) & (q7 != (q13 - 6))) & (q7 != (q13 + 6)));
  (((q7 != q14) & (q7 != (q14 - 7))) & (q7 != (q14 + 7)));
  (((q7 != q15) & (q7 != (q15 - 8))) & (q7 != (q15 + 8)));
  
  (((q8 != q9) & (q8 != (q9 - 1))) & (q8 != (q9 + 1)));
  (((q8 != q10) & (q8 != (q10 - 2))) & (q8 != (q10 + 2)));
  (((q8 != q11) & (q8 != (q11 - 3))) & (q8 != (q11 + 3)));
  (((q8 != q12) & (q8 != (q12 - 4))) & (q8 != (q12 + 4)));
  (((q8 != q13) & (q8 != (q13 - 5))) & (q8 != (q13 + 5)));
  (((q8 != q14) & (q8 != (q14 - 6))) & (q8 != (q14 + 6)));
  (((q8 != q15) & (q8 != (q15 - 7))) & (q8 != (q15 + 7)));
  
  (((q9 != q10) & (q9 != (q10 - 1))) & (q9 != (q10 + 1)));
  (((q9 != q11) & (q9 != (q11 - 2))) & (q9 != (q11 + 2)));
  (((q9 != q12) & (q9 != (q12 - 3))) & (q9 != (q12 + 3)));
  (((q9 != q13) & (q9 != (q13 - 4))) & (q9 != (q13 + 4)));
  (((q9 != q14) & (q9 != (q14 - 5))) & (q9 != (q14 + 5)));
  (((q9 != q15) & (q9 != (q15 - 6))) & (q9 != (q15 + 6)));
  
  (((q10 != q11) & (q10 != (q11 - 1))) & (q10 != (q11 + 1)));
  (((q10 != q12) & (q10 != (q12 - 2))) & (q10 != (q12 + 2)));
  (((q10 != q13) & (q10 != (q13 - 3))) & (q10 != (q13 + 3)));
  (((q10 != q14) & (q10 != (q14 - 4))) & (q10 != (q14 + 4)));
  (((q10 != q15) & (q10 != (q15 - 5))) & (q10 != (q15 + 5)));
  
  (((q11 != q12) & (q11 != (q12 - 1))) & (q11 != (q12 + 1)));
  (((q11 != q13) & (q11 != (q13 - 2))) & (q11 != (q13 + 2)));
  (((q11 != q14) & (q11 != (q14 - 3))) & (q11 != (q14 + 3)));
  (((q11 != q15) & (q11 != (q15 - 4))) & (q11 != (q15 + 4)));

  (((q12 != q13) & (q12 != (q13 - 1))) & (q12 != (q13 + 1)));
  (((q12 != q14) & (q12 != (q14 - 2))) & (q12 != (q14 + 2)));
  (((q12 != q15) & (q12 != (q15 - 3))) & (q12 != (q15 + 3)));

  (((q13 != q14) & (q13 != (q14 - 1))) & (q13 != (q14 + 1)));
  (((q13 != q15) & (q13 != (q15 - 2))) & (q13 != (q15 + 2)));
  
  (((q14 != q15) & (q14 != (q15 - 1))) & (q14 != (q15 + 1)));