set(arithmetic).
assign(domain_size,5).  
assign(max_models,-1).  

formulas(magic_labyrinth).
  f(x,y) != 4.
  f(x,y1) !=0 -> (f(x,y1) = f(x,y2)  -> y1 = y2).  %distinct if not empty
  f(x1,y) !=0 -> (f(x1,y) = f(x2,y)  -> x1 = x2).  %distinct if not empty
  f(x,0) + f(x,1) + f(x,2) + f(x,3) + f(x,4) = 6.  %1+2+3=6
    
  all y1 all y2 ((y1 < y2 & f(0,y1) != 0 & f(0,y2) != 0)         %seg. 1
     -> f(0,y1) < f(0,y2)).                                     
  all x1 all x2 ((x1 < x2 & f(x1,4) != 0 & f(x2,4) != 0          %seg. 2
      & f(0,4) != 3) -> f(x1,4) < f(x2,4)).                       
  all y1 all y2 ((y1 < y2 & f(4,y1) != 0 & f(4,y2) != 0          %seg. 3
      & f(4,4) != 3) -> f(4,y1) > f(4,y2)).        
  all x1 all x2 ((x1 < x2 & f(x1,0) != 0 & f(x2,0) != 0          %seg. 4  
      & f(4,0) != 3 & x1 != 0) -> f(x1,0) > f(x2,0)).        
  
  all y1 all y2 ((y1 < y2 & f(1,y1) != 0 & f(1,y2) != 0          %seg. 5  
      & f(1,0) != 3 & y2 < 4) -> f(1,y1) < f(1,y2)).             
  all x1 all x2 ((x1 < x2 & f(x1,3) != 0 & f(x2,3) != 0          %seg. 6
      & f(1,3) != 3 & x1 > 0 & x2 < 4) -> f(x1,3) < f(x2,3)).     
  all y1 all y2 ((y1 < y2 & f(3,y1) != 0 & f(3,y2) != 0          %seg. 7
      & f(3,3) !=3 & y1 > 0 & y2 < 4) -> f(3,y1) > f(3,y2)).        
end_of_list.

formulas(sample_puzzle).
  f(0,3) = 3. f(1,1) = 3. f(1,4) = 1. f(3,3) = 2. f(4,0) = 3.
end_of_list.
