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

formulas(demodulators).
  x<19 -> s(x) = x+1.           s(19)=0.
  c(0)=0  | c(0)=1  | c(0)=2  | c(0)=3.     %start with AB, AC, AD, AE
  c(9)=10 | c(9)=11 | c(9)=12 | c(9)=13.    %end with   BA, CA, DA, EA
  x>9 -> c(x)=0.                            %there are only 10 edges
end_of_list.

formulas(assumptions).  
 all x all y ((x != y & x <= 9 & y <= 9) -> (c(x) != c(y))).
 all x all y ((x = y  & x <= 9 & y <= 9) -> (c(x) = c(y))).
 %if car uses XY then it cannot use YX (XY + 10 = YX)
 all x all y all z ((z < 10 & c(x) = z & x != y) -> (c(y) != z + 10)). 
  
 %continutiy between edges
 all x ((x<9 & c(x)=0)  -> ((c(s(x))=4)  | (c(s(x))=5)  | (c(s(x))=6))).
 all x ((x<9 & c(x)=1)  -> ((c(s(x))=7)  | (c(s(x))=8)  | (c(s(x))=14))).
 all x ((x<9 & c(x)=2)  -> ((c(s(x))=9)  | (c(s(x))=15) | (c(s(x))=17))).
 all x ((x<9 & c(x)=3)  -> ((c(s(x))=16) | (c(s(x))=18) | (c(s(x))=19))).
 all x ((x<9 & c(x)=4)  -> ((c(s(x))=7)  | (c(s(x))=8)  | (c(s(x))=11))).
 all x ((x<9 & c(x)=5)  -> ((c(s(x))=9)  | (c(s(x))=12) | (c(s(x))=17))).
 all x ((x<9 & c(x)=6)  -> ((c(s(x))=13) | (c(s(x))=18) | (c(s(x))=19))).
 all x ((x<9 & c(x)=7)  -> ((c(s(x))=9)  | (c(s(x))=12) | (c(s(x))=15))).
 all x ((x<9 & c(x)=8)  -> ((c(s(x))=13) | (c(s(x))=16) | (c(s(x))=19))).
 all x ((x<9 & c(x)=9)  -> ((c(s(x))=13) | (c(s(x))=16) | (c(s(x))=18))).
 all x ((x<9 & c(x)=10) -> ((c(s(x))=1)  | (c(s(x))=2)  | (c(s(x))=3))).
 all x ((x<9 & c(x)=11) -> ((c(s(x))=0)  | (c(s(x))=2)  | (c(s(x))=3))).
 all x ((x<9 & c(x)=12) -> ((c(s(x))=0)  | (c(s(x))=1)  | (c(s(x))=3))).
 all x ((x<9 & c(x)=13) -> ((c(s(x))=0)  | (c(s(x))=1)  | (c(s(x))=2))).
 all x ((x<9 & c(x)=14) -> ((c(s(x))=5)  | (c(s(x))=6)  | (c(s(x))=10))).
 all x ((x<9 & c(x)=15) -> ((c(s(x))=4)  | (c(s(x))=6)  | (c(s(x))=10))).
 all x ((x<9 & c(x)=16) -> ((c(s(x))=4)  | (c(s(x))=5)  | (c(s(x))=10))).
 all x ((x<9 & c(x)=17) -> ((c(s(x))=8)  | (c(s(x))=11) | (c(s(x))=14))).
 all x ((x<9 & c(x)=18) -> ((c(s(x))=7)  | (c(s(x))=11) | (c(s(x))=14))).
 all x ((x<9 & c(x)=19) -> ((c(s(x))=12) | (c(s(x))=15) | (c(s(x))=17))).
end_of_list.
