assign(domain_size,12).   
assign(max_models,2).   
set(arithmetic).

formulas(utils).
  all x all y (less(x,y) < 2 & greater(x,y) < 2 & equal(x,y) < 2).
  less(x,y) = 1 -> (x <= y).     
  less(x,y) = 0 -> (x > y).
  greater(x,y) = 1 -> (x >= y).  
  greater(x,y) = 0 -> (x < y).
  equal(x,y) = 1 -> (x = 1 & y = 1).
  equal(x,y) = 0 -> (x  != 1  | y !=  1).
  f(x,y) = equal(less(c(x),y),greater(c(x),y)).
  h(x)   = f(0,x) + f(1,x) + f(2,x) + f(3,x) + f(4,x) + 
           f(5,x) + f(6,x) + f(7,x) + f(8,x) + f(9,x).   
end_of_list. 

formulas(self_counting_sentence).  
  c(0) = 1 | c(0) = 2 | c(0)=3. 
  c(1) != 1. 
  all x ((x > 1 & x <10)  -> (c(x) = 1 | c(x) = 2 |c(x) =3)).
    
  c(0) = 1 + h(10).                   %value 1 appears once in number 10
         
  %value 1 appears once in numbers 1 or 10, and twice in 11
  c(1) = 1 + 2 * h(11) + h(1) + h(10).
                     
  (x > 1 & x <10) -> c(x) =  1 + h(x). %value x appears once in number x
  
  all x  (x > 9 -> c(x) = 11).         %avoid isomorphic models
end_of_list.
