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

formulas(going_to_church).
  all x (f(x) = 0 | f(x) = 1 | f(x) = 2 | f(x) = 3).           
  f(x) = 0 <-> g(x) = 0 & h(x) = 1.      	               % goes N
  f(x) = 1 <-> g(x) = 1 & h(x) = 0.			       % goes E
  f(x) = 2 <-> g(x) = 1 & h(x) = 1.      		       % goes NE
  f(x) = 3 <-> g(x) = 0 & h(x) = 0.      		       % stays
  
   all x (f(x)  = 3 -> (all y (y > x -> f(y)=3))).
   x < 4 -> f(x) != 3.
  
  ((g(0) + g(1) + g(2) + g(3) = 4) &                             %4 moves
   (h(0) + h(1) + h(2) + h(3) = 4) & 
       (x>3 -> f(x)=3))  |                        
  ((g(0) + g(1) + g(2) + g(3) + g(4) = 4) &                      %5 moves
   (h(0) + h(1) + h(2) + h(3) + h(4) = 4) & 
       (x>4 -> f(x)=3)) |
  ((g(0) + g(1) + g(2) + g(3) + g(4) + g(5) = 4) &               %6 moves
   (h(0) + h(1) + h(2) + h(3) + h(4) + h(5) = 4) & 
       (x>5 -> f(x)=3 )) |
  ((g(0) + g(1) + g(2) + g(3) + g(4) + g(5) + g(6) = 4) &        %7 moves 
   (h(0) + h(1) + h(2) + h(3) + h(4) + h(5) + h(6) = 4) & 
        f(7) = 3)  |
  ((g(0) + g(1) + g(3) + g(4) + g(5) + g(6) + g(2) + g(7) = 4) & %8 moves
   (h(0) + h(1) + h(2) + h(3) + h(4) + h(5) + h(6) + h(7)= 4)).
end_of_list.
