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

formulas(kendoku).
  all x all y1 all y2                          %distinct values on rows x
   ((x < 5) & (y1 < 5) & (y2 < 5) & f(x,y1) = f(x,y2) -> y1 = y2).          

  all y all x1 all x2                       %distinct values on columns y
   ((y < 5) & (x1 < 5) & (x2 < 5) & f(x1,y) = f(x2,y) -> x1 = x2).

  all x all y ((x < 5 & y < 5) -> f(x,y) != 0).%values are from 1 to 5
  all x all y ((x > 4 | y > 4) -> f(x,y)  = 0).%last column and line is 0
end_of_list.

formulas(sample_puzzle).
  f(0,0) + f(1,0) = 4.              f(0,1) / f(1,1) = 2.           %row 0
  f(0,2) * f(0,3) * f(1,2) = 75.    f(0,4) = 2.                    %row 0
  f(1,3) * f(2,3) = 2.                                             %row 1
  f(2,1) * f(2,2) * f(3,1) = 60.    f(2,0) = 5.  f(2,4) = 1.       %row 2
  f(3,0) * f(4,0) * f(4,1) = 8.     f(3,2) * f(4,2) = 2.           %row 3
  abs(f(3,3) + -f(3,4)) = 1.                                       %row 3
  f(4,3) + f(4,4) = 8.                                             %row 4
end_of_list.
